From 8e1cc4fd833ec5fd6d257c28ef55cdaec4fe13b6 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Wed, 28 Aug 2024 16:04:48 +0300
Subject: [PATCH] [ test ] Add some simpler tests with implicit args of derived
 types

---
 .../norec t-pi->.. noext 005/DerivedGen.idr   | 34 +++++++++++++++
 .../RunDerivedGen.idr                         |  1 +
 .../core/norec t-pi->.. noext 005/derive.ipkg |  1 +
 .../core/norec t-pi->.. noext 005/expected    | 12 ++++++
 .../core/norec t-pi->.. noext 005/run         |  1 +
 .../norec t-pi->.. w_ext 003/DerivedGen.idr   | 41 +++++++++++++++++++
 .../RunDerivedGen.idr                         |  1 +
 .../core/norec t-pi->.. w_ext 003/derive.ipkg |  1 +
 .../core/norec t-pi->.. w_ext 003/expected    | 12 ++++++
 .../core/norec t-pi->.. w_ext 003/run         |  1 +
 10 files changed, 105 insertions(+)
 create mode 100644 tests/derivation/core/norec t-pi->.. noext 005/DerivedGen.idr
 create mode 120000 tests/derivation/core/norec t-pi->.. noext 005/RunDerivedGen.idr
 create mode 120000 tests/derivation/core/norec t-pi->.. noext 005/derive.ipkg
 create mode 100644 tests/derivation/core/norec t-pi->.. noext 005/expected
 create mode 120000 tests/derivation/core/norec t-pi->.. noext 005/run
 create mode 100644 tests/derivation/core/norec t-pi->.. w_ext 003/DerivedGen.idr
 create mode 120000 tests/derivation/core/norec t-pi->.. w_ext 003/RunDerivedGen.idr
 create mode 120000 tests/derivation/core/norec t-pi->.. w_ext 003/derive.ipkg
 create mode 100644 tests/derivation/core/norec t-pi->.. w_ext 003/expected
 create mode 120000 tests/derivation/core/norec t-pi->.. w_ext 003/run

diff --git a/tests/derivation/core/norec t-pi->.. noext 005/DerivedGen.idr b/tests/derivation/core/norec t-pi->.. noext 005/DerivedGen.idr
new file mode 100644
index 000000000..284af74cb
--- /dev/null
+++ b/tests/derivation/core/norec t-pi->.. noext 005/DerivedGen.idr	
@@ -0,0 +1,34 @@
+module DerivedGen
+
+import Data.Fin
+
+import Deriving.Show
+
+import RunDerivedGen
+
+%default total
+
+%language ElabReflection
+
+data FinEq : Fin n -> Fin n -> Type where
+  Here  : FinEq FZ FZ
+  These : FinEq n m -> FinEq (FS n) (FS m)
+
+data X : (n : Nat) -> Fin n -> Fin n -> Type where
+  MkX : (i1, i2 : Fin n) -> (i1 `FinEq` i2) -> X n i1 i2
+
+%hint ShowFinEq : {0 a, b : Fin n} -> Show (FinEq a b); ShowFinEq = %runElab derive
+
+Show (X n i1 i2) where
+  show $ MkX i1 i2 prf = "MkX \{show i1} \{show i2} \{show prf}"
+
+checkedGen : Fuel -> (n : Nat) -> (i1 : Fin n) -> (i2 : Fin n) -> Gen MaybeEmpty (X n i1 i2)
+checkedGen = deriveGen
+
+main : IO ()
+main = runGs
+  [ G $ \fl => checkedGen fl 3 0 1
+  , G $ \fl => checkedGen fl 3 1 1
+  , G $ \fl => checkedGen fl 3 2 1
+  , G $ \fl => checkedGen fl 3 2 2
+  ]
diff --git a/tests/derivation/core/norec t-pi->.. noext 005/RunDerivedGen.idr b/tests/derivation/core/norec t-pi->.. noext 005/RunDerivedGen.idr
new file mode 120000
index 000000000..2b18cc56c
--- /dev/null
+++ b/tests/derivation/core/norec t-pi->.. noext 005/RunDerivedGen.idr	
@@ -0,0 +1 @@
+../_common/RunDerivedGen.idr
\ No newline at end of file
diff --git a/tests/derivation/core/norec t-pi->.. noext 005/derive.ipkg b/tests/derivation/core/norec t-pi->.. noext 005/derive.ipkg
new file mode 120000
index 000000000..ff0da46fe
--- /dev/null
+++ b/tests/derivation/core/norec t-pi->.. noext 005/derive.ipkg	
@@ -0,0 +1 @@
+../_common/derive.ipkg
\ No newline at end of file
diff --git a/tests/derivation/core/norec t-pi->.. noext 005/expected b/tests/derivation/core/norec t-pi->.. noext 005/expected
new file mode 100644
index 000000000..0bbb77a96
--- /dev/null
+++ b/tests/derivation/core/norec t-pi->.. noext 005/expected	
@@ -0,0 +1,12 @@
+1/2: Building RunDerivedGen (RunDerivedGen.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+Error: While processing right hand side of checkedGen. Error during reflection: Named implicit applications (like to `DerivedGen.FinEq`) are not supported yet
+
+DerivedGen:14:11--14:22
+ 10 | 
+ 11 | %language ElabReflection
+ 12 | 
+ 13 | data FinEq : Fin n -> Fin n -> Type where
+ 14 |   Here  : FinEq FZ FZ
+                ^^^^^^^^^^^
+
diff --git a/tests/derivation/core/norec t-pi->.. noext 005/run b/tests/derivation/core/norec t-pi->.. noext 005/run
new file mode 120000
index 000000000..805165988
--- /dev/null
+++ b/tests/derivation/core/norec t-pi->.. noext 005/run	
@@ -0,0 +1 @@
+../_common/run
\ No newline at end of file
diff --git a/tests/derivation/core/norec t-pi->.. w_ext 003/DerivedGen.idr b/tests/derivation/core/norec t-pi->.. w_ext 003/DerivedGen.idr
new file mode 100644
index 000000000..292c17f63
--- /dev/null
+++ b/tests/derivation/core/norec t-pi->.. w_ext 003/DerivedGen.idr	
@@ -0,0 +1,41 @@
+module DerivedGen
+
+import Data.Fin
+
+import Deriving.Show
+
+import RunDerivedGen
+
+%default total
+
+%language ElabReflection
+
+data FinEq : Fin n -> Fin n -> Type where
+  Here  : FinEq FZ FZ
+  These : FinEq n m -> FinEq (FS n) (FS m)
+
+data X : (n : Nat) -> Fin n -> Fin n -> Type where
+  MkX : (i1, i2 : Fin n) -> (i1 `FinEq` i2) -> X n i1 i2
+
+%hint ShowFinEq : {0 a, b : Fin n} -> Show (FinEq a b); ShowFinEq = %runElab derive
+
+Show (X n i1 i2) where
+  show $ MkX i1 i2 prf = "MkX \{show i1} \{show i2} \{show prf}"
+
+checkedGen : Fuel -> (Fuel -> {n : Nat} -> (i1, i2 : Fin n) -> Gen MaybeEmpty $ FinEq i1 i2) =>
+             (n : Nat) -> (i1 : Fin n) -> (i2 : Fin n) -> Gen MaybeEmpty (X n i1 i2)
+checkedGen = deriveGen
+
+genFinEq : Fuel -> {n : Nat} -> (i1, i2 : Fin n) -> Gen MaybeEmpty $ FinEq i1 i2
+genFinEq _  FZ     FZ     = pure Here
+genFinEq fl (FS y) (FS z) = These <$> genFinEq fl y z
+genFinEq _  FZ     (FS _) = empty
+genFinEq _  (FS _) FZ     = empty
+
+main : IO ()
+main = runGs
+  [ G $ \fl => checkedGen @{genFinEq} fl 3 0 1
+  , G $ \fl => checkedGen @{genFinEq} fl 3 1 1
+  , G $ \fl => checkedGen @{genFinEq} fl 3 2 1
+  , G $ \fl => checkedGen @{genFinEq} fl 3 2 2
+  ]
diff --git a/tests/derivation/core/norec t-pi->.. w_ext 003/RunDerivedGen.idr b/tests/derivation/core/norec t-pi->.. w_ext 003/RunDerivedGen.idr
new file mode 120000
index 000000000..2b18cc56c
--- /dev/null
+++ b/tests/derivation/core/norec t-pi->.. w_ext 003/RunDerivedGen.idr	
@@ -0,0 +1 @@
+../_common/RunDerivedGen.idr
\ No newline at end of file
diff --git a/tests/derivation/core/norec t-pi->.. w_ext 003/derive.ipkg b/tests/derivation/core/norec t-pi->.. w_ext 003/derive.ipkg
new file mode 120000
index 000000000..ff0da46fe
--- /dev/null
+++ b/tests/derivation/core/norec t-pi->.. w_ext 003/derive.ipkg	
@@ -0,0 +1 @@
+../_common/derive.ipkg
\ No newline at end of file
diff --git a/tests/derivation/core/norec t-pi->.. w_ext 003/expected b/tests/derivation/core/norec t-pi->.. w_ext 003/expected
new file mode 100644
index 000000000..37b409bfc
--- /dev/null
+++ b/tests/derivation/core/norec t-pi->.. w_ext 003/expected	
@@ -0,0 +1,12 @@
+1/2: Building RunDerivedGen (RunDerivedGen.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+Error: While processing right hand side of checkedGen. Error during reflection: Target types with implicit type parameters are not supported yet
+
+DerivedGen:25:81--25:92
+ 21 | 
+ 22 | Show (X n i1 i2) where
+ 23 |   show $ MkX i1 i2 prf = "MkX \{show i1} \{show i2} \{show prf}"
+ 24 | 
+ 25 | checkedGen : Fuel -> (Fuel -> {n : Nat} -> (i1, i2 : Fin n) -> Gen MaybeEmpty $ FinEq i1 i2) =>
+                                                                                      ^^^^^^^^^^^
+
diff --git a/tests/derivation/core/norec t-pi->.. w_ext 003/run b/tests/derivation/core/norec t-pi->.. w_ext 003/run
new file mode 120000
index 000000000..805165988
--- /dev/null
+++ b/tests/derivation/core/norec t-pi->.. w_ext 003/run	
@@ -0,0 +1 @@
+../_common/run
\ No newline at end of file