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.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

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

module MIU where

data Symbol : Set where
  I : Symbol
  U : Symbol

open import Data.List

Word : Set
Word = List Symbol

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

#![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

#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

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

open import Agda.Builtin.FromNat
open import Data.Fin

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Nat renaming (_≤?_ to _N≤?_)
open import Data.Unit

instance
  NumFin : ∀ {n} → Number (Fin n)

gergoerdi

{-# OPTIONS --cubical #-}
module Quotient where

open import Cubical.Core.Prelude

Reflexive : ∀ {ℓ} {A : Set ℓ} → (A → A → Set ℓ) → Set _
Reflexive _∼_ = ∀ x → x ∼ x

module Quot {ℓ} (A : Set ℓ) (_∼_ : A → A → Set ℓ) (∼-refl : Reflexive _∼_) where
  data Q : Set ℓ where