src/HOL/Tools/datatype_package.ML
changeset 20597 65fe827aa595
parent 20328 5b240a4216b0
child 20715 c1f16b427d86
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 19 15:22:03 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 19 15:22:05 2006 +0200
     1.3 @@ -308,7 +308,7 @@
     1.4    (snd o PureThy.add_thmss [(("simps", simps), []),
     1.5      (("", List.concat case_thms @ size_thms @ 
     1.6            List.concat distinct  @ rec_thms), [Simplifier.simp_add]),
     1.7 -    (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
     1.8 +    (("", size_thms @ rec_thms),             [setmp CodegenData.strict_functyp false (RecfunCodegen.add NONE)]),
     1.9      (("", List.concat inject),               [iff_add]),
    1.10      (("", map name_notE (List.concat distinct)),  [Classical.safe_elim NONE]),
    1.11      (("", weak_case_congs),                  [cong_att])]);
    1.12 @@ -479,9 +479,10 @@
    1.13         strip_abs (length dts) t, is_dependent (length dts) t))
    1.14        (constrs ~~ fs);
    1.15      fun count_cases (cs, (_, _, true)) = cs
    1.16 -      | count_cases (cs, (cname, (_, body), false)) = (case AList.lookup (op =) cs body of
    1.17 -          NONE => (body, [cname]) :: cs
    1.18 -        | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs);
    1.19 +      | count_cases (cs, (cname, (_, body), false)) =
    1.20 +          case AList.lookup (op = : term * term -> bool) cs body
    1.21 +           of NONE => (body, [cname]) :: cs
    1.22 +            | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs;
    1.23      val cases' = sort (int_ord o Library.swap o pairself (length o snd))
    1.24        (Library.foldl count_cases ([], cases));
    1.25      fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
    1.26 @@ -558,33 +559,42 @@
    1.27  
    1.28  (********************* axiomatic introduction of datatypes ********************)
    1.29  
    1.30 -fun add_and_get_axioms_atts label tnames attss ts thy =
    1.31 -  foldr (fn (((tname, atts), t), (thy', axs)) =>
    1.32 -    let
    1.33 -      val ([ax], thy'') =
    1.34 -        thy'
    1.35 -        |> Theory.add_path tname
    1.36 -        |> PureThy.add_axioms_i [((label, t), atts)];
    1.37 -    in (Theory.parent_path thy'', ax::axs)
    1.38 -    end) (thy, []) (tnames ~~ attss ~~ ts) |> swap;
    1.39 +fun add_axiom label t atts thy =
    1.40 +  thy
    1.41 +  |> PureThy.add_axioms_i [((label, t), atts)];
    1.42 +
    1.43 +fun add_axioms label ts atts thy =
    1.44 +  thy
    1.45 +  |> PureThy.add_axiomss_i [((label, ts), atts)];
    1.46  
    1.47 -fun add_and_get_axioms label tnames =
    1.48 -  add_and_get_axioms_atts label tnames (replicate (length tnames) []);
    1.49 +fun add_and_get_axioms_atts label tnames ts attss =
    1.50 +  fold_map (fn (tname, (atts, t)) => fn thy =>
    1.51 +    thy
    1.52 +    |> Theory.add_path tname
    1.53 +    |> add_axiom label t atts
    1.54 +    ||> Theory.parent_path
    1.55 +    |-> (fn [ax] => pair ax)) (tnames ~~ (attss ~~ ts));
    1.56  
    1.57 -fun add_and_get_axiomss label tnames tss thy =
    1.58 -  foldr (fn ((tname, ts), (thy', axss)) =>
    1.59 -    let
    1.60 -      val ([axs], thy'') =
    1.61 -        thy'
    1.62 -        |> Theory.add_path tname
    1.63 -        |> PureThy.add_axiomss_i [((label, ts), [])];
    1.64 -    in (Theory.parent_path thy'', axs::axss)
    1.65 -    end) (thy, []) (tnames ~~ tss) |> swap;
    1.66 +fun add_and_get_axioms label tnames ts =
    1.67 +  add_and_get_axioms_atts label tnames ts (replicate (length tnames) []);
    1.68 +
    1.69 +fun add_and_get_axiomss label tnames tss =
    1.70 +  fold_map (fn (tname, ts) => fn thy =>
    1.71 +    thy
    1.72 +    |> Theory.add_path tname
    1.73 +    |> add_axioms label ts []
    1.74 +    ||> Theory.parent_path
    1.75 +    |-> (fn [ax] => pair ax)) (tnames ~~ tss);
    1.76  
    1.77  fun specify_consts args thy =
    1.78 -  let val specs =
    1.79 -    args |> map (fn (c, T, mx) => Const (Sign.full_name thy (Syntax.const_name c mx), T));
    1.80 -  in thy |> Theory.add_consts_i args |> Theory.add_finals_i false specs end;
    1.81 +  let
    1.82 +    val specs = map (fn (c, T, mx) =>
    1.83 +      Const (Sign.full_name thy (Syntax.const_name c mx), T)) args;
    1.84 +  in
    1.85 +    thy
    1.86 +    |> Sign.add_consts_i args
    1.87 +    |> Theory.add_finals_i false specs
    1.88 +  end;
    1.89  
    1.90  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    1.91      case_names_induct case_names_exhausts thy =
    1.92 @@ -675,10 +685,9 @@
    1.93      val ((([induct], [rec_thms]), inject), thy3) =
    1.94        thy2
    1.95        |> Theory.add_path (space_implode "_" new_type_names)
    1.96 -      |> PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
    1.97 -          [case_names_induct])]
    1.98 -      ||>> PureThy.add_axiomss_i [(("recs", rec_axs), [])]
    1.99 -      ||> (if no_size then I else snd o PureThy.add_axiomss_i [(("size", size_axs), [])])
   1.100 +      |> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct]
   1.101 +      ||>> add_axioms "recs" rec_axs []
   1.102 +      ||> (if no_size then I else add_axioms "size" size_axs [] #> snd)
   1.103        ||> Theory.parent_path
   1.104        ||>> add_and_get_axiomss "inject" new_type_names
   1.105              (DatatypeProp.make_injs descr sorts);
   1.106 @@ -688,7 +697,7 @@
   1.107  
   1.108      val exhaust_ts = DatatypeProp.make_casedists descr sorts;
   1.109      val (exhaustion, thy5) = add_and_get_axioms_atts "exhaust" new_type_names
   1.110 -      (map Library.single case_names_exhausts) exhaust_ts thy4;
   1.111 +      exhaust_ts (map single case_names_exhausts) thy4;
   1.112      val (case_thms, thy6) = add_and_get_axiomss "cases" new_type_names
   1.113        (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
   1.114      val (split_ts, split_asm_ts) = ListPair.unzip
   1.115 @@ -924,11 +933,9 @@
   1.116        Theory.add_types (map (fn (tvs, tname, mx, _) =>
   1.117          (tname, length tvs, mx)) dts);
   1.118  
   1.119 -    val sign = Theory.sign_of tmp_thy;
   1.120 -
   1.121      val (tyvars, _, _, _)::_ = dts;
   1.122      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
   1.123 -      let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
   1.124 +      let val full_tname = Sign.full_name tmp_thy (Syntax.type_name tname mx)
   1.125        in (case duplicates (op =) tvs of
   1.126              [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   1.127                    else error ("Mutually recursive datatypes must have same type parameters")
   1.128 @@ -943,12 +950,12 @@
   1.129        let
   1.130          fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
   1.131            let
   1.132 -            val (cargs', sorts'') = Library.foldl (prep_typ sign) (([], sorts'), cargs);
   1.133 +            val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
   1.134              val _ = (case foldr add_typ_tfree_names [] cargs' \\ tvs of
   1.135                  [] => ()
   1.136                | vs => error ("Extra type variables on rhs: " ^ commas vs))
   1.137 -          in (constrs @ [((if flat_names then Sign.full_name sign else
   1.138 -                Sign.full_name_path sign tname) (Syntax.const_name cname mx'),
   1.139 +          in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
   1.140 +                Sign.full_name_path tmp_thy tname) (Syntax.const_name cname mx'),
   1.141                     map (dtyp_of_typ new_dts) cargs')],
   1.142                constr_syntax' @ [(cname, mx')], sorts'')
   1.143            end handle ERROR msg =>
   1.144 @@ -961,7 +968,7 @@
   1.145        in
   1.146          case duplicates (op =) (map fst constrs') of
   1.147             [] =>
   1.148 -             (dts' @ [(i, (Sign.full_name sign (Syntax.type_name tname mx),
   1.149 +             (dts' @ [(i, (Sign.full_name tmp_thy (Syntax.type_name tname mx),
   1.150                  map DtTFree tvs, constrs'))],
   1.151                constr_syntax @ [constr_syntax'], sorts', i + 1)
   1.152           | dups => error ("Duplicate constructors " ^ commas dups ^
   1.153 @@ -969,9 +976,9 @@
   1.154        end;
   1.155  
   1.156      val (dts', constr_syntax, sorts', i) = Library.foldl prep_dt_spec (([], [], [], 0), dts);
   1.157 -    val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
   1.158 +    val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
   1.159      val dt_info = get_datatypes thy;
   1.160 -    val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
   1.161 +    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
   1.162      val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
   1.163        if err then error ("Nonemptiness check failed for datatype " ^ s)
   1.164        else raise exn;