# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261696675 -3600
# Node ID 0b60d8416ec569e000f7ee75a128bb847fb70749
# Parent  5cf83fa5b36c9fafc58e6e43ae1c65fe67adcd92
added sanity checks for quotient_type

diff -r 5cf83fa5b36c -r 0b60d8416ec5 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Thu Dec 24 22:28:19 2009 +0100
+++ b/Quot/quotient_typ.ML	Fri Dec 25 00:17:55 2009 +0100
@@ -60,7 +60,7 @@
        lambda x (HOLogic.mk_eq (c, (rel $ x))))
 end
 
-(* makes the new type definitions and proves non-emptyness*)
+(* makes the new type definitions and proves non-emptyness *)
 fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
 let
   val typedef_tac =
@@ -167,12 +167,51 @@
   ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add])
 end
 
+(* sanity checks of the quotient type specifications *)
+fun sanity_check ((vs, qty_name, _), (rty, rel)) =
+let
+  val rty_tfreesT = map fst (Term.add_tfreesT rty [])
+  val rel_tfrees = map fst (Term.add_tfrees rel [])
+  val rel_frees = map fst (Term.add_frees rel [])
+  val rel_vars = Term.add_vars rel []
+  val rel_tvars = Term.add_tvars rel []
+  val qty_str = (Binding.str_of qty_name) ^ ": "
+
+  val illegal_rel_vars =
+    if null rel_vars andalso null rel_tvars then []
+    else [qty_str ^ "illegal schematic variable(s) in the relation."]
+
+  val dup_vs =
+    (case duplicates (op =) vs of 
+       [] => []
+     | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
+
+  val extra_rty_tfrees =
+    (case subtract (op =) vs rty_tfreesT of 
+       [] => []
+     | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
+
+  val extra_rel_tfrees =
+    (case subtract (op =) vs rel_tfrees of 
+       [] => []
+     | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
+ 
+  val illegal_rel_frees =
+    (case rel_frees of 
+      [] => []
+    | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
+
+  val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
+in
+  if null errs then () else error (cat_lines errs)
+end
 
 (* interface and syntax setup *)
 
-(* the ML-interface takes a list of 4-tuples consisting of  *)
+(* the ML-interface takes a list of 5-tuples consisting of  *)
 (*                                                          *)
 (* - the name of the quotient type                          *)
+(* - its free type variables (first argument)               *)
 (* - its mixfix annotation                                  *)
 (* - the type to be quotient                                *)
 (* - the relation according to which the type is quotient   *)
@@ -190,6 +229,9 @@
               
   fun after_qed thms lthy =
     fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd
+
+  (* sanity check*)  
+  val _ = map sanity_check quot_list 
 in
   theorem after_qed goals lthy
 end
@@ -221,5 +263,3 @@
          OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
 
 end; (* structure *)
-
-