Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Multiway if syntax #2770

Merged
merged 7 commits into from
May 8, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion src/Juvix/Compiler/Concrete/Keywords.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,6 @@ import Juvix.Data.Keyword.All
delimParenR,
delimSemicolon,
-- keywords

kwAbove,
kwAlias,
kwAs,
Expand All @@ -37,11 +36,13 @@ import Juvix.Data.Keyword.All
kwCase,
kwCoercion,
kwColon,
kwElse,
kwEnd,
kwEq,
kwFixity,
kwHiding,
kwHole,
kwIf,
kwImport,
kwIn,
kwInductive,
Expand Down Expand Up @@ -87,6 +88,7 @@ reservedKeywords =
kwAxiom,
kwCase,
kwColon,
kwElse,
kwEnd,
kwHiding,
kwHole,
Expand Down
91 changes: 91 additions & 0 deletions src/Juvix/Compiler/Concrete/Language.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -2151,6 +2224,9 @@ makeLenses ''Case
makeLenses ''CaseBranch
makeLenses ''NewCase
makeLenses ''NewCaseBranch
makeLenses ''If
makeLenses ''IfBranch
makeLenses ''IfBranchElse
makeLenses ''PatternBinding
makeLenses ''PatternAtoms
makeLenses ''ExpressionAtoms
Expand Down Expand Up @@ -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
Expand All @@ -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)

Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -2779,6 +2869,7 @@ instance IsApe Expression ApeLeaf where
ExpressionList {} -> leaf
ExpressionCase {} -> leaf
ExpressionNewCase {} -> leaf
ExpressionIf {} -> leaf
ExpressionLambda {} -> leaf
ExpressionLet {} -> leaf
ExpressionUniverse {} -> leaf
Expand Down
30 changes: 30 additions & 0 deletions src/Juvix/Compiler/Concrete/Print/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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))

Expand Down Expand Up @@ -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))

Expand Down Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -2724,6 +2767,7 @@ parseTerm =
<|> parseLambda
<|> parseCase
<|> parseNewCase
<|> parseIf
<|> parseList
<|> parseLiteral
<|> parseLet
Expand Down Expand Up @@ -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

Expand Down
39 changes: 39 additions & 0 deletions src/Juvix/Compiler/Concrete/Translation/FromSource.hs
Original file line number Diff line number Diff line change
Expand Up @@ -864,6 +864,7 @@ expressionAtom =
<|> AtomNamedApplicationNew <$> namedApplicationNew
<|> AtomNamedApplication <$> namedApplication
<|> AtomList <$> parseList
<|> either AtomIf AtomIdentifier <$> multiwayIf
<|> AtomIdentifier <$> name
<|> AtomUniverse <$> universe
<|> AtomLambda <$> lambda
Expand Down Expand Up @@ -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
--------------------------------------------------------------------------------
Expand Down
Loading
Loading