author | paulson |
Wed, 27 Nov 1996 10:40:45 +0100 | |
changeset 2238 | c72a23bbe762 |
parent 1810 | 0eef167ebe1b |
child 3534 | c245c88194ff |
permissions | -rw-r--r-- |
1274 | 1 |
(* TTITLEF/thy_ops.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Mayr |
|
4 |
||
5 |
Additional theory file section for HOLCF: ops |
|
6 |
There's an elaborate but german description of this program, |
|
7 |
write to mayrt@informatik.tu-muenchen.de. |
|
8 |
For a short english description of the new sections |
|
9 |
write to regensbu@informatik.tu-muenchen.de. |
|
10 |
||
1512 | 11 |
TODO: maybe AST-representation with "op name" instead of _I_... |
1274 | 12 |
|
13 |
*) |
|
14 |
||
15 |
signature THY_OPS = |
|
16 |
sig |
|
1512 | 17 |
(* continuous mixfixes (extension of datatype Mixfix.mixfix) *) |
1274 | 18 |
datatype cmixfix = |
1512 | 19 |
Mixfix of Mixfix.mixfix | |
1274 | 20 |
CInfixl of int | |
21 |
CInfixr of int | |
|
22 |
CMixfix of string * int list *int; |
|
23 |
||
24 |
exception CINFIX of cmixfix; |
|
1512 | 25 |
val cmixfix_to_mixfix : cmixfix -> Mixfix.mixfix; |
1274 | 26 |
|
27 |
(* theory extenders : *) |
|
28 |
val add_ops : {curried: bool, total: bool, strict: bool} -> |
|
29 |
(string * string * cmixfix) list -> theory -> theory; |
|
30 |
val add_ops_i : {curried: bool, total: bool, strict: bool} -> |
|
31 |
(string * typ * cmixfix) list -> theory -> theory; |
|
32 |
val ops_keywords : string list; |
|
33 |
val ops_sections : (string * (ThyParse.token list -> |
|
34 |
(string * string) * ThyParse.token list)) list; |
|
35 |
val opt_cmixfix: ThyParse.token list -> (string * ThyParse.token list); |
|
36 |
val const_name : string -> cmixfix -> string; |
|
37 |
end; |
|
38 |
||
39 |
structure ThyOps : THY_OPS = |
|
40 |
struct |
|
41 |
||
42 |
open HOLCFlogic; |
|
43 |
||
44 |
(** library ******************************************************) |
|
45 |
||
46 |
(* abbreviations *) |
|
47 |
val internal = fst; (* cinfix-ops will have diffrent internal/external names *) |
|
48 |
val external = snd; |
|
49 |
||
50 |
fun apsnd_of_three f = fn (a,b,c) => (a,f b,c); |
|
51 |
||
52 |
||
53 |
(******** ops ********************) |
|
54 |
||
55 |
(* the extended copy of mixfix *) |
|
56 |
datatype cmixfix = |
|
1512 | 57 |
Mixfix of Mixfix.mixfix | |
1274 | 58 |
CInfixl of int | |
59 |
CInfixr of int | |
|
60 |
CMixfix of string * int list *int; |
|
61 |
||
62 |
exception CINFIX of cmixfix; |
|
63 |
||
64 |
fun cmixfix_to_mixfix (Mixfix x) = x |
|
65 |
| cmixfix_to_mixfix x = raise CINFIX x; |
|
66 |
||
67 |
||
68 |
(** theory extender : add_ops *) |
|
69 |
||
70 |
(* generating the declarations of the new constants. ************* |
|
71 |
cinfix names x are internally non infix (renamed by mk_internal_name) |
|
72 |
and externally non continous infix function names (changed by op_to_fun). |
|
73 |
Thus the cinfix declaration is splitted in an 'oldstyle' decl, |
|
74 |
which is NoSyn (non infix) and is added by add_consts_i, |
|
75 |
and an syn(tactic) decl, which is an infix function (not operation) |
|
76 |
added by add_syntax_i, so that it can appear in input strings, but |
|
77 |
not in terms. |
|
78 |
The interface between internal and external names is realized by |
|
79 |
transrules A x B <=> _x ' A ' B (generated by xrules_of) |
|
80 |
The boolean argument 'curried' distinguishes between curried and |
|
81 |
tupeled syntax of operation application *) |
|
82 |
||
83 |
local |
|
84 |
fun strip ("'" :: c :: cs) = c :: strip cs |
|
85 |
| strip ["'"] = [] |
|
86 |
| strip (c :: cs) = c :: strip cs |
|
87 |
| strip [] = []; |
|
88 |
||
89 |
val strip_esc = implode o strip o explode; |
|
90 |
||
91 |
fun infix_name c = "op " ^ strip_esc c; |
|
92 |
in |
|
93 |
val mk_internal_name = infix_name; |
|
94 |
(* |
|
95 |
(* changing e.g. 'ab' to '_I_97_98'. |
|
96 |
Called by oldstyle, xrules_of, strictness_axms and totality_axms. *) |
|
97 |
fun mk_internal_name name = |
|
98 |
let fun alphanum (s::ss) = "_"^(string_of_int (ord s))^(alphanum ss) |
|
99 |
| alphanum [] = ""; |
|
100 |
in |
|
101 |
"_I"^(alphanum o explode) name |
|
102 |
end; |
|
103 |
*) |
|
104 |
(* extension of Pure/Syntax/mixfix.ML: SynExt.const_name *) |
|
105 |
fun const_name c (CInfixl _) = mk_internal_name c |
|
106 |
| const_name c (CInfixr _) = mk_internal_name c |
|
107 |
| const_name c (CMixfix _) = c |
|
108 |
| const_name c (Mixfix x) = Syntax.const_name c x; |
|
109 |
end; |
|
110 |
||
111 |
(* Changing a->b->c res. a*b->c to a=>b=>c. Called by syn_decls. *) |
|
112 |
(*####*) |
|
113 |
fun op_to_fun true sign (Type("->" ,[larg,t]))= |
|
1461 | 114 |
Type("fun",[larg,op_to_fun true sign t]) |
1274 | 115 |
| op_to_fun false sign (Type("->",[args,res])) = let |
1461 | 116 |
fun otf (Type("*",[larg,rargs])) = Type("fun",[larg,otf rargs]) |
117 |
| otf t = Type("fun",[t,res]); |
|
118 |
in otf args end |
|
1274 | 119 |
| op_to_fun _ sign t = t(*error("Wrong type for cinfix/cmixfix : "^ |
120 |
(Sign.string_of_typ sign t))*); |
|
121 |
(*####*) |
|
122 |
||
123 |
(* oldstyle is called by add_ext_axioms(_i) *) |
|
124 |
(* the first part is just copying the homomorphic part of the structures *) |
|
125 |
fun oldstyle ((name,typ,Mixfix(x))::tl) = |
|
126 |
(name,typ,x)::(oldstyle tl) |
|
127 |
| oldstyle ((name,typ,CInfixl(i))::tl) = |
|
1512 | 128 |
(mk_internal_name name,typ,Mixfix.NoSyn):: |
1274 | 129 |
(oldstyle tl) |
130 |
| oldstyle ((name,typ,CInfixr(i))::tl) = |
|
1512 | 131 |
(mk_internal_name name,typ,Mixfix.NoSyn):: |
1274 | 132 |
(oldstyle tl) |
133 |
| oldstyle ((name,typ,CMixfix(x))::tl) = |
|
1512 | 134 |
(name,typ,Mixfix.NoSyn):: |
1274 | 135 |
(oldstyle tl) |
136 |
| oldstyle [] = []; |
|
137 |
||
138 |
(* generating the external purely syntactical infix functions. |
|
139 |
Called by add_ext_axioms(_i) *) |
|
140 |
fun syn_decls curried sign ((name,typ,CInfixl(i))::tl) = |
|
1512 | 141 |
(name,op_to_fun curried sign typ,Mixfix.Infixl(i)):: |
1274 | 142 |
(syn_decls curried sign tl) |
143 |
| syn_decls curried sign ((name,typ,CInfixr(i))::tl) = |
|
1512 | 144 |
(name,op_to_fun curried sign typ,Mixfix.Infixr(i)):: |
1274 | 145 |
(syn_decls curried sign tl) |
146 |
| syn_decls curried sign ((name,typ,CMixfix(x))::tl) = |
|
147 |
(*#### |
|
1512 | 148 |
("@"^name,op_to_fun curried sign typ,Mixfix.Mixfix(x)):: |
1274 | 149 |
####**) |
1512 | 150 |
(name,op_to_fun curried sign typ,Mixfix.Mixfix(x)):: |
1274 | 151 |
|
152 |
(syn_decls curried sign tl) |
|
153 |
| syn_decls curried sign (_::tl) = syn_decls curried sign tl |
|
154 |
| syn_decls _ _ [] = []; |
|
155 |
||
1810
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
156 |
fun translate name vars rhs = |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
157 |
Syntax.<-> ((Ast.mk_appl (Constant (mk_internal_name name)) |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
158 |
(map Variable vars)), |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
159 |
rhs); |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
160 |
|
1274 | 161 |
(* generating the translation rules. Called by add_ext_axioms(_i) *) |
1512 | 162 |
local open Ast in |
1274 | 163 |
fun xrules_of true ((name,typ,CInfixl(i))::tail) = |
1810
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
164 |
translate name ["A","B"] |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
165 |
(mk_appl (Constant "@fapp") |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
166 |
[(mk_appl (Constant "@fapp") |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
167 |
[Constant (mk_internal_name name),Variable "A"]),Variable "B"]) |
1274 | 168 |
::xrules_of true tail |
169 |
| xrules_of true ((name,typ,CInfixr(i))::tail) = |
|
1810
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
170 |
translate name ["A","B"] |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
171 |
(mk_appl (Constant "@fapp") |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
172 |
[(mk_appl (Constant "@fapp") |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
173 |
[Constant (mk_internal_name name),Variable "A"]),Variable "B"]) |
1274 | 174 |
::xrules_of true tail |
175 |
(*####*) |
|
1810
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
176 |
| xrules_of true ((name,typ,CMixfix(_))::tail) = |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
177 |
let fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
178 |
| argnames _ _ = []; |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
179 |
val names = argnames (ord"A") typ; |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
180 |
in if names = [] then [] else |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
181 |
[Syntax.<-> (mk_appl (Constant name) (map Variable names), |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
182 |
foldl (fn (t,arg) => |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
183 |
(mk_appl (Constant "@fapp") [t,Variable arg])) |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
184 |
(Constant name,names))] |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
185 |
end |
1274 | 186 |
@xrules_of true tail |
187 |
(*####*) |
|
188 |
| xrules_of false ((name,typ,CInfixl(i))::tail) = |
|
1810
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
189 |
translate name ["A","B"] |
1274 | 190 |
(mk_appl (Constant "@fapp") [ Constant(mk_internal_name name), |
1810
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
191 |
(mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])]) |
1274 | 192 |
::xrules_of false tail |
193 |
| xrules_of false ((name,typ,CInfixr(i))::tail) = |
|
1810
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
194 |
translate name ["A","B"] |
1274 | 195 |
(mk_appl (Constant "@fapp") [ Constant(mk_internal_name name), |
1810
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
196 |
(mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])]) |
1274 | 197 |
::xrules_of false tail |
198 |
(*####*) |
|
1810
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
199 |
| xrules_of false ((name,typ,CMixfix(_))::tail) = |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
200 |
let fun foldr' f l = |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
201 |
let fun itr [] = raise LIST "foldr'" |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
202 |
| itr [a] = a |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
203 |
| itr (a::l) = f(a, itr l) |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
204 |
in itr l end; |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
205 |
fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
206 |
| argnames n _ = [chr n]; |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
207 |
val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
208 |
| _ => []); |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
209 |
in if vars = [] then [] else |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
210 |
[Syntax.<-> |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
211 |
(mk_appl (Constant name) vars, |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
212 |
mk_appl (Constant "@fapp") |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
213 |
[Constant name, |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
214 |
case vars of [v] => v |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
215 |
| args => mk_appl (Constant "@ctuple") |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
216 |
[hd args, |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
217 |
foldr' (fn (t,arg) => |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
218 |
mk_appl (Constant "_args") |
0eef167ebe1b
Translation infixes <->, etc., no longer available at top-level
paulson
parents:
1512
diff
changeset
|
219 |
[t,arg]) (tl args)]])] |
1461 | 220 |
end |
1274 | 221 |
@xrules_of false tail |
222 |
(*####*) |
|
223 |
| xrules_of c ((name,typ,Mixfix(_))::tail) = xrules_of c tail |
|
224 |
| xrules_of _ [] = []; |
|
225 |
end; |
|
226 |
(**** producing the new axioms ****************) |
|
227 |
||
228 |
datatype arguments = Curried_args of ((typ*typ) list) | |
|
229 |
Tupeled_args of (typ list); |
|
230 |
||
231 |
fun num_of_args (Curried_args l) = length l |
|
232 |
| num_of_args (Tupeled_args l) = length l; |
|
233 |
||
234 |
fun types_of (Curried_args l) = map fst l |
|
235 |
| types_of (Tupeled_args l) = l; |
|
236 |
||
237 |
fun mk_mkNotEqUU_vars (typ::tl) cnt = mkNotEqUU (Free("x"^(string_of_int cnt),typ)):: |
|
238 |
(mk_mkNotEqUU_vars tl (cnt+1)) |
|
239 |
| mk_mkNotEqUU_vars [] _ = []; |
|
240 |
||
241 |
local |
|
242 |
(* T1*...*Tn goes to [T1,...,Tn] *) |
|
243 |
fun args_of_tupel (Type("*",[left,right])) = left::(args_of_tupel right) |
|
244 |
| args_of_tupel T = [T]; |
|
245 |
||
246 |
(* A1->...->An->R goes to [(A1,B1),...,(An,Bn)] where Bi=Ai->...->An->R |
|
247 |
Bi is the Type of the function that is applied to an Ai type argument *) |
|
248 |
fun args_of_curried (typ as (Type("->",[S,T]))) = |
|
249 |
(S,typ) :: args_of_curried T |
|
250 |
| args_of_curried _ = []; |
|
251 |
in |
|
252 |
fun args_of_op true typ = Curried_args(rev(args_of_curried typ)) |
|
253 |
| args_of_op false (typ as (Type("->",[S,T]))) = |
|
254 |
Tupeled_args(args_of_tupel S) |
|
255 |
| args_of_op false _ = Tupeled_args([]); |
|
256 |
end; |
|
257 |
||
258 |
(* generates for the type t the type of the fapp constant |
|
259 |
that will be applied to t *) |
|
260 |
fun mk_fapp_typ (typ as Type("->",argl)) = Type("fun",[typ,Type("fun",argl)]) |
|
1284 | 261 |
| mk_fapp_typ t = ( |
1274 | 262 |
error("Internal error:mk_fapp_typ: wrong argument\n")); |
263 |
||
264 |
fun mk_arg_tupel_UU uu_pos [typ] n = |
|
265 |
if n<>uu_pos then Free("x"^(string_of_int n),typ) |
|
266 |
else Const("UU",typ) |
|
267 |
| mk_arg_tupel_UU uu_pos (typ::tail) n = |
|
268 |
mkCPair |
|
269 |
(if n<>uu_pos then Free("x"^(string_of_int n),typ) |
|
270 |
else Const("UU",typ)) |
|
271 |
(mk_arg_tupel_UU uu_pos tail (n+1)) |
|
272 |
| mk_arg_tupel_UU _ [] _ = error("Internal error:mk_arg_tupel: empty list"); |
|
273 |
||
274 |
fun mk_app_UU cnt uu_pos fname (Curried_args((typ,ftyp)::tl)) = |
|
275 |
Const("fapp",mk_fapp_typ ftyp) $ |
|
276 |
(mk_app_UU (cnt-1) uu_pos fname (Curried_args tl))$ |
|
277 |
(if cnt = uu_pos then Const("UU",typ) |
|
278 |
else Free("x"^(string_of_int cnt),typ)) |
|
279 |
| mk_app_UU _ _ (name,typ) (Curried_args []) = Const(name,typ) |
|
280 |
| mk_app_UU cnt uu_pos (name,typ) (Tupeled_args []) = Const(name,typ) |
|
281 |
| mk_app_UU cnt uu_pos (name,typ) (Tupeled_args list) = |
|
282 |
Const("fapp",mk_fapp_typ typ) $ Const(name,typ) $ |
|
283 |
mk_arg_tupel_UU uu_pos list 0; |
|
284 |
||
285 |
fun mk_app cnt fname args = mk_app_UU cnt (~1) fname args; |
|
286 |
||
287 |
(* producing the strictness axioms *) |
|
288 |
local |
|
289 |
fun s_axm_of curried name typ args num cnt = |
|
290 |
if cnt = num then |
|
291 |
error("Internal error: s_axm_of: arg is no operation "^(external name)) |
|
292 |
else |
|
293 |
let val app = mk_app_UU (num-1) cnt (internal name,typ) args |
|
294 |
val equation = HOLogic.mk_eq(app,Const("UU",fastype_of app)) |
|
295 |
in |
|
296 |
if cnt = num-1 then equation |
|
297 |
else And $ equation $ |
|
298 |
s_axm_of curried name typ args num (cnt+1) |
|
299 |
end; |
|
300 |
in |
|
301 |
fun strictness_axms curried ((rawname,typ,cmixfix)::tail) = |
|
302 |
let val name = case cmixfix of |
|
303 |
(CInfixl _) => (mk_internal_name rawname,rawname) |
|
304 |
| (CInfixr _) => (mk_internal_name rawname,rawname) |
|
305 |
| _ => (rawname,rawname) |
|
306 |
val args = args_of_op curried typ; |
|
307 |
val num = num_of_args args; |
|
308 |
in |
|
309 |
((external name)^"_strict", |
|
310 |
if num <> 0 |
|
311 |
then HOLogic.mk_Trueprop(s_axm_of curried name typ args num 0) |
|
312 |
else HOLogic.mk_Trueprop(True)) :: strictness_axms curried tail |
|
313 |
end |
|
314 |
| strictness_axms _ [] = []; |
|
315 |
end; (*local*) |
|
316 |
||
317 |
(* producing the totality axioms *) |
|
318 |
||
319 |
fun totality_axms curried ((rawname,typ,cmixfix)::tail) = |
|
320 |
let val name = case cmixfix of |
|
321 |
(CInfixl _) => (mk_internal_name rawname,rawname) |
|
322 |
| (CInfixr _) => (mk_internal_name rawname,rawname) |
|
323 |
| _ => (rawname,rawname) |
|
324 |
val args = args_of_op curried typ; |
|
325 |
val prems = mk_mkNotEqUU_vars (if curried then rev (types_of args) |
|
326 |
else (types_of args)) 0; |
|
327 |
val term = mk_app (num_of_args args - 1) (internal name,typ) args; |
|
328 |
in |
|
329 |
((external name)^"_total", |
|
330 |
if num_of_args args <> 0 |
|
331 |
then Logic.list_implies (prems,mkNotEqUU term) |
|
332 |
else HOLogic.mk_Trueprop(True)) :: totality_axms curried tail |
|
333 |
end |
|
334 |
| totality_axms _ [] = []; |
|
335 |
||
336 |
||
337 |
||
338 |
(* the theory extenders ****************************) |
|
339 |
||
340 |
fun add_ops {curried,strict,total} raw_decls thy = |
|
341 |
let val {sign,...} = rep_theory thy; |
|
342 |
val decls = map (apsnd_of_three (typ_of o read_ctyp sign)) raw_decls; |
|
343 |
val oldstyledecls = oldstyle decls; |
|
344 |
val syndecls = syn_decls curried sign decls; |
|
345 |
val xrules = xrules_of curried decls; |
|
346 |
val s_axms = (if strict then strictness_axms curried decls else []); |
|
347 |
val t_axms = (if total then totality_axms curried decls else []); |
|
348 |
in |
|
349 |
add_trrules_i xrules (add_axioms_i (s_axms @ t_axms) |
|
350 |
(add_syntax_i syndecls (add_consts_i oldstyledecls thy))) |
|
351 |
end; |
|
352 |
||
353 |
fun add_ops_i {curried,strict,total} decls thy = |
|
354 |
let val {sign,...} = rep_theory thy; |
|
355 |
val oldstyledecls = oldstyle decls; |
|
356 |
val syndecls = syn_decls curried sign decls; |
|
357 |
val xrules = xrules_of curried decls; |
|
358 |
val s_axms = (if strict then strictness_axms curried decls else []); |
|
359 |
val t_axms = (if total then totality_axms curried decls else []); |
|
360 |
in |
|
361 |
add_trrules_i xrules (add_axioms_i (s_axms @ t_axms) |
|
362 |
(add_syntax_i syndecls (add_consts_i oldstyledecls thy))) |
|
363 |
end; |
|
364 |
||
365 |
||
366 |
(* parser: ops_decls ********************************) |
|
367 |
||
368 |
local open ThyParse |
|
369 |
in |
|
370 |
(* the following is an adapted version of const_decls from thy_parse.ML *) |
|
371 |
||
372 |
val names1 = list1 name; |
|
373 |
||
2238
c72a23bbe762
Eta-expanded some declarations that are illegal under value polymorphism
paulson
parents:
1810
diff
changeset
|
374 |
fun split_decls decls = flat (map (fn (xs, y) => map (rpair y) xs) decls); |
1274 | 375 |
|
376 |
fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z); |
|
377 |
||
378 |
fun mk_strict_vals [] = "" |
|
379 |
| mk_strict_vals [name] = |
|
380 |
"get_axiom thy \""^name^"_strict\"\n" |
|
381 |
| mk_strict_vals (name::tail) = |
|
382 |
"get_axiom thy \""^name^"_strict\",\n"^ |
|
383 |
mk_strict_vals tail; |
|
384 |
||
385 |
fun mk_total_vals [] = "" |
|
386 |
| mk_total_vals [name] = |
|
387 |
"get_axiom thy \""^name^"_total\"\n" |
|
388 |
| mk_total_vals (name::tail) = |
|
389 |
"get_axiom thy \""^name^"_total\",\n"^ |
|
390 |
mk_total_vals tail; |
|
391 |
||
392 |
fun mk_ops_decls (((curried,strict),total),list) = |
|
393 |
(* call for the theory extender *) |
|
394 |
("|> ThyOps.add_ops \n"^ |
|
395 |
"{ curried = "^curried^" , strict = "^strict^ |
|
396 |
" , total = "^total^" } \n"^ |
|
397 |
(mk_big_list o map mk_triple2) list^";\n"^ |
|
398 |
"val strict_axms = []; val total_axms = [];\nval thy = thy\n", |
|
399 |
(* additional declarations *) |
|
400 |
(if strict="true" then "val strict_axms = strict_axms @ [\n"^ |
|
401 |
mk_strict_vals (map (strip_quotes o fst) list)^ |
|
402 |
"];\n" |
|
403 |
else "")^ |
|
404 |
(if total="true" then "val total_axms = total_axms @ [\n"^ |
|
405 |
mk_total_vals (map (strip_quotes o fst) list)^ |
|
406 |
"];\n" |
|
407 |
else "")); |
|
408 |
||
409 |
(* mixfix annotations *) |
|
410 |
||
411 |
fun cat_parens pre1 pre2 s = cat pre1 (parens (cat pre2 s)); |
|
412 |
||
413 |
val infxl = "infixl" $$-- !! nat >> cat_parens "ThyOps.Mixfix" "Infixl"; |
|
414 |
val infxr = "infixr" $$-- !! nat >> cat_parens "ThyOps.Mixfix" "Infixr"; |
|
415 |
||
416 |
val cinfxl = "cinfixl" $$-- !! nat >> cat "ThyOps.CInfixl"; |
|
417 |
val cinfxr = "cinfixr" $$-- !! nat >> cat "ThyOps.CInfixr"; |
|
418 |
||
419 |
val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list; |
|
420 |
||
421 |
val cmixfx = "cmixfix" $$-- string -- !! (opt_pris -- optional nat "max_pri") |
|
422 |
>> (cat "ThyOps.CMixfix" o mk_triple2); |
|
423 |
||
424 |
val bindr = "binder" $$-- |
|
425 |
!! (string -- ( ("[" $$-- nat --$$ "]") -- nat |
|
426 |
|| nat >> (fn n => (n,n)) |
|
427 |
) ) |
|
428 |
>> (cat_parens "ThyOps.Mixfix" "Binder" o mk_triple2); |
|
429 |
||
430 |
val mixfx = string -- !! (opt_pris -- optional nat "max_pri") |
|
431 |
>> (cat_parens "ThyOps.Mixfix" "Mixfix" o mk_triple2); |
|
432 |
||
433 |
fun opt_syn fx = optional ("(" $$-- fx --$$ ")") "ThyOps.Mixfix NoSyn"; |
|
434 |
||
435 |
val opt_cmixfix = opt_syn (mixfx || infxl || infxr || bindr || |
|
436 |
cinfxl || cinfxr || cmixfx); |
|
437 |
||
438 |
fun ops_decls toks= |
|
439 |
(optional ($$ "curried" >> K "true") "false" -- |
|
440 |
optional ($$ "strict" >> K "true") "false" -- |
|
441 |
optional ($$ "total" >> K "true") "false" -- |
|
442 |
(repeat1 (names1 --$$ "::" -- !! (string -- opt_cmixfix)) |
|
443 |
>> split_decls) |
|
444 |
>> mk_ops_decls) toks |
|
445 |
||
446 |
end; |
|
447 |
||
448 |
(*** new keywords and sections: ******************************************) |
|
449 |
||
450 |
val ops_keywords = ["curried","strict","total","cinfixl","cinfixr","cmixfix"]; |
|
451 |
(* "::" is already a pure keyword *) |
|
452 |
||
453 |
val ops_sections = [("ops" , ops_decls) ]; |
|
454 |
||
455 |
end; (* the structure ThyOps *) |
|
456 |