Mercurial > urweb

comparison src/explify.sml @ 624:354800878b4d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)