src/Pure/Isar/typedecl.ML
author wenzelm
Thu Sep 24 23:33:29 2015 +0200 (2015-09-24)
changeset 61261 ddb2da7cb2e4
parent 61259 6dc3d5d50e57
child 69732 49d25343d3d4
permissions -rw-r--r--
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm@35626
     1
(*  Title:      Pure/Isar/typedecl.ML
wenzelm@35626
     2
    Author:     Makarius
wenzelm@35626
     3
wenzelm@36172
     4
Type declarations (with object-logic arities) and type abbreviations.
wenzelm@35626
     5
*)
wenzelm@35626
     6
wenzelm@35626
     7
signature TYPEDECL =
wenzelm@35626
     8
sig
wenzelm@35838
     9
  val read_constraint: Proof.context -> string option -> sort
wenzelm@61259
    10
  val basic_typedecl: {final: bool} -> binding * int * mixfix ->
wenzelm@61259
    11
    local_theory -> string * local_theory
wenzelm@61259
    12
  val typedecl: {final: bool} -> binding * (string * sort) list * mixfix ->
wenzelm@61259
    13
    local_theory -> typ * local_theory
wenzelm@61259
    14
  val typedecl_global: {final: bool} -> binding * (string * sort) list * mixfix ->
wenzelm@61259
    15
    theory -> typ * theory
wenzelm@36172
    16
  val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory
wenzelm@36172
    17
  val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory
wenzelm@36172
    18
  val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory
wenzelm@35626
    19
end;
wenzelm@35626
    20
wenzelm@35626
    21
structure Typedecl: TYPEDECL =
wenzelm@35626
    22
struct
wenzelm@35626
    23
wenzelm@36153
    24
(* constraints *)
wenzelm@36153
    25
wenzelm@36153
    26
fun read_constraint _ NONE = dummyS
wenzelm@36153
    27
  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
wenzelm@36153
    28
wenzelm@36153
    29
wenzelm@35834
    30
(* primitives *)
wenzelm@35834
    31
wenzelm@36172
    32
fun basic_decl decl (b, n, mx) lthy =
wenzelm@35834
    33
  let val name = Local_Theory.full_name lthy b in
wenzelm@35834
    34
    lthy
wenzelm@38757
    35
    |> Local_Theory.background_theory (decl name)
wenzelm@35834
    36
    |> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)]
wenzelm@35834
    37
    |> Local_Theory.type_alias b name
wenzelm@35834
    38
    |> pair name
wenzelm@35834
    39
  end;
wenzelm@35834
    40
wenzelm@35834
    41
wenzelm@36172
    42
(* global type -- without dependencies on type parameters of the context *)
wenzelm@36172
    43
wenzelm@36172
    44
fun global_type lthy (b, raw_args) =
wenzelm@35626
    45
  let
wenzelm@42381
    46
    fun err msg = error (msg ^ " in type declaration " ^ Binding.print b);
wenzelm@35681
    47
wenzelm@35834
    48
    val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
wenzelm@42360
    49
    val args = map (TFree o Proof_Context.check_tfree lthy) raw_args;
wenzelm@36156
    50
    val T = Type (Local_Theory.full_name lthy b, args);
wenzelm@35681
    51
wenzelm@35681
    52
    val bad_args =
wenzelm@35681
    53
      #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
wenzelm@35681
    54
      |> filter_out Term.is_TVar;
wenzelm@36172
    55
    val _ = null bad_args orelse
wenzelm@35740
    56
      err ("Locally fixed type arguments " ^
wenzelm@35834
    57
        commas_quote (map (Syntax.string_of_typ lthy) bad_args));
wenzelm@36172
    58
  in T end;
wenzelm@36172
    59
wenzelm@61250
    60
fun final_type (b, n) lthy =
wenzelm@61246
    61
  let
wenzelm@61250
    62
    val c = Local_Theory.full_name lthy b;
wenzelm@61250
    63
    val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
wenzelm@61255
    64
  in
wenzelm@61261
    65
    Local_Theory.background_theory
wenzelm@61261
    66
      (Theory.add_deps (Proof_Context.defs_context lthy) "" (Theory.type_dep (c, args)) []) lthy
wenzelm@61255
    67
  end;
wenzelm@61250
    68
wenzelm@61259
    69
fun basic_typedecl {final} (b, n, mx) lthy =
wenzelm@61250
    70
  lthy
wenzelm@61250
    71
  |> basic_decl (fn name =>
wenzelm@61250
    72
    Sign.add_type lthy (b, n, NoSyn) #>
wenzelm@61250
    73
    (case Object_Logic.get_base_sort lthy of
wenzelm@61250
    74
      SOME S => Axclass.arity_axiomatization (name, replicate n S, S)
wenzelm@61250
    75
    | NONE => I)) (b, n, mx)
wenzelm@61250
    76
  ||> final ? final_type (b, n);
wenzelm@61246
    77
wenzelm@36172
    78
wenzelm@36172
    79
(* type declarations *)
wenzelm@36172
    80
wenzelm@61259
    81
fun typedecl {final} (b, raw_args, mx) lthy =
wenzelm@36172
    82
  let val T = global_type lthy (b, raw_args) in
wenzelm@35681
    83
    lthy
wenzelm@61259
    84
    |> basic_typedecl {final = final} (b, length raw_args, mx)
wenzelm@35834
    85
    |> snd
wenzelm@35681
    86
    |> Variable.declare_typ T
wenzelm@35626
    87
    |> pair T
wenzelm@35626
    88
  end;
wenzelm@35626
    89
wenzelm@61259
    90
fun typedecl_global {final} decl =
haftmann@38388
    91
  Named_Target.theory_init
wenzelm@61259
    92
  #> typedecl {final = final} decl
wenzelm@35681
    93
  #> Local_Theory.exit_result_global Morphism.typ;
wenzelm@35681
    94
wenzelm@36172
    95
wenzelm@36172
    96
(* type abbreviations *)
wenzelm@36172
    97
wenzelm@36457
    98
local
wenzelm@36457
    99
wenzelm@36172
   100
fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy =
wenzelm@36172
   101
  let
wenzelm@36172
   102
    val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs);
wenzelm@36457
   103
    val rhs = prep_typ b lthy raw_rhs
wenzelm@42381
   104
      handle ERROR msg => cat_error msg ("in type abbreviation " ^ Binding.print b);
wenzelm@36172
   105
  in
wenzelm@36172
   106
    lthy
wenzelm@42375
   107
    |> basic_decl (fn _ => Sign.add_type_abbrev lthy (b, vs, rhs)) (b, length vs, mx)
wenzelm@36172
   108
    |> snd
wenzelm@36172
   109
    |> pair name
wenzelm@36172
   110
  end;
wenzelm@36172
   111
wenzelm@36457
   112
fun read_abbrev b ctxt raw_rhs =
wenzelm@36457
   113
  let
wenzelm@42360
   114
    val rhs = Proof_Context.read_typ_syntax (ctxt |> Proof_Context.set_defsort []) raw_rhs;
wenzelm@36457
   115
    val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
wenzelm@36457
   116
    val _ =
wenzelm@56294
   117
      if not (null ignored) andalso Context_Position.is_visible ctxt then
wenzelm@56294
   118
        warning
wenzelm@56294
   119
          ("Ignoring sort constraints in type variables(s): " ^
wenzelm@56294
   120
            commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
wenzelm@56294
   121
            "\nin type abbreviation " ^ Binding.print b)
wenzelm@56294
   122
      else ();
wenzelm@36457
   123
  in rhs end;
wenzelm@36457
   124
wenzelm@36457
   125
in
wenzelm@36457
   126
wenzelm@42360
   127
val abbrev = gen_abbrev (K Proof_Context.cert_typ_syntax);
wenzelm@36457
   128
val abbrev_cmd = gen_abbrev read_abbrev;
wenzelm@36457
   129
wenzelm@36457
   130
end;
wenzelm@36172
   131
wenzelm@36172
   132
fun abbrev_global decl rhs =
haftmann@38388
   133
  Named_Target.theory_init
wenzelm@36172
   134
  #> abbrev decl rhs
wenzelm@36172
   135
  #> Local_Theory.exit_result_global (K I);
wenzelm@36172
   136
wenzelm@35626
   137
end;