Mercurial > urweb
diff src/explify.sml @ 85:1f85890c9846
Disjointness assumptions in expressions
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 01 Jul 2008 12:25:12 -0400 |
parents | e86370850c30 |
children | 275aaeb73f1f |
line wrap: on
line diff
--- a/src/explify.sml Tue Jul 01 12:10:46 2008 -0400 +++ b/src/explify.sml Tue Jul 01 12:25:12 2008 -0400 @@ -48,6 +48,7 @@ case c of L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc) | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc) + | L.TDisjoint (_, _, c) => explifyCon c | L.TRecord c => (L'.TRecord (explifyCon c), loc) | L.CRel n => (L'.CRel n, loc) @@ -56,7 +57,7 @@ | L.CApp (c1, c2) => (L'.CApp (explifyCon c1, explifyCon c2), loc) | L.CAbs (x, k, c) => (L'.CAbs (x, explifyKind k, explifyCon c), loc) - | L.CDisjoint _ => raise Fail "Explify CDisjoint" + | L.CDisjoint (_, _, c) => explifyCon c | L.CName s => (L'.CName s, loc)