diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs index 9e16059b82..530dbc4755 100644 --- a/src/Juvix/Compiler/Concrete/Keywords.hs +++ b/src/Juvix/Compiler/Concrete/Keywords.hs @@ -20,7 +20,6 @@ import Juvix.Data.Keyword.All delimParenR, delimSemicolon, -- keywords - kwAbove, kwAlias, kwAs, @@ -37,11 +36,13 @@ import Juvix.Data.Keyword.All kwCase, kwCoercion, kwColon, + kwElse, kwEnd, kwEq, kwFixity, kwHiding, kwHole, + kwIf, kwImport, kwIn, kwInductive, @@ -87,6 +88,7 @@ reservedKeywords = kwAxiom, kwCase, kwColon, + kwElse, kwEnd, kwHiding, kwHole, diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 07764a2072..c763f5fc99 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -1275,6 +1275,7 @@ data Expression | ExpressionPostfixApplication PostfixApplication | ExpressionList (List 'Scoped) | ExpressionCase (Case 'Scoped) + | ExpressionIf (If 'Scoped) | ExpressionNewCase (NewCase 'Scoped) | ExpressionLambda (Lambda 'Scoped) | ExpressionLet (Let 'Scoped) @@ -1605,6 +1606,77 @@ deriving stock instance Ord (NewCase 'Parsed) deriving stock instance Ord (NewCase 'Scoped) +data IfBranch (s :: Stage) = IfBranch + { _ifBranchPipe :: Irrelevant KeywordRef, + _ifBranchAssignKw :: Irrelevant KeywordRef, + _ifBranchCondition :: ExpressionType s, + _ifBranchExpression :: ExpressionType s + } + deriving stock (Generic) + +instance Serialize (IfBranch 'Scoped) + +instance Serialize (IfBranch 'Parsed) + +deriving stock instance Show (IfBranch 'Parsed) + +deriving stock instance Show (IfBranch 'Scoped) + +deriving stock instance Eq (IfBranch 'Parsed) + +deriving stock instance Eq (IfBranch 'Scoped) + +deriving stock instance Ord (IfBranch 'Parsed) + +deriving stock instance Ord (IfBranch 'Scoped) + +data IfBranchElse (s :: Stage) = IfBranchElse + { _ifBranchElsePipe :: Irrelevant KeywordRef, + _ifBranchElseAssignKw :: Irrelevant KeywordRef, + _ifBranchElseKw :: Irrelevant KeywordRef, + _ifBranchElseExpression :: ExpressionType s + } + deriving stock (Generic) + +instance Serialize (IfBranchElse 'Scoped) + +instance Serialize (IfBranchElse 'Parsed) + +deriving stock instance Show (IfBranchElse 'Parsed) + +deriving stock instance Show (IfBranchElse 'Scoped) + +deriving stock instance Eq (IfBranchElse 'Parsed) + +deriving stock instance Eq (IfBranchElse 'Scoped) + +deriving stock instance Ord (IfBranchElse 'Parsed) + +deriving stock instance Ord (IfBranchElse 'Scoped) + +data If (s :: Stage) = If + { _ifKw :: KeywordRef, + _ifBranches :: NonEmpty (IfBranch s), + _ifBranchElse :: IfBranchElse s + } + deriving stock (Generic) + +instance Serialize (If 'Scoped) + +instance Serialize (If 'Parsed) + +deriving stock instance Show (If 'Parsed) + +deriving stock instance Show (If 'Scoped) + +deriving stock instance Eq (If 'Parsed) + +deriving stock instance Eq (If 'Scoped) + +deriving stock instance Ord (If 'Parsed) + +deriving stock instance Ord (If 'Scoped) + data Initializer (s :: Stage) = Initializer { _initializerPattern :: PatternParensType s, _initializerAssignKw :: Irrelevant KeywordRef, @@ -1891,6 +1963,7 @@ data ExpressionAtom (s :: Stage) | AtomList (List s) | AtomCase (Case s) | AtomNewCase (NewCase s) + | AtomIf (If s) | AtomHole (HoleType s) | AtomInstanceHole (HoleType s) | AtomDoubleBraces (DoubleBracesExpression s) @@ -2151,6 +2224,9 @@ makeLenses ''Case makeLenses ''CaseBranch makeLenses ''NewCase makeLenses ''NewCaseBranch +makeLenses ''If +makeLenses ''IfBranch +makeLenses ''IfBranchElse makeLenses ''PatternBinding makeLenses ''PatternAtoms makeLenses ''ExpressionAtoms @@ -2247,6 +2323,7 @@ instance HasAtomicity Expression where ExpressionFunction {} -> Aggregate funFixity ExpressionCase c -> atomicity c ExpressionNewCase c -> atomicity c + ExpressionIf x -> atomicity x ExpressionIterator i -> atomicity i ExpressionNamedApplication i -> atomicity i ExpressionNamedApplicationNew i -> atomicity i @@ -2267,6 +2344,9 @@ instance HasAtomicity (Case s) where instance HasAtomicity (NewCase s) where atomicity = const Atom +instance HasAtomicity (If s) where + atomicity = const Atom + instance HasAtomicity (Let 'Scoped) where atomicity l = atomicity (l ^. letExpression) @@ -2363,12 +2443,21 @@ instance (SingI s) => HasLoc (NewCaseBranch s) where branchLoc :: Interval branchLoc = getLocExpressionType (c ^. newCaseBranchExpression) +instance (SingI s) => HasLoc (IfBranch s) where + getLoc c = getLoc (c ^. ifBranchPipe) <> getLocExpressionType (c ^. ifBranchExpression) + +instance (SingI s) => HasLoc (IfBranchElse s) where + getLoc c = getLoc (c ^. ifBranchElsePipe) <> getLocExpressionType (c ^. ifBranchElseExpression) + instance (SingI s) => HasLoc (Case s) where getLoc c = getLoc (c ^. caseKw) <> getLoc (c ^. caseBranches . to last) instance (SingI s) => HasLoc (NewCase s) where getLoc c = getLoc (c ^. newCaseKw) <> getLoc (c ^. newCaseBranches . to last) +instance (SingI s) => HasLoc (If s) where + getLoc c = getLoc (c ^. ifKw) <> getLoc (c ^. ifBranchElse) + instance HasLoc (List s) where getLoc List {..} = getLoc _listBracketL <> getLoc _listBracketR @@ -2409,6 +2498,7 @@ instance HasLoc Expression where ExpressionList l -> getLoc l ExpressionCase i -> getLoc i ExpressionNewCase i -> getLoc i + ExpressionIf x -> getLoc x ExpressionLet i -> getLoc i ExpressionUniverse i -> getLoc i ExpressionLiteral i -> getLoc i @@ -2779,6 +2869,7 @@ instance IsApe Expression ApeLeaf where ExpressionList {} -> leaf ExpressionCase {} -> leaf ExpressionNewCase {} -> leaf + ExpressionIf {} -> leaf ExpressionLambda {} -> leaf ExpressionLet {} -> leaf ExpressionUniverse {} -> leaf diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 79d13ae92b..812e26e415 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -342,6 +342,7 @@ instance (SingI s) => PrettyPrint (ExpressionAtom s) where AtomLet lb -> ppCode lb AtomCase c -> ppCode c AtomNewCase c -> ppCode c + AtomIf c -> ppCode c AtomList l -> ppCode l AtomUniverse uni -> ppCode uni AtomRecordUpdate u -> ppCode u @@ -545,6 +546,23 @@ instance (SingI s) => PrettyPrint (Case s) where | singleBranch = Nothing | otherwise = Just (ppCode (b ^. caseBranchPipe . unIrrelevant)) +instance (SingI s) => PrettyPrint (If s) where + ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => If s -> Sem r () + ppCode If {..} = do + ppCode _ifKw <+> hardline <> indent (vsepHard (ppIfBranch <$> _ifBranches) <> hardline <> ppIfBranchElse _ifBranchElse) + where + ppIfBranch :: IfBranch s -> Sem r () + ppIfBranch b = pipeHelper <+> ppCode b + where + pipeHelper :: Sem r () + pipeHelper = ppCode (b ^. ifBranchPipe . unIrrelevant) + + ppIfBranchElse :: IfBranchElse s -> Sem r () + ppIfBranchElse b = pipeHelper <+> ppCode b + where + pipeHelper :: Sem r () + pipeHelper = ppCode (b ^. ifBranchElsePipe . unIrrelevant) + instance PrettyPrint Universe where ppCode Universe {..} = ppCode _universeKw <+?> (noLoc <$> (pretty <$> _universeLevel)) @@ -652,6 +670,17 @@ instance (SingI s) => PrettyPrint (NewCaseBranch s) where e' = ppExpressionType _newCaseBranchExpression pat' <+> ppCode _newCaseBranchAssignKw <> oneLineOrNext e' +instance (SingI s) => PrettyPrint (IfBranch s) where + ppCode IfBranch {..} = do + let cond' = ppExpressionType _ifBranchCondition + e' = ppExpressionType _ifBranchExpression + cond' <+> ppCode _ifBranchAssignKw <> oneLineOrNext e' + +instance (SingI s) => PrettyPrint (IfBranchElse s) where + ppCode IfBranchElse {..} = do + let e' = ppExpressionType _ifBranchElseExpression + ppCode _ifBranchElseKw <+> ppCode _ifBranchElseAssignKw <> oneLineOrNext e' + ppBlock :: (PrettyPrint a, Members '[Reader Options, ExactPrint] r, Traversable t) => t a -> Sem r () ppBlock items = vsep (sepEndSemicolon (fmap ppCode items)) @@ -787,6 +816,7 @@ instance PrettyPrint Expression where ExpressionFunction f -> ppCode f ExpressionCase c -> ppCode c ExpressionNewCase c -> ppCode c + ExpressionIf c -> ppCode c ExpressionIterator i -> ppCode i ExpressionNamedApplication i -> ppCode i ExpressionNamedApplicationNew i -> ppCode i diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 6cad380484..d56587b51e 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1972,6 +1972,48 @@ checkNewCase NewCase {..} = do _newCaseOfKw } +checkIfBranch :: + forall r. + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint] r) => + IfBranch 'Parsed -> + Sem r (IfBranch 'Scoped) +checkIfBranch IfBranch {..} = withLocalScope $ do + cond' <- checkParseExpressionAtoms _ifBranchCondition + expression' <- checkParseExpressionAtoms _ifBranchExpression + return $ + IfBranch + { _ifBranchCondition = cond', + _ifBranchExpression = expression', + .. + } + +checkIfBranchElse :: + forall r. + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint] r) => + IfBranchElse 'Parsed -> + Sem r (IfBranchElse 'Scoped) +checkIfBranchElse IfBranchElse {..} = withLocalScope $ do + expression' <- checkParseExpressionAtoms _ifBranchElseExpression + return $ + IfBranchElse + { _ifBranchElseExpression = expression', + .. + } + +checkIf :: + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint] r) => + If 'Parsed -> + Sem r (If 'Scoped) +checkIf If {..} = do + ifBranches' <- mapM checkIfBranch _ifBranches + ifBranchElse' <- checkIfBranchElse _ifBranchElse + return $ + If + { _ifBranchElse = ifBranchElse', + _ifBranches = ifBranches', + _ifKw + } + checkLambda :: (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint] r) => Lambda 'Parsed -> @@ -2183,6 +2225,7 @@ checkExpressionAtom e = case e of AtomLambda lam -> pure . AtomLambda <$> checkLambda lam AtomCase c -> pure . AtomCase <$> checkCase c AtomNewCase c -> pure . AtomNewCase <$> checkNewCase c + AtomIf c -> pure . AtomIf <$> checkIf c AtomLet letBlock -> pure . AtomLet <$> checkLet letBlock AtomUniverse uni -> return (pure (AtomUniverse uni)) AtomFunction fun -> pure . AtomFunction <$> checkFunction fun @@ -2724,6 +2767,7 @@ parseTerm = <|> parseLambda <|> parseCase <|> parseNewCase + <|> parseIf <|> parseList <|> parseLiteral <|> parseLet @@ -2781,11 +2825,19 @@ parseTerm = AtomNewCase l -> Just l _ -> Nothing + parseIf :: Parse Expression + parseIf = ExpressionIf <$> P.token if_ mempty + where + if_ :: ExpressionAtom 'Scoped -> Maybe (If 'Scoped) + if_ s = case s of + AtomIf l -> Just l + _ -> Nothing + parseList :: Parse Expression - parseList = ExpressionList <$> P.token case_ mempty + parseList = ExpressionList <$> P.token list_ mempty where - case_ :: ExpressionAtom 'Scoped -> Maybe (List 'Scoped) - case_ s = case s of + list_ :: ExpressionAtom 'Scoped -> Maybe (List 'Scoped) + list_ s = case s of AtomList l -> Just l _ -> Nothing diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index b3ea193262..ac43d3e2c4 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -864,6 +864,7 @@ expressionAtom = <|> AtomNamedApplicationNew <$> namedApplicationNew <|> AtomNamedApplication <$> namedApplication <|> AtomList <$> parseList + <|> either AtomIf AtomIdentifier <$> multiwayIf <|> AtomIdentifier <$> name <|> AtomUniverse <$> universe <|> AtomLambda <$> lambda @@ -1182,6 +1183,44 @@ newCase = P.label "new case" $ do _newCaseBranches <- braces (pipeSep1 newCaseBranch) return NewCase {..} +ifBranch' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash, NameIdGen] r) => Irrelevant KeywordRef -> ParsecS r (IfBranch 'Parsed) +ifBranch' _ifBranchPipe = do + _ifBranchCondition <- parseExpressionAtoms + _ifBranchAssignKw <- Irrelevant <$> kw kwAssign + _ifBranchExpression <- parseExpressionAtoms + return IfBranch {..} + +parseIfBranchElse' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash, NameIdGen] r) => Irrelevant KeywordRef -> ParsecS r (IfBranchElse 'Parsed) +parseIfBranchElse' _ifBranchElsePipe = do + _ifBranchElseKw <- Irrelevant <$> kw kwElse + _ifBranchElseAssignKw <- Irrelevant <$> kw kwAssign + _ifBranchElseExpression <- parseExpressionAtoms + return IfBranchElse {..} + +multiwayIf' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash, NameIdGen] r) => KeywordRef -> [IfBranch 'Parsed] -> ParsecS r (If 'Parsed) +multiwayIf' _ifKw brs = do + pipeKw <- Irrelevant <$> kw kwPipe + multiwayIfBranchElse' _ifKw pipeKw brs <|> multiwayIfBranch' _ifKw pipeKw brs + +multiwayIfBranch' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash, NameIdGen] r) => KeywordRef -> Irrelevant KeywordRef -> [IfBranch 'Parsed] -> ParsecS r (If 'Parsed) +multiwayIfBranch' _ifKw pipeKw brs = do + br <- ifBranch' pipeKw + multiwayIf' _ifKw (br : brs) + +multiwayIfBranchElse' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash, NameIdGen] r) => KeywordRef -> Irrelevant KeywordRef -> [IfBranch 'Parsed] -> ParsecS r (If 'Parsed) +multiwayIfBranchElse' _ifKw pipeKw brs = do + off <- P.getOffset + _ifBranchElse <- parseIfBranchElse' pipeKw + case nonEmpty (reverse brs) of + Nothing -> parseFailure off "A multiway if must have at least one condition branch" + Just _ifBranches -> return If {..} + +multiwayIf :: (Members '[ParserResultBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Either (If 'Parsed) Name) +multiwayIf = do + _ifKw <- kw kwIf + (Left <$> multiwayIf' _ifKw []) + <|> (return $ Right $ NameUnqualified $ WithLoc (getLoc _ifKw) (_ifKw ^. keywordRefKeyword . keywordAscii)) + -------------------------------------------------------------------------------- -- Universe expression -------------------------------------------------------------------------------- diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 23e04410b7..d14b030f5c 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -721,6 +721,7 @@ goExpression = \case ExpressionApplication a -> goApplication a ExpressionCase a -> Internal.ExpressionCase <$> goCase a ExpressionNewCase a -> Internal.ExpressionCase <$> goNewCase a + ExpressionIf a -> goIf a ExpressionInfixApplication ia -> Internal.ExpressionApplication <$> goInfix ia ExpressionPostfixApplication pa -> Internal.ExpressionApplication <$> goPostfix pa ExpressionLiteral l -> return (Internal.ExpressionLiteral (goLiteral l)) @@ -930,6 +931,21 @@ goExpression = \case where loc = getLoc l + goIf :: Concrete.If 'Scoped -> Sem r Internal.Expression + goIf e@Concrete.If {..} = do + if_ <- getBuiltinName (getLoc e) BuiltinBoolIf + go if_ (toList _ifBranches) + where + go :: Internal.Name -> [Concrete.IfBranch 'Scoped] -> Sem r Internal.Expression + go if_ = \case + [] -> + goExpression (_ifBranchElse ^. Concrete.ifBranchElseExpression) + Concrete.IfBranch {..} : brs -> do + c <- goExpression _ifBranchCondition + b1 <- goExpression _ifBranchExpression + b2 <- go if_ brs + return $ if_ Internal.@@ c Internal.@@ b1 Internal.@@ b2 + goIden :: Concrete.ScopedIden -> Internal.Expression goIden x = Internal.ExpressionIden $ case getNameKind x of KNameAxiom -> Internal.IdenAxiom n' diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 2c3572a61e..4a746c019f 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -445,5 +445,10 @@ tests = "Test074: Fields" $(mkRelDir ".") $(mkRelFile "test074.juvix") - $(mkRelFile "out/test074.out") + $(mkRelFile "out/test074.out"), + posTestEval + "Test075: Multiway If" + $(mkRelDir ".") + $(mkRelFile "test075.juvix") + $(mkRelFile "out/test075.out") ] diff --git a/tests/Compilation/positive/out/test075.out b/tests/Compilation/positive/out/test075.out new file mode 100644 index 0000000000..3fbedf693b --- /dev/null +++ b/tests/Compilation/positive/out/test075.out @@ -0,0 +1 @@ +-2 diff --git a/tests/Compilation/positive/test075.juvix b/tests/Compilation/positive/test075.juvix new file mode 100644 index 0000000000..35216c5f8a --- /dev/null +++ b/tests/Compilation/positive/test075.juvix @@ -0,0 +1,28 @@ +-- Test075: Multiway If +module test075; + +import Stdlib.Data.Field open; + +type Point := + mkPoint { + x : Field; + y : Field + }; + +f : Point -> Point -> Point + | p@(mkPoint x1 y1) q@(mkPoint x2 y2) := + if + | y1 == 0 := q + | y2 == 0 := p + | x1 == x2 := + if + | y1 == y2 := p + | else := mkPoint 0 0 + | else := + let + slope := (y1 - y2) / (x1 - x2); + r_x := slope * slope - x1 - x2; + r_y := slope * (x1 - r_x) - y1; + in mkPoint r_x r_y; + +main : Field := Point.x (f (mkPoint 2 3) (mkPoint 4 7));