1 (* Title: tactics, tacticals etc. for scripts
2 Author: Walther Neuper 000224
3 (c) due to copyright terms
7 imports "~~/src/Tools/isac/CalcElements/CalcElements"
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 * real) 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) * real) 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 Calculate1 :: "[char list, 'a] => 'a" (* unknown to lucas-interpreter *)
52 Check'_elementwise :: (* TODO: is idle, retained for test purposes in Minisubpbl *)
53 "['a list, 'b set] => 'a list" ("Check'_elementwise (_ _)" 11)
54 Assumptions :: bool (* TODO: remove with making ^^^ idle *)
57 subsection \<open>TODO\<close>
59 signature PROGAM_TACTIC =
61 val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * Celem.stacexpr
62 val get_stac : 'a -> term -> term option (*rename get_first*)
63 val dest_spec : term -> Celem.spec
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) : Celem.spec
80 | dest_spec t = raise TERM ("dest_spec: called with ", [t])
82 (* get argument of first Prog_Tac in a progam for init_form *)
83 fun get_stac thy (_ $ body) =
85 (* entries occur twice, for form curried by @@ or non-curried *)
86 fun get_t y (Const ("Tactical.Seq",_) $ e1 $ e2) a =
87 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
88 | get_t y (Const ("Tactical.Seq",_) $ e1 $ e2 $ a) _ =
89 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
90 | get_t y (Const ("Tactical.Try",_) $ e) a = get_t y e a
91 | get_t y (Const ("Tactical.Try",_) $ e $ a) _ = get_t y e a
92 | get_t y (Const ("Tactical.Repeat",_) $ e) a = get_t y e a
93 | get_t y (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t y e a
94 | get_t y (Const ("Tactical.Or",_) $e1 $ e2) a =
95 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
96 | get_t y (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ =
97 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
98 | get_t y (Const ("Tactical.While",_) $ _ $ e) a = get_t y e a
99 | get_t y (Const ("Tactical.While",_) $ _ $ e $ a) _ = get_t y e a
100 | get_t y (Const ("Tactical.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
101 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
102 | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a =
103 get_t y 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 thy body Rule.e_term end
123 | get_stac _ t = error ("get_stac: no fun-def. for " ^ Rule.term2str 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 an Celem.Expr by fall-through.
130 WN060906 quick and dirty fix: due to (2) a is returned, too *)
131 fun subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite",_) $ _ $ _)) =
132 (NONE, Celem.STac (subst_atomic E t))
133 | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite",_) $ _)) =
134 (a, (*in these cases we hope, that a = SOME _*)
135 Celem.STac (case a of SOME a' => (subst_atomic E (t $ a'))
136 | NONE => ((subst_atomic E t) $ v)))
137 | subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _ $ _)) =
138 (NONE, Celem.STac (subst_atomic E t))
139 | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _)) =
140 (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
141 | NONE => ((subst_atomic E t) $ v)))
142 | subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite'_Set", _) $ _ $ _)) =
143 (NONE, Celem.STac (subst_atomic E t))
144 | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite'_Set", _) $ _)) =
145 (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
146 | NONE => ((subst_atomic E t) $ v)))
147 | subst_stacexpr E _ _
148 (t as (*1*)(Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _ $ _)) =
149 (NONE, Celem.STac (subst_atomic E t))
150 | subst_stacexpr E a v
151 (t as (*2*)(Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _)) =
152 (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
153 | NONE => ((subst_atomic E t) $ v)))
154 | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Calculate", _) $ _ $ _)) =
155 (NONE, Celem.STac (subst_atomic E t))
156 | subst_stacexpr E a v (t as (Const ("Prog_Tac.Calculate", _) $ _)) =
157 (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
158 | NONE => ((subst_atomic E t) $ v)))
159 | subst_stacexpr E _ _
160 (t as (Const ("Prog_Tac.Check'_elementwise",_) $ _ $ _)) =
161 (NONE, Celem.STac (subst_atomic E t))
162 | subst_stacexpr E a v (t as (Const ("Prog_Tac.Check'_elementwise", _) $ _)) =
163 (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
164 | NONE => ((subst_atomic E t) $ v)))
165 | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =
166 (NONE, Celem.STac (subst_atomic E t))
167 | subst_stacexpr E a v (t as (Const ("Prog_Tac.Or'_to'_List", _))) = (*t $ v*)
168 (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
169 | NONE => ((subst_atomic E t) $ v)))
170 | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
171 (NONE, Celem.STac (subst_atomic E t))
172 | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Take",_) $ _)) =
173 (NONE, Celem.STac (subst_atomic E t))
174 | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Substitute", _) $ _ $ _)) =
175 (NONE, Celem.STac (subst_atomic E t))
176 | subst_stacexpr E a v (t as (Const ("Prog_Tac.Substitute", _) $ _)) =
177 (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
178 | NONE => ((subst_atomic E t) $ v)))
179 (*now all tactics are matched out and this leaf must be without a tactic*)
180 | subst_stacexpr E a v t =
181 (a, Celem.Expr (subst_atomic (case a of SOME a => Celem.upd_env E (a,v)
187 subsection \<open>TODO\<close>