summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-08 13:15:00 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-08 13:15:00 -0500
commit901b6d55e625be136ddd677a3d8a36e5068de2ae (patch)
treee8e154d621a2dcea385de57280730d135b25466e
parent91ac4dd03f4130e5e416d495d53237b74a37efc1 (diff)
Some small changes while failing to write [restrict]
-rw-r--r--src/disjoint.sig2
-rw-r--r--src/disjoint.sml8
-rw-r--r--src/elaborate.sml2
-rw-r--r--src/urweb.grm16
4 files changed, 19 insertions, 9 deletions
diff --git a/src/disjoint.sig b/src/disjoint.sig
index 025269cf..0d6793c5 100644
--- a/src/disjoint.sig
+++ b/src/disjoint.sig
@@ -40,4 +40,6 @@ signature DISJOINT = sig
val hnormCon : ElabEnv.env * env -> Elab.con -> Elab.con * goal list
+ val p_env : env -> unit
+
end
diff --git a/src/disjoint.sml b/src/disjoint.sml
index 808d8413..c6a8d50f 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -53,6 +53,8 @@ fun p2s p =
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 @@ structure PM = BinaryMapFn(PK)
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 --git a/src/elaborate.sml b/src/elaborate.sml
index e84f5307..17133d93 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3424,7 +3424,7 @@ fun elabFile basis topStr topSgn env file =
[("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 --git a/src/urweb.grm b/src/urweb.grm
index f344633d..5241ed20 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -625,11 +625,11 @@ cargp : SYMBOL (fn (c, k) =>
((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 @@ eargp : SYMBOL (fn (e, t) =>
((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))