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