module Tests.Reduce

import Quox.Syntax as Lib
import Quox.Syntax.Qty.Three
import Quox.Equal
import TermImpls
import TypingImpls
import TAP


parameters {0 isRedex : RedexTest tm} {auto _ : Whnf tm isRedex err}
           {auto _ : ToInfo err}
           {auto _ : forall d, n. Eq   (tm Three d n)}
           {auto _ : forall d, n. Show (tm Three d n)}
           {default empty defs : Definitions Three}
           {default 0 d, n : Nat}
  testWhnf : String -> tm Three d n -> tm Three d n -> Test
  testWhnf label from to = test "\{label}  (whnf)" $ do
    result <- bimap toInfo fst $ whnf defs from
    unless (result == to) $ Left [("exp", show to), ("got", show result)]

  testNoStep : String -> tm Three d n -> Test
  testNoStep label e = testWhnf label e e


tests = "whnf" :- [
  "head constructors" :- [
    testNoStep "★₀" $ TYPE 0,
    testNoStep "[A] ⊸ [B]" $
      Arr One (FT "A") (FT "B"),
    testNoStep "(x: [A]) ⊸ [B [x]]" $
      Pi One (FT "A") (S [< "x"] $ Y $ E $ F "B" :@ BVT 0),
    testNoStep "λx. [x]" $
      Lam $ S [< "x"] $ Y $ BVT 0,
    testNoStep "[f [a]]" $
      E $ F "f" :@ FT "a"
  ],

  "neutrals" :- [
    testNoStep "x" {n = 1} $ BV 0,
    testNoStep "a"         $ F "a",
    testNoStep "f [a]"     $ F "f" :@ FT "a",
    testNoStep "★₀ ∷ ★₁"   $ TYPE 0 :# TYPE 1
  ],

  "redexes" :- [
    testWhnf "[a] ∷ [A]"
      (FT "a" :# FT "A")
      (F "a"),
    testWhnf "[★₁ ∷ ★₃]"
      (E (TYPE 1 :# TYPE 3))
      (TYPE 1),
    testWhnf "(λx. [x] ∷ [A] ⊸ [A]) [a]"
      ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
      (F "a")
  ],

  "definitions" :- [
    testWhnf "a  (transparent)"
      {defs = fromList [("a", mkDef Zero (TYPE 1) (TYPE 0))]}
      (F "a") (TYPE 0 :# TYPE 1)
  ],

  "elim closure" :- [
    testWhnf "x{}" {n = 1}
      (CloE (BV 0) id)
      (BV 0),
    testWhnf "x{a/x}"
      (CloE (BV 0) (F "a" ::: id))
      (F "a"),
    testWhnf "x{x/x,a/y}" {n = 1}
      (CloE (BV 0) (BV 0 ::: F "a" ::: id))
      (BV 0),
    testWhnf "x{(y{a/y})/x}"
      (CloE (BV 0) ((CloE (BV 0) (F "a" ::: id)) ::: id))
      (F "a"),
    testWhnf "(x y){f/x,a/y}"
      (CloE (BV 0 :@ BVT 1) (F "f" ::: F "a" ::: id))
      (F "f" :@ FT "a"),
    testWhnf "([y] ∷ [x]){A/x}" {n = 1}
      (CloE (BVT 1 :# BVT 0) (F "A" ::: id))
      (BV 0),
    testWhnf "([y] ∷ [x]){A/x,a/y}"
      (CloE (BVT 1 :# BVT 0) (F "A" ::: F "a" ::: id))
      (F "a")
  ],

  "term closure" :- [
    testWhnf "(λy. x){a/x}"
      (CloT (Lam $ S [< "y"] $ N $ BVT 0) (F "a" ::: id))
      (Lam $ S [< "y"] $ N $ FT "a"),
    testWhnf "(λy. y){a/x}"
      (CloT ([< "y"] :\\ BVT 0) (F "a" ::: id))
      ([< "y"] :\\ BVT 0)
  ],

  "looking inside […]" :- [
    testWhnf "[(λx. x ∷ A ⊸ A) [a]]"
      (E $ (([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
      (FT "a")
  ],

  "nested redex" :- [
    note "whnf only looks at top level redexes",
    testNoStep "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" $
      [< "y"] :\\ E ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0),
    testNoStep "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
      F "a" :@
      E ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
    testNoStep "λx. [y [x]]{x/x,a/y}" {n = 1} $
      [< "x"] :\\ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
    testNoStep "f ([y [x]]{x/x,a/y})" {n = 1} $
      F "f" :@ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id)
  ]
]