Fix #27: implement multi-let

src/dhall_clj/alpha_normalize.clj

@@ -56,21 +56,33 @@
        (update :b alpha-normalize)))
 
   dhall_clj.ast.Let
-  (alpha-normalize [{:keys [label type? body next] :as this}]
-    (let [var   (->Var label 0)
+  (alpha-normalize [{:keys [bindings next] :as this}]
+    (let [[{:keys [label type? e] :as binding} & more-bindings] bindings
+          var   (->Var label 0)
           v'    (->Var "_" 0)
           next' (if (= label "_")
                   (alpha-normalize next)
                   (-> next
                      (shift 1 v')
                      (subst var v')
                      (shift -1 var)
-                     (alpha-normalize)))]
-      (assoc this
-             :label "_"
-             :type? (when type? (alpha-normalize type?))
-             :body  (alpha-normalize body)
-             :next  next')))
+                     (alpha-normalize)))
+          type?'   (when type? (alpha-normalize type?))
+          binding' (assoc
+                     binding
+                     :label "_"
+                     :type? type?'
+                     :e (alpha-normalize e))]
+      (if-not (seq more-bindings)
+        (assoc
+          this
+          :bindings (list binding')
+          :next next')
+        (-> this
+           (update :bindings rest)
+           (assoc :next next')
+           (alpha-normalize)
+           (update :bindings conj binding')))))
 
   dhall_clj.ast.Annot
   (alpha-normalize [this]

src/dhall_clj/ast.clj

@@ -21,25 +21,14 @@
 
 
 ;; All classes that form the expression tree follow
-;;
-;;   Implementation note: the classes here are basically the constructors
-;;   of the Expr type that the Haskell implementation has in Dhall.Core
-;;
-;;   However, two constructors are missing here:
-;;
-;;   - `Note`: this is used there for keeping track of the source position.
-;;     Here we use the metadata on nodes for that.
-;;
-;;   - `Embed`: it's there to make extending the type nice there, while
-;;     keeping type safety. Here we just hope we have enough tests :)
-
 
 (defrecord Const [c])
 (defrecord Var [x i])
 (defrecord Lam [arg type body])
 (defrecord Pi [arg type body])
 (defrecord App [a b])
-(defrecord Let [label type? body next])
+(defrecord Binding [label type? e]) ;; This is only ever contained only in Let
+(defrecord Let [bindings next])
 (defrecord Annot [val type])
 (defrecord BoolT [])
 (defrecord BoolLit [b])
@@ -161,14 +150,21 @@
        (update :b shift diff var)))
 
   Let
-  (shift [{:keys [label type?] :as this} diff {:keys [x i] :as var}]
-    (let [i' (if (= x label)
+  (shift [{:keys [bindings next] :as this} diff {:keys [x i] :as var}]
+    (let [[{:keys [label type?] :as binding} & more-bindings] bindings
+          i' (if (= x label)
                (inc i)
-               i)]
-      (-> this
-         (assoc  :type? (when type? (shift type? diff var)))
-         (update :body shift diff var)
-         (update :next shift diff (assoc var :i i')))))
+               i)
+          type?' (when type? (shift type? diff var))
+          binding' (-> binding
+                      (assoc :type? type?')
+                      (update :e shift diff var))]
+      (if-not (seq more-bindings)
+        (-> this
+           (assoc :bindings (list binding'))
+           (update :next shift diff (assoc var :i i')))
+        (let [new (shift (update this :bindings rest) diff var)]
+          (update new :bindings conj binding')))))
 
   Annot
   (shift [this diff var]
@@ -457,15 +453,22 @@
        (update :b subst var e)))
 
   Let
-  (subst [{:keys [label type?] :as this} {:keys [x i] :as var} e]
-    (let [y  label
+  (subst [{:keys [bindings next] :as this} {:keys [x i] :as var} e]
+    (let [[{:keys [label type?] :as binding} & more-bindings] bindings
+          y  label
           i' (if (= x y)
                (inc i)
-               i)]
-      (-> this
-         (assoc  :type? (when type? (subst type? var e)))
-         (update :body subst var e)
-         (update :next subst (->Var x i') (shift e 1 (->Var y 0))))))
+               i)
+          type?' (when type? (subst type? var e))
+          binding' (-> binding
+                      (assoc :type? type?')
+                      (update :e subst var e))]
+      (if-not (seq more-bindings)
+        (-> this
+           (assoc :bindings (list binding'))
+           (update :next subst (->Var x i') (shift e 1 (->Var y 0))))
+        (let [new (subst (update this :bindings rest) var e)]
+          (update new :bindings conj binding')))))
 
   Annot
   (subst [this var e]

src/dhall_clj/beta_normalize.clj

@@ -269,14 +269,19 @@
             :else (->App f' a'))))))
 
   dhall_clj.ast.Let
-  (beta-normalize [{:keys [label body next]}]
-    (let [var   (->Var label 0)
-          body' (shift body 1 var)]
+  (beta-normalize [{:keys [bindings next] :as this}]
+    (let [[{:keys [label type? e] :as binding} & more-bindings] bindings
+          var (->Var label 0)
+          e'  (shift e 1 var)
+          more-let (if (seq more-bindings)
+                     (assoc this :bindings more-bindings)
+                     next)]
       (beta-normalize
-        (-> next
-           (subst var body')
+        (-> more-let
+           (subst var e')
            (shift -1 var)))))
 
+
   dhall_clj.ast.Annot
   (beta-normalize [this]
     (beta-normalize (:val this)))

src/dhall_clj/binary.clj

@@ -196,12 +196,15 @@
                        (recur (conj res (decbor e) s) more))
                      res))))
           ;; TODO imports
-          25 (if (= 4 (count e))
-               (let [[label body next] (rest e)]
-                 (->Let label nil (decbor body) (decbor next)))
-               (let [[label typ body next] (rest e)]
-                 (assert-len! e 5)
-                 (->Let label (decbor typ) (decbor body) (decbor next))))
+          25 (->Let
+               (mapv
+                 (fn [[label type? body]]
+                   (->Binding
+                     label
+                     (when-not (nil? type?) (decbor type?))
+                     (decbor body)))
+                 (partition 3 (butlast (rest e))))
+               (decbor (last e)))
           26 (let [[val typ] (rest e)]
                (assert-len! e 3)
                (->Annot (decbor val) (decbor typ))))))))
@@ -259,10 +262,13 @@
     (into [] (concat [0] (map cbor (unapply this)))))
 
   dhall_clj.ast.Let
-  (cbor [{:keys [label type? body next]}]
-    (if type?
-      [25 label (cbor type?) (cbor body) (cbor next)]
-      [25 label              (cbor body) (cbor next)]))
+  (cbor [{:keys [bindings next]}]
+    (letfn [(make-binding [{:keys [label type? e]}]
+              [label
+               (when type?
+                 (cbor type?))
+               (cbor e)])]
+      (into [] (concat [25] (mapcat make-binding bindings) [(cbor next)]))))
 
   dhall_clj.ast.Annot
   (cbor [{:keys [val type]}]

src/dhall_clj/emit.clj

@@ -35,8 +35,13 @@
     `(~(emit a) ~(emit b)))
 
   dhall_clj.ast.Let
-  (emit [{:keys [label type? body next]}]
-    `(let [~(symbol label) ~(emit body)]
+  (emit [{:keys [bindings next]}]
+    `(let (into
+            []
+            (mapcat
+              (fn [{:keys [label type? e]}]
+                [(symbol label) (emit body)])
+              bindings))
        ~(emit next)))
 
   dhall_clj.ast.Annot

src/dhall_clj/import.clj

@@ -215,11 +215,17 @@
        (update :b resolve-imports state)))
 
   dhall_clj.ast.Let
-  (resolve-imports [{:keys [type?] :as this} state]
-    (-> this
-       (assoc  :type? (when type? (resolve-imports type? state)))
-       (update :body  resolve-imports state)
-       (update :next  resolve-imports state)))
+  (resolve-imports [{:keys [bindings next] :as this} state]
+    (assoc
+      this
+      :bindings (mapv
+                  (fn [{:keys [type? e] :as binding}]
+                    (assoc
+                      binding
+                      :type? (when type? (resolve-imports type? state))
+                      :e (resolve-imports e state)))
+                  bindings)
+      :next (resolve-imports next state)))
 
   dhall_clj.ast.Annot
   (resolve-imports [this state]

src/dhall_clj/parse.clj

@@ -257,15 +257,24 @@
       :if     (->BoolIf (expr (nth c 1))
                         (expr (nth c 3))
                         (expr (nth c 5)))
-      :let    (if (> (count c) 6)
-                (->Let (expr (nth c 1))
-                       (expr (nth c 3))
-                       (expr (nth c 5))
-                       (expr (nth c 7)))
-                (->Let (expr (nth c 1))
-                       nil
-                       (expr (nth c 3))
-                       (expr (nth c 5))))
+      :let    (loop [left c
+                     bindings []]
+                (if (= (count left) 2)
+                  (->Let bindings (expr (second left)))
+                  (if-let [type? (when (= :colon (:t (nth left 2)))
+                                   (expr (nth left 3)))]
+                    (recur
+                      (nthrest left 6)
+                      (conj bindings (->Binding
+                                       (expr (nth left 1))
+                                       type?
+                                       (expr (nth left 5)))))
+                    (recur
+                      (nthrest left 4)
+                      (conj bindings (->Binding
+                                       (expr (nth left 1))
+                                       nil
+                                       (expr (nth left 3))))))))
       :forall (->Pi (expr (nth c 2))
                     (expr (nth c 4))
                     (expr (nth c 7)))

src/dhall_clj/typecheck.clj

@@ -134,34 +134,38 @@
              (shift -1 v))))))
 
   dhall_clj.ast.Let
-  (typecheck [{:keys [label type? body next] :as this} ctx]
-    (let [bodyT (typecheck body ctx)
+  (typecheck [{:keys [bindings next] :as this} ctx]
+    (let [[{:keys [label type? e] :as binding} & more-bindings] bindings
+          bodyT (typecheck e ctx)
           ;; FIXME normalize in the else branch also in the haskell implementation
           _ (when type?
               (typecheck type? ctx)
               (when-not (judgmentally-equal type? bodyT)
                 (fail/annot-mismatch!
                   ctx
                   this
-                  {:val   body
+                  {:val   e
                    :type  (beta-normalize bodyT)
                    :annot (beta-normalize type?)})))
           bodyK (typecheck bodyT ctx)
           v (->Var label 0)
-          body' (-> body
+          body' (-> e
                    (beta-normalize)
-                   (shift 1 v))]
+                   (shift 1 v))
+          more-let (if (seq more-bindings)
+                     (assoc this :bindings more-bindings)
+                     next)]
       ;; If the body's type is Type, we can take a fast path
       ;; and typecheck only at context-insertion-time
       (if (= (->Const :type) (beta-normalize bodyK))
         (let [ctx' (-> (beta-normalize bodyT)
                       (context/insert label ctx)
                       (context/transform (fn [e] (shift e 1 v))))]
-          (-> next
+          (-> more-let
              (typecheck ctx')
              (subst v body')
              (shift -1 v)))
-        (-> next
+        (-> more-let
            (subst v body')
            (shift -1 v)
            (typecheck ctx)))))

test/dhall_clj/ast_test.clj

@@ -35,10 +35,14 @@
            (->Var "x" 0))
     (->Pi "x" (->Const :type) (->Var "x" 0))]
    ;; ↑(1, x, 0, let x = 1 in x) = let x = 1 in x
-   [(shift (->Let "x" nil (->NaturalLit 1) (->Var "x" 0))
+   [(shift (->Let
+             [(->Binding "x" nil (->NaturalLit 1))]
+             (->Var "x" 0))
            1
            (->Var "x" 0))
-    (->Let "x" nil (->NaturalLit 1) (->Var "x" 0))]
+    (->Let
+      [(->Binding "x" nil (->NaturalLit 1))]
+      (->Var "x" 0))]
    ;; ↑(1, x, 0, λ(y : Type) → x) = λ(y : Type) → x@1
    [(shift (->Lam "y" (->Const :type) (->Var "x" 0))
            1
@@ -50,10 +54,14 @@
            (->Var "x" 0))
     (->Pi "y" (->Const :type) (->Var "x" 1))]
    ;; ↑(1, x, 0, let y = 1 in x) = let y = 1 in x@1
-   [(shift (->Let "y" nil (->NaturalLit 1) (->Var "x" 0))
+   [(shift (->Let
+             [(->Binding "y" nil (->NaturalLit 1))]
+             (->Var "x" 0))
            1
            (->Var "x" 0))
-    (->Let "y" nil (->NaturalLit 1) (->Var "x" 1))]
+    (->Let
+      [(->Binding "y" nil (->NaturalLit 1))]
+      (->Var "x" 1))]
    ;; ↑(1, x, 0, List x) = List x@1
    [(shift (->ListLit (->Var "x" 0) [])
            1

test/dhall_clj/beta_normalize_test.clj

@@ -61,8 +61,6 @@
   "Here we list all the tests that blow up, so we categorize and exclude them.
   Note: they are vectors because the path creation is platform-sensitive."
   [
-   ;; Waiting on issue #27
-   ["dhall-lang" "tests" "normalization" "success" "simple" "letlet"]
    ;; Waiting for single quote strings to be standardized
    ["dhall-lang" "tests" "normalization" "success" "remoteSystems"]])
 

test/dhall_clj/binary_test.clj

@@ -60,7 +60,14 @@
 
 (defn lam          [a b] (gen/fmap (partial apply ->Lam) (gen/tuple label a b)))
 (defn pi           [a b] (gen/fmap (partial apply ->Pi) (gen/tuple label a b)))
-(defn let'         [a b] (gen/fmap (partial apply ->Let) (gen/tuple label (maybe a) a b)))
+(defn let'         [a b] (gen/fmap
+                           (partial apply ->Let)
+                           (gen/tuple
+                             (gen/not-empty
+                               (gen/resize 5 (gen/vector (gen/fmap
+                                                           (partial apply ->Binding)
+                                                           (gen/tuple label (maybe a) a)))))
+                             b)))
 (defn bool-if      [a b] (gen/fmap (partial apply ->BoolIf) (gen/tuple a a b)))
 (defn text         [a b] (gen/fmap
                            ->TextLit