src/HOL/Tools/datatype_codegen.ML
changeset 18247 b17724cae935
parent 18220 43cf5767f992
child 18334 a41ce9c10b73
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Nov 25 14:51:39 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Nov 25 17:41:52 2005 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    val is_datatype: theory -> string -> bool
     1.5    val get_datatype: theory -> string -> (string list * string list) option
     1.6    val get_datacons: theory -> string * string -> typ list option
     1.7 +  val get_case_const_data: theory -> string -> (string * int) list option;
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -264,17 +265,17 @@
    1.12  
    1.13  fun datatype_codegen thy defs gr dep module brack t = (case strip_comb t of
    1.14     (c as Const (s, T), ts) =>
    1.15 -       (case find_first (fn (_, {index, descr, case_name, ...}) =>
    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 isSome (get_assoc_code thy s T) then NONE else
    1.23 +           if is_some (get_assoc_code thy s T) then NONE else
    1.24             let val SOME (_, _, constrs) = AList.lookup (op =) descr index
    1.25             in (case (AList.lookup (op =) constrs s, strip_type T) of
    1.26                 (NONE, _) => SOME (pretty_case thy defs gr dep module brack
    1.27 -                 (#3 (valOf (AList.lookup (op =) descr index))) c ts)
    1.28 +                 ((#3 o the o AList.lookup (op =) descr) index) c ts)
    1.29               | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs
    1.30                   (fst (invoke_tycodegen thy defs dep module false
    1.31                      (gr, snd (strip_type T))))
    1.32 @@ -342,15 +343,26 @@
    1.33      else NONE
    1.34    end;
    1.35  
    1.36 +fun get_case_const_data thy f =
    1.37 +  case Library.find_first (fn (_, {index, descr, case_name, ...}) =>
    1.38 +      case_name = f
    1.39 +    ) ((Symtab.dest o DatatypePackage.get_datatypes) thy)
    1.40 +   of NONE => NONE
    1.41 +    | SOME (_, {index, descr, ...}) =>
    1.42 +        (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
    1.43 +
    1.44 +
    1.45  val setup = [
    1.46    add_codegen "datatype" datatype_codegen,
    1.47    add_tycodegen "datatype" datatype_tycodegen,
    1.48    CodegenPackage.set_is_datatype
    1.49      is_datatype,
    1.50 -  CodegenPackage.add_defgen 
    1.51 +  CodegenPackage.add_defgen
    1.52      ("datatype", CodegenPackage.defgen_datatype get_datatype),
    1.53    CodegenPackage.add_defgen
    1.54 -    ("datacons", CodegenPackage.defgen_datacons get_datacons)
    1.55 +    ("datacons", CodegenPackage.defgen_datacons get_datacons),
    1.56 +  CodegenPackage.add_codegen_expr
    1.57 +    ("case", CodegenPackage.codegen_case get_case_const_data)
    1.58  ];
    1.59  
    1.60  end;