parsing and printing deriving kw

src/Juvix/Compiler/Concrete/Extra.hs

@@ -108,6 +108,6 @@ isBodyExpression = \case
   SigBodyExpression {} -> True
   SigBodyClauses {} -> False
 
-isFunctionLike :: FunctionDef a -> Bool
+isFunctionLike :: FunctionDef 'Parsed -> Bool
 isFunctionLike = \case
-  FunctionDef {..} -> not (null _signArgs) || not (isBodyExpression _signBody)
+  FunctionDef {..} -> not (null _signArgs) || maybe False (not . isBodyExpression) _signBody

src/Juvix/Compiler/Concrete/Gen.hs

@@ -24,21 +24,27 @@ simplestFunctionDefParsed funNameTxt funBody = do
   funName <- symbol funNameTxt
   return (simplestFunctionDef funName (mkExpressionAtoms funBody))
 
-simplestFunctionDef :: FunctionName s -> ExpressionType s -> FunctionDef s
+simplestFunctionDef :: forall s. (SingI s) => FunctionName s -> ExpressionType s -> FunctionDef s
 simplestFunctionDef funName funBody =
   FunctionDef
     { _signName = funName,
-      _signBody = SigBodyExpression funBody,
+      _signBody = body,
       _signColonKw = Irrelevant Nothing,
       _signArgs = [],
       _signRetType = Nothing,
       _signDoc = Nothing,
       _signPragmas = Nothing,
       _signBuiltin = Nothing,
       _signTerminating = Nothing,
+      _signDeriving = Nothing,
       _signInstance = Nothing,
       _signCoercion = Nothing
     }
+  where
+    body :: FunctionDefBodyType s
+    body = case sing :: SStage s of
+      SParsed -> Just (SigBodyExpression funBody)
+      SScoped -> SigBodyExpression funBody
 
 smallUniverseExpression :: forall s r. (SingI s) => (Members '[Reader Interval] r) => Sem r (ExpressionType s)
 smallUniverseExpression = do

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

@@ -55,6 +55,11 @@ type family FieldArgIxType s = res | res -> s where
   FieldArgIxType 'Parsed = ()
   FieldArgIxType 'Scoped = Int
 
+type FunctionDefBodyType :: Stage -> GHCType
+type family FunctionDefBodyType s = res | res -> s where
+  FunctionDefBodyType 'Parsed = Maybe (FunctionDefBody 'Parsed)
+  FunctionDefBodyType 'Scoped = FunctionDefBody 'Scoped
+
 type SideIfBranchConditionType :: Stage -> IfBranchKind -> GHCType
 type family SideIfBranchConditionType s k = res where
   SideIfBranchConditionType s 'BranchIfBool = ExpressionType s
@@ -653,8 +658,10 @@ data FunctionDef (s :: Stage) = FunctionDef
     _signDoc :: Maybe (Judoc s),
     _signPragmas :: Maybe ParsedPragmas,
     _signBuiltin :: Maybe (WithLoc BuiltinFunction),
-    _signBody :: FunctionDefBody s,
+    -- | Only deriving instances can omit the body
+    _signBody :: FunctionDefBodyType s,
     _signTerminating :: Maybe KeywordRef,
+    _signDeriving :: Maybe KeywordRef,
     _signInstance :: Maybe KeywordRef,
     _signCoercion :: Maybe KeywordRef
   }
@@ -2807,6 +2814,7 @@ data FunctionLhs (s :: Stage) = FunctionLhs
   { _funLhsBuiltin :: Maybe (WithLoc BuiltinFunction),
     _funLhsTerminating :: Maybe KeywordRef,
     _funLhsInstance :: Maybe KeywordRef,
+    _funLhsDeriving :: Maybe KeywordRef,
     _funLhsCoercion :: Maybe KeywordRef,
     _funLhsName :: FunctionName s,
     _funLhsArgs :: [SigArg s],
@@ -2911,6 +2919,7 @@ functionDefLhs FunctionDef {..} =
       _funLhsCoercion = _signCoercion,
       _funLhsName = _signName,
       _funLhsArgs = _signArgs,
+      _funLhsDeriving = _signDeriving,
       _funLhsColonKw = _signColonKw,
       _funLhsRetType = _signRetType
     }
@@ -3310,8 +3319,17 @@ instance (SingI s) => HasLoc (FunctionDef s) where
       ?<> (getLoc <$> _signPragmas)
       ?<> (getLoc <$> _signBuiltin)
       ?<> (getLoc <$> _signTerminating)
-      ?<> getLocSymbolType _signName
-      <> getLoc _signBody
+      ?<> ( getLocSymbolType _signName
+              <>? (getLocFunctionDefBodyType _signBody)
+          )
+
+getFunctionDefBodyType :: forall s. (SingI s) => FunctionDefBodyType s -> Maybe (FunctionDefBody s)
+getFunctionDefBodyType m = case sing :: SStage s of
+  SParsed -> m
+  SScoped -> Just m
+
+getLocFunctionDefBodyType :: forall s. (SingI s) => FunctionDefBodyType s -> Maybe Interval
+getLocFunctionDefBodyType = fmap getLoc . getFunctionDefBodyType
 
 instance HasLoc (Example s) where
   getLoc e = e ^. exampleLoc

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

@@ -1147,7 +1147,9 @@ instance (SingI s) => PrettyPrint (FunctionLhs s) where
   ppCode FunctionLhs {..} = do
     let termin' = (<> line) . ppCode <$> _funLhsTerminating
         coercion' = (<> if isJust instance' then space else line) . ppCode <$> _funLhsCoercion
-        instance' = (<> line) . ppCode <$> _funLhsInstance
+        instance' = case _funLhsDeriving of
+          Nothing -> (<> line) . ppCode <$> _funLhsInstance
+          Just derKw -> Just (ppCode derKw <+> ppCode (fromJust _funLhsInstance) <> line)
         builtin' = (<> line) . ppCode <$> _funLhsBuiltin
         margs' = fmap ppCode <$> nonEmpty _funLhsArgs
         mtype' = case _funLhsColonKw ^. unIrrelevant of
@@ -1171,9 +1173,10 @@ instance (SingI s) => PrettyPrint (FunctionDef s) where
     let doc' :: Maybe (Sem r ()) = ppCode <$> _signDoc
         pragmas' :: Maybe (Sem r ()) = ppCode <$> _signPragmas
         sig' = ppCode (functionDefLhs fun)
-        body' = case _signBody of
-          SigBodyExpression e -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppTopExpressionType e)
-          SigBodyClauses k -> line <> indent (vsep (ppCode <$> k))
+        body' = case getFunctionDefBodyType _signBody of
+          Nothing -> return ()
+          Just (SigBodyExpression e) -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppTopExpressionType e)
+          Just (SigBodyClauses k) -> line <> indent (vsep (ppCode <$> k))
     doc'
       ?<> pragmas'
       ?<> sig'

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

@@ -1124,7 +1124,7 @@ checkFunctionDef fdef@FunctionDef {..} = do
             ..
           }
     checkBody :: Sem r (FunctionDefBody 'Scoped)
-    checkBody = case _signBody of
+    checkBody = case fromJust _signBody of -- FIXME
       SigBodyExpression e -> SigBodyExpression <$> checkParseExpressionAtoms e
       SigBodyClauses cls -> SigBodyClauses <$> mapM checkClause cls
 

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

@@ -1282,7 +1282,11 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
   unless (allowInstance || isNothing _funLhsCoercion) $
     parseFailure off "coercion not allowed here"
   off0 <- P.getOffset
-  _funLhsInstance <- optional (kw kwInstance)
+  _funLhsDeriving <- optional (kw kwDeriving)
+  _funLhsInstance <-
+    if
+        | isJust _funLhsDeriving -> Just <$> kw kwInstance
+        | otherwise -> optional (kw kwInstance)
   unless (allowInstance || isNothing _funLhsInstance) $
     parseFailure off0 "instance not allowed here"
   when (isJust _funLhsCoercion && isNothing _funLhsInstance) $
@@ -1301,6 +1305,7 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
   return
     FunctionLhs
       { _funLhsInstance,
+        _funLhsDeriving,
         _funLhsBuiltin,
         _funLhsCoercion,
         _funLhsName,
@@ -1361,16 +1366,20 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
   off <- P.getOffset
   _signDoc <- getJudoc
   _signPragmas <- getPragmas
-  _signBody <- parseBody
+  _signBody <-
+    if
+        | isJust _funLhsDeriving -> return Nothing
+        | otherwise -> Just <$> parseBody
   unless
     ( isJust (_funLhsColonKw ^. unIrrelevant)
-        || (P.isBodyExpression _signBody && null _funLhsArgs)
+        || (maybe True P.isBodyExpression _signBody && null _funLhsArgs)
     )
     $ parseFailure off "expected result type"
   return
     FunctionDef
       { _signName = _funLhsName,
         _signArgs = _funLhsArgs,
+        _signDeriving = _funLhsDeriving,
         _signColonKw = _funLhsColonKw,
         _signRetType = _funLhsRetType,
         _signTerminating = _funLhsTerminating,

src/Juvix/Compiler/Pipeline/Package/Loader.hs

@@ -83,18 +83,22 @@ toConcrete t p = run . runReader l $ do
       _signRetType <- Just <$> expressionAtoms' (packageTypeIdentifier :| [])
       _signName <- symbol Str.package
       _signColonKw <- Irrelevant . Just <$> kw kwColon
-      let _signBody = (t ^. packageDescriptionTypeTransform) p
+      let _signBody = Just ((t ^. packageDescriptionTypeTransform) p)
       return
         ( StatementFunctionDef
             FunctionDef
               { _signTerminating = Nothing,
                 _signPragmas = Nothing,
                 _signInstance = Nothing,
+                _signDeriving = Nothing,
                 _signDoc = Nothing,
                 _signCoercion = Nothing,
                 _signBuiltin = Nothing,
                 _signArgs = [],
-                ..
+                _signRetType,
+                _signName,
+                _signColonKw,
+                _signBody
               }
         )