(* Title:  tactics, tacticals etc. for scripts

   Author: Walther Neuper 000224

   (c) due to copyright terms

TODO: rearrange thy dependency such that "Tactical.Chain" etc are known const_name

 *)

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 -> References_Def.T

  val get_first_argument : term -> term option (*TODO rename get_first_argument*)

  val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option

  val is: term -> bool

  val Substitute_adapt_to_type: theory -> term -> Subst.as_string_eqs

(**)val Rewrite_Inst_adapt_to_type: theory -> term -> TermC.as_string list(**)

(**)val Take_adapt_to_type: Proof.context -> TermC.as_string -> term(**)

end

\<close> ML \<open>

(**)

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

struct

(**)

fun dest_spec (Const (\<^const_name>\<open>Pair\<close>, _) $ d $ (Const (\<^const_name>\<open>Pair\<close>, _) $ p $ m)) =

    (d |> HOLogic.dest_string, 

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

     m |> HOLogic.dest_list |> map HOLogic.dest_string) : References_Def.T

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

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

fun get_first_argument (_ $ body) =

  let

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      | get_t (Const (\<^const_name>\<open>Let\<close>, _) $ e1 $ Abs (_, _, _)) a =

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

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

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>,_) $ _ $ a) _ = SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>,_) $ _ ) a = SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>,_) $ _ $ _ $ a) _ = SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>,_) $ _ $ _ )    a = SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ _ $ a) _ = SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ _ )    a = SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ _ $a)_ =SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ _ )  a =SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ $ a) _ = SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ )    a = SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>,_) $ _ $ a) _ = SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>,_) $ _ )    a = SOME a

      | get_t (Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>,_) $ _ $ _) _ = NONE

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

    in get_t body TermC.empty end

  | get_first_argument t = raise ERROR ("get_first_argument: no fun-def. for " ^ UnparseC.term 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 a Prog_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 (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =

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

  | eval_leaf E _ _ (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)) =

    (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

(** adapt_to_type arguments of specific tactics **)

(*

  Programs are stored as terms typed by the theory they are defined in.

  Specific Prog_Tac take substitutions as arguments; these substitutions have

  the variables to be substituted typed with the program;

  these variables need to be adapt_to_type from the user-context in order to conform

  with the terms input by the user.

*)

fun Substitute_adapt_to_type thy isasub = 

  isasub

  |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)

  |> TermC.isalist2list

  |> Subst.eqs_to_input;

fun Rewrite_Inst_adapt_to_type thy sub =

  sub 

(*|> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)*)

  |> Subst.program_to_input

(*eliminated ERROR: c_2 = (0 :: 'a)*)

fun Take_adapt_to_type ctxt arg = arg

  |> TermC.parse ctxt

  |> Model_Pattern.adapt_term_to_type ctxt

(**)end(*struct*)

\<close> ML \<open>

\<close> 

subsection \<open>TODO\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> 

end