Same test code to multiple functions

Stream: Is there code for X?

[Asei Inoue]

I am working on a translation of haskell 99 into Lean.
https://github.com/lean-ja/lean99

Each question has a test code attached to it, so that the test passes if the sorry is replaced by the correct implementation.
I sometimes want to present more than one example solution to a problem, but I am faced with the problem that it is difficult to use the test code all over again.

Is there a way to use the same test code for S1.f and S2.f when there are functions f with the same name in different namespaces S1 and S2?

[Eric Wieser]

Write your test code as a function that takes in f as input?

[Asei Inoue]

Write your test code as a function that takes in f as input?

That way, I end up having to write as much test code as there are functions, don't I?

In one piece of code, I want to test all functions for a given test case.

[Eric Wieser]

That way, I end up having to write as much test code as there are functions, don't I?

You will need to write a new testbench for every specification of the function, but not for every implementation of that specification.

[Eric Wieser]

I think your question would be much clearer with a mwe; what do you mean by "function"? What do you mean by "test code"?

[Kyle Miller]

I see that the test cases are written like

example : rotate [1, 2, 3] 3 = [1, 2, 3] := rfl

One thing is you can write this as

#guard rotate [1, 2, 3] 3 = [1, 2, 3]

which checks that this condition evaluates to true.

[Kyle Miller]

If you want to parameterize your tests so that you can give multiple implementations (like Eric's suggestion), here's how I might do that (though I might set up some helper functions/macros to print error messages for the individual failing tests):

def test_rotate (rotate : List α -> Nat -> List α) : Bool :=
  (rotate [1, 2, 3, 4, 5] 2 = [3, 4, 5, 1, 2])
  && (rotate [1, 2, 3] 0 = [1, 2, 3])
  && (rotate [1, 2, 3] 3 = [1, 2, 3])
  && (rotate [1, 2, 3] 1 = [2, 3, 1])

#guard test_rotate rotate
#guard test_rotate other_rotate

[Asei Inoue]

@Eric Wieser @Kyle Miller Thank you.

variable {α : Type}

namespace S1

def myLast (l : List α) : Option α :=
  match l with
  | [] => none
  | [a] => a
  | _ :: as => myLast as

end S1

namespace S2

def myLast (l : List α) : Option α := l.reverse |>.head?

end S2

-- The following codes are for test

example : myLast [1, 2, 3, 4] = some 4 := by rfl

example : myLast ([] : List α) = none := by rfl

example : myLast [1] = some 1 := by rfl

example : myLast ['x', 'y', 'z'] = some 'z' := by rfl

[Asei Inoue]

Above is the MWE, can I test S1.myLast and S2.myLast at the same time?

[Eric Wieser]

Here's the lowest-tech solution:

macro "#mytests " f:ident : command =>
  `(example : $f [1, 2, 3, 4] = some 4 := by rfl

    example : $f ([] : List α) = none := by rfl

    example : $f [1] = some 1 := by rfl

    example : $f ['x', 'y', 'z'] = some 'z' := by rfl)

#mytests S1.myLast