diff 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
line wrap: on
line diff
--- a/src/explify.sml	Sun Feb 22 16:10:25 2009 -0500
+++ b/src/explify.sml	Sun Feb 22 16:32:56 2009 -0500
@@ -45,6 +45,9 @@
       | L.KUnif (_, _, ref (SOME k)) => explifyKind k
       | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
 
+      | L.KRel n => (L'.KRel n, loc)
+      | L.KFun (x, k) => (L'.KFun (x, explifyKind k), loc)
+
 fun explifyCon (c, loc) =
     case c of
         L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
@@ -74,6 +77,10 @@
       | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c
       | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
 
+      | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc)
+      | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc)
+      | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc)
+
 fun explifyPatCon pc =
     case pc of
         L.PConVar n => L'.PConVar n
@@ -123,6 +130,9 @@
                     | L.EDVal (x, t, e') => (L'.ELet (x, explifyCon t, explifyExp e', e), loc))
         (explifyExp e) des
 
+      | L.EKAbs (x, e) => (L'.EKAbs (x, explifyExp e), loc)
+      | L.EKApp (e, k) => (L'.EKApp (explifyExp e, explifyKind k), loc)
+
 fun explifySgi (sgi, loc) =
     case sgi of
         L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)