author | wenzelm |
Sat, 16 Apr 2011 15:47:52 +0200 | |
changeset 42360 | da8817d01e7c |
parent 38831 | 4933a3dfd745 |
child 42375 | 774df7c59508 |
permissions | -rw-r--r-- |
35626 | 1 |
(* Title: Pure/Isar/typedecl.ML |
2 |
Author: Makarius |
|
3 |
||
36172 | 4 |
Type declarations (with object-logic arities) and type abbreviations. |
35626 | 5 |
*) |
6 |
||
7 |
signature TYPEDECL = |
|
8 |
sig |
|
35838 | 9 |
val read_constraint: Proof.context -> string option -> sort |
36153
1ac501e16a6a
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents:
35838
diff
changeset
|
10 |
val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory |
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
11 |
val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
12 |
val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory |
36172 | 13 |
val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory |
14 |
val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory |
|
15 |
val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory |
|
35626 | 16 |
end; |
17 |
||
18 |
structure Typedecl: TYPEDECL = |
|
19 |
struct |
|
20 |
||
36153
1ac501e16a6a
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents:
35838
diff
changeset
|
21 |
(* constraints *) |
1ac501e16a6a
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents:
35838
diff
changeset
|
22 |
|
1ac501e16a6a
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents:
35838
diff
changeset
|
23 |
fun read_constraint _ NONE = dummyS |
1ac501e16a6a
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents:
35838
diff
changeset
|
24 |
| read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; |
1ac501e16a6a
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents:
35838
diff
changeset
|
25 |
|
1ac501e16a6a
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents:
35838
diff
changeset
|
26 |
|
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
27 |
(* primitives *) |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
28 |
|
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
29 |
fun object_logic_arity name thy = |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
30 |
(case Object_Logic.get_base_sort thy of |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
31 |
NONE => thy |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
32 |
| SOME S => AxClass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy); |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
33 |
|
36172 | 34 |
fun basic_decl decl (b, n, mx) lthy = |
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
35 |
let val name = Local_Theory.full_name lthy b in |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
36 |
lthy |
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38388
diff
changeset
|
37 |
|> Local_Theory.background_theory (decl name) |
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
38 |
|> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)] |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
39 |
|> Local_Theory.type_alias b name |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
40 |
|> pair name |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
41 |
end; |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
42 |
|
36172 | 43 |
fun basic_typedecl (b, n, mx) = |
44 |
basic_decl (fn name => Sign.add_types [(b, n, NoSyn)] #> object_logic_arity name) (b, n, mx); |
|
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
45 |
|
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
46 |
|
36172 | 47 |
(* global type -- without dependencies on type parameters of the context *) |
48 |
||
49 |
fun global_type lthy (b, raw_args) = |
|
35626 | 50 |
let |
35681 | 51 |
fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b)); |
52 |
||
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
53 |
val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters"; |
42360 | 54 |
val args = map (TFree o Proof_Context.check_tfree lthy) raw_args; |
36156 | 55 |
val T = Type (Local_Theory.full_name lthy b, args); |
35681 | 56 |
|
57 |
val bad_args = |
|
58 |
#2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T)) |
|
59 |
|> filter_out Term.is_TVar; |
|
36172 | 60 |
val _ = null bad_args orelse |
35740
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
61 |
err ("Locally fixed type arguments " ^ |
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
62 |
commas_quote (map (Syntax.string_of_typ lthy) bad_args)); |
36172 | 63 |
in T end; |
64 |
||
65 |
||
66 |
(* type declarations *) |
|
67 |
||
68 |
fun typedecl (b, raw_args, mx) lthy = |
|
69 |
let val T = global_type lthy (b, raw_args) in |
|
35681 | 70 |
lthy |
36172 | 71 |
|> basic_typedecl (b, length raw_args, mx) |
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
72 |
|> snd |
35681 | 73 |
|> Variable.declare_typ T |
35626 | 74 |
|> pair T |
75 |
end; |
|
76 |
||
35681 | 77 |
fun typedecl_global decl = |
38388 | 78 |
Named_Target.theory_init |
35681 | 79 |
#> typedecl decl |
80 |
#> Local_Theory.exit_result_global Morphism.typ; |
|
81 |
||
36172 | 82 |
|
83 |
(* type abbreviations *) |
|
84 |
||
36457
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
85 |
local |
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
86 |
|
36172 | 87 |
fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy = |
88 |
let |
|
89 |
val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs); |
|
36457
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
90 |
val rhs = prep_typ b lthy raw_rhs |
36172 | 91 |
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b)); |
92 |
in |
|
93 |
lthy |
|
36179
f45c708bcc01
replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
wenzelm
parents:
36175
diff
changeset
|
94 |
|> basic_decl (fn _ => Sign.add_type_abbrev (b, vs, rhs)) (b, length vs, mx) |
36172 | 95 |
|> snd |
96 |
|> pair name |
|
97 |
end; |
|
98 |
||
36457
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
99 |
fun read_abbrev b ctxt raw_rhs = |
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
100 |
let |
42360 | 101 |
val rhs = Proof_Context.read_typ_syntax (ctxt |> Proof_Context.set_defsort []) raw_rhs; |
36457
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
102 |
val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs []; |
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
103 |
val _ = |
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
104 |
if null ignored then () |
38831
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38757
diff
changeset
|
105 |
else Context_Position.if_visible ctxt warning |
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38757
diff
changeset
|
106 |
("Ignoring sort constraints in type variables(s): " ^ |
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38757
diff
changeset
|
107 |
commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^ |
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38757
diff
changeset
|
108 |
"\nin type abbreviation " ^ quote (Binding.str_of b)); |
36457
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
109 |
in rhs end; |
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
110 |
|
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
111 |
in |
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
112 |
|
42360 | 113 |
val abbrev = gen_abbrev (K Proof_Context.cert_typ_syntax); |
36457
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
114 |
val abbrev_cmd = gen_abbrev read_abbrev; |
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
115 |
|
7355af2a7e8a
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
wenzelm
parents:
36179
diff
changeset
|
116 |
end; |
36172 | 117 |
|
118 |
fun abbrev_global decl rhs = |
|
38388 | 119 |
Named_Target.theory_init |
36172 | 120 |
#> abbrev decl rhs |
121 |
#> Local_Theory.exit_result_global (K I); |
|
122 |
||
35626 | 123 |
end; |
124 |