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