{-# 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)
|])
|]
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"
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