diff options
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Base.thy | 4 | ||||
| -rw-r--r-- | Prod.thy | 2 | ||||
| -rw-r--r-- | typing.ML | 104 | ||||
| -rw-r--r-- | util.ML | 102 |
4 files changed, 108 insertions, 104 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 23e51e5..1eaed12 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -30,10 +30,10 @@ 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>The following file sets up type assumption and inference functionality.\<close> +text \<open>Set up type assumption and inference functionality:\<close> +ML_file "util.ML" ML_file "typing.ML" - ML \<open> val _ = let @@ -79,7 +79,7 @@ syntax "_compose" :: "[t, t] \<Rightarrow> t" (infixr "o" 110) parse_translation \<open> let fun compose_tr ctxt [g, f] = let - val [g, f] = [g, f] |> map (Typing.prep_term ctxt) + val [g, f] = [g, f] |> map (Util.prep_term ctxt) val dom = case f of Const ("Prod.lam", _) $ T $ _ => T @@ -6,73 +6,6 @@ Functionality for object-level type inference. ********) -(* ====================================== Helper functions ====================================== *) - -signature TYPING_LIB = -sig - (* Lexical functions *) - val unmark: string -> string - - (* General functions *) - val get_all_thms: Proof.context -> (string * thm) list - val find_thm: Proof.context -> string -> (string * thm) list - - (* Get specific theorems *) - val get_this: Proof.context -> thm list - val get_assms: Proof.context -> thm list -end - -structure Typing_Lib: TYPING_LIB = -struct - -fun unmark s = - Lexicon.unmark_class s - handle Fail "unprefix" => - Lexicon.unmark_type s - handle Fail "unprefix" => - Lexicon.unmark_const s - handle Fail "unprefix" => - Lexicon.unmark_fixed 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 = - Proof_Context.get_fact ctxt (Facts.named "local.this") - handle ERROR "Undefined fact: \"local.this\"" => ( - 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 - -(* ================================ Type inference functionality ================================ *) - signature TYPING = sig type jmt = term @@ -91,8 +24,6 @@ sig val put_declared_typing: term -> theory -> theory val get_typing: Proof.context -> term -> term option - - val prep_term: Proof.context -> term -> term end structure Typing: TYPING = @@ -112,14 +43,14 @@ fun type_of_jmt (@{const HoTT_Base.has_type} $ _ $ T) = T | type_of_jmt _ = Exn.error "Not a typing judgment" (* Get typing assumptions in "this" *) -fun typing_this ctxt = Typing_Lib.get_this ctxt |> map Thm.prop_of |> filter is_typing_jmt +fun typing_this ctxt = Util.get_this ctxt |> map Thm.prop_of |> filter is_typing_jmt (* Get the typing assumptions in the current context *) -val typing_assms = Typing_Lib.get_assms #> map Thm.prop_of #> filter is_typing_jmt +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 *) fun typing_all ctxt = - Typing_Lib.get_all_thms ctxt |> map (Thm.prop_of o snd) |> filter is_typing_jmt + Util.get_all_thms ctxt |> map (Thm.prop_of o snd) |> filter is_typing_jmt (* Search for a term typing in a list of judgments, and return the type if found. -- @@ -185,33 +116,4 @@ fun get_typing ctxt tm = NONE => get_declared_typing (Proof_Context.theory_of ctxt) tm | res => res -(* Prepare a Pure pre-term, converting it partway to a (unchecked) term *) -fun prep_term ctxt ptm = - let val ptm = Term_Position.strip_positions ptm - in - (case ptm of - Const ("_constrain", _) $ Free (t, _) $ - (Const ("\<^type>fun", _) $ Const(typ1, _) $ Const (typ2, _)) => - let - val typ1 = Lexicon.unmark_type typ1 - val typ2 = Lexicon.unmark_type typ2 - val typ = typ1 ^ "\<Rightarrow>" ^ typ2 |> Syntax.read_typ ctxt - in Free (t, typ) end - | Const ("_constrain", _) $ t $ Const (typ, _) => - let - val T = Syntax.read_typ ctxt (Lexicon.unmark_type typ) - in - case t of - Free (s, _) => Free (s, T) - | Const (s, _) => Const (Lexicon.unmark_const s, T) - | _ => Exn.error "Unimplemented term constraint handler" - end - | ptm1 $ ptm2 => - (prep_term ctxt ptm1) $ (prep_term ctxt ptm2) - | Abs (t, T, ptm') => - Abs (t, T, prep_term ctxt ptm') - | Const (t, T) => Const (Typing_Lib.unmark t, T) - | t => t) - end - end @@ -0,0 +1,102 @@ +(******** +Isabelle/HoTT: util.ML +Feb 2019 + +Libary of various helper functions. + +********) + +signature UTIL = +sig + (* Lexical functions *) + val unmark: string -> string + + (* Functions on terms *) + val prep_term: Proof.context -> term -> term + + (* General functions *) + val get_all_thms: Proof.context -> (string * thm) list + val find_thm: Proof.context -> string -> (string * thm) list + + (* Get specific theorems *) + val get_this: Proof.context -> thm list + val get_assms: Proof.context -> thm list +end + +structure Util: UTIL = +struct + +fun unmark s = + Lexicon.unmark_class s + handle Fail "unprefix" => + Lexicon.unmark_type s + handle Fail "unprefix" => + Lexicon.unmark_const s + handle Fail "unprefix" => + Lexicon.unmark_fixed 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 = + Proof_Context.get_fact ctxt (Facts.named "local.this") + handle ERROR "Undefined fact: \"local.this\"" => ( + 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 + in + (case ptm of + Const ("_constrain", _) $ Free (t, _) $ + (Const ("\<^type>fun", _) $ Const(typ1, _) $ Const (typ2, _)) => + let + val typ1 = Lexicon.unmark_type typ1 + val typ2 = Lexicon.unmark_type typ2 + val typ = typ1 ^ "\<Rightarrow>" ^ typ2 |> Syntax.read_typ ctxt + in Free (t, typ) end + | Const ("_constrain", _) $ t $ Const (typ, _) => + let + val T = Syntax.read_typ ctxt (Lexicon.unmark_type typ) + in + case t of + Free (s, _) => Free (s, T) + | Const (s, _) => Const (Lexicon.unmark_const s, T) + | _ => Exn.error "Unimplemented term constraint handler" + end + | ptm1 $ ptm2 => + (prep_term ctxt ptm1) $ (prep_term ctxt ptm2) + | Abs (t, T, ptm') => + Abs (t, T, prep_term ctxt ptm') + | Const (t, T) => Const (unmark t, T) + | t => t) + end + +end
\ No newline at end of file |