git.iko.soy/Idris-dev
on master help sign in
Changed tests for new record syntax.
7d42ba2Sune Alkærsig
test/basic001/reg005.dSYM/Contents/Info.plistnew file+20
compare with master
unifiedsplit
@@ -0,0 +1,20 @@
1+<?xml version="1.0" encoding="UTF-8"?>
2+<!DOCTYPE plist PUBLIC "-//Apple Computer//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
3+<plist version="1.0">
4+ <dict>
5+ <key>CFBundleDevelopmentRegion</key>
6+ <string>English</string>
7+ <key>CFBundleIdentifier</key>
8+ <string>com.apple.xcode.dsym.reg005</string>
9+ <key>CFBundleInfoDictionaryVersion</key>
10+ <string>6.0</string>
11+ <key>CFBundlePackageType</key>
12+ <string>dSYM</string>
13+ <key>CFBundleSignature</key>
14+ <string>????</string>
15+ <key>CFBundleShortVersionString</key>
16+ <string>1.0</string>
17+ <key>CFBundleVersion</key>
18+ <string>1</string>
19+ </dict>
20+</plist>
test/basic001/reg005.dSYM/Contents/Resources/DWARF/reg005new file

Binary file not shown.

test/records001/test011.idr+10−8
@@ -2,14 +2,16 @@ module Main
2
2
3import Data.Vect
3import Data.Vect
4
4
5−record Foo : Nat -> Type where
5+record Foo (n : Nat) where
6+ constructor MkFoo
6− MkFoo : (name : String) ->
7+ name : String
7− (things : Vect n a) ->
8+ things : Vect n a
8− (more_things : Vect m b) ->
9+ more_things : Vect m b
9− Foo n
10+
10−
11−record Person : Type where
11+record Person where
12+ constructor MkPerson
12− MkPerson : (name : String) -> (age : Int) -> Person
13+ name : String
14+ age : Int
13
15
14testFoo : Foo 3
16testFoo : Foo 3
15testFoo = MkFoo "name" [1,2,3] [4,5,6,7]
17testFoo = MkFoo "name" [1,2,3] [4,5,6,7]
test/records002/record002.idr+7−6
@@ -1,11 +1,12 @@
1−
2−record Foo : Nat -> Type where
1+record Foo (param : Nat) where
3− MkFoo : (param : Nat) -> (num : Int) -> Foo param
2+ constructor MkFoo
3+ num : Int
4
4
5instance Show (Foo n) where
5instance Show (Foo n) where
6− show f = show (param f) ++ ", " ++ show (num f)
6+ show f = show (param_param f) ++ ", " ++ show (num f)
7
7
8main : IO ()
8main : IO ()
9−main = do let x = MkFoo 10 20
9+main = do let x = MkFoo {param=10} 20
10− putStrLn (show (record { param = 42 } x))
10+ putStrLn (show (record { param_param = 42 } x))
11 putStrLn (show (record { num = 42 } x))
11 putStrLn (show (record { num = 42 } x))
12+
test/records003/records003.idr+32−26
@@ -1,47 +1,53 @@
1−record Person : Nat -> Type where
1+record Person (age : Nat) where
2− MkPerson : (name : String) ->
2+ constructor MkPerson
3− (age : Nat) ->
3+ name : String
4− Person age
4+
5−
5+--set_param_age : (age_in : Nat) -> Person age -> Person age_in
6+--set_param_age age_in (MkPerson {age=age} name) = MkPerson {age=age_in} name
7+
6−record Event : Type where
8+record Event where
9+ constructor MkEvent
10+ name : String
7− MkEvent : (name : String) -> (organiser : Person a) -> Event
11+ organiser : Person a
8−
12+
9−record Meeting : Int -> Type where
13+record Meeting (year : Int) where
14+ constructor MkMeeting
10− MkMeeting : (event : Event) ->
15+ event : Event
11− (organiser : Person a) ->
16+ organiser : Person a
12− (year : Int) ->
13− Meeting year
14
17
15new_organiser : String -> List (Meeting x) -> List (Meeting x)
18new_organiser : String -> List (Meeting x) -> List (Meeting x)
16new_organiser n = map (record { event->organiser->name = n })
19new_organiser n = map (record { event->organiser->name = n })
17
20
21+--set_param_year : (year_in : Int) -> Meeting year -> Meeting year_in
22+--set_param_year year_in (MkMeeting {year=year} event organiser) = MkMeeting {year=year_in} event organiser
23+
18next_year : Meeting x -> Meeting (x+1)
24next_year : Meeting x -> Meeting (x+1)
19−next_year m = record { organiser->age
25+next_year m = record { organiser->param_age
20− = record { organiser->age } m + 1,
26+ = record { organiser->param_age } m + 1,
21− event->organiser->age
27+ event->organiser->param_age
22− = record { event->organiser->age } m + 1,
28+ = record { event->organiser->param_age } m + 1,
23− year = _ } m
29+ param_year = _ } m
24
30
25fred : Person 20
31fred : Person 20
26−fred = MkPerson "Fred" _
32+fred = MkPerson "Fred"
27
33
28jim : Person 29
34jim : Person 29
29−jim = MkPerson "Jim" 29
35+jim = MkPerson {age=29} "Jim"
30
36
31idm : Event
37idm : Event
32idm = MkEvent "Idris Developers Meeting" fred
38idm = MkEvent "Idris Developers Meeting" fred
33
39
34idm_gbg : Meeting 2014
40idm_gbg : Meeting 2014
35−idm_gbg = MkMeeting idm jim _
41+idm_gbg = MkMeeting idm jim
36
42
37test : Meeting 2015
43test : Meeting 2015
38test = next_year idm_gbg
44test = next_year idm_gbg
39
45
40main : IO ()
46main : IO ()
41main = do print (record { event->organiser->name } test)
47main = do print (record { event->organiser->name } test)
42− print (record { event->organiser->age } test)
48+ print (record { event->organiser->param_age } test)
43− print (record { event->organiser->age } idm_gbg)
49+ print (record { event->organiser->param_age } idm_gbg)
44− print (record { organiser->age } test)
50+ print (record { organiser->param_age } test)
45− print (record { organiser->age } idm_gbg)
51+ print (record { organiser->param_age } idm_gbg)
46− print (record { year } idm_gbg)
52+ print (record { param_year } idm_gbg)
47
53