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 |
|
10 val add_consts: (binding * typ * mixfix) list -> theory -> theory |
|
11 val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory |
|
12 end; |
|
13 |
|
14 structure Cont_Consts: CONT_CONSTS = |
|
15 struct |
|
16 |
|
17 |
|
18 (* misc utils *) |
|
19 |
|
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], []); |
|
23 |
|
24 fun trans_rules name2 name1 n mx = |
|
25 let |
|
26 val vnames = Name.invents Name.context "a" n; |
|
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), |
|
31 fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a]) |
|
32 vnames (Constant name1))] @ |
|
33 (case mx of |
|
34 Infix _ => [extra_parse_rule] |
|
35 | Infixl _ => [extra_parse_rule] |
|
36 | Infixr _ => [extra_parse_rule] |
|
37 | _ => []) |
|
38 end; |
|
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 *) |
|
47 fun transform thy (c, T, mx) = |
|
48 let |
|
49 fun syntax b = Syntax.mark_const (Sign.full_bname thy b); |
|
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; |
|
58 |
|
59 fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0 |
|
60 | cfun_arity _ = 0; |
|
61 |
|
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; |
|
69 |
|
70 |
|
71 (* add_consts *) |
|
72 |
|
73 local |
|
74 |
|
75 fun gen_add_consts prep_typ raw_decls thy = |
|
76 let |
|
77 val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls; |
|
78 val (contconst_decls, normal_decls) = List.partition is_contconst decls; |
|
79 val transformed_decls = map (transform thy) contconst_decls; |
|
80 in |
|
81 thy |
|
82 |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) |
|
83 |> Sign.add_trrules_i (maps #3 transformed_decls) |
|
84 end; |
|
85 |
|
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; |
|
92 |
|
93 end; |
|