From e03096188af52e4113a19cc48b52e7af32190758 Mon Sep 17 00:00:00 2001 From: MarcelineVQ Date: Fri, 19 Jun 2020 22:28:48 -0700 Subject: [PATCH] add more Name reflections broaden what Names can be reflected and refied I did not add the Names I wasn't sure how to test but have put placeholders that produce clearer error messages. --- libs/base/Language/Reflection/TT.idr | 7 +++++ src/Core/Reflect.idr | 42 +++++++++++++++++++++++++--- tests/Main.idr | 2 +- tests/idris2/reflection010/Name.idr | 40 ++++++++++++++++++++++++++ tests/idris2/reflection010/expected | 10 +++++++ tests/idris2/reflection010/run | 3 ++ 6 files changed, 99 insertions(+), 5 deletions(-) create mode 100644 tests/idris2/reflection010/Name.idr create mode 100644 tests/idris2/reflection010/expected create mode 100755 tests/idris2/reflection010/run diff --git a/libs/base/Language/Reflection/TT.idr b/libs/base/Language/Reflection/TT.idr index a1188604e..f7009a988 100644 --- a/libs/base/Language/Reflection/TT.idr +++ b/libs/base/Language/Reflection/TT.idr @@ -64,6 +64,9 @@ data Name = UN String -- user defined name | MN String Int -- machine generated name | NS Namespace Name -- name in a namespace | DN String Name -- a name and how to display it + | Nested (Int, Int) Name -- nested function name + | CaseBlock Int Int -- case block nested in (resolved) name + | WithBlock Int Int -- with block nested in (resolved) name export Show Name where @@ -71,6 +74,10 @@ Show Name where show (UN x) = x show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}" show (DN str y) = str + show (Nested (outer, idx) inner) + = show outer ++ ":" ++ show idx ++ ":" ++ show inner + show (CaseBlock outer i) = "case block in " ++ show outer + show (WithBlock outer i) = "with block in " ++ show outer public export data Count = M0 | M1 | MW diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr index c6f9f77d7..dbeeace31 100644 --- a/src/Core/Reflect.idr +++ b/src/Core/Reflect.idr @@ -272,8 +272,22 @@ Reify Name where => do str' <- reify defs !(evalClosure defs str) n' <- reify defs !(evalClosure defs n) pure (DN str' n') - _ => cantReify val "Name" - reify defs val = cantReify val "Name" + (NS _ (UN "Nested"), [ix,str]) + => do ix' <- reify defs !(evalClosure defs ix) + str' <- reify defs !(evalClosure defs str) + pure (Nested ix' str') + (NS _ (UN "CaseBlock"), [outer,i]) + => do outer' <- reify defs !(evalClosure defs outer) + i' <- reify defs !(evalClosure defs i) + pure (CaseBlock outer' i') + (NS _ (UN "WithBlock"), [outer,i]) + => do outer' <- reify defs !(evalClosure defs outer) + i' <- reify defs !(evalClosure defs i) + pure (WithBlock outer' i') + (NS _ (UN _), _) + => cantReify val "Name, reifying it is unimplemented or intentionally internal" + _ => cantReify val "Name, the name was not found in context" + reify defs val = cantReify val "Name, value is not an NDCon interally" export Reflect Name where @@ -292,11 +306,31 @@ Reflect Name where = do str' <- reflect fc defs lhs env str n' <- reflect fc defs lhs env n appCon fc defs (reflectiontt "DN") [str', n'] + reflect fc defs lhs env (Nested ix n) + = do ix' <- reflect fc defs lhs env ix + n' <- reflect fc defs lhs env n + appCon fc defs (reflectiontt "Nested") [ix',n'] + reflect fc defs lhs env (CaseBlock outer i) + = do Resolved _ <- full (gamma defs) (Resolved i) + | _ => cantReflect fc + "Name inside CaseBlock, it is not a Resolved name" + outer' <- reflect fc defs lhs env outer + i' <- reflect fc defs lhs env i + appCon fc defs (reflectiontt "CaseBlock") [outer',i'] + reflect fc defs lhs env (WithBlock outer i) + = do Resolved _ <- full (gamma defs) (Resolved i) + | _ => cantReflect fc + "Name inside WithBlock, it is not a Resolved name" + outer' <- reflect fc defs lhs env outer + i' <- reflect fc defs lhs env i + appCon fc defs (reflectiontt "WithBlock") [outer',i'] reflect fc defs lhs env (Resolved i) = case !(full (gamma defs) (Resolved i)) of - Resolved _ => cantReflect fc "Name" + Resolved _ => cantReflect fc + "Name directly, Resolved is intentionally internal" n => reflect fc defs lhs env n - reflect fc defs lhs env val = cantReflect fc "Name" + reflect fc defs lhs env n = cantReflect fc + "Name, reflecting it is unimplemented or intentionally internal" export Reify NameType where diff --git a/tests/Main.idr b/tests/Main.idr index 63db6cdc9..d77e340bd 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -105,7 +105,7 @@ idrisTests -- Quotation and reflection "reflection001", "reflection002", "reflection003", "reflection004", "reflection005", "reflection006", "reflection007", "reflection008", - "reflection009", + "reflection009","reflection010", -- Miscellaneous regressions "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007", "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014", diff --git a/tests/idris2/reflection010/Name.idr b/tests/idris2/reflection010/Name.idr new file mode 100644 index 000000000..e1c6d7167 --- /dev/null +++ b/tests/idris2/reflection010/Name.idr @@ -0,0 +1,40 @@ +import Language.Reflection + +%language ElabReflection + +%logging 1 + +-- This test is for checking changes to how Names are reflected and reified. +-- It currently tests Names that refer to nested functions and Names that refer +-- to nested cases. + +-- Please add future tests for Names here if they would fit in. There's plenty +-- of room. + +data Identity a = MkIdentity a + +nested : Identity Int +nested = MkIdentity foo + where + foo : Int + foo = 12 + +-- a pattern matching lambda is really a case +cased : Identity Int -> Int +cased = \(MkIdentity x) => x + +test : Elab () +test = do + n <- quote nested + logTerm "" 1 "nested" n + MkIdentity n' <- check {expected=Identity Int} n + logMsg "" 1 $ show (n' == 12) + + c <- quote cased + logTerm "" 1 "cased" c + c' <- check {expected=Identity Int -> Int} c + logMsg "" 1 $ show (c' (MkIdentity 10)) + + pure () + +%runElab test diff --git a/tests/idris2/reflection010/expected b/tests/idris2/reflection010/expected new file mode 100644 index 000000000..3a3138f16 --- /dev/null +++ b/tests/idris2/reflection010/expected @@ -0,0 +1,10 @@ +1/1: Building Name (Name.idr) +LOG declare.data:1: Processing Main.Identity +LOG declare.type:1: Processing Main.nested +LOG declare.type:1: Processing Main.2091:3813:foo +LOG declare.type:1: Processing Main.cased +LOG declare.type:1: Processing Main.test +LOG 1: nested: ((Main.MkIdentity [Just a = Int]) Main.2091:3813:foo) +LOG 1: True +LOG 1: cased: (%lam RigW Explicit (Just {lamc:0}) (Main.Identity Int) (Main.case block in cased {lamc:0})) +LOG 1: 10 diff --git a/tests/idris2/reflection010/run b/tests/idris2/reflection010/run new file mode 100755 index 000000000..4bbf6a5d6 --- /dev/null +++ b/tests/idris2/reflection010/run @@ -0,0 +1,3 @@ +$1 --no-color --console-width 0 --no-banner --check Name.idr + +rm -rf build