1.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed Dec 21 08:57:47 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed Dec 21 09:21:26 2016 +0100
1.3 @@ -9,9 +9,9 @@
1.4 signature MATH_ENGINE =
1.5 sig
1.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
1.7 - val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Generate.mout * tac'_ * safe * ptree
1.8 + val me : Solve.tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Generate.mout * Solve.tac'_ * safe * ptree
1.9 val autocalc :
1.10 - pos' list -> pos' -> (ptree * pos') * Generate.taci list -> auto -> string * pos' list * (ptree * pos')
1.11 + pos' list -> pos' -> (ptree * pos') * Generate.taci list -> Solve.auto -> string * pos' list * (ptree * pos')
1.12 val locatetac :
1.13 tac -> ptree * (posel list * pos_) -> string * (Generate.taci list * pos' list * (ptree * pos'))
1.14 val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
1.15 @@ -68,7 +68,7 @@
1.16 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
1.17 fun loc_solve_ m (pt, pos) =
1.18 let
1.19 - val (msg, cs') = solve m (pt, pos);
1.20 + val (msg, cs') = Solve.solve m (pt, pos);
1.21 in
1.22 case msg of "ok" => Updated cs' | msg => ERror msg
1.23 end
1.24 @@ -82,13 +82,13 @@
1.25 fun locatetac _ (ptp as (_, ([], Res))) = ("end-of-calculation", ([], [], ptp))
1.26 | locatetac tac (ptp as (pt, p)) =
1.27 let
1.28 - val (mI, m) = mk_tac'_ tac;
1.29 + val (mI, m) = Solve.mk_tac'_ tac;
1.30 in
1.31 case Applicable.applicable_in p pt m of
1.32 Chead.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
1.33 | Chead.Appl m =>
1.34 let
1.35 - val x = if member op = specsteps mI
1.36 + val x = if member op = Solve.specsteps mI
1.37 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
1.38 in
1.39 case x of
1.40 @@ -129,7 +129,7 @@
1.41 in
1.42 case tac of
1.43 Apply_Method mI =>
1.44 - nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.45 + Solve.nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.46 | _ => Chead.nxt_specif tac ptp
1.47 end
1.48 end
1.49 @@ -198,7 +198,7 @@
1.50 let val (pt',c',p') = Generate.generate tacis (pt,[],p)
1.51 in ("ok", (tacis, c', (pt', p'))) end
1.52 else (case (if member op = [Pbl, Met] p_
1.53 - then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip))
1.54 + then nxt_specify_ (pt, ip) else Solve.nxt_solve_ (pt, ip))
1.55 handle ERROR msg => (writeln ("*** " ^ msg);
1.56 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
1.57 cs as ([],_,_) => ("helpless", cs)
1.58 @@ -208,7 +208,7 @@
1.59 | SOME _ => (*vvvvvv: Apply_Method without init_form*)
1.60 (case if member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
1.61 then nxt_specify_ (pt, ip)
1.62 - else (nxt_solve_ (pt,ip))
1.63 + else (Solve.nxt_solve_ (pt,ip))
1.64 handle ERROR msg => (writeln ("*** " ^ msg);
1.65 ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
1.66 cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
1.67 @@ -221,7 +221,7 @@
1.68 TODO.WN0512 ? redesign after the phases have been more separated
1.69 at the fron-end in 05:
1.70 eg. CompleteCalcHead could be done by a separate fun !!!*)
1.71 -fun autocalc c ip cs (Step s) =
1.72 +fun autocalc c ip cs (Solve.Step s) =
1.73 if s <= 1
1.74 then
1.75 let val (str, (_, c', ptp)) = step ip cs; (* autoord = 1, probably does 1 step too much*)
1.76 @@ -230,14 +230,14 @@
1.77 let val (str, (_, c', ptp as (_, p))) = step ip cs;
1.78 in
1.79 if str = "ok"
1.80 - then autocalc (c@c') p (ptp, []) (Step (s - 1))
1.81 + then autocalc (c@c') p (ptp, []) (Solve.Step (s - 1))
1.82 else (str, c@c', ptp) end
1.83 (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
1.84 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
1.85 - if autoord auto > 3 andalso just_created (pt, pos)
1.86 + if Solve.autoord auto > 3 andalso just_created (pt, pos)
1.87 then
1.88 let val ptp = Chead.all_modspec (pt, pos);
1.89 - in all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
1.90 + in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
1.91 else
1.92 if member op = [Pbl, Met] p_
1.93 then
1.94 @@ -245,26 +245,26 @@
1.95 then
1.96 let val ptp = Chead.complete_mod (pt, pos) (*... auto = 2 | 3 *)
1.97 in
1.98 - if autoord auto < 3 then ("ok", c, ptp)
1.99 + if Solve.autoord auto < 3 then ("ok", c, ptp)
1.100 else
1.101 if not (Chead.is_complete_spec ptp)
1.102 then
1.103 let val ptp = Chead.complete_spec ptp
1.104 in
1.105 - if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
1.106 + if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
1.107 end
1.108 - else if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
1.109 + else if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
1.110 end
1.111 else
1.112 if not (Chead.is_complete_spec (pt,pos))
1.113 then
1.114 let val ptp = Chead.complete_spec (pt, pos)
1.115 in
1.116 - if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
1.117 + if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
1.118 end
1.119 else
1.120 - if autoord auto = 3 then ("ok", c, (pt, pos)) else all_solve auto c (pt, pos)
1.121 - else complete_solve auto c (pt, pos);
1.122 + if Solve.autoord auto = 3 then ("ok", c, (pt, pos)) else Solve.all_solve auto c (pt, pos)
1.123 + else Solve.complete_solve auto c (pt, pos);
1.124
1.125 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
1.126 if no pbl has been specified, take the init from origin.*)
1.127 @@ -351,7 +351,7 @@
1.128 if null cn
1.129 then
1.130 if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
1.131 - then detailrls pt pos
1.132 + then Solve.detailrls pt pos
1.133 else ("no-Rewrite_Set...", EmptyPtree, e_pos')
1.134 else ("donesteps", pt, (p @ [length (children (get_nd pt p))], Res))
1.135 end;
1.136 @@ -418,7 +418,7 @@
1.137 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
1.138 | _ => if p = ([], Res) then End_Proof' else Empty_Tac;
1.139 in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
1.140 - (tac2IDstr tac, tac):tac'_, Sundef, pt)
1.141 + (tac2IDstr tac, tac): Solve.tac'_, Sundef, pt)
1.142 end
1.143
1.144 (* for quick test-print-out, until 'type inout' is removed *)