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, Mathias Lehnfeld
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 oris2fmz_vals : ori list -> string list * term list
115 val maxl : int list -> int
116 val match_ags_msg : string list -> Term.term -> Term.term list -> unit
117 val memI : ''a list -> ''a -> bool
118 val mk_additem : string -> cterm' -> tac
119 val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
121 theory -> pat -> Term.term -> SpecifyTools.preori option
124 SpecifyTools.ori list ->
125 (string * (Term.term * 'a)) list ->
126 SpecifyTools.itm list -> (string * cterm') option
127 val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
131 SpecifyTools.ori list ->
133 SpecifyTools.itm list * SpecifyTools.itm list ->
134 (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->
136 val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'
137 val nxt_specif_additem :
138 string -> cterm' -> ptree * (int list * pos_) -> calcstate'
139 val nxt_specify_init_calc : fmz -> calcstate
140 val ocalhd_complete :
141 SpecifyTools.itm list ->
142 (bool * Term.term) list -> domID * pblID * metID -> bool
144 pat list -> ori -> itm
147 Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
150 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
151 SpecifyTools.itm list ->
152 (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
153 val parse_ok : SpecifyTools.itm_ list -> bool
154 val posform2str : pos' * ptform -> string
155 val posforms2str : (pos' * ptform) list -> string
156 val posterms2str : (pos' * term) list -> string (*tests only*)
157 val ppc135list : 'a SpecifyTools.ppc -> 'a list
158 val ppc2list : 'a SpecifyTools.ppc -> 'a list
160 ptree * (int list * pos_) ->
161 ptform * tac option * Term.term list
162 val pt_form : ppobj -> ptform
163 val pt_model : ppobj -> pos_ -> ptform
164 val reset_calchead : ptree * pos' -> ptree * pos'
168 Term.term * Term.term list ->
169 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
170 -> string * SpecifyTools.ori * Term.term list
175 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
176 -> string * SpecifyTools.ori * Term.term list
178 int -> SpecifyTools.itm list -> SpecifyTools.itm option
179 val show_pt : ptree -> unit
180 val some_spec : spec -> spec -> spec
186 (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *
188 val specify_additem :
194 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
195 val tag_form : theory -> term * term -> term
196 val test_types : Proof.context -> Term.term * Term.term list -> string
197 val typeless : Term.term -> Term.term
198 val unbound_ppc : term SpecifyTools.ppc -> Term.term list
199 val vals_of_oris : SpecifyTools.ori list -> Term.term list
200 val variants_in : Term.term list -> int
201 val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
202 val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
209 structure CalcHead (**): CALC_HEAD(**) =
215 (*.the state wich is stored after each step of calculation; it contains
216 the calc-state and a list of [tac,istate](="tacis") to be applied next.
217 the last_elem tacis is the first to apply to the calc-state and
218 the (only) one shown to the front-end as the 'proposed tac'.
219 the calc-state resulting from the application of tacis is not stored,
220 because the tacis hold enough information for efficiently rebuilding
221 this state just by "fun generate ".*)
223 (ptree * pos') * (*the calc-state to which the tacis could be applied*)
224 (taci list); (*ev. several (hidden) steps;
225 in REVERSE order: first tac_ to apply is last_elem*)
226 val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
228 (*the state used during one calculation within the mathengine; it contains
229 a list of [tac,istate](="tacis") which generated the the calc-state;
230 while this state's tacis are extended by each (internal) step,
231 the calc-state is used for creating new nodes in the calc-tree
232 (eg. applicable_in requires several particular nodes of the calc-tree)
233 and then replaced by the the newly created;
234 on leave of the mathengine the resuing calc-state is dropped anyway,
235 because the tacis hold enought information for efficiently rebuilding
236 this state just by "fun generate ".*)
238 taci list * (*cas. several (hidden) steps;
239 in REVERSE order: first tac_ to apply is last_elem*)
240 pos' list * (*a "continuous" sequence of pos',
241 deleted by application of taci list*)
242 (ptree * pos'); (*the calc-state resulting from the application of tacis*)
243 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
245 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
246 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (Thm.term_of o the o (parse thy)) f
247 | f_mout thy _ = error "f_mout: not called with formula";
250 (*.is the calchead complete ?.*)
251 fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
252 foldl and_ (true, map #3 its) andalso
253 foldl and_ (true, map #1 pre) andalso
254 dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
256 (*["BOOL (1+x=2)","REAL x"] --match_ags--> oris
257 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"]*)
258 fun oris2fmz_vals oris =
259 let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) =
260 ((term2str o comp_dts') (dsc, ts), last_elem ts)
261 handle _ => error ("ori2fmz_env called with "^terms2str ts)
262 in (split_list o (map ori2fmz_vals)) oris end;
264 (* make a term 'typeless' for comparing with another 'typeless' term;
265 'type-less' usually is illtyped *)
266 fun typeless (Const(s,_)) = (Const(s,e_type))
267 | typeless (Free(s,_)) = (Free(s,e_type))
268 | typeless (Var(n,_)) = (Var(n,e_type))
269 | typeless (Bound i) = (Bound i)
270 | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
271 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
273 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
274 > val (_,t1) = split_dsc_t hs (Thm.term_of ct);
275 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
276 > val (_,t2) = split_dsc_t hs (Thm.term_of ct);
277 > typeless t1 = typeless t2;
283 (*.to an input (d,ts) find the according ori and insert the ts.*)
284 (*WN.11.03: + dont take first inter<>[]*)
285 fun seek_oridts ctxt sel (d,ts) [] =
286 ("seek_oridts: input ('" ^
287 (term_to_string' ctxt (comp_dts (d,ts))) ^ "') not found in oris (typed)",
290 | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =
291 if sel = sel' andalso d = d' andalso (inter op = ts ts') <> [] then
292 ("", (id, vat, sel, d, inter op = ts ts'), ts') else
293 seek_oridts ctxt sel (d, ts) oris;
295 (*.to an input (_,ts) find the according ori and insert the ts.*)
296 fun seek_orits ctxt sel ts [] =
297 ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^
298 "') not found in oris (typed)", e_ori_, [])
299 | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
300 if sel = sel' andalso (inter op = ts ts') <> []
302 then ("", (id,vat,sel,d, inter op = ts ts'):ori, ts')
303 else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])
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;
319 datatype appl = Appl of tac_ | Notappl of string;
321 fun ppc2list ({Given=gis,Where=whs,Find=fis,
322 With=wis,Relate=res}: 'a ppc) =
323 gis @ whs @ fis @ wis @ res;
324 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
330 (* get the number of variants in a problem in 'original',
331 assumes equal descriptions in immediate sequence *)
333 let fun eq(x,y) = head_of x = head_of y;
334 fun cnt eq [] y n = ([n],[])
335 | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
337 fun coll eq xs [] = xs
338 | coll eq xs (y::ys) =
339 let val (n,ys') = cnt eq (y::ys) y 0;
340 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
341 val vts = subtract op = [1] (distinct (coll eq [] ts));
342 in case vts of [] => 1 | [n] => n
343 | _ => error "different variants in formalization" end;
345 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
346 val it = ([3],[4,5,5,5,5,5]) : int list * int list
347 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
348 val it = [1,3,1,5] : int list
351 fun is_list_type (Type("List.list",_)) = true
352 | is_list_type _ = false;
353 (* fun destr (Type(str,sort)) = (str,sort);
354 > val (SOME ct) = parse thy "lll::real list";
355 > val ty = (#T o rep_cterm) ct;
359 val it = ("List.list",["RealDef.real"]) : string * typ list
360 > atomty ((#t o rep_cterm) ct);
362 *** Free ( lll, real list)
365 > val (SOME ct) = parse thy "[lll::real]";
366 > val ty = (#T o rep_cterm) ct;
370 val it = ("List.list",["'a"]) : string * typ list
371 > atomty ((#t o rep_cterm) ct);
373 *** Const ( List.list.Cons, [real, real list] => real list)
374 *** Free ( lll, real)
375 *** Const ( List.list.Nil, real list)
377 > val (SOME ct) = parse thy "lll";
378 > val ty = (#T o rep_cterm) ct;
380 val it = false : bool *)
383 fun has_list_type (Free(_,T)) = is_list_type T
384 | has_list_type _ = false;
386 > val (SOME ct) = parse thy "lll::real list";
387 > has_list_type (Thm.term_of ct);
389 > val (SOME ct) = parse thy "[lll::real]";
390 > has_list_type (Thm.term_of ct);
391 val it = false : bool *)
393 fun is_parsed (Syn _) = false
394 | is_parsed _ = true;
395 fun parse_ok its = foldl and_ (true, map is_parsed its);
397 fun all_dsc_in itm_s =
399 fun d_in (Cor ((d,_),_)) = [d]
402 | d_in (Inc ((d,_),_)) = [d]
403 | d_in (Sup (d,_)) = [d]
404 | d_in (Mis (d,_)) = [d];
405 in (flat o (map d_in)) itm_s end;
408 fun is_Syn (Syn _) = true
409 | is_Syn (Typ _) = true
412 fun is_error (Cor (_,ts)) = false
413 | is_error (Sup (_,ts)) = false
414 | is_error (Inc (_,ts)) = false
415 | is_error (Mis (_,ts)) = false
419 fun ct_in (Syn (c)) = c
420 | ct_in (Typ (c)) = c
421 | ct_in _ = error "ct_in called for Cor .. Sup";
424 (*#############################################################*)
425 (*#############################################################*)
426 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
429 (* testdaten besorgen:
430 use"test-coil-kernel.sml";
431 val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
436 variant V: oris union ppc => int, id ID: oris union ppc => int
439 EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
442 @vt = max sum(i : ppc) V i
448 > ((vts_cnt (vts_in itms))) itms;
453 > val vts = vts_in itms;
454 val vts = [1,2,3] : int list
455 > val nvts = vts_cnt vts itms;
456 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
457 > val mx = max2 nvts;
458 val mx = (3,7) : int * int
459 > val v = max_vt itms;
461 --------------------------
465 (*.get the first term in ts from ori.*)
466 (* val (_,_,fd,d,ts) = hd miss;
468 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
469 (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm');
470 (* val t = comp_dts (d,[hd ts]);
473 (* get a term from ori, notyet input in itm.
474 the term from ori is thrown back to a string in order to reuse
475 machinery for immediate input by the user. *)
476 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
477 (fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm')
479 (* in FE dsc, not dat: this is in itms ...*)
480 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
481 | is_untouched _ = false;
484 (* select an item in oris, notyet input in itms
485 (precondition: in itms are only Cor, Sup, Inc) *)
488 | x mem (y :: ys) = x = y orelse x mem ys;
492 oris: from formalization 'type fmz', structured for efficient access
493 pbt : the problem-pattern to be matched with oris in order to get itms
494 itms: already input items
496 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
498 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
499 fun is_elem itms (f,(d,t)) =
500 case find_first (test_d d) itms of
501 SOME _ => true | NONE => false;
502 in case filter_out (is_elem itms) pbt of
503 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
506 SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')
509 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
511 | nxt_add thy oris pbt itms =
513 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
514 andalso (#3 ori) <>"#undef";
515 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
516 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
517 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
518 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
519 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
520 | false_and_not_Sup (i,v,false,f, _) = true
521 | false_and_not_Sup _ = false;
523 val v = if itms = [] then 1 else max_vt itms;
524 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
525 val vits = if v = 0 then itms (*because of dsc without dat*)
526 else filter (testi_vt v) itms; (*itms..vat*)
527 val icl = filter false_and_not_Sup vits; (* incomplete *)
529 then case filter_out (test_id (map #1 vits)) vors of
531 (* val miss = filter_out (test_id (map #1 vits)) vors;
533 | miss => SOME (getr_ct thy (hd miss))
535 case find_first (test_subset (hd icl)) vors of
536 (* val SOME ori = find_first (test_subset (hd icl)) vors;
538 NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
539 | SOME ori => SOME (geti_ct thy ori (hd icl))
545 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
546 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
547 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
548 | mk_delete thy str _ =
549 error ("mk_delete: called with field '"^str^"'");
550 fun mk_additem "#Given" ct = Add_Given ct
551 | mk_additem "#Find" ct = Add_Find ct
552 | mk_additem "#Relate"ct = Add_Relation ct
554 error ("mk_additem: called with field '"^str^"'");
557 (* determine the next step of specification;
558 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
559 eg. in rootpbl 'no_met':
561 preok predicates are _all_ ok (and problem matches completely)
562 oris immediately from formalization
563 (dI',pI',mI') specification coming from author/parent-problem
564 (pbl, item lists specified by user
565 met) -"-, tacitly completed by copy_probl
566 (dI,pI,mI) specification explicitly done by the user
567 (pbt, mpc) problem type, guard of method
569 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
570 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
571 ((*tracing"### nxt_spec Pbl";*)
572 if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
573 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
574 else case find_first (is_error o #5) (pbl:itm list) of
575 SOME (_, _, _, fd, itm_) =>
577 (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
579 ((*tracing"### nxt_spec is_error NONE";*)
580 case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
582 SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
583 (Pbl, mk_additem fd ct'))
584 | NONE => (*pbl-items complete*)
585 if not preok then (Pbl, Refine_Problem pI')
587 if dI = e_domID then (Pbl, Specify_Theory dI')
588 else if pI = e_pblID then (Pbl, Specify_Problem pI')
589 else if mI = e_metID then (Pbl, Specify_Method mI')
591 case find_first (is_error o #5) met of
592 SOME (_,_,_,fd,itm_) =>
593 (Met, mk_delete (assoc_thy dI) fd itm_)
595 (case nxt_add (assoc_thy dI) oris mpc met of
596 SOME (fd,ct') => (*30.8.01: pre?!?*)
597 (Met, mk_additem fd ct')
599 ((*Solv 3.4.00*)Met, Apply_Method mI))))
601 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
602 ((*tracing"### nxt_spec Met"; *)
603 case find_first (is_error o #5) met of
604 SOME (_,_,_,fd,itm_) =>
605 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
607 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
608 SOME (fd,ct') => (Met, mk_additem fd ct')
610 ((*tracing"### nxt_spec Met: nxt_add NONE";*)
611 if dI = e_domID then (Met, Specify_Theory dI')
612 else if pI = e_pblID then (Met, Specify_Problem pI')
613 else if not preok then (Met, Specify_Method mI)
614 else (Met, Apply_Method mI)));
617 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
618 (2,[2],true,"#Find",Syn("empty"))];
621 fun is_field_correct sel d dscpbt =
622 case assoc (dscpbt, sel) of
624 | SOME ds => member op = ds d;
626 (*. update the itm_ already input, all..from ori .*)
627 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
629 fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
631 val ts' = union op = (ts_in itm_) ts;
632 val pval = pbl_ids' d ts'
633 (*WN.9.5.03: FIXXXME [#0, epsilon]
634 here would upd_penv be called for [#0, epsilon] etc. *)
635 val complete = if eq_set op = (ts', all) then true else false;
638 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
639 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
640 | (Syn c) => error ("ori_2itm wants to overwrite "^c)
641 | (Typ c) => error ("ori_2itm wants to overwrite "^c)
642 | (Inc _) => if complete
643 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
644 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
645 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
646 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
647 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
648 (* 28.1.00: not completely clear ---^^^ etc.*)
649 (* 4.9.01: Mis just copied---vvv *)
650 | (Mis _) => if complete
651 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
652 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
656 fun eq1 d (_,(d',_)) = (d = d');
657 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
660 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
661 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
662 pval: value for problem-environment _NOT_ checked for 'inter' --
663 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
664 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
665 (*. is_input ori itms <=>
666 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
667 (2) ori(ts) subset itm(ts) --- Err "already input"
668 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
669 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
670 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
672 fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
673 case find_first (eq1 d) pbt of
675 (case find_first (eq3 f d) itms of
676 SOME (_,_,_,_,itm_) =>
678 val ts' = inter op = (ts_in itm_) ts;
680 if subset op = (ts, ts')
681 then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm)(*2*)
682 else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
684 | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[]))) pid all (i,v,f,d,ts))) (*1*)
685 | NONE => ("", ori_2itm (Sup (d,ts)) e_term all (i,v,f,d,ts));
687 fun test_types ctxt (d,ts) =
689 val opt = (try comp_dts) (d,ts);
690 val msg = case opt of
692 | NONE => (term_to_string' ctxt d ^ " " ^
693 (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped");
696 fun maxl [] = error "maxl of []"
699 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
703 (*. is the input term t known in oris ?
704 give feedback on all(?) strange input;
705 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
706 fun is_known ctxt sel ori t =
708 val _ = tracing ("RM is_known: t=" ^ term2str t);
709 val ots = (distinct o flat o (map #5)) (ori:ori list);
710 val oids = ((map (fst o dest_Free)) o distinct o
711 flat o (map vars)) ots;
712 val (d, ts) = split_dts t;
713 val ids = map (fst o dest_Free)
714 ((distinct o (flat o (map vars))) ts);
715 in if (subtract op = oids ids) <> []
716 then (("identifiers "^(strs2str' (subtract op = oids ids)) ^
717 " not in example"), e_ori_, [])
721 if not (subset op = (map typeless ts, map typeless ots))
722 then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
723 "' not in example (typeless)", e_ori_, [])
725 (case seek_orits ctxt sel ts ori of
726 ("", ori_ as (_,_,_,d,ts), all) =>
727 (case test_types ctxt (d,ts) of
728 "" => ("", ori_, all)
729 | msg => (msg, e_ori_, []))
730 | (msg,_,_) => (msg, e_ori_, []))
732 if member op = (map #4 ori) d
733 then seek_oridts ctxt sel (d,ts) ori
734 else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
737 (*. for return-value of appl_add .*)
740 | Err of string; (*error-message*)
743 (** add an item to the model; check wrt. oris and pbt **)
744 (* in contrary to oris<>[] below, this part handles user-input
745 extremely acceptive, i.e. accept input instead error-msg *)
746 fun appl_add ctxt sel [] ppc pbt ct =
748 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
750 case parseNEW ctxt ct of
751 NONE => Add (i, [], false, sel, Syn ct)
753 let val (d, ts) = split_dts t;
756 then Add (i, [], false, sel, Mis (dsc_unknown, hd ts))
758 (case find_first (eq1 d) pbt of
759 NONE => Add (i, [], true, sel, Sup (d,ts))
760 | SOME (f, (_, id)) =>
761 let fun eq2 d (i, _, _, _, itm_) =
762 d = (d_in itm_) andalso i <> 0;
763 in case find_first (eq2 d) ppc of
764 NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
765 | SOME (i', _, _, _, itm_) =>
769 val in_itm = ts_in itm_;
770 val ts' = union op = ts in_itm;
771 val i'' = if in_itm = [] then i else i';
772 in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts'))) end
773 else Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
777 | appl_add ctxt sel oris ppc pbt str =
778 case parseNEW ctxt str of
779 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
781 case is_known ctxt sel oris t of
783 (case is_notyet_input ctxt ppc all ori' pbt of
785 | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
786 | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
789 (** make oris from args of the stac SubProblem and from pbt **)
790 (* can this formal argument (of a model-pattern) be omitted in the arg-list
791 of a SubProblem ? see calcelems.sml 'type met ' *)
792 fun is_copy_named_idstr str =
793 case (rev o Symbol.explode) str of
794 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
795 "is_copy_named_idstr: " ^ str ^ " T"); true)
796 | _ => (tracing ((strs2str o (rev o Symbol.explode))
797 "is_copy_named_idstr: " ^ str ^ " F"); false);
798 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
800 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
801 fun is_copy_named_generating_idstr str =
802 if is_copy_named_idstr str
803 then case (rev o Symbol.explode) str of
804 "'"::"'"::"'"::_ => false
807 fun is_copy_named_generating (_, (_, t)) =
808 (is_copy_named_generating_idstr o free2str) t;
810 (*.split type-wrapper from scr-arg and build part of an ori;
811 an type-error is reported immediately, raises an exn,
812 subsequent handling of exn provides 2nd part of error message.*)
813 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
814 (* val (thy, (str, (dsc, _)), (ty $ var)) =
817 (Thm.global_cterm_of thy (dsc $ var);(*type check*)
818 SOME ((([1], str, dsc, (*[var]*)
819 split_dts' (dsc, var))): preori)(*:ori without leading #*))
820 handle e as TYPE _ =>
821 (tracing (dashs 70 ^ "\n"
822 ^"*** ERROR while creating the items for the model of the ->problem\n"
823 ^"*** from the ->stac with ->typeconstructor in arglist:\n"
824 ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
825 ^"*** description: "^(term_detail2str dsc)
826 ^"*** value: "^(term_detail2str var)
827 ^"*** typeconstructor in script: "^(term_detail2str ty)
828 ^"*** checked by theory: "^(theory2str thy)^"\n"
830 (*OldGoals.print_exn e; raises exn again*)
831 writeln (PolyML.makestring e);
833 (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
836 (*.match each pat of the model-pattern with an actual argument;
837 precondition: copy-named vars are filtered out.*)
838 fun matc thy ([]:pat list) _ (oris:preori list) = oris
839 | matc thy pbt [] _ =
841 error ("actual arg(s) missing for '"^pats2str pbt
842 ^"' i.e. should be 'copy-named' by '*_._'"))
843 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
844 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
845 (thy, pbt', ags, []);
847 val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
848 (thy, pbt, ags, (oris @ [ori]));
850 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
851 else(*..del?*) let val opt = mtc thy p a;
853 (* val SOME ori = mtc thy p a;
855 SOME ori => matc thy pbt ags (oris @ [ori])
856 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
858 (* run subp-rooteq.sml until Init_Proof before ...
859 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
860 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
862 other vars as in mtc ..
863 > matc thy (drop_last pbt) ags [];
864 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
867 (* generate a new variable "x_i" name from a related given one "x"
868 by use of oris relating "v_i_" (is_copy_named!) to "v_"
869 e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
871 (* generate a new variable "x_i" name from a related given one "x"
872 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
873 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
874 but leave is_copy_named_generating as is, e.t. ss''' *)
875 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
876 (if is_copy_named_generating p
877 then (*WN051014 kept strange old code ...*)
878 let fun sel (_,_,d,ts) = comp_ts (d, ts)
879 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
880 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
881 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
882 val vals = map sel oris
883 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
884 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
885 else ([1], field, dsc, [t])
887 handle _ => error ("cpy_nam: for "^(term2str t));
889 (*.match the actual arguments of a SubProblem with a model-pattern
890 and create an ori list (in root-pbl created from formalization).
891 expects ags:pats = 1:1, while copy-named are filtered out of pats;
892 if no 1:1 the exn raised by matc/mtc and handled at call.
893 copy-named pats are appended in order to get them into the model-items.*)
894 fun match_ags thy (pbt:pat list) ags =
895 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
896 val pbt' = filter_out is_copy_named pbt;
897 val cy = filter is_copy_named pbt;
898 val oris' = matc thy pbt' ags [];
899 val cy' = map (cpy_nam pbt' oris') cy;
900 val ors = add_id (oris' @ cy');
901 (*appended in order to get ^^^^^ into the model-items*)
902 in (map flattup ors):ori list end;
904 (*.report part of the error-msg which is not available in match_args.*)
905 fun match_ags_msg pI stac ags =
906 let (*val s = !show_types
907 val _ = show_types:= true*)
908 val pats = (#ppc o get_pbt) pI
909 val msg = (dots 70^"\n"
910 ^"*** problem "^strs2str pI^" has the ...\n"
911 ^"*** model-pattern "^pats2str pats^"\n"
912 ^"*** stac '"^term2str stac^"' has the ...\n"
913 ^"*** arg-list "^terms2str ags^"\n"
915 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
916 (*val _ = show_types:= s*)
920 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
921 fun vars_of_pbl_ pbl_ =
922 let fun var_of_pbl_ (gfr,(dsc,t)) = t
923 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
924 fun vars_of_pbl_' pbl_ =
925 let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
926 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
928 fun overwrite_ppc thy itm ppc =
930 fun repl ppc' (_,_,_,_,itm_) [] =
931 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
933 | repl ppc' itm (p::ppc) =
934 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
935 else repl (ppc' @ [p]) itm ppc
936 in repl [] itm ppc end;
938 (*10.3.00: insert the already compiled itm into model;
939 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
942 fun insert_ppc thy itm ppc =
944 fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
945 | eq_untouched _ _ = false;
948 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
949 case seek_ppc (#1 itm) ppc of
950 (* val SOME xxx = seek_ppc (#1 itm) ppc;
952 SOME _ => (*itm updated in is_notyet_input WN.11.03*)
953 overwrite_ppc thy itm ppc
954 | NONE => (ppc @ [itm]));
955 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
957 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
958 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
960 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
961 (d_in itm_) = (d_in iitm_);
962 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
963 handles superfluous items carelessly*)
964 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
966 > gen_ins' eee (4,[1,3,5,7]);
967 val it = [1, 3, 5, 7, 4] : int list*)
970 (*. output the headline to a ppc .*)
971 fun header p_ pI mI =
972 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
974 | pos => error ("header called with "^ pos_2str pos);
977 fun specify_additem sel (ct,_) (p, Met) c pt =
979 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
980 probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
981 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
982 val cpI = if pI = e_pblID then pI' else pI;
983 val cmI = if mI = e_metID then mI' else mI;
984 val {ppc,pre,prls,...} = get_met cmI;
986 case appl_add ctxt sel oris met ppc ct of
987 Add itm (*..union old input *) =>
989 val met' = insert_ppc thy itm met;
990 val ((p, Met), _, _, pt') =
991 generate1 thy (case sel of
992 "#Given" => Add_Given' (ct, met')
993 | "#Find" => Add_Find' (ct, met')
994 | "#Relate"=> Add_Relation'(ct, met'))
995 (Uistate, ctxt) (p, Met) pt
996 val pre' = check_preconds thy prls pre met'
997 val pb = foldl and_ (true, map fst pre')
999 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1000 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1001 in ((p, p_), ((p, p_), Uistate),
1002 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1003 (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
1007 val pre' = check_preconds thy prls pre met
1008 val pb = foldl and_ (true, map fst pre')
1010 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1011 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1012 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1015 | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt =
1017 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1018 probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1019 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1020 val cpI = if pI = e_pblID then pI' else pI;
1021 val cmI = if mI = e_metID then mI' else mI;
1022 val {ppc,where_,prls,...} = get_pbt cpI;
1024 case appl_add ctxt sel oris pbl ppc ct of
1025 Add itm (*..union old input *) =>
1027 val pbl' = insert_ppc thy itm pbl
1028 val ((p, Pbl), _, _, pt') =
1029 generate1 thy (case sel of
1030 "#Given" => Add_Given' (ct, pbl')
1031 | "#Find" => Add_Find' (ct, pbl')
1032 | "#Relate"=> Add_Relation'(ct, pbl'))
1033 (Uistate, ctxt) (p,Pbl) pt
1034 val pre = check_preconds thy prls where_ pbl'
1035 val pb = foldl and_ (true, map fst pre)
1037 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1038 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1039 val ppc = if p_= Pbl then pbl' else met;
1040 in ((p,p_), ((p,p_),Uistate),
1041 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1042 (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt,Safe,pt')
1046 val pre = check_preconds thy prls where_ pbl
1047 val pb = foldl and_ (true, map fst pre)
1049 nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1050 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1051 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1054 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1055 let (* either """"""""""""""" all empty or complete *)
1056 val thy = assoc_thy dI';
1058 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
1060 else pI' |> #ppc o get_pbt |> prep_ori fmz thy
1061 val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1062 (oris, (dI',pI',mI'), e_term)
1063 val pt = update_ctxt pt [] ctxt
1064 val {ppc, prls, where_, ...} = get_pbt pI'
1065 val (pbl, pre, pb) = ([], [], false)
1069 (([], Pbl), (([], Pbl), Uistate),
1070 Form' (PpcKF (0, EdUndef, (length []), Nundef,
1071 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1072 Refine_Tacitly pI', Safe, pt)
1074 (([], Pbl), (([], Pbl), Uistate),
1075 Form' (PpcKF (0, EdUndef, (length []), Nundef,
1076 (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1077 Model_Problem, Safe, pt)
1080 (*ONLY for STARTING modeling phase*)
1081 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1083 val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_), ctxt, ...}) = get_obj I pt p
1084 val thy' = if dI = e_domID then dI' else dI
1085 val thy = assoc_thy thy'
1086 val {ppc,prls,where_,...} = get_pbt pI'
1087 val pre = check_preconds thy prls where_ pbl
1088 val pb = foldl and_ (true, map fst pre)
1089 val ((p,_),_,_,pt) =
1090 generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1091 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1092 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1093 in ((p, Pbl), ((p, p_), Uistate),
1094 Form' (PpcKF (0, EdUndef, length p, Nundef,
1095 (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1099 (*. called only if no_met is specified .*)
1100 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1102 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ctxt, ...}) = get_obj I pt p;
1103 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1104 val (domID, metID) =
1105 (string_of_thy thy, if length met = 0 then e_metID else hd met)
1106 val ((p,_),_,_,pt) =
1107 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1108 (Uistate, ctxt) pos pt
1109 val (pbl, pre, pb) = ([], [], false)
1110 in ((p, Pbl), (pos, Uistate),
1111 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1112 (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1113 Model_Problem, Safe, pt)
1116 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1118 val ctxt = get_ctxt pt pos
1120 generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1121 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1122 Model_Problem, Safe, pt)
1124 (*WN110515 initialise ctxt again from itms and add preconds*)
1125 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1127 val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1128 meth=met, ctxt, ...}) = get_obj I pt p;
1129 val thy = assoc_thy dI
1130 val ((p,Pbl),_,_,pt)=
1131 generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt
1132 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1133 val mI'' = if mI=e_metID then mI' else mI;
1135 nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1136 ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1137 in ((p,Pbl), (pos,Uistate),
1138 Form' (PpcKF (0,EdUndef,(length p),Nundef, (Problem pI, itms2itemppc dI'' itms pre))),
1141 (*WN110515 initialise ctxt again from itms and add preconds*)
1142 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1144 val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1145 meth=met, ctxt, ...}) = get_obj I pt p;
1146 val {ppc,pre,prls,...} = get_met mID
1147 val thy = assoc_thy dI
1148 val oris = add_field' thy ppc oris;
1149 val dI'' = if dI=e_domID then dI' else dI;
1150 val pI'' = if pI = e_pblID then pI' else pI;
1151 val met = if met=[] then pbl else met;
1152 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1153 val (pos, _, _, pt) =
1154 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1156 nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1157 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1158 in (pos, (pos,Uistate),
1159 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1160 (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1164 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1165 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1166 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1168 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1170 val p_ = case p_ of Met => Met | _ => Pbl
1171 val thy = assoc_thy domID;
1172 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1173 probl=pbl, spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1174 val mppc = case p_ of Met => met | _ => pbl;
1175 val cpI = if pI = e_pblID then pI' else pI;
1176 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1177 val cmI = if mI = e_metID then mI' else mI;
1178 val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1181 Met => (check_preconds thy mer mwh met)
1182 | _ => (check_preconds thy per pwh pbl)
1183 val pb = foldl and_ (true, map fst pre)
1187 let val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1188 (pbl,met) (ppc,mpc) (dI,pI,mI);
1189 in ((p,p_), (pos,Uistate),
1190 Form'(PpcKF (0,EdUndef,(length p), Nundef,
1191 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1194 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1196 val ((p,p_),_,_,pt) =
1197 generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1199 nxt_spec p_ pb oris (dI',pI',mI') (pbl,met) (ppc,mpc) (domID,pI,mI);
1200 in ((p,p_), (pos,Uistate),
1201 Form' (PpcKF (0, EdUndef, (length p),Nundef,
1202 (header p_ pI cmI, itms2itemppc thy mppc pre))),
1207 | specify m' _ _ _ =
1208 error ("specify: not impl. for " ^ tac_2str m');
1210 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
1211 -- for input from scratch*)
1212 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1214 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1215 probl=pbl,spec=(dI,pI,_), ctxt, ...}) = get_obj I pt p;
1216 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1217 val cpI = if pI = e_pblID then pI' else pI;
1219 case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
1220 Add itm (*..union old input *) =>
1222 (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1223 val pbl' = insert_ppc thy itm pbl
1226 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1227 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1228 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1229 val ((p,Pbl),c,_,pt') =
1230 generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt
1231 in ([(tac,tac_,((p,Pbl),(Uistate, ctxt)))], c, (pt',(p,Pbl))):calcstate'
1233 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1234 FIXME ..and dont abuse a tactic for that purpose*)
1235 ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1236 (e_pos', (e_istate, e_ctxt)))], [], ptp)
1239 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1241 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1242 probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1243 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1244 val cmI = if mI = e_metID then mI' else mI;
1246 case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
1247 Add itm (*..union old input *) =>
1249 val met' = insert_ppc thy itm met;
1252 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1253 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1254 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1255 val ((p,Met),c,_,pt') =
1256 generate1 thy tac_ (Uistate, ctxt) (p,Met) pt
1257 in ([(tac,tac_,((p,Met), (Uistate, ctxt)))], c, (pt',(p,Met))) end
1258 | Err msg => ([(*tacis*)], [], ptp)
1259 (*nxt_me collects tacis until not hide; here just no progress*)
1262 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1263 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1264 handle _ => error ("ori2Coritm: dsc "^
1266 "in ori, but not in pbt")
1268 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1269 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1270 (find_first (eq1 d))) pbt,ts))):itm)
1271 handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1272 ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1275 (*filter out oris which have same description in itms*)
1276 fun filter_outs oris [] = oris
1277 | filter_outs oris (i::itms) =
1278 let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1279 (#4:ori -> term)) oris;
1280 in filter_outs ors itms end;
1282 fun memI a b = member op = a b;
1283 (*filter oris which are in pbt, too*)
1284 fun filter_pbt oris pbt =
1285 let val dscs = map (fst o snd) pbt
1286 in filter ((memI dscs) o (#4: ori -> term)) oris end;
1288 (*.combine itms from pbl + met and complete them wrt. pbt.*)
1289 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1291 fun x mem [] = false
1292 | x mem (y :: ys) = x = y orelse x mem ys;
1294 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1295 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1297 let val vat = max_vt pits;
1299 (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1300 val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1301 val os = filter_outs ors itms;
1302 (*WN.12.03?: does _NOT_ add itms from met ?!*)
1303 in itms @ (map (ori2Coritm met) os) end
1308 (*.complete model and guard of a calc-head .*)
1310 fun x mem [] = false
1311 | x mem (y :: ys) = x = y orelse x mem ys;
1313 fun complete_mod_ (oris, mpc, ppc, probl) =
1314 let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1315 val vat = if probl = [] then 1 else max_vt probl
1316 val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1317 val pors = filter_outs pors pits (*which are in pbl already*)
1318 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1320 val pits = pits @ (map (ori2Coritm ppc) pors)
1321 val mits = complete_metitms oris pits [] mpc
1325 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1326 (if dI = e_domID then odI else dI,
1327 if pI = e_pblID then opI else pI,
1328 if mI = e_metID then omI else mI):spec;
1331 (*.find a next applicable tac (for calcstate) and update ptree
1332 (for ev. finding several more tacs due to hide).*)
1333 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1334 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1335 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1336 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1338 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p
1339 val (dI, pI, mI) = some_spec ospec spec
1340 val thy = assoc_thy dI
1341 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1342 val {cas, ppc, ...} = get_pbt pI
1343 val pbl = init_pbl ppc (* fill in descriptions *)
1344 (*----------------if you think, this should be done by the Dialog
1345 in the java front-end, search there for WN060225-modelProblem----*)
1347 case cas of NONE => (pbl, [])
1348 | _ => complete_mod_ (oris, mpc, ppc, probl)
1349 (*----------------------------------------------------------------*)
1350 val tac_ = Model_Problem' (pI, pbl, met)
1351 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, ctxt) pos pt
1352 in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1354 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1355 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1356 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1358 (*. called only if no_met is specified .*)
1359 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1361 val (PblObj {origin = (oris, (dI,_,_),_), ctxt, ...}) = get_obj I pt p
1362 val opt = refine_ori oris pI
1367 val {met,ppc,...} = get_pbt pI'
1368 val pbl = init_pbl ppc
1369 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1370 val mI = if length met = 0 then e_metID else hd met
1371 val thy = assoc_thy dI
1373 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1374 (Uistate, ctxt) pos pt
1375 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1376 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1378 | NONE => ([], [], ptp)
1381 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1383 val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), probl, ctxt, ...}) = get_obj I pt p
1384 val thy = if dI' = e_domID then dI else dI'
1386 case refine_pbl (assoc_thy thy) pI probl of
1387 NONE => ([], [], ptp)
1388 | SOME (rfd as (pI',_)) =>
1390 val (pos,c,_,pt) = generate1 (assoc_thy thy)
1391 (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1392 in ([(Refine_Problem pI, Refine_Problem' rfd,
1393 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1397 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1399 val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...}) = get_obj I pt p;
1400 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1401 val {ppc,where_,prls,...} = get_pbt pI
1402 val pbl as (_,(itms,_)) =
1403 if pI'=e_pblID andalso pI=e_pblID
1404 then (false, (init_pbl ppc, []))
1405 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1406 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1407 val ((p,Pbl),c,_,pt) =
1408 generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt
1409 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1410 (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1413 (*transfers oris (not required in pbl) to met-model for script-env
1414 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1415 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1417 val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1418 meth=met, ctxt, ...}) = get_obj I pt p;
1419 val {ppc,pre,prls,...} = get_met mID
1420 val thy = assoc_thy dI
1421 val oris = add_field' thy ppc oris;
1422 val dI'' = if dI=e_domID then dI' else dI;
1423 val pI'' = if pI = e_pblID then pI' else pI;
1424 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1425 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1427 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1428 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1429 (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1432 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1434 val ctxt = get_ctxt pt pos
1435 val (dI',_,_) = get_obj g_spec pt p
1437 generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1438 in (*FIXXXME: check if pbl can still be parsed*)
1439 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
1443 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1445 val ctxt = get_ctxt pt pos
1446 val (dI',_,_) = get_obj g_spec pt p
1448 generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1449 in (*FIXXXME: check if met can still be parsed*)
1450 ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
1455 error ("nxt_specif: not impl. for "^tac2str m');
1457 (* get the values from oris; handle the term list w.r.t. penv *)
1459 fun x mem [] = false
1460 | x mem (y :: ys) = x = y orelse x mem ys;
1462 fun vals_of_oris oris =
1463 ((map (mkval' o (#5:ori -> term list))) o
1464 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1467 (* create a calc-tree with oris via an cas.refined pbl *)
1468 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1470 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1472 val {cas, met, ppc, thy, ...} = get_pbt pI
1473 val dI = if dI = "" then theory2theory' thy else dI
1474 val thy = assoc_thy dI
1475 val mI = if mI = [] then hd met else mI
1476 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1477 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1478 ([], (dI,pI,mI), hdl)
1479 val pt = update_spec pt [] (dI,pI,mI)
1480 val pits = init_pbl' ppc
1481 val pt = update_pbl pt [] pits
1482 in ((pt, ([] ,Pbl)), []) : calcstate end
1485 then (* from met-browser *)
1487 val {ppc,...} = get_met mI
1488 val dI = if dI = "" then "Isac" else dI
1489 val thy = assoc_thy dI;
1490 val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1491 ([], (dI,pI,mI), e_term(*FIXME met*));
1492 val pt = update_spec pt [] (dI,pI,mI);
1493 val mits = init_pbl' ppc;
1494 val pt = update_met pt [] mits;
1495 in ((pt, ([], Met)), []) : calcstate end
1496 else (* new example, pepare for interactive modeling *)
1497 let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1498 ([], e_spec, e_term)
1499 in ((pt, ([], Pbl)), []) : calcstate end
1501 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1502 let (* both """"""""""""""""""""""""" either empty or complete *)
1503 val thy = assoc_thy dI
1504 val (pI, (pors, pctxt), mI) =
1508 val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
1509 val pI' = refine_ori' pors pI;
1510 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1511 (hd o #met o get_pbt) pI') end
1512 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
1513 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1514 val dI = theory2theory' (maxthy thy thy')
1517 NONE => pblterm dI pI
1518 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
1519 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
1520 (pors, (dI, pI, mI), hdl)
1521 val pt = update_ctxt pt [] pctxt
1522 in ((pt, ([], Pbl)),
1523 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1529 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1530 (* case appl_spec p pt m of /// 19.1.00
1531 Notappl e => Error' (Error_ e)
1533 *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1537 (*fun tag_form thy (formal, given) = Thm.global_cterm_of thy
1538 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819*)
1539 fun tag_form thy (formal, given) =
1541 val gf = (head_of given) $ formal;
1542 val _ = Thm.global_cterm_of thy gf
1544 handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
1545 " .. " ^ term_to_string''' thy formal ^ " ..types do not match");
1546 (* val formal = (the o (parse thy)) "[R::real]";
1547 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1548 > tag_form thy (formal, given);
1549 val it = "fixed_values [R]" : cterm
1552 fun chktyp thy (n, fs, gs) =
1553 ((writeln o (term_to_string''' thy) o (nth n)) fs;
1554 (writeln o (term_to_string''' thy) o (nth n)) gs;
1555 tag_form thy (nth n fs, nth n gs));
1556 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1558 (* #####################################################
1559 find the failing item:
1561 > val tag__form = chktyp (n,formals,givens);
1562 > (type_of o Thm.term_of o (nth n)) formals;
1563 > (type_of o Thm.term_of o (nth n)) givens;
1564 > atomty ((Thm.term_of o (nth n)) formals);
1565 > atomty ((Thm.term_of o (nth n)) givens);
1566 > atomty (Thm.term_of tag__form);
1567 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1568 ##################################################### *)
1570 (* #####################################################
1572 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1573 val formals = map (the o (parse thy)) origin;
1575 val given = ["equation (lhs=rhs)",
1576 "bound_variable bdv", (* TODO type *)
1578 val where_ = ["e is_root_equation_in bdv",
1580 "apx is_const_expr"];
1581 val find = ["L::rat set"];
1582 val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1583 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1584 val givens = map (the o (parse thy)) given;
1586 val tag__forms = chktyps (formals, givens);
1587 map ((atomty) o Thm.term_of) tag__forms;
1588 ##################################################### *)
1591 (* check pbltypes, announces one failure a time *)
1592 (*fun chk_vars ctppc =
1593 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1594 appc flat (mappc (vars o Thm.term_of) ctppc)
1595 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1596 else if (re\\(gi union fi)) <> []
1597 then ("re\\(gi union fi)",re\\(gi union fi))
1598 else ("ok",[]) end;*)
1599 fun chk_vars ctppc =
1600 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1601 appc flat (mappc vars ctppc)
1602 val chked = subtract op = gi wh
1603 in if chked <> [] then ("wh\\gi", chked)
1604 else let val chked = subtract op = (union op = gi fi) re
1606 then ("re\\(gi union fi)", chked)
1611 (* check a new pbltype: variables (Free) unbound by given, find*)
1612 fun unbound_ppc ctppc =
1613 let val {Given=gi,Find=fi,Relate=re,...} =
1614 appc flat (mappc vars ctppc)
1615 in distinct (*re\\(gi union fi)*)
1616 (subtract op = (union op = gi fi) re) end;
1618 > val org = {Given=["[R=(R::real)]"],Where=[],
1619 Find=["[A::real]"],With=[],
1620 Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1622 > val ctppc = mappc (the o (parse thy)) org;
1623 > unbound_ppc ctppc;
1624 val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1628 (* f, a binary operator, is nested rightassociative *)
1631 fun fld f (x::[]) = x
1632 | fld f (x::x'::[]) = f (x',x)
1633 | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1634 in ((fld f) o rev) xs end;
1636 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1637 > val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
1638 > val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
1639 > Thm.global_cterm_of thy conj;
1640 val it = "(a = b & c = d) & e = f" : cterm
1643 (* f, a binary operator, is nested leftassociative *)
1644 fun foldl1 f (x::[]) = x
1645 | foldl1 f (x::x'::[]) = f (x,x')
1646 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1648 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1649 > val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
1650 > val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
1651 > Thm.global_cterm_of thy conj;
1652 val it = "a = b & c = d & e = f & g = h" : cterm
1656 (* called only once, if a Subproblem has been located in the script*)
1657 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_,_)) ptp =
1660 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1661 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1662 (*all stored in tac_ itms^^^^^^^^^^*)
1663 | nxt_model_pbl tac_ _ =
1664 error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_);
1666 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1667 fun eq4 v (_,vts,_,_,_) = member op = vts v;
1668 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1671 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1672 + met from fmz; assumes pos on PblObj, meth = [].*)
1673 fun complete_mod (pt, pos as (p, p_):pos') =
1674 (* val (pt, (p, _)) = (pt, p);
1675 val (pt, (p, _)) = (pt, pos);
1677 let val _= if p_ <> Pbl
1678 then tracing("###complete_mod: only impl.for Pbl, called with "^
1679 pos'2str pos) else ()
1680 val (PblObj{origin=(oris, ospec, hdl), probl, spec, ...}) =
1682 val (dI,pI,mI) = some_spec ospec spec
1683 val mpc = (#ppc o get_met) mI
1684 val ppc = (#ppc o get_pbt) pI
1685 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1686 val pt = update_pblppc pt p pits
1687 val pt = update_metppc pt p mits
1688 in (pt, (p,Met):pos') end
1690 (*| complete_mod (pt, pos as (p, Met):pos') =
1691 error ("###complete_mod: only impl.for Pbl, called with "^
1694 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1695 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1696 fun all_modspec (pt, (p,_):pos') =
1698 val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
1699 val thy = assoc_thy dI;
1700 val {ppc, ...} = get_met mI;
1701 val (fmz_, vals) = oris2fmz_vals pors;
1702 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
1703 |> declare_constraints' vals
1704 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1705 val pt = update_metppc pt p (map (ori2Coritm ppc) pors); (*WN110716 = _pblppc ?!?*)
1706 val pt = update_spec pt p (dI,pI,mI);
1707 val pt = update_ctxt pt p ctxt
1709 val mors = prep_ori fmz_ thy ppc |> #1;
1710 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1711 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1712 (*WN110715: why pors, mors handled so differently?*)
1713 val pt = update_spec pt p (dI,pI,mI);
1715 in (pt, (p,Met): pos') end;
1717 (*WN0312: use in nxt_spec, too ? what about variants ???*)
1718 fun is_complete_mod_ ([]: itm list) = false
1719 | is_complete_mod_ itms =
1720 foldl and_ (true, (map #3 itms));
1722 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1723 if (is_pblobj o (get_obj I pt)) p
1724 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1725 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1726 | is_complete_mod (pt, pos as (p, Met)) =
1727 if (is_pblobj o (get_obj I pt)) p
1728 then (is_complete_mod_ o (get_obj g_met pt)) p
1729 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1730 | is_complete_mod (_, pos) =
1731 error ("is_complete_mod called by " ^ pos'2str pos ^
1732 " (should be Pbl or Met)");
1734 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1735 fun is_complete_spec (pt, pos as (p,_): pos') =
1736 if (not o is_pblobj o (get_obj I pt)) p
1737 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1738 else let val (dI,pI,mI) = get_obj g_spec pt p
1739 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1740 (*.complete empty items in specification from origin (pbl, met ev.refined);
1741 assumes 'is_complete_mod'.*)
1742 fun complete_spec (pt, pos as (p,_): pos') =
1743 let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1744 val pt = update_spec pt p (some_spec ospec spec)
1747 fun is_complete_modspec ptp =
1748 is_complete_mod ptp andalso is_complete_spec ptp;
1753 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1754 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1756 let val (_,_,metID) = get_somespec' spec spec'
1758 if metID = e_metID then []
1759 else let val {prls,pre=where_,...} = get_met metID
1760 val pre = check_preconds' prls where_ meth 0
1762 val allcorrect = is_complete_mod_ meth
1763 andalso foldl and_ (true, (map #1 pre))
1764 in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1765 | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1766 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1768 let val (_,pI,_) = get_somespec' spec spec'
1770 if pI = e_pblID then []
1771 else let val {prls,where_,cas,...} = get_pbt pI
1772 val pre = check_preconds' prls where_ probl 0
1774 val allcorrect = is_complete_mod_ probl
1775 andalso foldl and_ (true, (map #1 pre))
1776 in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1779 fun pt_form (PrfObj {form,...}) = Form form
1780 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1781 let val (dI, pI, _) = get_somespec' spec spec'
1782 val {cas,...} = get_pbt pI
1784 NONE => Form (pblterm dI pI)
1785 | SOME t => Form (subst_atomic (mk_env probl) t)
1787 (*vvv takes the tac _generating_ the formula=result, asm ok....
1788 fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1790 if null asm then NONE else SOME asm,
1792 | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1793 let val (_,_,metID) = some_spec ospec spec
1795 if null asm then NONE else SOME asm,
1796 if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1797 -------------------------------------------------------------------------*)
1800 (*.pt_extract returns
1801 # the formula at pos
1802 # the tactic applied to this formula
1803 # the list of assumptions generated at this formula
1804 (by application of another tac to the preceding formula !)
1805 pos is assumed to come from the frontend, ie. generated by moveDown.*)
1806 (*cannot be in ctree.sml, because ModSpec has to be calculated*)
1807 fun pt_extract (pt,([],Res)) = (* WN120512: --returns--> Check_Postcondition WRONGLY
1808 see --- build fun is_exactly_equal*)
1809 (* ML_TODO 110417 get assumptions from ctxt !? *)
1810 let val (f, asm) = get_obj g_result pt []
1811 in (Form f, NONE, asm) end
1812 | pt_extract (pt,(p,Res)) =
1814 val (f, asm) = get_obj g_result pt p
1818 if is_pblobj' pt (lev_up p)
1821 val (PblObj{spec=(_,pI,_),...}) = get_obj I pt (lev_up p)
1822 in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
1823 else SOME End_Trans (*WN0502 TODO for other branches*)
1825 let val p' = lev_on p
1829 let val (PblObj{origin = (_,(dI,pI,_),_),...}) = get_obj I pt p'
1830 in SOME (Subproblem (dI, pI)) end
1832 if f = get_obj g_form pt p'
1833 then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
1834 else SOME (Take (term2str (get_obj g_form pt p')))
1836 in (Form f, tac, asm) end
1837 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1839 val ppobj = get_obj I pt p
1840 val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
1841 val tac = g_tac ppobj
1842 in (f, SOME tac, []) end;
1845 (**. get the formula from a ctree-node:
1846 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1847 take res from all other PrfObj's .**)
1848 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1849 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1850 [("headline", (p, Frm), h),
1851 ("stepform", (p, Res), r)]
1852 | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1853 [("stepform", (p, Frm), form),
1854 ("stepform", (p, Res), r)];
1856 fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1857 [("stepform", (p, Res), r)]
1859 (*assumes to take whole level, in particular hd -- for use in interSteps*)
1860 fun get_formress fs p [] = flat fs
1861 | get_formress fs p (nd::nds) =
1862 (* start with 'form+res' and continue with trying 'res' only*)
1863 get_forms (fs @ [formres p nd]) (lev_on p) nds
1864 and get_forms fs p [] = flat fs
1865 | get_forms fs p (nd::nds) =
1867 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1868 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1869 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1870 (* continue with trying 'res' only*)
1871 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1873 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1874 (*WN050219 made robust against _'to' below or after Complete nodes
1875 by handling exn caused by move_dn*)
1876 (*WN0401 this functionality belongs to ctree.sml,
1877 but fetching a calc_head requires calculations defined in modspec.sml
1878 transfer to ME/me.sml !!!
1879 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1880 is returned !!!!!!!!!!!!!
1882 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1883 | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1884 | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1888 | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1892 | eq_pos' _ _ = false;
1894 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the
1895 total ordering Position#compareTo(Position p) in the java-code
1896 val get_interval = fn
1897 : pos' -> : from is "move_up 1st-element" to return
1898 pos' -> : to the last element to be returned; from < to
1899 int -> : level: 0 gets the flattest sub-tree possible
1900 >999 gets the deepest sub-tree possible
1902 (pos' * : of the formula
1903 Term.term) : the formula
1906 fun get_interval from to level pt =
1908 fun get_inter c (from:pos') (to:pos') lev pt =
1909 if eq_pos' from to orelse from = ([],Res)
1910 (*orelse ... avoids Exception- PTREE "end of calculation" raised,
1911 if 'to' has values NOT generated by move_dn, see systest/me.sml
1912 TODO.WN0501: introduce an order on pos' and check "from > to"..
1913 ...there is an order in Java!
1914 WN051224 the hack got worse with returning term instead ptform*)
1916 let val (f,_,_) = pt_extract (pt, from)
1919 ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
1920 | Form t => c @ [(from, t)]
1923 if lev < lev_of from
1924 then (get_inter c (move_dn [] pt from) to lev pt)
1925 handle (PTREE _(*from move_dn too far*)) => c
1928 val (f,_,_) = pt_extract (pt, from)
1929 val term = case f of
1930 ModSpec (_,_,headline,_,_,_) => headline
1932 in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)
1933 handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]
1935 in get_inter [] from to level pt end;
1938 fun posform2str (pos:pos', form) =
1939 "("^ pos'2str pos ^", "^
1941 Form f => term2str f
1942 | ModSpec c => term2str (#3 c(*the headline*)))
1944 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
1945 (map posform2str)) pfs;
1946 fun posterm2str (pos:pos', t) =
1947 "("^ pos'2str pos ^", "^term2str t^")";
1948 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
1949 (map posterm2str)) pfs;
1952 (*WN050225 omits the last step, if pt is incomplete*)
1954 tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
1956 (*.get a calchead from a PblObj-node in the ctree;
1957 preconditions must be calculated.*)
1958 fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
1959 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
1961 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
1962 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
1963 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
1964 | get_ocalhd (pt, pos' as (p,Met):pos') =
1965 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1968 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
1969 val pre = check_preconds (assoc_thy"Isac") prls pre meth
1970 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
1972 (*.at the activeFormula set the Model, the Guard and the Specification
1973 to empty and return a CalcHead;
1974 the 'origin' remains (for reconstructing all that).*)
1975 fun reset_calchead (pt, pos' as (p,_):pos') =
1976 let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
1977 val pt = update_pbl pt p []
1978 val pt = update_met pt p []
1979 val pt = update_spec pt p e_spec
1980 in (pt, (p,Pbl):pos') end;