(* Title:  tactics, tacticals etc. for scripts

   Author: Walther Neuper 000224

   (c) due to copyright terms

 *)

theory Prog_Tac

  imports "~~/src/Tools/isac/CalcElements/CalcElements"

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.. *)

  Calculate1   :: "[char list, 'a] => 'a" (* unknown to lucas-interpreter *)

  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>TODO\<close>

ML \<open>

signature PROGAM_TACTIC =

sig

  val dest_spec : term -> Celem.spec

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

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

(* ---- 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 Celem.Expr by fall-through.

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

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

    (NONE, Celem.STac (subst_atomic E t))

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

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

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

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

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

    (NONE, Celem.STac (subst_atomic E t))

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

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

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

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

    (NONE, Celem.STac (subst_atomic E t))

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

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

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

  | subst_stacexpr E _ _ 

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

    (NONE, Celem.STac (subst_atomic E t))

  | subst_stacexpr E a v 

	      (t as (*2*)(Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _)) =

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

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

  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Calculate", _) $ _ $ _)) =

    (NONE, Celem.STac (subst_atomic E t))

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

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

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

  | subst_stacexpr E _ _ 

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

    (NONE, Celem.STac (subst_atomic E t))

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

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

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

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

    (NONE, Celem.STac (subst_atomic E t))

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

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

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

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

    (NONE, Celem.STac (subst_atomic E t))

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

    (NONE, Celem.STac (subst_atomic E t))

  | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Substitute", _) $ _ $ _)) =

    (NONE, Celem.STac (subst_atomic E t))

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

    (a, Celem.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, Celem.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t));

(**)end(**)

\<close> ML \<open>

\<close> 

subsection \<open>TODO\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> 

end