wneuper@59601: (* Title:  tactics, tacticals etc. for scripts
wneuper@59601:    Author: Walther Neuper 000224
wneuper@59601:    (c) due to copyright terms
walther@60335: 
walther@60400: TODO: rearrange thy dependency such that "Tactical.Chain" etc are known const_name
wneuper@59601:  *)
wneuper@59601: 
walther@59603: theory Prog_Tac
walther@59717:   imports Program
walther@59603: begin
wneuper@59601: 
walther@59619: text \<open>Abstract:
walther@59619:   Specific constants for tactics in programs, which each create a step in a calculation
walther@59619:   as a side effect.
walther@59619:   These program-tactics are related to Tactic.input for use in calculations and
walther@59619:   Tactic.T for internal use by lucas-interpretation.
walther@59619: \<close>
walther@59619: 
wneuper@59601: subsection \<open>arguments of tactic SubProblem\<close>
wneuper@59601: 
wneuper@59601: typedecl
wneuper@59601:   arg
wneuper@59601: 
wneuper@59601: consts
wneuper@59601:   REAL        :: "real => arg"
wneuper@59601:   REAL_LIST   :: "(real list) => arg"
wneuper@59601:   REAL_SET    :: "(real set) => arg"
wneuper@59601:   BOOL        :: "bool => arg"
wneuper@59601:   BOOL_LIST   :: "(bool list) => arg"
wneuper@59601:   REAL_REAL   :: "(real => real) => arg"
wneuper@59601:   STRING      :: "(char list) => arg"
wneuper@59601:   STRING_LIST :: "(char list list) => arg"
wneuper@59601: 
wneuper@59601: subsection \<open>tactics in programs\<close>
wneuper@59601: text \<open>
wneuper@59601:   Note: the items below MUST ALL be recorded in xxx TODO
wneuper@59601: \<close>
wneuper@59601: consts
walther@59634:   Calculate    :: "[char list, 'a] => 'a"
walther@59635:   Rewrite      :: "[char list, 'a] => 'a"
walther@60278:   Rewrite_Inst:: "[(char list * 'b) list, char list, 'a] => 'a"
walther@59637: 			               ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
walther@60278:   Rewrite_Set :: "[char list, 'a] => 'a" ("(Rewrite'_Set (_))" 11)
walther@60278:   Rewrite_Set_Inst
walther@59636:                :: "[((char list) * 'b) list, char list, 'a] => 'a"
walther@59637: 		                 ("(Rewrite'_Set'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
walther@60278:   Or_to_List :: "bool => 'a list"  ("Or'_to'_List (_)" 11)
walther@59634:   SubProblem   :: "[char list * char list list * char list list, arg list] => 'a"
walther@59634:   Substitute   :: "[bool list, 'a] => 'a"
walther@59634:   Take         :: "'a => 'a"
walther@59634: 
walther@59635:   (* legacy.. *)
walther@60278:   Check_elementwise :: (* TODO: is idle, retained for test purposes in Minisubpbl *)
wneuper@59601: 		  "['a list, 'b set] => 'a list" ("Check'_elementwise (_ _)" 11)
wneuper@59601:   Assumptions  :: bool  (* TODO: remove with making ^^^ idle *)
walther@59634: 
wneuper@59601: 
walther@59716: subsection \<open>ML code for Prog_Tac\<close>
wneuper@59601: ML \<open>
wneuper@59601: signature PROGAM_TACTIC =
wneuper@59601: sig
walther@59985:   val dest_spec : term -> References_Def.T
walther@59848:   val get_first_argument : term -> term option (*TODO rename get_first_argument*)
walther@59800:   val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option
walther@59716:   val is: term -> bool
Walther@60567: 
Walther@60567:   val Substitute_adapt_to_type: theory -> term -> Subst.as_string_eqs
Walther@60567: (**)val Rewrite_Inst_adapt_to_type: theory -> term -> TermC.as_string list(**)
Walther@60567: (**)val Take_adapt_to_type: Proof.context -> TermC.as_string -> term(**)
Walther@60567: end
wneuper@59601: \<close> ML \<open>
wneuper@59601: (**)
wneuper@59601: structure Prog_Tac(**): PROGAM_TACTIC(**) =
wneuper@59601: struct
wneuper@59601: (**)
wneuper@59601: 
wenzelm@60309: fun dest_spec (Const (\<^const_name>\<open>Pair\<close>, _) $ d $ (Const (\<^const_name>\<open>Pair\<close>, _) $ p $ m)) =
walther@59618:     (d |> HOLogic.dest_string, 
walther@59618:      p |> HOLogic.dest_list |> map HOLogic.dest_string,
walther@59985:      m |> HOLogic.dest_list |> map HOLogic.dest_string) : References_Def.T
walther@59618:   | dest_spec t = raise TERM ("dest_spec: called with ", [t])
walther@59618: 
walther@59845: (* get argument of first Prog_Tac in a progam for implicit_take *)
walther@59848: fun get_first_argument (_ $ body) =
wneuper@59601:   let
walther@59637:     (* entries occur twice, for form curried by #> or non-curried *)
walther@59848:     fun get_t (Const ("Tactical.Chain",_) $ e1 $ e2) a = 
walther@59848:     	  (case get_t e1 a of NONE => get_t e2 a | la => la)
walther@59848:       | get_t (Const ("Tactical.Chain",_) $ e1 $ e2 $ a) _ = 
walther@59848:     	  (case get_t e1 a of NONE => get_t e2 a | la => la)
walther@59848:       | get_t (Const ("Tactical.Try",_) $ e) a = get_t e a
walther@59848:       | get_t (Const ("Tactical.Try",_) $ e $ a) _ = get_t e a
walther@60335:       | get_t (Const ("Tactical.Repeat", _) $ e) a = get_t e a
walther@59848:       | get_t (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t e a
walther@59848:       | get_t (Const ("Tactical.Or",_) $e1 $ e2) a =
walther@59848:     	  (case get_t e1 a of NONE => get_t e2 a | la => la)
walther@59848:       | get_t (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ =
walther@59848:     	  (case get_t e1 a of NONE => get_t e2 a | la => la)
walther@59848:       | get_t (Const ("Tactical.While",_) $ _ $ e) a = get_t e a
walther@60335:       | get_t (Const ("Tactical.While", _) $ _ $ e $ a) _ = get_t e a
walther@60335:       | get_t (Const ("Tactical.Letpar", _) $ e1 $ Abs (_, _, e2)) a = 
walther@59848:     	  (case get_t e1 a of NONE => get_t e2 a | la => la)
walther@60335:       | get_t (Const (\<^const_name>\<open>Let\<close>, _) $ e1 $ Abs (_, _, _)) a =
walther@59848:     	  get_t e1 a (* don't go deeper without evaluation *)
walther@59848:       | get_t (Const ("If", _) $ _ $ _ $ _) _ = NONE
wneuper@59601:     
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>,_) $ _ $ a) _ = SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>,_) $ _ ) a = SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>,_) $ _ $ _ $ a) _ = SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>,_) $ _ $ _ )    a = SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ _ $ a) _ = SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ _ )    a = SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ _ $a)_ =SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ _ )  a =SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ $ a) _ = SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ )    a = SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>,_) $ _ $ a) _ = SOME a
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>,_) $ _ )    a = SOME a
wneuper@59601:     
walther@60335:       | get_t (Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>,_) $ _ $ _) _ = NONE
wneuper@59601: 
walther@59848:       | get_t _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
walther@59861:     in get_t body TermC.empty end
walther@59962:   | get_first_argument t = raise ERROR ("get_first_argument: no fun-def. for " ^ UnparseC.term t);
wneuper@59601: 
walther@59635: (* substitute the Istate.T's environment to a leaf of the program
wneuper@59601:    and attach the curried argument of a tactic, if any.
walther@59637: CAUTION: (1) currying with #> requires 2 patterns for each tactic
wneuper@59601:          (2) the non-curried version must return NONE for a 
walther@59800: 	       (3) non-matching patterns become a Prog_Expr by fall-through.
wneuper@59601: WN060906 quick and dirty fix: due to (2) a is returned, too *)
walther@59718: fun eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) =
walther@59729:     (Program.Tac (subst_atomic E t), NONE)
walther@59718:   | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) =
walther@59729:     (Program.Tac (
walther@59800:       case a of SOME a' => (subst_atomic E (t $ a'))          
walther@59729: 		          | NONE => ((subst_atomic E t) $ v)),
walther@59729:     a)
walther@60278:   | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Inst"(*1*), _) $ _ $ _ $ _)) =
walther@59729:     (Program.Tac (subst_atomic E t), NONE)
walther@60278:   | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Inst"(*2*), _) $ _ $ _)) =
walther@59729:     (Program.Tac (
walther@59717:       case a of SOME a' => subst_atomic E (t $ a')
walther@59729: 	            | NONE => ((subst_atomic E t) $ v)),
walther@59729:     a)
walther@60278:   | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Set"(*1*), _) $ _ $ _)) =
walther@59729:     (Program.Tac (subst_atomic E t), NONE)
walther@60278:   | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Set"(*2*), _) $ _)) =
walther@59729:     (Program.Tac (
walther@59717:       case a of SOME a' => subst_atomic E (t $ a')
walther@59729: 	            | NONE => ((subst_atomic E t) $ v)),
walther@59729:     a)
walther@60278:   | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Set_Inst"(*1*), _) $ _ $ _ $ _)) =
walther@59729:     (Program.Tac (subst_atomic E t), NONE)
walther@60278:   | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Set_Inst"(*2*), _) $ _ $ _)) =
walther@59729:     (Program.Tac (
walther@59717:       case a of SOME a' => subst_atomic E (t $ a')
walther@59729: 	            | NONE => ((subst_atomic E t) $ v)),
walther@59729:     a)
walther@59718:   | eval_leaf E _ _ (t as (Const ("Prog_Tac.Calculate"(*1*), _) $ _ $ _)) =
walther@59729:     (Program.Tac (subst_atomic E t), NONE)
walther@59718:   | eval_leaf E a v (t as (Const ("Prog_Tac.Calculate"(*2*), _) $ _)) =
walther@59729:     (Program.Tac (
walther@59717:       case a of SOME a' => subst_atomic E (t $ a')
walther@59729: 	            | NONE => ((subst_atomic E t) $ v)),
walther@59729:     a)
walther@60278:   | eval_leaf E _ _ (t as (Const ("Prog_Tac.Check_elementwise"(*1*),_) $ _ $ _)) = 
walther@59729:     (Program.Tac (subst_atomic E t), NONE)
walther@60278:   | eval_leaf E a v (t as (Const ("Prog_Tac.Check_elementwise"(*2*), _) $ _)) = 
walther@59729:     (Program.Tac (
walther@59717:       case a of SOME a' => subst_atomic E (t $ a')
walther@59729: 		          | NONE => ((subst_atomic E t) $ v)),
walther@59729:     a)
walther@60278:   | eval_leaf E _ _ (t as (Const ("Prog_Tac.Or_to_List"(*1*), _) $ _)) = 
walther@59729:     (Program.Tac (subst_atomic E t), NONE)
walther@60278:   | eval_leaf E a v (t as (Const ("Prog_Tac.Or_to_List"(*2*), _))) = (*t $ v*)
walther@59729:     (Program.Tac (
walther@59717:       case a of SOME a' => subst_atomic E (t $ a')
walther@59729: 		          | NONE => ((subst_atomic E t) $ v)),
walther@59729:     a)
walther@60335:   | eval_leaf E _ _ (t as (Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
walther@59729:     (Program.Tac (subst_atomic E t), NONE)
walther@60335:   | eval_leaf E _ _ (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)) =
walther@59729:     (Program.Tac (subst_atomic E t), NONE)
walther@59718:   | eval_leaf E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) =
walther@59729:     (Program.Tac (subst_atomic E t), NONE)
walther@59718:   | eval_leaf E a v (t as (Const ("Prog_Tac.Substitute"(*2*), _) $ _)) =
walther@59729:     (Program.Tac (
walther@59717:       case a of SOME a' => subst_atomic E (t $ a')
walther@59729: 		          | NONE => ((subst_atomic E t) $ v)),
walther@59729:     a)
wneuper@59601:   (*now all tactics are matched out and this leaf must be without a tactic*)
walther@59718:   | eval_leaf E a v t = 
walther@59729:     (Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t), a);
wneuper@59601: 
walther@59716: 
walther@59716: (* check if a term is a Prog_Tac *)
walther@59716: 
walther@59716: val SOME Calculate = TermC.parseNEW @{context} "Calculate";
walther@59716: val SOME Rewrite = TermC.parseNEW @{context} "Rewrite";
walther@59716: val SOME Rewrite_Inst = TermC.parseNEW @{context} "Rewrite'_Inst";
walther@59716: val SOME Rewrite_Set = TermC.parseNEW @{context} "Rewrite'_Set";
walther@59716: val SOME Rewrite_Set_Inst = TermC.parseNEW @{context} "Rewrite'_Set'_Inst";
walther@59716: val SOME Or_to_List = TermC.parseNEW @{context} "Or'_to'_List";
walther@59716: val SOME SubProblem = TermC.parseNEW @{context} "SubProblem";
walther@59716: val SOME Substitute = TermC.parseNEW @{context} "Substitute";
walther@59716: val SOME Take = TermC.parseNEW @{context} "Take";
walther@59716: val SOME Check_elementwise = TermC.parseNEW @{context} "Check'_elementwise";
walther@59716: val SOME Assumptions = TermC.parseNEW @{context} "Assumptions";
walther@59716: 
walther@59716: val all_Consts = [Calculate, Rewrite, Rewrite_Inst, Rewrite_Set, Rewrite_Set_Inst, Or_to_List,
walther@59716:   SubProblem, Substitute, Take, Check_elementwise, Assumptions]
walther@59716: 
walther@59716: fun is t = TermC.contains_Const_typeless all_Consts t
Walther@60567: 
Walther@60567: 
Walther@60567: (** adapt_to_type arguments of specific tactics **)
Walther@60567: (*
Walther@60567:   Programs are stored as terms typed by the theory they are defined in.
Walther@60567:   Specific Prog_Tac take substitutions as arguments; these substitutions have
Walther@60567:   the variables to be substituted typed with the program;
Walther@60567:   these variables need to be adapt_to_type from the user-context in order to conform
Walther@60567:   with the terms input by the user.
Walther@60567: *)
Walther@60567: fun Substitute_adapt_to_type thy isasub = 
Walther@60567:   isasub
Walther@60567:   |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)
Walther@60567:   |> TermC.isalist2list
Walther@60567:   |> Subst.eqs_to_input;
Walther@60567: 
Walther@60567: fun Rewrite_Inst_adapt_to_type thy sub =
Walther@60567:   sub 
Walther@60567: (*|> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)*)
Walther@60567:   |> Subst.program_to_input
Walther@60567: 
Walther@60567: (*eliminated ERROR: c_2 = (0 :: 'a)*)
Walther@60567: fun Take_adapt_to_type ctxt arg = arg
Walther@60567:   |> TermC.parse ctxt
Walther@60567:   |> Model_Pattern.adapt_term_to_type ctxt
Walther@60567: 
Walther@60567: (**)end(*struct*)
wneuper@59601: \<close> ML \<open>
wneuper@59601: \<close> 
Walther@60567: 
wneuper@59601: subsection \<open>TODO\<close>
wneuper@59601: ML \<open>
wneuper@59601: \<close> ML \<open>
wneuper@59601: \<close> ML \<open>
wneuper@59601: \<close> 
wneuper@59601: end