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 (Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))) ^
288 "') not found in oris (typed)",
291 | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =
292 if sel = sel' andalso d = d' andalso (inter op = ts ts') <> [] then
293 ("", (id, vat, sel, d, inter op = ts ts'), ts') else
294 seek_oridts ctxt sel (d, ts) oris;
296 (*.to an input (_,ts) find the according ori and insert the ts.*)
297 fun seek_orits ctxt sel ts [] =
298 ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
300 "') not found in oris (typed)", e_ori_, [])
301 | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
302 if sel = sel' andalso (inter op = ts ts') <> []
305 (id,vat,sel,d, inter op = ts ts'):ori,
307 else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
312 else seek_orits ctxt sel ts oris;
314 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
315 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
316 uncaught exception TYPE
317 > seek_orits thy sel ts [];
318 uncaught exception TYPE
321 (*find_first item with #1 equal to id*)
322 fun seek_ppc id [] = NONE
323 | seek_ppc id (p::(ppc:itm list)) =
324 if id = #1 p then SOME p else seek_ppc id ppc;
328 (*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
331 datatype appl = Appl of tac_ | Notappl of string;
333 fun ppc2list ({Given=gis,Where=whs,Find=fis,
334 With=wis,Relate=res}: 'a ppc) =
335 gis @ whs @ fis @ wis @ res;
336 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
342 (* get the number of variants in a problem in 'original',
343 assumes equal descriptions in immediate sequence *)
345 let fun eq(x,y) = head_of x = head_of y;
346 fun cnt eq [] y n = ([n],[])
347 | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
349 fun coll eq xs [] = xs
350 | coll eq xs (y::ys) =
351 let val (n,ys') = cnt eq (y::ys) y 0;
352 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
353 val vts = subtract op = [1] (distinct (coll eq [] ts));
354 in case vts of [] => 1 | [n] => n
355 | _ => error "different variants in formalization" end;
357 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
358 val it = ([3],[4,5,5,5,5,5]) : int list * int list
359 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
360 val it = [1,3,1,5] : int list
363 fun is_list_type (Type("List.list",_)) = true
364 | is_list_type _ = false;
365 (* fun destr (Type(str,sort)) = (str,sort);
366 > val (SOME ct) = parse thy "lll::real list";
367 > val ty = (#T o rep_cterm) ct;
371 val it = ("List.list",["RealDef.real"]) : string * typ list
372 > atomty ((#t o rep_cterm) ct);
374 *** Free ( lll, real list)
377 > val (SOME ct) = parse thy "[lll::real]";
378 > val ty = (#T o rep_cterm) ct;
382 val it = ("List.list",["'a"]) : string * typ list
383 > atomty ((#t o rep_cterm) ct);
385 *** Const ( List.list.Cons, [real, real list] => real list)
386 *** Free ( lll, real)
387 *** Const ( List.list.Nil, real list)
389 > val (SOME ct) = parse thy "lll";
390 > val ty = (#T o rep_cterm) ct;
392 val it = false : bool *)
395 fun has_list_type (Free(_,T)) = is_list_type T
396 | has_list_type _ = false;
398 > val (SOME ct) = parse thy "lll::real list";
399 > has_list_type (term_of ct);
401 > val (SOME ct) = parse thy "[lll::real]";
402 > has_list_type (term_of ct);
403 val it = false : bool *)
405 fun is_parsed (Syn _) = false
406 | is_parsed _ = true;
407 fun parse_ok its = foldl and_ (true, map is_parsed its);
409 fun all_dsc_in itm_s =
411 fun d_in (Cor ((d,_),_)) = [d]
414 | d_in (Inc ((d,_),_)) = [d]
415 | d_in (Sup (d,_)) = [d]
416 | d_in (Mis (d,_)) = [d];
417 in (flat o (map d_in)) itm_s end;
420 fun is_Syn (Syn _) = true
421 | is_Syn (Typ _) = true
424 fun is_error (Cor (_,ts)) = false
425 | is_error (Sup (_,ts)) = false
426 | is_error (Inc (_,ts)) = false
427 | is_error (Mis (_,ts)) = false
431 fun ct_in (Syn (c)) = c
432 | ct_in (Typ (c)) = c
433 | ct_in _ = error "ct_in called for Cor .. Sup";
436 (*#############################################################*)
437 (*#############################################################*)
438 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
441 (* testdaten besorgen:
442 use"test-coil-kernel.sml";
443 val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
448 variant V: oris union ppc => int, id ID: oris union ppc => int
451 EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
454 @vt = max sum(i : ppc) V i
460 > ((vts_cnt (vts_in itms))) itms;
465 > val vts = vts_in itms;
466 val vts = [1,2,3] : int list
467 > val nvts = vts_cnt vts itms;
468 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
469 > val mx = max2 nvts;
470 val mx = (3,7) : int * int
471 > val v = max_vt itms;
473 --------------------------
477 (*.get the first term in ts from ori.*)
478 (* val (_,_,fd,d,ts) = hd miss;
480 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
481 (fd, (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) o
482 comp_dts) (d,[hd ts]) : cterm');
483 (* val t = comp_dts (d,[hd ts]);
486 (* get a term from ori, notyet input in itm.
487 the term from ori is thrown back to a string in order to reuse
488 machinery for immediate input by the user. *)
489 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
490 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
491 (d, subtract op = (ts_in itm_) ts) : cterm');
492 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
493 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
494 (d, subtract op = (ts_in itm_) ts) : cterm');
496 (* in FE dsc, not dat: this is in itms ...*)
497 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
498 | is_untouched _ = false;
501 (* select an item in oris, notyet input in itms
502 (precondition: in itms are only Cor, Sup, Inc) *)
505 | x mem (y :: ys) = x = y orelse x mem ys;
507 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
509 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
510 fun is_elem itms (f,(d,t)) =
511 case find_first (test_d d) itms of
512 SOME _ => true | NONE => false;
513 in case filter_out (is_elem itms) pbt of
514 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
518 ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
519 comp_dts) (d, []) : cterm')
522 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
524 | nxt_add thy oris pbt itms =
526 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
527 andalso (#3 ori) <>"#undef";
528 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
529 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
530 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
531 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
532 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
533 | false_and_not_Sup (i,v,false,f, _) = true
534 | false_and_not_Sup _ = false;
536 val v = if itms = [] then 1 else max_vt itms;
537 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
538 val vits = if v = 0 then itms (*because of dsc without dat*)
539 else filter (testi_vt v) itms; (*itms..vat*)
540 val icl = filter false_and_not_Sup vits; (* incomplete *)
542 then case filter_out (test_id (map #1 vits)) vors of
544 (* val miss = filter_out (test_id (map #1 vits)) vors;
546 | miss => SOME (getr_ct thy (hd miss))
548 case find_first (test_subset (hd icl)) vors of
549 (* val SOME ori = find_first (test_subset (hd icl)) vors;
551 NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
552 | SOME ori => SOME (geti_ct thy ori (hd icl))
558 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
559 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
560 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
561 | mk_delete thy str _ =
562 error ("mk_delete: called with field '"^str^"'");
563 fun mk_additem "#Given" ct = Add_Given ct
564 | mk_additem "#Find" ct = Add_Find ct
565 | mk_additem "#Relate"ct = Add_Relation ct
567 error ("mk_additem: called with field '"^str^"'");
570 (* determine the next step of specification;
571 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
572 eg. in rootpbl 'no_met':
574 preok predicates are _all_ ok (and problem matches completely)
575 oris immediately from formalization
576 (dI',pI',mI') specification coming from author/parent-problem
577 (pbl, item lists specified by user
578 met) -"-, tacitly completed by copy_probl
579 (dI,pI,mI) specification explicitly done by the user
580 (pbt, mpc) problem type, guard of method
582 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
583 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
584 ((*tracing"### nxt_spec Pbl";*)
585 if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
586 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
587 else case find_first (is_error o #5) (pbl:itm list) of
588 SOME (_, _, _, fd, itm_) =>
590 (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
592 ((*tracing"### nxt_spec is_error NONE";*)
593 case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
595 SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
596 (Pbl, mk_additem fd ct'))
597 | NONE => (*pbl-items complete*)
598 if not preok then (Pbl, Refine_Problem pI')
600 if dI = e_domID then (Pbl, Specify_Theory dI')
601 else if pI = e_pblID then (Pbl, Specify_Problem pI')
602 else if mI = e_metID then (Pbl, Specify_Method mI')
604 case find_first (is_error o #5) met of
605 SOME (_,_,_,fd,itm_) =>
606 (Met, mk_delete (assoc_thy dI) fd itm_)
608 (case nxt_add (assoc_thy dI) oris mpc met of
609 SOME (fd,ct') => (*30.8.01: pre?!?*)
610 (Met, mk_additem fd ct')
612 ((*Solv 3.4.00*)Met, Apply_Method mI))))
614 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
615 ((*tracing"### nxt_spec Met"; *)
616 case find_first (is_error o #5) met of
617 SOME (_,_,_,fd,itm_) =>
618 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
620 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
621 SOME (fd,ct') => (Met, mk_additem fd ct')
623 ((*tracing"### nxt_spec Met: nxt_add NONE";*)
624 if dI = e_domID then (Met, Specify_Theory dI')
625 else if pI = e_pblID then (Met, Specify_Problem pI')
626 else if not preok then (Met, Specify_Method mI)
627 else (Met, Apply_Method mI)));
630 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
631 (2,[2],true,"#Find",Syn("empty"))];
634 fun is_field_correct sel d dscpbt =
635 case assoc (dscpbt, sel) of
637 | SOME ds => member op = ds d;
639 (*. update the itm_ already input, all..from ori .*)
640 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
642 fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
644 val ts' = union op = (ts_in itm_) ts;
645 val pval = pbl_ids' d ts'
646 (*WN.9.5.03: FIXXXME [#0, epsilon]
647 here would upd_penv be called for [#0, epsilon] etc. *)
648 val complete = if eq_set op = (ts', all) then true else false;
651 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
652 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
653 | (Syn c) => error ("ori_2itm wants to overwrite "^c)
654 | (Typ c) => error ("ori_2itm wants to overwrite "^c)
655 | (Inc _) => if complete
656 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
657 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
658 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
659 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
660 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
661 (* 28.1.00: not completely clear ---^^^ etc.*)
662 (* 4.9.01: Mis just copied---vvv *)
663 | (Mis _) => if complete
664 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
665 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
669 fun eq1 d (_,(d',_)) = (d = d');
670 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
673 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
674 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
675 pval: value for problem-environment _NOT_ checked for 'inter' --
676 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
677 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
678 (*. is_input ori itms <=>
679 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
680 (2) ori(ts) subset itm(ts) --- Err "already input"
681 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
682 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
683 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
685 fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
686 case find_first (eq1 d) pbt of
687 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
688 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
690 (case find_first (eq3 f d) itms of
691 SOME (_,_,_,_,itm_) =>
693 val ts' = inter op = (ts_in itm_) ts;
694 in if subset op = (ts, ts')
696 map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts') ^
697 " already input", e_itm) (*2*)
699 ori_2itm itm_ pid all (i,v,f,d,
700 subtract op = ts' ts)) (*3,4*)
702 | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[])))
703 pid all (i,v,f,d,ts)) (*1*)
705 | NONE => ("", ori_2itm (Sup (d,ts))
706 e_term all (i,v,f,d,ts));
708 fun test_types ctxt (d,ts) =
710 (*val s = !show_types; val _ = show_types:= true;*)
711 val opt = (try comp_dts) (d,ts);
712 val msg = case opt of
714 | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
716 ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
719 (*val _ = show_types:= s*)
724 fun maxl [] = error "maxl of []"
727 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
731 (*. is the input term t known in oris ?
732 give feedback on all(?) strange input;
733 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
734 fun is_known ctxt sel ori t =
736 val _ = tracing ("RM is_known: t=" ^ term2str t);
737 val ots = (distinct o flat o (map #5)) (ori:ori list);
738 val oids = ((map (fst o dest_Free)) o distinct o
739 flat o (map vars)) ots;
740 val (d, ts) = split_dts t;
741 val ids = map (fst o dest_Free)
742 ((distinct o (flat o (map vars))) ts);
743 in if (subtract op = oids ids) <> []
744 then (("identifiers "^(strs2str' (subtract op = oids ids)) ^
745 " not in example"), e_ori_, [])
749 if not (subset op = (map typeless ts, map typeless ots))
750 then (("terms '" ^ ((strs2str' o
751 (map (Print_Mode.setmp [] (Syntax.string_of_term ctxt)))) ts) ^
752 "' not in example (typeless)"), e_ori_, [])
754 (case seek_orits ctxt sel ts ori of
755 ("", ori_ as (_,_,_,d,ts), all) =>
756 (case test_types ctxt (d,ts) of
757 "" => ("", ori_, all)
758 | msg => (msg, e_ori_, []))
759 | (msg,_,_) => (msg, e_ori_, []))
761 if member op = (map #4 ori) d
762 then seek_oridts ctxt sel (d,ts) ori
763 else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
764 " not in example", (0, [], sel, d, ts), [])
768 (*. for return-value of appl_add .*)
771 | Err of string; (*error-message*)
774 (** add an item to the model; check wrt. oris and pbt **)
775 (* in contrary to oris<>[] below, this part handles user-input
776 extremely acceptive, i.e. accept input instead error-msg *)
777 fun appl_add ctxt sel [] ppc pbt ct =
779 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
781 case parseNEW ctxt ct of
782 NONE => Add (i, [], false, sel, Syn ct)
784 let val (d, ts) = split_dts t;
787 then Add (i, [], false, sel, Mis (dsc_unknown, hd ts))
789 (case find_first (eq1 d) pbt of
790 NONE => Add (i, [], true, sel, Sup (d,ts))
791 | SOME (f, (_, id)) =>
792 let fun eq2 d (i, _, _, _, itm_) =
793 d = (d_in itm_) andalso i <> 0;
794 in case find_first (eq2 d) ppc of
795 NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
796 | SOME (i', _, _, _, itm_) =>
800 val in_itm = ts_in itm_;
801 val ts' = union op = ts in_itm;
802 val i'' = if in_itm = [] then i else i';
803 in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts'))) end
804 else Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
808 | appl_add ctxt sel oris ppc pbt str =
809 case parseNEW ctxt str of
810 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
812 case is_known ctxt sel oris t of
814 (case is_notyet_input ctxt ppc all ori' pbt of
816 | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
817 | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
820 (** make oris from args of the stac SubProblem and from pbt **)
821 (* can this formal argument (of a model-pattern) be omitted in the arg-list
822 of a SubProblem ? see ME/ptyps.sml 'type met ' *)
823 fun is_copy_named_idstr str =
824 case (rev o Symbol.explode) str of
825 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
826 "is_copy_named_idstr: " ^ str ^ " T"); true)
827 | _ => (tracing ((strs2str o (rev o Symbol.explode))
828 "is_copy_named_idstr: " ^ str ^ " F"); false);
829 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
831 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
832 fun is_copy_named_generating_idstr str =
833 if is_copy_named_idstr str
834 then case (rev o Symbol.explode) str of
835 "'"::"'"::"'"::_ => false
838 fun is_copy_named_generating (_, (_, t)) =
839 (is_copy_named_generating_idstr o free2str) t;
841 (*.split type-wrapper from scr-arg and build part of an ori;
842 an type-error is reported immediately, raises an exn,
843 subsequent handling of exn provides 2nd part of error message.*)
844 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
845 (* val (thy, (str, (dsc, _)), (ty $ var)) =
848 (cterm_of thy (dsc $ var);(*type check*)
849 SOME ((([1], str, dsc, (*[var]*)
850 split_dts' (dsc, var))): preori)(*:ori without leading #*))
851 handle e as TYPE _ =>
852 (tracing (dashs 70 ^ "\n"
853 ^"*** ERROR while creating the items for the model of the ->problem\n"
854 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
855 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
856 ^"*** description: "^(term_detail2str dsc)
857 ^"*** value: "^(term_detail2str var)
858 ^"*** typeconstructor in script: "^(term_detail2str ty)
859 ^"*** checked by theory: "^(theory2str thy)^"\n"
861 (*OldGoals.print_exn e; raises exn again*)
862 writeln (PolyML.makestring e);
864 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
867 (*.match each pat of the model-pattern with an actual argument;
868 precondition: copy-named vars are filtered out.*)
869 fun matc thy ([]:pat list) _ (oris:preori list) = oris
870 | matc thy pbt [] _ =
872 error ("actual arg(s) missing for '"^pats2str pbt
873 ^"' i.e. should be 'copy-named' by '*_._'"))
874 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
875 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
876 (thy, pbt', ags, []);
878 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
879 (thy, pbt, ags, (oris @ [ori]));
881 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
882 else(*..del?*) let val opt = mtc thy p a;
884 (* val SOME ori = mtc thy p a;
886 SOME ori => matc thy pbt ags (oris @ [ori])
887 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
889 (* run subp-rooteq.sml until Init_Proof before ...
890 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
891 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
893 other vars as in mtc ..
894 > matc thy (drop_last pbt) ags [];
895 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
898 (* generate a new variable "x_i" name from a related given one "x"
899 by use of oris relating "v_i_" (is_copy_named!) to "v_"
900 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
902 (* generate a new variable "x_i" name from a related given one "x"
903 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
904 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
905 but leave is_copy_named_generating as is, e.t. ss''' *)
906 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
907 (if is_copy_named_generating p
908 then (*WN051014 kept strange old code ...*)
909 let fun sel (_,_,d,ts) = comp_ts (d, ts)
910 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
911 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
912 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
913 val vals = map sel oris
914 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
915 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
916 else ([1], field, dsc, [t])
918 handle _ => error ("cpy_nam: for "^(term2str t));
920 (*.match the actual arguments of a SubProblem with a model-pattern
921 and create an ori list (in root-pbl created from formalization).
922 expects ags:pats = 1:1, while copy-named are filtered out of pats;
923 if no 1:1 the exn raised by matc/mtc and handled at call.
924 copy-named pats are appended in order to get them into the model-items.*)
925 fun match_ags thy (pbt:pat list) ags =
926 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
927 val pbt' = filter_out is_copy_named pbt;
928 val cy = filter is_copy_named pbt;
929 val oris' = matc thy pbt' ags [];
930 val cy' = map (cpy_nam pbt' oris') cy;
931 val ors = add_id (oris' @ cy');
932 (*appended in order to get ^^^^^ into the model-items*)
933 in (map flattup ors):ori list end;
935 (*.report part of the error-msg which is not available in match_args.*)
936 fun match_ags_msg pI stac ags =
937 let (*val s = !show_types
938 val _ = show_types:= true*)
939 val pats = (#ppc o get_pbt) pI
940 val msg = (dots 70^"\n"
941 ^"*** problem "^strs2str pI^" has the ...\n"
942 ^"*** model-pattern "^pats2str pats^"\n"
943 ^"*** stac '"^term2str stac^"' has the ...\n"
944 ^"*** arg-list "^terms2str ags^"\n"
946 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
947 (*val _ = show_types:= s*)
951 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
952 fun vars_of_pbl_ pbl_ =
953 let fun var_of_pbl_ (gfr,(dsc,t)) = t
954 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
955 fun vars_of_pbl_' pbl_ =
956 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
957 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
959 fun overwrite_ppc thy itm ppc =
961 fun repl ppc' (_,_,_,_,itm_) [] =
962 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
964 | repl ppc' itm (p::ppc) =
965 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
966 else repl (ppc' @ [p]) itm ppc
967 in repl [] itm ppc end;
969 (*10.3.00: insert the already compiled itm into model;
970 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
973 fun insert_ppc thy itm ppc =
975 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
976 | eq_untouched _ _ = false;
979 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
980 case seek_ppc (#1 itm) ppc of
981 (* val SOME xxx = seek_ppc (#1 itm) ppc;
983 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
984 overwrite_ppc thy itm ppc
985 | NONE => (ppc @ [itm]));
986 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
988 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
989 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
991 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
992 (d_in itm_) = (d_in iitm_);
993 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
994 handles superfluous items carelessly*)
995 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
997 > gen_ins' eee (4,[1,3,5,7]);
998 val it = [1, 3, 5, 7, 4] : int list*)
1001 (*. output the headline to a ppc .*)
1002 fun header p_ pI mI =
1003 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1005 | pos => error ("header called with "^ pos_2str pos);
1008 fun specify_additem sel (ct,_) (p, Met) c pt =
1010 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1011 probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1012 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1013 val cpI = if pI = e_pblID then pI' else pI;
1014 val cmI = if mI = e_metID then mI' else mI;
1015 val {ppc,pre,prls,...} = get_met cmI;
1017 case appl_add ctxt sel oris met ppc ct of
1018 Add itm (*..union old input *) =>
1020 val met' = insert_ppc thy itm met;
1021 val ((p, Met), _, _, pt') =
1022 generate1 thy (case sel of
1023 "#Given" => Add_Given' (ct, met')
1024 | "#Find" => Add_Find' (ct, met')
1025 | "#Relate"=> Add_Relation'(ct, met'))
1026 (Uistate, ctxt) (p, Met) pt
1027 val pre' = check_preconds thy prls pre met'
1028 val pb = foldl and_ (true, map fst pre')
1030 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1031 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1032 in ((p, p_), ((p, p_), Uistate),
1033 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1034 (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
1038 val pre' = check_preconds thy prls pre met
1039 val pb = foldl and_ (true, map fst pre')
1041 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1042 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1043 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1046 | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt =
1048 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1049 probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1050 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1051 val cpI = if pI = e_pblID then pI' else pI;
1052 val cmI = if mI = e_metID then mI' else mI;
1053 val {ppc,where_,prls,...} = get_pbt cpI;
1055 case appl_add ctxt sel oris pbl ppc ct of
1056 Add itm (*..union old input *) =>
1058 val pbl' = insert_ppc thy itm pbl
1059 val ((p, Pbl), _, _, pt') =
1060 generate1 thy (case sel of
1061 "#Given" => Add_Given' (ct, pbl')
1062 | "#Find" => Add_Find' (ct, pbl')
1063 | "#Relate"=> Add_Relation'(ct, pbl'))
1064 (Uistate, ctxt) (p,Pbl) pt
1065 val pre = check_preconds thy prls where_ pbl'
1066 val pb = foldl and_ (true, map fst pre)
1068 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1069 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1070 val ppc = if p_= Pbl then pbl' else met;
1071 in ((p,p_), ((p,p_),Uistate),
1072 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1073 (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt,Safe,pt')
1077 val pre = check_preconds thy prls where_ pbl
1078 val pb = foldl and_ (true, map fst pre)
1080 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1081 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1082 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1085 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1086 let (* either """"""""""""""" all empty or complete *)
1087 val thy = assoc_thy dI';
1089 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
1091 else pI' |> #ppc o get_pbt |> prep_ori fmz thy
1092 val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1093 (oris, (dI',pI',mI'), e_term)
1094 val pt = update_ctxt pt [] ctxt
1095 val {ppc, prls, where_, ...} = get_pbt pI'
1096 val (pbl, pre, pb) = ([], [], false)
1100 (([], Pbl), (([], Pbl), Uistate),
1101 Form' (PpcKF (0, EdUndef, (length []), Nundef,
1102 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1103 Refine_Tacitly pI', Safe, pt)
1105 (([], Pbl), (([], Pbl), Uistate),
1106 Form' (PpcKF (0, EdUndef, (length []), Nundef,
1107 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1108 Model_Problem, Safe, pt)
1111 (*ONLY for STARTING modeling phase*)
1112 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1114 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_), ctxt, ...}) = get_obj I pt p
1115 val thy' = if dI = e_domID then dI' else dI
1116 val thy = assoc_thy thy'
1117 val {ppc,prls,where_,...} = get_pbt pI'
1118 val pre = check_preconds thy prls where_ pbl
1119 val pb = foldl and_ (true, map fst pre)
1120 val ((p,_),_,_,pt) =
1121 generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1122 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1123 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1124 in ((p, Pbl), ((p, p_), Uistate),
1125 Form' (PpcKF (0, EdUndef, length p, Nundef,
1126 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1130 (*. called only if no_met is specified .*)
1131 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1133 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ctxt, ...}) = get_obj I pt p;
1134 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1135 val (domID, metID) =
1136 (string_of_thy thy, if length met = 0 then e_metID else hd met)
1137 val ((p,_),_,_,pt) =
1138 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1139 (Uistate, ctxt) pos pt
1140 val (pbl, pre, pb) = ([], [], false)
1141 in ((p, Pbl), (pos, Uistate),
1142 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1143 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1144 Model_Problem, Safe, pt)
1147 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1149 val ctxt = get_ctxt pt pos
1151 generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1152 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1153 Model_Problem, Safe, pt)
1155 (*WN110515 initialise ctxt again from itms and add preconds*)
1156 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1158 val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1159 meth=met, ctxt, ...}) = get_obj I pt p;
1160 val thy = assoc_thy dI
1161 val ((p,Pbl),_,_,pt)=
1162 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt
1163 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1164 val mI'' = if mI=e_metID then mI' else mI;
1166 nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1167 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1168 in ((p,Pbl), (pos,Uistate),
1169 Form' (PpcKF (0,EdUndef,(length p),Nundef, (Problem pI, itms2itemppc dI'' itms pre))),
1172 (*WN110515 initialise ctxt again from itms and add preconds*)
1173 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1175 val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1176 meth=met, ctxt, ...}) = get_obj I pt p;
1177 val {ppc,pre,prls,...} = get_met mID
1178 val thy = assoc_thy dI
1179 val oris = add_field' thy ppc oris;
1180 val dI'' = if dI=e_domID then dI' else dI;
1181 val pI'' = if pI = e_pblID then pI' else pI;
1182 val met = if met=[] then pbl else met;
1183 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1184 val (pos, _, _, pt) =
1185 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1187 nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1188 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1189 in (pos, (pos,Uistate),
1190 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1191 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1195 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1196 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1197 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1199 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1201 val p_ = case p_ of Met => Met | _ => Pbl
1202 val thy = assoc_thy domID;
1203 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1204 probl=pbl, spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1205 val mppc = case p_ of Met => met | _ => pbl;
1206 val cpI = if pI = e_pblID then pI' else pI;
1207 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1208 val cmI = if mI = e_metID then mI' else mI;
1209 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1212 Met => (check_preconds thy mer mwh met)
1213 | _ => (check_preconds thy per pwh pbl)
1214 val pb = foldl and_ (true, map fst pre)
1218 let val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1219 (pbl,met) (ppc,mpc) (dI,pI,mI);
1220 in ((p,p_), (pos,Uistate),
1221 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1222 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1225 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1227 val ((p,p_),_,_,pt) =
1228 generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1230 nxt_spec p_ pb oris (dI',pI',mI') (pbl,met) (ppc,mpc) (domID,pI,mI);
1231 in ((p,p_), (pos,Uistate),
1232 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1233 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1238 | specify m' _ _ _ =
1239 error ("specify: not impl. for " ^ tac_2str m');
1241 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
1242 -- for input from scratch*)
1243 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1245 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1246 probl=pbl,spec=(dI,pI,_), ctxt, ...}) = get_obj I pt p;
1247 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1248 val cpI = if pI = e_pblID then pI' else pI;
1250 case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
1251 Add itm (*..union old input *) =>
1253 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1254 val pbl' = insert_ppc thy itm pbl
1257 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1258 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1259 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1260 val ((p,Pbl),c,_,pt') =
1261 generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt
1262 in ([(tac,tac_,((p,Pbl),(Uistate, ctxt)))], c, (pt',(p,Pbl))):calcstate'
1264 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1265 FIXME ..and dont abuse a tactic for that purpose*)
1266 ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1267 (e_pos', (e_istate, e_ctxt)))], [], ptp)
1270 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1272 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1273 probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1274 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1275 val cmI = if mI = e_metID then mI' else mI;
1277 case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
1278 Add itm (*..union old input *) =>
1280 val met' = insert_ppc thy itm met;
1283 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1284 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1285 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1286 val ((p,Met),c,_,pt') =
1287 generate1 thy tac_ (Uistate, ctxt) (p,Met) pt
1288 in ([(tac,tac_,((p,Met), (Uistate, ctxt)))], c, (pt',(p,Met))) end
1289 | Err msg => ([(*tacis*)], [], ptp)
1290 (*nxt_me collects tacis until not hide; here just no progress*)
1293 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1294 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1295 handle _ => error ("ori2Coritm: dsc "^
1297 "in ori, but not in pbt")
1299 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1300 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1301 (find_first (eq1 d))) pbt,ts))):itm)
1302 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1303 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1306 (*filter out oris which have same description in itms*)
1307 fun filter_outs oris [] = oris
1308 | filter_outs oris (i::itms) =
1309 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1310 (#4:ori -> term)) oris;
1311 in filter_outs ors itms end;
1313 fun memI a b = member op = a b;
1314 (*filter oris which are in pbt, too*)
1315 fun filter_pbt oris pbt =
1316 let val dscs = map (fst o snd) pbt
1317 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1319 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1320 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1322 fun x mem [] = false
1323 | x mem (y :: ys) = x = y orelse x mem ys;
1325 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1326 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1328 let val vat = max_vt pits;
1330 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1331 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1332 val os = filter_outs ors itms;
1333 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1334 in itms @ (map (ori2Coritm met) os) end
1339 (*.complete model and guard of a calc-head .*)
1341 fun x mem [] = false
1342 | x mem (y :: ys) = x = y orelse x mem ys;
1344 fun complete_mod_ (oris, mpc, ppc, probl) =
1345 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1346 val vat = if probl = [] then 1 else max_vt probl
1347 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1348 val pors = filter_outs pors pits (*which are in pbl already*)
1349 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1351 val pits = pits @ (map (ori2Coritm ppc) pors)
1352 val mits = complete_metitms oris pits [] mpc
1356 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1357 (if dI = e_domID then odI else dI,
1358 if pI = e_pblID then opI else pI,
1359 if mI = e_metID then omI else mI):spec;
1362 (*.find a next applicable tac (for calcstate) and update ptree
1363 (for ev. finding several more tacs due to hide).*)
1364 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1365 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1366 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1367 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1369 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p
1370 val (dI, pI, mI) = some_spec ospec spec
1371 val thy = assoc_thy dI
1372 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1373 val {cas, ppc, ...} = get_pbt pI
1374 val pbl = init_pbl ppc (* fill in descriptions *)
1375 (*----------------if you think, this should be done by the Dialog
1376 in the java front-end, search there for WN060225-modelProblem----*)
1378 case cas of NONE => (pbl, [])
1379 | _ => complete_mod_ (oris, mpc, ppc, probl)
1380 (*----------------------------------------------------------------*)
1381 val tac_ = Model_Problem' (pI, pbl, met)
1382 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, ctxt) pos pt
1383 in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1385 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1386 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1387 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1389 (*. called only if no_met is specified .*)
1390 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1392 val (PblObj {origin = (oris, (dI,_,_),_), ctxt, ...}) = get_obj I pt p
1393 val opt = refine_ori oris pI
1398 val {met,ppc,...} = get_pbt pI'
1399 val pbl = init_pbl ppc
1400 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1401 val mI = if length met = 0 then e_metID else hd met
1402 val thy = assoc_thy dI
1404 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1405 (Uistate, ctxt) pos pt
1406 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1407 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1409 | NONE => ([], [], ptp)
1412 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1414 val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), probl, ctxt, ...}) = get_obj I pt p
1415 val thy = if dI' = e_domID then dI else dI'
1417 case refine_pbl (assoc_thy thy) pI probl of
1418 NONE => ([], [], ptp)
1419 | SOME (rfd as (pI',_)) =>
1421 val (pos,c,_,pt) = generate1 (assoc_thy thy)
1422 (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1423 in ([(Refine_Problem pI, Refine_Problem' rfd,
1424 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1428 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1430 val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...}) = get_obj I pt p;
1431 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1432 val {ppc,where_,prls,...} = get_pbt pI
1433 val pbl as (_,(itms,_)) =
1434 if pI'=e_pblID andalso pI=e_pblID
1435 then (false, (init_pbl ppc, []))
1436 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1437 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1438 val ((p,Pbl),c,_,pt) =
1439 generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt
1440 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1441 (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1444 (*transfers oris (not required in pbl) to met-model for script-env
1445 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1446 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1448 val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1449 meth=met, ctxt, ...}) = get_obj I pt p;
1450 val {ppc,pre,prls,...} = get_met mID
1451 val thy = assoc_thy dI
1452 val oris = add_field' thy ppc oris;
1453 val dI'' = if dI=e_domID then dI' else dI;
1454 val pI'' = if pI = e_pblID then pI' else pI;
1455 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1456 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1458 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1459 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1460 (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1463 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1465 val ctxt = get_ctxt pt pos
1466 val (dI',_,_) = get_obj g_spec pt p
1468 generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1469 in (*FIXXXME: check if pbl can still be parsed*)
1470 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
1474 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1476 val ctxt = get_ctxt pt pos
1477 val (dI',_,_) = get_obj g_spec pt p
1479 generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1480 in (*FIXXXME: check if met can still be parsed*)
1481 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
1486 error ("nxt_specif: not impl. for "^tac2str m');
1488 (* get the values from oris; handle the term list w.r.t. penv *)
1490 fun x mem [] = false
1491 | x mem (y :: ys) = x = y orelse x mem ys;
1493 fun vals_of_oris oris =
1494 ((map (mkval' o (#5:ori -> term list))) o
1495 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1498 (* create a calc-tree with oris via an cas.refined pbl *)
1499 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1501 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1503 val {cas, met, ppc, thy, ...} = get_pbt pI
1504 val dI = if dI = "" then theory2theory' thy else dI
1505 val thy = assoc_thy dI
1506 val mI = if mI = [] then hd met else mI
1507 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1508 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1509 ([], (dI,pI,mI), hdl)
1510 val pt = update_spec pt [] (dI,pI,mI)
1511 val pits = init_pbl' ppc
1512 val pt = update_pbl pt [] pits
1513 in ((pt, ([] ,Pbl)), []) : calcstate end
1516 then (* from met-browser *)
1518 val {ppc,...} = get_met mI
1519 val dI = if dI = "" then "Isac" else dI
1520 val thy = assoc_thy dI;
1521 val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1522 ([], (dI,pI,mI), e_term(*FIXME met*));
1523 val pt = update_spec pt [] (dI,pI,mI);
1524 val mits = init_pbl' ppc;
1525 val pt = update_met pt [] mits;
1526 in ((pt, ([], Met)), []) : calcstate end
1527 else (* new example, pepare for interactive modeling *)
1528 let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1529 ([], e_spec, e_term)
1530 in ((pt, ([], Pbl)), []) : calcstate end
1532 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1533 let (* both """"""""""""""""""""""""" either empty or complete *)
1534 val thy = assoc_thy dI
1535 val (pI, (pors, pctxt), mI) =
1539 val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
1540 val pI' = refine_ori' pors pI;
1541 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1542 (hd o #met o get_pbt) pI') end
1543 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
1544 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1545 val dI = theory2theory' (maxthy thy thy')
1548 NONE => pblterm dI pI
1549 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
1550 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
1551 (pors, (dI, pI, mI), hdl)
1552 val pt = update_ctxt pt [] pctxt
1553 in ((pt, ([], Pbl)),
1554 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1560 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1561 (* case appl_spec p pt m of /// 19.1.00
1562 Notappl e => Error' (Error_ e)
1564 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1568 (*fun tag_form thy (formal, given) = cterm_of thy
1569 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1570 fun tag_form thy (formal, given) =
1571 (let val gf = (head_of given) $ formal;
1572 val _ = cterm_of thy gf
1575 error ("calchead.tag_form: " ^
1576 Print_Mode.setmp [] (Syntax.string_of_term
1577 (thy2ctxt thy)) given ^ " .. " ^
1578 Print_Mode.setmp [] (Syntax.string_of_term
1579 (thy2ctxt thy)) formal ^
1580 " ..types do not match");
1581 (* val formal = (the o (parse thy)) "[R::real]";
1582 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1583 > tag_form thy (formal, given);
1584 val it = "fixed_values [R]" : cterm
1587 fun chktyp thy (n, fs, gs) =
1588 ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1590 (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1592 tag_form thy (nth n fs, nth n gs));
1593 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1595 (* #####################################################
1596 find the failing item:
1598 > val tag__form = chktyp (n,formals,givens);
1599 > (type_of o term_of o (nth n)) formals;
1600 > (type_of o term_of o (nth n)) givens;
1601 > atomty ((term_of o (nth n)) formals);
1602 > atomty ((term_of o (nth n)) givens);
1603 > atomty (term_of tag__form);
1604 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1605 ##################################################### *)
1607 (* #####################################################
1609 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1610 val formals = map (the o (parse thy)) origin;
1612 val given = ["equation (lhs=rhs)",
1613 "bound_variable bdv", (* TODO type *)
1615 val where_ = ["e is_root_equation_in bdv",
1617 "apx is_const_expr"];
1618 val find = ["L::rat set"];
1619 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1620 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1621 val givens = map (the o (parse thy)) given;
1623 val tag__forms = chktyps (formals, givens);
1624 map ((atomty) o term_of) tag__forms;
1625 ##################################################### *)
1628 (* check pbltypes, announces one failure a time *)
1629 (*fun chk_vars ctppc =
1630 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1631 appc flat (mappc (vars o term_of) ctppc)
1632 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1633 else if (re\\(gi union fi)) <> []
1634 then ("re\\(gi union fi)",re\\(gi union fi))
1635 else ("ok",[]) end;*)
1636 fun chk_vars ctppc =
1637 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1638 appc flat (mappc vars ctppc)
1639 val chked = subtract op = gi wh
1640 in if chked <> [] then ("wh\\gi", chked)
1641 else let val chked = subtract op = (union op = gi fi) re
1643 then ("re\\(gi union fi)", chked)
1648 (* check a new pbltype: variables (Free) unbound by given, find*)
1649 fun unbound_ppc ctppc =
1650 let val {Given=gi,Find=fi,Relate=re,...} =
1651 appc flat (mappc vars ctppc)
1652 in distinct (*re\\(gi union fi)*)
1653 (subtract op = (union op = gi fi) re) end;
1655 > val org = {Given=["[R=(R::real)]"],Where=[],
1656 Find=["[A::real]"],With=[],
1657 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1659 > val ctppc = mappc (the o (parse thy)) org;
1660 > unbound_ppc ctppc;
1661 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1665 (* f, a binary operator, is nested rightassociative *)
1668 fun fld f (x::[]) = x
1669 | fld f (x::x'::[]) = f (x',x)
1670 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1671 in ((fld f) o rev) xs end;
1673 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1674 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1675 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1676 > cterm_of thy conj;
1677 val it = "(a = b & c = d) & e = f" : cterm
1680 (* f, a binary operator, is nested leftassociative *)
1681 fun foldl1 f (x::[]) = x
1682 | foldl1 f (x::x'::[]) = f (x,x')
1683 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1685 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1686 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1687 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1688 > cterm_of thy conj;
1689 val it = "a = b & c = d & e = f & g = h" : cterm
1693 (* called only once, if a Subproblem has been located in the script*)
1694 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_,_)) ptp =
1697 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1698 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1699 (*all stored in tac_ itms^^^^^^^^^^*)
1700 | nxt_model_pbl tac_ _ =
1701 error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_);
1703 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1704 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1705 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1708 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1709 + met from fmz; assumes pos on PblObj, meth = [].*)
1710 fun complete_mod (pt, pos as (p, p_):pos') =
1711 (* val (pt, (p, _)) = (pt, p);
1712 val (pt, (p, _)) = (pt, pos);
1714 let val _= if p_ <> Pbl
1715 then tracing("###complete_mod: only impl.for Pbl, called with "^
1716 pos'2str pos) else ()
1717 val (PblObj{origin=(oris, ospec, hdl), probl, spec, ...}) =
1719 val (dI,pI,mI) = some_spec ospec spec
1720 val mpc = (#ppc o get_met) mI
1721 val ppc = (#ppc o get_pbt) pI
1722 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1723 val pt = update_pblppc pt p pits
1724 val pt = update_metppc pt p mits
1725 in (pt, (p,Met):pos') end
1727 (*| complete_mod (pt, pos as (p, Met):pos') =
1728 error ("###complete_mod: only impl.for Pbl, called with "^
1731 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1732 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1733 fun all_modspec (pt, (p,_):pos') =
1735 val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
1736 val thy = assoc_thy dI;
1737 val {ppc, ...} = get_met mI;
1738 val (fmz_, vals) = oris2fmz_vals pors;
1739 val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global
1740 |> declare_constraints' vals
1741 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1742 val pt = update_metppc pt p (map (ori2Coritm ppc) pors); (*WN110716 = _pblppc ?!?*)
1743 val pt = update_spec pt p (dI,pI,mI);
1744 val pt = update_ctxt pt p ctxt
1746 val mors = prep_ori fmz_ thy ppc |> #1;
1747 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1748 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1749 (*WN110715: why pors, mors handled so differently?*)
1750 val pt = update_spec pt p (dI,pI,mI);
1752 in (pt, (p,Met): pos') end;
1754 (*WN0312: use in nxt_spec, too ? what about variants ???*)
1755 fun is_complete_mod_ ([]: itm list) = false
1756 | is_complete_mod_ itms =
1757 foldl and_ (true, (map #3 itms));
1759 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1760 if (is_pblobj o (get_obj I pt)) p
1761 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1762 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1763 | is_complete_mod (pt, pos as (p, Met)) =
1764 if (is_pblobj o (get_obj I pt)) p
1765 then (is_complete_mod_ o (get_obj g_met pt)) p
1766 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1767 | is_complete_mod (_, pos) =
1768 error ("is_complete_mod called by " ^ pos'2str pos ^
1769 " (should be Pbl or Met)");
1771 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1772 fun is_complete_spec (pt, pos as (p,_): pos') =
1773 if (not o is_pblobj o (get_obj I pt)) p
1774 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1775 else let val (dI,pI,mI) = get_obj g_spec pt p
1776 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1777 (*.complete empty items in specification from origin (pbl, met ev.refined);
1778 assumes 'is_complete_mod'.*)
1779 fun complete_spec (pt, pos as (p,_): pos') =
1780 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1781 val pt = update_spec pt p (some_spec ospec spec)
1784 fun is_complete_modspec ptp =
1785 is_complete_mod ptp andalso is_complete_spec ptp;
1790 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1791 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1793 let val (_,_,metID) = get_somespec' spec spec'
1795 if metID = e_metID then []
1796 else let val {prls,pre=where_,...} = get_met metID
1797 val pre = check_preconds' prls where_ meth 0
1799 val allcorrect = is_complete_mod_ meth
1800 andalso foldl and_ (true, (map #1 pre))
1801 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1802 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1803 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1805 let val (_,pI,_) = get_somespec' spec spec'
1807 if pI = e_pblID then []
1808 else let val {prls,where_,cas,...} = get_pbt pI
1809 val pre = check_preconds' prls where_ probl 0
1811 val allcorrect = is_complete_mod_ probl
1812 andalso foldl and_ (true, (map #1 pre))
1813 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1816 fun pt_form (PrfObj {form,...}) = Form form
1817 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1818 let val (dI, pI, _) = get_somespec' spec spec'
1819 val {cas,...} = get_pbt pI
1821 NONE => Form (pblterm dI pI)
1822 | SOME t => Form (subst_atomic (mk_env probl) t)
1824 (*vvv takes the tac _generating_ the formula=result, asm ok....
1825 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1827 if null asm then NONE else SOME asm,
1829 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1830 let val (_,_,metID) = some_spec ospec spec
1832 if null asm then NONE else SOME asm,
1833 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1834 -------------------------------------------------------------------------*)
1837 (*.pt_extract returns
1838 # the formula at pos
1839 # the tactic applied to this formula
1840 # the list of assumptions generated at this formula
1841 (by application of another tac to the preceding formula !)
1842 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1843 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1844 fun pt_extract (pt,([],Res)) =
1845 (* val (pt,([],Res)) = ptp;
1847 (* ML_TODO 110417 get assumptions from ctxt !? *)
1848 let val (f, asm) = get_obj g_result pt []
1849 in (Form f, NONE, asm) end
1852 | pt_extract (pt,(p,Res)) =
1853 (* val (pt,(p,Res)) = ptp;
1855 let val (f, asm) = get_obj g_result pt p
1856 val tac = if last_onlev pt p
1857 then if is_pblobj' pt (lev_up p)
1858 then let val (PblObj{spec=(_,pI,_),...}) =
1859 get_obj I pt (lev_up p)
1860 in if pI = e_pblID then NONE
1861 else SOME (Check_Postcond pI) end
1862 else SOME End_Trans (*WN0502 TODO for other branches*)
1863 else let val p' = lev_on p
1864 in if is_pblobj' pt p'
1865 then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1867 in SOME (Subproblem (dI, pI)) end
1868 else if f = get_obj g_form pt p'
1869 then SOME (get_obj g_tac pt p')
1870 (*because this Frm ~~~is not on worksheet*)
1871 else SOME (Take (term2str (get_obj g_form pt p')))
1873 in (Form f, tac, asm) end
1875 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1876 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1877 val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
1879 let val ppobj = get_obj I pt p
1880 val f = if is_pblobj ppobj then pt_model ppobj p_
1881 else get_obj pt_form pt p
1882 val tac = g_tac ppobj
1883 in (f, SOME tac, []) end;
1886 (**. get the formula from a ctree-node:
1887 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1888 take res from all other PrfObj's .**)
1889 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1890 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1891 [("headline", (p, Frm), h),
1892 ("stepform", (p, Res), r)]
1893 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1894 [("stepform", (p, Frm), form),
1895 ("stepform", (p, Res), r)];
1897 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1898 [("stepform", (p, Res), r)]
1900 (*assumes to take whole level, in particular hd -- for use in interSteps*)
1901 fun get_formress fs p [] = flat fs
1902 | get_formress fs p (nd::nds) =
1903 (* start with 'form+res' and continue with trying 'res' only*)
1904 get_forms (fs @ [formres p nd]) (lev_on p) nds
1905 and get_forms fs p [] = flat fs
1906 | get_forms fs p (nd::nds) =
1908 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1909 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1910 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1911 (* continue with trying 'res' only*)
1912 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1914 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1915 (*WN050219 made robust against _'to' below or after Complete nodes
1916 by handling exn caused by move_dn*)
1917 (*WN0401 this functionality belongs to ctree.sml,
1918 but fetching a calc_head requires calculations defined in modspec.sml
1919 transfer to ME/me.sml !!!
1920 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1921 is returned !!!!!!!!!!!!!
1923 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1924 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1925 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1929 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1933 | eq_pos' _ _ = false;
1935 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
1936 total ordering Position#compareTo(Position p) in the java-code
1937 val get_interval = fn
1938 : pos' -> : from is "move_up 1st-element" to return
1939 pos' -> : to the last element to be returned; from < to
1940 int -> : level: 0 gets the flattest sub-tree possible
1941 >999 gets the deepest sub-tree possible
1943 (pos' * : of the formula
1944 Term.term) : the formula
1947 fun get_interval from to level pt =
1949 fun get_inter c (from:pos') (to:pos') lev pt =
1950 if eq_pos' from to orelse from = ([],Res)
1951 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
1952 if 'to' has values NOT generated by move_dn, see systest/me.sml
1953 TODO.WN0501: introduce an order on pos' and check "from > to"..
1954 ...there is an order in Java!
1955 WN051224 the hack got worse with returning term instead ptform*)
1957 let val (f,_,_) = pt_extract (pt, from)
1960 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
1961 | Form t => c @ [(from, t)]
1964 if lev < lev_of from
1965 then (get_inter c (move_dn [] pt from) to lev pt)
1966 handle (PTREE _(*from move_dn too far*)) => c
1969 val (f,_,_) = pt_extract (pt, from)
1970 val term = case f of
1971 ModSpec (_,_,headline,_,_,_) => headline
1973 in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)
1974 handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]
1976 in get_inter [] from to level pt end;
1979 fun posform2str (pos:pos', form) =
1980 "("^ pos'2str pos ^", "^
1982 Form f => term2str f
1983 | ModSpec c => term2str (#3 c(*the headline*)))
1985 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
1986 (map posform2str)) pfs;
1987 fun posterm2str (pos:pos', t) =
1988 "("^ pos'2str pos ^", "^term2str t^")";
1989 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
1990 (map posterm2str)) pfs;
1993 (*WN050225 omits the last step, if pt is incomplete*)
1995 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
1997 (*.get a calchead from a PblObj-node in the ctree;
1998 preconditions must be calculated.*)
1999 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
2000 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
2002 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2003 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
2004 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
2005 | get_ocalhd (pt, pos' as (p,Met):pos') =
2006 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2009 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2010 val pre = check_preconds (assoc_thy"Isac") prls pre meth
2011 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
2013 (*.at the activeFormula set the Model, the Guard and the Specification
2014 to empty and return a CalcHead;
2015 the 'origin' remains (for reconstructing all that).*)
2016 fun reset_calchead (pt, pos' as (p,_):pos') =
2017 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
2018 val pt = update_pbl pt p []
2019 val pt = update_met pt p []
2020 val pt = update_spec pt p e_spec
2021 in (pt, (p,Pbl):pos') end;