src/HOL/Tools/Datatype/datatype.ML
changeset 33959 2afc55e8ed27
parent 33957 e9afca2118d4
child 33963 977b94b64905
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed Nov 25 09:14:28 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Nov 25 11:16:57 2009 +0100
     1.3 @@ -7,10 +7,9 @@
     1.4  signature DATATYPE =
     1.5  sig
     1.6    include DATATYPE_COMMON
     1.7 -  val add_datatype : config -> string list -> (string list * binding * mixfix *
     1.8 -    (binding * typ list * mixfix) list) list -> theory -> string list * theory
     1.9 -  val datatype_cmd : string list -> (string list * binding * mixfix *
    1.10 -    (binding * string list * mixfix) list) list -> theory -> theory
    1.11 +  val derive_datatype_props : config -> string list -> string list option
    1.12 +    -> descr list -> (string * sort) list -> thm -> thm list list -> thm list list
    1.13 +    -> theory -> string list * theory
    1.14    val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
    1.15      -> string list option -> term list -> theory -> Proof.state
    1.16    val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
    1.17 @@ -30,6 +29,8 @@
    1.18      (term * term) list -> term * (term * (int * bool)) list
    1.19    val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    1.20    val read_typ: theory -> string -> (string * sort) list -> typ * (string * sort) list
    1.21 +  val cert_typ: theory -> typ -> (string * sort) list -> typ * (string * sort) list
    1.22 +  val mk_case_names_induct: descr -> attribute
    1.23    val setup: theory -> theory
    1.24  end;
    1.25  
    1.26 @@ -442,89 +443,6 @@
    1.27  
    1.28  
    1.29  
    1.30 -(** definitional introduction of datatypes **)
    1.31 -
    1.32 -fun gen_add_datatype prep_typ config new_type_names dts thy =
    1.33 -  let
    1.34 -    val _ = Theory.requires thy "Datatype" "datatype definitions";
    1.35 -
    1.36 -    (* this theory is used just for parsing *)
    1.37 -    val tmp_thy = thy |>
    1.38 -      Theory.copy |>
    1.39 -      Sign.add_types (map (fn (tvs, tname, mx, _) =>
    1.40 -        (tname, length tvs, mx)) dts);
    1.41 -
    1.42 -    val (tyvars, _, _, _)::_ = dts;
    1.43 -    val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
    1.44 -      let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
    1.45 -      in
    1.46 -        (case duplicates (op =) tvs of
    1.47 -          [] =>
    1.48 -            if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
    1.49 -            else error ("Mutually recursive datatypes must have same type parameters")
    1.50 -        | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
    1.51 -            " : " ^ commas dups))
    1.52 -      end) dts);
    1.53 -    val dt_names = map fst new_dts;
    1.54 -
    1.55 -    val _ =
    1.56 -      (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
    1.57 -        [] => ()
    1.58 -      | dups => error ("Duplicate datatypes: " ^ commas dups));
    1.59 -
    1.60 -    fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
    1.61 -      let
    1.62 -        fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
    1.63 -          let
    1.64 -            val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
    1.65 -            val _ =
    1.66 -              (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
    1.67 -                [] => ()
    1.68 -              | vs => error ("Extra type variables on rhs: " ^ commas vs))
    1.69 -          in (constrs @ [(Sign.full_name_path tmp_thy tname'
    1.70 -                  (Binding.map_name (Syntax.const_name mx') cname),
    1.71 -                   map (dtyp_of_typ new_dts) cargs')],
    1.72 -              constr_syntax' @ [(cname, mx')], sorts'')
    1.73 -          end handle ERROR msg => cat_error msg
    1.74 -           ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
    1.75 -            " of datatype " ^ quote (Binding.str_of tname));
    1.76 -
    1.77 -        val (constrs', constr_syntax', sorts') =
    1.78 -          fold prep_constr constrs ([], [], sorts)
    1.79 -
    1.80 -      in
    1.81 -        case duplicates (op =) (map fst constrs') of
    1.82 -           [] =>
    1.83 -             (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
    1.84 -                map DtTFree tvs, constrs'))],
    1.85 -              constr_syntax @ [constr_syntax'], sorts', i + 1)
    1.86 -         | dups => error ("Duplicate constructors " ^ commas dups ^
    1.87 -             " in datatype " ^ quote (Binding.str_of tname))
    1.88 -      end;
    1.89 -
    1.90 -    val (dts', constr_syntax, sorts', i) =
    1.91 -      fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
    1.92 -    val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars));
    1.93 -    val dt_info = get_all thy;
    1.94 -    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
    1.95 -    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
    1.96 -      if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
    1.97 -      else raise exn;
    1.98 -
    1.99 -    val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
   1.100 -    val ((inject, distinct, induct), thy') = thy |>
   1.101 -      DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
   1.102 -        types_syntax constr_syntax (mk_case_names_induct (flat descr));
   1.103 -  in
   1.104 -    derive_datatype_props config dt_names (SOME new_type_names) descr sorts
   1.105 -      induct inject distinct thy'
   1.106 -  end;
   1.107 -
   1.108 -val add_datatype = gen_add_datatype cert_typ;
   1.109 -val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
   1.110 -
   1.111 -
   1.112 -
   1.113  (** package setup **)
   1.114  
   1.115  (* setup theory *)
   1.116 @@ -540,27 +458,9 @@
   1.117  
   1.118  structure P = OuterParse and K = OuterKeyword
   1.119  
   1.120 -fun prep_datatype_decls args =
   1.121 -  let
   1.122 -    val names = map
   1.123 -      (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
   1.124 -    val specs = map (fn ((((_, vs), t), mx), cons) =>
   1.125 -      (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   1.126 -  in (names, specs) end;
   1.127 -
   1.128 -val parse_datatype_decl =
   1.129 -  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
   1.130 -    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
   1.131 -
   1.132 -val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
   1.133 -
   1.134  in
   1.135  
   1.136  val _ =
   1.137 -  OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
   1.138 -    (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
   1.139 -
   1.140 -val _ =
   1.141    OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
   1.142      (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
   1.143        >> (fn (alt_names, ts) => Toplevel.print