58 (*------------------------------------------------------------------*) |
58 (*------------------------------------------------------------------*) |
59 structure interface : INTERFACE = |
59 structure interface : INTERFACE = |
60 struct |
60 struct |
61 (*------------------------------------------------------------------*) |
61 (*------------------------------------------------------------------*) |
62 |
62 |
63 (*.encode "Isabelle"-strings as seen by the user to the |
63 (* encode "Isabelle"-strings as seen by the user to the |
64 format accepted by Isabelle. |
64 format accepted by Isabelle. |
65 encode "^" ---> "^^^"; see Knowledge/Atools.thy; |
65 encode "^" ---> "^^^"; see Knowledge/Atools.thy; |
66 called for each cterm', icalhd, fmz in this interface; |
66 called for each cterm', icalhd, fmz in this interface; |
67 + see "fun decode" in xmlsrc/mathml.sml.*) |
67 + see "fun decode" in xmlsrc/mathml.sml *) |
68 fun encode (str:cterm') = |
68 fun encode (str : cterm') = |
69 let fun enc [] = [] |
69 let fun enc [] = [] |
70 | enc ("^"::cs) = "^"::"^"::"^"::(enc cs) |
70 | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs) |
71 | enc (c::cs) = c::(enc cs) |
71 | enc (c :: cs) = c :: (enc cs) |
72 in (implode o enc o explode) str:cterm' end; |
72 in (implode o enc o explode) str:cterm' end; |
73 fun encode_imodel (imodel:imodel) = |
73 fun encode_imodel (imodel:imodel) = |
74 let fun enc (Given ifos) = Given (map encode ifos) |
74 let fun enc (Given ifos) = Given (map encode ifos) |
75 | enc (Find ifos) = Find (map encode ifos) |
75 | enc (Find ifos) = Find (map encode ifos) |
76 | enc (Relate ifos) = Relate (map encode ifos) |
76 | enc (Relate ifos) = Relate (map encode ifos) |
77 in map enc imodel:imodel end; |
77 in map enc imodel:imodel end; |
78 fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) = |
78 fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) = |
79 (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd; |
79 (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd; |
80 fun encode_fmz ((ifos, spec):fmz) = (map encode ifos, spec):fmz; |
80 fun encode_fmz ((ifos, spec) : fmz) = (map encode ifos, spec) : fmz; |
81 |
81 |
82 |
82 |
83 (***. CalcTree .***) |
83 (***. CalcTree .***) |
84 |
84 |
85 (** add and delete users **) |
85 (** add and delete users **) |
96 (*fun DEconstructIterator (cI:calcID) (uI:iterID) = |
96 (*fun DEconstructIterator (cI:calcID) (uI:iterID) = |
97 deluserOK2xml (del_user cI uI);*) |
97 deluserOK2xml (del_user cI uI);*) |
98 |
98 |
99 (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^; |
99 (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^; |
100 compare "fun CalcTreeTEST" which does NOT decode.*) |
100 compare "fun CalcTreeTEST" which does NOT decode.*) |
101 fun CalcTree |
101 fun CalcTree [(fmz, sp) : fmz] (*for several variants lateron*) = |
102 [(fmz, sp):fmz] (*for several variants lateron*) = |
|
103 (* val[(fmz,sp):fmz]=[(["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]", |
|
104 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", |
|
105 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", |
|
106 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", |
|
107 "boundVariable a","boundVariable b","boundVariable alpha", |
|
108 "interval {x::real. 0 <= x & x <= 2*r}", |
|
109 "interval {x::real. 0 <= x & x <= 2*r}", |
|
110 "interval {x::real. 0 <= x & x <= pi}", |
|
111 "errorBound (eps=(0::real))"], |
|
112 ("DiffApp.thy", ["maximum_of","function"], |
|
113 ["DiffApp","max_by_calculus"]))]; |
|
114 |
|
115 *) |
|
116 (let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp)) |
102 (let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp)) |
117 (*FIXME.WN.8.03: error-handling missing*) |
103 (*FIXME.WN.8.03: error-handling missing*) |
118 val cI = add_calc cs |
104 val cI = add_calc cs |
119 in calctreeOK2xml cI end) |
105 in calctreeOK2xml cI end) |
120 handle _ => sysERROR2xml 0 "error in kernel"; |
106 handle _ => sysERROR2xml 0 "error in kernel"; |
584 end) |
570 end) |
585 handle _ => sysERROR2xml cI "error in kernel"; |
571 handle _ => sysERROR2xml cI "error in kernel"; |
586 |
572 |
587 |
573 |
588 |
574 |
589 (*.replace a formula with_in_ a calculation; |
575 (* replace a formula with_in_ a calculation; |
590 this situation applies for initial CAS-commands, too.*) |
576 this situation applies for initial CAS-commands, too *) |
591 (* val (cI, ifo) = (2, "-1 + x = 0"); |
|
592 val (cI, ifo) = (1, "-1 + x = 0"); |
|
593 val (cI, ifo) = (1, "x - 1 = 0"); |
|
594 val (cI, ifo) = (1, "x = 1"); |
|
595 val (cI, ifo) = (1, "solve(x+1=2,x)"); |
|
596 val (cI, ifo) = (1, "Simplify (2*a + 3*a)"); |
|
597 val (cI, ifo) = (1, "Diff (x^2 + x + 1, x)"); |
|
598 *) |
|
599 fun replaceFormula cI (ifo:cterm') = |
577 fun replaceFormula cI (ifo:cterm') = |
600 (let val ((pt, _), _) = get_calc cI |
578 (let val ((pt, _), _) = get_calc cI |
601 val p = get_pos cI 1 |
579 val p = get_pos cI 1 |
602 in case inform (([], [], (pt, p)): calcstate') (encode ifo) of |
580 in case inform (([], [], (pt, p)): calcstate') (encode ifo) of |
603 ("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) => |
581 ("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) => |