diff options
| -rw-r--r-- | source/lux/data/list.lux | 2 | ||||
| -rw-r--r-- | src/lux/analyser.clj | 17 | ||||
| -rw-r--r-- | src/lux/type.clj | 56 |
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)] |