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.
67 signature SPECIFICATION =
72 type T = Specification_Def.T
73 val nxt_spec : Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
74 (string * (term * 'a)) list * (string * (term * 'b)) list -> References.T -> Pos.pos_ * Tactic.input
76 val reset_calchead : Calc.T -> Calc.T
77 val get_ocalhd : Calc.T -> T
78 val ocalhd_complete : I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
79 val all_modspec : Calc.T -> Calc.T
81 val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T
82 val insert_ppc' : I_Model.single -> I_Model.T -> I_Model.T
84 val complete_mod : Calc.T -> Calc.T
85 val is_complete_mod : Calc.T -> bool
86 val complete_spec : Calc.T -> Calc.T
87 val is_complete_spec : Calc.T -> bool
88 val some_spec : References.T -> References.T -> References.T
89 (* these could go to Ctree ..*)
90 val show_pt : Ctree.ctree -> unit
91 val show_pt_tac : Ctree.ctree -> unit
92 val pt_extract : Calc.T -> Ctree.ptform * Tactic.input option * term list
93 val get_interval : Pos.pos' -> Pos.pos' -> int -> Ctree.ctree -> (Pos.pos' * term * Tactic.input option) list
95 val match_ags : theory -> Model_Pattern.T -> term list -> O_Model.T
96 val match_ags_msg : Problem.id -> term -> term list -> unit
97 val oris2fmz_vals : O_Model.T -> string list * term list
98 val vars_of_pbl_' : Model_Pattern.T -> term list
100 val ppc2list : 'a P_Model.ppc -> 'a list
102 val itm_out : theory -> I_Model.feedback -> string
103 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
104 val mk_additem: string -> TermC.as_string -> Tactic.input
105 val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option
106 val is_error: I_Model.feedback -> bool
107 val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T ->
108 I_Model.T * I_Model.T
109 val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> calcstate'
110 val specify_additem: string -> TermC.as_string -> Calc.T -> string * calcstate'
111 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
112 val e_calcstate : Calc.T * State_Steps.T
113 val e_calcstate' : calcstate'
114 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
115 val posterms2str: (Pos.pos' * term * 'a) list -> string
116 val postermtacs2str: (Pos.pos' * term * Tactic.input option) list -> string
117 val is_copy_named_idstr: string -> bool
118 val is_copy_named_generating_idstr: string -> bool
119 val is_copy_named_generating: Model_Pattern.single -> bool
120 val is_copy_named: Model_Pattern.single -> bool
121 val ori2Coritm: Model_Pattern.T -> O_Model.single -> I_Model.single
122 val matc: theory -> Model_Pattern.T -> term list -> O_Model.preori list -> O_Model.preori list
123 val mtc: theory -> Model_Pattern.single -> term -> O_Model.preori option
124 val cpy_nam: Model_Pattern.T -> O_Model.preori list -> Model_Pattern.single -> O_Model.preori
125 val get: Calc.T -> I_Model.T * O_Model.T * ThyC.id * References.id * References.id *
126 I_Model.T * ThyC.id * References.id * References.id * Proof.context
127 val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
128 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
130 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
131 val variants_in : term list -> int
132 val is_untouched : I_Model.single -> bool
133 val is_list_type : typ -> bool
134 val parse_ok : I_Model.feedback list -> bool
135 val all_dsc_in : I_Model.feedback list -> term list
136 val chktyps : theory -> term list * term list -> term list (* only in old tests*)
137 val is_complete_modspec : Calc.T -> bool
138 val get_formress : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
139 (string * Pos.pos' * term) list
140 val get_forms : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
141 (string * Pos.pos' * term) list
145 structure Specification(**): SPECIFICATION(**) =
151 (* the state wich is stored after each step of calculation; it contains
152 the calc-state and a list of [tac,istate](="tacis") to be applied next.
153 the last_elem tacis is the first to apply to the calc-state and
154 the (only) one shown to the front-end as the 'proposed tac'.
155 the calc-state resulting from the application of tacis is not stored,
156 because the tacis hold enough information for efficiently rebuilding
157 this state just by "fun generate "
160 Calc.T * (* the calc-state to which the tacis could be applied *)
161 State_Steps.T (* ev. several (hidden) steps;
162 in REVERSE order: first tac_ to apply is last_elem *)
163 val e_calcstate = ((Ctree.EmptyPtree, Pos.e_pos'), [State_Steps.single_empty]);
165 (*the state used during one calculation within the mathengine; it contains
166 a list of [tac,istate](="tacis") which generated the the calc-state;
167 while this state's tacis are extended by each (internal) step,
168 the calc-state is used for creating new nodes in the calc-tree
169 (eg. applicable_in requires several particular nodes of the calc-tree)
170 and then replaced by the the newly created;
171 on leave of the mathengine the resuing calc-state is dropped anyway,
172 because the tacis hold enought information for efficiently rebuilding
173 this state just by "fun generate ".*)
175 State_Steps.T * (* cas. several (hidden) steps;
176 in REVERSE order: first tac_ to apply is last_elem *)
177 Pos.pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
178 Calc.T (* the calc-state resulting from the application of tacis *)
179 val e_calcstate' = ([State_Steps.single_empty], [Pos.e_pos'], (Ctree.EmptyPtree, Pos.e_pos')) : calcstate';
181 type T = Specification_Def.T;
183 (* is the calchead complete ? *)
184 fun ocalhd_complete its pre (dI, pI, mI) =
185 foldl and_ (true, map #3 (its: I_Model.T)) andalso
186 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
187 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
189 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
190 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
191 fun oris2fmz_vals oris =
192 let fun ori2fmz_vals (_, _, _, dsc, ts) =
193 ((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts)
194 handle _ => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
195 in (split_list o (map ori2fmz_vals)) oris end
197 fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
198 gis @ whs @ fis @ wis @ res
200 (* get the number of variants in a problem in 'original',
201 assumes equal descriptions in immediate sequence *)
204 fun eq (x, y) = head_of x = head_of y
205 fun cnt _ [] _ n = ([n], [])
206 | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
207 fun coll _ xs [] = xs
208 | coll eq xs (y :: ys) =
209 let val (n, ys') = cnt eq (y :: ys) y 0
210 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
211 val vts = subtract op = [1] (distinct (coll eq [] ts))
216 | _ => raise ERROR "different variants in formalization"
219 fun is_list_type (Type ("List.list", _)) = true
220 | is_list_type _ = false
221 fun is_parsed (I_Model.Syn _) = false
223 fun parse_ok its = foldl and_ (true, map is_parsed its)
225 fun all_dsc_in itm_s =
227 fun d_in (I_Model.Cor ((d, _), _)) = [d]
228 | d_in (I_Model.Syn _) = []
229 | d_in (I_Model.Typ _) = []
230 | d_in (I_Model.Inc ((d,_),_)) = [d]
231 | d_in (I_Model.Sup (d,_)) = [d]
232 | d_in (I_Model.Mis (d,_)) = [d]
233 | d_in i = raise ERROR ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
234 in (flat o (map d_in)) itm_s end;
236 fun is_error (I_Model.Cor _) = false
237 | is_error (I_Model.Sup _) = false
238 | is_error (I_Model.Inc _) = false
239 | is_error (I_Model.Mis _) = false
242 (* get the first term in ts from ori *)
243 fun getr_ct thy (_, _, fd, d, ts) =
244 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
246 (* get a term from ori, notyet input in itm.
247 the term from ori is thrown back to a string in order to reuse
248 machinery for immediate input by the user. *)
249 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
250 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))
252 (* in FE dsc, not dat: this is in itms ...*)
253 fun is_untouched (_, _, false, _, I_Model.Inc ((_, []), _)) = true
254 | is_untouched _ = false
256 (* select an item in oris, notyet input in itms
257 (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc) *)
260 oris: from formalization 'type fmz', structured for efficient access
261 pbt : the problem-pattern to be matched with oris in order to get itms
262 itms: already input items
264 fun nxt_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
266 fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0
267 fun is_elem itms (_, (d, _)) =
268 case find_first (test_d d) itms of SOME _ => true | NONE => false
270 case filter_out (is_elem itms) pbt of
271 (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))
274 | nxt_add thy oris _ itms =
276 fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
277 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
278 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
279 fun test_subset itm (_, _, _, d, ts) =
280 (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
281 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
282 | false_and_not_Sup (_, _, false, _, _) = true
283 | false_and_not_Sup _ = false
284 val v = if itms = [] then 1 else I_Model.max_vt itms
285 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
288 then itms (* because of dsc without dat *)
289 else filter (testi_vt v) itms; (* itms..vat *)
290 val icl = filter false_and_not_Sup vits; (* incomplete *)
293 then case filter_out (test_id (map #1 vits)) vors of
295 | miss => SOME (getr_ct thy (hd miss))
297 case find_first (test_subset (hd icl)) vors of
298 NONE => raise ERROR "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
299 | SOME ori => SOME (geti_ct thy ori (hd icl))
302 (*create output-string for itm_*)
303 fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
304 | itm_out _ (I_Model.Syn c) = c
305 | itm_out _ (I_Model.Typ c) = c
306 | itm_out _ (I_Model.Inc ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
307 | itm_out _ (I_Model.Sup (d, ts)) = UnparseC.term (Input_Descript.join (d, ts))
308 | itm_out _ (I_Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
309 | itm_out _ _ = raise ERROR "itm_out: uncovered definition"
311 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (itm_out thy itm_)
312 | mk_delete thy "#Find" itm_ = Tactic.Del_Find (itm_out thy itm_)
313 | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (itm_out thy itm_)
314 | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
315 fun mk_additem "#Given" ct = Tactic.Add_Given ct
316 | mk_additem "#Find" ct = Tactic.Add_Find ct
317 | mk_additem "#Relate"ct = Tactic.Add_Relation ct
318 | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")
320 (* determine the next step of specification;
321 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
322 eg. in rootpbl 'no_met':
324 preok predicates are _all_ ok (and problem matches completely)
325 oris immediately from formalization
326 (dI',pI',mI') specification coming from author/parent-problem
327 (pbl, item lists specified by user
328 met) -"-, tacitly completed by copy_probl
329 (dI,pI,mI) specification explicitly done by the user
330 (pbt, mpc) problem type, guard of method
332 fun nxt_spec Pos.Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
333 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
334 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
336 case find_first (is_error o #5) pbl of
337 SOME (_, _, _, fd, itm_) =>
338 (Pos.Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
340 (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
341 SOME (fd, ct') => (Pos.Pbl, mk_additem fd ct')
342 | NONE => (*pbl-items complete*)
343 if not preok then (Pos.Pbl, Tactic.Refine_Problem pI')
344 else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
345 else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
346 else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')
348 case find_first (is_error o #5) met of
349 SOME (_, _, _, fd, itm_) => (Pos.Met, mk_delete (ThyC.get_theory dI) fd itm_)
351 (case nxt_add (ThyC.get_theory dI) oris mpc met of
352 SOME (fd, ct') => (Pos.Met, mk_additem fd ct') (*30.8.01: pre?!?*)
353 | NONE => (Pos.Met, Tactic.Apply_Method mI))))
354 | nxt_spec Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
355 (case find_first (is_error o #5) met of
356 SOME (_,_,_,fd,itm_) => (Pos.Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
358 case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
359 SOME (fd,ct') => (Pos.Met, mk_additem fd ct')
361 (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI')
362 else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI')
363 else if not preok then (Pos.Met, Tactic.Specify_Method mI)
364 else (Pos.Met, Tactic.Apply_Method mI)))
365 | nxt_spec p _ _ _ _ _ _ = raise ERROR ("nxt_spec: uncovered case with " ^ Pos.pos_2str p)
367 (* make oris from args of the stac SubProblem and from pbt.
368 can this formal argument (of a model-pattern) be omitted in the arg-list
369 of a SubProblem ? see calcelems.sml 'type met ' *)
370 fun is_copy_named_idstr str =
371 case (rev o Symbol.explode) str of
372 "'" :: _ :: "'" :: _ => true
374 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t
376 (* should this formal argument (of a model-pattern) create a new identifier? *)
377 fun is_copy_named_generating_idstr str =
378 if is_copy_named_idstr str
380 case (rev o Symbol.explode) str of
381 "'" :: "'" :: "'" :: _ => false
384 fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t
386 (* split type-wrapper from scr-arg and build part of an ori;
387 an type-error is reported immediately, raises an exn,
388 subsequent handling of exn provides 2nd part of error message *)
389 fun mtc thy (str, (dsc, _)) (ty $ var) =
390 ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
391 SOME (([1], str, dsc, (*[var]*)
392 Input_Descript.split' (dsc, var))) (*:ori without leading #*))
393 handle e as TYPE _ =>
394 (tracing (dashs 70 ^ "\n"
395 ^ "*** ERROR while creating the items for the model of the ->problem\n"
396 ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
397 ^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"
398 ^ "*** description: " ^ TermC.term_detail2str dsc
399 ^ "*** value: " ^ TermC.term_detail2str var
400 ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
401 ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"
403 writeln (@{make_string} e);
404 Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
406 | mtc _ _ t = raise ERROR ("mtc: uncovered case with" ^ UnparseC.term t)
408 (* match each pat of the model-pattern with an actual argument;
409 precondition: copy-named vars are filtered out *)
410 fun matc _ [] _ oris = oris
413 raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
414 | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
415 (*del?..*)if (is_copy_named_idstr o TermC.free2str) t then oris
417 let val opt = mtc thy p a
420 SOME ori => matc thy pbt ags (oris @ [ori])
421 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
424 (* generate a new variable "x_i" name from a related given one "x"
425 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
426 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
427 but leave is_copy_named_generating as is, e.t. ss''' *)
428 fun cpy_nam pbt oris (p as (field, (dsc, t))) =
429 (if is_copy_named_generating p
430 then (*WN051014 kept strange old code ...*)
431 let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts)
432 val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
433 val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
434 val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
435 val vals = map sel oris
436 val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
437 in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
438 else ([1], field, dsc, [t])
439 ) handle _ => raise ERROR ("cpy_nam: for "^ UnparseC.term t)
441 (* match the actual arguments of a SubProblem with a model-pattern
442 and create an ori list (in root-pbl created from formalization).
443 expects ags:pats = 1:1, while copy-named are filtered out of pats;
444 if no 1:1 then exn raised by matc/mtc and handled at call.
445 copy-named pats are appended in order to get them into the model-items *)
446 fun match_ags thy pbt ags =
448 fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
449 val pbt' = filter_out is_copy_named pbt
450 val cy = filter is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *)
451 val oris' = matc thy pbt' ags []
452 val cy' = map (cpy_nam pbt' oris') cy
453 val ors = O_Model.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
454 in (map flattup ors) end
456 (* report part of the error-msg which is not available in match_args *)
457 fun match_ags_msg pI stac ags =
459 val pats = (#ppc o Problem.from_store) pI
460 val msg = (dots 70 ^ "\n"
461 ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
462 ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
463 ^ "*** stac '" ^ UnparseC.term stac ^ "' has the ...\n"
464 ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"
466 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
469 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
470 fun vars_of_pbl_' pbl_ =
472 fun var_of_pbl_ (_, (_, t)) = t: term
473 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
475 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (I_Model.d_in itm_ = I_Model.d_in iitm_)
477 (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
478 handles superfluous items carelessly *)
479 fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
481 (* output the headline to a ppc *)
482 fun header p_ pI mI =
484 Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI)
485 | Pos.Met => Test_Out.Method mI
486 | pos => raise ERROR ("header called with "^ Pos.pos_2str pos)
488 fun make m_field (term_as_string, i_model) =
490 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
491 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
492 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
493 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
494 fun get (pt, (p, _)) =
495 case Ctree.get_obj I pt p of
496 (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
497 => (meth, oris, dI', pI', mI', probl, dI, pI, mI, ctxt)
498 | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
499 fun specify_additem sel ct (pt, pos as (p, Pos.Met)) =
501 val (met, oris, dI', pI', mI', pbl, dI, pI, mI, ctxt) = get (pt, pos)
502 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
503 val cpI = if pI = Problem.id_empty then pI' else pI
504 val cmI = if mI = Method.id_empty then mI' else mI
505 val {ppc, pre, prls, ...} = Method.from_store cmI
507 case I_Model.check_single ctxt sel oris met ppc ct of
508 I_Model.Add itm => (*..union old input *)
510 val met' = I_Model.add_single thy itm met
512 case Specify_Step.add (make sel (ct, met')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
513 ((p, Pos.Met), _, _, pt') => (p, pt')
514 | _ => raise ERROR "specify_additem: uncovered case of generate1"
515 val pre' = Pre_Conds.check' thy prls pre met'
516 val pb = foldl and_ (true, map fst pre')
518 nxt_spec Pos.Met pb oris (dI',pI',mI') (pbl,met')
519 ((#ppc o Problem.from_store) cpI,ppc) (dI,pI,mI);
521 ("ok", ([], [], (pt', (p, p_))))
525 val pre' = Pre_Conds.check' thy prls pre met
526 val pb = foldl and_ (true, map fst pre')
528 nxt_spec Pos.Met pb oris (dI',pI',mI') (pbl,met)
529 ((#ppc o Problem.from_store) cpI,(#ppc o Method.from_store) cmI) (dI,pI,mI);
531 (msg, ([], [], (pt, (p, p_))))
534 | specify_additem sel ct (pt, pos as (p, _(*Frm, Pbl*))) =
536 val (met, oris, dI', pI', mI', pbl, dI, pI, mI, ctxt) = get (pt, pos)
537 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
538 val cpI = if pI = Problem.id_empty then pI' else pI
539 val cmI = if mI = Method.id_empty then mI' else mI
540 val {ppc, where_, prls, ...} = Problem.from_store cpI
542 case I_Model.check_single ctxt sel oris pbl ppc ct of
543 I_Model.Add itm => (*..union old input *)
545 val pbl' = I_Model.add_single thy itm pbl
547 case Specify_Step.add (make sel (ct, pbl')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
548 ((p, Pos.Pbl), _, _, pt') => (p, pt')
549 | _ => raise ERROR "specify_additem: uncovered case of Specify_Step.add"
550 (* only for getting final p_ ..*)
551 val pre = Pre_Conds.check' thy prls where_ pbl';
552 val pb = foldl and_ (true, map fst pre);
554 nxt_spec Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
556 ("ok", ([], [], (pt', (p, p_))))
560 val pre = Pre_Conds.check' thy prls where_ pbl
561 val pb = foldl and_ (true, map fst pre)
562 val (p_, _(*Tactic.input*)) =
563 nxt_spec Pos.Pbl pb oris (dI', pI', mI') (pbl, met)
564 (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)
566 (msg, ([], [], (pt, (p, p_))))
570 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
571 -- for input from scratch*)
572 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pos.Pbl))) =
574 val (oris, dI', pI', dI, pI, pbl, ctxt) = case Ctree.get_obj I pt p of
575 Ctree.PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
576 (oris, dI', pI', dI, pI, pbl, ctxt)
577 | _ => raise ERROR "specify (Specify_Theory': uncovered case get_obj"
578 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
579 val cpI = if pI = Problem.id_empty then pI' else pI;
581 case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of
582 I_Model.Add itm (*..union old input *) =>
584 val pbl' = I_Model.add_single thy itm pbl
585 val (tac, tac_) = case sel of
586 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, pbl'))
587 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, pbl'))
588 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))
589 | sel => raise ERROR ("nxt_specif_additem: uncovered case of" ^ sel)
591 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
592 ((p, Pos.Pbl), c, _, pt') => (p, c, pt')
593 | _ => raise ERROR "nxt_specif_additem: uncovered case generate1"
595 ([(tac, tac_, ((p, Pos.Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Pbl)))
597 | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..
598 FIXME ..and dont abuse a tactic for that purpose*)
599 ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),
600 (Pos.e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
602 | nxt_specif_additem sel ct (ptp as (pt, (p, Pos.Met))) =
604 val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of
605 Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
606 (oris, dI', mI', dI, mI, met, ctxt)
607 | _ => raise ERROR "nxt_specif_additem Met: uncovered case get_obj"
608 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
609 val cmI = if mI = Method.id_empty then mI' else mI;
611 case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of
612 I_Model.Add itm (*..union old input *) =>
614 val met' = I_Model.add_single thy itm met;
615 val (tac,tac_) = case sel of
616 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, met'))
617 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, met'))
618 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))
619 | sel => raise ERROR ("nxt_specif_additem Met: uncovered case of" ^ sel)
621 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
622 ((p, Pos.Met), c, _, pt') => (p, c, pt')
623 | _ => raise ERROR "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
625 ([(tac, tac_, ((p, Pos.Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Met)))
627 | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
629 | nxt_specif_additem _ _ (_, p) = raise ERROR ("nxt_specif_additem not impl. for" ^ Pos.pos'2str p)
631 fun ori2Coritm pbt (i, v, f, d, ts) =
632 (i, v, true, f, I_Model.Cor ((d, ts), ((snd o snd o the o (find_first (I_Model.eq1 d))) pbt, ts)))
633 handle _ => (i, v, true, f, I_Model.Cor ((d, ts), (d, ts)))
634 (*dsc in oris, but not in pbl pat list: keep this dsc*)
636 (* filter out oris which have same description in itms *)
637 fun filter_outs oris [] = oris
638 | filter_outs oris (i::itms) =
640 val ors = filter_out ((curry op = ((I_Model.d_in o #5) i)) o (#4)) oris
645 (* filter oris which are in pbt, too *)
646 fun filter_pbt oris pbt =
648 val dscs = map (fst o snd) pbt
650 filter ((member op= dscs) o (#4)) oris
653 (* combine itms from pbl + met and complete them wrt. pbt *)
654 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
655 fun complete_metitms oris pits mits met =
657 val vat = I_Model.max_vt pits;
658 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
659 val ors = filter ((member_swap op= vat) o (#2)) oris
660 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
662 itms @ (map (ori2Coritm met) os)
665 (* complete model and guard of a calc-head *)
666 fun complete_mod_ (oris, mpc, ppc, probl) =
668 val pits = filter_out ((curry op= false) o (#3)) probl
669 val vat = if probl = [] then 1 else I_Model.max_vt probl
670 val pors = filter ((member_swap op = vat) o (#2)) oris
671 val pors = filter_outs pors pits (*which are in pbl already*)
672 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
673 val pits = pits @ (map (ori2Coritm ppc) pors)
674 val mits = complete_metitms oris pits [] mpc
677 fun some_spec (odI, opI, omI) (dI, pI, mI) =
678 (if dI = ThyC.id_empty then odI else dI,
679 if pI = Problem.id_empty then opI else pI,
680 if mI = Method.id_empty then omI else mI)
682 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
683 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
684 fun tag_form thy (formal, given) =
686 val gf = (head_of given) $ formal;
687 val _ = Thm.global_cterm_of thy gf
689 handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^
690 " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")
692 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
694 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
695 + met from fmz; assumes pos on PblObj, meth = [] *)
696 fun complete_mod (pt, pos as (p, p_)) =
698 val _ = if p_ <> Pos.Pbl
699 then raise ERROR ("###complete_mod: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
701 val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of
702 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
703 | _ => raise ERROR "complete_mod: unvered case get_obj"
704 val (_, pI, mI) = some_spec ospec spec
705 val mpc = (#ppc o Method.from_store) mI
706 val ppc = (#ppc o Problem.from_store) pI
707 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
708 val pt = Ctree.update_pblppc pt p pits
709 val pt = Ctree.update_metppc pt p mits
710 in (pt, (p, Pos.Met)) end
712 (* do all specification in one single step:
713 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
714 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
716 fun all_modspec (pt, (p, _)) =
718 val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of
719 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}
720 => (pors, dI, pI, mI)
721 | _ => raise ERROR "all_modspec: uncovered case get_obj"
722 val {ppc, ...} = Method.from_store mI
723 val (_, vals) = oris2fmz_vals pors
724 val ctxt = ContextC.initialise dI vals
725 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
726 map (ori2Coritm ppc) pors, map (ori2Coritm ppc) pors, ctxt)
731 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
732 fun is_complete_mod_ [] = false
733 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
735 fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =
736 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
737 then (is_complete_mod_ o (Ctree.get_obj Ctree.g_pbl pt)) p
738 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
739 | is_complete_mod (pt, pos as (p, Pos.Met)) =
740 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
741 then (is_complete_mod_ o (Ctree.get_obj Ctree.g_met pt)) p
742 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
743 | is_complete_mod (_, pos) =
744 raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
746 (* have (thy, pbl, met) _all_ been specified explicitly ? *)
747 fun is_complete_spec (pt, pos as (p, _)) =
748 if (not o Ctree.is_pblobj o (Ctree.get_obj I pt)) p
749 then raise ERROR ("is_complete_spec: called by PrfObj at " ^ Pos.pos'2str pos)
751 let val (dI,pI,mI) = Ctree.get_obj Ctree.g_spec pt p
752 in dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty end
754 (* complete empty items in specification from origin (pbl, met ev.refined);
755 assumes 'is_complete_mod' *)
756 fun complete_spec (pt, pos as (p, _)) =
758 val (ospec, spec) = case Ctree.get_obj I pt p of
759 Ctree.PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
760 | _ => raise ERROR "complete_spec: uncovered case get_obj"
761 val pt = Ctree.update_spec pt p (some_spec ospec spec)
766 fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
768 fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ...}) Pos.Met =
770 val (_, _, metID) = Ctree.get_somespec' spec spec'
771 val pre = if metID = Method.id_empty then []
774 val {prls, pre= where_, ...} = Method.from_store metID
775 val pre = Pre_Conds.check prls where_ meth 0
777 val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
779 Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, pre, spec)
781 | pt_model (Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
783 val (_, pI, _) = Ctree.get_somespec' spec spec'
784 val pre = if pI = Problem.id_empty then []
787 val {prls, where_, ...} = Problem.from_store pI
788 val pre = Pre_Conds.check prls where_ probl 0
790 val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
792 Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, pre, spec)
794 | pt_model _ _ = raise ERROR "pt_model: uncovered definition"
796 fun pt_form (Ctree.PrfObj {form, ...}) = Ctree.Form form
797 | pt_form (Ctree.PblObj {probl, spec, origin = (_, spec', _), ...}) =
799 val (dI, pI, _) = Ctree.get_somespec' spec spec'
800 val {cas, ...} = Problem.from_store pI
802 NONE => Ctree.Form (Auto_Prog.pblterm dI pI)
803 | SOME t => Ctree.Form (subst_atomic (I_Model.mk_env probl) t)
806 (* pt_extract returns
808 # the tactic applied to this formula
809 # the list of assumptions generated at this formula
810 (by application of another tac to the preceding formula !)
811 pos is assumed to come from the frontend, ie. generated by moveDown.
812 Notes: cannot be in ctree.sml, because ModSpec has to be calculated.
813 TODO 110417 get assumptions from ctxt !?
815 fun pt_extract (pt, ([], Pos.Res)) =
816 (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)
818 val (f, asm) = Ctree.get_obj Ctree.g_result pt []
819 in (Ctree.Form f, NONE, asm) end
820 | pt_extract (pt, (p, Pos.Res)) =
822 val (f, asm) = Ctree.get_obj Ctree.g_result pt p
824 if Ctree.last_onlev pt p
826 if Ctree.is_pblobj' pt (Pos.lev_up p)
829 val pI = case Ctree.get_obj I pt (Pos.lev_up p) of
830 Ctree.PblObj{spec = (_, pI, _), ...} => pI
831 | _ => raise ERROR "pt_extract last_onlev: uncovered case get_obj"
832 in if pI = Problem.id_empty then NONE else SOME (Tactic.Check_Postcond pI) end
833 else SOME Tactic.End_Trans (* WN0502 TODO for other branches *)
835 let val p' = Pos.lev_on p
837 if Ctree.is_pblobj' pt p'
840 val (dI , pI) = case Ctree.get_obj I pt p' of
841 Ctree.PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)
842 | _ => raise ERROR "pt_extract \<not>last_onlev: uncovered case get_obj"
843 in SOME (Tactic.Subproblem (dI, pI)) end
845 if f = Ctree.get_obj Ctree.g_form pt p'
846 then SOME (Ctree.get_obj Ctree.g_tac pt p') (*because this Frm ~~~is not on worksheet*)
847 else SOME (Tactic.Take (UnparseC.term (Ctree.get_obj Ctree.g_form pt p')))
849 in (Ctree.Form f, tac, asm) end
850 | pt_extract (pt, (p, p_(*Frm,Pbl*))) =
852 val ppobj = Ctree.get_obj I pt p
853 val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p
854 val tac = Ctree.g_tac ppobj
855 in (f, SOME tac, []) end
858 (** get the formula from a ctree-node **)
860 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
861 take res from all other PrfObj's
862 Designed for interSteps, outcommented 04 in favour of calcChangedEvent
864 fun formres p (Ctree.Nd (Ctree.PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
865 [("headline", (p, Pos.Frm), h), ("stepform", (p, Pos.Res), r)]
866 | formres p (Ctree.Nd (Ctree.PrfObj {form, result = (r, _), ...}, _)) =
867 [("stepform", (p, Pos.Frm), form), ("stepform", (p, Pos.Res), r)]
868 | formres _ _ = raise ERROR "formres: uncovered definition"
869 fun form p (Ctree.Nd (Ctree.PrfObj {result = (r, _), ...}, _)) =
870 [("stepform", (p, Pos.Res), r)]
871 | form _ _ = raise ERROR "form: uncovered definition"
873 (* assumes to take whole level, in particular hd -- for use in interSteps *)
874 fun get_formress fs _ [] = flat fs
875 | get_formress fs p (nd::nds) =
876 (* start with 'form+res' and continue with trying 'res' only*)
877 get_forms (fs @ [formres p nd]) (Pos.lev_on p) nds
878 and get_forms fs _ [] = flat fs
879 | get_forms fs p (nd::nds) =
881 (* start again with 'form+res' ///ugly repeat with Check_elementwise
882 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
883 then get_forms (fs @ [formres p nd]) (Pos.lev_on p) nds
884 (* continue with trying 'res' only*)
885 else get_forms (fs @ [form p nd]) (Pos.lev_on p) nds;
888 (** get an 'interval' 'from' 'to' of formulae from a ctree **)
890 (* WN0401 this functionality belongs to ctree.sml *)
891 fun eq_pos' (p1, Pos.Frm) (p2, Pos.Frm) = p1 = p2
892 | eq_pos' (p1, Pos.Res) (p2, Pos.Res) = p1 = p2
893 | eq_pos' (p1, Pos.Pbl) (p2, p2_) =
894 p1 = p2 andalso (case p2_ of Pos.Pbl => true | Pos.Met => true | _ => false)
895 | eq_pos' (p1, Pos.Met) (p2, p2_) =
896 p1 = p2 andalso (case p2_ of Pos.Pbl => true | Pos.Met => true | _ => false)
897 | eq_pos' _ _ = false;
899 (* get an 'interval' from the ctree; 'interval' is w.r.t. the
900 total ordering Position#compareTo(Position p) in the java-code
901 val get_interval = fn :
902 pos' -> : from is "move_up 1st-element" to return
903 pos' -> : to the last element to be returned; from < to
904 int -> : level: 0 gets the flattest sub-tree possible, 999 the deepest
906 (pos' * : of the formula
907 Term.term) : the formula
909 fun get_interval from to level pt =
911 fun get_inter c (from) (to) lev pt =
912 if eq_pos' from to orelse from = ([], Pos.Res)
914 let val (f, tacopt, _) = pt_extract (pt, from)
916 Ctree.ModSpec (_, _, headline, _, _, _) => c @ [(from, headline, NONE)]
917 | Ctree.Form t => c @ [(from, t, tacopt)]
920 if lev < Pos.lev_of from
921 then (get_inter c (Ctree.move_dn [] pt from) to lev pt)
922 handle (Ctree.PTREE _(*from move_dn too far*)) => c
925 val (f, tacopt, _) = pt_extract (pt, from)
927 Ctree.ModSpec (_,_,headline,_,_,_) => headline
929 in (get_inter (c @ [(from, term, tacopt)]) (Ctree.move_dn [] pt from) to lev pt)
930 handle (Ctree.PTREE _(*from move_dn too far*)) => c @ [(from, term, tacopt)]
932 in get_inter [] from to level pt end
934 fun posterm2str (pos, t, _) = "(" ^ Pos.pos'2str pos ^ ", " ^ UnparseC.term t ^ ")"
935 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
937 fun postermtac2str (pos, t, SOME tac) =
938 Pos.pos'2str pos ^ ", " ^ UnparseC.term t ^ "\n" ^ indent 10 ^ Tactic.input_to_string tac
939 | postermtac2str (pos, t, NONE) =
940 Pos.pos'2str pos ^ ", " ^ UnparseC.term t
941 fun postermtacs2str pfts = (strs2str' o (map (curry op ^ "\n")) o (map postermtac2str)) pfts
943 (* WN050225 omits the last step, if pt is incomplete *)
944 fun show_pt pt = tracing (posterms2str (get_interval ([], Pos.Frm) ([], Pos.Res) 99999 pt))
945 fun show_pt_tac pt = tracing (postermtacs2str (get_interval ([], Pos.Frm) ([], Pos.Res) 99999 pt))
947 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
948 fun get_ocalhd (pt, (p, Pos.Pbl)) =
950 val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
951 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
952 | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj"
953 val {prls, where_, ...} = Problem.from_store (#2 (some_spec ospec spec))
954 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl
956 (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
958 | get_ocalhd (pt, (p, Pos.Met)) =
960 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
961 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
962 | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj"
963 val {prls, pre, ...} = Method.from_store (#3 (some_spec ospec spec))
964 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth
966 (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
968 | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition"
970 (* at the activeFormula set the Specification
971 to empty and return a CalcHead;
972 the 'origin' remains (for reconstructing all that) *)
973 fun reset_calchead (pt, (p,_)) =
975 val () = case Ctree.get_obj I pt p of
977 | _ => raise ERROR "reset_calchead: uncovered case get_obj"
978 val pt = Ctree.update_pbl pt p []
979 val pt = Ctree.update_met pt p []
980 val pt = Ctree.update_spec pt p References.empty
981 in (pt, (p, Pos.Pbl)) end