/-!
This files tests Lean's ability to guess the right lexicographic order.

When writing tests for GuesLex, keep in mind that it doesn't do anything
when there is only one plausible measure (one function, only one varying argument).
-/

set_option showInferredTerminationBy true

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)

def ackermann2 (n m : Nat) := match n, m with
  | m, 0 => m + 1
  | 0, .succ n => ackermann2 1 n
  | .succ m, .succ n => ackermann2 (ackermann2 m (n + 1)) n

def ackermannList (n m : List Unit) := match n, m with
  | [], m => () :: m
  | ()::n, [] => ackermannList n [()]
  | ()::n, ()::m => ackermannList n (ackermannList (()::n) m)

def foo2 : Nat → Nat → Nat
  | .succ n, 1 => foo2 n 1
  | .succ n, 2 => foo2 (.succ n) 1
  | n,       3 => foo2 (.succ n) 2
  | .succ n, 4 => foo2 (if n > 10 then n else .succ n) 3
  | n,       5 => foo2 (n - 1) 4
  | n, .succ m => foo2 n m
  | _, _ => 0

mutual
def even : Nat → Bool
  | 0 => true
  | .succ n => not (odd n)
def odd : Nat → Bool
  | 0 => false
  | .succ n => not (even n)
end

mutual
def evenWithFixed (m : String) : Nat → Bool
  | 0 => true
  | .succ n => not (oddWithFixed m n)
def oddWithFixed (m : String) : Nat → Bool
  | 0 => false
  | .succ n => not (evenWithFixed m n)
end

def ping (n : Nat) := pong n
   where pong : Nat → Nat
  | 0 => 0
  | .succ n => ping n

def hasForbiddenArg (n : Nat) (_h : n = n) (m : Nat) : Nat :=
  match n, m with
  | 0, 0 => 0
  | .succ m, n => hasForbiddenArg m rfl n
  | m, .succ n => hasForbiddenArg (.succ m) rfl n

/-!
Example from “Finding Lexicographic Orders for Termination Proofs in
Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow,
10.1007/978-3-540-74591-4_5
-/
def blowup : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat
  | 0, 0, 0, 0, 0, 0, 0, 0 => 0
  | 0, 0, 0, 0, 0, 0, 0, .succ i => .succ (blowup i i i i i i i i)
  | 0, 0, 0, 0, 0, 0, .succ h, i => .succ (blowup h h h h h h h i)
  | 0, 0, 0, 0, 0, .succ g, h, i => .succ (blowup g g g g g g h i)
  | 0, 0, 0, 0, .succ f, g, h, i => .succ (blowup f f f f f g h i)
  | 0, 0, 0, .succ e, f, g, h, i => .succ (blowup e e e e f g h i)
  | 0, 0, .succ d, e, f, g, h, i => .succ (blowup d d d e f g h i)
  | 0, .succ c, d, e, f, g, h, i => .succ (blowup c c d e f g h i)
  | .succ b, c, d, e, f, g, h, i => .succ (blowup b c d e f g h i)

-- Let’s try to confuse the lexicographic guessing function's
-- unpacking of packed n-ary arguments
def confuseLex1 : Nat → @PSigma Nat (fun _ => Nat) → Nat
  | 0, _p => 0
  | .succ n, ⟨x,y⟩ => confuseLex1 n ⟨x, .succ y⟩

def confuseLex2 : @PSigma Nat (fun _ => Nat) → Nat
  | ⟨_,0⟩ => 0
  | ⟨0,_⟩ => 0
  | ⟨.succ y,.succ n⟩ => confuseLex2 ⟨y,n⟩

def dependent : (n : Nat) → (m : Fin n) → Nat
 | 0, i => Fin.elim0 i
 | .succ 0, 0 => 0
 | .succ (.succ n), 0 => dependent (.succ n) ⟨n, n.lt_succ_self⟩
 | .succ (.succ n), ⟨.succ m, h⟩ =>
  dependent (.succ (.succ n)) ⟨m, Nat.lt_of_le_of_lt (Nat.le_succ _) h⟩

-- An example based on a real world problem, condensed by Leo
inductive Expr where
  | add (a b : Expr)
  | val (n : Nat)

mutual
def eval (a : Expr) : Nat :=
  match a with
  | .add x y => eval_add (x, y)
  | .val n => n

def eval_add (a : Expr × Expr) : Nat :=
  match a with
  | (x, y) => eval x + eval y
end

namespace VarNames

/-! Test that varnames are inferred nicely. -/

def shadow1 (x2 : Nat) : Nat → Nat
  | 0 => 0
  | .succ n => shadow1 (x2 + 1) n
decreasing_by decreasing_tactic


-- This test is a bit moot since #3081, but lets keep it
def some_n : Nat := 1
def shadow2 (some_n : Nat) : Nat → Nat
  | 0 => 0
  | .succ n => shadow2 (some_n + 1) n
decreasing_by decreasing_tactic

-- Shadowing `sizeOf`, as a varying paramter
def shadowSizeOf1 (sizeOf : Nat) : Nat → Nat
  | 0 => 0
  | .succ n => shadowSizeOf1 (sizeOf + 1) n
decreasing_by decreasing_tactic

-- Shadowing `sizeOf`, as a fixed paramter
def shadowSizeOf2 (sizeOf : Nat) : Nat → Nat → Nat
  | 0, m => m
  | .succ n, m => shadowSizeOf2 sizeOf n m
decreasing_by decreasing_tactic

-- Shadowing `sizeOf`, as something in the environment
def sizeOf : Nat := 2

def qualifiedSizeOf (m : Nat) : Nat → Nat
  | 0 => 0
  | .succ n => qualifiedSizeOf (m + 1) n
decreasing_by decreasing_tactic

end VarNames