author | wenzelm |
Tue, 22 Sep 2015 22:38:22 +0200 | |
changeset 61255 | 15865e0c5598 |
parent 61250 | 2f77019f6d0a |
child 61259 | 6dc3d5d50e57 |
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 |
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59970
diff
changeset
|
10 |
val basic_typedecl: bool -> binding * int * mixfix -> local_theory -> string * local_theory |
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59970
diff
changeset
|
11 |
val typedecl: bool -> binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory |
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59970
diff
changeset
|
12 |
val typedecl_global: bool -> 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 |
|
36172 | 29 |
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
|
30 |
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
|
31 |
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
|
32 |
|> 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
|
33 |
|> 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
|
34 |
|> 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
|
35 |
|> 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
|
36 |
end; |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
37 |
|
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
38 |
|
36172 | 39 |
(* global type -- without dependencies on type parameters of the context *) |
40 |
||
41 |
fun global_type lthy (b, raw_args) = |
|
35626 | 42 |
let |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42375
diff
changeset
|
43 |
fun err msg = error (msg ^ " in type declaration " ^ Binding.print b); |
35681 | 44 |
|
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 |
val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters"; |
42360 | 46 |
val args = map (TFree o Proof_Context.check_tfree lthy) raw_args; |
36156 | 47 |
val T = Type (Local_Theory.full_name lthy b, args); |
35681 | 48 |
|
49 |
val bad_args = |
|
50 |
#2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T)) |
|
51 |
|> filter_out Term.is_TVar; |
|
36172 | 52 |
val _ = null bad_args orelse |
35740
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
53 |
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
|
54 |
commas_quote (map (Syntax.string_of_typ lthy) bad_args)); |
36172 | 55 |
in T end; |
56 |
||
61250
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
57 |
fun final_type (b, n) lthy = |
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59970
diff
changeset
|
58 |
let |
61250
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
59 |
val c = Local_Theory.full_name lthy b; |
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
60 |
val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); |
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61250
diff
changeset
|
61 |
in |
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61250
diff
changeset
|
62 |
Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.type_dep (c, args)) []) lthy |
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61250
diff
changeset
|
63 |
end; |
61250
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
64 |
|
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
65 |
fun basic_typedecl final (b, n, mx) lthy = |
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
66 |
lthy |
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
67 |
|> basic_decl (fn name => |
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
68 |
Sign.add_type lthy (b, n, NoSyn) #> |
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
69 |
(case Object_Logic.get_base_sort lthy of |
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
70 |
SOME S => Axclass.arity_axiomatization (name, replicate n S, S) |
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
71 |
| NONE => I)) (b, n, mx) |
2f77019f6d0a
clarified deps entry: global names for arguments;
wenzelm
parents:
61247
diff
changeset
|
72 |
||> final ? final_type (b, n); |
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59970
diff
changeset
|
73 |
|
36172 | 74 |
|
75 |
(* type declarations *) |
|
76 |
||
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59970
diff
changeset
|
77 |
fun typedecl final (b, raw_args, mx) lthy = |
36172 | 78 |
let val T = global_type lthy (b, raw_args) in |
35681 | 79 |
lthy |
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59970
diff
changeset
|
80 |
|> basic_typedecl final (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
|
81 |
|> snd |
35681 | 82 |
|> Variable.declare_typ T |
35626 | 83 |
|> pair T |
84 |
end; |
|
85 |
||
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59970
diff
changeset
|
86 |
fun typedecl_global final decl = |
38388 | 87 |
Named_Target.theory_init |
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59970
diff
changeset
|
88 |
#> typedecl final decl |
35681 | 89 |
#> Local_Theory.exit_result_global Morphism.typ; |
90 |
||
36172 | 91 |
|
92 |
(* type abbreviations *) |
|
93 |
||
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
|
94 |
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
|
95 |
|
36172 | 96 |
fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy = |
97 |
let |
|
98 |
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
|
99 |
val rhs = prep_typ b lthy raw_rhs |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42375
diff
changeset
|
100 |
handle ERROR msg => cat_error msg ("in type abbreviation " ^ Binding.print b); |
36172 | 101 |
in |
102 |
lthy |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset
|
103 |
|> basic_decl (fn _ => Sign.add_type_abbrev lthy (b, vs, rhs)) (b, length vs, mx) |
36172 | 104 |
|> snd |
105 |
|> pair name |
|
106 |
end; |
|
107 |
||
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
|
108 |
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
|
109 |
let |
42360 | 110 |
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
|
111 |
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
|
112 |
val _ = |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
51685
diff
changeset
|
113 |
if not (null ignored) andalso Context_Position.is_visible ctxt then |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
51685
diff
changeset
|
114 |
warning |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
51685
diff
changeset
|
115 |
("Ignoring sort constraints in type variables(s): " ^ |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
51685
diff
changeset
|
116 |
commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^ |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
51685
diff
changeset
|
117 |
"\nin type abbreviation " ^ Binding.print b) |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
51685
diff
changeset
|
118 |
else (); |
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
|
119 |
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
|
120 |
|
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
|
121 |
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
|
122 |
|
42360 | 123 |
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
|
124 |
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
|
125 |
|
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
|
126 |
end; |
36172 | 127 |
|
128 |
fun abbrev_global decl rhs = |
|
38388 | 129 |
Named_Target.theory_init |
36172 | 130 |
#> abbrev decl rhs |
131 |
#> Local_Theory.exit_result_global (K I); |
|
132 |
||
35626 | 133 |
end; |