1.1 --- a/TODO.md Mon Aug 22 11:26:20 2022 +0200
1.2 +++ b/TODO.md Mon Aug 22 13:39:32 2022 +0200
1.3 @@ -100,6 +100,7 @@
1.4 - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
1.5 - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
1.6
1.7 +* WN: eliminate argument theory from Interpret/*, e.g. (LI_Tool.tac_from_prog + see TODO.thy)
1.8 * WN: rename Pos.* -- Pos.ints, Pos.spec, Pos.empty, Pos.ints_empty
1.9
1.10 * WN: redesign transition from Specification to Solution: how relate
2.1 --- a/src/Tools/isac/Interpret/derive.sml Mon Aug 22 11:26:20 2022 +0200
2.2 +++ b/src/Tools/isac/Interpret/derive.sml Mon Aug 22 13:39:32 2022 +0200
2.3 @@ -121,8 +121,8 @@
2.4 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
2.5 | derivat dt = (#1 o #3 o last_elem) dt
2.6 fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
2.7 - val fod = do_one (**)ctxt(*HACK* )(Proof_Context.init_global (ThyC.Isac()))( *ctxt*) erls rules (snd rew_ord) NONE fo
2.8 - val ifod = do_one (**)ctxt(*HACK* )(Proof_Context.init_global (ThyC.Isac()))( *ctxt*) erls rules (snd rew_ord) NONE ifo
2.9 + val fod = do_one ctxt erls rules (snd rew_ord) NONE fo
2.10 + val ifod = do_one ctxt erls rules (snd rew_ord) NONE ifo
2.11 in
2.12 case (fod, ifod) of
2.13 ([], []) => if fo = ifo then (true, []) else (false, [])
3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Aug 22 11:26:20 2022 +0200
3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Aug 22 13:39:32 2022 +0200
3.3 @@ -636,14 +636,9 @@
3.4 let
3.5 val ptp as (pt, pos as (p, _)) = Specify.do_all ptp (*<--------------------*)
3.6 val mI = Ctree.get_obj Ctree.g_metID pt p
3.7 -(*ctxt*)val (ist, ctxt) = (Istate.empty, Ctree.get_ctxt pt pos)(*ctxt*)
3.8 + val (ist, ctxt) = (Istate.empty, Ctree.get_ctxt pt pos)
3.9 in
3.10 -(*ctxt* )
3.11 - by_tactic (Tactic.Apply_Method' (mI, NONE, empty, ContextC.empty))
3.12 - (empty, ContextC.empty) ptp
3.13 -( *ctxt*)
3.14 by_tactic (Tactic.Apply_Method' (mI, NONE, ist, ctxt)) (ist, ctxt) ptp
3.15 -(*ctxt*)
3.16 end
3.17 | _ => msg_cs';
3.18 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
4.1 --- a/src/Tools/isac/Interpret/solve-step.sml Mon Aug 22 11:26:20 2022 +0200
4.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Mon Aug 22 13:39:32 2022 +0200
4.3 @@ -150,53 +150,33 @@
4.4 | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, pos as (p, _))) =
4.5 let
4.6 val pp = Ctree.par_pblobj pt p;
4.7 -(*ctxt* )
4.8 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
4.9 - val thy = ThyC.get_theory thy';
4.10 - val ctxt = Proof_Context.init_global thy;
4.11 -( *ctxt*)
4.12 -val ctxt = Ctree.get_loc pt pos |> snd
4.13 -val thy = Proof_Context.theory_of ctxt
4.14 -val thy' = Context.theory_name thy
4.15 -(*ctxt*)
4.16 + val ctxt = Ctree.get_loc pt pos |> snd
4.17 + val thy = Proof_Context.theory_of ctxt
4.18 val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp);
4.19 val f = Calc.current_formula cs;
4.20 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
4.21 in
4.22 case Rewrite.rewrite_inst_ ctxt (assoc_rew_ord thy ro') erls false subst (snd thm) f of
4.23 SOME (f', asm) =>
4.24 - Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
4.25 + Applicable.Yes (Tactic.Rewrite_Inst'
4.26 + (Context.theory_name thy, ro', erls, false, subst, thm, f, (f', asm)))
4.27 | NONE => Applicable.No (fst thm ^ " not applicable")
4.28 end
4.29 - | check (Tactic.Rewrite_Set rls) (cs as (pt, pos as (p, _))) =
4.30 + | check (Tactic.Rewrite_Set rls) (cs as (pt, pos)) =
4.31 let
4.32 -(*ctxt* )
4.33 - val pp = Ctree.par_pblobj pt p;
4.34 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
4.35 -( *ctxt*)
4.36 -val ctxt = Ctree.get_loc pt pos |> snd
4.37 -val thy = Proof_Context.theory_of ctxt
4.38 -val thy' = Context.theory_name thy
4.39 -(*ctxt*)
4.40 + val ctxt = Ctree.get_loc pt pos |> snd
4.41 + val thy' = ctxt |> Proof_Context.theory_of |> Context.theory_name
4.42 val f = Calc.current_formula cs;
4.43 in
4.44 - case Rewrite.rewrite_set_ (ThyC.id_to_ctxt thy') false (assoc_rls rls) f of
4.45 + case Rewrite.rewrite_set_ ctxt false (assoc_rls rls) f of
4.46 SOME (f', asm)
4.47 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
4.48 | NONE => Applicable.No (rls ^ " not applicable")
4.49 end
4.50 - | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, pos as (p, _))) =
4.51 + | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, pos)) =
4.52 let
4.53 -(*ctxt* )
4.54 - val pp = Ctree.par_pblobj pt p;
4.55 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
4.56 - val thy = ThyC.get_theory thy';
4.57 - val ctxt = Proof_Context.init_global thy;
4.58 -( *ctxt*)
4.59 -val ctxt = Ctree.get_loc pt pos |> snd
4.60 -val thy = Proof_Context.theory_of ctxt
4.61 -val thy' = Context.theory_name thy
4.62 -(*ctxt*)
4.63 + val ctxt = Ctree.get_loc pt pos |> snd
4.64 + val thy' = ctxt |> Proof_Context.theory_of |> Context.theory_name
4.65 val f = Calc.current_formula cs;
4.66 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
4.67 in
4.68 @@ -211,23 +191,16 @@
4.69 | check (Tactic.Substitute sube) (cs as (pt, pos as (p, _))) =
4.70 let
4.71 val pp = Ctree.par_pblobj pt p
4.72 -(*ctxt* )
4.73 - val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
4.74 - val ctxt = Proof_Context.init_global thy;
4.75 -( *ctxt*)
4.76 -val ctxt = Ctree.get_loc pt pos |> snd
4.77 -val thy = Proof_Context.theory_of ctxt
4.78 -val thy' = Context.theory_name thy
4.79 -(*ctxt*)
4.80 + val ctxt = Ctree.get_loc pt pos |> snd
4.81 + val thy = Proof_Context.theory_of ctxt
4.82 val f = Calc.current_formula cs;
4.83 val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
4.84 - val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
4.85 - val subst = Subst.T_from_string_eqs thy sube
4.86 + val subte = Subst.input_to_terms sube (*?TODO: input requires parse _: _ -> _ option?*)
4.87 val ro = assoc_rew_ord thy rew_ord'
4.88 in
4.89 if foldl and_ (true, map TermC.contains_Var subte)
4.90 then (*1*)
4.91 - let val f' = subst_atomic subst f
4.92 + let val f' = subst_atomic (Subst.T_from_string_eqs thy sube) f
4.93 in if f = f'
4.94 then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
4.95 else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
4.96 @@ -237,17 +210,9 @@
4.97 SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
4.98 | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
4.99 end
4.100 - | check (Tactic.Tac id) (cs as (pt, pos as (p, _))) =
4.101 + | check (Tactic.Tac id) (cs as (pt, pos)) =
4.102 let
4.103 -(*ctxt* )
4.104 - val pp = Ctree.par_pblobj pt p;
4.105 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
4.106 - val thy = ThyC.get_theory thy';
4.107 -( *ctxt*)
4.108 -val ctxt = Ctree.get_loc pt pos |> snd
4.109 -val thy = Proof_Context.theory_of ctxt
4.110 -val thy' = Context.theory_name thy
4.111 -(*ctxt*)
4.112 + val thy = (Ctree.get_loc pt pos |> snd) |> Proof_Context.theory_of
4.113 val f = Calc.current_formula cs;
4.114 in
4.115 Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
5.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Mon Aug 22 11:26:20 2022 +0200
5.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Mon Aug 22 13:39:32 2022 +0200
5.3 @@ -48,35 +48,36 @@
5.4 then [get_obj g_tac pt p]
5.5 else
5.6 let
5.7 - val pp = par_pblobj pt p
5.8 -(*ctxt* )
5.9 - val thy' = get_obj g_domID pt pp
5.10 - val thy = ThyC.get_theory thy'
5.11 -( **)
5.12 -val ctxt = Ctree.get_loc pt pos |> snd
5.13 -val thy = Proof_Context.theory_of ctxt
5.14 -(**)
5.15 + val pp = par_pblobj pt p
5.16 + val ctxt = Ctree.get_loc pt pos |> snd
5.17 + val thy = Ctree.get_loc pt pos |> snd |> Proof_Context.theory_of
5.18 +
5.19 val metID = get_obj g_metID pt pp
5.20 val metID' =
5.21 if metID = MethodC.id_empty
5.22 - then (thd3 o snd3) (get_obj g_origin pt pp)
5.23 + then (get_obj g_origin pt pp) |> #2 |> #3
5.24 else metID
5.25 val (sc, srls, erls, ro) = (case MethodC.from_store metID' of
5.26 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
5.27 | _ => raise ERROR "specific_from_prog 1")
5.28 - val (env, (a, v)) = (case get_istate_LI pt (p, p_) of
5.29 + val (env, (a, v)) = (case get_istate_LI pt pos of
5.30 Istate.Pstate pst => (Istate.get_subst pst) | _ => error "specific_from_prog 2")
5.31 - val ctxt = get_ctxt pt (p, p_)
5.32 - val alltacs = (*we expect at least 1 Prog_Tac in a program*)
5.33 - map ((LItool.tac_from_prog pt thy) o Program.rep_stacexpr o #1 o
5.34 - (LItool.check_leaf "selrul" ctxt srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
5.35 + val alltacs = sc
5.36 + |> Auto_Prog.stacpbls
5.37 + |> map (fn tac_pbl => tac_pbl
5.38 + |> LItool.check_leaf "selrul" ctxt srls (env, (a, v))
5.39 + |> #1
5.40 + |> Program.rep_stacexpr
5.41 + |> LItool.tac_from_prog pt thy)
5.42 val f =
5.43 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
5.44 - | _ => raise ERROR "specific_from_prog 2")
5.45 + | _ => raise ERROR "specific_from_prog 3")
5.46 (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
5.47 in
5.48 - ((distinct Tactic.eq_tac) o flat o
5.49 - (map (Tactic.applicable (Proof_Context.init_global thy) ro erls f))) alltacs
5.50 + alltacs
5.51 + |> map (Tactic.applicable ctxt ro erls f)
5.52 + |> flat
5.53 + |> distinct Tactic.eq_tac
5.54 end;
5.55
5.56 (**)end(**)
5.57 \ No newline at end of file