f-f · f-f · Nov 24, 2018
diff --git a/dhall-lang b/dhall-lang
diff --git a/src/dhall_clj/binary.clj b/src/dhall_clj/binary.clj
@@ -88,6 +88,7 @@
       "List"              (->ListT)
       "Type"              (->Const :type)
       "Kind"              (->Const :kind)
+      "Sort"              (->Const :sort)
       (->Var e 0)) ;; If no builtins match, then it's a variable
 
     (integer? e)
@@ -225,9 +226,10 @@
 
   dhall_clj.ast.Const
   (cbor [{:keys [c]}]
-    (if (= c :type)
-      "Type"
-      "Kind"))
+    (condp = c
+      :type "Type"
+      :kind "Kind"
+      :sort "Sort"))
 
   dhall_clj.ast.Var
   (cbor [{:keys [x i]}]

diff --git a/src/dhall_clj/parse.clj b/src/dhall_clj/parse.clj
@@ -259,7 +259,8 @@
       :True-raw     (->BoolLit true)
       :False-raw    (->BoolLit false)
       :Type-raw     (->Const :type)
-      :Kind-raw     (->Const :kind))))
+      :Kind-raw     (->Const :kind)
+      :Sort-raw     (->Const :sort))))
 
 (defmethod expr :reserved-namespaced-raw [e]
   (let [first-tag (-> e :c first :t)]

diff --git a/src/dhall_clj/typecheck.clj b/src/dhall_clj/typecheck.clj
@@ -48,6 +48,22 @@
     (->RecordT (into {} kts))))
 
 
+(defn axiom [c]
+  (condp = c
+    :type :kind
+    :kind :sort
+    :sort (fail/untyped! {} (->Const c))))
+
+(defn rule [c1 c2]
+  (condp = [c1 c2]
+    [:type :type] :type
+    [:kind :type] :type
+    [:kind :kind] :kind
+    [:sort :type] :type
+    [:sort :kind] :sort
+    [:sort :sort] :sort
+    :error))
+
 (defprotocol ITypecheck
   (typecheck [this context]
     "Typecheck an expression in a context.
@@ -59,9 +75,7 @@
 
   dhall_clj.ast.Const
   (typecheck [{:keys [c] :as this} ctx]
-    (if (= :type c)
-      (assoc this :c :kind)
-      (fail/untyped! ctx this)))
+    (assoc this :c (axiom c)))
 
   dhall_clj.ast.Var
   (typecheck [{:keys [x i] :as this} ctx]
@@ -92,10 +106,11 @@
           bodyT (-> body (typecheck ctx') beta-normalize)
           bodyK (if (instance? Const bodyT)
                   (:c bodyT)
-                  (fail/invalid-output-type! ctx' this {:body body}))]
-      (if (and (= typeK :type) (= bodyK :kind))
+                  (fail/invalid-output-type! ctx' this {:body body}))
+          k (rule typeK bodyK)]
+      (if (= k :error)
         (fail/no-dependent-types! ctx this {:type type :body body})
-        (->Const bodyK))))
+        (->Const k))))
 
   dhall_clj.ast.App
   (typecheck [{:keys [a b] :as this} ctx]
@@ -514,8 +529,11 @@
                   (= kind0 (->Const :type))
                   :type
 
+                  (= kind0 (->Const :kind))
+                  :kind
+
                   (and (= kind0 (->Const :kind))
-                       (judgmentally-equal t0 (->Const :type)))
+                       (judgmentally-equal t0 (->Const :kind)))
                   :kind
 
                   :else (fail/invalid-field-type! ctx this {:key k0 :type t0}))]
@@ -526,13 +544,18 @@
                                   (fail/field-annotation-mismatch!
                                     ctx
                                     this
-                                    {:key k :type t :key0 k0 :type0 t0 :meta :type}))
-                (->Const :kind) (if-not (= c :kind)
+                                    {:key k :type t :const c :key0 k0 :type0 t0 :meta :type}))
+                (->Const :kind) (when-not (= c :kind)
+                                  (fail/field-annotation-mismatch!
+                                    ctx
+                                    this
+                                    {:key k :type t :const c :key0 k0 :type0 t0 :meta :kind}))
+                (->Const :sort) (if-not (= c :sort)
                                   (fail/field-annotation-mismatch!
                                     ctx
                                     this
-                                    {:key k :type t :key0 k0 :type0 t0 :meta :kind})
-                                  (when-not (judgmentally-equal t (->Const :type))
+                                    {:key k :type t :const c :key0 k0 :type0 t0 :meta :sort})
+                                  (when-not (judgmentally-equal t (->Const :kind))
                                     (fail/invalid-field-type! ctx this {:key k :type t})))
                 (fail/invalid-field-type! ctx this {:key k :type t})))
             (rest kvs))
@@ -550,10 +573,13 @@
                   (= kind0 (->Const :type))
                   :type
 
-                  (and (= kind0 (->Const :kind))
-                       (judgmentally-equal t0 (->Const :type)))
+                  (= kind0 (->Const :kind))
                   :kind
 
+                  (and (= kind0 (->Const :sort))
+                       (judgmentally-equal t0 (->Const :kind)))
+                  :sort
+
                   :else (fail/invalid-field-type! ctx this {:key k0 :value v0}))]
           (map-kv
             (fn [k v]
@@ -563,12 +589,17 @@
                                     (fail/field-mismatch!
                                       ctx
                                       this
-                                      {:key k :value v :key0 k0 :value0 v0 :meta :type}))
-                  (->Const :kind) (if-not (= c :kind)
+                                      {:key k :value v :const c :key0 k0 :value0 v0 :meta :type}))
+                  (->Const :kind) (when-not (= c :kind)
+                                    (fail/field-mismatch!
+                                      ctx
+                                      this
+                                      {:key k :value v :const c :key0 k0 :value0 v0 :meta :kind}))
+                  (->Const :sort) (if-not (= c :sort)
                                     (fail/field-mismatch!
                                       ctx
                                       this
-                                      {:key k :value v :key0 k0 :value0 v0 :meta :kind})
+                                      {:key k :value v :const c :key0 k0 :value0 v0 :meta :sort})
                                     (when-not (judgmentally-equal t (->Const :type))
                                       (fail/invalid-field-type! ctx this {:key k :type t})))
                   (fail/invalid-field! ctx this {:key k :type t}))

diff --git a/test/dhall_clj/binary_test.clj b/test/dhall_clj/binary_test.clj
@@ -22,7 +22,7 @@
 (def integer (gen/fmap ->IntegerLit gen/int))
 (def bool    (gen/fmap ->BoolLit gen/boolean))
 (def double' (gen/fmap ->DoubleLit (gen/double* {:infinite? false :NaN? false})))
-(def const   (gen/fmap ->Const (gen/elements [:kind :type])))
+(def const   (gen/fmap ->Const (gen/elements [:kind :type :sort])))
 (def var     (gen/fmap (partial apply ->Var) (gen/tuple label gen/nat)))
 (def builtin (gen/elements
                [(->BoolT)

diff --git a/test/dhall_clj/parser_test.clj b/test/dhall_clj/parser_test.clj
@@ -339,9 +339,7 @@
    ["dhall-lang" "tests" "parser" "success" "label"]
    ["dhall-lang" "tests" "parser" "success" "quotedLabel"]
    ;; Waiting on issue #28
-   ["dhall-lang" "tests" "parser" "success" "quotedPaths"]
-   ;; Waiting on issue #17
-   ["dhall-lang" "tests" "parser" "success" "sort"]])
+   ["dhall-lang" "tests" "parser" "success" "quotedPaths"]])
 
 
 (defn valid-testcases []

diff --git a/test/dhall_clj/typecheck_test.clj b/test/dhall_clj/typecheck_test.clj
@@ -39,14 +39,9 @@
    ;; Duplicate fields should fail to typecheck
    ["dhall-lang" "tests" "typecheck" "failure" "duplicateFields.dhall"]
 
-   ;; Waiting on issue #17
+   ;; Waiting on issue #27
    ["dhall-lang" "tests" "typecheck" "failure" "hurkensParadox.dhall"]
-   ["dhall-lang" "tests" "typecheck" "success" "recordOfTypes"]
-   ["dhall-lang" "tests" "typecheck" "success" "accessEncodedType"]
-   ["dhall-lang" "tests" "typecheck" "success" "encodedRecordOfTypes"]
-   ["dhall-lang" "tests" "typecheck" "success" "accessType"]
-   ["dhall-lang" "tests" "typecheck" "success" "simple" "kindParameter"]
-   ["dhall-lang" "tests" "typecheck" "success" "simple" "fieldsAreTypes"]])
+   ["dhall-lang" "tests" "typecheck" "success" "recordOfRecordOfTypes"]])
 
 
 (defn valid-testcases []