diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-11-08 13:15:00 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-11-08 13:15:00 -0500 |
| commit | 901b6d55e625be136ddd677a3d8a36e5068de2ae (patch) | |
| tree | e8e154d621a2dcea385de57280730d135b25466e | |
| parent | 91ac4dd03f4130e5e416d495d53237b74a37efc1 (diff) | |
Some small changes while failing to write [restrict]
| -rw-r--r-- | src/disjoint.sig | 2 | ||||
| -rw-r--r-- | src/disjoint.sml | 8 | ||||
| -rw-r--r-- | src/elaborate.sml | 2 | ||||
| -rw-r--r-- | src/urweb.grm | 16 |
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)) |