summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab_print.sml2
-rw-r--r--src/expl.sml10
-rw-r--r--src/expl_env.sig3
-rw-r--r--src/expl_env.sml136
-rw-r--r--src/expl_print.sig2
-rw-r--r--src/expl_print.sml61
-rw-r--r--src/expl_util.sig25
-rw-r--r--src/expl_util.sml113
-rw-r--r--src/explify.sml10
9 files changed, 246 insertions, 116 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index a0e1a54a..e5dda58e 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -68,7 +68,7 @@ fun p_kind' par env (k, _) =
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
diff --git a/src/expl.sml b/src/expl.sml
index 0101dd1f..d7138620 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -37,6 +37,9 @@ datatype kind' =
| KTuple of kind list
| KRecord of kind
+ | 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
@@ -88,6 +95,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/expl_env.sig b/src/expl_env.sig
index 00179e45..5ded0f02 100644
--- a/src/expl_env.sig
+++ b/src/expl_env.sig
@@ -42,6 +42,9 @@ signature EXPL_ENV = sig
| 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
diff --git a/src/expl_env.sml b/src/expl_env.sml
index 0fefec2d..403a826a 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -45,8 +45,32 @@ exception UnboundNamed of int
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 @@ val liftConInCon =
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 @@ datatype 'a var =
| 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),
-
- renameE = #renameE env,
- relE = map (fn (x, c) => (x, lift c)) (#relE env),
- namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
-
- renameSgn = #renameSgn env,
- sgn = #sgn env,
-
- renameStr = #renameStr env,
- str = #str env
- }
- end
+ {relK = #relK env,
+
+ relC = (x, k) :: #relC env,
+ namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
+
+ relE = map (fn (x, c) => (x, lift c)) (#relE env),
+ namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
+
+ 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 @@ fun lookupCNamed (env : env) n =
| 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,
+
+ relC = #relC env,
+ namedC = #namedC env,
- renameE = SM.insert (renameE, x, Rel' (0, t)),
- relE = (x, t) :: #relE env,
- namedE = #namedE env,
+ relE = (x, t) :: #relE env,
+ namedE = #namedE env,
- renameSgn = #renameSgn env,
- sgn = #sgn env,
+ sgn = #sgn env,
- renameStr = #renameStr env,
- str = #str env}
- end
+ 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 @@ fun lookupENamed (env : env) n =
| 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 @@ fun lookupSgnNamed (env : env) n =
| 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 =
diff --git a/src/expl_print.sig b/src/expl_print.sig
index 1e2c8fbb..8f1cee97 100644
--- a/src/expl_print.sig
+++ b/src/expl_print.sig
@@ -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
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 313fef5c..e7fb51f6 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -38,22 +38,33 @@ structure E = ExplEnv
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,
@@ -116,7 +127,7 @@ fun p_con' par env (c, _) =
space,
string "::",
space,
- p_kind k,
+ p_kind env k,
space,
string "=>",
space,
@@ -134,7 +145,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) =>
@@ -158,6 +169,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
@@ -261,7 +287,7 @@ fun p_exp' par env (e, loc) =
space,
string "::",
space,
- p_kind k,
+ p_kind env k,
space,
string "=>",
space,
@@ -397,6 +423,15 @@ fun p_exp' par env (e, loc) =
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 @@ fun p_sgn_item env (sgi, _) =
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 @@ 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/expl_util.sig b/src/expl_util.sig
index 2a6c7abe..3e5c333f 100644
--- a/src/expl_util.sig
+++ b/src/expl_util.sig
@@ -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 @@ structure Con : sig
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 @@ end
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 @@ end
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,
diff --git a/src/expl_util.sml b/src/expl_util.sml
index febf3586..9e150b87 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -33,39 +33,55 @@ structure S = Search
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 @@ end
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 @@ 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 =>
@@ -119,16 +136,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,
@@ -146,9 +163,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)))
@@ -163,17 +180,32 @@ 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 ((), _) => ()} ()
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 @@ end
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 @@ 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' =>
@@ -338,12 +372,23 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
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 @@ end
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 mapfoldB {kind, con, sgn_item, sgn, bind} =
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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
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,
diff --git a/src/explify.sml b/src/explify.sml
index 5bce9268..b2564789 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -45,6 +45,9 @@ fun explifyKind (k, loc) =
| L.KUnif (_, _, ref (SOME k)) => explifyKind k
| L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
+ | L.KRel n => (L'.KRel n, loc)
+ | L.KFun (x, k) => (L'.KFun (x, explifyKind k), loc)
+
fun explifyCon (c, loc) =
case c of
L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
@@ -74,6 +77,10 @@ fun explifyCon (c, loc) =
| L.CUnif (_, _, _, ref (SOME c)) => explifyCon c
| L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
+ | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc)
+ | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc)
+ | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc)
+
fun explifyPatCon pc =
case pc of
L.PConVar n => L'.PConVar n
@@ -123,6 +130,9 @@ fun explifyExp (e, loc) =
| L.EDVal (x, t, e') => (L'.ELet (x, explifyCon t, explifyExp e', e), loc))
(explifyExp e) des
+ | L.EKAbs (x, e) => (L'.EKAbs (x, explifyExp e), loc)
+ | L.EKApp (e, k) => (L'.EKApp (explifyExp e, explifyKind k), loc)
+
fun explifySgi (sgi, loc) =
case sgi of
L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-09 16:17:45 +0000