35626
|
1 |
(* Title: Pure/Isar/typedecl.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Type declarations (within the object logic).
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature TYPEDECL =
|
|
8 |
sig
|
35681
|
9 |
val typedecl: binding * string list * mixfix -> local_theory -> typ * local_theory
|
|
10 |
val typedecl_global: binding * string list * mixfix -> theory -> typ * theory
|
35626
|
11 |
end;
|
|
12 |
|
|
13 |
structure Typedecl: TYPEDECL =
|
|
14 |
struct
|
|
15 |
|
35681
|
16 |
fun typedecl (b, vs, mx) lthy =
|
35626
|
17 |
let
|
35681
|
18 |
fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
|
|
19 |
val _ = has_duplicates (op =) vs andalso err "Duplicate parameters";
|
|
20 |
|
|
21 |
val name = Local_Theory.full_name lthy b;
|
35626
|
22 |
val n = length vs;
|
35681
|
23 |
val args = map (fn a => TFree (a, ProofContext.default_sort lthy (a, ~1))) vs;
|
|
24 |
val T = Type (name, args);
|
|
25 |
|
|
26 |
val bad_args =
|
|
27 |
#2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
|
|
28 |
|> filter_out Term.is_TVar;
|
|
29 |
val _ = not (null bad_args) andalso
|
|
30 |
err ("Locally fixed type arguments " ^ commas_quote (map (Syntax.string_of_typ lthy) bad_args));
|
|
31 |
|
|
32 |
val base_sort = Object_Logic.get_base_sort (ProofContext.theory_of lthy);
|
35626
|
33 |
in
|
35681
|
34 |
lthy
|
|
35 |
|> Local_Theory.theory
|
|
36 |
(Sign.add_types [(b, n, NoSyn)] #>
|
|
37 |
(case base_sort of
|
|
38 |
NONE => I
|
|
39 |
| SOME S => AxClass.axiomatize_arity (name, replicate n S, S)))
|
|
40 |
|> Local_Theory.checkpoint
|
|
41 |
|> Local_Theory.type_notation true Syntax.mode_default [(T, mx)]
|
|
42 |
|> Local_Theory.type_syntax false
|
|
43 |
(fn _ => Context.mapping (Sign.type_alias b name) (ProofContext.type_alias b name))
|
|
44 |
|> ProofContext.type_alias b name
|
|
45 |
|> Variable.declare_typ T
|
35626
|
46 |
|> pair T
|
|
47 |
end;
|
|
48 |
|
35681
|
49 |
fun typedecl_global decl =
|
|
50 |
Theory_Target.init NONE
|
|
51 |
#> typedecl decl
|
|
52 |
#> Local_Theory.exit_result_global Morphism.typ;
|
|
53 |
|
35626
|
54 |
end;
|
|
55 |
|