diff options
Diffstat (limited to '')
-rw-r--r-- | spartan/core/typechecking.ML | 96 |
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 |