(FEAT) Context data slots for known types and conditional type rules, as well as a separate one for judgmental equality rules.

(REF) Goal statement assumptions are now put into the new context data slots.

(FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data.

(REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context.
  MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`.

(REF) Fixed incompatibilities in theories.

1 files changed, 44 insertions, 0 deletions

diff --git a/spartan/core/context_facts.ML b/spartan/core/context_facts.ML
new file mode 100644
index 0000000..4b4bcd9
--- /dev/null
+++ b/spartan/core/context_facts.ML
@@ -0,0 +1,44 @@
+structure Context_Facts: sig
+
+val Eq: Proof.context -> thm Item_Net.T
+val eq: Proof.context -> thm list
+val eq_of: Proof.context -> term -> thm list
+val register_eq: thm -> Context.generic -> Context.generic
+val register_eqs: thm list -> Context.generic -> Context.generic
+val register_facts: thm list -> Proof.context -> Proof.context
+
+end = struct
+
+
+(* Equality statements *)
+
+structure Eq = Generic_Data (
+  type T = thm Item_Net.T
+  val empty = Item_Net.init Thm.eq_thm
+    (single o (#1 o Lib.dest_eq) o Thm.concl_of)
+  val extend = I
+  val merge = Item_Net.merge
+)
+
+val Eq = Eq.get o Context.Proof
+val eq = Item_Net.content o Eq
+fun eq_of ctxt tm = Item_Net.retrieve (Eq ctxt) tm
+
+fun register_eq rule =
+  if Lib.is_eq (Thm.concl_of rule) then Eq.map (Item_Net.update rule)
+  else error "Not a definitional equality judgment"
+
+fun register_eqs rules = foldr1 (op o) (map register_eq rules)
+
+
+(* Context assumptions *)
+
+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 e = register_eqs eqs handle Empty => I
+  in Context.proof_map (e o c o f) end
+
+end