1 (* Title: tactics, tacticals etc. for scripts
2 Author: Walther Neuper 000224
3 (c) due to copyright terms
11 Specific constants for tactics in programs, which each create a step in a calculation
13 These program-tactics are related to Tactic.input for use in calculations and
14 Tactic.T for internal use by lucas-interpretation.
17 subsection \<open>arguments of tactic SubProblem\<close>
24 REAL_LIST :: "(real list) => arg"
25 REAL_SET :: "(real set) => arg"
27 BOOL_LIST :: "(bool list) => arg"
28 REAL_REAL :: "(real => real) => arg"
29 STRING :: "(char list) => arg"
30 STRING_LIST :: "(char list list) => arg"
32 subsection \<open>tactics in programs\<close>
34 Note: the items below MUST ALL be recorded in xxx TODO
37 Calculate :: "[char list, 'a] => 'a"
38 Rewrite :: "[char list, 'a] => 'a"
39 Rewrite'_Inst:: "[(char list * 'b) list, char list, 'a] => 'a"
40 ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
41 Rewrite'_Set :: "[char list, 'a] => 'a" ("(Rewrite'_Set (_))" 11)
43 :: "[((char list) * 'b) list, char list, 'a] => 'a"
44 ("(Rewrite'_Set'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
45 Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
46 SubProblem :: "[char list * char list list * char list list, arg list] => 'a"
47 Substitute :: "[bool list, 'a] => 'a"
51 Check'_elementwise :: (* TODO: is idle, retained for test purposes in Minisubpbl *)
52 "['a list, 'b set] => 'a list" ("Check'_elementwise (_ _)" 11)
53 Assumptions :: bool (* TODO: remove with making ^^^ idle *)
56 subsection \<open>ML code for Prog_Tac\<close>
58 signature PROGAM_TACTIC =
60 val dest_spec : term -> Spec.T
61 val get_first_argument : term -> term option (*TODO rename get_first_argument*)
62 val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option
64 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
66 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
68 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
72 structure Prog_Tac(**): PROGAM_TACTIC(**) =
76 fun dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) $ p $ m)) =
77 (d |> HOLogic.dest_string,
78 p |> HOLogic.dest_list |> map HOLogic.dest_string,
79 m |> HOLogic.dest_list |> map HOLogic.dest_string) : Spec.T
80 | dest_spec t = raise TERM ("dest_spec: called with ", [t])
82 (* get argument of first Prog_Tac in a progam for implicit_take *)
83 fun get_first_argument (_ $ body) =
85 (* entries occur twice, for form curried by #> or non-curried *)
86 fun get_t (Const ("Tactical.Chain",_) $ e1 $ e2) a =
87 (case get_t e1 a of NONE => get_t e2 a | la => la)
88 | get_t (Const ("Tactical.Chain",_) $ e1 $ e2 $ a) _ =
89 (case get_t e1 a of NONE => get_t e2 a | la => la)
90 | get_t (Const ("Tactical.Try",_) $ e) a = get_t e a
91 | get_t (Const ("Tactical.Try",_) $ e $ a) _ = get_t e a
92 | get_t (Const ("Tactical.Repeat",_) $ e) a = get_t e a
93 | get_t (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t e a
94 | get_t (Const ("Tactical.Or",_) $e1 $ e2) a =
95 (case get_t e1 a of NONE => get_t e2 a | la => la)
96 | get_t (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ =
97 (case get_t e1 a of NONE => get_t e2 a | la => la)
98 | get_t (Const ("Tactical.While",_) $ _ $ e) a = get_t e a
99 | get_t (Const ("Tactical.While",_) $ _ $ e $ a) _ = get_t e a
100 | get_t (Const ("Tactical.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
101 (case get_t e1 a of NONE => get_t e2 a | la => la)
102 | get_t (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a =
103 get_t e1 a (* don't go deeper without evaluation *)
104 | get_t (Const ("If", _) $ _ $ _ $ _) _ = NONE
106 | get_t (Const ("Prog_Tac.Rewrite",_) $ _ $ a) _ = SOME a
107 | get_t (Const ("Prog_Tac.Rewrite",_) $ _ ) a = SOME a
108 | get_t (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ $ a) _ = SOME a
109 | get_t (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ ) a = SOME a
110 | get_t (Const ("Prog_Tac.Rewrite'_Set",_) $ _ $ a) _ = SOME a
111 | get_t (Const ("Prog_Tac.Rewrite'_Set",_) $ _ ) a = SOME a
112 | get_t (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ $a)_ =SOME a
113 | get_t (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ ) a =SOME a
114 | get_t (Const ("Prog_Tac.Calculate",_) $ _ $ a) _ = SOME a
115 | get_t (Const ("Prog_Tac.Calculate",_) $ _ ) a = SOME a
116 | get_t (Const ("Prog_Tac.Substitute",_) $ _ $ a) _ = SOME a
117 | get_t (Const ("Prog_Tac.Substitute",_) $ _ ) a = SOME a
119 | get_t (Const ("Prog_Tac.SubProblem",_) $ _ $ _) _ = NONE
121 | get_t _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
122 in get_t body TermC.empty end
123 | get_first_argument t = error ("get_first_argument: no fun-def. for " ^ UnparseC.term t);
125 (* substitute the Istate.T's environment to a leaf of the program
126 and attach the curried argument of a tactic, if any.
127 CAUTION: (1) currying with #> requires 2 patterns for each tactic
128 (2) the non-curried version must return NONE for a
129 (3) non-matching patterns become a Prog_Expr by fall-through.
130 WN060906 quick and dirty fix: due to (2) a is returned, too *)
131 fun eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) =
132 (Program.Tac (subst_atomic E t), NONE)
133 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) =
135 case a of SOME a' => (subst_atomic E (t $ a'))
136 | NONE => ((subst_atomic E t) $ v)),
138 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Inst"(*1*), _) $ _ $ _ $ _)) =
139 (Program.Tac (subst_atomic E t), NONE)
140 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Inst"(*2*), _) $ _ $ _)) =
142 case a of SOME a' => subst_atomic E (t $ a')
143 | NONE => ((subst_atomic E t) $ v)),
145 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set"(*1*), _) $ _ $ _)) =
146 (Program.Tac (subst_atomic E t), NONE)
147 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Set"(*2*), _) $ _)) =
149 case a of SOME a' => subst_atomic E (t $ a')
150 | NONE => ((subst_atomic E t) $ v)),
152 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*1*), _) $ _ $ _ $ _)) =
153 (Program.Tac (subst_atomic E t), NONE)
154 | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*2*), _) $ _ $ _)) =
156 case a of SOME a' => subst_atomic E (t $ a')
157 | NONE => ((subst_atomic E t) $ v)),
159 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Calculate"(*1*), _) $ _ $ _)) =
160 (Program.Tac (subst_atomic E t), NONE)
161 | eval_leaf E a v (t as (Const ("Prog_Tac.Calculate"(*2*), _) $ _)) =
163 case a of SOME a' => subst_atomic E (t $ a')
164 | NONE => ((subst_atomic E t) $ v)),
166 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Check'_elementwise"(*1*),_) $ _ $ _)) =
167 (Program.Tac (subst_atomic E t), NONE)
168 | eval_leaf E a v (t as (Const ("Prog_Tac.Check'_elementwise"(*2*), _) $ _)) =
170 case a of SOME a' => subst_atomic E (t $ a')
171 | NONE => ((subst_atomic E t) $ v)),
173 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Or'_to'_List"(*1*), _) $ _)) =
174 (Program.Tac (subst_atomic E t), NONE)
175 | eval_leaf E a v (t as (Const ("Prog_Tac.Or'_to'_List"(*2*), _))) = (*t $ v*)
177 case a of SOME a' => subst_atomic E (t $ a')
178 | NONE => ((subst_atomic E t) $ v)),
180 | eval_leaf E _ _ (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
181 (Program.Tac (subst_atomic E t), NONE)
182 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Take", _) $ _)) =
183 (Program.Tac (subst_atomic E t), NONE)
184 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) =
185 (Program.Tac (subst_atomic E t), NONE)
186 | eval_leaf E a v (t as (Const ("Prog_Tac.Substitute"(*2*), _) $ _)) =
188 case a of SOME a' => subst_atomic E (t $ a')
189 | NONE => ((subst_atomic E t) $ v)),
191 (*now all tactics are matched out and this leaf must be without a tactic*)
192 | eval_leaf E a v t =
193 (Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t), a);
196 (* check if a term is a Prog_Tac *)
198 val SOME Calculate = TermC.parseNEW @{context} "Calculate";
199 val SOME Rewrite = TermC.parseNEW @{context} "Rewrite";
200 val SOME Rewrite_Inst = TermC.parseNEW @{context} "Rewrite'_Inst";
201 val SOME Rewrite_Set = TermC.parseNEW @{context} "Rewrite'_Set";
202 val SOME Rewrite_Set_Inst = TermC.parseNEW @{context} "Rewrite'_Set'_Inst";
203 val SOME Or_to_List = TermC.parseNEW @{context} "Or'_to'_List";
204 val SOME SubProblem = TermC.parseNEW @{context} "SubProblem";
205 val SOME Substitute = TermC.parseNEW @{context} "Substitute";
206 val SOME Take = TermC.parseNEW @{context} "Take";
207 val SOME Check_elementwise = TermC.parseNEW @{context} "Check'_elementwise";
208 val SOME Assumptions = TermC.parseNEW @{context} "Assumptions";
210 val all_Consts = [Calculate, Rewrite, Rewrite_Inst, Rewrite_Set, Rewrite_Set_Inst, Or_to_List,
211 SubProblem, Substitute, Take, Check_elementwise, Assumptions]
213 fun is t = TermC.contains_Const_typeless all_Consts t
217 subsection \<open>TODO\<close>