08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
114 lines
2.8 KiB
Text
114 lines
2.8 KiB
Text
|
||
def foo (n : Nat) : Nat := match n with
|
||
| 0 => 0
|
||
| n+1 => foo n
|
||
termination_by structural n
|
||
|
||
-- Test that this is indeed by structural recursion
|
||
example : foo (n + 3) = foo n := Eq.refl _
|
||
|
||
|
||
-- Check that we can still refer to a variable called `structural` in
|
||
-- the `termination_by` syntax
|
||
def bar (structural : Nat) : True := match structural with
|
||
| 0 => .intro
|
||
| structural+1 => bar structural
|
||
termination_by «structural»
|
||
|
||
namespace Errors
|
||
-- A few error conditions
|
||
|
||
/--
|
||
error: cannot use specified measure for structural recursion:
|
||
it is unchanged in the recursive calls
|
||
-/
|
||
#guard_msgs in
|
||
def foo1 (n : Nat) : Nat := foo1 n
|
||
termination_by structural n
|
||
|
||
/--
|
||
error: cannot use specified measure for structural recursion:
|
||
its type Nat.le is an inductive family and indices are not variables
|
||
n.succ.le 100
|
||
-/
|
||
#guard_msgs in
|
||
def foo2 (n : Nat) (h : n < 100) : Nat := match n with
|
||
| 0 => 0
|
||
| n+1 => foo2 n (by omega)
|
||
termination_by structural h
|
||
|
||
/--
|
||
error: one parameter bound in `termination_by`, but the body of Errors.foo3 only binds 0 parameters.
|
||
-/
|
||
#guard_msgs in
|
||
def foo3 (n : Nat) : Nat → Nat := match n with
|
||
| 0 => id
|
||
| n+1 => foo3 n
|
||
termination_by structural m => m
|
||
|
||
/--
|
||
error: failed to infer structural recursion:
|
||
Cannot use parameter n:
|
||
failed to eliminate recursive application
|
||
ackermann (n + 1) m
|
||
-/
|
||
#guard_msgs in
|
||
def ackermann (n m : Nat) := match n, m with
|
||
| 0, m => m + 1
|
||
| .succ n, 0 => ackermann n 1
|
||
| .succ n, .succ m => ackermann n (ackermann (n + 1) m)
|
||
termination_by structural n
|
||
|
||
/--
|
||
error: failed to infer structural recursion:
|
||
Cannot use parameter m:
|
||
failed to eliminate recursive application
|
||
ackermann2 n 1
|
||
-/
|
||
#guard_msgs in
|
||
def ackermann2 (n m : Nat) := match n, m with
|
||
| 0, m => m + 1
|
||
| .succ n, 0 => ackermann2 n 1
|
||
| .succ n, .succ m => ackermann2 n (ackermann2 (n + 1) m)
|
||
termination_by structural m
|
||
|
||
/--
|
||
error: The termination measure of a structurally recursive function must be one of the parameters 'n', but
|
||
id n + 1
|
||
isn't one of these.
|
||
-/
|
||
#guard_msgs in
|
||
def foo4 (n : Nat) : Nat → Nat := match n with
|
||
| 0 => id
|
||
| n+1 => foo4 n
|
||
termination_by structural id n + 1
|
||
|
||
/--
|
||
error: failed to infer structural recursion:
|
||
Cannot use parameter #2:
|
||
the type Nat × Nat does not have a `.brecOn` recursor
|
||
-/
|
||
#guard_msgs in
|
||
def foo5 : Nat → (Nat × Nat) → Nat
|
||
| 0, _ => 0
|
||
| n+1, t => foo5 n t
|
||
termination_by structural n t => t
|
||
|
||
/--
|
||
error: failed to infer structural recursion:
|
||
Cannot use parameters #2 of Errors.foo6 and #2 of Errors.bar6:
|
||
the type Nat × Nat does not have a `.brecOn` recursor
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def foo6 : Nat → (Nat × Nat) → Nat
|
||
| 0, _ => 0
|
||
| n+1, t => bar6 n t
|
||
termination_by structural n t => t
|
||
def bar6 : Nat → (Nat × Nat) → Nat
|
||
| 0, _ => 0
|
||
| n+1, t => foo6 n t
|
||
termination_by structural n t => t
|
||
end
|
||
|
||
end Errors
|