src/Pure/Isar/typedecl.ML
author nipkow
Fri, 21 Jun 2013 09:00:26 +0200
changeset 52402 c2f30ba4bb98
parent 51685 385ef6706252
child 56294 85911b8a6868
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35626
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/typedecl.ML
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
     3
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
     4
Type declarations (with object-logic arities) and type abbreviations.
35626
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
     5
*)
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
     6
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
     7
signature TYPEDECL =
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
     8
sig
35838
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35834
diff changeset
     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
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    13
  val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    14
  val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    15
  val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory
35626
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
    16
end;
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
    17
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
    18
structure Typedecl: TYPEDECL =
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
    19
struct
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
    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
51685
385ef6706252 more standard module name Axclass (according to file name);
wenzelm
parents: 47005
diff changeset
    32
  | SOME S => Axclass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
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
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    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
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
    43
fun basic_typedecl (b, n, mx) lthy =
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 42381
diff changeset
    44
  basic_decl (fn name => Sign.add_type lthy (b, n, NoSyn) #> object_logic_arity name)
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
    45
    (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
    46
0c71e0d72d7a eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
wenzelm
parents: 35740
diff changeset
    47
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    48
(* global type -- without dependencies on type parameters of the context *)
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    49
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    50
fun global_type lthy (b, raw_args) =
35626
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
    51
  let
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42375
diff changeset
    52
    fun err msg = error (msg ^ " in type declaration " ^ Binding.print b);
35681
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    53
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
    val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 38831
diff changeset
    55
    val args = map (TFree o Proof_Context.check_tfree lthy) raw_args;
36156
6f0a8f6b1671 explicit ProofContext.check_tfree;
wenzelm
parents: 36153
diff changeset
    56
    val T = Type (Local_Theory.full_name lthy b, args);
35681
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    57
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    58
    val bad_args =
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    59
      #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    60
      |> filter_out Term.is_TVar;
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    61
    val _ = null bad_args orelse
35740
d3726291f252 added typedecl_wrt, which affects default sorts of type args;
wenzelm
parents: 35714
diff changeset
    62
      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
    63
        commas_quote (map (Syntax.string_of_typ lthy) bad_args));
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    64
  in T end;
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    65
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    66
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    67
(* type declarations *)
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    68
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    69
fun typedecl (b, raw_args, mx) lthy =
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    70
  let val T = global_type lthy (b, raw_args) in
35681
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    71
    lthy
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    72
    |> 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
    73
    |> snd
35681
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    74
    |> Variable.declare_typ T
35626
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
    75
    |> pair T
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
    76
  end;
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
    77
35681
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    78
fun typedecl_global decl =
38388
94d5624dd1f7 Named_Target.theory_init
haftmann
parents: 38350
diff changeset
    79
  Named_Target.theory_init
35681
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    80
  #> typedecl decl
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    81
  #> Local_Theory.exit_result_global Morphism.typ;
8b22a498b034 localized typedecl;
wenzelm
parents: 35626
diff changeset
    82
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    83
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    84
(* type abbreviations *)
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    85
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
    86
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
    87
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    88
fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy =
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    89
  let
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    90
    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
    91
    val rhs = prep_typ b lthy raw_rhs
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42375
diff changeset
    92
      handle ERROR msg => cat_error msg ("in type abbreviation " ^ Binding.print b);
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    93
  in
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    94
    lthy
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
    95
    |> basic_decl (fn _ => Sign.add_type_abbrev lthy (b, vs, rhs)) (b, length vs, mx)
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    96
    |> snd
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    97
    |> pair name
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    98
  end;
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
    99
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
   100
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
   101
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 38831
diff changeset
   102
    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
   103
    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
   104
    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
   105
      if null ignored then ()
38831
4933a3dfd745 more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents: 38757
diff changeset
   106
      else Context_Position.if_visible ctxt warning
4933a3dfd745 more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents: 38757
diff changeset
   107
        ("Ignoring sort constraints in type variables(s): " ^
4933a3dfd745 more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents: 38757
diff changeset
   108
          commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42375
diff changeset
   109
          "\nin type abbreviation " ^ Binding.print 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
   110
  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
   111
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
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
   113
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 38831
diff changeset
   114
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
   115
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
   116
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
   117
end;
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
   118
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
   119
fun abbrev_global decl rhs =
38388
94d5624dd1f7 Named_Target.theory_init
haftmann
parents: 38350
diff changeset
   120
  Named_Target.theory_init
36172
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
   121
  #> abbrev decl rhs
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
   122
  #> Local_Theory.exit_result_global (K I);
fc407d02af4a local type abbreviations;
wenzelm
parents: 36156
diff changeset
   123
35626
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
   124
end;
06197484c6ad separate structure Typedecl;
wenzelm
parents:
diff changeset
   125