Fix EDLet elab_util bug

4 files changed, 59 insertions, 56 deletions

diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 90729f5c..8493f2f5 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -1,38 +1,38 @@
 datatype t = datatype Basis.list
 
-val show (a ::: Type) (_ : show a) =
-    let
-        fun show' (ls : list a) =
-            case ls of
-                [] => "[]"
-              | x :: ls => show x ^ " :: " ^ show' ls
-    in
-        mkShow show'
-    end
+val show = fn [a] (_ : show a) =>
+              let
+                  fun show' (ls : list a) =
+                      case ls of
+                          [] => "[]"
+                        | x :: ls => show x ^ " :: " ^ show' ls
+              in
+                  mkShow show'
+              end
 
-val rev (a ::: Type) =
-    let
-        fun rev' acc (ls : list a) =
-            case ls of
-                [] => acc
-              | x :: ls => rev' (x :: acc) ls
-    in
-        rev' []
-    end
+val rev = fn [a] =>
+             let
+                 fun rev' acc (ls : list a) =
+                     case ls of
+                         [] => acc
+                       | x :: ls => rev' (x :: acc) ls
+             in
+                 rev' []
+             end
 
-val revAppend (a ::: Type) =
-    let
-        fun ra (ls : list a) acc =
-            case ls of
-                [] => acc
-              | x :: ls => ra ls (x :: acc)
-    in
-        ra
-    end
+val revAppend = fn [a] =>
+                   let
+                       fun ra (ls : list a) acc =
+                           case ls of
+                               [] => acc
+                             | x :: ls => ra ls (x :: acc)
+                   in
+                       ra
+                   end
 
-fun append (a ::: Type) (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2                
+fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2                
 
-fun mp (a ::: Type) (b ::: Type) f =
+fun mp [a] [b] f =
     let
         fun mp' acc ls =
             case ls of
@@ -42,7 +42,7 @@ fun mp (a ::: Type) (b ::: Type) f =
         mp' []
     end
 
-fun mapPartial (a ::: Type) (b ::: Type) f =
+fun mapPartial [a] [b] f =
     let
         fun mp' acc ls =
             case ls of
@@ -54,7 +54,7 @@ fun mapPartial (a ::: Type) (b ::: Type) f =
         mp' []
     end
 
-fun mapX (a ::: Type) (ctx ::: {Unit}) f =
+fun mapX [a] [ctx ::: {Unit}] f =
     let
         fun mapX' ls =
             case ls of
@@ -64,7 +64,7 @@ fun mapX (a ::: Type) (ctx ::: {Unit}) f =
         mapX'
     end
 
-fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f =
+fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
     let
         fun mapM' acc ls =
             case ls of
@@ -74,7 +74,7 @@ fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f =
         mapM' []
     end
 
-fun filter (a ::: Type) f =
+fun filter [a] f =
     let
         fun fil acc ls =
             case ls of
@@ -84,7 +84,7 @@ fun filter (a ::: Type) f =
         fil []
     end
 
-fun exists (a ::: Type) f =
+fun exists [a] f =
     let
         fun ex ls =
             case ls of
@@ -98,7 +98,7 @@ fun exists (a ::: Type) f =
         ex
     end
 
-fun foldlMap (a ::: Type) (b ::: Type) (c ::: Type) f =
+fun foldlMap [a] [b] [c] f =
     let
         fun fold ls' st ls =
             case ls of
diff --git a/lib/ur/listPair.ur b/lib/ur/listPair.ur
index 9a56f75a..a46cf187 100644
--- a/lib/ur/listPair.ur
+++ b/lib/ur/listPair.ur
@@ -1,4 +1,4 @@
-fun mapX (a ::: Type) (b ::: Type) (ctx ::: {Unit}) f =
+fun mapX [a] [b] [ctx ::: {Unit}] f =
     let
         fun mapX' ls1 ls2 =
             case (ls1, ls2) of
diff --git a/src/elab_util.sml b/src/elab_util.sml
index c2101ae3..8082cb1e 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -438,29 +438,30 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
 
               | ELet (des, e, t) =>
                 let
-                    val (des, ctx) = foldl (fn (ed, (des, ctx)) =>
-                                               let
-                                                   val ctx' =
-                                                       case #1 ed of
-                                                           EDVal (p, _, _) => doVars (p, ctx)
-                                                         | EDValRec vis =>
-                                                           foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
-                                               in
-                                                   (S.bind2 (des,
-                                                          fn des' =>
-                                                             S.map2 (mfed ctx ed,
-                                                               fn ed' => des' @ [ed'])),
-                                                    ctx')
-                                               end)
+                    val (des, ctx') = foldl (fn (ed, (des, ctx)) =>
+                                                let
+                                                    val ctx' =
+                                                        case #1 ed of
+                                                            EDVal (p, _, _) => doVars (p, ctx)
+                                                          | EDValRec vis =>
+                                                            foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t)))
+                                                                  ctx vis
+                                                in
+                                                    (S.bind2 (des,
+                                                           fn des' =>
+                                                              S.map2 (mfed ctx ed,
+                                                                   fn ed' => ed' :: des')),
+                                                     ctx')
+                                                end)
                                             (S.return2 [], ctx) des
                 in
                     S.bind2 (des,
                          fn des' =>
-                            S.bind2 (mfe ctx e,
+                            S.bind2 (mfe ctx' e,
                                     fn e' =>
                                        S.map2 (mfc ctx t,
                                                fn t' =>
-                                                  (ELet (des', e', t'), loc))))
+                                                  (ELet (rev des', e', t'), loc))))
                 end
 
               | EKAbs (x, e) =>
@@ -479,7 +480,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                 EDVal (p, t, e) =>
                 S.bind2 (mfc ctx t,
                          fn t' =>
-                            S.map2 (mfe (doVars (p, ctx)) e,
+                            S.map2 (mfe ctx e,
                                  fn e' =>
                                     (EDVal (p, t', e'), loc)))
               | EDValRec vis =>
diff --git a/src/unnest.sml b/src/unnest.sml
index 3dfa741d..e0245c6f 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -241,10 +241,12 @@ fun exp ((ks, ts), e as old, st : state) =
                                                        end)
                                                    (IS.empty, IS.empty) vis
 
-                            (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")
-                            val () = app (fn (x, t) =>
+                            (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
+                            (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
+                            (*val () = app (fn (x, t) =>
                                              Print.prefaces "Var" [("x", Print.PD.string x),
-                                                                   ("t", ElabPrint.p_con E.empty t)]) ts*)
+                                                                   ("t", ElabPrint.p_con E.empty t)]) ts
+                            val () = IS.app (fn n => print ("Free: " ^ Int.toString n ^ "\n")) efv*)
 
                             val cfv = IS.foldl (fn (x, cfv) =>
                                                    let