1.1 --- a/src/sml/FE-interface/interface.sml Thu Oct 19 17:35:39 2006 +0200
1.2 +++ b/src/sml/FE-interface/interface.sml Sun Oct 22 10:28:37 2006 +0200
1.3 @@ -531,11 +531,14 @@
1.4 end)
1.5 handle _ => sysERROR2xml cI "error in kernel";
1.6
1.7 +(*.replace a formula with_in_ a calculation;
1.8 + this situation applies for initial CAS-commands, too.*)
1.9 (* val (cI, ifo) = (2, "-1 + x = 0");
1.10 val (cI, ifo) = (1, "-1 + x = 0");
1.11 val (cI, ifo) = (1, "x - 1 = 0");
1.12 val (cI, ifo) = (1, "x = 1");
1.13 val (cI, ifo) = (1, "solve(x+1=2,x)");
1.14 + val (cI, ifo) = (1, "Simplify (2*a + 3*a)");
1.15 *)
1.16 fun replaceFormula cI (ifo:cterm') =
1.17 (let val ((pt, _), _) = get_calc cI
2.1 --- a/src/sml/IsacKnowledge/Simplify.ML Thu Oct 19 17:35:39 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Simplify.ML Sun Oct 22 10:28:37 2006 +0200
2.3 @@ -39,3 +39,25 @@
2.4 crls = e_rls, nrls = e_rls},
2.5 "empty_script"
2.6 ));
2.7 +
2.8 +(** CAS-command **)
2.9 +
2.10 +(*.function for handling the cas-input "Simplify (2*a + 3*a)":
2.11 + make a model which is already in ptree-internal format.*)
2.12 +(* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
2.13 + val (h,argl) = strip_comb ((term_of o the o (parse thy))
2.14 + "Simplify (2*a + 3*a)");
2.15 + *)
2.16 +fun argl2dtss t =
2.17 + [((term_of o the o (parse thy)) "term", t),
2.18 + ((term_of o the o (parse thy)) "normalform",
2.19 + [(term_of o the o (parse thy)) "N"])
2.20 + ]
2.21 + | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";
2.22 +
2.23 +castab :=
2.24 +overwritel (!castab,
2.25 + [((term_of o the o (parse thy)) "Simplify",
2.26 + (("Isac.thy", ["simplification"], ["no_met"]),
2.27 + argl2dtss))
2.28 + ]);
3.1 --- a/src/sml/ME/inform.sml Thu Oct 19 17:35:39 2006 +0200
3.2 +++ b/src/sml/ME/inform.sml Sun Oct 22 10:28:37 2006 +0200
3.3 @@ -173,7 +173,7 @@
3.4
3.5 (*.check if the input term is a CAScmd and return a ptree with
3.6 a _complete_ calchead.*)
3.7 -(* val hdt =
3.8 +(* val hdt = ifo;
3.9 *)
3.10 fun cas_input hdt =
3.11 let val (h,argl) = strip_comb hdt
3.12 @@ -185,7 +185,7 @@
3.13 in (pt, (false, Pbl, e_term(*FIXXME031:'not found'*),
3.14 [], [], e_spec)) end*)
3.15 | Some (spec as (dI,_,_), argl2dtss) =>
3.16 - (* val Some (spec, argl2dtss ) = assoc (!castab, h);
3.17 + (* val Some (spec as (dI,_,_), argl2dtss ) = assoc (!castab, h);
3.18 *)
3.19 let val dtss = argl2dtss argl
3.20 val (pI, pits, mI, mits, pre) = cas_input_ spec dtss
3.21 @@ -674,9 +674,9 @@
3.22 val ifo = str2term ifo;
3.23
3.24 val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
3.25 - (([],[],(pt,p)), "solve(x+1=2,x)");
3.26 + (cs', encode ifo);
3.27 val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
3.28 - (cs', encode ifo);
3.29 + (([],[],(pt,p)), (encode ifo));
3.30 *)
3.31 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
3.32 case parse (assoc_thy "Isac.thy") istr of
4.1 --- a/src/sml/xmlsrc/datatypes.sml Thu Oct 19 17:35:39 2006 +0200
4.2 +++ b/src/sml/xmlsrc/datatypes.sml Sun Oct 22 10:28:37 2006 +0200
4.3 @@ -629,7 +629,9 @@
4.4 indt j ^"<CALCFORMULA>\n"^
4.5 pos'2xml (j+i) ("POSITION", p) ^
4.6 indt (j+i) ^"<FORMULA>\n"^
4.7 - (if t = e_pblterm then "" else term2xml (j+i) t^"\n") ^
4.8 + (if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
4.9 + then "________________________________________________________________"
4.10 + else term2xml (j+i) t^"\n") ^
4.11 indt (j+i) ^"</FORMULA>\n"^
4.12 indt j ^"</CALCFORMULA>\n";
4.13
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/smltest/IsacKnowledge/simplify.sml Sun Oct 22 10:28:37 2006 +0200
5.3 @@ -0,0 +1,53 @@
5.4 +(* tests on simplification
5.5 + author: Walther Neuper
5.6 + 061019
5.7 + (c) due to copyright terms
5.8 +
5.9 +use"../smltest/IsacKnowledge/simplify.sml";
5.10 +use"simplify.sml";
5.11 +*)
5.12 +val thy = Simplify.thy;
5.13 +
5.14 +"-----------------------------------------------------------------";
5.15 +"table of contents -----------------------------------------------";
5.16 +"-----------------------------------------------------------------";
5.17 +"----------- CAS-command Simplify --------------------------------";
5.18 +"-----------------------------------------------------------------";
5.19 +"-----------------------------------------------------------------";
5.20 +"-----------------------------------------------------------------";
5.21 +
5.22 +
5.23 +
5.24 +"----------- CAS-command Simplify --------------------------------";
5.25 +"----------- CAS-command Simplify --------------------------------";
5.26 +"----------- CAS-command Simplify --------------------------------";
5.27 +states:=[];
5.28 +CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
5.29 +Iterator 1;
5.30 +moveActiveRoot 1;
5.31 +replaceFormula 1 "Simplify (2*a + 3*a)";
5.32 +autoCalculate 1 CompleteCalc;
5.33 +val ((pt,p),_) = get_calc 1;
5.34 +val Form res = (#1 o pt_extract) (pt, ([],Res));
5.35 +show_pt pt;
5.36 +if p = ([], Res) andalso term2str res = "5 * a" then ()
5.37 +else raise error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
5.38 +
5.39 +
5.40 +
5.41 +
5.42 +
5.43 +
5.44 +
5.45 +
5.46 +
5.47 +
5.48 +
5.49 +
5.50 +
5.51 +
5.52 +
5.53 +
5.54 +
5.55 +
5.56 +
6.1 --- a/src/smltest/ME/inform.sml Thu Oct 19 17:35:39 2006 +0200
6.2 +++ b/src/smltest/ME/inform.sml Sun Oct 22 10:28:37 2006 +0200
6.3 @@ -464,7 +464,6 @@
6.4 else raise error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
6.5
6.6
6.7 -
6.8 "--------- inform [rational,simplification] ----------------------";
6.9 "--------- inform [rational,simplification] ----------------------";
6.10 "--------- inform [rational,simplification] ----------------------";