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