neuper@37906
|
1 |
(* The _functional_ mathematics engine, ie. without a state.
|
neuper@37906
|
2 |
Input and output are Isabelle's formulae as strings.
|
neuper@37906
|
3 |
authors: Walther Neuper 2000
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
use"mathengine.sml";
|
neuper@37906
|
7 |
*)
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
signature MATHENGINE =
|
neuper@37906
|
10 |
sig
|
neuper@37906
|
11 |
type nxt_
|
neuper@37906
|
12 |
(* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *)
|
neuper@37906
|
13 |
type NEW
|
neuper@37906
|
14 |
type lOc_
|
neuper@37906
|
15 |
(*datatype
|
neuper@37906
|
16 |
lOc_ =
|
neuper@37906
|
17 |
ERror of string
|
neuper@37906
|
18 |
| UNsafe of CalcHead.calcstate'
|
neuper@37906
|
19 |
| Updated of CalcHead.calcstate' *)
|
neuper@37906
|
20 |
|
neuper@37906
|
21 |
val CalcTreeTEST :
|
neuper@37906
|
22 |
fmz list ->
|
neuper@37906
|
23 |
pos' * NEW * mout * (string * tac) * safe * ptree
|
neuper@37906
|
24 |
|
neuper@37906
|
25 |
val TESTg_form : ptree * (int list * pos_) -> mout
|
neuper@37906
|
26 |
val autocalc :
|
neuper@37906
|
27 |
pos' list ->
|
neuper@37906
|
28 |
pos' ->
|
neuper@37906
|
29 |
(ptree * pos') * taci list ->
|
neuper@37906
|
30 |
auto -> string * pos' list * (ptree * pos')
|
neuper@37906
|
31 |
val detailstep : ptree -> pos' -> string * ptree * pos'
|
neuper@37906
|
32 |
(* val e_tac_ : tac_ *)
|
neuper@37906
|
33 |
val f2str : mout -> cterm'
|
neuper@37931
|
34 |
(* val get_pblID : ptree * pos' -> pblID option *)
|
neuper@37906
|
35 |
val initmatch : ptree -> pos' -> ptform
|
neuper@37906
|
36 |
(* val loc_solve_ :
|
neuper@37906
|
37 |
string * tac_ -> ptree * (int list * pos_) -> lOc_ *)
|
neuper@37906
|
38 |
(* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *)
|
neuper@37906
|
39 |
val locatetac : (*tests only*)
|
neuper@37906
|
40 |
tac ->
|
neuper@37906
|
41 |
ptree * (posel list * pos_) ->
|
neuper@37906
|
42 |
string * (taci list * pos' list * (ptree * (posel list * pos_)))
|
neuper@37906
|
43 |
val me :
|
neuper@37906
|
44 |
tac'_ ->
|
neuper@37906
|
45 |
pos' ->
|
neuper@37906
|
46 |
NEW ->
|
neuper@37906
|
47 |
ptree -> pos' * NEW * mout * tac'_ * safe * ptree
|
neuper@37906
|
48 |
|
neuper@37906
|
49 |
val nxt_specify_ : ptree * (int list * pos_) -> calcstate'(*tests only*)
|
neuper@37906
|
50 |
val set_method : metID -> ptree * pos' -> ptree * ocalhd
|
neuper@37906
|
51 |
val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
|
neuper@37906
|
52 |
val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
|
neuper@37906
|
53 |
val step : pos' -> calcstate -> string * calcstate'
|
neuper@37906
|
54 |
val trymatch : pblID -> ptree -> pos' -> ptform
|
neuper@37906
|
55 |
val tryrefine : pblID -> ptree -> pos' -> ptform
|
neuper@37906
|
56 |
end
|
neuper@37906
|
57 |
|
neuper@37906
|
58 |
|
neuper@37906
|
59 |
|
neuper@37906
|
60 |
(*------------------------------------------------------------------(**)
|
neuper@37906
|
61 |
structure MathEngine : MATHENGINE =
|
neuper@37906
|
62 |
struct
|
neuper@37906
|
63 |
(**)------------------------------------------------------------------*)
|
neuper@37906
|
64 |
|
neuper@37906
|
65 |
fun get_pblID (pt, (p,_):pos') =
|
neuper@37906
|
66 |
let val p' = par_pblobj pt p
|
neuper@37906
|
67 |
val (_,pI,_) = get_obj g_spec pt p'
|
neuper@37906
|
68 |
val (_,(_,oI,_),_) = get_obj g_origin pt p'
|
neuper@37926
|
69 |
in if pI <> e_pblID then SOME pI
|
neuper@37926
|
70 |
else if oI <> e_pblID then SOME oI
|
neuper@37926
|
71 |
else NONE end;
|
neuper@37906
|
72 |
(*fun get_pblID (pt, (p,_):pos') =
|
neuper@37906
|
73 |
((snd3 o (get_obj g_spec pt)) (par_pblobj pt p));*)
|
neuper@37906
|
74 |
|
neuper@37906
|
75 |
|
neuper@37906
|
76 |
(*--vvv--dummies for test*)
|
neuper@37906
|
77 |
val e_tac_ = Tac_ (Pure.thy,"","","");
|
neuper@37906
|
78 |
datatype lOc_ =
|
neuper@37906
|
79 |
ERror of string (*after loc_specify, loc_solve*)
|
neuper@37906
|
80 |
| UNsafe of calcstate' (*after loc_specify, loc_solve*)
|
neuper@37906
|
81 |
| Updated of calcstate'; (*after loc_specify, loc_solve*)
|
neuper@37906
|
82 |
fun loc_specify_ m (pt,pos) =
|
neuper@37906
|
83 |
(* val pos = ip;
|
neuper@37906
|
84 |
*)
|
neuper@37906
|
85 |
let val (p,_,f,_,s,pt) = specify m pos [] pt;
|
neuper@37906
|
86 |
(* val (_,_,_,_,_,pt')= specify m pos [] pt;
|
neuper@37906
|
87 |
*)
|
neuper@37906
|
88 |
in case f of
|
neuper@37906
|
89 |
(Error' (Error_ e)) => ERror e
|
neuper@37906
|
90 |
| _ => Updated ([], [], (pt,p)) end;
|
neuper@37906
|
91 |
|
neuper@37906
|
92 |
(*. TODO push return-value cs' into solve and rename solve->loc_solve?_? .*)
|
neuper@37906
|
93 |
(* val (m, pos) = ((mI,m), ip);
|
neuper@37906
|
94 |
val (m,(pt,pos) ) = ((mI,m), ptp);
|
neuper@37906
|
95 |
*)
|
neuper@37906
|
96 |
fun loc_solve_ m (pt,pos) =
|
neuper@37906
|
97 |
let val (msg, cs') = solve m (pt, pos);
|
neuper@37906
|
98 |
(* val (tacis,dels,(pt',p')) = cs';
|
neuper@38015
|
99 |
(tracing o istate2str) (get_istate pt' p');
|
neuper@37906
|
100 |
(term2str o fst) (get_obj g_result pt' (fst p'));
|
neuper@37906
|
101 |
*)
|
neuper@37906
|
102 |
in case msg of
|
neuper@37906
|
103 |
"ok" => Updated cs'
|
neuper@37906
|
104 |
| msg => ERror msg
|
neuper@37906
|
105 |
end;
|
neuper@37906
|
106 |
|
neuper@37906
|
107 |
datatype nxt_ =
|
neuper@37906
|
108 |
HElpless (**)
|
neuper@37906
|
109 |
| Nexts of calcstate; (**)
|
neuper@37906
|
110 |
|
neuper@37906
|
111 |
(*. locate a tactic in a script and apply it if possible .*)
|
neuper@37906
|
112 |
(*report applicability of tac in tacis; pt is dropped in setNextTactic*)
|
neuper@37906
|
113 |
fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
|
neuper@37906
|
114 |
| locatetac tac (ptp as (pt, p)) =
|
neuper@41975
|
115 |
let val (mI,m) = mk_tac'_ tac;
|
neuper@41975
|
116 |
in case applicable_in p pt m of
|
neuper@41975
|
117 |
Notappl e => ("not-applicable", ([],[], ptp):calcstate')
|
neuper@41975
|
118 |
| Appl m =>
|
neuper@41975
|
119 |
let
|
neuper@41975
|
120 |
val x = if member op = specsteps mI
|
neuper@41975
|
121 |
then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
|
neuper@41975
|
122 |
in case x of
|
neuper@41975
|
123 |
ERror e => ("failure", ([], [], ptp))
|
neuper@41975
|
124 |
(*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
|
neuper@41975
|
125 |
| UNsafe cs' => ("unsafe-ok", cs')
|
neuper@41975
|
126 |
| Updated (cs' as (_,_,(_,p'))) => (*ev.SEVER.tacs like Begin_Trans*)
|
neuper@41975
|
127 |
(if p' = ([],Res) then "end-of-calculation" else "ok", cs')
|
neuper@41975
|
128 |
(*for SEVER.tacs user to ask ? *)
|
neuper@41975
|
129 |
end
|
neuper@41975
|
130 |
end;
|
neuper@37906
|
131 |
|
neuper@37906
|
132 |
(*iterated by nxt_me; there (the resulting) ptp dropped
|
neuper@37906
|
133 |
may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
|
neuper@37906
|
134 |
fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
|
neuper@41973
|
135 |
let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
|
neuper@41988
|
136 |
probl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
|
neuper@41973
|
137 |
in
|
neuper@41973
|
138 |
if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
|
neuper@41973
|
139 |
then
|
neuper@41973
|
140 |
case mI' of
|
neuper@41973
|
141 |
["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
|
neuper@41973
|
142 |
| _ => nxt_specif Model_Problem (pt, (p,Pbl))
|
neuper@41973
|
143 |
else
|
neuper@41973
|
144 |
let
|
neuper@41973
|
145 |
val cpI = if pI = e_pblID then pI' else pI;
|
neuper@41973
|
146 |
val cmI = if mI = e_metID then mI' else mI;
|
neuper@41973
|
147 |
val {ppc, prls, where_, ...} = get_pbt cpI;
|
neuper@41973
|
148 |
val pre = check_preconds "thy 100820" prls where_ probl;
|
neuper@41973
|
149 |
val pb = foldl and_ (true, map fst pre);
|
neuper@41973
|
150 |
(*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
|
neuper@41973
|
151 |
val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
|
neuper@41973
|
152 |
(ppc, (#ppc o get_met) cmI) (dI, pI, mI);
|
neuper@37906
|
153 |
in case tac of
|
neuper@41973
|
154 |
Apply_Method mI =>
|
neuper@41973
|
155 |
nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
|
neuper@41973
|
156 |
| _ => nxt_specif tac ptp end
|
neuper@41973
|
157 |
end;
|
neuper@37906
|
158 |
|
neuper@37906
|
159 |
(*.specify a new method;
|
neuper@37906
|
160 |
WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*)
|
neuper@37906
|
161 |
fun set_method (mI:metID) ptp =
|
neuper@37906
|
162 |
let val ([(_, Specify_Method' (_, _, mits), _)], [], (pt, pos as (p,_))) =
|
neuper@37906
|
163 |
nxt_specif (Specify_Method mI) ptp
|
neuper@37906
|
164 |
val pre = [] (*...from Specify_Method'*)
|
neuper@37906
|
165 |
val complete = true (*...from Specify_Method'*)
|
neuper@37906
|
166 |
(*from Specify_Method' ? vvv, vvv ?*)
|
neuper@37906
|
167 |
val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
|
neuper@37906
|
168 |
in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end;
|
neuper@37906
|
169 |
|
neuper@37906
|
170 |
(*.specify a new problem;
|
neuper@37906
|
171 |
WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*)
|
neuper@37906
|
172 |
fun set_problem pI (ptp: ptree * pos') =
|
neuper@37906
|
173 |
let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
|
neuper@37906
|
174 |
_, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp
|
neuper@37906
|
175 |
(*from Specify_Problem' ? vvv, vvv ?*)
|
neuper@37906
|
176 |
val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
|
neuper@37906
|
177 |
in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
|
neuper@37906
|
178 |
|
neuper@37906
|
179 |
fun set_theory (tI:thyID) (ptp: ptree * pos') =
|
neuper@37906
|
180 |
let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
|
neuper@37906
|
181 |
_, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp
|
neuper@37906
|
182 |
(*from Specify_Theory' ? vvv, vvv ?*)
|
neuper@37906
|
183 |
val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
|
neuper@37906
|
184 |
in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
|
neuper@37906
|
185 |
|
neuper@41981
|
186 |
(* does a step forward; returns tactic used, ctree updated.
|
neuper@41981
|
187 |
TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
|
neuper@37906
|
188 |
fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
|
neuper@41972
|
189 |
let val pIopt = get_pblID (pt,ip);
|
neuper@41972
|
190 |
in
|
neuper@41972
|
191 |
if (*p = ([],Res) orelse*) ip = ([],Res)
|
neuper@41972
|
192 |
then ("end-of-calculation",(tacis, [], ptp):calcstate')
|
neuper@41972
|
193 |
else
|
neuper@41972
|
194 |
case tacis of
|
neuper@41972
|
195 |
(_::_) =>
|
neuper@41972
|
196 |
if ip = p (*the request is done where ptp waits for*)
|
neuper@41972
|
197 |
then
|
neuper@41972
|
198 |
let val (pt',c',p') = generate tacis (pt,[],p)
|
neuper@41972
|
199 |
in ("ok", (tacis, c', (pt', p'))) end
|
neuper@41972
|
200 |
else (case (if member op = [Pbl,Met] p_
|
neuper@41972
|
201 |
then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
|
neuper@41972
|
202 |
handle _ => ([],[],ptp)(*e.g. Add_Given "equality///"*) of
|
neuper@41972
|
203 |
cs as ([],_,_) => ("helpless", cs)
|
neuper@41972
|
204 |
| cs => ("ok", cs))
|
neuper@41972
|
205 |
| _ => (case pIopt of
|
neuper@41972
|
206 |
NONE => ("no-fmz-spec", ([], [], ptp))
|
neuper@41972
|
207 |
| SOME pI =>
|
neuper@41972
|
208 |
(case (if member op = [Pbl,Met] p_
|
neuper@41972
|
209 |
andalso is_none (get_obj g_env pt (fst p))
|
neuper@41972
|
210 |
(*^^^^^^^^: Apply_Method without init_form*)
|
neuper@41982
|
211 |
then nxt_specify_ (pt, ip)
|
neuper@41972
|
212 |
else nxt_solve_ (pt,ip) )
|
neuper@41972
|
213 |
handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality///"*) of
|
neuper@41972
|
214 |
cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
|
neuper@41972
|
215 |
| cs => ("ok", cs)))
|
neuper@41972
|
216 |
end;
|
neuper@37906
|
217 |
|
neuper@37906
|
218 |
(*.does several steps within one calculation as given by "type auto";
|
neuper@37906
|
219 |
the steps may arbitrarily go into and leave different phases,
|
neuper@37906
|
220 |
i.e. specify-phase and solve-phase.*)
|
neuper@37906
|
221 |
(*TODO.WN0512 ? redesign after the phases have been more separated
|
neuper@37906
|
222 |
at the fron-end in 05:
|
neuper@37906
|
223 |
eg. CompleteCalcHead could be done by a separate fun !!!*)
|
neuper@37906
|
224 |
fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
|
neuper@37906
|
225 |
if s <= 1
|
neuper@37906
|
226 |
then let val (str, (_, c', ptp)) = step ip cs;(*1*)
|
neuper@37906
|
227 |
(*at least does 1 step, ev.1 too much*)
|
neuper@37906
|
228 |
in (str, c@c', ptp) end
|
neuper@37906
|
229 |
else let val (str, (_, c', ptp as (_, p))) = step ip cs;
|
neuper@37906
|
230 |
in if str = "ok"
|
neuper@37906
|
231 |
then autocalc (c@c') p (ptp,[]) (Step (s-1))
|
neuper@37906
|
232 |
else (str, c@c', ptp) end
|
neuper@37906
|
233 |
(*handles autoord <= 3, autoord > 3 handled by all_/complete_solve*)
|
neuper@37906
|
234 |
| autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto=
|
neuper@37906
|
235 |
(* val (c:pos' list, (pos as (_,p_)),((pt,_),_),auto) =
|
neuper@37906
|
236 |
([], pold, get_calc cI, auto);
|
neuper@37906
|
237 |
*)
|
neuper@37906
|
238 |
if autoord auto > 3 andalso just_created (pt, pos)
|
neuper@37906
|
239 |
then let val ptp = all_modspec (pt, pos);
|
neuper@37906
|
240 |
in all_solve auto c ptp end
|
neuper@37906
|
241 |
else
|
neuper@37939
|
242 |
if member op = [Pbl, Met] p_
|
neuper@37939
|
243 |
then if not (is_complete_mod (pt, pos))
|
neuper@37906
|
244 |
then let val ptp = complete_mod (pt, pos)
|
neuper@37906
|
245 |
in if autoord auto < 3 then ("ok", c, ptp)
|
neuper@37906
|
246 |
else
|
neuper@37906
|
247 |
if not (is_complete_spec ptp)
|
neuper@37906
|
248 |
then let val ptp = complete_spec ptp
|
neuper@37906
|
249 |
in if autoord auto = 3 then ("ok", c, ptp)
|
neuper@37906
|
250 |
else all_solve auto c ptp
|
neuper@37906
|
251 |
end
|
neuper@37906
|
252 |
else if autoord auto = 3 then ("ok", c, ptp)
|
neuper@37906
|
253 |
else all_solve auto c ptp
|
neuper@37906
|
254 |
end
|
neuper@37906
|
255 |
else
|
neuper@37906
|
256 |
if not (is_complete_spec (pt,pos))
|
neuper@37906
|
257 |
then let val ptp = complete_spec (pt, pos)
|
neuper@37906
|
258 |
in if autoord auto = 3 then ("ok", c, ptp)
|
neuper@37906
|
259 |
else all_solve auto c ptp
|
neuper@37906
|
260 |
end
|
neuper@37906
|
261 |
else if autoord auto = 3 then ("ok", c, (pt, pos))
|
neuper@37906
|
262 |
else all_solve auto c (pt, pos)
|
neuper@37906
|
263 |
else complete_solve auto c (pt, pos);
|
neuper@37906
|
264 |
(* val pbl = get_obj g_pbl (fst ptp) [];
|
neuper@37906
|
265 |
val (oris,_,_) = get_obj g_origin (fst ptp) [];
|
neuper@37906
|
266 |
*)
|
neuper@37906
|
267 |
|
neuper@37906
|
268 |
|
neuper@37906
|
269 |
|
neuper@37906
|
270 |
|
neuper@37906
|
271 |
|
neuper@37906
|
272 |
(*.initialiye matching; before 'tryMatch' get the pblID to match with:
|
neuper@37906
|
273 |
if no pbl has been specified, take the init from origin.*)
|
neuper@37906
|
274 |
(*fun initmatch pt (pos as (p,_):pos') =
|
neuper@37906
|
275 |
let val PblObj {probl,origin=(os,(_,pI,_),_),spec=(dI',pI',mI'),...} =
|
neuper@37906
|
276 |
get_obj I pt p
|
neuper@37906
|
277 |
val pblID = if pI' = e_pblID
|
neuper@37906
|
278 |
then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
|
neuper@37906
|
279 |
takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
|
neuper@37906
|
280 |
else pI'
|
neuper@37906
|
281 |
val spec = (dI',pblID,mI')
|
neuper@37906
|
282 |
val {ppc,where_,prls,...} = get_pbt pblID
|
neuper@37906
|
283 |
val (model_ok, (pbl, pre)) =
|
neuper@38050
|
284 |
match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
|
neuper@37906
|
285 |
in ModSpec (ocalhd_complete pbl pre spec,
|
neuper@37906
|
286 |
Pbl, e_term, pbl, pre, spec) end;*)
|
neuper@37906
|
287 |
fun initcontext_pbl pt (pos as (p,_):pos') =
|
neuper@37906
|
288 |
let val PblObj {probl,origin=(os,(_,pI,_),hdl),spec=(dI',pI',mI'),...} =
|
neuper@37906
|
289 |
get_obj I pt p
|
neuper@37906
|
290 |
val pblID = if pI' = e_pblID
|
neuper@37906
|
291 |
then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
|
neuper@37906
|
292 |
takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
|
neuper@37906
|
293 |
else pI'
|
neuper@37906
|
294 |
val {ppc,where_,prls,...} = get_pbt pblID
|
neuper@37906
|
295 |
val (model_ok, (pbl, pre)) =
|
neuper@38050
|
296 |
match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
|
neuper@37906
|
297 |
in (model_ok, pblID, hdl, pbl, pre) end;
|
neuper@37906
|
298 |
|
neuper@37906
|
299 |
fun initcontext_met pt (pos as (p,_):pos') =
|
neuper@37906
|
300 |
let val PblObj {meth,origin=(os,(_,_,mI), _),spec=(_, _, mI'),...} =
|
neuper@37906
|
301 |
get_obj I pt p
|
neuper@37906
|
302 |
val metID = if mI' = e_metID
|
neuper@37906
|
303 |
then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
|
neuper@37906
|
304 |
takelast (2, mI) (*FIXME.WN051125 a hack, impl.^^^*)
|
neuper@37906
|
305 |
else mI'
|
neuper@37906
|
306 |
val {ppc,pre,prls,scr,...} = get_met metID
|
neuper@37906
|
307 |
val (model_ok, (pbl, pre)) =
|
neuper@38050
|
308 |
match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
|
neuper@37906
|
309 |
in (model_ok, metID, scr, pbl, pre) end;
|
neuper@37906
|
310 |
|
neuper@37906
|
311 |
(*.match the model of a problem at pos p
|
neuper@37906
|
312 |
with the model-pattern of the problem with pblID*)
|
neuper@37906
|
313 |
fun context_pbl pI pt (p:pos) =
|
neuper@37906
|
314 |
let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
|
neuper@37906
|
315 |
val {ppc,where_,prls,...} = get_pbt pI
|
neuper@37906
|
316 |
val (model_ok, (pbl, pre)) =
|
neuper@38050
|
317 |
match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
|
neuper@37906
|
318 |
in (model_ok, pI, hdl, pbl, pre) end;
|
neuper@37906
|
319 |
|
neuper@37906
|
320 |
fun context_met mI pt (p:pos) =
|
neuper@37906
|
321 |
let val PblObj {meth,origin=(os,_,hdl),...} = get_obj I pt p
|
neuper@37906
|
322 |
val {ppc,pre,prls,scr,...} = get_met mI
|
neuper@37906
|
323 |
val (model_ok, (pbl, pre)) =
|
neuper@38050
|
324 |
match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
|
neuper@37906
|
325 |
in (model_ok, mI, scr, pbl, pre) end
|
neuper@37906
|
326 |
|
neuper@37906
|
327 |
|
neuper@37906
|
328 |
(* val (pI, pt, pos as (p,_)) = (pblID, pt, p);
|
neuper@37906
|
329 |
*)
|
neuper@37906
|
330 |
fun tryrefine pI pt (pos as (p,_):pos') =
|
neuper@37906
|
331 |
let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
|
neuper@38050
|
332 |
in case refine_pbl (assoc_thy "Isac") pI probl of
|
neuper@37926
|
333 |
NONE => (*copy from context_pbl*)
|
neuper@37906
|
334 |
let val {ppc,where_,prls,...} = get_pbt pI
|
neuper@38050
|
335 |
val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac")
|
neuper@37906
|
336 |
probl (ppc,where_,prls) os
|
neuper@37906
|
337 |
in (false, pI, hdl, pbl, pre) end
|
neuper@37926
|
338 |
| SOME (pI, (pbl, pre)) =>
|
neuper@37906
|
339 |
(true, pI, hdl, pbl, pre)
|
neuper@37906
|
340 |
end;
|
neuper@37906
|
341 |
|
neuper@37906
|
342 |
(* val (pt, (pos as (p,p_):pos')) = (pt, ip);
|
neuper@37906
|
343 |
*)
|
neuper@37906
|
344 |
fun detailstep pt (pos as (p,p_):pos') =
|
neuper@37906
|
345 |
let val nd = get_nd pt p
|
neuper@37906
|
346 |
val cn = children nd
|
neuper@37906
|
347 |
in if null cn
|
neuper@37906
|
348 |
then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
|
neuper@37906
|
349 |
then detailrls pt pos
|
neuper@37906
|
350 |
else ("no-Rewrite_Set...", EmptyPtree, e_pos')
|
neuper@37906
|
351 |
else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*),
|
neuper@37906
|
352 |
(p @ [length (children (get_nd pt p))], Res) )
|
neuper@37906
|
353 |
end;
|
neuper@37906
|
354 |
|
neuper@37906
|
355 |
|
neuper@37906
|
356 |
|
neuper@37906
|
357 |
(***. for mathematics authoring on sml-toplevel; no XML .***)
|
neuper@37906
|
358 |
|
neuper@37906
|
359 |
type NEW = int list;
|
neuper@37906
|
360 |
(* val sp = (dI',pI',mI');
|
neuper@37906
|
361 |
*)
|
neuper@37906
|
362 |
|
neuper@37906
|
363 |
(*15.8.03 for me with loc_specify/solve, nxt_specify/solve
|
neuper@37906
|
364 |
delete as soon as TESTg_form -> _mout_ dropped*)
|
neuper@37906
|
365 |
fun TESTg_form ptp =
|
neuper@37906
|
366 |
(* val ptp = (pt,p);
|
neuper@37906
|
367 |
*)
|
neuper@37906
|
368 |
let val (form,_,_) = pt_extract ptp
|
neuper@37906
|
369 |
in case form of
|
neuper@37906
|
370 |
Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
|
neuper@37906
|
371 |
| ModSpec (_,p_, head, gfr, pre, _) =>
|
neuper@37906
|
372 |
Form' (PpcKF (0,EdUndef,0,Nundef,
|
neuper@37906
|
373 |
(case p_ of Pbl => Problem[] | Met => Method[],
|
neuper@38050
|
374 |
itms2itemppc (assoc_thy"Isac") gfr pre)))
|
neuper@37906
|
375 |
end;
|
neuper@37906
|
376 |
|
neuper@37906
|
377 |
(*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;
|
neuper@37906
|
378 |
compare "fun CalcTree" which DOES decode.*)
|
neuper@37906
|
379 |
fun CalcTreeTEST [(fmz, sp):fmz] =
|
neuper@37906
|
380 |
(* val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
381 |
val [(fmz, sp):fmz] = [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
|
neuper@37906
|
382 |
*)
|
neuper@37906
|
383 |
let val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
|
neuper@37906
|
384 |
val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
|
neuper@37906
|
385 |
val f = TESTg_form (pt,p)
|
neuper@37906
|
386 |
in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end;
|
neuper@37906
|
387 |
|
neuper@37906
|
388 |
(*for tests > 15.8.03 after separation setnexttactic / nextTac:
|
neuper@37906
|
389 |
external view: me should be used by math-authors as done so far
|
neuper@37906
|
390 |
internal view: loc_specify/solve, nxt_specify/solve used
|
neuper@37906
|
391 |
i.e. same as in setnexttactic / nextTac*)
|
neuper@37906
|
392 |
(*ENDE TESTPHASE 08/10.03:
|
neuper@37906
|
393 |
NEW loeschen, eigene Version von locatetac, step
|
neuper@37906
|
394 |
meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
|
neuper@37906
|
395 |
|
neuper@37906
|
396 |
fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
|
neuper@41972
|
397 |
let
|
neuper@41972
|
398 |
val (pt, p) =
|
neuper@41972
|
399 |
(*locatetac is here for testing by me; step would suffice in me*)
|
neuper@37906
|
400 |
case locatetac tac (pt,p) of
|
neuper@41972
|
401 |
("ok", (_, _, ptp)) => ptp
|
neuper@41972
|
402 |
| ("unsafe-ok", (_, _, ptp)) => ptp
|
neuper@41972
|
403 |
| ("not-applicable",_) => (pt, p)
|
neuper@41972
|
404 |
| ("end-of-calculation", (_, _, ptp)) => ptp
|
neuper@41972
|
405 |
| ("failure",_) => error "sys-error";
|
neuper@41972
|
406 |
val (_, ts) = (*WN101102 NOT tested, if step would create _same_ ptp*)
|
neuper@37906
|
407 |
(case step p ((pt, e_pos'),[]) of
|
neuper@41972
|
408 |
("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
|
neuper@41972
|
409 |
| ("helpless",_) => ("helpless: cannot propose tac", [])
|
neuper@41972
|
410 |
| ("no-fmz-spec",_) => error "no-fmz-spec"
|
neuper@41972
|
411 |
| ("end-of-calculation", (ts, _, _)) => ("",ts))
|
neuper@38031
|
412 |
handle _ => error "sys-error";
|
neuper@41972
|
413 |
val tac =
|
neuper@41972
|
414 |
case ts of
|
neuper@41972
|
415 |
tacis as (_::_) => let val (tac,_,_) = last_elem tacis in tac end
|
neuper@41972
|
416 |
| _ => if p = ([],Res) then End_Proof' else Empty_Tac;
|
neuper@37906
|
417 |
(*form output comes from locatetac*)
|
neuper@41972
|
418 |
in (p:pos', []:NEW, TESTg_form (pt, p),
|
neuper@41972
|
419 |
(tac2IDstr tac, tac):tac'_, Sundef, pt) end;
|
neuper@37906
|
420 |
|
neuper@37906
|
421 |
(*for quick test-print-out, until 'type inout' is removed*)
|
neuper@37906
|
422 |
fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
|
neuper@37906
|
423 |
|
neuper@37906
|
424 |
|
neuper@37906
|
425 |
|
neuper@37906
|
426 |
(*------------------------------------------------------------------(**)
|
neuper@37906
|
427 |
end
|
neuper@37906
|
428 |
open MathEngine;
|
neuper@37906
|
429 |
(**)------------------------------------------------------------------*)
|
neuper@37906
|
430 |
|