[ derive ] Fix distribution for tricky dependency+recursion case

examples/sorted-list/tests/gens/len-distr/CheckDistribution.idr

@@ -0,0 +1,19 @@
+module CheckDistribution
+
+import Data.List.Sorted.Gen
+
+import Deriving.DepTyCheck.Gen
+
+import DistrCheckCommon
+
+%default total
+
+mainFor : (depth : Nat) -> IO ()
+mainFor depth = printVerdict (genSortedList $ limit depth) $ fromList
+                  $ [ coverWith (ratio 1 $ S depth) ((== n) . length) | n <- [0 .. depth] ]
+
+main : IO ()
+main = do
+  mainFor 2
+  mainFor 5
+  mainFor 10

examples/sorted-list/tests/gens/len-distr/DistrCheckCommon.idr

@@ -0,0 +1 @@
+../../../../../tests/lib/distribution/_common/DistrCheckCommon.idr

examples/sorted-list/tests/gens/len-distr/expected

@@ -0,0 +1,3 @@
+Just [ok, ok, ok]
+Just [ok, ok, ok, ok, ok, ok]
+Just [ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok]

examples/sorted-list/tests/gens/len-distr/run

@@ -0,0 +1 @@
+../../../../../tests/lib/distribution/_common/run

examples/sorted-list/tests/gens/len-distr/test.ipkg

@@ -0,0 +1,7 @@
+package test
+
+main = CheckDistribution
+
+depends = deptycheck
+        , summary-stat
+        , sorted-list

src/Deriving/DepTyCheck/Gen/Core.idr

@@ -18,18 +18,25 @@ import public Language.Reflection.Types
 data Recursiveness =
   ||| When constructor refers transitively to the type it belongs
   DirectlyRecursive |
+  ||| When constructor itself does not refer to the type it belongs,
+  ||| but its generated index either
+  ||| - refers to some constructor that is recursive, or
+  ||| - is general enough to be able to refer so some recursive constructor
+  IndexedByRecursive |
   ||| When constructor does not refer to the type it belongs,
   ||| nor to any recursive constructor in its generated indices
   NonRecursive
 
 ||| Checks if the status is anyhow recursive, directly or through index
 isRec : Recursiveness -> Bool
 isRec DirectlyRecursive  = True
+isRec IndexedByRecursive = True
 isRec NonRecursive       = False
 
 ||| Check if we are able to call for this constructor on a dry fuel
 isDirectlyRec : Recursiveness -> Bool
 isDirectlyRec DirectlyRecursive  = True
+isDirectlyRec IndexedByRecursive = False
 isDirectlyRec NonRecursive       = False
 
 ||| Property is implication from the strong property to the weak one
@@ -40,6 +47,17 @@ recStrengthProp {r=DirectlyRecursive} Oh = Oh
 --- Derivation functions ---
 ----------------------------
 
+[Short] Show TTImp where
+  show expr = do
+    let (l, rs) = unAppAny expr
+    "\{l}\{concatMap (const " (...)") rs}"
+
+printMatrix : Foldable f => Foldable t => Elaboration m => (desc : String) -> f (t TTImp) -> m ()
+printMatrix desc xxs = do
+  logMsg "debug" 0 desc
+  for_ xxs $ \xs => do
+    logMsg "debug" 0 "- \{joinBy ", " $ map (show @{Short}) $ toList xs}"
+
 export
 ConstructorDerivator => DerivatorCore where
   canonicBody sig n = do
@@ -57,11 +75,32 @@ ConstructorDerivator => DerivatorCore where
     consBodies <- for sig.targetType.cons $ \con => logBounds "consBody" [sig, con] $
       canonicConsBody sig (consGenName con) con <&> def (consGenName con)
 
+    -- prepare information about generated type arguments by constructors
+    genConParams <- either (uncurry failAt) pure $ for sig.targetType.cons.asVect $ \con => do
+      let conParams = snd $ unAppAny con.type
+      let Yes lengthCorrect = decEq conParams.length sig.targetType.args.length
+        | No _ => Left (getFC con.type, "INTERNAL ERROR: wrong count of unapp of constructor \{show con.name}")
+      let genConParams = sig.generatedParams.asVect <&> \gv => getExpr $ index' conParams $ rewrite lengthCorrect in gv
+      Right genConParams
+    -- clean up prefixes of potential indices, we kinda depend here on fact that constructor expressions are already normalised
+    printMatrix "before" genConParams
+    let genConParams = transpose . map (cutAppPrefix {n=sig.targetType.cons.length}) . transpose $ genConParams
+    printMatrix "after" genConParams
+
     -- calculate which constructors are recursive and which are not
-    consRecs <- logBounds "consRec" [sig] $ pure $ sig.targetType.cons <&> \con => do
+    consRecs <- logBounds "consRec" [sig] $ for (sig.targetType.cons `zipV` genConParams) $ \(con, genConIdxs) => do
       let False = isRecursive {containingType=Just sig.targetType} con
-        | True => (con, DirectlyRecursive)
-      (con, NonRecursive)
+        | True => pure (con, DirectlyRecursive)
+      -- this constructor is not directly recursive, check if any of generated indices are indexed by a recursive constructor
+      let conArgNames = fromList $ name <$> con.args
+      let namesInGivenConParams = concatMap allVarNames' genConIdxs
+      logMsg "debug" 0 "\{show con.name}: names in givens: \{show namesInGivenConParams.asList}"
+      let externalNamesInGivenConParams = SortedSet.toList $ namesInGivenConParams `difference` conArgNames
+      logMsg "debug" 0 "\{show con.name}: extrnal names in givens: \{show externalNamesInGivenConParams}"
+      -- now we want to check if external names can refer to non-constructors and/or recursive constructors;
+      -- if yes, then this constructor is potentially indexed by recursive something
+      let rec = if any ((/= Just False) . isRecursiveConstructor) externalNamesInGivenConParams then IndexedByRecursive else NonRecursive
+      pure (con, rec)
 
     -- decide how to name a fuel argument on the LHS
     let fuelArg = "^fuel_arg^" -- I'm using a name containing chars that cannot be present in the code parsed from the Idris frontend

src/Deriving/DepTyCheck/Util/Reflection.idr

@@ -15,6 +15,9 @@ import public Data.SortedMap
 import public Data.SortedMap.Dependent
 import public Data.SortedSet
 
+import public Decidable.Equality
+import public Decidable.Equality.Core
+
 import public Deriving.DepTyCheck.Util.Alternative
 import public Deriving.DepTyCheck.Util.Collections
 import public Deriving.DepTyCheck.Util.Fin
@@ -581,6 +584,35 @@ namespace UpToRenaming
   [UpToRenaming] Eq TTImp where
     x == y = (x == y) @{UpToSubst @{empty}}
 
+[AppUpToRenaming] Eq AnyApp where
+  (==) = (==) @{UpToRenaming} `on` getExpr
+
+export
+cutAppPrefix : {n : _} -> Vect n TTImp -> Vect n TTImp
+cutAppPrefix' : {n : _} -> Vect n AnyApp -> Vect n AnyApp
+cutAppPrefix [] = []
+cutAppPrefix {n=S k} xs@(_::_) = do
+  let unappXs = xs <&> unAppAny
+  let heads = fst <$> unappXs
+  let S Z = List.length . nub @{UpToRenaming} $ heads.asList
+    | _ => xs -- what is applied differs, to stop reduction
+  let first::unappXs = snd <$> unappXs
+  let unappXs : Maybe $ Vect k $ Vect first.length AnyApp = for unappXs $ \lst => do
+    let Yes lc = decEq first.length lst.length
+      | No _ => Nothing
+    rewrite lc
+    Just lst.asVect
+  let Just unappXs = unappXs
+    | Nothing => xs -- different count of args in apps, stop reduction
+  let unappXs = transpose $ first.asVect :: unappXs
+  let [unevenApp] = filter ((> 1) . List.length . nub @{AppUpToRenaming} . toList) unappXs.asList
+    | [] => xs <&> \expr => Implicit (getFC expr) False -- all equal, erase it
+    | _  => map (uncurry reAppAny) $ zip heads $ transpose $ assert_total cutAppPrefix' <$> unappXs
+  cutAppPrefix $ assert_smaller xs $ map getExpr $ unevenApp
+cutAppPrefix' xs = do
+  let xs' = cutAppPrefix $ getExpr <$> xs
+  xs' `zip` xs <&> uncurry (mapExpr . const)
+
 -- Returns a list without duplications
 export
 allInvolvedTypes : Elaboration m => (minimalRig : Count) -> TypeInfo -> m $ List TypeInfo

tests/derivation/distribution/dependent-rec-003/CheckDistribution.idr

@@ -0,0 +1,42 @@
+module CheckDistribution
+
+import Deriving.DepTyCheck.Gen
+
+import DistrCheckCommon
+
+%default total
+
+%hint DA : ConstructorDerivator; DA = LeastEffort
+
+data ListNat : Type
+data Constraint : Nat -> ListNat -> Type
+
+data ListNat : Type where
+  Nil  : ListNat
+  (::) : (x : Nat) -> (xs : ListNat) -> Constraint x xs => ListNat
+
+data Constraint : Nat -> ListNat -> Type where
+  Empty    : Constraint e []
+  NonEmpty : Constraint e $ (x::xs) @{prf}
+  Any1     : Constraint e xs
+  Any2     : Constraint e xs
+  Any3     : Constraint e xs
+
+length : ListNat -> Nat
+length []      = Z
+length (_::xs) = S $ length xs
+
+listNats : Fuel -> Gen MaybeEmpty ListNat
+listNats = deriveGen
+
+-- Check that length of generated lists is uniformly distributed
+
+mainFor : (depth : Nat) -> IO ()
+mainFor depth = printVerdict (listNats $ limit depth) $ fromList
+                  $ [ coverWith (ratio 1 $ S depth) ((== n) . length) | n <- [0 .. depth] ]
+
+main : IO ()
+main = do
+  mainFor 2
+  mainFor 5
+  mainFor 10

tests/derivation/distribution/dependent-rec-003/DistrCheckCommon.idr

@@ -0,0 +1 @@
+../_common/DistrCheckCommon.idr

tests/derivation/distribution/dependent-rec-003/expected

@@ -0,0 +1,3 @@
+Just [ok, ok, ok]
+Just [ok, ok, ok, ok, ok, ok]
+Just [ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok]

tests/derivation/distribution/dependent-rec-003/run

@@ -0,0 +1 @@
+../_common/run

tests/derivation/distribution/dependent-rec-003/test.ipkg

@@ -0,0 +1 @@
+../_common/test.ipkg

tests/derivation/distribution/dependent-rec-sh-003/CheckDistribution.idr

@@ -0,0 +1,42 @@
+module CheckDistribution
+
+import Deriving.DepTyCheck.Gen
+
+import DistrCheckCommon
+
+%default total
+
+%hint DA : ConstructorDerivator; DA = LeastEffort {simplificationHack=True}
+
+data ListNat : Type
+data Constraint : Nat -> ListNat -> Type
+
+data ListNat : Type where
+  Nil  : ListNat
+  (::) : (x : Nat) -> (xs : ListNat) -> Constraint x xs => ListNat
+
+data Constraint : Nat -> ListNat -> Type where
+  Empty    : Constraint e []
+  NonEmpty : Constraint e $ (x::xs) @{prf}
+  Any1     : Constraint e xs
+  Any2     : Constraint e xs
+  Any3     : Constraint e xs
+
+length : ListNat -> Nat
+length []      = Z
+length (_::xs) = S $ length xs
+
+listNats : Fuel -> Gen MaybeEmpty ListNat
+listNats = deriveGen
+
+-- Check that length of generated lists is uniformly distributed
+
+mainFor : (depth : Nat) -> IO ()
+mainFor depth = printVerdict (listNats $ limit depth) $ fromList
+                  $ [ coverWith (ratio 1 $ S depth) ((== n) . length) | n <- [0 .. depth] ]
+
+main : IO ()
+main = do
+  mainFor 2
+  mainFor 5
+  mainFor 10

tests/derivation/distribution/dependent-rec-sh-003/DistrCheckCommon.idr

@@ -0,0 +1 @@
+../_common/DistrCheckCommon.idr

tests/derivation/distribution/dependent-rec-sh-003/expected

@@ -0,0 +1,3 @@
+Just [ok, ok, ok]
+Just [ok, ok, ok, ok, ok, ok]
+Just [ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok]

tests/derivation/distribution/dependent-rec-sh-003/run

@@ -0,0 +1 @@
+../_common/run

tests/derivation/distribution/dependent-rec-sh-003/test.ipkg

@@ -0,0 +1 @@
+../_common/test.ipkg