{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE KindSignatures #-}
{-# 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
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
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
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
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
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)
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 ::
((forall b. TermD deps b -> b) -> GE a) ->
BinderD deps a ->
PredD deps
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
) =>
TermD deps b ->
TermD deps a ->
(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) ->
List (Weighted (BinderD deps)) as ->
PredD deps
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
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
data SpecificationD deps a where
ExplainSpec :: [String] -> SpecificationD deps a -> SpecificationD deps a
MemberSpec ::
NE.NonEmpty a ->
SpecificationD deps a
ErrorSpec ::
NE.NonEmpty String ->
SpecificationD deps a
SuspendedSpec ::
HasSpecD deps a =>
Var a ->
PredD deps ->
SpecificationD deps a
TypeSpecD ::
HasSpecD deps a =>
TypeSpecD deps a ->
[a] ->
SpecificationD deps a
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
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