input-output-hk / constrained-generators / 416

{-# LANGUAGE AllowAmbiguousTypes #-}

{-# LANGUAGE ConstraintKinds #-}

{-# LANGUAGE DataKinds #-}

{-# LANGUAGE DefaultSignatures #-}

{-# LANGUAGE FlexibleContexts #-}

{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE FunctionalDependencies #-}

{-# LANGUAGE GADTs #-}

{-# LANGUAGE LambdaCase #-}

{-# LANGUAGE OverloadedStrings #-}

{-# LANGUAGE PatternSynonyms #-}

{-# LANGUAGE ScopedTypeVariables #-}

{-# LANGUAGE StandaloneDeriving #-}

{-# LANGUAGE TypeApplications #-}

{-# LANGUAGE TypeFamilies #-}

{-# LANGUAGE TypeOperators #-}

{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE UndecidableSuperClasses #-}

{-# LANGUAGE ViewPatterns #-}

-- | This module contains the most basic parts the implementation. Essentially

--   everything to define Specification, HasSpec, HasSimpleRep, Term, Pred, and the Syntax,

--   Semantics, and Logic class. It also has a few HasSpec, HasSimpleRep, and Logic

--   instances for basic types needed to define the default types and methods of HasSpec.

--   It also supplies Eq, Pretty, and Show instances on the syntax (Term, Pred, Binder etc.)

--   because many functions require these instances. It exports functions that define the

--   user interface to the domain embedded language (constrained, forall, exists etc.).

--   And, by design, nothing more.

module Constrained.Base (

  -- * Implementing logic propagation

  Logic (..),

  pattern (:<:),

  pattern (:>:),

  pattern Unary,

  Ctx (..),

  toCtx,

  flipCtx,

  fromListCtx,

  ctxHasSpec,

  -- * Useful function symbols and patterns for building custom rewrite rules

  fromGeneric_,

  toGeneric_,

  pattern ToGeneric,

  pattern FromGeneric,

  -- * Syntax for building specifications

  constrained,

  notMemberSpec,

  notEqualSpec,

  typeSpec,

  addToErrorSpec,

  memberSpec,

  fromSimpleRepSpec,

  toSimpleRepSpec,

  explainSpec,

  -- * Instantiated types and helper patterns

  Term,

  Specification,

  Pred,

  Binder,

  pattern TypeSpec,

  pattern GenHint,

  -- * Constraints and classes

  HasSpec (..),

  HasGenHint (..),

  Forallable,

  AppRequires,

  GenericallyInstantiated,

  GenericRequires,

  -- * Building `Pred`, `Specification`, `Term` etc.

  bind,

  name,

  -- * TODO: documentme

  propagateSpec,

  appFun,

  errorLikeMessage,

  isErrorLike,

  BinaryShow (..),

  toPred,

  forAllToList,

  IsPred,

  equalSpec,

  appTerm,

  HOLE (..),

  fromForAllSpec,

  Fun (..),

  BaseW (..),

  Deps,

) where

import Constrained.AbstractSyntax

import Constrained.Core

import Constrained.DependencyInjection

import Constrained.FunctionSymbol

import Constrained.GenT

import Constrained.Generic

import Constrained.List hiding (toList)

import Constrained.TypeErrors

import Data.Foldable (

  toList,

 )

import Data.Kind (Constraint, Type)

import qualified Data.List.NonEmpty as NE

import Data.Orphans ()

import Data.Semigroup (Max (..), getMax)

import Data.Typeable

import GHC.Stack

import Prettyprinter hiding (cat)

import Test.QuickCheck (arbitrary, shrink)

newtype TypeSpecF a = TypeSpecF (TypeSpec a)

newtype HintF a = HintF (Hint a)

data Deps

instance Dependencies Deps where

  type HasSpecD Deps = HasSpec

  type TypeSpecD Deps = TypeSpecF

  type LogicD Deps = Logic

  type ForallableD Deps = Forallable

  type HasGenHintD Deps = HasGenHint

  type HintD Deps = HintF

-- | Binders instantiated with the correct `HasSpec` etc. classes

type Binder = BinderD Deps

-- | All the constraints needed for application in the first order term languge

type AppRequires t as b = AppRequiresD Deps t as b

-- | Predicates over `Term`s

type Pred = PredD Deps

-- | First-order language of variables, literals, and application

type Term = TermD Deps

-- | Specifications for generators instantiated with the `HasSpec` et al actual

-- classes

type Specification = SpecificationD Deps

-- | Pattern match out a `TypeSpec` and the can't-"set" - avoids some tedious

-- pitfalls related to the `Deps` and `Dependencies` trick

pattern TypeSpec :: () => HasSpec a => TypeSpec a -> [a] -> Specification a

{-# COMPLETE ExplainSpec, MemberSpec, ErrorSpec, SuspendedSpec, TypeSpec, TrueSpec #-}

-- | Build a specifiation from just a `TypeSpec`, useful internal function when

-- writing `Logic` instances

typeSpec :: HasSpec a => TypeSpec a -> Specification a

-- | Pattern match out a `Hint` and the `Term` it applies to - avoids some

-- tedious pitfalls related to the `Deps` and `Dependencies` trick

pattern GenHint :: () => HasGenHint a => Hint a -> Term a -> Pred

{-# COMPLETE

  ElemPred

  , Monitor

  , And

  , Exists

  , Subst

  , Let

  , Assert

  , Reifies

  , DependsOn

  , ForAll

  , Case

  , When

  , GenHint

  , TruePred

  , FalsePred

  , Explain

  #-}

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

-- A First-order typed logic has 4 components

--     1. Terms        (Variables (x), Constants (5), and Applications (F x 5)

--        Applications, apply a function symbol to a list of arguments: (FunctionSymbol term1 .. termN)

--     2. Predicates   (Ordered, Odd, ...)

--     3. Connectives  (And, Or, Not, =>, ...)

--     4. Quantifiers  (Forall, Exists)

--

-- The Syntax, Semantics, and Logic classes implement new function symbols in

-- the first order logic. Note that a function symbol is first order

-- data, that uniquely identifies a higher order function. The three classes

-- supply varying levels of functionality, relating to the Syntax, Semantics, and

-- Logical operations of the function symbol.

-- | Logical operations are one that support reasoning about how a function symbol

--   relates to logical properties, that we call Specification's

class (Typeable t, Semantics t, Syntax t) => Logic t where

  {-# MINIMAL propagate | (propagateTypeSpec, propagateMemberSpec) #-}

  propagateTypeSpec ::

    (AppRequires t as b, HasSpec a) =>

    t as b ->

    ListCtx Value as (HOLE a) ->

    TypeSpec b ->

    [b] ->

    Specification a

  propagateMemberSpec ::

    (AppRequires t as b, HasSpec a) =>

    t as b ->

    ListCtx Value as (HOLE a) ->

    NonEmpty b ->

    Specification a

  propagate ::

    (AppRequires t as b, HasSpec a) =>

    t as b ->

    ListCtx Value as (HOLE a) ->

    Specification b ->

    Specification a

  rewriteRules ::

    (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) =>

    t dom rng ->

    List Term dom ->

    Evidence (AppRequires t dom rng) ->

    Maybe (Term rng)

  mapTypeSpec ::

    forall a b.

    (HasSpec a, HasSpec b) =>

    t '[a] b ->

    TypeSpec a ->

    Specification b

  saturate :: t dom Bool -> List Term dom -> [Pred]

-- | This is where the logical properties of a function symbol are applied to transform one spec into another

-- Note if there is a bunch of functions nested together, like (sizeOf_ (elems_ (snd_ x)))

-- we propagate each of those nested function symbols over the current spec, one at a time.

-- The result of this propagation is then made the current spec in the recusive calls to 'propagateSpec'

propagateSpec ::

  forall v a.

  HasSpec v =>

  Specification a ->

  Ctx v a ->

  Specification v

  CtxApp f (ListCtx pre c suf)

ctxHasSpec :: Ctx v a -> Evidence (HasSpec a)

-- | Contexts for Terms, basically a term with a _single_ HOLE

-- instead of a variable. This is used to traverse the defining

-- constraints for a variable and turn them into a spec. Each

-- subterm `f vs Ctx vs'` for lists of values `vs` and `vs'`

-- gets given to the `propagateSpecFun` for `f` as  `(f vs HOLE vs')`.

data Ctx v a where

  -- | A single hole of type `v`. Note ctxHOLE is a nullary constructor, where the `a` type index is the same as the `v` type index.

  CtxHOLE ::

    HasSpec v =>

    Ctx v v

  -- | The application `f vs Ctx vs'`

  CtxApp ::

    ( AppRequires fn as b

    , HasSpec b

    , TypeList as

    , Typeable as

    , All HasSpec as

    , Logic fn

    ) =>

    fn as b ->

    -- This is basically a `List` where

    -- everything is `Value` except for

    -- one entry which is `Ctx fn v`.

    ListCtx Value as (Ctx v) ->

    Ctx v b

-- | This is used together with `ListCtx` to form

-- just the arguments to `f vs Ctx vs'` - replacing

-- `Ctx` with `HOLE`, to get a `ListCtx Value as (HOLE a)` which then can be used as an input to `propagate`.

data HOLE a b where

  HOLE :: HOLE a a

-- | Try to convert a `Term` to a single-hole context - works only if the `Var`

-- is the _only_ variable in the term _and_ it appears only once in the `Term`.

toCtx ::

  forall m v a.

  ( Typeable v

  , Show v

  , MonadGenError m

  , HasCallStack

  ) =>

  Var v ->

  Term a ->

  m (Ctx v a)

  where

    go :: forall b. Term b -> m (Ctx v b)

          ]

    go (V v')

              ]

-- | `toCtx` lifted to a `List` of `Term`s

toCtxList ::

  forall m v as.

  (Show v, Typeable v, MonadGenError m, HasCallStack) =>

  Var v ->

  List Term as ->

  m (ListCtx Value as (Ctx v))

  where

    prefix :: forall as'. HasCallStack => List Term as' -> m (ListCtx Value as' (Ctx v))

    suffix :: forall as'. List Term as' -> m (List Value as')

-- | A Convenient pattern for singleton contexts

pattern Unary :: HOLE a' a -> ListCtx f '[a] (HOLE a')

{-# COMPLETE Unary #-}

-- | Convenient patterns for binary contexts (the arrow :<: points towards the hole)

pattern (:<:) :: (Typeable b, Show b) => HOLE c a -> b -> ListCtx Value '[a, b] (HOLE c)

-- | Convenient patterns for binary contexts (the arrow :>: points towards the hole)

pattern (:>:) :: (Typeable a, Show a) => a -> HOLE c b -> ListCtx Value '[a, b] (HOLE c)

{-# COMPLETE (:<:), (:>:) #-}

-- | Flip a binary context around

flipCtx ::

  (Typeable a, Show a, Typeable b, Show b) =>

  ListCtx Value '[a, b] (HOLE c) -> ListCtx Value '[b, a] (HOLE c)

-- | From a ListCtx, build a (List Term as), to which the function symbol can be applied.

fromListCtx :: All HasSpec as => ListCtx Value as (HOLE a) -> Term a -> List Term as

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

-- The class (HasSpec a) tells us what operations type 'a' must

-- support to add it to the constraint solver and generator

-- Writing HasSpec instances gives the system the power to grow

-- Don't be afraid of all the methods. Most have default implementations.

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

-- | A type where the `HasSpec` instance has been instantiated via the `SimpleRep` with

-- constraints that give good type errors

type GenericallyInstantiated a =

  ( AssertComputes

      (SimpleRep a)

      ( Text "Trying to use a generic instantiation of "

          :<>: ShowType a

          :<>: Text ", likely in a HasSpec instance."

          :$$: Text

                 "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."

      )

  , HasSimpleRep a

  , HasSpec (SimpleRep a)

  , TypeSpec a ~ TypeSpec (SimpleRep a)

  )

-- | `Eq` and `Show` for `TypeSpec` with additional constraints to ensure good type errors

type TypeSpecEqShow a =

  ( AssertComputes

      (TypeSpec a)

      ( Text "Can't compute "

          :<>: ShowType (TypeSpec a)

          :$$: Text "Either because of a missing definition of TypeSpec or a missing instance of HasSimpleRep."

      )

  , Show (TypeSpec a)

  , Typeable (TypeSpec a)

  )

{- NOTE: type errors in constrained-generators

    It's easy to make a mistake like this:

      data Bad = Bad | Worse deriving (Eq, Show)

      instance HasSpec Bad

    Missing that this requires an instance of HasSimpleRep for Bad to work.

    The two `AssertComputes` uses above are here to give you better error messages when you make this mistake,

    e.g. giving you something like this:

      src/Constrained/Examples/Basic.hs:327:10: error: [GHC-64725]

          • Can't compute TypeSpec (SimpleRep Bad)

            Either because of a missing definition of TypeSpec or a missing instance of HasSimpleRep.

          • In the instance declaration for ‘HasSpec Bad’

          |

      327 | instance HasSpec Bad

          |          ^^^^^^^^^^^

      src/Constrained/Examples/Basic.hs:327:10: error: [GHC-64725]

          • Trying to use a generic instantiation of Bad, likely in a HasSpec instance.

            However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep.

          • In the expression: Constrained.Base.$dmemptySpec @(Bad)

            In an equation for ‘emptySpec’:

                emptySpec = Constrained.Base.$dmemptySpec @(Bad)

            In the instance declaration for ‘HasSpec Bad’

          |

      327 | instance HasSpec Bad

          |          ^^^^^^^^^^^

-}

-- | Class for talking about types that we can write `Specification`s about

class

  ( Typeable a

  , Eq a

  , Show a

  , TypeSpecEqShow a

  ) =>

  HasSpec a

  where

  -- | The `TypeSpec a` is the type-specific `Specification a`.

  type TypeSpec a

  type TypeSpec a = TypeSpec (SimpleRep a)

  -- `TypeSpec` behaves sort-of like a monoid with a neutral

  -- element `emptySpec` and a `combineSpec` for combining

  -- two `TypeSpec a`. However, in order to provide flexibilty

  -- `combineSpec` takes two `TypeSpec` and constucts a `Specification`. This

  -- avoids e.g. having to have a separate implementation of `ErrorSpec`

  -- and `MemberSpec` in `TypeSpec`.

  -- | Trivial `TypeSpec` that admits anything

  emptySpec :: TypeSpec a

  -- | Conjunction of two `TypeSpec`s

  combineSpec :: TypeSpec a -> TypeSpec a -> Specification a

  -- | Generate a value that satisfies the `TypeSpec`.

  -- The key property for this generator is soundness:

  --  ∀ a ∈ genFromTypeSpec spec. a `conformsTo` spec

  genFromTypeSpec :: (HasCallStack, MonadGenError m) => TypeSpec a -> GenT m a

  -- | Check conformance to the spec.

  conformsTo :: HasCallStack => a -> TypeSpec a -> Bool

  -- | Shrink an `a` with the aide of a `TypeSpec`

  shrinkWithTypeSpec :: TypeSpec a -> a -> [a]

  -- | Try to make an `a` conform to `TypeSpec` with minimal changes. When

  -- `fixupWithSpec ts a` returns `Just a'`, it should be the case that

  -- `conformsTo a' ts`. There are no constraints in the `Nothing` case. A

  -- non-trivial implementation of this function is important for shrinking.

  fixupWithTypeSpec :: TypeSpec a -> a -> Maybe a

  -- | Convert a spec to predicates:

  -- The key property here is:

  --   ∀ a. a `conformsTo` spec == a `conformsTo` constrained (\t -> toPreds t spec)

  toPreds :: Term a -> TypeSpec a -> Pred

  -- | Compute an upper and lower bound on the number of solutions genFromTypeSpec might return

  cardinalTypeSpec :: TypeSpec a -> Specification Integer

  -- | A bound on the number of solutions `genFromTypeSpec TrueSpec` can produce.

  --   For a type with finite elements, we can get a much more accurate

  --   answer than TrueSpec

  cardinalTrueSpec :: Specification Integer

  -- Each instance can decide if a TypeSpec has an Error, and what String

  -- to pass to ErrorSpec to create an ErrorSpec value. Particulary

  -- useful for type Sum and Prod. The default instance uses guardTypeSpec,

  -- which also has a default value, and if that defualt value is used, typeSpecHasError will

  -- return Nothing. Both 'typeSpecHasError' and 'guardTypeSpec' can be set individually.

  -- If you're only writing one of these non default values, give it to 'guardTypeSpec'

  typeSpecHasError :: TypeSpec a -> Maybe (NE.NonEmpty String)

  -- Some binary TypeSpecs, which nest to the right

  -- e.g. something like this (X a (TypeSpec (X b (TypeSpec (X c w))))))

  -- An would look better in Vertical mode as (X [a,b,c] m).

  -- This lets each HasSpec instance decide. Particulary useful for type Sum and Prod

  alternateShow :: TypeSpec a -> BinaryShow

  -- | For some types (especially finite ones) there may be much better ways to construct

  --   a Specification than the default method of just adding a large 'bad' list to TypSpec. This

  --   function allows each HasSpec instance to decide.

  typeSpecOpt :: TypeSpec a -> [a] -> Specification a

  -- | This can be used to detect self inconsistencies in a (TypeSpec t)

  --   Note this is similar to 'typeSpecHasError', and the default

  --   value for 'typeSpecHasError' is written in terms of 'guardTypeSpec'

  --   Both 'typeSpecHasError' and 'guardTypeSpec' can be set individually.

  guardTypeSpec :: [String] -> TypeSpec a -> Specification a

  -- | Prerequisites for the instance that are sometimes necessary

  -- when working with e.g. `Specification`s or functions in the universe.

  type Prerequisites a :: Constraint

  type Prerequisites a = ()

  -- | Materialize the `Prerequisites` dictionary. It should not be necessary to

  -- implement this function manually.

  prerequisites :: Evidence (Prerequisites a)

  default prerequisites :: Prerequisites a => Evidence (Prerequisites a)

  {- NOTE: Below follows default implementations for the functions in this

     class based on Generics.  They are meant to provide an implementation of

     `HasSpec a` when `HasSimpleRep a` and `HasSpec (SimpleRep a)`. For example,

     for a newtype wrapper like `newtype Foo = Foo Word64` we can define `SimpleRep

     Foo = Word64` with the requisite instance for `HasSimpleRep` (all of which

     is derived from `Generic Foo`) and the instance for `HasSpec Foo` is

     essentially the same as the instance for `Word64`. This is achieved by

     ensuring that `TypeSpec Foo = TypeSpec Word64` (c.f. the default

     implementation of `TypeSpec` above). To this end, the implementations

     below simply convert the relevant things between `SimpleRep a` and `a`.

     For example, in the implementation of `combineSpec s s'` we treat `s` and

     `s'` (which have type `TypeSpec a`) as `TypeSpec (SimpleRep a)`,

     combine them, and go from the resulting `Specification (SimpleRep a)` to `Specification

     a` using `fromSimpleRepSpec`.

   -}

  default emptySpec :: GenericallyInstantiated a => TypeSpec a

  default combineSpec ::

    GenericallyInstantiated a =>

    TypeSpec a ->

    TypeSpec a ->

    Specification a

  default genFromTypeSpec ::

    (GenericallyInstantiated a, HasCallStack, MonadGenError m) =>

    TypeSpec a ->

    GenT m a

  default conformsTo ::

    (GenericallyInstantiated a, HasCallStack) =>

    a ->

    TypeSpec a ->

    Bool

  default toPreds ::

    GenericallyInstantiated a =>

    Term a ->

    TypeSpec a ->

    Pred

  default shrinkWithTypeSpec ::

    GenericallyInstantiated a =>

    TypeSpec a ->

    a ->

    [a]

  default fixupWithTypeSpec ::

    GenericallyInstantiated a =>

    TypeSpec a ->

    a ->

    Maybe a

  default cardinalTypeSpec ::

    GenericallyInstantiated a =>

    TypeSpec a ->

    Specification Integer

------------------------------------------------------------------------

-- Some instances of HasSpec

------------------------------------------------------------------------

-- | NOTE: this instance means we have to use `ifElse`, `whenTrue`, and `whenFalse` instead

-- of `caseOn` for `Bool`

  type TypeSpec Bool = ()

  type TypeSpec () = ()

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

-- toGeneric and fromGeneric as Function Symbols

-- That means they can be used inside (Term a)

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

-- | The things you need to know to work with the generics which translates things

-- into their SimpleRep, made of Sum and Prod

type GenericRequires a =

  ( HasSpec a -- This gives Show, Eq, and Typeable instances

  , GenericallyInstantiated a

  )

-- | The constructors of BaseW, are first order data (i.e Function Symbols) that describe functions.

-- The Base functions are just the functions neccessary to define Specification, and the classes

-- HasSimpleRep, HasSpec, Syntax, Semantics, and Logic. We call BaseW a 'witness type', and use

-- the convention that all witness types (and their constructors) have "W" as thrit last character.

data BaseW (dom :: [Type]) (rng :: Type) where

  ToGenericW :: GenericRequires a => BaseW '[a] (SimpleRep a)

  FromGenericW :: GenericRequires a => BaseW '[SimpleRep a] a

instance Semantics BaseW where

-- -- ============== ToGenericW Logic instance

  rewriteRules (FromGenericW :: BaseW dom rng) (ToGeneric (x :: Term a) :> Nil) Evidence

-- | Convert an @a@ to a @`SimpleRep` a@

toGeneric_ ::

  forall a.

  GenericRequires a =>

  Term a ->

  Term (SimpleRep a)

-- | Convert an @`SimpleRep` a@ to an @a@

fromGeneric_ ::

  forall a.

  (GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>

  Term (SimpleRep a) ->

  Term a

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

-- Generic Transformers

-- Using Generics to transform from ordinary (Specifications a) to

-- Specifications over 'a's SimpleRep (Specification (SimpleRep a))

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

-- | Convert a `Specification` for a @`SimpleRep` a@ to one for @a@

fromSimpleRepSpec ::

  GenericRequires a =>

  Specification (SimpleRep a) ->

  Specification a

  SuspendedSpec x p ->

-- | Convert a @`Specification` a@ to one for @`SimpleRep` a@

toSimpleRepSpec ::

  forall a.

  GenericRequires a =>

  Specification a ->

  Specification (SimpleRep a)

  SuspendedSpec x p ->

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

-- Now the supporting operations and types.

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

-- | Used to show binary operators like SumSpec and PairSpec

data BinaryShow where

  BinaryShow :: forall a. String -> [Doc a] -> BinaryShow

  NonBinary :: BinaryShow

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

-- Term

-- | Like 'appSym' but builds functions over terms, rather that just one App term.

appTerm ::

  forall t ds r.

  AppRequires t ds r =>

  t ds r ->

  FunTy (MapList Term ds) (Term r)

-- | Give a `Term` a `String` name-hint _if_ the `Term` is a variable

name :: String -> Term a -> Term a

-- | Create a `Binder` with a fresh variable, used in e.g. `constrained`

bind :: (HasSpec a, IsPred p) => (Term a -> p) -> Binder a

  where

    boundBinder :: Binder a -> Int

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

-- Pred

-- | A collection @t@ with elements of type @e@ where the `forAll` syntax will

-- work

class Forallable t e | t -> e where

  -- | Lift the `Specification` for the elements to the collection

  fromForAllSpec ::

    (HasSpec t, HasSpec e) => Specification e -> Specification t

  default fromForAllSpec ::

    ( HasSpec e

    , Forallable (SimpleRep t) e

    , GenericRequires t

    ) =>

    Specification e ->

    Specification t

  -- | Get the underlying items in the collection

  forAllToList :: t -> [e]

  default forAllToList ::

    ( HasSimpleRep t

    , Forallable (SimpleRep t) e

    ) =>

    t ->

    [e]

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

-- IsPred

-- | Something from which we can construct a `Pred`, useful for providing

-- flexible syntax for `constrained` and friends.

class Show p => IsPred p where

  -- | Convert to a `Pred`

  toPred :: p -> Pred

instance IsPred Pred where

instance IsPred p => IsPred [p] where

instance IsPred Bool where

instance IsPred (Term Bool) where

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

-- Simple Widely used operations on Specification

-- | return a MemberSpec or ans ErrorSpec depending on if 'xs' is null or not

memberSpec :: Foldable f => f a -> NE.NonEmpty String -> Specification a

-- | Attach an explanation to a specification in order to track issues with satisfiability

explainSpec :: [String] -> Specification a -> Specification a

-- | A "discrete" specification satisfied by exactly one element

equalSpec :: a -> Specification a

-- | Anything but this

notEqualSpec :: forall a. HasSpec a => a -> Specification a

-- | Anything but these

notMemberSpec :: forall a f. (HasSpec a, Foldable f) => f a -> Specification a

-- | Build a `Specification` using predicates, e.g.

-- > constrained $ \ x -> assert $ x `elem_` lit [1..10 :: Int]

constrained ::

  forall a p.

  (IsPred p, HasSpec a) =>

  (Term a -> p) ->

  Specification a

-- | Sound but not complete check for empty `Specification`s

isErrorLike :: forall a. Specification a -> Bool

isErrorLike (TypeSpec x _) =

-- | Get the error message of an `isErrorLike` `Specification`

errorLikeMessage :: forall a. Specification a -> NE.NonEmpty String

errorLikeMessage (TypeSpec x _) =

-- | Add the explanations, if it's an ErrorSpec, else drop them

addToErrorSpec :: NE.NonEmpty String -> Specification a -> Specification a

------------------------------------------------------------------------

-- Pretty and Show instances

------------------------------------------------------------------------

-- | The Fun type encapuslates a Logic instance and symbol universe type to

-- hide everything but the domain and range. This is a way to pass around

-- functions without pain. Usefull in the ListFoldy implementaion that deals

-- with higher order functions.

data Fun dom rng where

  Fun ::

    forall t dom rng.

    AppRequires t dom rng =>

    t dom rng ->

    Fun dom rng

-- | Apply a single-argument `Fun` to a `Term`

appFun :: Fun '[x] b -> Term x -> Term b

sameFun :: Fun d1 r1 -> Fun d2 r2 -> Bool

-- | Pattern-match on an application of `fromGeneric_`, useful for writing

-- custom rewrite rules to help the solver

pattern FromGeneric ::

  forall rng.

  () =>

  forall a.

  (rng ~ a, GenericRequires a, HasSpec a, AppRequires BaseW '[SimpleRep a] rng) =>

  Term (SimpleRep a) ->

  Term rng

pattern FromGeneric x <-

-- | Pattern-match on an application of `toGeneric_`, useful for writing custom

-- rewrite rules to help the solver

pattern ToGeneric ::

  forall rng.

  () =>

  forall a.

  (rng ~ SimpleRep a, GenericRequires a, HasSpec a, AppRequires BaseW '[a] rng) =>

  Term a ->

  Term rng

-- | Hints are things that only affect generation, and not validation. For instance, parameters to

--   control distribution of generated values.

class (HasSpec a, Show (Hint a)) => HasGenHint a where

  type Hint a

  giveHint :: Hint a -> Specification a