Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-08-15 18:20:26 +03:00
Code Issues Projects Releases Wiki Activity

Add Idris2 benchmark

Browse Source
This commit is contained in:
Victor Maia 2022-07-14 13:06:28 -03:00
parent 1707c3dfc8
commit 182814b528
6 changed files with 95 additions and 88 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
bench/README.md
View File

@ -4,19 +4,25 @@ Bench
Benchmarks of Kind2 vs other proof assistants. These benchmarks measure the time
each assistant takes to verify a given file. Replicate as follows:
### Agda:
### Agda
```
time agda -i src file.agda
```
### Kind2-i (interpreted HVM)
### Idris2
```
time idris2 --check file.idr
```
### Kind2
```
time kind2 check file.kind2
```
### Kind2-c (compiled HVM)
### Kind2-C
```
kind2 check file.kind2
@ -28,14 +34,15 @@ time ./check
Results
=======
### slow_num
### nat_exp
Computes `2 ^ 24`, using the Nat type, on the type level.
Computes `3 ^ 8`, using the Nat type, on the type level.
```
language | time
-------- | --------
Agda | 11.277 s
Kind2-i | 2.350 s
Kind2-c | 0.925 s
Kind2-C | 0.17 s
Kind2 | 0.58 s
Agda | 15.55 s
Idris2 | 67.40 s
```

25
bench/nat_exp.agda Normal file
View File

@ -0,0 +1,25 @@
data Nat : Set where
z : Nat
s : Nat -> Nat
data The : (x : Nat) -> Set where
val : (x : Nat) -> The x
add : Nat -> Nat -> Nat
add a (s b) = s (add a b)
add a z = a
mul : Nat -> Nat -> Nat
mul a (s b) = add a (mul a b)
mul a z = z
exp : Nat -> Nat -> Nat
exp a (s b) = mul a (exp a b)
exp a z = s z
nul : Nat -> Nat
nul (s a) = (nul a)
nul z = z
work : The (nul (exp (s (s (s z))) (s (s (s (s (s (s (s (s z))))))))))
work = val z

26
bench/nat_exp.idr Normal file
View File

@ -0,0 +1,26 @@
data NAT : Type where
Z : NAT
S : NAT -> NAT
data The : NAT -> Type where
Val : (x : NAT) -> The x
add : NAT -> NAT -> NAT
add a (S b) = S (add a b)
add a Z = a
mul : NAT -> NAT -> NAT
mul a (S b) = add a (mul a b)
mul a Z = Z
exp : NAT -> NAT -> NAT
exp a (S b) = mul a (exp a b)
exp a Z = S Z
nul : NAT -> NAT
nul (S a) = nul a
nul Z = Z
work : The (nul (exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z))))))))))
work = Val Z

29
bench/nat_exp.kind2 Normal file
View File

@ -0,0 +1,29 @@
Nat : Type
Z : Nat
S (pred: Nat) : Nat
The (x: Nat) : Type
Val (x: Nat) : {The x}
Add (a: Nat) (b: Nat) : Nat {
Add a {S b} = {S (Add a b)}
Add a {Z} = a
}
Mul (a: Nat) (b: Nat) : Nat {
Mul a {S b} = (Add a (Mul a b))
Mul a {Z} = {Z}
}
Exp (a: Nat) (b: Nat) : Nat {
Exp a {S b} = (Mul a (Exp a b))
Exp a {Z} = {S Z}
}
Nul (n: Nat) : Nat {
Nul {S a} = (Nul a)
Nul {Z} = {Z}
}
Work : {The (Nul (Exp {S {S {S Z}}} {S {S {S {S {S {S {S {S Z}}}}}}}}))} =
{Val Z}

39
bench/slow_num.agda
View File

@ -1,39 +0,0 @@
data Nat : Set where
zero : Nat
succ : Nat -> Nat
data The : (x : Nat) -> Set where
val : (x : Nat) -> The x
double : (x : Nat) -> Nat
double (succ x) = (succ (succ (double x)))
double zero = zero
power2 : (x : Nat) -> Nat
power2 (succ x) = (double (power2 x))
power2 zero = (succ zero)
destroy : (x : Nat) -> Nat
destroy (succ n) = (destroy n)
destroy zero = zero
slowNumber : Nat
slowNumber =
(destroy (power2
(succ (succ (succ (succ
(succ (succ (succ (succ
(succ (succ (succ (succ
(succ (succ (succ (succ
(succ (succ (succ (succ
(succ (succ (succ (succ
zero
))))
))))
))))
))))
))))
))))
))
main : The slowNumber
main = val zero

41
bench/slow_num.kind2
View File

@ -1,41 +0,0 @@
Nat : Type
Zero : Nat
Succ (pred: Nat) : Nat
The (x: Nat) : Type
Val (x: Nat) : {The x}
Double (x: Nat) : Nat {
Double {Succ x} = {Succ {Succ (Double x)}}
Double {Zero} = {Zero}
}
Pow2 (x: Nat) : Nat {
Pow2 {Succ x} = (Double (Pow2 x))
Pow2 {Zero} = {Succ Zero}
}
Destroy (x: Nat) : Nat {
Destroy {Succ n} = (Destroy n)
Destroy {Zero} = {Zero}
}
SlowNumber : Nat =
(Destroy (Pow2
{Succ {Succ {Succ {Succ
{Succ {Succ {Succ {Succ
{Succ {Succ {Succ {Succ
{Succ {Succ {Succ {Succ
{Succ {Succ {Succ {Succ
{Succ {Succ {Succ {Succ
Zero
}}}}
}}}}
}}}}
}}}}
}}}}
}}}}
))
// Proof that SlowNumber is 0
Main : {The (SlowNumber)} = {Val Zero}