tuned whitespace;
authorwenzelm
Thu Oct 29 16:09:41 2009 +0100 (2009-10-29)
changeset 33313f6acebef3ea1
parent 33312 6ca8a7984fd9
child 33314 53d49370f7af
tuned whitespace;
src/HOL/Tools/Datatype/datatype.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 16:09:16 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 16:09:41 2009 +0100
     1.3 @@ -96,6 +96,7 @@
     1.4       cases = cases |> fold Symtab.update
     1.5         (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)});
     1.6  
     1.7 +
     1.8  (* complex queries *)
     1.9  
    1.10  fun the_spec thy dtco =
    1.11 @@ -157,6 +158,7 @@
    1.12      | NONE => NONE;
    1.13  
    1.14  
    1.15 +
    1.16  (** various auxiliary **)
    1.17  
    1.18  (* prepare datatype specifications *)
    1.19 @@ -209,6 +211,7 @@
    1.20  
    1.21  end;
    1.22  
    1.23 +
    1.24  (* translation rules for case *)
    1.25  
    1.26  fun make_case ctxt = DatatypeCase.make_case
    1.27 @@ -230,6 +233,7 @@
    1.28      [], []);
    1.29  
    1.30  
    1.31 +
    1.32  (** document antiquotation **)
    1.33  
    1.34  val _ = ThyOutput.antiquotation "datatype" Args.tyname
    1.35 @@ -256,15 +260,17 @@
    1.36      in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
    1.37  
    1.38  
    1.39 +
    1.40  (** abstract theory extensions relative to a datatype characterisation **)
    1.41  
    1.42 -structure DatatypeInterpretation = InterpretationFun
    1.43 +structure Datatype_Interpretation = InterpretationFun
    1.44    (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    1.45 -fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
    1.46 +fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
    1.47  
    1.48  fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
    1.49      (index, (((((((((((_, (tname, _, _))), inject), distinct),
    1.50 -      exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), (split, split_asm))) =
    1.51 +      exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
    1.52 +        (split, split_asm))) =
    1.53    (tname,
    1.54     {index = index,
    1.55      alt_names = alt_names,
    1.56 @@ -311,7 +317,8 @@
    1.57        config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
    1.58  
    1.59      val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
    1.60 -    val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
    1.61 +    val dt_infos = map_index
    1.62 +      (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
    1.63        (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
    1.64          case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
    1.65      val dt_names = map fst dt_infos;
    1.66 @@ -339,14 +346,16 @@
    1.67      |> snd
    1.68      |> add_case_tr' case_names
    1.69      |> register dt_infos
    1.70 -    |> DatatypeInterpretation.data (config, dt_names)
    1.71 +    |> Datatype_Interpretation.data (config, dt_names)
    1.72      |> pair dt_names
    1.73    end;
    1.74  
    1.75  
    1.76 +
    1.77  (** declare existing type as datatype **)
    1.78  
    1.79 -fun prove_rep_datatype config dt_names alt_names descr sorts raw_inject half_distinct raw_induct thy1 =
    1.80 +fun prove_rep_datatype config dt_names alt_names descr sorts
    1.81 +    raw_inject half_distinct raw_induct thy1 =
    1.82    let
    1.83      val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
    1.84      val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
    1.85 @@ -419,7 +428,8 @@
    1.86              (*FIXME somehow dubious*)
    1.87        in
    1.88          ProofContext.theory_result
    1.89 -          (prove_rep_datatype config dt_names alt_names descr vs raw_inject half_distinct raw_induct)
    1.90 +          (prove_rep_datatype config dt_names alt_names descr vs
    1.91 +            raw_inject half_distinct raw_induct)
    1.92          #-> after_qed
    1.93        end;
    1.94    in
    1.95 @@ -432,6 +442,7 @@
    1.96  val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
    1.97  
    1.98  
    1.99 +
   1.100  (** definitional introduction of datatypes **)
   1.101  
   1.102  fun gen_add_datatype prep_typ config new_type_names dts thy =
   1.103 @@ -447,16 +458,20 @@
   1.104      val (tyvars, _, _, _)::_ = dts;
   1.105      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
   1.106        let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
   1.107 -      in (case duplicates (op =) tvs of
   1.108 -            [] => if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   1.109 -                  else error ("Mutually recursive datatypes must have same type parameters")
   1.110 -          | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
   1.111 -              " : " ^ commas dups))
   1.112 +      in
   1.113 +        (case duplicates (op =) tvs of
   1.114 +          [] =>
   1.115 +            if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   1.116 +            else error ("Mutually recursive datatypes must have same type parameters")
   1.117 +        | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
   1.118 +            " : " ^ commas dups))
   1.119        end) dts);
   1.120      val dt_names = map fst new_dts;
   1.121  
   1.122 -    val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
   1.123 -      [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
   1.124 +    val _ =
   1.125 +      (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
   1.126 +        [] => ()
   1.127 +      | dups => error ("Duplicate datatypes: " ^ commas dups));
   1.128  
   1.129      fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
   1.130        let
   1.131 @@ -510,13 +525,15 @@
   1.132  val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
   1.133  
   1.134  
   1.135 +
   1.136  (** package setup **)
   1.137  
   1.138  (* setup theory *)
   1.139  
   1.140  val setup =
   1.141    trfun_setup #>
   1.142 -  DatatypeInterpretation.init;
   1.143 +  Datatype_Interpretation.init;
   1.144 +
   1.145  
   1.146  (* outer syntax *)
   1.147