{-# 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 :: Module -> Theorem -> Doc
showTheorem Module
md Theorem
thm =
  case Module -> Theorem -> Maybe TheoremProblem
sanityCheck' Module
md Theorem
thm of
    Just TheoremProblem
contradiction ->
      Theorem -> TheoremProblem -> Doc
showContradictoryTheorem Theorem
thm TheoremProblem
contradiction
    Maybe TheoremProblem
Nothing -> Theorem -> Doc
showSaneTheorem Theorem
thm

propTestEq :: Theorem -> ExpQ
propTestEq :: Theorem -> ExpQ
propTestEq t :: Theorem
t@(Law TheoremSource
_ Exp
exp1 Exp
exp2) = do
  Module
md <- Q Module
thisModule
  let vars :: [Name]
vars = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Exp -> [Name]
unboundVars Exp
exp1 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Exp -> [Name]
unboundVars Exp
exp2
  [Name]
names <- [Name] -> (Name -> Q Name) -> Q [Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
vars ((Name -> Q Name) -> Q [Name]) -> (Name -> Q Name) -> Q [Name]
forall a b. (a -> b) -> a -> b
$ String -> Q Name
newName (String -> Q Name) -> (Name -> String) -> Name -> Q Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
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 :: ExpQ -> ExpQ
testModel = (Exp -> ExpQ
testModelImpl (Exp -> ExpQ) -> ExpQ -> ExpQ
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<)

testModelImpl :: Exp -> ExpQ
testModelImpl :: Exp -> ExpQ
testModelImpl Exp
e = do
  Module
m <- Q Module
thisModule
  [ExpQ] -> ExpQ
listE ([ExpQ] -> ExpQ) -> ([NamedLaw] -> [ExpQ]) -> [NamedLaw] -> ExpQ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Theorem -> ExpQ) -> [Theorem] -> [ExpQ]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Theorem -> ExpQ
propTestEq ([Theorem] -> [ExpQ])
-> ([NamedLaw] -> [Theorem]) -> [NamedLaw] -> [ExpQ]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> [NamedLaw] -> [Theorem]
theorize Module
m ([NamedLaw] -> ExpQ) -> [NamedLaw] -> ExpQ
forall a b. (a -> b) -> a -> b
$ Exp -> [NamedLaw]
parseLaws Exp
e

parseLaws :: Exp -> [Law LawSort]
parseLaws :: Exp -> [NamedLaw]
parseLaws (DoE [Stmt]
z) = (Stmt -> [NamedLaw]) -> [Stmt] -> [NamedLaw]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Stmt -> [NamedLaw]
collect [Stmt]
z
parseLaws Exp
_ = String -> [NamedLaw]
forall a. HasCallStack => String -> a
error String
"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 :: ExpQ -> ExpQ
theoremsOf = (Exp -> ExpQ
theoremsOfImpl (Exp -> ExpQ) -> ExpQ -> ExpQ
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<)

theoremsOfImpl :: Exp -> ExpQ
theoremsOfImpl :: Exp -> ExpQ
theoremsOfImpl Exp
z = do
  Module
md <- Q Module
thisModule
  let ([Theorem]
theorems, [Theorem]
problems) = (Theorem -> Bool) -> [Theorem] -> ([Theorem], [Theorem])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Module -> Theorem -> Bool
sanityCheck Module
md) ([Theorem] -> ([Theorem], [Theorem]))
-> [Theorem] -> ([Theorem], [Theorem])
forall a b. (a -> b) -> a -> b
$ Module -> [NamedLaw] -> [Theorem]
theorize Module
md ([NamedLaw] -> [Theorem]) -> [NamedLaw] -> [Theorem]
forall a b. (a -> b) -> a -> b
$ Exp -> [NamedLaw]
parseLaws Exp
z
      contradicts :: [Theorem]
contradicts = (Theorem -> Bool) -> [Theorem] -> [Theorem]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> (TheoremProblem -> Bool) -> Maybe TheoremProblem -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False TheoremProblem -> Bool
isContradiction (Maybe TheoremProblem -> Bool)
-> (Theorem -> Maybe TheoremProblem) -> Theorem -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> Theorem -> Maybe TheoremProblem
sanityCheck' Module
md) [Theorem]
problems
      dodgy :: [Theorem]
dodgy       = (Theorem -> Bool) -> [Theorem] -> [Theorem]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> (TheoremProblem -> Bool) -> Maybe TheoremProblem -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False TheoremProblem -> Bool
isDodgy (Maybe TheoremProblem -> Bool)
-> (Theorem -> Maybe TheoremProblem) -> Theorem -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> Theorem -> Maybe TheoremProblem
sanityCheck' Module
md) [Theorem]
problems
  IO () -> Q ()
forall a. IO a -> Q a
runIO (IO () -> Q ()) -> IO () -> Q ()
forall a b. (a -> b) -> a -> b
$ do
    String -> IO ()
putStrLn String
""
    Module -> String -> [Theorem] -> IO ()
printStuff Module
md String
"Theorems"       [Theorem]
theorems
    Module -> String -> [Theorem] -> IO ()
printStuff Module
md String
"Dodgy Theorems" [Theorem]
dodgy
    Module -> String -> [Theorem] -> IO ()
printStuff Module
md String
"Contradictions" [Theorem]
contradicts
  [ExpQ] -> ExpQ
listE ([ExpQ] -> ExpQ) -> [ExpQ] -> ExpQ
forall a b. (a -> b) -> a -> b
$ (Theorem -> ExpQ) -> [Theorem] -> [ExpQ]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Theorem -> ExpQ
propTestEq ([Theorem] -> [ExpQ]) -> [Theorem] -> [ExpQ]
forall a b. (a -> b) -> a -> b
$ [Theorem]
theorems [Theorem] -> [Theorem] -> [Theorem]
forall a. [a] -> [a] -> [a]
++ [Theorem]
dodgy [Theorem] -> [Theorem] -> [Theorem]
forall a. [a] -> [a] -> [a]
++ [Theorem]
contradicts

printStuff :: Module -> String -> [Theorem] -> IO ()
printStuff :: Module -> String -> [Theorem] -> IO ()
printStuff Module
md String
sort [Theorem]
laws =
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Theorem] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Theorem]
laws) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    String -> IO ()
putStrLn (String -> IO ()) -> (Doc -> String) -> Doc -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
render
             (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep
             ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String
sort String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":") Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: String -> Doc
text String
"" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Theorem -> Doc) -> [Theorem] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Module -> Theorem -> Doc
showTheorem Module
md) [Theorem]
laws
    String -> IO ()
putStrLn String
""
    String -> IO ()
putStrLn String
""

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