src/HOL/Tools/datatype_package.ML
changeset 26267 ba710daf77a7
parent 26111 91e0999b075f
child 26336 a0e2b706ce73
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Mar 14 08:52:51 2008 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Mar 14 08:52:52 2008 +0100
     1.3 @@ -65,6 +65,10 @@
     1.4    val datatype_of_constr : theory -> string -> DatatypeAux.datatype_info option
     1.5    val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option
     1.6    val get_datatype_constrs : theory -> string -> (string * typ) list option
     1.7 +  val construction_interpretation: theory
     1.8 +    -> { atom: typ -> 'a, dtyp: string -> 'a, rtyp: string -> 'a list -> 'a }
     1.9 +    -> (string * Term.sort) list -> string list
    1.10 +    -> (string * (string * 'a list) list) list
    1.11    val interpretation: (string list -> theory -> theory) -> theory -> theory
    1.12    val print_datatypes : theory -> unit
    1.13    val make_case :  Proof.context -> bool -> string list -> term ->
    1.14 @@ -159,6 +163,22 @@
    1.15          in SOME (map mk_co cos) end
    1.16      | NONE => NONE;
    1.17  
    1.18 +fun construction_interpretation thy { atom, dtyp, rtyp } sorts tycos =
    1.19 +  let
    1.20 +    val descr = (#descr o the_datatype thy o hd) tycos;
    1.21 +    val k = length tycos;
    1.22 +    val descr_of = the o AList.lookup (op =) descr;
    1.23 +    fun interpT (T as DtTFree _) = atom (typ_of_dtyp descr sorts T)
    1.24 +      | interpT (T as DtType (tyco, Ts)) = if is_rec_type T
    1.25 +          then rtyp tyco (map interpT Ts)
    1.26 +          else atom (typ_of_dtyp descr sorts T)
    1.27 +      | interpT (DtRec l) = if l < k then (dtyp o #1 o descr_of) l
    1.28 +          else let val (tyco, Ts, _) = descr_of l
    1.29 +          in rtyp tyco (map interpT Ts) end;
    1.30 +    fun interpC (c, Ts) = (c, map interpT Ts);
    1.31 +    fun interpK (_, (tyco, _, cs)) = (tyco, map interpC cs);
    1.32 +  in map interpK (Library.take (k, descr)) end;
    1.33 +
    1.34  fun find_tname var Bi =
    1.35    let val frees = map dest_Free (term_frees Bi)
    1.36        val params = rename_wrt_term Bi (Logic.strip_params Bi);