# HG changeset patch # User Walther Neuper # Date 1573061669 -3600 # Node ID 62edafdc1df5f2cd8f1ad4319c795de6d7e7cf9c # Parent 3ce3d089bd649e86c35bf8e1b00e50bc700834fa lucin: renaming for paper diff -r 3ce3d089bd64 -r 62edafdc1df5 src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Nov 06 15:08:27 2019 +0100 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Nov 06 18:34:29 2019 +0100 @@ -3,7 +3,7 @@ (c) isac-team *) -fun file2str (path : Celem.path) (fnm : Celem.filename) = +fun file2str (path : Celem.filepath) (fnm : Celem.filename) = let val file = TextIO.openIn (path ^ fnm) val str = TextIO.inputAll file @@ -83,7 +83,7 @@ (* (writeln o hierarchy_pbl) (!ptyps); *) -fun pbl_hierarchy2file (path : Celem.path) = +fun pbl_hierarchy2file (path : Celem.filepath) = str2file (path ^ "pbl_hierarchy.xml") ("\n" ^ " problem hierarchy \n" ^ @@ -92,7 +92,7 @@ (hierarchy_pbl (get_ptyps ())) ^ ""); -fun met_hierarchy2file (path : Celem.path) = +fun met_hierarchy2file (path : Celem.filepath) = str2file (path ^ "met_hierarchy.xml") ("\n" ^ " method hierarchy \n" ^ @@ -181,7 +181,7 @@ (**. write pbls from hierarchy to files.**) -fun pbl2file (path: Celem.path) (pos: Ctree.pos) (id:Celem.metID) (pbl as {guh,...}) = +fun pbl2file (path: Celem.filepath) (pos: Ctree.pos) (id:Celem.metID) (pbl as {guh,...}) = (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Ctree.pos2str pos); ((str2file (path ^ Rtools.guh2filename guh)) o (pbl2xml id)) pbl ); @@ -254,17 +254,17 @@ *) (*.write the files using an int-key (pos') as filename.*) -fun met2file (path: Celem.path) (pos: Ctree.pos) (id: Celem.metID) met = +fun met2file (path: Celem.filepath) (pos: Ctree.pos) (id: Celem.metID) met = (writeln ("### met2file: id = " ^ strs2str id); ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met); (*.write the files using the guh as filename.*) -fun met2file (path: Celem.path) (pos: Ctree.pos) (id: Celem.metID) (met as {guh,...}) = +fun met2file (path: Celem.filepath) (pos: Ctree.pos) (id: Celem.metID) (met as {guh,...}) = (writeln ("### met2file: id = " ^ strs2str id); ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met); (*.scan the mtree Ptyp and print the nodes using wfn.*) -fun node (pa: Celem.path) ids po wfn (Celem.Ptyp (id,[n],ns)) = +fun node (pa: Celem.filepath) ids po wfn (Celem.Ptyp (id,[n],ns)) = let val po' = Ctree.lev_on po in wfn pa po' (ids@[id]) n; @@ -274,8 +274,8 @@ | nodes pa ids po wfn (n::ns) = (node pa ids po wfn n; nodes pa ids (Ctree.lev_on po) wfn ns); -fun pbls2file (p: Celem.path) = nodes p [] [0] pbl2file (get_ptyps ()); -fun mets2file (p: Celem.path) = nodes p [] [0] met2file (get_mets ()); +fun pbls2file (p: Celem.filepath) = nodes p [] [0] pbl2file (get_ptyps ()); +fun mets2file (p: Celem.filepath) = nodes p [] [0] met2file (get_mets ()); (* val path = "/home/neuper/proto2/isac/xmldata/"; val path = "/home/neuper/tmp/"; diff -r 3ce3d089bd64 -r 62edafdc1df5 src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Nov 06 15:08:27 2019 +0100 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Nov 06 18:34:29 2019 +0100 @@ -119,7 +119,7 @@ | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Ctree.lev_on p) theID ns); in nodes j [0] [] h end; -fun thy_hierarchy2file (path: Celem.path) = +fun thy_hierarchy2file (path: Celem.filepath) = str2file (path ^ "thy_hierarchy.xml") ("\n" ^ " theory hierarchy \n" ^ @@ -175,12 +175,12 @@ error ("thydata2xml: not implemented for "^ strs2str' theID); (* analoguous to 'fun met2file' *) -fun thydata2file (path : Celem.path) (pos : Ctree.pos) (theID : Celem.theID) thydata = +fun thydata2file (path : Celem.filepath) (pos : Ctree.pos) (theID : Celem.theID) thydata = (writeln ("### thes2file: id = " ^ strs2str theID); str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata))); (* analoguous to 'fun node' *) -fun thenode (pa : Celem.path) ids po wfn (Celem.Ptyp (id, [n], ns)) = +fun thenode (pa : Celem.filepath) ids po wfn (Celem.Ptyp (id, [n], ns)) = let val po' = Ctree.lev_on po in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Ctree.lev_dn po') wfn ns end and thenodes _ _ _ _ [] = () @@ -188,7 +188,7 @@ (thenode pa ids po wfn n; thenodes pa ids (Ctree.lev_on po) wfn ns); (* analoguous to 'fun mets2file' *) -fun thes2file (p : Celem.path) = thenodes p [] [0] thydata2file (get_thes ()); +fun thes2file (p : Celem.filepath) = thenodes p [] [0] thydata2file (get_thes ()); (***.store a single theory element in the hierarchy.***) diff -r 3ce3d089bd64 -r 62edafdc1df5 src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Wed Nov 06 15:08:27 2019 +0100 +++ b/src/Tools/isac/Build_Isac.thy Wed Nov 06 18:34:29 2019 +0100 @@ -20,6 +20,7 @@ theory CalcElements imports KEStore ML_file termC.sml ML_file contextC.sml + ML_file environment.sml *) "CalcElements/CalcElements" (* theory Calculate imports "~~/src/Tools/isac/CalcElements/CalcElements" diff -r 3ce3d089bd64 -r 62edafdc1df5 src/Tools/isac/CalcElements/calcelems.sml --- a/src/Tools/isac/CalcElements/calcelems.sml Wed Nov 06 15:08:27 2019 +0100 +++ b/src/Tools/isac/CalcElements/calcelems.sml Wed Nov 06 18:34:29 2019 +0100 @@ -62,8 +62,8 @@ val trace_rewrite: bool Unsynchronized.ref val depth: int Unsynchronized.ref val assoc_thy: Rule.theory' -> theory - type loc_ - val loc_2str: loc_ -> string + type path + val path2str: path -> string type thm'' val metID2str: string list -> string val e_pblID: pblID @@ -96,7 +96,7 @@ val ketype2str': ketype -> string val str2ketype': string -> ketype val thmID_of_derivation_name': thm -> string - eqtype path + eqtype filepath val theID2thyID: theID -> Rule.thyID val thy2guh: theID -> guh val thypart2guh: theID -> guh @@ -400,7 +400,7 @@ | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs)) | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs); -type path = string; +type filepath = string; type filename = string; @@ -463,15 +463,13 @@ val check_guhs_unique = Unsynchronized.ref true; -datatype lrd = (*elements of "type loc_" into an Isabelle term*) - L (*go left at $*) -| R (*go right at $*) -| D; (*go down at Abs*) -type loc_ = lrd list; +datatype lrd = L (*t1 in "t1$t2"*) + | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*) +type path = lrd list; fun ldr2str L = "L" | ldr2str R = "R" | ldr2str D = "D"; -fun loc_2str k = (strs2str' o (map ldr2str)) k; +fun path2str k = (strs2str' o (map ldr2str)) k; (* the pattern for an item of a problems model or a methods guard *) diff -r 3ce3d089bd64 -r 62edafdc1df5 src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 06 15:08:27 2019 +0100 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 06 18:34:29 2019 +0100 @@ -41,8 +41,8 @@ | NasNap of term * Env.T; val assoc2str : assoc -> string (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) - val go : Celem.loc_ -> term -> term - val go_up: Celem.loc_ -> term -> term + val go : Celem.path -> term -> term + val go_up: Celem.path -> term -> term val check_Let_up : Istate.pstate -> term -> term * term val check_Seq_up: Istate.pstate -> term -> term @@ -73,10 +73,10 @@ (*go to a location in a script and fetch the contents*) fun go [] t = t - | go (D :: p) (Abs(_, _, t0)) = go (p : Celem.loc_) t0 + | go (D :: p) (Abs(_, _, t0)) = go (p : Celem.path) t0 | go (L :: p) (t1 $ _) = go p t1 | go (R :: p) (_ $ t2) = go p t2 - | go l _ = error ("go: no " ^ Celem.loc_2str l); + | go l _ = error ("go: no " ^ Celem.path2str l); fun go_up l t = if length l > 1 then go (drop_last l) t else raise ERROR ("go_up [] " ^ Rule.term2str t) @@ -265,7 +265,7 @@ else (*interpreted to end*) if finish = Skip_ then Skip (get_act_env ist) else Napp env | nstep_up _ {path, ...} = - raise ERROR ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str path) + raise ERROR ("nstep_up: uncovered fun-def at " ^ Celem.path2str path) fun execute_progr_1 (sc as Rule.Prog prog, cct) (Istate.Pstate (ist as {path, ...})) = if 0 = length path @@ -465,7 +465,7 @@ then ass_up yyy (ist |> path_up) (go (path_up' path) sc) else (NasNap (get_act_env ist)) | astep_up _ {path, ...} = - raise ERROR ("astep_up: uncovered fun-def with " ^ Celem.loc_2str path) + raise ERROR ("astep_up: uncovered fun-def with " ^ Celem.path2str path) 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) diff -r 3ce3d089bd64 -r 62edafdc1df5 src/Tools/isac/MathEngBasic/ctree-basic.sml --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Nov 06 15:08:27 2019 +0100 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Nov 06 18:34:29 2019 +0100 @@ -220,7 +220,7 @@ (* executed tactics (tac_s) with local environment etc.; used for continuing eval script + for generate *) type ets = - (Celem.loc_ *(* of tactic in scr, tactic (weakly) associated with tac_ *) + (Celem.path *(* of tactic in scr, tactic (weakly) associated with tac_ *) (Tactic.T * (* (for generate) *) env * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *) env * (* with results of (ready) tacs *) @@ -230,7 +230,7 @@ list; fun ets2s (l,(m,eno,env,iar,res,s)) = - "\n(" ^ Celem.loc_2str l ^ ",(" ^ Tactic.tac_2str m ^ + "\n(" ^ Celem.path2str l ^ ",(" ^ Tactic.tac_2str m ^ ",\n ens= " ^ Env.subst2str eno ^ ",\n env= " ^ Env.subst2str env ^ ",\n iar= " ^ Rule.term2str iar ^ diff -r 3ce3d089bd64 -r 62edafdc1df5 src/Tools/isac/MathEngBasic/istate.sml --- a/src/Tools/isac/MathEngBasic/istate.sml Wed Nov 06 15:08:27 2019 +0100 +++ b/src/Tools/isac/MathEngBasic/istate.sml Wed Nov 06 18:34:29 2019 +0100 @@ -25,14 +25,14 @@ val trans_ass: pstate -> pstate -> pstate val trans_env_act: pstate -> pstate -> pstate - val path_down: Celem.loc_ -> pstate -> pstate - val path_down_form: (Celem.loc_ * term) -> pstate -> pstate - val path_up': Celem.loc_ -> Celem.loc_ + val path_down: Celem.path -> pstate -> pstate + val path_down_form: (Celem.path * term) -> pstate -> pstate + val path_up': Celem.path -> Celem.path val path_up: pstate -> pstate - val path_up_down: Celem.loc_ -> pstate -> pstate + val path_up_down: Celem.path -> pstate -> pstate val upd_form: term -> pstate -> pstate - val upd_path: Celem.loc_ -> pstate -> pstate + val upd_path: Celem.path -> pstate -> pstate val upd_rls: Rule.rls -> pstate -> pstate val upd_act: term -> pstate -> pstate val upd_appy: appy_ -> pstate -> pstate @@ -82,7 +82,7 @@ type pstate = (* state for script interpreter *) {env: Env.T,(*stack*) (* used to instantiate tac for checking associate 12.03.noticed: e_ not updated during execution ?!? *) - path: Celem.loc_, (* location of tac in script *) + path: Celem.path, (* location of tac in script *) eval: Rule.rls, (* for evaluating Prog_Expr *) form_arg: term option, (*id FORMal ARGument of curried functions *) act_arg: term, (*vl ACTual ARGument (value) for execution of Tactic.T @@ -97,7 +97,7 @@ fun topt2str NONE = "NONE" | topt2str (SOME t) = "SOME" ^ Rule.term2str t; fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *) - "(" ^ Env.env2str env ^ ", " ^ Celem.loc_2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^ + "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^ topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^ appy_2str finish ^ ", " ^ bool2str assoc ^ ")"; diff -r 3ce3d089bd64 -r 62edafdc1df5 test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Nov 06 15:08:27 2019 +0100 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Nov 06 18:34:29 2019 +0100 @@ -120,14 +120,14 @@ "----- ERROR Illegal reference to internal variable: 'Pure_' -----"; "----- ERROR Illegal reference to internal variable: 'Pure_' -----"; val path = "/tmp/"; -"~~~~~ fun pbls2file, args:"; val (p:path) = (path ^ "pbl/"); +"~~~~~ fun pbls2file, args:"; val (p:filepath) = (path ^ "pbl/"); get_ptyps (); (*not = []*) "~~~~~ fun nodes, args:"; val (pa, ids, po, wfn, (n::ns)) = (p, []: string list, [0], pbl2file, (get_ptyps ())); -"~~~~~ fun node, args:"; val (pa:path, ids, po, wfn, Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n); +"~~~~~ fun node, args:"; val (pa:filepath, ids, po, wfn, Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n); val po' = lev_on po; wfn (*= pbl2file*) -"~~~~~ fun pbl2file, args:"; val ((path:path), (pos:pos), (id:metID), (pbl as {guh,...})) = +"~~~~~ fun pbl2file, args:"; val ((path:filepath), (pos:pos), (id:metID), (pbl as {guh,...})) = (pa, po', (ids@[id]), n); strs2str id = "[\"e_pblID\"]"; (*true*) pos2str pos = "[1]"; (*true*) diff -r 3ce3d089bd64 -r 62edafdc1df5 test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Nov 06 15:08:27 2019 +0100 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Nov 06 18:34:29 2019 +0100 @@ -91,9 +91,9 @@ "----------- search for data error in thes2file ------------------"; "----------- search for data error in thes2file ------------------"; val TESTdump = Unsynchronized.ref - ("path": path, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp); + ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp); -fun TESTthenode (pa:path) ids po wfn (Ptyp (id, [n], ns)) TESTids = +fun TESTthenode (pa:filepath) ids po wfn (Ptyp (id, [n], ns)) TESTids = let val po' = lev_on po in if (ids@[id]) = TESTids @@ -112,7 +112,7 @@ val j = indentation; (* \--- side effects from previous test files ---/*) -"~~~~~ fun thes2file, args:"; val (p : path) = ("/tmp/"); +"~~~~~ fun thes2file, args:"; val (p : filepath) = ("/tmp/"); (* recursively descend into thehier just before the error by setting TESTids according to the last line in ouput ### thes2file: id = : *) @@ -123,7 +123,7 @@ (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*) val (pa, ids, po', wfn, (Ptyp (id, [n], ns))) = ! TESTdump; ; -"~~~~~ fun thydata2file, args:"; val ((xmldata:path), (pos:pos), (theID:theID), thydata) = +"~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:theID), thydata) = (pa, po', (ids@[id]), n); "~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = (theID:theID, thydata); @@ -329,7 +329,7 @@ "----------- ..CONTINUED: we adapt some required MINIfunctions ---"; "----------- ..CONTINUED: we adapt some required MINIfunctions ---"; fun MINIget_the (theID : theID) = get_py MINIthehier theID theID (*see ptyps.sml*) -fun MINIthy_hierarchy2file (path:path) = +fun MINIthy_hierarchy2file (path:filepath) = str2file (path ^ "thy_hierarchy.xml") ("\n" ^ " theory hierarchy \n" ^ @@ -337,7 +337,7 @@ " thy_ROOT \n" ^ (hierarchy_guh MINIthehier) ^ ""); -fun MINIthes2file (p : path) = thenodes p [] [0] thydata2file MINIthehier; +fun MINIthes2file (p : filepath) = thenodes p [] [0] thydata2file MINIthehier; "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------"; "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------"; @@ -359,7 +359,7 @@ "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/"); "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) = (path, [], [0], thydata2file, MINIthehier); -"~~~~~ fun thenode, args:"; val ((pa : path), ids, po, wfn, (Ptyp (id, [n], ns))) = +"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Ptyp (id, [n], ns))) = (pa, ids, po, wfn, n); val po' = lev_on po; (*wfn pa po' (ids @ [id]) n -------------> writes xml to file; we want xml before written: *) @@ -370,7 +370,7 @@ Hthm {guh = "thy_isac_Test_Build_Thydata-thm-thm111", mathauthors = ["isac-team"], ...}) => () | _ => error "a change inhibits successful continuation of this test"; val (theID, thydata) = hd thydata_list; -"~~~~~ fun thydata2file, args:"; val ((path : path), (pos : pos), (theID : theID), thydata) = +"~~~~~ fun thydata2file, args:"; val ((path : filepath), (pos : pos), (theID : theID), thydata) = (pa, po', (*ids @ [id]*)theID, (*n*)thydata); "~~~~~ fun thydata2xml, args:"; val ((theID, Hthm {guh, coursedesign, mathauthors, fillpats, thm}))= ((theID, thydata)); diff -r 3ce3d089bd64 -r 62edafdc1df5 test/Tools/isac/Minisubpbl/799-complete.sml --- a/test/Tools/isac/Minisubpbl/799-complete.sml Wed Nov 06 15:08:27 2019 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -(* 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";