intermed. context introduction to specification phase
1 (* Title: Specify-phase: specifying and modeling a problem or a subproblem. The
2 most important types are declared in mstools.sml.
3 Author: Walther Neuper 991122
4 (c) due to copyright terms
6 12345678901234567890123456789012345678901234567890123456789012345678901234567890
7 10 20 30 40 50 60 70 80
10 (* TODO interne Funktionen aus sig entfernen *)
13 datatype additm = Add of SpecifyTools.itm | Err of string
14 val all_dsc_in : SpecifyTools.itm_ list -> Term.term list
15 val all_modspec : ptree * pos' -> ptree * pos'
16 datatype appl = Appl of tac_ | Notappl of string
20 SpecifyTools.ori list ->
21 SpecifyTools.itm list ->
22 (string * (Term.term * Term.term)) list -> cterm' -> additm
25 val chk_vars : term ppc -> string * Term.term list
27 theory -> int * term list * term list -> term
29 theory -> term list * term list -> term list
30 val complete_metitms :
31 SpecifyTools.ori list ->
32 SpecifyTools.itm list ->
33 SpecifyTools.itm list -> pat list -> SpecifyTools.itm list
34 val complete_mod_ : ori list * pat list * pat list * itm list ->
36 val complete_mod : ptree * pos' -> ptree * (pos * pos_)
37 val complete_spec : ptree * pos' -> ptree * pos'
39 pat list -> preori list -> pat -> preori
40 val e_calcstate : calcstate
41 val e_calcstate' : calcstate'
42 val eq1 : ''a -> 'b * (''a * 'c) -> bool
44 ''a -> Term.term -> 'b * 'c * 'd * ''a * SpecifyTools.itm_ -> bool
45 val eq4 : ''a -> 'b * ''a list * 'c * 'd * 'e -> bool
47 'a * 'b * 'c * 'd * SpecifyTools.itm_ ->
48 'e * 'f * 'g * Term.term * 'h -> bool
49 val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool
50 val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool
51 val f_mout : theory -> mout -> Term.term
53 SpecifyTools.ori list ->
54 SpecifyTools.itm list -> SpecifyTools.ori list
56 SpecifyTools.ori list ->
57 ('a * (Term.term * 'b)) list -> SpecifyTools.ori list
58 val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
59 val foldr1 : ('a * 'a -> 'a) -> 'a list -> 'a
60 val form : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
61 val formres : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
62 val gen_ins' : ('a * 'a -> bool) -> 'a * 'a list -> 'a list
64 (string * (pos * pos_) * Term.term) list list ->
65 pos -> ptree list -> (string * (pos * pos_) * Term.term) list
67 (string * (pos * pos_) * Term.term) list list ->
68 posel list -> ptree list -> (string * (pos * pos_) * Term.term) list
69 val get_interval : pos' -> pos' -> int -> ptree -> (pos' * term) list
70 val get_ocalhd : ptree * pos' -> ocalhd
71 val get_spec_form : tac_ -> pos' -> ptree -> mout
74 SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'
75 val getr_ct : theory -> SpecifyTools.ori -> string * cterm'
76 val has_list_type : Term.term -> bool
77 val header : pos_ -> pblID -> metID -> pblmet
80 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
81 SpecifyTools.itm list -> SpecifyTools.itm list
83 SpecifyTools.itm -> SpecifyTools.itm list -> SpecifyTools.itm list
84 val is_complete_mod : ptree * pos' -> bool
85 val is_complete_mod_ : SpecifyTools.itm list -> bool
86 val is_complete_modspec : ptree * pos' -> bool
87 val is_complete_spec : ptree * pos' -> bool
88 val is_copy_named : 'a * ('b * Term.term) -> bool
89 val is_copy_named_idstr : string -> bool
90 val is_error : SpecifyTools.itm_ -> bool
91 val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
95 SpecifyTools.ori list ->
96 Term.term -> string * SpecifyTools.ori * Term.term list
97 val is_list_type : Term.typ -> bool
100 SpecifyTools.itm list ->
103 ('a * (Term.term * Term.term)) list -> string * SpecifyTools.itm
104 val is_parsed : SpecifyTools.itm_ -> bool
105 val is_untouched : SpecifyTools.itm -> bool
110 (int list * string * Term.term * Term.term list) list ->
111 (int list * string * Term.term * Term.term list) list
113 theory -> pat list -> Term.term list -> SpecifyTools.ori list
114 val maxl : int list -> int
115 val match_ags_msg : string list -> Term.term -> Term.term list -> unit
116 val memI : ''a list -> ''a -> bool
117 val mk_additem : string -> cterm' -> tac
118 val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
120 theory -> pat -> Term.term -> SpecifyTools.preori option
123 SpecifyTools.ori list ->
124 (string * (Term.term * 'a)) list ->
125 SpecifyTools.itm list -> (string * cterm') option
126 val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
130 SpecifyTools.ori list ->
132 SpecifyTools.itm list * SpecifyTools.itm list ->
133 (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->
135 val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'
136 val nxt_specif_additem :
137 string -> cterm' -> ptree * (int list * pos_) -> calcstate'
138 val nxt_specify_init_calc : fmz -> calcstate
139 val ocalhd_complete :
140 SpecifyTools.itm list ->
141 (bool * Term.term) list -> domID * pblID * metID -> bool
143 pat list -> ori -> itm
146 Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
149 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
150 SpecifyTools.itm list ->
151 (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
152 val parse_ok : SpecifyTools.itm_ list -> bool
153 val posform2str : pos' * ptform -> string
154 val posforms2str : (pos' * ptform) list -> string
155 val posterms2str : (pos' * term) list -> string (*tests only*)
156 val ppc135list : 'a SpecifyTools.ppc -> 'a list
157 val ppc2list : 'a SpecifyTools.ppc -> 'a list
159 ptree * (int list * pos_) ->
160 ptform * tac option * Term.term list
161 val pt_form : ppobj -> ptform
162 val pt_model : ppobj -> pos_ -> ptform
163 val reset_calchead : ptree * pos' -> ptree * pos'
167 Term.term * Term.term list ->
168 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
169 -> string * SpecifyTools.ori * Term.term list
174 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
175 -> string * SpecifyTools.ori * Term.term list
177 int -> SpecifyTools.itm list -> SpecifyTools.itm option
178 val show_pt : ptree -> unit
179 val some_spec : spec -> spec -> spec
185 (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *
187 val specify_additem :
193 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
194 val tag_form : theory -> term * term -> term
195 val test_types : Proof.context -> Term.term * Term.term list -> string
196 val typeless : Term.term -> Term.term
197 val unbound_ppc : term SpecifyTools.ppc -> Term.term list
198 val vals_of_oris : SpecifyTools.ori list -> Term.term list
199 val variants_in : Term.term list -> int
200 val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
201 val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
208 (*---------------------------------------------------------------------
209 structure CalcHead (**): CALC_HEAD(**) =
212 ---------------------------------------------------------------------*)
216 (*.the state wich is stored after each step of calculation; it contains
217 the calc-state and a list of [tac,istate](="tacis") to be applied next.
218 the last_elem tacis is the first to apply to the calc-state and
219 the (only) one shown to the front-end as the 'proposed tac'.
220 the calc-state resulting from the application of tacis is not stored,
221 because the tacis hold enough information for efficiently rebuilding
222 this state just by "fun generate ".*)
224 (ptree * pos') * (*the calc-state to which the tacis could be applied*)
225 (taci list); (*ev. several (hidden) steps;
226 in REVERSE order: first tac_ to apply is last_elem*)
227 val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
229 (*the state used during one calculation within the mathengine; it contains
230 a list of [tac,istate](="tacis") which generated the the calc-state;
231 while this state's tacis are extended by each (internal) step,
232 the calc-state is used for creating new nodes in the calc-tree
233 (eg. applicable_in requires several particular nodes of the calc-tree)
234 and then replaced by the the newly created;
235 on leave of the mathengine the resuing calc-state is dropped anyway,
236 because the tacis hold enought information for efficiently rebuilding
237 this state just by "fun generate ".*)
239 taci list * (*cas. several (hidden) steps;
240 in REVERSE order: first tac_ to apply is last_elem*)
241 pos' list * (*a "continuous" sequence of pos',
242 deleted by application of taci list*)
243 (ptree * pos'); (*the calc-state resulting from the application of tacis*)
244 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
246 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
247 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
248 | f_mout thy _ = error "f_mout: not called with formula";
251 (*.is the calchead complete ?.*)
252 fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
253 foldl and_ (true, map #3 its) andalso
254 foldl and_ (true, map #1 pre) andalso
255 dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
258 (* make a term 'typeless' for comparing with another 'typeless' term;
259 'type-less' usually is illtyped *)
260 fun typeless (Const(s,_)) = (Const(s,e_type))
261 | typeless (Free(s,_)) = (Free(s,e_type))
262 | typeless (Var(n,_)) = (Var(n,e_type))
263 | typeless (Bound i) = (Bound i)
264 | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
265 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
267 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
268 > val (_,t1) = split_dsc_t hs (term_of ct);
269 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
270 > val (_,t2) = split_dsc_t hs (term_of ct);
271 > typeless t1 = typeless t2;
277 (*.to an input (d,ts) find the according ori and insert the ts.*)
278 (*WN.11.03: + dont take first inter<>[]*)
279 (*fun seek_oridts ctxt sel (d,ts) [] =
280 ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
282 "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
284 | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
285 if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
287 (id,vat,sel,d, inter op = ts ts'):ori,
289 else seek_oridts ctxt sel (d,ts) oris;*)
291 fun seek_oridts ctxt sel (d,ts) [] =
292 ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
294 "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
296 | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
297 if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
300 (id,vat,sel,d, inter op = ts ts'):ori,
302 else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)))
303 ^ " not for " ^ sel, e_ori_, [])
304 else seek_oridts ctxt sel (d,ts) oris;
306 (*.to an input (_,ts) find the according ori and insert the ts.*)
307 fun seek_orits ctxt sel ts [] =
308 ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
310 "') not found in oris (typed)", e_ori_, [])
311 | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
312 if sel = sel' andalso (inter op = ts ts') <> []
315 (id,vat,sel,d, inter op = ts ts'):ori,
317 else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
322 else seek_orits ctxt sel ts oris;
324 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
325 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
326 uncaught exception TYPE
327 > seek_orits thy sel ts [];
328 uncaught exception TYPE
331 (*find_first item with #1 equal to id*)
332 fun seek_ppc id [] = NONE
333 | seek_ppc id (p::(ppc:itm list)) =
334 if id = #1 p then SOME p else seek_ppc id ppc;
338 (*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
341 datatype appl = Appl of tac_ | Notappl of string;
343 fun ppc2list ({Given=gis,Where=whs,Find=fis,
344 With=wis,Relate=res}: 'a ppc) =
345 gis @ whs @ fis @ wis @ res;
346 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
352 (* get the number of variants in a problem in 'original',
353 assumes equal descriptions in immediate sequence *)
355 let fun eq(x,y) = head_of x = head_of y;
356 fun cnt eq [] y n = ([n],[])
357 | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
359 fun coll eq xs [] = xs
360 | coll eq xs (y::ys) =
361 let val (n,ys') = cnt eq (y::ys) y 0;
362 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
363 val vts = subtract op = [1] (distinct (coll eq [] ts));
364 in case vts of [] => 1 | [n] => n
365 | _ => error "different variants in formalization" end;
367 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
368 val it = ([3],[4,5,5,5,5,5]) : int list * int list
369 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
370 val it = [1,3,1,5] : int list
373 fun is_list_type (Type("List.list",_)) = true
374 | is_list_type _ = false;
375 (* fun destr (Type(str,sort)) = (str,sort);
376 > val (SOME ct) = parse thy "lll::real list";
377 > val ty = (#T o rep_cterm) ct;
381 val it = ("List.list",["RealDef.real"]) : string * typ list
382 > atomty ((#t o rep_cterm) ct);
384 *** Free ( lll, real list)
387 > val (SOME ct) = parse thy "[lll::real]";
388 > val ty = (#T o rep_cterm) ct;
392 val it = ("List.list",["'a"]) : string * typ list
393 > atomty ((#t o rep_cterm) ct);
395 *** Const ( List.list.Cons, [real, real list] => real list)
396 *** Free ( lll, real)
397 *** Const ( List.list.Nil, real list)
399 > val (SOME ct) = parse thy "lll";
400 > val ty = (#T o rep_cterm) ct;
402 val it = false : bool *)
405 fun has_list_type (Free(_,T)) = is_list_type T
406 | has_list_type _ = false;
408 > val (SOME ct) = parse thy "lll::real list";
409 > has_list_type (term_of ct);
411 > val (SOME ct) = parse thy "[lll::real]";
412 > has_list_type (term_of ct);
413 val it = false : bool *)
415 fun is_parsed (Syn _) = false
416 | is_parsed _ = true;
417 fun parse_ok its = foldl and_ (true, map is_parsed its);
419 fun all_dsc_in itm_s =
421 fun d_in (Cor ((d,_),_)) = [d]
424 | d_in (Inc ((d,_),_)) = [d]
425 | d_in (Sup (d,_)) = [d]
426 | d_in (Mis (d,_)) = [d];
427 in (flat o (map d_in)) itm_s end;
430 fun is_Syn (Syn _) = true
431 | is_Syn (Typ _) = true
434 fun is_error (Cor (_,ts)) = false
435 | is_error (Sup (_,ts)) = false
436 | is_error (Inc (_,ts)) = false
437 | is_error (Mis (_,ts)) = false
441 fun ct_in (Syn (c)) = c
442 | ct_in (Typ (c)) = c
443 | ct_in _ = error "ct_in called for Cor .. Sup";
446 (*#############################################################*)
447 (*#############################################################*)
448 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
451 (* testdaten besorgen:
452 use"test-coil-kernel.sml";
453 val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
458 variant V: oris union ppc => int, id ID: oris union ppc => int
461 EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
464 @vt = max sum(i : ppc) V i
470 > ((vts_cnt (vts_in itms))) itms;
475 > val vts = vts_in itms;
476 val vts = [1,2,3] : int list
477 > val nvts = vts_cnt vts itms;
478 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
479 > val mx = max2 nvts;
480 val mx = (3,7) : int * int
481 > val v = max_vt itms;
483 --------------------------
487 (*.get the first term in ts from ori.*)
488 (* val (_,_,fd,d,ts) = hd miss;
490 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
491 (fd, (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) o
492 comp_dts) (d,[hd ts]) : cterm');
493 (* val t = comp_dts (d,[hd ts]);
496 (* get a term from ori, notyet input in itm.
497 the term from ori is thrown back to a string in order to reuse
498 machinery for immediate input by the user. *)
499 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
500 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
501 (d, subtract op = (ts_in itm_) ts) : cterm');
502 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
503 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
504 (d, subtract op = (ts_in itm_) ts) : cterm');
506 (* in FE dsc, not dat: this is in itms ...*)
507 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
508 | is_untouched _ = false;
511 (* select an item in oris, notyet input in itms
512 (precondition: in itms are only Cor, Sup, Inc) *)
515 | x mem (y :: ys) = x = y orelse x mem ys;
517 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
519 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
520 fun is_elem itms (f,(d,t)) =
521 case find_first (test_d d) itms of
522 SOME _ => true | NONE => false;
523 in case filter_out (is_elem itms) pbt of
524 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
528 ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
529 comp_dts) (d, []) : cterm')
532 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
534 | nxt_add thy oris pbt itms =
536 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
537 andalso (#3 ori) <>"#undef";
538 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
539 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
540 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
541 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
542 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
543 | false_and_not_Sup (i,v,false,f, _) = true
544 | false_and_not_Sup _ = false;
546 val v = if itms = [] then 1 else max_vt itms;
547 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
548 val vits = if v = 0 then itms (*because of dsc without dat*)
549 else filter (testi_vt v) itms; (*itms..vat*)
550 val icl = filter false_and_not_Sup vits; (* incomplete *)
552 then case filter_out (test_id (map #1 vits)) vors of
554 (* val miss = filter_out (test_id (map #1 vits)) vors;
556 | miss => SOME (getr_ct thy (hd miss))
558 case find_first (test_subset (hd icl)) vors of
559 (* val SOME ori = find_first (test_subset (hd icl)) vors;
561 NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
562 | SOME ori => SOME (geti_ct thy ori (hd icl))
568 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
569 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
570 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
571 | mk_delete thy str _ =
572 error ("mk_delete: called with field '"^str^"'");
573 fun mk_additem "#Given" ct = Add_Given ct
574 | mk_additem "#Find" ct = Add_Find ct
575 | mk_additem "#Relate"ct = Add_Relation ct
577 error ("mk_additem: called with field '"^str^"'");
580 (* determine the next step of specification;
581 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
582 eg. in rootpbl 'no_met':
584 preok predicates are _all_ ok (and problem matches completely)
585 oris immediately from formalization
586 (dI',pI',mI') specification coming from author/parent-problem
587 (pbl, item lists specified by user
588 met) -"-, tacitly completed by copy_probl
589 (dI,pI,mI) specification explicitly done by the user
590 (pbt, mpc) problem type, guard of method
592 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
593 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
594 ((*tracing"### nxt_spec Pbl";*)
595 if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
596 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
597 else case find_first (is_error o #5) (pbl:itm list) of
598 SOME (_, _, _, fd, itm_) =>
600 (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
602 ((*tracing"### nxt_spec is_error NONE";*)
603 case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
605 SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
606 (Pbl, mk_additem fd ct'))
607 | NONE => (*pbl-items complete*)
608 if not preok then (Pbl, Refine_Problem pI')
610 if dI = e_domID then (Pbl, Specify_Theory dI')
611 else if pI = e_pblID then (Pbl, Specify_Problem pI')
612 else if mI = e_metID then (Pbl, Specify_Method mI')
614 case find_first (is_error o #5) met of
615 SOME (_,_,_,fd,itm_) =>
616 (Met, mk_delete (assoc_thy dI) fd itm_)
618 (case nxt_add (assoc_thy dI) oris mpc met of
619 SOME (fd,ct') => (*30.8.01: pre?!?*)
620 (Met, mk_additem fd ct')
622 ((*Solv 3.4.00*)Met, Apply_Method mI))))
624 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
625 ((*tracing"### nxt_spec Met"; *)
626 case find_first (is_error o #5) met of
627 SOME (_,_,_,fd,itm_) =>
628 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
630 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
631 SOME (fd,ct') => (Met, mk_additem fd ct')
633 ((*tracing"### nxt_spec Met: nxt_add NONE";*)
634 if dI = e_domID then (Met, Specify_Theory dI')
635 else if pI = e_pblID then (Met, Specify_Problem pI')
636 else if not preok then (Met, Specify_Method mI)
637 else (Met, Apply_Method mI)));
640 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
641 (2,[2],true,"#Find",Syn("empty"))];
644 fun is_field_correct sel d dscpbt =
645 case assoc (dscpbt, sel) of
647 | SOME ds => member op = ds d;
649 (*. update the itm_ already input, all..from ori .*)
650 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
652 fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
654 val ts' = union op = (ts_in itm_) ts;
655 val pval = pbl_ids' d ts'
656 (*WN.9.5.03: FIXXXME [#0, epsilon]
657 here would upd_penv be called for [#0, epsilon] etc. *)
658 val complete = if eq_set op = (ts', all) then true else false;
661 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
662 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
663 | (Syn c) => error ("ori_2itm wants to overwrite "^c)
664 | (Typ c) => error ("ori_2itm wants to overwrite "^c)
665 | (Inc _) => if complete
666 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
667 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
668 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
669 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
670 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
671 (* 28.1.00: not completely clear ---^^^ etc.*)
672 (* 4.9.01: Mis just copied---vvv *)
673 | (Mis _) => if complete
674 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
675 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
679 fun eq1 d (_,(d',_)) = (d = d');
680 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
683 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
684 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
685 pval: value for problem-environment _NOT_ checked for 'inter' --
686 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
687 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
688 (*. is_input ori itms <=>
689 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
690 (2) ori(ts) subset itm(ts) --- Err "already input"
691 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
692 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
693 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
695 fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
696 case find_first (eq1 d) pbt of
697 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
698 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
700 (case find_first (eq3 f d) itms of
701 SOME (_,_,_,_,itm_) =>
703 val ts' = inter op = (ts_in itm_) ts;
704 in if subset op = (ts, ts')
706 map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts') ^
707 " already input", e_itm) (*2*)
709 ori_2itm itm_ pid all (i,v,f,d,
710 subtract op = ts' ts)) (*3,4*)
712 | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[])))
713 pid all (i,v,f,d,ts)) (*1*)
715 | NONE => ("", ori_2itm (Sup (d,ts))
716 e_term all (i,v,f,d,ts));
718 fun test_types ctxt (d,ts) =
720 (*val s = !show_types; val _ = show_types:= true;*)
721 val opt = (try comp_dts) (d,ts);
722 val msg = case opt of
724 | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
726 ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
729 (*val _ = show_types:= s*)
734 fun maxl [] = error "maxl of []"
737 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
741 (*. is the input term t known in oris ?
742 give feedback on all(?) strange input;
743 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
744 (*WN.11.03: from lists*)
745 fun is_known ctxt sel ori t =
746 (* val (ori,t)=(oris,term_of ct);
749 val _ = tracing ("RM is_known: t=" ^ term2str t);
750 val ots = (distinct o flat o (map #5)) (ori:ori list);
751 val oids = ((map (fst o dest_Free)) o distinct o
752 flat o (map vars)) ots;
753 val (d,ts(*,pval*)) = split_dts t;
754 val ids = map (fst o dest_Free)
755 ((distinct o (flat o (map vars))) ts);
756 in if (subtract op = oids ids) <> []
757 then (("identifiers "^(strs2str' (subtract op = oids ids))^
758 " not in example"), e_ori_, [])
762 if not (subset op = (map typeless ts, map typeless ots))
765 (map (Print_Mode.setmp [] (Syntax.string_of_term
767 "' not in example (typeless)"), e_ori_, [])
768 else (case seek_orits ctxt sel ts ori of
769 ("", ori_ as (_,_,_,d,ts), all) =>
770 (case test_types ctxt (d,ts) of
771 "" => ("", ori_, all)
772 | msg => (msg, e_ori_, []))
773 | (msg,_,_) => (msg, e_ori_, []))
775 if member op = (map #4 ori) d
776 then seek_oridts ctxt sel (d,ts) ori
777 else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
778 " not in example", (0, [], sel, d, ts), [])
782 (*. for return-value of appl_add .*)
785 | Err of string; (*error-message*)
788 (** add an item to the model; check wrt. oris and pbt **)
789 (* in contrary to oris<>[] below, this part handles user-input
790 extremely acceptive, i.e. accept input instead error-msg *)
791 fun appl_add ctxt sel [] ppc pbt t =
793 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
794 in case parseNEW ctxt t of
795 NONE => Add (i, [], false, sel, Syn t)
797 let val (d, ts) = split_dts t';
798 in if d = e_term then
799 Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
800 (case find_first (eq1 d) pbt of
801 NONE => Add (i, [], true, sel, Sup (d,ts))
802 | SOME (f, (_, id)) =>
803 let fun eq2 d (i, _, _, _, itm_) =
804 d = (d_in itm_) andalso i <> 0;
805 in case find_first (eq2 d) ppc of
806 NONE => Add (i, [], true, f,
807 Cor ((d, ts), (id, pbl_ids' d ts))
809 | SOME (i', _, _, _, itm_) => if is_list_dsc d then
811 val in_itm = ts_in itm_;
812 val ts' = union op = ts in_itm;
813 val i'' = if in_itm = [] then i else i';
814 in Add (i'', [], true, f,
815 Cor ((d, ts'), (id, pbl_ids' d ts'))
818 Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
822 | appl_add ctxt sel oris ppc pbt str =
823 case parseNEW ctxt str of
824 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
825 | SOME t => case is_known ctxt sel oris t of
826 ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
828 | (msg, _) => Err msg)
829 | (msg, _, _) => Err msg;
831 > val (msg,itm) = is_notyet_input thy ppc all ori';
832 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
834 > val ts = ts_in itm_;
838 (** make oris from args of the stac SubProblem and from pbt **)
840 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
841 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
842 fun is_copy_named_idstr str =
843 case (rev o Symbol.explode) str of
844 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
845 "is_copy_named_idstr: " ^ str ^ " T"); true)
846 | _ => (tracing ((strs2str o (rev o Symbol.explode))
847 "is_copy_named_idstr: " ^ str ^ " F"); false);
848 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
850 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
851 fun is_copy_named_generating_idstr str =
852 if is_copy_named_idstr str
853 then case (rev o Symbol.explode) str of
854 "'"::"'"::"'"::_ => false
857 fun is_copy_named_generating (_, (_, t)) =
858 (is_copy_named_generating_idstr o free2str) t;
860 (*.split type-wrapper from scr-arg and build part of an ori;
861 an type-error is reported immediately, raises an exn,
862 subsequent handling of exn provides 2nd part of error message.*)
863 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
864 (* val (thy, (str, (dsc, _)), (ty $ var)) =
867 (cterm_of thy (dsc $ var);(*type check*)
868 SOME ((([1], str, dsc, (*[var]*)
869 split_dts' (dsc, var))): preori)(*:ori without leading #*))
870 handle e as TYPE _ =>
871 (tracing (dashs 70 ^ "\n"
872 ^"*** ERROR while creating the items for the model of the ->problem\n"
873 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
874 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
875 ^"*** description: "^(term_detail2str dsc)
876 ^"*** value: "^(term_detail2str var)
877 ^"*** typeconstructor in script: "^(term_detail2str ty)
878 ^"*** checked by theory: "^(theory2str thy)^"\n"
880 (*OldGoals.print_exn e; raises exn again*)
881 writeln (PolyML.makestring e);
883 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
886 (*.match each pat of the model-pattern with an actual argument;
887 precondition: copy-named vars are filtered out.*)
888 fun matc thy ([]:pat list) _ (oris:preori list) = oris
889 | matc thy pbt [] _ =
891 error ("actual arg(s) missing for '"^pats2str pbt
892 ^"' i.e. should be 'copy-named' by '*_._'"))
893 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
894 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
895 (thy, pbt', ags, []);
897 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
898 (thy, pbt, ags, (oris @ [ori]));
900 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
901 else(*..del?*) let val opt = mtc thy p a;
903 (* val SOME ori = mtc thy p a;
905 SOME ori => matc thy pbt ags (oris @ [ori])
906 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
908 (* run subp-rooteq.sml until Init_Proof before ...
909 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
910 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
912 other vars as in mtc ..
913 > matc thy (drop_last pbt) ags [];
914 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
917 (* generate a new variable "x_i" name from a related given one "x"
918 by use of oris relating "v_i_" (is_copy_named!) to "v_"
919 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
921 (* generate a new variable "x_i" name from a related given one "x"
922 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
923 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
924 but leave is_copy_named_generating as is, e.t. ss''' *)
925 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
926 (if is_copy_named_generating p
927 then (*WN051014 kept strange old code ...*)
928 let fun sel (_,_,d,ts) = comp_ts (d, ts)
929 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
930 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
931 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
932 val vals = map sel oris
933 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
934 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
935 else ([1], field, dsc, [t])
937 handle _ => error ("cpy_nam: for "^(term2str t));
939 (*.match the actual arguments of a SubProblem with a model-pattern
940 and create an ori list (in root-pbl created from formalization).
941 expects ags:pats = 1:1, while copy-named are filtered out of pats;
942 if no 1:1 the exn raised by matc/mtc and handled at call.
943 copy-named pats are appended in order to get them into the model-items.*)
944 fun match_ags thy (pbt:pat list) ags =
945 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
946 val pbt' = filter_out is_copy_named pbt;
947 val cy = filter is_copy_named pbt;
948 val oris' = matc thy pbt' ags [];
949 val cy' = map (cpy_nam pbt' oris') cy;
950 val ors = add_id (oris' @ cy');
951 (*appended in order to get ^^^^^ into the model-items*)
952 in (map flattup ors):ori list end;
954 (*.report part of the error-msg which is not available in match_args.*)
955 fun match_ags_msg pI stac ags =
956 let (*val s = !show_types
957 val _ = show_types:= true*)
958 val pats = (#ppc o get_pbt) pI
959 val msg = (dots 70^"\n"
960 ^"*** problem "^strs2str pI^" has the ...\n"
961 ^"*** model-pattern "^pats2str pats^"\n"
962 ^"*** stac '"^term2str stac^"' has the ...\n"
963 ^"*** arg-list "^terms2str ags^"\n"
965 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
966 (*val _ = show_types:= s*)
970 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
971 fun vars_of_pbl_ pbl_ =
972 let fun var_of_pbl_ (gfr,(dsc,t)) = t
973 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
974 fun vars_of_pbl_' pbl_ =
975 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
976 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
978 fun overwrite_ppc thy itm ppc =
980 fun repl ppc' (_,_,_,_,itm_) [] =
981 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
983 | repl ppc' itm (p::ppc) =
984 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
985 else repl (ppc' @ [p]) itm ppc
986 in repl [] itm ppc end;
988 (*10.3.00: insert the already compiled itm into model;
989 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
992 fun insert_ppc thy itm ppc =
994 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
995 | eq_untouched _ _ = false;
998 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
999 case seek_ppc (#1 itm) ppc of
1000 (* val SOME xxx = seek_ppc (#1 itm) ppc;
1002 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
1003 overwrite_ppc thy itm ppc
1004 | NONE => (ppc @ [itm]));
1005 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
1007 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
1008 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
1010 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
1011 (d_in itm_) = (d_in iitm_);
1012 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
1013 handles superfluous items carelessly*)
1014 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
1016 > gen_ins' eee (4,[1,3,5,7]);
1017 val it = [1, 3, 5, 7, 4] : int list*)
1020 (*. output the headline to a ppc .*)
1021 fun header p_ pI mI =
1022 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1024 | pos => error ("header called with "^ pos_2str pos);
1027 fun specify_additem sel (ct,_) (p,Met) c pt =
1029 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1030 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1031 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1032 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1033 val cpI = if pI = e_pblID then pI' else pI;
1034 val cmI = if mI = e_metID then mI' else mI;
1035 val {ppc,pre,prls,...} = get_met cmI;
1036 in case appl_add (thy2ctxt thy) sel oris met ppc ct of
1037 Add itm (*..union old input *) =>
1038 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1040 val met' = insert_ppc thy itm met;
1041 (*val pt' = update_met pt p met';*)
1042 val ((p,Met),_,_,pt') =
1043 generate1 thy (case sel of
1044 "#Given" => Add_Given' (ct, met')
1045 | "#Find" => Add_Find' (ct, met')
1046 | "#Relate"=> Add_Relation'(ct, met'))
1047 (Uistate, e_ctxt) (p,Met) pt
1048 val pre' = check_preconds thy prls pre met'
1049 val pb = foldl and_ (true, map fst pre')
1050 (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
1052 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1053 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1054 in ((p,p_), ((p,p_),Uistate),
1055 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1056 (Method cmI, itms2itemppc thy met' pre'))),
1059 let val pre' = check_preconds thy prls pre met
1060 val pb = foldl and_ (true, map fst pre')
1061 (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
1063 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1064 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1065 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1069 | specify_additem sel (ct,_) (p,p_(*Frm, Pbl*)) c pt =
1071 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1072 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1073 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1074 val cpI = if pI = e_pblID then pI' else pI;
1075 val cmI = if mI = e_metID then mI' else mI;
1076 val {ppc,where_,prls,...} = get_pbt cpI;
1077 in case appl_add (thy2ctxt thy) sel oris pbl ppc ct of
1078 Add itm (*..union old input *) =>
1079 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1082 (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
1083 val pbl' = insert_ppc thy itm pbl
1084 val ((p,Pbl),_,_,pt') =
1085 generate1 thy (case sel of
1086 "#Given" => Add_Given' (ct, pbl')
1087 | "#Find" => Add_Find' (ct, pbl')
1088 | "#Relate"=> Add_Relation'(ct, pbl'))
1089 (Uistate, e_ctxt) (p,Pbl) pt
1090 val pre = check_preconds thy prls where_ pbl'
1091 val pb = foldl and_ (true, map fst pre)
1092 (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
1094 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1095 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1096 val ppc = if p_= Pbl then pbl' else met;
1097 in ((p,p_), ((p,p_),Uistate),
1098 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1100 itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1103 let val pre = check_preconds thy prls where_ pbl
1104 val pb = foldl and_ (true, map fst pre)
1105 (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
1107 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1108 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1109 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1111 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1112 val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1116 val (msg,itm) = appl_add thy sel oris ppc ct;
1117 val (Cor(d,ts)) = #5 itm;
1124 (* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1125 specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1127 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1128 let (* either """"""""""""""" all empty or complete *)
1129 val thy = assoc_thy dI';
1130 val (istate_, ctxt) = (#ppc o get_pbt) pI' |> prep_ori fmz thy;
1131 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1133 val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1134 (oris,(dI',pI',mI'),e_term);
1135 val {ppc,prls,where_,...} = get_pbt pI'
1136 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1137 val pt = update_pbl pt [] pbl;
1138 val pre = check_preconds thy prls where_ pbl
1139 val pb = foldl and_ (true, map fst pre)*)
1140 val (pbl, pre, pb) = ([], [], false)
1143 (([],Pbl), (([],Pbl),Uistate),
1144 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1145 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1146 Refine_Tacitly pI', Safe,pt)
1148 (([],Pbl), (([],Pbl),Uistate),
1149 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1150 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1154 (*ONLY for STARTING modeling phase*)
1155 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1156 let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
1158 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
1160 val thy' = if dI = e_domID then dI' else dI
1161 val thy = assoc_thy thy'
1162 val {ppc,prls,where_,...} = get_pbt pI'
1163 val pre = check_preconds thy prls where_ pbl
1164 val pb = foldl and_ (true, map fst pre)
1165 val ((p,_),_,_,pt) =
1166 generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
1167 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1168 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1169 in ((p,Pbl), ((p,p_),Uistate),
1170 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1171 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1174 (*. called only if no_met is specified .*)
1175 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1176 let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
1178 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
1180 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1181 (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
1182 (*val pt = update_pbl pt p pbl;
1183 val pt = update_orispec pt p
1184 (string_of_thy thy, pIre,
1185 if length met = 0 then e_metID else hd met);*)
1186 val (domID, metID) = (string_of_thy thy,
1187 if length met = 0 then e_metID else hd met)
1188 val ((p,_),_,_,pt) =
1189 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1190 (Uistate, e_ctxt) pos pt
1191 (*val pre = check_preconds thy prls where_ pbl
1192 val pb = foldl and_ (true, map fst pre)*)
1193 val (pbl, pre, pb) = ([], [], false)
1194 in ((p,Pbl), (pos,Uistate),
1195 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1196 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1197 Model_Problem, Safe, pt) end
1199 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1200 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
1201 (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1202 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1203 Model_Problem, Safe, pt) end
1205 (* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
1206 val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
1208 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1209 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1210 meth=met, ...}) = get_obj I pt p;
1211 (*val pt = update_pbl pt p itms;
1212 val pt = update_pblID pt p pI;*)
1213 val thy = assoc_thy dI
1214 val ((p,Pbl),_,_,pt)=
1215 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
1216 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1217 val mI'' = if mI=e_metID then mI' else mI;
1218 (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
1219 val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1220 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1221 in ((p,Pbl), (pos,Uistate),
1222 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1223 (Problem pI, itms2itemppc dI'' itms pre))),
1225 (* val Specify_Method' mID = nxt; val (p,_) = p;
1226 val Specify_Method' mID = m;
1227 specify (Specify_Method' mID) (p,p_) c pt;
1229 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1230 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1231 meth=met, ...}) = get_obj I pt p;
1232 val {ppc,pre,prls,...} = get_met mID
1233 val thy = assoc_thy dI
1234 val oris = add_field' thy ppc oris;
1235 (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1236 val dI'' = if dI=e_domID then dI' else dI;
1237 val pI'' = if pI = e_pblID then pI' else pI;
1238 val met = if met=[] then pbl else met;
1239 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1240 (*val pt = update_met pt p itms;
1241 val pt = update_metID pt p mID*)
1243 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1244 (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
1245 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1246 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1247 in (pos, (pos,Uistate),
1248 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1249 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1251 (* val Add_Find' ct = nxt; val sel = "#Find";
1253 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1254 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1255 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1256 (* val Specify_Theory' domID = m;
1257 val (Specify_Theory' domID, (p,p_)) = (m, pos);
1259 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1260 let val p_ = case p_ of Met => Met | _ => Pbl
1261 val thy = assoc_thy domID;
1262 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1263 probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
1264 val mppc = case p_ of Met => met | _ => pbl;
1265 val cpI = if pI = e_pblID then pI' else pI;
1266 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1267 val cmI = if mI = e_metID then mI' else mI;
1268 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1271 Met => (check_preconds thy mer mwh met)
1272 | _ => (check_preconds thy per pwh pbl)
1273 val pb = foldl and_ (true, map fst pre)
1276 (*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1277 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1278 (pbl,met) (ppc,mpc) (dI,pI,mI);
1279 in ((p,p_), (pos,Uistate),
1280 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1281 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1283 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1285 (*val pt = update_domID pt p domID;11.8.03*)
1286 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1287 (Uistate, e_ctxt) (p,p_) pt
1288 (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1289 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1290 (ppc,mpc) (domID,pI,mI);
1291 in ((p,p_), (pos,Uistate),
1292 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1293 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1296 (* itms2itemppc thy [](*mpc*) pre
1298 | specify m' _ _ _ =
1299 error ("specify: not impl. for "^tac_2str m');
1301 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1302 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1304 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1306 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1307 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1308 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1309 val cpI = if pI = e_pblID then pI' else pI;
1310 in case appl_add (thy2ctxt thy) sel oris pbl ((#ppc o get_pbt) cpI) ct of
1311 Add itm (*..union old input *) =>
1312 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1315 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1316 val pbl' = insert_ppc thy itm pbl
1319 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1320 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1321 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1322 val ((p,Pbl),c,_,pt') =
1323 generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
1324 in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate' end
1327 (*TODO.WN03 pass error-msgs to the frontend..
1328 FIXME ..and dont abuse a tactic for that purpose*)
1330 Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1331 (e_pos', (e_istate, e_ctxt)))], [], ptp)
1334 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1335 val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1337 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1339 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1340 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1341 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1342 val cmI = if mI = e_metID then mI' else mI;
1343 in case appl_add (thy2ctxt thy) sel oris met ((#ppc o get_met) cmI) ct of
1344 Add itm (*..union old input *) =>
1345 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1347 val met' = insert_ppc thy itm met;
1350 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1351 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1352 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1353 val ((p,Met),c,_,pt') =
1354 generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
1355 in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
1357 | Err msg => ([(*tacis*)], [], ptp)
1358 (*nxt_me collects tacis until not hide; here just no progress*)
1362 val (msg,itm) = appl_add thy sel oris ppc ct;
1363 val (Cor(d,ts)) = #5 itm;
1368 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1369 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1370 handle _ => error ("ori2Coritm: dsc "^
1372 "in ori, but not in pbt")
1374 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1375 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1376 (find_first (eq1 d))) pbt,ts))):itm)
1377 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1378 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1381 (*filter out oris which have same description in itms*)
1382 fun filter_outs oris [] = oris
1383 | filter_outs oris (i::itms) =
1384 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1385 (#4:ori -> term)) oris;
1386 in filter_outs ors itms end;
1388 fun memI a b = member op = a b;
1389 (*filter oris which are in pbt, too*)
1390 fun filter_pbt oris pbt =
1391 let val dscs = map (fst o snd) pbt
1392 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1394 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1395 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1397 fun x mem [] = false
1398 | x mem (y :: ys) = x = y orelse x mem ys;
1400 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1401 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1403 let val vat = max_vt pits;
1405 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1406 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1407 val os = filter_outs ors itms;
1408 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1409 in itms @ (map (ori2Coritm met) os) end
1414 (*.complete model and guard of a calc-head .*)
1416 fun x mem [] = false
1417 | x mem (y :: ys) = x = y orelse x mem ys;
1419 fun complete_mod_ (oris, mpc, ppc, probl) =
1420 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1421 val vat = if probl = [] then 1 else max_vt probl
1422 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1423 val pors = filter_outs pors pits (*which are in pbl already*)
1424 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1426 val pits = pits @ (map (ori2Coritm ppc) pors)
1427 val mits = complete_metitms oris pits [] mpc
1431 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1432 (if dI = e_domID then odI else dI,
1433 if pI = e_pblID then opI else pI,
1434 if mI = e_metID then omI else mI):spec;
1437 (*.find a next applicable tac (for calcstate) and update ptree
1438 (for ev. finding several more tacs due to hide).*)
1439 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1440 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1441 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1442 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1444 val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1445 val (dI, pI, mI) = some_spec ospec spec
1446 val thy = assoc_thy dI
1447 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1448 val {cas, ppc, ...} = get_pbt pI
1449 val pbl = init_pbl ppc (* fill in descriptions *)
1450 (*----------------if you think, this should be done by the Dialog
1451 in the java front-end, search there for WN060225-modelProblem----*)
1452 val (pbl, met) = case cas of NONE => (pbl, [])
1453 | _ => complete_mod_ (oris, mpc, ppc, probl)
1454 (*----------------------------------------------------------------*)
1455 val tac_ = Model_Problem' (pI, pbl, met)
1456 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
1457 in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1459 (* val Add_Find ct = tac;
1461 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1462 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1463 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1465 (*. called only if no_met is specified .*)
1466 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1467 let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1468 val opt = refine_ori oris pI
1471 let val {met,ppc,...} = get_pbt pI'
1472 val pbl = init_pbl ppc
1473 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1474 val mI = if length met = 0 then e_metID else hd met
1475 val thy = assoc_thy dI
1477 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1478 (Uistate, e_ctxt) pos pt
1479 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1480 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1481 | NONE => ([], [], ptp)
1484 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1485 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1486 probl, ...}) = get_obj I pt p
1487 val thy = if dI' = e_domID then dI else dI'
1488 in case refine_pbl (assoc_thy thy) pI probl of
1489 NONE => ([], [], ptp)
1490 | SOME (rfd as (pI',_)) =>
1491 let val (pos,c,_,pt) =
1492 generate1 (assoc_thy thy)
1493 (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1494 in ([(Refine_Problem pI, Refine_Problem' rfd,
1495 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1498 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1499 let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1500 probl, ...}) = get_obj I pt p;
1501 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1502 val {ppc,where_,prls,...} = get_pbt pI
1503 val pbl as (_,(itms,_)) =
1504 if pI'=e_pblID andalso pI=e_pblID
1505 then (false, (init_pbl ppc, []))
1506 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1507 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1508 val ((p,Pbl),c,_,pt)=
1509 generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
1510 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1511 (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1513 (*transfers oris (not required in pbl) to met-model for script-env
1514 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1515 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1516 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1517 meth=met, ...}) = get_obj I pt p;
1518 val {ppc,pre,prls,...} = get_met mID
1519 val thy = assoc_thy dI
1520 val oris = add_field' thy ppc oris;
1521 val dI'' = if dI=e_domID then dI' else dI;
1522 val pI'' = if pI = e_pblID then pI' else pI;
1523 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1524 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1526 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1527 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1528 (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1530 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1531 let val (dI',_,_) = get_obj g_spec pt p
1533 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1534 (Uistate, e_ctxt) pos pt
1535 in (*FIXXXME: check if pbl can still be parsed*)
1536 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1539 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1540 let val (dI',_,_) = get_obj g_spec pt p
1542 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1543 (Uistate, e_ctxt) pos pt
1544 in (*FIXXXME: check if met can still be parsed*)
1545 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1549 error ("nxt_specif: not impl. for "^tac2str m');
1551 (*.get the values from oris; handle the term list w.r.t. penv.*)
1554 fun x mem [] = false
1555 | x mem (y :: ys) = x = y orelse x mem ys;
1557 fun vals_of_oris oris =
1558 ((map (mkval' o (#5:ori -> term list))) o
1559 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1564 (* create a calc-tree with oris via an cas.refined pbl *)
1565 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1566 if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1567 let val {cas, met, ppc, thy, ...} = get_pbt pI
1568 val dI = if dI = "" then theory2theory' thy else dI
1569 val thy = assoc_thy dI
1570 val mI = if mI = [] then hd met else mI
1571 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1572 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1573 ([], (dI,pI,mI), hdl)
1574 val pt = update_spec pt [] (dI,pI,mI)
1575 val pits = init_pbl' ppc
1576 val pt = update_pbl pt [] pits
1577 in ((pt, ([] ,Pbl)), []) : calcstate end
1578 else if mI <> [] then (* from met-browser *)
1579 let val {ppc,...} = get_met mI
1580 val dI = if dI = "" then "Isac" else dI
1581 val thy = assoc_thy dI;
1582 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1583 ([], (dI,pI,mI), e_term(*FIXME met*));
1584 val pt = update_spec pt [] (dI,pI,mI);
1585 val mits = init_pbl' ppc;
1586 val pt = update_met pt [] mits;
1587 in ((pt, ([], Met)), []) : calcstate end
1588 else (* new example, pepare for interactive modeling *)
1589 let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1590 ([], e_spec, e_term)
1591 in ((pt,([],Pbl)), []) : calcstate end
1592 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1593 let (* both """"""""""""""""""""""""" either empty or complete *)
1594 val thy = assoc_thy dI
1595 val (pI, pors, mI) =
1597 then let val pors = get_pbt pI |> #ppc |> prep_ori fmz thy |> #1;
1598 val pI' = refine_ori' pors pI;
1599 in (pI', pors(*refinement over models with diff.precond only*),
1600 (hd o #met o get_pbt) pI') end
1601 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
1602 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1603 val dI = theory2theory' (maxthy thy thy');
1604 val ctxt = prep_ori fmz thy ppc |> #2;
1605 val hdl = case cas of
1606 NONE => pblterm dI pI
1607 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1608 ~~~ vals_of_oris pors) t;
1609 val (pt, _) = cappend_problem e_ptree [] (Uistate, ctxt) (fmz, (dI, pI, mI))
1610 (pors, (dI, pI, mI), hdl)
1611 in ((pt, ([], Pbl)),
1612 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1618 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1619 (* case appl_spec p pt m of /// 19.1.00
1620 Notappl e => Error' (Error_ e)
1622 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1626 (*fun tag_form thy (formal, given) = cterm_of thy
1627 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1628 fun tag_form thy (formal, given) =
1629 (let val gf = (head_of given) $ formal;
1630 val _ = cterm_of thy gf
1633 error ("calchead.tag_form: " ^
1634 Print_Mode.setmp [] (Syntax.string_of_term
1635 (thy2ctxt thy)) given ^ " .. " ^
1636 Print_Mode.setmp [] (Syntax.string_of_term
1637 (thy2ctxt thy)) formal ^
1638 " ..types do not match");
1639 (* val formal = (the o (parse thy)) "[R::real]";
1640 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1641 > tag_form thy (formal, given);
1642 val it = "fixed_values [R]" : cterm
1645 fun chktyp thy (n, fs, gs) =
1646 ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1648 (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1650 tag_form thy (nth n fs, nth n gs));
1651 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1653 (* #####################################################
1654 find the failing item:
1656 > val tag__form = chktyp (n,formals,givens);
1657 > (type_of o term_of o (nth n)) formals;
1658 > (type_of o term_of o (nth n)) givens;
1659 > atomty ((term_of o (nth n)) formals);
1660 > atomty ((term_of o (nth n)) givens);
1661 > atomty (term_of tag__form);
1662 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1663 ##################################################### *)
1665 (* #####################################################
1667 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1668 val formals = map (the o (parse thy)) origin;
1670 val given = ["equation (lhs=rhs)",
1671 "bound_variable bdv", (* TODO type *)
1673 val where_ = ["e is_root_equation_in bdv",
1675 "apx is_const_expr"];
1676 val find = ["L::rat set"];
1677 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1678 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1679 val givens = map (the o (parse thy)) given;
1681 val tag__forms = chktyps (formals, givens);
1682 map ((atomty) o term_of) tag__forms;
1683 ##################################################### *)
1686 (* check pbltypes, announces one failure a time *)
1687 (*fun chk_vars ctppc =
1688 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1689 appc flat (mappc (vars o term_of) ctppc)
1690 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1691 else if (re\\(gi union fi)) <> []
1692 then ("re\\(gi union fi)",re\\(gi union fi))
1693 else ("ok",[]) end;*)
1694 fun chk_vars ctppc =
1695 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1696 appc flat (mappc vars ctppc)
1697 val chked = subtract op = gi wh
1698 in if chked <> [] then ("wh\\gi", chked)
1699 else let val chked = subtract op = (union op = gi fi) re
1701 then ("re\\(gi union fi)", chked)
1706 (* check a new pbltype: variables (Free) unbound by given, find*)
1707 fun unbound_ppc ctppc =
1708 let val {Given=gi,Find=fi,Relate=re,...} =
1709 appc flat (mappc vars ctppc)
1710 in distinct (*re\\(gi union fi)*)
1711 (subtract op = (union op = gi fi) re) end;
1713 > val org = {Given=["[R=(R::real)]"],Where=[],
1714 Find=["[A::real]"],With=[],
1715 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1717 > val ctppc = mappc (the o (parse thy)) org;
1718 > unbound_ppc ctppc;
1719 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1723 (* f, a binary operator, is nested rightassociative *)
1726 fun fld f (x::[]) = x
1727 | fld f (x::x'::[]) = f (x',x)
1728 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1729 in ((fld f) o rev) xs end;
1731 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1732 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1733 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1734 > cterm_of thy conj;
1735 val it = "(a = b & c = d) & e = f" : cterm
1738 (* f, a binary operator, is nested leftassociative *)
1739 fun foldl1 f (x::[]) = x
1740 | foldl1 f (x::x'::[]) = f (x,x')
1741 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1743 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1744 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1745 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1746 > cterm_of thy conj;
1747 val it = "a = b & c = d & e = f & g = h" : cterm
1751 (* called only once, if a Subproblem has been located in the script*)
1752 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
1753 (* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
1757 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1758 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1759 (*all stored in tac_ itms ^^^^^^^^^^*)
1760 | nxt_model_pbl tac_ _ =
1761 error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1762 (* run subp_rooteq.sml ''
1763 until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
1764 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1765 (last_elem o drop_last) ets'';
1766 > val mst = (last_elem o drop_last) ets'';
1767 > nxt_model_pbl mst;
1768 val it = Refine_Tacitly ["univariate","equation"] : tac
1771 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1772 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1773 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1776 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1777 + met from fmz; assumes pos on PblObj, meth = [].*)
1778 fun complete_mod (pt, pos as (p, p_):pos') =
1779 (* val (pt, (p, _)) = (pt, p);
1780 val (pt, (p, _)) = (pt, pos);
1782 let val _= if p_ <> Pbl
1783 then tracing("###complete_mod: only impl.for Pbl, called with "^
1784 pos'2str pos) else ()
1785 val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
1787 val (dI,pI,mI) = some_spec ospec spec
1788 val mpc = (#ppc o get_met) mI
1789 val ppc = (#ppc o get_pbt) pI
1790 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1791 val pt = update_pblppc pt p pits
1792 val pt = update_metppc pt p mits
1793 in (pt, (p,Met):pos') end
1795 (*| complete_mod (pt, pos as (p, Met):pos') =
1796 error ("###complete_mod: only impl.for Pbl, called with "^
1799 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1800 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1801 fun all_modspec (pt, (p,_):pos') =
1802 (* val (pt, (p,_)) = ptp;
1804 let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1805 ...}) = get_obj I pt p;
1806 val thy = assoc_thy dI;
1807 val {ppc,...} = get_met mI;
1808 val mors = prep_ori fmz_ thy ppc |> #1;
1809 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1810 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1811 val pt = update_spec pt p (dI,pI,mI);
1812 in (pt, (p,Met): pos') end;
1814 (*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1815 fun is_complete_mod_ ([]: itm list) = false
1816 | is_complete_mod_ itms =
1817 foldl and_ (true, (map #3 itms));
1818 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1819 if (is_pblobj o (get_obj I pt)) p
1820 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1821 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1822 | is_complete_mod (pt, pos as (p, Met)) =
1823 if (is_pblobj o (get_obj I pt)) p
1824 then (is_complete_mod_ o (get_obj g_met pt)) p
1825 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1826 | is_complete_mod (_, pos) =
1827 error ("is_complete_mod called by "^pos'2str pos^
1828 " (should be Pbl or Met)");
1830 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1831 fun is_complete_spec (pt, pos as (p,_): pos') =
1832 if (not o is_pblobj o (get_obj I pt)) p
1833 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1834 else let val (dI,pI,mI) = get_obj g_spec pt p
1835 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1836 (*.complete empty items in specification from origin (pbl, met ev.refined);
1837 assumes 'is_complete_mod'.*)
1838 fun complete_spec (pt, pos as (p,_): pos') =
1839 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1840 val pt = update_spec pt p (some_spec ospec spec)
1843 fun is_complete_modspec ptp =
1844 is_complete_mod ptp andalso is_complete_spec ptp;
1849 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1850 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1852 let val (_,_,metID) = get_somespec' spec spec'
1854 if metID = e_metID then []
1855 else let val {prls,pre=where_,...} = get_met metID
1856 val pre = check_preconds' prls where_ meth 0
1858 val allcorrect = is_complete_mod_ meth
1859 andalso foldl and_ (true, (map #1 pre))
1860 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1861 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1862 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1864 let val (_,pI,_) = get_somespec' spec spec'
1866 if pI = e_pblID then []
1867 else let val {prls,where_,cas,...} = get_pbt pI
1868 val pre = check_preconds' prls where_ probl 0
1870 val allcorrect = is_complete_mod_ probl
1871 andalso foldl and_ (true, (map #1 pre))
1872 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1875 fun pt_form (PrfObj {form,...}) = Form form
1876 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1877 let val (dI, pI, _) = get_somespec' spec spec'
1878 val {cas,...} = get_pbt pI
1880 NONE => Form (pblterm dI pI)
1881 | SOME t => Form (subst_atomic (mk_env probl) t)
1883 (*vvv takes the tac _generating_ the formula=result, asm ok....
1884 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1886 if null asm then NONE else SOME asm,
1888 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1889 let val (_,_,metID) = some_spec ospec spec
1891 if null asm then NONE else SOME asm,
1892 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1893 -------------------------------------------------------------------------*)
1896 (*.pt_extract returns
1897 # the formula at pos
1898 # the tactic applied to this formula
1899 # the list of assumptions generated at this formula
1900 (by application of another tac to the preceding formula !)
1901 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1902 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1903 fun pt_extract (pt,([],Res)) =
1904 (* val (pt,([],Res)) = ptp;
1906 let val (f, asm) = get_obj g_result pt []
1907 in (Form f, NONE, asm) end
1910 | pt_extract (pt,(p,Res)) =
1911 (* val (pt,(p,Res)) = ptp;
1913 let val (f, asm) = get_obj g_result pt p
1914 val tac = if last_onlev pt p
1915 then if is_pblobj' pt (lev_up p)
1916 then let val (PblObj{spec=(_,pI,_),...}) =
1917 get_obj I pt (lev_up p)
1918 in if pI = e_pblID then NONE
1919 else SOME (Check_Postcond pI) end
1920 else SOME End_Trans (*WN0502 TODO for other branches*)
1921 else let val p' = lev_on p
1922 in if is_pblobj' pt p'
1923 then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1925 in SOME (Subproblem (dI, pI)) end
1926 else if f = get_obj g_form pt p'
1927 then SOME (get_obj g_tac pt p')
1928 (*because this Frm ~~~is not on worksheet*)
1929 else SOME (Take (term2str (get_obj g_form pt p')))
1931 in (Form f, tac, asm) end
1933 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1934 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1935 val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
1937 let val ppobj = get_obj I pt p
1938 val f = if is_pblobj ppobj then pt_model ppobj p_
1939 else get_obj pt_form pt p
1940 val tac = g_tac ppobj
1941 in (f, SOME tac, []) end;
1944 (**. get the formula from a ctree-node:
1945 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1946 take res from all other PrfObj's .**)
1947 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1948 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1949 [("headline", (p, Frm), h),
1950 ("stepform", (p, Res), r)]
1951 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1952 [("stepform", (p, Frm), form),
1953 ("stepform", (p, Res), r)];
1955 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1956 [("stepform", (p, Res), r)]
1958 (*assumes to take whole level, in particular hd -- for use in interSteps*)
1959 fun get_formress fs p [] = flat fs
1960 | get_formress fs p (nd::nds) =
1961 (* start with 'form+res' and continue with trying 'res' only*)
1962 get_forms (fs @ [formres p nd]) (lev_on p) nds
1963 and get_forms fs p [] = flat fs
1964 | get_forms fs p (nd::nds) =
1966 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1967 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1968 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1969 (* continue with trying 'res' only*)
1970 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1972 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1973 (*WN050219 made robust against _'to' below or after Complete nodes
1974 by handling exn caused by move_dn*)
1975 (*WN0401 this functionality belongs to ctree.sml,
1976 but fetching a calc_head requires calculations defined in modspec.sml
1977 transfer to ME/me.sml !!!
1978 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1979 is returned !!!!!!!!!!!!!
1981 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1982 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1983 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1987 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1991 | eq_pos' _ _ = false;
1993 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
1994 total ordering Position#compareTo(Position p) in the java-code
1995 val get_interval = fn
1996 : pos' -> : from is "move_up 1st-element" to return
1997 pos' -> : to the last element to be returned; from < to
1998 int -> : level: 0 gets the flattest sub-tree possible
1999 >999 gets the deepest sub-tree possible
2001 (pos' * : of the formula
2002 Term.term) : the formula
2005 fun get_interval from to level pt =
2006 (* val (from,level) = (f,lev);
2007 val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
2009 let fun get_inter c (from:pos') (to:pos') lev pt =
2010 (* val (c, from, to, lev) = ([], from, to, level);
2011 ------for recursion.......
2012 val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
2014 if eq_pos' from to orelse from = ([],Res)
2015 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
2016 if 'to' has values NOT generated by move_dn, see systest/me.sml
2017 TODO.WN0501: introduce an order on pos' and check "from > to"..
2018 ...there is an order in Java!
2019 WN051224 the hack got worse with returning term instead ptform*)
2020 then let val (f,_,_) = pt_extract (pt, from)
2022 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2023 | Form t => c @ [(from, t)]
2026 if lev < lev_of from
2027 then (get_inter c (move_dn [] pt from) to lev pt)
2028 handle (PTREE _(*from move_dn too far*)) => c
2029 else let val (f,_,_) = pt_extract (pt, from)
2030 val term = case f of
2031 ModSpec (_,_,headline,_,_,_)=> headline
2033 in (get_inter (c @ [(from, term)])
2034 (move_dn [] pt from) to lev pt)
2035 handle (PTREE _(*from move_dn too far*))
2036 => c @ [(from, term)] end
2037 in get_inter [] from to level pt end;
2040 fun posform2str (pos:pos', form) =
2041 "("^ pos'2str pos ^", "^
2043 Form f => term2str f
2044 | ModSpec c => term2str (#3 c(*the headline*)))
2046 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2047 (map posform2str)) pfs;
2048 fun posterm2str (pos:pos', t) =
2049 "("^ pos'2str pos ^", "^term2str t^")";
2050 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2051 (map posterm2str)) pfs;
2054 (*WN050225 omits the last step, if pt is incomplete*)
2056 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
2058 (*.get a calchead from a PblObj-node in the ctree;
2059 preconditions must be calculated.*)
2060 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
2061 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
2063 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2064 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
2065 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
2066 | get_ocalhd (pt, pos' as (p,Met):pos') =
2067 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2070 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2071 val pre = check_preconds (assoc_thy"Isac") prls pre meth
2072 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
2074 (*.at the activeFormula set the Model, the Guard and the Specification
2075 to empty and return a CalcHead;
2076 the 'origin' remains (for reconstructing all that).*)
2077 fun reset_calchead (pt, pos' as (p,_):pos') =
2078 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
2079 val pt = update_pbl pt p []
2080 val pt = update_met pt p []
2081 val pt = update_spec pt p e_spec
2082 in (pt, (p,Pbl):pos') end;
2084 (*---------------------------------------------------------------------
2088 ---------------------------------------------------------------------*)