From a5692e0ba36b372b9175d7b356f4b2fd1ee3d663 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 11 Feb 2019 15:37:18 +0100 Subject: Put typing functionality into a .thy and clean up antiquotations, which results in some reorganization of the theory import structure. --- HoTT_Base.thy | 53 ++--------------- HoTT_Methods.thy | 5 ++ HoTT_Typing.thy | 169 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ typing.ML | 119 --------------------------------------- util.ML | 72 ++++++++++++------------ 5 files changed, 217 insertions(+), 201 deletions(-) create mode 100644 HoTT_Typing.thy delete mode 100644 typing.ML diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 1eaed12..9dcf6d0 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,64 +1,21 @@ (******** -Isabelle/HoTT: Foundational definitions and notation +Isabelle/HoTT: Basic logical definitions and notation Feb 2019 -This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions. +This file completes the basic logical and functional setup of the HoTT logic. Among other things, it: -* Calls the setup of object-level type inference functionality. * Defines the universe hierarchy and its governing rules. * Defines named theorems for later use by proof methods. ********) theory HoTT_Base -imports Pure -keywords "assume_type" "assume_types" :: thy_decl +imports HoTT_Typing begin -section \Terms and typing\ - -typedecl t \ \Type of object-logic terms (which includes the types)\ - -judgment has_type :: "[t, t] \ prop" ("(3_:/ _)") - -section \Setup non-core logic functionality\ - -declare[[eta_contract=false]] \ \Do not eta-contract\ - -ML \val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\ - \ \Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\ - -text \Set up type assumption and inference functionality:\ - -ML_file "util.ML" -ML_file "typing.ML" -ML \ -val _ = - let - fun store_typing ctxt = Typing.put_declared_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_declared_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 -\ - + section \Universes\ typedecl ord \ \Type of meta-numerals\ @@ -92,6 +49,7 @@ Instead use @{method elim}, or instantiate the rules suitably. @{thm U_cumulative'} is an alternative rule used by the method @{theory_text cumulativity} in @{file HoTT_Methods.thy}. \ + section \Type families\ abbreviation (input) constraint :: "[t \ t, t, t] \ prop" ("(1_:/ _ \ _)") @@ -99,6 +57,7 @@ where "f: A \ B \ (\x. x: A \ f x: B)" text \We use the notation @{prop "B: A \ U i"} to abbreviate type families.\ + section \Named theorems\ named_theorems form diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 99f3446..088c1fa 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -9,6 +9,7 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" begin + section \Substitution and simplification\ ML_file "~~/src/Tools/misc_legacy.ML" @@ -25,6 +26,7 @@ Premises of the rule(s) applied are added as new subgoals. method compute declares comp = (subst comp) + section \Handling universes\ text \ @@ -46,6 +48,7 @@ method cumulativity declares form = ( ((elim U_cumulative | (rule U_cumulative, rule form)), provelt) ) + section \Deriving typing judgments\ method routine uses add = (assumption | rule add | rule)+ @@ -54,6 +57,7 @@ text \ The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}. \ + section \Derivation search\ text \ @@ -63,6 +67,7 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}. method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ + section \Induction\ text \ diff --git a/HoTT_Typing.thy b/HoTT_Typing.thy new file mode 100644 index 0000000..6433139 --- /dev/null +++ b/HoTT_Typing.thy @@ -0,0 +1,169 @@ +(******** +Isabelle/HoTT: Core typing judgment form and associated automation +Feb 2019 + +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 \Initial settings\ + +declare[[eta_contract=false]] \ \Do not eta-contract\ + +ML \val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\ + \ \Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\ + + +section \Terms and typing\ + +typedecl t \ \Type of object-logic terms (which includes the types)\ + +judgment has_type :: "[t, t] \ prop" ("(3_:/ _)") + + +section \Typing functionality\ + +ML_file "util.ML" + +ML \ +signature TYPING = +sig + type jmt = term + val is_typing_jmt: term -> bool + val term_of_jmt: jmt -> term + val type_of_jmt: jmt -> term + + val typing_this: Proof.context -> jmt list + val typing_assms: Proof.context -> jmt list + 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 put_theory_typing: term -> theory -> theory + val get_theory_typing: theory -> term -> term option + + val get_typing: Proof.context -> term -> term option +end + +structure Typing: TYPING = +struct + +type jmt = term + +(* Determine if a term is a typing judgment *) +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 has_type} $ t $ _) = t + | term_of_jmt _ = Exn.error "Not a typing judgment" + +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 proof context *) +val typing_assms = Util.get_assms #> map Thm.prop_of #> filter is_typing_jmt + +(* 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 + +(* Search for a term typing in a list of judgments, and return the type if found. + -- + The use of aconv_untyped as opposed to aconv is crucial here: + meta-level type inference is performed *after* syntax translation, which means that + the translation functions see an unannotated term "f" (in contrast to one annotated + e.g. "f::t") as having a blank type field. + Using aconv would result in no match ever being found for f, because any judgment + involving f records it together with its (non-blank) type field, e.g. + "Free ("f", "_")" + seen by the translation function, vs. + "Free ("f", "t")" + recorded in the typing judgment. +*) +fun get_typing_in tm jmts = + let val find_type = + fn jmt => if Term.aconv_untyped (tm, term_of_jmt jmt) then SOME (type_of_jmt jmt) else NONE + in get_first find_type jmts end + +(* Search for typing in the local proof context (no global data). + We search the facts bound to "this" before searching the assumptions. + -- + A previous version of this function passed the argument + (typing_this ctxt @ typing_assms ctxt) + to get_typing_in. + -- + This version only evaluates successive lists if the search on the previous list was unsuccessful. +*) +fun get_local_typing ctxt tm = + case get_typing_in tm (typing_this ctxt) of + NONE => get_typing_in tm (typing_assms ctxt) + | res => res + +(* 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 = Symtab.join (fn key => fn (x, y) => y) +) +(* Accessor for the above data *) +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 => + 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_theory_typing (Proof_Context.theory_of ctxt) tm + | res => res + +end +\ + +ML \ +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 +\ + +end diff --git a/typing.ML b/typing.ML deleted file mode 100644 index 8c3d42c..0000000 --- a/typing.ML +++ /dev/null @@ -1,119 +0,0 @@ -(******** -Isabelle/HoTT: typing.ML -Feb 2019 - -Functionality for object-level type inference. - -********) - -signature TYPING = -sig - type jmt = term - val is_typing_jmt: term -> bool - val term_of_jmt: jmt -> term - val type_of_jmt: jmt -> term - - val typing_this: Proof.context -> jmt list - val typing_assms: Proof.context -> jmt list - 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 get_typing: Proof.context -> term -> term option -end - -structure Typing: TYPING = -struct - -type jmt = term - -(* Determine if a term is a typing judgment *) -fun is_typing_jmt (@{const HoTT_Base.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 - | term_of_jmt _ = Exn.error "Not a typing judgment" - -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 = Util.get_this ctxt |> map Thm.prop_of |> filter is_typing_jmt - -(* Get the typing assumptions in the current 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 *) -fun typing_all ctxt = - 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. - -- - The use of aconv_untyped as opposed to aconv is crucial here: - meta-level type inference is performed *after* syntax translation, which means that - the translation functions see an unannotated term "f" (in contrast to one annotated - e.g. "f::t") as having a blank type field. - Using aconv would result in no match ever being found for f, because any judgment - involving f records it together with its (non-blank) type field, e.g. - "Free ("f", "_")" - seen by the translation function, vs. - "Free ("f", "t")" - recorded in the typing judgment. -*) -fun get_typing_in tm jmts = - let val find_type = - fn jmt => if Term.aconv_untyped (tm, term_of_jmt jmt) then SOME (type_of_jmt jmt) else NONE - in get_first find_type jmts end - -(* Search for typing in the local proof context (no global data). - We search the facts bound to "this" before searching the assumptions. - -- - A previous version of this function passed the argument - (typing_this ctxt @ typing_assms ctxt) - to get_typing_in. - -- - This version only evaluates successive lists if the search on the previous list was unsuccessful. -*) -fun get_local_typing ctxt tm = - case get_typing_in tm (typing_this ctxt) of - NONE => get_typing_in tm (typing_assms ctxt) - | res => res - -(* Storage space for declared typings *) -structure Declared_Typings = Theory_Data -( - type T = term Symtab.table - val empty = Symtab.empty - val extend = I - val merge = K Symtab.empty -) -(* 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 = - 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)") - | _ => 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 - | res => res - -end diff --git a/util.ML b/util.ML index c2e962b..f7aab9a 100644 --- a/util.ML +++ b/util.ML @@ -28,6 +28,7 @@ end structure Util: UTIL = struct +(* Unmark a name string identifier *) fun unmark s = Lexicon.unmark_class s handle Fail "unprefix" => @@ -39,40 +40,6 @@ fun unmark 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 = - Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN) - |> Proof_Context.lookup_fact ctxt |> the |> #thms - handle Option.Option => ( - 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 @@ -119,4 +86,39 @@ fun string_of_term tm = | Abs (_, typ, body) => "Abs (_, " ^ string_of_typ typ ^ ", " ^ string_of_term body ^ ")" | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")" -end \ No newline at end of file +fun name_and_thm (fact, thm) = + ((case fact of + Facts.Named ((name, _), _) => name + | Facts.Fact name => name), + thm) + +(* Return all visible theorems *) +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 = + Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN) + |> Proof_Context.lookup_fact ctxt |> the |> #thms + handle Option.Option => ( + 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 -- cgit v1.2.3