[ derive ] Search for hinted externals before deriving

src/Deriving/DepTyCheck/Gen/Checked.idr

@@ -110,31 +110,35 @@ namespace ClojuringCanonicImpl
   DerivatorCore => ClojuringContext m => Elaboration m => CanonicGen m where
     callGen sig fuel values = do
 
+      --- check if no derivation is needed ---
+
       -- look for external gens, and call it if exists
       let Nothing = lookupLengthChecked sig !ask
         | Just (name, Element extSig lenEq) => pure $ callExternalGen extSig name (var outmostFuelArg) $ rewrite lenEq in values
 
-      -- get the name of internal gen, derive if necessary
-      internalGenName <- do
+      -- look for existing already derived (internal) gen, use it if exists
+      let Nothing = lookup sig !get
+        | Just internalGenName => pure $ callCanonic sig internalGenName fuel values
 
-        -- look for existing (already derived) internals, use it if exists
-        let Nothing = lookup sig !get
-          | Just name => pure name
+      -- 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
 
-        -- nothing found, then derive! acquire the name
-        let name = nameForGen sig
+      --- nothing's found, then derive! ---
 
-        -- remember that we're responsible for this signature derivation
-        modify $ insert sig name
+      -- acquire the name
+      let internalGenName = nameForGen sig
 
-        -- derive declaration and body for the asked signature. It's important to call it AFTER update of the map in the state to not to cycle
-        (genFunClaim, genFunBody) <- logBounds "type" [sig] $ assert_total $ deriveCanonical sig name
+      -- remember that we're responsible for this signature derivation
+      modify $ insert sig internalGenName
 
-        -- remember the derived stuff
-        tell ([genFunClaim], [genFunBody])
+      -- derive declaration and body for the asked signature. It's important to call it AFTER update of the map in the state to not to cycle
+      (genFunClaim, genFunBody) <- logBounds "type" [sig] $ assert_total $ deriveCanonical sig internalGenName
 
-        -- return the name of the newly derived generator
-        pure name
+      -- remember the derived stuff
+      tell ([genFunClaim], [genFunBody])
 
       -- call the internal gen
       pure $ callCanonic sig internalGenName fuel values

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/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/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,7 @@
+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 $resolved17513,<DerivedGen.X>[]. While processing right hand side of $resolved17513,<DerivedGen.X>[],<<DerivedGen.MkX>>. Undefined name Test.DepTyCheck.Gen.NonEmpty.GenAlternatives.GenAlternatives. 
+Did you mean any of: GenAlternatives', Alternative, IAlternative, MkAlternative, deepAlternativesOf, or mapAlternativesOf?
+[ fatal ] Error when executing system command.
+          Command: "build/exec/_tmppack"
+          Error code: 127

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/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/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

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

@@ -0,0 +1,24 @@
+module DerivedGen
+
+import RunDerivedGen
+
+%default total
+
+%language ElabReflection
+
+data X = MkX Nat Nat
+
+%runElab derive "X" [Generic, Meta, Show]
+
+-- self-recursive type, should find the current generator instead of declared hint
+%hint
+hintedStringGen : Fuel -> Gen Nat
+hintedStringGen _ = elements [2, 4, 8, 16]
+
+-- shall use the hinted nats 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 005/RunDerivedGen.idr

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

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

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

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

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

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

@@ -0,0 +1,7 @@
+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 $resolved17513,<DerivedGen.X>[]. While processing right hand side of $resolved17513,<DerivedGen.X>[],<<DerivedGen.MkX>>. Undefined name Test.DepTyCheck.Gen.NonEmpty.GenAlternatives.GenAlternatives. 
+Did you mean any of: GenAlternatives', Alternative, IAlternative, MkAlternative, deepAlternativesOf, or mapAlternativesOf?
+[ fatal ] Error when executing system command.
+          Command: "build/exec/_tmppack"
+          Error code: 127