1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,491 @@
1.4 +(* tools which depend on Script.thy and thus are not in term.sml
1.5 + (c) Walther Neuper 2000
1.6 +
1.7 +use"ProgLang/scrtools.sml";
1.8 +use"scrtools.sml";
1.9 +*)
1.10 +
1.11 +
1.12 +fun is_reall_dsc
1.13 + (Const(_,Type("fun",[Type("List.list",
1.14 + [Type ("real",[])]),_]))) = true
1.15 + | is_reall_dsc
1.16 + (Const(_,Type("fun",[Type("List.list",
1.17 + [Type ("real",[])]),_])) $ t) = true
1.18 + | is_reall_dsc _ = false;
1.19 +fun is_booll_dsc
1.20 + (Const(_,Type("fun",[Type("List.list",
1.21 + [Type ("bool",[])]),_]))) = true
1.22 + | is_booll_dsc
1.23 + (Const(_,Type("fun",[Type("List.list",
1.24 + [Type ("bool",[])]),_])) $ t) = true
1.25 + | is_booll_dsc _ = false;
1.26 +(*
1.27 +> val t = (term_of o the o (parse thy)) "relations";
1.28 +> atomtyp (type_of t);
1.29 +*** Type (fun,[
1.30 +*** Type (List.list,[
1.31 +*** Type (bool,[])
1.32 +*** ]
1.33 +*** Type (Tools.una,[])
1.34 +*** ]
1.35 +> is_booll_dsc t;
1.36 +val it = true : bool
1.37 +> is_reall_dsc t;
1.38 +val it = false : bool
1.39 +*)
1.40 +
1.41 +fun is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_]))) = true
1.42 + | is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_])) $ t) = true
1.43 + (*WN:8.5.03: ??? ~~~~ ???*)
1.44 + | is_list_dsc _ = false;
1.45 +(*
1.46 +> val t = str2term "someList";
1.47 +> is_list_dsc t;
1.48 +val it = true : bool
1.49 +
1.50 +> val t = (term_of o the o (parse thy))
1.51 + "additional_relations [a=b,c=(d::real)]";
1.52 +> is_list_dsc t;
1.53 +val it = true : bool
1.54 +> is_list_dsc (head_of t);
1.55 +val it = true : bool
1.56 +
1.57 +> val t = (term_of o the o (parse thy))"max_relation (A=#2*a*b-a^^^#2)";
1.58 +> is_list_dsc t;
1.59 +val it = false : bool
1.60 +> is_list_dsc (head_of t);
1.61 +val it = false : bool
1.62 +> val t = (term_of o the o (parse thy)) "testdscforlist";
1.63 +> is_list_dsc (head_of t);
1.64 +val it = true : bool
1.65 +*)
1.66 +
1.67 +
1.68 +fun is_unl (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true
1.69 + | is_unl _ = false;
1.70 +(*
1.71 +> val t = str2term "someList"; is_unl t;
1.72 +val it = true : bool
1.73 +> val t = (term_of o the o (parse thy)) "maximum";
1.74 +> is_unl t;
1.75 +val it = false : bool
1.76 +*)
1.77 +
1.78 +fun is_dsc (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) = true
1.79 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.una",_)]))) = true
1.80 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true
1.81 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.str",_)]))) = true
1.82 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) = true
1.83 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))= true
1.84 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.tobooll",_)])))= true
1.85 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.unknow",_)])))= true
1.86 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.cpy",_)])))= true
1.87 + | is_dsc _ = false;
1.88 +fun is_dsc term =
1.89 + (case (range_type o type_of) term of
1.90 + Type("Tools.nam",_) => true
1.91 + | Type("Tools.una",_) => true
1.92 + | Type("Tools.unl",_) => true
1.93 + | Type("Tools.str",_) => true
1.94 + | Type("Tools.toreal",_) => true
1.95 + | Type("Tools.toreall",_) => true
1.96 + | Type("Tools.tobooll",_) => true
1.97 + | Type("Tools.unknow",_) => true
1.98 + | Type("Tools.cpy",_) => true
1.99 + | _ => false)
1.100 + handle Match => false;
1.101 +
1.102 +
1.103 +(*
1.104 +val t as t1 $ t2 = str2term "antiDerivativeName M_b";
1.105 +val Const (_, Type ("fun", [Type ("fun", _), Type ("Tools.una",[])])) $ _ = t;
1.106 +is_dsc t1;
1.107 +
1.108 +> val t = (term_of o the o (parse thy)) "maximum";
1.109 +> is_dsc t;
1.110 +val it = true : bool
1.111 +> val t = (term_of o the o (parse thy)) "testdscforlist";
1.112 +> is_dsc t;
1.113 +val it = true : bool
1.114 +
1.115 +> val t = (head_of o term_of o the o (parse thy)) "maximum A";
1.116 +> is_dsc t;
1.117 +val it = true : bool
1.118 +> val t = (head_of o term_of o the o (parse thy))
1.119 + "fixedValues [R=(R::real)]";
1.120 +> is_dsc t;
1.121 +val it = true : bool
1.122 +*)
1.123 +
1.124 +
1.125 +(*make the term 'Subproblem (domID, pblID)' to a formula for frontend;
1.126 + needs to be here after def. Subproblem in Script.thy*)
1.127 +val t as (subpbl_t $ (pair_t $ Free (domID,_) $ pblID)) =
1.128 + (term_of o the o (parse @{theory Script}))
1.129 + "Subproblem (Isac,[equation,univar])";
1.130 +val t as (pbl_t $ _) =
1.131 + (term_of o the o (parse @{theory Script}))
1.132 + "Problem (Isac,[equation,univar])";
1.133 +val Free (_, ID_type) = (term_of o the o (parse @{theory Script})) "x::ID";
1.134 +
1.135 +
1.136 +fun subpbl domID pblID =
1.137 + subpbl_t $ (pair_t $ Free (domID,ID_type) $
1.138 + (((list2isalist ID_type) o (map (mk_free ID_type))) pblID));
1.139 +(*> subpbl "Isac" ["equation","univar"] = t;
1.140 +val it = true : bool *)
1.141 +
1.142 +
1.143 +fun pblterm (domID:domID) (pblID:pblID) =
1.144 + pbl_t $ (pair_t $ Free (domID,ID_type) $
1.145 + (((list2isalist ID_type) o (map (mk_free ID_type))) pblID));
1.146 +
1.147 +
1.148 +(**.construct scr-env from scr(created automatically) and Rewrite_Set.**)
1.149 +
1.150 +fun one_scr_arg (Const _ $ arg $ _) = arg
1.151 + | one_scr_arg t = raise error ("one_scr_arg: called by "^(term2str t));
1.152 +fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2)
1.153 + | two_scr_arg t = raise error ("two_scr_arg: called by "^(term2str t));
1.154 +
1.155 +
1.156 +(**.generate calc from a script.**)
1.157 +
1.158 +(*.instantiate a stactic or scriptexpr, and ev. attach (curried) argument
1.159 +args:
1.160 + E environment
1.161 + v current value, is attached to curried stactics
1.162 + stac stactic to be instantiated
1.163 +precond:
1.164 + not (a = NONE) /\ (v = e_term) /\ (stac curried, i.e. without last arg.)
1.165 + this ........................ is the initialization for assy with l=[],
1.166 + but the 1st stac is
1.167 + (a) curried: then (a = SOME _), or
1.168 + (b) not curried: then the values of the initialization are not used
1.169 +.*)
1.170 +datatype stacexpr = STac of term | Expr of term
1.171 +fun rep_stacexpr (STac t ) = t
1.172 + | rep_stacexpr (Expr t) =
1.173 + raise error ("rep_stacexpr called with t= "^(term2str t));
1.174 +
1.175 +type env = (term * term) list;
1.176 +
1.177 +(*update environment; t <> empty if coming from listexpr*)
1.178 +fun upd_env (env:env) (v,t) =
1.179 + let val env' = if t = e_term then env else overwrite (env,(v,t));
1.180 + (*val _= writeln("### upd_env: = "^(subst2str env'));*)
1.181 + in env' end;
1.182 +
1.183 +(*.substitute the scripts environment in a leaf of the scripts parse-tree
1.184 + and attach the curried argument of a tactic, if any.
1.185 + a leaf is either a tactic or an 'exp' in 'let v = expr'
1.186 + where 'exp' does not contain a tactic.
1.187 +CAUTION: (1) currying with @@ requires 2 patterns for each tactic
1.188 + (2) the non-curried version must return NONE for a
1.189 + (3) non-matching patterns become an Expr by fall-through.
1.190 +WN060906 quick and dirty fix: due to (2) a is returned, too.*)
1.191 +fun subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=
1.192 + (NONE, STac (subst_atomic E t))
1.193 +
1.194 + | subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))=
1.195 + (a, (*in these cases we hope, that a = SOME _*)
1.196 + STac (case a of SOME a' => (subst_atomic E (t $ a'))
1.197 + | NONE => ((subst_atomic E t) $ v)))
1.198 +
1.199 + | subst_stacexpr E a v
1.200 + (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ _ )) =
1.201 + (NONE, STac (subst_atomic E t))
1.202 +
1.203 + | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _))=
1.204 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
1.205 + | NONE => ((subst_atomic E t) $ v)))
1.206 +
1.207 + | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ ))=
1.208 + (NONE, STac (subst_atomic E t))
1.209 +
1.210 + | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) =
1.211 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
1.212 + | NONE => ((subst_atomic E t) $ v)))
1.213 +
1.214 + | subst_stacexpr E a v
1.215 + (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ _ )) =
1.216 + (NONE, STac (subst_atomic E t))
1.217 +
1.218 + | subst_stacexpr E a v
1.219 + (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )) =
1.220 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
1.221 + | NONE => ((subst_atomic E t) $ v)))
1.222 +
1.223 + | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) =
1.224 + (NONE, STac (subst_atomic E t))
1.225 +
1.226 + | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ )) =
1.227 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
1.228 + | NONE => ((subst_atomic E t) $ v)))
1.229 +
1.230 + | subst_stacexpr E a v
1.231 + (t as (Const("Script.Check'_elementwise",_) $ _ $ _ )) =
1.232 + (NONE, STac (subst_atomic E t))
1.233 +
1.234 + | subst_stacexpr E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) =
1.235 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
1.236 + | NONE => ((subst_atomic E t) $ v)))
1.237 +
1.238 + | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) =
1.239 + (NONE, STac (subst_atomic E t))
1.240 +
1.241 + | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*)
1.242 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
1.243 + | NONE => ((subst_atomic E t) $ v)))
1.244 +
1.245 + | subst_stacexpr E a v (t as (Const ("Script.SubProblem",_) $ _ $ _ )) =
1.246 + (NONE, STac (subst_atomic E t))
1.247 +
1.248 + | subst_stacexpr E a v (t as (Const ("Script.Take",_) $ _ )) =
1.249 + (NONE, STac (subst_atomic E t))
1.250 +
1.251 + | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ $ _ )) =
1.252 + (NONE, STac (subst_atomic E t))
1.253 +
1.254 + | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ )) =
1.255 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
1.256 + | NONE => ((subst_atomic E t) $ v)))
1.257 +
1.258 + (*now all tactics are matched out and this leaf must be without a tactic*)
1.259 + | subst_stacexpr E a v t =
1.260 + (a, Expr (subst_atomic (case a of SOME a => upd_env E (a,v)
1.261 + | NONE => E) t));
1.262 +(*> val t = str2term "SubProblem(Test_, [linear, univariate, equation, test], [Test, solve_linear]) [bool_ e_, real_ v_]";
1.263 +> subst_stacexpr [] NONE e_term t;*)
1.264 +
1.265 +
1.266 +fun stacpbls (h $ body) =
1.267 + let
1.268 + fun scan ts (Const ("Let",_) $ e $ (Abs (v,T,b))) =
1.269 + (scan ts e) @ (scan ts b)
1.270 + | scan ts (Const ("If",_) $ c $ e1 $ e2) = (scan ts e1) @ (scan ts e2)
1.271 + | scan ts (Const ("Script.While",_) $ c $ e $ _) = scan ts e
1.272 + | scan ts (Const ("Script.While",_) $ c $ e) = scan ts e
1.273 + | scan ts (Const ("Script.Repeat",_) $ e $ _) = scan ts e
1.274 + | scan ts (Const ("Script.Repeat",_) $ e) = scan ts e
1.275 + | scan ts (Const ("Script.Try",_) $ e $ _) = scan ts e
1.276 + | scan ts (Const ("Script.Try",_) $ e) = scan ts e
1.277 + | scan ts (Const ("Script.Or",_) $e1 $ e2 $ _) =
1.278 + (scan ts e1) @ (scan ts e2)
1.279 + | scan ts (Const ("Script.Or",_) $e1 $ e2) =
1.280 + (scan ts e1) @ (scan ts e2)
1.281 + | scan ts (Const ("Script.Seq",_) $e1 $ e2 $ _) =
1.282 + (scan ts e1) @ (scan ts e2)
1.283 + | scan ts (Const ("Script.Seq",_) $e1 $ e2) =
1.284 + (scan ts e1) @ (scan ts e2)
1.285 + | scan ts t = case subst_stacexpr [] NONE e_term t of
1.286 + (_, STac _) => [t] | (_, Expr _) => []
1.287 + in (distinct o (scan [])) body end;
1.288 + (*sc = Solve_root_equation ...
1.289 +> val ts = stacpbls sc;
1.290 +> writeln (terms2str thy ts);
1.291 +["Rewrite square_equation_left True e_",
1.292 + "Rewrite_Set SqRoot_simplify False e_",
1.293 + "Rewrite_Set rearrange_assoc False e_",
1.294 + "Rewrite_Set isolate_root False e_",
1.295 + "Rewrite_Set norm_equation False e_",
1.296 + "Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False e_"]
1.297 +*)
1.298 +
1.299 +
1.300 +
1.301 +fun is_calc (Const ("Script.Calculate",_) $ _) = true
1.302 + | is_calc (Const ("Script.Calculate",_) $ _ $ _) = true
1.303 + | is_calc _ = false;
1.304 +fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_
1.305 + | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_
1.306 + | op_of_calc t = raise error ("op_of_calc called with"^term2str t);
1.307 +(*
1.308 + val Script sc = (#scr o rep_rls) Test_simplify;
1.309 + val stacs = stacpbls sc;
1.310 +
1.311 + val calcs = filter is_calc stacs;
1.312 + val ids = map op_of_calc calcs;
1.313 + map (curry assoc1 (!calclist')) ids;
1.314 +
1.315 + (((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
1.316 + (filter is_calc) o stacpbls) sc):calc list;
1.317 +*)
1.318 +
1.319 +(**.for automatic creation of scripts from rls.**)
1.320 +(* naming of identifiers in scripts ???...
1.321 +((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t::'z) = t";
1.322 +((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o
1.323 + (parse @{theory})) "(t't::'z) = t't";
1.324 +((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_t::'z) = t_t";
1.325 +(* not accepted !!!...*)
1.326 +((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_::'z) = t_";
1.327 +((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o
1.328 + (parse @{theory})) "(_t::'z) = _t";
1.329 +*)
1.330 +((inst_abs @{theory}) o term_of o the o (parse @{theory}))
1.331 +"Script Stepwise (t::'z) =\
1.332 + \(Repeat\
1.333 + \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
1.334 + \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
1.335 + \ (Try (Repeat (Rewrite real_mult_commute False)))) \
1.336 + \ t_t)";
1.337 +val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*)
1.338 + ((inst_abs @{theory}) o term_of o the o (parse @{theory}))
1.339 + "Script Stepwise (t::'z) =\
1.340 + \(Repeat\
1.341 + \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
1.342 + \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
1.343 + \ (Try (Repeat (Rewrite real_mult_commute False)))) \
1.344 + \ t_t)";
1.345 +(*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body
1.346 +are inconsistent !!!*)
1.347 +val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*)
1.348 + ((inst_abs @{theory}) o term_of o the o (parse @{theory}))
1.349 + "Script Stepwise_inst (t::'z) (v::real) =\
1.350 + \(Repeat\
1.351 + \ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \
1.352 + \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_add_commute False))) @@\
1.353 + \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \
1.354 + \ t)";
1.355 +val Repeat $ _ =
1.356 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
1.357 + "Repeat (Rewrite real_diff_minus False t)";
1.358 +val Try $ _ =
1.359 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
1.360 + "Try (Rewrite real_diff_minus False t)";
1.361 +val Cal $ _ =
1.362 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
1.363 + "Calculate PLUS";
1.364 +val Ca1 $ _ =
1.365 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
1.366 + "Calculate1 PLUS";
1.367 +val Rew $ (Free (_,IDtype)) $ _ $ t =
1.368 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
1.369 + "Rewrite real_diff_minus False t";
1.370 +val Rew_Inst $ Subs $ _ $ _ =
1.371 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
1.372 + "Rewrite_Inst [(bdv,v)] real_diff_minus False";
1.373 +val Rew_Set $ _ $ _ =
1.374 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
1.375 + "Rewrite_Set real_diff_minus False";
1.376 +val Rew_Set_Inst $ _ $ _ $ _ =
1.377 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
1.378 + "Rewrite_Set_Inst [(bdv,v)] real_diff_minus False";
1.379 +val SEq $ _ $ _ $ _ =
1.380 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
1.381 + " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
1.382 + \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
1.383 + \ (Try (Repeat (Rewrite real_mult_commute False)))) t";
1.384 +
1.385 +fun rule2stac _ (Thm (thmID, _)) =
1.386 + Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const))
1.387 + | rule2stac calc (Calc (c, _)) =
1.388 + Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
1.389 + | rule2stac calc (Cal1 (c, _)) =
1.390 + Try $ (Repeat $ (Ca1 $ Free (assoc_calc (calc ,c), IDtype)))
1.391 + | rule2stac _ (Rls_ rls) =
1.392 + Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);
1.393 +(*val t = rule2stac [] (Thm ("real_diff_minus", num_str real_diff_minus));
1.394 +atomt t; term2str t;
1.395 +val t = rule2stac calclist (Calc ("op +", eval_binop "#add_"));
1.396 +atomt t; term2str t;
1.397 +val t = rule2stac [] (Rls_ rearrange_assoc);
1.398 +atomt t; term2str t;
1.399 +*)
1.400 +fun rule2stac_inst _ (Thm (thmID, _)) =
1.401 + Try $ (Repeat $ (Rew_Inst $ Subs $ Free (thmID, IDtype) $
1.402 + HOLogic.false_const))
1.403 + | rule2stac_inst calc (Calc (c, _)) =
1.404 + Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
1.405 + | rule2stac_inst calc (Cal1 (c, _)) =
1.406 + Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
1.407 + | rule2stac_inst _ (Rls_ rls) =
1.408 + Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $
1.409 + HOLogic.false_const);
1.410 +(*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str real_diff_minus));
1.411 +atomt t; term2str t;
1.412 +val t = rule2stac_inst calclist (Calc ("op +", eval_binop "#add_"));
1.413 +atomt t; term2str t;
1.414 +val t = rule2stac_inst [] (Rls_ rearrange_assoc);
1.415 +atomt t; term2str t;
1.416 +*)
1.417 +
1.418 +(*for appropriate nesting take stacs in _reverse_ order*)
1.419 +fun @@@ sts [s] = SEq $ s $ sts
1.420 + | @@@ sts (s::ss) = @@@ (SEq $ s $ sts) ss;
1.421 +fun @@ [stac] = stac
1.422 + | @@ [s1, s2] = SEq $ s1 $ s2 (*---------vvv--*)
1.423 + | @@ stacs =
1.424 + let val s3::s2::ss = rev stacs
1.425 + in @@@ (SEq $ s2 $ s3) ss end;
1.426 +(*
1.427 + val rules = (#rules o rep_rls) isolate_root;
1.428 + val rs = map (rule2stac calclist) rules;
1.429 + val tt = @@ rs;
1.430 + atomt tt; writeln (term2str tt);
1.431 + *)
1.432 +
1.433 +val contains_bdv = (not o null o (filter is_bdv) o ids2str o #prop o rep_thm);
1.434 +
1.435 +(*.does a rule contain a 'bdv'; descend recursively into Rls_.*)
1.436 +fun contain_bdv [] = false
1.437 + | contain_bdv (Thm (_, thm)::rs) =
1.438 + if (not o contains_bdv) thm
1.439 + then contain_bdv rs
1.440 + else true
1.441 + | contain_bdv (Calc _ ::rs) = contain_bdv rs
1.442 + | contain_bdv (Cal1 _ ::rs) = contain_bdv rs
1.443 + | contain_bdv (Rls_ rls ::rs) =
1.444 + contain_bdv (get_rules rls) orelse contain_bdv rs
1.445 + | contain_bdv (r::_) =
1.446 + raise error ("contain_bdv called with ["^(id_rule r)^",...]");
1.447 +
1.448 +fun rules2scr_Rls calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
1.449 + if contain_bdv rules
1.450 + then ScrStep_inst $ Term $ Bdv $
1.451 + (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ e_term))
1.452 + else ScrStep $ Term $
1.453 + (Repeat $ (((@@ o (map (rule2stac calc))) rules) $ e_term));
1.454 +(* val (calc, rules) = (!calclist', rules);
1.455 + *)
1.456 +fun rules2scr_Seq calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
1.457 + if contain_bdv rules
1.458 + then ScrStep_inst $ Term $ Bdv $
1.459 + (((@@ o (map (rule2stac_inst calc))) rules) $ e_term)
1.460 + else ScrStep $ Term $
1.461 + (((@@ o (map (rule2stac calc))) rules) $ e_term);
1.462 +
1.463 +(*.prepare the input for an rls for use:
1.464 + # generate a script for stepwise execution of the rls
1.465 + # filter the operators for Calc out of the script
1.466 + !!!use this function in ruleset' := !!! .*)
1.467 +fun prep_rls Erls = raise error "prep_rls not impl. for Erls"
1.468 + | prep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,rules,...}) =
1.469 + let val sc = (rules2scr_Rls (!calclist') rules)
1.470 + in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
1.471 + srls=srls,
1.472 + calc = (*FIXXXME.040207 use also for met*)
1.473 + ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
1.474 + (filter is_calc) o stacpbls) sc,
1.475 + rules=rules,
1.476 + scr = Script sc} end
1.477 +(* val (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) = add_new_c;
1.478 + *)
1.479 + | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) =
1.480 + let val sc = (rules2scr_Seq (!calclist') rules)
1.481 + in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
1.482 + srls=srls,
1.483 + calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
1.484 + (filter is_calc) o stacpbls) sc,
1.485 + rules=rules,
1.486 + scr = Script sc} end
1.487 + | prep_rls (Rrls {id,...}) =
1.488 + raise error ("prep_rls not required for Rrls \""^id^"\"");
1.489 +(*
1.490 + val Script sc = (#scr o rep_rls o prep_rls) isolate_root;
1.491 + (writeln o term2str) sc;
1.492 + val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv;
1.493 + (writeln o term2str) sc;
1.494 + *)