Add deriving for Eq (#3176)

This pr adds automatic implementation of `Eq` instances for inductive
types. To create such an instance the user will use the same syntax as a
regular instance with two differences.
1. It is prefixed with the `deriving` keyword.
2. It has no body.

E.g. 
```
deriving instance
eqProductI {A B} {{Eq A}} {{Eq B}} : Eq (Pair A B);
```

This desugars into an instance that returns true when the constructors
match and all arguments are equal according to their respective
instances. There is no special handling of type errors occurring in the
generated code. I.e. if the user forgets a necessary instance argument
in the type signature, a type error will occur in the generated code.

## Stdlib PR
- anoma/juvix-stdlib#148

# Future work
* In the future we should look at
https://www.dreixel.net/research/pdf/gdmh_nocolor.pdf
* See also:
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/generic-deriving

---------

Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>

src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs

@@ -423,6 +423,7 @@ goStatement = \case
   StatementInductive t -> goInductive t
   StatementOpenModule t -> goOpen t
   StatementFunctionDef t -> goFunctionDef t
+  StatementDeriving t -> goDeriving t
   StatementSyntax syn -> goSyntax syn
   StatementImport t -> goImport t
   StatementModule m -> goLocalModule m
@@ -537,13 +538,15 @@ goAxiom axiom = do
     axiomHeader :: Sem r Html
     axiomHeader = ppCodeHtml defaultOptions (set axiomDoc Nothing axiom)
 
+goDeriving :: forall r. (Members '[Reader HtmlOptions] r) => Deriving 'Scoped -> Sem r Html
+goDeriving def = do
+  sig <- ppHelper (ppCode def)
+  defHeader (def ^. derivingFunLhs . funLhsName) sig Nothing
+
 goFunctionDef :: forall r. (Members '[Reader HtmlOptions] r) => FunctionDef 'Scoped -> Sem r Html
 goFunctionDef def = do
-  sig' <- funSig
-  defHeader (def ^. signName) sig' (def ^. signDoc)
-  where
-    funSig :: Sem r Html
-    funSig = ppHelper (ppCode (functionDefLhs def))
+  sig <- ppHelper (ppCode (functionDefLhs def))
+  defHeader (def ^. signName) sig (def ^. signDoc)
 
 goInductive :: forall r. (Members '[Reader HtmlOptions] r) => InductiveDef 'Scoped -> Sem r Html
 goInductive def = do

src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs

@@ -213,12 +213,13 @@ indModuleFilter :: forall s. [Concrete.Statement s] -> [Concrete.Statement s]
 indModuleFilter =
   filter
     ( \case
-        Concrete.StatementSyntax _ -> True
-        Concrete.StatementFunctionDef _ -> True
-        Concrete.StatementImport _ -> True
-        Concrete.StatementInductive _ -> True
         Concrete.StatementModule o -> o ^. Concrete.moduleOrigin == LocalModuleSource
-        Concrete.StatementOpenModule _ -> True
-        Concrete.StatementAxiom _ -> True
-        Concrete.StatementProjectionDef _ -> True
+        Concrete.StatementSyntax {} -> True
+        Concrete.StatementFunctionDef {} -> True
+        Concrete.StatementDeriving {} -> True
+        Concrete.StatementImport {} -> True
+        Concrete.StatementInductive {} -> True
+        Concrete.StatementOpenModule {} -> True
+        Concrete.StatementAxiom {} -> True
+        Concrete.StatementProjectionDef {} -> True
     )

src/Juvix/Compiler/Builtins.hs

@@ -1,6 +1,7 @@
 module Juvix.Compiler.Builtins
   ( module Juvix.Compiler.Builtins.Nat,
     module Juvix.Compiler.Builtins.IO,
+    module Juvix.Compiler.Builtins.Eq,
     module Juvix.Compiler.Builtins.Int,
     module Juvix.Compiler.Builtins.Bool,
     module Juvix.Compiler.Builtins.List,
@@ -24,6 +25,7 @@ import Juvix.Compiler.Builtins.ByteArray
 import Juvix.Compiler.Builtins.Cairo
 import Juvix.Compiler.Builtins.Control
 import Juvix.Compiler.Builtins.Debug
+import Juvix.Compiler.Builtins.Eq
 import Juvix.Compiler.Builtins.Field
 import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Int

src/Juvix/Compiler/Builtins/Eq.hs

@@ -0,0 +1,25 @@
+module Juvix.Compiler.Builtins.Eq where
+
+import Juvix.Compiler.Internal.Builtins
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+import Juvix.Prelude.Pretty
+
+checkEqDef :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
+checkEqDef d = do
+  let err :: forall a. Text -> Sem r a
+      err = builtinsErrorText (getLoc d)
+  let eqTxt = prettyText BuiltinEq
+  unless (isSmallUniverse' (d ^. inductiveType)) (err (eqTxt <> " should be in the small universe"))
+  case d ^. inductiveParameters of
+    [_] -> return ()
+    _ -> err (eqTxt <> " should have exactly one type parameter")
+  case d ^. inductiveConstructors of
+    [c1] -> checkMkEq c1
+    _ -> err (eqTxt <> " should have exactly two constructors")
+
+checkMkEq :: ConstructorDef -> Sem r ()
+checkMkEq _ = return ()
+
+checkIsEq :: FunctionDef -> Sem r ()
+checkIsEq _ = return ()

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -59,6 +59,7 @@ builtinConstructors = \case
   BuiltinEcPoint -> [BuiltinMkEcPoint]
   BuiltinAnomaResource -> [BuiltinMkAnomaResource]
   BuiltinAnomaAction -> [BuiltinMkAnomaAction]
+  BuiltinEq -> [BuiltinMkEq]
 
 data BuiltinInductive
   = BuiltinNat
@@ -67,6 +68,7 @@ data BuiltinInductive
   | BuiltinList
   | BuiltinMaybe
   | BuiltinPair
+  | BuiltinEq
   | BuiltinPoseidonState
   | BuiltinEcPoint
   | BuiltinAnomaResource
@@ -87,6 +89,7 @@ instance Pretty BuiltinInductive where
     BuiltinList -> Str.list
     BuiltinMaybe -> Str.maybe_
     BuiltinPair -> Str.pair
+    BuiltinEq -> Str.eq
     BuiltinPoseidonState -> Str.cairoPoseidonState
     BuiltinEcPoint -> Str.cairoEcPoint
     BuiltinAnomaResource -> Str.anomaResource
@@ -109,6 +112,7 @@ instance Pretty BuiltinConstructor where
     BuiltinMkEcPoint -> Str.cairoMkEcPoint
     BuiltinMkAnomaResource -> Str.anomaMkResource
     BuiltinMkAnomaAction -> Str.anomaMkAction
+    BuiltinMkEq -> Str.mkEq
 
 data BuiltinConstructor
   = BuiltinNatZero
@@ -119,6 +123,7 @@ data BuiltinConstructor
   | BuiltinIntNegSuc
   | BuiltinListNil
   | BuiltinListCons
+  | BuiltinMkEq
   | BuiltinMaybeNothing
   | BuiltinMaybeJust
   | BuiltinPairConstr
@@ -161,6 +166,7 @@ data BuiltinFunction
   | BuiltinIntLe
   | BuiltinIntLt
   | BuiltinFromNat
+  | BuiltinIsEqual
   | BuiltinFromInt
   | BuiltinSeq
   | BuiltinMonadBind
@@ -202,6 +208,7 @@ instance Pretty BuiltinFunction where
     BuiltinFromNat -> Str.fromNat
     BuiltinFromInt -> Str.fromInt
     BuiltinSeq -> Str.builtinSeq
+    BuiltinIsEqual -> Str.isEqual
     BuiltinMonadBind -> Str.builtinMonadBind
 
 data BuiltinAxiom
@@ -434,6 +441,7 @@ isNatBuiltin = \case
   BuiltinNatLt -> True
   BuiltinNatEq -> True
   --
+  BuiltinIsEqual -> False
   BuiltinAssert -> False
   BuiltinBoolIf -> False
   BuiltinBoolOr -> False
@@ -486,13 +494,15 @@ isIntBuiltin = \case
   BuiltinFromNat -> False
   BuiltinFromInt -> False
   BuiltinSeq -> False
+  BuiltinIsEqual -> False
   BuiltinMonadBind -> False
 
 isCastBuiltin :: BuiltinFunction -> Bool
 isCastBuiltin = \case
   BuiltinFromNat -> True
   BuiltinFromInt -> True
   --
+  BuiltinIsEqual -> False
   BuiltinAssert -> False
   BuiltinIntEq -> False
   BuiltinIntPlus -> False
@@ -532,6 +542,7 @@ isIgnoredBuiltin f
         .&&. (not . isIntBuiltin)
         .&&. (not . isCastBuiltin)
         .&&. (/= BuiltinMonadBind)
+        .&&. (/= BuiltinIsEqual)
         $ f
 
     explicit :: Bool
@@ -562,6 +573,8 @@ isIgnoredBuiltin f
       BuiltinNatLe -> False
       BuiltinNatLt -> False
       BuiltinNatEq -> False
+      -- Eq
+      BuiltinIsEqual -> False
       -- Monad
       BuiltinMonadBind -> False
       -- Ignored

src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs

@@ -28,7 +28,7 @@ data InfoTableBuilder :: Effect where
   RegisterRecordInfo :: S.NameId -> RecordInfo -> InfoTableBuilder m ()
   RegisterAlias :: S.NameId -> PreSymbolEntry -> InfoTableBuilder m ()
   RegisterLocalModule :: ScopedModule -> InfoTableBuilder m ()
-  GetInfoTable :: InfoTableBuilder m InfoTable
+  GetBuilderInfoTable :: InfoTableBuilder m InfoTable
   GetBuiltinSymbol' :: Interval -> BuiltinPrim -> InfoTableBuilder m S.Symbol
   RegisterBuiltin' :: BuiltinPrim -> S.Symbol -> InfoTableBuilder m ()
 
@@ -92,7 +92,7 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case
     modify (over infoScoperAlias (HashMap.insert uid a))
   RegisterLocalModule m ->
     mapM_ (uncurry registerBuiltinHelper) (m ^. scopedModuleInfoTable . infoBuiltins . to HashMap.toList)
-  GetInfoTable ->
+  GetBuilderInfoTable ->
     get
   GetBuiltinSymbol' i b -> do
     tbl <- get @InfoTable
@@ -154,15 +154,19 @@ anameFromScopedIden s =
     }
 
 lookupInfo :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r a
-lookupInfo f = do
-  tab1 <- ask
-  fromMaybe (fromJust (f tab1)) . f <$> getInfoTable
+lookupInfo f = fromJust <$> lookupInfo' f
+
+lookupInfo' :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r (Maybe a)
+lookupInfo' f = do
+  tab1 <- getBuilderInfoTable
+  tab2 <- ask
+  return (f tab1 <|> f tab2)
 
 lookupFixity :: (Members '[InfoTableBuilder, Reader InfoTable] r) => S.NameId -> Sem r FixityDef
-lookupFixity uid = lookupInfo (HashMap.lookup uid . (^. infoFixities))
+lookupFixity uid = lookupInfo (^. infoFixities . at uid)
 
 getPrecedenceGraph :: (Members '[InfoTableBuilder, Reader InfoTable] r) => Sem r PrecedenceGraph
 getPrecedenceGraph = do
   tab <- ask
-  tab' <- getInfoTable
+  tab' <- getBuilderInfoTable
   return $ combinePrecedenceGraphs (tab ^. infoPrecedenceGraph) (tab' ^. infoPrecedenceGraph)

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

@@ -15,6 +15,7 @@ where
 
 import Juvix.Compiler.Concrete.Data.NameSignature.Error
 import Juvix.Compiler.Concrete.Gen qualified as Gen
+import Juvix.Compiler.Concrete.Language.Base
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
 import Juvix.Prelude
 
@@ -63,8 +64,11 @@ instance (SingI s) => HasNameSignature s (AxiomDef s) where
   addArgs :: (Members '[NameSignatureBuilder s] r) => AxiomDef s -> Sem r ()
   addArgs a = addArgs (a ^. axiomTypeSig)
 
+instance (SingI s) => HasNameSignature s (FunctionLhs s) where
+  addArgs FunctionLhs {..} = addArgs _funLhsTypeSig
+
 instance (SingI s) => HasNameSignature s (FunctionDef s) where
-  addArgs a = addArgs (a ^. signTypeSig)
+  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,7 @@ groupStatements = \case
     -- blank line
     g :: Statement s -> Statement s -> Bool
     g a b = case (a, b) of
+      (StatementDeriving _, _) -> False
       (StatementSyntax _, StatementSyntax _) -> True
       (StatementSyntax (SyntaxFixity _), _) -> False
       (StatementSyntax (SyntaxOperator o), s) -> definesSymbol (o ^. opSymbol) s
@@ -108,6 +110,9 @@ isBodyExpression = \case
   SigBodyExpression {} -> True
   SigBodyClauses {} -> False
 
-isFunctionLike :: FunctionDef a -> Bool
-isFunctionLike = \case
-  FunctionDef {..} -> not (null (_signTypeSig ^. typeSigArgs)) || not (isBodyExpression _signBody)
+isLhsFunctionLike :: FunctionLhs 'Parsed -> Bool
+isLhsFunctionLike FunctionLhs {..} = notNull (_funLhsTypeSig ^. typeSigArgs)
+
+isFunctionLike :: FunctionDef 'Parsed -> Bool
+isFunctionLike d@FunctionDef {..} =
+  isLhsFunctionLike (functionDefLhs d) || (not . isBodyExpression) _signBody

src/Juvix/Compiler/Concrete/Keywords.hs

@@ -36,6 +36,7 @@ import Juvix.Data.Keyword.All
     kwCase,
     kwCoercion,
     kwColon,
+    kwDeriving,
     kwDo,
     kwElse,
     kwEnd,
@@ -85,6 +86,7 @@ reservedKeywords :: [Keyword]
 reservedKeywords =
   [ delimSemicolon,
     kwAssign,
+    kwDeriving,
     kwAt,
     kwAtQuestion,
     kwAxiom,

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)