Mercurial > urweb
comparison src/explify.sml @ 624:354800878b4d
Kind polymorphism through Explify
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 22 Feb 2009 16:32:56 -0500 |
parents | 588b9d16b00a |
children | 12b73f3c108e |
comparison
equal
deleted
inserted
replaced
623:588b9d16b00a | 624:354800878b4d |
---|---|
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 (SOME 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 | 47 |
48 | L.KRel n => (L'.KRel n, loc) | |
49 | L.KFun (x, k) => (L'.KFun (x, explifyKind k), loc) | |
50 | |
48 fun explifyCon (c, loc) = | 51 fun explifyCon (c, loc) = |
49 case c of | 52 case c of |
50 L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc) | 53 L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc) |
51 | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc) | 54 | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc) |
52 | L.CDisjoint (_, _, _, c) => explifyCon c | 55 | L.CDisjoint (_, _, _, c) => explifyCon c |
71 | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc) | 74 | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc) |
72 | 75 |
73 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) | 76 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) |
74 | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c | 77 | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c |
75 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) | 78 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) |
79 | |
80 | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc) | |
81 | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc) | |
82 | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc) | |
76 | 83 |
77 fun explifyPatCon pc = | 84 fun explifyPatCon pc = |
78 case pc of | 85 case pc of |
79 L.PConVar n => L'.PConVar n | 86 L.PConVar n => L'.PConVar n |
80 | L.PConProj x => L'.PConProj x | 87 | L.PConProj x => L'.PConProj x |
120 foldr (fn ((de, loc), e) => | 127 foldr (fn ((de, loc), e) => |
121 case de of | 128 case de of |
122 L.EDValRec _ => raise Fail "explifyExp: Local 'val rec' remains" | 129 L.EDValRec _ => raise Fail "explifyExp: Local 'val rec' remains" |
123 | L.EDVal (x, t, e') => (L'.ELet (x, explifyCon t, explifyExp e', e), loc)) | 130 | L.EDVal (x, t, e') => (L'.ELet (x, explifyCon t, explifyExp e', e), loc)) |
124 (explifyExp e) des | 131 (explifyExp e) des |
132 | |
133 | L.EKAbs (x, e) => (L'.EKAbs (x, explifyExp e), loc) | |
134 | L.EKApp (e, k) => (L'.EKApp (explifyExp e, explifyKind k), loc) | |
125 | 135 |
126 fun explifySgi (sgi, loc) = | 136 fun explifySgi (sgi, loc) = |
127 case sgi of | 137 case sgi of |
128 L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc) | 138 L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc) |
129 | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) | 139 | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) |