1.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Nov 06 15:08:27 2019 +0100
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Nov 06 18:34:29 2019 +0100
1.3 @@ -3,7 +3,7 @@
1.4 (c) isac-team
1.5 *)
1.6
1.7 -fun file2str (path : Celem.path) (fnm : Celem.filename) =
1.8 +fun file2str (path : Celem.filepath) (fnm : Celem.filename) =
1.9 let
1.10 val file = TextIO.openIn (path ^ fnm)
1.11 val str = TextIO.inputAll file
1.12 @@ -83,7 +83,7 @@
1.13 (* (writeln o hierarchy_pbl) (!ptyps);
1.14 *)
1.15
1.16 -fun pbl_hierarchy2file (path : Celem.path) =
1.17 +fun pbl_hierarchy2file (path : Celem.filepath) =
1.18 str2file (path ^ "pbl_hierarchy.xml")
1.19 ("<NODE>\n" ^
1.20 " <ID> problem hierarchy </ID>\n" ^
1.21 @@ -92,7 +92,7 @@
1.22 (hierarchy_pbl (get_ptyps ())) ^
1.23 "</NODE>");
1.24
1.25 -fun met_hierarchy2file (path : Celem.path) =
1.26 +fun met_hierarchy2file (path : Celem.filepath) =
1.27 str2file (path ^ "met_hierarchy.xml")
1.28 ("<NODE>\n" ^
1.29 " <ID> method hierarchy </ID>\n" ^
1.30 @@ -181,7 +181,7 @@
1.31
1.32
1.33 (**. write pbls from hierarchy to files.**)
1.34 -fun pbl2file (path: Celem.path) (pos: Ctree.pos) (id:Celem.metID) (pbl as {guh,...}) =
1.35 +fun pbl2file (path: Celem.filepath) (pos: Ctree.pos) (id:Celem.metID) (pbl as {guh,...}) =
1.36 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Ctree.pos2str pos);
1.37 ((str2file (path ^ Rtools.guh2filename guh)) o (pbl2xml id)) pbl
1.38 );
1.39 @@ -254,17 +254,17 @@
1.40 *)
1.41
1.42 (*.write the files using an int-key (pos') as filename.*)
1.43 -fun met2file (path: Celem.path) (pos: Ctree.pos) (id: Celem.metID) met =
1.44 +fun met2file (path: Celem.filepath) (pos: Ctree.pos) (id: Celem.metID) met =
1.45 (writeln ("### met2file: id = " ^ strs2str id);
1.46 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
1.47
1.48 (*.write the files using the guh as filename.*)
1.49 -fun met2file (path: Celem.path) (pos: Ctree.pos) (id: Celem.metID) (met as {guh,...}) =
1.50 +fun met2file (path: Celem.filepath) (pos: Ctree.pos) (id: Celem.metID) (met as {guh,...}) =
1.51 (writeln ("### met2file: id = " ^ strs2str id);
1.52 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met);
1.53
1.54 (*.scan the mtree Ptyp and print the nodes using wfn.*)
1.55 -fun node (pa: Celem.path) ids po wfn (Celem.Ptyp (id,[n],ns)) =
1.56 +fun node (pa: Celem.filepath) ids po wfn (Celem.Ptyp (id,[n],ns)) =
1.57 let val po' = Ctree.lev_on po
1.58 in
1.59 wfn pa po' (ids@[id]) n;
1.60 @@ -274,8 +274,8 @@
1.61 | nodes pa ids po wfn (n::ns) =
1.62 (node pa ids po wfn n; nodes pa ids (Ctree.lev_on po) wfn ns);
1.63
1.64 -fun pbls2file (p: Celem.path) = nodes p [] [0] pbl2file (get_ptyps ());
1.65 -fun mets2file (p: Celem.path) = nodes p [] [0] met2file (get_mets ());
1.66 +fun pbls2file (p: Celem.filepath) = nodes p [] [0] pbl2file (get_ptyps ());
1.67 +fun mets2file (p: Celem.filepath) = nodes p [] [0] met2file (get_mets ());
1.68 (*
1.69 val path = "/home/neuper/proto2/isac/xmldata/";
1.70 val path = "/home/neuper/tmp/";
2.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Nov 06 15:08:27 2019 +0100
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Nov 06 18:34:29 2019 +0100
2.3 @@ -119,7 +119,7 @@
2.4 | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Ctree.lev_on p) theID ns);
2.5 in nodes j [0] [] h end;
2.6
2.7 -fun thy_hierarchy2file (path: Celem.path) =
2.8 +fun thy_hierarchy2file (path: Celem.filepath) =
2.9 str2file (path ^ "thy_hierarchy.xml")
2.10 ("<NODE>\n" ^
2.11 " <ID> theory hierarchy </ID>\n" ^
2.12 @@ -175,12 +175,12 @@
2.13 error ("thydata2xml: not implemented for "^ strs2str' theID);
2.14
2.15 (* analoguous to 'fun met2file' *)
2.16 -fun thydata2file (path : Celem.path) (pos : Ctree.pos) (theID : Celem.theID) thydata =
2.17 +fun thydata2file (path : Celem.filepath) (pos : Ctree.pos) (theID : Celem.theID) thydata =
2.18 (writeln ("### thes2file: id = " ^ strs2str theID);
2.19 str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata)));
2.20
2.21 (* analoguous to 'fun node' *)
2.22 -fun thenode (pa : Celem.path) ids po wfn (Celem.Ptyp (id, [n], ns)) =
2.23 +fun thenode (pa : Celem.filepath) ids po wfn (Celem.Ptyp (id, [n], ns)) =
2.24 let val po' = Ctree.lev_on po
2.25 in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Ctree.lev_dn po') wfn ns end
2.26 and thenodes _ _ _ _ [] = ()
2.27 @@ -188,7 +188,7 @@
2.28 (thenode pa ids po wfn n; thenodes pa ids (Ctree.lev_on po) wfn ns);
2.29
2.30 (* analoguous to 'fun mets2file' *)
2.31 -fun thes2file (p : Celem.path) = thenodes p [] [0] thydata2file (get_thes ());
2.32 +fun thes2file (p : Celem.filepath) = thenodes p [] [0] thydata2file (get_thes ());
2.33
2.34
2.35 (***.store a single theory element in the hierarchy.***)
3.1 --- a/src/Tools/isac/Build_Isac.thy Wed Nov 06 15:08:27 2019 +0100
3.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Nov 06 18:34:29 2019 +0100
3.3 @@ -20,6 +20,7 @@
3.4 theory CalcElements imports KEStore
3.5 ML_file termC.sml
3.6 ML_file contextC.sml
3.7 + ML_file environment.sml
3.8 *) "CalcElements/CalcElements"
3.9
3.10 (* theory Calculate imports "~~/src/Tools/isac/CalcElements/CalcElements"
4.1 --- a/src/Tools/isac/CalcElements/calcelems.sml Wed Nov 06 15:08:27 2019 +0100
4.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml Wed Nov 06 18:34:29 2019 +0100
4.3 @@ -62,8 +62,8 @@
4.4 val trace_rewrite: bool Unsynchronized.ref
4.5 val depth: int Unsynchronized.ref
4.6 val assoc_thy: Rule.theory' -> theory
4.7 - type loc_
4.8 - val loc_2str: loc_ -> string
4.9 + type path
4.10 + val path2str: path -> string
4.11 type thm''
4.12 val metID2str: string list -> string
4.13 val e_pblID: pblID
4.14 @@ -96,7 +96,7 @@
4.15 val ketype2str': ketype -> string
4.16 val str2ketype': string -> ketype
4.17 val thmID_of_derivation_name': thm -> string
4.18 - eqtype path
4.19 + eqtype filepath
4.20 val theID2thyID: theID -> Rule.thyID
4.21 val thy2guh: theID -> guh
4.22 val thypart2guh: theID -> guh
4.23 @@ -400,7 +400,7 @@
4.24 | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
4.25 | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
4.26
4.27 -type path = string;
4.28 +type filepath = string;
4.29 type filename = string;
4.30
4.31
4.32 @@ -463,15 +463,13 @@
4.33 val check_guhs_unique = Unsynchronized.ref true;
4.34
4.35
4.36 -datatype lrd = (*elements of "type loc_" into an Isabelle term*)
4.37 - L (*go left at $*)
4.38 -| R (*go right at $*)
4.39 -| D; (*go down at Abs*)
4.40 -type loc_ = lrd list;
4.41 +datatype lrd = L (*t1 in "t1$t2"*)
4.42 + | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*)
4.43 +type path = lrd list;
4.44 fun ldr2str L = "L"
4.45 | ldr2str R = "R"
4.46 | ldr2str D = "D";
4.47 -fun loc_2str k = (strs2str' o (map ldr2str)) k;
4.48 +fun path2str k = (strs2str' o (map ldr2str)) k;
4.49
4.50
4.51 (* the pattern for an item of a problems model or a methods guard *)
5.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 06 15:08:27 2019 +0100
5.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 06 18:34:29 2019 +0100
5.3 @@ -41,8 +41,8 @@
5.4 | NasNap of term * Env.T;
5.5 val assoc2str : assoc -> string
5.6 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.7 - val go : Celem.loc_ -> term -> term
5.8 - val go_up: Celem.loc_ -> term -> term
5.9 + val go : Celem.path -> term -> term
5.10 + val go_up: Celem.path -> term -> term
5.11 val check_Let_up : Istate.pstate -> term -> term * term
5.12 val check_Seq_up: Istate.pstate -> term -> term
5.13
5.14 @@ -73,10 +73,10 @@
5.15
5.16 (*go to a location in a script and fetch the contents*)
5.17 fun go [] t = t
5.18 - | go (D :: p) (Abs(_, _, t0)) = go (p : Celem.loc_) t0
5.19 + | go (D :: p) (Abs(_, _, t0)) = go (p : Celem.path) t0
5.20 | go (L :: p) (t1 $ _) = go p t1
5.21 | go (R :: p) (_ $ t2) = go p t2
5.22 - | go l _ = error ("go: no " ^ Celem.loc_2str l);
5.23 + | go l _ = error ("go: no " ^ Celem.path2str l);
5.24 fun go_up l t =
5.25 if length l > 1 then go (drop_last l) t else raise ERROR ("go_up [] " ^ Rule.term2str t)
5.26
5.27 @@ -265,7 +265,7 @@
5.28 else (*interpreted to end*)
5.29 if finish = Skip_ then Skip (get_act_env ist) else Napp env
5.30 | nstep_up _ {path, ...} =
5.31 - raise ERROR ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str path)
5.32 + raise ERROR ("nstep_up: uncovered fun-def at " ^ Celem.path2str path)
5.33
5.34 fun execute_progr_1 (sc as Rule.Prog prog, cct) (Istate.Pstate (ist as {path, ...})) =
5.35 if 0 = length path
5.36 @@ -465,7 +465,7 @@
5.37 then ass_up yyy (ist |> path_up) (go (path_up' path) sc)
5.38 else (NasNap (get_act_env ist))
5.39 | astep_up _ {path, ...} =
5.40 - raise ERROR ("astep_up: uncovered fun-def with " ^ Celem.loc_2str path)
5.41 + raise ERROR ("astep_up: uncovered fun-def with " ^ Celem.path2str path)
5.42
5.43 fun execute_progr_2 (scr as Rule.Prog sc, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) =
5.44 if path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res)
6.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Nov 06 15:08:27 2019 +0100
6.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Nov 06 18:34:29 2019 +0100
6.3 @@ -220,7 +220,7 @@
6.4 (* executed tactics (tac_s) with local environment etc.;
6.5 used for continuing eval script + for generate *)
6.6 type ets =
6.7 - (Celem.loc_ *(* of tactic in scr, tactic (weakly) associated with tac_ *)
6.8 + (Celem.path *(* of tactic in scr, tactic (weakly) associated with tac_ *)
6.9 (Tactic.T * (* (for generate) *)
6.10 env * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *)
6.11 env * (* with results of (ready) tacs *)
6.12 @@ -230,7 +230,7 @@
6.13 list;
6.14
6.15 fun ets2s (l,(m,eno,env,iar,res,s)) =
6.16 - "\n(" ^ Celem.loc_2str l ^ ",(" ^ Tactic.tac_2str m ^
6.17 + "\n(" ^ Celem.path2str l ^ ",(" ^ Tactic.tac_2str m ^
6.18 ",\n ens= " ^ Env.subst2str eno ^
6.19 ",\n env= " ^ Env.subst2str env ^
6.20 ",\n iar= " ^ Rule.term2str iar ^
7.1 --- a/src/Tools/isac/MathEngBasic/istate.sml Wed Nov 06 15:08:27 2019 +0100
7.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml Wed Nov 06 18:34:29 2019 +0100
7.3 @@ -25,14 +25,14 @@
7.4 val trans_ass: pstate -> pstate -> pstate
7.5 val trans_env_act: pstate -> pstate -> pstate
7.6
7.7 - val path_down: Celem.loc_ -> pstate -> pstate
7.8 - val path_down_form: (Celem.loc_ * term) -> pstate -> pstate
7.9 - val path_up': Celem.loc_ -> Celem.loc_
7.10 + val path_down: Celem.path -> pstate -> pstate
7.11 + val path_down_form: (Celem.path * term) -> pstate -> pstate
7.12 + val path_up': Celem.path -> Celem.path
7.13 val path_up: pstate -> pstate
7.14 - val path_up_down: Celem.loc_ -> pstate -> pstate
7.15 + val path_up_down: Celem.path -> pstate -> pstate
7.16
7.17 val upd_form: term -> pstate -> pstate
7.18 - val upd_path: Celem.loc_ -> pstate -> pstate
7.19 + val upd_path: Celem.path -> pstate -> pstate
7.20 val upd_rls: Rule.rls -> pstate -> pstate
7.21 val upd_act: term -> pstate -> pstate
7.22 val upd_appy: appy_ -> pstate -> pstate
7.23 @@ -82,7 +82,7 @@
7.24 type pstate = (* state for script interpreter *)
7.25 {env: Env.T,(*stack*) (* used to instantiate tac for checking associate
7.26 12.03.noticed: e_ not updated during execution ?!? *)
7.27 - path: Celem.loc_, (* location of tac in script *)
7.28 + path: Celem.path, (* location of tac in script *)
7.29 eval: Rule.rls, (* for evaluating Prog_Expr *)
7.30 form_arg: term option, (*id FORMal ARGument of curried functions *)
7.31 act_arg: term, (*vl ACTual ARGument (value) for execution of Tactic.T
7.32 @@ -97,7 +97,7 @@
7.33 fun topt2str NONE = "NONE"
7.34 | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
7.35 fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *)
7.36 - "(" ^ Env.env2str env ^ ", " ^ Celem.loc_2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
7.37 + "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
7.38 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
7.39 appy_2str finish ^ ", " ^ bool2str assoc ^ ")";
7.40
8.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Nov 06 15:08:27 2019 +0100
8.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Nov 06 18:34:29 2019 +0100
8.3 @@ -120,14 +120,14 @@
8.4 "----- ERROR Illegal reference to internal variable: 'Pure_' -----";
8.5 "----- ERROR Illegal reference to internal variable: 'Pure_' -----";
8.6 val path = "/tmp/";
8.7 -"~~~~~ fun pbls2file, args:"; val (p:path) = (path ^ "pbl/");
8.8 +"~~~~~ fun pbls2file, args:"; val (p:filepath) = (path ^ "pbl/");
8.9 get_ptyps (); (*not = []*)
8.10 "~~~~~ fun nodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
8.11 (p, []: string list, [0], pbl2file, (get_ptyps ()));
8.12 -"~~~~~ fun node, args:"; val (pa:path, ids, po, wfn, Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n);
8.13 +"~~~~~ fun node, args:"; val (pa:filepath, ids, po, wfn, Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n);
8.14 val po' = lev_on po;
8.15 wfn (*= pbl2file*)
8.16 -"~~~~~ fun pbl2file, args:"; val ((path:path), (pos:pos), (id:metID), (pbl as {guh,...})) =
8.17 +"~~~~~ fun pbl2file, args:"; val ((path:filepath), (pos:pos), (id:metID), (pbl as {guh,...})) =
8.18 (pa, po', (ids@[id]), n);
8.19 strs2str id = "[\"e_pblID\"]"; (*true*)
8.20 pos2str pos = "[1]"; (*true*)
9.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Nov 06 15:08:27 2019 +0100
9.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Nov 06 18:34:29 2019 +0100
9.3 @@ -91,9 +91,9 @@
9.4 "----------- search for data error in thes2file ------------------";
9.5 "----------- search for data error in thes2file ------------------";
9.6 val TESTdump = Unsynchronized.ref
9.7 - ("path": path, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp);
9.8 + ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp);
9.9
9.10 -fun TESTthenode (pa:path) ids po wfn (Ptyp (id, [n], ns)) TESTids =
9.11 +fun TESTthenode (pa:filepath) ids po wfn (Ptyp (id, [n], ns)) TESTids =
9.12 let val po' = lev_on po
9.13 in
9.14 if (ids@[id]) = TESTids
9.15 @@ -112,7 +112,7 @@
9.16 val j = indentation;
9.17 (* \--- side effects from previous test files ---/*)
9.18
9.19 -"~~~~~ fun thes2file, args:"; val (p : path) = ("/tmp/");
9.20 +"~~~~~ fun thes2file, args:"; val (p : filepath) = ("/tmp/");
9.21 (* recursively descend into thehier just before the error
9.22 by setting TESTids according to the last line in ouput
9.23 ### thes2file: id = : *)
9.24 @@ -123,7 +123,7 @@
9.25 (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
9.26 val (pa, ids, po', wfn, (Ptyp (id, [n], ns))) = ! TESTdump;
9.27 ;
9.28 -"~~~~~ fun thydata2file, args:"; val ((xmldata:path), (pos:pos), (theID:theID), thydata) =
9.29 +"~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:theID), thydata) =
9.30 (pa, po', (ids@[id]), n);
9.31 "~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
9.32 (theID:theID, thydata);
9.33 @@ -329,7 +329,7 @@
9.34 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
9.35 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
9.36 fun MINIget_the (theID : theID) = get_py MINIthehier theID theID (*see ptyps.sml*)
9.37 -fun MINIthy_hierarchy2file (path:path) =
9.38 +fun MINIthy_hierarchy2file (path:filepath) =
9.39 str2file (path ^ "thy_hierarchy.xml")
9.40 ("<NODE>\n" ^
9.41 " <ID> theory hierarchy </ID>\n" ^
9.42 @@ -337,7 +337,7 @@
9.43 " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
9.44 (hierarchy_guh MINIthehier) ^
9.45 "</NODE>");
9.46 -fun MINIthes2file (p : path) = thenodes p [] [0] thydata2file MINIthehier;
9.47 +fun MINIthes2file (p : filepath) = thenodes p [] [0] thydata2file MINIthehier;
9.48
9.49 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
9.50 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
9.51 @@ -359,7 +359,7 @@
9.52 "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");
9.53 "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
9.54 (path, [], [0], thydata2file, MINIthehier);
9.55 -"~~~~~ fun thenode, args:"; val ((pa : path), ids, po, wfn, (Ptyp (id, [n], ns))) =
9.56 +"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Ptyp (id, [n], ns))) =
9.57 (pa, ids, po, wfn, n);
9.58 val po' = lev_on po;
9.59 (*wfn pa po' (ids @ [id]) n -------------> writes xml to file; we want xml before written: *)
9.60 @@ -370,7 +370,7 @@
9.61 Hthm {guh = "thy_isac_Test_Build_Thydata-thm-thm111", mathauthors = ["isac-team"], ...}) => ()
9.62 | _ => error "a change inhibits successful continuation of this test";
9.63 val (theID, thydata) = hd thydata_list;
9.64 -"~~~~~ fun thydata2file, args:"; val ((path : path), (pos : pos), (theID : theID), thydata) =
9.65 +"~~~~~ fun thydata2file, args:"; val ((path : filepath), (pos : pos), (theID : theID), thydata) =
9.66 (pa, po', (*ids @ [id]*)theID, (*n*)thydata);
9.67 "~~~~~ fun thydata2xml, args:"; val ((theID, Hthm {guh, coursedesign, mathauthors, fillpats, thm}))=
9.68 ((theID, thydata));
10.1 --- a/test/Tools/isac/Minisubpbl/799-complete.sml Wed Nov 06 15:08:27 2019 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,47 +0,0 @@
10.4 -(* Title: "Minisubpbl/799-complete.sml"
10.5 - Author: Walther Neuper 1105
10.6 - (c) copyright due to lincense terms.
10.7 -*)
10.8 -"----------- Minisubpbl/799-complete.sml -------------------------";
10.9 -"----------- Minisubpbl/799-complete.sml -------------------------";
10.10 -"----------- Minisubpbl/799-complete.sml -------------------------";
10.11 - val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
10.12 - val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
10.13 - ["Test","squ-equ-test-subpbl1"]);
10.14 - val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.15 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.16 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.17 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.18 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.19 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.20 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.21 - (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
10.22 - (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
10.23 - (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
10.24 - (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
10.25 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
10.26 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
10.27 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
10.28 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
10.29 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
10.30 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
10.31 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
10.32 - (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
10.33 - (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
10.34 - (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
10.35 - (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
10.36 - (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
10.37 - (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
10.38 - (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
10.39 -
10.40 - (* final test ...*)
10.41 - if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'"
10.42 - andalso pr_ctree pr_short pt =
10.43 - ". ----- pblobj -----\n" ^
10.44 - "1. x + 1 = 2\n" ^
10.45 - "2. x + 1 + -1 * 2 = 0\n" ^
10.46 - "3. ----- pblobj -----\n" ^
10.47 - "3.1. -1 + x = 0\n" ^
10.48 - "3.2. x = 0 + -1 * -1\n" ^
10.49 - "4. [x = 1]\n"
10.50 - then () else error "re-build: fun locate_input_tactic changed";