aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorEduardo Julian2015-09-07 01:33:53 -0400
committerEduardo Julian2015-09-07 01:33:53 -0400
commit08584c8d9a462ce0bd3ffb6d9535ecb3f7043289 (patch)
tree7e8355c804c26c0232620a67f7c1054151ee21aa /src
parent77aae538ed0d128e291292b5defe80967d181be9 (diff)
- 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.
Diffstat (limited to 'src')
-rw-r--r--src/lux/analyser.clj6
-rw-r--r--src/lux/analyser/case.clj26
-rw-r--r--src/lux/analyser/lux.clj161
-rw-r--r--src/lux/type.clj14
4 files changed, 105 insertions, 102 deletions
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)))