input-output-hk / constrained-generators / 371

Committed 04 Nov 2025 12:59PM UTC coverage: 77.171% (+0.06%) from 77.113%

Build # 371

Build Type

push

github

Committed by

web-flow

Commit Message

Improve shrinking performance (#53)

Run Details

16 of 17 new or added lines in 1 file covered. (94.12%)

89 existing lines in 2 files now uncovered.

3901 of 5055 relevant lines covered (77.17%)

1.46 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

79.27

/src/Constrained/Conformance.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
-- Semigroup (Specification a), Monoid (Specification a)
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Functions primarily for checking that a value conforms to a
-- `Specification`
module Constrained.Conformance (
  monitorSpec,
  conformsToSpec,
  conformsToSpecE,
  satisfies,
  checkPredE,
  checkPredsE,
) where

import Constrained.AbstractSyntax
import Constrained.Base
import Constrained.Core
import Constrained.Env
import Constrained.Env qualified as Env
import Constrained.GenT
import Constrained.List
import Constrained.PrettyUtils
import Constrained.Syntax
import Data.List (intersect, nub)
import Data.List.NonEmpty qualified as NE
import Data.Maybe
import Data.Semigroup (sconcat)
import Prettyprinter hiding (cat)
import Test.QuickCheck (Property, Testable, property)

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

-- | Like checkPredE, 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 msgs env ps =
  case catMaybes (fmap (checkPredE env msgs) ps) of
    [] -> Nothing
    (x : xs) -> Just (NE.nub (sconcat (x NE.:| xs)))

-- | Does the Pred evaluate to true under the given Env. An involved
-- explanation for a single Pred in case of failure and `Nothing` otherwise.
-- The most important explanations come when an assertion fails.
checkPredE :: Env -> NE.NonEmpty String -> Pred -> Maybe (NE.NonEmpty String)
checkPredE env msgs = \case
  p@(ElemPred bool t xs) ->
    case runTermE env t of
      Left message -> Just (msgs <> message)
      Right v -> case (elem v xs, bool) of
        (True, True) -> Nothing
        (True, False) -> Just ("notElemPred reduces to True" :| [show p])
        (False, True) -> Just ("elemPred reduces to False" :| [show p])
        (False, False) -> Nothing
  Monitor {} -> Nothing
  Subst x t p -> checkPredE env msgs $ substitutePred x t p
  Assert t -> case runTermE env t of
    Right True -> Nothing
    Right False ->
      Just
        (msgs <> pure ("Assert " ++ show t ++ " returns False") <> pure ("\nenv=\n" ++ show (pretty env)))
    Left es -> Just (msgs <> es)
  GenHint {} -> Nothing
  p@(Reifies t' t f) ->
    case runTermE env t of
      Left es -> Just (msgs <> NE.fromList ["checkPredE: Reification fails", "  " ++ show p] <> es)
      Right val -> case runTermE env t' of
        Left es -> Just (msgs <> NE.fromList ["checkPredE: Reification fails", "  " ++ show p] <> es)
        Right val' ->
          if f val == val'
            then Nothing
            else
              Just
                ( msgs
                    <> NE.fromList
                      [ "checkPredE: Reification doesn't match up"
                      , "  " ++ show p
                      , show (f val) ++ " /= " ++ show val'
                      ]
                )
  ForAll t (x :-> p) -> case runTermE env t of
    Left es -> Just $ (msgs <> NE.fromList ["checkPredE: ForAll fails to run."] <> es)
    Right set ->
      let answers =
            catMaybes
              [ checkPredE env' (pure "Some items in ForAll fail") p
              | v <- forAllToList set
              , let env' = Env.extend x v env
              ]
       in case answers of
            [] -> Nothing
            (y : ys) -> Just (NE.nub (sconcat (y NE.:| ys)))
  Case t bs -> case runTermE env t of
    Right v -> runCaseOn v (mapList thing bs) (\x val ps -> checkPredE (Env.extend x val env) msgs ps)
    Left es -> Just (msgs <> pure "checkPredE: Case fails" <> es)
  When bt p -> case runTermE env bt of
    Right b -> if b then checkPredE env msgs p else Nothing
    Left es -> Just (msgs <> pure "checkPredE: When fails" <> es)
  TruePred -> Nothing
  FalsePred es -> Just (msgs <> pure "checkPredE: FalsePred" <> es)
  DependsOn {} -> Nothing
  And ps ->
    case catMaybes (fmap (checkPredE env (pure "Some items in And  fail")) ps) of
      [] -> Nothing
      (x : xs) -> Just (msgs <> NE.nub (sconcat (x NE.:| xs)))
  Let t (x :-> p) -> case runTermE env t of
    Right val -> checkPredE (Env.extend x val env) msgs p
    Left es -> Just (msgs <> pure "checkPredE: Let fails" <> es)
  Exists k (x :-> p) ->
    let eval :: forall b. Term b -> b
        eval term = case runTermE env term of
          Right v -> v
          Left es -> error $ unlines $ NE.toList (msgs <> es)
     in case k eval of
          Result a -> checkPredE (Env.extend x a env) msgs p
          FatalError es -> Just (msgs <> catMessageList es)
          GenError es -> Just (msgs <> catMessageList es)
  Explain es p -> checkPredE env (msgs <> es) 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 a (ExplainSpec [] s) msgs = conformsToSpecE a s msgs
conformsToSpecE a (ExplainSpec (x : xs) s) msgs = conformsToSpecE a s ((x :| xs) <> msgs)
conformsToSpecE _ TrueSpec _ = Nothing
conformsToSpecE a (MemberSpec as) msgs =
  if elem a as
    then Nothing
    else
      Just
        ( msgs
            <> NE.fromList
              ["conformsToSpecE MemberSpec case", "  " ++ show a, "  not an element of", "  " ++ show as, ""]
        )
conformsToSpecE a spec@(TypeSpec s cant) msgs =
  if notElem a cant && conformsTo a s
    then Nothing
    else
      Just
        ( msgs
            <> NE.fromList
              ["conformsToSpecE TypeSpec case", "  " ++ show a, "  (" ++ show spec ++ ")", "fails", ""]
        )
conformsToSpecE a (SuspendedSpec v ps) msgs =
  case checkPredE (Env.singleton v a) msgs ps of
    Nothing -> Nothing
    Just es -> Just (pure ("conformsToSpecE SuspendedSpec case on var " ++ show v ++ " fails") <> es)
conformsToSpecE _ (ErrorSpec es) msgs = Just (msgs <> pure "conformsToSpecE ErrorSpec case" <> es)

-- | Check if an @a@ conforms to a @`Specification` a@
conformsToSpec :: HasSpec a => a -> Specification a -> Bool
conformsToSpec a x = case conformsToSpecE a x (pure "call to conformsToSpecE") of
  Nothing -> True
  Just _ -> False

-- | Embed a `Specification` in a `Pred`. Useful for re-using `Specification`s
satisfies :: forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies e (ExplainSpec [] s) = satisfies e s
satisfies e (ExplainSpec (x : xs) s) = Explain (x :| xs) $ satisfies e s
satisfies _ TrueSpec = TruePred
satisfies e (MemberSpec nonempty) = ElemPred True e nonempty
satisfies t (SuspendedSpec x p) = Subst x t p
satisfies e (TypeSpec s cant) = case cant of
  [] -> toPreds e s
  (c : cs) -> ElemPred False e (c :| cs) <> toPreds e s
satisfies _ (ErrorSpec e) = FalsePred e

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

instance HasSpec a => Semigroup (Specification a) where
  ExplainSpec es x <> y = explainSpec es (x <> y)
  x <> ExplainSpec es y = explainSpec es (x <> y)
  TrueSpec <> s = s
  s <> TrueSpec = s
  ErrorSpec e <> ErrorSpec e' =
    ErrorSpec
      ( e
          <> pure ("------ spec <> spec ------ @" ++ showType @a)
          <> e'
      )
  ErrorSpec e <> _ = ErrorSpec e
  _ <> ErrorSpec e = ErrorSpec e
  MemberSpec as <> MemberSpec as' =
    addToErrorSpec
      ( NE.fromList
          ["Intersecting: ", "  MemberSpec " ++ show (NE.toList as), "  MemberSpec " ++ show (NE.toList as')]
      )
      ( memberSpec
          (nub $ intersect (NE.toList as) (NE.toList as'))
          (pure "Empty intersection")
      )
  ms@(MemberSpec as) <> ts@TypeSpec {} =
    memberSpec
      (nub $ NE.filter (`conformsToSpec` ts) as)
      ( NE.fromList
          [ "The two " ++ showType @a ++ " Specifications are inconsistent."
          , "  " ++ show ms
          , "  " ++ show ts
          ]
      )
  TypeSpec s cant <> MemberSpec as = MemberSpec as <> TypeSpec s cant
  SuspendedSpec v p <> SuspendedSpec v' p' = SuspendedSpec v (p <> rename v' v p')
  SuspendedSpec v ps <> s = SuspendedSpec v (ps <> satisfies (V v) s)
  s <> SuspendedSpec v ps = SuspendedSpec v (ps <> satisfies (V v) s)
  TypeSpec s cant <> TypeSpec s' cant' = case combineSpec s s' of
    -- NOTE: This might look like an unnecessary case, but doing
    -- it like this avoids looping.
    TypeSpec s'' cant'' -> TypeSpec s'' (cant <> cant' <> cant'')
    s'' -> s'' <> notMemberSpec (cant <> cant')

instance HasSpec a => Monoid (Specification a) where
  mempty = 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 (SuspendedSpec x p) a =
  errorGE (monitorPred (Env.singleton x a) p) . property
monitorSpec _ _ = property

monitorPred ::
  forall m. MonadGenError m => Env -> Pred -> m (Property -> Property)
monitorPred env = \case
  ElemPred {} -> pure id -- Not sure about this, but ElemPred is a lot like Assert, so ...
  Monitor m -> pure (m $ errorGE . explain "monitorPred: Monitor" . runTerm env)
  Subst x t p -> monitorPred env $ substitutePred x t p
  Assert {} -> pure id
  GenHint {} -> pure id
  Reifies {} -> pure id
  ForAll t (x :-> p) -> do
    set <- runTerm env t
    foldr (.) id
      <$> sequence
        [ monitorPred env' p
        | v <- forAllToList set
        , let env' = Env.extend x v env
        ]
  Case t bs -> do
    v <- runTerm env t
    runCaseOn v (mapList thing bs) (\x val ps -> monitorPred (Env.extend x val env) ps)
  When b p -> do
    v <- runTerm env b
    if v then monitorPred env p else pure id
  TruePred -> pure id
  FalsePred {} -> pure id
  DependsOn {} -> pure id
  And ps -> foldr (.) id <$> mapM (monitorPred env) ps
  Let t (x :-> p) -> do
    val <- runTerm env t
    monitorPred (Env.extend x val env) p
  Exists k (x :-> p) -> do
    case k (errorGE . explain "monitorPred: Exists" . runTerm env) of
      Result a -> monitorPred (Env.extend x a env) p
      _ -> pure id
  Explain es p -> explainNE es $ monitorPred env p

1	{-# LANGUAGE FlexibleInstances #-}
2	{-# LANGUAGE ImportQualifiedPost #-}
3	{-# LANGUAGE LambdaCase #-}
4	{-# LANGUAGE PatternSynonyms #-}
5	{-# LANGUAGE ScopedTypeVariables #-}
6	{-# LANGUAGE TypeApplications #-}
7	-- Semigroup (Specification a), Monoid (Specification a)
8	{-# OPTIONS_GHC -Wno-orphans #-}
9
10	-- \| Functions primarily for checking that a value conforms to a
11	-- `Specification`
12	module Constrained.Conformance (
13	monitorSpec,
14	conformsToSpec,
15	conformsToSpecE,
16	satisfies,
17	checkPredE,
18	checkPredsE,
19	) where
20
21	import Constrained.AbstractSyntax
22	import Constrained.Base
23	import Constrained.Core
24	import Constrained.Env
25	import Constrained.Env qualified as Env
26	import Constrained.GenT
27	import Constrained.List
28	import Constrained.PrettyUtils
29	import Constrained.Syntax
30	import Data.List (intersect, nub)
31	import Data.List.NonEmpty qualified as NE
32	import Data.Maybe
33	import Data.Semigroup (sconcat)
34	import Prettyprinter hiding (cat)
35	import Test.QuickCheck (Property, Testable, property)
36
37	-- ==========================================================
38
39	-- \| Like checkPredE, But it takes [Pred] rather than a single Pred,
40	-- and it builds a much more involved explanation if it fails.
41	-- Does the Pred evaluate to True under the given Env?
42	-- If it doesn't, an involved explanation appears in the (Just message)
43	-- If it does, then it returns Nothing
44	checkPredsE ::
45	NE.NonEmpty String ->
46	Env ->
47	[Pred] ->
48	Maybe (NE.NonEmpty String)
49	checkPredsE msgs env ps =	2✔
50	case catMaybes (fmap (checkPredE env msgs) ps) of	1✔
51	[] -> Nothing	2✔
52	(x : xs) -> Just (NE.nub (sconcat (x NE.:\| xs)))	1✔
53
54	-- \| Does the Pred evaluate to true under the given Env. An involved
55	-- explanation for a single Pred in case of failure and `Nothing` otherwise.
56	-- The most important explanations come when an assertion fails.
57	checkPredE :: Env -> NE.NonEmpty String -> Pred -> Maybe (NE.NonEmpty String)
58	checkPredE env msgs = \case	2✔
59	p@(ElemPred bool t xs) ->
60	case runTermE env t of	2✔
61	Left message -> Just (msgs <> message)	×
62	Right v -> case (elem v xs, bool) of	2✔
63	(True, True) -> Nothing	2✔
64	(True, False) -> Just ("notElemPred reduces to True" :\| [show p])	1✔
65	(False, True) -> Just ("elemPred reduces to False" :\| [show p])	1✔
66	(False, False) -> Nothing	2✔
67	Monitor {} -> Nothing	×
68	Subst x t p -> checkPredE env msgs $ substitutePred x t p	1✔
69	Assert t -> case runTermE env t of	2✔
70	Right True -> Nothing	2✔
71	Right False ->
72	Just	2✔
73	(msgs <> pure ("Assert " ++ show t ++ " returns False") <> pure ("\nenv=\n" ++ show (pretty env)))	×
74	Left es -> Just (msgs <> es)	×
75	GenHint {} -> Nothing	2✔
76	p@(Reifies t' t f) ->
77	case runTermE env t of	2✔
78	Left es -> Just (msgs <> NE.fromList ["checkPredE: Reification fails", " " ++ show p] <> es)	×
79	Right val -> case runTermE env t' of	2✔
80	Left es -> Just (msgs <> NE.fromList ["checkPredE: Reification fails", " " ++ show p] <> es)	×
81	Right val' ->
82	if f val == val'	1✔
83	then Nothing	2✔
84	else
UNCOV 85	Just	×
86	( msgs	×
87	<> NE.fromList	×
88	[ "checkPredE: Reification doesn't match up"	×
89	, " " ++ show p	×
90	, show (f val) ++ " /= " ++ show val'	×
91	]
92	)
93	ForAll t (x :-> p) -> case runTermE env t of	2✔
94	Left es -> Just $ (msgs <> NE.fromList ["checkPredE: ForAll fails to run."] <> es)	×
95	Right set ->
96	let answers =	2✔
97	catMaybes	2✔
98	[ checkPredE env' (pure "Some items in ForAll fail") p	1✔
99	\| v <- forAllToList set	2✔
100	, let env' = Env.extend x v env	2✔
101	]
102	in case answers of	2✔
103	[] -> Nothing	2✔
104	(y : ys) -> Just (NE.nub (sconcat (y NE.:\| ys)))	1✔
105	Case t bs -> case runTermE env t of	2✔
106	Right v -> runCaseOn v (mapList thing bs) (\x val ps -> checkPredE (Env.extend x val env) msgs ps)	1✔
107	Left es -> Just (msgs <> pure "checkPredE: Case fails" <> es)	×
108	When bt p -> case runTermE env bt of	2✔
109	Right b -> if b then checkPredE env msgs p else Nothing	1✔
110	Left es -> Just (msgs <> pure "checkPredE: When fails" <> es)	×
111	TruePred -> Nothing	2✔
112	FalsePred es -> Just (msgs <> pure "checkPredE: FalsePred" <> es)	1✔
113	DependsOn {} -> Nothing	2✔
114	And ps ->
115	case catMaybes (fmap (checkPredE env (pure "Some items in And fail")) ps) of	1✔
116	[] -> Nothing	2✔
117	(x : xs) -> Just (msgs <> NE.nub (sconcat (x NE.:\| xs)))	1✔
118	Let t (x :-> p) -> case runTermE env t of	2✔
119	Right val -> checkPredE (Env.extend x val env) msgs p	1✔
120	Left es -> Just (msgs <> pure "checkPredE: Let fails" <> es)	×
121	Exists k (x :-> p) ->
122	let eval :: forall b. Term b -> b	2✔
123	eval term = case runTermE env term of	2✔
124	Right v -> v	2✔
125	Left es -> error $ unlines $ NE.toList (msgs <> es)	×
126	in case k eval of	2✔
127	Result a -> checkPredE (Env.extend x a env) msgs p	1✔
128	FatalError es -> Just (msgs <> catMessageList es)	1✔
129	GenError es -> Just (msgs <> catMessageList es)	×
130	Explain es p -> checkPredE env (msgs <> es) p	1✔
131
132	-- \| @conformsToSpec@ with explanation. Nothing if (conformsToSpec a spec),
133	-- but (Just explanations) if not(conformsToSpec a spec).
134	conformsToSpecE ::
135	forall a.
136	HasSpec a =>
137	a ->
138	Specification a ->
139	NE.NonEmpty String ->
140	Maybe (NE.NonEmpty String)
141	conformsToSpecE a (ExplainSpec [] s) msgs = conformsToSpecE a s msgs	1✔
142	conformsToSpecE a (ExplainSpec (x : xs) s) msgs = conformsToSpecE a s ((x :\| xs) <> msgs)	1✔
143	conformsToSpecE _ TrueSpec _ = Nothing	2✔
144	conformsToSpecE a (MemberSpec as) msgs =
145	if elem a as	2✔
146	then Nothing	2✔
147	else
148	Just	2✔
149	( msgs	×
150	<> NE.fromList	×
151	["conformsToSpecE MemberSpec case", " " ++ show a, " not an element of", " " ++ show as, ""]	×
152	)
153	conformsToSpecE a spec@(TypeSpec s cant) msgs =
154	if notElem a cant && conformsTo a s	2✔
155	then Nothing	2✔
156	else
157	Just	2✔
158	( msgs	×
159	<> NE.fromList	×
160	["conformsToSpecE TypeSpec case", " " ++ show a, " (" ++ show spec ++ ")", "fails", ""]	×
161	)
162	conformsToSpecE a (SuspendedSpec v ps) msgs =
163	case checkPredE (Env.singleton v a) msgs ps of	1✔
164	Nothing -> Nothing	2✔
165	Just es -> Just (pure ("conformsToSpecE SuspendedSpec case on var " ++ show v ++ " fails") <> es)	1✔
166	conformsToSpecE _ (ErrorSpec es) msgs = Just (msgs <> pure "conformsToSpecE ErrorSpec case" <> es)	1✔
167
168	-- \| Check if an @a@ conforms to a @`Specification` a@
169	conformsToSpec :: HasSpec a => a -> Specification a -> Bool
170	conformsToSpec a x = case conformsToSpecE a x (pure "call to conformsToSpecE") of	1✔
171	Nothing -> True	2✔
172	Just _ -> False	2✔
173
174	-- \| Embed a `Specification` in a `Pred`. Useful for re-using `Specification`s
175	satisfies :: forall a. HasSpec a => Term a -> Specification a -> Pred
176	satisfies e (ExplainSpec [] s) = satisfies e s	1✔
177	satisfies e (ExplainSpec (x : xs) s) = Explain (x :\| xs) $ satisfies e s	1✔
178	satisfies _ TrueSpec = TruePred	2✔
179	satisfies e (MemberSpec nonempty) = ElemPred True e nonempty	2✔
180	satisfies t (SuspendedSpec x p) = Subst x t p	2✔
181	satisfies e (TypeSpec s cant) = case cant of	2✔
182	[] -> toPreds e s	2✔
183	(c : cs) -> ElemPred False e (c :\| cs) <> toPreds e s	2✔
184	satisfies _ (ErrorSpec e) = FalsePred e	1✔
185
186	-- ==================================================================
187
188	instance HasSpec a => Semigroup (Specification a) where	×
189	ExplainSpec es x <> y = explainSpec es (x <> y)	2✔
190	x <> ExplainSpec es y = explainSpec es (x <> y)	2✔
191	TrueSpec <> s = s	2✔
192	s <> TrueSpec = s	2✔
193	ErrorSpec e <> ErrorSpec e' =
194	ErrorSpec	2✔
195	( e	×
196	<> pure ("------ spec <> spec ------ @" ++ showType @a)	×
197	<> e'	×
198	)
199	ErrorSpec e <> _ = ErrorSpec e	2✔
200	_ <> ErrorSpec e = ErrorSpec e	2✔
201	MemberSpec as <> MemberSpec as' =
202	addToErrorSpec	2✔
203	( NE.fromList	2✔
204	["Intersecting: ", " MemberSpec " ++ show (NE.toList as), " MemberSpec " ++ show (NE.toList as')]	2✔
205	)
206	( memberSpec	2✔
207	(nub $ intersect (NE.toList as) (NE.toList as'))	2✔
208	(pure "Empty intersection")	2✔
209	)
210	ms@(MemberSpec as) <> ts@TypeSpec {} =
211	memberSpec	2✔
212	(nub $ NE.filter (`conformsToSpec` ts) as)	2✔
213	( NE.fromList	×
214	[ "The two " ++ showType @a ++ " Specifications are inconsistent."	×
215	, " " ++ show ms	×
216	, " " ++ show ts	×
217	]
218	)
219	TypeSpec s cant <> MemberSpec as = MemberSpec as <> TypeSpec s cant	2✔
220	SuspendedSpec v p <> SuspendedSpec v' p' = SuspendedSpec v (p <> rename v' v p')	2✔
221	SuspendedSpec v ps <> s = SuspendedSpec v (ps <> satisfies (V v) s)	2✔
222	s <> SuspendedSpec v ps = SuspendedSpec v (ps <> satisfies (V v) s)	2✔
223	TypeSpec s cant <> TypeSpec s' cant' = case combineSpec s s' of	2✔
224	-- NOTE: This might look like an unnecessary case, but doing
225	-- it like this avoids looping.
226	TypeSpec s'' cant'' -> TypeSpec s'' (cant <> cant' <> cant'')	2✔
227	s'' -> s'' <> notMemberSpec (cant <> cant')	2✔
228
229	instance HasSpec a => Monoid (Specification a) where	2✔
230	mempty = TrueSpec	2✔
231
232	-- =========================================================================
233
234	-- \| Collect the 'monitor' calls from a specification instantiated to the given value. Typically,
235	--
236	-- > quickCheck $ forAll (genFromSpec spec) $ \ x -> monitorSpec spec x $ ...
237	monitorSpec :: Testable p => Specification a -> a -> p -> Property
238	monitorSpec (SuspendedSpec x p) a =	2✔
239	errorGE (monitorPred (Env.singleton x a) p) . property	2✔
240	monitorSpec _ _ = property	2✔
241
242	monitorPred ::
243	forall m. MonadGenError m => Env -> Pred -> m (Property -> Property)
244	monitorPred env = \case	2✔
245	ElemPred {} -> pure id -- Not sure about this, but ElemPred is a lot like Assert, so ...	×
246	Monitor m -> pure (m $ errorGE . explain "monitorPred: Monitor" . runTerm env)	2✔
247	Subst x t p -> monitorPred env $ substitutePred x t p	2✔
248	Assert {} -> pure id	2✔
249	GenHint {} -> pure id	2✔
250	Reifies {} -> pure id	2✔
251	ForAll t (x :-> p) -> do	2✔
252	set <- runTerm env t	2✔
253	foldr (.) id	2✔
254	<$> sequence	2✔
255	[ monitorPred env' p	2✔
256	\| v <- forAllToList set	2✔
257	, let env' = Env.extend x v env	2✔
258	]
259	Case t bs -> do	2✔
260	v <- runTerm env t	2✔
261	runCaseOn v (mapList thing bs) (\x val ps -> monitorPred (Env.extend x val env) ps)	2✔
262	When b p -> do	2✔
263	v <- runTerm env b	2✔
264	if v then monitorPred env p else pure id	1✔
265	TruePred -> pure id	2✔
266	FalsePred {} -> pure id	×
267	DependsOn {} -> pure id	2✔
268	And ps -> foldr (.) id <$> mapM (monitorPred env) ps	2✔
269	Let t (x :-> p) -> do	2✔
270	val <- runTerm env t	2✔
271	monitorPred (Env.extend x val env) p	2✔
272	Exists k (x :-> p) -> do	2✔
273	case k (errorGE . explain "monitorPred: Exists" . runTerm env) of	2✔
274	Result a -> monitorPred (Env.extend x a env) p	2✔
275	_ -> pure id	2✔
276	Explain es p -> explainNE es $ monitorPred env p	1✔

input-output-hk / constrained-generators / 371

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous