{-# 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.AbstractSyntax
import Constrained.Base (
  HasSpec,
  Pred,
  Specification,
  Term,
  addToErrorSpec,
  combineSpec,
  conformsTo,
  explainSpecOpt,
  forAllToList,
  memberSpecList,
  notMemberSpec,
  toPreds,
  pattern TypeSpec,
 )
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.PrettyUtils
import Constrained.Syntax (
  runCaseOn,
  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 TermD Deps a
term NonEmpty a
xs) -> do
    a
v <- Env -> TermD Deps a -> m a
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env TermD Deps a
term
    case (a -> NonEmpty a -> Bool
forall a. Eq a => a -> NonEmpty a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
v NonEmpty a
xs, Bool
bool) of
      (Bool
True, Bool
True) -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      (Bool
True, Bool
False) -> NonEmpty String -> m Bool
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (String
"notElemPred reduces to True" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [Pred -> String
forall a. Show a => a -> String
show Pred
p])
      (Bool
False, Bool
True) -> NonEmpty String -> m Bool
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (String
"elemPred reduces to False" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [Pred -> String
forall a. Show a => a -> String
show Pred
p])
      (Bool
False, Bool
False) -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  Monitor {} -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  Subst Var a
x TermD Deps a
t Pred
p -> Env -> Pred -> m Bool
forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred Env
env (Pred -> m Bool) -> Pred -> m Bool
forall a b. (a -> b) -> a -> b
$ Var a -> TermD Deps a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x TermD Deps a
t Pred
p
  Assert TermD Deps Bool
t -> Env -> TermD Deps Bool -> m Bool
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env TermD Deps Bool
t
  GenHint {} -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  p :: Pred
p@(Reifies TermD Deps b
t' TermD Deps a
t a -> b
f) -> do
    a
val <- Env -> TermD Deps a -> m a
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env TermD Deps a
t
    b
val' <- Env -> TermD Deps b -> m b
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env TermD Deps b
t'
    NonEmpty String -> m Bool -> m Bool
forall a. HasCallStack => NonEmpty String -> m a -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"Reification:", String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred -> String
forall a. Show a => a -> String
show Pred
p]) (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> b
f a
val b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
val')
  ForAll TermD Deps t
t (Var e
x :-> Pred
p) -> do
    t
set <- Env -> TermD Deps t -> m t
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env TermD Deps t
t
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      ([Bool] -> Bool) -> m [Bool] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m Bool] -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
        [ Env -> Pred -> m Bool
forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred Env
env' Pred
p
        | e
v <- t -> [e]
forall t e. Forallable t e => t -> [e]
forAllToList t
set
        , let env' :: Env
env' = Var e -> e -> Env -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var e
x e
v Env
env
        ]
  Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> do
    SumOver as
v <- Env -> TermD Deps (SumOver as) -> m (SumOver as)
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env TermD Deps (SumOver as)
t
    SumOver as
-> List (BinderD Deps) as
-> (forall a. (Typeable a, Show a) => Var a -> a -> Pred -> m Bool)
-> m Bool
forall (as :: [*]) r.
SumOver as
-> List (BinderD Deps) as
-> (forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as
v ((forall a. Weighted (BinderD Deps) a -> Binder a)
-> List (Weighted (BinderD Deps)) as -> List (BinderD Deps) as
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList Weighted (BinderD Deps) a -> Binder a
forall a. Weighted (BinderD Deps) a -> Binder a
forall (f :: * -> *) a. Weighted f a -> f a
thing List (Weighted (BinderD Deps)) as
bs) (\Var a
x a
val Pred
ps -> Env -> Pred -> m Bool
forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred (Var a -> a -> Env -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) Pred
ps)
  When TermD Deps Bool
bt Pred
p -> do
    Bool
b <- Env -> TermD Deps Bool -> m Bool
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env TermD Deps Bool
bt
    if Bool
b then Env -> Pred -> m Bool
forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred Env
env Pred
p else Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  Pred
TruePred -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  FalsePred NonEmpty String
es -> NonEmpty String -> m Bool -> m Bool
forall a. HasCallStack => NonEmpty String -> m a -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE NonEmpty String
es (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  DependsOn {} -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  And [Pred]
ps -> Env -> [Pred] -> m Bool
forall (m :: * -> *) (t :: * -> *).
(MonadGenError m, Traversable t) =>
Env -> t Pred -> m Bool
checkPreds Env
env [Pred]
ps
  Let TermD Deps a
t (Var a
x :-> Pred
p) -> do
    a
val <- Env -> TermD Deps a -> m a
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env TermD Deps a
t
    Env -> Pred -> m Bool
forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred (Var a -> a -> Env -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) Pred
p
  Exists (forall b. TermD Deps b -> b) -> GE a
k (Var a
x :-> Pred
p) -> do
    a
a <- GE a -> m a
forall (m :: * -> *) r. MonadGenError m => GE r -> m r
runGE (GE a -> m a) -> GE a -> m a
forall a b. (a -> b) -> a -> b
$ (forall b. TermD Deps b -> b) -> GE a
k (GE b -> b
forall a. GE a -> a
errorGE (GE b -> b) -> (TermD Deps b -> GE b) -> TermD Deps b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> GE b -> GE b
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"checkPred: Exists" (GE b -> GE b) -> (TermD Deps b -> GE b) -> TermD Deps b -> GE b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> TermD Deps b -> GE b
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env)
    Env -> Pred -> m Bool
forall (m :: * -> *). MonadGenError m => Env -> Pred -> m Bool
checkPred (Var a -> a -> Env -> Env
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 -> NonEmpty String -> m Bool -> m Bool
forall a. HasCallStack => NonEmpty String -> m a -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE NonEmpty String
es (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Env -> Pred -> m Bool
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 = t Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (t Bool -> Bool) -> m (t Bool) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pred -> m Bool) -> t Pred -> m (t Bool)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
mapM (Env -> Pred -> m Bool
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 = (NonEmpty (NonEmpty String) -> Bool) -> GE Bool -> Bool
forall a.
HasCallStack =>
(NonEmpty (NonEmpty String) -> a) -> GE a -> a
fromGE (Bool -> NonEmpty (NonEmpty String) -> Bool
forall a b. a -> b -> a
const Bool
False) (GE Bool -> Bool) -> GE Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Pred -> GE Bool
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 [Maybe (NonEmpty String)] -> [NonEmpty String]
forall a. [Maybe a] -> [a]
catMaybes ((Pred -> Maybe (NonEmpty String))
-> [Pred] -> [Maybe (NonEmpty String)]
forall a b. (a -> b) -> [a] -> [b]
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
    [] -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
    (NonEmpty String
x : [NonEmpty String]
xs) -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String -> NonEmpty String
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (NonEmpty (NonEmpty String) -> NonEmpty String
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty String
x NonEmpty String -> [NonEmpty String] -> NonEmpty (NonEmpty String)
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 TermD Deps a
t NonEmpty a
xs) ->
    case Env -> TermD Deps a -> Either (NonEmpty String) a
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env TermD Deps a
t of
      Left NonEmpty String
message -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
message)
      Right a
v -> case (a -> NonEmpty a -> Bool
forall a. Eq a => a -> NonEmpty a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
v NonEmpty a
xs, Bool
bool) of
        (Bool
True, Bool
True) -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
        (Bool
True, Bool
False) -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (String
"notElemPred reduces to True" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [Pred -> String
forall a. Show a => a -> String
show Pred
p])
        (Bool
False, Bool
True) -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (String
"elemPred reduces to False" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [Pred -> String
forall a. Show a => a -> String
show Pred
p])
        (Bool
False, Bool
False) -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
  Monitor {} -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
  Subst Var a
x TermD Deps a
t Pred
p -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env NonEmpty String
msgs (Pred -> Maybe (NonEmpty String))
-> Pred -> Maybe (NonEmpty String)
forall a b. (a -> b) -> a -> b
$ Var a -> TermD Deps a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x TermD Deps a
t Pred
p
  Assert TermD Deps Bool
t -> case Env -> TermD Deps Bool -> Either (NonEmpty String) Bool
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env TermD Deps Bool
t of
    Right Bool
True -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
    Right Bool
False ->
      NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just
        (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TermD Deps Bool -> String
forall a. Show a => a -> String
show TermD Deps Bool
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" returns False") NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"\nenv=\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Env -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Env -> Doc ann
pretty Env
env)))
    Left NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  GenHint {} -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
  p :: Pred
p@(Reifies TermD Deps b
t' TermD Deps a
t a -> b
f) ->
    case Env -> TermD Deps a -> Either (NonEmpty String) a
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env TermD Deps a
t of
      Left NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"checkPredE: Reification fails", String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred -> String
forall a. Show a => a -> String
show Pred
p] NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
      Right a
val -> case Env -> TermD Deps b -> Either (NonEmpty String) b
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env TermD Deps b
t' of
        Left NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"checkPredE: Reification fails", String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred -> String
forall a. Show a => a -> String
show Pred
p] NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
        Right b
val' ->
          if a -> b
f a
val b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
val'
            then Maybe (NonEmpty String)
forall a. Maybe a
Nothing
            else
              NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just
                ( NonEmpty String
msgs
                    NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
                      [ String
"checkPredE: Reification doesn't match up"
                      , String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred -> String
forall a. Show a => a -> String
show Pred
p
                      , b -> String
forall a. Show a => a -> String
show (a -> b
f a
val) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" /= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
val'
                      ]
                )
  ForAll TermD Deps t
t (Var e
x :-> Pred
p) -> case Env -> TermD Deps t -> Either (NonEmpty String) t
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env TermD Deps t
t of
    Left NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String -> Maybe (NonEmpty String))
-> NonEmpty String -> Maybe (NonEmpty String)
forall a b. (a -> b) -> a -> b
$ (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"checkPredE: ForAll fails to run."] NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
    Right t
set ->
      let answers :: [NonEmpty String]
answers =
            [Maybe (NonEmpty String)] -> [NonEmpty String]
forall a. [Maybe a] -> [a]
catMaybes
              [ Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env' (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Some items in ForAll fail") Pred
p
              | e
v <- t -> [e]
forall t e. Forallable t e => t -> [e]
forAllToList t
set
              , let env' :: Env
env' = Var e -> e -> Env -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var e
x e
v Env
env
              ]
       in case [NonEmpty String]
answers of
            [] -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
            (NonEmpty String
y : [NonEmpty String]
ys) -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String -> NonEmpty String
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (NonEmpty (NonEmpty String) -> NonEmpty String
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty String
y NonEmpty String -> [NonEmpty String] -> NonEmpty (NonEmpty String)
forall a. a -> [a] -> NonEmpty a
NE.:| [NonEmpty String]
ys)))
  Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> case Env
-> TermD Deps (SumOver as) -> Either (NonEmpty String) (SumOver as)
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env TermD Deps (SumOver as)
t of
    Right SumOver as
v -> SumOver as
-> List (BinderD Deps) as
-> (forall a.
    (Typeable a, Show a) =>
    Var a -> a -> Pred -> Maybe (NonEmpty String))
-> Maybe (NonEmpty String)
forall (as :: [*]) r.
SumOver as
-> List (BinderD Deps) as
-> (forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as
v ((forall a. Weighted (BinderD Deps) a -> Binder a)
-> List (Weighted (BinderD Deps)) as -> List (BinderD Deps) as
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList Weighted (BinderD Deps) a -> Binder a
forall a. Weighted (BinderD Deps) a -> Binder a
forall (f :: * -> *) a. Weighted f a -> f a
thing List (Weighted (BinderD Deps)) as
bs) (\Var a
x a
val Pred
ps -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (Var a -> a -> Env -> Env
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 -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: Case fails" NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  When TermD Deps Bool
bt Pred
p -> case Env -> TermD Deps Bool -> Either (NonEmpty String) Bool
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env TermD Deps 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 Maybe (NonEmpty String)
forall a. Maybe a
Nothing
    Left NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: When fails" NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  Pred
TruePred -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
  FalsePred NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: FalsePred" NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  DependsOn {} -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
  And [Pred]
ps ->
    case [Maybe (NonEmpty String)] -> [NonEmpty String]
forall a. [Maybe a] -> [a]
catMaybes ((Pred -> Maybe (NonEmpty String))
-> [Pred] -> [Maybe (NonEmpty String)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Some items in And  fail")) [Pred]
ps) of
      [] -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
      (NonEmpty String
x : [NonEmpty String]
xs) -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String -> NonEmpty String
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (NonEmpty (NonEmpty String) -> NonEmpty String
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty String
x NonEmpty String -> [NonEmpty String] -> NonEmpty (NonEmpty String)
forall a. a -> [a] -> NonEmpty a
NE.:| [NonEmpty String]
xs)))
  Let TermD Deps a
t (Var a
x :-> Pred
p) -> case Env -> TermD Deps a -> Either (NonEmpty String) a
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env TermD Deps a
t of
    Right a
val -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (Var a -> a -> Env -> Env
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 -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: Let fails" NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  Exists (forall b. TermD Deps b -> b) -> GE a
k (Var a
x :-> Pred
p) ->
    let eval :: forall b. Term b -> b
        eval :: forall b. TermD Deps b -> b
eval Term b
term = case Env -> Term b -> Either (NonEmpty String) b
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env Term b
term of
          Right b
v -> b
v
          Left NonEmpty String
es -> String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
NE.toList (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
     in case (forall b. TermD Deps b -> b) -> GE a
k Term b -> b
forall b. TermD Deps b -> b
eval of
          Result a
a -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (Var a -> a -> Env -> Env
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 -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty (NonEmpty String) -> NonEmpty String
catMessageList NonEmpty (NonEmpty String)
es)
          GenError NonEmpty (NonEmpty String)
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
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 NonEmpty String -> NonEmpty String -> NonEmpty String
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 [] SpecificationD Deps a
s) NonEmpty String
msgs = a
-> SpecificationD Deps a
-> NonEmpty String
-> Maybe (NonEmpty String)
forall a.
HasSpec a =>
a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE a
a SpecificationD Deps a
s NonEmpty String
msgs
conformsToSpecE a
a (ExplainSpec (String
x : [String]
xs) SpecificationD Deps a
s) NonEmpty String
msgs = a
-> SpecificationD Deps a
-> NonEmpty String
-> Maybe (NonEmpty String)
forall a.
HasSpec a =>
a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE a
a SpecificationD Deps a
s ((String
x String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [String]
xs) NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
msgs)
conformsToSpecE a
_ SpecificationD Deps a
TrueSpec NonEmpty String
_ = Maybe (NonEmpty String)
forall a. Maybe a
Nothing
conformsToSpecE a
a (MemberSpec NonEmpty a
as) NonEmpty String
msgs =
  if a -> NonEmpty a -> Bool
forall a. Eq a => a -> NonEmpty a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
a NonEmpty a
as
    then Maybe (NonEmpty String)
forall a. Maybe a
Nothing
    else
      NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just
        ( NonEmpty String
msgs
            NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
              [String
"conformsToSpecE MemberSpec case", String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a, String
"  not an element of", String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty a -> String
forall a. Show a => a -> String
show NonEmpty a
as, String
""]
        )
conformsToSpecE a
a spec :: SpecificationD Deps a
spec@(TypeSpec TypeSpec a
s [a]
cant) NonEmpty String
msgs =
  if a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem a
a [a]
cant Bool -> Bool -> Bool
&& a -> TypeSpec a -> Bool
forall a. (HasSpec a, HasCallStack) => a -> TypeSpec a -> Bool
conformsTo a
a TypeSpec a
s
    then Maybe (NonEmpty String)
forall a. Maybe a
Nothing
    else
      NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just
        ( NonEmpty String
msgs
            NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
              [String
"conformsToSpecE TypeSpec case", String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a, String
"  (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecificationD Deps a -> String
forall a. Show a => a -> String
show SpecificationD Deps a
spec String -> String -> String
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 (Var a -> a -> Env
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 -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
    Just NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"conformsToSpecE SuspendedSpec case on var " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Var a -> String
forall a. Show a => a -> String
show Var a
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" fails") NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
conformsToSpecE a
_ (ErrorSpec NonEmpty String
es) NonEmpty String
msgs = NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"conformsToSpecE ErrorSpec case" NonEmpty String -> NonEmpty String -> NonEmpty String
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 a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
forall a.
HasSpec a =>
a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE a
a Specification a
x (String -> NonEmpty String
forall a. a -> NonEmpty a
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 [] SpecificationD Deps a
s) = Term a -> SpecificationD Deps a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
e SpecificationD Deps a
s
satisfies Term a
e (ExplainSpec (String
x : [String]
xs) SpecificationD Deps a
s) = NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain (String
x String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [String]
xs) (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Term a -> SpecificationD Deps a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
e SpecificationD Deps a
s
satisfies Term a
_ SpecificationD Deps a
TrueSpec = Pred
forall deps. PredD deps
TruePred
satisfies Term a
e (MemberSpec NonEmpty a
nonempty) = Bool -> Term a -> NonEmpty a -> Pred
forall deps a.
(HasSpecD deps a, Show a) =>
Bool -> TermD deps a -> NonEmpty a -> PredD deps
ElemPred Bool
True Term a
e NonEmpty a
nonempty
satisfies Term a
t (SuspendedSpec Var a
x Pred
p) = Var a -> Term a -> Pred -> Pred
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> TermD deps a -> PredD deps -> PredD deps
Subst Var a
x Term a
t Pred
p
satisfies Term a
e (TypeSpec TypeSpec a
s [a]
cant) = case [a]
cant of
  [] -> Term a -> TypeSpec a -> Pred
forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds Term a
e TypeSpec a
s
  (a
c : [a]
cs) -> Bool -> Term a -> NonEmpty a -> Pred
forall deps a.
(HasSpecD deps a, Show a) =>
Bool -> TermD deps a -> NonEmpty a -> PredD deps
ElemPred Bool
False Term a
e (a
c a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
cs) Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term a -> TypeSpec a -> Pred
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
forall deps. NonEmpty String -> PredD deps
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 = [String] -> Specification a -> Specification a
forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (Specification a
x Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> Specification a
y)
  Specification a
x <> ExplainSpec [String]
es Specification a
y = [String] -> Specification a -> Specification a
forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (Specification a
x Specification a -> Specification a -> Specification a
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' =
    NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec
      ( NonEmpty String
e
          NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"------ spec <> spec ------ @" String -> String -> String
forall a. [a] -> [a] -> [a]
++ forall t. Typeable t => String
forall {k} (t :: k). Typeable t => String
showType @a)
          NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
e'
      )
  ErrorSpec NonEmpty String
e <> Specification a
_ = NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec NonEmpty String
e
  Specification a
_ <> ErrorSpec NonEmpty String
e = NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec NonEmpty String
e
  MemberSpec NonEmpty a
as <> MemberSpec NonEmpty a
as' =
    NonEmpty String -> Specification a -> Specification a
forall a. NonEmpty String -> Specification a -> Specification a
addToErrorSpec
      ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [String
"Intersecting: ", String
"  MemberSpec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as), String
"  MemberSpec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as')]
      )
      ( [a] -> NonEmpty String -> Specification a
forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
          ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
intersect (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as) (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as'))
          (String -> NonEmpty String
forall a. a -> NonEmpty a
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 {} =
    [a] -> NonEmpty String -> Specification a
forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
      ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> NonEmpty a -> [a]
forall a. (a -> Bool) -> NonEmpty a -> [a]
NE.filter (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
ts) NonEmpty a
as)
      ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [ String
"The two " String -> String -> String
forall a. [a] -> [a] -> [a]
++ forall t. Typeable t => String
forall {k} (t :: k). Typeable t => String
showType @a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" Specifications are inconsistent."
          , String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
ms
          , String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Specification a -> String
forall a. Show a => a -> String
show Specification a
ts
          ]
      )
  TypeSpec TypeSpec a
s [a]
cant <> MemberSpec NonEmpty a
as = NonEmpty a -> Specification a
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec NonEmpty a
as Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> TypeSpec a -> [a] -> Specification 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' = Var a -> Pred -> Specification a
forall deps a.
HasSpecD deps a =>
Var a -> PredD deps -> SpecificationD deps a
SuspendedSpec Var a
v (Pred
p Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Var a -> Var a -> Pred -> Pred
forall x. Typeable x => Var x -> Var x -> Pred -> Pred
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 = Var a -> Pred -> Specification a
forall deps a.
HasSpecD deps a =>
Var a -> PredD deps -> SpecificationD deps a
SuspendedSpec Var a
v (Pred
ps Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
v) Specification a
s)
  Specification a
s <> SuspendedSpec Var a
v Pred
ps = Var a -> Pred -> Specification a
forall deps a.
HasSpecD deps a =>
Var a -> PredD deps -> SpecificationD deps a
SuspendedSpec Var a
v (Pred
ps Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
v) Specification a
s)
  TypeSpec TypeSpec a
s [a]
cant <> TypeSpec TypeSpec a
s' [a]
cant' = case TypeSpec a -> TypeSpec a -> Specification a
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'' -> TypeSpec a -> [a] -> Specification a
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec a
s'' ([a]
cant [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
cant' [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
cant'')
    Specification a
s'' -> Specification a
s'' Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> [a] -> Specification a
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec ([a]
cant [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
cant')

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