module Tests.Reduce

import Quox.Syntax as Lib
import TermImpls
import TAP


testWhnf : (Eq b, Show b) => (a -> (Subset b _)) ->
           String -> a -> b -> Test
testWhnf whnf label from to = test "\{label}  (whnf)" $
  let result = fst (whnf from) in
  if result == to
     then Right ()
     else with Prelude.(::)
          Left [("expected", to), ("received", result)]

testNoStep : forall p. Show a => ((x : a) -> Either (p x) a) ->
            String -> a -> Test
testNoStep step label e = test "\{label}  (no step)" $
  case step e of
       Left  _  => Right ()
       Right e' => with Prelude.(::) Left [("reduced", e')]


parameters {default 0 d, n : Nat}
  testWhnfT : String -> Term d n -> Term d n -> Test
  testWhnfT = testWhnf whnfT

  testWhnfE : String -> Elim d n -> Elim d n -> Test
  testWhnfE = testWhnf whnfE

  testNoStepE : String -> Elim d n -> Test
  testNoStepE = testNoStep stepE

  testNoStepT : String -> Term d n -> Test
  testNoStepT = testNoStep stepT


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

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

  "redexes" :- [
    testWhnfE "[a] ∷ [A]"
      (FT "a" :# FT "A")
      (F "a"),
    testWhnfT "[★₁ ∷ ★₃]"
      (E (TYPE 1 :# TYPE 3))
      (TYPE 1),
    testWhnfE "(λx. [x] ∷ [A] ⊸ [A]) [a]"
      ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
      (F "a")
  ],

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

  "term closure" :- [
    testWhnfT "(λy. x){a/x}"
      (CloT (Lam "x" $ TUnused $ BVT 0) (F "a" ::: id))
      (Lam "x" $ TUnused $ FT "a")
  ],

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

  "nested redex" :- [
    note "whnf only looks at top level redexes",
    testNoStepT "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" $
      Lam "y" $ TUsed $ E $
        (Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0,
    testNoStepE "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
      F "a" :@
      E ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
  ]
]