mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 06:52:19 +03:00
[ new ] support record projections in refc backend (#1054)
This commit is contained in:
parent
0705ba55c5
commit
5384560009
@ -86,6 +86,7 @@ cName (UN n) = cCleanString n
|
||||
cName (MN n i) = cCleanString n ++ "_" ++ cCleanString (show i)
|
||||
cName (PV n d) = "pat__" ++ cName n
|
||||
cName (DN _ n) = cName n
|
||||
cName (RF n) = "rec__" ++ cCleanString n
|
||||
cName (Nested i n) = "n__" ++ cCleanString (show i) ++ "_" ++ cName n
|
||||
cName (CaseBlock x y) = "case__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
|
||||
cName (WithBlock x y) = "with__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
|
||||
|
@ -180,7 +180,7 @@ chezTests = MkTestPool [Chez]
|
||||
|
||||
refcTests : TestPool
|
||||
refcTests = MkTestPool [C]
|
||||
[ "refc001" ]
|
||||
[ "refc001" , "refc002" ]
|
||||
|
||||
racketTests : TestPool
|
||||
racketTests = MkTestPool [Racket]
|
||||
|
21
tests/refc/refc002/RecordProjection.idr
Normal file
21
tests/refc/refc002/RecordProjection.idr
Normal file
@ -0,0 +1,21 @@
|
||||
module RecordProjection
|
||||
|
||||
record Name where
|
||||
constructor MkName
|
||||
firstName : String
|
||||
lastName : String
|
||||
|
||||
(.fullName) : Name -> String
|
||||
name.fullName = name.firstName ++ " " ++ name.lastName
|
||||
|
||||
johnSmith : Name
|
||||
johnSmith = MkName
|
||||
{ firstName = "John"
|
||||
, lastName = "Smith"
|
||||
}
|
||||
|
||||
main : IO ()
|
||||
main = assert_total $ do
|
||||
putStrLn johnSmith.firstName
|
||||
putStrLn johnSmith.lastName
|
||||
putStrLn johnSmith.fullName
|
3
tests/refc/refc002/expected
Normal file
3
tests/refc/refc002/expected
Normal file
@ -0,0 +1,3 @@
|
||||
John
|
||||
Smith
|
||||
John Smith
|
4
tests/refc/refc002/run
Normal file
4
tests/refc/refc002/run
Normal file
@ -0,0 +1,4 @@
|
||||
$1 --no-banner --no-color --console-width 0 --cg refc -o refc002 RecordProjection.idr > /dev/null
|
||||
./build/exec/refc002
|
||||
|
||||
rm -rf build
|
Loading…
Reference in New Issue
Block a user