Add interpreted types to proof

pikelet-lang · Oct 11, 2017 · ba1b685 · ba1b685
1 parent 739c26e
commit ba1b685
Show file tree

Hide file tree

Showing 6 changed files with 35 additions and 9 deletions.
diff --git a/experiments/lean/src/ddl/binary/basic.lean b/experiments/lean/src/ddl/binary/basic.lean
@@ -24,13 +24,13 @@ namespace ddl.binary
     | struct_cons : ℓ → type → type → type
     | array : type → host.expr ℓ → type
     | cond : type → host.expr ℓ → type
+    | interp : type → host.expr ℓ → host.type ℓ → type
     | abs : kind → type → type
     | app : type → type → type
 
 
-  -- Abstraction and conditional type notation - note that we are a
-  -- using nameless for identifiers encoding so we don't include the argument
-  -- identifiers
+  -- Abstraction and conditional type notation - note that we are using a
+  -- nameless representation so we don't include the argument identifiers
   notation `Λ0: ` k `, ` t := type.abs k t
   notation `{0: ` t ` | ` e ` }` := type.cond t e
   -- Array type syntax

diff --git a/experiments/lean/src/ddl/binary/formation.lean b/experiments/lean/src/ddl/binary/formation.lean
@@ -40,6 +40,9 @@ namespace ddl.binary
       | cond {t e} :
           well_formed t →
           well_formed (cond t e)
+      | interp {t e th} :
+          well_formed t →
+          well_formed (interp t e th)
       | abs {t k} :
           well_formed t →
           well_formed (abs k t)

diff --git a/experiments/lean/src/ddl/binary/kinding.lean b/experiments/lean/src/ddl/binary/kinding.lean
@@ -35,8 +35,12 @@ namespace ddl.binary
           has_kind Γ [ t; e ] ★
       | cond {Γ t e} :
           has_kind Γ t ★ →
-          host.has_type e host.type.bool →
+          host.has_type /- FIXME: add binding? -/ e host.type.bool →
           has_kind Γ {0: t | e } ★
+      | interp {Γ t e th} :
+          has_kind Γ t ★ →
+          host.has_type /- FIXME: add binding? -/ e th →
+          has_kind Γ (type.interp t e th) ★
       | abs {Γ t k₁ k₂} :
           has_kind (binder.abs k₁ :: Γ) t k₁ →
           has_kind Γ (Λ0: k₁, t) (k₁ ⇒ k₂)

diff --git a/experiments/lean/src/ddl/binary/monad.lean b/experiments/lean/src/ddl/binary/monad.lean
@@ -17,6 +17,7 @@ namespace ddl.binary.type
     | (struct_cons l t₁ t₂) f := struct_cons l (bind t₁ f) (bind t₂ f)
     | (array t e)           f := array (bind t f) e
     | (cond t e)            f := cond (bind t f) e
+    | (interp t e th)       f := interp (bind t f) e th
     | (abs k t)             f := abs k (bind t f)
     | (app t₁ t₂)           f := app (bind t₁ f) (bind t₂ f)
 
@@ -48,6 +49,10 @@ namespace ddl.binary.type
             simp [bind, function.comp],
             rw [ht],
           },
+          case interp t e ht hht {
+            simp [bind, function.comp],
+            rw [hht],
+          },
           case abs k t ht {
             simp [bind, function.comp],
             rw [ht],
@@ -85,6 +90,11 @@ namespace ddl.binary.type
             simp [bind] at ht,
             rw [ht]
           },
+          case interp t e ht hht {
+            simp [bind],
+            simp [bind] at hht,
+            rw [hht]
+          },
           case abs k t ht {
             simp [bind],
             simp [bind] at ht,

diff --git a/experiments/lean/src/ddl/binary/repr.lean b/experiments/lean/src/ddl/binary/repr.lean
@@ -14,12 +14,13 @@ namespace ddl.binary
 
 
     def repr : type ℓ α → host.type ℓ
-      | (sum t₁ t₂) := t₁.repr + t₂.repr
-      | (struct_nil) := host.type.struct_nil
+      | (sum t₁ t₂)           := t₁.repr + t₂.repr
+      | (struct_nil)          := host.type.struct_nil
       | (struct_cons l t₁ t₂) := host.type.struct_cons l t₁.repr t₂.repr
-      | (array t e) := host.type.array (t.repr)
-      | (cond t e) := t.repr
-      | _ := sorry
+      | (array t e)           := host.type.array (t.repr)
+      | (cond t e)            := t.repr
+      | (interp t e ht)       := ht
+      | _                     := sorry
 
 
     lemma repr_well_formed [decidable_eq ℓ] :
@@ -45,6 +46,10 @@ namespace ddl.binary
           case well_formed.cond t₁ e hbtwf₁ hhtwf₁ {
             exact hhtwf₁,
           },
+          case well_formed.interp t₁ e ht hbtwf₁ hhtwf₁ {
+            simp [repr],
+            admit,
+          },
           case well_formed.abs t₁ k hbtwf₁ { admit },
           case well_formed.app t₁ t₂ hbtwf₁ hbtwf₂ { admit },
       end

diff --git a/experiments/lean/src/ddl/binary/subst.lean b/experiments/lean/src/ddl/binary/subst.lean
@@ -19,6 +19,7 @@ namespace ddl.binary
       | i x (struct_cons l t₁ t₂) := struct_cons l (open_var i x t₁) (open_var i x t₂)
       | i x (array t e) := array (open_var i x t) e
       | i x (cond t e) := cond (open_var i x t) e
+      | i x (interp t e th) := interp (open_var i x t) e th
       | i x (abs k t) := abs k (open_var (i + 1) x t)
       | i x (app t₁ t₂) := app (open_var i x t₁) (open_var i x t₂)
 
@@ -32,6 +33,7 @@ namespace ddl.binary
       | i x (struct_cons l t₁ t₂) := struct_cons l (close_var i x t₁) (close_var i x t₂)
       | i x (array t e) := array (close_var i x t) e
       | i x (cond t e) := cond (close_var i x t) e
+      | i x (interp t e th) := interp (close_var i x t) e th
       | i x (abs k t) := abs k (close_var (i + 1) x t)
       | i x (app t₁ t₂) := app (close_var i x t₁) (close_var i x t₂)
 
@@ -50,6 +52,7 @@ namespace ddl.binary
         case struct_cons l t₁ t₂ ht₁ ht₂ { admit },
         case array t e ht { admit },
         case cond t e ht { admit },
+        case interp t e ht hht { admit },
         case abs k t ht { admit },
         case app t₁ t₂ ht₁ ht₂ { admit },
     end
@@ -69,6 +72,7 @@ namespace ddl.binary
         case struct_cons l t₁ t₂ ht₁ ht₂ { admit },
         case array t e ht { admit },
         case cond t e ht { admit },
+        case interp t e ht hht { admit },
         case abs k t ht { admit },
         case app t₁ t₂ ht₁ ht₂ { admit },
     end