src/HOL/Tools/datatype_codegen.ML
changeset 18220 43cf5767f992
parent 17521 0f1c48de39f5
child 18247 b17724cae935
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Nov 22 12:42:59 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Nov 22 12:59:25 2005 +0100
     1.3 @@ -7,6 +7,9 @@
     1.4  
     1.5  signature DATATYPE_CODEGEN =
     1.6  sig
     1.7 +  val is_datatype: theory -> string -> bool
     1.8 +  val get_datatype: theory -> string -> (string list * string list) option
     1.9 +  val get_datacons: theory -> string * string -> typ list option
    1.10    val setup: (theory -> theory) list
    1.11  end;
    1.12  
    1.13 @@ -296,9 +299,58 @@
    1.14             end)
    1.15    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
    1.16  
    1.17 +fun is_datatype thy dtyco =
    1.18 +  Symtab.lookup (DatatypePackage.get_datatypes thy) dtyco
    1.19 +  |> is_some;
    1.20  
    1.21 -val setup =
    1.22 -  [add_codegen "datatype" datatype_codegen,
    1.23 -   add_tycodegen "datatype" datatype_tycodegen];
    1.24 +fun get_datatype thy dtname =
    1.25 +  case CodegenPackage.tname_of_idf thy dtname
    1.26 +   of SOME dtname =>
    1.27 +        dtname
    1.28 +        |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    1.29 +        |> Option.map #descr
    1.30 +        |> these
    1.31 +        |> get_first (fn (_, (dtname', vs, cs)) =>
    1.32 +             if dtname = dtname'
    1.33 +             then SOME (vs, map fst cs)
    1.34 +             else NONE)
    1.35 +        |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree)))
    1.36 +    | _ => NONE;
    1.37 +
    1.38 +fun get_datacons thy (c, dtname) =
    1.39 +  let
    1.40 +    val descr =
    1.41 +      dtname
    1.42 +      |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    1.43 +      |> Option.map #descr
    1.44 +      |> these
    1.45 +    val one_descr =
    1.46 +      descr
    1.47 +      |> get_first (fn (_, (dtname', vs, cs)) =>
    1.48 +          if dtname = dtname'
    1.49 +          then SOME (vs, cs)
    1.50 +          else NONE);
    1.51 +  in
    1.52 +    if is_some one_descr
    1.53 +    then
    1.54 +      the one_descr
    1.55 +      |> (fn (vs, cs) =>
    1.56 +          c
    1.57 +          |> AList.lookup (op =) cs
    1.58 +          |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair [])
    1.59 +               (map DatatypeAux.dest_DtTFree vs)))))
    1.60 +    else NONE
    1.61 +  end;
    1.62 +
    1.63 +val setup = [
    1.64 +  add_codegen "datatype" datatype_codegen,
    1.65 +  add_tycodegen "datatype" datatype_tycodegen,
    1.66 +  CodegenPackage.set_is_datatype
    1.67 +    is_datatype,
    1.68 +  CodegenPackage.add_defgen 
    1.69 +    ("datatype", CodegenPackage.defgen_datatype get_datatype),
    1.70 +  CodegenPackage.add_defgen
    1.71 +    ("datacons", CodegenPackage.defgen_datacons get_datacons)
    1.72 +];
    1.73  
    1.74  end;