{-# 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 #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

-- | This module contains the most basic parts the implementation. Essentially
--   everything to define Specification, HasSpec, HasSimpleRep, Term, Pred, and the Syntax,
--   Semantics, and Logic class. It also has a few HasSpec, HasSimpleRep, and Logic
--   instances for basic types needed to define the default types and methods of HasSpec.
--   It also supplies Eq, Pretty, and Show instances on the syntax (Term, Pred, Binder etc.)
--   because many functions require these instances. It exports functions that define the
--   user interface to the domain embedded language (constrained, forall, exists etc.).
--   And, by design, nothing more.
module Constrained.Base where

import Constrained.AbstractSyntax
import Constrained.Core (
  Evidence (..),
  Value (..),
  Var (..),
  eqVar,
 )
import Constrained.DependencyInjection
import Constrained.FunctionSymbol
import Constrained.GenT (
  GE (..),
  GenT,
  MonadGenError (..),
  catMessageList,
  catMessages,
  fatalError,
  pureGen,
 )
import Constrained.Generic (
  HasSimpleRep,
  SimpleRep,
  fromSimpleRep,
  toSimpleRep,
 )
import Constrained.List (
  All,
  FunTy,
  List (..),
  ListCtx (..),
  MapList,
  TypeList,
  curryList,
  fillListCtx,
  foldMapList,
  mapListCtxC,
  pattern ListCtx,
  pattern NilCtx,
 )
import Constrained.PrettyUtils
import Constrained.TypeErrors
import Control.Monad.Writer (
  Writer,
  tell,
 )
import Data.Foldable (
  toList,
 )
import Data.Kind (Constraint, Type)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NE
import Data.Orphans ()
import Data.Semigroup (Max (..), getMax)
import Data.Typeable
import GHC.Stack
import Prettyprinter hiding (cat)
import Test.QuickCheck (arbitrary, shrink)

newtype TypeSpecF a = TypeSpecF (TypeSpec a)

instance Show (TypeSpec a) => Show (TypeSpecF a) where
  show :: TypeSpecF a -> String
show (TypeSpecF TypeSpec a
ts) = TypeSpec a -> String
forall a. Show a => a -> String
show TypeSpec a
ts

newtype HintF a = HintF (Hint a)

instance Show (Hint a) => Show (HintF a) where
  show :: HintF a -> String
show (HintF Hint a
h) = Hint a -> String
forall a. Show a => a -> String
show Hint a
h

data Deps

instance Dependencies Deps where
  type HasSpecD Deps = HasSpec
  type TypeSpecD Deps = TypeSpecF
  type LogicD Deps = Logic
  type ForallableD Deps = Forallable
  type HasGenHintD Deps = HasGenHint
  type HintD Deps = HintF

type Binder = BinderD Deps

type AppRequires t as b = AppRequiresD Deps t as b

type Pred = PredD Deps

type Term = TermD Deps

type Specification = SpecificationD Deps

pattern TypeSpec :: () => HasSpec a => TypeSpec a -> [a] -> Specification a
pattern $mTypeSpec :: forall {r} {a}.
Specification a
-> (HasSpec a => TypeSpec a -> [a] -> r) -> ((# #) -> r) -> r
$bTypeSpec :: forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec ts cant = TypeSpecD (TypeSpecF ts) cant

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

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

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

-- | A First-order typed logic has 4 components
--     1. Terms        (Variables (x), Constants (5), and Applications (F x 5)
--        Applications, apply a function symbol to a list of arguments: (FunctionSymbol term1 .. termN)
--     2. Predicates   (Ordered, Odd, ...)
--     3. Connectives  (And, Or, Not, =>, ...)
--     4. Quantifiers  (Forall, Exists)
--
-- The Syntax, Semantics, and Logic classes implement new function symbols in
-- the first order logic. Note that a function symbol is first order
-- data, that uniquely identifies a higher order function. The three classes
-- supply varying levels of functionality, relating to the Syntax, Semantics, and
-- Logical operations of the function symbol.

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

  propagateTypeSpec ::
    (AppRequires t as b, HasSpec a) =>
    t as b ->
    ListCtx Value as (HOLE a) ->
    TypeSpec b ->
    [b] ->
    Specification a
  propagateTypeSpec t as b
f ListCtx Value as (HOLE a)
ctx TypeSpec b
ts [b]
cant = t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (as :: [*]) b a.
(AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate t as b
f ListCtx Value as (HOLE a)
ctx (TypeSpec b -> [b] -> Specification b
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec b
ts [b]
cant)

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

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

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

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

  saturate :: t dom Bool -> List Term dom -> [Pred]
  saturate t dom Bool
_symbol List (TermD Deps) dom
_ = []

-- This is where the logical properties of a function symbol are applied to transform one spec into another
-- Note if there is a bunch of functions nested together, like (sizeOf_ (elems_ (snd_ x)))
-- we propagate each of those nested function symbols over the current spec, one at a time.
-- The result of this propagation is then made the current spec in the recusive calls to 'propagateSpec'
propagateSpec ::
  forall v a.
  HasSpec v =>
  Specification a ->
  Ctx v a ->
  Specification v
propagateSpec :: forall v a.
HasSpec v =>
Specification a -> Ctx v a -> Specification v
propagateSpec Specification a
spec = \case
  Ctx v a
CtxHOLE -> Specification v
Specification a
spec
  CtxApp fn as a
f (ListCtx List Value as
pre Ctx v a
c List Value as'
suf)
    | Evidence (HasSpec a)
Evidence <- Ctx v a -> Evidence (HasSpec a)
forall v a. Ctx v a -> Evidence (HasSpec a)
ctxHasSpec Ctx v a
c -> Specification a -> Ctx v a -> Specification v
forall v a.
HasSpec v =>
Specification a -> Ctx v a -> Specification v
propagateSpec (fn as a
-> ListCtx Value as (HOLE a) -> Specification a -> Specification a
forall (as :: [*]) b a.
(AppRequires fn as b, HasSpec a) =>
fn as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate fn as a
f (List Value as
-> HOLE a a -> List Value as' -> ListCtx Value as (HOLE a)
forall (as'' :: [*]) (f :: * -> *) (c :: * -> *) (as :: [*]) a
       (as' :: [*]).
(as'' ~ Append as (a : as')) =>
List f as -> c a -> List f as' -> ListCtx f as'' c
ListCtx List Value as
pre HOLE a a
forall {k} (a :: k). HOLE a a
HOLE List Value as'
suf) Specification a
spec) Ctx v a
c

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

-- | Contexts for Terms, basically a term with a _single_ HOLE
-- instead of a variable. This is used to traverse the defining
-- constraints for a variable and turn them into a spec. Each
-- subterm `f vs Ctx vs'` for lists of values `vs` and `vs'`
-- gets given to the `propagateSpecFun` for `f` as  `(f vs HOLE vs')`.
data Ctx v a where
  -- | A single hole of type `v`. Note ctxHOLE is a nullary constructor, where the `a` type index is the same as the `v` type index.
  CtxHOLE ::
    HasSpec v =>
    Ctx v v
  -- | The application `f vs Ctx vs'`
  CtxApp ::
    ( AppRequires fn as b
    , HasSpec b
    , TypeList as
    , Typeable as
    , All HasSpec as
    , Logic fn
    ) =>
    fn as b ->
    -- This is basically a `List` where
    -- everything is `Value` except for
    -- one entry which is `Ctx fn v`.
    ListCtx Value as (Ctx v) ->
    Ctx v b

-- | This is used together with `ListCtx` to form
-- just the arguments to `f vs Ctx vs'` - replacing
-- `Ctx` with `HOLE`, to get a `ListCtx Value as (HOLE a)` which then can be used as an input to `propagate`.
data HOLE a b where
  HOLE :: HOLE a a

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

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

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

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

{-# COMPLETE Unary #-}

-- | Convenient patterns for binary contexts (the arrow :<: points towards the hole)
pattern (:<:) :: (Typeable b, Show b) => HOLE c a -> b -> ListCtx Value '[a, b] (HOLE c)
pattern h $m:<: :: forall {r} {b} {c} {a}.
(Typeable b, Show b) =>
ListCtx Value '[a, b] (HOLE c)
-> (HOLE c a -> b -> r) -> ((# #) -> r) -> r
$b:<: :: forall b c a.
(Typeable b, Show b) =>
HOLE c a -> b -> ListCtx Value '[a, b] (HOLE c)
:<: a = h :? Value a :> Nil

-- | Convenient patterns for binary contexts (the arrow :>: points towards the hole)
pattern (:>:) :: (Typeable a, Show a) => a -> HOLE c b -> ListCtx Value '[a, b] (HOLE c)
pattern a $m:>: :: forall {r} {a} {c} {b}.
(Typeable a, Show a) =>
ListCtx Value '[a, b] (HOLE c)
-> (a -> HOLE c b -> r) -> ((# #) -> r) -> r
$b:>: :: forall a c b.
(Typeable a, Show a) =>
a -> HOLE c b -> ListCtx Value '[a, b] (HOLE c)
:>: h = Value a :! NilCtx h

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

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

-- | From a ListCtx, build a (List Term as), to which the function symbol can be applied.
fromListCtx :: All HasSpec as => ListCtx Value as (HOLE a) -> Term a -> List Term as
fromListCtx :: forall (as :: [*]) a.
All HasSpec as =>
ListCtx Value as (HOLE a) -> Term a -> List (TermD Deps) as
fromListCtx ListCtx Value as (HOLE a)
ctx Term a
t = ListCtx (TermD Deps) as (HOLE a)
-> (forall a. HOLE a a -> Term a) -> List (TermD Deps) as
forall (f :: * -> *) (as :: [*]) (c :: * -> *).
ListCtx f as c -> (forall a. c a -> f a) -> List f as
fillListCtx (forall (c :: * -> Constraint) (as :: [*]) (f :: * -> *)
       (g :: * -> *) (h :: * -> *).
All c as =>
(forall a. c a => f a -> g a) -> ListCtx f as h -> ListCtx g as h
mapListCtxC @HasSpec (\(Value a
a) -> a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
a) ListCtx Value as (HOLE a)
ctx) (\HOLE a a
HOLE -> Term a
Term a
t)

-- =================================================================
-- The class (HasSpec a) tells us what operations type 'a' must
-- support to add it to the constraint solver and generator
-- Writing HasSpec instances gives the system the power to grow
-- Don't be afraid of all the methods. Most have default implementations.
-- =================================================================

type GenericallyInstantiated a =
  ( AssertComputes
      (SimpleRep a)
      ( Text "Trying to use a generic instantiation of "
          :<>: ShowType a
          :<>: Text ", likely in a HasSpec instance."
          :$$: Text
                 "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."
      )
  , HasSimpleRep a
  , HasSpec (SimpleRep a)
  , TypeSpec a ~ TypeSpec (SimpleRep a)
  )

type TypeSpecEqShow a =
  ( AssertComputes
      (TypeSpec a)
      ( Text "Can't compute "
          :<>: ShowType (TypeSpec a)
          :$$: Text "Either because of a missing definition of TypeSpec or a missing instance of HasSimpleRep."
      )
  , Show (TypeSpec a)
  , Typeable (TypeSpec a)
  )

{- NOTE: type errors in constrained-generators
    It's easy to make a mistake like this:
      data Bad = Bad | Worse deriving (Eq, Show)
      instance HasSpec Bad
    Missing that this requires an instance of HasSimpleRep for Bad to work.
    The two `AssertComputes` uses above are here to give you better error messages when you make this mistake,
    e.g. giving you something like this:
      src/Constrained/Examples/Basic.hs:327:10: error: [GHC-64725]
          • Can't compute TypeSpec (SimpleRep Bad)
            Either because of a missing definition of TypeSpec or a missing instance of HasSimpleRep.
          • In the instance declaration for ‘HasSpec Bad’
          |
      327 | instance HasSpec Bad
          |          ^^^^^^^^^^^

      src/Constrained/Examples/Basic.hs:327:10: error: [GHC-64725]
          • Trying to use a generic instantiation of Bad, likely in a HasSpec instance.
            However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep.
          • In the expression: Constrained.Base.$dmemptySpec @(Bad)
            In an equation for ‘emptySpec’:
                emptySpec = Constrained.Base.$dmemptySpec @(Bad)
            In the instance declaration for ‘HasSpec Bad’
          |
      327 | instance HasSpec Bad
          |          ^^^^^^^^^^^
-}

class
  ( Typeable a
  , Eq a
  , Show a
  , TypeSpecEqShow a
  ) =>
  HasSpec a
  where
  -- | The `TypeSpec a` is the type-specific `Specification a`.
  type TypeSpec a

  type TypeSpec a = TypeSpec (SimpleRep a)

  -- `TypeSpec` behaves sort-of like a monoid with a neutral
  -- element `emptySpec` and a `combineSpec` for combining
  -- two `TypeSpec a`. However, in order to provide flexibilty
  -- `combineSpec` takes two `TypeSpec` and constucts a `Specification`. This
  -- avoids e.g. having to have a separate implementation of `ErrorSpec`
  -- and `MemberSpec` in `TypeSpec`.

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

  -- | Generate a value that satisfies the `TypeSpec`.
  -- The key property for this generator is soundness:
  --  ∀ a ∈ genFromTypeSpec spec. a `conformsTo` spec
  genFromTypeSpec :: (HasCallStack, MonadGenError m) => TypeSpec a -> GenT m a

  -- | Check conformance to the spec.
  conformsTo :: HasCallStack => a -> TypeSpec a -> Bool

  -- | Shrink an `a` with the aide of a `TypeSpec`
  shrinkWithTypeSpec :: TypeSpec a -> a -> [a]

  -- | Convert a spec to predicates:
  -- The key property here is:
  --   ∀ a. a `conformsTo` spec == a `conformsTo` constrained (\t -> toPreds t spec)
  toPreds :: Term a -> TypeSpec a -> Pred

  -- | Compute an upper and lower bound on the number of solutions genFromTypeSpec might return
  cardinalTypeSpec :: TypeSpec a -> Specification Integer

  -- | A bound on the number of solutions `genFromTypeSpec TrueSpec` can produce.
  --   For a type with finite elements, we can get a much more accurate
  --   answer than TrueSpec
  cardinalTrueSpec :: Specification Integer
  cardinalTrueSpec = Specification Integer
forall deps a. SpecificationD deps 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 -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just NonEmpty String
msgs
    Specification a
_ -> Maybe (NonEmpty String)
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 Bool -> Writer [String] Bool
forall a. a -> WriterT [String] Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      else [String] -> WriterT [String] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [String
"Fails by " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeSpec a -> String
forall a. Show a => a -> String
show TypeSpec a
spec] WriterT [String] Identity ()
-> Writer [String] Bool -> Writer [String] Bool
forall a b.
WriterT [String] Identity a
-> WriterT [String] Identity b -> WriterT [String] Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Writer [String] Bool
forall a. a -> WriterT [String] Identity a
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 = TypeSpec a -> [a] -> Specification a
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 = TypeSpec a -> Specification a
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 = Evidence (Prerequisites a)
forall (c :: Constraint). c => Evidence c
Evidence

  {- NOTE: Below follows default implementations for the functions in this
     class based on Generics.  They are meant to provide an implementation of
     `HasSpec a` when `HasSimpleRep a` and `HasSpec (SimpleRep a)`. For example,
     for a newtype wrapper like `newtype Foo = Foo Word64` we can define `SimpleRep
     Foo = Word64` with the requisite instance for `HasSimpleRep` (all of which
     is derived from `Generic Foo`) and the instance for `HasSpec Foo` is
     essentially the same as the instance for `Word64`. This is achieved by
     ensuring that `TypeSpec Foo = TypeSpec Word64` (c.f. the default
     implementation of `TypeSpec` above). To this end, the implementations
     below simply convert the relevant things between `SimpleRep a` and `a`.
     For example, in the implementation of `combineSpec s s'` we treat `s` and
     `s'` (which have type `TypeSpec a`) as `TypeSpec (SimpleRep a)`,
     combine them, and go from the resulting `Specification (SimpleRep a)` to `Specification
     a` using `fromSimpleRepSpec`.
   -}

  default emptySpec :: GenericallyInstantiated a => TypeSpec a
  emptySpec = forall a. HasSpec a => TypeSpec a
emptySpec @(SimpleRep a)

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

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

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

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

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

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

------------------------------------------------------------------------
-- Some instances of HasSpec
------------------------------------------------------------------------

-- | NOTE: this instance means we have to use `ifElse`, `whenTrue`, and `whenFalse` instead
-- of `caseOn` for `Bool`
instance HasSpec Bool where
  type TypeSpec Bool = ()
  emptySpec :: TypeSpec Bool
emptySpec = ()
  combineSpec :: TypeSpec Bool -> TypeSpec Bool -> Specification Bool
combineSpec TypeSpec Bool
_ TypeSpec Bool
_ = TypeSpec Bool -> Specification Bool
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec ()
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Bool -> GenT m Bool
genFromTypeSpec TypeSpec Bool
_ = Gen Bool -> GenT m Bool
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen Gen Bool
forall a. Arbitrary a => Gen a
arbitrary
  cardinalTypeSpec :: TypeSpec Bool -> Specification Integer
cardinalTypeSpec TypeSpec Bool
_ = Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
2
  cardinalTrueSpec :: Specification Integer
cardinalTrueSpec = Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
2
  shrinkWithTypeSpec :: TypeSpec Bool -> Bool -> [Bool]
shrinkWithTypeSpec TypeSpec Bool
_ = Bool -> [Bool]
forall a. Arbitrary a => a -> [a]
shrink
  conformsTo :: HasCallStack => Bool -> TypeSpec Bool -> Bool
conformsTo Bool
_ TypeSpec Bool
_ = Bool
True
  toPreds :: Term Bool -> TypeSpec Bool -> Pred
toPreds Term Bool
_ TypeSpec Bool
_ = Bool -> Pred
forall p. IsPred p => p -> Pred
toPred Bool
True

instance HasSpec () where
  type TypeSpec () = ()
  emptySpec :: TypeSpec ()
emptySpec = ()
  combineSpec :: TypeSpec () -> TypeSpec () -> Specification ()
combineSpec TypeSpec ()
_ TypeSpec ()
_ = TypeSpec () -> Specification ()
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 ()
_ = () -> GenT m ()
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  toPreds :: Term () -> TypeSpec () -> Pred
toPreds Term ()
_ TypeSpec ()
_ = Pred
forall deps. PredD deps
TruePred
  cardinalTypeSpec :: TypeSpec () -> Specification Integer
cardinalTypeSpec TypeSpec ()
_ = NonEmpty Integer -> Specification Integer
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec (Integer -> NonEmpty Integer
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
1)
  cardinalTrueSpec :: Specification Integer
cardinalTrueSpec = Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
1
  typeSpecOpt :: TypeSpec () -> [()] -> Specification ()
typeSpecOpt TypeSpec ()
_ [] = Specification ()
forall deps a. SpecificationD deps a
TrueSpec
  typeSpecOpt TypeSpec ()
_ (()
_ : [()]
_) = NonEmpty String -> Specification ()
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Non null 'cant' set in typeSpecOpt @()")

-- ===================================================================
-- toGeneric and fromGeneric as Function Symbols
-- That means they can be used inside (Term a)
-- ===================================================================

-- The things you need to know to work with the generics which translates things
-- into their SimpleRep, made of Sum and Prod
type GenericRequires a =
  ( HasSpec a -- This gives Show, Eq, and Typeable instances
  , GenericallyInstantiated a
  )

-- The constructors of BaseW, are first order data (i.e Function Symbols) that describe functions.
-- The Base functions are just the functions neccessary to define Specification, and the classes
-- HasSimpleRep, HasSpec, Syntax, Semantics, and Logic. We call BaseW a 'witness type', and use
-- the convention that all witness types (and their constructors) have "W" as thrit last character.
data BaseW (dom :: [Type]) (rng :: Type) where
  ToGenericW :: GenericRequires a => BaseW '[a] (SimpleRep a)
  FromGenericW :: GenericRequires a => BaseW '[SimpleRep a] a

deriving instance Eq (BaseW dom rng)

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

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

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

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

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

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

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

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

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

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

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

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

toSimpleRepSpec ::
  forall a.
  GenericRequires a =>
  Specification a ->
  Specification (SimpleRep a)
toSimpleRepSpec :: forall a.
GenericRequires a =>
Specification a -> Specification (SimpleRep a)
toSimpleRepSpec = \case
  ExplainSpec [String]
es Specification a
s -> [String]
-> Specification (SimpleRep a) -> Specification (SimpleRep a)
forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (Specification a -> Specification (SimpleRep a)
forall a.
GenericRequires a =>
Specification a -> Specification (SimpleRep a)
toSimpleRepSpec Specification a
s)
  Specification a
TrueSpec -> Specification (SimpleRep a)
forall deps a. SpecificationD deps a
TrueSpec
  ErrorSpec NonEmpty String
e -> NonEmpty String -> Specification (SimpleRep a)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec NonEmpty String
e
  TypeSpec TypeSpec a
s'' [a]
cant -> TypeSpec (SimpleRep a)
-> [SimpleRep a] -> Specification (SimpleRep a)
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec a
TypeSpec (SimpleRep a)
s'' ([SimpleRep a] -> Specification (SimpleRep a))
-> [SimpleRep a] -> Specification (SimpleRep a)
forall a b. (a -> b) -> a -> b
$ (a -> SimpleRep a) -> [a] -> [SimpleRep a]
forall a b. (a -> b) -> [a] -> [b]
map a -> SimpleRep a
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep [a]
cant
  MemberSpec NonEmpty a
elems -> NonEmpty (SimpleRep a) -> Specification (SimpleRep a)
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec (NonEmpty (SimpleRep a) -> Specification (SimpleRep a))
-> NonEmpty (SimpleRep a) -> Specification (SimpleRep a)
forall a b. (a -> b) -> a -> b
$ NonEmpty (SimpleRep a) -> NonEmpty (SimpleRep a)
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (NonEmpty (SimpleRep a) -> NonEmpty (SimpleRep a))
-> NonEmpty (SimpleRep a) -> NonEmpty (SimpleRep a)
forall a b. (a -> b) -> a -> b
$ (a -> SimpleRep a) -> NonEmpty a -> NonEmpty (SimpleRep a)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> SimpleRep a
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep NonEmpty a
elems
  SuspendedSpec Var a
x Pred
p ->
    (Term (SimpleRep a) -> Pred) -> Specification (SimpleRep a)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (SimpleRep a) -> Pred) -> Specification (SimpleRep a))
-> (Term (SimpleRep a) -> Pred) -> Specification (SimpleRep a)
forall a b. (a -> b) -> a -> b
$ \Term (SimpleRep a)
x' ->
      TermD Deps a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (Term (SimpleRep a) -> TermD Deps a
forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ Term (SimpleRep a)
x') (Var a
x Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred
p) :: Pred

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

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

-- Like 'appSym' but builds functions over terms, rather that just one App term.
appTerm ::
  forall t ds r.
  AppRequires t ds r =>
  t ds r ->
  FunTy (MapList Term ds) (Term r)
appTerm :: forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList (TermD Deps) ds) (Term r)
appTerm t ds r
sym = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
curryList @ds (forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App @Deps @t @ds @r t ds r
sym)

name :: String -> Term a -> Term a
name :: forall a. String -> Term a -> Term a
name String
nh (V (Var Int
i String
_)) = Var a -> TermD Deps a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V (Int -> String -> Var a
forall a. Int -> String -> Var a
Var Int
i String
nh)
name String
_ TermD Deps a
_ = String -> TermD Deps 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 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"v" then Term a
t else Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V (Int -> String -> Var a
forall a. Int -> String -> Var a
Var Int
i String
nh)
named String
_ Term a
t = Term a
t

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 Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred
bodyPred
  where
    bodyPred :: Pred
bodyPred = p -> Pred
forall p. IsPred p => p -> Pred
toPred p
body
    newv :: Var a
newv = Int -> String -> Var a
forall a. Int -> String -> Var a
Var (Pred -> Int
nextVar Pred
bodyPred) String
"v"
    body :: p
body = Term a -> p
bodyf (Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
newv)

    nextVar :: Pred -> Int
nextVar Pred
q = Int
1 Int -> Int -> Int
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) = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Var a -> Int
forall a. Var a -> Int
nameOf Var a
x) (Pred -> Int
bound Pred
p)

    bound :: Pred -> Int
bound (ElemPred Bool
_ TermD Deps a
_ NonEmpty a
_) = -Int
1
    bound (Explain NonEmpty String
_ Pred
p) = Pred -> Int
bound Pred
p
    bound (Subst Var a
x TermD Deps a
_ Pred
p) = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Var a -> Int
forall a. Var a -> Int
nameOf Var a
x) (Pred -> Int
bound Pred
p)
    bound (And [Pred]
ps) = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (-Int
1) Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (Pred -> Int) -> [Pred] -> [Int]
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. TermD Deps b -> b) -> GE a
_ BinderD Deps a
b) = BinderD Deps a -> Int
forall a. Binder a -> Int
boundBinder BinderD Deps a
b
    bound (Let TermD Deps a
_ BinderD Deps a
b) = BinderD Deps a -> Int
forall a. Binder a -> Int
boundBinder BinderD Deps a
b
    bound (ForAll TermD Deps t
_ BinderD Deps e
b) = BinderD Deps e -> Int
forall a. Binder a -> Int
boundBinder BinderD Deps e
b
    bound (Case TermD Deps (SumOver as)
_ List (Weighted (BinderD Deps)) as
cs) = Max Int -> Int
forall a. Max a -> a
getMax (Max Int -> Int) -> Max Int -> Int
forall a b. (a -> b) -> a -> b
$ (forall a. Weighted (BinderD Deps) a -> Max Int)
-> List (Weighted (BinderD Deps)) as -> Max Int
forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList (Int -> Max Int
forall a. a -> Max a
Max (Int -> Max Int)
-> (Weighted (BinderD Deps) a -> Int)
-> Weighted (BinderD Deps) a
-> Max Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder a -> Int
forall a. Binder a -> Int
boundBinder (Binder a -> Int)
-> (Weighted (BinderD Deps) a -> Binder a)
-> Weighted (BinderD Deps) a
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Weighted (BinderD Deps) a -> Binder a
forall (f :: * -> *) a. Weighted f a -> f a
thing) List (Weighted (BinderD Deps)) 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

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

class Forallable t e | t -> e where
  fromForAllSpec ::
    (HasSpec t, HasSpec e) => Specification e -> Specification t
  default fromForAllSpec ::
    ( HasSpec e
    , Forallable (SimpleRep t) e
    , GenericRequires t
    ) =>
    Specification e ->
    Specification t
  fromForAllSpec Specification e
es = Specification (SimpleRep t) -> Specification t
forall a.
GenericRequires a =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec (Specification (SimpleRep t) -> Specification t)
-> Specification (SimpleRep t) -> Specification t
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 = SimpleRep t -> [e]
forall t e. Forallable t e => t -> [e]
forAllToList (t -> SimpleRep t
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep t
t)

-- ===========================================
-- 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
forall deps. NonEmpty String -> PredD deps
FalsePred (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"toPred(Lit False)")
  toPred (Assert (Lit Bool
True)) = Pred
forall deps. PredD deps
TruePred
  toPred (Explain NonEmpty String
xs Pred
p) = NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain NonEmpty String
xs (Pred -> Pred
forall p. IsPred p => p -> Pred
toPred Pred
p)
  toPred (And [Pred]
ps) = [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And ((Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
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
forall deps. [PredD deps] -> PredD deps
And ((p -> Pred) -> [p] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map p -> Pred
forall p. IsPred p => p -> Pred
toPred [p]
xs)

instance IsPred Bool where
  toPred :: Bool -> Pred
toPred Bool
True = Pred
forall deps. PredD deps
TruePred
  toPred Bool
False = NonEmpty String -> Pred
forall deps. NonEmpty String -> PredD deps
FalsePred (String -> NonEmpty String
forall a. a -> NonEmpty a
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) = Bool -> Pred
forall p. IsPred p => p -> Pred
toPred Bool
b
  toPred Term Bool
term = Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
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 [a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [a]
xs of
    Maybe (NonEmpty a)
Nothing -> NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec NonEmpty String
messages
    Just NonEmpty a
ys -> NonEmpty a -> Specification a
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec NonEmpty a
ys

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

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

equalSpec :: a -> Specification a
equalSpec :: forall a. a -> Specification a
equalSpec = NonEmpty a -> SpecificationD Deps a
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec (NonEmpty a -> SpecificationD Deps a)
-> (a -> NonEmpty a) -> a -> SpecificationD Deps a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> NonEmpty a
forall a. a -> NonEmpty a
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 = TypeSpec a -> [a] -> Specification a
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (forall a. HasSpec a => TypeSpec a
emptySpec @a) ([a] -> Specification a) -> (a -> [a]) -> a -> Specification a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [a]
forall a. a -> [a]
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 = TypeSpec a -> [a] -> Specification a
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
typeSpecOpt (forall a. HasSpec a => TypeSpec a
emptySpec @a) ([a] -> Specification a) -> (f a -> [a]) -> f a -> Specification a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> [a]
forall a. f a -> [a]
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 = (Term a -> p) -> BinderD Deps a
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term a -> p
body
   in Var a -> Pred -> SpecificationD Deps a
forall deps a.
HasSpecD deps a =>
Var a -> PredD deps -> SpecificationD deps a
SuspendedSpec Var a
x Pred
p

isErrorLike :: forall a. Specification a -> Bool
isErrorLike :: forall a. Specification a -> Bool
isErrorLike (ExplainSpec [String]
_ SpecificationD Deps a
s) = SpecificationD Deps a -> Bool
forall a. Specification a -> Bool
isErrorLike SpecificationD Deps 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 SpecificationD Deps 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 -> String -> NonEmpty String
forall a. a -> NonEmpty a
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 SpecificationD Deps a
_ = String -> NonEmpty String
forall a. a -> NonEmpty 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 -> NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty (NonEmpty String) -> NonEmpty String
catMessageList NonEmpty (NonEmpty String)
xs)
  FatalError NonEmpty (NonEmpty String)
es -> String -> Specification a
forall a. HasCallStack => String -> a
error (String -> Specification a) -> String -> Specification a
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 [] SpecificationD Deps a
x) = NonEmpty String -> SpecificationD Deps a -> SpecificationD Deps a
forall a. NonEmpty String -> Specification a -> Specification a
addToErrorSpec NonEmpty String
es SpecificationD Deps a
x
addToErrorSpec NonEmpty String
es (ExplainSpec [String]
es2 SpecificationD Deps a
x) = [String] -> SpecificationD Deps a -> SpecificationD Deps a
forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String]
es2 (NonEmpty String -> SpecificationD Deps a -> SpecificationD Deps a
forall a. NonEmpty String -> Specification a -> Specification a
addToErrorSpec NonEmpty String
es SpecificationD Deps a
x)
addToErrorSpec NonEmpty String
es (ErrorSpec NonEmpty String
es') = NonEmpty String -> SpecificationD Deps a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String
es NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es')
addToErrorSpec NonEmpty String
_ SpecificationD Deps a
s = SpecificationD Deps a
s

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

-- ====================================================
-- The Fun type encapuslates a Logic instance to hide
-- everything but the domain and range. This is a way
-- to pass around functions without pain. Usefull in the
-- ListFoldy implementaion that deals with higher order functions.

data Fun dom rng where
  Fun ::
    forall t dom rng.
    AppRequires t dom rng =>
    t dom rng ->
    Fun dom rng

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

extractf :: Typeable t => Fun d r -> Maybe (t d r)
extractf :: forall (t :: [*] -> * -> *) (d :: [*]) r.
Typeable t =>
Fun d r -> Maybe (t d r)
extractf (Fun t d r
f) = t d r -> Maybe (t d r)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast t d r
f

appFun :: Fun '[x] b -> Term x -> Term b
appFun :: forall x b. Fun '[x] b -> Term x -> Term b
appFun (Fun t '[x] b
f) Term x
x = t '[x] b -> List (TermD Deps) '[x] -> TermD Deps b
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App t '[x] b
f (Term x
x Term x -> List (TermD Deps) '[] -> List (TermD Deps) '[x]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List (TermD Deps) '[]
forall {k} (f :: k -> *). List f '[]
Nil)

sameFun :: Fun d1 r1 -> Fun d2 r2 -> Bool
sameFun :: forall (d1 :: [*]) r1 (d2 :: [*]) r2.
Fun d1 r1 -> Fun d2 r2 -> Bool
sameFun (Fun t d1 r1
f) (Fun t d2 r2
g) = case t d1 r1 -> Maybe (t d2 r2)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast t d1 r1
f of
  Just t d2 r2
f' -> t d2 r2
f' t d2 r2 -> t d2 r2 -> Bool
forall a. Eq a => a -> a -> Bool
== t d2 r2
g
  Maybe (t d2 r2)
Nothing -> Bool
False

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

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

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

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

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