1.1 --- a/src/Tools/isac/Interpret/mathengine.sml Mon Nov 21 12:47:02 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Tue Nov 22 10:42:21 2016 +0100
1.3 @@ -6,185 +6,185 @@
1.4 use"mathengine.sml";
1.5 *)
1.6
1.7 -signature MATHENGINE =
1.8 - sig
1.9 - type nxt_
1.10 - (* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *)
1.11 - type NEW
1.12 - type lOc_
1.13 - (*datatype
1.14 - lOc_ =
1.15 - ERror of string
1.16 - | UNsafe of CalcHead.calcstate'
1.17 - | Updated of CalcHead.calcstate' *)
1.18 +signature MATH_ENGINE =
1.19 +sig
1.20 + type NEW (* TODO: refactor "fun me" with calcstate and remove *)
1.21 + val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * mout * tac'_ * safe * ptree
1.22 + val autocalc :
1.23 + pos' list -> pos' -> (ptree * pos') * taci list -> auto -> string * pos' list * (ptree * pos')
1.24 + val locatetac :
1.25 + tac -> ptree * (posel list * pos_) -> string * (taci list * pos' list * (ptree * pos'))
1.26 + val step : pos' -> calcstate -> string * calcstate'
1.27 + val detailstep :
1.28 + ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
1.29
1.30 - val CalcTreeTEST :
1.31 - fmz list ->
1.32 - pos' * NEW * mout * (string * tac) * safe * ptree
1.33 + val initcontext_met : ptree -> pos' -> bool * string list * scr * itm list * (bool * term) list
1.34 + val initcontext_pbl : ptree -> pos' -> bool * string list * term * itm list * (bool * term) list
1.35 + val context_met : metID -> ptree -> pos -> bool * metID * scr * itm list * (bool * term) list
1.36 + val context_pbl : pblID -> ptree -> pos -> bool * pblID * term * itm list * (bool * term) list
1.37 + val set_method : metID -> ptree * pos' -> ptree * ocalhd
1.38 + val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
1.39 + val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
1.40 + val tryrefine : pblID -> ptree -> pos' -> bool * pblID * term * itm list * (bool * term) list
1.41
1.42 - val TESTg_form : ptree * (int list * pos_) -> mout
1.43 - val autocalc :
1.44 - pos' list ->
1.45 - pos' ->
1.46 - (ptree * pos') * taci list ->
1.47 - auto -> string * pos' list * (ptree * pos')
1.48 - val detailstep : ptree -> pos' -> string * ptree * pos'
1.49 - (* val e_tac_ : tac_ *)
1.50 - val f2str : mout -> cterm'
1.51 - (* val get_pblID : ptree * pos' -> pblID option *)
1.52 - val initmatch : ptree -> pos' -> ptform
1.53 - (* val loc_solve_ :
1.54 - string * tac_ -> ptree * (int list * pos_) -> lOc_ *)
1.55 - (* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *)
1.56 - val locatetac : (*tests only*)
1.57 - tac ->
1.58 - ptree * (posel list * pos_) ->
1.59 - string * (taci list * pos' list * (ptree * (posel list * pos_)))
1.60 - val me :
1.61 - tac'_ ->
1.62 - pos' ->
1.63 - NEW ->
1.64 - ptree -> pos' * NEW * mout * tac'_ * safe * ptree
1.65 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.66 + type nxt_
1.67 + type lOc_
1.68 + val CalcTreeTEST : fmz list -> pos' * NEW * mout * (string * tac) * safe * ptree
1.69 + val f2str : mout -> cterm'
1.70 + val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_
1.71 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.72 +end
1.73
1.74 - val nxt_specify_ : ptree * (int list * pos_) -> calcstate'(*tests only*)
1.75 - val set_method : metID -> ptree * pos' -> ptree * ocalhd
1.76 - val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
1.77 - val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
1.78 - val step : pos' -> calcstate -> string * calcstate'
1.79 - val trymatch : pblID -> ptree -> pos' -> ptform
1.80 - val tryrefine : pblID -> ptree -> pos' -> ptform
1.81 - end
1.82 +(**)
1.83 +structure Math_Engine(**): MATH_ENGINE(**) =
1.84 +struct
1.85 +(**)
1.86
1.87 +fun get_pblID (pt, (p, _):pos') =
1.88 + let val p' = par_pblobj pt p
1.89 + val (_, pI, _) = get_obj g_spec pt p'
1.90 + val (_, (_, oI, _), _) = get_obj g_origin pt p'
1.91 + in
1.92 + if pI <> e_pblID
1.93 + then SOME pI
1.94 + else
1.95 + if oI <> e_pblID then SOME oI else NONE end;
1.96
1.97 -
1.98 -(*------------------------------------------------------------------(**)
1.99 -structure MathEngine : MATHENGINE =
1.100 -struct
1.101 -(**)------------------------------------------------------------------*)
1.102 -
1.103 -fun get_pblID (pt, (p,_):pos') =
1.104 - let val p' = par_pblobj pt p
1.105 - val (_,pI,_) = get_obj g_spec pt p'
1.106 - val (_,(_,oI,_),_) = get_obj g_origin pt p'
1.107 - in if pI <> e_pblID then SOME pI
1.108 - else if oI <> e_pblID then SOME oI
1.109 - else NONE end;
1.110 -(*fun get_pblID (pt, (p,_):pos') =
1.111 - ((snd3 o (get_obj g_spec pt)) (par_pblobj pt p));*)
1.112 -
1.113 -
1.114 -(*--vvv--dummies for test*)
1.115 -val e_tac_ = Tac_ (Pure.thy,"","","");
1.116 +(* introduced for test only *)
1.117 +val e_tac_ = Tac_ (Pure.thy, "", "", "");
1.118 datatype lOc_ =
1.119 ERror of string (*after loc_specify, loc_solve*)
1.120 | UNsafe of calcstate' (*after loc_specify, loc_solve*)
1.121 -| Updated of calcstate'; (*after loc_specify, loc_solve*)
1.122 +| Updated of calcstate'; (*after loc_specify, loc_solve*)
1.123 +
1.124 fun loc_specify_ m (pt,pos) =
1.125 -(* val pos = ip;
1.126 - *)
1.127 - let val (p,_,f,_,s,pt) = specify m pos [] pt;
1.128 -(* val (_,_,_,_,_,pt')= specify m pos [] pt;
1.129 - *)
1.130 - in case f of
1.131 - (Error' (Error_ e)) => ERror e
1.132 - | _ => Updated ([], [], (pt,p)) end;
1.133 + let
1.134 + val (p, _, f, _, _, pt) = specify m pos [] pt;
1.135 + in
1.136 + case f of (Error' (Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
1.137 + end
1.138
1.139 -(*. TODO push return-value cs' into solve and rename solve->loc_solve?_? .*)
1.140 -(* val (m, pos) = ((mI,m), ip);
1.141 - val (m,(pt,pos) ) = ((mI,m), ptp);
1.142 - *)
1.143 -fun loc_solve_ m (pt,pos) =
1.144 - let val (msg, cs') = solve m (pt, pos);
1.145 -(* val (tacis,dels,(pt',p')) = cs';
1.146 - (tracing o istate2str) (get_istate pt' p');
1.147 - (term2str o fst) (get_obj g_result pt' (fst p'));
1.148 - *)
1.149 - in case msg of
1.150 - "ok" => Updated cs'
1.151 - | msg => ERror msg
1.152 - end;
1.153 +(* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
1.154 +fun loc_solve_ m (pt, pos) =
1.155 + let
1.156 + val (msg, cs') = solve m (pt, pos);
1.157 + in
1.158 + case msg of "ok" => Updated cs' | msg => ERror msg
1.159 + end
1.160
1.161 datatype nxt_ =
1.162 - HElpless (**)
1.163 - | Nexts of calcstate; (**)
1.164 + HElpless (**)
1.165 +| Nexts of calcstate; (**)
1.166
1.167 -(*. locate a tactic in a script and apply it if possible .*)
1.168 -(*report applicability of tac in tacis; pt is dropped in setNextTactic*)
1.169 -fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
1.170 +(* locate a tactic in a script and apply it if possible;
1.171 + report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
1.172 +fun locatetac _ (ptp as (_, ([], Res))) = ("end-of-calculation", ([], [], ptp))
1.173 | locatetac tac (ptp as (pt, p)) =
1.174 - let val (mI,m) = mk_tac'_ tac;
1.175 - in case applicable_in p pt m of
1.176 - Notappl e => ("not-applicable", ([],[], ptp):calcstate')
1.177 - | Appl m =>
1.178 - let
1.179 - val x = if member op = specsteps mI
1.180 - then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
1.181 - in case x of
1.182 - ERror e => ("failure", ([], [], ptp))
1.183 - (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
1.184 - | UNsafe cs' => ("unsafe-ok", cs')
1.185 - | Updated (cs' as (_,_,(_,p'))) => (*ev.SEVER.tacs like Begin_Trans*)
1.186 - (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
1.187 - (*for SEVER.tacs user to ask ? *)
1.188 - end
1.189 - end;
1.190 + let
1.191 + val (mI, m) = mk_tac'_ tac;
1.192 + in
1.193 + case applicable_in p pt m of
1.194 + Notappl _ => ("not-applicable", ([],[], ptp):calcstate')
1.195 + | Appl m =>
1.196 + let
1.197 + val x = if member op = specsteps mI
1.198 + then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
1.199 + in
1.200 + case x of
1.201 + ERror _ => ("failure", ([], [], ptp))
1.202 + (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
1.203 + | UNsafe cs' => ("unsafe-ok", cs')
1.204 + | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
1.205 + (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
1.206 + (*for SEVER.tacs user to ask ? *)
1.207 + end
1.208 + end
1.209
1.210 -(*iterated by nxt_me; there (the resulting) ptp dropped
1.211 - may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
1.212 -fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
1.213 - let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
1.214 - probl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
1.215 +(* iterated by nxt_me; there (the resulting) ptp dropped
1.216 + may call nxt_solve Apply_Method --- thus evaluated here after solve.sml *)
1.217 +fun nxt_specify_ (ptp as (pt, (p, p_))) =
1.218 + let
1.219 + val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
1.220 + case get_obj I pt p of
1.221 + pblobj as (PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
1.222 + probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
1.223 + | PrfObj _ => error "nxt_specify_: not on PrfObj"
1.224 in
1.225 if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
1.226 then
1.227 case mI' of
1.228 - ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
1.229 + ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
1.230 | _ => nxt_specif Model_Problem (pt, (p,Pbl))
1.231 else
1.232 let
1.233 val cpI = if pI = e_pblID then pI' else pI;
1.234 - val cmI = if mI = e_metID then mI' else mI;
1.235 - val {ppc, prls, where_, ...} = get_pbt cpI;
1.236 - val pre = check_preconds "thy 100820" prls where_ probl;
1.237 - val pb = foldl and_ (true, map fst pre);
1.238 - (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
1.239 - val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
1.240 - (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
1.241 - in case tac of
1.242 - Apply_Method mI =>
1.243 - nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.244 - | _ => nxt_specif tac ptp end
1.245 - end;
1.246 + val cmI = if mI = e_metID then mI' else mI;
1.247 + val {ppc, prls, where_, ...} = get_pbt cpI;
1.248 + val pre = check_preconds "thy 100820" prls where_ probl;
1.249 + val pb = foldl and_ (true, map fst pre);
1.250 + (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
1.251 + val (_, tac) =
1.252 + nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
1.253 + in
1.254 + case tac of
1.255 + Apply_Method mI =>
1.256 + nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.257 + | _ => nxt_specif tac ptp
1.258 + end
1.259 + end
1.260
1.261 -(*.specify a new method;
1.262 - WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*)
1.263 +(* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
1.264 fun set_method (mI:metID) ptp =
1.265 - let val ([(_, Specify_Method' (_, _, mits), _)], [], (pt, pos as (p,_))) =
1.266 - nxt_specif (Specify_Method mI) ptp
1.267 - val pre = [] (*...from Specify_Method'*)
1.268 - val complete = true (*...from Specify_Method'*)
1.269 - (*from Specify_Method' ? vvv, vvv ?*)
1.270 - val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
1.271 - in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end;
1.272 + let
1.273 + val (mits, pt, p) =
1.274 + case nxt_specif (Specify_Method mI) ptp of
1.275 + ([(_, Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p)
1.276 + | _ => error "set_method: case 1 uncovered"
1.277 + val pre = [] (*...from Specify_Method'*)
1.278 + val complete = true (*...from Specify_Method'*)
1.279 + (*from Specify_Method' ? vvv, vvv ?*)
1.280 + val (hdf, spec) =
1.281 + case get_obj I pt p of
1.282 + PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
1.283 + | PrfObj _ => error "set_method: case 2 uncovered"
1.284 + in
1.285 + (pt, (complete, Met, hdf, mits, pre, spec) : ocalhd)
1.286 + end
1.287
1.288 -(*.specify a new problem;
1.289 - WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*)
1.290 +(* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
1.291 fun set_problem pI (ptp: ptree * pos') =
1.292 - let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
1.293 - _, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp
1.294 - (*from Specify_Problem' ? vvv, vvv ?*)
1.295 - val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
1.296 - in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
1.297 + let
1.298 + val (complete, pits, pre, pt, p) =
1.299 + case nxt_specif (Specify_Problem pI) ptp of
1.300 + ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
1.301 + => (complete, pits, pre, pt, p)
1.302 + | _ => error "set_problem: case 1 uncovered"
1.303 + (*from Specify_Problem' ? vvv, vvv ?*)
1.304 + val (hdf, spec) =
1.305 + case get_obj I pt p of
1.306 + PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
1.307 + | PrfObj _ => error "set_problem: case 2 uncovered"
1.308 + in
1.309 + (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd)
1.310 + end
1.311
1.312 fun set_theory (tI:thyID) (ptp: ptree * pos') =
1.313 - let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
1.314 - _, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp
1.315 - (*from Specify_Theory' ? vvv, vvv ?*)
1.316 - val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
1.317 - in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
1.318 + let
1.319 + val (complete, pits, pre, pt, p) =
1.320 + case nxt_specif (Specify_Theory tI) ptp of
1.321 + ([(_, Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
1.322 + => (complete, pits, pre, pt, p)
1.323 + | _ => error "set_theory: case 1 uncovered"
1.324 + (*from Specify_Theory' ? vvv, vvv ?*)
1.325 + val (hdf, spec) =
1.326 + case get_obj I pt p of
1.327 + PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
1.328 + | PrfObj _ => error "set_theory: case 2 uncovered"
1.329 + in (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd) end;
1.330
1.331 (* does a step forward; returns tactic used, ctree updated.
1.332 -TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
1.333 + TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
1.334 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
1.335 let val pIopt = get_pblID (pt,ip);
1.336 in
1.337 @@ -192,194 +192,198 @@
1.338 then ("end-of-calculation", (tacis, [], ptp):calcstate')
1.339 else
1.340 case tacis of
1.341 - (_::_) =>
1.342 + (_::_) =>
1.343 if ip = p (*the request is done where ptp waits for*)
1.344 - then
1.345 + then
1.346 let val (pt',c',p') = generate tacis (pt,[],p)
1.347 - in ("ok", (tacis, c', (pt', p'))) end
1.348 - else (case (if member op = [Pbl,Met] p_
1.349 - then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.350 - handle ERROR msg => (writeln ("*** " ^ msg);
1.351 - ([],[],ptp))(*e.g. Add_Given "equality///"*) of
1.352 - cs as ([],_,_) => ("helpless", cs)
1.353 - | cs => ("ok", cs))
1.354 - | _ => (case pIopt of
1.355 - NONE => ("no-fmz-spec", ([], [], ptp))
1.356 - | SOME pI =>
1.357 - (case if member op = [Pbl,Met] p_
1.358 - andalso is_none (get_obj g_env pt (fst p))
1.359 - (*^^^^^^^^: Apply_Method without init_form*)
1.360 - then nxt_specify_ (pt, ip)
1.361 - else (nxt_solve_ (pt,ip) )
1.362 - handle ERROR msg => (writeln ("*** " ^ msg);
1.363 - ([],[],ptp))(*e.g. Add_Given "equality///"*) of
1.364 - cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
1.365 - | cs => ("ok", cs)))
1.366 - end;
1.367 + in ("ok", (tacis, c', (pt', p'))) end
1.368 + else (case (if member op = [Pbl, Met] p_
1.369 + then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip))
1.370 + handle ERROR msg => (writeln ("*** " ^ msg);
1.371 + ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
1.372 + cs as ([],_,_) => ("helpless", cs)
1.373 + | cs => ("ok", cs))
1.374 + | _ => (case pIopt of
1.375 + NONE => ("no-fmz-spec", ([], [], ptp))
1.376 + | SOME _ => (*vvvvvv: Apply_Method without init_form*)
1.377 + (case if member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
1.378 + then nxt_specify_ (pt, ip)
1.379 + else (nxt_solve_ (pt,ip))
1.380 + handle ERROR msg => (writeln ("*** " ^ msg);
1.381 + ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
1.382 + cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
1.383 + | cs => ("ok", cs)))
1.384 + end
1.385
1.386 -(*.does several steps within one calculation as given by "type auto";
1.387 +(* does several steps within one calculation as given by "type auto";
1.388 the steps may arbitrarily go into and leave different phases,
1.389 - i.e. specify-phase and solve-phase.*)
1.390 -(*TODO.WN0512 ? redesign after the phases have been more separated
1.391 - at the fron-end in 05:
1.392 - eg. CompleteCalcHead could be done by a separate fun !!!*)
1.393 -fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
1.394 + i.e. specify-phase and solve-phase
1.395 + TODO.WN0512 ? redesign after the phases have been more separated
1.396 + at the fron-end in 05:
1.397 + eg. CompleteCalcHead could be done by a separate fun !!!*)
1.398 +fun autocalc c ip cs (Step s) =
1.399 if s <= 1
1.400 - then let val (str, (_, c', ptp)) = step ip cs;(*1*)
1.401 - (*at least does 1 step, ev.1 too much*)
1.402 - in (str, c@c', ptp) end
1.403 - else let val (str, (_, c', ptp as (_, p))) = step ip cs;
1.404 - in if str = "ok"
1.405 - then autocalc (c@c') p (ptp,[]) (Step (s-1))
1.406 - else (str, c@c', ptp) end
1.407 -(* handles autoord <= 3, autoord > 3 handled by all_/complete_solve *)
1.408 - | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto =
1.409 - if autoord auto > 3 andalso just_created (pt, pos)
1.410 - then let val ptp = all_modspec (pt, pos);
1.411 - in all_solve auto c ptp end
1.412 - else
1.413 - if member op = [Pbl, Met] p_
1.414 - then if not (is_complete_mod (pt, pos))
1.415 - then let val ptp = complete_mod (pt, pos)
1.416 - in if autoord auto < 3 then ("ok", c, ptp)
1.417 - else
1.418 - if not (is_complete_spec ptp)
1.419 - then let val ptp = complete_spec ptp
1.420 - in if autoord auto = 3 then ("ok", c, ptp)
1.421 - else all_solve auto c ptp
1.422 - end
1.423 - else if autoord auto = 3 then ("ok", c, ptp)
1.424 - else all_solve auto c ptp
1.425 - end
1.426 - else
1.427 - if not (is_complete_spec (pt,pos))
1.428 - then let val ptp = complete_spec (pt, pos)
1.429 - in if autoord auto = 3 then ("ok", c, ptp)
1.430 - else all_solve auto c ptp
1.431 - end
1.432 - else if autoord auto = 3 then ("ok", c, (pt, pos))
1.433 - else all_solve auto c (pt, pos)
1.434 - else complete_solve auto c (pt, pos);
1.435 -(* val pbl = get_obj g_pbl (fst ptp) [];
1.436 - val (oris,_,_) = get_obj g_origin (fst ptp) [];
1.437 -*)
1.438 -
1.439 -
1.440 -
1.441 -
1.442 + then
1.443 + let val (str, (_, c', ptp)) = step ip cs; (* autoord = 1, probably does 1 step too much*)
1.444 + in (str, c@c', ptp) end
1.445 + else
1.446 + let val (str, (_, c', ptp as (_, p))) = step ip cs;
1.447 + in
1.448 + if str = "ok"
1.449 + then autocalc (c@c') p (ptp, []) (Step (s - 1))
1.450 + else (str, c@c', ptp) end
1.451 + (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
1.452 + | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
1.453 + if autoord auto > 3 andalso just_created (pt, pos)
1.454 + then
1.455 + let val ptp = all_modspec (pt, pos);
1.456 + in all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
1.457 + else
1.458 + if member op = [Pbl, Met] p_
1.459 + then
1.460 + if not (is_complete_mod (pt, pos))
1.461 + then
1.462 + let val ptp = complete_mod (pt, pos) (*... auto = 2 | 3 *)
1.463 + in
1.464 + if autoord auto < 3 then ("ok", c, ptp)
1.465 + else
1.466 + if not (is_complete_spec ptp)
1.467 + then
1.468 + let val ptp = complete_spec ptp
1.469 + in
1.470 + if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
1.471 + end
1.472 + else if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
1.473 + end
1.474 + else
1.475 + if not (is_complete_spec (pt,pos))
1.476 + then
1.477 + let val ptp = complete_spec (pt, pos)
1.478 + in
1.479 + if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
1.480 + end
1.481 + else
1.482 + if autoord auto = 3 then ("ok", c, (pt, pos)) else all_solve auto c (pt, pos)
1.483 + else complete_solve auto c (pt, pos);
1.484
1.485 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
1.486 if no pbl has been specified, take the init from origin.*)
1.487 -(*fun initmatch pt (pos as (p,_):pos') =
1.488 - let val PblObj {probl,origin=(os,(_,pI,_),_),spec=(dI',pI',mI'),...} =
1.489 - get_obj I pt p
1.490 - val pblID = if pI' = e_pblID
1.491 - then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
1.492 - takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
1.493 - else pI'
1.494 - val spec = (dI',pblID,mI')
1.495 - val {ppc,where_,prls,...} = get_pbt pblID
1.496 - val (model_ok, (pbl, pre)) =
1.497 - match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
1.498 - in ModSpec (ocalhd_complete pbl pre spec,
1.499 - Pbl, e_term, pbl, pre, spec) end;*)
1.500 -fun initcontext_pbl pt (pos as (p,_):pos') =
1.501 - let val PblObj {probl,origin=(os,(_,pI,_),hdl),spec=(dI',pI',mI'),...} =
1.502 - get_obj I pt p
1.503 - val pblID = if pI' = e_pblID
1.504 - then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
1.505 - takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
1.506 - else pI'
1.507 - val {ppc,where_,prls,...} = get_pbt pblID
1.508 - val (model_ok, (pbl, pre)) =
1.509 - match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
1.510 - in (model_ok, pblID, hdl, pbl, pre) end;
1.511 +fun initcontext_pbl pt (p, _) =
1.512 + let
1.513 + val (probl, os, pI, hdl, pI') =
1.514 + case get_obj I pt p of
1.515 + PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
1.516 + => (probl, os, pI, hdl, pI')
1.517 + | PrfObj _ => error "initcontext_pbl: uncovered case"
1.518 + val pblID =
1.519 + if pI' = e_pblID
1.520 + then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
1.521 + else pI'
1.522 + val {ppc, where_, prls, ...} = get_pbt pblID
1.523 + val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
1.524 + in
1.525 + (model_ok, pblID, hdl, pbl, pre)
1.526 + end
1.527
1.528 -fun initcontext_met pt (pos as (p,_):pos') =
1.529 - let val PblObj {meth,origin=(os,(_,_,mI), _),spec=(_, _, mI'),...} =
1.530 - get_obj I pt p
1.531 - val metID = if mI' = e_metID
1.532 - then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
1.533 - takelast (2, mI) (*FIXME.WN051125 a hack, impl.^^^*)
1.534 - else mI'
1.535 - val {ppc,pre,prls,scr,...} = get_met metID
1.536 - val (model_ok, (pbl, pre)) =
1.537 - match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
1.538 - in (model_ok, metID, scr, pbl, pre) end;
1.539 +fun initcontext_met pt (p,_) =
1.540 + let
1.541 + val (meth, os, mI, mI') =
1.542 + case get_obj I pt p of
1.543 + PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
1.544 + | PrfObj _ => error "initcontext_met: uncovered case"
1.545 + val metID = if mI' = e_metID
1.546 + then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
1.547 + else mI'
1.548 + val {ppc, pre, prls, scr, ...} = get_met metID
1.549 + val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
1.550 + in
1.551 + (model_ok, metID, scr, pbl, pre)
1.552 + end
1.553
1.554 -(*.match the model of a problem at pos p
1.555 - with the model-pattern of the problem with pblID*)
1.556 +(* match the model of a problem at pos p with the model-pattern of the problem with pblID *)
1.557 fun context_pbl pI pt (p:pos) =
1.558 - let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
1.559 - val {ppc,where_,prls,...} = get_pbt pI
1.560 - val (model_ok, (pbl, pre)) =
1.561 - match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
1.562 - in (model_ok, pI, hdl, pbl, pre) end;
1.563 + let
1.564 + val (probl, os, hdl) =
1.565 + case get_obj I pt p of
1.566 + PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
1.567 + | PrfObj _ => error "context_pbl: uncovered case"
1.568 + val {ppc,where_,prls,...} = get_pbt pI
1.569 + val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
1.570 + in
1.571 + (model_ok, pI, hdl, pbl, pre)
1.572 + end
1.573
1.574 fun context_met mI pt (p:pos) =
1.575 - let val PblObj {meth,origin=(os,_,hdl),...} = get_obj I pt p
1.576 - val {ppc,pre,prls,scr,...} = get_met mI
1.577 - val (model_ok, (pbl, pre)) =
1.578 - match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
1.579 - in (model_ok, mI, scr, pbl, pre) end
1.580 + let
1.581 + val (meth, os) =
1.582 + case get_obj I pt p of
1.583 + PblObj {meth, origin = (os, _, _),...} => (meth, os)
1.584 + | PrfObj _ => error "context_met: uncovered case"
1.585 + val {ppc,pre,prls,scr,...} = get_met mI
1.586 + val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
1.587 + in
1.588 + (model_ok, mI, scr, pbl, pre)
1.589 + end
1.590
1.591 +fun tryrefine pI pt (p,_) =
1.592 + let
1.593 + val (probl, os, hdl) =
1.594 + case get_obj I pt p of
1.595 + PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
1.596 + | PrfObj _ => error "context_met: uncovered case"
1.597 + in
1.598 + case refine_pbl (assoc_thy "Isac") pI probl of
1.599 + NONE => (*copy from context_pbl*)
1.600 + let
1.601 + val {ppc,where_,prls,...} = get_pbt pI
1.602 + val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
1.603 + in
1.604 + (false, pI, hdl, pbl, pre)
1.605 + end
1.606 + | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)
1.607 + end
1.608
1.609 -(* val (pI, pt, pos as (p,_)) = (pblID, pt, p);
1.610 - *)
1.611 -fun tryrefine pI pt (pos as (p,_):pos') =
1.612 - let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
1.613 - in case refine_pbl (assoc_thy "Isac") pI probl of
1.614 - NONE => (*copy from context_pbl*)
1.615 - let val {ppc,where_,prls,...} = get_pbt pI
1.616 - val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac")
1.617 - probl (ppc,where_,prls) os
1.618 - in (false, pI, hdl, pbl, pre) end
1.619 - | SOME (pI, (pbl, pre)) =>
1.620 - (true, pI, hdl, pbl, pre)
1.621 - end;
1.622 -
1.623 -fun detailstep pt (pos as (p,p_):pos') =
1.624 +fun detailstep pt (pos as (p, _):pos') =
1.625 let
1.626 val nd = get_nd pt p
1.627 val cn = children nd
1.628 in
1.629 if null cn
1.630 - then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
1.631 + then
1.632 + if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
1.633 then detailrls pt pos
1.634 else ("no-Rewrite_Set...", EmptyPtree, e_pos')
1.635 - else ("donesteps", pt,
1.636 - (p @ [length (children (get_nd pt p))], Res) )
1.637 + else ("donesteps", pt, (p @ [length (children (get_nd pt p))], Res))
1.638 end;
1.639
1.640
1.641 -(***. for mathematics authoring on sml-toplevel; no XML .***)
1.642 +(*** for mathematics authoring on sml-toplevel; no XML ***)
1.643
1.644 type NEW = int list;
1.645 -(* val sp = (dI',pI',mI');
1.646 - *)
1.647
1.648 -(*15.8.03 for me with loc_specify/solve, nxt_specify/solve
1.649 - delete as soon as TESTg_form -> _mout_ dropped*)
1.650 +(* 15.8.03 for me with loc_specify/solve, nxt_specify/solve
1.651 + delete as soon as TESTg_form -> _mout_ dropped *)
1.652 fun TESTg_form ptp =
1.653 -(* val ptp = (pt,p);
1.654 - *)
1.655 - let val (form,_,_) = pt_extract ptp
1.656 - in case form of
1.657 - Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
1.658 - | ModSpec (_,p_, head, gfr, pre, _) =>
1.659 - Form' (PpcKF (0,EdUndef,0,Nundef,
1.660 - (case p_ of Pbl => Problem[] | Met => Method[],
1.661 - itms2itemppc (assoc_thy"Isac") gfr pre)))
1.662 - end;
1.663 + let
1.664 + val (form, _, _) = pt_extract ptp
1.665 + in
1.666 + case form of
1.667 + Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
1.668 + | ModSpec (_,p_, _, gfr, pre, _) =>
1.669 + Form' (PpcKF (0, EdUndef, 0, Nundef,
1.670 + (case p_ of Pbl => Problem [] | Met => Method [] | _ => error "TESTg_form: uncovered case",
1.671 + itms2itemppc (assoc_thy"Isac") gfr pre)))
1.672 + end;
1.673
1.674 -(*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;
1.675 - compare "fun CalcTree" which DOES decode.*)
1.676 -fun CalcTreeTEST [(fmz, sp):fmz] =
1.677 +(* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
1.678 + compare "fun CalcTree" which DOES decode *)
1.679 +fun CalcTreeTEST [(fmz, sp)] =
1.680 let
1.681 - val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
1.682 + val ((pt, p), tacis) = nxt_specify_init_calc (fmz, sp)
1.683 val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
1.684 val f = TESTg_form (pt,p)
1.685 - in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end;
1.686 + in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end
1.687 +| CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
1.688
1.689 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
1.690 external view: me should be used by math-authors as done so far
1.691 @@ -389,7 +393,7 @@
1.692 NEW loeschen, eigene Version von locatetac, step
1.693 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
1.694
1.695 -fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
1.696 +fun me (_, tac) p _(*NEW remove*) pt =
1.697 let
1.698 val (pt, p) =
1.699 (*locatetac is here for testing by me; step would suffice in me*)
1.700 @@ -398,28 +402,25 @@
1.701 | ("unsafe-ok", (_, _, ptp)) => ptp
1.702 | ("not-applicable",_) => (pt, p)
1.703 | ("end-of-calculation", (_, _, ptp)) => ptp
1.704 - | ("failure",_) => error "sys-error";
1.705 + | ("failure", _) => error "sys-error"
1.706 + | _ => error "me: uncovered case"
1.707 val (_, ts) =
1.708 (case step p ((pt, e_pos'),[]) of
1.709 - ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
1.710 - | ("helpless",_) => ("helpless: cannot propose tac", [])
1.711 - | ("no-fmz-spec",_) => error "no-fmz-spec"
1.712 - | ("end-of-calculation", (ts, _, _)) => ("",ts))
1.713 - handle ERROR msg => raise ERROR msg
1.714 + ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
1.715 + | ("helpless", _) => ("helpless: cannot propose tac", [])
1.716 + | ("no-fmz-spec", _) => error "no-fmz-spec"
1.717 + | ("end-of-calculation", (ts, _, _)) => ("", ts)
1.718 + | _ => error "me: uncovered case")
1.719 + handle ERROR msg => raise ERROR msg
1.720 val tac =
1.721 case ts of
1.722 - tacis as (_::_) => let val (tac,_,_) = last_elem tacis in tac end
1.723 - | _ => if p = ([],Res) then End_Proof' else Empty_Tac;
1.724 - in (p:pos', []:NEW, TESTg_form (pt, p) (*form output comes from locatetac*),
1.725 - (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
1.726 + tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
1.727 + | _ => if p = ([], Res) then End_Proof' else Empty_Tac;
1.728 + in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
1.729 + (tac2IDstr tac, tac):tac'_, Sundef, pt)
1.730 + end
1.731
1.732 -(*for quick test-print-out, until 'type inout' is removed*)
1.733 +(* for quick test-print-out, until 'type inout' is removed *)
1.734 fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
1.735
1.736 -
1.737 -
1.738 -(*------------------------------------------------------------------(**)
1.739 end
1.740 -open MathEngine;
1.741 -(**)------------------------------------------------------------------*)
1.742 -