src/Pure/Isar/typedecl.ML
author wenzelm
Mon Nov 14 16:52:19 2011 +0100 (2011-11-14 ago)
changeset 45488 6d71d9e52369
parent 42381 309ec68442c6
child 47005 421760a1efe7
permissions -rw-r--r--
pass positions for named targets, for formal links in the document model;
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@38757
    37
    |> Local_Theory.background_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@42375
    43
fun basic_typedecl (b, n, mx) lthy =
wenzelm@42375
    44
  basic_decl (fn name => Sign.add_types lthy [(b, n, NoSyn)] #> object_logic_arity name)
wenzelm@42375
    45
    (b, n, mx) lthy;
wenzelm@35834
    46
wenzelm@35834
    47
wenzelm@36172
    48
(* global type -- without dependencies on type parameters of the context *)
wenzelm@36172
    49
wenzelm@36172
    50
fun global_type lthy (b, raw_args) =
wenzelm@35626
    51
  let
wenzelm@42381
    52
    fun err msg = error (msg ^ " in type declaration " ^ Binding.print b);
wenzelm@35681
    53
wenzelm@35834
    54
    val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
wenzelm@42360
    55
    val args = map (TFree o Proof_Context.check_tfree lthy) raw_args;
wenzelm@36156
    56
    val T = Type (Local_Theory.full_name lthy b, args);
wenzelm@35681
    57
wenzelm@35681
    58
    val bad_args =
wenzelm@35681
    59
      #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
wenzelm@35681
    60
      |> filter_out Term.is_TVar;
wenzelm@36172
    61
    val _ = null bad_args orelse
wenzelm@35740
    62
      err ("Locally fixed type arguments " ^
wenzelm@35834
    63
        commas_quote (map (Syntax.string_of_typ lthy) bad_args));
wenzelm@36172
    64
  in T end;
wenzelm@36172
    65
wenzelm@36172
    66
wenzelm@36172
    67
(* type declarations *)
wenzelm@36172
    68
wenzelm@36172
    69
fun typedecl (b, raw_args, mx) lthy =
wenzelm@36172
    70
  let val T = global_type lthy (b, raw_args) in
wenzelm@35681
    71
    lthy
wenzelm@36172
    72
    |> basic_typedecl (b, length raw_args, mx)
wenzelm@35834
    73
    |> snd
wenzelm@35681
    74
    |> Variable.declare_typ T
wenzelm@35626
    75
    |> pair T
wenzelm@35626
    76
  end;
wenzelm@35626
    77
wenzelm@35681
    78
fun typedecl_global decl =
haftmann@38388
    79
  Named_Target.theory_init
wenzelm@35681
    80
  #> typedecl decl
wenzelm@35681
    81
  #> Local_Theory.exit_result_global Morphism.typ;
wenzelm@35681
    82
wenzelm@36172
    83
wenzelm@36172
    84
(* type abbreviations *)
wenzelm@36172
    85
wenzelm@36457
    86
local
wenzelm@36457
    87
wenzelm@36172
    88
fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy =
wenzelm@36172
    89
  let
wenzelm@36172
    90
    val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs);
wenzelm@36457
    91
    val rhs = prep_typ b lthy raw_rhs
wenzelm@42381
    92
      handle ERROR msg => cat_error msg ("in type abbreviation " ^ Binding.print b);
wenzelm@36172
    93
  in
wenzelm@36172
    94
    lthy
wenzelm@42375
    95
    |> basic_decl (fn _ => Sign.add_type_abbrev lthy (b, vs, rhs)) (b, length vs, mx)
wenzelm@36172
    96
    |> snd
wenzelm@36172
    97
    |> pair name
wenzelm@36172
    98
  end;
wenzelm@36172
    99
wenzelm@36457
   100
fun read_abbrev b ctxt raw_rhs =
wenzelm@36457
   101
  let
wenzelm@42360
   102
    val rhs = Proof_Context.read_typ_syntax (ctxt |> Proof_Context.set_defsort []) raw_rhs;
wenzelm@36457
   103
    val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
wenzelm@36457
   104
    val _ =
wenzelm@36457
   105
      if null ignored then ()
wenzelm@38831
   106
      else Context_Position.if_visible ctxt warning
wenzelm@38831
   107
        ("Ignoring sort constraints in type variables(s): " ^
wenzelm@38831
   108
          commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
wenzelm@42381
   109
          "\nin type abbreviation " ^ Binding.print b);
wenzelm@36457
   110
  in rhs end;
wenzelm@36457
   111
wenzelm@36457
   112
in
wenzelm@36457
   113
wenzelm@42360
   114
val abbrev = gen_abbrev (K Proof_Context.cert_typ_syntax);
wenzelm@36457
   115
val abbrev_cmd = gen_abbrev read_abbrev;
wenzelm@36457
   116
wenzelm@36457
   117
end;
wenzelm@36172
   118
wenzelm@36172
   119
fun abbrev_global decl rhs =
haftmann@38388
   120
  Named_Target.theory_init
wenzelm@36172
   121
  #> abbrev decl rhs
wenzelm@36172
   122
  #> Local_Theory.exit_result_global (K I);
wenzelm@36172
   123
wenzelm@35626
   124
end;
wenzelm@35626
   125