src/Pure/Isar/typedecl.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 36457 7355af2a7e8a
child 38350 480b2de9927c
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
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@36153
    10
  val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory
wenzelm@35834
    11
  val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
wenzelm@35834
    12
  val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory
wenzelm@36172
    13
  val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory
wenzelm@36172
    14
  val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory
wenzelm@36172
    15
  val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory
wenzelm@35626
    16
end;
wenzelm@35626
    17
wenzelm@35626
    18
structure Typedecl: TYPEDECL =
wenzelm@35626
    19
struct
wenzelm@35626
    20
wenzelm@36153
    21
(* constraints *)
wenzelm@36153
    22
wenzelm@36153
    23
fun read_constraint _ NONE = dummyS
wenzelm@36153
    24
  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
wenzelm@36153
    25
wenzelm@36153
    26
wenzelm@35834
    27
(* primitives *)
wenzelm@35834
    28
wenzelm@35834
    29
fun object_logic_arity name thy =
wenzelm@35834
    30
  (case Object_Logic.get_base_sort thy of
wenzelm@35834
    31
    NONE => thy
wenzelm@35834
    32
  | SOME S => AxClass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
wenzelm@35834
    33
wenzelm@36172
    34
fun basic_decl decl (b, n, mx) lthy =
wenzelm@35834
    35
  let val name = Local_Theory.full_name lthy b in
wenzelm@35834
    36
    lthy
wenzelm@36172
    37
    |> Local_Theory.theory (decl name)
wenzelm@35834
    38
    |> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)]
wenzelm@35834
    39
    |> Local_Theory.type_alias b name
wenzelm@35834
    40
    |> pair name
wenzelm@35834
    41
  end;
wenzelm@35834
    42
wenzelm@36172
    43
fun basic_typedecl (b, n, mx) =
wenzelm@36172
    44
  basic_decl (fn name => Sign.add_types [(b, n, NoSyn)] #> object_logic_arity name) (b, n, mx);
wenzelm@35834
    45
wenzelm@35834
    46
wenzelm@36172
    47
(* global type -- without dependencies on type parameters of the context *)
wenzelm@36172
    48
wenzelm@36172
    49
fun global_type lthy (b, raw_args) =
wenzelm@35626
    50
  let
wenzelm@35681
    51
    fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
wenzelm@35681
    52
wenzelm@35834
    53
    val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
wenzelm@36156
    54
    val args = map (TFree o ProofContext.check_tfree lthy) raw_args;
wenzelm@36156
    55
    val T = Type (Local_Theory.full_name lthy b, args);
wenzelm@35681
    56
wenzelm@35681
    57
    val bad_args =
wenzelm@35681
    58
      #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
wenzelm@35681
    59
      |> filter_out Term.is_TVar;
wenzelm@36172
    60
    val _ = null bad_args orelse
wenzelm@35740
    61
      err ("Locally fixed type arguments " ^
wenzelm@35834
    62
        commas_quote (map (Syntax.string_of_typ lthy) bad_args));
wenzelm@36172
    63
  in T end;
wenzelm@36172
    64
wenzelm@36172
    65
wenzelm@36172
    66
(* type declarations *)
wenzelm@36172
    67
wenzelm@36172
    68
fun typedecl (b, raw_args, mx) lthy =
wenzelm@36172
    69
  let val T = global_type lthy (b, raw_args) in
wenzelm@35681
    70
    lthy
wenzelm@36172
    71
    |> basic_typedecl (b, length raw_args, mx)
wenzelm@35834
    72
    |> snd
wenzelm@35681
    73
    |> Variable.declare_typ T
wenzelm@35626
    74
    |> pair T
wenzelm@35626
    75
  end;
wenzelm@35626
    76
wenzelm@35681
    77
fun typedecl_global decl =
wenzelm@35681
    78
  Theory_Target.init NONE
wenzelm@35681
    79
  #> typedecl decl
wenzelm@35681
    80
  #> Local_Theory.exit_result_global Morphism.typ;
wenzelm@35681
    81
wenzelm@36172
    82
wenzelm@36172
    83
(* type abbreviations *)
wenzelm@36172
    84
wenzelm@36457
    85
local
wenzelm@36457
    86
wenzelm@36172
    87
fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy =
wenzelm@36172
    88
  let
wenzelm@36172
    89
    val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs);
wenzelm@36457
    90
    val rhs = prep_typ b lthy raw_rhs
wenzelm@36172
    91
      handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
wenzelm@36172
    92
  in
wenzelm@36172
    93
    lthy
wenzelm@36179
    94
    |> basic_decl (fn _ => Sign.add_type_abbrev (b, vs, rhs)) (b, length vs, mx)
wenzelm@36172
    95
    |> snd
wenzelm@36172
    96
    |> pair name
wenzelm@36172
    97
  end;
wenzelm@36172
    98
wenzelm@36457
    99
fun read_abbrev b ctxt raw_rhs =
wenzelm@36457
   100
  let
wenzelm@36457
   101
    val rhs = ProofContext.read_typ_syntax (ctxt |> ProofContext.set_defsort []) raw_rhs;
wenzelm@36457
   102
    val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
wenzelm@36457
   103
    val _ =
wenzelm@36457
   104
      if null ignored then ()
wenzelm@36457
   105
      else warning ("Ignoring sort constraints in type variables(s): " ^
wenzelm@36457
   106
        commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
wenzelm@36457
   107
        "\nin type abbreviation " ^ quote (Binding.str_of b));
wenzelm@36457
   108
  in rhs end;
wenzelm@36457
   109
wenzelm@36457
   110
in
wenzelm@36457
   111
wenzelm@36457
   112
val abbrev = gen_abbrev (K ProofContext.cert_typ_syntax);
wenzelm@36457
   113
val abbrev_cmd = gen_abbrev read_abbrev;
wenzelm@36457
   114
wenzelm@36457
   115
end;
wenzelm@36172
   116
wenzelm@36172
   117
fun abbrev_global decl rhs =
wenzelm@36172
   118
  Theory_Target.init NONE
wenzelm@36172
   119
  #> abbrev decl rhs
wenzelm@36172
   120
  #> Local_Theory.exit_result_global (K I);
wenzelm@36172
   121
wenzelm@35626
   122
end;
wenzelm@35626
   123