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

   (c) Walther Neuper 2000

*)

fun is_reall_dsc 

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

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

  | is_reall_dsc 

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

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

  | is_reall_dsc _ = false;

fun is_booll_dsc 

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

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

  | is_booll_dsc 

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

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

  | is_booll_dsc _ = false;

(*

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

> atomtyp (type_of t);

*** Type (fun,[

***   Type (List.list,[

***     Type (bool,[])

***     ]

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

***   ]

> is_booll_dsc t;

val it = true : bool

> is_reall_dsc t;

val it = false : bool

*)

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

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

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

  | is_list_dsc _ = false;

(*

> val t = str2term "someList";

> is_list_dsc t; 

val it = true : bool

> val t = (Thm.term_of o the o (parse thy))

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

> is_list_dsc t;

val it = true : bool

> is_list_dsc (head_of t);

val it = true : bool

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

> is_list_dsc t;

val it = false : bool

> is_list_dsc (head_of t);

val it = false : bool     

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

> is_list_dsc (head_of t);

val it = true : bool

*)

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

  | is_unl _ = false;

(*

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

val it = true : bool

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

> is_unl t;

val it = false : bool

*)

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

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

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

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

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

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

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

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

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

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

  | is_dsc _ = false;

*)

fun is_dsc term = 

    (case (range_type o type_of) term of

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

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

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

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

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

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

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

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

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

      | _ => false)

    handle Match => false;

(*

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

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

is_dsc t1;

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

> is_dsc t;

val it = true : bool

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

> is_dsc t;

val it = true : bool

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

> is_dsc t;

val it = true : bool

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

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

> is_dsc t;

val it = true : bool

*)

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

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

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

    (Thm.term_of o the o (parse @{theory Script})) 

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

val t as (pbl_t $ _) = 

    (Thm.term_of o the o (parse @{theory Script})) 

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

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

fun subpbl domID pblID =

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

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

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

val it = true : bool *)

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

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

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

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

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

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

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

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

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

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

args:

   E       environment

   v       current value, is attached to curried stactics

   stac     stactic to be instantiated

precond:

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

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

   but the 1st stac is

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

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

.*)

datatype stacexpr = STac of term | Expr of term

fun rep_stacexpr (STac t ) = t

  | rep_stacexpr (Expr t) = 

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

type env = (term * term) list;

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

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

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

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

  in env' end;

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

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

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

   where 'exp' does not contain a tactic.

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

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

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

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

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

    (NONE, STac (subst_atomic E t))

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

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

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

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

  | subst_stacexpr E a v 

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

    (NONE, STac (subst_atomic E t))

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

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

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

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

    (NONE, STac (subst_atomic E t))

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

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

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

  | subst_stacexpr E a v 

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

    (NONE, STac (subst_atomic E t))

  | subst_stacexpr E a v 

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

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

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

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

    (NONE, STac (subst_atomic E t))

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

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

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

  | subst_stacexpr E a v 

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

    (NONE, STac (subst_atomic E t))

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

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

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

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

    (NONE, STac (subst_atomic E t))

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

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

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

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

    (NONE, STac (subst_atomic E t))

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

    (NONE, STac (subst_atomic E t))

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

    (NONE, STac (subst_atomic E t))

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

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

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

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

  | subst_stacexpr E a v t = 

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

				| NONE => E) t));

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

> subst_stacexpr [] NONE e_term t;*)

fun stacpbls (h $ body) =

  let

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

      (scan ts e) @ (scan ts b)

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

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

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

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

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

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

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

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

	(scan ts e1) @ (scan ts e2)

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

	(scan ts e1) @ (scan ts e2)

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

	(scan ts e1) @ (scan ts e2)

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

	(scan ts e1) @ (scan ts e2)

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

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

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

    (*sc = Solve_root_equation ...

> val ts = stacpbls sc;

> tracing (terms2str thy ts);

["Rewrite square_equation_left True e_",

 "Rewrite_Set SqRoot_simplify False e_",

 "Rewrite_Set rearrange_assoc False e_",

 "Rewrite_Set isolate_root False e_",

 "Rewrite_Set norm_equation False e_",

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

*)

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

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

  | is_calc _ = false;

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

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

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

(*

 val Prog sc = (#scr o rep_rls) Test_simplify;

 val stacs = stacpbls sc;

 val calcs = filter is_calc stacs;

 val ids = map op_of_calc calcs;

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

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

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

*)

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

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

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

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

   not accepted !!!...

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

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

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

*)

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

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

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

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

((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory}))

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

        \(Repeat\

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

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

	\   (Try (Repeat (Rewrite mult_commute False))))  \

	\  t_t)";

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

    ((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory}))  

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

        \(Repeat\

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

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

	\   (Try (Repeat (Rewrite mult_commute False))))  \

	\  t_t)";

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

are inconsistent !!!*)

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

    ((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory})) 

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

        \(Repeat\

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

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

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

	\  t_t)"; 

val Repeat $ _ =

    ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory})) 

	"Repeat (Rewrite real_diff_minus False t)";

val Try $ _ = 

    ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory})) 

	"Try (Rewrite real_diff_minus False t)";

val Cal $ _ =

    ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory})) 

	"Calculate PLUS";

val Ca1 $ _ =

    ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory})) 

	"Calculate1 PLUS";

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

    ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory})) 

	"Rewrite real_diff_minus False t";

val Rew_Inst $ Subs $ _ $ _ =

    ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory})) 

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

val Rew_Set $ _ $ _ =

    ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory})) 

	"Rewrite_Set real_diff_minus False";

val Rew_Set_Inst $ _ $ _ $ _ =

    ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory})) 

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

val SEq $ _ $ _ $ _ =

    ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory})) 

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

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

        \   (Try (Repeat (Rewrite mult_commute False)))) t";

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

    Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ @{term False}))

  | rule2stac thy (Calc (c, _)) = 

    Try $ (Repeat $ (Cal $ Free (assoc_calc thy c, IDtype)))

  | rule2stac thy (Cal1 (c, _)) = 

    Try $ (Repeat $ (Ca1 $ Free (assoc_calc thy c, IDtype)))

  | rule2stac _ (Rls_ rls) = 

    Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ @{term False});

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

atomt t; term2str t;

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

atomt t; term2str t;

val t = rule2stac [] (Rls_ rearrange_assoc);

atomt t; term2str t;

*)

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

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

			      @{term False}))

  | rule2stac_inst thy (Calc (c, _)) = 

    Try $ (Repeat $ (Cal $ Free (assoc_calc thy c, IDtype)))

  | rule2stac_inst thy (Cal1 (c, _)) = 

    Try $ (Repeat $ (Cal $ Free (assoc_calc thy c, IDtype)))

  | rule2stac_inst _ (Rls_ rls) = 

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

			@{term False});

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

atomt t; term2str t;

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

atomt t; term2str t;

val t = rule2stac_inst [] (Rls_ rearrange_assoc);

atomt t; term2str t;

*)

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

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

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

fun @@ [stac] = stac

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

  | @@ stacs = 

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

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

(*

 val rules = (#rules o rep_rls) isolate_root;

 val rs = map (rule2stac calclist) rules;

 val tt = @@ rs;

 atomt tt; tracing (term2str tt);

 *)

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

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

fun contain_bdv [] = false

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

    if (not o contains_bdv) thm

    then contain_bdv rs

    else true

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

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

  | contain_bdv (Rls_ rls ::rs) = 

    contain_bdv (get_rules rls) orelse contain_bdv rs

  | contain_bdv (r::_) = 

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

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

    if contain_bdv rules

    then ScrStep_inst $ Term $ Bdv $ 

	 (Repeat $ (((@@ o (map (rule2stac_inst thy))) rules) $ e_term))

    else ScrStep $ Term $

	 (Repeat $ (((@@ o (map (rule2stac thy))) rules) $ e_term));

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

   *)

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

    if contain_bdv rules

    then ScrStep_inst $ Term $ Bdv $ 

	 (((@@ o (map (rule2stac_inst thy))) rules) $ e_term)

    else ScrStep $ Term $

	 (((@@ o (map (rule2stac thy))) rules) $ e_term);

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

   # generate a script for stepwise execution of the rls

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

   !!!use this function while storing by or integrate into KEStore_Elems.add_rlss.*)

fun prep_rls _ Erls = error "prep_rls' not impl. for Erls"

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

      let val sc = (rules2scr_Rls thy rules)

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

	      srls = srls,

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

	        ((assoc_calc' thy |> map) o (map op_of_calc) o 

	          (filter is_calc) o stacpbls) sc,

	      rules = rules,

	      errpatts=errpatts,

	      scr = Prog sc} end

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

      let val sc = (rules2scr_Seq thy rules)

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

	      srls=srls,

	      calc = ((assoc_calc' thy |> map) o (map op_of_calc) o 

		      (filter is_calc) o stacpbls) sc,

	      rules=rules,

	      errpatts=errpatts,

	      scr = Prog sc} end

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

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