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

module Constrained.AbstractSyntax where

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

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

-- See `Constrained.DependencyInjection` to better understand `deps` - it's a
-- pointer to postpone having to define `HasSpec` and friends here.
data TermD deps a where
  App ::
    AppRequiresD deps t dom rng =>
    t dom rng ->
    List (TermD deps) dom ->
    TermD deps rng
  Lit :: (Typeable a, Eq a, Show a) => a -> TermD deps a
  V :: (HasSpecD deps a, Typeable a) => Var a -> TermD deps a

type AppRequiresD deps (t :: [Type] -> Type -> Type) dom rng =
  ( LogicD deps t
  , Syntax t
  , Semantics t
  , TypeList dom
  , Eq (t dom rng)
  , Show (t dom rng)
  , Typeable t
  , All Typeable dom
  , Typeable dom
  , Typeable rng
  , All (HasSpecD deps) dom
  , All Show dom
  , HasSpecD deps rng
  , Show rng
  )

instance Eq (TermD deps a) where
  V Var a
x == :: TermD deps a -> TermD deps a -> Bool
== V Var a
x' = Var a
x Var a -> Var a -> Bool
forall a. Eq a => a -> a -> Bool
== Var a
x'
  Lit a
a == Lit a
b = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
  App (t dom a
w1 :: x1) (List (TermD deps) dom
ts :: List (TermD deps) dom1) == App (t dom a
w2 :: x2) (List (TermD deps) dom
ts' :: List (TermD deps) dom2) =
    case (forall (a :: [*]) (b :: [*]).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
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)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @x1 @x2) of
      (Just dom :~: dom
Refl, Just t dom a :~: t dom a
Refl) ->
        t dom a
w1 t dom a -> t dom a -> Bool
forall a. Eq a => a -> a -> Bool
== t dom a
t dom a
w2
          Bool -> Bool -> Bool
&& List (TermD deps) dom
ts List (TermD deps) dom -> List (TermD deps) dom -> Bool
forall a. Eq a => a -> a -> Bool
== List (TermD deps) dom
List (TermD deps) dom
ts'
      (Maybe (dom :~: dom), Maybe (t dom a :~: t dom a))
_ -> Bool
False
  TermD deps a
_ == TermD deps a
_ = Bool
False

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

runTermE :: forall a deps. Env -> TermD deps a -> Either (NE.NonEmpty String) a
runTermE :: forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env = \case
  Lit a
a -> a -> Either (NonEmpty String) a
forall a b. b -> Either a b
Right a
a
  V Var a
v -> case Env -> Var a -> Maybe a
forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
env Var a
v of
    Just a
a -> a -> Either (NonEmpty String) a
forall a b. b -> Either a b
Right a
a
    Maybe a
Nothing -> NonEmpty String -> Either (NonEmpty String) a
forall a b. a -> Either a b
Left (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Couldn't find " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Var a -> String
forall a. Show a => a -> String
show Var a
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Env -> String
forall a. Show a => a -> String
show Env
env))
  App t dom a
f List (TermD deps) dom
ts -> do
    List Identity dom
vs <- (forall a. TermD deps a -> Either (NonEmpty String) (Identity a))
-> List (TermD deps) dom
-> Either (NonEmpty String) (List Identity dom)
forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). f a -> m (g a)) -> List f as -> m (List g as)
mapMList ((a -> Identity a)
-> Either (NonEmpty String) a
-> Either (NonEmpty String) (Identity a)
forall a b.
(a -> b)
-> Either (NonEmpty String) a -> Either (NonEmpty String) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Identity a
forall a. a -> Identity a
Identity (Either (NonEmpty String) a
 -> Either (NonEmpty String) (Identity a))
-> (TermD deps a -> Either (NonEmpty String) a)
-> TermD deps a
-> Either (NonEmpty String) (Identity a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> TermD deps a -> Either (NonEmpty String) a
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env) List (TermD deps) dom
ts
    a -> Either (NonEmpty String) a
forall a. a -> Either (NonEmpty String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Either (NonEmpty String) a)
-> a -> Either (NonEmpty String) a
forall a b. (a -> b) -> a -> b
$ (forall a. Identity a -> a)
-> FunTy dom a -> List Identity dom -> a
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
forall (f :: * -> *) r.
(forall a. f a -> a) -> FunTy dom r -> List f dom -> r
uncurryList_ Identity a -> a
forall a. Identity a -> a
runIdentity (t dom a -> FunTy dom a
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t dom a
f) List Identity dom
vs

runTerm :: MonadGenError m => Env -> TermD deps a -> m a
runTerm :: forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env TermD deps a
x = case Env -> TermD deps a -> Either (NonEmpty String) a
forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env TermD deps a
x of
  Left NonEmpty String
msgs -> NonEmpty String -> m a
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE NonEmpty String
msgs
  Right a
val -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val

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

-- | Sound but not complete inequality on terms
fastInequality :: TermD deps a -> TermD deps b -> Bool
fastInequality :: forall deps a b. TermD deps a -> TermD deps b -> Bool
fastInequality (V (Var Int
i String
_)) (V (Var Int
j String
_)) = Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j
fastInequality Lit {} Lit {} = Bool
False
fastInequality (App t dom a
_ List (TermD deps) dom
as) (App t dom b
_ List (TermD deps) dom
bs) = List (TermD deps) dom -> List (TermD deps) dom -> Bool
forall deps (as :: [*]) (bs :: [*]).
List (TermD deps) as -> List (TermD deps) bs -> Bool
go List (TermD deps) dom
as List (TermD deps) dom
bs
  where
    go :: List (TermD deps) as -> List (TermD deps) bs -> Bool
    go :: forall deps (as :: [*]) (bs :: [*]).
List (TermD deps) as -> List (TermD deps) bs -> Bool
go List (TermD deps) as
Nil List (TermD deps) bs
Nil = Bool
False
    go (TermD deps a
a :> List (TermD deps) as1
as') (TermD deps a
b :> List (TermD deps) as1
bs') = TermD deps a -> TermD deps a -> Bool
forall deps a b. TermD deps a -> TermD deps b -> Bool
fastInequality TermD deps a
a TermD deps a
b Bool -> Bool -> Bool
|| List (TermD deps) as1 -> List (TermD deps) as1 -> Bool
forall deps (as :: [*]) (bs :: [*]).
List (TermD deps) as -> List (TermD deps) bs -> Bool
go List (TermD deps) as1
as' List (TermD deps) as1
bs'
    go List (TermD deps) as
_ List (TermD deps) bs
_ = Bool
True
fastInequality TermD deps a
_ TermD deps b
_ = Bool
True

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

-- | Syntactic operations are ones that have to do with the structure and appearence of the type.
-- See `Constrained.DependencyInjection` to better understand `deps` - it's a
-- pointer to postpone having to define `HasSpec` and friends here.
class Syntax (t :: [Type] -> Type -> Type) where
  isInfix :: t dom rng -> Bool
  isInfix t dom rng
_ = Bool
False
  prettySymbol ::
    forall deps dom rng ann.
    t dom rng ->
    List (TermD deps) dom ->
    Int ->
    Maybe (Doc ann)
  prettySymbol t dom rng
_ List (TermD deps) dom
_ Int
_ = Maybe (Doc ann)
forall a. Maybe a
Nothing

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

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

instance Show a => Show (TermD deps a) where
  showsPrec :: Int -> TermD deps a -> String -> String
showsPrec Int
p TermD deps a
t = Doc Any -> String -> String
forall a. Show a => a -> String -> String
shows (Doc Any -> String -> String) -> Doc Any -> String -> String
forall a b. (a -> b) -> a -> b
$ WithPrec (TermD deps a) -> Doc Any
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
t)

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

-- This is _essentially_ a first-order logic with some extra spicyness thrown
-- in to handle things like sum types and the specific problems you get into
-- when generating from constraints (mostly to do with choosing the order in
-- which to generate things).

-- See `Constrained.DependencyInjection` to better understand `deps` - it's a
-- pointer to postpone having to define `HasSpec` and friends here.
data PredD deps where
  ElemPred ::
    (HasSpecD deps a, Show a) =>
    Bool ->
    TermD deps a ->
    NonEmpty a ->
    PredD deps
  Monitor :: ((forall a. TermD deps a -> a) -> Property -> Property) -> PredD deps
  And :: [PredD deps] -> PredD deps
  Exists ::
    -- | Constructive recovery function for checking
    -- existential quantification
    ((forall b. TermD deps b -> b) -> GE a) ->
    BinderD deps a ->
    PredD deps
  -- This is here because we sometimes need to delay substitution until we're done building
  -- terms and predicates. This is because our surface syntax relies on names being "a bit"
  -- lazily bound to avoid infinite loops when trying to create new names.
  Subst ::
    ( HasSpecD deps a
    , Show a
    ) =>
    Var a ->
    TermD deps a ->
    PredD deps ->
    PredD deps
  Let ::
    TermD deps a ->
    BinderD deps a ->
    PredD deps
  Assert :: TermD deps Bool -> PredD deps
  Reifies ::
    ( HasSpecD deps a
    , HasSpecD deps b
    , Show a
    , Show b
    ) =>
    -- | This depends on the `a` term
    TermD deps b ->
    TermD deps a ->
    -- | Recover a useable value from the `a` term.
    (a -> b) ->
    PredD deps
  DependsOn ::
    ( HasSpecD deps a
    , HasSpecD deps b
    , Show a
    , Show b
    ) =>
    TermD deps a ->
    TermD deps b ->
    PredD deps
  ForAll ::
    ( ForallableD deps t e
    , HasSpecD deps t
    , HasSpecD deps e
    , Show t
    , Show e
    ) =>
    TermD deps t ->
    BinderD deps e ->
    PredD deps
  Case ::
    ( HasSpecD deps (SumOver as)
    , Show (SumOver as)
    ) =>
    TermD deps (SumOver as) ->
    -- | Each branch of the type is bound with
    -- only one variable because `as` are types.
    -- Constructors with multiple arguments are
    -- encoded with `ProdOver` (c.f. `Constrained.Univ`).
    List (Weighted (BinderD deps)) as ->
    PredD deps
  -- monadic-style `when` - if the first argument is False the second
  -- doesn't apply.
  When ::
    TermD deps Bool ->
    PredD deps ->
    PredD deps
  GenHint ::
    ( HasGenHintD deps a
    , Show a
    , Show (HintD deps a)
    ) =>
    HintD deps a ->
    TermD deps a ->
    PredD deps
  TruePred :: PredD deps
  FalsePred :: NE.NonEmpty String -> PredD deps
  Explain :: NE.NonEmpty String -> PredD deps -> PredD deps

data BinderD deps a where
  (:->) ::
    (HasSpecD deps a, Show a) =>
    Var a ->
    PredD deps ->
    BinderD deps a

deriving instance Show (BinderD deps a)

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

mapWeighted :: (f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted :: forall (f :: * -> *) a (g :: * -> *) b.
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted f a -> g b
f (Weighted Maybe Int
w f a
t) = Maybe Int -> g b -> Weighted g b
forall (f :: * -> *) a. 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 (m :: * -> *) (f :: * -> *) a (g :: * -> *).
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) = Maybe Int -> g a -> Weighted g a
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
w (g a -> Weighted g a) -> m (g a) -> m (Weighted g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> m (g a)
f f a
t

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

instance Monoid (PredD deps) where
  mempty :: PredD deps
mempty = PredD deps
forall deps. PredD deps
TruePred

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

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

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

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) = f a -> Doc ann
forall ann. f a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty f a
t
  pretty (Weighted (Just Int
w) f a
t) = Int -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Int
w Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"~" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> f a -> Doc ann
forall ann. f a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty f a
t

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

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

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

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

instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Pretty (SpecificationD deps a) where
  pretty :: forall ann. SpecificationD deps a -> Doc ann
pretty = WithPrec (SpecificationD deps a) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. WithPrec (SpecificationD deps a) -> Doc ann
pretty (WithPrec (SpecificationD deps a) -> Doc ann)
-> (SpecificationD deps a -> WithPrec (SpecificationD deps a))
-> SpecificationD deps a
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SpecificationD deps a -> WithPrec (SpecificationD deps a)
forall a. Int -> a -> WithPrec a
WithPrec Int
0

instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Show (SpecificationD deps a) where
  showsPrec :: Int -> SpecificationD deps a -> String -> String
showsPrec Int
d = Doc Any -> String -> String
forall a. Show a => a -> String -> String
shows (Doc Any -> String -> String)
-> (SpecificationD deps a -> Doc Any)
-> SpecificationD deps a
-> String
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithPrec (SpecificationD deps a) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. WithPrec (SpecificationD deps a) -> Doc ann
pretty (WithPrec (SpecificationD deps a) -> Doc Any)
-> (SpecificationD deps a -> WithPrec (SpecificationD deps a))
-> SpecificationD deps a
-> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SpecificationD deps a -> WithPrec (SpecificationD deps a)
forall a. Int -> a -> WithPrec a
WithPrec Int
d