From 8f4ff41d24dd8fa6844312456d47cad4be6cb239 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 9 Aug 2020 18:34:58 +0200 Subject: (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 --- hott/Equivalence.thy | 13 ++++++------- spartan/core/tactics.ML | 4 ++-- spartan/core/typechecking.ML | 19 ++++++++++--------- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index d85e6de..7d1f2b1 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -162,8 +162,7 @@ Corollary (def) commute_homotopy': rewrite at "_ = \" id_comp[symmetric]) have "H (f x) \ H x = H (f x) \ (id A)[H x]" - by (rule left_whisker) (fact, rule - ap_id[where ?A=A and ?x="f x" and ?y=x, simplified id_comp, symmetric]) + by (rule left_whisker, transport eq: ap_id) (reduce+, refl) also have [simplified id_comp]: "H (f x) \ (id A)[H x] = f[H x] \ H x" by (rule commute_homotopy) finally have *: "{}" by this @@ -433,28 +432,28 @@ Lemma (def) equiv_if_equal: \<^enum> vars A B apply (rewrite at A in "A \ B" id_comp[symmetric]) using [[solve_side_conds=1]] - apply (rewrite at B in "_ \ B" id_comp[symmetric]) + apply (rewrite at B in "_ \ B" id_comp[symmetric], fact) apply (rule transport, rule Ui_in_USi) apply (rule lift_universe_codomain, rule Ui_in_USi) apply (typechk, rule Ui_in_USi) - done + by facts \<^enum> vars A using [[solve_side_conds=1]] apply (subst transport_comp) \ by (rule Ui_in_USi) \ by reduce (rule in_USi_if_in_Ui) - \ by reduce (rule id_is_biinv) + \ by reduce (rule id_is_biinv, fact) done done \<^item> \ \Similar proof as in the first subgoal above\ apply (rewrite at A in "A \ B" id_comp[symmetric]) using [[solve_side_conds=1]] - apply (rewrite at B in "_ \ B" id_comp[symmetric]) + apply (rewrite at B in "_ \ B" id_comp[symmetric], fact) apply (rule transport, rule Ui_in_USi) apply (rule lift_universe_codomain, rule Ui_in_USi) apply (typechk, rule Ui_in_USi) - done + by facts done (*Uncomment this to see all implicits from here on. diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML index 446af15..45fd119 100644 --- a/spartan/core/tactics.ML +++ b/spartan/core/tactics.ML @@ -82,8 +82,8 @@ fun internalize_fact_tac t = Drule.infer_instantiate' ctxt [NONE, NONE, SOME B, SOME a] @{thm PiE} in HEADGOAL (resolve_tac ctxt [resolvent]) - (*known_tac infers the correct type T inferred by unification*) - THEN SOMEGOAL (NO_CONTEXT_TACTIC ctxt o Types.known_ctac []) + (*Infer the correct type T*) + THEN SOMEGOAL (NO_CONTEXT_TACTIC ctxt o Types.check_infer []) end) fun elim_core_tac tms types ctxt = 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>\type\) @(Named_Theorems.get ctxt \<^named_theorems>\form\) -- cgit v1.2.3