diff --git a/src/extra/Addition.agda b/src/extra/Addition.agda new file mode 100644 index 00000000..28a1b3a3 --- /dev/null +++ b/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 : ℕ +-} diff --git a/src/extra/CPP.lagda b/src/extra/CPP.lagda new file mode 100644 index 00000000..4942a94f --- /dev/null +++ b/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} +% +\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} +% +\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} +% +\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} +% +\begin{code} + where + + _-,_ : ∀ {Γ σ Δ} → (∀ {τ} → Var τ Γ → Val τ Δ) → Val σ Δ → ∀ {τ} → Var τ (σ ∷ Γ) → Val τ Δ + (ρ -, v) ze = v + (ρ -, v) (su k) = ρ k +\end{code} + + diff --git a/src/extra/DaraisPhoas.agda b/src/extra/DaraisPhoas.agda new file mode 100644 index 00000000..b513d70d --- /dev/null +++ b/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 +-} diff --git a/src/extra/DeBruijn-agda-list-3.lagda b/src/extra/DeBruijn-agda-list-3.lagda new file mode 100644 index 00000000..351ea516 --- /dev/null +++ b/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} + + + diff --git a/src/extra/Liftable.agda b/src/extra/Liftable.agda new file mode 100644 index 00000000..8de6b1c8 --- /dev/null +++ b/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 diff --git a/src/extra/Module.agda b/src/extra/Module.agda new file mode 100644 index 00000000..e8c6d7bf --- /dev/null +++ b/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; _+_) + diff --git a/src/extra/PHOAStoEXP.agda b/src/extra/PHOAStoEXP.agda new file mode 100644 index 00000000..51ed1a3a --- /dev/null +++ b/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