From 38622b28d1eac1c26dc49222f559eab69c012719 Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Tue, 31 Jan 2023 09:46:53 +0100 Subject: [PATCH] Allow type signatures to have a body (#1785) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Closes #1637. A function type signature is now allowed to have a body. This is valid for both top level and let definitions. ``` not : Bool -> Bool := λ { | true := false | false := true }; ``` --- .../Abstract/Translation/FromConcrete.hs | 78 +++++++++++-------- src/Juvix/Compiler/Concrete/Language.hs | 2 + src/Juvix/Compiler/Concrete/Pretty/Base.hs | 3 +- src/Juvix/Compiler/Concrete/Print/Base.hs | 4 + .../FromParsed/Analysis/Scoping.hs | 13 +--- .../FromParsed/Analysis/Scoping/Error.hs | 2 + .../Analysis/Scoping/Error/Types.hs | 29 +++++++ .../Concrete/Translation/FromSource.hs | 1 + test/Scope/Negative.hs | 7 ++ test/Scope/Positive.hs | 6 +- tests/negative/DuplicateClause.juvix | 10 +++ tests/positive/SignatureWithBody.juvix | 15 ++++ 12 files changed, 124 insertions(+), 46 deletions(-) create mode 100644 tests/negative/DuplicateClause.juvix create mode 100644 tests/positive/SignatureWithBody.juvix diff --git a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs index c55ff5732..1ef00a401 100644 --- a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs @@ -128,14 +128,11 @@ goModuleBody ss' = do [ Indexed i <$> funDef | Indexed i sig <- sigs, let name = sig ^. sigName, - let funDef = goFunctionDef sig (getClauses name) + let funDef = goTopFunctionDef sig (getClauses name) ] where - getClauses :: S.Symbol -> NonEmpty (FunctionClause 'Scoped) - getClauses name = - fromMaybe impossible $ - nonEmpty - [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction] + getClauses :: S.Symbol -> [FunctionClause 'Scoped] + getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction] sigs :: [Indexed (TypeSignature 'Scoped)] sigs = [Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss] @@ -171,23 +168,53 @@ goOpenModule o _ -> impossible | otherwise = return Nothing -goFunctionDef :: - forall r. - (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) => +goLetFunctionDef :: + (Members '[InfoTableBuilder, Error ScoperError] r) => TypeSignature 'Scoped -> - NonEmpty (FunctionClause 'Scoped) -> + [FunctionClause 'Scoped] -> Sem r Abstract.FunctionDef -goFunctionDef TypeSignature {..} clauses = do +goLetFunctionDef = goFunctionDefHelper + +goFunctionDefHelper :: + forall r. + (Members '[InfoTableBuilder, Error ScoperError] r) => + TypeSignature 'Scoped -> + [FunctionClause 'Scoped] -> + Sem r Abstract.FunctionDef +goFunctionDefHelper sig@TypeSignature {..} clauses = do let _funDefName = goSymbol _sigName _funDefTerminating = isJust _sigTerminating _funDefBuiltin = (^. withLocParam) <$> _sigBuiltin - _funDefClauses <- mapM goFunctionClause clauses _funDefTypeSig <- goExpression _sigType _funDefExamples <- goExamples _sigDoc + _funDefClauses <- case (_sigBody, nonEmpty clauses) of + (Nothing, Nothing) -> throw (ErrLacksFunctionClause (LacksFunctionClause sig)) + (Just {}, Just clauses') -> throw (ErrDuplicateFunctionClause (DuplicateFunctionClause sig (head clauses'))) + (Just body, Nothing) -> do + body' <- goExpression body + return + ( pure + Abstract.FunctionClause + { _clauseName = _funDefName, + _clausePatterns = [], + _clauseBody = body' + } + ) + (Nothing, Just clauses') -> mapM goFunctionClause clauses' let fun = Abstract.FunctionDef {..} - whenJust _sigBuiltin (registerBuiltinFunction fun . (^. withLocParam)) registerFunction' fun +goTopFunctionDef :: + forall r. + (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) => + TypeSignature 'Scoped -> + [FunctionClause 'Scoped] -> + Sem r Abstract.FunctionDef +goTopFunctionDef sig clauses = do + fun <- goFunctionDefHelper sig clauses + whenJust (sig ^. sigBuiltin) (registerBuiltinFunction fun . (^. withLocParam)) + return fun + goExamples :: forall r. (Members '[Error ScoperError, InfoTableBuilder] r) => @@ -352,27 +379,12 @@ goExpression = \case nonEmpty' <$> sequence [Abstract.LetFunDef <$> goSig sig | LetTypeSig sig <- toList cl] where goSig :: TypeSignature 'Scoped -> Sem r Abstract.FunctionDef - goSig sig = do - _funDefClauses <- getClauses - _funDefTypeSig <- goExpression (sig ^. sigType) - let _funDefBuiltin = (^. withLocParam) <$> sig ^. sigBuiltin - _funDefTerminating = isJust (sig ^. sigTerminating) - _funDefName = goSymbol (sig ^. sigName) - _funDefExamples :: [Abstract.Example] = [] - registerFunction' Abstract.FunctionDef {..} + goSig sig = goLetFunctionDef sig getClauses where - getClauses :: Sem r (NonEmpty Abstract.FunctionClause) - getClauses = do - cls <- - sequence - [ goFunctionClause c | LetFunClause c <- toList cl, sig ^. sigName == c ^. clauseOwnerFunction - ] - case nonEmpty cls of - Nothing -> - throw - ( ErrLacksFunctionClause (LacksFunctionClause sig) - ) - Just r -> return r + getClauses :: [FunctionClause 'Scoped] + getClauses = + [ c | LetFunClause c <- toList cl, sig ^. sigName == c ^. clauseOwnerFunction + ] goApplication :: Application -> Sem r Abstract.Application goApplication (Application l arg) = do diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 3c475ec94..7ad015b36 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -186,6 +186,7 @@ data TypeSignature (s :: Stage) = TypeSignature _sigType :: ExpressionType s, _sigDoc :: Maybe (Judoc s), _sigBuiltin :: Maybe (WithLoc BuiltinFunction), + _sigBody :: Maybe (ExpressionType s), _sigTerminating :: Maybe KeywordRef } @@ -1078,6 +1079,7 @@ instance SingI s => HasLoc (TypeSignature s) where (_sigDoc >>= getJudocLoc) ?<> (getLoc <$> _sigBuiltin) ?<> (getLoc <$> _sigTerminating) + ?<> (getLocExpressionType <$> _sigBody) ?<> getLocExpressionType _sigType instance HasLoc (Example s) where diff --git a/src/Juvix/Compiler/Concrete/Pretty/Base.hs b/src/Juvix/Compiler/Concrete/Pretty/Base.hs index d23e833bf..e95d4e276 100644 --- a/src/Juvix/Compiler/Concrete/Pretty/Base.hs +++ b/src/Juvix/Compiler/Concrete/Pretty/Base.hs @@ -439,7 +439,8 @@ instance (SingI s) => PrettyCode (TypeSignature s) where sigType' <- ppExpression _sigType builtin' <- traverse ppCode _sigBuiltin doc' <- mapM ppCode _sigDoc - return $ doc' ?<> builtin' sigTerminating' <> hang' (sigName' <+> kwColon <+> sigType') + body' :: Maybe (Doc Ann) <- fmap (kwAssign <+>) <$> mapM ppExpression _sigBody + return $ doc' ?<> builtin' sigTerminating' <> hang' (sigName' <+> kwColon <+> sigType' <+?> body') instance (SingI s) => PrettyCode (Function s) where ppCode :: forall r. (Members '[Reader Options] r) => Function s -> Sem r (Doc Ann) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 5026cf83e..045d9acf2 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -187,6 +187,9 @@ instance PrettyPrint (TypeSignature 'Scoped) where builtin' :: Maybe (Sem r ()) = ppCode <$> _sigBuiltin type' = ppCode _sigType name' = region (P.annDef _sigName) (ppCode _sigName) + body' = case _sigBody of + Nothing -> Nothing + Just body -> Just (noLoc P.kwAssign <+> ppCode body) doc' ?<> builtin' termin' @@ -194,6 +197,7 @@ instance PrettyPrint (TypeSignature 'Scoped) where ( name' <+> noLoc P.kwColon <+> type' + <+?> body' ) instance PrettyPrint Pattern where diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index a8ab59654..29266ce3e 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -421,7 +421,8 @@ checkTypeSignature TypeSignature {..} = do sigType' <- checkParseExpressionAtoms _sigType sigName' <- bindFunctionSymbol _sigName sigDoc' <- mapM checkJudoc _sigDoc - registerFunction' TypeSignature {_sigName = sigName', _sigType = sigType', _sigDoc = sigDoc', ..} + sigBody' <- mapM checkParseExpressionAtoms _sigBody + registerFunction' TypeSignature {_sigName = sigName', _sigType = sigType', _sigDoc = sigDoc', _sigBody = sigBody', ..} checkConstructorDef :: (Members '[Error ScoperError, Reader LocalVars, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => @@ -588,7 +589,6 @@ checkModuleBody :: checkModuleBody body = do body' <- mapM checkStatement body checkOrphanFixities - checkClausesExist body' exported <- get >>= exportScope return (exported, body') @@ -635,15 +635,6 @@ checkLocalModule Module {..} = do inheritEntry :: SymbolEntry -> SymbolEntry inheritEntry = entryOverName (over S.nameWhyInScope S.BecauseInherited . set S.nameVisibilityAnn VisPrivate) -checkClausesExist :: forall r. (Members '[Error ScoperError, State Scope] r) => [Statement 'Scoped] -> Sem r () -checkClausesExist ss = whenJust msig (throw . ErrLacksFunctionClause . LacksFunctionClause) - where - msig = - listToMaybe - [ ts | StatementTypeSignature ts <- ss, null - [c | StatementFunctionClause c <- ss, c ^. clauseOwnerFunction == ts ^. sigName] - ] - checkOrphanFixities :: forall r. (Members '[Error ScoperError, State Scope] r) => Sem r () checkOrphanFixities = do path <- gets (^. scopePath) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs index 6aec404f6..534961fa5 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -17,6 +17,7 @@ data ScoperError | ErrMultipleDeclarations MultipleDeclarations | ErrLacksTypeSig LacksTypeSig | ErrLacksFunctionClause LacksFunctionClause + | ErrDuplicateFunctionClause DuplicateFunctionClause | ErrImportCycle ImportCycle | ErrSymNotInScope NotInScope | ErrQualSymNotInScope QualSymNotInScope @@ -41,6 +42,7 @@ data ScoperError instance ToGenericError ScoperError where genericError = \case + ErrDuplicateFunctionClause e -> genericError e ErrInfixParser e -> genericError e ErrAppLeftImplicit e -> genericError e ErrInfixPattern e -> genericError e diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs index a22458f26..e15a932d4 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs @@ -722,3 +722,32 @@ instance ToGenericError ConstructorExpectedLeftApplication where msg = "Constructor expected on the left of a pattern application:" <+> ppCode opts' pat + +data DuplicateFunctionClause = DuplicateFunctionClause + { _duplicateFunctionClauseSignature :: TypeSignature 'Scoped, + _duplicateFunctionClauseClause :: FunctionClause 'Scoped + } + deriving stock (Show) + +makeLenses ''DuplicateFunctionClause + +instance ToGenericError DuplicateFunctionClause where + genericError e = ask >>= generr + where + generr opts = + return + GenericError + { _genericErrorLoc = clLoc, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [clLoc, sigLoc] + } + where + opts' = fromGenericOptions opts + cl :: FunctionClause 'Scoped + cl = e ^. duplicateFunctionClauseClause + name :: S.Symbol + name = e ^. duplicateFunctionClauseSignature . sigName + clLoc = getLoc (cl ^. clauseOwnerFunction) + sigLoc = getLoc name + msg = + "The function" <+> ppCode opts' name <+> "has already been assigned a definition and so it cannot have additional clauses" diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 3c0a0a654..b7e3cad2f 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -447,6 +447,7 @@ typeSignature _sigTerminating _sigName _sigBuiltin = do kw kwColon _sigType <- parseExpressionAtoms _sigDoc <- getJudoc + _sigBody <- optional (kw kwAssign >> parseExpressionAtoms) return TypeSignature {..} -- | Used to minimize the amount of required @P.try@s. diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index 9fdf44270..9a3859716 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -254,5 +254,12 @@ scoperErrorTests = $(mkRelFile "DuplicateInductiveParameterName.juvix") $ \case ErrDuplicateInductiveParameterName {} -> Nothing + _ -> wrongError, + NegTest + "A function has a duplicate clause" + $(mkRelDir ".") + $(mkRelFile "DuplicateClause.juvix") + $ \case + ErrDuplicateFunctionClause {} -> Nothing _ -> wrongError ] diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs index f6dea730f..9404150f0 100644 --- a/test/Scope/Positive.hs +++ b/test/Scope/Positive.hs @@ -216,5 +216,9 @@ tests = PosTest "Builtin bool" $(mkRelDir ".") - $(mkRelFile "BuiltinsBool.juvix") + $(mkRelFile "BuiltinsBool.juvix"), + PosTest + "Type signature with body" + $(mkRelDir ".") + $(mkRelFile "SignatureWithBody.juvix") ] diff --git a/tests/negative/DuplicateClause.juvix b/tests/negative/DuplicateClause.juvix new file mode 100644 index 000000000..85747f10d --- /dev/null +++ b/tests/negative/DuplicateClause.juvix @@ -0,0 +1,10 @@ +module DuplicateClause; + +axiom T : Type; + +id : T → T := λ { + t := t +}; +id t := t; + +end; diff --git a/tests/positive/SignatureWithBody.juvix b/tests/positive/SignatureWithBody.juvix new file mode 100644 index 000000000..f6264c161 --- /dev/null +++ b/tests/positive/SignatureWithBody.juvix @@ -0,0 +1,15 @@ +module SignatureWithBody; + open import Stdlib.Prelude; + + isNull : {A : Type} → List A → Bool := λ { + | nil := true + | _ := false + }; + + isNull' : {A : Type} → List A → Bool := let { + aux : {A : Type} → List A → Bool := λ { + | nil := true + | _ := false + }; + } in aux; +end;