1 (* ME/mathengine.sml *) |
1 (* The _functional_ mathematics engine, ie. without a state. |
2 (* ~~~~~~~~~~~~~~~~~~~~~~~~~~ *) |
2 Input and output are Isabelle's formulae as strings. |
3 (* The _functional_ mathematics engine, ie. without a state. Input and *) |
3 (c) Walther Neuper 2000 |
4 (* output are Isabelle's formulae as strings. *) |
4 (c) Stefan Rath 2005 |
5 |
5 |
6 |
6 use"~/proto2/isac/src/sml/ME/mathengine.sml"; |
7 (* sml-code for FE-interface |
7 *) |
8 |
|
9 use"../FE-interface/sml.sml"; |
|
10 use"FE-interface/sml.sml"; |
|
11 use"sml.sml"; |
|
12 *) |
|
13 |
8 |
14 signature MATHENGINE = |
9 signature MATHENGINE = |
15 sig |
10 sig |
16 type nxt_ |
11 type nxt_ |
17 (* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *) |
12 (* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *) |
47 val me : |
42 val me : |
48 tac'_ -> |
43 tac'_ -> |
49 pos' -> |
44 pos' -> |
50 NEW -> |
45 NEW -> |
51 ptree -> pos' * NEW * mout * tac'_ * safe * ptree |
46 ptree -> pos' * NEW * mout * tac'_ * safe * ptree |
52 val meNEW : |
|
53 tac'_ -> |
|
54 pos' -> |
|
55 NEW -> |
|
56 ptree -> pos' * NEW * mout * tac'_ * safe * ptree |
|
57 |
47 |
58 val nxt_specify_ : ptree * (int list * pos_) -> CalcHead.calcstate' |
48 val nxt_specify_ : ptree * (int list * pos_) -> CalcHead.calcstate' |
59 val step : pos' -> CalcHead.calcstate -> string * CalcHead.calcstate' |
49 val step : pos' -> CalcHead.calcstate -> string * CalcHead.calcstate' |
60 val trymatch : pblID -> ptree -> int list * 'a -> ptform |
50 val trymatch : pblID -> ptree -> int list * 'a -> ptform |
61 val tryrefine : pblID -> ptree -> int list * 'a -> ptform |
51 val tryrefine : pblID -> ptree -> int list * 'a -> ptform |
62 end |
52 end |
63 |
53 |
64 |
54 |
65 |
55 |
66 |
56 (* |
67 structure mathengine : MATHENGINE = |
57 structure mathengine : MATHENGINE = |
68 struct |
58 struct |
|
59 *) |
69 fun get_pblID (pt, (p,_):pos') = |
60 fun get_pblID (pt, (p,_):pos') = |
70 let val p' = par_pblobj pt p |
61 let val p' = par_pblobj pt p |
71 val (_,pI,_) = get_obj g_spec pt p' |
62 val (_,pI,_) = get_obj g_spec pt p' |
72 val (_,(_,oI,_),_) = get_obj g_origin pt p' |
63 val (_,(_,oI,_),_) = get_obj g_origin pt p' |
73 in if pI <> e_pblID then Some pI |
64 in if pI <> e_pblID then Some pI |
95 |
86 |
96 fun loc_solve_ m (pt,pos) = |
87 fun loc_solve_ m (pt,pos) = |
97 (* val (m, pos) = ((mI,m), ip); |
88 (* val (m, pos) = ((mI,m), ip); |
98 val (m,(pt,pos) ) = ((mI,m), ptp); |
89 val (m,(pt,pos) ) = ((mI,m), ptp); |
99 *) |
90 *) |
100 (*val (p',_,f,tac,s,pt') = solve m pos pt; |
|
101 |
|
102 (writeln o istate2str) (get_istate pt' p'); |
|
103 (term2str o fst) (get_obj g_result pt' (fst p')); |
|
104 *) |
|
105 let val (*p,_,f,_,s,pt*) (msg, cs') = solve m (pt, pos) |
91 let val (*p,_,f,_,s,pt*) (msg, cs') = solve m (pt, pos) |
106 (* val (_,(pt',p')) = cs'; |
92 (* val (msg, cs') = solve m (pt, pos); |
|
93 val (tacis,dels,(pt',p')) = cs'; |
107 (writeln o istate2str) (get_istate pt' p'); |
94 (writeln o istate2str) (get_istate pt' p'); |
108 (term2str o fst) (get_obj g_result pt' (fst p')); |
95 (term2str o fst) (get_obj g_result pt' (fst p')); |
109 *) |
96 *) |
110 in case msg of |
97 in case msg of |
111 "ok" => Updated cs' |
98 "ok" => Updated cs' |
117 | Nexts of calcstate; (**) |
104 | Nexts of calcstate; (**) |
118 |
105 |
119 (*report applicability of tac in tacis; pt is dropped in setNextTactic*) |
106 (*report applicability of tac in tacis; pt is dropped in setNextTactic*) |
120 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp)) |
107 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp)) |
121 | locatetac tac (ptp as (pt, p)) = |
108 | locatetac tac (ptp as (pt, p)) = |
122 (* val ptp as (pt, p) = (pt, p); |
109 (* val ptp as (pt, p) = (pt, ip); |
123 val ptp as (pt, p) = (pt, ip); |
110 val ptp as (pt, p) = (pt, p); |
124 *) |
111 *) |
125 let val (mI,m) = mk_tac'_ tac; |
112 let val (mI,m) = mk_tac'_ tac; |
126 in case applicable_in p pt m of |
113 in case applicable_in p pt m of |
127 Notappl e => ("not-applicable", ([],[], ptp):calcstate') |
114 Notappl e => ("not-applicable", ([],[], ptp):calcstate') |
128 | Appl m => |
115 | Appl m => |
234 ------------------------------------------------------------------*) |
221 ------------------------------------------------------------------*) |
235 |
222 |
236 (*.does a step forward; returns tactic used, ctree updated.*) |
223 (*.does a step forward; returns tactic used, ctree updated.*) |
237 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) = |
224 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) = |
238 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1); |
225 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1); |
|
226 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs); |
239 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[])); |
227 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[])); |
240 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs); |
|
241 *) |
228 *) |
242 let val pIopt = get_pblID (pt,ip); |
229 let val pIopt = get_pblID (pt,ip); |
243 in if p = ([],Res) orelse ip = ([],Res) |
230 in if p = ([],Res) orelse ip = ([],Res) |
244 then ("end-of-calculation",(tacis, [], ptp):calcstate') else |
231 then ("end-of-calculation",(tacis, [], ptp):calcstate') else |
245 case tacis of |
232 case tacis of |
256 | cs => ("ok", cs)) |
243 | cs => ("ok", cs)) |
257 | _ => (case pIopt of |
244 | _ => (case pIopt of |
258 None => ("no-fmz-spec", ([], [], ptp)) |
245 None => ("no-fmz-spec", ([], [], ptp)) |
259 | Some pI => |
246 | Some pI => |
260 (* val Some pI = pIopt; |
247 (* val Some pI = pIopt; |
261 val cs = (if p_ mem [Pbl,Met] |
248 val cs = (if p_ mem [Pbl,Met] andalso is_none (get_obj g_env pt (fst p)) |
262 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip)) |
249 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip)) |
263 handle _ => ([], ptp); |
250 handle _ => ([], ptp); |
264 *) |
251 *) |
265 (case (if p_ mem [Pbl,Met] |
252 (case (if p_ mem [Pbl,Met] |
266 andalso is_none (get_obj g_env pt (fst p)) |
253 andalso is_none (get_obj g_env pt (fst p)) |
267 (*........: no Apply_Method without init_form*) |
254 (*........: Apply_Method without init_form*) |
268 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip)) |
255 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip)) |
269 handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*) |
256 handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*) |
270 of cs as ([],_,_) => ("helpless", cs) |
257 of cs as ([],_,_) => ("helpless", cs) |
271 | cs => ("ok", cs))) |
258 | cs => ("ok", cs))) |
272 end; |
259 end; |
421 (*ENDE TESTPHASE 08/10.03: |
408 (*ENDE TESTPHASE 08/10.03: |
422 NEW loeschen, eigene Version von locatetac, step |
409 NEW loeschen, eigene Version von locatetac, step |
423 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *) |
410 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *) |
424 |
411 |
425 |
412 |
426 fun meNEW ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) = |
413 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) = |
427 (* val (_,tac) = nxt; |
414 (* val (_,tac) = nxt; |
428 *) let val (pt, p) = |
415 *) let val (pt, p) = |
429 (* val (eee, (tacis, (pt',p'))) = locatetac tac (pt,p); |
416 (* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p); |
430 (writeln o (itms2str thy)) (get_obj g_pbl pt' (fst p')); |
417 (writeln o (itms2str thy)) (get_obj g_pbl pt' (fst p')); |
431 writeln( istate2str (get_istate pt' ([3],Res))); |
418 writeln( istate2str (get_istate pt' ([3],Res))); |
432 term2str (fst (get_obj g_result pt' [3])); |
419 term2str (fst (get_obj g_result pt' [3])); |
433 val (pt,p) = (pt',p'); |
420 val (pt,p) = (pt',p'); |
434 *) |
421 *) |
452 val tac = case ts of ((tac,_,_)::_) => tac |
439 val tac = case ts of ((tac,_,_)::_) => tac |
453 | _ => if p = ([],Res) then End_Proof' |
440 | _ => if p = ([],Res) then End_Proof' |
454 else Empty_Tac; |
441 else Empty_Tac; |
455 in (p:pos',[]:NEW, TESTg_form (pt, p), |
442 in (p:pos',[]:NEW, TESTg_form (pt, p), |
456 (tac2IDstr tac, tac):tac'_, Sundef, pt) end; |
443 (tac2IDstr tac, tac):tac'_, Sundef, pt) end; |
457 |
444 (* |
458 (********************************************************************) |
|
459 (****************) val me = meNEW; (*********************************) |
|
460 (********************************************************************) |
|
461 |
|
462 end |
445 end |
463 |
446 |
464 open mathengine; |
447 open mathengine; |
|
448 *) |