ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Combine a chunk of regxxx tests

Browse Source 
Now reg001 contains lots of the tests which are only intended to check
whether some code type checks. More to do like this...
This commit is contained in:
Edwin Brady 2015-09-06 14:52:50 +01:00
parent 2f9d287d07
commit 5f47887822
38 changed files with 170 additions and 259 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
idris.cabal
View File

@ -143,36 +143,18 @@ Extra-source-files:
test/reg004/run
test/reg004/*.idr
test/reg004/expected
test/reg005/run
test/reg005/*.idr
test/reg005/expected
test/reg006/run
test/reg006/*.idr
test/reg006/expected
test/reg007/run
test/reg007/*.lidr
test/reg007/expected
test/reg009/run
test/reg009/*.lidr
test/reg009/expected
test/reg010/run
test/reg010/*.idr
test/reg010/expected
test/reg011/run
test/reg011/*.idr
test/reg011/expected
test/reg012/run
test/reg012/*.lidr
test/reg012/expected
test/reg013/run
test/reg013/*.idr
test/reg013/expected
test/reg014/run
test/reg014/*.idr
test/reg014/expected
test/reg015/run
test/reg015/*.idr
test/reg015/expected
test/reg016/run
test/reg016/*.idr
test/reg016/expected
@ -182,18 +164,9 @@ Extra-source-files:
test/reg018/run
test/reg018/*.idr
test/reg018/expected
test/reg019/run
test/reg019/*.idr
test/reg019/expected
test/reg020/run
test/reg020/*.idr
test/reg020/expected
test/reg021/run
test/reg021/*.idr
test/reg021/expected
test/reg022/run
test/reg022/*.idr
test/reg022/expected
test/reg023/run
test/reg023/*.idr
test/reg023/expected
@ -203,9 +176,6 @@ Extra-source-files:
test/reg025/run
test/reg025/*.idr
test/reg025/expected
test/reg026/run
test/reg026/*.idr
test/reg026/expected
test/reg027/run
test/reg027/*.idr
test/reg027/expected
@ -215,18 +185,12 @@ Extra-source-files:
test/reg029/run
test/reg029/*.idr
test/reg029/expected
test/reg030/run
test/reg030/*.idr
test/reg030/expected
test/reg031/run
test/reg031/*.idr
test/reg031/expected
test/reg032/run
test/reg032/*.idr
test/reg032/expected
test/reg033/run
test/reg033/*.idr
test/reg033/expected
test/reg034/run
test/reg034/*.idr
test/reg034/expected

170
test/reg001/reg001.idr
View File

@ -1,3 +1,11 @@
-- Everything here should type check but at some point in the past has
-- not.
import Data.So
import Data.Vect
import Data.Fin
import Control.Isomorphism
class Functor f => VerifiedFunctor (f : Type -> Type) where
identity : (fa : f a) -> map id fa = fa
@ -7,3 +15,165 @@ data Imp : Type where
testVal : Imp
testVal = MkImp (apply id Z)
zfin : Fin 1
zfin = 0
data Infer = MkInf a
foo : Infer
foo = MkInf (the (Fin 1) 0)
isAnyBy : (alpha -> Bool) -> (n : Nat ** Vect n alpha) -> Bool
isAnyBy _ (_ ** Nil) = False
isAnyBy p (_ ** (a :: as)) = p a || isAnyBy p (_ ** as)
filterTagP : (p : alpha -> Bool) ->
(as : Vect n alpha) ->
So (isAnyBy p (n ** as)) ->
(m : Nat ** (Vect m (a : alpha ** So (p a)), So (m > Z)))
filterTagP {n = S m} p (a :: as) q with (p a)
| True = (_
**
((a ** believe_me Oh)
::
(fst (getProof (filterTagP p as (believe_me Oh)))),
Oh
)
)
| False = filterTagP p as (believe_me Oh)
vfoldl : (P : Nat -> Type) ->
((x : Nat) -> P x -> a -> P (S x)) -> P Z
-> Vect m a -> P m
vfoldl P cons nil (x :: xs)
= vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons Z nil x) xs
total soElim : (C : (b : Bool) -> So b -> Type) ->
C True Oh ->
(b : Bool) -> (s : So b) -> (C b s)
soElim C coh True Oh = coh
soFalseElim : So False -> a
soFalseElim x = void (soElim C () False x)
where
C : (b : Bool) -> So b -> Type
C True s = ()
C False s = Void
soTrue : So b -> b = True
soTrue {b = False} x = soFalseElim x
soTrue {b = True} x = Refl
class Eq alpha => ReflEqEq alpha where
reflexive_eqeq : (a : alpha) -> So (a == a)
modifyFun : (Eq alpha) =>
(alpha -> beta) ->
(alpha, beta) ->
(alpha -> beta)
modifyFun f (a, b) a' = if a' == a then b else f a'
modifyFunLemma : (ReflEqEq alpha) =>
(f : alpha -> beta) ->
(ab : (alpha, beta)) ->
modifyFun f ab (fst ab) = snd ab
modifyFunLemma f (a,b) =
rewrite soTrue (reflexive_eqeq a) in Refl
Matrix : Type -> Nat -> Nat -> Type
Matrix a n m = Vect n (Vect m a)
mytranspose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)
mytranspose ((x:: []) :: []) = [[x]]
mytranspose [x :: y :: xs] = [x] :: (mytranspose [y :: xs])
mytranspose (x :: y :: xs)
= let tx = mytranspose [x] in
let ux = mytranspose (y :: xs) in zipWith (++) tx ux
using (A : Type, B : A->Type, C : Type)
foo2 : ((x:A) -> B x -> C) -> ((x:A ** B x) -> C)
foo2 f p = f (getWitness p) (getProof p)
m_add : Maybe (Either Bool Int) -> Maybe (Either Bool Int) ->
Maybe (Either Bool Int)
m_add x y = do x' <- x -- Extract value from x
y' <- y -- Extract value from y
case x' of
Left _ => Nothing
Right _ => Nothing
data Ty = TyBool
data Id a = I a
interpTy : Ty -> Type
interpTy TyBool = Id Bool
data Term : Ty -> Type where
TLit : Bool -> Term TyBool
TNot : Term TyBool -> Term TyBool
map : (a -> b) -> Id a -> Id b
map f (I x) = I (f x)
interp : Term t -> interpTy t
interp (TLit x) = I x
interp (TNot x) = map not (interp x)
data Result str a = Success str a | Failure String
instance Functor (Result str) where
map f (Success s x) = Success s (f x)
map f (Failure e ) = Failure e
ParserT : (Type -> Type) -> Type -> Type -> Type
ParserT m str a = str -> m (Result str a)
ap : Monad m => ParserT m str (a -> b) -> ParserT m str a ->
ParserT m str b
ap f x = \s => do f' <- f s
case f' of
Failure e => (pure (Failure e))
Success s' g => x s' >>= pure . map g
X : Nat -> Type
X t = (c : Nat ** So (c < 5))
column : X t -> Nat
column = getWitness
data Action = Left | Ahead | Right
admissible : X t -> Action -> Bool
admissible {t} x Ahead = column {t} x == 0 || column {t} x == 4
admissible {t} x Left = column {t} x <= 2
admissible {t} x Right = column {t} x >= 2
class Set univ where
member : univ -> univ -> Type
isSubsetOf : Set univ => univ -> univ -> Type
isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)
class Set univ => HasPower univ where
Powerset : (a : univ) ->
Sigma univ (\Pa => (c : univ) ->
(isSubsetOf c a) -> member c Pa)
powerset : HasPower univ => univ -> univ
powerset {univ} a = getWitness (Powerset a)
mapFilter : (alpha -> beta) ->
(alpha -> Bool) ->
Vect n alpha ->
(n : Nat ** Vect n beta)
mapFilter f p Nil = (_ ** Nil)
mapFilter f p (a :: as) with (p a)
| True = (_ ** (f a) :: (getProof (mapFilter f p as)))
| False = mapFilter f p as

0
test/reg005/expected
View File

12
test/reg005/reg005.idr
View File

@ -1,12 +0,0 @@
module reg032
import Data.Fin
zfin : Fin 1
zfin = 0
data Infer = MkInf a
foo : Infer
foo = MkInf (the (Fin 1) 0)

3
test/reg005/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg005.idr --check
rm -f *.ibc

0
test/reg009/expected
View File

21
test/reg009/reg009.lidr
View File

@ -1,21 +0,0 @@
> import Data.So
> import Data.Vect
> isAnyBy : (alpha -> Bool) -> (n : Nat ** Vect n alpha) -> Bool
> isAnyBy _ (_ ** Nil) = False
> isAnyBy p (_ ** (a :: as)) = p a || isAnyBy p (_ ** as)
> filterTagP : (p : alpha -> Bool) ->
> (as : Vect n alpha) ->
> So (isAnyBy p (n ** as)) ->
> (m : Nat ** (Vect m (a : alpha ** So (p a)), So (m > Z)))
> filterTagP {n = S m} p (a :: as) q with (p a)
> | True = (_
> **
> ((a ** believe_me Oh)
> ::
> (fst (getProof (filterTagP p as (believe_me Oh)))),
> Oh
> )
> )
> | False = filterTagP p as (believe_me Oh)

3
test/reg009/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg009.lidr --check
rm -f reg009 *.ibc

0
test/reg011/expected
View File

11
test/reg011/reg011.idr
View File

@ -1,11 +0,0 @@
import Data.Vect
vfoldl : (P : Nat -> Type) ->
((x : Nat) -> P x -> a -> P (S x)) -> P Z
-> Vect m a -> P m
-- vfoldl P cons nil []
-- = nil
vfoldl P cons nil (x :: xs)
= vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons Z nil x) xs
-- vfoldl P cons nil (x :: xs)
-- = vfoldl (\n => P (S n)) (\ n => cons _) (cons _ nil x) xs

3
test/reg011/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg011.idr --check
rm -f *.ibc

0
test/reg012/expected
View File

36
test/reg012/reg012.lidr
View File

@ -1,36 +0,0 @@
> import Data.So
> total soElim : (C : (b : Bool) -> So b -> Type) ->
> C True Oh ->
> (b : Bool) -> (s : So b) -> (C b s)
> soElim C coh True Oh = coh
> soFalseElim : So False -> a
> soFalseElim x = void (soElim C () False x)
> where
> C : (b : Bool) -> So b -> Type
> C True s = ()
> C False s = Void
> soTrue : So b -> b = True
> soTrue {b = False} x = soFalseElim x
> soTrue {b = True} x = Refl
> class Eq alpha => ReflEqEq alpha where
> reflexive_eqeq : (a : alpha) -> So (a == a)
> modifyFun : (Eq alpha) =>
> (alpha -> beta) ->
> (alpha, beta) ->
> (alpha -> beta)
> modifyFun f (a, b) a' = if a' == a then b else f a'
> modifyFunLemma : (ReflEqEq alpha) =>
> (f : alpha -> beta) ->
> (ab : (alpha, beta)) ->
> modifyFun f ab (fst ab) = snd ab
> modifyFunLemma f (a,b) =
> rewrite soTrue (reflexive_eqeq a) in Refl
replace {P = \ z => ifThenElse (a == a) b (f a) = ifThenElse z b (f a)}
(soTrue (reflexive_eqeq a)) Refl

3
test/reg012/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg012.lidr --check
rm -f *.ibc

0
test/reg014/expected
View File

14
test/reg014/reg014.idr
View File

@ -1,14 +0,0 @@
module reg014
import Data.Vect
Matrix : Type -> Nat -> Nat -> Type
Matrix a n m = Vect n (Vect m a)
mytranspose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)
mytranspose ((x:: []) :: []) = [[x]]
mytranspose [x :: y :: xs] = [x] :: (mytranspose [y :: xs])
mytranspose (x :: y :: xs)
= let tx = mytranspose [x] in
let ux = mytranspose (y :: xs) in zipWith (++) tx ux

3
test/reg014/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg014.idr --check
rm -f *.ibc

0
test/reg015/expected
View File

3
test/reg015/reg015.idr
View File

@ -1,3 +0,0 @@
using (A : Type, B : A->Type, C : Type)
foo : ((x:A) -> B x -> C) -> ((x:A ** B x) -> C)
foo f p = f (getWitness p) (getProof p)

3
test/reg015/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg015.idr --check
rm -f *.ibc

0
test/reg019/expected
View File

7
test/reg019/reg019.idr
View File

@ -1,7 +0,0 @@
m_add : Maybe (Either Bool Int) -> Maybe (Either Bool Int) ->
Maybe (Either Bool Int)
m_add x y = do x' <- x -- Extract value from x
y' <- y -- Extract value from y
case x' of
Left _ => Nothing
Right _ => Nothing

3
test/reg019/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg019.idr --check
rm -f *.ibc

0
test/reg021/expected
View File

22
test/reg021/reg021.idr
View File

@ -1,22 +0,0 @@
module Main
%default total
data Ty = TyBool
data Id a = I a
interpTy : Ty -> Type
interpTy TyBool = Id Bool
data Term : Ty -> Type where
TLit : Bool -> Term TyBool
TNot : Term TyBool -> Term TyBool
map : (a -> b) -> Id a -> Id b
map f (I x) = I (f x)
interp : Term t -> interpTy t
interp (TLit x) = I x
interp (TNot x) = map not (interp x)

3
test/reg021/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg021.idr --check
rm -f *.ibc

0
test/reg022/expected
View File

18
test/reg022/reg022.idr
View File

@ -1,18 +0,0 @@
module reg022
data Result str a = Success str a | Failure String
instance Functor (Result str) where
map f (Success s x) = Success s (f x)
map f (Failure e ) = Failure e
ParserT : (Type -> Type) -> Type -> Type -> Type
ParserT m str a = str -> m (Result str a)
ap : Monad m => ParserT m str (a -> b) -> ParserT m str a ->
ParserT m str b
ap f x = \s => do f' <- f s
case f' of
Failure e => (pure (Failure e))
Success s' g => x s' >>= pure . map g

3
test/reg022/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg022.idr --check
rm -f *.ibc

0
test/reg026/expected
View File

16
test/reg026/reg026.idr
View File

@ -1,16 +0,0 @@
module Test
import Data.So
X : Nat -> Type
X t = (c : Nat ** So (c < 5))
column : X t -> Nat
column = getWitness
data Action = Left | Ahead | Right
admissible : X t -> Action -> Bool
admissible {t} x Ahead = column {t} x == 0 || column {t} x == 4
admissible {t} x Left = column {t} x <= 2
admissible {t} x Right = column {t} x >= 2

3
test/reg026/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg026.idr --check reg026
rm -f *.ibc

0
test/reg030/expected
View File

15
test/reg030/reg030.idr
View File

@ -1,15 +0,0 @@
import Control.Isomorphism
class Set univ where
member : univ -> univ -> Type
isSubsetOf : Set univ => univ -> univ -> Type
isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)
class Set univ => HasPower univ where
Powerset : (a : univ) ->
Sigma univ (\Pa => (c : univ) ->
(isSubsetOf c a) -> member c Pa)
powerset : HasPower univ => univ -> univ
powerset {univ} a = getWitness (Powerset a)

3
test/reg030/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg030.idr --check
rm -f *.ibc

0
test/reg033/expected
View File

12
test/reg033/reg033.idr
View File

@ -1,12 +0,0 @@
import Data.Vect
mapFilter : (alpha -> beta) ->
(alpha -> Bool) ->
Vect n alpha ->
(n : Nat ** Vect n beta)
mapFilter f p Nil = (_ ** Nil)
mapFilter f p (a :: as) with (p a)
| True = (_ ** (f a) :: (getProof (mapFilter f p as)))
| False = mapFilter f p as

3
test/reg033/run
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg033.idr --check
rm -f reg033 *.ibc