# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1226168100 18000
# Node ID 6ee1c761818f489915b4773e288b0a915d58cae1
# Parent  667c0e54632a015c43d71e82dec958f3cd95157d
Some small changes while failing to write [restrict]

diff -r 667c0e54632a -r 6ee1c761818f src/disjoint.sig
--- a/src/disjoint.sig	Sat Nov 08 12:24:23 2008 -0500
+++ b/src/disjoint.sig	Sat Nov 08 13:15:00 2008 -0500
@@ -40,4 +40,6 @@
 
     val hnormCon : ElabEnv.env * env -> Elab.con -> Elab.con * goal list
 
+    val p_env : env -> unit
+
 end
diff -r 667c0e54632a -r 6ee1c761818f src/disjoint.sml
--- a/src/disjoint.sml	Sat Nov 08 12:24:23 2008 -0500
+++ b/src/disjoint.sml	Sat Nov 08 13:15:00 2008 -0500
@@ -53,6 +53,8 @@
 
 fun pp p = print (p2s p ^ "\n")
 
+fun rp2s (p, ns) = String.concatWith " " (p2s p :: map Int.toString ns)
+
 structure PK = struct
 
 type ord_key = piece
@@ -104,6 +106,12 @@
 
 type env = PS.set PM.map
 
+fun p_env x =
+    (print "\nDENV:\n";
+     PM.appi (fn (p1, ps) =>
+                 PS.app (fn p2 =>
+                            print (rp2s p1 ^ " ~ " ^ rp2s p2 ^ "\n")) ps) x)
+     
 structure E = ElabEnv
 
 type goal = ErrorMsg.span * E.env * env * Elab.con * Elab.con
diff -r 667c0e54632a -r 6ee1c761818f src/elaborate.sml
--- a/src/elaborate.sml	Sat Nov 08 12:24:23 2008 -0500
+++ b/src/elaborate.sml	Sat Nov 08 13:15:00 2008 -0500
@@ -3424,7 +3424,7 @@
                                                  [("loc", PD.string (ErrorMsg.spanToString loc)),
                                                   ("c1", p_con env c1),
                                                   ("c2", p_con env c2)];
-                                        raise Fail "Unresolve constraint in top.ur"))
+                                        raise Fail "Unresolved constraint in top.ur"))
                                 | TypeClass _ => raise Fail "Unresolved type class constraint in top.ur") gs
         val () = subSgn (env', D.empty) topSgn' topSgn
 
diff -r 667c0e54632a -r 6ee1c761818f src/urweb.grm
--- a/src/urweb.grm	Sat Nov 08 12:24:23 2008 -0500
+++ b/src/urweb.grm	Sat Nov 08 13:15:00 2008 -0500
@@ -625,11 +625,11 @@
                                                   ((CAbs (SYMBOL, SOME kind, c), loc),
                                                    (KArrow (kind, k), loc))
                                               end)
-       | LBRACK cterm TWIDDLE cterm RBRACK (fn (c, k) =>
+       | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) =>
                                             let
                                                 val loc = s (LBRACKleft, RBRACKright)
                                             in
-                                                ((CDisjoint (cterm1, cterm2, c), loc),
+                                                ((CDisjoint (cexp1, cexp2, c), loc),
                                                  k)
                                             end)
 
@@ -810,19 +810,19 @@
                                                 ((EAbs ("_", SOME cexp, e), loc),
                                                  (TFun (cexp, t), loc))
                                             end)
-       | LPAREN cterm TWIDDLE cterm RPAREN(fn (e, t) =>
+       | LPAREN cexp TWIDDLE cexp RPAREN  (fn (e, t) =>
                                             let
                                                 val loc = s (LPARENleft, RPARENright)
                                             in
-                                                ((EDisjoint (cterm1, cterm2, e), loc),
-                                                 (CDisjoint (cterm1, cterm2, t), loc))
+                                                ((EDisjoint (cexp1, cexp2, e), loc),
+                                                 (CDisjoint (cexp1, cexp2, t), loc))
                                             end)
-       | LBRACK cterm TWIDDLE cterm RBRACK(fn (e, t) =>
+       | LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) =>
                                             let
                                                 val loc = s (LBRACKleft, RBRACKright)
                                             in
-                                                ((EDisjoint (cterm1, cterm2, e), loc),
-                                                 (CDisjoint (cterm1, cterm2, t), loc))
+                                                ((EDisjoint (cexp1, cexp2, e), loc),
+                                                 (CDisjoint (cexp1, cexp2, t), loc))
                                             end)
 
 eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))