src/HOL/Tools/datatype_package.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 30025 52b93309fdeb
child 30201 39fefb3eedfc
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Tools/datatype_package.ML
11539
0f17da240450 tuned headers;
wenzelm
parents: 11345
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
     3
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
     4
Datatype package for Isabelle/HOL.
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
     5
*)
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
     6
27097
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
     7
signature DATATYPE_PACKAGE =
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
     8
sig
27097
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
     9
  val quiet_mode : bool ref
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    10
  val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    11
  val print_datatypes : theory -> unit
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    12
  val get_datatype : theory -> string -> DatatypeAux.datatype_info option
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    13
  val the_datatype : theory -> string -> DatatypeAux.datatype_info
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    14
  val datatype_of_constr : theory -> string -> DatatypeAux.datatype_info option
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    15
  val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    16
  val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    17
  val get_datatype_constrs : theory -> string -> (string * typ) list option
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    18
  val construction_interpretation : theory
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    19
    -> {atom : typ -> 'a, dtyp : string -> 'a, rtyp : string -> 'a list -> 'a}
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    20
    -> (string * sort) list -> string list
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    21
    -> (string * (string * 'a list) list) list
7015
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
    22
  val distinct_simproc : simproc
27097
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    23
  val make_case :  Proof.context -> bool -> string list -> term ->
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    24
    (term * term) list -> term * (term * (int * bool)) list
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    25
  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
27277
7b7ce2d7fafe export read_typ/cert_typ -- version with regular context operations;
wenzelm
parents: 27261
diff changeset
    26
  val read_typ: theory ->
7b7ce2d7fafe export read_typ/cert_typ -- version with regular context operations;
wenzelm
parents: 27261
diff changeset
    27
    (typ list * (string * sort) list) * string -> typ list * (string * sort) list
27097
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    28
  val interpretation : (string list -> theory -> theory) -> theory -> theory
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
    29
  val rep_datatype : ({distinct : thm list list,
6385
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
    30
       inject : thm list list,
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
    31
       exhaustion : thm list,
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
    32
       rec_thms : thm list,
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
    33
       case_thms : thm list list,
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
    34
       split_thms : (thm * thm) list,
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
    35
       induction : thm,
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
    36
       simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
    37
    -> theory -> Proof.state;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
    38
  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
    39
  val add_datatype : bool -> bool -> string list -> (string list * bstring * mixfix *
27097
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    40
    (bstring * typ list * mixfix) list) list -> theory ->
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    41
      {distinct : thm list list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    42
       inject : thm list list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    43
       exhaustion : thm list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    44
       rec_thms : thm list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    45
       case_thms : thm list list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    46
       split_thms : (thm * thm) list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    47
       induction : thm,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    48
       simps : thm list} * theory
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
    49
  val add_datatype_cmd : bool -> string list -> (string list * bstring * mixfix *
27097
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    50
    (bstring * string list * mixfix) list) list -> theory ->
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    51
      {distinct : thm list list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    52
       inject : thm list list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    53
       exhaustion : thm list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    54
       rec_thms : thm list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    55
       case_thms : thm list list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    56
       split_thms : (thm * thm) list,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    57
       induction : thm,
9a6db5d8ee8c signature cleanup -- no pervasives anymore;
wenzelm
parents: 27002
diff changeset
    58
       simps : thm list} * theory
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18702
diff changeset
    59
  val setup: theory -> theory
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    60
end;
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    61
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    62
structure DatatypePackage : DATATYPE_PACKAGE =
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    63
struct
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    64
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    65
open DatatypeAux;
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    66
5661
6ecb6ea25f19 - Changed structure of name spaces
berghofe
parents: 5578
diff changeset
    67
val quiet_mode = quiet_mode;
6ecb6ea25f19 - Changed structure of name spaces
berghofe
parents: 5578
diff changeset
    68
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
    69
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22777
diff changeset
    70
(* theory data *)
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    71
16430
bc07926e4f03 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    72
structure DatatypesData = TheoryDataFun
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22777
diff changeset
    73
(
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    74
  type T =
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    75
    {types: datatype_info Symtab.table,
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    76
     constrs: datatype_info Symtab.table,
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    77
     cases: datatype_info Symtab.table};
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    78
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    79
  val empty =
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    80
    {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
6556
daa00919502b theory data: copy;
wenzelm
parents: 6479
diff changeset
    81
  val copy = I;
16430
bc07926e4f03 accomodate change of TheoryDataFun;
wenzelm
parents: 16364
diff changeset
    82
  val extend = I;
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    83
  fun merge _
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    84
    ({types = types1, constrs = constrs1, cases = cases1},
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    85
     {types = types2, constrs = constrs2, cases = cases2}) =
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    86
    {types = Symtab.merge (K true) (types1, types2),
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    87
     constrs = Symtab.merge (K true) (constrs1, constrs2),
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    88
     cases = Symtab.merge (K true) (cases1, cases2)};
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22777
diff changeset
    89
);
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    90
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    91
val get_datatypes = #types o DatatypesData.get;
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
    92
val map_datatypes = DatatypesData.map;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22777
diff changeset
    93
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22777
diff changeset
    94
fun print_datatypes thy =
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22777
diff changeset
    95
  Pretty.writeln (Pretty.strs ("datatypes:" ::
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22777
diff changeset
    96
    map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy))));
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    97
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    98
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
    99
(** theory information about datatypes **)
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   100
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   101
fun put_dt_infos (dt_infos : (string * datatype_info) list) =
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   102
  map_datatypes (fn {types, constrs, cases} =>
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   103
    {types = fold Symtab.update dt_infos types,
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   104
     constrs = fold Symtab.update
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   105
       (maps (fn (_, info as {descr, index, ...}) => map (rpair info o fst)
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   106
          (#3 (the (AList.lookup op = descr index)))) dt_infos) constrs,
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   107
     cases = fold Symtab.update
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   108
       (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   109
       cases});
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   110
19346
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   111
val get_datatype = Symtab.lookup o get_datatypes;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   112
19346
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   113
fun the_datatype thy name = (case get_datatype thy name of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15457
diff changeset
   114
      SOME info => info
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15457
diff changeset
   115
    | NONE => error ("Unknown datatype " ^ quote name));
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   116
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   117
val datatype_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   118
val datatype_of_case = Symtab.lookup o #cases o DatatypesData.get;
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   119
19346
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   120
fun get_datatype_descr thy dtco =
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   121
  get_datatype thy dtco
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24699
diff changeset
   122
  |> Option.map (fn info as { descr, index, ... } =>
19346
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   123
       (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
7015
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   124
25537
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   125
fun the_datatype_spec thy dtco =
18518
3b1dfa53e64f adaptions to changes in code generator
haftmann
parents: 18462
diff changeset
   126
  let
26093
haftmann
parents: 25888
diff changeset
   127
    val info as { descr, index, sorts = raw_sorts, ... } = the_datatype thy dtco;
haftmann
parents: 25888
diff changeset
   128
    val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
haftmann
parents: 25888
diff changeset
   129
    val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
haftmann
parents: 25888
diff changeset
   130
      o DatatypeAux.dest_DtTFree) dtys;
haftmann
parents: 25888
diff changeset
   131
    val cos = map
haftmann
parents: 25888
diff changeset
   132
      (fn (co, tys) => (co, map (DatatypeAux.typ_of_dtyp descr sorts) tys)) raw_cos;
haftmann
parents: 25888
diff changeset
   133
  in (sorts, cos) end;
18518
3b1dfa53e64f adaptions to changes in code generator
haftmann
parents: 18462
diff changeset
   134
19346
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   135
fun get_datatype_constrs thy dtco =
25537
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   136
  case try (the_datatype_spec thy) dtco
19346
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   137
   of SOME (sorts, cos) =>
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   138
        let
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   139
          fun subst (v, sort) = TVar ((v, 0), sort);
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   140
          fun subst_ty (TFree v) = subst v
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   141
            | subst_ty ty = ty;
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   142
          val dty = Type (dtco, map subst sorts);
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   143
          fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty);
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   144
        in SOME (map mk_co cos) end
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   145
    | NONE => NONE;
18518
3b1dfa53e64f adaptions to changes in code generator
haftmann
parents: 18462
diff changeset
   146
26267
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   147
fun construction_interpretation thy { atom, dtyp, rtyp } sorts tycos =
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   148
  let
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   149
    val descr = (#descr o the_datatype thy o hd) tycos;
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   150
    val k = length tycos;
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   151
    val descr_of = the o AList.lookup (op =) descr;
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   152
    fun interpT (T as DtTFree _) = atom (typ_of_dtyp descr sorts T)
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   153
      | interpT (T as DtType (tyco, Ts)) = if is_rec_type T
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   154
          then rtyp tyco (map interpT Ts)
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   155
          else atom (typ_of_dtyp descr sorts T)
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   156
      | interpT (DtRec l) = if l < k then (dtyp o #1 o descr_of) l
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   157
          else let val (tyco, Ts, _) = descr_of l
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   158
          in rtyp tyco (map interpT Ts) end;
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   159
    fun interpC (c, Ts) = (c, map interpT Ts);
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   160
    fun interpK (_, (tyco, _, cs)) = (tyco, map interpC cs);
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   161
  in map interpK (Library.take (k, descr)) end;
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26111
diff changeset
   162
8541
b0d2002f9f04 proof methods: 'case_tac' / 'induct_tac';
wenzelm
parents: 8478
diff changeset
   163
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   164
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   165
(** induct method setup **)
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   166
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   167
(* case names *)
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   168
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   169
local
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   170
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   171
fun dt_recs (DtTFree _) = []
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   172
  | dt_recs (DtType (_, dts)) = maps dt_recs dts
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   173
  | dt_recs (DtRec i) = [i];
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   174
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   175
fun dt_cases (descr: descr) (_, args, constrs) =
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   176
  let
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   177
    fun the_bname i = Sign.base_name (#1 (the (AList.lookup (op =) descr i)));
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   178
    val bnames = map the_bname (distinct (op =) (maps dt_recs args));
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   179
  in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   180
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   181
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   182
fun induct_cases descr =
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   183
  DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   184
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   185
fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   186
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   187
in
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   188
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   189
fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   190
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   191
fun mk_case_names_exhausts descr new =
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   192
  map (RuleCases.case_names o exhaust_cases descr o #1)
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   193
    (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   194
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   195
end;
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   196
24699
c6674504103f datatype interpretators for size and datatype_realizer
haftmann
parents: 24626
diff changeset
   197
fun add_rules simps case_thms rec_thms inject distinct
11345
cd605c85e421 improved iff_add_global, new function add_rules factoring out common behaviour
oheimb
parents: 10930
diff changeset
   198
                  weak_case_congs cong_att =
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   199
  PureThy.add_thmss [((Binding.name "simps", simps), []),
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   200
    ((Binding.empty, flat case_thms @
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   201
          flat distinct @ rec_thms), [Simplifier.simp_add]),
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   202
    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   203
    ((Binding.empty, flat inject), [iff_add]),
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   204
    ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   205
    ((Binding.empty, weak_case_congs), [cong_att])]
21127
c8e862897d13 cleaned up
haftmann
parents: 21045
diff changeset
   206
  #> snd;
11345
cd605c85e421 improved iff_add_global, new function add_rules factoring out common behaviour
oheimb
parents: 10930
diff changeset
   207
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   208
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   209
(* add_cases_induct *)
8306
9855f1801d2b HOLogic.dest_conj;
wenzelm
parents: 8279
diff changeset
   210
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 19841
diff changeset
   211
fun add_cases_induct infos induction thy =
8306
9855f1801d2b HOLogic.dest_conj;
wenzelm
parents: 8279
diff changeset
   212
  let
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 19841
diff changeset
   213
    val inducts = ProjectRule.projections (ProofContext.init thy) induction;
8405
0255394a05da add_cases_induct: produce proper case names;
wenzelm
parents: 8325
diff changeset
   214
11805
b110a1ea90da declare projected induction rules stemming from nested recursion;
wenzelm
parents: 11725
diff changeset
   215
    fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   216
      [((Binding.empty, nth inducts index), [Induct.induct_type name]),
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   217
       ((Binding.empty, exhaustion), [Induct.cases_type name])];
11805
b110a1ea90da declare projected induction rules stemming from nested recursion;
wenzelm
parents: 11725
diff changeset
   218
    fun unnamed_rule i =
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   219
      ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
18462
b67d423b5234 *.inducts holds all projected rules;
wenzelm
parents: 18455
diff changeset
   220
  in
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 19841
diff changeset
   221
    thy |> PureThy.add_thms
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   222
      (maps named_rules infos @
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 19841
diff changeset
   223
        map unnamed_rule (length infos upto length inducts - 1)) |> snd
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   224
    |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
18462
b67d423b5234 *.inducts holds all projected rules;
wenzelm
parents: 18455
diff changeset
   225
  end;
8306
9855f1801d2b HOLogic.dest_conj;
wenzelm
parents: 8279
diff changeset
   226
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   227
8405
0255394a05da add_cases_induct: produce proper case names;
wenzelm
parents: 8325
diff changeset
   228
7015
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   229
(**** simplification procedure for showing distinctness of constructors ****)
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   230
7060
berghofe
parents: 7049
diff changeset
   231
fun stripT (i, Type ("fun", [_, T])) = stripT (i + 1, T)
berghofe
parents: 7049
diff changeset
   232
  | stripT p = p;
berghofe
parents: 7049
diff changeset
   233
berghofe
parents: 7049
diff changeset
   234
fun stripC (i, f $ x) = stripC (i + 1, f)
berghofe
parents: 7049
diff changeset
   235
  | stripC p = p;
berghofe
parents: 7049
diff changeset
   236
7015
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   237
val distinctN = "constr_distinct";
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   238
25537
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   239
fun distinct_rule thy ss tname eq_t = case #distinct (the_datatype thy tname) of
26533
aeef55a3d1d5 Deleted code for axiomatic introduction of datatypes. Instead, the package
berghofe
parents: 26496
diff changeset
   240
    FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
25537
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   241
      (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   242
        atac 2, resolve_tac thms 1, etac FalseE 1]))
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   243
  | ManyConstrs (thm, simpset) =>
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   244
      let
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   245
        val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
26343
0dd2eab7b296 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26336
diff changeset
   246
          map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy))
25537
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   247
            ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   248
      in
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   249
        Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   250
        (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   251
          full_simp_tac (Simplifier.inherit_context ss simpset) 1,
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   252
          REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   253
          eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   254
          etac FalseE 1]))
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   255
      end;
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   256
19539
5b37bb0ad964 ThyInfo.the_theory;
wenzelm
parents: 19346
diff changeset
   257
fun distinct_proc thy ss (t as Const ("op =", _) $ t1 $ t2) =
7060
berghofe
parents: 7049
diff changeset
   258
  (case (stripC (0, t1), stripC (0, t2)) of
berghofe
parents: 7049
diff changeset
   259
     ((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
berghofe
parents: 7049
diff changeset
   260
         (case (stripT (0, T1), stripT (0, T2)) of
berghofe
parents: 7049
diff changeset
   261
            ((i', Type (tname1, _)), (j', Type (tname2, _))) =>
berghofe
parents: 7049
diff changeset
   262
                if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
19539
5b37bb0ad964 ThyInfo.the_theory;
wenzelm
parents: 19346
diff changeset
   263
                   (case (get_datatype_descr thy) tname1 of
19346
c4c003abd830 cleanup in datatype package
haftmann
parents: 19046
diff changeset
   264
                      SOME (_, (_, constrs)) => let val cnames = map fst constrs
7015
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   265
                        in if cname1 mem cnames andalso cname2 mem cnames then
25537
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   266
                             SOME (distinct_rule thy ss tname1
55017c8b0a24 interface and distinct simproc tuned
haftmann
parents: 25495
diff changeset
   267
                               (Logic.mk_equals (t, Const ("False", HOLogic.boolT))))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15457
diff changeset
   268
                           else NONE
7015
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   269
                        end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15457
diff changeset
   270
                    | NONE => NONE)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15457
diff changeset
   271
                else NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15457
diff changeset
   272
          | _ => NONE)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15457
diff changeset
   273
   | _ => NONE)
20054
24d176b8f240 distinct simproc/simpset: proper context;
wenzelm
parents: 19925
diff changeset
   274
  | distinct_proc _ _ _ = NONE;
7015
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   275
13462
56610e2ba220 sane interface for simprocs;
wenzelm
parents: 13340
diff changeset
   276
val distinct_simproc =
29064
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
   277
  Simplifier.simproc @{theory HOL} distinctN ["s = t"] distinct_proc;
7015
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   278
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   279
val dist_ss = HOL_ss addsimprocs [distinct_simproc];
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   280
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   281
val simproc_setup =
26496
49ae9456eba9 purely functional setup of claset/simpset/clasimpset;
wenzelm
parents: 26343
diff changeset
   282
  Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
7015
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   283
85be09eb136c - Datatype package now also supports arbitrarily branching datatypes
berghofe
parents: 6851
diff changeset
   284
14799
a405aadff16c Added more flexible parse / print translations for case expressions.
berghofe
parents: 14471
diff changeset
   285
(**** translation rules for case ****)
a405aadff16c Added more flexible parse / print translations for case expressions.
berghofe
parents: 14471
diff changeset
   286
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   287
fun make_case ctxt = DatatypeCase.make_case
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   288
  (datatype_of_constr (ProofContext.theory_of ctxt)) ctxt;
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   289
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   290
fun strip_case ctxt = DatatypeCase.strip_case
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   291
  (datatype_of_case (ProofContext.theory_of ctxt));
14799
a405aadff16c Added more flexible parse / print translations for case expressions.
berghofe
parents: 14471
diff changeset
   292
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   293
fun add_case_tr' case_names thy =
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
   294
  Sign.add_advanced_trfuns ([], [],
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24699
diff changeset
   295
    map (fn case_name =>
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   296
      let val case_name' = Sign.const_syntax_name thy case_name
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   297
      in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   298
      end) case_names, []) thy;
14799
a405aadff16c Added more flexible parse / print translations for case expressions.
berghofe
parents: 14471
diff changeset
   299
a405aadff16c Added more flexible parse / print translations for case expressions.
berghofe
parents: 14471
diff changeset
   300
val trfun_setup =
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
   301
  Sign.add_advanced_trfuns ([],
24349
0dd8782fb02d Final mods for list comprehension
nipkow
parents: 24346
diff changeset
   302
    [("_case_syntax", DatatypeCase.case_tr true datatype_of_constr)],
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   303
    [], []);
14799
a405aadff16c Added more flexible parse / print translations for case expressions.
berghofe
parents: 14471
diff changeset
   304
a405aadff16c Added more flexible parse / print translations for case expressions.
berghofe
parents: 14471
diff changeset
   305
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   306
(* prepare types *)
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   307
27277
7b7ce2d7fafe export read_typ/cert_typ -- version with regular context operations;
wenzelm
parents: 27261
diff changeset
   308
fun read_typ thy ((Ts, sorts), str) =
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   309
  let
27277
7b7ce2d7fafe export read_typ/cert_typ -- version with regular context operations;
wenzelm
parents: 27261
diff changeset
   310
    val ctxt = ProofContext.init thy
7b7ce2d7fafe export read_typ/cert_typ -- version with regular context operations;
wenzelm
parents: 27261
diff changeset
   311
      |> fold (Variable.declare_typ o TFree) sorts;
7b7ce2d7fafe export read_typ/cert_typ -- version with regular context operations;
wenzelm
parents: 27261
diff changeset
   312
    val T = Syntax.read_typ ctxt str;
7b7ce2d7fafe export read_typ/cert_typ -- version with regular context operations;
wenzelm
parents: 27261
diff changeset
   313
  in (Ts @ [T], Term.add_tfreesT T sorts) end;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   314
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   315
fun cert_typ sign ((Ts, sorts), raw_T) =
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   316
  let
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   317
    val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   318
      TYPE (msg, _, _) => error msg;
27277
7b7ce2d7fafe export read_typ/cert_typ -- version with regular context operations;
wenzelm
parents: 27261
diff changeset
   319
    val sorts' = Term.add_tfreesT T sorts;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   320
  in (Ts @ [T],
18964
67f572e03236 renamed gen_duplicates to duplicates;
wenzelm
parents: 18963
diff changeset
   321
      case duplicates (op =) (map fst sorts') of
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   322
         [] => sorts'
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   323
       | dups => error ("Inconsistent sort constraints for " ^ commas dups))
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   324
  end;
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   325
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   326
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   327
(**** make datatype info ****)
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   328
25677
8b2ddc6e7be1 - Removed redundant head_len field in datatype_info
berghofe
parents: 25537
diff changeset
   329
fun make_dt_info alt_names descr sorts induct reccomb_names rec_thms
10121
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   330
    (((((((((i, (_, (tname, _, _))), case_name), case_thms),
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   331
      exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) =
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   332
  (tname,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   333
   {index = i,
25677
8b2ddc6e7be1 - Removed redundant head_len field in datatype_info
berghofe
parents: 25537
diff changeset
   334
    alt_names = alt_names,
10121
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   335
    descr = descr,
18319
c52b139ebde0 Added new component "sorts" to record datatype_info.
berghofe
parents: 18314
diff changeset
   336
    sorts = sorts,
10121
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   337
    rec_names = reccomb_names,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   338
    rec_rewrites = rec_thms,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   339
    case_name = case_name,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   340
    case_rewrites = case_thms,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   341
    induction = induct,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   342
    exhaustion = exhaustion_thm,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   343
    distinct = distinct_thm,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   344
    inject = inject,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   345
    nchotomy = nchotomy,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   346
    case_cong = case_cong,
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   347
    weak_case_cong = weak_case_cong});
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   348
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24699
diff changeset
   349
structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24699
diff changeset
   350
val interpretation = DatatypeInterpretation.interpretation;
24626
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24624
diff changeset
   351
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   352
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   353
(******************* definitional introduction of datatypes *******************)
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   354
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   355
fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   356
    case_names_induct case_names_exhausts thy =
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   357
  let
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   358
    val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   359
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   360
    val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
5661
6ecb6ea25f19 - Changed structure of name spaces
berghofe
parents: 5578
diff changeset
   361
      DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   362
        types_syntax constr_syntax case_names_induct;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   363
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   364
    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   365
      sorts induct case_names_exhausts thy2;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   366
    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
20054
24d176b8f240 distinct simproc/simpset: proper context;
wenzelm
parents: 19925
diff changeset
   367
      flat_names new_type_names descr sorts dt_info inject dist_rewrites
24d176b8f240 distinct simproc/simpset: proper context;
wenzelm
parents: 19925
diff changeset
   368
      (Simplifier.theory_context thy3 dist_ss) induct thy3;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   369
    val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
5661
6ecb6ea25f19 - Changed structure of name spaces
berghofe
parents: 5578
diff changeset
   370
      flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   371
    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   372
      descr sorts inject dist_rewrites casedist_thms case_thms thy6;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   373
    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   374
      descr sorts casedist_thms thy7;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   375
    val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   376
      descr sorts nchotomys case_thms thy8;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   377
    val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
8601
8fb3a81b4ccf added weak_case_cong feature
nipkow
parents: 8541
diff changeset
   378
      descr sorts thy9;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   379
25677
8b2ddc6e7be1 - Removed redundant head_len field in datatype_info
berghofe
parents: 25537
diff changeset
   380
    val dt_infos = map (make_dt_info NONE (flat descr) sorts induct reccomb_names rec_thms)
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   381
      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
10121
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   382
        casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   383
24699
c6674504103f datatype interpretators for size and datatype_realizer
haftmann
parents: 24626
diff changeset
   384
    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   385
18518
3b1dfa53e64f adaptions to changes in code generator
haftmann
parents: 18462
diff changeset
   386
    val thy12 =
24699
c6674504103f datatype interpretators for size and datatype_realizer
haftmann
parents: 24626
diff changeset
   387
      thy10
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   388
      |> add_case_tr' case_names
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
   389
      |> Sign.add_path (space_implode "_" new_type_names)
24699
c6674504103f datatype interpretators for size and datatype_realizer
haftmann
parents: 24626
diff changeset
   390
      |> add_rules simps case_thms rec_thms inject distinct
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   391
          weak_case_congs (Simplifier.attrib (op addcongs))
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   392
      |> put_dt_infos dt_infos
18518
3b1dfa53e64f adaptions to changes in code generator
haftmann
parents: 18462
diff changeset
   393
      |> add_cases_induct dt_infos induct
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
   394
      |> Sign.parent_path
18518
3b1dfa53e64f adaptions to changes in code generator
haftmann
parents: 18462
diff changeset
   395
      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24699
diff changeset
   396
      |> DatatypeInterpretation.data (map fst dt_infos);
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   397
  in
18008
f193815cab2c swapped add_datatype result
haftmann
parents: 17956
diff changeset
   398
    ({distinct = distinct,
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   399
      inject = inject,
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   400
      exhaustion = casedist_thms,
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   401
      rec_thms = rec_thms,
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   402
      case_thms = case_thms,
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   403
      split_thms = split_thms,
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   404
      induction = induct,
18008
f193815cab2c swapped add_datatype result
haftmann
parents: 17956
diff changeset
   405
      simps = simps}, thy12)
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   406
  end;
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   407
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   408
6385
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
   409
(*********************** declare existing type as datatype *********************)
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   410
27300
4cb3101d2bf7 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents: 27277
diff changeset
   411
fun prove_rep_datatype alt_names new_type_names descr sorts induct inject half_distinct thy =
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   412
  let
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   413
    val ((_, [induct']), _) =
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   414
      Variable.importT_thms [induct] (Variable.thm_context induct);
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   415
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   416
    fun err t = error ("Ill-formed predicate in induction rule: " ^
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   417
      Syntax.string_of_term_global thy t);
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   418
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   419
    fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
25888
48cc198b9ac5 Eliminated DatatypeAux.dest_TFree to avoid clashes
berghofe
parents: 25677
diff changeset
   420
          ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   421
      | get_typ t = err t;
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   422
    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   423
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   424
    val dt_info = get_datatypes thy;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   425
27300
4cb3101d2bf7 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents: 27277
diff changeset
   426
    val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
21419
809e7520234a added instance for class size
haftmann
parents: 21350
diff changeset
   427
    val (case_names_induct, case_names_exhausts) =
809e7520234a added instance for class size
haftmann
parents: 21350
diff changeset
   428
      (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   429
6427
fd36b2e7d80e tuned messages;
wenzelm
parents: 6423
diff changeset
   430
    val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   431
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   432
    val (casedist_thms, thy2) = thy |>
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   433
      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   434
        case_names_exhausts;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   435
    val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
20054
24d176b8f240 distinct simproc/simpset: proper context;
wenzelm
parents: 19925
diff changeset
   436
      false new_type_names [descr] sorts dt_info inject distinct
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   437
      (Simplifier.theory_context thy2 dist_ss) induct thy2;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   438
    val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   439
      new_type_names [descr] sorts reccomb_names rec_thms thy3;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   440
    val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   441
      new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   442
    val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   443
      [descr] sorts casedist_thms thy5;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   444
    val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   445
      [descr] sorts nchotomys case_thms thy6;
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   446
    val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
8601
8fb3a81b4ccf added weak_case_cong feature
nipkow
parents: 8541
diff changeset
   447
      [descr] sorts thy7;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   448
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   449
    val ((_, [induct']), thy10) =
24699
c6674504103f datatype interpretators for size and datatype_realizer
haftmann
parents: 24626
diff changeset
   450
      thy8
18377
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18319
diff changeset
   451
      |> store_thmss "inject" new_type_names inject
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18319
diff changeset
   452
      ||>> store_thmss "distinct" new_type_names distinct
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
   453
      ||> Sign.add_path (space_implode "_" new_type_names)
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29270
diff changeset
   454
      ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
9149
a126a40cba76 export proper induction rule;
wenzelm
parents: 8697
diff changeset
   455
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   456
    val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms)
10121
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   457
      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
fb9be005cc44 export get_datatypes_sg;
wenzelm
parents: 9747
diff changeset
   458
        map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   459
24699
c6674504103f datatype interpretators for size and datatype_realizer
haftmann
parents: 24626
diff changeset
   460
    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   461
19599
a5c7eb37d14f added DatatypeHooks
haftmann
parents: 19539
diff changeset
   462
    val thy11 =
a5c7eb37d14f added DatatypeHooks
haftmann
parents: 19539
diff changeset
   463
      thy10
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   464
      |> add_case_tr' case_names
24699
c6674504103f datatype interpretators for size and datatype_realizer
haftmann
parents: 24626
diff changeset
   465
      |> add_rules simps case_thms rec_thms inject distinct
19599
a5c7eb37d14f added DatatypeHooks
haftmann
parents: 19539
diff changeset
   466
           weak_case_congs (Simplifier.attrib (op addcongs))
22777
2fc921376a86 - Moved parse / print translations for case to datatype_case.ML
berghofe
parents: 22709
diff changeset
   467
      |> put_dt_infos dt_infos
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   468
      |> add_cases_induct dt_infos induct'
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
   469
      |> Sign.parent_path
19599
a5c7eb37d14f added DatatypeHooks
haftmann
parents: 19539
diff changeset
   470
      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
a5c7eb37d14f added DatatypeHooks
haftmann
parents: 19539
diff changeset
   471
      |> snd
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24699
diff changeset
   472
      |> DatatypeInterpretation.data (map fst dt_infos);
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   473
  in
18008
f193815cab2c swapped add_datatype result
haftmann
parents: 17956
diff changeset
   474
    ({distinct = distinct,
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   475
      inject = inject,
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   476
      exhaustion = casedist_thms,
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   477
      rec_thms = rec_thms,
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   478
      case_thms = case_thms,
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   479
      split_thms = split_thms,
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   480
      induction = induct',
18008
f193815cab2c swapped add_datatype result
haftmann
parents: 17956
diff changeset
   481
      simps = simps}, thy11)
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   482
  end;
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   483
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   484
fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy =
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   485
  let
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   486
    fun constr_of_term (Const (c, T)) = (c, T)
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   487
      | constr_of_term t =
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   488
          error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   489
    fun no_constr (c, T) = error ("Bad constructor: "
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   490
      ^ Sign.extern_const thy c ^ "::"
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   491
      ^ Syntax.string_of_typ_global thy T);
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   492
    fun type_of_constr (cT as (_, T)) =
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   493
      let
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29064
diff changeset
   494
        val frees = OldTerm.typ_tfrees T;
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   495
        val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   496
          handle TYPE _ => no_constr cT
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   497
        val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   498
        val _ = if length frees <> length vs then no_constr cT else ();
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   499
      in (tyco, (vs, cT)) end;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   500
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   501
    val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   502
    val _ = case map_filter (fn (tyco, _) =>
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   503
        if Symtab.defined (get_datatypes thy) tyco then SOME tyco else NONE) raw_cs
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   504
     of [] => ()
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   505
      | tycos => error ("Type(s) " ^ commas (map quote tycos)
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   506
          ^ " already represented inductivly");
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   507
    val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   508
    val ms = case distinct (op =) (map length raw_vss)
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   509
     of [n] => 0 upto n - 1
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   510
      | _ => error ("Different types in given constructors");
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   511
    fun inter_sort m = map (fn xs => nth xs m) raw_vss
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   512
      |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   513
    val sorts = map inter_sort ms;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   514
    val vs = Name.names Name.context Name.aT sorts;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   515
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   516
    fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   517
      (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   518
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   519
    val cs = map (apsnd (map norm_constr)) raw_cs;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   520
    val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   521
      o fst o strip_type;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   522
    val new_type_names = map NameSpace.base (the_default (map fst cs) alt_names);
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   523
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   524
    fun mk_spec (i, (tyco, constr)) = (i, (tyco,
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   525
      map (DtTFree o fst) vs,
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   526
      (map o apsnd) dtyps_of_typ constr))
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   527
    val descr = map_index mk_spec cs;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   528
    val injs = DatatypeProp.make_injs [descr] vs;
27300
4cb3101d2bf7 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents: 27277
diff changeset
   529
    val half_distincts = map snd (DatatypeProp.make_distincts [descr] vs);
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   530
    val ind = DatatypeProp.make_ind [descr] vs;
27300
4cb3101d2bf7 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents: 27277
diff changeset
   531
    val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   532
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   533
    fun after_qed' raw_thms =
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   534
      let
27300
4cb3101d2bf7 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents: 27277
diff changeset
   535
        val [[[induct]], injs, half_distincts] =
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   536
          unflat rules (map Drule.zero_var_indexes_list raw_thms);
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   537
            (*FIXME somehow dubious*)
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   538
      in
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   539
        ProofContext.theory_result
27300
4cb3101d2bf7 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents: 27277
diff changeset
   540
          (prove_rep_datatype alt_names new_type_names descr vs induct injs half_distincts)
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   541
        #-> after_qed
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   542
      end;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   543
  in
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   544
    thy
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   545
    |> ProofContext.init
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   546
    |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   547
  end;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   548
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   549
val rep_datatype = gen_rep_datatype Sign.cert_term;
27261
5b3101338f42 eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents: 27130
diff changeset
   550
val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global (K I);
6385
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
   551
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   552
11958
2ece34b9fd8e Isar: fixed rep_datatype args;
wenzelm
parents: 11805
diff changeset
   553
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   554
(******************************** add datatype ********************************)
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   555
14887
4938ce4ef295 Added exception Datatype_Empty.
berghofe
parents: 14799
diff changeset
   556
fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   557
  let
20820
58693343905f removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents: 20715
diff changeset
   558
    val _ = Theory.requires thy "Datatype" "datatype definitions";
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   559
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   560
    (* this theory is used just for parsing *)
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   561
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   562
    val tmp_thy = thy |>
5892
e5e44cc54eb2 Attribute.tthms_of;
wenzelm
parents: 5720
diff changeset
   563
      Theory.copy |>
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
   564
      Sign.add_types (map (fn (tvs, tname, mx, _) =>
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   565
        (tname, length tvs, mx)) dts);
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   566
5661
6ecb6ea25f19 - Changed structure of name spaces
berghofe
parents: 5578
diff changeset
   567
    val (tyvars, _, _, _)::_ = dts;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   568
    val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28703
diff changeset
   569
      let val full_tname = Sign.full_bname tmp_thy (Syntax.type_name tname mx)
18964
67f572e03236 renamed gen_duplicates to duplicates;
wenzelm
parents: 18963
diff changeset
   570
      in (case duplicates (op =) tvs of
5661
6ecb6ea25f19 - Changed structure of name spaces
berghofe
parents: 5578
diff changeset
   571
            [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
6ecb6ea25f19 - Changed structure of name spaces
berghofe
parents: 5578
diff changeset
   572
                  else error ("Mutually recursive datatypes must have same type parameters")
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   573
          | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   574
              " : " ^ commas dups))
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   575
      end) dts);
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   576
18964
67f572e03236 renamed gen_duplicates to duplicates;
wenzelm
parents: 18963
diff changeset
   577
    val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   578
      [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   579
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   580
    fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   581
      let
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   582
        fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
5279
cba6a96f5812 Improved well-formedness check.
berghofe
parents: 5177
diff changeset
   583
          let
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20328
diff changeset
   584
            val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29064
diff changeset
   585
            val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
5279
cba6a96f5812 Improved well-formedness check.
berghofe
parents: 5177
diff changeset
   586
                [] => ()
cba6a96f5812 Improved well-formedness check.
berghofe
parents: 5177
diff changeset
   587
              | vs => error ("Extra type variables on rhs: " ^ commas vs))
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28703
diff changeset
   588
          in (constrs @ [((if flat_names then Sign.full_bname tmp_thy else
1de908189869 cleaned up binding module and related code
haftmann
parents: 28703
diff changeset
   589
                Sign.full_bname_path tmp_thy tname) (Syntax.const_name cname mx'),
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   590
                   map (dtyp_of_typ new_dts) cargs')],
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   591
              constr_syntax' @ [(cname, mx')], sorts'')
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18643
diff changeset
   592
          end handle ERROR msg =>
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18643
diff changeset
   593
            cat_error msg ("The error above occured in constructor " ^ cname ^
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   594
              " of datatype " ^ tname);
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   595
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   596
        val (constrs', constr_syntax', sorts') =
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   597
          fold prep_constr constrs ([], [], sorts)
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   598
8405
0255394a05da add_cases_induct: produce proper case names;
wenzelm
parents: 8325
diff changeset
   599
      in
18964
67f572e03236 renamed gen_duplicates to duplicates;
wenzelm
parents: 18963
diff changeset
   600
        case duplicates (op =) (map fst constrs') of
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   601
           [] =>
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28703
diff changeset
   602
             (dts' @ [(i, (Sign.full_bname tmp_thy (Syntax.type_name tname mx),
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   603
                map DtTFree tvs, constrs'))],
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   604
              constr_syntax @ [constr_syntax'], sorts', i + 1)
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   605
         | dups => error ("Duplicate constructors " ^ commas dups ^
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   606
             " in datatype " ^ tname)
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   607
      end;
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   608
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   609
    val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20328
diff changeset
   610
    val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   611
    val dt_info = get_datatypes thy;
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20328
diff changeset
   612
    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
14887
4938ce4ef295 Added exception Datatype_Empty.
berghofe
parents: 14799
diff changeset
   613
    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
15661
9ef583b08647 reverted renaming of Some/None in comments and strings;
wenzelm
parents: 15574
diff changeset
   614
      if err then error ("Nonemptiness check failed for datatype " ^ s)
14887
4938ce4ef295 Added exception Datatype_Empty.
berghofe
parents: 14799
diff changeset
   615
      else raise exn;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   616
21045
66d6d1b0ddfa slight cleanup
haftmann
parents: 20820
diff changeset
   617
    val descr' = flat descr;
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   618
    val case_names_induct = mk_case_names_induct descr';
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   619
    val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   620
  in
26533
aeef55a3d1d5 Deleted code for axiomatic introduction of datatypes. Instead, the package
berghofe
parents: 26496
diff changeset
   621
    add_datatype_def
8437
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   622
      flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
258281c43dea removed cases_of;
wenzelm
parents: 8405
diff changeset
   623
      case_names_induct case_names_exhausts thy
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   624
  end;
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   625
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   626
val add_datatype = gen_add_datatype cert_typ;
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   627
val add_datatype_cmd = gen_add_datatype read_typ true;
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   628
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   629
26111
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   630
(** a datatype antiquotation **)
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   631
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   632
local
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   633
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   634
val sym_datatype = Pretty.str "\\isacommand{datatype}";
29898
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   635
val sym_binder = Pretty.str "\\ {\\isacharequal}";
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   636
val sym_sep = Pretty.str "{\\isacharbar}\\ ";
26111
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   637
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   638
in
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   639
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   640
fun args_datatype (ctxt, args) =
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   641
  let
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   642
    val (tyco, (ctxt', args')) = Args.tyname (ctxt, args);
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   643
    val thy = Context.theory_of ctxt';
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   644
    val spec = the_datatype_spec thy tyco;
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   645
  in ((tyco, spec), (ctxt', args')) end;
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   646
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   647
fun pretty_datatype ctxt (dtco, (vs, cos)) =
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   648
  let
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   649
    val ty = Type (dtco, map TFree vs);
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   650
    fun pretty_typ_br ty =
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   651
      let
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   652
        val p = Syntax.pretty_typ ctxt ty;
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   653
        val s = explode (Pretty.str_of p);
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   654
      in if member (op =) s " " then Pretty.enclose "(" ")" [p]
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   655
        else p
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   656
      end;
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   657
    fun pretty_constr (co, []) =
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   658
          Syntax.pretty_term ctxt (Const (co, ty))
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   659
      | pretty_constr (co, [ty']) =
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   660
          (Pretty.block o Pretty.breaks)
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   661
            [Syntax.pretty_term ctxt (Const (co, ty' --> ty)),
30025
52b93309fdeb datatype antiquotation: always bracket types with spaces in between
haftmann
parents: 29898
diff changeset
   662
              pretty_typ_br ty']
26111
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   663
      | pretty_constr (co, tys) =
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   664
          (Pretty.block o Pretty.breaks)
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   665
            (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
29898
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   666
              map pretty_typ_br tys);
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   667
  in
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   668
    Pretty.block
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   669
      (sym_datatype :: Pretty.brk 1 ::
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   670
       Syntax.pretty_typ ctxt ty ::
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   671
       sym_binder :: Pretty.brk 1 ::
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   672
       flat (separate [Pretty.brk 1, sym_sep]
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   673
         (map (single o pretty_constr) cos)))
62390f5d0826 Tuned datatype antiquotation.
berghofe
parents: 29579
diff changeset
   674
  end
26111
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   675
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   676
end;
18451
5ff0244e25e8 slight clean ups
haftmann
parents: 18418
diff changeset
   677
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   678
(** package setup **)
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   679
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   680
(* setup theory *)
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   681
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18702
diff changeset
   682
val setup =
27002
215d64dc971e moved distinctness_limit to datatype_rep_proofs.ML
haftmann
parents: 26939
diff changeset
   683
  DatatypeRepProofs.distinctness_limit_setup #>
24098
f1eb34ae33af replaced dtK ref by datatype_distinctness_limit configuration option;
wenzelm
parents: 22994
diff changeset
   684
  simproc_setup #>
24626
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24624
diff changeset
   685
  trfun_setup #>
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24699
diff changeset
   686
  DatatypeInterpretation.init;
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   687
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   688
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   689
(* outer syntax *)
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   690
17057
0934ac31985f OuterKeyword;
wenzelm
parents: 16973
diff changeset
   691
local structure P = OuterParse and K = OuterKeyword in
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   692
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   693
val datatype_decl =
6723
f342449d73ca outer syntax keyword classification;
wenzelm
parents: 6556
diff changeset
   694
  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
12876
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12708
diff changeset
   695
    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   696
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   697
fun mk_datatype args =
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   698
  let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15457
diff changeset
   699
    val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
12876
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12708
diff changeset
   700
    val specs = map (fn ((((_, vs), t), mx), cons) =>
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12708
diff changeset
   701
      (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   702
  in snd o add_datatype_cmd false names specs end;
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   703
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   704
val _ =
6723
f342449d73ca outer syntax keyword classification;
wenzelm
parents: 6556
diff changeset
   705
  OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
f342449d73ca outer syntax keyword classification;
wenzelm
parents: 6556
diff changeset
   706
    (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
6360
83573ae0f22c outer syntax for 'datatype';
wenzelm
parents: 6305
diff changeset
   707
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   708
val _ =
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   709
  OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   710
    (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   711
      >> (fn (alt_names, ts) => Toplevel.print
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 27097
diff changeset
   712
           o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
6385
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
   713
26111
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   714
val _ =
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   715
  ThyOutput.add_commands [("datatype",
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   716
    ThyOutput.args args_datatype (ThyOutput.output pretty_datatype))];
91e0999b075f added first version of datatype antiquotation
haftmann
parents: 26093
diff changeset
   717
6385
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
   718
end;
5a6570458d9e rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents: 6360
diff changeset
   719
5177
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   720
end;
0d3a168e4d44 New datatype definition package
berghofe
parents:
diff changeset
   721