{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_HADDOCK not-home #-}

module AlgebraCheckers.TH where

import AlgebraCheckers.Homos
import AlgebraCheckers.Patterns
import AlgebraCheckers.Ppr
import AlgebraCheckers.Theorems
import AlgebraCheckers.Types
import AlgebraCheckers.Unification
import Control.Monad
import Data.Bool
import Data.List (nub, partition)
import Data.Traversable
import Language.Haskell.TH hiding (ppr, Arity)
import Language.Haskell.TH.Syntax (lift, Module)
import Prelude hiding (exp)
import Test.QuickCheck hiding (collect)
import Test.QuickCheck.Checkers ((=-=))


showTheorem :: Module -> Theorem -> Doc
showTheorem md thm =
  case sanityCheck' md thm of
    Just contradiction ->
      showContradictoryTheorem thm contradiction
    Nothing -> showSaneTheorem thm

propTestEq :: Theorem -> ExpQ
propTestEq t@(Law _ exp1 exp2) = do
  md <- thisModule
  let vars = nub $ unboundVars exp1 ++ unboundVars exp2
  names <- for vars $ newName . nameBase
  [e|
    counterexample $(lift $ render $ showTheorem md t) $
      property $(lamE (fmap varP names) [e|
       $(pure exp1) =-= $(pure exp2)
      |])
    |]


------------------------------------------------------------------------------
-- | Generate QuickCheck property tests for the given model.
--
-- ==== __Examples__
--
-- @
--   lawTests :: ['Test.QuickCheck.Property']
--   lawTests = $('theoremsOf' [e| do
--
--   'AlgebraCheckers.law' "commutativity" $ a '+' b '==' b '+' a
--   'AlgebraCheckers.law' "identity" (a '+' 0 '==' a)
--
--   |])
-- @
testModel :: ExpQ -> ExpQ
testModel = (testModelImpl =<<)

testModelImpl :: Exp -> ExpQ
testModelImpl e = do
  m <- thisModule
  listE . fmap propTestEq . theorize m $ parseLaws e

parseLaws :: Exp -> [Law LawSort]
parseLaws (DoE z) = concatMap collect z
parseLaws _ = error "you must call parseLaws with a do block"

------------------------------------------------------------------------------
-- | Like 'testModel', but also interactively dumps all of the derived theorems
-- of your model. This is very helpful for finding dodgy derivations and
-- outright contradictions.
theoremsOf :: ExpQ -> ExpQ
theoremsOf = (theoremsOfImpl =<<)

theoremsOfImpl :: Exp -> ExpQ
theoremsOfImpl z = do
  md <- thisModule
  let (theorems, problems) = partition (sanityCheck md) $ theorize md $ parseLaws z
      contradicts = filter (maybe False isContradiction . sanityCheck' md) problems
      dodgy       = filter (maybe False isDodgy . sanityCheck' md) problems
  runIO $ do
    putStrLn ""
    printStuff md "Theorems"       theorems
    printStuff md "Dodgy Theorems" dodgy
    printStuff md "Contradictions" contradicts
  listE $ fmap propTestEq $ theorems ++ dodgy ++ contradicts

printStuff :: Module -> String -> [Theorem] -> IO ()
printStuff md sort laws =
  when (not $ null laws) $ do
    putStrLn . render
             $ sep
             $ text (sort ++ ":") : text "" : fmap (showTheorem md) laws
    putStrLn ""
    putStrLn ""

collect :: Stmt -> [Law LawSort]
collect (LawDef lawname exp1 exp2) = [Law (LawName lawname) exp1 exp2]
collect (NotDodgyDef exp1 exp2)    = [Law LawNotDodgy exp1 exp2]
collect (HomoDef ty expr)          = makeHomo ty (knownHomos ty) expr
collect x = error $ show x
  -- "collect must be called with the form [e| law \"name\" (foo a b c == bar a d e) |]"