{-# 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))
law
:: String
-> Bool
-> 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"
notDodgy
:: Bool
-> 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"
homo
:: (homo a, homo b)
=> (a -> b)
-> 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"