store self recursive args in constructor info

anoma · Nov 27, 2024 · f5e92a7 · f5e92a7
1 parent 9fea5f8
commit f5e92a7
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 43 deletions.
diff --git 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
@@ -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
@@ -9,6 +9,7 @@ data ConstructorInfo = ConstructorInfo
     _constructorInfoType :: Expression,
     _constructorInfoInductive :: InductiveName,
     _constructorInfoName :: ConstructorName,
+    _constructorSelfRecursiveArgs :: [Bool],
     _constructorInfoBuiltin :: Maybe BuiltinConstructor,
     _constructorInfoTrait :: Bool,
     _constructorInfoRecord :: Bool