diff options
| -rw-r--r-- | src/cjr.sml | 10 | ||||
| -rw-r--r-- | src/cjr_env.sig | 2 | ||||
| -rw-r--r-- | src/cjr_env.sml | 13 | ||||
| -rw-r--r-- | src/cjr_print.sml | 72 | ||||
| -rw-r--r-- | src/cjrize.sml | 19 | ||||
| -rw-r--r-- | src/core.sml | 8 | ||||
| -rw-r--r-- | src/core_print.sml | 16 | ||||
| -rw-r--r-- | src/core_util.sig | 2 | ||||
| -rw-r--r-- | src/core_util.sml | 12 | ||||
| -rw-r--r-- | src/corify.sml | 1184 | ||||
| -rw-r--r-- | src/elab.sml | 6 | ||||
| -rw-r--r-- | src/elab_env.sig | 4 | ||||
| -rw-r--r-- | src/elab_env.sml | 43 | ||||
| -rw-r--r-- | src/elab_print.sml | 8 | ||||
| -rw-r--r-- | src/elab_util.sig | 2 | ||||
| -rw-r--r-- | src/elab_util.sml | 6 | ||||
| -rw-r--r-- | src/elaborate.sml | 41 | ||||
| -rw-r--r-- | src/expl.sml | 4 | ||||
| -rw-r--r-- | src/expl_print.sml | 8 | ||||
| -rw-r--r-- | src/expl_util.sig | 2 | ||||
| -rw-r--r-- | src/expl_util.sml | 6 | ||||
| -rw-r--r-- | src/explify.sml | 2 | ||||
| -rw-r--r-- | src/mono.sml | 8 | ||||
| -rw-r--r-- | src/mono_env.sml | 9 | ||||
| -rw-r--r-- | src/mono_opt.sml | 8 | ||||
| -rw-r--r-- | src/mono_print.sml | 14 | ||||
| -rw-r--r-- | src/mono_reduce.sml | 8 | ||||
| -rw-r--r-- | src/mono_shake.sml | 2 | ||||
| -rw-r--r-- | src/mono_util.sig | 2 | ||||
| -rw-r--r-- | src/mono_util.sml | 20 | ||||
| -rw-r--r-- | src/monoize.sml | 20 |
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) => |