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