summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/cjr.sml10
-rw-r--r--src/cjr_env.sig2
-rw-r--r--src/cjr_env.sml13
-rw-r--r--src/cjr_print.sml72
-rw-r--r--src/cjrize.sml19
-rw-r--r--src/core.sml8
-rw-r--r--src/core_print.sml16
-rw-r--r--src/core_util.sig2
-rw-r--r--src/core_util.sml12
-rw-r--r--src/corify.sml1184
-rw-r--r--src/elab.sml6
-rw-r--r--src/elab_env.sig4
-rw-r--r--src/elab_env.sml43
-rw-r--r--src/elab_print.sml8
-rw-r--r--src/elab_util.sig2
-rw-r--r--src/elab_util.sml6
-rw-r--r--src/elaborate.sml41
-rw-r--r--src/expl.sml4
-rw-r--r--src/expl_print.sml8
-rw-r--r--src/expl_util.sig2
-rw-r--r--src/expl_util.sml6
-rw-r--r--src/explify.sml2
-rw-r--r--src/mono.sml8
-rw-r--r--src/mono_env.sml9
-rw-r--r--src/mono_opt.sml8
-rw-r--r--src/mono_print.sml14
-rw-r--r--src/mono_reduce.sml8
-rw-r--r--src/mono_shake.sml2
-rw-r--r--src/mono_util.sig2
-rw-r--r--src/mono_util.sml20
-rw-r--r--src/monoize.sml20
31 files changed, 835 insertions, 726 deletions
diff --git a/src/cjr.sml b/src/cjr.sml
index 95a21956..d9dc51c1 100644
--- a/src/cjr.sml
+++ b/src/cjr.sml
@@ -29,11 +29,13 @@ structure Cjr = struct
type 'a located = 'a ErrorMsg.located
+datatype datatype_kind = datatype Mono.datatype_kind
+
datatype typ' =
TTop
| TFun of typ * typ
| TRecord of int
- | TDatatype of int * (string * int * typ option) list
+ | TDatatype of datatype_kind * int * (string * int * typ option) list
| TFfi of string * string
withtype typ = typ' located
@@ -46,7 +48,7 @@ datatype pat' =
PWild
| PVar of string * typ
| PPrim of Prim.t
- | PCon of patCon * pat option
+ | PCon of datatype_kind * patCon * pat option
| PRecord of (string * pat * typ) list
withtype pat = pat' located
@@ -55,7 +57,7 @@ datatype exp' =
EPrim of Prim.t
| ERel of int
| ENamed of int
- | ECon of patCon * exp option
+ | ECon of datatype_kind * patCon * exp option
| EFfi of string * string
| EFfiApp of string * string * exp list
| EApp of exp * exp
@@ -72,7 +74,7 @@ withtype exp = exp' located
datatype decl' =
DStruct of int * (string * typ) list
- | DDatatype of string * int * (string * int * typ option) list
+ | DDatatype of datatype_kind * string * int * (string * int * typ option) list
| DVal of string * int * typ * exp
| DFun of string * int * (string * typ) list * typ * exp
| DFunRec of (string * int * (string * typ) list * typ * exp) list
diff --git a/src/cjr_env.sig b/src/cjr_env.sig
index 7573c75e..0254f150 100644
--- a/src/cjr_env.sig
+++ b/src/cjr_env.sig
@@ -53,5 +53,7 @@ signature CJR_ENV = sig
val lookupStruct : env -> int -> (string * Cjr.typ) list
val declBinds : env -> Cjr.decl -> env
+
+ val classifyDatatype : (string * int * Cjr.typ option) list -> Cjr.datatype_kind
end
diff --git a/src/cjr_env.sml b/src/cjr_env.sml
index 6a3c41bc..83f0cc30 100644
--- a/src/cjr_env.sml
+++ b/src/cjr_env.sml
@@ -129,14 +129,21 @@ fun lookupStruct (env : env) n =
NONE => raise UnboundStruct n
| SOME x => x
+fun classifyDatatype xncs =
+ if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+ Enum
+ else
+ Default
+
fun declBinds env (d, loc) =
case d of
- DDatatype (x, n, xncs) =>
+ DDatatype (_, x, n, xncs) =>
let
val env = pushDatatype env x n xncs
+ val dt = (TDatatype (classifyDatatype xncs, n, xncs), loc)
in
- foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype (n, xncs), loc)
- | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype (n, xncs), loc)), loc))
+ foldl (fn ((x', n', NONE), env) => pushENamed env x' n' dt
+ | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, dt), loc))
env xncs
end
| DStruct (n, xts) => pushStruct env n xts
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index 7ff8f60f..749f56ab 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -53,7 +53,7 @@ structure CM = BinaryMapFn(struct
val debug = ref false
-val dummyTyp = (TDatatype (0, []), ErrorMsg.dummySpan)
+val dummyTyp = (TDatatype (Enum, 0, []), ErrorMsg.dummySpan)
fun p_typ' par env (t, loc) =
case t of
@@ -69,7 +69,12 @@ fun p_typ' par env (t, loc) =
space,
string "__lws_",
string (Int.toString i)]
- | TDatatype (n, _) =>
+ | TDatatype (Enum, n, _) =>
+ (box [string "enum",
+ space,
+ string ("__lwe_" ^ #1 (E.lookupDatatype env n) ^ "_" ^ Int.toString n)]
+ handle CjrEnv.UnboundNamed _ => string ("__lwd_UNBOUND__" ^ Int.toString n))
+ | TDatatype (Default, n, _) =>
(box [string "struct",
space,
string ("__lwd_" ^ #1 (E.lookupDatatype env n) ^ "_" ^ Int.toString n ^ "*")]
@@ -103,8 +108,8 @@ fun p_pat_preamble env (p, _) =
newline],
env)
| PPrim _ => (box [], env)
- | PCon (_, NONE) => (box [], env)
- | PCon (_, SOME p) => p_pat_preamble env p
+ | PCon (_, _, NONE) => (box [], env)
+ | PCon (_, _, SOME p) => p_pat_preamble env p
| PRecord xps =>
foldl (fn ((_, p, _), (pp, env)) =>
let
@@ -161,7 +166,7 @@ fun p_pat (env, exit, depth) (p, _) =
env)
| PPrim _ => raise Fail "CjrPrint: Disallowed PPrim primitive"
- | PCon (pc, po) =>
+ | PCon (dk, pc, po) =>
let
val (p, env) =
case po of
@@ -175,9 +180,10 @@ fun p_pat (env, exit, depth) (p, _) =
let
val (x, to, _) = E.lookupConstructor env n
in
- (x, to)
+ ("__lwc_" ^ x, to)
end
- | PConFfi _ => raise Fail "PConFfi"
+ | PConFfi {mod = m, con, arg, ...} =>
+ ("lw_" ^ m ^ "_" ^ con, arg)
val t = case to of
NONE => raise Fail "CjrPrint: Constructor mismatch"
@@ -194,7 +200,7 @@ fun p_pat (env, exit, depth) (p, _) =
space,
string "disc",
string (Int.toString depth),
- string "->data.__lwc_",
+ string "->data.",
string x,
string ";",
newline,
@@ -208,7 +214,9 @@ fun p_pat (env, exit, depth) (p, _) =
space,
string "(disc",
string (Int.toString depth),
- string "->tag",
+ case dk of
+ Enum => box []
+ | Default => string "->tag",
space,
string "!=",
space,
@@ -285,7 +293,8 @@ fun p_exp' par env (e, loc) =
EPrim p => Prim.p_t p
| ERel n => p_rel env n
| ENamed n => p_enamed env n
- | ECon (pc, eo) =>
+ | ECon (Enum, pc, _) => p_patCon env pc
+ | ECon (Default, pc, eo) =>
let
val (xd, xc) = patConInfo env pc
in
@@ -497,7 +506,17 @@ fun p_decl env (dAll as (d, _) : decl) =
string ";",
newline]) xts,
string "};"]
- | DDatatype (x, n, xncs) =>
+ | DDatatype (Enum, x, n, xncs) =>
+ box [string "enum",
+ space,
+ string ("__lwe_" ^ x ^ "_" ^ Int.toString n),
+ space,
+ string "{",
+ space,
+ p_list_sep (box [string ",", space]) (fn (x, n, _) => string ("__lwc_" ^ x ^ "_" ^ Int.toString n)) xncs,
+ space,
+ string "};"]
+ | DDatatype (Default, x, n, xncs) =>
let
val xncsArgs = List.mapPartial (fn (x, n, NONE) => NONE
| (x, n, SOME t) => SOME (x, n, t)) xncs
@@ -541,7 +560,7 @@ fun p_decl env (dAll as (d, _) : decl) =
string "data;",
newline]),
string "};"]
- end
+ end
| DVal (x, n, t, e) =>
box [p_typ env t,
@@ -753,7 +772,34 @@ fun p_file env (ds, ps) =
string "})"]
end
- | TDatatype (i, _) =>
+ | TDatatype (Enum, i, _) =>
+ let
+ val (x, xncs) = E.lookupDatatype env i
+
+ fun doEm xncs =
+ case xncs of
+ [] => string ("(lw_error(ctx, FATAL, \"Error unurlifying datatype " ^ x ^ "\"), (enum __lwe_"
+ ^ x ^ "_" ^ Int.toString i ^ ")0)")
+ | (x', n, to) :: rest =>
+ box [string "((!strncmp(request, \"",
+ string x',
+ string "\", ",
+ string (Int.toString (size x')),
+ string ") && (request[",
+ string (Int.toString (size x')),
+ string "] == 0 || request[",
+ string (Int.toString (size x')),
+ string ("] == '/')) ? __lwc_" ^ x' ^ "_" ^ Int.toString n),
+ space,
+ string ":",
+ space,
+ doEm rest,
+ string ")"]
+ in
+ doEm xncs
+ end
+
+ | TDatatype (Default, i, _) =>
let
val (x, xncs) = E.lookupDatatype env i
diff --git a/src/cjrize.sml b/src/cjrize.sml
index 526a3788..5ba8ccb7 100644
--- a/src/cjrize.sml
+++ b/src/cjrize.sml
@@ -84,7 +84,7 @@ fun cifyTyp ((t, loc), sm) =
in
((L'.TRecord si, loc), sm)
end
- | L.TDatatype (n, xncs) =>
+ | L.TDatatype (dk, n, xncs) =>
let
val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) =>
case to of
@@ -97,7 +97,7 @@ fun cifyTyp ((t, loc), sm) =
end)
sm xncs
in
- ((L'.TDatatype (n, xncs), loc), sm)
+ ((L'.TDatatype (dk, n, xncs), loc), sm)
end
| L.TFfi mx => ((L'.TFfi mx, loc), sm)
@@ -131,18 +131,18 @@ fun cifyPat ((p, loc), sm) =
((L'.PVar (x, t), loc), sm)
end
| L.PPrim p => ((L'.PPrim p, loc), sm)
- | L.PCon (pc, NONE) =>
+ | L.PCon (dk, pc, NONE) =>
let
val (pc, sm) = cifyPatCon (pc, sm)
in
- ((L'.PCon (pc, NONE), loc), sm)
+ ((L'.PCon (dk, pc, NONE), loc), sm)
end
- | L.PCon (pc, SOME p) =>
+ | L.PCon (dk, pc, SOME p) =>
let
val (pc, sm) = cifyPatCon (pc, sm)
val (p, sm) = cifyPat (p, sm)
in
- ((L'.PCon (pc, SOME p), loc), sm)
+ ((L'.PCon (dk, pc, SOME p), loc), sm)
end
| L.PRecord xps =>
let
@@ -162,7 +162,7 @@ fun cifyExp ((e, loc), sm) =
L.EPrim p => ((L'.EPrim p, loc), sm)
| L.ERel n => ((L'.ERel n, loc), sm)
| L.ENamed n => ((L'.ENamed n, loc), sm)
- | L.ECon (pc, eo) =>
+ | L.ECon (dk, pc, eo) =>
let
val (eo, sm) =
case eo of
@@ -175,7 +175,7 @@ fun cifyExp ((e, loc), sm) =
end
val (pc, sm) = cifyPatCon (pc, sm)
in
- ((L'.ECon (pc, eo), loc), sm)
+ ((L'.ECon (dk, pc, eo), loc), sm)
end
| L.EFfi mx => ((L'.EFfi mx, loc), sm)
| L.EFfiApp (m, x, es) =>
@@ -268,6 +268,7 @@ fun cifyDecl ((d, loc), sm) =
case d of
L.DDatatype (x, n, xncs) =>
let
+ val dk = MonoUtil.classifyDatatype xncs
val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) =>
case to of
NONE => ((x, n, NONE), sm)
@@ -278,7 +279,7 @@ fun cifyDecl ((d, loc), sm) =
((x, n, SOME t), sm)
end) sm xncs
in
- (SOME (L'.DDatatype (x, n, xncs), loc), NONE, sm)
+ (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm)
end
| L.DVal (x, n, t, e, _) =>
diff --git a/src/core.sml b/src/core.sml
index e9fd570c..3f56b49c 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -59,15 +59,17 @@ datatype con' =
withtype con = con' located
+datatype datatype_kind = datatype Elab.datatype_kind
+
datatype patCon =
PConVar of int
- | PConFfi of {mod : string, datatyp : string, con : string, arg : con option}
+ | PConFfi of {mod : string, datatyp : string, con : string, arg : con option, kind : datatype_kind}
datatype pat' =
PWild
| PVar of string * con
| PPrim of Prim.t
- | PCon of patCon * pat option
+ | PCon of datatype_kind * patCon * pat option
| PRecord of (string * pat * con) list
withtype pat = pat' located
@@ -76,7 +78,7 @@ datatype exp' =
EPrim of Prim.t
| ERel of int
| ENamed of int
- | ECon of patCon * exp option
+ | ECon of datatype_kind * patCon * exp option
| EFfi of string * string
| EFfiApp of string * string * exp list
| EApp of exp * exp
diff --git a/src/core_print.sml b/src/core_print.sml
index 0e797d88..963c02a9 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -173,10 +173,10 @@ fun p_pat' par env (p, _) =
PWild => string "_"
| PVar (s, _) => string s
| PPrim p => Prim.p_t p
- | PCon (n, NONE) => p_patCon env n
- | PCon (n, SOME p) => parenIf par (box [p_patCon env n,
- space,
- p_pat' true env p])
+ | PCon (_, n, NONE) => p_patCon env n
+ | PCon (_,n, SOME p) => parenIf par (box [p_patCon env n,
+ space,
+ p_pat' true env p])
| PRecord xps =>
box [string "{",
p_list_sep (box [string ",", space]) (fn (x, p, _) =>
@@ -199,10 +199,10 @@ fun p_exp' par env (e, _) =
string (#1 (E.lookupERel env n)))
handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n))
| ENamed n => p_enamed env n
- | ECon (pc, NONE) => p_patCon env pc
- | ECon (pc, SOME e) => parenIf par (box [p_patCon env pc,
- space,
- p_exp' true env e])
+ | ECon (_, pc, NONE) => p_patCon env pc
+ | ECon (_, pc, SOME e) => parenIf par (box [p_patCon env pc,
+ space,
+ p_exp' true env e])
| EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"]
| EFfiApp (m, x, es) => box [string "FFI(",
string m,
diff --git a/src/core_util.sig b/src/core_util.sig
index 3a4e3210..ebfcf54b 100644
--- a/src/core_util.sig
+++ b/src/core_util.sig
@@ -27,6 +27,8 @@
signature CORE_UTIL = sig
+val classifyDatatype : (string * int * Core.con option) list -> Core.datatype_kind
+
structure Kind : sig
val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder
-> (Core.kind, 'state, 'abort) Search.mapfolder
diff --git a/src/core_util.sml b/src/core_util.sml
index 1cc25e37..6c790437 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -29,6 +29,12 @@ structure CoreUtil :> CORE_UTIL = struct
open Core
+fun classifyDatatype xncs =
+ if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+ Enum
+ else
+ Default
+
structure S = Search
structure Kind = struct
@@ -227,11 +233,11 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
EPrim _ => S.return2 eAll
| ERel _ => S.return2 eAll
| ENamed _ => S.return2 eAll
- | ECon (_, NONE) => S.return2 eAll
- | ECon (n, SOME e) =>
+ | ECon (_, _, NONE) => S.return2 eAll
+ | ECon (dk, n, SOME e) =>
S.map2 (mfe ctx e,
fn e' =>
- (ECon (n, SOME e'), loc))
+ (ECon (dk, n, SOME e'), loc))
| EFfi _ => S.return2 eAll
| EFfiApp (m, x, es) =>
S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es,
diff --git a/src/corify.sml b/src/corify.sml
index 146868e6..7e2f2493 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -62,7 +62,7 @@ structure St : sig
val enter : t -> t
val leave : t -> {outer : t, inner : t}
- val ffi : string -> L'.con SM.map -> (string * L'.con option) SM.map -> t
+ val ffi : string -> L'.con SM.map -> (string * L'.con option * L'.datatype_kind) SM.map -> t
datatype core_con =
CNormal of int
@@ -76,605 +76,609 @@ structure St : sig
val lookupConstructorByName : t -> string -> L'.patCon
val lookupConstructorById : t -> int -> L'.patCon
- datatype core_val =
- ENormal of int
- | EFfi of string * L'.con
- val bindVal : t -> string -> int -> t * int
- val bindConstructorVal : t -> string -> int -> t
- val lookupValById : t -> int -> int option
- val lookupValByName : t -> string -> core_val
-
- val bindStr : t -> string -> int -> t -> t
- val lookupStrById : t -> int -> t
- val lookupStrByName : string * t -> t
-
- val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
- val lookupFunctorById : t -> int -> string * int * L.str
- val lookupFunctorByName : string * t -> string * int * L.str
-end = struct
-
-datatype flattening =
- FNormal of {cons : int SM.map,
- constructors : L'.patCon SM.map,
- vals : int SM.map,
- strs : flattening SM.map,
- funs : (string * int * L.str) SM.map}
- | FFfi of {mod : string,
- vals : L'.con SM.map,
- constructors : (string * L'.con option) SM.map}
-
-type t = {
- cons : int IM.map,
- constructors : L'.patCon IM.map,
- vals : int IM.map,
- strs : flattening IM.map,
- funs : (string * int * L.str) IM.map,
- current : flattening,
- nested : flattening list
-}
-
-val empty = {
- cons = IM.empty,
- constructors = IM.empty,
- vals = IM.empty,
- strs = IM.empty,
- funs = IM.empty,
- current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
- nested = []
-}
-
-fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) =
- print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
- ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
- ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
- ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
- ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
- | debug _ = print "Not normal!\n"
-
-datatype core_con =
- CNormal of int
- | CFfi of string
-
-datatype core_val =
- ENormal of int
- | EFfi of string * L'.con
-
-fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n =
- let
- val n' = alloc ()
-
- val current =
- case current of
- FFfi _ => raise Fail "Binding inside FFfi"
- | FNormal {cons, constructors, vals, strs, funs} =>
- FNormal {cons = SM.insert (cons, s, n'),
- constructors = constructors,
- vals = vals,
- strs = strs,
- funs = funs}
- in
- ({cons = IM.insert (cons, n, n'),
+ datatype core_val =
+ ENormal of int
+ | EFfi of string * L'.con
+ val bindVal : t -> string -> int -> t * int
+ val bindConstructorVal : t -> string -> int -> t
+ val lookupValById : t -> int -> int option
+ val lookupValByName : t -> string -> core_val
+
+ val bindStr : t -> string -> int -> t -> t
+ val lookupStrById : t -> int -> t
+ val lookupStrByName : string * t -> t
+
+ val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
+ val lookupFunctorById : t -> int -> string * int * L.str
+ val lookupFunctorByName : string * t -> string * int * L.str
+ end = struct
+
+ datatype flattening =
+ FNormal of {cons : int SM.map,
+ constructors : L'.patCon SM.map,
+ vals : int SM.map,
+ strs : flattening SM.map,
+ funs : (string * int * L.str) SM.map}
+ | FFfi of {mod : string,
+ vals : L'.con SM.map,
+ constructors : (string * L'.con option * L'.datatype_kind) SM.map}
+
+ type t = {
+ cons : int IM.map,
+ constructors : L'.patCon IM.map,
+ vals : int IM.map,
+ strs : flattening IM.map,
+ funs : (string * int * L.str) IM.map,
+ current : flattening,
+ nested : flattening list
+ }
+
+ val empty = {
+ cons = IM.empty,
+ constructors = IM.empty,
+ vals = IM.empty,
+ strs = IM.empty,
+ funs = IM.empty,
+ current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
+ nested = []
+ }
+
+ fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) =
+ print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
+ ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
+ ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
+ ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
+ ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
+ | debug _ = print "Not normal!\n"
+
+ datatype core_con =
+ CNormal of int
+ | CFfi of string
+
+ datatype core_val =
+ ENormal of int
+ | EFfi of string * L'.con
+
+ fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n =
+ let
+ val n' = alloc ()
+
+ val current =
+ case current of
+ FFfi _ => raise Fail "Binding inside FFfi"
+ | FNormal {cons, constructors, vals, strs, funs} =>
+ FNormal {cons = SM.insert (cons, s, n'),
+ constructors = constructors,
+ vals = vals,
+ strs = strs,
+ funs = funs}
+ in
+ ({cons = IM.insert (cons, n, n'),
+ constructors = constructors,
+ vals = vals,
+ strs = strs,
+ funs = funs,
+ current = current,
+ nested = nested},
+ n')
+ end
+
+ fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
+
+ fun lookupConByName ({current, ...} : t) x =
+ case current of
+ FFfi {mod = m, ...} => CFfi m
+ | FNormal {cons, ...} =>
+ case SM.find (cons, x) of
+ NONE => raise Fail "Corify.St.lookupConByName"
+ | SOME n => CNormal n
+
+ fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n =
+ let
+ val n' = alloc ()
+
+ val current =
+ case current of
+ FFfi _ => raise Fail "Binding inside FFfi"
+ | FNormal {cons, constructors, vals, strs, funs} =>
+ FNormal {cons = cons,
+ constructors = constructors,
+ vals = SM.insert (vals, s, n'),
+ strs = strs,
+ funs = funs}
+ in
+ ({cons = cons,
+ constructors = constructors,
+ vals = IM.insert (vals, n, n'),
+ strs = strs,
+ funs = funs,
+ current = current,
+ nested = nested},
+ n')
+ end
+
+ fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n =
+ let
+ val current =
+ case current of
+ FFfi _ => raise Fail "Binding inside FFfi"
+ | FNormal {cons, constructors, vals, strs, funs} =>
+ FNormal {cons = cons,
+ constructors = constructors,
+ vals = SM.insert (vals, s, n),
+ strs = strs,
+ funs = funs}
+ in
+ {cons = cons,
constructors = constructors,
- vals = vals,
+ vals = IM.insert (vals, n, n),
strs = strs,
funs = funs,
current = current,
- nested = nested},
- n')
- end
-
-fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
-
-fun lookupConByName ({current, ...} : t) x =
- case current of
- FFfi {mod = m, ...} => CFfi m
- | FNormal {cons, ...} =>
- case SM.find (cons, x) of
- NONE => raise Fail "Corify.St.lookupConByName"
- | SOME n => CNormal n
-
-fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n =
- let
- val n' = alloc ()
-
- val current =
- case current of
- FFfi _ => raise Fail "Binding inside FFfi"
- | FNormal {cons, constructors, vals, strs, funs} =>
- FNormal {cons = cons,
- constructors = constructors,
- vals = SM.insert (vals, s, n'),
- strs = strs,
- funs = funs}
- in
- ({cons = cons,
- constructors = constructors,
- vals = IM.insert (vals, n, n'),
+ nested = nested}
+ end
+
+
+ fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
+
+ fun lookupValByName ({current, ...} : t) x =
+ case current of
+ FFfi {mod = m, vals, ...} =>
+ (case SM.find (vals, x) of
+ NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val"
+ | SOME t => EFfi (m, t))
+ | FNormal {vals, ...} =>
+ case SM.find (vals, x) of
+ NONE => raise Fail "Corify.St.lookupValByName"
+ | SOME n => ENormal n
+
+ fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' =
+ let
+ val current =
+ case current of
+ FFfi _ => raise Fail "Binding inside FFfi"
+ | FNormal {cons, constructors, vals, strs, funs} =>
+ FNormal {cons = cons,
+ constructors = SM.insert (constructors, s, n'),
+ vals = vals,
+ strs = strs,
+ funs = funs}
+ in
+ {cons = cons,
+ constructors = IM.insert (constructors, n, n'),
+ vals = vals,
strs = strs,
funs = funs,
current = current,
- nested = nested},
- n')
- end
-
-fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n =
- let
- val current =
- case current of
- FFfi _ => raise Fail "Binding inside FFfi"
- | FNormal {cons, constructors, vals, strs, funs} =>
- FNormal {cons = cons,
- constructors = constructors,
- vals = SM.insert (vals, s, n),
- strs = strs,
- funs = funs}
- in
- {cons = cons,
- constructors = constructors,
- vals = IM.insert (vals, n, n),
- strs = strs,
- funs = funs,
- current = current,
- nested = nested}
- end
-
-
-fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
-
-fun lookupValByName ({current, ...} : t) x =
- case current of
- FFfi {mod = m, vals, ...} =>
- (case SM.find (vals, x) of
- NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val"
- | SOME t => EFfi (m, t))
- | FNormal {vals, ...} =>
- case SM.find (vals, x) of
- NONE => raise Fail "Corify.St.lookupValByName"
- | SOME n => ENormal n
-
-fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' =
- let
- val current =
- case current of
- FFfi _ => raise Fail "Binding inside FFfi"
- | FNormal {cons, constructors, vals, strs, funs} =>
- FNormal {cons = cons,
- constructors = SM.insert (constructors, s, n'),
- vals = vals,
- strs = strs,
- funs = funs}
- in
- {cons = cons,
- constructors = IM.insert (constructors, n, n'),
- vals = vals,
- strs = strs,
- funs = funs,
- current = current,
- nested = nested}
- end
-
-fun lookupConstructorById ({constructors, ...} : t) n =
- case IM.find (constructors, n) of
- NONE => raise Fail "Corify.St.lookupConstructorById"
- | SOME x => x
-
-fun lookupConstructorByNameOpt ({current, ...} : t) x =
- case current of
- FFfi {mod = m, constructors, ...} =>
- (case SM.find (constructors, x) of
+ nested = nested}
+ end
+
+ fun lookupConstructorById ({constructors, ...} : t) n =
+ case IM.find (constructors, n) of
+ NONE => raise Fail "Corify.St.lookupConstructorById"
+ | SOME x => x
+
+ fun lookupConstructorByNameOpt ({current, ...} : t) x =
+ case current of
+ FFfi {mod = m, constructors, ...} =>
+ (case SM.find (constructors, x) of
+ NONE => NONE
+ | SOME (n, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk}))
+ | FNormal {constructors, ...} =>
+ case SM.find (constructors, x) of
NONE => NONE
- | SOME (n, to) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to}))
- | FNormal {constructors, ...} =>
- case SM.find (constructors, x) of
- NONE => NONE
- | SOME n => SOME n
-
-fun lookupConstructorByName ({current, ...} : t) x =
- case current of
- FFfi {mod = m, constructors, ...} =>
- (case SM.find (constructors, x) of
- NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
- | SOME (n, to) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to})
- | FNormal {constructors, ...} =>
- case SM.find (constructors, x) of
- NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
- | SOME n => n
-
-fun enter {cons, constructors, vals, strs, funs, current, nested} =
- {cons = cons,
- constructors = constructors,
- vals = vals,
- strs = strs,
- funs = funs,
- current = FNormal {cons = SM.empty,
- constructors = SM.empty,
- vals = SM.empty,
- strs = SM.empty,
- funs = SM.empty},
- nested = current :: nested}
-
-fun dummy f = {cons = IM.empty,
- constructors = IM.empty,
- vals = IM.empty,
- strs = IM.empty,
- funs = IM.empty,
- current = f,
- nested = []}
-
-fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
- {outer = {cons = cons,
- constructors = constructors,
- vals = vals,
- strs = strs,
- funs = funs,
- current = m1,
- nested = rest},
- inner = dummy current}
- | leave _ = raise Fail "Corify.St.leave"
-
-fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors})
-
-fun bindStr ({cons, constructors, vals, strs, funs,
- current = FNormal {cons = mcons, constructors = mconstructors,
- vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
- x n ({current = f, ...} : t) =
- {cons = cons,
- constructors = constructors,
- vals = vals,
- strs = IM.insert (strs, n, f),
- funs = funs,
- current = FNormal {cons = mcons,
- constructors = mconstructors,
- vals = mvals,
- strs = SM.insert (mstrs, x, f),
- funs = mfuns},
- nested = nested}
- | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
-
-fun lookupStrById ({strs, ...} : t) n =
- case IM.find (strs, n) of
- NONE => raise Fail "Corify.St.lookupStrById"
- | SOME f => dummy f
-
-fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) =
- (case SM.find (strs, m) of
- NONE => raise Fail "Corify.St.lookupStrByName"
- | SOME f => dummy f)
- | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
-
-fun bindFunctor ({cons, constructors, vals, strs, funs,
- current = FNormal {cons = mcons, constructors = mconstructors,
- vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
- x n xa na str =
- {cons = cons,
- constructors = constructors,
- vals = vals,
- strs = strs,
- funs = IM.insert (funs, n, (xa, na, str)),
- current = FNormal {cons = mcons,
- constructors = mconstructors,
- vals = mvals,
- strs = mstrs,
- funs = SM.insert (mfuns, x, (xa, na, str))},
- nested = nested}
- | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
-
-fun lookupFunctorById ({funs, ...} : t) n =
- case IM.find (funs, n) of
- NONE => raise Fail "Corify.St.lookupFunctorById"
- | SOME v => v
-
-fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
- (case SM.find (funs, m) of
- NONE => raise Fail "Corify.St.lookupFunctorByName"
- | SOME v => v)
- | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName"
-
-end
-
-
-fun corifyKind (k, loc) =
- case k of
- L.KType => (L'.KType, loc)
- | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc)
- | L.KName => (L'.KName, loc)
- | L.KRecord k => (L'.KRecord (corifyKind k), loc)
- | L.KUnit => (L'.KUnit, 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.TRecord c => (L'.TRecord (corifyCon st c), loc)
-
- | L.CRel n => (L'.CRel n, loc)
- | L.CNamed n =>
- (case St.lookupConById st n of
- NONE => (L'.CNamed n, loc)
- | SOME n => (L'.CNamed n, loc))
- | L.CModProj (m, ms, x) =>
- let
- val st = St.lookupStrById st m
- val st = foldl St.lookupStrByName st ms
- in
- case St.lookupConByName st x of
- St.CNormal n => (L'.CNamed n, loc)
- | St.CFfi m => (L'.CFfi (m, x), loc)
- end
-
- | 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.CName s => (L'.CName s, loc)
-
- | L.CRecord (k, xcs) =>
- (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
- | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
- | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
- | L.CUnit => (L'.CUnit, loc)
-
-fun corifyPatCon st pc =
- case pc of
- L.PConVar n => St.lookupConstructorById st n
- | L.PConProj (m1, ms, x) =>
- let
- val st = St.lookupStrById st m1
- val st = foldl St.lookupStrByName st ms
- in
- St.lookupConstructorByName st x
- end
-
-fun corifyPat st (p, loc) =
- case p of
- L.PWild => (L'.PWild, loc)
- | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
- | L.PPrim p => (L'.PPrim p, loc)
- | L.PCon (pc, po) => (L'.PCon (corifyPatCon st pc, Option.map (corifyPat st) po), loc)
- | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
-
-fun corifyExp st (e, loc) =
- case e of
- L.EPrim p => (L'.EPrim p, loc)
- | L.ERel n => (L'.ERel n, loc)
- | L.ENamed n =>
- (case St.lookupValById st n of
- NONE => (L'.ENamed n, loc)
- | SOME n => (L'.ENamed n, loc))
- | L.EModProj (m, ms, x) =>
- let
- val st = St.lookupStrById st m
- val st = foldl St.lookupStrByName st ms
- in
- case St.lookupConstructorByNameOpt st x of
- SOME (pc as L'.PConFfi {mod = m, datatyp, arg, ...}) =>
- (case arg of
- NONE => (L'.ECon (pc, NONE), loc)
- | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
- (L'.ECon (pc, SOME (L'.ERel 0, loc)), loc)), loc))
- | _ =>
- case St.lookupValByName st x of
- St.ENormal n => (L'.ENamed n, loc)
- | St.EFfi (m, t) =>
- case t of
- (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) =>
- (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc)
- | t as (L'.TFun _, _) =>
- let
- fun getArgs (all as (t, _), args) =
- case t of
- L'.TFun (dom, ran) => getArgs (ran, dom :: args)
- | _ => (all, rev args)
-
- val (result, args) = getArgs (t, [])
-
- val (actuals, _) = foldr (fn (_, (actuals, n)) =>
- ((L'.ERel n, loc) :: actuals,
- n + 1)) ([], 0) args
- val app = (L'.EFfiApp (m, x, actuals), loc)
- val (abs, _, _) = foldr (fn (t, (abs, ran, n)) =>
- ((L'.EAbs ("arg" ^ Int.toString n,
- t,
- ran,
- abs), loc),
- (L'.TFun (t, ran), loc),
- n - 1)) (app, result, length args - 1) args
- in
- abs
- end
- | _ => (L'.EFfi (m, x), loc)
- end
- | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), 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.ERecord xes => (L'.ERecord (map (fn (c, e, t) =>
- (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
- | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
- {field = corifyCon st field, rest = corifyCon st rest}), loc)
- | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
- {field = corifyCon st field, rest = corifyCon st rest}), loc)
- | L.EFold k => (L'.EFold (corifyKind k), loc)
-
- | L.ECase (e, pes, {disc, result}) =>
- (L'.ECase (corifyExp st e,
- map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
- {disc = corifyCon st disc, result = corifyCon st result}),
- loc)
-
- | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
-
-fun corifyDecl ((d, loc : EM.span), st) =
- case d of
- L.DCon (x, n, k, c) =>
- let
- val (st, n) = St.bindCon st x n
- in
- ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
- end
- | L.DDatatype (x, n, xncs) =>
- let
- val (st, n) = St.bindCon st x n
- val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
- let
- val st = St.bindConstructor st x n (L'.PConVar n)
- val st = St.bindConstructorVal st x n
- val co = Option.map (corifyCon st) co
- in
- ((x, n, co), st)
- end) st xncs
-
- val t = (L'.CNamed n, loc)
- val dcons = map (fn (x, n, to) =>
- let
- val (e, t) =
- case to of
- NONE => ((L'.ECon (L'.PConVar n, NONE), loc), t)
- | SOME t' => ((L'.EAbs ("x", t', t,
- (L'.ECon (L'.PConVar n, SOME (L'.ERel 0, loc)), loc)),
- loc),
- (L'.TFun (t', t), loc))
- in
- (L'.DVal (x, n, t, e, ""), loc)
- end) xncs
- in
- ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
- end
- | L.DDatatypeImp (x, n, m1, ms, s, xncs) =>
- let
- val (st, n) = St.bindCon st x n
- val c = corifyCon st (L.CModProj (m1, ms, s), loc)
-
- val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
- val (_, {inner, ...}) = corifyStr (m, st)
-
- val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
- let
- val n' = St.lookupConstructorByName inner x
- val st = St.bindConstructor st x n n'
- val (st, n) = St.bindVal st x n
- val co = Option.map (corifyCon st) co
- in
- ((x, n, co), st)
- end) st xncs
-
- val cds = map (fn (x, n, co) =>
- let
- val t = case co of
- NONE => c
- | SOME t' => (L'.TFun (t', c), loc)
- val e = corifyExp st (L.EModProj (m1, ms, x), loc)
- in
- (L'.DVal (x, n, t, e, x), loc)
- end) xncs
- in
- ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st)
- end
- | L.DVal (x, n, t, e) =>
- let
- val (st, n) = St.bindVal st x n
- val s =
- if String.isPrefix "wrap_" x then
- String.extract (x, 5, NONE)
- else
- x
- in
- ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st)
- end
- | L.DValRec vis =>
- let
- val (vis, st) = ListUtil.foldlMap
- (fn ((x, n, t, e), st) =>
+ | SOME n => SOME n
+
+ fun lookupConstructorByName ({current, ...} : t) x =
+ case current of
+ FFfi {mod = m, constructors, ...} =>
+ (case SM.find (constructors, x) of
+ NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
+ | SOME (n, to, dk) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk})
+ | FNormal {constructors, ...} =>
+ case SM.find (constructors, x) of
+ NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
+ | SOME n => n
+
+ fun enter {cons, constructors, vals, strs, funs, current, nested} =
+ {cons = cons,
+ constructors = constructors,
+ vals = vals,
+ strs = strs,
+ funs = funs,
+ current = FNormal {cons = SM.empty,
+ constructors = SM.empty,
+ vals = SM.empty,
+ strs = SM.empty,
+ funs = SM.empty},
+ nested = current :: nested}
+
+ fun dummy f = {cons = IM.empty,
+ constructors = IM.empty,
+ vals = IM.empty,
+ strs = IM.empty,
+ funs = IM.empty,
+ current = f,
+ nested = []}
+
+ fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
+ {outer = {cons = cons,
+ constructors = constructors,
+ vals = vals,
+ strs = strs,
+ funs = funs,
+ current = m1,
+ nested = rest},
+ inner = dummy current}
+ | leave _ = raise Fail "Corify.St.leave"
+
+ fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors})
+
+ fun bindStr ({cons, constructors, vals, strs, funs,
+ current = FNormal {cons = mcons, constructors = mconstructors,
+ vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
+ x n ({current = f, ...} : t) =
+ {cons = cons,
+ constructors = constructors,
+ vals = vals,
+ strs = IM.insert (strs, n, f),
+ funs = funs,
+ current = FNormal {cons = mcons,
+ constructors = mconstructors,
+ vals = mvals,
+ strs = SM.insert (mstrs, x, f),
+ funs = mfuns},
+ nested = nested}
+ | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
+
+ fun lookupStrById ({strs, ...} : t) n =
+ case IM.find (strs, n) of
+ NONE => raise Fail "Corify.St.lookupStrById"
+ | SOME f => dummy f
+
+ fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) =
+ (case SM.find (strs, m) of
+ NONE => raise Fail "Corify.St.lookupStrByName"
+ | SOME f => dummy f)
+ | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
+
+ fun bindFunctor ({cons, constructors, vals, strs, funs,
+ current = FNormal {cons = mcons, constructors = mconstructors,
+ vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
+ x n xa na str =
+ {cons = cons,
+ constructors = constructors,
+ vals = vals,
+ strs = strs,
+ funs = IM.insert (funs, n, (xa, na, str)),
+ current = FNormal {cons = mcons,
+ constructors = mconstructors,
+ vals = mvals,
+ strs = mstrs,
+ funs = SM.insert (mfuns, x, (xa, na, str))},
+ nested = nested}
+ | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
+
+ fun lookupFunctorById ({funs, ...} : t) n =
+ case IM.find (funs, n) of
+ NONE => raise Fail "Corify.St.lookupFunctorById"
+ | SOME v => v
+
+ fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
+ (case SM.find (funs, m) of
+ NONE => raise Fail "Corify.St.lookupFunctorByName"
+ | SOME v => v)
+ | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName"
+
+ end
+
+
+ fun corifyKind (k, loc) =
+ case k of
+ L.KType => (L'.KType, loc)
+ | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc)
+ | L.KName => (L'.KName, loc)
+ | L.KRecord k => (L'.KRecord (corifyKind k), loc)
+ | L.KUnit => (L'.KUnit, 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.TRecord c => (L'.TRecord (corifyCon st c), loc)
+
+ | L.CRel n => (L'.CRel n, loc)
+ | L.CNamed n =>
+ (case St.lookupConById st n of
+ NONE => (L'.CNamed n, loc)
+ | SOME n => (L'.CNamed n, loc))
+ | L.CModProj (m, ms, x) =>
+ let
+ val st = St.lookupStrById st m
+ val st = foldl St.lookupStrByName st ms
+ in
+ case St.lookupConByName st x of
+ St.CNormal n => (L'.CNamed n, loc)
+ | St.CFfi m => (L'.CFfi (m, x), loc)
+ end
+
+ | 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.CName s => (L'.CName s, loc)
+
+ | L.CRecord (k, xcs) =>
+ (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
+ | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
+ | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
+ | L.CUnit => (L'.CUnit, loc)
+
+ fun corifyPatCon st pc =
+ case pc of
+ L.PConVar n => St.lookupConstructorById st n
+ | L.PConProj (m1, ms, x) =>
+ let
+ val st = St.lookupStrById st m1
+ val st = foldl St.lookupStrByName st ms
+ in
+ St.lookupConstructorByName st x
+ end
+
+ fun corifyPat st (p, loc) =
+ case p of
+ L.PWild => (L'.PWild, loc)
+ | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
+ | L.PPrim p => (L'.PPrim p, loc)
+ | L.PCon (dk, pc, po) => (L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), loc)
+ | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
+
+ fun corifyExp st (e, loc) =
+ case e of
+ L.EPrim p => (L'.EPrim p, loc)
+ | L.ERel n => (L'.ERel n, loc)
+ | L.ENamed n =>
+ (case St.lookupValById st n of
+ NONE => (L'.ENamed n, loc)
+ | SOME n => (L'.ENamed n, loc))
+ | L.EModProj (m, ms, x) =>
+ let
+ val st = St.lookupStrById st m
+ val st = foldl St.lookupStrByName st ms
+ in
+ case St.lookupConstructorByNameOpt st x of
+ SOME (pc as L'.PConFfi {mod = m, datatyp, arg, kind, ...}) =>
+ (case arg of
+ NONE => (L'.ECon (kind, pc, NONE), loc)
+ | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
+ (L'.ECon (kind, pc, SOME (L'.ERel 0, loc)), loc)), loc))
+ | _ =>
+ case St.lookupValByName st x of
+ St.ENormal n => (L'.ENamed n, loc)
+ | St.EFfi (m, t) =>
+ case t of
+ (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) =>
+ (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc)
+ | t as (L'.TFun _, _) =>
+ let
+ fun getArgs (all as (t, _), args) =
+ case t of
+ L'.TFun (dom, ran) => getArgs (ran, dom :: args)
+ | _ => (all, rev args)
+
+ val (result, args) = getArgs (t, [])
+
+ val (actuals, _) = foldr (fn (_, (actuals, n)) =>
+ ((L'.ERel n, loc) :: actuals,
+ n + 1)) ([], 0) args
+ val app = (L'.EFfiApp (m, x, actuals), loc)
+ val (abs, _, _) = foldr (fn (t, (abs, ran, n)) =>
+ ((L'.EAbs ("arg" ^ Int.toString n,
+ t,
+ ran,
+ abs), loc),
+ (L'.TFun (t, ran), loc),
+ n - 1)) (app, result, length args - 1) args
+ in
+ abs
+ end
+ | _ => (L'.EFfi (m, x), loc)
+ end
+ | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), 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.ERecord xes => (L'.ERecord (map (fn (c, e, t) =>
+ (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
+ | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
+ {field = corifyCon st field, rest = corifyCon st rest}), loc)
+ | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
+ {field = corifyCon st field, rest = corifyCon st rest}), loc)
+ | L.EFold k => (L'.EFold (corifyKind k), loc)
+
+ | L.ECase (e, pes, {disc, result}) =>
+ (L'.ECase (corifyExp st e,
+ map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
+ {disc = corifyCon st disc, result = corifyCon st result}),
+ loc)
+
+ | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
+
+ fun corifyDecl ((d, loc : EM.span), st) =
+ case d of
+ L.DCon (x, n, k, c) =>
+ let
+ val (st, n) = St.bindCon st x n
+ in
+ ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
+ end
+ | L.DDatatype (x, n, xncs) =>
+ let
+ val (st, n) = St.bindCon st x n
+ val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
+ let
+ val st = St.bindConstructor st x n (L'.PConVar n)
+ val st = St.bindConstructorVal st x n
+ val co = Option.map (corifyCon st) co
+ in
+ ((x, n, co), st)
+ end) st xncs
+
+ val dk = CoreUtil.classifyDatatype xncs
+ val t = (L'.CNamed n, loc)
+ val dcons = map (fn (x, n, to) =>
+ let
+ val (e, t) =
+ case to of
+ NONE => ((L'.ECon (dk, L'.PConVar n, NONE), loc), t)
+ | SOME t' => ((L'.EAbs ("x", t', t,
+ (L'.ECon (dk, L'.PConVar n, SOME (L'.ERel 0, loc)),
+ loc)),
+ loc),
+ (L'.TFun (t', t), loc))
+ in
+ (L'.DVal (x, n, t, e, ""), loc)
+ end) xncs
+ in
+ ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
+ end
+ | L.DDatatypeImp (x, n, m1, ms, s, xncs) =>
+ let
+ val (st, n) = St.bindCon st x n
+ val c = corifyCon st (L.CModProj (m1, ms, s), loc)
+
+ val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
+ val (_, {inner, ...}) = corifyStr (m, st)
+
+ val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
+ let
+ val n' = St.lookupConstructorByName inner x
+ val st = St.bindConstructor st x n n'
+ val (st, n) = St.bindVal st x n
+ val co = Option.map (corifyCon st) co
+ in
+ ((x, n, co), st)
+ end) st xncs
+
+ val cds = map (fn (x, n, co) =>
+ let
+ val t = case co of
+ NONE => c
+ | SOME t' => (L'.TFun (t', c), loc)
+ val e = corifyExp st (L.EModProj (m1, ms, x), loc)
+ in
+ (L'.DVal (x, n, t, e, x), loc)
+ end) xncs
+ in
+ ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st)
+ end
+ | L.DVal (x, n, t, e) =>
+ let
+ val (st, n) = St.bindVal st x n
+ val s =
+ if String.isPrefix "wrap_" x then
+ String.extract (x, 5, NONE)
+ else
+ x
+ in
+ ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st)
+ end
+ | L.DValRec vis =>
+ let
+ val (vis, st) = ListUtil.foldlMap
+ (fn ((x, n, t, e), st) =>
+ let
+ val (st, n) = St.bindVal st x n
+ in
+ ((x, n, t, e), st)
+ end)
+ st vis
+
+ val vis = map
+ (fn (x, n, t, e) =>
+ let
+ val s =
+ if String.isPrefix "wrap_" x then
+ String.extract (x, 5, NONE)
+ else
+ x
+ in
+ (x, n, corifyCon st t, corifyExp st e, s)
+ end)
+ vis
+ in
+ ([(L'.DValRec vis, loc)], st)
+ end
+ | L.DSgn _ => ([], st)
+
+ | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
+ ([], St.bindFunctor st x n xa na str)
+
+ | L.DStr (x, n, _, str) =>
+ let
+ val (ds, {inner, outer}) = corifyStr (str, st)
+ val st = St.bindStr outer x n inner
+ in
+ (ds, st)
+ end
+
+ | L.DFfiStr (m, n, (sgn, _)) =>
+ (case sgn of
+ L.SgnConst sgis =>
+ let
+ val (ds, cmap, conmap, st) =
+ foldl (fn ((sgi, _), (ds, cmap, conmap, st)) =>
+ case sgi of
+ L.SgiConAbs (x, n, k) =>
let
- val (st, n) = St.bindVal st x n
+ val (st, n') = St.bindCon st x n
in
- ((x, n, t, e), st)
- end)
- st vis
-
- val vis = map
- (fn (x, n, t, e) =>
- let
- val s =
- if String.isPrefix "wrap_" x then
- String.extract (x, 5, NONE)
- else
- x
- in
- (x, n, corifyCon st t, corifyExp st e, s)
- end)
- vis
- in
- ([(L'.DValRec vis, loc)], st)
- end
- | L.DSgn _ => ([], st)
-
- | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
- ([], St.bindFunctor st x n xa na str)
-
- | L.DStr (x, n, _, str) =>
- let
- val (ds, {inner, outer}) = corifyStr (str, st)
- val st = St.bindStr outer x n inner
- in
- (ds, st)
- end
-
- | L.DFfiStr (m, n, (sgn, _)) =>
- (case sgn of
- L.SgnConst sgis =>
- let
- val (ds, cmap, conmap, st) =
- foldl (fn ((sgi, _), (ds, cmap, conmap, st)) =>
- case sgi of
- L.SgiConAbs (x, n, k) =>
- let
- val (st, n') = St.bindCon st x n
- in
- ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
- cmap,
- conmap,
- st)
- end
- | L.SgiCon (x, n, k, _) =>
- let
- val (st, n') = St.bindCon st x n
- in
- ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
- cmap,
- conmap,
- st)
- end
+ ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
+ cmap,
+ conmap,
+ st)
+ end
+ | L.SgiCon (x, n, k, _) =>
+ let
+ val (st, n') = St.bindCon st x n
+ in
+ ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
+ cmap,
+ conmap,
+ st)
+ end
- | L.SgiDatatype (x, n, xnts) =>
- let
- val (st, n') = St.bindCon st x n
- val (xnts, (ds', st, cmap, conmap)) =
- ListUtil.foldlMap
- (fn ((x', n, to), (ds', st, cmap, conmap)) =>
- let
- val dt = (L'.CNamed n', loc)
-
- val to = Option.map (corifyCon st) to
-
- val pc = L'.PConFfi {mod = m,
- datatyp = x,
- con = x',
- arg = to}
-
- val (cmap, d) =
- case to of
- NONE => (SM.insert (cmap, x', dt),
- (L'.DVal (x', n, dt,
- (L'.ECon (pc, NONE), loc),
- ""), loc))
- | SOME t =>
- let
- val tf = (L'.TFun (t, dt), loc)
- val d = (L'.DVal (x', n, tf,
- (L'.EAbs ("x", t, tf,
- (L'.ECon (pc,
- SOME (L'.ERel 0,
+ | L.SgiDatatype (x, n, xnts) =>
+ let
+ val dk = ExplUtil.classifyDatatype xnts
+ val (st, n') = St.bindCon st x n
+ val (xnts, (ds', st, cmap, conmap)) =
+ ListUtil.foldlMap
+ (fn ((x', n, to), (ds', st, cmap, conmap)) =>
+ let
+ val dt = (L'.CNamed n', loc)
+
+ val to = Option.map (corifyCon st) to
+
+ val pc = L'.PConFfi {mod = m,
+ datatyp = x,
+ con = x',
+ arg = to,
+ kind = dk}
+
+ val (cmap, d) =
+ case to of
+ NONE => (SM.insert (cmap, x', dt),
+ (L'.DVal (x', n, dt,
+ (L'.ECon (dk, pc, NONE), loc),
+ ""), loc))
+ | SOME t =>
+ let
+ val tf = (L'.TFun (t, dt), loc)
+ val d = (L'.DVal (x', n, tf,
+ (L'.EAbs ("x", t, tf,
+ (L'.ECon (dk, pc,
+ SOME (L'.ERel 0,
loc)),
loc)), loc), ""), loc)
in
@@ -684,7 +688,7 @@ fun corifyDecl ((d, loc : EM.span), st) =
val st = St.bindConstructor st x' n pc
(*val st = St.bindConstructorVal st x' n*)
- val conmap = SM.insert (conmap, x', (x, to))
+ val conmap = SM.insert (conmap, x', (x, to, dk))
in
((x', n, to),
(d :: ds', st, cmap, conmap))
diff --git a/src/elab.sml b/src/elab.sml
index fb67556b..2bf64f5a 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -71,6 +71,10 @@ datatype con' =
withtype con = con' located
+datatype datatype_kind =
+ Enum
+ | Default
+
datatype patCon =
PConVar of int
| PConProj of int * string list * string
@@ -79,7 +83,7 @@ datatype pat' =
PWild
| PVar of string * con
| PPrim of Prim.t
- | PCon of patCon * pat option
+ | PCon of datatype_kind * patCon * pat option
| PRecord of (string * pat * con) list
withtype pat = pat' located
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 229436ec..f341bed2 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -57,7 +57,7 @@ signature ELAB_ENV = sig
val lookupDatatypeConstructor : datatyp -> int -> string * Elab.con option
val constructors : datatyp -> (string * int * Elab.con option) list
- val lookupConstructor : env -> string -> (int * Elab.con option * int) option
+ val lookupConstructor : env -> string -> (Elab.datatype_kind * int * Elab.con option * int) option
val pushERel : env -> string -> Elab.con -> env
val lookupERel : env -> int -> string * Elab.con
@@ -89,7 +89,7 @@ signature ELAB_ENV = sig
val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
-> (string * int * Elab.con option) list option
val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
- -> (int * Elab.con option * Elab.con) option
+ -> (Elab.datatype_kind * int * Elab.con option * Elab.con) option
val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option
val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 0367e023..23b29155 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -81,7 +81,7 @@ type env = {
namedC : (string * kind * con option) IM.map,
datatypes : datatyp IM.map,
- constructors : (int * con option * int) SM.map,
+ constructors : (datatype_kind * int * con option * int) SM.map,
renameE : con var' SM.map,
relE : (string * con) list,
@@ -189,26 +189,30 @@ fun lookupC (env : env) x =
| SOME (Named' x) => Named x
fun pushDatatype (env : env) n xncs =
- {renameC = #renameC env,
- relC = #relC env,
- namedC = #namedC env,
+ let
+ val dk = U.classifyDatatype xncs
+ in
+ {renameC = #renameC env,
+ relC = #relC env,
+ namedC = #namedC env,
- datatypes = IM.insert (#datatypes env, n,
- foldl (fn ((x, n, to), cons) =>
- IM.insert (cons, n, (x, to))) IM.empty xncs),
- constructors = foldl (fn ((x, n', to), cmap) =>
- SM.insert (cmap, x, (n', to, n)))
- (#constructors env) xncs,
+ datatypes = IM.insert (#datatypes env, n,
+ foldl (fn ((x, n, to), cons) =>
+ IM.insert (cons, n, (x, to))) IM.empty xncs),
+ constructors = foldl (fn ((x, n', to), cmap) =>
+ SM.insert (cmap, x, (dk, n', to, n)))
+ (#constructors env) xncs,
- renameE = #renameE env,
- relE = #relE env,
- namedE = #namedE env,
+ renameE = #renameE env,
+ relE = #relE env,
+ namedE = #namedE env,
- renameSgn = #renameSgn env,
- sgn = #sgn env,
+ renameSgn = #renameSgn env,
+ sgn = #sgn env,
- renameStr = #renameStr env,
- str = #str env}
+ renameStr = #renameStr env,
+ str = #str env}
+ end
fun lookupDatatype (env : env) n =
case IM.find (#datatypes env, n) of
@@ -579,13 +583,14 @@ fun projectConstructor env {sgn, str, field} =
if x <> field then
NONE
else
- SOME (n', to, (CNamed n, #2 str))) xncs
+ SOME (U.classifyDatatype xncs, n', to, (CNamed n, #2 str))) xncs
in
case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs)
| SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs)
| _ => NONE) sgis of
NONE => NONE
- | SOME ((n, to, t), subs) => SOME (n, Option.map (sgnSubCon (str, subs)) to, sgnSubCon (str, subs) t)
+ | SOME ((dk, n, to, t), subs) => SOME (dk, n, Option.map (sgnSubCon (str, subs)) to,
+ sgnSubCon (str, subs) t)
end
| _ => NONE
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 93d4f7e2..122c6c02 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -216,10 +216,10 @@ fun p_pat' par env (p, _) =
PWild => string "_"
| PVar (s, _) => string s
| PPrim p => Prim.p_t p
- | PCon (pc, NONE) => p_patCon env pc
- | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc,
- space,
- p_pat' true env p])
+ | PCon (_, pc, NONE) => p_patCon env pc
+ | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc,
+ space,
+ p_pat' true env p])
| PRecord xps =>
box [string "{",
p_list_sep (box [string ",", space]) (fn (x, p, _) =>
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 1ecd6201..5be47ed6 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -27,6 +27,8 @@
signature ELAB_UTIL = sig
+val classifyDatatype : (string * int * Elab.con option) list -> Elab.datatype_kind
+
structure Kind : sig
val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder
-> (Elab.kind, 'state, 'abort) Search.mapfolder
diff --git a/src/elab_util.sml b/src/elab_util.sml
index a3754153..d8dd16b8 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -29,6 +29,12 @@ structure ElabUtil :> ELAB_UTIL = struct
open Elab
+fun classifyDatatype xncs =
+ if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+ Enum
+ else
+ Default
+
structure S = Search
structure Kind = struct
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 54af8dab..c999f844 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -933,22 +933,21 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) =
val pterror = (perror, terror)
val rerror = (pterror, (env, bound))
- fun pcon (pc, po, to, dn) =
-
- case (po, to) of
- (NONE, SOME _) => (expError env (PatHasNoArg loc);
- rerror)
- | (SOME _, NONE) => (expError env (PatHasArg loc);
- rerror)
- | (NONE, NONE) => (((L'.PCon (pc, NONE), loc), dn),
- (env, bound))
- | (SOME p, SOME t) =>
- let
- val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
- in
- (((L'.PCon (pc, SOME p'), loc), dn),
- (env, bound))
- end
+ fun pcon (pc, po, to, dn, dk) =
+ case (po, to) of
+ (NONE, SOME _) => (expError env (PatHasNoArg loc);
+ rerror)
+ | (SOME _, NONE) => (expError env (PatHasArg loc);
+ rerror)
+ | (NONE, NONE) => (((L'.PCon (dk, pc, NONE), loc), dn),
+ (env, bound))
+ | (SOME p, SOME t) =>
+ let
+ val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
+ in
+ (((L'.PCon (dk, pc, SOME p'), loc), dn),
+ (env, bound))
+ end
in
case p of
L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))),
@@ -970,7 +969,7 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) =
(case E.lookupConstructor env x of
NONE => (expError env (UnboundConstructor (loc, [], x));
rerror)
- | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, (L'.CNamed dn, loc)))
+ | SOME (dk, n, to, dn) => pcon (L'.PConVar n, po, to, (L'.CNamed dn, loc), dk))
| L.PCon (m1 :: ms, x, po) =>
(case E.lookupStr env m1 of
NONE => (expError env (UnboundStrInExp (loc, m1));
@@ -986,7 +985,7 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) =
case E.projectConstructor env {str = str, sgn = sgn, field = x} of
NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
rerror)
- | SOME (_, to, dn) => pcon (L'.PConProj (n, ms, x), po, to, dn)
+ | SOME (dk, _, to, dn) => pcon (L'.PConProj (n, ms, x), po, to, dn, dk)
end)
| L.PRecord (xps, flex) =>
@@ -1036,7 +1035,7 @@ fun exhaustive (env, denv, t, ps) =
in
case E.projectConstructor env {str = str, sgn = sgn, field = x} of
NONE => raise Fail "exhaustive: Can't project constructor"
- | SOME (n, _, _) => n
+ | SOME (_, n, _, _) => n
end
fun coverage (p, _) =
@@ -1044,8 +1043,8 @@ fun exhaustive (env, denv, t, ps) =
L'.PWild => Wild
| L'.PVar _ => Wild
| L'.PPrim _ => None
- | L'.PCon (pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
- | L'.PCon (pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
+ | L'.PCon (_, pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
+ | L'.PCon (_, pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
| L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) =>
SM.insert (fmap, x, coverage p)) SM.empty xps]
diff --git a/src/expl.sml b/src/expl.sml
index c561ff29..9fea3f19 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -59,6 +59,8 @@ datatype con' =
withtype con = con' located
+datatype datatype_kind = datatype Elab.datatype_kind
+
datatype patCon =
PConVar of int
| PConProj of int * string list * string
@@ -67,7 +69,7 @@ datatype pat' =
PWild
| PVar of string * con
| PPrim of Prim.t
- | PCon of patCon * pat option
+ | PCon of datatype_kind * patCon * pat option
| PRecord of (string * pat * con) list
withtype pat = pat' located
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 24bbd6c0..1056dfe4 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -181,10 +181,10 @@ fun p_pat' par env (p, _) =
PWild => string "_"
| PVar (s, _) => string s
| PPrim p => Prim.p_t p
- | PCon (pc, NONE) => p_patCon env pc
- | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc,
- space,
- p_pat' true env p])
+ | PCon (_, pc, NONE) => p_patCon env pc
+ | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc,
+ space,
+ p_pat' true env p])
| PRecord xps =>
box [string "{",
p_list_sep (box [string ",", space]) (fn (x, p, _) =>
diff --git a/src/expl_util.sig b/src/expl_util.sig
index 2a6c7abe..d15e7a76 100644
--- a/src/expl_util.sig
+++ b/src/expl_util.sig
@@ -27,6 +27,8 @@
signature EXPL_UTIL = sig
+val classifyDatatype : (string * int * Expl.con option) list -> Expl.datatype_kind
+
structure Kind : sig
val mapfold : (Expl.kind', 'state, 'abort) Search.mapfolder
-> (Expl.kind, 'state, 'abort) Search.mapfolder
diff --git a/src/expl_util.sml b/src/expl_util.sml
index 290c64f5..481a96b0 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -29,6 +29,12 @@ structure ExplUtil :> EXPL_UTIL = struct
open Expl
+fun classifyDatatype xncs =
+ if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+ Enum
+ else
+ Default
+
structure S = Search
structure Kind = struct
diff --git a/src/explify.sml b/src/explify.sml
index 90737f07..847fbc60 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -81,7 +81,7 @@ fun explifyPat (p, loc) =
L.PWild => (L'.PWild, loc)
| L.PVar (x, t) => (L'.PVar (x, explifyCon t), loc)
| L.PPrim p => (L'.PPrim p, loc)
- | L.PCon (pc, po) => (L'.PCon (explifyPatCon pc, Option.map explifyPat po), loc)
+ | L.PCon (dk, pc, po) => (L'.PCon (dk, explifyPatCon pc, Option.map explifyPat po), loc)
| L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, explifyPat p, explifyCon t)) xps), loc)
fun explifyExp (e, loc) =
diff --git a/src/mono.sml b/src/mono.sml
index 7cc0dc78..b19f5af6 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -29,10 +29,12 @@ structure Mono = struct
type 'a located = 'a ErrorMsg.located
+datatype datatype_kind = datatype Core.datatype_kind
+
datatype typ' =
TFun of typ * typ
| TRecord of (string * typ) list
- | TDatatype of int * (string * int * typ option) list
+ | TDatatype of datatype_kind * int * (string * int * typ option) list
| TFfi of string * string
withtype typ = typ' located
@@ -45,7 +47,7 @@ datatype pat' =
PWild
| PVar of string * typ
| PPrim of Prim.t
- | PCon of patCon * pat option
+ | PCon of datatype_kind * patCon * pat option
| PRecord of (string * pat * typ) list
withtype pat = pat' located
@@ -54,7 +56,7 @@ datatype exp' =
EPrim of Prim.t
| ERel of int
| ENamed of int
- | ECon of patCon * exp option
+ | ECon of datatype_kind * patCon * exp option
| EFfi of string * string
| EFfiApp of string * string * exp list
| EApp of exp * exp
diff --git a/src/mono_env.sml b/src/mono_env.sml
index f5f1f3d9..3beced1c 100644
--- a/src/mono_env.sml
+++ b/src/mono_env.sml
@@ -98,9 +98,10 @@ fun declBinds env (d, loc) =
DDatatype (x, n, xncs) =>
let
val env = pushDatatype env x n xncs
+ val dt = (TDatatype (MonoUtil.classifyDatatype xncs, n, xncs), loc)
in
- foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype (n, xncs), loc) NONE ""
- | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype (n, xncs), loc)), loc) NONE "")
+ foldl (fn ((x', n', NONE), env) => pushENamed env x' n' dt NONE ""
+ | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, dt), loc) NONE "")
env xncs
end
| DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s
@@ -112,8 +113,8 @@ fun patBinds env (p, loc) =
PWild => env
| PVar (x, t) => pushERel env x t NONE
| PPrim _ => env
- | PCon (_, NONE) => env
- | PCon (_, SOME p) => patBinds env p
+ | PCon (_, _, NONE) => env
+ | PCon (_, _, SOME p) => patBinds env p
| PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
end
diff --git a/src/mono_opt.sml b/src/mono_opt.sml
index 77071985..38812167 100644
--- a/src/mono_opt.sml
+++ b/src/mono_opt.sml
@@ -185,13 +185,13 @@ fun exp e =
| EWrite (EFfiApp ("Basis", "urlifyString", [e]), _) =>
EFfiApp ("Basis", "urlifyString_w", [e])
- | EFfiApp ("Basis", "urlifyBool", [(ECon (PConFfi {con = "True", ...}, NONE), _)]) =>
+ | EFfiApp ("Basis", "urlifyBool", [(ECon (Enum, PConFfi {con = "True", ...}, NONE), _)]) =>
EPrim (Prim.String "1")
- | EFfiApp ("Basis", "urlifyBool", [(ECon (PConFfi {con = "False", ...}, NONE), _)]) =>
+ | EFfiApp ("Basis", "urlifyBool", [(ECon (Enum, PConFfi {con = "False", ...}, NONE), _)]) =>
EPrim (Prim.String "0")
- | EWrite (EFfiApp ("Basis", "urlifyBool", [(ECon (PConFfi {con = "True", ...}, NONE), _)]), loc) =>
+ | EWrite (EFfiApp ("Basis", "urlifyBool", [(ECon (Enum, PConFfi {con = "True", ...}, NONE), _)]), loc) =>
EWrite (EPrim (Prim.String "1"), loc)
- | EWrite (EFfiApp ("Basis", "urlifyBool", [(ECon (PConFfi {con = "False", ...}, NONE), _)]), loc) =>
+ | EWrite (EFfiApp ("Basis", "urlifyBool", [(ECon (Enum, PConFfi {con = "False", ...}, NONE), _)]), loc) =>
EWrite (EPrim (Prim.String "0"), loc)
| EWrite (EFfiApp ("Basis", "urlifyBool", [e]), _) =>
EFfiApp ("Basis", "urlifyBool_w", [e])
diff --git a/src/mono_print.sml b/src/mono_print.sml
index 91e48b7f..fc19d8b5 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -53,7 +53,7 @@ fun p_typ' par env (t, _) =
space,
p_typ env t]) xcs,
string "}"]
- | TDatatype (n, _) =>
+ | TDatatype (_, n, _) =>
((if !debug then
string (#1 (E.lookupDatatype env n) ^ "__" ^ Int.toString n)
else
@@ -91,8 +91,8 @@ fun p_pat' par env (p, _) =
PWild => string "_"
| PVar (s, _) => string s
| PPrim p => Prim.p_t p
- | PCon (n, NONE) => p_patCon env n
- | PCon (n, SOME p) => parenIf par (box [p_patCon env n,
+ | PCon (_, n, NONE) => p_patCon env n
+ | PCon (_, n, SOME p) => parenIf par (box [p_patCon env n,
space,
p_pat' true env p])
| PRecord xps =>
@@ -117,10 +117,10 @@ fun p_exp' par env (e, _) =
string (#1 (E.lookupERel env n)))
handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n))
| ENamed n => p_enamed env n
- | ECon (pc, NONE) => p_patCon env pc
- | ECon (pc, SOME e) => parenIf par (box [p_patCon env pc,
- space,
- p_exp' true env e])
+ | ECon (_, pc, NONE) => p_patCon env pc
+ | ECon (_, pc, SOME e) => parenIf par (box [p_patCon env pc,
+ space,
+ p_exp' true env e])
| EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"]
| EFfiApp (m, x, es) => box [string "FFI(",
diff --git a/src/mono_reduce.sml b/src/mono_reduce.sml
index 20d26547..31757daa 100644
--- a/src/mono_reduce.sml
+++ b/src/mono_reduce.sml
@@ -79,25 +79,25 @@ fun match (env, p : pat, e : exp) =
else
NONE
- | (PCon (PConVar n1, NONE), ECon (PConVar n2, NONE)) =>
+ | (PCon (_, PConVar n1, NONE), ECon (_, PConVar n2, NONE)) =>
if n1 = n2 then
SOME env
else
NONE
- | (PCon (PConVar n1, SOME p), ECon (PConVar n2, SOME e)) =>
+ | (PCon (_, PConVar n1, SOME p), ECon (_, PConVar n2, SOME e)) =>
if n1 = n2 then
match (env, p, e)
else
NONE
- | (PCon (PConFfi {mod = m1, con = con1, ...}, NONE), ECon (PConFfi {mod = m2, con = con2, ...}, NONE)) =>
+ | (PCon (_, PConFfi {mod = m1, con = con1, ...}, NONE), ECon (_, PConFfi {mod = m2, con = con2, ...}, NONE)) =>
if m1 = m2 andalso con1 = con2 then
SOME env
else
NONE
- | (PCon (PConFfi {mod = m1, con = con1, ...}, SOME ep), ECon (PConFfi {mod = m2, con = con2, ...}, SOME e)) =>
+ | (PCon (_, PConFfi {mod = m1, con = con1, ...}, SOME ep), ECon (_, PConFfi {mod = m2, con = con2, ...}, SOME e)) =>
if m1 = m2 andalso con1 = con2 then
match (env, p, e)
else
diff --git a/src/mono_shake.sml b/src/mono_shake.sml
index e694c0dd..498a1ac6 100644
--- a/src/mono_shake.sml
+++ b/src/mono_shake.sml
@@ -58,7 +58,7 @@ fun shake file =
fun typ (c, s) =
case c of
- TDatatype (n, _) =>
+ TDatatype (_, n, _) =>
if IS.member (#con s, n) then
s
else
diff --git a/src/mono_util.sig b/src/mono_util.sig
index 4e9d5d91..1e94403f 100644
--- a/src/mono_util.sig
+++ b/src/mono_util.sig
@@ -27,6 +27,8 @@
signature MONO_UTIL = sig
+val classifyDatatype : (string * int * Mono.typ option) list -> Mono.datatype_kind
+
structure Typ : sig
val compare : Mono.typ * Mono.typ -> order
val sortFields : (string * Mono.typ) list -> (string * Mono.typ) list
diff --git a/src/mono_util.sml b/src/mono_util.sml
index 805a1c88..68cbda08 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -29,6 +29,12 @@ structure MonoUtil :> MONO_UTIL = struct
open Mono
+fun classifyDatatype xncs =
+ if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+ Enum
+ else
+ Default
+
structure S = Search
structure Typ = struct
@@ -57,7 +63,7 @@ fun compare ((t1, _), (t2, _)) =
in
joinL compareFields (xts1, xts2)
end
- | (TDatatype (n1, _), TDatatype (n2, _)) => Int.compare (n1, n2)
+ | (TDatatype (_, n1, _), TDatatype (_, n2, _)) => Int.compare (n1, n2)
| (TFfi (m1, x1), TFfi (m2, x2)) => join (String.compare (m1, m2), fn () => String.compare (x1, x2))
| (TFun _, _) => LESS
@@ -141,11 +147,11 @@ fun mapfoldB {typ = fc, exp = fe, bind} =
EPrim _ => S.return2 eAll
| ERel _ => S.return2 eAll
| ENamed _ => S.return2 eAll
- | ECon (_, NONE) => S.return2 eAll
- | ECon (n, SOME e) =>
+ | ECon (_, _, NONE) => S.return2 eAll
+ | ECon (dk, n, SOME e) =>
S.map2 (mfe ctx e,
fn e' =>
- (ECon (n, SOME e'), loc))
+ (ECon (dk, n, SOME e'), loc))
| EFfi _ => S.return2 eAll
| EFfiApp (m, x, es) =>
S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es,
@@ -191,8 +197,8 @@ fun mapfoldB {typ = fc, exp = fe, bind} =
PWild => ctx
| PVar (x, t) => bind (ctx, RelE (x, t))
| PPrim _ => ctx
- | PCon (_, NONE) => ctx
- | PCon (_, SOME p) => pb (p, ctx)
+ | PCon (_, _, NONE) => ctx
+ | PCon (_, _, SOME p) => pb (p, ctx)
| PRecord xps => foldl (fn ((_, p, _), ctx) =>
pb (p, ctx)) ctx xps
in
@@ -355,7 +361,7 @@ fun mapfoldB (all as {bind, ...}) =
DDatatype (x, n, xncs) =>
let
val ctx = bind (ctx, Datatype (x, n, xncs))
- val t = (TDatatype (n, xncs), #2 d')
+ val t = (TDatatype (classifyDatatype xncs, n, xncs), #2 d')
in
foldl (fn ((x, n, to), ctx) =>
let
diff --git a/src/monoize.sml b/src/monoize.sml
index bd7cdcd0..f6e5be6e 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -33,7 +33,7 @@ structure Env = CoreEnv
structure L = Core
structure L' = Mono
-val dummyTyp = (L'.TDatatype (0, []), E.dummySpan)
+val dummyTyp = (L'.TDatatype (L'.Enum, 0, []), E.dummySpan)
fun monoName env (all as (c, loc)) =
let
@@ -73,7 +73,7 @@ fun monoType env (all as (c, loc)) =
val xncs = map (fn (x, n, to) => (x, n, Option.map (monoType env) to)) xncs
in
- (L'.TDatatype (n, xncs), loc)
+ (L'.TDatatype (MonoUtil.classifyDatatype xncs, n, xncs), loc)
end
| L.CFfi mx => (L'.TFfi mx, loc)
| L.CApp _ => poly ()
@@ -202,7 +202,7 @@ fun fooifyExp fk env =
L'.TFfi (m, x) => ((L'.EFfiApp (m, fk2s fk ^ "ify" ^ capitalize x, [e]), loc), fm)
| L'.TRecord [] => ((L'.EPrim (Prim.String ""), loc), fm)
- | L'.TDatatype (i, _) =>
+ | L'.TDatatype (dk, i, _) =>
let
fun makeDecl n fm =
let
@@ -213,7 +213,7 @@ fun fooifyExp fk env =
(fn ((x, n, to), fm) =>
case to of
NONE =>
- (((L'.PCon (L'.PConVar n, NONE), loc),
+ (((L'.PCon (dk, L'.PConVar n, NONE), loc),
(L'.EPrim (Prim.String x), loc)),
fm)
| SOME t =>
@@ -221,7 +221,7 @@ fun fooifyExp fk env =
val t = monoType env t
val (arg, fm) = fooify fm ((L'.ERel 0, loc), t)
in
- (((L'.PCon (L'.PConVar n, SOME (L'.PVar ("a", t), loc)), loc),
+ (((L'.PCon (dk, L'.PConVar n, SOME (L'.PVar ("a", t), loc)), loc),
(L'.EStrcat ((L'.EPrim (Prim.String (x ^ "/")), loc),
arg), loc)),
fm)
@@ -289,15 +289,15 @@ end
fun monoPatCon env pc =
case pc of
L.PConVar n => L'.PConVar n
- | L.PConFfi {mod = m, datatyp, con, arg} => L'.PConFfi {mod = m, datatyp = datatyp, con = con,
- arg = Option.map (monoType env) arg}
+ | L.PConFfi {mod = m, datatyp, con, arg, ...} => L'.PConFfi {mod = m, datatyp = datatyp, con = con,
+ arg = Option.map (monoType env) arg}
fun monoPat env (p, loc) =
case p of
L.PWild => (L'.PWild, loc)
| L.PVar (x, t) => (L'.PVar (x, monoType env t), loc)
| L.PPrim p => (L'.PPrim p, loc)
- | L.PCon (pc, po) => (L'.PCon (monoPatCon env pc, Option.map (monoPat env) po), loc)
+ | L.PCon (dk, pc, po) => (L'.PCon (dk, monoPatCon env pc, Option.map (monoPat env) po), loc)
| L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, monoPat env p, monoType env t)) xps), loc)
fun monoExp (env, st, fm) (all as (e, loc)) =
@@ -311,7 +311,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
L.EPrim p => ((L'.EPrim p, loc), fm)
| L.ERel n => ((L'.ERel n, loc), fm)
| L.ENamed n => ((L'.ENamed n, loc), fm)
- | L.ECon (pc, eo) =>
+ | L.ECon (dk, pc, eo) =>
let
val (eo, fm) =
case eo of
@@ -323,7 +323,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
(SOME e, fm)
end
in
- ((L'.ECon (monoPatCon env pc, eo), loc), fm)
+ ((L'.ECon (dk, monoPatCon env pc, eo), loc), fm)
end
| L.EFfi mx => ((L'.EFfi mx, loc), fm)
| L.EFfiApp (m, x, es) =>