From d172f9d35a9a1680ec15e4c61e5becbbc92d2ce7 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 14 Aug 2020 11:21:59 +0200 Subject: reorganize --- spartan/core/Spartan.thy | 3 ++- spartan/core/context_facts.ML | 60 +++++++++++++++++++++++++++++++++++++++-- spartan/core/tactics.ML | 2 +- spartan/core/types.ML | 63 +++---------------------------------------- 4 files changed, 64 insertions(+), 64 deletions(-) diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 412881b..411eedd 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -184,6 +184,7 @@ axiomatization where section \Infrastructure\ ML_file \lib.ML\ +ML_file \context_facts.ML\ ML_file \context_tactical.ML\ subsection \Type-checking/inference\ @@ -202,6 +203,7 @@ lemmas [comp] = beta Sig_comp and [cong] = Pi_cong lam_cong Sig_cong +\ \Type-checking\ ML_file \types.ML\ method_setup typechk = @@ -214,7 +216,6 @@ method_setup known = subsection \Statement commands\ -ML_file \context_facts.ML\ ML_file \focus.ML\ ML_file \elaboration.ML\ ML_file \elaborated_statement.ML\ diff --git a/spartan/core/context_facts.ML b/spartan/core/context_facts.ML index 4b4bcd9..c372ca7 100644 --- a/spartan/core/context_facts.ML +++ b/spartan/core/context_facts.ML @@ -1,5 +1,17 @@ structure Context_Facts: sig +val Known: Proof.context -> thm Item_Net.T +val known: Proof.context -> thm list +val known_of: Proof.context -> term -> thm list +val register_known: thm -> Context.generic -> Context.generic +val register_knowns: thm list -> Context.generic -> Context.generic + +val Cond: Proof.context -> thm Item_Net.T +val cond: Proof.context -> thm list +val cond_of: Proof.context -> term -> thm list +val register_cond: thm -> Context.generic -> Context.generic +val register_conds: thm list -> Context.generic -> Context.generic + val Eq: Proof.context -> thm Item_Net.T val eq: Proof.context -> thm list val eq_of: Proof.context -> term -> thm list @@ -9,6 +21,50 @@ val register_facts: thm list -> Proof.context -> Proof.context end = struct +(* Known types *) + +structure Known = Generic_Data ( + type T = thm Item_Net.T + val empty = Item_Net.init Thm.eq_thm + (single o Lib.term_of_typing o Thm.prop_of) + val extend = I + val merge = Item_Net.merge +) + +val Known = Known.get o Context.Proof +val known = Item_Net.content o Known +fun known_of ctxt tm = Item_Net.retrieve (Known ctxt) tm + +fun register_known typing = + if Lib.is_typing (Thm.prop_of typing) then Known.map (Item_Net.update typing) + else error "Not a type judgment" + +fun register_knowns typings = foldr1 (op o) (map register_known typings) + + +(* Conditional type rules *) + +(*Two important cases: 1. general type inference rules and 2. type family + judgments*) + +structure Cond = Generic_Data ( + type T = thm Item_Net.T + val empty = Item_Net.init Thm.eq_thm + (single o Lib.term_of_typing o Thm.concl_of) + val extend = I + val merge = Item_Net.merge +) + +val Cond = Cond.get o Context.Proof +val cond = Item_Net.content o Cond +fun cond_of ctxt tm = Item_Net.retrieve (Cond ctxt) tm + +fun register_cond rule = + if Lib.is_typing (Thm.concl_of rule) then Cond.map (Item_Net.update rule) + else error "Not a conditional type judgment" + +fun register_conds rules = foldr1 (op o) (map register_cond rules) + (* Equality statements *) @@ -36,8 +92,8 @@ fun register_eqs rules = foldr1 (op o) (map register_eq rules) fun register_facts ths = let val (facts, conds, eqs) = Lib.partition_judgments ths - val f = Types.register_knowns facts handle Empty => I - val c = Types.register_conds conds handle Empty => I + val f = register_knowns facts handle Empty => I + val c = register_conds conds handle Empty => I val e = register_eqs eqs handle Empty => I in Context.proof_map (e o c o f) end diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML index 0c46ef0..923a3a7 100644 --- a/spartan/core/tactics.ML +++ b/spartan/core/tactics.ML @@ -111,7 +111,7 @@ fun elim_ctac tms = [] => CONTEXT_TACTIC' (fn ctxt => eresolve_tac ctxt (map #1 (Elim.rules ctxt))) | major :: _ => CONTEXT_SUBGOAL (fn (goal, _) => fn cst as (ctxt, st) => let - val facts = map Thm.prop_of (Types.known ctxt) + val facts = map Thm.prop_of (Context_Facts.known ctxt) val prems = Logic.strip_assums_hyp goal val template = Lib.typing_of_term major val types = filter (fn th => Term.could_unify (template, th)) (facts @ prems) diff --git a/spartan/core/types.ML b/spartan/core/types.ML index a521f7c..70e5057 100644 --- a/spartan/core/types.ML +++ b/spartan/core/types.ML @@ -1,23 +1,11 @@ -(* Title: typechecking.ML +(* Title: types.ML Author: Joshua Chen -Type information and type-checking infrastructure. +Type-checking infrastructure. *) structure Types: sig -val Known: Proof.context -> thm Item_Net.T -val known: Proof.context -> thm list -val known_of: Proof.context -> term -> thm list -val register_known: thm -> Context.generic -> Context.generic -val register_knowns: thm list -> Context.generic -> Context.generic - -val Cond: Proof.context -> thm Item_Net.T -val cond: Proof.context -> thm list -val cond_of: Proof.context -> term -> thm list -val register_cond: thm -> Context.generic -> Context.generic -val register_conds: thm list -> Context.generic -> Context.generic - val debug_typechk: bool Config.T val known_ctac: thm list -> int -> context_tactic @@ -25,52 +13,7 @@ val check_infer: thm list -> int -> context_tactic end = struct - -(** Context data **) - -(* Known types *) - -structure Known = Generic_Data ( - type T = thm Item_Net.T - val empty = Item_Net.init Thm.eq_thm - (single o Lib.term_of_typing o Thm.prop_of) - val extend = I - val merge = Item_Net.merge -) - -val Known = Known.get o Context.Proof -val known = Item_Net.content o Known -fun known_of ctxt tm = Item_Net.retrieve (Known ctxt) tm - -fun register_known typing = - if Lib.is_typing (Thm.prop_of typing) then Known.map (Item_Net.update typing) - else error "Not a type judgment" - -fun register_knowns typings = foldr1 (op o) (map register_known typings) - -(* Conditional type rules *) - -(*Two important cases: 1. general type inference rules and 2. type family - judgments*) - -structure Cond = Generic_Data ( - type T = thm Item_Net.T - val empty = Item_Net.init Thm.eq_thm - (single o Lib.term_of_typing o Thm.concl_of) - val extend = I - val merge = Item_Net.merge -) - -val Cond = Cond.get o Context.Proof -val cond = Item_Net.content o Cond -fun cond_of ctxt tm = Item_Net.retrieve (Cond ctxt) tm - -fun register_cond rule = - if Lib.is_typing (Thm.concl_of rule) then Cond.map (Item_Net.update rule) - else error "Not a conditional type judgment" - -fun register_conds rules = foldr1 (op o) (map register_cond rules) - +open Context_Facts (** [type] attribute **) -- cgit v1.2.3