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

------------------------------------------------------------------------
-- 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 forall a. Eq a => a -> a -> Bool
== Var a
x'
  Lit a
a == Lit a
b = a
a forall a. Eq a => a -> a -> Bool
== a
b
  App (t dom a
w1 :: x1) (List (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 {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @dom1 @dom2, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @x1 @x2) of
      (Just dom :~: dom
Refl, Just t dom a :~: t dom a
Refl) ->
        t dom a
w1 forall a. Eq a => a -> a -> Bool
== t dom a
w2
          Bool -> Bool -> Bool
&& List (TermD deps) dom
ts forall a. Eq a => a -> a -> Bool
== 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 -> forall a b. b -> Either a b
Right a
a
  V Var a
v -> case forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
env Var a
v of
    Just a
a -> forall a b. b -> Either a b
Right a
a
    Maybe a
Nothing -> forall a b. a -> Either a b
Left (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Couldn't find " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var a
v forall a. [a] -> [a] -> [a]
++ String
" in " forall a. [a] -> [a] -> [a]
++ 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 {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 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env) List (TermD deps) dom
ts
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ forall a. Identity a -> a
runIdentity (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 forall a deps. Env -> TermD deps a -> Either (NonEmpty String) a
runTermE Env
env TermD deps a
x of
  Left NonEmpty String
msgs -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE NonEmpty String
msgs
  Right a
val -> 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 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) = 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') = forall deps a b. TermD deps a -> TermD deps b -> Bool
fastInequality TermD deps a
a TermD deps a
b Bool -> Bool -> 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
_ = 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 -> forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
n String
""
    V Var a
x -> forall a ann. Show a => a -> Doc ann
viaShow Var a
x
    App t dom a
x List (TermD deps) dom
Nil -> 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 <- 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
      | 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 ->
          forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 TermD deps a
a forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow t dom a
f forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 TermD deps a
b
      | Bool
otherwise -> forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ forall a ann. Show a => a -> Doc ann
viaShow t dom a
f forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall ann. [Doc ann] -> Doc ann
fillSep (forall (f :: * -> *) (as :: [*]) ann.
All Show as =>
(forall a. Show a => f a -> Doc ann) -> List f as -> [Doc ann]
ppListShow (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 = 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 -> ShowS
showsPrec Int
p TermD deps a
t = forall a. Show a => a -> ShowS
shows forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Int -> a -> WithPrec a
WithPrec Int
p 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 -> Weighted f b -> Weighted f a
forall a b. (a -> b) -> Weighted f a -> Weighted f b
forall (f :: * -> *) a b.
Functor f =>
a -> Weighted f b -> Weighted f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Weighted f a -> Weighted f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Weighted f b -> Weighted f a
$c<$ :: forall (f :: * -> *) a b.
Functor f =>
a -> Weighted f b -> Weighted f a
fmap :: forall a b. (a -> b) -> Weighted f a -> Weighted f b
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Weighted f a -> Weighted f b
Functor, forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall {f :: * -> *}. Traversable f => Functor (Weighted f)
forall {f :: * -> *}. Traversable f => Foldable (Weighted f)
forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Weighted f (m a) -> m (Weighted f a)
forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Weighted f (f a) -> f (Weighted f a)
forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Weighted f a -> m (Weighted f b)
forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
sequence :: forall (m :: * -> *) a.
Monad m =>
Weighted f (m a) -> m (Weighted f a)
$csequence :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Weighted f (m a) -> m (Weighted f a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Weighted f a -> m (Weighted f b)
$cmapM :: forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Weighted f a -> m (Weighted f b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Weighted f (f a) -> f (Weighted f a)
$csequenceA :: forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Weighted f (f a) -> f (Weighted f a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
$ctraverse :: forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
Traversable, forall a. Weighted f a -> Bool
forall m a. Monoid m => (a -> m) -> Weighted f a -> m
forall a b. (a -> b -> b) -> b -> Weighted f a -> b
forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Weighted f a -> Bool
forall (f :: * -> *) a. (Foldable f, Num a) => Weighted f a -> a
forall (f :: * -> *) a. (Foldable f, Ord a) => Weighted f a -> a
forall (f :: * -> *) m. (Foldable f, Monoid m) => Weighted f m -> m
forall (f :: * -> *) a. Foldable f => Weighted f a -> Bool
forall (f :: * -> *) a. Foldable f => Weighted f a -> Int
forall (f :: * -> *) a. Foldable f => Weighted f a -> [a]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Weighted f a -> a
forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Weighted f a -> m
forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Weighted f a -> b
forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Weighted f a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Weighted f a -> a
$cproduct :: forall (f :: * -> *) a. (Foldable f, Num a) => Weighted f a -> a
sum :: forall a. Num a => Weighted f a -> a
$csum :: forall (f :: * -> *) a. (Foldable f, Num a) => Weighted f a -> a
minimum :: forall a. Ord a => Weighted f a -> a
$cminimum :: forall (f :: * -> *) a. (Foldable f, Ord a) => Weighted f a -> a
maximum :: forall a. Ord a => Weighted f a -> a
$cmaximum :: forall (f :: * -> *) a. (Foldable f, Ord a) => Weighted f a -> a
elem :: forall a. Eq a => a -> Weighted f a -> Bool
$celem :: forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Weighted f a -> Bool
length :: forall a. Weighted f a -> Int
$clength :: forall (f :: * -> *) a. Foldable f => Weighted f a -> Int
null :: forall a. Weighted f a -> Bool
$cnull :: forall (f :: * -> *) a. Foldable f => Weighted f a -> Bool
toList :: forall a. Weighted f a -> [a]
$ctoList :: forall (f :: * -> *) a. Foldable f => Weighted f a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Weighted f a -> a
$cfoldl1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Weighted f a -> a
foldr1 :: forall a. (a -> a -> a) -> Weighted f a -> a
$cfoldr1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Weighted f a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Weighted f a -> b
$cfoldl' :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Weighted f a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Weighted f a -> b
$cfoldl :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Weighted f a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Weighted f a -> b
$cfoldr' :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Weighted f a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Weighted f a -> b
$cfoldr :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Weighted f a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Weighted f a -> m
$cfoldMap' :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Weighted f a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Weighted f a -> m
$cfoldMap :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Weighted f a -> m
fold :: forall m. Monoid m => Weighted f m -> m
$cfold :: forall (f :: * -> *) m. (Foldable f, Monoid m) => Weighted f m -> m
Foldable)

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

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

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

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

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

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