1 files changed, 58 insertions, 2 deletions

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