1 (* Title: solve an example by interpreting a method's script
2 Author: Walther Neuper 1999
3 (c) copyright due to lincense terms.
4 1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80 90 100
12 fun safe (ScrState (_,_,_,_,s,_)) = s
13 | safe (RrlsState _) = Safe;
16 type tac'_ = mstID * tac; (*DG <-> ME*)
17 val e_tac'_ = ("Empty_Tac", Empty_Tac):tac'_;
19 fun mk_tac'_ m = case m of
20 Init_Proof (ppc, spec) => ("Init_Proof", Init_Proof (ppc, spec ))
21 | Model_Problem => ("Model_Problem", Model_Problem)
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')
31 | Specify_Theory domID => ("Specify_Theory", Specify_Theory 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)
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)
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'))
50 | Calculate op_ => ("Calculate", Calculate op_)
51 | Substitute sube => ("Substitute", Substitute sube)
52 | Apply_Assumption cts' => ("Apply_Assumption", Apply_Assumption cts')
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))
59 | Subproblem_Full(spec,cts')=> ("Subproblem_Full", Subproblem_Full(spec,cts'))
61 | End_Subproblem => ("End_Subproblem",End_Subproblem)
62 | CAScmd cterm' => ("CAScmd", CAScmd cterm')
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)
78 | Empty_Tac => ("Empty_Tac",Empty_Tac)
79 | Tac string => ("Tac",Tac string)
80 | End_Proof' => ("End_Proof'",End_Proof');
83 val empty_tac'_ = (mk_tac'_ Empty_Tac):tac'_;
85 fun mk_tac ((_,m):tac'_) = m;
86 fun mk_mstID ((mI,_):tac'_) = mI;
88 fun tac'_2str ((ID,ms):tac'_) = ID ^ (tac2str ms);
89 (* TODO: tac2str, tac'_2str NOT tested *)
93 type squ = ctree; (* TODO: safe etc. *)
95 (*13.9.02--------------
96 type ctr = (loc * pos) list;
97 val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","Groups.times_class.times"),
98 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];
100 @{term "PLUS"}; (*Free ("PLUS", "'a") : term*)
101 @{term "plus"}; (*Const ("Groups.plus_class.plus", "'a => 'a => 'a")*)
102 @{term "MINUS"}; (*Free ("MINUS", "'a")*)
103 @{term "minus"}; (*Const ("Groups.minus_class.minus", "'a => 'a => 'a")*)
104 @{term "TIMES"}; (*Free ("TIMES", "'a")*)
105 @{term "times"}; (*Const ("Groups.times_class.times", "'a => 'a => 'a")*)
106 @{term "CANCEL"}; (*Free ("CANCEL", "'a")*)
107 @{term "cancel"}; (*Free ("cancel", "'a")*)
108 @{term "POWER"}; (*Free ("POWER", "'a")*)
109 @{term "pow"}; (*Free ("pow", "'a")*)
110 @{term "SQRT"}; (*Free ("SQRT", "'a")*)
111 @{term "sqrt"}; (*Const ("NthRoot.sqrt", "RealDef.real => RealDef.real")*)
114 case assoc (ops, op_) of
115 SOME op' => op' | NONE => error ("op_intern: no op= "^op_);
116 -----------------------*)
120 (* use"ME/solve.sml";
123 val ttt = (Thm.term_of o the o (parse thy))"Substitute [(bdv,x)] g";
124 val ttt = (Thm.term_of o the o (parse thy))"Rewrite thmid True g";
126 Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f'
131 val specsteps = ["Init_Proof","Refine_Tacitly","Refine_Problem",
132 "Model_Problem",(*"Match_Problem",*)
133 "Add_Given","Del_Given","Add_Find","Del_Find",
134 "Add_Relation","Del_Relation",
135 "Specify_Theory","Specify_Problem","Specify_Method"];
139 fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)
140 (Lucin.tac_2tac tac_, tac_, (p, Ctree.get_loc pt p)): Generate.taci;
143 (*FIXME.WN050821 compare solve ... nxt_solv*)
144 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
145 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
147 fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ctree, (pos as (p,_))) =
148 let val {srls, ...} = Specify.get_met mI;
149 val PblObj {meth=itms, ...} = get_obj I pt p;
150 val thy' = get_obj g_domID pt p;
151 val thy = assoc_thy thy';
152 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = Lucin.init_scrstate thy itms mI;
153 val ini = Lucin.init_form thy sc env;
158 let val (pos,c,_,pt) =
159 Generate.generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
160 (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
161 in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
162 ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)) : Chead.calcstate')
164 | NONE => (*execute the first tac in the Script, compare solve m*)
166 val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
167 val d = e_rls (*FIXME: get simplifier from domID*);
169 case Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of
170 Lucin.Steps (is'', ss as (m'',f',pt',p',c')::_) =>
171 ("ok", (map step2taci ss, c', (pt',p')))
173 let val (p,ps,f,pt) = Generate.generate_hard (assoc_thy "Isac") m (p,Frm) pt;
175 ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p)))
180 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) =
181 let (*val _=tracing"###solve Free_Solve";*)
182 val p' = lev_dn_ (p,Res);
183 val pt = update_metID pt (par_pblobj pt p) e_metID;
184 in ("ok", ([(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p')))
187 | solve ("Check_Postcond", Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
189 val pp = par_pblobj pt p
191 (case get_obj g_tac pt p of
192 Check_elementwise _ => (*collects and instantiates asms*)
193 (snd o (get_obj g_result pt)) p
194 | _ => get_assumptions_ pt (p,p_))
195 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
196 val metID = get_obj g_metID pt pp;
197 val {srls=srls,scr=sc,...} = Specify.get_met metID;
198 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
199 val thy' = get_obj g_domID pt pp;
200 val thy = assoc_thy thy';
201 val (_,_,(scval,scsaf)) = Lucin.next_tac (thy',srls) (pt,(p,p_)) sc loc;
206 val is = ScrState (E,l,a,scval,scsaf,b)
207 val tac_ = Check_Postcond' (pI, (scval, asm))
208 val (pos,ps,f,pt) = Generate.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
209 in ("ok", ([(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
211 let (*resume script of parpbl, transfer value of subpbl-script*)
212 val ppp = par_pblobj pt (lev_up p);
213 val thy' = get_obj g_domID pt ppp;
214 val thy = assoc_thy thy';
215 val metID = get_obj g_metID pt ppp;
216 val sc = (#scr o Specify.get_met) metID;
217 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm);
218 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
219 val ((p,p_),ps,f,pt) =
220 Generate.generate1 thy (Check_Postcond' (pI, (scval, asm)))
221 (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
222 in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, asm)),
223 ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
227 | solve (_,End_Proof'') (pt, (p,p_)) =
229 ([(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_))))
231 (*-----------vvvvvvvvvvv could be done by generate1 ?!?*)
232 | solve (_,End_Detail' t) (pt, (p,p_)) =
234 val pr as (p',_) = (lev_up p, Res)
235 val pp = par_pblobj pt p
236 val r = (fst o (get_obj g_result pt)) p'
237 (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)
238 val thy' = get_obj g_domID pt pp
239 val (srls, is, sc) = Lucin.from_pblobj' thy' pr pt
240 val (tac_,is',_) = Lucin.next_tac (thy',srls) (pt,pr) sc is
241 in ("ok", ([(End_Detail, End_Detail' t ,
242 ((p,p_), get_loc pt (p,p_)))], [], (pt,pr)))
245 | solve (mI,m) (pt, po as (p,p_)) =
246 if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02: could be detail, too !!*)
249 val ctxt = get_ctxt pt po
250 val ((p,p_),ps,f,pt) =
251 Generate.generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
252 m (e_istate, ctxt) (p,p_) pt;
253 in ("no-method-specified", (*Free_Solve*)
254 ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, ctxt)))], ps, (pt,(p,p_))))
258 val thy' = get_obj g_domID pt (par_pblobj pt p);
259 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
260 val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
262 case Lucin.locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
263 Lucin.Steps (is', ss as (m',f',pt',p',c')::_) =>
265 (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
266 in ("ok", (map step2taci ss, c', (pt',p'))) end
268 let val (p,ps,f,pt) =
269 Generate.generate_hard (assoc_thy "Isac") m (p,p_) pt;
270 in ("not-found-in-script",
271 ([(Lucin.tac_2tac m, m, (po,is))], ps, (pt,p)))
275 (*FIXME.WN050821 compare fun solve ... fun nxt_solv*)
276 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
277 fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ctree, pos as (p,_)) =
279 val {srls,ppc,...} = Specify.get_met mI;
280 val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p;
281 val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
282 val thy' = get_obj g_domID pt p;
283 val thy = assoc_thy thy';
284 val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = Lucin.init_scrstate thy itms mI;
285 val ini = Lucin.init_form thy scr env;
290 val pos = ((lev_on o lev_dn) p, Frm)
291 val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
292 val (pos,c,_,pt) = (*implicit Take*)
293 Generate.generate1 thy tac_ (is, ctxt) pos pt
294 in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)) : Chead.calcstate' end
297 val pt = update_env pt (fst pos) (SOME (is, ctxt))
298 val (tacis, c, ptp) = nxt_solve_ (pt, pos)
300 [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, ctxt), (pos, (is, ctxt)))],
305 (*TODO.WN050913 remove unnecessary code below*)
306 | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_)) =
308 val pp = par_pblobj pt p
310 (case get_obj g_tac pt p of
311 Check_elementwise _ => (*collects and instantiates asms*)
312 (snd o (get_obj g_result pt)) p
313 | _ => get_assumptions_ pt (p,p_))
314 handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
315 val metID = get_obj g_metID pt pp;
316 val {srls=srls,scr=sc,...} = Specify.get_met metID;
317 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
318 val thy' = get_obj g_domID pt pp;
319 val thy = assoc_thy thy';
320 val (_,_,(scval,scsaf)) = Lucin.next_tac (thy',srls) (pt,(p,p_)) sc loc;
325 val is = ScrState (E,l,a,scval,scsaf,b)
326 val tac_ = Check_Postcond'(pI,(scval, asm))
327 val ((p,p_),ps,f,pt) =
328 Generate.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
329 in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
331 let (*resume script of parpbl, transfer value of subpbl-script*)
332 val ppp = par_pblobj pt (lev_up p);
333 val thy' = get_obj g_domID pt ppp;
334 val thy = assoc_thy thy';
335 val metID = get_obj g_metID pt ppp;
336 val {scr,...} = Specify.get_met metID;
337 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
338 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
339 val tac_ = Check_Postcond' (pI, (scval, asm))
340 val is = ScrState (E,l,a,scval,scsaf,b)
341 val ((p,p_),ps,f,pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
342 in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
345 | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)
347 | nxt_solv tac_ is (pt, pos as (p,p_)) =
351 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
352 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
354 val (pos',c,_,pt) = Generate.generate1 (assoc_thy "Isac") tac_ is pos pt;
355 in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
357 (* find the next tac from the script, nxt_solv will update the ctree *)
358 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
359 if e_metID = get_obj g_metID pt (par_pblobj pt p)
360 then ([], [], (pt, (p, p_))) : Chead.calcstate'
363 val thy' = get_obj g_domID pt (par_pblobj pt p);
364 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
365 val (tac_,is,(t,_)) = Lucin.next_tac (thy',srls) (pt,pos) sc is;
366 (*TODO here ^^^ return finished/helpless/ok !*)
368 End_Detail' _ => ([(End_Detail, End_Detail' (t,[(*FIXME.040215*)]),
369 (pos, is))], [], (pt, pos))
370 | _ => nxt_solv tac_ is ptp end;
372 (* says how may steps of a calculation should be done by "fun autocalc" *)
373 (*FIXXXME040624: does NOT match interfaces/ITOCalc.java
374 TODO.WN0512 redesign togehter with autocalc ?*)
376 Step of int (*1 do #int steps (may stop in model/specify)
377 IS VERY INEFFICIENT IN MODEL/SPECIY *)
378 | CompleteModel (*2 complete modeling
379 if model complete, finish specifying *)
380 | CompleteCalcHead (*3 complete model/specify in one go *)
381 | CompleteToSubpbl (*4 stop at the next begin of a subproblem,
382 if none, complete the actual (sub)problem *)
383 | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems) *)
384 | CompleteCalc; (*6 complete the calculation as a whole *)
386 fun autoord (Step _ ) = 1
387 | autoord CompleteModel = 2
388 | autoord CompleteCalcHead = 3
389 | autoord CompleteToSubpbl = 4
390 | autoord CompleteSubpbl = 5
391 | autoord CompleteCalc = 6;
393 fun complete_solve auto c (ptp as (_, p as (_,p_)): ctree * pos') =
395 then ("end-of-calculation", [], ptp)
397 if member op = [Pbl,Met] p_
400 val ptp = Chead.all_modspec ptp
401 val (_, c', ptp) = all_solve auto c ptp
402 in complete_solve auto (c @ c') ptp end
404 case nxt_solve_ ptp of
405 ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
407 then ("ok", c @ c', ptp)
410 val ptp = Chead.all_modspec ptp'
411 val (_, c'', ptp) = all_solve auto (c @ c') ptp
412 in complete_solve auto (c @ c'@ c'') ptp end
413 | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
414 if autoord auto < 6 orelse p' = ([],Res)
415 then ("ok", c @ c', ptp')
416 else complete_solve auto (c @ c') ptp'
417 | ((End_Detail, _, _)::_, c', ptp') =>
419 then ("ok", c @ c', ptp')
420 else complete_solve auto (c @ c') ptp'
421 | (_, c', ptp') => complete_solve auto (c @ c') ptp'
423 and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') =
425 val (_,_,mI) = get_obj g_spec pt p
426 val ctxt = get_ctxt pt pos
427 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp
428 in complete_solve auto (c @ c') ptp end;
430 (* aux.fun for detailrls with Rrls, reverse rewriting *)
431 fun rul_terms_2nds _ nds t [] = nds
432 | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
433 (append_atomic [] (e_istate, e_ctxt) t (rule2tac thy [] rule) res Complete EmptyPtree) ::
434 (rul_terms_2nds thy nds t' rts);
436 (* detail steps done internally by Rewrite_Set* into ctree by use of a script *)
437 fun detailrls pt (pos as (p,p_):pos') =
439 val t = get_obj g_form pt p
440 val tac = get_obj g_tac pt p
441 val rls = (assoc_rls o rls_of) tac
442 val ctxt = get_ctxt pt pos
445 Rrls {scr = Rfuns {init_state,...},...} =>
447 val (_,_,_,rul_terms) = init_state t
448 val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms
449 val pt''' = ins_chn newnds pt p
450 in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
453 val is = Generate.init_istate tac t
454 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
455 is wrong for simpl, but working ?!? *)
456 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
457 val pos' = ((lev_on o lev_dn) p, Frm)
458 val thy = assoc_thy "Isac"
459 val (_,_,_,pt') = (*implicit Take*)Generate.generate1 thy tac_ (is, ctxt) pos' pt
460 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
461 val newnds = children (get_nd pt'' p)
462 val pt''' = ins_chn newnds pt p
463 (*complete_solve cuts branches after*)
464 in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
469 (* val(mI,m)=m;val ppp=p;(*!!!*)val(p,p_)=pos;val(_,pt,_)=ppp(*!!!*);
470 get_form ((mI,m):tac'_) ((p,p_):pos') ppp;
472 fun get_form ((mI,m):tac'_) ((p,p_):pos') pt =
473 case Applicable.applicable_in (p,p_) pt m of
474 Chead.Notappl e => Generate.Error' e
476 (* val Appl m=applicable_in (p,p_) pt m;
478 if member op = specsteps mI
479 then let val (_,_,f,_,_,_) = Chead.specify m (p,p_) [] pt
481 else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
482 in (*f*) Generate.EmptyMout end;