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