wip

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/Concrete/Data/Builtins.hs

@@ -166,7 +166,7 @@ data BuiltinFunction
   | BuiltinIntLe
   | BuiltinIntLt
   | BuiltinFromNat
-  | BuiltinIsEq
+  | BuiltinIsEqual
   | BuiltinFromInt
   | BuiltinSeq
   | BuiltinMonadBind
@@ -208,7 +208,7 @@ instance Pretty BuiltinFunction where
     BuiltinFromNat -> Str.fromNat
     BuiltinFromInt -> Str.fromInt
     BuiltinSeq -> Str.builtinSeq
-    BuiltinIsEq -> Str.isEqual
+    BuiltinIsEqual -> Str.isEqual
     BuiltinMonadBind -> Str.builtinMonadBind
 
 data BuiltinAxiom
@@ -441,7 +441,7 @@ isNatBuiltin = \case
   BuiltinNatLt -> True
   BuiltinNatEq -> True
   --
-  BuiltinIsEq -> False
+  BuiltinIsEqual -> False
   BuiltinAssert -> False
   BuiltinBoolIf -> False
   BuiltinBoolOr -> False
@@ -494,15 +494,15 @@ isIntBuiltin = \case
   BuiltinFromNat -> False
   BuiltinFromInt -> False
   BuiltinSeq -> False
-  BuiltinIsEq -> False
+  BuiltinIsEqual -> False
   BuiltinMonadBind -> False
 
 isCastBuiltin :: BuiltinFunction -> Bool
 isCastBuiltin = \case
   BuiltinFromNat -> True
   BuiltinFromInt -> True
   --
-  BuiltinIsEq -> False
+  BuiltinIsEqual -> False
   BuiltinAssert -> False
   BuiltinIntEq -> False
   BuiltinIntPlus -> False
@@ -542,7 +542,7 @@ isIgnoredBuiltin f
         .&&. (not . isIntBuiltin)
         .&&. (not . isCastBuiltin)
         .&&. (/= BuiltinMonadBind)
-        .&&. (/= BuiltinIsEq)
+        .&&. (/= BuiltinIsEqual)
         $ f
 
     explicit :: Bool
@@ -574,7 +574,7 @@ isIgnoredBuiltin f
       BuiltinNatLt -> False
       BuiltinNatEq -> False
       -- Eq
-      BuiltinIsEq -> False
+      BuiltinIsEqual -> False
       -- Monad
       BuiltinMonadBind -> False
       -- Ignored

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

@@ -1052,19 +1052,108 @@ resolveIteratorSyntaxDef s@IteratorSyntaxDef {..} = do
 (@$>) :: (Functor m) => (a -> m ()) -> a -> m a
 (@$>) f a = f a $> a
 
-withFunctionDefLhs ::
-  FunctionLhs 'Parsed ->
-  (FunctionLhs 'Scoped -> Sem r a)
-  Sem r a
-withFunctionDefLhs FunctionLhs {..} checkBody = do
-  body' <- withLocalScope $ do
-    args' <- mapM checkArg _funLhsArgs
-    ret' <- mapM checkParseExpressionAtoms _funLhsRetType
-    let lhs' = FunctionLhs {
-          _funLhsArgs = args',
-          _funLhsRetType = ret'
-                           }
-    checkBody lhs'
+checkDeriving ::
+  ( Members
+      '[ State Scope,
+         Error ScoperError,
+         State ScoperState,
+         Reader ScopeParameters,
+         Reader InfoTable,
+         Reader PackageId,
+         HighlightBuilder,
+         InfoTableBuilder,
+         NameIdGen,
+         State ScoperSyntax,
+         Reader BindingStrategy
+       ]
+      r
+  ) =>
+  Deriving 'Parsed ->
+  Sem r (Deriving 'Scoped)
+checkDeriving Deriving {..} = withLocalScope $ do
+  let lhs@FunctionLhs {..} = _derivingFunLhs
+  args' <- mapM checkSigArg _funLhsArgs
+  ret' <- mapM checkParseExpressionAtoms _funLhsRetType
+  name' <-
+    if
+        | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol _funLhsName
+        | otherwise -> reserveFunctionSymbol lhs
+  let lhs' =
+        FunctionLhs
+          { _funLhsArgs = args',
+            _funLhsRetType = ret',
+            _funLhsName = name',
+            ..
+          }
+
+  return
+    Deriving
+      { _derivingFunLhs = lhs',
+        ..
+      }
+
+checkSigArg ::
+  ( Members
+      '[ State Scope,
+         Error ScoperError,
+         State ScoperState,
+         Reader ScopeParameters,
+         Reader InfoTable,
+         Reader PackageId,
+         HighlightBuilder,
+         InfoTableBuilder,
+         NameIdGen,
+         State ScoperSyntax,
+         Reader BindingStrategy
+       ]
+      r
+  ) =>
+  SigArg 'Parsed ->
+  Sem r (SigArg 'Scoped)
+checkSigArg arg@SigArg {..} = do
+  names' <- checkSigArgNames _sigArgNames
+  ty' <- mapM checkParseExpressionAtoms _sigArgType
+  default' <- case _sigArgDefault of
+    Nothing -> return Nothing
+    Just ArgDefault {..} ->
+      let err = throw (ErrWrongDefaultValue WrongDefaultValue {_wrongDefaultValue = arg})
+       in case _sigArgImplicit of
+            Explicit -> err
+            ImplicitInstance -> err
+            Implicit -> do
+              val' <- checkParseExpressionAtoms _argDefaultValue
+              return (Just ArgDefault {_argDefaultValue = val', ..})
+  return
+    SigArg
+      { _sigArgNames = names',
+        _sigArgType = ty',
+        _sigArgDefault = default',
+        ..
+      }
+
+checkSigArgNames ::
+  ( Members
+      '[ State Scope,
+         Error ScoperError,
+         State ScoperState,
+         Reader ScopeParameters,
+         Reader InfoTable,
+         Reader PackageId,
+         HighlightBuilder,
+         InfoTableBuilder,
+         NameIdGen,
+         State ScoperSyntax,
+         Reader BindingStrategy
+       ]
+      r
+  ) =>
+  SigArgNames 'Parsed ->
+  Sem r (SigArgNames 'Scoped)
+checkSigArgNames = \case
+  SigArgNamesInstance -> return SigArgNamesInstance
+  SigArgNames ns -> fmap SigArgNames . forM ns $ \case
+    ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s
+    ArgumentWildcard w -> return (ArgumentWildcard w)
 
 checkFunctionDef ::
   forall r.
@@ -1074,7 +1163,7 @@ checkFunctionDef ::
 checkFunctionDef fdef@FunctionDef {..} = do
   sigDoc' <- mapM checkJudoc _signDoc
   (args', sigType', sigBody') <- withLocalScope $ do
-    a' <- mapM checkArg _signArgs
+    a' <- mapM checkSigArg _signArgs
     t' <- mapM checkParseExpressionAtoms _signRetType
     b' <- checkBody
     return (a', t', b')
@@ -1094,34 +1183,6 @@ checkFunctionDef fdef@FunctionDef {..} = do
   registerNameSignature (sigName' ^. S.nameId) def
   registerFunctionDef @$> def
   where
-    checkSigArgNames :: SigArgNames 'Parsed -> Sem r (SigArgNames 'Scoped)
-    checkSigArgNames = \case
-      SigArgNamesInstance -> return SigArgNamesInstance
-      SigArgNames ns -> fmap SigArgNames . forM ns $ \case
-        ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s
-        ArgumentWildcard w -> return (ArgumentWildcard w)
-
-    checkArg :: SigArg 'Parsed -> Sem r (SigArg 'Scoped)
-    checkArg arg@SigArg {..} = do
-      names' <- checkSigArgNames _sigArgNames
-      ty' <- mapM checkParseExpressionAtoms _sigArgType
-      default' <- case _sigArgDefault of
-        Nothing -> return Nothing
-        Just ArgDefault {..} ->
-          let err = throw (ErrWrongDefaultValue WrongDefaultValue {_wrongDefaultValue = arg})
-           in case _sigArgImplicit of
-                Explicit -> err
-                ImplicitInstance -> err
-                Implicit -> do
-                  val' <- checkParseExpressionAtoms _argDefaultValue
-                  return (Just ArgDefault {_argDefaultValue = val', ..})
-      return
-        SigArg
-          { _sigArgNames = names',
-            _sigArgType = ty',
-            _sigArgDefault = default',
-            ..
-          }
     checkBody :: Sem r (FunctionDefBody 'Scoped)
     checkBody = case _signBody of
       SigBodyExpression e -> SigBodyExpression <$> checkParseExpressionAtoms e
@@ -2196,6 +2257,7 @@ checkLetStatements =
               DefinitionFunctionDef d -> LetFunctionDef d
               DefinitionSyntax syn -> fromSyn syn
               DefinitionInductive {} -> impossible
+              DefinitionDeriving {} -> impossible
               DefinitionProjectionDef {} -> impossible
               DefinitionAxiom {} -> impossible
 

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

@@ -1368,14 +1368,13 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
   _signBody <- parseBody
   unless
     ( isJust (_funLhsColonKw ^. unIrrelevant)
-        || (maybe True P.isBodyExpression _signBody && null _funLhsArgs)
+        || (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/Core/Translation/Stripped/FromCore.hs

@@ -54,7 +54,7 @@ fromCore fsize tab =
       BuiltinIntLe -> False
       BuiltinIntLt -> False
       BuiltinSeq -> False
-      BuiltinIsEq -> False
+      BuiltinIsEqual -> False
       BuiltinMonadBind -> True -- TODO revise
       BuiltinFromNat -> True
       BuiltinFromInt -> True

src/Juvix/Compiler/Internal/Extra/Base.hs

@@ -424,12 +424,15 @@ foldApplication f args = case nonEmpty args of
 unfoldApplication' :: Application -> (Expression, NonEmpty ApplicationArg)
 unfoldApplication' (Application l' r' i') = second (|: (ApplicationArg i' r')) (unfoldExpressionApp l')
 
--- TODO make it tail recursive
 unfoldExpressionApp :: Expression -> (Expression, [ApplicationArg])
-unfoldExpressionApp = \case
-  ExpressionApplication (Application l r i) ->
-    second (`snoc` ApplicationArg i r) (unfoldExpressionApp l)
-  e -> (e, [])
+unfoldExpressionApp = swap . run . runAccumListReverse . go
+  where
+    go :: Expression -> Sem '[Accum ApplicationArg] Expression
+    go = \case
+      ExpressionApplication (Application l r i) -> do
+        accum (ApplicationArg i r)
+        go l
+      e -> return e
 
 unfoldApplication :: Application -> (Expression, NonEmpty Expression)
 unfoldApplication = fmap (fmap (^. appArg)) . unfoldApplication'

src/Juvix/Compiler/Internal/Language.hs

@@ -19,6 +19,7 @@ import Juvix.Data.Universe hiding (smallUniverse)
 import Juvix.Data.WithLoc
 import Juvix.Extra.Serialize
 import Juvix.Prelude
+import Juvix.Prelude.Pretty
 
 type Module = Module' MutualBlock
 
@@ -31,6 +32,18 @@ type PreModuleBody = ModuleBody' PreStatement
 newtype PreLetStatement
   = PreLetFunctionDef FunctionDef
 
+-- | Traits that support builtin deriving
+data DerivingTrait = DerivingEq
+  deriving stock (Generic, Data, Bounded, Enum, Show)
+
+instance IsBuiltin DerivingTrait where
+  toBuiltinPrim :: DerivingTrait -> BuiltinPrim
+  toBuiltinPrim = \case
+    DerivingEq -> toBuiltinPrim BuiltinEq
+
+instance Pretty DerivingTrait where
+  pretty = pretty . toBuiltinPrim
+
 data PreStatement
   = PreFunctionDef FunctionDef
   | PreInductiveDef InductiveDef
@@ -484,6 +497,7 @@ data NormalizedExpression = NormalizedExpression
   }
 
 makePrisms ''Expression
+makePrisms ''Iden
 makePrisms ''MutualStatement
 
 makeLenses ''SideIfBranch
@@ -584,7 +598,7 @@ instance HasAtomicity Pattern where
     PatternWildcardConstructor {} -> Atom
 
 instance HasLoc Module where
-  getLoc m = getLoc (m ^. moduleName) <>? maybe Nothing (Just . getLocSpan) (nonEmpty (m ^. moduleBody . moduleStatements))
+  getLoc m = getLoc (m ^. moduleName) <>? fmap getLocSpan (nonEmpty (m ^. moduleBody . moduleStatements))
 
 instance HasLoc MutualBlock where
   getLoc = getLocSpan . (^. mutualStatements)