[ derive ] Do not pass values of arguments on which someone else depends

buzden · Sep 17, 2024 · bf5663d · bf5663d
1 parent 422d10e
commit bf5663d
Show file tree

Hide file tree

Showing 14 changed files with 146 additions and 8 deletions.
diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-impl-big/expected b/tests/derivation/least-effort/print/regression/dependent-givens-impl-big/expected
@@ -102,7 +102,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (v : VectMaybeAnyType n) ->
                                           .$ (   var "Builtin.DPair.MkDPair"
                                               .$ implicitTrue
                                               .$ (   var "DerivedGen.VectMaybeAnyType.Here"
-                                                  .! ("{n:4022}", var "^bnd^{n:4022}")
+                                                  .! ("{n:4022}", implicitTrue)
                                                   .! ("xs", var "xs")
                                                   .! ("x", var "x")))))
                              , var "<<DerivedGen.VectMaybeAnyType.Here>>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty"
@@ -134,10 +134,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (v : VectMaybeAnyType n) ->
                                                                  .$ implicitTrue
                                                                  .$ (   var "DerivedGen.VectMaybeAnyType.There"
                                                                      .! ("z", var "z")
-                                                                     .! ("x", var "x")
-                                                                     .! ("n", var "n")
-                                                                     .! ("i", var "i")
-                                                                     .! ("zs", var "zs")
+                                                                     .! ("x", implicitTrue)
+                                                                     .! ("n", implicitTrue)
+                                                                     .! ("i", implicitTrue)
+                                                                     .! ("zs", implicitTrue)
                                                                      .$ var "^bnd^{arg:4}")))
                                                     ]
                                                 }))

diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-deep/expected b/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-deep/expected
@@ -54,7 +54,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (f : Fin n) ->
                                   .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)"))
                                   .$ (   var "Prelude.pure"
                                       .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
-                                      .$ (var "DerivedGen.MkX" .$ var "n" .$ var "f"))
+                                      .$ (var "DerivedGen.MkX" .$ implicitTrue .$ var "f"))
                              , var "<<DerivedGen.MkX>>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty"
                              ]
                          ]

diff --git a/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-shallow/expected b/tests/derivation/least-effort/print/regression/dependent-givens-impl-small-shallow/expected
@@ -52,7 +52,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (n : Nat) -> (f : Fin n) ->
                                   .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)"))
                                   .$ (   var "Prelude.pure"
                                       .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
-                                      .$ (var "DerivedGen.MkX" .$ var "n" .$ var "f"))
+                                      .$ (var "DerivedGen.MkX" .$ implicitTrue .$ var "f"))
                              , var "<<DerivedGen.MkX>>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty"
                              ]
                          ]

diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-impl-full/DerivedGen.idr b/tests/derivation/least-effort/print/regression/underscore-in-cons-impl-full/DerivedGen.idr
@@ -0,0 +1,16 @@
+module DerivedGen
+
+import Data.Fin
+
+import Deriving.DepTyCheck.Gen
+
+%default total
+
+data IsFS : Fin n -> Type where
+  ItIsFS : IsFS (FS i)
+
+%language ElabReflection
+
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $
+  Fuel -> {n : Nat} -> (v : Fin n) -> Gen MaybeEmpty $ IsFS v
diff --git a/...s/derivation/least-effort/print/regression/underscore-in-cons-impl-full/RunDerivedGen.idr b/...s/derivation/least-effort/print/regression/underscore-in-cons-impl-full/RunDerivedGen.idr
@@ -0,0 +1 @@
+../_common/RunDerivedGen.idr
diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-impl-full/derive.ipkg b/tests/derivation/least-effort/print/regression/underscore-in-cons-impl-full/derive.ipkg
@@ -0,0 +1 @@
+../_common/derive.ipkg
diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-impl-full/expected b/tests/derivation/least-effort/print/regression/underscore-in-cons-impl-full/expected
@@ -0,0 +1,68 @@
+1/1: Building DerivedGen (DerivedGen.idr)
+LOG deptycheck.derive.print:5: type: (arg : Fuel) -> (v : Fin n) -> Gen MaybeEmpty (IsFS v)
+    MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
+.=> MkArg MW ImplicitArg (Just "outer^<n>") implicitTrue
+.=> MkArg MW ExplicitArg (Just "outer^<v>") implicitTrue
+.=> local
+      { decls =
+          [ IClaim
+              emptyFC
+              MW
+              Export
+              []
+              (mkTy
+                 { name = "<DerivedGen.IsFS>[0, 1]"
+                 , type =
+                         MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
+                     .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat")
+                     .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n")
+                     .->    var "Test.DepTyCheck.Gen.Gen"
+                         .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
+                         .$ (var "DerivedGen.IsFS" .! ("n", var "n") .$ var "{arg:1}")
+                 })
+          , IDef
+              emptyFC
+              "<DerivedGen.IsFS>[0, 1]"
+              [    var "<DerivedGen.IsFS>[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^<n>" .$ bindVar "inter^<{arg:1}>"
+                .= local
+                     { decls =
+                         [ IClaim
+                             emptyFC
+                             MW
+                             Export
+                             []
+                             (mkTy
+                                { name = "<<DerivedGen.ItIsFS>>"
+                                , type =
+                                        MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
+                                    .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat")
+                                    .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fin.Fin" .$ var "n")
+                                    .->    var "Test.DepTyCheck.Gen.Gen"
+                                        .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
+                                        .$ (var "DerivedGen.IsFS" .! ("n", var "n") .$ var "{arg:1}")
+                                })
+                         , IDef
+                             emptyFC
+                             "<<DerivedGen.ItIsFS>>"
+                             [       var "<<DerivedGen.ItIsFS>>"
+                                  .$ bindVar "^cons_fuel^"
+                                  .$ (var "Prelude.Types.S" .$ bindVar "^bnd^{k:3639}")
+                                  .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ bindVar "i")
+                               .=    var "Test.DepTyCheck.Gen.label"
+                                  .$ (var "fromString" .$ primVal (Str "DerivedGen.ItIsFS (orders)"))
+                                  .$ (   var "Prelude.pure"
+                                      .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
+                                      .$ (var "DerivedGen.ItIsFS" .! ("{k:3639}", implicitTrue) .! ("i", var "i")))
+                             , var "<<DerivedGen.ItIsFS>>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty"
+                             ]
+                         ]
+                     , scope =
+                            var "Test.DepTyCheck.Gen.label"
+                         .$ (var "fromString" .$ primVal (Str "DerivedGen.IsFS[0, 1] (non-recursive)"))
+                         .$ (var "<<DerivedGen.ItIsFS>>" .$ var "^fuel_arg^" .$ var "inter^<n>" .$ var "inter^<{arg:1}>")
+                     }
+              ]
+          ]
+      , scope = var "<DerivedGen.IsFS>[0, 1]" .$ var "^outmost-fuel^" .$ var "outer^<n>" .$ var "outer^<v>"
+      }
+
diff --git a/tests/derivation/least-effort/print/regression/underscore-in-cons-impl-full/run b/tests/derivation/least-effort/print/regression/underscore-in-cons-impl-full/run
@@ -0,0 +1 @@
+../_common/run
diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/expected b/tests/derivation/least-effort/run/regression/underscore-in-cons-expl-full-gend1/expected
@@ -2,7 +2,7 @@
 2/2: Building DerivedGen (DerivedGen.idr)
 Error: While processing right hand side of checkedGen. Sorry, I can't find any elaboration which works. All errors:
 Possible error:
-    Error during reflection: While processing right hand side of {u:1837},<DerivedGen.IsFS>[0]. While processing right hand side of $resolved13832,<<DerivedGen.ItIsFS>>. {k:1755} is not accessible in this context.
+    Error during reflection: While processing right hand side of {u:1837},<DerivedGen.IsFS>[0]. While processing right hand side of $resolved13825,<<DerivedGen.ItIsFS>>. {k:1755} is not accessible in this context.
 
 Possible error:
     Error during reflection: No arguments in the generator function signature, at least a fuel argument must be present

diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-impl-full/DerivedGen.idr b/tests/derivation/least-effort/run/regression/underscore-in-cons-impl-full/DerivedGen.idr
@@ -0,0 +1,23 @@
+module DerivedGen
+
+import RunDerivedGen
+
+import Data.Fin
+
+%default total
+
+data IsFS : Fin n -> Type where
+  ItIsFS : IsFS (FS i)
+
+Show (IsFS vs) where show ItIsFS = "ItIsFS"
+
+%language ElabReflection
+
+checkedGen : Fuel -> {n : Nat} -> (v : Fin n) -> Gen MaybeEmpty $ IsFS v
+checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}
+
+main : IO ()
+main = runGs
+  [ G $ \fl => checkedGen fl $ the (Fin 4) 3
+  , G $ \fl => checkedGen fl $ the (Fin 3) 0
+  ]
diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-impl-full/RunDerivedGen.idr b/tests/derivation/least-effort/run/regression/underscore-in-cons-impl-full/RunDerivedGen.idr
@@ -0,0 +1 @@
+../_common/RunDerivedGen.idr
diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-impl-full/derive.ipkg b/tests/derivation/least-effort/run/regression/underscore-in-cons-impl-full/derive.ipkg
@@ -0,0 +1 @@
+../_common/derive.ipkg
diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-impl-full/expected b/tests/derivation/least-effort/run/regression/underscore-in-cons-impl-full/expected
@@ -0,0 +1,25 @@
+1/2: Building RunDerivedGen (RunDerivedGen.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+Generated values:
+-----
+-----
+ItIsFS
+-----
+ItIsFS
+-----
+ItIsFS
+-----
+ItIsFS
+-----
+ItIsFS
+-----
+ItIsFS
+-----
+ItIsFS
+-----
+ItIsFS
+-----
+ItIsFS
+-----
+ItIsFS
+-----
diff --git a/tests/derivation/least-effort/run/regression/underscore-in-cons-impl-full/run b/tests/derivation/least-effort/run/regression/underscore-in-cons-impl-full/run
@@ -0,0 +1 @@
+../_common/run