1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Nov 21 12:47:02 2016 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Nov 22 10:42:21 2016 +0100
1.3 @@ -75,7 +75,7 @@
1.4 *} ML {*
1.5 *}
1.6 ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
1.7 -ML {* me; (*from "Interpret/mathengine.sml"*) *}
1.8 +ML {* Math_Engine.me; (*from "Interpret/mathengine.sml"*) *}
1.9 ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}
1.10 ML {* print_exn_unit *}
1.11 ML {* list_rls (*from Atools.thy WN130615??? or ProgLang???*) *}
2.1 --- a/src/Tools/isac/Frontend/interface.sml Mon Nov 21 12:47:02 2016 +0100
2.2 +++ b/src/Tools/isac/Frontend/interface.sml Tue Nov 22 10:42:21 2016 +0100
2.3 @@ -56,7 +56,7 @@
2.4 val setNextTactic : calcID -> tac -> XML.tree
2.5 val setProblem : calcID -> pblID -> XML.tree
2.6 val setTheory : calcID -> thyID -> XML.tree
2.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*
2.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.9 (* NONE *)
2.10 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.11 end
2.12 @@ -123,7 +123,7 @@
2.13 val ((pt, _), _) = get_calc cI (* retrieve calcstate from states *)
2.14 val ip = get_pos cI 1 (* retrieve position from states *)
2.15 in
2.16 - case locatetac tac (pt, ip) of
2.17 + case Math_Engine.locatetac tac (pt, ip) of
2.18 ("ok", (tacis, _, _)) => (* update calcstate in states *)
2.19 (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
2.20 | ("unsafe-ok", (tacis, _, _)) =>
2.21 @@ -140,7 +140,7 @@
2.22 val ((pt, _), _) = get_calc cI
2.23 val p = get_pos cI 1
2.24 in
2.25 - case locatetac tac (pt, ip) of
2.26 + case Math_Engine.locatetac tac (pt, ip) of
2.27 ("ok", (_, c, ptp as (_, p'))) =>
2.28 (upd_calc cI (ptp, []);
2.29 upd_ipos cI 1 p';
2.30 @@ -157,7 +157,7 @@
2.31 end;
2.32
2.33 fun fetchProposedTactic (cI:calcID) =
2.34 - (case step (get_pos cI 1) (get_calc cI) of
2.35 + (case Math_Engine.step (get_pos cI 1) (get_calc cI) of
2.36 ("ok", (tacis, _, _)) =>
2.37 let
2.38 val _= upd_tacis cI tacis
2.39 @@ -172,7 +172,7 @@
2.40 fun autoCalculate (cI:calcID) auto = (*Future.fork
2.41 (fn () => (( *)let
2.42 val pold = get_pos cI 1
2.43 - val x = autocalc [] pold (get_calc cI) auto
2.44 + val x = Math_Engine.autocalc [] pold (get_calc cI) auto
2.45 in
2.46 case x of
2.47 ("ok", c, ptp as (_,p)) =>
2.48 @@ -272,7 +272,7 @@
2.49 "may have intermediate steps above them")
2.50 else
2.51 let val ip' = lev_pred' pt ip
2.52 - in case detailstep pt ip of
2.53 + in case Math_Engine.detailstep pt ip of
2.54 ("detailrls", pt, lastpos) =>
2.55 (upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)
2.56 | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
2.57 @@ -327,7 +327,7 @@
2.58 val subs = subs_from is "dummy" guh
2.59 val tac = guh2rewtac guh subs
2.60 in
2.61 - case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
2.62 + case Math_Engine.locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
2.63 ("ok", (tacis, c, ptp as (_, p))) =>
2.64 (upd_calc cI ((pt, p), []);
2.65 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
2.66 @@ -356,7 +356,7 @@
2.67 in
2.68 if member op = [Pbl, Met] p_
2.69 then
2.70 - let val (pt, chd) = set_problem pI (pt, ip)
2.71 + let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)
2.72 in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.73 else sysERROR2xml cI "setContext for pbl requires ActiveFormula on CalcHead"
2.74 end
2.75 @@ -368,7 +368,7 @@
2.76 in
2.77 if member op = [Pbl, Met] p_
2.78 then
2.79 - let val (pt, chd) = set_method mI (pt, ip)
2.80 + let val (pt, chd) = Math_Engine.set_method mI (pt, ip)
2.81 in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.82 else sysERROR2xml cI "setContext for met requires ActiveFormula on CalcHead"
2.83 end
2.84 @@ -384,7 +384,7 @@
2.85 in
2.86 if member op = [Pbl,Met] p_
2.87 then
2.88 - let val (pt, chd) = set_method mI (pt, ip)
2.89 + let val (pt, chd) = Math_Engine.set_method mI (pt, ip)
2.90 in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.91 else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
2.92 end
2.93 @@ -399,7 +399,7 @@
2.94 in
2.95 if member op = [Pbl,Met] p_
2.96 then
2.97 - let val (pt, chd) = set_problem pI (pt, ip)
2.98 + let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)
2.99 in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.100 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
2.101 end
2.102 @@ -414,7 +414,7 @@
2.103 in
2.104 if member op = [Pbl,Met] p_
2.105 then
2.106 - let val (pt, chd) = set_theory tI (pt, ip)
2.107 + let val (pt, chd) = Math_Engine.set_theory tI (pt, ip)
2.108 in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.109 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
2.110 end
2.111 @@ -427,7 +427,7 @@
2.112 val pblID = guh2kestoreID guh
2.113 val ((pt,_),_) = get_calc cI
2.114 val pp = par_pblobj pt p
2.115 - val chd = tryrefine pblID pt (pp, p_)
2.116 + val chd = Math_Engine.tryrefine pblID pt (pp, p_)
2.117 in contextpblOK2xml cI chd end)
2.118 handle _ => sysERROR2xml cI "error in kernel 16";
2.119
2.120 @@ -437,7 +437,7 @@
2.121 val cs = get_calc cI
2.122 val pos = get_pos cI 1
2.123 in
2.124 - case step pos cs of
2.125 + case Math_Engine.step pos cs of
2.126 ("ok", cs') =>
2.127 (case inform cs' (encode ifo) of
2.128 ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>
2.129 @@ -581,7 +581,7 @@
2.130 end
2.131 else if is_curr_endof_calc pt pos
2.132 then
2.133 - case step pos cs of
2.134 + case Math_Engine.step pos cs of
2.135 ("ok", (tacis, _, (pt, _))) =>
2.136 let val tac = fst3 (last_elem tacis)
2.137 in
2.138 @@ -597,14 +597,14 @@
2.139 ((let
2.140 val ((pt, _), _) = get_calc cI
2.141 val pp = par_pblobj pt p
2.142 - val chd = initcontext_pbl pt (pp,p_)
2.143 + val chd = Math_Engine.initcontext_pbl pt (pp,p_)
2.144 in contextpblOK2xml cI chd end)
2.145 handle _ => sysERROR2xml cI "error in kernel 32")
2.146 | initContext cI Met_ (p, p_) =
2.147 ((let
2.148 val ((pt,_),_) = get_calc cI
2.149 val pp = par_pblobj pt p
2.150 - val chd = initcontext_met pt (pp,p_)
2.151 + val chd = Math_Engine.initcontext_met pt (pp,p_)
2.152 in contextmetOK2xml cI chd end)
2.153 handle _ => sysERROR2xml cI "error in kernel 33");
2.154
2.155 @@ -634,7 +634,7 @@
2.156 val ((pt, _), _) = get_calc cI
2.157 val pp = par_pblobj pt p
2.158 val keID = guh2kestoreID guh
2.159 - val chd = context_pbl keID pt pp
2.160 + val chd = Math_Engine.context_pbl keID pt pp
2.161 in contextpblOK2xml cI chd end
2.162 ) handle _ => sysERROR2xml cI "error in kernel 35")
2.163 | "met_" =>
2.164 @@ -642,7 +642,7 @@
2.165 val ((pt, _), _) = get_calc cI
2.166 val pp = par_pblobj pt p
2.167 val keID = guh2kestoreID guh
2.168 - val chd = context_met keID pt pp
2.169 + val chd = Math_Engine.context_met keID pt pp
2.170 in contextmetOK2xml cI chd end
2.171 ) handle _ => sysERROR2xml cI "error in kernel 36")
2.172 | str => sysERROR2xml cI ("checkContext: str = " ^ str)
2.173 @@ -694,7 +694,7 @@
2.174 ("ok", tac) =>
2.175 let
2.176 in (* cp from applyTactic *)
2.177 - case locatetac tac (pt, pos) of
2.178 + case Math_Engine.locatetac tac (pt, pos) of
2.179 ("ok", (_, c, ptp as (_,p'))) =>
2.180 (upd_calc cI (ptp, []);
2.181 upd_ipos cI 1 p';
3.1 --- a/src/Tools/isac/Interpret/mathengine.sml Mon Nov 21 12:47:02 2016 +0100
3.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Tue Nov 22 10:42:21 2016 +0100
3.3 @@ -6,185 +6,185 @@
3.4 use"mathengine.sml";
3.5 *)
3.6
3.7 -signature MATHENGINE =
3.8 - sig
3.9 - type nxt_
3.10 - (* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *)
3.11 - type NEW
3.12 - type lOc_
3.13 - (*datatype
3.14 - lOc_ =
3.15 - ERror of string
3.16 - | UNsafe of CalcHead.calcstate'
3.17 - | Updated of CalcHead.calcstate' *)
3.18 +signature MATH_ENGINE =
3.19 +sig
3.20 + type NEW (* TODO: refactor "fun me" with calcstate and remove *)
3.21 + val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * mout * tac'_ * safe * ptree
3.22 + val autocalc :
3.23 + pos' list -> pos' -> (ptree * pos') * taci list -> auto -> string * pos' list * (ptree * pos')
3.24 + val locatetac :
3.25 + tac -> ptree * (posel list * pos_) -> string * (taci list * pos' list * (ptree * pos'))
3.26 + val step : pos' -> calcstate -> string * calcstate'
3.27 + val detailstep :
3.28 + ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
3.29
3.30 - val CalcTreeTEST :
3.31 - fmz list ->
3.32 - pos' * NEW * mout * (string * tac) * safe * ptree
3.33 + val initcontext_met : ptree -> pos' -> bool * string list * scr * itm list * (bool * term) list
3.34 + val initcontext_pbl : ptree -> pos' -> bool * string list * term * itm list * (bool * term) list
3.35 + val context_met : metID -> ptree -> pos -> bool * metID * scr * itm list * (bool * term) list
3.36 + val context_pbl : pblID -> ptree -> pos -> bool * pblID * term * itm list * (bool * term) list
3.37 + val set_method : metID -> ptree * pos' -> ptree * ocalhd
3.38 + val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
3.39 + val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
3.40 + val tryrefine : pblID -> ptree -> pos' -> bool * pblID * term * itm list * (bool * term) list
3.41
3.42 - val TESTg_form : ptree * (int list * pos_) -> mout
3.43 - val autocalc :
3.44 - pos' list ->
3.45 - pos' ->
3.46 - (ptree * pos') * taci list ->
3.47 - auto -> string * pos' list * (ptree * pos')
3.48 - val detailstep : ptree -> pos' -> string * ptree * pos'
3.49 - (* val e_tac_ : tac_ *)
3.50 - val f2str : mout -> cterm'
3.51 - (* val get_pblID : ptree * pos' -> pblID option *)
3.52 - val initmatch : ptree -> pos' -> ptform
3.53 - (* val loc_solve_ :
3.54 - string * tac_ -> ptree * (int list * pos_) -> lOc_ *)
3.55 - (* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *)
3.56 - val locatetac : (*tests only*)
3.57 - tac ->
3.58 - ptree * (posel list * pos_) ->
3.59 - string * (taci list * pos' list * (ptree * (posel list * pos_)))
3.60 - val me :
3.61 - tac'_ ->
3.62 - pos' ->
3.63 - NEW ->
3.64 - ptree -> pos' * NEW * mout * tac'_ * safe * ptree
3.65 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.66 + type nxt_
3.67 + type lOc_
3.68 + val CalcTreeTEST : fmz list -> pos' * NEW * mout * (string * tac) * safe * ptree
3.69 + val f2str : mout -> cterm'
3.70 + val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_
3.71 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.72 +end
3.73
3.74 - val nxt_specify_ : ptree * (int list * pos_) -> calcstate'(*tests only*)
3.75 - val set_method : metID -> ptree * pos' -> ptree * ocalhd
3.76 - val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
3.77 - val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
3.78 - val step : pos' -> calcstate -> string * calcstate'
3.79 - val trymatch : pblID -> ptree -> pos' -> ptform
3.80 - val tryrefine : pblID -> ptree -> pos' -> ptform
3.81 - end
3.82 +(**)
3.83 +structure Math_Engine(**): MATH_ENGINE(**) =
3.84 +struct
3.85 +(**)
3.86
3.87 +fun get_pblID (pt, (p, _):pos') =
3.88 + let val p' = par_pblobj pt p
3.89 + val (_, pI, _) = get_obj g_spec pt p'
3.90 + val (_, (_, oI, _), _) = get_obj g_origin pt p'
3.91 + in
3.92 + if pI <> e_pblID
3.93 + then SOME pI
3.94 + else
3.95 + if oI <> e_pblID then SOME oI else NONE end;
3.96
3.97 -
3.98 -(*------------------------------------------------------------------(**)
3.99 -structure MathEngine : MATHENGINE =
3.100 -struct
3.101 -(**)------------------------------------------------------------------*)
3.102 -
3.103 -fun get_pblID (pt, (p,_):pos') =
3.104 - let val p' = par_pblobj pt p
3.105 - val (_,pI,_) = get_obj g_spec pt p'
3.106 - val (_,(_,oI,_),_) = get_obj g_origin pt p'
3.107 - in if pI <> e_pblID then SOME pI
3.108 - else if oI <> e_pblID then SOME oI
3.109 - else NONE end;
3.110 -(*fun get_pblID (pt, (p,_):pos') =
3.111 - ((snd3 o (get_obj g_spec pt)) (par_pblobj pt p));*)
3.112 -
3.113 -
3.114 -(*--vvv--dummies for test*)
3.115 -val e_tac_ = Tac_ (Pure.thy,"","","");
3.116 +(* introduced for test only *)
3.117 +val e_tac_ = Tac_ (Pure.thy, "", "", "");
3.118 datatype lOc_ =
3.119 ERror of string (*after loc_specify, loc_solve*)
3.120 | UNsafe of calcstate' (*after loc_specify, loc_solve*)
3.121 -| Updated of calcstate'; (*after loc_specify, loc_solve*)
3.122 +| Updated of calcstate'; (*after loc_specify, loc_solve*)
3.123 +
3.124 fun loc_specify_ m (pt,pos) =
3.125 -(* val pos = ip;
3.126 - *)
3.127 - let val (p,_,f,_,s,pt) = specify m pos [] pt;
3.128 -(* val (_,_,_,_,_,pt')= specify m pos [] pt;
3.129 - *)
3.130 - in case f of
3.131 - (Error' (Error_ e)) => ERror e
3.132 - | _ => Updated ([], [], (pt,p)) end;
3.133 + let
3.134 + val (p, _, f, _, _, pt) = specify m pos [] pt;
3.135 + in
3.136 + case f of (Error' (Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
3.137 + end
3.138
3.139 -(*. TODO push return-value cs' into solve and rename solve->loc_solve?_? .*)
3.140 -(* val (m, pos) = ((mI,m), ip);
3.141 - val (m,(pt,pos) ) = ((mI,m), ptp);
3.142 - *)
3.143 -fun loc_solve_ m (pt,pos) =
3.144 - let val (msg, cs') = solve m (pt, pos);
3.145 -(* val (tacis,dels,(pt',p')) = cs';
3.146 - (tracing o istate2str) (get_istate pt' p');
3.147 - (term2str o fst) (get_obj g_result pt' (fst p'));
3.148 - *)
3.149 - in case msg of
3.150 - "ok" => Updated cs'
3.151 - | msg => ERror msg
3.152 - end;
3.153 +(* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
3.154 +fun loc_solve_ m (pt, pos) =
3.155 + let
3.156 + val (msg, cs') = solve m (pt, pos);
3.157 + in
3.158 + case msg of "ok" => Updated cs' | msg => ERror msg
3.159 + end
3.160
3.161 datatype nxt_ =
3.162 - HElpless (**)
3.163 - | Nexts of calcstate; (**)
3.164 + HElpless (**)
3.165 +| Nexts of calcstate; (**)
3.166
3.167 -(*. locate a tactic in a script and apply it if possible .*)
3.168 -(*report applicability of tac in tacis; pt is dropped in setNextTactic*)
3.169 -fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
3.170 +(* locate a tactic in a script and apply it if possible;
3.171 + report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
3.172 +fun locatetac _ (ptp as (_, ([], Res))) = ("end-of-calculation", ([], [], ptp))
3.173 | locatetac tac (ptp as (pt, p)) =
3.174 - let val (mI,m) = mk_tac'_ tac;
3.175 - in case applicable_in p pt m of
3.176 - Notappl e => ("not-applicable", ([],[], ptp):calcstate')
3.177 - | Appl m =>
3.178 - let
3.179 - val x = if member op = specsteps mI
3.180 - then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
3.181 - in case x of
3.182 - ERror e => ("failure", ([], [], ptp))
3.183 - (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
3.184 - | UNsafe cs' => ("unsafe-ok", cs')
3.185 - | Updated (cs' as (_,_,(_,p'))) => (*ev.SEVER.tacs like Begin_Trans*)
3.186 - (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
3.187 - (*for SEVER.tacs user to ask ? *)
3.188 - end
3.189 - end;
3.190 + let
3.191 + val (mI, m) = mk_tac'_ tac;
3.192 + in
3.193 + case applicable_in p pt m of
3.194 + Notappl _ => ("not-applicable", ([],[], ptp):calcstate')
3.195 + | Appl m =>
3.196 + let
3.197 + val x = if member op = specsteps mI
3.198 + then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
3.199 + in
3.200 + case x of
3.201 + ERror _ => ("failure", ([], [], ptp))
3.202 + (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
3.203 + | UNsafe cs' => ("unsafe-ok", cs')
3.204 + | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
3.205 + (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
3.206 + (*for SEVER.tacs user to ask ? *)
3.207 + end
3.208 + end
3.209
3.210 -(*iterated by nxt_me; there (the resulting) ptp dropped
3.211 - may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
3.212 -fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
3.213 - let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
3.214 - probl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
3.215 +(* iterated by nxt_me; there (the resulting) ptp dropped
3.216 + may call nxt_solve Apply_Method --- thus evaluated here after solve.sml *)
3.217 +fun nxt_specify_ (ptp as (pt, (p, p_))) =
3.218 + let
3.219 + val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
3.220 + case get_obj I pt p of
3.221 + pblobj as (PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
3.222 + probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
3.223 + | PrfObj _ => error "nxt_specify_: not on PrfObj"
3.224 in
3.225 if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
3.226 then
3.227 case mI' of
3.228 - ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
3.229 + ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
3.230 | _ => nxt_specif Model_Problem (pt, (p,Pbl))
3.231 else
3.232 let
3.233 val cpI = if pI = e_pblID then pI' else pI;
3.234 - val cmI = if mI = e_metID then mI' else mI;
3.235 - val {ppc, prls, where_, ...} = get_pbt cpI;
3.236 - val pre = check_preconds "thy 100820" prls where_ probl;
3.237 - val pb = foldl and_ (true, map fst pre);
3.238 - (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
3.239 - val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
3.240 - (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
3.241 - in case tac of
3.242 - Apply_Method mI =>
3.243 - nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
3.244 - | _ => nxt_specif tac ptp end
3.245 - end;
3.246 + val cmI = if mI = e_metID then mI' else mI;
3.247 + val {ppc, prls, where_, ...} = get_pbt cpI;
3.248 + val pre = check_preconds "thy 100820" prls where_ probl;
3.249 + val pb = foldl and_ (true, map fst pre);
3.250 + (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
3.251 + val (_, tac) =
3.252 + nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
3.253 + in
3.254 + case tac of
3.255 + Apply_Method mI =>
3.256 + nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
3.257 + | _ => nxt_specif tac ptp
3.258 + end
3.259 + end
3.260
3.261 -(*.specify a new method;
3.262 - WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*)
3.263 +(* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
3.264 fun set_method (mI:metID) ptp =
3.265 - let val ([(_, Specify_Method' (_, _, mits), _)], [], (pt, pos as (p,_))) =
3.266 - nxt_specif (Specify_Method mI) ptp
3.267 - val pre = [] (*...from Specify_Method'*)
3.268 - val complete = true (*...from Specify_Method'*)
3.269 - (*from Specify_Method' ? vvv, vvv ?*)
3.270 - val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
3.271 - in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end;
3.272 + let
3.273 + val (mits, pt, p) =
3.274 + case nxt_specif (Specify_Method mI) ptp of
3.275 + ([(_, Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p)
3.276 + | _ => error "set_method: case 1 uncovered"
3.277 + val pre = [] (*...from Specify_Method'*)
3.278 + val complete = true (*...from Specify_Method'*)
3.279 + (*from Specify_Method' ? vvv, vvv ?*)
3.280 + val (hdf, spec) =
3.281 + case get_obj I pt p of
3.282 + PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
3.283 + | PrfObj _ => error "set_method: case 2 uncovered"
3.284 + in
3.285 + (pt, (complete, Met, hdf, mits, pre, spec) : ocalhd)
3.286 + end
3.287
3.288 -(*.specify a new problem;
3.289 - WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*)
3.290 +(* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
3.291 fun set_problem pI (ptp: ptree * pos') =
3.292 - let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
3.293 - _, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp
3.294 - (*from Specify_Problem' ? vvv, vvv ?*)
3.295 - val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
3.296 - in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
3.297 + let
3.298 + val (complete, pits, pre, pt, p) =
3.299 + case nxt_specif (Specify_Problem pI) ptp of
3.300 + ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
3.301 + => (complete, pits, pre, pt, p)
3.302 + | _ => error "set_problem: case 1 uncovered"
3.303 + (*from Specify_Problem' ? vvv, vvv ?*)
3.304 + val (hdf, spec) =
3.305 + case get_obj I pt p of
3.306 + PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
3.307 + | PrfObj _ => error "set_problem: case 2 uncovered"
3.308 + in
3.309 + (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd)
3.310 + end
3.311
3.312 fun set_theory (tI:thyID) (ptp: ptree * pos') =
3.313 - let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
3.314 - _, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp
3.315 - (*from Specify_Theory' ? vvv, vvv ?*)
3.316 - val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
3.317 - in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
3.318 + let
3.319 + val (complete, pits, pre, pt, p) =
3.320 + case nxt_specif (Specify_Theory tI) ptp of
3.321 + ([(_, Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
3.322 + => (complete, pits, pre, pt, p)
3.323 + | _ => error "set_theory: case 1 uncovered"
3.324 + (*from Specify_Theory' ? vvv, vvv ?*)
3.325 + val (hdf, spec) =
3.326 + case get_obj I pt p of
3.327 + PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
3.328 + | PrfObj _ => error "set_theory: case 2 uncovered"
3.329 + in (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd) end;
3.330
3.331 (* does a step forward; returns tactic used, ctree updated.
3.332 -TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
3.333 + TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
3.334 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
3.335 let val pIopt = get_pblID (pt,ip);
3.336 in
3.337 @@ -192,194 +192,198 @@
3.338 then ("end-of-calculation", (tacis, [], ptp):calcstate')
3.339 else
3.340 case tacis of
3.341 - (_::_) =>
3.342 + (_::_) =>
3.343 if ip = p (*the request is done where ptp waits for*)
3.344 - then
3.345 + then
3.346 let val (pt',c',p') = generate tacis (pt,[],p)
3.347 - in ("ok", (tacis, c', (pt', p'))) end
3.348 - else (case (if member op = [Pbl,Met] p_
3.349 - then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
3.350 - handle ERROR msg => (writeln ("*** " ^ msg);
3.351 - ([],[],ptp))(*e.g. Add_Given "equality///"*) of
3.352 - cs as ([],_,_) => ("helpless", cs)
3.353 - | cs => ("ok", cs))
3.354 - | _ => (case pIopt of
3.355 - NONE => ("no-fmz-spec", ([], [], ptp))
3.356 - | SOME pI =>
3.357 - (case if member op = [Pbl,Met] p_
3.358 - andalso is_none (get_obj g_env pt (fst p))
3.359 - (*^^^^^^^^: Apply_Method without init_form*)
3.360 - then nxt_specify_ (pt, ip)
3.361 - else (nxt_solve_ (pt,ip) )
3.362 - handle ERROR msg => (writeln ("*** " ^ msg);
3.363 - ([],[],ptp))(*e.g. Add_Given "equality///"*) of
3.364 - cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
3.365 - | cs => ("ok", cs)))
3.366 - end;
3.367 + in ("ok", (tacis, c', (pt', p'))) end
3.368 + else (case (if member op = [Pbl, Met] p_
3.369 + then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip))
3.370 + handle ERROR msg => (writeln ("*** " ^ msg);
3.371 + ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
3.372 + cs as ([],_,_) => ("helpless", cs)
3.373 + | cs => ("ok", cs))
3.374 + | _ => (case pIopt of
3.375 + NONE => ("no-fmz-spec", ([], [], ptp))
3.376 + | SOME _ => (*vvvvvv: Apply_Method without init_form*)
3.377 + (case if member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
3.378 + then nxt_specify_ (pt, ip)
3.379 + else (nxt_solve_ (pt,ip))
3.380 + handle ERROR msg => (writeln ("*** " ^ msg);
3.381 + ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
3.382 + cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
3.383 + | cs => ("ok", cs)))
3.384 + end
3.385
3.386 -(*.does several steps within one calculation as given by "type auto";
3.387 +(* does several steps within one calculation as given by "type auto";
3.388 the steps may arbitrarily go into and leave different phases,
3.389 - i.e. specify-phase and solve-phase.*)
3.390 -(*TODO.WN0512 ? redesign after the phases have been more separated
3.391 - at the fron-end in 05:
3.392 - eg. CompleteCalcHead could be done by a separate fun !!!*)
3.393 -fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
3.394 + i.e. specify-phase and solve-phase
3.395 + TODO.WN0512 ? redesign after the phases have been more separated
3.396 + at the fron-end in 05:
3.397 + eg. CompleteCalcHead could be done by a separate fun !!!*)
3.398 +fun autocalc c ip cs (Step s) =
3.399 if s <= 1
3.400 - then let val (str, (_, c', ptp)) = step ip cs;(*1*)
3.401 - (*at least does 1 step, ev.1 too much*)
3.402 - in (str, c@c', ptp) end
3.403 - else let val (str, (_, c', ptp as (_, p))) = step ip cs;
3.404 - in if str = "ok"
3.405 - then autocalc (c@c') p (ptp,[]) (Step (s-1))
3.406 - else (str, c@c', ptp) end
3.407 -(* handles autoord <= 3, autoord > 3 handled by all_/complete_solve *)
3.408 - | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto =
3.409 - if autoord auto > 3 andalso just_created (pt, pos)
3.410 - then let val ptp = all_modspec (pt, pos);
3.411 - in all_solve auto c ptp end
3.412 - else
3.413 - if member op = [Pbl, Met] p_
3.414 - then if not (is_complete_mod (pt, pos))
3.415 - then let val ptp = complete_mod (pt, pos)
3.416 - in if autoord auto < 3 then ("ok", c, ptp)
3.417 - else
3.418 - if not (is_complete_spec ptp)
3.419 - then let val ptp = complete_spec ptp
3.420 - in if autoord auto = 3 then ("ok", c, ptp)
3.421 - else all_solve auto c ptp
3.422 - end
3.423 - else if autoord auto = 3 then ("ok", c, ptp)
3.424 - else all_solve auto c ptp
3.425 - end
3.426 - else
3.427 - if not (is_complete_spec (pt,pos))
3.428 - then let val ptp = complete_spec (pt, pos)
3.429 - in if autoord auto = 3 then ("ok", c, ptp)
3.430 - else all_solve auto c ptp
3.431 - end
3.432 - else if autoord auto = 3 then ("ok", c, (pt, pos))
3.433 - else all_solve auto c (pt, pos)
3.434 - else complete_solve auto c (pt, pos);
3.435 -(* val pbl = get_obj g_pbl (fst ptp) [];
3.436 - val (oris,_,_) = get_obj g_origin (fst ptp) [];
3.437 -*)
3.438 -
3.439 -
3.440 -
3.441 -
3.442 + then
3.443 + let val (str, (_, c', ptp)) = step ip cs; (* autoord = 1, probably does 1 step too much*)
3.444 + in (str, c@c', ptp) end
3.445 + else
3.446 + let val (str, (_, c', ptp as (_, p))) = step ip cs;
3.447 + in
3.448 + if str = "ok"
3.449 + then autocalc (c@c') p (ptp, []) (Step (s - 1))
3.450 + else (str, c@c', ptp) end
3.451 + (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
3.452 + | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
3.453 + if autoord auto > 3 andalso just_created (pt, pos)
3.454 + then
3.455 + let val ptp = all_modspec (pt, pos);
3.456 + in all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
3.457 + else
3.458 + if member op = [Pbl, Met] p_
3.459 + then
3.460 + if not (is_complete_mod (pt, pos))
3.461 + then
3.462 + let val ptp = complete_mod (pt, pos) (*... auto = 2 | 3 *)
3.463 + in
3.464 + if autoord auto < 3 then ("ok", c, ptp)
3.465 + else
3.466 + if not (is_complete_spec ptp)
3.467 + then
3.468 + let val ptp = complete_spec ptp
3.469 + in
3.470 + if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
3.471 + end
3.472 + else if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
3.473 + end
3.474 + else
3.475 + if not (is_complete_spec (pt,pos))
3.476 + then
3.477 + let val ptp = complete_spec (pt, pos)
3.478 + in
3.479 + if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
3.480 + end
3.481 + else
3.482 + if autoord auto = 3 then ("ok", c, (pt, pos)) else all_solve auto c (pt, pos)
3.483 + else complete_solve auto c (pt, pos);
3.484
3.485 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
3.486 if no pbl has been specified, take the init from origin.*)
3.487 -(*fun initmatch pt (pos as (p,_):pos') =
3.488 - let val PblObj {probl,origin=(os,(_,pI,_),_),spec=(dI',pI',mI'),...} =
3.489 - get_obj I pt p
3.490 - val pblID = if pI' = e_pblID
3.491 - then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
3.492 - takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
3.493 - else pI'
3.494 - val spec = (dI',pblID,mI')
3.495 - val {ppc,where_,prls,...} = get_pbt pblID
3.496 - val (model_ok, (pbl, pre)) =
3.497 - match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
3.498 - in ModSpec (ocalhd_complete pbl pre spec,
3.499 - Pbl, e_term, pbl, pre, spec) end;*)
3.500 -fun initcontext_pbl pt (pos as (p,_):pos') =
3.501 - let val PblObj {probl,origin=(os,(_,pI,_),hdl),spec=(dI',pI',mI'),...} =
3.502 - get_obj I pt p
3.503 - val pblID = if pI' = e_pblID
3.504 - then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
3.505 - takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
3.506 - else pI'
3.507 - val {ppc,where_,prls,...} = get_pbt pblID
3.508 - val (model_ok, (pbl, pre)) =
3.509 - match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
3.510 - in (model_ok, pblID, hdl, pbl, pre) end;
3.511 +fun initcontext_pbl pt (p, _) =
3.512 + let
3.513 + val (probl, os, pI, hdl, pI') =
3.514 + case get_obj I pt p of
3.515 + PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
3.516 + => (probl, os, pI, hdl, pI')
3.517 + | PrfObj _ => error "initcontext_pbl: uncovered case"
3.518 + val pblID =
3.519 + if pI' = e_pblID
3.520 + then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
3.521 + else pI'
3.522 + val {ppc, where_, prls, ...} = get_pbt pblID
3.523 + val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
3.524 + in
3.525 + (model_ok, pblID, hdl, pbl, pre)
3.526 + end
3.527
3.528 -fun initcontext_met pt (pos as (p,_):pos') =
3.529 - let val PblObj {meth,origin=(os,(_,_,mI), _),spec=(_, _, mI'),...} =
3.530 - get_obj I pt p
3.531 - val metID = if mI' = e_metID
3.532 - then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
3.533 - takelast (2, mI) (*FIXME.WN051125 a hack, impl.^^^*)
3.534 - else mI'
3.535 - val {ppc,pre,prls,scr,...} = get_met metID
3.536 - val (model_ok, (pbl, pre)) =
3.537 - match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
3.538 - in (model_ok, metID, scr, pbl, pre) end;
3.539 +fun initcontext_met pt (p,_) =
3.540 + let
3.541 + val (meth, os, mI, mI') =
3.542 + case get_obj I pt p of
3.543 + PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
3.544 + | PrfObj _ => error "initcontext_met: uncovered case"
3.545 + val metID = if mI' = e_metID
3.546 + then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
3.547 + else mI'
3.548 + val {ppc, pre, prls, scr, ...} = get_met metID
3.549 + val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
3.550 + in
3.551 + (model_ok, metID, scr, pbl, pre)
3.552 + end
3.553
3.554 -(*.match the model of a problem at pos p
3.555 - with the model-pattern of the problem with pblID*)
3.556 +(* match the model of a problem at pos p with the model-pattern of the problem with pblID *)
3.557 fun context_pbl pI pt (p:pos) =
3.558 - let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
3.559 - val {ppc,where_,prls,...} = get_pbt pI
3.560 - val (model_ok, (pbl, pre)) =
3.561 - match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
3.562 - in (model_ok, pI, hdl, pbl, pre) end;
3.563 + let
3.564 + val (probl, os, hdl) =
3.565 + case get_obj I pt p of
3.566 + PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
3.567 + | PrfObj _ => error "context_pbl: uncovered case"
3.568 + val {ppc,where_,prls,...} = get_pbt pI
3.569 + val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
3.570 + in
3.571 + (model_ok, pI, hdl, pbl, pre)
3.572 + end
3.573
3.574 fun context_met mI pt (p:pos) =
3.575 - let val PblObj {meth,origin=(os,_,hdl),...} = get_obj I pt p
3.576 - val {ppc,pre,prls,scr,...} = get_met mI
3.577 - val (model_ok, (pbl, pre)) =
3.578 - match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
3.579 - in (model_ok, mI, scr, pbl, pre) end
3.580 + let
3.581 + val (meth, os) =
3.582 + case get_obj I pt p of
3.583 + PblObj {meth, origin = (os, _, _),...} => (meth, os)
3.584 + | PrfObj _ => error "context_met: uncovered case"
3.585 + val {ppc,pre,prls,scr,...} = get_met mI
3.586 + val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
3.587 + in
3.588 + (model_ok, mI, scr, pbl, pre)
3.589 + end
3.590
3.591 +fun tryrefine pI pt (p,_) =
3.592 + let
3.593 + val (probl, os, hdl) =
3.594 + case get_obj I pt p of
3.595 + PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
3.596 + | PrfObj _ => error "context_met: uncovered case"
3.597 + in
3.598 + case refine_pbl (assoc_thy "Isac") pI probl of
3.599 + NONE => (*copy from context_pbl*)
3.600 + let
3.601 + val {ppc,where_,prls,...} = get_pbt pI
3.602 + val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
3.603 + in
3.604 + (false, pI, hdl, pbl, pre)
3.605 + end
3.606 + | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)
3.607 + end
3.608
3.609 -(* val (pI, pt, pos as (p,_)) = (pblID, pt, p);
3.610 - *)
3.611 -fun tryrefine pI pt (pos as (p,_):pos') =
3.612 - let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
3.613 - in case refine_pbl (assoc_thy "Isac") pI probl of
3.614 - NONE => (*copy from context_pbl*)
3.615 - let val {ppc,where_,prls,...} = get_pbt pI
3.616 - val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac")
3.617 - probl (ppc,where_,prls) os
3.618 - in (false, pI, hdl, pbl, pre) end
3.619 - | SOME (pI, (pbl, pre)) =>
3.620 - (true, pI, hdl, pbl, pre)
3.621 - end;
3.622 -
3.623 -fun detailstep pt (pos as (p,p_):pos') =
3.624 +fun detailstep pt (pos as (p, _):pos') =
3.625 let
3.626 val nd = get_nd pt p
3.627 val cn = children nd
3.628 in
3.629 if null cn
3.630 - then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
3.631 + then
3.632 + if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
3.633 then detailrls pt pos
3.634 else ("no-Rewrite_Set...", EmptyPtree, e_pos')
3.635 - else ("donesteps", pt,
3.636 - (p @ [length (children (get_nd pt p))], Res) )
3.637 + else ("donesteps", pt, (p @ [length (children (get_nd pt p))], Res))
3.638 end;
3.639
3.640
3.641 -(***. for mathematics authoring on sml-toplevel; no XML .***)
3.642 +(*** for mathematics authoring on sml-toplevel; no XML ***)
3.643
3.644 type NEW = int list;
3.645 -(* val sp = (dI',pI',mI');
3.646 - *)
3.647
3.648 -(*15.8.03 for me with loc_specify/solve, nxt_specify/solve
3.649 - delete as soon as TESTg_form -> _mout_ dropped*)
3.650 +(* 15.8.03 for me with loc_specify/solve, nxt_specify/solve
3.651 + delete as soon as TESTg_form -> _mout_ dropped *)
3.652 fun TESTg_form ptp =
3.653 -(* val ptp = (pt,p);
3.654 - *)
3.655 - let val (form,_,_) = pt_extract ptp
3.656 - in case form of
3.657 - Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
3.658 - | ModSpec (_,p_, head, gfr, pre, _) =>
3.659 - Form' (PpcKF (0,EdUndef,0,Nundef,
3.660 - (case p_ of Pbl => Problem[] | Met => Method[],
3.661 - itms2itemppc (assoc_thy"Isac") gfr pre)))
3.662 - end;
3.663 + let
3.664 + val (form, _, _) = pt_extract ptp
3.665 + in
3.666 + case form of
3.667 + Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
3.668 + | ModSpec (_,p_, _, gfr, pre, _) =>
3.669 + Form' (PpcKF (0, EdUndef, 0, Nundef,
3.670 + (case p_ of Pbl => Problem [] | Met => Method [] | _ => error "TESTg_form: uncovered case",
3.671 + itms2itemppc (assoc_thy"Isac") gfr pre)))
3.672 + end;
3.673
3.674 -(*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;
3.675 - compare "fun CalcTree" which DOES decode.*)
3.676 -fun CalcTreeTEST [(fmz, sp):fmz] =
3.677 +(* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
3.678 + compare "fun CalcTree" which DOES decode *)
3.679 +fun CalcTreeTEST [(fmz, sp)] =
3.680 let
3.681 - val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
3.682 + val ((pt, p), tacis) = nxt_specify_init_calc (fmz, sp)
3.683 val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
3.684 val f = TESTg_form (pt,p)
3.685 - in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end;
3.686 + in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end
3.687 +| CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
3.688
3.689 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
3.690 external view: me should be used by math-authors as done so far
3.691 @@ -389,7 +393,7 @@
3.692 NEW loeschen, eigene Version von locatetac, step
3.693 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
3.694
3.695 -fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
3.696 +fun me (_, tac) p _(*NEW remove*) pt =
3.697 let
3.698 val (pt, p) =
3.699 (*locatetac is here for testing by me; step would suffice in me*)
3.700 @@ -398,28 +402,25 @@
3.701 | ("unsafe-ok", (_, _, ptp)) => ptp
3.702 | ("not-applicable",_) => (pt, p)
3.703 | ("end-of-calculation", (_, _, ptp)) => ptp
3.704 - | ("failure",_) => error "sys-error";
3.705 + | ("failure", _) => error "sys-error"
3.706 + | _ => error "me: uncovered case"
3.707 val (_, ts) =
3.708 (case step p ((pt, e_pos'),[]) of
3.709 - ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
3.710 - | ("helpless",_) => ("helpless: cannot propose tac", [])
3.711 - | ("no-fmz-spec",_) => error "no-fmz-spec"
3.712 - | ("end-of-calculation", (ts, _, _)) => ("",ts))
3.713 - handle ERROR msg => raise ERROR msg
3.714 + ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
3.715 + | ("helpless", _) => ("helpless: cannot propose tac", [])
3.716 + | ("no-fmz-spec", _) => error "no-fmz-spec"
3.717 + | ("end-of-calculation", (ts, _, _)) => ("", ts)
3.718 + | _ => error "me: uncovered case")
3.719 + handle ERROR msg => raise ERROR msg
3.720 val tac =
3.721 case ts of
3.722 - tacis as (_::_) => let val (tac,_,_) = last_elem tacis in tac end
3.723 - | _ => if p = ([],Res) then End_Proof' else Empty_Tac;
3.724 - in (p:pos', []:NEW, TESTg_form (pt, p) (*form output comes from locatetac*),
3.725 - (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
3.726 + tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
3.727 + | _ => if p = ([], Res) then End_Proof' else Empty_Tac;
3.728 + in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
3.729 + (tac2IDstr tac, tac):tac'_, Sundef, pt)
3.730 + end
3.731
3.732 -(*for quick test-print-out, until 'type inout' is removed*)
3.733 +(* for quick test-print-out, until 'type inout' is removed *)
3.734 fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
3.735
3.736 -
3.737 -
3.738 -(*------------------------------------------------------------------(**)
3.739 end
3.740 -open MathEngine;
3.741 -(**)------------------------------------------------------------------*)
3.742 -
4.1 --- a/src/Tools/isac/Interpret/script.sml Mon Nov 21 12:47:02 2016 +0100
4.2 +++ b/src/Tools/isac/Interpret/script.sml Tue Nov 22 10:42:21 2016 +0100
4.3 @@ -27,7 +27,7 @@
4.4 val rule2thm'' : rule -> thm''
4.5 val rule2rls' : rule -> string
4.6
4.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*
4.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.9 datatype asap = Aundef | AssOnly | AssGen
4.10 datatype appy = Appy of tac_ * scrstate | Napp of env | Skip of term * env
4.11 datatype appy_ = Napp_ | Skip_
5.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Mon Nov 21 12:47:02 2016 +0100
5.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Tue Nov 22 10:42:21 2016 +0100
5.3 @@ -1,3 +1,4 @@
5.4 +(* this is evaluated BEFORE Test_Isac.thu opens structures*)
5.5
5.6 theory All_Ctxt imports
5.7 "~~/src/Tools/isac/Knowledge/Isac"
5.8 @@ -15,7 +16,7 @@
5.9 val (dI',pI',mI') =
5.10 ("Test", ["sqroot-test","univariate","equation","test"],
5.11 ["Test","squ-equ-test-subpbl1"]);
5.12 - val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.13 + val (p,_,f,nxt,_,pt) = Math_Engine.CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.14 *}
5.15
5.16 section {* start of specify phase *}
5.17 @@ -32,14 +33,14 @@
5.18 *}
5.19
5.20 ML {*
5.21 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.22 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.23 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.24 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.25 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.26 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.27 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.28 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.29 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.30 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.31 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.32 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.33 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.34 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.35 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.36 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.37 *}
5.38
5.39 section {* start interpretation of method *}
5.40 @@ -51,9 +52,9 @@
5.41 *}
5.42
5.43 ML {*
5.44 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.45 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.46 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.47 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.48 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.49 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.50 *}
5.51
5.52 section {* start a subproblem: specification *}
5.53 @@ -71,14 +72,14 @@
5.54 *}
5.55
5.56 ML {*
5.57 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.58 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.59 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.60 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.61 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.62 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.63 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.64 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.65 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.66 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.67 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.68 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.69 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.70 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.71 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.72 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.73 *}
5.74
5.75 section {* interpretation of subproblem's method *}
5.76 @@ -91,7 +92,7 @@
5.77 *}
5.78
5.79 ML {*
5.80 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.81 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.82 *}
5.83
5.84 ML {*
5.85 @@ -103,8 +104,8 @@
5.86 *}
5.87
5.88 ML {*
5.89 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.90 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.91 +val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.92 +val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.93 *}
5.94
5.95 section {* finish subproblem, return to calling method*}
5.96 @@ -120,8 +121,8 @@
5.97 *}
5.98
5.99 ML {*
5.100 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.101 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.102 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.103 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p [] pt;
5.104 *}
5.105
5.106 section {* finish Lucas interpretation *}
6.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Mon Nov 21 12:47:02 2016 +0100
6.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Tue Nov 22 10:42:21 2016 +0100
6.3 @@ -1,7 +1,4 @@
6.4 -(*
6.5 -cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/course/
6.6 -/usr/local/Isabelle/bin/isabelle jedit -l Isac T2_Rewriting.thy &
6.7 -*)
6.8 +(* this is evaluated BEFORE Test_Isac.thu opens structures*)
6.9
6.10 theory T3_MathEngine imports Isac begin
6.11
6.12 @@ -63,7 +60,7 @@
6.13 So we can start testing the example by calling 'CalcTreeTEST':
6.14 *}
6.15 ML {* val (p,_,f,nxt,_,pt) =
6.16 - CalcTreeTEST
6.17 + Math_Engine.CalcTreeTEST
6.18 [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
6.19 "normalform N"],
6.20 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
6.21 @@ -90,18 +87,18 @@
6.22 Only note the tactic 'nxt' suggested for the next step:
6.23 *}
6.24 ML {* val c = [(*this is an unimportant, but necessary detail*)];
6.25 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.26 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.27 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
6.28 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
6.29 *}
6.30 text{* The tactics 'Add_Given' and 'Add_Find' inserted the respective values
6.31 into the model. Then 'Specify_Theory' determines the knowledge item no.1 from
6.32 above, 'Specify_Problem' item 2 and 'Specify_Method' item 3.
6.33 *}
6.34 ML {*
6.35 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.36 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.37 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.38 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.39 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
6.40 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
6.41 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
6.42 + val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
6.43 *}
6.44 text{* The final suggestion 'Apply_Method' completes the specification phase
6.45 and starts the 'solving phase', which is guided by the method determined.
6.46 @@ -116,10 +113,10 @@
6.47 term at the end:
6.48 *}
6.49 ML {* default_print_depth 40; *}
6.50 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
6.51 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
6.52 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
6.53 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
6.54 +ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
6.55 +ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
6.56 +ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
6.57 +ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
6.58 ML {* default_print_depth 3; *}
6.59 text{* And, please, note that the result of applying the 'nxt' ruleset is to be
6.60 found in the output of the next step !
6.61 @@ -130,7 +127,7 @@
6.62 perfect mathematics engine has to prove the socalled 'postcondition' of the
6.63 current problem; this is not yet implemented in the current version of ISAC.
6.64 *}
6.65 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
6.66 +ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
6.67 text{* Now the mathematics engine has found the end of the calculation.
6.68
6.69 With 'show_pt' the calculation can be inspected (in a more or less readable
6.70 @@ -144,12 +141,12 @@
6.71 the formalisation:
6.72 *}
6.73 ML {* val (p,_,f,nxt,_,pt) =
6.74 - CalcTreeTEST
6.75 + Math_Engine.CalcTreeTEST
6.76 [(["Term (1 + 2 + 3)", "normalform N"],
6.77 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
6.78 ["simplification","for_polynomials","with_minus"]))];
6.79 *}
6.80 -ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; *}
6.81 +ML {* val (p,_,f,nxt,_,pt) =Math_Engine.me nxt p c pt; *}
6.82 text{* and repeat this ML line as often as required ...*}
6.83
6.84 end
7.1 --- a/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml Mon Nov 21 12:47:02 2016 +0100
7.2 +++ b/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml Tue Nov 22 10:42:21 2016 +0100
7.3 @@ -62,7 +62,7 @@
7.4 tree as XML.Elem (("FORMALIZATION", []), _) => xml_to_fmz tree
7.5 | tree => error ("calctree: intree =" ^ xmlstr 0 tree)
7.6
7.7 - val result = Math_Engine.CalcTree fmz (* <--------------------------------- *)
7.8 + val result = CalcTree fmz (* <--------------------------------- *)
7.9 ;
7.10 val calcid = case result of
7.11 XML.Elem (("CALCTREE", []), [
7.12 @@ -79,7 +79,7 @@
7.13 ;
7.14 "----------- step 2: operation_setup iterator --------------------------------------------------";
7.15 "~~~~~ operation_setup iterator, args:"; val calcid = calcid
7.16 -val out = Math_Engine.Iterator calcid (* <--------------------------------- *)
7.17 +val out = Iterator calcid (* <--------------------------------- *)
7.18 val XML.Elem (("ADDUSER", []),
7.19 [XML.Elem (("CALCID", []), [XML.Text calcid]),
7.20 XML.Elem (("USERID", []), [XML.Text userid])]) = out;
7.21 @@ -101,7 +101,7 @@
7.22 ;
7.23 "----------- step 3: operation_setup moveactiveroot --------------------------------------------";
7.24 "~~~~~ operation_setup moveactiveroot, args:"; val calcid = calcid
7.25 -val out = Math_Engine.moveActiveRoot (str2int calcid) (* <--------------------------------- *)
7.26 +val out = moveActiveRoot (str2int calcid) (* <--------------------------------- *)
7.27 val XML.Elem (("CALCITERATOR", []), [
7.28 XML.Elem (("CALCID", []), [XML.Text calcid]),
7.29 XML.Elem (("POSITION", []), [
7.30 @@ -154,7 +154,7 @@
7.31 val to = xml_to_pos to
7.32 val SOME level = (*xml_to_int*) int_of_str level
7.33 val rules = (*xml_to_bool*) string_to_bool rules
7.34 - val out = Math_Engine.getFormulaeFromTo calcid from to level rules (* <-------------------- *)
7.35 + val out = getFormulaeFromTo calcid from to level rules (* <-------------------- *)
7.36 ;
7.37 if xmlstr 0 out = "(GETELEMENTSFROMTO)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (FORMHEADS)\n. . (CALCFORMULA)\n. . . (POSITION)\n. . . . (INTLIST)\n. . . . (/INTLIST)\n. . . . (POS)\n. . . . . Pbl\n. . . . (/POS)\n. . . (/POSITION)\n. . . (FORMULA)\n. . . . (ISA)\n. . . . . solve (x + 1 = 2, x)\n. . . . (/ISA)\n. . . . (TERM)\n. . . . . solve (x + 1 = 2, x)\n. . . . (/TERM)\n. . . (/FORMULA)\n. . (/CALCFORMULA)\n. (/FORMHEADS)\n(/GETELEMENTSFROMTO)\n"
7.38 then () else error "test--isac-java--isac-kernel step 4: operation_setup getformulaefromto CHANGED";
7.39 @@ -216,7 +216,7 @@
7.40 val pos = xml_to_pos p
7.41 ;
7.42 if calcid = 1 andalso pos = ([], Pbl) then () else error "--- step 6: intree changed";
7.43 - val result = Math_Engine.refFormula calcid pos
7.44 + val result = refFormula calcid pos
7.45 ;
7.46 (*this vanished by now..*)
7.47 xmlstr 0 result = "<REFFORMULA>\n. <CALCID>\n. . 1\n. </CALCID>\n. <ERROR>\n. . pos does not exist \n. </ERROR>\n</REFFORMULA>\n"
8.1 --- a/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml Mon Nov 21 12:47:02 2016 +0100
8.2 +++ b/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml Tue Nov 22 10:42:21 2016 +0100
8.3 @@ -99,7 +99,7 @@
8.4 pos as XML.Elem (("POSITION", []), _)])
8.5 => (str2int ci, xml_to_ketype ketype, xml_to_pos pos)
8.6 | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)
8.7 - val result = Math_Engine.initContext ci ketype pos
8.8 + val result = initContext ci ketype pos
8.9 in result end)
8.10 handle ERROR msg => sysERROR2xml 4711 msg)
8.11 handle _ => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")
9.1 --- a/test/Tools/isac/Test_Isac.thy Mon Nov 21 12:47:02 2016 +0100
9.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Nov 22 10:42:21 2016 +0100
9.3 @@ -20,9 +20,11 @@
9.4
9.5 In order to maintain these tests without changes, this has to be done before running tests:
9.6 (1) Query replace in src/Tools/isac:
9.7 - "--- ! aktivate for Test_Isac BEGIN ---\* )" \<longrightarrow> "--- ! aktivate for Test_Isac BEGIN ---\*)"
9.8 - "( *\--- ! aktivate for Test_Isac END ---" \<longrightarrow> "(*\--- ! aktivate for Test_Isac END ---"
9.9 - This extends the signatures with some functions required for some tests.
9.10 + \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit>
9.11 + \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit> \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit>
9.12 + ^^^ in signature outcommented, ^^^ NOT outcommented,
9.13 + this is status for coding this is status for tests
9.14 + "NOT outcommented" extends the signatures with some functions required for some tests.
9.15
9.16 Running Test_Isac.thy opens all structures, see code after "begin" below.
9.17
9.18 @@ -66,8 +68,9 @@
9.19
9.20 ML {*
9.21 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
9.22 + open Kernel;
9.23 + open Math_Engine
9.24 open Lucin;
9.25 - open Kernel;
9.26 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.27 *}
9.28 ML {*