- Switched from TupleT to ProdT (type-wise).

9 files changed, 183 insertions, 103 deletions

diff --git a/src/lux/analyser/base.clj b/src/lux/analyser/base.clj
index 2d6d72fb8..bbbe18a89 100644
--- a/src/lux/analyser/base.clj
+++ b/src/lux/analyser/base.clj
@@ -185,7 +185,7 @@
                   (return ?module))]
     (return (&/T module* ?name))))
 
-(let [tag-names #{"DataT" "VoidT" "UnitT" "SumT" "TupleT" "LambdaT" "BoundT" "VarT" "ExT" "UnivQ" "ExQ" "AppT" "NamedT"}]
+(let [tag-names #{"DataT" "VoidT" "UnitT" "SumT" "ProdT" "LambdaT" "BoundT" "VarT" "ExT" "UnivQ" "ExQ" "AppT" "NamedT"}]
   (defn type-tag? [module name]
     (and (= "lux" module)
          (contains? tag-names name))))
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj
index 3b6dceb27..d71782914 100644
--- a/src/lux/analyser/case.clj
+++ b/src/lux/analyser/case.clj
@@ -74,20 +74,20 @@
           =type (&type/apply-type type $var)]
       (adjust-type* up =type))
 
-    (&/$TupleT ?members)
-    (|do [(&/$TupleT ?members*) (&/fold% (fn [_abody ena]
-                                           (|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 _aidx _avar] ena]
-                                                  (&/V &/$UnivQ (&/T _aenv _abody))))
-                                              v
-                                              up))
-                                    ?members*))))
+    (&/$ProdT ?left ?right)
+    (|do [(&/$ProdT =left =right) (&/fold% (fn [_abody ena]
+                                             (|let [[_aenv _aidx (&/$VarT _avar)] ena]
+                                               (|do [_ (&type/set-var _avar (&/V &/$BoundT _aidx))]
+                                                 (&type/clean* _avar _abody))))
+                                           type
+                                           up)
+          :let [distributor (fn [v]
+                              (&/fold (fn [_abody ena]
+                                        (|let [[_aenv _aidx _avar] ena]
+                                          (&/V &/$UnivQ (&/T _aenv _abody))))
+                                      v
+                                      up))]]
+      (return (&type/Prod$ (distributor =left) (distributor =right))))
 
     (&/$SumT ?left ?right)
     (|do [(&/$SumT =left =right) (&/fold% (fn [_abody ena]
@@ -178,19 +178,25 @@
               =kont kont]
           (return (&/T (&/V $TupleTestAC (&/|list)) =kont)))
 
+        (&/$Cons ?member (&/$Nil))
+        (analyse-pattern var?? value-type ?member kont)
+
         _
         (|do [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 tuple[" (&/|length ?member-types) "]. Given tuple [" (&/|length ?members) "]" " -- " (&/show-ast pattern)))
+            (&/$ProdT _)
+            (|case (&type/tuple-types-for (&/|length ?members) value-type*)
+              (&/$None)
+              (fail (str "[Pattern-matching Error] Pattern-matching mismatch. Require tuple[" (&/|length (&type/flatten-prod value-type*)) "]. Given tuple [" (&/|length ?members) "]" " -- " (&/show-ast pattern)))
+
+              (&/$Some ?member-types*)
               (|do [[=tests =kont] (&/fold (fn [kont* vm]
                                              (|let [[v m] vm]
                                                (|do [[=test [=tests =kont]] (analyse-pattern &/None$ v m kont*)]
                                                  (return (&/T (&/Cons$ =test =tests) =kont)))))
                                            (|do [=kont kont]
                                              (return (&/T &/Nil$ =kont)))
-                                           (&/|reverse (&/zip2 ?member-types ?members)))]
+                                           (&/|reverse (&/zip2 ?member-types* ?members)))]
                 (return (&/T (&/V $TupleTestAC =tests) =kont))))
 
             _
@@ -382,18 +388,26 @@
       (|do [unknown? (&type/unknown? value-type)]
         (if unknown?
           (|do [=structs (&/map% (check-totality+ check-totality) ?structs)
-                _ (&type/check value-type (&/V &/$TupleT (&/|map &/|second =structs)))]
+                _ (&type/check value-type (|case (->> (&/|map &/|second =structs) (&/|reverse))
+                                            (&/$Cons last prevs)
+                                            (&/fold (fn [right left] (&type/Prod$ left right))
+                                                    last prevs)))]
             (return (or ?total
                         (&/fold #(and %1 %2) true (&/|map &/|first =structs)))))
           (if ?total
             (return true)
             (|do [value-type* (resolve-type value-type)]
               (|case value-type*
-                (&/$TupleT ?members)
-                (|do [totals (&/map2% (fn [sub-struct ?member]
-                                        (check-totality ?member sub-struct))
-                                      ?structs ?members)]
-                  (return (&/fold #(and %1 %2) true totals)))
+                (&/$ProdT _)
+                (|case (&type/tuple-types-for (&/|length ?structs) value-type*)
+                  (&/$None)
+                  (fail (str "[Pattern-maching Error] Tuple-mismatch. Require tuple[" (&/|length (&type/flatten-prod value-type*)) "]. Given tuple [" (&/|length ?structs) "]"))
+
+                  (&/$Some ?member-types*)
+                  (|do [totals (&/map2% check-totality
+                                        ?member-types*
+                                        ?structs)]
+                    (return (&/fold #(and %1 %2) true totals))))
 
                 _
                 (fail "[Pattern-maching Error] Tuple is not total.")))))))
@@ -404,8 +418,9 @@
       (|do [value-type* (resolve-type value-type)]
         (|case value-type*
           (&/$SumT _)
-          (|do [:let [?members (&type/flatten-sum value-type*)]
-                totals (&/map2% check-totality ?members ?structs)]
+          (|do [totals (&/map2% check-totality
+                                (&type/flatten-sum value-type*)
+                                ?structs)]
             (return (&/fold #(and %1 %2) true totals)))
 
           _
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index 415565c7c..3777e8053 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -56,6 +56,12 @@
                             (&/$Left exo-type) exo-type
                             (&/$Right exo-type) exo-type))
 
+    (&/$Cons ?elem (&/$Nil))
+    (analyse (|case ?exo-type
+               (&/$Left exo-type) exo-type
+               (&/$Right exo-type) exo-type)
+             ?elem)
+
     _
     (|case ?exo-type
       (&/$Left exo-type)
@@ -88,7 +94,10 @@
           (|do [=elems (&/map% #(|do [=analysis (&&/analyse-1+ analyse %)]
                                   (return =analysis))
                                ?elems)
-                _ (&type/check exo-type (&/V &/$TupleT (&/|map &&/expr-type* =elems)))
+                _ (&type/check exo-type (|case (->> (&/|map &&/expr-type* =elems) (&/|reverse))
+                                          (&/$Cons last prevs)
+                                          (&/fold (fn [right left] (&type/Prod$ left right))
+                                                  last prevs)))
                 _cursor &/cursor]
             (return (&/|list (&&/|meta exo-type _cursor
                                        (&/V &&/$tuple =elems)
@@ -96,14 +105,20 @@
           (|do [exo-type* (&type/actual-type exo-type)]
             (&/with-attempt
               (|case exo-type*
-                (&/$TupleT ?members)
-                (|do [=elems (&/map2% (fn [elem-t elem]
-                                        (&&/analyse-1 analyse elem-t elem))
-                                      ?members ?elems)
-                      _cursor &/cursor]
-                  (return (&/|list (&&/|meta exo-type _cursor
-                                             (&/V &&/$tuple =elems)
-                                             ))))
+                (&/$ProdT _)
+                (|case (&type/tuple-types-for (&/|length ?elems) exo-type*)
+                  (&/$None)
+                  (fail (str "[Analysis Error] Tuple-mismatch. Require tuple[" (&/|length (&type/flatten-prod exo-type*)) "]. Given tuple [" (&/|length ?elems) "]" " -- " (str "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]")))
+
+                  (&/$Some ?member-types*)
+                  (|do [=elems (&/map2% (fn [elem-t elem]
+                                          (&&/analyse-1 analyse elem-t elem))
+                                        ?member-types*
+                                        ?elems)
+                        _cursor &/cursor]
+                    (return (&/|list (&&/|meta exo-type _cursor
+                                               (&/V &&/$tuple =elems)
+                                               )))))
 
                 (&/$UnivQ _)
                 (|do [$var &type/existential
@@ -356,7 +371,15 @@
       (|do [[real-name [?type ?meta ?value]] (&&module/find-def ?module ?name)]
         (|case (&&meta/meta-get &&meta/macro?-tag ?meta)
           (&/$Some _)
-          (|do [macro-expansion (fn [state] (-> ?value (.apply ?args) (.apply state)))]
+          (|do [macro-expansion (fn [state] (-> ?value (.apply ?args) (.apply state)))
+                ;; :let [_ (when (or (= "using" (aget real-name 1))
+                ;;                   ;; (= "defsig" (aget real-name 1))
+                ;;                   )
+                ;;           (->> (&/|map &/show-ast macro-expansion)
+                ;;                (&/|interpose "\n")
+                ;;                (&/fold str "")
+                ;;                (prn (&/ident->text real-name))))]
+                ]
             (&/flat-map% (partial analyse exo-type) macro-expansion))
 
           _
diff --git a/src/lux/base.clj b/src/lux/base.clj
index fe8ce184a..ba1489726 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -48,7 +48,7 @@
    "VoidT"
    "UnitT"
    "SumT"
-   "TupleT"
+   "ProdT"
    "LambdaT"
    "BoundT"
    "VarT"
@@ -1082,3 +1082,17 @@
 
         ($Left msg)
         (V $Left msg)))))
+
+(defn |take [n xs]
+  (|case (T n xs)
+    [0 _]             Nil$
+    [_ ($Nil)]        Nil$
+    [_ ($Cons x xs*)] (Cons$ x (|take (dec n) xs*))
+    ))
+
+(defn |drop [n xs]
+  (|case (T n xs)
+    [0 _]             xs
+    [_ ($Nil)]        Nil$
+    [_ ($Cons x xs*)] (|drop (dec n) xs*)
+    ))
diff --git a/src/lux/compiler/case.clj b/src/lux/compiler/case.clj
index e0d1b886e..1a4006312 100644
--- a/src/lux/compiler/case.clj
+++ b/src/lux/compiler/case.clj
@@ -86,10 +86,16 @@
         (.visitJumpInsn Opcodes/GOTO $target))
 
       (&a-case/$TupleTestAC ?members)
-      (if (&/|empty? ?members)
+      (|case ?members
+        (&/$Nil)
         (doto writer
           (.visitInsn Opcodes/POP)
           (.visitJumpInsn Opcodes/GOTO $target))
+
+        (&/$Cons ?member (&/$Nil))
+        (compile-match ?member $target $else)
+
+        _
         (doto writer
           (.visitTypeInsn Opcodes/CHECKCAST "[Ljava/lang/Object;")
           (-> (doto (.visitInsn Opcodes/DUP)
diff --git a/src/lux/compiler/lux.clj b/src/lux/compiler/lux.clj
index edafc67e2..cbe9cb0f3 100644
--- a/src/lux/compiler/lux.clj
+++ b/src/lux/compiler/lux.clj
@@ -56,9 +56,15 @@
 (defn compile-tuple [compile ?elems]
   (|do [^MethodVisitor *writer* &/get-writer
         :let [num-elems (&/|length ?elems)]]
-    (if (= 0 num-elems)
+    (|case num-elems
+      0
       (|do [:let [_ (.visitInsn *writer* Opcodes/ACONST_NULL)]]
         (return nil))
+
+      1
+      (compile (&/|head ?elems))
+      
+      _
       (|do [:let [_ (doto *writer*
                       (.visitLdcInsn (int num-elems))
                       (.visitTypeInsn Opcodes/ANEWARRAY "java/lang/Object"))]
diff --git a/src/lux/compiler/type.clj b/src/lux/compiler/type.clj
index e053c8b3c..0abb4d42e 100644
--- a/src/lux/compiler/type.clj
+++ b/src/lux/compiler/type.clj
@@ -68,8 +68,8 @@
     (&/$UnitT)
     (variant$ &/$UnitT (tuple$ (&/|list)))
     
-    (&/$TupleT members)
-    (variant$ &/$TupleT (List$ (&/|map type->analysis members)))
+    (&/$ProdT left right)
+    (variant$ &/$ProdT (tuple$ (&/|list (type->analysis left) (type->analysis right))))
 
     (&/$SumT left right)
     (variant$ &/$SumT (tuple$ (&/|list (type->analysis left) (type->analysis right))))
diff --git a/src/lux/host.clj b/src/lux/host.clj
index c54da0799..473d0dc60 100644
--- a/src/lux/host.clj
+++ b/src/lux/host.clj
@@ -69,7 +69,7 @@
       (&/$SumT _)
       (return object-array)
 
-      (&/$TupleT _)
+      (&/$ProdT _)
       (return object-array)
 
       (&/$NamedT ?name ?type)
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 66ea59f6c..0655aa8b2 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -5,7 +5,8 @@
 
 (ns lux.type
   (:refer-clojure :exclude [deref apply merge bound?])
-  (:require clojure.core.match
+  (:require [clojure.template :refer [do-template]]
+            clojure.core.match
             clojure.core.match.array
             (lux [base :as & :refer [|do return* return fail fail* assert! |let |case]])
             [lux.type.host :as &&host]))
@@ -35,9 +36,8 @@
   (&/V &/$LambdaT (&/T in out)))
 (defn App$ [fun arg]
   (&/V &/$AppT (&/T fun arg)))
-(defn Tuple$ [members]
-  (assert (> (&/|length members) 0))
-  (&/V &/$TupleT members))
+(defn Prod$ [left right]
+  (&/V &/$ProdT (&/T left right)))
 (defn Sum$ [left right]
   (&/V &/$SumT (&/T left right)))
 (defn Univ$ [env body]
@@ -54,7 +54,7 @@
 (def Real (Named$ (&/T "lux" "Real") (Data$ "java.lang.Double" &/Nil$)))
 (def Char (Named$ (&/T "lux" "Char") (Data$ "java.lang.Character" &/Nil$)))
 (def Text (Named$ (&/T "lux" "Text") (Data$ "java.lang.String" &/Nil$)))
-(def Ident (Named$ (&/T "lux" "Ident") (Tuple$ (&/|list Text Text))))
+(def Ident (Named$ (&/T "lux" "Ident") (Prod$ Text Text)))
 
 (def IO
   (Named$ (&/T "lux/data" "IO")
@@ -68,9 +68,9 @@
                   ;; lux;Nil
                   Unit
                   ;; lux;Cons
-                  (Tuple$ (&/|list (Bound$ 1)
-                                   (App$ (Bound$ 0)
-                                         (Bound$ 1))))))))
+                  (Prod$ (Bound$ 1)
+                         (App$ (Bound$ 0)
+                               (Bound$ 1)))))))
 
 (def Maybe
   (Named$ (&/T "lux" "Maybe")
@@ -86,11 +86,11 @@
   (Named$ (&/T "lux" "Type")
           (let [Type (App$ (Bound$ 0) (Bound$ 1))
                 TypeList (App$ List Type)
-                TypePair (Tuple$ (&/|list Type Type))]
+                TypePair (Prod$ Type Type)]
             (App$ (Univ$ empty-env
                          (Sum$
                           ;; DataT
-                          (Tuple$ (&/|list Text TypeList))
+                          (Prod$ Text TypeList)
                           (Sum$
                            ;; VoidT
                            Unit
@@ -101,8 +101,8 @@
                              ;; SumT
                              TypePair
                              (Sum$
-                              ;; TupleT
-                              TypeList
+                              ;; ProdT
+                              TypePair
                               (Sum$
                                ;; LambdaT
                                TypePair
@@ -117,15 +117,15 @@
                                   Int
                                   (Sum$
                                    ;; UnivQ
-                                   (Tuple$ (&/|list TypeList Type))
+                                   (Prod$ TypeList Type)
                                    (Sum$
                                     ;; ExQ
-                                    (Tuple$ (&/|list TypeList Type))
+                                    (Prod$ TypeList Type)
                                     (Sum$
                                      ;; AppT
                                      TypePair
                                      ;; NamedT
-                                     (Tuple$ (&/|list Ident Type))))))))))))))
+                                     (Prod$ Ident Type)))))))))))))
                          )
                   $Void))))
 
@@ -155,13 +155,13 @@
                                 ;; ListM
                                 (App$ List DefMetaValue)
                                 ;; DictM
-                                (App$ List (Tuple$ (&/|list Text DefMetaValue))))))))))
+                                (App$ List (Prod$ Text DefMetaValue)))))))))
                          )
                   $Void))))
 
 (def DefMeta
   (Named$ (&/T "lux" "DefMeta")
-          (App$ List (Tuple$ (&/|list Ident DefMetaValue)))))
+          (App$ List (Prod$ Ident DefMetaValue))))
 
 (def Macro)
 
@@ -209,7 +209,7 @@
         
         (&/$None)
         (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id (&/V &/$Some type) %)
-                                                             ts))
+                                                            ts))
                             state)
                  nil))
       (fail* (str "[Type Error] <set-var> Unknown type-var: " id " | " (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) &/|length))))))
@@ -290,9 +290,10 @@
           =param (clean* ?tid ?param)]
       (return (App$ =lambda =param)))
 
-    (&/$TupleT ?members)
-    (|do [=members (&/map% (partial clean* ?tid) ?members)]
-      (return (Tuple$ =members)))
+    (&/$ProdT ?left ?right)
+    (|do [=left (clean* ?tid ?left)
+          =right (clean* ?tid ?right)]
+      (return (Prod$ =left =right)))
     
     (&/$SumT ?left ?right)
     (|do [=left (clean* ?tid ?left)
@@ -334,31 +335,36 @@
     _
     (&/T fun-type &/Nil$)))
 
-(defn flatten-sum [type]
-  "(-> Type (List Type))"
-  (|case type
-    (&/$SumT left right)
-    (&/Cons$ left (flatten-sum right))
+(do-template [<tag> <flatten> <at> <desc>]
+  (do (defn <flatten> [type]
+        "(-> Type (List Type))"
+        (|case type
+          (<tag> left right)
+          (&/Cons$ left (<flatten> right))
 
-    _
-    (&/|list type)))
+          _
+          (&/|list type)))
 
-(defn sum-at [tag type]
-  "(-> Int Type (Lux Type))"
-  (|case type
-    (&/$NamedT ?name ?type)
-    (sum-at tag ?type)
-    
-    (&/$SumT ?left ?right)
-    (|case (&/T tag ?right)
-      [0 _]                  (return ?left)
-      [1 (&/$SumT ?left* _)] (return ?left*)
-      [1 _]                  (return ?right)
-      [_ (&/$SumT _ _)]      (sum-at (dec tag) ?right)
-      _                      (fail (str "[Type Error] Variant lacks case: " tag " | " (show-type type))))
+    (defn <at> [tag type]
+      "(-> Int Type (Lux Type))"
+      (|case type
+        (&/$NamedT ?name ?type)
+        (<at> tag ?type)
+        
+        (<tag> ?left ?right)
+        (|case (&/T tag ?right)
+          [0 _]                (return ?left)
+          [1 (<tag> ?left* _)] (return ?left*)
+          [1 _]                (return ?right)
+          [_ (<tag> _ _)]      (<at> (dec tag) ?right)
+          _                    (fail (str "[Type Error] " <desc> " lacks member: " tag " | " (show-type type))))
 
-    _
-    (fail (str "[Type Error] Type is not a variant: " (show-type type)))))
+        _
+        (fail (str "[Type Error] Type is not a " <desc> ": " (show-type type))))))
+
+  &/$SumT  flatten-sum  sum-at "Sum"
+  &/$ProdT flatten-prod prod-at "Product"
+  )
 
 (defn show-type [^objects type]
   (|case type
@@ -376,10 +382,8 @@
     (&/$UnitT)
     "Unit"
     
-    (&/$TupleT elems)
-    (if (&/|empty? elems)
-      "(,)"
-      (str "(, " (->> elems (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")"))
+    (&/$ProdT _)
+    (str "(, " (->> (flatten-prod type) (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")
 
     (&/$SumT _)
     (str "(|| " (->> (flatten-sum type) (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")
@@ -431,10 +435,9 @@
                      [(&/$UnitT) (&/$UnitT)]
                      true
 
-                     [(&/$TupleT xelems) (&/$TupleT yelems)]
-                     (&/fold2 (fn [old x y] (and old (type= x y)))
-                              true
-                              xelems yelems)
+                     [(&/$ProdT xL xR) (&/$ProdT yL yR)]
+                     (and (type= xL yL)
+                          (type= xR yR))
 
                      [(&/$SumT xL xR) (&/$SumT yL yR)]
                      (and (type= xL yL)
@@ -519,8 +522,10 @@
           =right (beta-reduce env ?right)]
       (Sum$ =left =right))
 
-    (&/$TupleT ?members)
-    (Tuple$ (&/|map (partial beta-reduce env) ?members))
+    (&/$ProdT ?left ?right)
+    (let [=left (beta-reduce env ?left)
+          =right (beta-reduce env ?right)]
+      (Prod$ =left =right))
 
     (&/$AppT ?type-fn ?type-arg)
     (App$ (beta-reduce env ?type-fn) (beta-reduce env ?type-arg))
@@ -745,13 +750,9 @@
         (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? aI eI)]
           (check* class-loader fixpoints* invariant?? eO aO))
 
-        [(&/$TupleT e!members) (&/$TupleT a!members)]
-        (|do [fixpoints* (&/fold2% (fn [fp e a]
-                                     (|do [[fp* _] (check* class-loader fp invariant?? e a)]
-                                       (return fp*)))
-                                   fixpoints
-                                   e!members a!members)]
-          (return (&/T fixpoints* nil)))
+        [(&/$ProdT eL eR) (&/$ProdT aL aR)]
+        (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? eL aL)]
+          (check* class-loader fixpoints* invariant?? eR aR))
 
         [(&/$SumT eL eR) (&/$SumT aL aR)]
         (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? eL aL)]
@@ -827,3 +828,18 @@
 
     _
     (return type)))
+
+(defn tuple-types-for [size-members type]
+  "(-> Int Type (Maybe (List Type)))"
+  (|let [?member-types (flatten-prod type)
+         size-types (&/|length ?member-types)]
+    (if (not (>= size-types size-members))
+      &/None$
+      (|let [?member-types* (if (= size-types size-members)
+                              ?member-types
+                              (&/|++ (&/|take (dec size-members) ?member-types)
+                                     (&/|list (|case (->> (&/|drop (dec size-members) ?member-types) (&/|reverse))
+                                                (&/$Cons last prevs)
+                                                (&/fold (fn [right left] (Prod$ left right))
+                                                        last prevs)))))]
+        (&/Some$ ?member-types*)))))