From d08bf942b6ae56e288288adafc2721f7ab033542 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 4 Jul 2024 01:16:30 +0200 Subject: [PATCH] Add front-end support for case expressions boolean side conditions (#2852) - Syntax for #2804. - :warning: Depends on #2869. This pr introduces: 1. front-end support (parsing, printing, typechecking) for boolean side conditions for branches of case expressions. 2. Now `if` is a reserved keyword. 3. Multiway `if` is allowed to have only the `else` branch. I've also refactored the parser to be simpler. Example: ``` multiCaseBr : Nat := case 1 of | zero | if 0 < 0 := 3 | else := 4 | suc (suc n) | if 0 < 0 := 3 | else := n | suc n if 0 < 0 := 3; ``` The side if branches must satisfy the following. 1. There must be at least one `if` branch. 4. The `else` branch is optional. If present, it must be the last. Future work: 1. Translate side if conditions to Core and extend the exhaustiveness algorithm. 5. Add side if conditions to function clauses. --- .../Compiler/Backend/Rust/Pretty/Keywords.hs | 3 - .../Backend/VampIR/Pretty/Keywords.hs | 3 - .../Compiler/Concrete/Data/IfBranchKind.hs | 17 ++ src/Juvix/Compiler/Concrete/Keywords.hs | 1 + src/Juvix/Compiler/Concrete/Language.hs | 228 +++++++++++++++--- src/Juvix/Compiler/Concrete/Print/Base.hs | 90 +++++-- .../FromParsed/Analysis/Scoping.hs | 123 ++++++++-- .../Concrete/Translation/FromSource.hs | 107 +++++--- src/Juvix/Compiler/Core/Pretty/Base.hs | 3 - .../Compiler/Core/Translation/FromInternal.hs | 28 ++- src/Juvix/Compiler/Internal/Extra/Base.hs | 19 +- src/Juvix/Compiler/Internal/Extra/Clonable.hs | 29 ++- .../Internal/Extra/DependencyBuilder.hs | 32 ++- .../Compiler/Internal/Extra/HasLetDefs.hs | 18 +- src/Juvix/Compiler/Internal/Language.hs | 57 ++++- src/Juvix/Compiler/Internal/Pretty/Base.hs | 29 ++- .../Internal/Translation/FromConcrete.hs | 59 ++++- .../Analysis/Positivity/Checker.hs | 45 +++- .../Analysis/Termination/Checker.hs | 26 +- .../Analysis/TypeChecking/CheckerNew.hs | 124 ++++++++-- src/Juvix/Data/CodeAnn.hs | 3 + src/Juvix/Prelude/Base/Foundation.hs | 8 + tests/positive/Format.juvix | 19 ++ 23 files changed, 892 insertions(+), 179 deletions(-) create mode 100644 src/Juvix/Compiler/Concrete/Data/IfBranchKind.hs diff --git a/src/Juvix/Compiler/Backend/Rust/Pretty/Keywords.hs b/src/Juvix/Compiler/Backend/Rust/Pretty/Keywords.hs index 2a308704df..e0d5c54947 100644 --- a/src/Juvix/Compiler/Backend/Rust/Pretty/Keywords.hs +++ b/src/Juvix/Compiler/Backend/Rust/Pretty/Keywords.hs @@ -6,9 +6,6 @@ import Juvix.Extra.Strings qualified as Str kwFn :: Doc Ann kwFn = keyword Str.rustFn -kwIf :: Doc Ann -kwIf = keyword Str.rustIf - kwElse :: Doc Ann kwElse = keyword Str.rustElse diff --git a/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs b/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs index c40416fa74..fa46e1828f 100644 --- a/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs +++ b/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs @@ -51,6 +51,3 @@ kwLessThan = keyword Str.vampirLessThan kwLessOrEqual :: Doc Ann kwLessOrEqual = keyword Str.vampirLessOrEqual - -kwIf :: Doc Ann -kwIf = keyword Str.vampirIf diff --git a/src/Juvix/Compiler/Concrete/Data/IfBranchKind.hs b/src/Juvix/Compiler/Concrete/Data/IfBranchKind.hs new file mode 100644 index 0000000000..4f99854682 --- /dev/null +++ b/src/Juvix/Compiler/Concrete/Data/IfBranchKind.hs @@ -0,0 +1,17 @@ +module Juvix.Compiler.Concrete.Data.IfBranchKind where + +import Juvix.Extra.Serialize +import Juvix.Prelude + +data IfBranchKind + = -- | Boolean condition + BranchIfBool + | -- | Default branch + BranchIfElse + deriving stock (Show, Eq, Ord, Generic) + +instance Serialize IfBranchKind + +instance NFData IfBranchKind + +$(genSingletons [''IfBranchKind]) diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs index 530dbc4755..b60bd2c9ad 100644 --- a/src/Juvix/Compiler/Concrete/Keywords.hs +++ b/src/Juvix/Compiler/Concrete/Keywords.hs @@ -92,6 +92,7 @@ reservedKeywords = kwEnd, kwHiding, kwHole, + kwIf, kwImport, kwIn, kwInductive, diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index f236306025..8546907bbb 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -6,6 +6,7 @@ module Juvix.Compiler.Concrete.Language module Juvix.Compiler.Concrete.Data.IsOpenShort, module Juvix.Compiler.Concrete.Data.LocalModuleOrigin, module Juvix.Data.IteratorInfo, + module Juvix.Compiler.Concrete.Data.IfBranchKind, module Juvix.Compiler.Concrete.Data.Name, module Juvix.Compiler.Concrete.Data.Stage, module Juvix.Compiler.Concrete.Data.NameRef, @@ -23,6 +24,7 @@ where import Data.Kind qualified as GHC import Juvix.Compiler.Backend.Markdown.Data.Types (Mk) import Juvix.Compiler.Concrete.Data.Builtins +import Juvix.Compiler.Concrete.Data.IfBranchKind import Juvix.Compiler.Concrete.Data.IsOpenShort import Juvix.Compiler.Concrete.Data.Literal import Juvix.Compiler.Concrete.Data.LocalModuleOrigin @@ -57,6 +59,16 @@ type family FieldArgIxType s = res | res -> s where FieldArgIxType 'Parsed = () FieldArgIxType 'Scoped = Int +type SideIfBranchConditionType :: Stage -> IfBranchKind -> GHC.Type +type family SideIfBranchConditionType s k = res where + SideIfBranchConditionType s 'BranchIfBool = ExpressionType s + SideIfBranchConditionType _ 'BranchIfElse = () + +type IfBranchConditionType :: Stage -> IfBranchKind -> GHC.Type +type family IfBranchConditionType s k = res where + IfBranchConditionType s 'BranchIfBool = ExpressionType s + IfBranchConditionType _ 'BranchIfElse = Irrelevant KeywordRef + type ModuleIdType :: Stage -> ModuleIsTop -> GHC.Type type family ModuleIdType s t = res where ModuleIdType 'Parsed _ = () @@ -1706,11 +1718,136 @@ deriving stock instance Ord (Let 'Parsed) deriving stock instance Ord (Let 'Scoped) +data SideIfBranch (s :: Stage) (k :: IfBranchKind) = SideIfBranch + { _sideIfBranchPipe :: Irrelevant (Maybe KeywordRef), + _sideIfBranchKw :: Irrelevant KeywordRef, + _sideIfBranchCondition :: SideIfBranchConditionType s k, + _sideIfBranchAssignKw :: Irrelevant KeywordRef, + _sideIfBranchBody :: ExpressionType s + } + deriving stock (Generic) + +instance Serialize (SideIfBranch 'Scoped 'BranchIfBool) + +instance Serialize (SideIfBranch 'Scoped 'BranchIfElse) + +instance NFData (SideIfBranch 'Scoped 'BranchIfBool) + +instance NFData (SideIfBranch 'Scoped 'BranchIfElse) + +instance Serialize (SideIfBranch 'Parsed 'BranchIfBool) + +instance Serialize (SideIfBranch 'Parsed 'BranchIfElse) + +instance NFData (SideIfBranch 'Parsed 'BranchIfElse) + +instance NFData (SideIfBranch 'Parsed 'BranchIfBool) + +deriving stock instance Show (SideIfBranch 'Parsed 'BranchIfElse) + +deriving stock instance Show (SideIfBranch 'Parsed 'BranchIfBool) + +deriving stock instance Show (SideIfBranch 'Scoped 'BranchIfElse) + +deriving stock instance Show (SideIfBranch 'Scoped 'BranchIfBool) + +deriving stock instance Eq (SideIfBranch 'Parsed 'BranchIfElse) + +deriving stock instance Eq (SideIfBranch 'Parsed 'BranchIfBool) + +deriving stock instance Eq (SideIfBranch 'Scoped 'BranchIfElse) + +deriving stock instance Eq (SideIfBranch 'Scoped 'BranchIfBool) + +deriving stock instance Ord (SideIfBranch 'Parsed 'BranchIfElse) + +deriving stock instance Ord (SideIfBranch 'Parsed 'BranchIfBool) + +deriving stock instance Ord (SideIfBranch 'Scoped 'BranchIfElse) + +deriving stock instance Ord (SideIfBranch 'Scoped 'BranchIfBool) + +data SideIfs (s :: Stage) = SideIfs + { _sideIfBranches :: NonEmpty (SideIfBranch s 'BranchIfBool), + _sideIfElse :: Maybe (SideIfBranch s 'BranchIfElse) + } + deriving stock (Generic) + +instance Serialize (SideIfs 'Scoped) + +instance NFData (SideIfs 'Scoped) + +instance Serialize (SideIfs 'Parsed) + +instance NFData (SideIfs 'Parsed) + +deriving stock instance Show (SideIfs 'Parsed) + +deriving stock instance Show (SideIfs 'Scoped) + +deriving stock instance Eq (SideIfs 'Parsed) + +deriving stock instance Eq (SideIfs 'Scoped) + +deriving stock instance Ord (SideIfs 'Parsed) + +deriving stock instance Ord (SideIfs 'Scoped) + +data RhsExpression (s :: Stage) = RhsExpression + { _rhsExpressionAssignKw :: Irrelevant KeywordRef, + _rhsExpression :: ExpressionType s + } + deriving stock (Generic) + +instance Serialize (RhsExpression 'Scoped) + +instance NFData (RhsExpression 'Scoped) + +instance Serialize (RhsExpression 'Parsed) + +instance NFData (RhsExpression 'Parsed) + +deriving stock instance Show (RhsExpression 'Parsed) + +deriving stock instance Show (RhsExpression 'Scoped) + +deriving stock instance Eq (RhsExpression 'Parsed) + +deriving stock instance Eq (RhsExpression 'Scoped) + +deriving stock instance Ord (RhsExpression 'Parsed) + +deriving stock instance Ord (RhsExpression 'Scoped) + +data CaseBranchRhs (s :: Stage) + = CaseBranchRhsExpression (RhsExpression s) + | CaseBranchRhsIf (SideIfs s) + deriving stock (Generic) + +instance Serialize (CaseBranchRhs 'Scoped) + +instance NFData (CaseBranchRhs 'Scoped) + +instance Serialize (CaseBranchRhs 'Parsed) + +instance NFData (CaseBranchRhs 'Parsed) + +deriving stock instance Show (CaseBranchRhs 'Parsed) + +deriving stock instance Show (CaseBranchRhs 'Scoped) + +deriving stock instance Eq (CaseBranchRhs 'Parsed) + +deriving stock instance Eq (CaseBranchRhs 'Scoped) + +deriving stock instance Ord (CaseBranchRhs 'Parsed) + +deriving stock instance Ord (CaseBranchRhs 'Scoped) + data CaseBranch (s :: Stage) = CaseBranch { _caseBranchPipe :: Irrelevant (Maybe KeywordRef), - _caseBranchAssignKw :: Irrelevant KeywordRef, _caseBranchPattern :: PatternParensType s, - _caseBranchExpression :: ExpressionType s + _caseBranchRhs :: CaseBranchRhs s } deriving stock (Generic) @@ -1818,66 +1955,58 @@ deriving stock instance Ord (NewCase 'Parsed) deriving stock instance Ord (NewCase 'Scoped) -data IfBranch (s :: Stage) = IfBranch +data IfBranch (s :: Stage) (k :: IfBranchKind) = IfBranch { _ifBranchPipe :: Irrelevant KeywordRef, _ifBranchAssignKw :: Irrelevant KeywordRef, - _ifBranchCondition :: ExpressionType s, + _ifBranchCondition :: IfBranchConditionType s k, _ifBranchExpression :: ExpressionType s } deriving stock (Generic) -instance Serialize (IfBranch 'Scoped) +instance Serialize (IfBranch 'Scoped 'BranchIfBool) -instance NFData (IfBranch 'Scoped) +instance Serialize (IfBranch 'Scoped 'BranchIfElse) -instance Serialize (IfBranch 'Parsed) +instance NFData (IfBranch 'Scoped 'BranchIfBool) -instance NFData (IfBranch 'Parsed) +instance NFData (IfBranch 'Scoped 'BranchIfElse) -deriving stock instance Show (IfBranch 'Parsed) +instance Serialize (IfBranch 'Parsed 'BranchIfBool) -deriving stock instance Show (IfBranch 'Scoped) +instance Serialize (IfBranch 'Parsed 'BranchIfElse) -deriving stock instance Eq (IfBranch 'Parsed) +instance NFData (IfBranch 'Parsed 'BranchIfElse) -deriving stock instance Eq (IfBranch 'Scoped) +instance NFData (IfBranch 'Parsed 'BranchIfBool) -deriving stock instance Ord (IfBranch 'Parsed) +deriving stock instance Show (IfBranch 'Parsed 'BranchIfElse) -deriving stock instance Ord (IfBranch 'Scoped) +deriving stock instance Show (IfBranch 'Parsed 'BranchIfBool) -data IfBranchElse (s :: Stage) = IfBranchElse - { _ifBranchElsePipe :: Irrelevant KeywordRef, - _ifBranchElseAssignKw :: Irrelevant KeywordRef, - _ifBranchElseKw :: Irrelevant KeywordRef, - _ifBranchElseExpression :: ExpressionType s - } - deriving stock (Generic) - -instance Serialize (IfBranchElse 'Scoped) +deriving stock instance Show (IfBranch 'Scoped 'BranchIfElse) -instance NFData (IfBranchElse 'Scoped) +deriving stock instance Show (IfBranch 'Scoped 'BranchIfBool) -instance Serialize (IfBranchElse 'Parsed) +deriving stock instance Eq (IfBranch 'Parsed 'BranchIfElse) -instance NFData (IfBranchElse 'Parsed) +deriving stock instance Eq (IfBranch 'Parsed 'BranchIfBool) -deriving stock instance Show (IfBranchElse 'Parsed) +deriving stock instance Eq (IfBranch 'Scoped 'BranchIfElse) -deriving stock instance Show (IfBranchElse 'Scoped) +deriving stock instance Eq (IfBranch 'Scoped 'BranchIfBool) -deriving stock instance Eq (IfBranchElse 'Parsed) +deriving stock instance Ord (IfBranch 'Parsed 'BranchIfElse) -deriving stock instance Eq (IfBranchElse 'Scoped) +deriving stock instance Ord (IfBranch 'Parsed 'BranchIfBool) -deriving stock instance Ord (IfBranchElse 'Parsed) +deriving stock instance Ord (IfBranch 'Scoped 'BranchIfElse) -deriving stock instance Ord (IfBranchElse 'Scoped) +deriving stock instance Ord (IfBranch 'Scoped 'BranchIfBool) data If (s :: Stage) = If { _ifKw :: KeywordRef, - _ifBranches :: NonEmpty (IfBranch s), - _ifBranchElse :: IfBranchElse s + _ifBranches :: [IfBranch s 'BranchIfBool], + _ifBranchElse :: IfBranch s 'BranchIfElse } deriving stock (Generic) @@ -2468,6 +2597,9 @@ deriving stock instance Ord (JudocAtom 'Parsed) deriving stock instance Ord (JudocAtom 'Scoped) +makeLenses ''SideIfs +makeLenses ''SideIfBranch +makeLenses ''RhsExpression makeLenses ''PatternArg makeLenses ''WildcardConstructor makeLenses ''DoubleBracesExpression @@ -2526,7 +2658,6 @@ makeLenses ''Case makeLenses ''CaseBranch makeLenses ''If makeLenses ''IfBranch -makeLenses ''IfBranchElse makeLenses ''PatternBinding makeLenses ''PatternAtoms makeLenses ''ExpressionAtoms @@ -2732,20 +2863,37 @@ instance HasLoc (Function 'Scoped) where instance HasLoc (Let 'Scoped) where getLoc l = getLoc (l ^. letKw) <> getLoc (l ^. letExpression) +instance (SingI s) => HasLoc (SideIfBranch s k) where + getLoc SideIfBranch {..} = + (getLoc <$> _sideIfBranchPipe ^. unIrrelevant) + ?<> getLocExpressionType _sideIfBranchBody + +instance (SingI s) => HasLoc (SideIfs s) where + getLoc SideIfs {..} = + getLocSpan _sideIfBranches + <>? (getLoc <$> _sideIfElse) + +instance (SingI s) => HasLoc (RhsExpression s) where + getLoc RhsExpression {..} = + getLoc _rhsExpressionAssignKw + <> getLocExpressionType _rhsExpression + +instance (SingI s) => HasLoc (CaseBranchRhs s) where + getLoc = \case + CaseBranchRhsExpression e -> getLoc e + CaseBranchRhsIf e -> getLoc e + instance (SingI s) => HasLoc (CaseBranch s) where getLoc c = case c ^. caseBranchPipe . unIrrelevant of Nothing -> branchLoc Just p -> getLoc p <> branchLoc where branchLoc :: Interval - branchLoc = getLocExpressionType (c ^. caseBranchExpression) + branchLoc = getLoc (c ^. caseBranchRhs) -instance (SingI s) => HasLoc (IfBranch s) where +instance (SingI s) => HasLoc (IfBranch s k) 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) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 4299ff2c04..a5edf60c87 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -13,6 +13,8 @@ import Data.Map qualified as Map import Juvix.Compiler.Concrete.Data.Scope.Base import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Extra qualified as Concrete +import Juvix.Compiler.Concrete.Gen qualified as Gen +import Juvix.Compiler.Concrete.Keywords import Juvix.Compiler.Concrete.Keywords qualified as Kw import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Pretty.Options @@ -538,11 +540,52 @@ ppLet isTop Let {..} = do letExpression' = ppMaybeTopExpression isTop _letExpression align $ ppCode _letKw <> letFunDefs' <> ppCode _letInKw <+> letExpression' +instance (SingI s, SingI k) => PrettyPrint (SideIfBranch s k) where + ppCode SideIfBranch {..} = do + let kwPipe' = ppCode <$> _sideIfBranchPipe ^. unIrrelevant + kwIfElse' = ppCode _sideIfBranchKw + kwAssign' = ppCode _sideIfBranchAssignKw + condition' = case sing :: SIfBranchKind k of + SBranchIfBool -> Just (ppExpressionType _sideIfBranchCondition) + SBranchIfElse -> Nothing + body' = ppExpressionType _sideIfBranchBody + kwPipe' + ( kwIfElse' + <+?> condition' + <+> kwAssign' + <> oneLineOrNext body' + ) + +instance (SingI s) => PrettyPrint (SideIfs s) where + ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => SideIfs s -> Sem r () + ppCode SideIfs {..} = + case (_sideIfBranches, _sideIfElse) of + (b :| [], Nothing) -> ppCode (set sideIfBranchPipe (Irrelevant Nothing) b) + (b :| bs, _) -> do + let putPipe :: Maybe KeywordRef -> Maybe KeywordRef + putPipe = \case + Nothing -> Just (run (runReader (getLoc b) (Gen.kw kwPipe))) + Just p -> Just p + firstBr = over (sideIfBranchPipe . unIrrelevant) putPipe b + ifbranches = map ppCode (toList (firstBr : bs)) + allBranches :: [Sem r ()] = snocMaybe ifbranches (ppCode <$> _sideIfElse) + line <> indent (vsepHard allBranches) + +ppCaseBranchRhs :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> CaseBranchRhs s -> Sem r () +ppCaseBranchRhs isTop = \case + CaseBranchRhsExpression e -> ppExpressionRhs isTop e + CaseBranchRhsIf ifCond -> ppCode ifCond + +ppExpressionRhs :: (Member (Reader Options) r, Member ExactPrint r, SingI s) => IsTop -> RhsExpression s -> Sem r () +ppExpressionRhs isTop RhsExpression {..} = do + let expr' = ppMaybeTopExpression isTop _rhsExpression + ppCode _rhsExpressionAssignKw <> oneLineOrNext expr' + ppCaseBranch :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> CaseBranch s -> Sem r () ppCaseBranch isTop CaseBranch {..} = do let pat' = ppPatternParensType _caseBranchPattern - e' = ppMaybeTopExpression isTop _caseBranchExpression - pat' <+> ppCode _caseBranchAssignKw <> oneLineOrNext e' + rhs' = ppCaseBranchRhs isTop _caseBranchRhs + pat' <+> rhs' ppCase :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> Case s -> Sem r () ppCase isTop Case {..} = do @@ -573,32 +616,37 @@ ppCase isTop Case {..} = do Just p -> ppCode p Nothing -> ppCode Kw.kwPipe -instance (SingI s) => PrettyPrint (IfBranch s) where +instance (SingI s) => PrettyPrint (IfBranch s 'BranchIfBool) where ppCode IfBranch {..} = do - let cond' = ppExpressionType _ifBranchCondition + let pipe' = ppCode _ifBranchPipe + cond' = ppExpressionType _ifBranchCondition e' = ppExpressionType _ifBranchExpression - cond' <+> ppCode _ifBranchAssignKw <> oneLineOrNext e' + pipe' <+> cond' <+> ppCode _ifBranchAssignKw <> oneLineOrNext e' -ppIfBranchElse :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> IfBranchElse s -> Sem r () -ppIfBranchElse isTop IfBranchElse {..} = do - let e' = ppMaybeTopExpression isTop _ifBranchElseExpression - ppCode _ifBranchElseKw <+> ppCode _ifBranchElseAssignKw <> oneLineOrNext e' +ppIfBranchElse :: + forall r s. + (Members '[ExactPrint, Reader Options] r, SingI s) => + IsTop -> + IfBranch s 'BranchIfElse -> + Sem r () +ppIfBranchElse isTop IfBranch {..} = do + let e' = ppMaybeTopExpression isTop _ifBranchExpression + ppCode _ifBranchCondition <+> ppCode _ifBranchAssignKw <> oneLineOrNext e' ppIf :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> If s -> Sem r () ppIf isTop If {..} = do - ppCode _ifKw <+> hardline <> indent (vsepHard (ppIfBranch <$> _ifBranches) <> hardline <> ppIfBranchElse' _ifBranchElse) + ppCode _ifKw + <+> hardline + <> indent + ( vsepHard (ppIfBranch <$> _ifBranches) + <> hardline + <> ppIfBranch _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 <+> ppIfBranchElse isTop b - where - pipeHelper :: Sem r () - pipeHelper = ppCode (b ^. ifBranchElsePipe . unIrrelevant) + ppIfBranch :: forall k. (SingI k) => IfBranch s k -> Sem r () + ppIfBranch b = case sing :: SIfBranchKind k of + SBranchIfBool -> ppCode b + SBranchIfElse -> ppIfBranchElse isTop b instance PrettyPrint Universe where ppCode Universe {..} = ppCode _universeKw <+?> (noLoc . pretty <$> _universeLevel) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 10ec1a39cf..89d7b4450f 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -2189,6 +2189,98 @@ checkLet Let {..} = _letInKw } +checkRhsExpression :: + forall r. + ( Members + '[ HighlightBuilder, + Reader ScopeParameters, + Error ScoperError, + State Scope, + State ScoperState, + InfoTableBuilder, + Reader InfoTable, + NameIdGen, + Reader Package + ] + r + ) => + RhsExpression 'Parsed -> + Sem r (RhsExpression 'Scoped) +checkRhsExpression RhsExpression {..} = do + expr' <- checkParseExpressionAtoms _rhsExpression + return + RhsExpression + { _rhsExpression = expr', + _rhsExpressionAssignKw + } + +checkSideIfBranch :: + forall r (k :: IfBranchKind). + ( SingI k, + Members + '[ HighlightBuilder, + Reader ScopeParameters, + Error ScoperError, + State Scope, + State ScoperState, + InfoTableBuilder, + Reader InfoTable, + NameIdGen, + Reader Package + ] + r + ) => + SideIfBranch 'Parsed k -> + Sem r (SideIfBranch 'Scoped k) +checkSideIfBranch SideIfBranch {..} = do + cond' <- case sing :: SIfBranchKind k of + SBranchIfBool -> checkParseExpressionAtoms _sideIfBranchCondition + SBranchIfElse -> return _sideIfBranchCondition + body' <- checkParseExpressionAtoms _sideIfBranchBody + return + SideIfBranch + { _sideIfBranchBody = body', + _sideIfBranchCondition = cond', + _sideIfBranchPipe, + _sideIfBranchKw, + _sideIfBranchAssignKw + } + +checkSideIfs :: + forall r. + ( Members + '[ HighlightBuilder, + Reader ScopeParameters, + Error ScoperError, + State Scope, + State ScoperState, + InfoTableBuilder, + Reader InfoTable, + NameIdGen, + Reader Package + ] + r + ) => + SideIfs 'Parsed -> + Sem r (SideIfs 'Scoped) +checkSideIfs SideIfs {..} = do + branches' <- mapM checkSideIfBranch _sideIfBranches + else' <- mapM checkSideIfBranch _sideIfElse + return + SideIfs + { _sideIfBranches = branches', + _sideIfElse = else' + } + +checkCaseBranchRhs :: + forall r. + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => + CaseBranchRhs 'Parsed -> + Sem r (CaseBranchRhs 'Scoped) +checkCaseBranchRhs = \case + CaseBranchRhsExpression r -> CaseBranchRhsExpression <$> checkRhsExpression r + CaseBranchRhsIf r -> CaseBranchRhsIf <$> checkSideIfs r + checkCaseBranch :: forall r. (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => @@ -2196,11 +2288,11 @@ checkCaseBranch :: Sem r (CaseBranch 'Scoped) checkCaseBranch CaseBranch {..} = withLocalScope $ do pattern' <- checkParsePatternAtoms _caseBranchPattern - expression' <- (checkParseExpressionAtoms _caseBranchExpression) + rhs' <- checkCaseBranchRhs _caseBranchRhs return $ CaseBranch { _caseBranchPattern = pattern', - _caseBranchExpression = expression', + _caseBranchRhs = rhs', .. } @@ -2220,12 +2312,14 @@ checkCase Case {..} = do } checkIfBranch :: - forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => - IfBranch 'Parsed -> - Sem r (IfBranch 'Scoped) + forall r k. + (SingI k, Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => + IfBranch 'Parsed k -> + Sem r (IfBranch 'Scoped k) checkIfBranch IfBranch {..} = withLocalScope $ do - cond' <- checkParseExpressionAtoms _ifBranchCondition + cond' <- case sing :: SIfBranchKind k of + SBranchIfBool -> checkParseExpressionAtoms _ifBranchCondition + SBranchIfElse -> return _ifBranchCondition expression' <- checkParseExpressionAtoms _ifBranchExpression return $ IfBranch @@ -2234,26 +2328,13 @@ checkIfBranch IfBranch {..} = withLocalScope $ do .. } -checkIfBranchElse :: - forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] 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 Package] r) => If 'Parsed -> Sem r (If 'Scoped) checkIf If {..} = do ifBranches' <- mapM checkIfBranch _ifBranches - ifBranchElse' <- checkIfBranchElse _ifBranchElse + ifBranchElse' <- checkIfBranch _ifBranchElse return $ If { _ifBranchElse = ifBranchElse', diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 00c7afc572..893eb45754 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -825,7 +825,7 @@ expressionAtom = <|> AtomNamedApplicationNew <$> namedApplicationNew <|> AtomNamedApplication <$> namedApplication <|> AtomList <$> parseList - <|> either AtomIf AtomIdentifier <$> multiwayIf + <|> AtomIf <$> multiwayIf <|> AtomIdentifier <$> name <|> AtomUniverse <$> universe <|> AtomLambda <$> lambda @@ -1112,11 +1112,63 @@ letBlock = do _letExpression <- parseExpressionAtoms return Let {..} +-- | The pipe for the first branch is optional +sideIfBranch :: + forall r k. + (SingI k, Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => + Bool -> + ParsecS r (SideIfBranch 'Parsed k) +sideIfBranch isFirst = do + let ifElseKw = + Irrelevant <$> case sing :: SIfBranchKind k of + SBranchIfBool -> kw kwIf + SBranchIfElse -> kw kwElse + (_sideIfBranchPipe, _sideIfBranchKw) <- P.try $ do + let opt + | isFirst = optional + | otherwise = fmap Just + pipe' <- Irrelevant <$> opt (kw kwPipe) + condKw' <- ifElseKw + return (pipe', condKw') + _sideIfBranchCondition <- case sing :: SIfBranchKind k of + SBranchIfBool -> parseExpressionAtoms + SBranchIfElse -> return () + _sideIfBranchAssignKw <- Irrelevant <$> kw kwAssign + _sideIfBranchBody <- parseExpressionAtoms + return SideIfBranch {..} + +sideIfs :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (SideIfs 'Parsed) +sideIfs = do + fstBranch <- sideIfBranch True + moreBranches <- many (sideIfBranch False) + let _sideIfBranches = fstBranch :| moreBranches + _sideIfElse <- optional (sideIfBranch False) + return + SideIfs + { .. + } + +prhsExpression :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RhsExpression 'Parsed) +prhsExpression = do + _rhsExpressionAssignKw <- Irrelevant <$> kw kwAssign + _rhsExpression <- parseExpressionAtoms + return RhsExpression {..} + +pcaseBranchRhs :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (CaseBranchRhs 'Parsed) +pcaseBranchRhs = + CaseBranchRhsExpression <$> pcaseBranchRhsExpression + <|> CaseBranchRhsIf <$> sideIfs + +pcaseBranchRhsExpression :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RhsExpression 'Parsed) +pcaseBranchRhsExpression = do + _rhsExpressionAssignKw <- Irrelevant <$> kw kwAssign + _rhsExpression <- parseExpressionAtoms + return RhsExpression {..} + caseBranch :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (CaseBranch 'Parsed) caseBranch _caseBranchPipe = do _caseBranchPattern <- parsePatternAtoms - _caseBranchAssignKw <- Irrelevant <$> kw kwAssign - _caseBranchExpression <- parseExpressionAtoms + _caseBranchRhs <- pcaseBranchRhs return CaseBranch {..} case_ :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Case 'Parsed) @@ -1127,43 +1179,30 @@ case_ = P.label "case" $ do _caseBranches <- braces (pipeSep1 caseBranch) <|> pipeSep1 caseBranch return Case {..} -ifBranch' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Irrelevant KeywordRef -> ParsecS r (IfBranch 'Parsed) -ifBranch' _ifBranchPipe = do - _ifBranchCondition <- parseExpressionAtoms +ifBranch :: + forall r k. + (SingI k, Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => + ParsecS r (IfBranch 'Parsed k) +ifBranch = do + _ifBranchPipe <- Irrelevant <$> pipeHelper + _ifBranchCondition <- case sing :: SIfBranchKind k of + SBranchIfBool -> parseExpressionAtoms + SBranchIfElse -> Irrelevant <$> kw kwElse _ifBranchAssignKw <- Irrelevant <$> kw kwAssign _ifBranchExpression <- parseExpressionAtoms return IfBranch {..} + where + pipeHelper :: ParsecS r KeywordRef + pipeHelper = case sing :: SIfBranchKind k of + SBranchIfBool -> P.try (kw kwPipe <* P.notFollowedBy (kw kwElse)) + SBranchIfElse -> kw kwPipe -parseIfBranchElse' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] 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] 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] 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] 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] r) => ParsecS r (Either (If 'Parsed) Name) +multiwayIf :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (If 'Parsed) multiwayIf = do _ifKw <- kw kwIf - (Left <$> multiwayIf' _ifKw []) - <|> return (Right $ NameUnqualified $ WithLoc (getLoc _ifKw) (_ifKw ^. keywordRefKeyword . keywordAscii)) + _ifBranches <- many ifBranch + _ifBranchElse <- ifBranch + return If {..} -------------------------------------------------------------------------------- -- Universe expression diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 4462952137..b0f102a844 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -777,9 +777,6 @@ kwMatch = keyword Str.match_ kwWith :: Doc Ann kwWith = keyword Str.with_ -kwIf :: Doc Ann -kwIf = keyword Str.if_ - kwThen :: Doc Ann kwThen = keyword Str.then_ diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index f900b78c6e..8819620674 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -467,7 +467,7 @@ mkBody ppLam ty loc clauses <> (ppLam ^. withLocParam) goClause :: Level -> [Internal.PatternArg] -> Internal.Expression -> Sem r MatchBranch - goClause lvl pats body = goPatternArgs lvl body pats ptys + goClause lvl pats body = goPatternArgs lvl (Internal.CaseBranchRhsExpression body) pats ptys where ptys :: [Type] ptys = take (length pats) (typeArgs ty) @@ -498,13 +498,31 @@ goCase c = do body <- local (set indexTableVars vars') - (underBinders 1 (goExpression _caseBranchExpression)) + (underBinders 1 (goCaseBranchRhs _caseBranchRhs)) return $ mkLet i (Binder (name ^. nameText) (Just $ name ^. nameLoc) ty) expr body _ -> impossible where goCaseBranch :: Type -> Internal.CaseBranch -> Sem r MatchBranch - goCaseBranch ty b = goPatternArgs 0 (b ^. Internal.caseBranchExpression) [b ^. Internal.caseBranchPattern] [ty] + goCaseBranch ty b = goPatternArgs 0 (b ^. Internal.caseBranchRhs) [b ^. Internal.caseBranchPattern] [ty] + +-- | FIXME Fix this as soon as side if conditions are implemented in Core. This +-- is needed so that we can test typechecking without a crash. +todoSideIfs :: + forall r. + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) => + Internal.SideIfs -> + Sem r Node +todoSideIfs s = goExpression (s ^. Internal.sideIfBranches . _head1 . Internal.sideIfBranchBody) + +goCaseBranchRhs :: + forall r. + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) => + Internal.CaseBranchRhs -> + Sem r Node +goCaseBranchRhs = \case + Internal.CaseBranchRhsExpression e -> goExpression e + Internal.CaseBranchRhsIf i -> todoSideIfs i goLambda :: forall r. @@ -932,7 +950,7 @@ goPatternArgs :: forall r. (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) => Level -> -- the level of the first binder for the matched value - Internal.Expression -> + Internal.CaseBranchRhs -> [Internal.PatternArg] -> [Type] -> -- types of the patterns Sem r MatchBranch @@ -960,7 +978,7 @@ goPatternArgs lvl0 body = go lvl0 [] _ -> impossible ([], []) -> do - body' <- goExpression body + body' <- goCaseBranchRhs body return $ MatchBranch Info.empty (nonEmpty' (reverse pats)) body' _ -> impossible diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index 0c3502f074..66a7f2c72f 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -90,10 +90,27 @@ instance HasExpressions Pattern where PatternConstructorApp a -> PatternConstructorApp <$> leafExpressions f a PatternWildcardConstructor {} -> pure p +instance HasExpressions SideIfBranch where + leafExpressions f b = do + _sideIfBranchCondition <- leafExpressions f (b ^. sideIfBranchCondition) + _sideIfBranchBody <- leafExpressions f (b ^. sideIfBranchBody) + pure SideIfBranch {..} + +instance HasExpressions SideIfs where + leafExpressions f b = do + _sideIfBranches <- traverse (leafExpressions f) (b ^. sideIfBranches) + _sideIfElse <- traverse (leafExpressions f) (b ^. sideIfElse) + pure SideIfs {..} + +instance HasExpressions CaseBranchRhs where + leafExpressions f = \case + CaseBranchRhsExpression e -> CaseBranchRhsExpression <$> leafExpressions f e + CaseBranchRhsIf e -> CaseBranchRhsIf <$> leafExpressions f e + instance HasExpressions CaseBranch where leafExpressions f b = do _caseBranchPattern <- leafExpressions f (b ^. caseBranchPattern) - _caseBranchExpression <- leafExpressions f (b ^. caseBranchExpression) + _caseBranchRhs <- leafExpressions f (b ^. caseBranchRhs) pure CaseBranch {..} instance HasExpressions Case where diff --git a/src/Juvix/Compiler/Internal/Extra/Clonable.hs b/src/Juvix/Compiler/Internal/Extra/Clonable.hs index 473701d5ed..ad2ad2a071 100644 --- a/src/Juvix/Compiler/Internal/Extra/Clonable.hs +++ b/src/Juvix/Compiler/Internal/Extra/Clonable.hs @@ -107,14 +107,39 @@ underBinders ps f = do modify' @FreshBindersContext (set (at (v ^. nameId)) (Just uid')) return (set nameId uid' v) +instance Clonable SideIfBranch where + freshNameIds SideIfBranch {..} = do + cond' <- freshNameIds _sideIfBranchCondition + body' <- freshNameIds _sideIfBranchBody + return + SideIfBranch + { _sideIfBranchCondition = cond', + _sideIfBranchBody = body' + } + +instance Clonable SideIfs where + freshNameIds SideIfs {..} = do + branches' <- mapM freshNameIds _sideIfBranches + else' <- mapM freshNameIds _sideIfElse + return + SideIfs + { _sideIfBranches = branches', + _sideIfElse = else' + } + +instance Clonable CaseBranchRhs where + freshNameIds = \case + CaseBranchRhsExpression e -> CaseBranchRhsExpression <$> freshNameIds e + CaseBranchRhsIf e -> CaseBranchRhsIf <$> freshNameIds e + instance Clonable CaseBranch where freshNameIds CaseBranch {..} = underBinder _caseBranchPattern $ \pat' -> do - body' <- freshNameIds _caseBranchExpression + body' <- freshNameIds _caseBranchRhs return CaseBranch { _caseBranchPattern = pat', - _caseBranchExpression = body' + _caseBranchRhs = body' } instance Clonable Case where diff --git a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs index 04f5d9a6dd..5f0dace1aa 100644 --- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs +++ b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs @@ -259,10 +259,10 @@ goExpression p e = case e of ExpressionUniverse {} -> return () ExpressionFunction f -> do goFunctionParameter p (f ^. functionLeft) - goExpression p (f ^. functionRight) + goExpression_ (f ^. functionRight) ExpressionApplication (Application l r _) -> do - goExpression p l - goExpression p r + goExpression_ l + goExpression_ r ExpressionLiteral {} -> return () ExpressionCase c -> goCase c ExpressionHole {} -> return () @@ -271,6 +271,9 @@ goExpression p e = case e of ExpressionLet l -> goLet l ExpressionSimpleLambda l -> goSimpleLambda l where + goExpression_ :: Expression -> Sem r () + goExpression_ = goExpression p + goSimpleLambda :: SimpleLambda -> Sem r () goSimpleLambda l = do addEdgeMay p (l ^. slambdaBinder . sbinderVar) @@ -280,21 +283,36 @@ goExpression p e = case e of where goClause :: LambdaClause -> Sem r () goClause (LambdaClause {..}) = do - goExpression p _lambdaBody + goExpression_ _lambdaBody mapM_ (goPattern p) _lambdaPatterns goCase :: Case -> Sem r () goCase c = do - goExpression p (c ^. caseExpression) + goExpression_ (c ^. caseExpression) mapM_ goBranch (c ^. caseBranches) goBranch :: CaseBranch -> Sem r () - goBranch = goExpression p . (^. caseBranchExpression) + goBranch = goCaseBranchRhs . (^. caseBranchRhs) + + goSideIfBranch :: SideIfBranch -> Sem r () + goSideIfBranch SideIfBranch {..} = do + goExpression_ _sideIfBranchCondition + goExpression_ _sideIfBranchBody + + goSideIfs :: SideIfs -> Sem r () + goSideIfs SideIfs {..} = do + mapM_ goSideIfBranch _sideIfBranches + mapM_ goExpression_ _sideIfElse + + goCaseBranchRhs :: CaseBranchRhs -> Sem r () + goCaseBranchRhs = \case + CaseBranchRhsExpression expr -> goExpression_ expr + CaseBranchRhsIf s -> goSideIfs s goLet :: Let -> Sem r () goLet l = do mapM_ goLetClause (l ^. letClauses) - goExpression p (l ^. letExpression) + goExpression_ (l ^. letExpression) goLetClause :: LetClause -> Sem r () goLetClause = \case diff --git a/src/Juvix/Compiler/Internal/Extra/HasLetDefs.hs b/src/Juvix/Compiler/Internal/Extra/HasLetDefs.hs index 517aa81c3f..10def45522 100644 --- a/src/Juvix/Compiler/Internal/Extra/HasLetDefs.hs +++ b/src/Juvix/Compiler/Internal/Extra/HasLetDefs.hs @@ -5,8 +5,9 @@ import Juvix.Prelude class HasLetDefs a where letDefs' :: [Let] -> a -> [Let] - letDefs :: a -> [Let] - letDefs = letDefs' [] + +letDefs :: (HasLetDefs a) => a -> [Let] +letDefs = letDefs' [] instance (HasLetDefs a, Foldable f) => HasLetDefs (f a) where letDefs' = foldl' letDefs' @@ -69,8 +70,19 @@ instance HasLetDefs ConstructorApp where instance HasLetDefs Case where letDefs' acc Case {..} = letDefs' (letDefs' acc _caseExpression) _caseBranches +instance HasLetDefs SideIfs where + letDefs' acc SideIfs {..} = letDefs' (letDefs' acc _sideIfBranches) _sideIfElse + +instance HasLetDefs CaseBranchRhs where + letDefs' acc = \case + CaseBranchRhsExpression e -> letDefs' acc e + CaseBranchRhsIf e -> letDefs' acc e + +instance HasLetDefs SideIfBranch where + letDefs' acc SideIfBranch {..} = letDefs' (letDefs' acc _sideIfBranchCondition) _sideIfBranchBody + instance HasLetDefs CaseBranch where - letDefs' acc CaseBranch {..} = letDefs' acc _caseBranchExpression + letDefs' acc CaseBranch {..} = letDefs' acc _caseBranchRhs instance HasLetDefs MutualBlockLet where letDefs' acc MutualBlockLet {..} = letDefs' acc _mutualLet diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index c6e042fbfc..e05a7b770e 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -219,9 +219,44 @@ instance Serialize SimpleLambda instance NFData SimpleLambda +data SideIfBranch = SideIfBranch + { _sideIfBranchCondition :: Expression, + _sideIfBranchBody :: Expression + } + deriving stock (Eq, Generic, Data) + +instance Serialize SideIfBranch + +instance NFData SideIfBranch + +instance Hashable SideIfBranch + +data SideIfs = SideIfs + { _sideIfBranches :: NonEmpty SideIfBranch, + _sideIfElse :: Maybe Expression + } + deriving stock (Eq, Generic, Data) + +instance Serialize SideIfs + +instance NFData SideIfs + +instance Hashable SideIfs + +data CaseBranchRhs + = CaseBranchRhsExpression Expression + | CaseBranchRhsIf SideIfs + deriving stock (Eq, Generic, Data) + +instance Serialize CaseBranchRhs + +instance NFData CaseBranchRhs + +instance Hashable CaseBranchRhs + data CaseBranch = CaseBranch { _caseBranchPattern :: PatternArg, - _caseBranchExpression :: Expression + _caseBranchRhs :: CaseBranchRhs } deriving stock (Eq, Generic, Data) @@ -434,6 +469,9 @@ data NormalizedExpression = NormalizedExpression _normalizedExpressionOriginal :: Expression } +makeLenses ''SideIfBranch +makeLenses ''SideIfs +makeLenses ''CaseBranchRhs makeLenses ''ModuleIndex makeLenses ''ArgInfo makeLenses ''WildcardConstructor @@ -580,8 +618,23 @@ instance HasLoc LetClause where instance HasLoc Let where getLoc l = getLocSpan (l ^. letClauses) <> getLoc (l ^. letExpression) +instance HasLoc SideIfBranch where + getLoc SideIfBranch {..} = + getLoc _sideIfBranchCondition + <> getLoc _sideIfBranchBody + +instance HasLoc SideIfs where + getLoc SideIfs {..} = + getLocSpan _sideIfBranches + <>? (getLoc <$> _sideIfElse) + +instance HasLoc CaseBranchRhs where + getLoc = \case + CaseBranchRhsExpression e -> getLoc e + CaseBranchRhsIf e -> getLoc e + instance HasLoc CaseBranch where - getLoc c = getLoc (c ^. caseBranchPattern) <> getLoc (c ^. caseBranchExpression) + getLoc c = getLoc (c ^. caseBranchPattern) <> getLoc (c ^. caseBranchRhs) instance HasLoc Case where getLoc c = getLocSpan (c ^. caseBranches) diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 301a44199a..e22ce16022 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -83,10 +83,37 @@ instance PrettyCode Expression where ExpressionLet l -> ppCode l ExpressionCase c -> ppCode c +instance PrettyCode SideIfBranch where + ppCode SideIfBranch {..} = do + condition' <- ppCode _sideIfBranchCondition + body' <- ppCode _sideIfBranchBody + return $ + kwPipe + <+> kwIf + <+> condition' + <+> kwAssign + <+> oneLineOrNext body' + +instance PrettyCode SideIfs where + ppCode SideIfs {..} = + case (_sideIfBranches, _sideIfElse) of + (b :| [], Nothing) -> ppCode b + _ -> do + ifbranches <- mapM ppCode (toList _sideIfBranches) + elseBr <- mapM ppCode _sideIfElse + let allBranches = snocMaybe ifbranches elseBr + return $ + line <> indent' (vsep allBranches) + +instance PrettyCode CaseBranchRhs where + ppCode = \case + CaseBranchRhsExpression e -> ppCode e + CaseBranchRhsIf ifCond -> ppCode ifCond + instance PrettyCode CaseBranch where ppCode CaseBranch {..} = do pat <- ppCode _caseBranchPattern - e <- ppCode _caseBranchExpression + e <- ppCode _caseBranchRhs return $ kwPipe <+> pat <+> kwAssign <+> e instance PrettyCode Case where diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index a0c333b487..0276c1ec8b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -942,12 +942,12 @@ goExpression = \case goIf :: Concrete.If 'Scoped -> Sem r Internal.Expression goIf e@Concrete.If {..} = do if_ <- getBuiltinName (getLoc e) BuiltinBoolIf - go if_ (toList _ifBranches) + go if_ _ifBranches where - go :: Internal.Name -> [Concrete.IfBranch 'Scoped] -> Sem r Internal.Expression + go :: Internal.Name -> [Concrete.IfBranch 'Scoped 'BranchIfBool] -> Sem r Internal.Expression go if_ = \case [] -> - goExpression (_ifBranchElse ^. Concrete.ifBranchElseExpression) + goExpression (_ifBranchElse ^. Concrete.ifBranchExpression) Concrete.IfBranch {..} : brs -> do c <- goExpression _ifBranchCondition b1 <- goExpression _ifBranchExpression @@ -1070,9 +1070,60 @@ goCase c = do goBranch :: CaseBranch 'Scoped -> Sem r Internal.CaseBranch goBranch b = do _caseBranchPattern <- goPatternArg (b ^. caseBranchPattern) - _caseBranchExpression <- goExpression (b ^. caseBranchExpression) + _caseBranchRhs <- goCaseBranchRhs (b ^. caseBranchRhs) return Internal.CaseBranch {..} +gRhsExpression :: + forall r. + (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + RhsExpression 'Scoped -> + Sem r Internal.Expression +gRhsExpression RhsExpression {..} = goExpression _rhsExpression + +goSideIfBranch :: + forall r. + (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + SideIfBranch 'Scoped 'BranchIfBool -> + Sem r Internal.SideIfBranch +goSideIfBranch s = do + cond' <- goExpression (s ^. sideIfBranchCondition) + body' <- goExpression (s ^. sideIfBranchBody) + return + Internal.SideIfBranch + { _sideIfBranchCondition = cond', + _sideIfBranchBody = body' + } + +goSideIfBranchElse :: + forall r. + (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + SideIfBranch 'Scoped 'BranchIfElse -> + Sem r Internal.Expression +goSideIfBranchElse s = goExpression (s ^. sideIfBranchBody) + +goSideIfs :: + forall r. + (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + SideIfs 'Scoped -> + Sem r Internal.SideIfs +goSideIfs s = do + branches' <- mapM goSideIfBranch (s ^. sideIfBranches) + else' <- mapM goSideIfBranchElse (s ^. sideIfElse) + return + Internal.SideIfs + { _sideIfBranches = branches', + _sideIfElse = else' + } + +goCaseBranchRhs :: + forall r. + (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + CaseBranchRhs 'Scoped -> + Sem r Internal.CaseBranchRhs +goCaseBranchRhs = \case + CaseBranchRhsExpression e -> Internal.CaseBranchRhsExpression <$> gRhsExpression e + CaseBranchRhsIf s -> Internal.CaseBranchRhsIf <$> goSideIfs s + goLambda :: forall r. (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Lambda 'Scoped -> Sem r Internal.Lambda goLambda l = do clauses' <- mapM goClause (l ^. lambdaClauses) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs index e1af4e12b4..0560ff4cd4 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -65,7 +65,7 @@ checkStrictlyPositiveOccurrences :: Sem r () checkStrictlyPositiveOccurrences p = do typeOfConstr <- strongNormalize_ (p ^. checkPositivityArgsTypeOfConstructor) - go False typeOfConstr + goExpression False typeOfConstr where indInfo = p ^. checkPositivityArgsInductive ctorName = p ^. checkPositivityArgsConstructorName @@ -81,11 +81,11 @@ checkStrictlyPositiveOccurrences p = do used below indicates whether the current search is performed on the left of an inner arrow or not. -} - go :: Bool -> Expression -> Sem r () - go inside expr = case expr of + goExpression :: Bool -> Expression -> Sem r () + goExpression inside expr = case expr of ExpressionApplication tyApp -> goApp tyApp ExpressionCase l -> goCase l - ExpressionFunction (Function l r) -> go True (l ^. paramType) >> go inside r + ExpressionFunction (Function l r) -> goLeft (l ^. paramType) >> go r ExpressionHole {} -> return () ExpressionInstanceHole {} -> return () ExpressionIden i -> goIden i @@ -95,17 +95,38 @@ checkStrictlyPositiveOccurrences p = do ExpressionSimpleLambda l -> goSimpleLambda l ExpressionUniverse {} -> return () where + go :: Expression -> Sem r () + go = goExpression inside + + goLeft :: Expression -> Sem r () + goLeft = goExpression True + goCase :: Case -> Sem r () goCase l = do - go inside (l ^. caseExpression) + go (l ^. caseExpression) mapM_ goCaseBranch (l ^. caseBranches) + goSideIfBranch :: SideIfBranch -> Sem r () + goSideIfBranch b = do + go (b ^. sideIfBranchCondition) + go (b ^. sideIfBranchBody) + + goSideIfs :: SideIfs -> Sem r () + goSideIfs s = do + mapM_ goSideIfBranch (s ^. sideIfBranches) + mapM_ go (s ^. sideIfElse) + + goCaseBranchRhs :: CaseBranchRhs -> Sem r () + goCaseBranchRhs = \case + CaseBranchRhsExpression e -> go e + CaseBranchRhsIf s -> goSideIfs s + goCaseBranch :: CaseBranch -> Sem r () - goCaseBranch b = go inside (b ^. caseBranchExpression) + goCaseBranch b = goCaseBranchRhs (b ^. caseBranchRhs) goLet :: Let -> Sem r () goLet l = do - go inside (l ^. letExpression) + go (l ^. letExpression) mapM_ goLetClause (l ^. letClauses) goLetClause :: LetClause -> Sem r () @@ -118,19 +139,19 @@ checkStrictlyPositiveOccurrences p = do goFunctionDef :: FunctionDef -> Sem r () goFunctionDef d = do - go inside (d ^. funDefType) - go inside (d ^. funDefBody) + go (d ^. funDefType) + go (d ^. funDefBody) goSimpleLambda :: SimpleLambda -> Sem r () goSimpleLambda (SimpleLambda (SimpleBinder _ lamVarTy) lamBody) = do - go inside lamVarTy - go inside lamBody + go lamVarTy + go lamBody goLambda :: Lambda -> Sem r () goLambda l = mapM_ goClause (l ^. lambdaClauses) where goClause :: LambdaClause -> Sem r () - goClause (LambdaClause _ b) = go inside b + goClause (LambdaClause _ b) = go b goIden :: Iden -> Sem r () goIden = \case diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs index f3b3c739c2..9157299416 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs @@ -177,11 +177,35 @@ scanCase c = do mapM_ scanCaseBranch (c ^. caseBranches) scanExpression (c ^. caseExpression) +scanSideIfBranch :: + (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) => + SideIfBranch -> + Sem r () +scanSideIfBranch SideIfBranch {..} = do + scanExpression _sideIfBranchCondition + scanExpression _sideIfBranchBody + +scanSideIfs :: + (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) => + SideIfs -> + Sem r () +scanSideIfs SideIfs {..} = do + mapM_ scanSideIfBranch _sideIfBranches + mapM_ scanExpression _sideIfElse + +scanCaseBranchRhs :: + (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) => + CaseBranchRhs -> + Sem r () +scanCaseBranchRhs = \case + CaseBranchRhsExpression e -> scanExpression e + CaseBranchRhsIf e -> scanSideIfs e + scanCaseBranch :: (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) => CaseBranch -> Sem r () -scanCaseBranch = scanExpression . (^. caseBranchExpression) +scanCaseBranch = scanCaseBranchRhs . (^. caseBranchRhs) scanLet :: (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) => diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index 18c7708567..b860d2c697 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -444,6 +444,63 @@ checkCoercionType FunctionDef {..} = do Explicit -> throw (ErrWrongCoercionArgument (WrongCoercionArgument fp)) ImplicitInstance -> throw (ErrWrongCoercionArgument (WrongCoercionArgument fp)) +checkCaseBranchRhs :: + forall r. + (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + Expression -> + CaseBranchRhs -> + Sem r CaseBranchRhs +checkCaseBranchRhs expectedTy = \case + CaseBranchRhsExpression e -> CaseBranchRhsExpression <$> checkExpression expectedTy e + CaseBranchRhsIf s -> CaseBranchRhsIf <$> checkSideIfs expectedTy s + +checkSideIfs :: + forall r. + ( Members + '[ Reader InfoTable, + ResultBuilder, + Error TypeCheckerError, + NameIdGen, + Reader LocalVars, + Inference, + Output TypedHole, + Termination, + Output CastHole, + Reader InsertedArgsStack + ] + r + ) => + Expression -> + SideIfs -> + Sem r SideIfs +checkSideIfs expectedTy SideIfs {..} = do + branches' <- mapM (checkSideIfBranch expectedTy) _sideIfBranches + else' <- mapM (checkExpression expectedTy) _sideIfElse + return + SideIfs + { _sideIfBranches = branches', + _sideIfElse = else' + } + +checkSideIfBranch :: + forall r. + (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + Expression -> + SideIfBranch -> + Sem r SideIfBranch +checkSideIfBranch expectedTy SideIfBranch {..} = do + boolTy <- getBoolType (getLoc _sideIfBranchCondition) + cond' <- checkExpression boolTy _sideIfBranchCondition + body' <- checkExpression expectedTy _sideIfBranchBody + return + SideIfBranch + { _sideIfBranchCondition = cond', + _sideIfBranchBody = body' + } + +getBoolType :: (Members '[Reader InfoTable, Error TypeCheckerError] r) => Interval -> Sem r Expression +getBoolType loc = toExpression <$> getBuiltinName loc BuiltinBool + checkExpression :: forall r. (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => @@ -536,7 +593,7 @@ checkFunctionBody expectedTy body = case body of ExpressionLambda {} -> checkExpression expectedTy body _ -> do - (patterns', typedBody) <- checkClause (getLoc body) expectedTy [] body + (patterns', typedBody) <- checkClauseExpression (getLoc body) expectedTy [] body return $ case nonEmpty patterns' of Nothing -> typedBody Just lambdaPatterns' -> @@ -551,8 +608,7 @@ checkFunctionBody expectedTy body = } } --- | helper function for lambda functions and case branches -checkClause :: +checkClauseExpression :: forall r. (Members '[Reader InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> @@ -563,12 +619,30 @@ checkClause :: -- | Body Expression -> Sem r ([PatternArg], Expression) -- (Checked patterns, Checked body) +checkClauseExpression clauseLoc clauseType clausePats body = do + (pats', rhs') <- checkClause clauseLoc clauseType clausePats (CaseBranchRhsExpression body) + case rhs' of + CaseBranchRhsExpression body' -> return (pats', body') + CaseBranchRhsIf {} -> impossible + +-- | helper function for lambda functions and case branches +checkClause :: + forall r. + (Members '[Reader InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + Interval -> + -- | Type + Expression -> + -- | Arguments + [PatternArg] -> + -- | Body + CaseBranchRhs -> + Sem r ([PatternArg], CaseBranchRhs) -- (Checked patterns, Checked body) checkClause clauseLoc clauseType clausePats body = do locals0 <- ask (localsPats, (checkedPatterns, bodyType)) <- helper clausePats clauseType let locals' = locals0 <> localsPats bodyTy' <- substitutionE (localsToSubsE locals') bodyType - checkedBody <- local (const locals') (checkExpression bodyTy' body) + checkedBody <- local (const locals') (checkCaseBranchRhs bodyTy' body) return (checkedPatterns, checkedBody) where helper :: [PatternArg] -> Expression -> Sem r (LocalVars, ([PatternArg], Expression)) @@ -591,7 +665,7 @@ checkClause clauseLoc clauseType clausePats body = do [] -> do (bodyParams, bodyRest) <- unfoldFunType' bodyTy locals <- get - guessedBodyParams <- withLocalVars locals (unfoldArity <$> guessArity body) + guessedBodyParams <- withLocalVars locals (unfoldArity <$> arityCaseRhs body) let pref' :: [FunctionParameter] = take pref bodyParams pref :: Int = aI - targetI preImplicits = length . takeWhile isImplicitOrInstance @@ -921,7 +995,12 @@ inferLeftAppExpression mhint e = case e of _caseExpressionWholeType = Just ty goBranch :: CaseBranch -> Sem r CaseBranch goBranch b = do - (onePat, _caseBranchExpression) <- checkClause (getLoc b) funty [b ^. caseBranchPattern] (b ^. caseBranchExpression) + (onePat, _caseBranchRhs) <- + checkClause + (getLoc b) + funty + [b ^. caseBranchPattern] + (b ^. caseBranchRhs) let _caseBranchPattern = case onePat of [x] -> x _ -> impossible @@ -957,7 +1036,7 @@ inferLeftAppExpression mhint e = case e of where goClause :: Expression -> LambdaClause -> Sem r LambdaClause goClause ty cl@LambdaClause {..} = do - (pats', body') <- checkClause (getLoc cl) ty (toList _lambdaPatterns) _lambdaBody + (pats', body') <- checkClauseExpression (getLoc cl) ty (toList _lambdaPatterns) _lambdaBody return LambdaClause { _lambdaPatterns = nonEmpty' pats', @@ -1588,16 +1667,29 @@ guessPatternArgArity p = arityLet :: (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => Let -> Sem r Arity arityLet l = guessArity (l ^. letExpression) --- | All branches should have the same arity. If they are all the same, we --- return that, otherwise we return ArityBlocking. Probably something better can --- be done. +-- | If all arities are the same, we return that, otherwise we return +-- ArityNotKnown. Probably something better can be done. +arityBranches :: NonEmpty Arity -> Arity +arityBranches l + | allSame l = head l + | otherwise = ArityNotKnown + +-- | All branches should have the same arity. arityCase :: (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => Case -> Sem r Arity -arityCase c = do - aris <- mapM (guessArity . (^. caseBranchExpression)) (c ^. caseBranches) - return - if - | allSame aris -> head aris - | otherwise -> ArityNotKnown +arityCase c = arityBranches <$> mapM (arityCaseRhs . (^. caseBranchRhs)) (c ^. caseBranches) + +aritySideIf :: (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => SideIfs -> Sem r Arity +aritySideIf SideIfs {..} = do + let bodies :: NonEmpty Expression = + snocNonEmptyMaybe + ((^. sideIfBranchBody) <$> _sideIfBranches) + _sideIfElse + arityBranches <$> mapM guessArity bodies + +arityCaseRhs :: (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => CaseBranchRhs -> Sem r Arity +arityCaseRhs = \case + CaseBranchRhsExpression e -> guessArity e + CaseBranchRhsIf s -> aritySideIf s idenArity :: (Members '[Inference, Reader LocalVars, Reader InfoTable] r) => Iden -> Sem r Arity idenArity = \case diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs index 55c7ecd73a..6f8a4e2194 100644 --- a/src/Juvix/Data/CodeAnn.hs +++ b/src/Juvix/Data/CodeAnn.hs @@ -100,6 +100,9 @@ kwColon = keyword Str.colon kwData :: Doc Ann kwData = keyword Str.data_ +kwIf :: Doc Ann +kwIf = keyword Str.if_ + kwAssign :: Doc Ann kwAssign = keyword Str.assignAscii diff --git a/src/Juvix/Prelude/Base/Foundation.hs b/src/Juvix/Prelude/Base/Foundation.hs index 56399dfa30..090caf97e8 100644 --- a/src/Juvix/Prelude/Base/Foundation.hs +++ b/src/Juvix/Prelude/Base/Foundation.hs @@ -348,6 +348,14 @@ combineMaps mps = -- List -------------------------------------------------------------------------------- +snocMaybe :: [a] -> Maybe a -> [a] +snocMaybe l = \case + Nothing -> l + Just x -> snoc l x + +snocNonEmptyMaybe :: NonEmpty a -> Maybe a -> NonEmpty a +snocNonEmptyMaybe (h :| t) m = h :| snocMaybe t m + revAppend :: [a] -> [a] -> [a] revAppend [] !ys = ys revAppend (x : xs) !ys = revAppend xs (x : ys) diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix index 133fbcfeee..3acfaf30e8 100644 --- a/tests/positive/Format.juvix +++ b/tests/positive/Format.juvix @@ -427,6 +427,25 @@ fff {f7 : List Nat} : Nat := zero; +module SideIfConditions; + singleCaseBr : Nat := + case 12 of + _ + | if 0 < 0 := 3 + | else := 4; + + multiCaseBr : Nat := + case 12 of + | zero + | if 0 < 0 := 3 + | if 0 > 0 := 6 + | else := 4 + | suc (suc n) + | if 0 < 0 := 3 + | else := n + | suc n if 0 < 0 := 3; +end; + module PublicImports; module Inner;