Replace -> by := in lambda syntax (#1533)

src/Juvix/Compiler/Concrete/Pretty/Base.hs

@@ -482,7 +482,7 @@ instance SingI s => PrettyCode (LambdaClause s) where
   ppCode LambdaClause {..} = do
     lambdaParameters' <- hsep . toList <$> mapM ppPatternAtom lambdaParameters
     lambdaBody' <- ppExpression lambdaBody
-    return $ lambdaParameters' <+> kwMapsto <+> lambdaBody'
+    return $ lambdaParameters' <+> kwAssign <+> lambdaBody'
 
 instance SingI s => PrettyCode (Lambda s) where
   ppCode Lambda {..} = do

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -471,7 +471,7 @@ whereClause =
 lambdaClause :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (LambdaClause 'Parsed)
 lambdaClause = do
   lambdaParameters <- P.some patternAtom
-  kwMapsTo
+  kwAssign
   lambdaBody <- parseExpressionAtoms
   return LambdaClause {..}
 
@@ -537,7 +537,7 @@ parsePatternAtoms = do
 functionClause :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash, NameIdGen] r => Symbol -> ParsecS r (FunctionClause 'Parsed)
 functionClause _clauseOwnerFunction = do
   _clausePatterns <- P.many patternAtom
-  kwAssignment
+  kwAssign
   _clauseBody <- parseExpressionAtoms
   _clauseWhere <- optional whereBlock
   return FunctionClause {..}

src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs

@@ -93,7 +93,7 @@ dottedIdentifier = lexeme $ P.sepBy1 bareIdentifier dot
 
 allKeywords :: Members '[Reader ParserParams, InfoTableBuilder] r => [ParsecS r ()]
 allKeywords =
-  [ kwAssignment,
+  [ kwAssign,
     kwAxiom,
     kwColon,
     kwColonOmega,
@@ -112,7 +112,6 @@ allKeywords =
     kwInfixr,
     kwLambda,
     kwLet,
-    kwMapsTo,
     kwModule,
     kwOpen,
     kwPostfix,
@@ -146,8 +145,8 @@ braces = between (symbol "{") (symbol "}")
 kwBuiltin :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
 kwBuiltin = keyword Str.builtin
 
-kwAssignment :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
-kwAssignment = keyword Str.assignUnicode <|> keyword Str.assignAscii
+kwAssign :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
+kwAssign = keyword Str.assignUnicode <|> keyword Str.assignAscii
 
 kwAxiom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
 kwAxiom = keyword Str.axiom

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -143,12 +143,12 @@ ppCodeCase' branchBinderNames branchTagNames Case {..} = do
   bns <- mapM (mapM (maybe (return kwQuestion) ppCode)) branchBinderNames
   cns <- zipWithM (\tag -> maybe (ppCode tag) ppCode) branchTags branchTagNames
   v <- ppCode _caseValue
-  bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwMapsto <+> br') cns bns branchBodies
+  bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwAssign <+> br') cns bns branchBodies
   bs'' <-
     case _caseDefault of
       Just def -> do
         d' <- ppCode def
-        return $ bs' ++ [kwDefault <+> kwMapsto <+> d']
+        return $ bs' ++ [kwDefault <+> kwAssign <+> d']
       Nothing -> return bs'
   let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs''
   return $ kwCase <+> v <+> kwOf <+> bss

src/Juvix/Compiler/Core/Translation/FromSource.hs

@@ -156,7 +156,7 @@ parseDefinition ::
   Symbol ->
   ParsecS r ()
 parseDefinition sym = do
-  kwAssignment
+  kwAssign
   node <- expression
   lift $ registerIdentNode sym node
   let (is, _) = unfoldLambdas node
@@ -558,7 +558,7 @@ exprLetrecOne ::
 exprLetrecOne varsNum vars = do
   kwLetRec
   name <- parseLocalName
-  kwAssignment
+  kwAssign
   let vars' = HashMap.insert (name ^. nameText) varsNum vars
   value <- expr (varsNum + 1) vars'
   kwIn
@@ -599,7 +599,7 @@ letrecDefs names varsNum vars = case names of
     when (n /= txt) $
       parseFailure off "identifier name doesn't match letrec signature"
     name <- lift $ freshName KNameLocal txt i
-    kwAssignment
+    kwAssign
     v <- expr varsNum vars
     if
         | null names' -> optional kwSemicolon >> kwIn
@@ -615,7 +615,7 @@ letrecDef ::
 letrecDef varsNum vars = do
   (txt, i) <- identifierL
   name <- lift $ freshName KNameLocal txt i
-  kwAssignment
+  kwAssign
   v <- expr varsNum vars
   return (name, v)
 
@@ -627,7 +627,7 @@ exprLet ::
 exprLet varsNum vars = do
   kwLet
   name <- parseLocalName
-  kwAssignment
+  kwAssign
   value <- expr varsNum vars
   kwIn
   let vars' = HashMap.insert (name ^. nameText) varsNum vars
@@ -682,7 +682,7 @@ defaultBranch ::
   ParsecS r Node
 defaultBranch varsNum vars = do
   kwWildcard
-  kwMapsTo
+  kwAssign
   expr varsNum vars
 
 matchingBranch ::
@@ -704,7 +704,7 @@ matchingBranch varsNum vars = do
       when
         (ci ^. constructorArgsNum /= bindersNum)
         (parseFailure off "wrong number of constructor arguments")
-      kwMapsTo
+      kwAssign
       let vars' =
             fst $
               foldl'

src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs

@@ -52,7 +52,7 @@ bareIdentifier = rawIdentifier allKeywords
 
 allKeywords :: [ParsecS r ()]
 allKeywords =
-  [ kwAssignment,
+  [ kwAssign,
     kwColon,
     kwLambda,
     kwLet,
@@ -65,7 +65,6 @@ allKeywords =
     kwThen,
     kwElse,
     kwDef,
-    kwMapsTo,
     kwRightArrow,
     kwSemicolon,
     kwWildcard,
@@ -103,8 +102,8 @@ parens = between lparen rparen
 braces :: ParsecS r a -> ParsecS r a
 braces = between (symbol "{") (symbol "}")
 
-kwAssignment :: ParsecS r ()
-kwAssignment = keyword Str.assignUnicode <|> keyword Str.assignAscii
+kwAssign :: ParsecS r ()
+kwAssign = keyword Str.assignUnicode <|> keyword Str.assignAscii
 
 kwColon :: ParsecS r ()
 kwColon = keyword Str.colon

src/Juvix/Compiler/Internal/Pretty/Base.hs

@@ -44,7 +44,7 @@ instance PrettyCode Lambda where
   ppCode l = do
     b' <- ppCode (l ^. lambdaBody)
     v' <- ppCode (l ^. lambdaVar)
-    return $ kwLambda <+> braces (v' <+> kwMapsto <+> b')
+    return $ kwLambda <+> braces (v' <+> kwAssign <+> b')
 
 instance PrettyCode Application where
   ppCode a = do

tests/Core/benchmark/test004.jvc

@@ -7,7 +7,7 @@ def force := \f f nil;
 
 def filter := \p \s \_
   case force s of {
-    cons h t ->
+    cons h t :=
       if p h then
         cons h (filter p t)
       else
@@ -16,7 +16,7 @@ def filter := \p \s \_
 
 def nth := \n \s
   case force s of {
-    cons h t -> if n = 1 then h else nth (n - 1) t
+    cons h t := if n = 1 then h else nth (n - 1) t
   };
 
 def numbers := \n \_ cons n (numbers (n + 1));
@@ -24,7 +24,7 @@ def numbers := \n \_ cons n (numbers (n + 1));
 def indivisible := \n \x if x % n = 0 then false else true;
 def eratostenes := \s \_
   case force s of {
-    cons n t ->
+    cons n t :=
       cons n (eratostenes (filter (indivisible n) t))
   };
 def primes := eratostenes (numbers 2);

tests/Core/positive/test007.jvc

@@ -3,11 +3,11 @@
 constr nil 0;
 constr cons 2;
 
-def hd := \x case x of { cons x' _ -> x' };
-def tl := \x case x of { cons _ x' -> x' };
-def null := \x case x of { nil -> true; _ -> false };
+def hd := \x case x of { cons x' _ := x' };
+def tl := \x case x of { cons _ x' := x' };
+def null := \x case x of { nil := true; _ := false };
 
-def map := \f \x case x of { nil -> nil; cons h t -> cons (f h) (map f t) };
+def map := \f \x case x of { nil := nil; cons h t := cons (f h) (map f t) };
 def map' := \f \x if null x then nil else cons (f (hd x)) (map' f (tl x));
 
 def lst := cons 0 (cons 1 nil);

tests/Core/positive/test012.jvc

@@ -16,10 +16,10 @@ def gen := \n
     node3 (gen (n - 1)) (gen (n - 1)) (gen (n - 1));
 
 def preorder := \t case t of {
-  node1 c -> write 1 >> preorder c;
-  node2 l r -> write 2 >> preorder l >> preorder r;
-  node3 l m r -> write 3 >> preorder l >> preorder m >> preorder r;
-  leaf -> write 0;
+  node1 c := write 1 >> preorder c;
+  node2 l r := write 2 >> preorder l >> preorder r;
+  node3 l m r := write 3 >> preorder l >> preorder m >> preorder r;
+  leaf := write 0;
 };
 
 preorder (gen 3) >> write "\n" >>

tests/Core/positive/test023.jvc

@@ -3,16 +3,16 @@
 constr nil 0;
 constr cons 2;
 
-def head := \l case l of { cons h _ -> h };
-def tail := \l case l of { cons _ t -> t };
-def null := \l case l of { nil -> true; cons _ _ -> false };
-def map := \f \l case l of { nil -> nil; cons h t -> cons (f h) (map f t) };
-def foldl := \f \acc \l case l of { nil -> acc; cons h t -> foldl f (f acc h) t };
-def foldr := \f \acc \l case l of { nil -> acc; cons h t -> f h (foldr f acc t) };
+def head := \l case l of { cons h _ := h };
+def tail := \l case l of { cons _ t := t };
+def null := \l case l of { nil := true; cons _ _ := false };
+def map := \f \l case l of { nil := nil; cons h t := cons (f h) (map f t) };
+def foldl := \f \acc \l case l of { nil := acc; cons h t := foldl f (f acc h) t };
+def foldr := \f \acc \l case l of { nil := acc; cons h t := f h (foldr f acc t) };
 def filter := \f \l
   case l of {
-    nil -> nil;
-    cons h t ->
+    nil := nil;
+    cons h t :=
       if f h then
         cons h (filter f t)
       else

tests/Core/positive/test026.jvc

@@ -8,26 +8,26 @@ def gen := \n if n <= 0 then leaf else node (gen (n - 2)) (gen (n - 1));
 def g;
 
 def f := \t case t of {
-  leaf -> 1;
-  node l r ->
+  leaf := 1;
+  node l r :=
     let l := g l in
     let r := g r in
     let a := case l of {
-      leaf -> 0 - 3;
-      node l r -> f l + f r
+      leaf := 0 - 3;
+      node l r := f l + f r
     } in
     let b := case r of {
-      node l r -> f l + f r;
-      _ -> 2
+      node l r := f l + f r;
+      _ := 2
     } in
     a * b
 };
 
-def isNode := \t case t of { node _ _ -> true; _ -> false };
-def isLeaf := \t case t of { leaf -> true; _ -> false };
+def isNode := \t case t of { node _ _ := true; _ := false };
+def isLeaf := \t case t of { leaf := true; _ := false };
 
 def g := \t if isLeaf t then t else case t of {
-  node l r -> if isNode l then r else node r l
+  node l r := if isNode l then r else node r l
 };
 
 def writeLn := \x write x >> write "\n";

tests/Core/positive/test028.jvc

@@ -3,38 +3,38 @@
 constr nil 0;
 constr cons 2;
 
-def hd := \l case l of { cons x _ -> x };
-def tl := \l case l of { cons _ x -> x };
+def hd := \l case l of { cons x _ := x };
+def tl := \l case l of { cons _ x := x };
 
 def rev' := \l \acc case l of {
-  nil -> acc;
-  cons h t -> rev' t (cons h acc)
+  nil := acc;
+  cons h t := rev' t (cons h acc)
 };
 
 def rev := \l rev' l nil;
 
 constr queue 2;
 
-def fst := \q case q of { queue x _ -> x };
-def snd := \q case q of { queue _ x -> x };
+def fst := \q case q of { queue x _ := x };
+def snd := \q case q of { queue _ x := x };
 
 def front := \q hd (fst q);
 
 def pop_front := \q
   let q' := queue (tl (fst q)) (snd q) in
   case fst q' of {
-    nil -> queue (rev (snd q')) nil;
-    _ -> q'
+    nil := queue (rev (snd q')) nil;
+    _ := q'
   };
 
 def push_back := \q \x case fst q of {
-  nil -> queue (cons x nil) (snd q);
-  _ -> queue (fst q) (cons x (snd q))
+  nil := queue (cons x nil) (snd q);
+  _ := queue (fst q) (cons x (snd q))
 };
 
 def is_empty := \q case fst q of {
-  nil -> case snd q of { nil -> true; _ -> false };
-  _ -> false
+  nil := case snd q of { nil := true; _ := false };
+  _ := false
 };
 
 def empty := queue nil nil;

tests/Core/positive/test029.jvc

@@ -2,8 +2,8 @@
 
 constr pair 2;
 
-def fst := \p case p of { pair x _ -> x };
-def snd := \p case p of { pair _ x -> x };
+def fst := \p case p of { pair x _ := x };
+def snd := \p case p of { pair _ x := x };
 
 def compose := \f \g \x f (g x);
 

tests/Core/positive/test030.jvc

@@ -7,7 +7,7 @@ def force := \f f nil;
 
 def filter := \p \s \_
   case force s of {
-    cons h t ->
+    cons h t :=
       if p h then
         cons h (filter p t)
       else
@@ -19,12 +19,12 @@ def take := \n \s
     nil
   else
     case force s of {
-      cons h t -> cons h (take (n - 1) t)
+      cons h t := cons h (take (n - 1) t)
     };
 
 def nth := \n \s
   case force s of {
-    cons h t -> if n = 0 then h else nth (n - 1) t
+    cons h t := if n = 0 then h else nth (n - 1) t
   };
 
 def numbers := \n \_ cons n (numbers (n + 1));
@@ -32,7 +32,7 @@ def numbers := \n \_ cons n (numbers (n + 1));
 def indivisible := \n \x if x % n = 0 then false else true;
 def eratostenes := \s \_
   case force s of {
-    cons n t ->
+    cons n t :=
       cons n (eratostenes (filter (indivisible n) t))
   };
 def primes := eratostenes (numbers 2);

tests/Core/positive/test033.jvc

@@ -7,13 +7,13 @@ def mklst := \n if n = 0 then nil else cons n (mklst (n - 1));
 def mklst2 := \n if n = 0 then nil else cons (mklst n) (mklst2 (n - 1));
 
 def append := \xs \ys case xs of {
-  nil -> ys;
-  cons x xs' -> cons x (append xs' ys);
+  nil := ys;
+  cons x xs' := cons x (append xs' ys);
 };
 
 def flatten := \xs case xs of {
-  nil -> nil;
-  cons x xs' -> append x (flatten xs');
+  nil := nil;
+  cons x xs' := append x (flatten xs');
 };
 
 def writeLn := \x write x >> write "\n";

tests/Core/positive/test035.jvc

@@ -6,8 +6,8 @@ constr cons 2;
 constr pair 2;
 
 def length := \xs case xs of {
-  nil -> 0;
-  cons _ xs' -> length xs' + 1
+  nil := 0;
+  cons _ xs' := length xs' + 1
 };
 
 def split := \n \xs
@@ -15,18 +15,18 @@ def split := \n \xs
     pair nil xs
   else
     case xs of {
-      nil -> pair nil nil;
-      cons x xs' ->
+      nil := pair nil nil;
+      cons x xs' :=
         case split (n - 1) xs' of {
-          pair l1 l2 -> pair (cons x l1) l2
+          pair l1 l2 := pair (cons x l1) l2
         }
     };
 
 def merge := \xs \ys case xs of {
-  nil -> ys;
-  cons x xs' -> case ys of {
-    nil -> xs;
-    cons y ys' ->
+  nil := ys;
+  cons x xs' := case ys of {
+    nil := xs;
+    cons y ys' :=
       if x <= y then
         cons x (merge xs' ys)
       else
@@ -40,14 +40,14 @@ def sort := \xs
     xs
   else
     case split (length xs / 2) xs of {
-      pair l1 l2 -> merge (sort l1) (sort l2)
+      pair l1 l2 := merge (sort l1) (sort l2)
     };
 
 def uniq := \xs case xs of {
-  nil -> nil;
-  cons x xs' -> case xs' of {
-    nil -> xs;
-    cons x' _ ->
+  nil := nil;
+  cons x xs' := case xs' of {
+    nil := xs;
+    cons x' _ :=
       if x = x' then
         uniq xs'
       else
@@ -56,13 +56,13 @@ def uniq := \xs case xs of {
 };
 
 def append := \xs \ys case xs of {
-  nil -> ys;
-  cons x xs' -> cons x (append xs' ys);
+  nil := ys;
+  cons x xs' := cons x (append xs' ys);
 };
 
 def flatten := \xs case xs of {
-  nil -> nil;
-  cons x xs' -> append x (flatten xs');
+  nil := nil;
+  cons x xs' := append x (flatten xs');
 };
 
 def take := \n \xs
@@ -70,7 +70,7 @@ def take := \n \xs
     nil
   else
     case xs of {
-      cons x xs' -> cons x (take (n - 1) xs')
+      cons x xs' := cons x (take (n - 1) xs')
     };
 
 def gen := \n \f \acc if n = 0 then acc else gen (n - 1) f (cons (f n) acc);

tests/negative/BindGroupConflict/Lambda.juvix

@@ -5,6 +5,6 @@ module Lambda;
   };
 
   fst : (a : Type) → (b : Type) → Pair a b → a ;
-  fst ≔ λ { _ _ (mkPair _ _ x x) ↦ x };
+  fst ≔ λ { _ _ (mkPair _ _ x x) := x };
 
 end;

tests/positive/StdlibList/Data/List.juvix

@@ -27,8 +27,8 @@ map a b f (∷ _ h hs) ≔ ∷ a (f h) (map a b f hs);
 filter : (a : Type) → (a → Bool) → List a → List a;
 filter a f (nil _) ≔ nil a;
 filter a f (∷ _ h hs) ≔ match (f h) λ{
-  true ↦ ∷ a h (filter a f hs);
-  false ↦ filter a f hs;
+  true := ∷ a h (filter a f hs);
+  false := filter a f hs;
 };
 
 import Data.Nat;
@@ -64,14 +64,14 @@ splitAt : (a : Type) → ℕ → List a → List a;
 splitAt a _ (nil _) ≔ nil a, nil a;
 splitAt a zero xs ≔ , (List a) (List a) (nil a) xs;
 splitAt a (suc zero) (∷ _ x xs) ≔ , (List a) (List a) (∷ a x (nil a)) xs;
-splitAt a (suc (suc m)) (∷ _ x xs) ≔ match (splitAt a m xs) λ{
-    (, la _ xs' xs'') ↦ , la la (∷ a x xs') xs'';
+splitAt a (suc (suc m)) (∷ _ x xs) ≔ match (splitAt a m xs) λ {
+    (, la _ xs' xs'') := , la la (∷ a x xs') xs'';
   };
 
 merge : (a : Type) → (a → a → Ordering) → List a → List a → List a;
 merge a cmp (∷ _ x xs) (∷ _ y ys) ≔ match (cmp x y) λ{
-    LT ↦ ∷ a x (merge a cmp xs (∷ a y ys));
-    _ ↦ ∷ a y (merge a cmp (∷ a x xs) ys);
+    LT := ∷ a x (merge a cmp xs (∷ a y ys));
+    _ := ∷ a y (merge a cmp (∷ a x xs) ys);
   };
 merge _ _ (nil _) ys ≔ ys;
 merge _ _ xs (nil _) ≔ xs;
@@ -90,8 +90,8 @@ quickSort a cmp (∷ _ x ys) ≔
   where {
     ltx : a → Bool;
     ltx y ≔ match (cmp y x) λ{
-      LT ↦ true;
-      _ ↦ false;
+      LT := true;
+      _  := false;
     };
     gex : a → Bool;
     gex y ≔ not (ltx y)