diff options
author | Josh Chen | 2020-08-09 18:34:58 +0200 |
---|---|---|
committer | Josh Chen | 2020-08-09 18:34:58 +0200 |
commit | 8f4ff41d24dd8fa6844312456d47cad4be6cb239 (patch) | |
tree | 05cb7780daead07c4714daa7e1fc19c940283b02 /spartan/core/typechecking.ML | |
parent | c530305cbcafba9f66f1a55a1b5177a62f52535c (diff) |
(FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* goals; resolving with conditional typing judgments (e.g. type family assumptions) is part of check_infer_step
Diffstat (limited to '')
-rw-r--r-- | spartan/core/typechecking.ML | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML index b7a7f9b..ca89c8c 100644 --- a/spartan/core/typechecking.ML +++ b/spartan/core/typechecking.ML @@ -50,18 +50,15 @@ fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) => 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 @ map fst (Facts.props (Proof_Context.facts_of ctxt))) - (*FIXME: Shouldn't pull nameless facts directly from context*) - in - (debug_tac ctxt "resolve" THEN resolve_tac ctxt ths i ORELSE - debug_tac ctxt "assume" THEN assume_tac ctxt i) st + 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 `typechk` rules. The current implementation does not + search over arbitrary `type` rules. The current implementation does not perform any normalization.*) fun check_infer_step facts i (ctxt, st) = let @@ -69,8 +66,12 @@ fun check_infer_step facts i (ctxt, st) = if Lib.rigid_typing_concl goal then let val net = Tactic.build_net ( - map (Simplifier.norm_hhf ctxt) facts - (*MAYBE FIXME: Remove `typechk` from this list, and instead perform + 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>) |