Mercurial > urweb

comparison src/explify.sml @ 82:b4f2a258e52c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial disjointness prover
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 10:55:38 -0400
parents 522f4bd3955e
children e86370850c30
comparison
equal deleted inserted replaced
81:60d97de1bbe8 82:b4f2a258e52c
36 L.KType => (L'.KType, loc) 36 L.KType => (L'.KType, loc)
37 | L.KArrow (k1, k2) => (L'.KArrow (explifyKind k1, explifyKind k2), loc) 37 | L.KArrow (k1, k2) => (L'.KArrow (explifyKind k1, explifyKind k2), loc)
38 | L.KName => (L'.KName, loc) 38 | L.KName => (L'.KName, loc)
39 | L.KRecord k => (L'.KRecord (explifyKind k), loc) 39 | L.KRecord k => (L'.KRecord (explifyKind k), loc)
40 40
41 | L.KUnit => raise Fail "Explify KUnit"
42
41 | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc) 43 | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc)
42 | L.KUnif (_, _, ref (SOME k)) => explifyKind k 44 | L.KUnif (_, _, ref (SOME k)) => explifyKind k
43 | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc) 45 | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
44 46
45 fun explifyCon (c, loc) = 47 fun explifyCon (c, loc) =
58 | L.CName s => (L'.CName s, loc) 60 | L.CName s => (L'.CName s, loc)
59 61
60 | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc) 62 | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc)
61 | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc) 63 | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc)
62 | L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc) 64 | L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc)
65
66 | L.CUnit => raise Fail "Explify CUnit"
63 67
64 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) 68 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
65 | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c 69 | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c
66 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) 70 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
67 71