Mercurial > urweb
comparison src/corify.sml @ 34:44b5405e74c7
Elaborating module projection
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 17 Jun 2008 16:38:54 -0400 |
parents | 1c91c5e6840f |
children | 02f42e9a1825 |
comparison
equal
deleted
inserted
replaced
33:535c324f0b35 | 34:44b5405e74c7 |
---|---|
48 | L.TCFun (_, x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon t), loc) | 48 | L.TCFun (_, x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon t), loc) |
49 | L.TRecord c => (L'.TRecord (corifyCon c), loc) | 49 | L.TRecord c => (L'.TRecord (corifyCon c), loc) |
50 | 50 |
51 | L.CRel n => (L'.CRel n, loc) | 51 | L.CRel n => (L'.CRel n, loc) |
52 | L.CNamed n => (L'.CNamed n, loc) | 52 | L.CNamed n => (L'.CNamed n, loc) |
53 | L.CModProj _ => raise Fail "Corify CModProj" | |
54 | |
53 | L.CApp (c1, c2) => (L'.CApp (corifyCon c1, corifyCon c2), loc) | 55 | L.CApp (c1, c2) => (L'.CApp (corifyCon c1, corifyCon c2), loc) |
54 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon c), loc) | 56 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon c), loc) |
55 | 57 |
56 | L.CName s => (L'.CName s, loc) | 58 | L.CName s => (L'.CName s, loc) |
57 | 59 |
65 fun corifyExp (e, loc) = | 67 fun corifyExp (e, loc) = |
66 case e of | 68 case e of |
67 L.EPrim p => (L'.EPrim p, loc) | 69 L.EPrim p => (L'.EPrim p, loc) |
68 | L.ERel n => (L'.ERel n, loc) | 70 | L.ERel n => (L'.ERel n, loc) |
69 | L.ENamed n => (L'.ENamed n, loc) | 71 | L.ENamed n => (L'.ENamed n, loc) |
72 | L.EModProj _ => raise Fail "Corify EModProj" | |
70 | L.EApp (e1, e2) => (L'.EApp (corifyExp e1, corifyExp e2), loc) | 73 | L.EApp (e1, e2) => (L'.EApp (corifyExp e1, corifyExp e2), loc) |
71 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon dom, corifyCon ran, corifyExp e1), loc) | 74 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon dom, corifyCon ran, corifyExp e1), loc) |
72 | L.ECApp (e1, c) => (L'.ECApp (corifyExp e1, corifyCon c), loc) | 75 | L.ECApp (e1, c) => (L'.ECApp (corifyExp e1, corifyCon c), loc) |
73 | L.ECAbs (_, x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp e1), loc) | 76 | L.ECAbs (_, x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp e1), loc) |
74 | 77 |