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 interprete 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, interprete 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, interprete 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.
71 datatype appl = Appl of Tactic.T | Notappl of string
72 val nxt_specify_init_calc : Selem.fmz -> calcstate
73 val specify : Tactic.T -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
74 Ctree.pos' * (Ctree.pos' * Istate.T) * Generate.mout * Tactic.input * Istate.safe * Ctree.ctree
75 val nxt_specif : Tactic.input -> Ctree.state -> calcstate'
76 val nxt_spec : Ctree.pos_ -> bool -> Model.ori list -> Celem.spec -> Model.itm list * Model.itm list ->
77 (string * (term * 'a)) list * (string * (term * 'b)) list -> Celem.spec -> Ctree.pos_ * Tactic.input
79 val reset_calchead : Ctree.state -> Ctree.state
80 val get_ocalhd : Ctree.state -> Ctree.ocalhd
81 val ocalhd_complete : Model.itm list -> (bool * term) list -> Rule.domID * Celem.pblID * Celem.metID -> bool
82 val all_modspec : Ctree.state -> Ctree.state
84 val complete_metitms : Model.ori list -> Model.itm list -> Model.itm list -> Celem.pat list -> Model.itm list
85 val insert_ppc' : Model.itm -> Model.itm list -> Model.itm list
87 val complete_mod : Ctree.state -> Ctree.state
88 val is_complete_mod : Ctree.state -> bool
89 val complete_spec : Ctree.state -> Ctree.state
90 val is_complete_spec : Ctree.state -> bool
91 val some_spec : Celem.spec -> Celem.spec -> Celem.spec
92 (* these could go to Ctree ..*)
93 val show_pt : Ctree.ctree -> unit
94 val show_pt_tac : Ctree.ctree -> unit
95 val pt_extract : Ctree.state -> Ctree.ptform * Tactic.input option * term list
96 val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term * Tactic.input option) list
98 val match_ags : theory -> Celem.pat list -> term list -> Model.ori list
99 val match_ags_msg : Celem.pblID -> term -> term list -> unit
100 val oris2fmz_vals : Model.ori list -> string list * term list
101 val vars_of_pbl_' : ('a * ('b * term)) list -> term list
102 val is_known : Proof.context -> string -> Model.ori list -> term -> string * Model.ori * term list
103 val is_notyet_input : Proof.context -> Model.itm list -> term list -> Model.ori -> ('a * (term * term)) list
104 -> string * Model.itm
105 val ppc2list : 'a Model.ppc -> 'a list
106 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
107 val e_calcstate : Ctree.state * Generate.taci list
108 val e_calcstate' : calcstate'
109 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
110 val posterms2str : (pos' * term * 'a) list -> string
111 val postermtacs2str : (pos' * term * Tactic.input option) list -> string
112 val vals_of_oris : Model.ori list -> term list
113 val is_error : Model.itm_ -> bool
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 : Celem.pat list -> Model.ori -> Model.itm
119 val matc : theory -> (string * (term * term)) list -> term list -> Model.preori list -> Model.preori list
120 val mtc : theory -> Celem.pat -> term -> Model.preori option
121 val cpy_nam : Celem.pat list -> Model.preori list -> Celem.pat -> Model.preori
122 datatype additm = Add of Model.itm | Err of string
123 val appl_add: Proof.context -> string -> Model.ori list ->
124 Model.itm list -> (string * (term * term)) list -> Rule.cterm' -> additm
125 val nxt_add: theory -> (int * int list * string * term * term list) list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
126 val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
127 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
129 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
130 val variants_in : term list -> int
131 val is_untouched : Model.itm -> bool
132 val is_list_type : typ -> bool
133 val parse_ok : Model.itm_ list -> bool
134 val all_dsc_in : Model.itm_ list -> term list
135 val chktyps : theory -> term list * term list -> term list (* only in old tests*)
136 val chk_vars : term Model.ppc -> string * term list
137 val unbound_ppc : term Model.ppc -> term list
138 val nxt_model_pbl : Tactic.T -> Ctree.state -> Tactic.T
139 val is_complete_modspec : Ctree.state -> bool
140 val get_formress : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->
141 (string * Ctree.pos' * term) list
142 val get_forms : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->
143 (string * Ctree.pos' * term) list
146 structure Chead(**): CALC_HEAD(**) =
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 (ctree * pos') * (* the calc-state to which the tacis could be applied *)
161 (Generate.taci list) (* ev. several (hidden) steps;
162 in REVERSE order: first tac_ to apply is last_elem *)
163 val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]);
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 Generate.taci list * (* cas. several (hidden) steps;
176 in REVERSE order: first tac_ to apply is last_elem *)
177 pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
178 (ctree * pos') (* the calc-state resulting from the application of tacis *)
179 val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')) : calcstate';
181 (* is the calchead complete ? *)
182 fun ocalhd_complete its pre (dI, pI, mI) =
183 foldl and_ (true, map #3 (its: Model.itm list)) andalso
184 foldl and_ (true, map #1 (pre: (bool * term) list)) andalso
185 dI <> Rule.e_domID andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID
187 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
188 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
189 fun oris2fmz_vals oris =
190 let fun ori2fmz_vals (_, _, _, dsc, ts) =
191 ((Rule.term2str o Model.comp_dts') (dsc, ts), last_elem ts)
192 handle _ => error ("ori2fmz_env called with " ^ Rule.terms2str ts)
193 in (split_list o (map ori2fmz_vals)) oris end
195 (* make a term 'typeless' for comparing with another 'typeless' term;
196 'type-less' usually is illtyped *)
197 fun typeless (Const (s, _)) = (Const (s,Rule.e_type))
198 | typeless (Free (s, _)) = (Free (s,Rule.e_type))
199 | typeless (Var (n, _)) = (Var (n,Rule.e_type))
200 | typeless (Bound i) = (Bound i)
201 | typeless (Abs (s, _,t)) = Abs(s,Rule.e_type, typeless t)
202 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
204 (* to an input (d,ts) find the according ori and insert the ts)
205 WN.11.03: + dont take first inter<>[] *)
206 fun seek_oridts ctxt sel (d, ts) [] =
207 ("seek_oridts: input ('" ^
208 (Rule.term_to_string' ctxt (Model.comp_dts (d, ts))) ^ "') not found in oris (typed)",
211 | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
212 if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
213 then ("", (id, vat, sel, d, inter op = ts ts'), ts')
214 else seek_oridts ctxt sel (d, ts) oris
216 (* to an input (_,ts) find the according ori and insert the ts *)
217 fun seek_orits ctxt _ ts [] =
218 ("seek_orits: input (_, '" ^ strs2str (map (Rule.term_to_string' ctxt) ts) ^
219 "') not found in oris (typed)", Model.e_ori, [])
220 | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: oris) =
221 if sel = sel' andalso (inter op = ts ts') <> []
224 then ("", (id, vat, sel, d, inter op = ts ts'), ts')
225 else (((strs2str' o map (Rule.term_to_string' ctxt)) ts) ^ " not for " ^ sel, Model.e_ori, [])
226 else seek_orits ctxt sel ts oris
228 (* find_first item with #1 equal to id *)
229 fun seek_ppc _ [] = NONE
230 | seek_ppc id (p :: ppc) = if id = #1 (p: Model.itm) then SOME p else seek_ppc id ppc
233 Appl of Tactic.T (* tactic is applicable at a certain position in the Ctree *)
234 | Notappl of string (* tactic is NOT applicable *)
236 fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
237 gis @ whs @ fis @ wis @ res
239 (* get the number of variants in a problem in 'original',
240 assumes equal descriptions in immediate sequence *)
243 fun eq (x, y) = head_of x = head_of y
244 fun cnt _ [] _ n = ([n], [])
245 | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
246 fun coll _ xs [] = xs
247 | coll eq xs (y :: ys) =
248 let val (n, ys') = cnt eq (y :: ys) y 0
249 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
250 val vts = subtract op = [1] (distinct (coll eq [] ts))
255 | _ => error "different variants in formalization"
258 fun is_list_type (Type ("List.list", _)) = true
259 | is_list_type _ = false
260 fun is_parsed (Model.Syn _) = false
262 fun parse_ok its = foldl and_ (true, map is_parsed its)
264 fun all_dsc_in itm_s =
266 fun d_in (Model.Cor ((d, _), _)) = [d]
267 | d_in (Model.Syn _) = []
268 | d_in (Model.Typ _) = []
269 | d_in (Model.Inc ((d,_),_)) = [d]
270 | d_in (Model.Sup (d,_)) = [d]
271 | d_in (Model.Mis (d,_)) = [d]
272 | d_in i = error ("all_dsc_in: uncovered case with " ^ Model.itm_2str i)
273 in (flat o (map d_in)) itm_s end;
275 fun is_error (Model.Cor _) = false
276 | is_error (Model.Sup _) = false
277 | is_error (Model.Inc _) = false
278 | is_error (Model.Mis _) = false
281 (* get the first term in ts from ori *)
282 fun getr_ct thy (_, _, fd, d, ts) =
283 (fd, ((Rule.term_to_string''' thy) o Model.comp_dts) (d,[hd ts]))
285 (* get a term from ori, notyet input in itm.
286 the term from ori is thrown back to a string in order to reuse
287 machinery for immediate input by the user. *)
288 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
289 (fd, ((Rule.term_to_string''' thy) o Model.comp_dts) (d, subtract op = (Model.ts_in itm_) ts))
291 (* in FE dsc, not dat: this is in itms ...*)
292 fun is_untouched (_, _, false, _, Model.Inc ((_, []), _)) = true
293 | is_untouched _ = false
295 (* select an item in oris, notyet input in itms
296 (precondition: in itms are only Model.Cor, Model.Sup, Model.Inc) *)
299 oris: from formalization 'type fmz', structured for efficient access
300 pbt : the problem-pattern to be matched with oris in order to get itms
301 itms: already input items
303 fun nxt_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
305 fun test_d d (i, _, _, _, itm_) = (d = (Model.d_in itm_)) andalso i <> 0
306 fun is_elem itms (_, (d, _)) =
307 case find_first (test_d d) itms of SOME _ => true | NONE => false
309 case filter_out (is_elem itms) pbt of
310 (f, (d, _)) :: _ => SOME (f, ((Rule.term_to_string''' thy) o Model.comp_dts) (d, []))
313 | nxt_add thy oris _ itms =
315 fun testr_vt v ori = member op= (#2 (ori : Model.ori)) v andalso (#3 ori) <> "#undef"
316 fun testi_vt v itm = member op= (#2 (itm : Model.itm)) v
317 fun test_id ids r = member op= ids (#1 (r : Model.ori))
318 fun test_subset itm (_, _, _, d, ts) =
319 (Model.d_in (#5 (itm: Model.itm))) = d andalso subset op = (Model.ts_in (#5 itm), ts)
320 fun false_and_not_Sup (_, _, false, _, Model.Sup _) = false
321 | false_and_not_Sup (_, _, false, _, _) = true
322 | false_and_not_Sup _ = false
323 val v = if itms = [] then 1 else Model.max_vt itms
324 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
327 then itms (* because of dsc without dat *)
328 else filter (testi_vt v) itms; (* itms..vat *)
329 val icl = filter false_and_not_Sup vits; (* incomplete *)
332 then case filter_out (test_id (map #1 vits)) vors of
334 | miss => SOME (getr_ct thy (hd miss))
336 case find_first (test_subset (hd icl)) vors of
337 NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
338 | SOME ori => SOME (geti_ct thy ori (hd icl))
341 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (Specify.itm_out thy itm_)
342 | mk_delete thy "#Find" itm_ = Tactic.Del_Find (Specify.itm_out thy itm_)
343 | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (Specify.itm_out thy itm_)
344 | mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"")
345 fun mk_additem "#Given" ct = Tactic.Add_Given ct
346 | mk_additem "#Find" ct = Tactic.Add_Find ct
347 | mk_additem "#Relate"ct = Tactic.Add_Relation ct
348 | mk_additem str _ = error ("mk_additem: called with field \"" ^ str ^ "\"")
350 (* determine the next step of specification;
351 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
352 eg. in rootpbl 'no_met':
354 preok predicates are _all_ ok (and problem matches completely)
355 oris immediately from formalization
356 (dI',pI',mI') specification coming from author/parent-problem
357 (pbl, item lists specified by user
358 met) -"-, tacitly completed by copy_probl
359 (dI,pI,mI) specification explicitly done by the user
360 (pbt, mpc) problem type, guard of method
362 fun nxt_spec Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
363 (if dI' = Rule.e_domID andalso dI = Rule.e_domID then (Pbl, Tactic.Specify_Theory dI')
364 else if pI' = Celem.e_pblID andalso pI = Celem.e_pblID then (Pbl, Tactic.Specify_Problem pI')
366 case find_first (is_error o #5) pbl of
367 SOME (_, _, _, fd, itm_) =>
368 (Pbl, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_)
370 (case nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris pbt pbl of
371 SOME (fd,ct') => (Pbl, mk_additem fd ct')
372 | NONE => (*pbl-items complete*)
373 if not preok then (Pbl, Tactic.Refine_Problem pI')
374 else if dI = Rule.e_domID then (Pbl, Tactic.Specify_Theory dI')
375 else if pI = Celem.e_pblID then (Pbl, Tactic.Specify_Problem pI')
376 else if mI = Celem.e_metID then (Pbl, Tactic.Specify_Method mI')
378 case find_first (is_error o #5) met of
379 SOME (_, _, _, fd, itm_) => (Met, mk_delete (Celem.assoc_thy dI) fd itm_)
381 (case nxt_add (Celem.assoc_thy dI) oris mpc met of
382 SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*)
383 | NONE => (Met, Tactic.Apply_Method mI))))
384 | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
385 (case find_first (is_error o #5) met of
386 SOME (_,_,_,fd,itm_) => (Met, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_)
388 case nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris mpc met of
389 SOME (fd,ct') => (Met, mk_additem fd ct')
391 (if dI = Rule.e_domID then (Met, Tactic.Specify_Theory dI')
392 else if pI = Celem.e_pblID then (Met, Tactic.Specify_Problem pI')
393 else if not preok then (Met, Tactic.Specify_Method mI)
394 else (Met, Tactic.Apply_Method mI)))
395 | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)
397 (* update the itm_ already input, all..from ori *)
398 fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
400 val ts' = union op = (Model.ts_in itm_) ts;
401 val pval = Model.pbl_ids' d ts'
402 (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
403 val complete = if eq_set op = (ts', all) then true else false
407 (if fd = "#undef" then (id, vt, complete, fd, Model.Sup (d, ts'))
408 else (id, vt, complete, fd, Model.Cor ((d, ts'), (pid, pval))))
409 | (Model.Syn c) => error ("ori_2itm wants to overwrite " ^ c)
410 | (Model.Typ c) => error ("ori_2itm wants to overwrite " ^ c)
413 then (id, vt, true, fd, Model.Cor ((d, ts'), (pid, pval)))
414 else (id, vt, false, fd, Model.Inc ((d, ts'), (pid, pval)))
415 | (Model.Sup (d,ts')) => (*4.9.01 lost env*)
416 (*if fd = "#undef" then*) (id,vt,complete,fd,Model.Sup(d,ts'))
417 (*else (id,vt,complete,fd,Model.Cor((d,ts'),e))*)
418 (* 28.1.00: not completely clear ---^^^ etc.*)
419 | (Model.Mis _) => (* 4.9.01: Model.Mis just copied *)
421 then (id, vt, true, fd, Model.Cor ((d,ts'), (pid, pval)))
422 else (id, vt, false, fd, Model.Inc ((d,ts'), (pid, pval)))
423 | i => error ("ori_2itm: uncovered case of "^ Model.itm_2str i)
426 fun eq1 d (_, (d', _)) = (d = d')
427 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (Model.d_in itm_)
429 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
430 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
431 pval: value for problem-environment _NOT_ checked for 'inter' --
432 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
433 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
434 (*. is_input ori itms <=>
435 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
436 (2) ori(ts) subset itm(ts) --- Err "already input"
437 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
438 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
439 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
440 case find_first (eq1 d) pbt of
441 SOME (_, (_, pid)) =>
442 (case find_first (eq3 f d) itms of
443 SOME (_,_,_,_,itm_) =>
444 let val ts' = inter op = (Model.ts_in itm_) ts
446 if subset op = (ts, ts')
447 then (((strs2str' o map (Rule.term_to_string' ctxt)) ts') ^ " already input", Model.e_itm) (*2*)
448 else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
450 | NONE => ("", ori_2itm (Model.Inc ((Rule.e_term, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
451 | NONE => ("", ori_2itm (Model.Sup (d, ts)) Rule.e_term all (i, v, f, d, ts))
453 fun test_types ctxt (d,ts) =
455 val opt = (try Model.comp_dts) (d, ts)
456 val msg = case opt of
458 | NONE => (Rule.term_to_string' ctxt d ^ " " ^
459 (strs2str' o map (Rule.term_to_string' ctxt)) ts ^ " is illtyped")
462 (* is the term t input (or taken from fmz) known in oris ?
463 give feedback on all(?) strange input;
464 return _all_ terms already input to this item (e.g. valuesFor a,b) *)
465 fun is_known ctxt sel ori t =
467 val ots = (distinct o flat o (map #5)) ori
468 val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots
469 val (d, ts) = Model.split_dts t
470 val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)
472 if (subtract op = oids ids) <> []
473 then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", Model.e_ori, [])
477 if not (subset op = (map typeless ts, map typeless ots))
478 then ("terms '" ^ (strs2str' o (map (Rule.term_to_string' ctxt))) ts ^
479 "' not in example (typeless)", Model.e_ori, [])
481 (case seek_orits ctxt sel ts ori of
482 ("", ori_ as (_,_,_,d,ts), all) =>
483 (case test_types ctxt (d,ts) of
484 "" => ("", ori_, all)
485 | msg => (msg, Model.e_ori, []))
486 | (msg, _, _) => (msg, Model.e_ori, []))
488 if member op = (map #4 ori) d
489 then seek_oridts ctxt sel (d, ts) ori
490 else (Rule.term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
495 Add of Model.itm (* return-value of appl_add *)
496 | Err of string (* error-message *)
498 (* add an item to the model; check wrt. oris and pbt.
499 in contrary to oris<>[] below, this part handles user-input
500 extremely acceptive, i.e. accept input instead error-msg *)
501 fun appl_add ctxt sel [] ppc pbt ct =
503 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl)
505 case TermC.parseNEW ctxt ct of
506 NONE => Add (i, [], false, sel, Model.Syn ct)
508 let val (d, ts) = Model.split_dts t
511 then Add (i, [], false, sel, Model.Mis (Specify.dsc_unknown, hd ts))
513 (case find_first (eq1 d) pbt of
514 NONE => Add (i, [], true, sel, Model.Sup (d,ts))
515 | SOME (f, (_, id)) =>
516 let fun eq2 d (i, _, _, _, itm_) = d = (Model.d_in itm_) andalso i <> 0
517 in case find_first (eq2 d) ppc of
518 NONE => Add (i, [], true, f,Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
519 | SOME (i', _, _, _, itm_) =>
520 if LTool.is_list_dsc d
523 val in_itm = Model.ts_in itm_
524 val ts' = union op = ts in_itm
525 val i'' = if in_itm = [] then i else i'
526 in Add (i'', [], true, f, Model.Cor ((d, ts'), (id, Model.pbl_ids' d ts')))end
527 else Add (i', [], true, f, Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
531 | appl_add ctxt sel oris ppc pbt str =
532 case TermC.parseNEW ctxt str of
533 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
535 case is_known ctxt sel oris t of
537 (case is_notyet_input ctxt ppc all ori' pbt of
539 | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
540 | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
542 (* make oris from args of the stac SubProblem and from pbt.
543 can this formal argument (of a model-pattern) be omitted in the arg-list
544 of a SubProblem ? see calcelems.sml 'type met ' *)
545 fun is_copy_named_idstr str =
546 case (rev o Symbol.explode) str of
547 "'" :: _ :: "'" :: _ => true
549 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t
551 (* should this formal argument (of a model-pattern) create a new identifier? *)
552 fun is_copy_named_generating_idstr str =
553 if is_copy_named_idstr str
555 case (rev o Symbol.explode) str of
556 "'" :: "'" :: "'" :: _ => false
559 fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t
561 (* split type-wrapper from scr-arg and build part of an ori;
562 an type-error is reported immediately, raises an exn,
563 subsequent handling of exn provides 2nd part of error message *)
564 fun mtc thy (str, (dsc, _)) (ty $ var) =
565 ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
566 SOME (([1], str, dsc, (*[var]*)
567 Model.split_dts' (dsc, var))) (*:ori without leading #*))
568 handle e as TYPE _ =>
569 (tracing (dashs 70 ^ "\n"
570 ^ "*** ERROR while creating the items for the model of the ->problem\n"
571 ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
572 ^ "*** item (->description ->value): " ^ Rule.term2str dsc ^ " " ^ Rule.term2str var ^ "\n"
573 ^ "*** description: " ^ TermC.term_detail2str dsc
574 ^ "*** value: " ^ TermC.term_detail2str var
575 ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
576 ^ "*** checked by theory: " ^ Rule.theory2str thy ^ "\n"
578 writeln (@{make_string} e);
579 Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
581 | mtc _ _ t = error ("mtc: uncovered case with" ^ Rule.term2str t)
583 (* match each pat of the model-pattern with an actual argument;
584 precondition: copy-named vars are filtered out *)
585 fun matc _ [] _ oris = oris
588 error ("actual arg(s) missing for '" ^ Celem.pats2str pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
589 | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
590 (*del?..*)if (is_copy_named_idstr o TermC.free2str) t then oris
592 let val opt = mtc thy p a
595 SOME ori => matc thy pbt ags (oris @ [ori])
596 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
599 (* generate a new variable "x_i" name from a related given one "x"
600 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
601 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
602 but leave is_copy_named_generating as is, e.t. ss''' *)
603 fun cpy_nam pbt oris (p as (field, (dsc, t))) =
604 (if is_copy_named_generating p
605 then (*WN051014 kept strange old code ...*)
606 let fun sel (_,_,d,ts) = Model.comp_ts (d, ts)
607 val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
608 val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
609 val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
610 val vals = map sel oris
611 val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
612 in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
613 else ([1], field, dsc, [t])
614 ) handle _ => error ("cpy_nam: for "^ Rule.term2str t)
616 (* match the actual arguments of a SubProblem with a model-pattern
617 and create an ori list (in root-pbl created from formalization).
618 expects ags:pats = 1:1, while copy-named are filtered out of pats;
619 if no 1:1 then exn raised by matc/mtc and handled at call.
620 copy-named pats are appended in order to get them into the model-items *)
621 fun match_ags thy pbt ags =
623 fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
624 val pbt' = filter_out is_copy_named pbt
625 val cy = filter is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *)
626 val oris' = matc thy pbt' ags []
627 val cy' = map (cpy_nam pbt' oris') cy
628 val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
629 in (map flattup ors) end
631 (* report part of the error-msg which is not available in match_args *)
632 fun match_ags_msg pI stac ags =
634 val pats = (#ppc o Specify.get_pbt) pI
635 val msg = (dots 70 ^ "\n"
636 ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
637 ^ "*** model-pattern " ^ Celem.pats2str pats ^ "\n"
638 ^ "*** stac '" ^ Rule.term2str stac ^ "' has the ...\n"
639 ^ "*** arg-list " ^ Rule.terms2str ags ^ "\n"
641 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
644 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
645 fun vars_of_pbl_' pbl_ =
647 fun var_of_pbl_ (_, (_, t)) = t: term
648 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
650 fun overwrite_ppc thy itm ppc =
652 fun repl _ (_, _, _, _, itm_) [] =
653 error ("overwrite_ppc: " ^ (Model.itm_2str_ (Rule.thy2ctxt thy) itm_) ^ " not found")
654 | repl ppc' itm (p :: ppc) =
656 then ppc' @ [itm] @ ppc
657 else repl (ppc' @ [p]) itm ppc
658 in repl [] itm ppc end
660 (* 10.3.00: insert the already compiled itm into model;
661 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
662 fun insert_ppc thy itm ppc =
664 fun eq_untouched d (0, _, _, _, itm_) = (d = Model.d_in itm_)
665 | eq_untouched _ _ = false
666 val ppc' = case seek_ppc (#1 itm) ppc of
667 SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
668 | NONE => (ppc @ [itm])
669 in filter_out (eq_untouched ((Model.d_in o #5) itm)) ppc' end
671 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (Model.d_in itm_ = Model.d_in iitm_)
673 (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
674 handles superfluous items carelessly *)
675 fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
677 (* output the headline to a ppc *)
678 fun header p_ pI mI =
679 case p_ of Pbl => Generate.Problem (if pI = Celem.e_pblID then [] else pI)
680 | Met => Generate.Method mI
681 | pos => error ("header called with "^ pos_2str pos)
683 fun specify_additem sel (ct, _) (p, Met) _ pt =
685 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
686 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
687 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
688 | _ => error "specify_additem: uncovered case of get_obj I pt p"
689 val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
690 val cpI = if pI = Celem.e_pblID then pI' else pI
691 val cmI = if mI = Celem.e_metID then mI' else mI
692 val {ppc, pre, prls, ...} = Specify.get_met cmI
694 case appl_add ctxt sel oris met ppc ct of
695 Add itm => (*..union old input *)
697 val met' = insert_ppc thy itm met
698 val arg = case sel of
699 "#Given" => Tactic.Add_Given' (ct, met')
700 | "#Find" => Tactic.Add_Find' (ct, met')
701 | "#Relate"=> Tactic.Add_Relation'(ct, met')
702 | str => error ("specify_additem: uncovered case with " ^ str)
703 val (p, pt') = case Generate.generate1 thy arg (Istate.Uistate, ctxt) (p, Met) pt of
704 ((p, Met), _, _, pt') => (p, pt')
705 | _ => error "specify_additem: uncovered case of generate1"
706 val pre' = Stool.check_preconds thy prls pre met'
707 val pb = foldl and_ (true, map fst pre')
709 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
710 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
711 in ((p, p_), ((p, p_), Istate.Uistate),
712 Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Istate.Safe, pt')
716 val pre' = Stool.check_preconds thy prls pre met
717 val pb = foldl and_ (true, map fst pre')
719 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
720 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
721 in ((p,p_), ((p,p_),Istate.Uistate), Generate.Error' msg, nxt, Istate.Safe, pt) end
723 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
725 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
726 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
727 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
728 | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
729 val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
730 val cpI = if pI = Celem.e_pblID then pI' else pI
731 val cmI = if mI = Celem.e_metID then mI' else mI
732 val {ppc, where_, prls, ...} = Specify.get_pbt cpI
734 case appl_add ctxt sel oris pbl ppc ct of
735 Add itm => (*..union old input *)
737 val pbl' = insert_ppc thy itm pbl
738 val arg = case sel of
739 "#Given" => Tactic.Add_Given' (ct, pbl')
740 | "#Find" => Tactic.Add_Find' (ct, pbl')
741 | "#Relate"=> Tactic.Add_Relation'(ct, pbl')
742 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
743 val (p, pt') = case Generate.generate1 thy arg (Istate.Uistate, ctxt) (p,Pbl) pt of
744 ((p, Pbl), _, _, pt') => (p, pt')
745 | _ => error "specify_additem: uncovered case of Generate.generate1"
746 val pre = Stool.check_preconds thy prls where_ pbl'
747 val pb = foldl and_ (true, map fst pre)
749 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
750 val ppc = if p_= Pbl then pbl' else met
752 ((p, p_), ((p, p_), Istate.Uistate),
753 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Istate.Safe, pt')
757 val pre = Stool.check_preconds thy prls where_ pbl
758 val pb = foldl and_ (true, map fst pre)
760 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
761 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
762 in ((p, p_), ((p, p_), Istate.Uistate), Generate.Error' msg, nxt, Istate.Safe,pt) end
765 fun specify (Tactic.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
766 let (* either """"""""""""""" all empty or complete *)
767 val thy = Celem.assoc_thy dI'
769 if dI' = Rule.e_domID orelse pI' = Celem.e_pblID (*andalso? WN110511*)
770 then ([], ContextC.e_ctxt)
771 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
772 val (pt, _) = cappend_problem e_ctree [] (Istate.e_istate, ctxt) (fmz, spec')
773 (oris, (dI',pI',mI'), Rule.e_term)
774 val pt = update_ctxt pt [] ctxt
775 val (pbl, pre) = ([], [])
779 (([], Pbl), (([], Pbl), Istate.Uistate),
780 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
781 Tactic.Refine_Tacitly pI', Istate.Safe, pt)
783 (([], Pbl), (([], Pbl), Istate.Uistate),
784 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
785 Tactic.Model_Problem, Istate.Safe, pt)
787 (* ONLY for STARTING modeling phase *)
788 | specify (Tactic.Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt =
790 val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
791 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
792 (oris, dI',pI',mI', dI, ctxt)
793 | _ => error "specify (Model_Problem': uncovered case get_obj"
794 val thy' = if dI = Rule.e_domID then dI' else dI
795 val thy = Celem.assoc_thy thy'
796 val {ppc, prls, where_, ...} = Specify.get_pbt pI'
797 val pre = Stool.check_preconds thy prls where_ pbl
798 val pb = foldl and_ (true, map fst pre)
799 val ((p, _), _, _, pt) =
800 Generate.generate1 thy (Tactic.Model_Problem'([],pbl,met)) (Istate.Uistate, ctxt) pos pt
801 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
802 (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
804 ((p, Pbl), ((p, p_), Istate.Uistate),
805 Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
806 nxt, Istate.Safe, pt)
808 (* called only if no_met is specified *)
809 | specify (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt =
811 val (dI', ctxt) = case get_obj I pt p of
812 PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
813 | _ => error "specify (Refine_Tacitly': uncovered case get_obj"
814 val {met, thy,...} = Specify.get_pbt pIre
815 val (domID, metID) = (Rule.string_of_thy thy, if length met = 0 then Celem.e_metID else hd met)
816 val ((p,_), _, _, pt) =
817 Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Istate.Uistate, ctxt) pos pt
818 val (pbl, pre, _) = ([], [], false)
819 in ((p, Pbl), (pos, Istate.Uistate),
820 Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
821 Tactic.Model_Problem, Istate.Safe, pt)
823 | specify (Tactic.Refine_Problem' rfd) pos _ pt =
825 val ctxt = get_ctxt pt pos
826 val (pos, _, _, pt) =
827 Generate.generate1 (Celem.assoc_thy "Isac") (Tactic.Refine_Problem' rfd) (Istate.Uistate, ctxt) pos pt
829 (pos(*p,Pbl*), (pos(*p,Pbl*), Istate.Uistate), Generate.RefinedKF rfd, Tactic.Model_Problem, Istate.Safe, pt)
831 (*WN110515 initialise ctxt again from itms and add preconds*)
832 | specify (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
834 val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of
835 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
836 (oris, dI', pI', mI', dI, mI, ctxt, met)
837 | _ => error "specify (Specify_Problem': uncovered case get_obj"
838 val thy = Celem.assoc_thy dI
840 case Generate.generate1 thy (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate.Uistate, ctxt) pos pt of
841 ((p, Pbl), _, _, pt) => (p, pt)
842 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
843 val dI'' = Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)
844 val mI'' = if mI = Celem.e_metID then mI' else mI
845 val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI,
846 (#ppc o Specify.get_met) mI'') (dI, pI, mI);
848 ((p,Pbl), (pos,Istate.Uistate),
849 Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre),
850 nxt, Istate.Safe, pt)
852 (*WN110515 initialise ctxt again from itms and add preconds*)
853 | specify (Tactic.Specify_Method' (mID, _, _)) (pos as (p, _)) _ pt =
855 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
856 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
857 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
858 | _ => error "specify (Specify_Problem': uncovered case get_obj"
859 val {ppc, pre, prls,...} = Specify.get_met mID
860 val thy = Celem.assoc_thy dI
861 val dI'' = if dI = Rule.e_domID then dI' else dI
862 val pI'' = if pI = Celem.e_pblID then pI' else pI
863 val oris = Specify.add_field' thy ppc oris
864 val met = if met = [] then pbl else met
865 val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls) oris
866 (*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
868 if mI' = ["Biegelinien", "ausBelastung"]
870 [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
871 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
872 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
873 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
874 (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
875 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
876 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
877 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
879 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
880 val (pos, _, _, pt) =
881 Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate.Uistate, ctxt) pos pt
882 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
883 ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
885 (pos, (pos,Istate.Uistate),
886 Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (Celem.assoc_thy dI'') itms pre'),
887 nxt, Istate.Safe, pt)
889 | specify (Tactic.Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
890 | specify (Tactic.Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
891 | specify (Tactic.Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
892 | specify (Tactic.Specify_Theory' domID) (pos as (p,p_)) _ pt =
894 val p_ = case p_ of Met => Met | _ => Pbl
895 val thy = Celem.assoc_thy domID
896 val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
897 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
898 (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
899 | _ => error "specify (Specify_Theory': uncovered case get_obj"
900 val mppc = case p_ of Met => met | _ => pbl
901 val cpI = if pI = Celem.e_pblID then pI' else pI
902 val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI
903 val cmI = if mI = Celem.e_metID then mI' else mI
904 val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI
906 Met => (Stool.check_preconds thy mer mwh met)
907 | _ => (Stool.check_preconds thy per pwh pbl)
908 val pb = foldl and_ (true, map fst pre)
912 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
914 ((p, p_), (pos, Istate.Uistate),
915 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
916 nxt, Istate.Safe, pt)
918 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
920 val ((p, p_), _, _, pt) = Generate.generate1 thy (Tactic.Specify_Theory' domID) (Istate.Uistate, ctxt) (p,p_) pt
921 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
923 ((p,p_), (pos,Istate.Uistate),
924 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
925 nxt, Istate.Safe, pt)
928 | specify m' _ _ _ = error ("specify: not impl. for " ^ Tactic.tac_2str m')
930 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
931 -- for input from scratch*)
932 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
934 val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of
935 PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
936 (oris, dI', pI', dI, pI, pbl, ctxt)
937 | _ => error "specify (Specify_Theory': uncovered case get_obj"
938 val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI;
939 val cpI = if pI = Celem.e_pblID then pI' else pI;
941 case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
942 Add itm (*..union old input *) =>
944 val pbl' = insert_ppc thy itm pbl
945 val (tac, tac_) = case sel of
946 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, pbl'))
947 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, pbl'))
948 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))
949 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
950 val (p, c, pt') = case Generate.generate1 thy tac_ (Istate.Uistate, ctxt) (p,Pbl) pt of
951 ((p, Pbl), c, _, pt') => (p, c, pt')
952 | _ => error "nxt_specif_additem: uncovered case generate1"
954 ([(tac, tac_, ((p, Pbl), (Istate.Uistate, ctxt)))], c, (pt', (p, Pbl)))
956 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
957 FIXME ..and dont abuse a tactic for that purpose*)
958 ([(Tactic.Tac msg, Tactic.Tac_ (Rule.Thy_Info_get_theory "Isac", msg,msg,msg),
959 (e_pos', (Istate.e_istate, ContextC.e_ctxt)))], [], ptp)
961 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
963 val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of
964 PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
965 (oris, dI', mI', dI, mI, met, ctxt)
966 | _ => error "nxt_specif_additem Met: uncovered case get_obj"
967 val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI;
968 val cmI = if mI = Celem.e_metID then mI' else mI;
970 case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
971 Add itm (*..union old input *) =>
973 val met' = insert_ppc thy itm met;
974 val (tac,tac_) = case sel of
975 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, met'))
976 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, met'))
977 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))
978 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
979 val (p, c, pt') = case Generate.generate1 thy tac_ (Istate.Uistate, ctxt) (p, Met) pt of
980 ((p, Met), c, _, pt') => (p, c, pt')
981 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
983 ([(tac, tac_, ((p, Met), (Istate.Uistate, ctxt)))], c, (pt', (p, Met)))
985 | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
987 | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)
989 fun ori2Coritm pbt (i, v, f, d, ts) =
990 (i, v, true, f, Model.Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts)))
991 handle _ => (i, v, true, f, Model.Cor ((d, ts), (d, ts)))
992 (*dsc in oris, but not in pbl pat list: keep this dsc*)
994 (* filter out oris which have same description in itms *)
995 fun filter_outs oris [] = oris
996 | filter_outs oris (i::itms) =
998 val ors = filter_out ((curry op = ((Model.d_in o #5) i)) o (#4)) oris
1000 filter_outs ors itms
1003 (* filter oris which are in pbt, too *)
1004 fun filter_pbt oris pbt =
1006 val dscs = map (fst o snd) pbt
1008 filter ((member op= dscs) o (#4)) oris
1011 (* combine itms from pbl + met and complete them wrt. pbt *)
1012 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1013 fun complete_metitms oris pits mits met =
1015 val vat = Model.max_vt pits;
1016 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
1017 val ors = filter ((member_swap op= vat) o (#2)) oris
1018 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
1020 itms @ (map (ori2Coritm met) os)
1023 (* complete model and guard of a calc-head *)
1024 fun complete_mod_ (oris, mpc, ppc, probl) =
1026 val pits = filter_out ((curry op= false) o (#3)) probl
1027 val vat = if probl = [] then 1 else Model.max_vt probl
1028 val pors = filter ((member_swap op = vat) o (#2)) oris
1029 val pors = filter_outs pors pits (*which are in pbl already*)
1030 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1031 val pits = pits @ (map (ori2Coritm ppc) pors)
1032 val mits = complete_metitms oris pits [] mpc
1035 fun some_spec (odI, opI, omI) (dI, pI, mI) =
1036 (if dI = Rule.e_domID then odI else dI,
1037 if pI = Celem.e_pblID then opI else pI,
1038 if mI = Celem.e_metID then omI else mI)
1040 (* find a next applicable tac (for calcstate) and update ctree
1041 (for ev. finding several more tacs due to hide) *)
1042 (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
1043 (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
1044 (* WN.24.10.03 fun begin_end_prog = ...................................?? *)
1045 fun nxt_specif (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
1047 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
1048 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
1049 | _ => error "nxt_specif Model_Problem; uncovered case get_obj"
1050 val (dI, pI, mI) = some_spec ospec spec
1051 val thy = Celem.assoc_thy dI
1052 val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
1053 val {cas, ppc, ...} = Specify.get_pbt pI
1054 val pbl = Generate.init_pbl ppc (* fill in descriptions *)
1055 (*----------------if you think, this should be done by the Dialog
1056 in the java front-end, search there for WN060225-modelProblem----*)
1057 val (pbl, met) = case cas of
1059 | _ => complete_mod_ (oris, mpc, ppc, probl)
1060 (*----------------------------------------------------------------*)
1061 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
1062 val (pos,c,_,pt) = Generate.generate1 thy tac_ (Istate.Uistate, ctxt) pos pt
1063 in ([(tac, tac_, (pos, (Istate.Uistate, ContextC.e_ctxt)))], c, (pt,pos)) end
1064 | nxt_specif (Tactic.Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1065 | nxt_specif (Tactic.Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1066 | nxt_specif (Tactic.Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1067 (*. called only if no_met is specified .*)
1068 | nxt_specif (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1070 val (oris, dI, ctxt) = case get_obj I pt p of
1071 (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
1072 | _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj"
1073 val opt = Specify.refine_ori oris pI
1078 val {met, ...} = Specify.get_pbt pI'
1079 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1080 val mI = if length met = 0 then Celem.e_metID else hd met
1081 val thy = Celem.assoc_thy dI
1082 val (pos, c, _, pt) =
1083 Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate.Uistate, ctxt) pos pt
1085 ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1086 (pos, (Istate.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
1088 | NONE => ([], [], ptp)
1090 | nxt_specif (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1092 val (dI, dI', probl, ctxt) = case get_obj I pt p of
1093 PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
1094 (dI, dI', probl, ctxt)
1095 | _ => error "nxt_specif Refine_Problem: uncovered case get_obj"
1096 val thy = if dI' = Rule.e_domID then dI else dI'
1098 case Specify.refine_pbl (Celem.assoc_thy thy) pI probl of
1099 NONE => ([], [], ptp)
1102 val (pos,c,_,pt) = Generate.generate1 (Celem.assoc_thy thy) (Tactic.Refine_Problem' rfd) (Istate.Uistate, ctxt) pos pt
1104 ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
1107 | nxt_specif (Tactic.Specify_Problem pI) (pt, pos as (p,_)) =
1109 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
1110 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
1111 (oris, dI, dI', pI', probl, ctxt)
1113 val thy = Celem.assoc_thy (if dI' = Rule.e_domID then dI else dI');
1114 val {ppc,where_,prls,...} = Specify.get_pbt pI
1116 if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
1117 then (false, (Generate.init_pbl ppc, []))
1118 else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
1119 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1120 val (c, pt) = case Generate.generate1 thy (Tactic.Specify_Problem' (pI, pbl)) (Istate.Uistate, ctxt) pos pt of
1121 ((_, Pbl), c, _, pt) => (c, pt)
1124 ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
1126 (* transfers oris (not required in pbl) to met-model for script-env
1127 FIXME.WN.8.03: application of several mIDs to SAME model? *)
1128 | nxt_specif (Tactic.Specify_Method mID) (pt, pos as (p,_)) =
1130 val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of
1131 PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
1132 => (oris, pbl, dI, met, ctxt)
1133 | _ => error "nxt_specif Specify_Method: uncovered case get_obj"
1134 val {ppc,pre,prls,...} = Specify.get_met mID
1135 val thy = Celem.assoc_thy dI
1136 val oris = Specify.add_field' thy ppc oris
1137 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
1138 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
1139 (*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
1141 if mID = ["Biegelinien", "ausBelastung"]
1143 [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
1144 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
1145 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
1146 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
1147 (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
1148 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
1149 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
1150 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
1152 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
1153 val (pos, c, _, pt) =
1154 Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate.Uistate, ctxt) pos pt
1156 ([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate.Uistate, ContextC.e_ctxt)))], c, (pt, pos))
1158 | nxt_specif (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
1160 val ctxt = get_ctxt pt pos
1161 val (pos, c, _, pt) =
1162 Generate.generate1 (Celem.assoc_thy "Isac") (Tactic.Specify_Theory' dI) (Istate.Uistate, ctxt) pos pt
1163 in (*FIXXXME: check if pbl can still be parsed*)
1164 ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate.Uistate, ctxt)))], c,
1167 | nxt_specif (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =
1169 val ctxt = get_ctxt pt pos
1170 val (pos, c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac") (Tactic.Specify_Theory' dI) (Istate.Uistate, ctxt) pos pt
1171 in (*FIXXXME: check if met can still be parsed*)
1172 ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate.Uistate, ctxt)))], c, (pt, pos))
1174 | nxt_specif m' _ = error ("nxt_specif: not impl. for " ^ Tactic.tac2str m')
1176 (* get the values from oris; handle the term list w.r.t. penv *)
1177 fun vals_of_oris oris =
1178 ((map (Model.mkval' o (#5))) o
1179 (filter ((member_swap op= 1) o (#2)))) oris
1181 (* create a calc-tree with oris via an cas.refined pbl *)
1182 fun nxt_specify_init_calc ([], (dI, pI, mI)) =
1184 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1186 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
1187 val dI = if dI = "" then Rule.theory2theory' thy else dI
1188 val mI = if mI = [] then hd met else mI
1189 val hdl = case cas of NONE => LTool.pblterm dI pI | SOME t => t
1190 val (pt,_) = cappend_problem e_ctree [] (Istate.Uistate, ContextC.e_ctxt) ([], (dI, pI, mI))
1191 ([], (dI,pI,mI), hdl)
1192 val pt = update_spec pt [] (dI, pI, mI)
1193 val pits = Generate.init_pbl' ppc
1194 val pt = update_pbl pt [] pits
1195 in ((pt, ([] , Pbl)), []) end
1198 then (* from met-browser *)
1200 val {ppc, ...} = Specify.get_met mI
1201 val dI = if dI = "" then "Isac" else dI
1203 cappend_problem e_ctree [] (Istate.e_istate, ContextC.e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term (*FIXME met*))
1204 val pt = update_spec pt [] (dI, pI, mI)
1205 val mits = Generate.init_pbl' ppc
1206 val pt = update_met pt [] mits
1207 in ((pt, ([], Met)), []) end
1208 else (* new example, pepare for interactive modeling *)
1211 cappend_problem e_ctree [] (Istate.e_istate, ContextC.e_ctxt) ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term)
1212 in ((pt, ([], Pbl)), []) end
1213 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
1214 let (* both """"""""""""""""""""""""" either empty or complete *)
1215 val thy = Celem.assoc_thy dI
1216 val (pI, (pors, pctxt), mI) =
1220 val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
1221 val pI' = Specify.refine_ori' pors pI;
1222 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1223 (hd o #met o Specify.get_pbt) pI')
1225 else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
1226 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
1227 val dI = Rule.theory2theory' (Stool.common_subthy (thy, thy'))
1228 val hdl = case cas of
1229 NONE => LTool.pblterm dI pI
1230 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
1232 cappend_problem e_ctree [] (Istate.e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
1233 val pt = update_ctxt pt [] pctxt
1235 ((pt, ([], Pbl)), fst3 (nxt_specif Tactic.Model_Problem (pt, ([], Pbl))))
1238 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
1239 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
1240 fun tag_form thy (formal, given) =
1242 val gf = (head_of given) $ formal;
1243 val _ = Thm.global_cterm_of thy gf
1245 handle _ => error ("calchead.tag_form: " ^ Rule.term_to_string''' thy given ^
1246 " .. " ^ Rule.term_to_string''' thy formal ^ " ..types do not match")
1248 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
1250 (* check pbltypes, announces one failure a time *)
1251 fun chk_vars ctppc =
1253 val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc TermC.vars ctppc)
1254 val chked = subtract op = gi wh
1256 if chked <> [] then ("wh\\gi", chked)
1258 let val chked = subtract op = (union op = gi fi) re
1261 then ("re\\(gi union fi)", chked)
1266 (* check a new pbltype: variables (Free) unbound by given, find*)
1267 fun unbound_ppc ctppc =
1269 val {Given = gi, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc TermC.vars ctppc)
1271 distinct (subtract op = (union op = gi fi) re)
1274 (* called only once, if a Subproblem has been located in the script*)
1275 fun nxt_model_pbl (Tactic.Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp =
1277 ["no_met"] => (snd3 o hd o fst3) (nxt_specif (Tactic.Refine_Tacitly pblID) ptp)
1278 | _ => (snd3 o hd o fst3) (nxt_specif Tactic.Model_Problem ptp))
1279 (*all stored in tac_ itms^^^^^^^^^^*)
1280 | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ Tactic.tac_2str tac_)
1282 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1283 + met from fmz; assumes pos on PblObj, meth = [] *)
1284 fun complete_mod (pt, pos as (p, p_) : pos') =
1286 val _ = if p_ <> Pbl
1287 then error ("###complete_mod: only impl.for Pbl, called with " ^ pos'2str pos)
1289 val (oris, ospec, probl, spec) = case get_obj I pt p of
1290 PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
1291 | _ => error "complete_mod: unvered case get_obj"
1292 val (_, pI, mI) = some_spec ospec spec
1293 val mpc = (#ppc o Specify.get_met) mI
1294 val ppc = (#ppc o Specify.get_pbt) pI
1295 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1296 val pt = update_pblppc pt p pits
1297 val pt = update_metppc pt p mits
1298 in (pt, (p, Met) : pos') end
1300 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1301 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1302 fun all_modspec (pt, (p, _) : pos') =
1304 val (pors, dI, pI, mI) = case get_obj I pt p of
1305 PblObj {origin = (pors, (dI, pI, mI), _), ...} => (pors, dI, pI, mI)
1306 | _ => error "all_modspec: uncovered case get_obj"
1307 val {ppc, ...} = Specify.get_met mI
1308 val (_, vals) = oris2fmz_vals pors
1309 val ctxt = ContextC.initialise dI vals
1310 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors)
1311 val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*)
1312 val pt = update_spec pt p (dI, pI, mI)
1313 val pt = update_ctxt pt p ctxt
1315 (pt, (p, Met) : pos')
1318 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
1319 fun is_complete_mod_ [] = false
1320 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
1322 fun is_complete_mod (pt, pos as (p, Pbl) : pos') =
1323 if (is_pblobj o (get_obj I pt)) p
1324 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1325 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1326 | is_complete_mod (pt, pos as (p, Met)) =
1327 if (is_pblobj o (get_obj I pt)) p
1328 then (is_complete_mod_ o (get_obj g_met pt)) p
1329 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1330 | is_complete_mod (_, pos) =
1331 error ("is_complete_mod called by " ^ pos'2str pos ^ " (should be Pbl or Met)")
1333 (* have (thy, pbl, met) _all_ been specified explicitly ? *)
1334 fun is_complete_spec (pt, pos as (p, _) : pos') =
1335 if (not o is_pblobj o (get_obj I pt)) p
1336 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1338 let val (dI,pI,mI) = get_obj g_spec pt p
1339 in dI <> Rule.e_domID andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID end
1341 (* complete empty items in specification from origin (pbl, met ev.refined);
1342 assumes 'is_complete_mod' *)
1343 fun complete_spec (pt, pos as (p, _) : pos') =
1345 val (ospec, spec) = case get_obj I pt p of
1346 PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
1347 | _ => error "complete_spec: uncovered case get_obj"
1348 val pt = update_spec pt p (some_spec ospec spec)
1353 fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
1355 fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =
1357 val (_, _, metID) = get_somespec' spec spec'
1358 val pre = if metID = Celem.e_metID then []
1361 val {prls, pre= where_, ...} = Specify.get_met metID
1362 val pre = Stool.check_preconds' prls where_ meth 0
1364 val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
1366 ModSpec (allcorrect, Met, hdl, meth, pre, spec)
1368 | pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
1370 val (_, pI, _) = get_somespec' spec spec'
1371 val pre = if pI = Celem.e_pblID then []
1374 val {prls, where_, ...} = Specify.get_pbt pI
1375 val pre = Stool.check_preconds' prls where_ probl 0
1377 val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
1379 ModSpec (allcorrect, Pbl, hdl, probl, pre, spec)
1381 | pt_model _ _ = error "pt_model: uncovered definition"
1383 fun pt_form (PrfObj {form, ...}) = Form form
1384 | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) =
1386 val (dI, pI, _) = get_somespec' spec spec'
1387 val {cas, ...} = Specify.get_pbt pI
1389 NONE => Form (LTool.pblterm dI pI)
1390 | SOME t => Form (subst_atomic (Model.mk_env probl) t)
1393 (* pt_extract returns
1394 # the formula at pos
1395 # the tactic applied to this formula
1396 # the list of assumptions generated at this formula
1397 (by application of another tac to the preceding formula !)
1398 pos is assumed to come from the frontend, ie. generated by moveDown.
1399 Notes: cannot be in ctree.sml, because ModSpec has to be calculated.
1400 TODO 110417 get assumptions from ctxt !?
1402 fun pt_extract (pt, ([], Res)) =
1403 (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)
1405 val (f, asm) = get_obj g_result pt []
1406 in (Form f, NONE, asm) end
1407 | pt_extract (pt,(p,Res)) =
1409 val (f, asm) = get_obj g_result pt p
1413 if is_pblobj' pt (lev_up p)
1416 val pI = case get_obj I pt (lev_up p) of
1417 PblObj{spec = (_, pI, _), ...} => pI
1418 | _ => error "pt_extract last_onlev: uncovered case get_obj"
1419 in if pI = Celem.e_pblID then NONE else SOME (Tactic.Check_Postcond pI) end
1420 else SOME Tactic.End_Trans (* WN0502 TODO for other branches *)
1422 let val p' = lev_on p
1427 val (dI ,pI) = case get_obj I pt p' of
1428 PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)
1429 | _ => error "pt_extract \<not>last_onlev: uncovered case get_obj"
1430 in SOME (Tactic.Subproblem (dI, pI)) end
1432 if f = get_obj g_form pt p'
1433 then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
1434 else SOME (Tactic.Take (Rule.term2str (get_obj g_form pt p')))
1436 in (Form f, tac, asm) end
1437 | pt_extract (pt, (p,p_(*Frm,Pbl*))) =
1439 val ppobj = get_obj I pt p
1440 val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
1441 val tac = g_tac ppobj
1442 in (f, SOME tac, []) end
1444 (** get the formula from a ctree-node:
1445 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1446 take res from all other PrfObj's
1447 Designed for interSteps, outcommented 04 in favour of calcChangedEvent **)
1448 fun formres p (Nd (PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
1449 [("headline", (p, Frm), h), ("stepform", (p, Res), r)]
1450 | formres p (Nd (PrfObj {form, result = (r, _), ...}, _)) =
1451 [("stepform", (p, Frm), form), ("stepform", (p, Res), r)]
1452 | formres _ _ = error "formres: uncovered definition"
1453 fun form p (Nd (PrfObj {result = (r, _), ...}, _)) =
1454 [("stepform", (p, Res), r)]
1455 | form _ _ = error "form: uncovered definition"
1457 (* assumes to take whole level, in particular hd -- for use in interSteps *)
1458 fun get_formress fs _ [] = flat fs
1459 | get_formress fs p (nd::nds) =
1460 (* start with 'form+res' and continue with trying 'res' only*)
1461 get_forms (fs @ [formres p nd]) (lev_on p) nds
1462 and get_forms fs _ [] = flat fs
1463 | get_forms fs p (nd::nds) =
1465 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1466 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1467 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1468 (* continue with trying 'res' only*)
1469 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1471 (** get an 'interval' 'from' 'to' of formulae from a ctree **)
1472 (* WN0401 this functionality belongs to ctree.sml *)
1473 fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2
1474 | eq_pos' (p1, Res) (p2, Res) = p1 = p2
1475 | eq_pos' (p1, Pbl) (p2, p2_) =
1476 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
1477 | eq_pos' (p1, Met) (p2, p2_) =
1478 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
1479 | eq_pos' _ _ = false;
1481 (* get an 'interval' from the ctree; 'interval' is w.r.t. the
1482 total ordering Position#compareTo(Position p) in the java-code
1483 val get_interval = fn :
1484 pos' -> : from is "move_up 1st-element" to return
1485 pos' -> : to the last element to be returned; from < to
1486 int -> : level: 0 gets the flattest sub-tree possible, 999 the deepest
1488 (pos' * : of the formula
1489 Term.term) : the formula
1491 fun get_interval from to level pt =
1493 fun get_inter c (from : pos') (to : pos') lev pt =
1494 if eq_pos' from to orelse from = ([], Res)
1496 let val (f, tacopt, _) = pt_extract (pt, from)
1498 ModSpec (_, _, headline, _, _, _) => c @ [(from, headline, NONE)]
1499 | Form t => c @ [(from, t, tacopt)]
1502 if lev < lev_of from
1503 then (get_inter c (move_dn [] pt from) to lev pt)
1504 handle (PTREE _(*from move_dn too far*)) => c
1507 val (f, tacopt, _) = pt_extract (pt, from)
1508 val term = case f of
1509 ModSpec (_,_,headline,_,_,_) => headline
1511 in (get_inter (c @ [(from, term, tacopt)]) (move_dn [] pt from) to lev pt)
1512 handle (PTREE _(*from move_dn too far*)) => c @ [(from, term, tacopt)]
1514 in get_inter [] from to level pt end
1516 fun posterm2str (pos, t, _) = "(" ^ pos'2str pos ^ ", " ^ Rule.term2str t ^ ")"
1517 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
1519 fun postermtac2str (pos, t, SOME tac) =
1520 pos'2str pos ^ ", " ^ Rule.term2str t ^ "\n" ^ indent 10 ^ Tactic.tac2str tac
1521 | postermtac2str (pos, t, NONE) =
1522 pos'2str pos ^ ", " ^ Rule.term2str t
1523 fun postermtacs2str pfts = (strs2str' o (map (curry op ^ "\n")) o (map postermtac2str)) pfts
1525 (* WN050225 omits the last step, if pt is incomplete *)
1526 fun show_pt pt = tracing (posterms2str (get_interval ([], Frm) ([], Res) 99999 pt))
1527 fun show_pt_tac pt = tracing (postermtacs2str (get_interval ([], Frm) ([], Res) 99999 pt))
1529 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
1530 fun get_ocalhd (pt, (p, Pbl) : pos') =
1532 val (ospec, hdf', spec, probl) = case get_obj I pt p of
1533 PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
1534 | _ => error "get_ocalhd Pbl: uncovered case get_obj"
1535 val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))
1536 val pre = Stool.check_preconds (Celem.assoc_thy "Isac") prls where_ probl
1538 (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
1540 | get_ocalhd (pt, (p, Met)) =
1542 val (ospec, hdf', spec, meth) = case get_obj I pt p of
1543 PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
1544 | _ => error "get_ocalhd Met: uncovered case get_obj"
1545 val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec))
1546 val pre = Stool.check_preconds (Celem.assoc_thy "Isac") prls pre meth
1548 (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
1550 | get_ocalhd _ = error "get_ocalhd: uncovered definition"
1552 (* at the activeFormula set the Model, the Guard and the Specification
1553 to empty and return a CalcHead;
1554 the 'origin' remains (for reconstructing all that) *)
1555 fun reset_calchead (pt, (p,_) : pos') =
1557 val () = case get_obj I pt p of
1559 | _ => error "reset_calchead: uncovered case get_obj"
1560 val pt = update_pbl pt p []
1561 val pt = update_met pt p []
1562 val pt = update_spec pt p Celem.e_spec
1563 in (pt, (p, Pbl) : pos') end