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.
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 enought 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 ("'"^(Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))^
282 "' not found (typed)", (0,[],sel,d,ts):ori, [])
283 (* val (id,vat,sel',d',ts')::oris = ori;
284 val (id,vat,sel',d',ts') = ori;
286 | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
287 if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
290 (id,vat,sel,d, inter op = ts ts'):ori,
292 else ((Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))
296 else seek_oridts thy sel (d,ts) oris;
298 (*.to an input (_,ts) find the according ori and insert the ts.*)
299 fun seek_orits thy sel ts [] =
301 (strs2str (map (Syntax.string_of_term (thy2ctxt thy)) ts))^
302 "' not found (typed)", e_ori_, [])
303 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
304 if sel = sel' andalso (inter op = ts ts') <> []
307 (id,vat,sel,d, inter op = ts ts'):ori,
309 else (((strs2str' o map (Syntax.string_of_term (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, ((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, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy))
492 (d, subtract op = (ts_in itm_) ts) : cterm');
493 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
494 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
496 (d, subtract op = (ts_in itm_) ts) : cterm');
498 (* in FE dsc, not dat: this is in itms ...*)
499 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
500 | is_untouched _ = false;
503 (* select an item in oris, notyet input in itms
504 (precondition: in itms are only Cor, Sup, Inc) *)
507 | x mem (y :: ys) = x = y orelse x mem ys;
509 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
511 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
512 fun is_elem itms (f,(d,t)) =
513 case find_first (test_d d) itms of
514 SOME _ => true | NONE => false;
515 in case filter_out (is_elem itms) pbt of
516 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
519 SOME (f:string, ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts thy) (d,[]):cterm')
522 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
524 | nxt_add thy oris pbt itms =
526 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
527 andalso (#3 ori) <>"#undef";
528 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
529 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
530 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
531 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
532 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
533 | false_and_not_Sup (i,v,false,f, _) = true
534 | false_and_not_Sup _ = false;
536 val v = if itms = [] then 1 else max_vt itms;
537 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
538 val vits = if v = 0 then itms (*because of dsc without dat*)
539 else filter (testi_vt v) itms; (*itms..vat*)
540 val icl = filter false_and_not_Sup vits; (* incomplete *)
542 then case filter_out (test_id (map #1 vits)) vors of
544 (* val miss = filter_out (test_id (map #1 vits)) vors;
546 | miss => SOME (getr_ct thy (hd miss))
548 case find_first (test_subset (hd icl)) vors of
549 (* val SOME ori = find_first (test_subset (hd icl)) vors;
551 NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
552 | SOME ori => SOME (geti_ct thy ori (hd icl))
558 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
559 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
560 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
561 | mk_delete thy str _ =
562 error ("mk_delete: called with field '"^str^"'");
563 fun mk_additem "#Given" ct = Add_Given ct
564 | mk_additem "#Find" ct = Add_Find ct
565 | mk_additem "#Relate"ct = Add_Relation ct
567 error ("mk_additem: called with field '"^str^"'");
570 (* determine the next step of specification;
571 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
572 eg. in rootpbl 'no_met':
574 preok predicates are _all_ ok (and problem matches completely)
575 oris immediately from formalization
576 (dI',pI',mI') specification coming from author/parent-problem
577 (pbl, item lists specified by user
578 met) -"-, tacitly completed by copy_probl
579 (dI,pI,mI) specification explicitly done by the user
580 (pbt, mpc) problem type, guard of method
582 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
583 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
584 ((*tracing"### nxt_spec Pbl";*)
585 if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
586 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
587 else case find_first (is_error o #5) (pbl:itm list) of
588 SOME (_, _, _, fd, itm_) =>
590 (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
592 ((*tracing"### nxt_spec is_error NONE";*)
593 case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
595 SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
596 (Pbl, mk_additem fd ct'))
597 | NONE => (*pbl-items complete*)
598 if not preok then (Pbl, Refine_Problem pI')
600 if dI = e_domID then (Pbl, Specify_Theory dI')
601 else if pI = e_pblID then (Pbl, Specify_Problem pI')
602 else if mI = e_metID then (Pbl, Specify_Method mI')
604 case find_first (is_error o #5) met of
605 SOME (_,_,_,fd,itm_) =>
606 (Met, mk_delete (assoc_thy dI) fd itm_)
608 (case nxt_add (assoc_thy dI) oris mpc met of
609 SOME (fd,ct') => (*30.8.01: pre?!?*)
610 (Met, mk_additem fd ct')
612 ((*Solv 3.4.00*)Met, Apply_Method mI))))
614 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
615 ((*tracing"### nxt_spec Met"; *)
616 case find_first (is_error o #5) met of
617 SOME (_,_,_,fd,itm_) =>
618 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
620 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
621 SOME (fd,ct') => (Met, mk_additem fd ct')
623 ((*tracing"### nxt_spec Met: nxt_add NONE";*)
624 if dI = e_domID then (Met, Specify_Theory dI')
625 else if pI = e_pblID then (Met, Specify_Problem pI')
626 else if not preok then (Met, Specify_Method mI)
627 else (Met, Apply_Method mI)));
630 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
631 (2,[2],true,"#Find",Syn("empty"))];
635 (* ^^^--- aus nnewcode.sml am 30.1.00 ---^^^ *)
636 (*#############################################################*)
637 (*#############################################################*)
638 (* vvv--- aus nnewcode.sml vor 29.1.00 ---vvv *)
641 fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) =
642 (id,vt,cl,sl,Cor (d,ts)):itm
643 | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =
644 error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
645 " not not for Syn (s:cterm')")
646 | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) =
647 error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
648 " not not for Typ (s:cterm')")
649 | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
650 (id,vt,cl,sl,Fal (d,ts))
651 | update_itm (cl,d,ts) (id,vt,_,sl,Inc (_,_)) =
652 (id,vt,cl,sl,Inc (d,ts))
653 | update_itm (cl,d,ts) (id,vt,_,sl,Sup (_,_)) =
654 (id,vt,cl,sl,Sup (d,ts));
660 fun is_field_correct sel d dscpbt =
661 case assoc (dscpbt, sel) of
663 | SOME ds => member op = ds d;
665 (*. update the itm_ already input, all..from ori .*)
666 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
668 fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) =
670 val ts' = union op = (ts_in itm_) ts;
671 val pval = pbl_ids' thy d ts'
672 (*WN.9.5.03: FIXXXME [#0, epsilon]
673 here would upd_penv be called for [#0, epsilon] etc. *)
674 val complete = if eq_set op = (ts', all) then true else false;
677 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
678 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
679 | (Syn c) => error ("ori_2itm wants to overwrite "^c)
680 | (Typ c) => error ("ori_2itm wants to overwrite "^c)
681 | (Inc _) => if complete
682 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
683 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
684 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
685 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
686 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
687 (* 28.1.00: not completely clear ---^^^ etc.*)
688 (* 4.9.01: Mis just copied---vvv *)
689 | (Mis _) => if complete
690 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
691 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
695 fun eq1 d (_,(d',_)) = (d = d');
696 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
699 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
700 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
701 pval: value for problem-environment _NOT_ checked for 'inter' --
702 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
703 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
704 (*. is_input ori itms <=>
705 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
706 (2) ori(ts) subset itm(ts) --- Err "already input"
707 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
708 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
709 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
711 fun is_notyet_input thy (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
712 case find_first (eq1 d) pbt of
713 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
714 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
716 (case find_first (eq3 f d) itms of
717 SOME (_,_,_,_,itm_) =>
719 val ts' = inter op = (ts_in itm_) ts;
720 in if subset op = (ts, ts')
722 map (Syntax.string_of_term (thy2ctxt thy))) ts')^
723 " already input", e_itm) (*2*)
725 ori_2itm thy itm_ pid all (i,v,f,d,
726 subtract op = ts' ts)) (*3,4*)
728 | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
729 pid all (i,v,f,d,ts)) (*1*)
731 | NONE => ("", ori_2itm thy (Sup (d,ts))
732 e_term all (i,v,f,d,ts));
734 fun test_types thy (d,ts) =
736 val s = !show_types; val _ = show_types:= true;
737 val opt = (try (comp_dts thy)) (d,ts);
738 val msg = case opt of
740 | NONE => ((Syntax.string_of_term (thy2ctxt thy) d)^" "^
741 ((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
743 val _ = show_types:= s
748 fun maxl [] = error "maxl of []"
751 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
755 (*. is the input term t known in oris ?
756 give feedback on all(?) strange input;
757 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
758 (*WN.11.03: from lists*)
759 fun is_known thy sel ori t =
760 (* val (ori,t)=(oris,term_of ct);
763 val ots = (distinct o flat o (map #5)) (ori:ori list);
764 val oids = ((map (fst o dest_Free)) o distinct o
765 flat o (map vars)) ots;
766 val (d,ts(*,pval*)) = split_dts thy t;
767 val ids = map (fst o dest_Free)
768 ((distinct o (flat o (map vars))) ts);
769 in if (subtract op = oids ids) <> []
770 then (("identifiers "^(strs2str' (subtract op = oids ids))^
771 " not in example"), e_ori_, [])
775 if not (subset op = (map typeless ts, map typeless ots))
777 ((strs2str' o (map (Syntax.string_of_term
778 (thy2ctxt thy)))) ts)^
779 "' not in example (typeless)"), e_ori_, [])
780 else (case seek_orits thy sel ts ori of
781 ("", ori_ as (_,_,_,d,ts), all) =>
782 (case test_types thy (d,ts) of
783 "" => ("", ori_, all)
784 | msg => (msg, e_ori_, []))
785 | (msg,_,_) => (msg, e_ori_, []))
787 if member op = (map #4 ori) d
788 then seek_oridts thy sel (d,ts) ori
789 else ((Syntax.string_of_term (thy2ctxt thy) d)^
790 (*" not in example", e_ori_, []) ///11.11.03*)
791 " not in example", (0,[],sel,d,ts), [])
795 (*. for return-value of appl_add .*)
798 | Err of string; (*error-message*)
801 (** add an item to the model; check wrt. oris and pbt **)
802 (* in contrary to oris<>[] below, this part handles user-input
803 extremely acceptive, i.e. accept input instead error-msg *)
804 fun appl_add thy sel ([]:ori list) ppc pbt ct' =
805 (* val (ppc,pbt,ct',env) = (pbl, (#ppc o get_pbt) cpI, ct, []:envv);
806 !!!! 28.8.01: env tested _minimally_ !!!
809 val i = 1 + (if ppc=[] then 0 else maxl (map #1 ppc));
810 in case parse thy ct' of (*should be done in applicable_in 4.00.FIXME*)
811 NONE => Add (i,[],false,sel,Syn ct')
812 (* val (SOME ct) = parse thy ct';
816 val (d,ts(*,pval*)) = split_dts thy (term_of ct);
818 then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*)))
821 (case find_first (eq1 d) pbt of
822 NONE => Add (i,[],true,sel,Sup ((d,ts)))
824 (* val SOME (f,(_,id)) = find_first (eq1 d) pbt;
827 fun eq2 d ((i,_,_,_,itm_):itm) =
828 (d = (d_in itm_)) andalso i<>0;
829 in case find_first (eq2 d) ppc of
830 NONE => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*)
832 | SOME (i',_,_,_,itm_) =>
833 (* val SOME (i',_,_,_,itm_) = find_first (eq2 d) ppc;
834 val NONE = find_first (eq2 d) ppc;
837 then let val ts = union op = ts (ts_in itm_)
838 in Add (if ts_in itm_ = [] then i else i',
839 [],true,f,Cor ((d, ts), (id, (*pval*)
842 else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*)
849 (*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*)
850 | appl_add thy sel oris ppc pbt (*only for upd_envv*) str =
851 case parse thy str of
852 NONE => Err ("syntax error in " ^ str)
853 | SOME t => case is_known thy sel oris (term_of t) of
855 (case is_notyet_input thy ppc all ori' pbt of
857 | (msg, _) => Err msg)
858 | (msg, _, _) => Err msg;
860 > val (msg,itm) = is_notyet_input thy ppc all ori';
861 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
863 > val ts = ts_in itm_;
867 (** make oris from args of the stac SubProblem and from pbt **)
869 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
870 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
871 fun is_copy_named_idstr str =
872 case (rev o explode) str of
873 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode))
874 "is_copy_named_idstr: " ^ str ^ " T"); true)
875 | _ => (tracing ((strs2str o (rev o explode))
876 "is_copy_named_idstr: " ^ str ^ " F"); false);
877 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
879 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
880 fun is_copy_named_generating_idstr str =
881 if is_copy_named_idstr str
882 then case (rev o explode) str of
883 "'"::"'"::"'"::_ => false
886 fun is_copy_named_generating (_, (_, t)) =
887 (is_copy_named_generating_idstr o free2str) t;
889 (*.split type-wrapper from scr-arg and build part of an ori;
890 an type-error is reported immediately, raises an exn,
891 subsequent handling of exn provides 2nd part of error message.*)
892 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
893 (* val (thy, (str, (dsc, _)), (ty $ var)) =
896 (cterm_of thy (dsc $ var);(*type check*)
897 SOME ((([1], str, dsc, (*[var]*)
898 split_dts' (dsc, var))): preori)(*:ori without leading #*))
899 handle e as TYPE _ =>
900 (tracing (dashs 70 ^ "\n"
901 ^"*** ERROR while creating the items for the model of the ->problem\n"
902 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
903 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
904 ^"*** description: "^(term_detail2str dsc)
905 ^"*** value: "^(term_detail2str var)
906 ^"*** typeconstructor in script: "^(term_detail2str ty)
907 ^"*** checked by theory: "^(theory2str thy)^"\n"
909 OldGoals.print_exn e; (*raises exn again*)
910 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
913 (*.match each pat of the model-pattern with an actual argument;
914 precondition: copy-named vars are filtered out.*)
915 fun matc thy ([]:pat list) _ (oris:preori list) = oris
916 | matc thy pbt [] _ =
918 error ("actual arg(s) missing for '"^pats2str pbt
919 ^"' i.e. should be 'copy-named' by '*_._'"))
920 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
921 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
922 (thy, pbt', ags, []);
924 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
925 (thy, pbt, ags, (oris @ [ori]));
927 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
928 else(*..del?*) let val opt = mtc thy p a;
930 (* val SOME ori = mtc thy p a;
932 SOME ori => matc thy pbt ags (oris @ [ori])
933 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
935 (* run subp-rooteq.sml until Init_Proof before ...
936 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
937 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
939 other vars as in mtc ..
940 > matc thy (drop_last pbt) ags [];
941 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
944 (* generate a new variable "x_i" name from a related given one "x"
945 by use of oris relating "v_i_" (is_copy_named!) to "v_"
946 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
948 (* generate a new variable "x_i" name from a related given one "x"
949 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
950 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
951 but leave is_copy_named_generating as is, e.t. ss''' *)
952 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
953 (if is_copy_named_generating p
954 then (*WN051014 kept strange old code ...*)
955 let fun sel (_,_,d,ts) = comp_ts (d, ts)
956 val cy' = (implode o (drop_last_n 3) o explode o free2str) t
957 val ext = (last_elem o drop_last o explode o free2str) t
958 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
959 val vals = map sel oris
960 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
961 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
962 else ([1], field, dsc, [t])
964 handle _ => error ("cpy_nam: for "^(term2str t));
966 (*.match the actual arguments of a SubProblem with a model-pattern
967 and create an ori list (in root-pbl created from formalization).
968 expects ags:pats = 1:1, while copy-named are filtered out of pats;
969 if no 1:1 the exn raised by matc/mtc and handled at call.
970 copy-named pats are appended in order to get them into the model-items.*)
971 fun match_ags thy (pbt:pat list) ags =
972 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
973 val pbt' = filter_out is_copy_named pbt;
974 val cy = filter is_copy_named pbt;
975 val oris' = matc thy pbt' ags [];
976 val cy' = map (cpy_nam pbt' oris') cy;
977 val ors = add_id (oris' @ cy');
978 (*appended in order to get ^^^^^ into the model-items*)
979 in (map flattup ors):ori list end;
981 (*.report part of the error-msg which is not available in match_args.*)
982 fun match_ags_msg pI stac ags =
983 let val s = !show_types
984 val _ = show_types:= true
985 val pats = (#ppc o get_pbt) pI
986 val msg = (dots 70^"\n"
987 ^"*** problem "^strs2str pI^" has the ...\n"
988 ^"*** model-pattern "^pats2str pats^"\n"
989 ^"*** stac '"^term2str stac^"' has the ...\n"
990 ^"*** arg-list "^terms2str ags^"\n"
992 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
993 val _ = show_types:= s
997 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
998 fun vars_of_pbl_ pbl_ =
999 let fun var_of_pbl_ (gfr,(dsc,t)) = t
1000 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
1001 fun vars_of_pbl_' pbl_ =
1002 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
1003 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
1005 fun overwrite_ppc thy itm ppc =
1007 fun repl ppc' (_,_,_,_,itm_) [] =
1008 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
1010 | repl ppc' itm (p::ppc) =
1011 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
1012 else repl (ppc' @ [p]) itm ppc
1013 in repl [] itm ppc end;
1015 (*10.3.00: insert the already compiled itm into model;
1016 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
1019 fun insert_ppc thy itm ppc =
1021 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
1022 | eq_untouched _ _ = false;
1025 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
1026 case seek_ppc (#1 itm) ppc of
1027 (* val SOME xxx = seek_ppc (#1 itm) ppc;
1029 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
1030 overwrite_ppc thy itm ppc
1031 | NONE => (ppc @ [itm]));
1032 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
1034 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
1035 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
1037 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
1038 (d_in itm_) = (d_in iitm_);
1039 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
1040 handles superfluous items carelessly*)
1041 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
1043 > gen_ins' eee (4,[1,3,5,7]);
1044 val it = [1, 3, 5, 7, 4] : int list*)
1047 (*. output the headline to a ppc .*)
1048 fun header p_ pI mI =
1049 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1051 | pos => error ("header called with "^ pos_2str pos);
1055 (* test-printouts ---
1056 val _=tracing("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts))));
1057 val _=tracing("### insert_ppc: pts= "^
1058 (strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) pts);
1061 val sel = "#Given"; val Add_Given' ct = m;
1063 val sel = "#Find"; val Add_Find' (ct,_) = m;
1065 val (_,_,f,nxt',_,pt')= specify_additem sel (ct,[]) (p,Pbl(*!!!!!!!*)) c pt;
1067 val sel = "#Given"; val Add_Given' (ct,_) = nxt; val (p,_) = p;
1069 fun specify_additem sel (ct,_) (p,Met) c pt =
1071 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1072 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1073 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1074 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1075 val cpI = if pI = e_pblID then pI' else pI;
1076 val cmI = if mI = e_metID then mI' else mI;
1077 val {ppc,pre,prls,...} = get_met cmI
1078 in case appl_add thy sel oris met ppc ct of
1079 Add itm (*..union old input *) =>
1080 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1082 val met' = insert_ppc thy itm met;
1083 (*val pt' = update_met pt p met';*)
1084 val ((p,Met),_,_,pt') =
1085 generate1 thy (case sel of
1086 "#Given" => Add_Given' (ct, met')
1087 | "#Find" => Add_Find' (ct, met')
1088 | "#Relate"=> Add_Relation'(ct, met'))
1090 val pre' = check_preconds thy prls pre met'
1091 val pb = foldl and_ (true, map fst pre')
1092 (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
1094 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1095 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1096 in ((p,p_), ((p,p_),Uistate),
1097 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1098 (Method cmI, itms2itemppc thy met' pre'))),
1101 let val pre' = check_preconds thy prls pre met
1102 val pb = foldl and_ (true, map fst pre')
1103 (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
1105 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1106 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1107 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1111 | specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1113 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1114 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1115 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1116 val cpI = if pI = e_pblID then pI' else pI;
1117 val cmI = if mI = e_metID then mI' else mI;
1118 val {ppc,where_,prls,...} = get_pbt cpI;
1119 in case appl_add thy sel oris pbl ppc ct of
1120 Add itm (*..union old input *) =>
1121 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1124 (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
1125 val pbl' = insert_ppc thy itm pbl
1126 val ((p,Pbl),_,_,pt') =
1127 generate1 thy (case sel of
1128 "#Given" => Add_Given' (ct, pbl')
1129 | "#Find" => Add_Find' (ct, pbl')
1130 | "#Relate"=> Add_Relation'(ct, pbl'))
1132 val pre = check_preconds thy prls where_ pbl'
1133 val pb = foldl and_ (true, map fst pre)
1134 (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
1136 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1137 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1138 val ppc = if p_= Pbl then pbl' else met;
1139 in ((p,p_), ((p,p_),Uistate),
1140 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1142 itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1145 let val pre = check_preconds thy prls where_ pbl
1146 val pb = foldl and_ (true, map fst pre)
1147 (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
1149 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1150 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1151 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1153 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1154 val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1158 val (msg,itm) = appl_add thy sel oris ppc ct;
1159 val (Cor(d,ts)) = #5 itm;
1166 (* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1167 specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1169 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1170 let (* either """"""""""""""" all empty or complete *)
1171 val thy = assoc_thy dI';
1172 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1173 else prep_ori fmz thy ((#ppc o get_pbt) pI');
1174 val (pt,c) = cappend_problem e_ptree [] e_istate (fmz,(dI',pI',mI'))
1175 (oris,(dI',pI',mI'),e_term);
1176 val {ppc,prls,where_,...} = get_pbt pI'
1177 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1178 val pt = update_pbl pt [] pbl;
1179 val pre = check_preconds thy prls where_ pbl
1180 val pb = foldl and_ (true, map fst pre)*)
1181 val (pbl, pre, pb) = ([], [], false)
1184 (([],Pbl), (([],Pbl),Uistate),
1185 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1186 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1187 Refine_Tacitly pI', Safe,pt)
1189 (([],Pbl), (([],Pbl),Uistate),
1190 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1191 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1195 (*ONLY for STARTING modeling phase*)
1196 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1197 let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
1199 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
1201 val thy' = if dI = e_domID then dI' else dI
1202 val thy = assoc_thy thy'
1203 val {ppc,prls,where_,...} = get_pbt pI'
1204 val pre = check_preconds thy prls where_ pbl
1205 val pb = foldl and_ (true, map fst pre)
1206 val ((p,_),_,_,pt) =
1207 generate1 thy (Model_Problem'([],pbl,met)) Uistate pos pt
1208 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1209 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1210 in ((p,Pbl), ((p,p_),Uistate),
1211 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1212 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1215 (*. called only if no_met is specified .*)
1216 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1217 let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
1219 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
1221 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1222 (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
1223 (*val pt = update_pbl pt p pbl;
1224 val pt = update_orispec pt p
1225 (string_of_thy thy, pIre,
1226 if length met = 0 then e_metID else hd met);*)
1227 val (domID, metID) = (string_of_thy thy,
1228 if length met = 0 then e_metID else hd met)
1229 val ((p,_),_,_,pt) =
1230 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1232 (*val pre = check_preconds thy prls where_ pbl
1233 val pb = foldl and_ (true, map fst pre)*)
1234 val (pbl, pre, pb) = ([], [], false)
1235 in ((p,Pbl), (pos,Uistate),
1236 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1237 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1238 Model_Problem, Safe, pt) end
1240 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1241 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
1242 (Refine_Problem' rfd) Uistate pos pt
1243 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1244 Model_Problem, Safe, pt) end
1246 (* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
1247 val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
1249 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1250 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1251 meth=met, ...}) = get_obj I pt p;
1252 (*val pt = update_pbl pt p itms;
1253 val pt = update_pblID pt p pI;*)
1254 val thy = assoc_thy dI
1255 val ((p,Pbl),_,_,pt)=
1256 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
1257 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1258 val mI'' = if mI=e_metID then mI' else mI;
1259 (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
1260 val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1261 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1262 in ((p,Pbl), (pos,Uistate),
1263 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1264 (Problem pI, itms2itemppc dI'' itms pre))),
1266 (* val Specify_Method' mID = nxt; val (p,_) = p;
1267 val Specify_Method' mID = m;
1268 specify (Specify_Method' mID) (p,p_) c pt;
1270 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1271 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1272 meth=met, ...}) = get_obj I pt p;
1273 val {ppc,pre,prls,...} = get_met mID
1274 val thy = assoc_thy dI
1275 val oris = add_field' thy ppc oris;
1276 (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1277 val dI'' = if dI=e_domID then dI' else dI;
1278 val pI'' = if pI = e_pblID then pI' else pI;
1279 val met = if met=[] then pbl else met;
1280 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1281 (*val pt = update_met pt p itms;
1282 val pt = update_metID pt p mID*)
1284 generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1285 (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
1286 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1287 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1288 in (pos, (pos,Uistate),
1289 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1290 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1292 (* val Add_Find' ct = nxt; val sel = "#Find";
1294 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1295 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1296 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1297 (* val Specify_Theory' domID = m;
1298 val (Specify_Theory' domID, (p,p_)) = (m, pos);
1300 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1301 let val p_ = case p_ of Met => Met | _ => Pbl
1302 val thy = assoc_thy domID;
1303 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1304 probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
1305 val mppc = case p_ of Met => met | _ => pbl;
1306 val cpI = if pI = e_pblID then pI' else pI;
1307 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1308 val cmI = if mI = e_metID then mI' else mI;
1309 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1312 Met => (check_preconds thy mer mwh met)
1313 | _ => (check_preconds thy per pwh pbl)
1314 val pb = foldl and_ (true, map fst pre)
1317 (*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1318 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1319 (pbl,met) (ppc,mpc) (dI,pI,mI);
1320 in ((p,p_), (pos,Uistate),
1321 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1322 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1324 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1326 (*val pt = update_domID pt p domID;11.8.03*)
1327 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1329 (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1330 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1331 (ppc,mpc) (domID,pI,mI);
1332 in ((p,p_), (pos,Uistate),
1333 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1334 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1337 (* itms2itemppc thy [](*mpc*) pre
1339 | specify m' _ _ _ =
1340 error ("specify: not impl. for "^tac_2str m');
1342 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1343 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1345 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1347 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1348 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1349 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1350 val cpI = if pI = e_pblID then pI' else pI;
1351 in case appl_add thy sel oris pbl ((#ppc o get_pbt) cpI) ct of
1352 Add itm (*..union old input *) =>
1353 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1356 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1357 val pbl' = insert_ppc thy itm pbl
1360 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1361 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1362 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1363 val ((p,Pbl),c,_,pt') =
1364 generate1 thy tac_ Uistate (p,Pbl) pt
1365 in ([(tac,tac_,((p,Pbl),Uistate))], c, (pt',(p,Pbl))):calcstate' end
1368 (*TODO.WN03 pass error-msgs to the frontend..
1369 FIXME ..and dont abuse a tactic for that purpose*)
1371 Tac_ (theory "Pure", msg,msg,msg),
1372 (e_pos', e_istate))], [], ptp)
1375 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1376 val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1378 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1380 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1381 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1382 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1383 val cmI = if mI = e_metID then mI' else mI;
1384 in case appl_add thy sel oris met ((#ppc o get_met) cmI) ct of
1385 Add itm (*..union old input *) =>
1386 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1388 val met' = insert_ppc thy itm met;
1391 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1392 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1393 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1394 val ((p,Met),c,_,pt') =
1395 generate1 thy tac_ Uistate (p,Met) pt
1396 in ([(tac,tac_,((p,Met), Uistate))], c, (pt',(p,Met))) end
1398 | Err msg => ([(*tacis*)], [], ptp)
1399 (*nxt_me collects tacis until not hide; here just no progress*)
1403 val (msg,itm) = appl_add thy sel oris ppc ct;
1404 val (Cor(d,ts)) = #5 itm;
1409 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1410 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1411 handle _ => error ("ori2Coritm: dsc "^
1413 "in ori, but not in pbt")
1415 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1416 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1417 (find_first (eq1 d))) pbt,ts))):itm)
1418 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1419 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1422 (*filter out oris which have same description in itms*)
1423 fun filter_outs oris [] = oris
1424 | filter_outs oris (i::itms) =
1425 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1426 (#4:ori -> term)) oris;
1427 in filter_outs ors itms end;
1429 fun memI a b = member op = a b;
1430 (*filter oris which are in pbt, too*)
1431 fun filter_pbt oris pbt =
1432 let val dscs = map (fst o snd) pbt
1433 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1435 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1436 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1438 fun x mem [] = false
1439 | x mem (y :: ys) = x = y orelse x mem ys;
1441 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1442 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1444 let val vat = max_vt pits;
1446 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1447 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1448 val os = filter_outs ors itms;
1449 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1450 in itms @ (map (ori2Coritm met) os) end
1455 (*.complete model and guard of a calc-head .*)
1457 fun x mem [] = false
1458 | x mem (y :: ys) = x = y orelse x mem ys;
1460 fun complete_mod_ (oris, mpc, ppc, probl) =
1461 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1462 val vat = if probl = [] then 1 else max_vt probl
1463 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1464 val pors = filter_outs pors pits (*which are in pbl already*)
1465 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1467 val pits = pits @ (map (ori2Coritm ppc) pors)
1468 val mits = complete_metitms oris pits [] mpc
1472 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1473 (if dI = e_domID then odI else dI,
1474 if pI = e_pblID then opI else pI,
1475 if mI = e_metID then omI else mI):spec;
1478 (*.find a next applicable tac (for calcstate) and update ptree
1479 (for ev. finding several more tacs due to hide).*)
1480 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1481 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1482 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1483 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1485 val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1486 val (dI, pI, mI) = some_spec ospec spec
1487 val thy = assoc_thy dI
1488 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1489 val {cas, ppc, ...} = get_pbt pI
1490 val pbl = init_pbl ppc (* fill in descriptions *)
1491 (*----------------if you think, this should be done by the Dialog
1492 in the java front-end, search there for WN060225-modelProblem----*)
1493 val (pbl, met) = case cas of NONE => (pbl, [])
1494 | _ => complete_mod_ (oris, mpc, ppc, probl)
1495 (*----------------------------------------------------------------*)
1496 val tac_ = Model_Problem' (pI, pbl, met)
1497 val (pos,c,_,pt) = generate1 thy tac_ Uistate pos pt
1498 in ([(tac,tac_, (pos, Uistate))], c, (pt,pos)):calcstate' end
1500 (* val Add_Find ct = tac;
1502 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1503 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1504 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1506 (*. called only if no_met is specified .*)
1507 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1508 let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1509 val opt = refine_ori oris pI
1512 let val {met,ppc,...} = get_pbt pI'
1513 val pbl = init_pbl ppc
1514 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1515 val mI = if length met = 0 then e_metID else hd met
1516 val thy = assoc_thy dI
1518 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1520 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1521 (pos, Uistate))], c, (pt,pos)) end
1522 | NONE => ([], [], ptp)
1525 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1526 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1527 probl, ...}) = get_obj I pt p
1528 val thy = if dI' = e_domID then dI else dI'
1529 in case refine_pbl (assoc_thy thy) pI probl of
1530 NONE => ([], [], ptp)
1531 | SOME (rfd as (pI',_)) =>
1532 let val (pos,c,_,pt) =
1533 generate1 (assoc_thy thy)
1534 (Refine_Problem' rfd) Uistate pos pt
1535 in ([(Refine_Problem pI, Refine_Problem' rfd,
1536 (pos, Uistate))], c, (pt,pos)) end
1539 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1540 let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1541 probl, ...}) = get_obj I pt p;
1542 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1543 val {ppc,where_,prls,...} = get_pbt pI
1544 val pbl as (_,(itms,_)) =
1545 if pI'=e_pblID andalso pI=e_pblID
1546 then (false, (init_pbl ppc, []))
1547 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1548 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1549 val ((p,Pbl),c,_,pt)=
1550 generate1 thy (Specify_Problem' (pI, pbl)) Uistate pos pt
1551 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1552 (pos,Uistate))], c, (pt,pos)) end
1554 (*transfers oris (not required in pbl) to met-model for script-env
1555 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1556 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1557 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1558 meth=met, ...}) = get_obj I pt p;
1559 val {ppc,pre,prls,...} = get_met mID
1560 val thy = assoc_thy dI
1561 val oris = add_field' thy ppc oris;
1562 val dI'' = if dI=e_domID then dI' else dI;
1563 val pI'' = if pI = e_pblID then pI' else pI;
1564 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1565 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1567 generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1568 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1569 (pos,Uistate))], c, (pt,pos)) end
1571 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1572 let val (dI',_,_) = get_obj g_spec pt p
1574 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1576 in (*FIXXXME: check if pbl can still be parsed*)
1577 ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1580 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1581 let val (dI',_,_) = get_obj g_spec pt p
1583 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1585 in (*FIXXXME: check if met can still be parsed*)
1586 ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1590 error ("nxt_specif: not impl. for "^tac2str m');
1592 (*.get the values from oris; handle the term list w.r.t. penv.*)
1595 fun x mem [] = false
1596 | x mem (y :: ys) = x = y orelse x mem ys;
1598 fun vals_of_oris oris =
1599 ((map (mkval' o (#5:ori -> term list))) o
1600 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1605 (*.create a calc-tree with oris via an cas.refined pbl.*)
1606 fun nxt_specify_init_calc (([],(dI,pI,mI)): fmz) =
1607 (* val ([],(dI,pI,mI)) = (fmz, sp);
1609 if pI <> [] then (*comes from pbl-browser*)
1610 let val {cas,met,ppc,thy,...} = get_pbt pI
1611 val dI = if dI = "" then theory2theory' thy else dI
1612 val thy = assoc_thy dI
1613 val mI = if mI = [] then hd met else mI
1614 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1615 val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1616 ([], (dI,pI,mI), hdl)
1617 val pt = update_spec pt [] (dI,pI,mI)
1618 val pits = init_pbl' ppc
1619 val pt = update_pbl pt [] pits
1620 in ((pt,([],Pbl)), []): calcstate end
1621 else if mI <> [] then (*comes from met-browser*)
1622 let val {ppc,...} = get_met mI
1623 val dI = if dI = "" then "Isac" else dI
1624 val thy = assoc_thy dI
1625 val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1626 ([], (dI,pI,mI), e_term(*FIXME met*))
1627 val pt = update_spec pt [] (dI,pI,mI)
1628 val mits = init_pbl' ppc
1629 val pt = update_met pt [] mits
1630 in ((pt,([],Met)), []) end
1631 else (*completely new example*)
1632 let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec)
1633 ([], e_spec, e_term)
1634 in ((pt,([],Pbl)), []) end
1635 (* val (fmz, (dI,pI,mI)) = (fmz, sp);
1637 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1638 let (* both """"""""""""""""""""""""" either empty or complete *)
1639 val thy = assoc_thy dI
1640 val (pI, pors, mI) =
1642 then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI)
1643 val pI' = refine_ori' pors pI;
1644 in (pI', pors(*refinement over models with diff.precond only*),
1645 (hd o #met o get_pbt) pI') end
1646 else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI)
1647 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1648 val dI = theory2theory' (maxthy thy thy');
1649 val hdl = case cas of
1650 NONE => pblterm dI pI
1651 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1652 ~~~ vals_of_oris pors) t
1653 val (pt, _) = cappend_problem e_ptree [] e_istate (fmz, (dI, pI, mI))
1654 (pors, (dI, pI, mI), hdl)
1655 in ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) end;
1660 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1661 (* case appl_spec p pt m of /// 19.1.00
1662 Notappl e => Error' (Error_ e)
1664 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1668 (*fun tag_form thy (formal, given) = cterm_of thy
1669 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1670 fun tag_form thy (formal, given) =
1671 (let val gf = (head_of given) $ formal;
1672 val _ = cterm_of thy gf
1674 handle _ => error ("calchead.tag_form: " ^
1675 Syntax.string_of_term (thy2ctxt thy) given ^
1677 Syntax.string_of_term (thy2ctxt thy) formal ^
1678 " ..types do not match");
1679 (* val formal = (the o (parse thy)) "[R::real]";
1680 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1681 > tag_form thy (formal, given);
1682 val it = "fixed_values [R]" : cterm
1684 fun chktyp thy (n, fs, gs) =
1685 ((tracing o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) fs;
1686 (tracing o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) gs;
1687 tag_form thy (nth n fs, nth n gs));
1689 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1691 (* #####################################################
1692 find the failing item:
1694 > val tag__form = chktyp (n,formals,givens);
1695 > (type_of o term_of o (nth n)) formals;
1696 > (type_of o term_of o (nth n)) givens;
1697 > atomty ((term_of o (nth n)) formals);
1698 > atomty ((term_of o (nth n)) givens);
1699 > atomty (term_of tag__form);
1700 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1701 ##################################################### *)
1703 (* #####################################################
1705 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1706 val formals = map (the o (parse thy)) origin;
1708 val given = ["equation (lhs=rhs)",
1709 "bound_variable bdv", (* TODO type *)
1711 val where_ = ["e is_root_equation_in bdv",
1713 "apx is_const_expr"];
1714 val find = ["L::rat set"];
1715 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1716 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1717 val givens = map (the o (parse thy)) given;
1719 val tag__forms = chktyps (formals, givens);
1720 map ((atomty) o term_of) tag__forms;
1721 ##################################################### *)
1724 (* check pbltypes, announces one failure a time *)
1725 (*fun chk_vars ctppc =
1726 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1727 appc flat (mappc (vars o term_of) ctppc)
1728 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1729 else if (re\\(gi union fi)) <> []
1730 then ("re\\(gi union fi)",re\\(gi union fi))
1731 else ("ok",[]) end;*)
1732 fun chk_vars ctppc =
1733 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1734 appc flat (mappc vars ctppc)
1735 val chked = subtract op = gi wh
1736 in if chked <> [] then ("wh\\gi", chked)
1737 else let val chked = subtract op = (union op = gi fi) re
1739 then ("re\\(gi union fi)", chked)
1744 (* check a new pbltype: variables (Free) unbound by given, find*)
1745 fun unbound_ppc ctppc =
1746 let val {Given=gi,Find=fi,Relate=re,...} =
1747 appc flat (mappc vars ctppc)
1748 in distinct (*re\\(gi union fi)*)
1749 (subtract op = (union op = gi fi) re) end;
1751 > val org = {Given=["[R=(R::real)]"],Where=[],
1752 Find=["[A::real]"],With=[],
1753 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1755 > val ctppc = mappc (the o (parse thy)) org;
1756 > unbound_ppc ctppc;
1757 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1761 (* f, a binary operator, is nested rightassociative *)
1764 fun fld f (x::[]) = x
1765 | fld f (x::x'::[]) = f (x',x)
1766 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1767 in ((fld f) o rev) xs end;
1769 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1770 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1771 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1772 > cterm_of thy conj;
1773 val it = "(a = b & c = d) & e = f" : cterm
1776 (* f, a binary operator, is nested leftassociative *)
1777 fun foldl1 f (x::[]) = x
1778 | foldl1 f (x::x'::[]) = f (x,x')
1779 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1781 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1782 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1783 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1784 > cterm_of thy conj;
1785 val it = "a = b & c = d & e = f & g = h" : cterm
1789 (* called only once, if a Subproblem has been located in the script*)
1790 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
1791 (* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
1795 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1796 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1797 (*all stored in tac_ itms ^^^^^^^^^^*)
1798 | nxt_model_pbl tac_ _ =
1799 error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1800 (* run subp_rooteq.sml ''
1801 until nxt=("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1802 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1803 (last_elem o drop_last) ets'';
1804 > val mst = (last_elem o drop_last) ets'';
1805 > nxt_model_pbl mst;
1806 val it = Refine_Tacitly ["univariate","equation"] : tac
1809 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1810 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1811 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1816 tracing (oris2str pors);
1818 tracing (itms2str_ thy pits);
1819 tracing (itms2str_ thy mits);
1823 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1824 + met from fmz; assumes pos on PblObj, meth = [].*)
1825 fun complete_mod (pt, pos as (p, p_):pos') =
1826 (* val (pt, (p, _)) = (pt, p);
1827 val (pt, (p, _)) = (pt, pos);
1829 let val _= if p_ <> Pbl
1830 then tracing("###complete_mod: only impl.for Pbl, called with "^
1831 pos'2str pos) else ()
1832 val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
1834 val (dI,pI,mI) = some_spec ospec spec
1835 val mpc = (#ppc o get_met) mI
1836 val ppc = (#ppc o get_pbt) pI
1837 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1838 val pt = update_pblppc pt p pits
1839 val pt = update_metppc pt p mits
1840 in (pt, (p,Met):pos') end
1842 (*| complete_mod (pt, pos as (p, Met):pos') =
1843 error ("###complete_mod: only impl.for Pbl, called with "^
1846 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1847 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1848 fun all_modspec (pt, (p,_):pos') =
1849 (* val (pt, (p,_)) = ptp;
1851 let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1852 ...}) = get_obj I pt p;
1853 val thy = assoc_thy dI;
1854 val {ppc,...} = get_met mI;
1855 val mors = prep_ori fmz_ thy ppc;
1856 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1857 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1858 val pt = update_spec pt p (dI,pI,mI);
1859 in (pt, (p,Met): pos') end;
1861 (*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1862 fun is_complete_mod_ ([]: itm list) = false
1863 | is_complete_mod_ itms =
1864 foldl and_ (true, (map #3 itms));
1865 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1866 if (is_pblobj o (get_obj I pt)) p
1867 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1868 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1869 | is_complete_mod (pt, pos as (p, Met)) =
1870 if (is_pblobj o (get_obj I pt)) p
1871 then (is_complete_mod_ o (get_obj g_met pt)) p
1872 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1873 | is_complete_mod (_, pos) =
1874 error ("is_complete_mod called by "^pos'2str pos^
1875 " (should be Pbl or Met)");
1877 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1878 fun is_complete_spec (pt, pos as (p,_): pos') =
1879 if (not o is_pblobj o (get_obj I pt)) p
1880 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1881 else let val (dI,pI,mI) = get_obj g_spec pt p
1882 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1883 (*.complete empty items in specification from origin (pbl, met ev.refined);
1884 assumes 'is_complete_mod'.*)
1885 fun complete_spec (pt, pos as (p,_): pos') =
1886 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1887 val pt = update_spec pt p (some_spec ospec spec)
1890 fun is_complete_modspec ptp =
1891 is_complete_mod ptp andalso is_complete_spec ptp;
1896 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1897 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1899 let val (_,_,metID) = get_somespec' spec spec'
1901 if metID = e_metID then []
1902 else let val {prls,pre=where_,...} = get_met metID
1903 val pre = check_preconds' prls where_ meth 0
1905 val allcorrect = is_complete_mod_ meth
1906 andalso foldl and_ (true, (map #1 pre))
1907 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1908 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1909 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1911 let val (_,pI,_) = get_somespec' spec spec'
1913 if pI = e_pblID then []
1914 else let val {prls,where_,cas,...} = get_pbt pI
1915 val pre = check_preconds' prls where_ probl 0
1917 val allcorrect = is_complete_mod_ probl
1918 andalso foldl and_ (true, (map #1 pre))
1919 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1922 fun pt_form (PrfObj {form,...}) = Form form
1923 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1924 let val (dI, pI, _) = get_somespec' spec spec'
1925 val {cas,...} = get_pbt pI
1927 NONE => Form (pblterm dI pI)
1928 | SOME t => Form (subst_atomic (mk_env probl) t)
1930 (*vvv takes the tac _generating_ the formula=result, asm ok....
1931 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1933 if null asm then NONE else SOME asm,
1935 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1936 let val (_,_,metID) = some_spec ospec spec
1938 if null asm then NONE else SOME asm,
1939 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1940 -------------------------------------------------------------------------*)
1943 (*.pt_extract returns
1944 # the formula at pos
1945 # the tactic applied to this formula
1946 # the list of assumptions generated at this formula
1947 (by application of another tac to the preceding formula !)
1948 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1949 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1950 fun pt_extract (pt,([],Res)) =
1951 (* val (pt,([],Res)) = ptp;
1953 let val (f, asm) = get_obj g_result pt []
1954 in (Form f, NONE, asm) end
1957 | pt_extract (pt,(p,Res)) =
1958 (* val (pt,(p,Res)) = ptp;
1960 let val (f, asm) = get_obj g_result pt p
1961 val tac = if last_onlev pt p
1962 then if is_pblobj' pt (lev_up p)
1963 then let val (PblObj{spec=(_,pI,_),...}) =
1964 get_obj I pt (lev_up p)
1965 in if pI = e_pblID then NONE
1966 else SOME (Check_Postcond pI) end
1967 else SOME End_Trans (*WN0502 TODO for other branches*)
1968 else let val p' = lev_on p
1969 in if is_pblobj' pt p'
1970 then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1972 in SOME (Subproblem (dI, pI)) end
1973 else if f = get_obj g_form pt p'
1974 then SOME (get_obj g_tac pt p')
1975 (*because this Frm ~~~is not on worksheet*)
1976 else SOME (Take (term2str (get_obj g_form pt p')))
1978 in (Form f, tac, asm) end
1980 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1981 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1982 val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
1984 let val ppobj = get_obj I pt p
1985 val f = if is_pblobj ppobj then pt_model ppobj p_
1986 else get_obj pt_form pt p
1987 val tac = g_tac ppobj
1988 in (f, SOME tac, []) end;
1991 (**. get the formula from a ctree-node:
1992 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1993 take res from all other PrfObj's .**)
1994 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1995 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1996 [("headline", (p, Frm), h),
1997 ("stepform", (p, Res), r)]
1998 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1999 [("stepform", (p, Frm), form),
2000 ("stepform", (p, Res), r)];
2002 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
2003 [("stepform", (p, Res), r)]
2005 (*assumes to take whole level, in particular hd -- for use in interSteps*)
2006 fun get_formress fs p [] = flat fs
2007 | get_formress fs p (nd::nds) =
2008 (* start with 'form+res' and continue with trying 'res' only*)
2009 get_forms (fs @ [formres p nd]) (lev_on p) nds
2010 and get_forms fs p [] = flat fs
2011 | get_forms fs p (nd::nds) =
2013 (* start again with 'form+res' ///ugly repeat with Check_elementwise
2014 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
2015 then get_forms (fs @ [formres p nd]) (lev_on p) nds
2016 (* continue with trying 'res' only*)
2017 else get_forms (fs @ [form p nd]) (lev_on p) nds;
2019 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
2020 (*WN050219 made robust against _'to' below or after Complete nodes
2021 by handling exn caused by move_dn*)
2022 (*WN0401 this functionality belongs to ctree.sml,
2023 but fetching a calc_head requires calculations defined in modspec.sml
2024 transfer to ME/me.sml !!!
2025 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
2026 is returned !!!!!!!!!!!!!
2028 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
2029 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
2030 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
2034 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
2038 | eq_pos' _ _ = false;
2040 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
2041 total ordering Position#compareTo(Position p) in the java-code
2042 val get_interval = fn
2043 : pos' -> : from is "move_up 1st-element" to return
2044 pos' -> : to the last element to be returned; from < to
2045 int -> : level: 0 gets the flattest sub-tree possible
2046 >999 gets the deepest sub-tree possible
2048 (pos' * : of the formula
2049 Term.term) : the formula
2052 fun get_interval from to level pt =
2053 (* val (from,level) = (f,lev);
2054 val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
2056 let fun get_inter c (from:pos') (to:pos') lev pt =
2057 (* val (c, from, to, lev) = ([], from, to, level);
2058 ------for recursion.......
2059 val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
2061 if eq_pos' from to orelse from = ([],Res)
2062 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
2063 if 'to' has values NOT generated by move_dn, see systest/me.sml
2064 TODO.WN0501: introduce an order on pos' and check "from > to"..
2065 ...there is an order in Java!
2066 WN051224 the hack got worse with returning term instead ptform*)
2067 then let val (f,_,_) = pt_extract (pt, from)
2069 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2070 | Form t => c @ [(from, t)]
2073 if lev < lev_of from
2074 then (get_inter c (move_dn [] pt from) to lev pt)
2075 handle (PTREE _(*from move_dn too far*)) => c
2076 else let val (f,_,_) = pt_extract (pt, from)
2077 val term = case f of
2078 ModSpec (_,_,headline,_,_,_)=> headline
2080 in (get_inter (c @ [(from, term)])
2081 (move_dn [] pt from) to lev pt)
2082 handle (PTREE _(*from move_dn too far*))
2083 => c @ [(from, term)] end
2084 in get_inter [] from to level pt end;
2087 fun posform2str (pos:pos', form) =
2088 "("^ pos'2str pos ^", "^
2090 Form f => term2str f
2091 | ModSpec c => term2str (#3 c(*the headline*)))
2093 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2094 (map posform2str)) pfs;
2095 fun posterm2str (pos:pos', t) =
2096 "("^ pos'2str pos ^", "^term2str t^")";
2097 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2098 (map posterm2str)) pfs;
2101 (*WN050225 omits the last step, if pt is incomplete*)
2103 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
2105 (*.get a calchead from a PblObj-node in the ctree;
2106 preconditions must be calculated.*)
2107 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
2108 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
2110 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2111 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
2112 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
2113 | get_ocalhd (pt, pos' as (p,Met):pos') =
2114 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2117 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2118 val pre = check_preconds (assoc_thy"Isac") prls pre meth
2119 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
2121 (*.at the activeFormula set the Model, the Guard and the Specification
2122 to empty and return a CalcHead;
2123 the 'origin' remains (for reconstructing all that).*)
2124 fun reset_calchead (pt, pos' as (p,_):pos') =
2125 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
2126 val pt = update_pbl pt p []
2127 val pt = update_met pt p []
2128 val pt = update_spec pt p e_spec
2129 in (pt, (p,Pbl):pos') end;
2131 (*---------------------------------------------------------------------*)
2135 (*---------------------------------------------------------------------*)