summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/core.sml10
-rw-r--r--src/core_env.sig3
-rw-r--r--src/core_env.sml95
-rw-r--r--src/core_print.sig2
-rw-r--r--src/core_print.sml58
-rw-r--r--src/core_util.sig36
-rw-r--r--src/core_util.sml166
-rw-r--r--src/corify.sml9
-rw-r--r--src/defunc.sml9
-rw-r--r--src/especialize.sml9
-rw-r--r--src/monoize.sml7
-rw-r--r--src/reduce.sml138
-rw-r--r--src/reduce_local.sml4
13 files changed, 420 insertions, 126 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-07 10:31:21 +0000