|
1 (* Title: tactics, tacticals etc. for scripts |
|
2 Author: Walther Neuper 000224 |
|
3 (c) due to copyright terms |
|
4 |
|
5 use_thy_only"ProgLang/Script"; |
|
6 use_thy"../ProgLang/Script"; |
|
7 use_thy"Script"; |
|
8 *) |
|
9 |
|
10 theory Script imports Tools begin |
|
11 |
|
12 typedecl |
|
13 ID (* identifiers for thy, ruleset,... *) |
|
14 |
|
15 typedecl |
|
16 arg (* argument of subproblem *) |
|
17 |
|
18 consts |
|
19 |
|
20 (*types of subproblems' arguments*) |
|
21 real_' :: "real => arg" |
|
22 real_list_' :: "(real list) => arg" |
|
23 real_set_' :: "(real set) => arg" |
|
24 bool_' :: "bool => arg" |
|
25 bool_list_' :: "(bool list) => arg" |
|
26 real_real_' :: "(real => real) => arg" |
|
27 |
|
28 (*tactics*) |
|
29 Rewrite :: "[ID, bool, 'a] => 'a" |
|
30 Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a" |
|
31 ("(Rewrite'_Inst (_ _ _))" 11) |
|
32 (*without last argument ^^ for @@*) |
|
33 Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11) |
|
34 Rewrite'_Set'_Inst |
|
35 :: "[(real * real) list, ID, bool, 'a] => 'a" |
|
36 ("(Rewrite'_Set'_Inst (_ _ _))" 11) |
|
37 (*without last argument ^^ for @@*) |
|
38 Calculate :: "[ID, 'a] => 'a" (*WN100816 PLUS, TIMES, POWER miss.in scr*) |
|
39 Calculate1 :: "[ID, 'a] => 'a" (*FIXXXME: unknown to script-interpreter*) |
|
40 |
|
41 (* WN0509 substitution now is rewriting by a list of terms (of type bool) |
|
42 Substitute :: "[(real * real) list, 'a] => 'a"*) |
|
43 Substitute :: "[bool list, 'a] => 'a" |
|
44 |
|
45 Map :: "['a => 'b, 'a list] => 'b list" |
|
46 Tac :: "ID => 'a" (*deprecated; only use in Test.ML*) |
|
47 Check'_elementwise :: |
|
48 "['a list, 'b set] => 'a list" |
|
49 ("Check'_elementwise (_ _)" 11) |
|
50 Take :: "'a => 'a" (*for non-var args as long as no 'o'*) |
|
51 SubProblem :: "[ID * ID list * ID list, arg list] => 'a" |
|
52 |
|
53 Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11) |
|
54 (*=========== record these ^^^ in 'tacs' in Script.ML =========*) |
|
55 |
|
56 Assumptions :: bool |
|
57 Problem :: "[ID * ID list] => 'a" |
|
58 |
|
59 (*special formulas for frontend 'CAS format'*) |
|
60 Subproblem :: "(ID * ID list) => 'a" |
|
61 |
|
62 (*script-expressions (tacticals)*) |
|
63 Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*) |
|
64 Try :: "['a => 'a, 'a] => 'a" |
|
65 Repeat :: "['a => 'a, 'a] => 'a" |
|
66 Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10) |
|
67 While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9) |
|
68 (*WN100723 because of "Error in syntax translation" below... |
|
69 (*'b => bool doesn't work with "contains_root _"*) |
|
70 Letpar :: "['a, 'a => 'b] => 'b" |
|
71 (*--- defined in Isabelle/scr/HOL/HOL.thy: |
|
72 Let :: "['a, 'a => 'b] => 'b" |
|
73 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
|
74 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
|
75 %x. P x .. lambda is defined in Isabelles meta logic |
|
76 --- *) |
|
77 *) |
|
78 failtac :: 'a |
|
79 idletac :: 'a |
|
80 (*... + RECORD IN 'screxpr' in Script.ML *) |
|
81 |
|
82 (*for scripts generated automatically from rls*) |
|
83 Stepwise :: "['z, 'z] => 'z" ("((Script Stepwise (_ =))// (_))" 9) |
|
84 Stepwise'_inst:: "['z,real,'z] => 'z" |
|
85 ("((Script Stepwise'_inst (_ _ =))// (_))" 9) |
|
86 |
|
87 |
|
88 (*SHIFT -> resp.thys ----vvv---------------------------------------------*) |
|
89 (*script-names: initial capital letter, |
|
90 type of last arg (=script-body) == result-type ! |
|
91 Xxxx :: script ids, duplicate result-type 'r in last argument: |
|
92 "['a, ... , \ |
|
93 \ 'r] => 'r |
|
94 *) |
|
95 |
|
96 (*make'_solution'_set :: "bool => bool list" |
|
97 ("(make'_solution'_set (_))" 11) |
|
98 |
|
99 max'_on'_interval |
|
100 :: "[ID * (ID list) * ID, bool,real,real set] => real" |
|
101 ("(max'_on'_interval (_)/ (_ _ _))" 9) |
|
102 find'_vals |
|
103 :: "[ID * (ID list) * ID, |
|
104 real,real,real,real,bool list] => bool list" |
|
105 ("(find'_vals (_)/ (_ _ _ _ _))" 9) |
|
106 |
|
107 make'_fun :: "[ID * (ID list) * ID, real,real,bool list] => bool" |
|
108 ("(make'_fun (_)/ (_ _ _))" 9) |
|
109 |
|
110 solve'_univar |
|
111 :: "[ID * (ID list) * ID, bool,real] => bool list" |
|
112 ("(solve'_univar (_)/ (_ _ ))" 9) |
|
113 solve'_univar'_err |
|
114 :: "[ID * (ID list) * ID, bool,real,bool] => bool list" |
|
115 ("(solve'_univar (_)/ (_ _ _))" 9) |
|
116 ----------*) |
|
117 |
|
118 Testeq :: "[bool, bool] => bool" |
|
119 ("((Script Testeq (_ =))// |
|
120 (_))" 9) |
|
121 |
|
122 Testeq2 :: "[bool, bool list] => bool list" |
|
123 ("((Script Testeq2 (_ =))// |
|
124 (_))" 9) |
|
125 |
|
126 Testterm :: "[real, real] => real" |
|
127 ("((Script Testterm (_ =))// |
|
128 (_))" 9) |
|
129 |
|
130 Testchk :: "[bool, real, real list] => real list" |
|
131 ("((Script Testchk (_ _ =))// |
|
132 (_))" 9) |
|
133 (*... + RECORD IN 'subpbls' in Script.ML *) |
|
134 (*SHIFT -> resp.thys ----^^^----------------------------*) |
|
135 |
|
136 (*Makarius 10.03 |
|
137 syntax |
|
138 |
|
139 "_Letpar" :: "[letbinds, 'a] => 'a" ("(letpar (_)/ in (_))" 10) |
|
140 |
|
141 translations |
|
142 |
|
143 "_Letpar (_binds b bs) e" == "_Letpar b (_Letpar bs e)" |
|
144 "letpar x = a in e" == "Letpar a (%x. e)" |
|
145 *** Error in syntax translation rule: rhs contains extra variables |
|
146 *** ("_Letpar" ("_bind" x a) e) -> (Letpar a ("_abs" x e)) |
|
147 *** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script.thy"). |
|
148 *) |
|
149 |
|
150 ML {* (*the former Script.ML*) |
|
151 |
|
152 (*.record all theories defined for Scripts; in order to distinguish them |
|
153 from general IsacKnowledge defined later on.*) |
|
154 script_thys := !theory'; |
|
155 |
|
156 (*--vvv----- SHIFT? or delete ?*) |
|
157 val IDTyp = Type("Script.ID",[]); |
|
158 |
|
159 |
|
160 val tacs = ref (distinct (remove op = "" |
|
161 ["Calculate", |
|
162 "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst", |
|
163 "Substitute","Tac","Check'_elementswise", |
|
164 "Take","Subproblem","Or'_to'_List"])); |
|
165 |
|
166 val screxpr = ref (distinct (remove op = "" |
|
167 ["Let","If","Repeat","While","Try","Or"])); |
|
168 |
|
169 val listfuns = ref [(*_all_ functions in Isa99.List.thy *) |
|
170 "@","filter","concat","foldl","hd","last","set","list_all", |
|
171 "map","mem","nth","list_update","take","drop", |
|
172 "takeWhile","dropWhile","tl","butlast", |
|
173 "rev","zip","upt","remdups","nodups","replicate", |
|
174 |
|
175 "Cons","Nil"]; |
|
176 |
|
177 val scrfuns = ref (distinct (remove op = "" |
|
178 ["Testvar"])); |
|
179 |
|
180 val listexpr = ref (union op = (!listfuns) (!scrfuns)); |
|
181 |
|
182 val notsimp = ref |
|
183 (distinct (remove op = "" |
|
184 (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns))); |
|
185 |
|
186 val negotiable = ref ((!tacs (*@ !subpbls*))); |
|
187 |
|
188 val tacpbl = ref |
|
189 (distinct (remove op = "" (!tacs (*@ !subpbls*)))); |
|
190 (*--^^^----- SHIFT? or delete ?*) |
|
191 |
|
192 *} |
|
193 |
|
194 end |