Put typing functionality into a .thy and clean up antiquotations, which results in some reorganization of the theory import structure.

4 files changed, 125 insertions, 109 deletions

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 1eaed12..9dcf6d0 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,64 +1,21 @@
 (********
-Isabelle/HoTT: Foundational definitions and notation
+Isabelle/HoTT: Basic logical definitions and notation
 Feb 2019
 
-This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions.
+This file completes the basic logical and functional setup of the HoTT logic.
 Among other things, it:
 
-* Calls the setup of object-level type inference functionality.
 * Defines the universe hierarchy and its governing rules.
 * Defines named theorems for later use by proof methods.
 
 ********)
 
 theory HoTT_Base
-imports Pure
-keywords "assume_type" "assume_types" :: thy_decl
+imports HoTT_Typing
 
 begin
 
-section \<open>Terms and typing\<close>
-
-typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
-
-judgment has_type :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
-
-section \<open>Setup non-core logic functionality\<close>
-
-declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close>
-
-ML \<open>val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\<close>
-  \<comment> \<open>Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\<close>
-
-text \<open>Set up type assumption and inference functionality:\<close>
-
-ML_file "util.ML"
-ML_file "typing.ML"
-ML \<open>
-val _ =
-  let
-    fun store_typing ctxt = Typing.put_declared_typing o (Syntax.read_prop ctxt)
-  in
-    Outer_Syntax.local_theory
-      @{command_keyword "assume_type"}
-      "Declare typing assumptions"
-      (Parse.prop >>
-        (fn prop => fn lthy => Local_Theory.background_theory (store_typing lthy prop) lthy))
-  end
-
-val _ =
-  let
-    val parser = Parse.and_list (Parse.prop)
-    fun store_typings ctxt = fold (Typing.put_declared_typing o (Syntax.read_prop ctxt))
-  in
-    Outer_Syntax.local_theory
-      @{command_keyword "assume_types"}
-      "Declare typing assumptions"
-      (parser >>
-        (fn props => fn lthy => Local_Theory.background_theory (store_typings lthy props) lthy))
-  end
-\<close>
-                                                                                  
+
 section \<open>Universes\<close>
 
 typedecl ord \<comment> \<open>Type of meta-numerals\<close>
@@ -92,6 +49,7 @@ 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>
 
+
 section \<open>Type families\<close>
 
 abbreviation (input) constraint :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop"  ("(1_:/ _ \<leadsto> _)")
@@ -99,6 +57,7 @@ where "f: A \<leadsto> B \<equiv> (\<And>x. x: A \<Longrightarrow> f x: B)"
 
 text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type families.\<close>
 
+
 section \<open>Named theorems\<close>
 
 named_theorems form
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 99f3446..088c1fa 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -9,6 +9,7 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
 
 begin
 
+
 section \<open>Substitution and simplification\<close>
 
 ML_file "~~/src/Tools/misc_legacy.ML"
@@ -25,6 +26,7 @@ Premises of the rule(s) applied are added as new subgoals.
 
 method compute declares comp = (subst comp)
 
+
 section \<open>Handling universes\<close>
 
 text \<open>
@@ -46,6 +48,7 @@ method cumulativity declares form = (
   ((elim U_cumulative | (rule U_cumulative, rule form)), provelt)
 )
 
+
 section \<open>Deriving typing judgments\<close>
 
 method routine uses add = (assumption | rule add | rule)+
@@ -54,6 +57,7 @@ text \<open>
 The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}.
 \<close>
 
+
 section \<open>Derivation search\<close>
 
 text \<open>
@@ -63,6 +67,7 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}.
 
 method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
 
+
 section \<open>Induction\<close>
 
 text \<open>
diff --git a/typing.ML b/HoTT_Typing.thy
index 8c3d42c..6433139 100644
--- a/typing.ML
+++ b/HoTT_Typing.thy
@@ -1,11 +1,40 @@
 (********
-Isabelle/HoTT: typing.ML
+Isabelle/HoTT: Core typing judgment form and associated automation
 Feb 2019
 
-Functionality for object-level type inference.
+This file is the starting point of the definition of Isabelle/HoTT.
+It declares the fundamental typing judgment form and sets up various
+ML functionality to automate type inference.
 
 ********)
 
+theory HoTT_Typing
+imports Pure
+keywords "assume_type" "assume_types" :: thy_decl
+
+begin
+
+
+section \<open>Initial settings\<close>
+
+declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close>
+
+ML \<open>val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\<close>
+  \<comment> \<open>Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\<close>
+
+
+section \<open>Terms and typing\<close>
+
+typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
+
+judgment has_type :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
+
+
+section \<open>Typing functionality\<close>
+
+ML_file "util.ML"
+
+ML \<open>
 signature TYPING =
 sig
   type jmt = term
@@ -18,10 +47,11 @@ sig
   val typing_all: Proof.context -> jmt list
 
   val get_typing_in: term -> jmt list -> term option
+
   val get_local_typing: Proof.context -> term -> term option
 
-  val get_declared_typing: theory -> term -> term option
-  val put_declared_typing: term -> theory -> theory
+  val put_theory_typing: term -> theory -> theory
+  val get_theory_typing: theory -> term -> term option
 
   val get_typing: Proof.context -> term -> term option
 end
@@ -32,23 +62,23 @@ struct
 type jmt = term
 
 (* Determine if a term is a typing judgment *)
-fun is_typing_jmt (@{const HoTT_Base.has_type} $ _ $ _) = true
+fun is_typing_jmt (@{const has_type} $ _ $ _) = true
   | is_typing_jmt _ = false
 
 (* Functions to extract a and A from propositions "a: A" *)
-fun term_of_jmt (@{const HoTT_Base.has_type} $ t $ _) = t
+fun term_of_jmt (@{const has_type} $ t $ _) = t
   | term_of_jmt _ = Exn.error "Not a typing judgment"
 
-fun type_of_jmt (@{const HoTT_Base.has_type} $ _ $ T) = T
+fun type_of_jmt (@{const has_type} $ _ $ T) = T
   | type_of_jmt _ = Exn.error "Not a typing judgment"
 
 (* Get typing assumptions in "this" *)
 fun typing_this ctxt = Util.get_this ctxt |> map Thm.prop_of |> filter is_typing_jmt
 
-(* Get the typing assumptions in the current context *)
+(* Get the typing assumptions in the current proof context *)
 val typing_assms = Util.get_assms #> map Thm.prop_of #> filter is_typing_jmt
 
-(* Get all visible typing judgments—Quick hack for now; should record them separately *)
+(* Search the context and return all visible typing judgments *)
 fun typing_all ctxt =
   Util.get_all_thms ctxt |> map (Thm.prop_of o snd) |> filter is_typing_jmt
 
@@ -84,36 +114,56 @@ fun get_local_typing ctxt tm =
     NONE => get_typing_in tm (typing_assms ctxt)
   | res => res
 
-(* Storage space for declared typings *)
-structure Declared_Typings = Theory_Data
+(* Dedicated theory data for proven typing judgments *)
+structure Theory_Typings = Theory_Data
 (
   type T = term Symtab.table
   val empty = Symtab.empty
   val extend = I
-  val merge = K Symtab.empty
-)
+  val merge = Symtab.join (fn key => fn (x, y) => y)
+)                                                         
 (* Accessor for the above data *)
-fun get_declared_typing thy tm =
-  case tm of
-    (Free (v, _)) => Symtab.lookup (Declared_Typings.get thy) v
-  | _ => NONE
-
-(* Store new typing information for free variables only
-   (constants should have their types declared at the moment of definition).
-   End users should use the "typing" keyword instead.
-*)
-fun put_declared_typing jmt =
+fun get_theory_typing thy tm =
+  Symtab.lookup (Theory_Typings.get thy) (Util.string_of_term tm)
+
+fun put_theory_typing jmt =
   case jmt of
     Const("HoTT_Base.has_type", _) $ term $ typing =>
-      (case term of
-        Free (v, _) => Declared_Typings.map (Symtab.update (v, typing))
-      | _ => Exn.error "Cannot declare typing assumption (not a free variable)")
+      Theory_Typings.map (Symtab.update (Util.string_of_term term, typing))
   | _ => Exn.error "Not a typing judgment"
 
 (* Get the typing of a term *)
 fun get_typing ctxt tm =
   case get_local_typing ctxt tm of
-    NONE => get_declared_typing (Proof_Context.theory_of ctxt) tm
+    NONE => get_theory_typing (Proof_Context.theory_of ctxt) tm
   | res => res
 
 end
+\<close>
+
+ML \<open>
+val _ =
+  let
+    fun store_typing ctxt = Typing.put_theory_typing o (Syntax.read_prop ctxt)
+  in
+    Outer_Syntax.local_theory
+      @{command_keyword "assume_type"}
+      "Declare typing assumptions"
+      (Parse.prop >>
+        (fn prop => fn lthy => Local_Theory.background_theory (store_typing lthy prop) lthy))
+  end
+
+val _ =
+  let
+    val parser = Parse.and_list (Parse.prop)
+    fun store_typings ctxt = fold (Typing.put_theory_typing o (Syntax.read_prop ctxt))
+  in
+    Outer_Syntax.local_theory
+      @{command_keyword "assume_types"}
+      "Declare typing assumptions"
+      (parser >>
+        (fn props => fn lthy => Local_Theory.background_theory (store_typings lthy props) lthy))
+  end
+\<close>
+
+end
diff --git a/util.ML b/util.ML
index c2e962b..f7aab9a 100644
--- a/util.ML
+++ b/util.ML
@@ -28,6 +28,7 @@ end
 structure Util: UTIL =
 struct
 
+(* Unmark a name string identifier *)
 fun unmark s =
   Lexicon.unmark_class s
   handle Fail "unprefix" =>
@@ -39,40 +40,6 @@ fun unmark s =
   handle Fail "unprefix" =>
   s
 
-fun name_and_thm (fact, thm) =
-  ((case fact of
-    Facts.Named ((name, _), _) => name
-  | Facts.Fact name => name),
-  thm)
-
-fun get_all_thms ctxt =
-  let val (_, ref_thms) = Find_Theorems.find_theorems ctxt NONE NONE true []
-  in ref_thms |> (map name_and_thm)
-  end
-
-(* Search all visible theorems (including local assumptions) containing a given name *)
-fun find_thm ctxt name =
-  let val (_, ref_thms) =
-    Find_Theorems.find_theorems ctxt NONE NONE true [(true, Find_Theorems.Name name)]
-  in
-    ref_thms |> (map name_and_thm)
-  end
-
-(* Get the fact corresponding to the Isar term "this" in the current proof scope *)
-fun get_this ctxt =
-  Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN)
-    |> Proof_Context.lookup_fact ctxt |> the |> #thms
-  handle Option.Option => (
-    if (Config.get ctxt trace) then warning "\"this\" undefined in the context" else ();
-    []
-  )
-
-(* Get all visible assumptions in the current proof scope.
-   This includes the facts introduced in the statement of the goal using "assumes",
-   as well as all facts introduced using "assume" that are visible in the current block.
- *)
-val get_assms = Assumption.all_prems_of
-
 (* Prepare a Pure pre-term, converting it to a (unchecked) term *)
 fun prep_term ctxt ptm =
   let val ptm = Term_Position.strip_positions ptm
@@ -119,4 +86,39 @@ fun string_of_term tm =
   | Abs (_, typ, body) => "Abs (_, " ^ string_of_typ typ ^ ", " ^ string_of_term body ^ ")"
   | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")"
 
-end
\ No newline at end of file
+fun name_and_thm (fact, thm) =
+  ((case fact of
+    Facts.Named ((name, _), _) => name
+  | Facts.Fact name => name),
+  thm)
+
+(* Return all visible theorems *)
+fun get_all_thms ctxt =
+  let val (_, ref_thms) = Find_Theorems.find_theorems ctxt NONE NONE true []
+  in ref_thms |> (map name_and_thm)
+  end
+
+(* Search all visible theorems (including local assumptions) containing a given name *)
+fun find_thm ctxt name =
+  let val (_, ref_thms) =
+    Find_Theorems.find_theorems ctxt NONE NONE true [(true, Find_Theorems.Name name)]
+  in
+    ref_thms |> (map name_and_thm)
+  end
+
+(* Get the fact corresponding to the Isar term "this" in the current proof scope *)
+fun get_this ctxt =
+  Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN)
+    |> Proof_Context.lookup_fact ctxt |> the |> #thms
+  handle Option.Option => (
+    if (Config.get ctxt trace) then warning "\"this\" undefined in the context" else ();
+    []
+  )
+
+(* Get all visible assumptions in the current proof scope.
+   This includes the facts introduced in the statement of the goal using "assumes",
+   as well as all facts introduced using "assume" that are visible in the current block.
+ *)
+val get_assms = Assumption.all_prems_of
+
+end