{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE ViewPatterns          #-}

{-# OPTIONS_HADDOCK not-home #-}

module AlgebraCheckers.Patterns where

import Language.Haskell.TH hiding (ppr, Arity)

pattern NotDodgyParens :: Exp -> Exp -> Stmt
pattern $mNotDodgyParens :: forall r. Stmt -> (Exp -> Exp -> r) -> (Void# -> r) -> r
NotDodgyParens exp1 exp2 <- NoBindS
  (      VarE ((==) 'notDodgy -> True)
  `AppE` (InfixE (Just exp1)
                 (VarE ((==) '(==) -> True))
                 (Just exp2)
         )
  )

pattern NotDodgyDollar :: Exp -> Exp -> Stmt
pattern $mNotDodgyDollar :: forall r. Stmt -> (Exp -> Exp -> r) -> (Void# -> r) -> r
NotDodgyDollar exp1 exp2 <- NoBindS
  (InfixE
    (Just ( VarE ((==) 'notDodgy -> True)))
    (VarE ((==) '($) -> True))
    (Just (InfixE (Just exp1)
                  (VarE ((==) '(==) -> True))
                  (Just exp2)
          )
    )
  )

matchNotDodgy :: Stmt -> Maybe (Exp, Exp)
matchNotDodgy :: Stmt -> Maybe (Exp, Exp)
matchNotDodgy (NotDodgyParens Exp
exp1 Exp
exp2) = (Exp, Exp) -> Maybe (Exp, Exp)
forall a. a -> Maybe a
Just (Exp
exp1, Exp
exp2)
matchNotDodgy (NotDodgyDollar Exp
exp1 Exp
exp2) = (Exp, Exp) -> Maybe (Exp, Exp)
forall a. a -> Maybe a
Just (Exp
exp1, Exp
exp2)
matchNotDodgy Stmt
_ = Maybe (Exp, Exp)
forall a. Maybe a
Nothing

pattern NotDodgyDef :: Exp -> Exp -> Stmt
pattern $mNotDodgyDef :: forall r. Stmt -> (Exp -> Exp -> r) -> (Void# -> r) -> r
NotDodgyDef exp1 exp2 <- (matchNotDodgy -> Just (exp1, exp2))


pattern LawParens :: String -> Exp -> Exp -> Stmt
pattern $mLawParens :: forall r. Stmt -> (String -> Exp -> Exp -> r) -> (Void# -> r) -> r
LawParens lawname exp1 exp2 <- NoBindS
  (      VarE ((==) 'law -> True)
  `AppE` LitE  (StringL lawname)
  `AppE` (InfixE (Just exp1)
                 (VarE ((==) '(==) -> True))
                 (Just exp2)
         )
  )

pattern LawDollar :: String -> Exp -> Exp -> Stmt
pattern $mLawDollar :: forall r. Stmt -> (String -> Exp -> Exp -> r) -> (Void# -> r) -> r
LawDollar lawname exp1 exp2 <- NoBindS
  (InfixE
    (Just (  VarE ((==) 'law -> True)
      `AppE` LitE  (StringL lawname)))
    (VarE ((==) '($) -> True))
    (Just (InfixE (Just exp1)
                  (VarE ((==) '(==) -> True))
                  (Just exp2)
          )
    )
  )

matchLaw :: Stmt -> Maybe (String, Exp, Exp)
matchLaw :: Stmt -> Maybe (String, Exp, Exp)
matchLaw (LawParens String
name Exp
exp1 Exp
exp2) = (String, Exp, Exp) -> Maybe (String, Exp, Exp)
forall a. a -> Maybe a
Just (String
name, Exp
exp1, Exp
exp2)
matchLaw (LawDollar String
name Exp
exp1 Exp
exp2) = (String, Exp, Exp) -> Maybe (String, Exp, Exp)
forall a. a -> Maybe a
Just (String
name, Exp
exp1, Exp
exp2)
matchLaw Stmt
_ = Maybe (String, Exp, Exp)
forall a. Maybe a
Nothing

pattern LawDef :: String -> Exp -> Exp -> Stmt
pattern $mLawDef :: forall r. Stmt -> (String -> Exp -> Exp -> r) -> (Void# -> r) -> r
LawDef name exp1 exp2 <- (matchLaw -> Just (name, exp1, exp2))


pattern HomoParens :: Name -> Exp -> Stmt
pattern $mHomoParens :: forall r. Stmt -> (Name -> Exp -> r) -> (Void# -> r) -> r
HomoParens ty expr <- NoBindS
  (      (VarE ((==) 'homo -> True) `AppTypeE` ConT ty)
  `AppE` expr
  )

pattern HomoDollar :: Name -> Exp -> Stmt
pattern $mHomoDollar :: forall r. Stmt -> (Name -> Exp -> r) -> (Void# -> r) -> r
HomoDollar ty expr <- NoBindS
  (InfixE
    (Just ((VarE ((==) 'homo -> True) `AppTypeE` ConT ty)))
    (VarE ((==) '($) -> True))
    (Just expr)
  )

matchHomo :: Stmt -> Maybe (Name, Exp)
matchHomo :: Stmt -> Maybe (Name, Exp)
matchHomo (HomoParens Name
ty Exp
expr) = (Name, Exp) -> Maybe (Name, Exp)
forall a. a -> Maybe a
Just (Name
ty, Exp
expr)
matchHomo (HomoDollar Name
ty Exp
expr) = (Name, Exp) -> Maybe (Name, Exp)
forall a. a -> Maybe a
Just (Name
ty, Exp
expr)
matchHomo Stmt
_ = Maybe (Name, Exp)
forall a. Maybe a
Nothing


pattern HomoDef :: Name -> Exp -> Stmt
pattern $mHomoDef :: forall r. Stmt -> (Name -> Exp -> r) -> (Void# -> r) -> r
HomoDef ty expr <- (matchHomo -> Just (ty, expr))


------------------------------------------------------------------------------
-- | Asserts that an algebraic law must hold. This function /must/ be called
-- only in the context of either 'AlgebraCheckers.testModel' or
-- 'AlgebraCheckers.theoremsOf'.
--
-- Any variables that appear in the 'Bool' parameter are considered to be
-- metavariables, and will be varied in the resulting property test.
--
-- The 'Bool' parameter /must/ be an expression of the form @exp1 '==' exp2@
--
-- ==== __Examples__
--
-- @'law' "set/get" $ set x (get x s) '==' s@
--
-- @'law' "set/set" (set x' (set x s) '==' set x' s)@
law
    :: String  -- ^ Name
    -> Bool    -- ^ Law. /This is not any ordinary 'Bool'!/ See the documentation
               -- on 'law' for more information.
    -> law
law :: String -> Bool -> law
law =
  String -> String -> Bool -> law
forall a. HasCallStack => String -> a
error String
"law may be called only inside of a call to testModel or theoremsOf"


------------------------------------------------------------------------------
-- | Convinces 'AlgebraCheckers.theoremsOf' that the following law is not dodgy,
-- preventing it from appearing in the dodgy theorems list.
--
-- This function does not introduce a new law.
--
-- This function /must/ be called only in the context of either
-- 'AlgebraCheckers.testModel' or 'AlgebraCheckers.theoremsOf'.
notDodgy
    :: Bool  -- ^ Law. /This is not any ordinary 'Bool'!/ See the documentation
             -- on 'law' for more information.
    -> law
notDodgy :: Bool -> law
notDodgy =
  String -> Bool -> law
forall a. HasCallStack => String -> a
error String
"notDodgy may be called only inside of a call to testModel or theoremsOf"


------------------------------------------------------------------------------
-- | Asserts that a function should be a homomorphism in the argument described
-- by a lambda.
--
-- This function /must/ be called with a type application describing the desired
-- homomorphism. Acceptable typeclasses are 'Data.Semigroup.Semigroup',
-- 'Monoid', 'Data.Group.Group', 'Eq' and 'Ord'.
--
-- The argument to this function must be a lambda binding a single variable.
--
-- This function introduces a law for every method in the typeclass.
--
-- This function /must/ be called only in the context of either
-- 'AlgebraCheckers.testModel' or 'AlgebraCheckers.theoremsOf'.
--
-- ==== __Examples__
--
-- @'homo' \@'Monoid' $ \\s -> set x s@
homo
    :: (homo a, homo b)
    => (a -> b)  -- ^ The function expected to be a homomorphism.
                 -- /This is not any ordinary function!/ See the documentation
                 -- on 'homo' for more information.
    -> law
homo :: (a -> b) -> law
homo =
  String -> (a -> b) -> law
forall a. HasCallStack => String -> a
error String
"homo may be called only inside of a call to testModel or theoremsOf"