From 3bcaf5d1c40b513f8e4590f7d38d3eef8393092e Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 16 Jul 2020 16:46:09 +0200 Subject: Checkpoint. THIS BUILD WILL FAIL --- spartan/core/Spartan.thy | 105 +++++++++++++++------ spartan/core/context_tactical.ML | 129 ++++++++++++++++++++++++++ spartan/core/lib.ML | 3 + spartan/core/tactics.ML | 7 -- spartan/core/tactics2.ML | 191 +++++++++++++++++++++++++++++++++++++++ spartan/core/typechecking.ML | 67 +++++++++++--- 6 files changed, 451 insertions(+), 51 deletions(-) create mode 100644 spartan/core/context_tactical.ML create mode 100644 spartan/core/tactics2.ML diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 8fa6cfe..1b9093b 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -10,22 +10,29 @@ keywords "focus" "\" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and "congruence" "print_coercions" :: thy_decl and "rhs" "derive" "prems" "vars" :: quasi_command - begin section \Prelude\ +paragraph \Set up the meta-logic just so.\ + +paragraph \Notation.\ + declare [[eta_contract=false]] +text \ + Rebind notation for meta-lambdas since we want to use `\` for the object + lambdas. Meta-functions now use the binder `fn`. +\ setup \ let val typ = Simple_Syntax.read_typ fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range) in Sign.del_syntax (Print_Mode.ASCII, true) - [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3fn _./ _)", [0, 3], 3))] + [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3%_./ _)", [0, 3], 3))] #> Sign.del_syntax Syntax.mode_default [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3\_./ _)", [0, 3], 3))] #> Sign.add_syntax Syntax.mode_default @@ -38,11 +45,16 @@ translations "a $ b" \ "a (b)" abbreviation (input) K where "K x \ fn _. x" +paragraph \ + Deeply embed dependent type theory: meta-type of expressions, and typing + judgment. +\ + typedecl o judgment has_type :: \o \ o \ prop\ ("(2_:/ _)" 999) -text \Type annotations:\ +text \Type annotations for type-checking and inference.\ definition anno :: \o \ o \ o\ ("'(_ : _')") where "(a : A) \ a" if "a: A" @@ -51,7 +63,9 @@ lemma anno: "a: A \ (a : A): A" by (unfold anno_def) -section \Universes\ +section \Axioms\ + +subsection \Universes\ typedecl lvl \ \Universe levels\ @@ -77,7 +91,7 @@ lemma lift_U: by (erule U_cumulative, rule lt_S) -section \\-type\ +subsection \\-type\ axiomatization Pi :: \o \ (o \ o) \ o\ and @@ -100,9 +114,9 @@ translations abbreviation Fn (infixr "\" 40) where "A \ B \ \_: A. B" axiomatization where - PiF: "\\x. x: A \ B x: U i; A: U i\ \ \x: A. B x: U i" and + PiF: "\A: U i; \x. x: A \ B x: U i\ \ \x: A. B x: U i" and - PiI: "\\x. x: A \ b x: B x; A: U i\ \ \x: A. b x: \x: A. B x" and + PiI: "\A: U i; \x. x: A \ b x: B x\ \ \x: A. b x: \x: A. B x" and PiE: "\f: \x: A. B x; a: A\ \ f `a: B a" and @@ -113,14 +127,14 @@ axiomatization where Pi_cong: "\ \x. x: A \ B x \ B' x; A: U i; - \x. x: A \ B x: U i; - \x. x: A \ B' x: U i + \x. x: A \ B x: U j; + \x. x: A \ B' x: U j \ \ \x: A. B x \ \x: A. B' x" and lam_cong: "\\x. x: A \ b x \ c x; A: U i\ \ \x: A. b x \ \x: A. c x" -section \\-type\ +subsection \\-type\ axiomatization Sig :: \o \ (o \ o) \ o\ and @@ -138,16 +152,16 @@ abbreviation "and" (infixl "\" 60) where "A \ B \ A \ B" axiomatization where - SigF: "\\x. x: A \ B x: U i; A: U i\ \ \x: A. B x: U i" and + SigF: "\A: U i; \x. x: A \ B x: U i\ \ \x: A. B x: U i" and SigI: "\\x. x: A \ B x: U i; a: A; b: B a\ \ : \x: A. B x" and SigE: "\ p: \x: A. B x; A: U i; - \x. x : A \ B x: U i; - \x y. \x: A; y: B x\ \ f x y: C ; - \p. p: \x: A. B x \ C p: U i + \x. x : A \ B x: U j; + \p. p: \x: A. B x \ C p: U k; + \x y. \x: A; y: B x\ \ f x y: C \ \ SigInd A (fn x. B x) (fn p. C p) f p: C p" and Sig_comp: "\ @@ -161,22 +175,23 @@ axiomatization where Sig_cong: "\ \x. x: A \ B x \ B' x; A: U i; - \x. x : A \ B x: U i; - \x. x : A \ B' x: U i + \x. x : A \ B x: U j; + \x. x : A \ B' x: U j \ \ \x: A. B x \ \x: A. B' x" section \Infrastructure\ ML_file \lib.ML\ -ML_file \typechecking.ML\ +ML_file \context_tactical.ML\ subsection \Proof commands\ +ML_file \focus.ML\ + named_theorems typechk ML_file \goals.ML\ -ML_file \focus.ML\ subsection \Congruence automation\ @@ -184,19 +199,22 @@ consts "rhs" :: \'a\ ("..") ML_file \congruence.ML\ +subsection \Theorem attributes, type-checking and proof methods\ + +named_theorems intros and comps + ML_file \elimination.ML\ \ \elimination rules\ ML_file \cases.ML\ \ \case reasoning rules\ -subsection \Methods\ - -named_theorems intros and comps lemmas - [intros] = PiF PiI SigF SigI and + [intros] = anno PiF PiI SigF SigI and [elims "?f"] = PiE and [elims "?p"] = SigE and [comps] = beta Sig_comp and [cong] = Pi_cong lam_cong Sig_cong +ML_file \typechecking.ML\ +ML_file \tactics2.ML\ ML_file \tactics.ML\ method_setup assumptions = @@ -223,12 +241,12 @@ method_setup cases = \Args.term >> (fn tm => fn ctxt => SIMPLE_METHOD' (cases_tac tm ctxt))\ (*This could possibly use additional simplification hints via a simp: modifier*) -method_setup typechk = +method_setup typechk' = \Scan.succeed (fn ctxt => SIMPLE_METHOD' ( SIDE_CONDS (typechk_tac ctxt) ctxt)) (* CHANGED (ALLGOALS (TRY o typechk_tac ctxt)))) *)\ -method_setup rule = +method_setup rule' = \Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (rule_tac ths ctxt) ctxt)))\ @@ -237,6 +255,16 @@ method_setup dest = >> (fn (opt_n, ths) => fn ctxt => SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (dest_tac opt_n ths ctxt) ctxt)))\ +(*NEW*) +method_setup typechk = + \Scan.succeed (K (CONTEXT_METHOD ( + CHEADGOAL o Types.check_infer)))\ + +method_setup rule = + \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( + CHEADGOAL o Tactics2.SIDE_CONDS (Tactics2.rule_tac ths))))\ + + subsection \Reflexivity\ named_theorems refl @@ -348,12 +376,21 @@ lemma eta_exp: shows "f \ \x: A. f x" by (rule eta[symmetric]) +lemma refine_codomain: + assumes + "A: U i" + "f: \x: A. B x" + "\x. x: A \ f `x: C x" + shows "f: \x: A. C x" + by (subst eta_exp) + lemma lift_universe_codomain: assumes "A: U i" "f: A \ U j" shows "f: A \ U (S j)" - apply (sub eta_exp) - apply known - apply (Pure.rule intros; rule lift_U) + (*FIXME: Temporary; should be fixed once all methods are rewritten to use + the new typechk*) + apply (Pure.rule refine_codomain, typechk, typechk) + apply (Pure.rule lift_U, typechk) done subsection \Function composition\ @@ -472,7 +509,7 @@ definition fst_i ("fst") definition snd_i ("snd") where [implicit]: "snd \ Spartan.snd ? ?" -translations +no_translations "fst" \ "CONST Spartan.fst A B" "snd" \ "CONST Spartan.snd A B" @@ -483,14 +520,22 @@ Lemma fst [typechk]: "p: \x: A. B x" "A: U i" "\x. x: A \ B x: U i" shows "fst p: A" - by typechk + \ \This can't be solved by a single application of `typechk`; it needs + multiple (two) passes. Something to do with constraint/subgoal reordering.\ + apply (Pure.rule elims) + apply (Pure.rule typechk) + apply known [1] + defer \ \The deferred subgoal is an inhabitation problem.\ + apply known [1] + by known + Lemma snd [typechk]: assumes "p: \x: A. B x" "A: U i" "\x. x: A \ B x: U i" shows "snd p: B (fst p)" - by typechk + by typechk+ method fst for p::o = rule fst[of p] method snd for p::o = rule snd[of p] diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML new file mode 100644 index 0000000..78991a9 --- /dev/null +++ b/spartan/core/context_tactical.ML @@ -0,0 +1,129 @@ +(* Title: context_tactical.ML + Author: Joshua Chen + +More context tactics, and context tactic combinators. +*) + +infix 1 CTHEN CTHEN' CTHEN_ALL_NEW CTHEN_ALL_NEW_FWD +infix 0 CORELSE CAPPEND CORELSE' CAPPEND' + +structure Context_Tactical: +sig + +type context_tactic' = int -> context_tactic +val all_ctac: context_tactic +val no_ctac: context_tactic +val print_ctac: (Proof.context -> string) -> context_tactic +val CTHEN: context_tactic * context_tactic -> context_tactic +val CORELSE: context_tactic * context_tactic -> context_tactic +val CAPPEND: context_tactic * context_tactic -> context_tactic +val CTHEN': context_tactic' * context_tactic' -> context_tactic' +val CORELSE': context_tactic' * context_tactic' -> context_tactic' +val CAPPEND': context_tactic' * context_tactic' -> context_tactic' +val CTRY: context_tactic -> context_tactic +val CREPEAT: context_tactic -> context_tactic +val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic +val CCHANGED: context_tactic -> context_tactic +val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic' +val CREPEAT_ALL_NEW: context_tactic' -> context_tactic' +val CTHEN_ALL_NEW_FWD: context_tactic' * context_tactic' -> context_tactic' +val CREPEAT_ALL_NEW_FWD: context_tactic' -> context_tactic' +val CHEADGOAL: context_tactic' -> context_tactic +val CALLGOALS: context_tactic' -> context_tactic + +end = struct + +type context_tactic' = int -> context_tactic + +val all_ctac = Seq.make_results o Seq.single +val no_ctac = K Seq.empty +fun print_ctac f (ctxt, st) = CONTEXT_TACTIC (print_tac ctxt (f ctxt)) (ctxt, st) + +fun (ctac1 CTHEN ctac2) cst = Seq.maps_results ctac2 (ctac1 cst) + +fun (ctac1 CORELSE ctac2) cst = + (case Seq.pull (ctac1 cst) of + NONE => ctac2 cst + | some => Seq.make (fn () => some)) + +fun (ctac1 CAPPEND ctac2) cst = + Seq.append (ctac1 cst) (Seq.make (fn () => Seq.pull (ctac2 cst))) + +fun (ctac1 CTHEN' ctac2) x = ctac1 x CTHEN ctac2 x +fun (ctac1 CORELSE' ctac2) x = ctac1 x CORELSE ctac2 x +fun (ctac1 CAPPEND' ctac2) x = ctac1 x CAPPEND ctac2 x + +fun CTRY ctac = ctac CORELSE all_ctac + +fun CREPEAT ctac = + let + fun rep qs cst = + (case Seq.pull (Seq.filter_results (ctac cst)) of + NONE => SOME (cst, Seq.make (fn () => repq qs)) + | SOME (cst', q) => rep (q :: qs) cst') + and repq [] = NONE + | repq (q :: qs) = + (case Seq.pull q of + NONE => repq qs + | SOME (cst, q) => rep (q :: qs) cst); + in fn cst => Seq.make_results (Seq.make (fn () => rep [] cst)) end + +fun CFILTER pred ctac cst = + ctac cst + |> Seq.filter_results + |> Seq.filter pred + |> Seq.make_results + +(*Only accept next states where the subgoals have changed*) +fun CCHANGED ctac (cst as (_, st)) = + CFILTER (fn (_, st') => not (Thm.eq_thm (st, st'))) ctac cst + +local + fun op THEN (f, g) x = Seq.maps_results g (f x) + + fun INTERVAL f i j x = + if i > j then Seq.make_results (Seq.single x) + else op THEN (f j, INTERVAL f i (j - 1)) x + + (*By Peter Lammich: apply tactic to subgoals in interval in a forward manner, + skipping over emerging subgoals*) + fun INTERVAL_FWD ctac l u (cst as (_, st)) = + if l > u then all_ctac cst + else (ctac l CTHEN (fn cst' as (_, st') => + let val ofs = Thm.nprems_of st' - Thm.nprems_of st in + if ofs < ~1 + then raise THM ( + "INTERVAL_FWD: tactic solved more than one goal", ~1, [st, st']) + else INTERVAL_FWD ctac (l + 1 + ofs) (u + ofs) cst' + end)) cst +in + +fun (ctac1 CTHEN_ALL_NEW ctac2) i (cst as (_, st)) = + cst |> (ctac1 i CTHEN (fn cst' as (_, st') => + cst' |> INTERVAL ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st))) + +(*By Peter Lammich: apply ctac2 to all subgoals emerging from ctac1, in forward + manner*) +fun (ctac1 CTHEN_ALL_NEW_FWD ctac2) i (cst as (_, st)) = + cst |> (ctac1 i CTHEN (fn cst' as (_, st') => + cst' |> INTERVAL_FWD ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st))) + +end + +fun CREPEAT_ALL_NEW ctac = + ctac CTHEN_ALL_NEW (CTRY o (fn i => CREPEAT_ALL_NEW ctac i)) + +fun CREPEAT_ALL_NEW_FWD ctac = + ctac CTHEN_ALL_NEW_FWD (CTRY o (fn i => CREPEAT_ALL_NEW_FWD ctac i)) + +fun CHEADGOAL ctac = ctac 1 + +fun CALLGOALS ctac (cst as (_, st)) = + let + fun doall 0 = all_ctac + | doall n = ctac n CTHEN doall (n - 1); + in doall (Thm.nprems_of st) cst end + +end + +open Context_Tactical diff --git a/spartan/core/lib.ML b/spartan/core/lib.ML index 615f601..7b93a08 100644 --- a/spartan/core/lib.ML +++ b/spartan/core/lib.ML @@ -7,6 +7,7 @@ val maxint: int list -> int (*Terms*) val is_rigid: term -> bool +val no_vars: term -> bool val dest_eq: term -> term * term val mk_Var: string -> int -> typ -> term val lambda_var: term -> term -> term @@ -50,6 +51,8 @@ val maxint = max (op >) val is_rigid = not o is_Var o head_of +val no_vars = not o exists_subterm is_Var + fun dest_eq (Const (\<^const_name>\Pure.eq\, _) $ t $ def) = (t, def) | dest_eq _ = error "dest_eq" diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML index 0c71665..172ae90 100644 --- a/spartan/core/tactics.ML +++ b/spartan/core/tactics.ML @@ -64,13 +64,6 @@ fun typechk_tac ctxt = REPEAT_ALL_NEW (known_tac ctxt ORELSE' tac) end -fun typechk_context_tac (ctxt, st) = - let - - in - () - end - (*Many methods try to automatically discharge side conditions by typechecking. Switch this flag off to discharge by non-unifying assumption instead.*) val auto_typechk = Attrib.setup_config_bool \<^binding>\auto_typechk\ (K true) diff --git a/spartan/core/tactics2.ML b/spartan/core/tactics2.ML new file mode 100644 index 0000000..801424f --- /dev/null +++ b/spartan/core/tactics2.ML @@ -0,0 +1,191 @@ +(* Title: tactics.ML + Author: Joshua Chen + +General tactics for dependent type theory. +*) + +structure Tactics2: +sig + +val solve_side_conds: bool Config.T +val SIDE_CONDS: context_tactic' -> thm list -> context_tactic' +val rule_tac: thm list -> context_tactic' +val dest_tac: int option -> thm list -> context_tactic' +val intro_tac: context_tactic' +val intros_tac: context_tactic' +(* +val elim_context_tac: term list -> Proof.context -> int -> context_tactic +val cases_tac: term -> Proof.context -> int -> tactic +*) + +end = struct + +(*Automatically try to solve side conditions?*) +val solve_side_conds = + Attrib.setup_config_bool \<^binding>\solve_side_conds\ (K true) + +local + fun side_cond_ctac facts i (cst as (ctxt, _)) = + if Config.get ctxt solve_side_conds + then (Types.check_infer facts i) cst + else all_ctac cst +in + +(*Combinator runs tactic and tries to discharge newly arising side conditions*) +fun SIDE_CONDS ctac facts = ctac CTHEN_ALL_NEW (CTRY o side_cond_ctac facts) + +end + +local + fun mk_rules _ ths [] = ths + | mk_rules n ths ths' = + let val ths'' = foldr1 (op @) + (map + (fn th => [rotate_prems n (th RS @{thm PiE})] handle THM _ => []) + ths') + in + mk_rules n (ths @ ths') ths'' + end +in + +(*Resolves with given rules*) +fun rule_tac ths i (ctxt, st) = + TACTIC_CONTEXT ctxt (resolve_tac ctxt (mk_rules 0 [] ths) i st) + +(*Attempts destruct-resolution with the n-th premise of the given rules*) +fun dest_tac opt_n ths i (ctxt, st) = + TACTIC_CONTEXT ctxt (dresolve_tac ctxt + (mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths) + i st) + +end + +(*Applies some introduction rule*) +fun intro_tac i (ctxt, st) = + TACTIC_CONTEXT ctxt (resolve_tac ctxt + (Named_Theorems.get ctxt \<^named_theorems>\intros\) i st) + +val intros_tac = CONTEXT_SUBGOAL (fn (_, i) => + (CCHANGED o CREPEAT o CCHANGED o intro_tac) i) + +(* +(* Induction/elimination *) + +(*Pushes a context/goal premise typing t:T into a \-type*) +fun internalize_fact_tac t = + Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl = raw_concl, ...} => + let + val concl = Logic.strip_assums_concl (Thm.term_of raw_concl) + val C = Lib.type_of_typing concl + val B = Thm.cterm_of ctxt (Lib.lambda_var t C) + val a = Thm.cterm_of ctxt t + (*The resolvent is PiE[where ?B=B and ?a=a]*) + val resolvent = + 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 (known_tac ctxt) + end) + +(*Premises that have already been pushed into the \-type*) +structure Inserts = Proof_Data ( + type T = term Item_Net.T + val init = K (Item_Net.init Term.aconv_untyped single) +) + +local + +fun elim_core_tac tms types ctxt = SUBGOAL (K ( + let + val rule_insts = map ((Elim.lookup_rule ctxt) o Term.head_of) types + val rules = flat (map + (fn rule_inst => case rule_inst of + NONE => [] + | SOME (rl, idxnames) => [Drule.infer_instantiate ctxt + (idxnames ~~ map (Thm.cterm_of ctxt) tms) rl]) + rule_insts) + in + HEADGOAL (resolve_tac ctxt rules) + THEN RANGE (replicate (length tms) (typechk_tac ctxt)) 1 + end handle Option => no_tac)) + +in + +fun elim_context_tac tms ctxt = case tms of + [] => CONTEXT_SUBGOAL (K (Context_Tactic.CONTEXT_TACTIC (HEADGOAL ( + SIDE_CONDS' (eresolve_tac ctxt (map #1 (Elim.rules ctxt))) ctxt)))) + | major::_ => CONTEXT_SUBGOAL (fn (goal, _) => + let + val facts = Proof_Context.facts_of ctxt + val prems = Logic.strip_assums_hyp goal + val template = Lib.typing_of_term major + val types = + map (Thm.prop_of o #1) (Facts.could_unify facts template) + @ filter (fn prem => Term.could_unify (template, prem)) prems + |> map Lib.type_of_typing + in case types of + [] => Context_Tactic.CONTEXT_TACTIC no_tac + | _ => + let + val inserts = map (Thm.prop_of o fst) (Facts.props facts) @ prems + |> filter Lib.is_typing + |> map Lib.dest_typing + |> filter_out (fn (t, _) => + Term.aconv (t, major) orelse Item_Net.member (Inserts.get ctxt) t) + |> map (fn (t, T) => ((t, T), Lib.subterm_count_distinct tms T)) + |> filter (fn (_, i) => i > 0) + (*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm. + If they are incomparable, then order by decreasing + `subterm_count [p, x, y] T`*) + |> sort (fn (((t1, _), i), ((_, T2), j)) => + Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i))) + |> map (#1 o #1) + val record_inserts = Inserts.map (fold Item_Net.update inserts) + val tac = + (*Push premises having a subterm in `tms` into a \*) + fold (fn t => fn tac => + tac THEN HEADGOAL (internalize_fact_tac t ctxt)) + inserts all_tac + (*Apply elimination rule*) + THEN (HEADGOAL ( + elim_core_tac tms types ctxt + (*Pull pushed premises back out*) + THEN_ALL_NEW (SUBGOAL (fn (_, i) => + REPEAT_DETERM_N (length inserts) + (resolve_tac ctxt @{thms PiI} i))) + )) + (*Side conditions*) + THEN ALLGOALS (TRY o side_cond_tac ctxt) + in + fn (ctxt, st) => Context_Tactic.TACTIC_CONTEXT + (record_inserts ctxt) (tac st) + end + end) + +fun cases_tac tm ctxt = SUBGOAL (fn (goal, i) => + let + val facts = Proof_Context.facts_of ctxt + val prems = Logic.strip_assums_hyp goal + val template = Lib.typing_of_term tm + val types = + map (Thm.prop_of o #1) (Facts.could_unify facts template) + @ filter (fn prem => Term.could_unify (template, prem)) prems + |> map Lib.type_of_typing + val res = (case types of + [typ] => Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt tm)] + (the (Case.lookup_rule ctxt (Term.head_of typ))) + | [] => raise Option + | _ => raise error (Syntax.string_of_term ctxt tm ^ "not uniquely typed")) + handle Option => error ("no case rule known for " + ^ (Syntax.string_of_term ctxt tm)) + in + SIDE_CONDS' (resolve_tac ctxt [res]) ctxt i + end) + +end +*) + +end + +open Tactics2 diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML index 437a2dc..13ca440 100644 --- a/spartan/core/typechecking.ML +++ b/spartan/core/typechecking.ML @@ -1,7 +1,7 @@ (* Title: typechecking.ML Author: Joshua Chen -Type information and typechecking infrastructure. +Type information and type-checking infrastructure. *) structure Types: sig @@ -11,11 +11,12 @@ 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 check: Proof.context -> thm -> int -> tactic -val infer: Proof.context -> thm -> int -> tactic +val known_ctac: thm list -> int -> context_tactic +val check_infer: thm list -> int -> context_tactic end = struct + (* Context data *) structure Data = Generic_Data ( @@ -32,22 +33,60 @@ fun put_type typing = Context.proof_map (Data.map (Item_Net.update typing)) fun put_types typings = foldr1 (op o) (map put_type typings) -(* Checking and inference *) - -local +(* Context tactics for type-checking *) -fun checkable prop = Lib.is_typing prop - andalso not (exists_subterm is_Var (Lib.type_of_typing prop)) +(*For debugging*) +structure Probe = Proof_Data ( + type T = int + val init = K 0 +) +(*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 = facts + (*FIXME: Shouldn't pull nameless facts directly from context*) + @ map fst (Facts.props (Proof_Context.facts_of ctxt)) + in (resolve_tac ctxt ths i ORELSE assume_tac ctxt i) st end + else Seq.empty + end) + +(*Simple bidirectional typing tactic, with some nondeterminism from backtracking + search over arbitrary `typechk` rules. The current implementation does not + perform any normalization.*) +local + 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 (facts + (*MAYBE FIXME: Remove `typechk` from this list, and instead perform + definitional unfolding to (w?)hnf.*) + @(Named_Theorems.get ctxt \<^named_theorems>\typechk\) + @(Named_Theorems.get ctxt \<^named_theorems>\intros\) + @(map #1 (Elim.rules ctxt))) + in (resolve_from_net_tac ctxt net) i end + else no_tac) + val ctxt' = Probe.map (fn i => i + 1) ctxt + in + TACTIC_CONTEXT ctxt' (tac i st) + end in -fun check ctxt rule = Subgoal.FOCUS_PREMS ( - fn {context = goal_ctxt, prems, concl, ...} => no_tac) ctxt - -fun infer ctxt rule = Subgoal.FOCUS_PREMS ( - fn {context = goal_ctxt, prems, concl, ...} => no_tac) ctxt +fun check_infer facts = + let val probe = K (print_ctac (Int.toString o Probe.get)) + in + CREPEAT_ALL_NEW_FWD ( + probe CTHEN' known_ctac facts + CORELSE' probe CTHEN' check_infer_step facts) + end end - end -- cgit v1.2.3