neuper@37906
|
1 |
(* Types and tools for 'modeling' und 'specifying' to be used in
|
neuper@37906
|
2 |
modspec.sml. The types are separated from calchead.sml into this file,
|
neuper@37906
|
3 |
because some of them are stored in the calc-tree, and thus are required
|
neuper@37906
|
4 |
_before_ ctree.sml.
|
neuper@37906
|
5 |
author: Walther Neuper
|
neuper@37906
|
6 |
(c) due to copyright terms
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
use"ME/mstools.sml" (*re-evaluate sml/ from scratch!*);
|
neuper@37906
|
9 |
use"mstools.sml";
|
neuper@37924
|
10 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890
|
neuper@37924
|
11 |
10 20 30 40 50 60 70 80
|
neuper@37906
|
12 |
*)
|
neuper@37906
|
13 |
|
neuper@37906
|
14 |
signature SPECIFY_TOOLS =
|
neuper@37906
|
15 |
sig
|
neuper@37906
|
16 |
type envv
|
neuper@37906
|
17 |
datatype
|
neuper@37906
|
18 |
item =
|
neuper@37906
|
19 |
Correct of cterm'
|
neuper@37906
|
20 |
| False of cterm'
|
neuper@37906
|
21 |
| Incompl of cterm'
|
neuper@37906
|
22 |
| Missing of cterm'
|
neuper@37906
|
23 |
| Superfl of string
|
neuper@37906
|
24 |
| SyntaxE of string
|
neuper@37906
|
25 |
| TypeE of string
|
neuper@37906
|
26 |
val item2str : item -> string
|
neuper@37906
|
27 |
type itm
|
neuper@37924
|
28 |
val itm2str_ : Proof.context -> itm -> string
|
neuper@37906
|
29 |
datatype
|
neuper@37906
|
30 |
itm_ =
|
neuper@37924
|
31 |
Cor of (term * term list) * (term * term list)
|
neuper@37924
|
32 |
| Inc of (term * term list) * (term * term list)
|
neuper@37924
|
33 |
| Mis of term * term
|
neuper@37906
|
34 |
| Par of cterm'
|
neuper@37924
|
35 |
| Sup of term * term list
|
neuper@37906
|
36 |
| Syn of cterm'
|
neuper@37906
|
37 |
| Typ of cterm'
|
neuper@37906
|
38 |
val itm_2str : itm_ -> string
|
neuper@37924
|
39 |
val itm_2str_ : Proof.context -> itm_ -> string
|
neuper@37924
|
40 |
val itms2str_ : Proof.context -> itm list -> string
|
neuper@37906
|
41 |
type 'a ppc
|
neuper@37906
|
42 |
val ppc2str :
|
neuper@37906
|
43 |
{Find: string list, With: string list, Given: string list,
|
neuper@37906
|
44 |
Where: string list, Relate: string list} -> string
|
neuper@37906
|
45 |
datatype
|
neuper@37906
|
46 |
match =
|
neuper@37906
|
47 |
Matches of pblID * item ppc
|
neuper@37906
|
48 |
| NoMatch of pblID * item ppc
|
neuper@37906
|
49 |
val match2str : match -> string
|
neuper@37906
|
50 |
datatype
|
neuper@37906
|
51 |
match_ =
|
neuper@37924
|
52 |
Match_ of pblID * (itm list * (bool * term) list)
|
neuper@37906
|
53 |
| NoMatch_
|
neuper@37906
|
54 |
val matchs2str : match list -> string
|
neuper@37906
|
55 |
type ori
|
neuper@37906
|
56 |
val ori2str : ori -> string
|
neuper@37906
|
57 |
val oris2str : ori list -> string
|
neuper@37906
|
58 |
type preori
|
neuper@37906
|
59 |
val preori2str : preori -> string
|
neuper@37906
|
60 |
val preoris2str : preori list -> string
|
neuper@37906
|
61 |
type penv
|
neuper@37924
|
62 |
(* val penv2str_ : Proof.context -> penv -> string *)
|
neuper@37906
|
63 |
type vats
|
neuper@37906
|
64 |
(*----------------------------------------------------------------------*)
|
neuper@37924
|
65 |
val all_ts_in : itm_ list -> term list
|
neuper@37906
|
66 |
val check_preconds :
|
neuper@37906
|
67 |
'a ->
|
neuper@37906
|
68 |
rls ->
|
neuper@37924
|
69 |
term list -> itm list -> (bool * term) list
|
neuper@37906
|
70 |
val check_preconds' :
|
neuper@37906
|
71 |
rls ->
|
neuper@37924
|
72 |
term list ->
|
neuper@37924
|
73 |
itm list -> 'a -> (bool * term) list
|
neuper@37924
|
74 |
(* val chkpre2item : rls -> term -> bool * item *)
|
neuper@37924
|
75 |
val pres2str : (bool * term) list -> string
|
neuper@37924
|
76 |
(* val evalprecond : rls -> term -> bool * term *)
|
neuper@37906
|
77 |
(* val cnt : itm list -> int -> int * int *)
|
neuper@37924
|
78 |
val comp_dts : theory -> term * term list -> term
|
neuper@37924
|
79 |
val comp_dts' : term * term list -> term
|
neuper@37924
|
80 |
val comp_dts'' : term * term list -> string
|
neuper@37924
|
81 |
val comp_ts : term * term list -> term
|
neuper@37924
|
82 |
val d_in : itm_ -> term
|
neuper@37906
|
83 |
val de_item : item -> cterm'
|
neuper@37924
|
84 |
val dest_list : term * term list -> term list (* for testing *)
|
neuper@37924
|
85 |
val dest_list' : term -> term list
|
neuper@37924
|
86 |
val dts2str : term * term list -> string
|
neuper@37906
|
87 |
val e_itm : itm
|
neuper@37924
|
88 |
(* val e_listBool : term *)
|
neuper@37924
|
89 |
(* val e_listReal : term *)
|
neuper@37906
|
90 |
val e_ori : ori
|
neuper@37906
|
91 |
val e_ori_ : ori
|
neuper@37906
|
92 |
val empty_ppc : item ppc
|
neuper@37906
|
93 |
(* val empty_ppc_ct' : cterm' ppc *)
|
neuper@37924
|
94 |
(* val getval : term * term list -> term * term *)
|
neuper@37906
|
95 |
(*val head_precond :
|
neuper@37906
|
96 |
domID * pblID * 'a ->
|
neuper@37924
|
97 |
term option ->
|
neuper@37906
|
98 |
rls ->
|
neuper@37924
|
99 |
term list ->
|
neuper@37924
|
100 |
itm list -> 'b -> term * (bool * term) list*)
|
neuper@37906
|
101 |
(* val init_item : string -> item *)
|
neuper@37906
|
102 |
(* val is_matches : match -> bool *)
|
neuper@37906
|
103 |
(* val is_matches_ : match_ -> bool *)
|
neuper@37924
|
104 |
val is_var : term -> bool
|
neuper@37906
|
105 |
(* val item_ppc :
|
neuper@37906
|
106 |
string ppc -> item ppc *)
|
neuper@37906
|
107 |
val itemppc2str : item ppc -> string
|
neuper@37906
|
108 |
(* val matches_pblID : match -> pblID *)
|
neuper@37906
|
109 |
val max2 : ('a * int) list -> 'a * int
|
neuper@37906
|
110 |
val max_vt : itm list -> int
|
neuper@37924
|
111 |
val mk_e : itm_ -> (term * term) list
|
neuper@37924
|
112 |
val mk_en : int -> itm -> (term * term) list
|
neuper@37924
|
113 |
val mk_env : itm list -> (term * term) list
|
neuper@37924
|
114 |
val mkval : 'a -> term list -> term
|
neuper@37924
|
115 |
val mkval' : term list -> term
|
neuper@37906
|
116 |
(* val pblID_of_match : match -> pblID *)
|
neuper@37924
|
117 |
val pbl_ids : Proof.context -> term -> term -> term list
|
neuper@37924
|
118 |
val pbl_ids' : 'a -> term -> term list -> term list
|
neuper@37924
|
119 |
(* val pen2str : theory -> term * term list -> string *)
|
neuper@37924
|
120 |
val penvval_in : itm_ -> term list
|
neuper@37906
|
121 |
val refined : match list -> pblID
|
neuper@37906
|
122 |
val refined_ :
|
neuper@37924
|
123 |
match_ list -> match_ option
|
neuper@37906
|
124 |
(* val refined_IDitms :
|
neuper@37924
|
125 |
match list -> match option *)
|
neuper@37924
|
126 |
val split_dts : 'a -> term -> term * term list
|
neuper@37924
|
127 |
val split_dts' : term * term -> term list
|
neuper@37924
|
128 |
(* val take_apart : term -> term list *)
|
neuper@37924
|
129 |
(* val take_apart_inv : term list -> term *)
|
neuper@37924
|
130 |
val ts_in : itm_ -> term list
|
neuper@37924
|
131 |
(* val unique : term *)
|
neuper@37906
|
132 |
val untouched : itm list -> bool
|
neuper@37906
|
133 |
val upd :
|
neuper@37924
|
134 |
Proof.context ->
|
neuper@37924
|
135 |
(''a * (''b * term list) list) list ->
|
neuper@37924
|
136 |
term ->
|
neuper@37924
|
137 |
''b * term -> ''a -> ''a * (''b * term list) list
|
neuper@37906
|
138 |
val upd_envv :
|
neuper@37924
|
139 |
Proof.context ->
|
neuper@37906
|
140 |
envv ->
|
neuper@37906
|
141 |
vats ->
|
neuper@37924
|
142 |
term -> term -> term -> envv
|
neuper@37906
|
143 |
val upd_penv :
|
neuper@37924
|
144 |
Proof.context ->
|
neuper@37924
|
145 |
(''a * term list) list ->
|
neuper@37924
|
146 |
term -> ''a * term -> (''a * term list) list
|
neuper@37906
|
147 |
(* val upds_envv :
|
neuper@37924
|
148 |
Proof.context ->
|
neuper@37906
|
149 |
envv ->
|
neuper@37924
|
150 |
(vats * term * term * term) list ->
|
neuper@37906
|
151 |
envv *)
|
neuper@37906
|
152 |
val vts_cnt : int list -> itm list -> (int * int) list
|
neuper@37906
|
153 |
val vts_in : itm list -> int list
|
neuper@37924
|
154 |
(* val w_itms2str_ : Proof.context -> itm list -> unit *)
|
neuper@37906
|
155 |
end
|
neuper@37906
|
156 |
|
neuper@37906
|
157 |
(*----------------------------------------------------------*)
|
neuper@37906
|
158 |
structure SpecifyTools : SPECIFY_TOOLS =
|
neuper@37906
|
159 |
struct
|
neuper@37906
|
160 |
(*----------------------------------------------------------*)
|
neuper@37924
|
161 |
val e_listReal = (term_of o the o (parse (theory "Script"))) "[]::(real list)";
|
neuper@37924
|
162 |
val e_listBool = (term_of o the o (parse (theory "Script"))) "[]::(bool list)";
|
neuper@37906
|
163 |
|
neuper@37906
|
164 |
(*.take list-term apart w.r.t. handling elementwise input.*)
|
neuper@37906
|
165 |
fun take_apart t =
|
neuper@37906
|
166 |
let val elems = isalist2list t
|
neuper@37906
|
167 |
in map ((list2isalist (type_of (hd elems))) o single) elems end;
|
neuper@37906
|
168 |
(*val t = str2term "[a, b]";
|
neuper@37906
|
169 |
> val ts = take_apart t; writeln (terms2str ts);
|
neuper@37906
|
170 |
["[a]","[b]"]
|
neuper@37906
|
171 |
|
neuper@37906
|
172 |
> t = (take_apart_inv o take_apart) t;
|
neuper@37906
|
173 |
true*)
|
neuper@37906
|
174 |
fun take_apart_inv ts =
|
neuper@37906
|
175 |
let val elems = (flat o (map isalist2list)) ts;
|
neuper@37906
|
176 |
in list2isalist (type_of (hd elems)) elems end;
|
neuper@37906
|
177 |
(*val ts = [str2term "[a]", str2term "[b]"];
|
neuper@37906
|
178 |
> val t = take_apart_inv ts; term2str t;
|
neuper@37906
|
179 |
"[a, b]"
|
neuper@37906
|
180 |
|
neuper@37906
|
181 |
ts = (take_apart o take_apart_inv) ts;
|
neuper@37906
|
182 |
true*)
|
neuper@37906
|
183 |
|
neuper@37906
|
184 |
|
neuper@37906
|
185 |
|
neuper@37906
|
186 |
|
neuper@37906
|
187 |
(*.revert split_dts only for ts; compare comp_dts.*)
|
neuper@37906
|
188 |
fun comp_ts (d, ts) =
|
neuper@37906
|
189 |
if is_list_dsc d
|
neuper@37906
|
190 |
then if is_list (hd ts)
|
neuper@37906
|
191 |
then if is_unl d
|
neuper@37906
|
192 |
then (hd ts) (*e.g. someList [1,3,2]*)
|
neuper@37906
|
193 |
else (take_apart_inv ts)
|
neuper@37906
|
194 |
(* SML[ [a], [b] ]SML --> [a,b] *)
|
neuper@37906
|
195 |
else (hd ts) (*a variable or metavariable for a list*)
|
neuper@37906
|
196 |
else (hd ts);
|
neuper@37906
|
197 |
(*.revert split_.
|
neuper@37906
|
198 |
WN050903 we do NOT know which is from subtheory, description or term;
|
neuper@37906
|
199 |
typecheck thus may lead to TYPE-error 'unknown constant';
|
neuper@37906
|
200 |
solution: typecheck with Isac.thy; i.e. arg 'thy' superfluous*)
|
neuper@37924
|
201 |
(*fun comp_dts thy (d,[]) =
|
neuper@37924
|
202 |
cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
|
neuper@37924
|
203 |
(theory "Isac")
|
neuper@37906
|
204 |
(*comp_dts:FIXXME stay with term for efficiency !!!*)
|
neuper@37906
|
205 |
(if is_reall_dsc d then (d $ e_listReal)
|
neuper@37906
|
206 |
else if is_booll_dsc d then (d $ e_listBool)
|
neuper@37906
|
207 |
else d)
|
neuper@37906
|
208 |
| comp_dts thy (d,ts) =
|
neuper@37924
|
209 |
(cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
|
neuper@37924
|
210 |
(theory "Isac")
|
neuper@37906
|
211 |
(*comp_dts:FIXXME stay with term for efficiency !!*)
|
neuper@37906
|
212 |
(d $ (comp_ts (d, ts)))
|
neuper@37906
|
213 |
handle _ => raise error ("comp_dts: "^(term2str d)^
|
neuper@37924
|
214 |
" $ "^(term2str (hd ts))));*)
|
neuper@37924
|
215 |
fun comp_dts thy (d,[]) =
|
neuper@37924
|
216 |
(if is_reall_dsc d then (d $ e_listReal)
|
neuper@37924
|
217 |
else if is_booll_dsc d then (d $ e_listBool)
|
neuper@37924
|
218 |
else d)
|
neuper@37924
|
219 |
| comp_dts thy (d,ts) =
|
neuper@37924
|
220 |
(d $ (comp_ts (d, ts)))
|
neuper@37924
|
221 |
handle _ => raise error ("comp_dts: "^(term2str d)^
|
neuper@37924
|
222 |
" $ "^(term2str (hd ts)));
|
neuper@37906
|
223 |
(*25.8.03*)
|
neuper@37906
|
224 |
fun comp_dts' (d,[]) =
|
neuper@37906
|
225 |
if is_reall_dsc d then (d $ e_listReal)
|
neuper@37906
|
226 |
else if is_booll_dsc d then (d $ e_listBool)
|
neuper@37906
|
227 |
else d
|
neuper@37906
|
228 |
| comp_dts' (d,ts) = (d $ (comp_ts (d, ts)))
|
neuper@37906
|
229 |
handle _ => raise error ("comp_dts': "^(term2str d)^
|
neuper@37906
|
230 |
" $ "^(term2str (hd ts)));
|
neuper@37906
|
231 |
(*val t = str2term "maximum A";
|
neuper@37906
|
232 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
233 |
val it = "maximum A" : cterm
|
neuper@37906
|
234 |
> val t = str2term "fixedValues [r=Arbfix]";
|
neuper@37906
|
235 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
236 |
"fixedValues [r = Arbfix]"
|
neuper@37906
|
237 |
> val t = str2term "valuesFor [a]";
|
neuper@37906
|
238 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
239 |
"valuesFor [a]"
|
neuper@37906
|
240 |
> val t = str2term "valuesFor [a,b]";
|
neuper@37906
|
241 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
242 |
"valuesFor [a, b]"
|
neuper@37906
|
243 |
> val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
|
neuper@37906
|
244 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
245 |
relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"
|
neuper@37906
|
246 |
> val t = str2term "boundVariable a";
|
neuper@37906
|
247 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
248 |
"boundVariable a"
|
neuper@37906
|
249 |
> val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
|
neuper@37906
|
250 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
251 |
"interval {x. 0 <= x & x <= 2 * r}"
|
neuper@37906
|
252 |
|
neuper@37906
|
253 |
> val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
|
neuper@37906
|
254 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
255 |
"equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
|
neuper@37906
|
256 |
> val t = str2term "solveFor x";
|
neuper@37906
|
257 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
258 |
"solveFor x"
|
neuper@37906
|
259 |
> val t = str2term "errorBound (eps=0)";
|
neuper@37906
|
260 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
261 |
"errorBound (eps = 0)"
|
neuper@37906
|
262 |
> val t = str2term "solutions L";
|
neuper@37906
|
263 |
> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
|
neuper@37906
|
264 |
"solutions L"
|
neuper@37906
|
265 |
|
neuper@37906
|
266 |
before 6.5.03:
|
neuper@37906
|
267 |
> val t = (term_of o the o (parse thy)) "testdscforlist [#1]";
|
neuper@37906
|
268 |
> val (d,ts) = split_dts t;
|
neuper@37906
|
269 |
> comp_dts thy (d,ts);
|
neuper@37906
|
270 |
val it = "testdscforlist [#1]" : cterm
|
neuper@37906
|
271 |
|
neuper@37906
|
272 |
> val t = (term_of o the o (parse thy)) "(A::real)";
|
neuper@37906
|
273 |
> val (d,ts) = split_dts t;
|
neuper@37906
|
274 |
val d = Const ("empty","empty") : term
|
neuper@37906
|
275 |
val ts = [Free ("A","RealDef.real")] : term list
|
neuper@37906
|
276 |
> val t = (term_of o the o (parse thy)) "[R=(R::real)]";
|
neuper@37906
|
277 |
> val (d,ts) = split_dts t;
|
neuper@37906
|
278 |
val d = Const ("empty","empty") : term
|
neuper@37906
|
279 |
val ts = [Const # $ Free # $ Free (#,#)] : term list
|
neuper@37906
|
280 |
> val t = (term_of o the o (parse thy)) "[#1,#2]";
|
neuper@37906
|
281 |
> val (d,ts) = split_dts t;
|
neuper@37906
|
282 |
val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
|
neuper@37906
|
283 |
*)
|
neuper@37906
|
284 |
|
neuper@37906
|
285 |
(*for input_icalhd 11.03*)
|
neuper@37906
|
286 |
fun comp_dts'' (d,[]) =
|
neuper@37906
|
287 |
if is_reall_dsc d then term2str (d $ e_listReal)
|
neuper@37906
|
288 |
else if is_booll_dsc d then term2str (d $ e_listBool)
|
neuper@37906
|
289 |
else term2str d
|
neuper@37906
|
290 |
| comp_dts'' (d,ts) = term2str (d $ (comp_ts (d, ts)))
|
neuper@37906
|
291 |
handle _ => raise error ("comp_dts'': "^(term2str d)^
|
neuper@37906
|
292 |
" $ "^(term2str (hd ts)));
|
neuper@37906
|
293 |
|
neuper@37906
|
294 |
|
neuper@37906
|
295 |
|
neuper@37906
|
296 |
|
neuper@37906
|
297 |
|
neuper@37906
|
298 |
|
neuper@37906
|
299 |
(* this may decompose an object-language isa-list;
|
neuper@37906
|
300 |
use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)
|
neuper@37906
|
301 |
fun dest_list' t = if is_list t then isalist2list t else [t];
|
neuper@37906
|
302 |
|
neuper@37906
|
303 |
(*fun is_metavar (Free (str, _)) =
|
neuper@37906
|
304 |
if (last_elem o explode) str = "_" then true else false
|
neuper@37906
|
305 |
| is_metavar _ = false;*)
|
neuper@37906
|
306 |
fun is_var (Free _) = true
|
neuper@37906
|
307 |
| is_var _ = false;
|
neuper@37906
|
308 |
|
neuper@37906
|
309 |
(*.special handling for lists. ?WN:14.5.03 ??!?*)
|
neuper@37906
|
310 |
fun dest_list (d,ts) =
|
neuper@37906
|
311 |
let fun dest t =
|
neuper@37906
|
312 |
if is_list_dsc d andalso not (is_unl d)
|
neuper@37906
|
313 |
andalso not (is_var t) (*..for pbt*)
|
neuper@37906
|
314 |
then isalist2list t else [t]
|
neuper@37906
|
315 |
in (flat o (map dest)) ts end;
|
neuper@37906
|
316 |
|
neuper@37906
|
317 |
|
neuper@37906
|
318 |
(*.decompose an input into description, terms (ev. elems of lists),
|
neuper@37906
|
319 |
and the value for the problem-environment; inv to comp_dts .*)
|
neuper@37906
|
320 |
(*WN.8.6.03: corrected with minimal effort,
|
neuper@37906
|
321 |
fn : theory -> term ->
|
neuper@37906
|
322 |
term * description
|
neuper@37906
|
323 |
term list * lists decomposed for elementwise input
|
neuper@37906
|
324 |
term list pbl_ids not _HERE_: dont know which list-elems input*)
|
neuper@37906
|
325 |
fun split_dts thy (t as d $ arg) =
|
neuper@37906
|
326 |
if is_dsc d
|
neuper@37906
|
327 |
then if is_list_dsc d
|
neuper@37906
|
328 |
then if is_list arg
|
neuper@37906
|
329 |
then if is_unl d
|
neuper@37906
|
330 |
then (d, [arg]) (*e.g. someList [1,3,2]*)
|
neuper@37906
|
331 |
else (d, take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)
|
neuper@37906
|
332 |
else (d, [arg]) (*a variable or metavariable for a list*)
|
neuper@37906
|
333 |
else (d, [arg])
|
neuper@37906
|
334 |
else (e_term, dest_list' t(*9.01 ???*))
|
neuper@37906
|
335 |
| split_dts thy t = (*either dsc or term*)
|
neuper@37906
|
336 |
let val (h,argl) = strip_comb t
|
neuper@37906
|
337 |
in if (not o is_dsc) h then (e_term, dest_list' t)
|
neuper@37906
|
338 |
else (h, dest_list (h,argl))
|
neuper@37906
|
339 |
end;
|
neuper@37906
|
340 |
(* tests see fun comp_dts
|
neuper@37906
|
341 |
|
neuper@37906
|
342 |
> val t = str2term "someList []";
|
neuper@37906
|
343 |
> val (_,ts) = split_dts thy t; writeln (terms2str ts);
|
neuper@37906
|
344 |
["[]"]
|
neuper@37906
|
345 |
> val t = str2term "valuesFor []";
|
neuper@37906
|
346 |
> val (_,ts) = split_dts thy t; writeln (terms2str ts);
|
neuper@37906
|
347 |
["[]"]*)
|
neuper@37906
|
348 |
|
neuper@37906
|
349 |
(*.version returning ts only.*)
|
neuper@37906
|
350 |
fun split_dts' (d, arg) =
|
neuper@37906
|
351 |
if is_dsc d
|
neuper@37906
|
352 |
then if is_list_dsc d
|
neuper@37906
|
353 |
then if is_list arg
|
neuper@37906
|
354 |
then if is_unl d
|
neuper@37906
|
355 |
then ([arg]) (*e.g. someList [1,3,2]*)
|
neuper@37906
|
356 |
else (take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)
|
neuper@37906
|
357 |
else ([arg]) (*a variable or metavariable for a list*)
|
neuper@37906
|
358 |
else ([arg])
|
neuper@37906
|
359 |
else (dest_list' arg(*9.01 ???*))
|
neuper@37906
|
360 |
| split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
|
neuper@37906
|
361 |
let val (h,argl) = strip_comb t
|
neuper@37906
|
362 |
in if (not o is_dsc) h then (dest_list' t)
|
neuper@37906
|
363 |
else (dest_list (h,argl))
|
neuper@37906
|
364 |
end;
|
neuper@37906
|
365 |
|
neuper@37906
|
366 |
|
neuper@37906
|
367 |
|
neuper@37906
|
368 |
|
neuper@37906
|
369 |
|
neuper@37906
|
370 |
(*27.8.01: problem-environment
|
neuper@37906
|
371 |
WN.6.5.03: FIXXME reconsider if penv is worth the effort --
|
neuper@37906
|
372 |
-- just rerun a whole expl with num/var may show the same ?!
|
neuper@37906
|
373 |
WN.9.5.03: penv-concept stalled, immediately generate script env !
|
neuper@37906
|
374 |
but [#0, epsilon] only outcommented for eventual reconsideration
|
neuper@37906
|
375 |
*)
|
neuper@37906
|
376 |
type penv = (term (*err_*)
|
neuper@37906
|
377 |
* (term list) (*[#0, epsilon] 9.5.03 outcommented*)
|
neuper@37906
|
378 |
) list;
|
neuper@37924
|
379 |
fun pen2str ctxt (t, ts) =
|
neuper@37924
|
380 |
pair2str(Syntax.string_of_term ctxt t,
|
neuper@37924
|
381 |
(strs2str' o map (Syntax.string_of_term ctxt)) ts);
|
neuper@37924
|
382 |
fun penv2str_ thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv;
|
neuper@37906
|
383 |
|
neuper@37906
|
384 |
(*
|
neuper@37906
|
385 |
9.5.03: still unused, but left for eventual future development*)
|
neuper@37906
|
386 |
type envv = (int * penv) list; (*over variants*)
|
neuper@37906
|
387 |
|
neuper@37906
|
388 |
(*. 14.9.01: not used after putting penv-values into itm_
|
neuper@37906
|
389 |
make the result of split_* a value of problem-environment .*)
|
neuper@37906
|
390 |
fun mkval dsc [] = raise error "mkval called with []"
|
neuper@37906
|
391 |
| mkval dsc [t] = t
|
neuper@37906
|
392 |
| mkval dsc ts = list2isalist ((type_of o hd) ts) ts;
|
neuper@37906
|
393 |
(*WN.12.12.03*)
|
neuper@37906
|
394 |
fun mkval' x = mkval e_term x;
|
neuper@37906
|
395 |
|
neuper@37906
|
396 |
|
neuper@37906
|
397 |
|
neuper@37906
|
398 |
(*. get the constant value from a penv .*)
|
neuper@37906
|
399 |
fun getval (id, values) =
|
neuper@37906
|
400 |
case values of
|
neuper@37906
|
401 |
[] => raise error ("penv_value: no values in '"^
|
neuper@37924
|
402 |
(Syntax.string_of_term (thy2ctxt "Tools") id))
|
neuper@37906
|
403 |
| [v] => (id, v)
|
neuper@37906
|
404 |
| (v1::v2::_) => (case v1 of
|
neuper@37906
|
405 |
Const ("Script.Arbfix",_) => (id, v2)
|
neuper@37906
|
406 |
| _ => (id, v1));
|
neuper@37906
|
407 |
(*
|
neuper@37906
|
408 |
val e_ = (term_of o the o (parse thy)) "e_::bool";
|
neuper@37906
|
409 |
val ev = (term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0";
|
neuper@37906
|
410 |
val v_ = (term_of o the o (parse thy)) "v_";
|
neuper@37906
|
411 |
val vv = (term_of o the o (parse thy)) "x";
|
neuper@37906
|
412 |
val r_ = (term_of o the o (parse thy)) "err_::bool";
|
neuper@37906
|
413 |
val rv1 = (term_of o the o (parse thy)) "#0";
|
neuper@37906
|
414 |
val rv2 = (term_of o the o (parse thy)) "eps";
|
neuper@37906
|
415 |
|
neuper@37906
|
416 |
val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv;
|
neuper@37906
|
417 |
map getval penv;
|
neuper@37906
|
418 |
[(Free ("e_","bool"),
|
neuper@37906
|
419 |
Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#0","RealDef.real")),
|
neuper@37906
|
420 |
(Free ("v_","RealDef.real"),Free ("x","RealDef.real")),
|
neuper@37906
|
421 |
(Free ("err_","bool"),Free ("#0","RealDef.real"))] : (term * term) list
|
neuper@37906
|
422 |
*)
|
neuper@37906
|
423 |
|
neuper@37906
|
424 |
|
neuper@37906
|
425 |
(*23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc
|
neuper@37906
|
426 |
(1) kinds of itms:
|
neuper@37906
|
427 |
(1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
|
neuper@37906
|
428 |
=(presently) Mis (? should be Inc initially, and Mis after match_itms?)
|
neuper@37906
|
429 |
(1.2) Syn,Typ,Sup: not related to oris
|
neuper@37906
|
430 |
Syn, Typ (presently) should be accepted in appl_add (instead Error')
|
neuper@37906
|
431 |
Sup (presently) should be accepted in appl_add (instead Error')
|
neuper@37906
|
432 |
_could_ be w.r.t current vat (and then _is_ related to vat
|
neuper@37906
|
433 |
Mis should _not_ be made Inc ((presently, by appl_add & match_itms)
|
neuper@37906
|
434 |
- dsc in itm_ is timeconsuming -- keep id for respective queries ?
|
neuper@37906
|
435 |
- order of items in ppc should be stable w.r.t order of itms
|
neuper@37906
|
436 |
|
neuper@37906
|
437 |
- stepwise input of itms --- match_itms (in one go) ..not coordinated
|
neuper@37906
|
438 |
- unify code
|
neuper@37906
|
439 |
- match_itms / match_itms_oris ..2 versions ?!
|
neuper@37906
|
440 |
(fast, for refine / slow, for modeling)
|
neuper@37906
|
441 |
|
neuper@37906
|
442 |
- clarify: efficiency <--> simplicity !!!
|
neuper@37906
|
443 |
?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc
|
neuper@37906
|
444 |
| take int for perserving order of item ppc in itms
|
neuper@37906
|
445 |
| make all(!?) handling of itms stable against reordering(?)
|
neuper@37906
|
446 |
| field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)
|
neuper@37906
|
447 |
-"- "#undef" ?= not touched ?= (id,..)
|
neuper@37906
|
448 |
-----------------------------------------------------------------
|
neuper@37906
|
449 |
27.3.02:
|
neuper@37906
|
450 |
def: type pbt = (field, (dsc, pid))
|
neuper@37906
|
451 |
|
neuper@37906
|
452 |
(1) fmz + pbt -> oris
|
neuper@37906
|
453 |
(2) input + oris -> itm
|
neuper@37906
|
454 |
(3) match_itms : schnell(?) f"ur refine
|
neuper@37906
|
455 |
match_itms_oris : r"uckmeldung f"ur item ppc
|
neuper@37906
|
456 |
|
neuper@37906
|
457 |
(1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)
|
neuper@37906
|
458 |
---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!
|
neuper@37906
|
459 |
|
neuper@37906
|
460 |
(3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;
|
neuper@37906
|
461 |
wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:
|
neuper@37906
|
462 |
(a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid) dh.vt neu ????
|
neuper@37906
|
463 |
(b)
|
neuper@37906
|
464 |
*)
|
neuper@37906
|
465 |
|
neuper@37906
|
466 |
|
neuper@37906
|
467 |
|
neuper@37906
|
468 |
|
neuper@37906
|
469 |
(*the internal representation of a models' item
|
neuper@37906
|
470 |
|
neuper@37906
|
471 |
4.9.01: not consistent:
|
neuper@37906
|
472 |
after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
|
neuper@37906
|
473 |
(involves 'is_error');
|
neuper@37906
|
474 |
bool in itm really necessary ???*)
|
neuper@37906
|
475 |
datatype itm_ =
|
neuper@37906
|
476 |
Cor of (term * (* description *)
|
neuper@37906
|
477 |
(term list)) * (* for list: elem-wise input *)
|
neuper@37906
|
478 |
(*split_dts <-> comp_dts*)
|
neuper@37906
|
479 |
(term * (term list)) (* elem of penv *)
|
neuper@37906
|
480 |
(*9.5.03: ---- is already for script -- penv delayed to future*)
|
neuper@37906
|
481 |
| Syn of cterm'
|
neuper@37906
|
482 |
| Typ of cterm'
|
neuper@37906
|
483 |
| Inc of (term * (term list)) * (term * (term list)) (*lists,
|
neuper@37906
|
484 |
+ init_pbl WN.11.03 FIXXME: empty penv .. bad
|
neuper@37906
|
485 |
init_pbl should return Mis !!!*)
|
neuper@37906
|
486 |
| Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
|
neuper@37906
|
487 |
| Mis of (term * term) (* after re-specification pbt-item not found
|
neuper@37906
|
488 |
in pbl: only dsc, pid_*)
|
neuper@37906
|
489 |
| Par of cterm'; (*internal state from fun parsitm*)
|
neuper@37906
|
490 |
|
neuper@37906
|
491 |
type vats = int list; (*variants in formalizations*)
|
neuper@37906
|
492 |
|
neuper@37906
|
493 |
(*.data-type for working on pbl/met-ppc:
|
neuper@37906
|
494 |
in pbl initially holds descriptions (only) for user guidance.*)
|
neuper@37906
|
495 |
type itm =
|
neuper@37906
|
496 |
int * (* id =0 .. untouched - descript (only) from init
|
neuper@37906
|
497 |
23.3.02: seems to correspond to ori (fun insert_ppc)
|
neuper@37906
|
498 |
<> maintain order in item ppc?*)
|
neuper@37906
|
499 |
vats * (* variants - copy from ori *)
|
neuper@37906
|
500 |
bool * (* input on this item is not/complete *)
|
neuper@37906
|
501 |
string * (* #Given | #Find | #Relate *)
|
neuper@37906
|
502 |
itm_; (* *)
|
neuper@37906
|
503 |
(* use"ME/sequent.sml";
|
neuper@37906
|
504 |
*)
|
neuper@37906
|
505 |
val e_itm = (0,[],false,"e_itm",Syn"e_itm"):itm;
|
neuper@37906
|
506 |
(*in CalcTree/Subproblem an 'untouched' model is created
|
neuper@37906
|
507 |
FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
|
neuper@37906
|
508 |
fun untouched (itms: itm list) =
|
neuper@37906
|
509 |
foldl and_ (true ,map ((curry op= 0) o #1) itms);
|
neuper@37906
|
510 |
(*> untouched [];
|
neuper@37906
|
511 |
val it = true : bool
|
neuper@37906
|
512 |
> untouched [e_itm];
|
neuper@37906
|
513 |
val it = true : bool
|
neuper@37906
|
514 |
> untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")];
|
neuper@37906
|
515 |
val it = false : bool*)
|
neuper@37906
|
516 |
|
neuper@37906
|
517 |
|
neuper@37906
|
518 |
|
neuper@37906
|
519 |
|
neuper@37906
|
520 |
|
neuper@37906
|
521 |
(* find most frequent variant v in itms *)
|
neuper@37906
|
522 |
|
neuper@37906
|
523 |
fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
|
neuper@37906
|
524 |
|
neuper@37906
|
525 |
fun cnt itms v = (v,(length o (filter (curry op= v)) o
|
neuper@37906
|
526 |
flat o (map #2)) (itms:itm list));
|
neuper@37906
|
527 |
fun vts_cnt vts itms = map (cnt itms) vts;
|
neuper@37906
|
528 |
fun max2 [] = raise error "max2 of []"
|
neuper@37906
|
529 |
| max2 (y::ys) =
|
neuper@37906
|
530 |
let fun mx (a,x) [] = (a,x)
|
neuper@37906
|
531 |
| mx (a,x) ((b,y)::ys) =
|
neuper@37906
|
532 |
if x < y then mx (b,y) ys else mx (a,x) ys;
|
neuper@37906
|
533 |
in mx y ys end;
|
neuper@37906
|
534 |
|
neuper@37906
|
535 |
(*. find the variant with most items already input .*)
|
neuper@37906
|
536 |
fun max_vt itms =
|
neuper@37906
|
537 |
let val vts = (vts_cnt (vts_in itms)) itms;
|
neuper@37906
|
538 |
in if vts = [] then 0 else (fst o max2) vts end;
|
neuper@37906
|
539 |
|
neuper@37906
|
540 |
|
neuper@37906
|
541 |
(* TODO ev. make more efficient by avoiding flat *)
|
neuper@37906
|
542 |
fun mk_e (Cor (_, iv)) = [getval iv]
|
neuper@37906
|
543 |
| mk_e (Syn _) = []
|
neuper@37906
|
544 |
| mk_e (Typ _) = []
|
neuper@37906
|
545 |
| mk_e (Inc (_, iv)) = [getval iv]
|
neuper@37906
|
546 |
| mk_e (Sup _) = []
|
neuper@37906
|
547 |
| mk_e (Mis _) = [];
|
neuper@37906
|
548 |
fun mk_en vt ((i,vts,b,f,itm_):itm) =
|
neuper@37924
|
549 |
if member op = vts vt then mk_e itm_ else [];
|
neuper@37906
|
550 |
(*. extract the environment from an item list;
|
neuper@37906
|
551 |
takes the variant with most items .*)
|
neuper@37906
|
552 |
fun mk_env itms =
|
neuper@37906
|
553 |
let val vt = max_vt itms
|
neuper@37906
|
554 |
in (flat o (map (mk_en vt))) itms end;
|
neuper@37906
|
555 |
|
neuper@37906
|
556 |
|
neuper@37906
|
557 |
|
neuper@37906
|
558 |
(*. example as provided by an author, complete w.r.t. pbt specified
|
neuper@37906
|
559 |
not touched by any user action .*)
|
neuper@37906
|
560 |
type ori = (int * (* id: 10.3.00ff impl. only <>0 .. touched
|
neuper@37906
|
561 |
21.3.02: insert_ppc needs it ! ?:purpose maintain
|
neuper@37906
|
562 |
order in item ppc ???*)
|
neuper@37906
|
563 |
vats * (* variants 21.3.02: related to pbt..discard ?*)
|
neuper@37906
|
564 |
string * (* #Given | #Find | #Relate 21.3.02: discard ?*)
|
neuper@37906
|
565 |
term * (* description *)
|
neuper@37906
|
566 |
term list (* isalist2list t | [t] *)
|
neuper@37906
|
567 |
);
|
neuper@37906
|
568 |
val e_ori_ = (0,[],"",e_term,[e_term]):ori;
|
neuper@37906
|
569 |
val e_ori = (0,[],"",e_term,[e_term]):ori;
|
neuper@37906
|
570 |
|
neuper@37906
|
571 |
fun ori2str ((i,vs,fi,t,ts):ori) =
|
neuper@37906
|
572 |
"("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^
|
neuper@37906
|
573 |
(term2str t)^", "^((strs2str o (map term2str)) ts)^")";
|
neuper@37906
|
574 |
val oris2str =
|
neuper@37906
|
575 |
let val s = !show_types
|
neuper@37906
|
576 |
val _ = show_types:= true
|
neuper@37906
|
577 |
val str = (strs2str' o (map (linefeed o ori2str)))
|
neuper@37906
|
578 |
val _ = show_types:= s
|
neuper@37906
|
579 |
in str end;
|
neuper@37906
|
580 |
|
neuper@37906
|
581 |
(*.an or without leading integer.*)
|
neuper@37906
|
582 |
type preori = (vats *
|
neuper@37906
|
583 |
string *
|
neuper@37906
|
584 |
term *
|
neuper@37906
|
585 |
term list);
|
neuper@37906
|
586 |
fun preori2str ((vs,fi,t,ts):preori) =
|
neuper@37906
|
587 |
"("^((strs2str o (map string_of_int)) vs)^", "^fi^", "^
|
neuper@37906
|
588 |
(term2str t)^", "^((strs2str o (map term2str)) ts)^")";
|
neuper@37906
|
589 |
val preoris2str = (strs2str' o (map (linefeed o preori2str)));
|
neuper@37906
|
590 |
|
neuper@37906
|
591 |
(*. given the input value (from split_dts)
|
neuper@37906
|
592 |
make the value in a problem-env according to description-type .*)
|
neuper@37906
|
593 |
(*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
|
neuper@37924
|
594 |
fun pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v =
|
neuper@37906
|
595 |
if is_list v
|
neuper@37906
|
596 |
then [v] (*eg. [r=Arbfix]*)
|
neuper@37906
|
597 |
else (case v of (*eg. eps=#0*)
|
neuper@37906
|
598 |
(Const ("op =",_) $ l $ r) => [r,l]
|
neuper@37906
|
599 |
| _ => raise error ("pbl_ids Tools.nam: no equality "
|
neuper@37924
|
600 |
^(Syntax.string_of_term ctxt v)))
|
neuper@37924
|
601 |
| pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]
|
neuper@37924
|
602 |
| pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]
|
neuper@37924
|
603 |
| pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v]
|
neuper@37924
|
604 |
| pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v]
|
neuper@37924
|
605 |
| pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v]
|
neuper@37924
|
606 |
| pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v]
|
neuper@37924
|
607 |
| pbl_ids ctxt _ v = raise error ("pbl_ids: not implemented for "
|
neuper@37924
|
608 |
^(Syntax.string_of_term ctxt v));
|
neuper@37906
|
609 |
(*
|
neuper@37906
|
610 |
val t as t1 $ t2 = str2term "antiDerivativeName M_b";
|
neuper@37924
|
611 |
pbl_ids ctxt t1 t2;
|
neuper@37906
|
612 |
|
neuper@37906
|
613 |
val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
|
neuper@37906
|
614 |
val (d,argl) = strip_comb t;
|
neuper@37906
|
615 |
is_dsc d; (*see split_dts*)
|
neuper@37906
|
616 |
dest_list (d,argl);
|
neuper@37906
|
617 |
val (_ $ v) = t;
|
neuper@37906
|
618 |
is_list v;
|
neuper@37924
|
619 |
pbl_ids ctxt d v;
|
neuper@37906
|
620 |
[Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
|
neuper@37906
|
621 |
(Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
|
neuper@37906
|
622 |
|
neuper@37906
|
623 |
val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x";
|
neuper@37906
|
624 |
val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term
|
neuper@37906
|
625 |
val vl = Free ("x","RealDef.real") : term
|
neuper@37906
|
626 |
|
neuper@37906
|
627 |
val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
|
neuper@37924
|
628 |
pbl_ids ctxt dsc vl;
|
neuper@37906
|
629 |
val it = [Free ("x","RealDef.real")] : term list
|
neuper@37906
|
630 |
|
neuper@37906
|
631 |
val (dsc,vl) = (split_dts o term_of o the o(parse thy))
|
neuper@37906
|
632 |
"errorBound (eps=#0)";
|
neuper@37906
|
633 |
val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";
|
neuper@37924
|
634 |
pbl_ids ctxt dsc vl;
|
neuper@37906
|
635 |
val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *)
|
neuper@37906
|
636 |
|
neuper@37906
|
637 |
(*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
|
neuper@37906
|
638 |
make the value in a problem-env according to description-type .*)
|
neuper@37906
|
639 |
(*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
|
neuper@37906
|
640 |
fun pbl_ids' (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) vs =
|
neuper@37906
|
641 |
(case vs of
|
neuper@37906
|
642 |
[] => raise error ("pbl_ids' Tools.nam called with []")
|
neuper@37906
|
643 |
| [t] => (case t of (*eg. eps=#0*)
|
neuper@37906
|
644 |
(Const ("op =",_) $ l $ r) => [r,l]
|
neuper@37906
|
645 |
| _ => raise error ("pbl_ids' Tools.nam: no equality "
|
neuper@37924
|
646 |
^(Syntax.string_of_term (ctxt_Isac"")t)))
|
neuper@37906
|
647 |
| vs' => vs (*14.9.01: ???TODO *))
|
neuper@37906
|
648 |
| pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs
|
neuper@37906
|
649 |
| pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs
|
neuper@37906
|
650 |
| pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs
|
neuper@37906
|
651 |
| pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs
|
neuper@37906
|
652 |
| pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))vs = vs
|
neuper@37906
|
653 |
| pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))vs = vs
|
neuper@37906
|
654 |
| pbl_ids' _ vs =
|
neuper@37906
|
655 |
raise error ("pbl_ids': not implemented for "
|
neuper@37906
|
656 |
^(terms2str vs));
|
neuper@37906
|
657 |
(*9.5.03 penv postponed: pbl_ids'*)
|
neuper@37906
|
658 |
fun pbl_ids' thy d vs = [comp_ts (d, vs)];
|
neuper@37906
|
659 |
|
neuper@37906
|
660 |
|
neuper@37906
|
661 |
(*14.9.01: not used after putting values for penv into itm_
|
neuper@37906
|
662 |
WN.5.5.03: used in upd .. upd_envv*)
|
neuper@37924
|
663 |
fun upd_penv ctxt penv dsc (id, vl) =
|
neuper@37906
|
664 |
(writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
|
neuper@37906
|
665 |
writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
|
neuper@37906
|
666 |
writeln"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
|
neuper@37924
|
667 |
overwrite (penv, (id, pbl_ids ctxt dsc vl))
|
neuper@37906
|
668 |
);
|
neuper@37906
|
669 |
(*
|
neuper@37906
|
670 |
val penv = [];
|
neuper@37906
|
671 |
val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x";
|
neuper@37906
|
672 |
val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
|
neuper@37906
|
673 |
val penv = upd_penv thy penv dsc (id, vl);
|
neuper@37906
|
674 |
[(Free ("v_","RealDef.real"),
|
neuper@37906
|
675 |
[Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])]
|
neuper@37906
|
676 |
: (term * term list) list
|
neuper@37906
|
677 |
|
neuper@37906
|
678 |
val (dsc,vl) = (split_did o term_of o the o(parse thy))"errorBound (eps=#0)";
|
neuper@37906
|
679 |
val (dsc,id) = (split_did o term_of o the o(parse thy))"errorBound err_";
|
neuper@37906
|
680 |
upd_penv thy penv dsc (id, vl);
|
neuper@37906
|
681 |
[(Free ("v_","RealDef.real"),
|
neuper@37906
|
682 |
[Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]),
|
neuper@37906
|
683 |
(Free ("err_","bool"),
|
neuper@37906
|
684 |
[Free ("#0","RealDef.real"),Free ("eps","RealDef.real")])]
|
neuper@37906
|
685 |
: (term * term list) list ^.........!!!!
|
neuper@37906
|
686 |
*)
|
neuper@37906
|
687 |
|
neuper@37906
|
688 |
(*WN.9.5.03: not reconsidered; looks strange !!!*)
|
neuper@37906
|
689 |
fun upd thy envv dsc (id, vl) i =
|
neuper@37906
|
690 |
let val penv = case assoc (envv, i) of
|
neuper@37924
|
691 |
SOME e => e
|
neuper@37924
|
692 |
| NONE => [];
|
neuper@37906
|
693 |
val penv' = upd_penv thy penv dsc (id, vl);
|
neuper@37906
|
694 |
in (i, penv') end;
|
neuper@37906
|
695 |
(*
|
neuper@37906
|
696 |
val i = 2;
|
neuper@37906
|
697 |
val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
|
neuper@37906
|
698 |
val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";
|
neuper@37906
|
699 |
val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";
|
neuper@37906
|
700 |
upd thy envv dsc (id, vl) i;
|
neuper@37906
|
701 |
val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])
|
neuper@37906
|
702 |
: int * (term * term list) list*)
|
neuper@37906
|
703 |
|
neuper@37906
|
704 |
|
neuper@37906
|
705 |
(*14.9.01: not used after putting pre-penv into itm_*)
|
neuper@37906
|
706 |
fun upd_envv thy (envv:envv) (vats:vats) dsc id vl =
|
neuper@37906
|
707 |
let val vats = if length vats = 0
|
neuper@37906
|
708 |
then (*unknown id to _all_ variants*)
|
neuper@37906
|
709 |
if length envv = 0 then [1]
|
neuper@37906
|
710 |
else (intsto o length) envv
|
neuper@37906
|
711 |
else vats
|
neuper@37924
|
712 |
fun isin vats (i,_) = member op = vats i;
|
neuper@37906
|
713 |
val envs_notin_vat = filter_out (isin vats) envv;
|
neuper@37906
|
714 |
in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end;
|
neuper@37906
|
715 |
(*
|
neuper@37906
|
716 |
val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
|
neuper@37906
|
717 |
|
neuper@37906
|
718 |
val vats = [2]
|
neuper@37906
|
719 |
val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";
|
neuper@37906
|
720 |
val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";
|
neuper@37906
|
721 |
val envv = upd_envv thy envv vats dsc id vl;
|
neuper@37906
|
722 |
val envv = [(2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])]
|
neuper@37906
|
723 |
: (int * (term * term list) list) list
|
neuper@37906
|
724 |
|
neuper@37906
|
725 |
val vats = [1,2,3];
|
neuper@37906
|
726 |
val (dsc,vl) = (split_did o term_of o the o(parse thy))"maximum A";
|
neuper@37906
|
727 |
val (dsc,id) = (split_did o term_of o the o(parse thy))"maximum m_";
|
neuper@37906
|
728 |
upd_envv thy envv vats dsc id vl;
|
neuper@37906
|
729 |
[(1,[(Free ("m_","bool"),[Free ("A","bool")])]),
|
neuper@37906
|
730 |
(2,
|
neuper@37906
|
731 |
[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")]),
|
neuper@37906
|
732 |
(Free ("m_","bool"),[Free ("A","bool")])]),
|
neuper@37906
|
733 |
(3,[(Free ("m_","bool"),[Free ("A","bool")])])]
|
neuper@37906
|
734 |
: (int * (term * term list) list) list
|
neuper@37906
|
735 |
|
neuper@37906
|
736 |
|
neuper@37906
|
737 |
val env = []:envv;
|
neuper@37906
|
738 |
val (d,ts) = (split_dts o term_of o the o (parse thy))
|
neuper@37906
|
739 |
"fixedValues [r=Arbfix]";
|
neuper@37906
|
740 |
val (_,id) = (split_did o term_of o the o (parse thy))"fixedValues fix_";
|
neuper@37906
|
741 |
val vats = [1,2,3];
|
neuper@37906
|
742 |
val env = upd_envv thy env vats d id (mkval ts);
|
neuper@37906
|
743 |
*)
|
neuper@37906
|
744 |
|
neuper@37906
|
745 |
(*. update envv by folding from a list of arguments .*)
|
neuper@37906
|
746 |
fun upds_envv thy envv [] = envv
|
neuper@37906
|
747 |
| upds_envv thy envv ((vs, dsc, id, vl)::ps) =
|
neuper@37906
|
748 |
upds_envv thy (upd_envv thy envv vs dsc id vl) ps;
|
neuper@37906
|
749 |
(* eval test-maximum.sml until Specify_Method ...
|
neuper@37906
|
750 |
val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
|
neuper@37906
|
751 |
val met = (#ppc o get_met) mI;
|
neuper@37906
|
752 |
|
neuper@37906
|
753 |
val envv = [];
|
neuper@37906
|
754 |
val eargs = flat eargs;
|
neuper@37906
|
755 |
val (vs, dsc, id, vl) = hd eargs;
|
neuper@37906
|
756 |
val envv = upds_envv thy envv [(vs, dsc, id, vl)];
|
neuper@37906
|
757 |
|
neuper@37906
|
758 |
val (vs, dsc, id, vl) = hd (tl eargs);
|
neuper@37906
|
759 |
val envv = upds_envv thy envv [(vs, dsc, id, vl)];
|
neuper@37906
|
760 |
|
neuper@37906
|
761 |
val (vs, dsc, id, vl) = hd (tl (tl eargs));
|
neuper@37906
|
762 |
val envv = upds_envv thy envv [(vs, dsc, id, vl)];
|
neuper@37906
|
763 |
|
neuper@37906
|
764 |
val (vs, dsc, id, vl) = hd (tl (tl (tl eargs)));
|
neuper@37906
|
765 |
val envv = upds_envv thy envv [(vs, dsc, id, vl)];
|
neuper@37906
|
766 |
[(1,
|
neuper@37906
|
767 |
[(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
|
neuper@37906
|
768 |
(Free ("m_","bool"),[Free (#,#)]),
|
neuper@37906
|
769 |
(Free ("vs_","bool List.list"),[# $ # $ Const #]),
|
neuper@37906
|
770 |
(Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
|
neuper@37906
|
771 |
(2,
|
neuper@37906
|
772 |
[(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
|
neuper@37906
|
773 |
(Free ("m_","bool"),[Free (#,#)]),
|
neuper@37906
|
774 |
(Free ("vs_","bool List.list"),[# $ # $ Const #]),
|
neuper@37906
|
775 |
(Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
|
neuper@37906
|
776 |
(3,
|
neuper@37906
|
777 |
[(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
|
neuper@37906
|
778 |
(Free ("m_","bool"),[Free (#,#)]),
|
neuper@37906
|
779 |
(Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *)
|
neuper@37906
|
780 |
|
neuper@37906
|
781 |
(*for _output_ of the items of a Model*)
|
neuper@37906
|
782 |
datatype item =
|
neuper@37906
|
783 |
Correct of cterm' (*labels a correct formula (type cterm')*)
|
neuper@37906
|
784 |
| SyntaxE of string (**)
|
neuper@37906
|
785 |
| TypeE of string (**)
|
neuper@37906
|
786 |
| False of cterm' (*WN050618 notexistent in itm_: only used in Where*)
|
neuper@37906
|
787 |
| Incompl of cterm' (**)
|
neuper@37906
|
788 |
| Superfl of string (**)
|
neuper@37906
|
789 |
| Missing of cterm';
|
neuper@37924
|
790 |
fun item2str (Correct s) ="Correct " ^ s
|
neuper@37924
|
791 |
| item2str (SyntaxE s) ="SyntaxE " ^ s
|
neuper@37924
|
792 |
| item2str (TypeE s) ="TypeE " ^ s
|
neuper@37924
|
793 |
| item2str (False s) ="False " ^ s
|
neuper@37924
|
794 |
| item2str (Incompl s) ="Incompl " ^ s
|
neuper@37924
|
795 |
| item2str (Superfl s) ="Superfl " ^ s
|
neuper@37924
|
796 |
| item2str (Missing s) ="Missing " ^ s;
|
neuper@37906
|
797 |
(*make string for error-msgs*)
|
neuper@37924
|
798 |
fun itm_2str_ ctxt (Cor ((d,ts), penv)) =
|
neuper@37924
|
799 |
"Cor " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ,"
|
neuper@37924
|
800 |
^ pen2str ctxt penv
|
neuper@37924
|
801 |
| itm_2str_ ctxt (Syn c) = "Syn " ^ c
|
neuper@37924
|
802 |
| itm_2str_ ctxt (Typ c) = "Typ " ^ c
|
neuper@37924
|
803 |
| itm_2str_ ctxt (Inc ((d,ts), penv)) =
|
neuper@37924
|
804 |
"Inc " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts)) ^ " ,"
|
neuper@37924
|
805 |
^ pen2str ctxt penv
|
neuper@37924
|
806 |
| itm_2str_ ctxt (Sup (d,ts)) =
|
neuper@37924
|
807 |
"Sup " ^ Syntax.string_of_term ctxt (comp_dts ctxt (d,ts))
|
neuper@37924
|
808 |
| itm_2str_ ctxt (Mis (d,pid))=
|
neuper@37924
|
809 |
"Mis "^ Syntax.string_of_term ctxt d ^
|
neuper@37924
|
810 |
" "^ Syntax.string_of_term ctxt pid
|
neuper@37924
|
811 |
| itm_2str_ ctxt (Par s) = "Trm "^s;
|
neuper@37924
|
812 |
fun itm_2str t = itm_2str_ (thy2ctxt "Isac") t;
|
neuper@37924
|
813 |
fun itm2str_ ctxt ((i,is,b,s,itm_):itm) =
|
neuper@37906
|
814 |
"("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^
|
neuper@37924
|
815 |
s^" ,"^(itm_2str_ ctxt itm_)^")";
|
neuper@37924
|
816 |
fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
|
neuper@37924
|
817 |
fun w_itms2str_ ctxt itms = writeln (itms2str_ ctxt itms);
|
neuper@37906
|
818 |
|
neuper@37906
|
819 |
fun init_item str = SyntaxE str;
|
neuper@37906
|
820 |
|
neuper@37906
|
821 |
|
neuper@37906
|
822 |
|
neuper@37906
|
823 |
|
neuper@37906
|
824 |
type 'a ppc =
|
neuper@37906
|
825 |
{Given : 'a list,
|
neuper@37906
|
826 |
Where: 'a list,
|
neuper@37906
|
827 |
Find : 'a list,
|
neuper@37906
|
828 |
With : 'a list,
|
neuper@37906
|
829 |
Relate: 'a list};
|
neuper@37906
|
830 |
fun ppc2str {Given=Given,Where=Where,Find=Find,With=With,Relate=Relate}=
|
neuper@37906
|
831 |
("{Given =" ^ (strs2str Given ) ^
|
neuper@37906
|
832 |
",Where=" ^ (strs2str Where) ^
|
neuper@37906
|
833 |
",Find =" ^ (strs2str Find ) ^
|
neuper@37906
|
834 |
",With =" ^ (strs2str With ) ^
|
neuper@37906
|
835 |
",Relate=" ^ (strs2str Relate) ^ "}");
|
neuper@37906
|
836 |
|
neuper@37906
|
837 |
|
neuper@37906
|
838 |
|
neuper@37906
|
839 |
|
neuper@37906
|
840 |
fun item_ppc ({Given = gi,Where= wh,
|
neuper@37906
|
841 |
Find = fi,With = wi,Relate= re}: string ppc) =
|
neuper@37906
|
842 |
{Given = map init_item gi,Where= map init_item wh,
|
neuper@37906
|
843 |
Find = map init_item fi,With = map init_item wi,
|
neuper@37906
|
844 |
Relate= map init_item re}:item ppc;
|
neuper@37906
|
845 |
fun itemppc2str ({Given=Given,Where=Where,
|
neuper@37906
|
846 |
Find=Find,With=With,Relate=Relate}:item ppc)=
|
neuper@37906
|
847 |
("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
|
neuper@37906
|
848 |
",Where=" ^ ((strs2str' o (map item2str)) Where) ^
|
neuper@37906
|
849 |
",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
|
neuper@37906
|
850 |
",With =" ^ ((strs2str' o (map item2str)) With ) ^
|
neuper@37906
|
851 |
",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
|
neuper@37906
|
852 |
|
neuper@37906
|
853 |
fun de_item (Correct x) = x
|
neuper@37906
|
854 |
| de_item (SyntaxE x) = x
|
neuper@37906
|
855 |
| de_item (TypeE x) = x
|
neuper@37906
|
856 |
| de_item (False x) = x
|
neuper@37906
|
857 |
| de_item (Incompl x) = x
|
neuper@37906
|
858 |
| de_item (Superfl x) = x
|
neuper@37906
|
859 |
| de_item (Missing x) = x;
|
neuper@37906
|
860 |
val empty_ppc ={Given = [],
|
neuper@37906
|
861 |
Where= [],
|
neuper@37906
|
862 |
Find = [],
|
neuper@37906
|
863 |
With = [],
|
neuper@37906
|
864 |
Relate= []}:item ppc;
|
neuper@37906
|
865 |
val empty_ppc_ct' ={Given = [],
|
neuper@37906
|
866 |
Where = [],
|
neuper@37906
|
867 |
Find = [],
|
neuper@37906
|
868 |
With = [],
|
neuper@37906
|
869 |
Relate= []}:cterm' ppc;
|
neuper@37906
|
870 |
|
neuper@37906
|
871 |
|
neuper@37906
|
872 |
datatype match =
|
neuper@37906
|
873 |
Matches of pblID * item ppc
|
neuper@37906
|
874 |
| NoMatch of pblID * item ppc;
|
neuper@37906
|
875 |
fun match2str (Matches (pI, ppc)) =
|
neuper@37906
|
876 |
"Matches ("^(strs2str pI)^", "^(itemppc2str ppc)^")"
|
neuper@37906
|
877 |
| match2str(NoMatch (pI, ppc)) =
|
neuper@37906
|
878 |
"NoMatch ("^(strs2str pI)^", "^(itemppc2str ppc)^")";
|
neuper@37906
|
879 |
fun matchs2str ms = (strs2str o (map match2str)) ms;
|
neuper@37906
|
880 |
fun pblID_of_match (Matches (pI,_)) = pI
|
neuper@37906
|
881 |
| pblID_of_match (NoMatch (pI,_)) = pI;
|
neuper@37906
|
882 |
|
neuper@37906
|
883 |
(*10.03 for Refine_Problem*)
|
neuper@37906
|
884 |
datatype match_ =
|
neuper@37906
|
885 |
Match_ of pblID * ((itm list) * ((bool * term) list))
|
neuper@37906
|
886 |
| NoMatch_;
|
neuper@37906
|
887 |
|
neuper@37906
|
888 |
(*. the refined pbt is the last_element Matches in the list .*)
|
neuper@37906
|
889 |
fun is_matches (Matches _) = true
|
neuper@37906
|
890 |
| is_matches _ = false;
|
neuper@37906
|
891 |
fun matches_pblID (Matches (pI,_)) = pI;
|
neuper@37906
|
892 |
fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms)
|
neuper@37906
|
893 |
handle _ => []:pblID;
|
neuper@37906
|
894 |
fun refined_IDitms ms = ((find_first is_matches) o rev) ms;
|
neuper@37906
|
895 |
|
neuper@37906
|
896 |
(*. the refined pbt is the last_element Matches in the list,
|
neuper@37906
|
897 |
for Refine_Problem, tryrefine .*)
|
neuper@37906
|
898 |
fun is_matches_ (Match_ _) = true
|
neuper@37906
|
899 |
| is_matches_ _ = false;
|
neuper@37906
|
900 |
fun refined_ ms = ((find_first is_matches_) o rev) ms;
|
neuper@37906
|
901 |
|
neuper@37906
|
902 |
|
neuper@37906
|
903 |
fun ts_in (Cor ((_,ts),_)) = ts
|
neuper@37906
|
904 |
| ts_in (Syn (c)) = []
|
neuper@37906
|
905 |
| ts_in (Typ (c)) = []
|
neuper@37906
|
906 |
| ts_in (Inc ((_,ts),_)) = ts
|
neuper@37906
|
907 |
| ts_in (Sup (_,ts)) = ts
|
neuper@37906
|
908 |
| ts_in (Mis _) = [];
|
neuper@37906
|
909 |
(*WN050629 unused*)
|
neuper@37906
|
910 |
fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
|
neuper@37924
|
911 |
val unique = (term_of o the o (parse (theory "Real"))) "UnIqE_tErM";
|
neuper@37906
|
912 |
fun d_in (Cor ((d,_),_)) = d
|
neuper@37906
|
913 |
| d_in (Syn (c)) = (writeln("*** d_in: Syn ("^c^")"); unique)
|
neuper@37906
|
914 |
| d_in (Typ (c)) = (writeln("*** d_in: Typ ("^c^")"); unique)
|
neuper@37906
|
915 |
| d_in (Inc ((d,_),_)) = d
|
neuper@37906
|
916 |
| d_in (Sup (d,_)) = d
|
neuper@37906
|
917 |
| d_in (Mis (d,_)) = d;
|
neuper@37906
|
918 |
|
neuper@37906
|
919 |
fun dts2str (d,ts) = pair2str (term2str d, terms2str ts);
|
neuper@37906
|
920 |
fun penvval_in (Cor ((d,_),(_,ts))) = [comp_ts (d,ts)]
|
neuper@37906
|
921 |
| penvval_in (Syn (c)) = (writeln("*** penvval_in: Syn ("^c^")"); [])
|
neuper@37906
|
922 |
| penvval_in (Typ (c)) = (writeln("*** penvval_in: Typ ("^c^")"); [])
|
neuper@37906
|
923 |
| penvval_in (Inc (_,(_,ts))) = ts
|
neuper@37906
|
924 |
| penvval_in (Sup dts) = (writeln("*** penvval_in: Sup "^(dts2str dts)); [])
|
neuper@37906
|
925 |
| penvval_in (Mis (d,t)) = (writeln("*** penvval_in: Mis "^
|
neuper@37906
|
926 |
(pair2str(term2str d, term2str t))); []);
|
neuper@37906
|
927 |
|
neuper@37906
|
928 |
|
neuper@37906
|
929 |
(*. check a predicate labelled with indication of incomplete substitution;
|
neuper@37906
|
930 |
rls -> (*for eval_true*)
|
neuper@37906
|
931 |
bool * (*have _all_ variables(Free) from the model-pattern
|
neuper@37906
|
932 |
been substituted by a value from the pattern's environment ?*)
|
neuper@37924
|
933 |
term (*the precondition*)
|
neuper@37906
|
934 |
->
|
neuper@37906
|
935 |
bool * (*has the precondition evaluated to true*)
|
neuper@37924
|
936 |
term (*the precondition (for map)*)
|
neuper@37906
|
937 |
.*)
|
neuper@37906
|
938 |
fun evalprecond prls (false, pre) =
|
neuper@37906
|
939 |
(*NOT ALL Free's have been substituted, eg. because of incomplete model*)
|
neuper@37906
|
940 |
(false, pre)
|
neuper@37906
|
941 |
| evalprecond prls (true, pre) =
|
neuper@37906
|
942 |
(* val (prls, pre) = (prls, hd pres');
|
neuper@37906
|
943 |
val (prls, pre) = (prls, hd (tl pres'));
|
neuper@37906
|
944 |
*)
|
neuper@37906
|
945 |
if eval_true (assoc_thy "Isac.thy") (*for Pattern.match *)
|
neuper@37906
|
946 |
[pre] prls (*pre parsed, prls.thy*)
|
neuper@37906
|
947 |
then (true , pre)
|
neuper@37906
|
948 |
else (false , pre);
|
neuper@37906
|
949 |
|
neuper@37906
|
950 |
fun pre2str (b, t) = pair2str(bool2str b, term2str t);
|
neuper@37906
|
951 |
fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
|
neuper@37906
|
952 |
|
neuper@37906
|
953 |
(*. check preconditions, return true if all true .*)
|
neuper@37906
|
954 |
fun check_preconds' _ [] _ _ = [] (*empty preconditions are true*)
|
neuper@37906
|
955 |
| check_preconds' prls pres pbl _(*FIXME.WN0308 mvat re-introduce*) =
|
neuper@37906
|
956 |
(* val (prls, pres, pbl, _) = (prls, where_, probl, 0);
|
neuper@37906
|
957 |
val (prls, pres, pbl, _) = (prls, pre, itms, mvat);
|
neuper@37906
|
958 |
*)
|
neuper@37906
|
959 |
let val env = mk_env pbl;
|
neuper@37906
|
960 |
val pres' = map (subst_atomic_all env) pres;
|
neuper@37906
|
961 |
in map (evalprecond prls) pres' end;
|
neuper@37906
|
962 |
|
neuper@37906
|
963 |
fun check_preconds thy prls pres pbl =
|
neuper@37906
|
964 |
check_preconds' prls pres pbl (max_vt pbl);
|
neuper@37906
|
965 |
|
neuper@37906
|
966 |
|
neuper@37906
|
967 |
|
neuper@37906
|
968 |
|
neuper@37906
|
969 |
(*----------------------------24.3.02: done too much-----
|
neuper@37906
|
970 |
(**. copy the already input items from probl to meth (in PblObj):
|
neuper@37906
|
971 |
for each item in met search the related one in pbl,
|
neuper@37906
|
972 |
items not found in probl are (1) inserted as 'untouched' (0,...),
|
neuper@37906
|
973 |
and (2) completed from oris (via max_vt)
|
neuper@37906
|
974 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ "uberkomplett 21.2.02 ------------ .**)
|
neuper@37906
|
975 |
(* val (pbl, met) = (itms, ppc);
|
neuper@37906
|
976 |
*)
|
neuper@37906
|
977 |
fun copy_pbl thy oris pbl met =
|
neuper@37906
|
978 |
let val vt = max_vt pbl;
|
neuper@37906
|
979 |
fun vt_and_dsc d' ((i,v,f,d,ts):ori) =
|
neuper@37906
|
980 |
vt mem v andalso d'= d
|
neuper@37906
|
981 |
fun cpy its [] (f, (d, id)) =
|
neuper@37906
|
982 |
if length its = 0 (*no dsc found in pbl*)
|
neuper@37906
|
983 |
then case find_first (vt_and_dsc d) oris
|
neuper@37924
|
984 |
of SOME (i,v,_,_,ts) =>
|
neuper@37906
|
985 |
[(i,v,true,f, Cor ((d,ts), (id,pbl_ids' thy d ts)))]
|
neuper@37924
|
986 |
| NONE => [(0,[],false,f,Mis (d, id))]
|
neuper@37906
|
987 |
else its
|
neuper@37906
|
988 |
| cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
|
neuper@37906
|
989 |
if d = d_in itm_ andalso i<>0 (*already touched by user*)
|
neuper@37906
|
990 |
then cpy (its @ [it]) itms pb else cpy its itms pb;
|
neuper@37906
|
991 |
in ((flat o (map (cpy [] pbl))) met):itm list end;
|
neuper@37906
|
992 |
|
neuper@37906
|
993 |
|
neuper@37906
|
994 |
(**. copy the already input items from probl to meth (in PblObj):
|
neuper@37906
|
995 |
for each item in met search the related one in pbl,
|
neuper@37906
|
996 |
items not found in probl are inserted as 'untouched' (0,...)
|
neuper@37906
|
997 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ "uberkomplett 21.2.02 ------------ .**)
|
neuper@37906
|
998 |
(* val (pbl, met) = (itms, ppc);
|
neuper@37906
|
999 |
*)
|
neuper@37906
|
1000 |
fun copy_pbl (pbl:itm list) met =
|
neuper@37906
|
1001 |
let fun cpy its [] (f, (d, id)) =
|
neuper@37906
|
1002 |
if length its = 0 (*no dsc found in pbl*)
|
neuper@37906
|
1003 |
then [(0,[],false,f,Mis (d, id))]
|
neuper@37906
|
1004 |
else its
|
neuper@37906
|
1005 |
| cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
|
neuper@37906
|
1006 |
if d = d_in itm_ andalso i<>0 (*already touched by user*)
|
neuper@37906
|
1007 |
then cpy (its @ [it]) itms pb else cpy its itms pb;
|
neuper@37906
|
1008 |
in ((flat o (map (cpy [] pbl))) met):itm list end;
|
neuper@37906
|
1009 |
|
neuper@37906
|
1010 |
|
neuper@37906
|
1011 |
(**. copy the already input items from probl to meth (in PblObj):
|
neuper@37906
|
1012 |
for each item in met search the related one in pbl
|
neuper@37906
|
1013 |
(missing items are requested by nxt_spec) .**)
|
neuper@37906
|
1014 |
(* val (pbl, met) = (itms, ppc);
|
neuper@37906
|
1015 |
*)
|
neuper@37906
|
1016 |
fun copy_pbl (pbl:itm list) met =
|
neuper@37906
|
1017 |
let fun cpy its [] (f, (d, id)) = its
|
neuper@37906
|
1018 |
| cpy its ((it as (i, vs, b, f, itm_))::itms) (pb as (x, (d, id))) =
|
neuper@37906
|
1019 |
if d = d_in itm_ andalso i<>0 (*already touched by user*)
|
neuper@37906
|
1020 |
then cpy (its @ [it]) itms pb
|
neuper@37906
|
1021 |
else cpy its itms pb;
|
neuper@37906
|
1022 |
in ((flat o (map (cpy [] pbl))) met):itm list end;
|
neuper@37906
|
1023 |
|
neuper@37906
|
1024 |
(*. copy pbt to met (in Specify_Method)
|
neuper@37906
|
1025 |
ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
|
neuper@37906
|
1026 |
(2) filter (dsc(pbt) = dsc(oris)) oris; -> newitms;
|
neuper@37906
|
1027 |
(3) pbt @ newitms .*)
|
neuper@37906
|
1028 |
(* val (pbl, met) = (itms, pbt);
|
neuper@37906
|
1029 |
*)
|
neuper@37906
|
1030 |
fun copy_pbl (pbl:itm list) met oris =
|
neuper@37906
|
1031 |
let fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
|
neuper@37906
|
1032 |
fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
|
neuper@37924
|
1033 |
SOME _ => false | NONE => true;
|
neuper@37906
|
1034 |
(*1*)val mis = ((map (cons2 (fst, fst o snd))) o (filter (notmem pbl))) met;
|
neuper@37906
|
1035 |
|
neuper@37906
|
1036 |
fun eqdsc_ori d ((_,_,_,d',_):ori) = d = d';
|
neuper@37906
|
1037 |
fun ori2itmMis f ((i,v,_,d,ts):ori) = (i,v,false,f,Mis (d,ts)):itm;
|
neuper@37906
|
1038 |
fun oris2itms oris mis1 = ((map (ori2itmMis (fst mis1)))
|
neuper@37906
|
1039 |
o (filter ((eqdsc_ori o snd) mis1))) oris;
|
neuper@37906
|
1040 |
val news = (flat o (map (oris2itms oris))) mis;
|
neuper@37906
|
1041 |
in pbl @ news end;
|
neuper@37906
|
1042 |
----------------------------24.3.02: done too much-----*)
|
neuper@37906
|
1043 |
|
neuper@37906
|
1044 |
|
neuper@37906
|
1045 |
|
neuper@37906
|
1046 |
|
neuper@37906
|
1047 |
|
neuper@37906
|
1048 |
|
neuper@37906
|
1049 |
(* ---------------------------------------------NOT UPTODATE !!! 4.9.01
|
neuper@37906
|
1050 |
eval test-maximum.sml until Specify_Method ...
|
neuper@37906
|
1051 |
val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
|
neuper@37906
|
1052 |
val met = (#ppc o get_met) mI;
|
neuper@37906
|
1053 |
val (m::_) = met;
|
neuper@37906
|
1054 |
cpy [] pbl m;
|
neuper@37906
|
1055 |
[((1,[1,2,3],true,"#Given",Cor ((Const #,[#]),[])),
|
neuper@37906
|
1056 |
[([1,2,3],Const ("Descript.fixedValues","bool List.list => Tools.nam"),
|
neuper@37906
|
1057 |
Free ("fix_","bool List.list"),Const # $ Free # $ Const (#,#))])]
|
neuper@37906
|
1058 |
: (itm * (vats * term * term * term) list) list
|
neuper@37906
|
1059 |
|
neuper@37906
|
1060 |
upds_envv thy [] (flat eargs);
|
neuper@37906
|
1061 |
[(1,
|
neuper@37906
|
1062 |
[(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
|
neuper@37906
|
1063 |
(Free ("m_","bool"),[Free (#,#)]),
|
neuper@37906
|
1064 |
(Free ("vs_","bool List.list"),[# $ # $ (# $ #)]),
|
neuper@37906
|
1065 |
(Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
|
neuper@37906
|
1066 |
(2,
|
neuper@37906
|
1067 |
[(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
|
neuper@37906
|
1068 |
(Free ("m_","bool"),[Free (#,#)]),
|
neuper@37906
|
1069 |
(Free ("vs_","bool List.list"),[# $ # $ (# $ #)]),
|
neuper@37906
|
1070 |
(Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),
|
neuper@37906
|
1071 |
(3,
|
neuper@37906
|
1072 |
[(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
|
neuper@37906
|
1073 |
(Free ("m_","bool"),[Free (#,#)]),
|
neuper@37906
|
1074 |
(Free ("vs_","bool List.list"),[# $ # $ (# $ #)])])] : envv
|
neuper@37906
|
1075 |
*)
|
neuper@37906
|
1076 |
|
neuper@37906
|
1077 |
(*----------------------------------------------------------*)
|
neuper@37906
|
1078 |
end
|
neuper@37906
|
1079 |
open SpecifyTools;
|
neuper@37906
|
1080 |
(*----------------------------------------------------------*)
|