src/HOL/Tools/datatype_codegen.ML
changeset 22746 f090ecd44f12
parent 22578 b0eb5652f210
child 22778 a5b87573f427
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Apr 20 11:21:47 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Apr 20 11:21:48 2007 +0200
     1.3 @@ -530,41 +530,6 @@
     1.4  
     1.5  (* instrumentalizing the sort algebra *)
     1.6  
     1.7 -(*fun assume_arities_of_sort thy arities ty_sort =
     1.8 -  let
     1.9 -    val pp = Sign.pp thy;
    1.10 -    val algebra = Sign.classes_of thy
    1.11 -      |> fold (fn (tyco, asorts, sort) =>
    1.12 -           Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities;
    1.13 -  in Sorts.of_sort algebra ty_sort end;
    1.14 -
    1.15 -fun get_codetypes_arities thy tycos sort =
    1.16 -  let
    1.17 -    val algebra = Sign.classes_of thy;
    1.18 -    val (vs_proto, css_proto) = the_codetypes_mut_specs thy tycos;
    1.19 -    val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto;
    1.20 -    fun inst_type tyco (c, tys) =
    1.21 -      let
    1.22 -        val tys' = (map o map_atyps)
    1.23 -          (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys
    1.24 -      in (c, tys') end;
    1.25 -    val css = map (fn (tyco, (_, cs)) => (tyco, (map (inst_type tyco) cs))) css_proto;
    1.26 -    fun mk_arity tyco = (tyco, map snd vs, sort);
    1.27 -    fun typ_of_sort ty =
    1.28 -      let
    1.29 -        val arities = map (fn (tyco, _) => (tyco, map snd vs, sort)) css;
    1.30 -      in assume_arities_of_sort thy arities (ty, sort) end;
    1.31 -    fun mk_cons tyco (c, tys) =
    1.32 -      let
    1.33 -        val ts = Name.names Name.context "a" tys;
    1.34 -        val ty = tys ---> Type (tyco, map TFree vs);
    1.35 -      in list_comb (Const (c, ty), map Free ts) end;
    1.36 -  in if forall (fn (_, cs) => forall (fn (_, tys) => forall typ_of_sort tys) cs) css
    1.37 -    then SOME (
    1.38 -      map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
    1.39 -    ) else NONE
    1.40 -  end;*)
    1.41 -
    1.42  fun get_codetypes_arities thy tycos sort =
    1.43    let
    1.44      val pp = Sign.pp thy;