agda experiment

.gitignore

@@ -218,3 +218,4 @@ TSWLatexianTemp*
 
 # expex forward references with \gathertags
 *-tags.tex
+*.agdai

unary-cbv.agda

+module unary-cbv(Σ₀ : Set) where
+open import Relation.Binary.PropositionalEquality
+
+data Type : Set where
+  base : Σ₀ -> Type
+  □    : Type -> Type
+
+Sig₁ : Set₁
+Sig₁ = Type -> Type -> Set
+
+module ucbv1 (Σv : Sig₁) (Σt : Sig₁) where
+  data _⇒v_ : Type -> Type -> Set
+  data _⇒t_ : Type -> Type -> Set
+  data _⇒v_ where
+    base : ∀ {A B C} -> Σv B C -> A ⇒v B -> A ⇒v C
+    var  : ∀ {A} -> A ⇒v A
+    -- thunk
+    □-I  : ∀ {A B} -> A ⇒t B -> A ⇒v □ B
+  data _⇒t_ where
+    base : ∀ {A B C D} -> Σt B C -> A ⇒v B -> C ⇒t D -> A ⇒t D
+    ret  : ∀ {A B} -> A ⇒v B -> A ⇒t B
+
+  tvar : ∀ {A} -> A ⇒t A
+  tvar = ret var
+
+  _⟨_⟩v : ∀ {A B C} -> B ⇒v C -> A ⇒v B -> A ⇒v C
+  _⟨_⟩t : ∀ {A B C} -> B ⇒t C -> A ⇒v B -> A ⇒t C
+  _to_  : ∀ {A B C} -> A ⇒t B -> B ⇒t C -> A ⇒t C
+  base f v ⟨ u ⟩v = base f (v ⟨ u ⟩v)
+  var ⟨ u ⟩v = u
+  □-I t ⟨ u ⟩v = □-I (t ⟨ u ⟩t)
+  base p u t ⟨ v ⟩t = base p (u ⟨ v ⟩v) t
+  ret u ⟨ v ⟩t = ret (u ⟨ v ⟩v) 
+  base p v s to t = base p v (s to t)
+  ret v to t = t ⟨ v ⟩t
+
+  subst-v-id-inp : ∀ {A B} (v : A ⇒v B) -> v ⟨ var ⟩v ≡ v
+  subst-t-id-inp : ∀ {A B} (t : A ⇒t B) -> t ⟨ var ⟩t ≡ t
+  subst-v-id-inp (base x v) = cong (base x) (subst-v-id-inp v)
+  subst-v-id-inp var = refl
+  subst-v-id-inp (□-I t) = cong □-I (subst-t-id-inp t)
+
+  subst-t-id-inp (base p v t) = cong (\v -> base p v t) (subst-v-id-inp v)
+  subst-t-id-inp (ret v) = cong ret (subst-v-id-inp v)
+
+  subst-to-id-inp : ∀ {A B} (t : A ⇒t B) -> ret var to t ≡ t
+  subst-to-id-inp t = subst-t-id-inp t
+
+  subst-v-id-outp : ∀ {A B} (v : A ⇒v B) -> var ⟨ v ⟩v ≡ v
+  subst-to-id-outp : ∀ {A B} (t : A ⇒t B) -> t to ret var ≡ t
+  subst-v-id-outp v = refl
+  subst-to-id-outp (base p v t) = cong (\t -> base p v t) (subst-to-id-outp t)
+  subst-to-id-outp (ret v) = refl
+
+  subst-v-assoc : ∀ {A0 A1 A2 A3} (v2 : A2 ⇒v A3)(v1 : A1 ⇒v A2)(v0 : A0 ⇒v A1) -> v2 ⟨ v1 ⟨ v0 ⟩v ⟩v ≡ (v2 ⟨ v1 ⟩v) ⟨ v0 ⟩v
+  subst-tvv-assoc : ∀ {A0 A1 A2 A3} (t2 : A2 ⇒t A3)(v1 : A1 ⇒v A2)(v0 : A0 ⇒v A1) -> t2 ⟨ v1 ⟨ v0 ⟩v ⟩t ≡ (t2 ⟨ v1 ⟩t) ⟨ v0 ⟩t
+  subst-v-assoc (base f v2) v1 v0 = cong (λ v → base f v) (subst-v-assoc v2 v1 v0)
+  subst-v-assoc var v1 v0 = refl
+  subst-v-assoc (□-I t2) v1 v0 = cong □-I (subst-tvv-assoc t2 v1 v0)
+
+  subst-tvv-assoc (base p v2 t2) v1 v0 = cong (λ v → base p v t2) (subst-v-assoc v2 v1 v0)
+  subst-tvv-assoc (ret v2) v1 v0 = cong ret (subst-v-assoc v2 v1 v0)
+
+  subst-ttv-assoc : ∀ {A0 A1 A2 A3} (t2 : A2 ⇒t A3)(t1 : A1 ⇒t A2)(v0 : A0 ⇒v A1) -> (t1 ⟨ v0 ⟩t) to t2 ≡ (t1 to t2) ⟨ v0 ⟩t
+  subst-ttv-assoc t2 (base x x₁ t1) v0 = refl
+  subst-ttv-assoc t2 (ret v1) v0 = subst-tvv-assoc t2 v1 v0
+
+  subst-to-assoc : ∀ {A0 A1 A2 A3} (t2 : A2 ⇒t A3)(t1 : A1 ⇒t A2)(t0 : A0 ⇒t A1) -> (t0 to t1) to t2 ≡ t0 to (t1 to t2)
+  subst-to-assoc t2 t1 (base p v t0) = cong (λ t → base p v t) (subst-to-assoc t2 t1 t0)
+  subst-to-assoc t2 t1 (ret v0) = subst-ttv-assoc t2 t1 v0