1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,506 @@
1.4 +(* The _functional_ mathematics engine, ie. without a state.
1.5 + Input and output are Isabelle's formulae as strings.
1.6 + authors: Walther Neuper 2000
1.7 + (c) due to copyright terms
1.8 +
1.9 +use"mathengine.sml";
1.10 +*)
1.11 +
1.12 +signature MATHENGINE =
1.13 + sig
1.14 + type nxt_
1.15 + (* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *)
1.16 + type NEW
1.17 + type lOc_
1.18 + (*datatype
1.19 + lOc_ =
1.20 + ERror of string
1.21 + | UNsafe of CalcHead.calcstate'
1.22 + | Updated of CalcHead.calcstate' *)
1.23 +
1.24 + val CalcTreeTEST :
1.25 + fmz list ->
1.26 + pos' * NEW * mout * (string * tac) * safe * ptree
1.27 +
1.28 + val TESTg_form : ptree * (int list * pos_) -> mout
1.29 + val autocalc :
1.30 + pos' list ->
1.31 + pos' ->
1.32 + (ptree * pos') * taci list ->
1.33 + auto -> string * pos' list * (ptree * pos')
1.34 + val detailstep : ptree -> pos' -> string * ptree * pos'
1.35 + (* val e_tac_ : tac_ *)
1.36 + val f2str : mout -> cterm'
1.37 + (* val get_pblID : ptree * pos' -> pblID option *)
1.38 + val initmatch : ptree -> pos' -> ptform
1.39 + (* val loc_solve_ :
1.40 + string * tac_ -> ptree * (int list * pos_) -> lOc_ *)
1.41 + (* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *)
1.42 + val locatetac : (*tests only*)
1.43 + tac ->
1.44 + ptree * (posel list * pos_) ->
1.45 + string * (taci list * pos' list * (ptree * (posel list * pos_)))
1.46 + val me :
1.47 + tac'_ ->
1.48 + pos' ->
1.49 + NEW ->
1.50 + ptree -> pos' * NEW * mout * tac'_ * safe * ptree
1.51 +
1.52 + val nxt_specify_ : ptree * (int list * pos_) -> calcstate'(*tests only*)
1.53 + val set_method : metID -> ptree * pos' -> ptree * ocalhd
1.54 + val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
1.55 + val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
1.56 + val step : pos' -> calcstate -> string * calcstate'
1.57 + val trymatch : pblID -> ptree -> pos' -> ptform
1.58 + val tryrefine : pblID -> ptree -> pos' -> ptform
1.59 + end
1.60 +
1.61 +
1.62 +
1.63 +(*------------------------------------------------------------------(**)
1.64 +structure MathEngine : MATHENGINE =
1.65 +struct
1.66 +(**)------------------------------------------------------------------*)
1.67 +
1.68 +fun get_pblID (pt, (p,_):pos') =
1.69 + let val p' = par_pblobj pt p
1.70 + val (_,pI,_) = get_obj g_spec pt p'
1.71 + val (_,(_,oI,_),_) = get_obj g_origin pt p'
1.72 + in if pI <> e_pblID then SOME pI
1.73 + else if oI <> e_pblID then SOME oI
1.74 + else NONE end;
1.75 +(*fun get_pblID (pt, (p,_):pos') =
1.76 + ((snd3 o (get_obj g_spec pt)) (par_pblobj pt p));*)
1.77 +
1.78 +
1.79 +(*--vvv--dummies for test*)
1.80 +val e_tac_ = Tac_ (Pure.thy,"","","");
1.81 +datatype lOc_ =
1.82 + ERror of string (*after loc_specify, loc_solve*)
1.83 +| UNsafe of calcstate' (*after loc_specify, loc_solve*)
1.84 +| Updated of calcstate'; (*after loc_specify, loc_solve*)
1.85 +fun loc_specify_ m (pt,pos) =
1.86 +(* val pos = ip;
1.87 + *)
1.88 + let val (p,_,f,_,s,pt) = specify m pos [] pt;
1.89 +(* val (_,_,_,_,_,pt')= specify m pos [] pt;
1.90 + *)
1.91 + in case f of
1.92 + (Error' (Error_ e)) => ERror e
1.93 + | _ => Updated ([], [], (pt,p)) end;
1.94 +
1.95 +(*. TODO push return-value cs' into solve and rename solve->loc_solve?_? .*)
1.96 +(* val (m, pos) = ((mI,m), ip);
1.97 + val (m,(pt,pos) ) = ((mI,m), ptp);
1.98 + *)
1.99 +fun loc_solve_ m (pt,pos) =
1.100 + let val (msg, cs') = solve m (pt, pos);
1.101 +(* val (tacis,dels,(pt',p')) = cs';
1.102 + (writeln o istate2str) (get_istate pt' p');
1.103 + (term2str o fst) (get_obj g_result pt' (fst p'));
1.104 + *)
1.105 + in case msg of
1.106 + "ok" => Updated cs'
1.107 + | msg => ERror msg
1.108 + end;
1.109 +
1.110 +datatype nxt_ =
1.111 + HElpless (**)
1.112 + | Nexts of calcstate; (**)
1.113 +
1.114 +(*. locate a tactic in a script and apply it if possible .*)
1.115 +(*report applicability of tac in tacis; pt is dropped in setNextTactic*)
1.116 +fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
1.117 +(* val ptp as (pt, p) = (pt, p);
1.118 + val ptp as (pt, p) = (pt, ip);
1.119 + *)
1.120 + | locatetac tac (ptp as (pt, p)) =
1.121 + let val (mI,m) = mk_tac'_ tac;
1.122 + in case applicable_in p pt m of
1.123 + Notappl e => ("not-applicable", ([],[], ptp):calcstate')
1.124 + | Appl m =>
1.125 +(* val Appl m = applicable_in p pt m;
1.126 + *)
1.127 + let val x = if member op = specsteps mI
1.128 + then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
1.129 + in case x of
1.130 + ERror e => ("failure", ([], [], ptp))
1.131 + (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
1.132 + | UNsafe cs' => ("unsafe-ok", cs')
1.133 + | Updated (cs' as (_,_,(_,p'))) =>
1.134 + (*ev.SEVER.tacs like Begin_Trans*)
1.135 + (if p' = ([],Res) then "end-of-calculation" else "ok",
1.136 + cs')(*for -"- user to ask ? *)
1.137 + end
1.138 + end;
1.139 +
1.140 +
1.141 +(*------------------------------------------------------------------
1.142 +fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*)
1.143 +(*----------------------------------------------------from solve.sml*)
1.144 + | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) =
1.145 + let (*val rls = the (assoc(!ruleset',rls'))
1.146 + handle _ => raise error ("solve: '"^rls'^"' not known");*)
1.147 + val thy = assoc_thy thy';
1.148 + val (srls, sc, is) =
1.149 + case rls of
1.150 + Rrls {scr=sc as Rfuns {init_state=ii,...},...} =>
1.151 + (e_rls, sc, RrlsState (ii t))
1.152 + | Rls {srls=srls,scr=sc as Script s,...} =>
1.153 + (srls, sc, ScrState ([(one_scr_arg s,t)], [],
1.154 + NONE, e_term, Sundef, true));
1.155 + val pt = update_tac pt (fst p) (Detail_Set (id_rls rls));
1.156 + val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt;
1.157 + val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);
1.158 + val aopt = applicable_in p pt nx;
1.159 + in case aopt of
1.160 + Notappl s => raise error ("solve Detail_Set: "^s)
1.161 + (* val Appl m = aopt;
1.162 + *)
1.163 + | Appl m => solve ("discardFIXME",m) p pt end
1.164 +------------------------------------------------------------------*)
1.165 +
1.166 +
1.167 +(*iterated by nxt_me; there (the resulting) ptp dropped
1.168 + may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
1.169 +(* val (ptp as (pt, pos as (p,p_))) = ptp;
1.170 + val (ptp as (pt, pos as (p,p_))) = (pt,ip);
1.171 + *)
1.172 +fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
1.173 + let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
1.174 + probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.175 + in if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
1.176 + then case mI' of
1.177 + ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
1.178 + | _ => nxt_specif Model_Problem (pt, (p,Pbl))
1.179 + else let val cpI = if pI = e_pblID then pI' else pI;
1.180 + val cmI = if mI = e_metID then mI' else mI;
1.181 + val {ppc,prls,where_,...} = get_pbt cpI;
1.182 + val pre = check_preconds "thy 100820" prls where_ probl;
1.183 + val pb = foldl and_ (true, map fst pre);
1.184 + (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
1.185 + val (_,tac) =
1.186 + nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
1.187 + (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
1.188 + in case tac of
1.189 + Apply_Method mI =>
1.190 +(* val Apply_Method mI = tac;
1.191 + *)
1.192 + nxt_solv (Apply_Method' (mI, NONE, e_istate)) e_istate ptp
1.193 + | _ => nxt_specif tac ptp end
1.194 + end;
1.195 +
1.196 +
1.197 +(*.specify a new method;
1.198 + WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*)
1.199 +fun set_method (mI:metID) ptp =
1.200 + let val ([(_, Specify_Method' (_, _, mits), _)], [], (pt, pos as (p,_))) =
1.201 + nxt_specif (Specify_Method mI) ptp
1.202 + val pre = [] (*...from Specify_Method'*)
1.203 + val complete = true (*...from Specify_Method'*)
1.204 + (*from Specify_Method' ? vvv, vvv ?*)
1.205 + val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
1.206 + in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end;
1.207 +
1.208 +(* val ([(_, Specify_Method' (_, _, mits), _)], [],_) =
1.209 + nxt_specif (Specify_Method mI) ptp;
1.210 + *)
1.211 +
1.212 +(*.specify a new problem;
1.213 + WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*)
1.214 +(* val (pI, ptp) = (pI, (pt, ip));
1.215 + *)
1.216 +fun set_problem pI (ptp: ptree * pos') =
1.217 + let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
1.218 + _, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp
1.219 + (*from Specify_Problem' ? vvv, vvv ?*)
1.220 + val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
1.221 + in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
1.222 +
1.223 +fun set_theory (tI:thyID) (ptp: ptree * pos') =
1.224 + let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
1.225 + _, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp
1.226 + (*from Specify_Theory' ? vvv, vvv ?*)
1.227 + val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
1.228 + in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
1.229 +
1.230 +(*.does a step forward; returns tactic used, ctree updated.
1.231 +TODO.WN0512 redesign after specify-phase became more separated from solve-phase
1.232 +arg ip:
1.233 + calcstate
1.234 +.*)
1.235 +(* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
1.236 + val (ip as (_,p_), (ptp as (pt,p), tacis)) = (pos, cs);
1.237 + val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
1.238 + val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
1.239 + *)
1.240 +fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
1.241 + let val pIopt = get_pblID (pt,ip);
1.242 + in if (*p = ([],Res) orelse*) ip = ([],Res)
1.243 + then ("end-of-calculation",(tacis, [], ptp):calcstate') else
1.244 + case tacis of
1.245 + (_::_) =>
1.246 +(* val((tac,_,_)::_) = tacis;
1.247 + *)
1.248 + if ip = p (*the request is done where ptp waits for*)
1.249 + then let val (pt',c',p') = generate tacis (pt,[],p)
1.250 + in ("ok", (tacis, c', (pt', p'))) end
1.251 + else (case (if member op = [Pbl,Met] p_
1.252 + then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.253 + handle _ => ([],[],ptp)(*e.g.by Add_Given "equality///"*)
1.254 + of cs as ([],_,_) => ("helpless", cs)
1.255 + | cs => ("ok", cs))
1.256 +(* val [] = tacis;
1.257 + *)
1.258 + | _ => (case pIopt of
1.259 + NONE => ("no-fmz-spec", ([], [], ptp))
1.260 + | SOME pI =>
1.261 +(* val SOME pI = pIopt;
1.262 + val cs=(if member op = [Pbl,Met] p_ andalso is_none(get_obj g_env pt (fst p))
1.263 + then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.264 + handle _ => ([], ptp);
1.265 + *)
1.266 + (case (if member op = [Pbl,Met] p_
1.267 + andalso is_none (get_obj g_env pt (fst p))
1.268 + (*^^^^^^^^: Apply_Method without init_form*)
1.269 + then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip) )
1.270 + handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*)
1.271 + of cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
1.272 + | cs => ("ok", cs)))
1.273 + end;
1.274 +
1.275 +(* (nxt_solve_ (pt,ip)) handle e => print_exn e ;
1.276 +
1.277 + *)
1.278 +
1.279 +
1.280 +
1.281 +
1.282 +(*.does several steps within one calculation as given by "type auto";
1.283 + the steps may arbitrarily go into and leave different phases,
1.284 + i.e. specify-phase and solve-phase.*)
1.285 +(*TODO.WN0512 ? redesign after the phases have been more separated
1.286 + at the fron-end in 05:
1.287 + eg. CompleteCalcHead could be done by a separate fun !!!*)
1.288 +(* val (ip, cs as (ptp as (pt,p),tacis)) = (get_pos cI 1, get_calc cI);
1.289 + val (ip, cs as (ptp as (pt,p),tacis)) = (pold, get_calc cI);
1.290 + val (c, ip, cs as (ptp as (_,p),tacis), Step s) =
1.291 + ([]:pos' list, pold, get_calc cI, auto);
1.292 + *)
1.293 +fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
1.294 + if s <= 1
1.295 + then let val (str, (_, c', ptp)) = step ip cs;(*1*)
1.296 + (*at least does 1 step, ev.1 too much*)
1.297 + in (str, c@c', ptp) end
1.298 + else let val (str, (_, c', ptp as (_, p))) = step ip cs;
1.299 + in if str = "ok"
1.300 + then autocalc (c@c') p (ptp,[]) (Step (s-1))
1.301 + else (str, c@c', ptp) end
1.302 +(*handles autoord <= 3, autoord > 3 handled by all_/complete_solve*)
1.303 + | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto=
1.304 +(* val (c:pos' list, (pos as (_,p_)),((pt,_),_),auto) =
1.305 + ([], pold, get_calc cI, auto);
1.306 + *)
1.307 + if autoord auto > 3 andalso just_created (pt, pos)
1.308 + then let val ptp = all_modspec (pt, pos);
1.309 + in all_solve auto c ptp end
1.310 + else
1.311 + if member op = [Pbl, Met] p_
1.312 + then if not (is_complete_mod (pt, pos))
1.313 + then let val ptp = complete_mod (pt, pos)
1.314 + in if autoord auto < 3 then ("ok", c, ptp)
1.315 + else
1.316 + if not (is_complete_spec ptp)
1.317 + then let val ptp = complete_spec ptp
1.318 + in if autoord auto = 3 then ("ok", c, ptp)
1.319 + else all_solve auto c ptp
1.320 + end
1.321 + else if autoord auto = 3 then ("ok", c, ptp)
1.322 + else all_solve auto c ptp
1.323 + end
1.324 + else
1.325 + if not (is_complete_spec (pt,pos))
1.326 + then let val ptp = complete_spec (pt, pos)
1.327 + in if autoord auto = 3 then ("ok", c, ptp)
1.328 + else all_solve auto c ptp
1.329 + end
1.330 + else if autoord auto = 3 then ("ok", c, (pt, pos))
1.331 + else all_solve auto c (pt, pos)
1.332 + else complete_solve auto c (pt, pos);
1.333 +(* val pbl = get_obj g_pbl (fst ptp) [];
1.334 + val (oris,_,_) = get_obj g_origin (fst ptp) [];
1.335 +*)
1.336 +
1.337 +
1.338 +
1.339 +
1.340 +
1.341 +(*.initialiye matching; before 'tryMatch' get the pblID to match with:
1.342 + if no pbl has been specified, take the init from origin.*)
1.343 +(*fun initmatch pt (pos as (p,_):pos') =
1.344 + let val PblObj {probl,origin=(os,(_,pI,_),_),spec=(dI',pI',mI'),...} =
1.345 + get_obj I pt p
1.346 + val pblID = if pI' = e_pblID
1.347 + then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
1.348 + takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
1.349 + else pI'
1.350 + val spec = (dI',pblID,mI')
1.351 + val {ppc,where_,prls,...} = get_pbt pblID
1.352 + val (model_ok, (pbl, pre)) =
1.353 + match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os
1.354 + in ModSpec (ocalhd_complete pbl pre spec,
1.355 + Pbl, e_term, pbl, pre, spec) end;*)
1.356 +fun initcontext_pbl pt (pos as (p,_):pos') =
1.357 + let val PblObj {probl,origin=(os,(_,pI,_),hdl),spec=(dI',pI',mI'),...} =
1.358 + get_obj I pt p
1.359 + val pblID = if pI' = e_pblID
1.360 + then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
1.361 + takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
1.362 + else pI'
1.363 + val {ppc,where_,prls,...} = get_pbt pblID
1.364 + val (model_ok, (pbl, pre)) =
1.365 + match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os
1.366 + in (model_ok, pblID, hdl, pbl, pre) end;
1.367 +
1.368 +fun initcontext_met pt (pos as (p,_):pos') =
1.369 + let val PblObj {meth,origin=(os,(_,_,mI), _),spec=(_, _, mI'),...} =
1.370 + get_obj I pt p
1.371 + val metID = if mI' = e_metID
1.372 + then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
1.373 + takelast (2, mI) (*FIXME.WN051125 a hack, impl.^^^*)
1.374 + else mI'
1.375 + val {ppc,pre,prls,scr,...} = get_met metID
1.376 + val (model_ok, (pbl, pre)) =
1.377 + match_itms_oris (assoc_thy "Isac.thy") meth (ppc,pre,prls) os
1.378 + in (model_ok, metID, scr, pbl, pre) end;
1.379 +
1.380 +(*.match the model of a problem at pos p
1.381 + with the model-pattern of the problem with pblID*)
1.382 +fun context_pbl pI pt (p:pos) =
1.383 + let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
1.384 + val {ppc,where_,prls,...} = get_pbt pI
1.385 + val (model_ok, (pbl, pre)) =
1.386 + match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os
1.387 + in (model_ok, pI, hdl, pbl, pre) end;
1.388 +
1.389 +fun context_met mI pt (p:pos) =
1.390 + let val PblObj {meth,origin=(os,_,hdl),...} = get_obj I pt p
1.391 + val {ppc,pre,prls,scr,...} = get_met mI
1.392 + val (model_ok, (pbl, pre)) =
1.393 + match_itms_oris (assoc_thy "Isac.thy") meth (ppc,pre,prls) os
1.394 + in (model_ok, mI, scr, pbl, pre) end
1.395 +
1.396 +
1.397 +(* val (pI, pt, pos as (p,_)) = (pblID, pt, p);
1.398 + *)
1.399 +fun tryrefine pI pt (pos as (p,_):pos') =
1.400 + let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
1.401 + in case refine_pbl (assoc_thy "Isac.thy") pI probl of
1.402 + NONE => (*copy from context_pbl*)
1.403 + let val {ppc,where_,prls,...} = get_pbt pI
1.404 + val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy")
1.405 + probl (ppc,where_,prls) os
1.406 + in (false, pI, hdl, pbl, pre) end
1.407 + | SOME (pI, (pbl, pre)) =>
1.408 + (true, pI, hdl, pbl, pre)
1.409 + end;
1.410 +
1.411 +(* val (pt, (pos as (p,p_):pos')) = (pt, ip);
1.412 + *)
1.413 +fun detailstep pt (pos as (p,p_):pos') =
1.414 + let val nd = get_nd pt p
1.415 + val cn = children nd
1.416 + in if null cn
1.417 + then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
1.418 + then detailrls pt pos
1.419 + else ("no-Rewrite_Set...", EmptyPtree, e_pos')
1.420 + else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*),
1.421 + (p @ [length (children (get_nd pt p))], Res) )
1.422 + end;
1.423 +
1.424 +
1.425 +
1.426 +(***. for mathematics authoring on sml-toplevel; no XML .***)
1.427 +
1.428 +type NEW = int list;
1.429 +(* val sp = (dI',pI',mI');
1.430 + *)
1.431 +
1.432 +(*15.8.03 for me with loc_specify/solve, nxt_specify/solve
1.433 + delete as soon as TESTg_form -> _mout_ dropped*)
1.434 +fun TESTg_form ptp =
1.435 +(* val ptp = (pt,p);
1.436 + *)
1.437 + let val (form,_,_) = pt_extract ptp
1.438 + in case form of
1.439 + Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
1.440 + | ModSpec (_,p_, head, gfr, pre, _) =>
1.441 + Form' (PpcKF (0,EdUndef,0,Nundef,
1.442 + (case p_ of Pbl => Problem[] | Met => Method[],
1.443 + itms2itemppc (assoc_thy"Isac.thy") gfr pre)))
1.444 + end;
1.445 +
1.446 +(*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;
1.447 + compare "fun CalcTree" which DOES decode.*)
1.448 +fun CalcTreeTEST [(fmz, sp):fmz] =
1.449 +(* val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
1.450 + val [(fmz, sp):fmz] = [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
1.451 + *)
1.452 + let val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
1.453 + val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
1.454 + val f = TESTg_form (pt,p)
1.455 + in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end;
1.456 +
1.457 +(*for tests > 15.8.03 after separation setnexttactic / nextTac:
1.458 + external view: me should be used by math-authors as done so far
1.459 + internal view: loc_specify/solve, nxt_specify/solve used
1.460 + i.e. same as in setnexttactic / nextTac*)
1.461 +(*ENDE TESTPHASE 08/10.03:
1.462 + NEW loeschen, eigene Version von locatetac, step
1.463 + meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
1.464 +
1.465 +(* val ((_,tac), p, _, pt) = (nxt, p, c, pt);
1.466 + *)
1.467 +fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
1.468 + let val (pt, p) =
1.469 +(* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p);
1.470 + p = ([1, 9], Res);
1.471 + (writeln o istate2str) (get_istate pt p);
1.472 + *)
1.473 + (*locatetac is here for testing by me; step would suffice in me*)
1.474 + case locatetac tac (pt,p) of
1.475 + ("ok", (_, _, ptp)) => ptp
1.476 + | ("unsafe-ok", (_, _, ptp)) => ptp
1.477 + | ("not-applicable",_) => (pt, p)
1.478 + | ("end-of-calculation", (_, _, ptp)) => ptp
1.479 + | ("failure",_) => raise error "sys-error";
1.480 + val (_, ts) =
1.481 +(* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]);
1.482 + *)
1.483 + (case step p ((pt, e_pos'),[]) of
1.484 + ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
1.485 + | ("helpless",_) => ("helpless: cannot propose tac", [])
1.486 + | ("no-fmz-spec",_) => raise error "no-fmz-spec"
1.487 + | ("end-of-calculation", (ts, _, _)) => ("",ts))
1.488 + handle _ => raise error "sys-error";
1.489 + val tac = case ts of tacis as (_::_) =>
1.490 +(* val tacis as (_::_) = ts;
1.491 + *)
1.492 + let val (tac,_,_) = last_elem tacis
1.493 + in tac end
1.494 + | _ => if p = ([],Res) then End_Proof'
1.495 + else Empty_Tac;
1.496 + (*form output comes from locatetac*)
1.497 + in(p:pos',[]:NEW, TESTg_form (pt, p),
1.498 + (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
1.499 +
1.500 +(*for quick test-print-out, until 'type inout' is removed*)
1.501 +fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
1.502 +
1.503 +
1.504 +
1.505 +(*------------------------------------------------------------------(**)
1.506 +end
1.507 +open MathEngine;
1.508 +(**)------------------------------------------------------------------*)
1.509 +