{-# 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 #-}

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

import Constrained.Core (Evidence (..), Var (..))
import Constrained.GenT (
  GE (..),
  GenT,
  MonadGenError (..),
  catMessageList,
  catMessages,
 )
import Constrained.List
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 (Proxy (..), Typeable, eqT, typeRep, (:~:) (Refl))
import GHC.Stack
import GHC.TypeLits hiding (Text)
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.

-- The kind of a type, that is a candidate for a Function Symbol, and hence
-- instances of Syntax, Semantics, and Logic
type FSType = Symbol -> [Type] -> Type -> Type

-- | Syntactic operations are ones that have to do with the structure and appearence of the type.
class Syntax (t :: FSType) where
  isInFix :: forall s dom rng. t s dom rng -> Bool
  isInFix t s dom rng
_ = Bool
False
  prettyWit ::
    forall s dom rng ann.
    (All HasSpec dom, HasSpec rng) => t s dom rng -> List Term dom -> Int -> Maybe (Doc ann)
  prettyWit t s 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 :: Symbol -> [Type] -> Type -> Type) where
  semantics :: forall s d r. t s d r -> FunTy d r -- e.g. FunTy '[a,Int] Bool == a -> Int -> Bool

-- What properties we need to have Logical operations.
type LogicRequires s (t :: FSType) dom rng =
  ( Typeable t
  , Typeable s
  , TypeList dom
  , Typeable dom
  , Typeable rng
  , Syntax t
  , Semantics t
  , Eq (t s dom rng)
  , Show (t s dom rng)
  )

-- | Logical operations are one that support reasoning about how a function symbol
--   relates to logical properties, that we call Specification's
class LogicRequires s t dom rng => Logic s t dom rng | s -> t where
  {-# MINIMAL (propagate) #-}

  -- info :: String -- For documentation about what constructor of 't' implements 's'
  info :: t s dom rng -> String
  info t s dom rng
x = forall a. Show a => a -> String
show t s dom rng
x forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall {k} (t :: k). Typeable t => String
showType @s

  propagate :: Context s t dom rng hole -> Specification rng -> Specification hole

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

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

  saturate :: t s dom Bool -> List Term dom -> [Pred]
  saturate t s 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 f over them one at a time. Note 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
HOLE -> Specification a
spec
  Ctx (Context t s dom a
f (a
x :|> Ctx v y
newctx :<> a
y :<| CList 'Post as Any Any
End)) ->
    forall v a.
HasSpec v =>
Specification a -> Ctx v a -> Specification v
propagateSpec (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole a.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole a -> Context s t dom rng hole
Context t s dom a
f (a
x forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> forall a. HasSpec a => Ctx a a
HOLE forall y x (a :: [*]).
HasSpec y =>
Ctx x y
-> (forall i j. CList 'Post a i j) -> CList 'Pre (y : a) x y
:<> a
y forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Post b h y -> CList 'Post (a : b) h y
:<| forall h y. CList 'Post '[] h y
End)) Specification a
spec) Ctx v y
newctx
  Ctx (Context t s dom a
f CList 'Pre dom v y
clist) -> case CList 'Pre dom v y
clist of
    (Ctx v y
ctx :<> forall i j. CList 'Post as i j
more) -> forall v a.
HasSpec v =>
Specification a -> Ctx v a -> Specification v
propagateSpec (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole a.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole a -> Context s t dom rng hole
Context t s dom a
f (forall a. HasSpec a => Ctx a a
HOLE forall y x (a :: [*]).
HasSpec y =>
Ctx x y
-> (forall i j. CList 'Post a i j) -> CList 'Pre (y : a) x y
:<> forall i j. CList 'Post as i j
more)) Specification a
spec) Ctx v y
ctx
    (a
a :|> Ctx v y
ctx :<> forall i j. CList 'Post as i j
more) -> forall v a.
HasSpec v =>
Specification a -> Ctx v a -> Specification v
propagateSpec (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole a.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole a -> Context s t dom rng hole
Context t s dom a
f (a
a forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> forall a. HasSpec a => Ctx a a
HOLE forall y x (a :: [*]).
HasSpec y =>
Ctx x y
-> (forall i j. CList 'Post a i j) -> CList 'Pre (y : a) x y
:<> forall i j. CList 'Post as i j
more)) Specification a
spec) Ctx v y
ctx
    (a
a :|> a
b :|> Ctx v y
ctx :<> forall i j. CList 'Post as i j
more) ->
      forall v a.
HasSpec v =>
Specification a -> Ctx v a -> Specification v
propagateSpec (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole a.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole a -> Context s t dom rng hole
Context t s dom a
f (a
a forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> a
b forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> forall a. HasSpec a => Ctx a a
HOLE forall y x (a :: [*]).
HasSpec y =>
Ctx x y
-> (forall i j. CList 'Post a i j) -> CList 'Pre (y : a) x y
:<> forall i j. CList 'Post as i j
more)) Specification a
spec) Ctx v y
ctx
    (a
a :|> a
b :|> a
c :|> Ctx v y
ctx :<> forall i j. CList 'Post as i j
more) ->
      forall v a.
HasSpec v =>
Specification a -> Ctx v a -> Specification v
propagateSpec (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole a.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole a -> Context s t dom rng hole
Context t s dom a
f (a
a forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> a
b forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> a
c forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> forall a. HasSpec a => Ctx a a
HOLE forall y x (a :: [*]).
HasSpec y =>
Ctx x y
-> (forall i j. CList 'Post a i j) -> CList 'Pre (y : a) x y
:<> forall i j. CList 'Post as i j
more)) Specification a
spec) Ctx v y
ctx
    (a
a :|> a
b :|> a
c :|> a
d :|> Ctx v y
ctx :<> forall i j. CList 'Post as i j
more) ->
      forall v a.
HasSpec v =>
Specification a -> Ctx v a -> Specification v
propagateSpec (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole a.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole a -> Context s t dom rng hole
Context t s dom a
f (a
a forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> a
b forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> a
c forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> a
d forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> forall a. HasSpec a => Ctx a a
HOLE forall y x (a :: [*]).
HasSpec y =>
Ctx x y
-> (forall i j. CList 'Post a i j) -> CList 'Pre (y : a) x y
:<> forall i j. CList 'Post as i j
more)) Specification a
spec) Ctx v y
ctx
    CList 'Pre dom v y
_ -> forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"function with more than 5 arguments in propagateSpec: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t s dom a
f)

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

sameFunSym ::
  forall s1 (t1 :: FSType) d1 r1 s2 (t2 :: FSType) d2 r2.
  (Logic s1 t1 d1 r1, Logic s2 t2 d2 r2) =>
  t1 s1 d1 r1 ->
  t2 s2 d2 r2 ->
  Maybe (t1 s1 d1 r1, s1 :~: s2, t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym :: forall (s1 :: Symbol) (t1 :: Symbol -> [*] -> * -> *) (d1 :: [*])
       r1 (s2 :: Symbol) (t2 :: Symbol -> [*] -> * -> *) (d2 :: [*]) r2.
(Logic s1 t1 d1 r1, Logic s2 t2 d2 r2) =>
t1 s1 d1 r1
-> t2 s2 d2 r2
-> Maybe (t1 s1 d1 r1, s1 :~: s2, t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym t1 s1 d1 r1
x t2 s2 d2 r2
y = do
  s :: s1 :~: s2
s@s1 :~: s2
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @s1 @s2
  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 s1 d1 r1
x forall a. Eq a => a -> a -> Bool
== t2 s2 d2 r2
y
    then forall a. a -> Maybe a
Just (t1 s1 d1 r1
x, s1 :~: s2
s, 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.
sameWitness ::
  forall t s d r t' s' d' r'.
  (KnownSymbol s', Typeable t', Logic s t d r) =>
  (t' :: FSType) s' d' r' -> t s d r -> Maybe (t' s' d r, t :~: t', s :~: s')
sameWitness :: forall (t :: Symbol -> [*] -> * -> *) (s :: Symbol) (d :: [*]) r
       (t' :: Symbol -> [*] -> * -> *) (s' :: Symbol) (d' :: [*]) r'.
(KnownSymbol s', Typeable t', Logic s t d r) =>
t' s' d' r' -> t s d r -> Maybe (t' s' d r, t :~: t', s :~: s')
sameWitness t' s' d' r'
_x t s d r
y = case (forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @t' @t, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @s' @s) of
  (Just m :: t' :~: t
m@t' :~: t
Refl, Just n :: s' :~: s
n@s' :~: s
Refl) -> forall a. a -> Maybe a
Just (t s d r
y, t' :~: t
m, s' :~: s
n)
  (Maybe (t' :~: t), Maybe (s' :~: s))
_ -> forall a. Maybe a
Nothing

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

class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec 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 ::
    (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) => TypeSpec a
  emptySpec = forall a. HasSpec a => TypeSpec a
emptySpec @(SimpleRep a)

  default combineSpec ::
    ( HasSimpleRep a
    , HasSpec (SimpleRep a)
    , TypeSpec a ~ TypeSpec (SimpleRep 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 ::
    ( HasSimpleRep a
    , HasSpec (SimpleRep a)
    , TypeSpec a ~ TypeSpec (SimpleRep 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 ::
    ( HasSimpleRep a
    , HasSpec (SimpleRep a)
    , TypeSpec a ~ TypeSpec (SimpleRep 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 ::
    ( HasSpec (SimpleRep a)
    , TypeSpec a ~ TypeSpec (SimpleRep a)
    , HasSimpleRep 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 ::
    ( HasSpec (SimpleRep a)
    , TypeSpec a ~ TypeSpec (SimpleRep a)
    , HasSimpleRep 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 ::
    (HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep 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 (sym :: Symbol) (dom :: [Type]) (rng :: Type) where
  InjLeftW :: forall a b. BaseW "leftFn" '[a] (Sum a b)
  InjRightW :: forall a b. BaseW "rightFn" '[b] (Sum a b)
  ProdW :: forall a b. BaseW "prod_" '[a, b] (Prod a b)
  ProdFstW :: forall a b. BaseW "prodFst_" '[Prod a b] a
  ProdSndW :: forall a b. BaseW "prodSnd_" '[Prod a b] b
  EqualW :: forall a. Eq a => BaseW "==." '[a, a] Bool
  ToGenericW ::
    GenericRequires a => BaseW "toGenericFn" '[a] (SimpleRep a)
  FromGenericW ::
    GenericRequires a => BaseW "fromGenericFn" '[SimpleRep a] a
  ElemW :: forall a. Eq a => BaseW "elem_" '[a, [a]] Bool

deriving instance Eq (BaseW s dom rng)

instance Show (BaseW s d r) where
  show :: BaseW s d r -> String
show BaseW s d r
ToGenericW = String
"toSimpleRep"
  show BaseW s d r
FromGenericW = String
"fromSimpleRep"
  show BaseW s d r
InjLeftW = String
"leftFn"
  show BaseW s d r
InjRightW = String
"rightFn"
  show BaseW s d r
ProdW = String
"prod_"
  show BaseW s d r
ProdFstW = String
"prodFst_"
  show BaseW s d r
ProdSndW = String
"prodSnd_"
  show BaseW s d r
EqualW = String
"==."
  show BaseW s d r
ElemW = String
"elem_"

instance Syntax BaseW where
  isInFix :: forall (s :: Symbol) (dom :: [*]) rng. BaseW s dom rng -> Bool
isInFix BaseW s dom rng
EqualW = Bool
True
  isInFix BaseW s dom rng
_ = Bool
False
  prettyWit :: forall (s :: Symbol) (dom :: [*]) rng ann.
(All HasSpec dom, HasSpec rng) =>
BaseW s dom rng -> List Term dom -> Int -> Maybe (Doc ann)
prettyWit BaseW s dom rng
ElemW (Term a
y :> Lit a
n :> List Term as1
Nil) Int
prec = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
prec forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"elem_" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
y forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short a
n
  prettyWit BaseW s 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 s 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)
  prettyWit BaseW s dom rng
_ List Term dom
_ Int
_ = forall a. Maybe a
Nothing

instance Semantics BaseW where
  semantics :: forall (s :: Symbol) (d :: [*]) r. BaseW s d r -> FunTy d r
semantics BaseW s d r
FromGenericW = forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep
  semantics BaseW s d r
ToGenericW = forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep
  semantics BaseW s d r
InjLeftW = forall a b. a -> Sum a b
SumLeft
  semantics BaseW s d r
InjRightW = forall a b. b -> Sum a b
SumRight
  semantics BaseW s d r
ProdW = forall a b. a -> b -> Prod a b
Prod
  semantics BaseW s d r
ProdFstW = forall a b. Prod a b -> a
prodFst
  semantics BaseW s d r
ProdSndW = forall a b. Prod a b -> b
prodSnd
  semantics BaseW s d r
EqualW = forall a. Eq a => a -> a -> Bool
(==)
  semantics BaseW s d r
ElemW = forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem

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

instance
  (GenericRequires a, simplerepA ~ SimpleRep a) =>
  Logic
    "toGenericFn"
    BaseW
    '[a]
    simplerepA
  where
  propagate :: forall hole.
Context "toGenericFn" BaseW '[a] simplerepA hole
-> Specification simplerepA -> Specification hole
propagate Context "toGenericFn" BaseW '[a] simplerepA hole
ctxt (ExplainSpec [] Specification simplerepA
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "toGenericFn" BaseW '[a] simplerepA hole
ctxt Specification simplerepA
s
  propagate Context "toGenericFn" BaseW '[a] simplerepA hole
ctxt (ExplainSpec [String]
es Specification simplerepA
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "toGenericFn" BaseW '[a] simplerepA hole
ctxt Specification simplerepA
s
  propagate Context "toGenericFn" BaseW '[a] simplerepA hole
_ Specification simplerepA
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "toGenericFn" BaseW '[a] simplerepA hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context BaseW "toGenericFn" '[a] simplerepA
ToGenericW (Ctx hole y
HOLE :<> CList 'Post as Any Any
forall i j. CList 'Post as i j
End)) (SuspendedSpec Var simplerepA
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (a :: Symbol) (b :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
AppRequires a b dom rng =>
b a dom rng -> List Term dom -> Term rng
App forall a.
GenericRequires a =>
BaseW "toGenericFn" '[a] (SimpleRep a)
ToGenericW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var simplerepA
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context BaseW "toGenericFn" '[a] simplerepA
ToGenericW (Ctx hole y
HOLE :<> CList 'Post as Any Any
forall i j. CList 'Post as i j
End)) (TypeSpec TypeSpec simplerepA
s [simplerepA]
cant) = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec simplerepA
s (forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [simplerepA]
cant)
  propagate (Context BaseW "toGenericFn" '[a] simplerepA
ToGenericW (Ctx hole y
HOLE :<> CList 'Post as Any Any
forall i j. CList 'Post as i j
End)) (MemberSpec NonEmpty simplerepA
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 simplerepA
es)
  propagate Context "toGenericFn" BaseW '[a] simplerepA hole
ctx Specification simplerepA
_ =
    forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for ToGenericFn with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "toGenericFn" BaseW '[a] simplerepA hole
ctx)

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

  rewriteRules :: (TypeList '[a], Typeable '[a], HasSpec simplerepA,
 All HasSpec '[a]) =>
BaseW "toGenericFn" '[a] simplerepA
-> List Term '[a]
-> Evidence (AppRequires "toGenericFn" BaseW '[a] simplerepA)
-> Maybe (Term simplerepA)
rewriteRules BaseW "toGenericFn" '[a] simplerepA
ToGenericW ((App (t sym dom a
_fromgeneric :: t s d r) (Term a
x :> List Term as1
Nil)) :> List Term as1
Nil) Evidence (AppRequires "toGenericFn" BaseW '[a] simplerepA)
Evidence =
    case (forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @t @BaseW, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @s @"fromGenericFn", forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @d @'[SimpleRep a], forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @r @a) of
      (Just t :~: BaseW
Refl, Just sym :~: "fromGenericFn"
Refl, Just '[a] :~: '[simplerepA]
Refl, Just a :~: a
Refl) -> forall a. a -> Maybe a
Just Term a
x
      (Maybe (t :~: BaseW), Maybe (sym :~: "fromGenericFn"),
 Maybe ('[a] :~: '[simplerepA]), Maybe (a :~: a))
_ -> forall a. Maybe a
Nothing
  rewriteRules BaseW "toGenericFn" '[a] simplerepA
_ List Term '[a]
_ Evidence (AppRequires "toGenericFn" BaseW '[a] simplerepA)
_ = 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 (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a.
GenericRequires a =>
BaseW "toGenericFn" '[a] (SimpleRep a)
ToGenericW

-- ============== FromGenericW Logic instance

instance (GenericRequires a, dom ~ SimpleRep a) => Logic "fromGenericFn" BaseW '[dom] a where
  propagate :: forall hole.
Context "fromGenericFn" BaseW '[dom] a hole
-> Specification a -> Specification hole
propagate Context "fromGenericFn" BaseW '[dom] a hole
ctxt (ExplainSpec [] Specification a
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "fromGenericFn" BaseW '[dom] a hole
ctxt Specification a
s
  propagate Context "fromGenericFn" BaseW '[dom] a hole
ctxt (ExplainSpec [String]
es Specification a
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "fromGenericFn" BaseW '[dom] a hole
ctxt Specification a
s
  propagate Context "fromGenericFn" BaseW '[dom] a hole
_ Specification a
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "fromGenericFn" BaseW '[dom] a hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context BaseW "fromGenericFn" '[dom] a
FromGenericW (Ctx hole y
HOLE :<> CList 'Post as Any Any
forall i j. CList 'Post as i j
End)) (SuspendedSpec Var a
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (a :: Symbol) (b :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
AppRequires a b dom rng =>
b a dom rng -> List Term dom -> Term rng
App forall a.
GenericRequires a =>
BaseW "fromGenericFn" '[SimpleRep a] a
FromGenericW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var a
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context BaseW "fromGenericFn" '[dom] a
FromGenericW (Ctx hole y
HOLE :<> CList 'Post as Any Any
forall i j. CList 'Post as i j
End)) (TypeSpec TypeSpec a
s [a]
cant) = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec a
s (forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
cant)
  propagate (Context BaseW "fromGenericFn" '[dom] a
FromGenericW (Ctx hole y
HOLE :<> CList 'Post as Any Any
forall i j. CList 'Post as i j
End)) (MemberSpec NonEmpty a
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 a
es)
  propagate Context "fromGenericFn" BaseW '[dom] a hole
ctx Specification a
_ =
    forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for FromGenericFn with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "fromGenericFn" BaseW '[dom] a hole
ctx)

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

  rewriteRules :: (TypeList '[dom], Typeable '[dom], HasSpec a,
 All HasSpec '[dom]) =>
BaseW "fromGenericFn" '[dom] a
-> List Term '[dom]
-> Evidence (AppRequires "fromGenericFn" BaseW '[dom] a)
-> Maybe (Term a)
rewriteRules BaseW "fromGenericFn" '[dom] a
FromGenericW ((App (t sym dom a
_togeneric :: t s d r) (Term a
x :> List Term as1
Nil)) :> List Term as1
Nil) Evidence (AppRequires "fromGenericFn" BaseW '[dom] a)
Evidence =
    case (forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @t @BaseW, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @s @"toGenericFn", forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @d @'[a], forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @r @(SimpleRep a)) of
      (Just t :~: BaseW
Refl, Just sym :~: "toGenericFn"
Refl, Just dom :~: '[a]
Refl, Just dom :~: dom
Refl) -> forall a. a -> Maybe a
Just Term a
x
      (Maybe (t :~: BaseW), Maybe (sym :~: "toGenericFn"),
 Maybe (dom :~: '[a]), Maybe (dom :~: dom))
_ -> forall a. Maybe a
Nothing
  rewriteRules BaseW "fromGenericFn" '[dom] a
_ List Term '[dom]
_ Evidence (AppRequires "fromGenericFn" BaseW '[dom] a)
_ = forall a. Maybe a
Nothing

fromGeneric_ ::
  forall a.
  (GenericRequires a, AppRequires "fromGenericFn" BaseW '[SimpleRep a] a) =>
  Term (SimpleRep a) ->
  Term a
fromGeneric_ :: forall a.
(GenericRequires a,
 AppRequires "fromGenericFn" BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ = forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a.
GenericRequires a =>
BaseW "fromGenericFn" '[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)
  , Logic "fromGenericFn" BaseW '[SimpleRep a] a
  ) =>
  Specification a ->
  Specification (SimpleRep a)
toSimpleRepSpec :: forall a.
(HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 Logic "fromGenericFn" BaseW '[SimpleRep a] 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),
 Logic "fromGenericFn" BaseW '[SimpleRep a] 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 "fromGenericFn" 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

-- | Properties needed by objects to appear in the system,
--  if they have no semantic or logical requirements.
--  Mostly used for Lit terms, which are self evaluating
--  But such things also occurr in Contexts.
type Literal a = (Typeable a, Eq a, Show a)

-- | 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 sym t dom rng = (Logic sym t dom rng, All HasSpec dom, HasSpec rng)

data Term a where
  App ::
    forall sym t dom rng.
    AppRequires sym t dom rng =>
    t sym dom rng -> List Term dom -> Term rng
  Lit :: Literal 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 sym dom a
w1 :: x1) (List Term dom
ts :: List Term dom1) == App (t sym 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 sym dom a :~: t sym dom a
Refl) ->
        t sym dom a
w1 forall a. Eq a => a -> a -> Bool
== t sym 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 sym dom a :~: t sym 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_
--   Infix function symbols names end in '.', for example: ==. , <=.
--   E.g  appTerm NotW :: Term Bool -> Term Bool
--        (appTerm NotW (lit False)) builds the Term  (not_ False)
--   Note the witness (NotW) must have a Logic instance like:
--   instance Logic "not_"            BaseW       '[Bool]           Bool where ...
--        Name in Haskell^    type of NotW^    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 sym t as b.
  AppRequires sym t as b =>
  t sym as b -> List Term as -> Term b
appSym :: forall (a :: Symbol) (b :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
AppRequires a b dom rng =>
b a dom rng -> List Term dom -> Term rng
appSym t sym as b
w List Term as
xs = forall (a :: Symbol) (b :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
AppRequires a b dom rng =>
b a dom rng -> List Term dom -> Term rng
App t sym as b
w List Term as
xs

-- Like 'appSym' but builds functions over terms, rather that just one App term.
appTerm ::
  forall sym t ds r.
  AppRequires sym t ds r =>
  t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm :: forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm t sym ds r
sym = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
curryList @ds (forall (a :: Symbol) (b :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
AppRequires a b dom rng =>
b a dom rng -> List Term dom -> Term rng
App @sym @t @ds @r t sym 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

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 sym dom a
x List Term dom
Nil -> forall a ann. Show a => a -> Doc ann
viaShow t sym dom a
x
    App t sym dom a
f List Term dom
as
      | Just Doc ann
doc <- forall (t :: Symbol -> [*] -> * -> *) (s :: Symbol) (dom :: [*])
       rng ann.
(Syntax t, All HasSpec dom, HasSpec rng) =>
t s dom rng -> List Term dom -> Int -> Maybe (Doc ann)
prettyWit t sym dom a
f List Term dom
as Int
p -> Doc ann
doc -- Use Function Symbol specific pretty printers
    App t sym dom a
f List Term dom
as
      | forall (t :: Symbol -> [*] -> * -> *) (s :: Symbol) (dom :: [*])
       rng.
Syntax t =>
t s dom rng -> Bool
isInFix t sym 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 sym 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 sym 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

-- ==========================================================
-- Contexts
-- ==========================================================

data
  Context
    (s :: Symbol)
    (t :: Symbol -> [Type] -> Type -> Type)
    (dom :: [Type])
    rng
    hole
  where
  Context ::
    (All HasSpec dom, HasSpec rng) =>
    t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole

data Ctx hole rng where
  Ctx ::
    (HasSpec hole, HasSpec rng, Logic s t dom rng) => Context s t dom rng hole -> Ctx hole rng
  HOLE :: HasSpec a => Ctx a a

data Mode = Pre | Post

infixr 5 :<|
infixr 5 :|>
infixr 5 :<>

data CList (x :: Mode) (as :: [Type]) (hole :: Type) (y :: Type) where
  End :: CList 'Post '[] h y
  (:<|) :: Literal a => a -> CList 'Post as h y -> CList 'Post (a ': as) h y
  (:<>) :: HasSpec y => Ctx x y -> (forall i j. CList 'Post as i j) -> CList 'Pre (y ': as) x y
  (:|>) :: Literal a => a -> CList 'Pre as h y -> CList 'Pre (a ': as) h y

instance Show (CList mode as hole y) where
  show :: CList mode as hole y -> String
show CList mode as hole y
clist = String
"(" forall a. [a] -> [a] -> [a]
++ forall (mode :: Mode) (as :: [*]) hole y.
CList mode as hole y -> String
showCList CList mode as hole y
clist
    where
      showCList :: forall m ds h z. CList m ds h z -> String
      showCList :: forall (mode :: Mode) (as :: [*]) hole y.
CList mode as hole y -> String
showCList CList m ds h z
End = String
"End)"
      showCList (a
x :<| CList 'Post as h z
y) = forall a. Show a => a -> String
show a
x forall a. [a] -> [a] -> [a]
++ String
" :<| " forall a. [a] -> [a] -> [a]
++ forall (mode :: Mode) (as :: [*]) hole y.
CList mode as hole y -> String
showCList CList 'Post as h z
y
      showCList (Ctx h z
hole :<> forall i j. CList 'Post as i j
xs) = forall a. Show a => a -> String
show Ctx h z
hole forall a. [a] -> [a] -> [a]
++ String
" :<> " forall a. [a] -> [a] -> [a]
++ forall (mode :: Mode) (as :: [*]) hole y.
CList mode as hole y -> String
showCList forall i j. CList 'Post as i j
xs
      showCList (a
x :|> CList 'Pre as h z
y) = forall a. Show a => a -> String
show a
x forall a. [a] -> [a] -> [a]
++ String
" :|> " forall a. [a] -> [a] -> [a]
++ forall (mode :: Mode) (as :: [*]) hole y.
CList mode as hole y -> String
showCList CList 'Pre as h z
y

-- Examples
c6 :: HasSpec b => CList 'Pre [Bool, String, b, Bool, ()] b b
c6 :: forall b. HasSpec b => CList 'Pre '[Bool, String, b, Bool, ()] b b
c6 = Bool
True forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> (String
"abc" :: String) forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Pre b h y -> CList 'Pre (a : b) h y
:|> forall a. HasSpec a => Ctx a a
HOLE forall y x (a :: [*]).
HasSpec y =>
Ctx x y
-> (forall i j. CList 'Post a i j) -> CList 'Pre (y : a) x y
:<> Bool
True forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Post b h y -> CList 'Post (a : b) h y
:<| () forall a (b :: [*]) h y.
Literal a =>
a -> CList 'Post b h y -> CList 'Post (a : b) h y
:<| forall h y. CList 'Post '[] h y
End

val6 :: List [] [Bool, String, Int, Bool, ()]
val6 :: List [] '[Bool, String, Int, Bool, ()]
val6 = [] forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> [String
"abc"] forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> [Int
67, Int
12] forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> [Bool
True, Bool
False] forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> [()] forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil

-- Show instances

instance Show (Ctx rng hole) where
  show :: Ctx rng hole -> String
show (Ctx Context s t dom hole rng
context) = forall a. Show a => a -> String
show Context s t dom hole rng
context
  show Ctx rng hole
HOLE = String
"[_ " forall a. [a] -> [a] -> [a]
++ forall {k} (t :: k). Typeable t => String
showType @hole forall a. [a] -> [a] -> [a]
++ String
" _]"

instance Show (t s d r) => Show (Context s t d r h) where
  show :: Context s t d r h -> String
show (Context t s d r
f CList 'Pre d h y
xs) = String
"(Context " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t s d r
f forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CList 'Pre d h y
xs forall a. [a] -> [a] -> [a]
++ String
")"

-- ====================================================
-- 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 s t dom rng.
    Logic s t dom rng =>
    t s dom rng -> Fun dom rng

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

extractf :: forall s t d r. LogicRequires s t d r => Fun d r -> Maybe (t s d r)
extractf :: forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (d :: [*]) r.
LogicRequires s t d r =>
Fun d r -> Maybe (t s d r)
extractf (Fun (t s d r
x :: t1 s1 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 @s @s1, 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 s :~: s
Refl, Just d :~: d
Refl, Just r :~: r
Refl) -> forall a. a -> Maybe a
Just t s d r
x
    (Maybe (t :~: t), Maybe (s :~: s), Maybe (d :~: d),
 Maybe (r :~: r))
_ -> forall a. Maybe a
Nothing

appFun :: (HasSpec x, HasSpec b) => Fun '[x] b -> Term x -> Term b
appFun :: forall x b.
(HasSpec x, HasSpec b) =>
Fun '[x] b -> Term x -> Term b
appFun (Fun t s '[x] b
f) Term x
x = forall (a :: Symbol) (b :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
AppRequires a b dom rng =>
b a dom rng -> List Term dom -> Term rng
App t s '[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 s d1 r1
f) (Fun t s d2 r2
g) =
  case forall (s1 :: Symbol) (t1 :: Symbol -> [*] -> * -> *) (d1 :: [*])
       r1 (s2 :: Symbol) (t2 :: Symbol -> [*] -> * -> *) (d2 :: [*]) r2.
(Logic s1 t1 d1 r1, Logic s2 t2 d2 r2) =>
t1 s1 d1 r1
-> t2 s2 d2 r2
-> Maybe (t1 s1 d1 r1, s1 :~: s2, t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym t s d1 r1
f t s d2 r2
g of
    Just (t s d1 r1
_f, s :~: s
Refl, t :~: t
Refl, d1 :~: d2
Refl, r1 :~: r2
Refl) -> Bool
True
    Maybe (t s d1 r1, s :~: s, 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.
-- The commented out Constructor patterns , work but have such convoluted types,
-- that without a monomorphic typing, are basically useless. Use the xxx_ functions instead.

pattern Equal ::
  forall b.
  () =>
  forall a.
  (b ~ Bool, Eq a, HasSpec a) =>
  Term a -> Term a -> Term b
pattern $mEqual :: forall {r} {b}.
Term b
-> (forall {a}.
    (b ~ Bool, Eq a, HasSpec a) =>
    Term a -> Term a -> r)
-> ((# #) -> r)
-> r
Equal x y <-
  ( App
      (sameWitness (EqualW @Int) -> Just (EqualW, Refl, Refl))
      (x :> y :> Nil)
    )

pattern Elem ::
  forall b.
  () =>
  forall a.
  (b ~ Bool, Eq a, HasSpec a) =>
  Term a -> Term [a] -> Term b
pattern $mElem :: forall {r} {b}.
Term b
-> (forall {a}.
    (b ~ Bool, Eq a, HasSpec a) =>
    Term a -> Term [a] -> r)
-> ((# #) -> r)
-> r
Elem x y <-
  ( App
      (sameWitness (ElemW @()) -> Just (ElemW, Refl, Refl))
      (x :> y :> Nil)
    )

pattern FromGeneric ::
  forall rng.
  () =>
  forall a.
  (rng ~ a, GenericRequires a, HasSpec a, AppRequires "fromGenericFn" 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 "fromGenericFn" BaseW '[SimpleRep a] rng) =>
    Term (SimpleRep a) -> r)
-> ((# #) -> r)
-> r
FromGeneric x <-
  (App (sameWitness (FromGenericW @()) -> Just (FromGenericW, Refl, Refl)) (x :> Nil))

-- where FromGeneric x = App FromGenericW (x :> Nil)

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

-- where ToGeneric x = App ToGenericW (x :> Nil)

pattern InjRight ::
  forall c.
  () =>
  forall a b.
  ( c ~ Sum a b
  , AppRequires "rightFn" BaseW '[b] c
  ) =>
  Term b -> Term c
pattern $mInjRight :: forall {r} {c}.
Term c
-> (forall {a} {b}.
    (c ~ Sum a b, AppRequires "rightFn" BaseW '[b] c) =>
    Term b -> r)
-> ((# #) -> r)
-> r
InjRight x <- (App (sameWitness (InjRightW @_ @_) -> Just (InjRightW, Refl, Refl)) (x :> Nil))

-- whereInjRight x = App InjRightW (x :> Nil)

pattern InjLeft ::
  forall c.
  () =>
  forall a b.
  ( c ~ Sum a b
  , AppRequires "leftFn" BaseW '[a] c
  ) =>
  Term a -> Term c
pattern $mInjLeft :: forall {r} {c}.
Term c
-> (forall {a} {b}.
    (c ~ Sum a b, AppRequires "leftFn" BaseW '[a] c) =>
    Term a -> r)
-> ((# #) -> r)
-> r
InjLeft x <- (App (sameWitness (InjLeftW @() @()) -> Just (InjLeftW, Refl, Refl)) (x :> Nil))

-- where InjLeft x = App InjLeftW (x :> Nil)

pattern ProdFst ::
  forall c.
  () =>
  forall a b.
  ( c ~ a
  , Typeable (Prod a b)
  , HasSpec a
  , AppRequires "prodFst_" BaseW '[Prod a b] a
  ) =>
  Term (Prod a b) -> Term c
pattern $mProdFst :: forall {r} {c}.
Term c
-> (forall {a} {b}.
    (c ~ a, Typeable (Prod a b), HasSpec a,
     AppRequires "prodFst_" BaseW '[Prod a b] a) =>
    Term (Prod a b) -> r)
-> ((# #) -> r)
-> r
ProdFst x <- (App (sameWitness (ProdFstW @() @()) -> Just (ProdFstW, Refl, Refl)) (x :> Nil))

-- where Fst x = App ProdFstW (x :> Nil)

pattern ProdSnd ::
  forall c.
  () =>
  forall a b.
  ( c ~ b
  , Typeable (Prod a b)
  , HasSpec b
  , AppRequires "prodSnd_" BaseW '[Prod a b] b
  ) =>
  Term (Prod a b) -> Term c
pattern $mProdSnd :: forall {r} {c}.
Term c
-> (forall {a} {b}.
    (c ~ b, Typeable (Prod a b), HasSpec b,
     AppRequires "prodSnd_" BaseW '[Prod a b] b) =>
    Term (Prod a b) -> r)
-> ((# #) -> r)
-> r
ProdSnd x <- (App (sameWitness (ProdSndW @() @()) -> Just (ProdSndW, Refl, Refl)) (x :> Nil))

-- where Snd x = App ProdSndW (x :> Nil)

pattern Product ::
  forall c.
  () =>
  forall a b.
  ( c ~ Prod a b
  , AppRequires "prod_" BaseW '[a, b] c
  ) =>
  Term a -> Term b -> Term c
pattern $mProduct :: forall {r} {c}.
Term c
-> (forall {a} {b}.
    (c ~ Prod a b, AppRequires "prod_" BaseW '[a, b] c) =>
    Term a -> Term b -> r)
-> ((# #) -> r)
-> r
Product x y <- (App (sameWitness (ProdW @_ @_) -> Just (ProdW, Refl, Refl)) (x :> y :> Nil))

-- where Pair x y = App ProdW (x :> y :> Nil)