diff options
Diffstat (limited to 'typing.ML')
-rw-r--r-- | typing.ML | 104 |
1 files changed, 3 insertions, 101 deletions
@@ -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 |