# HG changeset patch # User Walther Neuper # Date 1573049307 -3600 # Node ID 3ce3d089bd649e86c35bf8e1b00e50bc700834fa # Parent 08512202c2c6c7547c542511843d87864c63673b lucin: args of appy, assy & Co reorganised diff -r 08512202c2c6 -r 3ce3d089bd64 src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 06 15:08:27 2019 +0100 @@ -31,8 +31,8 @@ | Helpless | End_Program (*val determine_next_tactic : Rule.program -> Ctree.state -> Istate.T -> Proof.context -> next_tactic_result *) - val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T * 'a -> - Tactic.T * (Istate.T * 'a) * (term * Telem.safe) + val determine_next_tactic: Rule.theory' * 'a -> Ctree.state -> Rule.program -> Istate.T * 'b + -> Tactic.T * (Istate.T * Proof.context) * (term * Telem.safe) (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) datatype assoc = @@ -41,26 +41,23 @@ | NasNap of term * Env.T; val assoc2str : assoc -> string (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) - datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T - val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate' -(*old* )val appy: Rule.theory' * Rule.rls -> Ctree.state -> Istate.pstate -> term -> appy( *old*) -(*new*)val appy: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> appy(*new*) -(*old* )val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> term -> appy( *old*) -(*new*)val nxt_up: Rule.program * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> appy(*new*) -(*old* )val nstep_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> appy( *old*) -(*new*)val nstep_up: Rule.program * (Ctree.state * Rule.theory') -> Istate.pstate -> appy(*new*) val go : Celem.loc_ -> term -> term val go_up: Celem.loc_ -> term -> term - val execute_progr_1 : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T -> appy - val execute_progr_2 : Rule.rls -> Tactic.T -> Ctree.state -> Rule.program * 'a -> Istate.T * Proof.context -> assoc val check_Let_up : Istate.pstate -> term -> term * term val check_Seq_up: Istate.pstate -> term -> term -(*old* )val assy : Proof.context * Rule.rls * Ctree.state * Istate.asap -> Istate.pstate * Tactic.T -> term -> assoc( *old*) -(*new*)val assy: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc(*new*) -(*old* )val ass_up : Proof.context * Rule.rls * Rule.program * Ctree.state -> Istate.pstate * Tactic.T -> term -> assoc( *old*) -(*new*)val ass_up: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc;(*new*) -(*old* )val astep_up : Proof.context * Rule.rls * Rule.program * Ctree.state -> Istate.pstate * Tactic.T -> assoc( *old*) -(*new*)val astep_up: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> assoc;(*new*) + + datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T + val appy: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> appy + val nxt_up: Rule.program * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> appy + val nstep_up: Rule.program * (Ctree.state * Rule.theory') -> Istate.pstate -> appy + val execute_progr_1: Rule.program * (Ctree.state * Rule.theory') -> Istate.T -> appy + + val assy: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc + val ass_up: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc; + val astep_up: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> assoc; + val execute_progr_2: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> assoc + + val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate' ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) end @@ -185,7 +182,7 @@ | _ => Napp env) end -fun nxt_up (yyy as (Rule.Prog sc, xxx)) (ist as {finish, ...}) (Const ("HOL.Let"(*1a*), _) $ _) = +fun nxt_up (yyy as (Rule.Prog sc, xxx)) (ist as {finish, ...}) (Const ("HOL.Let"(*1*), _) $ _) = if finish = Napp_ then nstep_up yyy (ist |> path_up) else (*Skip_*) @@ -267,19 +264,18 @@ nxt_up yyy (ist |> path_up) (go_up path sc) else (*interpreted to end*) if finish = Skip_ then Skip (get_act_env ist) else Napp env - | nstep_up _ (ist as {path, ...}) = + | nstep_up _ {path, ...} = raise ERROR ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str path) - -fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate (ist as {path, ...})) = +fun execute_progr_1 (sc as Rule.Prog prog, cct) (Istate.Pstate (ist as {path, ...})) = if 0 = length path - then appy (ptp, (fst thy)) (trans_scan_down2 ist)(*sets AppUndef?!?*) (Program.body_of prog)(*new*) - else nstep_up (sc, (ptp, (fst thy))) (trans_scan_up2 ist |> upd_appy Skip_)(*sets AppUndef?!?*)(*new*) -| execute_progr_1 _ _ _ _ = raise ERROR "execute_progr_1: uncovered pattern"; + then appy cct (trans_scan_down2 ist) (Program.body_of prog) + else nstep_up (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_) +| execute_progr_1 _ _ = raise ERROR "execute_progr_1: uncovered pattern"; (* decide for the next applicable Prog_Tac in the program *) -fun determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate ist, ctxt) = - (case execute_progr_1 thy ptp sc (Istate.Pstate ist) of +fun determine_next_tactic (thy, _) (ptp as (pt, (p, _))) sc (Istate.Pstate ist, _(*ctxt*)) = + (case execute_progr_1 (sc, (ptp, thy)) (Istate.Pstate ist) of Skip (v, _) => (* program finished *) (case par_pbl_det pt p of (true, p', _) => @@ -287,14 +283,14 @@ val (_, pblID, _) = get_obj g_spec pt p'; in (Tactic.Check_Postcond' (pblID, (v, [(*assigned in next step*)])), - (Istate.e_istate, ctxt), (v, Telem.Safe)) + (Istate.e_istate, ContextC.e_ctxt), (v, Telem.Safe)) end | _ => - (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v, Telem.Safe))) + (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ContextC.e_ctxt), (v, Telem.Safe))) | Napp _ => - (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *) + (Tactic.Empty_Tac_, (Istate.e_istate, ContextC.e_ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *) | Appy (m', (ist as {act_arg, ...})) => - (m', (Pstate ist, ctxt), (act_arg, Telem.Safe))) (* found next tac *) + (m', (Pstate ist, ContextC.e_ctxt), (act_arg, Telem.Safe))) (* found next tac *) | determine_next_tactic _ _ _ (is, _) = error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is)); @@ -322,7 +318,7 @@ fun assy xxx ist (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))) = (case assy xxx (ist |> path_down [L, R]) e of - NasApp (ist', ctxt, ss) => + NasApp (ist', _, _) => assy xxx (ist' |> path_down [R, D] |> upd_env' (TermC.mk_Free (id, T)) |> trans_ass ist) b | NasNap (v, E) => assy xxx (ist |> path_down [R, D] |> upd_env (Env.upd_env E (TermC.mk_Free (id, T), v))) b @@ -400,7 +396,7 @@ | Chead.Notappl _ => (NasNap (ist |> get_act_env))) )); -fun ass_up (yyy as (prog as Rule.Prog p, xxx as (cstate, ctxt, tac))) ist (Const ("HOL.Let"(*1*), _) $ _) = +fun ass_up (yyy as (prog as Rule.Prog p, xxx as (cstate, _, _))) ist (Const ("HOL.Let"(*1*), _) $ _) = let val (i, body) = check_Let_up ist p in case assy xxx (ist |> path_up_down [R, D] |> upd_env' i |> upd_or Aundef) body of @@ -412,21 +408,21 @@ | ass_up yyy ist (Const ("HOL.Let"(*3*), _) $ _ $ (Abs _)) = astep_up yyy ist (*all has been done in (*2*) below*) - | ass_up yyy ist (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _) = astep_up yyy ist + | ass_up yyy ist (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _) = astep_up yyy ist | ass_up yyy ist (Const ("Tactical.Seq"(*2*), _) $ _ $ _) = astep_up yyy ist (*2*: comes from e2*) (* comes from e1, goes to e2 *) | ass_up (yyy as (prog as Rule.Prog p, xxx as (cstate, _, _))) ist (Const ("Tactical.Seq"(*3*), _) $ _ ) = let val e2 = check_Seq_up ist p in - case assy xxx (ist |> path_up_down[R] |> upd_or Aundef) e2 of + case assy xxx (ist |> path_up_down [R] |> upd_or Aundef) e2 of NasNap (v, E) => astep_up yyy (ist |> path_up |> upd_act_env (v, E)) | NasApp (ist', ctxt', tac') => astep_up (prog, (cstate, ctxt', tac')) ist' | zzz => zzz end - | ass_up yyy ist (Const ("Tactical.Try"(*1*),_) $ _ $ _) = astep_up yyy ist - | ass_up yyy ist (Const ("Tactical.Try"(*2*),_) $ _) = astep_up yyy ist + | ass_up yyy ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = astep_up yyy ist + | ass_up yyy ist (Const ("Tactical.Try"(*2*), _) $ _) = astep_up yyy ist | ass_up (yyy as (prog, xxx as (cstate, _, _))) (ist as {eval, ...}) (t as Const ("Tactical.While"(*1*),_) $ c $ e $ a) = if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.upd_env' a (get_act_env ist)) c) @@ -468,18 +464,17 @@ if 1 < length path then ass_up yyy (ist |> path_up) (go (path_up' path) sc) else (NasNap (get_act_env ist)) - | astep_up _ (ist as {path, ...}) = + | astep_up _ {path, ...} = raise ERROR ("astep_up: uncovered fun-def with " ^ Celem.loc_2str path) - -fun execute_progr_2 _ m (pt, p) (scr as Rule.Prog sc, _) (Istate.Pstate (ist as {path, ...}), ctxt) = +fun execute_progr_2 (scr as Rule.Prog sc, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) = if path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) - then assy ((pt, p), ctxt, m) (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc) - else astep_up (scr, ((pt, p), ctxt, m)) ist - | execute_progr_2 _ _ _ _ _ = raise ERROR "execute_progr_2: uncovered pattern in fun.def" + then assy cctt (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc) + else astep_up (scr, cctt) ist + | execute_progr_2 _ _ = raise ERROR "execute_progr_2: uncovered pattern in fun.def" fun locate_input_tactic (progr as Rule.Prog _) cstate istate ctxt tac = - (case execute_progr_2 Rule.e_rls tac cstate (progr, Rule.e_rls) (istate, ctxt) of + (case execute_progr_2 (progr, (cstate, ctxt, tac)) istate of Assoc ((ist as {assoc, ...}), ctxt, tac') => if assoc then Safe_Step (Istate.Pstate ist, ctxt, tac') @@ -556,8 +551,7 @@ | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc" val thy' = get_obj g_domID pt pp; val thy = Celem.assoc_thy thy'; - val (_, _, (scval, _(*scsaf*))) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc; - (* Telem.safe should go on to Check_Postcond' vvvvv *) + val (_, _, (scval, _)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc; in if pp = [] then @@ -604,11 +598,11 @@ val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is; (* TODO here ^^^ return finished/helpless/ok ?*) in case tac_ of - Tactic.End_Detail' _ => ([(Tactic.End_Detail, - Tactic.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos)) - | _ => begin_end_prog tac_ is ptp + Tactic.End_Detail' _ => + ([(Tactic.End_Detail, Tactic.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos)) + | _ => begin_end_prog tac_ is ptp end; - + (* compare inform with ctree.form at current pos by nrls; if found, embed the derivation generated during comparison if not, let the mat-engine compute the next ctree.form *) diff -r 08512202c2c6 -r 3ce3d089bd64 src/Tools/isac/Knowledge/GCD_Poly_ML.thy --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Mon Nov 04 11:40:29 2019 +0100 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Wed Nov 06 15:08:27 2019 +0100 @@ -1373,6 +1373,25 @@ additionally a notepad is required. Further examples for GCD are at [[2]]. \ + +section \structure providing unique identifiers in tests\ +ML \ +\ ML \ +signature GCD_POLY_ML = +sig + val eval: poly -> int -> int -> poly end +(**) +structure Gcd_ML(**): GCD_POLY_ML(**) = +struct +(**) + fun eval (p: poly) var value = order (map (eval_monom var value) p) +end +\ ML \ +\ + +end + + diff -r 08512202c2c6 -r 3ce3d089bd64 src/Tools/isac/MathEngine/solve.sml --- a/src/Tools/isac/MathEngine/solve.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/src/Tools/isac/MathEngine/solve.sml Wed Nov 06 15:08:27 2019 +0100 @@ -141,18 +141,15 @@ in case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of LucinNEW.Safe_Step (istate, ctxt, tac) => -(*NEW*) let -(*NEW*) val (p'', _, _,pt') = -(*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac -(*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *) -(*NEW*) (istate, ctxt) (lev_on p, Pbl) pt; -(*NEW*) in -(*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))], -(*NEW*) [(*ctree NOT cut*)], (pt', p''))) -(*NEW*) end -(*OLD* ) ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], -(*OLD*) [(*ctree NOT cut*)], cstate)) -( *OLD*) + let + val (p'', _, _,pt') = + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *) + (istate, ctxt) (lev_on p, Pbl) pt; + in + ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))], + [(*ctree NOT cut*)], (pt', p''))) + end | _ => (* NotLocatable, but applicable_in from the beginning *) let val (p, ps, _, pt) = @@ -236,38 +233,34 @@ val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; in case LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m of -(*OLD* ) LucinNEW.Safe_Step ((*->*)cstate(*<-*), istate, (*->*)ctxt(*<-*), tac) => -( *NEW*) LucinNEW.Safe_Step (istate, ctxt, tac) => -(*NEW*) let -(*NEW*) val p' = -(*NEW*) case p_ of Frm => p -(*NEW*) | Res => lev_on p -(*NEW*) | _ => error ("solve: call by " ^ pos'2str (p, p_)); -(*NEW*) val (p'', _, _,pt') = -(*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac -(*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *) -(*NEW*) (istate, ctxt) (p', p_) pt; -(*NEW*) in -(*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))], -(*NEW*) [(*ctree NOT cut*)], (pt', p''))) -(*NEW*) end -(*OLD* ) ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], -(*OLD*) [(*ctree NOT cut*)], cstate)) -( *OLD*) + LucinNEW.Safe_Step (istate, ctxt, tac) => + let + val p' = + case p_ of Frm => p + | Res => lev_on p + | _ => error ("solve: call by " ^ pos'2str (p, p_)); + val (p'', _, _,pt') = + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *) + (istate, ctxt) (p', p_) pt; + in + ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))], + [(*ctree NOT cut*)], (pt', p''))) + end | LucinNEW.Unsafe_Step (istate, ctxt, tac) => -(*NEW*) let -(*NEW*) val p' = -(*NEW*) case p_ of Frm => p -(*NEW*) | Res => lev_on p -(*NEW*) | _ => error ("solve: call by " ^ pos'2str (p, p_)); -(*NEW*) val (p'', _, _,pt') = -(*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac -(*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *) -(*NEW*) (istate, ctxt) (p', p_) pt; -(*NEW*) in -(*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))], -(*NEW*) [(*ctree NOT cut*)], (pt', p''))) -(*NEW*) end + let + val p' = + case p_ of Frm => p + | Res => lev_on p + | _ => error ("solve: call by " ^ pos'2str (p, p_)); + val (p'', _, _,pt') = + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *) + (istate, ctxt) (p', p_) pt; + in + ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))], + [(*ctree NOT cut*)], (pt', p''))) + end | _ => (* NotLocatable *) let val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, p_) pt; @@ -401,10 +394,10 @@ SOME (pt, _) => ("ok",([], [], (pt, (p, Ctree.Met)))) | NONE => (*/-------------------------------------- NEW fun locate_input_formula------*) let - (*NEW*)val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p) - (*NEW*)val {scr = prog, ...} = Specify.get_met metID - (*NEW*)val istate = get_istate pt pos - (*NEW*)val ctxt = get_ctxt pt pos + val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p) + val {scr = prog, ...} = Specify.get_met metID + val istate = get_istate pt pos + val ctxt = get_ctxt pt pos in case LucinNEW.locate_input_formula prog (pt, pos) istate ctxt f_in of LucinNEW.Step (cstate, _(*istate*), _(*ctxt*)) => diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/BridgeLibisabelle/interface.sml --- a/test/Tools/isac/BridgeLibisabelle/interface.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/BridgeLibisabelle/interface.sml Wed Nov 06 15:08:27 2019 +0100 @@ -22,13 +22,13 @@ (* a simplified getter *) fun test_get_calc cI = - case assoc (!test_states, cI) of + case LibraryC.assoc (!test_states, cI) of NONE => error ("get_calc " ^ string_of_int cI ^ " not existent") | SOME c => c; (* a simplified updater *) fun test_upd_calc cI cs = - (if is_none (assoc (!test_states, cI)) + (if is_none (LibraryC.assoc (!test_states, cI)) then writeln ("upd_calc created new calculation " ^ string_of_int cI) else (); test_states := overwrite (!test_states, (cI, cs))) diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/BridgeLibisabelle/use-cases.sml --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Nov 06 15:08:27 2019 +0100 @@ -1044,7 +1044,7 @@ val p = get_pos 1 1; val (Form f, tac, asms) = pt_extract (pt, p); if term2str f = "[x = 1]" andalso p = ([], Res) - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then () + andalso terms2str asms = "[]" then () else error "FE-interface.sml: diff.behav. in from pbl -hierarchy"; DEconstrCalcTree 1; @@ -1062,7 +1062,7 @@ val p = get_pos 1 1; val (Form f, tac, asms) = pt_extract (pt, p); if term2str f = "[x = 1]" andalso p = ([], Res) - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then () + andalso terms2str asms = "[]" then () else error "FE-interface.sml: diff.behav. in from pbl -hierarchy"; DEconstrCalcTree 1; diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Interpret/inform.sml --- a/test/Tools/isac/Interpret/inform.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Interpret/inform.sml Wed Nov 06 15:08:27 2019 +0100 @@ -599,8 +599,7 @@ val ((pt, p), _) = get_calc 1; val (t, asm) = get_obj g_result pt []; if term2str t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso -terms2str asm = "[\"b * d * f \ 0\",\"d \ 0\",\"b \ 0\"," ^ - "\"a * x / (b * x) + c * x / (d * x) + e / f is_ratpolyexp\"]" +terms2str asm = "[]" then () else error "inform [rational,simplification] changed at end"; (*show_pt pt; [ diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Interpret/lucas-interpreter.sml --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 06 15:08:27 2019 +0100 @@ -40,35 +40,49 @@ val Appl m = applicable_in p pt m; member op = specsteps mI (*false*); "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = ((mI,m), ptp); -"~~~~~ fun solve , args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) = + +"~~~~~ fun solve , args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) = (m, (pt, pos)); -val {srls, ...} = get_met mI; - val PblObj {meth=itms, ...} = get_obj I pt p; - val thy' = get_obj g_domID pt p; - val thy = assoc_thy thy'; - val srls = Lucin.get_simplifier (pt, pos) - val (is as Istate.Pstate (ist as {env, ...}), ctxt, sc) = init_pstate srls ctxt itms mI; - val ini = init_form thy sc env; -(*+*)ini = NONE; (*true*) - val p = lev_dn p; - val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt); - val d = e_rls (*FIXME: get simplifier from domID*); -"~~~~~ fun locate_input_tactic , args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'), - (scr as Prog (h $ body),d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt)) = - ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt')); -val thy = assoc_thy thy'; -l = [] orelse ((*init.in solve..Apply_Method...*) - (last_elem o fst) p = 0 andalso snd p = Res); (*true*) -"~~~~~ fun assy, args:"; val (ya, (is as (E,l,rls,a,v,asap,S,b),ss), - (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) = - ((thy',ctxt,srls,d,Aundef), ((E,[R],rls,a,v,asap,S,b), [(m,EmptyMout,pt,p,[])]), body); - (*check: true*) term2str e = "Take (Integral f_f D v_v)"; -"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,rls,a,v,asap,S,b), (m,_,pt,(p,p_),c)::ss), t) = - (ya, ((E , l@[L,R], rls,a,v,asap,S,b),ss), e); -val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t; -(* val ctxt = get_ctxt pt (p,p_) -exception PTREE "get_obj: pos = [0] does not exist" raised -(line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*) + val {srls, ...} = get_met mI; + val itms = case get_obj I pt p of + PblObj {meth=itms, ...} => itms + | _ => error "solve Apply_Method: uncovered case get_obj" + val thy' = get_obj g_domID pt p; + val thy = Celem.assoc_thy thy'; + val srls = Lucin.get_simplifier (pt, pos) + val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of + (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc) + | _ => error "solve Apply_Method: uncovered case init_pstate" + val ini = Lucin.init_form thy sc env; + val p = lev_dn p; + + val NONE = (*case*) ini (*of*); + val (m', (is', ctxt'), _) = + LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt); + + val Safe_Step (_, _, Take' _) = (*case*) + locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*); +"~~~~~ fun locate_input_tactic , args:"; val ((progr as Rule.Prog _), cstate, istate, ctxt, tac) + = (sc, (pt, (p, Res)), is', ctxt', m'); + + (*case*) execute_progr_2 (progr, (cstate, ctxt, tac)) istate (*of*); +"~~~~~ fun execute_progr_2 , args:"; val ((scr as Rule.Prog sc, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...}))) + = ((progr, (cstate, ctxt, tac)), istate); + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*); + + val Assoc (_, _, Take' _) = + assy cctt (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc); +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b)))) + = (cctt, (ist |> upd_path [R] |> upd_or Aundef), (Program.body_of sc)); + +(*+*) if term2str e = "Take (Integral f_f D v_v)" then () else error "assy Integral changed"; + + (*case*) + assy xxx (ist |> path_down [L, R]) e (*of*); + (*======= end of scanning tacticals, a leaf =======*) +"~~~~~ fun assy , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) + = (xxx, (ist |> path_down [L, R]), e); +val (a', STac stac) = handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t; "----------- re-build: fun locate_input_tactic -------------------------------------------------"; @@ -88,7 +102,7 @@ (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*) (*// relevant call --------------------------------------------------------------------------\\*) -(*[1], Res* )val (*** )xxx( ***) (p,_,f,nxt,_,pt) =*) me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*) +(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*) "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt); @@ -114,57 +128,54 @@ val srls = get_simplifier cstate; (** )val Assoc ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **) - (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*); -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt)) - = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt)); - (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*); + (*case*) execute_progr_2 (progr, (cstate, ctxt, tac)) istate (*of*); +"~~~~~ fun execute_progr_2 , args:"; val ((scr as Rule.Prog sc, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...}))) + = ((progr, (cstate, ctxt, tac)), istate); + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*); (** )val xxxxx_xx = ( **) - assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],rls,a,v,asap,S,b), m) (Program.body_of sc); -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,asap,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) - = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],a,v,asap,S,b), m), (Program.body_of sc)); + assy cctt (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc); +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b)))) + = (cctt, (ist |> upd_path [R] |> upd_or Aundef), (Program.body_of sc)); - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac) e (*of*); -"~~~~~ fun xxx , args:"; val (ya, ((E,l,rls,_,v,asap,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $ e1 $ e2 $ a)) - = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac), e); + (*case*) assy xxx (ist |> path_down [L, R]) e (*of*); +"~~~~~ fun assy , args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Seq"(*1*), _) $ e1 $ e2 $ a)) + = (xxx, (ist |> path_down [L, R]), e); - (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,asap,S,b),ss) e1 (*of*); -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e)) - = (ya, ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,asap,S,b),ss), e1); + (*case*) assy xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*); +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e)) + = (xxx, (ist |> path_down_form ([L, L, R], a)), e1); - (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e (*of*); + (*case*) assy xxx (ist |> path_down [R]) e (*of*); (*======= end of scanning tacticals, a leaf =======*) -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t) - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e); - val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*); - val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*); - (* 1st ContextC.insert_assumptions asms' ctxt *) +"~~~~~ fun assy , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) + = (xxx, (ist |> path_down [R]), e); + val (a', Celem.STac stac) = + (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); + val Lucin.Ass (m, v', ctxt) = + (*case*) associate pt ctxt (m, stac) (*of*); -(*NEW*) Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m) (*return value*); + Assoc (ist |> upd_subst_true (a', v'), ctxt, m) (*return value*); "~~~~~ from assy to execute_progr_2 return val:"; val (xxxxx_xx) - = (Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m)); (*return value*) + = (Assoc (ist |> upd_subst_true (a', v'), ctxt, m)); -"~~~~~ from execute_progr_2 to locate_input_tactic return val:"; val Assoc (is as (_,_,_,_,_,_,_,strong_ass), ctxt(*NEW*), tac') - = (Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m)); - (*if*) strong_ass; (*then*) +"~~~~~ from execute_progr_2 to fun locate_input_tactic return val:"; val Assoc ((ist as {assoc, ...}), ctxt, tac') + = (Assoc (ist |> upd_subst_true (a', v'), ctxt, m)); + (*if*) LibraryC.assoc (*then*); -"~~~~~ from locate_input_tactic to solve return:"; val Safe_Step (istate, ctxt, tac) - = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate is, ctxt, tac')(**); + Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*); +"~~~~~ from locate_input_tactic to fun solve return:"; val Safe_Step (istate, ctxt, tac) + = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**); (*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of solve *) -(*NEW*) val p' = -(*NEW*) case p_ of Frm => p -(*NEW*) | Res => lev_on p -(*NEW*) | _ => error ("solve: call by " ^ pos'2str (p, p_)); -(*NEW*) val (p'', _, _,pt') = -(*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m -(*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *) -(*NEW*) (Istate.Pstate (E,l,rls,a',v',asap,S,true), ctxt) (p', p_) pt; -(*NEW*) (*in*) -(*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))], -(*NEW*) [(*ctree NOT cut*)], (pt', p''))); + val (p'', _, _,pt') = + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *) + (istate, ctxt) (lev_on p, Pbl) pt; + (*in*) -(*NEW*)("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)) )], [], (pt', p''))); + ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))], + [(*ctree NOT cut*)], (pt', p''))) (*return value*); "~~~~~ from solve to loc_solve_ return:"; val ((msg, cs' : calcstate')) = ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)) )], [(*ctree NOT cut*)], (pt', p''))); @@ -191,8 +202,8 @@ = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt); (*//--------------------- check results from modified me ----------------------------------\\*) -if p = ([1], Res) andalso - pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n" +if p = ([2], Res) andalso + pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n" then (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => () | _ => error "") @@ -201,7 +212,8 @@ "~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**); (*\\------------------ end of modified "fun me" ---------------------------------------------//*) -(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*) + +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*) (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*) (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*) (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*) @@ -244,15 +256,17 @@ (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*) (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*) -(*+*)map tac2str (sel_appl_atomic_tacs pt p) = +(*+*)if map tac2str (sel_appl_atomic_tacs pt p) = ["Rewrite (\"subtrahiere_x_plus_minus\", \"\?l is_const; ?m is_const\\n\ ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", - "Rewrite (\"subtrahiere_x_minus_plus\", \"\?l is_const; ?m is_const\\n\ ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]; + "Rewrite (\"subtrahiere_x_minus_plus\", \"\?l is_const; ?m is_const\\n\ ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"] + then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED"; (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p); -(*+*)map tac2str (sel_appl_atomic_tacs pt p) = +(*+*)if map tac2str (sel_appl_atomic_tacs pt p) = ["Rewrite (\"tausche_minus\", \"\?b ist_monom; ?a kleiner ?b\\n\ ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \ ?a + ?c - ?b = ?a - ?b + ?c\")", "Rewrite (\"subtrahiere_x_plus_minus\", \"\?l is_const; ?m is_const\\n\ ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", - "Rewrite (\"subtrahiere_x_minus_plus\", \"\?l is_const; ?m is_const\\n\ ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]; + "Rewrite (\"subtrahiere_x_minus_plus\", \"\?l is_const; ?m is_const\\n\ ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"] + then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED"; (* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p); (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*) @@ -271,64 +285,62 @@ val thy' = get_obj g_domID pt (par_pblobj pt p); val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; - (*case*) LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); + (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); "~~~~~ fun locate_input_tactic , args:"; val ((progr as Rule.Prog _), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac) = (sc, (pt, po), (fst is), (snd is), m); val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*); - (*case*) execute_progr_2 srls tac cstate (progr, Rule.e_rls) (istate, ctxt) (*of*); -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt)) - = (srls, tac, cstate ,(progr, Rule.e_rls), (istate, ctxt)); - (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*); + (*case*) execute_progr_2 (progr, (cstate, ctxt, tac)) istate (*of*); +"~~~~~ fun execute_progr_2 , args:"; val ((scr as Rule.Prog sc, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...}))) + = ((progr, (cstate, ctxt, tac)), istate); + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*); - astep_up (ctxt,srls,scr,(pt, p)) ((E,l,rls,a,v,asap,S,b), m); -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,asap,S,b),ss)) - = ((ctxt,srls,scr,(pt, p)), ((E,l,a,v,asap,S,b), m)); - (*if*) 1 < length l (*then*); - val up = drop_last l; (* = [R, L, R, L, R]*) + astep_up (scr, cctt) ist; +"~~~~~ and astep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...})) + = ((scr, cctt), ist); + (*if*) 1 < length path (*then*); - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc); -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Try"(*2*),_) $ _)) - = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc)); + ass_up yyy (ist |> path_up) (go (path_up' path) sc); +"~~~~~ fun ass_up , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _)) + = (yyy, (ist |> path_up), (go (path_up' path) sc)); - astep_up ysa iss; -"~~~~~ fun astep_up , args:"; val (((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss))) - = (ysa, iss); - (*if*) 1 < length l (*then*); - val up = drop_last l; (* = [R, L, R, L]*) + astep_up yyy ist; +"~~~~~ and astep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...})) + = (yyy, ist); + (*if*) 1 < length path (*then*); - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc); -"~~~~~ fun ass_up , args:"; val ((ysa as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,asap,S,b),ss), - (Const ("Tactical.Seq"(*3*),_) $ _ )) - = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc)); - val up = drop_last l; - val Const ("Tactical.Seq",_) $ _ $ e2 = (*case*) go up sc (*of*); + ass_up yyy (ist |> path_up) (go (path_up' path) sc); +"~~~~~ fun ass_up , args:"; val ((yyy as (prog as Rule.Prog p, xxx as (cstate, _, _))), ist, + (Const ("Tactical.Seq"(*3*), _) $ _ )) + = (yyy, (ist |> path_up), (go (path_up' path) sc)); + val e2 = check_Seq_up ist p +; + (*case*) assy xxx (ist |> path_up_down [R] |> upd_or Aundef) e (*of*); +"~~~~~ fun assy , args:"; val (yyy, ist, (Const ("Tactical.Seq"(*2*), _) $ _ $ _)) + = (xxx, (ist |> path_up_down [R] |> upd_or Aundef), e2); - (*case*) assy ((*y,*)ctxt,s,d,Aundef) ((E, up @ [Celem.R], rls,a,v,asap,S,b),ss) e2 (*of*); -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $e1 $ e2)) - = (((*y,*)ctxt,s,d,Aundef), ((E, up @ [Celem.R], rls,a,v,asap,S,b),ss), e2); - val NasApp ((E,_,_,_,v,_,_,_), ctxt(*NEW*), ss) = (*case*) assy ya ((E, l @ [Celem.L, Celem.R], rls,a,v,asap,S,b),ss) e1 (*of*); + (*case*) assy xxx (ist |> path_down [L, R]) e1 (*of*); +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e)) + = (xxx, (ist |> path_down [L, R]), e1); - assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e2; -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*2*),_) $ e)) - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e2); + (*case*) assy xxx (ist |> path_down [R]) e (*of*); + (*======= end of scanning tacticals, a leaf =======*) +"~~~~~ fun assy , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) + = (xxx, (ist |> path_down [R]), e); + val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); + val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*); + val Aundef = (*case*) or (*of*); + val Notappl "norm_equation not applicable" = + (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*); - (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e (*of*); - (*======= end of scanning tacticals, a leaf =======*) -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t) - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e); - val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*); - val Lucin.NotAss = (*case*) Lucin.associate pt ctxt (m, stac) (*of*); - val Aundef = (*case*) ap (*of*); - val Appl m' = (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*); - val is = (E,l,rls,a',Lucin.tac_2res m',asap,S,false(*FIXXXME.WN0?*)); - NasApp (is, ctxt, m) (* return value *); + (NasNap (ist |> get_act_env)) (* return value *); val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \ ?a kleiner ?b \ ?b - ?a = - ?a + ?b"*)), t, (res, asm)) = m; -if scrstate2str is = - "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,R,R], e_rls, SOMEt_t, \n" ^ - "- (8 * g) + (-9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Aundef, AppUndef_, false)" + +if scrstate2str ist = + "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], e_rls, SOMEt_t, \n" ^ + "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Aundef, AppUndef_, false)" andalso term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g" andalso @@ -346,3 +358,4 @@ "----------- re-build: fun locate_input_tactic -------------------------------------------------"; "----------- re-build: fun locate_input_tactic -------------------------------------------------"; "----------- re-build: fun locate_input_tactic -------------------------------------------------"; + diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Knowledge/atools.sml --- a/test/Tools/isac/Knowledge/atools.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Knowledge/atools.sml Wed Nov 06 15:08:27 2019 +0100 @@ -387,7 +387,7 @@ "----------- fun eval_binop -----------------------------"; "----------- fun eval_binop -----------------------------"; "----------- fun eval_binop -----------------------------"; -val (op_, ef) = the (assoc (KEStore_Elems.get_calcs @{theory}, "TIMES")); +val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES")); val t = (Thm.term_of o the o (parse thy)) "2 * 3"; (*val SOME (thmid,t') = *)get_pair thy op_ ef t; ; diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Knowledge/diophanteq.sml --- a/test/Tools/isac/Knowledge/diophanteq.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Wed Nov 06 15:08:27 2019 +0100 @@ -36,10 +36,10 @@ val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst (num_str @{thm "int_isolate_add"}) t; term2str t; -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; "----------- mathengine with usecase1 -------------------"; @@ -71,10 +71,10 @@ SOME t' => t' | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2"; -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Knowledge/gcd_poly_ml.sml --- a/test/Tools/isac/Knowledge/gcd_poly_ml.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Knowledge/gcd_poly_ml.sml Wed Nov 06 15:08:27 2019 +0100 @@ -55,7 +55,7 @@ "----------- infix %%*%% --------------------------------"; "----------- fun gcd_coeff ------------------------------"; (*"----------- fun gcd_coeff_poly -------------------------";*) -"----------- fun eval -----------------------------------"; +"----------- fun Gcd_ML.eval -----------------------------------"; "----------- fun multi_to_uni ---------------------------"; "----------- fun uni_to_multi ---------------------------"; "----------- fun find_new_r ----------------------------"; @@ -578,17 +578,17 @@ if gcd_coeff_poly [(~2, [2, 0]), (5, [5, 0]),(~4, [3, 2]), (2, [2, 3])] = 1 then () else error "gcd_coeff_poly [(~2, [2, 0]), (5, [5, 0]),(~4, [3, 2]), (2, [2, 3])] = 1 changed";*) -"----------- fun eval -----------------------------------"; -"----------- fun eval -----------------------------------"; -"----------- fun eval -----------------------------------"; -if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 0 1 = [(1, [0]), (~1, [1])] then () - else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 0 1 = [(1, [0]), (~1, [1])] changed"; -if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 1 1 = [(2, [0]), (~2, [2])] then () - else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 1 1 =[(2, [0]), (~2, [2])] changed"; -if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 0 3 = [(9, [0]), (~25, [1])] then () - else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 0 3 = [(9, [0]), (~25, [1])] changed"; -if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 1 3 = [(6, [0]), (~8, [2])] then () - else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 1 3 = [ (6, [0]), (~8, [2])] changed"; +"----------- fun Gcd_ML.eval -----------------------------------"; +"----------- fun Gcd_ML.eval -----------------------------------"; +"----------- fun Gcd_ML.eval -----------------------------------"; +if Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 0 1 = [(1, [0]), (~1, [1])] then () + else error " Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 0 1 = [(1, [0]), (~1, [1])] changed"; +if Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 1 1 = [(2, [0]), (~2, [2])] then () + else error " Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 1 1 =[(2, [0]), (~2, [2])] changed"; +if Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 0 3 = [(9, [0]), (~25, [1])] then () + else error " Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 0 3 = [(9, [0]), (~25, [1])] changed"; +if Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 1 3 = [(6, [0]), (~8, [2])] then () + else error " Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 1 3 = [ (6, [0]), (~8, [2])] changed"; "----------- fun multi_to_uni ---------------------------"; "----------- fun multi_to_uni ---------------------------"; @@ -846,8 +846,8 @@ "~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, [], []); val r = find_new_r a b r; val r_list = r_list @ [r]; - val g_r = gcd_poly' (order (eval a (n - 2) r)) - (order (eval b (n - 2) r)) (n - 1) 0 + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r)) + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0 val steps = steps @ [g_r]; (*HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1] exception Div raised*) @@ -856,8 +856,8 @@ m > M = false; val r = find_new_r a b r; val r_list = r_list @ [r]; - val g_r = gcd_poly' (order (eval a (n - 2) r)) - (order (eval b (n - 2) r)) (n - 1) 0; + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r)) + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0; lex_ord (lmonom g) (lmonom g_r) = false; lexp g = lexp g_r = true; val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2); @@ -873,8 +873,8 @@ "~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, r_list, steps); val r = find_new_r a b r; val r_list = r_list @ [r]; - val g_r = gcd_poly' (order (eval a (n - 2) r)) - (order (eval b (n - 2) r)) (n - 1) 0 + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r)) + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0 val steps = steps @ [g_r]; (*HENSEL_lifting a b n M 1 r r_list steps g_r (zero_poly n) [1] exception Div raised*) @@ -883,8 +883,8 @@ m > M = false; val r = find_new_r a b r; val r_list = r_list @ [r]; - val g_r = gcd_poly' (order (eval a (n - 2) r)) - (order (eval b (n - 2) r)) (n - 1) 0; + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r)) + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0; lex_ord (lmonom g) (lmonom g_r) = false; lexp g = lexp g_r = true; val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2); @@ -900,8 +900,8 @@ "~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, r_list, steps); val r = find_new_r a b r; val r_list = r_list @ [r]; - val g_r = gcd_poly' (order (eval a (n - 2) r)) - (order (eval b (n - 2) r)) (n - 1) 0 + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r)) + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0 val steps = steps @ [g_r]; (*HENSEL_lifting a b n M 1 r r_list steps g_r (zero_poly n) [1] exception Div raised*) @@ -910,8 +910,8 @@ m > M = false; val r = find_new_r a b r; val r_list = r_list @ [r]; - val g_r = gcd_poly' (order (eval a (n - 2) r)) - (order (eval b (n - 2) r)) (n - 1) 0; + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r)) + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0; lex_ord (lmonom g) (lmonom g_r) = false; lexp g = lexp g_r = true; val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2); diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/MathEngine/mathengine-stateless.sml --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Nov 06 15:08:27 2019 +0100 @@ -334,10 +334,11 @@ val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp; if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then () else error "autoCalculate..CompleteCalc: final result"; -if terms2strs (get_assumptions_ pt p) = +if terms2strs (get_assumptions_ pt p) = [] +(* assumptions are handled by Proof.context now: ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*) "x = 1", (*result of subpbl and rootpbl*) - "precond_rootmet x"] (*precond of rootmet*) + "precond_rootmet x"] (*precond of rootmet*) *) then () else error "autoCalculate..CompleteCalc: ctxt at final result"; diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/MathEngine/solve.sml --- a/test/Tools/isac/MathEngine/solve.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/MathEngine/solve.sml Wed Nov 06 15:08:27 2019 +0100 @@ -58,8 +58,7 @@ | _ => error "solve.sml: interSteps on norm_Rational 2"; get_obj g_res pt []; val (t, asm) = get_obj g_result pt []; -if terms2str asm = "[\"8 * x \ 0\",\"-9 + x ^^^ 2 \ 0\"," ^ - "\"(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9)) is_ratpolyexp\"]" +if terms2str asm = "[]" then () else error "solve.sml: interSteps on norm_Rational 2, asms"; diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Nov 06 15:08:27 2019 +0100 @@ -38,31 +38,31 @@ val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*); member op = Solve.specsteps mI (* = false*); -loc_solve_ (mI,m) ptp ; (* assy: call by ([3], Pbl)*) + loc_solve_ (mI,m) ptp ; (* assy: call by ([3], Pbl)*) "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos)) = ((mI,m), ptp); -Solve.solve m (pt, pos); (* assy: call by ([3], Pbl)*) - (* step somewhere within a calculation *) -"~~~~~ fun solve, args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos)); -Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*); + solve m (pt, pos); (* assy: call by ([3], Pbl)*) + (* ======== general tactic as fall through ======== *) +"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos)); + (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; + val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; - locate_input_tactic sc (pt, po) (fst is) (snd is) m; (* assy: call by ([3], Pbl)*) + val Safe_Step (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*) + locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); "~~~~~ fun locate_input_tactic , args:"; val (progr, cstate, istate, ctxt, tac) = (sc, (pt, po), (fst is), (snd is), m); val srls = get_simplifier cstate; - (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*); -"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), - (Istate.Pstate (ist as {env=E,path=l,eval=rls,form_arg=a,act_arg=v,or=asap,finish=S,assoc=b}), ctxt)) - = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt)); - (*if*)l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*); + (*case*) execute_progr_2 (progr, (cstate, ctxt, tac)) istate (*of*); +"~~~~~ fun execute_progr_2 , args:"; val ((scr as Rule.Prog sc, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...}))) + = ((progr, (cstate, ctxt, tac)), istate); + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*); - assy ((pt, p), ctxt, m) (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc); -"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) - = (((pt, p), ctxt, m), (ist |> upd_path [R] |> upd_or Aundef), (Program.body_of sc)); + assy cctt (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc); +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b)))) + = (cctt, (ist |> upd_path [R] |> upd_or Aundef), (Program.body_of sc)); -val Assoc (_, _, Rewrite_Set' (_, _, _, _, _)) = (*case*) +val Assoc (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*) assy xxx (ist |> path_down [L, R]) e (*of*); "~~~~~ fun assy, args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Seq"(*1*),_) $e1 $ e2 $ a)) = (xxx, (ist |> path_down [L, R]), e); @@ -77,9 +77,9 @@ val Assoc _ = (*case*) assy xxx (ist |> path_down_form ([L, R], a)) e (*of*); (*======= end of scanning tacticals, a leaf =======*) -"~~~~~ fun assy, args:"; val (((pt, p), ctxt, tac), ist, t) = +"~~~~~ fun assy, args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) = (xxx, (ist |> path_down_form ([L, R], a)), e); -val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) (get_rls ist) (get_subst ist) t (*of*); +val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); val Ass (Rewrite_Set' _, _, _) = (*case*) associate pt ctxt (m, stac) (*of*); @@ -99,31 +99,31 @@ (*if*) member op = [Pbl, Met] p_ = false; "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); -e_metID = get_obj g_metID pt (par_pblobj pt p) = false; + e_metID = get_obj g_metID pt (par_pblobj pt p) = false; (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)(*else*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; + val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; val (_, _, _) = determine_next_tactic (thy', srls) (pt, pos) sc is; -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, ctxt)) +"~~~~~ fun determine_next_tactic , args:"; val ((ctxt, _), (ptp as (pt, p)), sc, (Istate.Pstate ist, _)) = ((thy', srls), (pt, pos), sc, is); val Appy (Rewrite_Set' _, _) = (*case*) - execute_progr_1 thy ptp sc (Istate.Pstate ist) (*of*); -"~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.Pstate ist)) - = (thy, ptp, sc, (Istate.Pstate ist)); - (*if*) 0 = length (get_path ist) (*else*); + execute_progr_1 (sc, (ptp, ctxt)) (Istate.Pstate ist) (*of*); +"~~~~~ fun execute_progr_1 , args:"; val ((sc as Rule.Prog prog, cct), (Istate.Pstate (ist as {path, ...}))) + = ((sc, (ptp, ctxt)), (Istate.Pstate ist)); + (*if*) 0 = length path (*else*); val Appy (Rewrite_Set' _, _) = - nstep_up (sc, (ptp, (fst thy))) (trans_scan_up2 ist |> upd_appy Skip_); -"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), ist) = - ((sc, (ptp, (fst thy))), (trans_scan_up2 ist |> upd_appy Skip_)); - (*if*) 1 < length (get_path ist) (*then*); + nstep_up (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_); +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...})) = + ((sc, cct), (trans_scan_up2 ist |> upd_appy Skip_)); + (*if*) 1 < length path (*then*); - nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc); + nxt_up yyy (ist |> path_up) (go_up path sc); "~~~~~ fun nxt_up , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _)) = - (yyy, (ist |> path_up), (go_up (get_path ist) sc)); + (yyy, (ist |> path_up), (go_up path sc)); (*\\--1 end step into relevant call ----------------------------------------------------------//*) @@ -158,51 +158,54 @@ val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; + val (_, _, _) = determine_next_tactic (thy', srls) (pt, pos) sc is; -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, ctxt)) +"~~~~~ fun determine_next_tactic , args:"; val ((ctxt, _), (ptp as (pt, p)), sc, (Istate.Pstate ist, _)) = ((thy', srls), (pt, pos), sc, is); val Appy (_, _) = (*case*) - execute_progr_1 thy ptp sc (Istate.Pstate ist) (*of*); -"~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.Pstate ist)) - = (thy, ptp, sc, (Istate.Pstate ist)); - (*if*) 0 = length (get_path ist) (*else*); + execute_progr_1 (sc, (ptp, ctxt)) (Istate.Pstate ist) (*of*); +"~~~~~ fun execute_progr_1 , args:"; val ((sc as Rule.Prog prog, cct), (Istate.Pstate (ist as {path, ...}))) + = ((sc, (ptp, ctxt)), (Istate.Pstate ist)); + (*if*) 0 = length path (*else*); - nstep_up (sc, (ptp, (fst thy))) (trans_scan_up2 ist |> upd_appy Skip_); -"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), ist) - = ((sc, (ptp, (fst thy))), (trans_scan_up2 ist |> upd_appy Skip_)); - (*if*) 1 < length (get_path ist) (*then*); + nstep_up (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_); +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...})) + = ((sc, cct), (trans_scan_up2 ist |> upd_appy Skip_)); + (*if*) 1 < length path (*then*); - nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc); + nxt_up yyy (ist |> path_up) (go_up path sc); "~~~~~ fun nxt_up , args:"; val (yyy, ist, (Const ("Tactical.Try"(*1*),_) $ _ )) - = (yyy, (ist |> path_up), (go_up (get_path ist) sc)); + = (yyy, (ist |> path_up), (go_up path sc)); nstep_up yyy (ist |> upd_appy Skip_); -"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), ist) +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...})) = (yyy, (ist |> upd_appy Skip_)); - (*if*) 1 < length (get_path ist) (*then*); + (*if*) 1 < length path (*then*); - nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc); + nxt_up yyy (ist |> path_up) (go_up path sc); "~~~~~ fun nxt_up , args:"; val (yyy, ist, (Const ("Tactical.Seq"(*2*), _) $ _ $ _)) - = (yyy, (ist |> path_up), (go_up (get_path ist) sc)); + = (yyy, (ist |> path_up), (go_up path sc)); nstep_up yyy ist; -"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), ist) = (yyy, ist); - (*if*) 1 < length (get_path ist) (*then*); +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...})) + = (yyy, ist); + (*if*) 1 < length path (*then*); - nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc); + nxt_up yyy (ist |> path_up) (go_up path sc); "~~~~~ fun nxt_up , args:"; val (yyy, ist, (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _)) - = (yyy, (ist |> path_up), (go_up (get_path ist) sc)); + = (yyy, (ist |> path_up), (go_up path sc)); nstep_up yyy ist; -"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), ist) = (yyy, ist); - (*if*) 1 < length (get_path ist) (*then*); +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...})) + = (yyy, ist); + (*if*) 1 < length path (*then*); - nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc); -"~~~~~ fun nxt_up , args:"; val ((yyy as (Rule.Prog sc, xxx)), ist, (Const ("HOL.Let"(*1*), _) $ _)) - = (yyy, (ist |> path_up), (go_up (get_path ist) sc)); - (*if*) get_fini ist = Napp_ (*else*); - val (i, body) = check_Let_up (get_path ist) sc; + nxt_up yyy (ist |> path_up) (go_up path sc); +"~~~~~ fun nxt_up , args:"; val ((yyy as (Rule.Prog sc, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _)) + = (yyy, (ist |> path_up), (go_up path sc)); + (*if*) finish = Napp_ (*else*); + val (i, body) = check_Let_up ist sc; (*case*) appy xxx (ist |> path_up_down [R, D] |> upd_env' i) body (*of*); "~~~~~ fun appy , args:"; val (xxx, ist, (Const ("HOL.Let"(*1*),_) $ e $ (Abs (i,T,b)))) @@ -211,9 +214,9 @@ val Appy (Subproblem' _, _) = (*case*) appy xxx (ist |> path_down [L, R]) e (*of*); (*========== a leaf has been found ==========*) -"~~~~~ fun appy , args:"; val (((pt, p), ctxt), ist, t) +"~~~~~ fun appy , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t) = (xxx, (ist |> path_down [L, R]), e); - val (a', STac stac) = (*case*) Lucin.handle_leaf "next " ctxt (get_rls ist) (get_subst ist) t (*of*); + val (a', STac stac) = (*case*) Lucin.handle_leaf "next " ctxt eval (get_subst ist) t (*of*); (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy ctxt) stac; "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags')) diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Minisubpbl/300-init-subpbl.sml --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Nov 06 15:08:27 2019 +0100 @@ -40,67 +40,64 @@ locate_input_tactic sc (pt, po) (fst is) (snd is) m; "~~~~~ fun locate_input_tactic , args:"; val (progr, cstate, istate, ctxt, tac) = (sc, (pt, po), (fst is), (snd is), m); - val srls = get_simplifier cstate; - (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*); -"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt)) - = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt)); - (*if*)l = [] orelse ((*init.in solve..Apply_Method...*) - (last_elem o fst) p = 0 andalso snd p = Res) (*else*); -(*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) = - (astep_up (thy',srls,scr,d) ((E,l,a,v,asap,S,b), [(m,EmptyMout,pt,p,[])]) );*) -"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,asap,S,b),ss)) - = ((ctxt,srls,scr, (pt, p)), ((E,l,a,v,asap,S,b), m)); - (*if*) 1 < length l (*true*); -val up = drop_last l; + val Assoc (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*) + execute_progr_2 (progr, (cstate, ctxt, tac)) istate (*of*); +"~~~~~ fun execute_progr_2 , args:"; val ((scr as Rule.Prog sc, (cctt as ((_, p), _, _))), + (Istate.Pstate (ist as {path, ...}))) + = ( (progr, (cstate, ctxt, tac)), istate); + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*); - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc); -"~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Tactical.Try",_) $ e)) = - (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc)); - astep_up ysa iss; -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss); - (*if*) 1 < length l; (*then*) - val up = drop_last l; + astep_up (scr, cctt) ist; +"~~~~~ and astep_up, args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...})) + = ((scr, cctt), ist); + (*if*) 1 < length path (*true*); - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc); -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ )) = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc)); + ass_up yyy (ist |> path_up) (go (path_up' path) sc); +"~~~~~ fun ass_up, args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _)) + = (yyy, (ist |> path_up), (go (path_up' path) sc)); - astep_up ysa iss (*2*: comes from e2*); -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss); - (*if*) 1 < length l; (*then*) - val up = drop_last l; + astep_up yyy ist; +"~~~~~ and astep_up, args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...})) + = (yyy, ist); + (*if*) 1 < length path (*true*); - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc); -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc)); + ass_up yyy (ist |> path_up) (go (path_up' path) sc); +"~~~~~ fun ass_up , args:"; val (yyy, ist, (Const ("Tactical.Seq"(*2*), _) $ _ $ _)) + = (yyy, (ist |> path_up), (go (path_up' path) sc)); - astep_up ysa iss (*all has been done in (*2*) below*); -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss); - (*if*) 1 < length l; (*then*) - val up = drop_last l; + astep_up yyy ist (*2*: comes from e2*); +"~~~~~ and astep_up, args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...})) + = (yyy, ist); + (*if*) 1 < length path (*true*); - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc); -"~~~~~ fun ass_up , args:"; val ((ys as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,asap,S,b),ss), (Const ("HOL.Let",_) $ _)) - = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc)); - val l = drop_last l; (*comes from e, goes to Abs*) - val (i, T, body) = - (case go l sc of - Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (i, T, body) - | t => error ("ass_up..HOL.Let $ _ with " ^ Rule.term2str t)) - val i = TermC.mk_Free (i, T); - val E = Env.upd_env E (i, v); + ass_up yyy (ist |> path_up) (go (path_up' path) sc); +"~~~~~ fun ass_up , args:"; val (yyy, ist, (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _)) + = (yyy, (ist |> path_up), (go (path_up' path) sc)); - (*case*) assy (ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], rls,a,v,asap,S,b),ss) body (*of*); -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) - = ((ctxt,s,d,Aundef), ((E, l @ [Celem.R, Celem.D], rls,a,v,asap,S,b),ss), body); + astep_up yyy ist (*all has been done in (*2*) below*); +"~~~~~ and astep_up, args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...})) + = (yyy, ist); + (*if*) 1 < length path (*true*); - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), ss) e (*of*); + ass_up yyy (ist |> path_up) (go (path_up' path) sc); +"~~~~~ fun ass_up , args:"; val ((yyy as (prog as Rule.Prog p, xxx as (cstate, _, _))), ist, (Const ("HOL.Let"(*1*), _) $ _)) + = ( yyy, (ist |> path_up), (go (path_up' path) sc)); + val (i, body) = check_Let_up ist p +; + (*case*) assy xxx (ist |> path_up_down [R, D] |> upd_env' i |> upd_or Aundef) body (*of*); +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b)))) + = (xxx, (ist |> path_up_down [R, D] |> upd_env' i |> upd_or Aundef), body); + + (*case*) assy xxx (ist |> path_down [L, R]) e (*of*); (*======= end of scanning tacticals, a leaf =======*) -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t) - = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), ss), e); +"~~~~~ fun assy , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) + = (xxx, (ist |> path_down [L, R]), e); -(*val (a', STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*); +val (NONE, STac _) = (*case*) + handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t) - = ("locate", "Isac_Knowledge", sr, (E, (a, v)), t); + = ("locate", (Context.theory_name (Rule.Isac"")), eval, (get_subst ist), t); val (a', STac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*); "~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _))) diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Nov 06 15:08:27 2019 +0100 @@ -36,51 +36,51 @@ (*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''', p''', [], pt'''); - val ("ok", (_, _, (pt'''', p''''))) = - (*case*) locatetac tac (pt, p) (*of*); + val ("ok", (_, _, (pt'''', p''''))) = (*case*) + + locatetac tac (pt, p) (*of*); "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); val (mI,m) = mk_tac'_ tac; val Appl m = (*case*) applicable_in p pt m (*of*); member op = specsteps mI; (*else*) - loc_solve_ (mI, m) ptp; + loc_solve_ (mI, m) ptp; "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = ((mI, m), ptp); solve m (pt, pos); "~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _)))) = (m, (pt, pos)); - val {srls, ...} = get_met mI; - val PblObj {meth=itms, ...} = get_obj I pt p; - val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; - val thy' = get_obj g_domID pt p; - val thy = assoc_thy thy'; - val srls = Lucin.get_simplifier (pt, pos) - val (is as Pstate (env,_,_,_,_,_,_,_), ctxt, sc) = init_pstate srls ctxt itms mI; - (*dont take ctxt ^^^ from ^^^^^^^^^^^^^*) + val itms = case get_obj I pt p of + PblObj {meth=itms, ...} => itms + | _ => error "solve Apply_Method: uncovered case get_obj" + val thy' = get_obj g_domID pt p; + val thy = Celem.assoc_thy thy'; + val srls = Lucin.get_simplifier (pt, pos) + val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of + (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc) + | _ => error "solve Apply_Method: uncovered case init_pstate" (*+*)val (pt, p) = case locatetac tac (pt, pos) of ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac"; (*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; - "~~~~~ from solve to..to me return"; val (pt, p) = (pt'''', p''''); - (*case*) step p ((pt, e_pos'), []) (*of*); + val ("ok", ([(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), _, (_, (Pstate _, _)))], _, _)) = (*case*) + step p ((pt, e_pos'), []) (*of*); "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p'''', ((pt'''', e_pos'), [])) val pIopt = get_pblID (pt,ip); tacis; (*= []*) member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) -"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); + +"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), - (Pstate (ist as (E,l,rls,a,v,asap,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is); + +"~~~~~ fun determine_next_tactic , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*))) + = ((thy',srls), (pt,pos), sc, is); (*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; - -(*+*)val Appy (xxx, _) = appy thy ptp ist body; -(*+*)if l = [] andalso tac_2str xxx = "Rewrite_Set_Inst' " -then () else error "Minisubpbl/400-start-meth-subpbl changed -1"; (*\\--1 end step into relevant call ----------------------------------------------------------//*) val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*nxt = Rewrite_Set_Inst isolate_bdv*); diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Nov 06 15:08:27 2019 +0100 @@ -33,46 +33,52 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*); val (pt''''', p''''') = (pt, p); -"~~~~~ fun me, args:"; val (_,tac) = nxt; +"~~~~~ fun me , args:"; val (_,tac) = nxt; val (pt, p) = case locatetac tac (pt,p) of ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac"; val (pt'''', p'''') = (pt, p); -"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) +"~~~~~ fun step , args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*) -tacis; (*= []*) -val SOME pI = pIopt; -member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) -"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); + (*if*) tacis; (*= []*) + val SOME pI = pIopt; + (*if*) member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) + +"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) -val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is; -;tac_; (* = Check_Postcond' *) +val (tac_,is, (t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is; + +(*+*);tac_; (* = Check_Postcond' *) + "~~~~~ fun begin_end_prog, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) = (tac_, is, ptp); - val pp = par_pblobj pt p - val asm = - (case get_obj g_tac pt p of - Check_elementwise _ => (*collects and instantiates asms*) - (snd o (get_obj g_result pt)) p - | _ => get_assumptions_ pt (p,p_)) - handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*) - val metID = get_obj g_metID pt pp; - val {srls=srls,scr=sc,...} = get_met metID; - val loc as (Pstate (E,l,rls,a,_,_,_,b), ctxt) = get_loc pt (p,p_); - val thy' = get_obj g_domID pt pp; - val thy = assoc_thy thy'; - val (_,_,(scval,scsaf)) = determine_next_tactic (thy',srls) (pt,(p,p_)) sc loc; -;pp = []; (*false*) - val ppp = par_pblobj pt (lev_up p); - val thy' = get_obj g_domID pt ppp; - val thy = assoc_thy thy'; - val metID = get_obj g_metID pt ppp; - val {scr,...} = get_met metID; - val (Pstate (E,l,rls,a,_,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm) - val ctxt'' = from_subpbl_to_caller ctxt scval ctxt' - val tac_ = Check_Postcond' (pI, (scval, asm)) - val is = Pstate (E,l,rls,a,scval,asap,Istate.Skip_,b); + val pp = par_pblobj pt p + val asm = (case get_obj g_tac pt p of + Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*) + | _ => get_assumptions_ pt (p, p_)) + val metID = get_obj g_metID pt pp; + val {srls = srls, scr = sc, ...} = Specify.get_met metID; + val (loc, pst, ctxt) = case get_loc pt (p, p_) of + loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt) + | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc" + val thy' = get_obj g_domID pt pp; + val thy = Celem.assoc_thy thy'; + val (_, _, (scval, _)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc; + + (*if*) pp = []; (*false*) + + val ppp = par_pblobj pt (lev_up p); + val thy' = get_obj g_domID pt ppp; + val thy = Celem.assoc_thy thy'; + + val (pst', ctxt') = case get_loc pt (pp, Frm) of + (Istate.Pstate pst', ctxt') => (pst', ctxt') + | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc" + val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt' + val tac_ = Tactic.Check_Postcond' (pI, (scval, asm)) + val is = Istate.Pstate (pst' |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_) +; "~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) = (thy, tac_, (is, ctxt''), (pp, Res), pt); val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete; diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Nov 06 15:08:27 2019 +0100 @@ -52,35 +52,46 @@ val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*) tacis; (*= []*) member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) -"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); -val thy' = get_obj g_domID pt (par_pblobj pt p); -val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) -"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), -(Pstate (E,l,rls,a,v,asap,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); -val ctxt = get_ctxt pt pos -val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; -l; (*= [R, R, D, L, R]*) -"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = -(thy, ptp, sc, E, l, Skip_, a, v); -1 < length l; (*true*) -val up = drop_last l; -go up sc; (* = Const ("HOL.Let", *) -"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay, -(t as Const ("HOL.Let",_) $ _), a, v) = -(thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v); -ay = Napp_; (*false*) -val up = drop_last l; -val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; -val i = mk_Free (i, T); -val E = Env.upd_env E (i, v); -body; (*= Const ("Prog_Tac.Check'_elementwise"*) -"~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)= -(thy, ptp, E, (up@[R,D]), body, a, v); -handle_leaf "next " th sr (E, (a, v)) t; (*= (NONE, STac (Const ("Prog_Tac.Check'_elementwise"*) -val (a', STac stac) = handle_leaf "next " th sr (E, (a, v)) t; -"~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Prog_Tac.Check'_elementwise",_) $ _ $ -(set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac); -(*2011 changed ^^^^^ *) +"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); + (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); + val thy' = get_obj g_domID pt (par_pblobj pt p); + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; + + val (Check_elementwise' _, (Pstate _, _), _) = + determine_next_tactic (thy', srls) (pt, pos) sc is; +"~~~~~ fun determine_next_tactic , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*))) + = ((thy', srls), (pt, pos), sc, is); + + (*case*) + execute_progr_1 (sc, (ptp, thy)) (Istate.Pstate ist) (*of*); +"~~~~~ fun execute_progr_1 , args:"; val ((sc as Rule.Prog prog, cct), (Istate.Pstate (ist as {path, ...}))) + = ((sc, (ptp, thy)), (Istate.Pstate ist)); + (*if*) 0 = length path (*else*); + + nstep_up (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_); +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...})) + = ((sc, cct), (trans_scan_up2 ist |> upd_appy Skip_)); + (*if*) 1 < length path (*then*); + + nxt_up yyy (ist |> path_up) (go_up path sc); +"~~~~~ fun nxt_up , args:"; val ((yyy as (Rule.Prog sc, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _)) + = (yyy, (ist |> path_up), (go_up path sc)); + (*if*) finish = Napp_ (*else*); + val (i, body) = check_Let_up ist sc; + + (*case*) + appy xxx (ist |> path_up_down [R, D] |> upd_env' i) body (*of*); + (*========== a leaf has been found ==========*) +"~~~~~ fun appy , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t) + = (xxx, (ist |> path_up_down [R, D] |> upd_env' i), body); + val (a', STac stac) = (*case*) + handle_leaf "next " ctxt eval (get_subst ist) t; + + val (Check_elementwise "Assumptions", Empty_Tac_) = + stac2tac_ pt (Celem.assoc_thy ctxt) stac; +"~~~~~ fun stac2tac_ , args:"; val (pt, thy, (Const("Prog_Tac.Check'_elementwise",_) $ _ $ + (set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) + = (pt, (assoc_thy th), stac); val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*) case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Minisubpbl/700-interSteps.sml --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Nov 06 15:08:27 2019 +0100 @@ -41,12 +41,14 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; + if p = ([], Res) then case nxt of ("End_Proof'", End_Proof') => () | _ => error "calculation not finished correctly 1" else error "calculation not finished correctly 2"; show_pt pt; (* 11 lines with subpbl *) ; + "----- no thy-context at result -----"; (** val p = ([], Res); ** initContext 1 Thy_ p @@ -99,18 +101,19 @@ show_pt pt'; (* cut ctree after ([3,1,1], Frm) *) -(* val (_,_, (pt'', _)) =*) complete_solve CompleteSubpbl [] (pt', pos') -; + complete_solve CompleteSubpbl [] (pt', pos'); "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_, p_)))) = (CompleteSubpbl, [], (pt', pos')); (*if*) p = ([], Res) (* = false*); (*if*) member op = [Pbl,Met] p_ (* = false*); -(*case*) do_solve_step ptp (*of*) -; -"~~~~~ and do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (ptp); -(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false isabisac = ?*); + +val ([(Rewrite_Inst (["(''bdv'', x)"], ("risolate_bdv_add", _)), _, _)], _, _) = (*case*) + do_solve_step ptp (*of*); +"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (ptp); + (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false isabisac = ?*); val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; + val (srls, is, sc) = + from_pblobj_or_detail' thy' (p,p_) pt; "~~~~~ fun from_pblobj_or_detail' , args:"; val (_, (p, p_), pt) = (thy', (p,p_), pt); (*if*) member op = [Pbl, Met] p_ (*else*); val (pbl, p', rls') = par_pbl_det pt p; @@ -120,47 +123,49 @@ (*+*)id_rls rls' = "isolate_bdv"; "~~~~~ from from_pblobj_or_detail' to do_solve_step return val:"; val () = (); -(* val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is; -; -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), - (Istate.Pstate (ist as (E,l,rls,a,v,asap,s,_)), ctxt)) = ((thy', srls), (pt, pos), sc, is); -(*if*) l = [] (* = true *); - appy thy ptp ist body; -"~~~~~ fun appy , args:"; val (thy, ptp, E, l, (Const ("Tactical.Repeat"(*2*),_) $ e), a, v) = -(thy, ptp, E, [Celem.R], body, NONE, v); + val (Rewrite_Inst' (_, _, _, _, _, ("risolate_bdv_add", _), _, _), is, (t, _)) = + determine_next_tactic (thy', srls) (pt, pos) sc is; +"~~~~~ fun determine_next_tactic , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*))) + = ((thy', srls), (pt, pos), sc, is); - appy thy ptp ist e; -"~~~~~ fun appy , args:"; val (thy, ptp, ist, (Const ("Tactical.Seq"(*1*),_) $ e1 $ e2 $ a)) = - (thy, ptp, ist, e); + (*case*) + execute_progr_1 (sc, (ptp, thy)) (Istate.Pstate ist) (*of*); +"~~~~~ fun execute_progr_1 , args:"; val ((sc as Rule.Prog prog, cct), (Istate.Pstate (ist as {path, ...}))) + = ((sc, (ptp, thy)), (Istate.Pstate ist)); + (*if*) 0 = length path (*else*); - (*case*) appy thy ptp (ist |> path_down_form ([L, L, R], a)) e1 (*of*); -"~~~~~ fun appy , args:"; val (thy, ptp, ist, (Const ("Tactical.Try"(*2*),_) $ e)) = - (thy, ptp, (ist |> path_down_form ([L, L, R], a)), e1); + nstep_up (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_); +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...}) ) + = ((sc, cct), (trans_scan_up2 ist |> upd_appy Skip_)); + (*if*) 1 < length path (*then*); - (*case*) appy thy ptp (ist |> path_down [R]) e (*of*); -"~~~~~ fun appy , args:"; val (thy, ptp, ist, (Const ("Tactical.Repeat"(*2*),_) $ e)) = - (thy, ptp, (ist |> path_down [R]), e); + nxt_up yyy (ist |> path_up) (go_up path sc); +"~~~~~ fun nxt_up , args:"; val ((yyy as (_, xxx)), ist, (Const ("Tactical.Repeat"(*2*), _) $ e)) + = (yyy, (ist |> path_up), (go_up path sc)); + (*case*) + appy xxx (ist |> path_down [R]) e (*of*); (*========== a leaf has been found ==========*) - appy thy ptp (ist |> path_down [R]) e; -"~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v) = - (thy, ptp, E, (l @ [Celem.R]), e, a, v); +"~~~~~ fun appy , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t) + = (xxx, (ist |> path_down [R]), e); val (a', STac stac) = (*case*) handle_leaf "next " th sr (get_subst ist) t (*of*); -"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (get_subst ist), t); +"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t) + = ("next ", th, sr, (get_subst ist), t); + (*+*)val [(Free ("t_t", Tt_t), Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("-1", _) $ Free ("x", _)) $ Free ("0", _)), (Free ("v", Tv), Free ("x", Tx))] = E (* THE WRONG TYPES IN E ..(TODO.4)*) (*+*)val TFree ("'z", ["HOL.type"]) = Tt_t; -(*+*)val Type ("Real.real",[]) = Tv; -(*+*)val Type ("Real.real",[]) = Tx; +(*+*)val Type ("Real.real", []) = Tv; +(*+*)val Type ("Real.real", []) = Tx; (*+*)val SOME (Const ("empty", Ta)) = a; -(*+*)val Type ("'a",[]) = Ta; -(*+*)val Const ("empty", Tv) = v; -(*+*)val Type ("'a",[]) = Tv; +(*+*)val Type ("'a", []) = Ta; +(*+*)if term2str v = "x = 0 + -1 * -1" then () else error "handle_leaf changed"; +(*+*)val Type ("Real.real", []) = Tv; (*case*) Prog_Tac.subst_stacexpr E a v t (*of*); "~~~~~ fun subst_stacexpr , args:"; val (E, a, v, (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _))) diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Minisubpbl/790-complete.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Minisubpbl/790-complete.sml Wed Nov 06 15:08:27 2019 +0100 @@ -0,0 +1,47 @@ +(* Title: "Minisubpbl/799-complete.sml" + Author: Walther Neuper 1105 + (c) copyright due to lincense terms. +*) +"----------- Minisubpbl/799-complete.sml -------------------------"; +"----------- Minisubpbl/799-complete.sml -------------------------"; +"----------- Minisubpbl/799-complete.sml -------------------------"; + val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; + val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"], + ["Test","squ-equ-test-subpbl1"]); + val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*); + (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*) + (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*) + (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*) + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*) + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*) + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*) + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*) + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*) + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*) + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*) + (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*) + (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*) + (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*) + (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*) + (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*) + (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*) + (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*) + + (* final test ...*) + if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'" + andalso pr_ctree pr_short pt = + ". ----- pblobj -----\n" ^ + "1. x + 1 = 2\n" ^ + "2. x + 1 + -1 * 2 = 0\n" ^ + "3. ----- pblobj -----\n" ^ + "3.1. -1 + x = 0\n" ^ + "3.2. x = 0 + -1 * -1\n" ^ + "4. [x = 1]\n" + then () else error "re-build: fun locate_input_tactic changed"; diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Minisubpbl/791-complete-NEXT_STEP.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/Minisubpbl/791-complete-NEXT_STEP.sml Wed Nov 06 15:08:27 2019 +0100 @@ -0,0 +1,59 @@ +(* Title: "Minisubpbl/791-complete-NEXT_STEP.sml" + Author: Walther Neuper 1105 + (c) copyright due to lincense terms. +*) + +"----------- Minisubpbl/791-complete-NEXT_STEP.sml --------------------------------------------"; +"----------- Minisubpbl/791-complete-NEXT_STEP.sml --------------------------------------------"; +"----------- Minisubpbl/791-complete-NEXT_STEP.sml --------------------------------------------"; + +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; +val (dI',pI',mI') = + ("Test", ["sqroot-test","univariate","equation","test"], + ["Test","squ-equ-test-subpbl1"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);(*Model_Problem*) +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);(*Specify_Theory*) +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*) +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*) +(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*) +(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*) +(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) =(**) step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*) +(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*) +(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Model_Problem*) +(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Theory "Test"*) +(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*) +(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*) +(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*) +(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*) +(*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*) +(*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*) + +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[]";(*isa*) +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[\"matches (?a = ?b) (-1 + x = 0)\"]";(*REP*) +(* there are questionable assumptions either ---------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) + +(*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*) + +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[]";(*isa*) +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[\"precond_rootmet 1\"]";(*REP*) + +(*[], Res*)val ("ok", ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*) + +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[]";(*isa*) +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[\"precond_rootmet 1\"]";(*REP*) + +(*[], Res*)val ("end-of-calculation", ([], _, (pt, p))) = step p ((pt, e_pos'), []);(**) + +(*/--------------------- final test ----------------------------------\\*) +val (res, asm) = (get_obj g_result pt (fst p)); + +if term2str res = "[x = 1]" andalso terms2str asm = "[]" +then () else error "Minisubpbl/791-complete-NEXT_STEP.sml, determine_next_tactic CHANGED"; + +if p = ([], Und) +then + case get_obj g_tac pt (fst p) of + Apply_Method ["Test", "squ-equ-test-subpbl1"] => () + | _ => error "Minisubpbl/791-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 2" +else error "Minisubpbl/791-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 1" diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/OLDTESTS/root-equ.sml --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Nov 06 15:08:27 2019 +0100 @@ -28,7 +28,7 @@ (* > val t = (Thm.term_of o the o (parse thy)) "#2^^^#3"; -> val eval_fn = the (assoc (!eval_list, "pow")); +> val eval_fn = the (LibraryC.assoc (!eval_list, "pow")); > val (SOME (id,t')) = get_pair thy "pow" eval_fn t; > Syntax.string_of_term (thy2ctxt thy) t'; *) diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/ProgLang/calculate.sml --- a/test/Tools/isac/ProgLang/calculate.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/ProgLang/calculate.sml Wed Nov 06 15:08:27 2019 +0100 @@ -121,7 +121,7 @@ ie. cancel does not work properly *) val thy = @{theory "Test"}; - val op_ = the (assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE")); + val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE")); val ct = numbers_to_string @{term "sqrt (x ^^^ 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"}; case calculate_ thy op_ ct of @@ -247,32 +247,32 @@ val thy = @{theory Test}; val t = (Thm.term_of o the o (parse thy)) "12 / 3"; -val SOME (thmID,thm) = adhoc_thm thy(the(assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t; +val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; "12 / 3 = 4"; val thy = @{theory Test}; val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2"; -val SOME (thmID,thm) = adhoc_thm thy(the(assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t; +val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; "4 ^ 2 = 16"; val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; - val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; + val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; "1 + 2 = 3"; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; "(3 * 4 / 3) ^^^ 2"; - val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t; + val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t; "3 * 4 = 12"; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; "(12 / 3) ^^^ 2"; - val SOME (thmID,thm) =adhoc_thm thy(the(assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t; + val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t; "12 / 3 = 4"; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; "4 ^^^ 2"; - val SOME (thmID,thm) = adhoc_thm thy(the(assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t; + val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t; "4 ^^^ 2 = 16"; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; @@ -283,10 +283,10 @@ (*13.9.02 *** calc: operator = pow not defined*) val t = (Thm.term_of o the o (parse thy)) "3^^^2"; val SOME (thmID,thm) = - adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t; + adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t; (*** calc: operator = pow not defined*) - val (op_, eval_fn) = the (assoc(KEStore_Elems.get_calcs @{theory},"POWER")); + val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")); (* val op_ = "Prog_Expr.pow" : string val eval_fn = fn : string -> term -> theory -> (string * term) option*) @@ -333,7 +333,7 @@ "----------- fun get_pair: examples ------------------------------------------------------------"; "----------- fun get_pair: examples ------------------------------------------------------------"; val thy = @{theory}; -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "PLUS"); +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS"); val t = (Thm.term_of o the o (parse thy)) "3 + 4"; val SOME (str, term) = get_pair thy isa_str eval_fn t; @@ -355,14 +355,14 @@ if str = "#: 3 + (4 + a) = 7 + a" andalso term2str term = "3 + (4 + a) = 7 + a" then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed"; -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"); +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"); val t = (Thm.term_of o the o (parse thy)) "-4 / -2"; val SOME (str, term) = get_pair thy isa_str eval_fn t; if str = "#divide_e-4_-2" andalso term2str term = "-4 / -2 = 2" then () else error "get_pair -4 / -2 changed"; -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "POWER"); +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER"); val t = (Thm.term_of o the o (parse thy)) "2 ^^^ 3"; val SOME (str, term) = get_pair thy isa_str eval_fn t; @@ -373,7 +373,7 @@ "----------- fun adhoc_thm: examples -----------------------------------------------------------"; "----------- fun adhoc_thm: examples -----------------------------------------------------------"; (*--------------------------------------------------------------------vvvvvvvvvv*) -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "is_const"); +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const"); val SOME t = parseNEW @{context} "9 is_const"; val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; if str = "#is_const_9_" andalso thm2str thm = "(9 is_const) = True" @@ -383,7 +383,7 @@ case assoc_calc thy "Orderings.ord_class.less" of "le" => () | _ => error "Orderings.ord_class.less <-> le changed"; (*--------------------------------------------------------------------vvvvvvvvvv*) -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "le"); +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le"); val SOME t = parseNEW @{context} "4 < 4"; val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; @@ -396,14 +396,14 @@ (*--------------------------------------------------------------------vvvvvvvvvv*) -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "PLUS"); +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS"); val SOME t = parseNEW @{context} "1 + 2"; val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; if str = "#: 1 + 2 = 3" andalso thm2str thm = "1 + 2 = 3" then () else error "adhoc_thm 1 + 2 changed"; (*--------------------------------------------------------------------vvvvvvvvvv*) -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"); +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"); val SOME t = parseNEW @{context} "6 / -8"; val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; if str = "#divide_e6_-8" andalso thm2str thm = "6 / -8 = -3 / 4" @@ -413,7 +413,7 @@ case assoc_calc thy "Prog_Expr.ident" of "ident" => () | _ => error "Prog_Expr.ident <-> ident changed"; (*--------------------------------------------------------------------vvvvvvvvvv*) -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "ident"); +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident"); val SOME t = parseNEW @{context} "3 =!= 3"; val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Specify/calchead.sml --- a/test/Tools/isac/Specify/calchead.sml Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Specify/calchead.sml Wed Nov 06 15:08:27 2019 +0100 @@ -601,9 +601,9 @@ (*[x+1=2, x] OLD: [x+1=2, x] : term list*) vars' ~~ vals; (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*) -(assoc (vars'~~vals, cy')); +(LibraryC.assoc (vars'~~vals, cy')); (*SOME (Free ("x", "Real.real")) : term option*) - val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext; + val cy_ext = (free2str o the) (LibraryC.assoc (vars'~~vals, cy'))^"_"^ext; (*x_i*) "-----------------continue step through code match_ags---"; val cy' = map (cpy_nam pbt' oris') cy; diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Test_Isac.thy Wed Nov 06 15:08:27 2019 +0100 @@ -54,7 +54,7 @@ "~~~~~ from xxx to yyy return val:"; val () = (); (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); "xx" -^ "xxx" (*+*) +^ "xxx" (*+*) (*isa*) (*REP*) \ section \Run the tests\ text \ @@ -193,7 +193,8 @@ ML_file "Minisubpbl/530-error-Check_Elementwise.sml" ML_file "Minisubpbl/600-postcond.sml" ML_file "Minisubpbl/700-interSteps.sml" - ML_file "Minisubpbl/799-complete.sml" + ML_file "Minisubpbl/790-complete.sml" + ML_file "Minisubpbl/791-complete-NEXT_STEP.sml" subsection \further functionality alongside batch build sequence\ ML_file "MathEngBasic/model.sml" diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Nov 06 15:08:27 2019 +0100 @@ -193,7 +193,8 @@ ML_file "Minisubpbl/530-error-Check_Elementwise.sml" ML_file "Minisubpbl/600-postcond.sml" ML_file "Minisubpbl/700-interSteps.sml" - ML_file "Minisubpbl/799-complete.sml" + ML_file "Minisubpbl/790-complete.sml" + ML_file "Minisubpbl/791-complete-NEXT_STEP.sml" subsection \further functionality alongside batch build sequence\ ML_file "MathEngBasic/model.sml" @@ -212,6 +213,7 @@ ML_file "Interpret/script.sml" ML_file "Interpret/inform.sml" ML_file "Interpret/lucas-interpreter.sml" + ML_file "MathEngine/solve.sml" ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*) ML_file "MathEngine/messages.sml" diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Test_Some.thy Wed Nov 06 15:08:27 2019 +0100 @@ -79,596 +79,15 @@ "~~~~~ fun xxx , args:"; val () = (); \ -section \===============--- test/../lucas-interpreter.sml ----================\ +section \===================================================================================\ ML \ "~~~~~ fun xxx , args:"; val () = (); \ ML \ -(* Title: "Interpret/lucas-interpreter.sml" - Author: Walther Neuper - (c) due to copyright terms -*) - -"-----------------------------------------------------------------------------------------------"; -"table of contents -----------------------------------------------------------------------------"; -"-----------------------------------------------------------------------------------------------"; -"----------- Take as 1st stac in program -------------------------------------------------------"; -"----------- re-build: fun locate_input_tactic -------------------------------------------------"; -"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------"; -"----------- re-build: fun determine_next_tactic -----------------------------------------------"; -"----------- re-build: fun locate_input_formula ------------------------------------------------"; -"-----------------------------------------------------------------------------------------------"; -"-----------------------------------------------------------------------------------------------"; -"-----------------------------------------------------------------------------------------------"; - -"----------- Take as 1st stac in program -------------------------------------------------------"; -"----------- Take as 1st stac in program -------------------------------------------------------"; -"----------- Take as 1st stac in program -------------------------------------------------------"; -val p = e_pos'; val c = []; -val (p,_,f,nxt,_,pt) = - CalcTreeTEST - [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"], - ("Integrate", ["integrate","function"], ["diff","integration"]))]; -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -case nxt of (_, Apply_Method ["diff", "integration"]) => () - | _ => error "integrate.sml -- me method [diff,integration] -- spec"; -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")"; - -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); -val (mI,m) = mk_tac'_ tac; -val Appl m = applicable_in p pt m; -member op = specsteps mI (*false*); -"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = ((mI,m), ptp); -"~~~~~ fun solve , args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) = - (m, (pt, pos)); -val {srls, ...} = get_met mI; - val PblObj {meth=itms, ...} = get_obj I pt p; - val thy' = get_obj g_domID pt p; - val thy = assoc_thy thy'; - val srls = Lucin.get_simplifier (pt, pos) - val (is as Istate.Pstate (ist as {env, ...}), ctxt, sc) = init_pstate srls ctxt itms mI; - val ini = init_form thy sc env; - val p = lev_dn p; - - val NONE = (*case*) ini (*of*); - val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt); - val d = e_rls (*FIXME: get simplifier from domID*); -\ ML \ -val Safe_Step _ = (*case*) - locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*); -\ ML \ -"~~~~~ fun locate_input_tactic , args:"; val ((progr as Rule.Prog _), cstate, istate, ctxt, tac) = - (sc, (pt, (p, Res)), is', ctxt', m'); - -\ ML \ -(*val Assoc ((ist as {assoc, ...}), ctxt, tac') = ( *case*) - execute_progr_2 Rule.e_rls tac cstate (progr, Rule.e_rls) (istate, ctxt) (*of*); -\ ML \ -"~~~~~ fun execute_progr_2 , args:"; val () = (); -\ ML \ -\ ML \ -\ ML \ -val thy = assoc_thy thy'; -l = [] orelse ((*init.in solve..Apply_Method...*) - (last_elem o fst) p = 0 andalso snd p = Res); (*true*) -\ ML \ -\ ML \ -"~~~~~ fun assy, args:"; val (ya, (is as (E,l,rls,a,v,asap,S,b),ss), - (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) = - ((thy',ctxt,srls,d,Aundef), ((E,[R],rls,a,v,asap,S,b), [(m,EmptyMout,pt,p,[])]), body); - (*check: true*) term2str e = "Take (Integral f_f D v_v)"; -\ ML \ -\ ML \ -"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,rls,a,v,asap,S,b), (m,_,pt,(p,p_),c)::ss), t) = - (ya, ((E , l@[L,R], rls,a,v,asap,S,b),ss), e); -val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t; -(* val ctxt = get_ctxt pt (p,p_) -exception PTREE "get_obj: pos = [0] does not exist" raised -(line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*) - - -"----------- re-build: fun locate_input_tactic -------------------------------------------------"; -"----------- re-build: fun locate_input_tactic -------------------------------------------------"; -"----------- re-build: fun locate_input_tactic -------------------------------------------------"; -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*); -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*) - -(*// relevant call --------------------------------------------------------------------------\\*) -(*[1], Res* )val (*** )xxx( ***) (p,_,f,nxt,_,pt) =*) me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*) - -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt); - - (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*) locatetac tac (pt,p) (*of*); -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); - val (mI, m) = Solve.mk_tac'_ tac; - val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*); - (*if*) member op = Solve.specsteps mI; (*else*) - - (** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ (mI,m) ptp; -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp); - - (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Solve.solve m (pt, pos); -"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos)); -(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_)); - (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*) - val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, is, sc) = Lucin.from_pblobj' thy' (p,p_) pt; - - locate_input_tactic sc (pt, po) (fst is) (snd is) m; -"~~~~~ fun locate_input_tactic , args:"; val (progr, cstate, istate, ctxt, tac) - = (sc, (pt, po), (fst is), (snd is), m); - val srls = get_simplifier cstate; - - (** )val Assoc ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **) - (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*); -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt)) - = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt)); - (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*); - - (** )val xxxxx_xx = ( **) - assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],rls,a,v,asap,S,b), m) (Program.body_of sc); -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,asap,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) - = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],a,v,asap,S,b), m), (Program.body_of sc)); - - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac) e (*of*); -"~~~~~ fun xxx , args:"; val (ya, ((E,l,rls,_,v,asap,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $ e1 $ e2 $ a)) - = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac), e); - - (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,asap,S,b),ss) e1 (*of*); -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e)) - = (ya, ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,asap,S,b),ss), e1); - - (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e (*of*); - (*======= end of scanning tacticals, a leaf =======*) -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t) - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e); - val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*); - val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*); - (* 1st ContextC.insert_assumptions asms' ctxt *) - -(*NEW*) Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m) (*return value*); -"~~~~~ from assy to execute_progr_2 return val:"; val (xxxxx_xx) - = (Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m)); (*return value*) - -"~~~~~ from execute_progr_2 to locate_input_tactic return val:"; val Assoc (is as (_,_,_,_,_,_,_,strong_ass), ctxt(*NEW*), tac') - = (Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m)); - (*if*) strong_ass; (*then*) - -"~~~~~ from locate_input_tactic to solve return:"; val Safe_Step (istate, ctxt, tac) - = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate is, ctxt, tac')(**); - -(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of solve *) -(*NEW*) val p' = -(*NEW*) case p_ of Frm => p -(*NEW*) | Res => lev_on p -(*NEW*) | _ => error ("solve: call by " ^ pos'2str (p, p_)); -(*NEW*) val (p'', _, _,pt') = -(*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m -(*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *) -(*NEW*) (Istate.Pstate (E,l,rls,a',v',asap,S,true), ctxt) (p', p_) pt; -(*NEW*) (*in*) -(*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))], -(*NEW*) [(*ctree NOT cut*)], (pt', p''))); - -(*NEW*)("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)) )], [], (pt', p''))); -"~~~~~ from solve to loc_solve_ return:"; val ((msg, cs' : calcstate')) - = ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)) )], [(*ctree NOT cut*)], (pt', p''))); - -"~~~~~ from loc_solve_ to locatetac return:"; val (Updated (cs' as (_, _, (_, p')))) - = (*** )xxxxx( ***) (Updated (cs')); - (*if*) p' = ([], Ctree.Res); (*else*) - ("ok", cs'); -"~~~~~ from locatetac to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs'); - val (_, ts) = - (case step p ((pt, Ctree.e_pos'), []) of - ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts) - | ("helpless", _) => ("helpless: cannot propose tac", []) - | ("no-fmz-spec", _) => error "no-fmz-spec" - | ("end-of-calculation", (ts, _, _)) => ("", ts) - | _ => error "me: uncovered case") - handle ERROR msg => raise ERROR msg - val tac = - case ts of - tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end - | _ => if p = ([], Ctree.Res) then Tactic.End_Proof' else Tactic.Empty_Tac; - - (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt); -"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt) - = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt); - -(*//--------------------- check results from modified me ----------------------------------\\*) -if p = ([1], Res) andalso - pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n" -then - (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => () - | _ => error "") -else error "check results from modified me CHANGED"; -(*\\--------------------- check results from modified me ----------------------------------//*) - -"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**); -(*\\------------------ end of modified "fun me" ---------------------------------------------//*) -(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*) -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*) -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*) -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*) -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*) -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*) -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*) -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*) -(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*) -(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*) -(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*) -(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*) -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*) -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*) -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*) - -(*/--------------------- final test ----------------------------------\\*) -if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'" - andalso pr_ctree pr_short pt = - ". ----- pblobj -----\n" ^ - "1. x + 1 = 2\n" ^ - "2. x + 1 + -1 * 2 = 0\n" ^ - "3. ----- pblobj -----\n" ^ - "3.1. -1 + x = 0\n" ^ - "3.2. x = 0 + -1 * -1\n" ^ - "4. [x = 1]\n" -then () else error "re-build: fun locate_input_tactic changed"; - - -"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------"; -"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------"; -"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------"; -(*cp from -- try fun applyTactics ------- *) -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", - "normalform N"], - ("PolyMinus",["plus_minus","polynom","vereinfachen"], - ["simplification","for_polynomials","with_minus"]))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*) -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*) - -(*+*)map tac2str (sel_appl_atomic_tacs pt p) = - ["Rewrite (\"subtrahiere_x_plus_minus\", \"\?l is_const; ?m is_const\\n\ ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", - "Rewrite (\"subtrahiere_x_minus_plus\", \"\?l is_const; ?m is_const\\n\ ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]; -(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p); - -(*+*)map tac2str (sel_appl_atomic_tacs pt p) = - ["Rewrite (\"tausche_minus\", \"\?b ist_monom; ?a kleiner ?b\\n\ ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \ ?a + ?c - ?b = ?a - ?b + ?c\")", - "Rewrite (\"subtrahiere_x_plus_minus\", \"\?l is_const; ?m is_const\\n\ ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", - "Rewrite (\"subtrahiere_x_minus_plus\", \"\?l is_const; ?m is_const\\n\ ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]; -(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p); - -(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*) -(** )val ("ok", (_, _, ptp as (pt, p))) =( **) locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p); -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (hd (sel_appl_atomic_tacs pt p), (pt, p)); - val (mI, m) = Solve.mk_tac'_ tac; - val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*); - (*if*) member op = Solve.specsteps mI (*else*); - - loc_solve_ (mI, m) ptp; -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI, m), ptp); - solve m (pt, pos); - (* ======== general case ======== *) -"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos)); - (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); - val thy' = get_obj g_domID pt (par_pblobj pt p); - val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; - - (*case*) LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); -"~~~~~ fun locate_input_tactic , args:"; val ((progr as Rule.Prog _), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac) - = (sc, (pt, po), (fst is), (snd is), m); - val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*); - - (*case*) execute_progr_2 srls tac cstate (progr, Rule.e_rls) (istate, ctxt) (*of*); -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt)) - = (srls, tac, cstate ,(progr, Rule.e_rls), (istate, ctxt)); - (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*); - - astep_up (ctxt,srls,scr,(pt, p)) ((E,l,rls,a,v,asap,S,b), m); -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,asap,S,b),ss)) - = ((ctxt,srls,scr,(pt, p)), ((E,l,a,v,asap,S,b), m)); - (*if*) 1 < length l (*then*); - val up = drop_last l; (* = [R, L, R, L, R]*) - - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc); -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Try"(*2*),_) $ _)) - = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc)); - - astep_up ysa iss; -"~~~~~ fun astep_up , args:"; val (((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss))) - = (ysa, iss); - (*if*) 1 < length l (*then*); - val up = drop_last l; (* = [R, L, R, L]*) - - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc); -"~~~~~ fun ass_up , args:"; val ((ysa as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,asap,S,b),ss), - (Const ("Tactical.Seq"(*3*),_) $ _ )) - = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc)); - val up = drop_last l; - val Const ("Tactical.Seq",_) $ _ $ e2 = (*case*) go up sc (*of*); - - (*case*) assy ((*y,*)ctxt,s,d,Aundef) ((E, up @ [Celem.R], rls,a,v,asap,S,b),ss) e2 (*of*); -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $e1 $ e2)) - = (((*y,*)ctxt,s,d,Aundef), ((E, up @ [Celem.R], rls,a,v,asap,S,b),ss), e2); - val NasApp ((E,_,_,_,v,_,_,_), ctxt(*NEW*), ss) = (*case*) assy ya ((E, l @ [Celem.L, Celem.R], rls,a,v,asap,S,b),ss) e1 (*of*); - - assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e2; -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*2*),_) $ e)) - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e2); - - (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e (*of*); - (*======= end of scanning tacticals, a leaf =======*) -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t) - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e); - val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*); - val Lucin.NotAss = (*case*) Lucin.associate pt ctxt (m, stac) (*of*); - val Aundef = (*case*) ap (*of*); - val Appl m' = (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*); - val is = (E,l,rls,a',Lucin.tac_2res m',asap,S,false(*FIXXXME.WN0?*)); - NasApp (is, ctxt, m) (* return value *); - -val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \ ?a kleiner ?b \ ?b - ?a = - ?a + ?b"*)), - t, (res, asm)) = m; -if scrstate2str is = - "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,R,R], e_rls, SOMEt_t, \n" ^ - "- (8 * g) + (-9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Aundef, AppUndef_, false)" -andalso - term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g" -andalso - term2str res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g" -andalso - terms2str asm = "[\"4 kleiner 6\",\"6 ist_monom\"]" -then () else error "locate_input_tactic Helpless, but applicable CHANGED"; - - -"----------- re-build: fun determine_next_tactic -----------------------------------------------"; -"----------- re-build: fun determine_next_tactic -----------------------------------------------"; -"----------- re-build: fun determine_next_tactic -----------------------------------------------"; - - -"----------- re-build: fun locate_input_tactic -------------------------------------------------"; -"----------- re-build: fun locate_input_tactic -------------------------------------------------"; -"----------- re-build: fun locate_input_tactic -------------------------------------------------"; \ ML \ \ ML \ "~~~~~ fun xxx , args:"; val () = (); \ -section \=== --- Minisubpbl/251-Rewrite_Set-from-method.sml, determine_next_tactic --- =========\ -ML \ -\ ML \ -\ ML \ -"----------- Minisubpbl/251-Rewrite_Set-from-method.sml, determine_next_tactic ------ ----------"; -"----------- Minisubpbl/251-Rewrite_Set-from-method.sml, determine_next_tactic ------ ----------"; -"----------- Minisubpbl/251-Rewrite_Set-from-method.sml, determine_next_tactic ------ ----------"; -\ ML \ -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; -val (dI',pI',mI') = - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -\ ML \ -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []); -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []); -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []); -(*([], Met)*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*) -(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*) -\ ML \ -(*[1], Res*)val (_, ([(tac, _, _)], _, (pt''''', p'''''))) = step p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*) - -(*// relevant call --------------------------------------------------------------------------\\*) -\ ML \ -"~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])); -\ ML \ - val pIopt = get_pblID (pt,ip); -\ ML \ - (*if*) ip = ([], Ctree.Res) (*else*); -\ ML \ - val _ = (*case*) tacis (*of*); -\ ML \ - val SOME _ = (*case*) pIopt (*of*); -\ ML \ - (*if*) member op = [Ctree.Pbl, Ctree.Met] p_ - andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*else*); -\ ML \ - do_solve_step (pt, ip); -\ ML \ -"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); -\ ML \ - (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); -\ ML \ - val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; -\ ML \ - determine_next_tactic (thy', srls) (pt, pos) sc is; - (* TODO here ^^^ return finished/helpless/ok ?*) -\ ML \ -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,a,v,s,_), ctxt)) - = ((thy', srls), (pt, pos), sc, is); -\ ML \ - (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) (*of*); -\ ML \ -"~~~~~ fun execute_progr_1 , args:"; val () = (); -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -(*//--------------------- check results from modified step ----------------------------------\\*) -(*\\--------------------- check results from modified step ----------------------------------//*) -\ ML \ -"~~~~~ from me to TOPLEVEL return:"; val () = (*** )xxx( ***) (**)()(**); -(*\\------------------ end of modified "fun step" -------------------------------------------//*) -\ ML \ -(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p''''' ((pt''''', e_pos'), []);(*Rewrite_Set "Test_simplify"*) -\ ML \ -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) =(**) step p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p''''' ((pt''''', e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -\ ML \ -(**)val ("end-of-calculation", ([], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -\ ML \ - -(*/--------------------- final test ----------------------------------\\*) -\ ML \ -val (res, asm) = (get_obj g_result pt (fst p)); -if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]" -then () else error "Minisubpbl/301-init-subpbl.sml, determine_next_tactic CHANGED" - -\ ML \ -if p = ([], Und) -then - case get_obj g_tac pt (fst p) of - Apply_Method ["Test", "squ-equ-test-subpbl1"] => () - | _ => error "301-init-subpbl WRONG RESULT CHANGED 2" -else error "301-init-subpbl WRONG RESULT CHANGED 1" -\ ML \ -\ - -section \=== --- Minisubpbl/301-init-subpbl.sml, determine_next_tactic --- ======================\ -ML \ -\ ML \ -\ ML \ -"----------- Minisubpbl/301-init-subpbl.sml, determine_next_tactic -----------------------------"; -"----------- Minisubpbl/301-init-subpbl.sml, determine_next_tactic -----------------------------"; -"----------- Minisubpbl/301-init-subpbl.sml, determine_next_tactic -----------------------------"; -\ ML \ -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; -val (dI',pI',mI') = - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -\ ML \ -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []); -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []); -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []); -(*([], Met)*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*) -(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*) -(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*) -(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*) -\ ML \ -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt''''', p'''''))) =(**) step p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*) - -(*// relevant call --------------------------------------------------------------------------\\*) -\ ML \ -"~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])); -\ ML \ - val pIopt = get_pblID (pt,ip); -\ ML \ - (*if*) ip = ([], Ctree.Res) (*else*); -\ ML \ - val _ = (*case*) tacis (*of*); -\ ML \ - val SOME _ = (*case*) pIopt (*of*); -\ ML \ - (*if*) member op = [Ctree.Pbl, Ctree.Met] p_ - andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*else*); -\ ML \ - do_solve_step (pt, ip); -\ ML \ -"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); -\ ML \ - (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*); -\ ML \ - val thy' = get_obj g_domID pt (par_pblobj pt p); - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; -\ ML \ - determine_next_tactic (thy', srls) (pt, pos) sc is; - (* TODO here ^^^ return finished/helpless/ok ?*) -\ ML \ -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,a,v,s,_), ctxt)) - = ((thy', srls), (pt, pos), sc, is); -\ ML \ - (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) (*of*); -\ ML \ -"~~~~~ fun execute_progr_1 , args:"; val () = (); -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -(*//--------------------- check results from modified step ----------------------------------\\*) -(*\\--------------------- check results from modified step ----------------------------------//*) -\ ML \ -"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**); -(*\\------------------ end of modified "fun step" -------------------------------------------//*) -\ ML \ -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p''''' ((pt''''', e_pos'), []);(**) -\ ML \ -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**) -(**)val ("end-of-calculation", ([], _, (pt, p))) = step p ((pt, e_pos'), []);(**) - -(*/--------------------- final test ----------------------------------\\*) -\ ML \ -val (res, asm) = (get_obj g_result pt (fst p)); -if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]" -then () else error "Minisubpbl/301-init-subpbl.sml, determine_next_tactic CHANGED" - -\ ML \ -if p = ([], Und) -then - case get_obj g_tac pt (fst p) of - Apply_Method ["Test", "squ-equ-test-subpbl1"] => () - | _ => error "301-init-subpbl WRONG RESULT CHANGED 2" -else error "301-init-subpbl WRONG RESULT CHANGED 1" -\ ML \ -\ - section \===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\ ML \ "~~~~~ fun xxx , args:"; val () = (); diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Test_Theory.thy --- a/test/Tools/isac/Test_Theory.thy Mon Nov 04 11:40:29 2019 +0100 +++ b/test/Tools/isac/Test_Theory.thy Wed Nov 06 15:08:27 2019 +0100 @@ -1,17 +1,19 @@ (* use this theory for tests before Build_Isac.thy has succeeded *) -theory Test_Theory imports Isac.Program +theory Test_Theory imports "~~/src/Tools/isac/Specify/Specify" begin -ML_file "~~/src/Tools/isac/library.sml" -(* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.get_theory +ML_file "~~/src/Tools/isac/CalcElements/libraryC.sml" +(* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.getfu _theory requires session Isac, see ~~/test/Tools/isac/ADDTESTS/session-get_theory *) section \code for copy & paste ===============================================================\ ML \ -"~~~~~ fun , args:"; val () = (); -"~~~~~ and , args:"; val () = (); - -"~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*)); - +"~~~~~ fun xxx , args:"; val () = (); +"~~~~~ and xxx , args:"; val () = (); +"~~~~~ from xxx -> fun yyy -> fun zzz, return val:"; val () = (); +(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); +"xx" +^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) +\ ML \ \ text \ declare [[show_types]] @@ -46,7 +48,6 @@ \ ML \ \ ML \ \ ML \ -\ ML \ \ section \=================================================================\ ML \