1 files changed, 91 insertions, 0 deletions
diff --git a/typing.ML b/typing.ML
new file mode 100644
index 0000000..bfe8409
--- /dev/null
+++ b/typing.ML
@@ -0,0 +1,91 @@
+(********
+Isabelle/HoTT: typing.ML
+Feb 2019
+
+Functionality for object-level type inference.
+
+********)
+
+signature TYPING =
+sig
+  type jmt = term
+  val term_of_jmt: jmt -> term
+  val type_of_jmt: jmt -> term
+  val typing_assms: Proof.context -> jmt list
+  val get_typing: term -> jmt list -> term option
+  val get_global_typing: theory -> Proof.context -> term -> term option
+  val tm_of_ptm: Proof.context -> term -> term
+end
+
+structure Typing: TYPING =
+struct
+
+type jmt = term
+
+(* Functions to extract a and A from propositions "a: A" *)
+fun term_of_jmt (@{const has_type} $ t $ _) = t
+  | term_of_jmt _ = Exn.error "Not a typing judgment"
+
+fun type_of_jmt (@{const has_type} $ _ $ T) = T
+  | type_of_jmt _ = Exn.error "Not a typing judgment"
+
+(* Get the typing assumptions in the current context *)
+fun typing_assms ctxt =
+  let
+    fun is_typing_jmt (@{const has_type} $ _ $ _) = true
+      | is_typing_jmt _ = false
+  in
+    Assumption.all_prems_of ctxt |> map Thm.prop_of |> filter is_typing_jmt
+  end
+
+(* Search for a term typing in a list of judgments*)
+fun get_typing tm jmts =
+  let val find_type =
+        fn jmt => if Term.aconv_untyped (tm, term_of_jmt jmt) then SOME (type_of_jmt jmt) else NONE
+  in get_first find_type jmts end
+
+(* Private storage space for global typing data *)
+structure Typing_Data = Theory_Data
+(
+  type T = term Symtab.table
+  val empty = Symtab.empty
+  val extend = I
+
+  fun merge (tbl, tbl') =
+    let
+      val key_vals = map (Symtab.lookup_key tbl') (Symtab.keys tbl')
+      val updates = map (fn SOME kv => Symtab.update kv) key_vals
+      fun f u t = u t
+    in fold f updates tbl end
+)
+
+(* Accessor for the above data *)
+fun get_global_typing thy ctxt tm = Symtab.lookup (Typing_Data.get thy) (Syntax.string_of_term ctxt tm)
+
+(* Convert a Pure pre-term to an unchecked Pure term *)
+fun tm_of_ptm ctxt ptm =
+  let val ptm = Term_Position.strip_positions ptm
+  in
+  (case ptm of
+    Const ("_constrain", _) $ Free (t, _) $ (Const ("\<^type>fun", _) $ Const(n1, _) $ Const (n2, _)) =>
+      let
+        val typ1 = unprefix "\<^type>" n1
+        val typ2 = unprefix "\<^type>" n2
+        val typ = typ1 ^ "\<Rightarrow>" ^ typ2 |> Syntax.read_typ ctxt
+      in Free (t, typ) end
+  | Const ("_constrain", _) $ Free (t, _) $ Const (T, _) =>
+      Free (t, Syntax.read_typ ctxt (unprefix "\<^type>" T))
+  | ptm1 $ ptm2 =>
+      (tm_of_ptm ctxt ptm1) $ (tm_of_ptm ctxt ptm2)
+  | Const (t, T) =>
+      let val t' =
+        unprefix "\<^const>" t handle Fail "unprefix" =>
+        unprefix "\<^type>" t handle Fail "unprefix" =>
+        t
+      in Const (t', T) end
+  | Abs (t, T, ptm') =>
+      Abs (t, T, tm_of_ptm ctxt ptm')
+  | t => t)
+  end
+
+end