wneuper/isa: src/Tools/isac/ProgLang/scrtools.sml@ed0ff27b6165

     1 (* tools which depend on Script.thy and thus are not in termC.sml

     2    (c) Walther Neuper 2000

     4 use"ProgLang/scrtools.sml";

     5 use"scrtools.sml";

     6 *)

     9 fun is_reall_dsc

    10   (Const(_,Type("fun",[Type("List.list",

    11 			    [Type ("real",[])]),_]))) = true

    12   | is_reall_dsc

    13   (Const(_,Type("fun",[Type("List.list",

    14 			    [Type ("real",[])]),_])) $ t) = true

    15   | is_reall_dsc _ = false;

    16 fun is_booll_dsc

    17   (Const(_,Type("fun",[Type("List.list",

    18 			    [Type ("bool",[])]),_]))) = true

    19   | is_booll_dsc

    20   (Const(_,Type("fun",[Type("List.list",

    21 			    [Type ("bool",[])]),_])) $ t) = true

    22   | is_booll_dsc _ = false;

    23 (*

    24 > val t = (term_of o the o (parse thy)) "relations";

    25 > atomtyp (type_of t);

    26 *** Type (fun,[

    27 ***   Type (List.list,[

    28 ***     Type (bool,[])

    29 ***     ]

    30 ***   Type (Tools.una,[])

    31 ***   ]

    32 > is_booll_dsc t;

    33 val it = true : bool

    34 > is_reall_dsc t;

    35 val it = false : bool

    36 *)

    38 fun is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_]))) = true

    39   | is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_])) $ t) = true

    40   (*WN:8.5.03: ???                                           ~~~~ ???*)

    41   | is_list_dsc _ = false;

    42 (*

    43 > val t = str2term "someList";

    44 > is_list_dsc t;

    45 val it = true : bool

    47 > val t = (term_of o the o (parse thy))

    48           "additional_relations [a=b,c=(d::real)]";

    49 > is_list_dsc t;

    50 val it = true : bool

    51 > is_list_dsc (head_of t);

    52 val it = true : bool

    54 > val t = (term_of o the o (parse thy))"max_relation (A=#2*a*b-a^^^#2)";

    55 > is_list_dsc t;

    56 val it = false : bool

    57 > is_list_dsc (head_of t);

    58 val it = false : bool

    59 > val t = (term_of o the o (parse thy)) "testdscforlist";

    60 > is_list_dsc (head_of t);

    61 val it = true : bool

    62 *)

    65 fun is_unl (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true

    66   | is_unl _ = false;

    67 (*

    68 > val t = str2term "someList"; is_unl t;

    69 val it = true : bool

    70 > val t = (term_of o the o (parse thy)) "maximum";

    71 > is_unl t;

    72 val it = false : bool

    73 *)

    75 (*WN110511  Const would be clearer !!! TODO combine both fun is_dsc ...

    76 fun is_dsc (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) = true

    77   | is_dsc (Const(_,Type("fun",[_,Type("Tools.una",_)]))) = true

    78   | is_dsc (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true

    79   | is_dsc (Const(_,Type("fun",[_,Type("Tools.str",_)]))) = true

    80   | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) = true

    81   | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))= true

    82   | is_dsc (Const(_,Type("fun",[_,Type("Tools.tobooll",_)])))= true

    83   | is_dsc (Const(_,Type("fun",[_,Type("Tools.unknow",_)])))= true

    84   | is_dsc (Const(_,Type("fun",[_,Type("Tools.cpy",_)])))= true

    85   | is_dsc _ = false;

    86 *)

    87 fun is_dsc term =

    88     (case (range_type o type_of) term of

    89 	Type("Tools.nam",_) => true

    90       | Type("Tools.una",_) => true

    91       | Type("Tools.unl",_) => true

    92       | Type("Tools.str",_) => true

    93       | Type("Tools.toreal",_) => true

    94       | Type("Tools.toreall",_) => true

    95       | Type("Tools.tobooll",_) => true

    96       | Type("Tools.unknow",_) => true

    97       | Type("Tools.cpy",_) => true

    98       | _ => false)

    99     handle Match => false;

   102 (*

   103 val t as t1 $ t2 = str2term "antiDerivativeName M_b";

   104 val Const (_, Type ("fun", [Type ("fun", _), Type ("Tools.una",[])])) $ _ = t;

   105 is_dsc t1;

   107 > val t = (term_of o the o (parse thy)) "maximum";

   108 > is_dsc t;

   109 val it = true : bool

   110 > val t = (term_of o the o (parse thy)) "testdscforlist";

   111 > is_dsc t;

   112 val it = true : bool

   114 > val t = (head_of o term_of o the o (parse thy)) "maximum A";

   115 > is_dsc t;

   116 val it = true : bool

   117 > val t = (head_of o term_of o the o (parse thy))

   118   "fixedValues [R=(R::real)]";

   119 > is_dsc t;

   120 val it = true : bool

   121 *)

   124 (*make the term 'Subproblem (domID, pblID)' to a formula for frontend;

   125   needs to be here after def. Subproblem in Script.thy*)

   126 val t as (subpbl_t $ (pair_t $ Free (domID,_) $ pblID)) =

   127     (term_of o the o (parse @{theory Script}))

   128 	"Subproblem (Isac,[equation,univar])";

   129 val t as (pbl_t $ _) =

   130     (term_of o the o (parse @{theory Script}))

   131 	"Problem (Isac,[equation,univar])";

   132 val Free (_, ID_type) = (term_of o the o (parse @{theory Script})) "x::ID";

   135 fun subpbl domID pblID =

   136     subpbl_t $ (pair_t $ Free (domID,ID_type) $

   137 	(((list2isalist ID_type) o (map (mk_free ID_type))) pblID));

   138 (*> subpbl "Isac" ["equation","univar"] = t;

   139 val it = true : bool *)

   142 fun pblterm (domID:domID) (pblID:pblID) =

   143     pbl_t $ (pair_t $ Free (domID,ID_type) $

   144 	(((list2isalist ID_type) o (map (mk_free ID_type))) pblID));

   147 (**.construct scr-env from scr(created automatically) and Rewrite_Set.**)

   149 fun one_scr_arg (Const _ $ arg $ _) = arg

   150   | one_scr_arg t = error ("one_scr_arg: called by "^(term2str t));

   151 fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2)

   152   | two_scr_arg t = error ("two_scr_arg: called by "^(term2str t));

   155 (**.generate calc from a script.**)

   157 (*.instantiate a stactic or scriptexpr, and ev. attach (curried) argument

   158 args:

   159    E       environment

   160    v       current value, is attached to curried stactics

   161    stac     stactic to be instantiated

   162 precond:

   163    not (a = NONE) /\ (v = e_term) /\ (stac curried, i.e. without last arg.)

   164    this ........................ is the initialization for assy with l=[],

   165    but the 1st stac is

   166    (a) curried:     then (a = SOME _), or

   167    (b) not curried: then the values of the initialization are not used

   168 .*)

   169 datatype stacexpr = STac of term | Expr of term

   170 fun rep_stacexpr (STac t ) = t

   171   | rep_stacexpr (Expr t) =

   172     error ("rep_stacexpr called with t= "^(term2str t));

   174 type env = (term * term) list;

   176 (*update environment; t <> empty if coming from listexpr*)

   177 fun upd_env (env:env) (v,t) =

   178   let val env' = if t = e_term then env else overwrite (env,(v,t));

   179     (*val _= tracing("### upd_env: = "^(subst2str env'));*)

   180   in env' end;

   182 (*.substitute the script's environment in a leaf of the script's parse-tree

   183    and attach the curried argument of a tactic, if any.

   184    a leaf is either a tactic or an 'exp' in 'let v = expr'

   185    where 'exp' does not contain a tactic.

   186 CAUTION: (1) currying with @@ requires 2 patterns for each tactic

   187          (2) the non-curried version must return NONE for a

   188 	 (3) non-matching patterns become an Expr by fall-through.

   189 WN060906 quick and dirty fix: due to (2) a is returned, too.*)

   190 fun subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=

   191     (NONE, STac (subst_atomic E t))

   193   | subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))=

   194     (a, (*in these cases we hope, that a = SOME _*)

   195      STac (case a of SOME a' => (subst_atomic E (t $ a'))

   196 		   | NONE => ((subst_atomic E t) $ v)))

   198   | subst_stacexpr E a v

   199 	      (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ _ )) =

   200     (NONE, STac (subst_atomic E t))

   202   | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _))=

   203     (a, STac (case a of SOME a' => subst_atomic E (t $ a')

   204 	     | NONE => ((subst_atomic E t) $ v)))

   206   | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ ))=

   207     (NONE, STac (subst_atomic E t))

   209   | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) =

   210     (a, STac (case a of SOME a' => subst_atomic E (t $ a')

   211 	     | NONE => ((subst_atomic E t) $ v)))

   213   | subst_stacexpr E a v

   214 	      (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ _ )) =

   215     (NONE, STac (subst_atomic E t))

   217   | subst_stacexpr E a v

   218 	      (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )) =

   219     (a, STac (case a of SOME a' => subst_atomic E (t $ a')

   220 	     | NONE => ((subst_atomic E t) $ v)))

   222   | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) =

   223     (NONE, STac (subst_atomic E t))

   225   | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ )) =

   226     (a, STac (case a of SOME a' => subst_atomic E (t $ a')

   227 	     | NONE => ((subst_atomic E t) $ v)))

   229   | subst_stacexpr E a v

   230 	      (t as (Const("Script.Check'_elementwise",_) $ _ $ _ )) =

   231     (NONE, STac (subst_atomic E t))

   233   | subst_stacexpr E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) =

   234     (a, STac (case a of SOME a' => subst_atomic E (t $ a')

   235 		 | NONE => ((subst_atomic E t) $ v)))

   237   | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) =

   238     (NONE, STac (subst_atomic E t))

   240   | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*)

   241     (a, STac (case a of SOME a' => subst_atomic E (t $ a')

   242 		 | NONE => ((subst_atomic E t) $ v)))

   244   | subst_stacexpr E a v (t as (Const ("Script.SubProblem",_) $ _ $ _ )) =

   245     (NONE, STac (subst_atomic E t))

   247   | subst_stacexpr E a v (t as (Const ("Script.Take",_) $ _ )) =

   248     (NONE, STac (subst_atomic E t))

   250   | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ $ _ )) =

   251     (NONE, STac (subst_atomic E t))

   253   | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ )) =

   254     (a, STac (case a of SOME a' => subst_atomic E (t $ a')

   255 		 | NONE => ((subst_atomic E t) $ v)))

   257   (*now all tactics are matched out and this leaf must be without a tactic*)

   258   | subst_stacexpr E a v t =

   259     (a, Expr (subst_atomic (case a of SOME a => upd_env E (a,v)

   260 				| NONE => E) t));

   261 (*> val t = str2term "SubProblem(Test_, [linear, univariate, equation, test], [Test, solve_linear]) [BOOL e_, REAL v_]";

   262 > subst_stacexpr [] NONE e_term t;*)

   265 fun stacpbls (h $ body) =

   266   let

   267     fun scan ts (Const ("HOL.Let",_) $ e $ (Abs (v,T,b))) =

   268       (scan ts e) @ (scan ts b)

   269       | scan ts (Const ("If",_) $ c $ e1 $ e2) = (scan ts e1) @ (scan ts e2)

   270       | scan ts (Const ("Script.While",_) $ c $ e $ _) = scan ts e

   271       | scan ts (Const ("Script.While",_) $ c $ e) = scan ts e

   272       | scan ts (Const ("Script.Repeat",_) $ e $ _) = scan ts e

   273       | scan ts (Const ("Script.Repeat",_) $ e) = scan ts e

   274       | scan ts (Const ("Script.Try",_) $ e $ _) = scan ts e

   275       | scan ts (Const ("Script.Try",_) $ e) = scan ts e

   276       | scan ts (Const ("Script.Or",_) $e1 $ e2 $ _) =

   277 	(scan ts e1) @ (scan ts e2)

   278       | scan ts (Const ("Script.Or",_) $e1 $ e2) =

   279 	(scan ts e1) @ (scan ts e2)

   280       | scan ts (Const ("Script.Seq",_) $e1 $ e2 $ _) =

   281 	(scan ts e1) @ (scan ts e2)

   282       | scan ts (Const ("Script.Seq",_) $e1 $ e2) =

   283 	(scan ts e1) @ (scan ts e2)

   284       | scan ts t = case subst_stacexpr [] NONE e_term t of

   285 			(_, STac _) => [t] | (_, Expr _) => []

   286   in (distinct o (scan [])) body end;

   287     (*sc = Solve_root_equation ...

   288 > val ts = stacpbls sc;

   289 > tracing (terms2str thy ts);

   290 ["Rewrite square_equation_left True e_",

   291  "Rewrite_Set SqRoot_simplify False e_",

   292  "Rewrite_Set rearrange_assoc False e_",

   293  "Rewrite_Set isolate_root False e_",

   294  "Rewrite_Set norm_equation False e_",

   295  "Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False e_"]

   296 *)

   300 fun is_calc (Const ("Script.Calculate",_) $ _) = true

   301   | is_calc (Const ("Script.Calculate",_) $ _ $ _) = true

   302   | is_calc _ = false;

   303 fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_

   304   | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_

   305   | op_of_calc t = error ("op_of_calc called with" ^ term2str t);

   306 (*

   307  val Script sc = (#scr o rep_rls) Test_simplify;

   308  val stacs = stacpbls sc;

   310  val calcs = filter is_calc stacs;

   311  val ids = map op_of_calc calcs;

   312  map (curry assoc1 (!calclist')) ids;

   314  (((map (curry assoc1 (!calclist'))) o (map op_of_calc) o

   315   (filter is_calc) o stacpbls) sc):calc list;

   316 *)

   318 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

   319 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

   321 (** for automatic creation of scripts from rls **)

   322 (* naming of identifiers in scripts ???...

   323    not accepted !!!...

   324 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_::'z) = t_";

   325 ((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o

   326      (parse @{theory})) "(_t::'z) = _t";

   327 *)

   328 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t::'z) = t";

   329 ((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o

   330      (parse @{theory})) "(t't::'z) = t't";

   331 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_t::'z) = t_t";

   333 ((inst_abs @{theory}) o term_of o the o (parse @{theory}))

   334 "Script Stepwise (t_t::'z) =\

   335         \(Repeat\

   336 	\  ((Try (Repeat (Rewrite real_diff_minus False))) @@  \

   337 	\   (Try (Repeat (Rewrite add_commute False))) @@ \

   338 	\   (Try (Repeat (Rewrite real_mult_commute False))))  \

   339 	\  t_t)";

   340 val ScrStep $ _ $ _ =     (*'z not affected by parse: 'a --> real*)

   341     ((inst_abs @{theory}) o term_of o the o (parse @{theory}))

   342 	"Script Stepwise (t_t::'z) =\

   343         \(Repeat\

   344 	\  ((Try (Repeat (Rewrite real_diff_minus False))) @@  \

   345 	\   (Try (Repeat (Rewrite add_commute False))) @@ \

   346 	\   (Try (Repeat (Rewrite real_mult_commute False))))  \

   347 	\  t_t)";

   348 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body

   349 are inconsistent !!!*)

   350 val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*)

   351     ((inst_abs @{theory}) o term_of o the o (parse @{theory}))

   352 	"Script Stepwise_inst (t_t::'z) (v::real) =\

   353         \(Repeat\

   354 	\  ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \

   355 	\   (Try (Repeat (Rewrite_Inst [(bdv,v)] add_commute False))) @@\

   356 	\   (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \

   357 	\  t_t)";

   358 val Repeat $ _ =

   359     ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))

   360 	"Repeat (Rewrite real_diff_minus False t)";

   361 val Try $ _ =

   362     ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))

   363 	"Try (Rewrite real_diff_minus False t)";

   364 val Cal $ _ =

   365     ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))

   366 	"Calculate PLUS";

   367 val Ca1 $ _ =

   368     ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))

   369 	"Calculate1 PLUS";

   370 val Rew $ (Free (_,IDtype)) $ _ $ t =

   371     ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))

   372 	"Rewrite real_diff_minus False t";

   373 val Rew_Inst $ Subs $ _ $ _ =

   374     ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))

   375 	"Rewrite_Inst [(bdv,v)] real_diff_minus False";

   376 val Rew_Set $ _ $ _ =

   377     ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))

   378 	"Rewrite_Set real_diff_minus False";

   379 val Rew_Set_Inst $ _ $ _ $ _ =

   380     ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))

   381 	"Rewrite_Set_Inst [(bdv,v)] real_diff_minus False";

   382 val SEq $ _ $ _ $ _ =

   383     ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))

   384 	"  ((Try (Repeat (Rewrite real_diff_minus False))) @@  \

   385         \   (Try (Repeat (Rewrite add_commute False))) @@ \

   386         \   (Try (Repeat (Rewrite real_mult_commute False)))) t";

   388 fun rule2stac _ (Thm (thmID, _)) =

   389     Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const))

   390   | rule2stac calc (Calc (c, _)) =

   391     Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))

   392   | rule2stac calc (Cal1 (c, _)) =

   393     Try $ (Repeat $ (Ca1 $ Free (assoc_calc (calc ,c), IDtype)))

   394   | rule2stac _ (Rls_ rls) =

   395     Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);

   396 (*val t = rule2stac [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));

   397 atomt t; term2str t;

   398 val t = rule2stac calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_"));

   399 atomt t; term2str t;

   400 val t = rule2stac [] (Rls_ rearrange_assoc);

   401 atomt t; term2str t;

   402 *)

   403 fun rule2stac_inst _ (Thm (thmID, _)) =

   404     Try $ (Repeat $ (Rew_Inst $ Subs $ Free (thmID, IDtype) $

   405 			      HOLogic.false_const))

   406   | rule2stac_inst calc (Calc (c, _)) =

   407     Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))

   408   | rule2stac_inst calc (Cal1 (c, _)) =

   409     Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))

   410   | rule2stac_inst _ (Rls_ rls) =

   411     Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $

   412 			HOLogic.false_const);

   413 (*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));

   414 atomt t; term2str t;

   415 val t = rule2stac_inst calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_"));

   416 atomt t; term2str t;

   417 val t = rule2stac_inst [] (Rls_ rearrange_assoc);

   418 atomt t; term2str t;

   419 *)

   421 (*for appropriate nesting take stacs in _reverse_ order*)

   422 fun @@@ sts [s] = SEq $ s $ sts

   423   | @@@ sts (s::ss) = @@@ (SEq $ s $ sts) ss;

   424 fun @@ [stac] = stac

   425   | @@ [s1, s2] = SEq $ s1 $ s2 (*---------vvv--*)

   426   | @@ stacs =

   427     let val s3::s2::ss = rev stacs

   428     in @@@ (SEq $ s2 $ s3) ss end;

   429 (*

   430  val rules = (#rules o rep_rls) isolate_root;

   431  val rs = map (rule2stac calclist) rules;

   432  val tt = @@ rs;

   433  atomt tt; tracing (term2str tt);

   434  *)

   436 val contains_bdv = (not o null o (filter is_bdv) o ids2str o #prop o rep_thm);

   438 (*.does a rule contain a 'bdv'; descend recursively into Rls_.*)

   439 fun contain_bdv [] = false

   440   | contain_bdv (Thm (_, thm)::rs) =

   441     if (not o contains_bdv) thm

   442     then contain_bdv rs

   443     else true

   444   | contain_bdv (Calc _ ::rs) = contain_bdv rs

   445   | contain_bdv (Cal1 _ ::rs) = contain_bdv rs

   446   | contain_bdv (Rls_ rls ::rs) =

   447     contain_bdv (get_rules rls) orelse contain_bdv rs

   448   | contain_bdv (r::_) =

   449     error ("contain_bdv called with ["^(id_rule r)^",...]");

   451 fun rules2scr_Rls calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)

   452     if contain_bdv rules

   453     then ScrStep_inst $ Term $ Bdv $

   454 	 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ e_term))

   455     else ScrStep $ Term $

   456 	 (Repeat $ (((@@ o (map (rule2stac      calc))) rules) $ e_term));

   457 (* val (calc, rules) = (!calclist', rules);

   458    *)

   459 fun rules2scr_Seq calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)

   460     if contain_bdv rules

   461     then ScrStep_inst $ Term $ Bdv $

   462 	 (((@@ o (map (rule2stac_inst calc))) rules) $ e_term)

   463     else ScrStep $ Term $

   464 	 (((@@ o (map (rule2stac      calc))) rules) $ e_term);

   466 (*.prepare the input for an rls for use:

   467    # generate a script for stepwise execution of the rls

   468    # filter the operators for Calc out of the script ?WN111014?

   469    !!!use this function in ruleset' := !!! .*)

   470 fun prep_rls Erls = error "prep_rls not impl. for Erls"

   471   | prep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,rules,...}) =

   472       let val sc = (rules2scr_Rls (!calclist') rules)

   473       in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,

   474 	      srls = srls,

   475 	      calc = (*FIXXXME.040207 use also for met*)

   476 	        ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o

   477 	          (filter is_calc) o stacpbls) sc,

   478 	      rules = rules,

   479 	      scr = Script sc} end

   480   | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) =

   481       let val sc = (rules2scr_Seq (!calclist') rules)

   482       in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,

   483 	      srls=srls,

   484 	      calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o

   485 		      (filter is_calc) o stacpbls) sc,

   486 	      rules=rules,

   487 	      scr = Script sc} end

   488   | prep_rls (Rrls {id,...}) =

   489       error ("prep_rls not required for Rrls \"" ^ id ^ "\"");

   490 (*

   491  val Script sc = (#scr o rep_rls o prep_rls) isolate_root;

   492  (tracing o term2str) sc;

   493  val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv;

   494  (tracing o term2str) sc;

   495   *)

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 24 May 2012 17:13:58 +0200
changeset 42433	ed0ff27b6165
parent 42426	fc042a668d7a
child 42451	bc03b5d60547
permissions	-rw-r--r--