mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-20 09:48:38 +03:00
Remove some tests which are no longer useful
These are ttimp tests that are now subsumed by idris2 tests, and we'd need to implement some ttimp source that isn't really worth it at this stage.
This commit is contained in:
parent
a972778eab
commit
63f0dae035
@ -24,11 +24,8 @@ ttimpTests
|
|||||||
"nest001", "nest002",
|
"nest001", "nest002",
|
||||||
"perf001", "perf002", "perf003",
|
"perf001", "perf002", "perf003",
|
||||||
"record001", "record002", "record003",
|
"record001", "record002", "record003",
|
||||||
"rewrite001",
|
|
||||||
"qtt001", "qtt002", "qtt003",
|
"qtt001", "qtt002", "qtt003",
|
||||||
"search001", "search002", "search003", "search004", "search005",
|
"total001", "total002", "total003"]
|
||||||
"total001", "total002", "total003",
|
|
||||||
"with001"]
|
|
||||||
|
|
||||||
idrisTests : List String
|
idrisTests : List String
|
||||||
idrisTests
|
idrisTests
|
||||||
|
@ -1,37 +0,0 @@
|
|||||||
data Nat : Type where
|
|
||||||
Z : Nat
|
|
||||||
S : Nat -> Nat
|
|
||||||
|
|
||||||
plus : Nat -> Nat -> Nat
|
|
||||||
plus Z y = y
|
|
||||||
plus (S k) y = S (plus k y)
|
|
||||||
|
|
||||||
data Eq : a -> b -> Type where
|
|
||||||
Refl : Eq x x
|
|
||||||
|
|
||||||
rewrite__impl : {0 x, y : a} -> (0 p : _) ->
|
|
||||||
(0 rule : Eq x y) -> (1 val : p y) -> p x
|
|
||||||
rewrite__impl p Refl prf = prf
|
|
||||||
|
|
||||||
%rewrite Eq rewrite__impl
|
|
||||||
|
|
||||||
plusnZ : (n : Nat) -> Eq (plus n Z) n
|
|
||||||
plusnZ Z = Refl
|
|
||||||
plusnZ (S k) = rewrite plusnZ k in Refl
|
|
||||||
|
|
||||||
plusnSm : (n : Nat) -> (m : Nat) ->
|
|
||||||
Eq (S (plus n m)) (plus n (S m))
|
|
||||||
plusnSm Z m = Refl
|
|
||||||
plusnSm (S k) m
|
|
||||||
= let ih = plusnSm k m in
|
|
||||||
rewrite ih in Refl
|
|
||||||
|
|
||||||
plusComm : (n : Nat) -> (m : Nat) -> Eq (plus n m) (plus m n)
|
|
||||||
plusComm Z m = rewrite plusnZ m in Refl
|
|
||||||
plusComm (S k) m =
|
|
||||||
let ih = plusComm k m in
|
|
||||||
rewrite ih in
|
|
||||||
rewrite plusnSm m k in Refl
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -1,3 +0,0 @@
|
|||||||
Processing as TTImp
|
|
||||||
Written TTC
|
|
||||||
Yaffle> Bye for now!
|
|
@ -1 +0,0 @@
|
|||||||
:q
|
|
@ -1,3 +0,0 @@
|
|||||||
$1 --yaffle Rewrite.yaff < input
|
|
||||||
|
|
||||||
rm -rf build
|
|
@ -1,47 +0,0 @@
|
|||||||
data Nat : Type where
|
|
||||||
Z : Nat
|
|
||||||
S : Nat -> Nat
|
|
||||||
|
|
||||||
data List : Type -> Type where
|
|
||||||
Nil : List $a
|
|
||||||
Cons : $a -> List $a -> List $a
|
|
||||||
|
|
||||||
data Elem : $a -> List $a -> Type where
|
|
||||||
Here : Elem $x (Cons $x $xs)
|
|
||||||
There : Elem $x $xs -> Elem $x (Cons $y $xs)
|
|
||||||
|
|
||||||
data Pair : Type -> Type -> Type where
|
|
||||||
MkPair : $a -> $b -> Pair $a $b
|
|
||||||
|
|
||||||
fst : {0 a, b : _} -> Pair a b -> a
|
|
||||||
fst (MkPair $x _) = x
|
|
||||||
|
|
||||||
snd : {0 a, b : _} -> Pair a b -> b
|
|
||||||
snd (MkPair _ $y) = y
|
|
||||||
|
|
||||||
%pair Pair fst snd
|
|
||||||
|
|
||||||
isThere : Elem Z (Cons (S Z) (Cons Z Nil))
|
|
||||||
isThere = %search
|
|
||||||
|
|
||||||
isThere2 : Elem (S Z) (Cons (S Z) (Cons Z Nil))
|
|
||||||
isThere2 = %search
|
|
||||||
|
|
||||||
isThere3 : Elem (S (S Z)) (Cons (S Z) (Cons Z Nil))
|
|
||||||
-- isThere3 = %search
|
|
||||||
|
|
||||||
fn : $a -> $b -> $a
|
|
||||||
fn = %search
|
|
||||||
|
|
||||||
app : ($a -> $b) -> $a -> $b
|
|
||||||
app = %search
|
|
||||||
|
|
||||||
test : $a -> Pair (Integer -> $a) Integer
|
|
||||||
test $y = MkPair (\x => y) 42
|
|
||||||
|
|
||||||
foo : Pair (Integer -> $a) (Pair $c $b) -> Integer -> Pair $b $a
|
|
||||||
foo = %search
|
|
||||||
|
|
||||||
bar : Pair (Int -> $a) (Pair $c $b) -> Int -> Pair $b Char
|
|
||||||
|
|
||||||
|
|
@ -1,6 +0,0 @@
|
|||||||
Processing as TTImp
|
|
||||||
Written TTC
|
|
||||||
Yaffle> (((((Main.There [Just {a:19} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:11} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
|
|
||||||
Yaffle> (((Main.Here [Just {a:11} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
|
|
||||||
Yaffle> ((((Main.MkPair [Just b = Integer]) [Just a = String]) "b") 94)
|
|
||||||
Yaffle> Bye for now!
|
|
@ -1,4 +0,0 @@
|
|||||||
isThere
|
|
||||||
isThere2
|
|
||||||
foo (MkPair (\x => x) (MkPair 'a' "b")) 94
|
|
||||||
:q
|
|
@ -1,3 +0,0 @@
|
|||||||
$1 --yaffle Auto.yaff < input
|
|
||||||
|
|
||||||
rm -rf build
|
|
@ -1,32 +0,0 @@
|
|||||||
data Nat : Type where
|
|
||||||
Z : Nat
|
|
||||||
S : Nat -> Nat
|
|
||||||
|
|
||||||
data List : Type -> Type where
|
|
||||||
Nil : List $a
|
|
||||||
Cons : $a -> List $a -> List $a
|
|
||||||
|
|
||||||
data Pair : Type -> Type -> Type where
|
|
||||||
MkPair : $a -> $b -> Pair $a $b
|
|
||||||
|
|
||||||
data Elem : $a -> List (Pair $a $b) -> Type where
|
|
||||||
Here : Elem $x (Cons (MkPair $x $y) $xs)
|
|
||||||
There : Elem $x $xs -> Elem $x (Cons $y $xs)
|
|
||||||
|
|
||||||
fst : {0 a, b : _} -> Pair a b -> a
|
|
||||||
fst (MkPair $x _) = x
|
|
||||||
|
|
||||||
snd : {0 a, b : _} -> Pair a b -> b
|
|
||||||
snd (MkPair _ $y) = y
|
|
||||||
|
|
||||||
%pair Pair fst snd
|
|
||||||
|
|
||||||
getNth : (x : $a) -> (xs : List (Pair $a $b)) -> Elem x xs -> $b
|
|
||||||
getNth $x (Cons (MkPair $x $y) $xs) Here = y
|
|
||||||
getNth $x (Cons _ $xs) (There $p) = getNth x xs p
|
|
||||||
|
|
||||||
getNth' : (x : $a) -> (xs : List (Pair $a $b)) ->
|
|
||||||
{auto prf : Elem x xs} -> $b
|
|
||||||
getNth' $x $xs {prf = $prf} = getNth x xs prf
|
|
||||||
|
|
||||||
|
|
@ -1,10 +0,0 @@
|
|||||||
Processing as TTImp
|
|
||||||
Written TTC
|
|
||||||
Yaffle> 94
|
|
||||||
Yaffle> 94
|
|
||||||
Yaffle> Bye for now!
|
|
||||||
Processing as TTC
|
|
||||||
Read TTC
|
|
||||||
Yaffle> 94
|
|
||||||
Yaffle> 94
|
|
||||||
Yaffle> Bye for now!
|
|
@ -1,3 +0,0 @@
|
|||||||
getNth "x" (Cons (MkPair "y" 42) (Cons (MkPair "x" 94) Nil)) %search
|
|
||||||
getNth' "x" (Cons (MkPair "y" 42) (Cons (MkPair "x" 94) Nil))
|
|
||||||
:q
|
|
@ -1,4 +0,0 @@
|
|||||||
$1 --yaffle Auto.yaff < input
|
|
||||||
$1 --yaffle build/ttc/Auto.ttc < input
|
|
||||||
|
|
||||||
rm -rf build
|
|
@ -1,133 +0,0 @@
|
|||||||
data Bool : Type where
|
|
||||||
False : Bool
|
|
||||||
True : Bool
|
|
||||||
|
|
||||||
not : Bool -> Bool
|
|
||||||
not False = True
|
|
||||||
not True = False
|
|
||||||
|
|
||||||
data Nat : Type where
|
|
||||||
Z : Nat
|
|
||||||
S : Nat -> Nat
|
|
||||||
|
|
||||||
data List : Type -> Type where
|
|
||||||
Nil : List $a
|
|
||||||
Cons : $a -> List $a -> List $a
|
|
||||||
|
|
||||||
data Maybe : Type -> Type where
|
|
||||||
Nothing : Maybe $a
|
|
||||||
Just : $a -> Maybe $a
|
|
||||||
|
|
||||||
data Pair : Type -> Type -> Type where
|
|
||||||
MkPair : $a -> $b -> Pair $a $b
|
|
||||||
|
|
||||||
fst : {0 a, b : _} -> Pair a b -> a
|
|
||||||
fst (MkPair $x _) = x
|
|
||||||
|
|
||||||
snd : {0 a, b : _} -> Pair a b -> b
|
|
||||||
snd (MkPair _ $y) = y
|
|
||||||
|
|
||||||
%pair Pair fst snd
|
|
||||||
|
|
||||||
data Show : (a : Type) -> Type where
|
|
||||||
[noHints, search a]
|
|
||||||
MkShow : (showFn : $a -> String) -> Show $a
|
|
||||||
|
|
||||||
show : {auto c : Show $a} -> $a -> String
|
|
||||||
show {c = MkShow $show'} $x = show' x
|
|
||||||
|
|
||||||
showNat : Nat -> String
|
|
||||||
showNat Z = "Z"
|
|
||||||
showNat (S $k) = "s" -- (showNat k)
|
|
||||||
|
|
||||||
%hint
|
|
||||||
ShowNat : Show Nat
|
|
||||||
ShowNat = MkShow showNat
|
|
||||||
|
|
||||||
%hint
|
|
||||||
ShowBool : Show Bool
|
|
||||||
ShowBool = MkShow (\b : Bool => case b of
|
|
||||||
True => "True"
|
|
||||||
False => "False")
|
|
||||||
|
|
||||||
data Eq : (a : Type) -> Type where
|
|
||||||
[noHints, search a]
|
|
||||||
MkEq : (eq : $a -> $a -> Bool) -> (neq : $a -> $a -> Bool) -> Eq $a
|
|
||||||
|
|
||||||
-- Signatures
|
|
||||||
eq : {auto c : Eq $a} -> $a -> $a -> Bool
|
|
||||||
neq : {auto c : Eq $a} -> $a -> $a -> Bool
|
|
||||||
|
|
||||||
-- Top level method bodies
|
|
||||||
eq {c = MkEq $eq' $neq'} $x $y = eq' x y
|
|
||||||
neq {c = MkEq $eq' $neq'} $x $y = neq' x y
|
|
||||||
|
|
||||||
-- Default definitions
|
|
||||||
defaultEq : {auto c : Eq $a} -> $a -> $a -> Bool
|
|
||||||
defaultEq $x $y = not (neq x y)
|
|
||||||
|
|
||||||
defaultNotEq : {auto c : Eq $a} -> $a -> $a -> Bool
|
|
||||||
defaultNotEq $x $y = not (eq x y)
|
|
||||||
|
|
||||||
-- e.g. Nat
|
|
||||||
|
|
||||||
-- Instance type
|
|
||||||
%hint
|
|
||||||
EqNat : Eq Nat
|
|
||||||
|
|
||||||
-- Method bodies
|
|
||||||
|
|
||||||
eqNat : Nat -> Nat -> Bool
|
|
||||||
eqNat Z Z = True
|
|
||||||
eqNat (S $j) (S $k) = eq j k
|
|
||||||
eqNat _ _ = False
|
|
||||||
|
|
||||||
-- Rest of instance
|
|
||||||
EqNat = MkEq eqNat (\x, y => not (eqNat x y))
|
|
||||||
|
|
||||||
%hint
|
|
||||||
EqMaybe : {auto c : Eq $a} -> Eq (Maybe $a)
|
|
||||||
|
|
||||||
eqMaybe : {auto c : Eq $a} -> Maybe $a -> Maybe $a -> Bool
|
|
||||||
eqMaybe Nothing Nothing = True
|
|
||||||
eqMaybe (Just $x) (Just $y) = eq x y
|
|
||||||
eqMaybe _ _ = False
|
|
||||||
|
|
||||||
EqMaybe = MkEq eqMaybe (\x, y => not (eqMaybe x y))
|
|
||||||
|
|
||||||
public export
|
|
||||||
data Compare : Type where
|
|
||||||
LT : Compare
|
|
||||||
EQ : Compare
|
|
||||||
GT : Compare
|
|
||||||
|
|
||||||
public export
|
|
||||||
data Ord : (a : Type) -> Type where
|
|
||||||
MkOrd : {auto eqc : Eq $a} ->
|
|
||||||
(cmp : $a -> $a -> Compare) -> Ord $a
|
|
||||||
|
|
||||||
%chaser
|
|
||||||
findEq : Ord $a -> Eq $a
|
|
||||||
findEq (MkOrd _) = %search
|
|
||||||
|
|
||||||
cmp : {auto c : Ord $a} -> $a -> $a -> Compare
|
|
||||||
cmp {c = MkOrd $cmp'} $x $y = cmp' x y
|
|
||||||
|
|
||||||
cmpNat : Nat -> Nat -> Compare
|
|
||||||
cmpNat Z Z = EQ
|
|
||||||
cmpNat Z (S $k) = LT
|
|
||||||
cmpNat (S $k) Z = GT
|
|
||||||
cmpNat (S $x) (S $y) = cmpNat x y
|
|
||||||
|
|
||||||
%hint
|
|
||||||
ordNat : Ord Nat
|
|
||||||
ordNat = MkOrd cmpNat
|
|
||||||
|
|
||||||
testEq : {auto c : Ord $a} -> $a -> $a -> Bool
|
|
||||||
testEq $x $y = eq x y
|
|
||||||
|
|
||||||
testThings : {auto c : Pair (Show $a) (Ord $a)} -> $a -> $a ->
|
|
||||||
Pair String Bool
|
|
||||||
testThings $x $y = MkPair (show x) (eq x y)
|
|
||||||
|
|
||||||
|
|
@ -1,12 +0,0 @@
|
|||||||
Processing as TTImp
|
|
||||||
Written TTC
|
|
||||||
Yaffle> Main.True
|
|
||||||
Yaffle> "True"
|
|
||||||
Yaffle> ((((Main.MkPair [Just b = Main.Bool]) [Just a = String]) "Z") Main.False)
|
|
||||||
Yaffle> Bye for now!
|
|
||||||
Processing as TTC
|
|
||||||
Read TTC
|
|
||||||
Yaffle> Main.True
|
|
||||||
Yaffle> "True"
|
|
||||||
Yaffle> ((((Main.MkPair [Just b = Main.Bool]) [Just a = String]) "Z") Main.False)
|
|
||||||
Yaffle> Bye for now!
|
|
@ -1,4 +0,0 @@
|
|||||||
eq (S (S Z)) (S (S Z))
|
|
||||||
show True
|
|
||||||
testThings Z (S (S (S Z)))
|
|
||||||
:q
|
|
@ -1,4 +0,0 @@
|
|||||||
$1 --yaffle FakeTC.yaff < input
|
|
||||||
$1 --yaffle build/ttc/FakeTC.ttc < input
|
|
||||||
|
|
||||||
rm -rf build
|
|
@ -1,76 +0,0 @@
|
|||||||
data Bool : Type where
|
|
||||||
False : Bool
|
|
||||||
True : Bool
|
|
||||||
|
|
||||||
not : Bool -> Bool
|
|
||||||
not False = True
|
|
||||||
not True = False
|
|
||||||
|
|
||||||
data Nat : Type where
|
|
||||||
Z : Nat
|
|
||||||
S : Nat -> Nat
|
|
||||||
|
|
||||||
plus : Nat -> Nat -> Nat
|
|
||||||
plus Z $y = y
|
|
||||||
plus (S $k) $y = S (plus k y)
|
|
||||||
|
|
||||||
data List : Type -> Type where
|
|
||||||
Nil : List $a
|
|
||||||
Cons : $a -> List $a -> List $a
|
|
||||||
|
|
||||||
data Maybe : Type -> Type where
|
|
||||||
Nothing : Maybe $a
|
|
||||||
Just : $a -> Maybe $a
|
|
||||||
|
|
||||||
data Pair : Type -> Type -> Type where
|
|
||||||
MkPair : $a -> $b -> Pair $a $b
|
|
||||||
|
|
||||||
fst : {0 a, b : _} -> Pair a b -> a
|
|
||||||
fst (MkPair $x _) = x
|
|
||||||
|
|
||||||
snd : {0 a, b : _} -> Pair a b -> b
|
|
||||||
snd (MkPair _ $y) = y
|
|
||||||
|
|
||||||
%pair Pair fst snd
|
|
||||||
|
|
||||||
data Functor : (f : ?) -> Type where
|
|
||||||
[noHints, search f]
|
|
||||||
MkFunctor : (map : {0 a, b: Type} -> (a -> b) -> $f a -> $f b) ->
|
|
||||||
Functor $f
|
|
||||||
|
|
||||||
map : {auto c : Functor $f} -> ($a -> $b) -> $f $a -> $f $b
|
|
||||||
map {c = MkFunctor $map_meth} = map_meth
|
|
||||||
|
|
||||||
%hint
|
|
||||||
ListFunctor : Functor List
|
|
||||||
|
|
||||||
mapList : ($a -> $b) -> List $a -> List $b
|
|
||||||
mapList $f Nil = Nil
|
|
||||||
mapList $f (Cons $x $xs) = Cons (f x) (map f xs)
|
|
||||||
|
|
||||||
ListFunctor = MkFunctor mapList
|
|
||||||
|
|
||||||
namespace Vect
|
|
||||||
public export
|
|
||||||
data Vect : ? -> Type -> Type where
|
|
||||||
Nil : Vect Z $a
|
|
||||||
Cons : $a -> Vect $k $a -> Vect (S $k) $a
|
|
||||||
|
|
||||||
%hint
|
|
||||||
public export
|
|
||||||
VectFunctor : Functor (Vect $n)
|
|
||||||
|
|
||||||
public export
|
|
||||||
mapVect : ($a -> $b) -> Vect $n $a -> Vect $n $b
|
|
||||||
mapVect $f Nil = Nil
|
|
||||||
mapVect $f (Cons $x $xs) = Cons (f x) (map f xs)
|
|
||||||
|
|
||||||
VectFunctor = MkFunctor mapVect
|
|
||||||
|
|
||||||
tryMap : Nat -> Nat -> List Nat
|
|
||||||
tryMap $x $y = map (plus x) (Cons y (Cons (S y) Nil))
|
|
||||||
|
|
||||||
tryVMap : Nat -> Nat -> Vect (S (S Z)) Nat
|
|
||||||
tryVMap $x $y = map (plus x) (Cons y (Cons (S y) Nil))
|
|
||||||
|
|
||||||
|
|
@ -1,10 +0,0 @@
|
|||||||
Processing as TTImp
|
|
||||||
Written TTC
|
|
||||||
Yaffle> (((Main.Cons [Just a = Main.Nat]) (Main.S (Main.S (Main.S Main.Z)))) (((Main.Cons [Just a = Main.Nat]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) (Main.Nil [Just a = Main.Nat])))
|
|
||||||
Yaffle> ((((Main.Vect.Cons [Just k = (Main.S Main.Z)]) [Just a = Main.Nat]) (Main.S (Main.S (Main.S Main.Z)))) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Main.Nat]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) (Main.Vect.Nil [Just a = Main.Nat])))
|
|
||||||
Yaffle> Bye for now!
|
|
||||||
Processing as TTC
|
|
||||||
Read TTC
|
|
||||||
Yaffle> (((Main.Cons [Just a = Main.Nat]) (Main.S (Main.S (Main.S Main.Z)))) (((Main.Cons [Just a = Main.Nat]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) (Main.Nil [Just a = Main.Nat])))
|
|
||||||
Yaffle> ((((Main.Vect.Cons [Just k = (Main.S Main.Z)]) [Just a = Main.Nat]) (Main.S (Main.S (Main.S Main.Z)))) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Main.Nat]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) (Main.Vect.Nil [Just a = Main.Nat])))
|
|
||||||
Yaffle> Bye for now!
|
|
@ -1,3 +0,0 @@
|
|||||||
tryMap (S Z) (S (S Z))
|
|
||||||
tryVMap (S Z) (S (S Z))
|
|
||||||
:q
|
|
@ -1,4 +0,0 @@
|
|||||||
$1 --yaffle Functor.yaff < input
|
|
||||||
$1 --yaffle build/ttc/Functor.ttc < input
|
|
||||||
|
|
||||||
rm -rf build
|
|
@ -1,33 +0,0 @@
|
|||||||
data Bool : Type where
|
|
||||||
False : Bool
|
|
||||||
True : Bool
|
|
||||||
|
|
||||||
not : Bool -> Bool
|
|
||||||
not False = True
|
|
||||||
not True = False
|
|
||||||
|
|
||||||
data Nat : Type where
|
|
||||||
Z : Nat
|
|
||||||
S : Nat -> Nat
|
|
||||||
|
|
||||||
plus : Nat -> Nat -> Nat
|
|
||||||
plus Z y = y
|
|
||||||
plus (S k) y = S (plus k y)
|
|
||||||
|
|
||||||
data Vect : ? -> Type -> Type where
|
|
||||||
Nil : Vect Z a
|
|
||||||
Cons : a -> Vect k a -> Vect (S k) a
|
|
||||||
|
|
||||||
append : Vect n a -> Vect m a -> Vect (plus n m) a
|
|
||||||
append Nil ys = ?appNil
|
|
||||||
append (Cons x xs) ys = ?appCons
|
|
||||||
|
|
||||||
app2 : Vect n a -> Vect m a -> Vect (plus n m) a
|
|
||||||
|
|
||||||
data Pair : Type -> Type -> Type where
|
|
||||||
MkPair : a -> b -> Pair a b
|
|
||||||
|
|
||||||
zip : Vect n a -> Vect n b -> Vect n (Pair a b)
|
|
||||||
|
|
||||||
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
|
|
||||||
|
|
@ -1,8 +0,0 @@
|
|||||||
Processing as TTImp
|
|
||||||
Written TTC
|
|
||||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \ys : (Main.Vect m[1] a[0]) => \0 n : Main.Nat => ys[1]
|
|
||||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:30} : Main.Nat => \x : a[1] => \xs : (Main.Vect {k:30}[1] a[2]) => \ys : (Main.Vect m[4] a[3]) => \0 n : Main.Nat => (Main.Cons (Main.plus {k:30}[4] m[6]) a[5] x[3] (Main.append m[6] a[5] {k:30}[4] xs[2] ys[1]))
|
|
||||||
Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:203}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:203}]) z) y))]
|
|
||||||
Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:319}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:319}]) z) w))]
|
|
||||||
Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:481}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:481}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))]
|
|
||||||
Yaffle> Bye for now!
|
|
@ -1,6 +0,0 @@
|
|||||||
:es appNil
|
|
||||||
:es appCons
|
|
||||||
:gd 25 app2
|
|
||||||
:gd 30 zip
|
|
||||||
:gd 32 zipWith
|
|
||||||
:q
|
|
@ -1,3 +0,0 @@
|
|||||||
$1 --yaffle Vect.yaff < input
|
|
||||||
|
|
||||||
rm -rf build
|
|
@ -1,57 +0,0 @@
|
|||||||
data Nat : Type where
|
|
||||||
Z : Nat
|
|
||||||
S : Nat -> Nat
|
|
||||||
|
|
||||||
plus : Nat -> Nat -> Nat
|
|
||||||
plus Z y = y
|
|
||||||
plus (S k) y = S (plus k y)
|
|
||||||
|
|
||||||
data Eq : a -> b -> Type where
|
|
||||||
Refl : Eq x x
|
|
||||||
|
|
||||||
rewrite__impl : {0 x, y : a} -> (0 p : _) ->
|
|
||||||
(0 rule : Eq x y) -> (1 val : p y) -> p x
|
|
||||||
rewrite__impl p Refl prf = prf
|
|
||||||
|
|
||||||
%rewrite Eq rewrite__impl
|
|
||||||
|
|
||||||
data Parity : Nat -> Type where
|
|
||||||
Even : (k : _) -> Parity (plus k k)
|
|
||||||
Odd : (k : _) -> Parity (S (plus k k))
|
|
||||||
|
|
||||||
plusnSm : (n : Nat) -> (m : Nat) ->
|
|
||||||
Eq (S (plus n m)) (plus n (S m))
|
|
||||||
plusnSm Z m = Refl
|
|
||||||
plusnSm (S k) m
|
|
||||||
= let ih = plusnSm k m in
|
|
||||||
rewrite ih in Refl
|
|
||||||
|
|
||||||
parity : (n : Nat) -> Parity n
|
|
||||||
parity Z = Even Z
|
|
||||||
parity (S k) with (parity k)
|
|
||||||
parity (S (plus l l)) | Even l = Odd l
|
|
||||||
parity (S (S (plus k k))) | Odd k
|
|
||||||
= rewrite plusnSm k k in Even (S k)
|
|
||||||
|
|
||||||
data Maybe : Type -> Type where
|
|
||||||
Nothing : Maybe a
|
|
||||||
Just : a -> Maybe a
|
|
||||||
|
|
||||||
eqNat : (x : Nat) -> (y : Nat) -> Maybe (Eq x y)
|
|
||||||
eqNat Z Z = Just Refl
|
|
||||||
eqNat Z (S k) = Nothing
|
|
||||||
eqNat (S k) Z = Nothing
|
|
||||||
eqNat (S k) (S j) with (eqNat k j)
|
|
||||||
eqNat (S k) (S k) | Just Refl = Just Refl
|
|
||||||
eqNat (S k) (S j) | Nothing = Nothing
|
|
||||||
|
|
||||||
data Pair : Type -> Type -> Type where
|
|
||||||
MkPair : a -> b -> Pair a b
|
|
||||||
|
|
||||||
eqPair : (x : Pair Nat Nat) -> (y : Pair Nat Nat) -> Maybe (Eq x y)
|
|
||||||
eqPair (MkPair x y) (MkPair w z) with (eqNat x w)
|
|
||||||
eqPair (MkPair x y) (MkPair x z) | Just Refl with (eqNat y z)
|
|
||||||
eqPair (MkPair x y) (MkPair x y) | Just Refl | Just Refl = Just Refl
|
|
||||||
eqPair (MkPair x y) (MkPair x z) | Just Refl | Nothing = Nothing
|
|
||||||
eqPair (MkPair x y) (MkPair w z) | Nothing = Nothing
|
|
||||||
|
|
@ -1,7 +0,0 @@
|
|||||||
Processing as TTImp
|
|
||||||
Written TTC
|
|
||||||
Yaffle> (Main.Odd (Main.S Main.Z))
|
|
||||||
Yaffle> (Main.Even (Main.S Main.Z))
|
|
||||||
Yaffle> (Main.Nothing [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) (Main.S Main.Z)) (Main.S (Main.S Main.Z))))])
|
|
||||||
Yaffle> ((Main.Just [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z)))]) ((Main.Refl [Just {b:10} = ((Main.Pair Main.Nat) Main.Nat)]) [Just x = ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))]))
|
|
||||||
Yaffle> Bye for now!
|
|
@ -1,5 +0,0 @@
|
|||||||
parity (S (S (S Z)))
|
|
||||||
parity (S (S Z))
|
|
||||||
eqPair (MkPair Z (S Z)) (MkPair (S Z) (S (S Z)))
|
|
||||||
eqPair (MkPair Z (S Z)) (MkPair Z (S Z))
|
|
||||||
:q
|
|
@ -1,3 +0,0 @@
|
|||||||
$1 --yaffle With.yaff < input
|
|
||||||
|
|
||||||
rm -rf build
|
|
Loading…
Reference in New Issue
Block a user