1.1 --- a/src/Tools/isac/Interpret/mathengine.sml Tue May 03 16:23:07 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed May 04 09:01:10 2011 +0200
1.3 @@ -235,39 +235,34 @@
1.4 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
1.5 *)
1.6 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
1.7 - let val pIopt = get_pblID (pt,ip);
1.8 - in if (*p = ([],Res) orelse*) ip = ([],Res)
1.9 - then ("end-of-calculation",(tacis, [], ptp):calcstate') else
1.10 - case tacis of
1.11 - (_::_) =>
1.12 -(* val((tac,_,_)::_) = tacis;
1.13 - *)
1.14 - if ip = p (*the request is done where ptp waits for*)
1.15 - then let val (pt',c',p') = generate tacis (pt,[],p)
1.16 - in ("ok", (tacis, c', (pt', p'))) end
1.17 - else (case (if member op = [Pbl,Met] p_
1.18 - then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.19 - handle _ => ([],[],ptp)(*e.g.by Add_Given "equality///"*)
1.20 - of cs as ([],_,_) => ("helpless", cs)
1.21 - | cs => ("ok", cs))
1.22 -(* val [] = tacis;
1.23 - *)
1.24 - | _ => (case pIopt of
1.25 - NONE => ("no-fmz-spec", ([], [], ptp))
1.26 - | SOME pI =>
1.27 -(* val SOME pI = pIopt;
1.28 - val cs=(if member op = [Pbl,Met] p_ andalso is_none(get_obj g_env pt (fst p))
1.29 - then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.30 - handle _ => ([], ptp);
1.31 - *)
1.32 - (case (if member op = [Pbl,Met] p_
1.33 - andalso is_none (get_obj g_env pt (fst p))
1.34 - (*^^^^^^^^: Apply_Method without init_form*)
1.35 - then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip) )
1.36 - handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*)
1.37 - of cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
1.38 - | cs => ("ok", cs)))
1.39 - end;
1.40 + let val pIopt = get_pblID (pt,ip);
1.41 + in
1.42 + if (*p = ([],Res) orelse*) ip = ([],Res)
1.43 + then ("end-of-calculation",(tacis, [], ptp):calcstate')
1.44 + else
1.45 + case tacis of
1.46 + (_::_) =>
1.47 + if ip = p (*the request is done where ptp waits for*)
1.48 + then
1.49 + let val (pt',c',p') = generate tacis (pt,[],p)
1.50 + in ("ok", (tacis, c', (pt', p'))) end
1.51 + else (case (if member op = [Pbl,Met] p_
1.52 + then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.53 + handle _ => ([],[],ptp)(*e.g. Add_Given "equality///"*) of
1.54 + cs as ([],_,_) => ("helpless", cs)
1.55 + | cs => ("ok", cs))
1.56 + | _ => (case pIopt of
1.57 + NONE => ("no-fmz-spec", ([], [], ptp))
1.58 + | SOME pI =>
1.59 + (case (if member op = [Pbl,Met] p_
1.60 + andalso is_none (get_obj g_env pt (fst p))
1.61 + (*^^^^^^^^: Apply_Method without init_form*)
1.62 + then nxt_specify_ (pt,ip)
1.63 + else nxt_solve_ (pt,ip) )
1.64 + handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality///"*) of
1.65 + cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
1.66 + | cs => ("ok", cs)))
1.67 + end;
1.68
1.69 (* (nxt_solve_ (pt,ip)) handle e => print_exn e ;
1.70
1.71 @@ -462,29 +457,29 @@
1.72 (* val ((_,tac), p, _, pt) = (nxt, p, c, pt);
1.73 *)
1.74 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
1.75 - let val (pt, p) =
1.76 - (*locatetac is here for testing by me; step would suffice in me*)
1.77 + let
1.78 + val (pt, p) =
1.79 + (*locatetac is here for testing by me; step would suffice in me*)
1.80 case locatetac tac (pt,p) of
1.81 - ("ok", (_, _, ptp)) => ptp
1.82 - | ("unsafe-ok", (_, _, ptp)) => ptp
1.83 - | ("not-applicable",_) => (pt, p)
1.84 - | ("end-of-calculation", (_, _, ptp)) => ptp
1.85 - | ("failure",_) => error "sys-error";
1.86 - val (_, ts) = (*WN101102 NOT tested, if step would create _same_ ptp*)
1.87 + ("ok", (_, _, ptp)) => ptp
1.88 + | ("unsafe-ok", (_, _, ptp)) => ptp
1.89 + | ("not-applicable",_) => (pt, p)
1.90 + | ("end-of-calculation", (_, _, ptp)) => ptp
1.91 + | ("failure",_) => error "sys-error";
1.92 + val (_, ts) = (*WN101102 NOT tested, if step would create _same_ ptp*)
1.93 (case step p ((pt, e_pos'),[]) of
1.94 - ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
1.95 - | ("helpless",_) => ("helpless: cannot propose tac", [])
1.96 - | ("no-fmz-spec",_) => error "no-fmz-spec"
1.97 - | ("end-of-calculation", (ts, _, _)) => ("",ts))
1.98 + ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
1.99 + | ("helpless",_) => ("helpless: cannot propose tac", [])
1.100 + | ("no-fmz-spec",_) => error "no-fmz-spec"
1.101 + | ("end-of-calculation", (ts, _, _)) => ("",ts))
1.102 handle _ => error "sys-error";
1.103 - val tac = case ts of tacis as (_::_) =>
1.104 - let val (tac,_,_) = last_elem tacis
1.105 - in tac end
1.106 - | _ => if p = ([],Res) then End_Proof'
1.107 - else Empty_Tac;
1.108 + val tac =
1.109 + case ts of
1.110 + tacis as (_::_) => let val (tac,_,_) = last_elem tacis in tac end
1.111 + | _ => if p = ([],Res) then End_Proof' else Empty_Tac;
1.112 (*form output comes from locatetac*)
1.113 - in (p:pos', []:NEW, TESTg_form (pt, p),
1.114 - (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
1.115 + in (p:pos', []:NEW, TESTg_form (pt, p),
1.116 + (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
1.117
1.118 (*for quick test-print-out, until 'type inout' is removed*)
1.119 fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';