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

git.iko.soy/Idris-dev

Change 'data' and where syntax so that they don't need '|'

This breaks old code - instead of data Foo : T where c1 : Foo T1 | c2 : Foo T2 use data Foo : T where c1 : Foo T1 c2 : Foo T2 For consistency with other syntactic forms, explicit grouping is achieved by data Foo : T where { c1 : Foo T1; c2 : Foo T2; }

commit8b1e498807e144f949eb1917d62cb3bacf938ead authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 7 Jan 2012, 16:24 (15 years ago) parent2852e71

15 files changed+95−86

compare with master

unifiedsplit

lib/prelude/list.idr+2−2 lib/prelude/strings.idr+1−1 lib/prelude/vect.idr+2−2 src/Idris/Parser.hs+37−23 test/test001/test001.idr+8−8 test/test006/test006.idr+1−1 test/test008/test008.idr+12−16 tutorial/examples/binary.idr+4−4 tutorial/examples/interp.idr+7−7 tutorial/examples/usefultypes.idr+1−1 tutorial/examples/views.idr+1−1 tutorial/interp.tex+8−8 tutorial/provisional.tex+3−3 tutorial/typesfuns.tex+7−8 tutorial/views.tex+1−1

lib/prelude/list.idr+2−2

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

4545mapMaybe f [] = []

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

4747 Nothing => mapMaybe f xs

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

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

4949

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

5151filter pred [] = []

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

9292split p [] = []

9393split p xs = case break p xs of

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

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

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

9696

lib/prelude/strings.idr+1−1

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

99data StrM : String -> Set where

1010 StrNil : StrM ""

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

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

1212

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

1414strHead' x p = prim__strHead x

lib/prelude/vect.idr+2−2

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

77data Fin : Nat -> Set where

88 fO : Fin (S k)

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

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

1010

1111instance Eq (Fin n) where

1212 fO == fO = True

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

1717

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

1919 Nil : Vect a O

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

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

2121

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

2323lookup fO (x :: xs) = x

src/Idris/Parser.hs+37−23

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

201201 else fail "Not a terminator"

202202 <|> lookAhead eof

203203

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+

204211pKeepTerminator

205212 = do lchar ';'; return ()

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

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

208215 else fail "Not a terminator"

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

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

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

211218 else fail "Not a terminator"

212219 <|> lookAhead eof

213220

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

255262 return (collect x)

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

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

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

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

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

260267

261268-- Collect PClauses with the same function name

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

605612 return (PTactics ts)

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

607614 open_block

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

615+ push_indent

616+ opts <- many1 (do notEndBlock

617+ x <- pCaseOpt syn

618+ pKeepTerminator

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

620+ pop_indent

609621 close_block

610622 return (PCase fc scr opts)

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

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

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

884896

885897pData :: SyntaxInfo -> IParser PDecl

886−pData syn = try (do push_indent

887− acc <- pAccessibility

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

888899 reserved "data"; fc <- pfc

889900 tyn_in <- pfName; ty <- pTSig syn

890901 let tyn = expandNS syn tyn_in

891902 reserved "where"

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

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

894− pTerminator

903+ open_block

904+ push_indent

905+ cons <- many (do notEndBlock

906+ c <- pConstructor syn

907+ pKeepTerminator

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

909+ pop_indent

910+ close_block

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

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

897− <|> do push_indent

898− acc <- pAccessibility

899− reserved "data"; fc <- pfc

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

901− let tyn = expandNS syn tyn_in

902− lchar '='

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

904− pTerminator

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

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

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

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

913+ <|> try (do push_indent

914+ acc <- pAccessibility

915+ reserved "data"; fc <- pfc

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

917+ let tyn = expandNS syn tyn_in

918+ lchar '='

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

920+ pTerminator

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

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

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

909924 do let cty = bindArgs cargs conty

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

911925 return (x, cty, cfc)) cons

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

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

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

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

914928 where

915929 mkPApp fc t [] = t

916930 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) {

1111

1212 data Env : Vect Ty n -> Set where

1313 Nil : Env Nil

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

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

1515

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

1717 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

1919

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

2121 lookup stop (x :: xs) = x

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

2323

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

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

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

27− | Lam : Expr (a :: G) t -> Expr G (TyFun a 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 ->

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

27+ Lam : Expr (a :: G) t -> Expr G (TyFun a 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 ->

3030 Expr G c

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

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

3333

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

3535 interp env (Var i) = lookup i env

test/test006/test006.idr+1−1

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

33data Parity : Nat -> Set where

44 even : Parity (n + n)

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

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

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

88parity O = even {n=O}

test/test008/test008.idr+12−16

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

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

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

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

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

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

8+ Just v => case lookup x xs of

99 Just v' => v

10− }

11− | Nothing => b

12− }

10+ Nothing => b

1311

1412foo : (Int, String)

1513foo = (4, "foo")

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

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

2018

2119main : IO ()

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

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

24− let x = "bar"

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

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

27− print z

28− case lookup x testlist of {

29− Just v => putStrLn (show v)

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

31− }

32− }

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

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

22+ let x = "bar"

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

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

25+ print z

26+ case lookup x testlist of

27+ Just v => putStrLn (show v)

28+ Nothing => putStrLn "Not there!"

3329

tutorial/examples/binary.idr+4−4

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

11module main

33data Binary : Nat -> Set where

4− bEnd : Binary O

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

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

4+ bEnd : Binary O

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

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

88instance Show (Binary n) where

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

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

1212

1313data Parity : Nat -> Set where

1414 even : Parity (n + n)

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

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

1616

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

1818parity O = even {n=O}

tutorial/examples/interp.idr+7−7

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

1111

1212 data Env : Vect Ty n -> Set where

1313 Nil : Env Nil

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

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

1515

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

1717 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

1919

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

2121 lookup stop (x :: xs) = x

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

2323

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

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

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

27− | Lam : Expr (a :: G) t -> Expr G (TyFun a 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 ->

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

27+ Lam : Expr (a :: G) t -> Expr G (TyFun a 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 ->

3030 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

3232

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

3434 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

1616lookup_default : Nat -> List a -> a -> a

1717lookup_default i xs def = case list_lookup i xs of

1818 Nothing => def

19− | Just x => x

19+ Just x => x

2020

tutorial/examples/views.idr+1−1

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

33data Parity : Nat -> Set where

44 even : Parity (n + n)

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

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

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

88parity O = even {n=O}

tutorial/interp.tex+8−8

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

6262

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

6464 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

6666

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

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

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

70− | Lam : Expr (a :: G) t -> Expr G (TyFun a 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 ->

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

70+ Lam : Expr (a :: G) t -> Expr G (TyFun a 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 ->

7373 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

7575

7676\end{SaveVerbatim}

7777\codefig{exprty}{Expression representation}

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

8686

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

8888 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

9090

9191\end{SaveVerbatim}

9292\useverb{hastype}

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

180180

181181data Env : Vect Ty n -> Set where

182182 Nil : Env Nil

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

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

184184

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

186186lookup stop (x :: xs) = x

tutorial/provisional.tex+3−3

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

1010data Parity : Nat -> Set where

1111 even : Parity (n + n)

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

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

1313

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

1515

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

220220

221221data Binary : Nat -> Set where

222222 bEnd : Binary O

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

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

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

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

225225

226226\end{SaveVerbatim}

227227\useverb{bindef}

tutorial/typesfuns.tex+7−8

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

219219\begin{SaveVerbatim}{revwhereb}

220220

221221rev : List a -> List a

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

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

223223 revAcc : List a -> List a -> List a

224224 ...

225−}

226225

227226\end{SaveVerbatim}

228227\useverb{revwhereb}

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

239238

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

241240 Nil : Vect a O

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

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

243242

244243\end{SaveVerbatim}

245244\useverb{vect}

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

317316

318317data Fin : Nat -> Set where

319318 fO : Fin (S k)

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

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

321320

322321\end{SaveVerbatim}

323322\useverb{findecl}

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

423422

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

425424 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)

427426

428427\end{SaveVerbatim}

429428\useverb{elem}

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

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

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

457456 here : Elem x (x :: xs)

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

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

459458

460459\end{SaveVerbatim}

461460\useverb{elemusing}

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

589588

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

591590 Nil : Vect a O

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

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

593592

594593\end{SaveVerbatim}

595594\useverb{listvec}

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

954953lookup_default : Nat -> List a -> a -> a

955954lookup_default i xs def = case list_lookup i xs of

956955 Nothing => def

957− | Just x => x

956+ Just x => x

958957

959958\end{SaveVerbatim}

960959\useverb{listlookup}

tutorial/views.tex+1−1

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

5959

6060data Parity : Nat -> Set where

6161 even : Parity (n + n)

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

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

6363

6464\end{SaveVerbatim}

6565\useverb{parity}