summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab.sml4
-rw-r--r--src/elab_env.sml20
-rw-r--r--src/elab_print.sml16
-rw-r--r--src/elab_util.sml31
-rw-r--r--src/elaborate.sml18
-rw-r--r--src/explify.sml7
-rw-r--r--src/source.sml2
-rw-r--r--src/source_print.sml10
-rw-r--r--src/termination.sml2
-rw-r--r--src/unnest.sml21
-rw-r--r--src/urweb.grm2
11 files changed, 85 insertions, 48 deletions
diff --git a/src/elab.sml b/src/elab.sml
index de2db500..76ea6725 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -120,10 +120,10 @@ datatype exp' =
| EError
| EUnif of exp option ref
- | ELet of edecl list * exp
+ | ELet of edecl list * exp * con
and edecl' =
- EDVal of string * con * exp
+ EDVal of pat * con * exp
| EDValRec of (string * con * exp) list
withtype exp = exp' located
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 88b2554b..2296d819 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1454,9 +1454,18 @@ fun projectConstraints env {sgn, str} =
| SgnError => SOME []
| _ => NONE
+fun patBinds env (p, loc) =
+ case p of
+ PWild => env
+ | 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
+
fun edeclBinds env (d, loc) =
case d of
- EDVal (x, t, _) => pushERel env x t
+ EDVal (p, _, _) => patBinds env p
| EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis
fun declBinds env (d, loc) =
@@ -1565,13 +1574,4 @@ fun declBinds env (d, loc) =
pushENamedAs env x n t
end
-fun patBinds env (p, loc) =
- case p of
- PWild => env
- | 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
-
end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index ab38c2e1..3e4ea659 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -423,7 +423,7 @@ fun p_exp' par env (e, _) =
| EUnif (ref (SOME e)) => p_exp env e
| EUnif _ => string "_"
- | ELet (ds, e) =>
+ | ELet (ds, e, _) =>
let
val (dsp, env) = ListUtil.foldlMap
(fn (d, env) =>
@@ -456,9 +456,17 @@ and p_exp env = p_exp' false env
and p_edecl env (dAll as (d, _)) =
case d of
- EDVal vi => box [string "val",
- space,
- p_evali env vi]
+ EDVal (p, t, e) => box [string "val",
+ space,
+ p_pat env p,
+ space,
+ string ":",
+ space,
+ p_con env t,
+ space,
+ string "=",
+ space,
+ p_exp env e]
| EDValRec vis =>
let
val env = E.edeclBinds env dAll
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 036aa867..c2101ae3 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -306,6 +306,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
end
val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
+ fun doVars ((p, _), ctx) =
+ case p of
+ PWild => ctx
+ | PVar xt => bind (ctx, RelE xt)
+ | PPrim _ => ctx
+ | PCon (_, _, _, NONE) => ctx
+ | PCon (_, _, _, SOME p) => doVars (p, ctx)
+ | PRecord xpcs =>
+ foldl (fn ((_, p, _), ctx) => doVars (p, ctx))
+ ctx xpcs
+
fun mfe ctx e acc =
S.bindP (mfe' ctx e acc, fe ctx)
@@ -425,13 +436,13 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
| EUnif (ref (SOME e)) => mfe ctx e
| EUnif _ => S.return2 eAll
- | ELet (des, e) =>
+ | ELet (des, e, t) =>
let
val (des, ctx) = foldl (fn (ed, (des, ctx)) =>
let
val ctx' =
case #1 ed of
- EDVal (x, t, _) => bind (ctx, RelE (x, t))
+ EDVal (p, _, _) => doVars (p, ctx)
| EDValRec vis =>
foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
in
@@ -445,9 +456,11 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
in
S.bind2 (des,
fn des' =>
- S.map2 (mfe ctx e,
+ S.bind2 (mfe ctx e,
fn e' =>
- (ELet (des', e'), loc)))
+ S.map2 (mfc ctx t,
+ fn t' =>
+ (ELet (des', e', t'), loc))))
end
| EKAbs (x, e) =>
@@ -463,10 +476,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
and mfed ctx (dAll as (d, loc)) =
case d of
- EDVal vi =>
- S.map2 (mfvi ctx vi,
- fn vi' =>
- (EDVal vi', loc))
+ EDVal (p, t, e) =>
+ S.bind2 (mfc ctx t,
+ fn t' =>
+ S.map2 (mfe (doVars (p, ctx)) e,
+ fn e' =>
+ (EDVal (p, t', e'), loc)))
| EDValRec vis =>
let
val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 6f8575db..b4ce1861 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2093,7 +2093,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val (eds, (env, gs1)) = ListUtil.foldlMap (elabEdecl denv) (env, []) eds
val (e, t, gs2) = elabExp (env, denv) e
in
- ((L'.ELet (eds, e), loc), t, gs1 @ gs2)
+ ((L'.ELet (eds, e, t), loc), t, gs1 @ gs2)
end
in
(*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*)
@@ -2104,20 +2104,16 @@ and elabEdecl denv (dAll as (d, loc), (env, gs)) =
let
val r =
case d of
- L.EDVal (x, co, e) =>
+ L.EDVal (p, e) =>
let
- val (c', _, gs1) = case co of
- NONE => (cunif (loc, ktype), ktype, [])
- | SOME c => elabCon (env, denv) c
+ val ((p', pt), (env', _)) = elabPat (p, (env, SS.empty))
+ val (e', et, gs1) = elabExp (env, denv) e
- val (e', et, gs2) = elabExp (env, denv) e
+ val () = checkCon env e' et pt
- val () = checkCon env e' et c'
-
- val c' = normClassConstraint env c'
- val env' = E.pushERel env x c'
+ val pt = normClassConstraint env pt
in
- ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ gs))
+ ((L'.EDVal (p', pt, e'), loc), (env', gs1 @ gs))
end
| L.EDValRec vis =>
let
diff --git a/src/explify.sml b/src/explify.sml
index d8bd6bff..3ec588fa 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -123,11 +123,14 @@ fun explifyExp (e, loc) =
| L.EUnif (ref (SOME e)) => explifyExp e
| L.EUnif _ => raise Fail ("explifyExp: Undetermined EUnif at " ^ EM.spanToString loc)
- | L.ELet (des, e) =>
+ | L.ELet (des, e, t) =>
foldr (fn ((de, loc), e) =>
case de of
L.EDValRec _ => raise Fail "explifyExp: Local 'val rec' remains"
- | L.EDVal (x, t, e') => (L'.ELet (x, explifyCon t, explifyExp e', e), loc))
+ | L.EDVal ((L.PVar (x, _), _), t', e') => (L'.ELet (x, explifyCon t', explifyExp e', e), loc)
+ | L.EDVal (p, t', e') => (L'.ECase (explifyExp e',
+ [(explifyPat p, e)],
+ {disc = explifyCon t', result = explifyCon t}), loc))
(explifyExp e) des
| L.EKAbs (x, e) => (L'.EKAbs (x, explifyExp e), loc)
diff --git a/src/source.sml b/src/source.sml
index bfa270d8..c5950b36 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -138,7 +138,7 @@ and exp' =
| ELet of edecl list * exp
and edecl' =
- EDVal of string * con option * exp
+ EDVal of pat * exp
| EDValRec of (string * con option * exp) list
withtype sgn_item = sgn_item' located
diff --git a/src/source_print.sml b/src/source_print.sml
index a16b5bb1..7ec584d7 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -338,9 +338,13 @@ and p_exp e = p_exp' false e
and p_edecl (d, _) =
case d of
- EDVal vi => box [string "val",
- space,
- p_vali vi]
+ EDVal (p, e) => box [string "val",
+ space,
+ p_pat p,
+ space,
+ string "=",
+ space,
+ p_exp e]
| EDValRec vis => box [string "val",
space,
string "rec",
diff --git a/src/termination.sml b/src/termination.sml
index 5dd95f46..f0b21d99 100644
--- a/src/termination.sml
+++ b/src/termination.sml
@@ -306,7 +306,7 @@ fun declOk' env (d, loc) =
| EUnif (ref (SOME e)) => exp parent (penv, calls) e
| EUnif (ref NONE) => (Rabble, calls)
- | ELet (eds, e) =>
+ | ELet (eds, e, _) =>
let
fun extPenv ((ed, _), penv) =
case ed of
diff --git a/src/unnest.sml b/src/unnest.sml
index 51b66aa4..3dfa741d 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -173,7 +173,7 @@ fun kind (_, k, st) = (k, st)
fun exp ((ks, ts), e as old, st : state) =
case e of
- ELet (eds, e) =>
+ ELet (eds, e, t) =>
let
(*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
@@ -190,12 +190,23 @@ fun exp ((ks, ts), e as old, st : state) =
ListUtil.foldlMapConcat
(fn (ed, (ts, maxName, ds, subs, by)) =>
case #1 ed of
- EDVal (x, t, e) =>
+ EDVal (p, t, e) =>
let
val e = doSubst (e, subs, by)
+
+ fun doVars ((p, _), ts) =
+ case p of
+ PWild => ts
+ | PVar xt => xt :: ts
+ | PPrim _ => ts
+ | PCon (_, _, _, NONE) => ts
+ | PCon (_, _, _, SOME p) => doVars (p, ts)
+ | PRecord xpcs =>
+ foldl (fn ((_, p, _), ts) => doVars (p, ts))
+ ts xpcs
in
- ([(EDVal (x, t, e), #2 ed)],
- ((x, t) :: ts,
+ ([(EDVal (p, t, e), #2 ed)],
+ (doVars (p, ts),
maxName, ds,
((0, (ERel 0, #2 ed))
:: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs),
@@ -341,7 +352,7 @@ fun exp ((ks, ts), e as old, st : state) =
(*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e),
("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))),
("e'", ElabPrint.p_exp ElabEnv.empty e')];*)
- (ELet (eds, e'),
+ (ELet (eds, e', t),
{maxName = maxName,
decls = ds})
(*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*)
diff --git a/src/urweb.grm b/src/urweb.grm
index 0d2c1d47..8cdf8063 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -1167,7 +1167,7 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
edecls : ([])
| edecl edecls (edecl :: edecls)
-edecl : VAL vali ((EDVal vali, s (VALleft, valiright)))
+edecl : VAL pat EQ eexp ((EDVal (pat, eexp), s (VALleft, eexpright)))
| VAL REC valis ((EDValRec valis, s (VALleft, valisright)))
| FUN valis ((EDValRec valis, s (FUNleft, valisright)))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 01:20:15 +0000