Mercurial > urweb

comparison src/explify.sml @ 85:1f85890c9846

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Disjointness assumptions in expressions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 12:25:12 -0400
parents e86370850c30
children 275aaeb73f1f
comparison
equal deleted inserted replaced
84:e86370850c30 85:1f85890c9846
46 46
47 fun explifyCon (c, loc) = 47 fun explifyCon (c, loc) =
48 case c of 48 case c of
49 L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc) 49 L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
50 | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc) 50 | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc)
51 | L.TDisjoint (_, _, c) => explifyCon c
51 | L.TRecord c => (L'.TRecord (explifyCon c), loc) 52 | L.TRecord c => (L'.TRecord (explifyCon c), loc)
52 53
53 | L.CRel n => (L'.CRel n, loc) 54 | L.CRel n => (L'.CRel n, loc)
54 | L.CNamed n => (L'.CNamed n, loc) 55 | L.CNamed n => (L'.CNamed n, loc)
55 | L.CModProj (m, ms, x) => (L'.CModProj (m, ms, x), loc) 56 | L.CModProj (m, ms, x) => (L'.CModProj (m, ms, x), loc)
56 57
57 | L.CApp (c1, c2) => (L'.CApp (explifyCon c1, explifyCon c2), loc) 58 | L.CApp (c1, c2) => (L'.CApp (explifyCon c1, explifyCon c2), loc)
58 | L.CAbs (x, k, c) => (L'.CAbs (x, explifyKind k, explifyCon c), loc) 59 | L.CAbs (x, k, c) => (L'.CAbs (x, explifyKind k, explifyCon c), loc)
59 | L.CDisjoint _ => raise Fail "Explify CDisjoint" 60 | L.CDisjoint (_, _, c) => explifyCon c
60 61
61 | L.CName s => (L'.CName s, loc) 62 | L.CName s => (L'.CName s, loc)
62 63
63 | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc) 64 | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc)
64 | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc) 65 | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc)