datatype packages: record datatype_config for configuration flags; less verbose signatures
authorhaftmann
Wed Jun 17 08:13:05 2009 +0200 (2009-06-17 ago)
changeset 3167181e5e8ffe92f
parent 31670 ce07fc5fcb17
child 31672 2f8e3150e073
datatype packages: record datatype_config for configuration flags; less verbose signatures
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 16 17:27:10 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Jun 17 08:13:05 2009 +0200
     1.3 @@ -101,8 +101,9 @@
     1.4      val (_,thy1) = 
     1.5      fold_map (fn ak => fn thy => 
     1.6            let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
     1.7 -              val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
     1.8 -              val inject_flat = Library.flat inject
     1.9 +              val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype
    1.10 +                DatatypeAux.default_datatype_config [ak] [dt] thy
    1.11 +              val inject_flat = flat inject
    1.12                val ak_type = Type (Sign.intern_type thy1 ak,[])
    1.13                val ak_sign = Sign.intern_const thy1 ak 
    1.14                
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Jun 16 17:27:10 2009 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Jun 17 08:13:05 2009 +0200
     2.3 @@ -6,8 +6,9 @@
     2.4  
     2.5  signature NOMINAL_PACKAGE =
     2.6  sig
     2.7 -  val add_nominal_datatype : bool -> string list -> (string list * bstring * mixfix *
     2.8 -    (bstring * string list * mixfix) list) list -> theory -> theory
     2.9 +  val add_nominal_datatype : DatatypeAux.datatype_config -> string list ->
    2.10 +    (string list * bstring * mixfix *
    2.11 +      (bstring * string list * mixfix) list) list -> theory -> theory
    2.12    type descr
    2.13    type nominal_datatype_info
    2.14    val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
    2.15 @@ -190,7 +191,7 @@
    2.16  fun fresh_star_const T U =
    2.17    Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
    2.18  
    2.19 -fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
    2.20 +fun gen_add_nominal_datatype prep_typ config new_type_names dts thy =
    2.21    let
    2.22      (* this theory is used just for parsing *)
    2.23  
    2.24 @@ -243,7 +244,7 @@
    2.25      val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
    2.26  
    2.27      val ({induction, ...},thy1) =
    2.28 -      DatatypePackage.add_datatype err flat_names new_type_names' dts'' thy;
    2.29 +      DatatypePackage.add_datatype config new_type_names' dts'' thy;
    2.30  
    2.31      val SOME {descr, ...} = Symtab.lookup
    2.32        (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
    2.33 @@ -815,7 +816,7 @@
    2.34          val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
    2.35            ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
    2.36        in
    2.37 -        (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
    2.38 +        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
    2.39        end;
    2.40  
    2.41      val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
    2.42 @@ -1509,7 +1510,7 @@
    2.43      val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
    2.44        thy10 |>
    2.45          InductivePackage.add_inductive_global (serial_string ())
    2.46 -          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
    2.47 +          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    2.48             alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
    2.49             skip_mono = true, fork_mono = false}
    2.50            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    2.51 @@ -2067,7 +2068,7 @@
    2.52      thy13
    2.53    end;
    2.54  
    2.55 -val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ true;
    2.56 +val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ;
    2.57  
    2.58  
    2.59  (* FIXME: The following stuff should be exported by DatatypePackage *)
    2.60 @@ -2083,7 +2084,7 @@
    2.61      val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
    2.62      val specs = map (fn ((((_, vs), t), mx), cons) =>
    2.63        (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
    2.64 -  in add_nominal_datatype false names specs end;
    2.65 +  in add_nominal_datatype DatatypeAux.default_datatype_config names specs end;
    2.66  
    2.67  val _ =
    2.68    OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl