added various files in extra

src/extra/Addition.agda

@@ -0,0 +1,27 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; cong)
+open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+open import Data.Nat using (ℕ; zero; suc)
+
+
+_+_ : ℕ → ℕ → ℕ
+zero + n = n
+suc m + n = suc (m + n)
+
++-assoc′ : ∀ m n p → (m + n) + p ≡ m + (n + p)
++-assoc′ zero n p = refl
++-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl
+
+
+{-
+Goal: ℕ
+————————————————————————————————————————————————————————————
+n : ℕ
+-}
+
+{-
+Goal: ℕ
+————————————————————————————————————————————————————————————
+n : ℕ
+m : ℕ
+-}

src/extra/CPP.lagda

@@ -0,0 +1,122 @@
+\begin{code}
+module CPP where
+
+open import Data.List hiding ([_])
+open import Function
+
+data Type : Set where
+  base : Type
+  arr  : Type → Type → Type
+
+Cx' = List Type
+Model' = Type → Cx' → Set
+
+infixr 8 _⇒_
+_⇒_ : (Cx' → Set) → (Cx' → Set) → Cx' → Set
+(f ⇒ g) Γ = f Γ → g Γ
+
+[_]' : (Cx' → Set) → Set
+[ P ]' = ∀ {x} → P x
+
+infix 9 _⊢_
+_⊢_ : Type → (Cx' → Set) → Cx' → Set
+(σ ⊢ T) Γ = T (σ ∷ Γ)
+
+
+data Var : Model' where
+  ze : ∀ {σ} → [ σ ⊢ Var σ ]'
+  su : ∀ {σ τ} → [ Var σ ⇒ τ ⊢ Var σ ]'
+
+□ : (Cx' → Set) → (Cx' → Set)
+□ P Γ = ∀ {Δ} → (∀ {σ} → Var σ Γ → Var σ Δ) → P Δ
+
+
+data Tm : Model' where
+  `var : ∀ {σ} → [ Var σ ⇒ Tm σ ]'
+  _`$_ : ∀ {σ τ} → [ Tm (arr σ τ) ⇒ Tm σ ⇒ Tm τ ]'
+  `λ   : ∀ {σ τ} → [ σ ⊢ Tm τ ⇒ Tm (arr σ τ) ]'
+\end{code}
+%<*ren>
+\begin{code}
+ren : {Γ Δ : List Type} → (∀ {σ} → Var σ Γ → Var σ Δ) → (∀ {σ} → Tm σ Γ → Tm σ Δ)
+ren ρ (`var v)  = `var (ρ v)
+ren ρ (f `$ t)  = ren ρ f `$ ren ρ t
+ren ρ (`λ b)    = `λ (ren ((su ∘ ρ) -, ze) b)
+\end{code}
+%</ren>
+\begin{code}
+  where 
+
+  _-,_ : ∀ {Γ σ Δ} → (∀ {τ} → Var τ Γ → Var τ Δ) → Var σ Δ → ∀ {τ} → Var τ (σ ∷ Γ) → Var τ Δ
+  (ρ -, v) ze     = v
+  (ρ -, v) (su k) = ρ k
+\end{code}
+%<*sub>
+\begin{code}
+sub : {Γ Δ : List Type} → (∀ {σ} → Var σ Γ → Tm σ Δ) → (∀ {σ} → Tm σ Γ → Tm σ Δ)
+sub ρ (`var v)  = ρ v
+sub ρ (f `$ t)  = sub ρ f `$ sub ρ t
+sub ρ (`λ b)    = `λ (sub ((ren su ∘ ρ) -, `var ze) b)
+\end{code}
+%</sub>
+\begin{code}
+  where
+
+  _-,_ :  ∀ {Γ σ Δ} → (∀ {τ} → Var τ Γ → Tm τ Δ) → Tm σ Δ → ∀ {τ} → Var τ (σ ∷ Γ) → Tm τ Δ
+  (ρ -, v) ze     = v
+  (ρ -, v) (su k) = ρ k
+
+record Kit (◆ : Model') : Set where
+  field
+    var : ∀ {σ} → [ ◆ σ ⇒ Tm σ ]'
+    zro : ∀ {σ} → [ σ ⊢ ◆ σ ]'
+    wkn : ∀ {σ τ} → [ ◆ τ ⇒ σ ⊢ ◆ τ ]'
+
+module kitkit {◆ : Model'} (κ : Kit ◆) where
+\end{code}
+%<*kit>
+\begin{code}
+ kit : {Γ Δ : List Type} → (∀ {σ} → Var σ Γ → ◆ σ Δ) → (∀ {σ} → Tm σ Γ → Tm σ Δ)
+ kit ρ (`var v)  = Kit.var κ (ρ v)
+ kit ρ (f `$ t)  = kit ρ f `$ kit ρ t
+ kit ρ (`λ b)    = `λ (kit ((Kit.wkn κ ∘ ρ) -, Kit.zro κ) b)
+\end{code}
+%</kit>
+\begin{code}
+    where
+
+    _-,_ :  ∀ {Γ σ Δ} → (∀ {τ} → Var τ Γ → ◆ τ Δ) → ◆ σ Δ → ∀ {τ} → Var τ (σ ∷ Γ) → ◆ τ Δ
+    (ρ -, v) ze    = v
+    (ρ -, v) (su k) = ρ k
+
+Val : Model'
+Val base      Γ = Tm base Γ
+Val (arr σ τ) Γ = ∀ {Δ} → (∀ {ν} → Var ν Γ → Var ν Δ) → Val σ Δ → Val τ Δ
+
+wk : ∀ {Γ Δ} → (∀ {σ} → Var σ Γ → Var σ Δ) → ∀ {σ} → Val σ Γ → Val σ Δ
+wk ρ {base}    v = ren ρ v
+wk ρ {arr σ τ} v = λ ρ′ → v (ρ′ ∘ ρ)
+
+APP : ∀ {σ τ Γ} → Val (arr σ τ) Γ →  Val σ Γ → Val τ Γ
+APP f t = f id t
+
+LAM : ∀ {Γ σ τ} → Val (arr σ τ) Γ → Val (arr σ τ) Γ
+LAM = id
+\end{code}
+%<*nbe>
+\begin{code}
+nbe : {Γ Δ : List Type} → (∀ {σ} → Var σ Γ → Val σ Δ) → (∀ {σ} → Tm σ Γ → Val σ Δ)
+nbe ρ (`var v)    = ρ v
+nbe ρ (f `$ t)  = APP (nbe ρ f) (nbe ρ t)
+nbe ρ (`λ t)    = LAM (λ re v → nbe ((wk re ∘ ρ) -, v) t)
+\end{code}
+%</nbe>
+\begin{code}
+  where
+
+  _-,_ : ∀ {Γ σ Δ} → (∀ {τ} → Var τ Γ → Val τ Δ) → Val σ Δ → ∀ {τ} → Var τ (σ ∷ Γ) → Val τ Δ
+  (ρ -, v) ze     = v
+  (ρ -, v) (su k) = ρ k
+\end{code}
+
+

src/extra/DaraisPhoas.agda

@@ -0,0 +1,90 @@
+module DaraisPhoas where
+
+open import Agda.Primitive using (_⊔_)
+
+module Prelude where
+
+  infixr 3 ∃𝑠𝑡
+  infixl 5 _∨_
+  infixr 20 _∷_
+  
+  data 𝔹 : Set where
+    T : 𝔹
+    F : 𝔹
+
+  data _∨_ {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
+    Inl : A → A ∨ B
+    Inr : B → A ∨ B
+
+  syntax ∃𝑠𝑡 A (λ x → B) = ∃ x ⦂ A 𝑠𝑡 B
+  data ∃𝑠𝑡 {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
+    ⟨∃_,_⟩ : ∀ (x : A) → B x → ∃ x ⦂ A 𝑠𝑡 B x
+
+  data ⟬_⟭ {ℓ} (A : Set ℓ) : Set ℓ where
+    [] : ⟬ A ⟭
+    _∷_ : A → ⟬ A ⟭ → ⟬ A ⟭
+
+open Prelude
+
+infixr 15 _⟨→⟩_
+data type : Set where
+  ⟨ℕ⟩   : type
+  _⟨→⟩_ : type → type → type
+
+infixl 15 _⟨∙⟩_
+data exp-phoas (var : type → ⟬ type ⟭ → Set) : ∀ (Γ : ⟬ type ⟭) (τ : type) → Set where
+  Var : ∀ {Γ τ}
+    (x : var τ Γ)
+    → exp-phoas var Γ τ
+  ⟨λ⟩ : ∀ {Γ τ₁ τ₂}
+    (e : var τ₁ (τ₁ ∷ Γ) → exp-phoas var (τ₁ ∷ Γ) τ₂)
+    → exp-phoas var Γ (τ₁ ⟨→⟩ τ₂)
+  _⟨∙⟩_ : ∀ {Γ τ₁ τ₂}
+    (e₁ : exp-phoas var Γ (τ₁ ⟨→⟩ τ₂))
+    (e₂ : exp-phoas var Γ τ₁)
+    → exp-phoas var Γ τ₂
+
+infix 10 _∈_
+data _∈_ {ℓ} {A : Set ℓ} (x : A) : ∀ (xs : ⟬ A ⟭) → Set ℓ where
+  Z : ∀ {xs} → x ∈ x ∷ xs
+  S : ∀ {x′ xs} → x ∈ xs → x ∈ x′ ∷ xs
+
+infix 10 _⊢_
+data _⊢_ : ∀ (Γ : ⟬ type ⟭) (τ : type) → Set where
+  Var : ∀ {Γ τ}
+    (x : τ ∈ Γ)
+    → Γ ⊢ τ
+  ⟨λ⟩ : ∀ {Γ τ₁ τ₂}
+    (e : τ₁ ∷ Γ ⊢ τ₂)
+    → Γ ⊢ τ₁ ⟨→⟩ τ₂
+  _⟨∙⟩_ : ∀ {Γ τ₁ τ₂}
+    (e₁ : Γ ⊢ τ₁ ⟨→⟩ τ₂)
+    (e₂ : Γ ⊢ τ₁)
+    → Γ ⊢ τ₂
+
+⟦_⟧₁ : ∀ {Γ τ} (e : exp-phoas _∈_ Γ τ) → Γ ⊢ τ
+⟦ Var x ⟧₁ = Var x
+⟦ ⟨λ⟩ e ⟧₁ = ⟨λ⟩ ⟦ e Z ⟧₁
+⟦ e₁ ⟨∙⟩ e₂ ⟧₁ = ⟦ e₁ ⟧₁ ⟨∙⟩ ⟦ e₂ ⟧₁
+
+⟦_⟧₂ : ∀ {Γ τ} (e : Γ ⊢ τ) → exp-phoas _∈_ Γ τ
+⟦ Var x ⟧₂ = Var x
+⟦ ⟨λ⟩ e ⟧₂ = ⟨λ⟩ (λ _ → ⟦ e ⟧₂)
+⟦ e₁ ⟨∙⟩ e₂ ⟧₂ = ⟦ e₁ ⟧₂ ⟨∙⟩ ⟦ e₂ ⟧₂
+
+Ch : type
+Ch =  (⟨ℕ⟩ ⟨→⟩ ⟨ℕ⟩) ⟨→⟩ ⟨ℕ⟩ ⟨→⟩ ⟨ℕ⟩
+
+twoDB : [] ⊢ Ch
+twoDB = ⟨λ⟩ (⟨λ⟩ (Var (S Z) ⟨∙⟩ (Var (S Z) ⟨∙⟩ Var Z)))
+
+twoPH : exp-phoas _∈_ [] Ch
+twoPH = ⟨λ⟩ (λ f → ⟨λ⟩ (λ x → Var f ⟨∙⟩ (Var f ⟨∙⟩ Var x)))
+
+{-
+/Users/wadler/sf/src/extra/DaraisPhoas.agda:82,9-60
+⟨ℕ⟩ ⟨→⟩ ⟨ℕ⟩ != ⟨ℕ⟩ of type type
+when checking that the expression
+⟨λ⟩ (λ f → ⟨λ⟩ (λ x → Var f ⟨∙⟩ (Var f ⟨∙⟩ Var x))) has type
+exp-phoas _∈_ [] Ch
+-}

src/extra/DeBruijn-agda-list-3.lagda

@@ -0,0 +1,200 @@
+Many thanks to Nils and Roman.
+
+Attached find an implementation along the lines sketched by Roman;
+I found it after I sent my request and before Roman sent his helpful
+reply.
+
+One thing I note, in both Roman's code and mine, is that the code to
+decide whether two contexts are equal is lengthy (_≟T_ and _≟_,
+below).  Is there a better way to do it?  Does Agda offer an
+equivalent of Haskell's derivable for equality?
+
+Cheers, -- P
+
+[Version using Ulf's prelude to derive equality]
+
+## Imports
+
+\begin{code}
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Data.Nat using (ℕ; zero; suc; _+_; _∸_)
+open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Nullary.Decidable using (map)
+open import Relation.Nullary.Negation using (contraposition)
+open import Relation.Nullary.Product using (_×-dec_)
+open import Data.Unit using (⊤; tt)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Function using (_∘_)
+open import Function.Equivalence using (_⇔_; equivalence)
+\end{code}
+
+## Typed DeBruijn
+
+\begin{code}
+infixr 5 _⇒_
+
+data Type : Set where
+  o : Type
+  _⇒_ : Type → Type → Type
+
+data Env : Set where
+  ε : Env
+  _,_ : Env → Type → Env
+
+data Var : Env → Type → Set where
+  Z : ∀ {Γ : Env} {A : Type} → Var (Γ , A) A
+  S : ∀ {Γ : Env} {A B : Type} → Var Γ B → Var (Γ , A) B
+
+data Exp : Env → Type → Set where
+  var : ∀ {Γ : Env} {A : Type} → Var Γ A → Exp Γ A
+  abs : ∀ {Γ : Env} {A B : Type} → Exp (Γ , A) B → Exp Γ (A ⇒ B)
+  app : ∀ {Γ : Env} {A B : Type} → Exp Γ (A ⇒ B) → Exp Γ A → Exp Γ B
+\end{code}
+
+## Untyped DeBruijn
+
+\begin{code}
+data DB : Set where
+  var : ℕ → DB
+  abs : DB → DB
+  app : DB → DB → DB
+\end{code}
+
+# PHOAS
+
+\begin{code}
+data PH (X : Type → Set) : Type → Set where
+  var : ∀ {A : Type} → X A → PH X A
+  abs : ∀ {A B : Type} → (X A → PH X B) → PH X (A ⇒ B)
+  app : ∀ {A B : Type} → PH X (A ⇒ B) → PH X A → PH X B
+\end{code}
+
+# Convert PHOAS to DB
+
+\begin{code}
+PH→DB : ∀ {A} → (∀ {X} → PH X A) → DB
+PH→DB M = h M 0
+  where
+  K : Type → Set
+  K A = ℕ
+
+  h : ∀ {A} → PH K A → ℕ → DB
+  h (var k) j    =  var (j ∸ (k + 1))
+  h (abs N) j    =  abs (h (N j) (j + 1))
+  h (app L M) j  =  app (h L j) (h M j)
+\end{code}
+
+# Test examples
+
+\begin{code}
+Church : Type
+Church = (o ⇒ o) ⇒ o ⇒ o
+
+twoExp : Exp ε Church
+twoExp = (abs (abs (app (var (S Z)) (app (var (S Z)) (var Z)))))
+
+twoPH : ∀ {X} → PH X Church
+twoPH = (abs (λ f → (abs (λ x → (app (var f) (app (var f) (var x)))))))
+
+twoDB : DB
+twoDB = (abs (abs (app (var 1) (app (var 1) (var 0)))))
+
+ex : PH→DB twoPH ≡ twoDB
+ex = refl
+\end{code}
+
+## Decide whether environments and types are equal
+
+\begin{code}
+-- These two imports are from agda-prelude (https://github.com/UlfNorell/agda-prelude)
+open import Tactic.Deriving.Eq using (deriveEq)
+import Prelude
+
+instance
+  unquoteDecl EqType = deriveEq EqType (quote Type)
+  unquoteDecl EqEnv  = deriveEq EqEnv  (quote Env)
+
+⊥To⊥ : Prelude.⊥ → ⊥
+⊥To⊥ ()
+
+decToDec : ∀ {a} {A : Set a} → Prelude.Dec A → Dec A
+decToDec (Prelude.yes x) = yes x
+decToDec (Prelude.no nx) = no (⊥To⊥ ∘ nx)
+
+_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
+A ≟T B = decToDec (A Prelude.== B)
+
+_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
+Γ ≟ Δ = decToDec (Γ Prelude.== Δ)
+\end{code}
+
+[Old version, no longer needed]
+
+_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
+o ≟T o = yes refl
+o ≟T (A′ ⇒ B′) = no (λ())
+(A ⇒ B) ≟T o = no (λ())
+(A ⇒ B) ≟T (A′ ⇒ B′) = map (equivalence obv1 obv2) ((A ≟T A′) ×-dec (B ≟T B′))
+  where
+  obv1 : ∀ {A B A′ B′ : Type} → (A ≡ A′) × (B ≡ B′) → A ⇒ B ≡ A′ ⇒ B′
+  obv1 ⟨ refl , refl ⟩ = refl
+  obv2 : ∀ {A B A′ B′ : Type} → A ⇒ B ≡ A′ ⇒ B′ → (A ≡ A′) × (B ≡ B′)
+  obv2 refl = ⟨ refl , refl ⟩
+
+_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
+ε ≟ ε = yes refl
+ε ≟ (Γ , A) = no (λ())
+(Γ , A) ≟ ε = no (λ())
+(Γ , A) ≟ (Δ , B) = map (equivalence obv1 obv2) ((Γ ≟ Δ) ×-dec (A ≟T B))
+  where
+  obv1 : ∀ {Γ Δ A B} → (Γ ≡ Δ) × (A ≡ B) → (Γ , A) ≡ (Δ , B)
+  obv1 ⟨ refl , refl ⟩ = refl
+  obv2 : ∀ {Γ Δ A B} → (Γ , A) ≡ (Δ , B) → (Γ ≡ Δ) × (A ≡ B)
+  obv2 refl = ⟨ refl , refl ⟩
+
+## Convert Phoas to Exp
+
+\begin{code}
+compare : ∀ (A : Type) (Γ Δ : Env) → Var Δ A
+compare A Γ Δ    with (Γ , A) ≟ Δ
+compare A Γ Δ       | yes refl = Z
+compare A Γ (Δ , B) | no _     = S (compare A Γ Δ)
+compare A Γ ε       | no _     = impossible
+  where
+    postulate
+      impossible : ∀ {A : Set} → A
+
+PH→Exp : ∀ {A : Type} → (∀ {X} → PH X A) → Exp ε A
+PH→Exp M = h M ε
+  where
+  K : Type → Set
+  K A = Env
+
+  h : ∀ {A} → PH K A → (Δ : Env) → Exp Δ A
+  h {A} (var Γ) Δ = var (compare A Γ Δ)
+  h {A ⇒ B} (abs N) Δ = abs (h (N Δ) (Δ , A))
+  h (app L M) Δ = app (h L Δ) (h M Δ)
+
+ex₁ : PH→Exp twoPH ≡ twoExp
+ex₁ = refl
+\end{code}
+
+## When one environment extends another
+
+We could get rid of the use of `impossible` above if we could prove
+that `Extends (Γ , A) Δ` in the `(var Γ)` case of the definition of `h`.
+
+\begin{code}
+data Extends : (Γ : Env) → (Δ : Env) → Set where
+  Z : ∀ {Γ : Env} → Extends Γ Γ
+  S : ∀ {A : Type} {Γ Δ : Env} → Extends Γ Δ → Extends Γ (Δ , A)
+
+extract : ∀ {A : Type} {Γ Δ : Env} → Extends (Γ , A) Δ → Var Δ A
+extract Z     = Z
+extract (S k) = S (extract k)
+\end{code}
+
+
+

src/extra/Liftable.agda

@@ -0,0 +1,167 @@
+open import Function
+open import Relation.Nullary
+open import Relation.Binary hiding (_⇒_)
+open import Relation.Binary.PropositionalEquality hiding ([_])
+open import Data.Sum
+open import Data.Product
+
+delim : ∀ {α β} {A : Set α} {B : Dec A -> Set β}
+      -> (d : Dec A) -> (∀ x -> B (yes x)) -> (∀ c -> B (no c)) -> B d
+delim (yes x) f g = f x
+delim (no  c) f g = g c
+
+drec = λ {α β} {A : Set α} {B : Set β} -> delim {A = A} {B = λ _ -> B}
+
+dcong₂ : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ} {x y v w}
+       -> (f : A -> B -> C)
+       -> (∀ {x y} -> f x v ≡ f y w -> x ≡ y × v ≡ w)
+       -> Dec (x ≡ y)
+       -> Dec (v ≡ w)
+       -> Dec (f x v ≡ f y w)
+dcong₂ f inj d₁ d₂ = drec d₁
+    (λ p₁ -> drec d₂
+      (λ p₂ -> yes (cong₂ f p₁ p₂))
+      (λ c  -> no (c ∘ proj₂ ∘ inj)))
+    (λ c  -> no (c ∘ proj₁ ∘ inj))
+
+infixl 5 _▻_
+infixr 6 _⇒_
+infix  4 _≟ᵗ_ _≟ᶜ_ _∈_ _⊂[_]_ _⊂?_ _⊢_
+infixr 6 vs_
+infixr 5 ƛ_
+infixl 7 _·_
+
+data Type : Set where
+  ⋆   : Type
+  _⇒_ : Type -> Type -> Type
+
+data Con : Set where
+  ε   : Con
+  _▻_ : Con -> Type -> Con
+
+data _∈_ σ : Con -> Set where
+  vz  : ∀ {Γ}   -> σ ∈ Γ ▻ σ
+  vs_ : ∀ {Γ τ} -> σ ∈ Γ     -> σ ∈ Γ ▻ τ 
+
+data _⊢_ Γ : Type -> Set where
+  var : ∀ {σ}   -> σ ∈ Γ     -> Γ ⊢ σ
+  ƛ_  : ∀ {σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ ⇒ τ
+  _·_ : ∀ {σ τ} -> Γ ⊢ σ ⇒ τ -> Γ ⊢ σ     -> Γ ⊢ τ
+
+⇒-inj : ∀ {σ₁ σ₂ τ₁ τ₂} -> σ₁ ⇒ τ₁ ≡ σ₂ ⇒ τ₂ -> σ₁ ≡ σ₂ × τ₁ ≡ τ₂
+⇒-inj refl = refl , refl
+
+▻-inj : ∀ {Γ₁ Γ₂ σ₁ σ₂} -> Γ₁ ▻ σ₁ ≡ Γ₂ ▻ σ₂ -> Γ₁ ≡ Γ₂ × σ₁ ≡ σ₂
+▻-inj refl = refl , refl
+
+_≟ᵗ_ : Decidable (_≡_ {A = Type})
+⋆         ≟ᵗ ⋆         = yes refl
+(σ₁ ⇒ τ₁) ≟ᵗ (σ₂ ⇒ τ₂) = dcong₂ _⇒_ ⇒-inj (σ₁ ≟ᵗ σ₂) (τ₁ ≟ᵗ τ₂)
+⋆         ≟ᵗ (σ₂ ⇒ τ₂) = no λ()
+(σ₁ ⇒ τ₁) ≟ᵗ ⋆         = no λ()
+
+_≟ᶜ_ : Decidable (_≡_ {A = Con})
+ε     ≟ᶜ ε     = yes refl
+Γ ▻ σ ≟ᶜ Δ ▻ τ = dcong₂ _▻_ ▻-inj (Γ ≟ᶜ Δ) (σ ≟ᵗ τ)
+ε     ≟ᶜ Δ ▻ τ = no λ()
+Γ ▻ σ ≟ᶜ ε     = no λ()
+
+data _⊂[_]_ : Con -> Type -> Con -> Set where
+  stop : ∀ {Γ σ}     -> Γ ⊂[ σ ] Γ ▻ σ
+  skip : ∀ {Γ Δ σ τ} -> Γ ⊂[ σ ] Δ     -> Γ ⊂[ σ ] Δ ▻ τ
+
+sub : ∀ {Γ Δ σ} -> Γ ⊂[ σ ] Δ -> σ ∈ Δ
+sub  stop    = vz
+sub (skip p) = vs (sub p)
+
+⊂-inj : ∀ {Γ Δ σ τ} -> Γ ⊂[ σ ] Δ ▻ τ -> Γ ⊂[ σ ] Δ ⊎ Γ ≡ Δ × σ ≡ τ
+⊂-inj  stop    = inj₂ (refl , refl)
+⊂-inj (skip p) = inj₁ p
+
+_⊂?_ : ∀ {σ} -> Decidable _⊂[ σ ]_
+_⊂?_     Γ  ε      = no λ()
+_⊂?_ {σ} Γ (Δ ▻ τ) with λ c₁ -> drec (Γ ⊂? Δ) (yes ∘ skip) (λ c₂ -> no ([ c₂ , c₁ ] ∘ ⊂-inj))
+... | r with σ ≟ᵗ τ
+... | no  c₁ = r (c₁ ∘ proj₂)
+... | yes p₁ rewrite p₁ with Γ ≟ᶜ Δ
+... | no  c₁ = r (c₁ ∘ proj₁)
+... | yes p₂ rewrite p₂ = yes stop
+
+⊢_ : Type -> Set
+⊢ σ = ∀ {Γ} -> Γ ⊢ σ
+
+⟦_⟧ᵗ : Type -> Set
+⟦ ⋆     ⟧ᵗ = ⊢ ⋆
+⟦ σ ⇒ τ ⟧ᵗ = ⟦ σ ⟧ᵗ -> ⟦ τ ⟧ᵗ
+
+mutual
+  ↑ : ∀ {σ} -> ⊢ σ -> ⟦ σ ⟧ᵗ
+  ↑ {⋆}     t = t
+  ↑ {σ ⇒ τ} f = λ x -> ↑ (f · ↓ x)
+
+  ↓ : ∀ {σ} -> ⟦ σ ⟧ᵗ -> ⊢ σ
+  ↓ {⋆}     t = t
+  ↓ {σ ⇒ τ} f = λ {Γ} -> ƛ (↓ (f (varˢ Γ σ)))
+
+  varˢ : ∀ Γ σ -> ⟦ σ ⟧ᵗ
+  varˢ Γ σ = ↑ (λ {Δ} -> var (diff Δ Γ σ)) where
+    diff : ∀ Δ Γ σ -> σ ∈ Δ
+    diff Δ Γ σ = drec (Γ ⊂? Δ) sub ⊥ where postulate ⊥ : _
+
+data ⟦_⟧ᶜ : Con -> Set where
+  Ø   : ⟦ ε ⟧ᶜ
+  _▷_ : ∀ {Γ σ} -> ⟦ Γ ⟧ᶜ -> ⟦ σ ⟧ᵗ -> ⟦ Γ ▻ σ ⟧ᶜ
+
+lookupᵉ : ∀ {Γ σ} -> σ ∈ Γ -> ⟦ Γ ⟧ᶜ -> ⟦ σ ⟧ᵗ
+lookupᵉ  vz    (ρ ▷ x) = x
+lookupᵉ (vs v) (ρ ▷ x) = lookupᵉ v ρ
+
+idᵉ : ∀ {Γ} -> ⟦ Γ ⟧ᶜ
+idᵉ {ε}     = Ø
+idᵉ {Γ ▻ σ} = idᵉ ▷ varˢ Γ σ
+
+⟦_⟧ : ∀ {Γ σ} -> Γ ⊢ σ -> ⟦ Γ ⟧ᶜ -> ⟦ σ ⟧ᵗ
+⟦ var v ⟧ ρ = lookupᵉ v ρ
+⟦ ƛ b   ⟧ ρ = λ x -> ⟦ b ⟧ (ρ ▷ x)
+⟦ f · x ⟧ ρ = ⟦ f ⟧ ρ (⟦ x ⟧ ρ)
+
+eval : ∀ {Γ σ} -> Γ ⊢ σ -> ⟦ σ ⟧ᵗ
+eval t = ⟦ t ⟧ idᵉ
+
+norm : ∀ {Γ σ} -> Γ ⊢ σ -> Γ ⊢ σ
+norm t = ↓ (eval t)
+
+
+
+Term : Type -> Set
+Term σ = ε ⊢ σ
+
+I : Term (⋆ ⇒ ⋆)
+I = ↓ id
+
+K : Term (⋆ ⇒ ⋆ ⇒ ⋆)
+K = ↓ const
+
+S : Term ((⋆ ⇒ ⋆ ⇒ ⋆) ⇒ (⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆)
+S = ↓ _ˢ_
+
+B : Term ((⋆ ⇒ ⋆) ⇒ (⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆)
+B = ↓ _∘′_
+
+C : Term ((⋆ ⇒ ⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆ ⇒ ⋆)
+C = ↓ flip
+
+W : Term ((⋆ ⇒ ⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆)
+W = ↓ λ f x -> f x x
+
+P : Term ((⋆ ⇒ ⋆ ⇒ ⋆) ⇒ (⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆ ⇒ ⋆)
+P = ↓ _on_
+
+O : Term (((⋆ ⇒ ⋆) ⇒ ⋆) ⇒ (⋆ ⇒ ⋆) ⇒ ⋆)
+O = ↓ λ g f -> f (g f)
+
+test₁ : norm (ε ▻ ⋆ ⇒ ⋆ ▻ ⋆ ⊢ ⋆ ∋ (ƛ var (vs vs vz) · var vz) · var vz) ≡ var (vs vz) · var vz
+test₁ = refl
+
+test₂ : S ≡ ƛ ƛ ƛ var (vs vs vz) · var vz · (var (vs vz) · var vz)
+test₂ = refl

src/extra/Module.agda

@@ -0,0 +1,12 @@
+module Module where
+
+data ℕ : Set where
+  zero : ℕ
+  suc : ℕ → ℕ
+
+_+_ : ℕ → ℕ → ℕ
+zero + n = zero
+suc m + n = suc (m + n)
+
+import Data.Nat using (ℕ; zero; suc; _+_)
+

src/extra/PHOAStoEXP.agda

@@ -0,0 +1,112 @@
+open import Algebra
+open import Data.Product
+open import Data.Bool
+open import Data.List
+open import Data.List.Properties
+open import Relation.Binary.PropositionalEquality
+open import Function
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+
+module LM {A : Set} = Monoid (Data.List.Properties.++-monoid A)
+
+infixr 4 _⇒_
+
+data Type : Set where
+  o : Type
+  _⇒_ : Type → Type → Type
+
+Env = List Type
+
+Type≡? : (A B : Type) → Dec (A ≡ B)
+Type≡? o o = yes refl
+Type≡? o (B ⇒ B₁) = no (λ ())
+Type≡? (A ⇒ A₁) o = no (λ ())
+Type≡? (A ⇒ B) (A' ⇒ B') with Type≡? A A'
+Type≡? (A ⇒ B) (.A ⇒ B') | yes refl with Type≡? B B'
+Type≡? (A ⇒ B) (.A ⇒ .B) | yes refl | yes refl = yes refl
+Type≡? (A ⇒ B) (.A ⇒ B') | yes refl | no ¬p = no (λ {refl → ¬p refl})
+Type≡? (A ⇒ B) (A' ⇒ B') | no ¬p = no (λ {refl → ¬p refl})
+
+Env≡? : (Γ Δ : Env) → Dec (Γ ≡ Δ)
+Env≡? [] [] = yes refl
+Env≡? [] (x ∷ Δ) = no (λ ())
+Env≡? (x ∷ Γ) [] = no (λ ())
+Env≡? (A ∷ Γ) (A' ∷ Δ) with Type≡? A A'
+Env≡? (A ∷ Γ) (A' ∷ Δ) | yes p with Env≡? Γ Δ
+Env≡? (A ∷ Γ) (.A ∷ .Γ) | yes refl | yes refl = yes refl
+Env≡? (A ∷ Γ) (A' ∷ Δ) | yes p | no ¬q = no (λ {refl → ¬q refl})
+Env≡? (A ∷ Γ) (A' ∷ Δ) | no ¬p = no (λ {refl → ¬p refl})
+
+data Var : Env → Type → Set where
+  Z : ∀ {Γ : Env} {A : Type} → Var (A ∷ Γ) A
+  S : ∀ {Γ : Env} {A B : Type} → Var Γ B → Var (A ∷ Γ) B
+
+data Exp : Env → Type → Set where
+  var : ∀ {Γ : Env} {A : Type} → Var Γ A → Exp Γ A
+  abs : ∀ {Γ : Env} {A B : Type} → Exp (A ∷ Γ) B → Exp Γ (A ⇒ B)
+  app : ∀ {Γ : Env} {A B : Type} → Exp Γ (A ⇒ B) → Exp Γ A → Exp Γ B
+
+data PH (X : Type → Set) : Type → Set where
+  var : ∀ {A : Type} → X A → PH X A
+  abs : ∀ {A B : Type} → (X A → PH X B) → PH X (A ⇒ B)
+  app : ∀ {A B : Type} → PH X (A ⇒ B) → PH X A → PH X B
+
+-- logical prediacte on PH
+PHᴾ : ∀ {X}(Xᴾ : ∀ {A} → X A → Set) → ∀ {A} → PH X A → Set
+PHᴾ Xᴾ (var a)   = Xᴾ a
+PHᴾ Xᴾ (abs t)   = ∀ a → Xᴾ a → PHᴾ Xᴾ (t a)
+PHᴾ Xᴾ (app t u) = PHᴾ Xᴾ t × PHᴾ Xᴾ u
+
+postulate
+  free-thm :
+    ∀ {A}(t : ∀ {X} → PH X A) → ∀ X (Xᴾ : ∀ {A} → X A → Set) → PHᴾ {X} Xᴾ t
+
+PH' : Type → Set
+PH' = PH (λ _ → Env)
+
+VarOK? : ∀ Γ A Δ → Dec (∃ λ Ξ → (Ξ ++ A ∷ Δ) ≡ Γ)
+VarOK? []       A Δ = no (λ {([] , ()) ; (_ ∷ _ , ())})
+VarOK? (A' ∷ Γ) A Δ with Env≡? (A' ∷ Γ) (A ∷ Δ)
+VarOK? (A' ∷ Γ) .A' .Γ | yes refl = yes ([] , refl)
+VarOK? (A' ∷ Γ) A Δ | no ¬p with VarOK? Γ A Δ
+VarOK? (A' ∷ Γ) A Δ | no ¬p | yes (Σ , refl) =
+  yes (A' ∷ Σ , refl)
+VarOK? (A' ∷ Γ) A Δ | no ¬p | no ¬q
+  = no λ { ([] , refl) → ¬p refl ; (x ∷ Σ , s) → ¬q (Σ , proj₂ (∷-injective s))}
+
+OK : ∀ {A} → Env → PH' A → Set
+OK {A} Γ t = ∀ Δ → PHᴾ (λ {B} Σ → True (VarOK? (Δ ++ Γ) B Σ)) t
+
+toVar : ∀ {Γ Σ A} → (∃ λ Ξ → (Ξ ++ A ∷ Σ) ≡ Γ) → Var Γ A
+toVar ([]    , refl) = Z
+toVar (x ∷ Ξ , refl) = S (toVar (Ξ , refl))
+
+toExp' : ∀ {Γ A} (t : PH' A) → OK {A} Γ t → Exp Γ A
+toExp' (var x) p = var (toVar (toWitness (p [])))
+toExp' {Γ} (abs {A} {B} t) p =
+  abs (toExp' (t Γ)
+      λ Δ → subst (λ z → PHᴾ (λ {B₁} Σ₁ → True (VarOK? z B₁ Σ₁)) (t Γ))
+                   (LM.assoc Δ (A ∷ []) Γ)
+                   (p (Δ ++ A ∷ []) Γ (fromWitness (Δ , sym (LM.assoc Δ (A ∷ []) Γ)))))
+toExp' (app t u) p =
+  app (toExp' t (proj₁ ∘ p)) (toExp' u (proj₂ ∘ p))
+
+toExp : ∀ {A} → (∀ {X} → PH X A) → Exp [] A
+toExp {A} t = toExp' t λ Δ → free-thm t _ _
+
+-- examples
+------------------------------------------------------------
+
+t0 : ∀ {X} → PH X ((o ⇒ o) ⇒ o ⇒ o)
+t0 = abs var
+
+t1 : ∀ {X} → PH X ((o ⇒ o) ⇒ o ⇒ o)
+t1 = abs λ f → abs λ x → app (var f) (app (var f) (var x))
+
+test1 : toExp t0 ≡ abs (var Z)
+test1 = refl
+
+test2 : toExp t1 ≡ abs (abs (app (var (S Z)) (app (var (S Z)) (var Z))))
+test2 = refl