Allow type signatures to have a body (#1785)

- 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
};
```

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

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

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)

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

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)

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

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"

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.

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
   ]

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")
   ]

tests/negative/DuplicateClause.juvix

@@ -0,0 +1,10 @@
+module DuplicateClause;
+
+axiom T : Type;
+
+id : T → T := λ {
+  t := t
+};
+id t := t;
+
+end;

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;