Merge branch 'dev'

1 files changed, 76 insertions, 0 deletions

diff --git a/spartan/core/elaboration.ML b/spartan/core/elaboration.ML
new file mode 100644
index 0000000..27b6bb0
--- /dev/null
+++ b/spartan/core/elaboration.ML
@@ -0,0 +1,76 @@
+(*  Title:      elaboration.ML
+    Author:     Joshua Chen
+
+Basic elaboration.
+*)
+
+structure Elab: sig
+
+val elab: Proof.context -> cterm list -> term -> Envir.env
+val elab_stmt: Proof.context -> cterm list -> term -> Envir.env * term
+
+end = struct
+
+(*Elaborate `tm` by solving the inference problem `tm: {}`, knowing `assums`,
+  which are fully elaborated, in `ctxt`. Return a substitution.*)
+fun elab ctxt assums tm =
+  if Lib.no_vars tm
+  then Envir.init
+  else
+    let
+      val inf = Goal.init (Thm.cterm_of ctxt (Lib.typing_of_term tm))
+      val res = Types.check_infer (map Thm.assume assums) 1 (ctxt, inf)
+      val tm' =
+        Thm.prop_of (#2 (Seq.hd (Seq.filter_results res)))
+        |> Lib.dest_prop |> Lib.term_of_typing
+        handle TERM ("dest_typing", [t]) =>
+          let val typ = Logic.unprotect (Logic.strip_assums_concl t)
+            |> Lib.term_of_typing
+          in
+            error ("Elaboration of " ^ Syntax.string_of_term ctxt typ ^ " failed")
+          end
+    in
+      Seq.hd (Unify.matchers (Context.Proof ctxt) [(tm, tm')])
+    end
+    handle Option => error
+      ("Elaboration of " ^ Syntax.string_of_term ctxt tm ^ " failed")
+
+(*Recursively elaborate a statement \<And>x ... y. \<lbrakk>...\<rbrakk> \<Longrightarrow> P x ... y by elaborating
+  only the types of typing judgments (in particular, does not look at judgmental
+  equality statements). Could also elaborate the terms of typing judgments, but
+  for now we assume that these are always free variables in all the cases we're
+  interested in.*)
+fun elab_stmt ctxt assums stmt =
+  let
+    val stmt = Lib.dest_prop stmt
+    fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env)
+  in
+    if Lib.no_vars stmt orelse Lib.is_eq stmt then
+      (Envir.init, stmt)
+    else if Lib.is_typing stmt then
+      let
+        val typ = Lib.type_of_typing stmt
+        val subst = elab ctxt assums typ
+      in (subst, subst_term subst stmt) end
+    else
+      let
+        fun elab' assums (x :: xs) =
+              let
+                val (env, x') = elab_stmt ctxt assums x
+                val assums' =
+                  if Lib.no_vars x' then Thm.cterm_of ctxt x' :: assums else assums
+              in env :: elab' assums' xs end
+          | elab' _ [] = []
+        val (prems, concl) = Lib.decompose_goal ctxt stmt
+        val subst = fold (curry Envir.merge) (elab' assums prems) Envir.init
+        val prems' = map (Thm.cterm_of ctxt o subst_term subst) prems
+        val subst' =
+          if Lib.is_typing concl then
+            let val typ = Lib.type_of_typing concl
+            in Envir.merge (subst, elab ctxt (assums @ prems') typ) end
+          else subst
+      in (subst', subst_term subst' stmt) end
+  end
+
+
+end