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