From 1f7d0c20ae30c11cdc64a2c2fc90f15cdf02c34b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 22 Feb 2009 17:17:01 -0500 Subject: demo/hello compiles with kind polymorphism --- src/core.sml | 10 ++++ src/core_env.sig | 3 + src/core_env.sml | 95 +++++++++++++++++++++++++---- src/core_print.sig | 2 +- src/core_print.sml | 58 ++++++++++++++---- src/core_util.sig | 36 ++++++----- src/core_util.sml | 166 +++++++++++++++++++++++++++++++++++++-------------- src/corify.sml | 9 +++ src/defunc.sml | 9 +-- src/especialize.sml | 9 ++- src/monoize.sml | 7 +++ src/reduce.sml | 138 ++++++++++++++++++++++++++++++++---------- src/reduce_local.sml | 4 +- 13 files changed, 420 insertions(+), 126 deletions(-) (limited to 'src') diff --git a/src/core.sml b/src/core.sml index a28d93dd..b384c576 100644 --- a/src/core.sml +++ b/src/core.sml @@ -37,6 +37,9 @@ datatype kind' = | KUnit | KTuple of kind list + | KRel of int + | KFun of string * kind + withtype kind = kind' located datatype con' = @@ -50,6 +53,10 @@ datatype con' = | 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 @@ -91,6 +98,9 @@ datatype exp' = | 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 diff --git a/src/core_env.sig b/src/core_env.sig index 98e345cc..6b954c12 100644 --- a/src/core_env.sig +++ b/src/core_env.sig @@ -43,6 +43,9 @@ signature CORE_ENV = sig exception UnboundRel of int exception UnboundNamed of int + val pushKRel : env -> string -> env + val lookupKRel : env -> int -> string + val pushCRel : env -> string -> Core.kind -> env val lookupCRel : env -> int -> string * Core.kind diff --git a/src/core_env.sml b/src/core_env.sml index 07162606..2c100aa5 100644 --- a/src/core_env.sml +++ b/src/core_env.sml @@ -36,8 +36,46 @@ structure IM = IntBinaryMap (* AST utility functions *) +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 liftKindInExp = + U.Exp.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, + exp = fn _ => fn e => e, + bind = fn (bound, U.Exp.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 => @@ -46,13 +84,13 @@ val liftConInCon = else CRel (xn + 1) | _ => c, - bind = fn (bound, U.Con.Rel _) => bound + 1 + bind = fn (bound, U.Con.RelC _) => bound + 1 | (bound, _) => bound} val lift = liftConInCon 0 val subConInCon = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn (xn, rep) => fn c => case c of CRel xn' => @@ -61,12 +99,12 @@ val subConInCon = | GREATER => CRel (xn' - 1) | LESS => c) | _ => c, - bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) + bind = fn ((xn, rep), U.Con.RelC _) => (xn+1, liftConInCon 0 rep) | (ctx, _) => ctx} val liftConInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn bound => fn c => case c of CRel xn => @@ -80,7 +118,7 @@ val liftConInExp = | (bound, _) => bound} val subConInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn (xn, rep) => fn c => case c of CRel xn' => @@ -94,7 +132,7 @@ val subConInExp = | (ctx, _) => ctx} val liftExpInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn bound => fn e => case e of @@ -108,7 +146,7 @@ val liftExpInExp = | (bound, _) => bound} val subExpInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn (xn, rep) => fn e => case e of @@ -128,6 +166,8 @@ exception UnboundRel of int exception UnboundNamed of int type env = { + relK : string list, + relC : (string * kind) list, namedC : (string * kind * con option) IM.map, @@ -139,6 +179,8 @@ type env = { } val empty = { + relK = [], + relC = [], namedC = IM.empty, @@ -149,8 +191,27 @@ val empty = { namedE = 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, + + datatypes = #datatypes env, + constructors = #constructors env + } + +fun lookupKRel (env : env) n = + (List.nth (#relK env, n)) + handle Subscript => raise UnboundRel n + fun pushCRel (env : env) x k = - {relC = (x, k) :: #relC env, + {relK = #relK env, + + relC = (x, k) :: #relC env, namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), datatypes = #datatypes env, @@ -164,7 +225,9 @@ fun lookupCRel (env : env) n = handle Subscript => raise UnboundRel n fun pushCNamed (env : env) x n k co = - {relC = #relC env, + {relK = #relK env, + + relC = #relC env, namedC = IM.insert (#namedC env, n, (x, k, co)), datatypes = #datatypes env, @@ -179,7 +242,9 @@ fun lookupCNamed (env : env) n = | SOME x => x fun pushDatatype (env : env) x n xs xncs = - {relC = #relC env, + {relK = #relK env, + + relC = #relC env, namedC = #namedC env, datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)), @@ -201,7 +266,9 @@ fun lookupConstructor (env : env) n = | SOME x => x fun pushERel (env : env) x t = - {relC = #relC env, + {relK = #relK env, + + relC = #relC env, namedC = #namedC env, datatypes = #datatypes env, @@ -215,7 +282,9 @@ fun lookupERel (env : env) n = handle Subscript => raise UnboundRel n fun pushENamed (env : env) x n t eo s = - {relC = #relC env, + {relK = #relK env, + + relC = #relC env, namedC = #namedC env, datatypes = #datatypes env, diff --git a/src/core_print.sig b/src/core_print.sig index 38a51aef..64a73a46 100644 --- a/src/core_print.sig +++ b/src/core_print.sig @@ -28,7 +28,7 @@ (* Pretty-printing Ur/Web internal language *) signature CORE_PRINT = sig - val p_kind : Core.kind Print.printer + val p_kind : CoreEnv.env -> Core.kind Print.printer val p_con : CoreEnv.env -> Core.con Print.printer val p_pat : CoreEnv.env -> Core.pat Print.printer val p_exp : CoreEnv.env -> Core.exp Print.printer diff --git a/src/core_print.sml b/src/core_print.sml index 504773ab..cc6e5428 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -38,22 +38,33 @@ structure E = CoreEnv 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 @@ fun p_con' par env (c, _) = space, string "::", space, - p_kind k, + p_kind env k, space, string "->", space, @@ -105,7 +116,7 @@ fun p_con' par env (c, _) = space, string "::", space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -123,7 +134,7 @@ fun p_con' par env (c, _) = space, p_con env c]) xcs, string "]::", - p_kind k]) + p_kind env k]) else parenIf par (box [string "[", p_list (fn (x, c) => @@ -147,6 +158,21 @@ fun p_con' par env (c, _) = | 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 @@ -252,7 +278,7 @@ fun p_exp' par env (e, _) = space, string "::", space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -402,6 +428,16 @@ fun p_exp' par env (e, _) = p_exp env e, string "]"] + | 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 fun p_named x n = @@ -480,7 +516,7 @@ fun p_decl env (dAll as (d, _) : decl) = space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, diff --git a/src/core_util.sig b/src/core_util.sig index fc5a2bea..fabb9878 100644 --- a/src/core_util.sig +++ b/src/core_util.sig @@ -30,20 +30,27 @@ signature CORE_UTIL = sig structure Kind : sig val compare : Core.kind * Core.kind -> order + val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB, + bind : 'context * string -> 'context} + -> ('context, Core.kind, 'state, 'abort) Search.mapfolderB val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder -> (Core.kind, 'state, 'abort) Search.mapfolder val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind val exists : (Core.kind' -> bool) -> Core.kind -> bool + val mapB : {kind : 'context -> Core.kind' -> Core.kind', + bind : 'context * string -> 'context} + -> 'context -> (Core.kind -> Core.kind) end structure Con : sig val compare : Core.con * Core.con -> order datatype binder = - Rel of string * Core.kind - | Named of string * int * Core.kind * Core.con option + RelK of string + | RelC of string * Core.kind + | NamedC of string * int * Core.kind * Core.con option - val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, bind : 'context * binder -> 'context} -> ('context, Core.con, 'state, 'abort) Search.mapfolderB @@ -55,7 +62,7 @@ structure Con : sig con : Core.con' -> Core.con'} -> Core.con -> Core.con - val mapB : {kind : Core.kind' -> Core.kind', + val mapB : {kind : 'context -> Core.kind' -> Core.kind', con : 'context -> Core.con' -> Core.con', bind : 'context * binder -> 'context} -> 'context -> (Core.con -> Core.con) @@ -76,12 +83,13 @@ structure Exp : sig val compare : Core.exp * Core.exp -> order datatype binder = - RelC of string * Core.kind + RelK of string + | RelC of string * Core.kind | NamedC of string * int * Core.kind * Core.con option | RelE of string * Core.con | NamedE of string * int * Core.con * Core.exp option * string - val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB, bind : 'context * binder -> 'context} @@ -95,7 +103,7 @@ structure Exp : sig con : Core.con' -> Core.con', exp : Core.exp' -> Core.exp'} -> Core.exp -> Core.exp - val mapB : {kind : Core.kind' -> Core.kind', + val mapB : {kind : 'context -> Core.kind' -> Core.kind', con : 'context -> Core.con' -> Core.con', exp : 'context -> Core.exp' -> Core.exp', bind : 'context * binder -> 'context} @@ -106,7 +114,7 @@ structure Exp : sig exp : Core.exp' * 'state -> 'state} -> 'state -> Core.exp -> 'state - val foldB : {kind : Core.kind' * 'state -> 'state, + val foldB : {kind : 'context * Core.kind' * 'state -> 'state, con : 'context * Core.con' * 'state -> 'state, exp : 'context * Core.exp' * 'state -> 'state, bind : 'context * binder -> 'context} @@ -116,7 +124,7 @@ structure Exp : sig con : Core.con' -> bool, exp : Core.exp' -> bool} -> Core.exp -> bool - val existsB : {kind : Core.kind' -> bool, + val existsB : {kind : 'context * Core.kind' -> bool, con : 'context * Core.con' -> bool, exp : 'context * Core.exp' -> bool, bind : 'context * binder -> 'context} @@ -126,7 +134,7 @@ structure Exp : sig con : Core.con' * 'state -> Core.con' * 'state, exp : Core.exp' * 'state -> Core.exp' * 'state} -> 'state -> Core.exp -> Core.exp * 'state - val foldMapB : {kind : Core.kind' * 'state -> Core.kind' * 'state, + val foldMapB : {kind : 'context * Core.kind' * 'state -> Core.kind' * 'state, con : 'context * Core.con' * 'state -> Core.con' * 'state, exp : 'context * Core.exp' * 'state -> Core.exp' * 'state, bind : 'context * binder -> 'context} @@ -136,7 +144,7 @@ end structure Decl : sig datatype binder = datatype Exp.binder - val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB, decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB, @@ -159,7 +167,7 @@ structure Decl : sig exp : Core.exp' * 'state -> Core.exp' * 'state, decl : Core.decl' * 'state -> Core.decl' * 'state} -> 'state -> Core.decl -> Core.decl * 'state - val foldMapB : {kind : Core.kind' * 'state -> Core.kind' * 'state, + val foldMapB : {kind : 'context * Core.kind' * 'state -> Core.kind' * 'state, con : 'context * Core.con' * 'state -> Core.con' * 'state, exp : 'context * Core.exp' * 'state -> Core.exp' * 'state, decl : 'context * Core.decl' * 'state -> Core.decl' * 'state, @@ -177,7 +185,7 @@ structure File : sig datatype binder = datatype Exp.binder - val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB, decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB, @@ -190,7 +198,7 @@ structure File : sig decl : (Core.decl', 'state, 'abort) Search.mapfolder} -> (Core.file, 'state, 'abort) Search.mapfolder - val mapB : {kind : Core.kind' -> Core.kind', + val mapB : {kind : 'context -> Core.kind' -> Core.kind', con : 'context -> Core.con' -> Core.con', exp : 'context -> Core.exp' -> Core.exp', decl : 'context -> Core.decl' -> Core.decl', diff --git a/src/core_util.sml b/src/core_util.sml index d5f8dd05..b1d07b79 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -58,45 +58,69 @@ fun compare ((k1, _), (k2, _)) = | (_, KUnit) => GREATER | (KTuple ks1, KTuple ks2) => joinL compare (ks1, ks2) + | (KTuple _, _) => LESS + | (_, KTuple _) => GREATER -fun mapfold f = + | (KRel n1, KRel n2) => Int.compare (n1, n2) + | (KRel _, _) => LESS + | (_, KRel _) => GREATER + + | (KFun (_, k1), KFun (_, k2)) => compare (k1, k2) + +fun mapfoldB {kind = f, bind} = let - fun mfk k acc = - S.bindP (mfk' k acc, f) + fun mfk ctx k acc = + S.bindP (mfk' ctx k acc, f 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 map f k = case mapfold (fn k => fn () => S.Continue (f k, ())) k () of - S.Return () => raise Fail "Core_util.Kind.map" + S.Return () => raise Fail "CoreUtil.Kind.map" | S.Continue (k, ()) => k +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 "CoreUtil.Kind.mapB: Impossible" + fun exists f k = case mapfold (fn k => fn () => if f k then @@ -194,14 +218,29 @@ fun compare ((c1, _), (c2, _)) = | (CProj (c1, n1), CProj (c2, n2)) => join (Int.compare (n1, n2), fn () => compare (c1, c2)) + | (CProj _, _) => LESS + | (_, CProj _) => GREATER + + | (CKAbs (_, c1), CKAbs (_, c2)) => compare (c1, c2) + | (CKAbs _, _) => LESS + | (_, CKAbs _) => GREATER + + | (CKApp (c1, k1), CKApp (c2, k2)) => + join (compare (c1, c2), + fn () => Kind.compare (k1, k2)) + | (CKApp _, _) => LESS + | (_, CKApp _) => GREATER + + | (TKFun (_, c1), TKFun (_, c2)) => compare (c1, c2) datatype binder = - Rel of string * kind - | Named of string * int * kind * con option + RelK of string + | RelC of string * kind + | NamedC of string * int * kind * con option 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) @@ -215,9 +254,9 @@ fun mapfoldB {kind = fk, con = fc, bind} = 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 => @@ -235,16 +274,16 @@ fun mapfoldB {kind = fk, con = fc, bind} = 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, @@ -262,9 +301,9 @@ fun mapfoldB {kind = fk, con = fc, bind} = 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))) @@ -279,12 +318,27 @@ fun mapfoldB {kind = fk, con = fc, bind} = 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 ((), _) => ()} () @@ -295,7 +349,7 @@ fun map {kind, con} c = | S.Continue (c, ()) => c 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 @@ -482,22 +536,34 @@ fun compare ((e1, _), (e2, _)) = join (Int.compare (n1, n2), fn () => join (joinL compare (es1, es2), fn () => compare (e1, e2))) + | (EServerCall _, _) => LESS + | (_, EServerCall _) => GREATER + + | (EKAbs (_, e1), EKAbs (_, e2)) => compare (e1, e2) + | (EKAbs _, _) => LESS + | (_, EKAbs _) => GREATER + + | (EKApp (e1, k1), EKApp (e2, k2)) => + join (compare (e1, e2), + fn () => Kind.compare (k1, k2)) datatype binder = - RelC of string * kind + RelK of string + | RelC of string * kind | NamedC of string * int * kind * con option | RelE of string * con | NamedE of string * int * con * exp option * string 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 @@ -548,7 +614,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = 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' => @@ -660,6 +726,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.map2 (mfc ctx t, fn t' => (EServerCall (n, es', e', t'), 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))) and mfp ctx (pAll as (p, loc)) = case p of @@ -704,13 +781,13 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = end fun mapfold {kind = fk, con = fc, exp = fe} = - mapfoldB {kind = fk, + mapfoldB {kind = fn () => fk, con = fn () => fc, exp = fn () => fe, bind = fn ((), _) => ()} () fun mapB {kind, con, exp, bind} ctx e = - 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, ()), exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), bind = bind} ctx e () of @@ -732,7 +809,7 @@ fun fold {kind, con, exp} s e = | S.Return _ => raise Fail "CoreUtil.Exp.fold: Impossible" fun foldB {kind, con, exp, bind} ctx s e = - case mapfoldB {kind = fn k => fn s => S.Continue (k, kind (k, s)), + case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (k, kind (ctx, k, s)), con = fn ctx => fn c => fn s => S.Continue (c, con (ctx, c, s)), exp = fn ctx => fn e => fn s => S.Continue (e, exp (ctx, e, s)), bind = bind} ctx e s of @@ -759,11 +836,11 @@ fun exists {kind, con, exp} k = | S.Continue _ => false fun existsB {kind, con, exp, bind} ctx k = - case mapfoldB {kind = fn k => fn () => - if kind k then - S.Return () - else - S.Continue (k, ()), + case mapfoldB {kind = fn ctx => fn k => fn () => + if kind (ctx, k) then + S.Return () + else + S.Continue (k, ()), con = fn ctx => fn c => fn () => if con (ctx, c) then S.Return () @@ -786,7 +863,7 @@ fun foldMap {kind, con, exp} s e = | S.Return _ => raise Fail "CoreUtil.Exp.foldMap: Impossible" fun foldMapB {kind, con, exp, bind} ctx s e = - case mapfoldB {kind = fn k => fn s => S.Continue (kind (k, s)), + case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (kind (ctx, k, s)), con = fn ctx => fn c => fn s => S.Continue (con (ctx, c, s)), exp = fn ctx => fn e => fn s => S.Continue (exp (ctx, e, s)), bind = bind} ctx e s of @@ -801,13 +878,14 @@ datatype binder = datatype Exp.binder fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, 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 @@ -821,7 +899,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} = and mfd' ctx (dAll as (d, loc)) = case d of DCon (x, n, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (mfc ctx c, fn c' => @@ -877,7 +955,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} = end fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} = - mapfoldB {kind = fk, + mapfoldB {kind = fn () => fk, con = fn () => fc, exp = fn () => fe, decl = fn () => fd, @@ -900,7 +978,7 @@ fun foldMap {kind, con, exp, decl} s d = | S.Return _ => raise Fail "CoreUtil.Decl.foldMap: Impossible" fun foldMapB {kind, con, exp, decl, bind} ctx s d = - case mapfoldB {kind = fn k => fn s => S.Continue (kind (k, s)), + case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (kind (ctx, k, s)), con = fn ctx => fn c => fn s => S.Continue (con (ctx, c, s)), exp = fn ctx => fn e => fn s => S.Continue (exp (ctx, e, s)), decl = fn ctx => fn d => fn s => S.Continue (decl (ctx, d, s)), @@ -1009,14 +1087,14 @@ fun mapfoldB (all as {bind, ...}) = end fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} = - mapfoldB {kind = fk, + mapfoldB {kind = fn () => fk, con = fn () => fc, exp = fn () => fe, decl = fn () => fd, bind = fn ((), _) => ()} () fun mapB {kind, con, exp, decl, bind} ctx ds = - 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, ()), exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()), @@ -1025,7 +1103,7 @@ fun mapB {kind, con, exp, decl, bind} ctx ds = | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible" fun map {kind, con, exp, decl} ds = - mapB {kind = kind, + mapB {kind = fn () => kind, con = fn () => con, exp = fn () => exp, decl = fn () => decl, diff --git a/src/corify.sml b/src/corify.sml index 802baf66..9ca6c915 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -444,10 +444,14 @@ fun corifyKind (k, loc) = | L.KUnit => (L'.KUnit, loc) | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc) + | L.KRel n => (L'.KRel n, loc) + | L.KFun (x, k) => (L'.KFun (x, corifyKind k), loc) + fun corifyCon st (c, loc) = case c of L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc) | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) + | L.TKFun (x, t) => (L'.TKFun (x, corifyCon st t), loc) | L.TRecord c => (L'.TRecord (corifyCon st c), loc) | L.CRel n => (L'.CRel n, loc) @@ -468,6 +472,9 @@ fun corifyCon st (c, loc) = | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) + | L.CKApp (c1, k) => (L'.CKApp (corifyCon st c1, corifyKind k), loc) + | L.CKAbs (x, c) => (L'.CKAbs (x, corifyCon st c), loc) + | L.CName s => (L'.CName s, loc) | L.CRecord (k, xcs) => @@ -581,6 +588,8 @@ fun corifyExp st (e, loc) = | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) + | L.EKApp (e1, k) => (L'.EKApp (corifyExp st e1, corifyKind k), loc) + | L.EKAbs (x, e1) => (L'.EKAbs (x, corifyExp st e1), loc) | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) diff --git a/src/defunc.sml b/src/defunc.sml index 1e997983..7a17d1dc 100644 --- a/src/defunc.sml +++ b/src/defunc.sml @@ -39,7 +39,7 @@ val functionInside = U.Con.exists {kind = fn _ => false, | CFfi ("Basis", "transaction") => true | _ => false} -val freeVars = U.Exp.foldB {kind = fn (_, xs) => xs, +val freeVars = U.Exp.foldB {kind = fn (_, _, xs) => xs, con = fn (_, _, xs) => xs, exp = fn (bound, e, xs) => case e of @@ -70,7 +70,7 @@ fun positionOf (v : int, ls) = end fun squish fvs = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn bound => fn e => case e of @@ -211,12 +211,13 @@ fun exp (env, e, st) = fun bind (env, b) = case b of - U.Decl.RelC (x, k) => E.pushCRel env x k + U.Decl.RelK x => E.pushKRel env x + | U.Decl.RelC (x, k) => E.pushCRel env x k | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co | U.Decl.RelE (x, t) => E.pushERel env x t | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s -fun doDecl env = U.Decl.foldMapB {kind = fn x => x, +fun doDecl env = U.Decl.foldMapB {kind = default, con = default, exp = exp, decl = default, diff --git a/src/especialize.sml b/src/especialize.sml index 7abc0582..6486842b 100644 --- a/src/especialize.sml +++ b/src/especialize.sml @@ -43,7 +43,7 @@ structure KM = BinaryMapFn(K) structure IM = IntBinaryMap structure IS = IntBinarySet -val freeVars = U.Exp.foldB {kind = fn (_, xs) => xs, +val freeVars = U.Exp.foldB {kind = fn (_, _, xs) => xs, con = fn (_, _, xs) => xs, exp = fn (bound, e, xs) => case e of @@ -80,7 +80,7 @@ fun positionOf (v : int, ls) = end fun squish fvs = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn bound => fn e => case e of @@ -110,7 +110,6 @@ type state = { decls : (string * int * con * exp * string) list } -fun id x = x fun default (_, x, st) = (x, st) fun specialize' file = @@ -281,9 +280,9 @@ fun specialize' file = end end - and specExp env = U.Exp.foldMapB {kind = id, con = default, exp = exp, bind = bind} env + and specExp env = U.Exp.foldMapB {kind = default, con = default, exp = exp, bind = bind} env - val specDecl = U.Decl.foldMapB {kind = id, con = default, exp = exp, decl = default, bind = bind} + val specDecl = U.Decl.foldMapB {kind = default, con = default, exp = exp, decl = default, bind = bind} fun doDecl (d, (st : state, changed)) = let diff --git a/src/monoize.sml b/src/monoize.sml index 96ef2c6a..892ae81f 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -211,6 +211,10 @@ fun monoType env = | L.CTuple _ => poly () | L.CProj _ => poly () + + | L.CKAbs _ => poly () + | L.CKApp _ => poly () + | L.TKFun _ => poly () end in mt env IM.empty @@ -2265,6 +2269,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = in ((L'.EServerCall (call, ek, t), loc), fm) end + + | L.EKAbs _ => poly () + | L.EKApp _ => poly () end fun monoDecl (env, fm) (all as (d, loc)) = diff --git a/src/reduce.sml b/src/reduce.sml index 77718b66..8664d38d 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -34,60 +34,104 @@ open Core structure IM = IntBinaryMap datatype env_item = - UnknownC + UnknownK + | KnownK of kind + + | UnknownC | KnownC of con | UnknownE | KnownE of exp - | Lift of int * int + | Lift of int * int * int type env = env_item list fun ei2s ei = case ei of - UnknownC => "UC" + UnknownK => "UK" + | KnownK _ => "KK" + | UnknownC => "UC" | KnownC _ => "KC" | UnknownE => "UE" | KnownE _ => "KE" - | Lift (n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")" + | Lift (_, n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")" fun e2s env = String.concatWith " " (map ei2s env) val deKnown = List.filter (fn KnownC _ => false | KnownE _ => false + | KnownK _ => false | _ => true) -fun conAndExp (namedC, namedE) = +fun kindConAndExp (namedC, namedE) = let + fun kind env (all as (k, loc)) = + case k of + KType => all + | KArrow (k1, k2) => (KArrow (kind env k1, kind env k2), loc) + | KName => all + | KRecord k => (KRecord (kind env k), loc) + | KUnit => all + | KTuple ks => (KTuple (map (kind env) ks), loc) + + | KRel n => + let + fun find (n', env, nudge, lift) = + case env of + [] => raise Fail "Reduce.kind: KRel" + | UnknownC :: rest => find (n', rest, nudge, lift) + | KnownC _ :: rest => find (n', rest, nudge, lift) + | UnknownE :: rest => find (n', rest, nudge, lift) + | KnownE _ :: rest => find (n', rest, nudge, lift) + | Lift (lift', _, _) :: rest => find (n', rest, nudge + lift', lift + lift') + | UnknownK :: rest => + if n' = 0 then + (KRel (n + nudge), loc) + else + find (n' - 1, rest, nudge, lift + 1) + | KnownK k :: rest => + if n' = 0 then + kind (Lift (lift, 0, 0) :: rest) k + else + find (n' - 1, rest, nudge - 1, lift) + in + find (n, env, 0, 0) + end + | KFun (x, k) => (KFun (x, kind (UnknownK :: env) k), loc) + fun con env (all as (c, loc)) = ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*) case c of TFun (c1, c2) => (TFun (con env c1, con env c2), loc) - | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc) + | TCFun (x, k, c2) => (TCFun (x, kind env k, con (UnknownC :: env) c2), loc) + | TKFun (x, c2) => (TKFun (x, con (UnknownK :: env) c2), loc) | TRecord c => (TRecord (con env c), loc) | CRel n => let - fun find (n', env, nudge, lift) = + fun find (n', env, nudge, liftK, liftC) = case env of [] => raise Fail "Reduce.con: CRel" - | UnknownE :: rest => find (n', rest, nudge, lift) - | KnownE _ :: rest => find (n', rest, nudge, lift) - | Lift (lift', _) :: rest => find (n', rest, nudge + lift', lift + lift') + | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC) + | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC) + | UnknownE :: rest => find (n', rest, nudge, liftK, liftC) + | KnownE _ :: rest => find (n', rest, nudge, liftK, liftC) + | Lift (liftK', liftC', _) :: rest => find (n', rest, nudge + liftC', + liftK + liftK', liftC + liftC') | UnknownC :: rest => if n' = 0 then (CRel (n + nudge), loc) else - find (n' - 1, rest, nudge, lift + 1) + find (n' - 1, rest, nudge, liftK, liftC + 1) | KnownC c :: rest => if n' = 0 then - con (Lift (lift, 0) :: rest) c + con (Lift (liftK, liftC, 0) :: rest) c else - find (n' - 1, rest, nudge - 1, lift) + find (n' - 1, rest, nudge - 1, liftK, liftC) in (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) - find (n, env, 0, 0) + find (n, env, 0, 0, 0) end | CNamed n => (case IM.find (namedC, n) of @@ -105,20 +149,32 @@ fun conAndExp (namedC, namedE) = | CApp ((CMap (dom, ran), _), f) => (case #1 c2 of - CRecord (_, []) => (CRecord (ran, []), loc) + CRecord (_, []) => (CRecord (kind env ran, []), loc) | CRecord (_, (x, c) :: rest) => con (deKnown env) (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc), - (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc) + (CApp (c1, (CRecord (kind env dom, rest), loc)), loc)), loc) | _ => (CApp (c1, c2), loc)) | _ => (CApp (c1, c2), loc) end - | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc) + | CAbs (x, k, b) => (CAbs (x, kind env k, con (UnknownC :: env) b), loc) + + | CKApp (c1, k) => + let + val c1 = con env c1 + in + case #1 c1 of + CKAbs (_, b) => + con (KnownK k :: deKnown env) b + + | _ => (CKApp (c1, kind env k), loc) + end + | CKAbs (x, b) => (CKAbs (x, con (UnknownK :: env) b), loc) | CName _ => all - | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc) + | CRecord (k, xcs) => (CRecord (kind env k, map (fn (x, c) => (con env x, con env c)) xcs), loc) | CConcat (c1, c2) => let val c1 = con env c1 @@ -126,10 +182,10 @@ fun conAndExp (namedC, namedE) = in case (#1 c1, #1 c2) of (CRecord (k, xcs1), CRecord (_, xcs2)) => - (CRecord (k, xcs1 @ xcs2), loc) + (CRecord (kind env k, xcs1 @ xcs2), loc) | _ => (CConcat (c1, c2), loc) end - | CMap _ => all + | CMap (dom, ran) => (CMap (kind env dom, kind env ran), loc) | CUnit => all @@ -164,27 +220,30 @@ fun conAndExp (namedC, namedE) = EPrim _ => all | ERel n => let - fun find (n', env, nudge, liftC, liftE) = + fun find (n', env, nudge, liftK, liftC, liftE) = case env of [] => raise Fail "Reduce.exp: ERel" - | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE) - | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE) - | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', - liftC + liftC', liftE + liftE') + | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC, liftE) + | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC, liftE) + | UnknownC :: rest => find (n', rest, nudge, liftK, liftC + 1, liftE) + | KnownC _ :: rest => find (n', rest, nudge, liftK, liftC, liftE) + | Lift (liftK', liftC', liftE') :: rest => + find (n', rest, nudge + liftE', + liftK + liftK', liftC + liftC', liftE + liftE') | UnknownE :: rest => if n' = 0 then (ERel (n + nudge), loc) else - find (n' - 1, rest, nudge, liftC, liftE + 1) + find (n' - 1, rest, nudge, liftK, liftC, liftE + 1) | KnownE e :: rest => if n' = 0 then ((*print "SUBSTITUTING\n";*) - exp (Lift (liftC, liftE) :: rest) e) + exp (Lift (liftK, liftC, liftE) :: rest) e) else - find (n' - 1, rest, nudge - 1, liftC, liftE) + find (n' - 1, rest, nudge - 1, liftK, liftC, liftE) in (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) - find (n, env, 0, 0, 0) + find (n, env, 0, 0, 0, 0) end | ENamed n => (case IM.find (namedE, n) of @@ -217,7 +276,18 @@ fun conAndExp (namedC, namedE) = | _ => (ECApp (e, c), loc) end - | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc) + | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc) + + | EKApp (e, k) => + let + val e = exp env e + in + case #1 e of + EKAbs (_, b) => exp (KnownK k :: deKnown env) b + | _ => (EKApp (e, kind env k), loc) + end + + | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc) | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) | EField (e, c, {field, rest}) => @@ -353,11 +423,12 @@ fun conAndExp (namedC, namedE) = | EServerCall (n, es, e, t) => (EServerCall (n, map (exp env) es, exp env e, con env t), loc)) in - {con = con, exp = exp} + {kind = kind, con = con, exp = exp} end -fun con namedC env c = #con (conAndExp (namedC, IM.empty)) env c -fun exp (namedC, namedE) env e = #exp (conAndExp (namedC, namedE)) env e +fun kind namedC env k = #kind (kindConAndExp (namedC, IM.empty)) env k +fun con namedC env c = #con (kindConAndExp (namedC, IM.empty)) env c +fun exp (namedC, namedE) env e = #exp (kindConAndExp (namedC, namedE)) env e fun reduce file = let @@ -365,6 +436,7 @@ fun reduce file = case #1 d of DCon (x, n, k, c) => let + val k = kind namedC [] k val c = con namedC [] c in ((DCon (x, n, k, c), loc), diff --git a/src/reduce_local.sml b/src/reduce_local.sml index 25b1023a..8b963e1b 100644 --- a/src/reduce_local.sml +++ b/src/reduce_local.sml @@ -85,9 +85,11 @@ fun exp env (all as (e, loc)) = | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc) | ECApp (e, c) => (ECApp (exp env e, c), loc) - | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc) + | EKApp (e, k) => (EKApp (exp env e, k), loc) + | EKAbs (x, e) => (EKAbs (x, exp env e), loc) + | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc) | EField (e, c, others) => let -- cgit v1.2.3