# HG changeset patch
# User haftmann
# Date 1174639253 -3600
# Node ID 6ee2edbce31cd4796c1a2fa8f5502949a17aa5d4
# Parent  3572bc633d9a212f6ef9767622b1410beaddb6d1
added concept for term constructors

diff -r 3572bc633d9a -r 6ee2edbce31c src/Pure/Tools/codegen_consts.ML
--- a/src/Pure/Tools/codegen_consts.ML	Fri Mar 23 09:40:50 2007 +0100
+++ b/src/Pure/Tools/codegen_consts.ML	Fri Mar 23 09:40:53 2007 +0100
@@ -16,8 +16,19 @@
   val typ_of_inst: theory -> const -> string * typ
   val norm: theory -> const -> const
   val norm_of_typ: theory -> string * typ -> const
-  val typ_sort_inst: Sorts.algebra -> typ * sort -> sort Vartab.table -> sort Vartab.table
+  val typ_sort_inst: Sorts.algebra -> typ * sort
+    -> sort Vartab.table -> sort Vartab.table
   val typargs: theory -> string * typ -> typ list
+  val co_of_const: theory -> const
+    -> string * ((string * sort) list * (string * typ list))
+  val co_of_const': theory -> const
+    -> (string * ((string * sort) list * (string * typ list))) option
+  val cos_of_consts: theory -> const list
+    -> string * ((string * sort) list * (string * typ list) list)
+  val const_of_co: theory -> string -> (string * sort) list
+    -> string * typ list -> const
+  val consts_of_cos: theory -> string -> (string * sort) list
+    -> (string * typ list) list -> const list
   val find_def: theory -> const -> (string (*theory name*) * thm) option
   val consts_of: theory -> term -> const list
   val read_const: theory -> string -> const
@@ -117,6 +128,75 @@
   end;
 
 
+(* printing *)
+
+fun string_of_const thy (c, tys) =
+  space_implode " " (Sign.extern_const thy c
+    :: map (enclose "[" "]" o Sign.string_of_typ thy) tys);
+
+fun raw_string_of_const (c, tys) =
+  space_implode " " (c
+    :: map (enclose "[" "]" o Display.raw_string_of_typ) tys);
+
+fun string_of_const_typ thy (c, ty) =
+  string_of_const thy (c, Consts.typargs (Sign.consts_of thy) (c, ty));
+
+
+(* conversion between constants and datatype constructors *)
+
+fun const_of_co thy tyco vs (co, tys) =
+  norm_of_typ thy (co, tys ---> Type (tyco, map TFree vs));
+
+fun consts_of_cos thy tyco vs cos =
+  let
+    val dty = Type (tyco, map TFree vs);
+    fun mk_co (co, tys) = norm_of_typ thy (co, tys ---> dty);
+  in map mk_co cos end;
+
+local
+
+exception BAD of string;
+
+fun gen_co_of_const thy const =
+  let
+    val (c, ty) = (apsnd Logic.unvarifyT o typ_of_inst thy) const;
+    fun err () = raise BAD
+     ("Illegal type for datatype constructor: " ^ Sign.string_of_typ thy ty);
+    val (tys, ty') = strip_type ty;
+    val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
+      handle TYPE _ => err ();
+    val sorts = if has_duplicates (eq_fst op =) vs then err ()
+      else map snd vs;
+    val vs_names = Name.invent_list [] "'a" (length vs);
+    val vs_map = map fst vs ~~ vs_names;
+    val vs' = vs_names ~~ sorts;
+    val tys' = (map o map_type_tfree) (fn (v, sort) =>
+      (TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys
+      handle Option => err ();
+  in (tyco, (vs', (c, tys'))) end;
+
+in
+
+fun co_of_const thy const = gen_co_of_const thy const handle BAD msg => error msg;
+fun co_of_const' thy const = SOME (gen_co_of_const thy const) handle BAD msg => NONE;
+
+end;
+
+fun cos_of_consts thy consts =
+  let
+    val raw_cos  = map (co_of_const thy) consts;
+    val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1
+      then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos,
+        map ((apfst o map) snd o snd) raw_cos))
+      else error ("Term constructors not referring to the same type: "
+        ^ commas (map (string_of_const thy) consts));
+    val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy))
+      (map fst sorts_cos);
+    val cos = map snd sorts_cos;
+    val vs = vs_names ~~ sorts;
+  in (tyco, (vs, cos)) end;
+
+
 (* reading constants as terms *)
 
 fun read_const_typ thy raw_t =
@@ -131,17 +211,4 @@
   norm_of_typ thy o read_const_typ thy;
 
 
-(* printing *)
-
-fun string_of_const thy (c, tys) =
-  space_implode " " (Sign.extern_const thy c
-    :: map (enclose "[" "]" o Sign.string_of_typ thy) tys);
-
-fun raw_string_of_const (c, tys) =
-  space_implode " " (c
-    :: map (enclose "[" "]" o Display.raw_string_of_typ) tys);
-
-fun string_of_const_typ thy (c, ty) =
-  string_of_const thy (c, Consts.typargs (Sign.consts_of thy) (c, ty));
-
 end;