1 (* Title: tactics, tacticals etc. for scripts
2 Author: Walther Neuper 000224
3 (c) due to copyright terms
5 TODO: rearrange thy dependency such that "Tactical.Chain" etc are known const_name
13 Specific constants for tactics in programs, which each create a step in a calculation
15 These program-tactics are related to Tactic.input for use in calculations and
16 Tactic.T for internal use by lucas-interpretation.
19 subsection \<open>arguments of tactic SubProblem\<close>
26 REAL_LIST :: "(real list) => arg"
27 REAL_SET :: "(real set) => arg"
29 BOOL_LIST :: "(bool list) => arg"
30 REAL_REAL :: "(real => real) => arg"
31 STRING :: "(char list) => arg"
32 STRING_LIST :: "(char list list) => arg"
34 subsection \<open>tactics in programs\<close>
36 Note: the items below MUST ALL be recorded in xxx TODO
39 Calculate :: "[char list, 'a] => 'a"
40 Rewrite :: "[char list, 'a] => 'a"
41 Rewrite_Inst:: "[(char list * 'b) list, char list, 'a] => 'a"
42 ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
43 Rewrite_Set :: "[char list, 'a] => 'a" ("(Rewrite'_Set (_))" 11)
45 :: "[((char list) * 'b) list, char list, 'a] => 'a"
46 ("(Rewrite'_Set'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
47 Or_to_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
48 SubProblem :: "[char list * char list list * char list list, arg list] => 'a"
49 Substitute :: "[bool list, 'a] => 'a"
53 Check_elementwise :: (* TODO: is idle, retained for test purposes in Minisubpbl *)
54 "['a list, 'b set] => 'a list" ("Check'_elementwise (_ _)" 11)
55 Assumptions :: bool (* TODO: remove with making ^^^ idle *)
58 subsection \<open>ML code for Prog_Tac\<close>
60 signature PROGAM_TACTIC =
62 val dest_spec : term -> References_Def.T
63 val get_first_argument : term -> term option (*TODO rename get_first_argument*)
64 val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option
67 val Substitute_adapt_to_type: theory -> term -> Subst.as_string_eqs
68 (**)val Rewrite_Inst_adapt_to_type: theory -> term -> TermC.as_string list(**)
69 (**)val Take_adapt_to_type: Proof.context -> TermC.as_string -> term(**)
73 structure Prog_Tac(**): PROGAM_TACTIC(**) =
77 fun dest_spec (Const (\<^const_name>\<open>Pair\<close>, _) $ d $ (Const (\<^const_name>\<open>Pair\<close>, _) $ p $ m)) =
78 (d |> HOLogic.dest_string,
79 p |> HOLogic.dest_list |> map HOLogic.dest_string,
80 m |> HOLogic.dest_list |> map HOLogic.dest_string) : References_Def.T
81 | dest_spec t = raise TERM ("dest_spec: called with ", [t])
83 (* get argument of first Prog_Tac in a progam for implicit_take *)
84 fun get_first_argument (_ $ body) =
86 (* entries occur twice, for form curried by #> or non-curried *)
87 fun get_t (Const ("Tactical.Chain",_) $ e1 $ e2) a =
88 (case get_t e1 a of NONE => get_t e2 a | la => la)
89 | get_t (Const ("Tactical.Chain",_) $ e1 $ e2 $ a) _ =
90 (case get_t e1 a of NONE => get_t e2 a | la => la)
91 | get_t (Const ("Tactical.Try",_) $ e) a = get_t e a
92 | get_t (Const ("Tactical.Try",_) $ e $ a) _ = get_t e a
93 | get_t (Const ("Tactical.Repeat", _) $ e) a = get_t e a
94 | get_t (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t e a
95 | get_t (Const ("Tactical.Or",_) $e1 $ e2) a =
96 (case get_t e1 a of NONE => get_t e2 a | la => la)
97 | get_t (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ =
98 (case get_t e1 a of NONE => get_t e2 a | la => la)
99 | get_t (Const ("Tactical.While",_) $ _ $ e) a = get_t e a
100 | get_t (Const ("Tactical.While", _) $ _ $ e $ a) _ = get_t e a
101 | get_t (Const ("Tactical.Letpar", _) $ e1 $ Abs (_, _, e2)) a =
102 (case get_t e1 a of NONE => get_t e2 a | la => la)
103 | get_t (Const (\<^const_name>\<open>Let\<close>, _) $ e1 $ Abs (_, _, _)) a =
104 get_t e1 a (* don't go deeper without evaluation *)
105 | get_t (Const ("If", _) $ _ $ _ $ _) _ = NONE
107 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>,_) $ _ $ a) _ = SOME a
108 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>,_) $ _ ) a = SOME a
109 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>,_) $ _ $ _ $ a) _ = SOME a
110 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>,_) $ _ $ _ ) a = SOME a
111 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ _ $ a) _ = SOME a
112 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ _ ) a = SOME a
113 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ _ $a)_ =SOME a
114 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ _ ) a =SOME a
115 | get_t (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ $ a) _ = SOME a
116 | get_t (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ ) a = SOME a
117 | get_t (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>,_) $ _ $ a) _ = SOME a
118 | get_t (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>,_) $ _ ) a = SOME a
120 | get_t (Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>,_) $ _ $ _) _ = NONE
122 | get_t _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
123 in get_t body TermC.empty end
124 | get_first_argument t = raise ERROR ("get_first_argument: no fun-def. for " ^ UnparseC.term t);
126 (* substitute the Istate.T's environment to a leaf of the program
127 and attach the curried argument of a tactic, if any.
128 CAUTION: (1) currying with #> requires 2 patterns for each tactic
129 (2) the non-curried version must return NONE for a
130 (3) non-matching patterns become a Prog_Expr by fall-through.
131 WN060906 quick and dirty fix: due to (2) a is returned, too *)
132 fun eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) =
133 (Program.Tac (subst_atomic E t), NONE)
134 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) =
136 case a of SOME a' => (subst_atomic E (t $ a'))
137 | NONE => ((subst_atomic E t) $ v)),
139 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Inst"(*1*), _) $ _ $ _ $ _)) =
140 (Program.Tac (subst_atomic E t), NONE)
141 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Inst"(*2*), _) $ _ $ _)) =
143 case a of SOME a' => subst_atomic E (t $ a')
144 | NONE => ((subst_atomic E t) $ v)),
146 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Set"(*1*), _) $ _ $ _)) =
147 (Program.Tac (subst_atomic E t), NONE)
148 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Set"(*2*), _) $ _)) =
150 case a of SOME a' => subst_atomic E (t $ a')
151 | NONE => ((subst_atomic E t) $ v)),
153 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Set_Inst"(*1*), _) $ _ $ _ $ _)) =
154 (Program.Tac (subst_atomic E t), NONE)
155 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Set_Inst"(*2*), _) $ _ $ _)) =
157 case a of SOME a' => subst_atomic E (t $ a')
158 | NONE => ((subst_atomic E t) $ v)),
160 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Calculate"(*1*), _) $ _ $ _)) =
161 (Program.Tac (subst_atomic E t), NONE)
162 | eval_leaf E a v (t as (Const ("Prog_Tac.Calculate"(*2*), _) $ _)) =
164 case a of SOME a' => subst_atomic E (t $ a')
165 | NONE => ((subst_atomic E t) $ v)),
167 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Check_elementwise"(*1*),_) $ _ $ _)) =
168 (Program.Tac (subst_atomic E t), NONE)
169 | eval_leaf E a v (t as (Const ("Prog_Tac.Check_elementwise"(*2*), _) $ _)) =
171 case a of SOME a' => subst_atomic E (t $ a')
172 | NONE => ((subst_atomic E t) $ v)),
174 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Or_to_List"(*1*), _) $ _)) =
175 (Program.Tac (subst_atomic E t), NONE)
176 | eval_leaf E a v (t as (Const ("Prog_Tac.Or_to_List"(*2*), _))) = (*t $ v*)
178 case a of SOME a' => subst_atomic E (t $ a')
179 | NONE => ((subst_atomic E t) $ v)),
181 | eval_leaf E _ _ (t as (Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
182 (Program.Tac (subst_atomic E t), NONE)
183 | eval_leaf E _ _ (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)) =
184 (Program.Tac (subst_atomic E t), NONE)
185 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) =
186 (Program.Tac (subst_atomic E t), NONE)
187 | eval_leaf E a v (t as (Const ("Prog_Tac.Substitute"(*2*), _) $ _)) =
189 case a of SOME a' => subst_atomic E (t $ a')
190 | NONE => ((subst_atomic E t) $ v)),
192 (*now all tactics are matched out and this leaf must be without a tactic*)
193 | eval_leaf E a v t =
194 (Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t), a);
197 (* check if a term is a Prog_Tac *)
199 val SOME Calculate = TermC.parseNEW @{context} "Calculate";
200 val SOME Rewrite = TermC.parseNEW @{context} "Rewrite";
201 val SOME Rewrite_Inst = TermC.parseNEW @{context} "Rewrite'_Inst";
202 val SOME Rewrite_Set = TermC.parseNEW @{context} "Rewrite'_Set";
203 val SOME Rewrite_Set_Inst = TermC.parseNEW @{context} "Rewrite'_Set'_Inst";
204 val SOME Or_to_List = TermC.parseNEW @{context} "Or'_to'_List";
205 val SOME SubProblem = TermC.parseNEW @{context} "SubProblem";
206 val SOME Substitute = TermC.parseNEW @{context} "Substitute";
207 val SOME Take = TermC.parseNEW @{context} "Take";
208 val SOME Check_elementwise = TermC.parseNEW @{context} "Check'_elementwise";
209 val SOME Assumptions = TermC.parseNEW @{context} "Assumptions";
211 val all_Consts = [Calculate, Rewrite, Rewrite_Inst, Rewrite_Set, Rewrite_Set_Inst, Or_to_List,
212 SubProblem, Substitute, Take, Check_elementwise, Assumptions]
214 fun is t = TermC.contains_Const_typeless all_Consts t
217 (** adapt_to_type arguments of specific tactics **)
219 Programs are stored as terms typed by the theory they are defined in.
220 Specific Prog_Tac take substitutions as arguments; these substitutions have
221 the variables to be substituted typed with the program;
222 these variables need to be adapt_to_type from the user-context in order to conform
223 with the terms input by the user.
225 fun Substitute_adapt_to_type thy isasub =
227 |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)
228 |> TermC.isalist2list
229 |> Subst.eqs_to_input;
231 fun Rewrite_Inst_adapt_to_type thy sub =
233 (*|> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)*)
234 |> Subst.program_to_input
236 (*eliminated ERROR: c_2 = (0 :: 'a)*)
237 fun Take_adapt_to_type ctxt arg = arg
239 |> Model_Pattern.adapt_term_to_type ctxt
245 subsection \<open>TODO\<close>