src/HOL/Tools/datatype_codegen.ML
changeset 22778 a5b87573f427
parent 22746 f090ecd44f12
child 22921 475ff421a6a3
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Apr 24 15:11:07 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Apr 24 15:13:19 2007 +0200
     1.3 @@ -65,8 +65,6 @@
     1.4  
     1.5  fun add_dt_defs thy defs dep module gr (descr: DatatypeAux.descr) =
     1.6    let
     1.7 -    val tab = DatatypePackage.get_datatypes thy;
     1.8 -
     1.9      val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
    1.10      val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
    1.11        exists (exists DatatypeAux.is_rec_type o snd) cs) descr');
    1.12 @@ -285,27 +283,26 @@
    1.13  
    1.14  fun datatype_codegen thy defs gr dep module brack t = (case strip_comb t of
    1.15     (c as Const (s, T), ts) =>
    1.16 -       (case Library.find_first (fn (_, {index, descr, case_name, ...}) =>
    1.17 -         s = case_name orelse
    1.18 -           AList.defined (op =) ((#3 o the o AList.lookup (op =) descr) index) s)
    1.19 -             (Symtab.dest (DatatypePackage.get_datatypes thy)) of
    1.20 -          NONE => NONE
    1.21 -        | SOME (tname, {index, descr, ...}) =>
    1.22 -           if is_some (get_assoc_code thy s T) then NONE else
    1.23 -           let val SOME (_, _, constrs) = AList.lookup (op =) descr index
    1.24 -           in (case (AList.lookup (op =) constrs s, strip_type T) of
    1.25 -               (NONE, _) => SOME (pretty_case thy defs gr dep module brack
    1.26 -                 ((#3 o the o AList.lookup (op =) descr) index) c ts)
    1.27 -             | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs
    1.28 -                 (fst (invoke_tycodegen thy defs dep module false
    1.29 -                    (gr, snd (strip_type T))))
    1.30 -                 dep module brack args c ts)
    1.31 -             | _ => NONE)
    1.32 -           end)
    1.33 - |  _ => NONE);
    1.34 +     (case DatatypePackage.datatype_of_case thy s of
    1.35 +        SOME {index, descr, ...} =>
    1.36 +          if is_some (get_assoc_code thy s T) then NONE else
    1.37 +          SOME (pretty_case thy defs gr dep module brack
    1.38 +            (#3 (the (AList.lookup op = descr index))) c ts)
    1.39 +      | NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of
    1.40 +        (SOME {index, descr, ...}, (_, U as Type _)) =>
    1.41 +          if is_some (get_assoc_code thy s T) then NONE else
    1.42 +          let val SOME args = AList.lookup op =
    1.43 +            (#3 (the (AList.lookup op = descr index))) s
    1.44 +          in
    1.45 +            SOME (pretty_constr thy defs
    1.46 +              (fst (invoke_tycodegen thy defs dep module false (gr, U)))
    1.47 +              dep module brack args c ts)
    1.48 +          end
    1.49 +      | _ => NONE)
    1.50 + | _ => NONE);
    1.51  
    1.52  fun datatype_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    1.53 -      (case Symtab.lookup (DatatypePackage.get_datatypes thy) s of
    1.54 +      (case DatatypePackage.get_datatype thy s of
    1.55           NONE => NONE
    1.56         | SOME {descr, ...} =>
    1.57             if isSome (get_assoc_type thy s) then NONE else
    1.58 @@ -325,8 +322,8 @@
    1.59  (** datatypes for code 2nd generation **)
    1.60  
    1.61  fun dtyp_of_case_const thy c =
    1.62 -  get_first (fn (dtco, { case_name, ... }) => if case_name = c then SOME dtco else NONE)
    1.63 -    ((Symtab.dest o DatatypePackage.get_datatypes) thy);
    1.64 +  Option.map (fn {descr, index, ...} => #1 (the (AList.lookup op = descr index)))
    1.65 +    (DatatypePackage.datatype_of_case thy c);
    1.66  
    1.67  fun dest_case_app cs ts tys =
    1.68    let