author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 43329 | 84472e198515 |
child 56239 | 17df7145a871 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tools/cont_consts.ML |
23152 | 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 |
|
40832 | 12 |
end |
23152 | 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]) |
|
40832 | 22 |
| change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []) |
23152 | 23 |
|
33245 | 24 |
fun trans_rules name2 name1 n mx = |
25 |
let |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42381
diff
changeset
|
26 |
val vnames = Name.invent Name.context "a" n |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42204
diff
changeset
|
27 |
val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1) |
33245 | 28 |
in |
42204 | 29 |
[Syntax.Parse_Print_Rule |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42204
diff
changeset
|
30 |
(Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames), |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42204
diff
changeset
|
31 |
fold (fn a => fn t => |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42204
diff
changeset
|
32 |
Ast.mk_appl (Ast.Constant @{const_syntax Rep_cfun}) [t, Ast.Variable a]) |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42204
diff
changeset
|
33 |
vnames (Ast.Constant name1))] @ |
33245 | 34 |
(case mx of |
35130 | 35 |
Infix _ => [extra_parse_rule] |
36 |
| Infixl _ => [extra_parse_rule] |
|
37 |
| Infixr _ => [extra_parse_rule] |
|
33245 | 38 |
| _ => []) |
40832 | 39 |
end |
23152 | 40 |
|
41 |
||
42 |
(* transforming infix/mixfix declarations of constants with type ...->... |
|
43 |
a declaration of such a constant is transformed to a normal declaration with |
|
44 |
an internal name, the same type, and nofix. Additionally, a purely syntactic |
|
45 |
declaration with the original name, type ...=>..., and the original mixfix |
|
46 |
is generated and connected to the other declaration via some translation. |
|
47 |
*) |
|
35257 | 48 |
fun transform thy (c, T, mx) = |
49 |
let |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42287
diff
changeset
|
50 |
fun syntax b = Lexicon.mark_const (Sign.full_bname thy b) |
40832 | 51 |
val c1 = Binding.name_of c |
52 |
val c2 = c1 ^ "_cont_syntax" |
|
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42224
diff
changeset
|
53 |
val n = Mixfix.mixfix_args mx |
35257 | 54 |
in |
55 |
((c, T, NoSyn), |
|
56 |
(Binding.name c2, change_arrow n T, mx), |
|
57 |
trans_rules (syntax c2) (syntax c1) n mx) |
|
40832 | 58 |
end |
23152 | 59 |
|
35525 | 60 |
fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0 |
40832 | 61 |
| cfun_arity _ = 0 |
23152 | 62 |
|
35257 | 63 |
fun is_contconst (_, _, NoSyn) = false |
64 |
| is_contconst (_, _, Binder _) = false (* FIXME ? *) |
|
65 |
| is_contconst (c, T, mx) = |
|
66 |
let |
|
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42224
diff
changeset
|
67 |
val n = Mixfix.mixfix_args mx handle ERROR msg => |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42290
diff
changeset
|
68 |
cat_error msg ("in mixfix annotation for " ^ Binding.print c) |
40832 | 69 |
in cfun_arity T >= n end |
23152 | 70 |
|
71 |
||
35257 | 72 |
(* add_consts *) |
73 |
||
74 |
local |
|
23152 | 75 |
|
76 |
fun gen_add_consts prep_typ raw_decls thy = |
|
77 |
let |
|
40832 | 78 |
val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls |
79 |
val (contconst_decls, normal_decls) = List.partition is_contconst decls |
|
80 |
val transformed_decls = map (transform thy) contconst_decls |
|
23152 | 81 |
in |
82 |
thy |
|
35257 | 83 |
|> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) |
42204 | 84 |
|> Sign.add_trrules (maps #3 transformed_decls) |
40832 | 85 |
end |
23152 | 86 |
|
35257 | 87 |
in |
88 |
||
40832 | 89 |
val add_consts = gen_add_consts Sign.certify_typ |
90 |
val add_consts_cmd = gen_add_consts Syntax.read_typ_global |
|
35257 | 91 |
|
40832 | 92 |
end |
23152 | 93 |
|
40832 | 94 |
end |