(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, 0 insertions, 96 deletions

diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML
deleted file mode 100644
index ca89c8c..0000000
--- a/spartan/core/typechecking.ML
+++ /dev/null
@@ -1,96 +0,0 @@
-(*  Title:      typechecking.ML
-    Author:     Joshua Chen
-
-Type information and type-checking infrastructure.
-*)
-
-structure Types: sig
-
-val Data: Proof.context -> thm Item_Net.T
-val types: Proof.context -> term -> thm list
-val put_type: thm -> Proof.context -> Proof.context
-val put_types: thm list -> Proof.context -> Proof.context
-
-val debug_typechk: bool Config.T
-
-val known_ctac: thm list -> int -> context_tactic
-val check_infer: thm list -> int -> context_tactic
-
-end = struct
-
-
-(* Context data *)
-
-structure Data = 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 Data = Data.get o Context.Proof
-fun types ctxt tm = Item_Net.retrieve (Data ctxt) tm
-fun put_type typing = Context.proof_map (Data.map (Item_Net.update typing))
-fun put_types typings = foldr1 (op o) (map put_type typings)
-
-
-(* Context tactics for type-checking *)
-
-val debug_typechk = Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false)
-
-fun debug_tac ctxt s =
-  if Config.get ctxt debug_typechk then print_tac ctxt s else all_tac
-
-(*Solves goals without metavariables and type inference problems by resolving
-  with facts or assumption from inline premises.*)
-fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
-  TACTIC_CONTEXT ctxt
-    let val concl = Logic.strip_assums_concl goal in
-      if Lib.no_vars concl orelse
-        (Lib.is_typing concl andalso Lib.no_vars (Lib.term_of_typing concl))
-      then
-        let val ths = map (Simplifier.norm_hhf ctxt) facts
-        in st |>
-          (assume_tac ctxt ORELSE' resolve_tac ctxt ths THEN_ALL_NEW K no_tac) i
-        end
-      else Seq.empty
-    end)
-
-(*Simple bidirectional typing tactic, with some nondeterminism from backtracking
-  search over arbitrary `type` rules. The current implementation does not
-  perform any normalization.*)
-fun check_infer_step facts i (ctxt, st) =
-  let
-    val tac = SUBGOAL (fn (goal, i) =>
-      if Lib.rigid_typing_concl goal
-      then
-        let val net = Tactic.build_net (
-          map (Simplifier.norm_hhf ctxt)
-            (*FIXME: Shouldn't pull nameless facts directly from context. Note
-              that we *do* need to be able to resolve with conditional
-              statements expressing type family judgments*)
-            (facts @ map fst (Facts.props (Proof_Context.facts_of ctxt)))
-          (*MAYBE FIXME: Remove `type` from this list, and instead perform
-            definitional unfolding to (w?)hnf.*)
-          @(Named_Theorems.get ctxt \<^named_theorems>\<open>type\<close>)
-          @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>)
-          @(Named_Theorems.get ctxt \<^named_theorems>\<open>intr\<close>)
-          @(map #1 (Elim.rules ctxt)))
-        in (resolve_from_net_tac ctxt net) i end
-      else no_tac)
-
-    val ctxt' = ctxt (*TODO: Use this to store already-derived typing judgments*)
-  in
-    TACTIC_CONTEXT ctxt' (tac i st)
-  end
-
-fun check_infer facts i (cst as (_, st)) =
-  let val ctac = known_ctac facts CORELSE' check_infer_step facts
-  in
-    cst |> (ctac i CTHEN
-      CREPEAT_IN_RANGE i (Thm.nprems_of st - i) (CTRY o CREPEAT_ALL_NEW_FWD ctac))
-  end
-
-
-end