From 08584c8d9a462ce0bd3ffb6d9535ecb3f7043289 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Mon, 7 Sep 2015 01:33:53 -0400 Subject: - Type checking of polymorphic functions now relies on ExT types to guarantee that type-variables don't unify to anything, instead of relying on VarT types. - Fixed some bugs in the standard library due to improper behavior of the type-checker. - The analysis and pattern-matching code for records now reuses that of tuples. --- source/lux/codata/state.lux | 3 +- source/lux/meta/syntax.lux | 5 +- src/lux/analyser.clj | 6 ++ src/lux/analyser/case.clj | 26 +------ src/lux/analyser/lux.clj | 161 +++++++++++++++++++++++--------------------- src/lux/type.clj | 14 +++- 6 files changed, 110 insertions(+), 105 deletions(-) diff --git a/source/lux/codata/state.lux b/source/lux/codata/state.lux index ec0a6bf63..de7220a45 100644 --- a/source/lux/codata/state.lux +++ b/source/lux/codata/state.lux @@ -12,7 +12,8 @@ (-> s (, s a))) ## [Structures] -(defstruct #export State/Functor (Functor State) +(defstruct #export State/Functor (All [s] + (Functor (State s))) (def (map f ma) (lambda [state] (let [[state' a] (ma state)] diff --git a/source/lux/meta/syntax.lux b/source/lux/meta/syntax.lux index ee5a37d53..4ee3163b0 100644 --- a/source/lux/meta/syntax.lux +++ b/source/lux/meta/syntax.lux @@ -183,13 +183,14 @@ (def #export (|^ p1 p2 tokens) (All [a b] - (-> (Parser a) (Parser b) (Parser (Either b)))) + (-> (Parser a) (Parser b) (Parser (Either a b)))) (case (p1 tokens) (#;Some [tokens' x1]) (#;Some [tokens' (#;Left x1)]) #;None (run-parser (do Parser/Monad [x2 p2] (wrap (#;Right x2))) - tokens))) + tokens) + )) (def #export (||^ ps tokens) (All [a] diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj index fbc360628..9a57191f5 100644 --- a/src/lux/analyser.clj +++ b/src/lux/analyser.clj @@ -532,6 +532,12 @@ (prn 'analyse-basic-ast/Error-1 e) (prn 'analyse-basic-ast/Error-2 (&/show-ast token)) (prn 'analyse-basic-ast/Error-3 (&type/show-type exo-type)) + (|case ((&type/deref+ exo-type) state) + (&/$Right [_state _exo-type]) + (prn 'analyse-basic-ast/Error-4 (&type/show-type _exo-type)) + + _ + (prn 'analyse-basic-ast/Error-4 'YOLO)) (throw e)) ) (&/$Right state* output) diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj index 3b12270c2..f2afdb0e9 100644 --- a/src/lux/analyser/case.clj +++ b/src/lux/analyser/case.clj @@ -49,14 +49,9 @@ (resolve-type type*)) (&/$UnivQ _) - ;; (&type/actual-type _abody) (|do [$var &type/existential =type (&type/apply-type type $var)] (&type/actual-type =type)) - ;; (&type/with-var - ;; (fn [$var] - ;; (|do [=type (&type/apply-type type $var)] - ;; (&type/actual-type =type)))) _ (&type/actual-type type))) @@ -126,7 +121,7 @@ (adjust-type* (&/|list) type)) (defn ^:private analyse-pattern [value-type pattern kont] - (|let [[_ pattern*] pattern] + (|let [[meta pattern*] pattern] (|case pattern* (&/$SymbolS "" name) (|do [=kont (&env/with-local name value-type @@ -183,23 +178,8 @@ (fail (str "[Pattern-matching Error] Tuples require tuple-types: " (&type/show-type value-type*)))))) (&/$RecordS pairs) - (|do [?members (&&record/order-record pairs) - value-type* (adjust-type value-type)] - (|case value-type* - (&/$TupleT ?member-types) - (if (not (.equals ^Object (&/|length ?member-types) (&/|length ?members))) - (fail (str "[Pattern-matching Error] Pattern-matching mismatch. Require record[" (&/|length ?member-types) "]. Given record[" (&/|length ?members) "]")) - (|do [[=tests =kont] (&/fold (fn [kont* vm] - (|let [[v m] vm] - (|do [[=test [=tests =kont]] (analyse-pattern v m kont*)] - (return (&/T (&/Cons$ =test =tests) =kont))))) - (|do [=kont kont] - (return (&/T (&/|list) =kont))) - (&/|reverse (&/zip2 ?member-types ?members)))] - (return (&/T (&/V $TupleTestAC =tests) =kont)))) - - _ - (fail "[Pattern-matching Error] Record requires record-type."))) + (|do [?members (&&record/order-record pairs)] + (analyse-pattern value-type (&/T meta (&/V &/$TupleS ?members)) kont)) (&/$TagS ?ident) (|do [;; :let [_ (println "#00" (&/ident->text ?ident))] diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj index 3a9b822ca..f22cc6c9a 100644 --- a/src/lux/analyser/lux.clj +++ b/src/lux/analyser/lux.clj @@ -44,19 +44,39 @@ (analyse-tuple analyse exo-type** ?elems)))) _ - (fail (str "[Analyser Error] Tuples require tuple-types: " (&type/show-type exo-type*) (&type/show-type exo-type)))))))) + (fail (str "[Analyser Error] Tuples require tuple-types: " (&type/show-type exo-type*) " " (&type/show-type exo-type) " " "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]")) + ;; (assert false (str "[Analyser Error] Tuples require tuple-types: " (&type/show-type exo-type*) " " (&type/show-type exo-type) " " "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]")) + ))))) -(defn ^:private analyse-variant-body [analyse exo-type ?values] - (|do [output (|case ?values - (&/$Nil) - (analyse-tuple analyse exo-type (&/|list)) - - (&/$Cons ?value (&/$Nil)) - (analyse exo-type ?value) +(defn with-attempt [m-value on-error] + (fn [state] + (|case (m-value state) + (&/$Left msg) + ((on-error msg) state) + + output + output))) - _ - (analyse-tuple analyse exo-type ?values) - )] +(defn ^:private analyse-variant-body [analyse exo-type ?values] + (|do [output (with-attempt + (|case ?values + (&/$Nil) + (analyse-tuple analyse exo-type (&/|list)) + + (&/$Cons ?value (&/$Nil)) + (analyse exo-type ?value) + + _ + (analyse-tuple analyse exo-type ?values)) + (fn [err] + (fail (str err "\n" + 'analyse-variant-body " " (&type/show-type exo-type) + " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")))) + ;; (assert false + ;; (str err "\n" + ;; 'analyse-variant-body " " (&type/show-type exo-type) + ;; " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")))) + ))] (|case output (&/$Cons x (&/$Nil)) (return x) @@ -78,7 +98,13 @@ (&/$VariantT ?cases) (|case (&/|at idx ?cases) (&/$Some vtype) - (|do [=value (analyse-variant-body analyse vtype ?values)] + (|do [=value (with-attempt + (analyse-variant-body analyse vtype ?values) + (fn [err] + (|do [_exo-type (&type/deref+ exo-type)] + (fail (str err "\n" + 'analyse-variant " " idx " " (&type/show-type exo-type) " " (&type/show-type _exo-type) + " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")))))))] (return (&/|list (&/T (&/V &&/$variant (&/T idx =value)) exo-type)))) @@ -95,41 +121,8 @@ (fail (str "[Analyser Error] Can't create a variant if the expected type is " (&type/show-type exo-type*)))))) (defn analyse-record [analyse exo-type ?elems] - ;; (when @&type/!flag - ;; (prn 'analyse-record (&type/show-type exo-type) - ;; (&/->seq (&/|map (fn [pair] - ;; (|let [[k v] pair] - ;; (str (&/show-ast k) " " (&/show-ast v)))) - ;; ?elems)))) - (|do [exo-type* (|case exo-type - (&/$VarT ?id) - (|do [exo-type* (&type/deref ?id)] - (&type/actual-type exo-type*)) - - (&/$UnivQ _) - (|do [$var &type/existential - =type (&type/apply-type exo-type $var)] - (&type/actual-type =type)) - ;; (&type/with-var - ;; (fn [$var] - ;; (|do [=type (&type/apply-type exo-type $var)] - ;; (&type/actual-type =type)))) - - _ - (&type/actual-type exo-type)) - types (|case exo-type* - (&/$TupleT ?table) - (return ?table) - - _ - (fail (str "[Analyser Error] The type of a record must be a record-type:\n" (&type/show-type exo-type*) "\n" (&type/show-type exo-type)))) - _ (&/assert! (= (&/|length types) (&/|length ?elems)) - (str "[Analyser Error] Record length mismatch. Expected: " (&/|length types) "; actual: " (&/|length ?elems))) - members (&&record/order-record ?elems) - =members (&/map2% (fn [elem-t elem] - (&&/analyse-1 analyse elem-t elem)) - types members)] - (return (&/|list (&/T (&/V &&/$tuple =members) exo-type))))) + (|do [members (&&record/order-record ?elems)] + (analyse-tuple analyse exo-type members))) (defn ^:private analyse-global [analyse exo-type module name] (|do [[[r-module r-name] $def] (&&module/find-def module name) @@ -222,7 +215,10 @@ ;; (prn 'analyse-apply* (aget fun-type 0)) (|case ?args (&/$Nil) - (|do [_ (&type/check exo-type fun-type)] + (|do [;; :let [_ (prn 'analyse-apply*/_0 (&type/show-type exo-type) (&type/show-type fun-type))] + _ (&type/check exo-type fun-type) + ;; :let [_ (prn 'analyse-apply*/_1 'SUCCESS (str "(_ " (->> ?args (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) ")"))] + ] (return (&/T fun-type (&/|list)))) (&/$Cons ?arg ?args*) @@ -248,7 +244,12 @@ (&/$LambdaT ?input-t ?output-t) (|do [[=output-t =args] (analyse-apply* analyse exo-type ?output-t ?args*) - =arg (&&/analyse-1 analyse ?input-t ?arg)] + =arg (with-attempt + (&&/analyse-1 analyse ?input-t ?arg) + (fn [err] + (fail (str err "\n" + 'analyse-apply* " " (&type/show-type exo-type) " " (&type/show-type ?fun-type*) + " " "(_ " (->> ?args (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) ")"))))] (return (&/T =output-t (&/Cons$ =arg =args)))) ;; [[&/$VarT ?id-t]] @@ -325,35 +326,39 @@ (defn analyse-lambda** [analyse exo-type ?self ?arg ?body] (|case exo-type (&/$UnivQ _) - (&type/with-var - (fn [$var] - (|do [exo-type* (&type/apply-type exo-type $var) - [_expr _] (analyse-lambda** analyse exo-type* ?self ?arg ?body)] - (|case $var - (&/$VarT ?id) - (|do [? (&type/bound? ?id)] - (if ? - (|do [dtype (&type/deref ?id) - ;; dtype* (&type/actual-type dtype) - ] - (|case dtype - (&/$BoundT ?vname) - (return (&/T _expr exo-type)) - - (&/$ExT _) - (return (&/T _expr exo-type)) - - (&/$VarT ?_id) - (|do [?? (&type/bound? ?_id)] - ;; (return (&/T _expr exo-type)) - (if ?? - (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype))) - (return (&/T _expr exo-type))) - ) - - _ - (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype))))) - (return (&/T _expr exo-type)))))))) + (|do [$var &type/existential + exo-type* (&type/apply-type exo-type $var) + [_expr _] (analyse-lambda** analyse exo-type* ?self ?arg ?body)] + (return (&/T _expr exo-type))) + ;; (&type/with-var + ;; (fn [$var] + ;; (|do [exo-type* (&type/apply-type exo-type $var) + ;; [_expr _] (analyse-lambda** analyse exo-type* ?self ?arg ?body)] + ;; (|case $var + ;; (&/$VarT ?id) + ;; (|do [? (&type/bound? ?id)] + ;; (if ? + ;; (|do [dtype (&type/deref ?id) + ;; ;; dtype* (&type/actual-type dtype) + ;; ] + ;; (|case dtype + ;; (&/$BoundT ?vname) + ;; (return (&/T _expr exo-type)) + + ;; (&/$ExT _) + ;; (return (&/T _expr exo-type)) + + ;; (&/$VarT ?_id) + ;; (|do [?? (&type/bound? ?_id)] + ;; ;; (return (&/T _expr exo-type)) + ;; (if ?? + ;; (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype))) + ;; (return (&/T _expr exo-type))) + ;; ) + + ;; _ + ;; (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype))))) + ;; (return (&/T _expr exo-type)))))))) _ (|do [exo-type* (&type/actual-type exo-type)] diff --git a/src/lux/type.clj b/src/lux/type.clj index 5fbc33de2..889d4fc47 100644 --- a/src/lux/type.clj +++ b/src/lux/type.clj @@ -342,7 +342,9 @@ (deref id) _ - (fail (str "[Type Error] Type is not a variable: " (show-type type))))) + ;; (assert false (str "[Type Error] Type is not a variable: " (show-type type))) + (fail (str "[Type Error] Type is not a variable: " (show-type type))) + )) (defn set-var [id type] (fn [state] @@ -370,6 +372,7 @@ id)))) (def existential + ;; (Lux Type) (|do [seed &/gen-id] (return (&/V &/$ExT seed)))) @@ -650,6 +653,9 @@ (&/$NamedT ?name ?type) (apply-type ?type param) + + (&/$ExT id) + (return (App$ type-fn param)) _ (fail (str "[Type System] Not a type function:\n" (show-type type-fn) "\n")))) @@ -728,6 +734,11 @@ (check* class-loader fixpoints expected bound)) state))) + [(&/$AppT (&/$ExT eid) eA) (&/$AppT (&/$ExT aid) aA)] + (if (= eid aid) + (check* class-loader fixpoints eA aA) + (fail (check-error expected actual))) + [(&/$AppT (&/$VarT ?eid) A1) (&/$AppT (&/$VarT ?aid) A2)] (fn [state] (|case ((|do [F1 (deref ?eid)] @@ -757,6 +768,7 @@ [fixpoints** _] (check* class-loader fixpoints* A1 A2)] (return (&/T fixpoints** nil))) state)))) + ;; (|do [_ (check* class-loader fixpoints (Var$ ?eid) (Var$ ?aid)) ;; _ (check* class-loader fixpoints A1 A2)] ;; (return (&/T fixpoints nil))) -- cgit v1.2.3