|
1 (* use"../ME/solve.sml"; |
|
2 use"ME/solve.sml"; |
|
3 use"solve.sml"; |
|
4 W.N.10.12.99 |
|
5 |
|
6 cd ~/Isabelle/Zerlege-Isa98-1/src/HOL/ |
|
7 /src/HOL> sml @SMLload=HOL-plus |
|
8 cd"~/MathEngine99/src/"; |
|
9 use"ROOT.sml"; |
|
10 *) |
|
11 |
|
12 fun safe (ScrState (_,_,_,_,s,_)) = s |
|
13 | safe (RrlsState _) = Safe; |
|
14 |
|
15 type mstID = string; |
|
16 type mstep_ = mstID * mstep; (*DG <-> ME*) |
|
17 val e_mstep_ = ("Empty_Mstep", Empty_Mstep):mstep_; |
|
18 |
|
19 fun mk_mstep_ m = case m of |
|
20 Init_Proof (ppc, spec) => ("Init_Proof", Init_Proof (ppc, spec )) |
|
21 | Model_Problem pblID => ("Model_Problem", Model_Problem pblID) |
|
22 | Refine_Tacitly pblID => ("Refine_Tacitly", Refine_Tacitly pblID) |
|
23 | Refine_Problem pblID => ("Refine_Problem", Refine_Problem pblID) |
|
24 | Add_Given cterm' => ("Add_Given", Add_Given cterm') |
|
25 | Del_Given cterm' => ("Del_Given", Del_Given cterm') |
|
26 | Add_Find cterm' => ("Add_Find", Add_Find cterm') |
|
27 | Del_Find cterm' => ("Del_Find", Del_Find cterm') |
|
28 | Add_Relation cterm' => ("Add_Relation", Add_Relation cterm') |
|
29 | Del_Relation cterm' => ("Del_Relation", Del_Relation cterm') |
|
30 |
|
31 | Specify_Domain domID => ("Specify_Domain", Specify_Domain domID) |
|
32 | Specify_Problem pblID => ("Specify_Problem", Specify_Problem pblID) |
|
33 | Specify_Method metID => ("Specify_Method", Specify_Method metID) |
|
34 | Apply_Method metID => ("Apply_Method", Apply_Method metID) |
|
35 | Check_Postcond pblID => ("Check_Postcond", Check_Postcond pblID) |
|
36 | Free_Solve => ("Free_Solve",Free_Solve) |
|
37 |
|
38 | Rewrite_Inst (subs, thm') => ("Rewrite_Inst", Rewrite_Inst (subs, thm')) |
|
39 | Rewrite thm' => ("Rewrite", Rewrite thm') |
|
40 | Rewrite_Asm thm' => ("Rewrite_Asm", Rewrite_Asm thm') |
|
41 | Rewrite_Set_Inst (subs, rls') |
|
42 => ("Rewrite_Set_Inst", Rewrite_Set_Inst (subs, rls')) |
|
43 | Rewrite_Set rls' => ("Rewrite_Set", Rewrite_Set rls') |
|
44 | End_Ruleset => ("End_Ruleset", End_Ruleset) |
|
45 |
|
46 | End_Detail => ("End_Detail", End_Detail) |
|
47 | Detail_Set rls' => ("Detail_Set", Detail_Set rls') |
|
48 | Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Detail_Set_Inst (s, rls')) |
|
49 |
|
50 | Calculate op_ => ("Calculate", Calculate op_) |
|
51 | Substitute subs => ("Substitute", Substitute subs) |
|
52 | Apply_Assumption cts' => ("Apply_Assumption", Apply_Assumption cts') |
|
53 |
|
54 | Take cterm' => ("Take", Take cterm') |
|
55 | Take_Inst cterm' => ("Take_Inst", Take_Inst cterm') |
|
56 | Group (con, ints) => ("Group", Group (con, ints)) |
|
57 | Subproblem (domID, pblID) => ("Subproblem", Subproblem (domID, pblID)) |
|
58 (* |
|
59 | Subproblem_Full(spec,cts')=> ("Subproblem_Full", Subproblem_Full(spec,cts')) |
|
60 *) |
|
61 | End_Subproblem => ("End_Subproblem",End_Subproblem) |
|
62 | CAScmd cterm' => ("CAScmd", CAScmd cterm') |
|
63 |
|
64 | Split_And => ("Split_And", Split_And) |
|
65 | Conclude_And => ("Conclude_And", Conclude_And) |
|
66 | Split_Or => ("Split_Or", Split_Or) |
|
67 | Conclude_Or => ("Conclude_Or", Conclude_Or) |
|
68 | Begin_Trans => ("Begin_Trans", Begin_Trans) |
|
69 | End_Trans => ("End_Trans", End_Trans) |
|
70 | Begin_Sequ => ("Begin_Sequ", Begin_Sequ) |
|
71 | End_Sequ => ("End_Sequ", Begin_Sequ) |
|
72 | Split_Intersect => ("Split_Intersect", Split_Intersect) |
|
73 | End_Intersect => ("End_Intersect", End_Intersect) |
|
74 | Check_elementwise cterm' => ("Check_elementwise", Check_elementwise cterm') |
|
75 | Or_to_List => ("Or_to_List", Or_to_List) |
|
76 | Collect_Trues => ("Collect_Results", Collect_Trues) |
|
77 |
|
78 | Empty_Mstep => ("Empty_Mstep",Empty_Mstep) |
|
79 | Mstep string => ("Mstep",Mstep string) |
|
80 | User => ("User",User) |
|
81 | End_Proof' => ("End_Proof'",End_Proof'); |
|
82 |
|
83 (*Detail*) |
|
84 val empty_mstep_ = (mk_mstep_ Empty_Mstep):mstep_; |
|
85 |
|
86 fun mk_mstep ((_,m):mstep_) = m; |
|
87 fun mk_mstID ((mI,_):mstep_) = mI; |
|
88 |
|
89 fun mstep_2str ((ID,ms):mstep_) = ID ^ (mstep2str ms); |
|
90 (* TODO: mstep2str, mstep_2str NOT tested *) |
|
91 |
|
92 |
|
93 |
|
94 type squ = ptree; (* TODO: safe etc. *) |
|
95 |
|
96 (*13.9.02-------------- |
|
97 type ctr = (loc * pos) list; |
|
98 val ops = [("plus","op +"),("minus","op -"),("times","op *"), |
|
99 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")]; |
|
100 fun op_intern op_ = |
|
101 case assoc (ops,op_) of |
|
102 Some op' => op' | None => raise error ("op_intern: no op= "^op_); |
|
103 -----------------------*) |
|
104 |
|
105 |
|
106 |
|
107 (* use"ME/solve.sml"; |
|
108 use"solve.sml"; |
|
109 |
|
110 val ttt = (term_of o the o (parse thy))"Substitute [(bdv,x)] g"; |
|
111 val ttt = (term_of o the o (parse thy))"Rewrite thmid True g"; |
|
112 |
|
113 Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f' |
|
114 *) |
|
115 |
|
116 |
|
117 |
|
118 val specsteps = ["Init_Proof","Refine_Tacitly","Refine_Problem", |
|
119 "Model_Problem",(*"Match_Problem",*) |
|
120 "Add_Given","Del_Given","Add_Find","Del_Find", |
|
121 "Add_Relation","Del_Relation", |
|
122 "Specify_Domain","Specify_Problem","Specify_Method"]; |
|
123 |
|
124 |
|
125 fun solve ("Apply_Method",Apply_Method' mI) ((p,_):pos') (pt:ptree) = |
|
126 (* val ("Apply_Method",Apply_Method' mI)=(mI,m); |
|
127 *) |
|
128 let val {srls,...} = get_met mI; |
|
129 val PblObj{meth=itms,...} = get_obj I pt p; |
|
130 val thy' = get_obj g_domID pt p; |
|
131 val thy = assoc_thy thy'; |
|
132 val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI; |
|
133 val ini = init_form thy scr env; |
|
134 val (p,p_) = (lev_dn p,Res); |
|
135 in |
|
136 case ini of |
|
137 Some t => (* val Some t = ini; |
|
138 *) |
|
139 let val (p,p_) = (lev_on p,Frm); (*implicit Take*) |
|
140 val f = Sign.string_of_term (sign_of (assoc_thy thy')) t; |
|
141 val (pt,ps) = cappend_form pt p is f |
|
142 val {srls,...} = get_met mI; |
|
143 in ((p,p_), [], Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), |
|
144 fst (next_tac (thy',srls) (pt,(p,p_)) scr is), Safe, pt) end |
|
145 | None => |
|
146 let val (m,_) = next_tac (thy',srls) (pt,(lev_on p,Frm)) scr is |
|
147 val f = case m of |
|
148 Subproblem (domID, pblID) => |
|
149 Form' (FormKF (~1,EdUndef,(length p), Nundef, |
|
150 (Sign.string_of_term (sign_of (assoc_thy thy')) |
|
151 (subpbl domID pblID)))) |
|
152 | _ => EmptyMout |
|
153 (*nothing written to pt !!!*) |
|
154 in ((p,p_), [], f, m, Safe, pt) end |
|
155 end |
|
156 |
|
157 | solve ("Free_Solve", Free_Solve') (p,_) pt = |
|
158 let val _=writeln"###solve Free_Solve"; |
|
159 val p' = lev_dn_ (p,Res); |
|
160 val pt = update_metID pt (par_pblobj pt p) e_metID; |
|
161 in (p', [], EmptyMout, Empty_Mstep, Unsafe, pt) end |
|
162 |
|
163 (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m); |
|
164 *) |
|
165 | solve ("Check_Postcond",Check_Postcond' (pI,_)) (p,p_) pt = |
|
166 let (*val _=writeln"###solve Check_Postcond";*) |
|
167 val pp = par_pblobj pt p; |
|
168 val metID = get_obj g_metID pt pp; |
|
169 val {srls=srls,scr=sc,...} = get_met metID; |
|
170 val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); |
|
171 (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_))); |
|
172 val _= writeln("### solve Check_postc, is= "^(istate2str is));*) |
|
173 val thy' = get_obj g_domID pt pp; |
|
174 val thy = assoc_thy thy'; |
|
175 val (_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is; |
|
176 (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*) |
|
177 in if pp = [] then |
|
178 let val ((p,p_),ps,f,pt) = generate1 thy (Check_Postcond'(pI,scval)) |
|
179 (ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt; |
|
180 in ((p,p_), ps, f, End_Proof', scsaf, pt) end |
|
181 else |
|
182 let |
|
183 (*resume script of parpbl, transfer value of subpbl-script*) |
|
184 val ppp = par_pblobj pt ((**)lev_up(**) p); |
|
185 val thy' = get_obj g_domID pt ppp; |
|
186 val thy = assoc_thy thy'; |
|
187 val metID = get_obj g_metID pt ppp; |
|
188 val sc = (#scr o get_met) metID; |
|
189 val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm); |
|
190 (*val _=writeln("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm))); |
|
191 val _=writeln("### solve Check_postc, is(pt)= "^(istate2str is)); |
|
192 val _=writeln("### solve Check_postc, is'= "^ |
|
193 (istate2str (E,l,a,scval,scsaf,b)));*) |
|
194 val ((p,p_),ps,f,pt) = generate1 thy (Check_Postcond'(pI,scval)) |
|
195 (ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt; |
|
196 (*val _=writeln("### solve Check_postc, is(pt')= "^ |
|
197 (istate2str (get_istate pt ([3],Res))));*) |
|
198 val (nxt,_) = next_tac (thy',srls) (pt,(p,p_)) sc |
|
199 (ScrState (E,l,a,scval,scsaf,b)); |
|
200 in ((p,p_), ps, f, nxt, scsaf, pt) end |
|
201 end |
|
202 (* writeln(istate2str(get_istate pt (p,p_))); |
|
203 *) |
|
204 |
|
205 | solve (_,End_Proof'') (p,p_) pt = |
|
206 ((p,p_), [], EmptyMout, Empty_Mstep, Safe, pt) |
|
207 |
|
208 (*.start interpreter and do one rewrite.*) |
|
209 (* val (_,Detail_Set'(thy',rls',t)) = (mI,m); val p = (p,p_); |
|
210 solve ("",Detail_Set'(thy', rls',t)) p pt; |
|
211 *) |
|
212 | solve (_,Detail_Set'(thy', rls(*'*),t)) p pt = |
|
213 let (*val rls = the (assoc(!ruleset',rls')) |
|
214 handle _ => raise error ("solve: '"^rls'^"' not known");*) |
|
215 val thy = assoc_thy thy'; |
|
216 val (srls, sc, is) = |
|
217 case rls of |
|
218 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => |
|
219 (e_rls, sc, RrlsState (ii t)) |
|
220 | Rls {srls=srls,scr=sc as Script s,...} => |
|
221 (srls, sc, ScrState ([(one_scr_arg s,t)], [], |
|
222 None, e_term, Sundef, true)); |
|
223 val pt = update_mstep pt (fst p) (Detail_Set (id_rls rls)); |
|
224 val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt; |
|
225 val (nx,_) = next_tac (thy',srls) (pt,p) sc is; |
|
226 val aopt = applicable_in p pt nx; |
|
227 in case aopt of |
|
228 Notappl s => raise error ("solve Detail_Set: "^s) |
|
229 (* val Appl m = aopt; |
|
230 *) |
|
231 | Appl m => solve ("discardFIXME",m) p pt end |
|
232 |
|
233 | solve (_,End_Detail' t) (p,p_) pt = |
|
234 let val pr as (p',_) = (lev_up p, Res) |
|
235 val pp = par_pblobj pt p |
|
236 val r = get_obj g_result pt p' (*Rewrite_Set* done at Detail_Set**) |
|
237 val thy' = get_obj g_domID pt pp |
|
238 val (srls, is, sc) = from_pblobj' thy' pr pt |
|
239 in (pr, [], Form' (FormKF (~1, EdUndef, length p', Nundef, r)), |
|
240 fst (next_tac (thy',srls) (pt,pr) sc is), Sundef, pt) end |
|
241 (* val (mI,(p,p_)) = ("xxx",p); |
|
242 *) |
|
243 | solve (mI,m) (p,p_) pt = |
|
244 if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02: |
|
245 could be detail, too !!*) |
|
246 then let val ((p,p_),ps,f,pt) = |
|
247 generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) |
|
248 m e_istate (p,p_) pt; |
|
249 in ((p,p_),ps,f, Empty_Mstep, Unsafe, pt) end |
|
250 else |
|
251 let val thy' = get_obj g_domID pt (par_pblobj pt p); |
|
252 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
|
253 (*val _= writeln("### solve, before locate_gen p="^(pos'2str(p,p_)));*) |
|
254 val d = e_rls; (*FIXME: canon.simplifier for domain is missing |
|
255 8.01: generate from domID?*) |
|
256 in case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of |
|
257 Steps (is', (m',f',pt',p',c')::ss) => |
|
258 (* val Steps (is', (m',f',pt',p',c')::ss) = |
|
259 locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is; |
|
260 *) |
|
261 let val nxt = |
|
262 case p' of (*change from solve to model subprobl*) |
|
263 (_,Pbl) => nxt_model_pbl m' |
|
264 | _ => fst (next_tac (thy',srls) (pt',p') sc is'); |
|
265 (*27.8.02: next_tac may change to other branches in ptFIXXXXME*) |
|
266 in (p',c', f', nxt, safe is', pt'(*'*)) end |
|
267 | NotLocatable => |
|
268 let val (p,ps,f,pt) = |
|
269 generate_hard (assoc_thy "Isac.thy") m (p,p_) pt; |
|
270 in (p,ps,f, Empty_Mstep, Unsafe, pt) end |
|
271 end; |
|
272 |
|
273 |
|
274 (* unused: _____ 4.4.00 TODO: pos list !!!*) |
|
275 fun me ((mI,m):mstep_) (pos' as (p,p_):pos') (c:cid) (pt:ptree) = |
|
276 (* val (pos' as (p,p_),pt) = (p,EmptyPtree); |
|
277 |
|
278 val (mI,m) = nxt; val pos' as (p,p_) = p; |
|
279 *) |
|
280 case applicable_in (p,p_) pt m of |
|
281 Appl m => (* val Appl m = applicable_in (p,p_) pt m; |
|
282 *) |
|
283 (case m of |
|
284 ( Refine_Problem' ms) => |
|
285 (pos',c, Problems (RefinedKF ms), |
|
286 ("Specify_Problem", Specify_Problem (refined ms)), Safe, pt) |
|
287 |
|
288 | _ => (if mI mem specsteps |
|
289 then let val (p',c,f,m,s,pt) = specify m (p,p_) c pt; |
|
290 in (p',c,f,mk_mstep_ m,s,pt) |
|
291 end |
|
292 else let val ((p,p_),c,f,m,s,pt) = solve (mI,m) (p,p_) pt; |
|
293 in ((p,p_),c,f,mk_mstep_ m,s,pt) end)) |
|
294 | Notappl e => ((p,p_),c, Error' (Error_ e), |
|
295 mk_mstep_ Empty_Mstep (*nxtstep ??*), Unsafe,pt); |
|
296 |
|
297 (* val(mI,m)=m;val ppp=p;(*!!!*)val(p,p_)=pos;val(_,pt,_)=ppp(*!!!*); |
|
298 get_form ((mI,m):mstep_) ((p,p_):pos') ppp; |
|
299 *) |
|
300 fun get_form ((mI,m):mstep_) ((p,p_):pos') pt = |
|
301 case applicable_in (p,p_) pt m of |
|
302 Notappl e => Error' (Error_ e) |
|
303 | Appl m => |
|
304 (* val Appl m=applicable_in (p,p_) pt m; |
|
305 *) |
|
306 if mI mem specsteps |
|
307 then let val (_,_,f,_,_,_) = specify m (p,p_) [] pt |
|
308 in f end |
|
309 else let val (_,_,f,_,_,_) = solve (mI,m) (p,p_) pt |
|
310 in f end; |
|
311 |
|
312 |
|
313 (* use"ME/solve.sml"; |
|
314 use"solve.sml"; |
|
315 *) |
|
316 |