summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-01 11:17:29 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-01 11:17:29 -0400
commit3f497272d327fea2638006c751d812dbbc449c78 (patch)
tree60d3ec0e0ab4ba36e8ad9396aad35e05d4725153
parent89f97891a33b5c0a8971d3508059a139a8815091 (diff)
Elaborating 'let'
-rw-r--r--src/elab.sml7
-rw-r--r--src/elab_env.sig1
-rw-r--r--src/elab_env.sml5
-rw-r--r--src/elab_print.sml61
-rw-r--r--src/elab_util.sml42
-rw-r--r--src/elaborate.sml91
-rw-r--r--tests/let.ur4
7 files changed, 192 insertions, 19 deletions
diff --git a/src/elab.sml b/src/elab.sml
index 4202d367..b5350c2a 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -117,7 +117,14 @@ datatype exp' =
| EError
| EUnif of exp option ref
+ | ELet of edecl list * exp
+
+and edecl' =
+ EDVal of string * con * exp
+ | EDValRec of (string * con * exp) list
+
withtype exp = exp' located
+ and edecl = edecl' located
datatype sgn_item' =
SgiConAbs of string * int * kind
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 363cbe26..727ee259 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -85,6 +85,7 @@ signature ELAB_ENV = sig
val lookupStr : env -> string -> (int * Elab.sgn) option
+ val edeclBinds : env -> Elab.edecl -> env
val declBinds : env -> Elab.decl -> env
val sgiBinds : env -> Elab.sgn_item -> env
diff --git a/src/elab_env.sml b/src/elab_env.sml
index edda9f38..f4f5d2cb 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1075,6 +1075,11 @@ fun projectConstraints env {sgn, str} =
| SgnError => SOME []
| _ => NONE
+fun edeclBinds env (d, loc) =
+ case d of
+ EDVal (x, t, _) => pushERel env x t
+ | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis
+
fun declBinds env (d, loc) =
case d of
DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 8c0b41f7..3d7ce625 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -378,15 +378,52 @@ fun p_exp' par env (e, _) =
| EUnif (ref (SOME e)) => p_exp env e
| EUnif _ => string "_"
+ | ELet (ds, e) =>
+ let
+ val (dsp, env) = ListUtil.foldlMap
+ (fn (d, env) =>
+ (p_edecl env d,
+ E.edeclBinds env d))
+ env ds
+ in
+ box [string "let",
+ newline,
+ box [p_list_sep newline (fn x => x) dsp],
+ newline,
+ string "in",
+ newline,
+ box [p_exp env e],
+ newline,
+ string "end"]
+ end
+
and p_exp env = p_exp' false env
-fun p_named x n =
- if !debug then
- box [string x,
- string "__",
- string (Int.toString n)]
- else
- string x
+and p_edecl env (dAll as (d, _)) =
+ case d of
+ EDVal vi => box [string "val",
+ space,
+ p_evali env vi]
+ | EDValRec vis =>
+ let
+ val env = E.edeclBinds env dAll
+ in
+ box [string "val",
+ space,
+ string "rec",
+ space,
+ p_list_sep (box [newline, string "and", space]) (p_evali env) vis]
+ end
+
+and p_evali env (x, t, e) = box [string x,
+ space,
+ string ":",
+ space,
+ p_con env t,
+ space,
+ string "=",
+ space,
+ p_exp env e]
fun p_datatype env (x, n, xs, cons) =
let
@@ -407,6 +444,14 @@ fun p_datatype env (x, n, xs, cons) =
cons]
end
+fun p_named x n =
+ if !debug then
+ box [string x,
+ string "__",
+ string (Int.toString n)]
+ else
+ string x
+
fun p_sgn_item env (sgi, _) =
case sgi of
SgiConAbs (x, n, k) => box [string "con",
@@ -556,6 +601,8 @@ fun p_vali env (x, n, t, e) = box [p_named x n,
space,
p_exp env e]
+
+
fun p_decl env (dAll as (d, _) : decl) =
case d of
DCon (x, n, k, c) => box [string "con",
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 247e2b3a..28fe8f22 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -352,6 +352,48 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
| EError => S.return2 eAll
| EUnif (ref (SOME e)) => mfe ctx e
| EUnif _ => S.return2 eAll
+
+ | ELet (des, e) =>
+ let
+ val (des, ctx) = foldl (fn (ed, (des, ctx)) =>
+ (S.bind2 (des,
+ fn des' =>
+ S.map2 (mfed ctx ed,
+ fn ed' => des' @ [ed'])),
+ case #1 ed of
+ EDVal (x, t, _) => bind (ctx, RelE (x, t))
+ | EDValRec vis =>
+ foldl (fn ((x, t, _), env) => bind (ctx, RelE (x, t))) ctx vis))
+ (S.return2 [], ctx) des
+ in
+ S.bind2 (des,
+ fn des' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (ELet (des', e'), loc)))
+ end
+
+ and mfed ctx (dAll as (d, loc)) =
+ case d of
+ EDVal vi =>
+ S.map2 (mfvi ctx vi,
+ fn vi' =>
+ (EDVal vi', loc))
+ | EDValRec vis =>
+ let
+ val ctx = foldl (fn ((x, t, _), env) => bind (ctx, RelE (x, t))) ctx vis
+ in
+ S.map2 (ListUtil.mapfold (mfvi ctx) vis,
+ fn vis' =>
+ (EDValRec vis', loc))
+ end
+
+ and mfvi ctx (x, c, e) =
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (x, c', e')))
in
mfe
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 4927e37d..38c03f6e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1400,6 +1400,18 @@ fun normClassConstraint envs (c, loc) =
end
| _ => ((c, loc), [])
+
+val makeInstantiable =
+ let
+ fun kind k = k
+ fun con c =
+ case c of
+ L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c)
+ | _ => c
+ in
+ U.Con.map {kind = kind, con = con}
+ end
+
fun elabExp (env, denv) (eAll as (e, loc)) =
let
(*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
@@ -1670,11 +1682,79 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs)
end
+
+ | L.ELet (eds, e) =>
+ let
+ 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)
+ end
in
(*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*)
r
end
+and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) =
+ let
+ val r =
+ case d of
+ L.EDVal (x, co, e) =>
+ let
+ val (c', _, gs1) = case co of
+ NONE => (cunif (loc, ktype), ktype, [])
+ | SOME c => elabCon (env, denv) c
+
+ val (e', et, gs2) = elabExp (env, denv) e
+ val gs3 = checkCon (env, denv) e' et c'
+ val (c', gs4) = normClassConstraint (env, denv) c'
+ val env' = E.pushERel env x c'
+ val c' = makeInstantiable c'
+ in
+ ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
+ end
+ | L.EDValRec vis =>
+ let
+ fun allowable (e, _) =
+ case e of
+ L.EAbs _ => true
+ | L.ECAbs (_, _, _, e) => allowable e
+ | L.EDisjoint (_, _, e) => allowable e
+ | _ => false
+
+ val (vis, gs) = ListUtil.foldlMap
+ (fn ((x, co, e), gs) =>
+ let
+ val (c', _, gs1) = case co of
+ NONE => (cunif (loc, ktype), ktype, [])
+ | SOME c => elabCon (env, denv) c
+ in
+ ((x, c', e), enD gs1 @ gs)
+ end) gs vis
+
+ val env = foldl (fn ((x, c', _), env) => E.pushERel env x c') env vis
+
+ val (vis, gs) = ListUtil.foldlMap (fn ((x, c', e), gs) =>
+ let
+ val (e', et, gs1) = elabExp (env, denv) e
+
+ val gs2 = checkCon (env, denv) e' et c'
+
+ val c' = makeInstantiable c'
+ in
+ if allowable e then
+ ()
+ else
+ expError env (IllegalRec (x, e'));
+ ((x, c', e'), gs1 @ enD gs2 @ gs)
+ end) gs vis
+ in
+ ((L'.EDValRec vis, loc), (env, gs))
+ end
+ in
+ r
+ end
+
val hnormSgn = E.hnormSgn
fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
@@ -2742,17 +2822,6 @@ fun wildifyStr env (str, sgn) =
| _ => str)
| _ => str
-val makeInstantiable =
- let
- fun kind k = k
- fun con c =
- case c of
- L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c)
- | _ => c
- in
- U.Con.map {kind = kind, con = con}
- end
-
fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
let
(*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
diff --git a/tests/let.ur b/tests/let.ur
index 45d52ded..14dc936c 100644
--- a/tests/let.ur
+++ b/tests/let.ur
@@ -1,6 +1,8 @@
fun main () : transaction page =
let
val x = 1
+ val y = "Hello"
+ val z = 3.45
in
- return <xml>{[x]}</xml>
+ return <xml>{[x]}, {[y]}, {[z]}</xml>
end