neuper@37947
|
1 |
(* tools which depend on Script.thy and thus are not in term.sml
|
neuper@37906
|
2 |
(c) Walther Neuper 2000
|
neuper@37906
|
3 |
|
neuper@37947
|
4 |
use"ProgLang/scrtools.sml";
|
neuper@37906
|
5 |
use"scrtools.sml";
|
neuper@37906
|
6 |
*)
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
fun is_reall_dsc
|
neuper@37906
|
10 |
(Const(_,Type("fun",[Type("List.list",
|
neuper@37906
|
11 |
[Type ("real",[])]),_]))) = true
|
neuper@37906
|
12 |
| is_reall_dsc
|
neuper@37906
|
13 |
(Const(_,Type("fun",[Type("List.list",
|
neuper@37906
|
14 |
[Type ("real",[])]),_])) $ t) = true
|
neuper@37906
|
15 |
| is_reall_dsc _ = false;
|
neuper@37906
|
16 |
fun is_booll_dsc
|
neuper@37906
|
17 |
(Const(_,Type("fun",[Type("List.list",
|
neuper@37906
|
18 |
[Type ("bool",[])]),_]))) = true
|
neuper@37906
|
19 |
| is_booll_dsc
|
neuper@37906
|
20 |
(Const(_,Type("fun",[Type("List.list",
|
neuper@37906
|
21 |
[Type ("bool",[])]),_])) $ t) = true
|
neuper@37906
|
22 |
| is_booll_dsc _ = false;
|
neuper@37906
|
23 |
(*
|
neuper@37906
|
24 |
> val t = (term_of o the o (parse thy)) "relations";
|
neuper@37906
|
25 |
> atomtyp (type_of t);
|
neuper@37906
|
26 |
*** Type (fun,[
|
neuper@37906
|
27 |
*** Type (List.list,[
|
neuper@37906
|
28 |
*** Type (bool,[])
|
neuper@37906
|
29 |
*** ]
|
neuper@37906
|
30 |
*** Type (Tools.una,[])
|
neuper@37906
|
31 |
*** ]
|
neuper@37906
|
32 |
> is_booll_dsc t;
|
neuper@37906
|
33 |
val it = true : bool
|
neuper@37906
|
34 |
> is_reall_dsc t;
|
neuper@37906
|
35 |
val it = false : bool
|
neuper@37906
|
36 |
*)
|
neuper@37906
|
37 |
|
neuper@37906
|
38 |
fun is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_]))) = true
|
neuper@37906
|
39 |
| is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_])) $ t) = true
|
neuper@37906
|
40 |
(*WN:8.5.03: ??? ~~~~ ???*)
|
neuper@37906
|
41 |
| is_list_dsc _ = false;
|
neuper@37906
|
42 |
(*
|
neuper@37906
|
43 |
> val t = str2term "someList";
|
neuper@37906
|
44 |
> is_list_dsc t;
|
neuper@37906
|
45 |
val it = true : bool
|
neuper@37906
|
46 |
|
neuper@37906
|
47 |
> val t = (term_of o the o (parse thy))
|
neuper@37906
|
48 |
"additional_relations [a=b,c=(d::real)]";
|
neuper@37906
|
49 |
> is_list_dsc t;
|
neuper@37906
|
50 |
val it = true : bool
|
neuper@37906
|
51 |
> is_list_dsc (head_of t);
|
neuper@37906
|
52 |
val it = true : bool
|
neuper@37906
|
53 |
|
neuper@37906
|
54 |
> val t = (term_of o the o (parse thy))"max_relation (A=#2*a*b-a^^^#2)";
|
neuper@37906
|
55 |
> is_list_dsc t;
|
neuper@37906
|
56 |
val it = false : bool
|
neuper@37906
|
57 |
> is_list_dsc (head_of t);
|
neuper@37906
|
58 |
val it = false : bool
|
neuper@37906
|
59 |
> val t = (term_of o the o (parse thy)) "testdscforlist";
|
neuper@37906
|
60 |
> is_list_dsc (head_of t);
|
neuper@37906
|
61 |
val it = true : bool
|
neuper@37906
|
62 |
*)
|
neuper@37906
|
63 |
|
neuper@37906
|
64 |
|
neuper@37906
|
65 |
fun is_unl (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true
|
neuper@37906
|
66 |
| is_unl _ = false;
|
neuper@37906
|
67 |
(*
|
neuper@37906
|
68 |
> val t = str2term "someList"; is_unl t;
|
neuper@37906
|
69 |
val it = true : bool
|
neuper@37906
|
70 |
> val t = (term_of o the o (parse thy)) "maximum";
|
neuper@37906
|
71 |
> is_unl t;
|
neuper@37906
|
72 |
val it = false : bool
|
neuper@37906
|
73 |
*)
|
neuper@37906
|
74 |
|
neuper@37906
|
75 |
fun is_dsc (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) = true
|
neuper@37906
|
76 |
| is_dsc (Const(_,Type("fun",[_,Type("Tools.una",_)]))) = true
|
neuper@37906
|
77 |
| is_dsc (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true
|
neuper@37906
|
78 |
| is_dsc (Const(_,Type("fun",[_,Type("Tools.str",_)]))) = true
|
neuper@37906
|
79 |
| is_dsc (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) = true
|
neuper@37906
|
80 |
| is_dsc (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))= true
|
neuper@37906
|
81 |
| is_dsc (Const(_,Type("fun",[_,Type("Tools.tobooll",_)])))= true
|
neuper@37906
|
82 |
| is_dsc (Const(_,Type("fun",[_,Type("Tools.unknow",_)])))= true
|
neuper@37906
|
83 |
| is_dsc (Const(_,Type("fun",[_,Type("Tools.cpy",_)])))= true
|
neuper@37906
|
84 |
| is_dsc _ = false;
|
neuper@37906
|
85 |
fun is_dsc term =
|
neuper@37906
|
86 |
(case (range_type o type_of) term of
|
neuper@37906
|
87 |
Type("Tools.nam",_) => true
|
neuper@37906
|
88 |
| Type("Tools.una",_) => true
|
neuper@37906
|
89 |
| Type("Tools.unl",_) => true
|
neuper@37906
|
90 |
| Type("Tools.str",_) => true
|
neuper@37906
|
91 |
| Type("Tools.toreal",_) => true
|
neuper@37906
|
92 |
| Type("Tools.toreall",_) => true
|
neuper@37906
|
93 |
| Type("Tools.tobooll",_) => true
|
neuper@37906
|
94 |
| Type("Tools.unknow",_) => true
|
neuper@37906
|
95 |
| Type("Tools.cpy",_) => true
|
neuper@37906
|
96 |
| _ => false)
|
neuper@37906
|
97 |
handle Match => false;
|
neuper@37906
|
98 |
|
neuper@37906
|
99 |
|
neuper@37906
|
100 |
(*
|
neuper@37906
|
101 |
val t as t1 $ t2 = str2term "antiDerivativeName M_b";
|
neuper@37906
|
102 |
val Const (_, Type ("fun", [Type ("fun", _), Type ("Tools.una",[])])) $ _ = t;
|
neuper@37906
|
103 |
is_dsc t1;
|
neuper@37906
|
104 |
|
neuper@37906
|
105 |
> val t = (term_of o the o (parse thy)) "maximum";
|
neuper@37906
|
106 |
> is_dsc t;
|
neuper@37906
|
107 |
val it = true : bool
|
neuper@37906
|
108 |
> val t = (term_of o the o (parse thy)) "testdscforlist";
|
neuper@37906
|
109 |
> is_dsc t;
|
neuper@37906
|
110 |
val it = true : bool
|
neuper@37906
|
111 |
|
neuper@37906
|
112 |
> val t = (head_of o term_of o the o (parse thy)) "maximum A";
|
neuper@37906
|
113 |
> is_dsc t;
|
neuper@37906
|
114 |
val it = true : bool
|
neuper@37906
|
115 |
> val t = (head_of o term_of o the o (parse thy))
|
neuper@37906
|
116 |
"fixedValues [R=(R::real)]";
|
neuper@37906
|
117 |
> is_dsc t;
|
neuper@37906
|
118 |
val it = true : bool
|
neuper@37906
|
119 |
*)
|
neuper@37906
|
120 |
|
neuper@37906
|
121 |
|
neuper@37906
|
122 |
(*make the term 'Subproblem (domID, pblID)' to a formula for frontend;
|
neuper@37906
|
123 |
needs to be here after def. Subproblem in Script.thy*)
|
neuper@37906
|
124 |
val t as (subpbl_t $ (pair_t $ Free (domID,_) $ pblID)) =
|
neuper@37906
|
125 |
(term_of o the o (parse @{theory Script}))
|
neuper@37906
|
126 |
"Subproblem (Isac,[equation,univar])";
|
neuper@37906
|
127 |
val t as (pbl_t $ _) =
|
neuper@37906
|
128 |
(term_of o the o (parse @{theory Script}))
|
neuper@37906
|
129 |
"Problem (Isac,[equation,univar])";
|
neuper@37906
|
130 |
val Free (_, ID_type) = (term_of o the o (parse @{theory Script})) "x::ID";
|
neuper@37906
|
131 |
|
neuper@37906
|
132 |
|
neuper@37906
|
133 |
fun subpbl domID pblID =
|
neuper@37906
|
134 |
subpbl_t $ (pair_t $ Free (domID,ID_type) $
|
neuper@37906
|
135 |
(((list2isalist ID_type) o (map (mk_free ID_type))) pblID));
|
neuper@37906
|
136 |
(*> subpbl "Isac" ["equation","univar"] = t;
|
neuper@37906
|
137 |
val it = true : bool *)
|
neuper@37906
|
138 |
|
neuper@37906
|
139 |
|
neuper@37906
|
140 |
fun pblterm (domID:domID) (pblID:pblID) =
|
neuper@37906
|
141 |
pbl_t $ (pair_t $ Free (domID,ID_type) $
|
neuper@37906
|
142 |
(((list2isalist ID_type) o (map (mk_free ID_type))) pblID));
|
neuper@37906
|
143 |
|
neuper@37906
|
144 |
|
neuper@37906
|
145 |
(**.construct scr-env from scr(created automatically) and Rewrite_Set.**)
|
neuper@37906
|
146 |
|
neuper@37906
|
147 |
fun one_scr_arg (Const _ $ arg $ _) = arg
|
neuper@37906
|
148 |
| one_scr_arg t = raise error ("one_scr_arg: called by "^(term2str t));
|
neuper@37906
|
149 |
fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2)
|
neuper@37906
|
150 |
| two_scr_arg t = raise error ("two_scr_arg: called by "^(term2str t));
|
neuper@37906
|
151 |
|
neuper@37906
|
152 |
|
neuper@37906
|
153 |
(**.generate calc from a script.**)
|
neuper@37906
|
154 |
|
neuper@37906
|
155 |
(*.instantiate a stactic or scriptexpr, and ev. attach (curried) argument
|
neuper@37906
|
156 |
args:
|
neuper@37906
|
157 |
E environment
|
neuper@37906
|
158 |
v current value, is attached to curried stactics
|
neuper@37906
|
159 |
stac stactic to be instantiated
|
neuper@37906
|
160 |
precond:
|
neuper@37906
|
161 |
not (a = NONE) /\ (v = e_term) /\ (stac curried, i.e. without last arg.)
|
neuper@37906
|
162 |
this ........................ is the initialization for assy with l=[],
|
neuper@37906
|
163 |
but the 1st stac is
|
neuper@37906
|
164 |
(a) curried: then (a = SOME _), or
|
neuper@37906
|
165 |
(b) not curried: then the values of the initialization are not used
|
neuper@37906
|
166 |
.*)
|
neuper@37906
|
167 |
datatype stacexpr = STac of term | Expr of term
|
neuper@37906
|
168 |
fun rep_stacexpr (STac t ) = t
|
neuper@37906
|
169 |
| rep_stacexpr (Expr t) =
|
neuper@37906
|
170 |
raise error ("rep_stacexpr called with t= "^(term2str t));
|
neuper@37906
|
171 |
|
neuper@37906
|
172 |
type env = (term * term) list;
|
neuper@37906
|
173 |
|
neuper@37906
|
174 |
(*update environment; t <> empty if coming from listexpr*)
|
neuper@37906
|
175 |
fun upd_env (env:env) (v,t) =
|
neuper@37906
|
176 |
let val env' = if t = e_term then env else overwrite (env,(v,t));
|
neuper@37906
|
177 |
(*val _= writeln("### upd_env: = "^(subst2str env'));*)
|
neuper@37906
|
178 |
in env' end;
|
neuper@37906
|
179 |
|
neuper@37906
|
180 |
(*.substitute the scripts environment in a leaf of the scripts parse-tree
|
neuper@37906
|
181 |
and attach the curried argument of a tactic, if any.
|
neuper@37906
|
182 |
a leaf is either a tactic or an 'exp' in 'let v = expr'
|
neuper@37906
|
183 |
where 'exp' does not contain a tactic.
|
neuper@37906
|
184 |
CAUTION: (1) currying with @@ requires 2 patterns for each tactic
|
neuper@37906
|
185 |
(2) the non-curried version must return NONE for a
|
neuper@37906
|
186 |
(3) non-matching patterns become an Expr by fall-through.
|
neuper@37906
|
187 |
WN060906 quick and dirty fix: due to (2) a is returned, too.*)
|
neuper@37906
|
188 |
fun subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=
|
neuper@37906
|
189 |
(NONE, STac (subst_atomic E t))
|
neuper@37906
|
190 |
|
neuper@37906
|
191 |
| subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))=
|
neuper@37906
|
192 |
(a, (*in these cases we hope, that a = SOME _*)
|
neuper@37906
|
193 |
STac (case a of SOME a' => (subst_atomic E (t $ a'))
|
neuper@37906
|
194 |
| NONE => ((subst_atomic E t) $ v)))
|
neuper@37906
|
195 |
|
neuper@37906
|
196 |
| subst_stacexpr E a v
|
neuper@37906
|
197 |
(t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ _ )) =
|
neuper@37906
|
198 |
(NONE, STac (subst_atomic E t))
|
neuper@37906
|
199 |
|
neuper@37906
|
200 |
| subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _))=
|
neuper@37906
|
201 |
(a, STac (case a of SOME a' => subst_atomic E (t $ a')
|
neuper@37906
|
202 |
| NONE => ((subst_atomic E t) $ v)))
|
neuper@37906
|
203 |
|
neuper@37906
|
204 |
| subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ ))=
|
neuper@37906
|
205 |
(NONE, STac (subst_atomic E t))
|
neuper@37906
|
206 |
|
neuper@37906
|
207 |
| subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) =
|
neuper@37906
|
208 |
(a, STac (case a of SOME a' => subst_atomic E (t $ a')
|
neuper@37906
|
209 |
| NONE => ((subst_atomic E t) $ v)))
|
neuper@37906
|
210 |
|
neuper@37906
|
211 |
| subst_stacexpr E a v
|
neuper@37906
|
212 |
(t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ _ )) =
|
neuper@37906
|
213 |
(NONE, STac (subst_atomic E t))
|
neuper@37906
|
214 |
|
neuper@37906
|
215 |
| subst_stacexpr E a v
|
neuper@37906
|
216 |
(t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )) =
|
neuper@37906
|
217 |
(a, STac (case a of SOME a' => subst_atomic E (t $ a')
|
neuper@37906
|
218 |
| NONE => ((subst_atomic E t) $ v)))
|
neuper@37906
|
219 |
|
neuper@37906
|
220 |
| subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) =
|
neuper@37906
|
221 |
(NONE, STac (subst_atomic E t))
|
neuper@37906
|
222 |
|
neuper@37906
|
223 |
| subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ )) =
|
neuper@37906
|
224 |
(a, STac (case a of SOME a' => subst_atomic E (t $ a')
|
neuper@37906
|
225 |
| NONE => ((subst_atomic E t) $ v)))
|
neuper@37906
|
226 |
|
neuper@37906
|
227 |
| subst_stacexpr E a v
|
neuper@37906
|
228 |
(t as (Const("Script.Check'_elementwise",_) $ _ $ _ )) =
|
neuper@37906
|
229 |
(NONE, STac (subst_atomic E t))
|
neuper@37906
|
230 |
|
neuper@37906
|
231 |
| subst_stacexpr E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) =
|
neuper@37906
|
232 |
(a, STac (case a of SOME a' => subst_atomic E (t $ a')
|
neuper@37906
|
233 |
| NONE => ((subst_atomic E t) $ v)))
|
neuper@37906
|
234 |
|
neuper@37906
|
235 |
| subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) =
|
neuper@37906
|
236 |
(NONE, STac (subst_atomic E t))
|
neuper@37906
|
237 |
|
neuper@37906
|
238 |
| subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*)
|
neuper@37906
|
239 |
(a, STac (case a of SOME a' => subst_atomic E (t $ a')
|
neuper@37906
|
240 |
| NONE => ((subst_atomic E t) $ v)))
|
neuper@37906
|
241 |
|
neuper@37906
|
242 |
| subst_stacexpr E a v (t as (Const ("Script.SubProblem",_) $ _ $ _ )) =
|
neuper@37906
|
243 |
(NONE, STac (subst_atomic E t))
|
neuper@37906
|
244 |
|
neuper@37906
|
245 |
| subst_stacexpr E a v (t as (Const ("Script.Take",_) $ _ )) =
|
neuper@37906
|
246 |
(NONE, STac (subst_atomic E t))
|
neuper@37906
|
247 |
|
neuper@37906
|
248 |
| subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ $ _ )) =
|
neuper@37906
|
249 |
(NONE, STac (subst_atomic E t))
|
neuper@37906
|
250 |
|
neuper@37906
|
251 |
| subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ )) =
|
neuper@37906
|
252 |
(a, STac (case a of SOME a' => subst_atomic E (t $ a')
|
neuper@37906
|
253 |
| NONE => ((subst_atomic E t) $ v)))
|
neuper@37906
|
254 |
|
neuper@37906
|
255 |
(*now all tactics are matched out and this leaf must be without a tactic*)
|
neuper@37906
|
256 |
| subst_stacexpr E a v t =
|
neuper@37906
|
257 |
(a, Expr (subst_atomic (case a of SOME a => upd_env E (a,v)
|
neuper@37906
|
258 |
| NONE => E) t));
|
neuper@37906
|
259 |
(*> val t = str2term "SubProblem(Test_, [linear, univariate, equation, test], [Test, solve_linear]) [bool_ e_, real_ v_]";
|
neuper@37906
|
260 |
> subst_stacexpr [] NONE e_term t;*)
|
neuper@37906
|
261 |
|
neuper@37906
|
262 |
|
neuper@37906
|
263 |
fun stacpbls (h $ body) =
|
neuper@37906
|
264 |
let
|
neuper@37906
|
265 |
fun scan ts (Const ("Let",_) $ e $ (Abs (v,T,b))) =
|
neuper@37906
|
266 |
(scan ts e) @ (scan ts b)
|
neuper@37906
|
267 |
| scan ts (Const ("If",_) $ c $ e1 $ e2) = (scan ts e1) @ (scan ts e2)
|
neuper@37906
|
268 |
| scan ts (Const ("Script.While",_) $ c $ e $ _) = scan ts e
|
neuper@37906
|
269 |
| scan ts (Const ("Script.While",_) $ c $ e) = scan ts e
|
neuper@37906
|
270 |
| scan ts (Const ("Script.Repeat",_) $ e $ _) = scan ts e
|
neuper@37906
|
271 |
| scan ts (Const ("Script.Repeat",_) $ e) = scan ts e
|
neuper@37906
|
272 |
| scan ts (Const ("Script.Try",_) $ e $ _) = scan ts e
|
neuper@37906
|
273 |
| scan ts (Const ("Script.Try",_) $ e) = scan ts e
|
neuper@37906
|
274 |
| scan ts (Const ("Script.Or",_) $e1 $ e2 $ _) =
|
neuper@37906
|
275 |
(scan ts e1) @ (scan ts e2)
|
neuper@37906
|
276 |
| scan ts (Const ("Script.Or",_) $e1 $ e2) =
|
neuper@37906
|
277 |
(scan ts e1) @ (scan ts e2)
|
neuper@37906
|
278 |
| scan ts (Const ("Script.Seq",_) $e1 $ e2 $ _) =
|
neuper@37906
|
279 |
(scan ts e1) @ (scan ts e2)
|
neuper@37906
|
280 |
| scan ts (Const ("Script.Seq",_) $e1 $ e2) =
|
neuper@37906
|
281 |
(scan ts e1) @ (scan ts e2)
|
neuper@37906
|
282 |
| scan ts t = case subst_stacexpr [] NONE e_term t of
|
neuper@37906
|
283 |
(_, STac _) => [t] | (_, Expr _) => []
|
neuper@37906
|
284 |
in (distinct o (scan [])) body end;
|
neuper@37906
|
285 |
(*sc = Solve_root_equation ...
|
neuper@37906
|
286 |
> val ts = stacpbls sc;
|
neuper@37906
|
287 |
> writeln (terms2str thy ts);
|
neuper@37906
|
288 |
["Rewrite square_equation_left True e_",
|
neuper@37906
|
289 |
"Rewrite_Set SqRoot_simplify False e_",
|
neuper@37906
|
290 |
"Rewrite_Set rearrange_assoc False e_",
|
neuper@37906
|
291 |
"Rewrite_Set isolate_root False e_",
|
neuper@37906
|
292 |
"Rewrite_Set norm_equation False e_",
|
neuper@37906
|
293 |
"Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False e_"]
|
neuper@37906
|
294 |
*)
|
neuper@37906
|
295 |
|
neuper@37906
|
296 |
|
neuper@37906
|
297 |
|
neuper@37906
|
298 |
fun is_calc (Const ("Script.Calculate",_) $ _) = true
|
neuper@37906
|
299 |
| is_calc (Const ("Script.Calculate",_) $ _ $ _) = true
|
neuper@37906
|
300 |
| is_calc _ = false;
|
neuper@37906
|
301 |
fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_
|
neuper@37906
|
302 |
| op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_
|
neuper@37906
|
303 |
| op_of_calc t = raise error ("op_of_calc called with"^term2str t);
|
neuper@37906
|
304 |
(*
|
neuper@37906
|
305 |
val Script sc = (#scr o rep_rls) Test_simplify;
|
neuper@37906
|
306 |
val stacs = stacpbls sc;
|
neuper@37906
|
307 |
|
neuper@37906
|
308 |
val calcs = filter is_calc stacs;
|
neuper@37906
|
309 |
val ids = map op_of_calc calcs;
|
neuper@37906
|
310 |
map (curry assoc1 (!calclist')) ids;
|
neuper@37906
|
311 |
|
neuper@37906
|
312 |
(((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
|
neuper@37906
|
313 |
(filter is_calc) o stacpbls) sc):calc list;
|
neuper@37906
|
314 |
*)
|
neuper@37906
|
315 |
|
neuper@37906
|
316 |
(**.for automatic creation of scripts from rls.**)
|
neuper@37906
|
317 |
(* naming of identifiers in scripts ???...
|
neuper@37906
|
318 |
((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t::'z) = t";
|
neuper@37906
|
319 |
((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o
|
neuper@37906
|
320 |
(parse @{theory})) "(t't::'z) = t't";
|
neuper@37906
|
321 |
((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_t::'z) = t_t";
|
neuper@37906
|
322 |
(* not accepted !!!...*)
|
neuper@37906
|
323 |
((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_::'z) = t_";
|
neuper@37906
|
324 |
((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o
|
neuper@37906
|
325 |
(parse @{theory})) "(_t::'z) = _t";
|
neuper@37906
|
326 |
*)
|
neuper@37906
|
327 |
((inst_abs @{theory}) o term_of o the o (parse @{theory}))
|
neuper@37906
|
328 |
"Script Stepwise (t::'z) =\
|
neuper@37906
|
329 |
\(Repeat\
|
neuper@37906
|
330 |
\ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
|
neuper@37906
|
331 |
\ (Try (Repeat (Rewrite real_add_commute False))) @@ \
|
neuper@37906
|
332 |
\ (Try (Repeat (Rewrite real_mult_commute False)))) \
|
neuper@37923
|
333 |
\ t_t)";
|
neuper@37906
|
334 |
val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*)
|
neuper@37906
|
335 |
((inst_abs @{theory}) o term_of o the o (parse @{theory}))
|
neuper@37906
|
336 |
"Script Stepwise (t::'z) =\
|
neuper@37906
|
337 |
\(Repeat\
|
neuper@37906
|
338 |
\ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
|
neuper@37906
|
339 |
\ (Try (Repeat (Rewrite real_add_commute False))) @@ \
|
neuper@37906
|
340 |
\ (Try (Repeat (Rewrite real_mult_commute False)))) \
|
neuper@37923
|
341 |
\ t_t)";
|
neuper@37906
|
342 |
(*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body
|
neuper@37906
|
343 |
are inconsistent !!!*)
|
neuper@37906
|
344 |
val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*)
|
neuper@37906
|
345 |
((inst_abs @{theory}) o term_of o the o (parse @{theory}))
|
neuper@37906
|
346 |
"Script Stepwise_inst (t::'z) (v::real) =\
|
neuper@37906
|
347 |
\(Repeat\
|
neuper@37906
|
348 |
\ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \
|
neuper@37906
|
349 |
\ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_add_commute False))) @@\
|
neuper@37906
|
350 |
\ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \
|
neuper@37906
|
351 |
\ t)";
|
neuper@37921
|
352 |
val Repeat $ _ =
|
neuper@37906
|
353 |
((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
|
neuper@37906
|
354 |
"Repeat (Rewrite real_diff_minus False t)";
|
neuper@37906
|
355 |
val Try $ _ =
|
neuper@37906
|
356 |
((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
|
neuper@37906
|
357 |
"Try (Rewrite real_diff_minus False t)";
|
neuper@37906
|
358 |
val Cal $ _ =
|
neuper@37906
|
359 |
((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
|
neuper@37921
|
360 |
"Calculate PLUS";
|
neuper@37906
|
361 |
val Ca1 $ _ =
|
neuper@37906
|
362 |
((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
|
neuper@37921
|
363 |
"Calculate1 PLUS";
|
neuper@37906
|
364 |
val Rew $ (Free (_,IDtype)) $ _ $ t =
|
neuper@37906
|
365 |
((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
|
neuper@37906
|
366 |
"Rewrite real_diff_minus False t";
|
neuper@37906
|
367 |
val Rew_Inst $ Subs $ _ $ _ =
|
neuper@37906
|
368 |
((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
|
neuper@37906
|
369 |
"Rewrite_Inst [(bdv,v)] real_diff_minus False";
|
neuper@37906
|
370 |
val Rew_Set $ _ $ _ =
|
neuper@37906
|
371 |
((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
|
neuper@37906
|
372 |
"Rewrite_Set real_diff_minus False";
|
neuper@37906
|
373 |
val Rew_Set_Inst $ _ $ _ $ _ =
|
neuper@37906
|
374 |
((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
|
neuper@37906
|
375 |
"Rewrite_Set_Inst [(bdv,v)] real_diff_minus False";
|
neuper@37906
|
376 |
val SEq $ _ $ _ $ _ =
|
neuper@37906
|
377 |
((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
|
neuper@37906
|
378 |
" ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
|
neuper@37906
|
379 |
\ (Try (Repeat (Rewrite real_add_commute False))) @@ \
|
neuper@37906
|
380 |
\ (Try (Repeat (Rewrite real_mult_commute False)))) t";
|
neuper@37906
|
381 |
|
neuper@37906
|
382 |
fun rule2stac _ (Thm (thmID, _)) =
|
neuper@37906
|
383 |
Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const))
|
neuper@37906
|
384 |
| rule2stac calc (Calc (c, _)) =
|
neuper@37906
|
385 |
Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
|
neuper@37906
|
386 |
| rule2stac calc (Cal1 (c, _)) =
|
neuper@37906
|
387 |
Try $ (Repeat $ (Ca1 $ Free (assoc_calc (calc ,c), IDtype)))
|
neuper@37906
|
388 |
| rule2stac _ (Rls_ rls) =
|
neuper@37906
|
389 |
Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);
|
neuper@37969
|
390 |
(*val t = rule2stac [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
|
neuper@37906
|
391 |
atomt t; term2str t;
|
neuper@37906
|
392 |
val t = rule2stac calclist (Calc ("op +", eval_binop "#add_"));
|
neuper@37906
|
393 |
atomt t; term2str t;
|
neuper@37906
|
394 |
val t = rule2stac [] (Rls_ rearrange_assoc);
|
neuper@37906
|
395 |
atomt t; term2str t;
|
neuper@37906
|
396 |
*)
|
neuper@37906
|
397 |
fun rule2stac_inst _ (Thm (thmID, _)) =
|
neuper@37906
|
398 |
Try $ (Repeat $ (Rew_Inst $ Subs $ Free (thmID, IDtype) $
|
neuper@37906
|
399 |
HOLogic.false_const))
|
neuper@37906
|
400 |
| rule2stac_inst calc (Calc (c, _)) =
|
neuper@37906
|
401 |
Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
|
neuper@37906
|
402 |
| rule2stac_inst calc (Cal1 (c, _)) =
|
neuper@37906
|
403 |
Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
|
neuper@37906
|
404 |
| rule2stac_inst _ (Rls_ rls) =
|
neuper@37906
|
405 |
Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $
|
neuper@37906
|
406 |
HOLogic.false_const);
|
neuper@37969
|
407 |
(*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
|
neuper@37906
|
408 |
atomt t; term2str t;
|
neuper@37906
|
409 |
val t = rule2stac_inst calclist (Calc ("op +", eval_binop "#add_"));
|
neuper@37906
|
410 |
atomt t; term2str t;
|
neuper@37906
|
411 |
val t = rule2stac_inst [] (Rls_ rearrange_assoc);
|
neuper@37906
|
412 |
atomt t; term2str t;
|
neuper@37906
|
413 |
*)
|
neuper@37906
|
414 |
|
neuper@37906
|
415 |
(*for appropriate nesting take stacs in _reverse_ order*)
|
neuper@37906
|
416 |
fun @@@ sts [s] = SEq $ s $ sts
|
neuper@37906
|
417 |
| @@@ sts (s::ss) = @@@ (SEq $ s $ sts) ss;
|
neuper@37906
|
418 |
fun @@ [stac] = stac
|
neuper@37906
|
419 |
| @@ [s1, s2] = SEq $ s1 $ s2 (*---------vvv--*)
|
neuper@37906
|
420 |
| @@ stacs =
|
neuper@37906
|
421 |
let val s3::s2::ss = rev stacs
|
neuper@37906
|
422 |
in @@@ (SEq $ s2 $ s3) ss end;
|
neuper@37906
|
423 |
(*
|
neuper@37906
|
424 |
val rules = (#rules o rep_rls) isolate_root;
|
neuper@37906
|
425 |
val rs = map (rule2stac calclist) rules;
|
neuper@37906
|
426 |
val tt = @@ rs;
|
neuper@37906
|
427 |
atomt tt; writeln (term2str tt);
|
neuper@37906
|
428 |
*)
|
neuper@37906
|
429 |
|
neuper@37906
|
430 |
val contains_bdv = (not o null o (filter is_bdv) o ids2str o #prop o rep_thm);
|
neuper@37906
|
431 |
|
neuper@37906
|
432 |
(*.does a rule contain a 'bdv'; descend recursively into Rls_.*)
|
neuper@37906
|
433 |
fun contain_bdv [] = false
|
neuper@37906
|
434 |
| contain_bdv (Thm (_, thm)::rs) =
|
neuper@37906
|
435 |
if (not o contains_bdv) thm
|
neuper@37906
|
436 |
then contain_bdv rs
|
neuper@37906
|
437 |
else true
|
neuper@37906
|
438 |
| contain_bdv (Calc _ ::rs) = contain_bdv rs
|
neuper@37906
|
439 |
| contain_bdv (Cal1 _ ::rs) = contain_bdv rs
|
neuper@37906
|
440 |
| contain_bdv (Rls_ rls ::rs) =
|
neuper@37906
|
441 |
contain_bdv (get_rules rls) orelse contain_bdv rs
|
neuper@37906
|
442 |
| contain_bdv (r::_) =
|
neuper@37906
|
443 |
raise error ("contain_bdv called with ["^(id_rule r)^",...]");
|
neuper@37906
|
444 |
|
neuper@37923
|
445 |
fun rules2scr_Rls calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
|
neuper@37906
|
446 |
if contain_bdv rules
|
neuper@37906
|
447 |
then ScrStep_inst $ Term $ Bdv $
|
neuper@37921
|
448 |
(Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ e_term))
|
neuper@37906
|
449 |
else ScrStep $ Term $
|
neuper@37921
|
450 |
(Repeat $ (((@@ o (map (rule2stac calc))) rules) $ e_term));
|
neuper@37906
|
451 |
(* val (calc, rules) = (!calclist', rules);
|
neuper@37906
|
452 |
*)
|
neuper@37923
|
453 |
fun rules2scr_Seq calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
|
neuper@37906
|
454 |
if contain_bdv rules
|
neuper@37906
|
455 |
then ScrStep_inst $ Term $ Bdv $
|
neuper@37921
|
456 |
(((@@ o (map (rule2stac_inst calc))) rules) $ e_term)
|
neuper@37906
|
457 |
else ScrStep $ Term $
|
neuper@37921
|
458 |
(((@@ o (map (rule2stac calc))) rules) $ e_term);
|
neuper@37906
|
459 |
|
neuper@37906
|
460 |
(*.prepare the input for an rls for use:
|
neuper@37906
|
461 |
# generate a script for stepwise execution of the rls
|
neuper@37906
|
462 |
# filter the operators for Calc out of the script
|
neuper@37906
|
463 |
!!!use this function in ruleset' := !!! .*)
|
neuper@37906
|
464 |
fun prep_rls Erls = raise error "prep_rls not impl. for Erls"
|
neuper@37906
|
465 |
| prep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,rules,...}) =
|
neuper@37906
|
466 |
let val sc = (rules2scr_Rls (!calclist') rules)
|
neuper@37906
|
467 |
in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
|
neuper@37906
|
468 |
srls=srls,
|
neuper@37906
|
469 |
calc = (*FIXXXME.040207 use also for met*)
|
neuper@37906
|
470 |
((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
|
neuper@37906
|
471 |
(filter is_calc) o stacpbls) sc,
|
neuper@37906
|
472 |
rules=rules,
|
neuper@37906
|
473 |
scr = Script sc} end
|
neuper@37906
|
474 |
(* val (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) = add_new_c;
|
neuper@37906
|
475 |
*)
|
neuper@37906
|
476 |
| prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) =
|
neuper@37906
|
477 |
let val sc = (rules2scr_Seq (!calclist') rules)
|
neuper@37906
|
478 |
in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
|
neuper@37906
|
479 |
srls=srls,
|
neuper@37906
|
480 |
calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
|
neuper@37906
|
481 |
(filter is_calc) o stacpbls) sc,
|
neuper@37906
|
482 |
rules=rules,
|
neuper@37906
|
483 |
scr = Script sc} end
|
neuper@37906
|
484 |
| prep_rls (Rrls {id,...}) =
|
neuper@37906
|
485 |
raise error ("prep_rls not required for Rrls \""^id^"\"");
|
neuper@37906
|
486 |
(*
|
neuper@37906
|
487 |
val Script sc = (#scr o rep_rls o prep_rls) isolate_root;
|
neuper@37906
|
488 |
(writeln o term2str) sc;
|
neuper@37906
|
489 |
val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv;
|
neuper@37906
|
490 |
(writeln o term2str) sc;
|
neuper@37906
|
491 |
*)
|