Merge remote-tracking branch 'origin/main' into module-dependencies

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,

src/Juvix/Compiler/Concrete/Language.hs

@@ -1280,6 +1280,7 @@ data Expression
   | ExpressionPostfixApplication PostfixApplication
   | ExpressionList (List 'Scoped)
   | ExpressionCase (Case 'Scoped)
+  | ExpressionIf (If 'Scoped)
   | ExpressionNewCase (NewCase 'Scoped)
   | ExpressionLambda (Lambda 'Scoped)
   | ExpressionLet (Let 'Scoped)
@@ -1610,6 +1611,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,
@@ -1896,6 +1968,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)
@@ -2156,6 +2229,9 @@ makeLenses ''Case
 makeLenses ''CaseBranch
 makeLenses ''NewCase
 makeLenses ''NewCaseBranch
+makeLenses ''If
+makeLenses ''IfBranch
+makeLenses ''IfBranchElse
 makeLenses ''PatternBinding
 makeLenses ''PatternAtoms
 makeLenses ''ExpressionAtoms
@@ -2252,6 +2328,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
@@ -2272,6 +2349,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)
 
@@ -2368,12 +2448,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
 
@@ -2414,6 +2503,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
@@ -2784,6 +2874,7 @@ instance IsApe Expression ApeLeaf where
     ExpressionList {} -> leaf
     ExpressionCase {} -> leaf
     ExpressionNewCase {} -> leaf
+    ExpressionIf {} -> leaf
     ExpressionLambda {} -> leaf
     ExpressionLet {} -> leaf
     ExpressionUniverse {} -> leaf

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

@@ -345,6 +345,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
@@ -548,6 +549,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)
 
@@ -655,6 +673,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))
 
@@ -790,6 +819,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

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -1980,6 +1980,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 ->
@@ -2191,6 +2233,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
@@ -2732,6 +2775,7 @@ parseTerm =
     <|> parseLambda
     <|> parseCase
     <|> parseNewCase
+    <|> parseIf
     <|> parseList
     <|> parseLiteral
     <|> parseLet
@@ -2789,11 +2833,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
 

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

@@ -826,6 +826,7 @@ expressionAtom =
       <|> AtomNamedApplicationNew <$> namedApplicationNew
       <|> AtomNamedApplication <$> namedApplication
       <|> AtomList <$> parseList
+      <|> either AtomIf AtomIdentifier <$> multiwayIf
       <|> AtomIdentifier <$> name
       <|> AtomUniverse <$> universe
       <|> AtomLambda <$> lambda
@@ -1144,6 +1145,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
 --------------------------------------------------------------------------------