1 (* use"ME/generate.sml";
5 sig (*vvv request into signature is incremental *)
9 datatype edit = EdUndef | Protect | Write
11 datatype nest = Closed | Nundef | Open
12 datatype pblmet = Method of metID | Problem of pblID | Upblmet
14 = Error_ of string | FormKF of cellID * edit * indent * nest * cterm'
15 | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) | RefineKF of match list
16 | RefinedKF of pblID * (itm list * (bool * term) list)
17 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
18 val generate1 : theory -> tac_ -> istate * Proof.context ->
19 posel list * pos_ -> ptree -> pos' * pos' list * mout * ptree
20 val init_pbl : (string * (term * 'a)) list -> itm list
21 val init_pbl' : (string * (term * term)) list -> itm list
25 val generate_hard : theory -> tac_ -> pos * pos_ -> ptree -> pos' * pos' list * mout * ptree
26 val init_istate : tac -> term -> istate
28 val embed_deriv : taci list -> ptree * pos' -> pos' list * (ptree * pos')
29 (* for mathengine.sml *)
30 val generate : (tac * tac_ * ((posel list * pos_) * (istate * Proof.context))) list ->
31 ptree * pos' list * pos' -> ptree * pos' list * pos'
32 (* for interface.sml *)
33 val generate_inconsistent_rew :
34 subs option * thm'' ->
35 term -> istate * Proof.context -> pos * pos_ -> ptree -> ptree * (posel list * pos_)
36 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
37 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
41 structure Ctree(**): CALC_TREE(**) =
44 (* initialize istate for Detail_Set *)
45 fun init_istate (Rewrite_Set rls) t =
46 (case assoc_rls rls of
47 Rrls {scr = Rfuns {init_state = ii, ...}, ...} => RrlsState (ii t)
48 | Rls {scr = EmptyScr, ...} =>
49 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
50 "use prep_rls' for storing rule-sets !")
51 | Rls {scr = Prog s, ...} => (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
52 | Seq {scr=EmptyScr,...} =>
53 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
54 "use prep_rls' for storing rule-sets !")
55 | Seq {scr = Prog s,...} => (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
56 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
57 | init_istate (Rewrite_Set_Inst (subs, rls)) t =
59 val v = case subs2subst (assoc_thy "Isac") subs of
61 | _ => error "init_istate: uncovered case "
62 (*...we suppose the substitution of only _one_ bound variable*)
63 in case assoc_rls rls of
64 Rls {scr = EmptyScr, ...} =>
65 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
66 "use prep_rls' for storing rule-sets !")
67 | Rls {scr = Prog s, ...} =>
68 let val (form, bdv) = two_scr_arg s
69 in (ScrState ([(form, t), (bdv, v)], [], NONE, e_term, Sundef,true))
71 | Seq {scr = EmptyScr, ...} =>
72 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
73 "use prep_rls' for storing rule-sets !")
74 | Seq {scr = Prog s,...} =>
75 let val (form, bdv) = two_scr_arg s
76 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
78 | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
80 | init_istate tac _ = error ("init_istate: uncovered definition for " ^ tac2str tac)
82 (* a taci holds alle information required to build a node in the calc-tree;
83 a taci is assumed to be used efficiently such that the calc-tree
84 resulting from applying a taci need not be stored separately;
85 see "type calcstate" *)
86 (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
87 TODO.WN0512 ? redesign this _list_:
88 # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
89 # the latter problem may be resolved automatically if "fun autocalc" is
90 not any more used for the specify-phase and for changing the phases*)
92 (tac * (* for comparison with input tac *)
93 tac_ * (* for ptree generation *)
94 (pos' * (* after applying tac_, for ptree generation *)
95 (istate * Proof.context))) (* after applying tac_, for ptree generation *)
96 val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci
97 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
98 "( " ^ tac2str tac ^ ", " ^ tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
99 istate2str istate ^ " ))"
100 fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis
102 datatype pblmet = (*%^%*)
103 Upblmet (*undefined*)
104 | Problem of pblID (*%^%*)
105 | Method of metID; (*%^%*)
106 fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
107 | pblmet2str (Method metID) = "Method " ^ metID2str metID (*%^%*)
108 | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)
110 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
111 datatype foppFK = (* in DG cases div 2 *)
112 EmptyFoppFK (*DG internal*)
114 | PpcFK of cterm' ppc
115 fun foppFK2str (FormFK ct') ="FormFK " ^ ct'
116 | foppFK2str (PpcFK ppc) ="PpcFK " ^ ppc2str ppc
117 | foppFK2str EmptyFoppFK ="EmptyFoppFK"
119 datatype nest = Open | Closed | Nundef;
120 fun nest2str Open = "Open"
121 | nest2str Closed = "Closed"
122 | nest2str Nundef = "Nundef"
125 datatype edit = EdUndef | Write | Protect;
126 (* bridge --> kernel *)
127 (* bridge <-> kernel *)
128 (* needed in dialog.sml *) (* bridge <-- kernel *)
129 fun edit2str EdUndef = "EdUndef"
130 | edit2str Write = "Write"
131 | edit2str Protect = "Protect";
133 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
134 Error_ of string (*<--*)
135 | FormKF of cellID * edit * indent * nest * cterm' (*<--*)
136 | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*)
137 | RefineKF of match list (*<--*)
138 | RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)
140 fun inout2str End_Proof = "End_Proof"
141 | inout2str (Error_ s) = "Error_ "^s
142 | inout2str (FormKF (cellID, edit, indent, nest, ct')) =
143 "FormKF ("^(string_of_int cellID)^","
144 ^(edit2str edit)^","^(string_of_int indent)^","
145 ^(nest2str nest)^",("
147 | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) =
148 "PpcKF ("^(string_of_int cellID)^","
149 ^(edit2str edit)^","^(string_of_int indent)^","
150 ^(nest2str nest)^",("
151 ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))"
152 | inout2str (RefineKF ms) = "RefineKF "^(matchs2str ms)
153 | inout2str _ = error "inout2str: uncovered definition"
154 fun inouts2str ios = (strs2str' o (map inout2str)) ios
157 Form' of inout (* packing cterm' | cterm' ppc *)
158 | Problems of inout (* passes specify (and solve) *)
162 fun mout2str (Form' inout) ="Form' "^(inout2str inout)
163 | mout2str (Error' inout) ="Error' "^(inout2str inout)
164 | mout2str (EmptyMout ) ="EmptyMout"
165 | mout2str _ = error "mout2str: uncovered definition"
167 (* init pbl with ...,dsc,empty | [] *)
170 fun pbt2itm (f, (d, _)) = ((0, [], false, f, Inc ((d, []), (e_term, []))) : itm)
171 in map pbt2itm pbt end
173 (* take formal parameters from pbt, for transfer from pbl/met-hierarchy *)
176 fun pbt2itm (f, (d, t)) = ((0, [], false, f, Inc((d, [t]), (e_term, []))) : itm)
177 in map pbt2itm pbt end
179 (*generate 1 ppobj in ptree*)
180 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
181 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt =
182 (pos:pos',[],Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [][]))),
184 Pbl => update_pbl pt p itmlist
185 | Met => update_met pt p itmlist
186 | _ => error ("uncovered case " ^ pos_2str p_))
187 (* WN110515 probably declare_constraints with input item (without dsc) --
188 -- important when specifying without formalisation *)
189 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt =
190 (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
192 Pbl => update_pbl pt p itmlist
193 | Met => update_met pt p itmlist
194 | _ => error ("uncovered case " ^ pos_2str p_))
195 (*WN110515 probably declare_constraints with input item (without dsc)*)
196 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt =
197 (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
199 Pbl => update_pbl pt p itmlist
200 | Met => update_met pt p itmlist
201 | _ => error ("uncovered case " ^ pos_2str p_))
202 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
203 (pos, [] ,Form' (PpcKF (0 ,EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
204 update_domID pt p domID)
205 | generate1 thy (Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt =
207 val pt = update_pbl pt p itms
208 val pt = update_pblID pt p pI
210 ((p, Pbl), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
212 | generate1 thy (Specify_Method' (mID, oris, itms)) _ (p, _) pt =
214 val pt = update_oris pt p oris
215 val pt = update_met pt p itms
216 val pt = update_metID pt p mID
218 ((p, Met), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
220 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
222 val pt = update_pbl pt p itms
223 val pt = update_met pt p met
225 (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
227 | generate1 thy (Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt =
229 val pt = update_pbl pt p pbl
230 val pt = update_orispec pt p (domID, pIre, metID)
232 (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
234 | generate1 thy (Refine_Problem' (pI, _)) _ (pos as (p, _)) pt =
236 val (dI, _, mI) = get_obj g_spec pt p
237 val pt = update_spec pt p (dI, pI, mI)
239 (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
241 | generate1 _ (Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt =
244 let val (pt, c) = cappend_form pt p (is, ctxt) t
245 in (pos, c, EmptyMout, pt) end
246 | NONE => (pos, [], EmptyMout, update_env pt p (SOME (is, ctxt))))
247 | generate1 _ (Take' t) l (p, _) pt = (* val (Take' t) = m; *)
250 let val (ps, p') = split_last p (* no connex to prev.ppobj *)
251 in if p' = 0 then ps @ [1] else p end
252 val (pt, c) = cappend_form pt p l t
254 ((p, Frm): pos', c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
256 | generate1 _ (Begin_Trans' t) l (p, Frm) pt =
258 val (pt, c) = cappend_form pt p l t
259 val pt = update_branch pt p TransitiveB (*040312*)
260 (* replace the old PrfOjb ~~~~~ *)
261 val p = (lev_on o lev_dn (* starts with [...,0] *)) p
262 val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*)
264 ((p, Frm), c @ c', Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
266 | generate1 thy (Begin_Trans' t) l (p, Res) pt =
267 (*append after existing PrfObj vvvvvvvvvvvvv*)
268 generate1 thy (Begin_Trans' t) l (lev_on p, Frm) pt
269 | generate1 _ (End_Trans' tasm) l (p, _) pt =
272 val (pt, c) = append_result pt p' l tasm Complete
274 ((p', Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
276 | generate1 _ (Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt =
278 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
279 (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;
280 val pt = update_branch pt p TransitiveB
281 in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt) end
282 | generate1 _ (Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =
284 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
285 (Rewrite thm') (f', asm) Complete
286 val pt = update_branch pt p TransitiveB
288 ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
290 | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
291 | generate1 _ (Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt =
293 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
294 (Rewrite_Set_Inst (subst2subs subs', id_rls rls')) (f', asm) Complete
295 val pt = update_branch pt p TransitiveB
297 ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
299 | generate1 thy (Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
301 val ctxt' = insert_assumptions asm ctxt
302 val (pt, _) = cappend_form pt p (is, ctxt') f
303 val pt = update_branch pt p TransitiveB
304 val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
305 val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
306 val pos' = ((lev_on o lev_dn) p, Frm)
308 generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
310 | generate1 _ (Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (p, _) pt =
312 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
313 (Rewrite_Set (id_rls rls')) (f',asm) Complete
314 val pt = update_branch pt p TransitiveB
316 ((p, Res), c, Form' (FormKF (~1 ,EdUndef, length p, Nundef, term2str f')), pt)
318 | generate1 thy (Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
320 val ctxt' = insert_assumptions asm ctxt
321 val (pt, _) = cappend_form pt p (is, ctxt') f
322 val pt = update_branch pt p TransitiveB
323 val is = init_istate (Rewrite_Set (id_rls rls)) f
324 val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
325 val pos' = ((lev_on o lev_dn) p, Frm)
327 generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
329 | generate1 _ (Check_Postcond' (_, (scval, asm))) l (p, _) pt =
331 val (pt, c) = append_result pt p l (scval, asm) Complete
333 ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str scval)), pt)
335 | generate1 _ (Calculate' (_, op_, f, (f', _))) l (p, _) pt =
337 val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f', []) Complete
339 ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
341 | generate1 _ (Check_elementwise' (consts, pred, (f', asm))) l (p, _) pt =
343 val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete
345 ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
347 | generate1 _ (Or_to_List' (ors, list)) l (p, _) pt =
349 val (pt,c) = cappend_atomic pt p l ors Or_to_List (list, []) Complete
351 ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str list)), pt)
353 | generate1 _ (Substitute' (_, _, subte, t, t')) l (p, _) pt =
356 cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete
357 in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t')), pt)
359 | generate1 _ (Tac_ (_, f, id, f')) l (p, _) pt =
361 val (pt, c) = cappend_atomic pt p l (str2term f) (Tac id) (str2term f', []) Complete
363 ((p,Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f')), pt)
365 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p, _) pt =
367 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl)
368 val pt = update_ctxt pt p ctxt
369 val f = Syntax.string_of_term (thy2ctxt thy) f
371 ((p, Pbl), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f)), pt)
373 | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ tac_2str m')
375 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
377 val f = get_curr_formula (pt, pos)
378 val pos' as (p', _) = (lev_on p, Res)
379 val (pt, _) = case subs_opt of
380 NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
381 (Rewrite thm') (f', []) Inconsistent
382 | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
383 (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
384 val pt = update_branch pt p' TransitiveB
387 fun generate_hard thy m' (p,p_) pt =
390 Frm => p | Res => lev_on p
391 | _ => error ("generate_hard: call by " ^ pos'2str (p,p_))
392 in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end
394 (* tacis are in reverse order from nxt_solve_/specify_: last = fst to insert *)
395 fun generate ([]: taci list) ptp = ptp
396 | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*))=
398 val (tacis', (_, tac_, (p, is))) = split_last tacis
399 val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
401 generate tacis' (pt', c@c', p')
404 (* update pos in tacis for embedding by generate *)
405 fun insert_pos (_: pos) [] = []
406 | insert_pos (p: pos) (((tac, tac_, (_, ist)): taci) :: tacis) =
407 ((tac, tac_, ((p, Res), ist)): taci) :: (insert_pos (lev_on p) tacis)
409 fun res_from_taci (_, Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
410 | res_from_taci (_, Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
411 | res_from_taci (_, tac_, _) = error ("res_from_taci: called with" ^ tac_2str tac_)
413 (* embed the tacis created by a '_deriv'ation; sys.form <> input.form
414 tacis are in order, thus are reverted for generate *)
415 fun embed_deriv (tacis: taci list) (pt, pos as (p, Frm): pos') =
416 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
417 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
419 val (res, asm) = (res_from_taci o last_elem) tacis
420 val (ist, ctxt) = case get_obj g_loc pt p of
421 (SOME (ist, ctxt), _) => (ist, ctxt)
422 | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj"
423 val form = get_obj g_form pt p
424 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
425 val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt))) ::
426 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm),
427 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
428 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
429 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
430 val pt = update_tac pt p (Derive (id_rls nrls))
431 val pt = update_branch pt p TransitiveB
432 in (c, (pt, pos: pos')) end
433 | embed_deriv tacis (pt, (p, Res)) =
434 (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
435 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
436 let val (res, asm) = (res_from_taci o last_elem) tacis
437 val (ist, ctxt) = case get_obj g_loc pt p of
438 (_, SOME (ist, ctxt)) => (ist, ctxt)
439 | (_, NONE) => error "embed_deriv Frm: uncovered case get_obj"
440 val (f, _) = get_obj g_result pt p
441 val p = lev_on p(*---------------only difference to (..,Frm) above*);
442 val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt))) ::
443 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm),
444 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
445 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
446 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
447 val pt = update_tac pt p (Derive (id_rls nrls))
448 val pt = update_branch pt p TransitiveB
449 in (c, (pt, pos)) end
450 | embed_deriv _ _ = error "embed_deriv: uncovered definition"