{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
-- Show Evidence
{-# OPTIONS_GHC -Wno-orphans -Wno-unticked-promoted-constructors #-}

-- | 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 where

import Constrained.Core (
  Evidence (..),
  Value (..),
  Var (..),
  eqVar,
 )
import Constrained.GenT (
  GE (..),
  GenT,
  MonadGenError (..),
  catMessageList,
  catMessages,
  fatalError,
 )
import Constrained.Generic (
  HasSimpleRep,
  SimpleRep,
  SumOver,
  fromSimpleRep,
  toSimpleRep,
 )
import Constrained.List (
  All,
  FunTy,
  List (..),
  ListCtx (..),
  MapList,
  TypeList,
  curryList,
  fillListCtx,
  foldMapList,
  mapListCtxC,
  pattern ListCtx,
  pattern NilCtx,
 )
import Constrained.TypeErrors

import Control.Monad.Writer (
  Writer,
  tell,
 )
import Data.Foldable (
  toList,
 )
import Data.Kind (Constraint, Type)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NE
import Data.Orphans ()
import Data.Semigroup (Max (..), getMax)
import Data.String (fromString)
import Data.Typeable
import GHC.Stack
import Prettyprinter hiding (cat)
import Test.QuickCheck hiding (Args, Fun, Witness, forAll, witness)

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

-- | 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.

-- | Syntactic operations are ones that have to do with the structure and appearence of the type.
class Syntax (t :: [Type] -> Type -> Type) where
  inFix :: forall dom rng. t dom rng -> Bool
  inFix t dom rng
_ = Bool
False
  prettyWit ::
    forall dom rng ann.
    (All HasSpec dom, HasSpec rng) =>
    t dom rng ->
    List Term dom ->
    Int ->
    Maybe (Doc ann)
  prettyWit t dom rng
_ List Term dom
_ Int
_ = forall a. Maybe a
Nothing

-- | Semantic operations are ones that give the function symbol, meaning as a function.
--   I.e. how to apply the function to a list of arguments and return a value.
class Syntax t => Semantics (t :: [Type] -> Type -> Type) where
  semantics :: forall d r. t d r -> FunTy d r -- e.g. FunTy '[a,Int] Bool == a -> Int -> Bool

-- -- What properties we need to have Logical operations.
type LogicRequires t =
  ( Typeable t
  , Syntax t
  , Semantics t
  )

-- | Logical operations are one that support reasoning about how a function symbol
--   relates to logical properties, that we call Specification's
class LogicRequires 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
  propagateTypeSpec t as b
f ListCtx Value as (HOLE a)
ctx TypeSpec b
ts [b]
cant = forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate t as b
f ListCtx Value as (HOLE a)
ctx (forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec b
ts [b]
cant)

  propagateMemberSpec ::
    (AppRequires t as b, HasSpec a) =>
    t as b ->
    ListCtx Value as (HOLE a) ->
    NonEmpty b ->
    Specification a
  propagateMemberSpec t as b
f ListCtx Value as (HOLE a)
ctx NonEmpty b
xs = forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate t as b
f ListCtx Value as (HOLE a)
ctx (forall a. NonEmpty a -> Specification a
MemberSpec NonEmpty b
xs)

  propagate ::
    (AppRequires t as b, HasSpec a) =>
    t as b ->
    ListCtx Value as (HOLE a) ->
    Specification b ->
    Specification a
  propagate t as b
f ListCtx Value as (HOLE a)
ctx (ExplainSpec [String]
es Specification b
s) = forall a. [String] -> Specification a -> Specification a
explainSpec [String]
es (forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate t as b
f ListCtx Value as (HOLE a)
ctx Specification b
s)
  propagate t as b
_ ListCtx Value as (HOLE a)
_ Specification b
TrueSpec = forall a. Specification a
TrueSpec
  propagate t as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
es) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
es
  propagate t as b
f ListCtx Value as (HOLE a)
ctx (SuspendedSpec Var b
v Pred
ps) = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (a :: [*] -> * -> *) (as :: [*]) rng.
AppRequires a as rng =>
a as rng -> List Term as -> Term rng
App t as b
f (forall (as :: [*]) a.
All HasSpec as =>
ListCtx Value as (HOLE a) -> Term a -> List Term as
fromListCtx ListCtx Value as (HOLE a)
ctx Term a
v')) (Var b
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate t as b
f ListCtx Value as (HOLE a)
ctx (TypeSpec TypeSpec b
ts [b]
cant) = forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a)
-> TypeSpec b
-> [b]
-> Specification a
propagateTypeSpec t as b
f ListCtx Value as (HOLE a)
ctx TypeSpec b
ts [b]
cant
  propagate t as b
f ListCtx Value as (HOLE a)
ctx (MemberSpec NonEmpty b
xs) = forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> NonEmpty b -> Specification a
propagateMemberSpec t as b
f ListCtx Value as (HOLE a)
ctx NonEmpty b
xs

  rewriteRules ::
    (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) =>
    t dom rng ->
    List Term dom ->
    Evidence (AppRequires t dom rng) ->
    Maybe (Term rng)
  rewriteRules t dom rng
_ List Term dom
_ Evidence (AppRequires t dom rng)
_ = forall a. Maybe a
Nothing

  mapTypeSpec ::
    forall a b.
    (HasSpec a, HasSpec b) =>
    t '[a] b ->
    TypeSpec a ->
    Specification b
  mapTypeSpec t '[a] b
_ts TypeSpec a
_spec = forall a. Specification a
TrueSpec

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

-- 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
propagateSpec :: forall v a.
HasSpec v =>
Specification a -> Ctx v a -> Specification v
propagateSpec Specification a
spec = \case
  Ctx v a
CtxHOLE -> Specification a
spec
  CtxApp fn as a
f (ListCtx List Value as
pre Ctx v a
c List Value as'
suf)
    | Evidence (HasSpec a)
Evidence <- forall v a. Ctx v a -> Evidence (HasSpec a)
ctxHasSpec Ctx v a
c -> forall v a.
HasSpec v =>
Specification a -> Ctx v a -> Specification v
propagateSpec (forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate fn as a
f (forall (as'' :: [*]) (f :: * -> *) (c :: * -> *) (as :: [*]) a
       (as' :: [*]).
(as'' ~ Append as (a : as')) =>
List f as -> c a -> List f as' -> ListCtx f as'' c
ListCtx List Value as
pre forall {k} (a :: k). HOLE a a
HOLE List Value as'
suf) Specification a
spec) Ctx v a
c

ctxHasSpec :: Ctx v a -> Evidence (HasSpec a)
ctxHasSpec :: forall v a. Ctx v a -> Evidence (HasSpec a)
ctxHasSpec Ctx v a
CtxHOLE = forall (c :: Constraint). c => Evidence c
Evidence
ctxHasSpec CtxApp {} = forall (c :: Constraint). c => Evidence c
Evidence

-- | 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

toCtx ::
  forall m v a.
  ( Typeable v
  , Show v
  , MonadGenError m
  , HasCallStack
  ) =>
  Var v ->
  Term a ->
  m (Ctx v a)
toCtx :: forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var v
v = forall b. Term b -> m (Ctx v b)
go
  where
    go :: forall b. Term b -> m (Ctx v b)
    go :: forall b. Term b -> m (Ctx v b)
go (Lit b
i) =
      forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE forall a b. (a -> b) -> a -> b
$
        forall a. [a] -> NonEmpty a
NE.fromList
          [ String
"toCtx applied to literal: (Lit " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show b
i forall a. [a] -> [a] -> [a]
++ String
")"
          , String
"A context is always constructed from an (App f xs) term."
          ]
    go (App t dom b
f List Term dom
as) = forall (a :: [*] -> * -> *) (as :: [*]) b v.
(AppRequires a as b, HasSpec b, TypeList as, Typeable as,
 All HasSpec as, Logic a) =>
a as b -> ListCtx Value as (Ctx v) -> Ctx v b
CtxApp t dom b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) v (as :: [*]).
(Show v, Typeable v, MonadGenError m, HasCallStack) =>
Var v -> List Term as -> m (ListCtx Value as (Ctx v))
toCtxList Var v
v List Term dom
as
    go (V Var b
v')
      | Just v :~: b
Refl <- forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var v
v Var b
v' = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall v. HasSpec v => Ctx v v
CtxHOLE
      | Bool
otherwise =
          forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE forall a b. (a -> b) -> a -> b
$
            forall a. [a] -> NonEmpty a
NE.fromList
              [ String
"A context is always constructed from an (App f xs) term,"
              , String
"with a single occurence of the variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var v
v forall a. [a] -> [a] -> [a]
++ String
"@(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Typeable a => a -> TypeRep
typeOf Var v
v) forall a. [a] -> [a] -> [a]
++ String
")"
              , String
"Instead we found an unknown variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var b
v' forall a. [a] -> [a] -> [a]
++ String
"@(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Typeable a => a -> TypeRep
typeOf Var b
v') forall a. [a] -> [a] -> [a]
++ String
")"
              ]

toCtxList ::
  forall m v as.
  (Show v, Typeable v, MonadGenError m, HasCallStack) =>
  Var v ->
  List Term as ->
  m (ListCtx Value as (Ctx v))
toCtxList :: forall (m :: * -> *) v (as :: [*]).
(Show v, Typeable v, MonadGenError m, HasCallStack) =>
Var v -> List Term as -> m (ListCtx Value as (Ctx v))
toCtxList Var v
v List Term as
xs = forall (as' :: [*]).
HasCallStack =>
List Term as' -> m (ListCtx Value as' (Ctx v))
prefix List Term as
xs
  where
    prefix :: forall as'. HasCallStack => List Term as' -> m (ListCtx Value as' (Ctx v))
    prefix :: forall (as' :: [*]).
HasCallStack =>
List Term as' -> m (ListCtx Value as' (Ctx v))
prefix List Term as'
Nil = forall (m :: * -> *) a. MonadGenError m => String -> m a
fatalError (String
"toCtxList without hole, for variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var v
v)
    prefix (Lit a
l :> List Term as1
ts) = do
      ListCtx Value as1 (Ctx v)
ctx <- forall (as' :: [*]).
HasCallStack =>
List Term as' -> m (ListCtx Value as' (Ctx v))
prefix List Term as1
ts
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> Value a
Value a
l forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:! ListCtx Value as1 (Ctx v)
ctx
    prefix (Term a
t :> List Term as1
ts) = do
      Ctx v a
hole <- forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var v
v Term a
t
      List Value as1
suf <- forall (as' :: [*]). List Term as' -> m (List Value as')
suffix List Term as1
ts
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Ctx v a
hole forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? List Value as1
suf

    suffix :: forall as'. List Term as' -> m (List Value as')
    suffix :: forall (as' :: [*]). List Term as' -> m (List Value as')
suffix List Term as'
Nil = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). List f '[]
Nil
    suffix (Lit a
l :> List Term as1
ts) = (forall a. Show a => a -> Value a
Value a
l forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (as' :: [*]). List Term as' -> m (List Value as')
suffix List Term as1
ts
    suffix (Term a
_ :> List Term as1
_) = forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE forall a b. (a -> b) -> a -> b
$ forall a. [a] -> NonEmpty a
NE.fromList [String
"toCtxList with too many holes, for variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var v
v]

-- | A Convenient pattern for singleton contexts
pattern Unary :: HOLE a' a -> ListCtx f '[a] (HOLE a')
pattern $bUnary :: forall a' a (f :: * -> *). HOLE a' a -> ListCtx f '[a] (HOLE a')
$mUnary :: forall {r} {a'} {a} {f :: * -> *}.
ListCtx f '[a] (HOLE a') -> (HOLE a' a -> r) -> ((# #) -> r) -> r
Unary h = NilCtx h

{-# 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)
pattern h $b:<: :: forall b c a.
(Typeable b, Show b) =>
HOLE c a -> b -> ListCtx Value '[a, b] (HOLE c)
$m:<: :: forall {r} {b} {c} {a}.
(Typeable b, Show b) =>
ListCtx Value '[a, b] (HOLE c)
-> (HOLE c a -> b -> r) -> ((# #) -> r) -> r
:<: a = h :? Value a :> Nil

-- | 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)
pattern a $b:>: :: forall a c b.
(Typeable a, Show a) =>
a -> HOLE c b -> ListCtx Value '[a, b] (HOLE c)
$m:>: :: forall {r} {a} {c} {b}.
(Typeable a, Show a) =>
ListCtx Value '[a, b] (HOLE c)
-> (a -> HOLE c b -> r) -> ((# #) -> r) -> r
:>: h = Value a :! NilCtx h

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

flipCtx ::
  (Typeable a, Show a, Typeable b, Show b) =>
  ListCtx Value '[a, b] (HOLE c) -> ListCtx Value '[b, a] (HOLE c)
flipCtx :: forall a b c.
(Typeable a, Show a, Typeable b, Show b) =>
ListCtx Value '[a, b] (HOLE c) -> ListCtx Value '[b, a] (HOLE c)
flipCtx (HOLE c a
HOLE :<: b
x) = b
x forall a c b.
(Typeable a, Show a) =>
a -> HOLE c b -> ListCtx Value '[a, b] (HOLE c)
:>: forall {k} (a :: k). HOLE a a
HOLE
flipCtx (a
x :>: HOLE c b
HOLE) = forall {k} (a :: k). HOLE a a
HOLE forall b c a.
(Typeable b, Show b) =>
HOLE c a -> b -> ListCtx Value '[a, b] (HOLE c)
:<: a
x

-- | 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
fromListCtx :: forall (as :: [*]) a.
All HasSpec as =>
ListCtx Value as (HOLE a) -> Term a -> List Term as
fromListCtx ListCtx Value as (HOLE a)
ctx Term a
t = forall (f :: * -> *) (as :: [*]) (c :: * -> *).
ListCtx f as c -> (forall a. c a -> f a) -> List f as
fillListCtx (forall (c :: * -> Constraint) (as :: [*]) (f :: * -> *)
       (g :: * -> *) (h :: * -> *).
All c as =>
(forall a. c a => f a -> g a) -> ListCtx f as h -> ListCtx g as h
mapListCtxC @HasSpec (\(Value a
a) -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a) ListCtx Value as (HOLE a)
ctx) (\HOLE a a
HOLE -> Term a
t)

-- ========================================================================
-- Useful for testing if two function symbols are `the same` for some notion of `the same`

sameFunSym ::
  forall (t1 :: [Type] -> Type -> Type) d1 r1 (t2 :: [Type] -> Type -> Type) d2 r2.
  (AppRequires t1 d1 r1, AppRequires t2 d2 r2) =>
  t1 d1 r1 ->
  t2 d2 r2 ->
  Maybe (t1 d1 r1, t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym :: forall (t1 :: [*] -> * -> *) (d1 :: [*]) r1 (t2 :: [*] -> * -> *)
       (d2 :: [*]) r2.
(AppRequires t1 d1 r1, AppRequires t2 d2 r2) =>
t1 d1 r1
-> t2 d2 r2 -> Maybe (t1 d1 r1, t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym t1 d1 r1
x t2 d2 r2
y = do
  t :: t1 :~: t2
t@t1 :~: t2
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @t1 @t2
  d :: d1 :~: d2
d@d1 :~: d2
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @d1 @d2
  r :: r1 :~: r2
r@r1 :~: r2
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @r1 @r2
  if t1 d1 r1
x forall a. Eq a => a -> a -> Bool
== t2 d2 r2
y
    then forall a. a -> Maybe a
Just (t1 d1 r1
x, t1 :~: t2
t, d1 :~: d2
d, r1 :~: r2
r)
    else forall a. Maybe a
Nothing

-- | Here we only care about the Type 't' and the Symbol 's'
--   the dom, and the rng can be anything. Useful for defining patterns.
getWitness :: forall t t' d r. (AppRequires t d r, Typeable t') => t d r -> Maybe (t' d r)
getWitness :: forall (t :: [*] -> * -> *) (t' :: [*] -> * -> *) (d :: [*]) r.
(AppRequires t d r, Typeable t') =>
t d r -> Maybe (t' d r)
getWitness = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast

-- ========================================================
-- A Specification tells us what constraints must hold
-- ========================================================

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

typeSpec :: HasSpec a => TypeSpec a -> Specification a
typeSpec :: forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
ts = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec a
ts forall a. Monoid a => a
mempty

-- =================================================================
-- 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.
-- =================================================================

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)
  )

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
  ( 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`.

  emptySpec :: TypeSpec a
  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]

  -- | 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
  cardinalTrueSpec = forall a. Specification a
TrueSpec

  -- 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)
  typeSpecHasError TypeSpec a
tspec = case forall a. HasSpec a => [String] -> TypeSpec a -> Specification a
guardTypeSpec @a [] TypeSpec a
tspec of
    ErrorSpec NonEmpty String
msgs -> forall a. a -> Maybe a
Just NonEmpty String
msgs
    Specification a
_ -> forall a. Maybe a
Nothing

  -- 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
  alternateShow TypeSpec a
_ = BinaryShow
NonBinary

  monadConformsTo :: a -> TypeSpec a -> Writer [String] Bool
  monadConformsTo a
x TypeSpec a
spec =
    if forall a. (HasSpec a, HasCallStack) => a -> TypeSpec a -> Bool
conformsTo @a a
x TypeSpec a
spec
      then forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      else forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [String
"Fails by " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeSpec a
spec] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

  -- | 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
  typeSpecOpt TypeSpec a
tySpec [a]
bad = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec a
tySpec [a]
bad

  -- | 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
  guardTypeSpec [String]
_ TypeSpec a
ty = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
ty

  -- | 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)
  prerequisites = forall (c :: Constraint). c => Evidence c
Evidence

  {- 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
  emptySpec = forall a. HasSpec a => TypeSpec a
emptySpec @(SimpleRep a)

  default combineSpec ::
    GenericallyInstantiated a =>
    TypeSpec a ->
    TypeSpec a ->
    Specification a
  combineSpec TypeSpec a
s TypeSpec a
s' = forall a.
(HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => TypeSpec a -> TypeSpec a -> Specification a
combineSpec @(SimpleRep a) TypeSpec a
s TypeSpec a
s'

  default genFromTypeSpec ::
    (GenericallyInstantiated a, HasCallStack, MonadGenError m) =>
    TypeSpec a ->
    GenT m a
  genFromTypeSpec TypeSpec a
s = forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(HasSpec a, HasCallStack, MonadGenError m) =>
TypeSpec a -> GenT m a
genFromTypeSpec TypeSpec a
s

  default conformsTo ::
    (GenericallyInstantiated a, HasCallStack) =>
    a ->
    TypeSpec a ->
    Bool
  a
a `conformsTo` TypeSpec a
s = forall a. (HasSpec a, HasCallStack) => a -> TypeSpec a -> Bool
conformsTo (forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep a
a) TypeSpec a
s

  default toPreds ::
    GenericallyInstantiated a =>
    Term a ->
    TypeSpec a ->
    Pred
  toPreds Term a
v TypeSpec a
s = forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds (forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term a
v) TypeSpec a
s

  default shrinkWithTypeSpec ::
    GenericallyInstantiated a =>
    TypeSpec a ->
    a ->
    [a]
  shrinkWithTypeSpec TypeSpec a
spec a
a = forall a b. (a -> b) -> [a] -> [b]
map forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => TypeSpec a -> a -> [a]
shrinkWithTypeSpec TypeSpec a
spec (forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep a
a)

  default cardinalTypeSpec ::
    GenericallyInstantiated a =>
    TypeSpec a ->
    Specification Integer
  cardinalTypeSpec = forall a. HasSpec a => TypeSpec a -> Specification Integer
cardinalTypeSpec @(SimpleRep a)

-- ===================================================================
-- 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
  , HasSimpleRep a
  , HasSpec (SimpleRep a)
  , TypeSpec a ~ TypeSpec (SimpleRep 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
deriving instance Eq (BaseW dom rng)

instance Show (BaseW d r) where
  show :: BaseW d r -> String
show BaseW d r
ToGenericW = String
"toSimpleRep"
  show BaseW d r
FromGenericW = String
"fromSimpleRep"

instance Syntax BaseW where
  prettyWit :: forall (dom :: [*]) rng ann.
(All HasSpec dom, HasSpec rng) =>
BaseW dom rng -> List Term dom -> Int -> Maybe (Doc ann)
prettyWit BaseW dom rng
ToGenericW (Term a
x :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Doc ann
"to" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Int -> a -> WithPrec a
WithPrec Int
p Term a
x)
  prettyWit BaseW dom rng
FromGenericW (Term a
x :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Doc ann
"from" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Int -> a -> WithPrec a
WithPrec Int
p Term a
x)

instance Semantics BaseW where
  semantics :: forall (d :: [*]) r. BaseW d r -> FunTy d r
semantics BaseW d r
FromGenericW = forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep
  semantics BaseW d r
ToGenericW = forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep

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

instance Logic BaseW where
  propagateTypeSpec :: forall (as :: [*]) b a.
(AppRequires BaseW as b, HasSpec a) =>
BaseW as b
-> ListCtx Value as (HOLE a)
-> TypeSpec b
-> [b]
-> Specification a
propagateTypeSpec BaseW as b
ToGenericW (Unary HOLE a a
HOLE) TypeSpec b
s [b]
cant = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec b
s (forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b]
cant)
  propagateTypeSpec BaseW as b
FromGenericW (Unary HOLE a (SimpleRep b)
HOLE) TypeSpec b
s [b]
cant = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec b
s (forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b]
cant)

  propagateMemberSpec :: forall (as :: [*]) b a.
(AppRequires BaseW as b, HasSpec a) =>
BaseW as b
-> ListCtx Value as (HOLE a) -> NonEmpty b -> Specification a
propagateMemberSpec BaseW as b
ToGenericW (Unary HOLE a a
HOLE) NonEmpty b
es = forall a. NonEmpty a -> Specification a
MemberSpec (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep NonEmpty b
es)
  propagateMemberSpec BaseW as b
FromGenericW (Unary HOLE a (SimpleRep b)
HOLE) NonEmpty b
es = forall a. NonEmpty a -> Specification a
MemberSpec (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep NonEmpty b
es)

  mapTypeSpec :: forall a b.
(HasSpec a, HasSpec b) =>
BaseW '[a] b -> TypeSpec a -> Specification b
mapTypeSpec BaseW '[a] b
ToGenericW TypeSpec a
ts = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
ts
  mapTypeSpec BaseW '[a] b
FromGenericW TypeSpec a
ts = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
ts

  rewriteRules :: forall (dom :: [*]) rng.
(TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) =>
BaseW dom rng
-> List Term dom
-> Evidence (AppRequires BaseW dom rng)
-> Maybe (Term rng)
rewriteRules BaseW dom rng
ToGenericW (FromGeneric Term (SimpleRep a)
x :> List Term as1
Nil) Evidence (AppRequires BaseW dom rng)
Evidence = forall a. a -> Maybe a
Just Term (SimpleRep a)
x
  rewriteRules (BaseW dom rng
FromGenericW :: BaseW dom rng) (ToGeneric (Term a
x :: Term a) :> List Term as1
Nil) Evidence (AppRequires BaseW dom rng)
Evidence
    | Just rng :~: a
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @rng @a = forall a. a -> Maybe a
Just Term a
x
  rewriteRules BaseW dom rng
_ List Term dom
_ Evidence (AppRequires BaseW dom rng)
_ = forall a. Maybe a
Nothing

toGeneric_ ::
  forall a.
  GenericRequires a =>
  Term a ->
  Term (SimpleRep a)
toGeneric_ :: forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW

fromGeneric_ ::
  forall a.
  (GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
  Term (SimpleRep a) ->
  Term a
fromGeneric_ :: forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. GenericRequires a => BaseW '[SimpleRep a] a
FromGenericW

-- ====================================================================
-- Generic Transformers
-- Using Generics to transform from ordinary (Specifications a) to
-- Specifications over 'a's SimpleRep (Specification (SimpleRep a))
-- ====================================================================

fromSimpleRepSpec ::
  forall a.
  (HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) =>
  Specification (SimpleRep a) ->
  Specification a
fromSimpleRepSpec :: forall a.
(HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec = \case
  ExplainSpec [String]
es Specification (SimpleRep a)
s -> forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (forall a.
(HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec Specification (SimpleRep a)
s)
  Specification (SimpleRep a)
TrueSpec -> forall a. Specification a
TrueSpec
  ErrorSpec NonEmpty String
e -> forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
e
  TypeSpec TypeSpec (SimpleRep a)
s'' [SimpleRep a]
cant -> forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec (SimpleRep a)
s'' forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep [SimpleRep a]
cant
  MemberSpec NonEmpty (SimpleRep a)
elems -> forall a. NonEmpty a -> Specification a
MemberSpec forall a b. (a -> b) -> a -> b
$ forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep NonEmpty (SimpleRep a)
elems)
  SuspendedSpec Var (SimpleRep a)
x Pred
p ->
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
x' ->
      forall a. Term a -> Binder a -> Pred
Let (forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term a
x') (Var (SimpleRep a)
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
p)

toSimpleRepSpec ::
  forall a.
  ( HasSpec (SimpleRep a)
  , HasSimpleRep a
  , TypeSpec a ~ TypeSpec (SimpleRep a)
  ) =>
  Specification a ->
  Specification (SimpleRep a)
toSimpleRepSpec :: forall a.
(HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a)) =>
Specification a -> Specification (SimpleRep a)
toSimpleRepSpec = \case
  ExplainSpec [String]
es Specification a
s -> forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (forall a.
(HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a)) =>
Specification a -> Specification (SimpleRep a)
toSimpleRepSpec Specification a
s)
  Specification a
TrueSpec -> forall a. Specification a
TrueSpec
  ErrorSpec NonEmpty String
e -> forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
e
  TypeSpec TypeSpec a
s'' [a]
cant -> forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec a
s'' forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep [a]
cant
  MemberSpec NonEmpty a
elems -> forall a. NonEmpty a -> Specification a
MemberSpec forall a b. (a -> b) -> a -> b
$ forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep NonEmpty a
elems
  SuspendedSpec Var a
x Pred
p ->
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (SimpleRep a)
x' ->
      forall a. Term a -> Binder a -> Pred
Let (forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ Term (SimpleRep a)
x') (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
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

-- | What constraints does the Term constructor App require?
--   (Logic sym t dom rng) supplies the Logic of propagating contexts
--   (All HasSpec dom) the argument types are part of the system
--   (HasSpec rng) the return type is part of the system.
type AppRequires t dom rng =
  ( Logic t
  , TypeList dom
  , Eq (t dom rng)
  , Show (t dom rng)
  , Typeable dom
  , Typeable rng
  , All HasSpec dom
  , HasSpec rng
  )

data Term a where
  App ::
    forall t dom rng.
    AppRequires t dom rng =>
    t dom rng ->
    List Term dom ->
    Term rng
  Lit :: (Typeable a, Eq a, Show a) => a -> Term a
  V :: HasSpec a => Var a -> Term a

instance Eq (Term a) where
  V Var a
x == :: Term a -> Term a -> Bool
== V Var a
x' = Var a
x forall a. Eq a => a -> a -> Bool
== Var a
x'
  Lit a
a == Lit a
b = a
a forall a. Eq a => a -> a -> Bool
== a
b
  App (t dom a
w1 :: x1) (List Term dom
ts :: List Term dom1) == App (t dom a
w2 :: x2) (List Term dom
ts' :: List Term dom2) =
    case (forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @dom1 @dom2, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @x1 @x2) of
      (Just dom :~: dom
Refl, Just t dom a :~: t dom a
Refl) ->
        t dom a
w1 forall a. Eq a => a -> a -> Bool
== t dom a
w2
          Bool -> Bool -> Bool
&& forall (as :: [*]).
All HasSpec as =>
List Term as -> List Term as -> Bool
sameTerms List Term dom
ts List Term dom
ts'
      (Maybe (dom :~: dom), Maybe (t dom a :~: t dom a))
_ -> Bool
False
  Term a
_ == Term a
_ = Bool
False

-- How to compare the args of two applications for equality
sameTerms :: All HasSpec as => List Term as -> List Term as -> Bool
sameTerms :: forall (as :: [*]).
All HasSpec as =>
List Term as -> List Term as -> Bool
sameTerms List Term as
Nil List Term as
Nil = Bool
True
sameTerms (Term a
x :> List Term as1
xs) (Term a
y :> List Term as1
ys) = Term a
x forall a. Eq a => a -> a -> Bool
== Term a
y Bool -> Bool -> Bool
&& forall (as :: [*]).
All HasSpec as =>
List Term as -> List Term as -> Bool
sameTerms List Term as1
xs List Term as1
ys

-- Building App terms

-- | Recall function symbols are objects that you can use to build applications
--   They carry information about both its semantic and logical properties.
--   Usually the Haskel name ends in '_', for example consider: not_, subset_ ,lookup_, toGeneric_
--   Infix function symbols names end in '.', for example: ==. , <=.
--   E.g  appTerm ToGenericW  :: Term a -> Term(SimpleRep a)
--        (appTerm ToGenericW  (lit True)) builds the Term  (toGeneric_ True)
--   Note the witness (ToGenericW ) must have a Logic instance like:
--   instance Logic      BaseW          '[a]           (SimpleRep a) where ...
--        type of ToGenericW ^    arg types^            result type^
--   The Logic instance does not demand any of these things have any properties at all.
--   It is here, where we actually build the App node, that we demand the properties App terms require.
--   App :: AppRequires s t ds r => t s ds r -> List Term dom -> Term rng
appSym ::
  forall t as b.
  AppRequires t as b =>
  t as b ->
  List Term as ->
  Term b
appSym :: forall (a :: [*] -> * -> *) (as :: [*]) rng.
AppRequires a as rng =>
a as rng -> List Term as -> Term rng
appSym t as b
w List Term as
xs = forall (a :: [*] -> * -> *) (as :: [*]) rng.
AppRequires a as rng =>
a as rng -> List Term as -> Term rng
App t as b
w List Term as
xs

-- 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)
appTerm :: forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm t ds r
sym = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
curryList @ds (forall (a :: [*] -> * -> *) (as :: [*]) rng.
AppRequires a as rng =>
a as rng -> List Term as -> Term rng
App @t @ds @r t ds r
sym)

name :: String -> Term a -> Term a
name :: forall a. String -> Term a -> Term a
name String
nh (V (Var Int
i String
_)) = forall a. HasSpec a => Var a -> Term a
V (forall a. Int -> String -> Var a
Var Int
i String
nh)
name String
_ Term a
_ = forall a. HasCallStack => String -> a
error String
"applying name to non-var thing! Shame on you!"

-- | Give a Term a nameHint, if its a Var, and doesn't already have one,
--  otherwise return the Term unchanged.
named :: String -> Term a -> Term a
named :: forall a. String -> Term a -> Term a
named String
nh t :: Term a
t@(V (Var Int
i String
x)) = if String
x forall a. Eq a => a -> a -> Bool
/= String
"v" then Term a
t else forall a. HasSpec a => Var a -> Term a
V (forall a. Int -> String -> Var a
Var Int
i String
nh)
named String
_ Term a
t = Term a
t

-- ===========================================
-- Binder

data Binder a where
  (:->) ::
    HasSpec a =>
    Var a ->
    Pred ->
    Binder a

deriving instance Show (Binder a)

bind :: (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind :: forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term a -> p
bodyf = Var a
newv forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
bodyPred
  where
    bodyPred :: Pred
bodyPred = forall p. IsPred p => p -> Pred
toPred p
body
    newv :: Var a
newv = forall a. Int -> String -> Var a
Var (Pred -> Int
nextVar Pred
bodyPred) String
"v"
    body :: p
body = Term a -> p
bodyf (forall a. HasSpec a => Var a -> Term a
V Var a
newv)

    nextVar :: Pred -> Int
nextVar Pred
q = Int
1 forall a. Num a => a -> a -> a
+ Pred -> Int
bound Pred
q

    boundBinder :: Binder a -> Int
    boundBinder :: forall a. Binder a -> Int
boundBinder (Var a
x :-> Pred
p) = forall a. Ord a => a -> a -> a
max (forall a. Var a -> Int
nameOf Var a
x) (Pred -> Int
bound Pred
p)

    bound :: Pred -> Int
bound (ElemPred Bool
_ Term a
_ NonEmpty a
_) = -Int
1
    bound (Explain NonEmpty String
_ Pred
p) = Pred -> Int
bound Pred
p
    bound (Subst Var a
x Term a
_ Pred
p) = forall a. Ord a => a -> a -> a
max (forall a. Var a -> Int
nameOf Var a
x) (Pred -> Int
bound Pred
p)
    bound (And [Pred]
ps) = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ (-Int
1) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Pred -> Int
bound [Pred]
ps -- (-1) as the default to get 0 as `nextVar p`
    bound (Exists (forall b. Term b -> b) -> GE a
_ Binder a
b) = forall a. Binder a -> Int
boundBinder Binder a
b
    bound (Let Term a
_ Binder a
b) = forall a. Binder a -> Int
boundBinder Binder a
b
    bound (ForAll Term t
_ Binder a
b) = forall a. Binder a -> Int
boundBinder Binder a
b
    bound (Case Term (SumOver as)
_ List (Weighted Binder) as
cs) = forall a. Max a -> a
getMax forall a b. (a -> b) -> a -> b
$ forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList (forall a. a -> Max a
Max forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Binder a -> Int
boundBinder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing) List (Weighted Binder) as
cs
    bound (When Term Bool
_ Pred
p) = Pred -> Int
bound Pred
p
    bound Reifies {} = -Int
1
    bound GenHint {} = -Int
1
    bound Assert {} = -Int
1
    bound DependsOn {} = -Int
1
    bound Pred
TruePred = -Int
1
    bound FalsePred {} = -Int
1
    bound Monitor {} = -Int
1

-- =======================================================
-- Weighted

data Weighted f a = Weighted {forall {k} (f :: k -> *) (a :: k). Weighted f a -> Maybe Int
weight :: Maybe Int, forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing :: f a}
  deriving (forall a b. a -> Weighted f b -> Weighted f a
forall a b. (a -> b) -> Weighted f a -> Weighted f b
forall (f :: * -> *) a b.
Functor f =>
a -> Weighted f b -> Weighted f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Weighted f a -> Weighted f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Weighted f b -> Weighted f a
$c<$ :: forall (f :: * -> *) a b.
Functor f =>
a -> Weighted f b -> Weighted f a
fmap :: forall a b. (a -> b) -> Weighted f a -> Weighted f b
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Weighted f a -> Weighted f b
Functor, forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall {f :: * -> *}. Traversable f => Functor (Weighted f)
forall {f :: * -> *}. Traversable f => Foldable (Weighted f)
forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Weighted f (m a) -> m (Weighted f a)
forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Weighted f (f a) -> f (Weighted f a)
forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Weighted f a -> m (Weighted f b)
forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
sequence :: forall (m :: * -> *) a.
Monad m =>
Weighted f (m a) -> m (Weighted f a)
$csequence :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Weighted f (m a) -> m (Weighted f a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Weighted f a -> m (Weighted f b)
$cmapM :: forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Weighted f a -> m (Weighted f b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Weighted f (f a) -> f (Weighted f a)
$csequenceA :: forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Weighted f (f a) -> f (Weighted f a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
$ctraverse :: forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
Traversable, forall a. Weighted f a -> Bool
forall m a. Monoid m => (a -> m) -> Weighted f a -> m
forall a b. (a -> b -> b) -> b -> Weighted f a -> b
forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Weighted f a -> Bool
forall (f :: * -> *) a. (Foldable f, Num a) => Weighted f a -> a
forall (f :: * -> *) a. (Foldable f, Ord a) => Weighted f a -> a
forall (f :: * -> *) m. (Foldable f, Monoid m) => Weighted f m -> m
forall (f :: * -> *) a. Foldable f => Weighted f a -> Bool
forall (f :: * -> *) a. Foldable f => Weighted f a -> Int
forall (f :: * -> *) a. Foldable f => Weighted f a -> [a]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Weighted f a -> a
forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Weighted f a -> m
forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Weighted f a -> b
forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Weighted f a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Weighted f a -> a
$cproduct :: forall (f :: * -> *) a. (Foldable f, Num a) => Weighted f a -> a
sum :: forall a. Num a => Weighted f a -> a
$csum :: forall (f :: * -> *) a. (Foldable f, Num a) => Weighted f a -> a
minimum :: forall a. Ord a => Weighted f a -> a
$cminimum :: forall (f :: * -> *) a. (Foldable f, Ord a) => Weighted f a -> a
maximum :: forall a. Ord a => Weighted f a -> a
$cmaximum :: forall (f :: * -> *) a. (Foldable f, Ord a) => Weighted f a -> a
elem :: forall a. Eq a => a -> Weighted f a -> Bool
$celem :: forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Weighted f a -> Bool
length :: forall a. Weighted f a -> Int
$clength :: forall (f :: * -> *) a. Foldable f => Weighted f a -> Int
null :: forall a. Weighted f a -> Bool
$cnull :: forall (f :: * -> *) a. Foldable f => Weighted f a -> Bool
toList :: forall a. Weighted f a -> [a]
$ctoList :: forall (f :: * -> *) a. Foldable f => Weighted f a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Weighted f a -> a
$cfoldl1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Weighted f a -> a
foldr1 :: forall a. (a -> a -> a) -> Weighted f a -> a
$cfoldr1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Weighted f a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Weighted f a -> b
$cfoldl' :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Weighted f a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Weighted f a -> b
$cfoldl :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Weighted f a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Weighted f a -> b
$cfoldr' :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Weighted f a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Weighted f a -> b
$cfoldr :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Weighted f a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Weighted f a -> m
$cfoldMap' :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Weighted f a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Weighted f a -> m
$cfoldMap :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Weighted f a -> m
fold :: forall m. Monoid m => Weighted f m -> m
$cfold :: forall (f :: * -> *) m. (Foldable f, Monoid m) => Weighted f m -> m
Foldable)

mapWeighted :: (f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted :: forall {k} {k} (f :: k -> *) (a :: k) (g :: k -> *) (b :: k).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted f a -> g b
f (Weighted Maybe Int
w f a
t) = forall {k} (f :: k -> *) (a :: k). Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
w (f a -> g b
f f a
t)

traverseWeighted :: Applicative m => (f a -> m (g a)) -> Weighted f a -> m (Weighted g a)
traverseWeighted :: forall {k} (m :: * -> *) (f :: k -> *) (a :: k) (g :: k -> *).
Applicative m =>
(f a -> m (g a)) -> Weighted f a -> m (Weighted g a)
traverseWeighted f a -> m (g a)
f (Weighted Maybe Int
w f a
t) = forall {k} (f :: k -> *) (a :: k). Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> m (g a)
f f a
t

-- ==================================================
-- Pred

data Pred where
  ElemPred :: forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
  Monitor :: ((forall a. Term a -> a) -> Property -> Property) -> Pred
  And :: [Pred] -> Pred
  Exists ::
    -- | Constructive recovery function for checking
    -- existential quantification
    ((forall b. Term b -> b) -> GE a) ->
    Binder a ->
    Pred
  Subst :: HasSpec a => Var a -> Term a -> Pred -> Pred
  Let :: Term a -> Binder a -> Pred
  Assert :: Term Bool -> Pred
  Reifies ::
    ( HasSpec a
    , HasSpec b
    ) =>
    -- | This depends on the `a` term
    Term b ->
    Term a ->
    -- | Recover a useable value from the `a` term.
    (a -> b) ->
    Pred
  -- TODO: there is good cause for not limiting this to `Term a` and `Term b`.
  -- However, changing it requires re-working quite a lot of code.
  DependsOn ::
    ( HasSpec a
    , HasSpec b
    ) =>
    Term a ->
    Term b ->
    Pred
  ForAll ::
    ( Forallable t a
    , HasSpec t
    , HasSpec a
    ) =>
    Term t ->
    Binder a ->
    Pred
  Case ::
    HasSpec (SumOver as) =>
    Term (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 Binder) as ->
    Pred
  -- monadic-style `when` - if the first argument is False the second
  -- doesn't apply.
  When ::
    HasSpec Bool =>
    Term Bool ->
    Pred ->
    Pred
  GenHint ::
    HasGenHint a =>
    Hint a ->
    Term a ->
    Pred
  TruePred :: Pred
  FalsePred :: NE.NonEmpty String -> Pred
  Explain :: NE.NonEmpty String -> Pred -> Pred

instance Semigroup Pred where
  FalsePred NonEmpty String
xs <> :: Pred -> Pred -> Pred
<> FalsePred NonEmpty String
ys = NonEmpty String -> Pred
FalsePred (NonEmpty String
xs forall a. Semigroup a => a -> a -> a
<> NonEmpty String
ys)
  FalsePred NonEmpty String
es <> Pred
_ = NonEmpty String -> Pred
FalsePred NonEmpty String
es
  Pred
_ <> FalsePred NonEmpty String
es = NonEmpty String -> Pred
FalsePred NonEmpty String
es
  Pred
TruePred <> Pred
p = Pred
p
  Pred
p <> Pred
TruePred = Pred
p
  Pred
p <> Pred
p' = [Pred] -> Pred
And (Pred -> [Pred]
unpackPred Pred
p forall a. [a] -> [a] -> [a]
++ Pred -> [Pred]
unpackPred Pred
p')
    where
      unpackPred :: Pred -> [Pred]
unpackPred (And [Pred]
ps) = [Pred]
ps
      unpackPred Pred
x = [Pred
x]

instance Monoid Pred where
  mempty :: Pred
mempty = Pred
TruePred

class Forallable t e | t -> e where
  fromForAllSpec ::
    (HasSpec t, HasSpec e) => Specification e -> Specification t
  default fromForAllSpec ::
    ( HasSpec t
    , HasSpec e
    , HasSimpleRep t
    , TypeSpec t ~ TypeSpec (SimpleRep t)
    , Forallable (SimpleRep t) e
    , HasSpec (SimpleRep t)
    ) =>
    Specification e ->
    Specification t
  fromForAllSpec Specification e
es = forall a.
(HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec forall a b. (a -> b) -> a -> b
$ forall t e.
(Forallable t e, HasSpec t, HasSpec e) =>
Specification e -> Specification t
fromForAllSpec @(SimpleRep t) @e Specification e
es

  forAllToList :: t -> [e]
  default forAllToList ::
    ( HasSimpleRep t
    , Forallable (SimpleRep t) e
    ) =>
    t ->
    [e]
  forAllToList t
t = forall t e. Forallable t e => t -> [e]
forAllToList (forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep t
t)

-- | 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

-- ===========================================
-- IsPred

class Show p => IsPred p where
  toPred :: p -> Pred

instance IsPred Pred where
  toPred :: Pred -> Pred
toPred (Assert (Lit Bool
False)) = NonEmpty String -> Pred
FalsePred (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"toPred(Lit False)")
  toPred (Assert (Lit Bool
True)) = Pred
TruePred
  toPred (Explain NonEmpty String
xs Pred
p) = NonEmpty String -> Pred -> Pred
Explain NonEmpty String
xs (forall p. IsPred p => p -> Pred
toPred Pred
p)
  toPred (And [Pred]
ps) = [Pred] -> Pred
And (forall a b. (a -> b) -> [a] -> [b]
map forall p. IsPred p => p -> Pred
toPred [Pred]
ps)
  toPred Pred
x = Pred
x

instance IsPred p => IsPred [p] where
  toPred :: [p] -> Pred
toPred [p]
xs = [Pred] -> Pred
And (forall a b. (a -> b) -> [a] -> [b]
map forall p. IsPred p => p -> Pred
toPred [p]
xs)

instance IsPred Bool where
  toPred :: Bool -> Pred
toPred Bool
True = Pred
TruePred
  toPred Bool
False = NonEmpty String -> Pred
FalsePred (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"toPred False")

instance IsPred (Term Bool) where
  toPred :: Term Bool -> Pred
toPred (Lit Bool
b) = forall p. IsPred p => p -> Pred
toPred Bool
b
  toPred Term Bool
term = Term Bool -> Pred
Assert Term Bool
term

-- ============================================================
-- Simple Widely used operations on Specification

-- | return a MemberSpec or ans ErrorSpec depending on if 'xs' the null list or not
memberSpecList :: [a] -> NE.NonEmpty String -> Specification a
memberSpecList :: forall a. [a] -> NonEmpty String -> Specification a
memberSpecList [a]
xs NonEmpty String
messages =
  case forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [a]
xs of
    Maybe (NonEmpty a)
Nothing -> forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
messages
    Just NonEmpty a
ys -> forall a. NonEmpty a -> Specification a
MemberSpec NonEmpty a
ys

explainSpec :: [String] -> Specification a -> Specification a
explainSpec :: forall a. [String] -> Specification a -> Specification a
explainSpec [] Specification a
x = Specification a
x
explainSpec [String]
es Specification a
spec = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es Specification a
spec

explainSpecOpt :: [String] -> Specification a -> Specification a
explainSpecOpt :: forall a. [String] -> Specification a -> Specification a
explainSpecOpt [] Specification a
x = Specification a
x
explainSpecOpt [String]
es1 (ExplainSpec [String]
es2 Specification a
x) = forall a. [String] -> Specification a -> Specification a
explainSpecOpt ([String]
es1 forall a. [a] -> [a] -> [a]
++ [String]
es2) Specification a
x
explainSpecOpt [String]
es Specification a
spec = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es Specification a
spec

equalSpec :: a -> Specification a
equalSpec :: forall a. a -> Specification a
equalSpec = forall a. NonEmpty a -> Specification a
MemberSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure

notEqualSpec :: forall a. HasSpec a => a -> Specification a
notEqualSpec :: forall a. HasSpec a => a -> Specification a
notEqualSpec = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (forall a. HasSpec a => TypeSpec a
emptySpec @a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure

notMemberSpec :: forall a f. (HasSpec a, Foldable f) => f a -> Specification a
notMemberSpec :: forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
typeSpecOpt (forall a. HasSpec a => TypeSpec a
emptySpec @a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

constrained ::
  forall a p.
  (IsPred p, HasSpec a) =>
  (Term a -> p) ->
  Specification a
constrained :: forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained Term a -> p
body =
  let Var a
x :-> Pred
p = forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term a -> p
body
   in forall a. HasSpec a => Var a -> Pred -> Specification a
SuspendedSpec Var a
x Pred
p

isErrorLike :: forall a. Specification a -> Bool
isErrorLike :: forall a. Specification a -> Bool
isErrorLike (ExplainSpec [String]
_ Specification a
s) = forall a. Specification a -> Bool
isErrorLike Specification a
s
isErrorLike ErrorSpec {} = Bool
True
isErrorLike (TypeSpec TypeSpec a
x [a]
_) =
  case forall a. HasSpec a => TypeSpec a -> Maybe (NonEmpty String)
typeSpecHasError @a TypeSpec a
x of
    Maybe (NonEmpty String)
Nothing -> Bool
False
    Just NonEmpty String
_ -> Bool
True
isErrorLike Specification a
_ = Bool
False

errorLikeMessage :: forall a. Specification a -> NE.NonEmpty String
errorLikeMessage :: forall a. Specification a -> NonEmpty String
errorLikeMessage (ErrorSpec NonEmpty String
es) = NonEmpty String
es
errorLikeMessage (TypeSpec TypeSpec a
x [a]
_) =
  case forall a. HasSpec a => TypeSpec a -> Maybe (NonEmpty String)
typeSpecHasError @a TypeSpec a
x of
    Maybe (NonEmpty String)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Bad call to errorLikeMessage case 1, not guarded by isErrorLike")
    Just NonEmpty String
xs -> NonEmpty String
xs
errorLikeMessage Specification a
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Bad call to errorLikeMessage, case 2, not guarded by isErrorLike")

fromGESpec :: HasCallStack => GE (Specification a) -> Specification a
fromGESpec :: forall a. HasCallStack => GE (Specification a) -> Specification a
fromGESpec GE (Specification a)
ge = case GE (Specification a)
ge of
  Result Specification a
s -> Specification a
s
  GenError NonEmpty (NonEmpty String)
xs -> forall a. NonEmpty String -> Specification a
ErrorSpec (NonEmpty (NonEmpty String) -> NonEmpty String
catMessageList NonEmpty (NonEmpty String)
xs)
  FatalError NonEmpty (NonEmpty String)
es -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ NonEmpty (NonEmpty String) -> String
catMessages NonEmpty (NonEmpty String)
es

-- | Add the explanations, if it's an ErrorSpec, else drop them
addToErrorSpec :: NE.NonEmpty String -> Specification a -> Specification a
addToErrorSpec :: forall a. NonEmpty String -> Specification a -> Specification a
addToErrorSpec NonEmpty String
es (ExplainSpec [] Specification a
x) = forall a. NonEmpty String -> Specification a -> Specification a
addToErrorSpec NonEmpty String
es Specification a
x
addToErrorSpec NonEmpty String
es (ExplainSpec [String]
es2 Specification a
x) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es2 (forall a. NonEmpty String -> Specification a -> Specification a
addToErrorSpec NonEmpty String
es Specification a
x)
addToErrorSpec NonEmpty String
es (ErrorSpec NonEmpty String
es') = forall a. NonEmpty String -> Specification a
ErrorSpec (NonEmpty String
es forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es')
addToErrorSpec NonEmpty String
_ Specification a
s = Specification a
s

-- ===================================================================
-- Pretty Printer Helper functions
-- ===================================================================

data WithPrec a = WithPrec Int a

parensIf :: Bool -> Doc ann -> Doc ann
parensIf :: forall ann. Bool -> Doc ann -> Doc ann
parensIf Bool
True = forall ann. Doc ann -> Doc ann
parens
parensIf Bool
False = forall a. a -> a
id

prettyPrec :: Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec :: forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
p = forall a ann. Pretty a => a -> Doc ann
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> a -> WithPrec a
WithPrec Int
p

ppList ::
  forall f as ann.
  All HasSpec as => -- can we use something other than All HasSpec as here? We know Function Symbol HERE
  (forall a. HasSpec a => f a -> Doc ann) ->
  List f as ->
  [Doc ann]
ppList :: forall (f :: * -> *) (as :: [*]) ann.
All HasSpec as =>
(forall a. HasSpec a => f a -> Doc ann) -> List f as -> [Doc ann]
ppList forall a. HasSpec a => f a -> Doc ann
_ List f as
Nil = []
ppList forall a. HasSpec a => f a -> Doc ann
pp (f a
a :> List f as1
as) = forall a. HasSpec a => f a -> Doc ann
pp f a
a forall a. a -> [a] -> [a]
: forall (f :: * -> *) (as :: [*]) ann.
All HasSpec as =>
(forall a. HasSpec a => f a -> Doc ann) -> List f as -> [Doc ann]
ppList forall a. HasSpec a => f a -> Doc ann
pp List f as1
as

ppList_ :: forall f as ann. (forall a. f a -> Doc ann) -> List f as -> [Doc ann]
ppList_ :: forall {k} (f :: k -> *) (as :: [k]) ann.
(forall (a :: k). f a -> Doc ann) -> List f as -> [Doc ann]
ppList_ forall (a :: k). f a -> Doc ann
_ List f as
Nil = []
ppList_ forall (a :: k). f a -> Doc ann
pp (f a
a :> List f as1
as) = forall (a :: k). f a -> Doc ann
pp f a
a forall a. a -> [a] -> [a]
: forall {k} (f :: k -> *) (as :: [k]) ann.
(forall (a :: k). f a -> Doc ann) -> List f as -> [Doc ann]
ppList_ forall (a :: k). f a -> Doc ann
pp List f as1
as

prettyType :: forall t x. Typeable t => Doc x
prettyType :: forall {k} (t :: k) x. Typeable t => Doc x
prettyType = forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t))

vsep' :: [Doc ann] -> Doc ann
vsep' :: forall ann. [Doc ann] -> Doc ann
vsep' = forall ann. Doc ann -> Doc ann
align forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate forall ann. Doc ann
hardline

(/>) :: Doc ann -> Doc ann -> Doc ann
Doc ann
h /> :: forall ann. Doc ann -> Doc ann -> Doc ann
/> Doc ann
cont = forall ann. Int -> Doc ann -> Doc ann
hang Int
2 forall a b. (a -> b) -> a -> b
$ forall ann. [Doc ann] -> Doc ann
sep [Doc ann
h, forall ann. Doc ann -> Doc ann
align Doc ann
cont]

infixl 5 />

short :: forall a x. (Show a, Typeable a) => [a] -> Doc x
short :: forall a x. (Show a, Typeable a) => [a] -> Doc x
short [] = Doc x
"[]"
short [a
x] =
  let raw :: String
raw = forall a. Show a => a -> String
show a
x
      refined :: String
refined = if forall (t :: * -> *) a. Foldable t => t a -> Int
length String
raw forall a. Ord a => a -> a -> Bool
<= Int
20 then String
raw else forall a. Int -> [a] -> [a]
take Int
20 String
raw forall a. [a] -> [a] -> [a]
++ String
" ... "
   in Doc x
"[" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a. IsString a => String -> a
fromString String
refined forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc x
"]"
short [a]
xs =
  let raw :: String
raw = forall a. Show a => a -> String
show [a]
xs
   in if forall (t :: * -> *) a. Foldable t => t a -> Int
length String
raw forall a. Ord a => a -> a -> Bool
<= Int
50
        then forall a. IsString a => String -> a
fromString String
raw
        else Doc x
"([" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc x
"elements ...] @" forall a. Semigroup a => a -> a -> a
<> forall {k} (t :: k) x. Typeable t => Doc x
prettyType @a forall a. Semigroup a => a -> a -> a
<> Doc x
")"

showType :: forall t. Typeable t => String
showType :: forall {k} (t :: k). Typeable t => String
showType = forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t))

-- Seems to cause GHC 8.107 to fail because it doesn't know about SSymbol
-- ppSymbol :: KnownSymbol a => (SSymbol a) -> Doc ann
-- ppSymbol (_ :: SSymbol z) = fromString (symbolVal (Proxy @z))

instance forall (c :: Constraint). Typeable c => Show (Evidence c) where
  show :: Evidence c -> String
show Evidence c
_ = String
"Evidence@(" forall a. [a] -> [a] -> [a]
++ forall {k} (t :: k). Typeable t => String
showType @c forall a. [a] -> [a] -> [a]
++ String
")"

-- ==========================================================================
-- Pretty and Show instances
-- ==========================================================================

-- ------------ Term -----------------
instance Show a => Pretty (WithPrec (Term a)) where
  pretty :: forall ann. WithPrec (Term a) -> Doc ann
pretty (WithPrec Int
p Term a
t) = case Term a
t of
    Lit a
n -> forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
n String
""
    V Var a
x -> forall a ann. Show a => a -> Doc ann
viaShow Var a
x
    App t dom a
x List Term dom
Nil -> forall a ann. Show a => a -> Doc ann
viaShow t dom a
x
    App t dom a
f List Term dom
as
      | Just Doc ann
doc <- forall (t :: [*] -> * -> *) (dom :: [*]) rng ann.
(Syntax t, All HasSpec dom, HasSpec rng) =>
t dom rng -> List Term dom -> Int -> Maybe (Doc ann)
prettyWit t dom a
f List Term dom
as Int
p -> Doc ann
doc -- Use Function Symbol specific pretty printers
    App t dom a
f List Term dom
as
      | forall (t :: [*] -> * -> *) (dom :: [*]) rng.
Syntax t =>
t dom rng -> Bool
inFix t dom a
f
      , Term a
a :> Term a
b :> List Term as1
Nil <- List Term dom
as ->
          forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
a forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow t dom a
f forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
b
      | Bool
otherwise -> forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ forall a ann. Show a => a -> Doc ann
viaShow t dom a
f forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall ann. [Doc ann] -> Doc ann
fillSep (forall (f :: * -> *) (as :: [*]) ann.
All HasSpec as =>
(forall a. HasSpec a => f a -> Doc ann) -> List f as -> [Doc ann]
ppList (forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
11) List Term dom
as))

instance Show a => Pretty (Term a) where
  pretty :: forall ann. Term a -> Doc ann
pretty = forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
0

instance Show a => Show (Term a) where
  showsPrec :: Int -> Term a -> ShowS
showsPrec Int
p Term a
t = forall a. Show a => a -> ShowS
shows forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Int -> a -> WithPrec a
WithPrec Int
p Term a
t)

-- ------------ Pred -----------------

instance Pretty Pred where
  pretty :: forall ann. Pred -> Doc ann
pretty = \case
    ElemPred Bool
True Term a
term NonEmpty a
vs ->
      forall ann. Doc ann -> Doc ann
align forall a b. (a -> b) -> a -> b
$
        forall ann. [Doc ann] -> Doc ann
sep
          [ Doc ann
"memberPred"
          , forall a ann. Pretty a => a -> Doc ann
pretty Term a
term
          , Doc ann
"(" forall a. Semigroup a => a -> a -> a
<> forall a ann. Show a => a -> Doc ann
viaShow (forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty a
vs) forall a. Semigroup a => a -> a -> a
<> Doc ann
" items)"
          , forall ann. Doc ann -> Doc ann
brackets (forall ann. [Doc ann] -> Doc ann
fillSep (forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Show a => a -> Doc ann
viaShow (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
vs))))
          ]
    ElemPred Bool
False Term a
term NonEmpty a
vs -> forall ann. Doc ann -> Doc ann
align forall a b. (a -> b) -> a -> b
$ forall ann. [Doc ann] -> Doc ann
sep [Doc ann
"notMemberPred", forall a ann. Pretty a => a -> Doc ann
pretty Term a
term, forall ann. [Doc ann] -> Doc ann
fillSep (forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Show a => a -> Doc ann
viaShow (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
vs)))]
    Exists (forall b. Term b -> b) -> GE a
_ (Var a
x :-> Pred
p) -> forall ann. Doc ann -> Doc ann
align forall a b. (a -> b) -> a -> b
$ forall ann. [Doc ann] -> Doc ann
sep [Doc ann
"exists" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Var a
x forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"in", forall a ann. Pretty a => a -> Doc ann
pretty Pred
p]
    Let Term a
t (Var a
x :-> Pred
p) -> forall ann. Doc ann -> Doc ann
align forall a b. (a -> b) -> a -> b
$ forall ann. [Doc ann] -> Doc ann
sep [Doc ann
"let" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Var a
x forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Term a
t forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"in", forall a ann. Pretty a => a -> Doc ann
pretty Pred
p]
    And [Pred]
ps -> forall ann. Doc ann -> Doc ann
braces forall a b. (a -> b) -> a -> b
$ forall ann. [Doc ann] -> Doc ann
vsep' forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Pred]
ps
    Assert Term Bool
t -> Doc ann
"assert $" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Term Bool
t
    Reifies Term b
t' Term a
t a -> b
_ -> Doc ann
"reifies" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Int -> a -> WithPrec a
WithPrec Int
11 Term b
t') forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Int -> a -> WithPrec a
WithPrec Int
11 Term a
t)
    DependsOn Term a
a Term b
b -> forall a ann. Pretty a => a -> Doc ann
pretty Term a
a forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"<-" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Term b
b
    ForAll Term t
t (Var a
x :-> Pred
p) -> Doc ann
"forall" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Var a
x forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"in" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Term t
t forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"$" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Pred
p
    Case Term (SumOver as)
t List (Weighted Binder) as
bs -> Doc ann
"case" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Term (SumOver as)
t forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"of" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep' (forall {k} (f :: k -> *) (as :: [k]) ann.
(forall (a :: k). f a -> Doc ann) -> List f as -> [Doc ann]
ppList_ forall a ann. Pretty a => a -> Doc ann
pretty List (Weighted Binder) as
bs)
    When Term Bool
b Pred
p -> Doc ann
"whenTrue" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Int -> a -> WithPrec a
WithPrec Int
11 Term Bool
b) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"$" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Pred
p
    Subst Var a
x Term a
t Pred
p -> Doc ann
"[" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Term a
t forall a. Semigroup a => a -> a -> a
<> Doc ann
"/" forall a. Semigroup a => a -> a -> a
<> forall a ann. Show a => a -> Doc ann
viaShow Var a
x forall a. Semigroup a => a -> a -> a
<> Doc ann
"]" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Pred
p
    GenHint Hint a
h Term a
t -> Doc ann
"genHint" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a. IsString a => String -> a
fromString (forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Hint a
h String
"") forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"$" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Term a
t
    Pred
TruePred -> Doc ann
"True"
    FalsePred {} -> Doc ann
"False"
    Monitor {} -> Doc ann
"monitor"
    Explain NonEmpty String
es Pred
p -> Doc ann
"Explain" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow (forall a. NonEmpty a -> [a]
NE.toList NonEmpty String
es) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"$" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Pred
p

instance Show Pred where
  show :: Pred -> String
show = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
pretty

-- TODO: make nicer
instance Pretty (f a) => Pretty (Weighted f a) where
  pretty :: forall ann. Weighted f a -> Doc ann
pretty (Weighted Maybe Int
Nothing f a
t) = forall a ann. Pretty a => a -> Doc ann
pretty f a
t
  pretty (Weighted (Just Int
w) f a
t) = forall a ann. Show a => a -> Doc ann
viaShow Int
w forall a. Semigroup a => a -> a -> a
<> Doc ann
"~" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty f a
t

instance Pretty (Binder a) where
  pretty :: forall ann. Binder a -> Doc ann
pretty (Var a
x :-> Pred
p) = forall a ann. Show a => a -> Doc ann
viaShow Var a
x forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"->" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Pred
p

-- ------------ Specifications -----------------

instance HasSpec a => Pretty (WithPrec (Specification a)) where
  pretty :: forall ann. WithPrec (Specification a) -> Doc ann
pretty (WithPrec Int
d Specification a
s) = case Specification a
s of
    ExplainSpec [String]
es Specification a
z -> Doc ann
"ExplainSpec" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow [String]
es forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"$" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Specification a
z
    ErrorSpec NonEmpty String
es -> Doc ann
"ErrorSpec" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep' (forall a b. (a -> b) -> [a] -> [b]
map forall a. IsString a => String -> a
fromString (forall a. NonEmpty a -> [a]
NE.toList NonEmpty String
es))
    Specification a
TrueSpec -> forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ String
"TrueSpec @(" forall a. [a] -> [a] -> [a]
++ forall {k} (t :: k). Typeable t => String
showType @a forall a. [a] -> [a] -> [a]
++ String
")"
    MemberSpec NonEmpty a
xs -> Doc ann
"MemberSpec" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
xs)
    SuspendedSpec Var a
x Pred
p -> forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"constrained $ \\" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Var a
x forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"->" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Pred
p
    -- TODO: require pretty for `TypeSpec` to make this much nicer
    TypeSpec TypeSpec a
ts [a]
cant ->
      forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
        Doc ann
"TypeSpec"
          forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep
            [ forall a. IsString a => String -> a
fromString (forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 TypeSpec a
ts String
"")
            , forall a ann. Show a => a -> Doc ann
viaShow [a]
cant
            ]

instance HasSpec a => Pretty (Specification a) where
  pretty :: forall ann. Specification a -> Doc ann
pretty = forall a ann. Pretty a => a -> Doc ann
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> a -> WithPrec a
WithPrec Int
0

instance HasSpec a => Show (Specification a) where
  showsPrec :: Int -> Specification a -> ShowS
showsPrec Int
d = forall a. Show a => a -> ShowS
shows forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> a -> WithPrec a
WithPrec Int
d

-- ====================================================
-- The Fun type encapuslates a Logic instance 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

instance Show (Fun dom r) where
  show :: Fun dom r -> String
show (Fun (t dom r
f :: t dom rng)) = String
"(Fun " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t dom r
f forall a. [a] -> [a] -> [a]
++ String
")"

extractf :: forall t d r. LogicRequires t => Fun d r -> Maybe (t d r)
extractf :: forall (t :: [*] -> * -> *) (d :: [*]) r.
LogicRequires t =>
Fun d r -> Maybe (t d r)
extractf (Fun (t d r
x :: t1 d1 r1)) =
  case (forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @t @t1, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @d @d1, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @r @r1) of
    (Just t :~: t
Refl, Just d :~: d
Refl, Just r :~: r
Refl) -> forall a. a -> Maybe a
Just t d r
x
    (Maybe (t :~: t), Maybe (d :~: d), Maybe (r :~: r))
_ -> forall a. Maybe a
Nothing

appFun :: Fun '[x] b -> Term x -> Term b
appFun :: forall x b. Fun '[x] b -> Term x -> Term b
appFun (Fun t '[x] b
f) Term x
x = forall (a :: [*] -> * -> *) (as :: [*]) rng.
AppRequires a as rng =>
a as rng -> List Term as -> Term rng
App t '[x] b
f (Term x
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)

sameFun :: Fun d1 r1 -> Fun d2 r2 -> Bool
sameFun :: forall (d1 :: [*]) r1 (d2 :: [*]) r2.
Fun d1 r1 -> Fun d2 r2 -> Bool
sameFun (Fun t d1 r1
f) (Fun t d2 r2
g) =
  case forall (t1 :: [*] -> * -> *) (d1 :: [*]) r1 (t2 :: [*] -> * -> *)
       (d2 :: [*]) r2.
(AppRequires t1 d1 r1, AppRequires t2 d2 r2) =>
t1 d1 r1
-> t2 d2 r2 -> Maybe (t1 d1 r1, t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym t d1 r1
f t d2 r2
g of
    Just (t d1 r1
_f, t :~: t
Refl, d1 :~: d2
Refl, r1 :~: r2
Refl) -> Bool
True
    Maybe (t d1 r1, t :~: t, d1 :~: d2, r1 :~: r2)
Nothing -> Bool
False

instance Eq (Fun d r) where
  == :: Fun d r -> Fun d r -> Bool
(==) = forall (d1 :: [*]) r1 (d2 :: [*]) r2.
Fun d1 r1 -> Fun d2 r2 -> Bool
sameFun

-- =================================================================
-- A simple but important HasSpec instances. The  other
-- instances usually come in a file of their own.

instance HasSimpleRep () where
  type SimpleRep () = ()
  toSimpleRep :: () -> SimpleRep ()
toSimpleRep ()
x = ()
x
  fromSimpleRep :: SimpleRep () -> ()
fromSimpleRep SimpleRep ()
x = SimpleRep ()
x

instance HasSpec () where
  type TypeSpec () = ()
  emptySpec :: TypeSpec ()
emptySpec = ()
  combineSpec :: TypeSpec () -> TypeSpec () -> Specification ()
combineSpec TypeSpec ()
_ TypeSpec ()
_ = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec ()
  ()
_ conformsTo :: HasCallStack => () -> TypeSpec () -> Bool
`conformsTo` TypeSpec ()
_ = Bool
True
  shrinkWithTypeSpec :: TypeSpec () -> () -> [()]
shrinkWithTypeSpec TypeSpec ()
_ ()
_ = []
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec () -> GenT m ()
genFromTypeSpec TypeSpec ()
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  toPreds :: Term () -> TypeSpec () -> Pred
toPreds Term ()
_ TypeSpec ()
_ = Pred
TruePred
  cardinalTypeSpec :: TypeSpec () -> Specification Integer
cardinalTypeSpec TypeSpec ()
_ = forall a. NonEmpty a -> Specification a
MemberSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
1)
  cardinalTrueSpec :: Specification Integer
cardinalTrueSpec = forall a. a -> Specification a
equalSpec Integer
1 -- there is exactly one, ()
  typeSpecOpt :: TypeSpec () -> [()] -> Specification ()
typeSpecOpt TypeSpec ()
_ [] = forall a. Specification a
TrueSpec
  typeSpecOpt TypeSpec ()
_ (()
_ : [()]
_) = forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Non null 'cant' set in typeSpecOpt @()")

-- ========================================================================
-- Uni-directional, Match only patterns, for the Function Symbols in BaseW.
-- We do not defined Constructor patterns. Use the xxx_ functions instead.

pattern FromGeneric ::
  forall rng.
  () =>
  forall a.
  (rng ~ a, GenericRequires a, HasSpec a, AppRequires BaseW '[SimpleRep a] rng) =>
  Term (SimpleRep a) ->
  Term rng
pattern $mFromGeneric :: forall {r} {rng}.
Term rng
-> (forall {a}.
    (rng ~ a, GenericRequires a, HasSpec a,
     AppRequires BaseW '[SimpleRep a] rng) =>
    Term (SimpleRep a) -> r)
-> ((# #) -> r)
-> r
FromGeneric x <-
  (App (getWitness -> Just FromGenericW) (x :> Nil))

pattern ToGeneric ::
  forall rng.
  () =>
  forall a.
  (rng ~ SimpleRep a, GenericRequires a, HasSpec a, AppRequires BaseW '[a] rng) =>
  Term a ->
  Term rng
pattern $mToGeneric :: forall {r} {rng}.
Term rng
-> (forall {a}.
    (rng ~ SimpleRep a, GenericRequires a, HasSpec a,
     AppRequires BaseW '[a] rng) =>
    Term a -> r)
-> ((# #) -> r)
-> r
ToGeneric x <- (App (getWitness -> Just ToGenericW) (x :> Nil))