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
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 maxl : int list -> int
115 val match_ags_msg : string list -> Term.term -> Term.term list -> unit
116 val memI : ''a list -> ''a -> bool
117 val mk_additem : string -> cterm' -> tac
118 val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
120 theory -> pat -> Term.term -> SpecifyTools.preori option
123 SpecifyTools.ori list ->
124 (string * (Term.term * 'a)) list ->
125 SpecifyTools.itm list -> (string * cterm') option
126 val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
130 SpecifyTools.ori list ->
132 SpecifyTools.itm list * SpecifyTools.itm list ->
133 (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->
135 val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'
136 val nxt_specif_additem :
137 string -> cterm' -> ptree * (int list * pos_) -> calcstate'
138 val nxt_specify_init_calc : fmz -> calcstate
139 val ocalhd_complete :
140 SpecifyTools.itm list ->
141 (bool * Term.term) list -> domID * pblID * metID -> bool
143 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 : theory -> 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 (*---------------------------------------------------------------------*)
210 structure CalcHead (**): CALC_HEAD(**) =
213 (*---------------------------------------------------------------------*)
217 (*.the state wich is stored after each step of calculation; it contains
218 the calc-state and a list of [tac,istate](="tacis") to be applied next.
219 the last_elem tacis is the first to apply to the calc-state and
220 the (only) one shown to the front-end as the 'proposed tac'.
221 the calc-state resulting from the application of tacis is not stored,
222 because the tacis hold enough information for efficiently rebuilding
223 this state just by "fun generate ".*)
225 (ptree * pos') * (*the calc-state to which the tacis could be applied*)
226 (taci list); (*ev. several (hidden) steps;
227 in REVERSE order: first tac_ to apply is last_elem*)
228 val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
230 (*the state used during one calculation within the mathengine; it contains
231 a list of [tac,istate](="tacis") which generated the the calc-state;
232 while this state's tacis are extended by each (internal) step,
233 the calc-state is used for creating new nodes in the calc-tree
234 (eg. applicable_in requires several particular nodes of the calc-tree)
235 and then replaced by the the newly created;
236 on leave of the mathengine the resuing calc-state is dropped anyway,
237 because the tacis hold enought information for efficiently rebuilding
238 this state just by "fun generate ".*)
240 taci list * (*cas. several (hidden) steps;
241 in REVERSE order: first tac_ to apply is last_elem*)
242 pos' list * (*a "continuous" sequence of pos',
243 deleted by application of taci list*)
244 (ptree * pos'); (*the calc-state resulting from the application of tacis*)
245 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
247 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
248 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
249 | f_mout thy _ = error "f_mout: not called with formula";
252 (*.is the calchead complete ?.*)
253 fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
254 foldl and_ (true, map #3 its) andalso
255 foldl and_ (true, map #1 pre) andalso
256 dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
259 (* make a term 'typeless' for comparing with another 'typeless' term;
260 'type-less' usually is illtyped *)
261 fun typeless (Const(s,_)) = (Const(s,e_type))
262 | typeless (Free(s,_)) = (Free(s,e_type))
263 | typeless (Var(n,_)) = (Var(n,e_type))
264 | typeless (Bound i) = (Bound i)
265 | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
266 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
268 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
269 > val (_,t1) = split_dsc_t hs (term_of ct);
270 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
271 > val (_,t2) = split_dsc_t hs (term_of ct);
272 > typeless t1 = typeless t2;
278 (*.to an input (d,ts) find the according ori and insert the ts.*)
279 (*WN.11.03: + dont take first inter<>[]*)
280 fun seek_oridts thy sel (d,ts) [] =
281 ("'" ^ (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
282 (comp_dts thy (d,ts))) ^
283 "' not found (typed)", (0, [], sel, d, ts) : ori,
285 | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
286 if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
289 (id,vat,sel,d, inter op = ts ts'):ori,
291 else ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
292 (comp_dts thy (d,ts))) ^ " not for " ^ sel,
295 else seek_oridts thy sel (d,ts) oris;
297 (*.to an input (_,ts) find the according ori and insert the ts.*)
298 fun seek_orits thy sel ts [] =
299 ("'" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
300 (thy2ctxt thy))) ts) ^
301 "' not found (typed)", e_ori_, [])
302 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
303 if sel = sel' andalso (inter op = ts ts') <> []
306 (id,vat,sel,d, inter op = ts ts'):ori,
308 else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
309 (thy2ctxt thy)))) ts)
313 else seek_orits thy sel ts oris;
315 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
316 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
317 uncaught exception TYPE
318 > seek_orits thy sel ts [];
319 uncaught exception TYPE
322 (*find_first item with #1 equal to id*)
323 fun seek_ppc id [] = NONE
324 | seek_ppc id (p::(ppc:itm list)) =
325 if id = #1 p then SOME p else seek_ppc id ppc;
329 (*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
332 datatype appl = Appl of tac_ | Notappl of string;
334 fun ppc2list ({Given=gis,Where=whs,Find=fis,
335 With=wis,Relate=res}: 'a ppc) =
336 gis @ whs @ fis @ wis @ res;
337 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
343 (* get the number of variants in a problem in 'original',
344 assumes equal descriptions in immediate sequence *)
346 let fun eq(x,y) = head_of x = head_of y;
347 fun cnt eq [] y n = ([n],[])
348 | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
350 fun coll eq xs [] = xs
351 | coll eq xs (y::ys) =
352 let val (n,ys') = cnt eq (y::ys) y 0;
353 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
354 val vts = subtract op = [1] (distinct (coll eq [] ts));
355 in case vts of [] => 1 | [n] => n
356 | _ => error "different variants in formalization" end;
358 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
359 val it = ([3],[4,5,5,5,5,5]) : int list * int list
360 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
361 val it = [1,3,1,5] : int list
364 fun is_list_type (Type("List.list",_)) = true
365 | is_list_type _ = false;
366 (* fun destr (Type(str,sort)) = (str,sort);
367 > val (SOME ct) = parse thy "lll::real list";
368 > val ty = (#T o rep_cterm) ct;
372 val it = ("List.list",["RealDef.real"]) : string * typ list
373 > atomty ((#t o rep_cterm) ct);
375 *** Free ( lll, real list)
378 > val (SOME ct) = parse thy "[lll::real]";
379 > val ty = (#T o rep_cterm) ct;
383 val it = ("List.list",["'a"]) : string * typ list
384 > atomty ((#t o rep_cterm) ct);
386 *** Const ( List.list.Cons, [real, real list] => real list)
387 *** Free ( lll, real)
388 *** Const ( List.list.Nil, real list)
390 > val (SOME ct) = parse thy "lll";
391 > val ty = (#T o rep_cterm) ct;
393 val it = false : bool *)
396 fun has_list_type (Free(_,T)) = is_list_type T
397 | has_list_type _ = false;
399 > val (SOME ct) = parse thy "lll::real list";
400 > has_list_type (term_of ct);
402 > val (SOME ct) = parse thy "[lll::real]";
403 > has_list_type (term_of ct);
404 val it = false : bool *)
406 fun is_parsed (Syn _) = false
407 | is_parsed _ = true;
408 fun parse_ok its = foldl and_ (true, map is_parsed its);
410 fun all_dsc_in itm_s =
412 fun d_in (Cor ((d,_),_)) = [d]
415 | d_in (Inc ((d,_),_)) = [d]
416 | d_in (Sup (d,_)) = [d]
417 | d_in (Mis (d,_)) = [d];
418 in (flat o (map d_in)) itm_s end;
421 fun is_Syn (Syn _) = true
422 | is_Syn (Typ _) = true
425 fun is_error (Cor (_,ts)) = false
426 | is_error (Sup (_,ts)) = false
427 | is_error (Inc (_,ts)) = false
428 | is_error (Mis (_,ts)) = false
432 fun ct_in (Syn (c)) = c
433 | ct_in (Typ (c)) = c
434 | ct_in _ = error "ct_in called for Cor .. Sup";
437 (*#############################################################*)
438 (*#############################################################*)
439 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
442 (* testdaten besorgen:
443 use"test-coil-kernel.sml";
444 val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
449 variant V: oris union ppc => int, id ID: oris union ppc => int
452 EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
455 @vt = max sum(i : ppc) V i
461 > ((vts_cnt (vts_in itms))) itms;
466 > val vts = vts_in itms;
467 val vts = [1,2,3] : int list
468 > val nvts = vts_cnt vts itms;
469 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
470 > val mx = max2 nvts;
471 val mx = (3,7) : int * int
472 > val v = max_vt itms;
474 --------------------------
478 (*.get the first term in ts from ori.*)
479 (* val (_,_,fd,d,ts) = hd miss;
481 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
482 (fd, (Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy))) o
483 (comp_dts thy)) (d,[hd ts]) : cterm');
484 (* val t = comp_dts thy (d,[hd ts]);
487 (* get a term from ori, notyet input in itm.
488 the term from ori is thrown back to a string in order to reuse
489 machinery for immediate input by the user. *)
490 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
491 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
493 (d, subtract op = (ts_in itm_) ts) : cterm');
494 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
495 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
497 (d, subtract op = (ts_in itm_) ts) : cterm');
499 (* in FE dsc, not dat: this is in itms ...*)
500 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
501 | is_untouched _ = false;
504 (* select an item in oris, notyet input in itms
505 (precondition: in itms are only Cor, Sup, Inc) *)
508 | x mem (y :: ys) = x = y orelse x mem ys;
510 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
512 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
513 fun is_elem itms (f,(d,t)) =
514 case find_first (test_d d) itms of
515 SOME _ => true | NONE => false;
516 in case filter_out (is_elem itms) pbt of
517 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
521 ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
522 comp_dts thy) (d, []) : cterm')
525 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
527 | nxt_add thy oris pbt itms =
529 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
530 andalso (#3 ori) <>"#undef";
531 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
532 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
533 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
534 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
535 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
536 | false_and_not_Sup (i,v,false,f, _) = true
537 | false_and_not_Sup _ = false;
539 val v = if itms = [] then 1 else max_vt itms;
540 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
541 val vits = if v = 0 then itms (*because of dsc without dat*)
542 else filter (testi_vt v) itms; (*itms..vat*)
543 val icl = filter false_and_not_Sup vits; (* incomplete *)
545 then case filter_out (test_id (map #1 vits)) vors of
547 (* val miss = filter_out (test_id (map #1 vits)) vors;
549 | miss => SOME (getr_ct thy (hd miss))
551 case find_first (test_subset (hd icl)) vors of
552 (* val SOME ori = find_first (test_subset (hd icl)) vors;
554 NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
555 | SOME ori => SOME (geti_ct thy ori (hd icl))
561 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
562 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
563 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
564 | mk_delete thy str _ =
565 error ("mk_delete: called with field '"^str^"'");
566 fun mk_additem "#Given" ct = Add_Given ct
567 | mk_additem "#Find" ct = Add_Find ct
568 | mk_additem "#Relate"ct = Add_Relation ct
570 error ("mk_additem: called with field '"^str^"'");
573 (* determine the next step of specification;
574 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
575 eg. in rootpbl 'no_met':
577 preok predicates are _all_ ok (and problem matches completely)
578 oris immediately from formalization
579 (dI',pI',mI') specification coming from author/parent-problem
580 (pbl, item lists specified by user
581 met) -"-, tacitly completed by copy_probl
582 (dI,pI,mI) specification explicitly done by the user
583 (pbt, mpc) problem type, guard of method
585 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
586 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
587 ((*tracing"### nxt_spec Pbl";*)
588 if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
589 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
590 else case find_first (is_error o #5) (pbl:itm list) of
591 SOME (_, _, _, fd, itm_) =>
593 (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
595 ((*tracing"### nxt_spec is_error NONE";*)
596 case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
598 SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
599 (Pbl, mk_additem fd ct'))
600 | NONE => (*pbl-items complete*)
601 if not preok then (Pbl, Refine_Problem pI')
603 if dI = e_domID then (Pbl, Specify_Theory dI')
604 else if pI = e_pblID then (Pbl, Specify_Problem pI')
605 else if mI = e_metID then (Pbl, Specify_Method mI')
607 case find_first (is_error o #5) met of
608 SOME (_,_,_,fd,itm_) =>
609 (Met, mk_delete (assoc_thy dI) fd itm_)
611 (case nxt_add (assoc_thy dI) oris mpc met of
612 SOME (fd,ct') => (*30.8.01: pre?!?*)
613 (Met, mk_additem fd ct')
615 ((*Solv 3.4.00*)Met, Apply_Method mI))))
617 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
618 ((*tracing"### nxt_spec Met"; *)
619 case find_first (is_error o #5) met of
620 SOME (_,_,_,fd,itm_) =>
621 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
623 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
624 SOME (fd,ct') => (Met, mk_additem fd ct')
626 ((*tracing"### nxt_spec Met: nxt_add NONE";*)
627 if dI = e_domID then (Met, Specify_Theory dI')
628 else if pI = e_pblID then (Met, Specify_Problem pI')
629 else if not preok then (Met, Specify_Method mI)
630 else (Met, Apply_Method mI)));
633 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
634 (2,[2],true,"#Find",Syn("empty"))];
637 fun is_field_correct sel d dscpbt =
638 case assoc (dscpbt, sel) of
640 | SOME ds => member op = ds d;
642 (*. update the itm_ already input, all..from ori .*)
643 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
645 fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) =
647 val ts' = union op = (ts_in itm_) ts;
648 val pval = pbl_ids' thy d ts'
649 (*WN.9.5.03: FIXXXME [#0, epsilon]
650 here would upd_penv be called for [#0, epsilon] etc. *)
651 val complete = if eq_set op = (ts', all) then true else false;
654 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
655 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
656 | (Syn c) => error ("ori_2itm wants to overwrite "^c)
657 | (Typ c) => error ("ori_2itm wants to overwrite "^c)
658 | (Inc _) => if complete
659 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
660 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
661 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
662 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
663 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
664 (* 28.1.00: not completely clear ---^^^ etc.*)
665 (* 4.9.01: Mis just copied---vvv *)
666 | (Mis _) => if complete
667 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
668 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
672 fun eq1 d (_,(d',_)) = (d = d');
673 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
676 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
677 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
678 pval: value for problem-environment _NOT_ checked for 'inter' --
679 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
680 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
681 (*. is_input ori itms <=>
682 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
683 (2) ori(ts) subset itm(ts) --- Err "already input"
684 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
685 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
686 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
688 fun is_notyet_input thy (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
689 case find_first (eq1 d) pbt of
690 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
691 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
693 (case find_first (eq3 f d) itms of
694 SOME (_,_,_,_,itm_) =>
696 val ts' = inter op = (ts_in itm_) ts;
697 in if subset op = (ts, ts')
699 map (Print_Mode.setmp [] (Syntax.string_of_term
700 (thy2ctxt thy)))) ts') ^
701 " already input", e_itm) (*2*)
703 ori_2itm thy itm_ pid all (i,v,f,d,
704 subtract op = ts' ts)) (*3,4*)
706 | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
707 pid all (i,v,f,d,ts)) (*1*)
709 | NONE => ("", ori_2itm thy (Sup (d,ts))
710 e_term all (i,v,f,d,ts));
712 fun test_types thy (d,ts) =
714 val s = !show_types; val _ = show_types:= true;
715 val opt = (try (comp_dts thy)) (d,ts);
716 val msg = case opt of
718 | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) d) ^
720 ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
721 (thy2ctxt thy)))) ts)
723 val _ = show_types:= s
728 fun maxl [] = error "maxl of []"
731 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
735 (*. is the input term t known in oris ?
736 give feedback on all(?) strange input;
737 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
738 (*WN.11.03: from lists*)
739 fun is_known thy sel ori t =
740 (* val (ori,t)=(oris,term_of ct);
743 val ots = (distinct o flat o (map #5)) (ori:ori list);
744 val oids = ((map (fst o dest_Free)) o distinct o
745 flat o (map vars)) ots;
746 val (d,ts(*,pval*)) = split_dts thy t;
747 val ids = map (fst o dest_Free)
748 ((distinct o (flat o (map vars))) ts);
749 in if (subtract op = oids ids) <> []
750 then (("identifiers "^(strs2str' (subtract op = oids ids))^
751 " not in example"), e_ori_, [])
755 if not (subset op = (map typeless ts, map typeless ots))
758 (map (Print_Mode.setmp [] (Syntax.string_of_term
759 (thy2ctxt thy))))) ts)^
760 "' not in example (typeless)"), e_ori_, [])
761 else (case seek_orits thy sel ts ori of
762 ("", ori_ as (_,_,_,d,ts), all) =>
763 (case test_types thy (d,ts) of
764 "" => ("", ori_, all)
765 | msg => (msg, e_ori_, []))
766 | (msg,_,_) => (msg, e_ori_, []))
768 if member op = (map #4 ori) d
769 then seek_oridts thy sel (d,ts) ori
770 else ((Print_Mode.setmp [] (Syntax.string_of_term
772 " not in example", (0, [], sel, d, ts), [])
776 (*. for return-value of appl_add .*)
779 | Err of string; (*error-message*)
782 (** add an item to the model; check wrt. oris and pbt **)
783 (* in contrary to oris<>[] below, this part handles user-input
784 extremely acceptive, i.e. accept input instead error-msg *)
785 fun appl_add thy sel ([]:ori list) ppc pbt ct' =
786 (* val (ppc,pbt,ct',env) = (pbl, (#ppc o get_pbt) cpI, ct, []:envv);
787 !!!! 28.8.01: env tested _minimally_ !!!
790 val i = 1 + (if ppc=[] then 0 else maxl (map #1 ppc));
791 in case parse thy ct' of (*should be done in applicable_in 4.00.FIXME*)
792 NONE => Add (i,[],false,sel,Syn ct')
793 (* val (SOME ct) = parse thy ct';
797 val (d,ts(*,pval*)) = split_dts thy (term_of ct);
799 then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*)))
802 (case find_first (eq1 d) pbt of
803 NONE => Add (i,[],true,sel,Sup ((d,ts)))
805 (* val SOME (f,(_,id)) = find_first (eq1 d) pbt;
808 fun eq2 d ((i,_,_,_,itm_):itm) =
809 (d = (d_in itm_)) andalso i<>0;
810 in case find_first (eq2 d) ppc of
811 NONE => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*)
813 | SOME (i',_,_,_,itm_) =>
814 (* val SOME (i',_,_,_,itm_) = find_first (eq2 d) ppc;
815 val NONE = find_first (eq2 d) ppc;
818 then let val ts = union op = ts (ts_in itm_)
819 in Add (if ts_in itm_ = [] then i else i',
820 [],true,f,Cor ((d, ts), (id, (*pval*)
823 else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*)
830 (*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*)
831 | appl_add thy sel oris ppc pbt (*only for upd_envv*) str =
832 case parse thy str of
833 NONE => Err ("syntax error in " ^ str)
834 | SOME t => case is_known thy sel oris (term_of t) of
836 (case is_notyet_input thy ppc all ori' pbt of
838 | (msg, _) => Err msg)
839 | (msg, _, _) => Err msg;
841 > val (msg,itm) = is_notyet_input thy ppc all ori';
842 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
844 > val ts = ts_in itm_;
848 (** make oris from args of the stac SubProblem and from pbt **)
850 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
851 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
852 fun is_copy_named_idstr str =
853 case (rev o explode) str of
854 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode))
855 "is_copy_named_idstr: " ^ str ^ " T"); true)
856 | _ => (tracing ((strs2str o (rev o explode))
857 "is_copy_named_idstr: " ^ str ^ " F"); false);
858 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
860 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
861 fun is_copy_named_generating_idstr str =
862 if is_copy_named_idstr str
863 then case (rev o explode) str of
864 "'"::"'"::"'"::_ => false
867 fun is_copy_named_generating (_, (_, t)) =
868 (is_copy_named_generating_idstr o free2str) t;
870 (*.split type-wrapper from scr-arg and build part of an ori;
871 an type-error is reported immediately, raises an exn,
872 subsequent handling of exn provides 2nd part of error message.*)
873 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
874 (* val (thy, (str, (dsc, _)), (ty $ var)) =
877 (cterm_of thy (dsc $ var);(*type check*)
878 SOME ((([1], str, dsc, (*[var]*)
879 split_dts' (dsc, var))): preori)(*:ori without leading #*))
880 handle e as TYPE _ =>
881 (tracing (dashs 70 ^ "\n"
882 ^"*** ERROR while creating the items for the model of the ->problem\n"
883 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
884 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
885 ^"*** description: "^(term_detail2str dsc)
886 ^"*** value: "^(term_detail2str var)
887 ^"*** typeconstructor in script: "^(term_detail2str ty)
888 ^"*** checked by theory: "^(theory2str thy)^"\n"
890 OldGoals.print_exn e; (*raises exn again*)
891 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
894 (*.match each pat of the model-pattern with an actual argument;
895 precondition: copy-named vars are filtered out.*)
896 fun matc thy ([]:pat list) _ (oris:preori list) = oris
897 | matc thy pbt [] _ =
899 error ("actual arg(s) missing for '"^pats2str pbt
900 ^"' i.e. should be 'copy-named' by '*_._'"))
901 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
902 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
903 (thy, pbt', ags, []);
905 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
906 (thy, pbt, ags, (oris @ [ori]));
908 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
909 else(*..del?*) let val opt = mtc thy p a;
911 (* val SOME ori = mtc thy p a;
913 SOME ori => matc thy pbt ags (oris @ [ori])
914 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
916 (* run subp-rooteq.sml until Init_Proof before ...
917 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
918 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
920 other vars as in mtc ..
921 > matc thy (drop_last pbt) ags [];
922 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
925 (* generate a new variable "x_i" name from a related given one "x"
926 by use of oris relating "v_i_" (is_copy_named!) to "v_"
927 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
929 (* generate a new variable "x_i" name from a related given one "x"
930 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
931 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
932 but leave is_copy_named_generating as is, e.t. ss''' *)
933 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
934 (if is_copy_named_generating p
935 then (*WN051014 kept strange old code ...*)
936 let fun sel (_,_,d,ts) = comp_ts (d, ts)
937 val cy' = (implode o (drop_last_n 3) o explode o free2str) t
938 val ext = (last_elem o drop_last o explode o free2str) t
939 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
940 val vals = map sel oris
941 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
942 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
943 else ([1], field, dsc, [t])
945 handle _ => error ("cpy_nam: for "^(term2str t));
947 (*.match the actual arguments of a SubProblem with a model-pattern
948 and create an ori list (in root-pbl created from formalization).
949 expects ags:pats = 1:1, while copy-named are filtered out of pats;
950 if no 1:1 the exn raised by matc/mtc and handled at call.
951 copy-named pats are appended in order to get them into the model-items.*)
952 fun match_ags thy (pbt:pat list) ags =
953 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
954 val pbt' = filter_out is_copy_named pbt;
955 val cy = filter is_copy_named pbt;
956 val oris' = matc thy pbt' ags [];
957 val cy' = map (cpy_nam pbt' oris') cy;
958 val ors = add_id (oris' @ cy');
959 (*appended in order to get ^^^^^ into the model-items*)
960 in (map flattup ors):ori list end;
962 (*.report part of the error-msg which is not available in match_args.*)
963 fun match_ags_msg pI stac ags =
964 let val s = !show_types
965 val _ = show_types:= true
966 val pats = (#ppc o get_pbt) pI
967 val msg = (dots 70^"\n"
968 ^"*** problem "^strs2str pI^" has the ...\n"
969 ^"*** model-pattern "^pats2str pats^"\n"
970 ^"*** stac '"^term2str stac^"' has the ...\n"
971 ^"*** arg-list "^terms2str ags^"\n"
973 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
974 val _ = show_types:= s
978 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
979 fun vars_of_pbl_ pbl_ =
980 let fun var_of_pbl_ (gfr,(dsc,t)) = t
981 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
982 fun vars_of_pbl_' pbl_ =
983 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
984 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
986 fun overwrite_ppc thy itm ppc =
988 fun repl ppc' (_,_,_,_,itm_) [] =
989 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
991 | repl ppc' itm (p::ppc) =
992 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
993 else repl (ppc' @ [p]) itm ppc
994 in repl [] itm ppc end;
996 (*10.3.00: insert the already compiled itm into model;
997 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
1000 fun insert_ppc thy itm ppc =
1002 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
1003 | eq_untouched _ _ = false;
1006 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
1007 case seek_ppc (#1 itm) ppc of
1008 (* val SOME xxx = seek_ppc (#1 itm) ppc;
1010 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
1011 overwrite_ppc thy itm ppc
1012 | NONE => (ppc @ [itm]));
1013 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
1015 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
1016 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
1018 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
1019 (d_in itm_) = (d_in iitm_);
1020 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
1021 handles superfluous items carelessly*)
1022 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
1024 > gen_ins' eee (4,[1,3,5,7]);
1025 val it = [1, 3, 5, 7, 4] : int list*)
1028 (*. output the headline to a ppc .*)
1029 fun header p_ pI mI =
1030 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1032 | pos => error ("header called with "^ pos_2str pos);
1035 fun specify_additem sel (ct,_) (p,Met) c pt =
1037 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1038 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1039 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1040 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1041 val cpI = if pI = e_pblID then pI' else pI;
1042 val cmI = if mI = e_metID then mI' else mI;
1043 val {ppc,pre,prls,...} = get_met cmI
1044 in case appl_add thy sel oris met ppc ct of
1045 Add itm (*..union old input *) =>
1046 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1048 val met' = insert_ppc thy itm met;
1049 (*val pt' = update_met pt p met';*)
1050 val ((p,Met),_,_,pt') =
1051 generate1 thy (case sel of
1052 "#Given" => Add_Given' (ct, met')
1053 | "#Find" => Add_Find' (ct, met')
1054 | "#Relate"=> Add_Relation'(ct, met'))
1056 val pre' = check_preconds thy prls pre met'
1057 val pb = foldl and_ (true, map fst pre')
1058 (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
1060 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1061 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1062 in ((p,p_), ((p,p_),Uistate),
1063 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1064 (Method cmI, itms2itemppc thy met' pre'))),
1067 let val pre' = check_preconds thy prls pre met
1068 val pb = foldl and_ (true, map fst pre')
1069 (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
1071 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1072 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1073 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1077 | specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1079 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1080 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1081 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1082 val cpI = if pI = e_pblID then pI' else pI;
1083 val cmI = if mI = e_metID then mI' else mI;
1084 val {ppc,where_,prls,...} = get_pbt cpI;
1085 in case appl_add thy sel oris pbl ppc ct of
1086 Add itm (*..union old input *) =>
1087 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1090 (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
1091 val pbl' = insert_ppc thy itm pbl
1092 val ((p,Pbl),_,_,pt') =
1093 generate1 thy (case sel of
1094 "#Given" => Add_Given' (ct, pbl')
1095 | "#Find" => Add_Find' (ct, pbl')
1096 | "#Relate"=> Add_Relation'(ct, pbl'))
1098 val pre = check_preconds thy prls where_ pbl'
1099 val pb = foldl and_ (true, map fst pre)
1100 (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
1102 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1103 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1104 val ppc = if p_= Pbl then pbl' else met;
1105 in ((p,p_), ((p,p_),Uistate),
1106 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1108 itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1111 let val pre = check_preconds thy prls where_ pbl
1112 val pb = foldl and_ (true, map fst pre)
1113 (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
1115 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1116 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1117 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1119 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1120 val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1124 val (msg,itm) = appl_add thy sel oris ppc ct;
1125 val (Cor(d,ts)) = #5 itm;
1132 (* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1133 specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1135 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1136 let (* either """"""""""""""" all empty or complete *)
1137 val thy = assoc_thy dI';
1138 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1139 else prep_ori fmz thy ((#ppc o get_pbt) pI');
1140 val (pt,c) = cappend_problem e_ptree [] e_istate (fmz,(dI',pI',mI'))
1141 (oris,(dI',pI',mI'),e_term);
1142 val {ppc,prls,where_,...} = get_pbt pI'
1143 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1144 val pt = update_pbl pt [] pbl;
1145 val pre = check_preconds thy prls where_ pbl
1146 val pb = foldl and_ (true, map fst pre)*)
1147 val (pbl, pre, pb) = ([], [], false)
1150 (([],Pbl), (([],Pbl),Uistate),
1151 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1152 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1153 Refine_Tacitly pI', Safe,pt)
1155 (([],Pbl), (([],Pbl),Uistate),
1156 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1157 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1161 (*ONLY for STARTING modeling phase*)
1162 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1163 let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
1165 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
1167 val thy' = if dI = e_domID then dI' else dI
1168 val thy = assoc_thy thy'
1169 val {ppc,prls,where_,...} = get_pbt pI'
1170 val pre = check_preconds thy prls where_ pbl
1171 val pb = foldl and_ (true, map fst pre)
1172 val ((p,_),_,_,pt) =
1173 generate1 thy (Model_Problem'([],pbl,met)) Uistate pos pt
1174 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1175 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1176 in ((p,Pbl), ((p,p_),Uistate),
1177 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1178 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1181 (*. called only if no_met is specified .*)
1182 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1183 let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
1185 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
1187 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1188 (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
1189 (*val pt = update_pbl pt p pbl;
1190 val pt = update_orispec pt p
1191 (string_of_thy thy, pIre,
1192 if length met = 0 then e_metID else hd met);*)
1193 val (domID, metID) = (string_of_thy thy,
1194 if length met = 0 then e_metID else hd met)
1195 val ((p,_),_,_,pt) =
1196 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1198 (*val pre = check_preconds thy prls where_ pbl
1199 val pb = foldl and_ (true, map fst pre)*)
1200 val (pbl, pre, pb) = ([], [], false)
1201 in ((p,Pbl), (pos,Uistate),
1202 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1203 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1204 Model_Problem, Safe, pt) end
1206 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1207 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
1208 (Refine_Problem' rfd) Uistate pos pt
1209 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1210 Model_Problem, Safe, pt) end
1212 (* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
1213 val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
1215 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1216 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1217 meth=met, ...}) = get_obj I pt p;
1218 (*val pt = update_pbl pt p itms;
1219 val pt = update_pblID pt p pI;*)
1220 val thy = assoc_thy dI
1221 val ((p,Pbl),_,_,pt)=
1222 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
1223 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1224 val mI'' = if mI=e_metID then mI' else mI;
1225 (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
1226 val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1227 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1228 in ((p,Pbl), (pos,Uistate),
1229 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1230 (Problem pI, itms2itemppc dI'' itms pre))),
1232 (* val Specify_Method' mID = nxt; val (p,_) = p;
1233 val Specify_Method' mID = m;
1234 specify (Specify_Method' mID) (p,p_) c pt;
1236 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1237 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1238 meth=met, ...}) = get_obj I pt p;
1239 val {ppc,pre,prls,...} = get_met mID
1240 val thy = assoc_thy dI
1241 val oris = add_field' thy ppc oris;
1242 (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1243 val dI'' = if dI=e_domID then dI' else dI;
1244 val pI'' = if pI = e_pblID then pI' else pI;
1245 val met = if met=[] then pbl else met;
1246 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1247 (*val pt = update_met pt p itms;
1248 val pt = update_metID pt p mID*)
1250 generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1251 (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
1252 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1253 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1254 in (pos, (pos,Uistate),
1255 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1256 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1258 (* val Add_Find' ct = nxt; val sel = "#Find";
1260 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1261 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1262 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1263 (* val Specify_Theory' domID = m;
1264 val (Specify_Theory' domID, (p,p_)) = (m, pos);
1266 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1267 let val p_ = case p_ of Met => Met | _ => Pbl
1268 val thy = assoc_thy domID;
1269 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1270 probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
1271 val mppc = case p_ of Met => met | _ => pbl;
1272 val cpI = if pI = e_pblID then pI' else pI;
1273 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1274 val cmI = if mI = e_metID then mI' else mI;
1275 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1278 Met => (check_preconds thy mer mwh met)
1279 | _ => (check_preconds thy per pwh pbl)
1280 val pb = foldl and_ (true, map fst pre)
1283 (*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1284 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1285 (pbl,met) (ppc,mpc) (dI,pI,mI);
1286 in ((p,p_), (pos,Uistate),
1287 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1288 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1290 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1292 (*val pt = update_domID pt p domID;11.8.03*)
1293 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1295 (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1296 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1297 (ppc,mpc) (domID,pI,mI);
1298 in ((p,p_), (pos,Uistate),
1299 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1300 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1303 (* itms2itemppc thy [](*mpc*) pre
1305 | specify m' _ _ _ =
1306 error ("specify: not impl. for "^tac_2str m');
1308 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1309 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1311 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1313 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1314 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1315 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1316 val cpI = if pI = e_pblID then pI' else pI;
1317 in case appl_add thy sel oris pbl ((#ppc o get_pbt) cpI) ct of
1318 Add itm (*..union old input *) =>
1319 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1322 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1323 val pbl' = insert_ppc thy itm pbl
1326 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1327 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1328 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1329 val ((p,Pbl),c,_,pt') =
1330 generate1 thy tac_ Uistate (p,Pbl) pt
1331 in ([(tac,tac_,((p,Pbl),Uistate))], c, (pt',(p,Pbl))):calcstate' end
1334 (*TODO.WN03 pass error-msgs to the frontend..
1335 FIXME ..and dont abuse a tactic for that purpose*)
1337 Tac_ (theory "Pure", msg,msg,msg),
1338 (e_pos', e_istate))], [], ptp)
1341 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1342 val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1344 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1346 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1347 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1348 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1349 val cmI = if mI = e_metID then mI' else mI;
1350 in case appl_add thy sel oris met ((#ppc o get_met) cmI) ct of
1351 Add itm (*..union old input *) =>
1352 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1354 val met' = insert_ppc thy itm met;
1357 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1358 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1359 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1360 val ((p,Met),c,_,pt') =
1361 generate1 thy tac_ Uistate (p,Met) pt
1362 in ([(tac,tac_,((p,Met), Uistate))], c, (pt',(p,Met))) end
1364 | Err msg => ([(*tacis*)], [], ptp)
1365 (*nxt_me collects tacis until not hide; here just no progress*)
1369 val (msg,itm) = appl_add thy sel oris ppc ct;
1370 val (Cor(d,ts)) = #5 itm;
1375 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1376 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1377 handle _ => error ("ori2Coritm: dsc "^
1379 "in ori, but not in pbt")
1381 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1382 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1383 (find_first (eq1 d))) pbt,ts))):itm)
1384 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1385 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1388 (*filter out oris which have same description in itms*)
1389 fun filter_outs oris [] = oris
1390 | filter_outs oris (i::itms) =
1391 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1392 (#4:ori -> term)) oris;
1393 in filter_outs ors itms end;
1395 fun memI a b = member op = a b;
1396 (*filter oris which are in pbt, too*)
1397 fun filter_pbt oris pbt =
1398 let val dscs = map (fst o snd) pbt
1399 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1401 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1402 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1404 fun x mem [] = false
1405 | x mem (y :: ys) = x = y orelse x mem ys;
1407 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1408 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1410 let val vat = max_vt pits;
1412 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1413 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1414 val os = filter_outs ors itms;
1415 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1416 in itms @ (map (ori2Coritm met) os) end
1421 (*.complete model and guard of a calc-head .*)
1423 fun x mem [] = false
1424 | x mem (y :: ys) = x = y orelse x mem ys;
1426 fun complete_mod_ (oris, mpc, ppc, probl) =
1427 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1428 val vat = if probl = [] then 1 else max_vt probl
1429 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1430 val pors = filter_outs pors pits (*which are in pbl already*)
1431 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1433 val pits = pits @ (map (ori2Coritm ppc) pors)
1434 val mits = complete_metitms oris pits [] mpc
1438 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1439 (if dI = e_domID then odI else dI,
1440 if pI = e_pblID then opI else pI,
1441 if mI = e_metID then omI else mI):spec;
1444 (*.find a next applicable tac (for calcstate) and update ptree
1445 (for ev. finding several more tacs due to hide).*)
1446 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1447 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1448 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1449 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1451 val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1452 val (dI, pI, mI) = some_spec ospec spec
1453 val thy = assoc_thy dI
1454 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1455 val {cas, ppc, ...} = get_pbt pI
1456 val pbl = init_pbl ppc (* fill in descriptions *)
1457 (*----------------if you think, this should be done by the Dialog
1458 in the java front-end, search there for WN060225-modelProblem----*)
1459 val (pbl, met) = case cas of NONE => (pbl, [])
1460 | _ => complete_mod_ (oris, mpc, ppc, probl)
1461 (*----------------------------------------------------------------*)
1462 val tac_ = Model_Problem' (pI, pbl, met)
1463 val (pos,c,_,pt) = generate1 thy tac_ Uistate pos pt
1464 in ([(tac,tac_, (pos, Uistate))], c, (pt,pos)):calcstate' end
1466 (* val Add_Find ct = tac;
1468 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1469 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1470 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1472 (*. called only if no_met is specified .*)
1473 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1474 let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1475 val opt = refine_ori oris pI
1478 let val {met,ppc,...} = get_pbt pI'
1479 val pbl = init_pbl ppc
1480 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1481 val mI = if length met = 0 then e_metID else hd met
1482 val thy = assoc_thy dI
1484 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1486 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1487 (pos, Uistate))], c, (pt,pos)) end
1488 | NONE => ([], [], ptp)
1491 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1492 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1493 probl, ...}) = get_obj I pt p
1494 val thy = if dI' = e_domID then dI else dI'
1495 in case refine_pbl (assoc_thy thy) pI probl of
1496 NONE => ([], [], ptp)
1497 | SOME (rfd as (pI',_)) =>
1498 let val (pos,c,_,pt) =
1499 generate1 (assoc_thy thy)
1500 (Refine_Problem' rfd) Uistate pos pt
1501 in ([(Refine_Problem pI, Refine_Problem' rfd,
1502 (pos, Uistate))], c, (pt,pos)) end
1505 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1506 let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1507 probl, ...}) = get_obj I pt p;
1508 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1509 val {ppc,where_,prls,...} = get_pbt pI
1510 val pbl as (_,(itms,_)) =
1511 if pI'=e_pblID andalso pI=e_pblID
1512 then (false, (init_pbl ppc, []))
1513 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1514 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1515 val ((p,Pbl),c,_,pt)=
1516 generate1 thy (Specify_Problem' (pI, pbl)) Uistate pos pt
1517 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1518 (pos,Uistate))], c, (pt,pos)) end
1520 (*transfers oris (not required in pbl) to met-model for script-env
1521 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1522 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1523 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1524 meth=met, ...}) = get_obj I pt p;
1525 val {ppc,pre,prls,...} = get_met mID
1526 val thy = assoc_thy dI
1527 val oris = add_field' thy ppc oris;
1528 val dI'' = if dI=e_domID then dI' else dI;
1529 val pI'' = if pI = e_pblID then pI' else pI;
1530 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1531 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1533 generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1534 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1535 (pos,Uistate))], c, (pt,pos)) end
1537 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1538 let val (dI',_,_) = get_obj g_spec pt p
1540 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1542 in (*FIXXXME: check if pbl can still be parsed*)
1543 ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1546 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1547 let val (dI',_,_) = get_obj g_spec pt p
1549 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1551 in (*FIXXXME: check if met can still be parsed*)
1552 ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1556 error ("nxt_specif: not impl. for "^tac2str m');
1558 (*.get the values from oris; handle the term list w.r.t. penv.*)
1561 fun x mem [] = false
1562 | x mem (y :: ys) = x = y orelse x mem ys;
1564 fun vals_of_oris oris =
1565 ((map (mkval' o (#5:ori -> term list))) o
1566 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1571 (* create a calc-tree with oris via an cas.refined pbl *)
1572 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1573 if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1574 let val {cas, met, ppc, thy, ...} = get_pbt pI
1575 val dI = if dI = "" then theory2theory' thy else dI
1576 val thy = assoc_thy dI
1577 val mI = if mI = [] then hd met else mI
1578 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1579 val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1580 ([], (dI,pI,mI), hdl)
1581 val pt = update_spec pt [] (dI,pI,mI)
1582 val pits = init_pbl' ppc
1583 val pt = update_pbl pt [] pits
1584 in ((pt, ([] ,Pbl)), []) : calcstate end
1585 else if mI <> [] then (* from met-browser *)
1586 let val {ppc,...} = get_met mI
1587 val dI = if dI = "" then "Isac" else dI
1588 val thy = assoc_thy dI
1589 val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1590 ([], (dI,pI,mI), e_term(*FIXME met*))
1591 val pt = update_spec pt [] (dI,pI,mI)
1592 val mits = init_pbl' ppc
1593 val pt = update_met pt [] mits
1594 in ((pt, ([], Met)), []) : calcstate end
1595 else (* new example, pepare for interactive modeling *)
1596 let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec)
1597 ([], e_spec, e_term)
1598 in ((pt,([],Pbl)), []) : calcstate end
1599 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1600 let (* both """"""""""""""""""""""""" either empty or complete *)
1601 val thy = assoc_thy dI
1602 val (pI, pors, mI) =
1604 then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI)
1605 val pI' = refine_ori' pors pI;
1606 in (pI', pors(*refinement over models with diff.precond only*),
1607 (hd o #met o get_pbt) pI') end
1608 else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI)
1609 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1610 val dI = theory2theory' (maxthy thy thy');
1611 val hdl = case cas of
1612 NONE => pblterm dI pI
1613 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1614 ~~~ vals_of_oris pors) t
1615 val (pt, _) = cappend_problem e_ptree [] e_istate (fmz, (dI, pI, mI))
1616 (pors, (dI, pI, mI), hdl)
1617 in ((pt, ([], Pbl)),
1618 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1624 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1625 (* case appl_spec p pt m of /// 19.1.00
1626 Notappl e => Error' (Error_ e)
1628 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1632 (*fun tag_form thy (formal, given) = cterm_of thy
1633 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1634 fun tag_form thy (formal, given) =
1635 (let val gf = (head_of given) $ formal;
1636 val _ = cterm_of thy gf
1639 error ("calchead.tag_form: " ^
1640 Print_Mode.setmp [] (Syntax.string_of_term
1641 (thy2ctxt thy)) given ^ " .. " ^
1642 Print_Mode.setmp [] (Syntax.string_of_term
1643 (thy2ctxt thy)) formal ^
1644 " ..types do not match");
1645 (* val formal = (the o (parse thy)) "[R::real]";
1646 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1647 > tag_form thy (formal, given);
1648 val it = "fixed_values [R]" : cterm
1651 fun chktyp thy (n, fs, gs) =
1652 ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1654 (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1656 tag_form thy (nth n fs, nth n gs));
1657 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1659 (* #####################################################
1660 find the failing item:
1662 > val tag__form = chktyp (n,formals,givens);
1663 > (type_of o term_of o (nth n)) formals;
1664 > (type_of o term_of o (nth n)) givens;
1665 > atomty ((term_of o (nth n)) formals);
1666 > atomty ((term_of o (nth n)) givens);
1667 > atomty (term_of tag__form);
1668 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1669 ##################################################### *)
1671 (* #####################################################
1673 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1674 val formals = map (the o (parse thy)) origin;
1676 val given = ["equation (lhs=rhs)",
1677 "bound_variable bdv", (* TODO type *)
1679 val where_ = ["e is_root_equation_in bdv",
1681 "apx is_const_expr"];
1682 val find = ["L::rat set"];
1683 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1684 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1685 val givens = map (the o (parse thy)) given;
1687 val tag__forms = chktyps (formals, givens);
1688 map ((atomty) o term_of) tag__forms;
1689 ##################################################### *)
1692 (* check pbltypes, announces one failure a time *)
1693 (*fun chk_vars ctppc =
1694 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1695 appc flat (mappc (vars o term_of) ctppc)
1696 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1697 else if (re\\(gi union fi)) <> []
1698 then ("re\\(gi union fi)",re\\(gi union fi))
1699 else ("ok",[]) end;*)
1700 fun chk_vars ctppc =
1701 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1702 appc flat (mappc vars ctppc)
1703 val chked = subtract op = gi wh
1704 in if chked <> [] then ("wh\\gi", chked)
1705 else let val chked = subtract op = (union op = gi fi) re
1707 then ("re\\(gi union fi)", chked)
1712 (* check a new pbltype: variables (Free) unbound by given, find*)
1713 fun unbound_ppc ctppc =
1714 let val {Given=gi,Find=fi,Relate=re,...} =
1715 appc flat (mappc vars ctppc)
1716 in distinct (*re\\(gi union fi)*)
1717 (subtract op = (union op = gi fi) re) end;
1719 > val org = {Given=["[R=(R::real)]"],Where=[],
1720 Find=["[A::real]"],With=[],
1721 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1723 > val ctppc = mappc (the o (parse thy)) org;
1724 > unbound_ppc ctppc;
1725 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1729 (* f, a binary operator, is nested rightassociative *)
1732 fun fld f (x::[]) = x
1733 | fld f (x::x'::[]) = f (x',x)
1734 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1735 in ((fld f) o rev) xs end;
1737 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1738 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1739 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1740 > cterm_of thy conj;
1741 val it = "(a = b & c = d) & e = f" : cterm
1744 (* f, a binary operator, is nested leftassociative *)
1745 fun foldl1 f (x::[]) = x
1746 | foldl1 f (x::x'::[]) = f (x,x')
1747 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1749 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1750 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1751 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1752 > cterm_of thy conj;
1753 val it = "a = b & c = d & e = f & g = h" : cterm
1757 (* called only once, if a Subproblem has been located in the script*)
1758 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
1759 (* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
1763 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1764 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1765 (*all stored in tac_ itms ^^^^^^^^^^*)
1766 | nxt_model_pbl tac_ _ =
1767 error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1768 (* run subp_rooteq.sml ''
1769 until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
1770 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1771 (last_elem o drop_last) ets'';
1772 > val mst = (last_elem o drop_last) ets'';
1773 > nxt_model_pbl mst;
1774 val it = Refine_Tacitly ["univariate","equation"] : tac
1777 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1778 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1779 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1782 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1783 + met from fmz; assumes pos on PblObj, meth = [].*)
1784 fun complete_mod (pt, pos as (p, p_):pos') =
1785 (* val (pt, (p, _)) = (pt, p);
1786 val (pt, (p, _)) = (pt, pos);
1788 let val _= if p_ <> Pbl
1789 then tracing("###complete_mod: only impl.for Pbl, called with "^
1790 pos'2str pos) else ()
1791 val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
1793 val (dI,pI,mI) = some_spec ospec spec
1794 val mpc = (#ppc o get_met) mI
1795 val ppc = (#ppc o get_pbt) pI
1796 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1797 val pt = update_pblppc pt p pits
1798 val pt = update_metppc pt p mits
1799 in (pt, (p,Met):pos') end
1801 (*| complete_mod (pt, pos as (p, Met):pos') =
1802 error ("###complete_mod: only impl.for Pbl, called with "^
1805 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1806 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1807 fun all_modspec (pt, (p,_):pos') =
1808 (* val (pt, (p,_)) = ptp;
1810 let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1811 ...}) = get_obj I pt p;
1812 val thy = assoc_thy dI;
1813 val {ppc,...} = get_met mI;
1814 val mors = prep_ori fmz_ thy ppc;
1815 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1816 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1817 val pt = update_spec pt p (dI,pI,mI);
1818 in (pt, (p,Met): pos') end;
1820 (*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1821 fun is_complete_mod_ ([]: itm list) = false
1822 | is_complete_mod_ itms =
1823 foldl and_ (true, (map #3 itms));
1824 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1825 if (is_pblobj o (get_obj I pt)) p
1826 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1827 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1828 | is_complete_mod (pt, pos as (p, Met)) =
1829 if (is_pblobj o (get_obj I pt)) p
1830 then (is_complete_mod_ o (get_obj g_met pt)) p
1831 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1832 | is_complete_mod (_, pos) =
1833 error ("is_complete_mod called by "^pos'2str pos^
1834 " (should be Pbl or Met)");
1836 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1837 fun is_complete_spec (pt, pos as (p,_): pos') =
1838 if (not o is_pblobj o (get_obj I pt)) p
1839 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1840 else let val (dI,pI,mI) = get_obj g_spec pt p
1841 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1842 (*.complete empty items in specification from origin (pbl, met ev.refined);
1843 assumes 'is_complete_mod'.*)
1844 fun complete_spec (pt, pos as (p,_): pos') =
1845 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1846 val pt = update_spec pt p (some_spec ospec spec)
1849 fun is_complete_modspec ptp =
1850 is_complete_mod ptp andalso is_complete_spec ptp;
1855 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1856 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1858 let val (_,_,metID) = get_somespec' spec spec'
1860 if metID = e_metID then []
1861 else let val {prls,pre=where_,...} = get_met metID
1862 val pre = check_preconds' prls where_ meth 0
1864 val allcorrect = is_complete_mod_ meth
1865 andalso foldl and_ (true, (map #1 pre))
1866 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1867 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1868 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1870 let val (_,pI,_) = get_somespec' spec spec'
1872 if pI = e_pblID then []
1873 else let val {prls,where_,cas,...} = get_pbt pI
1874 val pre = check_preconds' prls where_ probl 0
1876 val allcorrect = is_complete_mod_ probl
1877 andalso foldl and_ (true, (map #1 pre))
1878 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1881 fun pt_form (PrfObj {form,...}) = Form form
1882 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1883 let val (dI, pI, _) = get_somespec' spec spec'
1884 val {cas,...} = get_pbt pI
1886 NONE => Form (pblterm dI pI)
1887 | SOME t => Form (subst_atomic (mk_env probl) t)
1889 (*vvv takes the tac _generating_ the formula=result, asm ok....
1890 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1892 if null asm then NONE else SOME asm,
1894 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1895 let val (_,_,metID) = some_spec ospec spec
1897 if null asm then NONE else SOME asm,
1898 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1899 -------------------------------------------------------------------------*)
1902 (*.pt_extract returns
1903 # the formula at pos
1904 # the tactic applied to this formula
1905 # the list of assumptions generated at this formula
1906 (by application of another tac to the preceding formula !)
1907 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1908 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1909 fun pt_extract (pt,([],Res)) =
1910 (* val (pt,([],Res)) = ptp;
1912 let val (f, asm) = get_obj g_result pt []
1913 in (Form f, NONE, asm) end
1916 | pt_extract (pt,(p,Res)) =
1917 (* val (pt,(p,Res)) = ptp;
1919 let val (f, asm) = get_obj g_result pt p
1920 val tac = if last_onlev pt p
1921 then if is_pblobj' pt (lev_up p)
1922 then let val (PblObj{spec=(_,pI,_),...}) =
1923 get_obj I pt (lev_up p)
1924 in if pI = e_pblID then NONE
1925 else SOME (Check_Postcond pI) end
1926 else SOME End_Trans (*WN0502 TODO for other branches*)
1927 else let val p' = lev_on p
1928 in if is_pblobj' pt p'
1929 then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1931 in SOME (Subproblem (dI, pI)) end
1932 else if f = get_obj g_form pt p'
1933 then SOME (get_obj g_tac pt p')
1934 (*because this Frm ~~~is not on worksheet*)
1935 else SOME (Take (term2str (get_obj g_form pt p')))
1937 in (Form f, tac, asm) end
1939 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1940 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1941 val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
1943 let val ppobj = get_obj I pt p
1944 val f = if is_pblobj ppobj then pt_model ppobj p_
1945 else get_obj pt_form pt p
1946 val tac = g_tac ppobj
1947 in (f, SOME tac, []) end;
1950 (**. get the formula from a ctree-node:
1951 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1952 take res from all other PrfObj's .**)
1953 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1954 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1955 [("headline", (p, Frm), h),
1956 ("stepform", (p, Res), r)]
1957 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1958 [("stepform", (p, Frm), form),
1959 ("stepform", (p, Res), r)];
1961 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1962 [("stepform", (p, Res), r)]
1964 (*assumes to take whole level, in particular hd -- for use in interSteps*)
1965 fun get_formress fs p [] = flat fs
1966 | get_formress fs p (nd::nds) =
1967 (* start with 'form+res' and continue with trying 'res' only*)
1968 get_forms (fs @ [formres p nd]) (lev_on p) nds
1969 and get_forms fs p [] = flat fs
1970 | get_forms fs p (nd::nds) =
1972 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1973 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1974 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1975 (* continue with trying 'res' only*)
1976 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1978 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1979 (*WN050219 made robust against _'to' below or after Complete nodes
1980 by handling exn caused by move_dn*)
1981 (*WN0401 this functionality belongs to ctree.sml,
1982 but fetching a calc_head requires calculations defined in modspec.sml
1983 transfer to ME/me.sml !!!
1984 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1985 is returned !!!!!!!!!!!!!
1987 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1988 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1989 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1993 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1997 | eq_pos' _ _ = false;
1999 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
2000 total ordering Position#compareTo(Position p) in the java-code
2001 val get_interval = fn
2002 : pos' -> : from is "move_up 1st-element" to return
2003 pos' -> : to the last element to be returned; from < to
2004 int -> : level: 0 gets the flattest sub-tree possible
2005 >999 gets the deepest sub-tree possible
2007 (pos' * : of the formula
2008 Term.term) : the formula
2011 fun get_interval from to level pt =
2012 (* val (from,level) = (f,lev);
2013 val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
2015 let fun get_inter c (from:pos') (to:pos') lev pt =
2016 (* val (c, from, to, lev) = ([], from, to, level);
2017 ------for recursion.......
2018 val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
2020 if eq_pos' from to orelse from = ([],Res)
2021 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
2022 if 'to' has values NOT generated by move_dn, see systest/me.sml
2023 TODO.WN0501: introduce an order on pos' and check "from > to"..
2024 ...there is an order in Java!
2025 WN051224 the hack got worse with returning term instead ptform*)
2026 then let val (f,_,_) = pt_extract (pt, from)
2028 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2029 | Form t => c @ [(from, t)]
2032 if lev < lev_of from
2033 then (get_inter c (move_dn [] pt from) to lev pt)
2034 handle (PTREE _(*from move_dn too far*)) => c
2035 else let val (f,_,_) = pt_extract (pt, from)
2036 val term = case f of
2037 ModSpec (_,_,headline,_,_,_)=> headline
2039 in (get_inter (c @ [(from, term)])
2040 (move_dn [] pt from) to lev pt)
2041 handle (PTREE _(*from move_dn too far*))
2042 => c @ [(from, term)] end
2043 in get_inter [] from to level pt end;
2046 fun posform2str (pos:pos', form) =
2047 "("^ pos'2str pos ^", "^
2049 Form f => term2str f
2050 | ModSpec c => term2str (#3 c(*the headline*)))
2052 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2053 (map posform2str)) pfs;
2054 fun posterm2str (pos:pos', t) =
2055 "("^ pos'2str pos ^", "^term2str t^")";
2056 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2057 (map posterm2str)) pfs;
2060 (*WN050225 omits the last step, if pt is incomplete*)
2062 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
2064 (*.get a calchead from a PblObj-node in the ctree;
2065 preconditions must be calculated.*)
2066 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
2067 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
2069 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2070 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
2071 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
2072 | get_ocalhd (pt, pos' as (p,Met):pos') =
2073 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2076 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2077 val pre = check_preconds (assoc_thy"Isac") prls pre meth
2078 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
2080 (*.at the activeFormula set the Model, the Guard and the Specification
2081 to empty and return a CalcHead;
2082 the 'origin' remains (for reconstructing all that).*)
2083 fun reset_calchead (pt, pos' as (p,_):pos') =
2084 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
2085 val pt = update_pbl pt p []
2086 val pt = update_met pt p []
2087 val pt = update_spec pt p e_spec
2088 in (pt, (p,Pbl):pos') end;
2090 (*---------------------------------------------------------------------*)
2094 (*---------------------------------------------------------------------*)