{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE ViewPatterns          #-}

module AlgebraCheckers.Theorems where

import Data.Either
import Control.Monad
import Data.Bool
import Data.Char
import Data.Function (on)
import Data.Generics.Schemes (listify)
import Data.List (nub, (\\))
import Data.Maybe (isNothing, fromMaybe, mapMaybe)
import Data.Semigroup
import Language.Haskell.TH hiding (ppr, Arity)
import Language.Haskell.TH.Syntax (Module)
import Prelude hiding (exp)
import AlgebraCheckers.Homos
import AlgebraCheckers.Suggestions
import AlgebraCheckers.Types
import AlgebraCheckers.Unification


sanityCheck :: Module -> Theorem -> Bool
sanityCheck :: Module -> Theorem -> Bool
sanityCheck Module
md = Maybe TheoremProblem -> Bool
forall a. Maybe a -> Bool
isNothing (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

sanityCheck' :: Module -> Theorem -> Maybe TheoremProblem
sanityCheck' :: Module -> Theorem -> Maybe TheoremProblem
sanityCheck' Module
md (Law TheoremSource
_ Exp
lhs Exp
rhs) =
  (TheoremProblem -> Maybe TheoremProblem)
-> (() -> Maybe TheoremProblem)
-> Either TheoremProblem ()
-> Maybe TheoremProblem
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TheoremProblem -> Maybe TheoremProblem
forall a. a -> Maybe a
Just (Maybe TheoremProblem -> () -> Maybe TheoremProblem
forall a b. a -> b -> a
const Maybe TheoremProblem
forall a. Maybe a
Nothing) (Either TheoremProblem () -> Maybe TheoremProblem)
-> Either TheoremProblem () -> Maybe TheoremProblem
forall a b. (a -> b) -> a -> b
$ (Either TheoremProblem ()
 -> Either TheoremProblem () -> Either TheoremProblem ())
-> [Either TheoremProblem ()] -> Either TheoremProblem ()
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Either TheoremProblem ()
-> Either TheoremProblem () -> Either TheoremProblem ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>)
    [ ([Name] -> TheoremProblem) -> [Name] -> Either TheoremProblem ()
forall a a. ([a] -> a) -> [a] -> Either a ()
lift_error (ContradictionReason -> TheoremProblem
Contradiction (ContradictionReason -> TheoremProblem)
-> ([Name] -> ContradictionReason) -> [Name] -> TheoremProblem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> ContradictionReason
UnknownConstructors)
        ([Name] -> Either TheoremProblem ())
-> [Name] -> Either TheoremProblem ()
forall a b. (a -> b) -> a -> b
$ (Exp -> Name) -> [Exp] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(UnboundVarE Name
n) -> Name
n)
        ([Exp] -> [Name]) -> [Exp] -> [Name]
forall a b. (a -> b) -> a -> b
$ (Exp -> Bool) -> (Exp, Exp) -> [Exp]
forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify Exp -> Bool
is_unbound_ctor (Exp
lhs, Exp
rhs)
    , Exp -> Exp -> Either TheoremProblem ()
forall a. Data a => a -> Exp -> Either TheoremProblem ()
ensure_bound_matches Exp
lhs Exp
rhs
    , Exp -> Exp -> Either TheoremProblem ()
forall a. Data a => a -> Exp -> Either TheoremProblem ()
ensure_bound_matches Exp
rhs Exp
lhs
    , Either TheoremProblem ()
-> Either TheoremProblem () -> Bool -> Either TheoremProblem ()
forall a. a -> a -> Bool -> a
bool (TheoremProblem -> Either TheoremProblem ()
forall a b. a -> Either a b
Left (TheoremProblem -> Either TheoremProblem ())
-> TheoremProblem -> Either TheoremProblem ()
forall a b. (a -> b) -> a -> b
$ ContradictionReason -> TheoremProblem
Contradiction ContradictionReason
UnequalValues) (() -> Either TheoremProblem ()
forall a b. b -> Either a b
Right ()) (Bool -> Either TheoremProblem ())
-> Bool -> Either TheoremProblem ()
forall a b. (a -> b) -> a -> b
$
        (Bool -> Bool -> Bool) -> (Exp -> Bool) -> Exp -> Exp -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Bool -> Bool -> Bool
(&&) Exp -> Bool
isFullyMatchable Exp
lhs Exp
rhs Bool -> Bool -> Bool
`implies` Exp -> Exp -> Bool
forall a. Eq a => a -> a -> Bool
(==) Exp
lhs Exp
rhs
    , Either TheoremProblem ()
-> Either TheoremProblem () -> Bool -> Either TheoremProblem ()
forall a. a -> a -> Bool -> a
bool (TheoremProblem -> Either TheoremProblem ()
forall a b. a -> Either a b
Left (TheoremProblem -> Either TheoremProblem ())
-> TheoremProblem -> Either TheoremProblem ()
forall a b. (a -> b) -> a -> b
$ ContradictionReason -> TheoremProblem
Contradiction ContradictionReason
UnequalValues) (() -> Either TheoremProblem ()
forall a b. b -> Either a b
Right ()) (Bool -> Either TheoremProblem ())
-> Bool -> Either TheoremProblem ()
forall a b. (a -> b) -> a -> b
$ Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
True (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$
        (Name -> Name -> Bool) -> Maybe Name -> Maybe Name -> Maybe Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Exp -> Maybe Name
matchableAppHead Exp
lhs) (Exp -> Maybe Name
matchableAppHead Exp
rhs)
    , Either TheoremProblem ()
-> Either TheoremProblem () -> Bool -> Either TheoremProblem ()
forall a. a -> a -> Bool -> a
bool (() -> Either TheoremProblem ()
forall a b. b -> Either a b
Right ()) (TheoremProblem -> Either TheoremProblem ()
forall a b. a -> Either a b
Left (TheoremProblem -> Either TheoremProblem ())
-> TheoremProblem -> Either TheoremProblem ()
forall a b. (a -> b) -> a -> b
$ DodgyReason -> TheoremProblem
Dodgy DodgyReason
SelfRecursive) (Bool -> Either TheoremProblem ())
-> Bool -> Either TheoremProblem ()
forall a b. (a -> b) -> a -> b
$ Module -> Exp -> Exp -> Bool
nonlinearUse Module
md Exp
lhs Exp
rhs
    , Either TheoremProblem ()
-> Either TheoremProblem () -> Bool -> Either TheoremProblem ()
forall a. a -> a -> Bool -> a
bool (() -> Either TheoremProblem ()
forall a b. b -> Either a b
Right ()) (TheoremProblem -> Either TheoremProblem ()
forall a b. a -> Either a b
Left (TheoremProblem -> Either TheoremProblem ())
-> TheoremProblem -> Either TheoremProblem ()
forall a b. (a -> b) -> a -> b
$ DodgyReason -> TheoremProblem
Dodgy DodgyReason
SelfRecursive) (Bool -> Either TheoremProblem ())
-> Bool -> Either TheoremProblem ()
forall a b. (a -> b) -> a -> b
$ Module -> Exp -> Exp -> Bool
nonlinearUse Module
md Exp
rhs Exp
lhs
    ]
  where
    is_unbound_ctor :: Exp -> Bool
is_unbound_ctor (UnboundVarE Name
n) = Char -> Bool
isUpper (Char -> Bool) -> ([Char] -> Char) -> [Char] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Char
forall a. [a] -> a
head ([Char] -> Bool) -> [Char] -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> [Char]
nameBase Name
n
    is_unbound_ctor Exp
_ = Bool
False

    ensure_bound_matches :: a -> Exp -> Either TheoremProblem ()
ensure_bound_matches a
a Exp
b
      = ([Name] -> TheoremProblem) -> [Name] -> Either TheoremProblem ()
forall a a. ([a] -> a) -> [a] -> Either a ()
lift_error (ContradictionReason -> TheoremProblem
Contradiction (ContradictionReason -> TheoremProblem)
-> ([Name] -> ContradictionReason) -> [Name] -> TheoremProblem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> ContradictionReason
UnboundMatchableVars)
      ([Name] -> Either TheoremProblem ())
-> [Name] -> Either TheoremProblem ()
forall a b. (a -> b) -> a -> b
$ (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Name -> Bool) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Name -> Bool
forall a a. (Eq a, Data a, Typeable a) => a -> a -> Bool
exists_in a
a)
      ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Exp -> [Name]
matchableMetaVars Exp
b
    lift_error :: ([a] -> a) -> [a] -> Either a ()
lift_error [a] -> a
_ [] = () -> Either a ()
forall a b. b -> Either a b
Right ()
    lift_error [a] -> a
ctor [a]
x = a -> Either a ()
forall a b. a -> Either a b
Left (a -> Either a ()) -> a -> Either a ()
forall a b. (a -> b) -> a -> b
$ [a] -> a
ctor [a]
x
    exists_in :: a -> a -> Bool
exists_in a
exp a
var = Bool -> Bool
not (Bool -> Bool) -> ([a] -> Bool) -> [a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([a] -> Bool) -> [a] -> Bool
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> a -> [a]
forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
var) a
exp

implies :: Bool -> Bool -> Bool
implies :: Bool -> Bool -> Bool
implies Bool
p Bool
q = Bool -> Bool
not Bool
p Bool -> Bool -> Bool
|| Bool
q

matchableMetaVars :: Exp -> [Name]
matchableMetaVars :: Exp -> [Name]
matchableMetaVars (UnboundVarE Name
n) = [Name
n]
matchableMetaVars Exp
e =
  case Exp -> Maybe Name
matchableAppHead Exp
e of
    Just Name
_ -> Exp -> [Name]
go Exp
e
    Maybe Name
Nothing -> []
  where
    go :: Exp -> [Name]
go (Exp
exp1 `AppE` Exp
exp2) =
      Exp -> [Name]
go Exp
exp1 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Exp -> [Name]
matchableMetaVars Exp
exp2
    go Exp
_ = []

isFullyMatchable :: Exp -> Bool
isFullyMatchable :: Exp -> Bool
isFullyMatchable (ConE Name
_)                      = Bool
True
isFullyMatchable (TupE ([Maybe Exp] -> Maybe [Exp]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA -> Just [Exp]
es)) = (Exp -> Bool) -> [Exp] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Exp -> Bool
isFullyMatchable [Exp]
es
isFullyMatchable (ListE [Exp]
es)                    = (Exp -> Bool) -> [Exp] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Exp -> Bool
isFullyMatchable [Exp]
es
isFullyMatchable (LitE Lit
_)                      = Bool
True
isFullyMatchable (UnboundVarE Name
_)               = Bool
True
isFullyMatchable (AppE (UnboundVarE Name
_) Exp
_)      = Bool
False
isFullyMatchable (AppE Exp
exp1 Exp
exp2)              = Exp -> Bool
isFullyMatchable Exp
exp1 Bool -> Bool -> Bool
&& Exp -> Bool
isFullyMatchable Exp
exp2
isFullyMatchable Exp
_                             = Bool
False

namedLawToEither :: NamedLaw -> Either (Law ()) (Law String)
namedLawToEither :: NamedLaw -> Either (Law ()) (Law [Char])
namedLawToEither (Law (LawName [Char]
n) Exp
a Exp
b) = Law [Char] -> Either (Law ()) (Law [Char])
forall a b. b -> Either a b
Right ([Char] -> Exp -> Exp -> Law [Char]
forall a. a -> Exp -> Exp -> Law a
Law [Char]
n Exp
a Exp
b)
namedLawToEither (Law LawSort
LawNotDodgy Exp
a Exp
b) = Law () -> Either (Law ()) (Law [Char])
forall a b. a -> Either a b
Left (() -> Exp -> Exp -> Law ()
forall a. a -> Exp -> Exp -> Law a
Law () Exp
a Exp
b)

theorize :: Module -> [NamedLaw] -> [Theorem]
theorize :: Module -> [NamedLaw] -> [Theorem]
theorize Module
md [NamedLaw]
named_laws =
  let ([Law ()]
not_dodgy, [Law [Char]]
laws) = [Either (Law ()) (Law [Char])] -> ([Law ()], [Law [Char]])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either (Law ()) (Law [Char])] -> ([Law ()], [Law [Char]]))
-> [Either (Law ()) (Law [Char])] -> ([Law ()], [Law [Char]])
forall a b. (a -> b) -> a -> b
$ (NamedLaw -> Either (Law ()) (Law [Char]))
-> [NamedLaw] -> [Either (Law ()) (Law [Char])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedLaw -> Either (Law ()) (Law [Char])
namedLawToEither [NamedLaw]
named_laws
      law_defs :: [Theorem]
law_defs = (Law [Char] -> Theorem) -> [Law [Char]] -> [Theorem]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Law [Char]
t -> Law [Char]
t { lawData :: TheoremSource
lawData = [Char] -> TheoremSource
LawDefn ([Char] -> TheoremSource) -> [Char] -> TheoremSource
forall a b. (a -> b) -> a -> b
$ Law [Char] -> [Char]
forall a. Law a -> a
lawData Law [Char]
t }) [Law [Char]]
laws
      sane_laws :: [Theorem]
sane_laws = (Theorem -> Bool) -> [Theorem] -> [Theorem]
forall a. (a -> Bool) -> [a] -> [a]
filter (Module -> Theorem -> Bool
sanityCheck Module
md) [Theorem]
law_defs
      theorems :: [Theorem]
theorems = do
         l1 :: Theorem
l1@Law{lawData :: forall a. Law a -> a
lawData = LawDefn [Char]
l1name} <- [Theorem]
sane_laws
         l2 :: Theorem
l2@Law{lawData :: forall a. Law a -> a
lawData = LawDefn [Char]
l2name} <- [Theorem]
sane_laws
         Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Theorem
l1 Theorem -> Theorem -> Bool
forall a. Eq a => a -> a -> Bool
/= Theorem
l2
         (Exp
lhs, Exp
rhs) <- Theorem -> Theorem -> [(Exp, Exp)]
forall a. Law a -> Law a -> [(Exp, Exp)]
criticalPairs Theorem
l1 Theorem
l2
         Theorem -> [Theorem]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Theorem -> [Theorem]) -> Theorem -> [Theorem]
forall a b. (a -> b) -> a -> b
$ TheoremSource -> Exp -> Exp -> Theorem
forall a. a -> Exp -> Exp -> Law a
Law ([Char] -> [Char] -> TheoremSource
Interaction [Char]
l1name [Char]
l2name) Exp
lhs Exp
rhs
   in ([Theorem] -> [Theorem]
forall a. Eq a => [a] -> [a]
nub ([Theorem] -> [Theorem]) -> [Theorem] -> [Theorem]
forall a b. (a -> b) -> a -> b
$ [Theorem]
law_defs [Theorem] -> [Theorem] -> [Theorem]
forall a. Semigroup a => a -> a -> a
<> [Theorem]
theorems) [Theorem] -> [Theorem] -> [Theorem]
forall a. Eq a => [a] -> [a] -> [a]
\\ (Law () -> Theorem) -> [Law ()] -> [Theorem]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Law ()
l -> Law ()
l {lawData :: TheoremSource
lawData = [Char] -> TheoremSource
LawDefn [Char]
""} ) [Law ()]
not_dodgy

matchableAppHead :: Exp -> Maybe Name
matchableAppHead :: Exp -> Maybe Name
matchableAppHead (ConE Name
n)   = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
matchableAppHead (AppE Exp
f Exp
_) = Exp -> Maybe Name
matchableAppHead Exp
f
matchableAppHead Exp
_          = Maybe Name
forall a. Maybe a
Nothing

nonlinearUse :: Module -> Exp -> Exp -> Bool
nonlinearUse :: Module -> Exp -> Exp -> Bool
nonlinearUse Module
md Exp
exp1 Exp
exp2 =
  let exp2s :: [(Name, [Exp])]
exp2s = (Exp -> Maybe (Name, [Exp])) -> [Exp] -> [(Name, [Exp])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\Exp
exp -> Exp -> Maybe (Name, [Exp])
splitApps Exp
exp) ([Exp] -> [(Name, [Exp])]) -> [Exp] -> [(Name, [Exp])]
forall a b. (a -> b) -> a -> b
$ (SubExp -> Exp) -> [SubExp] -> [Exp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SubExp -> Exp
seExp ([SubExp] -> [Exp]) -> [SubExp] -> [Exp]
forall a b. (a -> b) -> a -> b
$ Exp -> [SubExp]
subexps Exp
exp2
   in ((Name, [Exp]) -> Bool) -> [(Name, [Exp])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(Name
apphead, [Exp]
exps) -> Module -> Name -> Bool
nonlinearFunc Module
md Name
apphead Bool -> Bool -> Bool
&& (Exp -> Bool) -> [Exp] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Exp -> Exp -> Bool
equalUpToAlpha Exp
exp1) [Exp]
exps) [(Name, [Exp])]
exp2s

nonlinearFunc :: Module -> Name -> Bool
nonlinearFunc :: Module -> Name -> Bool
nonlinearFunc Module
md Name
name = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Module -> Name -> Bool
sameModule Module
md Name
name