Mercurial > urweb

comparison src/explify.sml @ 1639:6c00d8af6239

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add a new scoping check for unification variables, to fix a type inference bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 11:29:13 -0500
parents c7b9a33c26c8
children bb942416bf1c
comparison
equal deleted inserted replaced
1638:3bf727a08db8 1639:6c00d8af6239
40 40
41 | L.KUnit => (L'.KUnit, loc) 41 | L.KUnit => (L'.KUnit, loc)
42 | L.KTuple ks => (L'.KTuple (map explifyKind ks), loc) 42 | L.KTuple ks => (L'.KTuple (map explifyKind ks), loc)
43 43
44 | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc) 44 | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc)
45 | L.KUnif (_, _, ref (SOME k)) => explifyKind k 45 | L.KUnif (_, _, ref (L.KKnown k)) => explifyKind k
46 | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc) 46 | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
47 | L.KTupleUnif (loc, _, ref (SOME k)) => explifyKind k 47 | L.KTupleUnif (loc, _, ref (L.KKnown k)) => explifyKind k
48 | L.KTupleUnif _ => raise Fail ("explifyKind: KTupleUnif at " ^ EM.spanToString loc) 48 | L.KTupleUnif _ => raise Fail ("explifyKind: KTupleUnif at " ^ EM.spanToString loc)
49 49
50 | L.KRel n => (L'.KRel n, loc) 50 | L.KRel n => (L'.KRel n, loc)
51 | L.KFun (x, k) => (L'.KFun (x, explifyKind k), loc) 51 | L.KFun (x, k) => (L'.KFun (x, explifyKind k), loc)
52 52
74 74
75 | L.CTuple cs => (L'.CTuple (map explifyCon cs), loc) 75 | L.CTuple cs => (L'.CTuple (map explifyCon cs), loc)
76 | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc) 76 | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc)
77 77
78 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) 78 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
79 | L.CUnif (nl, _, _, _, ref (SOME c)) => explifyCon (ElabEnv.mliftConInCon nl c) 79 | L.CUnif (nl, _, _, _, ref (L.Known c)) => explifyCon (ElabEnv.mliftConInCon nl c)
80 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) 80 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
81 81
82 | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc) 82 | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc)
83 | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc) 83 | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc)
84 | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc) 84 | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc)