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 Symbol.explode) str of
854 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
855 "is_copy_named_idstr: " ^ str ^ " T"); true)
856 | _ => (tracing ((strs2str o (rev o Symbol.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 Symbol.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 writeln (PolyML.makestring e);
893 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
896 (*.match each pat of the model-pattern with an actual argument;
897 precondition: copy-named vars are filtered out.*)
898 fun matc thy ([]:pat list) _ (oris:preori list) = oris
899 | matc thy pbt [] _ =
901 error ("actual arg(s) missing for '"^pats2str pbt
902 ^"' i.e. should be 'copy-named' by '*_._'"))
903 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
904 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
905 (thy, pbt', ags, []);
907 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
908 (thy, pbt, ags, (oris @ [ori]));
910 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
911 else(*..del?*) let val opt = mtc thy p a;
913 (* val SOME ori = mtc thy p a;
915 SOME ori => matc thy pbt ags (oris @ [ori])
916 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
918 (* run subp-rooteq.sml until Init_Proof before ...
919 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
920 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
922 other vars as in mtc ..
923 > matc thy (drop_last pbt) ags [];
924 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
927 (* generate a new variable "x_i" name from a related given one "x"
928 by use of oris relating "v_i_" (is_copy_named!) to "v_"
929 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
931 (* generate a new variable "x_i" name from a related given one "x"
932 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
933 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
934 but leave is_copy_named_generating as is, e.t. ss''' *)
935 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
936 (if is_copy_named_generating p
937 then (*WN051014 kept strange old code ...*)
938 let fun sel (_,_,d,ts) = comp_ts (d, ts)
939 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
940 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
941 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
942 val vals = map sel oris
943 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
944 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
945 else ([1], field, dsc, [t])
947 handle _ => error ("cpy_nam: for "^(term2str t));
949 (*.match the actual arguments of a SubProblem with a model-pattern
950 and create an ori list (in root-pbl created from formalization).
951 expects ags:pats = 1:1, while copy-named are filtered out of pats;
952 if no 1:1 the exn raised by matc/mtc and handled at call.
953 copy-named pats are appended in order to get them into the model-items.*)
954 fun match_ags thy (pbt:pat list) ags =
955 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
956 val pbt' = filter_out is_copy_named pbt;
957 val cy = filter is_copy_named pbt;
958 val oris' = matc thy pbt' ags [];
959 val cy' = map (cpy_nam pbt' oris') cy;
960 val ors = add_id (oris' @ cy');
961 (*appended in order to get ^^^^^ into the model-items*)
962 in (map flattup ors):ori list end;
964 (*.report part of the error-msg which is not available in match_args.*)
965 fun match_ags_msg pI stac ags =
966 let (*val s = !show_types
967 val _ = show_types:= true*)
968 val pats = (#ppc o get_pbt) pI
969 val msg = (dots 70^"\n"
970 ^"*** problem "^strs2str pI^" has the ...\n"
971 ^"*** model-pattern "^pats2str pats^"\n"
972 ^"*** stac '"^term2str stac^"' has the ...\n"
973 ^"*** arg-list "^terms2str ags^"\n"
975 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
976 (*val _ = show_types:= s*)
980 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
981 fun vars_of_pbl_ pbl_ =
982 let fun var_of_pbl_ (gfr,(dsc,t)) = t
983 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
984 fun vars_of_pbl_' pbl_ =
985 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
986 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
988 fun overwrite_ppc thy itm ppc =
990 fun repl ppc' (_,_,_,_,itm_) [] =
991 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
993 | repl ppc' itm (p::ppc) =
994 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
995 else repl (ppc' @ [p]) itm ppc
996 in repl [] itm ppc end;
998 (*10.3.00: insert the already compiled itm into model;
999 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
1002 fun insert_ppc thy itm ppc =
1004 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
1005 | eq_untouched _ _ = false;
1008 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
1009 case seek_ppc (#1 itm) ppc of
1010 (* val SOME xxx = seek_ppc (#1 itm) ppc;
1012 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
1013 overwrite_ppc thy itm ppc
1014 | NONE => (ppc @ [itm]));
1015 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
1017 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
1018 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
1020 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
1021 (d_in itm_) = (d_in iitm_);
1022 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
1023 handles superfluous items carelessly*)
1024 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
1026 > gen_ins' eee (4,[1,3,5,7]);
1027 val it = [1, 3, 5, 7, 4] : int list*)
1030 (*. output the headline to a ppc .*)
1031 fun header p_ pI mI =
1032 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1034 | pos => error ("header called with "^ pos_2str pos);
1037 fun specify_additem sel (ct,_) (p,Met) c pt =
1039 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1040 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1041 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1042 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1043 val cpI = if pI = e_pblID then pI' else pI;
1044 val cmI = if mI = e_metID then mI' else mI;
1045 val {ppc,pre,prls,...} = get_met cmI
1046 in case appl_add thy sel oris met ppc ct of
1047 Add itm (*..union old input *) =>
1048 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1050 val met' = insert_ppc thy itm met;
1051 (*val pt' = update_met pt p met';*)
1052 val ((p,Met),_,_,pt') =
1053 generate1 thy (case sel of
1054 "#Given" => Add_Given' (ct, met')
1055 | "#Find" => Add_Find' (ct, met')
1056 | "#Relate"=> Add_Relation'(ct, met'))
1058 val pre' = check_preconds thy prls pre met'
1059 val pb = foldl and_ (true, map fst pre')
1060 (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
1062 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1063 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1064 in ((p,p_), ((p,p_),Uistate),
1065 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1066 (Method cmI, itms2itemppc thy met' pre'))),
1069 let val pre' = check_preconds thy prls pre met
1070 val pb = foldl and_ (true, map fst pre')
1071 (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
1073 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1074 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1075 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1079 | specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1081 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1082 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1083 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1084 val cpI = if pI = e_pblID then pI' else pI;
1085 val cmI = if mI = e_metID then mI' else mI;
1086 val {ppc,where_,prls,...} = get_pbt cpI;
1087 in case appl_add thy sel oris pbl ppc ct of
1088 Add itm (*..union old input *) =>
1089 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1092 (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
1093 val pbl' = insert_ppc thy itm pbl
1094 val ((p,Pbl),_,_,pt') =
1095 generate1 thy (case sel of
1096 "#Given" => Add_Given' (ct, pbl')
1097 | "#Find" => Add_Find' (ct, pbl')
1098 | "#Relate"=> Add_Relation'(ct, pbl'))
1100 val pre = check_preconds thy prls where_ pbl'
1101 val pb = foldl and_ (true, map fst pre)
1102 (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
1104 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1105 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1106 val ppc = if p_= Pbl then pbl' else met;
1107 in ((p,p_), ((p,p_),Uistate),
1108 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1110 itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1113 let val pre = check_preconds thy prls where_ pbl
1114 val pb = foldl and_ (true, map fst pre)
1115 (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
1117 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1118 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1119 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1121 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1122 val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1126 val (msg,itm) = appl_add thy sel oris ppc ct;
1127 val (Cor(d,ts)) = #5 itm;
1134 (* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1135 specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1137 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1138 let (* either """"""""""""""" all empty or complete *)
1139 val thy = assoc_thy dI';
1140 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1141 else prep_ori fmz thy ((#ppc o get_pbt) pI');
1142 val (pt,c) = cappend_problem e_ptree [] e_istate (fmz,(dI',pI',mI'))
1143 (oris,(dI',pI',mI'),e_term);
1144 val {ppc,prls,where_,...} = get_pbt pI'
1145 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1146 val pt = update_pbl pt [] pbl;
1147 val pre = check_preconds thy prls where_ pbl
1148 val pb = foldl and_ (true, map fst pre)*)
1149 val (pbl, pre, pb) = ([], [], false)
1152 (([],Pbl), (([],Pbl),Uistate),
1153 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1154 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1155 Refine_Tacitly pI', Safe,pt)
1157 (([],Pbl), (([],Pbl),Uistate),
1158 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1159 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1163 (*ONLY for STARTING modeling phase*)
1164 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1165 let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
1167 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
1169 val thy' = if dI = e_domID then dI' else dI
1170 val thy = assoc_thy thy'
1171 val {ppc,prls,where_,...} = get_pbt pI'
1172 val pre = check_preconds thy prls where_ pbl
1173 val pb = foldl and_ (true, map fst pre)
1174 val ((p,_),_,_,pt) =
1175 generate1 thy (Model_Problem'([],pbl,met)) Uistate pos pt
1176 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1177 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1178 in ((p,Pbl), ((p,p_),Uistate),
1179 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1180 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1183 (*. called only if no_met is specified .*)
1184 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1185 let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
1187 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
1189 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1190 (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
1191 (*val pt = update_pbl pt p pbl;
1192 val pt = update_orispec pt p
1193 (string_of_thy thy, pIre,
1194 if length met = 0 then e_metID else hd met);*)
1195 val (domID, metID) = (string_of_thy thy,
1196 if length met = 0 then e_metID else hd met)
1197 val ((p,_),_,_,pt) =
1198 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1200 (*val pre = check_preconds thy prls where_ pbl
1201 val pb = foldl and_ (true, map fst pre)*)
1202 val (pbl, pre, pb) = ([], [], false)
1203 in ((p,Pbl), (pos,Uistate),
1204 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1205 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1206 Model_Problem, Safe, pt) end
1208 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1209 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
1210 (Refine_Problem' rfd) Uistate pos pt
1211 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1212 Model_Problem, Safe, pt) end
1214 (* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
1215 val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
1217 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1218 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1219 meth=met, ...}) = get_obj I pt p;
1220 (*val pt = update_pbl pt p itms;
1221 val pt = update_pblID pt p pI;*)
1222 val thy = assoc_thy dI
1223 val ((p,Pbl),_,_,pt)=
1224 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
1225 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1226 val mI'' = if mI=e_metID then mI' else mI;
1227 (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
1228 val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1229 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1230 in ((p,Pbl), (pos,Uistate),
1231 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1232 (Problem pI, itms2itemppc dI'' itms pre))),
1234 (* val Specify_Method' mID = nxt; val (p,_) = p;
1235 val Specify_Method' mID = m;
1236 specify (Specify_Method' mID) (p,p_) c pt;
1238 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1239 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1240 meth=met, ...}) = get_obj I pt p;
1241 val {ppc,pre,prls,...} = get_met mID
1242 val thy = assoc_thy dI
1243 val oris = add_field' thy ppc oris;
1244 (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1245 val dI'' = if dI=e_domID then dI' else dI;
1246 val pI'' = if pI = e_pblID then pI' else pI;
1247 val met = if met=[] then pbl else met;
1248 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1249 (*val pt = update_met pt p itms;
1250 val pt = update_metID pt p mID*)
1252 generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1253 (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
1254 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1255 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1256 in (pos, (pos,Uistate),
1257 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1258 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1260 (* val Add_Find' ct = nxt; val sel = "#Find";
1262 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1263 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1264 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1265 (* val Specify_Theory' domID = m;
1266 val (Specify_Theory' domID, (p,p_)) = (m, pos);
1268 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1269 let val p_ = case p_ of Met => Met | _ => Pbl
1270 val thy = assoc_thy domID;
1271 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1272 probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
1273 val mppc = case p_ of Met => met | _ => pbl;
1274 val cpI = if pI = e_pblID then pI' else pI;
1275 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1276 val cmI = if mI = e_metID then mI' else mI;
1277 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1280 Met => (check_preconds thy mer mwh met)
1281 | _ => (check_preconds thy per pwh pbl)
1282 val pb = foldl and_ (true, map fst pre)
1285 (*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1286 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1287 (pbl,met) (ppc,mpc) (dI,pI,mI);
1288 in ((p,p_), (pos,Uistate),
1289 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1290 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1292 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1294 (*val pt = update_domID pt p domID;11.8.03*)
1295 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1297 (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1298 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1299 (ppc,mpc) (domID,pI,mI);
1300 in ((p,p_), (pos,Uistate),
1301 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1302 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1305 (* itms2itemppc thy [](*mpc*) pre
1307 | specify m' _ _ _ =
1308 error ("specify: not impl. for "^tac_2str m');
1310 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1311 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1313 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1315 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1316 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1317 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1318 val cpI = if pI = e_pblID then pI' else pI;
1319 in case appl_add thy sel oris pbl ((#ppc o get_pbt) cpI) ct of
1320 Add itm (*..union old input *) =>
1321 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1324 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1325 val pbl' = insert_ppc thy itm pbl
1328 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1329 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1330 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1331 val ((p,Pbl),c,_,pt') =
1332 generate1 thy tac_ Uistate (p,Pbl) pt
1333 in ([(tac,tac_,((p,Pbl),Uistate))], c, (pt',(p,Pbl))):calcstate' end
1336 (*TODO.WN03 pass error-msgs to the frontend..
1337 FIXME ..and dont abuse a tactic for that purpose*)
1339 Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1340 (e_pos', e_istate))], [], ptp)
1343 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1344 val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1346 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1348 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1349 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1350 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1351 val cmI = if mI = e_metID then mI' else mI;
1352 in case appl_add thy sel oris met ((#ppc o get_met) cmI) ct of
1353 Add itm (*..union old input *) =>
1354 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1356 val met' = insert_ppc thy itm met;
1359 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1360 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1361 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1362 val ((p,Met),c,_,pt') =
1363 generate1 thy tac_ Uistate (p,Met) pt
1364 in ([(tac,tac_,((p,Met), Uistate))], c, (pt',(p,Met))) end
1366 | Err msg => ([(*tacis*)], [], ptp)
1367 (*nxt_me collects tacis until not hide; here just no progress*)
1371 val (msg,itm) = appl_add thy sel oris ppc ct;
1372 val (Cor(d,ts)) = #5 itm;
1377 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1378 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1379 handle _ => error ("ori2Coritm: dsc "^
1381 "in ori, but not in pbt")
1383 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1384 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1385 (find_first (eq1 d))) pbt,ts))):itm)
1386 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1387 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1390 (*filter out oris which have same description in itms*)
1391 fun filter_outs oris [] = oris
1392 | filter_outs oris (i::itms) =
1393 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1394 (#4:ori -> term)) oris;
1395 in filter_outs ors itms end;
1397 fun memI a b = member op = a b;
1398 (*filter oris which are in pbt, too*)
1399 fun filter_pbt oris pbt =
1400 let val dscs = map (fst o snd) pbt
1401 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1403 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1404 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1406 fun x mem [] = false
1407 | x mem (y :: ys) = x = y orelse x mem ys;
1409 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1410 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1412 let val vat = max_vt pits;
1414 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1415 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1416 val os = filter_outs ors itms;
1417 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1418 in itms @ (map (ori2Coritm met) os) end
1423 (*.complete model and guard of a calc-head .*)
1425 fun x mem [] = false
1426 | x mem (y :: ys) = x = y orelse x mem ys;
1428 fun complete_mod_ (oris, mpc, ppc, probl) =
1429 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1430 val vat = if probl = [] then 1 else max_vt probl
1431 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1432 val pors = filter_outs pors pits (*which are in pbl already*)
1433 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1435 val pits = pits @ (map (ori2Coritm ppc) pors)
1436 val mits = complete_metitms oris pits [] mpc
1440 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1441 (if dI = e_domID then odI else dI,
1442 if pI = e_pblID then opI else pI,
1443 if mI = e_metID then omI else mI):spec;
1446 (*.find a next applicable tac (for calcstate) and update ptree
1447 (for ev. finding several more tacs due to hide).*)
1448 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1449 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1450 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1451 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1453 val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1454 val (dI, pI, mI) = some_spec ospec spec
1455 val thy = assoc_thy dI
1456 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1457 val {cas, ppc, ...} = get_pbt pI
1458 val pbl = init_pbl ppc (* fill in descriptions *)
1459 (*----------------if you think, this should be done by the Dialog
1460 in the java front-end, search there for WN060225-modelProblem----*)
1461 val (pbl, met) = case cas of NONE => (pbl, [])
1462 | _ => complete_mod_ (oris, mpc, ppc, probl)
1463 (*----------------------------------------------------------------*)
1464 val tac_ = Model_Problem' (pI, pbl, met)
1465 val (pos,c,_,pt) = generate1 thy tac_ Uistate pos pt
1466 in ([(tac,tac_, (pos, Uistate))], c, (pt,pos)):calcstate' end
1468 (* val Add_Find ct = tac;
1470 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1471 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1472 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1474 (*. called only if no_met is specified .*)
1475 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1476 let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1477 val opt = refine_ori oris pI
1480 let val {met,ppc,...} = get_pbt pI'
1481 val pbl = init_pbl ppc
1482 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1483 val mI = if length met = 0 then e_metID else hd met
1484 val thy = assoc_thy dI
1486 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1488 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1489 (pos, Uistate))], c, (pt,pos)) end
1490 | NONE => ([], [], ptp)
1493 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1494 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1495 probl, ...}) = get_obj I pt p
1496 val thy = if dI' = e_domID then dI else dI'
1497 in case refine_pbl (assoc_thy thy) pI probl of
1498 NONE => ([], [], ptp)
1499 | SOME (rfd as (pI',_)) =>
1500 let val (pos,c,_,pt) =
1501 generate1 (assoc_thy thy)
1502 (Refine_Problem' rfd) Uistate pos pt
1503 in ([(Refine_Problem pI, Refine_Problem' rfd,
1504 (pos, Uistate))], c, (pt,pos)) end
1507 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1508 let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1509 probl, ...}) = get_obj I pt p;
1510 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1511 val {ppc,where_,prls,...} = get_pbt pI
1512 val pbl as (_,(itms,_)) =
1513 if pI'=e_pblID andalso pI=e_pblID
1514 then (false, (init_pbl ppc, []))
1515 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1516 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1517 val ((p,Pbl),c,_,pt)=
1518 generate1 thy (Specify_Problem' (pI, pbl)) Uistate pos pt
1519 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1520 (pos,Uistate))], c, (pt,pos)) end
1522 (*transfers oris (not required in pbl) to met-model for script-env
1523 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1524 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1525 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1526 meth=met, ...}) = get_obj I pt p;
1527 val {ppc,pre,prls,...} = get_met mID
1528 val thy = assoc_thy dI
1529 val oris = add_field' thy ppc oris;
1530 val dI'' = if dI=e_domID then dI' else dI;
1531 val pI'' = if pI = e_pblID then pI' else pI;
1532 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1533 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1535 generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1536 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1537 (pos,Uistate))], c, (pt,pos)) end
1539 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1540 let val (dI',_,_) = get_obj g_spec pt p
1542 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1544 in (*FIXXXME: check if pbl can still be parsed*)
1545 ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1548 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1549 let val (dI',_,_) = get_obj g_spec pt p
1551 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1553 in (*FIXXXME: check if met can still be parsed*)
1554 ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1558 error ("nxt_specif: not impl. for "^tac2str m');
1560 (*.get the values from oris; handle the term list w.r.t. penv.*)
1563 fun x mem [] = false
1564 | x mem (y :: ys) = x = y orelse x mem ys;
1566 fun vals_of_oris oris =
1567 ((map (mkval' o (#5:ori -> term list))) o
1568 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1573 (* create a calc-tree with oris via an cas.refined pbl *)
1574 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1575 if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1576 let val {cas, met, ppc, thy, ...} = get_pbt pI
1577 val dI = if dI = "" then theory2theory' thy else dI
1578 val thy = assoc_thy dI
1579 val mI = if mI = [] then hd met else mI
1580 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1581 val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1582 ([], (dI,pI,mI), hdl)
1583 val pt = update_spec pt [] (dI,pI,mI)
1584 val pits = init_pbl' ppc
1585 val pt = update_pbl pt [] pits
1586 in ((pt, ([] ,Pbl)), []) : calcstate end
1587 else if mI <> [] then (* from met-browser *)
1588 let val {ppc,...} = get_met mI
1589 val dI = if dI = "" then "Isac" else dI
1590 val thy = assoc_thy dI
1591 val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1592 ([], (dI,pI,mI), e_term(*FIXME met*))
1593 val pt = update_spec pt [] (dI,pI,mI)
1594 val mits = init_pbl' ppc
1595 val pt = update_met pt [] mits
1596 in ((pt, ([], Met)), []) : calcstate end
1597 else (* new example, pepare for interactive modeling *)
1598 let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec)
1599 ([], e_spec, e_term)
1600 in ((pt,([],Pbl)), []) : calcstate end
1601 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1602 let (* both """"""""""""""""""""""""" either empty or complete *)
1603 val thy = assoc_thy dI
1604 val (pI, pors, mI) =
1606 then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI)
1607 val pI' = refine_ori' pors pI;
1608 in (pI', pors(*refinement over models with diff.precond only*),
1609 (hd o #met o get_pbt) pI') end
1610 else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI)
1611 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1612 val dI = theory2theory' (maxthy thy thy');
1613 val hdl = case cas of
1614 NONE => pblterm dI pI
1615 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1616 ~~~ vals_of_oris pors) t
1617 val (pt, _) = cappend_problem e_ptree [] e_istate (fmz, (dI, pI, mI))
1618 (pors, (dI, pI, mI), hdl)
1619 in ((pt, ([], Pbl)),
1620 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1626 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1627 (* case appl_spec p pt m of /// 19.1.00
1628 Notappl e => Error' (Error_ e)
1630 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1634 (*fun tag_form thy (formal, given) = cterm_of thy
1635 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1636 fun tag_form thy (formal, given) =
1637 (let val gf = (head_of given) $ formal;
1638 val _ = cterm_of thy gf
1641 error ("calchead.tag_form: " ^
1642 Print_Mode.setmp [] (Syntax.string_of_term
1643 (thy2ctxt thy)) given ^ " .. " ^
1644 Print_Mode.setmp [] (Syntax.string_of_term
1645 (thy2ctxt thy)) formal ^
1646 " ..types do not match");
1647 (* val formal = (the o (parse thy)) "[R::real]";
1648 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1649 > tag_form thy (formal, given);
1650 val it = "fixed_values [R]" : cterm
1653 fun chktyp thy (n, fs, gs) =
1654 ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1656 (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1658 tag_form thy (nth n fs, nth n gs));
1659 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1661 (* #####################################################
1662 find the failing item:
1664 > val tag__form = chktyp (n,formals,givens);
1665 > (type_of o term_of o (nth n)) formals;
1666 > (type_of o term_of o (nth n)) givens;
1667 > atomty ((term_of o (nth n)) formals);
1668 > atomty ((term_of o (nth n)) givens);
1669 > atomty (term_of tag__form);
1670 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1671 ##################################################### *)
1673 (* #####################################################
1675 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1676 val formals = map (the o (parse thy)) origin;
1678 val given = ["equation (lhs=rhs)",
1679 "bound_variable bdv", (* TODO type *)
1681 val where_ = ["e is_root_equation_in bdv",
1683 "apx is_const_expr"];
1684 val find = ["L::rat set"];
1685 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1686 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1687 val givens = map (the o (parse thy)) given;
1689 val tag__forms = chktyps (formals, givens);
1690 map ((atomty) o term_of) tag__forms;
1691 ##################################################### *)
1694 (* check pbltypes, announces one failure a time *)
1695 (*fun chk_vars ctppc =
1696 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1697 appc flat (mappc (vars o term_of) ctppc)
1698 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1699 else if (re\\(gi union fi)) <> []
1700 then ("re\\(gi union fi)",re\\(gi union fi))
1701 else ("ok",[]) end;*)
1702 fun chk_vars ctppc =
1703 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1704 appc flat (mappc vars ctppc)
1705 val chked = subtract op = gi wh
1706 in if chked <> [] then ("wh\\gi", chked)
1707 else let val chked = subtract op = (union op = gi fi) re
1709 then ("re\\(gi union fi)", chked)
1714 (* check a new pbltype: variables (Free) unbound by given, find*)
1715 fun unbound_ppc ctppc =
1716 let val {Given=gi,Find=fi,Relate=re,...} =
1717 appc flat (mappc vars ctppc)
1718 in distinct (*re\\(gi union fi)*)
1719 (subtract op = (union op = gi fi) re) end;
1721 > val org = {Given=["[R=(R::real)]"],Where=[],
1722 Find=["[A::real]"],With=[],
1723 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1725 > val ctppc = mappc (the o (parse thy)) org;
1726 > unbound_ppc ctppc;
1727 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1731 (* f, a binary operator, is nested rightassociative *)
1734 fun fld f (x::[]) = x
1735 | fld f (x::x'::[]) = f (x',x)
1736 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1737 in ((fld f) o rev) xs end;
1739 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1740 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1741 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1742 > cterm_of thy conj;
1743 val it = "(a = b & c = d) & e = f" : cterm
1746 (* f, a binary operator, is nested leftassociative *)
1747 fun foldl1 f (x::[]) = x
1748 | foldl1 f (x::x'::[]) = f (x,x')
1749 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1751 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1752 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1753 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1754 > cterm_of thy conj;
1755 val it = "a = b & c = d & e = f & g = h" : cterm
1759 (* called only once, if a Subproblem has been located in the script*)
1760 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
1761 (* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
1765 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1766 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1767 (*all stored in tac_ itms ^^^^^^^^^^*)
1768 | nxt_model_pbl tac_ _ =
1769 error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1770 (* run subp_rooteq.sml ''
1771 until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
1772 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1773 (last_elem o drop_last) ets'';
1774 > val mst = (last_elem o drop_last) ets'';
1775 > nxt_model_pbl mst;
1776 val it = Refine_Tacitly ["univariate","equation"] : tac
1779 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1780 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1781 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1784 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1785 + met from fmz; assumes pos on PblObj, meth = [].*)
1786 fun complete_mod (pt, pos as (p, p_):pos') =
1787 (* val (pt, (p, _)) = (pt, p);
1788 val (pt, (p, _)) = (pt, pos);
1790 let val _= if p_ <> Pbl
1791 then tracing("###complete_mod: only impl.for Pbl, called with "^
1792 pos'2str pos) else ()
1793 val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
1795 val (dI,pI,mI) = some_spec ospec spec
1796 val mpc = (#ppc o get_met) mI
1797 val ppc = (#ppc o get_pbt) pI
1798 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1799 val pt = update_pblppc pt p pits
1800 val pt = update_metppc pt p mits
1801 in (pt, (p,Met):pos') end
1803 (*| complete_mod (pt, pos as (p, Met):pos') =
1804 error ("###complete_mod: only impl.for Pbl, called with "^
1807 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1808 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1809 fun all_modspec (pt, (p,_):pos') =
1810 (* val (pt, (p,_)) = ptp;
1812 let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1813 ...}) = get_obj I pt p;
1814 val thy = assoc_thy dI;
1815 val {ppc,...} = get_met mI;
1816 val mors = prep_ori fmz_ thy ppc;
1817 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1818 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1819 val pt = update_spec pt p (dI,pI,mI);
1820 in (pt, (p,Met): pos') end;
1822 (*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1823 fun is_complete_mod_ ([]: itm list) = false
1824 | is_complete_mod_ itms =
1825 foldl and_ (true, (map #3 itms));
1826 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1827 if (is_pblobj o (get_obj I pt)) p
1828 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1829 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1830 | is_complete_mod (pt, pos as (p, Met)) =
1831 if (is_pblobj o (get_obj I pt)) p
1832 then (is_complete_mod_ o (get_obj g_met pt)) p
1833 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1834 | is_complete_mod (_, pos) =
1835 error ("is_complete_mod called by "^pos'2str pos^
1836 " (should be Pbl or Met)");
1838 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1839 fun is_complete_spec (pt, pos as (p,_): pos') =
1840 if (not o is_pblobj o (get_obj I pt)) p
1841 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1842 else let val (dI,pI,mI) = get_obj g_spec pt p
1843 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1844 (*.complete empty items in specification from origin (pbl, met ev.refined);
1845 assumes 'is_complete_mod'.*)
1846 fun complete_spec (pt, pos as (p,_): pos') =
1847 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1848 val pt = update_spec pt p (some_spec ospec spec)
1851 fun is_complete_modspec ptp =
1852 is_complete_mod ptp andalso is_complete_spec ptp;
1857 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1858 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1860 let val (_,_,metID) = get_somespec' spec spec'
1862 if metID = e_metID then []
1863 else let val {prls,pre=where_,...} = get_met metID
1864 val pre = check_preconds' prls where_ meth 0
1866 val allcorrect = is_complete_mod_ meth
1867 andalso foldl and_ (true, (map #1 pre))
1868 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1869 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1870 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1872 let val (_,pI,_) = get_somespec' spec spec'
1874 if pI = e_pblID then []
1875 else let val {prls,where_,cas,...} = get_pbt pI
1876 val pre = check_preconds' prls where_ probl 0
1878 val allcorrect = is_complete_mod_ probl
1879 andalso foldl and_ (true, (map #1 pre))
1880 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1883 fun pt_form (PrfObj {form,...}) = Form form
1884 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1885 let val (dI, pI, _) = get_somespec' spec spec'
1886 val {cas,...} = get_pbt pI
1888 NONE => Form (pblterm dI pI)
1889 | SOME t => Form (subst_atomic (mk_env probl) t)
1891 (*vvv takes the tac _generating_ the formula=result, asm ok....
1892 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1894 if null asm then NONE else SOME asm,
1896 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1897 let val (_,_,metID) = some_spec ospec spec
1899 if null asm then NONE else SOME asm,
1900 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1901 -------------------------------------------------------------------------*)
1904 (*.pt_extract returns
1905 # the formula at pos
1906 # the tactic applied to this formula
1907 # the list of assumptions generated at this formula
1908 (by application of another tac to the preceding formula !)
1909 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1910 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1911 fun pt_extract (pt,([],Res)) =
1912 (* val (pt,([],Res)) = ptp;
1914 let val (f, asm) = get_obj g_result pt []
1915 in (Form f, NONE, asm) end
1918 | pt_extract (pt,(p,Res)) =
1919 (* val (pt,(p,Res)) = ptp;
1921 let val (f, asm) = get_obj g_result pt p
1922 val tac = if last_onlev pt p
1923 then if is_pblobj' pt (lev_up p)
1924 then let val (PblObj{spec=(_,pI,_),...}) =
1925 get_obj I pt (lev_up p)
1926 in if pI = e_pblID then NONE
1927 else SOME (Check_Postcond pI) end
1928 else SOME End_Trans (*WN0502 TODO for other branches*)
1929 else let val p' = lev_on p
1930 in if is_pblobj' pt p'
1931 then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1933 in SOME (Subproblem (dI, pI)) end
1934 else if f = get_obj g_form pt p'
1935 then SOME (get_obj g_tac pt p')
1936 (*because this Frm ~~~is not on worksheet*)
1937 else SOME (Take (term2str (get_obj g_form pt p')))
1939 in (Form f, tac, asm) end
1941 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1942 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1943 val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
1945 let val ppobj = get_obj I pt p
1946 val f = if is_pblobj ppobj then pt_model ppobj p_
1947 else get_obj pt_form pt p
1948 val tac = g_tac ppobj
1949 in (f, SOME tac, []) end;
1952 (**. get the formula from a ctree-node:
1953 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1954 take res from all other PrfObj's .**)
1955 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1956 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1957 [("headline", (p, Frm), h),
1958 ("stepform", (p, Res), r)]
1959 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1960 [("stepform", (p, Frm), form),
1961 ("stepform", (p, Res), r)];
1963 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1964 [("stepform", (p, Res), r)]
1966 (*assumes to take whole level, in particular hd -- for use in interSteps*)
1967 fun get_formress fs p [] = flat fs
1968 | get_formress fs p (nd::nds) =
1969 (* start with 'form+res' and continue with trying 'res' only*)
1970 get_forms (fs @ [formres p nd]) (lev_on p) nds
1971 and get_forms fs p [] = flat fs
1972 | get_forms fs p (nd::nds) =
1974 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1975 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1976 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1977 (* continue with trying 'res' only*)
1978 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1980 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1981 (*WN050219 made robust against _'to' below or after Complete nodes
1982 by handling exn caused by move_dn*)
1983 (*WN0401 this functionality belongs to ctree.sml,
1984 but fetching a calc_head requires calculations defined in modspec.sml
1985 transfer to ME/me.sml !!!
1986 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1987 is returned !!!!!!!!!!!!!
1989 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1990 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1991 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1995 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1999 | eq_pos' _ _ = false;
2001 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
2002 total ordering Position#compareTo(Position p) in the java-code
2003 val get_interval = fn
2004 : pos' -> : from is "move_up 1st-element" to return
2005 pos' -> : to the last element to be returned; from < to
2006 int -> : level: 0 gets the flattest sub-tree possible
2007 >999 gets the deepest sub-tree possible
2009 (pos' * : of the formula
2010 Term.term) : the formula
2013 fun get_interval from to level pt =
2014 (* val (from,level) = (f,lev);
2015 val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
2017 let fun get_inter c (from:pos') (to:pos') lev pt =
2018 (* val (c, from, to, lev) = ([], from, to, level);
2019 ------for recursion.......
2020 val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
2022 if eq_pos' from to orelse from = ([],Res)
2023 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
2024 if 'to' has values NOT generated by move_dn, see systest/me.sml
2025 TODO.WN0501: introduce an order on pos' and check "from > to"..
2026 ...there is an order in Java!
2027 WN051224 the hack got worse with returning term instead ptform*)
2028 then let val (f,_,_) = pt_extract (pt, from)
2030 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2031 | Form t => c @ [(from, t)]
2034 if lev < lev_of from
2035 then (get_inter c (move_dn [] pt from) to lev pt)
2036 handle (PTREE _(*from move_dn too far*)) => c
2037 else let val (f,_,_) = pt_extract (pt, from)
2038 val term = case f of
2039 ModSpec (_,_,headline,_,_,_)=> headline
2041 in (get_inter (c @ [(from, term)])
2042 (move_dn [] pt from) to lev pt)
2043 handle (PTREE _(*from move_dn too far*))
2044 => c @ [(from, term)] end
2045 in get_inter [] from to level pt end;
2048 fun posform2str (pos:pos', form) =
2049 "("^ pos'2str pos ^", "^
2051 Form f => term2str f
2052 | ModSpec c => term2str (#3 c(*the headline*)))
2054 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2055 (map posform2str)) pfs;
2056 fun posterm2str (pos:pos', t) =
2057 "("^ pos'2str pos ^", "^term2str t^")";
2058 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2059 (map posterm2str)) pfs;
2062 (*WN050225 omits the last step, if pt is incomplete*)
2064 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
2066 (*.get a calchead from a PblObj-node in the ctree;
2067 preconditions must be calculated.*)
2068 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
2069 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
2071 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2072 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
2073 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
2074 | get_ocalhd (pt, pos' as (p,Met):pos') =
2075 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2078 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2079 val pre = check_preconds (assoc_thy"Isac") prls pre meth
2080 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
2082 (*.at the activeFormula set the Model, the Guard and the Specification
2083 to empty and return a CalcHead;
2084 the 'origin' remains (for reconstructing all that).*)
2085 fun reset_calchead (pt, pos' as (p,_):pos') =
2086 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
2087 val pt = update_pbl pt p []
2088 val pt = update_met pt p []
2089 val pt = update_spec pt p e_spec
2090 in (pt, (p,Pbl):pos') end;
2092 (*---------------------------------------------------------------------*)
2096 (*---------------------------------------------------------------------*)