Mercurial > urweb
changeset 478:6ee1c761818f
Some small changes while failing to write [restrict]
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 08 Nov 2008 13:15:00 -0500 |
| parents | 667c0e54632a |
| children | ffa18975e661 |
| files | src/disjoint.sig src/disjoint.sml src/elaborate.sml src/urweb.grm |
| diffstat | 4 files changed, 19 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- 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
--- 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
--- 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
--- 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))