wneuper@59571
|
1 |
(* Title: Tactics; tac_ for interaction with frontend, input for internal use.
|
wneuper@59304
|
2 |
Author: Walther Neuper 170121
|
wneuper@59304
|
3 |
(c) due to copyright terms
|
wneuper@59304
|
4 |
|
wneuper@59304
|
5 |
regular expression for search:
|
wneuper@59304
|
6 |
|
wneuper@59304
|
7 |
Add_Find|Add_Given|Add_Relation|Apply_Assumption|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|Collect_Trues|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|CAScmd|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Asm|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
|
wneuper@59304
|
8 |
|
wneuper@59304
|
9 |
*)
|
wneuper@59298
|
10 |
signature TACTIC =
|
wneuper@59298
|
11 |
sig
|
walther@59740
|
12 |
datatype T = datatype Tactic_Def.T
|
walther@59728
|
13 |
val string_of : T -> string
|
wneuper@59302
|
14 |
|
walther@59740
|
15 |
datatype input = datatype Tactic_Def.input
|
wneuper@59571
|
16 |
val tac2str : input -> string
|
wneuper@59302
|
17 |
|
walther@59728
|
18 |
val eq_tac : input * input -> bool
|
walther@59728
|
19 |
val is_empty_tac : input -> bool
|
walther@59728
|
20 |
val is_rewtac : input -> bool
|
walther@59728
|
21 |
val is_rewset : input -> bool
|
walther@59728
|
22 |
val rls_of : input -> Rule.rls'
|
wneuper@59571
|
23 |
val tac2IDstr : input -> string
|
walther@59728
|
24 |
val rule2tac : theory -> (term * term) list -> Rule.rule -> input
|
walther@59704
|
25 |
val input_from_T : T -> input
|
walther@59728
|
26 |
val result : T -> term
|
walther@59728
|
27 |
val creates_assms: T -> term list
|
walther@59728
|
28 |
val insert_assumptions: T -> Proof.context -> Proof.context
|
walther@59735
|
29 |
|
wneuper@59310
|
30 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
wneuper@59310
|
31 |
(* NONE *)
|
walther@59702
|
32 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59310
|
33 |
(* NONE *)
|
walther@59702
|
34 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59298
|
35 |
|
wneuper@59310
|
36 |
(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
|
wneuper@59310
|
37 |
(* NONE *)
|
wneuper@59298
|
38 |
end
|
wneuper@59298
|
39 |
|
walther@59728
|
40 |
(**)
|
wneuper@59571
|
41 |
structure Tactic(**): TACTIC(**) =
|
wneuper@59298
|
42 |
struct
|
walther@59728
|
43 |
(**)
|
wneuper@59298
|
44 |
|
wneuper@59302
|
45 |
(* tactics for user at front-end.
|
wneuper@59571
|
46 |
input propagates the construction of the calc-tree;
|
wneuper@59302
|
47 |
there are
|
wneuper@59302
|
48 |
(a) 'specsteps' for the specify-phase, and others for the solve-phase
|
wneuper@59302
|
49 |
(b) those of the solve-phase are 'initac's and others;
|
wneuper@59302
|
50 |
initacs start with a formula different from the preceding formula.
|
wneuper@59302
|
51 |
see 'type tac_' for the internal representation of tactics
|
wneuper@59302
|
52 |
*)
|
walther@59740
|
53 |
datatype input = datatype Tactic_Def.input
|
wneuper@59302
|
54 |
|
walther@59740
|
55 |
val tac2str = Tactic_Def.tac2str
|
wneuper@59302
|
56 |
|
walther@59740
|
57 |
val is_empty_tac = Tactic_Def.is_empty_tac
|
wneuper@59302
|
58 |
|
wneuper@59302
|
59 |
fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
|
wneuper@59302
|
60 |
| eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
|
wneuper@59302
|
61 |
| eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
|
wneuper@59302
|
62 |
| eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
|
wneuper@59302
|
63 |
| eq_tac (Calculate id1, Calculate id2) = id1 = id2
|
wneuper@59302
|
64 |
| eq_tac _ = false
|
wneuper@59302
|
65 |
|
wneuper@59302
|
66 |
fun is_rewset (Rewrite_Set_Inst _) = true
|
wneuper@59302
|
67 |
| is_rewset (Rewrite_Set _) = true
|
wneuper@59302
|
68 |
| is_rewset _ = false;
|
wneuper@59302
|
69 |
fun is_rewtac (Rewrite _) = true
|
wneuper@59302
|
70 |
| is_rewtac (Rewrite_Inst _) = true
|
wneuper@59302
|
71 |
| is_rewtac (Rewrite_Asm _) = true
|
wneuper@59571
|
72 |
| is_rewtac input = is_rewset input;
|
wneuper@59302
|
73 |
|
wneuper@59302
|
74 |
fun tac2IDstr ma = case ma of
|
wneuper@59302
|
75 |
Model_Problem => "Model_Problem"
|
wneuper@59302
|
76 |
| Refine_Tacitly _ => "Refine_Tacitly"
|
wneuper@59302
|
77 |
| Refine_Problem _ => "Refine_Problem"
|
wneuper@59302
|
78 |
| Add_Given _ => "Add_Given"
|
wneuper@59302
|
79 |
| Del_Given _ => "Del_Given"
|
wneuper@59302
|
80 |
| Add_Find _ => "Add_Find"
|
wneuper@59302
|
81 |
| Del_Find _ => "Del_Find"
|
wneuper@59302
|
82 |
| Add_Relation _ => "Add_Relation"
|
wneuper@59302
|
83 |
| Del_Relation _ => "Del_Relation"
|
wneuper@59302
|
84 |
|
wneuper@59302
|
85 |
| Specify_Theory _ => "Specify_Theory"
|
wneuper@59302
|
86 |
| Specify_Problem _ => "Specify_Problem"
|
wneuper@59302
|
87 |
| Specify_Method _ => "Specify_Method"
|
wneuper@59302
|
88 |
| Apply_Method _ => "Apply_Method"
|
wneuper@59302
|
89 |
| Check_Postcond _ => "Check_Postcond"
|
wneuper@59302
|
90 |
| Free_Solve => "Free_Solve"
|
wneuper@59302
|
91 |
|
wneuper@59302
|
92 |
| Rewrite_Inst _ => "Rewrite_Inst"
|
wneuper@59302
|
93 |
| Rewrite _ => "Rewrite"
|
wneuper@59302
|
94 |
| Rewrite_Asm _ => "Rewrite_Asm"
|
wneuper@59302
|
95 |
| Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
|
wneuper@59302
|
96 |
| Rewrite_Set _ => "Rewrite_Set"
|
wneuper@59302
|
97 |
| Detail_Set _ => "Detail_Set"
|
wneuper@59302
|
98 |
| Detail_Set_Inst _ => "Detail_Set_Inst"
|
wneuper@59302
|
99 |
| Derive _ => "Derive "
|
wneuper@59302
|
100 |
| Calculate _ => "Calculate "
|
wneuper@59302
|
101 |
| Substitute _ => "Substitute"
|
wneuper@59302
|
102 |
| Apply_Assumption _ => "Apply_Assumption"
|
wneuper@59302
|
103 |
|
wneuper@59302
|
104 |
| Take _ => "Take"
|
wneuper@59302
|
105 |
| Take_Inst _ => "Take_Inst"
|
wneuper@59302
|
106 |
| Subproblem _ => "Subproblem"
|
wneuper@59302
|
107 |
| End_Subproblem => "End_Subproblem"
|
wneuper@59302
|
108 |
| CAScmd _ => "CAScmd"
|
wneuper@59302
|
109 |
|
wneuper@59302
|
110 |
| Check_elementwise _ => "Check_elementwise"
|
wneuper@59302
|
111 |
| Or_to_List => "Or_to_List "
|
wneuper@59302
|
112 |
| Collect_Trues => "Collect_Trues"
|
wneuper@59302
|
113 |
|
wneuper@59302
|
114 |
| Empty_Tac => "Empty_Tac"
|
wneuper@59302
|
115 |
| Tac _ => "Tac "
|
wneuper@59302
|
116 |
| End_Proof' => "End_Proof'"
|
wneuper@59302
|
117 |
| _ => "tac2str not impl. for ?!";
|
wneuper@59302
|
118 |
|
wneuper@59302
|
119 |
fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
|
wneuper@59302
|
120 |
| rls_of (Rewrite_Set rls) = rls
|
wneuper@59571
|
121 |
| rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
|
wneuper@59302
|
122 |
|
wneuper@59416
|
123 |
fun rule2tac thy _ (Rule.Calc (opID, _)) = Calculate (assoc_calc thy opID)
|
wneuper@59416
|
124 |
| rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
|
wneuper@59416
|
125 |
| rule2tac _ subst (Rule.Thm thm'') =
|
wneuper@59302
|
126 |
Rewrite_Inst (Selem.subst2subs subst, thm'')
|
wneuper@59416
|
127 |
| rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule.id_rls rls)
|
wneuper@59416
|
128 |
| rule2tac _ subst (Rule.Rls_ rls) =
|
wneuper@59416
|
129 |
Rewrite_Set_Inst (Selem.subst2subs subst, (Rule.id_rls rls))
|
wneuper@59302
|
130 |
| rule2tac _ _ rule =
|
wneuper@59416
|
131 |
error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
|
wneuper@59302
|
132 |
|
wneuper@59571
|
133 |
(* tactics for for internal use, compare "input" for user at the front-end.
|
wneuper@59302
|
134 |
tac_ contains results from check in 'fun applicable_in'.
|
wneuper@59302
|
135 |
This is useful for costly results, e.g. from rewriting;
|
wneuper@59302
|
136 |
however, these results might be changed by Scripts like
|
wneuper@59499
|
137 |
" eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
|
wneuper@59302
|
138 |
" eq = (Rewrite_Set equival_trans False) eq;" ^
|
wneuper@59302
|
139 |
TODO.WN120106 ANALOGOUSLY TO Substitute':
|
wneuper@59302
|
140 |
So tac_ contains the term t the result was calculated from
|
wneuper@59302
|
141 |
in order to compare t with t' possibly changed by "Expr "
|
wneuper@59302
|
142 |
and re-calculate result if t<>t'
|
wneuper@59302
|
143 |
TODO.WN161219: replace *every* cterm' by term
|
wneuper@59302
|
144 |
*)
|
walther@59740
|
145 |
datatype T = datatype Tactic_Def.T
|
wneuper@59302
|
146 |
|
walther@59740
|
147 |
val string_of = Tactic_Def.string_of
|
wneuper@59302
|
148 |
|
walther@59704
|
149 |
fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
|
walther@59704
|
150 |
| input_from_T (Model_Problem' (_, _, _)) = Model_Problem
|
walther@59704
|
151 |
| input_from_T (Add_Given' (t, _)) = Add_Given t
|
walther@59704
|
152 |
| input_from_T (Add_Find' (t, _)) = Add_Find t
|
walther@59704
|
153 |
| input_from_T (Add_Relation' (t, _)) = Add_Relation t
|
walther@59704
|
154 |
|
walther@59704
|
155 |
| input_from_T (Specify_Theory' dI) = Specify_Theory dI
|
walther@59704
|
156 |
| input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI
|
walther@59704
|
157 |
| input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
|
walther@59704
|
158 |
|
walther@59704
|
159 |
| input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
|
walther@59704
|
160 |
| input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
|
walther@59704
|
161 |
|
walther@59704
|
162 |
| input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule.id_rls rls)
|
walther@59704
|
163 |
| input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule.id_rls rls)
|
walther@59704
|
164 |
|
walther@59704
|
165 |
| input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
|
walther@59704
|
166 |
Rewrite_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
|
walther@59704
|
167 |
| input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
|
walther@59704
|
168 |
Detail_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
|
walther@59704
|
169 |
|
walther@59704
|
170 |
| input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
|
walther@59704
|
171 |
| input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
|
walther@59704
|
172 |
|
walther@59704
|
173 |
| input_from_T (Or_to_List' _) = Or_to_List
|
walther@59704
|
174 |
| input_from_T (Take' term) = Take (Rule.term2str term)
|
walther@59704
|
175 |
| input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Selem.subte2sube subte)
|
walther@59704
|
176 |
| input_from_T (Tac_ (_, _, id, _)) = Tac id
|
walther@59704
|
177 |
|
walther@59704
|
178 |
| input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
|
walther@59704
|
179 |
| input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
|
walther@59704
|
180 |
| input_from_T Empty_Tac_ = Empty_Tac
|
walther@59728
|
181 |
| input_from_T m = error (": not impl. for "^(string_of m));
|
walther@59704
|
182 |
|
walther@59728
|
183 |
fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
|
walther@59728
|
184 |
| res (Rewrite' (_, _, _, _, _, _, res)) = res
|
walther@59728
|
185 |
| res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
|
walther@59728
|
186 |
| res (Rewrite_Set' (_, _, _, _, res)) = res
|
walther@59728
|
187 |
| res (Calculate' (_, _, _, (t, _))) = (t, [])
|
walther@59728
|
188 |
| res (Check_elementwise' (_, _, res)) = res
|
walther@59728
|
189 |
| res (Subproblem' (_, _, _, _, _, t)) = (t, [])
|
walther@59728
|
190 |
| res (Take' t) = (t, [])
|
walther@59728
|
191 |
| res (Substitute' (_, _, _, _, t)) = (t, [])
|
walther@59728
|
192 |
| res (Or_to_List' (_, t)) = (t, [])
|
walther@59728
|
193 |
| res m = raise ERROR ("result: not impl.for " ^ string_of m)
|
walther@59728
|
194 |
|
walther@59728
|
195 |
(*fun result m = (fst o res) m; TODO*)
|
walther@59728
|
196 |
fun result tac = (fst o res) tac;
|
walther@59728
|
197 |
fun creates_assms tac = (snd o res) tac;
|
walther@59728
|
198 |
|
walther@59728
|
199 |
fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
|
walther@59728
|
200 |
|
walther@59728
|
201 |
(**)end(**)
|