1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 19 12:40:17 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 19 16:41:57 2019 +0100
1.3 @@ -18,15 +18,18 @@
1.4 val find_next_tactic: Rule.program -> Ctree.state -> Istate.T -> Proof.context
1.5 -> next_tactic_result
1.6
1.7 -(*datatype input_formula_result = FStep of calcstate' | Not_Derivable *)
1.8 +(*TODO input_formula_result = Found_Step of Ctree.state | Not_Derivable *)
1.9 datatype input_formula_result =
1.10 Found_Step of Ctree.state * Istate.T * Proof.context
1.11 | Not_Derivable of Chead.calcstate'
1.12 -(*val locate_input_formula: Ctree.state -> term -> input_formula_result *)
1.13 +(*TODOlocate_input_formula: Ctree.state -> term -> input_formula_result *)
1.14 val locate_input_formula: Rule.program -> Ctree.state -> Istate.T -> Proof.context -> term
1.15 -> input_formula_result
1.16 -
1.17 - (*TODO vvv \<longrightarrow> Sove_Step.begin_end_prog, Sove_Step.do ?TODO? is mut.rec. necessary?*)
1.18 +
1.19 + (* must reside here:
1.20 + find_next_tactic calls do_solve_step and is called by begin_end_prog;
1.21 + begin_end_prog and do_solve_step are mutually recursive via begin_end_prog Apply_Method'
1.22 + *)
1.23 val begin_end_prog: Tactic.T -> Istate.T * Proof.context -> Ctree.state -> Chead.calcstate'
1.24 val do_solve_step: Ctree.state -> Chead.calcstate'
1.25
1.26 @@ -529,14 +532,6 @@
1.27 let
1.28 val pt = update_env pt (fst pos) (SOME (is, ctxt))
1.29 val (tacis, c, ptp) = do_solve_step (pt, pos)
1.30 -(*
1.31 -val _ = (tracing ("=========================== begin_end_prog Apply_Method' rec.call do_solve_step\n"
1.32 -^ "at " ^ pos'2str pos ^ " called Apply_Method'= " ^ strs2str' mI ^ "\n"
1.33 -^ "with NONE ini calls do_solve_step, which returns tacis=\n"
1.34 -^ Generate.tacis2str tacis ^ "\n"
1.35 -^ "-------------------------------------------------------------------------------------\n);
1.36 -raise ERROR "begin_end_prog Apply_Method' rec.call do_solve_step")
1.37 -*)
1.38 in (tacis @ [(Tactic.Apply_Method mI,
1.39 Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt), (pos, (is, ctxt)))], c, ptp)
1.40 end
2.1 --- a/src/Tools/isac/Interpret/step-solve.sml Thu Dec 19 12:40:17 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Thu Dec 19 16:41:57 2019 +0100
2.3 @@ -5,6 +5,7 @@
2.4
2.5 signature STEP_SOLVE =
2.6 sig
2.7 + val solve : Tactic.T -> Ctree.state -> string * Chead.calcstate'
2.8
2.9 end
2.10
2.11 @@ -12,5 +13,142 @@
2.12 structure Step_Solve(**): STEP_SOLVE(**) =
2.13 struct
2.14 (**)
2.15 +open Ctree;
2.16 +open Pos
2.17 +
2.18 +(*FIXME.WN050821 compare solve ... begin_end_prog:
2.19 + WN190811: solve ("Apply_Method",.. used by root-pbl + by locate_input_tactic !!!
2.20 +*)
2.21 +fun solve (m as Tactic.Apply_Method' (mI, _, _, ctxt)) (pt, (pos as (p, _))) =
2.22 + let
2.23 + val itms = case get_obj I pt p of
2.24 + PblObj {meth=itms, ...} => itms
2.25 + | _ => error "solve Apply_Method: uncovered case get_obj"
2.26 + val thy' = get_obj g_domID pt p;
2.27 + val thy = Celem.assoc_thy thy';
2.28 + val srls = Lucin.get_simplifier (pt, pos)
2.29 + val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
2.30 + (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
2.31 + | _ => error "solve Apply_Method: uncovered case init_pstate"
2.32 + val ini = Lucin.init_form thy sc env;
2.33 + val p = lev_dn p;
2.34 + in
2.35 + case ini of
2.36 + SOME t =>
2.37 + let val (pos,c,_, pt) =
2.38 + Generate.generate1 thy (Tactic.Apply_Method' (mI, SOME t, is, ctxt))
2.39 + (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
2.40 + in ("ok",([(Tactic.Apply_Method mI, Tactic.Apply_Method' (mI, SOME t, is, ctxt),
2.41 + ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)))
2.42 + end
2.43 + | NONE =>
2.44 + let
2.45 + val (m', is', ctxt') =
2.46 + case LucinNEW.find_next_tactic sc (pt, (p, Res)) is ctxt of
2.47 + LucinNEW.Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
2.48 + | _ => raise ERROR ("solve Apply_Method " ^ strs2str' mI)
2.49 + in
2.50 + case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of
2.51 + LucinNEW.Safe_Step (istate, ctxt, tac) =>
2.52 + let
2.53 + val (p'', _, _,pt') =
2.54 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
2.55 + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
2.56 + (istate, ctxt) (lev_on p, Pbl) pt;
2.57 + in
2.58 + ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
2.59 + [(*ctree NOT cut*)], (pt', p'')))
2.60 + end
2.61 + | _ => (* NotLocatable, but applicable_in from the beginning *)
2.62 + let
2.63 + val (p, ps, _, pt) =
2.64 + Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, Frm) pt;
2.65 + in
2.66 + ("not-found-in-script",([(Tactic.input_from_T m, m, (pos, (is, ctxt)))], ps, (pt, p)))
2.67 + end
2.68 + end
2.69 + end
2.70 + | solve (Tactic.Free_Solve') (pt, po as (p, _)) =
2.71 + let
2.72 + val p' = lev_dn_ (p, Res);
2.73 + val pt = update_metID pt (par_pblobj pt p) Celem.e_metID;
2.74 + in
2.75 + ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.e_ctxt)))], [], (pt,p')))
2.76 + end
2.77 + | solve (Tactic.Check_Postcond' (pI, _)) (ptp as (pt, (p, p_))) =
2.78 + let
2.79 + val pp = par_pblobj pt p
2.80 + val {scr, ...} = Specify.get_met (get_obj g_metID pt pp);
2.81 + val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)
2.82 + | _ => error "solve Check_Postcond: uncovered case get_loc"
2.83 + val prog_res =
2.84 + case LucinNEW.find_next_tactic scr (pt, (p, p_)) (Istate.Pstate pst) ctxt of
2.85 + LucinNEW.Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
2.86 + | LucinNEW.End_Program (_, Tactic.Check_Postcond' (_, (prog_res, _))) => prog_res
2.87 + | _ => raise ERROR ("solve Check_Postcond " ^ strs2str' pI)
2.88 + in (*for Applicable.applicable_in not yet available -----------vvvvv*)
2.89 + ("ok", LucinNEW.begin_end_prog (Tactic.Check_Postcond' (pI, (prog_res, [(*fill.later*)])))
2.90 + (Istate.e_istate, ContextC.e_ctxt) ptp)
2.91 + end
2.92 + | solve (Tactic.End_Proof'') (pt, (p, p_)) =
2.93 + ("end-proof", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (([], Res), (Istate.Uistate, ContextC.e_ctxt)))], [], (pt, (p, p_))))
2.94 + | solve (Tactic.End_Detail' t) (pt, (p, p_)) = (* could be done by generate1 ?!? *)
2.95 + let (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)
2.96 + val pr = (lev_up p, Res)
2.97 + in
2.98 + ("ok", ([(Tactic.End_Detail, Tactic.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))
2.99 + end
2.100 + (* ======== general case as fall htrough ======== *)
2.101 + | solve m (pt, po as (p, p_)) =
2.102 + if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
2.103 + then
2.104 + let
2.105 + val ctxt = get_ctxt pt po
2.106 + val ((p,p_),ps,_,pt) = Generate.generate1 (Celem.assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
2.107 + m (Istate.e_istate, ctxt) (p, p_) pt;
2.108 + in ("no-method-specified", (*Free_Solve*)
2.109 + ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, ((p, p_), (Istate.Uistate, ctxt)))], ps, (pt, (p, p_))))
2.110 + end
2.111 + else
2.112 + let
2.113 + val thy' = get_obj g_domID pt (par_pblobj pt p);
2.114 + val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
2.115 + in
2.116 + case LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
2.117 + LucinNEW.Safe_Step (istate, ctxt, tac) =>
2.118 + let
2.119 + val p' =
2.120 + case p_ of Frm => p
2.121 + | Res => lev_on p
2.122 + | _ => error ("solve: call by " ^ pos'2str (p, p_));
2.123 + val (p'', _, _,pt') =
2.124 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
2.125 + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
2.126 + (istate, ctxt) (p', p_) pt;
2.127 + in
2.128 + ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
2.129 + [(*ctree NOT cut*)], (pt', p'')))
2.130 + end
2.131 + | LucinNEW.Unsafe_Step (istate, ctxt, tac) =>
2.132 + let
2.133 + val p' =
2.134 + case p_ of Frm => p
2.135 + | Res => lev_on p
2.136 + | _ => error ("solve: call by " ^ pos'2str (p, p_));
2.137 + val (p'', _, _,pt') =
2.138 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
2.139 + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
2.140 + (istate, ctxt) (p', p_) pt;
2.141 + in
2.142 + ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
2.143 + [(*ctree NOT cut*)], (pt', p'')))
2.144 + end
2.145 + | _ => (* NotLocatable *)
2.146 + let
2.147 + val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, p_) pt;
2.148 + in
2.149 + ("not-found-in-script", ([(Tactic.input_from_T m, m, (po, is))], ps, (pt, p)))
2.150 + end
2.151 + end;
2.152
2.153 end
3.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Thu Dec 19 12:40:17 2019 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Thu Dec 19 16:41:57 2019 +0100
3.3 @@ -114,6 +114,8 @@
3.4 val result : T -> term
3.5 val creates_assms: T -> term list
3.6 val insert_assumptions: T -> Proof.context -> Proof.context
3.7 + val for_specify: input -> bool
3.8 + val for_specify': T -> bool
3.9
3.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.11 (* NONE *)
3.12 @@ -504,4 +506,33 @@
3.13
3.14 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
3.15
3.16 +fun for_specify (Init_Proof _) = true
3.17 + | for_specify Model_Problem = true
3.18 + | for_specify (Refine_Tacitly _) = true
3.19 + | for_specify (Refine_Problem _) = true
3.20 + | for_specify (Add_Given _) = true
3.21 + | for_specify (Del_Given _) = true
3.22 + | for_specify (Add_Find _) = true
3.23 + | for_specify (Del_Find _) = true
3.24 + | for_specify (Add_Relation _) = true
3.25 + | for_specify (Del_Relation _) = true
3.26 + | for_specify (Specify_Theory _) = true
3.27 + | for_specify (Specify_Problem _) = true
3.28 + | for_specify (Specify_Method _) = true
3.29 + | for_specify _ = false
3.30 +fun for_specify' (Init_Proof' _) = true
3.31 + | for_specify' (Model_Problem' _) = true
3.32 + | for_specify' (Refine_Tacitly' _) = true
3.33 + | for_specify' (Refine_Problem' _) = true
3.34 + | for_specify' (Add_Given' _) = true
3.35 + | for_specify' (Del_Given' _) = true
3.36 + | for_specify' (Add_Find' _) = true
3.37 + | for_specify' (Del_Find' _) = true
3.38 + | for_specify' (Add_Relation' _) = true
3.39 + | for_specify' (Del_Relation' _) = true
3.40 + | for_specify' (Specify_Theory' _) = true
3.41 + | for_specify' (Specify_Problem' _) = true
3.42 + | for_specify' (Specify_Method' _) = true
3.43 + | for_specify' _ = false
3.44 +
3.45 (**)end(**)
4.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 19 12:40:17 2019 +0100
4.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 19 16:41:57 2019 +0100
4.3 @@ -7,8 +7,8 @@
4.4 signature MATH_ENGINE =
4.5 sig
4.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
4.7 - val me : Solve.tac'_ -> Ctree.pos' -> NEW ->
4.8 - Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Telem.safe * Ctree.ctree
4.9 + val me : Tactic.input -> Ctree.pos' -> NEW -> Ctree.ctree ->
4.10 + Ctree.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
4.11 val autocalc : Ctree.pos' list -> Ctree.pos' -> (Ctree.state) * Generate.taci list ->
4.12 Solve.auto -> string * Ctree.pos' list * (Ctree.state)
4.13 val locatetac :
4.14 @@ -26,12 +26,12 @@
4.15 val set_theory : Rule.thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
4.16 val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
4.17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.18 - val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tactic.input) * Telem.safe * Ctree.ctree
4.19 + val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
4.20 val f2str : Generate.mout -> Rule.cterm'
4.21 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.22 type nxt_
4.23 datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
4.24 - val loc_solve_ : string * Tactic.T -> Ctree.ctree * Ctree.pos' -> lOc_
4.25 + val loc_solve_ : Tactic.T -> Ctree.ctree * Ctree.pos' -> lOc_
4.26 val loc_specify_ : Tactic.T -> Ctree.state -> lOc_
4.27 val nxt_specify_: Ctree.ctree * Ctree.pos' -> Chead.calcstate'
4.28 val TESTg_form : Ctree.state -> Generate.mout
4.29 @@ -71,7 +71,7 @@
4.30 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
4.31 fun loc_solve_ m (pt, pos) =
4.32 let
4.33 - val (msg, cs') = Solve.solve m (pt, pos);
4.34 + val (msg, cs') = Step_Solve.solve m (pt, pos);
4.35 in
4.36 case msg of "ok" => Updated cs' | msg => ERror msg
4.37 end
4.38 @@ -80,7 +80,7 @@
4.39 HElpless (**)
4.40 | Nexts of Chead.calcstate (**)
4.41
4.42 -(* locate a tactic in a script and apply it if possible;
4.43 +(* locate a tactic in a program and apply it if possible;
4.44 report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
4.45 fun locatetac _ (ptp as (_, ([], Pos.Res))) = ("end-of-calculation", ([], [], ptp))
4.46 | locatetac tac (ptp as (pt, p)) =
4.47 @@ -91,8 +91,8 @@
4.48 Applicable.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
4.49 | Applicable.Appl m =>
4.50 let
4.51 - val x = if member op = Solve.specsteps mI
4.52 - then loc_specify_ m ptp else loc_solve_ (mI, m) ptp
4.53 + val x = if Tactic.for_specify' m
4.54 + then loc_specify_ m ptp else loc_solve_ m ptp
4.55 in
4.56 case x of
4.57 ERror _ => ("failure", ([], [], ptp))
4.58 @@ -386,7 +386,7 @@
4.59 val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
4.60 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
4.61 val f = TESTg_form (pt,p)
4.62 - in (p, []:NEW, f, (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt) end
4.63 + in (p, []:NEW, f, tac, Telem.Sundef, pt) end
4.64 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
4.65
4.66 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
4.67 @@ -397,8 +397,8 @@
4.68 NEW loeschen, eigene Version von locatetac, step
4.69 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
4.70
4.71 -fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
4.72 - | me*) (_, tac) p _(*NEW remove*) pt =
4.73 +fun me (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
4.74 + | me*) tac p _(*NEW remove*) pt =
4.75 let
4.76 val (pt, p) =
4.77 (*locatetac is here for testing by me; step would suffice in me*)
4.78 @@ -424,11 +424,11 @@
4.79 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
4.80 in
4.81 (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
4.82 - (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt)
4.83 + tac, Telem.Sundef, pt)
4.84 end
4.85
4.86 (* for quick test-print-out, until 'type inout' is removed *)
4.87 fun f2str (Generate.FormKF cterm') = cterm'
4.88 - | f2str _ = error "f2str: uncovered case in fun.def.";
4.89 + | f2str _ = error "f2str: uncovered case in fun.def.";
4.90
4.91 -end
4.92 +(**)end(**)
5.1 --- a/src/Tools/isac/MathEngine/solve.sml Thu Dec 19 12:40:17 2019 +0100
5.2 +++ b/src/Tools/isac/MathEngine/solve.sml Thu Dec 19 16:41:57 2019 +0100
5.3 @@ -16,8 +16,9 @@
5.4 string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_))
5.5 val complete_solve :
5.6 auto -> Ctree.pos' list -> Ctree.state -> string * Ctree.pos' list * Ctree.state
5.7 +(*
5.8 val solve : string * Tactic.T -> Ctree.state -> string * Chead.calcstate'
5.9 -
5.10 +*)
5.11 val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
5.12
5.13 val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
5.14 @@ -113,6 +114,7 @@
5.15 (*FIXME.WN050821 compare solve ... begin_end_prog:
5.16 WN190811: solve ("Apply_Method",.. used by root-pbl + by locate_input_tactic !!!
5.17 *)
5.18 +(*-------------------------------------------------------------------
5.19 fun solve ("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)) (pt, (pos as (p, _))) =
5.20 let
5.21 val itms = case get_obj I pt p of
5.22 @@ -244,6 +246,7 @@
5.23 ("not-found-in-script", ([(Tactic.input_from_T m, m, (po, is))], ps, (pt, p)))
5.24 end
5.25 end;
5.26 +------------------------------------------------*)
5.27
5.28 (* tell how may steps of a calculation should be done by "fun autocalc"
5.29 FIXXXME040624: does NOT match interfaces/ITOCalc.java
5.30 @@ -344,7 +347,7 @@
5.31 case Applicable.applicable_in (p, p_) pt m of
5.32 Applicable.Notappl e => Generate.Error' e
5.33 | Applicable.Appl m =>
5.34 - if member op = specsteps mI
5.35 + if Tactic.for_specify' m
5.36 then
5.37 let val (_, _, f, _, _, _) = Chead.specify m (p, p_) [] pt
5.38 in f end
6.1 --- a/src/Tools/isac/TODO.thy Thu Dec 19 12:40:17 2019 +0100
6.2 +++ b/src/Tools/isac/TODO.thy Thu Dec 19 16:41:57 2019 +0100
6.3 @@ -83,7 +83,6 @@
6.4 \item Step_Specify in Specify/step-specify.sml in analogy to Interpret/... TODO
6.5 \begin{itemize}
6.6 \item Step_Specify.check <-- Applicable.applicable_in
6.7 - inserts all data into Tactic.T available -- not all are at time of call!
6.8 \item Step_Specify.add <-- Generate.generate1
6.9 \item Step_Specify.by_tactic : Tactic.input -> Ctree.state -> step_result
6.10 \item Step_Specify.by_formula: ?term? -> Ctree.state -> step_result
7.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Dec 19 12:40:17 2019 +0100
7.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Dec 19 16:41:57 2019 +0100
7.3 @@ -194,10 +194,10 @@
7.4 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
7.5 (*if*) member op = Solve.specsteps mI; (*else*)
7.6
7.7 - (*val Updated (cs' as (_, _, (_, p'))) =*) loc_solve_ (mI,m) ptp;
7.8 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
7.9 + (*val Updated (cs' as (_, _, (_, p'))) =*) loc_solve_ m ptp;
7.10 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
7.11
7.12 -"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
7.13 +"~~~~~ fun solve , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
7.14 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
7.15 val thy' = get_obj g_domID pt (par_pblobj pt p);
7.16 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
8.1 --- a/test/Tools/isac/Interpret/inform.sml Thu Dec 19 12:40:17 2019 +0100
8.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu Dec 19 16:41:57 2019 +0100
8.3 @@ -470,7 +470,7 @@
8.4 val ifo = "solve(x+1=2,x)";
8.5 val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "solve(x+1=2,x)";
8.6 show_pt pt;
8.7 -val nxt = ("Apply_Method",Apply_Method ["Test","squ-equ-test-subpbl1"]);
8.8 +val nxt = (Apply_Method ["Test","squ-equ-test-subpbl1"]);
8.9 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.10 if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
8.11 else error "inform.sml: diff.behav. CAScmd ([],Pbl)";
9.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 19 12:40:17 2019 +0100
9.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 19 16:41:57 2019 +0100
9.3 @@ -30,19 +30,19 @@
9.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.7 -case nxt of (_, Apply_Method ["diff", "integration"]) => ()
9.8 +case nxt of (Apply_Method ["diff", "integration"]) => ()
9.9 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
9.10 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
9.11
9.12 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
9.13 +"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
9.14 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
9.15 val (mI,m) = mk_tac'_ tac;
9.16 val Appl m = applicable_in p pt m;
9.17 member op = specsteps mI (*false*);
9.18 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = ((mI,m), ptp);
9.19 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
9.20
9.21 -"~~~~~ fun solve , args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) =
9.22 - (m, (pt, pos));
9.23 +"~~~~~ fun solve , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
9.24 + = (m, (pt, pos));
9.25 val {srls, ...} = get_met mI;
9.26 val itms = case get_obj I pt p of
9.27 PblObj {meth=itms, ...} => itms
9.28 @@ -105,7 +105,7 @@
9.29 (*// relevant call --------------------------------------------------------------------------\\*)
9.30 (*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
9.31
9.32 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt);
9.33 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
9.34
9.35 (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*) locatetac tac (pt,p) (*of*);
9.36 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
9.37 @@ -113,11 +113,11 @@
9.38 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
9.39 (*if*) member op = Solve.specsteps mI; (*else*)
9.40
9.41 - (** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ (mI,m) ptp;
9.42 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
9.43 + (** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ m ptp;
9.44 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
9.45
9.46 - (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Solve.solve m (pt, pos);
9.47 -"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
9.48 + (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Step_Solve.solve m (pt, pos);
9.49 +"~~~~~ fun solve , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
9.50 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
9.51 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
9.52 val thy' = get_obj g_domID pt (par_pblobj pt p);
9.53 @@ -231,8 +231,7 @@
9.54 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
9.55
9.56 (*/--------------------- final test ----------------------------------\\*)
9.57 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'"
9.58 - andalso pr_ctree pr_short pt =
9.59 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
9.60 ". ----- pblobj -----\n" ^
9.61 "1. x + 1 = 2\n" ^
9.62 "2. x + 1 + -1 * 2 = 0\n" ^
9.63 @@ -240,7 +239,8 @@
9.64 "3.1. -1 + x = 0\n" ^
9.65 "3.2. x = 0 + -1 * -1\n" ^
9.66 "4. [x = 1]\n"
9.67 -then () else error "re-build: fun locate_input_tactic changed";
9.68 +then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
9.69 +else error "re-build: fun locate_input_tactic changed 2";
9.70
9.71
9.72 "----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
9.73 @@ -277,11 +277,11 @@
9.74 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
9.75 (*if*) member op = Solve.specsteps mI (*else*);
9.76
9.77 - loc_solve_ (mI, m) ptp;
9.78 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI, m), ptp);
9.79 + loc_solve_ m ptp;
9.80 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
9.81 solve m (pt, pos);
9.82 (* ======== general case ======== *)
9.83 -"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
9.84 +"~~~~~ fun solve , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
9.85 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
9.86 val thy' = get_obj g_domID pt (par_pblobj pt p);
9.87 val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
10.1 --- a/test/Tools/isac/Interpret/script.sml Thu Dec 19 12:40:17 2019 +0100
10.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Dec 19 16:41:57 2019 +0100
10.3 @@ -67,12 +67,12 @@
10.4 (*val it = fn: string * tac_ -> ctree * (pos * pos_) -> lOc_*)
10.5 (mI,m); (*string * tac*)
10.6 ptp (*ctree * pos'*);
10.7 -"~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
10.8 +"~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = (m, ptp);
10.9 (*val (msg, cs') = solve m (pt, pos);
10.10 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
10.11 m;
10.12 (pt, pos);
10.13 -"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
10.14 +"~~~~~ fun solve, args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
10.15 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
10.16
10.17 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
10.18 @@ -106,13 +106,13 @@
10.19 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.20 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.21 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.22 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
10.23 +"~~~~~ fun me, args:"; val tac = nxt;
10.24 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
10.25 val (mI,m) = mk_tac'_ tac;
10.26 val Appl m = applicable_in p pt m;
10.27 member op = specsteps mI; (*false*)
10.28 -"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
10.29 -"~~~~~ fun solve , args:"; val (("Apply_Method", Apply_Method' (mI,_,_,ctxt)), pos as (p,_)) = (m, pos);
10.30 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
10.31 +"~~~~~ fun solve , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_)) = (m, pos);
10.32 val {srls, ...} = get_met mI;
10.33 val PblObj {meth=itms, ...} = get_obj I pt p;
10.34 val thy' = get_obj g_domID pt p;
10.35 @@ -323,5 +323,6 @@
10.36 then () else error "init_pstate changed for Biegelinie";
10.37
10.38 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
10.39 -if p = ([1], Pbl) andalso (fst nxt) = "Model_Problem" then ()
10.40 +if p = ([1], Pbl)
10.41 +then case nxt of Model_Problem => () | _ => error "Biegelinie 7.70 changed 1"
10.42 else error "modeling root-problem of Biegelinie 7.70 changed";
11.1 --- a/test/Tools/isac/Knowledge/algein.sml Thu Dec 19 12:40:17 2019 +0100
11.2 +++ b/test/Tools/isac/Knowledge/algein.sml Thu Dec 19 16:41:57 2019 +0100
11.3 @@ -74,7 +74,7 @@
11.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
11.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.6 if f2str f = "L = 104"
11.7 -then case nxt of ("End_Proof'", End_Proof') => ()
11.8 +then case nxt of End_Proof' => ()
11.9 | _ => error "algein.sml diff.behav. in erstNumerisch 99 1"
11.10 else error "algein.sml diff.behav. in erstNumerisch 99 2";
11.11 DEconstrCalcTree 1;
12.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Thu Dec 19 12:40:17 2019 +0100
12.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Thu Dec 19 16:41:57 2019 +0100
12.3 @@ -109,7 +109,7 @@
12.4 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
12.5 if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
12.6 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
12.7 -then case nxt of ("End_Proof'", End_Proof') => ()
12.8 +then case nxt of End_Proof' => ()
12.9 | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
12.10 else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
12.11
13.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Thu Dec 19 12:40:17 2019 +0100
13.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Thu Dec 19 16:41:57 2019 +0100
13.3 @@ -124,7 +124,7 @@
13.4 formals: ["l","q","v","b","s","vs","id_abl"]
13.5 actuals: ["L","q_0","x","[c, c_2, c_3, c_4]","dy","y","[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]"]*)
13.6
13.7 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
13.8 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
13.9 val (pt''', p''') =
13.10 (*locatetac is here for testing by me; step would suffice in me*)
13.11 case locatetac tac (pt,p) of
13.12 @@ -148,10 +148,10 @@
13.13 (*if*) member op = Solve.specsteps mI = false; (*else*)
13.14
13.15 loc_solve_ (mI,m) ptp;
13.16 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
13.17 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
13.18
13.19 Solve.solve m (pt, pos);
13.20 -"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _)))) =
13.21 +"~~~~~ fun solve , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _)))) =
13.22 (m, (pt, pos));
13.23 val {srls, ...} = Specify.get_met mI;
13.24 val itms = case get_obj I pt p of
13.25 @@ -218,7 +218,7 @@
13.26 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";
13.27 writeln (itms2str_ @{context} meth); (*[]*)
13.28
13.29 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
13.30 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
13.31 (* val (pt, p) = *)
13.32 (*locatetac is here for testing by me; step would suffice in me*)
13.33 case locatetac tac (pt,p) of
14.1 --- a/test/Tools/isac/Knowledge/diff.sml Thu Dec 19 12:40:17 2019 +0100
14.2 +++ b/test/Tools/isac/Knowledge/diff.sml Thu Dec 19 16:41:57 2019 +0100
14.3 @@ -176,7 +176,7 @@
14.4 (*val nxt = ("End_Proof'",End_Proof');*)
14.5 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
14.6 if f2str f = "3 + 2 * x"
14.7 - then case nxt of ("End_Proof'", End_Proof') => ()
14.8 + then case nxt of End_Proof' => ()
14.9 | _ => error "diff.sml: new.behav. in me (*+ tacs input*) 1"
14.10 else error "diff.sml: new.behav. in me (*+ tacs input*) 2";
14.11 (*if f = EmptyMout then () else error "new behaviour in + tacs input";
14.12 @@ -213,7 +213,7 @@
14.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.15 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.16 -case nxt of ("End_Proof'",End_Proof') => ()
14.17 +case nxt of End_Proof' => ()
14.18 | _ => error "new behaviour in tests/differentiate, 1.5.02 me from script";
14.19
14.20 "----------- primed id ----------------------------------";
15.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Thu Dec 19 12:40:17 2019 +0100
15.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Thu Dec 19 16:41:57 2019 +0100
15.3 @@ -310,7 +310,7 @@
15.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.5 (*val nxt = ("Model_Problem",Model_Problem ["by_explicit","make","function"])*)
15.6 ----------------------------------------------------------------------------*)
15.7 -case nxt of (_, Model_Problem(*["by_explicit", "make", "function"]*)) => ()
15.8 +case nxt of (Model_Problem(*["by_explicit", "make", "function"]*)) => ()
15.9 | _ => error "diffapp.sml: max-exp me, nxt = Model_Problem";
15.10
15.11 (*=== inhibit exn 110722=============================================================
16.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Thu Dec 19 12:40:17 2019 +0100
16.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Thu Dec 19 16:41:57 2019 +0100
16.3 @@ -519,7 +519,7 @@
16.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.7 -case nxt of ("Specify_Method",_) => ()
16.8 +case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
16.9 | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
16.10
16.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.12 @@ -529,7 +529,7 @@
16.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.15 case nxt of
16.16 - (_, Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
16.17 + (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
16.18 | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
16.19
16.20 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.21 @@ -537,7 +537,7 @@
16.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.24 case nxt of
16.25 - (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
16.26 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
16.27 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
16.28
16.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.30 @@ -557,14 +557,14 @@
16.31 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.33 case nxt of
16.34 - (_, Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
16.35 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
16.36 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
16.37 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.38 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.39 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
16.40 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
16.41 case nxt of
16.42 - (_, End_Proof') => ()
16.43 + (End_Proof') => ()
16.44 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
16.45
16.46 "----------- me [linear,system] ..normalise..top_down_sub..-------";
16.47 @@ -585,7 +585,7 @@
16.48 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.49 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.50 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.51 -case nxt of (_,Specify_Method ["EqSystem", "normalise", "2x2"]) => ()
16.52 +case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => ()
16.53 | _ => error "eqsystem.sml [linear,system] specify b";
16.54 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.55 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.56 @@ -597,7 +597,7 @@
16.57 "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
16.58 then () else error "eqsystem.sml me simpl. before SubProblem b";
16.59 case nxt of
16.60 - (_, Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
16.61 + (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
16.62 | _ => error "eqsystem.sml me [linear,system] SubProblem b";
16.63
16.64 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.65 @@ -605,7 +605,7 @@
16.66 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.67 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.68 case nxt of
16.69 - (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
16.70 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
16.71 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
16.72
16.73 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.74 @@ -625,7 +625,7 @@
16.75 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.76 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.77 case nxt of
16.78 - (_, Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
16.79 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
16.80 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
16.81 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.82 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
16.83 @@ -633,7 +633,7 @@
16.84 if f2str f = "[c = -1 * q_0 * L ^^^ 3 / (24 * EI), c_2 = 0]"
16.85 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
16.86 case nxt of
16.87 - (_, End_Proof') => ()
16.88 + (End_Proof') => ()
16.89 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
16.90
16.91
17.1 --- a/test/Tools/isac/Knowledge/inssort.sml Thu Dec 19 12:40:17 2019 +0100
17.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Thu Dec 19 16:41:57 2019 +0100
17.3 @@ -110,7 +110,7 @@
17.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.6 if f2str f = "{|| 1, 2, 3 ||}"
17.7 -then case nxt of ("End_Proof'", End_Proof') => ()
17.8 +then case nxt of End_Proof' => ()
17.9 | _ => error "--- insertion sort with MathEngine CHANGED 1"
17.10 else error "--- insertion sort with MathEngine CHANGED 2";
17.11
17.12 @@ -144,7 +144,7 @@
17.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* nxt = ("Check_Postcond",..*)
17.14 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* nxt = ("End_Proof'",..*)
17.15 if f2str f = "{|| 1, 2, 3 ||}"
17.16 -then case nxt of ("End_Proof'", End_Proof') => ()
17.17 +then case nxt of End_Proof' => ()
17.18 | _ => error "--- insertion sort: CAS-command CHANGED 1"
17.19 else error "--- insertion sort: CAS-command CHANGED 2";
17.20
18.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Dec 19 12:40:17 2019 +0100
18.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Thu Dec 19 16:41:57 2019 +0100
18.3 @@ -414,7 +414,7 @@
18.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.5 "----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
18.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.7 -case nxt of (_, Apply_Method ["diff", "integration"]) => ()
18.8 +case nxt of (Apply_Method ["diff", "integration"]) => ()
18.9 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
18.10 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
18.11 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
19.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu Dec 19 12:40:17 2019 +0100
19.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Dec 19 16:41:57 2019 +0100
19.3 @@ -39,7 +39,7 @@
19.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
19.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
19.6 val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
19.7 -"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
19.8 +"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
19.9 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
19.10 val (pt, p) = ptp;
19.11 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
19.12 @@ -58,7 +58,7 @@
19.13 "----------- why not nxt = Model_Problem here ? ---------";
19.14 "----------- why not nxt = Model_Problem here ? ---------";
19.15 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt''';
19.16 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
19.17 +"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
19.18 val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
19.19 val (pt, p) = ptp;
19.20 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
20.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Thu Dec 19 12:40:17 2019 +0100
20.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Thu Dec 19 16:41:57 2019 +0100
20.3 @@ -182,7 +182,7 @@
20.4
20.5 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
20.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
20.7 -"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
20.8 +"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
20.9 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
20.10 val (mI,m) = mk_tac'_ tac;
20.11 val Appl m = applicable_in p pt m;
20.12 @@ -200,10 +200,10 @@
20.13 member op = specsteps mI (*false*);
20.14 (*loc_solve_ (mI,m) ptp;
20.15 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
20.16 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
20.17 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
20.18 (*solve m (pt, pos);
20.19 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
20.20 -"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
20.21 +"~~~~~ fun solve, args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
20.22 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
20.23 val thy' = get_obj g_domID pt (par_pblobj pt p);
20.24 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
21.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Thu Dec 19 12:40:17 2019 +0100
21.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu Dec 19 16:41:57 2019 +0100
21.3 @@ -263,8 +263,9 @@
21.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.7 -if f2str f = "3 - 2 * e + 2 * f + 2 * g" andalso #1 nxt = "End_Proof'" then ()
21.8 -else error "polyminus.sml: me simplification.for_polynomials.with_minus";
21.9 +if f2str f = "3 - 2 * e + 2 * f + 2 * g"
21.10 +then case nxt of End_Proof' => () | _ => error "me simplification.for_polynomials.with_minus 1"
21.11 +else error "polyminus.sml: me simplification.for_polynomials.with_minus 2";
21.12
21.13 "----------- pbl polynom vereinfachen p.33 -----------------------";
21.14 "----------- pbl polynom vereinfachen p.33 -----------------------";
22.1 --- a/test/Tools/isac/Knowledge/rateq.sml Thu Dec 19 12:40:17 2019 +0100
22.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu Dec 19 16:41:57 2019 +0100
22.3 @@ -92,7 +92,7 @@
22.4 val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt;
22.5 f2str f = "[x = 1 / 5]";
22.6 case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*));
22.7 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
22.8 +"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
22.9 val (pt, p) = case locatetac tac (pt,p) of
22.10 ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. locatetac";
22.11 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
22.12 @@ -276,7 +276,7 @@
22.13 test --- 'trace_script' from outside 'fun me '---
22.14 *)
22.15 val (pt''', p''') = (pt, p);
22.16 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
22.17 +"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
22.18 val (pt, p) = case locatetac tac (pt,p) of
22.19 ("ok", (_, _, ptp)) => ptp | _ => error "error in test setup";
22.20 "~~~~~ step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
23.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Thu Dec 19 12:40:17 2019 +0100
23.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Thu Dec 19 16:41:57 2019 +0100
23.3 @@ -91,7 +91,7 @@
23.4 term2str t = "1 = 2 + -2 * sqrt x";
23.5 (*... which works; thus error must be in script interpretation*)
23.6
23.7 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
23.8 +"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
23.9 val (pt, p) = case locatetac tac (pt,p) of
23.10 ("ok", (_, _, ptp)) => ptp;
23.11 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
24.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Thu Dec 19 12:40:17 2019 +0100
24.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Thu Dec 19 16:41:57 2019 +0100
24.3 @@ -46,7 +46,7 @@
24.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
24.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem",*)
24.6 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Model_Problem",*)
24.7 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
24.8 +"~~~~~ fun me, args:"; val (tac) = nxt;
24.9 val (pt, p) = case locatetac tac (pt,p) of
24.10 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
24.11 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
25.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Thu Dec 19 12:40:17 2019 +0100
25.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Thu Dec 19 16:41:57 2019 +0100
25.3 @@ -133,7 +133,7 @@
25.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
25.5 val FormKF res = f;
25.6 if res = "[x = 1]"
25.7 -then case nxt of ("End_Proof'", End_Proof') => ()
25.8 +then case nxt of End_Proof' => ()
25.9 | _ => error "new behaviour in test: miniscript with mini-subpbl 1"
25.10 else error "new behaviour in test: miniscript with mini-subpbl 2"
25.11
26.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Thu Dec 19 12:40:17 2019 +0100
26.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Thu Dec 19 16:41:57 2019 +0100
26.3 @@ -46,7 +46,7 @@
26.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem",*)
26.6 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Model_Problem",*)
26.7 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
26.8 +"~~~~~ fun me, args:"; val (tac) = nxt;
26.9 val (pt, p) = case locatetac tac (pt,p) of
26.10 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
26.11 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
27.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 19 12:40:17 2019 +0100
27.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 19 16:41:57 2019 +0100
27.3 @@ -136,7 +136,7 @@
27.4 ("Test", ["sqroot-test","univariate","equation","test"],
27.5 ["Test","squ-equ-test-subpbl1"]);
27.6 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
27.7 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
27.8 +"~~~~~ fun me, args:"; val tac = nxt;
27.9 val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
27.10 "~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
27.11 val pIopt = get_pblID (pt,ip);
27.12 @@ -369,7 +369,7 @@
27.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
27.14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
27.15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
27.16 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ctree)) =
27.17 +"~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW(*remove*)), (pt:ctree)) =
27.18 (nxt, p, [], pt);
27.19 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
27.20 val (pt, p) = ptp;
28.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu Dec 19 12:40:17 2019 +0100
28.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu Dec 19 16:41:57 2019 +0100
28.3 @@ -69,7 +69,7 @@
28.4 (*\\\----------------------------------------- saved for final check -----------------------///*)
28.5
28.6 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
28.7 -case nxt of ("Model_Problem", _) => ()
28.8 +case nxt of Model_Problem => ()
28.9 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";
28.10
28.11
29.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Thu Dec 19 12:40:17 2019 +0100
29.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Thu Dec 19 16:41:57 2019 +0100
29.3 @@ -11,7 +11,7 @@
29.4 (*for resuming after stepping into code*)
29.5 val (p''',f''',nxt''',pt''') = (p,f,nxt,pt);
29.6
29.7 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ctree)) = (nxt, p, [], pt);
29.8 +"~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW), (pt:ctree)) = (nxt, p, [], pt);
29.9 val (pt, p) =
29.10 (*ERROR nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)
29.11 case locatetac tac (pt,p) of
29.12 @@ -93,5 +93,5 @@
29.13
29.14 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_,Add_Given "equality (x + 1 = 2)*)
29.15 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = (_,Add_Given "solveFor x"*)
29.16 -case nxt of (_, Add_Given "solveFor x") => ()
29.17 +case nxt of (Add_Given "solveFor x") => ()
29.18 | _ => error "minisubpbl: Add_Given is broken in root-problem";
30.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Dec 19 12:40:17 2019 +0100
30.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Dec 19 16:41:57 2019 +0100
30.3 @@ -21,7 +21,7 @@
30.4 (*me nxt'''' p'''' [] pt''''; "ERROR in creating the environment..", SHOULD BE("Apply_Method",.*)
30.5 "~~~~~ we continue with (@1) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
30.6 val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
30.7 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
30.8 +"~~~~~ fun me, args:"; val tac = nxt;
30.9 val (pt, p) =
30.10 (*locatetac is here for testing by me; step would suffice in me*)
30.11 case locatetac tac (pt,p) of
30.12 @@ -44,14 +44,14 @@
30.13 1.ERROR WAS: nxt = ("Empty_Tac",..
30.14 2.ERROR WAS: *** stac2tac_ TODO: no match for (Rewrite_Set ''norm_equation'') (x + 1 = 2)*)
30.15 "~~~~~ we continue with (@2) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
30.16 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
30.17 +"~~~~~ fun me, args:"; val tac = nxt;
30.18 val ("ok", (_, _, (pt''''',p'''''))) = locatetac tac (pt,p);
30.19 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
30.20 val (mI,m) = mk_tac'_ tac; (*mI = "Apply_Method"*)
30.21 val Appl m = applicable_in p pt m; (*m = Apply_Method'..*)
30.22 member op = specsteps mI; (*false*)
30.23 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
30.24 -"~~~~~ fun solve , args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
30.25 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);
30.26 +"~~~~~ fun solve , args:"; val (Apply_Method' (mI,_,_,_), pos as (p,_)) = (m, pos);
30.27 val PblObj {meth, ctxt, ...} = get_obj I pt p;
30.28 val thy' = get_obj g_domID pt p;
30.29 val thy = assoc_thy thy';
30.30 @@ -165,5 +165,5 @@
30.31 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule.id_rls rls, idT) *)
30.32
30.33 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
30.34 -case nxt of ("Rewrite_Set", _) => ()
30.35 +case nxt of (Rewrite_Set _) => ()
30.36 | _ => error "minisubpbl: Method not started in root-problem";
31.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Dec 19 12:40:17 2019 +0100
31.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Dec 19 16:41:57 2019 +0100
31.3 @@ -24,12 +24,13 @@
31.4 1 relevant for original decomposition *)
31.5 (*[1], Res*)val (p'''_',_,f,nxt'''_',_,pt'''_') = me nxt'''' p'''' [] pt'''';(*nxt = Rewrite_Set "Test_simplify"*)
31.6
31.7 -if p'''' = ([1], Frm) andalso f'''' = FormKF "x + 1 = 2" andalso fst nxt'''' = "Rewrite_Set"
31.8 -then () else error "250-Rewrite_Set-from-method.sml: start of test CHANGED";
31.9 +if p'''' = ([1], Frm) andalso f'''' = FormKF "x + 1 = 2"
31.10 +then case nxt'''' of Rewrite_Set _ => () | _ => error "start of test CHANGED 1"
31.11 +else error "250-Rewrite_Set-from-method.sml: start of test CHANGED";
31.12
31.13 (* val (p,_,f,nxt,_,pt) = ERROR WAS: nxt = ("Empty_Tac",..*) me nxt p [] pt;
31.14 (* ERROR WAS: scan_dn1: call by ([3], Pbl) *)
31.15 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt'''', p'''', [], pt'''');
31.16 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt'''', p'''', [], pt'''');
31.17
31.18 (*ERROR WAS: scan_dn1: call by ([3], Pbl)*)
31.19 val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt,p) (*of*);
31.20 @@ -38,11 +39,11 @@
31.21 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
31.22 member op = Solve.specsteps mI (* = false*);
31.23
31.24 - loc_solve_ (mI,m) ptp ; (* scan_dn1: call by ([3], Pbl)*)
31.25 -"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos)) = ((mI,m), ptp);
31.26 + loc_solve_ m ptp ; (* scan_dn1: call by ([3], Pbl)*)
31.27 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos)) = (m, ptp);
31.28 solve m (pt, pos); (* scan_dn1: call by ([3], Pbl)*)
31.29 (* ======== general tactic as fall through ======== *)
31.30 -"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
31.31 +"~~~~~ fun solve , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
31.32 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = else*);
31.33 val thy' = get_obj g_domID pt (par_pblobj pt p);
31.34 val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
31.35 @@ -130,7 +131,7 @@
31.36 //--2 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
31.37 2 relevant for exception TERM raised (line 297 of "term.ML"): dest_Free -1 + x = 0 *)
31.38 (**)val (p,_,f,nxt,_,pt) = me nxt'''_' p'''_' [] pt'''_';(**)
31.39 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt'''_', p'''_', [], pt'''_');
31.40 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt'''_', p'''_', [], pt'''_');
31.41 val (pt, p) =
31.42 (*locatetac is here for testing by me; step would suffice in me*)
31.43 case locatetac tac (pt, p) of
31.44 @@ -237,7 +238,7 @@
31.45
31.46 if p = ([2], Res) andalso f2str f = "-1 + x = 0" then
31.47 case nxt of
31.48 - ("Subproblem", Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])) => ()
31.49 + (Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])) => ()
31.50 | _ => error "Minisubpbl/250-Rewrite_Set-from-method changed 1"
31.51 else error "Minisubpbl/250-Rewrite_Set-from-method changed 2";
31.52
32.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Dec 19 12:40:17 2019 +0100
32.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Dec 19 16:41:57 2019 +0100
32.3 @@ -23,16 +23,16 @@
32.4 (*[2], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = ("Subproblem"*)
32.5 (*//--1 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
32.6 1 relevant for updating ctxt *)
32.7 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
32.8 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
32.9
32.10 "~~~~~ fun locatetac , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
32.11 val (mI,m) = mk_tac'_ tac;
32.12 val Appl m = applicable_in p pt m;
32.13 member op = specsteps mI; (*false*)
32.14 (*val Updated (cs' as (_,_,(_,p'))) = loc_solve_ (mI,m) ptp;*)
32.15 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
32.16 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
32.17 (*val (msg, cs') = solve m (pt, pos);*)
32.18 -"~~~~~ fun solve , args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
32.19 +"~~~~~ fun solve , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
32.20 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
32.21 val thy' = get_obj g_domID pt (par_pblobj pt p);
32.22 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
32.23 @@ -122,6 +122,6 @@
32.24
32.25 if p = ([3], Pbl) andalso not (get_ctxt pt p |> is_e_ctxt)
32.26 then
32.27 - case nxt of ("Model_Problem", _) => ()
32.28 + case nxt of (Model_Problem) => ()
32.29 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem"
32.30 else error "Minisubpbl/300-init-subpbl.sml changed";
33.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Dec 19 12:40:17 2019 +0100
33.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Dec 19 16:41:57 2019 +0100
33.3 @@ -35,7 +35,7 @@
33.4 (*+*)if get_ctxt pt p |> is_e_ctxt then error "ctxt NOT initialised by Subproblem'}" else ();
33.5 (*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
33.6
33.7 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
33.8 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
33.9 val ("ok", (_, _, (pt'''', p''''))) = (*case*)
33.10
33.11 locatetac tac (pt, p) (*of*);
33.12 @@ -44,11 +44,11 @@
33.13 val Appl m = (*case*) applicable_in p pt m (*of*);
33.14 member op = specsteps mI; (*else*)
33.15
33.16 - loc_solve_ (mI, m) ptp;
33.17 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
33.18 + loc_solve_ m ptp;
33.19 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);
33.20
33.21 solve m (pt, pos);
33.22 -"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _))))
33.23 +"~~~~~ fun solve , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p, _))))
33.24 = (m, (pt, pos));
33.25 val itms = case get_obj I pt p of
33.26 PblObj {meth=itms, ...} => itms
33.27 @@ -86,5 +86,5 @@
33.28 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
33.29
33.30 if p = ([3, 1], Frm) andalso f2str f = "-1 + x = 0" andalso
33.31 - tac2str (snd nxt) = "Rewrite_Set_Inst ([(''bdv'', x)], \"isolate_bdv\")"
33.32 + tac2str nxt = "Rewrite_Set_Inst ([(''bdv'', x)], \"isolate_bdv\")"
33.33 then () else error "Minisubpbl/400-start-meth-subpbl changed";
34.1 --- a/test/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml Thu Dec 19 12:40:17 2019 +0100
34.2 +++ b/test/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml Thu Dec 19 16:41:57 2019 +0100
34.3 @@ -30,5 +30,5 @@
34.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
34.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
34.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
34.7 -case nxt of ("Rewrite_Set_Inst", Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")) => ()
34.8 +case nxt of (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")) => ()
34.9 | _ => error "Rewrite_Set_Inst changed";
35.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Thu Dec 19 12:40:17 2019 +0100
35.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Thu Dec 19 16:41:57 2019 +0100
35.3 @@ -33,7 +33,7 @@
35.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
35.5 val (pt''''', p''''') = (pt, p);
35.6
35.7 -"~~~~~ fun me , args:"; val (_,tac) = nxt;
35.8 +"~~~~~ fun me , args:"; val tac = nxt;
35.9 val (pt, p) = case locatetac tac (pt,p) of
35.10 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
35.11 val (pt'''', p'''') = (pt, p);
35.12 @@ -81,5 +81,5 @@
35.13 (*----------------------------------------############### changed*)
35.14
35.15 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
35.16 -case nxt of ("Check_Postcond", Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()
35.17 +case nxt of ( Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()
35.18 | _ => error "450-nxt-Check_Postcond broken"
36.1 --- a/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Thu Dec 19 12:40:17 2019 +0100
36.2 +++ b/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Thu Dec 19 16:41:57 2019 +0100
36.3 @@ -37,6 +37,6 @@
36.4 (*WN110521 worked without testing*)
36.5
36.6 val (p,_,f,nxt,_,pt) = me nxt p''' [] pt'''; (*nxt = Check_elementwise "Assumptions"*)
36.7 -case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => ()
36.8 +case nxt of (Check_elementwise "Assumptions") => ()
36.9 | _ => error "Check_elementwise changed; after switch sub-->root-method";
36.10
37.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Dec 19 12:40:17 2019 +0100
37.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Dec 19 16:41:57 2019 +0100
37.3 @@ -44,7 +44,7 @@
37.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR","univariate", ...]) *);
37.5
37.6 val (pt'''', p'''') = (pt, p);
37.7 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
37.8 +"~~~~~ fun me, args:"; val tac = nxt;
37.9 val (pt, p) = case locatetac tac (pt,p) of
37.10 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
37.11 show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
37.12 @@ -94,5 +94,5 @@
37.13 = (pt, (Proof_Context.theory_of ctxt), stac);
37.14
37.15 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
37.16 -case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => ()
37.17 +case nxt of (Check_elementwise "Assumptions") => ()
37.18 | _ => error "Check_elementwise changed; after switch sub-->root-method";
38.1 --- a/test/Tools/isac/Minisubpbl/600-postcond.sml Thu Dec 19 12:40:17 2019 +0100
38.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond.sml Thu Dec 19 16:41:57 2019 +0100
38.3 @@ -33,6 +33,6 @@
38.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
38.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
38.6 if p = ([], Res)
38.7 -then case nxt of ("End_Proof'", End_Proof') => ()
38.8 +then case nxt of End_Proof' => ()
38.9 | _ => error "calculation not finished correctly 1"
38.10 else error "calculation not finished correctly 2"
39.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Dec 19 12:40:17 2019 +0100
39.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Dec 19 16:41:57 2019 +0100
39.3 @@ -43,7 +43,7 @@
39.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.5
39.6 (*+*)if p = ([], Res)
39.7 -(*+*)then case nxt of ("End_Proof'", End_Proof') => ()
39.8 +(*+*)then case nxt of End_Proof' => ()
39.9 (*+*) | _ => error "calculation not finished correctly 1"
39.10 (*+*)else error "calculation not finished correctly 2";
39.11 (*+*)show_pt pt; (* 11 lines with subpbl *)
40.1 --- a/test/Tools/isac/Minisubpbl/790-complete.sml Thu Dec 19 12:40:17 2019 +0100
40.2 +++ b/test/Tools/isac/Minisubpbl/790-complete.sml Thu Dec 19 16:41:57 2019 +0100
40.3 @@ -35,8 +35,7 @@
40.4 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
40.5
40.6 (* final test ...*)
40.7 - if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'"
40.8 - andalso pr_ctree pr_short pt =
40.9 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
40.10 ". ----- pblobj -----\n" ^
40.11 "1. x + 1 = 2\n" ^
40.12 "2. x + 1 + -1 * 2 = 0\n" ^
40.13 @@ -44,4 +43,5 @@
40.14 "3.1. -1 + x = 0\n" ^
40.15 "3.2. x = 0 + -1 * -1\n" ^
40.16 "4. [x = 1]\n"
40.17 - then () else error "re-build: fun locate_input_tactic changed";
40.18 +then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
40.19 +else error "re-build: fun locate_input_tactic changed";
41.1 --- a/test/Tools/isac/Specify/calchead.sml Thu Dec 19 12:40:17 2019 +0100
41.2 +++ b/test/Tools/isac/Specify/calchead.sml Thu Dec 19 16:41:57 2019 +0100
41.3 @@ -74,7 +74,7 @@
41.4 ["DiffApp","max_by_calculus"]);
41.5 val c = []:cid;
41.6
41.7 -val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
41.8 +val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
41.9 val nxt = tac2tac_ pt p nxt;
41.10 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
41.11 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
41.12 @@ -166,7 +166,7 @@
41.13 ["DiffApp","max_by_calculus"]);
41.14 val c = []:cid;
41.15 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
41.16 -val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
41.17 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
41.18
41.19 val nxt = tac2tac_ pt p nxt;
41.20 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] pt;
41.21 @@ -735,14 +735,14 @@
41.22 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
41.23 []) : ctree*)
41.24 "----- WN101007 worked until here (checked same as isac2002) ---";
41.25 -case nxt of ("Model_Problem", Model_Problem) => ()
41.26 +case nxt of Model_Problem => ()
41.27 | _ => error "clchead.sml: check specify phase step 1";
41.28 "--- step 2 --";
41.29 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
41.30 (*val it = "--- step 2 --" : string
41.31 val p = ([], Pbl) : pos'
41.32 val f =
41.33 - Form'
41.34 + Form'
41.35 (PpcKF
41.36 (0, EdUndef, 0, Nundef,
41.37 (Problem [],
41.38 @@ -808,12 +808,12 @@
41.39 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
41.40 []) : ctree*)
41.41 "----- WN101007 ctree checked same as isac2002, diff. in nxt --- REPAIRED";
41.42 -case nxt of ("Add_Given", Add_Given "functionTerm (x + 1)") => ()
41.43 +case nxt of (Add_Given "functionTerm (x + 1)") => ()
41.44 | _ => error "clchead.sml: check specify phase step 2";
41.45 "--- step 3 --";
41.46 val (p,_,f,nxt,_,pt) = me nxt p c pt;
41.47 "----- WN101008 ctree checked same as isac2002, diff. in nxt --- REPAIRED";
41.48 -case nxt of ("Add_Given", Add_Given "integrateBy x") => ()
41.49 +case nxt of (Add_Given "integrateBy x") => ()
41.50 | _ => error "clchead.sml: check specify phase step 2";
41.51
41.52 "--------- check: fmz matches pbt -----------------------";
42.1 --- a/test/Tools/isac/Specify/ptyps.sml Thu Dec 19 12:40:17 2019 +0100
42.2 +++ b/test/Tools/isac/Specify/ptyps.sml Thu Dec 19 16:41:57 2019 +0100
42.3 @@ -333,7 +333,7 @@
42.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
42.5 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Add_Find", Add_Find "solutions L")*)
42.6
42.7 -val nxt = ("Specify_Problem", Specify_Problem ["LINEAR","univariate","equation","test"]);
42.8 +val nxt = (Specify_Problem ["LINEAR","univariate","equation","test"]);
42.9 (*=== specify a not-matching problem ------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
42.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
42.11 val www =
42.12 @@ -363,7 +363,7 @@
42.13 (*val nxt = ("Empty_Tac",Empty_Tac)
42.14 ... Refine_Problem ["LINEAR"..] fails internally 040312: works!?!*)
42.15
42.16 -val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
42.17 +val nxt = (Refine_Problem ["univariate","equation","test"]);
42.18 (*=== refine problem -----------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
42.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;
42.20 (*("Specify_Problem", Specify_Problem ["normalise", "univariate", ...])*)
42.21 @@ -392,7 +392,7 @@
42.22 (*nxt = Specify_Problem ["LINEAR","univariate","equation","test"])*)
42.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
42.24 (*xt = ("Specify_Method", Specify_Method ["Test", "solve_linear"])*)
42.25 -val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
42.26 +val nxt = (Refine_Problem ["univariate","equation","test"]);
42.27 val (p,_,f,nxt,_,pt) = me nxt p c pt;
42.28 (*("Specify_Problem", Specify_Problem ["LINEAR", "univariate", ...])*)
42.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
42.30 @@ -413,7 +413,7 @@
42.31 val FormKF res = f;
42.32
42.33 if res = "[x = 2]"
42.34 -then case nxt of ("End_Proof'", End_Proof') => ()
42.35 +then case nxt of End_Proof' => ()
42.36 | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"
42.37 else error "new behaviour in test:refine.sml:miniscript with mini-subpb 2"
42.38
43.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Dec 19 12:40:17 2019 +0100
43.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Dec 19 16:41:57 2019 +0100
43.3 @@ -107,6 +107,7 @@
43.4 open Input_Descript;
43.5 open Specify; show_ptyps;
43.6 open Applicable; mk_set;
43.7 + open Step_Solve;
43.8 open Solve; (* NONE *)
43.9 open Selem; e_fmz;
43.10 open Stool; (* NONE *)
44.1 --- a/test/Tools/isac/Test_Some.thy Thu Dec 19 12:40:17 2019 +0100
44.2 +++ b/test/Tools/isac/Test_Some.thy Thu Dec 19 16:41:57 2019 +0100
44.3 @@ -200,7 +200,7 @@
44.4 = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\"]"
44.5 (* should formulas from calculation really go into ctxt ? ^^^^^ ^^^^^^^^^*)
44.6 \<close> ML \<open>
44.7 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [1], pt);
44.8 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [1], pt);
44.9 \<close> ML \<open>
44.10 val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt, p) (*of*);
44.11 \<close> ML \<open>
44.12 @@ -222,7 +222,7 @@
44.13 \<close> ML \<open>
44.14 Solve.solve m (pt, pos);
44.15 \<close> ML \<open>
44.16 -"~~~~~ fun solve , args:"; val (("Check_Postcond", Tactic.Check_Postcond' (pI, _)), (pt, (p, p_)))
44.17 +"~~~~~ fun solve , args:"; val (Tactic.Check_Postcond' (pI, _)), (pt, (p, p_)))
44.18 = (m, (pt, pos));
44.19 \<close> ML \<open>
44.20 \<close> ML \<open>