1.1 --- a/src/Tools/isac/Interpret/mathengine.sml Mon Dec 19 09:02:41 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Mon Dec 19 10:37:44 2016 +0100
1.3 @@ -9,11 +9,11 @@
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 * Ctree.mout * tac'_ * safe * ptree
1.8 + val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Generate.mout * tac'_ * safe * ptree
1.9 val autocalc :
1.10 - pos' list -> pos' -> (ptree * pos') * Ctree.taci list -> auto -> string * pos' list * (ptree * pos')
1.11 + pos' list -> pos' -> (ptree * pos') * Generate.taci list -> auto -> string * pos' list * (ptree * pos')
1.12 val locatetac :
1.13 - tac -> ptree * (posel list * pos_) -> string * (Ctree.taci list * pos' list * (ptree * pos'))
1.14 + tac -> ptree * (posel list * pos_) -> string * (Generate.taci list * pos' list * (ptree * pos'))
1.15 val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
1.16 val detailstep :
1.17 ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
1.18 @@ -30,8 +30,8 @@
1.19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.20 type nxt_
1.21 type lOc_
1.22 - val CalcTreeTEST : fmz list -> pos' * NEW * Ctree.mout * (string * tac) * safe * ptree
1.23 - val f2str : Ctree.mout -> cterm'
1.24 + val CalcTreeTEST : fmz list -> pos' * NEW * Generate.mout * (string * tac) * safe * ptree
1.25 + val f2str : Generate.mout -> cterm'
1.26 val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_
1.27 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.28 end
1.29 @@ -62,7 +62,7 @@
1.30 let
1.31 val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
1.32 in
1.33 - case f of (Ctree.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
1.34 + case f of (Generate.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
1.35 end
1.36
1.37 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
1.38 @@ -195,7 +195,7 @@
1.39 (_::_) =>
1.40 if ip = p (*the request is done where ptp waits for*)
1.41 then
1.42 - let val (pt',c',p') = Ctree.generate tacis (pt,[],p)
1.43 + let val (pt',c',p') = Generate.generate tacis (pt,[],p)
1.44 in ("ok", (tacis, c', (pt', p'))) end
1.45 else (case (if member op = [Pbl, Met] p_
1.46 then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip))
1.47 @@ -368,10 +368,10 @@
1.48 val (form, _, _) = Chead.pt_extract ptp
1.49 in
1.50 case form of
1.51 - Form t => Ctree.FormKF (term2str t)
1.52 + Form t => Generate.FormKF (term2str t)
1.53 | ModSpec (_, p_, _, gfr, pre, _) =>
1.54 - Ctree.PpcKF (
1.55 - (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method []
1.56 + Generate.PpcKF (
1.57 + (case p_ of Pbl => Generate.Problem [] | Met => Generate.Method []
1.58 | _ => error "TESTg_form: uncovered case",
1.59 Specify.itms2itemppc (assoc_thy"Isac") gfr pre))
1.60 end
1.61 @@ -422,6 +422,6 @@
1.62 end
1.63
1.64 (* for quick test-print-out, until 'type inout' is removed *)
1.65 -fun f2str (Ctree.FormKF cterm') = cterm';
1.66 +fun f2str (Generate.FormKF cterm') = cterm';
1.67
1.68 end