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

   (c) Walther Neuper 2000

*)

signature LANGUAGE_TOOLS =

  sig

    datatype stacexpr = Expr of term | STac of term

    val rep_stacexpr: stacexpr -> term

    val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * stacexpr

    val contain_bdv: Celem.rule list -> bool

    val contains_bdv: thm -> bool

    type env = (term * term) list

    val upd_env: env -> term * term -> env

    val is_booll_dsc: term -> bool

    val is_calc: term -> bool

    val is_dsc: term -> bool

    val is_list_dsc: term -> bool

    val is_reall_dsc: term -> bool

    val is_unl: term -> bool

    val pblterm: Celem.domID -> Celem.pblID -> term

    val subpbl: string -> string list -> term

    val stacpbls: term -> term list

    val one_scr_arg: term -> term

    val two_scr_arg: term -> term * term

    val op_of_calc: term -> string

    val get_calcs: theory -> term -> (Celem.prog_calcID * (Celem.calID * Celem.eval_fn)) list

    val prep_rls: theory -> Celem.rls -> Celem.rls

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  (* NONE *)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

    val rule2stac: theory -> rule -> term

    val rule2stac_inst: theory -> rule -> term

    val @@ : term list -> term

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

  end

(**)

structure LTool(**): LANGUAGE_TOOLS(**) =

struct

(**)

(* distinguish input to Model (deep embedding of terms as Isac's object language) *)

fun is_reall_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]), _]))) = true

  | is_reall_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]),_])) $ _) = true

  | is_reall_dsc _ = false;

fun is_booll_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _]))) = true

  | is_booll_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("HOL.bool", [])]),_])) $ _) = true

  | is_booll_dsc _ = false;

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

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

  (*WN:8.5.03: ???   TODO test/../scrtools.sml                ~~~~ ???*)

  | is_list_dsc _ = false;

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

  | is_unl _ = false;

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;

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

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

val subpbl_t $ (pair_t $ Free (_, _) $ _) = 

  (Thm.term_of o the o (TermC.parse @{theory Script})) "Subproblem (Isac,[equation,univar])"

val pbl_t $ _ = 

  (Thm.term_of o the o (TermC.parse @{theory Script})) "Problem (Isac,[equation,univar])"

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

fun subpbl domID pblID =

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

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

fun pblterm domID pblID =

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

	  (((TermC.list2isalist ID_type) o (map (TermC.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 " ^ Celem.term2str t);

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

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

(** generate a "type 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= " ^ Celem.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 = Celem.e_term then env else overwrite (env,(v,t));

  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 _ _ (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 _ _ 

	      (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 _ _ (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 _ _ 

	      (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 _ _ (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 _ _ 

	      (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 _ _ (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 _ _ (t as (Const ("Script.SubProblem", _) $ _ $ _)) =

    (NONE, STac (subst_atomic E t))

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

    (NONE, STac (subst_atomic E t))

  | subst_stacexpr E _ _ (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));

(* fetch tactics from a program omitting tacticals like While, Repeat,.. *)

fun stacpbls (_ $ body) =

    let

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

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

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

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

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

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

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

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

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

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

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

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

        | scan t = case subst_stacexpr [] NONE Celem.e_term t of

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

    in (distinct o scan) body end

  | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ Celem.term2str t ^ "'")

(* get operators out of a program *)

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" ^ Celem.term2str t);

fun get_calcs thy sc =

    sc

    |> stacpbls

    |> filter is_calc

    |> map op_of_calc

    |> (assoc_calc' thy |> map);

(** build up a program from rules **)

(* transform type rule to a term *)

val ScrStep $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory}))

  (*'z not affected by parse: 'a --> real*)

	"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 $ _= (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory}))

  (*'z not affected by parse: 'a --> real*)

	"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 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Repeat (Rewrite real_diff_minus False t)";

val Try $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Try (Rewrite real_diff_minus False t)";

val Cal $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Calculate PLUS";

val Ca1 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Calculate1 PLUS";

val Rew $ (Free (_, IDtype)) $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Rewrite real_diff_minus False t";

val Rew_Inst $ Subs $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

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

val Rew_Set $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Rewrite_Set real_diff_minus False";

val Rew_Set_Inst $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

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

val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

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

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

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

fun rule2stac _ (Celem.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ @{term False}))

  | rule2stac thy (Celem.Calc (c, _)) = Try $ (Repeat $ (Cal $ Free (assoc_calc thy c, IDtype)))

  | rule2stac thy (Celem.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ Free (assoc_calc thy c, IDtype)))

  | rule2stac _ (Celem.Rls_ rls) = Try $ (Rew_Set $ Free (Celem.id_rls rls, IDtype) $ @{term False})

  | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Celem.rule2str r ^ "\"");

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

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

			      @{term False}))

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

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

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

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

  | rule2stac_inst _ (Celem.Rls_ rls) = 

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

			@{term False})

  | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Celem.rule2str r ^ "\"");

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

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

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

  | op @@@ t ts =

    raise ERROR ("fun @@@ not applicable to \"" ^ Celem.term2str t ^ "\" \"" ^ Celem.terms2str ts  ^ "\"");

fun @@ [stac] = stac

  | @@ [s1, s2] = SEq $ s1 $ s2

  | @@ stacs = case rev stacs of

      s3 :: s2 :: ss => op @@@ (SEq $ s2 $ s3) ss

    | ts => raise ERROR ("fun @@ not applicable to \"" ^ Celem.terms2str ts ^ "\"")

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

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

fun contain_bdv [] = false

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

    if (not o contains_bdv) thm

    then contain_bdv rs

    else true

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

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

  | contain_bdv (Celem.Rls_ rls :: rs) = 

    contain_bdv (Celem.get_rules rls) orelse contain_bdv rs

  | contain_bdv (r :: _) = 

    error ("contain_bdv called with [" ^ Celem.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) $ Celem.e_term))

    else ScrStep $ Term $ (Repeat $ (((@@ o (map (rule2stac thy))) rules) $ Celem.e_term));

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) $ Celem.e_term)

    else ScrStep $ Term $

	 (((@@ o (map (rule2stac thy))) rules) $ Celem.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 _ Celem.Erls = error "prep_rls' not impl. for Erls"

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

      let val sc = (rules2scr_Rls thy rules)

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

	      srls = srls,

	      calc = get_calcs thy sc,

	      rules = rules,

	      errpatts=errpatts,

	      scr = Celem.Prog sc} end

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

      let val sc = (rules2scr_Seq thy rules)

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

	      srls = srls,

	      calc = get_calcs thy sc,

	      rules = rules,

	      errpatts = errpatts,

	      scr = Celem.Prog sc} end

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

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

end