Type inference setup begun - first use-case for function composition.

3 files changed, 118 insertions, 61 deletions

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index a5280ce..aa13815 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -3,11 +3,11 @@ Isabelle/HoTT: Foundational definitions and notation
 Jan 2019
 
 This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions.
-Among other things, it defines:
+Among other things, it:
 
-* Containers for storing type information of object-level terms.
-* The universe hierarchy and its governing rules.
-* Named theorems for later use by proof methods.
+* Sets up object-level type inference functionality (via typing.ML).
+* Defines the universe hierarchy and its governing rules.
+* Defines named theorems for later use by proof methods.
 
 ********)
 
@@ -20,48 +20,9 @@ section \<open>Terms and typing\<close>
 
 typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
 
-consts has_type :: "[t, t] \<Rightarrow> prop"  \<comment> \<open>The judgment coercion\<close>
+judgment has_type :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
 
-text \<open>
-We create a dedicated container in which to store object-level typing information whenever a typing judgment that does not depend on assumptions is proved.
-\<close>
-
-ML \<open>
-signature TYPINGS =
-sig
-  val get: term -> term
-end
-
-structure Typings: TYPINGS = 
-struct
-
-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
-)
-
-fun get tm =
-  case Symtab.lookup (Typing_Data.get @{theory}) (Syntax.string_of_term @{context} tm) of
-    SOME tm' => tm'
-  | NONE => raise Fail "No typing information available"
-
-end
-\<close>
-
-syntax "_has_type" :: "[t, t] \<Rightarrow> prop"  ("3(_:/ _)")
-
-parse_translation \<open>
-
-\<close>
+ML_file "typing.ML"
 
 section \<open>Universes\<close>
 
@@ -85,13 +46,13 @@ declare
 axiomatization
   U :: "ord \<Rightarrow> t"
 where
-  U_hierarchy: "i < j \<Longrightarrow> U i: U j" and                               
+  U_hierarchy: "i < j \<Longrightarrow> U i: U j" and
   U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j" and
   U_cumulative': "\<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j"
 
 text \<open>
-Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will very easily lead to non-termination.
-Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
+Using method @{method rule} with @{thm U_cumulative} and @{thm U_cumulative'} is unsafe: if applied blindly it will very easily lead to non-termination.
+Instead use @{method elim}, or instantiate the rules suitably.
 
 @{thm U_cumulative'} is an alternative rule used by the method @{theory_text cumulativity} in @{file HoTT_Methods.thy}.
 \<close>
diff --git a/Prod.thy b/Prod.thy
index 68c9405..4c572ce 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -79,32 +79,37 @@ syntax "_compose" :: "[t, t] \<Rightarrow> t"  (infixr "o" 110)
 parse_translation \<open>
 let fun compose_tr ctxt tms =
   let
-    val f::g::_ = tms;
-    fun domain f = @{term "A :: t"}
+    val g :: f :: _ = tms |> map (Typing.tm_of_ptm ctxt)
+    val dom =
+      case Typing.get_typing f (Typing.typing_assms ctxt) of
+        SOME (Const ("Prod.Prod", _) $ T $ _) => T
+      | SOME _ => Exn.error "Can't compose with a non-function"
+      | NONE => Exn.error "Cannot infer domain of composition—please state this explicitly"
   in
-    @{const compose} $ (domain f) $ f $ g
+    @{const compose} $ dom $ g $ f
   end
 in
   [("_compose", compose_tr)]
 end
 \<close>
 
-ML_val \<open>
-Proof_Context.get_thms @{context} "compose_def"
-\<close>
-
 lemma compose_assoc:
-  assumes "A: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: TT x: C. D x"
+  assumes "A: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: TT x: C. D x" "(,\\(x: A). b x): TT x: A. D x"
   shows "(h o g) o f \<equiv> h o (g o f)"
-ML_prf \<open>
-@{thms assms};
-\<close>
 (* (derive lems: assms Prod_intro_eq) *)
+sorry
 
 lemma compose_comp:
   assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x"
-  shows "(\<^bold>\<lambda>x. c x) \<circ> (\<^bold>\<lambda>x. b x) \<equiv> \<^bold>\<lambda>x. c (b x)"
-by (derive lems: assms Prod_intro_eq)
+  shows "(,\\x: B. c x) o (,\\x: A. b x) \<equiv> ,\\x: A. c (b x)"
+ML_prf \<open>
+Assumption.all_assms_of @{context};
+nth (Assumption.all_assms_of @{context}) 1 |> Thm.term_of;
+Assumption.all_prems_of @{context};
+nth (Assumption.all_prems_of @{context}) 0 |> Thm.prop_of;
+typing_assms @{context}
+\<close>
+(*by (derive lems: assms Prod_intro_eq)*)
 
 abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> ,\\x: A. x"
 
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