author | wenzelm |
Sat, 13 Mar 2010 14:41:37 +0100 | |
changeset 35740 | d3726291f252 |
parent 35714 | 68f7603f2aeb |
child 35834 | 0c71e0d72d7a |
permissions | -rw-r--r-- |
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 |
|
35740
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
9 |
val typedecl_wrt: term list -> binding * string list * mixfix -> |
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
10 |
local_theory -> typ * local_theory |
35681 | 11 |
val typedecl: binding * string list * mixfix -> local_theory -> typ * local_theory |
12 |
val typedecl_global: binding * string list * mixfix -> theory -> typ * theory |
|
35626 | 13 |
end; |
14 |
||
15 |
structure Typedecl: TYPEDECL = |
|
16 |
struct |
|
17 |
||
35740
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
18 |
fun typedecl_wrt terms (b, vs, mx) lthy = |
35626 | 19 |
let |
35681 | 20 |
fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b)); |
21 |
val _ = has_duplicates (op =) vs andalso err "Duplicate parameters"; |
|
22 |
||
23 |
val name = Local_Theory.full_name lthy b; |
|
35626 | 24 |
val n = length vs; |
35740
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
25 |
|
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
26 |
val args_ctxt = lthy |> fold Variable.declare_constraints terms; |
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
27 |
val args = map (fn a => TFree (a, ProofContext.default_sort args_ctxt (a, ~1))) vs; |
35681 | 28 |
val T = Type (name, args); |
29 |
||
30 |
val bad_args = |
|
31 |
#2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T)) |
|
32 |
|> filter_out Term.is_TVar; |
|
33 |
val _ = not (null bad_args) andalso |
|
35740
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
34 |
err ("Locally fixed type arguments " ^ |
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
35 |
commas_quote (map (Syntax.string_of_typ args_ctxt) bad_args)); |
35681 | 36 |
|
37 |
val base_sort = Object_Logic.get_base_sort (ProofContext.theory_of lthy); |
|
35626 | 38 |
in |
35681 | 39 |
lthy |
40 |
|> Local_Theory.theory |
|
41 |
(Sign.add_types [(b, n, NoSyn)] #> |
|
42 |
(case base_sort of |
|
43 |
NONE => I |
|
44 |
| SOME S => AxClass.axiomatize_arity (name, replicate n S, S))) |
|
45 |
|> Local_Theory.type_notation true Syntax.mode_default [(T, mx)] |
|
35740
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
46 |
|> Local_Theory.type_alias b name |
35681 | 47 |
|> Variable.declare_typ T |
35626 | 48 |
|> pair T |
49 |
end; |
|
50 |
||
35740
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
51 |
val typedecl = typedecl_wrt []; |
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
52 |
|
35681 | 53 |
fun typedecl_global decl = |
54 |
Theory_Target.init NONE |
|
55 |
#> typedecl decl |
|
56 |
#> Local_Theory.exit_result_global Morphism.typ; |
|
57 |
||
35626 | 58 |
end; |
59 |