wip

src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs

@@ -58,10 +58,13 @@ instance (SingI s) => HasNameSignature s (AxiomDef s) where
   addArgs :: (Members '[NameSignatureBuilder s] r) => AxiomDef s -> Sem r ()
   addArgs a = addExpressionType (a ^. axiomType)
 
-instance (SingI s) => HasNameSignature s (FunctionDef s) where
+instance (SingI s) => HasNameSignature s (FunctionLhs s) where
   addArgs a = do
-    mapM_ addSigArg (a ^. signArgs)
-    whenJust (a ^. signRetType) addExpressionType
+    mapM_ addSigArg (a ^. funLhsArgs)
+    whenJust (a ^. funLhsRetType) addExpressionType
+
+instance (SingI s) => HasNameSignature s (FunctionDef s) where
+  addArgs = addArgs . functionDefLhs
 
 instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) where
   addArgs ::

src/Juvix/Compiler/Concrete/Extra.hs

@@ -9,6 +9,7 @@ module Juvix.Compiler.Concrete.Extra
     getPatternAtomIden,
     isBodyExpression,
     isFunctionLike,
+    isLhsFunctionLike,
     symbolParsed,
   )
 where
@@ -46,6 +47,8 @@ groupStatements = \case
     -- blank line
     g :: Statement s -> Statement s -> Bool
     g a b = case (a, b) of
+      (StatementDeriving _, StatementDeriving _) -> True
+      (StatementDeriving _, _) -> False
       (StatementSyntax _, StatementSyntax _) -> True
       (StatementSyntax (SyntaxFixity _), _) -> False
       (StatementSyntax (SyntaxOperator o), s) -> definesSymbol (o ^. opSymbol) s
@@ -108,6 +111,9 @@ isBodyExpression = \case
   SigBodyExpression {} -> True
   SigBodyClauses {} -> False
 
+isLhsFunctionLike :: FunctionLhs 'Parsed -> Bool
+isLhsFunctionLike FunctionLhs {..} = not (null _funLhsArgs)
+
 isFunctionLike :: FunctionDef 'Parsed -> Bool
-isFunctionLike = \case
-  FunctionDef {..} -> not (null _signArgs) || maybe False (not . isBodyExpression) _signBody
+isFunctionLike d@FunctionDef {..} =
+   isLhsFunctionLike (functionDefLhs d) || (not . isBodyExpression) _signBody

src/Juvix/Compiler/Concrete/Gen.hs

@@ -24,27 +24,21 @@ simplestFunctionDefParsed funNameTxt funBody = do
   funName <- symbol funNameTxt
   return (simplestFunctionDef funName (mkExpressionAtoms funBody))
 
-simplestFunctionDef :: forall s. (SingI s) => FunctionName s -> ExpressionType s -> FunctionDef s
+simplestFunctionDef :: FunctionName s -> ExpressionType s -> FunctionDef s
 simplestFunctionDef funName funBody =
   FunctionDef
     { _signName = funName,
-      _signBody = body,
+      _signBody = SigBodyExpression funBody,
       _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.hs

@@ -31,6 +31,7 @@ statementLabel = \case
   StatementOpenModule {} -> Nothing
   StatementProjectionDef {} -> Nothing
   StatementFunctionDef f -> Just (f ^. signName . symbolTypeLabel)
+  StatementDeriving f -> Just (f ^. derivingFunLhs . funLhsName . symbolTypeLabel)
   StatementImport i -> Just (i ^. importModulePath . to modulePathTypeLabel)
   StatementInductive i -> Just (i ^. inductiveName . symbolTypeLabel)
   StatementModule i -> Just (i ^. modulePath . to modulePathTypeLabel)

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

@@ -55,11 +55,6 @@ 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
@@ -276,6 +271,7 @@ data NonDefinitionsSection (s :: Stage) = NonDefinitionsSection
 data Definition (s :: Stage)
   = DefinitionSyntax (SyntaxDef s)
   | DefinitionFunctionDef (FunctionDef s)
+  | DefinitionDeriving (Deriving s)
   | DefinitionInductive (InductiveDef s)
   | DefinitionAxiom (AxiomDef s)
   | DefinitionProjectionDef (ProjectionDef s)
@@ -292,6 +288,7 @@ newtype Statements (s :: Stage) = Statements
 data Statement (s :: Stage)
   = StatementSyntax (SyntaxDef s)
   | StatementFunctionDef (FunctionDef s)
+  | StatementDeriving (Deriving s)
   | StatementImport (Import s)
   | StatementInductive (InductiveDef s)
   | StatementModule (Module s 'ModuleLocal)
@@ -650,6 +647,32 @@ deriving stock instance Ord (FunctionDefBody 'Parsed)
 
 deriving stock instance Ord (FunctionDefBody 'Scoped)
 
+data Deriving (s :: Stage) = Deriving
+  { _derivingKw :: KeywordRef,
+    _derivingFunLhs :: FunctionLhs s
+  }
+  deriving stock (Generic)
+
+instance Serialize (Deriving 'Scoped)
+
+instance NFData (Deriving 'Scoped)
+
+instance Serialize (Deriving 'Parsed)
+
+instance NFData (Deriving 'Parsed)
+
+deriving stock instance Show (Deriving 'Parsed)
+
+deriving stock instance Show (Deriving 'Scoped)
+
+deriving stock instance Eq (Deriving 'Parsed)
+
+deriving stock instance Eq (Deriving 'Scoped)
+
+deriving stock instance Ord (Deriving 'Parsed)
+
+deriving stock instance Ord (Deriving 'Scoped)
+
 data FunctionDef (s :: Stage) = FunctionDef
   { _signName :: FunctionName s,
     _signArgs :: [SigArg s],
@@ -658,10 +681,8 @@ data FunctionDef (s :: Stage) = FunctionDef
     _signDoc :: Maybe (Judoc s),
     _signPragmas :: Maybe ParsedPragmas,
     _signBuiltin :: Maybe (WithLoc BuiltinFunction),
-    -- | Only deriving instances can omit the body
-    _signBody :: FunctionDefBodyType s,
+    _signBody :: FunctionDefBody s,
     _signTerminating :: Maybe KeywordRef,
-    _signDeriving :: Maybe KeywordRef,
     _signInstance :: Maybe KeywordRef,
     _signCoercion :: Maybe KeywordRef
   }
@@ -2814,13 +2835,33 @@ 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],
     _funLhsColonKw :: Irrelevant (Maybe KeywordRef),
     _funLhsRetType :: Maybe (ExpressionType s)
   }
+  deriving stock (Generic)
+
+instance Serialize (FunctionLhs 'Scoped)
+
+instance NFData (FunctionLhs 'Scoped)
+
+instance Serialize (FunctionLhs 'Parsed)
+
+instance NFData (FunctionLhs 'Parsed)
+
+deriving stock instance Show (FunctionLhs 'Parsed)
+
+deriving stock instance Show (FunctionLhs 'Scoped)
+
+deriving stock instance Eq (FunctionLhs 'Parsed)
+
+deriving stock instance Eq (FunctionLhs 'Scoped)
+
+deriving stock instance Ord (FunctionLhs 'Parsed)
+
+deriving stock instance Ord (FunctionLhs 'Scoped)
 
 makeLenses ''SideIfs
 makeLenses ''FunctionLhs
@@ -2908,6 +2949,8 @@ makeLenses ''NameBlock
 makeLenses ''NameItem
 makeLenses ''RecordInfo
 makeLenses ''MarkdownInfo
+makeLenses ''Deriving
+
 makePrisms ''NamedArgumentNew
 
 functionDefLhs :: FunctionDef s -> FunctionLhs s
@@ -2919,7 +2962,6 @@ functionDefLhs FunctionDef {..} =
       _funLhsCoercion = _signCoercion,
       _funLhsName = _signName,
       _funLhsArgs = _signArgs,
-      _funLhsDeriving = _signDeriving,
       _funLhsColonKw = _signColonKw,
       _funLhsRetType = _signRetType
     }
@@ -3083,10 +3125,16 @@ instance HasLoc (OpenModule s short) where
 instance HasLoc (ProjectionDef s) where
   getLoc = getLoc . (^. projectionConstructor)
 
+instance (SingI s) => HasLoc (Deriving s) where
+  getLoc Deriving {..} =
+    getLoc _derivingKw
+      <> getLoc _derivingFunLhs
+
 instance HasLoc (Statement 'Scoped) where
   getLoc :: Statement 'Scoped -> Interval
   getLoc = \case
     StatementSyntax t -> getLoc t
+    StatementDeriving t -> getLoc t
     StatementFunctionDef t -> getLoc t
     StatementImport t -> getLoc t
     StatementInductive t -> getLoc t
@@ -3313,23 +3361,22 @@ instance (SingI s) => HasLoc (FunctionDefBody s) where
     SigBodyExpression e -> getLocExpressionType e
     SigBodyClauses cl -> getLocSpan cl
 
+instance (SingI s) => HasLoc (FunctionLhs s) where
+  getLoc FunctionLhs {..} =
+    (getLoc <$> _funLhsBuiltin)
+      ?<> (getLoc <$> _funLhsTerminating)
+      ?<> ( getLocSymbolType _funLhsName
+              <>? (getLocExpressionType <$> _funLhsRetType)
+          )
+
 instance (SingI s) => HasLoc (FunctionDef s) where
   getLoc FunctionDef {..} =
     (getLoc <$> _signDoc)
       ?<> (getLoc <$> _signPragmas)
       ?<> (getLoc <$> _signBuiltin)
       ?<> (getLoc <$> _signTerminating)
-      ?<> ( 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
+      ?<> getLocSymbolType _signName
+      <> (getLoc _signBody)
 
 instance HasLoc (Example s) where
   getLoc e = e ^. exampleLoc

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

@@ -1143,13 +1143,16 @@ instance (SingI s) => PrettyPrint (SigArg s) where
         defaultVal = ppCode <$> _sigArgDefault
     ppCode l <> arg <+?> defaultVal <> ppCode r
 
+instance (SingI s) => PrettyPrint (Deriving s) where
+  ppCode Deriving {..} =
+    ppCode _derivingKw
+      <+> ppCode _derivingFunLhs
+
 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' = case _funLhsDeriving of
-          Nothing -> (<> line) . ppCode <$> _funLhsInstance
-          Just derKw -> Just (ppCode derKw <+> ppCode (fromJust _funLhsInstance) <> line)
+        instance' = (<> line) . ppCode <$> _funLhsInstance
         builtin' = (<> line) . ppCode <$> _funLhsBuiltin
         margs' = fmap ppCode <$> nonEmpty _funLhsArgs
         mtype' = case _funLhsColonKw ^. unIrrelevant of
@@ -1173,10 +1176,9 @@ 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 getFunctionDefBodyType _signBody of
-          Nothing -> return ()
-          Just (SigBodyExpression e) -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppTopExpressionType e)
-          Just (SigBodyClauses k) -> line <> indent (vsep (ppCode <$> k))
+        body' = case _signBody of
+          SigBodyExpression e -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppTopExpressionType e)
+          SigBodyClauses k -> line <> indent (vsep (ppCode <$> k))
     doc'
       ?<> pragmas'
       ?<> sig'
@@ -1535,6 +1537,7 @@ instance (SingI s) => PrettyPrint (Statement s) where
   ppCode = \case
     StatementSyntax s -> ppCode s
     StatementFunctionDef f -> ppCode f
+    StatementDeriving f -> ppCode f
     StatementImport i -> ppCode i
     StatementInductive i -> ppCode i
     StatementModule m -> ppCode m