author | wenzelm |
Thu, 15 Apr 2010 18:09:22 +0200 | |
changeset 36153 | 1ac501e16a6a |
parent 35838 | c8bd075c4de8 |
child 36156 | 6f0a8f6b1671 |
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 |
|
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 |
35626 | 13 |
end; |
14 |
||
15 |
structure Typedecl: TYPEDECL = |
|
16 |
struct |
|
17 |
||
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
|
18 |
(* 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
|
19 |
|
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
|
20 |
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
|
21 |
| 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
|
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 |
|
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
24 |
(* primitives *) |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
25 |
|
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
26 |
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
|
27 |
(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
|
28 |
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
|
29 |
| 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
|
30 |
|
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
31 |
fun basic_typedecl (b, n, mx) lthy = |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
32 |
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
|
33 |
lthy |
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.theory (Sign.add_types [(b, n, NoSyn)] #> object_logic_arity 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 |
|> 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
|
36 |
|> 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
|
37 |
|> 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
|
38 |
end; |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
39 |
|
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
40 |
|
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
|
41 |
(* regular typedecl -- without dependencies on type parameters of the context *) |
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
42 |
|
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
43 |
fun typedecl (b, raw_args, mx) lthy = |
35626 | 44 |
let |
35681 | 45 |
fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b)); |
46 |
||
35834
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
47 |
val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters"; |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
48 |
val args = raw_args |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
49 |
|> map (fn (a, S) => (a, if S = dummyS then ProofContext.default_sort lthy (a, ~1) else S)); |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
50 |
val T = Type (Local_Theory.full_name lthy b, map TFree args); |
35681 | 51 |
|
52 |
val bad_args = |
|
53 |
#2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T)) |
|
54 |
|> filter_out Term.is_TVar; |
|
55 |
val _ = not (null bad_args) andalso |
|
35740
d3726291f252
added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents:
35714
diff
changeset
|
56 |
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
|
57 |
commas_quote (map (Syntax.string_of_typ lthy) bad_args)); |
35626 | 58 |
in |
35681 | 59 |
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
|
60 |
|> basic_typedecl (b, length args, mx) |
0c71e0d72d7a
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents:
35740
diff
changeset
|
61 |
|> snd |
35681 | 62 |
|> Variable.declare_typ T |
35626 | 63 |
|> pair T |
64 |
end; |
|
65 |
||
35681 | 66 |
fun typedecl_global decl = |
67 |
Theory_Target.init NONE |
|
68 |
#> typedecl decl |
|
69 |
#> Local_Theory.exit_result_global Morphism.typ; |
|
70 |
||
35626 | 71 |
end; |
72 |