aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEduardo Julian2015-09-28 21:22:42 -0400
committerEduardo Julian2015-09-28 21:22:42 -0400
commit968eb87adef6d62803543adf2ec51049527ccb33 (patch)
tree92d6462bae32cb57d22b1db90d47f3c2482c5887
parent39a00124a102e5479271c2dbd6791979a34e1e2e (diff)
- Added a rule that Void is a subtype of every other type.
- Added the type-checking rules for existential quantification (ExQ). - Fixed one of the rules for type-checking universal quantification (UnivQ).
-rw-r--r--source/lux/data/list.lux2
-rw-r--r--src/lux/analyser.clj17
-rw-r--r--src/lux/type.clj56
3 files changed, 42 insertions, 33 deletions
diff --git a/source/lux/data/list.lux b/source/lux/data/list.lux
index 7b9d4a60b..563282f32 100644
--- a/source/lux/data/list.lux
+++ b/source/lux/data/list.lux
@@ -190,7 +190,7 @@
(#;Cons [x (#;Cons [sep (interpose sep xs')])])))
(def #export (size list)
- (-> List Int)
+ (All [a] (-> (List a) Int))
(foldL (lambda [acc _] (i:+ 1 acc)) 0 list))
(do-template [<name> <init> <op>]
diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index 4e1093cec..c02ba03d0 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -68,7 +68,7 @@
(&&lux/analyse-variant analyser (&/V &/$Right exo-type) idx values)
)))
-(defn ^:private aba8 [analyse eval! compile-module compile-token exo-type token]
+(defn ^:private aba10 [analyse eval! compile-module compile-token exo-type token]
(|case token
;; Arrays
(&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_znewarray")] (&/$Cons ?length (&/$Nil))))
@@ -116,6 +116,12 @@
(&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_laload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
(&&host/analyse-jvm-laload analyse exo-type ?array ?idx)
+ _
+ (assert false (str "Unknown syntax: " (prn-str (&/show-ast (&&/|meta (&/T "" -1 -1) token)))))))
+
+(defn ^:private aba9 [analyse eval! compile-module compile-token exo-type token]
+ (|case token
+ ;; Arrays
(&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_fnewarray")] (&/$Cons [_ (&/$SymbolS _ ?class)] (&/$Cons ?length (&/$Nil)))))
(&&host/analyse-jvm-fnewarray analyse exo-type ?length)
@@ -143,6 +149,12 @@
(&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_caload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
(&&host/analyse-jvm-caload analyse exo-type ?array ?idx)
+ _
+ (aba10 analyse eval! compile-module compile-token exo-type token)))
+
+(defn ^:private aba8 [analyse eval! compile-module compile-token exo-type token]
+ (|case token
+ ;; Arrays
(&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_anewarray")] (&/$Cons [_ (&/$TextS ?class)] (&/$Cons ?length (&/$Nil)))))
(&&host/analyse-jvm-anewarray analyse exo-type ?class ?length)
@@ -156,8 +168,7 @@
(&&host/analyse-jvm-arraylength analyse exo-type ?array)
_
- (do (prn 'aba8 (&/adt->text token))
- (assert false (str "Unknown syntax: " (prn-str (&/show-ast (&&/|meta (&/T "" -1 -1) token))))))))
+ (aba9 analyse eval! compile-module compile-token exo-type token)))
(defn ^:private aba7 [analyse eval! compile-module compile-token exo-type token]
(|case token
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 7eae7e181..ed0dd8898 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -638,10 +638,13 @@
(check* class-loader fixpoints invariant?? expected actual*))
[(&/$UnivQ _) _]
- (with-var
- (fn [$arg]
- (|do [expected* (apply-type expected $arg)]
- (check* class-loader fixpoints invariant?? expected* actual))))
+ (|do [$arg existential
+ expected* (apply-type expected $arg)]
+ (check* class-loader fixpoints invariant?? expected* actual))
+ ;; (with-var
+ ;; (fn [$arg]
+ ;; (|do [expected* (apply-type expected $arg)]
+ ;; (check* class-loader fixpoints invariant?? expected* actual))))
[_ (&/$UnivQ _)]
(with-var
@@ -649,6 +652,23 @@
(|do [actual* (apply-type actual $arg)]
(check* class-loader fixpoints invariant?? expected actual*))))
+ [(&/$ExQ e!env e!def) _]
+ (with-var
+ (fn [$arg]
+ (|let [expected* (beta-reduce (->> e!env
+ (&/Cons$ expected)
+ (&/Cons$ $arg))
+ e!def)]
+ (check* class-loader fixpoints invariant?? expected* actual))))
+
+ [_ (&/$ExQ a!env a!def)]
+ (|do [$arg existential]
+ (|let [actual* (beta-reduce (->> a!env
+ (&/Cons$ expected)
+ (&/Cons$ $arg))
+ a!def)]
+ (check* class-loader fixpoints invariant?? expected actual*)))
+
[(&/$DataT e!data) (&/$DataT a!data)]
(&&host/check-host-types (partial check* class-loader fixpoints true)
check-error
@@ -658,31 +678,6 @@
invariant??
e!data
a!data)
- ;; [(&/$DataT e!name e!params) (&/$DataT a!name a!params)]
- ;; (cond (= "#Null" a!name)
- ;; (if (not (&&host/primitive-type? e!name))
- ;; (return (&/T fixpoints nil))
- ;; (fail (check-error expected actual)))
-
- ;; (= "#Null" e!name)
- ;; (if (= "#Null" a!name)
- ;; (return (&/T fixpoints nil))
- ;; (fail (check-error expected actual)))
-
- ;; :else
- ;; (let [e!name (&&host/as-obj e!name)
- ;; a!name (&&host/as-obj a!name)]
- ;; (cond (and (.equals ^Object e!name a!name)
- ;; (= (&/|length e!params) (&/|length a!params)))
- ;; (|do [_ (&/map2% (partial check* class-loader fixpoints true) e!params a!params)]
- ;; (return (&/T fixpoints nil)))
-
- ;; (not invariant??)
- ;; (|do [actual* (&&host/->super-type existential class-loader e!name a!name a!params)]
- ;; (check* class-loader fixpoints invariant?? expected actual*))
-
- ;; :else
- ;; (fail (str "[Type Error] Names don't match: " e!name " =/= " a!name)))))
[(&/$LambdaT eI eO) (&/$LambdaT aI aO)]
(|do [[fixpoints* _] (check* class-loader fixpoints invariant?? aI eI)]
@@ -696,6 +691,9 @@
e!members a!members)]
(return (&/T fixpoints* nil)))
+ [_ (&/$VariantT (&/$Nil))]
+ (return (&/T fixpoints nil))
+
[(&/$VariantT e!cases) (&/$VariantT a!cases)]
(|do [fixpoints* (&/fold2% (fn [fp e a]
(|do [[fp* _] (check* class-loader fp invariant?? e a)]