input-output-hk / constrained-generators / 407

Committed 20 Nov 2025 12:46PM UTC coverage: 76.922% (-0.4%) from 77.308%

Build # 407

Build Type

push

github

Committed by

web-flow

Commit Message

initial stab at speeding up maps with more optimistic first assumption (#58)

Run Details

12 of 13 new or added lines in 3 files covered. (92.31%)

45 existing lines in 5 files now uncovered.

3923 of 5100 relevant lines covered (76.92%)

1.45 hits per line

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

58.49

/src/Constrained/AbstractSyntax.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | This module contains the abstract syntax of terms, predicates, and specifications
module Constrained.AbstractSyntax (
  TermD (..),
  runTermE,
  runTerm,
  fastInequality,
  PredD (..),
  SpecificationD (..),
  BinderD (..),
  Weighted (..),
  mapWeighted,
  traverseWeighted,
  AppRequiresD,
  Syntax (..),
) where

import Constrained.Core
import Constrained.DependencyInjection
import Constrained.Env (Env)
import Constrained.Env qualified as Env
import Constrained.FunctionSymbol
import Constrained.GenT
import Constrained.Generic
import Constrained.List
import Constrained.PrettyUtils
import Control.Monad.Identity
import Data.Kind
import Data.List.NonEmpty qualified as NE
import Data.String
import Data.Typeable
import Prettyprinter hiding (cat)
import Test.QuickCheck

------------------------------------------------------------------------
-- The first-order term language
------------------------------------------------------------------------

-- $depsExplanation
-- See `Constrained.DependencyInjection` to better understand @deps@ - it's a
-- pointer to postpone having to define `Constrained.Base.HasSpec` and friends here.

-- | First-order terms, application, literals, variables. $depsExplanation
data TermD deps a where
  App ::
    AppRequiresD deps t dom rng =>
    t dom rng ->
    List (TermD deps) dom ->
    TermD deps rng
  Lit :: (Typeable a, Eq a, Show a) => a -> TermD deps a
  V :: (HasSpecD deps a, Typeable a) => Var a -> TermD deps a

-- | Everything required to deal with applications of a function to arguments
-- of type @dom@
type AppRequiresD deps (t :: [Type] -> Type -> Type) dom rng =
  ( LogicD deps t
  , Syntax t
  , Semantics t
  , TypeList dom
  , Eq (t dom rng)
  , Show (t dom rng)
  , Typeable t
  , All Typeable dom
  , Typeable dom
  , Typeable rng
  , All (HasSpecD deps) dom
  , All Show dom
  , HasSpecD deps rng
  , Show rng
  )

instance Eq (TermD deps a) where
  V x == V x' = x == x'
  Lit a == Lit b = a == b
  App (w1 :: x1) (ts :: List (TermD deps) dom1) == App (w2 :: x2) (ts' :: List (TermD deps) dom2) =
    case (eqT @dom1 @dom2, eqT @x1 @x2) of
      (Just Refl, Just Refl) ->
        w1 == w2
          && ts == ts'
      _ -> False
  _ == _ = False

-- Semantics --------------------------------------------------------------

-- | Run a term in an environment, with an error if it fails
runTermE :: forall a deps. Env -> TermD deps a -> Either (NE.NonEmpty String) a
runTermE env = \case
  Lit a -> Right a
  V v -> case Env.lookup env v of
    Just a -> Right a
    Nothing -> Left (pure ("Couldn't find " ++ show v ++ " in " ++ show env))
  -- The first two cases here are an optimization to avoid dispatching to `mapMList` (which does all sorts of
  -- unpacking and packing and doesn't fuse nicely with `uncurryList_`)
  App f (ta :> Nil) -> semantics f <$> runTermE env ta
  App f (ta :> tb :> Nil) -> semantics f <$> runTermE env ta <*> runTermE env tb
  App f ts -> do
    vs <- mapMList (fmap Identity . runTermE env) ts
    pure $ uncurryList_ runIdentity (semantics f) vs

-- | Generalized `runTermE` to `MonadGenError`
runTerm :: MonadGenError m => Env -> TermD deps a -> m a
runTerm env x = case runTermE env x of
  Left msgs -> fatalErrorNE msgs
  Right val -> pure val

-- Utilities --------------------------------------------------------------

-- | Sound but not complete inequality on terms
fastInequality :: TermD deps a -> TermD deps b -> Bool
fastInequality (V (Var i _)) (V (Var j _)) = i /= j
fastInequality Lit {} Lit {} = False
fastInequality (App _ as) (App _ bs) = go as bs
  where
    go :: List (TermD deps) as -> List (TermD deps) bs -> Bool
    go Nil Nil = False
    go (a :> as') (b :> bs') = fastInequality a b || go as' bs'
    go _ _ = True
fastInequality _ _ = True

-- Pretty-printing --------------------------------------------------------

-- | Syntactic operations are ones that have to do with the structure and appearence of the type. $depsExplanation
class Syntax (t :: [Type] -> Type -> Type) where
  isInfix :: t dom rng -> Bool
  isInfix _ = False

  prettySymbol ::
    forall deps dom rng ann.
    t dom rng ->
    List (TermD deps) dom ->
    Int ->
    Maybe (Doc ann)
  prettySymbol _ _ _ = Nothing

instance Show a => Pretty (WithPrec (TermD deps a)) where
  pretty (WithPrec p t) = case t of
    Lit n -> fromString $ showsPrec p n ""
    V x -> viaShow x
    App x Nil -> viaShow x
    App f as
      | Just doc <- prettySymbol f as p -> doc -- Use Function Symbol specific pretty printers
    App f as
      | isInfix f
      , a :> b :> Nil <- as ->
          parensIf (p > 9) $ prettyPrec 10 a <+> viaShow f <+> prettyPrec 10 b
      | otherwise -> parensIf (p > 10) $ viaShow f <+> align (fillSep (ppListC @Show (prettyPrec 11) as))

instance Show a => Pretty (TermD deps a) where
  pretty = prettyPrec 0

instance Show a => Show (TermD deps a) where
  showsPrec p t = shows $ pretty (WithPrec p t)

------------------------------------------------------------------------
-- The language for predicates
------------------------------------------------------------------------

-- | This is _essentially_ a first-order logic with some extra spicyness thrown
-- in to handle things like sum types and the specific problems you get into
-- when generating from constraints (mostly to do with choosing the order in
-- which to generate things). $depsExplanation
data PredD deps where
  ElemPred ::
    (HasSpecD deps a, Show a) =>
    Bool ->
    TermD deps a ->
    NonEmpty a ->
    PredD deps
  Monitor :: ((forall a. TermD deps a -> a) -> Property -> Property) -> PredD deps
  And :: [PredD deps] -> PredD deps
  Exists ::
    -- | Constructive recovery function for checking
    -- existential quantification
    ((forall b. TermD deps b -> b) -> GE a) ->
    BinderD deps a ->
    PredD deps
  -- This is here because we sometimes need to delay substitution until we're done building
  -- terms and predicates. This is because our surface syntax relies on names being "a bit"
  -- lazily bound to avoid infinite loops when trying to create new names.
  Subst ::
    ( HasSpecD deps a
    , Show a
    ) =>
    Var a ->
    TermD deps a ->
    PredD deps ->
    PredD deps
  Let ::
    TermD deps a ->
    BinderD deps a ->
    PredD deps
  Assert :: TermD deps Bool -> PredD deps
  Reifies ::
    ( HasSpecD deps a
    , HasSpecD deps b
    , Show a
    , Show b
    ) =>
    -- | This depends on the @a@ term
    TermD deps b ->
    TermD deps a ->
    -- | Recover a useable @b@ value from the @a@ term in normal Haskell land
    (a -> b) ->
    PredD deps
  DependsOn ::
    ( HasSpecD deps a
    , HasSpecD deps b
    , Show a
    , Show b
    ) =>
    TermD deps a ->
    TermD deps b ->
    PredD deps
  ForAll ::
    ( ForallableD deps t e
    , HasSpecD deps t
    , HasSpecD deps e
    , Show t
    , Show e
    ) =>
    TermD deps t ->
    BinderD deps e ->
    PredD deps
  Case ::
    ( HasSpecD deps (SumOver as)
    , Show (SumOver as)
    ) =>
    TermD deps (SumOver as) ->
    -- | Each branch of the type is bound with
    -- only one variable because `as` are types.
    -- Constructors with multiple arguments are
    -- encoded with `ProdOver` (c.f. `Constrained.Univ`).
    List (Weighted (BinderD deps)) as ->
    PredD deps
  -- monadic-style `when` - if the first argument is False the second
  -- doesn't apply.
  When ::
    TermD deps Bool ->
    PredD deps ->
    PredD deps
  GenHintD ::
    ( HasGenHintD deps a
    , Show a
    , Show (HintD deps a)
    ) =>
    HintD deps a ->
    TermD deps a ->
    PredD deps
  TruePred :: PredD deps
  FalsePred :: NE.NonEmpty String -> PredD deps
  Explain :: NE.NonEmpty String -> PredD deps -> PredD deps

-- | Binders, a t`Var` is bound in a `PredD`, never anywhere else
data BinderD deps a where
  (:->) ::
    (HasSpecD deps a, Show a) =>
    Var a ->
    PredD deps ->
    BinderD deps a

deriving instance Show (BinderD deps a)

-- | A thing, wrapped in a functor, with a weight
data Weighted f a = Weighted {weight :: Maybe Int, thing :: f a}
  deriving (Functor, Traversable, Foldable)

-- | Apply a natural transformation to the weighted value
mapWeighted :: (f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted f (Weighted w t) = Weighted w (f t)

-- | Like `mapWeighted` but `Applicative`
traverseWeighted :: Applicative m => (f a -> m (g a)) -> Weighted f a -> m (Weighted g a)
traverseWeighted f (Weighted w t) = Weighted w <$> f t

instance Semigroup (PredD deps) where
  FalsePred xs <> FalsePred ys = FalsePred (xs <> ys)
  FalsePred es <> _ = FalsePred es
  _ <> FalsePred es = FalsePred es
  TruePred <> p = p
  p <> TruePred = p
  p <> p' = And (unpackPred p ++ unpackPred p')
    where
      unpackPred (And ps) = ps
      unpackPred x = [x]

instance Monoid (PredD deps) where
  mempty = TruePred

-- Pretty-printing --------------------------------------------------------

instance Pretty (PredD deps) where
  pretty = \case
    ElemPred True term vs ->
      align $
        sep
          [ "memberPred"
          , pretty term
          , prettyShowList (NE.toList vs)
          ]
    ElemPred False term vs -> align $ sep ["notMemberPred", pretty term, prettyShowList (NE.toList vs)]
    Exists _ (x :-> p) -> align $ sep ["exists" <+> viaShow x <+> "in", pretty p]
    Let t (x :-> p) -> align $ sep ["let" <+> viaShow x <+> "=" /> pretty t <+> "in", pretty p]
    And ps -> braces $ vsep' $ map pretty ps
    Assert t -> "assert $" <+> pretty t
    Reifies t' t _ -> "reifies" <+> pretty (WithPrec 11 t') <+> pretty (WithPrec 11 t)
    DependsOn a b -> pretty a <+> "<-" /> pretty b
    ForAll t (x :-> p) -> "forall" <+> viaShow x <+> "in" <+> pretty t <+> "$" /> pretty p
    Case t bs -> "case" <+> pretty t <+> "of" /> vsep' (ppList pretty bs)
    When b p -> "whenTrue" <+> pretty (WithPrec 11 b) <+> "$" /> pretty p
    Subst x t p -> "[" <> pretty t <> "/" <> viaShow x <> "]" <> pretty p
    GenHintD h t -> "genHint" <+> fromString (showsPrec 11 h "") <+> "$" <+> pretty t
    TruePred -> "True"
    FalsePred {} -> "False"
    Monitor {} -> "monitor"
    Explain es p -> "Explain" <+> viaShow (NE.toList es) <+> "$" /> pretty p

instance Show (PredD deps) where
  show = show . pretty

instance Pretty (f a) => Pretty (Weighted f a) where
  pretty (Weighted Nothing t) = pretty t
  pretty (Weighted (Just w) t) = viaShow w <> "~" <> pretty t

instance Pretty (BinderD deps a) where
  pretty (x :-> p) = viaShow x <+> "->" <+> pretty p

------------------------------------------------------------------------
-- The language of specifications
------------------------------------------------------------------------

-- | A @`SpecificationD` deps a@ denotes a set of @a@s. $depsExplanation
data SpecificationD deps a where
  -- | Explain a Specification
  ExplainSpec :: [String] -> SpecificationD deps a -> SpecificationD deps a
  -- | Elements of a known set
  MemberSpec ::
    -- | It must be an element of this list. Try hard not to put duplicates in the List.
    NE.NonEmpty a ->
    SpecificationD deps a
  -- | The empty set
  ErrorSpec ::
    NE.NonEmpty String ->
    SpecificationD deps a
  -- | The set described by some predicates
  -- over the bound variable.
  SuspendedSpec ::
    HasSpecD deps a =>
    -- | This variable ranges over values denoted by
    -- the spec
    Var a ->
    -- | And the variable is subject to these constraints
    PredD deps ->
    SpecificationD deps a
  -- | A type-specific spec
  TypeSpecD ::
    HasSpecD deps a =>
    TypeSpecD deps a ->
    -- | It can't be any of the elements of this set
    [a] ->
    SpecificationD deps a
  -- | Anything
  TrueSpec :: SpecificationD deps a

instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Pretty (WithPrec (SpecificationD deps a)) where
  pretty (WithPrec d s) = case s of
    ExplainSpec es z -> "ExplainSpec" <+> viaShow es <+> "$" /> pretty z
    ErrorSpec es -> "ErrorSpec" /> vsep' (map fromString (NE.toList es))
    TrueSpec -> fromString $ "TrueSpec @(" ++ showType @a ++ ")"
    MemberSpec xs -> "MemberSpec" <+> prettyShowList (NE.toList xs)
    SuspendedSpec x p -> parensIf (d > 10) $ "constrained $ \\" <+> viaShow x <+> "->" /> pretty p
    -- TODO: require pretty for `TypeSpec` to make this much nicer
    TypeSpecD ts cant ->
      parensIf (d > 10) $
        "TypeSpec"
          /> vsep
            [ fromString (showsPrec 11 ts "")
            , prettyShowList cant
            ]

instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Pretty (SpecificationD deps a) where
  pretty = pretty . WithPrec 0

instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Show (SpecificationD deps a) where
  showsPrec d = shows . pretty . WithPrec d

1	{-# LANGUAGE ConstraintKinds #-}
2	{-# LANGUAGE DataKinds #-}
3	{-# LANGUAGE DeriveTraversable #-}
4	{-# LANGUAGE FlexibleContexts #-}
5	{-# LANGUAGE FlexibleInstances #-}
6	{-# LANGUAGE GADTs #-}
7	{-# LANGUAGE ImportQualifiedPost #-}
8	{-# LANGUAGE LambdaCase #-}
9	{-# LANGUAGE OverloadedStrings #-}
10	{-# LANGUAGE RankNTypes #-}
11	{-# LANGUAGE ScopedTypeVariables #-}
12	{-# LANGUAGE StandaloneDeriving #-}
13	{-# LANGUAGE TypeApplications #-}
14	{-# LANGUAGE TypeFamilies #-}
15	{-# LANGUAGE UndecidableInstances #-}
16
17	-- \| This module contains the abstract syntax of terms, predicates, and specifications
18	module Constrained.AbstractSyntax (
19	TermD (..),
20	runTermE,
21	runTerm,
22	fastInequality,
23	PredD (..),
24	SpecificationD (..),
25	BinderD (..),
26	Weighted (..),
27	mapWeighted,
28	traverseWeighted,
29	AppRequiresD,
30	Syntax (..),
31	) where
32
33	import Constrained.Core
34	import Constrained.DependencyInjection
35	import Constrained.Env (Env)
36	import Constrained.Env qualified as Env
37	import Constrained.FunctionSymbol
38	import Constrained.GenT
39	import Constrained.Generic
40	import Constrained.List
41	import Constrained.PrettyUtils
42	import Control.Monad.Identity
43	import Data.Kind
44	import Data.List.NonEmpty qualified as NE
45	import Data.String
46	import Data.Typeable
47	import Prettyprinter hiding (cat)
48	import Test.QuickCheck
49
50	------------------------------------------------------------------------
51	-- The first-order term language
52	------------------------------------------------------------------------
53
54	-- $depsExplanation
55	-- See `Constrained.DependencyInjection` to better understand @deps@ - it's a
56	-- pointer to postpone having to define `Constrained.Base.HasSpec` and friends here.
57
58	-- \| First-order terms, application, literals, variables. $depsExplanation
59	data TermD deps a where
60	App ::
61	AppRequiresD deps t dom rng =>
62	t dom rng ->
63	List (TermD deps) dom ->
64	TermD deps rng
65	Lit :: (Typeable a, Eq a, Show a) => a -> TermD deps a
66	V :: (HasSpecD deps a, Typeable a) => Var a -> TermD deps a
67
68	-- \| Everything required to deal with applications of a function to arguments
69	-- of type @dom@
70	type AppRequiresD deps (t :: [Type] -> Type -> Type) dom rng =
71	( LogicD deps t
72	, Syntax t
73	, Semantics t
74	, TypeList dom
75	, Eq (t dom rng)
76	, Show (t dom rng)
77	, Typeable t
78	, All Typeable dom
79	, Typeable dom
80	, Typeable rng
81	, All (HasSpecD deps) dom
82	, All Show dom
83	, HasSpecD deps rng
84	, Show rng
85	)
86
87	instance Eq (TermD deps a) where	×
88	V x == V x' = x == x'	2✔
89	Lit a == Lit b = a == b	2✔
90	App (w1 :: x1) (ts :: List (TermD deps) dom1) == App (w2 :: x2) (ts' :: List (TermD deps) dom2) =
91	case (eqT @dom1 @dom2, eqT @x1 @x2) of	2✔
92	(Just Refl, Just Refl) ->
93	w1 == w2	2✔
94	&& ts == ts'	2✔
95	_ -> False	2✔
96	_ == _ = False	2✔
97
98	-- Semantics --------------------------------------------------------------
99
100	-- \| Run a term in an environment, with an error if it fails
101	runTermE :: forall a deps. Env -> TermD deps a -> Either (NE.NonEmpty String) a
102	runTermE env = \case	2✔
103	Lit a -> Right a	2✔
104	V v -> case Env.lookup env v of	2✔
105	Just a -> Right a	2✔
106	Nothing -> Left (pure ("Couldn't find " ++ show v ++ " in " ++ show env))	×
107	-- The first two cases here are an optimization to avoid dispatching to `mapMList` (which does all sorts of
108	-- unpacking and packing and doesn't fuse nicely with `uncurryList_`)
109	App f (ta :> Nil) -> semantics f <$> runTermE env ta	2✔
110	App f (ta :> tb :> Nil) -> semantics f <$> runTermE env ta <*> runTermE env tb	2✔
UNCOV 111	App f ts -> do	×
UNCOV 112	vs <- mapMList (fmap Identity . runTermE env) ts	×
UNCOV 113	pure $ uncurryList_ runIdentity (semantics f) vs	×
114
115	-- \| Generalized `runTermE` to `MonadGenError`
116	runTerm :: MonadGenError m => Env -> TermD deps a -> m a
117	runTerm env x = case runTermE env x of	2✔
UNCOV 118	Left msgs -> fatalErrorNE msgs	×
119	Right val -> pure val	2✔
120
121	-- Utilities --------------------------------------------------------------
122
123	-- \| Sound but not complete inequality on terms
124	fastInequality :: TermD deps a -> TermD deps b -> Bool
125	fastInequality (V (Var i _)) (V (Var j _)) = i /= j	2✔
UNCOV 126	fastInequality Lit {} Lit {} = False	×
127	fastInequality (App _ as) (App _ bs) = go as bs	2✔
128	where
129	go :: List (TermD deps) as -> List (TermD deps) bs -> Bool
130	go Nil Nil = False	2✔
131	go (a :> as') (b :> bs') = fastInequality a b \|\| go as' bs'	2✔
UNCOV 132	go _ _ = True	×
133	fastInequality _ _ = True	2✔
134
135	-- Pretty-printing --------------------------------------------------------
136
137	-- \| Syntactic operations are ones that have to do with the structure and appearence of the type. $depsExplanation
138	class Syntax (t :: [Type] -> Type -> Type) where
139	isInfix :: t dom rng -> Bool
UNCOV 140	isInfix _ = False	×
141
142	prettySymbol ::
143	forall deps dom rng ann.
144	t dom rng ->
145	List (TermD deps) dom ->
146	Int ->
147	Maybe (Doc ann)
148	prettySymbol _ _ _ = Nothing	2✔
149
150	instance Show a => Pretty (WithPrec (TermD deps a)) where	×
151	pretty (WithPrec p t) = case t of	2✔
152	Lit n -> fromString $ showsPrec p n ""	2✔
153	V x -> viaShow x	2✔
UNCOV 154	App x Nil -> viaShow x	×
155	App f as
156	\| Just doc <- prettySymbol f as p -> doc -- Use Function Symbol specific pretty printers	2✔
157	App f as
158	\| isInfix f	1✔
159	, a :> b :> Nil <- as ->	2✔
160	parensIf (p > 9) $ prettyPrec 10 a <+> viaShow f <+> prettyPrec 10 b	2✔
UNCOV 161	\| otherwise -> parensIf (p > 10) $ viaShow f <+> align (fillSep (ppListC @Show (prettyPrec 11) as))	×
162
UNCOV 163	instance Show a => Pretty (TermD deps a) where	×
164	pretty = prettyPrec 0	2✔
165
UNCOV 166	instance Show a => Show (TermD deps a) where	×
167	showsPrec p t = shows $ pretty (WithPrec p t)	1✔
168
169	------------------------------------------------------------------------
170	-- The language for predicates
171	------------------------------------------------------------------------
172
173	-- \| This is _essentially_ a first-order logic with some extra spicyness thrown
174	-- in to handle things like sum types and the specific problems you get into
175	-- when generating from constraints (mostly to do with choosing the order in
176	-- which to generate things). $depsExplanation
177	data PredD deps where
178	ElemPred ::
179	(HasSpecD deps a, Show a) =>
180	Bool ->
181	TermD deps a ->
182	NonEmpty a ->
183	PredD deps
184	Monitor :: ((forall a. TermD deps a -> a) -> Property -> Property) -> PredD deps
185	And :: [PredD deps] -> PredD deps
186	Exists ::
187	-- \| Constructive recovery function for checking
188	-- existential quantification
189	((forall b. TermD deps b -> b) -> GE a) ->
190	BinderD deps a ->
191	PredD deps
192	-- This is here because we sometimes need to delay substitution until we're done building
193	-- terms and predicates. This is because our surface syntax relies on names being "a bit"
194	-- lazily bound to avoid infinite loops when trying to create new names.
195	Subst ::
196	( HasSpecD deps a
197	, Show a
198	) =>
199	Var a ->
200	TermD deps a ->
201	PredD deps ->
202	PredD deps
203	Let ::
204	TermD deps a ->
205	BinderD deps a ->
206	PredD deps
207	Assert :: TermD deps Bool -> PredD deps
208	Reifies ::
209	( HasSpecD deps a
210	, HasSpecD deps b
211	, Show a
212	, Show b
213	) =>
214	-- \| This depends on the @a@ term
215	TermD deps b ->
216	TermD deps a ->
217	-- \| Recover a useable @b@ value from the @a@ term in normal Haskell land
218	(a -> b) ->
219	PredD deps
220	DependsOn ::
221	( HasSpecD deps a
222	, HasSpecD deps b
223	, Show a
224	, Show b
225	) =>
226	TermD deps a ->
227	TermD deps b ->
228	PredD deps
229	ForAll ::
230	( ForallableD deps t e
231	, HasSpecD deps t
232	, HasSpecD deps e
233	, Show t
234	, Show e
235	) =>
236	TermD deps t ->
237	BinderD deps e ->
238	PredD deps
239	Case ::
240	( HasSpecD deps (SumOver as)
241	, Show (SumOver as)
242	) =>
243	TermD deps (SumOver as) ->
244	-- \| Each branch of the type is bound with
245	-- only one variable because `as` are types.
246	-- Constructors with multiple arguments are
247	-- encoded with `ProdOver` (c.f. `Constrained.Univ`).
248	List (Weighted (BinderD deps)) as ->
249	PredD deps
250	-- monadic-style `when` - if the first argument is False the second
251	-- doesn't apply.
252	When ::
253	TermD deps Bool ->
254	PredD deps ->
255	PredD deps
256	GenHintD ::
257	( HasGenHintD deps a
258	, Show a
259	, Show (HintD deps a)
260	) =>
261	HintD deps a ->
262	TermD deps a ->
263	PredD deps
264	TruePred :: PredD deps
265	FalsePred :: NE.NonEmpty String -> PredD deps
266	Explain :: NE.NonEmpty String -> PredD deps -> PredD deps
267
268	-- \| Binders, a t`Var` is bound in a `PredD`, never anywhere else
269	data BinderD deps a where
270	(:->) ::
271	(HasSpecD deps a, Show a) =>
272	Var a ->
273	PredD deps ->
274	BinderD deps a
275
276	deriving instance Show (BinderD deps a)	×
277
278	-- \| A thing, wrapped in a functor, with a weight
279	data Weighted f a = Weighted {weight :: Maybe Int, thing :: f a}	2✔
UNCOV 280	deriving (Functor, Traversable, Foldable)	×
281
282	-- \| Apply a natural transformation to the weighted value
283	mapWeighted :: (f a -> g b) -> Weighted f a -> Weighted g b
284	mapWeighted f (Weighted w t) = Weighted w (f t)	2✔
285
286	-- \| Like `mapWeighted` but `Applicative`
287	traverseWeighted :: Applicative m => (f a -> m (g a)) -> Weighted f a -> m (Weighted g a)
288	traverseWeighted f (Weighted w t) = Weighted w <$> f t	2✔
289
UNCOV 290	instance Semigroup (PredD deps) where	×
291	FalsePred xs <> FalsePred ys = FalsePred (xs <> ys)	1✔
292	FalsePred es <> _ = FalsePred es	1✔
293	_ <> FalsePred es = FalsePred es	1✔
294	TruePred <> p = p	2✔
295	p <> TruePred = p	2✔
296	p <> p' = And (unpackPred p ++ unpackPred p')	2✔
297	where
298	unpackPred (And ps) = ps	2✔
299	unpackPred x = [x]	2✔
300
301	instance Monoid (PredD deps) where	2✔
302	mempty = TruePred	2✔
303
304	-- Pretty-printing --------------------------------------------------------
305
306	instance Pretty (PredD deps) where	×
307	pretty = \case	2✔
308	ElemPred True term vs ->
309	align $	×
UNCOV 310	sep	×
311	[ "memberPred"	×
312	, pretty term	×
313	, prettyShowList (NE.toList vs)	×
314	]
UNCOV 315	ElemPred False term vs -> align $ sep ["notMemberPred", pretty term, prettyShowList (NE.toList vs)]	×
UNCOV 316	Exists _ (x :-> p) -> align $ sep ["exists" <+> viaShow x <+> "in", pretty p]	×
317	Let t (x :-> p) -> align $ sep ["let" <+> viaShow x <+> "=" /> pretty t <+> "in", pretty p]	×
318	And ps -> braces $ vsep' $ map pretty ps	2✔
319	Assert t -> "assert $" <+> pretty t	2✔
320	Reifies t' t _ -> "reifies" <+> pretty (WithPrec 11 t') <+> pretty (WithPrec 11 t)	1✔
321	DependsOn a b -> pretty a <+> "<-" /> pretty b	×
322	ForAll t (x :-> p) -> "forall" <+> viaShow x <+> "in" <+> pretty t <+> "$" /> pretty p	×
UNCOV 323	Case t bs -> "case" <+> pretty t <+> "of" /> vsep' (ppList pretty bs)	×
324	When b p -> "whenTrue" <+> pretty (WithPrec 11 b) <+> "$" /> pretty p	×
325	Subst x t p -> "[" <> pretty t <> "/" <> viaShow x <> "]" <> pretty p	×
UNCOV 326	GenHintD h t -> "genHint" <+> fromString (showsPrec 11 h "") <+> "$" <+> pretty t	×
327	TruePred -> "True"	2✔
328	FalsePred {} -> "False"	×
UNCOV 329	Monitor {} -> "monitor"	×
330	Explain es p -> "Explain" <+> viaShow (NE.toList es) <+> "$" /> pretty p	2✔
331
332	instance Show (PredD deps) where	×
333	show = show . pretty	2✔
334
335	instance Pretty (f a) => Pretty (Weighted f a) where	×
336	pretty (Weighted Nothing t) = pretty t	×
UNCOV 337	pretty (Weighted (Just w) t) = viaShow w <> "~" <> pretty t	×
338
UNCOV 339	instance Pretty (BinderD deps a) where	×
UNCOV 340	pretty (x :-> p) = viaShow x <+> "->" <+> pretty p	×
341
342	------------------------------------------------------------------------
343	-- The language of specifications
344	------------------------------------------------------------------------
345
346	-- \| A @`SpecificationD` deps a@ denotes a set of @a@s. $depsExplanation
347	data SpecificationD deps a where
348	-- \| Explain a Specification
349	ExplainSpec :: [String] -> SpecificationD deps a -> SpecificationD deps a
350	-- \| Elements of a known set
351	MemberSpec ::
352	-- \| It must be an element of this list. Try hard not to put duplicates in the List.
353	NE.NonEmpty a ->
354	SpecificationD deps a
355	-- \| The empty set
356	ErrorSpec ::
357	NE.NonEmpty String ->
358	SpecificationD deps a
359	-- \| The set described by some predicates
360	-- over the bound variable.
361	SuspendedSpec ::
362	HasSpecD deps a =>
363	-- \| This variable ranges over values denoted by
364	-- the spec
365	Var a ->
366	-- \| And the variable is subject to these constraints
367	PredD deps ->
368	SpecificationD deps a
369	-- \| A type-specific spec
370	TypeSpecD ::
371	HasSpecD deps a =>
372	TypeSpecD deps a ->
373	-- \| It can't be any of the elements of this set
374	[a] ->
375	SpecificationD deps a
376	-- \| Anything
377	TrueSpec :: SpecificationD deps a
378
UNCOV 379	instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Pretty (WithPrec (SpecificationD deps a)) where	×
380	pretty (WithPrec d s) = case s of	2✔
UNCOV 381	ExplainSpec es z -> "ExplainSpec" <+> viaShow es <+> "$" /> pretty z	×
382	ErrorSpec es -> "ErrorSpec" /> vsep' (map fromString (NE.toList es))	2✔
383	TrueSpec -> fromString $ "TrueSpec @(" ++ showType @a ++ ")"	2✔
384	MemberSpec xs -> "MemberSpec" <+> prettyShowList (NE.toList xs)	2✔
385	SuspendedSpec x p -> parensIf (d > 10) $ "constrained $ \\" <+> viaShow x <+> "->" /> pretty p	2✔
386	-- TODO: require pretty for `TypeSpec` to make this much nicer
387	TypeSpecD ts cant ->
388	parensIf (d > 10) $	2✔
389	"TypeSpec"	2✔
390	/> vsep	2✔
391	[ fromString (showsPrec 11 ts "")	1✔
392	, prettyShowList cant	2✔
393	]
394
UNCOV 395	instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Pretty (SpecificationD deps a) where	×
396	pretty = pretty . WithPrec 0	2✔
397
UNCOV 398	instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Show (SpecificationD deps a) where	×
399	showsPrec d = shows . pretty . WithPrec d	2✔

input-output-hk / constrained-generators / 407

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