packages feed

algebra-checkers (empty) → 0.1.0.0

raw patch · 15 files changed

+1143/−0 lines, 15 filesdep +QuickCheckdep +ansi-terminaldep +basesetup-changed

Dependencies added: QuickCheck, ansi-terminal, base, checkers, containers, groups, mtl, pretty, syb, template-haskell, th-instance-reification, transformers

Files

+ ChangeLog.md view
@@ -0,0 +1,3 @@+# Changelog for algebra-checkers++## Unreleased changes
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Sandy Maguire (c) 2020++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Sandy Maguire nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,92 @@+# algebra-checkers++[![Build Status](https://travis-ci.org/isovector/algebra-checkers.svg?branch=master)](https://travis-ci.org/isovector/algebra-checkers)++## Dedication++> "Any fool can make a rule, and any fool will mind it."+>+> Henry David Thoreau+++## Overview++`algebra-checkers` is a little library for testing algebraic laws. For example,+imagine we're writing an ADT:++```haskell+data Foo a+instance Semigroup (Foo a)+instance Monoid (Foo a)++data Key+++get :: Key -> Foo a -> a+get = undefined++set :: Key -> a -> Foo a -> Foo a+set = undefined+```++Let's say we expect the lens laws to hold for `get` and `set`, as well for `set`+to be a monoid homomorphism. We can express those facts to `algebra-checkers`+and have it generate tests for us:++```haskell+lawTests :: [Property]+lawTests = $(testModel [e| do++law "set/set"+    (set i x' (set i x s) == set i x' s)++law "set/get"+    (set i (get i s) s == s)++law "get/set"+    (get i (set i x s) == x)++homo @Monoid+    (\s -> set i x s)++|])+```++Furthermore, `algebra-checkers` will generate tests to show that these laws are+confluent. We can run these tests via `quickCheck lawTests`.++If we use the `theoremsOf` function instead of `testModel`, `algebra-checkers`+will dump out all the additional theorems it has proven about our algebra. This+serves as a good sanity check:++```+Theorems:++• set i x' (set i x s) = set i x' s (definition of "set/set")+• set i (get i s) s = s (definition of "set/get")+• get i (set i x s) = x (definition of "get/set")+• set i x mempty = mempty (definition of "set:Monoid:mempty")+• set i x (s1 <> s2) = set i x s1 <> set i x s2+    (definition of "set:Monoid:<>")+• set i1 (get i1 (set i1 x1 s1)) s1 = set i1 x1 s1+    (implied by "set/get" and "set/set")+• set i1 (get i1 (s12 <> s22)) s12 <> set i1 (get i1 (s12 <> s22)) s22+        = s12 <> s22+    (implied by "set/get" and "set:Monoid:<>")+• set i1 x'2 (set i1 x1 s11 <> set i1 x1 s21)+        = set i1 x'2 (s11 <> s21)+    (implied by "set/set" and "set:Monoid:<>")+• get i1 (set i1 x1 s11 <> set i1 x1 s21) = x1+    (implied by "get/set" and "set:Monoid:<>")+++Contradictions:++• get i1 mempty = x1+    the variable x1 is undetermined+    (implied by "get/set" and "set:Monoid:mempty")+```++Uh oh! Look at that! This contradiction is  clearly a bogus theorem, which lets+us know that "get/set" and "set mempty" are nonconfluent with one another!+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ algebra-checkers.cabal view
@@ -0,0 +1,58 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: b82e33c00a44f13bb2653ad3fb8f750bc17d16b2c3c2c62c4aa0efed07997433++name:           algebra-checkers+version:        0.1.0.0+synopsis:       Model and test API surfaces algebraically+description:    Please see the README on GitHub at <https://github.com/isovector/algebra-checkers#readme>+category:       Model+homepage:       https://github.com/isovector/algebra-checkers#readme+bug-reports:    https://github.com/isovector/algebra-checkers/issues+author:         Sandy Maguire+maintainer:     sandy@sandymaguire.me+copyright:      2020 Sandy Maguire+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md++source-repository head+  type: git+  location: https://github.com/isovector/algebra-checkers++library+  exposed-modules:+      AlgebraCheckers+  other-modules:+      AlgebraCheckers.Homos+      AlgebraCheckers.Patterns+      AlgebraCheckers.Ppr+      AlgebraCheckers.Suggestions+      AlgebraCheckers.Theorems+      AlgebraCheckers.TH+      AlgebraCheckers.Types+      AlgebraCheckers.Unification+  hs-source-dirs:+      src+  ghc-options: -Wall+  build-depends:+      QuickCheck >=2.10.1 && <3+    , ansi-terminal >=0.10.3+    , base >=4.7 && <5+    , checkers >=0.5.5+    , containers >=0.5.10.2+    , groups >=0.4.1.0+    , mtl >=2.2.2 && <3+    , pretty >=1.1.3.3 && <2+    , syb >=0.7+    , template-haskell >=2.12.0.0 && <3+    , th-instance-reification >=0.1.5+    , transformers >=0.5.2.0+  default-language: Haskell2010
+ src/AlgebraCheckers.hs view
@@ -0,0 +1,14 @@+module AlgebraCheckers+  ( -- * Model Checking+    testModel+  , theoremsOf++    -- * Modeling Tools+  , law+  , homo+  , notDodgy+  ) where++import AlgebraCheckers.Patterns+import AlgebraCheckers.TH+
+ src/AlgebraCheckers/Homos.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE CPP                   #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++module AlgebraCheckers.Homos where++import           AlgebraCheckers.Types+import           AlgebraCheckers.Unification+import           Control.Arrow (second)+import           Data.Group+import           Data.List (foldl')+import qualified Data.Map as M+import           Data.Maybe+import           Language.Haskell.TH hiding (ppr, Arity)++#if __GLASGOW_HASKELL__ <= 802+import           Data.Semigroup+#endif+++appHead :: Exp -> Maybe Name+appHead = fmap fst . splitApps++splitApps :: Exp -> Maybe (Name, [Exp])+splitApps (VarE n)         = Just (n, [])+splitApps (ConE n)         = Just (n, [])+splitApps (AppE f e)       = fmap (second (++ [e])) $ splitApps f+splitApps (InfixE e1 f e2) =+  fmap (second (\e -> e ++ maybeToList e1 ++ maybeToList e2)) $ splitApps f+splitApps _                = Nothing++aritySize :: Arity -> Int+aritySize Binary     = 2+aritySize (Prefix n) = n++makeHomo :: Name -> [(Name, Arity)] -> Exp -> [Law LawSort]+makeHomo ty ops (LamE [VarP name] body) =+  let app_head = maybe "<expr>" nameBase $ appHead body+      homo_name = nameBase ty+      hs = fmap (UnboundVarE . mkName . (nameBase name ++) . show)+                [1 .. maximum $ fmap (aritySize . snd) ops]+      mk_lawname fn =+        mconcat+          [ app_head, ":", homo_name, ":", nameBase fn ]+   in flip fmap ops $ \(fn_name, arity) ->+        mkHomo name hs body (mk_lawname fn_name) (VarE fn_name) arity+makeHomo _ _ _ = error "monoidal homomorphism needs a lambda"+++mkHomo :: Name -> [Exp] -> Exp -> String -> Exp -> Arity -> NamedLaw+mkHomo name vars body law_name fn Binary =+  case vars of+    (v1:v2:_) ->+      let replace x = rebindVars (M.singleton name x) body+       in Law (LawName law_name)+              (replace $ InfixE (Just v1) fn (Just v2))+              (InfixE (Just $ replace v1)+                      fn+                      (Just $ replace v2))+    _ -> error "not enough args to mkHomo"+mkHomo name all_vars body law_name fn (Prefix n)=+  let replace x = rebindVars (M.singleton name x) body+      vars = take n all_vars+   in Law (LawName law_name)+          (replace $ foldl' AppE fn vars)+          (foldl' AppE fn $ fmap replace vars)+++knownHomos :: Name -> [(Name, Arity)]+knownHomos nm+  | nm == ''Semigroup+        = [ ('(<>),   Binary) ]+  | nm == ''Monoid+        = [ ('mempty, Prefix 0)+          , ('(<>),   Binary)+          ]+  | nm == ''Group+        = [ ('invert, Prefix 1) ]+  | nm == ''Eq+        = [ ('(==), Binary) ]+  | nm == ''Ord+        = [ ('compare, Prefix 2) ]+  | otherwise = error $ "unsupported homo type " ++ show nm+
+ src/AlgebraCheckers/Patterns.hs view
@@ -0,0 +1,167 @@+{-# 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 NotDodgyParens exp1 exp2 <- NoBindS+  (      VarE ((==) 'notDodgy -> True)+  `AppE` (InfixE (Just exp1)+                 (VarE ((==) '(==) -> True))+                 (Just exp2)+         )+  )++pattern NotDodgyDollar :: Exp -> Exp -> Stmt+pattern 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 (NotDodgyParens exp1 exp2) = Just (exp1, exp2)+matchNotDodgy (NotDodgyDollar exp1 exp2) = Just (exp1, exp2)+matchNotDodgy _ = Nothing++pattern NotDodgyDef :: Exp -> Exp -> Stmt+pattern NotDodgyDef exp1 exp2 <- (matchNotDodgy -> Just (exp1, exp2))+++pattern LawParens :: String -> Exp -> Exp -> Stmt+pattern 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 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 (LawParens name exp1 exp2) = Just (name, exp1, exp2)+matchLaw (LawDollar name exp1 exp2) = Just (name, exp1, exp2)+matchLaw _ = Nothing++pattern LawDef :: String -> Exp -> Exp -> Stmt+pattern LawDef name exp1 exp2 <- (matchLaw -> Just (name, exp1, exp2))+++pattern HomoParens :: Name -> Exp -> Stmt+pattern HomoParens ty expr <- NoBindS+  (      (VarE ((==) 'homo -> True) `AppTypeE` ConT ty)+  `AppE` expr+  )++pattern HomoDollar :: Name -> Exp -> Stmt+pattern HomoDollar ty expr <- NoBindS+  (InfixE+    (Just ((VarE ((==) 'homo -> True) `AppTypeE` ConT ty)))+    (VarE ((==) '($) -> True))+    (Just expr)+  )++matchHomo :: Stmt -> Maybe (Name, Exp)+matchHomo (HomoParens ty expr) = Just (ty, expr)+matchHomo (HomoDollar ty expr) = Just (ty, expr)+matchHomo _ = Nothing+++pattern HomoDef :: Name -> Exp -> Stmt+pattern 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 =+  error "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 =+  error "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 =+  error "homo may be called only inside of a call to testModel or theoremsOf"+
+ src/AlgebraCheckers/Ppr.hs view
@@ -0,0 +1,129 @@+module AlgebraCheckers.Ppr+  ( module AlgebraCheckers.Ppr+  , Doc+  , render+  , sep+  , vcat+  , hsep+  , text+  ) where++import           Control.Monad+import qualified Language.Haskell.TH as Ppr (ppr)+import           Language.Haskell.TH hiding (ppr, Arity)+import           Language.Haskell.TH.PprLib (to_HPJ_Doc)+import           Prelude hiding (exp)+import           System.Console.ANSI+import           AlgebraCheckers.Types+import           AlgebraCheckers.Unification+import qualified Text.PrettyPrint.HughesPJ as Ppr+import           Text.PrettyPrint.HughesPJ hiding ((<>))+++ppr :: Ppr a => a -> Doc+ppr = to_HPJ_Doc . Ppr.ppr++showTheoremSource :: TheoremSource -> Doc+showTheoremSource (LawDefn n) =+  text "definition of" <+> colorize lawColor (text $ show n)+showTheoremSource (Interaction a b) =+  hsep+    [ text "implied by"+    , colorize lawColor $ text $ show $ min a b+    , text "and"+    , colorize lawColor $ text $ show $ max a b+    ]++colorize :: Color -> Doc -> Doc+colorize c doc+       = zeroWidthText (setSGRCode [SetColor Foreground Vivid c])+  Ppr.<> doc+  Ppr.<> zeroWidthText (setSGRCode [SetDefaultColor Foreground])++deepColorize :: Color -> Doc -> Doc+deepColorize c doc+       = zeroWidthText (setSGRCode [SetColor Foreground Vivid c, SetConsoleIntensity BoldIntensity])+  Ppr.<> doc+  Ppr.<> zeroWidthText (setSGRCode [SetDefaultColor Foreground, SetConsoleIntensity NormalIntensity])++backcolorize :: Color -> Doc -> Doc+backcolorize c doc+       = zeroWidthText (setSGRCode [SetColor Background Dull c])+  Ppr.<> doc+  Ppr.<> zeroWidthText (setSGRCode [SetDefaultColor Background])++showSaneTheorem :: Theorem -> Doc+showSaneTheorem (Law n a b) = hang (text "•") 2 $+  sep+  [ hang (colorize exprColor $ ppr $ deModuleName a) 6+      . hang (text "=") 2+      . colorize exprColor+      . ppr+      $ deModuleName b+  , nest 2 $ parens $ showTheoremSource n+  ]++showContradictoryTheorem :: Theorem -> TheoremProblem -> Doc+showContradictoryTheorem (Law n a b) (Contradiction reason) = hang (text "•") 2 $+  sep+  [ vcat+      [ backcolorize Red $ hang (ppr $ deModuleName a) 6+          . hang (text "=") 2+          . ppr+          $ deModuleName b+      , nest 2 $ pprContradiction reason+      ]+  , nest 2 $ parens $ showTheoremSource n+  ]+showContradictoryTheorem (Law n a b) (Dodgy reason) = hang (text "•") 2 $+  sep+  [ vcat+      [ hang (backcolorize Black $ ppr $ deModuleName a) 6+          . hang (text "=") 2+          . backcolorize Black+          . ppr+          $ deModuleName b+      , nest 2 $ pprDodgy reason+      ]+  , nest 2 $ parens $ showTheoremSource n+  ]++plural :: String -> String -> [a] -> Doc+plural one _ [_] = text one+plural _ many _  = text many++pprContradiction :: ContradictionReason -> Doc+pprContradiction (UnboundMatchableVars vars) =+  sep+    [ text "the"+    , plural "variable" "variables" vars+    , sep $ punctuate (char ',') $ fmap ppr vars+    , nest 4 $ sep+        [ plural "is" "are" vars+        , text "undetermined"+        ]+    ]+pprContradiction (UnknownConstructors vars) =+  sep+    [ text "the"+    , plural "constructor" "constructors" vars+    , sep $ punctuate (char ',') $ fmap ppr vars+    , nest 4 $ sep+        [ plural "does" "do" vars+        , text "not exist"+        ]+    ]+pprContradiction UnequalValues =+  text "unequal values"++pprDodgy :: DodgyReason -> Doc+pprDodgy SelfRecursive =+  text "not necessarily productive"+++exprColor :: Color+exprColor = Blue++lawColor :: Color+lawColor = Yellow+
+ src/AlgebraCheckers/Suggestions.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE TemplateHaskellQuotes #-}++module AlgebraCheckers.Suggestions where++import AlgebraCheckers.Patterns+import AlgebraCheckers.Ppr+import AlgebraCheckers.Unification+import Control.Monad+import Data.Char+import Data.Data+import Data.Generics.Schemes (listify)+import Data.Group+import Data.List+import Data.Maybe+import Data.Semigroup+import Data.Traversable+import Language.Haskell.TH hiding (ppr)+import Language.Haskell.TH.Syntax+import Prelude hiding (exp)+import THInstanceReification+++data Suggestion+  = HomoSuggestion Name Name Int Type Type Exp+  deriving (Eq, Ord, Show)++homoSuggestionEq :: Suggestion -> Suggestion -> Bool+homoSuggestionEq (HomoSuggestion _ fn1 ix1 _ _ _)+                 (HomoSuggestion _ fn2 ix2 _ _ _) = fn1 == fn2+                                                 && ix1 == ix2+++pprSuggestion :: Suggestion -> Doc+pprSuggestion (HomoSuggestion nm _ _ arg_ty res_ty (LamE [VarP var] exp)) =+  ppr $ deModuleName $+    VarE 'law `AppTypeE` ConT nm `AppE` (LamE [SigP (VarP var) arg_ty] $ SigE exp res_ty)+pprSuggestion (HomoSuggestion nm _ _ _ _ exp) =+  ppr $ deModuleName $+    VarE 'law `AppTypeE` ConT nm `AppE` exp+++knownSuggestionHierarchies :: [[Name]]+knownSuggestionHierarchies =+  [ [ ''Group, ''Monoid, ''Semigroup ]+  ]++suggest :: Data a => Module -> a -> Q [Suggestion]+suggest md a = do+  let surface = getSurface md a+  fmap (join . join) $+    for surface $ \nm ->+      for knownSuggestionHierarchies $ \hierarchy -> do+        zs <- fmap join $ for hierarchy $ \tc_name -> do+          VarI _ ty _ <- reify nm+          possibleHomos tc_name nm ty+        pure $ nubBy homoSuggestionEq zs+++suggest' :: Data a => a -> Q [Suggestion]+suggest' a = do+  md <- thisModule+  suggest md a++++possibleHomos :: Name -> Name -> Type -> Q [Suggestion]+possibleHomos tc_name fn ty = do+  let (args, res) = unrollTyArr ty+  hasInstance tc_name res >>= \case+    False -> pure []+    True  -> do+      names <- for args $ newName . goodTyName+      fmap catMaybes $ for (zip3 names args [0..]) $ \(name, arg, ix) ->+        hasInstance tc_name arg >>= \case+          False -> pure Nothing+          True  -> do+            exp <- lamE [varP name] $ appsE $ varE fn : fmap varE names+            pure $ Just $ HomoSuggestion tc_name fn ix arg res exp+++goodTyName :: Type -> String+goodTyName = fmap toLower . take 1 . dropWhile (not . isAlpha) . render . ppr . deModuleName++getSurface :: Data a => Module -> a -> [Name]+getSurface m = listify (sameModule m)+++sameModule :: Module -> Name -> Bool+sameModule (Module (PkgName pkg) (ModName md)) n =+  nameModule n == Just md && namePackage n == Just pkg+++unrollTyArr :: Type -> ([Type], Type)+unrollTyArr ty =+  let tys = unloopTyArrs ty+   in (init tys, last tys)+  where+    unloopTyArrs :: Type -> [Type]+    unloopTyArrs (ArrowT `AppT` a `AppT` b) =  a : unloopTyArrs b+    unloopTyArrs t =  [t]++hasInstance :: Name -> Type -> Q Bool+hasInstance tc_name = isProperInstance tc_name . pure+
+ src/AlgebraCheckers/TH.hs view
@@ -0,0 +1,106 @@+{-# 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 md thm =+  case sanityCheck' md thm of+    Just contradiction ->+      showContradictoryTheorem thm contradiction+    Nothing -> showSaneTheorem thm++propTestEq :: Theorem -> ExpQ+propTestEq t@(Law _ exp1 exp2) = do+  md <- thisModule+  let vars = nub $ unboundVars exp1 ++ unboundVars exp2+  names <- for vars $ newName . 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 = (testModelImpl =<<)++testModelImpl :: Exp -> ExpQ+testModelImpl e = do+  m <- thisModule+  listE . fmap propTestEq . theorize m $ parseLaws e++parseLaws :: Exp -> [Law LawSort]+parseLaws (DoE z) = concatMap collect z+parseLaws _ = error "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 = (theoremsOfImpl =<<)++theoremsOfImpl :: Exp -> ExpQ+theoremsOfImpl z = do+  md <- thisModule+  let (theorems, problems) = partition (sanityCheck md) $ theorize md $ parseLaws z+      contradicts = filter (maybe False isContradiction . sanityCheck' md) problems+      dodgy       = filter (maybe False isDodgy . sanityCheck' md) problems+  runIO $ do+    putStrLn ""+    printStuff md "Theorems"       theorems+    printStuff md "Dodgy Theorems" dodgy+    printStuff md "Contradictions" contradicts+  listE $ fmap propTestEq $ theorems ++ dodgy ++ contradicts++printStuff :: Module -> String -> [Theorem] -> IO ()+printStuff md sort laws =+  when (not $ null laws) $ do+    putStrLn . render+             $ sep+             $ text (sort ++ ":") : text "" : fmap (showTheorem md) laws+    putStrLn ""+    putStrLn ""++collect :: Stmt -> [Law LawSort]+collect (LawDef lawname exp1 exp2) = [Law (LawName lawname) exp1 exp2]+collect (NotDodgyDef exp1 exp2)    = [Law LawNotDodgy exp1 exp2]+collect (HomoDef ty expr)          = makeHomo ty (knownHomos ty) expr+collect x = error $ show x+  -- "collect must be called with the form [e| law \"name\" (foo a b c == bar a d e) |]"+
+ src/AlgebraCheckers/Theorems.hs view
@@ -0,0 +1,107 @@+{-# LANGUAGE TemplateHaskellQuotes #-}+{-# LANGUAGE TupleSections         #-}++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 md = isNothing . sanityCheck' md++sanityCheck' :: Module -> Theorem -> Maybe TheoremProblem+sanityCheck' md (Law _ lhs rhs) =+  either Just (const Nothing) $ foldr1 (>>)+    [ lift_error (Contradiction . UnknownConstructors)+        $ fmap (\(UnboundVarE n) -> n)+        $ listify is_unbound_ctor (lhs, rhs)+    , ensure_bound_matches lhs rhs+    , ensure_bound_matches rhs lhs+    , bool (Left $ Contradiction UnequalValues) (Right ()) $+        on (&&) isFullyMatchable lhs rhs `implies` (==) lhs rhs+    , bool (Left $ Contradiction UnequalValues) (Right ()) $ fromMaybe True $+        liftM2 (==) (matchableAppHead lhs) (matchableAppHead rhs)+    , bool (Right ()) (Left $ Dodgy SelfRecursive) $ nonlinearUse md lhs rhs+    , bool (Right ()) (Left $ Dodgy SelfRecursive) $ nonlinearUse md rhs lhs+    ]+  where+    is_unbound_ctor (UnboundVarE n) = isUpper . head $ nameBase n+    is_unbound_ctor _ = False++    ensure_bound_matches a b+      = lift_error (Contradiction . UnboundMatchableVars)+      $ filter (not . exists_in a)+      $ matchableMetaVars b+    lift_error _ [] = Right ()+    lift_error ctor x = Left $ ctor x+    exists_in exp var = not . null $ listify (== var) exp++implies :: Bool -> Bool -> Bool+implies p q = not p || q++matchableMetaVars :: Exp -> [Name]+matchableMetaVars (UnboundVarE n) = [n]+matchableMetaVars e =+  case matchableAppHead e of+    Just _ -> go e+    Nothing -> []+  where+    go (exp1 `AppE` exp2) =+      go exp1 ++ matchableMetaVars exp2+    go _ = []++isFullyMatchable :: Exp -> Bool+isFullyMatchable (ConE _)                 = True+isFullyMatchable (TupE es)                = all isFullyMatchable es+isFullyMatchable (ListE es)               = all isFullyMatchable es+isFullyMatchable (LitE _)                 = True+isFullyMatchable (UnboundVarE _)          = True+isFullyMatchable (AppE (UnboundVarE _) _) = False+isFullyMatchable (AppE exp1 exp2)         = isFullyMatchable exp1 && isFullyMatchable exp2+isFullyMatchable _                        = False++namedLawToEither :: NamedLaw -> Either (Law ()) (Law String)+namedLawToEither (Law (LawName n) a b) = Right (Law n a b)+namedLawToEither (Law LawNotDodgy a b) = Left (Law () a b)++theorize :: Module -> [NamedLaw] -> [Theorem]+theorize md named_laws =+  let (not_dodgy, laws) = partitionEithers $ fmap namedLawToEither named_laws+      law_defs = fmap (\t -> t { lawData = LawDefn $ lawData t }) laws+      sane_laws = filter (sanityCheck md) law_defs+      theorems = do+         l1@Law{lawData = LawDefn l1name} <- sane_laws+         l2@Law{lawData = LawDefn l2name} <- sane_laws+         guard $ l1 /= l2+         (lhs, rhs) <- criticalPairs l1 l2+         pure $ Law (Interaction l1name l2name) lhs rhs+   in (nub $ law_defs <> theorems) \\ fmap (\l -> l {lawData = LawDefn ""} ) not_dodgy++matchableAppHead :: Exp -> Maybe Name+matchableAppHead (ConE n)   = Just n+matchableAppHead (AppE f _) = matchableAppHead f+matchableAppHead _          = Nothing++nonlinearUse :: Module -> Exp -> Exp -> Bool+nonlinearUse md exp1 exp2 =+  let exp2s = mapMaybe (\exp -> splitApps exp) $ fmap seExp $ subexps exp2+   in any (\(apphead, exps) -> nonlinearFunc md apphead && any (equalUpToAlpha exp1) exps) exp2s++nonlinearFunc :: Module -> Name -> Bool+nonlinearFunc md name = not $ sameModule md name+
+ src/AlgebraCheckers/Types.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFunctor      #-}++module AlgebraCheckers.Types where++import Data.Data+import AlgebraCheckers.Unification+import Language.Haskell.TH++data Law a = Law+  { lawData :: a+  , lawLhsExp :: Exp+  , lawRhsExp :: Exp+  }+  deriving (Ord, Show, Data, Typeable)++instance Eq a => Eq (Law a) where+  Law _ a a' == Law _ b b' =+    and+      [ equalUpToAlpha a b && equalUpToAlpha a' b'+      ]++data LawSort+  = LawName String+  | LawNotDodgy+  deriving (Eq, Ord, Show)++type NamedLaw = Law LawSort+type Theorem  = Law TheoremSource++data Arity = Binary | Prefix Int+  deriving (Eq, Ord, Show)++data TheoremProblem+  = Dodgy DodgyReason+  | Contradiction ContradictionReason+  deriving (Eq, Ord, Show)++isContradiction :: TheoremProblem -> Bool+isContradiction Contradiction{} = True+isContradiction _               = False++isDodgy :: TheoremProblem -> Bool+isDodgy Dodgy{} = True+isDodgy _       = False++data ContradictionReason+  = UnboundMatchableVars [Name]+  | UnequalValues+  | UnknownConstructors [Name]+  deriving (Eq, Ord, Show)++data DodgyReason+  = SelfRecursive+  deriving (Eq, Ord, Show)++data TheoremSource+  = LawDefn String+  | Interaction String String+  deriving (Eq, Ord, Show)+
+ src/AlgebraCheckers/Types.hs-boot view
@@ -0,0 +1,11 @@+module AlgebraCheckers.Types where++import Language.Haskell.TH++data Law a = Law+  { lawData :: a+  , lawLhsExp :: Exp+  , lawRhsExp :: Exp+  }++
+ src/AlgebraCheckers/Unification.hs view
@@ -0,0 +1,175 @@+{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE ViewPatterns    #-}++module AlgebraCheckers.Unification where++import           Control.Applicative+import           Control.Monad.State+import           Control.Monad.Trans.Writer+import           Data.Data+import           Data.Function+import           Data.Generics.Aliases+import           Data.Generics.Schemes+import qualified Data.Map as M+import           Language.Haskell.TH+import           Language.Haskell.TH.Syntax+import           Prelude hiding (exp)+import {-# SOURCE #-} AlgebraCheckers.Types+++data SubExp = SubExp+  { seExp  :: Exp+  , seSubId :: Int+  } deriving (Eq, Ord, Show)+++deModuleName :: Data a => a -> a+deModuleName = everywhere $ mkT $ \case+  NameQ _ -> NameS+  NameG _ _ _ -> NameS+  n       -> n+++unboundVars :: Exp -> [Name]+unboundVars = everything (++) $+  mkQ [] $ \case+    UnboundVarE n -> [n]+    _ -> []+++------------------------------------------------------------------------------+-- | Operates over UnboundVarEs+bindVars :: Data a => M.Map Name Exp -> a -> a+bindVars m = everywhere $ mkT $ \case+  e@(UnboundVarE n) ->+    case M.lookup n m of+      Just e' -> e'+      Nothing -> e+  t -> t+++------------------------------------------------------------------------------+-- | Operates over VarEs+rebindVars :: Data a => M.Map Name Exp -> a -> a+rebindVars m = everywhere $ mkT $ \case+  e@(VarE n) ->+    case M.lookup n m of+      Just e' -> e'+      Nothing -> e+  t -> t+++renameVars :: Data a => (String -> String) -> a -> a+renameVars f = everywhere $ mkT $ \case+  UnboundVarE n -> UnboundVarE . mkName . f $ nameBase n+  t -> t+++type Subst = M.Map Name Exp++sub :: Data a => Subst -> a -> a+sub = bindVars++unifySub :: Subst -> Exp -> Exp -> Maybe Subst+unifySub s a+  = fmap ((M.map =<< sub) . flip mappend s)+  . on unify (sub s) a++++type Critical = (Exp, Exp)++criticalPairs :: Law a -> Law a -> [Critical]+criticalPairs other me = do+  let (otherlhs, otherrhs)+        = renameVars (++ "1") (lawLhsExp other, lawRhsExp other)+      (melhs, merhs)+        = renameVars (++ "2") (lawLhsExp me, lawRhsExp me)++  pat <- subexps melhs+  Just subs <- pure $ unify (seExp pat) otherlhs+  let res = bindVars subs (merhs, replaceSubexp pat (const otherrhs) melhs)+  guard $ uncurry (/=) res+  let (a,b) = res+  pure (min a b, max a b)++++subexps :: Exp -> [SubExp]+subexps e =+  flip evalState 0 $ execWriterT $+    everywhereM (mkM  $ \e' -> do+      ix <- get+      modify (+1)+      case e' of+        UnboundVarE _ -> pure ()+        se -> tell [(SubExp se ix)]+      pure e'+                             ) e+++replaceSubexp :: SubExp -> (Exp -> Exp) -> Exp -> Exp+replaceSubexp (SubExp _ ix) f old =+  flip evalState 0 $+    everywhereM (mkM $ \e' -> do+      ix' <- get+      modify (+1)+      pure $ case ix == ix' of+        True  -> f e'+        False -> e'+                ) old+++equalUpToAlpha :: Exp -> Exp -> Bool+equalUpToAlpha a b =+  maybe+    False+    (\subst -> all isUnbound subst+            && uncurry (==) (bindVars subst (a, b)))+    (unify a b)+  where+    isUnbound (UnboundVarE _) = True+    isUnbound _ = False+++unify :: Exp -> Exp -> Maybe Subst+unify (ParensE exp1) exp2 = unify exp1 exp2+unify exp1 (ParensE exp2) = unify exp1 exp2+unify (UnboundVarE name) exp = pure $ M.singleton name exp+unify exp (UnboundVarE name) = pure $ M.singleton name exp+unify (AppE f1 exp1) (AppE f2 exp2) = do+  s1 <- unify f1 f2+  s2 <- unifySub s1 exp1 exp2+  pure s2+unify (AppTypeE exp1 t1) (AppTypeE exp2 t2) = do+  guard $ t1 == t2+  unify exp1 exp2+unify (InfixE (Just lhs1) exp1 (Just rhs1))+      (InfixE (Just lhs2) exp2 (Just rhs2)) = do+  s1 <- unify exp1 exp2+  s2 <- unifySub s1 lhs1 lhs2+  s3 <- unifySub s2 rhs1 rhs2+  pure s3+unify (InfixE Nothing exp1 (Just rhs1))+      (InfixE Nothing exp2 (Just rhs2)) = do+  s1 <- unify exp1 exp2+  unifySub s1 rhs1 rhs2+unify (InfixE (Just lhs1) exp1 Nothing)+      (InfixE (Just lhs2) exp2 Nothing) = do+  s1 <- unify lhs1 lhs2+  unifySub s1 exp1 exp2+unify (TupE exps1) (TupE exps2) = do+  guard $ exps1 == exps2+  foldM (uncurry . unifySub) mempty $ zip exps1 exps2+unify (CondE cond1 then1 else1) (CondE cond2 then2 else2) = do+  s1 <- unify cond1 cond2+  s2 <- unifySub s1 then1 then2+  unifySub s2 else1 else2+unify (SigE exp1 t1) (SigE exp2 t2) = do+  guard $ t1 == t2+  unify exp1 exp2+unify a b = do+  guard $ a == b+  pure mempty+