Elaborating 'let'

6 files changed, 189 insertions, 18 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))*)