idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-26 05:01:34 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #291 from melted/fix_refl003

Browse Source 
Fix overly nitpicky reflection test
This commit is contained in:
Niklas Larsson 2020-06-12 13:16:48 +02:00 committed by GitHub
commit d86d96f35a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 12 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
tests/idris2/reflection003/expected
View File

@ -5,11 +5,11 @@ LOG 0: Name: Prelude.Strings.++
LOG 0: Type: (%pi Rig1 Explicit (Just _) String (%pi Rig1 Explicit (Just _) String String))
LOG 0: Resolved name: Prelude.Nat
LOG 0: Constructors: [Prelude.Z, Prelude.S]
refprims.idr:37:10--39:1:While processing right hand side of dummy1 at refprims.idr:37:1--39:1:
refprims.idr:43:10--45:1:While processing right hand side of dummy1 at refprims.idr:43:1--45:1:
Error during reflection: Not really trying
refprims.idr:40:10--42:1:While processing right hand side of dummy2 at refprims.idr:40:1--42:1:
refprims.idr:46:10--48:1:While processing right hand side of dummy2 at refprims.idr:46:1--48:1:
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:
refprims.idr:49:10--51:1:While processing right hand side of dummy3 at refprims.idr:49:1--51: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:6078}
refprims.idr:52:10--54:1:While processing right hand side of dummy4 at refprims.idr:52:1--54:1:
Error during reflection: failed after generating Main.{plus:XXXX}

8
tests/idris2/reflection003/refprims.idr
View File

@ -27,11 +27,17 @@ logBad
logMsg 0 ("Constructors: " ++ show !(getCons n))
fail "Still not trying"
-- because the exact sequence number in a gensym depends on
-- the library and compiler internals we need to censor it so the
-- output won't be overly dependent on the exact versions used.
censorDigits : String -> String
censorDigits str = pack $ map (\c => if isDigit c then 'X' else c) (unpack str)
tryGenSym : Elab a
tryGenSym
= do n <- genSym "plus"
ns <- inCurrentNS n
fail $ "failed after generating " ++ show ns
fail $ "failed after generating " ++ censorDigits (show ns)
dummy1 : a
dummy1 = %runElab logPrims