[ derive ] Support searching for very external generators

src/Deriving/DepTyCheck/Gen/Checked.idr

@@ -114,6 +114,12 @@ namespace ClojuringCanonicImpl
       let Nothing = lookupLengthChecked sig !ask
         | Just (name, Element extSig lenEq) => pure $ callExternalGen extSig name (var outmostFuelArg) $ rewrite lenEq in values
 
+      -- look for very external gens, i.e. those that can be reached with `%search`
+      canonicSigType <- try .| check (canonicSig sig)
+                            .| fail "INTERNAL ERROR: canonic signature of \{show sig.targetType.name} is not a type"
+      Nothing <- search canonicSigType
+        | Just found => flip (foldl app) values <$> flip app fuel <$> quote found
+
       -- get the name of internal gen, derive if necessary
       internalGenName <- do
 

src/Test/DepTyCheck/Gen.idr

@@ -32,6 +32,7 @@ import Test.DepTyCheck.Gen.NonEmpty
 
 export
 data Gen : Type -> Type where
+  [noHints]
   Empty    : Gen a
   NonEmpty : Lazy (Gen1 $ Maybe a) -> Gen a
 

src/Test/DepTyCheck/Gen/NonEmpty.idr

@@ -38,19 +38,22 @@ transport z Refl = z
 --------------------------------
 
 record RawGen a where
+  [noHints]
   constructor MkRawGen
   unRawGen : forall m. MonadRandom m => m a
 
 record OneOfAlternatives (0 a : Type)
 
 export
 data Gen1 : Type -> Type where
+  [noHints]
   Pure  : a -> Gen1 a
   Raw   : RawGen a -> Gen1 a
   OneOf : OneOfAlternatives a -> Gen1 a
   Bind  : RawGen c -> (c -> Gen1 a) -> Gen1 a
 
 record OneOfAlternatives (0 a : Type) where
+  [noHints]
   constructor MkOneOf
   desc : Maybe String
   gens : LazyLst1 (PosNat, Lazy (Gen1 a))

tests/gen-derivation/derivation/_common/RunDerivedGen.idr

@@ -8,11 +8,11 @@ import System.Random.Pure.StdGen
 
 %default total
 
-export %hint
+export
 smallStrs : Fuel -> Gen String
 smallStrs _ = elements ["", "a", "bc"]
 
-export %hint
+export
 smallNats : Fuel -> Gen Nat
 smallNats _ = elements [0, 10]
 
@@ -21,10 +21,28 @@ aVect : Fuel -> (Fuel -> Gen a) => (n : Nat) -> Gen (Vect n a)
 aVect f Z             = [| [] |]
 aVect f (S n) @{genA} = [| genA f :: aVect f n @{genA} |]
 
-export %hint
+export
 someTypes : Fuel -> Gen Type
 someTypes _ = elements [Nat, String, Bool]
 
+namespace SomeTestType
+
+  public export -- it would be good if this worked for non-public too
+  data SomeTestType : (n : Nat) -> Type where
+    MkSomeTestType : String -> Vect n Nat -> SomeTestType n
+
+  export
+  Show (SomeTestType n) where
+    show (MkSomeTestType desc xs) = "MkSomeTestType \{show desc} \{show xs}"
+
+  export
+  TunableSomeTestTypeGen : String -> Fuel -> (n : Nat) -> Gen $ SomeTestType n
+  TunableSomeTestTypeGen desc f n = MkSomeTestType desc <$> aVect f @{smallNats} n
+
+  export %hint
+  HintedSomeTestTypeGen : Fuel -> (n : Nat) -> Gen $ SomeTestType n
+  HintedSomeTestTypeGen = TunableSomeTestTypeGen "very-external"
+
 export
 Show (a = b) where
   show Refl = "Refl"

tests/gen-derivation/derivation/core/norec nodep w_hnt 001/DerivedGen.idr

@@ -0,0 +1,23 @@
+module DerivedGen
+
+import RunDerivedGen
+
+%default total
+
+%language ElabReflection
+
+data X = MkX String String
+
+%runElab derive "X" [Generic, Meta, Show]
+
+%hint
+hintedStringGen : Fuel -> Gen String
+hintedStringGen _ = elements ["very-external", "hinted"]
+
+-- shall not use hinted strings gen, shall use the given one
+export
+checkedGen : Fuel -> (Fuel -> Gen String) => Gen X
+checkedGen = deriveGen
+
+main : IO ()
+main = runGs [ G $ \fl => checkedGen fl @{smallStrs} ]

tests/gen-derivation/derivation/core/norec nodep w_hnt 001/RunDerivedGen.idr

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 001/depends

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 001/derive.ipkg

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 001/expected

@@ -0,0 +1,24 @@
+1/2: Building RunDerivedGen (RunDerivedGen.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+Generated values:
+-----
+-----
+MkX "a" ""
+-----
+MkX "" ""
+-----
+MkX "" "a"
+-----
+MkX "a" "a"
+-----
+MkX "" "a"
+-----
+MkX "a" "bc"
+-----
+MkX "" ""
+-----
+MkX "bc" "a"
+-----
+MkX "a" "a"
+-----
+MkX "a" ""

tests/gen-derivation/derivation/core/norec nodep w_hnt 001/run

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 002/DerivedGen.idr

@@ -0,0 +1,23 @@
+module DerivedGen
+
+import RunDerivedGen
+
+%default total
+
+%language ElabReflection
+
+data X = MkX String String
+
+%runElab derive "X" [Generic, Meta, Show]
+
+%hint
+hintedStringGen : Fuel -> Gen String
+hintedStringGen _ = elements ["very-external", "hinted"]
+
+-- shall use the hinted strings gen
+export
+checkedGen : Fuel -> Gen X
+checkedGen = deriveGen
+
+main : IO ()
+main = runGs [ G $ \fl => checkedGen fl ]

tests/gen-derivation/derivation/core/norec nodep w_hnt 002/RunDerivedGen.idr

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 002/depends

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 002/derive.ipkg

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 002/dont-run

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 002/expected

@@ -0,0 +1,9 @@
+1/2: Building RunDerivedGen (RunDerivedGen.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+Error: While processing right hand side of checkedGen. Error during reflection: While processing right hand side of $resolved16321,<DerivedGen.X>[]. While processing right hand side of $resolved16321,<DerivedGen.X>[],<<DerivedGen.MkX>>. Name Test.DepTyCheck.Gen.Uniform is private.
+
+Suggestion: add an explicit export or public export modifier. By default, all names are private in namespace blocks.
+Error: While processing right hand side of checkedGen. Error during reflection: While processing right hand side of $resolved16321,<DerivedGen.X>[]. While processing right hand side of $resolved16321,<DerivedGen.X>[],<<DerivedGen.MkX>>. Name Test.DepTyCheck.Gen.Uniform is private.
+
+Suggestion: add an explicit export or public export modifier. By default, all names are private in namespace blocks.
+Warning: compiling hole DerivedGen.checkedGen

tests/gen-derivation/derivation/core/norec nodep w_hnt 003/DerivedGen.idr

@@ -0,0 +1,19 @@
+module DerivedGen
+
+import RunDerivedGen
+
+%default total
+
+%language ElabReflection
+
+data X = MkX (SomeTestType 2) (SomeTestType 3)
+
+%runElab derive "X" [Generic, Meta, Show]
+
+-- shall not use hinted strings gen, shall use the given one
+export
+checkedGen : Fuel -> (Fuel -> (n : Nat) -> Gen $ SomeTestType n) => Gen X
+checkedGen = deriveGen
+
+main : IO ()
+main = runGs [ G $ \fl => checkedGen fl @{TunableSomeTestTypeGen "given"} ]

tests/gen-derivation/derivation/core/norec nodep w_hnt 003/RunDerivedGen.idr

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 003/depends

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 003/derive.ipkg

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 003/expected

@@ -0,0 +1,24 @@
+1/2: Building RunDerivedGen (RunDerivedGen.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+Generated values:
+-----
+-----
+MkX MkSomeTestType "given" [10, 0] MkSomeTestType "given" [0, 0, 0]
+-----
+MkX MkSomeTestType "given" [10, 10] MkSomeTestType "given" [10, 10, 10]
+-----
+MkX MkSomeTestType "given" [0, 10] MkSomeTestType "given" [10, 0, 0]
+-----
+MkX MkSomeTestType "given" [10, 0] MkSomeTestType "given" [0, 10, 10]
+-----
+MkX MkSomeTestType "given" [10, 10] MkSomeTestType "given" [10, 0, 0]
+-----
+MkX MkSomeTestType "given" [0, 10] MkSomeTestType "given" [10, 10, 0]
+-----
+MkX MkSomeTestType "given" [0, 0] MkSomeTestType "given" [10, 0, 10]
+-----
+MkX MkSomeTestType "given" [10, 10] MkSomeTestType "given" [10, 0, 10]
+-----
+MkX MkSomeTestType "given" [0, 10] MkSomeTestType "given" [10, 10, 10]
+-----
+MkX MkSomeTestType "given" [10, 0] MkSomeTestType "given" [10, 0, 0]

tests/gen-derivation/derivation/core/norec nodep w_hnt 003/run

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 004/DerivedGen.idr

@@ -0,0 +1,19 @@
+module DerivedGen
+
+import RunDerivedGen
+
+%default total
+
+%language ElabReflection
+
+data X = MkX (SomeTestType 2) (SomeTestType 3)
+
+%runElab derive "X" [Generic, Meta, Show]
+
+-- shall not use hinted strings gen, shall use the given one
+export
+checkedGen : Fuel -> Gen X
+checkedGen = deriveGen
+
+main : IO ()
+main = runGs [ G $ \fl => checkedGen fl ]

tests/gen-derivation/derivation/core/norec nodep w_hnt 004/RunDerivedGen.idr

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 004/depends

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 004/derive.ipkg

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

tests/gen-derivation/derivation/core/norec nodep w_hnt 004/expected

@@ -0,0 +1,24 @@
+1/2: Building RunDerivedGen (RunDerivedGen.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+Generated values:
+-----
+-----
+MkX MkSomeTestType "very-external" [10, 0] MkSomeTestType "very-external" [0, 0, 0]
+-----
+MkX MkSomeTestType "very-external" [10, 10] MkSomeTestType "very-external" [10, 10, 10]
+-----
+MkX MkSomeTestType "very-external" [0, 10] MkSomeTestType "very-external" [10, 0, 0]
+-----
+MkX MkSomeTestType "very-external" [10, 0] MkSomeTestType "very-external" [0, 10, 10]
+-----
+MkX MkSomeTestType "very-external" [10, 10] MkSomeTestType "very-external" [10, 0, 0]
+-----
+MkX MkSomeTestType "very-external" [0, 10] MkSomeTestType "very-external" [10, 10, 0]
+-----
+MkX MkSomeTestType "very-external" [0, 0] MkSomeTestType "very-external" [10, 0, 10]
+-----
+MkX MkSomeTestType "very-external" [10, 10] MkSomeTestType "very-external" [10, 0, 10]
+-----
+MkX MkSomeTestType "very-external" [0, 10] MkSomeTestType "very-external" [10, 10, 10]
+-----
+MkX MkSomeTestType "very-external" [10, 0] MkSomeTestType "very-external" [10, 0, 0]

tests/gen-derivation/derivation/core/norec nodep w_hnt 004/run

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