From 448a73e4364c143baaf9026a32df0f5a2e4aad5e Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Mon, 18 Dec 2023 19:13:40 +0300 Subject: [PATCH] [ fix, re #3063 ] Fix forgotten reflection values --- src/Core/Reflect.idr | 4 ++-- .../idris2/reflection/reflection026/Issue3168.idr | 15 +++++++++++++++ tests/idris2/reflection/reflection026/expected | 1 + tests/idris2/reflection/reflection026/run | 3 +++ tests/idris2/reflection/reflection026/test.ipkg | 1 + 5 files changed, 22 insertions(+), 2 deletions(-) create mode 100644 tests/idris2/reflection/reflection026/Issue3168.idr create mode 100644 tests/idris2/reflection/reflection026/expected create mode 100755 tests/idris2/reflection/reflection026/run create mode 100644 tests/idris2/reflection/reflection026/test.ipkg diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr index c229cc93e0..c464c454f9 100644 --- a/src/Core/Reflect.idr +++ b/src/Core/Reflect.idr @@ -330,9 +330,9 @@ export Reflect a => Reflect (WithDefault a def) where reflect fc defs lhs env def = onWithDefault - (appCon fc defs (reflectionttimp "Default") [Erased fc Placeholder, Erased fc Placeholder]) + (appCon fc defs (reflectionttimp "DefaultedValue") [Erased fc Placeholder, Erased fc Placeholder]) (\x => do x' <- reflect fc defs lhs env x - appCon fc defs (reflectionttimp "Value") [Erased fc Placeholder, Erased fc Placeholder, x']) + appCon fc defs (reflectionttimp "SpecifiedValue") [Erased fc Placeholder, Erased fc Placeholder, x']) def export diff --git a/tests/idris2/reflection/reflection026/Issue3168.idr b/tests/idris2/reflection/reflection026/Issue3168.idr new file mode 100644 index 0000000000..734ff5f676 --- /dev/null +++ b/tests/idris2/reflection/reflection026/Issue3168.idr @@ -0,0 +1,15 @@ +import Language.Reflection + +%language ElabReflection + +data_decl : List Decl +data_decl = `[data T = A | B] + +record_decl : List Decl +record_decl = `[record R where] + +data_decl' : List Decl +data_decl' = `[public export data T = A | B] + +record_decl' : List Decl +record_decl' = `[public export record R where] diff --git a/tests/idris2/reflection/reflection026/expected b/tests/idris2/reflection/reflection026/expected new file mode 100644 index 0000000000..5d85513b9c --- /dev/null +++ b/tests/idris2/reflection/reflection026/expected @@ -0,0 +1 @@ +1/1: Building Issue3168 (Issue3168.idr) diff --git a/tests/idris2/reflection/reflection026/run b/tests/idris2/reflection/reflection026/run new file mode 100755 index 0000000000..350880b18c --- /dev/null +++ b/tests/idris2/reflection/reflection026/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Issue3168.idr diff --git a/tests/idris2/reflection/reflection026/test.ipkg b/tests/idris2/reflection/reflection026/test.ipkg new file mode 100644 index 0000000000..2c5b5ab52d --- /dev/null +++ b/tests/idris2/reflection/reflection026/test.ipkg @@ -0,0 +1 @@ +package a-test