From c3ee2a3facaf2db4e2b78bc2822f69aca1039357 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Tue, 2 Jun 2020 12:13:38 +0100 Subject: [PATCH] Change genSym behaviour Instead of merely generating a locally unique name, use the existing code for generating a new unique variable name in the unifier, which is therefore globally unique. --- src/TTImp/Elab/RunElab.idr | 4 ++-- tests/idris2/reflection003/expected | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index 7bbfff585..75ad2d97c 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/src/TTImp/Elab/RunElab.idr @@ -84,8 +84,8 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp scriptRet (Just !(unelabNoSugar env ty)) elabCon defs "GenSym" [str] = do str' <- evalClosure defs str - n <- uniqueName defs [] !(reify defs str') - scriptRet (UN n) + n <- genVarName !(reify defs str') + scriptRet n elabCon defs "InCurrentNS" [n] = do n' <- evalClosure defs n nsn <- inCurrentNS !(reify defs n') diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected index bba3c69dc..f48ec40b1 100644 --- a/tests/idris2/reflection003/expected +++ b/tests/idris2/reflection003/expected @@ -12,4 +12,4 @@ Error during reflection: Still not trying refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1: Error during reflection: Undefined name refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1: -Error during reflection: failed after generating Main.plus_1 +Error during reflection: failed after generating Main.{plus:5817}