diff options
| -rw-r--r-- | src/cjr.sml | 6 | ||||
| -rw-r--r-- | src/cjr_env.sml | 4 | ||||
| -rw-r--r-- | src/cjr_print.sml | 261 | ||||
| -rw-r--r-- | src/cjrize.sml | 44 | ||||
| -rw-r--r-- | src/core.sml | 6 | ||||
| -rw-r--r-- | src/core_env.sml | 4 | ||||
| -rw-r--r-- | src/core_print.sml | 4 | ||||
| -rw-r--r-- | src/core_util.sml | 10 | ||||
| -rw-r--r-- | src/corify.sml | 13 | ||||
| -rw-r--r-- | src/elab.sml | 6 | ||||
| -rw-r--r-- | src/elab_print.sml | 4 | ||||
| -rw-r--r-- | src/elab_util.sml | 10 | ||||
| -rw-r--r-- | src/elaborate.sml | 51 | ||||
| -rw-r--r-- | src/expl.sml | 6 | ||||
| -rw-r--r-- | src/expl_print.sml | 4 | ||||
| -rw-r--r-- | src/expl_util.sml | 10 | ||||
| -rw-r--r-- | src/explify.sml | 11 | ||||
| -rw-r--r-- | src/mono.sml | 6 | ||||
| -rw-r--r-- | src/mono_env.sml | 10 | ||||
| -rw-r--r-- | src/mono_print.sml | 4 | ||||
| -rw-r--r-- | src/mono_util.sml | 16 | ||||
| -rw-r--r-- | src/monoize.sml | 23 |
22 files changed, 377 insertions, 136 deletions
diff --git a/src/cjr.sml b/src/cjr.sml index eb035e40..4c9cf4c3 100644 --- a/src/cjr.sml +++ b/src/cjr.sml @@ -44,10 +44,10 @@ datatype patCon = datatype pat' = PWild - | PVar of string + | PVar of string * typ | PPrim of Prim.t | PCon of patCon * pat option - | PRecord of (string * pat) list + | PRecord of (string * pat * typ) list withtype pat = pat' located @@ -63,7 +63,7 @@ datatype exp' = | ERecord of int * (string * exp) list | EField of exp * string - | ECase of exp * (pat * exp) list * typ + | ECase of exp * (pat * exp) list * { disc : typ, result : typ } | EWrite of exp | ESeq of exp * exp diff --git a/src/cjr_env.sml b/src/cjr_env.sml index f972a80e..6a3c41bc 100644 --- a/src/cjr_env.sml +++ b/src/cjr_env.sml @@ -61,8 +61,8 @@ val empty = { fun pushDatatype (env : env) x n xncs = {datatypes = IM.insert (#datatypes env, n, (x, xncs)), - constructors = foldl (fn ((x, n, to), constructors) => - IM.insert (constructors, n, (x, to, n))) + constructors = foldl (fn ((x, n', to), constructors) => + IM.insert (constructors, n', (x, to, n))) (#constructors env) xncs, numRelE = #numRelE env, diff --git a/src/cjr_print.sml b/src/cjr_print.sml index 61b2d6ce..4a6971b0 100644 --- a/src/cjr_print.sml +++ b/src/cjr_print.sml @@ -85,7 +85,188 @@ fun p_enamed env n = string ("__lwn_" ^ #1 (E.lookupENamed env n) ^ "_" ^ Int.toString n) handle CjrEnv.UnboundNamed _ => string ("__lwn_UNBOUND_" ^ Int.toString n) -fun p_exp' par env (e, _) = +fun p_con_named env n = + string ("__lwc_" ^ #1 (E.lookupConstructor env n) ^ "_" ^ Int.toString n) + handle CjrEnv.UnboundNamed _ => string ("__lwc_UNBOUND_" ^ Int.toString n) + +fun p_pat_preamble env (p, _) = + case p of + PWild => (box [], + env) + | PVar (x, t) => (box [p_typ env t, + space, + string "__lwr_", + string x, + string "_", + string (Int.toString (E.countERels env)), + string ";", + newline], + env) + | PPrim _ => (box [], env) + | PCon (_, NONE) => (box [], env) + | PCon (_, SOME p) => p_pat_preamble env p + | PRecord xps => + foldl (fn ((_, p, _), (pp, env)) => + let + val (pp', env) = p_pat_preamble env p + in + (box [pp', pp], env) + end) (box [], env) xps + +fun p_patCon env pc = + case pc of + PConVar n => p_con_named env n + | PConFfi _ => raise Fail "CjrPrint PConFfi" + +fun p_pat (env, exit, depth) (p, _) = + case p of + PWild => + (box [], env) + | PVar (x, t) => + (box [string "__lwr_", + string x, + string "_", + string (Int.toString (E.countERels env)), + space, + string "=", + space, + string "disc", + string (Int.toString depth), + string ";"], + E.pushERel env x t) + | PPrim (Prim.Int n) => + (box [string "if", + space, + string "(disc", + string (Int.toString depth), + space, + string "!=", + space, + Prim.p_t (Prim.Int n), + string ")", + space, + exit], + env) + | PPrim (Prim.String s) => + (box [string "if", + space, + string "(strcmp(disc", + string (Int.toString depth), + string ",", + space, + Prim.p_t (Prim.String s), + string "))", + space, + exit], + env) + | PPrim _ => raise Fail "CjrPrint: Disallowed PPrim primitive" + + | PCon (pc, po) => + let + val (p, env) = + case po of + NONE => (box [], env) + | SOME p => + let + val (p, env) = p_pat (env, exit, depth + 1) p + + val (x, to) = case pc of + PConVar n => + let + val (x, to, _) = E.lookupConstructor env n + in + (x, to) + end + | PConFfi _ => raise Fail "PConFfi" + + val t = case to of + NONE => raise Fail "CjrPrint: Constructor mismatch" + | SOME t => t + in + (box [string "{", + newline, + p_typ env t, + space, + string "disc", + string (Int.toString (depth + 1)), + space, + string "=", + space, + string "disc", + string (Int.toString depth), + string "->data.__lwc_", + string x, + string ";", + newline, + p, + newline, + string "}"], + env) + end + in + (box [string "if", + space, + string "(disc", + string (Int.toString depth), + string "->tag", + space, + string "!=", + space, + p_patCon env pc, + string ")", + space, + exit, + newline, + p], + env) + end + + | PRecord xps => + let + val (xps, env) = + ListUtil.foldlMap (fn ((x, p, t), env) => + let + val (p, env) = p_pat (env, exit, depth + 1) p + + val p = box [string "{", + newline, + p_typ env t, + space, + string "disc", + string (Int.toString (depth + 1)), + space, + string "=", + space, + string "disc", + string (Int.toString depth), + string ".", + string x, + string ";", + newline, + p, + newline, + string "}"] + in + (p, env) + end) env xps + in + (p_list_sep newline (fn x => x) xps, + env) + end + +local + val count = ref 0 +in +fun newGoto () = + let + val r = !count + in + count := r + 1; + string ("L" ^ Int.toString r) + end +end + +fun p_exp' par env (e, loc) = case e of EPrim p => Prim.p_t p | ERel n => p_rel env n @@ -95,7 +276,7 @@ fun p_exp' par env (e, _) = val (x, _, dn) = E.lookupConstructor env n val (dx, _) = E.lookupDatatype env dn in - box [string "{(", + box [string "({", newline, string "struct", space, @@ -123,7 +304,7 @@ fun p_exp' par env (e, _) = newline, case eo of NONE => box [] - | SOME e => box [string "tmp->data.", + | SOME e => box [string "tmp->data.__lwc_", string x, space, string "=", @@ -180,10 +361,77 @@ fun p_exp' par env (e, _) = string "})" ] | EField (e, x) => box [p_exp' true env e, - string ".", + string ".__lwf_", string x] - | ECase _ => raise Fail "CjrPrint ECase" + | ECase (e, pes, {disc, result}) => + let + val final = newGoto () + + val body = foldl (fn ((p, e), body) => + let + val exit = newGoto () + val (pr, _) = p_pat_preamble env p + val (p, env) = p_pat (env, + box [string "goto", + space, + exit, + string ";"], + 0) p + in + box [body, + box [string "{", + newline, + pr, + newline, + p, + newline, + string "result", + space, + string "=", + space, + p_exp env e, + string ";", + newline, + string "goto", + space, + final, + string ";", + newline, + string "}"], + newline, + exit, + string ":", + newline] + end) (box []) pes + in + box [string "({", + newline, + p_typ env disc, + space, + string "disc0", + space, + string "=", + space, + p_exp env e, + string ";", + newline, + p_typ env result, + space, + string "result;", + newline, + body, + string "lw_error(ctx, FATAL, \"", + string (ErrorMsg.spanToString loc), + string ": pattern match failure\");", + newline, + final, + string ":", + space, + string "result;", + newline, + string "})"] + end | EWrite e => box [string "(lw_write(ctx, ", p_exp env e, @@ -236,6 +484,7 @@ fun p_decl env (dAll as (d, _) : decl) = newline, p_list_sep (box []) (fn (x, t) => box [p_typ env t, space, + string "__lwf_", string x, string ";", newline]) xts, @@ -538,7 +787,7 @@ fun p_file env (ds, ps) = newline, case to of NONE => box [] - | SOME t => box [string "tmp->data.", + | SOME t => box [string "tmp->data.__lwc_", string x', space, string "=", diff --git a/src/cjrize.sml b/src/cjrize.sml index 7830e740..8e410f92 100644 --- a/src/cjrize.sml +++ b/src/cjrize.sml @@ -108,13 +108,35 @@ fun cifyPatCon pc = L.PConVar n => L'.PConVar n | L.PConFfi mx => L'.PConFfi mx -fun cifyPat (p, loc) = +fun cifyPat ((p, loc), sm) = case p of - L.PWild => (L'.PWild, loc) - | L.PVar x => (L'.PVar x, loc) - | L.PPrim p => (L'.PPrim p, loc) - | L.PCon (pc, po) => (L'.PCon (cifyPatCon pc, Option.map cifyPat po), loc) - | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, cifyPat p)) xps), loc) + L.PWild => ((L'.PWild, loc), sm) + | L.PVar (x, t) => + let + val (t, sm) = cifyTyp (t, sm) + in + ((L'.PVar (x, t), loc), sm) + end + | L.PPrim p => ((L'.PPrim p, loc), sm) + | L.PCon (pc, NONE) => ((L'.PCon (cifyPatCon pc, NONE), loc), sm) + | L.PCon (pc, SOME p) => + let + val (p, sm) = cifyPat (p, sm) + in + ((L'.PCon (cifyPatCon pc, SOME p), loc), sm) + end + | L.PRecord xps => + let + val (xps, sm) = ListUtil.foldlMap (fn ((x, p, t), sm) => + let + val (p, sm) = cifyPat (p, sm) + val (t, sm) = cifyTyp (t, sm) + in + ((x, p, t), sm) + end) sm xps + in + ((L'.PRecord xps, loc), sm) + end fun cifyExp ((e, loc), sm) = case e of @@ -179,19 +201,21 @@ fun cifyExp ((e, loc), sm) = ((L'.EField (e, x), loc), sm) end - | L.ECase (e, pes, t) => + | L.ECase (e, pes, {disc, result}) => let val (e, sm) = cifyExp (e, sm) val (pes, sm) = ListUtil.foldlMap (fn ((p, e), sm) => let val (e, sm) = cifyExp (e, sm) + val (p, sm) = cifyPat (p, sm) in - ((cifyPat p, e), sm) + ((p, e), sm) end) sm pes - val (t, sm) = cifyTyp (t, sm) + val (disc, sm) = cifyTyp (disc, sm) + val (result, sm) = cifyTyp (result, sm) in - ((L'.ECase (e, pes, t), loc), sm) + ((L'.ECase (e, pes, {disc = disc, result = result}), loc), sm) end | L.EStrcat (e1, e2) => diff --git a/src/core.sml b/src/core.sml index 5baa0351..257f7ed1 100644 --- a/src/core.sml +++ b/src/core.sml @@ -65,10 +65,10 @@ datatype patCon = datatype pat' = PWild - | PVar of string + | PVar of string * con | PPrim of Prim.t | PCon of patCon * pat option - | PRecord of (string * pat) list + | PRecord of (string * pat * con) list withtype pat = pat' located @@ -89,7 +89,7 @@ datatype exp' = | ECut of exp * con * { field : con, rest : con } | EFold of kind - | ECase of exp * (pat * exp) list * con + | ECase of exp * (pat * exp) list * { disc : con, result : con } | EWrite of exp diff --git a/src/core_env.sml b/src/core_env.sml index 4895de9c..1cc10ada 100644 --- a/src/core_env.sml +++ b/src/core_env.sml @@ -113,8 +113,8 @@ fun pushDatatype (env : env) x n xncs = namedC = #namedC env, datatypes = IM.insert (#datatypes env, n, (x, xncs)), - constructors = foldl (fn ((x, n, to), constructors) => - IM.insert (constructors, n, (x, to, n))) + constructors = foldl (fn ((x, n', to), constructors) => + IM.insert (constructors, n', (x, to, n))) (#constructors env) xncs, relE = #relE env, diff --git a/src/core_print.sml b/src/core_print.sml index 7458fef0..520ca903 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -171,7 +171,7 @@ fun p_patCon env pc = fun p_pat' par env (p, _) = case p of PWild => string "_" - | PVar s => string s + | 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, @@ -179,7 +179,7 @@ fun p_pat' par env (p, _) = p_pat' true env p]) | PRecord xps => box [string "{", - p_list_sep (box [string ",", space]) (fn (x, p) => + p_list_sep (box [string ",", space]) (fn (x, p, _) => box [string x, space, string "=", diff --git a/src/core_util.sml b/src/core_util.sml index 7ec4fa6c..1cc25e37 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -302,16 +302,18 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn k' => (EFold k', loc)) - | ECase (e, pes, t) => + | ECase (e, pes, {disc, result}) => S.bind2 (mfe ctx e, fn e' => S.bind2 (ListUtil.mapfold (fn (p, e) => S.map2 (mfe ctx e, fn e' => (p, e'))) pes, fn pes' => - S.map2 (mfc ctx t, - fn t' => - (ECase (e', pes', t'), loc)))) + S.bind2 (mfc ctx disc, + fn disc' => + S.map2 (mfc ctx result, + fn result' => + (ECase (e', pes', {disc = disc', result = result'}), loc))))) | EWrite e => S.map2 (mfe ctx e, diff --git a/src/corify.sml b/src/corify.sml index 44da20da..a3cbb92e 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -411,10 +411,10 @@ fun corifyPatCon st pc = fun corifyPat st (p, loc) = case p of L.PWild => (L'.PWild, loc) - | L.PVar x => (L'.PVar x, 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) => (x, corifyPat st p)) xps), 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 @@ -473,10 +473,11 @@ fun corifyExp st (e, loc) = {field = corifyCon st field, rest = corifyCon st rest}), loc) | L.EFold k => (L'.EFold (corifyKind k), loc) - | L.ECase (e, pes, t) => (L'.ECase (corifyExp st e, - map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes, - corifyCon st t), - 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) diff --git a/src/elab.sml b/src/elab.sml index 58e69629..fb67556b 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -77,10 +77,10 @@ datatype patCon = datatype pat' = PWild - | PVar of string + | PVar of string * con | PPrim of Prim.t | PCon of patCon * pat option - | PRecord of (string * pat) list + | PRecord of (string * pat * con) list withtype pat = pat' located @@ -99,7 +99,7 @@ datatype exp' = | ECut of exp * con * { field : con, rest : con } | EFold of kind - | ECase of exp * (pat * exp) list * con + | ECase of exp * (pat * exp) list * { disc : con, result : con } | EError diff --git a/src/elab_print.sml b/src/elab_print.sml index 591e019b..93d4f7e2 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -214,7 +214,7 @@ fun p_patCon env pc = fun p_pat' par env (p, _) = case p of PWild => string "_" - | PVar s => string s + | 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, @@ -222,7 +222,7 @@ fun p_pat' par env (p, _) = p_pat' true env p]) | PRecord xps => box [string "{", - p_list_sep (box [string ",", space]) (fn (x, p) => + p_list_sep (box [string ",", space]) (fn (x, p, _) => box [string x, space, string "=", diff --git a/src/elab_util.sml b/src/elab_util.sml index ac2e1a99..a3754153 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -308,16 +308,18 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn k' => (EFold k', loc)) - | ECase (e, pes, t) => + | ECase (e, pes, {disc, result}) => S.bind2 (mfe ctx e, fn e' => S.bind2 (ListUtil.mapfold (fn (p, e) => S.map2 (mfe ctx e, fn e' => (p, e'))) pes, fn pes' => - S.map2 (mfc ctx t, - fn t' => - (ECase (e', pes', t'), loc)))) + S.bind2 (mfc ctx disc, + fn disc' => + S.map2 (mfc ctx result, + fn result' => + (ECase (e', pes', {disc = disc', result = result'}), loc))))) | EError => S.return2 eAll in diff --git a/src/elaborate.sml b/src/elaborate.sml index da38cbba..54af8dab 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -904,45 +904,6 @@ fun foldType (dom, loc) = (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)), loc)), loc)), loc) -fun typeof env (e, loc) = - case e of - L'.EPrim p => primType env p - | L'.ERel n => #2 (E.lookupERel env n) - | L'.ENamed n => #2 (E.lookupENamed env n) - | L'.EModProj (n, ms, x) => - let - val (_, sgn) = E.lookupStrNamed env n - val (str, sgn) = foldl (fn (m, (str, sgn)) => - case E.projectStr env {sgn = sgn, str = str, field = m} of - NONE => raise Fail "typeof: Unknown substructure" - | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) - ((L'.StrVar n, loc), sgn) ms - in - case E.projectVal env {sgn = sgn, str = str, field = x} of - NONE => raise Fail "typeof: Unknown val in structure" - | SOME t => t - end - - | L'.EApp (e1, _) => - (case #1 (typeof env e1) of - L'.TFun (_, c) => c - | _ => raise Fail "typeof: Bad EApp") - | L'.EAbs (_, _, ran, _) => ran - | L'.ECApp (e1, c) => - (case #1 (typeof env e1) of - L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1 - | _ => raise Fail "typeof: Bad ECApp") - | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc) - - | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc) - | L'.EField (_, _, {field, ...}) => field - | L'.ECut (_, _, {rest, ...}) => (L'.TRecord rest, loc) - | L'.EFold dom => foldType (dom, loc) - - | L'.ECase (_, _, t) => t - - | L'.EError => cerror - fun elabHead (env, denv) (e as (_, loc)) t = let fun unravel (t, e) = @@ -1000,7 +961,7 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) = else cunif (loc, (L'.KType, loc)) in - (((L'.PVar x, loc), t), + (((L'.PVar (x, t), loc), t), (E.pushERel env x t, SS.add (bound, x))) end | L.PPrim p => (((L'.PPrim p, loc), primType env p), @@ -1018,7 +979,7 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) = let val (str, sgn) = foldl (fn (m, (str, sgn)) => case E.projectStr env {sgn = sgn, str = str, field = m} of - NONE => raise Fail "typeof: Unknown substructure" + NONE => raise Fail "elabPat: Unknown substructure" | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) ((L'.StrVar n, loc), sgn) ms in @@ -1051,7 +1012,7 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) = else c in - (((L'.PRecord (map (fn (x, p', _) => (x, p')) xpts), loc), + (((L'.PRecord xpts, loc), (L'.TRecord c, loc)), (env, bound)) end @@ -1085,8 +1046,8 @@ fun exhaustive (env, denv, t, ps) = | 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'.PRecord xps => Record [foldl (fn ((x, p), fmap) => - SM.insert (fmap, x, coverage p)) SM.empty xps] + | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) => + SM.insert (fmap, x, coverage p)) SM.empty xps] fun merge (c1, c2) = case (c1, c2) of @@ -1458,7 +1419,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) = else expError env (Inexhaustive loc); - ((L'.ECase (e', pes', result), loc), result, gs' @ gs) + ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs' @ gs) end end diff --git a/src/expl.sml b/src/expl.sml index 52dbee63..c561ff29 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -65,10 +65,10 @@ datatype patCon = datatype pat' = PWild - | PVar of string + | PVar of string * con | PPrim of Prim.t | PCon of patCon * pat option - | PRecord of (string * pat) list + | PRecord of (string * pat * con) list withtype pat = pat' located @@ -87,7 +87,7 @@ datatype exp' = | ECut of exp * con * { field : con, rest : con } | EFold of kind - | ECase of exp * (pat * exp) list * con + | ECase of exp * (pat * exp) list * { disc : con, result : con } | EWrite of exp diff --git a/src/expl_print.sml b/src/expl_print.sml index 3595f65a..24bbd6c0 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -179,7 +179,7 @@ fun p_patCon env pc = fun p_pat' par env (p, _) = case p of PWild => string "_" - | PVar s => string s + | 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, @@ -187,7 +187,7 @@ fun p_pat' par env (p, _) = p_pat' true env p]) | PRecord xps => box [string "{", - p_list_sep (box [string ",", space]) (fn (x, p) => + p_list_sep (box [string ",", space]) (fn (x, p, _) => box [string x, space, string "=", diff --git a/src/expl_util.sml b/src/expl_util.sml index 685605c3..290c64f5 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -287,16 +287,18 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn e' => (EWrite e', loc)) - | ECase (e, pes, t) => + | ECase (e, pes, {disc, result}) => S.bind2 (mfe ctx e, fn e' => S.bind2 (ListUtil.mapfold (fn (p, e) => S.map2 (mfe ctx e, fn e' => (p, e'))) pes, fn pes' => - S.map2 (mfc ctx t, - fn t' => - (ECase (e', pes', t'), loc)))) + S.bind2 (mfc ctx disc, + fn disc' => + S.map2 (mfc ctx result, + fn result' => + (ECase (e', pes', {disc = disc', result = result'}), loc))))) in mfe end diff --git a/src/explify.sml b/src/explify.sml index 7c23c2f5..90737f07 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -79,10 +79,10 @@ fun explifyPatCon pc = fun explifyPat (p, loc) = case p of L.PWild => (L'.PWild, loc) - | L.PVar x => (L'.PVar x, 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.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, explifyPat p)) xps), loc) + | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, explifyPat p, explifyCon t)) xps), loc) fun explifyExp (e, loc) = case e of @@ -102,9 +102,10 @@ fun explifyExp (e, loc) = {field = explifyCon field, rest = explifyCon rest}), loc) | L.EFold k => (L'.EFold (explifyKind k), loc) - | L.ECase (e, pes, t) => (L'.ECase (explifyExp e, - map (fn (p, e) => (explifyPat p, explifyExp e)) pes, - explifyCon t), loc) + | L.ECase (e, pes, {disc, result}) => + (L'.ECase (explifyExp e, + map (fn (p, e) => (explifyPat p, explifyExp e)) pes, + {disc = explifyCon disc, result = explifyCon result}), loc) | L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc) diff --git a/src/mono.sml b/src/mono.sml index 7ed1aca1..f8c7dbfe 100644 --- a/src/mono.sml +++ b/src/mono.sml @@ -43,10 +43,10 @@ datatype patCon = datatype pat' = PWild - | PVar of string + | PVar of string * typ | PPrim of Prim.t | PCon of patCon * pat option - | PRecord of (string * pat) list + | PRecord of (string * pat * typ) list withtype pat = pat' located @@ -63,7 +63,7 @@ datatype exp' = | ERecord of (string * exp * typ) list | EField of exp * string - | ECase of exp * (pat * exp) list * typ + | ECase of exp * (pat * exp) list * { disc : typ, result : typ } | EStrcat of exp * exp diff --git a/src/mono_env.sml b/src/mono_env.sml index c28942a1..f2be9b4b 100644 --- a/src/mono_env.sml +++ b/src/mono_env.sml @@ -53,8 +53,8 @@ val empty = { fun pushDatatype (env : env) x n xncs = {datatypes = IM.insert (#datatypes env, n, (x, xncs)), - constructors = foldl (fn ((x, n, to), constructors) => - IM.insert (constructors, n, (x, to, n))) + constructors = foldl (fn ((x, n', to), constructors) => + IM.insert (constructors, n', (x, to, n))) (#constructors env) xncs, relE = #relE env, @@ -107,15 +107,13 @@ fun declBinds env (d, loc) = | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis | DExport _ => env -val dummyt = (TFfi ("", ""), ErrorMsg.dummySpan) - fun patBinds env (p, loc) = case p of PWild => env - | PVar x => pushERel env x dummyt + | PVar (x, t) => pushERel env x t | PPrim _ => env | PCon (_, NONE) => env | PCon (_, SOME p) => patBinds env p - | PRecord xps => foldl (fn ((_, p), env) => patBinds env p) env xps + | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps end diff --git a/src/mono_print.sml b/src/mono_print.sml index 161cbe9f..dcd4eb84 100644 --- a/src/mono_print.sml +++ b/src/mono_print.sml @@ -89,7 +89,7 @@ fun p_patCon env pc = fun p_pat' par env (p, _) = case p of PWild => string "_" - | PVar s => string s + | 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, @@ -97,7 +97,7 @@ fun p_pat' par env (p, _) = p_pat' true env p]) | PRecord xps => box [string "{", - p_list_sep (box [string ",", space]) (fn (x, p) => + p_list_sep (box [string ",", space]) (fn (x, p, _) => box [string x, space, string "=", diff --git a/src/mono_util.sml b/src/mono_util.sml index 4414385d..805a1c88 100644 --- a/src/mono_util.sml +++ b/src/mono_util.sml @@ -181,30 +181,30 @@ fun mapfoldB {typ = fc, exp = fe, bind} = fn e' => (EField (e', x), loc)) - | ECase (e, pes, t) => + | ECase (e, pes, {disc, result}) => S.bind2 (mfe ctx e, fn e' => S.bind2 (ListUtil.mapfold (fn (p, e) => let - val dummyt = (TFfi ("", ""), ErrorMsg.dummySpan) - fun pb ((p, _), ctx) = case p of PWild => ctx - | PVar x => bind (ctx, RelE (x, dummyt)) + | PVar (x, t) => bind (ctx, RelE (x, t)) | PPrim _ => ctx | PCon (_, NONE) => ctx | PCon (_, SOME p) => pb (p, ctx) - | PRecord xps => foldl (fn ((_, p), ctx) => + | PRecord xps => foldl (fn ((_, p, _), ctx) => pb (p, ctx)) ctx xps in S.map2 (mfe (pb (p, ctx)) e, fn e' => (p, e')) end) pes, fn pes' => - S.map2 (mft t, - fn t' => - (ECase (e', pes', t'), loc)))) + S.bind2 (mft disc, + fn disc' => + S.map2 (mft result, + fn result' => + (ECase (e', pes', {disc = disc', result = result'}), loc))))) | EStrcat (e1, e2) => S.bind2 (mfe ctx e1, diff --git a/src/monoize.sml b/src/monoize.sml index 995c2a7c..dfd727f7 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -212,10 +212,10 @@ fun fooifyExp fk env = fm) | SOME t => let - val (arg, fm) = fooify fm ((L'.ERel 0, loc), - monoType env t) + 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", loc)), loc), + (((L'.PCon (L'.PConVar n, SOME (L'.PVar ("a", t), loc)), loc), (L'.EStrcat ((L'.EPrim (Prim.String (x ^ "/")), loc), arg), loc)), fm) @@ -233,7 +233,8 @@ fun fooifyExp fk env = ran, (L'.ECase ((L'.ERel 0, loc), branches, - ran), loc)), loc), + {disc = dom, + result = ran}), loc)), loc), "")], loc), fm) end @@ -284,13 +285,13 @@ fun monoPatCon pc = L.PConVar n => L'.PConVar n | L.PConFfi mx => L'.PConFfi mx -fun monoPat (p, loc) = +fun monoPat env (p, loc) = case p of L.PWild => (L'.PWild, loc) - | L.PVar x => (L'.PVar x, 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 pc, Option.map monoPat po), loc) - | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, monoPat p)) xps), loc) + | L.PCon (pc, po) => (L'.PCon (monoPatCon 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)) = let @@ -667,7 +668,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = | L.ECut _ => poly () | L.EFold _ => poly () - | L.ECase (e, pes, t) => + | L.ECase (e, pes, {disc, result}) => let val (e, fm) = monoExp (env, st, fm) e val (pes, fm) = ListUtil.foldlMap @@ -675,10 +676,10 @@ fun monoExp (env, st, fm) (all as (e, loc)) = let val (e, fm) = monoExp (env, st, fm) e in - ((monoPat p, e), fm) + ((monoPat env p, e), fm) end) fm pes in - ((L'.ECase (e, pes, monoType env t), loc), fm) + ((L'.ECase (e, pes, {disc = monoType env disc, result = monoType env result}), loc), fm) end | L.EWrite e => |