aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--spartan/core/Spartan.thy3
-rw-r--r--spartan/core/context_facts.ML60
-rw-r--r--spartan/core/tactics.ML2
-rw-r--r--spartan/core/types.ML63
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 \<open>Infrastructure\<close>
ML_file \<open>lib.ML\<close>
+ML_file \<open>context_facts.ML\<close>
ML_file \<open>context_tactical.ML\<close>
subsection \<open>Type-checking/inference\<close>
@@ -202,6 +203,7 @@ lemmas
[comp] = beta Sig_comp and
[cong] = Pi_cong lam_cong Sig_cong
+\<comment> \<open>Type-checking\<close>
ML_file \<open>types.ML\<close>
method_setup typechk =
@@ -214,7 +216,6 @@ method_setup known =
subsection \<open>Statement commands\<close>
-ML_file \<open>context_facts.ML\<close>
ML_file \<open>focus.ML\<close>
ML_file \<open>elaboration.ML\<close>
ML_file \<open>elaborated_statement.ML\<close>
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 **)