From a8f4acaca2af0d380ba09c5538d5814dc6c1c739 Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Wed, 20 Jul 2022 11:33:52 +0300 Subject: [PATCH] Curly braces are allowed nested in patterns (#1380) --- src/Juvix/Syntax/Abstract/Language.hs | 12 ++- src/Juvix/Syntax/Abstract/Language/Extra.hs | 73 +++++++++------- src/Juvix/Syntax/Concrete/Language.hs | 28 ++++--- .../Syntax/Concrete/Scoped/Pretty/Base.hs | 9 +- src/Juvix/Syntax/Concrete/Scoped/Scoper.hs | 83 +++++++++++-------- src/Juvix/Syntax/IsImplicit.hs | 6 ++ src/Juvix/Syntax/MicroJuvix/ArityChecker.hs | 69 ++++++++------- .../Syntax/MicroJuvix/ArityChecker/Error.hs | 4 +- .../MicroJuvix/ArityChecker/Error/Types.hs | 24 ++++-- src/Juvix/Syntax/MicroJuvix/Language.hs | 21 +++-- src/Juvix/Syntax/MicroJuvix/Language/Extra.hs | 40 ++++----- src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs | 15 +++- src/Juvix/Syntax/MicroJuvix/TypeChecker.hs | 32 ++++--- src/Juvix/Termination/FunctionCall.hs | 2 +- src/Juvix/Termination/Types/SizeInfo.hs | 15 ++-- src/Juvix/Translation/AbstractToMicroJuvix.hs | 14 +++- src/Juvix/Translation/MicroJuvixToMiniC.hs | 10 ++- .../Translation/MicroJuvixToMiniC/Base.hs | 12 ++- .../Translation/MicroJuvixToMonoJuvix.hs | 20 +++-- src/Juvix/Translation/ScopedToAbstract.hs | 31 +++++-- test/Arity/Negative.hs | 2 +- test/TypeCheck/Negative.hs | 7 ++ tests/negative/258/M.juvix | 11 +++ tests/negative/258/juvix.yaml | 0 tests/negative/issue1337/Braces.juvix | 11 +++ tests/negative/issue1337/juvix.yaml | 0 26 files changed, 354 insertions(+), 197 deletions(-) create mode 100644 tests/negative/258/M.juvix create mode 100644 tests/negative/258/juvix.yaml create mode 100644 tests/negative/issue1337/Braces.juvix create mode 100644 tests/negative/issue1337/juvix.yaml diff --git a/src/Juvix/Syntax/Abstract/Language.hs b/src/Juvix/Syntax/Abstract/Language.hs index eee42076f..ea22791de 100644 --- a/src/Juvix/Syntax/Abstract/Language.hs +++ b/src/Juvix/Syntax/Abstract/Language.hs @@ -60,7 +60,7 @@ data FunctionDef = FunctionDef data FunctionClause = FunctionClause { _clauseName :: FunctionName, - _clausePatterns :: [Pattern], + _clausePatterns :: [PatternArg], _clauseBody :: Expression } deriving stock (Eq, Show) @@ -152,7 +152,13 @@ instance HasAtomicity Function where -- | Fully applied constructor in a pattern. data ConstructorApp = ConstructorApp { _constrAppConstructor :: ConstructorRef, - _constrAppParameters :: [Pattern] + _constrAppParameters :: [PatternArg] + } + deriving stock (Eq, Show) + +data PatternArg = PatternArg + { _patternArgIsImplicit :: IsImplicit, + _patternArgPattern :: Pattern } deriving stock (Eq, Show) @@ -161,7 +167,6 @@ data Pattern | PatternConstructorApp ConstructorApp | PatternWildcard Wildcard | PatternEmpty - | PatternBraces Pattern deriving stock (Eq, Show) data InductiveDef = InductiveDef @@ -187,6 +192,7 @@ data AxiomDef = AxiomDef deriving stock (Eq, Show) makeLenses ''Module +makeLenses ''PatternArg makeLenses ''FunctionParameter makeLenses ''Function makeLenses ''FunctionDef diff --git a/src/Juvix/Syntax/Abstract/Language/Extra.hs b/src/Juvix/Syntax/Abstract/Language/Extra.hs index 830c0871a..26b601767 100644 --- a/src/Juvix/Syntax/Abstract/Language/Extra.hs +++ b/src/Juvix/Syntax/Abstract/Language/Extra.hs @@ -17,16 +17,18 @@ data ApplicationArg = ApplicationArg makeLenses ''ApplicationArg -patternVariables :: Pattern -> [VarName] -patternVariables = \case - PatternVariable v -> [v] - PatternWildcard {} -> [] - PatternEmpty {} -> [] - PatternBraces b -> patternVariables b - PatternConstructorApp app -> appVariables app +patternVariables :: Traversal' Pattern VarName +patternVariables f p = case p of + PatternVariable v -> PatternVariable <$> f v + PatternWildcard {} -> pure p + PatternEmpty {} -> pure p + PatternConstructorApp app -> PatternConstructorApp <$> appVariables f app -appVariables :: ConstructorApp -> [VarName] -appVariables (ConstructorApp _ ps) = concatMap patternVariables ps +patternArgVariables :: Traversal' PatternArg VarName +patternArgVariables f = traverseOf patternArgPattern (patternVariables f) + +appVariables :: Traversal' ConstructorApp VarName +appVariables f = traverseOf constrAppParameters (traverse (patternArgVariables f)) idenName :: Iden -> Name idenName = \case @@ -36,25 +38,35 @@ idenName = \case IdenInductive (InductiveRef i) -> i IdenAxiom (AxiomRef a) -> a -smallerPatternVariables :: Pattern -> [VarName] -smallerPatternVariables = \case - PatternVariable {} -> [] - PatternBraces b -> smallerPatternVariables b - PatternWildcard {} -> [] - PatternEmpty {} -> [] - PatternConstructorApp app -> appVariables app +smallerPatternVariables :: Traversal' Pattern VarName +smallerPatternVariables f p = case p of + PatternVariable {} -> pure p + PatternWildcard {} -> pure p + PatternEmpty {} -> pure p + PatternConstructorApp app -> PatternConstructorApp <$> appVariables f app -viewApp :: Expression -> (Expression, [Expression]) -viewApp e = case e of - ExpressionApplication (Application l r _) -> - second (`snoc` r) (viewApp l) - _ -> (e, []) +viewApp :: Expression -> (Expression, [ApplicationArg]) +viewApp e = + case e of + ExpressionApplication (Application l r i) -> + second (`snoc` ApplicationArg i r) (viewApp l) + _ -> (e, []) + +viewAppArgAsPattern :: ApplicationArg -> Maybe PatternArg +viewAppArgAsPattern a = do + p' <- viewExpressionAsPattern (a ^. appArg) + return + ( PatternArg + { _patternArgIsImplicit = a ^. appArgIsImplicit, + _patternArgPattern = p' + } + ) viewExpressionAsPattern :: Expression -> Maybe Pattern viewExpressionAsPattern e = case viewApp e of (f, args) | Just c <- getConstructor f -> do - args' <- mapM viewExpressionAsPattern args + args' <- mapM viewAppArgAsPattern args Just $ PatternConstructorApp (ConstructorApp c args') (f, []) | Just v <- getVariable f -> Just (PatternVariable v) @@ -200,13 +212,16 @@ isSmallUniverse' = \case ExpressionUniverse u -> isSmallUniverse u _ -> False -toApplicationArg :: Pattern -> ApplicationArg -toApplicationArg = \case - PatternVariable v -> ApplicationArg Explicit (toExpression v) - PatternConstructorApp a -> ApplicationArg Explicit (toExpression a) - PatternEmpty -> impossible - PatternBraces p -> set appArgIsImplicit Implicit (toApplicationArg p) - PatternWildcard _ -> error "TODO" +toApplicationArg :: PatternArg -> ApplicationArg +toApplicationArg p = + set appArgIsImplicit (p ^. patternArgIsImplicit) (helper (p ^. patternArgPattern)) + where + helper :: Pattern -> ApplicationArg + helper = \case + PatternVariable v -> ApplicationArg Explicit (toExpression v) + PatternConstructorApp a -> ApplicationArg Explicit (toExpression a) + PatternEmpty -> impossible + PatternWildcard _ -> error "TODO" clauseLhsAsExpression :: FunctionClause -> Expression clauseLhsAsExpression cl = diff --git a/src/Juvix/Syntax/Concrete/Language.hs b/src/Juvix/Syntax/Concrete/Language.hs index e99325744..43f09133c 100644 --- a/src/Juvix/Syntax/Concrete/Language.hs +++ b/src/Juvix/Syntax/Concrete/Language.hs @@ -83,7 +83,7 @@ type family ExpressionType s = res | res -> s where type PatternType :: Stage -> GHC.Type type family PatternType s = res | res -> s where PatternType 'Parsed = PatternAtom 'Parsed - PatternType 'Scoped = Pattern + PatternType 'Scoped = PatternArg type family ImportType (s :: Stage) :: GHC.Type where ImportType 'Parsed = TopModulePath @@ -257,15 +257,15 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Ind -------------------------------------------------------------------------------- data PatternApp = PatternApp - { _patAppLeft :: Pattern, - _patAppRight :: Pattern + { _patAppLeft :: PatternArg, + _patAppRight :: PatternArg } deriving stock (Show, Eq, Ord) data PatternInfixApp = PatternInfixApp - { _patInfixLeft :: Pattern, + { _patInfixLeft :: PatternArg, _patInfixConstructor :: ConstructorRef, - _patInfixRight :: Pattern + _patInfixRight :: PatternArg } deriving stock (Show, Eq, Ord) @@ -273,7 +273,7 @@ instance HasFixity PatternInfixApp where getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. constructorRefName . S.nameFixity) data PatternPostfixApp = PatternPostfixApp - { _patPostfixParameter :: Pattern, + { _patPostfixParameter :: PatternArg, _patPostfixConstructor :: ConstructorRef } deriving stock (Show, Eq, Ord) @@ -281,13 +281,18 @@ data PatternPostfixApp = PatternPostfixApp instance HasFixity PatternPostfixApp where getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. constructorRefName . S.nameFixity) +data PatternArg = PatternArg + { _patternArgIsImplicit :: IsImplicit, + _patternArgPattern :: Pattern + } + deriving stock (Show, Eq, Ord) + data Pattern = PatternVariable (SymbolType 'Scoped) | PatternConstructor ConstructorRef | PatternApplication PatternApp | PatternInfixApplication PatternInfixApp | PatternPostfixApplication PatternPostfixApp - | PatternBraces Pattern | PatternWildcard Wildcard | PatternEmpty deriving stock (Show, Eq, Ord) @@ -300,7 +305,6 @@ instance HasAtomicity Pattern where PatternInfixApplication a -> Aggregate (getFixity a) PatternPostfixApplication p -> Aggregate (getFixity p) PatternWildcard {} -> Atom - PatternBraces {} -> Atom PatternEmpty -> Atom -------------------------------------------------------------------------------- @@ -887,8 +891,7 @@ data ExpressionAtoms (s :: Stage) = ExpressionAtoms _expressionAtomsLoc :: Interval } --------------------------------------------------------------------------------- - +makeLenses ''PatternArg makeLenses ''Function makeLenses ''InductiveDef makeLenses ''PostfixApplication @@ -1048,6 +1051,11 @@ instance -------------------------------------------------------------------------------- +instance HasAtomicity PatternArg where + atomicity p + | Implicit <- p ^. patternArgIsImplicit = Atom + | otherwise = atomicity (p ^. patternArgPattern) + idenOverName :: (forall s. S.Name' s -> S.Name' s) -> ScopedIden -> ScopedIden idenOverName f = \case ScopedAxiom a -> ScopedAxiom (over axiomRefName f a) diff --git a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs index ae4d2bcbe..5e89c52cc 100644 --- a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs +++ b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs @@ -448,6 +448,9 @@ instance PrettyCode QualifiedName where let symbols = _qualifiedPath ^. pathParts NonEmpty.|> _qualifiedSymbol dotted <$> mapM ppSymbol symbols +bracesIf :: Bool -> Doc Ann -> Doc Ann +bracesIf t = if t then braces else id + ppName :: forall s r. (SingI s, Members '[Reader Options] r) => IdentifierType s -> Sem r (Doc Ann) ppName = case sing :: SStage s of SParsed -> ppCode @@ -652,6 +655,11 @@ instance PrettyCode PatternScopedIden where PatternScopedVar v -> ppCode v PatternScopedConstructor c -> ppCode c +instance PrettyCode PatternArg where + ppCode a = do + p <- ppCode (a ^. patternArgPattern) + return (bracesIf (Implicit == a ^. patternArgIsImplicit) p) + instance SingI s => PrettyCode (PatternAtom s) where ppCode a = case a of PatternAtomIden n -> case sing :: SStage s of @@ -750,7 +758,6 @@ instance PrettyCode Pattern where return $ l' <+> r' PatternWildcard {} -> return kwWildcard PatternEmpty -> return $ parens mempty - PatternBraces p -> braces <$> ppCode p PatternConstructor constr -> ppCode constr PatternInfixApplication i -> ppPatternInfixApp i PatternPostfixApplication i -> ppPatternPostfixApp i diff --git a/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs b/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs index 8268cde27..b2f309c52 100644 --- a/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs +++ b/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs @@ -1198,7 +1198,7 @@ checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms checkParsePatternAtom :: Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => PatternAtom 'Parsed -> - Sem r Pattern + Sem r PatternArg checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom checkStatement :: @@ -1423,7 +1423,7 @@ parseTerm = type ParsePat = P.Parsec () [PatternAtom 'Scoped] makePatternTable :: - PatternAtom 'Scoped -> [[P.Operator ParsePat Pattern]] + PatternAtom 'Scoped -> [[P.Operator ParsePat PatternArg]] makePatternTable atom = [appOp] : operators where getConstructorRef :: PatternAtom 'Scoped -> Maybe ConstructorRef @@ -1437,24 +1437,24 @@ makePatternTable atom = [appOp] : operators constructorRefs = case atom of PatternAtomParens (PatternAtoms atoms _) -> mapMaybe getConstructorRef (toList atoms) _ -> [] - mkSymbolTable :: [ConstructorRef] -> [[P.Operator ParsePat Pattern]] + mkSymbolTable :: [ConstructorRef] -> [[P.Operator ParsePat PatternArg]] mkSymbolTable = reverse . map (map snd) . groupSortOn' fst . mapMaybe unqualifiedSymbolOp where - unqualifiedSymbolOp :: ConstructorRef -> Maybe (Precedence, P.Operator ParsePat Pattern) + unqualifiedSymbolOp :: ConstructorRef -> Maybe (Precedence, P.Operator ParsePat PatternArg) unqualifiedSymbolOp (ConstructorRef' S.Name' {..}) | Just Fixity {..} <- _nameFixity, _nameKind == S.KNameConstructor = Just $ case _fixityArity of Unary u -> (_fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId)) where - unaryApp :: ConstructorRef -> Pattern -> Pattern + unaryApp :: ConstructorRef -> PatternArg -> PatternArg unaryApp funName = case u of - AssocPostfix -> PatternPostfixApplication . (`PatternPostfixApp` funName) + AssocPostfix -> explicitP . PatternPostfixApplication . (`PatternPostfixApp` funName) Binary b -> (_fixityPrecedence, infixLRN (binaryInfixApp <$> parseSymbolId _nameId)) where - binaryInfixApp :: ConstructorRef -> Pattern -> Pattern -> Pattern - binaryInfixApp name argLeft = PatternInfixApplication . PatternInfixApp argLeft name - infixLRN :: ParsePat (Pattern -> Pattern -> Pattern) -> P.Operator ParsePat Pattern + binaryInfixApp :: ConstructorRef -> PatternArg -> PatternArg -> PatternArg + binaryInfixApp name argLeft = explicitP . PatternInfixApplication . PatternInfixApp argLeft name + infixLRN :: ParsePat (PatternArg -> PatternArg -> PatternArg) -> P.Operator ParsePat PatternArg infixLRN = case b of AssocLeft -> P.InfixL AssocRight -> P.InfixR @@ -1470,22 +1470,30 @@ makePatternTable atom = [appOp] : operators return ref -- Application by juxtaposition. - appOp :: P.Operator ParsePat Pattern + appOp :: P.Operator ParsePat PatternArg appOp = P.InfixL (return app) where - app :: Pattern -> Pattern -> Pattern + app :: PatternArg -> PatternArg -> PatternArg app l r = - PatternApplication - ( PatternApp - { _patAppLeft = l, - _patAppRight = r - } + explicitP + ( PatternApplication + ( PatternApp + { _patAppLeft = l, + _patAppRight = r + } + ) ) +explicitP :: Pattern -> PatternArg +explicitP = PatternArg Explicit + +implicitP :: Pattern -> PatternArg +implicitP = PatternArg Implicit + parsePatternTerm :: forall r. - Members '[Reader (ParsePat Pattern), Embed ParsePat] r => - Sem r Pattern + Members '[Reader (ParsePat PatternArg), Embed ParsePat] r => + Sem r PatternArg parsePatternTerm = do pPat <- ask embed @ParsePat $ @@ -1496,9 +1504,9 @@ parsePatternTerm = do <|> parseWildcard <|> parseEmpty where - parseNoInfixConstructor :: ParsePat Pattern + parseNoInfixConstructor :: ParsePat PatternArg parseNoInfixConstructor = - PatternConstructor + explicitP . PatternConstructor <$> P.token constructorNoFixity mempty where constructorNoFixity :: PatternAtom 'Scoped -> Maybe ConstructorRef @@ -1509,35 +1517,38 @@ parsePatternTerm = do n = ref ^. constructorRefName _ -> Nothing - parseWildcard :: ParsePat Pattern - parseWildcard = PatternWildcard <$> P.token isWildcard mempty + parseWildcard :: ParsePat PatternArg + parseWildcard = explicitP . PatternWildcard <$> P.token isWildcard mempty where isWildcard :: PatternAtom 'Scoped -> Maybe Wildcard isWildcard s = case s of PatternAtomWildcard i -> Just i _ -> Nothing - parseEmpty :: ParsePat Pattern - parseEmpty = PatternEmpty <$ P.satisfy isEmpty + parseEmpty :: ParsePat PatternArg + parseEmpty = explicitP PatternEmpty <$ P.satisfy isEmpty where isEmpty :: PatternAtom 'Scoped -> Bool isEmpty s = case s of PatternAtomEmpty -> True _ -> False - parseVariable :: ParsePat Pattern - parseVariable = PatternVariable <$> P.token var mempty + parseVariable :: ParsePat PatternArg + parseVariable = explicitP . PatternVariable <$> P.token var mempty where var :: PatternAtom 'Scoped -> Maybe S.Symbol var s = case s of PatternAtomIden (PatternScopedVar sym) -> Just sym _ -> Nothing - parseBraces :: ParsePat Pattern -> ParsePat Pattern + parseBraces :: ParsePat PatternArg -> ParsePat PatternArg parseBraces patternParser = do exprs <- P.token bracesPat mempty case P.parse patternParser "" exprs of - Right r -> return (PatternBraces r) + Right (PatternArg i p) + -- TODO proper error + | Implicit <- i -> error "nested braces" + | otherwise -> return (implicitP p) Left {} -> mzero where bracesPat :: PatternAtom 'Scoped -> Maybe [PatternAtom 'Scoped] @@ -1545,7 +1556,7 @@ parsePatternTerm = do PatternAtomBraces (PatternAtoms ss _) -> Just (toList ss) _ -> Nothing - parseParens :: ParsePat Pattern -> ParsePat Pattern + parseParens :: ParsePat PatternArg -> ParsePat PatternArg parseParens patternParser = do exprs <- P.token parenPat mempty case P.parse patternParser "" exprs of @@ -1560,22 +1571,22 @@ parsePatternTerm = do mkPatternParser :: forall r. Members '[Embed ParsePat] r => - [[P.Operator ParsePat Pattern]] -> - Sem r Pattern + [[P.Operator ParsePat PatternArg]] -> + Sem r PatternArg mkPatternParser table = embed @ParsePat pPattern where - pPattern :: ParsePat Pattern + pPattern :: ParsePat PatternArg pPattern = P.makeExprParser pTerm table - pTerm :: ParsePat Pattern + pTerm :: ParsePat PatternArg pTerm = runM parseTermRec where - parseTermRec :: Sem '[Embed ParsePat] Pattern + parseTermRec :: Sem '[Embed ParsePat] PatternArg parseTermRec = runReader pPattern parsePatternTerm parsePatternAtom :: Members '[Error ScoperError, State Scope] r => PatternAtom 'Scoped -> - Sem r Pattern + Sem r PatternArg parsePatternAtom sec = do case res of Left {} -> case sec of @@ -1584,7 +1595,7 @@ parsePatternAtom sec = do Right r -> return r where tbl = makePatternTable sec - parser :: ParsePat Pattern + parser :: ParsePat PatternArg parser = runM (mkPatternParser tbl) <* P.eof res = P.parse parser filePath [sec] diff --git a/src/Juvix/Syntax/IsImplicit.hs b/src/Juvix/Syntax/IsImplicit.hs index fe33b0b9f..b4e67b477 100644 --- a/src/Juvix/Syntax/IsImplicit.hs +++ b/src/Juvix/Syntax/IsImplicit.hs @@ -1,8 +1,14 @@ module Juvix.Syntax.IsImplicit where import Juvix.Prelude +import Juvix.Prelude.Pretty data IsImplicit = Explicit | Implicit deriving stock (Show, Eq, Ord, Generic) instance Hashable IsImplicit + +instance Pretty IsImplicit where + pretty = \case + Implicit -> "implicit" + Explicit -> "explicit" diff --git a/src/Juvix/Syntax/MicroJuvix/ArityChecker.hs b/src/Juvix/Syntax/MicroJuvix/ArityChecker.hs index 0bae63cd3..9c0b58775 100644 --- a/src/Juvix/Syntax/MicroJuvix/ArityChecker.hs +++ b/src/Juvix/Syntax/MicroJuvix/ArityChecker.hs @@ -163,8 +163,8 @@ checkLhs :: Interval -> Maybe Arity -> Arity -> - [Pattern] -> - Sem r ([Pattern], LocalVars, Arity) + [PatternArg] -> + Sem r ([PatternArg], LocalVars, Arity) checkLhs loc hint ariSignature pats = do (locals, (pats', bodyAri)) <- runState emptyLocalVars (goLhs ariSignature pats) return (pats', locals, bodyAri) @@ -173,7 +173,7 @@ checkLhs loc hint ariSignature pats = do -- body once all the patterns have been processed). -- Does not insert holes greedily. I.e. implicit wildcards are only inserted -- between explicit parameters already in the pattern. - goLhs :: Arity -> [Pattern] -> Sem (State LocalVars ': r) ([Pattern], Arity) + goLhs :: Arity -> [PatternArg] -> Sem (State LocalVars ': r) ([PatternArg], Arity) goLhs a = \case [] -> return $ case hint >>= tailHelper a of Nothing -> ([], a) @@ -192,25 +192,26 @@ checkLhs loc hint ariSignature pats = do p' <- checkPattern ArityUnknown p first (p' :) <$> goLhs ArityUnknown ps ArityFunction (FunctionArity l r) -> - case (getPatternBraces p, l) of - (Just b, ParamImplicit) -> do - b' <- checkPattern (arityParameter l) b + case (p ^. patternArgIsImplicit, l) of + (Implicit, ParamImplicit) -> do + b' <- checkPattern (arityParameter l) p first (b' :) <$> goLhs r ps - (Just x, ParamExplicit {}) -> + (Implicit, ParamExplicit {}) -> throw - ( ErrExpectedExplicitPattern - ExpectedExplicitPattern - { _expectedExplicitPattern = x + ( ErrWrongPatternIsImplicit + WrongPatternIsImplicit + { _wrongPatternIsImplicitExpected = Explicit, + _wrongPatternIsImplicitActual = p } ) - (Nothing, ParamImplicit) -> + (Explicit, ParamImplicit) -> first (wildcard :) <$> goLhs r lhs - (Nothing, ParamExplicit pa) -> do + (Explicit, ParamExplicit pa) -> do p' <- checkPattern pa p first (p' :) <$> goLhs r ps where - wildcard :: Pattern - wildcard = PatternBraces (PatternWildcard (Wildcard loc)) + wildcard :: PatternArg + wildcard = PatternArg Implicit (PatternWildcard (Wildcard loc)) tailHelper :: Arity -> Arity -> Maybe Int tailHelper a target @@ -220,30 +221,28 @@ checkLhs loc hint ariSignature pats = do a' = dropSuffix target' (unfoldArity a) target' = unfoldArity target - getPatternBraces :: Pattern -> Maybe Pattern - getPatternBraces p = case p of - PatternBraces {} -> Just p - _ -> Nothing - checkPattern :: + forall r. Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars] r => Arity -> - Pattern -> - Sem r Pattern -checkPattern ari = \case - PatternBraces p -> checkPattern ari p - PatternVariable v -> addArity v ari $> PatternVariable v - PatternWildcard i -> return (PatternWildcard i) - PatternConstructorApp c -> case ari of - ArityUnit -> PatternConstructorApp <$> checkConstructorApp c - ArityUnknown -> PatternConstructorApp <$> checkConstructorApp c - ArityFunction {} -> - throw - ( ErrPatternFunction - PatternFunction - { _patternFunction = c - } - ) + PatternArg -> + Sem r PatternArg +checkPattern ari = traverseOf patternArgPattern helper + where + helper :: Pattern -> Sem r Pattern + helper = \case + PatternVariable v -> addArity v ari $> PatternVariable v + PatternWildcard i -> return (PatternWildcard i) + PatternConstructorApp c -> case ari of + ArityUnit -> PatternConstructorApp <$> checkConstructorApp c + ArityUnknown -> PatternConstructorApp <$> checkConstructorApp c + ArityFunction {} -> + throw + ( ErrPatternFunction + PatternFunction + { _patternFunction = c + } + ) checkConstructorApp :: forall r. diff --git a/src/Juvix/Syntax/MicroJuvix/ArityChecker/Error.hs b/src/Juvix/Syntax/MicroJuvix/ArityChecker/Error.hs index 677b7900c..9e188aedd 100644 --- a/src/Juvix/Syntax/MicroJuvix/ArityChecker/Error.hs +++ b/src/Juvix/Syntax/MicroJuvix/ArityChecker/Error.hs @@ -10,7 +10,7 @@ import Juvix.Syntax.MicroJuvix.ArityChecker.Error.Types data ArityCheckerError = ErrWrongConstructorAppLength WrongConstructorAppLength | ErrLhsTooManyPatterns LhsTooManyPatterns - | ErrExpectedExplicitPattern ExpectedExplicitPattern + | ErrWrongPatternIsImplicit WrongPatternIsImplicit | ErrExpectedExplicitArgument ExpectedExplicitArgument | ErrPatternFunction PatternFunction | ErrTooManyArguments TooManyArguments @@ -21,7 +21,7 @@ instance ToGenericError ArityCheckerError where genericError = \case ErrWrongConstructorAppLength e -> genericError e ErrLhsTooManyPatterns e -> genericError e - ErrExpectedExplicitPattern e -> genericError e + ErrWrongPatternIsImplicit e -> genericError e ErrExpectedExplicitArgument e -> genericError e ErrPatternFunction e -> genericError e ErrTooManyArguments e -> genericError e diff --git a/src/Juvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs b/src/Juvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs index f62bed818..255355386 100644 --- a/src/Juvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs +++ b/src/Juvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs @@ -40,7 +40,7 @@ instance ToGenericError WrongConstructorAppLength where | otherwise = pretty n newtype LhsTooManyPatterns = LhsTooManyPatterns - { _lhsTooManyPatternsRemaining :: NonEmpty Pattern + { _lhsTooManyPatternsRemaining :: NonEmpty PatternArg } makeLenses ''LhsTooManyPatterns @@ -65,13 +65,14 @@ instance ToGenericError LhsTooManyPatterns where | n == 1 = "was" | otherwise = "were" -newtype ExpectedExplicitPattern = ExpectedExplicitPattern - { _expectedExplicitPattern :: Pattern +data WrongPatternIsImplicit = WrongPatternIsImplicit + { _wrongPatternIsImplicitExpected :: IsImplicit, + _wrongPatternIsImplicitActual :: PatternArg } -makeLenses ''ExpectedExplicitPattern +makeLenses ''WrongPatternIsImplicit -instance ToGenericError ExpectedExplicitPattern where +instance ToGenericError WrongPatternIsImplicit where genericError e = GenericError { _genericErrorLoc = i, @@ -79,10 +80,17 @@ instance ToGenericError ExpectedExplicitPattern where _genericErrorIntervals = [i] } where - i = getLoc (e ^. expectedExplicitPattern) + i = getLoc (e ^. wrongPatternIsImplicitActual) + expec = e ^. wrongPatternIsImplicitExpected + found = e ^. wrongPatternIsImplicitActual . patternArgIsImplicit + pat = e ^. wrongPatternIsImplicitActual msg = - "Expected an explicit pattern but found an implicit pattern" - <+> ppCode (e ^. expectedExplicitPattern) + "Expected an" + <+> pretty expec + <+> "pattern but found an" + <+> pretty found + <+> "pattern:" + <+> ppCode pat data ExpectedExplicitArgument = ExpectedExplicitArgument { _expectedExplicitArgumentApp :: (Expression, [(IsImplicit, Expression)]), diff --git a/src/Juvix/Syntax/MicroJuvix/Language.hs b/src/Juvix/Syntax/MicroJuvix/Language.hs index 2accb5e5e..2403290ef 100644 --- a/src/Juvix/Syntax/MicroJuvix/Language.hs +++ b/src/Juvix/Syntax/MicroJuvix/Language.hs @@ -57,7 +57,7 @@ data FunctionDef = FunctionDef data FunctionClause = FunctionClause { _clauseName :: FunctionName, - _clausePatterns :: [Pattern], + _clausePatterns :: [PatternArg], _clauseBody :: Expression } @@ -113,14 +113,18 @@ instance Hashable Application where -- | Fully applied constructor in a pattern. data ConstructorApp = ConstructorApp { _constrAppConstructor :: Name, - _constrAppParameters :: [Pattern] + _constrAppParameters :: [PatternArg] + } + +data PatternArg = PatternArg + { _patternArgIsImplicit :: IsImplicit, + _patternArgPattern :: Pattern } data Pattern = PatternVariable VarName | PatternConstructorApp ConstructorApp | PatternWildcard Wildcard - | PatternBraces Pattern newtype InductiveParameter = InductiveParameter { _inductiveParamName :: VarName @@ -157,6 +161,7 @@ data Function = Function instance Hashable Function makeLenses ''Module +makeLenses ''PatternArg makeLenses ''Include makeLenses ''FunctionDef makeLenses ''FunctionClause @@ -191,12 +196,16 @@ instance HasAtomicity ConstructorApp where | null args = Atom | otherwise = Aggregate appFixity +instance HasAtomicity PatternArg where + atomicity p + | Implicit <- p ^. patternArgIsImplicit = Atom + | otherwise = atomicity (p ^. patternArgPattern) + instance HasAtomicity Pattern where atomicity p = case p of PatternConstructorApp a -> atomicity a PatternVariable {} -> Atom PatternWildcard {} -> Atom - PatternBraces {} -> Atom instance HasLoc FunctionParameter where getLoc f = v (getLoc (f ^. paramType)) @@ -232,9 +241,11 @@ instance HasLoc Pattern where getLoc = \case PatternVariable v -> getLoc v PatternConstructorApp a -> getLoc a - PatternBraces p -> getLoc p PatternWildcard i -> getLoc i +instance HasLoc PatternArg where + getLoc = getLoc . (^. patternArgPattern) + instance HasLoc ConstructorApp where getLoc (ConstructorApp c ps) = case last <$> nonEmpty ps of diff --git a/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs b/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs index 71100725c..872370073 100644 --- a/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs +++ b/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs @@ -244,27 +244,28 @@ renameToSubsE = fmap (ExpressionIden . IdenVar) renameExpression :: Rename -> Expression -> Expression renameExpression r = substitutionE (renameToSubsE r) -patternVariables :: Pattern -> [VarName] -patternVariables = \case - PatternVariable v -> [v] - PatternConstructorApp a -> goApp a - PatternBraces b -> patternVariables b - PatternWildcard {} -> [] +patternArgVariables :: Traversal' PatternArg VarName +patternArgVariables f = traverseOf patternArgPattern (patternVariables f) + +patternVariables :: Traversal' Pattern VarName +patternVariables f p = case p of + PatternVariable v -> PatternVariable <$> f v + PatternConstructorApp a -> PatternConstructorApp <$> goApp f a + PatternWildcard {} -> pure p where - goApp :: ConstructorApp -> [VarName] - goApp (ConstructorApp _ ps) = concatMap patternVariables ps + goApp :: Traversal' ConstructorApp VarName + goApp g = traverseOf constrAppParameters (traverse (patternArgVariables g)) + +renamePatternArg :: Rename -> PatternArg -> PatternArg +renamePatternArg = over patternArgPattern . renamePattern renamePattern :: Rename -> Pattern -> Pattern -renamePattern m = go +renamePattern m = over patternVariables renameVar where - go :: Pattern -> Pattern - go p = case p of - PatternVariable v - | Just v' <- m ^. at v -> PatternVariable v' - PatternConstructorApp a -> PatternConstructorApp (goApp a) - _ -> p - goApp :: ConstructorApp -> ConstructorApp - goApp (ConstructorApp c ps) = ConstructorApp c (map go ps) + renameVar :: VarName -> VarName + renameVar v + | Just v' <- m ^. at v = v' + | otherwise = v inductiveTypeVarsAssoc :: Foldable f => InductiveDef -> f a -> HashMap VarName a inductiveTypeVarsAssoc def l @@ -275,6 +276,7 @@ inductiveTypeVarsAssoc def l vars :: [VarName] vars = def ^.. inductiveParameters . each . inductiveParamName +-- TODO remove this after monojuvix is gone functionTypeVarsAssoc :: forall a f. Foldable f => FunctionDef -> f a -> HashMap VarName a functionTypeVarsAssoc def l = sig <> mconcatMap clause (def ^. funDefClauses) where @@ -297,8 +299,8 @@ functionTypeVarsAssoc def l = sig <> mconcatMap clause (def ^. funDefClauses) clauseVars :: [Maybe VarName] clauseVars = take n (map patternVar (c ^. clausePatterns)) where - patternVar :: Pattern -> Maybe VarName - patternVar = \case + patternVar :: PatternArg -> Maybe VarName + patternVar a = case a ^. patternArgPattern of PatternVariable v -> Just v _ -> Nothing diff --git a/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs index 32bd3170a..3576d30d9 100644 --- a/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs +++ b/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs @@ -199,6 +199,11 @@ instance PrettyCode InductiveDef where rhs <- indent' $ align $ concatWith (\a b -> a <> line <> kwPipe <+> b) inductiveConstructors' return $ kwData <+> inductiveName' <+?> params <+> kwEquals <> line <> rhs +instance PrettyCode PatternArg where + ppCode a = do + p <- ppCode (a ^. patternArgPattern) + return (bracesIf (Implicit == a ^. patternArgIsImplicit) p) + instance PrettyCode ConstructorApp where ppCode c = do constr' <- ppCode (c ^. constrAppConstructor) @@ -210,7 +215,6 @@ instance PrettyCode Pattern where PatternVariable v -> ppCode v PatternConstructorApp a -> ppCode a PatternWildcard {} -> return kwWildcard - PatternBraces b -> braces <$> ppCode b instance PrettyCode FunctionDef where ppCode f = do @@ -327,8 +331,11 @@ instance PrettyCode TypeCalls where elems' <- mapM ppCode elems return $ title <> line <> vsep elems' <> line -parensCond :: Bool -> Doc Ann -> Doc Ann -parensCond t d = if t then parens d else d +parensIf :: Bool -> Doc Ann -> Doc Ann +parensIf t = if t then parens else id + +bracesIf :: Bool -> Doc Ann -> Doc Ann +bracesIf t = if t then braces else id ppPostExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => @@ -358,7 +365,7 @@ ppLRExpression :: a -> Sem r (Doc Ann) ppLRExpression associates fixlr e = - parensCond (atomParens associates (atomicity e) fixlr) + parensIf (atomParens associates (atomicity e) fixlr) <$> ppCode e ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann) diff --git a/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs b/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs index 87df20ef3..79d42e82f 100644 --- a/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs +++ b/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs @@ -174,9 +174,9 @@ checkFunctionClause info FunctionClause {..} = do where clauseType :: Expression clauseType = info ^. functionInfoDef . funDefType - helper :: [Pattern] -> Expression -> Sem r (LocalVars, Expression) + helper :: [PatternArg] -> Expression -> Sem r (LocalVars, Expression) helper pats ty = runState emptyLocalVars (go pats ty) - go :: [Pattern] -> Expression -> Sem (State LocalVars ': r) Expression + go :: [PatternArg] -> Expression -> Sem (State LocalVars ': r) Expression go pats bodyTy = case pats of [] -> return bodyTy (p : ps) -> case bodyTy of @@ -200,26 +200,38 @@ checkFunctionClause info FunctionClause {..} = do typeOfArg :: FunctionParameter -> Expression typeOfArg = (^. paramType) +matchIsImplicit :: Member (Error TypeCheckerError) r => IsImplicit -> PatternArg -> Sem r () +matchIsImplicit expected actual = + unless + (expected == actual ^. patternArgIsImplicit) + ( throw + ( ErrArity + ( ErrWrongPatternIsImplicit + WrongPatternIsImplicit + { _wrongPatternIsImplicitExpected = expected, + _wrongPatternIsImplicitActual = actual + } + ) + ) + ) + checkPattern :: forall r. Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference, NameIdGen] r => FunctionName -> FunctionParameter -> - Pattern -> + PatternArg -> Sem r () checkPattern funName = go where - go :: FunctionParameter -> Pattern -> Sem r () - go argTy p = do + go :: FunctionParameter -> PatternArg -> Sem r () + go argTy patArg = do + matchIsImplicit (argTy ^. paramImplicit) patArg tyVarMap <- fmap (ExpressionIden . IdenVar) . (^. localTyMap) <$> get ty <- normalizeType (substitutionE tyVarMap (typeOfArg argTy)) - let unbrace = \case - PatternBraces b -> b - x -> x - pat = unbrace p + let pat = patArg ^. patternArgPattern case pat of PatternWildcard {} -> return () - PatternBraces {} -> impossible PatternVariable v -> do modify (addType v ty) registerIden v ty diff --git a/src/Juvix/Termination/FunctionCall.hs b/src/Juvix/Termination/FunctionCall.hs index 9c99fac02..0c80c703a 100644 --- a/src/Juvix/Termination/FunctionCall.hs +++ b/src/Juvix/Termination/FunctionCall.hs @@ -42,7 +42,7 @@ viewCall = \case return $ case s of Nothing -> CallRow Nothing Just s' -> CallRow (Just (s', REq)) - _ -> return (CallRow Nothing) + Nothing -> return (CallRow Nothing) ExpressionIden (IdenFunction x) -> return (Just (singletonCall x)) _ -> return Nothing diff --git a/src/Juvix/Termination/Types/SizeInfo.hs b/src/Juvix/Termination/Types/SizeInfo.hs index 05e7ec5c5..2728b1daa 100644 --- a/src/Juvix/Termination/Types/SizeInfo.hs +++ b/src/Juvix/Termination/Types/SizeInfo.hs @@ -20,15 +20,16 @@ emptySizeInfo = _sizeSmaller = mempty } -mkSizeInfo :: [Pattern] -> SizeInfo +mkSizeInfo :: [PatternArg] -> SizeInfo mkSizeInfo ps = SizeInfo {..} where - ps' = filter (not . isBrace) ps - isBrace = \case - PatternBraces {} -> True - _ -> False - _sizeEqual = ps + ps' :: [Pattern] + ps' = map (^. patternArgPattern) (filter (not . isBrace) ps) + isBrace :: PatternArg -> Bool + isBrace = (== Implicit) . (^. patternArgIsImplicit) + _sizeEqual = map (^. patternArgPattern) ps + _sizeSmaller :: HashMap VarName Int _sizeSmaller = HashMap.fromList - [ (v, i) | (i, p) <- zip [0 ..] ps', v <- smallerPatternVariables p + [ (v, i) | (i, p) <- zip [0 ..] ps', v <- p ^.. smallerPatternVariables ] diff --git a/src/Juvix/Translation/AbstractToMicroJuvix.hs b/src/Juvix/Translation/AbstractToMicroJuvix.hs index d48b58ba6..10ad4296c 100644 --- a/src/Juvix/Translation/AbstractToMicroJuvix.hs +++ b/src/Juvix/Translation/AbstractToMicroJuvix.hs @@ -163,7 +163,7 @@ goFunctionDef f = do goFunctionClause :: Name -> Abstract.FunctionClause -> Sem r FunctionClause goFunctionClause n c = do _clauseBody' <- goExpression (c ^. Abstract.clauseBody) - _clausePatterns' <- mapM goPattern (c ^. Abstract.clausePatterns) + _clausePatterns' <- mapM goPatternArg (c ^. Abstract.clausePatterns) return FunctionClause { _clauseName = n, @@ -171,17 +171,25 @@ goFunctionClause n c = do _clauseBody = _clauseBody' } +goPatternArg :: Abstract.PatternArg -> Sem r PatternArg +goPatternArg p = do + pat' <- goPattern (p ^. Abstract.patternArgPattern) + return + PatternArg + { _patternArgIsImplicit = p ^. Abstract.patternArgIsImplicit, + _patternArgPattern = pat' + } + goPattern :: Abstract.Pattern -> Sem r Pattern goPattern p = case p of Abstract.PatternVariable v -> return (PatternVariable v) Abstract.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c Abstract.PatternWildcard i -> return (PatternWildcard i) - Abstract.PatternBraces b -> PatternBraces <$> goPattern b Abstract.PatternEmpty -> unsupported "pattern empty" goConstructorApp :: Abstract.ConstructorApp -> Sem r ConstructorApp goConstructorApp c = do - _constrAppParameters' <- mapM goPattern (c ^. Abstract.constrAppParameters) + _constrAppParameters' <- mapM goPatternArg (c ^. Abstract.constrAppParameters) return ConstructorApp { _constrAppConstructor = c ^. Abstract.constrAppConstructor . Abstract.constructorRefName, diff --git a/src/Juvix/Translation/MicroJuvixToMiniC.hs b/src/Juvix/Translation/MicroJuvixToMiniC.hs index 97f2cbccc..da7eb728b 100644 --- a/src/Juvix/Translation/MicroJuvixToMiniC.hs +++ b/src/Juvix/Translation/MicroJuvixToMiniC.hs @@ -315,11 +315,17 @@ goFunctionClause funSig argTyps clause = do projCtor :: Text -> Expression projCtor ctorArg = functionCall (ExpressionVar (asProjName ctorArg ctorName)) [castToType ty arg] subConditions :: Sem r [Expression] - subConditions = fmap concat (zipWithM patternCondition (map projCtor ctorArgs) _constrAppParameters) + subConditions = + fmap + concat + ( zipWithM + patternCondition + (map projCtor ctorArgs) + (_constrAppParameters ^.. each . Micro.patternArgPattern) + ) fmap (isCtor :) subConditions Micro.PatternVariable {} -> return [] Micro.PatternWildcard {} -> return [] - Micro.PatternBraces b -> patternCondition arg b clauseCondition :: Sem r (Maybe Expression) clauseCondition = fmap (foldr1 f) . nonEmpty <$> conditions diff --git a/src/Juvix/Translation/MicroJuvixToMiniC/Base.hs b/src/Juvix/Translation/MicroJuvixToMiniC/Base.hs index e1949890a..4ccd7ca34 100644 --- a/src/Juvix/Translation/MicroJuvixToMiniC/Base.hs +++ b/src/Juvix/Translation/MicroJuvixToMiniC/Base.hs @@ -174,7 +174,14 @@ typeOfConstructor name = do getInductiveCType (info ^. Micro.constructorInfoInductive) getClausePatterns :: Member (Reader Micro.TypesTable) r => Micro.FunctionClause -> Sem r [Micro.Pattern] -getClausePatterns c = filterCompileTimeArgsOrPatterns (c ^. Micro.clauseName) (c ^. Micro.clausePatterns) +getClausePatterns c = + filterCompileTimeArgsOrPatterns + (c ^. Micro.clauseName) + ( c + ^.. Micro.clausePatterns + . each + . Micro.patternArgPattern + ) functionInfoPatternsNum :: Member (Reader Micro.TypesTable) r => Micro.FunctionInfo -> Sem r Int functionInfoPatternsNum fInfo = do @@ -203,9 +210,8 @@ buildPatternInfoTable argTyps c = return [(v ^. Micro.nameText, BindingInfo {_bindingInfoExpr = exp, _bindingInfoType = typ})] Micro.PatternConstructorApp Micro.ConstructorApp {..} -> - goConstructorApp exp _constrAppConstructor _constrAppParameters + goConstructorApp exp _constrAppConstructor (_constrAppParameters ^.. each . Micro.patternArgPattern) Micro.PatternWildcard {} -> return [] - Micro.PatternBraces b -> go (b, (exp, typ)) goConstructorApp :: Expression -> Micro.Name -> [Micro.Pattern] -> Sem r [(Text, BindingInfo)] goConstructorApp exp constructorName ps = do diff --git a/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs b/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs index 77b6a3862..4997674a7 100644 --- a/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs +++ b/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs @@ -359,7 +359,7 @@ goFunctionDefConcrete n d = do goClause :: Micro.FunctionClause -> Sem r FunctionClause goClause c = do body' <- goExpression (c ^. Micro.clauseBody) - patterns' <- zipWithM goPattern' patternTys (c ^. Micro.clausePatterns) + patterns' <- zipWithM goPatternArg patternTys (c ^. Micro.clausePatterns) return FunctionClause { _clauseName = funName, @@ -437,7 +437,7 @@ goFunctionDefPoly def poly pvars' <- mapM cloneName' pvars let localVarsRename :: Micro.Rename localVarsRename = HashMap.fromList (zipExact pvars pvars') - _clausePatterns = map (Micro.renamePattern localVarsRename) patsTail + _clausePatterns = map (Micro.renamePatternArg localVarsRename) patsTail _clauseBody = Micro.substitutionE (concreteSubsE <> Micro.renameToSubsE localVarsRename) @@ -448,19 +448,21 @@ goFunctionDefPoly def poly .. } where - patsTail :: [Micro.Pattern] + patsTail :: [Micro.PatternArg] patsTail = dropExact (length tyVars) (c ^. Micro.clausePatterns) pvars :: [Micro.VarName] - pvars = concatMap Micro.patternVariables patsTail + pvars = concatMap (^.. Micro.patternArgVariables) patsTail sig' :: Micro.ConcreteType sig' = Micro.substitutionConcrete (i ^. concreteTypeSubs) tyTail -goPattern' :: forall r. Members '[Reader ConcreteTable, Reader Micro.InfoTable] r => Micro.ConcreteType -> Micro.Pattern -> Sem r Pattern -goPattern' ty = \case +goPatternArg :: forall r. Members '[Reader ConcreteTable, Reader Micro.InfoTable] r => Micro.ConcreteType -> Micro.PatternArg -> Sem r Pattern +goPatternArg ty = goPattern ty . (^. Micro.patternArgPattern) + +goPattern :: forall r. Members '[Reader ConcreteTable, Reader Micro.InfoTable] r => Micro.ConcreteType -> Micro.Pattern -> Sem r Pattern +goPattern ty = \case Micro.PatternVariable v -> return (PatternVariable (goName v)) Micro.PatternConstructorApp capp -> PatternConstructorApp <$> goApp capp Micro.PatternWildcard {} -> return PatternWildcard - Micro.PatternBraces b -> goPattern' ty b where goApp :: Micro.ConstructorApp -> Sem r ConstructorApp goApp capp = case ty ^. Micro.unconcreteType of @@ -469,7 +471,7 @@ goPattern' ty = \case c' = goName (capp ^. Micro.constrAppConstructor) cInfo <- Micro.lookupConstructor (capp ^. Micro.constrAppConstructor) let psTysConcrete = map Micro.mkConcreteType' (cInfo ^. Micro.constructorInfoArgs) - ps' <- zipWithM goPattern' psTysConcrete (capp ^. Micro.constrAppParameters) + ps' <- zipWithM goPatternArg psTysConcrete (capp ^. Micro.constrAppParameters) return (ConstructorApp c' ps') Micro.ExpressionApplication a -> do let getInductive :: Micro.Expression -> Micro.Name @@ -493,7 +495,7 @@ goPattern' ty = \case subs = HashMap.fromList (zipExact tyParamVars (toList instanceTypes)) psTysConcrete :: [Micro.ConcreteType] psTysConcrete = map (Micro.substitutionConcrete subs) psTys - ps' <- zipWithM goPattern' psTysConcrete (capp ^. Micro.constrAppParameters) + ps' <- zipWithM goPatternArg psTysConcrete (capp ^. Micro.constrAppParameters) return (ConstructorApp c' ps') _ -> impossible diff --git a/src/Juvix/Translation/ScopedToAbstract.hs b/src/Juvix/Translation/ScopedToAbstract.hs index 351a1990c..86583edd2 100644 --- a/src/Juvix/Translation/ScopedToAbstract.hs +++ b/src/Juvix/Translation/ScopedToAbstract.hs @@ -174,7 +174,7 @@ goFunctionClause :: FunctionClause 'Scoped -> Sem r Abstract.FunctionClause goFunctionClause FunctionClause {..} = do - _clausePatterns' <- mapM goPattern _clausePatterns + _clausePatterns' <- mapM goPatternArg _clausePatterns _clauseBody' <- goExpression _clauseBody goWhereBlock _clauseWhere return @@ -360,30 +360,44 @@ goPostfixPatternApplication :: Sem r Abstract.ConstructorApp goPostfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternPostfixApplication a) -viewApp :: forall r. Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.Pattern]) +viewApp :: forall r. Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg]) viewApp = \case PatternConstructor c -> return (goConstructorRef c, []) PatternApplication (PatternApp l r) -> do - r' <- goPattern r - second (`snoc` r') <$> viewApp l + r' <- goPatternArg r + second (`snoc` r') <$> viewAppLeft l PatternInfixApplication (PatternInfixApp l c r) -> do - l' <- goPattern l - r' <- goPattern r + l' <- goPatternArg l + r' <- goPatternArg r return (goConstructorRef c, [l', r']) PatternPostfixApplication (PatternPostfixApp l c) -> do - l' <- goPattern l + l' <- goPatternArg l return (goConstructorRef c, [l']) PatternVariable {} -> err PatternWildcard {} -> err - PatternBraces {} -> err PatternEmpty {} -> err where + viewAppLeft :: PatternArg -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg]) + viewAppLeft p + -- TODO proper error + | Implicit <- p ^. patternArgIsImplicit = error "An implicit pattern cannot be on the left of an application" + | otherwise = viewApp (p ^. patternArgPattern) + -- TODO proper error err :: a err = error "constructor expected on the left of a pattern application" goConstructorRef :: ConstructorRef -> Abstract.ConstructorRef goConstructorRef (ConstructorRef' n) = Abstract.ConstructorRef (goName n) +goPatternArg :: PatternArg -> Sem r Abstract.PatternArg +goPatternArg p = do + pat' <- goPattern (p ^. patternArgPattern) + return + Abstract.PatternArg + { _patternArgIsImplicit = p ^. patternArgIsImplicit, + _patternArgPattern = pat' + } + goPattern :: Pattern -> Sem r Abstract.Pattern goPattern p = case p of PatternVariable a -> return $ Abstract.PatternVariable (goSymbol a) @@ -393,7 +407,6 @@ goPattern p = case p of PatternPostfixApplication a -> Abstract.PatternConstructorApp <$> goPostfixPatternApplication a PatternWildcard i -> return (Abstract.PatternWildcard i) PatternEmpty -> return Abstract.PatternEmpty - PatternBraces b -> Abstract.PatternBraces <$> goPattern b goAxiom :: Members '[InfoTableBuilder, Error ScoperError, Builtins] r => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef goAxiom a = do diff --git a/test/Arity/Negative.hs b/test/Arity/Negative.hs index 97b6ba67c..86a79b585 100644 --- a/test/Arity/Negative.hs +++ b/test/Arity/Negative.hs @@ -68,7 +68,7 @@ tests = "MicroJuvix" "ExpectedExplicitPattern.juvix" $ \case - ErrExpectedExplicitPattern {} -> Nothing + ErrWrongPatternIsImplicit {} -> Nothing _ -> wrongError, NegTest "Expected explicit argument" diff --git a/test/TypeCheck/Negative.hs b/test/TypeCheck/Negative.hs index c5c9461cc..499d3e3ad 100644 --- a/test/TypeCheck/Negative.hs +++ b/test/TypeCheck/Negative.hs @@ -84,6 +84,13 @@ tests = $ \case ErrWrongType {} -> Nothing _ -> wrongError, + NegTest + "Unexpected braces in pattern" + "issue1337" + "Braces.juvix" + $ \case + ErrArity (ErrWrongPatternIsImplicit {}) -> Nothing + _ -> wrongError, NegTest "Wrong return type name for a constructor of a simple data type" "MicroJuvix" diff --git a/tests/negative/258/M.juvix b/tests/negative/258/M.juvix new file mode 100644 index 000000000..79feec3bc --- /dev/null +++ b/tests/negative/258/M.juvix @@ -0,0 +1,11 @@ +module M; + +inductive Nat { + O : Nat; + S : Nat -> Nat; +}; + +fun : Nat -> Nat; +fun (S {S {x}}) := x; + +end; diff --git a/tests/negative/258/juvix.yaml b/tests/negative/258/juvix.yaml new file mode 100644 index 000000000..e69de29bb diff --git a/tests/negative/issue1337/Braces.juvix b/tests/negative/issue1337/Braces.juvix new file mode 100644 index 000000000..661545755 --- /dev/null +++ b/tests/negative/issue1337/Braces.juvix @@ -0,0 +1,11 @@ +module Braces; + +inductive Nat { + O : Nat; + S : Nat -> Nat; +}; + +fun : Nat -> Nat; +fun (S {S {x}}) := x; + +end; diff --git a/tests/negative/issue1337/juvix.yaml b/tests/negative/issue1337/juvix.yaml new file mode 100644 index 000000000..e69de29bb