git.iko.soy/Idris-dev
on master help sign in
Changed tests for new record syntax.
commit7d42ba28d75a28c14865aabf2ed568f7755c5082 authorSune Alkærsig <sual@itu.dk> dateThu 19 Mar 2015, 18:49 (12 years ago) parent7e43af7
5 files changed+69−40
compare with master
unifiedsplit
test/basic001/reg005.dSYM/Contents/Info.plist+20 test/basic001/reg005.dSYM/Contents/Resources/DWARF/reg005 test/records001/test011.idr+10−8 test/records002/record002.idr+7−6 test/records003/records003.idr+32−26
test/basic001/reg005.dSYM/Contents/Info.plistnew file+20
@@ -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
22
33import Data.Vect
44
5−record Foo : Nat -> Type where
6− MkFoo : (name : String) ->
7− (things : Vect n a) ->
8− (more_things : Vect m b) ->
9− Foo n
10−
11−record Person : Type where
12− MkPerson : (name : String) -> (age : Int) -> Person
5+record Foo (n : Nat) where
6+ constructor MkFoo
7+ name : String
8+ things : Vect n a
9+ more_things : Vect m b
10+
11+record Person where
12+ constructor MkPerson
13+ name : String
14+ age : Int
1315
1416testFoo : Foo 3
1517testFoo = 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
3− MkFoo : (param : Nat) -> (num : Int) -> Foo param
1+record Foo (param : Nat) where
2+ constructor MkFoo
3+ num : Int
44
55instance Show (Foo n) where
6− show f = show (param f) ++ ", " ++ show (num f)
6+ show f = show (param_param f) ++ ", " ++ show (num f)
77
88main : IO ()
9−main = do let x = MkFoo 10 20
10− putStrLn (show (record { param = 42 } x))
9+main = do let x = MkFoo {param=10} 20
10+ putStrLn (show (record { param_param = 42 } x))
1111 putStrLn (show (record { num = 42 } x))
12+
test/records003/records003.idr+32−26
@@ -1,47 +1,53 @@
1−record Person : Nat -> Type where
2− MkPerson : (name : String) ->
3− (age : Nat) ->
4− Person age
5−
6−record Event : Type where
7− MkEvent : (name : String) -> (organiser : Person a) -> Event
8−
9−record Meeting : Int -> Type where
10− MkMeeting : (event : Event) ->
11− (organiser : Person a) ->
12− (year : Int) ->
13− Meeting year
1+record Person (age : Nat) where
2+ constructor MkPerson
3+ name : String
4+
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+
8+record Event where
9+ constructor MkEvent
10+ name : String
11+ organiser : Person a
12+
13+record Meeting (year : Int) where
14+ constructor MkMeeting
15+ event : Event
16+ organiser : Person a
1417
1518new_organiser : String -> List (Meeting x) -> List (Meeting x)
1619new_organiser n = map (record { event->organiser->name = n })
1720
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+
1824next_year : Meeting x -> Meeting (x+1)
19−next_year m = record { organiser->age
20− = record { organiser->age } m + 1,
21− event->organiser->age
22− = record { event->organiser->age } m + 1,
23− year = _ } m
25+next_year m = record { organiser->param_age
26+ = record { organiser->param_age } m + 1,
27+ event->organiser->param_age
28+ = record { event->organiser->param_age } m + 1,
29+ param_year = _ } m
2430
2531fred : Person 20
26−fred = MkPerson "Fred" _
32+fred = MkPerson "Fred"
2733
2834jim : Person 29
29−jim = MkPerson "Jim" 29
35+jim = MkPerson {age=29} "Jim"
3036
3137idm : Event
3238idm = MkEvent "Idris Developers Meeting" fred
3339
3440idm_gbg : Meeting 2014
35−idm_gbg = MkMeeting idm jim _
41+idm_gbg = MkMeeting idm jim
3642
3743test : Meeting 2015
3844test = next_year idm_gbg
3945
4046main : IO ()
4147main = do print (record { event->organiser->name } test)
42− print (record { event->organiser->age } test)
43− print (record { event->organiser->age } idm_gbg)
44− print (record { organiser->age } test)
45− print (record { organiser->age } idm_gbg)
46− print (record { year } idm_gbg)
48+ print (record { event->organiser->param_age } test)
49+ print (record { event->organiser->param_age } idm_gbg)
50+ print (record { organiser->param_age } test)
51+ print (record { organiser->param_age } idm_gbg)
52+ print (record { param_year } idm_gbg)
4753