diff options
Diffstat (limited to 'util.ML')
-rw-r--r-- | util.ML | 102 |
1 files changed, 102 insertions, 0 deletions
@@ -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 |