ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 01:25:05 +03:00
Code Issues Projects Releases Wiki Activity

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

Browse Source 
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;
}
This commit is contained in:
Edwin Brady 2012-01-07 16:24:59 +00:00
parent 2852e711cb
commit 8b1e498807
15 changed files with 95 additions and 86 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/prelude/list.idr
View File

@ -45,7 +45,7 @@ mapMaybe : (a -> Maybe b) -> List a -> List b
mapMaybe f [] = []
mapMaybe f (x :: xs) = case f x of
Nothing => mapMaybe f xs
| Just v => v :: mapMaybe f xs
Just v => v :: mapMaybe f xs
filter : (y -> Bool) -> List y -> List y
filter pred [] = []
@ -92,5 +92,5 @@ split : (a -> Bool) -> List a -> List (List a)
split p [] = []
split p xs = case break p xs of
(chunk, []) => [chunk]
| (chunk, (c :: rest)) => chunk :: split p rest
(chunk, (c :: rest)) => chunk :: split p rest

2
lib/prelude/strings.idr
View File

@ -8,7 +8,7 @@ import prelude.char
data StrM : String -> Set where
StrNil : StrM ""
| StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
strHead' : (x : String) -> so (not (x == "")) -> Char
strHead' x p = prim__strHead x

4
lib/prelude/vect.idr
View File

@ -6,7 +6,7 @@ import prelude.nat
data Fin : Nat -> Set where
fO : Fin (S k)
| fS : Fin k -> Fin (S k)
fS : Fin k -> Fin (S k)
instance Eq (Fin n) where
fO == fO = True
@ -17,7 +17,7 @@ infixr 7 ::
data Vect : Set -> Nat -> Set where
Nil : Vect a O
| (::) : a -> Vect a k -> Vect a (S k)
(::) : a -> Vect a k -> Vect a (S k)
lookup : Fin n -> Vect a n -> a
lookup fO (x :: xs) = x

60
src/Idris/Parser.hs
View File

@ -201,13 +201,20 @@ pTerminator = do lchar ';'; pop_indent
else fail "Not a terminator"
<|> lookAhead eof
pBarTerminator
= do lchar '|'; return ()
<|> do c <- indent; l <- last_indent
if (c <= l) then return ()
else fail "Not a terminator"
<|> lookAhead eof
pKeepTerminator
= do lchar ';'; return ()
<|> do c <- indent; l <- last_indent
if (c <= l) then return ()
else fail "Not a terminator"
<|> do i <- getInput; let h = take 1 i
if (h == "}" || h == ")") then return ()
if (h == "}" || h == ")" || h == "|") then return ()
else fail "Not a terminator"
<|> lookAhead eof
@ -255,7 +262,7 @@ parseProg syn fname input pos
return (collect x)
where ishow err = let ln = sourceLine (errorPos err) in
fname ++ ":" ++ show ln ++ ":parse error"
++ " " ++ show (sourceColumn (errorPos err))
++ " at column " ++ show (sourceColumn (errorPos err))
-- show (map messageString (errorMessages err))
-- Collect PClauses with the same function name
@ -605,7 +612,12 @@ pSimpleExpr syn =
return (PTactics ts)
<|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
open_block
opts <- sepBy1 (pCaseOpt syn) (lchar '|')
push_indent
opts <- many1 (do notEndBlock
x <- pCaseOpt syn
pKeepTerminator
return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
pop_indent
close_block
return (PCase fc scr opts)
<|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
@ -883,34 +895,36 @@ accData (Just Frozen) n ns = do addAcc n (Just Frozen)
accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns
pData :: SyntaxInfo -> IParser PDecl
pData syn = try (do push_indent
acc <- pAccessibility
pData syn = try (do acc <- pAccessibility
reserved "data"; fc <- pfc
tyn_in <- pfName; ty <- pTSig syn
let tyn = expandNS syn tyn_in
reserved "where"
-- ty' <- implicit syn tyn ty
cons <- sepBy (pConstructor syn) (lchar '|')
pTerminator
open_block
push_indent
cons <- many (do notEndBlock
c <- pConstructor syn
pKeepTerminator
return c) -- (lchar '|')
pop_indent
close_block
accData acc tyn (map (\ (n, _, _) -> n) cons)
return $ PData syn fc (PDatadecl tyn ty cons))
<|> do push_indent
acc <- pAccessibility
reserved "data"; fc <- pfc
tyn_in <- pfName; args <- many pName
let tyn = expandNS syn tyn_in
lchar '='
cons <- sepBy1 (pSimpleCon syn) (lchar '|')
pTerminator
let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
let ty = bindArgs (map (\a -> PSet) args) PSet
-- ty' <- implicit syn tyn ty
cons' <- mapM (\ (x, cargs, cfc) ->
<|> try (do push_indent
acc <- pAccessibility
reserved "data"; fc <- pfc
tyn_in <- pfName; args <- many pName
let tyn = expandNS syn tyn_in
lchar '='
cons <- sepBy1 (pSimpleCon syn) (lchar '|')
pTerminator
let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
let ty = bindArgs (map (\a -> PSet) args) PSet
cons' <- mapM (\ (x, cargs, cfc) ->
do let cty = bindArgs cargs conty
-- cty' <- implicit syn x cty
return (x, cty, cfc)) cons
accData acc tyn (map (\ (n, _, _) -> n) cons')
return $ PData syn fc (PDatadecl tyn ty cons')
accData acc tyn (map (\ (n, _, _) -> n) cons')
return $ PData syn fc (PDatadecl tyn ty cons'))
where
mkPApp fc t [] = t
mkPApp fc t xs = PApp fc t (map pexp xs)

16
test/test001/test001.idr
View File

@ -11,11 +11,11 @@ using (G : Vect Ty n) {
data Env : Vect Ty n -> Set where
Nil : Env Nil
| (::) : interpTy a -> Env G -> Env (a :: G)
(::) : interpTy a -> Env G -> Env (a :: G)
data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
stop : HasType fO (t :: G) t
| pop : HasType k G t -> HasType (fS k) (u :: G) t
pop : HasType k G t -> HasType (fS k) (u :: G) t
lookup : HasType i G t -> Env G -> interpTy t
lookup stop (x :: xs) = x
@ -23,13 +23,13 @@ using (G : Vect Ty n) {
data Expr : Vect Ty n -> Ty -> Set where
Var : HasType i G t -> Expr G t
| Val : (x : Int) -> Expr G TyInt
| Lam : Expr (a :: G) t -> Expr G (TyFun a t)
| App : Expr G (TyFun a t) -> Expr G a -> Expr G t
| Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
Val : (x : Int) -> Expr G TyInt
Lam : Expr (a :: G) t -> Expr G (TyFun a t)
App : Expr G (TyFun a t) -> Expr G a -> Expr G t
Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
Expr G c
| If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
| Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
interp : Env G -> {static} Expr G t -> interpTy t
interp env (Var i) = lookup i env

2
test/test006/test006.idr
View File

@ -2,7 +2,7 @@ module main
data Parity : Nat -> Set where
even : Parity (n + n)
| odd : Parity (S (n + n))
odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n
parity O = even {n=O}

28
test/test008/test008.idr
View File

@ -4,12 +4,10 @@ testlist : List (String, Int)
testlist = [("foo", 1), ("bar", 2)]
getVal : String -> a -> List (String, a) -> a
getVal x b xs = case lookup x xs of {
Just v => case lookup x xs of {
getVal x b xs = case lookup x xs of
Just v => case lookup x xs of
Just v' => v
}
| Nothing => b
}
Nothing => b
foo : (Int, String)
foo = (4, "foo")
@ -19,15 +17,13 @@ ioVals : IO (String, String)
ioVals = do { return ("First", "second") }
main : IO ()
main = do { (a, b) <- ioVals
putStr (show a ++ " and " ++ show b ++ "? ")
let x = "bar"
putStrLn (show (getVal x 7 testlist))
let ((y, z) :: _) = testlist
print z
case lookup x testlist of {
Just v => putStrLn (show v)
| Nothing => putStrLn "Not there!"
}
}
main = do (a, b) <- ioVals
putStr (show a ++ " and " ++ show b ++ "? ")
let x = "bar"
putStrLn (show (getVal x 7 testlist))
let ((y, z) :: _) = testlist
print z
case lookup x testlist of
Just v => putStrLn (show v)
Nothing => putStrLn "Not there!"

8
tutorial/examples/binary.idr
View File

@ -1,9 +1,9 @@
module main
data Binary : Nat -> Set where
bEnd : Binary O
| bO : Binary n -> Binary (n + n)
| bI : Binary n -> Binary (S (n + n))
bEnd : Binary O
bO : Binary n -> Binary (n + n)
bI : Binary n -> Binary (S (n + n))
instance Show (Binary n) where
show (bO x) = show x ++ "0"
@ -12,7 +12,7 @@ instance Show (Binary n) where
data Parity : Nat -> Set where
even : Parity (n + n)
| odd : Parity (S (n + n))
odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n
parity O = even {n=O}

14
tutorial/examples/interp.idr
View File

@ -11,11 +11,11 @@ using (G : Vect Ty n)
data Env : Vect Ty n -> Set where
Nil : Env Nil
| (::) : interpTy a -> Env G -> Env (a :: G)
(::) : interpTy a -> Env G -> Env (a :: G)
data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
stop : HasType fO (t :: G) t
| pop : HasType k G t -> HasType (fS k) (u :: G) t
pop : HasType k G t -> HasType (fS k) (u :: G) t
lookup : HasType i G t -> Env G -> interpTy t
lookup stop (x :: xs) = x
@ -23,12 +23,12 @@ using (G : Vect Ty n)
data Expr : Vect Ty n -> Ty -> Set where
Var : HasType i G t -> Expr G t
| Val : (x : Int) -> Expr G TyInt
| Lam : Expr (a :: G) t -> Expr G (TyFun a t)
| App : Expr G (TyFun a t) -> Expr G a -> Expr G t
| Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
Val : (x : Int) -> Expr G TyInt
Lam : Expr (a :: G) t -> Expr G (TyFun a t)
App : Expr G (TyFun a t) -> Expr G a -> Expr G t
Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
Expr G c
| If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
interp : Env G -> {static} Expr G t -> interpTy t
interp env (Var i) = lookup i env

2
tutorial/examples/usefultypes.idr
View File

@ -16,5 +16,5 @@ list_lookup (S k) (x :: xs) = list_lookup k xs
lookup_default : Nat -> List a -> a -> a
lookup_default i xs def = case list_lookup i xs of
Nothing => def
| Just x => x
Just x => x

2
tutorial/examples/views.idr
View File

@ -2,7 +2,7 @@ module views
data Parity : Nat -> Set where
even : Parity (n + n)
| odd : Parity (S (n + n))
odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n
parity O = even {n=O}

16
tutorial/interp.tex
View File

@ -62,16 +62,16 @@ constructor in turn.
data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
stop : HasType fO (t :: G) t
| pop : HasType k G t -> HasType (fS k) (u :: G) t
pop : HasType k G t -> HasType (fS k) (u :: G) t
data Expr : Vect Ty n -> Ty -> Set where
Var : HasType i G t -> Expr G t
| Val : (x : Int) -> Expr G TyInt
| Lam : Expr (a :: G) t -> Expr G (TyFun a t)
| App : Expr G (TyFun a t) -> Expr G a -> Expr G t
| Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
Val : (x : Int) -> Expr G TyInt
Lam : Expr (a :: G) t -> Expr G (TyFun a t)
App : Expr G (TyFun a t) -> Expr G a -> Expr G t
Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
Expr G c
| If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
\end{SaveVerbatim}
\codefig{exprty}{Expression representation}
@ -86,7 +86,7 @@ Variables are represented by a proof of their membership in the context,
data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
stop : HasType fO (t :: G) t
| pop : HasType k G t -> HasType (fS k) (u :: G) t
pop : HasType k G t -> HasType (fS k) (u :: G) t
\end{SaveVerbatim}
\useverb{hastype}
@ -180,7 +180,7 @@ is defined in the context, we can then produce a value from the environment:
data Env : Vect Ty n -> Set where
Nil : Env Nil
| (::) : interpTy a -> Env G -> Env (a :: G)
(::) : interpTy a -> Env G -> Env (a :: G)
lookup : HasType i G t -> Env G -> interpTy t
lookup stop (x :: xs) = x

6
tutorial/provisional.tex
View File

@ -9,7 +9,7 @@ example, recall the \texttt{parity} function:
data Parity : Nat -> Set where
even : Parity (n + n)
| odd : Parity (S (n + n))
odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n
@ -220,8 +220,8 @@ case \texttt{Nat}):
data Binary : Nat -> Set where
bEnd : Binary O
| bO : Binary n -> Binary (n + n)
| bI : Binary n -> Binary (S (n + n))
bO : Binary n -> Binary (n + n)
bI : Binary n -> Binary (S (n + n))
\end{SaveVerbatim}
\useverb{bindef}

15
tutorial/typesfuns.tex
View File

@ -219,10 +219,9 @@ behaviour, the \texttt{a} can be brought into scope as follows:
\begin{SaveVerbatim}{revwhereb}
rev : List a -> List a
rev {a} xs = revAcc [] xs where {
rev {a} xs = revAcc [] xs where
revAcc : List a -> List a -> List a
...
}
\end{SaveVerbatim}
\useverb{revwhereb}
@ -239,7 +238,7 @@ we declare vectors as follows:
data Vect : Set -> Nat -> Set where
Nil : Vect a O
| (::) : a -> Vect a k -> Vect a (S k)
(::) : a -> Vect a k -> Vect a (S k)
\end{SaveVerbatim}
\useverb{vect}
@ -317,7 +316,7 @@ They are declared as follows (again, in the prelude):
data Fin : Nat -> Set where
fO : Fin (S k)
| fS : Fin k -> Fin (S k)
fS : Fin k -> Fin (S k)
\end{SaveVerbatim}
\useverb{findecl}
@ -423,7 +422,7 @@ definition, which defines a predicate on vectors:
data Elem : a -> (Vect a n) -> Set where
here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)
| there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)
there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)
\end{SaveVerbatim}
\useverb{elem}
@ -455,7 +454,7 @@ ordering of any implicit arguments which can appear within the block:
using (x:a, y:a, xs:Vect a n)
data Elem : a -> (Vect a n) -> Set where
here : Elem x (x :: xs)
| there : Elem x xs -> Elem x (y :: xs)
there : Elem x xs -> Elem x (y :: xs)
\end{SaveVerbatim}
\useverb{elemusing}
@ -589,7 +588,7 @@ data List a = Nil | (::) a (List a)
data Vect : Set -> Nat -> Set where
Nil : Vect a O
| (::) : a -> Vect a k -> Vect a (S k)
(::) : a -> Vect a k -> Vect a (S k)
\end{SaveVerbatim}
\useverb{listvec}
@ -954,7 +953,7 @@ looks up an index and returns a default value if the index is out of bounds:
lookup_default : Nat -> List a -> a -> a
lookup_default i xs def = case list_lookup i xs of
Nothing => def
| Just x => x
Just x => x
\end{SaveVerbatim}
\useverb{listlookup}

2
tutorial/views.tex
View File

@ -59,7 +59,7 @@ plus one:
data Parity : Nat -> Set where
even : Parity (n + n)
| odd : Parity (S (n + n))
odd : Parity (S (n + n))
\end{SaveVerbatim}
\useverb{parity}