(* Title:  tacticals for programs

    Author: Walther Neuper, Aug.2019

    (c) due to copyright terms

  *)

 theory Tactical

   imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"

 begin

 text \<open>Abstract:

   Define specific constants for tacticals, which determine the flow of evaluation in programs.

   Tacticals are not visible in calculations, which are generated by programs as a side effect.

 \<close>

 subsection \<open>Consts for tacticals\<close>

 consts

   Chain    :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10)

   Try      :: "['a => 'a, 'a] => 'a"

   Repeat   :: "['a => 'a, 'a] => 'a" 

   Or       :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)

   While    :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)

   If       :: "[bool, 'a, 'a] => 'a"       ("(If (_)/ Then (_)/ Else (_))" 10)

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

 ML \<open>

 signature TACTICAL =

 sig

   val is: term -> bool

   val contained_in: term -> bool

 end

 \<close> ML \<open>

 (**)

 structure Tactical(**): TACTICAL(**) =

 struct

 (**)

 val SOME (Let $ _ $ _) = ParseC.term_opt @{context} "let aaa = 1 in aaa"

 val SOME (Chain) = ParseC.term_opt @{context} "Chain";

 val SOME (Try) = ParseC.term_opt @{context} "Try";

 val SOME (Repeat) = ParseC.term_opt @{context} "Repeat";

 val SOME (Or $ _ $ _) = ParseC.term_opt @{context} "aaa Or bbb";

 val SOME (While $ _ $ _) = ParseC.term_opt @{context} "While aaa Do bbb";

 val SOME (If $ _ $ _ $ _) = ParseC.term_opt @{context} "If aaa Then bbb Else ccc";

 val all_Consts = [Let, Chain, Try, Repeat, Or, While, If]

 fun is t = TermC.contains_Const_typeless all_Consts t

 fun contained_in t =

   let

     fun eqal (Const (fid, _), Const (constid, _)) = fid = constid

       | eqal _ = false

     val (f, args) = strip_comb t

   in

     if member eqal all_Consts f

     then true

     else fold cor_ (map contained_in args) false

   end 

 (**)end(**)

 \<close> ML \<open>

 \<close>

 end