intermed. context integration: parse replaced in some cases
- seek_oridts cleanup
- appl_add update
- appl_add' update
- prep_ori cleanup
- Equation.thy update
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 structure CalcHead (**): CALC_HEAD(**) =
214 (*.the state wich is stored after each step of calculation; it contains
215 the calc-state and a list of [tac,istate](="tacis") to be applied next.
216 the last_elem tacis is the first to apply to the calc-state and
217 the (only) one shown to the front-end as the 'proposed tac'.
218 the calc-state resulting from the application of tacis is not stored,
219 because the tacis hold enough information for efficiently rebuilding
220 this state just by "fun generate ".*)
222 (ptree * pos') * (*the calc-state to which the tacis could be applied*)
223 (taci list); (*ev. several (hidden) steps;
224 in REVERSE order: first tac_ to apply is last_elem*)
225 val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
227 (*the state used during one calculation within the mathengine; it contains
228 a list of [tac,istate](="tacis") which generated the the calc-state;
229 while this state's tacis are extended by each (internal) step,
230 the calc-state is used for creating new nodes in the calc-tree
231 (eg. applicable_in requires several particular nodes of the calc-tree)
232 and then replaced by the the newly created;
233 on leave of the mathengine the resuing calc-state is dropped anyway,
234 because the tacis hold enought information for efficiently rebuilding
235 this state just by "fun generate ".*)
237 taci list * (*cas. several (hidden) steps;
238 in REVERSE order: first tac_ to apply is last_elem*)
239 pos' list * (*a "continuous" sequence of pos',
240 deleted by application of taci list*)
241 (ptree * pos'); (*the calc-state resulting from the application of tacis*)
242 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
244 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
245 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
246 | f_mout thy _ = error "f_mout: not called with formula";
249 (*.is the calchead complete ?.*)
250 fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
251 foldl and_ (true, map #3 its) andalso
252 foldl and_ (true, map #1 pre) andalso
253 dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
256 (* make a term 'typeless' for comparing with another 'typeless' term;
257 'type-less' usually is illtyped *)
258 fun typeless (Const(s,_)) = (Const(s,e_type))
259 | typeless (Free(s,_)) = (Free(s,e_type))
260 | typeless (Var(n,_)) = (Var(n,e_type))
261 | typeless (Bound i) = (Bound i)
262 | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
263 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
265 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
266 > val (_,t1) = split_dsc_t hs (term_of ct);
267 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
268 > val (_,t2) = split_dsc_t hs (term_of ct);
269 > typeless t1 = typeless t2;
275 (*.to an input (d,ts) find the according ori and insert the ts.*)
276 (*WN.11.03: + dont take first inter<>[]*)
277 fun seek_oridts ctxt sel (d,ts) [] =
278 ("seek_oridts: input ('" ^
279 (Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))) ^
280 "') not found in oris (typed)",
283 | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =
284 if sel = sel' andalso d = d' andalso (inter op = ts ts') <> [] then
285 ("", (id, vat, sel, d, inter op = ts ts'), ts') else
286 seek_oridts ctxt sel (d, ts) oris;
288 (*.to an input (_,ts) find the according ori and insert the ts.*)
289 fun seek_orits ctxt sel ts [] =
290 ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
292 "') not found in oris (typed)", e_ori_, [])
293 | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
294 if sel = sel' andalso (inter op = ts ts') <> []
297 (id,vat,sel,d, inter op = ts ts'):ori,
299 else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
304 else seek_orits ctxt sel ts oris;
306 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
307 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
308 uncaught exception TYPE
309 > seek_orits thy sel ts [];
310 uncaught exception TYPE
313 (*find_first item with #1 equal to id*)
314 fun seek_ppc id [] = NONE
315 | seek_ppc id (p::(ppc:itm list)) =
316 if id = #1 p then SOME p else seek_ppc id ppc;
320 (*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
323 datatype appl = Appl of tac_ | Notappl of string;
325 fun ppc2list ({Given=gis,Where=whs,Find=fis,
326 With=wis,Relate=res}: 'a ppc) =
327 gis @ whs @ fis @ wis @ res;
328 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
334 (* get the number of variants in a problem in 'original',
335 assumes equal descriptions in immediate sequence *)
337 let fun eq(x,y) = head_of x = head_of y;
338 fun cnt eq [] y n = ([n],[])
339 | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
341 fun coll eq xs [] = xs
342 | coll eq xs (y::ys) =
343 let val (n,ys') = cnt eq (y::ys) y 0;
344 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
345 val vts = subtract op = [1] (distinct (coll eq [] ts));
346 in case vts of [] => 1 | [n] => n
347 | _ => error "different variants in formalization" end;
349 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
350 val it = ([3],[4,5,5,5,5,5]) : int list * int list
351 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
352 val it = [1,3,1,5] : int list
355 fun is_list_type (Type("List.list",_)) = true
356 | is_list_type _ = false;
357 (* fun destr (Type(str,sort)) = (str,sort);
358 > val (SOME ct) = parse thy "lll::real list";
359 > val ty = (#T o rep_cterm) ct;
363 val it = ("List.list",["RealDef.real"]) : string * typ list
364 > atomty ((#t o rep_cterm) ct);
366 *** Free ( lll, real list)
369 > val (SOME ct) = parse thy "[lll::real]";
370 > val ty = (#T o rep_cterm) ct;
374 val it = ("List.list",["'a"]) : string * typ list
375 > atomty ((#t o rep_cterm) ct);
377 *** Const ( List.list.Cons, [real, real list] => real list)
378 *** Free ( lll, real)
379 *** Const ( List.list.Nil, real list)
381 > val (SOME ct) = parse thy "lll";
382 > val ty = (#T o rep_cterm) ct;
384 val it = false : bool *)
387 fun has_list_type (Free(_,T)) = is_list_type T
388 | has_list_type _ = false;
390 > val (SOME ct) = parse thy "lll::real list";
391 > has_list_type (term_of ct);
393 > val (SOME ct) = parse thy "[lll::real]";
394 > has_list_type (term_of ct);
395 val it = false : bool *)
397 fun is_parsed (Syn _) = false
398 | is_parsed _ = true;
399 fun parse_ok its = foldl and_ (true, map is_parsed its);
401 fun all_dsc_in itm_s =
403 fun d_in (Cor ((d,_),_)) = [d]
406 | d_in (Inc ((d,_),_)) = [d]
407 | d_in (Sup (d,_)) = [d]
408 | d_in (Mis (d,_)) = [d];
409 in (flat o (map d_in)) itm_s end;
412 fun is_Syn (Syn _) = true
413 | is_Syn (Typ _) = true
416 fun is_error (Cor (_,ts)) = false
417 | is_error (Sup (_,ts)) = false
418 | is_error (Inc (_,ts)) = false
419 | is_error (Mis (_,ts)) = false
423 fun ct_in (Syn (c)) = c
424 | ct_in (Typ (c)) = c
425 | ct_in _ = error "ct_in called for Cor .. Sup";
428 (*#############################################################*)
429 (*#############################################################*)
430 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
433 (* testdaten besorgen:
434 use"test-coil-kernel.sml";
435 val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
440 variant V: oris union ppc => int, id ID: oris union ppc => int
443 EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
446 @vt = max sum(i : ppc) V i
452 > ((vts_cnt (vts_in itms))) itms;
457 > val vts = vts_in itms;
458 val vts = [1,2,3] : int list
459 > val nvts = vts_cnt vts itms;
460 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
461 > val mx = max2 nvts;
462 val mx = (3,7) : int * int
463 > val v = max_vt itms;
465 --------------------------
469 (*.get the first term in ts from ori.*)
470 (* val (_,_,fd,d,ts) = hd miss;
472 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
473 (fd, (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) o
474 comp_dts) (d,[hd ts]) : cterm');
475 (* val t = comp_dts (d,[hd ts]);
478 (* get a term from ori, notyet input in itm.
479 the term from ori is thrown back to a string in order to reuse
480 machinery for immediate input by the user. *)
481 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
482 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
483 (d, subtract op = (ts_in itm_) ts) : cterm');
484 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
485 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
486 (d, subtract op = (ts_in itm_) ts) : cterm');
488 (* in FE dsc, not dat: this is in itms ...*)
489 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
490 | is_untouched _ = false;
493 (* select an item in oris, notyet input in itms
494 (precondition: in itms are only Cor, Sup, Inc) *)
497 | x mem (y :: ys) = x = y orelse x mem ys;
499 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
501 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
502 fun is_elem itms (f,(d,t)) =
503 case find_first (test_d d) itms of
504 SOME _ => true | NONE => false;
505 in case filter_out (is_elem itms) pbt of
506 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
510 ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
511 comp_dts) (d, []) : cterm')
514 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
516 | nxt_add thy oris pbt itms =
518 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
519 andalso (#3 ori) <>"#undef";
520 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
521 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
522 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
523 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
524 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
525 | false_and_not_Sup (i,v,false,f, _) = true
526 | false_and_not_Sup _ = false;
528 val v = if itms = [] then 1 else max_vt itms;
529 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
530 val vits = if v = 0 then itms (*because of dsc without dat*)
531 else filter (testi_vt v) itms; (*itms..vat*)
532 val icl = filter false_and_not_Sup vits; (* incomplete *)
534 then case filter_out (test_id (map #1 vits)) vors of
536 (* val miss = filter_out (test_id (map #1 vits)) vors;
538 | miss => SOME (getr_ct thy (hd miss))
540 case find_first (test_subset (hd icl)) vors of
541 (* val SOME ori = find_first (test_subset (hd icl)) vors;
543 NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
544 | SOME ori => SOME (geti_ct thy ori (hd icl))
550 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
551 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
552 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
553 | mk_delete thy str _ =
554 error ("mk_delete: called with field '"^str^"'");
555 fun mk_additem "#Given" ct = Add_Given ct
556 | mk_additem "#Find" ct = Add_Find ct
557 | mk_additem "#Relate"ct = Add_Relation ct
559 error ("mk_additem: called with field '"^str^"'");
562 (* determine the next step of specification;
563 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
564 eg. in rootpbl 'no_met':
566 preok predicates are _all_ ok (and problem matches completely)
567 oris immediately from formalization
568 (dI',pI',mI') specification coming from author/parent-problem
569 (pbl, item lists specified by user
570 met) -"-, tacitly completed by copy_probl
571 (dI,pI,mI) specification explicitly done by the user
572 (pbt, mpc) problem type, guard of method
574 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
575 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
576 ((*tracing"### nxt_spec Pbl";*)
577 if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
578 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
579 else case find_first (is_error o #5) (pbl:itm list) of
580 SOME (_, _, _, fd, itm_) =>
582 (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
584 ((*tracing"### nxt_spec is_error NONE";*)
585 case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
587 SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
588 (Pbl, mk_additem fd ct'))
589 | NONE => (*pbl-items complete*)
590 if not preok then (Pbl, Refine_Problem pI')
592 if dI = e_domID then (Pbl, Specify_Theory dI')
593 else if pI = e_pblID then (Pbl, Specify_Problem pI')
594 else if mI = e_metID then (Pbl, Specify_Method mI')
596 case find_first (is_error o #5) met of
597 SOME (_,_,_,fd,itm_) =>
598 (Met, mk_delete (assoc_thy dI) fd itm_)
600 (case nxt_add (assoc_thy dI) oris mpc met of
601 SOME (fd,ct') => (*30.8.01: pre?!?*)
602 (Met, mk_additem fd ct')
604 ((*Solv 3.4.00*)Met, Apply_Method mI))))
606 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
607 ((*tracing"### nxt_spec Met"; *)
608 case find_first (is_error o #5) met of
609 SOME (_,_,_,fd,itm_) =>
610 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
612 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
613 SOME (fd,ct') => (Met, mk_additem fd ct')
615 ((*tracing"### nxt_spec Met: nxt_add NONE";*)
616 if dI = e_domID then (Met, Specify_Theory dI')
617 else if pI = e_pblID then (Met, Specify_Problem pI')
618 else if not preok then (Met, Specify_Method mI)
619 else (Met, Apply_Method mI)));
622 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
623 (2,[2],true,"#Find",Syn("empty"))];
626 fun is_field_correct sel d dscpbt =
627 case assoc (dscpbt, sel) of
629 | SOME ds => member op = ds d;
631 (*. update the itm_ already input, all..from ori .*)
632 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
634 fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
636 val ts' = union op = (ts_in itm_) ts;
637 val pval = pbl_ids' d ts'
638 (*WN.9.5.03: FIXXXME [#0, epsilon]
639 here would upd_penv be called for [#0, epsilon] etc. *)
640 val complete = if eq_set op = (ts', all) then true else false;
643 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
644 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
645 | (Syn c) => error ("ori_2itm wants to overwrite "^c)
646 | (Typ c) => error ("ori_2itm wants to overwrite "^c)
647 | (Inc _) => if complete
648 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
649 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
650 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
651 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
652 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
653 (* 28.1.00: not completely clear ---^^^ etc.*)
654 (* 4.9.01: Mis just copied---vvv *)
655 | (Mis _) => if complete
656 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
657 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
661 fun eq1 d (_,(d',_)) = (d = d');
662 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
665 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
666 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
667 pval: value for problem-environment _NOT_ checked for 'inter' --
668 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
669 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
670 (*. is_input ori itms <=>
671 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
672 (2) ori(ts) subset itm(ts) --- Err "already input"
673 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
674 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
675 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
677 fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
678 case find_first (eq1 d) pbt of
679 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
680 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
682 (case find_first (eq3 f d) itms of
683 SOME (_,_,_,_,itm_) =>
685 val ts' = inter op = (ts_in itm_) ts;
686 in if subset op = (ts, ts')
688 map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts') ^
689 " already input", e_itm) (*2*)
691 ori_2itm itm_ pid all (i,v,f,d,
692 subtract op = ts' ts)) (*3,4*)
694 | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[])))
695 pid all (i,v,f,d,ts)) (*1*)
697 | NONE => ("", ori_2itm (Sup (d,ts))
698 e_term all (i,v,f,d,ts));
700 fun test_types ctxt (d,ts) =
702 (*val s = !show_types; val _ = show_types:= true;*)
703 val opt = (try comp_dts) (d,ts);
704 val msg = case opt of
706 | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
708 ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
711 (*val _ = show_types:= s*)
716 fun maxl [] = error "maxl of []"
719 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
723 (*. is the input term t known in oris ?
724 give feedback on all(?) strange input;
725 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
726 (*WN.11.03: from lists*)
727 fun is_known ctxt sel ori t =
728 (* val (ori,t)=(oris,term_of ct);
731 val _ = tracing ("RM is_known: t=" ^ term2str t);
732 val ots = (distinct o flat o (map #5)) (ori:ori list);
733 val oids = ((map (fst o dest_Free)) o distinct o
734 flat o (map vars)) ots;
735 val (d,ts(*,pval*)) = split_dts t;
736 val ids = map (fst o dest_Free)
737 ((distinct o (flat o (map vars))) ts);
738 in if (subtract op = oids ids) <> []
739 then (("identifiers "^(strs2str' (subtract op = oids ids))^
740 " not in example"), e_ori_, [])
744 if not (subset op = (map typeless ts, map typeless ots))
747 (map (Print_Mode.setmp [] (Syntax.string_of_term
749 "' not in example (typeless)"), e_ori_, [])
750 else (case seek_orits ctxt sel ts ori of
751 ("", ori_ as (_,_,_,d,ts), all) =>
752 (case test_types ctxt (d,ts) of
753 "" => ("", ori_, all)
754 | msg => (msg, e_ori_, []))
755 | (msg,_,_) => (msg, e_ori_, []))
757 if member op = (map #4 ori) d
758 then seek_oridts ctxt sel (d,ts) ori
759 else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
760 " not in example", (0, [], sel, d, ts), [])
764 (*. for return-value of appl_add .*)
767 | Err of string; (*error-message*)
770 (** add an item to the model; check wrt. oris and pbt **)
771 (* in contrary to oris<>[] below, this part handles user-input
772 extremely acceptive, i.e. accept input instead error-msg *)
773 fun appl_add ctxt sel [] ppc pbt ct =
775 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
776 in case parseNEW ctxt ct of
777 NONE => Add (i, [], false, sel, Syn ct)
779 let val (d, ts) = split_dts t;
780 in if d = e_term then
781 Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
782 (case find_first (eq1 d) pbt of
783 NONE => Add (i, [], true, sel, Sup (d,ts))
784 | SOME (f, (_, id)) =>
785 let fun eq2 d (i, _, _, _, itm_) =
786 d = (d_in itm_) andalso i <> 0;
787 in case find_first (eq2 d) ppc of
788 NONE => Add (i, [], true, f,
789 Cor ((d, ts), (id, pbl_ids' d ts))
791 | SOME (i', _, _, _, itm_) => if is_list_dsc d then
793 val in_itm = ts_in itm_;
794 val ts' = union op = ts in_itm;
795 val i'' = if in_itm = [] then i else i';
796 in Add (i'', [], true, f,
797 Cor ((d, ts'), (id, pbl_ids' d ts'))
800 Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
804 | appl_add ctxt sel oris ppc pbt str =
805 case parse (ProofContext.theory_of ctxt) str of
806 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
807 | SOME t => case is_known ctxt sel oris (term_of t) of
808 ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
810 | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
811 | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
813 > val (msg,itm) = is_notyet_input thy ppc all ori';
814 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
816 > val ts = ts_in itm_;
820 (** make oris from args of the stac SubProblem and from pbt **)
822 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
823 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
824 fun is_copy_named_idstr str =
825 case (rev o Symbol.explode) str of
826 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
827 "is_copy_named_idstr: " ^ str ^ " T"); true)
828 | _ => (tracing ((strs2str o (rev o Symbol.explode))
829 "is_copy_named_idstr: " ^ str ^ " F"); false);
830 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
832 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
833 fun is_copy_named_generating_idstr str =
834 if is_copy_named_idstr str
835 then case (rev o Symbol.explode) str of
836 "'"::"'"::"'"::_ => false
839 fun is_copy_named_generating (_, (_, t)) =
840 (is_copy_named_generating_idstr o free2str) t;
842 (*.split type-wrapper from scr-arg and build part of an ori;
843 an type-error is reported immediately, raises an exn,
844 subsequent handling of exn provides 2nd part of error message.*)
845 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
846 (* val (thy, (str, (dsc, _)), (ty $ var)) =
849 (cterm_of thy (dsc $ var);(*type check*)
850 SOME ((([1], str, dsc, (*[var]*)
851 split_dts' (dsc, var))): preori)(*:ori without leading #*))
852 handle e as TYPE _ =>
853 (tracing (dashs 70 ^ "\n"
854 ^"*** ERROR while creating the items for the model of the ->problem\n"
855 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
856 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
857 ^"*** description: "^(term_detail2str dsc)
858 ^"*** value: "^(term_detail2str var)
859 ^"*** typeconstructor in script: "^(term_detail2str ty)
860 ^"*** checked by theory: "^(theory2str thy)^"\n"
862 (*OldGoals.print_exn e; raises exn again*)
863 writeln (PolyML.makestring e);
865 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
868 (*.match each pat of the model-pattern with an actual argument;
869 precondition: copy-named vars are filtered out.*)
870 fun matc thy ([]:pat list) _ (oris:preori list) = oris
871 | matc thy pbt [] _ =
873 error ("actual arg(s) missing for '"^pats2str pbt
874 ^"' i.e. should be 'copy-named' by '*_._'"))
875 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
876 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
877 (thy, pbt', ags, []);
879 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
880 (thy, pbt, ags, (oris @ [ori]));
882 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
883 else(*..del?*) let val opt = mtc thy p a;
885 (* val SOME ori = mtc thy p a;
887 SOME ori => matc thy pbt ags (oris @ [ori])
888 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
890 (* run subp-rooteq.sml until Init_Proof before ...
891 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
892 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
894 other vars as in mtc ..
895 > matc thy (drop_last pbt) ags [];
896 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
899 (* generate a new variable "x_i" name from a related given one "x"
900 by use of oris relating "v_i_" (is_copy_named!) to "v_"
901 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
903 (* generate a new variable "x_i" name from a related given one "x"
904 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
905 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
906 but leave is_copy_named_generating as is, e.t. ss''' *)
907 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
908 (if is_copy_named_generating p
909 then (*WN051014 kept strange old code ...*)
910 let fun sel (_,_,d,ts) = comp_ts (d, ts)
911 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
912 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
913 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
914 val vals = map sel oris
915 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
916 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
917 else ([1], field, dsc, [t])
919 handle _ => error ("cpy_nam: for "^(term2str t));
921 (*.match the actual arguments of a SubProblem with a model-pattern
922 and create an ori list (in root-pbl created from formalization).
923 expects ags:pats = 1:1, while copy-named are filtered out of pats;
924 if no 1:1 the exn raised by matc/mtc and handled at call.
925 copy-named pats are appended in order to get them into the model-items.*)
926 fun match_ags thy (pbt:pat list) ags =
927 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
928 val pbt' = filter_out is_copy_named pbt;
929 val cy = filter is_copy_named pbt;
930 val oris' = matc thy pbt' ags [];
931 val cy' = map (cpy_nam pbt' oris') cy;
932 val ors = add_id (oris' @ cy');
933 (*appended in order to get ^^^^^ into the model-items*)
934 in (map flattup ors):ori list end;
936 (*.report part of the error-msg which is not available in match_args.*)
937 fun match_ags_msg pI stac ags =
938 let (*val s = !show_types
939 val _ = show_types:= true*)
940 val pats = (#ppc o get_pbt) pI
941 val msg = (dots 70^"\n"
942 ^"*** problem "^strs2str pI^" has the ...\n"
943 ^"*** model-pattern "^pats2str pats^"\n"
944 ^"*** stac '"^term2str stac^"' has the ...\n"
945 ^"*** arg-list "^terms2str ags^"\n"
947 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
948 (*val _ = show_types:= s*)
952 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
953 fun vars_of_pbl_ pbl_ =
954 let fun var_of_pbl_ (gfr,(dsc,t)) = t
955 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
956 fun vars_of_pbl_' pbl_ =
957 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
958 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
960 fun overwrite_ppc thy itm ppc =
962 fun repl ppc' (_,_,_,_,itm_) [] =
963 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
965 | repl ppc' itm (p::ppc) =
966 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
967 else repl (ppc' @ [p]) itm ppc
968 in repl [] itm ppc end;
970 (*10.3.00: insert the already compiled itm into model;
971 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
974 fun insert_ppc thy itm ppc =
976 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
977 | eq_untouched _ _ = false;
980 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
981 case seek_ppc (#1 itm) ppc of
982 (* val SOME xxx = seek_ppc (#1 itm) ppc;
984 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
985 overwrite_ppc thy itm ppc
986 | NONE => (ppc @ [itm]));
987 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
989 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
990 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
992 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
993 (d_in itm_) = (d_in iitm_);
994 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
995 handles superfluous items carelessly*)
996 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
998 > gen_ins' eee (4,[1,3,5,7]);
999 val it = [1, 3, 5, 7, 4] : int list*)
1002 (*. output the headline to a ppc .*)
1003 fun header p_ pI mI =
1004 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1006 | pos => error ("header called with "^ pos_2str pos);
1009 fun specify_additem sel (ct,_) (p,Met) c pt =
1011 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1012 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1013 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1014 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1015 val cpI = if pI = e_pblID then pI' else pI;
1016 val cmI = if mI = e_metID then mI' else mI;
1017 val {ppc,pre,prls,...} = get_met cmI;
1018 in case appl_add (thy2ctxt thy) sel oris met ppc ct of
1019 Add itm (*..union old input *) =>
1020 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1022 val met' = insert_ppc thy itm met;
1023 (*val pt' = update_met pt p met';*)
1024 val ((p,Met),_,_,pt') =
1025 generate1 thy (case sel of
1026 "#Given" => Add_Given' (ct, met')
1027 | "#Find" => Add_Find' (ct, met')
1028 | "#Relate"=> Add_Relation'(ct, met'))
1029 (Uistate, e_ctxt) (p,Met) pt
1030 val pre' = check_preconds thy prls pre met'
1031 val pb = foldl and_ (true, map fst pre')
1032 (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
1034 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1035 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1036 in ((p,p_), ((p,p_),Uistate),
1037 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1038 (Method cmI, itms2itemppc thy met' pre'))),
1041 let val pre' = check_preconds thy prls pre met
1042 val pb = foldl and_ (true, map fst pre')
1043 (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
1045 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1046 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1047 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1051 | specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1053 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1054 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1055 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1056 val cpI = if pI = e_pblID then pI' else pI;
1057 val cmI = if mI = e_metID then mI' else mI;
1058 val {ppc,where_,prls,...} = get_pbt cpI;
1059 in case appl_add (thy2ctxt thy) sel oris pbl ppc ct of
1060 Add itm (*..union old input *) =>
1061 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1064 (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
1065 val pbl' = insert_ppc thy itm pbl
1066 val ((p,Pbl),_,_,pt') =
1067 generate1 thy (case sel of
1068 "#Given" => Add_Given' (ct, pbl')
1069 | "#Find" => Add_Find' (ct, pbl')
1070 | "#Relate"=> Add_Relation'(ct, pbl'))
1071 (Uistate, e_ctxt) (p,Pbl) pt
1072 val pre = check_preconds thy prls where_ pbl'
1073 val pb = foldl and_ (true, map fst pre)
1074 (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
1076 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1077 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1078 val ppc = if p_= Pbl then pbl' else met;
1079 in ((p,p_), ((p,p_),Uistate),
1080 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1082 itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1085 let val pre = check_preconds thy prls where_ pbl
1086 val pb = foldl and_ (true, map fst pre)
1087 (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
1089 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1090 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1091 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1093 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1094 val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1098 val (msg,itm) = appl_add thy sel oris ppc ct;
1099 val (Cor(d,ts)) = #5 itm;
1106 (* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1107 specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1109 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1110 let (* either """"""""""""""" all empty or complete *)
1111 val thy = assoc_thy dI';
1112 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1113 else pI' |> #ppc o get_pbt |> prep_ori fmz thy |> #1;
1114 val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
1115 (oris,(dI',pI',mI'),e_term);
1116 val {ppc,prls,where_,...} = get_pbt pI'
1117 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1118 val pt = update_pbl pt [] pbl;
1119 val pre = check_preconds thy prls where_ pbl
1120 val pb = foldl and_ (true, map fst pre)*)
1121 val (pbl, pre, pb) = ([], [], false)
1124 (([],Pbl), (([],Pbl),Uistate),
1125 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1126 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1127 Refine_Tacitly pI', Safe,pt)
1129 (([],Pbl), (([],Pbl),Uistate),
1130 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1131 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1135 (*ONLY for STARTING modeling phase*)
1136 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1137 let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
1139 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
1141 val thy' = if dI = e_domID then dI' else dI
1142 val thy = assoc_thy thy'
1143 val {ppc,prls,where_,...} = get_pbt pI'
1144 val pre = check_preconds thy prls where_ pbl
1145 val pb = foldl and_ (true, map fst pre)
1146 val ((p,_),_,_,pt) =
1147 generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
1148 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1149 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1150 in ((p,Pbl), ((p,p_),Uistate),
1151 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1152 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1155 (*. called only if no_met is specified .*)
1156 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1157 let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
1159 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
1161 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1162 (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
1163 (*val pt = update_pbl pt p pbl;
1164 val pt = update_orispec pt p
1165 (string_of_thy thy, pIre,
1166 if length met = 0 then e_metID else hd met);*)
1167 val (domID, metID) = (string_of_thy thy,
1168 if length met = 0 then e_metID else hd met)
1169 val ((p,_),_,_,pt) =
1170 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1171 (Uistate, e_ctxt) pos pt
1172 (*val pre = check_preconds thy prls where_ pbl
1173 val pb = foldl and_ (true, map fst pre)*)
1174 val (pbl, pre, pb) = ([], [], false)
1175 in ((p,Pbl), (pos,Uistate),
1176 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1177 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1178 Model_Problem, Safe, pt) end
1180 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1181 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
1182 (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1183 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1184 Model_Problem, Safe, pt) end
1186 (* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
1187 val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
1189 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1190 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1191 meth=met, ...}) = get_obj I pt p;
1192 (*val pt = update_pbl pt p itms;
1193 val pt = update_pblID pt p pI;*)
1194 val thy = assoc_thy dI
1195 val ((p,Pbl),_,_,pt)=
1196 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
1197 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1198 val mI'' = if mI=e_metID then mI' else mI;
1199 (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
1200 val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1201 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1202 in ((p,Pbl), (pos,Uistate),
1203 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1204 (Problem pI, itms2itemppc dI'' itms pre))),
1206 (* val Specify_Method' mID = nxt; val (p,_) = p;
1207 val Specify_Method' mID = m;
1208 specify (Specify_Method' mID) (p,p_) c pt;
1210 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1211 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1212 meth=met, ...}) = get_obj I pt p;
1213 val {ppc,pre,prls,...} = get_met mID
1214 val thy = assoc_thy dI
1215 val oris = add_field' thy ppc oris;
1216 (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1217 val dI'' = if dI=e_domID then dI' else dI;
1218 val pI'' = if pI = e_pblID then pI' else pI;
1219 val met = if met=[] then pbl else met;
1220 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1221 (*val pt = update_met pt p itms;
1222 val pt = update_metID pt p mID*)
1224 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1225 (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
1226 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1227 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1228 in (pos, (pos,Uistate),
1229 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1230 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1232 (* val Add_Find' ct = nxt; val sel = "#Find";
1234 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1235 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1236 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1237 (* val Specify_Theory' domID = m;
1238 val (Specify_Theory' domID, (p,p_)) = (m, pos);
1240 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1241 let val p_ = case p_ of Met => Met | _ => Pbl
1242 val thy = assoc_thy domID;
1243 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1244 probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
1245 val mppc = case p_ of Met => met | _ => pbl;
1246 val cpI = if pI = e_pblID then pI' else pI;
1247 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1248 val cmI = if mI = e_metID then mI' else mI;
1249 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1252 Met => (check_preconds thy mer mwh met)
1253 | _ => (check_preconds thy per pwh pbl)
1254 val pb = foldl and_ (true, map fst pre)
1257 (*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1258 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1259 (pbl,met) (ppc,mpc) (dI,pI,mI);
1260 in ((p,p_), (pos,Uistate),
1261 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1262 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1264 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1266 (*val pt = update_domID pt p domID;11.8.03*)
1267 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1268 (Uistate, e_ctxt) (p,p_) pt
1269 (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1270 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1271 (ppc,mpc) (domID,pI,mI);
1272 in ((p,p_), (pos,Uistate),
1273 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1274 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1277 (* itms2itemppc thy [](*mpc*) pre
1279 | specify m' _ _ _ =
1280 error ("specify: not impl. for "^tac_2str m');
1282 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1283 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1285 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1287 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1288 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1289 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1290 val cpI = if pI = e_pblID then pI' else pI;
1291 in case appl_add (thy2ctxt thy) sel oris pbl ((#ppc o get_pbt) cpI) ct of
1292 Add itm (*..union old input *) =>
1293 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1296 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1297 val pbl' = insert_ppc thy itm pbl
1300 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1301 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1302 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1303 val ((p,Pbl),c,_,pt') =
1304 generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
1305 in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate' end
1308 (*TODO.WN03 pass error-msgs to the frontend..
1309 FIXME ..and dont abuse a tactic for that purpose*)
1311 Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1312 (e_pos', (e_istate, e_ctxt)))], [], ptp)
1315 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1316 val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1318 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1320 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1321 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1322 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1323 val cmI = if mI = e_metID then mI' else mI;
1324 in case appl_add (thy2ctxt thy) sel oris met ((#ppc o get_met) cmI) ct of
1325 Add itm (*..union old input *) =>
1326 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1328 val met' = insert_ppc thy itm met;
1331 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1332 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1333 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1334 val ((p,Met),c,_,pt') =
1335 generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
1336 in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
1338 | Err msg => ([(*tacis*)], [], ptp)
1339 (*nxt_me collects tacis until not hide; here just no progress*)
1343 val (msg,itm) = appl_add thy sel oris ppc ct;
1344 val (Cor(d,ts)) = #5 itm;
1349 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1350 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1351 handle _ => error ("ori2Coritm: dsc "^
1353 "in ori, but not in pbt")
1355 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1356 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1357 (find_first (eq1 d))) pbt,ts))):itm)
1358 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1359 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1362 (*filter out oris which have same description in itms*)
1363 fun filter_outs oris [] = oris
1364 | filter_outs oris (i::itms) =
1365 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1366 (#4:ori -> term)) oris;
1367 in filter_outs ors itms end;
1369 fun memI a b = member op = a b;
1370 (*filter oris which are in pbt, too*)
1371 fun filter_pbt oris pbt =
1372 let val dscs = map (fst o snd) pbt
1373 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1375 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1376 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1378 fun x mem [] = false
1379 | x mem (y :: ys) = x = y orelse x mem ys;
1381 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1382 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1384 let val vat = max_vt pits;
1386 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1387 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1388 val os = filter_outs ors itms;
1389 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1390 in itms @ (map (ori2Coritm met) os) end
1395 (*.complete model and guard of a calc-head .*)
1397 fun x mem [] = false
1398 | x mem (y :: ys) = x = y orelse x mem ys;
1400 fun complete_mod_ (oris, mpc, ppc, probl) =
1401 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1402 val vat = if probl = [] then 1 else max_vt probl
1403 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1404 val pors = filter_outs pors pits (*which are in pbl already*)
1405 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1407 val pits = pits @ (map (ori2Coritm ppc) pors)
1408 val mits = complete_metitms oris pits [] mpc
1412 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1413 (if dI = e_domID then odI else dI,
1414 if pI = e_pblID then opI else pI,
1415 if mI = e_metID then omI else mI):spec;
1418 (*.find a next applicable tac (for calcstate) and update ptree
1419 (for ev. finding several more tacs due to hide).*)
1420 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1421 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1422 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1423 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1425 val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1426 val (dI, pI, mI) = some_spec ospec spec
1427 val thy = assoc_thy dI
1428 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1429 val {cas, ppc, ...} = get_pbt pI
1430 val pbl = init_pbl ppc (* fill in descriptions *)
1431 (*----------------if you think, this should be done by the Dialog
1432 in the java front-end, search there for WN060225-modelProblem----*)
1433 val (pbl, met) = case cas of NONE => (pbl, [])
1434 | _ => complete_mod_ (oris, mpc, ppc, probl)
1435 (*----------------------------------------------------------------*)
1436 val tac_ = Model_Problem' (pI, pbl, met)
1437 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
1438 in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1440 (* val Add_Find ct = tac;
1442 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1443 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1444 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1446 (*. called only if no_met is specified .*)
1447 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1448 let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1449 val opt = refine_ori oris pI
1452 let val {met,ppc,...} = get_pbt pI'
1453 val pbl = init_pbl ppc
1454 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1455 val mI = if length met = 0 then e_metID else hd met
1456 val thy = assoc_thy dI
1458 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1459 (Uistate, e_ctxt) pos pt
1460 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1461 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1462 | NONE => ([], [], ptp)
1465 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1466 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1467 probl, ...}) = get_obj I pt p
1468 val thy = if dI' = e_domID then dI else dI'
1469 in case refine_pbl (assoc_thy thy) pI probl of
1470 NONE => ([], [], ptp)
1471 | SOME (rfd as (pI',_)) =>
1472 let val (pos,c,_,pt) =
1473 generate1 (assoc_thy thy)
1474 (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1475 in ([(Refine_Problem pI, Refine_Problem' rfd,
1476 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1479 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1480 let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1481 probl, ...}) = get_obj I pt p;
1482 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1483 val {ppc,where_,prls,...} = get_pbt pI
1484 val pbl as (_,(itms,_)) =
1485 if pI'=e_pblID andalso pI=e_pblID
1486 then (false, (init_pbl ppc, []))
1487 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1488 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1489 val ((p,Pbl),c,_,pt)=
1490 generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
1491 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1492 (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1494 (*transfers oris (not required in pbl) to met-model for script-env
1495 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1496 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1497 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1498 meth=met, ...}) = get_obj I pt p;
1499 val {ppc,pre,prls,...} = get_met mID
1500 val thy = assoc_thy dI
1501 val oris = add_field' thy ppc oris;
1502 val dI'' = if dI=e_domID then dI' else dI;
1503 val pI'' = if pI = e_pblID then pI' else pI;
1504 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1505 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1507 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1508 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1509 (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1511 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1512 let val (dI',_,_) = get_obj g_spec pt p
1514 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1515 (Uistate, e_ctxt) pos pt
1516 in (*FIXXXME: check if pbl can still be parsed*)
1517 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1520 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1521 let val (dI',_,_) = get_obj g_spec pt p
1523 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1524 (Uistate, e_ctxt) pos pt
1525 in (*FIXXXME: check if met can still be parsed*)
1526 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1530 error ("nxt_specif: not impl. for "^tac2str m');
1532 (*.get the values from oris; handle the term list w.r.t. penv.*)
1535 fun x mem [] = false
1536 | x mem (y :: ys) = x = y orelse x mem ys;
1538 fun vals_of_oris oris =
1539 ((map (mkval' o (#5:ori -> term list))) o
1540 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1545 (* create a calc-tree with oris via an cas.refined pbl *)
1546 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1547 if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1548 let val {cas, met, ppc, thy, ...} = get_pbt pI
1549 val dI = if dI = "" then theory2theory' thy else dI
1550 val thy = assoc_thy dI
1551 val mI = if mI = [] then hd met else mI
1552 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1553 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1554 ([], (dI,pI,mI), hdl)
1555 val pt = update_spec pt [] (dI,pI,mI)
1556 val pits = init_pbl' ppc
1557 val pt = update_pbl pt [] pits
1558 in ((pt, ([] ,Pbl)), []) : calcstate end
1559 else if mI <> [] then (* from met-browser *)
1560 let val {ppc,...} = get_met mI
1561 val dI = if dI = "" then "Isac" else dI
1562 val thy = assoc_thy dI;
1563 val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1564 ([], (dI,pI,mI), e_term(*FIXME met*));
1565 val pt = update_spec pt [] (dI,pI,mI);
1566 val mits = init_pbl' ppc;
1567 val pt = update_met pt [] mits;
1568 in ((pt, ([], Met)), []) : calcstate end
1569 else (* new example, pepare for interactive modeling *)
1570 let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1571 ([], e_spec, e_term)
1572 in ((pt,([],Pbl)), []) : calcstate end
1573 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1574 let (* both """"""""""""""""""""""""" either empty or complete *)
1575 val thy = assoc_thy dI
1576 val (pI, pors, mI) =
1578 then let val pors = get_pbt pI |> #ppc |> prep_ori fmz thy |> #1;
1579 val pI' = refine_ori' pors pI;
1580 in (pI', pors(*refinement over models with diff.precond only*),
1581 (hd o #met o get_pbt) pI') end
1582 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
1583 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1584 val dI = theory2theory' (maxthy thy thy');
1585 val hdl = case cas of
1586 NONE => pblterm dI pI
1587 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1588 ~~~ vals_of_oris pors) t;
1589 val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
1590 (pors, (dI, pI, mI), hdl)
1591 in ((pt, ([], Pbl)),
1592 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1598 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1599 (* case appl_spec p pt m of /// 19.1.00
1600 Notappl e => Error' (Error_ e)
1602 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1606 (*fun tag_form thy (formal, given) = cterm_of thy
1607 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1608 fun tag_form thy (formal, given) =
1609 (let val gf = (head_of given) $ formal;
1610 val _ = cterm_of thy gf
1613 error ("calchead.tag_form: " ^
1614 Print_Mode.setmp [] (Syntax.string_of_term
1615 (thy2ctxt thy)) given ^ " .. " ^
1616 Print_Mode.setmp [] (Syntax.string_of_term
1617 (thy2ctxt thy)) formal ^
1618 " ..types do not match");
1619 (* val formal = (the o (parse thy)) "[R::real]";
1620 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1621 > tag_form thy (formal, given);
1622 val it = "fixed_values [R]" : cterm
1625 fun chktyp thy (n, fs, gs) =
1626 ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1628 (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1630 tag_form thy (nth n fs, nth n gs));
1631 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1633 (* #####################################################
1634 find the failing item:
1636 > val tag__form = chktyp (n,formals,givens);
1637 > (type_of o term_of o (nth n)) formals;
1638 > (type_of o term_of o (nth n)) givens;
1639 > atomty ((term_of o (nth n)) formals);
1640 > atomty ((term_of o (nth n)) givens);
1641 > atomty (term_of tag__form);
1642 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1643 ##################################################### *)
1645 (* #####################################################
1647 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1648 val formals = map (the o (parse thy)) origin;
1650 val given = ["equation (lhs=rhs)",
1651 "bound_variable bdv", (* TODO type *)
1653 val where_ = ["e is_root_equation_in bdv",
1655 "apx is_const_expr"];
1656 val find = ["L::rat set"];
1657 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1658 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1659 val givens = map (the o (parse thy)) given;
1661 val tag__forms = chktyps (formals, givens);
1662 map ((atomty) o term_of) tag__forms;
1663 ##################################################### *)
1666 (* check pbltypes, announces one failure a time *)
1667 (*fun chk_vars ctppc =
1668 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1669 appc flat (mappc (vars o term_of) ctppc)
1670 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1671 else if (re\\(gi union fi)) <> []
1672 then ("re\\(gi union fi)",re\\(gi union fi))
1673 else ("ok",[]) end;*)
1674 fun chk_vars ctppc =
1675 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1676 appc flat (mappc vars ctppc)
1677 val chked = subtract op = gi wh
1678 in if chked <> [] then ("wh\\gi", chked)
1679 else let val chked = subtract op = (union op = gi fi) re
1681 then ("re\\(gi union fi)", chked)
1686 (* check a new pbltype: variables (Free) unbound by given, find*)
1687 fun unbound_ppc ctppc =
1688 let val {Given=gi,Find=fi,Relate=re,...} =
1689 appc flat (mappc vars ctppc)
1690 in distinct (*re\\(gi union fi)*)
1691 (subtract op = (union op = gi fi) re) end;
1693 > val org = {Given=["[R=(R::real)]"],Where=[],
1694 Find=["[A::real]"],With=[],
1695 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1697 > val ctppc = mappc (the o (parse thy)) org;
1698 > unbound_ppc ctppc;
1699 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1703 (* f, a binary operator, is nested rightassociative *)
1706 fun fld f (x::[]) = x
1707 | fld f (x::x'::[]) = f (x',x)
1708 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1709 in ((fld f) o rev) xs end;
1711 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1712 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1713 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1714 > cterm_of thy conj;
1715 val it = "(a = b & c = d) & e = f" : cterm
1718 (* f, a binary operator, is nested leftassociative *)
1719 fun foldl1 f (x::[]) = x
1720 | foldl1 f (x::x'::[]) = f (x,x')
1721 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1723 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1724 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1725 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1726 > cterm_of thy conj;
1727 val it = "a = b & c = d & e = f & g = h" : cterm
1731 (* called only once, if a Subproblem has been located in the script*)
1732 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
1733 (* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
1737 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1738 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1739 (*all stored in tac_ itms ^^^^^^^^^^*)
1740 | nxt_model_pbl tac_ _ =
1741 error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1742 (* run subp_rooteq.sml ''
1743 until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
1744 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1745 (last_elem o drop_last) ets'';
1746 > val mst = (last_elem o drop_last) ets'';
1747 > nxt_model_pbl mst;
1748 val it = Refine_Tacitly ["univariate","equation"] : tac
1751 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1752 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1753 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1756 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1757 + met from fmz; assumes pos on PblObj, meth = [].*)
1758 fun complete_mod (pt, pos as (p, p_):pos') =
1759 (* val (pt, (p, _)) = (pt, p);
1760 val (pt, (p, _)) = (pt, pos);
1762 let val _= if p_ <> Pbl
1763 then tracing("###complete_mod: only impl.for Pbl, called with "^
1764 pos'2str pos) else ()
1765 val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
1767 val (dI,pI,mI) = some_spec ospec spec
1768 val mpc = (#ppc o get_met) mI
1769 val ppc = (#ppc o get_pbt) pI
1770 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1771 val pt = update_pblppc pt p pits
1772 val pt = update_metppc pt p mits
1773 in (pt, (p,Met):pos') end
1775 (*| complete_mod (pt, pos as (p, Met):pos') =
1776 error ("###complete_mod: only impl.for Pbl, called with "^
1779 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1780 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1781 fun all_modspec (pt, (p,_):pos') =
1782 (* val (pt, (p,_)) = ptp;
1784 let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1785 ...}) = get_obj I pt p;
1786 val thy = assoc_thy dI;
1787 val {ppc,...} = get_met mI;
1788 val mors = prep_ori fmz_ thy ppc |> #1;
1789 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1790 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1791 val pt = update_spec pt p (dI,pI,mI);
1792 in (pt, (p,Met): pos') end;
1794 (*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1795 fun is_complete_mod_ ([]: itm list) = false
1796 | is_complete_mod_ itms =
1797 foldl and_ (true, (map #3 itms));
1798 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1799 if (is_pblobj o (get_obj I pt)) p
1800 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1801 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1802 | is_complete_mod (pt, pos as (p, Met)) =
1803 if (is_pblobj o (get_obj I pt)) p
1804 then (is_complete_mod_ o (get_obj g_met pt)) p
1805 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1806 | is_complete_mod (_, pos) =
1807 error ("is_complete_mod called by "^pos'2str pos^
1808 " (should be Pbl or Met)");
1810 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1811 fun is_complete_spec (pt, pos as (p,_): pos') =
1812 if (not o is_pblobj o (get_obj I pt)) p
1813 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1814 else let val (dI,pI,mI) = get_obj g_spec pt p
1815 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1816 (*.complete empty items in specification from origin (pbl, met ev.refined);
1817 assumes 'is_complete_mod'.*)
1818 fun complete_spec (pt, pos as (p,_): pos') =
1819 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1820 val pt = update_spec pt p (some_spec ospec spec)
1823 fun is_complete_modspec ptp =
1824 is_complete_mod ptp andalso is_complete_spec ptp;
1829 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1830 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1832 let val (_,_,metID) = get_somespec' spec spec'
1834 if metID = e_metID then []
1835 else let val {prls,pre=where_,...} = get_met metID
1836 val pre = check_preconds' prls where_ meth 0
1838 val allcorrect = is_complete_mod_ meth
1839 andalso foldl and_ (true, (map #1 pre))
1840 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1841 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1842 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1844 let val (_,pI,_) = get_somespec' spec spec'
1846 if pI = e_pblID then []
1847 else let val {prls,where_,cas,...} = get_pbt pI
1848 val pre = check_preconds' prls where_ probl 0
1850 val allcorrect = is_complete_mod_ probl
1851 andalso foldl and_ (true, (map #1 pre))
1852 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1855 fun pt_form (PrfObj {form,...}) = Form form
1856 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1857 let val (dI, pI, _) = get_somespec' spec spec'
1858 val {cas,...} = get_pbt pI
1860 NONE => Form (pblterm dI pI)
1861 | SOME t => Form (subst_atomic (mk_env probl) t)
1863 (*vvv takes the tac _generating_ the formula=result, asm ok....
1864 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1866 if null asm then NONE else SOME asm,
1868 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1869 let val (_,_,metID) = some_spec ospec spec
1871 if null asm then NONE else SOME asm,
1872 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1873 -------------------------------------------------------------------------*)
1876 (*.pt_extract returns
1877 # the formula at pos
1878 # the tactic applied to this formula
1879 # the list of assumptions generated at this formula
1880 (by application of another tac to the preceding formula !)
1881 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1882 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1883 fun pt_extract (pt,([],Res)) =
1884 (* val (pt,([],Res)) = ptp;
1886 let val (f, asm) = get_obj g_result pt []
1887 in (Form f, NONE, asm) end
1890 | pt_extract (pt,(p,Res)) =
1891 (* val (pt,(p,Res)) = ptp;
1893 let val (f, asm) = get_obj g_result pt p
1894 val tac = if last_onlev pt p
1895 then if is_pblobj' pt (lev_up p)
1896 then let val (PblObj{spec=(_,pI,_),...}) =
1897 get_obj I pt (lev_up p)
1898 in if pI = e_pblID then NONE
1899 else SOME (Check_Postcond pI) end
1900 else SOME End_Trans (*WN0502 TODO for other branches*)
1901 else let val p' = lev_on p
1902 in if is_pblobj' pt p'
1903 then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1905 in SOME (Subproblem (dI, pI)) end
1906 else if f = get_obj g_form pt p'
1907 then SOME (get_obj g_tac pt p')
1908 (*because this Frm ~~~is not on worksheet*)
1909 else SOME (Take (term2str (get_obj g_form pt p')))
1911 in (Form f, tac, asm) end
1913 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1914 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1915 val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
1917 let val ppobj = get_obj I pt p
1918 val f = if is_pblobj ppobj then pt_model ppobj p_
1919 else get_obj pt_form pt p
1920 val tac = g_tac ppobj
1921 in (f, SOME tac, []) end;
1924 (**. get the formula from a ctree-node:
1925 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1926 take res from all other PrfObj's .**)
1927 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1928 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1929 [("headline", (p, Frm), h),
1930 ("stepform", (p, Res), r)]
1931 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1932 [("stepform", (p, Frm), form),
1933 ("stepform", (p, Res), r)];
1935 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1936 [("stepform", (p, Res), r)]
1938 (*assumes to take whole level, in particular hd -- for use in interSteps*)
1939 fun get_formress fs p [] = flat fs
1940 | get_formress fs p (nd::nds) =
1941 (* start with 'form+res' and continue with trying 'res' only*)
1942 get_forms (fs @ [formres p nd]) (lev_on p) nds
1943 and get_forms fs p [] = flat fs
1944 | get_forms fs p (nd::nds) =
1946 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1947 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1948 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1949 (* continue with trying 'res' only*)
1950 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1952 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1953 (*WN050219 made robust against _'to' below or after Complete nodes
1954 by handling exn caused by move_dn*)
1955 (*WN0401 this functionality belongs to ctree.sml,
1956 but fetching a calc_head requires calculations defined in modspec.sml
1957 transfer to ME/me.sml !!!
1958 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1959 is returned !!!!!!!!!!!!!
1961 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1962 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1963 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1967 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1971 | eq_pos' _ _ = false;
1973 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
1974 total ordering Position#compareTo(Position p) in the java-code
1975 val get_interval = fn
1976 : pos' -> : from is "move_up 1st-element" to return
1977 pos' -> : to the last element to be returned; from < to
1978 int -> : level: 0 gets the flattest sub-tree possible
1979 >999 gets the deepest sub-tree possible
1981 (pos' * : of the formula
1982 Term.term) : the formula
1985 fun get_interval from to level pt =
1986 (* val (from,level) = (f,lev);
1987 val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
1989 let fun get_inter c (from:pos') (to:pos') lev pt =
1990 (* val (c, from, to, lev) = ([], from, to, level);
1991 ------for recursion.......
1992 val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
1994 if eq_pos' from to orelse from = ([],Res)
1995 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
1996 if 'to' has values NOT generated by move_dn, see systest/me.sml
1997 TODO.WN0501: introduce an order on pos' and check "from > to"..
1998 ...there is an order in Java!
1999 WN051224 the hack got worse with returning term instead ptform*)
2000 then let val (f,_,_) = pt_extract (pt, from)
2002 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2003 | Form t => c @ [(from, t)]
2006 if lev < lev_of from
2007 then (get_inter c (move_dn [] pt from) to lev pt)
2008 handle (PTREE _(*from move_dn too far*)) => c
2009 else let val (f,_,_) = pt_extract (pt, from)
2010 val term = case f of
2011 ModSpec (_,_,headline,_,_,_)=> headline
2013 in (get_inter (c @ [(from, term)])
2014 (move_dn [] pt from) to lev pt)
2015 handle (PTREE _(*from move_dn too far*))
2016 => c @ [(from, term)] end
2017 in get_inter [] from to level pt end;
2020 fun posform2str (pos:pos', form) =
2021 "("^ pos'2str pos ^", "^
2023 Form f => term2str f
2024 | ModSpec c => term2str (#3 c(*the headline*)))
2026 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2027 (map posform2str)) pfs;
2028 fun posterm2str (pos:pos', t) =
2029 "("^ pos'2str pos ^", "^term2str t^")";
2030 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2031 (map posterm2str)) pfs;
2034 (*WN050225 omits the last step, if pt is incomplete*)
2036 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
2038 (*.get a calchead from a PblObj-node in the ctree;
2039 preconditions must be calculated.*)
2040 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
2041 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
2043 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2044 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
2045 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
2046 | get_ocalhd (pt, pos' as (p,Met):pos') =
2047 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2050 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2051 val pre = check_preconds (assoc_thy"Isac") prls pre meth
2052 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
2054 (*.at the activeFormula set the Model, the Guard and the Specification
2055 to empty and return a CalcHead;
2056 the 'origin' remains (for reconstructing all that).*)
2057 fun reset_calchead (pt, pos' as (p,_):pos') =
2058 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
2059 val pt = update_pbl pt p []
2060 val pt = update_met pt p []
2061 val pt = update_spec pt p e_spec
2062 in (pt, (p,Pbl):pos') end;