1 files changed, 77 insertions, 27 deletions

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