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

lib/prelude/list.idr+2−2

compare with master

unifiedsplit

@@ -45,7 +45,7 @@ mapMaybe : (a -> Maybe b) -> List a -> List b

45mapMaybe f [] = []

46mapMaybe f (x :: xs) = case f x of

47 Nothing => mapMaybe f xs

48− | Just v => v :: mapMaybe f xs

48+ Just v => v :: mapMaybe f xs

49

50filter : (y -> Bool) -> List y -> List y

51filter pred [] = []

@@ -92,5 +92,5 @@ split : (a -> Bool) -> List a -> List (List a)

92split p [] = []

93split p xs = case break p xs of

94 (chunk, []) => [chunk]

95− | (chunk, (c :: rest)) => chunk :: split p rest

95+ (chunk, (c :: rest)) => chunk :: split p rest

96

lib/prelude/strings.idr+1−1

@@ -8,7 +8,7 @@ import prelude.char

8

9data StrM : String -> Set where

10 StrNil : StrM ""

11− | StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)

11+ StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)

12

13strHead' : (x : String) -> so (not (x == "")) -> Char

14strHead' x p = prim__strHead x

lib/prelude/vect.idr+2−2

@@ -6,7 +6,7 @@ import prelude.nat

6

7data Fin : Nat -> Set where

8 fO : Fin (S k)

9− | fS : Fin k -> Fin (S k)

9+ fS : Fin k -> Fin (S k)

10

11instance Eq (Fin n) where

12 fO == fO = True

@@ -17,7 +17,7 @@ infixr 7 ::

17

18data Vect : Set -> Nat -> Set where

19 Nil : Vect a O

20− | (::) : a -> Vect a k -> Vect a (S k)

20+ (::) : a -> Vect a k -> Vect a (S k)

21

22lookup : Fin n -> Vect a n -> a

23lookup fO (x :: xs) = x

src/Idris/Parser.hs+37−23

@@ -201,13 +201,20 @@ pTerminator = do lchar ';'; pop_indent

201 else fail "Not a terminator"

202 <|> lookAhead eof

203

204+pBarTerminator

205+ = do lchar '|'; return ()

206+ <|> do c <- indent; l <- last_indent

207+ if (c <= l) then return ()

208+ else fail "Not a terminator"

209+ <|> lookAhead eof

210+

204pKeepTerminator

211pKeepTerminator

205 = do lchar ';'; return ()

212 = do lchar ';'; return ()

206 <|> do c <- indent; l <- last_indent

213 <|> do c <- indent; l <- last_indent

207 if (c <= l) then return ()

214 if (c <= l) then return ()

208 else fail "Not a terminator"

215 else fail "Not a terminator"

209 <|> do i <- getInput; let h = take 1 i

216 <|> do i <- getInput; let h = take 1 i

210− if (h == "}" || h == ")") then return ()

217+ if (h == "}" || h == ")" || h == "|") then return ()

211 else fail "Not a terminator"

218 else fail "Not a terminator"

212 <|> lookAhead eof

219 <|> lookAhead eof

213

220

@@ -255,7 +262,7 @@ parseProg syn fname input pos

255 return (collect x)

262 return (collect x)

256 where ishow err = let ln = sourceLine (errorPos err) in

263 where ishow err = let ln = sourceLine (errorPos err) in

257 fname ++ ":" ++ show ln ++ ":parse error"

264 fname ++ ":" ++ show ln ++ ":parse error"

258− ++ " " ++ show (sourceColumn (errorPos err))

265+ ++ " at column " ++ show (sourceColumn (errorPos err))

259-- show (map messageString (errorMessages err))

266-- show (map messageString (errorMessages err))

260

267

261-- Collect PClauses with the same function name

268-- Collect PClauses with the same function name

@@ -605,7 +612,12 @@ pSimpleExpr syn =

605 return (PTactics ts)

612 return (PTactics ts)

606 <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";

613 <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";

607 open_block

614 open_block

615+ push_indent

616+ opts <- many1 (do notEndBlock

617+ x <- pCaseOpt syn

618+ pKeepTerminator

608− opts <- sepBy1 (pCaseOpt syn) (lchar '|')

619+ return x) -- sepBy1 (pCaseOpt syn) (lchar '|')

620+ pop_indent

609 close_block

621 close_block

610 return (PCase fc scr opts)

622 return (PCase fc scr opts)

611 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

623 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

@@ -883,34 +895,36 @@ accData (Just Frozen) n ns = do addAcc n (Just Frozen)

883accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns

895accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns

884

896

885pData :: SyntaxInfo -> IParser PDecl

897pData :: SyntaxInfo -> IParser PDecl

886−pData syn = try (do push_indent

887− acc <- pAccessibility

898+pData syn = try (do acc <- pAccessibility

888 reserved "data"; fc <- pfc

899 reserved "data"; fc <- pfc

889 tyn_in <- pfName; ty <- pTSig syn

900 tyn_in <- pfName; ty <- pTSig syn

890 let tyn = expandNS syn tyn_in

901 let tyn = expandNS syn tyn_in

891 reserved "where"

902 reserved "where"

892−-- ty' <- implicit syn tyn ty

903+ open_block

904+ push_indent

905+ cons <- many (do notEndBlock

893− cons <- sepBy (pConstructor syn) (lchar '|')

906+ c <- pConstructor syn

894− pTerminator

907+ pKeepTerminator

908+ return c) -- (lchar '|')

909+ pop_indent

910+ close_block

895 accData acc tyn (map (\ (n, _, _) -> n) cons)

911 accData acc tyn (map (\ (n, _, _) -> n) cons)

896 return $ PData syn fc (PDatadecl tyn ty cons))

912 return $ PData syn fc (PDatadecl tyn ty cons))

897− <|> do push_indent

913+ <|> try (do push_indent

898− acc <- pAccessibility

914+ acc <- pAccessibility

899− reserved "data"; fc <- pfc

915+ reserved "data"; fc <- pfc

900− tyn_in <- pfName; args <- many pName

916+ tyn_in <- pfName; args <- many pName

901− let tyn = expandNS syn tyn_in

917+ let tyn = expandNS syn tyn_in

902− lchar '='

918+ lchar '='

903− cons <- sepBy1 (pSimpleCon syn) (lchar '|')

919+ cons <- sepBy1 (pSimpleCon syn) (lchar '|')

904− pTerminator

920+ pTerminator

905− let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

921+ let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

906− let ty = bindArgs (map (\a -> PSet) args) PSet

922+ let ty = bindArgs (map (\a -> PSet) args) PSet

907−-- ty' <- implicit syn tyn ty

908− cons' <- mapM (\ (x, cargs, cfc) ->

923+ cons' <- mapM (\ (x, cargs, cfc) ->

909 do let cty = bindArgs cargs conty

924 do let cty = bindArgs cargs conty

910−-- cty' <- implicit syn x cty

911 return (x, cty, cfc)) cons

925 return (x, cty, cfc)) cons

912− accData acc tyn (map (\ (n, _, _) -> n) cons')

926+ accData acc tyn (map (\ (n, _, _) -> n) cons')

913− return $ PData syn fc (PDatadecl tyn ty cons')

927+ return $ PData syn fc (PDatadecl tyn ty cons'))

914 where

928 where

915 mkPApp fc t [] = t

929 mkPApp fc t [] = t

916 mkPApp fc t xs = PApp fc t (map pexp xs)

930 mkPApp fc t xs = PApp fc t (map pexp xs)

test/test001/test001.idr+8−8

@@ -11,11 +11,11 @@ using (G : Vect Ty n) {

11

12 data Env : Vect Ty n -> Set where

13 Nil : Env Nil

14− | (::) : interpTy a -> Env G -> Env (a :: G)

14+ (::) : interpTy a -> Env G -> Env (a :: G)

15

16 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

17 stop : HasType fO (t :: G) t

18− | pop : HasType k G t -> HasType (fS k) (u :: G) t

18+ pop : HasType k G t -> HasType (fS k) (u :: G) t

19

20 lookup : HasType i G t -> Env G -> interpTy t

21 lookup stop (x :: xs) = x

@@ -23,13 +23,13 @@ using (G : Vect Ty n) {

23

24 data Expr : Vect Ty n -> Ty -> Set where

25 Var : HasType i G t -> Expr G t

26− | Val : (x : Int) -> Expr G TyInt

26+ Val : (x : Int) -> Expr G TyInt

27− | Lam : Expr (a :: G) t -> Expr G (TyFun a t)

27+ Lam : Expr (a :: G) t -> Expr G (TyFun a t)

28− | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

28+ App : Expr G (TyFun a t) -> Expr G a -> Expr G t

29− | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

29+ Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

30 Expr G c

31− | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

31+ If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

32− | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

32+ Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

33

34 interp : Env G -> {static} Expr G t -> interpTy t

35 interp env (Var i) = lookup i env

test/test006/test006.idr+1−1

@@ -2,7 +2,7 @@ module main

2

3data Parity : Nat -> Set where

4 even : Parity (n + n)

5− | odd : Parity (S (n + n))

5+ odd : Parity (S (n + n))

6

7parity : (n:Nat) -> Parity n

8parity O = even {n=O}

test/test008/test008.idr+12−16

@@ -4,12 +4,10 @@ testlist : List (String, Int)

4testlist = [("foo", 1), ("bar", 2)]

5

6getVal : String -> a -> List (String, a) -> a

7−getVal x b xs = case lookup x xs of {

7+getVal x b xs = case lookup x xs of

8− Just v => case lookup x xs of {

8+ Just v => case lookup x xs of

9 Just v' => v

10− }

11− | Nothing => b

10+ Nothing => b

12− }

13

11

14foo : (Int, String)

12foo : (Int, String)

15foo = (4, "foo")

13foo = (4, "foo")

@@ -19,15 +17,13 @@ ioVals : IO (String, String)

19ioVals = do { return ("First", "second") }

17ioVals = do { return ("First", "second") }

20

18

21main : IO ()

19main : IO ()

22−main = do { (a, b) <- ioVals

20+main = do (a, b) <- ioVals

23− putStr (show a ++ " and " ++ show b ++ "? ")

21+ putStr (show a ++ " and " ++ show b ++ "? ")

24− let x = "bar"

22+ let x = "bar"

25− putStrLn (show (getVal x 7 testlist))

23+ putStrLn (show (getVal x 7 testlist))

26− let ((y, z) :: _) = testlist

24+ let ((y, z) :: _) = testlist

27− print z

25+ print z

28− case lookup x testlist of {

26+ case lookup x testlist of

29− Just v => putStrLn (show v)

27+ Just v => putStrLn (show v)

30− | Nothing => putStrLn "Not there!"

28+ Nothing => putStrLn "Not there!"

31− }

32− }

33

29

tutorial/examples/binary.idr+4−4

@@ -1,9 +1,9 @@

1module main

2

3data Binary : Nat -> Set where

4− bEnd : Binary O

4+ bEnd : Binary O

5− | bO : Binary n -> Binary (n + n)

5+ bO : Binary n -> Binary (n + n)

6− | bI : Binary n -> Binary (S (n + n))

6+ bI : Binary n -> Binary (S (n + n))

7

8instance Show (Binary n) where

9 show (bO x) = show x ++ "0"

@@ -12,7 +12,7 @@ instance Show (Binary n) where

12

13data Parity : Nat -> Set where

14 even : Parity (n + n)

15− | odd : Parity (S (n + n))

15+ odd : Parity (S (n + n))

16

17parity : (n:Nat) -> Parity n

18parity O = even {n=O}

tutorial/examples/interp.idr+7−7

@@ -11,11 +11,11 @@ using (G : Vect Ty n)

11

12 data Env : Vect Ty n -> Set where

13 Nil : Env Nil

14− | (::) : interpTy a -> Env G -> Env (a :: G)

14+ (::) : interpTy a -> Env G -> Env (a :: G)

15

16 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

17 stop : HasType fO (t :: G) t

18− | pop : HasType k G t -> HasType (fS k) (u :: G) t

18+ pop : HasType k G t -> HasType (fS k) (u :: G) t

19

20 lookup : HasType i G t -> Env G -> interpTy t

21 lookup stop (x :: xs) = x

@@ -23,12 +23,12 @@ using (G : Vect Ty n)

23

24 data Expr : Vect Ty n -> Ty -> Set where

25 Var : HasType i G t -> Expr G t

26− | Val : (x : Int) -> Expr G TyInt

26+ Val : (x : Int) -> Expr G TyInt

27− | Lam : Expr (a :: G) t -> Expr G (TyFun a t)

27+ Lam : Expr (a :: G) t -> Expr G (TyFun a t)

28− | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

28+ App : Expr G (TyFun a t) -> Expr G a -> Expr G t

29− | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

29+ Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

30 Expr G c

31− | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

31+ If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

32

33 interp : Env G -> {static} Expr G t -> interpTy t

34 interp env (Var i) = lookup i env

tutorial/examples/usefultypes.idr+1−1

@@ -16,5 +16,5 @@ list_lookup (S k) (x :: xs) = list_lookup k xs

16lookup_default : Nat -> List a -> a -> a

17lookup_default i xs def = case list_lookup i xs of

18 Nothing => def

19− | Just x => x

19+ Just x => x

20

tutorial/examples/views.idr+1−1

@@ -2,7 +2,7 @@ module views

2

3data Parity : Nat -> Set where

4 even : Parity (n + n)

5− | odd : Parity (S (n + n))

5+ odd : Parity (S (n + n))

6

7parity : (n:Nat) -> Parity n

8parity O = even {n=O}

tutorial/interp.tex+8−8

@@ -62,16 +62,16 @@ constructor in turn.

62

63data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

64 stop : HasType fO (t :: G) t

65− | pop : HasType k G t -> HasType (fS k) (u :: G) t

65+ pop : HasType k G t -> HasType (fS k) (u :: G) t

66

67data Expr : Vect Ty n -> Ty -> Set where

68 Var : HasType i G t -> Expr G t

69− | Val : (x : Int) -> Expr G TyInt

69+ Val : (x : Int) -> Expr G TyInt

70− | Lam : Expr (a :: G) t -> Expr G (TyFun a t)

70+ Lam : Expr (a :: G) t -> Expr G (TyFun a t)

71− | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

71+ App : Expr G (TyFun a t) -> Expr G a -> Expr G t

72− | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

72+ Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

73 Expr G c

74− | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

74+ If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

75

76\end{SaveVerbatim}

77\codefig{exprty}{Expression representation}

@@ -86,7 +86,7 @@ Variables are represented by a proof of their membership in the context,

86

87data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

88 stop : HasType fO (t :: G) t

89− | pop : HasType k G t -> HasType (fS k) (u :: G) t

89+ pop : HasType k G t -> HasType (fS k) (u :: G) t

90

91\end{SaveVerbatim}

92\useverb{hastype}

@@ -180,7 +180,7 @@ is defined in the context, we can then produce a value from the environment:

180

181data Env : Vect Ty n -> Set where

182 Nil : Env Nil

183− | (::) : interpTy a -> Env G -> Env (a :: G)

183+ (::) : interpTy a -> Env G -> Env (a :: G)

184

185lookup : HasType i G t -> Env G -> interpTy t

186lookup stop (x :: xs) = x

tutorial/provisional.tex+3−3

@@ -9,7 +9,7 @@ example, recall the \texttt{parity} function:

9

10data Parity : Nat -> Set where

11 even : Parity (n + n)

12− | odd : Parity (S (n + n))

12+ odd : Parity (S (n + n))

13

14parity : (n:Nat) -> Parity n

15

@@ -220,8 +220,8 @@ case \texttt{Nat}):

220

221data Binary : Nat -> Set where

222 bEnd : Binary O

223− | bO : Binary n -> Binary (n + n)

223+ bO : Binary n -> Binary (n + n)

224− | bI : Binary n -> Binary (S (n + n))

224+ bI : Binary n -> Binary (S (n + n))

225

226\end{SaveVerbatim}

227\useverb{bindef}

tutorial/typesfuns.tex+7−8

@@ -219,10 +219,9 @@ behaviour, the \texttt{a} can be brought into scope as follows:

219\begin{SaveVerbatim}{revwhereb}

220

221rev : List a -> List a

222−rev {a} xs = revAcc [] xs where {

222+rev {a} xs = revAcc [] xs where

223 revAcc : List a -> List a -> List a

224 ...

225−}

226

225

227\end{SaveVerbatim}

226\end{SaveVerbatim}

228\useverb{revwhereb}

227\useverb{revwhereb}

@@ -239,7 +238,7 @@ we declare vectors as follows:

239

238

240data Vect : Set -> Nat -> Set where

239data Vect : Set -> Nat -> Set where

241 Nil : Vect a O

240 Nil : Vect a O

242− | (::) : a -> Vect a k -> Vect a (S k)

241+ (::) : a -> Vect a k -> Vect a (S k)

243

242

244\end{SaveVerbatim}

243\end{SaveVerbatim}

245\useverb{vect}

244\useverb{vect}

@@ -317,7 +316,7 @@ They are declared as follows (again, in the prelude):

317

316

318data Fin : Nat -> Set where

317data Fin : Nat -> Set where

319 fO : Fin (S k)

318 fO : Fin (S k)

320− | fS : Fin k -> Fin (S k)

319+ fS : Fin k -> Fin (S k)

321

320

322\end{SaveVerbatim}

321\end{SaveVerbatim}

323\useverb{findecl}

322\useverb{findecl}

@@ -423,7 +422,7 @@ definition, which defines a predicate on vectors:

423

422

424data Elem : a -> (Vect a n) -> Set where

423data Elem : a -> (Vect a n) -> Set where

425 here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)

424 here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)

426− | there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)

425+ there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)

427

426

428\end{SaveVerbatim}

427\end{SaveVerbatim}

429\useverb{elem}

428\useverb{elem}

@@ -455,7 +454,7 @@ ordering of any implicit arguments which can appear within the block:

455using (x:a, y:a, xs:Vect a n)

454using (x:a, y:a, xs:Vect a n)

456 data Elem : a -> (Vect a n) -> Set where

455 data Elem : a -> (Vect a n) -> Set where

457 here : Elem x (x :: xs)

456 here : Elem x (x :: xs)

458− | there : Elem x xs -> Elem x (y :: xs)

457+ there : Elem x xs -> Elem x (y :: xs)

459

458

460\end{SaveVerbatim}

459\end{SaveVerbatim}

461\useverb{elemusing}

460\useverb{elemusing}

@@ -589,7 +588,7 @@ data List a = Nil | (::) a (List a)

589

588

590data Vect : Set -> Nat -> Set where

589data Vect : Set -> Nat -> Set where

591 Nil : Vect a O

590 Nil : Vect a O

592− | (::) : a -> Vect a k -> Vect a (S k)

591+ (::) : a -> Vect a k -> Vect a (S k)

593

592

594\end{SaveVerbatim}

593\end{SaveVerbatim}

595\useverb{listvec}

594\useverb{listvec}

@@ -954,7 +953,7 @@ looks up an index and returns a default value if the index is out of bounds:

954lookup_default : Nat -> List a -> a -> a

953lookup_default : Nat -> List a -> a -> a

955lookup_default i xs def = case list_lookup i xs of

954lookup_default i xs def = case list_lookup i xs of

956 Nothing => def

955 Nothing => def

957− | Just x => x

956+ Just x => x

958

957

959\end{SaveVerbatim}

958\end{SaveVerbatim}

960\useverb{listlookup}

959\useverb{listlookup}

tutorial/views.tex+1−1

@@ -59,7 +59,7 @@ plus one:

59

60data Parity : Nat -> Set where

61 even : Parity (n + n)

62− | odd : Parity (S (n + n))

62+ odd : Parity (S (n + n))

63

64\end{SaveVerbatim}

65\useverb{parity}