2 Specify-phase: specifying and modeling a problem or a subproblem. The
3 most important types are declared in Selem and Stool (mstools.sml).
4 TODO: allocate elements of structure Selem and of structure Stool appropriately.
5 Author: Walther Neuper 991122, Mathias Lehnfeld
6 (c) due to copyright terms
8 (* Survey on type fmz_ .. type ori .. type itm (in probl, meth) .. formal args of root-/SubProblem
9 and relations between respective list elements: #1#
10 fmz = [ dsc $ v......................................(dsc $ v)..]
11 root problem on pos = ([], _)
12 fmz_ = [(dsc, v).......................................(dsc, v)..]
14 oris = [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)...........(dsc, v)..]
15 \<down> #Given,..,#Relate #Find #undef............#undef \<down>
16 \<down> \<down> \<down> \<down>
17 Specify_Problem + pbl.ppc= [(dsc,id)..(dsc,id),(dsc,id)] \<down> \<down> \<down>
18 \<down> \<down> \<down> \<down>
19 itms = [(dsc, v)..(dsc, v),(dsc, v)] \<down> \<down> \<down>
20 int.modelling +Cor ++++++++++Cor +Cor \<down> \<down> \<down>
21 \<down> \<down> \<down> \<down>
22 Specify_Method + met.ppc= [(dsc,id)..(dsc,id),(dsc,id)] \<down> \<down> \<down>
23 \<down> \<down> \<down> \<down>
24 itms = [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)..(dsc, v)] \<down> \<down>
25 int.modelling +Cor ++++++Cor \<down> \<down>
26 form.args= [ id ..... id , /////// id ....... id ] \<down> \<down>
27 env = [(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
28 interpret code env = [(id, v)..(id, v),(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
29 ..extends env ^^^^^^^^^^^^^^^^ \<down> \<down> \<down> \<down> \<down>
30 \<down> \<down> \<down> \<down> \<down> \<down>
31 SubProblem on pos = ([2], _) \<down> \<down> \<down> \<down> \<down> \<down>
32 form.args= [id ................................ id ]\<down> \<down> \<down>
33 \<down> REAL..BOOL.. \<down> \<down> \<down>
34 \<down> \<down> \<down> \<down>
35 + met.ppc= [(dsc,id).......................(dsc,id)]\<down> \<down> \<down>
36 \<down> \<down> \<down> \<down> \<down>
37 oris = [(dsc, v)...................... (dsc, v) ........... (dsc, v)]\<down>
38 Specify_Problem, int.modelling, Specify_Method, interpret code as above #1# \<down>
40 SubProblem on pos = ([3, 4], _) \<down>
41 form.args= [id ...................... id ] \<down>
42 \<down> REAL..BOOL.. \<down>
43 + met.ppc= [(dsc,id).............(dsc,id)] \<down>
44 oris = [(dsc, v).............(dsc, v)...................(dsc, v)]
45 Specify_Problem, int.modelling, Specify_Method, interpret code as above #1#
48 (1) SubProblem implements sub-function calls such, that the arguments (+ pre- + post-condition)
49 of the functions become concern of interactive modelling.
50 (2) In Isac-terms, the above concerns the phases of modelling and
51 and of specifying (Specify_Problem, Specify_Method),
52 while stepwise construction of solutions is called solving.
53 The latter is supported by Lucas-Interpretation of the functions' body.
54 (3) ori list is determined by fmz_ (in root-pbl) or by args of SubProblem;
55 it is as complete as possible (this has been different up to now).
56 (4) itm list is initialised by pbl-ppc | met-pps and completed (Cor) by stepwise user input.
57 (5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName,
58 add them to the model-pattern of met and let this input be done automatically;
59 respective items must be in fmz.
60 #1# fmz contains items, which are stored in oris of the root(!)-problem.
61 This allows to specify methods, which require more input as anticipated
62 in writing partial_functions: such an item can be fetched from the root-problem's oris.
63 A candidate for this situation is "errorBound" in case an equation cannot be solved symbolically
64 and thus is solved numerically.
72 val nxt_spec : Pos.pos_ -> bool -> O_Model.T -> Spec.T -> I_Model.T * I_Model.T ->
73 (string * (term * 'a)) list * (string * (term * 'b)) list -> Spec.T -> Pos.pos_ * Tactic.input
75 val reset_calchead : Calc.T -> Calc.T
76 val get_ocalhd : Calc.T -> Ctree.ocalhd
77 val ocalhd_complete : I_Model.T -> (bool * term) list -> ThyC.id * Problem.id * Method.id -> bool
78 val all_modspec : Calc.T -> Calc.T
80 val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T
81 val insert_ppc' : I_Model.single -> I_Model.T -> I_Model.T
83 val complete_mod : Calc.T -> Calc.T
84 val is_complete_mod : Calc.T -> bool
85 val complete_spec : Calc.T -> Calc.T
86 val is_complete_spec : Calc.T -> bool
87 val some_spec : Spec.T -> Spec.T -> Spec.T
88 (* these could go to Ctree ..*)
89 val show_pt : Ctree.ctree -> unit
90 val show_pt_tac : Ctree.ctree -> unit
91 val pt_extract : Calc.T -> Ctree.ptform * Tactic.input option * term list
92 val get_interval : Pos.pos' -> Pos.pos' -> int -> Ctree.ctree -> (Pos.pos' * term * Tactic.input option) list
94 val match_ags : theory -> Model_Pattern.T -> term list -> O_Model.T
95 val match_ags_msg : Problem.id -> term -> term list -> unit
96 val oris2fmz_vals : O_Model.T -> string list * term list
97 val vars_of_pbl_' : ('a * ('b * term)) list -> term list
99 val ppc2list : 'a Model.ppc -> 'a list
100 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
101 val mk_additem: string -> TermC.as_string -> Tactic.input
102 val nxt_add: theory -> O_Model.T -> (string * (term * 'a)) list -> (int * Model_Def.variants * bool * string * I_Model.feedback) list -> (string * string) option
103 val is_error: I_Model.feedback -> bool
104 val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * I_Model.T -> I_Model.T * I_Model.T
105 val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> calcstate'
106 val vals_of_oris : O_Model.T -> term list
107 val specify_additem: string -> TermC.as_string -> Calc.T -> string * calcstate'
108 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
109 val e_calcstate : Calc.T * State_Steps.T
110 val e_calcstate' : calcstate'
111 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
112 val posterms2str : (Pos.pos' * term * 'a) list -> string
113 val postermtacs2str : (Pos.pos' * term * Tactic.input option) list -> string
114 val is_copy_named_idstr : string -> bool
115 val is_copy_named_generating_idstr : string -> bool
116 val is_copy_named_generating : 'a * ('b * term) -> bool
117 val is_copy_named : 'a * ('b * term) -> bool
118 val ori2Coritm : Model_Pattern.T -> O_Model.single -> I_Model.single
119 val matc : theory -> (string * (term * term)) list -> term list -> O_Model.preori list -> O_Model.preori list
120 val mtc : theory -> Model_Pattern.single -> term -> O_Model.preori option
121 val cpy_nam : Model_Pattern.T -> O_Model.preori list -> Model_Pattern.single -> O_Model.preori
122 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
124 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
125 val variants_in : term list -> int
126 val is_untouched : I_Model.single -> bool
127 val is_list_type : typ -> bool
128 val parse_ok : I_Model.feedback list -> bool
129 val all_dsc_in : I_Model.feedback list -> term list
130 val chktyps : theory -> term list * term list -> term list (* only in old tests*)
131 val chk_vars : term Model.ppc -> string * term list
132 val unbound_ppc : term Model.ppc -> term list
133 val is_complete_modspec : Calc.T -> bool
134 val get_formress : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
135 (string * Pos.pos' * term) list
136 val get_forms : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
137 (string * Pos.pos' * term) list
141 structure Chead(**): CALC_HEAD(**) =
148 (* the state wich is stored after each step of calculation; it contains
149 the calc-state and a list of [tac,istate](="tacis") to be applied next.
150 the last_elem tacis is the first to apply to the calc-state and
151 the (only) one shown to the front-end as the 'proposed tac'.
152 the calc-state resulting from the application of tacis is not stored,
153 because the tacis hold enough information for efficiently rebuilding
154 this state just by "fun generate "
157 Calc.T * (* the calc-state to which the tacis could be applied *)
158 State_Steps.T (* ev. several (hidden) steps;
159 in REVERSE order: first tac_ to apply is last_elem *)
160 val e_calcstate = ((EmptyPtree, e_pos'), [State_Steps.single_empty]);
162 (*the state used during one calculation within the mathengine; it contains
163 a list of [tac,istate](="tacis") which generated the the calc-state;
164 while this state's tacis are extended by each (internal) step,
165 the calc-state is used for creating new nodes in the calc-tree
166 (eg. applicable_in requires several particular nodes of the calc-tree)
167 and then replaced by the the newly created;
168 on leave of the mathengine the resuing calc-state is dropped anyway,
169 because the tacis hold enought information for efficiently rebuilding
170 this state just by "fun generate ".*)
172 State_Steps.T * (* cas. several (hidden) steps;
173 in REVERSE order: first tac_ to apply is last_elem *)
174 pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
175 Calc.T (* the calc-state resulting from the application of tacis *)
176 val e_calcstate' = ([State_Steps.single_empty], [e_pos'], (EmptyPtree, e_pos')) : calcstate';
178 (* is the calchead complete ? *)
179 fun ocalhd_complete its pre (dI, pI, mI) =
180 foldl and_ (true, map #3 (its: I_Model.T)) andalso
181 foldl and_ (true, map #1 (pre: (bool * term) list)) andalso
182 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
184 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
185 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
186 fun oris2fmz_vals oris =
187 let fun ori2fmz_vals (_, _, _, dsc, ts) =
188 ((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts)
189 handle _ => error ("ori2fmz_env called with " ^ UnparseC.terms ts)
190 in (split_list o (map ori2fmz_vals)) oris end
192 (* find_first item with #1 equal to id *)
193 fun seek_ppc _ [] = NONE
194 | seek_ppc id (p :: ppc) = if id = #1 (p: I_Model.single) then SOME p else seek_ppc id ppc
196 fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
197 gis @ whs @ fis @ wis @ res
199 (* get the number of variants in a problem in 'original',
200 assumes equal descriptions in immediate sequence *)
203 fun eq (x, y) = head_of x = head_of y
204 fun cnt _ [] _ n = ([n], [])
205 | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
206 fun coll _ xs [] = xs
207 | coll eq xs (y :: ys) =
208 let val (n, ys') = cnt eq (y :: ys) y 0
209 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
210 val vts = subtract op = [1] (distinct (coll eq [] ts))
215 | _ => error "different variants in formalization"
218 fun is_list_type (Type ("List.list", _)) = true
219 | is_list_type _ = false
220 fun is_parsed (I_Model.Syn _) = false
222 fun parse_ok its = foldl and_ (true, map is_parsed its)
224 fun all_dsc_in itm_s =
226 fun d_in (I_Model.Cor ((d, _), _)) = [d]
227 | d_in (I_Model.Syn _) = []
228 | d_in (I_Model.Typ _) = []
229 | d_in (I_Model.Inc ((d,_),_)) = [d]
230 | d_in (I_Model.Sup (d,_)) = [d]
231 | d_in (I_Model.Mis (d,_)) = [d]
232 | d_in i = raise ERROR ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
233 in (flat o (map d_in)) itm_s end;
235 fun is_error (I_Model.Cor _) = false
236 | is_error (I_Model.Sup _) = false
237 | is_error (I_Model.Inc _) = false
238 | is_error (I_Model.Mis _) = false
241 (* get the first term in ts from ori *)
242 fun getr_ct thy (_, _, fd, d, ts) =
243 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
245 (* get a term from ori, notyet input in itm.
246 the term from ori is thrown back to a string in order to reuse
247 machinery for immediate input by the user. *)
248 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
249 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))
251 (* in FE dsc, not dat: this is in itms ...*)
252 fun is_untouched (_, _, false, _, I_Model.Inc ((_, []), _)) = true
253 | is_untouched _ = false
255 (* select an item in oris, notyet input in itms
256 (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc) *)
259 oris: from formalization 'type fmz', structured for efficient access
260 pbt : the problem-pattern to be matched with oris in order to get itms
261 itms: already input items
263 fun nxt_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
265 fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0
266 fun is_elem itms (_, (d, _)) =
267 case find_first (test_d d) itms of SOME _ => true | NONE => false
269 case filter_out (is_elem itms) pbt of
270 (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))
273 | nxt_add thy oris _ itms =
275 fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
276 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
277 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
278 fun test_subset itm (_, _, _, d, ts) =
279 (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
280 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
281 | false_and_not_Sup (_, _, false, _, _) = true
282 | false_and_not_Sup _ = false
283 val v = if itms = [] then 1 else I_Model.max_vt itms
284 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
287 then itms (* because of dsc without dat *)
288 else filter (testi_vt v) itms; (* itms..vat *)
289 val icl = filter false_and_not_Sup vits; (* incomplete *)
292 then case filter_out (test_id (map #1 vits)) vors of
294 | miss => SOME (getr_ct thy (hd miss))
296 case find_first (test_subset (hd icl)) vors of
297 NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
298 | SOME ori => SOME (geti_ct thy ori (hd icl))
301 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (Specify.itm_out thy itm_)
302 | mk_delete thy "#Find" itm_ = Tactic.Del_Find (Specify.itm_out thy itm_)
303 | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (Specify.itm_out thy itm_)
304 | mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"")
305 fun mk_additem "#Given" ct = Tactic.Add_Given ct
306 | mk_additem "#Find" ct = Tactic.Add_Find ct
307 | mk_additem "#Relate"ct = Tactic.Add_Relation ct
308 | mk_additem str _ = error ("mk_additem: called with field \"" ^ str ^ "\"")
310 (* determine the next step of specification;
311 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
312 eg. in rootpbl 'no_met':
314 preok predicates are _all_ ok (and problem matches completely)
315 oris immediately from formalization
316 (dI',pI',mI') specification coming from author/parent-problem
317 (pbl, item lists specified by user
318 met) -"-, tacitly completed by copy_probl
319 (dI,pI,mI) specification explicitly done by the user
320 (pbt, mpc) problem type, guard of method
322 fun nxt_spec Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
323 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pbl, Tactic.Specify_Theory dI')
324 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pbl, Tactic.Specify_Problem pI')
326 case find_first (is_error o #5) pbl of
327 SOME (_, _, _, fd, itm_) =>
328 (Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
330 (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
331 SOME (fd, ct') => (Pbl, mk_additem fd ct')
332 | NONE => (*pbl-items complete*)
333 if not preok then (Pbl, Tactic.Refine_Problem pI')
334 else if dI = ThyC.id_empty then (Pbl, Tactic.Specify_Theory dI')
335 else if pI = Problem.id_empty then (Pbl, Tactic.Specify_Problem pI')
336 else if mI = Method.id_empty then (Pbl, Tactic.Specify_Method mI')
338 case find_first (is_error o #5) met of
339 SOME (_, _, _, fd, itm_) => (Met, mk_delete (ThyC.get_theory dI) fd itm_)
341 (case nxt_add (ThyC.get_theory dI) oris mpc met of
342 SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*)
343 | NONE => (Met, Tactic.Apply_Method mI))))
344 | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
345 (case find_first (is_error o #5) met of
346 SOME (_,_,_,fd,itm_) => (Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
348 case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
349 SOME (fd,ct') => (Met, mk_additem fd ct')
351 (if dI = ThyC.id_empty then (Met, Tactic.Specify_Theory dI')
352 else if pI = Problem.id_empty then (Met, Tactic.Specify_Problem pI')
353 else if not preok then (Met, Tactic.Specify_Method mI)
354 else (Met, Tactic.Apply_Method mI)))
355 | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)
357 (* make oris from args of the stac SubProblem and from pbt.
358 can this formal argument (of a model-pattern) be omitted in the arg-list
359 of a SubProblem ? see calcelems.sml 'type met ' *)
360 fun is_copy_named_idstr str =
361 case (rev o Symbol.explode) str of
362 "'" :: _ :: "'" :: _ => true
364 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t
366 (* should this formal argument (of a model-pattern) create a new identifier? *)
367 fun is_copy_named_generating_idstr str =
368 if is_copy_named_idstr str
370 case (rev o Symbol.explode) str of
371 "'" :: "'" :: "'" :: _ => false
374 fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t
376 (* split type-wrapper from scr-arg and build part of an ori;
377 an type-error is reported immediately, raises an exn,
378 subsequent handling of exn provides 2nd part of error message *)
379 fun mtc thy (str, (dsc, _)) (ty $ var) =
380 ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
381 SOME (([1], str, dsc, (*[var]*)
382 Input_Descript.split' (dsc, var))) (*:ori without leading #*))
383 handle e as TYPE _ =>
384 (tracing (dashs 70 ^ "\n"
385 ^ "*** ERROR while creating the items for the model of the ->problem\n"
386 ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
387 ^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"
388 ^ "*** description: " ^ TermC.term_detail2str dsc
389 ^ "*** value: " ^ TermC.term_detail2str var
390 ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
391 ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"
393 writeln (@{make_string} e);
394 Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
396 | mtc _ _ t = error ("mtc: uncovered case with" ^ UnparseC.term t)
398 (* match each pat of the model-pattern with an actual argument;
399 precondition: copy-named vars are filtered out *)
400 fun matc _ [] _ oris = oris
403 error ("actual arg(s) missing for '" ^ Model_Pattern.to_string pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
404 | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
405 (*del?..*)if (is_copy_named_idstr o TermC.free2str) t then oris
407 let val opt = mtc thy p a
410 SOME ori => matc thy pbt ags (oris @ [ori])
411 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
414 (* generate a new variable "x_i" name from a related given one "x"
415 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
416 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
417 but leave is_copy_named_generating as is, e.t. ss''' *)
418 fun cpy_nam pbt oris (p as (field, (dsc, t))) =
419 (if is_copy_named_generating p
420 then (*WN051014 kept strange old code ...*)
421 let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts)
422 val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
423 val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
424 val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
425 val vals = map sel oris
426 val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
427 in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
428 else ([1], field, dsc, [t])
429 ) handle _ => error ("cpy_nam: for "^ UnparseC.term t)
431 (* match the actual arguments of a SubProblem with a model-pattern
432 and create an ori list (in root-pbl created from formalization).
433 expects ags:pats = 1:1, while copy-named are filtered out of pats;
434 if no 1:1 then exn raised by matc/mtc and handled at call.
435 copy-named pats are appended in order to get them into the model-items *)
436 fun match_ags thy pbt ags =
438 fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
439 val pbt' = filter_out is_copy_named pbt
440 val cy = filter is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *)
441 val oris' = matc thy pbt' ags []
442 val cy' = map (cpy_nam pbt' oris') cy
443 val ors = O_Model.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
444 in (map flattup ors) end
446 (* report part of the error-msg which is not available in match_args *)
447 fun match_ags_msg pI stac ags =
449 val pats = (#ppc o Specify.get_pbt) pI
450 val msg = (dots 70 ^ "\n"
451 ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
452 ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
453 ^ "*** stac '" ^ UnparseC.term stac ^ "' has the ...\n"
454 ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"
456 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
459 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
460 fun vars_of_pbl_' pbl_ =
462 fun var_of_pbl_ (_, (_, t)) = t: term
463 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
465 fun overwrite_ppc thy itm ppc =
467 fun repl _ (_, _, _, _, itm_) [] =
468 error ("overwrite_ppc: " ^ (I_Model.feedback_to_string (ThyC.to_ctxt thy) itm_) ^ " not found")
469 | repl ppc' itm (p :: ppc) =
471 then ppc' @ [itm] @ ppc
472 else repl (ppc' @ [p]) itm ppc
473 in repl [] itm ppc end
475 (* 10.3.00: insert the already compiled itm into model;
476 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
477 fun insert_ppc thy itm ppc =
479 fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.d_in itm_)
480 | eq_untouched _ _ = false
481 val ppc' = case seek_ppc (#1 itm) ppc of
482 SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
483 | NONE => (ppc @ [itm])
484 in filter_out (eq_untouched ((I_Model.d_in o #5) itm)) ppc' end
486 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (I_Model.d_in itm_ = I_Model.d_in iitm_)
488 (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
489 handles superfluous items carelessly *)
490 fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
492 (* output the headline to a ppc *)
493 fun header p_ pI mI =
494 case p_ of Pbl => Generate.Problem (if pI = Problem.id_empty then [] else pI)
495 | Met => Generate.Method mI
496 | pos => error ("header called with "^ pos_2str pos)
498 fun specify_additem sel ct (pt, (p, Met)) =
500 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
501 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
502 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
503 | _ => error "specify_additem: uncovered case of get_obj I pt p"
504 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
505 val cpI = if pI = Problem.id_empty then pI' else pI
506 val cmI = if mI = Method.id_empty then mI' else mI
507 val {ppc, pre, prls, ...} = Specify.get_met cmI
509 case I_Model.add_single ctxt sel oris met ppc ct of
510 I_Model.Add itm => (*..union old input *)
512 val met' = insert_ppc thy itm met
513 val arg = case sel of
514 "#Given" => Tactic.Add_Given' (ct, met')
515 | "#Find" => Tactic.Add_Find' (ct, met')
516 | "#Relate"=> Tactic.Add_Relation'(ct, met')
517 | str => error ("specify_additem: uncovered case with " ^ str)
518 val (p, pt') = case Specify_Step.add arg (Istate_Def.Uistate, ctxt) (pt, (p, Met)) of
519 ((p, Met), _, _, pt') => (p, pt')
520 | _ => error "specify_additem: uncovered case of generate1"
521 val pre' = Stool.check_preconds thy prls pre met'
522 val pb = foldl and_ (true, map fst pre')
524 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
525 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
527 ("ok", ([], [], (pt', (p, p_))))
531 val pre' = Stool.check_preconds thy prls pre met
532 val pb = foldl and_ (true, map fst pre')
534 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
535 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
537 (msg, ([], [], (pt, (p, p_))))
540 | specify_additem sel ct (pt, (p,_(*Frm, Pbl*))) =
542 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
543 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
544 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
545 | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
546 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
547 val cpI = if pI = Problem.id_empty then pI' else pI
548 val cmI = if mI = Method.id_empty then mI' else mI
549 val {ppc, where_, prls, ...} = Specify.get_pbt cpI
551 case I_Model.add_single ctxt sel oris pbl ppc ct of
552 I_Model.Add itm => (*..union old input *)
554 val pbl' = insert_ppc thy itm pbl
555 val arg = case sel of
556 "#Given" => Tactic.Add_Given' (ct, pbl')
557 | "#Find" => Tactic.Add_Find' (ct, pbl')
558 | "#Relate"=> Tactic.Add_Relation'(ct, pbl')
559 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
561 case Specify_Step.add arg (Istate_Def.Uistate, ctxt) (pt, (p, Pbl)) of
562 ((p, Pbl), _, _, pt') => (p, pt')
563 | _ => error "specify_additem: uncovered case of Specify_Step.add"
564 val pre = Stool.check_preconds thy prls where_ pbl'
565 val pb = foldl and_ (true, map fst pre)
567 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
568 val ppc = if p_= Pbl then pbl' else met
570 ("ok", ([], [], (pt', (p, p_))))
574 val pre = Stool.check_preconds thy prls where_ pbl
575 val pb = foldl and_ (true, map fst pre)
577 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
578 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
580 (msg, ([], [], (pt, (p, p_))))
584 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
585 -- for input from scratch*)
586 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
588 val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of
589 PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
590 (oris, dI', pI', dI, pI, pbl, ctxt)
591 | _ => error "specify (Specify_Theory': uncovered case get_obj"
592 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
593 val cpI = if pI = Problem.id_empty then pI' else pI;
595 case I_Model.add_single ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
596 I_Model.Add itm (*..union old input *) =>
598 val pbl' = insert_ppc thy itm pbl
599 val (tac, tac_) = case sel of
600 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, pbl'))
601 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, pbl'))
602 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))
603 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
605 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pbl)) of
606 ((p, Pbl), c, _, pt') => (p, c, pt')
607 | _ => error "nxt_specif_additem: uncovered case generate1"
609 ([(tac, tac_, ((p, Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pbl)))
611 | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..
612 FIXME ..and dont abuse a tactic for that purpose*)
613 ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),
614 (e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
616 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
618 val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of
619 PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
620 (oris, dI', mI', dI, mI, met, ctxt)
621 | _ => error "nxt_specif_additem Met: uncovered case get_obj"
622 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
623 val cmI = if mI = Method.id_empty then mI' else mI;
625 case I_Model.add_single ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
626 I_Model.Add itm (*..union old input *) =>
628 val met' = insert_ppc thy itm met;
629 val (tac,tac_) = case sel of
630 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, met'))
631 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, met'))
632 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))
633 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
635 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Met)) of
636 ((p, Met), c, _, pt') => (p, c, pt')
637 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
639 ([(tac, tac_, ((p, Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Met)))
641 | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
643 | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)
645 fun ori2Coritm pbt (i, v, f, d, ts) =
646 (i, v, true, f, I_Model.Cor ((d,ts),((snd o snd o the o (find_first (I_Model.eq1 d))) pbt,ts)))
647 handle _ => (i, v, true, f, I_Model.Cor ((d, ts), (d, ts)))
648 (*dsc in oris, but not in pbl pat list: keep this dsc*)
650 (* filter out oris which have same description in itms *)
651 fun filter_outs oris [] = oris
652 | filter_outs oris (i::itms) =
654 val ors = filter_out ((curry op = ((I_Model.d_in o #5) i)) o (#4)) oris
659 (* filter oris which are in pbt, too *)
660 fun filter_pbt oris pbt =
662 val dscs = map (fst o snd) pbt
664 filter ((member op= dscs) o (#4)) oris
667 (* combine itms from pbl + met and complete them wrt. pbt *)
668 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
669 fun complete_metitms oris pits mits met =
671 val vat = I_Model.max_vt pits;
672 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
673 val ors = filter ((member_swap op= vat) o (#2)) oris
674 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
676 itms @ (map (ori2Coritm met) os)
679 (* complete model and guard of a calc-head *)
680 fun complete_mod_ (oris, mpc, ppc, probl) =
682 val pits = filter_out ((curry op= false) o (#3)) probl
683 val vat = if probl = [] then 1 else I_Model.max_vt probl
684 val pors = filter ((member_swap op = vat) o (#2)) oris
685 val pors = filter_outs pors pits (*which are in pbl already*)
686 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
687 val pits = pits @ (map (ori2Coritm ppc) pors)
688 val mits = complete_metitms oris pits [] mpc
691 fun some_spec (odI, opI, omI) (dI, pI, mI) =
692 (if dI = ThyC.id_empty then odI else dI,
693 if pI = Problem.id_empty then opI else pI,
694 if mI = Method.id_empty then omI else mI)
696 (* get the values from oris; handle the term list w.r.t. penv *)
697 fun vals_of_oris (oris: O_Model.T) =
698 ((map (Model.mkval' o (#5))) o
699 (filter ((member_swap op= 1) o (#2)))) oris
701 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
702 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
703 fun tag_form thy (formal, given) =
705 val gf = (head_of given) $ formal;
706 val _ = Thm.global_cterm_of thy gf
708 handle _ => error ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^
709 " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")
711 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
713 (* check pbltypes, announces one failure a time *)
716 val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc TermC.vars ctppc)
717 val chked = subtract op = gi wh
719 if chked <> [] then ("wh\\gi", chked)
721 let val chked = subtract op = (union op = gi fi) re
724 then ("re\\(gi union fi)", chked)
729 (* check a new pbltype: variables (Free) unbound by given, find*)
730 fun unbound_ppc ctppc =
732 val {Given = gi, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc TermC.vars ctppc)
734 distinct (subtract op = (union op = gi fi) re)
737 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
738 + met from fmz; assumes pos on PblObj, meth = [] *)
739 fun complete_mod (pt, pos as (p, p_) : pos') =
742 then error ("###complete_mod: only impl.for Pbl, called with " ^ pos'2str pos)
744 val (oris, ospec, probl, spec) = case get_obj I pt p of
745 PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
746 | _ => error "complete_mod: unvered case get_obj"
747 val (_, pI, mI) = some_spec ospec spec
748 val mpc = (#ppc o Specify.get_met) mI
749 val ppc = (#ppc o Specify.get_pbt) pI
750 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
751 val pt = update_pblppc pt p pits
752 val pt = update_metppc pt p mits
753 in (pt, (p, Met) : pos') end
755 (* do all specification in one single step:
756 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
757 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
759 fun all_modspec (pt, (p, _)) =
761 val (pors, dI, pI, mI) = case get_obj I pt p of
762 PblObj {origin = (pors, (dI, pI, mI), _), ...}
763 => (pors, dI, pI, mI)
764 | _ => raise ERROR "all_modspec: uncovered case get_obj"
765 val {ppc, ...} = Specify.get_met mI
766 val (_, vals) = oris2fmz_vals pors
767 val ctxt = ContextC.initialise dI vals
768 val (pt, _) = cupdate_problem pt p ((dI, pI, mI),
769 map (ori2Coritm ppc) pors, map (ori2Coritm ppc) pors, ctxt)
774 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
775 fun is_complete_mod_ [] = false
776 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
778 fun is_complete_mod (pt, pos as (p, Pbl) : pos') =
779 if (is_pblobj o (get_obj I pt)) p
780 then (is_complete_mod_ o (get_obj g_pbl pt)) p
781 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
782 | is_complete_mod (pt, pos as (p, Met)) =
783 if (is_pblobj o (get_obj I pt)) p
784 then (is_complete_mod_ o (get_obj g_met pt)) p
785 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
786 | is_complete_mod (_, pos) =
787 error ("is_complete_mod called by " ^ pos'2str pos ^ " (should be Pbl or Met)")
789 (* have (thy, pbl, met) _all_ been specified explicitly ? *)
790 fun is_complete_spec (pt, pos as (p, _) : pos') =
791 if (not o is_pblobj o (get_obj I pt)) p
792 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
794 let val (dI,pI,mI) = get_obj g_spec pt p
795 in dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty end
797 (* complete empty items in specification from origin (pbl, met ev.refined);
798 assumes 'is_complete_mod' *)
799 fun complete_spec (pt, pos as (p, _) : pos') =
801 val (ospec, spec) = case get_obj I pt p of
802 PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
803 | _ => error "complete_spec: uncovered case get_obj"
804 val pt = update_spec pt p (some_spec ospec spec)
809 fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
811 fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =
813 val (_, _, metID) = get_somespec' spec spec'
814 val pre = if metID = Method.id_empty then []
817 val {prls, pre= where_, ...} = Specify.get_met metID
818 val pre = Stool.check_preconds' prls where_ meth 0
820 val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
822 ModSpec (allcorrect, Met, hdl, meth, pre, spec)
824 | pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
826 val (_, pI, _) = get_somespec' spec spec'
827 val pre = if pI = Problem.id_empty then []
830 val {prls, where_, ...} = Specify.get_pbt pI
831 val pre = Stool.check_preconds' prls where_ probl 0
833 val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
835 ModSpec (allcorrect, Pbl, hdl, probl, pre, spec)
837 | pt_model _ _ = error "pt_model: uncovered definition"
839 fun pt_form (PrfObj {form, ...}) = Form form
840 | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) =
842 val (dI, pI, _) = get_somespec' spec spec'
843 val {cas, ...} = Specify.get_pbt pI
845 NONE => Form (Auto_Prog.pblterm dI pI)
846 | SOME t => Form (subst_atomic (I_Model.mk_env probl) t)
849 (* pt_extract returns
851 # the tactic applied to this formula
852 # the list of assumptions generated at this formula
853 (by application of another tac to the preceding formula !)
854 pos is assumed to come from the frontend, ie. generated by moveDown.
855 Notes: cannot be in ctree.sml, because ModSpec has to be calculated.
856 TODO 110417 get assumptions from ctxt !?
858 fun pt_extract (pt, ([], Res)) =
859 (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)
861 val (f, asm) = get_obj g_result pt []
862 in (Form f, NONE, asm) end
863 | pt_extract (pt,(p,Res)) =
865 val (f, asm) = get_obj g_result pt p
869 if is_pblobj' pt (lev_up p)
872 val pI = case get_obj I pt (lev_up p) of
873 PblObj{spec = (_, pI, _), ...} => pI
874 | _ => error "pt_extract last_onlev: uncovered case get_obj"
875 in if pI = Problem.id_empty then NONE else SOME (Tactic.Check_Postcond pI) end
876 else SOME Tactic.End_Trans (* WN0502 TODO for other branches *)
878 let val p' = lev_on p
883 val (dI ,pI) = case get_obj I pt p' of
884 PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)
885 | _ => error "pt_extract \<not>last_onlev: uncovered case get_obj"
886 in SOME (Tactic.Subproblem (dI, pI)) end
888 if f = get_obj g_form pt p'
889 then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
890 else SOME (Tactic.Take (UnparseC.term (get_obj g_form pt p')))
892 in (Form f, tac, asm) end
893 | pt_extract (pt, (p,p_(*Frm,Pbl*))) =
895 val ppobj = get_obj I pt p
896 val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
897 val tac = g_tac ppobj
898 in (f, SOME tac, []) end
900 (** get the formula from a ctree-node:
901 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
902 take res from all other PrfObj's
903 Designed for interSteps, outcommented 04 in favour of calcChangedEvent **)
904 fun formres p (Nd (PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
905 [("headline", (p, Frm), h), ("stepform", (p, Res), r)]
906 | formres p (Nd (PrfObj {form, result = (r, _), ...}, _)) =
907 [("stepform", (p, Frm), form), ("stepform", (p, Res), r)]
908 | formres _ _ = error "formres: uncovered definition"
909 fun form p (Nd (PrfObj {result = (r, _), ...}, _)) =
910 [("stepform", (p, Res), r)]
911 | form _ _ = error "form: uncovered definition"
913 (* assumes to take whole level, in particular hd -- for use in interSteps *)
914 fun get_formress fs _ [] = flat fs
915 | get_formress fs p (nd::nds) =
916 (* start with 'form+res' and continue with trying 'res' only*)
917 get_forms (fs @ [formres p nd]) (lev_on p) nds
918 and get_forms fs _ [] = flat fs
919 | get_forms fs p (nd::nds) =
921 (* start again with 'form+res' ///ugly repeat with Check_elementwise
922 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
923 then get_forms (fs @ [formres p nd]) (lev_on p) nds
924 (* continue with trying 'res' only*)
925 else get_forms (fs @ [form p nd]) (lev_on p) nds;
927 (** get an 'interval' 'from' 'to' of formulae from a ctree **)
928 (* WN0401 this functionality belongs to ctree.sml *)
929 fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2
930 | eq_pos' (p1, Res) (p2, Res) = p1 = p2
931 | eq_pos' (p1, Pbl) (p2, p2_) =
932 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
933 | eq_pos' (p1, Met) (p2, p2_) =
934 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
935 | eq_pos' _ _ = false;
937 (* get an 'interval' from the ctree; 'interval' is w.r.t. the
938 total ordering Position#compareTo(Position p) in the java-code
939 val get_interval = fn :
940 pos' -> : from is "move_up 1st-element" to return
941 pos' -> : to the last element to be returned; from < to
942 int -> : level: 0 gets the flattest sub-tree possible, 999 the deepest
944 (pos' * : of the formula
945 Term.term) : the formula
947 fun get_interval from to level pt =
949 fun get_inter c (from : pos') (to : pos') lev pt =
950 if eq_pos' from to orelse from = ([], Res)
952 let val (f, tacopt, _) = pt_extract (pt, from)
954 ModSpec (_, _, headline, _, _, _) => c @ [(from, headline, NONE)]
955 | Form t => c @ [(from, t, tacopt)]
959 then (get_inter c (move_dn [] pt from) to lev pt)
960 handle (PTREE _(*from move_dn too far*)) => c
963 val (f, tacopt, _) = pt_extract (pt, from)
965 ModSpec (_,_,headline,_,_,_) => headline
967 in (get_inter (c @ [(from, term, tacopt)]) (move_dn [] pt from) to lev pt)
968 handle (PTREE _(*from move_dn too far*)) => c @ [(from, term, tacopt)]
970 in get_inter [] from to level pt end
972 fun posterm2str (pos, t, _) = "(" ^ pos'2str pos ^ ", " ^ UnparseC.term t ^ ")"
973 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
975 fun postermtac2str (pos, t, SOME tac) =
976 pos'2str pos ^ ", " ^ UnparseC.term t ^ "\n" ^ indent 10 ^ Tactic.input_to_string tac
977 | postermtac2str (pos, t, NONE) =
978 pos'2str pos ^ ", " ^ UnparseC.term t
979 fun postermtacs2str pfts = (strs2str' o (map (curry op ^ "\n")) o (map postermtac2str)) pfts
981 (* WN050225 omits the last step, if pt is incomplete *)
982 fun show_pt pt = tracing (posterms2str (get_interval ([], Frm) ([], Res) 99999 pt))
983 fun show_pt_tac pt = tracing (postermtacs2str (get_interval ([], Frm) ([], Res) 99999 pt))
985 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
986 fun get_ocalhd (pt, (p, Pbl) : pos') =
988 val (ospec, hdf', spec, probl) = case get_obj I pt p of
989 PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
990 | _ => error "get_ocalhd Pbl: uncovered case get_obj"
991 val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))
992 val pre = Stool.check_preconds (ThyC.get_theory "Isac_Knowledge") prls where_ probl
994 (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
996 | get_ocalhd (pt, (p, Met)) =
998 val (ospec, hdf', spec, meth) = case get_obj I pt p of
999 PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
1000 | _ => error "get_ocalhd Met: uncovered case get_obj"
1001 val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec))
1002 val pre = Stool.check_preconds (ThyC.get_theory "Isac_Knowledge") prls pre meth
1004 (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
1006 | get_ocalhd _ = error "get_ocalhd: uncovered definition"
1008 (* at the activeFormula set the Model, the Guard and the Specification
1009 to empty and return a CalcHead;
1010 the 'origin' remains (for reconstructing all that) *)
1011 fun reset_calchead (pt, (p,_) : pos') =
1013 val () = case get_obj I pt p of
1015 | _ => error "reset_calchead: uncovered case get_obj"
1016 val pt = update_pbl pt p []
1017 val pt = update_met pt p []
1018 val pt = update_spec pt p Spec.empty
1019 in (pt, (p, Pbl) : pos') end