1 (* Specify-phase: specifying and modeling a problem or a subproblem. The
2 most important types are declared in mstools.sml.
5 (c) due to copyright terms
9 12345678901234567890123456789012345678901234567890123456789012345678901234567890
10 10 20 30 40 50 60 70 80
13 (* TODO interne Funktionen aus sig entfernen *)
16 datatype additm = Add of SpecifyTools.itm | Err of string
17 val all_dsc_in : SpecifyTools.itm_ list -> Term.term list
18 val all_modspec : ptree * pos' -> ptree * pos'
19 datatype appl = Appl of tac_ | Notappl of string
23 SpecifyTools.ori list ->
24 SpecifyTools.itm list ->
25 (string * (Term.term * Term.term)) list -> cterm' -> additm
28 val chk_vars : term ppc -> string * Term.term list
30 theory -> int * term list * term list -> term
32 theory -> term list * term list -> term list
33 val complete_metitms :
34 SpecifyTools.ori list ->
35 SpecifyTools.itm list ->
36 SpecifyTools.itm list -> pat list -> SpecifyTools.itm list
37 val complete_mod_ : ori list * pat list * pat list * itm list ->
39 val complete_mod : ptree * pos' -> ptree * (pos * pos_)
40 val complete_spec : ptree * pos' -> ptree * pos'
42 pat list -> preori list -> pat -> preori
43 val e_calcstate : calcstate
44 val e_calcstate' : calcstate'
45 val eq1 : ''a -> 'b * (''a * 'c) -> bool
47 ''a -> Term.term -> 'b * 'c * 'd * ''a * SpecifyTools.itm_ -> bool
48 val eq4 : ''a -> 'b * ''a list * 'c * 'd * 'e -> bool
50 'a * 'b * 'c * 'd * SpecifyTools.itm_ ->
51 'e * 'f * 'g * Term.term * 'h -> bool
52 val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool
53 val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool
54 val f_mout : theory -> mout -> Term.term
56 SpecifyTools.ori list ->
57 SpecifyTools.itm list -> SpecifyTools.ori list
59 SpecifyTools.ori list ->
60 ('a * (Term.term * 'b)) list -> SpecifyTools.ori list
61 val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
62 val foldr1 : ('a * 'a -> 'a) -> 'a list -> 'a
63 val form : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
64 val formres : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
65 val gen_ins' : ('a * 'a -> bool) -> 'a * 'a list -> 'a list
67 (string * (pos * pos_) * Term.term) list list ->
68 pos -> ptree list -> (string * (pos * pos_) * Term.term) list
70 (string * (pos * pos_) * Term.term) list list ->
71 posel list -> ptree list -> (string * (pos * pos_) * Term.term) list
72 val get_interval : pos' -> pos' -> int -> ptree -> (pos' * term) list
73 val get_ocalhd : ptree * pos' -> ocalhd
74 val get_spec_form : tac_ -> pos' -> ptree -> mout
77 SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'
78 val getr_ct : theory -> SpecifyTools.ori -> string * cterm'
79 val has_list_type : Term.term -> bool
80 val header : pos_ -> pblID -> metID -> pblmet
83 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
84 SpecifyTools.itm list -> SpecifyTools.itm list
86 SpecifyTools.itm -> SpecifyTools.itm list -> SpecifyTools.itm list
87 val is_complete_mod : ptree * pos' -> bool
88 val is_complete_mod_ : SpecifyTools.itm list -> bool
89 val is_complete_modspec : ptree * pos' -> bool
90 val is_complete_spec : ptree * pos' -> bool
91 val is_copy_named : 'a * ('b * Term.term) -> bool
92 val is_copy_named_idstr : string -> bool
93 val is_error : SpecifyTools.itm_ -> bool
94 val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
98 SpecifyTools.ori list ->
99 Term.term -> string * SpecifyTools.ori * Term.term list
100 val is_list_type : Term.typ -> bool
101 val is_notyet_input :
103 SpecifyTools.itm list ->
106 ('a * (Term.term * Term.term)) list -> string * SpecifyTools.itm
107 val is_parsed : SpecifyTools.itm_ -> bool
108 val is_untouched : SpecifyTools.itm -> bool
113 (int list * string * Term.term * Term.term list) list ->
114 (int list * string * Term.term * Term.term list) list
116 theory -> pat list -> Term.term list -> SpecifyTools.ori list
117 val maxl : int list -> int
118 val match_ags_msg : string list -> Term.term -> Term.term list -> unit
119 val memI : ''a list -> ''a -> bool
120 val mk_additem : string -> cterm' -> tac
121 val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
123 theory -> pat -> Term.term -> SpecifyTools.preori option
126 SpecifyTools.ori list ->
127 (string * (Term.term * 'a)) list ->
128 SpecifyTools.itm list -> (string * cterm') option
129 val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
133 SpecifyTools.ori list ->
135 SpecifyTools.itm list * SpecifyTools.itm list ->
136 (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->
138 val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'
139 val nxt_specif_additem :
140 string -> cterm' -> ptree * (int list * pos_) -> calcstate'
141 val nxt_specify_init_calc : fmz -> calcstate
142 val ocalhd_complete :
143 SpecifyTools.itm list ->
144 (bool * Term.term) list -> domID * pblID * metID -> bool
146 pat list -> ori -> itm
150 Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
153 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
154 SpecifyTools.itm list ->
155 (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
156 val parse_ok : SpecifyTools.itm_ list -> bool
157 val posform2str : pos' * ptform -> string
158 val posforms2str : (pos' * ptform) list -> string
159 val posterms2str : (pos' * term) list -> string (*tests only*)
160 val ppc135list : 'a SpecifyTools.ppc -> 'a list
161 val ppc2list : 'a SpecifyTools.ppc -> 'a list
163 ptree * (int list * pos_) ->
164 ptform * tac option * Term.term list
165 val pt_form : ppobj -> ptform
166 val pt_model : ppobj -> pos_ -> ptform
167 val reset_calchead : ptree * pos' -> ptree * pos'
171 Term.term * Term.term list ->
172 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
173 -> string * SpecifyTools.ori * Term.term list
178 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
179 -> string * SpecifyTools.ori * Term.term list
181 int -> SpecifyTools.itm list -> SpecifyTools.itm option
182 val show_pt : ptree -> unit
183 val some_spec : spec -> spec -> spec
189 (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *
191 val specify_additem :
197 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
198 val tag_form : theory -> term * term -> term
199 val test_types : theory -> Term.term * Term.term list -> string
200 val typeless : Term.term -> Term.term
201 val unbound_ppc : term SpecifyTools.ppc -> Term.term list
202 val vals_of_oris : SpecifyTools.ori list -> Term.term list
203 val variants_in : Term.term list -> int
204 val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
205 val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
212 (*---------------------------------------------------------------------*)
213 structure CalcHead (**): CALC_HEAD(**) =
216 (*---------------------------------------------------------------------*)
220 (*.the state wich is stored after each step of calculation; it contains
221 the calc-state and a list of [tac,istate](="tacis") to be applied.
222 the last_elem tacis is the first to apply to the calc-state and
223 the (only) one shown to the front-end as the 'proposed tac'.
224 the calc-state resulting from the application of tacis is not stored,
225 because the tacis hold enought information for efficiently rebuilding
226 this state just by "fun generate ".*)
228 (ptree * pos') * (*the calc-state to which the tacis could be applied*)
229 (taci list); (*ev. several (hidden) steps;
230 in REVERSE order: first tac_ to apply is last_elem*)
231 val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
233 (*the state used during one calculation within the mathengine; it contains
234 a list of [tac,istate](="tacis") which generated the the calc-state;
235 while this state's tacis are extended by each (internal) step,
236 the calc-state is used for creating new nodes in the calc-tree
237 (eg. applicable_in requires several particular nodes of the calc-tree)
238 and then replaced by the the newly created;
239 on leave of the mathengine the resuing calc-state is dropped anyway,
240 because the tacis hold enought information for efficiently rebuilding
241 this state just by "fun generate ".*)
243 taci list * (*cas. several (hidden) steps;
244 in REVERSE order: first tac_ to apply is last_elem*)
245 pos' list * (*a "continuous" sequence of pos',
246 deleted by application of taci list*)
247 (ptree * pos'); (*the calc-state resulting from the application of tacis*)
248 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
250 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
251 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
252 | f_mout thy _ = raise error "f_mout: not called with formula";
255 (*.is the calchead complete ?.*)
256 fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
257 foldl and_ (true, map #3 its) andalso
258 foldl and_ (true, map #1 pre) andalso
259 dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
262 (* make a term 'typeless' for comparing with another 'typeless' term;
263 'type-less' usually is illtyped *)
264 fun typeless (Const(s,_)) = (Const(s,e_type))
265 | typeless (Free(s,_)) = (Free(s,e_type))
266 | typeless (Var(n,_)) = (Var(n,e_type))
267 | typeless (Bound i) = (Bound i)
268 | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
269 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
271 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
272 > val (_,t1) = split_dsc_t hs (term_of ct);
273 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
274 > val (_,t2) = split_dsc_t hs (term_of ct);
275 > typeless t1 = typeless t2;
281 (*.to an input (d,ts) find the according ori and insert the ts.*)
282 (*WN.11.03: + dont take first inter<>[]*)
283 fun seek_oridts thy sel (d,ts) [] =
284 ("'"^(Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))^
285 "' not found (typed)", (0,[],sel,d,ts):ori, [])
286 (* val (id,vat,sel',d',ts')::oris = ori;
287 val (id,vat,sel',d',ts') = ori;
289 | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
290 if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
293 (id,vat,sel,d, inter op = ts ts'):ori,
295 else ((Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))
299 else seek_oridts thy sel (d,ts) oris;
301 (*.to an input (_,ts) find the according ori and insert the ts.*)
302 fun seek_orits thy sel ts [] =
304 (strs2str (map (Syntax.string_of_term (thy2ctxt thy)) ts))^
305 "' not found (typed)", e_ori_, [])
306 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
307 if sel = sel' andalso (inter op = ts ts') <> []
310 (id,vat,sel,d, inter op = ts ts'):ori,
312 else (((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
316 else seek_orits thy sel ts oris;
318 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
319 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
320 uncaught exception TYPE
321 > seek_orits thy sel ts [];
322 uncaught exception TYPE
325 (*find_first item with #1 equal to id*)
326 fun seek_ppc id [] = NONE
327 | seek_ppc id (p::(ppc:itm list)) =
328 if id = #1 p then SOME p else seek_ppc id ppc;
332 (*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
335 datatype appl = Appl of tac_ | Notappl of string;
337 fun ppc2list ({Given=gis,Where=whs,Find=fis,
338 With=wis,Relate=res}: 'a ppc) =
339 gis @ whs @ fis @ wis @ res;
340 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
346 (* get the number of variants in a problem in 'original',
347 assumes equal descriptions in immediate sequence *)
349 let fun eq(x,y) = head_of x = head_of y;
350 fun cnt eq [] y n = ([n],[])
351 | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
353 fun coll eq xs [] = xs
354 | coll eq xs (y::ys) =
355 let val (n,ys') = cnt eq (y::ys) y 0;
356 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
357 val vts = subtract op = [1] (distinct (coll eq [] ts));
358 in case vts of [] => 1 | [n] => n
359 | _ => error "different variants in formalization" end;
361 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
362 val it = ([3],[4,5,5,5,5,5]) : int list * int list
363 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
364 val it = [1,3,1,5] : int list
367 fun is_list_type (Type("List.list",_)) = true
368 | is_list_type _ = false;
369 (* fun destr (Type(str,sort)) = (str,sort);
370 > val (SOME ct) = parse thy "lll::real list";
371 > val ty = (#T o rep_cterm) ct;
375 val it = ("List.list",["RealDef.real"]) : string * typ list
376 > atomty ((#t o rep_cterm) ct);
378 *** Free ( lll, real list)
381 > val (SOME ct) = parse thy "[lll::real]";
382 > val ty = (#T o rep_cterm) ct;
386 val it = ("List.list",["'a"]) : string * typ list
387 > atomty ((#t o rep_cterm) ct);
389 *** Const ( List.list.Cons, [real, real list] => real list)
390 *** Free ( lll, real)
391 *** Const ( List.list.Nil, real list)
393 > val (SOME ct) = parse thy "lll";
394 > val ty = (#T o rep_cterm) ct;
396 val it = false : bool *)
399 fun has_list_type (Free(_,T)) = is_list_type T
400 | has_list_type _ = false;
402 > val (SOME ct) = parse thy "lll::real list";
403 > has_list_type (term_of ct);
405 > val (SOME ct) = parse thy "[lll::real]";
406 > has_list_type (term_of ct);
407 val it = false : bool *)
409 fun is_parsed (Syn _) = false
410 | is_parsed _ = true;
411 fun parse_ok its = foldl and_ (true, map is_parsed its);
413 fun all_dsc_in itm_s =
415 fun d_in (Cor ((d,_),_)) = [d]
418 | d_in (Inc ((d,_),_)) = [d]
419 | d_in (Sup (d,_)) = [d]
420 | d_in (Mis (d,_)) = [d];
421 in (flat o (map d_in)) itm_s end;
424 fun is_Syn (Syn _) = true
425 | is_Syn (Typ _) = true
428 fun is_error (Cor (_,ts)) = false
429 | is_error (Sup (_,ts)) = false
430 | is_error (Inc (_,ts)) = false
431 | is_error (Mis (_,ts)) = false
435 fun ct_in (Syn (c)) = c
436 | ct_in (Typ (c)) = c
437 | ct_in _ = raise error "ct_in called for Cor .. Sup";
440 (*#############################################################*)
441 (*#############################################################*)
442 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
445 (* testdaten besorgen:
446 use"test-coil-kernel.sml";
447 val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
452 variant V: oris union ppc => int, id ID: oris union ppc => int
455 EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
458 @vt = max sum(i : ppc) V i
464 > ((vts_cnt (vts_in itms))) itms;
469 > val vts = vts_in itms;
470 val vts = [1,2,3] : int list
471 > val nvts = vts_cnt vts itms;
472 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
473 > val mx = max2 nvts;
474 val mx = (3,7) : int * int
475 > val v = max_vt itms;
477 --------------------------
481 (*.get the first term in ts from ori.*)
482 (* val (_,_,fd,d,ts) = hd miss;
484 fun getr_ct thy ((_,_,fd,d,ts):ori) =
485 (fd, ((Syntax.string_of_term (thy2ctxt thy)) o
486 (comp_dts thy)) (d,[hd ts]):cterm');
487 (* val t = comp_dts thy (d,[hd ts]);
490 (* get a term from ori, notyet input in itm *)
491 fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) =
492 (fd, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy))
493 (d, subtract op = (ts_in itm_) ts):cterm');
494 (* test-maximum.sml fmy <> [], Init_Proof ...
495 val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl;
496 val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
501 Thm.cterm_of thy (d $ (hd ts));
502 Thm.cterm_of thy (d' $ ts');
508 (* in FE dsc, not dat: this is in itms ...*)
509 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
510 | is_untouched _ = false;
513 (* select an item in oris, notyet input in itms
514 (precondition: in itms are only Cor, Sup, Inc) *)
518 | x mem (y :: ys) = x = y orelse x mem ys;
520 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
522 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
523 fun is_elem itms (f,(d,t)) =
524 case find_first (test_d d) itms of
525 SOME _ => true | NONE => false;
526 in case filter_out (is_elem itms) pbt of
527 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
530 SOME (f:string, ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts thy) (d,[]):cterm')
533 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
535 | nxt_add thy oris pbt itms =
537 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
538 andalso (#3 ori) <>"#undef";
539 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
540 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
541 (* val itm = hd icl; val (_,_,_,d,ts) = v6;
543 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
544 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
545 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
546 | false_and_not_Sup (i,v,false,f, _) = true
547 | false_and_not_Sup _ = false;
549 val v = if itms = [] then 1 else max_vt itms;
550 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
551 val vits = if v = 0 then itms (*because of dsc without dat*)
552 else filter (testi_vt v) itms; (*itms..vat*)
553 val icl = filter false_and_not_Sup vits; (* incomplete *)
555 then case filter_out (test_id (map #1 vits)) vors of
557 (* val miss = filter_out (test_id (map #1 vits)) vors;
559 | miss => SOME (getr_ct thy (hd miss))
561 case find_first (test_subset (hd icl)) vors of
562 (* val SOME ori = find_first (test_subset (hd icl)) vors;
564 NONE => raise error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
565 | SOME ori => SOME (geti_ct thy ori (hd icl))
571 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
572 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
573 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
574 | mk_delete thy str _ =
575 raise error ("mk_delete: called with field '"^str^"'");
576 fun mk_additem "#Given" ct = Add_Given ct
577 | mk_additem "#Find" ct = Add_Find ct
578 | mk_additem "#Relate"ct = Add_Relation ct
580 raise error ("mk_additem: called with field '"^str^"'");
586 (* find the next tac in specify (except nxt_model_pbl)
587 4.00.: TODO: do not return a pos !!!
588 (sind from DG comes the _OLD_ writepos)*)
590 > val (pbl,pbt,mpc) =(pbl',get_pbt cpI,(#ppc o get_met) cmI);
591 > val (dI,pI,mI) = empty_spec;
592 > nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*))
593 ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec);
596 > val met = [];val (pbt,mpc) = (get_pbt pI',(#ppc o get_met) mI');
597 > val (dI,pI,mI) = empty_spec;
598 > nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*))
599 ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec);
602 (*. determine the next step of specification;
603 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
604 eg. in rootpbl 'no_met':
606 preok predicates are _all_ ok, or problem matches completely
607 oris immediately from formalization
608 (dI',pI',mI') specification coming from author/parent-problem
609 (pbl, item lists specified by user
610 met) -"-, tacitly completed by copy_probl
611 (dI,pI,mI) specification explicitly done by the user
612 (pbt, mpc) problem type, guard of method
614 (* val (preok,pbl,pbt,mpc)=(pb,pbl',(#ppc o get_pbt) cpI,(#ppc o get_met) cmI);
615 val (preok,pbl,pbt,mpc)=(pb,pbl',ppc,(#ppc o get_met) cmI);
616 val (Pbl, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) =
617 (p_, pb, oris, (dI',pI',mI'), (probl,meth),
618 (ppc, (#ppc o get_met) cmI), (dI,pI,mI));
620 fun nxt_spec Pbl preok (oris:ori list) ((dI',pI',mI'):spec)
621 ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec) =
622 ((*writeln"### nxt_spec Pbl";*)
623 if dI'=e_domID andalso dI=e_domID then (Pbl, Specify_Theory dI')
624 else if pI'=e_pblID andalso pI=e_pblID then (Pbl, Specify_Problem pI')
625 else case find_first (is_error o #5) (pbl:itm list) of
626 SOME (_,_,_,fd,itm_) =>
628 (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
630 ((*writeln"### nxt_spec is_error NONE";*)
631 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))
633 (* val SOME (fd,ct') = nxt_add (assoc_thy (if dI=e_domID then dI' else dI))
636 SOME (fd,ct') => ((*writeln"### nxt_spec nxt_add SOME";*)
637 (Pbl, mk_additem fd ct'))
638 | NONE => (*pbl-items complete*)
639 if not preok then (Pbl, Refine_Problem pI')
641 if dI = e_domID then (Pbl, Specify_Theory dI')
642 else if pI = e_pblID then (Pbl, Specify_Problem pI')
643 else if mI = e_metID then (Pbl, Specify_Method mI')
645 case find_first (is_error o #5) met of
646 SOME (_,_,_,fd,itm_) =>
647 (Met, mk_delete (assoc_thy dI) fd itm_)
649 (case nxt_add (assoc_thy dI) oris mpc met of
650 SOME (fd,ct') => (*30.8.01: pre?!?*)
651 (Met, mk_additem fd ct')
653 ((*Solv 3.4.00*)Met, Apply_Method mI))))
654 (* val preok=pb; val (pbl, met) = (pbl,met');
655 val (pbt,mpc)=((#ppc o get_pbt) cpI,(#ppc o get_met) cmI);
656 val (Met, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) =
657 (p_, pb, oris, (dI',pI',mI'), (probl,meth),
658 (ppc, (#ppc o get_met) cmI), (dI,pI,mI));
660 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
661 ((*writeln"### nxt_spec Met"; *)
662 case find_first (is_error o #5) met of
663 SOME (_,_,_,fd,itm_) =>
664 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
666 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
667 SOME (fd,ct') => (Met, mk_additem fd ct')
669 ((*writeln"### nxt_spec Met: nxt_add NONE";*)
670 if dI = e_domID then (Met, Specify_Theory dI')
671 else if pI = e_pblID then (Met, Specify_Problem pI')
672 else if not preok then (Met, Specify_Method mI)
673 else (Met, Apply_Method mI)));
676 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
677 (2,[2],true,"#Find",Syn("empty"))];
681 (* ^^^--- aus nnewcode.sml am 30.1.00 ---^^^ *)
682 (*#############################################################*)
683 (*#############################################################*)
684 (* vvv--- aus nnewcode.sml vor 29.1.00 ---vvv *)
687 fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) =
688 (id,vt,cl,sl,Cor (d,ts)):itm
689 | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =
690 raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
691 " not not for Syn (s:cterm')")
692 | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) =
693 raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
694 " not not for Typ (s:cterm')")
695 | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
696 (id,vt,cl,sl,Fal (d,ts))
697 | update_itm (cl,d,ts) (id,vt,_,sl,Inc (_,_)) =
698 (id,vt,cl,sl,Inc (d,ts))
699 | update_itm (cl,d,ts) (id,vt,_,sl,Sup (_,_)) =
700 (id,vt,cl,sl,Sup (d,ts));
706 fun is_field_correct sel d dscpbt =
707 case assoc (dscpbt, sel) of
709 | SOME ds => member op = ds d;
711 (*. update the itm_ already input, all..from ori .*)
712 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
714 fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) =
716 val ts' = union op = (ts_in itm_) ts;
717 val pval = pbl_ids' thy d ts'
718 (*WN.9.5.03: FIXXXME [#0, epsilon]
719 here would upd_penv be called for [#0, epsilon] etc. *)
720 val complete = if eq_set op = (ts', all) then true else false;
723 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
724 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
725 | (Syn c) => raise error ("ori_2itm wants to overwrite "^c)
726 | (Typ c) => raise error ("ori_2itm wants to overwrite "^c)
727 | (Inc _) => if complete
728 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
729 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
730 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
731 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
732 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
733 (* 28.1.00: not completely clear ---^^^ etc.*)
734 (* 4.9.01: Mis just copied---vvv *)
735 | (Mis _) => if complete
736 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
737 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
741 fun eq1 d (_,(d',_)) = (d = d');
742 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
745 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
746 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
747 pval: value for problem-environment _NOT_ checked for 'inter' --
748 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
749 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
750 (*. is_input ori itms <=>
751 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
752 (2) ori(ts) subset itm(ts) --- Err "already input"
753 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
754 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
755 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
757 fun is_notyet_input thy (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
758 case find_first (eq1 d) pbt of
759 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
760 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
762 (case find_first (eq3 f d) itms of
763 SOME (_,_,_,_,itm_) =>
765 val ts' = inter op = (ts_in itm_) ts;
766 in if subset op = (ts, ts')
768 map (Syntax.string_of_term (thy2ctxt thy))) ts')^
769 " already input", e_itm) (*2*)
771 ori_2itm thy itm_ pid all (i,v,f,d,
772 subtract op = ts' ts)) (*3,4*)
774 | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
775 pid all (i,v,f,d,ts)) (*1*)
777 | NONE => ("", ori_2itm thy (Sup (d,ts))
778 e_term all (i,v,f,d,ts));
780 fun test_types thy (d,ts) =
782 val s = !show_types; val _ = show_types:= true;
783 val opt = (try (comp_dts thy)) (d,ts);
784 val msg = case opt of
786 | NONE => ((Syntax.string_of_term (thy2ctxt thy) d)^" "^
787 ((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
789 val _ = show_types:= s
794 fun maxl [] = raise error "maxl of []"
797 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
801 (*. is the input term t known in oris ?
802 give feedback on all(?) strange input;
803 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
804 (*WN.11.03: from lists*)
805 fun is_known thy sel ori t =
806 (* val (ori,t)=(oris,term_of ct);
809 val ots = (distinct o flat o (map #5)) (ori:ori list);
810 val oids = ((map (fst o dest_Free)) o distinct o
811 flat o (map vars)) ots;
812 val (d,ts(*,pval*)) = split_dts thy t;
813 val ids = map (fst o dest_Free)
814 ((distinct o (flat o (map vars))) ts);
815 in if (subtract op = oids ids) <> []
816 then (("identifiers "^(strs2str' (subtract op = oids ids))^
817 " not in example"), e_ori_, [])
821 if not (subset op = (map typeless ts, map typeless ots))
823 ((strs2str' o (map (Syntax.string_of_term
824 (thy2ctxt thy)))) ts)^
825 "' not in example (typeless)"), e_ori_, [])
826 else (case seek_orits thy sel ts ori of
827 ("", ori_ as (_,_,_,d,ts), all) =>
828 (case test_types thy (d,ts) of
829 "" => ("", ori_, all)
830 | msg => (msg, e_ori_, []))
831 | (msg,_,_) => (msg, e_ori_, []))
833 if member op = (map #4 ori) d
834 then seek_oridts thy sel (d,ts) ori
835 else ((Syntax.string_of_term (thy2ctxt thy) d)^
836 (*" not in example", e_ori_, []) ///11.11.03*)
837 " not in example", (0,[],sel,d,ts), [])
841 (*. for return-value of appl_add .*)
844 | Err of string; (*error-message*)
847 (*. add an item; check wrt. oris and pbt .*)
849 (* in contrary to oris<>[] below, this part handles user-input
850 extremely acceptive, i.e. accept input instead error-msg *)
851 fun appl_add thy sel ([]:ori list) ppc pbt ct' =
852 (* val (ppc,pbt,ct',env) = (pbl, (#ppc o get_pbt) cpI, ct, []:envv);
853 !!!! 28.8.01: env tested _minimally_ !!!
856 val i = 1 + (if ppc=[] then 0 else maxl (map #1 ppc));
857 in case parse thy ct' of (*should be done in applicable_in 4.00.FIXME*)
858 NONE => Add (i,[],false,sel,Syn ct')
859 (* val (SOME ct) = parse thy ct';
863 val (d,ts(*,pval*)) = split_dts thy (term_of ct);
865 then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*)))
868 (case find_first (eq1 d) pbt of
869 NONE => Add (i,[],true,sel,Sup ((d,ts)))
871 (* val SOME (f,(_,id)) = find_first (eq1 d) pbt;
874 fun eq2 d ((i,_,_,_,itm_):itm) =
875 (d = (d_in itm_)) andalso i<>0;
876 in case find_first (eq2 d) ppc of
877 NONE => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*)
879 | SOME (i',_,_,_,itm_) =>
880 (* val SOME (i',_,_,_,itm_) = find_first (eq2 d) ppc;
881 val NONE = find_first (eq2 d) ppc;
884 then let val ts = union op = ts (ts_in itm_)
885 in Add (if ts_in itm_ = [] then i else i',
886 [],true,f,Cor ((d, ts), (id, (*pval*)
889 else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*)
895 (*. add ct to ppc .*)
896 (*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*)
897 (* val (ppc,pbt) = (pbl, ppc);
898 val (ppc,pbt) = (met, (#ppc o get_met) cmI);
900 val (ppc,pbt) = (pbl, (#ppc o get_pbt) cpI);
902 | appl_add thy sel oris ppc pbt(*only for upd_envv*) ct =
904 val ctopt = parse thy ct;
906 NONE => Err ("syntax error in "^ct)
907 | SOME ct =>(* val SOME ct = ctopt;
908 val (msg,ori',all) = is_known thy sel oris (term_of ct);
909 val (msg,itm) = is_notyet_input thy ppc all ori' pbt;
911 (case is_known thy sel oris (term_of ct) of
912 ("",ori'(*ts='ct'*), all) =>
913 (case is_notyet_input thy ppc all ori' pbt of
915 | (msg,_) => Err msg)
916 | (msg,_,_) => Err msg)
919 > val (msg,itm) = is_notyet_input thy ppc all ori';
920 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
922 > val ts = ts_in itm_;
926 (*---------------------------------------------(4) nach ptyps.sml 23.3.02*)
929 (** make oris from args of the stac SubProblem and from pbt **)
931 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
932 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
933 fun is_copy_named_idstr str =
934 case (rev o explode) str of
935 "_"::_::"_"::_ => true
937 (*> is_copy_named_idstr "v_i_";
939 > is_copy_named_idstr "e_";
940 val it = false : bool
941 > is_copy_named_idstr "L___";
944 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
945 fun is_copy_named_generating_idstr str =
946 if is_copy_named_idstr str
947 then case (rev o explode) str of
948 "_"::"_"::"_"::_ => false
951 (*> is_copy_named_generating_idstr "v_i_";
953 > is_copy_named_generating_idstr "L___";
954 val it = false : bool
957 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
958 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
959 fun is_copy_named (_,(_,t)) = (is_copy_named_idstr o free2str) t;
960 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
961 fun is_copy_named_generating (_,(_,t)) =
962 (is_copy_named_generating_idstr o free2str) t;
965 (*.split type-wrapper from scr-arg and build part of an ori;
966 an type-error is reported immediately, raises an exn,
967 subsequent handling of exn provides 2nd part of error message.*)
968 (*fun mtc thy ((str, (dsc, _)):pat) (ty $ var) = WN100820 made cterm to term
969 (* val (thy, (str, (dsc, _)), (ty $ var)) =
972 (Thm.cterm_of thy (dsc $ var);(*type check*)
973 SOME ((([1], str, dsc, (*[var]*)
974 split_dts' (dsc, var))): preori)(*:ori without leading #*))
975 handle e as TYPE _ =>
976 (writeln (dashs 70^"\n"
977 ^"*** ERROR while creating the items for the model of the ->problem\n"
978 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
979 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
980 ^"*** description: "^(term_detail2str dsc)
981 ^"*** value: "^(term_detail2str var)
982 ^"*** typeconstructor in script: "^(term_detail2str ty)
983 ^"*** checked by theory: "^(theory2str thy)^"\n"
985 print_exn e; (*raises exn again*)
987 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
988 (* val (thy, (str, (dsc, _)), (ty $ var)) =
991 (Thm.cterm_of thy (dsc $ var);(*type check*)
992 SOME ((([1], str, dsc, (*[var]*)
993 split_dts' (dsc, var))): preori)(*:ori without leading #*))
994 handle e as TYPE _ =>
995 (writeln (dashs 70^"\n"
996 ^"*** ERROR while creating the items for the model of the ->problem\n"
997 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
998 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
999 ^"*** description: "^(term_detail2str dsc)
1000 ^"*** value: "^(term_detail2str var)
1001 ^"*** typeconstructor in script: "^(term_detail2str ty)
1002 ^"*** checked by theory: "^(theory2str thy)^"\n"
1004 (*WN100820 postponed: print_exn e; raises exn again*)
1006 (*> val pbt = (#ppc o get_pbt) ["univariate","equation"];
1007 > val Const ("Script.SubProblem",_) $
1008 (Const ("Pair",_) $ Free (thy', _) $
1009 (Const ("Pair",_) $ pblID' $ metID')) $ ags =
1010 str2term"(SubProblem (SqRoot_,[univariate,equation],\
1011 \[SqRoot_,solve_linear]) [bool_ (x+1- 2=0), real_ x])::bool list";
1012 > val ags = isalist2list ags;
1013 > mtc thy (hd pbt) (hd ags);
1014 val it = SOME ([1],"#Given",Const (#,#),[# $ #]) *)
1016 (*.match each pat of the model-pattern with an actual argument;
1017 precondition: copy-named vars are filtered out.*)
1018 fun matc thy ([]:pat list) _ (oris:preori list) = oris
1019 | matc thy pbt [] _ =
1020 (writeln (dashs 70);
1021 raise error ("actual arg(s) missing for '"^pats2str pbt
1022 ^"' i.e. should be 'copy-named' by '*_._'"))
1023 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
1024 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
1025 (thy, pbt', ags, []);
1027 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
1028 (thy, pbt, ags, (oris @ [ori]));
1030 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
1031 else(*..del?*) let val opt = mtc thy p a;
1033 (* val SOME ori = mtc thy p a;
1035 SOME ori => matc thy pbt ags (oris @ [ori])
1036 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
1038 (* run subp-rooteq.sml until Init_Proof before ...
1039 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
1040 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
1042 other vars as in mtc ..
1043 > matc thy (drop_last pbt) ags [];
1044 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
1047 (*WN051014 outcommented with redesign copy-named (for omitting '#Find'
1049 kept as initial idea for generating x_1, x_2, ... for equations*)
1050 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
1051 (* val ((pbt:pat list), (oris:preori list), ((field,(dsc,t)):pat)) =
1052 (pbt', oris', hd (*!!!!!*) cy);
1054 (if is_copy_named_generating p
1055 then (*WN051014 kept strange old code ...*)
1056 let fun sel (_,_,d,ts) = comp_ts (d, ts)
1057 val cy' = (implode o drop_last o drop_last o explode o free2str) t
1058 val ext = (last_elem o drop_last o explode o free2str) t
1059 val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*)
1060 val vals = map sel oris
1061 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
1062 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
1063 else ([1], field, dsc, [t])
1065 handle _ => raise error ("cpy_nam: for "^(term2str t));
1067 (*> val (field,(dsc,t)) = last_elem pbt;
1068 > cpy_nam pbt (drop_last oris) (field,(dsc,t));
1069 val it = ([1],"#Find",
1070 Const ("Descript.solutions","bool List.list => Tools.toreall"),
1071 [Free ("x_i","bool List.list")]) *)
1074 (*.match the actual arguments of a SubProblem with a model-pattern
1075 and create an ori list (in root-pbl created from formalization).
1076 expects ags:pats = 1:1, while copy-named are filtered out of pats;
1077 copy-named pats are appended in order to get them into the model-items.*)
1078 fun match_ags thy (pbt:pat list) ags =
1079 (* val (thy, pbt, ags) = (thy, (#ppc o get_pbt) pI, ags);
1080 val (thy, pbt, ags) = (thy, pats, ags);
1082 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
1083 val pbt' = filter_out is_copy_named pbt;
1084 val cy = filter is_copy_named pbt;
1085 val oris' = matc thy pbt' ags [];
1086 val cy' = map (cpy_nam pbt' oris') cy;
1087 val ors = add_id (oris' @ cy');
1088 (*appended in order to get ^^^^^ them into the model-items*)
1089 in (map flattup ors):ori list end;
1091 > match_ags thy pbt ags;
1093 [(1,[1],"#Given",Const ("Descript.equality","bool => Tools.una"),
1094 [Const # $ (# $ #) $ Free (#,#)]),
1095 (2,[1],"#Given",Const ("Descript.solveFor","RealDef.real => Tools.una"),
1096 [Free ("x","RealDef.real")]),
1098 Const ("Descript.solutions","bool List.list => Tools.toreall"),
1099 [Free ("x_i","bool List.list")])] : ori list*)
1101 (*.report part of the error-msg which is not available in match_args.*)
1102 fun match_ags_msg pI stac ags =
1103 let val s = !show_types
1104 val _ = show_types:= true
1105 val pats = (#ppc o get_pbt) pI
1106 val msg = (dots 70^"\n"
1107 ^"*** problem "^strs2str pI^" has the ...\n"
1108 ^"*** model-pattern "^pats2str pats^"\n"
1109 ^"*** stac '"^term2str stac^"' has the ...\n"
1110 ^"*** arg-list "^terms2str ags^"\n"
1112 val _ = show_types:= s
1116 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
1117 fun vars_of_pbl_ pbl_ =
1118 let fun var_of_pbl_ (gfr,(dsc,t)) = t
1119 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
1120 fun vars_of_pbl_' pbl_ =
1121 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
1122 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
1124 fun overwrite_ppc thy itm ppc =
1126 fun repl ppc' (_,_,_,_,itm_) [] =
1127 raise error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
1129 | repl ppc' itm (p::ppc) =
1130 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
1131 else repl (ppc' @ [p]) itm ppc
1132 in repl [] itm ppc end;
1134 (*10.3.00: insert the already compiled itm into model;
1135 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
1138 fun insert_ppc thy itm ppc =
1140 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
1141 | eq_untouched _ _ = false;
1144 (*writeln("### insert_ppc: itm= "^(itm2str_ itm));*)
1145 case seek_ppc (#1 itm) ppc of
1146 (* val SOME xxx = seek_ppc (#1 itm) ppc;
1148 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
1149 overwrite_ppc thy itm ppc
1150 | NONE => (ppc @ [itm]));
1151 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
1153 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
1154 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
1156 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
1157 (d_in itm_) = (d_in iitm_);
1158 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
1159 handles superfluous items carelessly*)
1160 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
1162 > gen_ins' eee (4,[1,3,5,7]);
1163 val it = [1, 3, 5, 7, 4] : int list*)
1166 (*. output the headline to a ppc .*)
1167 fun header p_ pI mI =
1168 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1170 | pos => raise error ("header called with "^ pos_2str pos);
1174 (* test-printouts ---
1175 val _=writeln("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts))));
1176 val _=writeln("### insert_ppc: pts= "^
1177 (strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) pts);
1180 val sel = "#Given"; val Add_Given' ct = m;
1182 val sel = "#Find"; val Add_Find' (ct,_) = m;
1184 val (_,_,f,nxt',_,pt')= specify_additem sel (ct,[]) (p,Pbl(*!!!!!!!*)) c pt;
1186 val sel = "#Given"; val Add_Given' (ct,_) = nxt; val (p,_) = p;
1188 fun specify_additem sel (ct,_) (p,Met) c pt =
1190 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1191 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1192 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1193 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1194 val cpI = if pI = e_pblID then pI' else pI;
1195 val cmI = if mI = e_metID then mI' else mI;
1196 val {ppc,pre,prls,...} = get_met cmI
1197 in case appl_add thy sel oris met ppc ct of
1198 Add itm (*..union old input *) =>
1199 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1201 val met' = insert_ppc thy itm met;
1202 (*val pt' = update_met pt p met';*)
1203 val ((p,Met),_,_,pt') =
1204 generate1 thy (case sel of
1205 "#Given" => Add_Given' (ct, met')
1206 | "#Find" => Add_Find' (ct, met')
1207 | "#Relate"=> Add_Relation'(ct, met'))
1209 val pre' = check_preconds thy prls pre met'
1210 val pb = foldl and_ (true, map fst pre')
1211 (*val _=writeln("@@@ specify_additem: Met Add before nxt_spec")*)
1213 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1214 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1215 in ((p,p_), ((p,p_),Uistate),
1216 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1217 (Method cmI, itms2itemppc thy met' pre'))),
1220 let val pre' = check_preconds thy prls pre met
1221 val pb = foldl and_ (true, map fst pre')
1222 (*val _=writeln("@@@ specify_additem: Met Err before nxt_spec")*)
1224 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1225 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1226 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1230 | specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1232 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1233 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1234 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1235 val cpI = if pI = e_pblID then pI' else pI;
1236 val cmI = if mI = e_metID then mI' else mI;
1237 val {ppc,where_,prls,...} = get_pbt cpI;
1238 in case appl_add thy sel oris pbl ppc ct of
1239 Add itm (*..union old input *) =>
1240 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1243 (*val _= writeln("###specify_additem: itm= "^(itm2str_ itm));*)
1244 val pbl' = insert_ppc thy itm pbl
1245 val ((p,Pbl),_,_,pt') =
1246 generate1 thy (case sel of
1247 "#Given" => Add_Given' (ct, pbl')
1248 | "#Find" => Add_Find' (ct, pbl')
1249 | "#Relate"=> Add_Relation'(ct, pbl'))
1251 val pre = check_preconds thy prls where_ pbl'
1252 val pb = foldl and_ (true, map fst pre)
1253 (*val _=writeln("@@@ specify_additem: Pbl Add before nxt_spec")*)
1255 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1256 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1257 val ppc = if p_= Pbl then pbl' else met;
1258 in ((p,p_), ((p,p_),Uistate),
1259 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1261 itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1264 let val pre = check_preconds thy prls where_ pbl
1265 val pb = foldl and_ (true, map fst pre)
1266 (*val _=writeln("@@@ specify_additem: Pbl Err before nxt_spec")*)
1268 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1269 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1270 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1272 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1273 val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1277 val (msg,itm) = appl_add thy sel oris ppc ct;
1278 val (Cor(d,ts)) = #5 itm;
1285 (* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1286 specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1288 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1289 let (* either """"""""""""""" all empty or complete *)
1290 val thy = assoc_thy dI';
1291 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1292 else prep_ori fmz thy ((#ppc o get_pbt) pI');
1293 val (pt,c) = cappend_problem e_ptree [] e_istate (fmz,(dI',pI',mI'))
1294 (oris,(dI',pI',mI'),e_term);
1295 val {ppc,prls,where_,...} = get_pbt pI'
1296 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1297 val pt = update_pbl pt [] pbl;
1298 val pre = check_preconds thy prls where_ pbl
1299 val pb = foldl and_ (true, map fst pre)*)
1300 val (pbl, pre, pb) = ([], [], false)
1303 (([],Pbl), (([],Pbl),Uistate),
1304 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1305 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1306 Refine_Tacitly pI', Safe,pt)
1308 (([],Pbl), (([],Pbl),Uistate),
1309 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1310 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1314 (*ONLY for STARTING modeling phase*)
1315 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1316 let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
1318 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
1320 val thy' = if dI = e_domID then dI' else dI
1321 val thy = assoc_thy thy'
1322 val {ppc,prls,where_,...} = get_pbt pI'
1323 val pre = check_preconds thy prls where_ pbl
1324 val pb = foldl and_ (true, map fst pre)
1325 val ((p,_),_,_,pt) =
1326 generate1 thy (Model_Problem'([],pbl,met)) Uistate pos pt
1327 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1328 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1329 in ((p,Pbl), ((p,p_),Uistate),
1330 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1331 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1334 (*. called only if no_met is specified .*)
1335 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1336 let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
1338 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
1340 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1341 (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
1342 (*val pt = update_pbl pt p pbl;
1343 val pt = update_orispec pt p
1344 (string_of_thy thy, pIre,
1345 if length met = 0 then e_metID else hd met);*)
1346 val (domID, metID) = (string_of_thy thy,
1347 if length met = 0 then e_metID else hd met)
1348 val ((p,_),_,_,pt) =
1349 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1351 (*val pre = check_preconds thy prls where_ pbl
1352 val pb = foldl and_ (true, map fst pre)*)
1353 val (pbl, pre, pb) = ([], [], false)
1354 in ((p,Pbl), (pos,Uistate),
1355 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1356 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1357 Model_Problem, Safe, pt) end
1359 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1360 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac.thy")
1361 (Refine_Problem' rfd) Uistate pos pt
1362 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1363 Model_Problem, Safe, pt) end
1365 (* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
1366 val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
1368 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1369 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1370 meth=met, ...}) = get_obj I pt p;
1371 (*val pt = update_pbl pt p itms;
1372 val pt = update_pblID pt p pI;*)
1373 val thy = assoc_thy dI
1374 val ((p,Pbl),_,_,pt)=
1375 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
1376 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1377 val mI'' = if mI=e_metID then mI' else mI;
1378 (*val _=writeln("@@@ specify (Specify_Problem) before nxt_spec")*)
1379 val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1380 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1381 in ((p,Pbl), (pos,Uistate),
1382 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1383 (Problem pI, itms2itemppc dI'' itms pre))),
1385 (* val Specify_Method' mID = nxt; val (p,_) = p;
1386 val Specify_Method' mID = m;
1387 specify (Specify_Method' mID) (p,p_) c pt;
1389 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1390 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1391 meth=met, ...}) = get_obj I pt p;
1392 val {ppc,pre,prls,...} = get_met mID
1393 val thy = assoc_thy dI
1394 val oris = add_field' thy ppc oris;
1395 (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1396 val dI'' = if dI=e_domID then dI' else dI;
1397 val pI'' = if pI = e_pblID then pI' else pI;
1398 val met = if met=[] then pbl else met;
1399 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1400 (*val pt = update_met pt p itms;
1401 val pt = update_metID pt p mID*)
1403 generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1404 (*val _=writeln("@@@ specify (Specify_Method) before nxt_spec")*)
1405 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1406 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1407 in (pos, (pos,Uistate),
1408 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1409 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1411 (* val Add_Find' ct = nxt; val sel = "#Find";
1413 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1414 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1415 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1416 (* val Specify_Theory' domID = m;
1417 val (Specify_Theory' domID, (p,p_)) = (m, pos);
1419 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1420 let val p_ = case p_ of Met => Met | _ => Pbl
1421 val thy = assoc_thy domID;
1422 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1423 probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
1424 val mppc = case p_ of Met => met | _ => pbl;
1425 val cpI = if pI = e_pblID then pI' else pI;
1426 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1427 val cmI = if mI = e_metID then mI' else mI;
1428 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1431 Met => (check_preconds thy mer mwh met)
1432 | _ => (check_preconds thy per pwh pbl)
1433 val pb = foldl and_ (true, map fst pre)
1436 (*val _=writeln("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1437 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1438 (pbl,met) (ppc,mpc) (dI,pI,mI);
1439 in ((p,p_), (pos,Uistate),
1440 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1441 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1443 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1445 (*val pt = update_domID pt p domID;11.8.03*)
1446 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1448 (*val _=writeln("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1449 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1450 (ppc,mpc) (domID,pI,mI);
1451 in ((p,p_), (pos,Uistate),
1452 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1453 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1456 (* itms2itemppc thy [](*mpc*) pre
1458 | specify m' _ _ _ =
1459 raise error ("specify: not impl. for "^tac_2str m');
1461 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1462 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1464 fun nxt_specif_additem sel ct (ptp as (pt,(p,Pbl))) =
1466 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1467 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1468 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1469 val cpI = if pI = e_pblID then pI' else pI;
1470 in case appl_add thy sel oris pbl ((#ppc o get_pbt) cpI) ct of
1471 Add itm (*..union old input *) =>
1472 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1475 (*val _=writeln("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1476 val pbl' = insert_ppc thy itm pbl
1479 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1480 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1481 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1482 val ((p,Pbl),c,_,pt') =
1483 generate1 thy tac_ Uistate (p,Pbl) pt
1484 in ([(tac,tac_,((p,Pbl),Uistate))], c, (pt',(p,Pbl))):calcstate' end
1487 (*TODO.WN03 pass error-msgs to the frontend..
1488 FIXME ..and dont abuse a tactic for that purpose*)
1490 Tac_ (theory "Pure", msg,msg,msg),
1491 (e_pos', e_istate))], [], ptp)
1494 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1495 val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1497 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1499 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1500 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1501 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1502 val cmI = if mI = e_metID then mI' else mI;
1503 in case appl_add thy sel oris met ((#ppc o get_met) cmI) ct of
1504 Add itm (*..union old input *) =>
1505 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1507 val met' = insert_ppc thy itm met;
1510 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1511 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1512 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1513 val ((p,Met),c,_,pt') =
1514 generate1 thy tac_ Uistate (p,Met) pt
1515 in ([(tac,tac_,((p,Met), Uistate))], c, (pt',(p,Met))) end
1517 | Err msg => ([(*tacis*)], [], ptp)
1518 (*nxt_me collects tacis until not hide; here just no progress*)
1522 val (msg,itm) = appl_add thy sel oris ppc ct;
1523 val (Cor(d,ts)) = #5 itm;
1528 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1529 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1530 handle _ => raise error ("ori2Coritm: dsc "^
1532 "in ori, but not in pbt")
1534 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1535 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1536 (find_first (eq1 d))) pbt,ts))):itm)
1537 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1538 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1541 (*filter out oris which have same description in itms*)
1542 fun filter_outs oris [] = oris
1543 | filter_outs oris (i::itms) =
1544 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1545 (#4:ori -> term)) oris;
1546 in filter_outs ors itms end;
1548 fun memI a b = member op = a b;
1549 (*filter oris which are in pbt, too*)
1550 fun filter_pbt oris pbt =
1551 let val dscs = map (fst o snd) pbt
1552 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1554 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1555 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1558 fun x mem [] = false
1559 | x mem (y :: ys) = x = y orelse x mem ys;
1561 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1562 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1564 let val vat = max_vt pits;
1566 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1567 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1568 val os = filter_outs ors itms;
1569 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1570 in itms @ (map (ori2Coritm met) os) end
1575 (*.complete model and guard of a calc-head .*)
1578 fun x mem [] = false
1579 | x mem (y :: ys) = x = y orelse x mem ys;
1581 fun complete_mod_ (oris, mpc, ppc, probl) =
1582 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1583 val vat = if probl = [] then 1 else max_vt probl
1584 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1585 val pors = filter_outs pors pits (*which are in pbl already*)
1586 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1588 val pits = pits @ (map (ori2Coritm ppc) pors)
1589 val mits = complete_metitms oris pits [] mpc
1593 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1594 (if dI = e_domID then odI else dI,
1595 if pI = e_pblID then opI else pI,
1596 if mI = e_metID then omI else mI):spec;
1599 (*.find a next applicable tac (for calcstate) and update ptree
1600 (for ev. finding several more tacs due to hide).*)
1601 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1602 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1603 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1604 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1606 val (PblObj{origin=(oris,ospec,_),probl,spec,...}) = get_obj I pt p
1607 val (dI,pI,mI) = some_spec ospec spec
1608 val thy = assoc_thy dI
1609 val mpc = (#ppc o get_met) mI (*just for reuse complete_mod_*)
1610 val {cas,ppc,...} = get_pbt pI
1611 val pbl = init_pbl ppc (*fill in descriptions*)
1612 (*--------------if you think, this should be done by the Dialog
1613 in the java front-end, search there for WN060225-modelProblem----*)
1614 val (pbl,met) = case cas of NONE => (pbl,[])
1615 | _ => complete_mod_ (oris, mpc, ppc, probl)
1616 (*----------------------------------------------------------------*)
1617 val tac_ = Model_Problem' (pI, pbl, met)
1618 val (pos,c,_,pt) = generate1 thy tac_ Uistate pos pt
1619 in ([(tac,tac_, (pos, Uistate))], c, (pt,pos)):calcstate' end
1621 (* val Add_Find ct = tac;
1623 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1624 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1625 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1627 (*. called only if no_met is specified .*)
1628 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1629 let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1630 val opt = refine_ori oris pI
1633 let val {met,ppc,...} = get_pbt pI'
1634 val pbl = init_pbl ppc
1635 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1636 val mI = if length met = 0 then e_metID else hd met
1637 val thy = assoc_thy dI
1639 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1641 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1642 (pos, Uistate))], c, (pt,pos)) end
1643 | NONE => ([], [], ptp)
1646 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1647 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1648 probl, ...}) = get_obj I pt p
1649 val thy = if dI' = e_domID then dI else dI'
1650 in case refine_pbl (assoc_thy thy) pI probl of
1651 NONE => ([], [], ptp)
1652 | SOME (rfd as (pI',_)) =>
1653 let val (pos,c,_,pt) =
1654 generate1 (assoc_thy thy)
1655 (Refine_Problem' rfd) Uistate pos pt
1656 in ([(Refine_Problem pI, Refine_Problem' rfd,
1657 (pos, Uistate))], c, (pt,pos)) end
1660 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1661 let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1662 probl, ...}) = get_obj I pt p;
1663 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1664 val {ppc,where_,prls,...} = get_pbt pI
1665 val pbl as (_,(itms,_)) =
1666 if pI'=e_pblID andalso pI=e_pblID
1667 then (false, (init_pbl ppc, []))
1668 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1669 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1670 val ((p,Pbl),c,_,pt)=
1671 generate1 thy (Specify_Problem' (pI, pbl)) Uistate pos pt
1672 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1673 (pos,Uistate))], c, (pt,pos)) end
1675 (*transfers oris (not required in pbl) to met-model for script-env
1676 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1677 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1678 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1679 meth=met, ...}) = get_obj I pt p;
1680 val {ppc,pre,prls,...} = get_met mID
1681 val thy = assoc_thy dI
1682 val oris = add_field' thy ppc oris;
1683 val dI'' = if dI=e_domID then dI' else dI;
1684 val pI'' = if pI = e_pblID then pI' else pI;
1685 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1686 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1688 generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1689 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1690 (pos,Uistate))], c, (pt,pos)) end
1692 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1693 let val (dI',_,_) = get_obj g_spec pt p
1695 generate1 (assoc_thy "Isac.thy") (Specify_Theory' dI)
1697 in (*FIXXXME: check if pbl can still be parsed*)
1698 ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1701 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1702 let val (dI',_,_) = get_obj g_spec pt p
1704 generate1 (assoc_thy "Isac.thy") (Specify_Theory' dI)
1706 in (*FIXXXME: check if met can still be parsed*)
1707 ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1711 raise error ("nxt_specif: not impl. for "^tac2str m');
1713 (*.get the values from oris; handle the term list w.r.t. penv.*)
1717 fun x mem [] = false
1718 | x mem (y :: ys) = x = y orelse x mem ys;
1720 fun vals_of_oris oris =
1721 ((map (mkval' o (#5:ori -> term list))) o
1722 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1727 (*.create a calc-tree with oris via an cas.refined pbl.*)
1728 fun nxt_specify_init_calc (([],(dI,pI,mI)): fmz) =
1729 (* val ([],(dI,pI,mI)) = (fmz, sp);
1731 if pI <> [] then (*comes from pbl-browser*)
1732 let val {cas,met,ppc,thy,...} = get_pbt pI
1733 val dI = if dI = "" then theory2theory' thy else dI
1734 val thy = assoc_thy dI
1735 val mI = if mI = [] then hd met else mI
1736 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1737 val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1738 ([], (dI,pI,mI), hdl)
1739 val pt = update_spec pt [] (dI,pI,mI)
1740 val pits = init_pbl' ppc
1741 val pt = update_pbl pt [] pits
1742 in ((pt,([],Pbl)), []): calcstate end
1743 else if mI <> [] then (*comes from met-browser*)
1744 let val {ppc,...} = get_met mI
1745 val dI = if dI = "" then "Isac.thy" else dI
1746 val thy = assoc_thy dI
1747 val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1748 ([], (dI,pI,mI), e_term(*FIXME met*))
1749 val pt = update_spec pt [] (dI,pI,mI)
1750 val mits = init_pbl' ppc
1751 val pt = update_met pt [] mits
1752 in ((pt,([],Met)), []) end
1753 else (*completely new example*)
1754 let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec)
1755 ([], e_spec, e_term)
1756 in ((pt,([],Pbl)), []) end
1757 (* val (fmz, (dI,pI,mI)) = (fmz, sp);
1759 | nxt_specify_init_calc (fmz:fmz_,(dI,pI,mI):spec) =
1760 let (* either """"""""""""""" all empty or complete *)
1761 val thy = assoc_thy dI
1762 val (pI, pors, mI) =
1764 then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI)
1765 val pI' = refine_ori' pors pI;
1766 in (pI', pors (*refinement over models with diff.prec only*),
1767 (hd o #met o get_pbt) pI') end
1768 else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI)
1769 val {cas,ppc,thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1770 val dI = theory2theory' (maxthy thy thy');
1771 val hdl = case cas of
1772 NONE => pblterm dI pI
1773 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1774 ~~~ vals_of_oris pors) t
1775 val (pt,_) = cappend_problem e_ptree [] e_istate (fmz,(dI,pI,mI))
1776 (pors,(dI,pI,mI),hdl)
1777 (*val pbl = init_pbl ppc WN.9.03: done by Model/Refine_Problem
1778 val pt = update_pbl pt [] pbl*)
1779 in ((pt,([],Pbl)), fst3 (nxt_specif Model_Problem (pt, ([],Pbl))))
1785 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1786 (* case appl_spec p pt m of /// 19.1.00
1787 Notappl e => Error' (Error_ e)
1789 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1793 (*fun tag_form thy (formal, given) = Thm.cterm_of thy
1794 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1795 fun tag_form thy (formal, given) =
1796 (let val gf = (head_of given) $ formal;
1797 val _ = Thm.cterm_of thy gf
1799 handle _ => raise error ("calchead.tag_form: " ^
1800 Syntax.string_of_term (thy2ctxt thy) given ^
1802 Syntax.string_of_term (thy2ctxt thy) formal ^
1803 " ..types do not match");
1804 (* val formal = (the o (parse thy)) "[R::real]";
1805 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1806 > tag_form thy (formal, given);
1807 val it = "fixed_values [R]" : cterm
1809 fun chktyp thy (n, fs, gs) =
1810 ((writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) fs;
1811 (writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) gs;
1812 tag_form thy (nth n fs, nth n gs));
1814 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1816 (* #####################################################
1817 find the failing item:
1819 > val tag__form = chktyp (n,formals,givens);
1820 > (type_of o term_of o (nth n)) formals;
1821 > (type_of o term_of o (nth n)) givens;
1822 > atomty ((term_of o (nth n)) formals);
1823 > atomty ((term_of o (nth n)) givens);
1824 > atomty (term_of tag__form);
1825 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1826 ##################################################### *)
1828 (* #####################################################
1830 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1831 val formals = map (the o (parse thy)) origin;
1833 val given = ["equation (lhs=rhs)",
1834 "bound_variable bdv", (* TODO type *)
1836 val where_ = ["e is_root_equation_in bdv",
1838 "apx is_const_expr"];
1839 val find = ["L::rat set"];
1840 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1841 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1842 val givens = map (the o (parse thy)) given;
1844 val tag__forms = chktyps (formals, givens);
1845 map ((atomty) o term_of) tag__forms;
1846 ##################################################### *)
1849 (* check pbltypes, announces one failure a time *)
1850 (*fun chk_vars ctppc =
1851 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1852 appc flat (mappc (vars o term_of) ctppc)
1853 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1854 else if (re\\(gi union fi)) <> []
1855 then ("re\\(gi union fi)",re\\(gi union fi))
1856 else ("ok",[]) end;*)
1857 fun chk_vars ctppc =
1858 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1859 appc flat (mappc vars ctppc)
1860 val chked = subtract op = gi wh
1861 in if chked <> [] then ("wh\\gi", chked)
1862 else let val chked = subtract op = (union op = gi fi) re
1864 then ("re\\(gi union fi)", chked)
1869 (* check a new pbltype: variables (Free) unbound by given, find*)
1870 fun unbound_ppc ctppc =
1871 let val {Given=gi,Find=fi,Relate=re,...} =
1872 appc flat (mappc vars ctppc)
1873 in distinct (*re\\(gi union fi)*)
1874 (subtract op = (union op = gi fi) re) end;
1876 > val org = {Given=["[R=(R::real)]"],Where=[],
1877 Find=["[A::real]"],With=[],
1878 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1880 > val ctppc = mappc (the o (parse thy)) org;
1881 > unbound_ppc ctppc;
1882 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1886 (* f, a binary operator, is nested rightassociative *)
1889 fun fld f (x::[]) = x
1890 | fld f (x::x'::[]) = f (x',x)
1891 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1892 in ((fld f) o rev) xs end;
1894 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1895 > val ces = map (Thm.cterm_of thy) (isalist2list (term_of ct));
1896 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1897 > Thm.cterm_of thy conj;
1898 val it = "(a = b & c = d) & e = f" : cterm
1901 (* f, a binary operator, is nested leftassociative *)
1902 fun foldl1 f (x::[]) = x
1903 | foldl1 f (x::x'::[]) = f (x,x')
1904 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1906 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1907 > val ces = map (Thm.cterm_of thy) (isalist2list (term_of ct));
1908 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1909 > Thm.cterm_of thy conj;
1910 val it = "a = b & c = d & e = f & g = h" : cterm
1914 (* called only once, if a Subproblem has been located in the script*)
1915 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
1916 (* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
1920 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1921 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1922 (*all stored in tac_ itms ^^^^^^^^^^*)
1923 | nxt_model_pbl tac_ _ =
1924 raise error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1925 (* run subp_rooteq.sml ''
1926 until nxt=("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1927 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1928 (last_elem o drop_last) ets'';
1929 > val mst = (last_elem o drop_last) ets'';
1930 > nxt_model_pbl mst;
1931 val it = Refine_Tacitly ["univariate","equation"] : tac
1934 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1935 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1936 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1941 writeln (oris2str pors);
1943 writeln (itms2str_ thy pits);
1944 writeln (itms2str_ thy mits);
1948 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1949 + met from fmz; assumes pos on PblObj, meth = [].*)
1950 fun complete_mod (pt, pos as (p, p_):pos') =
1951 (* val (pt, (p, _)) = (pt, p);
1952 val (pt, (p, _)) = (pt, pos);
1954 let val _= if p_ <> Pbl
1955 then writeln("###complete_mod: only impl.for Pbl, called with "^
1956 pos'2str pos) else ()
1957 val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
1959 val (dI,pI,mI) = some_spec ospec spec
1960 val mpc = (#ppc o get_met) mI
1961 val ppc = (#ppc o get_pbt) pI
1962 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1963 val pt = update_pblppc pt p pits
1964 val pt = update_metppc pt p mits
1965 in (pt, (p,Met):pos') end
1967 (*| complete_mod (pt, pos as (p, Met):pos') =
1968 raise error ("###complete_mod: only impl.for Pbl, called with "^
1971 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1972 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1973 fun all_modspec (pt, (p,_):pos') =
1974 (* val (pt, (p,_)) = ptp;
1976 let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1977 ...}) = get_obj I pt p;
1978 val thy = assoc_thy dI;
1979 val {ppc,...} = get_met mI;
1980 val mors = prep_ori fmz_ thy ppc;
1981 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1982 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1983 val pt = update_spec pt p (dI,pI,mI);
1984 in (pt, (p,Met): pos') end;
1986 (*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1987 fun is_complete_mod_ ([]: itm list) = false
1988 | is_complete_mod_ itms =
1989 foldl and_ (true, (map #3 itms));
1990 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1991 if (is_pblobj o (get_obj I pt)) p
1992 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1993 else raise error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1994 | is_complete_mod (pt, pos as (p, Met)) =
1995 if (is_pblobj o (get_obj I pt)) p
1996 then (is_complete_mod_ o (get_obj g_met pt)) p
1997 else raise error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1998 | is_complete_mod (_, pos) =
1999 raise error ("is_complete_mod called by "^pos'2str pos^
2000 " (should be Pbl or Met)");
2002 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
2003 fun is_complete_spec (pt, pos as (p,_): pos') =
2004 if (not o is_pblobj o (get_obj I pt)) p
2005 then raise error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
2006 else let val (dI,pI,mI) = get_obj g_spec pt p
2007 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
2008 (*.complete empty items in specification from origin (pbl, met ev.refined);
2009 assumes 'is_complete_mod'.*)
2010 fun complete_spec (pt, pos as (p,_): pos') =
2011 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
2012 val pt = update_spec pt p (some_spec ospec spec)
2015 fun is_complete_modspec ptp =
2016 is_complete_mod ptp andalso is_complete_spec ptp;
2021 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
2022 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
2024 let val (_,_,metID) = get_somespec' spec spec'
2026 if metID = e_metID then []
2027 else let val {prls,pre=where_,...} = get_met metID
2028 val pre = check_preconds' prls where_ meth 0
2030 val allcorrect = is_complete_mod_ meth
2031 andalso foldl and_ (true, (map #1 pre))
2032 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
2033 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
2034 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
2036 let val (_,pI,_) = get_somespec' spec spec'
2038 if pI = e_pblID then []
2039 else let val {prls,where_,cas,...} = get_pbt pI
2040 val pre = check_preconds' prls where_ probl 0
2042 val allcorrect = is_complete_mod_ probl
2043 andalso foldl and_ (true, (map #1 pre))
2044 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
2047 fun pt_form (PrfObj {form,...}) = Form form
2048 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
2049 let val (dI, pI, _) = get_somespec' spec spec'
2050 val {cas,...} = get_pbt pI
2052 NONE => Form (pblterm dI pI)
2053 | SOME t => Form (subst_atomic (mk_env probl) t)
2055 (*vvv takes the tac _generating_ the formula=result, asm ok....
2056 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
2058 if null asm then NONE else SOME asm,
2060 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
2061 let val (_,_,metID) = some_spec ospec spec
2063 if null asm then NONE else SOME asm,
2064 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
2065 -------------------------------------------------------------------------*)
2068 (*.pt_extract returns
2069 # the formula at pos
2070 # the tactic applied to this formula
2071 # the list of assumptions generated at this formula
2072 (by application of another tac to the preceding formula !)
2073 pos is assumed to come from the frontend, ie. generated by moveDown.*)
2074 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
2075 fun pt_extract (pt,([],Res)) =
2076 (* val (pt,([],Res)) = ptp;
2078 let val (f, asm) = get_obj g_result pt []
2079 in (Form f, NONE, asm) end
2082 | pt_extract (pt,(p,Res)) =
2083 (* val (pt,(p,Res)) = ptp;
2085 let val (f, asm) = get_obj g_result pt p
2086 val tac = if last_onlev pt p
2087 then if is_pblobj' pt (lev_up p)
2088 then let val (PblObj{spec=(_,pI,_),...}) =
2089 get_obj I pt (lev_up p)
2090 in if pI = e_pblID then NONE
2091 else SOME (Check_Postcond pI) end
2092 else SOME End_Trans (*WN0502 TODO for other branches*)
2093 else let val p' = lev_on p
2094 in if is_pblobj' pt p'
2095 then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
2097 in SOME (Subproblem (dI, pI)) end
2098 else if f = get_obj g_form pt p'
2099 then SOME (get_obj g_tac pt p')
2100 (*because this Frm ~~~is not on worksheet*)
2101 else SOME (Take (term2str (get_obj g_form pt p')))
2103 in (Form f, tac, asm) end
2105 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
2106 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
2107 val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
2109 let val ppobj = get_obj I pt p
2110 val f = if is_pblobj ppobj then pt_model ppobj p_
2111 else get_obj pt_form pt p
2112 val tac = g_tac ppobj
2113 in (f, SOME tac, []) end;
2116 (**. get the formula from a ctree-node:
2117 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
2118 take res from all other PrfObj's .**)
2119 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
2120 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
2121 [("headline", (p, Frm), h),
2122 ("stepform", (p, Res), r)]
2123 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
2124 [("stepform", (p, Frm), form),
2125 ("stepform", (p, Res), r)];
2127 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
2128 [("stepform", (p, Res), r)]
2130 (*assumes to take whole level, in particular hd -- for use in interSteps*)
2131 fun get_formress fs p [] = flat fs
2132 | get_formress fs p (nd::nds) =
2133 (* start with 'form+res' and continue with trying 'res' only*)
2134 get_forms (fs @ [formres p nd]) (lev_on p) nds
2135 and get_forms fs p [] = flat fs
2136 | get_forms fs p (nd::nds) =
2138 (* start again with 'form+res' ///ugly repeat with Check_elementwise
2139 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
2140 then get_forms (fs @ [formres p nd]) (lev_on p) nds
2141 (* continue with trying 'res' only*)
2142 else get_forms (fs @ [form p nd]) (lev_on p) nds;
2144 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
2145 (*WN050219 made robust against _'to' below or after Complete nodes
2146 by handling exn caused by move_dn*)
2147 (*WN0401 this functionality belongs to ctree.sml,
2148 but fetching a calc_head requires calculations defined in modspec.sml
2149 transfer to ME/me.sml !!!
2150 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
2151 is returned !!!!!!!!!!!!!
2153 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
2154 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
2155 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
2159 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
2163 | eq_pos' _ _ = false;
2165 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
2166 total ordering Position#compareTo(Position p) in the java-code
2167 val get_interval = fn
2168 : pos' -> : from is "move_up 1st-element" to return
2169 pos' -> : to the last element to be returned; from < to
2170 int -> : level: 0 gets the flattest sub-tree possible
2171 >999 gets the deepest sub-tree possible
2173 (pos' * : of the formula
2174 Term.term) : the formula
2177 fun get_interval from to level pt =
2178 (* val (from,level) = (f,lev);
2179 val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
2181 let fun get_inter c (from:pos') (to:pos') lev pt =
2182 (* val (c, from, to, lev) = ([], from, to, level);
2183 ------for recursion.......
2184 val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
2186 if eq_pos' from to orelse from = ([],Res)
2187 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
2188 if 'to' has values NOT generated by move_dn, see systest/me.sml
2189 TODO.WN0501: introduce an order on pos' and check "from > to"..
2190 ...there is an order in Java!
2191 WN051224 the hack got worse with returning term instead ptform*)
2192 then let val (f,_,_) = pt_extract (pt, from)
2194 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2195 | Form t => c @ [(from, t)]
2198 if lev < lev_of from
2199 then (get_inter c (move_dn [] pt from) to lev pt)
2200 handle (PTREE _(*from move_dn too far*)) => c
2201 else let val (f,_,_) = pt_extract (pt, from)
2202 val term = case f of
2203 ModSpec (_,_,headline,_,_,_)=> headline
2205 in (get_inter (c @ [(from, term)])
2206 (move_dn [] pt from) to lev pt)
2207 handle (PTREE _(*from move_dn too far*))
2208 => c @ [(from, term)] end
2209 in get_inter [] from to level pt end;
2212 fun posform2str (pos:pos', form) =
2213 "("^ pos'2str pos ^", "^
2215 Form f => term2str f
2216 | ModSpec c => term2str (#3 c(*the headline*)))
2218 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2219 (map posform2str)) pfs;
2220 fun posterm2str (pos:pos', t) =
2221 "("^ pos'2str pos ^", "^term2str t^")";
2222 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2223 (map posterm2str)) pfs;
2226 (*WN050225 omits the last step, if pt is incomplete*)
2228 writeln (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
2230 (*.get a calchead from a PblObj-node in the ctree;
2231 preconditions must be calculated.*)
2232 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
2233 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
2235 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2236 val pre = check_preconds (assoc_thy"Isac.thy") prls where_ probl
2237 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
2238 | get_ocalhd (pt, pos' as (p,Met):pos') =
2239 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2242 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2243 val pre = check_preconds (assoc_thy"Isac.thy") prls pre meth
2244 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
2246 (*.at the activeFormula set the Model, the Guard and the Specification
2247 to empty and return a CalcHead;
2248 the 'origin' remains (for reconstructing all that).*)
2249 fun reset_calchead (pt, pos' as (p,_):pos') =
2250 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
2251 val pt = update_pbl pt p []
2252 val pt = update_met pt p []
2253 val pt = update_spec pt p e_spec
2254 in (pt, (p,Pbl):pos') end;
2256 (*---------------------------------------------------------------------*)
2260 (*---------------------------------------------------------------------*)