1.1 --- a/src/Tools/isac/ME/mathengine.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,506 +0,0 @@
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 -