1 (* Title: Specify-phase: specifying and modeling a problem or a subproblem. The
2 most important types are declared in mstools.sml.
3 Author: Walther Neuper 991122, Mathias Lehnfeld
4 (c) due to copyright terms
6 12345678901234567890123456789012345678901234567890123456789012345678901234567890
7 10 20 30 40 50 60 70 80
10 (* TODO interne Funktionen aus sig entfernen *)
13 datatype additm = Add of SpecifyTools.itm | Err of string
14 val all_dsc_in : SpecifyTools.itm_ list -> Term.term list
15 val all_modspec : ptree * pos' -> ptree * pos'
16 datatype appl = Appl of tac_ | Notappl of string
20 SpecifyTools.ori list ->
21 SpecifyTools.itm list ->
22 (string * (Term.term * Term.term)) list -> cterm' -> additm
25 val chk_vars : term ppc -> string * Term.term list
27 theory -> int * term list * term list -> term
29 theory -> term list * term list -> term list
30 val complete_metitms :
31 SpecifyTools.ori list ->
32 SpecifyTools.itm list ->
33 SpecifyTools.itm list -> pat list -> SpecifyTools.itm list
34 val complete_mod_ : ori list * pat list * pat list * itm list ->
36 val complete_mod : ptree * pos' -> ptree * (pos * pos_)
37 val complete_spec : ptree * pos' -> ptree * pos'
39 pat list -> preori list -> pat -> preori
40 val e_calcstate : calcstate
41 val e_calcstate' : calcstate'
42 val eq1 : ''a -> 'b * (''a * 'c) -> bool
44 ''a -> Term.term -> 'b * 'c * 'd * ''a * SpecifyTools.itm_ -> bool
45 val eq4 : ''a -> 'b * ''a list * 'c * 'd * 'e -> bool
47 'a * 'b * 'c * 'd * SpecifyTools.itm_ ->
48 'e * 'f * 'g * Term.term * 'h -> bool
49 val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool
50 val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool
51 val f_mout : theory -> mout -> Term.term
53 SpecifyTools.ori list ->
54 SpecifyTools.itm list -> SpecifyTools.ori list
56 SpecifyTools.ori list ->
57 ('a * (Term.term * 'b)) list -> SpecifyTools.ori list
58 val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
59 val foldr1 : ('a * 'a -> 'a) -> 'a list -> 'a
60 val form : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
61 val formres : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
62 val gen_ins' : ('a * 'a -> bool) -> 'a * 'a list -> 'a list
64 (string * (pos * pos_) * Term.term) list list ->
65 pos -> ptree list -> (string * (pos * pos_) * Term.term) list
67 (string * (pos * pos_) * Term.term) list list ->
68 posel list -> ptree list -> (string * (pos * pos_) * Term.term) list
69 val get_interval : pos' -> pos' -> int -> ptree -> (pos' * term) list
70 val get_ocalhd : ptree * pos' -> ocalhd
71 val get_spec_form : tac_ -> pos' -> ptree -> mout
74 SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'
75 val getr_ct : theory -> SpecifyTools.ori -> string * cterm'
76 val has_list_type : Term.term -> bool
77 val header : pos_ -> pblID -> metID -> pblmet
80 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
81 SpecifyTools.itm list -> SpecifyTools.itm list
83 SpecifyTools.itm -> SpecifyTools.itm list -> SpecifyTools.itm list
84 val is_complete_mod : ptree * pos' -> bool
85 val is_complete_mod_ : SpecifyTools.itm list -> bool
86 val is_complete_modspec : ptree * pos' -> bool
87 val is_complete_spec : ptree * pos' -> bool
88 val is_copy_named : 'a * ('b * Term.term) -> bool
89 val is_copy_named_idstr : string -> bool
90 val is_error : SpecifyTools.itm_ -> bool
91 val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
95 SpecifyTools.ori list ->
96 Term.term -> string * SpecifyTools.ori * Term.term list
97 val is_list_type : Term.typ -> bool
100 SpecifyTools.itm list ->
103 ('a * (Term.term * Term.term)) list -> string * SpecifyTools.itm
104 val is_parsed : SpecifyTools.itm_ -> bool
105 val is_untouched : SpecifyTools.itm -> bool
110 (int list * string * Term.term * Term.term list) list ->
111 (int list * string * Term.term * Term.term list) list
113 theory -> pat list -> Term.term list -> SpecifyTools.ori list
114 val oris2fmz_vals : ori list -> string list * term list
115 val maxl : int list -> int
116 val match_ags_msg : string list -> Term.term -> Term.term list -> unit
117 val memI : ''a list -> ''a -> bool
118 val mk_additem : string -> cterm' -> tac
119 val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
121 theory -> pat -> Term.term -> SpecifyTools.preori option
124 SpecifyTools.ori list ->
125 (string * (Term.term * 'a)) list ->
126 SpecifyTools.itm list -> (string * cterm') option
127 val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
131 SpecifyTools.ori list ->
133 SpecifyTools.itm list * SpecifyTools.itm list ->
134 (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->
136 val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'
137 val nxt_specif_additem :
138 string -> cterm' -> ptree * (int list * pos_) -> calcstate'
139 val nxt_specify_init_calc : fmz -> calcstate
140 val ocalhd_complete :
141 SpecifyTools.itm list ->
142 (bool * Term.term) list -> domID * pblID * metID -> bool
144 pat list -> ori -> itm
147 Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
150 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
151 SpecifyTools.itm list ->
152 (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
153 val parse_ok : SpecifyTools.itm_ list -> bool
154 val posform2str : pos' * ptform -> string
155 val posforms2str : (pos' * ptform) list -> string
156 val posterms2str : (pos' * term) list -> string (*tests only*)
157 val ppc135list : 'a SpecifyTools.ppc -> 'a list
158 val ppc2list : 'a SpecifyTools.ppc -> 'a list
160 ptree * (int list * pos_) ->
161 ptform * tac option * Term.term list
162 val pt_form : ppobj -> ptform
163 val pt_model : ppobj -> pos_ -> ptform
164 val reset_calchead : ptree * pos' -> ptree * pos'
168 Term.term * Term.term list ->
169 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
170 -> string * SpecifyTools.ori * Term.term list
175 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
176 -> string * SpecifyTools.ori * Term.term list
178 int -> SpecifyTools.itm list -> SpecifyTools.itm option
179 val show_pt : ptree -> unit
180 val some_spec : spec -> spec -> spec
186 (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *
188 val specify_additem :
194 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
195 val tag_form : theory -> term * term -> term
196 val test_types : Proof.context -> Term.term * Term.term list -> string
197 val typeless : Term.term -> Term.term
198 val unbound_ppc : term SpecifyTools.ppc -> Term.term list
199 val vals_of_oris : SpecifyTools.ori list -> Term.term list
200 val variants_in : Term.term list -> int
201 val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
202 val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
209 structure CalcHead (**): CALC_HEAD(**) =
215 (*.the state wich is stored after each step of calculation; it contains
216 the calc-state and a list of [tac,istate](="tacis") to be applied next.
217 the last_elem tacis is the first to apply to the calc-state and
218 the (only) one shown to the front-end as the 'proposed tac'.
219 the calc-state resulting from the application of tacis is not stored,
220 because the tacis hold enough information for efficiently rebuilding
221 this state just by "fun generate ".*)
223 (ptree * pos') * (*the calc-state to which the tacis could be applied*)
224 (taci list); (*ev. several (hidden) steps;
225 in REVERSE order: first tac_ to apply is last_elem*)
226 val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
228 (*the state used during one calculation within the mathengine; it contains
229 a list of [tac,istate](="tacis") which generated the the calc-state;
230 while this state's tacis are extended by each (internal) step,
231 the calc-state is used for creating new nodes in the calc-tree
232 (eg. applicable_in requires several particular nodes of the calc-tree)
233 and then replaced by the the newly created;
234 on leave of the mathengine the resuing calc-state is dropped anyway,
235 because the tacis hold enought information for efficiently rebuilding
236 this state just by "fun generate ".*)
238 taci list * (*cas. several (hidden) steps;
239 in REVERSE order: first tac_ to apply is last_elem*)
240 pos' list * (*a "continuous" sequence of pos',
241 deleted by application of taci list*)
242 (ptree * pos'); (*the calc-state resulting from the application of tacis*)
243 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
245 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
246 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
247 | f_mout thy _ = error "f_mout: not called with formula";
250 (*.is the calchead complete ?.*)
251 fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
252 foldl and_ (true, map #3 its) andalso
253 foldl and_ (true, map #1 pre) andalso
254 dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
256 (*["BOOL (1+x=2)","REAL x"] --match_ags--> oris
257 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"]*)
258 fun oris2fmz_vals oris =
259 let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) =
260 ((term2str o comp_dts') (dsc, ts), last_elem ts)
261 handle _ => error ("ori2fmz_env called with "^terms2str ts)
262 in (split_list o (map ori2fmz_vals)) oris end;
264 (* make a term 'typeless' for comparing with another 'typeless' term;
265 'type-less' usually is illtyped *)
266 fun typeless (Const(s,_)) = (Const(s,e_type))
267 | typeless (Free(s,_)) = (Free(s,e_type))
268 | typeless (Var(n,_)) = (Var(n,e_type))
269 | typeless (Bound i) = (Bound i)
270 | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
271 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
273 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
274 > val (_,t1) = split_dsc_t hs (term_of ct);
275 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
276 > val (_,t2) = split_dsc_t hs (term_of ct);
277 > typeless t1 = typeless t2;
283 (*.to an input (d,ts) find the according ori and insert the ts.*)
284 (*WN.11.03: + dont take first inter<>[]*)
285 fun seek_oridts ctxt sel (d,ts) [] =
286 ("seek_oridts: input ('" ^
287 (term_to_string' ctxt (comp_dts (d,ts))) ^ "') not found in oris (typed)",
290 | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =
291 if sel = sel' andalso d = d' andalso (inter op = ts ts') <> [] then
292 ("", (id, vat, sel, d, inter op = ts ts'), ts') else
293 seek_oridts ctxt sel (d, ts) oris;
295 (*.to an input (_,ts) find the according ori and insert the ts.*)
296 fun seek_orits ctxt sel ts [] =
297 ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^
298 "') not found in oris (typed)", e_ori_, [])
299 | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
300 if sel = sel' andalso (inter op = ts ts') <> []
302 then ("", (id,vat,sel,d, inter op = ts ts'):ori, ts')
303 else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])
304 else seek_orits ctxt sel ts oris;
306 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
307 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
308 uncaught exception TYPE
309 > seek_orits thy sel ts [];
310 uncaught exception TYPE
313 (*find_first item with #1 equal to id*)
314 fun seek_ppc id [] = NONE
315 | seek_ppc id (p::(ppc:itm list)) =
316 if id = #1 p then SOME p else seek_ppc id ppc;
320 (*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
323 datatype appl = Appl of tac_ | Notappl of string;
325 fun ppc2list ({Given=gis,Where=whs,Find=fis,
326 With=wis,Relate=res}: 'a ppc) =
327 gis @ whs @ fis @ wis @ res;
328 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
334 (* get the number of variants in a problem in 'original',
335 assumes equal descriptions in immediate sequence *)
337 let fun eq(x,y) = head_of x = head_of y;
338 fun cnt eq [] y n = ([n],[])
339 | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
341 fun coll eq xs [] = xs
342 | coll eq xs (y::ys) =
343 let val (n,ys') = cnt eq (y::ys) y 0;
344 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
345 val vts = subtract op = [1] (distinct (coll eq [] ts));
346 in case vts of [] => 1 | [n] => n
347 | _ => error "different variants in formalization" end;
349 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
350 val it = ([3],[4,5,5,5,5,5]) : int list * int list
351 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
352 val it = [1,3,1,5] : int list
355 fun is_list_type (Type("List.list",_)) = true
356 | is_list_type _ = false;
357 (* fun destr (Type(str,sort)) = (str,sort);
358 > val (SOME ct) = parse thy "lll::real list";
359 > val ty = (#T o rep_cterm) ct;
363 val it = ("List.list",["RealDef.real"]) : string * typ list
364 > atomty ((#t o rep_cterm) ct);
366 *** Free ( lll, real list)
369 > val (SOME ct) = parse thy "[lll::real]";
370 > val ty = (#T o rep_cterm) ct;
374 val it = ("List.list",["'a"]) : string * typ list
375 > atomty ((#t o rep_cterm) ct);
377 *** Const ( List.list.Cons, [real, real list] => real list)
378 *** Free ( lll, real)
379 *** Const ( List.list.Nil, real list)
381 > val (SOME ct) = parse thy "lll";
382 > val ty = (#T o rep_cterm) ct;
384 val it = false : bool *)
387 fun has_list_type (Free(_,T)) = is_list_type T
388 | has_list_type _ = false;
390 > val (SOME ct) = parse thy "lll::real list";
391 > has_list_type (term_of ct);
393 > val (SOME ct) = parse thy "[lll::real]";
394 > has_list_type (term_of ct);
395 val it = false : bool *)
397 fun is_parsed (Syn _) = false
398 | is_parsed _ = true;
399 fun parse_ok its = foldl and_ (true, map is_parsed its);
401 fun all_dsc_in itm_s =
403 fun d_in (Cor ((d,_),_)) = [d]
406 | d_in (Inc ((d,_),_)) = [d]
407 | d_in (Sup (d,_)) = [d]
408 | d_in (Mis (d,_)) = [d];
409 in (flat o (map d_in)) itm_s end;
412 fun is_Syn (Syn _) = true
413 | is_Syn (Typ _) = true
416 fun is_error (Cor (_,ts)) = false
417 | is_error (Sup (_,ts)) = false
418 | is_error (Inc (_,ts)) = false
419 | is_error (Mis (_,ts)) = false
423 fun ct_in (Syn (c)) = c
424 | ct_in (Typ (c)) = c
425 | ct_in _ = error "ct_in called for Cor .. Sup";
428 (*#############################################################*)
429 (*#############################################################*)
430 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
433 (* testdaten besorgen:
434 use"test-coil-kernel.sml";
435 val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
440 variant V: oris union ppc => int, id ID: oris union ppc => int
443 EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
446 @vt = max sum(i : ppc) V i
452 > ((vts_cnt (vts_in itms))) itms;
457 > val vts = vts_in itms;
458 val vts = [1,2,3] : int list
459 > val nvts = vts_cnt vts itms;
460 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
461 > val mx = max2 nvts;
462 val mx = (3,7) : int * int
463 > val v = max_vt itms;
465 --------------------------
469 (*.get the first term in ts from ori.*)
470 (* val (_,_,fd,d,ts) = hd miss;
472 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
473 (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm');
474 (* val t = comp_dts (d,[hd ts]);
477 (* get a term from ori, notyet input in itm.
478 the term from ori is thrown back to a string in order to reuse
479 machinery for immediate input by the user. *)
480 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
481 (fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm')
483 (* in FE dsc, not dat: this is in itms ...*)
484 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
485 | is_untouched _ = false;
488 (* select an item in oris, notyet input in itms
489 (precondition: in itms are only Cor, Sup, Inc) *)
492 | x mem (y :: ys) = x = y orelse x mem ys;
494 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
496 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
497 fun is_elem itms (f,(d,t)) =
498 case find_first (test_d d) itms of
499 SOME _ => true | NONE => false;
500 in case filter_out (is_elem itms) pbt of
501 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
504 SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')
507 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
509 | nxt_add thy oris pbt itms =
511 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
512 andalso (#3 ori) <>"#undef";
513 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
514 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
515 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
516 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
517 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
518 | false_and_not_Sup (i,v,false,f, _) = true
519 | false_and_not_Sup _ = false;
521 val v = if itms = [] then 1 else max_vt itms;
522 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
523 val vits = if v = 0 then itms (*because of dsc without dat*)
524 else filter (testi_vt v) itms; (*itms..vat*)
525 val icl = filter false_and_not_Sup vits; (* incomplete *)
527 then case filter_out (test_id (map #1 vits)) vors of
529 (* val miss = filter_out (test_id (map #1 vits)) vors;
531 | miss => SOME (getr_ct thy (hd miss))
533 case find_first (test_subset (hd icl)) vors of
534 (* val SOME ori = find_first (test_subset (hd icl)) vors;
536 NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
537 | SOME ori => SOME (geti_ct thy ori (hd icl))
543 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
544 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
545 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
546 | mk_delete thy str _ =
547 error ("mk_delete: called with field '"^str^"'");
548 fun mk_additem "#Given" ct = Add_Given ct
549 | mk_additem "#Find" ct = Add_Find ct
550 | mk_additem "#Relate"ct = Add_Relation ct
552 error ("mk_additem: called with field '"^str^"'");
555 (* determine the next step of specification;
556 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
557 eg. in rootpbl 'no_met':
559 preok predicates are _all_ ok (and problem matches completely)
560 oris immediately from formalization
561 (dI',pI',mI') specification coming from author/parent-problem
562 (pbl, item lists specified by user
563 met) -"-, tacitly completed by copy_probl
564 (dI,pI,mI) specification explicitly done by the user
565 (pbt, mpc) problem type, guard of method
567 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
568 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
569 ((*tracing"### nxt_spec Pbl";*)
570 if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
571 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
572 else case find_first (is_error o #5) (pbl:itm list) of
573 SOME (_, _, _, fd, itm_) =>
575 (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
577 ((*tracing"### nxt_spec is_error NONE";*)
578 case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
580 SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
581 (Pbl, mk_additem fd ct'))
582 | NONE => (*pbl-items complete*)
583 if not preok then (Pbl, Refine_Problem pI')
585 if dI = e_domID then (Pbl, Specify_Theory dI')
586 else if pI = e_pblID then (Pbl, Specify_Problem pI')
587 else if mI = e_metID then (Pbl, Specify_Method mI')
589 case find_first (is_error o #5) met of
590 SOME (_,_,_,fd,itm_) =>
591 (Met, mk_delete (assoc_thy dI) fd itm_)
593 (case nxt_add (assoc_thy dI) oris mpc met of
594 SOME (fd,ct') => (*30.8.01: pre?!?*)
595 (Met, mk_additem fd ct')
597 ((*Solv 3.4.00*)Met, Apply_Method mI))))
599 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
600 ((*tracing"### nxt_spec Met"; *)
601 case find_first (is_error o #5) met of
602 SOME (_,_,_,fd,itm_) =>
603 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
605 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
606 SOME (fd,ct') => (Met, mk_additem fd ct')
608 ((*tracing"### nxt_spec Met: nxt_add NONE";*)
609 if dI = e_domID then (Met, Specify_Theory dI')
610 else if pI = e_pblID then (Met, Specify_Problem pI')
611 else if not preok then (Met, Specify_Method mI)
612 else (Met, Apply_Method mI)));
615 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
616 (2,[2],true,"#Find",Syn("empty"))];
619 fun is_field_correct sel d dscpbt =
620 case assoc (dscpbt, sel) of
622 | SOME ds => member op = ds d;
624 (*. update the itm_ already input, all..from ori .*)
625 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
627 fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
629 val ts' = union op = (ts_in itm_) ts;
630 val pval = pbl_ids' d ts'
631 (*WN.9.5.03: FIXXXME [#0, epsilon]
632 here would upd_penv be called for [#0, epsilon] etc. *)
633 val complete = if eq_set op = (ts', all) then true else false;
636 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
637 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
638 | (Syn c) => error ("ori_2itm wants to overwrite "^c)
639 | (Typ c) => error ("ori_2itm wants to overwrite "^c)
640 | (Inc _) => if complete
641 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
642 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
643 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
644 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
645 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
646 (* 28.1.00: not completely clear ---^^^ etc.*)
647 (* 4.9.01: Mis just copied---vvv *)
648 | (Mis _) => if complete
649 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
650 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
654 fun eq1 d (_,(d',_)) = (d = d');
655 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
658 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
659 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
660 pval: value for problem-environment _NOT_ checked for 'inter' --
661 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
662 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
663 (*. is_input ori itms <=>
664 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
665 (2) ori(ts) subset itm(ts) --- Err "already input"
666 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
667 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
668 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
670 fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
671 case find_first (eq1 d) pbt of
673 (case find_first (eq3 f d) itms of
674 SOME (_,_,_,_,itm_) =>
676 val ts' = inter op = (ts_in itm_) ts;
678 if subset op = (ts, ts')
679 then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm)(*2*)
680 else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
682 | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[]))) pid all (i,v,f,d,ts))) (*1*)
683 | NONE => ("", ori_2itm (Sup (d,ts)) e_term all (i,v,f,d,ts));
685 fun test_types ctxt (d,ts) =
687 val opt = (try comp_dts) (d,ts);
688 val msg = case opt of
690 | NONE => (term_to_string' ctxt d ^ " " ^
691 (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped");
694 fun maxl [] = error "maxl of []"
697 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
701 (*. is the input term t known in oris ?
702 give feedback on all(?) strange input;
703 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
704 fun is_known ctxt sel ori t =
706 val _ = tracing ("RM is_known: t=" ^ term2str t);
707 val ots = (distinct o flat o (map #5)) (ori:ori list);
708 val oids = ((map (fst o dest_Free)) o distinct o
709 flat o (map vars)) ots;
710 val (d, ts) = split_dts t;
711 val ids = map (fst o dest_Free)
712 ((distinct o (flat o (map vars))) ts);
713 in if (subtract op = oids ids) <> []
714 then (("identifiers "^(strs2str' (subtract op = oids ids)) ^
715 " not in example"), e_ori_, [])
719 if not (subset op = (map typeless ts, map typeless ots))
720 then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
721 "' not in example (typeless)", e_ori_, [])
723 (case seek_orits ctxt sel ts ori of
724 ("", ori_ as (_,_,_,d,ts), all) =>
725 (case test_types ctxt (d,ts) of
726 "" => ("", ori_, all)
727 | msg => (msg, e_ori_, []))
728 | (msg,_,_) => (msg, e_ori_, []))
730 if member op = (map #4 ori) d
731 then seek_oridts ctxt sel (d,ts) ori
732 else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
735 (*. for return-value of appl_add .*)
738 | Err of string; (*error-message*)
741 (** add an item to the model; check wrt. oris and pbt **)
742 (* in contrary to oris<>[] below, this part handles user-input
743 extremely acceptive, i.e. accept input instead error-msg *)
744 fun appl_add ctxt sel [] ppc pbt ct =
746 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
748 case parseNEW ctxt ct of
749 NONE => Add (i, [], false, sel, Syn ct)
751 let val (d, ts) = split_dts t;
754 then Add (i, [], false, sel, Mis (dsc_unknown, hd ts))
756 (case find_first (eq1 d) pbt of
757 NONE => Add (i, [], true, sel, Sup (d,ts))
758 | SOME (f, (_, id)) =>
759 let fun eq2 d (i, _, _, _, itm_) =
760 d = (d_in itm_) andalso i <> 0;
761 in case find_first (eq2 d) ppc of
762 NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
763 | SOME (i', _, _, _, itm_) =>
767 val in_itm = ts_in itm_;
768 val ts' = union op = ts in_itm;
769 val i'' = if in_itm = [] then i else i';
770 in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts'))) end
771 else Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
775 | appl_add ctxt sel oris ppc pbt str =
776 case parseNEW ctxt str of
777 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
779 case is_known ctxt sel oris t of
781 (case is_notyet_input ctxt ppc all ori' pbt of
783 | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
784 | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
787 (** make oris from args of the stac SubProblem and from pbt **)
788 (* can this formal argument (of a model-pattern) be omitted in the arg-list
789 of a SubProblem ? see ME/ptyps.sml 'type met ' *)
790 fun is_copy_named_idstr str =
791 case (rev o Symbol.explode) str of
792 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
793 "is_copy_named_idstr: " ^ str ^ " T"); true)
794 | _ => (tracing ((strs2str o (rev o Symbol.explode))
795 "is_copy_named_idstr: " ^ str ^ " F"); false);
796 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
798 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
799 fun is_copy_named_generating_idstr str =
800 if is_copy_named_idstr str
801 then case (rev o Symbol.explode) str of
802 "'"::"'"::"'"::_ => false
805 fun is_copy_named_generating (_, (_, t)) =
806 (is_copy_named_generating_idstr o free2str) t;
808 (*.split type-wrapper from scr-arg and build part of an ori;
809 an type-error is reported immediately, raises an exn,
810 subsequent handling of exn provides 2nd part of error message.*)
811 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
812 (* val (thy, (str, (dsc, _)), (ty $ var)) =
815 (Thm.global_cterm_of thy (dsc $ var);(*type check*)
816 SOME ((([1], str, dsc, (*[var]*)
817 split_dts' (dsc, var))): preori)(*:ori without leading #*))
818 handle e as TYPE _ =>
819 (tracing (dashs 70 ^ "\n"
820 ^"*** ERROR while creating the items for the model of the ->problem\n"
821 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
822 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
823 ^"*** description: "^(term_detail2str dsc)
824 ^"*** value: "^(term_detail2str var)
825 ^"*** typeconstructor in script: "^(term_detail2str ty)
826 ^"*** checked by theory: "^(theory2str thy)^"\n"
828 (*OldGoals.print_exn e; raises exn again*)
829 writeln (PolyML.makestring e);
831 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
834 (*.match each pat of the model-pattern with an actual argument;
835 precondition: copy-named vars are filtered out.*)
836 fun matc thy ([]:pat list) _ (oris:preori list) = oris
837 | matc thy pbt [] _ =
839 error ("actual arg(s) missing for '"^pats2str pbt
840 ^"' i.e. should be 'copy-named' by '*_._'"))
841 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
842 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
843 (thy, pbt', ags, []);
845 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
846 (thy, pbt, ags, (oris @ [ori]));
848 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
849 else(*..del?*) let val opt = mtc thy p a;
851 (* val SOME ori = mtc thy p a;
853 SOME ori => matc thy pbt ags (oris @ [ori])
854 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
856 (* run subp-rooteq.sml until Init_Proof before ...
857 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
858 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
860 other vars as in mtc ..
861 > matc thy (drop_last pbt) ags [];
862 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
865 (* generate a new variable "x_i" name from a related given one "x"
866 by use of oris relating "v_i_" (is_copy_named!) to "v_"
867 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
869 (* generate a new variable "x_i" name from a related given one "x"
870 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
871 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
872 but leave is_copy_named_generating as is, e.t. ss''' *)
873 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
874 (if is_copy_named_generating p
875 then (*WN051014 kept strange old code ...*)
876 let fun sel (_,_,d,ts) = comp_ts (d, ts)
877 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
878 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
879 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
880 val vals = map sel oris
881 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
882 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
883 else ([1], field, dsc, [t])
885 handle _ => error ("cpy_nam: for "^(term2str t));
887 (*.match the actual arguments of a SubProblem with a model-pattern
888 and create an ori list (in root-pbl created from formalization).
889 expects ags:pats = 1:1, while copy-named are filtered out of pats;
890 if no 1:1 the exn raised by matc/mtc and handled at call.
891 copy-named pats are appended in order to get them into the model-items.*)
892 fun match_ags thy (pbt:pat list) ags =
893 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
894 val pbt' = filter_out is_copy_named pbt;
895 val cy = filter is_copy_named pbt;
896 val oris' = matc thy pbt' ags [];
897 val cy' = map (cpy_nam pbt' oris') cy;
898 val ors = add_id (oris' @ cy');
899 (*appended in order to get ^^^^^ into the model-items*)
900 in (map flattup ors):ori list end;
902 (*.report part of the error-msg which is not available in match_args.*)
903 fun match_ags_msg pI stac ags =
904 let (*val s = !show_types
905 val _ = show_types:= true*)
906 val pats = (#ppc o get_pbt) pI
907 val msg = (dots 70^"\n"
908 ^"*** problem "^strs2str pI^" has the ...\n"
909 ^"*** model-pattern "^pats2str pats^"\n"
910 ^"*** stac '"^term2str stac^"' has the ...\n"
911 ^"*** arg-list "^terms2str ags^"\n"
913 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
914 (*val _ = show_types:= s*)
918 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
919 fun vars_of_pbl_ pbl_ =
920 let fun var_of_pbl_ (gfr,(dsc,t)) = t
921 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
922 fun vars_of_pbl_' pbl_ =
923 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
924 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
926 fun overwrite_ppc thy itm ppc =
928 fun repl ppc' (_,_,_,_,itm_) [] =
929 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
931 | repl ppc' itm (p::ppc) =
932 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
933 else repl (ppc' @ [p]) itm ppc
934 in repl [] itm ppc end;
936 (*10.3.00: insert the already compiled itm into model;
937 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
940 fun insert_ppc thy itm ppc =
942 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
943 | eq_untouched _ _ = false;
946 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
947 case seek_ppc (#1 itm) ppc of
948 (* val SOME xxx = seek_ppc (#1 itm) ppc;
950 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
951 overwrite_ppc thy itm ppc
952 | NONE => (ppc @ [itm]));
953 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
955 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
956 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
958 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
959 (d_in itm_) = (d_in iitm_);
960 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
961 handles superfluous items carelessly*)
962 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
964 > gen_ins' eee (4,[1,3,5,7]);
965 val it = [1, 3, 5, 7, 4] : int list*)
968 (*. output the headline to a ppc .*)
969 fun header p_ pI mI =
970 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
972 | pos => error ("header called with "^ pos_2str pos);
975 fun specify_additem sel (ct,_) (p, Met) c pt =
977 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
978 probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
979 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
980 val cpI = if pI = e_pblID then pI' else pI;
981 val cmI = if mI = e_metID then mI' else mI;
982 val {ppc,pre,prls,...} = get_met cmI;
984 case appl_add ctxt sel oris met ppc ct of
985 Add itm (*..union old input *) =>
987 val met' = insert_ppc thy itm met;
988 val ((p, Met), _, _, pt') =
989 generate1 thy (case sel of
990 "#Given" => Add_Given' (ct, met')
991 | "#Find" => Add_Find' (ct, met')
992 | "#Relate"=> Add_Relation'(ct, met'))
993 (Uistate, ctxt) (p, Met) pt
994 val pre' = check_preconds thy prls pre met'
995 val pb = foldl and_ (true, map fst pre')
997 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
998 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
999 in ((p, p_), ((p, p_), Uistate),
1000 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1001 (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
1005 val pre' = check_preconds thy prls pre met
1006 val pb = foldl and_ (true, map fst pre')
1008 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1009 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1010 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1013 | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt =
1015 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1016 probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1017 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1018 val cpI = if pI = e_pblID then pI' else pI;
1019 val cmI = if mI = e_metID then mI' else mI;
1020 val {ppc,where_,prls,...} = get_pbt cpI;
1022 case appl_add ctxt sel oris pbl ppc ct of
1023 Add itm (*..union old input *) =>
1025 val pbl' = insert_ppc thy itm pbl
1026 val ((p, Pbl), _, _, pt') =
1027 generate1 thy (case sel of
1028 "#Given" => Add_Given' (ct, pbl')
1029 | "#Find" => Add_Find' (ct, pbl')
1030 | "#Relate"=> Add_Relation'(ct, pbl'))
1031 (Uistate, ctxt) (p,Pbl) pt
1032 val pre = check_preconds thy prls where_ pbl'
1033 val pb = foldl and_ (true, map fst pre)
1035 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1036 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1037 val ppc = if p_= Pbl then pbl' else met;
1038 in ((p,p_), ((p,p_),Uistate),
1039 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1040 (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt,Safe,pt')
1044 val pre = check_preconds thy prls where_ pbl
1045 val pb = foldl and_ (true, map fst pre)
1047 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1048 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1049 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1052 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1053 let (* either """"""""""""""" all empty or complete *)
1054 val thy = assoc_thy dI';
1056 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
1058 else pI' |> #ppc o get_pbt |> prep_ori fmz thy
1059 val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1060 (oris, (dI',pI',mI'), e_term)
1061 val pt = update_ctxt pt [] ctxt
1062 val {ppc, prls, where_, ...} = get_pbt pI'
1063 val (pbl, pre, pb) = ([], [], false)
1067 (([], Pbl), (([], Pbl), Uistate),
1068 Form' (PpcKF (0, EdUndef, (length []), Nundef,
1069 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1070 Refine_Tacitly pI', Safe, pt)
1072 (([], Pbl), (([], Pbl), Uistate),
1073 Form' (PpcKF (0, EdUndef, (length []), Nundef,
1074 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1075 Model_Problem, Safe, pt)
1078 (*ONLY for STARTING modeling phase*)
1079 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1081 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_), ctxt, ...}) = get_obj I pt p
1082 val thy' = if dI = e_domID then dI' else dI
1083 val thy = assoc_thy thy'
1084 val {ppc,prls,where_,...} = get_pbt pI'
1085 val pre = check_preconds thy prls where_ pbl
1086 val pb = foldl and_ (true, map fst pre)
1087 val ((p,_),_,_,pt) =
1088 generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1089 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1090 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1091 in ((p, Pbl), ((p, p_), Uistate),
1092 Form' (PpcKF (0, EdUndef, length p, Nundef,
1093 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1097 (*. called only if no_met is specified .*)
1098 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1100 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ctxt, ...}) = get_obj I pt p;
1101 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1102 val (domID, metID) =
1103 (string_of_thy thy, if length met = 0 then e_metID else hd met)
1104 val ((p,_),_,_,pt) =
1105 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1106 (Uistate, ctxt) pos pt
1107 val (pbl, pre, pb) = ([], [], false)
1108 in ((p, Pbl), (pos, Uistate),
1109 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1110 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1111 Model_Problem, Safe, pt)
1114 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1116 val ctxt = get_ctxt pt pos
1118 generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1119 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1120 Model_Problem, Safe, pt)
1122 (*WN110515 initialise ctxt again from itms and add preconds*)
1123 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1125 val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1126 meth=met, ctxt, ...}) = get_obj I pt p;
1127 val thy = assoc_thy dI
1128 val ((p,Pbl),_,_,pt)=
1129 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt
1130 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1131 val mI'' = if mI=e_metID then mI' else mI;
1133 nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1134 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1135 in ((p,Pbl), (pos,Uistate),
1136 Form' (PpcKF (0,EdUndef,(length p),Nundef, (Problem pI, itms2itemppc dI'' itms pre))),
1139 (*WN110515 initialise ctxt again from itms and add preconds*)
1140 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1142 val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1143 meth=met, ctxt, ...}) = get_obj I pt p;
1144 val {ppc,pre,prls,...} = get_met mID
1145 val thy = assoc_thy dI
1146 val oris = add_field' thy ppc oris;
1147 val dI'' = if dI=e_domID then dI' else dI;
1148 val pI'' = if pI = e_pblID then pI' else pI;
1149 val met = if met=[] then pbl else met;
1150 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1151 val (pos, _, _, pt) =
1152 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1154 nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1155 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1156 in (pos, (pos,Uistate),
1157 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1158 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1162 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1163 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1164 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1166 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1168 val p_ = case p_ of Met => Met | _ => Pbl
1169 val thy = assoc_thy domID;
1170 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1171 probl=pbl, spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1172 val mppc = case p_ of Met => met | _ => pbl;
1173 val cpI = if pI = e_pblID then pI' else pI;
1174 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1175 val cmI = if mI = e_metID then mI' else mI;
1176 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1179 Met => (check_preconds thy mer mwh met)
1180 | _ => (check_preconds thy per pwh pbl)
1181 val pb = foldl and_ (true, map fst pre)
1185 let val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1186 (pbl,met) (ppc,mpc) (dI,pI,mI);
1187 in ((p,p_), (pos,Uistate),
1188 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1189 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1192 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1194 val ((p,p_),_,_,pt) =
1195 generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1197 nxt_spec p_ pb oris (dI',pI',mI') (pbl,met) (ppc,mpc) (domID,pI,mI);
1198 in ((p,p_), (pos,Uistate),
1199 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1200 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1205 | specify m' _ _ _ =
1206 error ("specify: not impl. for " ^ tac_2str m');
1208 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
1209 -- for input from scratch*)
1210 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1212 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1213 probl=pbl,spec=(dI,pI,_), ctxt, ...}) = get_obj I pt p;
1214 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1215 val cpI = if pI = e_pblID then pI' else pI;
1217 case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
1218 Add itm (*..union old input *) =>
1220 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1221 val pbl' = insert_ppc thy itm pbl
1224 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1225 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1226 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1227 val ((p,Pbl),c,_,pt') =
1228 generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt
1229 in ([(tac,tac_,((p,Pbl),(Uistate, ctxt)))], c, (pt',(p,Pbl))):calcstate'
1231 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1232 FIXME ..and dont abuse a tactic for that purpose*)
1233 ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1234 (e_pos', (e_istate, e_ctxt)))], [], ptp)
1237 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1239 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1240 probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1241 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1242 val cmI = if mI = e_metID then mI' else mI;
1244 case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
1245 Add itm (*..union old input *) =>
1247 val met' = insert_ppc thy itm met;
1250 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1251 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1252 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1253 val ((p,Met),c,_,pt') =
1254 generate1 thy tac_ (Uistate, ctxt) (p,Met) pt
1255 in ([(tac,tac_,((p,Met), (Uistate, ctxt)))], c, (pt',(p,Met))) end
1256 | Err msg => ([(*tacis*)], [], ptp)
1257 (*nxt_me collects tacis until not hide; here just no progress*)
1260 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1261 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1262 handle _ => error ("ori2Coritm: dsc "^
1264 "in ori, but not in pbt")
1266 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1267 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1268 (find_first (eq1 d))) pbt,ts))):itm)
1269 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1270 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1273 (*filter out oris which have same description in itms*)
1274 fun filter_outs oris [] = oris
1275 | filter_outs oris (i::itms) =
1276 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1277 (#4:ori -> term)) oris;
1278 in filter_outs ors itms end;
1280 fun memI a b = member op = a b;
1281 (*filter oris which are in pbt, too*)
1282 fun filter_pbt oris pbt =
1283 let val dscs = map (fst o snd) pbt
1284 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1286 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1287 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1289 fun x mem [] = false
1290 | x mem (y :: ys) = x = y orelse x mem ys;
1292 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1293 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1295 let val vat = max_vt pits;
1297 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1298 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1299 val os = filter_outs ors itms;
1300 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1301 in itms @ (map (ori2Coritm met) os) end
1306 (*.complete model and guard of a calc-head .*)
1308 fun x mem [] = false
1309 | x mem (y :: ys) = x = y orelse x mem ys;
1311 fun complete_mod_ (oris, mpc, ppc, probl) =
1312 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1313 val vat = if probl = [] then 1 else max_vt probl
1314 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1315 val pors = filter_outs pors pits (*which are in pbl already*)
1316 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1318 val pits = pits @ (map (ori2Coritm ppc) pors)
1319 val mits = complete_metitms oris pits [] mpc
1323 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1324 (if dI = e_domID then odI else dI,
1325 if pI = e_pblID then opI else pI,
1326 if mI = e_metID then omI else mI):spec;
1329 (*.find a next applicable tac (for calcstate) and update ptree
1330 (for ev. finding several more tacs due to hide).*)
1331 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1332 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1333 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1334 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1336 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p
1337 val (dI, pI, mI) = some_spec ospec spec
1338 val thy = assoc_thy dI
1339 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1340 val {cas, ppc, ...} = get_pbt pI
1341 val pbl = init_pbl ppc (* fill in descriptions *)
1342 (*----------------if you think, this should be done by the Dialog
1343 in the java front-end, search there for WN060225-modelProblem----*)
1345 case cas of NONE => (pbl, [])
1346 | _ => complete_mod_ (oris, mpc, ppc, probl)
1347 (*----------------------------------------------------------------*)
1348 val tac_ = Model_Problem' (pI, pbl, met)
1349 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, ctxt) pos pt
1350 in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1352 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1353 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1354 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1356 (*. called only if no_met is specified .*)
1357 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1359 val (PblObj {origin = (oris, (dI,_,_),_), ctxt, ...}) = get_obj I pt p
1360 val opt = refine_ori oris pI
1365 val {met,ppc,...} = get_pbt pI'
1366 val pbl = init_pbl ppc
1367 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1368 val mI = if length met = 0 then e_metID else hd met
1369 val thy = assoc_thy dI
1371 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1372 (Uistate, ctxt) pos pt
1373 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1374 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1376 | NONE => ([], [], ptp)
1379 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1381 val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), probl, ctxt, ...}) = get_obj I pt p
1382 val thy = if dI' = e_domID then dI else dI'
1384 case refine_pbl (assoc_thy thy) pI probl of
1385 NONE => ([], [], ptp)
1386 | SOME (rfd as (pI',_)) =>
1388 val (pos,c,_,pt) = generate1 (assoc_thy thy)
1389 (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1390 in ([(Refine_Problem pI, Refine_Problem' rfd,
1391 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1395 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1397 val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...}) = get_obj I pt p;
1398 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1399 val {ppc,where_,prls,...} = get_pbt pI
1400 val pbl as (_,(itms,_)) =
1401 if pI'=e_pblID andalso pI=e_pblID
1402 then (false, (init_pbl ppc, []))
1403 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1404 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1405 val ((p,Pbl),c,_,pt) =
1406 generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt
1407 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1408 (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1411 (*transfers oris (not required in pbl) to met-model for script-env
1412 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1413 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1415 val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1416 meth=met, ctxt, ...}) = get_obj I pt p;
1417 val {ppc,pre,prls,...} = get_met mID
1418 val thy = assoc_thy dI
1419 val oris = add_field' thy ppc oris;
1420 val dI'' = if dI=e_domID then dI' else dI;
1421 val pI'' = if pI = e_pblID then pI' else pI;
1422 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1423 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1425 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1426 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1427 (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1430 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1432 val ctxt = get_ctxt pt pos
1433 val (dI',_,_) = get_obj g_spec pt p
1435 generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1436 in (*FIXXXME: check if pbl can still be parsed*)
1437 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
1441 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1443 val ctxt = get_ctxt pt pos
1444 val (dI',_,_) = get_obj g_spec pt p
1446 generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1447 in (*FIXXXME: check if met can still be parsed*)
1448 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
1453 error ("nxt_specif: not impl. for "^tac2str m');
1455 (* get the values from oris; handle the term list w.r.t. penv *)
1457 fun x mem [] = false
1458 | x mem (y :: ys) = x = y orelse x mem ys;
1460 fun vals_of_oris oris =
1461 ((map (mkval' o (#5:ori -> term list))) o
1462 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1465 (* create a calc-tree with oris via an cas.refined pbl *)
1466 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1468 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1470 val {cas, met, ppc, thy, ...} = get_pbt pI
1471 val dI = if dI = "" then theory2theory' thy else dI
1472 val thy = assoc_thy dI
1473 val mI = if mI = [] then hd met else mI
1474 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1475 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1476 ([], (dI,pI,mI), hdl)
1477 val pt = update_spec pt [] (dI,pI,mI)
1478 val pits = init_pbl' ppc
1479 val pt = update_pbl pt [] pits
1480 in ((pt, ([] ,Pbl)), []) : calcstate end
1483 then (* from met-browser *)
1485 val {ppc,...} = get_met mI
1486 val dI = if dI = "" then "Isac" else dI
1487 val thy = assoc_thy dI;
1488 val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1489 ([], (dI,pI,mI), e_term(*FIXME met*));
1490 val pt = update_spec pt [] (dI,pI,mI);
1491 val mits = init_pbl' ppc;
1492 val pt = update_met pt [] mits;
1493 in ((pt, ([], Met)), []) : calcstate end
1494 else (* new example, pepare for interactive modeling *)
1495 let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1496 ([], e_spec, e_term)
1497 in ((pt, ([], Pbl)), []) : calcstate end
1499 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1500 let (* both """"""""""""""""""""""""" either empty or complete *)
1501 val thy = assoc_thy dI
1502 val (pI, (pors, pctxt), mI) =
1506 val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
1507 val pI' = refine_ori' pors pI;
1508 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1509 (hd o #met o get_pbt) pI') end
1510 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
1511 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1512 val dI = theory2theory' (maxthy thy thy')
1515 NONE => pblterm dI pI
1516 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
1517 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
1518 (pors, (dI, pI, mI), hdl)
1519 val pt = update_ctxt pt [] pctxt
1520 in ((pt, ([], Pbl)),
1521 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1527 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1528 (* case appl_spec p pt m of /// 19.1.00
1529 Notappl e => Error' (Error_ e)
1531 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1535 (*fun tag_form thy (formal, given) = Thm.global_cterm_of thy
1536 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1537 fun tag_form thy (formal, given) =
1539 val gf = (head_of given) $ formal;
1540 val _ = Thm.global_cterm_of thy gf
1542 handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
1543 " .. " ^ term_to_string''' thy formal ^ " ..types do not match");
1544 (* val formal = (the o (parse thy)) "[R::real]";
1545 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1546 > tag_form thy (formal, given);
1547 val it = "fixed_values [R]" : cterm
1550 fun chktyp thy (n, fs, gs) =
1551 ((writeln o (term_to_string''' thy) o (nth n)) fs;
1552 (writeln o (term_to_string''' thy) o (nth n)) gs;
1553 tag_form thy (nth n fs, nth n gs));
1554 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1556 (* #####################################################
1557 find the failing item:
1559 > val tag__form = chktyp (n,formals,givens);
1560 > (type_of o term_of o (nth n)) formals;
1561 > (type_of o term_of o (nth n)) givens;
1562 > atomty ((term_of o (nth n)) formals);
1563 > atomty ((term_of o (nth n)) givens);
1564 > atomty (term_of tag__form);
1565 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1566 ##################################################### *)
1568 (* #####################################################
1570 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1571 val formals = map (the o (parse thy)) origin;
1573 val given = ["equation (lhs=rhs)",
1574 "bound_variable bdv", (* TODO type *)
1576 val where_ = ["e is_root_equation_in bdv",
1578 "apx is_const_expr"];
1579 val find = ["L::rat set"];
1580 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1581 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1582 val givens = map (the o (parse thy)) given;
1584 val tag__forms = chktyps (formals, givens);
1585 map ((atomty) o term_of) tag__forms;
1586 ##################################################### *)
1589 (* check pbltypes, announces one failure a time *)
1590 (*fun chk_vars ctppc =
1591 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1592 appc flat (mappc (vars o term_of) ctppc)
1593 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1594 else if (re\\(gi union fi)) <> []
1595 then ("re\\(gi union fi)",re\\(gi union fi))
1596 else ("ok",[]) end;*)
1597 fun chk_vars ctppc =
1598 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1599 appc flat (mappc vars ctppc)
1600 val chked = subtract op = gi wh
1601 in if chked <> [] then ("wh\\gi", chked)
1602 else let val chked = subtract op = (union op = gi fi) re
1604 then ("re\\(gi union fi)", chked)
1609 (* check a new pbltype: variables (Free) unbound by given, find*)
1610 fun unbound_ppc ctppc =
1611 let val {Given=gi,Find=fi,Relate=re,...} =
1612 appc flat (mappc vars ctppc)
1613 in distinct (*re\\(gi union fi)*)
1614 (subtract op = (union op = gi fi) re) end;
1616 > val org = {Given=["[R=(R::real)]"],Where=[],
1617 Find=["[A::real]"],With=[],
1618 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1620 > val ctppc = mappc (the o (parse thy)) org;
1621 > unbound_ppc ctppc;
1622 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1626 (* f, a binary operator, is nested rightassociative *)
1629 fun fld f (x::[]) = x
1630 | fld f (x::x'::[]) = f (x',x)
1631 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1632 in ((fld f) o rev) xs end;
1634 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1635 > val ces = map (Thm.global_cterm_of thy) (isalist2list (term_of ct));
1636 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1637 > Thm.global_cterm_of thy conj;
1638 val it = "(a = b & c = d) & e = f" : cterm
1641 (* f, a binary operator, is nested leftassociative *)
1642 fun foldl1 f (x::[]) = x
1643 | foldl1 f (x::x'::[]) = f (x,x')
1644 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1646 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1647 > val ces = map (Thm.global_cterm_of thy) (isalist2list (term_of ct));
1648 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1649 > Thm.global_cterm_of thy conj;
1650 val it = "a = b & c = d & e = f & g = h" : cterm
1654 (* called only once, if a Subproblem has been located in the script*)
1655 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_,_)) ptp =
1658 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1659 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1660 (*all stored in tac_ itms^^^^^^^^^^*)
1661 | nxt_model_pbl tac_ _ =
1662 error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_);
1664 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1665 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1666 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1669 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1670 + met from fmz; assumes pos on PblObj, meth = [].*)
1671 fun complete_mod (pt, pos as (p, p_):pos') =
1672 (* val (pt, (p, _)) = (pt, p);
1673 val (pt, (p, _)) = (pt, pos);
1675 let val _= if p_ <> Pbl
1676 then tracing("###complete_mod: only impl.for Pbl, called with "^
1677 pos'2str pos) else ()
1678 val (PblObj{origin=(oris, ospec, hdl), probl, spec, ...}) =
1680 val (dI,pI,mI) = some_spec ospec spec
1681 val mpc = (#ppc o get_met) mI
1682 val ppc = (#ppc o get_pbt) pI
1683 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1684 val pt = update_pblppc pt p pits
1685 val pt = update_metppc pt p mits
1686 in (pt, (p,Met):pos') end
1688 (*| complete_mod (pt, pos as (p, Met):pos') =
1689 error ("###complete_mod: only impl.for Pbl, called with "^
1692 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1693 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1694 fun all_modspec (pt, (p,_):pos') =
1696 val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
1697 val thy = assoc_thy dI;
1698 val {ppc, ...} = get_met mI;
1699 val (fmz_, vals) = oris2fmz_vals pors;
1700 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
1701 |> declare_constraints' vals
1702 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1703 val pt = update_metppc pt p (map (ori2Coritm ppc) pors); (*WN110716 = _pblppc ?!?*)
1704 val pt = update_spec pt p (dI,pI,mI);
1705 val pt = update_ctxt pt p ctxt
1707 val mors = prep_ori fmz_ thy ppc |> #1;
1708 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1709 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1710 (*WN110715: why pors, mors handled so differently?*)
1711 val pt = update_spec pt p (dI,pI,mI);
1713 in (pt, (p,Met): pos') end;
1715 (*WN0312: use in nxt_spec, too ? what about variants ???*)
1716 fun is_complete_mod_ ([]: itm list) = false
1717 | is_complete_mod_ itms =
1718 foldl and_ (true, (map #3 itms));
1720 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1721 if (is_pblobj o (get_obj I pt)) p
1722 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1723 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1724 | is_complete_mod (pt, pos as (p, Met)) =
1725 if (is_pblobj o (get_obj I pt)) p
1726 then (is_complete_mod_ o (get_obj g_met pt)) p
1727 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1728 | is_complete_mod (_, pos) =
1729 error ("is_complete_mod called by " ^ pos'2str pos ^
1730 " (should be Pbl or Met)");
1732 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1733 fun is_complete_spec (pt, pos as (p,_): pos') =
1734 if (not o is_pblobj o (get_obj I pt)) p
1735 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1736 else let val (dI,pI,mI) = get_obj g_spec pt p
1737 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1738 (*.complete empty items in specification from origin (pbl, met ev.refined);
1739 assumes 'is_complete_mod'.*)
1740 fun complete_spec (pt, pos as (p,_): pos') =
1741 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1742 val pt = update_spec pt p (some_spec ospec spec)
1745 fun is_complete_modspec ptp =
1746 is_complete_mod ptp andalso is_complete_spec ptp;
1751 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1752 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1754 let val (_,_,metID) = get_somespec' spec spec'
1756 if metID = e_metID then []
1757 else let val {prls,pre=where_,...} = get_met metID
1758 val pre = check_preconds' prls where_ meth 0
1760 val allcorrect = is_complete_mod_ meth
1761 andalso foldl and_ (true, (map #1 pre))
1762 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1763 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1764 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1766 let val (_,pI,_) = get_somespec' spec spec'
1768 if pI = e_pblID then []
1769 else let val {prls,where_,cas,...} = get_pbt pI
1770 val pre = check_preconds' prls where_ probl 0
1772 val allcorrect = is_complete_mod_ probl
1773 andalso foldl and_ (true, (map #1 pre))
1774 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1777 fun pt_form (PrfObj {form,...}) = Form form
1778 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1779 let val (dI, pI, _) = get_somespec' spec spec'
1780 val {cas,...} = get_pbt pI
1782 NONE => Form (pblterm dI pI)
1783 | SOME t => Form (subst_atomic (mk_env probl) t)
1785 (*vvv takes the tac _generating_ the formula=result, asm ok....
1786 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1788 if null asm then NONE else SOME asm,
1790 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1791 let val (_,_,metID) = some_spec ospec spec
1793 if null asm then NONE else SOME asm,
1794 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1795 -------------------------------------------------------------------------*)
1798 (*.pt_extract returns
1799 # the formula at pos
1800 # the tactic applied to this formula
1801 # the list of assumptions generated at this formula
1802 (by application of another tac to the preceding formula !)
1803 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1804 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1805 fun pt_extract (pt,([],Res)) = (* WN120512: --returns--> Check_Postcondition WRONGLY
1806 see --- build fun is_exactly_equal*)
1807 (* ML_TODO 110417 get assumptions from ctxt !? *)
1808 let val (f, asm) = get_obj g_result pt []
1809 in (Form f, NONE, asm) end
1810 | pt_extract (pt,(p,Res)) =
1812 val (f, asm) = get_obj g_result pt p
1816 if is_pblobj' pt (lev_up p)
1819 val (PblObj{spec=(_,pI,_),...}) = get_obj I pt (lev_up p)
1820 in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
1821 else SOME End_Trans (*WN0502 TODO for other branches*)
1823 let val p' = lev_on p
1827 let val (PblObj{origin = (_,(dI,pI,_),_),...}) = get_obj I pt p'
1828 in SOME (Subproblem (dI, pI)) end
1830 if f = get_obj g_form pt p'
1831 then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
1832 else SOME (Take (term2str (get_obj g_form pt p')))
1834 in (Form f, tac, asm) end
1835 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1837 val ppobj = get_obj I pt p
1838 val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
1839 val tac = g_tac ppobj
1840 in (f, SOME tac, []) end;
1843 (**. get the formula from a ctree-node:
1844 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1845 take res from all other PrfObj's .**)
1846 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1847 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1848 [("headline", (p, Frm), h),
1849 ("stepform", (p, Res), r)]
1850 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1851 [("stepform", (p, Frm), form),
1852 ("stepform", (p, Res), r)];
1854 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1855 [("stepform", (p, Res), r)]
1857 (*assumes to take whole level, in particular hd -- for use in interSteps*)
1858 fun get_formress fs p [] = flat fs
1859 | get_formress fs p (nd::nds) =
1860 (* start with 'form+res' and continue with trying 'res' only*)
1861 get_forms (fs @ [formres p nd]) (lev_on p) nds
1862 and get_forms fs p [] = flat fs
1863 | get_forms fs p (nd::nds) =
1865 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1866 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1867 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1868 (* continue with trying 'res' only*)
1869 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1871 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1872 (*WN050219 made robust against _'to' below or after Complete nodes
1873 by handling exn caused by move_dn*)
1874 (*WN0401 this functionality belongs to ctree.sml,
1875 but fetching a calc_head requires calculations defined in modspec.sml
1876 transfer to ME/me.sml !!!
1877 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1878 is returned !!!!!!!!!!!!!
1880 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1881 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1882 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1886 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1890 | eq_pos' _ _ = false;
1892 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
1893 total ordering Position#compareTo(Position p) in the java-code
1894 val get_interval = fn
1895 : pos' -> : from is "move_up 1st-element" to return
1896 pos' -> : to the last element to be returned; from < to
1897 int -> : level: 0 gets the flattest sub-tree possible
1898 >999 gets the deepest sub-tree possible
1900 (pos' * : of the formula
1901 Term.term) : the formula
1904 fun get_interval from to level pt =
1906 fun get_inter c (from:pos') (to:pos') lev pt =
1907 if eq_pos' from to orelse from = ([],Res)
1908 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
1909 if 'to' has values NOT generated by move_dn, see systest/me.sml
1910 TODO.WN0501: introduce an order on pos' and check "from > to"..
1911 ...there is an order in Java!
1912 WN051224 the hack got worse with returning term instead ptform*)
1914 let val (f,_,_) = pt_extract (pt, from)
1917 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
1918 | Form t => c @ [(from, t)]
1921 if lev < lev_of from
1922 then (get_inter c (move_dn [] pt from) to lev pt)
1923 handle (PTREE _(*from move_dn too far*)) => c
1926 val (f,_,_) = pt_extract (pt, from)
1927 val term = case f of
1928 ModSpec (_,_,headline,_,_,_) => headline
1930 in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)
1931 handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]
1933 in get_inter [] from to level pt end;
1936 fun posform2str (pos:pos', form) =
1937 "("^ pos'2str pos ^", "^
1939 Form f => term2str f
1940 | ModSpec c => term2str (#3 c(*the headline*)))
1942 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
1943 (map posform2str)) pfs;
1944 fun posterm2str (pos:pos', t) =
1945 "("^ pos'2str pos ^", "^term2str t^")";
1946 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
1947 (map posterm2str)) pfs;
1950 (*WN050225 omits the last step, if pt is incomplete*)
1952 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
1954 (*.get a calchead from a PblObj-node in the ctree;
1955 preconditions must be calculated.*)
1956 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
1957 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
1959 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
1960 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
1961 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
1962 | get_ocalhd (pt, pos' as (p,Met):pos') =
1963 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1966 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
1967 val pre = check_preconds (assoc_thy"Isac") prls pre meth
1968 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
1970 (*.at the activeFormula set the Model, the Guard and the Specification
1971 to empty and return a CalcHead;
1972 the 'origin' remains (for reconstructing all that).*)
1973 fun reset_calchead (pt, pos' as (p,_):pos') =
1974 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
1975 val pt = update_pbl pt p []
1976 val pt = update_met pt p []
1977 val pt = update_spec pt p e_spec
1978 in (pt, (p,Pbl):pos') end;