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.
57 #1# fmz contains items, which are stored in oris of the root(!)-problem.
58 This allows to specify methods, which require more input as anticipated
59 in writing partial_functions: such an item can be fetched from the root-problem's oris.
60 A candidate for this situation is "errorBound" in case an equation cannot be solved symbolically
61 and thus is solved numerically.
64 signature SPECIFICATION =
67 type T = Specification_Def.T
68 val nxt_spec : Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
69 (string * (term * 'a)) list * (string * (term * 'b)) list -> References.T -> Pos.pos_ * Tactic.input
71 val reset_calchead : Calc.T -> Calc.T
72 val get_ocalhd : Calc.T -> T
73 val ocalhd_complete : I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
74 val all_modspec : Calc.T -> Calc.T
76 val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T
77 val insert_ppc' : I_Model.single -> I_Model.T -> I_Model.T
79 val complete_mod : Calc.T -> Calc.T
80 val is_complete_mod : Calc.T -> bool
81 val complete_spec : Calc.T -> Calc.T
82 val is_complete_spec : Calc.T -> bool
84 val match_ags : theory -> Model_Pattern.T -> term list -> O_Model.T
85 val match_ags_msg : Problem.id -> term -> term list -> unit
86 val oris2fmz_vals : O_Model.T -> string list * term list
87 val vars_of_pbl_' : Model_Pattern.T -> term list
89 val ppc2list : 'a P_Model.ppc -> 'a list
91 val itm_out : theory -> I_Model.feedback -> string
92 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
93 val mk_additem: string -> TermC.as_string -> Tactic.input
94 val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option
95 val is_error: I_Model.feedback -> bool
96 val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T ->
98 val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post
99 val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
101 val is_complete_mod_: ('a * 'b * bool * 'c * 'd) list -> bool
102 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
104 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
105 val is_copy_named_idstr: string -> bool
106 val is_copy_named_generating_idstr: string -> bool
107 val is_copy_named_generating: Model_Pattern.single -> bool
108 val is_copy_named: Model_Pattern.single -> bool
109 val ori2Coritm: Model_Pattern.T -> O_Model.single -> I_Model.single
110 val matc: theory -> Model_Pattern.T -> term list -> O_Model.preori list -> O_Model.preori list
111 val mtc: theory -> Model_Pattern.single -> term -> O_Model.preori option
112 val cpy_nam: Model_Pattern.T -> O_Model.preori list -> Model_Pattern.single -> O_Model.preori
113 val get: Calc.T -> I_Model.T * O_Model.T * ThyC.id * References.id * References.id *
114 I_Model.T * ThyC.id * References.id * References.id * Proof.context
115 val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
116 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
118 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
119 val variants_in : term list -> int
120 val is_untouched : I_Model.single -> bool
121 val is_list_type : typ -> bool
122 val parse_ok : I_Model.feedback list -> bool
123 val all_dsc_in : I_Model.feedback list -> term list
124 val chktyps : theory -> term list * term list -> term list (* only in old tests*)
125 val is_complete_modspec : Calc.T -> bool
126 val get_formress : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
127 (string * Pos.pos' * term) list
128 val get_forms : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
129 (string * Pos.pos' * term) list
133 structure Specification(**): SPECIFICATION(**) =
137 type T = Specification_Def.T;
139 (* is the calchead complete ? *)
140 fun ocalhd_complete its pre (dI, pI, mI) =
141 foldl and_ (true, map #3 (its: I_Model.T)) andalso
142 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
143 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
145 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
146 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
147 fun oris2fmz_vals oris =
148 let fun ori2fmz_vals (_, _, _, dsc, ts) =
149 ((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts)
150 handle _ => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
151 in (split_list o (map ori2fmz_vals)) oris end
153 fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
154 gis @ whs @ fis @ wis @ res
156 (* get the number of variants in a problem in 'original',
157 assumes equal descriptions in immediate sequence *)
160 fun eq (x, y) = head_of x = head_of y
161 fun cnt _ [] _ n = ([n], [])
162 | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
163 fun coll _ xs [] = xs
164 | coll eq xs (y :: ys) =
165 let val (n, ys') = cnt eq (y :: ys) y 0
166 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
167 val vts = subtract op = [1] (distinct (coll eq [] ts))
172 | _ => raise ERROR "different variants in formalization"
175 fun is_list_type (Type ("List.list", _)) = true
176 | is_list_type _ = false
177 fun is_parsed (I_Model.Syn _) = false
179 fun parse_ok its = foldl and_ (true, map is_parsed its)
181 fun all_dsc_in itm_s =
183 fun d_in (I_Model.Cor ((d, _), _)) = [d]
184 | d_in (I_Model.Syn _) = []
185 | d_in (I_Model.Typ _) = []
186 | d_in (I_Model.Inc ((d,_),_)) = [d]
187 | d_in (I_Model.Sup (d,_)) = [d]
188 | d_in (I_Model.Mis (d,_)) = [d]
189 | d_in i = raise ERROR ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
190 in (flat o (map d_in)) itm_s end;
192 fun is_error (I_Model.Cor _) = false
193 | is_error (I_Model.Sup _) = false
194 | is_error (I_Model.Inc _) = false
195 | is_error (I_Model.Mis _) = false
198 (* get the first term in ts from ori *)
199 fun getr_ct thy (_, _, fd, d, ts) =
200 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
202 (* get a term from ori, notyet input in itm.
203 the term from ori is thrown back to a string in order to reuse
204 machinery for immediate input by the user. *)
205 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
206 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))
208 (* in FE dsc, not dat: this is in itms ...*)
209 fun is_untouched (_, _, false, _, I_Model.Inc ((_, []), _)) = true
210 | is_untouched _ = false
212 (* select an item in oris, notyet input in itms
213 (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc) *)
216 oris: from formalization 'type fmz', structured for efficient access
217 pbt : the problem-pattern to be matched with oris in order to get itms
218 itms: already input items
220 fun nxt_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
222 fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0
223 fun is_elem itms (_, (d, _)) =
224 case find_first (test_d d) itms of SOME _ => true | NONE => false
226 case filter_out (is_elem itms) pbt of
227 (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))
230 | nxt_add thy oris _ itms =
232 fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
233 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
234 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
235 fun test_subset itm (_, _, _, d, ts) =
236 (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
237 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
238 | false_and_not_Sup (_, _, false, _, _) = true
239 | false_and_not_Sup _ = false
240 val v = if itms = [] then 1 else I_Model.max_vt itms
241 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
244 then itms (* because of dsc without dat *)
245 else filter (testi_vt v) itms; (* itms..vat *)
246 val icl = filter false_and_not_Sup vits; (* incomplete *)
249 then case filter_out (test_id (map #1 vits)) vors of
251 | miss => SOME (getr_ct thy (hd miss))
253 case find_first (test_subset (hd icl)) vors of
254 NONE => raise ERROR "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
255 | SOME ori => SOME (geti_ct thy ori (hd icl))
258 (*create output-string for itm_*)
259 fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
260 | itm_out _ (I_Model.Syn c) = c
261 | itm_out _ (I_Model.Typ c) = c
262 | itm_out _ (I_Model.Inc ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
263 | itm_out _ (I_Model.Sup (d, ts)) = UnparseC.term (Input_Descript.join (d, ts))
264 | itm_out _ (I_Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
265 | itm_out _ _ = raise ERROR "itm_out: uncovered definition"
267 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (itm_out thy itm_)
268 | mk_delete thy "#Find" itm_ = Tactic.Del_Find (itm_out thy itm_)
269 | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (itm_out thy itm_)
270 | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
271 fun mk_additem "#Given" ct = Tactic.Add_Given ct
272 | mk_additem "#Find" ct = Tactic.Add_Find ct
273 | mk_additem "#Relate"ct = Tactic.Add_Relation ct
274 | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")
276 (* determine the next step of specification;
277 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
278 eg. in rootpbl 'no_met':
280 preok predicates are _all_ ok (and problem matches completely)
281 oris immediately from formalization
282 (dI',pI',mI') specification coming from author/parent-problem
283 (pbl, item lists specified by user
284 met) -"-, tacitly completed by copy_probl
285 (dI,pI,mI) specification explicitly done by the user
286 (pbt, mpc) problem type, guard of method
288 fun nxt_spec Pos.Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
289 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
290 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
292 case find_first (is_error o #5) pbl of
293 SOME (_, _, _, fd, itm_) =>
294 (Pos.Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
296 (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
297 SOME (fd, ct') => (Pos.Pbl, mk_additem fd ct')
298 | NONE => (*pbl-items complete*)
299 if not preok then (Pos.Pbl, Tactic.Refine_Problem pI')
300 else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
301 else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
302 else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')
304 case find_first (is_error o #5) met of
305 SOME (_, _, _, fd, itm_) => (Pos.Met, mk_delete (ThyC.get_theory dI) fd itm_)
307 (case nxt_add (ThyC.get_theory dI) oris mpc met of
308 SOME (fd, ct') => (Pos.Met, mk_additem fd ct') (*30.8.01: pre?!?*)
309 | NONE => (Pos.Met, Tactic.Apply_Method mI))))
310 | nxt_spec Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
311 (case find_first (is_error o #5) met of
312 SOME (_,_,_,fd,itm_) => (Pos.Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
314 case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
315 SOME (fd,ct') => (Pos.Met, mk_additem fd ct')
317 (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI')
318 else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI')
319 else if not preok then (Pos.Met, Tactic.Specify_Method mI)
320 else (Pos.Met, Tactic.Apply_Method mI)))
321 | nxt_spec p _ _ _ _ _ _ = raise ERROR ("nxt_spec: uncovered case with " ^ Pos.pos_2str p)
323 (* make oris from args of the stac SubProblem and from pbt.
324 can this formal argument (of a model-pattern) be omitted in the arg-list
325 of a SubProblem ? see calcelems.sml 'type met ' *)
326 fun is_copy_named_idstr str =
327 case (rev o Symbol.explode) str of
328 "'" :: _ :: "'" :: _ => true
330 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t
332 (* should this formal argument (of a model-pattern) create a new identifier? *)
333 fun is_copy_named_generating_idstr str =
334 if is_copy_named_idstr str
336 case (rev o Symbol.explode) str of
337 "'" :: "'" :: "'" :: _ => false
340 fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t
342 (* split type-wrapper from scr-arg and build part of an ori;
343 an type-error is reported immediately, raises an exn,
344 subsequent handling of exn provides 2nd part of error message *)
345 fun mtc thy (str, (dsc, _)) (ty $ var) =
346 ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
347 SOME (([1], str, dsc, (*[var]*)
348 Input_Descript.split' (dsc, var))) (*:ori without leading #*))
349 handle e as TYPE _ =>
350 (tracing (dashs 70 ^ "\n"
351 ^ "*** ERROR while creating the items for the model of the ->problem\n"
352 ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
353 ^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"
354 ^ "*** description: " ^ TermC.term_detail2str dsc
355 ^ "*** value: " ^ TermC.term_detail2str var
356 ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
357 ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"
359 writeln (@{make_string} e);
360 Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
362 | mtc _ _ t = raise ERROR ("mtc: uncovered case with" ^ UnparseC.term t)
364 (* match each pat of the model-pattern with an actual argument;
365 precondition: copy-named vars are filtered out *)
366 fun matc _ [] _ oris = oris
369 raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
370 | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
371 (*del?..*)if (is_copy_named_idstr o TermC.free2str) t then oris
373 let val opt = mtc thy p a
376 SOME ori => matc thy pbt ags (oris @ [ori])
377 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
380 (* generate a new variable "x_i" name from a related given one "x"
381 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
382 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
383 but leave is_copy_named_generating as is, e.t. ss''' *)
384 fun cpy_nam pbt oris (p as (field, (dsc, t))) =
385 (if is_copy_named_generating p
386 then (*WN051014 kept strange old code ...*)
387 let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts)
388 val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
389 val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
390 val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
391 val vals = map sel oris
392 val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
393 in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
394 else ([1], field, dsc, [t])
395 ) handle _ => raise ERROR ("cpy_nam: for "^ UnparseC.term t)
397 (* match the actual arguments of a SubProblem with a model-pattern
398 and create an ori list (in root-pbl created from formalization).
399 expects ags:pats = 1:1, while copy-named are filtered out of pats;
400 if no 1:1 then exn raised by matc/mtc and handled at call.
401 copy-named pats are appended in order to get them into the model-items *)
402 fun match_ags thy pbt ags =
404 fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
405 val pbt' = filter_out is_copy_named pbt
406 val cy = filter is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *)
407 val oris' = matc thy pbt' ags []
408 val cy' = map (cpy_nam pbt' oris') cy
409 val ors = O_Model.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
410 in (map flattup ors) end
412 (* report part of the error-msg which is not available in match_args *)
413 fun match_ags_msg pI stac ags =
415 val pats = (#ppc o Problem.from_store) pI
416 val msg = (dots 70 ^ "\n"
417 ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
418 ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
419 ^ "*** stac '" ^ UnparseC.term stac ^ "' has the ...\n"
420 ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"
422 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
425 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
426 fun vars_of_pbl_' pbl_ =
428 fun var_of_pbl_ (_, (_, t)) = t: term
429 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
431 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (I_Model.d_in itm_ = I_Model.d_in iitm_)
433 (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
434 handles superfluous items carelessly *)
435 fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
437 (* output the headline to a ppc *)
438 fun header p_ pI mI =
440 Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI)
441 | Pos.Met => Test_Out.Method mI
442 | pos => raise ERROR ("header called with "^ Pos.pos_2str pos)
444 fun make m_field (term_as_string, i_model) =
446 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
447 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
448 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
449 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
450 fun get (pt, (p, _)) =
451 case Ctree.get_obj I pt p of
452 (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
453 => (meth, oris, dI', pI', mI', probl, dI, pI, mI, ctxt)
454 | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
455 fun specify_additem sel ct (pt, pos as (p, Pos.Met)) =
457 val (met, oris, dI', pI', mI', pbl, dI, pI, mI, ctxt) = get (pt, pos)
458 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
459 val cpI = if pI = Problem.id_empty then pI' else pI
460 val cmI = if mI = Method.id_empty then mI' else mI
461 val {ppc, pre, prls, ...} = Method.from_store cmI
463 case I_Model.check_single ctxt sel oris met ppc ct of
464 I_Model.Add itm => (*..union old input *)
466 val met' = I_Model.add_single thy itm met
468 case Specify_Step.add (make sel (ct, met')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
469 ((p, Pos.Met), _, _, pt') => (p, pt')
470 | _ => raise ERROR "specify_additem: uncovered case of generate1"
471 val pre' = Pre_Conds.check' thy prls pre met'
472 val pb = foldl and_ (true, map fst pre')
474 nxt_spec Pos.Met pb oris (dI',pI',mI') (pbl,met')
475 ((#ppc o Problem.from_store) cpI,ppc) (dI,pI,mI);
477 ("ok", ([], [], (pt', (p, p_))))
481 val pre' = Pre_Conds.check' thy prls pre met
482 val pb = foldl and_ (true, map fst pre')
484 nxt_spec Pos.Met pb oris (dI',pI',mI') (pbl,met)
485 ((#ppc o Problem.from_store) cpI,(#ppc o Method.from_store) cmI) (dI,pI,mI);
487 (msg, ([], [], (pt, (p, p_))))
490 | specify_additem sel ct (pt, pos as (p, _(*Frm, Pbl*))) =
492 val (met, oris, dI', pI', mI', pbl, dI, pI, mI, ctxt) = get (pt, pos)
493 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
494 val cpI = if pI = Problem.id_empty then pI' else pI
495 val cmI = if mI = Method.id_empty then mI' else mI
496 val {ppc, where_, prls, ...} = Problem.from_store cpI
498 case I_Model.check_single ctxt sel oris pbl ppc ct of
499 I_Model.Add itm => (*..union old input *)
501 val pbl' = I_Model.add_single thy itm pbl
503 case Specify_Step.add (make sel (ct, pbl')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
504 ((p, Pos.Pbl), _, _, pt') => (p, pt')
505 | _ => raise ERROR "specify_additem: uncovered case of Specify_Step.add"
506 (* only for getting final p_ ..*)
507 val pre = Pre_Conds.check' thy prls where_ pbl';
508 val pb = foldl and_ (true, map fst pre);
510 nxt_spec Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
512 ("ok", ([], [], (pt', (p, p_))))
516 val pre = Pre_Conds.check' thy prls where_ pbl
517 val pb = foldl and_ (true, map fst pre)
518 val (p_, _(*Tactic.input*)) =
519 nxt_spec Pos.Pbl pb oris (dI', pI', mI') (pbl, met)
520 (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)
522 (msg, ([], [], (pt, (p, p_))))
526 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
527 -- for input from scratch*)
528 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pos.Pbl))) =
530 val (oris, dI', pI', dI, pI, pbl, ctxt) = case Ctree.get_obj I pt p of
531 Ctree.PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
532 (oris, dI', pI', dI, pI, pbl, ctxt)
533 | _ => raise ERROR "specify (Specify_Theory': uncovered case get_obj"
534 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
535 val cpI = if pI = Problem.id_empty then pI' else pI;
537 case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of
538 I_Model.Add itm (*..union old input *) =>
540 val pbl' = I_Model.add_single thy itm pbl
541 val (tac, tac_) = case sel of
542 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, pbl'))
543 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, pbl'))
544 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))
545 | sel => raise ERROR ("nxt_specif_additem: uncovered case of" ^ sel)
547 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
548 ((p, Pos.Pbl), c, _, pt') => (p, c, pt')
549 | _ => raise ERROR "nxt_specif_additem: uncovered case generate1"
551 ([(tac, tac_, ((p, Pos.Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Pbl)))
553 | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..
554 FIXME ..and dont abuse a tactic for that purpose*)
555 ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),
556 (Pos.e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
558 | nxt_specif_additem sel ct (ptp as (pt, (p, Pos.Met))) =
560 val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of
561 Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
562 (oris, dI', mI', dI, mI, met, ctxt)
563 | _ => raise ERROR "nxt_specif_additem Met: uncovered case get_obj"
564 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
565 val cmI = if mI = Method.id_empty then mI' else mI;
567 case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of
568 I_Model.Add itm (*..union old input *) =>
570 val met' = I_Model.add_single thy itm met;
571 val (tac,tac_) = case sel of
572 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, met'))
573 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, met'))
574 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))
575 | sel => raise ERROR ("nxt_specif_additem Met: uncovered case of" ^ sel)
577 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
578 ((p, Pos.Met), c, _, pt') => (p, c, pt')
579 | _ => raise ERROR "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
581 ([(tac, tac_, ((p, Pos.Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Met)))
583 | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
585 | nxt_specif_additem _ _ (_, p) = raise ERROR ("nxt_specif_additem not impl. for" ^ Pos.pos'2str p)
587 fun ori2Coritm pbt (i, v, f, d, ts) =
588 (i, v, true, f, I_Model.Cor ((d, ts), ((snd o snd o the o (find_first (I_Model.eq1 d))) pbt, ts)))
589 handle _ => (i, v, true, f, I_Model.Cor ((d, ts), (d, ts)))
590 (*dsc in oris, but not in pbl pat list: keep this dsc*)
592 (* filter out oris which have same description in itms *)
593 fun filter_outs oris [] = oris
594 | filter_outs oris (i::itms) =
596 val ors = filter_out ((curry op = ((I_Model.d_in o #5) i)) o (#4)) oris
601 (* filter oris which are in pbt, too *)
602 fun filter_pbt oris pbt =
604 val dscs = map (fst o snd) pbt
606 filter ((member op= dscs) o (#4)) oris
609 (* combine itms from pbl + met and complete them wrt. pbt *)
610 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
611 fun complete_metitms oris pits mits met =
613 val vat = I_Model.max_vt pits;
614 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
615 val ors = filter ((member_swap op= vat) o (#2)) oris
616 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
618 itms @ (map (ori2Coritm met) os)
621 (* complete model and guard of a calc-head *)
622 fun complete_mod_ (oris, mpc, ppc, probl) =
624 val pits = filter_out ((curry op= false) o (#3)) probl
625 val vat = if probl = [] then 1 else I_Model.max_vt probl
626 val pors = filter ((member_swap op = vat) o (#2)) oris
627 val pors = filter_outs pors pits (*which are in pbl already*)
628 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
629 val pits = pits @ (map (ori2Coritm ppc) pors)
630 val mits = complete_metitms oris pits [] mpc
633 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
634 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
635 fun tag_form thy (formal, given) =
637 val gf = (head_of given) $ formal;
638 val _ = Thm.global_cterm_of thy gf
640 handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^
641 " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")
643 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
645 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
646 + met from fmz; assumes pos on PblObj, meth = [] *)
647 fun complete_mod (pt, pos as (p, p_)) =
649 val _ = if p_ <> Pos.Pbl
650 then raise ERROR ("###complete_mod: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
652 val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of
653 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
654 | _ => raise ERROR "complete_mod: unvered case get_obj"
655 val (_, pI, mI) = References.select ospec spec
656 val mpc = (#ppc o Method.from_store) mI
657 val ppc = (#ppc o Problem.from_store) pI
658 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
659 val pt = Ctree.update_pblppc pt p pits
660 val pt = Ctree.update_metppc pt p mits
661 in (pt, (p, Pos.Met)) end
663 (* do all specification in one single step:
664 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
665 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
667 fun all_modspec (pt, (p, _)) =
669 val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of
670 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}
671 => (pors, dI, pI, mI)
672 | _ => raise ERROR "all_modspec: uncovered case get_obj"
673 val {ppc, ...} = Method.from_store mI
674 val (_, vals) = oris2fmz_vals pors
675 val ctxt = ContextC.initialise dI vals
676 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
677 map (ori2Coritm ppc) pors, map (ori2Coritm ppc) pors, ctxt)
682 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
683 fun is_complete_mod_ [] = false
684 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
686 fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =
687 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
688 then (is_complete_mod_ o (Ctree.get_obj Ctree.g_pbl pt)) p
689 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
690 | is_complete_mod (pt, pos as (p, Pos.Met)) =
691 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
692 then (is_complete_mod_ o (Ctree.get_obj Ctree.g_met pt)) p
693 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
694 | is_complete_mod (_, pos) =
695 raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
697 (* have (thy, pbl, met) _all_ been specified explicitly ? *)
698 fun is_complete_spec (pt, pos as (p, _)) =
699 if (not o Ctree.is_pblobj o (Ctree.get_obj I pt)) p
700 then raise ERROR ("is_complete_spec: called by PrfObj at " ^ Pos.pos'2str pos)
702 let val (dI,pI,mI) = Ctree.get_obj Ctree.g_spec pt p
703 in dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty end
705 (* complete empty items in specification from origin (pbl, met ev.refined);
706 assumes 'is_complete_mod' *)
707 fun complete_spec (pt, pos as (p, _)) =
709 val (ospec, spec) = case Ctree.get_obj I pt p of
710 Ctree.PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
711 | _ => raise ERROR "complete_spec: uncovered case get_obj"
712 val pt = Ctree.update_spec pt p (References.select ospec spec)
717 fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
720 (** get the formula from a ctree-node **)
722 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
723 take res from all other PrfObj's
724 Designed for interSteps, outcommented 04 in favour of calcChangedEvent
726 fun formres p (Ctree.Nd (Ctree.PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
727 [("headline", (p, Pos.Frm), h), ("stepform", (p, Pos.Res), r)]
728 | formres p (Ctree.Nd (Ctree.PrfObj {form, result = (r, _), ...}, _)) =
729 [("stepform", (p, Pos.Frm), form), ("stepform", (p, Pos.Res), r)]
730 | formres _ _ = raise ERROR "formres: uncovered definition"
731 fun form p (Ctree.Nd (Ctree.PrfObj {result = (r, _), ...}, _)) =
732 [("stepform", (p, Pos.Res), r)]
733 | form _ _ = raise ERROR "form: uncovered definition"
735 (* assumes to take whole level, in particular hd -- for use in interSteps *)
736 fun get_formress fs _ [] = flat fs
737 | get_formress fs p (nd::nds) =
738 (* start with 'form+res' and continue with trying 'res' only*)
739 get_forms (fs @ [formres p nd]) (Pos.lev_on p) nds
740 and get_forms fs _ [] = flat fs
741 | get_forms fs p (nd::nds) =
743 (* start again with 'form+res' ///ugly repeat with Check_elementwise
744 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
745 then get_forms (fs @ [formres p nd]) (Pos.lev_on p) nds
746 (* continue with trying 'res' only*)
747 else get_forms (fs @ [form p nd]) (Pos.lev_on p) nds;
750 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
751 fun get_ocalhd (pt, (p, Pos.Pbl)) =
753 val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
754 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
755 | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj"
756 val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec))
757 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl
759 (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
761 | get_ocalhd (pt, (p, Pos.Met)) =
763 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
764 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
765 | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj"
766 val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec))
767 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth
769 (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
771 | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition"
773 (* at the activeFormula set the Specification
774 to empty and return a CalcHead;
775 the 'origin' remains (for reconstructing all that) *)
776 fun reset_calchead (pt, (p,_)) =
778 val () = case Ctree.get_obj I pt p of
780 | _ => raise ERROR "reset_calchead: uncovered case get_obj"
781 val pt = Ctree.update_pbl pt p []
782 val pt = Ctree.update_met pt p []
783 val pt = Ctree.update_spec pt p References.empty
784 in (pt, (p, Pos.Pbl)) end