gergoerdi

open import Data.Nat
open import Relation.Binary.PropositionalEquality renaming (subst to ≡-subst)
open import Data.Empty
open import Data.Unit
open import Relation.Binary
open import Data.Star
open import Level renaming (zero to lzero; suc to lsuc)
open import Data.Product
open import Function using (_⟨_⟩_)
-- open import Function using (_∘_; id)

gergoerdi

#include "sim_avr.h"
#include "avr_ioport.h"
#include "sim_elf.h"

#include <stdio.h>

void ext_cb(struct avr_irq_t* irq, uint32_t val, void* closure)
{
    avr_irq_t *trigger = (avr_irq_t*)(closure);

gergoerdi

#![feature(lang_items)]
#![feature(fundamental)]
#![feature(intrinsics)]
#![feature(on_unimplemented)]
#![feature(optin_builtin_traits)]
#![feature(unboxed_closures)]
#![feature(associated_type_defaults)]
#![feature(asm)]
#![feature(abi_avr_interrupt)]
#![feature(unwind_attributes)]

gergoerdi

module _ where

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Relation.Nullary
open import Data.Empty

-- Untyped lambda calculus, with "weak" names
module _ where

gergoerdi

{-# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}

import GHC.TypeLits
import GHC.Types
import Data.Singletons
import Data.Singletons.Prelude

data Format = Lit Symbol | Str | Shown Type

gergoerdi

fib' :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer
fib' (p, q) (x0, x1) n = go n (p, q) (x0, x1)
  where
    go 0 (p, q) (x0, x1) = x0
    go n (p, q) (x0, x1) = if odd then go (n-1) (p, q) $! step (p, q) (x0, x1)
                           else go n' (p', q') (x0, x1)
      where
        (n', b) = n `divMod` 2
        odd = not (b == 0)

gergoerdi

-- https://stackoverflow.com/questions/34388484/parametricity-exploiting-proofs-in-agda

PolyFun : Set → Set1
PolyFun A = ∀ {X : Set} → A → X → A

open import Relation.Binary.PropositionalEquality

Parametricity : {A : Set} → Set _
Parametricity {A} = ∀ {X Y} → (f : PolyFun A) → ∀ a x y → f {X} a x ≡ f {Y} a y

gergoerdi

open import Data.Product
open import Function using (_∘_; id)

data Cont : Set₁ where
  _<|_ : (S : Set) → (P : S → Set) → Cont

[_]C : Cont → Set → Set
[ S <| P ]C X = Σ[ s ∈ S ] (P s → X)

gergoerdi

open import Data.List
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) renaming (map to mapSum)
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality

Con : Set → Set
Con = List

data Var {A : Set} (t : A) : Con A → Set where
  here : ∀ {Γ : Con A} → Var t (t ∷ Γ)

gergoerdi

import Data.Vect
import Data.Fin

%default total

fins : Vect n (Fin n)
fins {n = Z} = []
fins {n = S n} = FZ :: map FS fins

Permutation : Nat -> Type