- WIP: Added pattern-matching (case) analysis.

10 files changed, 626 insertions, 92 deletions

diff --git a/new-luxc/source/luxc/analyser.lux b/new-luxc/source/luxc/analyser.lux
index eba8ae62a..d8f5abe9b 100644
--- a/new-luxc/source/luxc/analyser.lux
+++ b/new-luxc/source/luxc/analyser.lux
@@ -19,9 +19,23 @@
      ["&&;" reference]
      ["&&;" type]
      ["&&;" struct]
-     ## ["&&;" case]
+     ["&&;" case]
      ["&&;" proc]))
 
+(def: (to-branches raw)
+  (-> (List Code) (Lux (List [Code Code])))
+  (case raw
+    (^ (list))
+    (:: Monad<Lux> wrap (list))
+
+    (^ (list& patternH bodyH inputT))
+    (do Monad<Lux>
+      [outputT (to-branches inputT)]
+      (wrap (list& [patternH bodyH] outputT)))
+
+    _
+    (&;fail "Uneven expressions for pattern-matching.")))
+
 (def: #export (analyser eval)
   (-> &;Eval &;Analyser)
   (: (-> Code (Lux la;Analysis))
@@ -67,10 +81,12 @@
                               [_ (#;Tuple args)])))
              (&&proc;analyse-proc analyse proc args)
 
-             ## (^ (#;Form (list& [_ (#;Symbol ["" "_lux_case"])]
-             ##                   input
-             ##                   branches)))
-             ## (&&case;analyse-case analyse proc branches)
+             (^ (#;Form (list& [_ (#;Symbol ["" "_lux_case"])]
+                               input
+                               branches)))
+             (do Monad<Lux>
+               [paired (to-branches branches)]
+               (&&case;analyse-case analyse input paired))
 
              (^ (#;Form (list [_ (#;Nat tag)]
                               value)))
diff --git a/new-luxc/source/luxc/analyser/case.lux b/new-luxc/source/luxc/analyser/case.lux
new file mode 100644
index 000000000..fc151f771
--- /dev/null
+++ b/new-luxc/source/luxc/analyser/case.lux
@@ -0,0 +1,448 @@
+(;module:
+  lux
+  (lux (control monad
+                eq)
+       (data [bool "B/" Eq<Bool>]
+             [number]
+             [char]
+             [text]
+             text/format
+             [product]
+             ["R" result "R/" Monad<Result>]
+             (coll [list "L/" Fold<List> Monoid<List> Monad<List>]
+                   ["D" dict]))
+       [macro #+ Monad<Lux>]
+       (macro [code])
+       [type]
+       (type ["TC" check]))
+  (luxc ["&" base]
+        (lang ["la" analysis #+ Analysis]
+              ["lp" pattern #+ Pattern])
+        ["&;" env]
+        (analyser ["&;" common]
+                  ["&;" struct])))
+
+(type: #rec Coverage
+  #PartialC
+  (#BoolC Bool)
+  (#VariantC Nat (D;Dict Nat Coverage))
+  (#SeqC Coverage Coverage)
+  (#AltC Coverage Coverage)
+  #TotalC)
+
+(def: (pattern-error type pattern)
+  (-> Type Code Text)
+  (format "Cannot match this type: " (%type type) "\n"
+          "     With this pattern: " (%code pattern)))
+
+(def: (simplify-case-type type)
+  (-> Type (Lux Type))
+  (case type
+    (#;Var id)
+    (do Monad<Lux>
+      [? (&;within-type-env
+          (TC;bound? id))]
+      (if ?
+        (do @
+          [type' (&;within-type-env
+                  (TC;read-var id))]
+          (simplify-case-type type'))
+        (&;fail (format "Cannot simplify type for pattern-matching: " (%type type)))))
+
+    (#;Named name unnamedT)
+    (simplify-case-type unnamedT)
+
+    (^or (#;UnivQ _) (#;ExQ _))
+    (do Monad<Lux>
+      [[ex-id exT] (&;within-type-env
+                    TC;existential)]
+      (simplify-case-type (assume (type;apply-type type exT))))
+
+    _
+    (:: Monad<Lux> wrap type)))
+
+(def: (analyse-pattern num-tags inputT pattern next)
+  (All [a] (-> (Maybe Nat) Type Code (Lux a) (Lux [Pattern a])))
+  (case pattern
+    [cursor (#;Symbol ["" name])]
+    (&;with-cursor cursor
+      (do Monad<Lux>
+        [outputA (&env;with-local [name inputT]
+                   next)
+         idx &env;next-local]
+        (wrap [(#lp;Bind idx) outputA])))
+
+    [cursor (#;Symbol ident)]
+    (&;with-cursor cursor
+      (&;fail (format "Symbols must be unqualified inside patterns: " (%ident ident))))
+
+    (^template [<type> <code-tag> <pattern-tag>]
+      [cursor (<code-tag> test)]
+      (&;with-cursor cursor
+        (do Monad<Lux>
+          [_ (&;within-type-env
+              (TC;check inputT <type>))
+           outputA next]
+          (wrap [(<pattern-tag> test) outputA]))))
+    ([Bool #;Bool #lp;Bool]
+     [Nat  #;Nat  #lp;Nat]
+     [Int  #;Int  #lp;Int]
+     [Deg  #;Deg  #lp;Deg]
+     [Real #;Real #lp;Real]
+     [Char #;Char #lp;Char]
+     [Text #;Text #lp;Text])
+
+    (^ [cursor (#;Tuple (list))])
+    (&;with-cursor cursor
+      (do Monad<Lux>
+        [_ (&;within-type-env
+            (TC;check inputT Unit))
+         outputA next]
+        (wrap [#lp;Unit outputA])))
+
+    (^ [cursor (#;Tuple (list singleton))])
+    (analyse-pattern #;None inputT singleton next)
+    
+    [cursor (#;Tuple sub-patterns)]
+    (&;with-cursor cursor
+      (do Monad<Lux>
+        [inputT' (simplify-case-type inputT)]
+        (case inputT'
+          (#;Product _)
+          (let [sub-types (type;flatten-tuple inputT)
+                num-sub-types (default (list;size sub-types)
+                                num-tags)
+                num-sub-patterns (list;size sub-patterns)
+                matches (cond (n.< num-sub-types num-sub-patterns)
+                              (let [[prefix suffix] (list;split (n.dec num-sub-patterns) sub-types)]
+                                (list;zip2 (L/append prefix (list (type;tuple suffix))) sub-patterns))
+
+                              (n.> num-sub-types num-sub-patterns)
+                              (let [[prefix suffix] (list;split (n.dec num-sub-types) sub-patterns)]
+                                (list;zip2 sub-types (L/append prefix (list (code;tuple suffix)))))
+                              
+                              ## (n.= num-sub-types num-sub-patterns)
+                              (list;zip2 sub-types sub-patterns)
+                              )]
+            (do @
+              [[memberP+ thenA] (L/fold (: (All [a]
+                                             (-> [Type Code] (Lux [(List Pattern) a])
+                                                 (Lux [(List Pattern) a])))
+                                           (function [[memberT memberC] then]
+                                             (do @
+                                               [[memberP [memberP+ thenA]] ((:! (All [a] (-> (Maybe Nat) Type Code (Lux a) (Lux [Pattern a])))
+                                                                                analyse-pattern)
+                                                                            #;None memberT memberC then)]
+                                               (wrap [(list& memberP memberP+) thenA]))))
+                                        (do @
+                                          [nextA next]
+                                          (wrap [(list) nextA]))
+                                        matches)]
+              (wrap [(#lp;Tuple memberP+) thenA])))
+
+          _
+          (&;fail (pattern-error inputT pattern))
+          )))
+
+    [cursor (#;Record pairs)]
+    (do Monad<Lux>
+      [pairs (&struct;normalize-record pairs)
+       [members recordT] (&struct;order-record pairs)
+       _ (&;within-type-env
+          (TC;check inputT recordT))]
+      (analyse-pattern (#;Some (list;size members)) inputT [cursor (#;Tuple members)] next))
+
+    [cursor (#;Tag tag)]
+    (&;with-cursor cursor
+      (analyse-pattern #;None inputT (` ((~ pattern))) next))
+
+    (^ [cursor (#;Form (list& [_ (#;Nat idx)] values))])
+    (&;with-cursor cursor
+      (do Monad<Lux>
+        [inputT' (simplify-case-type inputT)]
+        (case inputT'
+          (#;Sum _)
+          (let [flat-sum (type;flatten-variant inputT)]
+            (case (list;nth idx flat-sum)
+              #;None
+              (&;fail (format "Cannot match index " (%n idx) " against type: " (%type inputT)))
+
+              (#;Some case-type)
+              (do Monad<Lux>
+                [[testP nextA] (analyse-pattern #;None case-type (' [(~@ values)]) next)]
+                (wrap [(#lp;Variant [idx (default (list;size flat-sum)
+                                           num-tags)]
+                                    testP)
+                       nextA]))))
+
+          _
+          (&;fail (pattern-error inputT pattern)))))
+
+    (^ [cursor (#;Form (list& [_ (#;Tag tag)] values))])
+    (&;with-cursor cursor
+      (do Monad<Lux>
+        [tag (macro;normalize tag)
+         [idx group tagT] (macro;resolve-tag tag)
+         _ (&;within-type-env
+            (TC;check inputT tagT))]
+        (analyse-pattern (#;Some (list;size group)) inputT (' ((~ (code;nat idx)) (~@ values))) next)))
+
+    _
+    (&;fail (format "Unrecognized pattern syntax: " (%code pattern)))
+    ))
+
+(def: (analyse-branch analyse inputT pattern body)
+  (-> &;Analyser Type Code Code (Lux [Pattern Analysis]))
+  (analyse-pattern #;None inputT pattern (analyse body)))
+
+(do-template [<name> <tag>]
+  [(def: (<name> coverage)
+     (-> Coverage Bool)
+     (case coverage
+       (<tag> _)
+       true
+
+       _
+       false))]
+
+  [total? #TotalC]
+  [alt?   #AltC])
+
+(def: (determine-coverage pattern)
+  (-> Pattern Coverage)
+  (case pattern
+    (^or (#lp;Bind _) #lp;Unit)
+    #TotalC
+    
+    (#lp;Bool value)
+    (#BoolC value)
+    
+    (^or (#lp;Nat _)  (#lp;Int _)  (#lp;Deg _)
+         (#lp;Real _) (#lp;Char _) (#lp;Text _))
+    #PartialC
+    
+    (#lp;Tuple subs)
+    (loop [subs subs]
+      (case subs
+        #;Nil
+        #TotalC
+
+        (#;Cons sub subs')
+        (let [post (recur subs')]
+          (if (total? post)
+            (determine-coverage sub)
+            (#SeqC (determine-coverage sub)
+                   post)))))
+    
+    (#lp;Variant [tag-id num-tags] sub)
+    (#VariantC num-tags
+               (|> (D;new number;Hash<Nat>)
+                   (D;put tag-id (determine-coverage sub))))))
+
+(def: (xor left right)
+  (-> Bool Bool Bool)
+  (or (and left (not right))
+      (and (not left) right)))
+
+(def: redundant-pattern
+  (R;Result Coverage)
+  (R;fail "Redundant pattern."))
+
+(def: (flatten-alt coverage)
+  (-> Coverage (List Coverage))
+  (case coverage
+    (#AltC left right)
+    (list& left (flatten-alt right))
+
+    _
+    (list coverage)))
+
+(struct: _ (Eq Coverage)
+  (def: (= reference sample)
+    (case [reference sample]
+      (^or [#TotalC #TotalC] [#PartialC #PartialC])
+      true
+
+      [(#BoolC sideR) (#BoolC sideS)]
+      (B/= sideR sideS)
+
+      [(#VariantC allR casesR) (#VariantC allS casesS)]
+      (and (n.= allR allS)
+           (:: (D;Eq<Dict> =) = casesR casesS))
+
+      [(#SeqC leftR rightR) (#SeqC leftS rightS)]
+      (and (= leftR leftS)
+           (= rightR rightS))
+
+      [(#AltC _) (#AltC _)]
+      (let [flatR (flatten-alt reference)
+            flatS (flatten-alt sample)]
+        (and (n.= (list;size flatR) (list;size flatS))
+             (list;every? (function [[coverageR coverageS]]
+                            (= coverageR coverageS))
+                          (list;zip2 flatR flatS))))
+
+      _
+      false)))
+
+(open Eq<Coverage> "C/")
+
+(def: (merge-coverages addition so-far)
+  (-> Coverage Coverage (R;Result Coverage))
+  (case [addition so-far]
+    ## The addition cannot possibly improve the coverage.
+    [_ #TotalC]
+    redundant-pattern
+
+    ## The addition completes the coverage.
+    [#TotalC _]
+    (R/wrap #TotalC)
+
+    [#PartialC #PartialC]
+    (R/wrap #PartialC)
+
+    (^=> [(#BoolC sideA) (#BoolC sideSF)]
+         (xor sideA sideSF))
+    (R/wrap #TotalC)
+
+    [(#VariantC allA casesA) (#VariantC allSF casesSF)]
+    (cond (not (n.= allSF allA))
+          (R;fail "Variants do not match.")
+
+          (:: (D;Eq<Dict> Eq<Coverage>) = casesSF casesA)
+          redundant-pattern
+
+          ## else
+          (do R;Monad<Result>
+            [casesM (foldM @
+                           (function [[tagA coverageA] casesSF']
+                             (case (D;get tagA casesSF')
+                               (#;Some coverageSF)
+                               (do @
+                                 [coverageM (merge-coverages coverageA coverageSF)]
+                                 (wrap (D;put tagA coverageM casesSF')))
+
+                               #;None
+                               (wrap (D;put tagA coverageA casesSF'))))
+                           casesSF (D;entries casesA))]
+            (wrap (if (list;every? total? (D;values casesM))
+                    #TotalC
+                    (#VariantC allSF casesM)))))
+
+    [(#SeqC leftA rightA) (#SeqC leftSF rightSF)]
+    (case [(C/= leftSF leftA) (C/= rightSF rightA)]
+      ## There is nothing the addition adds to the coverage.
+      [true true]
+      redundant-pattern
+
+      ## The 2 sequences cannot possibly be merged.
+      [false false]
+      (R/wrap (#AltC so-far addition))
+
+      ## Same prefix
+      [true false]
+      (do R;Monad<Result>
+        [rightM (merge-coverages rightA rightSF)]
+        (if (total? rightM)
+          (wrap leftSF)
+          (wrap (#SeqC leftSF rightM))))
+
+      ## Same suffix
+      [false true]
+      (do R;Monad<Result>
+        [leftM (merge-coverages leftA leftSF)]
+        (wrap (#SeqC leftM rightA))))
+    
+    ## The left part will always match, so the addition is redundant.
+    (^=> [(#SeqC left right) single]
+         (C/= left single))
+    redundant-pattern
+
+    ## The right part is not necessary, since it can always match the left.
+    (^=> [single (#SeqC left right)]
+         (C/= left single))
+    (R/wrap single)
+
+    [_ (#AltC leftS rightS)]
+    (do R;Monad<Result>
+      [#let [fuse-once (: (-> Coverage (List Coverage)
+                              (R;Result [(Maybe Coverage)
+                                         (List Coverage)]))
+                          (function [coverage possibilities]
+                            (loop [alts possibilities]
+                              (case alts
+                                #;Nil
+                                (wrap [#;None (list coverage)])
+                                
+                                (#;Cons alt alts')
+                                (case (merge-coverages coverage alt)
+                                  (#R;Success altM)
+                                  (case altM
+                                    (#AltC _)
+                                    (do @
+                                      [[success alts+] (recur alts')]
+                                      (wrap [success (#;Cons alt alts+)]))
+
+                                    _
+                                    (wrap [(#;Some altM) alts']))
+                                  
+                                  (#R;Error error)
+                                  (R;fail error))
+                                ))))]
+       [success possibilities] (fuse-once addition (flatten-alt so-far))]
+      (loop [success success
+             possibilities possibilities]
+        (case success
+          (#;Some coverage')
+          (do @
+            [[success' possibilities'] (fuse-once coverage' possibilities)]
+            (recur success' possibilities'))
+          
+          #;None
+          (case (list;reverse possibilities)
+            #;Nil
+            (R;fail "{ This is not supposed to happen... }")
+            
+            (#;Cons last prevs)
+            (wrap (L/fold (function [left right] (#AltC left right))
+                          last
+                          prevs))))))
+
+    _
+    (if (C/= so-far addition)
+      ## The addition cannot possibly improve the coverage.
+      redundant-pattern
+      ## There are now 2 alternative paths.
+      (R/wrap (#AltC so-far addition)))))
+
+(def: get-coverage
+  (-> [Pattern Analysis] Coverage)
+  (|>. product;left determine-coverage))
+
+(def: #export (analyse-case analyse input branches)
+  (-> &;Analyser Code (List [Code Code]) (Lux Analysis))
+  (case branches
+    #;Nil
+    (&;fail "Cannot have empty branches in pattern-matching expression.")
+
+    (#;Cons [patternH bodyH] branchesT)
+    (do Monad<Lux>
+      [[inputT inputA] (&common;with-unknown-type
+                         (analyse input))
+       outputH (analyse-branch analyse inputT patternH bodyH)
+       outputT (mapM @
+                     (function [[patternT bodyT]]
+                       (analyse-branch analyse inputT patternT bodyT))
+                     branchesT)
+       _ (case (foldM R;Monad<Result>
+                      merge-coverages
+                      (get-coverage outputH)
+                      (L/map get-coverage outputT))
+           (#R;Success coverage)
+           (if (total? coverage)
+             (wrap [])
+             (&;fail "Pattern-matching is not total."))
+
+           (#R;Error error)
+           (&;fail error))]
+      (wrap (#la;Case inputA (#;Cons outputH outputT))))))
diff --git a/new-luxc/source/luxc/analyser/function.lux b/new-luxc/source/luxc/analyser/function.lux
index 4b867551e..44deec45b 100644
--- a/new-luxc/source/luxc/analyser/function.lux
+++ b/new-luxc/source/luxc/analyser/function.lux
@@ -50,81 +50,76 @@
 (def: #export (analyse-function analyse func-name arg-name body)
   (-> &;Analyser Text Text Code (Lux Analysis))
   (do Monad<Lux>
-    [expected macro;expected-type]
-    (&;with-stacked-errors
-      (function [_] (format "Functions require function types: " (type;to-text expected)))
-      (case expected
-        (#;Named name unnamedT)
-        (&;with-expected-type unnamedT
-          (analyse-function analyse func-name arg-name body))
+    [original macro;expected-type]
+    (loop [expected original]
+      (&;with-stacked-errors
+        (function [_] (format "Functions require function types: " (type;to-text expected)))
+        (case expected
+          (#;Named name unnamedT)
+          (recur unnamedT)
 
-        (#;App funT argT)
-        (do @
-          [fully-applied (case (type;apply-type funT argT)
-                           (#;Some value)
-                           (wrap value)
+          (#;App funT argT)
+          (do @
+            [fully-applied (case (type;apply-type funT argT)
+                             (#;Some value)
+                             (wrap value)
 
-                           #;None
-                           (&;fail (format "Cannot apply type " (%type funT) " to  type " (%type argT))))]
-          (&;with-expected-type fully-applied
-            (analyse-function analyse func-name arg-name body)))
-        
-        (#;UnivQ _)
-        (do @
-          [[var-id var] (&;within-type-env
-                         TC;existential)]
-          (&;with-expected-type (assume (type;apply-type expected var))
-            (analyse-function analyse func-name arg-name body)))
+                             #;None
+                             (&;fail (format "Cannot apply type " (%type funT) " to  type " (%type argT))))]
+            (recur fully-applied))
+          
+          (#;UnivQ _)
+          (do @
+            [[var-id var] (&;within-type-env
+                           TC;existential)]
+            (recur (assume (type;apply-type expected var))))
 
-        (#;ExQ _)
-        (&common;with-var
-          (function [[var-id var]]
-            (&;with-expected-type (assume (type;apply-type expected var))
-              (analyse-function analyse func-name arg-name body))))
-        
-        (#;Var id)
-        (do @
-          [? (&;within-type-env
-              (TC;bound? id))]
-          (if ?
-            (do @
-              [expected' (&;within-type-env
-                          (TC;read-var id))]
-              (&;with-expected-type expected'
-                (analyse-function analyse func-name arg-name body)))
-            ## Inference
-            (&common;with-var
-              (function [[input-id inputT]]
-                (&common;with-var
-                  (function [[output-id outputT]]
-                    (do @
-                      [#let [funT (#;Function inputT outputT)]
-                       =function (&;with-expected-type funT
-                                   (analyse-function analyse func-name arg-name body))
-                       funT' (&;within-type-env
-                              (TC;clean output-id funT))
-                       concrete-input? (&;within-type-env
-                                        (TC;bound? input-id))
-                       funT'' (if concrete-input?
-                                (&;within-type-env
-                                 (TC;clean input-id funT'))
-                                (wrap (#;UnivQ (list) (bind-var input-id +1 funT'))))
-                       _ (&;within-type-env
-                          (TC;check expected funT''))]
-                      (wrap =function))
-                    ))))))
+          (#;ExQ _)
+          (&common;with-var
+            (function [[var-id var]]
+              (recur (assume (type;apply-type expected var)))))
+          
+          (#;Var id)
+          (do @
+            [? (&;within-type-env
+                (TC;bound? id))]
+            (if ?
+              (do @
+                [expected' (&;within-type-env
+                            (TC;read-var id))]
+                (recur expected'))
+              ## Inference
+              (&common;with-var
+                (function [[input-id inputT]]
+                  (&common;with-var
+                    (function [[output-id outputT]]
+                      (do @
+                        [#let [funT (#;Function inputT outputT)]
+                         =function (recur funT)
+                         funT' (&;within-type-env
+                                (TC;clean output-id funT))
+                         concrete-input? (&;within-type-env
+                                          (TC;bound? input-id))
+                         funT'' (if concrete-input?
+                                  (&;within-type-env
+                                   (TC;clean input-id funT'))
+                                  (wrap (#;UnivQ (list) (bind-var input-id +1 funT'))))
+                         _ (&;within-type-env
+                            (TC;check expected funT''))]
+                        (wrap =function))
+                      ))))))
 
-        (#;Function inputT outputT)
-        (<| (:: @ map (|>. #la;Function))
-            &;with-scope
-            (&env;with-local [func-name expected])
-            (&env;with-local [arg-name inputT])
-            (&;with-expected-type outputT)
-            (analyse body))
-        
-        _
-        (&;fail "")
-        ))))
+          (#;Function inputT outputT)
+          (<| (:: @ map (|>. #la;Function))
+              &;with-scope
+              (&env;with-local [func-name original])
+              (&env;with-local [arg-name inputT])
+              (&;with-expected-type outputT)
+              (analyse body))
+          
+          _
+          (&;fail "")
+          )))))
 
 (def: (analyse-apply' analyse funcT args)
   (-> &;Analyser Type (List Code) (Lux [Type (List Analysis)]))
diff --git a/new-luxc/source/luxc/analyser/pattern.lux b/new-luxc/source/luxc/analyser/pattern.lux
deleted file mode 100644
index f4a14d855..000000000
--- a/new-luxc/source/luxc/analyser/pattern.lux
+++ /dev/null
@@ -1,3 +0,0 @@
-(;module:
-  lux)
-
diff --git a/new-luxc/source/luxc/analyser/struct.lux b/new-luxc/source/luxc/analyser/struct.lux
index 0ca3c9f63..1fbca886f 100644
--- a/new-luxc/source/luxc/analyser/struct.lux
+++ b/new-luxc/source/luxc/analyser/struct.lux
@@ -6,11 +6,14 @@
        (concurrency ["A" atom])
        (data [text "T/" Eq<Text>]
              text/format
+             [ident]
              (coll [list "L/" Fold<List> Monoid<List> Monad<List>]
-                   ["D" dict])
+                   ["D" dict]
+                   ["S" set])
              [number]
              [product])
        [macro #+ Monad<Lux>]
+       (macro [code])
        [type]
        (type ["TC" check]))
   (luxc ["&" base]
@@ -169,3 +172,65 @@
         
         _
         (&;fail "")))))
+
+(def: (resolve-pair [key val])
+  (-> [Ident Code] (Lux [Type Nat Code]))
+  (do Monad<Lux>
+    [key (macro;normalize key)
+     [idx tag-set recordT] (macro;resolve-tag key)]
+    (wrap [recordT idx val])))
+
+(def: #export (normalize-record pairs)
+  (-> (List [Code Code]) (Lux (List [Ident Code])))
+  (mapM Monad<Lux>
+        (function [[key val]]
+          (case key
+            [_ (#;Tag key)]
+            (do Monad<Lux>
+              [key (macro;normalize key)]
+              (wrap [key val]))
+
+            _
+            (&;fail (format "Cannot use non-tag tokens in key positions in records: " (%code key)))))
+        pairs))
+
+(def: #export (order-record pairs)
+  (-> (List [Ident Code]) (Lux [(List Code) Type]))
+  (case pairs
+    (#;Cons [head-k head-v] _)
+    (do Monad<Lux>
+      [head-k (macro;normalize head-k)
+       [_ tag-set recordT] (macro;resolve-tag head-k)
+       #let [size-record (list;size pairs)
+             size-ts (list;size tag-set)]
+       _ (if (n.= size-ts size-record)
+           (wrap [])
+           (&;fail (format "Record size does not match tag-set size." "\n"
+                           "Expected: " (|> size-ts nat-to-int %i) "\n"
+                           "  Actual: " (|> size-record nat-to-int %i) "\n"
+                           "For type: " (%type recordT))))
+       #let [tuple-range (list;n.range +0 size-ts)
+             tag->idx (D;from-list ident;Hash<Ident> (list;zip2 tag-set tuple-range))]
+       idx->val (foldM @
+                       (function [[key val] idx->val]
+                         (do @
+                           [key (macro;normalize key)]
+                           (case (D;get key tag->idx)
+                             #;None
+                             (&;fail (format "Tag " (%code (code;tag key))
+                                             " does not belong to tag-set for type " (%type recordT)))
+
+                             (#;Some idx)
+                             (if (D;contains? idx idx->val)
+                               (&;fail (format "Cannot repeat tag inside record: " (%code (code;tag key))))
+                               (wrap (D;put idx val idx->val))))))
+                       (: (D;Dict Nat Code)
+                          (D;new number;Hash<Nat>))
+                       pairs)
+       #let [ordered-tuple (L/map (function [idx]
+                                    (assume (D;get idx idx->val)))
+                                  tuple-range)]]
+      (wrap [ordered-tuple recordT]))
+
+    _
+    (:: Monad<Lux> wrap [(list) Unit])))
diff --git a/new-luxc/source/luxc/base.lux b/new-luxc/source/luxc/base.lux
index e900edf6c..612ce70d2 100644
--- a/new-luxc/source/luxc/base.lux
+++ b/new-luxc/source/luxc/base.lux
@@ -3,6 +3,7 @@
   (lux (control monad)
        (data [text "T/" Eq<Text>]
              text/format
+             [product]
              ["R" result])
        [macro #+ Monad<Lux>]
        (type ["TC" check]))
@@ -142,12 +143,14 @@
 
 (def: #export (with-cursor cursor action)
   (All [a] (-> Cursor (Lux a) (Lux a)))
-  (function [compiler]
-    (let [old-cursor (get@ #;cursor compiler)]
-      (case (action (set@ #;cursor cursor compiler))
-        (#R;Success [compiler' output])
-        (#R;Success [(set@ #;cursor old-cursor compiler')
-                     output])
-
-        (#R;Error error)
-        (#R;Error error)))))
+  (if (T/= "" (product;left cursor))
+    action
+    (function [compiler]
+      (let [old-cursor (get@ #;cursor compiler)]
+        (case (action (set@ #;cursor cursor compiler))
+          (#R;Success [compiler' output])
+          (#R;Success [(set@ #;cursor old-cursor compiler')
+                       output])
+
+          (#R;Error error)
+          (#R;Error error))))))
diff --git a/new-luxc/source/luxc/env.lux b/new-luxc/source/luxc/env.lux
index edc6a4a5b..e15e01130 100644
--- a/new-luxc/source/luxc/env.lux
+++ b/new-luxc/source/luxc/env.lux
@@ -146,3 +146,13 @@
                      output])
         ))
     ))
+
+(def: #export next-local
+  (Lux Nat)
+  (function [compiler]
+    (case (get@ #;scopes compiler)
+      #;Nil
+      (#R;Error "Cannot get next reference when there is no scope.")
+      
+      (#;Cons top _)
+      (#R;Success [compiler (get@ [#;locals #;counter] top)]))))
diff --git a/new-luxc/source/luxc/lang/analysis.lux b/new-luxc/source/luxc/lang/analysis.lux
index 71073f901..d9064604a 100644
--- a/new-luxc/source/luxc/lang/analysis.lux
+++ b/new-luxc/source/luxc/lang/analysis.lux
@@ -14,7 +14,7 @@
   (#Text Text)
   (#Variant Nat Bool Analysis)
   (#Tuple (List Analysis))
-  (#Case (List [lp;Pattern Analysis]))
+  (#Case Analysis (List [lp;Pattern Analysis]))
   (#Function Scope Analysis)
   (#Apply Analysis Analysis)
   (#Procedure Ident (List Analysis))
diff --git a/new-luxc/source/luxc/lang/pattern.lux b/new-luxc/source/luxc/lang/pattern.lux
index a0077133b..c422ea419 100644
--- a/new-luxc/source/luxc/lang/pattern.lux
+++ b/new-luxc/source/luxc/lang/pattern.lux
@@ -2,7 +2,7 @@
   lux)
 
 (type: #export #rec Pattern
-  (#Ref Nat)
+  (#Bind Nat)
   #Unit
   (#Bool Bool)
   (#Nat Nat)
diff --git a/new-luxc/source/luxc/synthesizer.lux b/new-luxc/source/luxc/synthesizer.lux
index d2f559c3e..fae6d8c5f 100644
--- a/new-luxc/source/luxc/synthesizer.lux
+++ b/new-luxc/source/luxc/synthesizer.lux
@@ -32,7 +32,7 @@
     (#la;Variant tag last? value)
     (undefined)
 
-    (#la;Case pattern)
+    (#la;Case input matches)
     (undefined)
 
     (#la;Function scope body)