intermed. context integration appl_add does not work
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
146 Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
149 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
150 SpecifyTools.itm list ->
151 (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
152 val parse_ok : SpecifyTools.itm_ list -> bool
153 val posform2str : pos' * ptform -> string
154 val posforms2str : (pos' * ptform) list -> string
155 val posterms2str : (pos' * term) list -> string (*tests only*)
156 val ppc135list : 'a SpecifyTools.ppc -> 'a list
157 val ppc2list : 'a SpecifyTools.ppc -> 'a list
159 ptree * (int list * pos_) ->
160 ptform * tac option * Term.term list
161 val pt_form : ppobj -> ptform
162 val pt_model : ppobj -> pos_ -> ptform
163 val reset_calchead : ptree * pos' -> ptree * pos'
167 Term.term * Term.term list ->
168 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
169 -> string * SpecifyTools.ori * Term.term list
174 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
175 -> string * SpecifyTools.ori * Term.term list
177 int -> SpecifyTools.itm list -> SpecifyTools.itm option
178 val show_pt : ptree -> unit
179 val some_spec : spec -> spec -> spec
185 (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *
187 val specify_additem :
193 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
194 val tag_form : theory -> term * term -> term
195 val test_types : Proof.context -> Term.term * Term.term list -> string
196 val typeless : Term.term -> Term.term
197 val unbound_ppc : term SpecifyTools.ppc -> Term.term list
198 val vals_of_oris : SpecifyTools.ori list -> Term.term list
199 val variants_in : Term.term list -> int
200 val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
201 val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
208 (*---------------------------------------------------------------------
209 structure CalcHead (**): CALC_HEAD(**) =
212 ---------------------------------------------------------------------*)
216 (*.the state wich is stored after each step of calculation; it contains
217 the calc-state and a list of [tac,istate](="tacis") to be applied next.
218 the last_elem tacis is the first to apply to the calc-state and
219 the (only) one shown to the front-end as the 'proposed tac'.
220 the calc-state resulting from the application of tacis is not stored,
221 because the tacis hold enough information for efficiently rebuilding
222 this state just by "fun generate ".*)
224 (ptree * pos') * (*the calc-state to which the tacis could be applied*)
225 (taci list); (*ev. several (hidden) steps;
226 in REVERSE order: first tac_ to apply is last_elem*)
227 val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
229 (*the state used during one calculation within the mathengine; it contains
230 a list of [tac,istate](="tacis") which generated the the calc-state;
231 while this state's tacis are extended by each (internal) step,
232 the calc-state is used for creating new nodes in the calc-tree
233 (eg. applicable_in requires several particular nodes of the calc-tree)
234 and then replaced by the the newly created;
235 on leave of the mathengine the resuing calc-state is dropped anyway,
236 because the tacis hold enought information for efficiently rebuilding
237 this state just by "fun generate ".*)
239 taci list * (*cas. several (hidden) steps;
240 in REVERSE order: first tac_ to apply is last_elem*)
241 pos' list * (*a "continuous" sequence of pos',
242 deleted by application of taci list*)
243 (ptree * pos'); (*the calc-state resulting from the application of tacis*)
244 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
246 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
247 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
248 | f_mout thy _ = error "f_mout: not called with formula";
251 (*.is the calchead complete ?.*)
252 fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
253 foldl and_ (true, map #3 its) andalso
254 foldl and_ (true, map #1 pre) andalso
255 dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
258 (* make a term 'typeless' for comparing with another 'typeless' term;
259 'type-less' usually is illtyped *)
260 fun typeless (Const(s,_)) = (Const(s,e_type))
261 | typeless (Free(s,_)) = (Free(s,e_type))
262 | typeless (Var(n,_)) = (Var(n,e_type))
263 | typeless (Bound i) = (Bound i)
264 | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
265 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
267 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
268 > val (_,t1) = split_dsc_t hs (term_of ct);
269 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
270 > val (_,t2) = split_dsc_t hs (term_of ct);
271 > typeless t1 = typeless t2;
277 (*.to an input (d,ts) find the according ori and insert the ts.*)
278 (*WN.11.03: + dont take first inter<>[]*)
279 fun seek_oridts ctxt sel (d,ts) [] =
280 ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
282 "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
284 | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
285 if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
287 (id,vat,sel,d, inter op = ts ts'):ori,
289 else seek_oridts ctxt sel (d,ts) oris;
291 (*.to an input (_,ts) find the according ori and insert the ts.*)
292 fun seek_orits ctxt sel ts [] =
293 ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
295 "') not found in oris (typed)", e_ori_, [])
296 | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
297 if sel = sel' andalso (inter op = ts ts') <> []
300 (id,vat,sel,d, inter op = ts ts'):ori,
302 else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
307 else seek_orits ctxt sel ts oris;
309 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
310 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
311 uncaught exception TYPE
312 > seek_orits thy sel ts [];
313 uncaught exception TYPE
316 (*find_first item with #1 equal to id*)
317 fun seek_ppc id [] = NONE
318 | seek_ppc id (p::(ppc:itm list)) =
319 if id = #1 p then SOME p else seek_ppc id ppc;
323 (*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
326 datatype appl = Appl of tac_ | Notappl of string;
328 fun ppc2list ({Given=gis,Where=whs,Find=fis,
329 With=wis,Relate=res}: 'a ppc) =
330 gis @ whs @ fis @ wis @ res;
331 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
337 (* get the number of variants in a problem in 'original',
338 assumes equal descriptions in immediate sequence *)
340 let fun eq(x,y) = head_of x = head_of y;
341 fun cnt eq [] y n = ([n],[])
342 | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
344 fun coll eq xs [] = xs
345 | coll eq xs (y::ys) =
346 let val (n,ys') = cnt eq (y::ys) y 0;
347 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
348 val vts = subtract op = [1] (distinct (coll eq [] ts));
349 in case vts of [] => 1 | [n] => n
350 | _ => error "different variants in formalization" end;
352 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
353 val it = ([3],[4,5,5,5,5,5]) : int list * int list
354 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
355 val it = [1,3,1,5] : int list
358 fun is_list_type (Type("List.list",_)) = true
359 | is_list_type _ = false;
360 (* fun destr (Type(str,sort)) = (str,sort);
361 > val (SOME ct) = parse thy "lll::real list";
362 > val ty = (#T o rep_cterm) ct;
366 val it = ("List.list",["RealDef.real"]) : string * typ list
367 > atomty ((#t o rep_cterm) ct);
369 *** Free ( lll, real list)
372 > val (SOME ct) = parse thy "[lll::real]";
373 > val ty = (#T o rep_cterm) ct;
377 val it = ("List.list",["'a"]) : string * typ list
378 > atomty ((#t o rep_cterm) ct);
380 *** Const ( List.list.Cons, [real, real list] => real list)
381 *** Free ( lll, real)
382 *** Const ( List.list.Nil, real list)
384 > val (SOME ct) = parse thy "lll";
385 > val ty = (#T o rep_cterm) ct;
387 val it = false : bool *)
390 fun has_list_type (Free(_,T)) = is_list_type T
391 | has_list_type _ = false;
393 > val (SOME ct) = parse thy "lll::real list";
394 > has_list_type (term_of ct);
396 > val (SOME ct) = parse thy "[lll::real]";
397 > has_list_type (term_of ct);
398 val it = false : bool *)
400 fun is_parsed (Syn _) = false
401 | is_parsed _ = true;
402 fun parse_ok its = foldl and_ (true, map is_parsed its);
404 fun all_dsc_in itm_s =
406 fun d_in (Cor ((d,_),_)) = [d]
409 | d_in (Inc ((d,_),_)) = [d]
410 | d_in (Sup (d,_)) = [d]
411 | d_in (Mis (d,_)) = [d];
412 in (flat o (map d_in)) itm_s end;
415 fun is_Syn (Syn _) = true
416 | is_Syn (Typ _) = true
419 fun is_error (Cor (_,ts)) = false
420 | is_error (Sup (_,ts)) = false
421 | is_error (Inc (_,ts)) = false
422 | is_error (Mis (_,ts)) = false
426 fun ct_in (Syn (c)) = c
427 | ct_in (Typ (c)) = c
428 | ct_in _ = error "ct_in called for Cor .. Sup";
431 (*#############################################################*)
432 (*#############################################################*)
433 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
436 (* testdaten besorgen:
437 use"test-coil-kernel.sml";
438 val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
443 variant V: oris union ppc => int, id ID: oris union ppc => int
446 EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
449 @vt = max sum(i : ppc) V i
455 > ((vts_cnt (vts_in itms))) itms;
460 > val vts = vts_in itms;
461 val vts = [1,2,3] : int list
462 > val nvts = vts_cnt vts itms;
463 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
464 > val mx = max2 nvts;
465 val mx = (3,7) : int * int
466 > val v = max_vt itms;
468 --------------------------
472 (*.get the first term in ts from ori.*)
473 (* val (_,_,fd,d,ts) = hd miss;
475 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
476 (fd, (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) o
477 comp_dts) (d,[hd ts]) : cterm');
478 (* val t = comp_dts (d,[hd ts]);
481 (* get a term from ori, notyet input in itm.
482 the term from ori is thrown back to a string in order to reuse
483 machinery for immediate input by the user. *)
484 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
485 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
486 (d, subtract op = (ts_in itm_) ts) : cterm');
487 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
488 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
489 (d, subtract op = (ts_in itm_) ts) : cterm');
491 (* in FE dsc, not dat: this is in itms ...*)
492 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
493 | is_untouched _ = false;
496 (* select an item in oris, notyet input in itms
497 (precondition: in itms are only Cor, Sup, Inc) *)
500 | x mem (y :: ys) = x = y orelse x mem ys;
502 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
504 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
505 fun is_elem itms (f,(d,t)) =
506 case find_first (test_d d) itms of
507 SOME _ => true | NONE => false;
508 in case filter_out (is_elem itms) pbt of
509 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
513 ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
514 comp_dts) (d, []) : cterm')
517 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
519 | nxt_add thy oris pbt itms =
521 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
522 andalso (#3 ori) <>"#undef";
523 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
524 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
525 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
526 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
527 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
528 | false_and_not_Sup (i,v,false,f, _) = true
529 | false_and_not_Sup _ = false;
531 val v = if itms = [] then 1 else max_vt itms;
532 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
533 val vits = if v = 0 then itms (*because of dsc without dat*)
534 else filter (testi_vt v) itms; (*itms..vat*)
535 val icl = filter false_and_not_Sup vits; (* incomplete *)
537 then case filter_out (test_id (map #1 vits)) vors of
539 (* val miss = filter_out (test_id (map #1 vits)) vors;
541 | miss => SOME (getr_ct thy (hd miss))
543 case find_first (test_subset (hd icl)) vors of
544 (* val SOME ori = find_first (test_subset (hd icl)) vors;
546 NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
547 | SOME ori => SOME (geti_ct thy ori (hd icl))
553 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
554 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
555 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
556 | mk_delete thy str _ =
557 error ("mk_delete: called with field '"^str^"'");
558 fun mk_additem "#Given" ct = Add_Given ct
559 | mk_additem "#Find" ct = Add_Find ct
560 | mk_additem "#Relate"ct = Add_Relation ct
562 error ("mk_additem: called with field '"^str^"'");
565 (* determine the next step of specification;
566 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
567 eg. in rootpbl 'no_met':
569 preok predicates are _all_ ok (and problem matches completely)
570 oris immediately from formalization
571 (dI',pI',mI') specification coming from author/parent-problem
572 (pbl, item lists specified by user
573 met) -"-, tacitly completed by copy_probl
574 (dI,pI,mI) specification explicitly done by the user
575 (pbt, mpc) problem type, guard of method
577 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
578 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
579 ((*tracing"### nxt_spec Pbl";*)
580 if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
581 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
582 else case find_first (is_error o #5) (pbl:itm list) of
583 SOME (_, _, _, fd, itm_) =>
585 (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
587 ((*tracing"### nxt_spec is_error NONE";*)
588 case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
590 SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
591 (Pbl, mk_additem fd ct'))
592 | NONE => (*pbl-items complete*)
593 if not preok then (Pbl, Refine_Problem pI')
595 if dI = e_domID then (Pbl, Specify_Theory dI')
596 else if pI = e_pblID then (Pbl, Specify_Problem pI')
597 else if mI = e_metID then (Pbl, Specify_Method mI')
599 case find_first (is_error o #5) met of
600 SOME (_,_,_,fd,itm_) =>
601 (Met, mk_delete (assoc_thy dI) fd itm_)
603 (case nxt_add (assoc_thy dI) oris mpc met of
604 SOME (fd,ct') => (*30.8.01: pre?!?*)
605 (Met, mk_additem fd ct')
607 ((*Solv 3.4.00*)Met, Apply_Method mI))))
609 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
610 ((*tracing"### nxt_spec Met"; *)
611 case find_first (is_error o #5) met of
612 SOME (_,_,_,fd,itm_) =>
613 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
615 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
616 SOME (fd,ct') => (Met, mk_additem fd ct')
618 ((*tracing"### nxt_spec Met: nxt_add NONE";*)
619 if dI = e_domID then (Met, Specify_Theory dI')
620 else if pI = e_pblID then (Met, Specify_Problem pI')
621 else if not preok then (Met, Specify_Method mI)
622 else (Met, Apply_Method mI)));
625 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
626 (2,[2],true,"#Find",Syn("empty"))];
629 fun is_field_correct sel d dscpbt =
630 case assoc (dscpbt, sel) of
632 | SOME ds => member op = ds d;
634 (*. update the itm_ already input, all..from ori .*)
635 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
637 fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
639 val ts' = union op = (ts_in itm_) ts;
640 val pval = pbl_ids' d ts'
641 (*WN.9.5.03: FIXXXME [#0, epsilon]
642 here would upd_penv be called for [#0, epsilon] etc. *)
643 val complete = if eq_set op = (ts', all) then true else false;
646 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
647 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
648 | (Syn c) => error ("ori_2itm wants to overwrite "^c)
649 | (Typ c) => error ("ori_2itm wants to overwrite "^c)
650 | (Inc _) => if complete
651 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
652 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
653 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
654 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
655 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
656 (* 28.1.00: not completely clear ---^^^ etc.*)
657 (* 4.9.01: Mis just copied---vvv *)
658 | (Mis _) => if complete
659 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
660 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
664 fun eq1 d (_,(d',_)) = (d = d');
665 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
668 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
669 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
670 pval: value for problem-environment _NOT_ checked for 'inter' --
671 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
672 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
673 (*. is_input ori itms <=>
674 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
675 (2) ori(ts) subset itm(ts) --- Err "already input"
676 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
677 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
678 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
680 fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
681 case find_first (eq1 d) pbt of
682 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
683 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
685 (case find_first (eq3 f d) itms of
686 SOME (_,_,_,_,itm_) =>
688 val ts' = inter op = (ts_in itm_) ts;
689 in if subset op = (ts, ts')
691 map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts') ^
692 " already input", e_itm) (*2*)
694 ori_2itm itm_ pid all (i,v,f,d,
695 subtract op = ts' ts)) (*3,4*)
697 | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[])))
698 pid all (i,v,f,d,ts)) (*1*)
700 | NONE => ("", ori_2itm (Sup (d,ts))
701 e_term all (i,v,f,d,ts));
703 fun test_types ctxt (d,ts) =
705 (*val s = !show_types; val _ = show_types:= true;*)
706 val opt = (try comp_dts) (d,ts);
707 val msg = case opt of
709 | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
711 ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
714 (*val _ = show_types:= s*)
719 fun maxl [] = error "maxl of []"
722 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
726 (*. is the input term t known in oris ?
727 give feedback on all(?) strange input;
728 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
729 (*WN.11.03: from lists*)
730 fun is_known ctxt sel ori t =
731 (* val (ori,t)=(oris,term_of ct);
734 val _ = tracing ("RM is_known: t=" ^ term2str t);
735 val ots = (distinct o flat o (map #5)) (ori:ori list);
736 val oids = ((map (fst o dest_Free)) o distinct o
737 flat o (map vars)) ots;
738 val (d,ts(*,pval*)) = split_dts t;
739 val ids = map (fst o dest_Free)
740 ((distinct o (flat o (map vars))) ts);
741 in if (subtract op = oids ids) <> []
742 then (("identifiers "^(strs2str' (subtract op = oids ids))^
743 " not in example"), e_ori_, [])
747 if not (subset op = (map typeless ts, map typeless ots))
750 (map (Print_Mode.setmp [] (Syntax.string_of_term
752 "' not in example (typeless)"), e_ori_, [])
753 else (case seek_orits ctxt sel ts ori of
754 ("", ori_ as (_,_,_,d,ts), all) =>
755 (case test_types ctxt (d,ts) of
756 "" => ("", ori_, all)
757 | msg => (msg, e_ori_, []))
758 | (msg,_,_) => (msg, e_ori_, []))
760 if member op = (map #4 ori) d
761 then seek_oridts ctxt sel (d,ts) ori
762 else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
763 " not in example", (0, [], sel, d, ts), [])
767 (*. for return-value of appl_add .*)
770 | Err of string; (*error-message*)
773 (** add an item to the model; check wrt. oris and pbt **)
774 (* in contrary to oris<>[] below, this part handles user-input
775 extremely acceptive, i.e. accept input instead error-msg *)
776 fun appl_add ctxt sel [] ppc pbt t =
778 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
779 in case parseNEW ctxt t of
780 NONE => Add (i, [], false, sel, Syn t)
782 let val (d, ts) = split_dts t';
783 in if d = e_term then
784 Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
785 (case find_first (eq1 d) pbt of
786 NONE => Add (i, [], true, sel, Sup (d,ts))
787 | SOME (f, (_, id)) =>
788 let fun eq2 d (i, _, _, _, itm_) =
789 d = (d_in itm_) andalso i <> 0;
790 in case find_first (eq2 d) ppc of
791 NONE => Add (i, [], true, f,
792 Cor ((d, ts), (id, pbl_ids' d ts))
794 | SOME (i', _, _, _, itm_) => if is_list_dsc d then
796 val in_itm = ts_in itm_;
797 val ts' = union op = ts in_itm;
798 val i'' = if in_itm = [] then i else i';
799 in Add (i'', [], true, f,
800 Cor ((d, ts'), (id, pbl_ids' d ts'))
803 Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
807 | appl_add ctxt sel oris ppc pbt str =
808 case parseNEW ctxt str of
809 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
810 | SOME t => case is_known ctxt sel oris t of
811 ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
813 | (msg, _) => Err msg)
814 | (msg, _, _) => Err msg;
816 > val (msg,itm) = is_notyet_input thy ppc all ori';
817 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
819 > val ts = ts_in itm_;
823 (** make oris from args of the stac SubProblem and from pbt **)
825 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
826 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
827 fun is_copy_named_idstr str =
828 case (rev o Symbol.explode) str of
829 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
830 "is_copy_named_idstr: " ^ str ^ " T"); true)
831 | _ => (tracing ((strs2str o (rev o Symbol.explode))
832 "is_copy_named_idstr: " ^ str ^ " F"); false);
833 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
835 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
836 fun is_copy_named_generating_idstr str =
837 if is_copy_named_idstr str
838 then case (rev o Symbol.explode) str of
839 "'"::"'"::"'"::_ => false
842 fun is_copy_named_generating (_, (_, t)) =
843 (is_copy_named_generating_idstr o free2str) t;
845 (*.split type-wrapper from scr-arg and build part of an ori;
846 an type-error is reported immediately, raises an exn,
847 subsequent handling of exn provides 2nd part of error message.*)
848 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
849 (* val (thy, (str, (dsc, _)), (ty $ var)) =
852 (cterm_of thy (dsc $ var);(*type check*)
853 SOME ((([1], str, dsc, (*[var]*)
854 split_dts' (dsc, var))): preori)(*:ori without leading #*))
855 handle e as TYPE _ =>
856 (tracing (dashs 70 ^ "\n"
857 ^"*** ERROR while creating the items for the model of the ->problem\n"
858 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
859 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
860 ^"*** description: "^(term_detail2str dsc)
861 ^"*** value: "^(term_detail2str var)
862 ^"*** typeconstructor in script: "^(term_detail2str ty)
863 ^"*** checked by theory: "^(theory2str thy)^"\n"
865 (*OldGoals.print_exn e; raises exn again*)
866 writeln (PolyML.makestring e);
868 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
871 (*.match each pat of the model-pattern with an actual argument;
872 precondition: copy-named vars are filtered out.*)
873 fun matc thy ([]:pat list) _ (oris:preori list) = oris
874 | matc thy pbt [] _ =
876 error ("actual arg(s) missing for '"^pats2str pbt
877 ^"' i.e. should be 'copy-named' by '*_._'"))
878 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
879 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
880 (thy, pbt', ags, []);
882 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
883 (thy, pbt, ags, (oris @ [ori]));
885 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
886 else(*..del?*) let val opt = mtc thy p a;
888 (* val SOME ori = mtc thy p a;
890 SOME ori => matc thy pbt ags (oris @ [ori])
891 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
893 (* run subp-rooteq.sml until Init_Proof before ...
894 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
895 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
897 other vars as in mtc ..
898 > matc thy (drop_last pbt) ags [];
899 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
902 (* generate a new variable "x_i" name from a related given one "x"
903 by use of oris relating "v_i_" (is_copy_named!) to "v_"
904 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
906 (* generate a new variable "x_i" name from a related given one "x"
907 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
908 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
909 but leave is_copy_named_generating as is, e.t. ss''' *)
910 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
911 (if is_copy_named_generating p
912 then (*WN051014 kept strange old code ...*)
913 let fun sel (_,_,d,ts) = comp_ts (d, ts)
914 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
915 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
916 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
917 val vals = map sel oris
918 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
919 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
920 else ([1], field, dsc, [t])
922 handle _ => error ("cpy_nam: for "^(term2str t));
924 (*.match the actual arguments of a SubProblem with a model-pattern
925 and create an ori list (in root-pbl created from formalization).
926 expects ags:pats = 1:1, while copy-named are filtered out of pats;
927 if no 1:1 the exn raised by matc/mtc and handled at call.
928 copy-named pats are appended in order to get them into the model-items.*)
929 fun match_ags thy (pbt:pat list) ags =
930 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
931 val pbt' = filter_out is_copy_named pbt;
932 val cy = filter is_copy_named pbt;
933 val oris' = matc thy pbt' ags [];
934 val cy' = map (cpy_nam pbt' oris') cy;
935 val ors = add_id (oris' @ cy');
936 (*appended in order to get ^^^^^ into the model-items*)
937 in (map flattup ors):ori list end;
939 (*.report part of the error-msg which is not available in match_args.*)
940 fun match_ags_msg pI stac ags =
941 let (*val s = !show_types
942 val _ = show_types:= true*)
943 val pats = (#ppc o get_pbt) pI
944 val msg = (dots 70^"\n"
945 ^"*** problem "^strs2str pI^" has the ...\n"
946 ^"*** model-pattern "^pats2str pats^"\n"
947 ^"*** stac '"^term2str stac^"' has the ...\n"
948 ^"*** arg-list "^terms2str ags^"\n"
950 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
951 (*val _ = show_types:= s*)
955 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
956 fun vars_of_pbl_ pbl_ =
957 let fun var_of_pbl_ (gfr,(dsc,t)) = t
958 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
959 fun vars_of_pbl_' pbl_ =
960 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
961 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
963 fun overwrite_ppc thy itm ppc =
965 fun repl ppc' (_,_,_,_,itm_) [] =
966 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
968 | repl ppc' itm (p::ppc) =
969 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
970 else repl (ppc' @ [p]) itm ppc
971 in repl [] itm ppc end;
973 (*10.3.00: insert the already compiled itm into model;
974 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
977 fun insert_ppc thy itm ppc =
979 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
980 | eq_untouched _ _ = false;
983 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
984 case seek_ppc (#1 itm) ppc of
985 (* val SOME xxx = seek_ppc (#1 itm) ppc;
987 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
988 overwrite_ppc thy itm ppc
989 | NONE => (ppc @ [itm]));
990 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
992 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
993 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
995 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
996 (d_in itm_) = (d_in iitm_);
997 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
998 handles superfluous items carelessly*)
999 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
1001 > gen_ins' eee (4,[1,3,5,7]);
1002 val it = [1, 3, 5, 7, 4] : int list*)
1005 (*. output the headline to a ppc .*)
1006 fun header p_ pI mI =
1007 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1009 | pos => error ("header called with "^ pos_2str pos);
1012 fun specify_additem sel (ct,_) (p,Met) c pt =
1014 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1015 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1016 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1017 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1018 val cpI = if pI = e_pblID then pI' else pI;
1019 val cmI = if mI = e_metID then mI' else mI;
1020 val {ppc,pre,prls,...} = get_met cmI;
1021 in case appl_add (thy2ctxt thy) sel oris met ppc ct of
1022 Add itm (*..union old input *) =>
1023 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1025 val met' = insert_ppc thy itm met;
1026 (*val pt' = update_met pt p met';*)
1027 val ((p,Met),_,_,pt') =
1028 generate1 thy (case sel of
1029 "#Given" => Add_Given' (ct, met')
1030 | "#Find" => Add_Find' (ct, met')
1031 | "#Relate"=> Add_Relation'(ct, met'))
1032 (Uistate, e_ctxt) (p,Met) pt
1033 val pre' = check_preconds thy prls pre met'
1034 val pb = foldl and_ (true, map fst pre')
1035 (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
1037 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1038 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1039 in ((p,p_), ((p,p_),Uistate),
1040 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1041 (Method cmI, itms2itemppc thy met' pre'))),
1044 let val pre' = check_preconds thy prls pre met
1045 val pb = foldl and_ (true, map fst pre')
1046 (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
1048 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1049 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1050 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1054 | specify_additem sel (ct,_) (p,p_(*Frm, Pbl*)) c pt =
1056 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1057 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1058 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1059 val cpI = if pI = e_pblID then pI' else pI;
1060 val cmI = if mI = e_metID then mI' else mI;
1061 val {ppc,where_,prls,...} = get_pbt cpI;
1062 in case appl_add (thy2ctxt thy) sel oris pbl ppc ct of
1063 Add itm (*..union old input *) =>
1064 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1067 (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
1068 val pbl' = insert_ppc thy itm pbl
1069 val ((p,Pbl),_,_,pt') =
1070 generate1 thy (case sel of
1071 "#Given" => Add_Given' (ct, pbl')
1072 | "#Find" => Add_Find' (ct, pbl')
1073 | "#Relate"=> Add_Relation'(ct, pbl'))
1074 (Uistate, e_ctxt) (p,Pbl) pt
1075 val pre = check_preconds thy prls where_ pbl'
1076 val pb = foldl and_ (true, map fst pre)
1077 (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
1079 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1080 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1081 val ppc = if p_= Pbl then pbl' else met;
1082 in ((p,p_), ((p,p_),Uistate),
1083 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1085 itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1088 let val pre = check_preconds thy prls where_ pbl
1089 val pb = foldl and_ (true, map fst pre)
1090 (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
1092 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1093 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1094 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1096 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1097 val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1101 val (msg,itm) = appl_add thy sel oris ppc ct;
1102 val (Cor(d,ts)) = #5 itm;
1109 (* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1110 specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1112 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1113 let (* either """"""""""""""" all empty or complete *)
1114 val thy = assoc_thy dI';
1115 val (istate_, ctxt) = (#ppc o get_pbt) pI' |> prep_ori fmz thy;
1116 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1118 val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1119 (oris,(dI',pI',mI'),e_term);
1120 val {ppc,prls,where_,...} = get_pbt pI'
1121 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1122 val pt = update_pbl pt [] pbl;
1123 val pre = check_preconds thy prls where_ pbl
1124 val pb = foldl and_ (true, map fst pre)*)
1125 val (pbl, pre, pb) = ([], [], false)
1128 (([],Pbl), (([],Pbl),Uistate),
1129 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1130 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1131 Refine_Tacitly pI', Safe,pt)
1133 (([],Pbl), (([],Pbl),Uistate),
1134 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1135 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1139 (*ONLY for STARTING modeling phase*)
1140 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1141 let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
1143 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
1145 val thy' = if dI = e_domID then dI' else dI
1146 val thy = assoc_thy thy'
1147 val {ppc,prls,where_,...} = get_pbt pI'
1148 val pre = check_preconds thy prls where_ pbl
1149 val pb = foldl and_ (true, map fst pre)
1150 val ((p,_),_,_,pt) =
1151 generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
1152 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1153 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1154 in ((p,Pbl), ((p,p_),Uistate),
1155 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1156 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1159 (*. called only if no_met is specified .*)
1160 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1161 let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
1163 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
1165 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1166 (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
1167 (*val pt = update_pbl pt p pbl;
1168 val pt = update_orispec pt p
1169 (string_of_thy thy, pIre,
1170 if length met = 0 then e_metID else hd met);*)
1171 val (domID, metID) = (string_of_thy thy,
1172 if length met = 0 then e_metID else hd met)
1173 val ((p,_),_,_,pt) =
1174 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1175 (Uistate, e_ctxt) pos pt
1176 (*val pre = check_preconds thy prls where_ pbl
1177 val pb = foldl and_ (true, map fst pre)*)
1178 val (pbl, pre, pb) = ([], [], false)
1179 in ((p,Pbl), (pos,Uistate),
1180 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1181 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1182 Model_Problem, Safe, pt) end
1184 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1185 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
1186 (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1187 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1188 Model_Problem, Safe, pt) end
1190 (* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
1191 val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
1193 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1194 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1195 meth=met, ...}) = get_obj I pt p;
1196 (*val pt = update_pbl pt p itms;
1197 val pt = update_pblID pt p pI;*)
1198 val thy = assoc_thy dI
1199 val ((p,Pbl),_,_,pt)=
1200 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
1201 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1202 val mI'' = if mI=e_metID then mI' else mI;
1203 (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
1204 val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1205 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1206 in ((p,Pbl), (pos,Uistate),
1207 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1208 (Problem pI, itms2itemppc dI'' itms pre))),
1210 (* val Specify_Method' mID = nxt; val (p,_) = p;
1211 val Specify_Method' mID = m;
1212 specify (Specify_Method' mID) (p,p_) c pt;
1214 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1215 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1216 meth=met, ...}) = get_obj I pt p;
1217 val {ppc,pre,prls,...} = get_met mID
1218 val thy = assoc_thy dI
1219 val oris = add_field' thy ppc oris;
1220 (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1221 val dI'' = if dI=e_domID then dI' else dI;
1222 val pI'' = if pI = e_pblID then pI' else pI;
1223 val met = if met=[] then pbl else met;
1224 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1225 (*val pt = update_met pt p itms;
1226 val pt = update_metID pt p mID*)
1228 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1229 (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
1230 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1231 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1232 in (pos, (pos,Uistate),
1233 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1234 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1236 (* val Add_Find' ct = nxt; val sel = "#Find";
1238 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1239 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1240 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1241 (* val Specify_Theory' domID = m;
1242 val (Specify_Theory' domID, (p,p_)) = (m, pos);
1244 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1245 let val p_ = case p_ of Met => Met | _ => Pbl
1246 val thy = assoc_thy domID;
1247 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1248 probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
1249 val mppc = case p_ of Met => met | _ => pbl;
1250 val cpI = if pI = e_pblID then pI' else pI;
1251 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1252 val cmI = if mI = e_metID then mI' else mI;
1253 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1256 Met => (check_preconds thy mer mwh met)
1257 | _ => (check_preconds thy per pwh pbl)
1258 val pb = foldl and_ (true, map fst pre)
1261 (*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1262 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1263 (pbl,met) (ppc,mpc) (dI,pI,mI);
1264 in ((p,p_), (pos,Uistate),
1265 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1266 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1268 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1270 (*val pt = update_domID pt p domID;11.8.03*)
1271 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1272 (Uistate, e_ctxt) (p,p_) pt
1273 (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1274 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1275 (ppc,mpc) (domID,pI,mI);
1276 in ((p,p_), (pos,Uistate),
1277 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1278 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1281 (* itms2itemppc thy [](*mpc*) pre
1283 | specify m' _ _ _ =
1284 error ("specify: not impl. for "^tac_2str m');
1286 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1287 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1289 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1291 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1292 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1293 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1294 val cpI = if pI = e_pblID then pI' else pI;
1295 in case appl_add (thy2ctxt thy) sel oris pbl ((#ppc o get_pbt) cpI) ct of
1296 Add itm (*..union old input *) =>
1297 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1300 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1301 val pbl' = insert_ppc thy itm pbl
1304 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1305 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1306 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1307 val ((p,Pbl),c,_,pt') =
1308 generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
1309 in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate' end
1312 (*TODO.WN03 pass error-msgs to the frontend..
1313 FIXME ..and dont abuse a tactic for that purpose*)
1315 Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1316 (e_pos', (e_istate, e_ctxt)))], [], ptp)
1319 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1320 val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1322 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1324 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1325 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1326 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1327 val cmI = if mI = e_metID then mI' else mI;
1328 in case appl_add (thy2ctxt thy) sel oris met ((#ppc o get_met) cmI) ct of
1329 Add itm (*..union old input *) =>
1330 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1332 val met' = insert_ppc thy itm met;
1335 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1336 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1337 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1338 val ((p,Met),c,_,pt') =
1339 generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
1340 in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
1342 | Err msg => ([(*tacis*)], [], ptp)
1343 (*nxt_me collects tacis until not hide; here just no progress*)
1347 val (msg,itm) = appl_add thy sel oris ppc ct;
1348 val (Cor(d,ts)) = #5 itm;
1353 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1354 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1355 handle _ => error ("ori2Coritm: dsc "^
1357 "in ori, but not in pbt")
1359 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1360 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1361 (find_first (eq1 d))) pbt,ts))):itm)
1362 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1363 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1366 (*filter out oris which have same description in itms*)
1367 fun filter_outs oris [] = oris
1368 | filter_outs oris (i::itms) =
1369 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1370 (#4:ori -> term)) oris;
1371 in filter_outs ors itms end;
1373 fun memI a b = member op = a b;
1374 (*filter oris which are in pbt, too*)
1375 fun filter_pbt oris pbt =
1376 let val dscs = map (fst o snd) pbt
1377 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1379 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1380 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1382 fun x mem [] = false
1383 | x mem (y :: ys) = x = y orelse x mem ys;
1385 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1386 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1388 let val vat = max_vt pits;
1390 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1391 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1392 val os = filter_outs ors itms;
1393 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1394 in itms @ (map (ori2Coritm met) os) end
1399 (*.complete model and guard of a calc-head .*)
1401 fun x mem [] = false
1402 | x mem (y :: ys) = x = y orelse x mem ys;
1404 fun complete_mod_ (oris, mpc, ppc, probl) =
1405 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1406 val vat = if probl = [] then 1 else max_vt probl
1407 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1408 val pors = filter_outs pors pits (*which are in pbl already*)
1409 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1411 val pits = pits @ (map (ori2Coritm ppc) pors)
1412 val mits = complete_metitms oris pits [] mpc
1416 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1417 (if dI = e_domID then odI else dI,
1418 if pI = e_pblID then opI else pI,
1419 if mI = e_metID then omI else mI):spec;
1422 (*.find a next applicable tac (for calcstate) and update ptree
1423 (for ev. finding several more tacs due to hide).*)
1424 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1425 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1426 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1427 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1429 val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1430 val (dI, pI, mI) = some_spec ospec spec
1431 val thy = assoc_thy dI
1432 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1433 val {cas, ppc, ...} = get_pbt pI
1434 val pbl = init_pbl ppc (* fill in descriptions *)
1435 (*----------------if you think, this should be done by the Dialog
1436 in the java front-end, search there for WN060225-modelProblem----*)
1437 val (pbl, met) = case cas of NONE => (pbl, [])
1438 | _ => complete_mod_ (oris, mpc, ppc, probl)
1439 (*----------------------------------------------------------------*)
1440 val tac_ = Model_Problem' (pI, pbl, met)
1441 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
1442 in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1444 (* val Add_Find ct = tac;
1446 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1447 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1448 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1450 (*. called only if no_met is specified .*)
1451 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1452 let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1453 val opt = refine_ori oris pI
1456 let val {met,ppc,...} = get_pbt pI'
1457 val pbl = init_pbl ppc
1458 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1459 val mI = if length met = 0 then e_metID else hd met
1460 val thy = assoc_thy dI
1462 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1463 (Uistate, e_ctxt) pos pt
1464 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1465 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1466 | NONE => ([], [], ptp)
1469 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1470 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1471 probl, ...}) = get_obj I pt p
1472 val thy = if dI' = e_domID then dI else dI'
1473 in case refine_pbl (assoc_thy thy) pI probl of
1474 NONE => ([], [], ptp)
1475 | SOME (rfd as (pI',_)) =>
1476 let val (pos,c,_,pt) =
1477 generate1 (assoc_thy thy)
1478 (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1479 in ([(Refine_Problem pI, Refine_Problem' rfd,
1480 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1483 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1484 let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1485 probl, ...}) = get_obj I pt p;
1486 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1487 val {ppc,where_,prls,...} = get_pbt pI
1488 val pbl as (_,(itms,_)) =
1489 if pI'=e_pblID andalso pI=e_pblID
1490 then (false, (init_pbl ppc, []))
1491 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1492 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1493 val ((p,Pbl),c,_,pt)=
1494 generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
1495 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1496 (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1498 (*transfers oris (not required in pbl) to met-model for script-env
1499 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1500 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1501 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1502 meth=met, ...}) = get_obj I pt p;
1503 val {ppc,pre,prls,...} = get_met mID
1504 val thy = assoc_thy dI
1505 val oris = add_field' thy ppc oris;
1506 val dI'' = if dI=e_domID then dI' else dI;
1507 val pI'' = if pI = e_pblID then pI' else pI;
1508 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1509 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1511 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1512 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1513 (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1515 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1516 let val (dI',_,_) = get_obj g_spec pt p
1518 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1519 (Uistate, e_ctxt) pos pt
1520 in (*FIXXXME: check if pbl can still be parsed*)
1521 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1524 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1525 let val (dI',_,_) = get_obj g_spec pt p
1527 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1528 (Uistate, e_ctxt) pos pt
1529 in (*FIXXXME: check if met can still be parsed*)
1530 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1534 error ("nxt_specif: not impl. for "^tac2str m');
1536 (*.get the values from oris; handle the term list w.r.t. penv.*)
1539 fun x mem [] = false
1540 | x mem (y :: ys) = x = y orelse x mem ys;
1542 fun vals_of_oris oris =
1543 ((map (mkval' o (#5:ori -> term list))) o
1544 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1549 (* create a calc-tree with oris via an cas.refined pbl *)
1550 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1551 if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1552 let val {cas, met, ppc, thy, ...} = get_pbt pI
1553 val dI = if dI = "" then theory2theory' thy else dI
1554 val thy = assoc_thy dI
1555 val mI = if mI = [] then hd met else mI
1556 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1557 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1558 ([], (dI,pI,mI), hdl)
1559 val pt = update_spec pt [] (dI,pI,mI)
1560 val pits = init_pbl' ppc
1561 val pt = update_pbl pt [] pits
1562 in ((pt, ([] ,Pbl)), []) : calcstate end
1563 else if mI <> [] then (* from met-browser *)
1564 let val {ppc,...} = get_met mI
1565 val dI = if dI = "" then "Isac" else dI
1566 val thy = assoc_thy dI;
1567 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1568 ([], (dI,pI,mI), e_term(*FIXME met*));
1569 val pt = update_spec pt [] (dI,pI,mI);
1570 val mits = init_pbl' ppc;
1571 val pt = update_met pt [] mits;
1572 in ((pt, ([], Met)), []) : calcstate end
1573 else (* new example, pepare for interactive modeling *)
1574 let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1575 ([], e_spec, e_term)
1576 in ((pt,([],Pbl)), []) : calcstate end
1577 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1578 let (* both """"""""""""""""""""""""" either empty or complete *)
1579 val thy = assoc_thy dI
1580 val (pI, pors, mI) =
1582 then let val pors = get_pbt pI |> #ppc |> prep_ori fmz thy |> #1;
1583 val pI' = refine_ori' pors pI;
1584 in (pI', pors(*refinement over models with diff.precond only*),
1585 (hd o #met o get_pbt) pI') end
1586 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
1587 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1588 val dI = theory2theory' (maxthy thy thy');
1589 val ctxt = prep_ori fmz thy ppc |> #2;
1590 val hdl = case cas of
1591 NONE => pblterm dI pI
1592 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1593 ~~~ vals_of_oris pors) t;
1594 val (pt, _) = cappend_problem e_ptree [] (Uistate, ctxt) (fmz, (dI, pI, mI))
1595 (pors, (dI, pI, mI), hdl)
1596 in ((pt, ([], Pbl)),
1597 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1603 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1604 (* case appl_spec p pt m of /// 19.1.00
1605 Notappl e => Error' (Error_ e)
1607 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1611 (*fun tag_form thy (formal, given) = cterm_of thy
1612 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1613 fun tag_form thy (formal, given) =
1614 (let val gf = (head_of given) $ formal;
1615 val _ = cterm_of thy gf
1618 error ("calchead.tag_form: " ^
1619 Print_Mode.setmp [] (Syntax.string_of_term
1620 (thy2ctxt thy)) given ^ " .. " ^
1621 Print_Mode.setmp [] (Syntax.string_of_term
1622 (thy2ctxt thy)) formal ^
1623 " ..types do not match");
1624 (* val formal = (the o (parse thy)) "[R::real]";
1625 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1626 > tag_form thy (formal, given);
1627 val it = "fixed_values [R]" : cterm
1630 fun chktyp thy (n, fs, gs) =
1631 ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1633 (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1635 tag_form thy (nth n fs, nth n gs));
1636 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1638 (* #####################################################
1639 find the failing item:
1641 > val tag__form = chktyp (n,formals,givens);
1642 > (type_of o term_of o (nth n)) formals;
1643 > (type_of o term_of o (nth n)) givens;
1644 > atomty ((term_of o (nth n)) formals);
1645 > atomty ((term_of o (nth n)) givens);
1646 > atomty (term_of tag__form);
1647 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1648 ##################################################### *)
1650 (* #####################################################
1652 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1653 val formals = map (the o (parse thy)) origin;
1655 val given = ["equation (lhs=rhs)",
1656 "bound_variable bdv", (* TODO type *)
1658 val where_ = ["e is_root_equation_in bdv",
1660 "apx is_const_expr"];
1661 val find = ["L::rat set"];
1662 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1663 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1664 val givens = map (the o (parse thy)) given;
1666 val tag__forms = chktyps (formals, givens);
1667 map ((atomty) o term_of) tag__forms;
1668 ##################################################### *)
1671 (* check pbltypes, announces one failure a time *)
1672 (*fun chk_vars ctppc =
1673 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1674 appc flat (mappc (vars o term_of) ctppc)
1675 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1676 else if (re\\(gi union fi)) <> []
1677 then ("re\\(gi union fi)",re\\(gi union fi))
1678 else ("ok",[]) end;*)
1679 fun chk_vars ctppc =
1680 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1681 appc flat (mappc vars ctppc)
1682 val chked = subtract op = gi wh
1683 in if chked <> [] then ("wh\\gi", chked)
1684 else let val chked = subtract op = (union op = gi fi) re
1686 then ("re\\(gi union fi)", chked)
1691 (* check a new pbltype: variables (Free) unbound by given, find*)
1692 fun unbound_ppc ctppc =
1693 let val {Given=gi,Find=fi,Relate=re,...} =
1694 appc flat (mappc vars ctppc)
1695 in distinct (*re\\(gi union fi)*)
1696 (subtract op = (union op = gi fi) re) end;
1698 > val org = {Given=["[R=(R::real)]"],Where=[],
1699 Find=["[A::real]"],With=[],
1700 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1702 > val ctppc = mappc (the o (parse thy)) org;
1703 > unbound_ppc ctppc;
1704 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1708 (* f, a binary operator, is nested rightassociative *)
1711 fun fld f (x::[]) = x
1712 | fld f (x::x'::[]) = f (x',x)
1713 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1714 in ((fld f) o rev) xs end;
1716 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1717 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1718 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1719 > cterm_of thy conj;
1720 val it = "(a = b & c = d) & e = f" : cterm
1723 (* f, a binary operator, is nested leftassociative *)
1724 fun foldl1 f (x::[]) = x
1725 | foldl1 f (x::x'::[]) = f (x,x')
1726 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1728 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1729 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1730 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1731 > cterm_of thy conj;
1732 val it = "a = b & c = d & e = f & g = h" : cterm
1736 (* called only once, if a Subproblem has been located in the script*)
1737 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
1738 (* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
1742 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1743 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1744 (*all stored in tac_ itms ^^^^^^^^^^*)
1745 | nxt_model_pbl tac_ _ =
1746 error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1747 (* run subp_rooteq.sml ''
1748 until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
1749 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1750 (last_elem o drop_last) ets'';
1751 > val mst = (last_elem o drop_last) ets'';
1752 > nxt_model_pbl mst;
1753 val it = Refine_Tacitly ["univariate","equation"] : tac
1756 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1757 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1758 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1761 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1762 + met from fmz; assumes pos on PblObj, meth = [].*)
1763 fun complete_mod (pt, pos as (p, p_):pos') =
1764 (* val (pt, (p, _)) = (pt, p);
1765 val (pt, (p, _)) = (pt, pos);
1767 let val _= if p_ <> Pbl
1768 then tracing("###complete_mod: only impl.for Pbl, called with "^
1769 pos'2str pos) else ()
1770 val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
1772 val (dI,pI,mI) = some_spec ospec spec
1773 val mpc = (#ppc o get_met) mI
1774 val ppc = (#ppc o get_pbt) pI
1775 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1776 val pt = update_pblppc pt p pits
1777 val pt = update_metppc pt p mits
1778 in (pt, (p,Met):pos') end
1780 (*| complete_mod (pt, pos as (p, Met):pos') =
1781 error ("###complete_mod: only impl.for Pbl, called with "^
1784 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1785 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1786 fun all_modspec (pt, (p,_):pos') =
1787 (* val (pt, (p,_)) = ptp;
1789 let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1790 ...}) = get_obj I pt p;
1791 val thy = assoc_thy dI;
1792 val {ppc,...} = get_met mI;
1793 val mors = prep_ori fmz_ thy ppc |> #1;
1794 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1795 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1796 val pt = update_spec pt p (dI,pI,mI);
1797 in (pt, (p,Met): pos') end;
1799 (*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1800 fun is_complete_mod_ ([]: itm list) = false
1801 | is_complete_mod_ itms =
1802 foldl and_ (true, (map #3 itms));
1803 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1804 if (is_pblobj o (get_obj I pt)) p
1805 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1806 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1807 | is_complete_mod (pt, pos as (p, Met)) =
1808 if (is_pblobj o (get_obj I pt)) p
1809 then (is_complete_mod_ o (get_obj g_met pt)) p
1810 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1811 | is_complete_mod (_, pos) =
1812 error ("is_complete_mod called by "^pos'2str pos^
1813 " (should be Pbl or Met)");
1815 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1816 fun is_complete_spec (pt, pos as (p,_): pos') =
1817 if (not o is_pblobj o (get_obj I pt)) p
1818 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1819 else let val (dI,pI,mI) = get_obj g_spec pt p
1820 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1821 (*.complete empty items in specification from origin (pbl, met ev.refined);
1822 assumes 'is_complete_mod'.*)
1823 fun complete_spec (pt, pos as (p,_): pos') =
1824 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1825 val pt = update_spec pt p (some_spec ospec spec)
1828 fun is_complete_modspec ptp =
1829 is_complete_mod ptp andalso is_complete_spec ptp;
1834 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1835 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1837 let val (_,_,metID) = get_somespec' spec spec'
1839 if metID = e_metID then []
1840 else let val {prls,pre=where_,...} = get_met metID
1841 val pre = check_preconds' prls where_ meth 0
1843 val allcorrect = is_complete_mod_ meth
1844 andalso foldl and_ (true, (map #1 pre))
1845 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1846 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1847 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1849 let val (_,pI,_) = get_somespec' spec spec'
1851 if pI = e_pblID then []
1852 else let val {prls,where_,cas,...} = get_pbt pI
1853 val pre = check_preconds' prls where_ probl 0
1855 val allcorrect = is_complete_mod_ probl
1856 andalso foldl and_ (true, (map #1 pre))
1857 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1860 fun pt_form (PrfObj {form,...}) = Form form
1861 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1862 let val (dI, pI, _) = get_somespec' spec spec'
1863 val {cas,...} = get_pbt pI
1865 NONE => Form (pblterm dI pI)
1866 | SOME t => Form (subst_atomic (mk_env probl) t)
1868 (*vvv takes the tac _generating_ the formula=result, asm ok....
1869 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1871 if null asm then NONE else SOME asm,
1873 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1874 let val (_,_,metID) = some_spec ospec spec
1876 if null asm then NONE else SOME asm,
1877 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1878 -------------------------------------------------------------------------*)
1881 (*.pt_extract returns
1882 # the formula at pos
1883 # the tactic applied to this formula
1884 # the list of assumptions generated at this formula
1885 (by application of another tac to the preceding formula !)
1886 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1887 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1888 fun pt_extract (pt,([],Res)) =
1889 (* val (pt,([],Res)) = ptp;
1891 let val (f, asm) = get_obj g_result pt []
1892 in (Form f, NONE, asm) end
1895 | pt_extract (pt,(p,Res)) =
1896 (* val (pt,(p,Res)) = ptp;
1898 let val (f, asm) = get_obj g_result pt p
1899 val tac = if last_onlev pt p
1900 then if is_pblobj' pt (lev_up p)
1901 then let val (PblObj{spec=(_,pI,_),...}) =
1902 get_obj I pt (lev_up p)
1903 in if pI = e_pblID then NONE
1904 else SOME (Check_Postcond pI) end
1905 else SOME End_Trans (*WN0502 TODO for other branches*)
1906 else let val p' = lev_on p
1907 in if is_pblobj' pt p'
1908 then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1910 in SOME (Subproblem (dI, pI)) end
1911 else if f = get_obj g_form pt p'
1912 then SOME (get_obj g_tac pt p')
1913 (*because this Frm ~~~is not on worksheet*)
1914 else SOME (Take (term2str (get_obj g_form pt p')))
1916 in (Form f, tac, asm) end
1918 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1919 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1920 val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
1922 let val ppobj = get_obj I pt p
1923 val f = if is_pblobj ppobj then pt_model ppobj p_
1924 else get_obj pt_form pt p
1925 val tac = g_tac ppobj
1926 in (f, SOME tac, []) end;
1929 (**. get the formula from a ctree-node:
1930 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1931 take res from all other PrfObj's .**)
1932 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1933 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1934 [("headline", (p, Frm), h),
1935 ("stepform", (p, Res), r)]
1936 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1937 [("stepform", (p, Frm), form),
1938 ("stepform", (p, Res), r)];
1940 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1941 [("stepform", (p, Res), r)]
1943 (*assumes to take whole level, in particular hd -- for use in interSteps*)
1944 fun get_formress fs p [] = flat fs
1945 | get_formress fs p (nd::nds) =
1946 (* start with 'form+res' and continue with trying 'res' only*)
1947 get_forms (fs @ [formres p nd]) (lev_on p) nds
1948 and get_forms fs p [] = flat fs
1949 | get_forms fs p (nd::nds) =
1951 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1952 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1953 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1954 (* continue with trying 'res' only*)
1955 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1957 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1958 (*WN050219 made robust against _'to' below or after Complete nodes
1959 by handling exn caused by move_dn*)
1960 (*WN0401 this functionality belongs to ctree.sml,
1961 but fetching a calc_head requires calculations defined in modspec.sml
1962 transfer to ME/me.sml !!!
1963 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1964 is returned !!!!!!!!!!!!!
1966 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1967 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1968 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1972 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1976 | eq_pos' _ _ = false;
1978 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
1979 total ordering Position#compareTo(Position p) in the java-code
1980 val get_interval = fn
1981 : pos' -> : from is "move_up 1st-element" to return
1982 pos' -> : to the last element to be returned; from < to
1983 int -> : level: 0 gets the flattest sub-tree possible
1984 >999 gets the deepest sub-tree possible
1986 (pos' * : of the formula
1987 Term.term) : the formula
1990 fun get_interval from to level pt =
1991 (* val (from,level) = (f,lev);
1992 val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
1994 let fun get_inter c (from:pos') (to:pos') lev pt =
1995 (* val (c, from, to, lev) = ([], from, to, level);
1996 ------for recursion.......
1997 val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
1999 if eq_pos' from to orelse from = ([],Res)
2000 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
2001 if 'to' has values NOT generated by move_dn, see systest/me.sml
2002 TODO.WN0501: introduce an order on pos' and check "from > to"..
2003 ...there is an order in Java!
2004 WN051224 the hack got worse with returning term instead ptform*)
2005 then let val (f,_,_) = pt_extract (pt, from)
2007 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2008 | Form t => c @ [(from, t)]
2011 if lev < lev_of from
2012 then (get_inter c (move_dn [] pt from) to lev pt)
2013 handle (PTREE _(*from move_dn too far*)) => c
2014 else let val (f,_,_) = pt_extract (pt, from)
2015 val term = case f of
2016 ModSpec (_,_,headline,_,_,_)=> headline
2018 in (get_inter (c @ [(from, term)])
2019 (move_dn [] pt from) to lev pt)
2020 handle (PTREE _(*from move_dn too far*))
2021 => c @ [(from, term)] end
2022 in get_inter [] from to level pt end;
2025 fun posform2str (pos:pos', form) =
2026 "("^ pos'2str pos ^", "^
2028 Form f => term2str f
2029 | ModSpec c => term2str (#3 c(*the headline*)))
2031 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2032 (map posform2str)) pfs;
2033 fun posterm2str (pos:pos', t) =
2034 "("^ pos'2str pos ^", "^term2str t^")";
2035 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2036 (map posterm2str)) pfs;
2039 (*WN050225 omits the last step, if pt is incomplete*)
2041 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
2043 (*.get a calchead from a PblObj-node in the ctree;
2044 preconditions must be calculated.*)
2045 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
2046 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
2048 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2049 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
2050 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
2051 | get_ocalhd (pt, pos' as (p,Met):pos') =
2052 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2055 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2056 val pre = check_preconds (assoc_thy"Isac") prls pre meth
2057 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
2059 (*.at the activeFormula set the Model, the Guard and the Specification
2060 to empty and return a CalcHead;
2061 the 'origin' remains (for reconstructing all that).*)
2062 fun reset_calchead (pt, pos' as (p,_):pos') =
2063 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
2064 val pt = update_pbl pt p []
2065 val pt = update_met pt p []
2066 val pt = update_spec pt p e_spec
2067 in (pt, (p,Pbl):pos') end;
2069 (*---------------------------------------------------------------------
2073 ---------------------------------------------------------------------*)