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;
     1 (*  Title:      Pure/Isar/typedecl.ML
     2     Author:     Makarius
     3 
     4 Type declarations (with object-logic arities) and type abbreviations.
     5 *)
     6 
     7 signature TYPEDECL =
     8 sig
     9   val read_constraint: Proof.context -> string option -> sort
    10   val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory
    11   val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
    12   val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory
    13   val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory
    14   val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory
    15   val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory
    16 end;
    17 
    18 structure Typedecl: TYPEDECL =
    19 struct
    20 
    21 (* constraints *)
    22 
    23 fun read_constraint _ NONE = dummyS
    24   | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
    25 
    26 
    27 (* primitives *)
    28 
    29 fun object_logic_arity name thy =
    30   (case Object_Logic.get_base_sort thy of
    31     NONE => thy
    32   | SOME S => AxClass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
    33 
    34 fun basic_decl decl (b, n, mx) lthy =
    35   let val name = Local_Theory.full_name lthy b in
    36     lthy
    37     |> Local_Theory.background_theory (decl name)
    38     |> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)]
    39     |> Local_Theory.type_alias b name
    40     |> pair name
    41   end;
    42 
    43 fun basic_typedecl (b, n, mx) lthy =
    44   basic_decl (fn name => Sign.add_types lthy [(b, n, NoSyn)] #> object_logic_arity name)
    45     (b, n, mx) lthy;
    46 
    47 
    48 (* global type -- without dependencies on type parameters of the context *)
    49 
    50 fun global_type lthy (b, raw_args) =
    51   let
    52     fun err msg = error (msg ^ " in type declaration " ^ Binding.print b);
    53 
    54     val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
    55     val args = map (TFree o Proof_Context.check_tfree lthy) raw_args;
    56     val T = Type (Local_Theory.full_name lthy b, args);
    57 
    58     val bad_args =
    59       #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
    60       |> filter_out Term.is_TVar;
    61     val _ = null bad_args orelse
    62       err ("Locally fixed type arguments " ^
    63         commas_quote (map (Syntax.string_of_typ lthy) bad_args));
    64   in T end;
    65 
    66 
    67 (* type declarations *)
    68 
    69 fun typedecl (b, raw_args, mx) lthy =
    70   let val T = global_type lthy (b, raw_args) in
    71     lthy
    72     |> basic_typedecl (b, length raw_args, mx)
    73     |> snd
    74     |> Variable.declare_typ T
    75     |> pair T
    76   end;
    77 
    78 fun typedecl_global decl =
    79   Named_Target.theory_init
    80   #> typedecl decl
    81   #> Local_Theory.exit_result_global Morphism.typ;
    82 
    83 
    84 (* type abbreviations *)
    85 
    86 local
    87 
    88 fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy =
    89   let
    90     val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs);
    91     val rhs = prep_typ b lthy raw_rhs
    92       handle ERROR msg => cat_error msg ("in type abbreviation " ^ Binding.print b);
    93   in
    94     lthy
    95     |> basic_decl (fn _ => Sign.add_type_abbrev lthy (b, vs, rhs)) (b, length vs, mx)
    96     |> snd
    97     |> pair name
    98   end;
    99 
   100 fun read_abbrev b ctxt raw_rhs =
   101   let
   102     val rhs = Proof_Context.read_typ_syntax (ctxt |> Proof_Context.set_defsort []) raw_rhs;
   103     val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
   104     val _ =
   105       if null ignored then ()
   106       else Context_Position.if_visible ctxt warning
   107         ("Ignoring sort constraints in type variables(s): " ^
   108           commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
   109           "\nin type abbreviation " ^ Binding.print b);
   110   in rhs end;
   111 
   112 in
   113 
   114 val abbrev = gen_abbrev (K Proof_Context.cert_typ_syntax);
   115 val abbrev_cmd = gen_abbrev read_abbrev;
   116 
   117 end;
   118 
   119 fun abbrev_global decl rhs =
   120   Named_Target.theory_init
   121   #> abbrev decl rhs
   122   #> Local_Theory.exit_result_global (K I);
   123 
   124 end;
   125