intermed. context integration: Isac compiles.
1 (* Title: Specify-phase: specifying and modeling a problem or a subproblem. The
2 most important types are declared in mstools.sml.
3 Author: Walther Neuper 991122
4 (c) due to copyright terms
6 12345678901234567890123456789012345678901234567890123456789012345678901234567890
7 10 20 30 40 50 60 70 80
10 (* TODO interne Funktionen aus sig entfernen *)
13 datatype additm = Add of SpecifyTools.itm | Err of string
14 val all_dsc_in : SpecifyTools.itm_ list -> Term.term list
15 val all_modspec : ptree * pos' -> ptree * pos'
16 datatype appl = Appl of tac_ | Notappl of string
20 SpecifyTools.ori list ->
21 SpecifyTools.itm list ->
22 (string * (Term.term * Term.term)) list -> cterm' -> additm
25 val chk_vars : term ppc -> string * Term.term list
27 theory -> int * term list * term list -> term
29 theory -> term list * term list -> term list
30 val complete_metitms :
31 SpecifyTools.ori list ->
32 SpecifyTools.itm list ->
33 SpecifyTools.itm list -> pat list -> SpecifyTools.itm list
34 val complete_mod_ : ori list * pat list * pat list * itm list ->
36 val complete_mod : ptree * pos' -> ptree * (pos * pos_)
37 val complete_spec : ptree * pos' -> ptree * pos'
39 pat list -> preori list -> pat -> preori
40 val e_calcstate : calcstate
41 val e_calcstate' : calcstate'
42 val eq1 : ''a -> 'b * (''a * 'c) -> bool
44 ''a -> Term.term -> 'b * 'c * 'd * ''a * SpecifyTools.itm_ -> bool
45 val eq4 : ''a -> 'b * ''a list * 'c * 'd * 'e -> bool
47 'a * 'b * 'c * 'd * SpecifyTools.itm_ ->
48 'e * 'f * 'g * Term.term * 'h -> bool
49 val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool
50 val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool
51 val f_mout : theory -> mout -> Term.term
53 SpecifyTools.ori list ->
54 SpecifyTools.itm list -> SpecifyTools.ori list
56 SpecifyTools.ori list ->
57 ('a * (Term.term * 'b)) list -> SpecifyTools.ori list
58 val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
59 val foldr1 : ('a * 'a -> 'a) -> 'a list -> 'a
60 val form : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
61 val formres : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
62 val gen_ins' : ('a * 'a -> bool) -> 'a * 'a list -> 'a list
64 (string * (pos * pos_) * Term.term) list list ->
65 pos -> ptree list -> (string * (pos * pos_) * Term.term) list
67 (string * (pos * pos_) * Term.term) list list ->
68 posel list -> ptree list -> (string * (pos * pos_) * Term.term) list
69 val get_interval : pos' -> pos' -> int -> ptree -> (pos' * term) list
70 val get_ocalhd : ptree * pos' -> ocalhd
71 val get_spec_form : tac_ -> pos' -> ptree -> mout
74 SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'
75 val getr_ct : theory -> SpecifyTools.ori -> string * cterm'
76 val has_list_type : Term.term -> bool
77 val header : pos_ -> pblID -> metID -> pblmet
80 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
81 SpecifyTools.itm list -> SpecifyTools.itm list
83 SpecifyTools.itm -> SpecifyTools.itm list -> SpecifyTools.itm list
84 val is_complete_mod : ptree * pos' -> bool
85 val is_complete_mod_ : SpecifyTools.itm list -> bool
86 val is_complete_modspec : ptree * pos' -> bool
87 val is_complete_spec : ptree * pos' -> bool
88 val is_copy_named : 'a * ('b * Term.term) -> bool
89 val is_copy_named_idstr : string -> bool
90 val is_error : SpecifyTools.itm_ -> bool
91 val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
95 SpecifyTools.ori list ->
96 Term.term -> string * SpecifyTools.ori * Term.term list
97 val is_list_type : Term.typ -> bool
100 SpecifyTools.itm list ->
103 ('a * (Term.term * Term.term)) list -> string * SpecifyTools.itm
104 val is_parsed : SpecifyTools.itm_ -> bool
105 val is_untouched : SpecifyTools.itm -> bool
110 (int list * string * Term.term * Term.term list) list ->
111 (int list * string * Term.term * Term.term list) list
113 theory -> pat list -> Term.term list -> SpecifyTools.ori list
114 val maxl : int list -> int
115 val match_ags_msg : string list -> Term.term -> Term.term list -> unit
116 val memI : ''a list -> ''a -> bool
117 val mk_additem : string -> cterm' -> tac
118 val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
120 theory -> pat -> Term.term -> SpecifyTools.preori option
123 SpecifyTools.ori list ->
124 (string * (Term.term * 'a)) list ->
125 SpecifyTools.itm list -> (string * cterm') option
126 val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
130 SpecifyTools.ori list ->
132 SpecifyTools.itm list * SpecifyTools.itm list ->
133 (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->
135 val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'
136 val nxt_specif_additem :
137 string -> cterm' -> ptree * (int list * pos_) -> calcstate'
138 val nxt_specify_init_calc : fmz -> calcstate
139 val ocalhd_complete :
140 SpecifyTools.itm list ->
141 (bool * Term.term) list -> domID * pblID * metID -> bool
143 pat list -> ori -> itm
147 Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
150 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
151 SpecifyTools.itm list ->
152 (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
153 val parse_ok : SpecifyTools.itm_ list -> bool
154 val posform2str : pos' * ptform -> string
155 val posforms2str : (pos' * ptform) list -> string
156 val posterms2str : (pos' * term) list -> string (*tests only*)
157 val ppc135list : 'a SpecifyTools.ppc -> 'a list
158 val ppc2list : 'a SpecifyTools.ppc -> 'a list
160 ptree * (int list * pos_) ->
161 ptform * tac option * Term.term list
162 val pt_form : ppobj -> ptform
163 val pt_model : ppobj -> pos_ -> ptform
164 val reset_calchead : ptree * pos' -> ptree * pos'
168 Term.term * Term.term list ->
169 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
170 -> string * SpecifyTools.ori * Term.term list
175 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
176 -> string * SpecifyTools.ori * Term.term list
178 int -> SpecifyTools.itm list -> SpecifyTools.itm option
179 val show_pt : ptree -> unit
180 val some_spec : spec -> spec -> spec
186 (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *
188 val specify_additem :
194 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
195 val tag_form : theory -> term * term -> term
196 val test_types : theory -> Term.term * Term.term list -> string
197 val typeless : Term.term -> Term.term
198 val unbound_ppc : term SpecifyTools.ppc -> Term.term list
199 val vals_of_oris : SpecifyTools.ori list -> Term.term list
200 val variants_in : Term.term list -> int
201 val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
202 val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
209 (*---------------------------------------------------------------------
210 structure CalcHead (**): CALC_HEAD(**) =
213 ---------------------------------------------------------------------*)
217 (*.the state wich is stored after each step of calculation; it contains
218 the calc-state and a list of [tac,istate](="tacis") to be applied next.
219 the last_elem tacis is the first to apply to the calc-state and
220 the (only) one shown to the front-end as the 'proposed tac'.
221 the calc-state resulting from the application of tacis is not stored,
222 because the tacis hold enough information for efficiently rebuilding
223 this state just by "fun generate ".*)
225 (ptree * pos') * (*the calc-state to which the tacis could be applied*)
226 (taci list); (*ev. several (hidden) steps;
227 in REVERSE order: first tac_ to apply is last_elem*)
228 val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
230 (*the state used during one calculation within the mathengine; it contains
231 a list of [tac,istate](="tacis") which generated the the calc-state;
232 while this state's tacis are extended by each (internal) step,
233 the calc-state is used for creating new nodes in the calc-tree
234 (eg. applicable_in requires several particular nodes of the calc-tree)
235 and then replaced by the the newly created;
236 on leave of the mathengine the resuing calc-state is dropped anyway,
237 because the tacis hold enought information for efficiently rebuilding
238 this state just by "fun generate ".*)
240 taci list * (*cas. several (hidden) steps;
241 in REVERSE order: first tac_ to apply is last_elem*)
242 pos' list * (*a "continuous" sequence of pos',
243 deleted by application of taci list*)
244 (ptree * pos'); (*the calc-state resulting from the application of tacis*)
245 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
247 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
248 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
249 | f_mout thy _ = error "f_mout: not called with formula";
252 (*.is the calchead complete ?.*)
253 fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
254 foldl and_ (true, map #3 its) andalso
255 foldl and_ (true, map #1 pre) andalso
256 dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
259 (* make a term 'typeless' for comparing with another 'typeless' term;
260 'type-less' usually is illtyped *)
261 fun typeless (Const(s,_)) = (Const(s,e_type))
262 | typeless (Free(s,_)) = (Free(s,e_type))
263 | typeless (Var(n,_)) = (Var(n,e_type))
264 | typeless (Bound i) = (Bound i)
265 | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
266 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
268 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
269 > val (_,t1) = split_dsc_t hs (term_of ct);
270 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
271 > val (_,t2) = split_dsc_t hs (term_of ct);
272 > typeless t1 = typeless t2;
278 (*.to an input (d,ts) find the according ori and insert the ts.*)
279 (*WN.11.03: + dont take first inter<>[]*)
280 fun seek_oridts thy sel (d,ts) [] =
281 ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
282 (comp_dts thy (d,ts))) ^
283 "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
285 | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
286 if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
289 (id,vat,sel,d, inter op = ts ts'):ori,
291 else ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
292 (comp_dts thy (d,ts))) ^ " not for " ^ sel,
295 else seek_oridts thy sel (d,ts) oris;
297 (*.to an input (_,ts) find the according ori and insert the ts.*)
298 fun seek_orits thy sel ts [] =
299 ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
300 (thy2ctxt thy))) ts) ^
301 "') not found in oris (typed)", e_ori_, [])
302 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
303 if sel = sel' andalso (inter op = ts ts') <> []
306 (id,vat,sel,d, inter op = ts ts'):ori,
308 else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
309 (thy2ctxt thy)))) ts)
313 else seek_orits thy sel ts oris;
315 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
316 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
317 uncaught exception TYPE
318 > seek_orits thy sel ts [];
319 uncaught exception TYPE
322 (*find_first item with #1 equal to id*)
323 fun seek_ppc id [] = NONE
324 | seek_ppc id (p::(ppc:itm list)) =
325 if id = #1 p then SOME p else seek_ppc id ppc;
329 (*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
332 datatype appl = Appl of tac_ | Notappl of string;
334 fun ppc2list ({Given=gis,Where=whs,Find=fis,
335 With=wis,Relate=res}: 'a ppc) =
336 gis @ whs @ fis @ wis @ res;
337 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
343 (* get the number of variants in a problem in 'original',
344 assumes equal descriptions in immediate sequence *)
346 let fun eq(x,y) = head_of x = head_of y;
347 fun cnt eq [] y n = ([n],[])
348 | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
350 fun coll eq xs [] = xs
351 | coll eq xs (y::ys) =
352 let val (n,ys') = cnt eq (y::ys) y 0;
353 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
354 val vts = subtract op = [1] (distinct (coll eq [] ts));
355 in case vts of [] => 1 | [n] => n
356 | _ => error "different variants in formalization" end;
358 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
359 val it = ([3],[4,5,5,5,5,5]) : int list * int list
360 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
361 val it = [1,3,1,5] : int list
364 fun is_list_type (Type("List.list",_)) = true
365 | is_list_type _ = false;
366 (* fun destr (Type(str,sort)) = (str,sort);
367 > val (SOME ct) = parse thy "lll::real list";
368 > val ty = (#T o rep_cterm) ct;
372 val it = ("List.list",["RealDef.real"]) : string * typ list
373 > atomty ((#t o rep_cterm) ct);
375 *** Free ( lll, real list)
378 > val (SOME ct) = parse thy "[lll::real]";
379 > val ty = (#T o rep_cterm) ct;
383 val it = ("List.list",["'a"]) : string * typ list
384 > atomty ((#t o rep_cterm) ct);
386 *** Const ( List.list.Cons, [real, real list] => real list)
387 *** Free ( lll, real)
388 *** Const ( List.list.Nil, real list)
390 > val (SOME ct) = parse thy "lll";
391 > val ty = (#T o rep_cterm) ct;
393 val it = false : bool *)
396 fun has_list_type (Free(_,T)) = is_list_type T
397 | has_list_type _ = false;
399 > val (SOME ct) = parse thy "lll::real list";
400 > has_list_type (term_of ct);
402 > val (SOME ct) = parse thy "[lll::real]";
403 > has_list_type (term_of ct);
404 val it = false : bool *)
406 fun is_parsed (Syn _) = false
407 | is_parsed _ = true;
408 fun parse_ok its = foldl and_ (true, map is_parsed its);
410 fun all_dsc_in itm_s =
412 fun d_in (Cor ((d,_),_)) = [d]
415 | d_in (Inc ((d,_),_)) = [d]
416 | d_in (Sup (d,_)) = [d]
417 | d_in (Mis (d,_)) = [d];
418 in (flat o (map d_in)) itm_s end;
421 fun is_Syn (Syn _) = true
422 | is_Syn (Typ _) = true
425 fun is_error (Cor (_,ts)) = false
426 | is_error (Sup (_,ts)) = false
427 | is_error (Inc (_,ts)) = false
428 | is_error (Mis (_,ts)) = false
432 fun ct_in (Syn (c)) = c
433 | ct_in (Typ (c)) = c
434 | ct_in _ = error "ct_in called for Cor .. Sup";
437 (*#############################################################*)
438 (*#############################################################*)
439 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
442 (* testdaten besorgen:
443 use"test-coil-kernel.sml";
444 val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
449 variant V: oris union ppc => int, id ID: oris union ppc => int
452 EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
455 @vt = max sum(i : ppc) V i
461 > ((vts_cnt (vts_in itms))) itms;
466 > val vts = vts_in itms;
467 val vts = [1,2,3] : int list
468 > val nvts = vts_cnt vts itms;
469 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
470 > val mx = max2 nvts;
471 val mx = (3,7) : int * int
472 > val v = max_vt itms;
474 --------------------------
478 (*.get the first term in ts from ori.*)
479 (* val (_,_,fd,d,ts) = hd miss;
481 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
482 (fd, (Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy))) o
483 (comp_dts thy)) (d,[hd ts]) : cterm');
484 (* val t = comp_dts thy (d,[hd ts]);
487 (* get a term from ori, notyet input in itm.
488 the term from ori is thrown back to a string in order to reuse
489 machinery for immediate input by the user. *)
490 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
491 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
493 (d, subtract op = (ts_in itm_) ts) : cterm');
494 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
495 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
497 (d, subtract op = (ts_in itm_) ts) : cterm');
499 (* in FE dsc, not dat: this is in itms ...*)
500 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
501 | is_untouched _ = false;
504 (* select an item in oris, notyet input in itms
505 (precondition: in itms are only Cor, Sup, Inc) *)
508 | x mem (y :: ys) = x = y orelse x mem ys;
510 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
512 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
513 fun is_elem itms (f,(d,t)) =
514 case find_first (test_d d) itms of
515 SOME _ => true | NONE => false;
516 in case filter_out (is_elem itms) pbt of
517 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
521 ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
522 comp_dts thy) (d, []) : cterm')
525 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
527 | nxt_add thy oris pbt itms =
529 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
530 andalso (#3 ori) <>"#undef";
531 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
532 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
533 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
534 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
535 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
536 | false_and_not_Sup (i,v,false,f, _) = true
537 | false_and_not_Sup _ = false;
539 val v = if itms = [] then 1 else max_vt itms;
540 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
541 val vits = if v = 0 then itms (*because of dsc without dat*)
542 else filter (testi_vt v) itms; (*itms..vat*)
543 val icl = filter false_and_not_Sup vits; (* incomplete *)
545 then case filter_out (test_id (map #1 vits)) vors of
547 (* val miss = filter_out (test_id (map #1 vits)) vors;
549 | miss => SOME (getr_ct thy (hd miss))
551 case find_first (test_subset (hd icl)) vors of
552 (* val SOME ori = find_first (test_subset (hd icl)) vors;
554 NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
555 | SOME ori => SOME (geti_ct thy ori (hd icl))
561 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
562 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
563 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
564 | mk_delete thy str _ =
565 error ("mk_delete: called with field '"^str^"'");
566 fun mk_additem "#Given" ct = Add_Given ct
567 | mk_additem "#Find" ct = Add_Find ct
568 | mk_additem "#Relate"ct = Add_Relation ct
570 error ("mk_additem: called with field '"^str^"'");
573 (* determine the next step of specification;
574 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
575 eg. in rootpbl 'no_met':
577 preok predicates are _all_ ok (and problem matches completely)
578 oris immediately from formalization
579 (dI',pI',mI') specification coming from author/parent-problem
580 (pbl, item lists specified by user
581 met) -"-, tacitly completed by copy_probl
582 (dI,pI,mI) specification explicitly done by the user
583 (pbt, mpc) problem type, guard of method
585 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
586 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
587 ((*tracing"### nxt_spec Pbl";*)
588 if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
589 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
590 else case find_first (is_error o #5) (pbl:itm list) of
591 SOME (_, _, _, fd, itm_) =>
593 (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
595 ((*tracing"### nxt_spec is_error NONE";*)
596 case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
598 SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
599 (Pbl, mk_additem fd ct'))
600 | NONE => (*pbl-items complete*)
601 if not preok then (Pbl, Refine_Problem pI')
603 if dI = e_domID then (Pbl, Specify_Theory dI')
604 else if pI = e_pblID then (Pbl, Specify_Problem pI')
605 else if mI = e_metID then (Pbl, Specify_Method mI')
607 case find_first (is_error o #5) met of
608 SOME (_,_,_,fd,itm_) =>
609 (Met, mk_delete (assoc_thy dI) fd itm_)
611 (case nxt_add (assoc_thy dI) oris mpc met of
612 SOME (fd,ct') => (*30.8.01: pre?!?*)
613 (Met, mk_additem fd ct')
615 ((*Solv 3.4.00*)Met, Apply_Method mI))))
617 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
618 ((*tracing"### nxt_spec Met"; *)
619 case find_first (is_error o #5) met of
620 SOME (_,_,_,fd,itm_) =>
621 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
623 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
624 SOME (fd,ct') => (Met, mk_additem fd ct')
626 ((*tracing"### nxt_spec Met: nxt_add NONE";*)
627 if dI = e_domID then (Met, Specify_Theory dI')
628 else if pI = e_pblID then (Met, Specify_Problem pI')
629 else if not preok then (Met, Specify_Method mI)
630 else (Met, Apply_Method mI)));
633 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
634 (2,[2],true,"#Find",Syn("empty"))];
637 fun is_field_correct sel d dscpbt =
638 case assoc (dscpbt, sel) of
640 | SOME ds => member op = ds d;
642 (*. update the itm_ already input, all..from ori .*)
643 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
645 fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) =
647 val ts' = union op = (ts_in itm_) ts;
648 val pval = pbl_ids' thy d ts'
649 (*WN.9.5.03: FIXXXME [#0, epsilon]
650 here would upd_penv be called for [#0, epsilon] etc. *)
651 val complete = if eq_set op = (ts', all) then true else false;
654 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
655 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
656 | (Syn c) => error ("ori_2itm wants to overwrite "^c)
657 | (Typ c) => error ("ori_2itm wants to overwrite "^c)
658 | (Inc _) => if complete
659 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
660 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
661 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
662 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
663 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
664 (* 28.1.00: not completely clear ---^^^ etc.*)
665 (* 4.9.01: Mis just copied---vvv *)
666 | (Mis _) => if complete
667 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
668 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
672 fun eq1 d (_,(d',_)) = (d = d');
673 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
676 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
677 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
678 pval: value for problem-environment _NOT_ checked for 'inter' --
679 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
680 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
681 (*. is_input ori itms <=>
682 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
683 (2) ori(ts) subset itm(ts) --- Err "already input"
684 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
685 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
686 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
688 fun is_notyet_input thy (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
689 case find_first (eq1 d) pbt of
690 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
691 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
693 (case find_first (eq3 f d) itms of
694 SOME (_,_,_,_,itm_) =>
696 val ts' = inter op = (ts_in itm_) ts;
697 in if subset op = (ts, ts')
699 map (Print_Mode.setmp [] (Syntax.string_of_term
700 (thy2ctxt thy)))) ts') ^
701 " already input", e_itm) (*2*)
703 ori_2itm thy itm_ pid all (i,v,f,d,
704 subtract op = ts' ts)) (*3,4*)
706 | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
707 pid all (i,v,f,d,ts)) (*1*)
709 | NONE => ("", ori_2itm thy (Sup (d,ts))
710 e_term all (i,v,f,d,ts));
712 fun test_types thy (d,ts) =
714 (*val s = !show_types; val _ = show_types:= true;*)
715 val opt = (try (comp_dts thy)) (d,ts);
716 val msg = case opt of
718 | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) d) ^
720 ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
721 (thy2ctxt thy)))) ts)
723 (*val _ = show_types:= s*)
728 fun maxl [] = error "maxl of []"
731 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
735 (*. is the input term t known in oris ?
736 give feedback on all(?) strange input;
737 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
738 (*WN.11.03: from lists*)
739 fun is_known thy sel ori t =
740 (* val (ori,t)=(oris,term_of ct);
743 val _ = tracing ("RM is_known: t=" ^ term2str t);
744 val ots = (distinct o flat o (map #5)) (ori:ori list);
745 val oids = ((map (fst o dest_Free)) o distinct o
746 flat o (map vars)) ots;
747 val (d,ts(*,pval*)) = split_dts thy t;
748 val ids = map (fst o dest_Free)
749 ((distinct o (flat o (map vars))) ts);
750 in if (subtract op = oids ids) <> []
751 then (("identifiers "^(strs2str' (subtract op = oids ids))^
752 " not in example"), e_ori_, [])
756 if not (subset op = (map typeless ts, map typeless ots))
759 (map (Print_Mode.setmp [] (Syntax.string_of_term
760 (thy2ctxt thy))))) ts)^
761 "' not in example (typeless)"), e_ori_, [])
762 else (case seek_orits thy sel ts ori of
763 ("", ori_ as (_,_,_,d,ts), all) =>
764 (case test_types thy (d,ts) of
765 "" => ("", ori_, all)
766 | msg => (msg, e_ori_, []))
767 | (msg,_,_) => (msg, e_ori_, []))
769 if member op = (map #4 ori) d
770 then seek_oridts thy sel (d,ts) ori
771 else ((Print_Mode.setmp [] (Syntax.string_of_term
773 " not in example", (0, [], sel, d, ts), [])
777 (*. for return-value of appl_add .*)
780 | Err of string; (*error-message*)
783 (** add an item to the model; check wrt. oris and pbt **)
784 (* in contrary to oris<>[] below, this part handles user-input
785 extremely acceptive, i.e. accept input instead error-msg *)
786 fun appl_add thy sel ([]:ori list) ppc pbt ct' =
787 (* val (ppc,pbt,ct',env) = (pbl, (#ppc o get_pbt) cpI, ct, []:envv);
788 !!!! 28.8.01: env tested _minimally_ !!!
791 val i = 1 + (if ppc=[] then 0 else maxl (map #1 ppc));
792 in case parse thy ct' of (*should be done in applicable_in 4.00.FIXME*)
793 NONE => Add (i,[],false,sel,Syn ct')
794 (* val (SOME ct) = parse thy ct';
798 val (d,ts(*,pval*)) = split_dts thy (term_of ct);
800 then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*)))
803 (case find_first (eq1 d) pbt of
804 NONE => Add (i,[],true,sel,Sup ((d,ts)))
806 (* val SOME (f,(_,id)) = find_first (eq1 d) pbt;
809 fun eq2 d ((i,_,_,_,itm_):itm) =
810 (d = (d_in itm_)) andalso i<>0;
811 in case find_first (eq2 d) ppc of
812 NONE => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*)
814 | SOME (i',_,_,_,itm_) =>
815 (* val SOME (i',_,_,_,itm_) = find_first (eq2 d) ppc;
816 val NONE = find_first (eq2 d) ppc;
819 then let val ts = union op = ts (ts_in itm_)
820 in Add (if ts_in itm_ = [] then i else i',
821 [],true,f,Cor ((d, ts), (id, (*pval*)
824 else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*)
831 (*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*)
832 | appl_add thy sel oris ppc pbt (*only for upd_envv*) str =
833 case parse thy str of
834 NONE => Err ("syntax error in " ^ str)
835 | SOME t => case is_known thy sel oris (term_of t) of
837 (case is_notyet_input thy ppc all ori' pbt of
839 | (msg, _) => Err msg)
840 | (msg, _, _) => Err msg;
842 > val (msg,itm) = is_notyet_input thy ppc all ori';
843 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
845 > val ts = ts_in itm_;
849 (** make oris from args of the stac SubProblem and from pbt **)
851 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
852 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
853 fun is_copy_named_idstr str =
854 case (rev o Symbol.explode) str of
855 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
856 "is_copy_named_idstr: " ^ str ^ " T"); true)
857 | _ => (tracing ((strs2str o (rev o Symbol.explode))
858 "is_copy_named_idstr: " ^ str ^ " F"); false);
859 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
861 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
862 fun is_copy_named_generating_idstr str =
863 if is_copy_named_idstr str
864 then case (rev o Symbol.explode) str of
865 "'"::"'"::"'"::_ => false
868 fun is_copy_named_generating (_, (_, t)) =
869 (is_copy_named_generating_idstr o free2str) t;
871 (*.split type-wrapper from scr-arg and build part of an ori;
872 an type-error is reported immediately, raises an exn,
873 subsequent handling of exn provides 2nd part of error message.*)
874 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
875 (* val (thy, (str, (dsc, _)), (ty $ var)) =
878 (cterm_of thy (dsc $ var);(*type check*)
879 SOME ((([1], str, dsc, (*[var]*)
880 split_dts' (dsc, var))): preori)(*:ori without leading #*))
881 handle e as TYPE _ =>
882 (tracing (dashs 70 ^ "\n"
883 ^"*** ERROR while creating the items for the model of the ->problem\n"
884 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
885 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
886 ^"*** description: "^(term_detail2str dsc)
887 ^"*** value: "^(term_detail2str var)
888 ^"*** typeconstructor in script: "^(term_detail2str ty)
889 ^"*** checked by theory: "^(theory2str thy)^"\n"
891 (*OldGoals.print_exn e; raises exn again*)
892 writeln (PolyML.makestring e);
894 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
897 (*.match each pat of the model-pattern with an actual argument;
898 precondition: copy-named vars are filtered out.*)
899 fun matc thy ([]:pat list) _ (oris:preori list) = oris
900 | matc thy pbt [] _ =
902 error ("actual arg(s) missing for '"^pats2str pbt
903 ^"' i.e. should be 'copy-named' by '*_._'"))
904 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
905 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
906 (thy, pbt', ags, []);
908 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
909 (thy, pbt, ags, (oris @ [ori]));
911 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
912 else(*..del?*) let val opt = mtc thy p a;
914 (* val SOME ori = mtc thy p a;
916 SOME ori => matc thy pbt ags (oris @ [ori])
917 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
919 (* run subp-rooteq.sml until Init_Proof before ...
920 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
921 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
923 other vars as in mtc ..
924 > matc thy (drop_last pbt) ags [];
925 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
928 (* generate a new variable "x_i" name from a related given one "x"
929 by use of oris relating "v_i_" (is_copy_named!) to "v_"
930 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
932 (* generate a new variable "x_i" name from a related given one "x"
933 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
934 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
935 but leave is_copy_named_generating as is, e.t. ss''' *)
936 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
937 (if is_copy_named_generating p
938 then (*WN051014 kept strange old code ...*)
939 let fun sel (_,_,d,ts) = comp_ts (d, ts)
940 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
941 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
942 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
943 val vals = map sel oris
944 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
945 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
946 else ([1], field, dsc, [t])
948 handle _ => error ("cpy_nam: for "^(term2str t));
950 (*.match the actual arguments of a SubProblem with a model-pattern
951 and create an ori list (in root-pbl created from formalization).
952 expects ags:pats = 1:1, while copy-named are filtered out of pats;
953 if no 1:1 the exn raised by matc/mtc and handled at call.
954 copy-named pats are appended in order to get them into the model-items.*)
955 fun match_ags thy (pbt:pat list) ags =
956 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
957 val pbt' = filter_out is_copy_named pbt;
958 val cy = filter is_copy_named pbt;
959 val oris' = matc thy pbt' ags [];
960 val cy' = map (cpy_nam pbt' oris') cy;
961 val ors = add_id (oris' @ cy');
962 (*appended in order to get ^^^^^ into the model-items*)
963 in (map flattup ors):ori list end;
965 (*.report part of the error-msg which is not available in match_args.*)
966 fun match_ags_msg pI stac ags =
967 let (*val s = !show_types
968 val _ = show_types:= true*)
969 val pats = (#ppc o get_pbt) pI
970 val msg = (dots 70^"\n"
971 ^"*** problem "^strs2str pI^" has the ...\n"
972 ^"*** model-pattern "^pats2str pats^"\n"
973 ^"*** stac '"^term2str stac^"' has the ...\n"
974 ^"*** arg-list "^terms2str ags^"\n"
976 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
977 (*val _ = show_types:= s*)
981 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
982 fun vars_of_pbl_ pbl_ =
983 let fun var_of_pbl_ (gfr,(dsc,t)) = t
984 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
985 fun vars_of_pbl_' pbl_ =
986 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
987 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
989 fun overwrite_ppc thy itm ppc =
991 fun repl ppc' (_,_,_,_,itm_) [] =
992 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
994 | repl ppc' itm (p::ppc) =
995 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
996 else repl (ppc' @ [p]) itm ppc
997 in repl [] itm ppc end;
999 (*10.3.00: insert the already compiled itm into model;
1000 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
1003 fun insert_ppc thy itm ppc =
1005 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
1006 | eq_untouched _ _ = false;
1009 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
1010 case seek_ppc (#1 itm) ppc of
1011 (* val SOME xxx = seek_ppc (#1 itm) ppc;
1013 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
1014 overwrite_ppc thy itm ppc
1015 | NONE => (ppc @ [itm]));
1016 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
1018 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
1019 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
1021 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
1022 (d_in itm_) = (d_in iitm_);
1023 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
1024 handles superfluous items carelessly*)
1025 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
1027 > gen_ins' eee (4,[1,3,5,7]);
1028 val it = [1, 3, 5, 7, 4] : int list*)
1031 (*. output the headline to a ppc .*)
1032 fun header p_ pI mI =
1033 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1035 | pos => error ("header called with "^ pos_2str pos);
1038 fun specify_additem sel (ct,_) (p,Met) c pt =
1040 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1041 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1042 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1043 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1044 val cpI = if pI = e_pblID then pI' else pI;
1045 val cmI = if mI = e_metID then mI' else mI;
1046 val {ppc,pre,prls,...} = get_met cmI
1047 in case appl_add thy sel oris met ppc ct of
1048 Add itm (*..union old input *) =>
1049 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1051 val met' = insert_ppc thy itm met;
1052 (*val pt' = update_met pt p met';*)
1053 val ((p,Met),_,_,pt') =
1054 generate1 thy (case sel of
1055 "#Given" => Add_Given' (ct, met')
1056 | "#Find" => Add_Find' (ct, met')
1057 | "#Relate"=> Add_Relation'(ct, met'))
1058 (Uistate, e_ctxt) (p,Met) pt
1059 val pre' = check_preconds thy prls pre met'
1060 val pb = foldl and_ (true, map fst pre')
1061 (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
1063 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1064 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1065 in ((p,p_), ((p,p_),Uistate),
1066 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1067 (Method cmI, itms2itemppc thy met' pre'))),
1070 let val pre' = check_preconds thy prls pre met
1071 val pb = foldl and_ (true, map fst pre')
1072 (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
1074 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1075 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1076 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1080 | specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1082 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1083 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1084 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1085 val cpI = if pI = e_pblID then pI' else pI;
1086 val cmI = if mI = e_metID then mI' else mI;
1087 val {ppc,where_,prls,...} = get_pbt cpI;
1088 in case appl_add thy sel oris pbl ppc ct of
1089 Add itm (*..union old input *) =>
1090 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1093 (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
1094 val pbl' = insert_ppc thy itm pbl
1095 val ((p,Pbl),_,_,pt') =
1096 generate1 thy (case sel of
1097 "#Given" => Add_Given' (ct, pbl')
1098 | "#Find" => Add_Find' (ct, pbl')
1099 | "#Relate"=> Add_Relation'(ct, pbl'))
1100 (Uistate, e_ctxt) (p,Pbl) pt
1101 val pre = check_preconds thy prls where_ pbl'
1102 val pb = foldl and_ (true, map fst pre)
1103 (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
1105 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1106 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1107 val ppc = if p_= Pbl then pbl' else met;
1108 in ((p,p_), ((p,p_),Uistate),
1109 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1111 itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1114 let val pre = check_preconds thy prls where_ pbl
1115 val pb = foldl and_ (true, map fst pre)
1116 (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
1118 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1119 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1120 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1122 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1123 val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1127 val (msg,itm) = appl_add thy sel oris ppc ct;
1128 val (Cor(d,ts)) = #5 itm;
1135 (* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1136 specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1138 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1139 let (* either """"""""""""""" all empty or complete *)
1140 val thy = assoc_thy dI';
1141 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1142 else prep_ori fmz thy ((#ppc o get_pbt) pI');
1143 val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
1144 (oris,(dI',pI',mI'),e_term);
1145 val {ppc,prls,where_,...} = get_pbt pI'
1146 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1147 val pt = update_pbl pt [] pbl;
1148 val pre = check_preconds thy prls where_ pbl
1149 val pb = foldl and_ (true, map fst pre)*)
1150 val (pbl, pre, pb) = ([], [], false)
1153 (([],Pbl), (([],Pbl),Uistate),
1154 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1155 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1156 Refine_Tacitly pI', Safe,pt)
1158 (([],Pbl), (([],Pbl),Uistate),
1159 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1160 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1164 (*ONLY for STARTING modeling phase*)
1165 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1166 let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
1168 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
1170 val thy' = if dI = e_domID then dI' else dI
1171 val thy = assoc_thy thy'
1172 val {ppc,prls,where_,...} = get_pbt pI'
1173 val pre = check_preconds thy prls where_ pbl
1174 val pb = foldl and_ (true, map fst pre)
1175 val ((p,_),_,_,pt) =
1176 generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
1177 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1178 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1179 in ((p,Pbl), ((p,p_),Uistate),
1180 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1181 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1184 (*. called only if no_met is specified .*)
1185 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1186 let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
1188 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
1190 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1191 (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
1192 (*val pt = update_pbl pt p pbl;
1193 val pt = update_orispec pt p
1194 (string_of_thy thy, pIre,
1195 if length met = 0 then e_metID else hd met);*)
1196 val (domID, metID) = (string_of_thy thy,
1197 if length met = 0 then e_metID else hd met)
1198 val ((p,_),_,_,pt) =
1199 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1200 (Uistate, e_ctxt) pos pt
1201 (*val pre = check_preconds thy prls where_ pbl
1202 val pb = foldl and_ (true, map fst pre)*)
1203 val (pbl, pre, pb) = ([], [], false)
1204 in ((p,Pbl), (pos,Uistate),
1205 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1206 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1207 Model_Problem, Safe, pt) end
1209 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1210 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
1211 (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1212 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1213 Model_Problem, Safe, pt) end
1215 (* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
1216 val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
1218 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1219 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1220 meth=met, ...}) = get_obj I pt p;
1221 (*val pt = update_pbl pt p itms;
1222 val pt = update_pblID pt p pI;*)
1223 val thy = assoc_thy dI
1224 val ((p,Pbl),_,_,pt)=
1225 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
1226 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1227 val mI'' = if mI=e_metID then mI' else mI;
1228 (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
1229 val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1230 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1231 in ((p,Pbl), (pos,Uistate),
1232 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1233 (Problem pI, itms2itemppc dI'' itms pre))),
1235 (* val Specify_Method' mID = nxt; val (p,_) = p;
1236 val Specify_Method' mID = m;
1237 specify (Specify_Method' mID) (p,p_) c pt;
1239 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1240 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1241 meth=met, ...}) = get_obj I pt p;
1242 val {ppc,pre,prls,...} = get_met mID
1243 val thy = assoc_thy dI
1244 val oris = add_field' thy ppc oris;
1245 (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1246 val dI'' = if dI=e_domID then dI' else dI;
1247 val pI'' = if pI = e_pblID then pI' else pI;
1248 val met = if met=[] then pbl else met;
1249 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1250 (*val pt = update_met pt p itms;
1251 val pt = update_metID pt p mID*)
1253 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1254 (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
1255 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1256 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1257 in (pos, (pos,Uistate),
1258 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1259 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1261 (* val Add_Find' ct = nxt; val sel = "#Find";
1263 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1264 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1265 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1266 (* val Specify_Theory' domID = m;
1267 val (Specify_Theory' domID, (p,p_)) = (m, pos);
1269 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1270 let val p_ = case p_ of Met => Met | _ => Pbl
1271 val thy = assoc_thy domID;
1272 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1273 probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
1274 val mppc = case p_ of Met => met | _ => pbl;
1275 val cpI = if pI = e_pblID then pI' else pI;
1276 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1277 val cmI = if mI = e_metID then mI' else mI;
1278 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1281 Met => (check_preconds thy mer mwh met)
1282 | _ => (check_preconds thy per pwh pbl)
1283 val pb = foldl and_ (true, map fst pre)
1286 (*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1287 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1288 (pbl,met) (ppc,mpc) (dI,pI,mI);
1289 in ((p,p_), (pos,Uistate),
1290 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1291 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1293 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1295 (*val pt = update_domID pt p domID;11.8.03*)
1296 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1297 (Uistate, e_ctxt) (p,p_) pt
1298 (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1299 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1300 (ppc,mpc) (domID,pI,mI);
1301 in ((p,p_), (pos,Uistate),
1302 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1303 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1306 (* itms2itemppc thy [](*mpc*) pre
1308 | specify m' _ _ _ =
1309 error ("specify: not impl. for "^tac_2str m');
1311 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1312 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1314 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1316 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1317 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1318 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1319 val cpI = if pI = e_pblID then pI' else pI;
1320 in case appl_add thy sel oris pbl ((#ppc o get_pbt) cpI) ct of
1321 Add itm (*..union old input *) =>
1322 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1325 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1326 val pbl' = insert_ppc thy itm pbl
1329 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1330 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1331 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1332 val ((p,Pbl),c,_,pt') =
1333 generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
1334 in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate' end
1337 (*TODO.WN03 pass error-msgs to the frontend..
1338 FIXME ..and dont abuse a tactic for that purpose*)
1340 Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1341 (e_pos', (e_istate, e_ctxt)))], [], ptp)
1344 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1345 val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1347 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1349 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1350 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1351 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1352 val cmI = if mI = e_metID then mI' else mI;
1353 in case appl_add thy sel oris met ((#ppc o get_met) cmI) ct of
1354 Add itm (*..union old input *) =>
1355 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1357 val met' = insert_ppc thy itm met;
1360 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1361 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1362 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1363 val ((p,Met),c,_,pt') =
1364 generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
1365 in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
1367 | Err msg => ([(*tacis*)], [], ptp)
1368 (*nxt_me collects tacis until not hide; here just no progress*)
1372 val (msg,itm) = appl_add thy sel oris ppc ct;
1373 val (Cor(d,ts)) = #5 itm;
1378 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1379 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1380 handle _ => error ("ori2Coritm: dsc "^
1382 "in ori, but not in pbt")
1384 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1385 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1386 (find_first (eq1 d))) pbt,ts))):itm)
1387 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1388 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1391 (*filter out oris which have same description in itms*)
1392 fun filter_outs oris [] = oris
1393 | filter_outs oris (i::itms) =
1394 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1395 (#4:ori -> term)) oris;
1396 in filter_outs ors itms end;
1398 fun memI a b = member op = a b;
1399 (*filter oris which are in pbt, too*)
1400 fun filter_pbt oris pbt =
1401 let val dscs = map (fst o snd) pbt
1402 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1404 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1405 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1407 fun x mem [] = false
1408 | x mem (y :: ys) = x = y orelse x mem ys;
1410 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1411 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1413 let val vat = max_vt pits;
1415 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1416 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1417 val os = filter_outs ors itms;
1418 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1419 in itms @ (map (ori2Coritm met) os) end
1424 (*.complete model and guard of a calc-head .*)
1426 fun x mem [] = false
1427 | x mem (y :: ys) = x = y orelse x mem ys;
1429 fun complete_mod_ (oris, mpc, ppc, probl) =
1430 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1431 val vat = if probl = [] then 1 else max_vt probl
1432 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1433 val pors = filter_outs pors pits (*which are in pbl already*)
1434 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1436 val pits = pits @ (map (ori2Coritm ppc) pors)
1437 val mits = complete_metitms oris pits [] mpc
1441 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1442 (if dI = e_domID then odI else dI,
1443 if pI = e_pblID then opI else pI,
1444 if mI = e_metID then omI else mI):spec;
1447 (*.find a next applicable tac (for calcstate) and update ptree
1448 (for ev. finding several more tacs due to hide).*)
1449 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1450 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1451 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1452 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1454 val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1455 val (dI, pI, mI) = some_spec ospec spec
1456 val thy = assoc_thy dI
1457 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1458 val {cas, ppc, ...} = get_pbt pI
1459 val pbl = init_pbl ppc (* fill in descriptions *)
1460 (*----------------if you think, this should be done by the Dialog
1461 in the java front-end, search there for WN060225-modelProblem----*)
1462 val (pbl, met) = case cas of NONE => (pbl, [])
1463 | _ => complete_mod_ (oris, mpc, ppc, probl)
1464 (*----------------------------------------------------------------*)
1465 val tac_ = Model_Problem' (pI, pbl, met)
1466 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
1467 in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1469 (* val Add_Find ct = tac;
1471 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1472 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1473 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1475 (*. called only if no_met is specified .*)
1476 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1477 let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1478 val opt = refine_ori oris pI
1481 let val {met,ppc,...} = get_pbt pI'
1482 val pbl = init_pbl ppc
1483 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1484 val mI = if length met = 0 then e_metID else hd met
1485 val thy = assoc_thy dI
1487 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1488 (Uistate, e_ctxt) pos pt
1489 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1490 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1491 | NONE => ([], [], ptp)
1494 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1495 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1496 probl, ...}) = get_obj I pt p
1497 val thy = if dI' = e_domID then dI else dI'
1498 in case refine_pbl (assoc_thy thy) pI probl of
1499 NONE => ([], [], ptp)
1500 | SOME (rfd as (pI',_)) =>
1501 let val (pos,c,_,pt) =
1502 generate1 (assoc_thy thy)
1503 (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1504 in ([(Refine_Problem pI, Refine_Problem' rfd,
1505 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1508 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1509 let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1510 probl, ...}) = get_obj I pt p;
1511 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1512 val {ppc,where_,prls,...} = get_pbt pI
1513 val pbl as (_,(itms,_)) =
1514 if pI'=e_pblID andalso pI=e_pblID
1515 then (false, (init_pbl ppc, []))
1516 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1517 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1518 val ((p,Pbl),c,_,pt)=
1519 generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
1520 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1521 (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1523 (*transfers oris (not required in pbl) to met-model for script-env
1524 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1525 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1526 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1527 meth=met, ...}) = get_obj I pt p;
1528 val {ppc,pre,prls,...} = get_met mID
1529 val thy = assoc_thy dI
1530 val oris = add_field' thy ppc oris;
1531 val dI'' = if dI=e_domID then dI' else dI;
1532 val pI'' = if pI = e_pblID then pI' else pI;
1533 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1534 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1536 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1537 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1538 (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1540 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1541 let val (dI',_,_) = get_obj g_spec pt p
1543 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1544 (Uistate, e_ctxt) pos pt
1545 in (*FIXXXME: check if pbl can still be parsed*)
1546 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1549 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1550 let val (dI',_,_) = get_obj g_spec pt p
1552 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1553 (Uistate, e_ctxt) pos pt
1554 in (*FIXXXME: check if met can still be parsed*)
1555 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1559 error ("nxt_specif: not impl. for "^tac2str m');
1561 (*.get the values from oris; handle the term list w.r.t. penv.*)
1564 fun x mem [] = false
1565 | x mem (y :: ys) = x = y orelse x mem ys;
1567 fun vals_of_oris oris =
1568 ((map (mkval' o (#5:ori -> term list))) o
1569 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1574 (* create a calc-tree with oris via an cas.refined pbl *)
1575 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1576 if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1577 let val {cas, met, ppc, thy, ...} = get_pbt pI
1578 val dI = if dI = "" then theory2theory' thy else dI
1579 val thy = assoc_thy dI
1580 val mI = if mI = [] then hd met else mI
1581 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1582 val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1583 ([], (dI,pI,mI), hdl)
1584 val pt = update_spec pt [] (dI,pI,mI)
1585 val pits = init_pbl' ppc
1586 val pt = update_pbl pt [] pits
1587 in ((pt, ([] ,Pbl)), []) : calcstate end
1588 else if mI <> [] then (* from met-browser *)
1589 let val {ppc,...} = get_met mI
1590 val dI = if dI = "" then "Isac" else dI
1591 val thy = assoc_thy dI
1592 val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1593 ([], (dI,pI,mI), e_term(*FIXME met*))
1594 val pt = update_spec pt [] (dI,pI,mI)
1595 val mits = init_pbl' ppc
1596 val pt = update_met pt [] mits
1597 in ((pt, ([], Met)), []) : calcstate end
1598 else (* new example, pepare for interactive modeling *)
1599 let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1600 ([], e_spec, e_term)
1601 in ((pt,([],Pbl)), []) : calcstate end
1602 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1603 let (* both """"""""""""""""""""""""" either empty or complete *)
1604 val thy = assoc_thy dI
1605 val (pI, pors, mI) =
1607 then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI)
1608 val pI' = refine_ori' pors pI;
1609 in (pI', pors(*refinement over models with diff.precond only*),
1610 (hd o #met o get_pbt) pI') end
1611 else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI)
1612 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1613 val dI = theory2theory' (maxthy thy thy');
1614 val hdl = case cas of
1615 NONE => pblterm dI pI
1616 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1617 ~~~ vals_of_oris pors) t
1618 val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
1619 (pors, (dI, pI, mI), hdl)
1620 in ((pt, ([], Pbl)),
1621 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1627 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1628 (* case appl_spec p pt m of /// 19.1.00
1629 Notappl e => Error' (Error_ e)
1631 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1635 (*fun tag_form thy (formal, given) = cterm_of thy
1636 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1637 fun tag_form thy (formal, given) =
1638 (let val gf = (head_of given) $ formal;
1639 val _ = cterm_of thy gf
1642 error ("calchead.tag_form: " ^
1643 Print_Mode.setmp [] (Syntax.string_of_term
1644 (thy2ctxt thy)) given ^ " .. " ^
1645 Print_Mode.setmp [] (Syntax.string_of_term
1646 (thy2ctxt thy)) formal ^
1647 " ..types do not match");
1648 (* val formal = (the o (parse thy)) "[R::real]";
1649 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1650 > tag_form thy (formal, given);
1651 val it = "fixed_values [R]" : cterm
1654 fun chktyp thy (n, fs, gs) =
1655 ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1657 (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1659 tag_form thy (nth n fs, nth n gs));
1660 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1662 (* #####################################################
1663 find the failing item:
1665 > val tag__form = chktyp (n,formals,givens);
1666 > (type_of o term_of o (nth n)) formals;
1667 > (type_of o term_of o (nth n)) givens;
1668 > atomty ((term_of o (nth n)) formals);
1669 > atomty ((term_of o (nth n)) givens);
1670 > atomty (term_of tag__form);
1671 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1672 ##################################################### *)
1674 (* #####################################################
1676 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1677 val formals = map (the o (parse thy)) origin;
1679 val given = ["equation (lhs=rhs)",
1680 "bound_variable bdv", (* TODO type *)
1682 val where_ = ["e is_root_equation_in bdv",
1684 "apx is_const_expr"];
1685 val find = ["L::rat set"];
1686 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1687 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1688 val givens = map (the o (parse thy)) given;
1690 val tag__forms = chktyps (formals, givens);
1691 map ((atomty) o term_of) tag__forms;
1692 ##################################################### *)
1695 (* check pbltypes, announces one failure a time *)
1696 (*fun chk_vars ctppc =
1697 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1698 appc flat (mappc (vars o term_of) ctppc)
1699 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1700 else if (re\\(gi union fi)) <> []
1701 then ("re\\(gi union fi)",re\\(gi union fi))
1702 else ("ok",[]) end;*)
1703 fun chk_vars ctppc =
1704 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1705 appc flat (mappc vars ctppc)
1706 val chked = subtract op = gi wh
1707 in if chked <> [] then ("wh\\gi", chked)
1708 else let val chked = subtract op = (union op = gi fi) re
1710 then ("re\\(gi union fi)", chked)
1715 (* check a new pbltype: variables (Free) unbound by given, find*)
1716 fun unbound_ppc ctppc =
1717 let val {Given=gi,Find=fi,Relate=re,...} =
1718 appc flat (mappc vars ctppc)
1719 in distinct (*re\\(gi union fi)*)
1720 (subtract op = (union op = gi fi) re) end;
1722 > val org = {Given=["[R=(R::real)]"],Where=[],
1723 Find=["[A::real]"],With=[],
1724 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1726 > val ctppc = mappc (the o (parse thy)) org;
1727 > unbound_ppc ctppc;
1728 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1732 (* f, a binary operator, is nested rightassociative *)
1735 fun fld f (x::[]) = x
1736 | fld f (x::x'::[]) = f (x',x)
1737 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1738 in ((fld f) o rev) xs end;
1740 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1741 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1742 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1743 > cterm_of thy conj;
1744 val it = "(a = b & c = d) & e = f" : cterm
1747 (* f, a binary operator, is nested leftassociative *)
1748 fun foldl1 f (x::[]) = x
1749 | foldl1 f (x::x'::[]) = f (x,x')
1750 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1752 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1753 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1754 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1755 > cterm_of thy conj;
1756 val it = "a = b & c = d & e = f & g = h" : cterm
1760 (* called only once, if a Subproblem has been located in the script*)
1761 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
1762 (* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
1766 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1767 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1768 (*all stored in tac_ itms ^^^^^^^^^^*)
1769 | nxt_model_pbl tac_ _ =
1770 error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1771 (* run subp_rooteq.sml ''
1772 until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
1773 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1774 (last_elem o drop_last) ets'';
1775 > val mst = (last_elem o drop_last) ets'';
1776 > nxt_model_pbl mst;
1777 val it = Refine_Tacitly ["univariate","equation"] : tac
1780 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1781 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1782 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1785 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1786 + met from fmz; assumes pos on PblObj, meth = [].*)
1787 fun complete_mod (pt, pos as (p, p_):pos') =
1788 (* val (pt, (p, _)) = (pt, p);
1789 val (pt, (p, _)) = (pt, pos);
1791 let val _= if p_ <> Pbl
1792 then tracing("###complete_mod: only impl.for Pbl, called with "^
1793 pos'2str pos) else ()
1794 val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
1796 val (dI,pI,mI) = some_spec ospec spec
1797 val mpc = (#ppc o get_met) mI
1798 val ppc = (#ppc o get_pbt) pI
1799 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1800 val pt = update_pblppc pt p pits
1801 val pt = update_metppc pt p mits
1802 in (pt, (p,Met):pos') end
1804 (*| complete_mod (pt, pos as (p, Met):pos') =
1805 error ("###complete_mod: only impl.for Pbl, called with "^
1808 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1809 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1810 fun all_modspec (pt, (p,_):pos') =
1811 (* val (pt, (p,_)) = ptp;
1813 let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1814 ...}) = get_obj I pt p;
1815 val thy = assoc_thy dI;
1816 val {ppc,...} = get_met mI;
1817 val mors = prep_ori fmz_ thy ppc;
1818 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1819 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1820 val pt = update_spec pt p (dI,pI,mI);
1821 in (pt, (p,Met): pos') end;
1823 (*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1824 fun is_complete_mod_ ([]: itm list) = false
1825 | is_complete_mod_ itms =
1826 foldl and_ (true, (map #3 itms));
1827 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1828 if (is_pblobj o (get_obj I pt)) p
1829 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1830 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1831 | is_complete_mod (pt, pos as (p, Met)) =
1832 if (is_pblobj o (get_obj I pt)) p
1833 then (is_complete_mod_ o (get_obj g_met pt)) p
1834 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1835 | is_complete_mod (_, pos) =
1836 error ("is_complete_mod called by "^pos'2str pos^
1837 " (should be Pbl or Met)");
1839 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1840 fun is_complete_spec (pt, pos as (p,_): pos') =
1841 if (not o is_pblobj o (get_obj I pt)) p
1842 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1843 else let val (dI,pI,mI) = get_obj g_spec pt p
1844 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1845 (*.complete empty items in specification from origin (pbl, met ev.refined);
1846 assumes 'is_complete_mod'.*)
1847 fun complete_spec (pt, pos as (p,_): pos') =
1848 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1849 val pt = update_spec pt p (some_spec ospec spec)
1852 fun is_complete_modspec ptp =
1853 is_complete_mod ptp andalso is_complete_spec ptp;
1858 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1859 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1861 let val (_,_,metID) = get_somespec' spec spec'
1863 if metID = e_metID then []
1864 else let val {prls,pre=where_,...} = get_met metID
1865 val pre = check_preconds' prls where_ meth 0
1867 val allcorrect = is_complete_mod_ meth
1868 andalso foldl and_ (true, (map #1 pre))
1869 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1870 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1871 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1873 let val (_,pI,_) = get_somespec' spec spec'
1875 if pI = e_pblID then []
1876 else let val {prls,where_,cas,...} = get_pbt pI
1877 val pre = check_preconds' prls where_ probl 0
1879 val allcorrect = is_complete_mod_ probl
1880 andalso foldl and_ (true, (map #1 pre))
1881 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1884 fun pt_form (PrfObj {form,...}) = Form form
1885 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1886 let val (dI, pI, _) = get_somespec' spec spec'
1887 val {cas,...} = get_pbt pI
1889 NONE => Form (pblterm dI pI)
1890 | SOME t => Form (subst_atomic (mk_env probl) t)
1892 (*vvv takes the tac _generating_ the formula=result, asm ok....
1893 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1895 if null asm then NONE else SOME asm,
1897 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1898 let val (_,_,metID) = some_spec ospec spec
1900 if null asm then NONE else SOME asm,
1901 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1902 -------------------------------------------------------------------------*)
1905 (*.pt_extract returns
1906 # the formula at pos
1907 # the tactic applied to this formula
1908 # the list of assumptions generated at this formula
1909 (by application of another tac to the preceding formula !)
1910 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1911 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1912 fun pt_extract (pt,([],Res)) =
1913 (* val (pt,([],Res)) = ptp;
1915 let val (f, asm) = get_obj g_result pt []
1916 in (Form f, NONE, asm) end
1919 | pt_extract (pt,(p,Res)) =
1920 (* val (pt,(p,Res)) = ptp;
1922 let val (f, asm) = get_obj g_result pt p
1923 val tac = if last_onlev pt p
1924 then if is_pblobj' pt (lev_up p)
1925 then let val (PblObj{spec=(_,pI,_),...}) =
1926 get_obj I pt (lev_up p)
1927 in if pI = e_pblID then NONE
1928 else SOME (Check_Postcond pI) end
1929 else SOME End_Trans (*WN0502 TODO for other branches*)
1930 else let val p' = lev_on p
1931 in if is_pblobj' pt p'
1932 then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1934 in SOME (Subproblem (dI, pI)) end
1935 else if f = get_obj g_form pt p'
1936 then SOME (get_obj g_tac pt p')
1937 (*because this Frm ~~~is not on worksheet*)
1938 else SOME (Take (term2str (get_obj g_form pt p')))
1940 in (Form f, tac, asm) end
1942 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1943 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1944 val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
1946 let val ppobj = get_obj I pt p
1947 val f = if is_pblobj ppobj then pt_model ppobj p_
1948 else get_obj pt_form pt p
1949 val tac = g_tac ppobj
1950 in (f, SOME tac, []) end;
1953 (**. get the formula from a ctree-node:
1954 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1955 take res from all other PrfObj's .**)
1956 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1957 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1958 [("headline", (p, Frm), h),
1959 ("stepform", (p, Res), r)]
1960 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1961 [("stepform", (p, Frm), form),
1962 ("stepform", (p, Res), r)];
1964 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1965 [("stepform", (p, Res), r)]
1967 (*assumes to take whole level, in particular hd -- for use in interSteps*)
1968 fun get_formress fs p [] = flat fs
1969 | get_formress fs p (nd::nds) =
1970 (* start with 'form+res' and continue with trying 'res' only*)
1971 get_forms (fs @ [formres p nd]) (lev_on p) nds
1972 and get_forms fs p [] = flat fs
1973 | get_forms fs p (nd::nds) =
1975 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1976 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1977 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1978 (* continue with trying 'res' only*)
1979 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1981 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1982 (*WN050219 made robust against _'to' below or after Complete nodes
1983 by handling exn caused by move_dn*)
1984 (*WN0401 this functionality belongs to ctree.sml,
1985 but fetching a calc_head requires calculations defined in modspec.sml
1986 transfer to ME/me.sml !!!
1987 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1988 is returned !!!!!!!!!!!!!
1990 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1991 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1992 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1996 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
2000 | eq_pos' _ _ = false;
2002 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
2003 total ordering Position#compareTo(Position p) in the java-code
2004 val get_interval = fn
2005 : pos' -> : from is "move_up 1st-element" to return
2006 pos' -> : to the last element to be returned; from < to
2007 int -> : level: 0 gets the flattest sub-tree possible
2008 >999 gets the deepest sub-tree possible
2010 (pos' * : of the formula
2011 Term.term) : the formula
2014 fun get_interval from to level pt =
2015 (* val (from,level) = (f,lev);
2016 val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
2018 let fun get_inter c (from:pos') (to:pos') lev pt =
2019 (* val (c, from, to, lev) = ([], from, to, level);
2020 ------for recursion.......
2021 val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
2023 if eq_pos' from to orelse from = ([],Res)
2024 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
2025 if 'to' has values NOT generated by move_dn, see systest/me.sml
2026 TODO.WN0501: introduce an order on pos' and check "from > to"..
2027 ...there is an order in Java!
2028 WN051224 the hack got worse with returning term instead ptform*)
2029 then let val (f,_,_) = pt_extract (pt, from)
2031 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2032 | Form t => c @ [(from, t)]
2035 if lev < lev_of from
2036 then (get_inter c (move_dn [] pt from) to lev pt)
2037 handle (PTREE _(*from move_dn too far*)) => c
2038 else let val (f,_,_) = pt_extract (pt, from)
2039 val term = case f of
2040 ModSpec (_,_,headline,_,_,_)=> headline
2042 in (get_inter (c @ [(from, term)])
2043 (move_dn [] pt from) to lev pt)
2044 handle (PTREE _(*from move_dn too far*))
2045 => c @ [(from, term)] end
2046 in get_inter [] from to level pt end;
2049 fun posform2str (pos:pos', form) =
2050 "("^ pos'2str pos ^", "^
2052 Form f => term2str f
2053 | ModSpec c => term2str (#3 c(*the headline*)))
2055 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2056 (map posform2str)) pfs;
2057 fun posterm2str (pos:pos', t) =
2058 "("^ pos'2str pos ^", "^term2str t^")";
2059 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2060 (map posterm2str)) pfs;
2063 (*WN050225 omits the last step, if pt is incomplete*)
2065 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
2067 (*.get a calchead from a PblObj-node in the ctree;
2068 preconditions must be calculated.*)
2069 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
2070 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
2072 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2073 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
2074 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
2075 | get_ocalhd (pt, pos' as (p,Met):pos') =
2076 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2079 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2080 val pre = check_preconds (assoc_thy"Isac") prls pre meth
2081 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
2083 (*.at the activeFormula set the Model, the Guard and the Specification
2084 to empty and return a CalcHead;
2085 the 'origin' remains (for reconstructing all that).*)
2086 fun reset_calchead (pt, pos' as (p,_):pos') =
2087 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
2088 val pt = update_pbl pt p []
2089 val pt = update_met pt p []
2090 val pt = update_spec pt p e_spec
2091 in (pt, (p,Pbl):pos') end;
2093 (*---------------------------------------------------------------------
2097 ---------------------------------------------------------------------*)