From 85c5fc291ece27b13a28a3ec50b67ff437a18834 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 22 Feb 2009 16:32:56 -0500 Subject: Kind polymorphism through Explify --- src/explify.sml | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/explify.sml') diff --git a/src/explify.sml b/src/explify.sml index 5bce9268..b2564789 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -45,6 +45,9 @@ fun explifyKind (k, loc) = | 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 @@ fun explifyCon (c, loc) = | 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 @@ fun explifyExp (e, loc) = | 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) -- cgit v1.2.3