1 (* Title: Specify/specification.sml
2 Author: Walther Neuper, Mathias Lehnfeld
3 (c) due to copyright terms
5 (* Survey on type fmz_ .. type ori .. type itm (in probl, meth) .. formal args of root-/SubProblem
6 and relations between respective list elements: #1#
7 fmz = [ dsc $ v......................................(dsc $ v)..]
8 root problem on pos = ([], _)
9 fmz_ = [(dsc, v).......................................(dsc, v)..]
11 oris = [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)...........(dsc, v)..]
12 \<down> #Given,..,#Relate #Find #undef............#undef \<down>
13 \<down> \<down> \<down> \<down>
14 Specify_Problem + pbl.ppc= [(dsc,id)..(dsc,id),(dsc,id)] \<down> \<down> \<down>
15 \<down> \<down> \<down> \<down>
16 itms = [(dsc, v)..(dsc, v),(dsc, v)] \<down> \<down> \<down>
17 int.modelling +Cor ++++++++++Cor +Cor \<down> \<down> \<down>
18 \<down> \<down> \<down> \<down>
19 Specify_Method + met.ppc= [(dsc,id)..(dsc,id),(dsc,id)] \<down> \<down> \<down>
20 \<down> \<down> \<down> \<down>
21 itms = [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)..(dsc, v)] \<down> \<down>
22 int.modelling +Cor ++++++Cor \<down> \<down>
23 form.args= [ id ..... id , /////// id ....... id ] \<down> \<down>
24 env = [(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
25 interpret code env = [(id, v)..(id, v),(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
26 ..extends env ^^^^^^^^^^^^^^^^ \<down> \<down> \<down> \<down> \<down>
27 \<down> \<down> \<down> \<down> \<down> \<down>
28 SubProblem on pos = ([2], _) \<down> \<down> \<down> \<down> \<down> \<down>
29 form.args= [id ................................ id ]\<down> \<down> \<down>
30 \<down> REAL..BOOL.. \<down> \<down> \<down>
31 \<down> \<down> \<down> \<down>
32 + met.ppc= [(dsc,id).......................(dsc,id)]\<down> \<down> \<down>
33 \<down> \<down> \<down> \<down> \<down>
34 oris = [(dsc, v)...................... (dsc, v) ........... (dsc, v)]\<down>
35 Specify_Problem, int.modelling, Specify_Method, interpret code as above #1# \<down>
37 SubProblem on pos = ([3, 4], _) \<down>
38 form.args= [id ...................... id ] \<down>
39 \<down> REAL..BOOL.. \<down>
40 + met.ppc= [(dsc,id).............(dsc,id)] \<down>
41 oris = [(dsc, v).............(dsc, v)...................(dsc, v)]
42 Specify_Problem, int.modelling, Specify_Method, interpret code as above #1#
45 (1) SubProblem implements sub-function calls such, that the arguments (+ pre- + post-condition)
46 of the functions become concern of interactive modelling.
47 (2) In Isac-terms, the above concerns the phases of modelling and
48 and of specifying (Specify_Problem, Specify_Method),
49 while stepwise construction of solutions is called solving.
50 The latter is supported by Lucas-Interpretation of the functions' body.
51 (3) ori list is determined by fmz_ (in root-pbl) or by args of SubProblem;
52 it is as complete as possible (this has been different up to now).
53 (4) itm list is initialised by pbl-ppc | met-pps and completed (Cor) by stepwise user input.
54 (5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName,
55 add them to the model-pattern of met and let this input be done automatically;
56 respective items must be in fmz.
58 signature SPECIFICATION =
61 type T = Specification_Def.T
63 (*val reset: Calc.T -> Calc.T*)
64 val reset_calchead: Calc.T -> Calc.T
65 (*val get: Calc.T -> T*)
66 val get_ocalhd: Calc.T -> T
67 (*val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)
68 val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
69 (*val is_complete: Calc.T -> bool*)
70 val is_complete_mod: Calc.T -> bool
72 (*/------- to Specify from Specification -------\* )
73 (*val find_next_step': Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
74 Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input*)
75 val nxt_spec: Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
76 Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input
77 (*val do_all : Calc.T -> Calc.T*)
78 val all_modspec: Calc.T -> Calc.T
79 (*val finish_phase: Calc.T -> Calc.T*)
80 val complete_mod: Calc.T -> Calc.T
81 (*val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option*)
82 val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option
83 (*val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post*)
84 val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post
85 (*val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post*)
86 val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
87 ( *\------- to Specify from Specification -------/*)
89 (*/------- to I_Model from Specification -------\*)
90 val complete_metitms: O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T
91 val insert_ppc': I_Model.single -> I_Model.T -> I_Model.T
92 val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T ->
94 val is_error: I_Model.feedback -> bool
95 val itm_out: theory -> I_Model.feedback -> string
96 val is_complete_mod_: ('a * 'b * bool * 'c * 'd) list -> bool
97 val ori2Coritm: Model_Pattern.T -> O_Model.single -> I_Model.single
98 (*\------- to I_Model from Specification -------/*)
100 (*/------- to P_Model from Specification -------\*)
101 val ppc2list: 'a P_Model.ppc -> 'a list
102 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
103 val mk_additem: string -> TermC.as_string -> Tactic.input
104 (*\------- to P_Model from Specification -------/*)
106 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
108 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
109 val get: Calc.T -> I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
110 val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
111 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
113 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
114 val variants_in: term list -> int
115 val is_untouched: I_Model.single -> bool
116 val is_list_type: typ -> bool
117 val parse_ok: I_Model.feedback list -> bool
118 val all_dsc_in: I_Model.feedback list -> term list
119 val chktyps: theory -> term list * term list -> term list (* only in old tests*)
120 val is_complete_modspec: Calc.T -> bool
121 val get_formress: (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
122 (string * Pos.pos' * term) list
123 val get_forms: (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
124 (string * Pos.pos' * term) list
128 structure Specification(** ): SPECIFICATION( **) =
132 type T = Specification_Def.T;
134 (* is the calchead complete ? *)
135 fun ocalhd_complete its pre (dI, pI, mI) =
136 foldl and_ (true, map #3 (its: I_Model.T)) andalso
137 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
138 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
140 fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
141 gis @ whs @ fis @ wis @ res
143 (* get the number of variants in a problem in 'original',
144 assumes equal descriptions in immediate sequence *)
147 fun eq (x, y) = head_of x = head_of y
148 fun cnt _ [] _ n = ([n], [])
149 | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
150 fun coll _ xs [] = xs
151 | coll eq xs (y :: ys) =
152 let val (n, ys') = cnt eq (y :: ys) y 0
153 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
154 val vts = subtract op = [1] (distinct (coll eq [] ts))
159 | _ => raise ERROR "different variants in formalization"
162 fun is_list_type (Type ("List.list", _)) = true
163 | is_list_type _ = false
164 fun is_parsed (I_Model.Syn _) = false
166 fun parse_ok its = foldl and_ (true, map is_parsed its)
168 fun all_dsc_in itm_s =
170 fun d_in (I_Model.Cor ((d, _), _)) = [d]
171 | d_in (I_Model.Syn _) = []
172 | d_in (I_Model.Typ _) = []
173 | d_in (I_Model.Inc ((d,_),_)) = [d]
174 | d_in (I_Model.Sup (d,_)) = [d]
175 | d_in (I_Model.Mis (d,_)) = [d]
176 | d_in i = raise ERROR ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
177 in (flat o (map d_in)) itm_s end;
179 fun is_error (I_Model.Cor _) = false
180 | is_error (I_Model.Sup _) = false
181 | is_error (I_Model.Inc _) = false
182 | is_error (I_Model.Mis _) = false
185 (* get the first term in ts from ori *)
186 fun getr_ct thy (_, _, fd, d, ts) =
187 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
189 (* get a term from ori, notyet input in itm.
190 the term from ori is thrown back to a string in order to reuse
191 machinery for immediate input by the user. *)
192 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
193 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))
195 (* in FE dsc, not dat: this is in itms ...*)
196 fun is_untouched (_, _, false, _, I_Model.Inc ((_, []), _)) = true
197 | is_untouched _ = false
199 (* select an item in oris, notyet input in itms
200 (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc) *)
203 oris: from formalization 'type fmz', structured for efficient access
204 pbt : the problem-pattern to be matched with oris in order to get itms
205 itms: already input items
207 fun nxt_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
209 fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0
210 fun is_elem itms (_, (d, _)) =
211 case find_first (test_d d) itms of SOME _ => true | NONE => false
213 case filter_out (is_elem itms) pbt of
214 (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))
217 | nxt_add thy oris _ itms =
219 fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
220 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
221 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
222 fun test_subset itm (_, _, _, d, ts) =
223 (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
224 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
225 | false_and_not_Sup (_, _, false, _, _) = true
226 | false_and_not_Sup _ = false
227 val v = if itms = [] then 1 else I_Model.max_vt itms
228 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
231 then itms (* because of dsc without dat *)
232 else filter (testi_vt v) itms; (* itms..vat *)
233 val icl = filter false_and_not_Sup vits; (* incomplete *)
236 then case filter_out (test_id (map #1 vits)) vors of
238 | miss => SOME (getr_ct thy (hd miss))
240 case find_first (test_subset (hd icl)) vors of
241 NONE => raise ERROR "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
242 | SOME ori => SOME (geti_ct thy ori (hd icl))
245 (*create output-string for itm_*)
246 fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
247 | itm_out _ (I_Model.Syn c) = c
248 | itm_out _ (I_Model.Typ c) = c
249 | itm_out _ (I_Model.Inc ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
250 | itm_out _ (I_Model.Sup (d, ts)) = UnparseC.term (Input_Descript.join (d, ts))
251 | itm_out _ (I_Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
252 | itm_out _ _ = raise ERROR "itm_out: uncovered definition"
254 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (itm_out thy itm_)
255 | mk_delete thy "#Find" itm_ = Tactic.Del_Find (itm_out thy itm_)
256 | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (itm_out thy itm_)
257 | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
258 fun mk_additem "#Given" ct = Tactic.Add_Given ct
259 | mk_additem "#Find" ct = Tactic.Add_Find ct
260 | mk_additem "#Relate"ct = Tactic.Add_Relation ct
261 | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")
263 (*/------- to Specify from Specification -------\*)
265 TODO: unify with Specify.find_next_step ! ! ! USED ONLY to determine Pos.Pbl .. Pos.Met
267 determine the next step of specification;
268 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
269 eg. in rootpbl 'no_met':
271 preok predicates are _all_ ok (and problem matches completely)
272 oris immediately from formalization
273 (dI',pI',mI') specification coming from author/parent-problem
274 (pbl, item lists specified by user
275 met) -"-, tacitly completed by copy_probl
276 (dI,pI,mI) specification explicitly done by the user
277 (pbt, mpc) problem type, guard of method
279 fun nxt_spec Pos.Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
280 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
281 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
283 case find_first (is_error o #5) pbl of
284 SOME (_, _, _, fd, itm_) =>
285 (Pos.Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
287 (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
288 SOME (fd, ct') => (Pos.Pbl, mk_additem fd ct')
289 | NONE => (*pbl-items complete*)
290 if not preok then (Pos.Pbl, Tactic.Refine_Problem pI')
291 else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
292 else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
293 else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')
295 case find_first (is_error o #5) met of
296 SOME (_, _, _, fd, itm_) => (Pos.Met, mk_delete (ThyC.get_theory dI) fd itm_)
298 (case nxt_add (ThyC.get_theory dI) oris mpc met of
299 SOME (fd, ct') => (Pos.Met, mk_additem fd ct') (*30.8.01: pre?!?*)
300 | NONE => (Pos.Met, Tactic.Apply_Method mI))))
301 | nxt_spec Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
302 (case find_first (is_error o #5) met of
303 SOME (_,_,_,fd,itm_) => (Pos.Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
305 case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
306 SOME (fd,ct') => (Pos.Met, mk_additem fd ct')
308 (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI')
309 else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI')
310 else if not preok then (Pos.Met, Tactic.Specify_Method mI)
311 else (Pos.Met, Tactic.Apply_Method mI)))
312 | nxt_spec p _ _ _ _ _ _ = raise ERROR ("nxt_spec: uncovered case with " ^ Pos.pos_2str p)
313 (*\------- to Specify from Specification -------/*)
316 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (I_Model.d_in itm_ = I_Model.d_in iitm_)
318 (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
319 handles superfluous items carelessly *)
320 fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
322 (* output the headline to a ppc *)
323 fun header p_ pI mI =
325 Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI)
326 | Pos.Met => Test_Out.Method mI
327 | pos => raise ERROR ("header called with "^ Pos.pos_2str pos)
329 fun make m_field (term_as_string, i_model) =
331 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
332 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
333 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
334 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
335 fun get (pt, (p, _)) =
336 case Ctree.get_obj I pt p of
337 (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
338 => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
339 | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
340 fun specify_additem sel ct (pt, pos as (p, Pos.Met)) =
342 val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos)
343 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
344 val cpI = if pI = Problem.id_empty then pI' else pI
345 val cmI = if mI = Method.id_empty then mI' else mI
346 val {ppc, pre, prls, ...} = Method.from_store cmI
348 case I_Model.check_single ctxt sel oris met ppc ct of
349 I_Model.Add itm => (*..union old input *)
351 val met' = I_Model.add_single thy itm met
353 case Specify_Step.add (make sel (ct, met')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
354 ((p, Pos.Met), _, _, pt') => (p, pt')
355 | _ => raise ERROR "specify_additem: uncovered case of generate1"
356 val pre' = Pre_Conds.check' thy prls pre met'
357 val pb = foldl and_ (true, map fst pre')
359 nxt_spec Pos.Met pb oris (dI',pI',mI') (pbl,met')
360 ((#ppc o Problem.from_store) cpI,ppc) (dI,pI,mI);
362 ("ok", ([], [], (pt', (p, p_))))
366 val pre' = Pre_Conds.check' thy prls pre met
367 val pb = foldl and_ (true, map fst pre')
369 nxt_spec Pos.Met pb oris (dI',pI',mI') (pbl,met)
370 ((#ppc o Problem.from_store) cpI,(#ppc o Method.from_store) cmI) (dI,pI,mI);
372 (msg, ([], [], (pt, (p, p_))))
375 | specify_additem sel ct (pt, pos as (p, _(*Frm, Pbl*))) =
377 val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos)
378 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
379 val cpI = if pI = Problem.id_empty then pI' else pI
380 val cmI = if mI = Method.id_empty then mI' else mI
381 val {ppc, where_, prls, ...} = Problem.from_store cpI
383 case I_Model.check_single ctxt sel oris pbl ppc ct of
384 I_Model.Add itm => (*..union old input *)
386 val pbl' = I_Model.add_single thy itm pbl
388 case Specify_Step.add (make sel (ct, pbl')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
389 ((p, Pos.Pbl), _, _, pt') => (p, pt')
390 | _ => raise ERROR "specify_additem: uncovered case of Specify_Step.add"
391 (* only for getting final p_ ..*)
392 val pre = Pre_Conds.check' thy prls where_ pbl';
393 val pb = foldl and_ (true, map fst pre);
395 nxt_spec Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
397 ("ok", ([], [], (pt', (p, p_))))
401 val pre = Pre_Conds.check' thy prls where_ pbl
402 val pb = foldl and_ (true, map fst pre)
403 val (p_, _(*Tactic.input*)) =
404 nxt_spec Pos.Pbl pb oris (dI', pI', mI') (pbl, met)
405 (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)
407 (msg, ([], [], (pt, (p, p_))))
411 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
412 -- for input from scratch*)
413 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pos.Pbl))) =
415 val (oris, dI', pI', dI, pI, pbl, ctxt) = case Ctree.get_obj I pt p of
416 Ctree.PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
417 (oris, dI', pI', dI, pI, pbl, ctxt)
418 | _ => raise ERROR "specify (Specify_Theory': uncovered case get_obj"
419 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
420 val cpI = if pI = Problem.id_empty then pI' else pI;
422 case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of
423 I_Model.Add itm (*..union old input *) =>
425 val pbl' = I_Model.add_single thy itm pbl
426 val (tac, tac_) = case sel of
427 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, pbl'))
428 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, pbl'))
429 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))
430 | sel => raise ERROR ("nxt_specif_additem: uncovered case of" ^ sel)
432 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
433 ((p, Pos.Pbl), c, _, pt') => (p, c, pt')
434 | _ => raise ERROR "nxt_specif_additem: uncovered case generate1"
436 ([(tac, tac_, ((p, Pos.Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Pbl)))
438 | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..
439 FIXME ..and dont abuse a tactic for that purpose*)
440 ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),
441 (Pos.e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
443 | nxt_specif_additem sel ct (ptp as (pt, (p, Pos.Met))) =
445 val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of
446 Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
447 (oris, dI', mI', dI, mI, met, ctxt)
448 | _ => raise ERROR "nxt_specif_additem Met: uncovered case get_obj"
449 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
450 val cmI = if mI = Method.id_empty then mI' else mI;
452 case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of
453 I_Model.Add itm (*..union old input *) =>
455 val met' = I_Model.add_single thy itm met;
456 val (tac,tac_) = case sel of
457 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, met'))
458 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, met'))
459 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))
460 | sel => raise ERROR ("nxt_specif_additem Met: uncovered case of" ^ sel)
462 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
463 ((p, Pos.Met), c, _, pt') => (p, c, pt')
464 | _ => raise ERROR "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
466 ([(tac, tac_, ((p, Pos.Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Met)))
468 | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
470 | nxt_specif_additem _ _ (_, p) = raise ERROR ("nxt_specif_additem not impl. for" ^ Pos.pos'2str p)
472 (*/------- to I_Model from Specification -------\*)
473 fun ori2Coritm pbt (i, v, f, d, ts) =
474 (i, v, true, f, I_Model.Cor ((d, ts), ((snd o snd o the o (find_first (I_Model.eq1 d))) pbt, ts)))
475 handle _ => (i, v, true, f, I_Model.Cor ((d, ts), (d, ts)))
476 (*dsc in oris, but not in pbl pat list: keep this dsc*)
477 (*\------- to I_Model from Specification -------/*)
479 (* filter out oris which have same description in itms *)
480 fun filter_outs oris [] = oris
481 | filter_outs oris (i::itms) =
483 val ors = filter_out ((curry op = ((I_Model.d_in o #5) i)) o (#4)) oris
488 (* filter oris which are in pbt, too *)
489 fun filter_pbt oris pbt =
491 val dscs = map (fst o snd) pbt
493 filter ((member op= dscs) o (#4)) oris
496 (* combine itms from pbl + met and complete them wrt. pbt *)
497 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
498 fun complete_metitms oris pits mits met =
500 val vat = I_Model.max_vt pits;
501 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
502 val ors = filter ((member_swap op= vat) o (#2)) oris
503 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
505 itms @ (map (ori2Coritm met) os)
508 (* complete model and guard of a calc-head *)
509 fun complete_mod_ (oris, mpc, ppc, probl) =
511 val pits = filter_out ((curry op= false) o (#3)) probl
512 val vat = if probl = [] then 1 else I_Model.max_vt probl
513 val pors = filter ((member_swap op = vat) o (#2)) oris
514 val pors = filter_outs pors pits (*which are in pbl already*)
515 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
516 val pits = pits @ (map (ori2Coritm ppc) pors)
517 val mits = complete_metitms oris pits [] mpc
520 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
521 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
522 fun tag_form thy (formal, given) =
524 val gf = (head_of given) $ formal;
525 val _ = Thm.global_cterm_of thy gf
527 handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^
528 " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")
530 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
532 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
533 + met from fmz; assumes pos on PblObj, meth = [] *)
534 fun complete_mod (pt, pos as (p, p_)) =
536 val _ = if p_ <> Pos.Pbl
537 then raise ERROR ("###complete_mod: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
539 val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of
540 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
541 | _ => raise ERROR "complete_mod: unvered case get_obj"
542 val (_, pI, mI) = References.select ospec spec
543 val mpc = (#ppc o Method.from_store) mI
544 val ppc = (#ppc o Problem.from_store) pI
545 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
546 val pt = Ctree.update_pblppc pt p pits
547 val pt = Ctree.update_metppc pt p mits
548 in (pt, (p, Pos.Met)) end
550 (* do all specification in one single step:
551 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
552 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
554 fun all_modspec (pt, (p, _)) =
556 val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of
557 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}
558 => (pors, dI, pI, mI)
559 | _ => raise ERROR "all_modspec: uncovered case get_obj"
560 val {ppc, ...} = Method.from_store mI
561 val (_, vals) = O_Model.values' pors
562 val ctxt = ContextC.initialise dI vals
563 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
564 map (ori2Coritm ppc) pors, map (ori2Coritm ppc) pors, ctxt)
569 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
570 fun is_complete_mod_ [] = false
571 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
573 fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =
574 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
575 then (is_complete_mod_ o (Ctree.get_obj Ctree.g_pbl pt)) p
576 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
577 | is_complete_mod (pt, pos as (p, Pos.Met)) =
578 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
579 then (is_complete_mod_ o (Ctree.get_obj Ctree.g_met pt)) p
580 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
581 | is_complete_mod (_, pos) =
582 raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
584 fun is_complete_modspec ptp = is_complete_mod ptp andalso References.are_complete ptp
587 (** get the formula from a ctree-node **)
589 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
590 take res from all other PrfObj's
591 Designed for interSteps, outcommented 04 in favour of calcChangedEvent
593 fun formres p (Ctree.Nd (Ctree.PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
594 [("headline", (p, Pos.Frm), h), ("stepform", (p, Pos.Res), r)]
595 | formres p (Ctree.Nd (Ctree.PrfObj {form, result = (r, _), ...}, _)) =
596 [("stepform", (p, Pos.Frm), form), ("stepform", (p, Pos.Res), r)]
597 | formres _ _ = raise ERROR "formres: uncovered definition"
598 fun form p (Ctree.Nd (Ctree.PrfObj {result = (r, _), ...}, _)) =
599 [("stepform", (p, Pos.Res), r)]
600 | form _ _ = raise ERROR "form: uncovered definition"
602 (* assumes to take whole level, in particular hd -- for use in interSteps *)
603 fun get_formress fs _ [] = flat fs
604 | get_formress fs p (nd::nds) =
605 (* start with 'form+res' and continue with trying 'res' only*)
606 get_forms (fs @ [formres p nd]) (Pos.lev_on p) nds
607 and get_forms fs _ [] = flat fs
608 | get_forms fs p (nd::nds) =
610 (* start again with 'form+res' ///ugly repeat with Check_elementwise
611 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
612 then get_forms (fs @ [formres p nd]) (Pos.lev_on p) nds
613 (* continue with trying 'res' only*)
614 else get_forms (fs @ [form p nd]) (Pos.lev_on p) nds;
617 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
618 fun get_ocalhd (pt, (p, Pos.Pbl)) =
620 val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
621 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
622 | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj"
623 val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec))
624 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl
626 (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
628 | get_ocalhd (pt, (p, Pos.Met)) =
630 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
631 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
632 | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj"
633 val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec))
634 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth
636 (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
638 | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition"
640 (* at the activeFormula set the Specification
641 to empty and return a CalcHead;
642 the 'origin' remains (for reconstructing all that) *)
643 fun reset_calchead (pt, (p,_)) =
645 val () = case Ctree.get_obj I pt p of
647 | _ => raise ERROR "reset_calchead: uncovered case get_obj"
648 val pt = Ctree.update_pbl pt p []
649 val pt = Ctree.update_met pt p []
650 val pt = Ctree.update_spec pt p References.empty
651 in (pt, (p, Pos.Pbl)) end