author | huffman |
Sat, 06 Mar 2010 16:02:22 -0800 | |
changeset 35630 | 8e562d56d404 |
parent 35525 | fa231b86cb1e |
child 36960 | 01594f816e3a |
permissions | -rw-r--r-- |
23152 | 1 |
(* Title: HOLCF/Tools/cont_consts.ML |
2 |
Author: Tobias Mayr, David von Oheimb, and Markus Wenzel |
|
3 |
||
4 |
HOLCF version of consts: handle continuous function types in mixfix |
|
5 |
syntax. |
|
6 |
*) |
|
7 |
||
8 |
signature CONT_CONSTS = |
|
9 |
sig |
|
35257 | 10 |
val add_consts: (binding * typ * mixfix) list -> theory -> theory |
11 |
val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory |
|
23152 | 12 |
end; |
13 |
||
35257 | 14 |
structure Cont_Consts: CONT_CONSTS = |
23152 | 15 |
struct |
16 |
||
17 |
||
18 |
(* misc utils *) |
|
19 |
||
35257 | 20 |
fun change_arrow 0 T = T |
21 |
| change_arrow n (Type (_, [S, T])) = Type ("fun", [S, change_arrow (n - 1) T]) |
|
22 |
| change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []); |
|
23152 | 23 |
|
33245 | 24 |
fun trans_rules name2 name1 n mx = |
25 |
let |
|
35257 | 26 |
val vnames = Name.invents Name.context "a" n; |
33245 | 27 |
val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); |
28 |
in |
|
29 |
[Syntax.ParsePrintRule |
|
30 |
(Syntax.mk_appl (Constant name2) (map Variable vnames), |
|
35257 | 31 |
fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_CFun}) [t, Variable a]) |
33245 | 32 |
vnames (Constant name1))] @ |
33 |
(case mx of |
|
35130 | 34 |
Infix _ => [extra_parse_rule] |
35 |
| Infixl _ => [extra_parse_rule] |
|
36 |
| Infixr _ => [extra_parse_rule] |
|
33245 | 37 |
| _ => []) |
38 |
end; |
|
23152 | 39 |
|
40 |
||
41 |
(* transforming infix/mixfix declarations of constants with type ...->... |
|
42 |
a declaration of such a constant is transformed to a normal declaration with |
|
43 |
an internal name, the same type, and nofix. Additionally, a purely syntactic |
|
44 |
declaration with the original name, type ...=>..., and the original mixfix |
|
45 |
is generated and connected to the other declaration via some translation. |
|
46 |
*) |
|
35257 | 47 |
fun transform thy (c, T, mx) = |
48 |
let |
|
35262
9ea4445d2ccf
slightly more abstract syntax mark/unmark operations;
wenzelm
parents:
35257
diff
changeset
|
49 |
fun syntax b = Syntax.mark_const (Sign.full_bname thy b); |
35257 | 50 |
val c1 = Binding.name_of c; |
51 |
val c2 = c1 ^ "_cont_syntax"; |
|
52 |
val n = Syntax.mixfix_args mx; |
|
53 |
in |
|
54 |
((c, T, NoSyn), |
|
55 |
(Binding.name c2, change_arrow n T, mx), |
|
56 |
trans_rules (syntax c2) (syntax c1) n mx) |
|
57 |
end; |
|
23152 | 58 |
|
35525 | 59 |
fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0 |
35257 | 60 |
| cfun_arity _ = 0; |
23152 | 61 |
|
35257 | 62 |
fun is_contconst (_, _, NoSyn) = false |
63 |
| is_contconst (_, _, Binder _) = false (* FIXME ? *) |
|
64 |
| is_contconst (c, T, mx) = |
|
65 |
let |
|
66 |
val n = Syntax.mixfix_args mx handle ERROR msg => |
|
67 |
cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c)); |
|
68 |
in cfun_arity T >= n end; |
|
23152 | 69 |
|
70 |
||
35257 | 71 |
(* add_consts *) |
72 |
||
73 |
local |
|
23152 | 74 |
|
75 |
fun gen_add_consts prep_typ raw_decls thy = |
|
76 |
let |
|
35257 | 77 |
val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls; |
23152 | 78 |
val (contconst_decls, normal_decls) = List.partition is_contconst decls; |
35257 | 79 |
val transformed_decls = map (transform thy) contconst_decls; |
23152 | 80 |
in |
81 |
thy |
|
35257 | 82 |
|> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) |
83 |
|> Sign.add_trrules_i (maps #3 transformed_decls) |
|
23152 | 84 |
end; |
85 |
||
35257 | 86 |
in |
87 |
||
88 |
val add_consts = gen_add_consts Sign.certify_typ; |
|
89 |
val add_consts_cmd = gen_add_consts Syntax.read_typ_global; |
|
90 |
||
91 |
end; |
|
23152 | 92 |
|
93 |
||
94 |
(* outer syntax *) |
|
95 |
||
96 |
local structure P = OuterParse and K = OuterKeyword in |
|
97 |
||
24867 | 98 |
val _ = |
23152 | 99 |
OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl |
35257 | 100 |
(Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts_cmd)); |
23152 | 101 |
|
102 |
end; |
|
103 |
||
104 |
end; |