1.1 --- a/TODO.md Sat Aug 06 19:05:33 2022 +0200
1.2 +++ b/TODO.md Tue Aug 16 12:21:21 2022 +0200
1.3 @@ -55,9 +55,6 @@
1.4 ***** priority of WN items is top down, most urgent/simple on top
1.5
1.6 * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
1.7 - - Fetch_Tacs.specific_from_prog ?
1.8 - - Eval.adhoc_thm, adhoc_thm1_
1.9 - - ? LIST IS NOT COMPLETE
1.10 - Solve_Step.check ..Rewrite_Inst, Substitute, etc: push ctxt through Interpret/*
1.11 a step in a calculation
1.12 initialises ctxt from specified thy -> pushes ctxt through whole calculation
1.13 @@ -66,7 +63,7 @@
1.14 val thy = ThyC.get_theory thy'; -> val thy = Proof_Context.theory_of ctxt
1.15 val ctxt = Proof_Context.init_global thy; -> val thy' = Context.theory_name thy
1.16 cp code to test/*
1.17 - - Derive.steps: note HACK
1.18 + - Derive.steps: note HACK, new code still outcommented
1.19
1.20 * WN: eliminate SPARK; as an example replaced by Outer_Syntax.command..problem
1.21
2.1 --- a/src/Tools/isac/Interpret/derive.sml Sat Aug 06 19:05:33 2022 +0200
2.2 +++ b/src/Tools/isac/Interpret/derive.sml Tue Aug 16 12:21:21 2022 +0200
2.3 @@ -139,7 +139,7 @@
2.4 (** embed a derivation into the Ctree **)
2.5
2.6 fun embed tacis (pt, pos as (p, Pos.Frm)) =
2.7 - (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
2.8 + (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj
2.9 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
2.10 let
2.11 val (res, asm) = (State_Steps.result o last_elem) tacis
2.12 @@ -157,7 +157,7 @@
2.13 val pt = Ctree.update_branch pt p Ctree.TransitiveB
2.14 in (c, (pt, pos)) end
2.15 | embed tacis (pt, (p, Pos.Res)) =
2.16 - (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
2.17 + (*inform at Res: append a Transitive-PrfObj
2.18 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
2.19 let
2.20 val (res, asm) = (State_Steps.result o last_elem) tacis
3.1 --- a/src/Tools/isac/Interpret/solve-step.sml Sat Aug 06 19:05:33 2022 +0200
3.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Tue Aug 16 12:21:21 2022 +0200
3.3 @@ -147,12 +147,18 @@
3.4 | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable")
3.5 else Applicable.No msg
3.6 end
3.7 - | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) =
3.8 + | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, pos as (p, _))) =
3.9 let
3.10 val pp = Ctree.par_pblobj pt p;
3.11 +(*ctxt*)
3.12 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.13 val thy = ThyC.get_theory thy';
3.14 val ctxt = Proof_Context.init_global thy;
3.15 +(*ctxt* )
3.16 +val ctxt = Ctree.get_loc pt pos |> snd
3.17 +val thy = Proof_Context.theory_of ctxt
3.18 +val thy' = Context.theory_name thy
3.19 +( *ctxt*)
3.20 val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp);
3.21 val f = Calc.current_formula cs;
3.22 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
3.23 @@ -162,10 +168,16 @@
3.24 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
3.25 | NONE => Applicable.No (fst thm ^ " not applicable")
3.26 end
3.27 - | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =
3.28 + | check (Tactic.Rewrite_Set rls) (cs as (pt, pos as (p, _))) =
3.29 let
3.30 +(*ctxt*)
3.31 val pp = Ctree.par_pblobj pt p;
3.32 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.33 +(*ctxt* )
3.34 +val ctxt = Ctree.get_loc pt pos |> snd
3.35 +val thy = Proof_Context.theory_of ctxt
3.36 +val thy' = Context.theory_name thy
3.37 +( *ctxt*)
3.38 val f = Calc.current_formula cs;
3.39 in
3.40 case Rewrite.rewrite_set_ (ThyC.id_to_ctxt thy') false (assoc_rls rls) f of
3.41 @@ -173,12 +185,18 @@
3.42 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
3.43 | NONE => Applicable.No (rls ^ " not applicable")
3.44 end
3.45 - | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, _))) =
3.46 + | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, pos as (p, _))) =
3.47 let
3.48 +(*ctxt*)
3.49 val pp = Ctree.par_pblobj pt p;
3.50 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.51 val thy = ThyC.get_theory thy';
3.52 val ctxt = Proof_Context.init_global thy;
3.53 +(*ctxt* )
3.54 +val ctxt = Ctree.get_loc pt pos |> snd
3.55 +val thy = Proof_Context.theory_of ctxt
3.56 +val thy' = Context.theory_name thy
3.57 +( *ctxt*)
3.58 val f = Calc.current_formula cs;
3.59 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
3.60 in
3.61 @@ -190,11 +208,17 @@
3.62 | check (Tactic.Subproblem (domID, pblID)) (_, _) =
3.63 Applicable.Yes (Tactic.Subproblem' ((domID, pblID, MethodC.id_empty), [],
3.64 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
3.65 - | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
3.66 + | check (Tactic.Substitute sube) (cs as (pt, pos as (p, _))) =
3.67 let
3.68 val pp = Ctree.par_pblobj pt p
3.69 +(*ctxt*)
3.70 val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
3.71 val ctxt = Proof_Context.init_global thy;
3.72 +(*ctxt* )
3.73 +val ctxt = Ctree.get_loc pt pos |> snd
3.74 +val thy = Proof_Context.theory_of ctxt
3.75 +val thy' = Context.theory_name thy
3.76 +( *ctxt*)
3.77 val f = Calc.current_formula cs;
3.78 val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
3.79 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
3.80 @@ -215,9 +239,15 @@
3.81 end
3.82 | check (Tactic.Tac id) (cs as (pt, (p, _))) =
3.83 let
3.84 +(*ctxt*)
3.85 val pp = Ctree.par_pblobj pt p;
3.86 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.87 val thy = ThyC.get_theory thy';
3.88 +(*ctxt* )
3.89 +val ctxt = Ctree.get_loc pt pos |> snd
3.90 +val thy = Proof_Context.theory_of ctxt
3.91 +val thy' = Context.theory_name thy
3.92 +( *ctxt*)
3.93 val f = Calc.current_formula cs;
3.94 in
3.95 Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))