diff options
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Typing.thy (renamed from typing.ML) | 104 |
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 |