diff --git a/src/dhall_clj/alpha_normalize.clj b/src/dhall_clj/alpha_normalize.clj index 7c8fbd2..e0843bc 100644 --- a/src/dhall_clj/alpha_normalize.clj +++ b/src/dhall_clj/alpha_normalize.clj @@ -56,8 +56,9 @@ (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) @@ -65,12 +66,23 @@ (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] diff --git a/src/dhall_clj/ast.clj b/src/dhall_clj/ast.clj index d9a7da2..6c0e359 100644 --- a/src/dhall_clj/ast.clj +++ b/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] diff --git a/src/dhall_clj/beta_normalize.clj b/src/dhall_clj/beta_normalize.clj index faef4bf..791770b 100644 --- a/src/dhall_clj/beta_normalize.clj +++ b/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))) diff --git a/src/dhall_clj/binary.clj b/src/dhall_clj/binary.clj index fca0b79..fbc2087 100644 --- a/src/dhall_clj/binary.clj +++ b/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]}] diff --git a/src/dhall_clj/emit.clj b/src/dhall_clj/emit.clj index 1989ffe..8701667 100644 --- a/src/dhall_clj/emit.clj +++ b/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 diff --git a/src/dhall_clj/import.clj b/src/dhall_clj/import.clj index 590f9db..44aa536 100644 --- a/src/dhall_clj/import.clj +++ b/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] diff --git a/src/dhall_clj/parse.clj b/src/dhall_clj/parse.clj index 5d4ca75..f5a2067 100644 --- a/src/dhall_clj/parse.clj +++ b/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))) diff --git a/src/dhall_clj/typecheck.clj b/src/dhall_clj/typecheck.clj index 604895a..ff1ce13 100644 --- a/src/dhall_clj/typecheck.clj +++ b/src/dhall_clj/typecheck.clj @@ -134,8 +134,9 @@ (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) @@ -143,25 +144,28 @@ (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))))) diff --git a/test/dhall_clj/ast_test.clj b/test/dhall_clj/ast_test.clj index df0af6e..459d5c2 100644 --- a/test/dhall_clj/ast_test.clj +++ b/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 diff --git a/test/dhall_clj/beta_normalize_test.clj b/test/dhall_clj/beta_normalize_test.clj index eb1da0d..01d1f87 100644 --- a/test/dhall_clj/beta_normalize_test.clj +++ b/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"]]) diff --git a/test/dhall_clj/binary_test.clj b/test/dhall_clj/binary_test.clj index 11e24d0..21fd622 100644 --- a/test/dhall_clj/binary_test.clj +++ b/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 diff --git a/test/dhall_clj/parser_test.clj b/test/dhall_clj/parser_test.clj index f423490..3bd7b8d 100644 --- a/test/dhall_clj/parser_test.clj +++ b/test/dhall_clj/parser_test.clj @@ -153,10 +153,14 @@ (->BoolT))] ["let x : t = e1 in e2" - (->Let "x" (->Var "t" 0) (->Var "e1" 0) (->Var "e2" 0))] + (->Let + [(->Binding "x" (->Var "t" 0) (->Var "e1" 0))] + (->Var "e2" 0))] ["let x = e1 in e2" - (->Let "x" nil (->Var "e1" 0) (->Var "e2" 0))] + (->Let + [(->Binding "x" nil (->Var "e1" 0))] + (->Var "e2" 0))] ["forall (x : a) -> b" (->Pi "x" (->Var "a" 0) (->Var "b" 0))] @@ -325,19 +329,12 @@ ["dhall-lang" "tests" "parser" "success" "urls"] ["dhall-lang" "tests" "parser" "success" "environmentVariables"] ["dhall-lang" "tests" "parser" "success" "pathTermination"] + ["dhall-lang" "tests" "parser" "success" "importAlt"] ;; Broken operators? ["dhall-lang" "tests" "parser" "success" "operators"] ;; Something's broken ["dhall-lang" "tests" "parser" "success" "largeExpression"] - ;; Waiting on issue #12 - ["dhall-lang" "tests" "parser" "success" "importAlt"] - ;; Waiting on issue #27 - ["dhall-lang" "tests" "parser" "success" "multilet"] - ["dhall-lang" "tests" "parser" "success" "reservedPrefix"] - ["dhall-lang" "tests" "parser" "success" "let"] - ["dhall-lang" "tests" "parser" "success" "label"] - ["dhall-lang" "tests" "parser" "success" "quotedLabel"] ;; Waiting on issue #28 ["dhall-lang" "tests" "parser" "success" "quotedPaths"]]) diff --git a/test/dhall_clj/typecheck_test.clj b/test/dhall_clj/typecheck_test.clj index acd3d2d..2811c1d 100644 --- a/test/dhall_clj/typecheck_test.clj +++ b/test/dhall_clj/typecheck_test.clj @@ -37,11 +37,7 @@ Note: they are vectors because the path creation is platform-sensitive." [ ;; Duplicate fields should fail to typecheck - ["dhall-lang" "tests" "typecheck" "failure" "duplicateFields.dhall"] - - ;; Waiting on issue #27 - ["dhall-lang" "tests" "typecheck" "failure" "hurkensParadox.dhall"] - ["dhall-lang" "tests" "typecheck" "success" "recordOfRecordOfTypes"]]) + ["dhall-lang" "tests" "typecheck" "failure" "duplicateFields.dhall"]]) (defn valid-testcases []