mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-08-15 10:10:28 +03:00
Perf bugfixes and benchmarks
This commit is contained in:
Victor Maia
parent
1ee09c0b2b
commit
1707c3dfc8
41
bench/README.md
Normal file
41
bench/README.md
Normal file
@ -0,0 +1,41 @@
|
||||
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:
|
||||
|
||||
```
|
||||
time agda -i src file.agda
|
||||
```
|
||||
|
||||
### Kind2-i (interpreted HVM)
|
||||
|
||||
```
|
||||
time kind2 check file.kind2
|
||||
```
|
||||
|
||||
### Kind2-c (compiled HVM)
|
||||
|
||||
```
|
||||
kind2 check file.kind2
|
||||
hvm compile file.kind2.hvm
|
||||
clang file.kind2.c -O3 -o check
|
||||
time ./check
|
||||
```
|
||||
|
||||
Results
|
||||
=======
|
||||
|
||||
### slow_num
|
||||
|
||||
Computes `2 ^ 24`, using the Nat type, on the type level.
|
||||
|
||||
```
|
||||
language | time
|
||||
-------- | --------
|
||||
Agda | 11.277 s
|
||||
Kind2-i | 2.350 s
|
||||
Kind2-c | 0.925 s
|
||||
```
|
||||
39
bench/slow_num.agda
Normal file
39
bench/slow_num.agda
Normal file
@ -0,0 +1,39 @@
|
||||
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
Normal file
41
bench/slow_num.kind2
Normal file
@ -0,0 +1,41 @@
|
||||
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}
|
||||
@ -32,17 +32,12 @@ Double (x: Nat) : Nat {
|
||||
Double {Zero} = {Zero}
|
||||
}
|
||||
|
||||
// FIXME: this won't check since `a != t`
|
||||
// FIXME: shouldn't type-check, but does due to Inp treatment
|
||||
Tail (a: Type) (xs: {List a}) : {List a} {
|
||||
Tail a {Cons t x xs} = xs
|
||||
Tail a {Cons t x xs} = x
|
||||
}
|
||||
|
||||
The (x: Nat) : Type
|
||||
Val (x: Nat) : {The x}
|
||||
|
||||
Main : {The {Succ {Succ Zero}}} =
|
||||
{Val (Double {Succ Zero})}
|
||||
|
||||
|
||||
Main : Nat = (Double {Succ {Succ Zero}})
|
||||
|
||||
|
||||
|
||||
|
||||
316
src/checker.hvm
316
src/checker.hvm
@ -1,3 +1,5 @@
|
||||
Main = Api.check_all
|
||||
|
||||
Api.check_all =
|
||||
let output = (Api.output (Api.check_functions Functions))
|
||||
(Bool.if (String.is_empty output)
|
||||
@ -429,7 +431,7 @@ Api.run_main =
|
||||
// Checks others
|
||||
(Check term type) =
|
||||
ask term_typ = (Checker.bind (Infer term))
|
||||
ask is_equal = (Checker.bind (Equal (Eval term_typ) (Eval type)))
|
||||
ask is_equal = (Checker.bind (Equal term_typ type))
|
||||
(Bool.if is_equal
|
||||
// then
|
||||
(Checker.done Unit)
|
||||
@ -628,39 +630,78 @@ Api.run_main =
|
||||
|
||||
// Eval Fn0
|
||||
(Eval (Fn0 ctid)) =
|
||||
(Eval (Rule_0 ctid))
|
||||
(Rule_0 ctid)
|
||||
|
||||
// Eval Fn1
|
||||
(Eval (Fn1 ctid x0)) =
|
||||
(Eval (Rule_1 ctid (Eval x0)))
|
||||
(Rule_1 ctid (Eval x0))
|
||||
|
||||
// Eval Fn2
|
||||
(Eval (Fn2 ctid x0 x1)) =
|
||||
(Eval (Rule_2 ctid (Eval x0) (Eval x1)))
|
||||
(Rule_2 ctid (Eval x0) (Eval x1))
|
||||
|
||||
// Eval Fn3
|
||||
(Eval (Fn3 ctid x0 x1 x2)) =
|
||||
(Eval (Rule_3 ctid (Eval x0) (Eval x1) (Eval x2)))
|
||||
(Rule_3 ctid (Eval x0) (Eval x1) (Eval x2))
|
||||
|
||||
// Eval Fn4
|
||||
(Eval (Fn4 ctid x0 x1 x2 x3)) =
|
||||
(Eval (Rule_4 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3)))
|
||||
(Rule_4 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3))
|
||||
|
||||
// Eval Fn5
|
||||
(Eval (Fn5 ctid x0 x1 x2 x3 x4)) =
|
||||
(Eval (Rule_5 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4)))
|
||||
(Rule_5 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4))
|
||||
|
||||
// Eval Fn6
|
||||
(Eval (Fn6 ctid x0 x1 x2 x3 x4 x5)) =
|
||||
(Eval (Rule_6 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5)))
|
||||
(Rule_6 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5))
|
||||
|
||||
// Eval Fn7
|
||||
(Eval (Fn7 ctid x0 x1 x2 x3 x4 x5 x6)) =
|
||||
(Eval (Rule_7 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5) (Eval x6)))
|
||||
(Rule_7 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5) (Eval x6))
|
||||
|
||||
// Eval Fn8
|
||||
(Eval (Fn8 ctid x0 x1 x2 x3 x4 x5 x6 x7)) =
|
||||
(Eval (Rule_8 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5) (Eval x6) (Eval x7)))
|
||||
(Rule_8 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5) (Eval x6) (Eval x7))
|
||||
|
||||
// Func
|
||||
// ----
|
||||
|
||||
// NewFn0 to Fn0
|
||||
(NewFn0 ctid) =
|
||||
(Fn0 ctid)
|
||||
|
||||
// NewFn1 to Fn1
|
||||
(NewFn1 ctid x0) =
|
||||
(Fn1 ctid x0)
|
||||
|
||||
// NewFn2 to Fn2
|
||||
(NewFn2 ctid x0 x1) =
|
||||
(Fn2 ctid x0 x1)
|
||||
|
||||
// NewFn3 to Fn3
|
||||
(NewFn3 ctid x0 x1 x2) =
|
||||
(Fn3 ctid x0 x1 x2)
|
||||
|
||||
// NewFn4 to Fn4
|
||||
(NewFn4 ctid x0 x1 x2 x3) =
|
||||
(Fn4 ctid x0 x1 x2 x3)
|
||||
|
||||
// NewFn5 to Fn5
|
||||
(NewFn5 ctid x0 x1 x2 x3 x4) =
|
||||
(Fn5 ctid x0 x1 x2 x3 x4)
|
||||
|
||||
// NewFn6 to Fn6
|
||||
(NewFn6 ctid x0 x1 x2 x3 x4 x5) =
|
||||
(Fn6 ctid x0 x1 x2 x3 x4 x5)
|
||||
|
||||
// NewFn7 to Fn7
|
||||
(NewFn7 ctid x0 x1 x2 x3 x4 x5 x6) =
|
||||
(Fn7 ctid x0 x1 x2 x3 x4 x5 x6)
|
||||
|
||||
// NewFn8 to Fn8
|
||||
(NewFn8 ctid x0 x1 x2 x3 x4 x5 x6 x7) =
|
||||
(Fn8 ctid x0 x1 x2 x3 x4 x5 x6 x7)
|
||||
|
||||
// Apply Term Term : Term
|
||||
// ----------------------
|
||||
@ -890,3 +931,258 @@ Api.run_main =
|
||||
// User-Defined Functions
|
||||
// ----------------------
|
||||
////INJECT////
|
||||
|
||||
Functions =
|
||||
let fns = Nil
|
||||
let fns = (Cons And. fns)
|
||||
let fns = (Cons Bool. fns)
|
||||
let fns = (Cons Not. fns)
|
||||
let fns = (Cons Main. fns)
|
||||
let fns = (Cons Pow2. fns)
|
||||
let fns = (Cons False. fns)
|
||||
let fns = (Cons True. fns)
|
||||
let fns = (Cons Succ. fns)
|
||||
let fns = (Cons Foo. fns)
|
||||
let fns = (Cons Negate. fns)
|
||||
let fns = (Cons Tail. fns)
|
||||
let fns = (Cons Nat. fns)
|
||||
let fns = (Cons Double. fns)
|
||||
let fns = (Cons Zero. fns)
|
||||
let fns = (Cons The. fns)
|
||||
let fns = (Cons List. fns)
|
||||
let fns = (Cons Val. fns)
|
||||
let fns = (Cons Nil. fns)
|
||||
let fns = (Cons Destroy. fns)
|
||||
let fns = (Cons Cons. fns)
|
||||
fns
|
||||
|
||||
// And
|
||||
// ---
|
||||
|
||||
(NameOf And.) = "And"
|
||||
(HashOf And.) = %And
|
||||
(TypeOf And.) = (All (Ct0 Bool.) λa (All (Ct0 Bool.) λb (Ct0 Bool.)))
|
||||
(Body_2 And. (Ct0 True.) (Ct0 True.)) = (Ct0 True.)
|
||||
(Rule_2 And. (Ct0 True.) (Ct0 True.)) = (Ct0 True.)
|
||||
(Body_2 And. (Ct0 True.) (Ct0 False.)) = (Ct0 False.)
|
||||
(Rule_2 And. (Ct0 True.) (Ct0 False.)) = (Ct0 False.)
|
||||
(Body_2 And. (Ct0 False.) (Ct0 True.)) = (Ct0 False.)
|
||||
(Rule_2 And. (Ct0 False.) (Ct0 True.)) = (Ct0 False.)
|
||||
(Body_2 And. (Ct0 False.) (Ct0 False.)) = (Ct0 False.)
|
||||
(Rule_2 And. (Ct0 False.) (Ct0 False.)) = (Ct0 False.)
|
||||
(Verify And.) =
|
||||
(Cons (LHS (Ct0 True.) (LHS (Ct0 True.) (RHS (Body_2 And. (Ct0 True.) (Ct0 True.)))))
|
||||
(Cons (LHS (Ct0 True.) (LHS (Ct0 False.) (RHS (Body_2 And. (Ct0 True.) (Ct0 False.)))))
|
||||
(Cons (LHS (Ct0 False.) (LHS (Ct0 True.) (RHS (Body_2 And. (Ct0 False.) (Ct0 True.)))))
|
||||
(Cons (LHS (Ct0 False.) (LHS (Ct0 False.) (RHS (Body_2 And. (Ct0 False.) (Ct0 False.)))))
|
||||
Nil))))
|
||||
|
||||
// Bool
|
||||
// ----
|
||||
|
||||
(NameOf Bool.) = "Bool"
|
||||
(HashOf Bool.) = %Bool
|
||||
(TypeOf Bool.) = Typ
|
||||
(Verify Bool.) =
|
||||
Nil
|
||||
|
||||
// Not
|
||||
// ---
|
||||
|
||||
(NameOf Not.) = "Not"
|
||||
(HashOf Not.) = %Not
|
||||
(TypeOf Not.) = (All (Ct0 Bool.) λa (Ct0 Bool.))
|
||||
(Body_1 Not. (Ct0 True.)) = (Ct0 False.)
|
||||
(Rule_1 Not. (Ct0 True.)) = (Ct0 False.)
|
||||
(Body_1 Not. (Ct0 False.)) = (Ct0 True.)
|
||||
(Rule_1 Not. (Ct0 False.)) = (Ct0 True.)
|
||||
(Verify Not.) =
|
||||
(Cons (LHS (Ct0 True.) (RHS (Body_1 Not. (Ct0 True.))))
|
||||
(Cons (LHS (Ct0 False.) (RHS (Body_1 Not. (Ct0 False.))))
|
||||
Nil))
|
||||
|
||||
// Main
|
||||
// ----
|
||||
|
||||
(NameOf Main.) = "Main"
|
||||
(HashOf Main.) = %Main
|
||||
(TypeOf Main.) = (Ct0 Nat.)
|
||||
(Body_0 Main.) = (NewFn0 Foo.)
|
||||
(Rule_0 Main.) = (Rule_0 Foo.)
|
||||
(Verify Main.) =
|
||||
(Cons (RHS (Body_0 Main.))
|
||||
Nil)
|
||||
|
||||
// Pow2
|
||||
// ----
|
||||
|
||||
(NameOf Pow2.) = "Pow2"
|
||||
(HashOf Pow2.) = %Pow2
|
||||
(TypeOf Pow2.) = (All (Ct0 Nat.) λx (Ct0 Nat.))
|
||||
(Body_1 Pow2. (Ct1 Succ. x)) = (NewFn1 Double. (NewFn1 Pow2. x))
|
||||
(Rule_1 Pow2. (Ct1 Succ. x)) = (Rule_1 Double. (Rule_1 Pow2. x))
|
||||
(Body_1 Pow2. (Ct0 Zero.)) = (Ct1 Succ. (Ct0 Zero.))
|
||||
(Rule_1 Pow2. (Ct0 Zero.)) = (Ct1 Succ. (Ct0 Zero.))
|
||||
(Verify Pow2.) =
|
||||
(Cons (LHS (Ct1 Succ. (Inp 0)) (RHS (Body_1 Pow2. (Ct1 Succ. (Var 0)))))
|
||||
(Cons (LHS (Ct0 Zero.) (RHS (Body_1 Pow2. (Ct0 Zero.))))
|
||||
Nil))
|
||||
|
||||
// False
|
||||
// -----
|
||||
|
||||
(NameOf False.) = "False"
|
||||
(HashOf False.) = %False
|
||||
(TypeOf False.) = (Ct0 Bool.)
|
||||
(Verify False.) =
|
||||
Nil
|
||||
|
||||
// True
|
||||
// ----
|
||||
|
||||
(NameOf True.) = "True"
|
||||
(HashOf True.) = %True
|
||||
(TypeOf True.) = (Ct0 Bool.)
|
||||
(Verify True.) =
|
||||
Nil
|
||||
|
||||
// Succ
|
||||
// ----
|
||||
|
||||
(NameOf Succ.) = "Succ"
|
||||
(HashOf Succ.) = %Succ
|
||||
(TypeOf Succ.) = (All (Ct0 Nat.) λpred (Ct0 Nat.))
|
||||
(Verify Succ.) =
|
||||
Nil
|
||||
|
||||
// Foo
|
||||
// ---
|
||||
|
||||
(NameOf Foo.) = "Foo"
|
||||
(HashOf Foo.) = %Foo
|
||||
(TypeOf Foo.) = (Ct0 Nat.)
|
||||
(Body_0 Foo.) = (NewFn1 Destroy. (NewFn1 Pow2. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct0 Zero.)))))))))))))))))
|
||||
(Rule_0 Foo.) = (Rule_1 Destroy. (Rule_1 Pow2. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct1 Succ. (Ct0 Zero.)))))))))))))))))
|
||||
(Verify Foo.) =
|
||||
(Cons (RHS (Body_0 Foo.))
|
||||
Nil)
|
||||
|
||||
// Negate
|
||||
// ------
|
||||
|
||||
(NameOf Negate.) = "Negate"
|
||||
(HashOf Negate.) = %Negate
|
||||
(TypeOf Negate.) = (All (Ct1 List. (Ct0 Bool.)) λxs (Ct1 List. (Ct0 Bool.)))
|
||||
(Body_1 Negate. (Ct3 Cons. (Ct0 Bool.) x xs)) = (Ct3 Cons. (Ct0 Bool.) (NewFn1 Not. x) (NewFn1 Negate. xs))
|
||||
(Rule_1 Negate. (Ct3 Cons. (Ct0 Bool.) x xs)) = (Ct3 Cons. (Ct0 Bool.) (Rule_1 Not. x) (Rule_1 Negate. xs))
|
||||
(Body_1 Negate. (Ct1 Nil. (Ct0 Bool.))) = (Ct1 Nil. (Ct0 Bool.))
|
||||
(Rule_1 Negate. (Ct1 Nil. (Ct0 Bool.))) = (Ct1 Nil. (Ct0 Bool.))
|
||||
(Verify Negate.) =
|
||||
(Cons (LHS (Ct3 Cons. (Ct0 Bool.) (Inp 0) (Inp 1)) (RHS (Body_1 Negate. (Ct3 Cons. (Ct0 Bool.) (Var 0) (Var 1)))))
|
||||
(Cons (LHS (Ct1 Nil. (Ct0 Bool.)) (RHS (Body_1 Negate. (Ct1 Nil. (Ct0 Bool.)))))
|
||||
Nil))
|
||||
|
||||
// Tail
|
||||
// ----
|
||||
|
||||
(NameOf Tail.) = "Tail"
|
||||
(HashOf Tail.) = %Tail
|
||||
(TypeOf Tail.) = (All Typ λa (All (Ct1 List. a) λxs (Ct1 List. a)))
|
||||
(Body_2 Tail. a (Ct3 Cons. t x xs)) = xs
|
||||
(Rule_2 Tail. a (Ct3 Cons. t x xs)) = xs
|
||||
(Verify Tail.) =
|
||||
(Cons (LHS (Inp 0) (LHS (Ct3 Cons. (Inp 1) (Inp 2) (Inp 3)) (RHS (Body_2 Tail. (Var 0) (Ct3 Cons. (Var 1) (Var 2) (Var 3))))))
|
||||
Nil)
|
||||
|
||||
// Nat
|
||||
// ---
|
||||
|
||||
(NameOf Nat.) = "Nat"
|
||||
(HashOf Nat.) = %Nat
|
||||
(TypeOf Nat.) = Typ
|
||||
(Verify Nat.) =
|
||||
Nil
|
||||
|
||||
// Double
|
||||
// ------
|
||||
|
||||
(NameOf Double.) = "Double"
|
||||
(HashOf Double.) = %Double
|
||||
(TypeOf Double.) = (All (Ct0 Nat.) λx (Ct0 Nat.))
|
||||
(Body_1 Double. (Ct1 Succ. x)) = (Ct1 Succ. (Ct1 Succ. (NewFn1 Double. x)))
|
||||
(Rule_1 Double. (Ct1 Succ. x)) = (Ct1 Succ. (Ct1 Succ. (Rule_1 Double. x)))
|
||||
(Body_1 Double. (Ct0 Zero.)) = (Ct0 Zero.)
|
||||
(Rule_1 Double. (Ct0 Zero.)) = (Ct0 Zero.)
|
||||
(Verify Double.) =
|
||||
(Cons (LHS (Ct1 Succ. (Inp 0)) (RHS (Body_1 Double. (Ct1 Succ. (Var 0)))))
|
||||
(Cons (LHS (Ct0 Zero.) (RHS (Body_1 Double. (Ct0 Zero.))))
|
||||
Nil))
|
||||
|
||||
// Zero
|
||||
// ----
|
||||
|
||||
(NameOf Zero.) = "Zero"
|
||||
(HashOf Zero.) = %Zero
|
||||
(TypeOf Zero.) = (Ct0 Nat.)
|
||||
(Verify Zero.) =
|
||||
Nil
|
||||
|
||||
// The
|
||||
// ---
|
||||
|
||||
(NameOf The.) = "The"
|
||||
(HashOf The.) = %The
|
||||
(TypeOf The.) = (All (Ct0 Nat.) λx Typ)
|
||||
(Verify The.) =
|
||||
Nil
|
||||
|
||||
// List
|
||||
// ----
|
||||
|
||||
(NameOf List.) = "List"
|
||||
(HashOf List.) = %List
|
||||
(TypeOf List.) = (All Typ λa Typ)
|
||||
(Verify List.) =
|
||||
Nil
|
||||
|
||||
// Val
|
||||
// ---
|
||||
|
||||
(NameOf Val.) = "Val"
|
||||
(HashOf Val.) = %Val
|
||||
(TypeOf Val.) = (All (Ct0 Nat.) λx (Ct1 The. x))
|
||||
(Verify Val.) =
|
||||
Nil
|
||||
|
||||
// Nil
|
||||
// ---
|
||||
|
||||
(NameOf Nil.) = "Nil"
|
||||
(HashOf Nil.) = %Nil
|
||||
(TypeOf Nil.) = (All Typ λa (Ct1 List. a))
|
||||
(Verify Nil.) =
|
||||
Nil
|
||||
|
||||
// Destroy
|
||||
// -------
|
||||
|
||||
(NameOf Destroy.) = "Destroy"
|
||||
(HashOf Destroy.) = %Destroy
|
||||
(TypeOf Destroy.) = (All (Ct0 Nat.) λx (Ct0 Nat.))
|
||||
(Body_1 Destroy. (Ct1 Succ. n)) = (NewFn1 Destroy. n)
|
||||
(Rule_1 Destroy. (Ct1 Succ. n)) = (Rule_1 Destroy. n)
|
||||
(Body_1 Destroy. (Ct0 Zero.)) = (Ct0 Zero.)
|
||||
(Rule_1 Destroy. (Ct0 Zero.)) = (Ct0 Zero.)
|
||||
(Verify Destroy.) =
|
||||
(Cons (LHS (Ct1 Succ. (Inp 0)) (RHS (Body_1 Destroy. (Ct1 Succ. (Var 0)))))
|
||||
(Cons (LHS (Ct0 Zero.) (RHS (Body_1 Destroy. (Ct0 Zero.))))
|
||||
Nil))
|
||||
|
||||
// Cons
|
||||
// ----
|
||||
|
||||
(NameOf Cons.) = "Cons"
|
||||
(HashOf Cons.) = %Cons
|
||||
(TypeOf Cons.) = (All Typ λa (All a λx (All (Ct1 List. a) λxs (Ct1 List. a))))
|
||||
(Verify Cons.) =
|
||||
Nil
|
||||
|
||||
106
src/main.rs
106
src/main.rs
@ -7,6 +7,7 @@ use std::collections::HashMap;
|
||||
use hvm::parser as parser;
|
||||
|
||||
fn main() -> Result<(), String> {
|
||||
gen();
|
||||
|
||||
let args: Vec<String> = std::env::args().collect();
|
||||
|
||||
@ -35,16 +36,26 @@ fn main() -> Result<(), String> {
|
||||
let mut checker = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string();
|
||||
checker.push_str(&code);
|
||||
|
||||
std::fs::write("tmp.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file
|
||||
std::fs::write(format!("{}.hvm", path), checker.clone()).ok(); // writes checker to the checker.hvm file
|
||||
|
||||
let mut rt = hvm::Runtime::from_code(&checker)?;
|
||||
let main = rt.alloc_code(if args[1] == "check" { "Api.check_all" } else { "Api.run_main" })?;
|
||||
rt.normalize(main);
|
||||
println!("{}", readback_string(&rt, main)); // TODO: optimize by deserializing term into text directly
|
||||
|
||||
println!("Rewrites: {}", rt.get_rewrites());
|
||||
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
fn gen() {
|
||||
let file = read_file(&DEMO_CODE).unwrap();
|
||||
let code = compile_file(&file);
|
||||
let mut checker = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string();
|
||||
checker.push_str(&code);
|
||||
std::fs::write("tmp.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file
|
||||
}
|
||||
|
||||
const CHECKER_HVM: &str = include_str!("checker.hvm");
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
@ -384,7 +395,7 @@ pub fn read_file(code: &str) -> Result<Box<File>, String> {
|
||||
//Ctr { name: String, args: Vec<Box<Term>> },
|
||||
//Fun { name: String, args: Vec<Box<Term>> },
|
||||
//}
|
||||
pub fn compile_term(term: &Term) -> String {
|
||||
pub fn compile_term(term: &Term, quote: bool) -> String {
|
||||
match term {
|
||||
Term::Typ => {
|
||||
format!("Typ")
|
||||
@ -396,27 +407,27 @@ pub fn compile_term(term: &Term) -> String {
|
||||
todo!()
|
||||
}
|
||||
Term::All { name, tipo, body } => {
|
||||
format!("(All {} λ{} {})", compile_term(tipo), name, compile_term(body))
|
||||
format!("(All {} λ{} {})", compile_term(tipo, quote), name, compile_term(body, quote))
|
||||
}
|
||||
Term::Lam { name, body } => {
|
||||
format!("(Lam λ{} {})", name, compile_term(body))
|
||||
format!("(Lam λ{} {})", name, compile_term(body, quote))
|
||||
}
|
||||
Term::App { func, argm } => {
|
||||
format!("(App {} {})", compile_term(func), compile_term(argm))
|
||||
format!("({} {} {})", if quote { "App" } else { "Apply" }, compile_term(func, quote), compile_term(argm, quote))
|
||||
}
|
||||
Term::Ctr { name, args } => {
|
||||
let mut args_strs : Vec<String> = Vec::new();
|
||||
for arg in args {
|
||||
args_strs.push(format!(" {}", compile_term(arg)));
|
||||
args_strs.push(format!(" {}", compile_term(arg, quote)));
|
||||
}
|
||||
format!("(Ct{} {}.{})", args.len(), name, args_strs.join(""))
|
||||
}
|
||||
Term::Fun { name, args } => {
|
||||
let mut args_strs : Vec<String> = Vec::new();
|
||||
for arg in args {
|
||||
args_strs.push(format!(" {}", compile_term(arg)));
|
||||
args_strs.push(format!(" {}", compile_term(arg, quote)));
|
||||
}
|
||||
format!("(Fn{} {}.{})", args.len(), name, args_strs.join(""))
|
||||
format!("({}{} {}.{})", if quote { "NewFn" } else { "Rule_" }, args.len(), name, args_strs.join(""))
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -425,21 +436,23 @@ pub fn compile_entry(entry: &Entry) -> String {
|
||||
fn compile_type(args: &Vec<Box<Argument>>, tipo: &Box<Term>, index: usize) -> String {
|
||||
if index < args.len() {
|
||||
let arg = &args[index];
|
||||
format!("(All {} λ{} {})", compile_term(&arg.tipo), arg.name, compile_type(args, tipo, index + 1))
|
||||
format!("(All {} λ{} {})", compile_term(&arg.tipo, false), arg.name, compile_type(args, tipo, index + 1))
|
||||
} else {
|
||||
compile_term(tipo)
|
||||
compile_term(tipo, false)
|
||||
}
|
||||
}
|
||||
|
||||
fn compile_rule(rule: &Rule) -> String {
|
||||
let mut pats = vec![];
|
||||
for pat in &rule.pats {
|
||||
pats.push(format!(" {}", compile_term(pat)));
|
||||
pats.push(format!(" {}", compile_term(pat, false)));
|
||||
}
|
||||
let body = compile_term(&rule.body);
|
||||
let body_quot = compile_term(&rule.body, true);
|
||||
let body_exec = compile_term(&rule.body, false);
|
||||
let mut text = String::new();
|
||||
//text.push_str(&format!(" (Rule{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body));
|
||||
text.push_str(&format!(" (Rule_{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body));
|
||||
text.push_str(&format!(" (Body_{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body_quot));
|
||||
text.push_str(&format!(" (Rule_{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body_exec));
|
||||
return text;
|
||||
}
|
||||
|
||||
@ -451,7 +464,7 @@ pub fn compile_entry(entry: &Entry) -> String {
|
||||
let tail = compile_rule_chk(rule, index + 1, vars, args);
|
||||
return format!("(LHS {} {})", head, tail);
|
||||
} else {
|
||||
return format!("(RHS (Rule_{} {}.{}))", index, rule.name, args.iter().map(|x| format!(" {}", x)).collect::<Vec<String>>().join(""));
|
||||
return format!("(RHS (Body_{} {}.{}))", index, rule.name, args.iter().map(|x| format!(" {}", x)).collect::<Vec<String>>().join(""));
|
||||
}
|
||||
}
|
||||
|
||||
@ -542,38 +555,45 @@ fn readback_string(rt: &hvm::Runtime, host: u64) -> String {
|
||||
}
|
||||
|
||||
const DEMO_CODE: &str = "
|
||||
Bool : Type
|
||||
True : Bool
|
||||
False : Bool
|
||||
Nat : Type
|
||||
Zero : Nat
|
||||
Succ (pred: Nat) : Nat
|
||||
|
||||
Nat : Type
|
||||
Zero : Nat
|
||||
Succ (pred: Nat) : Nat
|
||||
The (x: Nat) : Type
|
||||
Val (x: Nat) : {The x}
|
||||
|
||||
List (a: Type) : Type
|
||||
Nil (a: Type) : {List a}
|
||||
Cons (a: Type) (x: a) (xs: {List a}) : {List a}
|
||||
Double (x: Nat) : Nat {
|
||||
Double {Succ x} = {Succ {Succ (Double x)}}
|
||||
Double {Zero} = {Zero}
|
||||
}
|
||||
|
||||
Not (a: Bool) : Bool {
|
||||
Not True = False
|
||||
Not False = True
|
||||
}
|
||||
Pow2 (x: Nat) : Nat {
|
||||
Pow2 {Succ x} = (Double (Pow2 x))
|
||||
Pow2 {Zero} = {Succ Zero}
|
||||
}
|
||||
|
||||
And (a: Bool) (b: Bool) : Bool {
|
||||
And True True = True
|
||||
And True False = False
|
||||
And False True = False
|
||||
And False False = False
|
||||
}
|
||||
Destroy (x: Nat) : Nat {
|
||||
Destroy {Succ n} = (Destroy n)
|
||||
Destroy {Zero} = {Zero}
|
||||
}
|
||||
|
||||
Negate (xs: {List Bool}) : {List Bool} {
|
||||
Negate {Cons Bool x xs} = {Cons Bool (Not x) (Negate xs)}
|
||||
Negate {Nil Bool} = {Nil Bool}
|
||||
}
|
||||
|
||||
Tail (a: Type) (xs: {List a}) : {List a} {
|
||||
Tail a {Cons t x xs} = xs
|
||||
}
|
||||
|
||||
Main : {List Bool} = (Tail Bool {Cons Bool True {Cons Bool False {Nil Bool}}})
|
||||
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}
|
||||
";
|
||||
|
||||
Loading…
Reference in New Issue
Block a user