# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1262470515 -3600
# Node ID d193e2111811ca34897727740d2e0f9d29b8773f
# Parent  ba7e81531c6d2bb17f73a288180f13bcc2b7c9c3
added a warning to the quotient_type definition, if a map function is missing

diff -r ba7e81531c6d -r d193e2111811 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Fri Jan 01 23:59:32 2010 +0100
+++ b/Quot/quotient_info.ML	Sat Jan 02 23:15:15 2010 +0100
@@ -3,6 +3,7 @@
   exception NotFound
 
   type maps_info = {mapfun: string, relmap: string}
+  val maps_exists: theory -> string -> bool
   val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
@@ -77,6 +78,11 @@
    val extend = I
    val merge = Symtab.merge (K true))
 
+fun maps_exists thy s = 
+  case (Symtab.lookup (MapsData.get thy) s) of
+    SOME _ => true
+  | NONE => false
+
 fun maps_lookup thy s = 
   case (Symtab.lookup (MapsData.get thy) s) of
     SOME map_fun => map_fun
diff -r ba7e81531c6d -r d193e2111811 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Fri Jan 01 23:59:32 2010 +0100
+++ b/Quot/quotient_typ.ML	Sat Jan 02 23:15:15 2010 +0100
@@ -166,7 +166,7 @@
 end
 
 
-(* sanity checks of the quotient type specifications *)
+(* sanity checks for the quotient type specifications *)
 fun sanity_check ((vs, qty_name, _), (rty, rel)) =
 let
   val rty_tfreesT = map fst (Term.add_tfreesT rty [])
@@ -205,6 +205,24 @@
   if null errs then () else error (cat_lines errs)
 end
 
+(* check for existence of map functions *)
+fun map_check ctxt (_, (rty, _)) =
+let
+  val thy = ProofContext.theory_of ctxt
+
+  fun map_check_aux rty warns =
+    case rty of
+      Type (_, []) => warns
+    | Type (s, _) => if (maps_exists thy s) then warns else s::warns
+    | _ => warns
+
+  val warns = map_check_aux rty []
+in
+  if null warns then () 
+  else warning ("No map function defined for " ^ (commas warns) ^ 
+                ". This will cause problems later on.")
+end
+
 
 (******************************)
 (* interface and syntax setup *)
@@ -225,6 +243,7 @@
 let
   (* sanity check *)  
   val _ = map sanity_check quot_list 
+  val _ = map (map_check lthy) quot_list
 
   fun mk_goal (rty, rel) =
   let