Remove the 'match' keyword (#238)

Remove the 'match' keyword (#215)

Since lambda-expressions will support pattern matching, explicit 'match' is redundant.

src/MiniJuvix/Internal/Strings.hs

@@ -50,9 +50,6 @@ infixl_ = "infixl"
 infixr_ :: IsString s => s
 infixr_ = "infixr"
 
-match :: IsString s => s
-match = "match"
-
 open :: IsString s => s
 open = "open"
 

src/MiniJuvix/Syntax/Abstract/Language.hs

@@ -98,7 +98,6 @@ data Expression
   | ExpressionFunction Function
   | ExpressionLiteral LiteralLoc
   | ExpressionHole Hole
-  --- | ExpressionMatch Match
   ---  ExpressionLambda Lambda not supported yet
   deriving stock (Eq, Show)
 
@@ -111,18 +110,6 @@ instance HasAtomicity Expression where
     ExpressionFunction f -> atomicity f
     ExpressionLiteral f -> atomicity f
 
-data Match = Match
-  { _matchExpression :: Expression,
-    _matchAlts :: [MatchAlt]
-  }
-  deriving stock (Eq, Show)
-
-data MatchAlt = MatchAlt
-  { _matchAltPattern :: Pattern,
-    _matchAltBody :: Expression
-  }
-  deriving stock (Eq, Show)
-
 data Application = Application
   { _appLeft :: Expression,
     _appRight :: Expression,

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -549,7 +549,6 @@ data Expression
   | ExpressionInfixApplication InfixApplication
   | ExpressionPostfixApplication PostfixApplication
   | ExpressionLambda (Lambda 'Scoped)
-  | ExpressionMatch (Match 'Scoped)
   | ExpressionLetBlock (LetBlock 'Scoped)
   | ExpressionUniverse Universe
   | ExpressionLiteral LiteralLoc
@@ -568,62 +567,11 @@ instance HasAtomicity Expression where
     ExpressionPostfixApplication a -> Aggregate (getFixity a)
     ExpressionLambda {} -> Atom
     ExpressionLiteral {} -> Atom
-    ExpressionMatch {} -> Atom
     ExpressionLetBlock {} -> Atom
     ExpressionBraces {} -> Atom
     ExpressionUniverse {} -> Atom
     ExpressionFunction {} -> Aggregate funFixity
 
---------------------------------------------------------------------------------
--- Match expression
---------------------------------------------------------------------------------
-
-data MatchAlt (s :: Stage) = MatchAlt
-  { matchAltPattern :: PatternType s,
-    matchAltBody :: ExpressionType s
-  }
-
-deriving stock instance
-  ( Show (ExpressionType s),
-    Show (PatternType s)
-  ) =>
-  Show (MatchAlt s)
-
-deriving stock instance
-  ( Eq (ExpressionType s),
-    Eq (PatternType s)
-  ) =>
-  Eq (MatchAlt s)
-
-deriving stock instance
-  ( Ord (ExpressionType s),
-    Ord (PatternType s)
-  ) =>
-  Ord (MatchAlt s)
-
-data Match (s :: Stage) = Match
-  { matchExpression :: ExpressionType s,
-    matchAlts :: [MatchAlt s]
-  }
-
-deriving stock instance
-  ( Show (ExpressionType s),
-    Show (PatternType s)
-  ) =>
-  Show (Match s)
-
-deriving stock instance
-  ( Eq (ExpressionType s),
-    Eq (PatternType s)
-  ) =>
-  Eq (Match s)
-
-deriving stock instance
-  ( Ord (ExpressionType s),
-    Ord (PatternType s)
-  ) =>
-  Ord (Match s)
-
 --------------------------------------------------------------------------------
 -- Function expression
 --------------------------------------------------------------------------------
@@ -933,7 +881,6 @@ data ExpressionAtom (s :: Stage)
   | AtomUniverse Universe
   | AtomFunction (Function s)
   | AtomFunArrow
-  | AtomMatch (Match s)
   | AtomLiteral LiteralLoc
   | AtomParens (ExpressionType s)
 

src/MiniJuvix/Syntax/Concrete/Lexer.hs

@@ -161,7 +161,6 @@ allKeywords =
     kwLambda,
     kwLet,
     kwMapsTo,
-    kwMatch,
     kwModule,
     kwOpen,
     kwPostfix,
@@ -256,9 +255,6 @@ kwLet = keyword Str.let_
 kwMapsTo :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
 kwMapsTo = keyword Str.mapstoUnicode <|> keyword Str.mapstoAscii
 
-kwMatch :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
-kwMatch = keyword Str.match
-
 kwModule :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
 kwModule = keyword Str.module_
 

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -237,13 +237,11 @@ expressionAtom =
     <|> (AtomUniverse <$> universe)
     <|> (AtomLambda <$> lambda)
     <|> (AtomFunction <$> function)
-    <|> (AtomMatch <$> match)
     <|> (AtomLetBlock <$> letBlock)
     <|> (AtomFunArrow <$ kwRightArrow)
     <|> (AtomHole <$> hole)
     <|> parens (AtomParens <$> parseExpressionAtoms)
-    -- TODO: revise this try. Necessary to avoid confusion with match
-    <|> P.try (braces (AtomBraces <$> withLoc parseExpressionAtoms))
+    <|> (braces (AtomBraces <$> withLoc parseExpressionAtoms))
 
 parseExpressionAtoms ::
   Members '[Reader ParserParams, InfoTableBuilder] r =>
@@ -280,24 +278,6 @@ literal = do
       <|> literalString
   P.lift (registerLiteral l)
 
---------------------------------------------------------------------------------
--- Match expression
---------------------------------------------------------------------------------
-
-matchAlt :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (MatchAlt 'Parsed)
-matchAlt = do
-  matchAltPattern <- patternAtom
-  kwMapsTo
-  matchAltBody <- parseExpressionAtoms
-  return MatchAlt {..}
-
-match :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Match 'Parsed)
-match = do
-  kwMatch
-  matchExpression <- parseExpressionAtoms
-  matchAlts <- braces (P.sepEndBy matchAlt kwSemicolon)
-  return Match {..}
-
 --------------------------------------------------------------------------------
 -- Let expression
 --------------------------------------------------------------------------------

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -61,9 +61,6 @@ kwColon = keyword Str.colon
 kwArrowR :: Doc Ann
 kwArrowR = keyword Str.toUnicode
 
-kwMatch :: Doc Ann
-kwMatch = keyword Str.match
-
 kwLambda :: Doc Ann
 kwLambda = keyword Str.lambdaUnicode
 
@@ -602,18 +599,6 @@ instance SingI s => PrettyCode (LetClause s) where
 ppBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
 ppBlock items = mapM (fmap endSemicolon . ppCode) items >>= bracesIndent . vsep . toList
 
-instance SingI s => PrettyCode (MatchAlt s) where
-  ppCode MatchAlt {..} = do
-    matchAltPattern' <- ppPatternAtom matchAltPattern
-    matchAltBody' <- ppExpression matchAltBody
-    return $ matchAltPattern' <+> kwMapsto <+> matchAltBody'
-
-instance SingI s => PrettyCode (Match s) where
-  ppCode Match {..} = do
-    matchExpression' <- ppExpression matchExpression
-    matchAlts' <- ppBlock matchAlts
-    return $ kwMatch <+> matchExpression' <+> matchAlts'
-
 instance SingI s => PrettyCode (LambdaClause s) where
   ppCode LambdaClause {..} = do
     lambdaParameters' <- hsep . toList <$> mapM ppPatternAtom lambdaParameters
@@ -775,7 +760,6 @@ instance PrettyCode Expression where
     ExpressionInfixApplication a -> ppCode a
     ExpressionPostfixApplication a -> ppCode a
     ExpressionLambda l -> ppCode l
-    ExpressionMatch m -> ppCode m
     ExpressionLetBlock lb -> ppCode lb
     ExpressionUniverse u -> ppCode u
     ExpressionLiteral l -> ppCode l
@@ -867,7 +851,6 @@ instance SingI s => PrettyCode (ExpressionAtom s) where
     AtomFunction fun -> ppCode fun
     AtomLiteral lit -> ppCode lit
     AtomFunArrow -> return kwArrowR
-    AtomMatch m -> ppCode m
     AtomParens e -> parens <$> ppExpression e
     AtomBraces e -> braces <$> ppExpression (e ^. withLocParam)
     AtomHole w -> ppHole w

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -1151,7 +1151,6 @@ checkExpressionAtom e = case e of
   AtomFunArrow -> return AtomFunArrow
   AtomHole h -> AtomHole <$> checkHole h
   AtomLiteral l -> return (AtomLiteral l)
-  AtomMatch match -> AtomMatch <$> checkMatch match
 
 checkHole ::
   Members '[NameIdGen] r =>
@@ -1176,32 +1175,6 @@ checkParens e@(ExpressionAtoms as _) = case as of
     return (ExpressionParensIdentifier scopedIdenNoFix)
   _ -> checkParseExpressionAtoms e
 
-checkMatchAlt ::
-  Members '[Error ScoperError, State Scope, Reader LocalVars, State ScoperState, InfoTableBuilder, NameIdGen] r =>
-  MatchAlt 'Parsed ->
-  Sem r (MatchAlt 'Scoped)
-checkMatchAlt MatchAlt {..} = do
-  matchAltPattern' <- checkParsePatternAtom matchAltPattern
-  matchAltBody' <- withBindCurrentGroup (checkParseExpressionAtoms matchAltBody)
-  return
-    MatchAlt
-      { matchAltPattern = matchAltPattern',
-        matchAltBody = matchAltBody'
-      }
-
-checkMatch ::
-  Members '[Error ScoperError, State Scope, Reader LocalVars, State ScoperState, InfoTableBuilder, NameIdGen] r =>
-  Match 'Parsed ->
-  Sem r (Match 'Scoped)
-checkMatch Match {..} = do
-  matchExpression' <- checkParseExpressionAtoms matchExpression
-  matchAlts' <- mapM checkMatchAlt matchAlts
-  return
-    Match
-      { matchExpression = matchExpression',
-        matchAlts = matchAlts'
-      }
-
 checkExpressionAtoms ::
   Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
   ExpressionAtoms 'Parsed ->
@@ -1362,7 +1335,6 @@ parseTerm =
       <|> parseFunction
       <|> parseLambda
       <|> parseLiteral
-      <|> parseMatch
       <|> parseLetBlock
       <|> parseBraces
   where
@@ -1390,14 +1362,6 @@ parseTerm =
           AtomLambda l -> Just l
           _ -> Nothing
 
-    parseMatch :: Parse Expression
-    parseMatch = ExpressionMatch <$> P.token match mempty
-      where
-        match :: ExpressionAtom 'Scoped -> Maybe (Match 'Scoped)
-        match s = case s of
-          AtomMatch l -> Just l
-          _ -> Nothing
-
     parseUniverse :: Parse Expression
     parseUniverse = ExpressionUniverse <$> P.token universe' mempty
       where

src/MiniJuvix/Translation/ScopedToAbstract.hs

@@ -276,7 +276,6 @@ goExpression = \case
   ExpressionLiteral l -> return (Abstract.ExpressionLiteral l)
   ExpressionLambda {} -> unsupported "Lambda"
   ExpressionBraces b -> throw (ErrAppLeftImplicit (AppLeftImplicit b))
-  ExpressionMatch {} -> unsupported "Match"
   ExpressionLetBlock {} -> unsupported "Let Block"
   ExpressionUniverse uni -> return (Abstract.ExpressionUniverse (goUniverse uni))
   ExpressionFunction func -> Abstract.ExpressionFunction <$> goFunction func

tests/positive/StdlibList/Data/List.mjuvix

@@ -9,6 +9,9 @@ inductive List (a : Type) {
   ∷ : a → List a → List a;
 };
 
+match : {A : Type} → {B : Type} → A → (A → B) → B;
+match x f ≔ f x;
+
 foldr : (a : Type) → (b : Type) → (a → b → b) → b → List a → b;
 foldr _ _ _ z (nil _) ≔ z;
 foldr a b f z (∷ _ h hs) ≔ f h (foldr a b f z hs);
@@ -23,7 +26,7 @@ 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 {
+filter a f (∷ _ h hs) ≔ match (f h) λ{
   true ↦ ∷ a h (filter a f hs);
   false ↦ filter a f hs;
 };
@@ -61,12 +64,12 @@ 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 {
+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 {
+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);
   };
@@ -86,7 +89,7 @@ quickSort a cmp (∷ _ x ys) ≔
   (++ a (∷ a x (nil a)) (quickSort a (filter a gex) ys))
   where {
     ltx : a → Bool;
-    ltx y ≔ match cmp y x {
+    ltx y ≔ match (cmp y x) λ{
       LT ↦ true;
       _ ↦ false;
     };