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
69 structure Prog_Tac(**): PROGAM_TACTIC(**) =
73 fun dest_spec (Const (\<^const_name>\<open>Pair\<close>, _) $ d $ (Const (\<^const_name>\<open>Pair\<close>, _) $ p $ m)) =
74 (d |> HOLogic.dest_string,
75 p |> HOLogic.dest_list |> map HOLogic.dest_string,
76 m |> HOLogic.dest_list |> map HOLogic.dest_string) : References_Def.T
77 | dest_spec t = raise TERM ("dest_spec: called with ", [t])
79 (* get argument of first Prog_Tac in a progam for implicit_take *)
80 fun get_first_argument (_ $ body) =
82 (* entries occur twice, for form curried by #> or non-curried *)
83 fun get_t (Const ("Tactical.Chain",_) $ e1 $ e2) a =
84 (case get_t e1 a of NONE => get_t e2 a | la => la)
85 | get_t (Const ("Tactical.Chain",_) $ e1 $ e2 $ a) _ =
86 (case get_t e1 a of NONE => get_t e2 a | la => la)
87 | get_t (Const ("Tactical.Try",_) $ e) a = get_t e a
88 | get_t (Const ("Tactical.Try",_) $ e $ a) _ = get_t e a
89 | get_t (Const ("Tactical.Repeat", _) $ e) a = get_t e a
90 | get_t (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t e a
91 | get_t (Const ("Tactical.Or",_) $e1 $ e2) a =
92 (case get_t e1 a of NONE => get_t e2 a | la => la)
93 | get_t (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ =
94 (case get_t e1 a of NONE => get_t e2 a | la => la)
95 | get_t (Const ("Tactical.While",_) $ _ $ e) a = get_t e a
96 | get_t (Const ("Tactical.While", _) $ _ $ e $ a) _ = get_t e a
97 | get_t (Const ("Tactical.Letpar", _) $ e1 $ Abs (_, _, e2)) a =
98 (case get_t e1 a of NONE => get_t e2 a | la => la)
99 | get_t (Const (\<^const_name>\<open>Let\<close>, _) $ e1 $ Abs (_, _, _)) a =
100 get_t e1 a (* don't go deeper without evaluation *)
101 | get_t (Const ("If", _) $ _ $ _ $ _) _ = NONE
103 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>,_) $ _ $ a) _ = SOME a
104 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>,_) $ _ ) a = SOME a
105 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>,_) $ _ $ _ $ a) _ = SOME a
106 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>,_) $ _ $ _ ) a = SOME a
107 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ _ $ a) _ = SOME a
108 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ _ ) a = SOME a
109 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ _ $a)_ =SOME a
110 | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ _ ) a =SOME a
111 | get_t (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ $ a) _ = SOME a
112 | get_t (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ ) a = SOME a
113 | get_t (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>,_) $ _ $ a) _ = SOME a
114 | get_t (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>,_) $ _ ) a = SOME a
116 | get_t (Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>,_) $ _ $ _) _ = NONE
118 | get_t _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
119 in get_t body TermC.empty end
120 | get_first_argument t = raise ERROR ("get_first_argument: no fun-def. for " ^ UnparseC.term t);
122 (* substitute the Istate.T's environment to a leaf of the program
123 and attach the curried argument of a tactic, if any.
124 CAUTION: (1) currying with #> requires 2 patterns for each tactic
125 (2) the non-curried version must return NONE for a
126 (3) non-matching patterns become a Prog_Expr by fall-through.
127 WN060906 quick and dirty fix: due to (2) a is returned, too *)
128 fun eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) =
129 (Program.Tac (subst_atomic E t), NONE)
130 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) =
132 case a of SOME a' => (subst_atomic E (t $ a'))
133 | NONE => ((subst_atomic E t) $ v)),
135 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Inst"(*1*), _) $ _ $ _ $ _)) =
136 (Program.Tac (subst_atomic E t), NONE)
137 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Inst"(*2*), _) $ _ $ _)) =
139 case a of SOME a' => subst_atomic E (t $ a')
140 | NONE => ((subst_atomic E t) $ v)),
142 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Set"(*1*), _) $ _ $ _)) =
143 (Program.Tac (subst_atomic E t), NONE)
144 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Set"(*2*), _) $ _)) =
146 case a of SOME a' => subst_atomic E (t $ a')
147 | NONE => ((subst_atomic E t) $ v)),
149 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Set_Inst"(*1*), _) $ _ $ _ $ _)) =
150 (Program.Tac (subst_atomic E t), NONE)
151 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Set_Inst"(*2*), _) $ _ $ _)) =
153 case a of SOME a' => subst_atomic E (t $ a')
154 | NONE => ((subst_atomic E t) $ v)),
156 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Calculate"(*1*), _) $ _ $ _)) =
157 (Program.Tac (subst_atomic E t), NONE)
158 | eval_leaf E a v (t as (Const ("Prog_Tac.Calculate"(*2*), _) $ _)) =
160 case a of SOME a' => subst_atomic E (t $ a')
161 | NONE => ((subst_atomic E t) $ v)),
163 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Check_elementwise"(*1*),_) $ _ $ _)) =
164 (Program.Tac (subst_atomic E t), NONE)
165 | eval_leaf E a v (t as (Const ("Prog_Tac.Check_elementwise"(*2*), _) $ _)) =
167 case a of SOME a' => subst_atomic E (t $ a')
168 | NONE => ((subst_atomic E t) $ v)),
170 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Or_to_List"(*1*), _) $ _)) =
171 (Program.Tac (subst_atomic E t), NONE)
172 | eval_leaf E a v (t as (Const ("Prog_Tac.Or_to_List"(*2*), _))) = (*t $ v*)
174 case a of SOME a' => subst_atomic E (t $ a')
175 | NONE => ((subst_atomic E t) $ v)),
177 | eval_leaf E _ _ (t as (Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
178 (Program.Tac (subst_atomic E t), NONE)
179 | eval_leaf E _ _ (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)) =
180 (Program.Tac (subst_atomic E t), NONE)
181 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) =
182 (Program.Tac (subst_atomic E t), NONE)
183 | eval_leaf E a v (t as (Const ("Prog_Tac.Substitute"(*2*), _) $ _)) =
185 case a of SOME a' => subst_atomic E (t $ a')
186 | NONE => ((subst_atomic E t) $ v)),
188 (*now all tactics are matched out and this leaf must be without a tactic*)
189 | eval_leaf E a v t =
190 (Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t), a);
193 (* check if a term is a Prog_Tac *)
195 val SOME Calculate = TermC.parseNEW @{context} "Calculate";
196 val SOME Rewrite = TermC.parseNEW @{context} "Rewrite";
197 val SOME Rewrite_Inst = TermC.parseNEW @{context} "Rewrite'_Inst";
198 val SOME Rewrite_Set = TermC.parseNEW @{context} "Rewrite'_Set";
199 val SOME Rewrite_Set_Inst = TermC.parseNEW @{context} "Rewrite'_Set'_Inst";
200 val SOME Or_to_List = TermC.parseNEW @{context} "Or'_to'_List";
201 val SOME SubProblem = TermC.parseNEW @{context} "SubProblem";
202 val SOME Substitute = TermC.parseNEW @{context} "Substitute";
203 val SOME Take = TermC.parseNEW @{context} "Take";
204 val SOME Check_elementwise = TermC.parseNEW @{context} "Check'_elementwise";
205 val SOME Assumptions = TermC.parseNEW @{context} "Assumptions";
207 val all_Consts = [Calculate, Rewrite, Rewrite_Inst, Rewrite_Set, Rewrite_Set_Inst, Or_to_List,
208 SubProblem, Substitute, Take, Check_elementwise, Assumptions]
210 fun is t = TermC.contains_Const_typeless all_Consts t
214 subsection \<open>TODO\<close>