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 =
69 type T = Specification_Def.T
70 val nxt_spec : Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
71 (string * (term * 'a)) list * (string * (term * 'b)) list -> References.T -> Pos.pos_ * Tactic.input
73 val reset_calchead : Calc.T -> Calc.T
74 val get_ocalhd : Calc.T -> T
75 val ocalhd_complete : I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
76 val all_modspec : Calc.T -> Calc.T
78 val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T
79 val insert_ppc' : I_Model.single -> I_Model.T -> I_Model.T
81 val complete_mod : Calc.T -> Calc.T
82 val is_complete_mod : Calc.T -> bool
83 val complete_spec : Calc.T -> Calc.T
84 val is_complete_spec : Calc.T -> bool
85 val some_spec : References.T -> References.T -> References.T
86 (* these could go to Ctree ..*)
87 val show_pt : Ctree.ctree -> unit
88 val show_pt_tac : Ctree.ctree -> unit
89 val pt_extract : Calc.T -> Ctree.ptform * Tactic.input option * term list
90 val get_interval : Pos.pos' -> Pos.pos' -> int -> Ctree.ctree -> (Pos.pos' * term * Tactic.input option) list
92 val match_ags : theory -> Model_Pattern.T -> term list -> O_Model.T
93 val match_ags_msg : Problem.id -> term -> term list -> unit
94 val oris2fmz_vals : O_Model.T -> string list * term list
95 val vars_of_pbl_' : Model_Pattern.T -> term list
97 val ppc2list : 'a P_Model.ppc -> 'a list
99 val itm_out : theory -> I_Model.feedback -> string
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 -> Model_Pattern.T -> I_Model.T -> (string * string) option
103 val is_error: I_Model.feedback -> bool
104 val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T ->
105 I_Model.T * I_Model.T
106 val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> calcstate'
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: Model_Pattern.single -> bool
117 val is_copy_named: Model_Pattern.single -> bool
118 val ori2Coritm: Model_Pattern.T -> O_Model.single -> I_Model.single
119 val matc: theory -> Model_Pattern.T -> 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 val get: Calc.T -> I_Model.T * O_Model.T * ThyC.id * References.id * References.id *
123 I_Model.T * ThyC.id * References.id * References.id * Proof.context
124 val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
125 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
127 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
128 val variants_in : term list -> int
129 val is_untouched : I_Model.single -> bool
130 val is_list_type : typ -> bool
131 val parse_ok : I_Model.feedback list -> bool
132 val all_dsc_in : I_Model.feedback list -> term list
133 val chktyps : theory -> term list * term list -> term list (* only in old tests*)
134 val is_complete_modspec : Calc.T -> bool
135 val get_formress : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
136 (string * Pos.pos' * term) list
137 val get_forms : (string * Pos.pos' * term) list list -> Pos.pos -> Ctree.ctree list ->
138 (string * Pos.pos' * term) list
142 structure Specification(**): SPECIFICATION(**) =
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 = ((Ctree.EmptyPtree, Pos.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.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], [Pos.e_pos'], (Ctree.EmptyPtree, Pos.e_pos')) : calcstate';
178 type T = Specification_Def.T;
180 (* is the calchead complete ? *)
181 fun ocalhd_complete its pre (dI, pI, mI) =
182 foldl and_ (true, map #3 (its: I_Model.T)) andalso
183 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
184 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
186 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
187 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
188 fun oris2fmz_vals oris =
189 let fun ori2fmz_vals (_, _, _, dsc, ts) =
190 ((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts)
191 handle _ => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
192 in (split_list o (map ori2fmz_vals)) oris end
194 fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
195 gis @ whs @ fis @ wis @ res
197 (* get the number of variants in a problem in 'original',
198 assumes equal descriptions in immediate sequence *)
201 fun eq (x, y) = head_of x = head_of y
202 fun cnt _ [] _ n = ([n], [])
203 | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
204 fun coll _ xs [] = xs
205 | coll eq xs (y :: ys) =
206 let val (n, ys') = cnt eq (y :: ys) y 0
207 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
208 val vts = subtract op = [1] (distinct (coll eq [] ts))
213 | _ => raise ERROR "different variants in formalization"
216 fun is_list_type (Type ("List.list", _)) = true
217 | is_list_type _ = false
218 fun is_parsed (I_Model.Syn _) = false
220 fun parse_ok its = foldl and_ (true, map is_parsed its)
222 fun all_dsc_in itm_s =
224 fun d_in (I_Model.Cor ((d, _), _)) = [d]
225 | d_in (I_Model.Syn _) = []
226 | d_in (I_Model.Typ _) = []
227 | d_in (I_Model.Inc ((d,_),_)) = [d]
228 | d_in (I_Model.Sup (d,_)) = [d]
229 | d_in (I_Model.Mis (d,_)) = [d]
230 | d_in i = raise ERROR ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
231 in (flat o (map d_in)) itm_s end;
233 fun is_error (I_Model.Cor _) = false
234 | is_error (I_Model.Sup _) = false
235 | is_error (I_Model.Inc _) = false
236 | is_error (I_Model.Mis _) = false
239 (* get the first term in ts from ori *)
240 fun getr_ct thy (_, _, fd, d, ts) =
241 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
243 (* get a term from ori, notyet input in itm.
244 the term from ori is thrown back to a string in order to reuse
245 machinery for immediate input by the user. *)
246 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
247 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))
249 (* in FE dsc, not dat: this is in itms ...*)
250 fun is_untouched (_, _, false, _, I_Model.Inc ((_, []), _)) = true
251 | is_untouched _ = false
253 (* select an item in oris, notyet input in itms
254 (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc) *)
257 oris: from formalization 'type fmz', structured for efficient access
258 pbt : the problem-pattern to be matched with oris in order to get itms
259 itms: already input items
261 fun nxt_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
263 fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0
264 fun is_elem itms (_, (d, _)) =
265 case find_first (test_d d) itms of SOME _ => true | NONE => false
267 case filter_out (is_elem itms) pbt of
268 (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))
271 | nxt_add thy oris _ itms =
273 fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
274 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
275 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
276 fun test_subset itm (_, _, _, d, ts) =
277 (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
278 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
279 | false_and_not_Sup (_, _, false, _, _) = true
280 | false_and_not_Sup _ = false
281 val v = if itms = [] then 1 else I_Model.max_vt itms
282 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
285 then itms (* because of dsc without dat *)
286 else filter (testi_vt v) itms; (* itms..vat *)
287 val icl = filter false_and_not_Sup vits; (* incomplete *)
290 then case filter_out (test_id (map #1 vits)) vors of
292 | miss => SOME (getr_ct thy (hd miss))
294 case find_first (test_subset (hd icl)) vors of
295 NONE => raise ERROR "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
296 | SOME ori => SOME (geti_ct thy ori (hd icl))
299 (*create output-string for itm_*)
300 fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
301 | itm_out _ (I_Model.Syn c) = c
302 | itm_out _ (I_Model.Typ c) = c
303 | itm_out _ (I_Model.Inc ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
304 | itm_out _ (I_Model.Sup (d, ts)) = UnparseC.term (Input_Descript.join (d, ts))
305 | itm_out _ (I_Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
306 | itm_out _ _ = raise ERROR "itm_out: uncovered definition"
308 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (itm_out thy itm_)
309 | mk_delete thy "#Find" itm_ = Tactic.Del_Find (itm_out thy itm_)
310 | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (itm_out thy itm_)
311 | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
312 fun mk_additem "#Given" ct = Tactic.Add_Given ct
313 | mk_additem "#Find" ct = Tactic.Add_Find ct
314 | mk_additem "#Relate"ct = Tactic.Add_Relation ct
315 | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")
317 (* determine the next step of specification;
318 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
319 eg. in rootpbl 'no_met':
321 preok predicates are _all_ ok (and problem matches completely)
322 oris immediately from formalization
323 (dI',pI',mI') specification coming from author/parent-problem
324 (pbl, item lists specified by user
325 met) -"-, tacitly completed by copy_probl
326 (dI,pI,mI) specification explicitly done by the user
327 (pbt, mpc) problem type, guard of method
329 fun nxt_spec Pos.Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
330 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
331 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
333 case find_first (is_error o #5) pbl of
334 SOME (_, _, _, fd, itm_) =>
335 (Pos.Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
337 (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
338 SOME (fd, ct') => (Pos.Pbl, mk_additem fd ct')
339 | NONE => (*pbl-items complete*)
340 if not preok then (Pos.Pbl, Tactic.Refine_Problem pI')
341 else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
342 else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
343 else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')
345 case find_first (is_error o #5) met of
346 SOME (_, _, _, fd, itm_) => (Pos.Met, mk_delete (ThyC.get_theory dI) fd itm_)
348 (case nxt_add (ThyC.get_theory dI) oris mpc met of
349 SOME (fd, ct') => (Pos.Met, mk_additem fd ct') (*30.8.01: pre?!?*)
350 | NONE => (Pos.Met, Tactic.Apply_Method mI))))
351 | nxt_spec Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
352 (case find_first (is_error o #5) met of
353 SOME (_,_,_,fd,itm_) => (Pos.Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
355 case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
356 SOME (fd,ct') => (Pos.Met, mk_additem fd ct')
358 (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI')
359 else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI')
360 else if not preok then (Pos.Met, Tactic.Specify_Method mI)
361 else (Pos.Met, Tactic.Apply_Method mI)))
362 | nxt_spec p _ _ _ _ _ _ = raise ERROR ("nxt_spec: uncovered case with " ^ Pos.pos_2str p)
364 (* make oris from args of the stac SubProblem and from pbt.
365 can this formal argument (of a model-pattern) be omitted in the arg-list
366 of a SubProblem ? see calcelems.sml 'type met ' *)
367 fun is_copy_named_idstr str =
368 case (rev o Symbol.explode) str of
369 "'" :: _ :: "'" :: _ => true
371 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t
373 (* should this formal argument (of a model-pattern) create a new identifier? *)
374 fun is_copy_named_generating_idstr str =
375 if is_copy_named_idstr str
377 case (rev o Symbol.explode) str of
378 "'" :: "'" :: "'" :: _ => false
381 fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t
383 (* split type-wrapper from scr-arg and build part of an ori;
384 an type-error is reported immediately, raises an exn,
385 subsequent handling of exn provides 2nd part of error message *)
386 fun mtc thy (str, (dsc, _)) (ty $ var) =
387 ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
388 SOME (([1], str, dsc, (*[var]*)
389 Input_Descript.split' (dsc, var))) (*:ori without leading #*))
390 handle e as TYPE _ =>
391 (tracing (dashs 70 ^ "\n"
392 ^ "*** ERROR while creating the items for the model of the ->problem\n"
393 ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
394 ^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"
395 ^ "*** description: " ^ TermC.term_detail2str dsc
396 ^ "*** value: " ^ TermC.term_detail2str var
397 ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
398 ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"
400 writeln (@{make_string} e);
401 Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
403 | mtc _ _ t = raise ERROR ("mtc: uncovered case with" ^ UnparseC.term t)
405 (* match each pat of the model-pattern with an actual argument;
406 precondition: copy-named vars are filtered out *)
407 fun matc _ [] _ oris = oris
410 raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
411 | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
412 (*del?..*)if (is_copy_named_idstr o TermC.free2str) t then oris
414 let val opt = mtc thy p a
417 SOME ori => matc thy pbt ags (oris @ [ori])
418 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
421 (* generate a new variable "x_i" name from a related given one "x"
422 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
423 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
424 but leave is_copy_named_generating as is, e.t. ss''' *)
425 fun cpy_nam pbt oris (p as (field, (dsc, t))) =
426 (if is_copy_named_generating p
427 then (*WN051014 kept strange old code ...*)
428 let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts)
429 val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
430 val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
431 val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
432 val vals = map sel oris
433 val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
434 in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
435 else ([1], field, dsc, [t])
436 ) handle _ => raise ERROR ("cpy_nam: for "^ UnparseC.term t)
438 (* match the actual arguments of a SubProblem with a model-pattern
439 and create an ori list (in root-pbl created from formalization).
440 expects ags:pats = 1:1, while copy-named are filtered out of pats;
441 if no 1:1 then exn raised by matc/mtc and handled at call.
442 copy-named pats are appended in order to get them into the model-items *)
443 fun match_ags thy pbt ags =
445 fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
446 val pbt' = filter_out is_copy_named pbt
447 val cy = filter is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *)
448 val oris' = matc thy pbt' ags []
449 val cy' = map (cpy_nam pbt' oris') cy
450 val ors = O_Model.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
451 in (map flattup ors) end
453 (* report part of the error-msg which is not available in match_args *)
454 fun match_ags_msg pI stac ags =
456 val pats = (#ppc o Problem.from_store) pI
457 val msg = (dots 70 ^ "\n"
458 ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
459 ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
460 ^ "*** stac '" ^ UnparseC.term stac ^ "' has the ...\n"
461 ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"
463 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
466 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
467 fun vars_of_pbl_' pbl_ =
469 fun var_of_pbl_ (_, (_, t)) = t: term
470 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
472 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (I_Model.d_in itm_ = I_Model.d_in iitm_)
474 (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
475 handles superfluous items carelessly *)
476 fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
478 (* output the headline to a ppc *)
479 fun header p_ pI mI =
481 Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI)
482 | Pos.Met => Test_Out.Method mI
483 | pos => raise ERROR ("header called with "^ Pos.pos_2str pos)
485 fun make m_field (term_as_string, i_model) =
487 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
488 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
489 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
490 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
491 fun get (pt, (p, _)) =
492 case Ctree.get_obj I pt p of
493 (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
494 => (meth, oris, dI', pI', mI', probl, dI, pI, mI, ctxt)
495 | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
496 fun specify_additem sel ct (pt, pos as (p, Pos.Met)) =
498 val (met, oris, dI', pI', mI', pbl, dI, pI, mI, ctxt) = get (pt, pos)
499 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
500 val cpI = if pI = Problem.id_empty then pI' else pI
501 val cmI = if mI = Method.id_empty then mI' else mI
502 val {ppc, pre, prls, ...} = Method.from_store cmI
504 case I_Model.check_single ctxt sel oris met ppc ct of
505 I_Model.Add itm => (*..union old input *)
507 val met' = I_Model.add_single thy itm met
509 case Specify_Step.add (make sel (ct, met')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
510 ((p, Pos.Met), _, _, pt') => (p, pt')
511 | _ => raise ERROR "specify_additem: uncovered case of generate1"
512 val pre' = Pre_Conds.check' thy prls pre met'
513 val pb = foldl and_ (true, map fst pre')
515 nxt_spec Pos.Met pb oris (dI',pI',mI') (pbl,met')
516 ((#ppc o Problem.from_store) cpI,ppc) (dI,pI,mI);
518 ("ok", ([], [], (pt', (p, p_))))
522 val pre' = Pre_Conds.check' thy prls pre met
523 val pb = foldl and_ (true, map fst pre')
525 nxt_spec Pos.Met pb oris (dI',pI',mI') (pbl,met)
526 ((#ppc o Problem.from_store) cpI,(#ppc o Method.from_store) cmI) (dI,pI,mI);
528 (msg, ([], [], (pt, (p, p_))))
531 | specify_additem sel ct (pt, pos as (p, _(*Frm, Pbl*))) =
533 val (met, oris, dI', pI', mI', pbl, dI, pI, mI, ctxt) = get (pt, pos)
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
536 val cmI = if mI = Method.id_empty then mI' else mI
537 val {ppc, where_, prls, ...} = Problem.from_store cpI
539 case I_Model.check_single ctxt sel oris pbl ppc ct of
540 I_Model.Add itm => (*..union old input *)
542 val pbl' = I_Model.add_single thy itm pbl
544 case Specify_Step.add (make sel (ct, pbl')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
545 ((p, Pos.Pbl), _, _, pt') => (p, pt')
546 | _ => raise ERROR "specify_additem: uncovered case of Specify_Step.add"
547 (* only for getting final p_ ..*)
548 val pre = Pre_Conds.check' thy prls where_ pbl';
549 val pb = foldl and_ (true, map fst pre);
551 nxt_spec Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
553 ("ok", ([], [], (pt', (p, p_))))
557 val pre = Pre_Conds.check' thy prls where_ pbl
558 val pb = foldl and_ (true, map fst pre)
559 val (p_, _(*Tactic.input*)) =
560 nxt_spec Pos.Pbl pb oris (dI', pI', mI') (pbl, met)
561 (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)
563 (msg, ([], [], (pt, (p, p_))))
567 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
568 -- for input from scratch*)
569 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pos.Pbl))) =
571 val (oris, dI', pI', dI, pI, pbl, ctxt) = case Ctree.get_obj I pt p of
572 Ctree.PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
573 (oris, dI', pI', dI, pI, pbl, ctxt)
574 | _ => raise ERROR "specify (Specify_Theory': uncovered case get_obj"
575 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
576 val cpI = if pI = Problem.id_empty then pI' else pI;
578 case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of
579 I_Model.Add itm (*..union old input *) =>
581 val pbl' = I_Model.add_single thy itm pbl
582 val (tac, tac_) = case sel of
583 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, pbl'))
584 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, pbl'))
585 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))
586 | sel => raise ERROR ("nxt_specif_additem: uncovered case of" ^ sel)
588 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
589 ((p, Pos.Pbl), c, _, pt') => (p, c, pt')
590 | _ => raise ERROR "nxt_specif_additem: uncovered case generate1"
592 ([(tac, tac_, ((p, Pos.Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Pbl)))
594 | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..
595 FIXME ..and dont abuse a tactic for that purpose*)
596 ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),
597 (Pos.e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
599 | nxt_specif_additem sel ct (ptp as (pt, (p, Pos.Met))) =
601 val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of
602 Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
603 (oris, dI', mI', dI, mI, met, ctxt)
604 | _ => raise ERROR "nxt_specif_additem Met: uncovered case get_obj"
605 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
606 val cmI = if mI = Method.id_empty then mI' else mI;
608 case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of
609 I_Model.Add itm (*..union old input *) =>
611 val met' = I_Model.add_single thy itm met;
612 val (tac,tac_) = case sel of
613 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, met'))
614 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, met'))
615 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))
616 | sel => raise ERROR ("nxt_specif_additem Met: uncovered case of" ^ sel)
618 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
619 ((p, Pos.Met), c, _, pt') => (p, c, pt')
620 | _ => raise ERROR "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
622 ([(tac, tac_, ((p, Pos.Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Met)))
624 | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
626 | nxt_specif_additem _ _ (_, p) = raise ERROR ("nxt_specif_additem not impl. for" ^ Pos.pos'2str p)
628 fun ori2Coritm pbt (i, v, f, d, ts) =
629 (i, v, true, f, I_Model.Cor ((d, ts), ((snd o snd o the o (find_first (I_Model.eq1 d))) pbt, ts)))
630 handle _ => (i, v, true, f, I_Model.Cor ((d, ts), (d, ts)))
631 (*dsc in oris, but not in pbl pat list: keep this dsc*)
633 (* filter out oris which have same description in itms *)
634 fun filter_outs oris [] = oris
635 | filter_outs oris (i::itms) =
637 val ors = filter_out ((curry op = ((I_Model.d_in o #5) i)) o (#4)) oris
642 (* filter oris which are in pbt, too *)
643 fun filter_pbt oris pbt =
645 val dscs = map (fst o snd) pbt
647 filter ((member op= dscs) o (#4)) oris
650 (* combine itms from pbl + met and complete them wrt. pbt *)
651 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
652 fun complete_metitms oris pits mits met =
654 val vat = I_Model.max_vt pits;
655 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
656 val ors = filter ((member_swap op= vat) o (#2)) oris
657 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
659 itms @ (map (ori2Coritm met) os)
662 (* complete model and guard of a calc-head *)
663 fun complete_mod_ (oris, mpc, ppc, probl) =
665 val pits = filter_out ((curry op= false) o (#3)) probl
666 val vat = if probl = [] then 1 else I_Model.max_vt probl
667 val pors = filter ((member_swap op = vat) o (#2)) oris
668 val pors = filter_outs pors pits (*which are in pbl already*)
669 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
670 val pits = pits @ (map (ori2Coritm ppc) pors)
671 val mits = complete_metitms oris pits [] mpc
674 fun some_spec (odI, opI, omI) (dI, pI, mI) =
675 (if dI = ThyC.id_empty then odI else dI,
676 if pI = Problem.id_empty then opI else pI,
677 if mI = Method.id_empty then omI else mI)
679 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
680 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
681 fun tag_form thy (formal, given) =
683 val gf = (head_of given) $ formal;
684 val _ = Thm.global_cterm_of thy gf
686 handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^
687 " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")
689 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
691 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
692 + met from fmz; assumes pos on PblObj, meth = [] *)
693 fun complete_mod (pt, pos as (p, p_)) =
695 val _ = if p_ <> Pos.Pbl
696 then raise ERROR ("###complete_mod: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
698 val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of
699 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
700 | _ => raise ERROR "complete_mod: unvered case get_obj"
701 val (_, pI, mI) = some_spec ospec spec
702 val mpc = (#ppc o Method.from_store) mI
703 val ppc = (#ppc o Problem.from_store) pI
704 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
705 val pt = Ctree.update_pblppc pt p pits
706 val pt = Ctree.update_metppc pt p mits
707 in (pt, (p, Pos.Met)) end
709 (* do all specification in one single step:
710 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
711 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
713 fun all_modspec (pt, (p, _)) =
715 val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of
716 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}
717 => (pors, dI, pI, mI)
718 | _ => raise ERROR "all_modspec: uncovered case get_obj"
719 val {ppc, ...} = Method.from_store mI
720 val (_, vals) = oris2fmz_vals pors
721 val ctxt = ContextC.initialise dI vals
722 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
723 map (ori2Coritm ppc) pors, map (ori2Coritm ppc) pors, ctxt)
728 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
729 fun is_complete_mod_ [] = false
730 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
732 fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =
733 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
734 then (is_complete_mod_ o (Ctree.get_obj Ctree.g_pbl pt)) p
735 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
736 | is_complete_mod (pt, pos as (p, Pos.Met)) =
737 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
738 then (is_complete_mod_ o (Ctree.get_obj Ctree.g_met pt)) p
739 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
740 | is_complete_mod (_, pos) =
741 raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
743 (* have (thy, pbl, met) _all_ been specified explicitly ? *)
744 fun is_complete_spec (pt, pos as (p, _)) =
745 if (not o Ctree.is_pblobj o (Ctree.get_obj I pt)) p
746 then raise ERROR ("is_complete_spec: called by PrfObj at " ^ Pos.pos'2str pos)
748 let val (dI,pI,mI) = Ctree.get_obj Ctree.g_spec pt p
749 in dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty end
751 (* complete empty items in specification from origin (pbl, met ev.refined);
752 assumes 'is_complete_mod' *)
753 fun complete_spec (pt, pos as (p, _)) =
755 val (ospec, spec) = case Ctree.get_obj I pt p of
756 Ctree.PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
757 | _ => raise ERROR "complete_spec: uncovered case get_obj"
758 val pt = Ctree.update_spec pt p (some_spec ospec spec)
763 fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
765 fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ...}) Pos.Met =
767 val (_, _, metID) = Ctree.get_somespec' spec spec'
768 val pre = if metID = Method.id_empty then []
771 val {prls, pre= where_, ...} = Method.from_store metID
772 val pre = Pre_Conds.check prls where_ meth 0
774 val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
776 Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, pre, spec)
778 | pt_model (Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
780 val (_, pI, _) = Ctree.get_somespec' spec spec'
781 val pre = if pI = Problem.id_empty then []
784 val {prls, where_, ...} = Problem.from_store pI
785 val pre = Pre_Conds.check prls where_ probl 0
787 val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
789 Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, pre, spec)
791 | pt_model _ _ = raise ERROR "pt_model: uncovered definition"
793 fun pt_form (Ctree.PrfObj {form, ...}) = Ctree.Form form
794 | pt_form (Ctree.PblObj {probl, spec, origin = (_, spec', _), ...}) =
796 val (dI, pI, _) = Ctree.get_somespec' spec spec'
797 val {cas, ...} = Problem.from_store pI
799 NONE => Ctree.Form (Auto_Prog.pblterm dI pI)
800 | SOME t => Ctree.Form (subst_atomic (I_Model.mk_env probl) t)
803 (* pt_extract returns
805 # the tactic applied to this formula
806 # the list of assumptions generated at this formula
807 (by application of another tac to the preceding formula !)
808 pos is assumed to come from the frontend, ie. generated by moveDown.
809 Notes: cannot be in ctree.sml, because ModSpec has to be calculated.
810 TODO 110417 get assumptions from ctxt !?
812 fun pt_extract (pt, ([], Pos.Res)) =
813 (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)
815 val (f, asm) = Ctree.get_obj Ctree.g_result pt []
816 in (Ctree.Form f, NONE, asm) end
817 | pt_extract (pt, (p, Pos.Res)) =
819 val (f, asm) = Ctree.get_obj Ctree.g_result pt p
821 if Ctree.last_onlev pt p
823 if Ctree.is_pblobj' pt (Pos.lev_up p)
826 val pI = case Ctree.get_obj I pt (Pos.lev_up p) of
827 Ctree.PblObj{spec = (_, pI, _), ...} => pI
828 | _ => raise ERROR "pt_extract last_onlev: uncovered case get_obj"
829 in if pI = Problem.id_empty then NONE else SOME (Tactic.Check_Postcond pI) end
830 else SOME Tactic.End_Trans (* WN0502 TODO for other branches *)
832 let val p' = Pos.lev_on p
834 if Ctree.is_pblobj' pt p'
837 val (dI , pI) = case Ctree.get_obj I pt p' of
838 Ctree.PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)
839 | _ => raise ERROR "pt_extract \<not>last_onlev: uncovered case get_obj"
840 in SOME (Tactic.Subproblem (dI, pI)) end
842 if f = Ctree.get_obj Ctree.g_form pt p'
843 then SOME (Ctree.get_obj Ctree.g_tac pt p') (*because this Frm ~~~is not on worksheet*)
844 else SOME (Tactic.Take (UnparseC.term (Ctree.get_obj Ctree.g_form pt p')))
846 in (Ctree.Form f, tac, asm) end
847 | pt_extract (pt, (p, p_(*Frm,Pbl*))) =
849 val ppobj = Ctree.get_obj I pt p
850 val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p
851 val tac = Ctree.g_tac ppobj
852 in (f, SOME tac, []) end
855 (** get the formula from a ctree-node **)
857 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
858 take res from all other PrfObj's
859 Designed for interSteps, outcommented 04 in favour of calcChangedEvent
861 fun formres p (Ctree.Nd (Ctree.PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
862 [("headline", (p, Pos.Frm), h), ("stepform", (p, Pos.Res), r)]
863 | formres p (Ctree.Nd (Ctree.PrfObj {form, result = (r, _), ...}, _)) =
864 [("stepform", (p, Pos.Frm), form), ("stepform", (p, Pos.Res), r)]
865 | formres _ _ = raise ERROR "formres: uncovered definition"
866 fun form p (Ctree.Nd (Ctree.PrfObj {result = (r, _), ...}, _)) =
867 [("stepform", (p, Pos.Res), r)]
868 | form _ _ = raise ERROR "form: uncovered definition"
870 (* assumes to take whole level, in particular hd -- for use in interSteps *)
871 fun get_formress fs _ [] = flat fs
872 | get_formress fs p (nd::nds) =
873 (* start with 'form+res' and continue with trying 'res' only*)
874 get_forms (fs @ [formres p nd]) (Pos.lev_on p) nds
875 and get_forms fs _ [] = flat fs
876 | get_forms fs p (nd::nds) =
878 (* start again with 'form+res' ///ugly repeat with Check_elementwise
879 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
880 then get_forms (fs @ [formres p nd]) (Pos.lev_on p) nds
881 (* continue with trying 'res' only*)
882 else get_forms (fs @ [form p nd]) (Pos.lev_on p) nds;
885 (** get an 'interval' 'from' 'to' of formulae from a ctree **)
887 (* WN0401 this functionality belongs to ctree.sml *)
888 fun eq_pos' (p1, Pos.Frm) (p2, Pos.Frm) = p1 = p2
889 | eq_pos' (p1, Pos.Res) (p2, Pos.Res) = p1 = p2
890 | eq_pos' (p1, Pos.Pbl) (p2, p2_) =
891 p1 = p2 andalso (case p2_ of Pos.Pbl => true | Pos.Met => true | _ => false)
892 | eq_pos' (p1, Pos.Met) (p2, p2_) =
893 p1 = p2 andalso (case p2_ of Pos.Pbl => true | Pos.Met => true | _ => false)
894 | eq_pos' _ _ = false;
896 (* get an 'interval' from the ctree; 'interval' is w.r.t. the
897 total ordering Position#compareTo(Position p) in the java-code
898 val get_interval = fn :
899 pos' -> : from is "move_up 1st-element" to return
900 pos' -> : to the last element to be returned; from < to
901 int -> : level: 0 gets the flattest sub-tree possible, 999 the deepest
903 (pos' * : of the formula
904 Term.term) : the formula
906 fun get_interval from to level pt =
908 fun get_inter c (from) (to) lev pt =
909 if eq_pos' from to orelse from = ([], Pos.Res)
911 let val (f, tacopt, _) = pt_extract (pt, from)
913 Ctree.ModSpec (_, _, headline, _, _, _) => c @ [(from, headline, NONE)]
914 | Ctree.Form t => c @ [(from, t, tacopt)]
917 if lev < Pos.lev_of from
918 then (get_inter c (Ctree.move_dn [] pt from) to lev pt)
919 handle (Ctree.PTREE _(*from move_dn too far*)) => c
922 val (f, tacopt, _) = pt_extract (pt, from)
924 Ctree.ModSpec (_,_,headline,_,_,_) => headline
926 in (get_inter (c @ [(from, term, tacopt)]) (Ctree.move_dn [] pt from) to lev pt)
927 handle (Ctree.PTREE _(*from move_dn too far*)) => c @ [(from, term, tacopt)]
929 in get_inter [] from to level pt end
931 fun posterm2str (pos, t, _) = "(" ^ Pos.pos'2str pos ^ ", " ^ UnparseC.term t ^ ")"
932 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
934 fun postermtac2str (pos, t, SOME tac) =
935 Pos.pos'2str pos ^ ", " ^ UnparseC.term t ^ "\n" ^ indent 10 ^ Tactic.input_to_string tac
936 | postermtac2str (pos, t, NONE) =
937 Pos.pos'2str pos ^ ", " ^ UnparseC.term t
938 fun postermtacs2str pfts = (strs2str' o (map (curry op ^ "\n")) o (map postermtac2str)) pfts
940 (* WN050225 omits the last step, if pt is incomplete *)
941 fun show_pt pt = tracing (posterms2str (get_interval ([], Pos.Frm) ([], Pos.Res) 99999 pt))
942 fun show_pt_tac pt = tracing (postermtacs2str (get_interval ([], Pos.Frm) ([], Pos.Res) 99999 pt))
944 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
945 fun get_ocalhd (pt, (p, Pos.Pbl)) =
947 val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
948 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
949 | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj"
950 val {prls, where_, ...} = Problem.from_store (#2 (some_spec ospec spec))
951 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl
953 (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
955 | get_ocalhd (pt, (p, Pos.Met)) =
957 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
958 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
959 | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj"
960 val {prls, pre, ...} = Method.from_store (#3 (some_spec ospec spec))
961 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth
963 (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
965 | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition"
967 (* at the activeFormula set the Specification
968 to empty and return a CalcHead;
969 the 'origin' remains (for reconstructing all that) *)
970 fun reset_calchead (pt, (p,_)) =
972 val () = case Ctree.get_obj I pt p of
974 | _ => raise ERROR "reset_calchead: uncovered case get_obj"
975 val pt = Ctree.update_pbl pt p []
976 val pt = Ctree.update_met pt p []
977 val pt = Ctree.update_spec pt p References.empty
978 in (pt, (p, Pos.Pbl)) end