Mercurial > urweb
changeset 624:354800878b4d
Kind polymorphism through Explify
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 22 Feb 2009 16:32:56 -0500 |
| parents | 588b9d16b00a |
| children | 47947d6e9750 |
| files | src/elab_print.sml src/expl.sml src/expl_env.sig src/expl_env.sml src/expl_print.sig src/expl_print.sml src/expl_util.sig src/expl_util.sml src/explify.sml |
| diffstat | 9 files changed, 243 insertions(+), 113 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_print.sml Sun Feb 22 16:10:25 2009 -0500 +++ b/src/elab_print.sml Sun Feb 22 16:32:56 2009 -0500 @@ -68,7 +68,7 @@ space, p_kind (E.pushKRel env x) k] -and p_kind k = p_kind' false k +and p_kind env = p_kind' false env fun p_explicitness e = case e of
--- a/src/expl.sml Sun Feb 22 16:10:25 2009 -0500 +++ b/src/expl.sml Sun Feb 22 16:32:56 2009 -0500 @@ -37,6 +37,9 @@ | KTuple of kind list | KRecord of kind + | KRel of int + | KFun of string * kind + withtype kind = kind' located datatype con' = @@ -50,6 +53,10 @@ | CApp of con * con | CAbs of string * kind * con + | CKAbs of string * con + | CKApp of con * kind + | TKFun of string * con + | CName of string | CRecord of kind * (con * con) list @@ -88,6 +95,9 @@ | ECApp of exp * con | ECAbs of string * kind * exp + | EKAbs of string * exp + | EKApp of exp * kind + | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } | EConcat of exp * con * exp * con
--- a/src/expl_env.sig Sun Feb 22 16:10:25 2009 -0500 +++ b/src/expl_env.sig Sun Feb 22 16:32:56 2009 -0500 @@ -42,6 +42,9 @@ | Rel of int * 'a | Named of int * 'a + val pushKRel : env -> string -> env + val lookupKRel : env -> int -> string + val pushCRel : env -> string -> Expl.kind -> env val lookupCRel : env -> int -> string * Expl.kind
--- a/src/expl_env.sml Sun Feb 22 16:10:25 2009 -0500 +++ b/src/expl_env.sml Sun Feb 22 16:32:56 2009 -0500 @@ -45,8 +45,32 @@ exception SynUnif +val liftKindInKind = + U.Kind.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + bind = fn (bound, _) => bound + 1} + +val liftKindInCon = + U.Con.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + con = fn _ => fn c => c, + bind = fn (bound, U.Con.RelK _) => bound + 1 + | (bound, _) => bound} + val liftConInCon = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn bound => fn c => case c of CRel xn => @@ -56,7 +80,7 @@ CRel (xn + 1) (*| CUnif _ => raise SynUnif*) | _ => c, - bind = fn (bound, U.Con.Rel _) => bound + 1 + bind = fn (bound, U.Con.RelC _) => bound + 1 | (bound, _) => bound} val lift = liftConInCon 0 @@ -74,77 +98,82 @@ | Named of int * 'a type env = { - renameC : kind var' SM.map, + relK : string list, + relC : (string * kind) list, namedC : (string * kind * con option) IM.map, - renameE : con var' SM.map, relE : (string * con) list, namedE : (string * con) IM.map, - renameSgn : (int * sgn) SM.map, sgn : (string * sgn) IM.map, - renameStr : (int * sgn) SM.map, str : (string * sgn) IM.map } val namedCounter = ref 0 val empty = { - renameC = SM.empty, + relK = [], + relC = [], namedC = IM.empty, - renameE = SM.empty, relE = [], namedE = IM.empty, - renameSgn = SM.empty, sgn = IM.empty, - renameStr = SM.empty, str = IM.empty } +fun pushKRel (env : env) x = + {relK = x :: #relK env, + + relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env), + namedC = #namedC env, + + relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env), + namedE = #namedE env, + + sgn = #sgn env, + + str = #str env + } + +fun lookupKRel (env : env) n = + (List.nth (#relK env, n)) + handle Subscript => raise UnboundRel n + fun pushCRel (env : env) x k = - let - val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) - | x => x) (#renameC env) - in - {renameC = SM.insert (renameC, x, Rel' (0, k)), - relC = (x, k) :: #relC env, - namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), + {relK = #relK env, - renameE = #renameE env, - relE = map (fn (x, c) => (x, lift c)) (#relE env), - namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), + relC = (x, k) :: #relC env, + namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), - renameSgn = #renameSgn env, - sgn = #sgn env, + relE = map (fn (x, c) => (x, lift c)) (#relE env), + namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), - renameStr = #renameStr env, - str = #str env - } - end + sgn = #sgn env, + + str = #str env + } fun lookupCRel (env : env) n = (List.nth (#relC env, n)) handle Subscript => raise UnboundRel n fun pushCNamed (env : env) x n k co = - {renameC = SM.insert (#renameC env, x, Named' (n, k)), + {relK = #relK env, + relC = #relC env, namedC = IM.insert (#namedC env, n, (x, k, co)), - renameE = #renameE env, relE = #relE env, namedE = #namedE env, - renameSgn = #renameSgn env, sgn = #sgn env, - renameStr = #renameStr env, str = #str env} fun lookupCNamed (env : env) n = @@ -153,42 +182,33 @@ | SOME x => x fun pushERel (env : env) x t = - let - val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) - | x => x) (#renameE env) - in - {renameC = #renameC env, - relC = #relC env, - namedC = #namedC env, + {relK = #relK env, - renameE = SM.insert (renameE, x, Rel' (0, t)), - relE = (x, t) :: #relE env, - namedE = #namedE env, + relC = #relC env, + namedC = #namedC env, - renameSgn = #renameSgn env, - sgn = #sgn env, + relE = (x, t) :: #relE env, + namedE = #namedE env, - renameStr = #renameStr env, - str = #str env} - end + sgn = #sgn env, + + str = #str env} fun lookupERel (env : env) n = (List.nth (#relE env, n)) handle Subscript => raise UnboundRel n fun pushENamed (env : env) x n t = - {renameC = #renameC env, + {relK = #relK env, + relC = #relC env, namedC = #namedC env, - renameE = SM.insert (#renameE env, x, Named' (n, t)), relE = #relE env, namedE = IM.insert (#namedE env, n, (x, t)), - renameSgn = #renameSgn env, sgn = #sgn env, - renameStr = #renameStr env, str = #str env} fun lookupENamed (env : env) n = @@ -197,18 +217,16 @@ | SOME x => x fun pushSgnNamed (env : env) x n sgis = - {renameC = #renameC env, + {relK = #relK env, + relC = #relC env, namedC = #namedC env, - renameE = #renameE env, relE = #relE env, namedE = #namedE env, - renameSgn = SM.insert (#renameSgn env, x, (n, sgis)), sgn = IM.insert (#sgn env, n, (x, sgis)), - renameStr = #renameStr env, str = #str env} fun lookupSgnNamed (env : env) n = @@ -217,18 +235,16 @@ | SOME x => x fun pushStrNamed (env : env) x n sgis = - {renameC = #renameC env, + {relK = #relK env, + relC = #relC env, namedC = #namedC env, - renameE = #renameE env, relE = #relE env, namedE = #namedE env, - renameSgn = #renameSgn env, sgn = #sgn env, - renameStr = SM.insert (#renameStr env, x, (n, sgis)), str = IM.insert (#str env, n, (x, sgis))} fun lookupStrNamed (env : env) n =
--- a/src/expl_print.sig Sun Feb 22 16:10:25 2009 -0500 +++ b/src/expl_print.sig Sun Feb 22 16:32:56 2009 -0500 @@ -26,7 +26,7 @@ *) signature EXPL_PRINT = sig - val p_kind : Expl.kind Print.printer + val p_kind : ExplEnv.env -> Expl.kind Print.printer val p_con : ExplEnv.env -> Expl.con Print.printer val p_exp : ExplEnv.env -> Expl.exp Print.printer val p_decl : ExplEnv.env -> Expl.decl Print.printer
--- a/src/expl_print.sml Sun Feb 22 16:10:25 2009 -0500 +++ b/src/expl_print.sml Sun Feb 22 16:32:56 2009 -0500 @@ -38,22 +38,33 @@ val debug = ref false -fun p_kind' par (k, _) = +fun p_kind' par env (k, _) = case k of KType => string "Type" - | KArrow (k1, k2) => parenIf par (box [p_kind' true k1, + | KArrow (k1, k2) => parenIf par (box [p_kind' true env k1, space, string "->", space, - p_kind k2]) + p_kind env k2]) | KName => string "Name" - | KRecord k => box [string "{", p_kind k, string "}"] + | KRecord k => box [string "{", p_kind env k, string "}"] | KUnit => string "Unit" | KTuple ks => box [string "(", - p_list_sep (box [space, string "*", space]) p_kind ks, + p_list_sep (box [space, string "*", space]) (p_kind env) ks, string ")"] -and p_kind k = p_kind' false k + | KRel n => ((if !debug then + string (E.lookupKRel env n ^ "_" ^ Int.toString n) + else + string (E.lookupKRel env n)) + handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n)) + | KFun (x, k) => box [string x, + space, + string "-->", + space, + p_kind (E.pushKRel env x) k] + +and p_kind env = p_kind' false env fun p_con' par env (c, _) = case c of @@ -66,7 +77,7 @@ space, string "::", space, - p_kind k, + p_kind env k, space, string "->", space, @@ -116,7 +127,7 @@ space, string "::", space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -134,7 +145,7 @@ space, p_con env c]) xcs, string "]::", - p_kind k]) + p_kind env k]) else parenIf par (box [string "[", p_list (fn (x, c) => @@ -158,6 +169,21 @@ | CProj (c, n) => box [p_con env c, string ".", string (Int.toString n)] + + | CKAbs (x, c) => box [string x, + space, + string "==>", + space, + p_con (E.pushKRel env x) c] + | CKApp (c, k) => box [p_con env c, + string "[[", + p_kind env k, + string "]]"] + | TKFun (x, c) => box [string x, + space, + string "-->", + space, + p_con (E.pushKRel env x) c] and p_con env = p_con' false env @@ -261,7 +287,7 @@ space, string "::", space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -397,6 +423,15 @@ newline, p_exp (E.pushERel env x t) e2] + | EKAbs (x, e) => box [string x, + space, + string "==>", + space, + p_exp (E.pushKRel env x) e] + | EKApp (e, k) => box [p_exp env e, + string "[[", + p_kind env k, + string "]]"] and p_exp env = p_exp' false env @@ -438,14 +473,14 @@ space, string "::", space, - p_kind k] + p_kind env k] | SgiCon (x, n, k, c) => box [string "con", space, p_named x n, space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -559,7 +594,7 @@ space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space,
--- a/src/expl_util.sig Sun Feb 22 16:10:25 2009 -0500 +++ b/src/expl_util.sig Sun Feb 22 16:32:56 2009 -0500 @@ -28,17 +28,24 @@ signature EXPL_UTIL = sig structure Kind : sig + val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB, + bind : 'context * string -> 'context} + -> ('context, Expl.kind, 'state, 'abort) Search.mapfolderB val mapfold : (Expl.kind', 'state, 'abort) Search.mapfolder -> (Expl.kind, 'state, 'abort) Search.mapfolder val exists : (Expl.kind' -> bool) -> Expl.kind -> bool + val mapB : {kind : 'context -> Expl.kind' -> Expl.kind', + bind : 'context * string -> 'context} + -> 'context -> (Expl.kind -> Expl.kind) end structure Con : sig datatype binder = - Rel of string * Expl.kind - | Named of string * Expl.kind + RelK of string + | RelC of string * Expl.kind + | NamedC of string * Expl.kind - val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB, bind : 'context * binder -> 'context} -> ('context, Expl.con, 'state, 'abort) Search.mapfolderB @@ -46,7 +53,7 @@ con : (Expl.con', 'state, 'abort) Search.mapfolder} -> (Expl.con, 'state, 'abort) Search.mapfolder - val mapB : {kind : Expl.kind' -> Expl.kind', + val mapB : {kind : 'context -> Expl.kind' -> Expl.kind', con : 'context -> Expl.con' -> Expl.con', bind : 'context * binder -> 'context} -> 'context -> (Expl.con -> Expl.con) @@ -59,12 +66,13 @@ structure Exp : sig datatype binder = - RelC of string * Expl.kind + RelK of string + | RelC of string * Expl.kind | NamedC of string * Expl.kind | RelE of string * Expl.con | NamedE of string * Expl.con - val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB, exp : ('context, Expl.exp', 'state, 'abort) Search.mapfolderB, bind : 'context * binder -> 'context} @@ -80,12 +88,13 @@ structure Sgn : sig datatype binder = - RelC of string * Expl.kind + RelK of string + | RelC of string * Expl.kind | NamedC of string * Expl.kind | Sgn of string * Expl.sgn | Str of string * Expl.sgn - val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB, sgn_item : ('context, Expl.sgn_item', 'state, 'abort) Search.mapfolderB, sgn : ('context, Expl.sgn', 'state, 'abort) Search.mapfolderB,
--- a/src/expl_util.sml Sun Feb 22 16:10:25 2009 -0500 +++ b/src/expl_util.sml Sun Feb 22 16:32:56 2009 -0500 @@ -33,39 +33,55 @@ structure Kind = struct -fun mapfold f = +fun mapfoldB {kind, bind} = let - fun mfk k acc = - S.bindP (mfk' k acc, f) + fun mfk ctx k acc = + S.bindP (mfk' ctx k acc, kind ctx) - and mfk' (kAll as (k, loc)) = + and mfk' ctx (kAll as (k, loc)) = case k of KType => S.return2 kAll | KArrow (k1, k2) => - S.bind2 (mfk k1, + S.bind2 (mfk ctx k1, fn k1' => - S.map2 (mfk k2, + S.map2 (mfk ctx k2, fn k2' => (KArrow (k1', k2'), loc))) | KName => S.return2 kAll | KRecord k => - S.map2 (mfk k, + S.map2 (mfk ctx k, fn k' => (KRecord k', loc)) | KUnit => S.return2 kAll | KTuple ks => - S.map2 (ListUtil.mapfold mfk ks, + S.map2 (ListUtil.mapfold (mfk ctx) ks, fn ks' => (KTuple ks', loc)) + + | KRel _ => S.return2 kAll + | KFun (x, k) => + S.map2 (mfk (bind (ctx, x)) k, + fn k' => + (KFun (x, k'), loc)) in mfk end +fun mapfold fk = + mapfoldB {kind = fn () => fk, + bind = fn ((), _) => ()} () + +fun mapB {kind, bind} ctx k = + case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), + bind = bind} ctx k () of + S.Continue (k, ()) => k + | S.Return _ => raise Fail "ExplUtil.Kind.mapB: Impossible" + fun exists f k = case mapfold (fn k => fn () => if f k then @@ -80,12 +96,13 @@ structure Con = struct datatype binder = - Rel of string * Expl.kind - | Named of string * Expl.kind + RelK of string + | RelC of string * Expl.kind + | NamedC of string * Expl.kind fun mapfoldB {kind = fk, con = fc, bind} = let - val mfk = Kind.mapfold fk + val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)} fun mfc ctx c acc = S.bindP (mfc' ctx c acc, fc ctx) @@ -99,9 +116,9 @@ fn c2' => (TFun (c1', c2'), loc))) | TCFun (x, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => - S.map2 (mfc (bind (ctx, Rel (x, k))) c, + S.map2 (mfc (bind (ctx, RelC (x, k))) c, fn c' => (TCFun (x, k', c'), loc))) | TRecord c => @@ -119,16 +136,16 @@ fn c2' => (CApp (c1', c2'), loc))) | CAbs (x, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => - S.map2 (mfc (bind (ctx, Rel (x, k))) c, + S.map2 (mfc (bind (ctx, RelC (x, k))) c, fn c' => (CAbs (x, k', c'), loc))) | CName _ => S.return2 cAll | CRecord (k, xcs) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (ListUtil.mapfold (fn (x, c) => S.bind2 (mfc ctx x, @@ -146,9 +163,9 @@ fn c2' => (CConcat (c1', c2'), loc))) | CMap (k1, k2) => - S.bind2 (mfk k1, + S.bind2 (mfk ctx k1, fn k1' => - S.map2 (mfk k2, + S.map2 (mfk ctx k2, fn k2' => (CMap (k1', k2'), loc))) @@ -163,17 +180,32 @@ S.map2 (mfc ctx c, fn c' => (CProj (c', n), loc)) + + | CKAbs (x, c) => + S.map2 (mfc (bind (ctx, RelK x)) c, + fn c' => + (CKAbs (x, c'), loc)) + | CKApp (c, k) => + S.bind2 (mfc ctx c, + fn c' => + S.map2 (mfk ctx k, + fn k' => + (CKApp (c', k'), loc))) + | TKFun (x, c) => + S.map2 (mfc (bind (ctx, RelK x)) c, + fn c' => + (TKFun (x, c'), loc)) in mfc end fun mapfold {kind = fk, con = fc} = - mapfoldB {kind = fk, + mapfoldB {kind = fn () => fk, con = fn () => fc, bind = fn ((), _) => ()} () fun mapB {kind, con, bind} ctx c = - case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), + case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), bind = bind} ctx c () of S.Continue (c, ()) => c @@ -204,20 +236,22 @@ structure Exp = struct datatype binder = - RelC of string * Expl.kind + RelK of string + | RelC of string * Expl.kind | NamedC of string * Expl.kind | RelE of string * Expl.con | NamedE of string * Expl.con fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = let - val mfk = Kind.mapfold fk + val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)} fun bind' (ctx, b) = let val b' = case b of - Con.Rel x => RelC x - | Con.Named x => NamedC x + Con.RelK x => RelK x + | Con.RelC x => RelC x + | Con.NamedC x => NamedC x in bind (ctx, b') end @@ -254,7 +288,7 @@ fn c' => (ECApp (e', c'), loc))) | ECAbs (x, k, e) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (mfe (bind (ctx, RelC (x, k))) e, fn e' => @@ -338,12 +372,23 @@ S.map2 (mfe (bind (ctx, RelE (x, t))) e2, fn e2' => (ELet (x, t', e1', e2'), loc)))) + + | EKAbs (x, e) => + S.map2 (mfe (bind (ctx, RelK x)) e, + fn e' => + (EKAbs (x, e'), loc)) + | EKApp (e, k) => + S.bind2 (mfe ctx e, + fn e' => + S.map2 (mfk ctx k, + fn k' => + (EKApp (e', k'), loc))) in mfe end fun mapfold {kind = fk, con = fc, exp = fe} = - mapfoldB {kind = fk, + mapfoldB {kind = fn () => fk, con = fn () => fc, exp = fn () => fe, bind = fn ((), _) => ()} () @@ -372,7 +417,8 @@ structure Sgn = struct datatype binder = - RelC of string * Expl.kind + RelK of string + | RelC of string * Expl.kind | NamedC of string * Expl.kind | Str of string * Expl.sgn | Sgn of string * Expl.sgn @@ -382,14 +428,15 @@ fun bind' (ctx, b) = let val b' = case b of - Con.Rel x => RelC x - | Con.Named x => NamedC x + Con.RelK x => RelK x + | Con.RelC x => RelC x + | Con.NamedC x => NamedC x in bind (ctx, b') end val con = Con.mapfoldB {kind = kind, con = con, bind = bind'} - val kind = Kind.mapfold kind + val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)} fun sgi ctx si acc = S.bindP (sgi' ctx si acc, sgn_item ctx) @@ -397,11 +444,11 @@ and sgi' ctx (siAll as (si, loc)) = case si of SgiConAbs (x, n, k) => - S.map2 (kind k, + S.map2 (kind ctx k, fn k' => (SgiConAbs (x, n, k'), loc)) | SgiCon (x, n, k, c) => - S.bind2 (kind k, + S.bind2 (kind ctx k, fn k' => S.map2 (con ctx c, fn c' => @@ -482,7 +529,7 @@ end fun mapfold {kind, con, sgn_item, sgn} = - mapfoldB {kind = kind, + mapfoldB {kind = fn () => kind, con = fn () => con, sgn_item = fn () => sgn_item, sgn = fn () => sgn,
--- 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)