1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Sat Dec 21 18:05:13 2019 +0100
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Mon Dec 23 11:12:24 2019 +0100
1.3 @@ -179,6 +179,9 @@
1.4 ("ok", c, ptp as (_,p)) =>
1.5 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.6 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.7 + | ("dummy", c, ptp as (_,p)) => (*prelim. until \<open>Review modelling- + specification-phase\<close>*)
1.8 + (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.9 + autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.10 | ("end-of-calculation", c, ptp as (_,p)) =>
1.11 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.12 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Dec 21 18:05:13 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 23 11:12:24 2019 +0100
2.3 @@ -30,8 +30,8 @@
2.4 find_next_tactic calls do_next and is called by by_tactic;
2.5 by_tactic and do_next are mutually recursive via by_tactic Apply_Method'
2.6 *)
2.7 - val by_tactic: Tactic.T -> Istate.T * Proof.context -> Ctree.state -> Chead.calcstate'
2.8 - val do_next: Ctree.state -> Chead.calcstate'
2.9 + val by_tactic: Tactic.T -> Istate.T * Proof.context -> Ctree.state -> string * Chead.calcstate'
2.10 + val do_next: Ctree.state -> string * Chead.calcstate'
2.11
2.12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.13 datatype expr_val1 =
2.14 @@ -524,14 +524,14 @@
2.15 val tac_ = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
2.16 val (pos, c, _, pt) = Generate.generate1 thy tac_ (is, ctxt) pos pt (* implicit Take *)
2.17 in
2.18 - ([(Tactic.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos))
2.19 + ("ok", ([(Tactic.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)))
2.20 end
2.21 | NONE =>
2.22 let
2.23 val pt = update_env pt (fst pos) (SOME (is, ctxt))
2.24 - val (tacis, c, ptp) = do_next (pt, pos)
2.25 - in (tacis @ [(Tactic.Apply_Method mI,
2.26 - Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt), (pos, (is, ctxt)))], c, ptp)
2.27 + val (_, (tacis, c, ptp)) = do_next (pt, pos)
2.28 + in ("ok", (tacis @ [(Tactic.Apply_Method mI,
2.29 + Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt), (pos, (is, ctxt)))], c, ptp))
2.30 end
2.31 end
2.32 | by_tactic (Tactic.Check_Postcond' (pI, (prog_res, _))) _ (pt, pos as (p, _)) =
2.33 @@ -550,7 +550,7 @@
2.34 val is = Istate.Pstate (ist |> the_pstate
2.35 |> Istate.set_act prog_res |> Istate.set_appy Istate.Skip_)
2.36 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac (is, ctxt) (pp, Res) pt;
2.37 - in ([(Tactic.Check_Postcond pI, tac, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_))) end
2.38 + in ("ok", ([(Tactic.Check_Postcond pI, tac, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_)))) end
2.39 else
2.40 let (*resume script of parent PblObj, transfer value of subpbl-script*)
2.41 val thy = Celem.assoc_thy (get_obj g_domID pt (par_pblobj pt (lev_up p)));
2.42 @@ -561,20 +561,20 @@
2.43 val ctxt'' = ContextC.from_subpbl_to_caller ctxt prog_res ctxt'
2.44 val is = Istate.Pstate (pst' |> Istate.set_act prog_res |> Istate.set_appy Istate.Skip_)
2.45 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac (is, ctxt'') (pp, Res) pt;
2.46 - in ([(Tactic.Check_Postcond pI, tac, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end
2.47 + in ("ok", ([(Tactic.Check_Postcond pI, tac, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_)))) end
2.48 end
2.49 - | by_tactic (Tactic.End_Proof'') _ ptp = ([], [], ptp)
2.50 + | by_tactic (Tactic.End_Proof'') _ ptp = ("end-of-calculation", ([], [], ptp))
2.51 | by_tactic tac_ is (pt, pos) =
2.52 let
2.53 val pos = next_in_prog' pos
2.54 val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac_ is pos pt;
2.55 in
2.56 - ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos'))
2.57 + ("ok", ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos')))
2.58 end
2.59 (*find_next_tactic from program, by_tactic will update Ctree*)
2.60 and do_next (ptp as (pt, pos as (p, p_))) =
2.61 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
2.62 - then ([], [], (pt, (p, p_)))
2.63 + then ("helpless", ([], [], (pt, (p, p_))))
2.64 else
2.65 let
2.66 val thy' = get_obj g_domID pt (par_pblobj pt p);
2.67 @@ -586,10 +586,11 @@
2.68 | End_Program (ist, tac) =>
2.69 (case tac of
2.70 Tactic.End_Detail' res =>
2.71 - ([(Tactic.End_Detail,
2.72 - Tactic.End_Detail' res, (pos, (ist, ctxt)))], [], ptp)
2.73 - | _ => by_tactic tac (ist, ctxt) ptp)
2.74 - | Helpless => Chead.e_calcstate'
2.75 + ("ok", ([(Tactic.End_Detail,
2.76 + Tactic.End_Detail' res, (pos, (ist, ctxt)))], [], ptp))
2.77 + | _ => by_tactic tac (ist, ctxt) ptp
2.78 + )
2.79 + | Helpless => ("helpless", Chead.e_calcstate')
2.80 end;
2.81
2.82 (*
2.83 @@ -623,8 +624,8 @@
2.84 then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
2.85 else
2.86 let
2.87 - val cs' as (tacis, c', ptp) = do_next ptp; (*<---------------------*)
2.88 - val (tacis, c'', ptp) = case tacis of
2.89 + val msg_cs' as (_, (tacis, c', ptp)) = do_next ptp; (*<---------------------*)
2.90 + val (_, (tacis, c'', ptp)) = case tacis of
2.91 ((Tactic.Subproblem _, _, _)::_) =>
2.92 let
2.93 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
2.94 @@ -632,7 +633,7 @@
2.95 in
2.96 by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) (Istate.e_istate, ContextC.e_ctxt) ptp
2.97 end
2.98 - | _ => cs';
2.99 + | _ => msg_cs';
2.100 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
2.101 end
2.102
3.1 --- a/src/Tools/isac/Interpret/step-solve.sml Sat Dec 21 18:05:13 2019 +0100
3.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Mon Dec 23 11:12:24 2019 +0100
3.3 @@ -6,7 +6,7 @@
3.4 signature STEP_SOLVE =
3.5 sig
3.6 val by_tactic : Tactic.T -> Ctree.state -> string * Chead.calcstate'
3.7 - val do_next: Ctree.state -> Chead.calcstate'
3.8 + val do_next: Ctree.state -> string * Chead.calcstate'
3.9
3.10 end
3.11
3.12 @@ -82,7 +82,7 @@
3.13 | LucinNEW.End_Program (_, Tactic.Check_Postcond' (_, (prog_res, _))) => prog_res
3.14 | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
3.15 in (*from Applicable.applicable_in not yet available -----vvvvvvvv*)
3.16 - ("ok", LucinNEW.by_tactic (Tactic.Check_Postcond' (pI, (prog_res, [(*fill.later*)])))
3.17 + (LucinNEW.by_tactic (Tactic.Check_Postcond' (pI, (prog_res, [(*fill.later*)])))
3.18 (Istate.e_istate, ContextC.e_ctxt) ptp)
3.19 end
3.20 | by_tactic (Tactic.End_Proof'') ptp = ("end-proof", ([], [], ptp))
4.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Sat Dec 21 18:05:13 2019 +0100
4.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 23 11:12:24 2019 +0100
4.3 @@ -32,7 +32,7 @@
4.4 datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
4.5 val loc_solve_ : Tactic.T -> Ctree.ctree * Ctree.pos' -> lOc_
4.6 val loc_specify_ : Tactic.T -> Ctree.state -> lOc_
4.7 - val nxt_specify_: Ctree.ctree * Ctree.pos' -> Chead.calcstate'
4.8 + val nxt_specify_: Ctree.ctree * Ctree.pos' -> string * Chead.calcstate'
4.9 val TESTg_form : Ctree.state -> Generate.mout
4.10 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.11
4.12 @@ -57,7 +57,6 @@
4.13 case f of (Generate.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
4.14 end
4.15
4.16 -(* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
4.17 fun loc_solve_ m (pt, pos) =
4.18 let
4.19 val (msg, cs') = Step_Solve.by_tactic m (pt, pos);
4.20 @@ -102,8 +101,8 @@
4.21 if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin
4.22 then
4.23 case mI' of
4.24 - ["no_met"] => Chead.nxt_specif (Tactic.Refine_Tacitly pI') (pt, (p, Pos.Pbl))
4.25 - | _ => Chead.nxt_specif Tactic.Model_Problem (pt, (p, Pos.Pbl))
4.26 + ["no_met"] => ("dummy", Chead.nxt_specif (Tactic.Refine_Tacitly pI') (pt, (p, Pos.Pbl)))
4.27 + | _ => ("dummy", Chead.nxt_specif Tactic.Model_Problem (pt, (p, Pos.Pbl)))
4.28 else
4.29 let
4.30 val cpI = if pI = Celem.e_pblID then pI' else pI;
4.31 @@ -118,8 +117,9 @@
4.32 in
4.33 case tac of
4.34 Tactic.Apply_Method mI =>
4.35 - LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp
4.36 - | _ => Chead.nxt_specif tac ptp
4.37 + LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt))
4.38 + ist_ctxt ptp
4.39 + | _ => ("dummy", Chead.nxt_specif tac ptp)
4.40 end
4.41 end
4.42
4.43 @@ -189,9 +189,9 @@
4.44 else (case (if member op = [Pos.Pbl, Pos.Met] p_
4.45 then nxt_specify_ (pt, ip) else LucinNEW.do_next (pt, ip))
4.46 handle ERROR msg => (writeln ("*** " ^ msg);
4.47 - ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
4.48 - cs as ([], _, _) => ("helpless", cs)
4.49 - | cs => ("ok", cs))
4.50 + ("e.g. Add_Given equality ///", ([], [], ptp))) of
4.51 + (_, cs as ([], _, _)) => ("helpless", cs)
4.52 + | cs => cs)
4.53 | _ => (case pIopt of
4.54 NONE => ("no-fmz-spec", ([], [], ptp))
4.55 | SOME _ => (*vvvvvv: Apply_Method without init_form*)
4.56 @@ -200,9 +200,9 @@
4.57 then nxt_specify_ (pt, ip)
4.58 else (Step_Solve.do_next (pt, ip))
4.59 handle ERROR msg => (writeln ("*** " ^ msg);
4.60 - ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
4.61 - cs as ([], _, _) => ("helpless", cs)
4.62 - | cs => ("ok", cs)))
4.63 + ("e.g. Add_Given equality ///", ([], [], ptp))) of
4.64 + (_, cs as ([], _, _)) => ("helpless", cs)
4.65 + | cs => cs))
4.66 end
4.67
4.68 (* does several steps within one calculation as given by "type auto";
4.69 @@ -393,16 +393,15 @@
4.70 | ("not-applicable",_) => (pt, p)
4.71 | ("end-of-calculation", (_, _, ptp)) => ptp
4.72 | ("failure", _) => error "sys-error"
4.73 - | _ => error "me: uncovered case"
4.74 + | _ => error "me: uncovered case locatetac"
4.75 val (_, ts) =
4.76 (*step's correct ctree is not tested in me, but in autocalc*)
4.77 (case do_next p ((pt, Pos.e_pos'), []) of
4.78 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
4.79 | ("helpless", _) => ("helpless: cannot propose tac", [])
4.80 - | ("no-fmz-spec", _) => error "no-fmz-spec"
4.81 + | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts) (*intermed.from specify*)
4.82 | ("end-of-calculation", (ts, _, _)) => ("", ts)
4.83 - | _ => error "me: uncovered case")
4.84 - handle ERROR msg => raise ERROR msg
4.85 + | _ => error "me: uncovered case do_next")
4.86 val tac =
4.87 case ts of
4.88 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
5.1 --- a/src/Tools/isac/MathEngine/solve.sml Sat Dec 21 18:05:13 2019 +0100
5.2 +++ b/src/Tools/isac/MathEngine/solve.sml Mon Dec 23 11:12:24 2019 +0100
5.3 @@ -67,8 +67,8 @@
5.4 val (_, c', ptp) = all_solve auto c ptp
5.5 in complete_solve auto (c @ c') ptp end
5.6 else
5.7 - case LucinNEW.do_next ptp of
5.8 - ((Tactic.Subproblem _, _, _) :: _, c', ptp') =>
5.9 + case Step_Solve.do_next ptp of
5.10 + (_, ((Tactic.Subproblem _, _, _) :: _, c', ptp')) =>
5.11 if autoord auto < 5
5.12 then ("ok", c @ c', ptp)
5.13 else
5.14 @@ -76,20 +76,20 @@
5.15 val ptp = Chead.all_modspec ptp'
5.16 val (_, c'', ptp) = all_solve auto (c @ c') ptp
5.17 in complete_solve auto (c @ c'@ c'') ptp end
5.18 - | ((Tactic.Check_Postcond _, _, _) :: _, c', ptp' as (_, p')) =>
5.19 + | (_, ((Tactic.Check_Postcond _, _, _) :: _, c', ptp' as (_, p'))) =>
5.20 if autoord auto < 6 orelse p' = ([], Res)
5.21 then ("ok", c @ c', ptp')
5.22 else complete_solve auto (c @ c') ptp'
5.23 - | ((Tactic.End_Detail, _, _) :: _, c', ptp') =>
5.24 + | (_, ((Tactic.End_Detail, _, _) :: _, c', ptp')) =>
5.25 if autoord auto < 6
5.26 then ("ok", c @ c', ptp')
5.27 else complete_solve auto (c @ c') ptp'
5.28 - | (_, c', ptp') => complete_solve auto (c @ c') ptp'
5.29 + | (_, (_, c', ptp')) => complete_solve auto (c @ c') ptp'
5.30 and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') =
5.31 let
5.32 val (_, _, mI) = get_obj g_spec pt p
5.33 val ctxt = get_ctxt pt pos
5.34 - val (_, c', ptp) = LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp
5.35 + val (_, (_, c', ptp)) = LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp
5.36 in
5.37 complete_solve auto (c @ c') ptp
5.38 end;
6.1 --- a/src/Tools/isac/Specify/calchead.sml Sat Dec 21 18:05:13 2019 +0100
6.2 +++ b/src/Tools/isac/Specify/calchead.sml Mon Dec 23 11:12:24 2019 +0100
6.3 @@ -365,7 +365,7 @@
6.4 (Pbl, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_)
6.5 | NONE =>
6.6 (case nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris pbt pbl of
6.7 - SOME (fd,ct') => (Pbl, mk_additem fd ct')
6.8 + SOME (fd, ct') => (Pbl, mk_additem fd ct')
6.9 | NONE => (*pbl-items complete*)
6.10 if not preok then (Pbl, Tactic.Refine_Problem pI')
6.11 else if dI = Rule.e_domID then (Pbl, Tactic.Specify_Theory dI')
7.1 --- a/src/Tools/isac/TODO.thy Sat Dec 21 18:05:13 2019 +0100
7.2 +++ b/src/Tools/isac/TODO.thy Mon Dec 23 11:12:24 2019 +0100
7.3 @@ -60,16 +60,6 @@
7.4 \item open Istate in LucinNEW
7.5 \end{itemize}
7.6 \<close>
7.7 -subsection \<open>Differences between code and paper\<close>
7.8 -text \<open>
7.9 - \begin{itemize}
7.10 - \item xxx
7.11 - \item xxx
7.12 - \item xxx
7.13 - \item xxx
7.14 - \item xxx
7.15 - \end{itemize}
7.16 -\<close>
7.17 subsection \<open>Postponed from current changeset\<close>
7.18 text \<open>
7.19 \begin{itemize}
7.20 @@ -77,24 +67,22 @@
7.21 \item re-organise code for Interpret
7.22 \begin{itemize}
7.23 \item Step*:
7.24 - datatype step_result = Step of Ctree.state | Step_Failed of msg (*TODO: exn hierarchy*)
7.25 - not other returns, because Step_Solve.add immediately after lucin, so all in Ctree.state.
7.26 \begin{itemize}
7.27 \item Step_Specify in Specify/step-specify.sml in analogy to Interpret/... TODO
7.28 \begin{itemize}
7.29 \item Step_Specify.check <-- Applicable.applicable_in
7.30 \item Step_Specify.add <-- Generate.generate1
7.31 \item Step_Specify.by_tactic : Tactic.input -> Ctree.state -> ...stay as is
7.32 - \item Step_Specify.by_formula: ?term? -> Ctree.state -> .............
7.33 - \item Step_Specify.do_next : Ctree.state -> ...
7.34 + \item Step_Specify.by_formula: ?term? -> Ctree.state -> ...stay as is
7.35 + \item Step_Specify.do_next : Ctree.state -> ...stay as is
7.36 \end{itemize}
7.37 \item Step_Solve in Interpret/step-solve.sml
7.38 \begin{itemize}
7.39 \item Step_Solve.check <-- Applicable.applicable_in
7.40 inserts all data into Tactic.T available -- not all are at time of call!
7.41 \item Step_Solve.add <-- Generate.generate1
7.42 - \item Step_Solve.by_formula : term -> Ctree.state -> ...
7.43 - \item Step_Solve.do_next : Ctree.state -> ...
7.44 + \item Step_Solve.by_formula : term -> Ctree.state -> ...stay as is
7.45 + \item Step_Solve.do_next : Ctree.state -> ...stay as is
7.46 ^^^^LucinNEW.do_next
7.47 \end{itemize}
7.48 \item Step in MathEngine/step.sml
7.49 @@ -108,18 +96,10 @@
7.50 \end{itemize}
7.51 \item NOTE on mut.rec: Step.do_next calls Step_Solve.do_next + Step_Specify.do_next
7.52 ^ Math_Engine.nxt_specify_
7.53 - so special efforts are required:
7.54 - https://en.wikipedia.org/wiki/Mutual_recursion#Conversion_to_direct_recursion
7.55 + so some restructuring is required.
7.56 INTERMEDIATE STEP: Step.do_next is still Math_Engine.do_next
7.57 \end{itemize}
7.58 \item xxx
7.59 - \item MathEngBasic/calculation.sml
7.60 - \begin{itemize}
7.61 - \item rename Calc --> Calc_
7.62 - \item ? type Calc.T = CTree.state ?
7.63 - \item Calc.add_step <-- ???_Specify.add + ???_Solve.add <-- Generate.generate*
7.64 - \item xxx
7.65 - \end{itemize}
7.66 \item xxx
7.67 \end{itemize}
7.68 \item xxx
7.69 @@ -138,18 +118,12 @@
7.70 \item xxx
7.71 \item NEW structures
7.72 \begin{itemize}
7.73 - \item Step
7.74 + \item MathEngBasic/calculation.sml ??("Calc" is occupied ?!?) ? rename Calc --> Calc_
7.75 \begin{itemize}
7.76 - \item Applicable.applicable_in --> Step.applicable
7.77 - \item Generate.generate1 --> Step.add ?-->? Calculation.add_step
7.78 + \item rename existing Calc --> Calc_
7.79 + \item ? type Calc.T = CTree.state ?
7.80 \item xxx
7.81 - \end{itemize}
7.82 - \item Calculation ("Calc" is occupied ?!?) ?^^^? Calculation
7.83 - \begin{itemize}
7.84 - \item Ctree.state ?-->? Calculation.T
7.85 - \item Chead.calcstate --> Calculation.prestate
7.86 - \item Chead.calcstate' --> Calculation.poststate
7.87 - \item e_calcstate, e_calcstate' -"-
7.88 + \item xxx
7.89 \item xxx
7.90 \end{itemize}
7.91 \end{itemize}
7.92 @@ -184,13 +158,6 @@
7.93 \item xxx
7.94 \item complete mstools.sml (* survey on handling contexts:
7.95 \item xxx
7.96 - \item dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) FORALL occur.
7.97 - \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper
7.98 - \item xxx
7.99 - \item check in states: length ?? > 1 with tracing these cases
7.100 - \item xxx
7.101 - \item xxx
7.102 - \item Lucin.Ass_Weak etc \<longrightarrow> NEW structutre ? LItool ?
7.103 \item xxx
7.104 \item istate
7.105 \begin{itemize}
7.106 @@ -408,11 +375,20 @@
7.107 \<close>
7.108 subsection \<open>taci list, type step\<close>
7.109 text \<open>
7.110 +taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,
7.111 +and probably, because the Kernel interface separated setNextTactic and applyTactic.
7.112 +Both are no good reasons to make code more complicated. For instance Math_Engine.do_next
7.113 +could drop half of the code. So try to use Ctree.state only.
7.114 \begin{itemize}
7.115 + \item xxx
7.116 + \item Step* functions should return Ctree.state instead of Chead.calcstate'
7.117 + \item xxx
7.118 \item states.sml: check, when "length tacis > 1"
7.119 \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
7.120 \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
7.121 \item xxx
7.122 + \item brute force setting all empty ([], [], ptp) but ptp causes errors -- investigate!
7.123 + \item xxx
7.124 \end{itemize}
7.125 \<close>
7.126 subsection \<open>Ctree\<close>
8.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Sat Dec 21 18:05:13 2019 +0100
8.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 23 11:12:24 2019 +0100
8.3 @@ -220,24 +220,6 @@
8.4 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
8.5 Iterator 1;
8.6 moveActiveRoot 1;
8.7 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
8.8 -modeling is skipped FIXME
8.9 -see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
8.10 - setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
8.11 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); (*equality added*);
8.12 -
8.13 - fetchProposedTactic 1;
8.14 - setNextTactic 1 (Add_Given "solveFor x");
8.15 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
8.16 -
8.17 - fetchProposedTactic 1;
8.18 - setNextTactic 1 (Add_Find "solutions L");
8.19 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
8.20 -
8.21 - fetchProposedTactic 1;
8.22 - setNextTactic 1 (Specify_Theory "Test");
8.23 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
8.24 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
8.25 autoCalculate 1 (Steps 1);
8.26 "----- step 1 ---";
8.27 autoCalculate 1 (Steps 1);
8.28 @@ -287,25 +269,25 @@
8.29 (auto, c, ptp);
8.30 val (_,_,mI) = get_obj g_spec pt p
8.31 val ctxt = get_ctxt pt pos
8.32 - val (ttt, c', ptp) = LucinNEW.by_tactic (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
8.33 + val (_, (ttt, c', ptp)) = LucinNEW.by_tactic (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
8.34 (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
8.35 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
8.36 (auto, (c @ c'), ptp);
8.37 p = ([], Res) (*false p = ([1], Frm)*);
8.38 member op = [Pbl,Met] p_ (*false*);
8.39 -val (ttt, c', ptp') = Step_Solve.do_next ptp; (*ttt = Rewrite_Set "norm_equation"*)
8.40 +val (_, (ttt, c', ptp')) = Step_Solve.do_next ptp; (*ttt = Rewrite_Set "norm_equation"*)
8.41 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
8.42 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
8.43 (auto, (c @ c'), ptp');
8.44 p = ([], Res) (*false p = ([1], Res)*);
8.45 member op = [Pbl,Met] p_ (*false*);
8.46 -val (ttt, c', ptp') = Step_Solve.do_next ptp; (*ttt = Rewrite_Set "Test_simplify"*)
8.47 +val (_, (ttt, c', ptp')) = Step_Solve.do_next ptp; (*ttt = Rewrite_Set "Test_simplify"*)
8.48 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
8.49 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
8.50 (auto, (c @ c'), ptp');
8.51 p = ([], Res) (*false p = ([2], Res)*);
8.52 member op = [Pbl,Met] p_ (*false*);
8.53 -val ((Subproblem _, tac_, (_, is)) ::_, c', ptp') = Step_Solve.do_next ptp;
8.54 +val (_, ((Subproblem _, tac_, (_, is)) ::_, c', ptp')) = Step_Solve.do_next ptp;
8.55 autoord auto < 5 (*false*);
8.56 (* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
8.57 "~~~~~ fun all_modspec , args:"; val (pt, pos as (p,_)) = (ptp');
8.58 @@ -480,7 +462,7 @@
8.59 (CompleteSubpbl, [], (pt',pos'));
8.60 p = ([], Res) = false;
8.61 member op = [Pbl,Met] p_ = false;
8.62 -val (_, c', ptp') = Step_Solve.do_next ptp;
8.63 +val (_, (_, c', ptp')) = Step_Solve.do_next ptp;
8.64 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
8.65 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
8.66 "~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
9.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Sat Dec 21 18:05:13 2019 +0100
9.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Dec 23 11:12:24 2019 +0100
9.3 @@ -26,7 +26,7 @@
9.4 (*if*) member op = [Pos.Pbl, Pos.Met] p_
9.5 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*then*);
9.6
9.7 -(*+*)val ([_], _, (pt''''', p''''')) =
9.8 +(*+*)val (_, ([_], _, (pt''''', p'''''))) =
9.9 nxt_specify_ (pt, ip);
9.10 "~~~~~ fun nxt_specify_ , args:"; val ((ptp as (pt, (p, p_)))) = (pt, ip);
9.11 val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
9.12 @@ -46,7 +46,7 @@
9.13 val ist_ctxt = get_loc pt (p, p_)
9.14
9.15 val Apply_Method mI = (*case*) tac (*of*);
9.16 -(*+*)val (_, _, (pt'''', p'''')) =
9.17 +(*+*)val (_, (_, _, (pt'''', p''''))) =
9.18 LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp;
9.19 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
9.20 = ((Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)), ist_ctxt, ptp);
10.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Sat Dec 21 18:05:13 2019 +0100
10.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Dec 23 11:12:24 2019 +0100
10.3 @@ -101,7 +101,7 @@
10.4 = (CompleteSubpbl, [], (pt', pos'));
10.5 (*if*) p = ([], Res) (*else*);
10.6 (*if*) member op = [Pbl,Met] p_ (*else*);
10.7 - val ([(Rewrite ("radd_commute", _), _, _)], c', ptp') = (*case*)Step_Solve.do_next ptp (*of*);
10.8 + val (_, ([(Rewrite ("radd_commute", _), _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
10.9
10.10 (*+*)c' = [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)];
10.11 (*+*)show_pt (fst ptp');(*[
10.12 @@ -118,12 +118,12 @@
10.13 (*if*) p = ([], Res) (*else*);
10.14 (*if*) member op = [Pbl,Met] p_ (*else*);
10.15
10.16 - val ([(Rewrite ("add_assoc", _), _, _)], c', ptp') = (*case*)Step_Solve.do_next ptp (*of*);
10.17 + val (_, ([(Rewrite ("add_assoc", _), _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
10.18 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
10.19 = (auto, (c @ c'), ptp');
10.20 (*if*) p = ([], Res) (*else*);
10.21 (*if*) member op = [Pbl,Met] p_ (*else*);
10.22 - val ([(Calculate "TIMES", _, _)], c', ptp') = (*case*)Step_Solve.do_next ptp (*of*);
10.23 + val (_, ([(Calculate "TIMES", _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
10.24
10.25 show_pt (fst ptp'); (* added [2,1]..[2,3], more to come *)
10.26 (*\\-------------------------- 1. go down along calls to error ------------------------------//*)
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/test/Tools/isac/Specify/step-specify.sml Mon Dec 23 11:12:24 2019 +0100
11.3 @@ -0,0 +1,123 @@
11.4 +(* Title: "Specify/step-specify.sml"
11.5 + Author: Walther Neuper
11.6 + (c) due to copyright terms
11.7 +*)
11.8 +
11.9 +"-----------------------------------------------------------------------------------------------";
11.10 +"table of contents -----------------------------------------------------------------------------";
11.11 +"-----------------------------------------------------------------------------------------------";
11.12 +"-----------------------------------------------------------------------------------------------";
11.13 +"----------- re-build: Step_Specify.do_next ---------------------------------------------------";
11.14 +"-----------------------------------------------------------------------------------------------";
11.15 +"-----------------------------------------------------------------------------------------------";
11.16 +"-----------------------------------------------------------------------------------------------";
11.17 +
11.18 +"----------- re-build: Step_Specify.do_next ---------------------------------------------------";
11.19 +"----------- re-build: Step_Specify.do_next ---------------------------------------------------";
11.20 +"----------- re-build: Step_Specify.do_next ---------------------------------------------------";
11.21 +reset_states ();
11.22 +CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
11.23 + [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
11.24 + ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
11.25 +Iterator 1;
11.26 +moveActiveRoot 1;
11.27 +autoCalculate 1 (Steps 1);
11.28 +
11.29 +val (ptp as (pt, p), _) = get_calc 1;
11.30 +pt;(*isa==REP*)
11.31 +val (_, ("Integrate", ["integrate", "function"], ["diff", "integration"]), _)
11.32 + = get_obj g_origin pt (fst p);
11.33 +get_obj g_spec pt (fst p) = ("e_domID", ["e_pblID"], ["e_metID"]); (*isa==REP*)
11.34 +
11.35 +(*this steps into according to "----- step 2 ---" below*)
11.36 +"~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
11.37 + val pold = get_pos cI 1
11.38 +;
11.39 + (*case*) Math_Engine.autocalc [] pold (get_calc cI) auto (*of*);
11.40 +"~~~~~ fun autocalc , args:"; val (c: pos' list, ip, cs, (Solve.Steps s)) = ([], pold, (get_calc cI), auto);
11.41 +val c''''' = c; (*for from fun nxt_specify_\<longrightarrow>fun Math_Engine.do_next\<longrightarrow>fun autocalc, return*)
11.42 +
11.43 + (*if*) s <= 1 (*then*);
11.44 + (**)val ("dummy", (([(Specify_Theory "Integrate", _, _)]), c', ptp)) =(**)
11.45 +Math_Engine.do_next ip cs;
11.46 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs);
11.47 + val pIopt = Ctree.get_pblID (pt, ip);
11.48 + (*if*) ip = ([], Pos.Res) (*else*);
11.49 + val [] = (*case*) tacis (*of*);
11.50 + val SOME _ = (*case*) pIopt (*of*);
11.51 + (*if*) member op = [Pos.Pbl, Pos.Met] p_
11.52 + andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*then*);
11.53 +
11.54 + val ("dummy", ([(Specify_Theory "Integrate", _, _)], _, _)) =
11.55 + nxt_specify_ (pt, ip);
11.56 +"~~~~~ fun nxt_specify_ , args:"; val ((ptp as (pt, (p, p_)))) = (pt, ip);
11.57 + val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
11.58 +(*isa<>REP ^^*)
11.59 + case Ctree.get_obj I pt p of
11.60 + pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
11.61 + probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
11.62 + | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj";
11.63 + (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
11.64 + val cpI = if pI = Celem.e_pblID then pI' else pI;
11.65 + val cmI = if mI = Celem.e_metID then mI' else mI;
11.66 + val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
11.67 + val pre = Stool.check_preconds "thy 100820" prls where_ probl;
11.68 + val pb = foldl and_ (true, map fst pre);
11.69 +
11.70 + val (Pbl, Specify_Theory "Integrate") =
11.71 + Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI);
11.72 +"~~~~~ fun nxt_spec , args:"; val (Pbl, preok, oris, (dI', pI', mI'), (pbl, met), (pbt, mpc), (dI, pI, mI))
11.73 +(* vv----^^*)
11.74 + = (p_, pb, oris, (dI', pI', mI'), (probl, meth), (ppc, (#ppc o Specify.get_met) cmI), (dI, pI, mI));
11.75 + (*if*) dI' = Rule.e_domID andalso dI = Rule.e_domID (*else*);
11.76 + (*if*) pI' = Celem.e_pblID andalso pI = Celem.e_pblID (*else*);
11.77 + val NONE = (*case*) find_first (is_error o #5) pbl (*of*);
11.78 + val NONE = (*case*) nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris pbt pbl (*of*);
11.79 + (*if*) not preok (*else*);
11.80 + (*if*) dI = Rule.e_domID (*then*);
11.81 +
11.82 + (Pbl, Tactic.Specify_Theory dI') (*return from nxt_spec*);
11.83 +"~~~~~ from fun nxt_spec\<longrightarrow>fun nxt_specify_, return:"; val (_, tac)
11.84 + = (Pbl, Tactic.Specify_Theory dI');
11.85 + val _ = (*case*) tac (*of*);
11.86 +
11.87 + ("dummy", Chead.nxt_specif tac ptp) (*return from nxt_specify_*);
11.88 +"~~~~~ from fun nxt_specify_\<longrightarrow>fun Math_Engine.do_next\<longrightarrow>fun autocalc, return:"; val (str, (_, c', ptp))
11.89 + = ("dummy", Chead.nxt_specif tac ptp);
11.90 +
11.91 + (str, c''''' @ c', ptp) (*return from autocalc*);
11.92 +
11.93 +"----- step 2 ---";(*isa<>REP*)
11.94 +autoCalculate 1 (Steps 1);
11.95 +
11.96 +val (ptp as (pt, p), _) = get_calc 1;
11.97 +pt;(*REP
11.98 +val it =
11.99 + Nd (PblObj
11.100 +:
11.101 + result = (Const ("empty", "??.'a"), []), spec =
11.102 + ("Integrate", ["integrate", "function"], ["e_metID"])},
11.103 + []):
11.104 + ctree*)
11.105 +
11.106 +"----- step 3 ---";
11.107 +autoCalculate 1 (Steps 1);
11.108 +val (ptp as (pt, p), _) = get_calc 1;
11.109 +
11.110 +"----- step 4 ---";
11.111 +autoCalculate 1 (Steps 1);
11.112 +"----- step 5 ---";
11.113 +autoCalculate 1 (Steps 1);
11.114 +"----- step 6 ---";
11.115 +autoCalculate 1 (Steps 1);
11.116 +"----- step 7 ---";
11.117 +autoCalculate 1 (Steps 1);
11.118 +"----- step 8 ---";
11.119 +autoCalculate 1 (Steps 1);
11.120 +
11.121 +val (ptp as (_, p), _) = get_calc 1;
11.122 +
11.123 +val (Form t,_,_) = pt_extract ptp;
11.124 +
11.125 +if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
11.126 +else error "mathengine.sml -- fun autoCalculate -- end";