content: -- |
  -- Module      : LCQC
  -- Description : Generators for well-scoped lambda calculus terms
  -- Stability   : experimental
  --
  -- This module demonstrates the use of well-scoped lambda calculus terms
  -- with QuickCheck. It then demonstrates how to use QC to test the normalization
  -- functions in the `LC` module.
  module LCQC where
  
  import LC
  import Test.QuickCheck
  import Rebound
  import Rebound.Bind.Single
  import Data.Fin
  import Data.Maybe as Maybe
  
  ----------------------------------------------
  -- Generating well-scoped expressions
  ----------------------------------------------
  
  -- | Generate an expression in scope `n`, using
  -- size parameter sz
  -- >>> sample' (genExp s3 10)
  -- [(λ. (λ. (0 2))),(((λ. 0) (1 2)) ((0 2) 2)),(((2 1) 0) (1 1)),1,((λ. 2) (2 (λ. 1))),(λ. 2),2,0,((λ. (0 1)) (λ. (1 3))),(((1 2) 2) (λ. (0 2))),(λ. 2)]
  genExp :: forall n. SNat n -> Int -> Gen (Exp n)
  genExp n sz =
      let
          genLam = Lam <$> (bind <$> genExp (next n) (sz `div` 2))
          genApp = App <$> genExp n (sz `div` 2) <*> genExp n (sz `div` 2)
      in
      case snat_ n of
         SZ_ -> if sz <= 1
                  then pure $ Lam (bind (Var 0))  -- smallest closed term
                  else oneof [genLam, genApp]     -- closed term, no vars
         SS_ x ->
           let
              genVar = withSNat x $ elements $ map Var universe
           in
              if sz <= 1
                then genVar
                else oneof [genVar, genLam, genApp]
  
  -- | shrink a lambda calculus term, maintaining the same scope.
  shrinkExp :: SNatI n => Exp n -> [Exp n]
  shrinkExp (Var FZ) = []
  shrinkExp (Var x ) = [ Var (pred x) ]
  shrinkExp (Lam t)  = [ Lam (bind t') | t' <- shrinkExp (getBody t) ]
  shrinkExp (App f a) =
    [f,a] ++ [ App f' a | f' <- shrinkExp f]
          ++ [ App f a' | a' <- shrinkExp a]
  
  -- | arbitrary instance for lambda calculus terms
  instance SNatI n => Arbitrary (Exp n) where
    arbitrary :: SNatI n => Gen (Exp n)
    arbitrary = sized (genExp snat)
    shrink :: SNatI n => Exp n -> [Exp n]
    shrink = shrinkExp
  
  
  ----------------------------------------------
  -- Property-based testing example
  ----------------------------------------------
  
  {-
  
  Let's use QuickCheck to make sure that our various
  normalization functions for the lambda calculus all produce the
  same result.
  
  However, we need to deal with the fact that not all lambda
  calculus terms normalize. Therefore, we will instruct QC to discard
  the test case if the expression does not normalize within 0.1 seconds.
  We will also discard expressions that are already in normal form.
  -}
  
  prop_normalize :: (Exp n -> Exp n) -> Exp n -> Property
  prop_normalize f e = discardAfter 100000 $
      e /= e' ==> e' == f e
     where e' = nf e
  
  prop_nf1 :: Exp Z -> Property
  prop_nf1 = prop_normalize nf1
  
  prop_nfEnv :: Exp Z -> Property
  prop_nfEnv = prop_normalize nfEnv
  