neuper@37947: (* tools which depend on Script.thy and thus are not in term.sml
neuper@37906:    (c) Walther Neuper 2000
neuper@37906: 
neuper@37947: use"ProgLang/scrtools.sml";
neuper@37906: use"scrtools.sml";
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: fun is_reall_dsc 
neuper@37906:   (Const(_,Type("fun",[Type("List.list",
neuper@37906: 			    [Type ("real",[])]),_]))) = true
neuper@37906:   | is_reall_dsc 
neuper@37906:   (Const(_,Type("fun",[Type("List.list",
neuper@37906: 			    [Type ("real",[])]),_])) $ t) = true
neuper@37906:   | is_reall_dsc _ = false;
neuper@37906: fun is_booll_dsc 
neuper@37906:   (Const(_,Type("fun",[Type("List.list",
neuper@37906: 			    [Type ("bool",[])]),_]))) = true
neuper@37906:   | is_booll_dsc 
neuper@37906:   (Const(_,Type("fun",[Type("List.list",
neuper@37906: 			    [Type ("bool",[])]),_])) $ t) = true
neuper@37906:   | is_booll_dsc _ = false;
neuper@37906: (*
neuper@37906: > val t = (term_of o the o (parse thy)) "relations";
neuper@37906: > atomtyp (type_of t);
neuper@37906: *** Type (fun,[
neuper@37906: ***   Type (List.list,[
neuper@37906: ***     Type (bool,[])
neuper@37906: ***     ]
neuper@37906: ***   Type (Tools.una,[])
neuper@37906: ***   ]
neuper@37906: > is_booll_dsc t;
neuper@37906: val it = true : bool
neuper@37906: > is_reall_dsc t;
neuper@37906: val it = false : bool
neuper@37906: *)
neuper@37906: 
neuper@37906: fun is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_]))) = true
neuper@37906:   | is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_])) $ t) = true
neuper@37906:   (*WN:8.5.03: ???                                           ~~~~ ???*)
neuper@37906:   | is_list_dsc _ = false;
neuper@37906: (*
neuper@37906: > val t = str2term "someList";
neuper@37906: > is_list_dsc t; 
neuper@37906: val it = true : bool
neuper@37906: 
neuper@37906: > val t = (term_of o the o (parse thy))
neuper@37906:           "additional_relations [a=b,c=(d::real)]";
neuper@37906: > is_list_dsc t;
neuper@37906: val it = true : bool
neuper@37906: > is_list_dsc (head_of t);
neuper@37906: val it = true : bool
neuper@37906: 
neuper@37906: > val t = (term_of o the o (parse thy))"max_relation (A=#2*a*b-a^^^#2)";
neuper@37906: > is_list_dsc t;
neuper@37906: val it = false : bool
neuper@37906: > is_list_dsc (head_of t);
neuper@37906: val it = false : bool     
neuper@37906: > val t = (term_of o the o (parse thy)) "testdscforlist";
neuper@37906: > is_list_dsc (head_of t);
neuper@37906: val it = true : bool
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: fun is_unl (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true
neuper@37906:   | is_unl _ = false;
neuper@37906: (*
neuper@37906: > val t = str2term "someList"; is_unl t;
neuper@37906: val it = true : bool
neuper@37906: > val t = (term_of o the o (parse thy)) "maximum";
neuper@37906: > is_unl t;
neuper@37906: val it = false : bool
neuper@37906: *)
neuper@37906: 
neuper@37906: fun is_dsc (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) = true
neuper@37906:   | is_dsc (Const(_,Type("fun",[_,Type("Tools.una",_)]))) = true
neuper@37906:   | is_dsc (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true
neuper@37906:   | is_dsc (Const(_,Type("fun",[_,Type("Tools.str",_)]))) = true
neuper@37906:   | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) = true
neuper@37906:   | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))= true
neuper@37906:   | is_dsc (Const(_,Type("fun",[_,Type("Tools.tobooll",_)])))= true
neuper@37906:   | is_dsc (Const(_,Type("fun",[_,Type("Tools.unknow",_)])))= true
neuper@37906:   | is_dsc (Const(_,Type("fun",[_,Type("Tools.cpy",_)])))= true
neuper@37906:   | is_dsc _ = false;
neuper@37906: fun is_dsc term = 
neuper@37906:     (case (range_type o type_of) term of
neuper@37906: 	Type("Tools.nam",_) => true
neuper@37906:       | Type("Tools.una",_) => true
neuper@37906:       | Type("Tools.unl",_) => true
neuper@37906:       | Type("Tools.str",_) => true
neuper@37906:       | Type("Tools.toreal",_) => true
neuper@37906:       | Type("Tools.toreall",_) => true
neuper@37906:       | Type("Tools.tobooll",_) => true
neuper@37906:       | Type("Tools.unknow",_) => true
neuper@37906:       | Type("Tools.cpy",_) => true
neuper@37906:       | _ => false)
neuper@37906:     handle Match => false;
neuper@37906: 
neuper@37906: 
neuper@37906: (*
neuper@37906: val t as t1 $ t2 = str2term "antiDerivativeName M_b";
neuper@37906: val Const (_, Type ("fun", [Type ("fun", _), Type ("Tools.una",[])])) $ _ = t;
neuper@37906: is_dsc t1;
neuper@37906: 
neuper@37906: > val t = (term_of o the o (parse thy)) "maximum";
neuper@37906: > is_dsc t;
neuper@37906: val it = true : bool
neuper@37906: > val t = (term_of o the o (parse thy)) "testdscforlist";
neuper@37906: > is_dsc t;
neuper@37906: val it = true : bool
neuper@37906: 
neuper@37906: > val t = (head_of o term_of o the o (parse thy)) "maximum A";
neuper@37906: > is_dsc t;
neuper@37906: val it = true : bool
neuper@37906: > val t = (head_of o term_of o the o (parse thy)) 
neuper@37906:   "fixedValues [R=(R::real)]";
neuper@37906: > is_dsc t;
neuper@37906: val it = true : bool
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: (*make the term 'Subproblem (domID, pblID)' to a formula for frontend;
neuper@37906:   needs to be here after def. Subproblem in Script.thy*)
neuper@37906: val t as (subpbl_t $ (pair_t $ Free (domID,_) $ pblID)) = 
neuper@37906:     (term_of o the o (parse @{theory Script})) 
neuper@37906: 	"Subproblem (Isac,[equation,univar])";
neuper@37906: val t as (pbl_t $ _) = 
neuper@37906:     (term_of o the o (parse @{theory Script})) 
neuper@37906: 	"Problem (Isac,[equation,univar])";
neuper@37906: val Free (_, ID_type) = (term_of o the o (parse @{theory Script})) "x::ID";
neuper@37906: 
neuper@37906: 
neuper@37906: fun subpbl domID pblID =
neuper@37906:     subpbl_t $ (pair_t $ Free (domID,ID_type) $ 
neuper@37906: 	(((list2isalist ID_type) o (map (mk_free ID_type))) pblID));
neuper@37906: (*> subpbl "Isac" ["equation","univar"] = t;
neuper@37906: val it = true : bool *)
neuper@37906: 
neuper@37906: 
neuper@37906: fun pblterm (domID:domID) (pblID:pblID) =
neuper@37906:     pbl_t $ (pair_t $ Free (domID,ID_type) $ 
neuper@37906: 	(((list2isalist ID_type) o (map (mk_free ID_type))) pblID));
neuper@37906: 
neuper@37906: 
neuper@37906: (**.construct scr-env from scr(created automatically) and Rewrite_Set.**)
neuper@37906: 
neuper@37906: fun one_scr_arg (Const _ $ arg $ _) = arg
neuper@37906:   | one_scr_arg t = raise error ("one_scr_arg: called by "^(term2str t));
neuper@37906: fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2)
neuper@37906:   | two_scr_arg t = raise error ("two_scr_arg: called by "^(term2str t));
neuper@37906: 
neuper@37906: 
neuper@37906: (**.generate calc from a script.**)
neuper@37906: 
neuper@37906: (*.instantiate a stactic or scriptexpr, and ev. attach (curried) argument
neuper@37906: args:
neuper@37906:    E       environment
neuper@37906:    v       current value, is attached to curried stactics
neuper@37906:    stac     stactic to be instantiated
neuper@37906: precond:
neuper@37906:    not (a = NONE) /\ (v = e_term) /\ (stac curried, i.e. without last arg.)
neuper@37906:    this ........................ is the initialization for assy with l=[],
neuper@37906:    but the 1st stac is
neuper@37906:    (a) curried:     then (a = SOME _), or 
neuper@37906:    (b) not curried: then the values of the initialization are not used
neuper@37906: .*)
neuper@37906: datatype stacexpr = STac of term | Expr of term
neuper@37906: fun rep_stacexpr (STac t ) = t
neuper@37906:   | rep_stacexpr (Expr t) = 
neuper@37906:     raise error ("rep_stacexpr called with t= "^(term2str t));
neuper@37906: 
neuper@37906: type env = (term * term) list;
neuper@37906: 
neuper@37906: (*update environment; t <> empty if coming from listexpr*)
neuper@37906: fun upd_env (env:env) (v,t) =
neuper@37906:   let val env' = if t = e_term then env else overwrite (env,(v,t));
neuper@37906:     (*val _= writeln("### upd_env: = "^(subst2str env'));*)
neuper@37906:   in env' end;
neuper@37906: 
neuper@37906: (*.substitute the scripts environment in a leaf of the scripts parse-tree
neuper@37906:    and attach the curried argument of a tactic, if any.
neuper@37906:    a leaf is either a tactic or an 'exp' in 'let v = expr'
neuper@37906:    where 'exp' does not contain a tactic.
neuper@37906: CAUTION: (1) currying with @@ requires 2 patterns for each tactic
neuper@37906:          (2) the non-curried version must return NONE for a 
neuper@37906: 	 (3) non-matching patterns become an Expr by fall-through.
neuper@37906: WN060906 quick and dirty fix: due to (2) a is returned, too.*)
neuper@37906: fun subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=
neuper@37906:     (NONE, STac (subst_atomic E t))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))=
neuper@37906:     (a, (*in these cases we hope, that a = SOME _*)
neuper@37906:      STac (case a of SOME a' => (subst_atomic E (t $ a'))
neuper@37906: 		   | NONE => ((subst_atomic E t) $ v)))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v 
neuper@37906: 	      (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ _ )) =
neuper@37906:     (NONE, STac (subst_atomic E t))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _))=
neuper@37906:     (a, STac (case a of SOME a' => subst_atomic E (t $ a')
neuper@37906: 	     | NONE => ((subst_atomic E t) $ v)))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ ))=
neuper@37906:     (NONE, STac (subst_atomic E t))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) =
neuper@37906:     (a, STac (case a of SOME a' => subst_atomic E (t $ a')
neuper@37906: 	     | NONE => ((subst_atomic E t) $ v)))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v 
neuper@37906: 	      (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ _ )) =
neuper@37906:     (NONE, STac (subst_atomic E t))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v 
neuper@37906: 	      (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )) =
neuper@37906:     (a, STac (case a of SOME a' => subst_atomic E (t $ a')
neuper@37906: 	     | NONE => ((subst_atomic E t) $ v)))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) =
neuper@37906:     (NONE, STac (subst_atomic E t))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ )) =
neuper@37906:     (a, STac (case a of SOME a' => subst_atomic E (t $ a')
neuper@37906: 	     | NONE => ((subst_atomic E t) $ v)))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v 
neuper@37906: 	      (t as (Const("Script.Check'_elementwise",_) $ _ $ _ )) = 
neuper@37906:     (NONE, STac (subst_atomic E t))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) = 
neuper@37906:     (a, STac (case a of SOME a' => subst_atomic E (t $ a')
neuper@37906: 		 | NONE => ((subst_atomic E t) $ v)))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) = 
neuper@37906:     (NONE, STac (subst_atomic E t))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*)
neuper@37906:     (a, STac (case a of SOME a' => subst_atomic E (t $ a')
neuper@37906: 		 | NONE => ((subst_atomic E t) $ v)))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const ("Script.SubProblem",_) $ _ $ _ )) =
neuper@37906:     (NONE, STac (subst_atomic E t))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const ("Script.Take",_) $ _ )) =
neuper@37906:     (NONE, STac (subst_atomic E t))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ $ _ )) =
neuper@37906:     (NONE, STac (subst_atomic E t))
neuper@37906: 
neuper@37906:   | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ )) =
neuper@37906:     (a, STac (case a of SOME a' => subst_atomic E (t $ a')
neuper@37906: 		 | NONE => ((subst_atomic E t) $ v)))
neuper@37906: 
neuper@37906:   (*now all tactics are matched out and this leaf must be without a tactic*)
neuper@37906:   | subst_stacexpr E a v t = 
neuper@37906:     (a, Expr (subst_atomic (case a of SOME a => upd_env E (a,v) 
neuper@37906: 				| NONE => E) t));
neuper@37984: (*> val t = str2term "SubProblem(Test_, [linear, univariate, equation, test], [Test, solve_linear]) [BOOL e_, REAL v_]";
neuper@37906: > subst_stacexpr [] NONE e_term t;*)
neuper@37906: 
neuper@37906: 
neuper@37906: fun stacpbls (h $ body) =
neuper@37906:   let
neuper@37906:     fun scan ts (Const ("Let",_) $ e $ (Abs (v,T,b))) =
neuper@37906:       (scan ts e) @ (scan ts b)
neuper@37906:       | scan ts (Const ("If",_) $ c $ e1 $ e2) = (scan ts e1) @ (scan ts e2)
neuper@37906:       | scan ts (Const ("Script.While",_) $ c $ e $ _) = scan ts e
neuper@37906:       | scan ts (Const ("Script.While",_) $ c $ e) = scan ts e
neuper@37906:       | scan ts (Const ("Script.Repeat",_) $ e $ _) = scan ts e
neuper@37906:       | scan ts (Const ("Script.Repeat",_) $ e) = scan ts e
neuper@37906:       | scan ts (Const ("Script.Try",_) $ e $ _) = scan ts e
neuper@37906:       | scan ts (Const ("Script.Try",_) $ e) = scan ts e
neuper@37906:       | scan ts (Const ("Script.Or",_) $e1 $ e2 $ _) = 
neuper@37906: 	(scan ts e1) @ (scan ts e2)
neuper@37906:       | scan ts (Const ("Script.Or",_) $e1 $ e2) = 
neuper@37906: 	(scan ts e1) @ (scan ts e2)
neuper@37906:       | scan ts (Const ("Script.Seq",_) $e1 $ e2 $ _) = 
neuper@37906: 	(scan ts e1) @ (scan ts e2)
neuper@37906:       | scan ts (Const ("Script.Seq",_) $e1 $ e2) = 
neuper@37906: 	(scan ts e1) @ (scan ts e2)
neuper@37906:       | scan ts t = case subst_stacexpr [] NONE e_term t of
neuper@37906: 			(_, STac _) => [t] | (_, Expr _) => []
neuper@37906:   in (distinct o (scan [])) body end;
neuper@37906:     (*sc = Solve_root_equation ...
neuper@37906: > val ts = stacpbls sc;
neuper@37906: > writeln (terms2str thy ts);
neuper@37906: ["Rewrite square_equation_left True e_",
neuper@37906:  "Rewrite_Set SqRoot_simplify False e_",
neuper@37906:  "Rewrite_Set rearrange_assoc False e_",
neuper@37906:  "Rewrite_Set isolate_root False e_",
neuper@37906:  "Rewrite_Set norm_equation False e_",
neuper@37906:  "Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False e_"]
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: fun is_calc (Const ("Script.Calculate",_) $ _) = true
neuper@37906:   | is_calc (Const ("Script.Calculate",_) $ _ $ _) = true
neuper@37906:   | is_calc _ = false;
neuper@37906: fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_
neuper@37906:   | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_
neuper@37906:   | op_of_calc t = raise error ("op_of_calc called with"^term2str t);
neuper@37906: (*
neuper@37906:  val Script sc = (#scr o rep_rls) Test_simplify;
neuper@37906:  val stacs = stacpbls sc;
neuper@37906: 
neuper@37906:  val calcs = filter is_calc stacs;
neuper@37906:  val ids = map op_of_calc calcs;
neuper@37906:  map (curry assoc1 (!calclist')) ids;
neuper@37906: 
neuper@37906:  (((map (curry assoc1 (!calclist'))) o (map op_of_calc) o 
neuper@37906:   (filter is_calc) o stacpbls) sc):calc list;
neuper@37906: *)
neuper@37906: 
neuper@37906: (**.for automatic creation of scripts from rls.**)
neuper@37906: (* naming of identifiers in scripts ???...
neuper@37906: ((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t::'z) = t";
neuper@37906: ((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o 
neuper@37906:      (parse @{theory})) "(t't::'z) = t't";
neuper@37906: ((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_t::'z) = t_t";
neuper@37906: (* not accepted !!!...*)
neuper@37906: ((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_::'z) = t_";
neuper@37906: ((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o 
neuper@37906:      (parse @{theory})) "(_t::'z) = _t";
neuper@37906: *)
neuper@37906: ((inst_abs @{theory}) o term_of o the o (parse @{theory}))
neuper@37906: "Script Stepwise (t::'z) =\
neuper@37906:         \(Repeat\
neuper@37906: 	\  ((Try (Repeat (Rewrite real_diff_minus False))) @@  \
neuper@37971: 	\   (Try (Repeat (Rewrite add_commute False))) @@ \
neuper@37906: 	\   (Try (Repeat (Rewrite real_mult_commute False))))  \
neuper@37923: 	\  t_t)";
neuper@37906: val ScrStep $ _ $ _ =     (*'z not affected by parse: 'a --> real*)
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parse @{theory}))  
neuper@37906: 	"Script Stepwise (t::'z) =\
neuper@37906:         \(Repeat\
neuper@37906: 	\  ((Try (Repeat (Rewrite real_diff_minus False))) @@  \
neuper@37971: 	\   (Try (Repeat (Rewrite add_commute False))) @@ \
neuper@37906: 	\   (Try (Repeat (Rewrite real_mult_commute False))))  \
neuper@37923: 	\  t_t)";
neuper@37906: (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body 
neuper@37906: are inconsistent !!!*)
neuper@37906: val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*)
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parse @{theory})) 
neuper@37906: 	"Script Stepwise_inst (t::'z) (v::real) =\
neuper@37906:         \(Repeat\
neuper@37906: 	\  ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \
neuper@37971: 	\   (Try (Repeat (Rewrite_Inst [(bdv,v)] add_commute False))) @@\
neuper@37906: 	\   (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \
neuper@37906: 	\  t)"; 
neuper@37921: val Repeat $ _ =
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
neuper@37906: 	"Repeat (Rewrite real_diff_minus False t)";
neuper@37906: val Try $ _ = 
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
neuper@37906: 	"Try (Rewrite real_diff_minus False t)";
neuper@37906: val Cal $ _ =
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
neuper@37921: 	"Calculate PLUS";
neuper@37906: val Ca1 $ _ =
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
neuper@37921: 	"Calculate1 PLUS";
neuper@37906: val Rew $ (Free (_,IDtype)) $ _ $ t =
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
neuper@37906: 	"Rewrite real_diff_minus False t";
neuper@37906: val Rew_Inst $ Subs $ _ $ _ =
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
neuper@37906: 	"Rewrite_Inst [(bdv,v)] real_diff_minus False";
neuper@37906: val Rew_Set $ _ $ _ =
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
neuper@37906: 	"Rewrite_Set real_diff_minus False";
neuper@37906: val Rew_Set_Inst $ _ $ _ $ _ =
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
neuper@37906: 	"Rewrite_Set_Inst [(bdv,v)] real_diff_minus False";
neuper@37906: val SEq $ _ $ _ $ _ =
neuper@37906:     ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
neuper@37906: 	"  ((Try (Repeat (Rewrite real_diff_minus False))) @@  \
neuper@37971:         \   (Try (Repeat (Rewrite add_commute False))) @@ \
neuper@37906:         \   (Try (Repeat (Rewrite real_mult_commute False)))) t";
neuper@37906: 
neuper@37906: fun rule2stac _ (Thm (thmID, _)) = 
neuper@37906:     Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const))
neuper@37906:   | rule2stac calc (Calc (c, _)) = 
neuper@37906:     Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
neuper@37906:   | rule2stac calc (Cal1 (c, _)) = 
neuper@37906:     Try $ (Repeat $ (Ca1 $ Free (assoc_calc (calc ,c), IDtype)))
neuper@37906:   | rule2stac _ (Rls_ rls) = 
neuper@37906:     Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);
neuper@37969: (*val t = rule2stac [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
neuper@37906: atomt t; term2str t;
neuper@38014: val t = rule2stac calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
neuper@37906: atomt t; term2str t;
neuper@37906: val t = rule2stac [] (Rls_ rearrange_assoc);
neuper@37906: atomt t; term2str t;
neuper@37906: *)
neuper@37906: fun rule2stac_inst _ (Thm (thmID, _)) = 
neuper@37906:     Try $ (Repeat $ (Rew_Inst $ Subs $ Free (thmID, IDtype) $ 
neuper@37906: 			      HOLogic.false_const))
neuper@37906:   | rule2stac_inst calc (Calc (c, _)) = 
neuper@37906:     Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
neuper@37906:   | rule2stac_inst calc (Cal1 (c, _)) = 
neuper@37906:     Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
neuper@37906:   | rule2stac_inst _ (Rls_ rls) = 
neuper@37906:     Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $ 
neuper@37906: 			HOLogic.false_const);
neuper@37969: (*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
neuper@37906: atomt t; term2str t;
neuper@38014: val t = rule2stac_inst calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
neuper@37906: atomt t; term2str t;
neuper@37906: val t = rule2stac_inst [] (Rls_ rearrange_assoc);
neuper@37906: atomt t; term2str t;
neuper@37906: *)
neuper@37906: 
neuper@37906: (*for appropriate nesting take stacs in _reverse_ order*)
neuper@37906: fun @@@ sts [s] = SEq $ s $ sts
neuper@37906:   | @@@ sts (s::ss) = @@@ (SEq $ s $ sts) ss;
neuper@37906: fun @@ [stac] = stac
neuper@37906:   | @@ [s1, s2] = SEq $ s1 $ s2 (*---------vvv--*)
neuper@37906:   | @@ stacs = 
neuper@37906:     let val s3::s2::ss = rev stacs
neuper@37906:     in @@@ (SEq $ s2 $ s3) ss end;
neuper@37906: (*
neuper@37906:  val rules = (#rules o rep_rls) isolate_root;
neuper@37906:  val rs = map (rule2stac calclist) rules;
neuper@37906:  val tt = @@ rs;
neuper@37906:  atomt tt; writeln (term2str tt);
neuper@37906:  *)
neuper@37906: 
neuper@37906: val contains_bdv = (not o null o (filter is_bdv) o ids2str o #prop o rep_thm);
neuper@37906: 
neuper@37906: (*.does a rule contain a 'bdv'; descend recursively into Rls_.*)
neuper@37906: fun contain_bdv [] = false
neuper@37906:   | contain_bdv (Thm (_, thm)::rs) = 
neuper@37906:     if (not o contains_bdv) thm
neuper@37906:     then contain_bdv rs
neuper@37906:     else true
neuper@37906:   | contain_bdv (Calc _ ::rs) = contain_bdv rs
neuper@37906:   | contain_bdv (Cal1 _ ::rs) = contain_bdv rs
neuper@37906:   | contain_bdv (Rls_ rls ::rs) = 
neuper@37906:     contain_bdv (get_rules rls) orelse contain_bdv rs
neuper@37906:   | contain_bdv (r::_) = 
neuper@37906:     raise error ("contain_bdv called with ["^(id_rule r)^",...]");
neuper@37906: 
neuper@37923: fun rules2scr_Rls calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
neuper@37906:     if contain_bdv rules
neuper@37906:     then ScrStep_inst $ Term $ Bdv $ 
neuper@37921: 	 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ e_term))
neuper@37906:     else ScrStep $ Term $
neuper@37921: 	 (Repeat $ (((@@ o (map (rule2stac      calc))) rules) $ e_term));
neuper@37906: (* val (calc, rules) = (!calclist', rules);
neuper@37906:    *)
neuper@37923: fun rules2scr_Seq calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
neuper@37906:     if contain_bdv rules
neuper@37906:     then ScrStep_inst $ Term $ Bdv $ 
neuper@37921: 	 (((@@ o (map (rule2stac_inst calc))) rules) $ e_term)
neuper@37906:     else ScrStep $ Term $
neuper@37921: 	 (((@@ o (map (rule2stac      calc))) rules) $ e_term);
neuper@37906: 
neuper@37906: (*.prepare the input for an rls for use:
neuper@37906:    # generate a script for stepwise execution of the rls
neuper@37906:    # filter the operators for Calc out of the script
neuper@37906:    !!!use this function in ruleset' := !!! .*)
neuper@37906: fun prep_rls Erls = raise error "prep_rls not impl. for Erls"
neuper@37906:   | prep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,rules,...}) = 
neuper@37906:     let val sc = (rules2scr_Rls (!calclist') rules)
neuper@37906:     in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
neuper@37906: 	    srls=srls,
neuper@37906: 	    calc = (*FIXXXME.040207 use also for met*)
neuper@37906: 	    ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o 
neuper@37906: 	     (filter is_calc) o stacpbls) sc,
neuper@37906: 	    rules=rules,
neuper@37906: 	    scr = Script sc} end
neuper@37906: (* val (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) = add_new_c;
neuper@37906:    *)
neuper@37906:   | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) = 
neuper@37906:     let val sc = (rules2scr_Seq (!calclist') rules)
neuper@37906:     in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
neuper@37906: 	 srls=srls,
neuper@37906: 	    calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o 
neuper@37906: 		    (filter is_calc) o stacpbls) sc,
neuper@37906: 	 rules=rules,
neuper@37906: 	 scr = Script sc} end
neuper@37906:   | prep_rls (Rrls {id,...}) = 
neuper@37906:     raise error ("prep_rls not required for Rrls \""^id^"\"");
neuper@37906: (*
neuper@37906:  val Script sc = (#scr o rep_rls o prep_rls) isolate_root;
neuper@37906:  (writeln o term2str) sc;
neuper@37906:  val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv;
neuper@37906:  (writeln o term2str) sc;
neuper@37906:   *)