1 (* tools which depend on Script.thy and thus are not in termC.sml
2 (c) Walther Neuper 2000
5 signature LANGUAGE_TOOLS =
7 datatype stacexpr = Expr of term | STac of term
8 val rep_stacexpr: stacexpr -> term
9 val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * stacexpr
10 val contain_bdv: Celem.rule list -> bool
11 val contains_bdv: thm -> bool
12 type env = (term * term) list
13 val upd_env: env -> term * term -> env
14 val is_booll_dsc: term -> bool
15 val is_calc: term -> bool
16 val is_dsc: term -> bool
17 val is_list_dsc: term -> bool
18 val is_reall_dsc: term -> bool
19 val is_unl: term -> bool
20 val pblterm: Celem.domID -> Celem.pblID -> term
21 val subpbl: string -> string list -> term
22 val stacpbls: term -> term list
23 val one_scr_arg: term -> term
24 val two_scr_arg: term -> term * term
25 val op_of_calc: term -> string
26 val get_calcs: theory -> term -> (Celem.prog_calcID * (Celem.calID * Celem.eval_fn)) list
27 val prep_rls: theory -> Celem.rls -> Celem.rls
28 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
30 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
31 val rule2stac: theory -> Celem.rule -> term
32 val rule2stac_inst: theory -> Celem.rule -> term
33 val @@ : term list -> term
34 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
38 structure LTool(**): LANGUAGE_TOOLS(**) =
42 (* distinguish input to Model (deep embedding of terms as Isac's object language) *)
43 fun is_reall_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]), _]))) = true
44 | is_reall_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]),_])) $ _) = true
45 | is_reall_dsc _ = false;
46 fun is_booll_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _]))) = true
47 | is_booll_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("HOL.bool", [])]),_])) $ _) = true
48 | is_booll_dsc _ = false;
49 fun is_list_dsc (Const (_, Type("fun", [Type("List.list", _), _]))) = true
50 | is_list_dsc (Const (_, Type("fun", [Type("List.list", _), _])) $ _) = true
51 (*WN:8.5.03: ??? TODO test/../scrtools.sml ~~~~ ???*)
52 | is_list_dsc _ = false;
53 fun is_unl (Const (_, Type("fun", [_, Type("Tools.unl", _)]))) = true
55 fun is_dsc (Const(_, Type("fun", [_, Type ("Tools.nam",_)]))) = true
56 | is_dsc (Const(_, Type("fun", [_, Type ("Tools.una",_)]))) = true
57 | is_dsc (Const(_, Type("fun", [_, Type ("Tools.unl",_)]))) = true
58 | is_dsc (Const(_, Type("fun", [_, Type ("Tools.str",_)]))) = true
59 | is_dsc (Const(_, Type("fun", [_, Type ("Tools.toreal",_)]))) = true
60 | is_dsc (Const(_, Type("fun", [_, Type ("Tools.toreall",_)])))= true
61 | is_dsc (Const(_, Type("fun", [_, Type ("Tools.tobooll",_)])))= true
62 | is_dsc (Const(_, Type("fun", [_, Type ("Tools.unknow",_)])))= true
63 | is_dsc (Const(_, Type("fun", [_, Type ("Tools.cpy",_)])))= true
67 (* make the term 'Subproblem (domID, pblID)' to a formula for frontend;
68 needs to be here after def. Subproblem in Script.thy *)
69 val subpbl_t $ (pair_t $ Free (_, _) $ _) =
70 (Thm.term_of o the o (TermC.parse @{theory Script})) "Subproblem (Isac,[equation,univar])"
72 (Thm.term_of o the o (TermC.parse @{theory Script})) "Problem (Isac,[equation,univar])"
73 val Free (_, ID_type) = (Thm.term_of o the o (TermC.parse @{theory Script})) "xxx::ID"
75 fun subpbl domID pblID =
76 subpbl_t $ (pair_t $ Free (domID, ID_type) $
77 (((TermC.list2isalist ID_type) o (map (TermC.mk_free ID_type))) pblID));
78 fun pblterm domID pblID =
79 pbl_t $ (pair_t $ Free (domID,ID_type) $
80 (((TermC.list2isalist ID_type) o (map (TermC.mk_free ID_type))) pblID));
82 (* construct scr-env from scr(created automatically) and Rewrite_Set *)
83 fun one_scr_arg (Const _ $ arg $ _) = arg
84 | one_scr_arg t = error ("one_scr_arg: called by " ^ Celem.term2str t);
85 fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2)
86 | two_scr_arg t = error ("two_scr_arg: called by " ^ Celem.term2str t);
89 (** generate a "type calc" from a script **)
91 (* instantiate a stactic or scriptexpr, and ev. attach (curried) argument
94 v current value, is attached to curried stactics
95 stac stactic to be instantiated
97 not (a = NONE) /\ (v = e_term) /\ (stac curried, i.e. without last arg.)
98 this ........................ is the initialization for assy with l=[],
100 (a) curried: then (a = SOME _), or
101 (b) not curried: then the values of the initialization are not used
103 datatype stacexpr = STac of term | Expr of term
104 fun rep_stacexpr (STac t ) = t
105 | rep_stacexpr (Expr t) =
106 error ("rep_stacexpr called with t= " ^ Celem.term2str t);
108 type env = (term * term) list;
110 (* update environment; t <> empty if coming from listexpr *)
111 fun upd_env (env:env) (v,t) =
112 let val env' = if t = Celem.e_term then env else overwrite (env,(v,t));
115 (* substitute the script's environment in a leaf of the script's parse-tree
116 and attach the curried argument of a tactic, if any.
117 a leaf is either a tactic or an 'exp' in 'let v = expr'
118 where 'exp' does not contain a tactic.
119 CAUTION: (1) currying with @@ requires 2 patterns for each tactic
120 (2) the non-curried version must return NONE for a
121 (3) non-matching patterns become an Expr by fall-through.
122 WN060906 quick and dirty fix: due to (2) a is returned, too *)
123 fun subst_stacexpr E _ _ (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _)) =
124 (NONE, STac (subst_atomic E t))
125 | subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _)) =
126 (a, (*in these cases we hope, that a = SOME _*)
127 STac (case a of SOME a' => (subst_atomic E (t $ a'))
128 | NONE => ((subst_atomic E t) $ v)))
129 | subst_stacexpr E _ _
130 (t as (Const ("Script.Rewrite'_Inst", _) $ _ $ _ $ _ $ _)) =
131 (NONE, STac (subst_atomic E t))
132 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst", _) $ _ $ _ $ _)) =
133 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
134 | NONE => ((subst_atomic E t) $ v)))
135 | subst_stacexpr E _ _ (t as (Const ("Script.Rewrite'_Set", _) $ _ $ _ $ _)) =
136 (NONE, STac (subst_atomic E t))
137 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set", _) $ _ $ _)) =
138 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
139 | NONE => ((subst_atomic E t) $ v)))
140 | subst_stacexpr E _ _
141 (t as (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ _ $ _ $ _)) =
142 (NONE, STac (subst_atomic E t))
143 | subst_stacexpr E a v
144 (t as (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ _ $ _)) =
145 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
146 | NONE => ((subst_atomic E t) $ v)))
147 | subst_stacexpr E _ _ (t as (Const ("Script.Calculate", _) $ _ $ _)) =
148 (NONE, STac (subst_atomic E t))
149 | subst_stacexpr E a v (t as (Const ("Script.Calculate", _) $ _)) =
150 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
151 | NONE => ((subst_atomic E t) $ v)))
152 | subst_stacexpr E _ _
153 (t as (Const ("Script.Check'_elementwise",_) $ _ $ _)) =
154 (NONE, STac (subst_atomic E t))
155 | subst_stacexpr E a v (t as (Const ("Script.Check'_elementwise", _) $ _)) =
156 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
157 | NONE => ((subst_atomic E t) $ v)))
158 | subst_stacexpr E _ _ (t as (Const ("Script.Or'_to'_List", _) $ _)) =
159 (NONE, STac (subst_atomic E t))
160 | subst_stacexpr E a v (t as (Const ("Script.Or'_to'_List", _))) = (*t $ v*)
161 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
162 | NONE => ((subst_atomic E t) $ v)))
163 | subst_stacexpr E _ _ (t as (Const ("Script.SubProblem", _) $ _ $ _)) =
164 (NONE, STac (subst_atomic E t))
165 | subst_stacexpr E _ _ (t as (Const ("Script.Take",_) $ _)) =
166 (NONE, STac (subst_atomic E t))
167 | subst_stacexpr E _ _ (t as (Const ("Script.Substitute", _) $ _ $ _)) =
168 (NONE, STac (subst_atomic E t))
169 | subst_stacexpr E a v (t as (Const ("Script.Substitute", _) $ _)) =
170 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
171 | NONE => ((subst_atomic E t) $ v)))
172 (*now all tactics are matched out and this leaf must be without a tactic*)
173 | subst_stacexpr E a v t =
174 (a, Expr (subst_atomic (case a of SOME a => upd_env E (a,v)
177 (* fetch tactics from a program omitting tacticals like While, Repeat,.. *)
178 fun stacpbls (_ $ body) =
180 fun scan (Const ("HOL.Let", _) $ e $ (Abs (_, _, b))) = (scan e) @ (scan b)
181 | scan (Const ("If", _) $ _ $ e1 $ e2) = (scan e1) @ (scan e2)
182 | scan (Const ("Script.While", _) $ _ $ e $ _) = scan e
183 | scan (Const ("Script.While", _) $ _ $ e) = scan e
184 | scan (Const ("Script.Repeat", _) $ e $ _) = scan e
185 | scan (Const ("Script.Repeat", _) $ e) = scan e
186 | scan (Const ("Script.Try", _) $ e $ _) = scan e
187 | scan (Const ("Script.Try", _) $ e) = scan e
188 | scan (Const ("Script.Or", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
189 | scan (Const ("Script.Or", _) $ e1 $ e2) = (scan e1) @ (scan e2)
190 | scan (Const ("Script.Seq", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
191 | scan (Const ("Script.Seq", _) $ e1 $ e2) = (scan e1) @ (scan e2)
192 | scan t = case subst_stacexpr [] NONE Celem.e_term t of
193 (_, STac _) => [t] | (_, Expr _) => []
194 in (distinct o scan) body end
195 | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ Celem.term2str t ^ "'")
197 (* get operators out of a program *)
198 fun is_calc (Const ("Script.Calculate",_) $ _) = true
199 | is_calc (Const ("Script.Calculate",_) $ _ $ _) = true
201 fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_
202 | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_
203 | op_of_calc t = error ("op_of_calc called with" ^ Celem.term2str t);
204 fun get_calcs thy sc =
209 |> (assoc_calc' thy |> map);
211 (** build up a program from rules **)
213 (* transform type rule to a term *)
214 val ScrStep $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory}))
215 (*'z not affected by parse: 'a --> real*)
216 "Script Stepwise (t_t::'z) =\
218 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
219 \ (Try (Repeat (Rewrite add_commute False))) @@ \
220 \ (Try (Repeat (Rewrite mult_commute False)))) \
222 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body are inconsistent !!!*)
223 val ScrStep_inst $ Term $ Bdv $ _= (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory}))
224 (*'z not affected by parse: 'a --> real*)
225 "Script Stepwise_inst (t_t::'z) (v::real) =\
227 \ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \
228 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] add_commute False))) @@\
229 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] mult_commute False)))) \
231 val Repeat $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
232 "Repeat (Rewrite real_diff_minus False t)";
233 val Try $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
234 "Try (Rewrite real_diff_minus False t)";
235 val Cal $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
237 val Ca1 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
239 val Rew $ (Free (_, IDtype)) $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
240 "Rewrite real_diff_minus False t";
241 val Rew_Inst $ Subs $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
242 "Rewrite_Inst [(bdv,v)] real_diff_minus False";
243 val Rew_Set $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
244 "Rewrite_Set real_diff_minus False";
245 val Rew_Set_Inst $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
246 "Rewrite_Set_Inst [(bdv,v)] real_diff_minus False";
247 val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
248 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
249 \ (Try (Repeat (Rewrite add_commute False))) @@ \
250 \ (Try (Repeat (Rewrite mult_commute False)))) t";
252 fun rule2stac _ (Celem.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ @{term False}))
253 | rule2stac thy (Celem.Calc (c, _)) = Try $ (Repeat $ (Cal $ Free (assoc_calc thy c, IDtype)))
254 | rule2stac thy (Celem.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ Free (assoc_calc thy c, IDtype)))
255 | rule2stac _ (Celem.Rls_ rls) = Try $ (Rew_Set $ Free (Celem.id_rls rls, IDtype) $ @{term False})
256 | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Celem.rule2str r ^ "\"");
257 fun rule2stac_inst _ (Celem.Thm (thmID, _)) =
258 Try $ (Repeat $ (Rew_Inst $ Subs $ Free (thmID, IDtype) $
260 | rule2stac_inst thy (Celem.Calc (c, _)) =
261 Try $ (Repeat $ (Cal $ Free (assoc_calc thy c, IDtype)))
262 | rule2stac_inst thy (Celem.Cal1 (c, _)) =
263 Try $ (Repeat $ (Cal $ Free (assoc_calc thy c, IDtype)))
264 | rule2stac_inst _ (Celem.Rls_ rls) =
265 Try $ (Rew_Set_Inst $ Subs $ Free (Celem.id_rls rls, IDtype) $
267 | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Celem.rule2str r ^ "\"");
269 (*for appropriate nesting take stacs in _reverse_ order*)
270 fun op @@@ sts [s] = SEq $ s $ sts
271 | op @@@ sts (s::ss) = op @@@ (SEq $ s $ sts) ss
273 raise ERROR ("fun @@@ not applicable to \"" ^ Celem.term2str t ^ "\" \"" ^ Celem.terms2str ts ^ "\"");
275 | @@ [s1, s2] = SEq $ s1 $ s2
276 | @@ stacs = case rev stacs of
277 s3 :: s2 :: ss => op @@@ (SEq $ s2 $ s3) ss
278 | ts => raise ERROR ("fun @@ not applicable to \"" ^ Celem.terms2str ts ^ "\"")
280 val contains_bdv = (not o null o (filter TermC.is_bdv) o TermC.ids2str o #prop o Thm.rep_thm);
282 (* does a rule contain a 'bdv'; descend recursively into Rls_ *)
283 fun contain_bdv [] = false
284 | contain_bdv (Celem.Thm (_, thm) :: rs) =
285 if (not o contains_bdv) thm
288 | contain_bdv (Celem.Calc _ :: rs) = contain_bdv rs
289 | contain_bdv (Celem.Cal1 _ :: rs) = contain_bdv rs
290 | contain_bdv (Celem.Rls_ rls :: rs) =
291 contain_bdv (Celem.get_rules rls) orelse contain_bdv rs
292 | contain_bdv (r :: _) =
293 error ("contain_bdv called with [" ^ Celem.id_rule r ^ ",...]");
295 fun rules2scr_Rls thy rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
297 then ScrStep_inst $ Term $ Bdv $ (Repeat $ (((@@ o (map (rule2stac_inst thy))) rules) $ Celem.e_term))
298 else ScrStep $ Term $ (Repeat $ (((@@ o (map (rule2stac thy))) rules) $ Celem.e_term));
299 fun rules2scr_Seq thy rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
301 then ScrStep_inst $ Term $ Bdv $
302 (((@@ o (map (rule2stac_inst thy))) rules) $ Celem.e_term)
303 else ScrStep $ Term $
304 (((@@ o (map (rule2stac thy))) rules) $ Celem.e_term);
306 (* prepare the input for an rls for use:
307 # generate a script for stepwise execution of the rls
308 # filter the operators for Calc out of the script ?WN111014?
309 !!!use this function while storing (TODO integrate..) into KEStore_Elems.add_rlss *)
310 fun prep_rls _ Celem.Erls = error "prep_rls: not required for Erls"
311 | prep_rls thy (Celem.Rls {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
312 let val sc = (rules2scr_Rls thy rules)
313 in Celem.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls,
315 calc = get_calcs thy sc,
318 scr = Celem.Prog sc} end
319 | prep_rls thy (Celem.Seq {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
320 let val sc = (rules2scr_Seq thy rules)
321 in Celem.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls,
323 calc = get_calcs thy sc,
326 scr = Celem.Prog sc} end
327 | prep_rls _ (Celem.Rrls {id, ...}) =
328 error ("prep_rls: not required for Rrls \"" ^ id ^ "\"");