intermed. context integration
- prep_ori works with parseNEW
- unused thy function parameters removed
- thy parameter replaced by ctxt where useful
- appl_add adjusted and cleaned up - still uses parse due to error
- seek_oridts cleaned up
- split_dts cleaned up
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 ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
280 "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
282 | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
283 if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
286 (id,vat,sel,d, inter op = ts ts'):ori,
288 else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)))
289 ^ " not for " ^ sel, e_ori_, [])
290 else seek_oridts ctxt sel (d,ts) oris;
292 (*.to an input (_,ts) find the according ori and insert the ts.*)
293 fun seek_orits ctxt sel ts [] =
294 ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
296 "') not found in oris (typed)", e_ori_, [])
297 | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
298 if sel = sel' andalso (inter op = ts ts') <> []
301 (id,vat,sel,d, inter op = ts ts'):ori,
303 else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
308 else seek_orits ctxt sel ts oris;
310 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
311 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
312 uncaught exception TYPE
313 > seek_orits thy sel ts [];
314 uncaught exception TYPE
317 (*find_first item with #1 equal to id*)
318 fun seek_ppc id [] = NONE
319 | seek_ppc id (p::(ppc:itm list)) =
320 if id = #1 p then SOME p else seek_ppc id ppc;
324 (*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
327 datatype appl = Appl of tac_ | Notappl of string;
329 fun ppc2list ({Given=gis,Where=whs,Find=fis,
330 With=wis,Relate=res}: 'a ppc) =
331 gis @ whs @ fis @ wis @ res;
332 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
338 (* get the number of variants in a problem in 'original',
339 assumes equal descriptions in immediate sequence *)
341 let fun eq(x,y) = head_of x = head_of y;
342 fun cnt eq [] y n = ([n],[])
343 | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
345 fun coll eq xs [] = xs
346 | coll eq xs (y::ys) =
347 let val (n,ys') = cnt eq (y::ys) y 0;
348 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
349 val vts = subtract op = [1] (distinct (coll eq [] ts));
350 in case vts of [] => 1 | [n] => n
351 | _ => error "different variants in formalization" end;
353 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
354 val it = ([3],[4,5,5,5,5,5]) : int list * int list
355 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
356 val it = [1,3,1,5] : int list
359 fun is_list_type (Type("List.list",_)) = true
360 | is_list_type _ = false;
361 (* fun destr (Type(str,sort)) = (str,sort);
362 > val (SOME ct) = parse thy "lll::real list";
363 > val ty = (#T o rep_cterm) ct;
367 val it = ("List.list",["RealDef.real"]) : string * typ list
368 > atomty ((#t o rep_cterm) ct);
370 *** Free ( lll, real list)
373 > val (SOME ct) = parse thy "[lll::real]";
374 > val ty = (#T o rep_cterm) ct;
378 val it = ("List.list",["'a"]) : string * typ list
379 > atomty ((#t o rep_cterm) ct);
381 *** Const ( List.list.Cons, [real, real list] => real list)
382 *** Free ( lll, real)
383 *** Const ( List.list.Nil, real list)
385 > val (SOME ct) = parse thy "lll";
386 > val ty = (#T o rep_cterm) ct;
388 val it = false : bool *)
391 fun has_list_type (Free(_,T)) = is_list_type T
392 | has_list_type _ = false;
394 > val (SOME ct) = parse thy "lll::real list";
395 > has_list_type (term_of ct);
397 > val (SOME ct) = parse thy "[lll::real]";
398 > has_list_type (term_of ct);
399 val it = false : bool *)
401 fun is_parsed (Syn _) = false
402 | is_parsed _ = true;
403 fun parse_ok its = foldl and_ (true, map is_parsed its);
405 fun all_dsc_in itm_s =
407 fun d_in (Cor ((d,_),_)) = [d]
410 | d_in (Inc ((d,_),_)) = [d]
411 | d_in (Sup (d,_)) = [d]
412 | d_in (Mis (d,_)) = [d];
413 in (flat o (map d_in)) itm_s end;
416 fun is_Syn (Syn _) = true
417 | is_Syn (Typ _) = true
420 fun is_error (Cor (_,ts)) = false
421 | is_error (Sup (_,ts)) = false
422 | is_error (Inc (_,ts)) = false
423 | is_error (Mis (_,ts)) = false
427 fun ct_in (Syn (c)) = c
428 | ct_in (Typ (c)) = c
429 | ct_in _ = error "ct_in called for Cor .. Sup";
432 (*#############################################################*)
433 (*#############################################################*)
434 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
437 (* testdaten besorgen:
438 use"test-coil-kernel.sml";
439 val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
444 variant V: oris union ppc => int, id ID: oris union ppc => int
447 EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
450 @vt = max sum(i : ppc) V i
456 > ((vts_cnt (vts_in itms))) itms;
461 > val vts = vts_in itms;
462 val vts = [1,2,3] : int list
463 > val nvts = vts_cnt vts itms;
464 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
465 > val mx = max2 nvts;
466 val mx = (3,7) : int * int
467 > val v = max_vt itms;
469 --------------------------
473 (*.get the first term in ts from ori.*)
474 (* val (_,_,fd,d,ts) = hd miss;
476 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
477 (fd, (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) o
478 comp_dts) (d,[hd ts]) : cterm');
479 (* val t = comp_dts (d,[hd ts]);
482 (* get a term from ori, notyet input in itm.
483 the term from ori is thrown back to a string in order to reuse
484 machinery for immediate input by the user. *)
485 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
486 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
487 (d, subtract op = (ts_in itm_) ts) : cterm');
488 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
489 (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
490 (d, subtract op = (ts_in itm_) ts) : cterm');
492 (* in FE dsc, not dat: this is in itms ...*)
493 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
494 | is_untouched _ = false;
497 (* select an item in oris, notyet input in itms
498 (precondition: in itms are only Cor, Sup, Inc) *)
501 | x mem (y :: ys) = x = y orelse x mem ys;
503 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
505 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
506 fun is_elem itms (f,(d,t)) =
507 case find_first (test_d d) itms of
508 SOME _ => true | NONE => false;
509 in case filter_out (is_elem itms) pbt of
510 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
514 ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
515 comp_dts) (d, []) : cterm')
518 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
520 | nxt_add thy oris pbt itms =
522 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
523 andalso (#3 ori) <>"#undef";
524 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
525 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
526 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
527 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
528 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
529 | false_and_not_Sup (i,v,false,f, _) = true
530 | false_and_not_Sup _ = false;
532 val v = if itms = [] then 1 else max_vt itms;
533 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
534 val vits = if v = 0 then itms (*because of dsc without dat*)
535 else filter (testi_vt v) itms; (*itms..vat*)
536 val icl = filter false_and_not_Sup vits; (* incomplete *)
538 then case filter_out (test_id (map #1 vits)) vors of
540 (* val miss = filter_out (test_id (map #1 vits)) vors;
542 | miss => SOME (getr_ct thy (hd miss))
544 case find_first (test_subset (hd icl)) vors of
545 (* val SOME ori = find_first (test_subset (hd icl)) vors;
547 NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
548 | SOME ori => SOME (geti_ct thy ori (hd icl))
554 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
555 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
556 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
557 | mk_delete thy str _ =
558 error ("mk_delete: called with field '"^str^"'");
559 fun mk_additem "#Given" ct = Add_Given ct
560 | mk_additem "#Find" ct = Add_Find ct
561 | mk_additem "#Relate"ct = Add_Relation ct
563 error ("mk_additem: called with field '"^str^"'");
566 (* determine the next step of specification;
567 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
568 eg. in rootpbl 'no_met':
570 preok predicates are _all_ ok (and problem matches completely)
571 oris immediately from formalization
572 (dI',pI',mI') specification coming from author/parent-problem
573 (pbl, item lists specified by user
574 met) -"-, tacitly completed by copy_probl
575 (dI,pI,mI) specification explicitly done by the user
576 (pbt, mpc) problem type, guard of method
578 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
579 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
580 ((*tracing"### nxt_spec Pbl";*)
581 if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
582 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
583 else case find_first (is_error o #5) (pbl:itm list) of
584 SOME (_, _, _, fd, itm_) =>
586 (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
588 ((*tracing"### nxt_spec is_error NONE";*)
589 case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
591 SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
592 (Pbl, mk_additem fd ct'))
593 | NONE => (*pbl-items complete*)
594 if not preok then (Pbl, Refine_Problem pI')
596 if dI = e_domID then (Pbl, Specify_Theory dI')
597 else if pI = e_pblID then (Pbl, Specify_Problem pI')
598 else if mI = e_metID then (Pbl, Specify_Method mI')
600 case find_first (is_error o #5) met of
601 SOME (_,_,_,fd,itm_) =>
602 (Met, mk_delete (assoc_thy dI) fd itm_)
604 (case nxt_add (assoc_thy dI) oris mpc met of
605 SOME (fd,ct') => (*30.8.01: pre?!?*)
606 (Met, mk_additem fd ct')
608 ((*Solv 3.4.00*)Met, Apply_Method mI))))
610 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
611 ((*tracing"### nxt_spec Met"; *)
612 case find_first (is_error o #5) met of
613 SOME (_,_,_,fd,itm_) =>
614 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
616 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
617 SOME (fd,ct') => (Met, mk_additem fd ct')
619 ((*tracing"### nxt_spec Met: nxt_add NONE";*)
620 if dI = e_domID then (Met, Specify_Theory dI')
621 else if pI = e_pblID then (Met, Specify_Problem pI')
622 else if not preok then (Met, Specify_Method mI)
623 else (Met, Apply_Method mI)));
626 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
627 (2,[2],true,"#Find",Syn("empty"))];
630 fun is_field_correct sel d dscpbt =
631 case assoc (dscpbt, sel) of
633 | SOME ds => member op = ds d;
635 (*. update the itm_ already input, all..from ori .*)
636 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
638 fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
640 val ts' = union op = (ts_in itm_) ts;
641 val pval = pbl_ids' d ts'
642 (*WN.9.5.03: FIXXXME [#0, epsilon]
643 here would upd_penv be called for [#0, epsilon] etc. *)
644 val complete = if eq_set op = (ts', all) then true else false;
647 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
648 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
649 | (Syn c) => error ("ori_2itm wants to overwrite "^c)
650 | (Typ c) => error ("ori_2itm wants to overwrite "^c)
651 | (Inc _) => if complete
652 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
653 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
654 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
655 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
656 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
657 (* 28.1.00: not completely clear ---^^^ etc.*)
658 (* 4.9.01: Mis just copied---vvv *)
659 | (Mis _) => if complete
660 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
661 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
665 fun eq1 d (_,(d',_)) = (d = d');
666 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
669 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
670 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
671 pval: value for problem-environment _NOT_ checked for 'inter' --
672 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
673 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
674 (*. is_input ori itms <=>
675 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
676 (2) ori(ts) subset itm(ts) --- Err "already input"
677 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
678 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
679 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
681 fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
682 case find_first (eq1 d) pbt of
683 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
684 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
686 (case find_first (eq3 f d) itms of
687 SOME (_,_,_,_,itm_) =>
689 val ts' = inter op = (ts_in itm_) ts;
690 in if subset op = (ts, ts')
692 map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts') ^
693 " already input", e_itm) (*2*)
695 ori_2itm itm_ pid all (i,v,f,d,
696 subtract op = ts' ts)) (*3,4*)
698 | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[])))
699 pid all (i,v,f,d,ts)) (*1*)
701 | NONE => ("", ori_2itm (Sup (d,ts))
702 e_term all (i,v,f,d,ts));
704 fun test_types ctxt (d,ts) =
706 (*val s = !show_types; val _ = show_types:= true;*)
707 val opt = (try comp_dts) (d,ts);
708 val msg = case opt of
710 | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
712 ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
715 (*val _ = show_types:= s*)
720 fun maxl [] = error "maxl of []"
723 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
727 (*. is the input term t known in oris ?
728 give feedback on all(?) strange input;
729 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
730 (*WN.11.03: from lists*)
731 fun is_known ctxt sel ori t =
732 (* val (ori,t)=(oris,term_of ct);
735 val _ = tracing ("RM is_known: t=" ^ term2str t);
736 val ots = (distinct o flat o (map #5)) (ori:ori list);
737 val oids = ((map (fst o dest_Free)) o distinct o
738 flat o (map vars)) ots;
739 val (d,ts(*,pval*)) = split_dts t;
740 val ids = map (fst o dest_Free)
741 ((distinct o (flat o (map vars))) ts);
742 in if (subtract op = oids ids) <> []
743 then (("identifiers "^(strs2str' (subtract op = oids ids))^
744 " not in example"), e_ori_, [])
748 if not (subset op = (map typeless ts, map typeless ots))
751 (map (Print_Mode.setmp [] (Syntax.string_of_term
753 "' not in example (typeless)"), e_ori_, [])
754 else (case seek_orits ctxt sel ts ori of
755 ("", ori_ as (_,_,_,d,ts), all) =>
756 (case test_types ctxt (d,ts) of
757 "" => ("", ori_, all)
758 | msg => (msg, e_ori_, []))
759 | (msg,_,_) => (msg, e_ori_, []))
761 if member op = (map #4 ori) d
762 then seek_oridts ctxt sel (d,ts) ori
763 else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
764 " not in example", (0, [], sel, d, ts), [])
768 (*. for return-value of appl_add .*)
771 | Err of string; (*error-message*)
774 (** add an item to the model; check wrt. oris and pbt **)
775 (* in contrary to oris<>[] below, this part handles user-input
776 extremely acceptive, i.e. accept input instead error-msg *)
777 fun appl_add ctxt sel [] ppc pbt t =
779 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
780 in case parse (ProofContext.theory_of ctxt) t of
781 NONE => Add (i, [], false, sel, Syn t)
783 let val (d, ts) = split_dts (term_of t');
784 in if d = e_term then
785 Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
786 (case find_first (eq1 d) pbt of
787 NONE => Add (i, [], true, sel, Sup (d,ts))
788 | SOME (f, (_, id)) =>
789 let fun eq2 d (i, _, _, _, itm_) =
790 d = (d_in itm_) andalso i <> 0;
791 in case find_first (eq2 d) ppc of
792 NONE => Add (i, [], true, f,
793 Cor ((d, ts), (id, pbl_ids' d ts))
795 | SOME (i', _, _, _, itm_) => if is_list_dsc d then
797 val in_itm = ts_in itm_;
798 val ts' = union op = ts in_itm;
799 val i'' = if in_itm = [] then i else i';
800 in Add (i'', [], true, f,
801 Cor ((d, ts'), (id, pbl_ids' d ts'))
804 Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
808 | appl_add ctxt sel oris ppc pbt str =
809 case parse (ProofContext.theory_of ctxt) str of
810 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
811 | SOME t => case is_known ctxt sel oris (term_of t) of
812 ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
814 | (msg, _) => Err msg)
815 | (msg, _, _) => Err msg;
817 > val (msg,itm) = is_notyet_input thy ppc all ori';
818 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
820 > val ts = ts_in itm_;
824 (** make oris from args of the stac SubProblem and from pbt **)
826 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
827 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
828 fun is_copy_named_idstr str =
829 case (rev o Symbol.explode) str of
830 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
831 "is_copy_named_idstr: " ^ str ^ " T"); true)
832 | _ => (tracing ((strs2str o (rev o Symbol.explode))
833 "is_copy_named_idstr: " ^ str ^ " F"); false);
834 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
836 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
837 fun is_copy_named_generating_idstr str =
838 if is_copy_named_idstr str
839 then case (rev o Symbol.explode) str of
840 "'"::"'"::"'"::_ => false
843 fun is_copy_named_generating (_, (_, t)) =
844 (is_copy_named_generating_idstr o free2str) t;
846 (*.split type-wrapper from scr-arg and build part of an ori;
847 an type-error is reported immediately, raises an exn,
848 subsequent handling of exn provides 2nd part of error message.*)
849 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
850 (* val (thy, (str, (dsc, _)), (ty $ var)) =
853 (cterm_of thy (dsc $ var);(*type check*)
854 SOME ((([1], str, dsc, (*[var]*)
855 split_dts' (dsc, var))): preori)(*:ori without leading #*))
856 handle e as TYPE _ =>
857 (tracing (dashs 70 ^ "\n"
858 ^"*** ERROR while creating the items for the model of the ->problem\n"
859 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
860 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
861 ^"*** description: "^(term_detail2str dsc)
862 ^"*** value: "^(term_detail2str var)
863 ^"*** typeconstructor in script: "^(term_detail2str ty)
864 ^"*** checked by theory: "^(theory2str thy)^"\n"
866 (*OldGoals.print_exn e; raises exn again*)
867 writeln (PolyML.makestring e);
869 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
872 (*.match each pat of the model-pattern with an actual argument;
873 precondition: copy-named vars are filtered out.*)
874 fun matc thy ([]:pat list) _ (oris:preori list) = oris
875 | matc thy pbt [] _ =
877 error ("actual arg(s) missing for '"^pats2str pbt
878 ^"' i.e. should be 'copy-named' by '*_._'"))
879 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
880 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
881 (thy, pbt', ags, []);
883 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
884 (thy, pbt, ags, (oris @ [ori]));
886 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
887 else(*..del?*) let val opt = mtc thy p a;
889 (* val SOME ori = mtc thy p a;
891 SOME ori => matc thy pbt ags (oris @ [ori])
892 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
894 (* run subp-rooteq.sml until Init_Proof before ...
895 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
896 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
898 other vars as in mtc ..
899 > matc thy (drop_last pbt) ags [];
900 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
903 (* generate a new variable "x_i" name from a related given one "x"
904 by use of oris relating "v_i_" (is_copy_named!) to "v_"
905 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
907 (* generate a new variable "x_i" name from a related given one "x"
908 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
909 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
910 but leave is_copy_named_generating as is, e.t. ss''' *)
911 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
912 (if is_copy_named_generating p
913 then (*WN051014 kept strange old code ...*)
914 let fun sel (_,_,d,ts) = comp_ts (d, ts)
915 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
916 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
917 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
918 val vals = map sel oris
919 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
920 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
921 else ([1], field, dsc, [t])
923 handle _ => error ("cpy_nam: for "^(term2str t));
925 (*.match the actual arguments of a SubProblem with a model-pattern
926 and create an ori list (in root-pbl created from formalization).
927 expects ags:pats = 1:1, while copy-named are filtered out of pats;
928 if no 1:1 the exn raised by matc/mtc and handled at call.
929 copy-named pats are appended in order to get them into the model-items.*)
930 fun match_ags thy (pbt:pat list) ags =
931 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
932 val pbt' = filter_out is_copy_named pbt;
933 val cy = filter is_copy_named pbt;
934 val oris' = matc thy pbt' ags [];
935 val cy' = map (cpy_nam pbt' oris') cy;
936 val ors = add_id (oris' @ cy');
937 (*appended in order to get ^^^^^ into the model-items*)
938 in (map flattup ors):ori list end;
940 (*.report part of the error-msg which is not available in match_args.*)
941 fun match_ags_msg pI stac ags =
942 let (*val s = !show_types
943 val _ = show_types:= true*)
944 val pats = (#ppc o get_pbt) pI
945 val msg = (dots 70^"\n"
946 ^"*** problem "^strs2str pI^" has the ...\n"
947 ^"*** model-pattern "^pats2str pats^"\n"
948 ^"*** stac '"^term2str stac^"' has the ...\n"
949 ^"*** arg-list "^terms2str ags^"\n"
951 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
952 (*val _ = show_types:= s*)
956 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
957 fun vars_of_pbl_ pbl_ =
958 let fun var_of_pbl_ (gfr,(dsc,t)) = t
959 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
960 fun vars_of_pbl_' pbl_ =
961 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
962 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
964 fun overwrite_ppc thy itm ppc =
966 fun repl ppc' (_,_,_,_,itm_) [] =
967 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
969 | repl ppc' itm (p::ppc) =
970 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
971 else repl (ppc' @ [p]) itm ppc
972 in repl [] itm ppc end;
974 (*10.3.00: insert the already compiled itm into model;
975 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
978 fun insert_ppc thy itm ppc =
980 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
981 | eq_untouched _ _ = false;
984 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
985 case seek_ppc (#1 itm) ppc of
986 (* val SOME xxx = seek_ppc (#1 itm) ppc;
988 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
989 overwrite_ppc thy itm ppc
990 | NONE => (ppc @ [itm]));
991 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
993 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
994 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
996 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
997 (d_in itm_) = (d_in iitm_);
998 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
999 handles superfluous items carelessly*)
1000 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
1002 > gen_ins' eee (4,[1,3,5,7]);
1003 val it = [1, 3, 5, 7, 4] : int list*)
1006 (*. output the headline to a ppc .*)
1007 fun header p_ pI mI =
1008 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1010 | pos => error ("header called with "^ pos_2str pos);
1013 fun specify_additem sel (ct,_) (p,Met) c pt =
1015 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1016 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1017 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1018 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1019 val cpI = if pI = e_pblID then pI' else pI;
1020 val cmI = if mI = e_metID then mI' else mI;
1021 val {ppc,pre,prls,...} = get_met cmI;
1022 in case appl_add (thy2ctxt thy) sel oris met ppc ct of
1023 Add itm (*..union old input *) =>
1024 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1026 val met' = insert_ppc thy itm met;
1027 (*val pt' = update_met pt p met';*)
1028 val ((p,Met),_,_,pt') =
1029 generate1 thy (case sel of
1030 "#Given" => Add_Given' (ct, met')
1031 | "#Find" => Add_Find' (ct, met')
1032 | "#Relate"=> Add_Relation'(ct, met'))
1033 (Uistate, e_ctxt) (p,Met) pt
1034 val pre' = check_preconds thy prls pre met'
1035 val pb = foldl and_ (true, map fst pre')
1036 (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
1038 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1039 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1040 in ((p,p_), ((p,p_),Uistate),
1041 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1042 (Method cmI, itms2itemppc thy met' pre'))),
1045 let val pre' = check_preconds thy prls pre met
1046 val pb = foldl and_ (true, map fst pre')
1047 (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
1049 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1050 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1051 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1055 | specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1057 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1058 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1059 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1060 val cpI = if pI = e_pblID then pI' else pI;
1061 val cmI = if mI = e_metID then mI' else mI;
1062 val {ppc,where_,prls,...} = get_pbt cpI;
1063 in case appl_add (thy2ctxt thy) sel oris pbl ppc ct of
1064 Add itm (*..union old input *) =>
1065 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1068 (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
1069 val pbl' = insert_ppc thy itm pbl
1070 val ((p,Pbl),_,_,pt') =
1071 generate1 thy (case sel of
1072 "#Given" => Add_Given' (ct, pbl')
1073 | "#Find" => Add_Find' (ct, pbl')
1074 | "#Relate"=> Add_Relation'(ct, pbl'))
1075 (Uistate, e_ctxt) (p,Pbl) pt
1076 val pre = check_preconds thy prls where_ pbl'
1077 val pb = foldl and_ (true, map fst pre)
1078 (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
1080 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1081 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1082 val ppc = if p_= Pbl then pbl' else met;
1083 in ((p,p_), ((p,p_),Uistate),
1084 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1086 itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1089 let val pre = check_preconds thy prls where_ pbl
1090 val pb = foldl and_ (true, map fst pre)
1091 (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
1093 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1094 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1095 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1097 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1098 val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1102 val (msg,itm) = appl_add thy sel oris ppc ct;
1103 val (Cor(d,ts)) = #5 itm;
1110 (* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1111 specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1113 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1114 let (* either """"""""""""""" all empty or complete *)
1115 val thy = assoc_thy dI';
1116 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1117 else pI' |> #ppc o get_pbt |> prep_ori fmz thy |> #1;
1118 val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
1119 (oris,(dI',pI',mI'),e_term);
1120 val {ppc,prls,where_,...} = get_pbt pI'
1121 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1122 val pt = update_pbl pt [] pbl;
1123 val pre = check_preconds thy prls where_ pbl
1124 val pb = foldl and_ (true, map fst pre)*)
1125 val (pbl, pre, pb) = ([], [], false)
1128 (([],Pbl), (([],Pbl),Uistate),
1129 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1130 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1131 Refine_Tacitly pI', Safe,pt)
1133 (([],Pbl), (([],Pbl),Uistate),
1134 Form' (PpcKF (0,EdUndef,(length []),Nundef,
1135 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1139 (*ONLY for STARTING modeling phase*)
1140 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1141 let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
1143 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
1145 val thy' = if dI = e_domID then dI' else dI
1146 val thy = assoc_thy thy'
1147 val {ppc,prls,where_,...} = get_pbt pI'
1148 val pre = check_preconds thy prls where_ pbl
1149 val pb = foldl and_ (true, map fst pre)
1150 val ((p,_),_,_,pt) =
1151 generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
1152 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1153 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1154 in ((p,Pbl), ((p,p_),Uistate),
1155 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1156 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1159 (*. called only if no_met is specified .*)
1160 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1161 let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
1163 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
1165 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1166 (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
1167 (*val pt = update_pbl pt p pbl;
1168 val pt = update_orispec pt p
1169 (string_of_thy thy, pIre,
1170 if length met = 0 then e_metID else hd met);*)
1171 val (domID, metID) = (string_of_thy thy,
1172 if length met = 0 then e_metID else hd met)
1173 val ((p,_),_,_,pt) =
1174 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1175 (Uistate, e_ctxt) pos pt
1176 (*val pre = check_preconds thy prls where_ pbl
1177 val pb = foldl and_ (true, map fst pre)*)
1178 val (pbl, pre, pb) = ([], [], false)
1179 in ((p,Pbl), (pos,Uistate),
1180 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1181 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1182 Model_Problem, Safe, pt) end
1184 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1185 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
1186 (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1187 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1188 Model_Problem, Safe, pt) end
1190 (* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
1191 val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
1193 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1194 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1195 meth=met, ...}) = get_obj I pt p;
1196 (*val pt = update_pbl pt p itms;
1197 val pt = update_pblID pt p pI;*)
1198 val thy = assoc_thy dI
1199 val ((p,Pbl),_,_,pt)=
1200 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
1201 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1202 val mI'' = if mI=e_metID then mI' else mI;
1203 (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
1204 val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1205 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1206 in ((p,Pbl), (pos,Uistate),
1207 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1208 (Problem pI, itms2itemppc dI'' itms pre))),
1210 (* val Specify_Method' mID = nxt; val (p,_) = p;
1211 val Specify_Method' mID = m;
1212 specify (Specify_Method' mID) (p,p_) c pt;
1214 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1215 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1216 meth=met, ...}) = get_obj I pt p;
1217 val {ppc,pre,prls,...} = get_met mID
1218 val thy = assoc_thy dI
1219 val oris = add_field' thy ppc oris;
1220 (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1221 val dI'' = if dI=e_domID then dI' else dI;
1222 val pI'' = if pI = e_pblID then pI' else pI;
1223 val met = if met=[] then pbl else met;
1224 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1225 (*val pt = update_met pt p itms;
1226 val pt = update_metID pt p mID*)
1228 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1229 (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
1230 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1231 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1232 in (pos, (pos,Uistate),
1233 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1234 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1236 (* val Add_Find' ct = nxt; val sel = "#Find";
1238 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1239 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1240 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1241 (* val Specify_Theory' domID = m;
1242 val (Specify_Theory' domID, (p,p_)) = (m, pos);
1244 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1245 let val p_ = case p_ of Met => Met | _ => Pbl
1246 val thy = assoc_thy domID;
1247 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1248 probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
1249 val mppc = case p_ of Met => met | _ => pbl;
1250 val cpI = if pI = e_pblID then pI' else pI;
1251 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1252 val cmI = if mI = e_metID then mI' else mI;
1253 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1256 Met => (check_preconds thy mer mwh met)
1257 | _ => (check_preconds thy per pwh pbl)
1258 val pb = foldl and_ (true, map fst pre)
1261 (*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1262 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1263 (pbl,met) (ppc,mpc) (dI,pI,mI);
1264 in ((p,p_), (pos,Uistate),
1265 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1266 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1268 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1270 (*val pt = update_domID pt p domID;11.8.03*)
1271 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1272 (Uistate, e_ctxt) (p,p_) pt
1273 (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1274 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1275 (ppc,mpc) (domID,pI,mI);
1276 in ((p,p_), (pos,Uistate),
1277 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1278 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1281 (* itms2itemppc thy [](*mpc*) pre
1283 | specify m' _ _ _ =
1284 error ("specify: not impl. for "^tac_2str m');
1286 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1287 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1289 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1291 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1292 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1293 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1294 val cpI = if pI = e_pblID then pI' else pI;
1295 in case appl_add (thy2ctxt thy) sel oris pbl ((#ppc o get_pbt) cpI) ct of
1296 Add itm (*..union old input *) =>
1297 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1300 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1301 val pbl' = insert_ppc thy itm pbl
1304 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1305 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1306 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1307 val ((p,Pbl),c,_,pt') =
1308 generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
1309 in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate' end
1312 (*TODO.WN03 pass error-msgs to the frontend..
1313 FIXME ..and dont abuse a tactic for that purpose*)
1315 Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1316 (e_pos', (e_istate, e_ctxt)))], [], ptp)
1319 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1320 val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1322 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1324 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1325 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1326 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1327 val cmI = if mI = e_metID then mI' else mI;
1328 in case appl_add (thy2ctxt thy) sel oris met ((#ppc o get_met) cmI) ct of
1329 Add itm (*..union old input *) =>
1330 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1332 val met' = insert_ppc thy itm met;
1335 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1336 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1337 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1338 val ((p,Met),c,_,pt') =
1339 generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
1340 in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
1342 | Err msg => ([(*tacis*)], [], ptp)
1343 (*nxt_me collects tacis until not hide; here just no progress*)
1347 val (msg,itm) = appl_add thy sel oris ppc ct;
1348 val (Cor(d,ts)) = #5 itm;
1353 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1354 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1355 handle _ => error ("ori2Coritm: dsc "^
1357 "in ori, but not in pbt")
1359 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1360 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1361 (find_first (eq1 d))) pbt,ts))):itm)
1362 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1363 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1366 (*filter out oris which have same description in itms*)
1367 fun filter_outs oris [] = oris
1368 | filter_outs oris (i::itms) =
1369 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1370 (#4:ori -> term)) oris;
1371 in filter_outs ors itms end;
1373 fun memI a b = member op = a b;
1374 (*filter oris which are in pbt, too*)
1375 fun filter_pbt oris pbt =
1376 let val dscs = map (fst o snd) pbt
1377 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1379 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1380 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1382 fun x mem [] = false
1383 | x mem (y :: ys) = x = y orelse x mem ys;
1385 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1386 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1388 let val vat = max_vt pits;
1390 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1391 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1392 val os = filter_outs ors itms;
1393 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1394 in itms @ (map (ori2Coritm met) os) end
1399 (*.complete model and guard of a calc-head .*)
1401 fun x mem [] = false
1402 | x mem (y :: ys) = x = y orelse x mem ys;
1404 fun complete_mod_ (oris, mpc, ppc, probl) =
1405 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1406 val vat = if probl = [] then 1 else max_vt probl
1407 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1408 val pors = filter_outs pors pits (*which are in pbl already*)
1409 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1411 val pits = pits @ (map (ori2Coritm ppc) pors)
1412 val mits = complete_metitms oris pits [] mpc
1416 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1417 (if dI = e_domID then odI else dI,
1418 if pI = e_pblID then opI else pI,
1419 if mI = e_metID then omI else mI):spec;
1422 (*.find a next applicable tac (for calcstate) and update ptree
1423 (for ev. finding several more tacs due to hide).*)
1424 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1425 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1426 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1427 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1429 val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1430 val (dI, pI, mI) = some_spec ospec spec
1431 val thy = assoc_thy dI
1432 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1433 val {cas, ppc, ...} = get_pbt pI
1434 val pbl = init_pbl ppc (* fill in descriptions *)
1435 (*----------------if you think, this should be done by the Dialog
1436 in the java front-end, search there for WN060225-modelProblem----*)
1437 val (pbl, met) = case cas of NONE => (pbl, [])
1438 | _ => complete_mod_ (oris, mpc, ppc, probl)
1439 (*----------------------------------------------------------------*)
1440 val tac_ = Model_Problem' (pI, pbl, met)
1441 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
1442 in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1444 (* val Add_Find ct = tac;
1446 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1447 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1448 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1450 (*. called only if no_met is specified .*)
1451 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1452 let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1453 val opt = refine_ori oris pI
1456 let val {met,ppc,...} = get_pbt pI'
1457 val pbl = init_pbl ppc
1458 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1459 val mI = if length met = 0 then e_metID else hd met
1460 val thy = assoc_thy dI
1462 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1463 (Uistate, e_ctxt) pos pt
1464 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1465 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1466 | NONE => ([], [], ptp)
1469 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1470 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1471 probl, ...}) = get_obj I pt p
1472 val thy = if dI' = e_domID then dI else dI'
1473 in case refine_pbl (assoc_thy thy) pI probl of
1474 NONE => ([], [], ptp)
1475 | SOME (rfd as (pI',_)) =>
1476 let val (pos,c,_,pt) =
1477 generate1 (assoc_thy thy)
1478 (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1479 in ([(Refine_Problem pI, Refine_Problem' rfd,
1480 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1483 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1484 let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1485 probl, ...}) = get_obj I pt p;
1486 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1487 val {ppc,where_,prls,...} = get_pbt pI
1488 val pbl as (_,(itms,_)) =
1489 if pI'=e_pblID andalso pI=e_pblID
1490 then (false, (init_pbl ppc, []))
1491 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1492 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1493 val ((p,Pbl),c,_,pt)=
1494 generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
1495 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1496 (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1498 (*transfers oris (not required in pbl) to met-model for script-env
1499 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1500 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1501 let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1502 meth=met, ...}) = get_obj I pt p;
1503 val {ppc,pre,prls,...} = get_met mID
1504 val thy = assoc_thy dI
1505 val oris = add_field' thy ppc oris;
1506 val dI'' = if dI=e_domID then dI' else dI;
1507 val pI'' = if pI = e_pblID then pI' else pI;
1508 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1509 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1511 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1512 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1513 (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1515 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1516 let val (dI',_,_) = get_obj g_spec pt p
1518 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1519 (Uistate, e_ctxt) pos pt
1520 in (*FIXXXME: check if pbl can still be parsed*)
1521 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1524 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1525 let val (dI',_,_) = get_obj g_spec pt p
1527 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1528 (Uistate, e_ctxt) pos pt
1529 in (*FIXXXME: check if met can still be parsed*)
1530 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1534 error ("nxt_specif: not impl. for "^tac2str m');
1536 (*.get the values from oris; handle the term list w.r.t. penv.*)
1539 fun x mem [] = false
1540 | x mem (y :: ys) = x = y orelse x mem ys;
1542 fun vals_of_oris oris =
1543 ((map (mkval' o (#5:ori -> term list))) o
1544 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1549 (* create a calc-tree with oris via an cas.refined pbl *)
1550 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1551 if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1552 let val {cas, met, ppc, thy, ...} = get_pbt pI
1553 val dI = if dI = "" then theory2theory' thy else dI
1554 val thy = assoc_thy dI
1555 val mI = if mI = [] then hd met else mI
1556 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1557 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1558 ([], (dI,pI,mI), hdl)
1559 val pt = update_spec pt [] (dI,pI,mI)
1560 val pits = init_pbl' ppc
1561 val pt = update_pbl pt [] pits
1562 in ((pt, ([] ,Pbl)), []) : calcstate end
1563 else if mI <> [] then (* from met-browser *)
1564 let val {ppc,...} = get_met mI
1565 val dI = if dI = "" then "Isac" else dI
1566 val thy = assoc_thy dI;
1567 val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1568 ([], (dI,pI,mI), e_term(*FIXME met*));
1569 val pt = update_spec pt [] (dI,pI,mI);
1570 val mits = init_pbl' ppc;
1571 val pt = update_met pt [] mits;
1572 in ((pt, ([], Met)), []) : calcstate end
1573 else (* new example, pepare for interactive modeling *)
1574 let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1575 ([], e_spec, e_term)
1576 in ((pt,([],Pbl)), []) : calcstate end
1577 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1578 let (* both """"""""""""""""""""""""" either empty or complete *)
1579 val thy = assoc_thy dI
1580 val (pI, pors, mI) =
1582 then let val pors = get_pbt pI |> #ppc |> prep_ori fmz thy |> #1;
1583 val pI' = refine_ori' pors pI;
1584 in (pI', pors(*refinement over models with diff.precond only*),
1585 (hd o #met o get_pbt) pI') end
1586 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
1587 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1588 val dI = theory2theory' (maxthy thy thy');
1589 val hdl = case cas of
1590 NONE => pblterm dI pI
1591 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1592 ~~~ vals_of_oris pors) t;
1593 val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
1594 (pors, (dI, pI, mI), hdl)
1595 in ((pt, ([], Pbl)),
1596 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1602 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1603 (* case appl_spec p pt m of /// 19.1.00
1604 Notappl e => Error' (Error_ e)
1606 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1610 (*fun tag_form thy (formal, given) = cterm_of thy
1611 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1612 fun tag_form thy (formal, given) =
1613 (let val gf = (head_of given) $ formal;
1614 val _ = cterm_of thy gf
1617 error ("calchead.tag_form: " ^
1618 Print_Mode.setmp [] (Syntax.string_of_term
1619 (thy2ctxt thy)) given ^ " .. " ^
1620 Print_Mode.setmp [] (Syntax.string_of_term
1621 (thy2ctxt thy)) formal ^
1622 " ..types do not match");
1623 (* val formal = (the o (parse thy)) "[R::real]";
1624 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1625 > tag_form thy (formal, given);
1626 val it = "fixed_values [R]" : cterm
1629 fun chktyp thy (n, fs, gs) =
1630 ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1632 (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1634 tag_form thy (nth n fs, nth n gs));
1635 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1637 (* #####################################################
1638 find the failing item:
1640 > val tag__form = chktyp (n,formals,givens);
1641 > (type_of o term_of o (nth n)) formals;
1642 > (type_of o term_of o (nth n)) givens;
1643 > atomty ((term_of o (nth n)) formals);
1644 > atomty ((term_of o (nth n)) givens);
1645 > atomty (term_of tag__form);
1646 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1647 ##################################################### *)
1649 (* #####################################################
1651 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1652 val formals = map (the o (parse thy)) origin;
1654 val given = ["equation (lhs=rhs)",
1655 "bound_variable bdv", (* TODO type *)
1657 val where_ = ["e is_root_equation_in bdv",
1659 "apx is_const_expr"];
1660 val find = ["L::rat set"];
1661 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1662 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1663 val givens = map (the o (parse thy)) given;
1665 val tag__forms = chktyps (formals, givens);
1666 map ((atomty) o term_of) tag__forms;
1667 ##################################################### *)
1670 (* check pbltypes, announces one failure a time *)
1671 (*fun chk_vars ctppc =
1672 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1673 appc flat (mappc (vars o term_of) ctppc)
1674 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1675 else if (re\\(gi union fi)) <> []
1676 then ("re\\(gi union fi)",re\\(gi union fi))
1677 else ("ok",[]) end;*)
1678 fun chk_vars ctppc =
1679 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1680 appc flat (mappc vars ctppc)
1681 val chked = subtract op = gi wh
1682 in if chked <> [] then ("wh\\gi", chked)
1683 else let val chked = subtract op = (union op = gi fi) re
1685 then ("re\\(gi union fi)", chked)
1690 (* check a new pbltype: variables (Free) unbound by given, find*)
1691 fun unbound_ppc ctppc =
1692 let val {Given=gi,Find=fi,Relate=re,...} =
1693 appc flat (mappc vars ctppc)
1694 in distinct (*re\\(gi union fi)*)
1695 (subtract op = (union op = gi fi) re) end;
1697 > val org = {Given=["[R=(R::real)]"],Where=[],
1698 Find=["[A::real]"],With=[],
1699 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1701 > val ctppc = mappc (the o (parse thy)) org;
1702 > unbound_ppc ctppc;
1703 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1707 (* f, a binary operator, is nested rightassociative *)
1710 fun fld f (x::[]) = x
1711 | fld f (x::x'::[]) = f (x',x)
1712 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1713 in ((fld f) o rev) xs end;
1715 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1716 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1717 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1718 > cterm_of thy conj;
1719 val it = "(a = b & c = d) & e = f" : cterm
1722 (* f, a binary operator, is nested leftassociative *)
1723 fun foldl1 f (x::[]) = x
1724 | foldl1 f (x::x'::[]) = f (x,x')
1725 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1727 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1728 > val ces = map (cterm_of thy) (isalist2list (term_of ct));
1729 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1730 > cterm_of thy conj;
1731 val it = "a = b & c = d & e = f & g = h" : cterm
1735 (* called only once, if a Subproblem has been located in the script*)
1736 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
1737 (* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
1741 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1742 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1743 (*all stored in tac_ itms ^^^^^^^^^^*)
1744 | nxt_model_pbl tac_ _ =
1745 error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1746 (* run subp_rooteq.sml ''
1747 until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
1748 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1749 (last_elem o drop_last) ets'';
1750 > val mst = (last_elem o drop_last) ets'';
1751 > nxt_model_pbl mst;
1752 val it = Refine_Tacitly ["univariate","equation"] : tac
1755 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1756 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1757 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1760 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1761 + met from fmz; assumes pos on PblObj, meth = [].*)
1762 fun complete_mod (pt, pos as (p, p_):pos') =
1763 (* val (pt, (p, _)) = (pt, p);
1764 val (pt, (p, _)) = (pt, pos);
1766 let val _= if p_ <> Pbl
1767 then tracing("###complete_mod: only impl.for Pbl, called with "^
1768 pos'2str pos) else ()
1769 val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
1771 val (dI,pI,mI) = some_spec ospec spec
1772 val mpc = (#ppc o get_met) mI
1773 val ppc = (#ppc o get_pbt) pI
1774 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1775 val pt = update_pblppc pt p pits
1776 val pt = update_metppc pt p mits
1777 in (pt, (p,Met):pos') end
1779 (*| complete_mod (pt, pos as (p, Met):pos') =
1780 error ("###complete_mod: only impl.for Pbl, called with "^
1783 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1784 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1785 fun all_modspec (pt, (p,_):pos') =
1786 (* val (pt, (p,_)) = ptp;
1788 let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1789 ...}) = get_obj I pt p;
1790 val thy = assoc_thy dI;
1791 val {ppc,...} = get_met mI;
1792 val mors = prep_ori fmz_ thy ppc |> #1;
1793 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1794 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1795 val pt = update_spec pt p (dI,pI,mI);
1796 in (pt, (p,Met): pos') end;
1798 (*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1799 fun is_complete_mod_ ([]: itm list) = false
1800 | is_complete_mod_ itms =
1801 foldl and_ (true, (map #3 itms));
1802 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1803 if (is_pblobj o (get_obj I pt)) p
1804 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1805 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1806 | is_complete_mod (pt, pos as (p, Met)) =
1807 if (is_pblobj o (get_obj I pt)) p
1808 then (is_complete_mod_ o (get_obj g_met pt)) p
1809 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1810 | is_complete_mod (_, pos) =
1811 error ("is_complete_mod called by "^pos'2str pos^
1812 " (should be Pbl or Met)");
1814 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1815 fun is_complete_spec (pt, pos as (p,_): pos') =
1816 if (not o is_pblobj o (get_obj I pt)) p
1817 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1818 else let val (dI,pI,mI) = get_obj g_spec pt p
1819 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1820 (*.complete empty items in specification from origin (pbl, met ev.refined);
1821 assumes 'is_complete_mod'.*)
1822 fun complete_spec (pt, pos as (p,_): pos') =
1823 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1824 val pt = update_spec pt p (some_spec ospec spec)
1827 fun is_complete_modspec ptp =
1828 is_complete_mod ptp andalso is_complete_spec ptp;
1833 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1834 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1836 let val (_,_,metID) = get_somespec' spec spec'
1838 if metID = e_metID then []
1839 else let val {prls,pre=where_,...} = get_met metID
1840 val pre = check_preconds' prls where_ meth 0
1842 val allcorrect = is_complete_mod_ meth
1843 andalso foldl and_ (true, (map #1 pre))
1844 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1845 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1846 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1848 let val (_,pI,_) = get_somespec' spec spec'
1850 if pI = e_pblID then []
1851 else let val {prls,where_,cas,...} = get_pbt pI
1852 val pre = check_preconds' prls where_ probl 0
1854 val allcorrect = is_complete_mod_ probl
1855 andalso foldl and_ (true, (map #1 pre))
1856 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1859 fun pt_form (PrfObj {form,...}) = Form form
1860 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1861 let val (dI, pI, _) = get_somespec' spec spec'
1862 val {cas,...} = get_pbt pI
1864 NONE => Form (pblterm dI pI)
1865 | SOME t => Form (subst_atomic (mk_env probl) t)
1867 (*vvv takes the tac _generating_ the formula=result, asm ok....
1868 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1870 if null asm then NONE else SOME asm,
1872 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1873 let val (_,_,metID) = some_spec ospec spec
1875 if null asm then NONE else SOME asm,
1876 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1877 -------------------------------------------------------------------------*)
1880 (*.pt_extract returns
1881 # the formula at pos
1882 # the tactic applied to this formula
1883 # the list of assumptions generated at this formula
1884 (by application of another tac to the preceding formula !)
1885 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1886 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1887 fun pt_extract (pt,([],Res)) =
1888 (* val (pt,([],Res)) = ptp;
1890 let val (f, asm) = get_obj g_result pt []
1891 in (Form f, NONE, asm) end
1894 | pt_extract (pt,(p,Res)) =
1895 (* val (pt,(p,Res)) = ptp;
1897 let val (f, asm) = get_obj g_result pt p
1898 val tac = if last_onlev pt p
1899 then if is_pblobj' pt (lev_up p)
1900 then let val (PblObj{spec=(_,pI,_),...}) =
1901 get_obj I pt (lev_up p)
1902 in if pI = e_pblID then NONE
1903 else SOME (Check_Postcond pI) end
1904 else SOME End_Trans (*WN0502 TODO for other branches*)
1905 else let val p' = lev_on p
1906 in if is_pblobj' pt p'
1907 then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1909 in SOME (Subproblem (dI, pI)) end
1910 else if f = get_obj g_form pt p'
1911 then SOME (get_obj g_tac pt p')
1912 (*because this Frm ~~~is not on worksheet*)
1913 else SOME (Take (term2str (get_obj g_form pt p')))
1915 in (Form f, tac, asm) end
1917 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1918 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1919 val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
1921 let val ppobj = get_obj I pt p
1922 val f = if is_pblobj ppobj then pt_model ppobj p_
1923 else get_obj pt_form pt p
1924 val tac = g_tac ppobj
1925 in (f, SOME tac, []) end;
1928 (**. get the formula from a ctree-node:
1929 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1930 take res from all other PrfObj's .**)
1931 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1932 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1933 [("headline", (p, Frm), h),
1934 ("stepform", (p, Res), r)]
1935 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1936 [("stepform", (p, Frm), form),
1937 ("stepform", (p, Res), r)];
1939 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1940 [("stepform", (p, Res), r)]
1942 (*assumes to take whole level, in particular hd -- for use in interSteps*)
1943 fun get_formress fs p [] = flat fs
1944 | get_formress fs p (nd::nds) =
1945 (* start with 'form+res' and continue with trying 'res' only*)
1946 get_forms (fs @ [formres p nd]) (lev_on p) nds
1947 and get_forms fs p [] = flat fs
1948 | get_forms fs p (nd::nds) =
1950 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1951 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1952 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1953 (* continue with trying 'res' only*)
1954 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1956 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1957 (*WN050219 made robust against _'to' below or after Complete nodes
1958 by handling exn caused by move_dn*)
1959 (*WN0401 this functionality belongs to ctree.sml,
1960 but fetching a calc_head requires calculations defined in modspec.sml
1961 transfer to ME/me.sml !!!
1962 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1963 is returned !!!!!!!!!!!!!
1965 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1966 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1967 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1971 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1975 | eq_pos' _ _ = false;
1977 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
1978 total ordering Position#compareTo(Position p) in the java-code
1979 val get_interval = fn
1980 : pos' -> : from is "move_up 1st-element" to return
1981 pos' -> : to the last element to be returned; from < to
1982 int -> : level: 0 gets the flattest sub-tree possible
1983 >999 gets the deepest sub-tree possible
1985 (pos' * : of the formula
1986 Term.term) : the formula
1989 fun get_interval from to level pt =
1990 (* val (from,level) = (f,lev);
1991 val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
1993 let fun get_inter c (from:pos') (to:pos') lev pt =
1994 (* val (c, from, to, lev) = ([], from, to, level);
1995 ------for recursion.......
1996 val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
1998 if eq_pos' from to orelse from = ([],Res)
1999 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
2000 if 'to' has values NOT generated by move_dn, see systest/me.sml
2001 TODO.WN0501: introduce an order on pos' and check "from > to"..
2002 ...there is an order in Java!
2003 WN051224 the hack got worse with returning term instead ptform*)
2004 then let val (f,_,_) = pt_extract (pt, from)
2006 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
2007 | Form t => c @ [(from, t)]
2010 if lev < lev_of from
2011 then (get_inter c (move_dn [] pt from) to lev pt)
2012 handle (PTREE _(*from move_dn too far*)) => c
2013 else let val (f,_,_) = pt_extract (pt, from)
2014 val term = case f of
2015 ModSpec (_,_,headline,_,_,_)=> headline
2017 in (get_inter (c @ [(from, term)])
2018 (move_dn [] pt from) to lev pt)
2019 handle (PTREE _(*from move_dn too far*))
2020 => c @ [(from, term)] end
2021 in get_inter [] from to level pt end;
2024 fun posform2str (pos:pos', form) =
2025 "("^ pos'2str pos ^", "^
2027 Form f => term2str f
2028 | ModSpec c => term2str (#3 c(*the headline*)))
2030 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2031 (map posform2str)) pfs;
2032 fun posterm2str (pos:pos', t) =
2033 "("^ pos'2str pos ^", "^term2str t^")";
2034 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2035 (map posterm2str)) pfs;
2038 (*WN050225 omits the last step, if pt is incomplete*)
2040 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
2042 (*.get a calchead from a PblObj-node in the ctree;
2043 preconditions must be calculated.*)
2044 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
2045 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
2047 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2048 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
2049 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
2050 | get_ocalhd (pt, pos' as (p,Met):pos') =
2051 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2054 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2055 val pre = check_preconds (assoc_thy"Isac") prls pre meth
2056 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
2058 (*.at the activeFormula set the Model, the Guard and the Specification
2059 to empty and return a CalcHead;
2060 the 'origin' remains (for reconstructing all that).*)
2061 fun reset_calchead (pt, pos' as (p,_):pos') =
2062 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
2063 val pt = update_pbl pt p []
2064 val pt = update_met pt p []
2065 val pt = update_spec pt p e_spec
2066 in (pt, (p,Pbl):pos') end;