1.1 --- a/src/Tools/isac/Frontend/interface.sml Sat Oct 09 16:20:02 2010 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Sun Oct 10 14:15:43 2010 +0200
1.3 @@ -60,15 +60,15 @@
1.4 struct
1.5 (*------------------------------------------------------------------*)
1.6
1.7 -(*.encode "Isabelle"-strings as seen by the user to the
1.8 +(* encode "Isabelle"-strings as seen by the user to the
1.9 format accepted by Isabelle.
1.10 encode "^" ---> "^^^"; see Knowledge/Atools.thy;
1.11 called for each cterm', icalhd, fmz in this interface;
1.12 - + see "fun decode" in xmlsrc/mathml.sml.*)
1.13 -fun encode (str:cterm') =
1.14 + + see "fun decode" in xmlsrc/mathml.sml *)
1.15 +fun encode (str : cterm') =
1.16 let fun enc [] = []
1.17 - | enc ("^"::cs) = "^"::"^"::"^"::(enc cs)
1.18 - | enc (c::cs) = c::(enc cs)
1.19 + | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
1.20 + | enc (c :: cs) = c :: (enc cs)
1.21 in (implode o enc o explode) str:cterm' end;
1.22 fun encode_imodel (imodel:imodel) =
1.23 let fun enc (Given ifos) = Given (map encode ifos)
1.24 @@ -77,7 +77,7 @@
1.25 in map enc imodel:imodel end;
1.26 fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) =
1.27 (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;
1.28 -fun encode_fmz ((ifos, spec):fmz) = (map encode ifos, spec):fmz;
1.29 +fun encode_fmz ((ifos, spec) : fmz) = (map encode ifos, spec) : fmz;
1.30
1.31
1.32 (***. CalcTree .***)
1.33 @@ -98,21 +98,7 @@
1.34
1.35 (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
1.36 compare "fun CalcTreeTEST" which does NOT decode.*)
1.37 -fun CalcTree
1.38 - [(fmz, sp):fmz] (*for several variants lateron*) =
1.39 -(* val[(fmz,sp):fmz]=[(["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
1.40 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.41 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.42 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.43 - "boundVariable a","boundVariable b","boundVariable alpha",
1.44 - "interval {x::real. 0 <= x & x <= 2*r}",
1.45 - "interval {x::real. 0 <= x & x <= 2*r}",
1.46 - "interval {x::real. 0 <= x & x <= pi}",
1.47 - "errorBound (eps=(0::real))"],
1.48 - ("DiffApp.thy", ["maximum_of","function"],
1.49 - ["DiffApp","max_by_calculus"]))];
1.50 -
1.51 - *)
1.52 +fun CalcTree [(fmz, sp) : fmz] (*for several variants lateron*) =
1.53 (let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))
1.54 (*FIXME.WN.8.03: error-handling missing*)
1.55 val cI = add_calc cs
1.56 @@ -586,16 +572,8 @@
1.57
1.58
1.59
1.60 -(*.replace a formula with_in_ a calculation;
1.61 - this situation applies for initial CAS-commands, too.*)
1.62 -(* val (cI, ifo) = (2, "-1 + x = 0");
1.63 - val (cI, ifo) = (1, "-1 + x = 0");
1.64 - val (cI, ifo) = (1, "x - 1 = 0");
1.65 - val (cI, ifo) = (1, "x = 1");
1.66 - val (cI, ifo) = (1, "solve(x+1=2,x)");
1.67 - val (cI, ifo) = (1, "Simplify (2*a + 3*a)");
1.68 - val (cI, ifo) = (1, "Diff (x^2 + x + 1, x)");
1.69 - *)
1.70 +(* replace a formula with_in_ a calculation;
1.71 + this situation applies for initial CAS-commands, too *)
1.72 fun replaceFormula cI (ifo:cterm') =
1.73 (let val ((pt, _), _) = get_calc cI
1.74 val p = get_pos cI 1
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Sat Oct 09 16:20:02 2010 +0200
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Sun Oct 10 14:15:43 2010 +0200
2.3 @@ -1568,12 +1568,10 @@
2.4
2.5
2.6
2.7 -(*.create a calc-tree with oris via an cas.refined pbl.*)
2.8 -fun nxt_specify_init_calc (([],(dI,pI,mI)): fmz) =
2.9 -(* val ([],(dI,pI,mI)) = (fmz, sp);
2.10 - *)
2.11 - if pI <> [] then (*comes from pbl-browser*)
2.12 - let val {cas,met,ppc,thy,...} = get_pbt pI
2.13 +(* create a calc-tree with oris via an cas.refined pbl *)
2.14 +fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
2.15 + if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
2.16 + let val {cas, met, ppc, thy, ...} = get_pbt pI
2.17 val dI = if dI = "" then theory2theory' thy else dI
2.18 val thy = assoc_thy dI
2.19 val mI = if mI = [] then hd met else mI
2.20 @@ -1583,8 +1581,8 @@
2.21 val pt = update_spec pt [] (dI,pI,mI)
2.22 val pits = init_pbl' ppc
2.23 val pt = update_pbl pt [] pits
2.24 - in ((pt,([],Pbl)), []): calcstate end
2.25 - else if mI <> [] then (*comes from met-browser*)
2.26 + in ((pt, ([] ,Pbl)), []) : calcstate end
2.27 + else if mI <> [] then (* from met-browser *)
2.28 let val {ppc,...} = get_met mI
2.29 val dI = if dI = "" then "Isac" else dI
2.30 val thy = assoc_thy dI
2.31 @@ -1593,13 +1591,11 @@
2.32 val pt = update_spec pt [] (dI,pI,mI)
2.33 val mits = init_pbl' ppc
2.34 val pt = update_met pt [] mits
2.35 - in ((pt,([],Met)), []) end
2.36 - else (*completely new example*)
2.37 + in ((pt, ([], Met)), []) : calcstate end
2.38 + else (* new example, pepare for interactive modeling *)
2.39 let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec)
2.40 ([], e_spec, e_term)
2.41 - in ((pt,([],Pbl)), []) end
2.42 -(* val (fmz, (dI,pI,mI)) = (fmz, sp);
2.43 - *)
2.44 + in ((pt,([],Pbl)), []) : calcstate end
2.45 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
2.46 let (* both """"""""""""""""""""""""" either empty or complete *)
2.47 val thy = assoc_thy dI
2.48 @@ -1617,8 +1613,10 @@
2.49 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
2.50 ~~~ vals_of_oris pors) t
2.51 val (pt, _) = cappend_problem e_ptree [] e_istate (fmz, (dI, pI, mI))
2.52 - (pors, (dI, pI, mI), hdl)
2.53 - in ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) end;
2.54 + (pors, (dI, pI, mI), hdl)
2.55 + in ((pt, ([], Pbl)),
2.56 + fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
2.57 + end;
2.58
2.59
2.60
3.1 --- a/src/Tools/isac/Test_Isac.thy Sat Oct 09 16:20:02 2010 +0200
3.2 +++ b/src/Tools/isac/Test_Isac.thy Sun Oct 10 14:15:43 2010 +0200
3.3 @@ -66,7 +66,9 @@
3.4 use"thy-hierarchy.sml";
3.5 cd "../..";
3.6 cd"smltest/FE-interface";
3.7 - use"interface.sml";
3.8 +*)
3.9 +use"../../../test/Tools/isac/Frontend/interface.sml"; (**)
3.10 +(*
3.11 cd "../..";
3.12 *)
3.13 ML{* writeln "**** run tests on math-engine complete ******************" *};
3.14 @@ -94,10 +96,7 @@
3.15 use"logexp.sml";
3.16 use"diff.sml";
3.17 *)
3.18 -use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*)
3.19 -
3.20 -ML {*111*}
3.21 -
3.22 +use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*all done*)
3.23 (*
3.24 use"eqsystem.sml";
3.25 *)
3.26 @@ -148,8 +147,14 @@
3.27 (*=== inhibit exn ?=============================================================
3.28 ===== inhibit exn ?===========================================================*)
3.29
3.30 +
3.31 (*========== inhibit exn =======================================================
3.32 +
3.33 +"########### testcode inserted vvv ###########################################";
3.34 +"########### testcode inserted ^^^ ###########################################";
3.35 +
3.36 ============ inhibit exn =====================================================*)
3.37
3.38 +
3.39 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
3.40 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
4.1 --- a/src/Tools/isac/calcelems.sml Sat Oct 09 16:20:02 2010 +0200
4.2 +++ b/src/Tools/isac/calcelems.sml Sun Oct 10 14:15:43 2010 +0200
4.3 @@ -550,8 +550,10 @@
4.4
4.5 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
4.6 handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
4.7 -fun assoc_thy (thy:theory') = (*FIXME100818 abolish*)
4.8 - (theory thy) handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
4.9 +fun assoc_thy (thy:theory') =
4.10 + if thy = "e_domID" then (theory "Script") (*lower bound of Knowledge*)
4.11 + else (theory thy)
4.12 + handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
4.13
4.14 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
4.15 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
5.1 --- a/test/Tools/isac/Frontend/interface.sml Sat Oct 09 16:20:02 2010 +0200
5.2 +++ b/test/Tools/isac/Frontend/interface.sml Sun Oct 10 14:15:43 2010 +0200
5.3 @@ -7,7 +7,8 @@
5.4 use"interface.sml";
5.5 *)
5.6
5.7 - print_depth 3;
5.8 +print_depth 3;
5.9 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
5.10
5.11 "-----------------------------------------------------------------";
5.12 "table of contents -----------------------------------------------";
5.13 @@ -84,6 +85,8 @@
5.14 refFormula 1 (get_pos 1 1);
5.15 (*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
5.16
5.17 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
5.18 +
5.19
5.20 "---------------- solve_linear as rootpbl FE ---------------------";
5.21 "---------------- solve_linear as rootpbl FE ---------------------";
5.22 @@ -97,8 +100,18 @@
5.23 Iterator 1; (*create an active Iterator on CalcTree No.1*)
5.24
5.25 moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
5.26 +"########### testcode inserted vvv ###########################################";
5.27 +states ;
5.28 +(*========== inhibit exn =======================================================
5.29 +(get_pos 1 1);
5.30 +GOON
5.31 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
5.32 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
5.33 +
5.34 +"########### testcode inserted ^^^ ###########################################";
5.35 refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
5.36
5.37 +
5.38 fetchProposedTactic 1 (*by using Iterator No.1*);
5.39 setNextTactic 1 (Model_Problem (*["linear","univariate","equation","test"]*));
5.40 (*by using Iterator No.1*)
5.41 @@ -1347,3 +1360,4 @@
5.42 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
5.43
5.44
5.45 +============ inhibit exn =====================================================*)
6.1 --- a/test/Tools/isac/Knowledge/integrate.sml Sat Oct 09 16:20:02 2010 +0200
6.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sun Oct 10 14:15:43 2010 +0200
6.3 @@ -31,7 +31,6 @@
6.4 "--------------------------------------------------------";
6.5
6.6
6.7 -
6.8 "----------- parsing ------------------------------------";
6.9 "----------- parsing ------------------------------------";
6.10 "----------- parsing ------------------------------------";
6.11 @@ -567,11 +566,9 @@
6.12 *** ((Integral (?u + ?v) D ?bdv) =
6.13 *** ((Integral ?u D ?bdv) + (Integral ?v D ?bdv)))
6.14 *)
6.15 -
6.16 if existpt' ([1,1,5], Res) pt then ()
6.17 else error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
6.18
6.19 -(*=== inhibit exn ==============================================================
6.20
6.21 "----------- CAS input ----------------------------------";
6.22 "----------- CAS input ----------------------------------";
6.23 @@ -592,7 +589,8 @@
6.24 show_pt pt;
6.25 (* WN070703 does not work like Diff due to error in next-pos
6.26 if p = ([], Res) andalso term2str res = "5 * a" then ()
6.27 -else error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
6.28 +else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
6.29 +
6.30 +WN101010 this test produced <SYSERROR>.."error in kernel" already in CVS-version
6.31 +from 2007; not touched since then.
6.32 *)
6.33 -
6.34 -===== inhibit exn ============================================================*)