8e112d7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added tests

commit8e112d79eec536186d05da1d9dced6dc02d73fd5 authorsualitu <sual@itu.dk> dateMon 6 Apr 2015, 12:16 (12 years ago) parent9c13628

15 files changed+100−6

compare with master

unifiedsplit

libs/prelude/Prelude/Nat.idr−2 src/Idris/Elab/Record.hs+2−1 src/Idris/ParseData.hs+1−1 src/Idris/ParseHelpers.hs−2 test/basic001/reg005.dSYM/Contents/Resources/DWARF/reg005 test/corecords001/corecords001.idr+24 test/corecords001/expected+5 test/corecords001/run+4 test/corecords002/corecords002.idr+24 test/corecords002/expected+3 test/corecords002/run+4 test/docs004/docs004.idr+11 test/docs004/expected+16 test/docs004/input+3 test/docs004/run+3

libs/prelude/Prelude/Nat.idr−2

@@ -214,8 +214,6 @@ instance Cast Integer Nat where

214214 cast = fromInteger

215215

216216||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)

217−--record Multiplicative : Type where

218−-- getMultiplicative : Nat -> Multiplicative

219217record Multiplicative where

220218 constructor getMultiplicative

221219 _ : Nat

src/Idris/Elab/Record.hs+2−1

@@ -40,6 +40,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

4040 logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy

4141

4242 -- Build data declaration for elaboration

43+ iLOG $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)

4344 let datadecl = PDatadecl tyn tycon [(cdoc, dconsArgDocs, dconName, dconTy, fc, [])]

4445 elabData info rsyn doc paramDocs fc opts datadecl

4546

@@ -88,7 +89,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

8889 dconsArgDocs = paramDocs ++ (dcad fieldsWithName)

8990 where

9091 dcad :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Docstring (Either Err PTerm))]

91− dcad ((n, _, _, (Just d)) : rest) = (n, d) : (dcad rest)

92+ dcad ((n, _, _, (Just d)) : rest) = ((nsroot n), d) : (dcad rest)

9293 dcad (_ : rest) = dcad rest

9394 dcad [] = []

9495

src/Idris/ParseData.hs+1−1

@@ -101,7 +101,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

101101 t <- typeExpr (allowImp syn)

102102 p <- endPlicity c

103103 ist <- get

104− let doc' = case doc of

104+ let doc' = case doc of -- Temp: Throws away any possible arg docs

105105 Just (d,_) -> Just $ annotate syn ist d

106106 Nothing -> Nothing

107107 return (n, p, t, doc')

src/Idris/ParseHelpers.hs−2

@@ -189,8 +189,6 @@ docComment = do dc <- pushIndent *> docCommentLine

189189 eol ; someSpace

190190 return (n, docs)

191191

192−

193−

194192-- | Parses some white space

195193whiteSpace :: MonadicParsing m => m ()

196194whiteSpace = Tok.whiteSpace

test/basic001/reg005.dSYM/Contents/Resources/DWARF/reg005

Binary file not shown.

test/corecords001/corecords001.idrnew file+24

@@ -0,0 +1,24 @@

1+module Main

3+corecord Str a where -- Current stream is codata, not a corecord

4+ constructor (::)

5+ head : a

6+ tail : Str a

8+instance Functor Str where

9+ map f (x :: xs) = (f x) :: (map f xs)

10+

11+total -- marked total to check that corecords are indeed treated as coinductive types

12+zeros : Str Int

13+zeros = 0 :: zeros

14+

15+ones : Str Int

16+ones = map (1+) zeros

17+

18+main : IO ()

19+main = do let x = record { head = 1 } zeros

20+ printLn $ head zeros

21+ printLn $ head x

22+ printLn $ head (record { head = 3 } x)

23+ printLn $ head (tail ones)

24+ printLn $ head (tail (record { tail = zeros } ones))

test/corecords001/expectednew file+5

@@ -0,0 +1,5 @@

1+0

2+1

3+3

4+1

5+0

test/corecords001/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ corecords001.idr -o corecords001

3+./corecords001

4+rm -f corecords001 corecords001.ibc

test/corecords002/corecords002.idrnew file+24

@@ -0,0 +1,24 @@

1+module Main

3+corecord Foo (n : Nat) where

4+ constructor MkFoo

5+ bar : String

6+ baz : Foo n

8+corecord Blargh where

9+ constructor MkBlargh

10+ num : Nat

11+ argh : Foo num

12+

13+total

14+foo : Foo 7

15+foo = MkFoo "Foo" foo

16+

17+total

18+blargh : Blargh

19+blargh = MkBlargh 7 foo

20+

21+main : IO ()

22+main = do printLn (record { argh->bar } blargh)

23+ printLn (record { argh->baz->bar } blargh)

24+ printLn (record { argh->baz->baz->bar } blargh)

test/corecords002/expectednew file+3

@@ -0,0 +1,3 @@

1+"Foo"

2+"Foo"

3+"Foo"

test/corecords002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ corecords002.idr -o corecords002

3+./corecords002

4+rm -f corecords002 corecords002.ibc

test/docs004/docs004.idrnew file+11

@@ -0,0 +1,11 @@

1+module Main

3+||| Some record Foo

4+||| @a a type

5+record Foo a where

6+ ||| Constructor for Foo

7+ constructor MkFoo

8+ ||| A field bar

9+ bar : Nat

10+ ||| A field baz

11+ baz : Bool

test/docs004/expectednew file+16

@@ -0,0 +1,16 @@

1+Type checking ./docs004.idr

2+MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a

3+ Constructor for Foo

4+ Arguments:

5+ (implicit) a : Type -- a type

7+ bar : Nat -- A field bar

9+ baz : Bool -- A field baz

10+

11+bar : (rec : Foo a) -> Nat

12+ A field bar

13+

14+baz : (rec : Foo a) -> Bool

15+ A field baz

16+

test/docs004/inputnew file+3

@@ -0,0 +1,3 @@

1+:doc MkFoo

2+:doc bar

3+:doc baz

test/docs004/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --quiet --nocolor --consolewidth 80 docs004.idr < input

3+rm *.ibc