diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index e2c936e915..48d818d06b 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -263,5 +263,15 @@ mkConstructorEntries d = let _constructorInfoType = c ^. inductiveConstructorType, let _constructorInfoName = c ^. inductiveConstructorName, let _constructorInfoTrait = d ^. inductiveTrait, - let _constructorInfoRecord = c ^. inductiveConstructorIsRecord + let _constructorInfoRecord = c ^. inductiveConstructorIsRecord, + let _constructorSelfRecursiveArgs = selfRecursiveArgs (c ^. inductiveConstructorType) ] + where + selfRecursiveArgs :: Expression -> [Bool] + selfRecursiveArgs constrTy = constructorArgs constrTy ^.. each . paramType . to (== ty) + where + ty :: Expression + ty = + foldExplicitApplication + (toExpression (d ^. inductiveName)) + (d ^.. inductiveParameters . each . inductiveParamName . to toExpression) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index a224f20bee..e812525deb 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -28,7 +28,6 @@ import Juvix.Compiler.Internal.Data.NameDependencyInfo qualified as Internal import Juvix.Compiler.Internal.Extra (mkLetClauses) import Juvix.Compiler.Internal.Extra qualified as Internal import Juvix.Compiler.Internal.Extra.DependencyBuilder -import Juvix.Compiler.Internal.Pretty qualified as I import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context import Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker @@ -578,7 +577,7 @@ deriveOrd :: DerivingArgs -> Sem r Internal.FunctionDef deriveOrd der@DerivingArgs {..} = do - (constrs, subjectTy) <- derivingGetConstrs fullret args + constrs <- derivingGetConstrs ret args argsInfo <- goArgsInfo _derivingInstanceName let loc = getLoc ordName mkOrd <- getBuiltin loc BuiltinMkOrd @@ -592,14 +591,14 @@ deriveOrd der@DerivingArgs {..} = do _ordBuiltinGt = bgt, _ordBuiltinEq = beq } - (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs subjectTy constrs) + (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs constrs) let body = Internal.ExpressionLet Internal.Let { _letClauses = pure mutblock, _letExpression = mkOrd Internal.@@ recName } - ty = Internal.foldFunType _derivingParameters fullret + ty = Internal.foldFunType _derivingParameters ret pragmas' <- goPragmas _derivingPragmas return Internal.FunctionDef @@ -614,8 +613,8 @@ deriveOrd der@DerivingArgs {..} = do _funDefBuiltin = Nothing } where - fullret :: Internal.Expression - fullret = Internal.foldApplication (Internal.toExpression ordName) args + ret :: Internal.Expression + ret = Internal.foldApplication (Internal.toExpression ordName) args ordName :: Internal.InductiveName args :: [Internal.ApplicationArg] @@ -626,11 +625,10 @@ deriveOrd der@DerivingArgs {..} = do (Members '[NameIdGen] r') => Interval -> OrdBuiltins -> - Internal.Expression -> [ConstructorInfo] -> (Bool -> Internal.ApplicationArg -> Internal.ApplicationArg -> Internal.Expression) -> Sem r' Internal.Expression - genOrdCompare loc bs subjectTy cs recCmp = do + genOrdCompare loc bs cs recCmp = do res <- fmap nonEmpty . execOutputList @@ -659,24 +657,8 @@ deriveOrd der@DerivingArgs {..} = do let mkPat = Internal.genConstructorPattern loc Explicit c (p1, v1) <- mkPat (p2, v2) <- mkPat - let tmp = - c - ^.. Internal.constructorInfoType - . to Internal.constructorArgs - . each - . Internal.paramType - let selfRecArgs :: [Bool] - selfRecArgs = - trace - ("fullret " <> I.ppTrace fullret <> "\nargs = " <> I.ppTrace ((^. Internal.appArg) <$> args)) - tmp - ^.. each - . to (== subjectTy) - traceM ("cargs = " <> I.ppTrace tmp) - traceM ("selfrecargs = " <> prettyText selfRecArgs) - traceM ("subjectTy = " <> I.ppTrace subjectTy) - traceM "\n\n" + selfRecArgs = c ^. constructorSelfRecursiveArgs lord <- lexOrder (zip3Exact selfRecArgs v1 v2) let sameConstr = Internal.LambdaClause @@ -729,12 +711,11 @@ derivingGetConstrs :: (Members '[Error ScoperError, State LocalTable, Reader S.InfoTable, Reader Internal.InfoTable] r) => Internal.Expression -> [Internal.ApplicationArg] -> - Sem r ([Internal.ConstructorInfo], Internal.Expression) + Sem r [Internal.ConstructorInfo] derivingGetConstrs retTy args = runFailDefaultM (throwDerivingWrongForm retTy) $ do [Internal.ApplicationArg Explicit a] <- return args Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a)) - cs <- getDefinedInductiveConstructors ind - return (cs, a) + getDefinedInductiveConstructors ind deriveRecursiveBinaryFunction :: (Members '[NameIdGen] r) => @@ -800,7 +781,7 @@ deriveEq der@DerivingArgs {..} = do { _letClauses = pure mutblock, _letExpression = mkEq Internal.@@ recDefName } - ty = Internal.foldFunType _derivingParameters fullret + ty = Internal.foldFunType _derivingParameters ret pragmas' <- goPragmas _derivingPragmas return Internal.FunctionDef @@ -815,8 +796,8 @@ deriveEq der@DerivingArgs {..} = do _funDefBuiltin = Nothing } where - fullret :: Internal.Expression - fullret = Internal.foldApplication (Internal.toExpression eqName) args + ret :: Internal.Expression + ret = Internal.foldApplication (Internal.toExpression eqName) args eqName :: Internal.InductiveName args :: [Internal.ApplicationArg] @@ -846,11 +827,11 @@ deriveEq der@DerivingArgs {..} = do ) -> Sem r Internal.Expression eqLambda bs recCall = do - (constrs, subjectTy) <- derivingGetConstrs fullret args + constrs <- derivingGetConstrs ret args case nonEmpty constrs of Nothing -> return (Internal.toExpression (bs ^. eqBuiltinTrue)) Just cs -> do - cl' <- mapM (lambdaClause subjectTy) cs + cl' <- mapM lambdaClause cs defaultCl' <- if | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause @@ -874,10 +855,9 @@ deriveEq der@DerivingArgs {..} = do } lambdaClause :: - Internal.Expression -> Internal.ConstructorInfo -> Sem r Internal.LambdaClause - lambdaClause subjectTy cinfo = do + lambdaClause cinfo = do let loc = getLoc _derivingInstanceName mkpat = Internal.genConstructorPattern loc Explicit cinfo (p1, v1) <- mkpat @@ -899,13 +879,7 @@ deriveEq der@DerivingArgs {..} = do kargs = map (over both Internal.explicitApplicationArg) k selfRecArgs :: [Bool] - selfRecArgs = - cinfo - ^.. Internal.constructorInfoType - . to Internal.constructorArgs - . each - . Internal.paramType - . to (== subjectTy) + selfRecArgs = cinfo ^. Internal.constructorSelfRecursiveArgs mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression mkAnds = foldl1 mkAnd . fmap Internal.toExpression diff --git a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs index 71c71145a9..47ed0b90c7 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs @@ -9,6 +9,7 @@ data ConstructorInfo = ConstructorInfo _constructorInfoType :: Expression, _constructorInfoInductive :: InductiveName, _constructorInfoName :: ConstructorName, + _constructorSelfRecursiveArgs :: [Bool], _constructorInfoBuiltin :: Maybe BuiltinConstructor, _constructorInfoTrait :: Bool, _constructorInfoRecord :: Bool