{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
-- Semigroup (Specification a), Monoid (Specification a)
{-# OPTIONS_GHC -Wno-orphans #-}

module Constrained.Conformance where

import Constrained.Base (
  Binder (..),
  HasSpec,
  Pred (..),
  Specification (..),
  Term (..),
  Weighted (..),
  addToErrorSpec,
  combineSpec,
  conformsTo,
  explainSpecOpt,
  forAllToList,
  memberSpecList,
  notMemberSpec,
  showType,
  toPreds,
 )
import Constrained.Core (
  NonEmpty ((:|)),
  Rename (rename),
 )
import Constrained.Env (
  Env,
  extendEnv,
  singletonEnv,
 )
import Constrained.GenT (
  GE (..),
  MonadGenError (..),
  catMessageList,
  errorGE,
  explain,
  fromGE,
  runGE,
 )
import Constrained.List (
  mapList,
 )
import Constrained.Syntax (
  runCaseOn,
  runTerm,
  runTermE,
  substitutePred,
 )

import Data.List (intersect, nub)
import qualified Data.List.NonEmpty as NE
import Data.Maybe
import Data.Semigroup (sconcat)
import Prettyprinter hiding (cat)
import Test.QuickCheck (Property, Testable, property)

-- =========================================================================

-- | Does the Pred evaluate to true under the given Env.
--   If it doesn't, some explanation appears in the failure of the monad 'm'
checkPred :: forall m. MonadGenError m => Env -> Pred -> m Bool
checkPred :: forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred Env
env = \case
  p :: Pred
p@(ElemPred Bool
bool Term a
term NonEmpty a
xs) -> do
    a
v <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term a
term
    case (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
v NonEmpty a
xs, Bool
bool) of
      (Bool
True, Bool
True) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      (Bool
True, Bool
False) -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (String
"notElemPred reduces to True" forall a. a -> [a] -> NonEmpty a
:| [forall a. Show a => a -> String
show Pred
p])
      (Bool
False, Bool
True) -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (String
"elemPred reduces to False" forall a. a -> [a] -> NonEmpty a
:| [forall a. Show a => a -> String
show Pred
p])
      (Bool
False, Bool
False) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  Monitor {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  Subst Var a
x Term a
t Pred
p -> forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred Env
env forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
  Assert Term Bool
t -> forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term Bool
t
  GenHint {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  p :: Pred
p@(Reifies Term b
t' Term a
t a -> b
f) -> do
    a
val <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term a
t
    b
val' <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term b
t'
    forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE (forall a. [a] -> NonEmpty a
NE.fromList [String
"Reification:", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred
p]) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> b
f a
val forall a. Eq a => a -> a -> Bool
== b
val')
  ForAll Term t
t (Var a
x :-> Pred
p) -> do
    t
set <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term t
t
    forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
        [ forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred Env
env' Pred
p
        | a
v <- forall t e. Forallable t e => t -> [e]
forAllToList t
set
        , let env' :: Env
env' = forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env
        ]
  Case Term (SumOver as)
t List (Weighted Binder) as
bs -> do
    SumOver as
v <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term (SumOver as)
t
    forall (as :: [*]) r.
SumOver as
-> List Binder as
-> (forall a. HasSpec a => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as
v (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing List (Weighted Binder) as
bs) (\Var a
x a
val Pred
ps -> forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) Pred
ps)
  When Term Bool
bt Pred
p -> do
    Bool
b <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term Bool
bt
    if Bool
b then forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred Env
env Pred
p else forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  Pred
TruePred -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  FalsePred NonEmpty String
es -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE NonEmpty String
es forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  DependsOn {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  And [Pred]
ps -> forall (m :: * -> *) (t :: * -> *).
(MonadGenError m, Traversable t) =>
Env -> t Pred -> m Bool
checkPreds Env
env [Pred]
ps
  Let Term a
t (Var a
x :-> Pred
p) -> do
    a
val <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term a
t
    forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) Pred
p
  Exists (forall b. Term b -> b) -> GE a
k (Var a
x :-> Pred
p) -> do
    a
a <- forall (m :: * -> *) r. MonadGenError m => GE r -> m r
runGE forall a b. (a -> b) -> a -> b
$ (forall b. Term b -> b) -> GE a
k (forall a. GE a -> a
errorGE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"checkPred: Exists" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env)
    forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
a Env
env) Pred
p
  Explain NonEmpty String
es Pred
p -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE NonEmpty String
es forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred Env
env Pred
p

checkPreds :: (MonadGenError m, Traversable t) => Env -> t Pred -> m Bool
checkPreds :: forall (m :: * -> *) (t :: * -> *).
(MonadGenError m, Traversable t) =>
Env -> t Pred -> m Bool
checkPreds Env
env t Pred
ps = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred Env
env) t Pred
ps

checkPredPure :: Env -> Pred -> Bool
checkPredPure :: Env -> Pred -> Bool
checkPredPure Env
env Pred
p = forall a.
HasCallStack =>
(NonEmpty (NonEmpty String) -> a) -> GE a -> a
fromGE (forall a b. a -> b -> a
const Bool
False) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred Env
env Pred
p

-- ==========================================================

-- | Like checkPred, But it takes [Pred] rather than a single Pred,
--   and it builds a much more involved explanation if it fails.
--   Does the Pred evaluate to True under the given Env?
--   If it doesn't, an involved explanation appears in the (Just message)
--   If it does, then it returns Nothing
checkPredsE ::
  NE.NonEmpty String ->
  Env ->
  [Pred] ->
  Maybe (NE.NonEmpty String)
checkPredsE :: NonEmpty String -> Env -> [Pred] -> Maybe (NonEmpty String)
checkPredsE NonEmpty String
msgs Env
env [Pred]
ps =
  case forall a. [Maybe a] -> [a]
catMaybes (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env NonEmpty String
msgs) [Pred]
ps) of
    [] -> forall a. Maybe a
Nothing
    (NonEmpty String
x : [NonEmpty String]
xs) -> forall a. a -> Maybe a
Just (forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty String
x forall a. a -> [a] -> NonEmpty a
NE.:| [NonEmpty String]
xs)))

-- | An involved explanation for a single Pred
--   The most important explanations come when an assertion fails.
checkPredE :: Env -> NE.NonEmpty String -> Pred -> Maybe (NE.NonEmpty String)
checkPredE :: Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env NonEmpty String
msgs = \case
  p :: Pred
p@(ElemPred Bool
bool Term a
t NonEmpty a
xs) ->
    case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term a
t of
      Left NonEmpty String
message -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> NonEmpty String
message)
      Right a
v -> case (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
v NonEmpty a
xs, Bool
bool) of
        (Bool
True, Bool
True) -> forall a. Maybe a
Nothing
        (Bool
True, Bool
False) -> forall a. a -> Maybe a
Just (String
"notElemPred reduces to True" forall a. a -> [a] -> NonEmpty a
:| [forall a. Show a => a -> String
show Pred
p])
        (Bool
False, Bool
True) -> forall a. a -> Maybe a
Just (String
"elemPred reduces to False" forall a. a -> [a] -> NonEmpty a
:| [forall a. Show a => a -> String
show Pred
p])
        (Bool
False, Bool
False) -> forall a. Maybe a
Nothing
  Monitor {} -> forall a. Maybe a
Nothing
  Subst Var a
x Term a
t Pred
p -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env NonEmpty String
msgs forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
  Assert Term Bool
t -> case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term Bool
t of
    Right Bool
True -> forall a. Maybe a
Nothing
    Right Bool
False ->
      forall a. a -> Maybe a
Just
        (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Assert " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term Bool
t forall a. [a] -> [a] -> [a]
++ String
" returns False") forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"\nenv=\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a ann. Pretty a => a -> Doc ann
pretty Env
env)))
    Left NonEmpty String
es -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  GenHint {} -> forall a. Maybe a
Nothing
  p :: Pred
p@(Reifies Term b
t' Term a
t a -> b
f) ->
    case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term a
t of
      Left NonEmpty String
es -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> forall a. [a] -> NonEmpty a
NE.fromList [String
"checkPredE: Reification fails", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred
p] forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
      Right a
val -> case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term b
t' of
        Left NonEmpty String
es -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> forall a. [a] -> NonEmpty a
NE.fromList [String
"checkPredE: Reification fails", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred
p] forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
        Right b
val' ->
          if a -> b
f a
val forall a. Eq a => a -> a -> Bool
== b
val'
            then forall a. Maybe a
Nothing
            else
              forall a. a -> Maybe a
Just
                ( NonEmpty String
msgs
                    forall a. Semigroup a => a -> a -> a
<> forall a. [a] -> NonEmpty a
NE.fromList
                      [ String
"checkPredE: Reification doesn't match up"
                      , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred
p
                      , forall a. Show a => a -> String
show (a -> b
f a
val) forall a. [a] -> [a] -> [a]
++ String
" /= " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show b
val'
                      ]
                )
  ForAll Term t
t (Var a
x :-> Pred
p) -> case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term t
t of
    Left NonEmpty String
es -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> forall a. [a] -> NonEmpty a
NE.fromList [String
"checkPredE: ForAll fails to run."] forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
    Right t
set ->
      let answers :: [NonEmpty String]
answers =
            forall a. [Maybe a] -> [a]
catMaybes
              [ Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env' (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Some items in ForAll fail") Pred
p
              | a
v <- forall t e. Forallable t e => t -> [e]
forAllToList t
set
              , let env' :: Env
env' = forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env
              ]
       in case [NonEmpty String]
answers of
            [] -> forall a. Maybe a
Nothing
            (NonEmpty String
y : [NonEmpty String]
ys) -> forall a. a -> Maybe a
Just (forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty String
y forall a. a -> [a] -> NonEmpty a
NE.:| [NonEmpty String]
ys)))
  Case Term (SumOver as)
t List (Weighted Binder) as
bs -> case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term (SumOver as)
t of
    Right SumOver as
v -> forall (as :: [*]) r.
SumOver as
-> List Binder as
-> (forall a. HasSpec a => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as
v (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing List (Weighted Binder) as
bs) (\Var a
x a
val Pred
ps -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) NonEmpty String
msgs Pred
ps)
    Left NonEmpty String
es -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: Case fails" forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  When Term Bool
bt Pred
p -> case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term Bool
bt of
    Right Bool
b -> if Bool
b then Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env NonEmpty String
msgs Pred
p else forall a. Maybe a
Nothing
    Left NonEmpty String
es -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: When fails" forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  Pred
TruePred -> forall a. Maybe a
Nothing
  FalsePred NonEmpty String
es -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: FalsePred" forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  DependsOn {} -> forall a. Maybe a
Nothing
  And [Pred]
ps ->
    case forall a. [Maybe a] -> [a]
catMaybes (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Some items in And  fail")) [Pred]
ps) of
      [] -> forall a. Maybe a
Nothing
      (NonEmpty String
x : [NonEmpty String]
xs) -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty String
x forall a. a -> [a] -> NonEmpty a
NE.:| [NonEmpty String]
xs)))
  Let Term a
t (Var a
x :-> Pred
p) -> case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term a
t of
    Right a
val -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) NonEmpty String
msgs Pred
p
    Left NonEmpty String
es -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: Let fails" forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  Exists (forall b. Term b -> b) -> GE a
k (Var a
x :-> Pred
p) ->
    let eval :: forall b. Term b -> b
        eval :: forall b. Term b -> b
eval Term b
term = case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term b
term of
          Right b
v -> b
v
          Left NonEmpty String
es -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
NE.toList (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
     in case (forall b. Term b -> b) -> GE a
k forall b. Term b -> b
eval of
          Result a
a -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
a Env
env) NonEmpty String
msgs Pred
p
          FatalError NonEmpty (NonEmpty String)
es -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> NonEmpty (NonEmpty String) -> NonEmpty String
catMessageList NonEmpty (NonEmpty String)
es)
          GenError NonEmpty (NonEmpty String)
es -> forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> NonEmpty (NonEmpty String) -> NonEmpty String
catMessageList NonEmpty (NonEmpty String)
es)
  Explain NonEmpty String
es Pred
p -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es) Pred
p

-- | conformsToSpec with explanation. Nothing if (conformsToSpec a spec),
--   but (Just explanations) if not(conformsToSpec a spec).
conformsToSpecE ::
  forall a.
  HasSpec a =>
  a ->
  Specification a ->
  NE.NonEmpty String ->
  Maybe (NE.NonEmpty String)
conformsToSpecE :: forall a.
HasSpec a =>
a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE a
a (ExplainSpec [] Specification a
s) NonEmpty String
msgs = forall a.
HasSpec a =>
a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE a
a Specification a
s NonEmpty String
msgs
conformsToSpecE a
a (ExplainSpec (String
x : [String]
xs) Specification a
s) NonEmpty String
msgs = forall a.
HasSpec a =>
a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE a
a Specification a
s ((String
x forall a. a -> [a] -> NonEmpty a
:| [String]
xs) forall a. Semigroup a => a -> a -> a
<> NonEmpty String
msgs)
conformsToSpecE a
_ Specification a
TrueSpec NonEmpty String
_ = forall a. Maybe a
Nothing
conformsToSpecE a
a (MemberSpec NonEmpty a
as) NonEmpty String
msgs =
  if forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
a NonEmpty a
as
    then forall a. Maybe a
Nothing
    else
      forall a. a -> Maybe a
Just
        ( NonEmpty String
msgs
            forall a. Semigroup a => a -> a -> a
<> forall a. [a] -> NonEmpty a
NE.fromList
              [String
"conformsToSpecE MemberSpec case", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
a, String
"  not an element of", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NonEmpty a
as, String
""]
        )
conformsToSpecE a
a spec :: Specification a
spec@(TypeSpec TypeSpec a
s [a]
cant) NonEmpty String
msgs =
  if forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem a
a [a]
cant Bool -> Bool -> Bool
&& forall a. (HasSpec a, HasCallStack) => a -> TypeSpec a -> Bool
conformsTo a
a TypeSpec a
s
    then forall a. Maybe a
Nothing
    else
      forall a. a -> Maybe a
Just
        ( NonEmpty String
msgs
            forall a. Semigroup a => a -> a -> a
<> forall a. [a] -> NonEmpty a
NE.fromList
              [String
"conformsToSpecE TypeSpec case", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
a, String
"  (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
spec forall a. [a] -> [a] -> [a]
++ String
")", String
"fails", String
""]
        )
conformsToSpecE a
a (SuspendedSpec Var a
v Pred
ps) NonEmpty String
msgs =
  case Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
v a
a) NonEmpty String
msgs Pred
ps of
    Maybe (NonEmpty String)
Nothing -> forall a. Maybe a
Nothing
    Just NonEmpty String
es -> forall a. a -> Maybe a
Just (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"conformsToSpecE SuspendedSpec case on var " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var a
v forall a. [a] -> [a] -> [a]
++ String
" fails") forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
conformsToSpecE a
_ (ErrorSpec NonEmpty String
es) NonEmpty String
msgs = forall a. a -> Maybe a
Just (NonEmpty String
msgs forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"conformsToSpecE ErrorSpec case" forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)

conformsToSpec :: HasSpec a => a -> Specification a -> Bool
conformsToSpec :: forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec a
a Specification a
x = case forall a.
HasSpec a =>
a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE a
a Specification a
x (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"call to conformsToSpecE") of
  Maybe (NonEmpty String)
Nothing -> Bool
True
  Just NonEmpty String
_ -> Bool
False

satisfies :: forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies :: forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
e (ExplainSpec [] Specification a
s) = forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
e Specification a
s
satisfies Term a
e (ExplainSpec (String
x : [String]
xs) Specification a
s) = NonEmpty String -> Pred -> Pred
Explain (String
x forall a. a -> [a] -> NonEmpty a
:| [String]
xs) forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
e Specification a
s
satisfies Term a
_ Specification a
TrueSpec = Pred
TruePred
satisfies Term a
e (MemberSpec NonEmpty a
nonempty) = forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
True Term a
e NonEmpty a
nonempty
satisfies Term a
t (SuspendedSpec Var a
x Pred
p) = forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
Subst Var a
x Term a
t Pred
p
satisfies Term a
e (TypeSpec TypeSpec a
s [a]
cant) = case [a]
cant of
  [] -> forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds Term a
e TypeSpec a
s
  (a
c : [a]
cs) -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
False Term a
e (a
c forall a. a -> [a] -> NonEmpty a
:| [a]
cs) forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds Term a
e TypeSpec a
s
satisfies Term a
_ (ErrorSpec NonEmpty String
e) = NonEmpty String -> Pred
FalsePred NonEmpty String
e

-- ==================================================================

instance HasSpec a => Semigroup (Specification a) where
  ExplainSpec [String]
es Specification a
x <> :: Specification a -> Specification a -> Specification a
<> Specification a
y = forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (Specification a
x forall a. Semigroup a => a -> a -> a
<> Specification a
y)
  Specification a
x <> ExplainSpec [String]
es Specification a
y = forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (Specification a
x forall a. Semigroup a => a -> a -> a
<> Specification a
y)
  Specification a
TrueSpec <> Specification a
s = Specification a
s
  Specification a
s <> Specification a
TrueSpec = Specification a
s
  ErrorSpec NonEmpty String
e <> ErrorSpec NonEmpty String
e' =
    forall a. NonEmpty String -> Specification a
ErrorSpec
      ( NonEmpty String
e
          forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"------ spec <> spec ------ @" forall a. [a] -> [a] -> [a]
++ forall {k} (t :: k). Typeable t => String
showType @a)
          forall a. Semigroup a => a -> a -> a
<> NonEmpty String
e'
      )
  ErrorSpec NonEmpty String
e <> Specification a
_ = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
e
  Specification a
_ <> ErrorSpec NonEmpty String
e = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
e
  MemberSpec NonEmpty a
as <> MemberSpec NonEmpty a
as' =
    forall a. NonEmpty String -> Specification a -> Specification a
addToErrorSpec
      ( forall a. [a] -> NonEmpty a
NE.fromList
          [String
"Intersecting: ", String
"  MemberSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as), String
"  MemberSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as')]
      )
      ( forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
          (forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a] -> [a]
intersect (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as) (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as'))
          (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Empty intersection")
      )
  ms :: Specification a
ms@(MemberSpec NonEmpty a
as) <> ts :: Specification a
ts@TypeSpec {} =
    forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
      (forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> NonEmpty a -> [a]
NE.filter (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
ts) NonEmpty a
as)
      ( forall a. [a] -> NonEmpty a
NE.fromList
          [ String
"The two " forall a. [a] -> [a] -> [a]
++ forall {k} (t :: k). Typeable t => String
showType @a forall a. [a] -> [a] -> [a]
++ String
" Specifications are inconsistent."
          , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
ms
          , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
ts
          ]
      )
  TypeSpec TypeSpec a
s [a]
cant <> MemberSpec NonEmpty a
as = forall a. NonEmpty a -> Specification a
MemberSpec NonEmpty a
as forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec a
s [a]
cant
  SuspendedSpec Var a
v Pred
p <> SuspendedSpec Var a
v' Pred
p' = forall a. HasSpec a => Var a -> Pred -> Specification a
SuspendedSpec Var a
v (Pred
p forall a. Semigroup a => a -> a -> a
<> forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var a
v' Var a
v Pred
p')
  SuspendedSpec Var a
v Pred
ps <> Specification a
s = forall a. HasSpec a => Var a -> Pred -> Specification a
SuspendedSpec Var a
v (Pred
ps forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall a. HasSpec a => Var a -> Term a
V Var a
v) Specification a
s)
  Specification a
s <> SuspendedSpec Var a
v Pred
ps = forall a. HasSpec a => Var a -> Pred -> Specification a
SuspendedSpec Var a
v (Pred
ps forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall a. HasSpec a => Var a -> Term a
V Var a
v) Specification a
s)
  TypeSpec TypeSpec a
s [a]
cant <> TypeSpec TypeSpec a
s' [a]
cant' = case forall a. HasSpec a => TypeSpec a -> TypeSpec a -> Specification a
combineSpec TypeSpec a
s TypeSpec a
s' of
    -- NOTE: This might look like an unnecessary case, but doing
    -- it like this avoids looping.
    TypeSpec TypeSpec a
s'' [a]
cant'' -> forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec a
s'' ([a]
cant forall a. Semigroup a => a -> a -> a
<> [a]
cant' forall a. Semigroup a => a -> a -> a
<> [a]
cant'')
    Specification a
s'' -> Specification a
s'' forall a. Semigroup a => a -> a -> a
<> forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec ([a]
cant forall a. Semigroup a => a -> a -> a
<> [a]
cant')

instance HasSpec a => Monoid (Specification a) where
  mempty :: Specification a
mempty = forall a. Specification a
TrueSpec

-- =========================================================================

-- | Collect the 'monitor' calls from a specification instantiated to the given value. Typically,
--
--   >>> quickCheck $ forAll (genFromSpec spec) $ \ x -> monitorSpec spec x $ ...
monitorSpec :: Testable p => Specification a -> a -> p -> Property
monitorSpec :: forall p a. Testable p => Specification a -> a -> p -> Property
monitorSpec (SuspendedSpec Var a
x Pred
p) a
a =
  forall a. GE a -> a
errorGE (forall (m :: * -> *).
MonadGenError m =>
Env -> Pred -> m (Property -> Property)
monitorPred (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
a) Pred
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => prop -> Property
property
monitorSpec Specification a
_ a
_ = forall prop. Testable prop => prop -> Property
property

monitorPred ::
  forall m. MonadGenError m => Env -> Pred -> m (Property -> Property)
monitorPred :: forall (m :: * -> *).
MonadGenError m =>
Env -> Pred -> m (Property -> Property)
monitorPred Env
env = \case
  ElemPred {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id -- Not sure about this, but ElemPred is a lot like Assert, so ...
  Monitor (forall b. Term b -> b) -> Property -> Property
m -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ((forall b. Term b -> b) -> Property -> Property
m forall a b. (a -> b) -> a -> b
$ forall a. GE a -> a
errorGE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"monitorPred: Monitor" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env)
  Subst Var a
x Term a
t Pred
p -> forall (m :: * -> *).
MonadGenError m =>
Env -> Pred -> m (Property -> Property)
monitorPred Env
env forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
  Assert {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  GenHint {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  Reifies {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  ForAll Term t
t (Var a
x :-> Pred
p) -> do
    t
set <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term t
t
    forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
        [ forall (m :: * -> *).
MonadGenError m =>
Env -> Pred -> m (Property -> Property)
monitorPred Env
env' Pred
p
        | a
v <- forall t e. Forallable t e => t -> [e]
forAllToList t
set
        , let env' :: Env
env' = forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env
        ]
  Case Term (SumOver as)
t List (Weighted Binder) as
bs -> do
    SumOver as
v <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term (SumOver as)
t
    forall (as :: [*]) r.
SumOver as
-> List Binder as
-> (forall a. HasSpec a => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as
v (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing List (Weighted Binder) as
bs) (\Var a
x a
val Pred
ps -> forall (m :: * -> *).
MonadGenError m =>
Env -> Pred -> m (Property -> Property)
monitorPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) Pred
ps)
  When Term Bool
b Pred
p -> do
    Bool
v <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term Bool
b
    if Bool
v then forall (m :: * -> *).
MonadGenError m =>
Env -> Pred -> m (Property -> Property)
monitorPred Env
env Pred
p else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  Pred
TruePred -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  FalsePred {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  DependsOn {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  And [Pred]
ps -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
MonadGenError m =>
Env -> Pred -> m (Property -> Property)
monitorPred Env
env) [Pred]
ps
  Let Term a
t (Var a
x :-> Pred
p) -> do
    a
val <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term a
t
    forall (m :: * -> *).
MonadGenError m =>
Env -> Pred -> m (Property -> Property)
monitorPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) Pred
p
  Exists (forall b. Term b -> b) -> GE a
k (Var a
x :-> Pred
p) -> do
    case (forall b. Term b -> b) -> GE a
k (forall a. GE a -> a
errorGE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"monitorPred: Exists" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env) of
      Result a
a -> forall (m :: * -> *).
MonadGenError m =>
Env -> Pred -> m (Property -> Property)
monitorPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
a Env
env) Pred
p
      GE a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  Explain NonEmpty String
es Pred
p -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE NonEmpty String
es forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadGenError m =>
Env -> Pred -> m (Property -> Property)
monitorPred Env
env Pred
p