From d6442cc652eacecf0c6860ed69fad4549110c1dd Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Mon, 12 Sep 2022 18:04:23 +0200
Subject: [PATCH 1/9] match first version

---
 src/Juvix/Compiler/Core/Evaluator.hs          | 30 ++++++
 src/Juvix/Compiler/Core/Extra/Base.hs         | 72 +++++++++++++--
 src/Juvix/Compiler/Core/Info/BranchInfo.hs    | 23 -----
 src/Juvix/Compiler/Core/Language.hs           | 18 +++-
 src/Juvix/Compiler/Core/Language/Nodes.hs     | 84 ++++++++++++++++-
 src/Juvix/Compiler/Core/Pretty/Base.hs        | 52 +++++++++--
 .../Compiler/Core/Translation/FromSource.hs   | 91 +++++++++++++++++--
 .../Core/Translation/FromSource/Lexer.hs      |  8 ++
 src/Juvix/Extra/Strings.hs                    |  6 ++
 9 files changed, 333 insertions(+), 51 deletions(-)
 delete mode 100644 src/Juvix/Compiler/Core/Info/BranchInfo.hs

diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index dcdcd8399c..ddcbb1c0eb 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -74,6 +74,9 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
         case eval' env v of
           NCtr (Constr _ tag args) -> branch n env args tag def bs
           v' -> evalError "matching on non-data" (substEnv env (mkCase i v' bs def))
+      NMatch (Match _ vs bs) ->
+        let !vs' = map' (eval' env) (toList vs)
+         in match n env vs' bs
       NPi {} -> substEnv env n
       NUniv {} -> n
       NTyp (TypeConstr i sym args) -> mkTypeConstr i sym (map' (eval' env) args)
@@ -89,6 +92,33 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
         Just b -> eval' env b
         Nothing -> evalError "no matching case branch" (substEnv env n)
 
+    match :: Node -> Env -> [Node] -> [MatchBranch] -> Node
+    match n env vs = \case
+      br : brs ->
+        case matchPatterns [] vs (toList (br ^. matchBranchPatterns)) of
+          Just args -> eval' (args ++ env) (br ^. matchBranchBody)
+          Nothing -> match n env vs brs
+        where
+          matchPatterns :: [Node] -> [Node] -> [Pattern] -> Maybe [Node]
+          matchPatterns acc (v : vs') (p : ps') =
+            case patmatch acc v p of
+              Just acc' -> matchPatterns acc' vs' ps'
+              Nothing -> Nothing
+          matchPatterns acc [] [] =
+            Just acc
+          matchPatterns _ _ _ =
+            evalError "the number of patterns doesn't match the number of arguments" (substEnv env n)
+
+          patmatch :: [Node] -> Node -> Pattern -> Maybe [Node]
+          patmatch acc _ PatWildcard {} = Just acc
+          patmatch acc v PatBinder {} = Just (v : acc)
+          patmatch acc (NCtr (Constr _ tag args)) (PatConstr PatternConstr {..})
+            | tag == _patternConstrTag =
+                matchPatterns acc args _patternConstrArgs
+          patmatch _ _ _ = Nothing
+      [] ->
+        evalError "no matching pattern" (substEnv env n)
+
     applyBuiltin :: Node -> Env -> BuiltinOp -> [Node] -> Node
     applyBuiltin _ env OpIntAdd [l, r] = nodeFromInteger (integerFromNode (eval' env l) + integerFromNode (eval' env r))
     applyBuiltin _ env OpIntSub [l, r] = nodeFromInteger (integerFromNode (eval' env l) - integerFromNode (eval' env r))
diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index 8eae664904..e188925d74 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -70,6 +70,12 @@ mkCase i v bs def = NCase (Case i v bs def)
 mkCase' :: Node -> [CaseBranch] -> Maybe Node -> Node
 mkCase' = mkCase Info.empty
 
+mkMatch :: Info -> NonEmpty Node -> [MatchBranch] -> Node
+mkMatch i vs bs = NMatch (Match i vs bs)
+
+mkMatch' :: NonEmpty Node -> [MatchBranch] -> Node
+mkMatch' = mkMatch Info.empty
+
 mkIf :: Info -> Node -> Node -> Node -> Node
 mkIf i v b1 b2 = mkCase i v [CaseBranch Info.empty (BuiltinTag TagTrue) 0 b1] (Just b2)
 
@@ -157,6 +163,30 @@ unfoldLambdas = go []
 unfoldLambdas' :: Node -> (Int, Node)
 unfoldLambdas' = first length . unfoldLambdas
 
+getBinderPatternInfos :: Pattern -> [Info]
+getBinderPatternInfos = go []
+  where
+    go :: [Info] -> Pattern -> [Info]
+    go acc = \case
+      PatConstr (PatternConstr {..}) ->
+        foldl' go acc _patternConstrArgs
+      PatBinder (PatternBinder {..}) ->
+        _patternBinderInfo : acc
+      PatWildcard {} ->
+        acc
+
+getPatternInfos :: Pattern -> [Info]
+getPatternInfos = go []
+  where
+    go :: [Info] -> Pattern -> [Info]
+    go acc = \case
+      PatConstr (PatternConstr {..}) ->
+        foldl' go (_patternConstrInfo : acc) _patternConstrArgs
+      PatBinder (PatternBinder {..}) ->
+        _patternBinderInfo : acc
+      PatWildcard (PatternWildcard {..}) ->
+        _patternWildcardInfo : acc
+
 -- | `NodeDetails` is a convenience datatype which provides the most commonly needed
 -- information about a node in a generic fashion.
 data NodeDetails = NodeDetails
@@ -257,11 +287,11 @@ destruct = \case
             _nodeReassemble = \i' args' -> mkLetRec i' (fromList (tl args')) (hd args')
           }
   NCase (Case i v bs Nothing) ->
-    let branchBinderNums = map (\(CaseBranch _ _ k _) -> k) bs
-        branchBinderInfos = map (\(CaseBranch bi _ k _) -> getInfoBinders k bi) bs
+    let branchBinderNums = map (^. caseBranchBindersNum) bs
+        branchBinderInfos = map (\(CaseBranch {..}) -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
      in NodeDetails
           { _nodeInfo = i,
-            _nodeChildren = v : map (\(CaseBranch _ _ _ br) -> br) bs,
+            _nodeChildren = v : map (^. caseBranchBody) bs,
             _nodeChildBindersNum = 0 : branchBinderNums,
             _nodeChildBindersInfo = [] : branchBinderInfos,
             _nodeReassemble = \i' args' ->
@@ -269,18 +299,18 @@ destruct = \case
                 i'
                 (hd args')
                 ( zipWithExact
-                    (\(CaseBranch bi tag k _) br' -> CaseBranch bi tag k br')
+                    (\br body' -> br {_caseBranchBody = body'})
                     bs
                     (tl args')
                 )
                 Nothing
           }
   NCase (Case i v bs (Just def)) ->
-    let branchBinderNums = map (\(CaseBranch _ _ k _) -> k) bs
-        branchBinderInfos = map (\(CaseBranch bi _ k _) -> getInfoBinders k bi) bs
+    let branchBinderNums = map (^. caseBranchBindersNum) bs
+        branchBinderInfos = map (\(CaseBranch {..}) -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
      in NodeDetails
           { _nodeInfo = i,
-            _nodeChildren = v : def : map (\(CaseBranch _ _ _ br) -> br) bs,
+            _nodeChildren = v : def : map (^. caseBranchBody) bs,
             _nodeChildBindersNum = 0 : 0 : branchBinderNums,
             _nodeChildBindersInfo = [] : [] : branchBinderInfos,
             _nodeReassemble = \i' args' ->
@@ -288,12 +318,38 @@ destruct = \case
                 i'
                 (hd args')
                 ( zipWithExact
-                    (\(CaseBranch bi tag k _) br' -> CaseBranch bi tag k br')
+                    (\br body' -> br {_caseBranchBody = body'})
                     bs
                     (tl (tl args'))
                 )
                 (Just (hd (tl args')))
           }
+  NMatch (Match i vs bs) ->
+    let branchBinderInfos =
+          map
+            ( \br ->
+                concatMap
+                  getBinderPatternInfos
+                  (reverse (toList (br ^. matchBranchPatterns)))
+            )
+            bs
+        branchBinderNums = map length branchBinderInfos
+        n = length vs
+     in NodeDetails
+          { _nodeInfo = i,
+            _nodeChildren = toList vs ++ map (^. matchBranchBody) bs,
+            _nodeChildBindersNum = replicate n 0 ++ branchBinderNums,
+            _nodeChildBindersInfo = replicate n [] ++ branchBinderInfos,
+            _nodeReassemble = \i' args' ->
+              mkMatch
+                i'
+                (fromList $ List.take n args')
+                ( zipWithExact
+                    (\br body' -> br {_matchBranchBody = body'})
+                    bs
+                    (drop n args')
+                )
+          }
   NPi (Pi i ty b) ->
     NodeDetails
       { _nodeInfo = i,
diff --git a/src/Juvix/Compiler/Core/Info/BranchInfo.hs b/src/Juvix/Compiler/Core/Info/BranchInfo.hs
deleted file mode 100644
index ceb7c33e3c..0000000000
--- a/src/Juvix/Compiler/Core/Info/BranchInfo.hs
+++ /dev/null
@@ -1,23 +0,0 @@
-module Juvix.Compiler.Core.Info.BranchInfo where
-
-import Juvix.Compiler.Core.Info qualified as Info
-import Juvix.Compiler.Core.Language.Base
-
-newtype BranchInfo = BranchInfo
-  { _infoTagName :: Name
-  }
-
-instance IsInfo BranchInfo
-
-kBranchInfo :: Key BranchInfo
-kBranchInfo = Proxy
-
-makeLenses ''BranchInfo
-
-getInfoTagName :: Info -> Maybe Name
-getInfoTagName i = case Info.lookup kBranchInfo i of
-  Just BranchInfo {..} -> Just _infoTagName
-  Nothing -> Nothing
-
-setInfoTagName :: Name -> Info -> Info
-setInfoTagName = Info.insert . BranchInfo
diff --git a/src/Juvix/Compiler/Core/Language.hs b/src/Juvix/Compiler/Core/Language.hs
index d9272b7dee..6de540dd05 100644
--- a/src/Juvix/Compiler/Core/Language.hs
+++ b/src/Juvix/Compiler/Core/Language.hs
@@ -32,6 +32,20 @@ type LetRec = LetRec' Info Node
 
 type Case = Case' Info Info Node
 
+type CaseBranch = CaseBranch' Info Node
+
+type Match = Match' Info Node
+
+type MatchBranch = MatchBranch' Info Node
+
+type PatternWildcard = PatternWildcard' Info
+
+type PatternBinder = PatternBinder' Info
+
+type PatternConstr = PatternConstr' Info
+
+type Pattern = Pattern' Info
+
 type Pi = Pi' Info Node
 
 type Univ = Univ' Info
@@ -42,8 +56,6 @@ type TypePrim = TypePrim' Info
 
 type Dynamic = Dynamic' Info
 
-type CaseBranch = CaseBranch' Info Node
-
 {---------------------------------------------------------------------------------}
 
 -- | `Node` is the type of nodes in the program tree. The nodes themselves
@@ -61,6 +73,7 @@ data Node
   | NLet {-# UNPACK #-} !Let
   | NRec {-# UNPACK #-} !LetRec
   | NCase {-# UNPACK #-} !Case
+  | NMatch {-# UNPACK #-} !Match
   | NPi {-# UNPACK #-} !Pi
   | NUniv {-# UNPACK #-} !Univ
   | NTyp {-# UNPACK #-} !TypeConstr
@@ -105,6 +118,7 @@ instance HasAtomicity Node where
     NLet x -> atomicity x
     NRec x -> atomicity x
     NCase x -> atomicity x
+    NMatch x -> atomicity x
     NPi x -> atomicity x
     NUniv x -> atomicity x
     NTyp x -> atomicity x
diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs
index 8e57929046..f6df2a6e5e 100644
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/src/Juvix/Compiler/Core/Language/Nodes.hs
@@ -87,23 +87,63 @@ data CaseBranch' i a = CaseBranch
     _caseBranchBody :: !a
   }
 
+-- | Complex pattern match. `Match` is lazy: only the selected branch is evaluated.
+data Match' i a = Match
+  { _matchInfo :: i,
+    _matchValues :: !(NonEmpty a),
+    _matchBranches :: ![MatchBranch' i a]
+  }
+
+-- | The patterns introduce binders from left to right, e.g., matching on the
+-- patterns '(C (D x) y) (E _ z)' with body 'f x y z' may be represented by a
+-- 'MatchBranch' with '_matchBranchPatterns' equal to '[PatConstr Ctag
+-- [PatConstr Dtag [PatBinder], PatBinder], PatConstr Etag [PatWildcard,
+-- PatBinder]]' and '_matchBranchBody' equal to 'App (App (App (Ident f) (Var
+-- 2)) (Var 1)) (Var 0)'. So the de Bruijn indices increase from right to left.
+data MatchBranch' i a = MatchBranch
+  { _matchBranchInfo :: i,
+    _matchBranchPatterns :: !(NonEmpty (Pattern' i)),
+    _matchBranchBody :: !a
+  }
+
+data Pattern' i
+  = PatWildcard (PatternWildcard' i)
+  | PatBinder (PatternBinder' i)
+  | PatConstr (PatternConstr' i)
+  deriving stock (Eq)
+
+newtype PatternWildcard' i = PatternWildcard
+  { _patternWildcardInfo :: i
+  }
+
+newtype PatternBinder' i = PatternBinder
+  { _patternBinderInfo :: i
+  }
+
+data PatternConstr' i = PatternConstr
+  { _patternConstrInfo :: i,
+    _patternConstrTag :: !Tag,
+    _patternConstrArgs :: ![Pattern' i]
+  }
+
 -- | Dependent Pi-type. Compilation-time only. Pi implicitly introduces a binder
 -- in the body, exactly like Lambda. So `Pi info ty body` is `Pi x : ty .
 -- body` in more familiar notation, but references to `x` in `body` are via de
--- Bruijn index. For example, Pi A : GHC.Type . A -> A translates to (omitting
+-- Bruijn index. For example, Pi A : Type . A -> A translates to (omitting
 -- Infos): Pi (Univ level) (Pi (Var 0) (Var 1)).
 data Pi' i a = Pi {_piInfo :: i, _piType :: !a, _piBody :: !a}
 
 -- | Universe. Compilation-time only.
 data Univ' i = Univ {_univInfo :: i, _univLevel :: !Int}
 
--- | GHC.Type constructor application. Compilation-time only.
+-- | Type constructor application. Compilation-time only.
 data TypeConstr' i a = TypeConstr
   { _typeConstrInfo :: i,
     _typeConstrSymbol :: !Symbol,
     _typeConstrArgs :: ![a]
   }
 
+-- | A primitive type.
 data TypePrim' i = TypePrim
   { _typePrimInfo :: i,
     _typePrimPrimitive :: Primitive
@@ -154,6 +194,24 @@ instance HasAtomicity (LetRec' i a) where
 instance HasAtomicity (Case' i bi a) where
   atomicity _ = Aggregate lambdaFixity
 
+instance HasAtomicity (Match' i a) where
+  atomicity _ = Aggregate lambdaFixity
+
+instance HasAtomicity (PatternWildcard' i) where
+  atomicity _ = Atom
+
+instance HasAtomicity (PatternBinder' i) where
+  atomicity _ = Atom
+
+instance HasAtomicity (PatternConstr' i) where
+  atomicity _ = Aggregate appFixity
+
+instance HasAtomicity (Pattern' i) where
+  atomicity = \case
+    PatWildcard x -> atomicity x
+    PatBinder x -> atomicity x
+    PatConstr x -> atomicity x
+
 instance HasAtomicity (Pi' i a) where
   atomicity _ = Aggregate lambdaFixity
 
@@ -208,6 +266,21 @@ instance Eq a => Eq (Case' i bi a) where
 instance Eq a => Eq (CaseBranch' i a) where
   (CaseBranch _ tag1 n1 b1) == (CaseBranch _ tag2 n2 b2) = tag1 == tag2 && n1 == n2 && b1 == b2
 
+instance Eq a => Eq (Match' i a) where
+  (Match _ vs1 bs1) == (Match _ vs2 bs2) = vs1 == vs2 && bs1 == bs2
+
+instance Eq a => Eq (MatchBranch' i a) where
+  (MatchBranch _ pats1 b1) == (MatchBranch _ pats2 b2) = pats1 == pats2 && b1 == b2
+
+instance Eq (PatternWildcard' i) where
+  _ == _ = True
+
+instance Eq (PatternBinder' i) where
+  _ == _ = True
+
+instance Eq (PatternConstr' i) where
+  (PatternConstr _ tag1 ps1) == (PatternConstr _ tag2 ps2) = tag1 == tag2 && ps1 == ps2
+
 instance Eq a => Eq (Pi' i a) where
   (Pi _ ty1 b1) == (Pi _ ty2 b2) = ty1 == ty2 && b1 == b2
 
@@ -232,11 +305,16 @@ makeLenses ''Constr'
 makeLenses ''Let'
 makeLenses ''LetRec'
 makeLenses ''Case'
+makeLenses ''CaseBranch'
+makeLenses ''Match'
+makeLenses ''MatchBranch'
+makeLenses ''PatternWildcard'
+makeLenses ''PatternBinder'
+makeLenses ''PatternConstr'
 makeLenses ''Pi'
 makeLenses ''Univ'
 makeLenses ''TypeConstr'
 makeLenses ''Dynamic'
-makeLenses ''CaseBranch'
 
 instance Hashable (Ident' i) where
   hashWithSalt s = hashWithSalt s . (^. identSymbol)
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index d481f2bfb8..ce84075a0b 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -5,13 +5,13 @@ module Juvix.Compiler.Core.Pretty.Base
   )
 where
 
+import Data.Functor
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Data.Stripped.InfoTable qualified as Stripped
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.BinderInfo
-import Juvix.Compiler.Core.Info.BranchInfo as BranchInfo
 import Juvix.Compiler.Core.Info.NameInfo as NameInfo
 import Juvix.Compiler.Core.Language
 import Juvix.Compiler.Core.Language.Stripped qualified as Stripped
@@ -138,8 +138,8 @@ ppCodeLet' name lt = do
 
 ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Maybe Name]] -> [Maybe Name] -> Case' i bi a -> Sem r (Doc Ann)
 ppCodeCase' branchBinderNames branchTagNames Case {..} = do
-  let branchTags = map (\(CaseBranch _ tag _ _) -> tag) _caseBranches
-  let branchBodies = map (\(CaseBranch _ _ _ b) -> b) _caseBranches
+  let branchTags = map (^. caseBranchTag) _caseBranches
+  let branchBodies = map (^. caseBranchBody) _caseBranches
   bns <- mapM (mapM (maybe (return kwQuestion) ppCode)) branchBinderNames
   cns <- zipWithM (\tag -> maybe (ppCode tag) ppCode) branchTags branchTagNames
   v <- ppCode _caseValue
@@ -153,6 +153,30 @@ ppCodeCase' branchBinderNames branchTagNames Case {..} = do
   let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs''
   return $ kwCase <+> v <+> kwOf <+> bss
 
+instance PrettyCode PatternWildcard where
+  ppCode _ = return kwWildcard
+
+instance PrettyCode PatternBinder where
+  ppCode PatternBinder {..} =
+    case getInfoName _patternBinderInfo of
+      Just name -> ppCode name
+      Nothing -> return kwQuestion
+
+instance PrettyCode PatternConstr where
+  ppCode PatternConstr {..} = do
+    n <- maybe (ppCode _patternConstrTag) ppCode (getInfoName _patternConstrInfo)
+    args <- mapM (ppRightExpression appFixity) _patternConstrArgs
+    return $ n <+> hsep args
+
+instance PrettyCode Pattern where
+  ppCode = \case
+    PatWildcard x -> ppCode x
+    PatBinder x -> ppCode x
+    PatConstr x -> ppCode x
+
+ppPatterns :: Member (Reader Options) r => NonEmpty Pattern -> Sem r (Doc Ann)
+ppPatterns pats = mapM (ppRightExpression appFixity) pats <&> hsep
+
 instance PrettyCode Node where
   ppCode :: forall r. Member (Reader Options) r => Node -> Sem r (Doc Ann)
   ppCode node = case node of
@@ -206,9 +230,17 @@ instance PrettyCode Node where
             Just name -> ppCode name
             Nothing -> return kwQuestion
     NCase x@Case {..} ->
-      let branchBinderNames = map (\(CaseBranch bi _ k _) -> map getInfoName (getInfoBinders k bi)) _caseBranches
-          branchTagNames = map (\(CaseBranch bi _ _ _) -> getInfoTagName bi) _caseBranches
+      let branchBinderNames = map (\(CaseBranch {..}) -> map getInfoName (getInfoBinders _caseBranchBindersNum _caseBranchInfo)) _caseBranches
+          branchTagNames = map (\(CaseBranch {..}) -> getInfoName _caseBranchInfo) _caseBranches
        in ppCodeCase' branchBinderNames branchTagNames x
+    NMatch Match {..} -> do
+      let branchPatterns = map (^. matchBranchPatterns) _matchBranches
+      let branchBodies = map (^. matchBranchBody) _matchBranches
+      pats <- mapM ppPatterns branchPatterns
+      vs <- mapM ppCode _matchValues
+      bs <- sequence $ zipWithExact (\ps br -> ppCode br >>= \br' -> return $ ps <+> kwMapsto <+> br') pats branchBodies
+      let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs
+      return $ kwMatch <+> hsep vs <+> kwWith <+> bss
     NPi Pi {..} ->
       case getInfoName $ getInfoBinder _piInfo of
         Just name -> do
@@ -250,8 +282,8 @@ instance PrettyCode Stripped.Node where
       let name = x ^. (letInfo . Stripped.letInfoBinderName)
        in ppCodeLet' name x
     Stripped.NCase x@Stripped.Case {..} ->
-      let branchBinderNames = map (\(Stripped.CaseBranch bi _ _ _) -> bi ^. Stripped.caseBranchInfoBinderNames) _caseBranches
-          branchTagNames = map (\(Stripped.CaseBranch bi _ _ _) -> bi ^. Stripped.caseBranchInfoConstrName) _caseBranches
+      let branchBinderNames = map (^. (caseBranchInfo . Stripped.caseBranchInfoBinderNames)) _caseBranches
+          branchTagNames = map (^. (caseBranchInfo . Stripped.caseBranchInfoConstrName)) _caseBranches
        in ppCodeCase' branchBinderNames branchTagNames x
 
 instance PrettyCode InfoTable where
@@ -381,6 +413,12 @@ kwCase = keyword Str.case_
 kwOf :: Doc Ann
 kwOf = keyword Str.of_
 
+kwMatch :: Doc Ann
+kwMatch = keyword Str.match_
+
+kwWith :: Doc Ann
+kwWith = keyword Str.with_
+
 kwDefault :: Doc Ann
 kwDefault = keyword Str.underscore
 
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 215e1b4890..6b27f55492 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -13,7 +13,6 @@ import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.BinderInfo as BinderInfo
-import Juvix.Compiler.Core.Info.BranchInfo as BranchInfo
 import Juvix.Compiler.Core.Info.LocationInfo as LocationInfo
 import Juvix.Compiler.Core.Info.NameInfo as NameInfo
 import Juvix.Compiler.Core.Info.TypeInfo as TypeInfo
@@ -672,25 +671,25 @@ caseBranchP ::
   HashMap Text Index ->
   ParsecS r (Either CaseBranch Node)
 caseBranchP varsNum vars =
-  (defaultBranch varsNum vars <&> Right)
-    <|> (matchingBranch varsNum vars <&> Left)
+  (caseDefaultBranch varsNum vars <&> Right)
+    <|> (caseMatchingBranch varsNum vars <&> Left)
 
-defaultBranch ::
+caseDefaultBranch ::
   Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
   Index ->
   HashMap Text Index ->
   ParsecS r Node
-defaultBranch varsNum vars = do
+caseDefaultBranch varsNum vars = do
   kwWildcard
   kwAssign
   expr varsNum vars
 
-matchingBranch ::
+caseMatchingBranch ::
   Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
   Index ->
   HashMap Text Index ->
   ParsecS r CaseBranch
-matchingBranch varsNum vars = do
+caseMatchingBranch varsNum vars = do
   off <- P.getOffset
   txt <- identifier
   r <- lift (getIdent txt)
@@ -714,7 +713,7 @@ matchingBranch varsNum vars = do
                 (vars, varsNum)
                 ns
       br <- expr (varsNum + bindersNum) vars'
-      let info = setInfoTagName (ci ^. constructorName) $ setInfoBinders (map (Info.singleton . NameInfo) ns) Info.empty
+      let info = setInfoName (ci ^. constructorName) $ setInfoBinders (map (Info.singleton . NameInfo) ns) Info.empty
       return $ CaseBranch info tag bindersNum br
     Nothing ->
       parseFailure off ("undeclared identifier: " ++ fromText txt)
@@ -732,3 +731,79 @@ exprIf varsNum vars = do
   kwElse
   br2 <- expr varsNum vars
   return $ mkIf Info.empty value br1 br2
+
+exprMatch ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+exprMatch varsNum vars = do
+  kwMatch
+  values <- P.some (expr varsNum vars)
+  kwWith
+  braces (exprMatch' values varsNum vars)
+    <|> exprMatch' values varsNum vars
+
+exprMatch' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  [Node] ->
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+exprMatch' values varsNum vars = do
+  bs <- P.sepEndBy (matchBranch (length values) varsNum vars) kwSemicolon
+  return $ mkMatch' (fromList values) bs
+
+matchBranch ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Int ->
+  Index ->
+  HashMap Text Index ->
+  ParsecS r MatchBranch
+matchBranch patsNum varsNum vars = do
+  off <- P.getOffset
+  pats <- P.some branchPattern
+  kwMapsTo
+  unless (length pats == patsNum) $
+    parseFailure off "wrong number of patterns"
+  let pis = concatMap (reverse . getBinderPatternInfos) pats
+  let (vars', varsNum') =
+        foldl'
+          ( \(vs, k) name ->
+              (HashMap.insert (name ^. nameText) k vs, k + 1)
+          )
+          (vars, varsNum)
+          (map (fromJust . getInfoName) pis)
+  br <- expr varsNum' vars'
+  return $ MatchBranch Info.empty (fromList pats) br
+
+branchPattern ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r Pattern
+branchPattern =
+  wildcardPattern
+    <|> parens wildcardPattern
+    <|> parens binderOrConstrPattern
+    <|> binderOrConstrPattern
+
+wildcardPattern :: ParsecS r Pattern
+wildcardPattern = do
+  kwWildcard
+  return $ PatWildcard (PatternWildcard Info.empty)
+
+binderOrConstrPattern ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r Pattern
+binderOrConstrPattern = do
+  (txt, i) <- identifierL
+  r <- lift (getIdent txt)
+  case r of
+    Just (IdentTag tag) -> do
+      ps <- P.many branchPattern
+      ci <- lift $ getConstructorInfo tag
+      kwMapsTo
+      let info = setInfoName (ci ^. constructorName) Info.empty
+      return $ PatConstr (PatternConstr info tag ps)
+    _ -> do
+      n <- lift $ freshName KNameLocal txt i
+      return $ PatBinder (PatternBinder (setInfoName n Info.empty))
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
index 47fd05b843..4c5e93af0f 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
@@ -61,6 +61,8 @@ allKeywords =
     kwConstr,
     kwCase,
     kwOf,
+    kwMatch,
+    kwWith,
     kwIf,
     kwThen,
     kwElse,
@@ -132,6 +134,12 @@ kwCase = keyword Str.case_
 kwOf :: ParsecS r ()
 kwOf = keyword Str.of_
 
+kwMatch :: ParsecS r ()
+kwMatch = keyword Str.match_
+
+kwWith :: ParsecS r ()
+kwWith = keyword Str.with_
+
 kwIf :: ParsecS r ()
 kwIf = keyword Str.if_
 
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index 76b2729e63..1b5768af65 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -338,6 +338,12 @@ case_ = "case"
 of_ :: IsString s => s
 of_ = "of"
 
+match_ :: IsString s => s
+match_ = "match"
+
+with_ :: IsString s => s
+with_ = "with"
+
 juvixFunctionT :: IsString s => s
 juvixFunctionT = "juvix_function_t"
 

From d3d8c4e043a576f2cabc2a32ac6652b0f5e38a8f Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Mon, 12 Sep 2022 19:19:54 +0200
Subject: [PATCH 2/9] nodeSubinfos

---
 src/Juvix/Compiler/Core/Extra/Base.hs         | 147 +++++++++++++-----
 .../Compiler/Core/Extra/Recursors/Map.hs      |   4 +-
 .../Compiler/Core/Translation/FromSource.hs   |   2 +-
 3 files changed, 114 insertions(+), 39 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index e188925d74..d040683f31 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -163,6 +163,9 @@ unfoldLambdas = go []
 unfoldLambdas' :: Node -> (Int, Node)
 unfoldLambdas' = first length . unfoldLambdas
 
+{------------------------------------------------------------------------}
+{- functions on Pattern -}
+
 getBinderPatternInfos :: Pattern -> [Info]
 getBinderPatternInfos = go []
   where
@@ -187,120 +190,143 @@ getPatternInfos = go []
       PatWildcard (PatternWildcard {..}) ->
         _patternWildcardInfo : acc
 
+{------------------------------------------------------------------------}
+{- generic Node destruction -}
+
 -- | `NodeDetails` is a convenience datatype which provides the most commonly needed
 -- information about a node in a generic fashion.
 data NodeDetails = NodeDetails
-  { -- `nodeInfo` is the info associated with the node,
+  { -- | 'nodeInfo' is the info associated with the node,
     _nodeInfo :: Info,
-    -- `nodeChildren` are the children, in a fixed order, i.e., the immediate
+    -- | 'nodeSubinfos' contains, in a fixed order, infos other than the main
+    -- one, e.g., for a Case these are the infos associated with the branches,
+    -- for a Match the infos associated with all patterns in all branches.
+    _nodeSubinfos :: [Info],
+    -- | 'nodeChildren' are the children, in a fixed order, i.e., the immediate
     -- recursive subnodes
     _nodeChildren :: [Node],
-    -- `nodeChildBindersNum` is the number of binders introduced for each child
-    -- in the parent node. Same length and order as in `nodeChildren`.
+    -- | 'nodeChildBindersNum' is the number of binders introduced for each
+    -- child in the parent node. Same length and order as in `nodeChildren`.
     _nodeChildBindersNum :: [Int],
-    -- `nodeChildBindersInfo` is information about binders for each child, if
+    -- | 'nodeChildBindersInfo' is information about binders for each child, if
     -- present. Same length and order as in `nodeChildren`.
     _nodeChildBindersInfo :: [[Info]],
-    -- `nodeReassemble` reassembles the node from the info and the children
-    -- (which should be in the same fixed order as in the `nodeChildren`
-    -- component).
-    _nodeReassemble :: Info -> [Node] -> Node
+    -- | 'nodeReassemble' reassembles the node from the info, the subinfos and
+    -- the children (which should be in the same fixed order as in the
+    -- 'nodeSubinfos' and 'nodeChildren' component).
+    _nodeReassemble :: Info -> [Info] -> [Node] -> Node
   }
 
 makeLenses ''NodeDetails
 
--- Destruct a node into NodeDetails. This is an ugly internal function used to
+-- | Destruct a node into NodeDetails. This is an ugly internal function used to
 -- implement more high-level accessors and recursors.
 destruct :: Node -> NodeDetails
 destruct = \case
   NVar (Var i idx) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ -> mkVar i' idx
+        _nodeReassemble = \i' _ _ -> mkVar i' idx
       }
   NIdt (Ident i sym) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ -> mkIdent i' sym
+        _nodeReassemble = \i' _ _ -> mkIdent i' sym
       }
   NCst (Constant i c) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ -> mkConstant i' c
+        _nodeReassemble = \i' _ _ -> mkConstant i' c
       }
   NApp (App i l r) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = [l, r],
         _nodeChildBindersNum = [0, 0],
         _nodeChildBindersInfo = [[], []],
-        _nodeReassemble = \i' args' -> mkApp i' (hd args') (args' !! 1)
+        _nodeReassemble = \i' _ args' -> mkApp i' (hd args') (args' !! 1)
       }
   NBlt (BuiltinApp i op args) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = args,
         _nodeChildBindersNum = map (const 0) args,
         _nodeChildBindersInfo = map (const []) args,
-        _nodeReassemble = (`mkBuiltinApp` op)
+        _nodeReassemble = \i' _ args' -> mkBuiltinApp i' op args'
       }
   NCtr (Constr i tag args) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = args,
         _nodeChildBindersNum = map (const 0) args,
         _nodeChildBindersInfo = map (const []) args,
-        _nodeReassemble = (`mkConstr` tag)
+        _nodeReassemble = \i' _ args' -> mkConstr i' tag args'
       }
   NLam (Lambda i b) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = [b],
         _nodeChildBindersNum = [1],
         _nodeChildBindersInfo = [fetchBinderInfo i],
-        _nodeReassemble = \i' args' -> mkLambda i' (hd args')
+        _nodeReassemble = \i' _ args' -> mkLambda i' (hd args')
       }
   NLet (Let i v b) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = [v, b],
         _nodeChildBindersNum = [0, 1],
         _nodeChildBindersInfo = [[], fetchBinderInfo i],
-        _nodeReassemble = \i' args' -> mkLet i' (hd args') (args' !! 1)
+        _nodeReassemble = \i' _ args' -> mkLet i' (hd args') (args' !! 1)
       }
   NRec (LetRec i vs b) ->
     let n = length vs
      in NodeDetails
           { _nodeInfo = i,
+            _nodeSubinfos = [],
             _nodeChildren = b : toList vs,
             _nodeChildBindersNum = replicate (n + 1) n,
             _nodeChildBindersInfo = replicate (n + 1) (getInfoBinders n i),
-            _nodeReassemble = \i' args' -> mkLetRec i' (fromList (tl args')) (hd args')
+            _nodeReassemble = \i' _ args' -> mkLetRec i' (fromList (tl args')) (hd args')
           }
   NCase (Case i v bs Nothing) ->
     let branchBinderNums = map (^. caseBranchBindersNum) bs
         branchBinderInfos = map (\(CaseBranch {..}) -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
      in NodeDetails
           { _nodeInfo = i,
+            _nodeSubinfos = map (^. caseBranchInfo) bs,
             _nodeChildren = v : map (^. caseBranchBody) bs,
             _nodeChildBindersNum = 0 : branchBinderNums,
             _nodeChildBindersInfo = [] : branchBinderInfos,
-            _nodeReassemble = \i' args' ->
+            _nodeReassemble = \i' is' args' ->
               mkCase
                 i'
                 (hd args')
-                ( zipWithExact
-                    (\br body' -> br {_caseBranchBody = body'})
+                ( zipWith3Exact
+                    ( \br is body' ->
+                        br
+                          { _caseBranchInfo = is,
+                            _caseBranchBody = body'
+                          }
+                    )
                     bs
+                    is'
                     (tl args')
                 )
                 Nothing
@@ -310,16 +336,23 @@ destruct = \case
         branchBinderInfos = map (\(CaseBranch {..}) -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
      in NodeDetails
           { _nodeInfo = i,
+            _nodeSubinfos = map (^. caseBranchInfo) bs,
             _nodeChildren = v : def : map (^. caseBranchBody) bs,
             _nodeChildBindersNum = 0 : 0 : branchBinderNums,
             _nodeChildBindersInfo = [] : [] : branchBinderInfos,
-            _nodeReassemble = \i' args' ->
+            _nodeReassemble = \i' is' args' ->
               mkCase
                 i'
                 (hd args')
-                ( zipWithExact
-                    (\br body' -> br {_caseBranchBody = body'})
+                ( zipWith3Exact
+                    ( \br is body' ->
+                        br
+                          { _caseBranchInfo = is,
+                            _caseBranchBody = body'
+                          }
+                    )
                     bs
+                    is'
                     (tl (tl args'))
                 )
                 (Just (hd (tl args')))
@@ -334,18 +367,33 @@ destruct = \case
             )
             bs
         branchBinderNums = map length branchBinderInfos
+        branchPatternInfos =
+          concatMap
+            ( \br ->
+                concatMap
+                  (reverse . getPatternInfos)
+                  (br ^. matchBranchPatterns)
+            )
+            bs
         n = length vs
      in NodeDetails
           { _nodeInfo = i,
+            _nodeSubinfos = branchPatternInfos,
             _nodeChildren = toList vs ++ map (^. matchBranchBody) bs,
             _nodeChildBindersNum = replicate n 0 ++ branchBinderNums,
             _nodeChildBindersInfo = replicate n [] ++ branchBinderInfos,
-            _nodeReassemble = \i' args' ->
+            _nodeReassemble = \i' is' args' ->
               mkMatch
                 i'
                 (fromList $ List.take n args')
                 ( zipWithExact
-                    (\br body' -> br {_matchBranchBody = body'})
+                    ( \br body' ->
+                        br
+                          { _matchBranchPatterns =
+                              fromList $ setPatternsInfos is' (toList (br ^. matchBranchPatterns)),
+                            _matchBranchBody = body'
+                          }
+                    )
                     bs
                     (drop n args')
                 )
@@ -353,55 +401,81 @@ destruct = \case
   NPi (Pi i ty b) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = [ty, b],
         _nodeChildBindersNum = [0, 1],
         _nodeChildBindersInfo = [[], fetchBinderInfo i],
-        _nodeReassemble = \i' args' -> mkPi i' (hd args') (args' !! 1)
+        _nodeReassemble = \i' _ args' -> mkPi i' (hd args') (args' !! 1)
       }
   NUniv (Univ i l) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ -> mkUniv i' l
+        _nodeReassemble = \i' _ _ -> mkUniv i' l
       }
   NTyp (TypeConstr i sym args) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = args,
         _nodeChildBindersNum = map (const 0) args,
         _nodeChildBindersInfo = map (const []) args,
-        _nodeReassemble = (`mkTypeConstr` sym)
+        _nodeReassemble = \i' _ args' -> mkTypeConstr i' sym args'
       }
   NPrim (TypePrim i prim) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ -> mkTypePrim i' prim
+        _nodeReassemble = \i' _ _ -> mkTypePrim i' prim
       }
   NDyn (Dynamic i) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ -> mkDynamic i'
+        _nodeReassemble = \i' _ _ -> mkDynamic i'
       }
   Closure env (Lambda i b) ->
     NodeDetails
       { _nodeInfo = i,
+        _nodeSubinfos = [],
         _nodeChildren = b : env,
         _nodeChildBindersNum = 1 : map (const 0) env,
         _nodeChildBindersInfo = fetchBinderInfo i : map (const []) env,
-        _nodeReassemble = \i' args' -> Closure (tl args') (Lambda i' (hd args'))
+        _nodeReassemble = \i' _ args' -> Closure (tl args') (Lambda i' (hd args'))
       }
   where
     fetchBinderInfo :: Info -> [Info]
     fetchBinderInfo i = [getInfoBinder i]
 
+    setPatternsInfos :: [Info] -> [Pattern] -> [Pattern]
+    setPatternsInfos is ps = snd $ setPatternsInfos' is ps
+
+    setPatternsInfos' :: [Info] -> [Pattern] -> ([Info], [Pattern])
+    setPatternsInfos' is [] = (is, [])
+    setPatternsInfos' is (p : ps) =
+      let (is', p') = setPatInfos is p
+          (is'', ps') = setPatternsInfos' is' ps
+       in (is'', p' : ps')
+
+    setPatInfos :: [Info] -> Pattern -> ([Info], Pattern)
+    setPatInfos is = \case
+      PatWildcard x ->
+        (tl is, PatWildcard (x {_patternWildcardInfo = hd is}))
+      PatBinder x ->
+        (tl is, PatBinder (x {_patternBinderInfo = hd is}))
+      PatConstr x ->
+        let (is', ps) = setPatternsInfos' (tl is) (x ^. patternConstrArgs)
+         in (is', PatConstr (x {_patternConstrInfo = hd is, _patternConstrArgs = ps}))
+
     hd :: [a] -> a
     hd = List.head
 
@@ -409,7 +483,7 @@ destruct = \case
     tl = List.tail
 
 reassemble :: Node -> [Node] -> Node
-reassemble n = (d ^. nodeReassemble) (d ^. nodeInfo)
+reassemble n = (d ^. nodeReassemble) (d ^. nodeInfo) (d ^. nodeSubinfos)
   where
     d = destruct n
 
@@ -429,12 +503,13 @@ schildren = map snd . filter (\p -> fst p == 0) . bchildren
 getInfo :: Node -> Info
 getInfo = (^. nodeInfo) . destruct
 
-modifyInfoM :: Applicative m => (Info -> m Info) -> Node -> m Node
+modifyInfoM :: Monad m => (Info -> m Info) -> Node -> m Node
 modifyInfoM f n =
   let ni = destruct n
    in do
         i' <- f (ni ^. nodeInfo)
-        return ((ni ^. nodeReassemble) i' (ni ^. nodeChildren))
+        is' <- mapM f (ni ^. nodeSubinfos)
+        return ((ni ^. nodeReassemble) i' is' (ni ^. nodeChildren))
 
 modifyInfo :: (Info -> Info) -> Node -> Node
 modifyInfo f n = runIdentity $ modifyInfoM (pure . f) n
diff --git a/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs b/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs
index a29aaedd31..3803647d48 100644
--- a/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs
+++ b/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs
@@ -36,7 +36,7 @@ umapG coll f = go (coll ^. cEmpty)
                   (ni ^. nodeChildren)
                   (ni ^. nodeChildBindersNum)
                   (ni ^. nodeChildBindersInfo)
-            f c ((ni ^. nodeReassemble) (ni ^. nodeInfo) ns)
+            f c ((ni ^. nodeReassemble) (ni ^. nodeInfo) (ni ^. nodeSubinfos) ns)
 
 dmapG ::
   forall c m.
@@ -61,7 +61,7 @@ dmapG coll f = go (coll ^. cEmpty)
                 (ni ^. nodeChildren)
                 (ni ^. nodeChildBindersNum)
                 (ni ^. nodeChildBindersInfo)
-          return ((ni ^. nodeReassemble) (ni ^. nodeInfo) ns)
+          return ((ni ^. nodeReassemble) (ni ^. nodeInfo) (ni ^. nodeSubinfos) ns)
       where
         goChild :: Node -> Int -> [Info] -> m Node
         goChild n'' k bis = go ((coll ^. cCollect) (k, bis) c) n''
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 6b27f55492..6ef5429ac6 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -25,7 +25,7 @@ import Text.Megaparsec qualified as P
 parseText :: InfoTable -> Text -> Either ParserError (InfoTable, Maybe Node)
 parseText = runParser "" ""
 
--- Note: only new symbols and tags that are not in the InfoTable already will be
+-- | Note: only new symbols and tags that are not in the InfoTable already will be
 -- generated during parsing, but nameIds are generated starting from 0
 -- regardless of the names already in the InfoTable
 runParser :: FilePath -> FilePath -> InfoTable -> Text -> Either ParserError (InfoTable, Maybe Node)

From ca9d56070e4c298425a864dfa3a7b191d5e179d4 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 13 Sep 2022 09:59:32 +0200
Subject: [PATCH 3/9] fix parsing

---
 src/Juvix/Compiler/Core/Pretty/Base.hs                  | 6 ++++--
 src/Juvix/Compiler/Core/Translation/FromSource.hs       | 9 ++++-----
 src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs | 4 ++++
 3 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index ce84075a0b..de12389232 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -175,7 +175,9 @@ instance PrettyCode Pattern where
     PatConstr x -> ppCode x
 
 ppPatterns :: Member (Reader Options) r => NonEmpty Pattern -> Sem r (Doc Ann)
-ppPatterns pats = mapM (ppRightExpression appFixity) pats <&> hsep
+ppPatterns pats = do
+  ps' <- mapM ppCode pats
+  return $ hsep (punctuate comma (toList ps'))
 
 instance PrettyCode Node where
   ppCode :: forall r. Member (Reader Options) r => Node -> Sem r (Doc Ann)
@@ -240,7 +242,7 @@ instance PrettyCode Node where
       vs <- mapM ppCode _matchValues
       bs <- sequence $ zipWithExact (\ps br -> ppCode br >>= \br' -> return $ ps <+> kwMapsto <+> br') pats branchBodies
       let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs
-      return $ kwMatch <+> hsep vs <+> kwWith <+> bss
+      return $ kwMatch <+> hsep (punctuate comma (toList vs)) <+> kwWith <+> bss
     NPi Pi {..} ->
       case getInfoName $ getInfoBinder _piInfo of
         Just name -> do
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 6ef5429ac6..3138b5c171 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -479,6 +479,7 @@ atom varsNum vars =
     <|> exprLetrecOne varsNum vars
     <|> exprLet varsNum vars
     <|> exprCase varsNum vars
+    <|> exprMatch varsNum vars
     <|> exprIf varsNum vars
     <|> parens (expr varsNum vars)
     <|> braces (expr varsNum vars)
@@ -739,7 +740,7 @@ exprMatch ::
   ParsecS r Node
 exprMatch varsNum vars = do
   kwMatch
-  values <- P.some (expr varsNum vars)
+  values <- P.sepBy (expr varsNum vars) kwComma
   kwWith
   braces (exprMatch' values varsNum vars)
     <|> exprMatch' values varsNum vars
@@ -762,7 +763,7 @@ matchBranch ::
   ParsecS r MatchBranch
 matchBranch patsNum varsNum vars = do
   off <- P.getOffset
-  pats <- P.some branchPattern
+  pats <- P.sepBy branchPattern kwComma
   kwMapsTo
   unless (length pats == patsNum) $
     parseFailure off "wrong number of patterns"
@@ -782,9 +783,8 @@ branchPattern ::
   ParsecS r Pattern
 branchPattern =
   wildcardPattern
-    <|> parens wildcardPattern
-    <|> parens binderOrConstrPattern
     <|> binderOrConstrPattern
+    <|> parens branchPattern
 
 wildcardPattern :: ParsecS r Pattern
 wildcardPattern = do
@@ -801,7 +801,6 @@ binderOrConstrPattern = do
     Just (IdentTag tag) -> do
       ps <- P.many branchPattern
       ci <- lift $ getConstructorInfo tag
-      kwMapsTo
       let info = setInfoName (ci ^. constructorName) Info.empty
       return $ PatConstr (PatternConstr info tag ps)
     _ -> do
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
index 4c5e93af0f..219c907336 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
@@ -69,6 +69,7 @@ allKeywords =
     kwDef,
     kwRightArrow,
     kwSemicolon,
+    kwComma,
     kwWildcard,
     kwPlus,
     kwMinus,
@@ -161,6 +162,9 @@ kwRightArrow = keyword Str.toUnicode <|> keyword Str.toAscii
 kwSemicolon :: ParsecS r ()
 kwSemicolon = keyword Str.semicolon
 
+kwComma :: ParsecS r ()
+kwComma = keyword Str.comma
+
 kwWildcard :: ParsecS r ()
 kwWildcard = keyword Str.underscore
 

From b0f529498cce94e60bee563db46c7ef28619bf41 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 13 Sep 2022 13:31:29 +0200
Subject: [PATCH 4/9] named subpatterns

---
 src/Juvix/Compiler/Core/Language/Nodes.hs     |  7 ++++---
 src/Juvix/Compiler/Core/Pretty/Base.hs        | 12 +++++++++--
 .../Compiler/Core/Translation/FromSource.hs   | 20 +++++++++++++++----
 .../Core/Translation/FromSource/Lexer.hs      |  4 ++++
 src/Juvix/Extra/Strings.hs                    |  3 +++
 src/Juvix/Parser/Lexer.hs                     |  2 +-
 6 files changed, 38 insertions(+), 10 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs
index f6df2a6e5e..127216fd87 100644
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/src/Juvix/Compiler/Core/Language/Nodes.hs
@@ -116,8 +116,9 @@ newtype PatternWildcard' i = PatternWildcard
   { _patternWildcardInfo :: i
   }
 
-newtype PatternBinder' i = PatternBinder
-  { _patternBinderInfo :: i
+data PatternBinder' i = PatternBinder
+  { _patternBinderInfo :: i,
+    _patternBinderPattern :: Pattern' i
   }
 
 data PatternConstr' i = PatternConstr
@@ -276,7 +277,7 @@ instance Eq (PatternWildcard' i) where
   _ == _ = True
 
 instance Eq (PatternBinder' i) where
-  _ == _ = True
+  (PatternBinder _ p1) == (PatternBinder _ p2) = p1 == p2
 
 instance Eq (PatternConstr' i) where
   (PatternConstr _ tag1 ps1) == (PatternConstr _ tag2 ps2) = tag1 == tag2 && ps1 == ps2
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index de12389232..06d6806b8a 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -157,10 +157,15 @@ instance PrettyCode PatternWildcard where
   ppCode _ = return kwWildcard
 
 instance PrettyCode PatternBinder where
-  ppCode PatternBinder {..} =
-    case getInfoName _patternBinderInfo of
+  ppCode PatternBinder {..} = do
+    n <- case getInfoName _patternBinderInfo of
       Just name -> ppCode name
       Nothing -> return kwQuestion
+    case _patternBinderPattern of
+      PatWildcard {} -> return n
+      _ -> do
+        pat <- ppRightExpression appFixity _patternBinderPattern
+        return $ n <> kwAt <> pat
 
 instance PrettyCode PatternConstr where
   ppCode PatternConstr {..} = do
@@ -367,6 +372,9 @@ ppLRExpression associates fixlr e =
 {--------------------------------------------------------------------------------}
 {- keywords -}
 
+kwAt :: Doc Ann
+kwAt = delimiter "@"
+
 kwSquareL :: Doc Ann
 kwSquareL = delimiter "["
 
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 3138b5c171..dea49648ad 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -783,7 +783,7 @@ branchPattern ::
   ParsecS r Pattern
 branchPattern =
   wildcardPattern
-    <|> binderOrConstrPattern
+    <|> binderOrConstrPattern True
     <|> parens branchPattern
 
 wildcardPattern :: ParsecS r Pattern
@@ -793,16 +793,28 @@ wildcardPattern = do
 
 binderOrConstrPattern ::
   Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Bool ->
   ParsecS r Pattern
-binderOrConstrPattern = do
+binderOrConstrPattern parseArgs = do
   (txt, i) <- identifierL
   r <- lift (getIdent txt)
   case r of
     Just (IdentTag tag) -> do
-      ps <- P.many branchPattern
+      ps <- if parseArgs then P.many branchPattern else return []
       ci <- lift $ getConstructorInfo tag
       let info = setInfoName (ci ^. constructorName) Info.empty
       return $ PatConstr (PatternConstr info tag ps)
     _ -> do
       n <- lift $ freshName KNameLocal txt i
-      return $ PatBinder (PatternBinder (setInfoName n Info.empty))
+      mp <- optional binderPattern
+      let pat = fromMaybe (PatWildcard (PatternWildcard Info.empty)) mp
+      return $ PatBinder (PatternBinder (setInfoName n Info.empty) pat)
+
+binderPattern ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r Pattern
+binderPattern = do
+  kwAt
+  wildcardPattern
+    <|> binderOrConstrPattern False
+    <|> parens branchPattern
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
index 219c907336..d5fe9a7e4c 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
@@ -54,6 +54,7 @@ allKeywords :: [ParsecS r ()]
 allKeywords =
   [ kwAssign,
     kwColon,
+    kwAt,
     kwLambda,
     kwLet,
     kwLetRec,
@@ -168,6 +169,9 @@ kwComma = keyword Str.comma
 kwWildcard :: ParsecS r ()
 kwWildcard = keyword Str.underscore
 
+kwAt :: ParsecS r ()
+kwAt = keyword Str.at_
+
 kwPlus :: ParsecS r ()
 kwPlus = keyword Str.plus
 
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index 1b5768af65..3abd73a7a3 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -200,6 +200,9 @@ semicolon = ";"
 underscore :: IsString s => s
 underscore = "_"
 
+at_ :: IsString s => s
+at_ = "@"
+
 colon :: IsString s => s
 colon = ":"
 
diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs
index 4e900c96dd..09d910dd02 100644
--- a/src/Juvix/Parser/Lexer.hs
+++ b/src/Juvix/Parser/Lexer.hs
@@ -100,7 +100,7 @@ delimiterSymbols :: [Char]
 delimiterSymbols = ","
 
 reservedSymbols :: [Char]
-reservedSymbols = "\";(){}[].≔λ\\"
+reservedSymbols = "@\";(){}[].≔λ\\"
 
 validFirstChar :: Char -> Bool
 validFirstChar c = not (isNumber c || isSpace c || (c `elem` reservedSymbols))

From 67058260cb207ebc0970a2e04eff42970c0f847e Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 13 Sep 2022 14:23:00 +0200
Subject: [PATCH 5/9] fix parsing and printing

---
 src/Juvix/Compiler/Core/Language/Nodes.hs     |  4 +++-
 src/Juvix/Compiler/Core/Pretty/Base.hs        |  2 +-
 .../Compiler/Core/Translation/FromSource.hs   |  8 +++++--
 .../Core/Translation/FromSource/Lexer.hs      | 24 +++++--------------
 src/Juvix/Parser/Lexer.hs                     |  6 -----
 5 files changed, 16 insertions(+), 28 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs
index 127216fd87..1a3607a004 100644
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/src/Juvix/Compiler/Core/Language/Nodes.hs
@@ -205,7 +205,9 @@ instance HasAtomicity (PatternBinder' i) where
   atomicity _ = Atom
 
 instance HasAtomicity (PatternConstr' i) where
-  atomicity _ = Aggregate appFixity
+  atomicity PatternConstr {..}
+    | null _patternConstrArgs = Atom
+    | otherwise = Aggregate appFixity
 
 instance HasAtomicity (Pattern' i) where
   atomicity = \case
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 06d6806b8a..3a68fc5632 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -171,7 +171,7 @@ instance PrettyCode PatternConstr where
   ppCode PatternConstr {..} = do
     n <- maybe (ppCode _patternConstrTag) ppCode (getInfoName _patternConstrInfo)
     args <- mapM (ppRightExpression appFixity) _patternConstrArgs
-    return $ n <+> hsep args
+    return $ foldl' (<+>) n args
 
 instance PrettyCode Pattern where
   ppCode = \case
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index dea49648ad..fba1f2230c 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -544,7 +544,7 @@ exprLambda ::
   HashMap Text Index ->
   ParsecS r Node
 exprLambda varsNum vars = do
-  kwLambda
+  lambda
   name <- parseLocalName
   let vars' = HashMap.insert (name ^. nameText) varsNum vars
   body <- expr (varsNum + 1) vars'
@@ -796,12 +796,16 @@ binderOrConstrPattern ::
   Bool ->
   ParsecS r Pattern
 binderOrConstrPattern parseArgs = do
+  off <- P.getOffset
   (txt, i) <- identifierL
   r <- lift (getIdent txt)
   case r of
     Just (IdentTag tag) -> do
       ps <- if parseArgs then P.many branchPattern else return []
       ci <- lift $ getConstructorInfo tag
+      when
+        (ci ^. constructorArgsNum /= length ps)
+        (parseFailure off "wrong number of constructor arguments")
       let info = setInfoName (ci ^. constructorName) Info.empty
       return $ PatConstr (PatternConstr info tag ps)
     _ -> do
@@ -814,7 +818,7 @@ binderPattern ::
   Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
   ParsecS r Pattern
 binderPattern = do
-  kwAt
+  symbolAt
   wildcardPattern
     <|> binderOrConstrPattern False
     <|> parens branchPattern
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
index d5fe9a7e4c..237ebd9153 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
@@ -37,9 +37,6 @@ string = lexemeInterval string'
 keyword :: Text -> ParsecS r ()
 keyword = keyword' space
 
-rawKeyword :: Text -> ParsecS r ()
-rawKeyword = rawKeyword' space
-
 identifier :: ParsecS r Text
 identifier = lexeme bareIdentifier
 
@@ -53,9 +50,6 @@ bareIdentifier = rawIdentifier allKeywords
 allKeywords :: [ParsecS r ()]
 allKeywords =
   [ kwAssign,
-    kwColon,
-    kwAt,
-    kwLambda,
     kwLet,
     kwLetRec,
     kwIn,
@@ -88,6 +82,12 @@ allKeywords =
     kwFail
   ]
 
+symbolAt :: ParsecS r ()
+symbolAt = symbol Str.at_
+
+lambda :: ParsecS r ()
+lambda = symbol Str.lambdaUnicode <|> symbol Str.lambdaAscii
+
 lbrace :: ParsecS r ()
 lbrace = symbol "{"
 
@@ -109,15 +109,6 @@ braces = between (symbol "{") (symbol "}")
 kwAssign :: ParsecS r ()
 kwAssign = keyword Str.assignUnicode <|> keyword Str.assignAscii
 
-kwColon :: ParsecS r ()
-kwColon = keyword Str.colon
-
-kwInductive :: ParsecS r ()
-kwInductive = keyword Str.inductive
-
-kwLambda :: ParsecS r ()
-kwLambda = rawKeyword Str.lambdaUnicode <|> rawKeyword Str.lambdaAscii
-
 kwLet :: ParsecS r ()
 kwLet = keyword Str.let_
 
@@ -169,9 +160,6 @@ kwComma = keyword Str.comma
 kwWildcard :: ParsecS r ()
 kwWildcard = keyword Str.underscore
 
-kwAt :: ParsecS r ()
-kwAt = keyword Str.at_
-
 kwPlus :: ParsecS r ()
 kwPlus = keyword Str.plus
 
diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs
index 09d910dd02..abf4fd0ac7 100644
--- a/src/Juvix/Parser/Lexer.hs
+++ b/src/Juvix/Parser/Lexer.hs
@@ -79,12 +79,6 @@ keywordL' spc kw = do
     spc
     return i
 
-rawKeyword' :: ParsecS r () -> Text -> ParsecS r ()
-rawKeyword' spc kw = do
-  P.try $ do
-    void (P.chunk kw)
-    spc
-
 rawIdentifier :: [ParsecS r ()] -> ParsecS r Text
 rawIdentifier allKeywords = do
   notFollowedBy (choice allKeywords)

From bf3954c13959f496e078c5a3007b9c69dfc53fb0 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 13 Sep 2022 14:40:04 +0200
Subject: [PATCH 6/9] fix recursors and evaluator

---
 src/Juvix/Compiler/Core/Evaluator.hs  | 6 ++++--
 src/Juvix/Compiler/Core/Extra/Base.hs | 4 ++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index ddcbb1c0eb..0faf9e2552 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -110,8 +110,10 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
             evalError "the number of patterns doesn't match the number of arguments" (substEnv env n)
 
           patmatch :: [Node] -> Node -> Pattern -> Maybe [Node]
-          patmatch acc _ PatWildcard {} = Just acc
-          patmatch acc v PatBinder {} = Just (v : acc)
+          patmatch acc _ PatWildcard {} =
+            Just acc
+          patmatch acc v (PatBinder PatternBinder {..}) =
+            patmatch (v : acc) v _patternBinderPattern
           patmatch acc (NCtr (Constr _ tag args)) (PatConstr PatternConstr {..})
             | tag == _patternConstrTag =
                 matchPatterns acc args _patternConstrArgs
diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index d040683f31..19ebbfe50a 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -174,7 +174,7 @@ getBinderPatternInfos = go []
       PatConstr (PatternConstr {..}) ->
         foldl' go acc _patternConstrArgs
       PatBinder (PatternBinder {..}) ->
-        _patternBinderInfo : acc
+        go (_patternBinderInfo : acc) _patternBinderPattern
       PatWildcard {} ->
         acc
 
@@ -186,7 +186,7 @@ getPatternInfos = go []
       PatConstr (PatternConstr {..}) ->
         foldl' go (_patternConstrInfo : acc) _patternConstrArgs
       PatBinder (PatternBinder {..}) ->
-        _patternBinderInfo : acc
+        go (_patternBinderInfo : acc) _patternBinderPattern
       PatWildcard (PatternWildcard {..}) ->
         _patternWildcardInfo : acc
 

From d7bccce7d698cefe312c5a8b9c5758d81bb27860 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 13 Sep 2022 15:19:28 +0200
Subject: [PATCH 7/9] add tests

---
 test/Core/Eval/Positive.hs          |  7 ++++-
 tests/Core/positive/out/test041.out |  7 +++++
 tests/Core/positive/test041.jvc     | 49 +++++++++++++++++++++++++++++
 3 files changed, 62 insertions(+), 1 deletion(-)
 create mode 100644 tests/Core/positive/out/test041.out
 create mode 100644 tests/Core/positive/test041.jvc

diff --git a/test/Core/Eval/Positive.hs b/test/Core/Eval/Positive.hs
index 8d6f1aad21..f689b65ea1 100644
--- a/test/Core/Eval/Positive.hs
+++ b/test/Core/Eval/Positive.hs
@@ -229,5 +229,10 @@ tests =
       "LetRec"
       "."
       "test040.jvc"
-      "out/test040.out"
+      "out/test040.out",
+    PosTest
+      "Match with complex patterns"
+      "."
+      "test041.jvc"
+      "out/test041.out"
   ]
diff --git a/tests/Core/positive/out/test041.out b/tests/Core/positive/out/test041.out
new file mode 100644
index 0000000000..2f5bb2d1ca
--- /dev/null
+++ b/tests/Core/positive/out/test041.out
@@ -0,0 +1,7 @@
+cons 9 (cons 7 (cons 5 (cons 3 (cons 1 nil))))
+-12096
+-1448007509520
+5510602057585725
+-85667472308246220
+527851146861989286336
+-441596546382859135501706333021475
diff --git a/tests/Core/positive/test041.jvc b/tests/Core/positive/test041.jvc
new file mode 100644
index 0000000000..a572db1d24
--- /dev/null
+++ b/tests/Core/positive/test041.jvc
@@ -0,0 +1,49 @@
+-- match
+
+constr cons 2;
+constr nil 0;
+
+def lgen := \n if n = 0 then nil else cons n (lgen (n - 1));
+
+def sum2 := \x {
+  match x with {
+    cons x y@(cons z _) -> cons (x + z) (sum2 y);
+    _ -> x
+  }
+};
+
+constr leaf 0;
+constr node 2;
+
+def gen := \n if n <= 0 then leaf else node (gen (n - 2)) (gen (n - 1));
+
+def g;
+
+def f := \t match t with {
+  leaf -> 1;
+  node l r ->
+    match g l, g r with {
+      leaf, leaf -> 0 - 6;
+      node l r, leaf -> (f l + f r) * 2;
+      node l1 r1, node l2 r2 -> (f l1 + f r1) * (f l2 + f r2);
+      _, node l r -> (f l + f r) * (0 - 3)
+    }
+};
+
+def g := \t {
+  match t with {
+    leaf -> t;
+    node (node _ _) r -> r;
+    node l r -> node r l;
+  }
+};
+
+def writeLn := \x write x >> write "\n";
+
+writeLn (sum2 (lgen 5)) >>
+writeLn (f (gen 10)) >>
+writeLn (f (gen 15)) >>
+writeLn (f (gen 16)) >>
+writeLn (f (gen 17)) >>
+writeLn (f (gen 18)) >>
+writeLn (f (gen 20))

From ec9b9bdbef3ecb1b75e7981349cad3dc43d3dad3 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 13 Sep 2022 15:35:19 +0200
Subject: [PATCH 8/9] minor fixes

---
 src/Juvix/Compiler/Core/Pretty/Base.hs                  | 1 -
 src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs | 5 ++++-
 src/Juvix/Parser/Lexer.hs                               | 6 ++++++
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 3a68fc5632..10712203bd 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -5,7 +5,6 @@ module Juvix.Compiler.Core.Pretty.Base
   )
 where
 
-import Data.Functor
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Data.Stripped.InfoTable qualified as Stripped
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
index 237ebd9153..49ca85d725 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
@@ -37,6 +37,9 @@ string = lexemeInterval string'
 keyword :: Text -> ParsecS r ()
 keyword = keyword' space
 
+keywordSymbol :: Text -> ParsecS r ()
+keywordSymbol = keywordSymbol' space
+
 identifier :: ParsecS r Text
 identifier = lexeme bareIdentifier
 
@@ -155,7 +158,7 @@ kwSemicolon :: ParsecS r ()
 kwSemicolon = keyword Str.semicolon
 
 kwComma :: ParsecS r ()
-kwComma = keyword Str.comma
+kwComma = keywordSymbol Str.comma
 
 kwWildcard :: ParsecS r ()
 kwWildcard = keyword Str.underscore
diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs
index abf4fd0ac7..6771f936ce 100644
--- a/src/Juvix/Parser/Lexer.hs
+++ b/src/Juvix/Parser/Lexer.hs
@@ -79,6 +79,12 @@ keywordL' spc kw = do
     spc
     return i
 
+keywordSymbol' :: ParsecS r () -> Text -> ParsecS r ()
+keywordSymbol' spc kw = do
+  P.try $ do
+    void $ P.chunk kw
+    spc
+
 rawIdentifier :: [ParsecS r ()] -> ParsecS r Text
 rawIdentifier allKeywords = do
   notFollowedBy (choice allKeywords)

From 5586f7a10c06c23ff50c17533ba67f0bbfe620fb Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 14 Sep 2022 15:15:22 +0200
Subject: [PATCH 9/9] adapt to PR #1533

---
 .../Compiler/Core/Translation/FromSource.hs   |  2 +-
 .../Core/Translation/FromSource/Lexer.hs      |  3 ---
 tests/Core/positive/test041.jvc               | 22 +++++++++----------
 3 files changed, 12 insertions(+), 15 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index fba1f2230c..78861930af 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -764,7 +764,7 @@ matchBranch ::
 matchBranch patsNum varsNum vars = do
   off <- P.getOffset
   pats <- P.sepBy branchPattern kwComma
-  kwMapsTo
+  kwAssign
   unless (length pats == patsNum) $
     parseFailure off "wrong number of patterns"
   let pis = concatMap (reverse . getBinderPatternInfos) pats
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
index 49ca85d725..e1850d5ab2 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
@@ -148,9 +148,6 @@ kwElse = keyword Str.else_
 kwDef :: ParsecS r ()
 kwDef = keyword Str.def
 
-kwMapsTo :: ParsecS r ()
-kwMapsTo = keyword Str.mapstoUnicode <|> keyword Str.mapstoAscii
-
 kwRightArrow :: ParsecS r ()
 kwRightArrow = keyword Str.toUnicode <|> keyword Str.toAscii
 
diff --git a/tests/Core/positive/test041.jvc b/tests/Core/positive/test041.jvc
index a572db1d24..f8500ce29a 100644
--- a/tests/Core/positive/test041.jvc
+++ b/tests/Core/positive/test041.jvc
@@ -7,8 +7,8 @@ def lgen := \n if n = 0 then nil else cons n (lgen (n - 1));
 
 def sum2 := \x {
   match x with {
-    cons x y@(cons z _) -> cons (x + z) (sum2 y);
-    _ -> x
+    cons x y@(cons z _) := cons (x + z) (sum2 y);
+    _ := x
   }
 };
 
@@ -20,21 +20,21 @@ def gen := \n if n <= 0 then leaf else node (gen (n - 2)) (gen (n - 1));
 def g;
 
 def f := \t match t with {
-  leaf -> 1;
-  node l r ->
+  leaf := 1;
+  node l r :=
     match g l, g r with {
-      leaf, leaf -> 0 - 6;
-      node l r, leaf -> (f l + f r) * 2;
-      node l1 r1, node l2 r2 -> (f l1 + f r1) * (f l2 + f r2);
-      _, node l r -> (f l + f r) * (0 - 3)
+      leaf, leaf := 0 - 6;
+      node l r, leaf := (f l + f r) * 2;
+      node l1 r1, node l2 r2 := (f l1 + f r1) * (f l2 + f r2);
+      _, node l r := (f l + f r) * (0 - 3)
     }
 };
 
 def g := \t {
   match t with {
-    leaf -> t;
-    node (node _ _) r -> r;
-    node l r -> node r l;
+    leaf := t;
+    node (node _ _) r := r;
+    node l r := node r l;
   }
 };