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