(* Title:  tactics, tacticals etc. for scripts

   Author: Walther Neuper 000224

   (c) due to copyright terms

 *)

theory Prog_Tac

  imports Program

begin

text \<open>Abstract:

  Specific constants for tactics in programs, which each create a step in a calculation

  as a side effect.

  These program-tactics are related to Tactic.input for use in calculations and

  Tactic.T for internal use by lucas-interpretation.

\<close>

subsection \<open>arguments of tactic SubProblem\<close>

typedecl

  arg

consts

  REAL        :: "real => arg"

  REAL_LIST   :: "(real list) => arg"

  REAL_SET    :: "(real set) => arg"

  BOOL        :: "bool => arg"

  BOOL_LIST   :: "(bool list) => arg"

  REAL_REAL   :: "(real => real) => arg"

  STRING      :: "(char list) => arg"

  STRING_LIST :: "(char list list) => arg"

subsection \<open>tactics in programs\<close>

text \<open>

  Note: the items below MUST ALL be recorded in xxx TODO

\<close>

consts

  Calculate    :: "[char list, 'a] => 'a"

  Rewrite      :: "[char list, 'a] => 'a"

  Rewrite'_Inst:: "[(char list * 'b) list, char list, 'a] => 'a"

			               ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for #>*)

  Rewrite'_Set :: "[char list, 'a] => 'a" ("(Rewrite'_Set (_))" 11)

  Rewrite'_Set'_Inst

               :: "[((char list) * 'b) list, char list, 'a] => 'a"

		                 ("(Rewrite'_Set'_Inst (_ _))" 11) (*without last argument ^^ for #>*)

  Or'_to'_List :: "bool => 'a list"  ("Or'_to'_List (_)" 11)

  SubProblem   :: "[char list * char list list * char list list, arg list] => 'a"

  Substitute   :: "[bool list, 'a] => 'a"

  Take         :: "'a => 'a"

  (* legacy.. *)

  Check'_elementwise :: (* TODO: is idle, retained for test purposes in Minisubpbl *)

		  "['a list, 'b set] => 'a list" ("Check'_elementwise (_ _)" 11)

  Assumptions  :: bool  (* TODO: remove with making ^^^ idle *)

subsection \<open>ML code for Prog_Tac\<close>

ML \<open>

signature PROGAM_TACTIC =

sig

  val dest_spec : term -> Celem.spec

  val get_stac : 'a -> term -> term option (*rename get_first*)

  val eval_leaf: (term * term) list -> term option -> term -> term -> Program.leaf * term option

  val is: term -> bool

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

  (*NONE*)

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

  (*NONE*)

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

end 

\<close> ML \<open>

(**)

structure Prog_Tac(**): PROGAM_TACTIC(**) =

struct

(**)

fun dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) $ p $ m)) =

    (d |> HOLogic.dest_string, 

     p |> HOLogic.dest_list |> map HOLogic.dest_string,

     m |> HOLogic.dest_list |> map HOLogic.dest_string) : Celem.spec

  | dest_spec t = raise TERM ("dest_spec: called with ", [t])

(* get argument of first Prog_Tac in a progam for init_form *)

fun get_stac thy (_ $ body) =

  let

    (* entries occur twice, for form curried by #> or non-curried *)

    fun get_t y (Const ("Tactical.Chain",_) $ e1 $ e2) a = 

    	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)

      | get_t y (Const ("Tactical.Chain",_) $ e1 $ e2 $ a) _ = 

    	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)

      | get_t y (Const ("Tactical.Try",_) $ e) a = get_t y e a

      | get_t y (Const ("Tactical.Try",_) $ e $ a) _ = get_t y e a

      | get_t y (Const ("Tactical.Repeat",_) $ e) a = get_t y e a

      | get_t y (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t y e a

      | get_t y (Const ("Tactical.Or",_) $e1 $ e2) a =

    	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)

      | get_t y (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ =

    	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)

      | get_t y (Const ("Tactical.While",_) $ _ $ e) a = get_t y e a

      | get_t y (Const ("Tactical.While",_) $ _ $ e $ a) _ = get_t y e a

      | get_t y (Const ("Tactical.Letpar",_) $ e1 $ Abs (_, _, e2)) a = 

    	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)

      | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a =

    	  get_t y e1 a (* don't go deeper without evaluation *)

      | get_t _ (Const ("If", _) $ _ $ _ $ _) _ = NONE

      | get_t _ (Const ("Prog_Tac.Rewrite",_) $ _ $ a) _ = SOME a

      | get_t _ (Const ("Prog_Tac.Rewrite",_) $ _ ) a = SOME a

      | get_t _ (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ $ a) _ = SOME a

      | get_t _ (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ )    a = SOME a

      | get_t _ (Const ("Prog_Tac.Rewrite'_Set",_) $ _ $ a) _ = SOME a

      | get_t _ (Const ("Prog_Tac.Rewrite'_Set",_) $ _ )    a = SOME a

      | get_t _ (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ $a)_ =SOME a

      | get_t _ (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ )  a =SOME a

      | get_t _ (Const ("Prog_Tac.Calculate",_) $ _ $ a) _ = SOME a

      | get_t _ (Const ("Prog_Tac.Calculate",_) $ _ )    a = SOME a

      | get_t _ (Const ("Prog_Tac.Substitute",_) $ _ $ a) _ = SOME a

      | get_t _ (Const ("Prog_Tac.Substitute",_) $ _ )    a = SOME a

      | get_t _ (Const ("Prog_Tac.SubProblem",_) $ _ $ _) _ = NONE

      | get_t _ _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)

    in get_t thy body Rule.e_term end

  | get_stac _ t = error ("get_stac: no fun-def. for " ^ Rule.term2str t);

(* substitute the Istate.T's environment to a leaf of the program

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

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 Program.Expr by fall-through.

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

fun eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) =

    (Program.Tac (subst_atomic E t), NONE)

  | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) =

    (Program.Tac (

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

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

    a)

  | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Inst"(*1*), _) $ _ $ _ $ _)) =

    (Program.Tac (subst_atomic E t), NONE)

  | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Inst"(*2*), _) $ _ $ _)) =

    (Program.Tac (

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

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

    a)

  | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set"(*1*), _) $ _ $ _)) =

    (Program.Tac (subst_atomic E t), NONE)

  | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Set"(*2*), _) $ _)) =

    (Program.Tac (

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

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

    a)

  | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*1*), _) $ _ $ _ $ _)) =

    (Program.Tac (subst_atomic E t), NONE)

  | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*2*), _) $ _ $ _)) =

    (Program.Tac (

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

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

    a)

  | eval_leaf E _ _ (t as (Const ("Prog_Tac.Calculate"(*1*), _) $ _ $ _)) =

    (Program.Tac (subst_atomic E t), NONE)

  | eval_leaf E a v (t as (Const ("Prog_Tac.Calculate"(*2*), _) $ _)) =

    (Program.Tac (

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

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

    a)

  | eval_leaf E _ _ (t as (Const ("Prog_Tac.Check'_elementwise"(*1*),_) $ _ $ _)) = 

    (Program.Tac (subst_atomic E t), NONE)

  | eval_leaf E a v (t as (Const ("Prog_Tac.Check'_elementwise"(*2*), _) $ _)) = 

    (Program.Tac (

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

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

    a)

  | eval_leaf E _ _ (t as (Const ("Prog_Tac.Or'_to'_List"(*1*), _) $ _)) = 

    (Program.Tac (subst_atomic E t), NONE)

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

    (Program.Tac (

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

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

    a)

  | eval_leaf E _ _ (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =

    (Program.Tac (subst_atomic E t), NONE)

  | eval_leaf E _ _ (t as (Const ("Prog_Tac.Take", _) $ _)) =

    (Program.Tac (subst_atomic E t), NONE)

  | eval_leaf E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) =

    (Program.Tac (subst_atomic E t), NONE)

  | eval_leaf E a v (t as (Const ("Prog_Tac.Substitute"(*2*), _) $ _)) =

    (Program.Tac (

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

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

    a)

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

  | eval_leaf E a v t = 

    (Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t), a);

(* check if a term is a Prog_Tac *)

val SOME Calculate = TermC.parseNEW @{context} "Calculate";

val SOME Rewrite = TermC.parseNEW @{context} "Rewrite";

val SOME Rewrite_Inst = TermC.parseNEW @{context} "Rewrite'_Inst";

val SOME Rewrite_Set = TermC.parseNEW @{context} "Rewrite'_Set";

val SOME Rewrite_Set_Inst = TermC.parseNEW @{context} "Rewrite'_Set'_Inst";

val SOME Or_to_List = TermC.parseNEW @{context} "Or'_to'_List";

val SOME SubProblem = TermC.parseNEW @{context} "SubProblem";

val SOME Substitute = TermC.parseNEW @{context} "Substitute";

val SOME Take = TermC.parseNEW @{context} "Take";

val SOME Check_elementwise = TermC.parseNEW @{context} "Check'_elementwise";

val SOME Assumptions = TermC.parseNEW @{context} "Assumptions";

val all_Consts = [Calculate, Rewrite, Rewrite_Inst, Rewrite_Set, Rewrite_Set_Inst, Or_to_List,

  SubProblem, Substitute, Take, Check_elementwise, Assumptions]

fun is t = TermC.contains_Const_typeless all_Consts t

(**)end(**)

\<close> ML \<open>

\<close> 

subsection \<open>TODO\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> 

end