# HG changeset patch
# User oheimb
# Date 1057924472 -7200
# Node ID f4d2ff3cad097b65ecbc0997eec931f746be5557
# Parent  f79d139c7e46815685ac5a3ed84bd4531e787b9c
re-introduced sort constraints on LHS

diff -r f79d139c7e46 -r f4d2ff3cad09 src/HOLCF/domain/extender.ML
--- a/src/HOLCF/domain/extender.ML	Fri Jul 11 13:54:26 2003 +0200
+++ b/src/HOLCF/domain/extender.ML	Fri Jul 11 13:54:32 2003 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOLCF/domain/extender.ML
     ID:         $Id$
-    Author:     David von Oheimb and Markus Wenzel
+    Author:     David von Oheimb
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Theory extender for domain section, including new-style theory syntax.
@@ -49,23 +49,23 @@
 	|   rm_sorts (TVar(s,_))  = TVar(s,[])
 	and remove_sorts l = map rm_sorts l;
 	fun analyse(TFree(v,s)) = (case assoc_string(tvars,v) of 
-		    None      => error ("Free type variable " ^ v ^ " on rhs.")
+		    None => error ("Free type variable " ^ quote v ^ " on rhs.")
 	          | Some sort => if eq_set_string (s,defaultS) orelse
 				    eq_set_string (s,sort    )
 				 then TFree(distinct_name v,sort)
-				 else error ("Additional constraint on rhs "^
-					     "for type variable "^quote v))
+				 else error ("Inconsistent sort constraint" ^
+				             " for type variable " ^ quote v))
 	(** BUG OR FEATURE?: mutual recursion may use different arguments **)
         |   analyse(Type(s,typl)) = (case assoc_string((*dtnvs*)
 						       [(dname,typevars)],s) of 
 		None          => Type(s,map analyse typl)
 	      | Some typevars => if remove_sorts typevars = remove_sorts typl 
 				then Type(s,map analyse typl)
-				else error ("Recursion of type " ^ s ^ 
+				else error ("Recursion of type " ^ quote s ^ 
 					    " with different arguments"))
         |   analyse(TVar _) = Imposs "extender:analyse";
 	fun check_pcpo t = (pcpo_type sg t orelse error(
-			   "Type not of sort pcpo: "^string_of_typ sg t); t);
+      "Constructor argument type is not of sort pcpo: "^string_of_typ sg t); t);
 	val analyse_con = upd_third (map (upd_third (check_pcpo o analyse)));
       in ((dname,distinct_typevars), map analyse_con cons') end; 
   in ListPair.map analyse_equation (dtnvs,cons'')
@@ -127,7 +127,14 @@
   P.name -- Scan.repeat dest_decl -- P.opt_mixfix
   >> (fn ((c, ds), mx) => (c, mx, ds));
 
-val domain_decl = (P.type_args -- P.name >> Library.swap) -- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+val type_var' = (P.type_ident ^^ 
+                 Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) "");
+val type_args' = type_var' >> single ||
+                 P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
+ 		 Scan.succeed [];
+
+val domain_decl = (type_args' -- P.name >> Library.swap) -- 
+                  (P.$$$ "=" |-- P.enum1 "|" cons_decl);
 val domains_decl =
   Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
   >> (fn (opt_name, doms) =>
diff -r f79d139c7e46 -r f4d2ff3cad09 src/HOLCF/domain/interface.ML
--- a/src/HOLCF/domain/interface.ML	Fri Jul 11 13:54:26 2003 +0200
+++ b/src/HOLCF/domain/interface.ML	Fri Jul 11 13:54:32 2003 +0200
@@ -5,6 +5,7 @@
 
 Parser for domain section.
 *)
+(** BEWARE: this is still needed for old-style theories **)
 
 local 
   open ThyParse;
@@ -101,21 +102,21 @@
       "") end;
 
 (* ----- parser for domain declaration equation ----------------------------- *)
+(** BEWARE: should be consistent with domains_decl in extender.ML **)
 
   val name' = name >> unenclose;
-  val type_var' = type_var >> unenclose;
   fun esc_quote s = let fun esc [] = []
 			|   esc ("\""::xs) = esc xs
 			|   esc ("[" ::xs) = "{"::esc xs
 			|   esc ("]" ::xs) = "}"::esc xs
 			|   esc (x   ::xs) = x  ::esc xs
 		    in implode (esc (Symbol.explode s)) end;
-  val tvar = (type_var' ^^ 
-	      optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
-  fun type_args l = (tvar >> (fn x => [x])
-                 ||  "(" $$-- !! (list1 tvar --$$ ")")
-                 ||  empty >> K []) l
-  fun con_typ l   = (type_args -- name' >> (fn (x,y) => (y,x))) l
+  val type_var' = ((type_var >> unenclose) ^^ 
+	          optional ($$ "::" ^^ !! (sort >> esc_quote)) "") >> quote;
+  val type_args = (type_var' >> single
+                 ||  "(" $$-- !! (list1 type_var' --$$ ")")
+                 ||  empty >> K [])
+  val con_typ   = (type_args -- name' >> Library.swap)
                       (* here ident may be used instead of name' 
                          to avoid ambiguity with standard mixfix option *)
   val domain_arg  = "(" $$-- (optional ($$ "lazy" >> K true) false)