aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorEduardo Julian2015-08-28 22:46:12 -0400
committerEduardo Julian2015-08-28 22:46:12 -0400
commit8de225f98aaed212bf3b683208bff5c6ab85a835 (patch)
treef9a3e197c7bf62cffa411f5a9e768cbca6a76d9b /src
parenta10d922283a9256f0f0015d9d00a0c549b1891cb (diff)
- Changed the name of AllT (for-all type) to UnivQ (universal quantification).
- UnivQ no longer stores the environment as key-val pairs with Text names, but instead stores it as type-lists with variables accessed via an index through a (updated) BoundT. - UnivQ no longer stores the name of the type-fun, not the name of the type-arg.
Diffstat (limited to '')
-rw-r--r--src/lux/analyser/case.clj44
-rw-r--r--src/lux/analyser/env.clj4
-rw-r--r--src/lux/analyser/host.clj2
-rw-r--r--src/lux/analyser/lux.clj63
-rw-r--r--src/lux/analyser/module.clj2
-rw-r--r--src/lux/base.clj37
-rw-r--r--src/lux/compiler/type.clj19
-rw-r--r--src/lux/reader.clj4
-rw-r--r--src/lux/type.clj445
9 files changed, 290 insertions, 330 deletions
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj
index 5987cbdf7..829b5b6d8 100644
--- a/src/lux/analyser/case.clj
+++ b/src/lux/analyser/case.clj
@@ -48,7 +48,7 @@
(fail "##9##")))]
(resolve-type type*))
- (&/$AllT _aenv _aname _aarg _abody)
+ (&/$UnivQ _)
;; (&type/actual-type _abody)
(|do [$var &type/existential
=type (&type/apply-type type $var)]
@@ -61,42 +61,46 @@
_
(&type/actual-type type)))
+(defn update-up-frame [frame]
+ (|let [[_env _idx _var] frame]
+ (&/T _env (+ 2 _idx) _var)))
+
(defn adjust-type* [up type]
- "(-> (List (, (Maybe (Env Text Type)) Text Text Type)) Type (Lux Type))"
+ "(-> (List (, (Maybe (List Type)) Int Type)) Type (Lux Type))"
;; (prn 'adjust-type* (&type/show-type type))
(|case type
- (&/$AllT _aenv _aname _aarg _abody)
+ (&/$UnivQ _aenv _abody)
(&type/with-var
(fn [$var]
(|do [=type (&type/apply-type type $var)]
- (adjust-type* (&/|cons (&/T _aenv _aname _aarg $var) up) =type))))
+ (adjust-type* (&/Cons$ (&/T _aenv 1 $var) (&/|map update-up-frame up)) =type))))
(&/$TupleT ?members)
(|do [(&/$TupleT ?members*) (&/fold% (fn [_abody ena]
- (|let [[_aenv _aname _aarg (&/$VarT _avar)] ena]
- (|do [_ (&type/set-var _avar (&/V &/$BoundT _aarg))]
+ (|let [[_aenv _aidx (&/$VarT _avar)] ena]
+ (|do [_ (&type/set-var _avar (&/V &/$BoundT _aidx))]
(&type/clean* _avar _abody))))
type
up)]
(return (&type/Tuple$ (&/|map (fn [v]
(&/fold (fn [_abody ena]
- (|let [[_aenv _aname _aarg _avar] ena]
- (&/V &/$AllT (&/T _aenv _aname _aarg _abody))))
+ (|let [[_aenv _aidx _avar] ena]
+ (&/V &/$UnivQ (&/T _aenv _abody))))
v
up))
?members*))))
(&/$VariantT ?members)
(|do [(&/$VariantT ?members*) (&/fold% (fn [_abody ena]
- (|let [[_aenv _aname _aarg (&/$VarT _avar)] ena]
- (|do [_ (&type/set-var _avar (&/V &/$BoundT _aarg))]
+ (|let [[_aenv _aidx (&/$VarT _avar)] ena]
+ (|do [_ (&type/set-var _avar (&/V &/$BoundT _aidx))]
(&type/clean* _avar _abody))))
type
up)]
(return (&/V &/$VariantT (&/|map (fn [v]
(&/fold (fn [_abody ena]
- (|let [[_aenv _aname _aarg _avar] ena]
- (&/V &/$AllT (&/T _aenv _aname _aarg _abody))))
+ (|let [[_aenv _aidx _avar] ena]
+ (&/V &/$UnivQ (&/T _aenv _abody))))
v
up))
?members*))))
@@ -169,7 +173,7 @@
(|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)))))
+ (return (&/T (&/Cons$ =test =tests) =kont)))))
(|do [=kont kont]
(return (&/T (&/|list) =kont)))
(&/|reverse (&/zip2 ?member-types ?members)))]
@@ -192,7 +196,7 @@
(|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)))))
+ (return (&/T (&/Cons$ =test =tests) =kont)))))
(|do [=kont kont]
(return (&/T (&/|list) =kont)))
(&/|reverse (&/zip2 ?member-types ?members)))]
@@ -242,7 +246,7 @@
(defn ^:private analyse-branch [analyse exo-type value-type pattern body patterns]
(|do [pattern+body (analyse-pattern value-type pattern
(&&/analyse-1 analyse exo-type body))]
- (return (&/|cons pattern+body patterns))))
+ (return (&/Cons$ pattern+body patterns))))
(let [compare-kv #(.compareTo ^String (aget ^objects %1 0) ^String (aget ^objects %2 0))]
(defn ^:private merge-total [struct test+body]
@@ -258,31 +262,31 @@
(return (&/V $BoolTotal (&/T total? (&/|list ?value))))
[($BoolTotal total? ?values) ($BoolTestAC ?value)]
- (return (&/V $BoolTotal (&/T total? (&/|cons ?value ?values))))
+ (return (&/V $BoolTotal (&/T total? (&/Cons$ ?value ?values))))
[($DefaultTotal total?) ($IntTestAC ?value)]
(return (&/V $IntTotal (&/T total? (&/|list ?value))))
[($IntTotal total? ?values) ($IntTestAC ?value)]
- (return (&/V $IntTotal (&/T total? (&/|cons ?value ?values))))
+ (return (&/V $IntTotal (&/T total? (&/Cons$ ?value ?values))))
[($DefaultTotal total?) ($RealTestAC ?value)]
(return (&/V $RealTotal (&/T total? (&/|list ?value))))
[($RealTotal total? ?values) ($RealTestAC ?value)]
- (return (&/V $RealTotal (&/T total? (&/|cons ?value ?values))))
+ (return (&/V $RealTotal (&/T total? (&/Cons$ ?value ?values))))
[($DefaultTotal total?) ($CharTestAC ?value)]
(return (&/V $CharTotal (&/T total? (&/|list ?value))))
[($CharTotal total? ?values) ($CharTestAC ?value)]
- (return (&/V $CharTotal (&/T total? (&/|cons ?value ?values))))
+ (return (&/V $CharTotal (&/T total? (&/Cons$ ?value ?values))))
[($DefaultTotal total?) ($TextTestAC ?value)]
(return (&/V $TextTotal (&/T total? (&/|list ?value))))
[($TextTotal total? ?values) ($TextTestAC ?value)]
- (return (&/V $TextTotal (&/T total? (&/|cons ?value ?values))))
+ (return (&/V $TextTotal (&/T total? (&/Cons$ ?value ?values))))
[($DefaultTotal total?) ($TupleTestAC ?tests)]
(|do [structs (&/map% (fn [t]
diff --git a/src/lux/analyser/env.clj b/src/lux/analyser/env.clj
index 666807586..66478eecc 100644
--- a/src/lux/analyser/env.clj
+++ b/src/lux/analyser/env.clj
@@ -22,7 +22,7 @@
=return (body (&/update$ &/$envs
(fn [stack]
(let [bound-unit (&/V &&/$var (&/V &/$Local (->> (&/|head stack) (&/get$ &/$locals) (&/get$ &/$counter))))]
- (&/|cons (&/update$ &/$locals #(->> %
+ (&/Cons$ (&/update$ &/$locals #(->> %
(&/update$ &/$counter inc)
(&/update$ &/$mappings (fn [m] (&/|put name (&/T bound-unit type) m))))
(&/|head stack))
@@ -31,7 +31,7 @@
(|case =return
(&/$Right ?state ?value)
(return* (&/update$ &/$envs (fn [stack*]
- (&/|cons (&/update$ &/$locals #(->> %
+ (&/Cons$ (&/update$ &/$locals #(->> %
(&/update$ &/$counter dec)
(&/set$ &/$mappings old-mappings))
(&/|head stack*))
diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj
index 8ccfc5ace..098dc89df 100644
--- a/src/lux/analyser/host.clj
+++ b/src/lux/analyser/host.clj
@@ -313,7 +313,7 @@
(&&/analyse-1 analyse (&/V &/$DataT (as-otype ?method-output)) ?method-body))
(&/|reverse (if (:static? =method-modifiers)
=method-inputs
- (&/|cons (&/T ";this" ?super-class)
+ (&/Cons$ (&/T ";this" ?super-class)
=method-inputs)))))]
(return {:name ?method-name
:modifiers =method-modifiers
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index 634769839..c3f7622b8 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -42,7 +42,7 @@
(return (&/|list (&/T (&/V &&/$tuple =elems)
exo-type))))
- (&/$AllT _)
+ (&/$UnivQ _)
(&type/with-var
(fn [$var]
(|do [exo-type** (&type/apply-type exo-type* $var)]
@@ -90,7 +90,7 @@
(&/$None)
(fail (str "[Analyser Error] There is no case " idx " for variant type " (&type/show-type exo-type*))))
- (&/$AllT _)
+ (&/$UnivQ _)
(&type/with-var
(fn [$var]
(|do [exo-type** (&type/apply-type exo-type* $var)]
@@ -98,41 +98,20 @@
_
(fail (str "[Analyser Error] Can't create a variant if the expected type is " (&type/show-type exo-type*))))))
-;; (defn analyse-variant [analyse exo-type ident ?values]
-;; (|do [exo-type* (|case exo-type
-;; (&/$VarT ?id)
-;; (&/try-all% (&/|list (|do [exo-type* (&type/deref ?id)]
-;; (&type/actual-type exo-type*))
-;; (|do [_ (&type/set-var ?id &type/Type)]
-;; (&type/actual-type &type/Type))))
-
-;; _
-;; (&type/actual-type exo-type))]
-;; (|case exo-type*
-;; (&/$VariantT ?cases)
-;; (|do [?tag (&&/resolved-ident ident)]
-;; (if-let [vtype (&/|get ?tag ?cases)]
-;; (|do [=value (analyse-variant-body analyse vtype ?values)]
-;; (return (&/|list (&/T (&/V &&/$variant (&/T ?tag =value))
-;; exo-type))))
-;; (fail (str "[Analyser Error] There is no case " ?tag " for variant type " (&type/show-type exo-type*)))))
-
-;; (&/$AllT _)
-;; (&type/with-var
-;; (fn [$var]
-;; (|do [exo-type** (&type/apply-type exo-type* $var)]
-;; (analyse-variant analyse exo-type** ident ?values))))
-
-;; _
-;; (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*))
- (&/$AllT _)
+ (&/$UnivQ _)
(|do [$var &type/existential
=type (&type/apply-type exo-type $var)]
(&type/actual-type =type))
@@ -148,7 +127,7 @@
(return ?table)
_
- (fail (str "[Analyser Error] The type of a record must be a record-type:\n" (&type/show-type exo-type*))))
+ (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)
@@ -221,13 +200,13 @@
(&/$Cons top-outer _)
(do ;; (prn 'analyse-symbol/_3 ?module name)
- (|let [scopes (&/|tail (&/folds #(&/|cons (&/get$ &/$name %2) %1)
+ (|let [scopes (&/|tail (&/folds #(&/Cons$ (&/get$ &/$name %2) %1)
(&/|map #(&/get$ &/$name %) outer)
(&/|reverse inner)))
[=local inner*] (&/fold2 (fn [register+new-inner frame in-scope]
(|let [[register new-inner] register+new-inner
[register* frame*] (&&lambda/close-over (&/|reverse in-scope) name register frame)]
- (&/T register* (&/|cons frame* new-inner))))
+ (&/T register* (&/Cons$ frame* new-inner))))
(&/T (or (->> top-outer (&/get$ &/$locals) (&/get$ &/$mappings) (&/|get name))
(->> top-outer (&/get$ &/$closure) (&/get$ &/$mappings) (&/|get name)))
(&/|list))
@@ -255,7 +234,7 @@
(&/$Cons ?arg ?args*)
(|do [?fun-type* (&type/actual-type fun-type)]
(|case ?fun-type*
- (&/$AllT _aenv _aname _aarg _abody)
+ (&/$UnivQ _)
;; (|do [$var &type/existential
;; type* (&type/apply-type ?fun-type* $var)]
;; (analyse-apply* analyse exo-type type* ?args))
@@ -268,7 +247,7 @@
(|do [? (&type/bound? ?id)
type** (if ?
(&type/clean $var =output-t)
- (|do [_ (&type/set-var ?id (&/V &/$BoundT _aarg))]
+ (|do [_ (&type/set-var ?id (&/V &/$BoundT 1))]
(&type/clean $var =output-t)))]
(return (&/T type** =args)))
))))
@@ -276,7 +255,7 @@
(&/$LambdaT ?input-t ?output-t)
(|do [[=output-t =args] (analyse-apply* analyse exo-type ?output-t ?args*)
=arg (&&/analyse-1 analyse ?input-t ?arg)]
- (return (&/T =output-t (&/|cons =arg =args))))
+ (return (&/T =output-t (&/Cons$ =arg =args))))
;; [[&/$VarT ?id-t]]
;; (|do [ (&type/deref ?id-t)])
@@ -332,7 +311,7 @@
(defn analyse-lambda* [analyse exo-type ?self ?arg ?body]
(|do [exo-type* (&type/actual-type exo-type)]
(|case exo-type
- (&/$AllT _)
+ (&/$UnivQ _)
(&type/with-var
(fn [$var]
(|do [exo-type** (&type/apply-type exo-type* $var)]
@@ -353,7 +332,7 @@
(defn analyse-lambda** [analyse exo-type ?self ?arg ?body]
(|case exo-type
- (&/$AllT _env _self _arg _body)
+ (&/$UnivQ _)
(&type/with-var
(fn [$var]
(|do [exo-type* (&type/apply-type exo-type $var)
@@ -376,12 +355,12 @@
(|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 ":" _arg " " (&type/show-type dtype)))
+ (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 ":" _arg " " (&type/show-type dtype)))))
+ (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))))))))
_
@@ -395,8 +374,8 @@
(defn analyse-def [analyse compile-token ?name ?value]
;; (prn 'analyse-def/BEGIN ?name)
- ;; (when (= "PList/Dict" ?name)
- ;; (prn 'DEF ?name (&/show-ast ?value)))
+ ;; (when (= "monoid$" ?name)
+ ;; (reset! &type/!flag true))
(|do [module-name &/get-module-name
;; :let [_ (println 'DEF/PRE (str module-name ";" ?name))]
? (&&module/defined? module-name ?name)]
diff --git a/src/lux/analyser/module.clj b/src/lux/analyser/module.clj
index 77630bafe..6eca13b44 100644
--- a/src/lux/analyser/module.clj
+++ b/src/lux/analyser/module.clj
@@ -41,7 +41,7 @@
(return* (&/update$ &/$modules
(fn [ms]
(&/|update current-module
- (fn [m] (&/update$ $imports (partial &/|cons module) m))
+ (fn [m] (&/update$ $imports (partial &/Cons$ module) m))
ms))
state)
nil))))
diff --git a/src/lux/base.clj b/src/lux/base.clj
index 44459beb4..5444c6c81 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -54,7 +54,7 @@
"BoundT"
"VarT"
"ExT"
- "AllT"
+ "UnivQ"
"AppT"
"NamedT")
@@ -285,9 +285,6 @@
(reverse (partition 2 steps))))
;; [Resources/Combinators]
-(defn |cons [head tail]
- (V $Cons (T head tail)))
-
(defn |++ [xs ys]
(|case xs
($Nil)
@@ -348,7 +345,7 @@
($Cons x xs*)
(if (p x)
(|let [[pre post] (|split-with p xs*)]
- (T (|cons x pre) post))
+ (T (Cons$ x pre) post))
(T (V $Nil nil) xs))))
(defn |contains? [k table]
@@ -383,7 +380,7 @@
(|list init)
($Cons x xs*)
- (|cons init (folds f (f init x) xs*))))
+ (Cons$ init (folds f (f init x) xs*))))
(defn |length [xs]
(fold (fn [acc _] (inc acc)) 0 xs))
@@ -417,7 +414,7 @@
(|list)
($Cons [k v] plist*)
- (|cons k (|keys plist*))))
+ (Cons$ k (|keys plist*))))
(defn |vals [plist]
(|case plist
@@ -425,7 +422,7 @@
(|list)
($Cons [k v] plist*)
- (|cons v (|vals plist*))))
+ (Cons$ v (|vals plist*))))
(defn |interpose [sep xs]
(|case xs
@@ -449,7 +446,7 @@
ys (<name> f xs*)]
(return (<joiner> y ys)))))
- map% |cons
+ map% Cons$
flat-map% |++)
(defn list-join [xss]
@@ -465,7 +462,7 @@
(defn |reverse [xs]
(fold (fn [tail head]
- (|cons head tail))
+ (Cons$ head tail))
(|list)
xs))
@@ -501,7 +498,7 @@
(defn repeat% [monad]
(try-all% (|list (|do [head monad
tail (repeat% monad)]
- (return (|cons head tail)))
+ (return (Cons$ head tail)))
(return (|list)))))
(defn exhaust% [step]
@@ -677,11 +674,11 @@
(defn ->list [seq]
(if (empty? seq)
(|list)
- (|cons (first seq) (->list (rest seq)))))
+ (Cons$ (first seq) (->list (rest seq)))))
(defn |repeat [n x]
(if (> n 0)
- (|cons x (|repeat (dec n) x))
+ (Cons$ x (|repeat (dec n) x))
(|list)))
(def get-module-name
@@ -707,7 +704,7 @@
(defn with-scope [name body]
(fn [state]
- (let [output (body (update$ $envs #(|cons (env name) %) state))]
+ (let [output (body (update$ $envs #(Cons$ (env name) %) state))]
(|case output
($Right state* datum)
(return* (update$ $envs |tail state*) datum)
@@ -723,7 +720,7 @@
(return (->> top (get$ $inner-closures) str)))]
(fn [state]
(let [body* (with-scope closure-name body)]
- (run-state body* (update$ $envs #(|cons (update$ $inner-closures inc (|head %))
+ (run-state body* (update$ $envs #(Cons$ (update$ $inner-closures inc (|head %))
(|tail %))
state))))))
@@ -789,10 +786,10 @@
($Meta _ ($TagS ?module ?tag))
(str "#" ?module ";" ?tag)
- ($Meta _ ($SymbolS ?module ?ident))
+ ($Meta _ ($SymbolS ?module ?name))
(if (.equals "" ?module)
- ?ident
- (str ?module ";" ?ident))
+ ?name
+ (str ?module ";" ?name))
($Meta _ ($TupleS ?elems))
(str "[" (->> ?elems (|map show-ast) (|interpose " ") (fold str "")) "]")
@@ -832,7 +829,7 @@
[($Cons x xs*) ($Cons y ys*)]
(|do [z (f x y)
zs (map2% f xs* ys*)]
- (return (|cons z zs)))
+ (return (Cons$ z zs)))
[($Nil) ($Nil)]
(return (V $Nil nil))
@@ -843,7 +840,7 @@
(defn map2 [f xs ys]
(|case [xs ys]
[($Cons x xs*) ($Cons y ys*)]
- (|cons (f x y) (map2 f xs* ys*))
+ (Cons$ (f x y) (map2 f xs* ys*))
[_ _]
(V $Nil nil)))
diff --git a/src/lux/compiler/type.clj b/src/lux/compiler/type.clj
index 54a7c5e0c..0d0300844 100644
--- a/src/lux/compiler/type.clj
+++ b/src/lux/compiler/type.clj
@@ -21,6 +21,11 @@
(&/T (&/V &a/$tuple members)
&type/$Void))
+(defn ^:private int$ [value]
+ "(-> Int Analysis)"
+ (&/T (&/V &a/$int value)
+ &type/$Void))
+
(defn ^:private text$ [text]
"(-> Text Analysis)"
(&/T (&/V &a/$text text)
@@ -58,20 +63,16 @@
(&/$LambdaT ?input ?output)
(variant$ &/$LambdaT (tuple$ (&/|list (->analysis ?input) (->analysis ?output))))
- (&/$AllT ?env ?name ?arg ?body)
- (variant$ &/$AllT
+ (&/$UnivQ ?env ?body)
+ (variant$ &/$UnivQ
(tuple$ (&/|list (&/fold (fn [tail head]
- (|let [[hlabel htype] head]
- (Cons$ (tuple$ (&/|list (text$ hlabel) (->analysis htype)))
- tail)))
+ (Cons$ (->analysis head) tail))
$Nil
(&/|reverse ?env))
- (text$ ?name)
- (text$ ?arg)
(->analysis ?body))))
- (&/$BoundT ?name)
- (variant$ &/$BoundT (text$ ?name))
+ (&/$BoundT ?idx)
+ (variant$ &/$BoundT (int$ ?idx))
(&/$AppT ?fun ?arg)
(variant$ &/$AppT (tuple$ (&/|list (->analysis ?fun) (->analysis ?arg))))
diff --git a/src/lux/reader.clj b/src/lux/reader.clj
index aa845c09d..0fcb5097b 100644
--- a/src/lux/reader.clj
+++ b/src/lux/reader.clj
@@ -33,7 +33,7 @@
output)
($Yes output line*)
- (return* (&/set$ &/$source (&/|cons line* more) state)
+ (return* (&/set$ &/$source (&/Cons$ line* more) state)
output))
)))
@@ -117,7 +117,7 @@
column-num* (+ column-num match-length)]
(if (= column-num* (.length line))
(recur (str prefix match "\n") reader**)
- (&/V &/$Right (&/T (&/|cons (&/T (&/T file-name line-num column-num*) line)
+ (&/V &/$Right (&/T (&/Cons$ (&/T (&/T file-name line-num column-num*) line)
reader**)
(&/T (&/T file-name line-num column-num) (str prefix match))))))
(&/V &/$Left (str "[Reader Error] Pattern failed: " regex))))))))
diff --git a/src/lux/type.clj b/src/lux/type.clj
index bcef74475..2b06553c3 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -40,8 +40,8 @@
(defn Variant$ [members]
;; (assert (|list? members))
(&/V &/$VariantT members))
-(defn All$ [env name arg body]
- (&/V &/$AllT (&/T env name arg body)))
+(defn Univ$ [env body]
+ (&/V &/$UnivQ (&/T env body)))
(defn Named$ [name type]
(&/V &/$NamedT (&/T name type)))
@@ -57,91 +57,90 @@
(def IO
(Named$ (&/T "lux/data" "IO")
- (All$ empty-env "IO" "a"
- (Lambda$ Unit (Bound$ "a")))))
+ (Univ$ empty-env
+ (Lambda$ Unit (Bound$ 1)))))
(def List
(Named$ (&/T "lux" "List")
- (All$ empty-env "lux;List" "a"
- (Variant$ (&/|list
- ;; lux;Nil
- Unit
- ;; lux;Cons
- (Tuple$ (&/|list (Bound$ "a")
- (App$ (Bound$ "lux;List")
- (Bound$ "a"))))
- )))))
+ (Univ$ empty-env
+ (Variant$ (&/|list
+ ;; lux;Nil
+ Unit
+ ;; lux;Cons
+ (Tuple$ (&/|list (Bound$ 1)
+ (App$ (Bound$ 0)
+ (Bound$ 1))))
+ )))))
(def Maybe
(Named$ (&/T "lux" "Maybe")
- (All$ empty-env "lux;Maybe" "a"
- (Variant$ (&/|list
- ;; lux;None
- Unit
- ;; lux;Some
- (Bound$ "a")
- )))))
+ (Univ$ empty-env
+ (Variant$ (&/|list
+ ;; lux;None
+ Unit
+ ;; lux;Some
+ (Bound$ 1)
+ )))))
(def Type
(Named$ (&/T "lux" "Type")
- (let [Type (App$ (Bound$ "Type") (Bound$ "_"))
+ (let [Type (App$ (Bound$ 0) (Bound$ 1))
TypeList (App$ List Type)
- TypeEnv (App$ List (Tuple$ (&/|list Text Type)))
TypePair (Tuple$ (&/|list Type Type))]
- (App$ (All$ empty-env "Type" "_"
- (Variant$ (&/|list
- ;; DataT
- Text
- ;; VariantT
- TypeList
- ;; TupleT
- TypeList
- ;; LambdaT
- TypePair
- ;; BoundT
- Text
- ;; VarT
- Int
- ;; ExT
- Int
- ;; AllT
- (Tuple$ (&/|list TypeEnv Text Text Type))
- ;; AppT
- TypePair
- ;; NamedT
- (Tuple$ (&/|list Ident Type))
- )))
+ (App$ (Univ$ empty-env
+ (Variant$ (&/|list
+ ;; DataT
+ Text
+ ;; VariantT
+ TypeList
+ ;; TupleT
+ TypeList
+ ;; LambdaT
+ TypePair
+ ;; BoundT
+ Int
+ ;; VarT
+ Int
+ ;; ExT
+ Int
+ ;; UnivQ
+ (Tuple$ (&/|list TypeList Type))
+ ;; AppT
+ TypePair
+ ;; NamedT
+ (Tuple$ (&/|list Ident Type))
+ )))
$Void))))
(def Bindings
(Named$ (&/T "lux" "Bindings")
- (All$ empty-env "lux;Bindings" "k"
- (All$ empty-env "" "v"
- (Tuple$ (&/|list
- ;; "lux;counter"
- Int
- ;; "lux;mappings"
- (App$ List
- (Tuple$ (&/|list (Bound$ "k")
- (Bound$ "v"))))))))))
+ (Univ$ empty-env
+ (Univ$ empty-env
+ (Tuple$ (&/|list
+ ;; "lux;counter"
+ Int
+ ;; "lux;mappings"
+ (App$ List
+ (Tuple$ (&/|list (Bound$ 3)
+ (Bound$ 1))))))))))
(def Env
(Named$ (&/T "lux" "Env")
- (let [bindings (App$ (App$ Bindings (Bound$ "k"))
- (Bound$ "v"))]
- (All$ empty-env "lux;Env" "k"
- (All$ empty-env "" "v"
- (Tuple$
- (&/|list
- ;; "lux;name"
- Text
- ;; "lux;inner-closures"
- Int
- ;; "lux;locals"
- bindings
- ;; "lux;closure"
- bindings
- )))))))
+ (let [bindings (App$ (App$ Bindings (Bound$ 3))
+ (Bound$ 1))]
+ (Univ$ empty-env
+ (Univ$ empty-env
+ (Tuple$
+ (&/|list
+ ;; "lux;name"
+ Text
+ ;; "lux;inner-closures"
+ Int
+ ;; "lux;locals"
+ bindings
+ ;; "lux;closure"
+ bindings
+ )))))))
(def Cursor
(Named$ (&/T "lux" "Cursor")
@@ -149,42 +148,42 @@
(def Meta
(Named$ (&/T "lux" "Meta")
- (All$ empty-env "lux;Meta" "m"
- (All$ empty-env "" "v"
- (Variant$ (&/|list
- ;; &/$Meta
- (Tuple$ (&/|list (Bound$ "m")
- (Bound$ "v")))))))))
+ (Univ$ empty-env
+ (Univ$ empty-env
+ (Variant$ (&/|list
+ ;; &/$Meta
+ (Tuple$ (&/|list (Bound$ 3)
+ (Bound$ 1)))))))))
(def AST*
(Named$ (&/T "lux" "AST'")
- (let [AST* (App$ (Bound$ "w")
- (App$ (Bound$ "lux;AST'")
- (Bound$ "w")))
+ (let [AST* (App$ (Bound$ 1)
+ (App$ (Bound$ 0)
+ (Bound$ 1)))
AST*List (App$ List AST*)]
- (All$ empty-env "lux;AST'" "w"
- (Variant$ (&/|list
- ;; &/$BoolS
- Bool
- ;; &/$IntS
- Int
- ;; &/$RealS
- Real
- ;; &/$CharS
- Char
- ;; &/$TextS
- Text
- ;; &/$SymbolS
- Ident
- ;; &/$TagS
- Ident
- ;; &/$FormS
- AST*List
- ;; &/$TupleS
- AST*List
- ;; &/$RecordS
- (App$ List (Tuple$ (&/|list AST* AST*))))
- )))))
+ (Univ$ empty-env
+ (Variant$ (&/|list
+ ;; &/$BoolS
+ Bool
+ ;; &/$IntS
+ Int
+ ;; &/$RealS
+ Real
+ ;; &/$CharS
+ Char
+ ;; &/$TextS
+ Text
+ ;; &/$SymbolS
+ Ident
+ ;; &/$TagS
+ Ident
+ ;; &/$FormS
+ AST*List
+ ;; &/$TupleS
+ AST*List
+ ;; &/$RecordS
+ (App$ List (Tuple$ (&/|list AST* AST*))))
+ )))))
(def AST
(Named$ (&/T "lux" "AST")
@@ -195,21 +194,21 @@
(def Either
(Named$ (&/T "lux" "Either")
- (All$ empty-env "lux;Either" "l"
- (All$ empty-env "" "r"
- (Variant$ (&/|list
- ;; &/$Left
- (Bound$ "l")
- ;; &/$Right
- (Bound$ "r")))))))
+ (Univ$ empty-env
+ (Univ$ empty-env
+ (Variant$ (&/|list
+ ;; &/$Left
+ (Bound$ 3)
+ ;; &/$Right
+ (Bound$ 1)))))))
(def StateE
- (All$ empty-env "lux;StateE" "s"
- (All$ empty-env "" "a"
- (Lambda$ (Bound$ "s")
- (App$ (App$ Either Text)
- (Tuple$ (&/|list (Bound$ "s")
- (Bound$ "a"))))))))
+ (Univ$ empty-env
+ (Univ$ empty-env
+ (Lambda$ (Bound$ 3)
+ (App$ (App$ Either Text)
+ (Tuple$ (&/|list (Bound$ 3)
+ (Bound$ 1))))))))
(def Source
(Named$ (&/T "lux" "Source")
@@ -229,17 +228,17 @@
(Data$ "clojure.lang.Atom")))))
(def DefData*
- (All$ empty-env "lux;DefData'" ""
- (Variant$ (&/|list
- ;; "lux;ValueD"
- (Tuple$ (&/|list Type Unit))
- ;; "lux;TypeD"
- Type
- ;; "lux;MacroD"
- (Bound$ "")
- ;; "lux;AliasD"
- Ident
- ))))
+ (Univ$ empty-env
+ (Variant$ (&/|list
+ ;; "lux;ValueD"
+ (Tuple$ (&/|list Type Unit))
+ ;; "lux;TypeD"
+ Type
+ ;; "lux;MacroD"
+ (Bound$ 1)
+ ;; "lux;AliasD"
+ Ident
+ ))))
(def LuxVar
(Named$ (&/T "lux" "LuxVar")
@@ -250,63 +249,63 @@
Ident))))
(def $Module
- (All$ empty-env "lux;$Module" "Compiler"
- (Tuple$
- (&/|list
- ;; "lux;module-aliases"
- (App$ List (Tuple$ (&/|list Text Text)))
- ;; "lux;defs"
- (App$ List
- (Tuple$ (&/|list Text
- (Tuple$ (&/|list Bool
- (App$ DefData*
- (Lambda$ ASTList
- (App$ (App$ StateE (Bound$ "Compiler"))
- ASTList))))))))
- ;; "lux;imports"
- (App$ List Text)
- ;; "lux;tags"
- ;; (List (, Text (, Int (List Ident) Type)))
- (App$ List
- (Tuple$ (&/|list Text
- (Tuple$ (&/|list Int
- (App$ List Ident)
- Type)))))
- ;; "lux;types"
- ;; (List (, Text (, (List Ident) Type)))
- (App$ List
- (Tuple$ (&/|list Text
- (Tuple$ (&/|list (App$ List Ident)
- Type)))))
- ))))
+ (Univ$ empty-env
+ (Tuple$
+ (&/|list
+ ;; "lux;module-aliases"
+ (App$ List (Tuple$ (&/|list Text Text)))
+ ;; "lux;defs"
+ (App$ List
+ (Tuple$ (&/|list Text
+ (Tuple$ (&/|list Bool
+ (App$ DefData*
+ (Lambda$ ASTList
+ (App$ (App$ StateE (Bound$ 1))
+ ASTList))))))))
+ ;; "lux;imports"
+ (App$ List Text)
+ ;; "lux;tags"
+ ;; (List (, Text (, Int (List Ident) Type)))
+ (App$ List
+ (Tuple$ (&/|list Text
+ (Tuple$ (&/|list Int
+ (App$ List Ident)
+ Type)))))
+ ;; "lux;types"
+ ;; (List (, Text (, (List Ident) Type)))
+ (App$ List
+ (Tuple$ (&/|list Text
+ (Tuple$ (&/|list (App$ List Ident)
+ Type)))))
+ ))))
(def $Compiler
(Named$ (&/T "lux" "Compiler")
- (App$ (All$ empty-env "lux;Compiler" ""
- (Tuple$
- (&/|list
- ;; "lux;source"
- Source
- ;; "lux;cursor"
- Cursor
- ;; "lux;modules"
- (App$ List (Tuple$ (&/|list Text
- (App$ $Module (App$ (Bound$ "lux;Compiler") (Bound$ ""))))))
- ;; "lux;envs"
- (App$ List
- (App$ (App$ Env Text)
- (Tuple$ (&/|list LuxVar Type))))
- ;; "lux;types"
- (App$ (App$ Bindings Int) Type)
- ;; "lux;expected"
- Type
- ;; "lux;seed"
- Int
- ;; "lux;eval?"
- Bool
- ;; "lux;host"
- Host
- )))
+ (App$ (Univ$ empty-env
+ (Tuple$
+ (&/|list
+ ;; "lux;source"
+ Source
+ ;; "lux;cursor"
+ Cursor
+ ;; "lux;modules"
+ (App$ List (Tuple$ (&/|list Text
+ (App$ $Module (App$ (Bound$ 0) (Bound$ 1))))))
+ ;; "lux;envs"
+ (App$ List
+ (App$ (App$ Env Text)
+ (Tuple$ (&/|list LuxVar Type))))
+ ;; "lux;types"
+ (App$ (App$ Bindings Int) Type)
+ ;; "lux;expected"
+ Type
+ ;; "lux;seed"
+ Int
+ ;; "lux;eval?"
+ Bool
+ ;; "lux;host"
+ Host
+ )))
$Void)))
(def Macro
@@ -439,13 +438,10 @@
(|do [=members (&/map% (partial clean* ?tid) ?members)]
(return (Variant$ =members)))
- (&/$AllT ?env ?name ?arg ?body)
- (|do [=env (&/map% (fn [[k v]]
- (|do [=v (clean* ?tid v)]
- (return (&/T k =v))))
- ?env)
+ (&/$UnivQ ?env ?body)
+ (|do [=env (&/map% (partial clean* ?tid) ?env)
body* (clean* ?tid ?body)]
- (return (All$ =env ?name ?arg body*)))
+ (return (Univ$ =env body*)))
_
(return type)
@@ -463,7 +459,7 @@
(|case type
(&/$LambdaT ?in ?out)
(|let [[??out ?args] (unravel-fun ?out)]
- (&/T ??out (&/|cons ?in ?args)))
+ (&/T ??out (&/Cons$ ?in ?args)))
_
(&/T type (&/|list))))
@@ -505,26 +501,16 @@
(&/$ExT ?id)
(str "⟨" ?id "⟩")
- (&/$BoundT name)
- name
+ (&/$BoundT idx)
+ (str idx)
(&/$AppT _ _)
(|let [[?call-fun ?call-args] (unravel-app type)]
(str "(" (show-type ?call-fun) " " (->> ?call-args (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")"))
- (&/$AllT ?env ?name ?arg ?body)
- (if (= "" ?name)
- (let [[args body] (loop [args (list ?arg)
- body* ?body]
- (|case body*
- (&/$AllT ?env* ?name* ?arg* ?body*)
- (recur (cons ?arg* args) ?body*)
-
- _
- [args body*]))]
- (str "(All " ?name " [" (->> args reverse (interpose " ") (reduce str "")) "] " (show-type body) ")"))
- ?name)
-
+ (&/$UnivQ ?env ?body)
+ (str "(All " (show-type ?body) ")")
+
(&/$NamedT ?name ?type)
(&/ident->text ?name)
@@ -554,8 +540,8 @@
[(&/$VarT xid) (&/$VarT yid)]
(.equals ^Object xid yid)
- [(&/$BoundT xname) (&/$BoundT yname)]
- (.equals ^Object xname yname)
+ [(&/$BoundT xidx) (&/$BoundT yidx)]
+ (= xidx yidx)
[(&/$ExT xid) (&/$ExT yid)]
(.equals ^Object xid yid)
@@ -563,24 +549,8 @@
[(&/$AppT xlambda xparam) (&/$AppT ylambda yparam)]
(and (type= xlambda ylambda) (type= xparam yparam))
- [(&/$AllT xenv xname xarg xbody) (&/$AllT yenv yname yarg ybody)]
- (and (.equals ^Object xname yname)
- (.equals ^Object xarg yarg)
- ;; (matchv ::M/objects [xenv yenv]
- ;; [[&/$None _] [&/$None _]]
- ;; true
-
- ;; [[&/$Some xenv*] [&/$Some yenv*]]
- ;; (&/fold (fn [old bname]
- ;; (and old
- ;; (type= (&/|get bname xenv*) (&/|get bname yenv*))))
- ;; (= (&/|length xenv*) (&/|length yenv*))
- ;; (&/|keys xenv*))
-
- ;; [_ _]
- ;; false)
- (type= xbody ybody)
- )
+ [(&/$UnivQ xenv xbody) (&/$UnivQ yenv ybody)]
+ (type= xbody ybody)
[(&/$NamedT ?xname ?xtype) _]
(type= ?xtype y)
@@ -607,14 +577,18 @@
)))
(defn ^:private fp-put [k v fixpoints]
- (&/|cons (&/T k v) fixpoints))
+ (&/Cons$ (&/T k v) fixpoints))
(defn ^:private check-error [expected actual]
(str "[Type Checker]\nExpected: " (show-type expected)
"\n\nActual: " (show-type actual)
"\n"))
+;; (def !flag (atom false))
+
(defn beta-reduce [env type]
+ ;; (when @!flag
+ ;; (prn 'beta-reduce (show-type type)))
(|case type
(&/$VariantT ?members)
(Variant$ (&/|map (partial beta-reduce env) ?members))
@@ -625,10 +599,10 @@
(&/$AppT ?type-fn ?type-arg)
(App$ (beta-reduce env ?type-fn) (beta-reduce env ?type-arg))
- (&/$AllT ?local-env ?local-name ?local-arg ?local-def)
+ (&/$UnivQ ?local-env ?local-def)
(|case ?local-env
(&/$Nil)
- (All$ env ?local-name ?local-arg ?local-def)
+ (Univ$ env ?local-def)
_
type)
@@ -636,21 +610,26 @@
(&/$LambdaT ?input ?output)
(Lambda$ (beta-reduce env ?input) (beta-reduce env ?output))
- (&/$BoundT ?name)
- (if-let [bound (&/|get ?name env)]
+ (&/$BoundT ?idx)
+ (|case (&/|at ?idx env)
+ (&/$Some bound)
(beta-reduce env bound)
- type)
+
+ _
+ (assert false (str "[Type Error] Unknown var: " ?idx " | " (&/->seq (&/|map show-type env)))))
_
type
))
(defn apply-type [type-fn param]
+ ;; (when @!flag
+ ;; (prn 'apply-type (show-type type-fn) (show-type param)))
(|case type-fn
- (&/$AllT local-env local-name local-arg local-def)
+ (&/$UnivQ local-env local-def)
(return (beta-reduce (->> local-env
- (&/|put local-name type-fn)
- (&/|put local-arg param))
+ (&/Cons$ param)
+ (&/Cons$ type-fn))
local-def))
(&/$AppT F A)
@@ -839,13 +818,13 @@
(|do [actual* (apply-type F A)]
(check* class-loader fixpoints expected actual*))
- [(&/$AllT _) _]
+ [(&/$UnivQ _) _]
(with-var
(fn [$arg]
(|do [expected* (apply-type expected $arg)]
(check* class-loader fixpoints expected* actual))))
- [_ (&/$AllT _)]
+ [_ (&/$UnivQ _)]
(with-var
(fn [$arg]
(|do [actual* (apply-type actual $arg)]
@@ -910,7 +889,7 @@
(|do [_ (check* init-fixpoints input param)]
(return output))
- (&/$AllT _)
+ (&/$UnivQ _)
(with-var
(fn [$var]
(|do [func* (apply-type func $var)