1.1 --- a/src/sml/ME/mathengine.sml Sat Aug 20 19:10:30 2005 +0200
1.2 +++ b/src/sml/ME/mathengine.sml Sat Aug 20 21:20:16 2005 +0200
1.3 @@ -1,15 +1,10 @@
1.4 -(* ME/mathengine.sml *)
1.5 -(* ~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
1.6 -(* The _functional_ mathematics engine, ie. without a state. Input and *)
1.7 -(* output are Isabelle's formulae as strings. *)
1.8 +(* The _functional_ mathematics engine, ie. without a state.
1.9 + Input and output are Isabelle's formulae as strings.
1.10 + (c) Walther Neuper 2000
1.11 + (c) Stefan Rath 2005
1.12
1.13 -
1.14 -(* sml-code for FE-interface
1.15 -
1.16 - use"../FE-interface/sml.sml";
1.17 - use"FE-interface/sml.sml";
1.18 - use"sml.sml";
1.19 - *)
1.20 +use"~/proto2/isac/src/sml/ME/mathengine.sml";
1.21 +*)
1.22
1.23 signature MATHENGINE =
1.24 sig
1.25 @@ -49,11 +44,6 @@
1.26 pos' ->
1.27 NEW ->
1.28 ptree -> pos' * NEW * mout * tac'_ * safe * ptree
1.29 - val meNEW :
1.30 - tac'_ ->
1.31 - pos' ->
1.32 - NEW ->
1.33 - ptree -> pos' * NEW * mout * tac'_ * safe * ptree
1.34
1.35 val nxt_specify_ : ptree * (int list * pos_) -> CalcHead.calcstate'
1.36 val step : pos' -> CalcHead.calcstate -> string * CalcHead.calcstate'
1.37 @@ -63,9 +53,10 @@
1.38
1.39
1.40
1.41 -
1.42 +(*
1.43 structure mathengine : MATHENGINE =
1.44 struct
1.45 +*)
1.46 fun get_pblID (pt, (p,_):pos') =
1.47 let val p' = par_pblobj pt p
1.48 val (_,pI,_) = get_obj g_spec pt p'
1.49 @@ -97,13 +88,9 @@
1.50 (* val (m, pos) = ((mI,m), ip);
1.51 val (m,(pt,pos) ) = ((mI,m), ptp);
1.52 *)
1.53 - (*val (p',_,f,tac,s,pt') = solve m pos pt;
1.54 -
1.55 - (writeln o istate2str) (get_istate pt' p');
1.56 - (term2str o fst) (get_obj g_result pt' (fst p'));
1.57 - *)
1.58 let val (*p,_,f,_,s,pt*) (msg, cs') = solve m (pt, pos)
1.59 -(* val (_,(pt',p')) = cs';
1.60 +(* val (msg, cs') = solve m (pt, pos);
1.61 + val (tacis,dels,(pt',p')) = cs';
1.62 (writeln o istate2str) (get_istate pt' p');
1.63 (term2str o fst) (get_obj g_result pt' (fst p'));
1.64 *)
1.65 @@ -119,8 +106,8 @@
1.66 (*report applicability of tac in tacis; pt is dropped in setNextTactic*)
1.67 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
1.68 | locatetac tac (ptp as (pt, p)) =
1.69 -(* val ptp as (pt, p) = (pt, p);
1.70 - val ptp as (pt, p) = (pt, ip);
1.71 +(* val ptp as (pt, p) = (pt, ip);
1.72 + val ptp as (pt, p) = (pt, p);
1.73 *)
1.74 let val (mI,m) = mk_tac'_ tac;
1.75 in case applicable_in p pt m of
1.76 @@ -236,8 +223,8 @@
1.77 (*.does a step forward; returns tactic used, ctree updated.*)
1.78 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
1.79 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
1.80 + val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
1.81 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
1.82 - val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
1.83 *)
1.84 let val pIopt = get_pblID (pt,ip);
1.85 in if p = ([],Res) orelse ip = ([],Res)
1.86 @@ -258,13 +245,13 @@
1.87 None => ("no-fmz-spec", ([], [], ptp))
1.88 | Some pI =>
1.89 (* val Some pI = pIopt;
1.90 - val cs = (if p_ mem [Pbl,Met]
1.91 + val cs = (if p_ mem [Pbl,Met] andalso is_none (get_obj g_env pt (fst p))
1.92 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.93 handle _ => ([], ptp);
1.94 *)
1.95 (case (if p_ mem [Pbl,Met]
1.96 andalso is_none (get_obj g_env pt (fst p))
1.97 - (*........: no Apply_Method without init_form*)
1.98 + (*........: Apply_Method without init_form*)
1.99 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.100 handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*)
1.101 of cs as ([],_,_) => ("helpless", cs)
1.102 @@ -423,10 +410,10 @@
1.103 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
1.104
1.105
1.106 -fun meNEW ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
1.107 +fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
1.108 (* val (_,tac) = nxt;
1.109 *) let val (pt, p) =
1.110 -(* val (eee, (tacis, (pt',p'))) = locatetac tac (pt,p);
1.111 +(* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p);
1.112 (writeln o (itms2str thy)) (get_obj g_pbl pt' (fst p'));
1.113 writeln( istate2str (get_istate pt' ([3],Res)));
1.114 term2str (fst (get_obj g_result pt' [3]));
1.115 @@ -454,11 +441,8 @@
1.116 else Empty_Tac;
1.117 in (p:pos',[]:NEW, TESTg_form (pt, p),
1.118 (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
1.119 -
1.120 -(********************************************************************)
1.121 -(****************) val me = meNEW; (*********************************)
1.122 -(********************************************************************)
1.123 -
1.124 +(*
1.125 end
1.126
1.127 open mathengine;
1.128 +*)
1.129 \ No newline at end of file