{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
-- HasSpec instances for known types Integer, Bool, Set , (,)
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Minimal.Model where

import Constrained.Core (
  Evidence (..),
  Var (..),
  eqVar,
  freshen,
  unionWithMaybe,
 )
import Constrained.Env
import Constrained.GenT
import qualified Constrained.Graph as Graph
import Constrained.List hiding (ListCtx)
import Control.Monad (guard)
import Control.Monad.Writer (Writer, runWriter, tell)
import Data.Foldable (fold)
import qualified Data.Foldable as Foldable (fold)
import Data.Kind
import Data.List (nub, partition, (\\))
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Maybe (isNothing, listToMaybe, maybeToList)
import Data.Semigroup (Any (..))
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable
import GHC.Stack
import Prettyprinter
import Test.Minimal.Base
import Test.Minimal.Syntax
import Test.QuickCheck hiding (forAll)

-- ====================================================
-- Now some concrete examples
-- 1) Introduce the function symbols
-- 2) Give the Syntax, Semantics, and Logic instances
-- 3) Give the HasSpec instance
-- ====================================================

-- ======== Integer example ==============

data IntegerSym (dom :: [Type]) rng where
  PlusW :: IntegerSym '[Integer, Integer] Integer
  MinusW :: IntegerSym '[Integer, Integer] Integer
  NegateW :: IntegerSym '[Integer] Integer
  LessOrEqW :: IntegerSym '[Integer, Integer] Bool
  GreaterOrEqW :: IntegerSym '[Integer, Integer] Bool

deriving instance Eq (IntegerSym dom rng)

instance Show (IntegerSym dom rng) where show :: IntegerSym dom rng -> String
show = IntegerSym dom rng -> String
forall (dom :: [*]) rng. IntegerSym dom rng -> String
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
Syntax t =>
t dom rng -> String
name

instance Syntax IntegerSym where
  name :: forall (dom :: [*]) rng. IntegerSym dom rng -> String
name IntegerSym dom rng
PlusW = String
"+."
  name IntegerSym dom rng
MinusW = String
"-."
  name IntegerSym dom rng
NegateW = String
"negate_"
  name IntegerSym dom rng
LessOrEqW = String
"<=."
  name IntegerSym dom rng
GreaterOrEqW = String
">=."
  inFix :: forall (dom :: [*]) rng. IntegerSym dom rng -> Bool
inFix IntegerSym dom rng
NegateW = Bool
False
  inFix IntegerSym dom rng
_ = Bool
True

instance Semantics IntegerSym where
  semantics :: forall (d :: [*]) r. IntegerSym d r -> FunTy d r
semantics IntegerSym d r
PlusW = FunTy d r
Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)
  semantics IntegerSym d r
MinusW = (-)
  semantics IntegerSym d r
NegateW = FunTy d r
Integer -> Integer
forall a. Num a => a -> a
negate
  semantics IntegerSym d r
LessOrEqW = FunTy d r
Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
  semantics IntegerSym d r
GreaterOrEqW = FunTy d r
Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(>=)

instance Logic IntegerSym where
  propagate :: forall (as :: [*]) b a.
(AppRequires IntegerSym as b, HasSpec a) =>
IntegerSym as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate IntegerSym as b
tag ListCtx as (HOLE a)
ctx Spec b
spec = case (IntegerSym as b
tag, ListCtx as (HOLE a)
ctx, Spec b
spec) of
    (IntegerSym as b
_, ListCtx as (HOLE a)
_, Spec b
TrueSpec) -> Spec a
forall a. Spec a
TrueSpec
    (IntegerSym as b
_, ListCtx as (HOLE a)
_, ErrorSpec NonEmpty String
xs) -> NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
xs
    (IntegerSym as b
f, ListCtx as (HOLE a)
context, SuspendedSpec Var b
v Pred
ps) ->
      (Term a -> Pred) -> Spec a
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term a -> Pred) -> Spec a) -> (Term a -> Pred) -> Spec a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> Term b -> Binder b -> Pred
forall a. Term a -> Binder a -> Pred
Let (IntegerSym as b -> List Term as -> Term b
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App IntegerSym as b
f (ListCtx as (HOLE a) -> Term a -> List Term as
forall (as :: [*]) a.
All HasSpec as =>
ListCtx as (HOLE a) -> Term a -> List Term as
fromListCtx ListCtx as (HOLE a)
context Term a
v')) (Var b
v Var b -> Pred -> Binder b
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
    (IntegerSym as b
LessOrEqW, HOLE a b
HOLE :<| x
l, Spec b
bspec) ->
      Spec Bool -> (Bool -> Spec a) -> Spec a
forall a.
(HasSpec Bool, HasSpec a) =>
Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec Spec b
Spec Bool
bspec ((Bool -> Spec a) -> Spec a) -> (Bool -> Spec a) -> Spec a
forall a b. (a -> b) -> a -> b
$ \case Bool
True -> Integer -> Spec Integer
leqSpec x
Integer
l; Bool
False -> Integer -> Spec Integer
gtSpec x
Integer
l
    (IntegerSym as b
LessOrEqW, x
l :|> HOLE a b
HOLE, Spec b
bspec) ->
      Spec Bool -> (Bool -> Spec a) -> Spec a
forall a.
(HasSpec Bool, HasSpec a) =>
Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec Spec b
Spec Bool
bspec ((Bool -> Spec a) -> Spec a) -> (Bool -> Spec a) -> Spec a
forall a b. (a -> b) -> a -> b
$ \case Bool
True -> Integer -> Spec Integer
geqSpec x
Integer
l; Bool
False -> Integer -> Spec Integer
ltSpec x
Integer
l
    (IntegerSym as b
GreaterOrEqW, HOLE a b
HOLE :<| x
x, Spec b
spec1) ->
      IntegerSym '[Integer, Integer] Bool
-> ListCtx '[Integer, Integer] (HOLE a) -> Spec Bool -> Spec a
forall (as :: [*]) b a.
(AppRequires IntegerSym as b, HasSpec a) =>
IntegerSym as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate IntegerSym '[Integer, Integer] Bool
LessOrEqW (x
Integer
x Integer -> HOLE a Integer -> ListCtx '[Integer, Integer] (HOLE a)
forall x (c :: * -> *) b. x -> c b -> ListCtx '[x, b] c
:|> HOLE a a
HOLE a Integer
forall a. HOLE a a
HOLE) Spec b
Spec Bool
spec1
    (IntegerSym as b
GreaterOrEqW, x
x :|> HOLE a b
HOLE, Spec b
spec2) ->
      IntegerSym '[Integer, Integer] Bool
-> ListCtx '[Integer, Integer] (HOLE a) -> Spec Bool -> Spec a
forall (as :: [*]) b a.
(AppRequires IntegerSym as b, HasSpec a) =>
IntegerSym as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate IntegerSym '[Integer, Integer] Bool
LessOrEqW (HOLE a a
HOLE a Integer
forall a. HOLE a a
HOLE HOLE a Integer -> Integer -> ListCtx '[Integer, Integer] (HOLE a)
forall (c :: * -> *) b x. c b -> x -> ListCtx '[b, x] c
:<| x
Integer
x) Spec b
Spec Bool
spec2
    (IntegerSym as b
NegateW, Unary HOLE a a
HOLE, TypeSpec TypeSpec b
interval [b]
cant) -> TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Range -> Range
negateRange TypeSpec b
Range
interval) Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> [a] -> Spec a
forall a (f :: * -> *). (HasSpec a, Foldable f) => f a -> Spec a
notMemberSpec ((a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
forall a. Num a => a -> a
negate [b]
[a]
cant)
    (IntegerSym as b
NegateW, Unary HOLE a a
HOLE, MemberSpec NonEmpty b
xs) -> NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec (NonEmpty a -> Spec a) -> NonEmpty a -> Spec a
forall a b. (a -> b) -> a -> b
$ NonEmpty a -> NonEmpty a
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (NonEmpty a -> NonEmpty a) -> NonEmpty a -> NonEmpty a
forall a b. (a -> b) -> a -> b
$ (a -> a) -> NonEmpty a -> NonEmpty a
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. Num a => a -> a
negate NonEmpty b
NonEmpty a
xs
    (IntegerSym as b
PlusW, HOLE a b
HOLE :<| x
n, TypeSpec (Interval Maybe Integer
lo Maybe Integer
hi) [b]
bad) ->
      TypeSpec a -> [a] -> Spec a
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec (Maybe Integer -> Maybe Integer -> Range
Interval ((Integer -> Integer -> Integer
minus x
Integer
n) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
lo) ((Integer -> Integer -> Integer
minus x
Integer
n) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
hi)) ((Integer -> a) -> [Integer] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> Integer -> Integer
minus x
Integer
n) [b]
[Integer]
bad)
    (IntegerSym as b
PlusW, HOLE a b
HOLE :<| x
n, MemberSpec NonEmpty b
xs) ->
      NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec ((Integer -> a) -> NonEmpty Integer -> NonEmpty a
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Integer
minus x
Integer
n) NonEmpty b
NonEmpty Integer
xs)
    (IntegerSym as b
PlusW, x
n :|> HOLE a b
HOLE, TypeSpec (Interval Maybe Integer
lo Maybe Integer
hi) [b]
bad) ->
      TypeSpec a -> [a] -> Spec a
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec (Maybe Integer -> Maybe Integer -> Range
Interval ((Integer -> Integer -> Integer
minus x
Integer
n) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
lo) ((Integer -> Integer -> Integer
minus x
Integer
n) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
hi)) ((Integer -> a) -> [Integer] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> Integer -> Integer
minus x
Integer
n) [b]
[Integer]
bad)
    (IntegerSym as b
PlusW, x
n :|> HOLE a b
HOLE, MemberSpec NonEmpty b
xs) -> NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec ((Integer -> a) -> NonEmpty Integer -> NonEmpty a
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Integer
minus x
Integer
n) NonEmpty b
NonEmpty Integer
xs)
    (IntegerSym as b
MinusW, HOLE a b
HOLE :<| x
n, TypeSpec (Interval Maybe Integer
lo Maybe Integer
hi) [b]
bad) ->
      TypeSpec a -> [a] -> Spec a
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec (Maybe Integer -> Maybe Integer -> Range
Interval ((x -> x -> x
forall a. Num a => a -> a -> a
+ x
n) (x -> Integer) -> Maybe x -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe x
Maybe Integer
lo) ((x -> x -> x
forall a. Num a => a -> a -> a
+ x
n) (x -> Integer) -> Maybe x -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe x
Maybe Integer
hi)) ((x -> a) -> [x] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (x -> x -> x
forall a. Num a => a -> a -> a
+ x
n) [b]
[x]
bad)
    (IntegerSym as b
MinusW, HOLE a b
HOLE :<| x
n, MemberSpec NonEmpty b
xs) ->
      NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec ((x -> a) -> NonEmpty x -> NonEmpty a
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (x -> x -> x
forall a. Num a => a -> a -> a
+ x
n) NonEmpty b
NonEmpty x
xs)
    (IntegerSym as b
MinusW, x
n :|> HOLE a b
HOLE, TypeSpec (Interval Maybe Integer
lo Maybe Integer
hi) [b]
bad) ->
      TypeSpec a -> [a] -> Spec a
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec (Range -> Range
negateRange (Maybe Integer -> Maybe Integer -> Range
Interval ((Integer -> Integer -> Integer
minus x
Integer
n) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
lo) ((Integer -> Integer -> Integer
minus x
Integer
n) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
hi))) ((Integer -> a) -> [Integer] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> Integer -> Integer
minus x
Integer
n) [b]
[Integer]
bad)
    (IntegerSym as b
MinusW, x
n :|> HOLE a b
HOLE, MemberSpec NonEmpty b
xs) ->
      NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec ((Integer -> a) -> NonEmpty Integer -> NonEmpty a
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Integer
minus x
Integer
n) NonEmpty b
NonEmpty Integer
xs)

negateRange :: Range -> Range
negateRange :: Range -> Range
negateRange (Interval Maybe Integer
ml Maybe Integer
mu) = Maybe Integer -> Maybe Integer -> Range
Interval (Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
mu) (Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
ml)

minus :: Integer -> Integer -> Integer
minus :: Integer -> Integer -> Integer
minus Integer
n Integer
x = Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
x

geqSpec :: Integer -> Spec Integer
geqSpec :: Integer -> Spec Integer
geqSpec Integer
n = TypeSpec Integer -> Spec Integer
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Maybe Integer -> Maybe Integer -> Range
Interval (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n) Maybe Integer
forall a. Maybe a
Nothing)

leqSpec :: Integer -> Spec Integer
leqSpec :: Integer -> Spec Integer
leqSpec Integer
n = TypeSpec Integer -> Spec Integer
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Maybe Integer -> Maybe Integer -> Range
Interval Maybe Integer
forall a. Maybe a
Nothing (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n))

gtSpec :: Integer -> Spec Integer
gtSpec :: Integer -> Spec Integer
gtSpec Integer
n = TypeSpec Integer -> Spec Integer
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Maybe Integer -> Maybe Integer -> Range
Interval (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)) Maybe Integer
forall a. Maybe a
Nothing)

ltSpec :: Integer -> Spec Integer
ltSpec :: Integer -> Spec Integer
ltSpec Integer
n = TypeSpec Integer -> Spec Integer
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Maybe Integer -> Maybe Integer -> Range
Interval Maybe Integer
forall a. Maybe a
Nothing (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))

(<=.) :: Term Integer -> Term Integer -> Term Bool
<=. :: Term Integer -> Term Integer -> Term Bool
(<=.) Term Integer
x Term Integer
y = IntegerSym '[Integer, Integer] Bool
-> List Term '[Integer, Integer] -> Term Bool
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App IntegerSym '[Integer, Integer] Bool
LessOrEqW (Term Integer
x Term Integer
-> List Term '[Integer] -> List Term '[Integer, Integer]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term Integer
y Term Integer -> List Term '[] -> List Term '[Integer]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

(>=.) :: Term Integer -> Term Integer -> Term Bool
>=. :: Term Integer -> Term Integer -> Term Bool
(>=.) Term Integer
x Term Integer
y = IntegerSym '[Integer, Integer] Bool
-> List Term '[Integer, Integer] -> Term Bool
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App IntegerSym '[Integer, Integer] Bool
GreaterOrEqW (Term Integer
x Term Integer
-> List Term '[Integer] -> List Term '[Integer, Integer]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term Integer
y Term Integer -> List Term '[] -> List Term '[Integer]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

(+.) :: Term Integer -> Term Integer -> Term Integer
+. :: Term Integer -> Term Integer -> Term Integer
(+.) Term Integer
x Term Integer
y = IntegerSym '[Integer, Integer] Integer
-> List Term '[Integer, Integer] -> Term Integer
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App IntegerSym '[Integer, Integer] Integer
PlusW (Term Integer
x Term Integer
-> List Term '[Integer] -> List Term '[Integer, Integer]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term Integer
y Term Integer -> List Term '[] -> List Term '[Integer]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

(-.) :: Term Integer -> Term Integer -> Term Integer
-. :: Term Integer -> Term Integer -> Term Integer
(-.) Term Integer
x Term Integer
y = IntegerSym '[Integer, Integer] Integer
-> List Term '[Integer, Integer] -> Term Integer
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App IntegerSym '[Integer, Integer] Integer
MinusW (Term Integer
x Term Integer
-> List Term '[Integer] -> List Term '[Integer, Integer]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term Integer
y Term Integer -> List Term '[] -> List Term '[Integer]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

negate_ :: Term Integer -> Term Integer
negate_ :: Term Integer -> Term Integer
negate_ Term Integer
x = IntegerSym '[Integer] Integer
-> List Term '[Integer] -> Term Integer
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App IntegerSym '[Integer] Integer
NegateW (Term Integer
x Term Integer -> List Term '[] -> List Term '[Integer]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

-- =========================
-- HasSpec Integer instance

data Range = Interval (Maybe Integer) (Maybe Integer) deriving (Range -> Range -> Bool
(Range -> Range -> Bool) -> (Range -> Range -> Bool) -> Eq Range
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Range -> Range -> Bool
== :: Range -> Range -> Bool
$c/= :: Range -> Range -> Bool
/= :: Range -> Range -> Bool
Eq, Int -> Range -> ShowS
[Range] -> ShowS
Range -> String
(Int -> Range -> ShowS)
-> (Range -> String) -> ([Range] -> ShowS) -> Show Range
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Range -> ShowS
showsPrec :: Int -> Range -> ShowS
$cshow :: Range -> String
show :: Range -> String
$cshowList :: [Range] -> ShowS
showList :: [Range] -> ShowS
Show)

instance Semigroup Range where
  Interval Maybe Integer
ml Maybe Integer
mu <> :: Range -> Range -> Range
<> Interval Maybe Integer
ml' Maybe Integer
mu' =
    Maybe Integer -> Maybe Integer -> Range
Interval
      ((Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Maybe Integer
ml Maybe Integer
ml')
      ((Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Maybe Integer
mu Maybe Integer
mu')

instance Monoid Range where
  mempty :: Range
mempty = Maybe Integer -> Maybe Integer -> Range
Interval Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing

instance HasSpec Integer where
  type TypeSpec Integer = Range

  -- \| From -∞ to +∞
  anySpec :: TypeSpec Integer
anySpec = Maybe Integer -> Maybe Integer -> Range
Interval Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing

  -- \| Catch inconsistencies after using Monoid operation of the two Ranges.
  combineSpec :: TypeSpec Integer -> TypeSpec Integer -> Spec Integer
combineSpec TypeSpec Integer
s TypeSpec Integer
s' = TypeSpec Integer -> Spec Integer
forall a. HasSpec a => TypeSpec a -> Spec a
guardTypeSpec (TypeSpec Integer
Range
s Range -> Range -> Range
forall a. Semigroup a => a -> a -> a
<> TypeSpec Integer
Range
s')

  -- \| In Interval where the lo bound is greater than the hi bound is inconsistent
  guardTypeSpec :: TypeSpec Integer -> Spec Integer
guardTypeSpec r :: TypeSpec Integer
r@(Interval (Just Integer
n) (Just Integer
m))
    | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
m = NonEmpty String -> Spec Integer
forall a. NonEmpty String -> Spec a
ErrorSpec (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"lower bound greater than upper bound\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Show a => a -> String
show TypeSpec Integer
Range
r))
    | Bool
otherwise = TypeSpec Integer -> Spec Integer
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec TypeSpec Integer
r
  guardTypeSpec TypeSpec Integer
range = TypeSpec Integer -> Spec Integer
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec TypeSpec Integer
range

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Integer -> GenT m Integer
genFromTypeSpec (Interval Maybe Integer
ml Maybe Integer
mu) = do
    Int
n <- GenT m Int
forall (m :: * -> *). Monad m => GenT m Int
sizeT
    (Integer, Integer) -> GenT m Integer
forall a (m :: * -> *).
(Random a, Ord a, Show a, MonadGenError m) =>
(a, a) -> GenT m a
chooseT ((Integer, Integer) -> GenT m Integer)
-> GenT m (Integer, Integer) -> GenT m Integer
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe Integer
-> Maybe Integer -> Integer -> GenT m (Integer, Integer)
forall (m :: * -> *).
MonadGenError m =>
Maybe Integer -> Maybe Integer -> Integer -> m (Integer, Integer)
constrainInterval Maybe Integer
ml Maybe Integer
mu (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)

  conformsTo :: HasCallStack => Integer -> TypeSpec Integer -> Bool
conformsTo Integer
i (Interval Maybe Integer
ml Maybe Integer
mu) = Bool -> (Integer -> Bool) -> Maybe Integer -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
i) Maybe Integer
ml Bool -> Bool -> Bool
&& Bool -> (Integer -> Bool) -> Maybe Integer -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<=) Maybe Integer
mu

  toPreds :: Term Integer -> TypeSpec Integer -> Pred
toPreds Term Integer
v (Interval Maybe Integer
ml Maybe Integer
mu) =
    [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Foldable.fold ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$
      [Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Integer -> Term Integer
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Integer
l Term Integer -> Term Integer -> Term Bool
<=. Term Integer
v | Integer
l <- Maybe Integer -> [Integer]
forall a. Maybe a -> [a]
maybeToList Maybe Integer
ml]
        [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Integer
v Term Integer -> Term Integer -> Term Bool
<=. Integer -> Term Integer
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Integer
u | Integer
u <- Maybe Integer -> [Integer]
forall a. Maybe a -> [a]
maybeToList Maybe Integer
mu]

constrainInterval ::
  MonadGenError m => Maybe Integer -> Maybe Integer -> Integer -> m (Integer, Integer)
constrainInterval :: forall (m :: * -> *).
MonadGenError m =>
Maybe Integer -> Maybe Integer -> Integer -> m (Integer, Integer)
constrainInterval Maybe Integer
ml Maybe Integer
mu Integer
qcSize =
  case (Maybe Integer
ml, Maybe Integer
mu) of
    (Maybe Integer
Nothing, Maybe Integer
Nothing) -> (Integer, Integer) -> m (Integer, Integer)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (-Integer
qcSize', Integer
qcSize')
    (Just Integer
l, Maybe Integer
Nothing)
      | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 -> (Integer, Integer) -> m (Integer, Integer)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
l (Integer -> Integer
forall a. Num a => a -> a
negate Integer
qcSize'), Integer
qcSize')
      | Bool
otherwise -> (Integer, Integer) -> m (Integer, Integer)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
l, Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
qcSize')
    (Maybe Integer
Nothing, Just Integer
u)
      | Integer
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> (Integer, Integer) -> m (Integer, Integer)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer
forall a. Num a => a -> a
negate Integer
qcSize', Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
u Integer
qcSize')
      | Bool
otherwise -> (Integer, Integer) -> m (Integer, Integer)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
u Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
qcSize' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
qcSize', Integer
u)
    (Just Integer
l, Just Integer
u)
      | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
u -> String -> m (Integer, Integer)
forall (m :: * -> *) a. MonadGenError m => String -> m a
genError (String
"bad interval: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
u)
      | Integer
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 -> (Integer, Integer) -> m (Integer, Integer)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> Integer -> Integer
forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeSub Integer
l (Integer -> Integer -> Integer -> Integer
forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeSub Integer
l Integer
u Integer
qcSize') Integer
qcSize', Integer
u)
      | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 -> (Integer, Integer) -> m (Integer, Integer)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
l, Integer -> Integer -> Integer -> Integer
forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeAdd Integer
u (Integer -> Integer -> Integer -> Integer
forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeAdd Integer
u Integer
l Integer
qcSize') Integer
qcSize')
      -- TODO: this is a bit suspect if the bounds are lopsided
      | Bool
otherwise -> (Integer, Integer) -> m (Integer, Integer)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
l (-Integer
qcSize'), Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
u Integer
qcSize')
  where
    qcSize' :: Integer
qcSize' = Integer -> Integer
forall a. Num a => a -> a
abs (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => Integer -> a
fromInteger Integer
qcSize
    -- FIX THIS TO WORK just on Integer, Should be much simpler, as Integer has no undeflow or overflow.
    safeSub :: p -> p -> p -> p
safeSub p
l p
a p
b
      | p
a p -> p -> p
forall a. Num a => a -> a -> a
- p
b p -> p -> Bool
forall a. Ord a => a -> a -> Bool
> p
a = p
l
      | Bool
otherwise = p -> p -> p
forall a. Ord a => a -> a -> a
max p
l (p
a p -> p -> p
forall a. Num a => a -> a -> a
- p
b)
    safeAdd :: p -> p -> p -> p
safeAdd p
u p
a p
b
      | p
a p -> p -> p
forall a. Num a => a -> a -> a
+ p
b p -> p -> Bool
forall a. Ord a => a -> a -> Bool
< p
a = p
u
      | Bool
otherwise = p -> p -> p
forall a. Ord a => a -> a -> a
min p
u (p
a p -> p -> p
forall a. Num a => a -> a -> a
+ p
b)

-- ========== Bool example ==================

data BoolSym (dom :: [Type]) rng where
  NotW :: BoolSym '[Bool] Bool

deriving instance Eq (BoolSym dom rng)

instance Show (BoolSym dom rng) where show :: BoolSym dom rng -> String
show = BoolSym dom rng -> String
forall (dom :: [*]) rng. BoolSym dom rng -> String
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
Syntax t =>
t dom rng -> String
name

instance Syntax BoolSym where
  name :: forall (dom :: [*]) rng. BoolSym dom rng -> String
name BoolSym dom rng
NotW = String
"not_"
  inFix :: forall (dom :: [*]) rng. BoolSym dom rng -> Bool
inFix BoolSym dom rng
_ = Bool
False

instance Semantics BoolSym where
  semantics :: forall (d :: [*]) r. BoolSym d r -> FunTy d r
semantics BoolSym d r
NotW = FunTy d r
Bool -> Bool
not

instance Logic BoolSym where
  propagate :: forall (as :: [*]) b a.
(AppRequires BoolSym as b, HasSpec a) =>
BoolSym as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate BoolSym as b
_ ListCtx as (HOLE a)
_ Spec b
TrueSpec = Spec a
forall a. Spec a
TrueSpec
  propagate BoolSym as b
_ ListCtx as (HOLE a)
_ (ErrorSpec NonEmpty String
msgs) = NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
msgs
  propagate BoolSym as b
NotW (Unary HOLE a a
HOLE) (SuspendedSpec Var b
v Pred
ps) =
    (Term a -> Pred) -> Spec a
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term a -> Pred) -> Spec a) -> (Term a -> Pred) -> Spec a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> Term Bool -> Binder Bool -> Pred
forall a. Term a -> Binder a -> Pred
Let (BoolSym '[Bool] Bool -> List Term '[Bool] -> Term Bool
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App BoolSym '[Bool] Bool
NotW (Term a
Term Bool
v' Term Bool -> List Term '[] -> List Term '[Bool]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)) (Var b
Var Bool
v Var Bool -> Pred -> Binder Bool
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate BoolSym as b
NotW (Unary HOLE a a
HOLE) Spec b
spec =
    Spec Bool -> (Bool -> Spec a) -> Spec a
forall a.
(HasSpec Bool, HasSpec a) =>
Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec Spec b
Spec Bool
spec (a -> Spec a
forall a. a -> Spec a
equalSpec (a -> Spec a) -> (Bool -> a) -> Bool -> Spec a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> a
Bool -> Bool
not)

not_ :: Term Bool -> Term Bool
not_ :: Term Bool -> Term Bool
not_ Term Bool
x = BoolSym '[Bool] Bool -> List Term '[Bool] -> Term Bool
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App BoolSym '[Bool] Bool
NotW (Term Bool
x Term Bool -> List Term '[] -> List Term '[Bool]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

-- =========================
-- HasSpec Bool instance

instance HasSpec Bool where
  type TypeSpec Bool = Set Bool

  anySpec :: TypeSpec Bool
anySpec = [Bool] -> Set Bool
forall a. Ord a => [a] -> Set a
Set.fromList [Bool
False, Bool
True]

  combineSpec :: TypeSpec Bool -> TypeSpec Bool -> Spec Bool
combineSpec TypeSpec Bool
s TypeSpec Bool
s' = TypeSpec Bool -> Spec Bool
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Set Bool -> Set Bool -> Set Bool
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Bool
TypeSpec Bool
s Set Bool
TypeSpec Bool
s')

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Bool -> GenT m Bool
genFromTypeSpec TypeSpec Bool
set
    | Set Bool -> Bool
forall a. Set a -> Bool
Set.null Set Bool
TypeSpec Bool
set = String -> GenT m Bool
forall (m :: * -> *) a. MonadGenError m => String -> m a
fatalError String
"genFromTypeSpec @Set where the typeSpec is Set.empty"
    | Bool
otherwise = [GenT GE Bool] -> GenT m Bool
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
[GenT GE a] -> GenT m a
oneofT ((Bool -> GenT GE Bool) -> [Bool] -> [GenT GE Bool]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> GenT GE Bool
forall a. a -> GenT GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set Bool -> [Bool]
forall a. Set a -> [a]
Set.toList Set Bool
TypeSpec Bool
set))

  guardTypeSpec :: TypeSpec Bool -> Spec Bool
guardTypeSpec TypeSpec Bool
s
    | Set Bool -> Bool
forall a. Set a -> Bool
Set.null Set Bool
TypeSpec Bool
s = NonEmpty String -> Spec Bool
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty String -> Spec Bool) -> NonEmpty String -> Spec Bool
forall a b. (a -> b) -> a -> b
$ String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"guardTypeSpec @Set where the typeSpec is Set.empty"
    | Bool
otherwise = TypeSpec Bool -> [Bool] -> Spec Bool
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec TypeSpec Bool
s []

  conformsTo :: HasCallStack => Bool -> TypeSpec Bool -> Bool
conformsTo Bool
i TypeSpec Bool
set = Bool -> Set Bool -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Bool
i Set Bool
TypeSpec Bool
set

  toPreds :: Term Bool -> TypeSpec Bool -> Pred
toPreds Term Bool
v TypeSpec Bool
set = case Set Bool -> [Bool]
forall a. Set a -> [a]
Set.toList Set Bool
TypeSpec Bool
set of
    [] -> NonEmpty String -> Pred
FalsePred (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"toPreds @Set where the typeSpec is Set.empty")
    (Bool
x : [Bool]
xs) -> Bool -> Term Bool -> NonEmpty Bool -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
True Term Bool
v (Bool
x Bool -> [Bool] -> NonEmpty Bool
forall a. a -> [a] -> NonEmpty a
:| [Bool]
xs)

-- ========== Set example =======================

data SetSym (dom :: [Type]) rng where
  MemberW :: (HasSpec a, Ord a) => SetSym [a, Set a] Bool
  SizeW :: (HasSpec a, Ord a) => SetSym '[Set a] Integer
  SubsetW :: (HasSpec a, Ord a) => SetSym [Set a, Set a] Bool

deriving instance Eq (SetSym dom rng)

instance Show (SetSym dom rng) where show :: SetSym dom rng -> String
show = SetSym dom rng -> String
forall (dom :: [*]) rng. SetSym dom rng -> String
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
Syntax t =>
t dom rng -> String
name

instance Syntax SetSym where
  name :: forall (dom :: [*]) rng. SetSym dom rng -> String
name SetSym dom rng
MemberW = String
"member_"
  name SetSym dom rng
SizeW = String
"size_"
  name SetSym dom rng
SubsetW = String
"subset_"
  inFix :: forall (dom :: [*]) rng. SetSym dom rng -> Bool
inFix SetSym dom rng
_ = Bool
False

instance Semantics SetSym where
  semantics :: forall (d :: [*]) r. SetSym d r -> FunTy d r
semantics SetSym d r
MemberW = FunTy d r
a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member
  semantics SetSym d r
SizeW = FunTy d r
Set a -> Integer
forall a. Set a -> Integer
setSize
  semantics SetSym d r
SubsetW = FunTy d r
Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf

  rewriteRules :: forall (ds :: [*]) rng.
(TypeList ds, Typeable ds, HasSpec rng, All HasSpec ds) =>
SetSym ds rng
-> List Term ds
-> Evidence (Typeable rng, Eq rng, Show rng)
-> Maybe (Term rng)
rewriteRules SetSym ds rng
SubsetW (Lit a
s :> Term a
_ :> List Term as1
Nil) Evidence (Typeable rng, Eq rng, Show rng)
Evidence | Set a -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
Set a
s = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just (Term rng -> Maybe (Term rng)) -> Term rng -> Maybe (Term rng)
forall a b. (a -> b) -> a -> b
$ rng -> Term rng
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit rng
Bool
True
  rewriteRules SetSym ds rng
SubsetW (Term a
x :> Lit a
s :> List Term as1
Nil) Evidence (Typeable rng, Eq rng, Show rng)
Evidence | Set a -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
Set a
s = Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a
x Term a -> Term a -> Term Bool
forall a.
(HasSpec Bool, HasSpec a) =>
Term a -> Term a -> Term Bool
==. a -> Term a
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
Set a
forall a. Set a
Set.empty
  rewriteRules SetSym ds rng
MemberW (Term a
t :> Lit a
s :> List Term as1
Nil) Evidence (Typeable rng, Eq rng, Show rng)
Evidence
    | Set a -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
Set a
s = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just (Term rng -> Maybe (Term rng)) -> Term rng -> Maybe (Term rng)
forall a b. (a -> b) -> a -> b
$ rng -> Term rng
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit rng
Bool
False
    | [a
a] <- Set a -> [a]
forall a. Set a -> [a]
Set.toList a
Set a
s = Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a
t Term a -> Term a -> Term Bool
forall a.
(HasSpec Bool, HasSpec a) =>
Term a -> Term a -> Term Bool
==. a -> Term a
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
  rewriteRules SetSym ds rng
t List Term ds
l Evidence (Typeable rng, Eq rng, Show rng)
Evidence = rng -> Term rng
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (rng -> Term rng) -> Maybe rng -> Maybe (Term rng)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: [*] -> * -> *) (ds :: [*]) rng.
(Typeable rng, Eq rng, Show rng, Semantics t) =>
FunTy ds rng -> List Term ds -> Maybe rng
applyFunSym @SetSym (SetSym ds rng -> FunTy ds rng
forall (d :: [*]) r. SetSym d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics SetSym ds rng
t) List Term ds
l)

instance Logic SetSym where
  propagate :: forall (as :: [*]) b a.
(AppRequires SetSym as b, HasSpec a) =>
SetSym as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate SetSym as b
tag ListCtx as (HOLE a)
ctx Spec b
spec = case (SetSym as b
tag, ListCtx as (HOLE a)
ctx, Spec b
spec) of
    (SetSym as b
_, ListCtx as (HOLE a)
_, Spec b
TrueSpec) -> Spec a
forall a. Spec a
TrueSpec
    (SetSym as b
_, ListCtx as (HOLE a)
_, ErrorSpec NonEmpty String
es) -> NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
es
    (SetSym as b
f, ListCtx as (HOLE a)
context, SuspendedSpec Var b
v Pred
ps) -> (Term a -> Pred) -> Spec a
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term a -> Pred) -> Spec a) -> (Term a -> Pred) -> Spec a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> Term b -> Binder b -> Pred
forall a. Term a -> Binder a -> Pred
Let (SetSym as b -> List Term as -> Term b
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App SetSym as b
f (ListCtx as (HOLE a) -> Term a -> List Term as
forall (as :: [*]) a.
All HasSpec as =>
ListCtx as (HOLE a) -> Term a -> List Term as
fromListCtx ListCtx as (HOLE a)
context Term a
v')) (Var b
v Var b -> Pred -> Binder b
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
    (SetSym as b
MemberW, HOLE a b
HOLE :<| (Set a
s :: Set a), Spec b
spec1) ->
      Spec Bool -> (Bool -> Spec a) -> Spec a
forall a.
(HasSpec Bool, HasSpec a) =>
Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec Spec b
Spec Bool
spec1 ((Bool -> Spec a) -> Spec a) -> (Bool -> Spec a) -> Spec a
forall a b. (a -> b) -> a -> b
$ \case
        Bool
True -> [a] -> NonEmpty String -> Spec a
forall a. [a] -> NonEmpty String -> Spec a
memberSpecList (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
s) (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"propagateSpecFun on (Member x s) where s is Set.empty")
        Bool
False -> Set a -> Spec a
forall a (f :: * -> *). (HasSpec a, Foldable f) => f a -> Spec a
notMemberSpec Set a
s
    (SetSym as b
MemberW, x
e :|> HOLE a b
HOLE, Spec b
spec2) ->
      Spec Bool -> (Bool -> Spec a) -> Spec a
forall a.
(HasSpec Bool, HasSpec a) =>
Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec Spec b
Spec Bool
spec2 ((Bool -> Spec a) -> Spec a) -> (Bool -> Spec a) -> Spec a
forall a b. (a -> b) -> a -> b
$ \case
        Bool
True -> TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec a -> Spec a) -> TypeSpec a -> Spec a
forall a b. (a -> b) -> a -> b
$ Set x -> Spec x -> Spec Integer -> SetSpec x
forall a. Set a -> Spec a -> Spec Integer -> SetSpec a
SetSpec (x -> Set x
forall a. a -> Set a
Set.singleton x
e) Spec x
forall a. Monoid a => a
mempty Spec Integer
forall a. Monoid a => a
mempty
        Bool
False -> TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec a -> Spec a) -> TypeSpec a -> Spec a
forall a b. (a -> b) -> a -> b
$ Set x -> Spec x -> Spec Integer -> SetSpec x
forall a. Set a -> Spec a -> Spec Integer -> SetSpec a
SetSpec Set x
forall a. Monoid a => a
mempty (x -> Spec x
forall a. HasSpec a => a -> Spec a
notEqualSpec x
e) Spec Integer
forall a. Monoid a => a
mempty
    (SetSym as b
SizeW, Unary HOLE a a
HOLE, Spec b
spec3) -> TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Set a -> Spec a -> Spec Integer -> SetSpec a
forall a. Set a -> Spec a -> Spec Integer -> SetSpec a
SetSpec Set a
forall a. Monoid a => a
mempty Spec a
forall a. Monoid a => a
mempty Spec b
Spec Integer
spec3)
    (SetSym as b
SubsetW, HOLE a b
HOLE :<| x
big, Spec b
spec4) -> Spec Bool -> (Bool -> Spec a) -> Spec a
forall a.
(HasSpec Bool, HasSpec a) =>
Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec Spec b
Spec Bool
spec4 ((Bool -> Spec a) -> Spec a) -> (Bool -> Spec a) -> Spec a
forall a b. (a -> b) -> a -> b
$ \case
      Bool
True -> (Term a -> Pred) -> Spec a
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term a -> Pred) -> Spec a) -> (Term a -> Pred) -> Spec a
forall a b. (a -> b) -> a -> b
$ \Term a
small ->
        [Pred] -> Pred
And
          [ Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set a) -> Term Integer
forall s. (HasSpec s, Ord s) => Term (Set s) -> Term Integer
size_ Term a
Term (Set a)
small Term Integer -> Term Integer -> Term Bool
<=. Integer -> Term Integer
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (Set a -> Integer
forall a. Set a -> Integer
setSize x
Set a
big)
          , Term a -> (Term a -> Pred) -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> (Term a -> Pred) -> Pred
forAll Term a
small ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x -> Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term a -> Term (Set a) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
x (Set a -> Term (Set a)
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit x
Set a
big)
          ]
      Bool
False -> (Term a -> Pred) -> Spec a
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term a -> Pred) -> Spec a) -> (Term a -> Pred) -> Spec a
forall a b. (a -> b) -> a -> b
$ \Term a
small ->
        ((forall b. Term b -> b) -> GE a) -> (Term a -> Pred) -> Pred
forall a.
HasSpec a =>
((forall b. Term b -> b) -> GE a) -> (Term a -> Pred) -> Pred
exists (\forall b. Term b -> b
eval -> Set a -> GE a
forall (t :: * -> *) a. Foldable t => t a -> GE a
headGE (Set a -> GE a) -> Set a -> GE a
forall a b. (a -> b) -> a -> b
$ Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.difference x
Set a
big (Term (Set a) -> Set a
forall b. Term b -> b
eval Term a
Term (Set a)
small)) ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
e ->
          [Pred] -> Pred
And
            [ -- set `DependsOn` e,
              Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term a -> Term (Set a) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
e (Set a -> Term (Set a)
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit x
Set a
big)
            , Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term a -> Term (Set a) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
e Term a
Term (Set a)
small
            ]
    (SetSym as b
SubsetW, x
small :|> HOLE a b
HOLE, Spec b
spec5) -> Spec Bool -> (Bool -> Spec a) -> Spec a
forall a.
(HasSpec Bool, HasSpec a) =>
Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec Spec b
Spec Bool
spec5 ((Bool -> Spec a) -> Spec a) -> (Bool -> Spec a) -> Spec a
forall a b. (a -> b) -> a -> b
$ \case
      Bool
True -> TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec a -> Spec a) -> TypeSpec a -> Spec a
forall a b. (a -> b) -> a -> b
$ Set a -> Spec a -> Spec Integer -> SetSpec a
forall a. Set a -> Spec a -> Spec Integer -> SetSpec a
SetSpec x
Set a
small Spec a
forall a. Spec a
TrueSpec Spec Integer
forall a. Monoid a => a
mempty
      Bool
False -> (Term a -> Pred) -> Spec a
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term a -> Pred) -> Spec a) -> (Term a -> Pred) -> Spec a
forall a b. (a -> b) -> a -> b
$ \Term a
big ->
        ((forall b. Term b -> b) -> GE a) -> (Term a -> Pred) -> Pred
forall a.
HasSpec a =>
((forall b. Term b -> b) -> GE a) -> (Term a -> Pred) -> Pred
exists (\forall b. Term b -> b
eval -> Set a -> GE a
forall (t :: * -> *) a. Foldable t => t a -> GE a
headGE (Set a -> GE a) -> Set a -> GE a
forall a b. (a -> b) -> a -> b
$ Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Term (Set a) -> Set a
forall b. Term b -> b
eval Term a
Term (Set a)
big) x
Set a
small) ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
e ->
          [Pred] -> Pred
And
            [ -- set `DependsOn` e,
              Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term a -> Term (Set a) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
e (Set a -> Term (Set a)
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit x
Set a
small)
            , Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term a -> Term (Set a) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
e Term a
Term (Set a)
big
            ]

setSize :: Set a -> Integer
setSize :: forall a. Set a -> Integer
setSize = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> (Set a -> Int) -> Set a -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> Int
forall a. Set a -> Int
Set.size

size_ :: (HasSpec s, Ord s) => Term (Set s) -> Term Integer
size_ :: forall s. (HasSpec s, Ord s) => Term (Set s) -> Term Integer
size_ Term (Set s)
s = SetSym '[Set s] Integer -> List Term '[Set s] -> Term Integer
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App SetSym '[Set s] Integer
forall b. (HasSpec b, Ord b) => SetSym '[Set b] Integer
SizeW (Term (Set s)
s Term (Set s) -> List Term '[] -> List Term '[Set s]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

subset_ :: (HasSpec s, Ord s) => Term (Set s) -> Term (Set s) -> Term Bool
subset_ :: forall s.
(HasSpec s, Ord s) =>
Term (Set s) -> Term (Set s) -> Term Bool
subset_ Term (Set s)
s1 Term (Set s)
s2 = SetSym '[Set s, Set s] Bool
-> List Term '[Set s, Set s] -> Term Bool
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App SetSym '[Set s, Set s] Bool
forall b. (HasSpec b, Ord b) => SetSym '[Set b, Set b] Bool
SubsetW (Term (Set s)
s1 Term (Set s) -> List Term '[Set s] -> List Term '[Set s, Set s]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term (Set s)
s2 Term (Set s) -> List Term '[] -> List Term '[Set s]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

member_ :: (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ :: forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term a
x Term (Set a)
y = SetSym '[a, Set a] Bool -> List Term '[a, Set a] -> Term Bool
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App SetSym '[a, Set a] Bool
forall b. (HasSpec b, Ord b) => SetSym '[b, Set b] Bool
MemberW (Term a
x Term a -> List Term '[Set a] -> List Term '[a, Set a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term (Set a)
y Term (Set a) -> List Term '[] -> List Term '[Set a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

-- Helpers for the `HasSpec (Set s)` instance

instance Ord s => Container (Set s) s where
  fromForAllSpec :: (HasSpec (Set s), HasSpec s) => Spec s -> Spec (Set s)
fromForAllSpec Spec s
e = TypeSpec (Set s) -> Spec (Set s)
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec (Set s) -> Spec (Set s))
-> TypeSpec (Set s) -> Spec (Set s)
forall a b. (a -> b) -> a -> b
$ Set s -> Spec s -> Spec Integer -> SetSpec s
forall a. Set a -> Spec a -> Spec Integer -> SetSpec a
SetSpec Set s
forall a. Monoid a => a
mempty Spec s
e Spec Integer
forall a. Spec a
TrueSpec
  forAllToList :: Set s -> [s]
forAllToList = Set s -> [s]
forall a. Set a -> [a]
Set.toList

data SetSpec a = SetSpec {forall a. SetSpec a -> Set a
setMust :: Set a, forall a. SetSpec a -> Spec a
setAll :: Spec a, forall a. SetSpec a -> Spec Integer
setCount :: Spec Integer}
  deriving (Int -> SetSpec a -> ShowS
[SetSpec a] -> ShowS
SetSpec a -> String
(Int -> SetSpec a -> ShowS)
-> (SetSpec a -> String)
-> ([SetSpec a] -> ShowS)
-> Show (SetSpec a)
forall a. HasSpec a => Int -> SetSpec a -> ShowS
forall a. HasSpec a => [SetSpec a] -> ShowS
forall a. HasSpec a => SetSpec a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. HasSpec a => Int -> SetSpec a -> ShowS
showsPrec :: Int -> SetSpec a -> ShowS
$cshow :: forall a. HasSpec a => SetSpec a -> String
show :: SetSpec a -> String
$cshowList :: forall a. HasSpec a => [SetSpec a] -> ShowS
showList :: [SetSpec a] -> ShowS
Show)

guardSetSpec :: (HasSpec a, Ord a) => SetSpec a -> Spec (Set a)
guardSetSpec :: forall a. (HasSpec a, Ord a) => SetSpec a -> Spec (Set a)
guardSetSpec (SetSpec Set a
must Spec a
elemS ((Spec Integer -> Spec Integer -> Spec Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Spec Integer
geqSpec Integer
0) -> Spec Integer
size))
  | Just Integer
u <- Spec Integer -> Maybe Integer
knownUpperBound Spec Integer
size
  , Integer
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 =
      NonEmpty String -> Spec (Set a)
forall a. NonEmpty String -> Spec a
ErrorSpec ((String
"guardSetSpec: negative size " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
u) String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [])
  | Bool -> Bool
not ((a -> Bool) -> Set a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
`conformsToSpec` Spec a
elemS) Set a
must) =
      NonEmpty String -> Spec (Set a)
forall a. NonEmpty String -> Spec a
ErrorSpec ((String
"Some 'must' items do not conform to 'element' spec: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
elemS) String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [])
  | Spec Integer -> Bool
forall a. Spec a -> Bool
isErrorLike Spec Integer
size = NonEmpty String -> Spec (Set a)
forall a. NonEmpty String -> Spec a
ErrorSpec (String
"guardSetSpec: error in size" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [])
  | Spec Integer -> Bool
forall a. Spec a -> Bool
isErrorLike (Integer -> Spec Integer
geqSpec (Set a -> Integer
forall a. Set a -> Integer
setSize Set a
must) Spec Integer -> Spec Integer -> Spec Integer
forall a. Semigroup a => a -> a -> a
<> Spec Integer
size) =
      NonEmpty String -> Spec (Set a)
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty String -> Spec (Set a))
-> NonEmpty String -> Spec (Set a)
forall a b. (a -> b) -> a -> b
$
        (String
"Must set size " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Set a -> Integer
forall a. Set a -> Integer
setSize Set a
must) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", is inconsistent with SetSpec size" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec Integer -> String
forall a. Show a => a -> String
show Spec Integer
size)
          String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| []
  | Bool
otherwise = TypeSpec (Set a) -> Spec (Set a)
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Set a -> Spec a -> Spec Integer -> SetSpec a
forall a. Set a -> Spec a -> Spec Integer -> SetSpec a
SetSpec Set a
must Spec a
elemS Spec Integer
size)

knownUpperBound :: Spec Integer -> Maybe Integer
knownUpperBound :: Spec Integer -> Maybe Integer
knownUpperBound Spec Integer
TrueSpec = Maybe Integer
forall a. Maybe a
Nothing
knownUpperBound (MemberSpec NonEmpty Integer
as) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ NonEmpty Integer -> Integer
forall a. Ord a => NonEmpty a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum NonEmpty Integer
as
knownUpperBound ErrorSpec {} = Maybe Integer
forall a. Maybe a
Nothing
knownUpperBound SuspendedSpec {} = Maybe Integer
forall a. Maybe a
Nothing
knownUpperBound (TypeSpec (Interval Maybe Integer
lo Maybe Integer
hi) [Integer]
cant) = Maybe Integer -> Maybe Integer -> Maybe Integer
upper Maybe Integer
lo Maybe Integer
hi
  where
    upper :: Maybe Integer -> Maybe Integer -> Maybe Integer
upper Maybe Integer
_ Maybe Integer
Nothing = Maybe Integer
forall a. Maybe a
Nothing
    upper Maybe Integer
Nothing (Just Integer
b) = [Integer] -> Maybe Integer
forall a. [a] -> Maybe a
listToMaybe ([Integer] -> Maybe Integer) -> [Integer] -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ [Integer
b, Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 ..] [Integer] -> [Integer] -> [Integer]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Integer]
cant
    upper (Just Integer
a) (Just Integer
b)
      | Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
b = Integer
a Integer -> Maybe () -> Maybe Integer
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
a Integer -> [Integer] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Integer]
cant)
      | Bool
otherwise = [Integer] -> Maybe Integer
forall a. [a] -> Maybe a
listToMaybe ([Integer] -> Maybe Integer) -> [Integer] -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ [Integer
b, Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 .. Integer
a] [Integer] -> [Integer] -> [Integer]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Integer]
cant

instance (Ord a, HasSpec a) => Semigroup (SetSpec a) where
  SetSpec Set a
must Spec a
es Spec Integer
size <> :: SetSpec a -> SetSpec a -> SetSpec a
<> SetSpec Set a
must' Spec a
es' Spec Integer
size' =
    Set a -> Spec a -> Spec Integer -> SetSpec a
forall a. Set a -> Spec a -> Spec Integer -> SetSpec a
SetSpec (Set a
must Set a -> Set a -> Set a
forall a. Semigroup a => a -> a -> a
<> Set a
must') (Spec a
es Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> Spec a
es') (Spec Integer
size Spec Integer -> Spec Integer -> Spec Integer
forall a. Semigroup a => a -> a -> a
<> Spec Integer
size')

instance (Ord a, HasSpec a) => Monoid (SetSpec a) where
  mempty :: SetSpec a
mempty = Set a -> Spec a -> Spec Integer -> SetSpec a
forall a. Set a -> Spec a -> Spec Integer -> SetSpec a
SetSpec Set a
forall a. Monoid a => a
mempty Spec a
forall a. Monoid a => a
mempty Spec Integer
forall a. Spec a
TrueSpec

-- =========================
-- HasSpec Set instance

instance (Container (Set a) a, Ord a, HasSpec a) => HasSpec (Set a) where
  type TypeSpec (Set a) = SetSpec a

  anySpec :: TypeSpec (Set a)
anySpec = Set a -> Spec a -> Spec Integer -> SetSpec a
forall a. Set a -> Spec a -> Spec Integer -> SetSpec a
SetSpec Set a
forall a. Set a
Set.empty Spec a
forall a. Spec a
TrueSpec Spec Integer
forall a. Spec a
TrueSpec

  combineSpec :: TypeSpec (Set a) -> TypeSpec (Set a) -> Spec (Set a)
combineSpec TypeSpec (Set a)
x TypeSpec (Set a)
y = SetSpec a -> Spec (Set a)
forall a. (HasSpec a, Ord a) => SetSpec a -> Spec (Set a)
guardSetSpec (TypeSpec (Set a)
SetSpec a
x SetSpec a -> SetSpec a -> SetSpec a
forall a. Semigroup a => a -> a -> a
<> TypeSpec (Set a)
SetSpec a
y)

  conformsTo :: HasCallStack => Set a -> TypeSpec (Set a) -> Bool
conformsTo Set a
s (SetSpec Set a
must Spec a
es Spec Integer
size) =
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ Set a -> Integer
forall a. Set a -> Integer
setSize Set a
s Integer -> Spec Integer -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
`conformsToSpec` Spec Integer
size
      , Set a
must Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set a
s
      , (a -> Bool) -> Set a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
`conformsToSpec` Spec a
es) Set a
s
      ]

  toPreds :: Term (Set a) -> TypeSpec (Set a) -> Pred
toPreds Term (Set a)
s (SetSpec Set a
m Spec a
es Spec Integer
size) =
    [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Foldable.fold ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$
      -- Don't include this if the must set is empty
      [Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set a) -> Term (Set a) -> Term Bool
forall s.
(HasSpec s, Ord s) =>
Term (Set s) -> Term (Set s) -> Term Bool
subset_ (Set a -> Term (Set a)
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Set a
m) Term (Set a)
s | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
m]
        [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [ Term (Set a) -> (Term a -> Pred) -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> (Term a -> Pred) -> Pred
forAll Term (Set a)
s (\Term a
e -> Term a -> Spec a -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies Term a
e Spec a
es)
           , Term Integer -> Spec Integer -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (Set a) -> Term Integer
forall s. (HasSpec s, Ord s) => Term (Set s) -> Term Integer
size_ Term (Set a)
s) Spec Integer
size
           ]

  guardTypeSpec :: TypeSpec (Set a) -> Spec (Set a)
guardTypeSpec = TypeSpec (Set a) -> Spec (Set a)
SetSpec a -> Spec (Set a)
forall a. (HasSpec a, Ord a) => SetSpec a -> Spec (Set a)
guardSetSpec

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Set a) -> GenT m (Set a)
genFromTypeSpec (SetSpec Set a
must Spec a
e Spec Integer
_)
    | (a -> Bool) -> Set a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
`conformsToSpec` Spec a
e)) Set a
must =
        NonEmpty String -> GenT m (Set a)
forall a. HasCallStack => NonEmpty String -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE
          ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
              [ String
"Failed to generate set"
              , String
"Some element in the must set does not conform to the elem specification"
              , String
"Unconforming elements from the must set:"
              , [String] -> String
unlines ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\a
x -> String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x) ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
`conformsToSpec` Spec a
e)) (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
must)))
              , String
"Element Specifcation"
              , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
e
              ]
          )
  -- Special case when elemS is a MemberSpec.
  -- Just union 'must' with enough elements of 'xs' to meet  'szSpec'
  genFromTypeSpec (SetSpec Set a
must (MemberSpec NonEmpty a
xs) Spec Integer
szSpec) = do
    let szSpec' :: Spec Integer
szSpec' = Spec Integer
szSpec Spec Integer -> Spec Integer -> Spec Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Spec Integer
geqSpec (Set a -> Integer
forall a. Set a -> Integer
setSize Set a
must) -- <> maxSpec (cardinality elemS)
    [a]
choices <- Gen [a] -> GenT m [a]
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (Gen [a] -> GenT m [a]) -> Gen [a] -> GenT m [a]
forall a b. (a -> b) -> a -> b
$ [a] -> Gen [a]
forall a. [a] -> Gen [a]
shuffle (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
xs [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
must)
    Int
size <- Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> GenT m Integer -> GenT m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec Integer -> GenT m Integer
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec Integer
szSpec'
    let additions :: Set a
additions = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList ([a] -> Set a) -> [a] -> Set a
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take (Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Set a -> Int
forall a. Set a -> Int
Set.size Set a
must) [a]
choices
    Set a -> GenT m (Set a)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set a
must Set a
additions)
  genFromTypeSpec (SetSpec Set a
must Spec a
elemS Spec Integer
szSpec) = do
    let szSpec' :: Spec Integer
szSpec' = Spec Integer
szSpec Spec Integer -> Spec Integer -> Spec Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Spec Integer
geqSpec (Set a -> Integer
forall a. Set a -> Integer
setSize Set a
must) -- <> maxSpec (cardinality elemS)
    Integer
sizecount <-
      String -> GenT m Integer -> GenT m Integer
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"Choose a size for the Set to be generated" (GenT m Integer -> GenT m Integer)
-> GenT m Integer -> GenT m Integer
forall a b. (a -> b) -> a -> b
$
        Spec Integer -> GenT m Integer
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec Integer
szSpec'
    let targetSize :: Integer
targetSize = Integer
sizecount Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Set a -> Integer
forall a. Set a -> Integer
setSize Set a
must
    NonEmpty String -> GenT m (Set a) -> GenT m (Set a)
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
      ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [ String
"Choose size count = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
sizecount
          , String
"szSpec' = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec Integer -> String
forall a. Show a => a -> String
show Spec Integer
szSpec'
          , String
"Picking items not in must = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
must)
          , String
"that also meet the element test: "
          , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
elemS
          ]
      )
      (GenT m (Set a) -> GenT m (Set a))
-> GenT m (Set a) -> GenT m (Set a)
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> Set a -> GenT m (Set a)
go Int
100 Integer
targetSize Set a
must
    where
      go :: Int -> Integer -> Set a -> GenT m (Set a)
go Int
_ Integer
n Set a
s | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = Set a -> GenT m (Set a)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Set a
s
      go Int
tries Integer
n Set a
s = do
        a
e <-
          NonEmpty String -> GenT m a -> GenT m a
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
            ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
                [ String
"Generate set member at type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ forall t. Typeable t => String
showType @a
                , String
"  number of items starting with  = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Set a -> Int
forall a. Set a -> Int
Set.size Set a
must)
                , String
"  number of items left to pick   = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
                , String
"  number of items already picked = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Set a -> Int
forall a. Set a -> Int
Set.size Set a
s)
                ]
            )
            (GenT m a -> GenT m a) -> GenT m a -> GenT m a
forall a b. (a -> b) -> a -> b
$ GenMode -> GenT m a -> GenT m a
forall (m :: * -> *) a. GenMode -> GenT m a -> GenT m a
withMode GenMode
Strict
            (GenT m a -> GenT m a) -> GenT m a -> GenT m a
forall a b. (a -> b) -> a -> b
$ Int -> GenT m a -> (a -> Bool) -> GenT m a
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
Int -> GenT m a -> (a -> Bool) -> GenT m a
suchThatWithTryT Int
tries (Spec a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec a
elemS) (a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set a
s)

        Int -> Integer -> Set a -> GenT m (Set a)
go Int
tries (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
e Set a
s)

-- ========== Pairs example =======================

pattern Pair ::
  forall c. () => forall a b. (c ~ (a, b), HasSpec a, HasSpec b) => Term a -> Term b -> Term c
pattern $mPair :: forall {r} {c}.
Term c
-> (forall {a} {b}.
    (c ~ (a, b), HasSpec a, HasSpec b) =>
    Term a -> Term b -> r)
-> ((# #) -> r)
-> r
Pair x y <- App (getWitness -> Just PairW) (x :> y :> Nil)

data PairSym (dom :: [Type]) rng where
  FstW :: PairSym '[(a, b)] a
  SndW :: PairSym '[(a, b)] b
  PairW :: PairSym '[a, b] (a, b)

deriving instance Eq (PairSym dom rng)

instance Show (PairSym dom rng) where show :: PairSym dom rng -> String
show = PairSym dom rng -> String
forall (dom :: [*]) rng. PairSym dom rng -> String
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
Syntax t =>
t dom rng -> String
name

instance Syntax PairSym where
  name :: forall (dom :: [*]) rng. PairSym dom rng -> String
name PairSym dom rng
FstW = String
"fst_"
  name PairSym dom rng
SndW = String
"snd_"
  name PairSym dom rng
PairW = String
"pair_"
  inFix :: forall (dom :: [*]) rng. PairSym dom rng -> Bool
inFix PairSym dom rng
_ = Bool
False

instance Semantics PairSym where
  semantics :: forall (d :: [*]) r. PairSym d r -> FunTy d r
semantics PairSym d r
FstW = FunTy d r
(r, b) -> r
forall a b. (a, b) -> a
fst
  semantics PairSym d r
SndW = FunTy d r
(a, r) -> r
forall a b. (a, b) -> b
snd
  semantics PairSym d r
PairW = (,)
  rewriteRules :: forall (ds :: [*]) rng.
(TypeList ds, Typeable ds, HasSpec rng, All HasSpec ds) =>
PairSym ds rng
-> List Term ds
-> Evidence (Typeable rng, Eq rng, Show rng)
-> Maybe (Term rng)
rewriteRules PairSym ds rng
FstW (Pair Term a
x Term b
_ :> List Term as1
Nil) Evidence (Typeable rng, Eq rng, Show rng)
Evidence = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just Term rng
Term a
x
  rewriteRules PairSym ds rng
SndW (Pair Term a
_ Term b
y :> List Term as1
Nil) Evidence (Typeable rng, Eq rng, Show rng)
Evidence = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just Term rng
Term b
y
  rewriteRules PairSym ds rng
t List Term ds
l Evidence (Typeable rng, Eq rng, Show rng)
Evidence = rng -> Term rng
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (rng -> Term rng) -> Maybe rng -> Maybe (Term rng)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: [*] -> * -> *) (ds :: [*]) rng.
(Typeable rng, Eq rng, Show rng, Semantics t) =>
FunTy ds rng -> List Term ds -> Maybe rng
applyFunSym @PairSym (PairSym ds rng -> FunTy ds rng
forall (d :: [*]) r. PairSym d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics PairSym ds rng
t) List Term ds
l

instance Logic PairSym where
  propagateTypeSpec :: forall (as :: [*]) b a.
(AppRequires PairSym as b, HasSpec a) =>
PairSym as b -> ListCtx as (HOLE a) -> TypeSpec b -> [b] -> Spec a
propagateTypeSpec PairSym as b
FstW (Unary HOLE a a
HOLE) TypeSpec b
ts [b]
cant = TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec a -> Spec a) -> TypeSpec a -> Spec a
forall a b. (a -> b) -> a -> b
$ Spec b -> Spec b -> PairSpec b b
forall a b. Spec a -> Spec b -> PairSpec a b
Cartesian (TypeSpec b -> [b] -> Spec b
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec TypeSpec b
ts [b]
cant) Spec b
forall a. Spec a
TrueSpec
  propagateTypeSpec PairSym as b
SndW (Unary HOLE a a
HOLE) TypeSpec b
ts [b]
cant = TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec a -> Spec a) -> TypeSpec a -> Spec a
forall a b. (a -> b) -> a -> b
$ Spec a -> Spec b -> PairSpec a b
forall a b. Spec a -> Spec b -> PairSpec a b
Cartesian Spec a
forall a. Spec a
TrueSpec (TypeSpec b -> [b] -> Spec b
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec TypeSpec b
ts [b]
cant)
  propagateTypeSpec PairSym as b
PairW (x
a :|> HOLE a b
HOLE) sc :: TypeSpec b
sc@(Cartesian Spec x
sa Spec a
sb) [b]
cant
    | x
a x -> Spec x -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
`conformsToSpec` Spec x
sa = Spec a
sb Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> (a -> Spec a) -> [a] -> Spec a
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> Spec a
forall a. HasSpec a => a -> Spec a
notEqualSpec (x -> [(x, a)] -> [a]
forall a1 a2. Eq a1 => a1 -> [(a1, a2)] -> [a2]
sameFst x
a [b]
[(x, a)]
cant)
    | Bool
otherwise =
        NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec
          ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
              [String
"propagate (pair_ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" HOLE) has conformance failure on a", Spec b -> String
forall a. Show a => a -> String
show (TypeSpec b -> [b] -> Spec b
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec TypeSpec b
sc [b]
cant)]
          )
  propagateTypeSpec PairSym as b
PairW (HOLE a b
HOLE :<| x
b) sc :: TypeSpec b
sc@(Cartesian Spec a
sa Spec x
sb) [b]
cant
    | x
b x -> Spec x -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
`conformsToSpec` Spec x
sb = Spec a
sa Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> (a -> Spec a) -> [a] -> Spec a
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> Spec a
forall a. HasSpec a => a -> Spec a
notEqualSpec (x -> [(a, x)] -> [a]
forall a1 a2. Eq a1 => a1 -> [(a2, a1)] -> [a2]
sameSnd x
b [b]
[(a, x)]
cant)
    | Bool
otherwise =
        NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec
          ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
              [String
"propagate (pair_ HOLE " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") has conformance failure on b", Spec b -> String
forall a. Show a => a -> String
show (TypeSpec b -> [b] -> Spec b
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec TypeSpec b
sc [b]
cant)]
          )

  propagateMemberSpec :: forall (as :: [*]) b a.
(AppRequires PairSym as b, HasSpec a) =>
PairSym as b -> ListCtx as (HOLE a) -> NonEmpty b -> Spec a
propagateMemberSpec PairSym as b
FstW (Unary HOLE a a
HOLE) NonEmpty b
es = TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec a -> Spec a) -> TypeSpec a -> Spec a
forall a b. (a -> b) -> a -> b
$ Spec b -> Spec b -> PairSpec b b
forall a b. Spec a -> Spec b -> PairSpec a b
Cartesian (NonEmpty b -> Spec b
forall a. NonEmpty a -> Spec a
MemberSpec NonEmpty b
es) Spec b
forall a. Spec a
TrueSpec
  propagateMemberSpec PairSym as b
SndW (Unary HOLE a a
HOLE) NonEmpty b
es = TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec a -> Spec a) -> TypeSpec a -> Spec a
forall a b. (a -> b) -> a -> b
$ Spec a -> Spec b -> PairSpec a b
forall a b. Spec a -> Spec b -> PairSpec a b
Cartesian Spec a
forall a. Spec a
TrueSpec (NonEmpty b -> Spec b
forall a. NonEmpty a -> Spec a
MemberSpec NonEmpty b
es)
  propagateMemberSpec PairSym as b
PairW (x
a :|> HOLE a b
HOLE) NonEmpty b
es =
    case ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub (x -> [(x, a)] -> [a]
forall a1 a2. Eq a1 => a1 -> [(a1, a2)] -> [a2]
sameFst x
a (NonEmpty (x, a) -> [(x, a)]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
NonEmpty (x, a)
es))) of
      (a
w : [a]
ws) -> NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec (a
w a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
ws)
      [] ->
        NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty String -> Spec a) -> NonEmpty String -> Spec a
forall a b. (a -> b) -> a -> b
$
          [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
            [ String
"propagate (pair_ HOLE " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") on (MemberSpec " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [b] -> String
forall a. Show a => a -> String
show (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)
            , String
"Where " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" does not appear as the fst component of anything in the MemberSpec."
            ]
  propagateMemberSpec PairSym as b
PairW (HOLE a b
HOLE :<| x
b) NonEmpty b
es =
    case ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub (x -> [(a, x)] -> [a]
forall a1 a2. Eq a1 => a1 -> [(a2, a1)] -> [a2]
sameSnd x
b (NonEmpty (a, x) -> [(a, x)]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
NonEmpty (a, x)
es))) of
      (a
w : [a]
ws) -> NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec (a
w a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
ws)
      [] ->
        NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty String -> Spec a) -> NonEmpty String -> Spec a
forall a b. (a -> b) -> a -> b
$
          [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
            [ String
"propagate (pair_ HOLE " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") on (MemberSpec " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [b] -> String
forall a. Show a => a -> String
show (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)
            , String
"Where " String -> ShowS
forall a. [a] -> [a] -> [a]
++ x -> String
forall a. Show a => a -> String
show x
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" does not appear as the snd component of anything in the MemberSpec."
            ]

sameFst :: Eq a1 => a1 -> [(a1, a2)] -> [a2]
sameFst :: forall a1 a2. Eq a1 => a1 -> [(a1, a2)] -> [a2]
sameFst a1
a [(a1, a2)]
ps = [a2
b | (a1
a', a2
b) <- [(a1, a2)]
ps, a1
a a1 -> a1 -> Bool
forall a. Eq a => a -> a -> Bool
== a1
a']

sameSnd :: Eq a1 => a1 -> [(a2, a1)] -> [a2]
sameSnd :: forall a1 a2. Eq a1 => a1 -> [(a2, a1)] -> [a2]
sameSnd a1
b [(a2, a1)]
ps = [a2
a | (a2
a, a1
b') <- [(a2, a1)]
ps, a1
b a1 -> a1 -> Bool
forall a. Eq a => a -> a -> Bool
== a1
b']

fst_ :: (HasSpec a, HasSpec b) => Term (a, b) -> Term a
fst_ :: forall a b. (HasSpec a, HasSpec b) => Term (a, b) -> Term a
fst_ Term (a, b)
x = PairSym '[(a, b)] a -> List Term '[(a, b)] -> Term a
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App PairSym '[(a, b)] a
forall a b. PairSym '[(a, b)] a
FstW (Term (a, b)
x Term (a, b) -> List Term '[] -> List Term '[(a, b)]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

snd_ :: (HasSpec a, HasSpec b) => Term (a, b) -> Term b
snd_ :: forall a b. (HasSpec a, HasSpec b) => Term (a, b) -> Term b
snd_ Term (a, b)
x = PairSym '[(a, b)] b -> List Term '[(a, b)] -> Term b
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App PairSym '[(a, b)] b
forall b b. PairSym '[(b, b)] b
SndW (Term (a, b)
x Term (a, b) -> List Term '[] -> List Term '[(a, b)]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

pair_ :: (HasSpec a, HasSpec b) => Term a -> Term b -> Term (a, b)
pair_ :: forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> Term (a, b)
pair_ Term a
a Term b
b = PairSym '[a, b] (a, b) -> List Term '[a, b] -> Term (a, b)
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App PairSym '[a, b] (a, b)
forall b a. PairSym '[b, a] (b, a)
PairW (Term a
a Term a -> List Term '[b] -> List Term '[a, b]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term b
b Term b -> List Term '[] -> List Term '[b]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

-- ========== The Pair (a,b) HasSpec instance

data PairSpec a b = Cartesian (Spec a) (Spec b)

instance (HasSpec a, HasSpec b) => Show (PairSpec a b) where
  show :: PairSpec a b -> String
show (Cartesian Spec a
l Spec b
r) = String
"(Cartesian " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec b -> String
forall a. Show a => a -> String
show Spec b
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"))"

instance (HasSpec a, HasSpec b) => Semigroup (PairSpec a b) where
  (Cartesian Spec a
x Spec b
y) <> :: PairSpec a b -> PairSpec a b -> PairSpec a b
<> (Cartesian Spec a
a Spec b
b) = Spec a -> Spec b -> PairSpec a b
forall a b. Spec a -> Spec b -> PairSpec a b
Cartesian (Spec a
x Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> Spec a
a) (Spec b
y Spec b -> Spec b -> Spec b
forall a. Semigroup a => a -> a -> a
<> Spec b
b)

instance (HasSpec a, HasSpec b) => Monoid (PairSpec a b) where mempty :: PairSpec a b
mempty = Spec a -> Spec b -> PairSpec a b
forall a b. Spec a -> Spec b -> PairSpec a b
Cartesian Spec a
forall a. Monoid a => a
mempty Spec b
forall a. Monoid a => a
mempty

guardPair :: forall a b. (HasSpec a, HasSpec b) => Spec a -> Spec b -> Spec (a, b)
guardPair :: forall a b.
(HasSpec a, HasSpec b) =>
Spec a -> Spec b -> Spec (a, b)
guardPair Spec a
specA Spec b
specB = Spec a
-> Spec b -> (Spec a -> Spec b -> Spec (a, b)) -> Spec (a, b)
forall a b c.
Spec a -> Spec b -> (Spec a -> Spec b -> Spec c) -> Spec c
handleErrors Spec a
specA Spec b
specB (\Spec a
s Spec b
t -> TypeSpec (a, b) -> Spec (a, b)
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Spec a -> Spec b -> PairSpec a b
forall a b. Spec a -> Spec b -> PairSpec a b
Cartesian Spec a
s Spec b
t))

instance (HasSpec a, HasSpec b) => HasSpec (a, b) where
  type TypeSpec (a, b) = PairSpec a b

  anySpec :: TypeSpec (a, b)
anySpec = Spec a -> Spec b -> PairSpec a b
forall a b. Spec a -> Spec b -> PairSpec a b
Cartesian Spec a
forall a. Monoid a => a
mempty Spec b
forall a. Monoid a => a
mempty

  combineSpec :: TypeSpec (a, b) -> TypeSpec (a, b) -> Spec (a, b)
combineSpec (Cartesian Spec a
a Spec b
b) (Cartesian Spec a
a' Spec b
b') = Spec a -> Spec b -> Spec (a, b)
forall a b.
(HasSpec a, HasSpec b) =>
Spec a -> Spec b -> Spec (a, b)
guardPair (Spec a
a Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> Spec a
a') (Spec b
b Spec b -> Spec b -> Spec b
forall a. Semigroup a => a -> a -> a
<> Spec b
b')

  conformsTo :: HasCallStack => (a, b) -> TypeSpec (a, b) -> Bool
conformsTo (a
a, b
b) (Cartesian Spec a
sa Spec b
sb) = a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec a
a Spec a
sa Bool -> Bool -> Bool
&& b -> Spec b -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec b
b Spec b
sb

  guardTypeSpec :: TypeSpec (a, b) -> Spec (a, b)
guardTypeSpec (Cartesian Spec a
x Spec b
y) = Spec a -> Spec b -> Spec (a, b)
forall a b.
(HasSpec a, HasSpec b) =>
Spec a -> Spec b -> Spec (a, b)
guardPair Spec a
x Spec b
y

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (a, b) -> GenT m (a, b)
genFromTypeSpec (Cartesian Spec a
sa Spec b
sb) = (,) (a -> b -> (a, b)) -> GenT m a -> GenT m (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec a
sa GenT m (b -> (a, b)) -> GenT m b -> GenT m (a, b)
forall a b. GenT m (a -> b) -> GenT m a -> GenT m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Spec b -> GenT m b
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec b
sb

  toPreds :: Term (a, b) -> TypeSpec (a, b) -> Pred
toPreds Term (a, b)
x (Cartesian Spec a
sf Spec b
ss) =
    Term a -> Spec a -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (a, b) -> Term a
forall a b. (HasSpec a, HasSpec b) => Term (a, b) -> Term a
fst_ Term (a, b)
x) Spec a
sf
      Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term b -> Spec b -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (a, b) -> Term b
forall a b. (HasSpec a, HasSpec b) => Term (a, b) -> Term b
snd_ Term (a, b)
x) Spec b
ss

-- ========== Either example =======================

data EitherSym (dom :: [Type]) rng where
  LeftW :: EitherSym '[a] (Either a b)
  RightW :: EitherSym '[b] (Either a b)

deriving instance Eq (EitherSym dom rng)

instance Show (EitherSym dom rng) where show :: EitherSym dom rng -> String
show = EitherSym dom rng -> String
forall (dom :: [*]) rng. EitherSym dom rng -> String
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
Syntax t =>
t dom rng -> String
name

instance Syntax EitherSym where
  name :: forall (dom :: [*]) rng. EitherSym dom rng -> String
name EitherSym dom rng
LeftW = String
"left_"
  name EitherSym dom rng
RightW = String
"right_"
  inFix :: forall (dom :: [*]) rng. EitherSym dom rng -> Bool
inFix EitherSym dom rng
_ = Bool
False

instance Semantics EitherSym where
  semantics :: forall (d :: [*]) r. EitherSym d r -> FunTy d r
semantics EitherSym d r
LeftW = FunTy d r
a -> Either a b
forall a b. a -> Either a b
Left
  semantics EitherSym d r
RightW = FunTy d r
b -> Either a b
forall a b. b -> Either a b
Right

instance Logic EitherSym where
  propagateTypeSpec :: forall (as :: [*]) b a.
(AppRequires EitherSym as b, HasSpec a) =>
EitherSym as b
-> ListCtx as (HOLE a) -> TypeSpec b -> [b] -> Spec a
propagateTypeSpec EitherSym as b
LeftW (Unary HOLE a a
HOLE) (SumSpec Spec a
sl Spec b
_) [b]
cant = Spec a
sl Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> (a -> Spec a) -> [a] -> Spec a
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> Spec a
forall a. HasSpec a => a -> Spec a
notEqualSpec [a
a | Left a
a <- [b]
cant]
  propagateTypeSpec EitherSym as b
RightW (Unary HOLE a a
HOLE) (SumSpec Spec a
_ Spec a
sr) [b]
cant = Spec a
sr Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> (a -> Spec a) -> [a] -> Spec a
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> Spec a
forall a. HasSpec a => a -> Spec a
notEqualSpec [a
a | Right a
a <- [b]
cant]

  propagateMemberSpec :: forall (as :: [*]) b a.
(AppRequires EitherSym as b, HasSpec a) =>
EitherSym as b -> ListCtx as (HOLE a) -> NonEmpty b -> Spec a
propagateMemberSpec EitherSym as b
LeftW (Unary HOLE a a
HOLE) NonEmpty b
es =
    case [a
a | Left a
a <- NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es] of
      (a
x : [a]
xs) -> NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec (a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
xs)
      [] ->
        NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty String -> Spec a) -> NonEmpty String -> Spec a
forall a b. (a -> b) -> a -> b
$
          String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> NonEmpty String) -> String -> NonEmpty String
forall a b. (a -> b) -> a -> b
$
            String
"propMemberSpec (left_ HOLE) on (MemberSpec es) with no Left in es: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [b] -> String
forall a. Show a => a -> String
show (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)
  propagateMemberSpec EitherSym as b
RightW (Unary HOLE a a
HOLE) NonEmpty b
es =
    case [a
a | Right a
a <- NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es] of
      (a
x : [a]
xs) -> NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec (a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
xs)
      [] ->
        NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty String -> Spec a) -> NonEmpty String -> Spec a
forall a b. (a -> b) -> a -> b
$
          String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> NonEmpty String) -> String -> NonEmpty String
forall a b. (a -> b) -> a -> b
$
            String
"propagate (Right HOLE) on (MemberSpec es) with no Right in es: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [b] -> String
forall a. Show a => a -> String
show (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)

left_ :: (HasSpec a, HasSpec b) => Term a -> Term (Either a b)
left_ :: forall a b. (HasSpec a, HasSpec b) => Term a -> Term (Either a b)
left_ Term a
x = EitherSym '[a] (Either a b) -> List Term '[a] -> Term (Either a b)
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App EitherSym '[a] (Either a b)
forall b a. EitherSym '[b] (Either b a)
LeftW (Term a
x Term a -> List Term '[] -> List Term '[a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

right_ :: (HasSpec a, HasSpec b) => Term b -> Term (Either a b)
right_ :: forall a b. (HasSpec a, HasSpec b) => Term b -> Term (Either a b)
right_ Term b
x = EitherSym '[b] (Either a b) -> List Term '[b] -> Term (Either a b)
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App EitherSym '[b] (Either a b)
forall b a. EitherSym '[b] (Either a b)
RightW (Term b
x Term b -> List Term '[] -> List Term '[b]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

-- ========== The Either HasSpec instance

data SumSpec a b = SumSpec a b

deriving instance (Eq a, Eq b) => Eq (SumSpec a b)

deriving instance (Show a, Show b) => Show (SumSpec a b)

guardSum :: forall a b. (HasSpec a, HasSpec b) => Spec a -> Spec b -> Spec (Either a b)
guardSum :: forall a b.
(HasSpec a, HasSpec b) =>
Spec a -> Spec b -> Spec (Either a b)
guardSum (ErrorSpec NonEmpty String
es) (ErrorSpec NonEmpty String
fs) = NonEmpty String -> Spec (Either a b)
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty String
es NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
fs)
guardSum (ErrorSpec NonEmpty String
es) Spec b
_ = NonEmpty String -> Spec (Either a b)
forall a. NonEmpty String -> Spec a
ErrorSpec (String -> NonEmpty String -> NonEmpty String
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons String
"sum error on left" NonEmpty String
es)
guardSum Spec a
_ (ErrorSpec NonEmpty String
es) = NonEmpty String -> Spec (Either a b)
forall a. NonEmpty String -> Spec a
ErrorSpec (String -> NonEmpty String -> NonEmpty String
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons String
"sum error on right" NonEmpty String
es)
guardSum Spec a
s Spec b
s' = TypeSpec (Either a b) -> Spec (Either a b)
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec (Either a b) -> Spec (Either a b))
-> TypeSpec (Either a b) -> Spec (Either a b)
forall a b. (a -> b) -> a -> b
$ Spec a -> Spec b -> SumSpec (Spec a) (Spec b)
forall a b. a -> b -> SumSpec a b
SumSpec Spec a
s Spec b
s'

instance (HasSpec a, HasSpec b) => HasSpec (Either a b) where
  type TypeSpec (Either a b) = SumSpec (Spec a) (Spec b)

  anySpec :: TypeSpec (Either a b)
anySpec = Spec a -> Spec b -> SumSpec (Spec a) (Spec b)
forall a b. a -> b -> SumSpec a b
SumSpec Spec a
forall a. Monoid a => a
mempty Spec b
forall a. Monoid a => a
mempty

  combineSpec :: TypeSpec (Either a b) -> TypeSpec (Either a b) -> Spec (Either a b)
combineSpec (SumSpec Spec a
a Spec b
b) (SumSpec Spec a
c Spec b
d) = Spec a -> Spec b -> Spec (Either a b)
forall a b.
(HasSpec a, HasSpec b) =>
Spec a -> Spec b -> Spec (Either a b)
guardSum (Spec a
a Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> Spec a
c) (Spec b
b Spec b -> Spec b -> Spec b
forall a. Semigroup a => a -> a -> a
<> Spec b
d)

  conformsTo :: HasCallStack => Either a b -> TypeSpec (Either a b) -> Bool
conformsTo (Left a
a) (SumSpec Spec a
sa Spec b
_) = a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec a
a Spec a
sa
  conformsTo (Right b
b) (SumSpec Spec a
_ Spec b
sb) = b -> Spec b -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec b
b Spec b
sb

  toPreds :: Term (Either a b) -> TypeSpec (Either a b) -> Pred
toPreds Term (Either a b)
x (SumSpec Spec a
a Spec b
b) = Term (Either a b) -> Binder a -> Binder b -> Pred
forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
Case Term (Either a b)
x ((Term a -> Pred) -> Binder a
forall a. HasSpec a => (Term a -> Pred) -> Binder a
bind ((Term a -> Pred) -> Binder a) -> (Term a -> Pred) -> Binder a
forall a b. (a -> b) -> a -> b
$ \Term a
y -> Term a -> Spec a -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies Term a
y Spec a
a) ((Term b -> Pred) -> Binder b
forall a. HasSpec a => (Term a -> Pred) -> Binder a
bind ((Term b -> Pred) -> Binder b) -> (Term b -> Pred) -> Binder b
forall a b. (a -> b) -> a -> b
$ \Term b
y -> Term b -> Spec b -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies Term b
y Spec b
b)

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Either a b) -> GenT m (Either a b)
genFromTypeSpec (SumSpec (Spec a -> Spec a
forall a. HasSpec a => Spec a -> Spec a
simplifySpec -> Spec a
sa) (Spec b -> Spec b
forall a. HasSpec a => Spec a -> Spec a
simplifySpec -> Spec b
sb))
    | Bool
emptyA, Bool
emptyB = String -> GenT m (Either a b)
forall (m :: * -> *) a. MonadGenError m => String -> m a
genError String
"genFromTypeSpec @SumSpec: empty"
    | Bool
emptyA = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> GenT m b -> GenT m (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec b -> GenT m b
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec b
sb
    | Bool
emptyB = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> GenT m a -> GenT m (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec a
sa
    | Bool
otherwise = [GenT GE (Either a b)] -> GenT m (Either a b)
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
[GenT GE a] -> GenT m a
oneofT [a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> GenT GE a -> GenT GE (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec a
sa, b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> GenT GE b -> GenT GE (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec b -> GenT GE b
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec b
sb]
    where
      emptyA :: Bool
emptyA = Spec a -> Bool
forall a. Spec a -> Bool
isErrorLike Spec a
sa
      emptyB :: Bool
emptyB = Spec b -> Bool
forall a. Spec a -> Bool
isErrorLike Spec b
sb

-- ========== List example ===================

data ListSym (dom :: [Type]) rng where
  ElemW :: Eq a => ListSym [a, [a]] Bool
  LengthW :: ListSym '[[a]] Integer

instance Syntax ListSym where
  name :: forall (dom :: [*]) rng. ListSym dom rng -> String
name ListSym dom rng
ElemW = String
"elem_"
  name ListSym dom rng
LengthW = String
"length_"
  inFix :: forall (dom :: [*]) rng. ListSym dom rng -> Bool
inFix ListSym dom rng
_ = Bool
False

instance Semantics ListSym where
  semantics :: forall (d :: [*]) r. ListSym d r -> FunTy d r
semantics ListSym d r
ElemW = FunTy d r
a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem
  semantics ListSym d r
LengthW = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> ([a] -> Int) -> [a] -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length

-- =========================================================================
-- User Facing functions
-- ====================================================================

-- | Generalize `genFromTypeSpec` from `TypeSpec t` to `Spec t`
--   Generate a value that satisfies the spec. This function can fail if the
--   spec is inconsistent, there is a dependency error, or if the underlying
--   generators are not flexible enough.
genFromSpecT ::
  forall a m. (HasCallStack, HasSpec a, MonadGenError m) => Spec a -> GenT m a
genFromSpecT :: forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT (Spec a -> Spec a
forall a. HasSpec a => Spec a -> Spec a
simplifySpec -> Spec a
spec) = case Spec a
spec of
  MemberSpec NonEmpty a
as -> String -> GenT m a -> GenT m a
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain (String
"genFromSpecT on spec" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
spec) (GenT m a -> GenT m a) -> GenT m a -> GenT m a
forall a b. (a -> b) -> a -> b
$ Gen a -> GenT m a
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen ([a] -> Gen a
forall a. HasCallStack => [a] -> Gen a
elements (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as))
  Spec a
TrueSpec -> Spec a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT (TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec a -> Spec a) -> TypeSpec a -> Spec a
forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => TypeSpec a
anySpec @a)
  SuspendedSpec Var a
x Pred
p
    -- NOTE: If `x` isn't free in `p` we still have to try to generate things
    -- from `p` to make sure `p` is sat and then we can throw it away. A better
    -- approach would be to only do this in the case where we don't know if `p`
    -- is sat. The proper way to implement such a sat check is to remove
    -- sat-but-unnecessary variables in the optimiser.
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x Name -> Pred -> Bool
forall a. HasVariables a => Name -> a -> Bool
`appearsIn` Pred
p -> do
        !Env
_ <- Env -> Pred -> GenT m Env
forall (m :: * -> *). MonadGenError m => Env -> Pred -> GenT m Env
genFromPreds Env
forall a. Monoid a => a
mempty Pred
p
        Spec a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec a
forall a. Spec a
TrueSpec
    | Bool
otherwise -> do
        Env
env <- Env -> Pred -> GenT m Env
forall (m :: * -> *). MonadGenError m => Env -> Pred -> GenT m Env
genFromPreds Env
forall a. Monoid a => a
mempty Pred
p
        Env -> Var a -> GenT m a
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
Env -> Var a -> m a
findEnv Env
env Var a
x
  TypeSpec TypeSpec a
s [a]
cant -> do
    GenMode
mode <- GenT m GenMode
forall (m :: * -> *). Applicative m => GenT m GenMode
getMode
    NonEmpty String -> GenT m a -> GenT m a
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
      ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [ String
"genFromSpecT on (TypeSpec tspec cant) at type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ forall t. Typeable t => String
showType @a
          , String
"tspec = "
          , TypeSpec a -> String
forall a. Show a => a -> String
show TypeSpec a
s
          , String
"cant = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show [a]
cant
          , String
"with mode " String -> ShowS
forall a. [a] -> [a] -> [a]
++ GenMode -> String
forall a. Show a => a -> String
show GenMode
mode
          ]
      )
      (GenT m a -> GenT m a) -> GenT m a -> GenT m a
forall a b. (a -> b) -> a -> b
$
      -- TODO: we could consider giving `cant` as an argument to `genFromTypeSpec` if this
      -- starts giving us trouble.
      TypeSpec a -> GenT m a
forall a (m :: * -> *).
(HasSpec a, HasCallStack, MonadGenError m) =>
TypeSpec a -> GenT m a
forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec a -> GenT m a
genFromTypeSpec TypeSpec a
s GenT m a -> (a -> Bool) -> GenT m a
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
GenT m a -> (a -> Bool) -> GenT m a
`suchThatT` (a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
cant)
  ErrorSpec NonEmpty String
e -> NonEmpty String -> GenT m a
forall a. HasCallStack => NonEmpty String -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE NonEmpty String
e

-- | A version of `genFromSpecT` that simply errors if the generator fails
genFromSpec :: forall a. (HasCallStack, HasSpec a) => Spec a -> Gen a
genFromSpec :: forall a. (HasCallStack, HasSpec a) => Spec a -> Gen a
genFromSpec Spec a
spec = do
  Either (NonEmpty (NonEmpty String)) a
res <- GenT GE a -> Gen (Either (NonEmpty (NonEmpty String)) a)
forall a. GenT GE a -> Gen (Either (NonEmpty (NonEmpty String)) a)
catchGen (GenT GE a -> Gen (Either (NonEmpty (NonEmpty String)) a))
-> GenT GE a -> Gen (Either (NonEmpty (NonEmpty String)) a)
forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT @a @GE Spec a
spec
  (NonEmpty (NonEmpty String) -> Gen a)
-> (a -> Gen a) -> Either (NonEmpty (NonEmpty String)) a -> Gen a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Gen a
forall a. HasCallStack => String -> a
error (String -> Gen a)
-> (NonEmpty (NonEmpty String) -> String)
-> NonEmpty (NonEmpty String)
-> Gen a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'\n' Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS
-> (NonEmpty (NonEmpty String) -> String)
-> NonEmpty (NonEmpty String)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (NonEmpty String) -> String
catMessages) a -> Gen a
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Either (NonEmpty (NonEmpty String)) a
res

-- | A version of `genFromSpecT` that runs in the IO monad. Good for debugging.
debugSpec :: forall a. HasSpec a => Spec a -> IO ()
debugSpec :: forall a. HasSpec a => Spec a -> IO ()
debugSpec Spec a
spec = do
  GE a
ans <- Gen (GE a) -> IO (GE a)
forall a. Gen a -> IO a
generate (Gen (GE a) -> IO (GE a)) -> Gen (GE a) -> IO (GE a)
forall a b. (a -> b) -> a -> b
$ GenT GE (GE a) -> Gen (GE a)
forall a. GenT GE a -> Gen a
genFromGenT (GenT GE (GE a) -> Gen (GE a)) -> GenT GE (GE a) -> Gen (GE a)
forall a b. (a -> b) -> a -> b
$ GenT GE a -> GenT GE (GE a)
forall (m :: * -> *) x.
MonadGenError m =>
GenT GE x -> GenT m (GE x)
inspect (Spec a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec a
spec)
  let f :: NonEmpty String -> IO ()
f NonEmpty String
x = String -> IO ()
putStrLn ([String] -> String
unlines (NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty String
x))
      ok :: a -> IO ()
ok a
x =
        if a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec a
x Spec a
spec
          then String -> IO ()
putStrLn String
"True"
          else String -> IO ()
putStrLn String
"False, perhaps there is an unsafeExists in the spec?"
  case GE a
ans of
    FatalError NonEmpty (NonEmpty String)
xs -> (NonEmpty String -> IO ()) -> NonEmpty (NonEmpty String) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ NonEmpty String -> IO ()
f NonEmpty (NonEmpty String)
xs
    GenError NonEmpty (NonEmpty String)
xs -> (NonEmpty String -> IO ()) -> NonEmpty (NonEmpty String) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ NonEmpty String -> IO ()
f NonEmpty (NonEmpty String)
xs
    Result a
x -> Spec a -> IO ()
forall a. Show a => a -> IO ()
print Spec a
spec IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Spec a -> IO ()
forall a. Show a => a -> IO ()
print (Spec a -> Spec a
forall a. HasSpec a => Spec a -> Spec a
simplifySpec Spec a
spec) IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> IO ()
forall a. Show a => a -> IO ()
print a
x IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> IO ()
ok a
x

-- | Generate a satisfying `Env` for a `p : Pred fn`. The `Env` contains values for
-- all the free variables in `flattenPred p`.
genFromPreds :: forall m. MonadGenError m => Env -> Pred -> GenT m Env
-- TODO: remove this once optimisePred does a proper fixpoint computation
genFromPreds :: forall (m :: * -> *). MonadGenError m => Env -> Pred -> GenT m Env
genFromPreds Env
env0 (Pred -> Pred
optimisePred (Pred -> Pred) -> (Pred -> Pred) -> Pred -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Pred
optimisePred -> Pred
preds) =
  {- explain1 (show $ "genFromPreds fails\nPreds are:" /> pretty preds) -} do
    -- NOTE: this is just lazy enough that the work of flattening,
    -- computing dependencies, and linearizing is memoized in
    -- properties that use `genFromPreds`.
    SolverPlan
plan <- GE SolverPlan -> GenT m SolverPlan
forall (m :: * -> *) r. MonadGenError m => GE r -> m r
runGE (GE SolverPlan -> GenT m SolverPlan)
-> GE SolverPlan -> GenT m SolverPlan
forall a b. (a -> b) -> a -> b
$ Pred -> GE SolverPlan
prepareLinearization Pred
preds
    Env -> SolverPlan -> GenT m Env
go Env
env0 SolverPlan
plan
  where
    go :: Env -> SolverPlan -> GenT m Env
    go :: Env -> SolverPlan -> GenT m Env
go Env
env SolverPlan
plan | SolverPlan -> Bool
isEmptyPlan SolverPlan
plan = Env -> GenT m Env
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
    go Env
env SolverPlan
plan = String -> GenT m Env -> GenT m Env
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain (Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Stepping the plan:" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc Any] -> Doc Any
forall ann. [Doc ann] -> Doc ann
vsep [Env -> Doc Any
forall ann. Env -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Env
env, SolverPlan -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. SolverPlan -> Doc ann
pretty (Env -> SolverPlan -> SolverPlan
substPlan Env
env SolverPlan
plan)]) (GenT m Env -> GenT m Env) -> GenT m Env -> GenT m Env
forall a b. (a -> b) -> a -> b
$ do
      (Env
env', SolverPlan
plan') <- Env -> SolverPlan -> GenT m (Env, SolverPlan)
forall (m :: * -> *).
MonadGenError m =>
Env -> SolverPlan -> GenT m (Env, SolverPlan)
stepPlan Env
env SolverPlan
plan
      Env -> SolverPlan -> GenT m Env
go Env
env' SolverPlan
plan'

-- =============================================================
-- Simplifcation
-- =============================================================

simplifySpec :: HasSpec a => Spec a -> Spec a
simplifySpec :: forall a. HasSpec a => Spec a -> Spec a
simplifySpec Spec a
spec = case Spec a -> Spec a
forall a. Spec a -> Spec a
regularizeNames Spec a
spec of
  SuspendedSpec Var a
x Pred
p ->
    let optP :: Pred
optP = Pred -> Pred
optimisePred Pred
p
     in GE (Spec a) -> Spec a
forall a. HasCallStack => GE (Spec a) -> Spec a
fromGESpec (GE (Spec a) -> Spec a) -> GE (Spec a) -> Spec a
forall a b. (a -> b) -> a -> b
$
          String -> GE (Spec a) -> GE (Spec a)
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain
            (String
"\nWhile calling simplifySpec on var " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var a -> String
forall a. Show a => a -> String
show Var a
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\noptP=\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pred -> String
forall a. Show a => a -> String
show Pred
optP String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n")
            (Var a -> Pred -> GE (Spec a)
forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpecSimplified Var a
x Pred
optP)
  MemberSpec NonEmpty a
xs -> NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec NonEmpty a
xs
  ErrorSpec NonEmpty String
es -> NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
es
  TypeSpec TypeSpec a
ts [a]
cant -> TypeSpec a -> [a] -> Spec a
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec TypeSpec a
ts [a]
cant
  Spec a
TrueSpec -> Spec a
forall a. Spec a
TrueSpec

-- | Turn 'GenError' into 'ErrorSpec', and FatalError into 'error'
fromGESpec :: HasCallStack => GE (Spec a) -> Spec a
fromGESpec :: forall a. HasCallStack => GE (Spec a) -> Spec a
fromGESpec GE (Spec a)
ge = case GE (Spec a)
ge of
  Result Spec a
s -> Spec a
s
  GenError NonEmpty (NonEmpty String)
xs -> NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty (NonEmpty String) -> NonEmpty String
catMessageList NonEmpty (NonEmpty String)
xs)
  FatalError NonEmpty (NonEmpty String)
es -> String -> Spec a
forall a. HasCallStack => String -> a
error (String -> Spec a) -> String -> Spec a
forall a b. (a -> b) -> a -> b
$ NonEmpty (NonEmpty String) -> String
catMessages NonEmpty (NonEmpty String)
es

------- Stages of simplifying -------------------------------

-- TODO: it might be necessary to run aggressiveInlining again after the let floating etc.
optimisePred :: Pred -> Pred
optimisePred :: Pred -> Pred
optimisePred Pred
p =
  Pred -> Pred
simplifyPred
    (Pred -> Pred) -> (Pred -> Pred) -> Pred -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasSpec Bool => Pred -> Pred
Pred -> Pred
letSubexpressionElimination
    (Pred -> Pred) -> (Pred -> Pred) -> Pred -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Pred
letFloating
    (Pred -> Pred) -> (Pred -> Pred) -> Pred -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Pred
aggressiveInlining
    (Pred -> Pred) -> (Pred -> Pred) -> Pred -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Pred
simplifyPred
    (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Pred
p

aggressiveInlining :: Pred -> Pred
aggressiveInlining :: Pred -> Pred
aggressiveInlining Pred
pred0
  | Bool
inlined = Pred -> Pred
aggressiveInlining Pred
pInlined
  | Bool
otherwise = Pred
pred0
  where
    (Pred
pInlined, Any Bool
inlined) = Writer Any Pred -> (Pred, Any)
forall w a. Writer w a -> (a, w)
runWriter (Writer Any Pred -> (Pred, Any)) -> Writer Any Pred -> (Pred, Any)
forall a b. (a -> b) -> a -> b
$ FreeVars -> [SubstEntry] -> Pred -> Writer Any Pred
go (Pred -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Pred
pred0) [] Pred
pred0

    underBinder :: FreeVars -> Var a -> a -> FreeVars
underBinder FreeVars
fvs Var a
x a
p = FreeVars
fvs FreeVars -> [Name] -> FreeVars
forall (t :: * -> *). Foldable t => FreeVars -> t Name -> FreeVars
`without` [Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x] FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> Name -> Int -> FreeVars
singleton (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x) (Name -> a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x) a
p)

    underBinderSub :: [SubstEntry] -> Var a -> [SubstEntry]
underBinderSub [SubstEntry]
sub Var a
x =
      [ Var a
x' Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
t
      | Var a
x' := Term a
t <- [SubstEntry]
sub
      , Maybe (a :~: a) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (a :~: a) -> Bool) -> Maybe (a :~: a) -> Bool
forall a b. (a -> b) -> a -> b
$ Var a -> Var a -> Maybe (a :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
x'
      ]

    -- NOTE: this is safe because we only use the `Subst` when it results in a literal so there
    -- is no risk of variable capture.
    goBinder :: FreeVars -> Subst -> Binder a -> Writer Any (Binder a)
    goBinder :: forall a.
FreeVars -> [SubstEntry] -> Binder a -> Writer Any (Binder a)
goBinder FreeVars
fvs [SubstEntry]
sub (Var a
x :-> Pred
p) = (Var a
x Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:->) (Pred -> Binder a)
-> Writer Any Pred -> WriterT Any Identity (Binder a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreeVars -> [SubstEntry] -> Pred -> Writer Any Pred
go (FreeVars -> Var a -> Pred -> FreeVars
forall {a} {a}.
(HasSpec a, HasVariables a) =>
FreeVars -> Var a -> a -> FreeVars
underBinder FreeVars
fvs Var a
x Pred
p) ([SubstEntry] -> Var a -> [SubstEntry]
forall {a}. Typeable a => [SubstEntry] -> Var a -> [SubstEntry]
underBinderSub [SubstEntry]
sub Var a
x) Pred
p

    -- Check that the name `n` is only ever used as the only variable
    -- in the expressions where it appears. This ensures that it doesn't
    -- interact with anything.
    onlyUsedUniquely :: Name -> Pred -> Bool
onlyUsedUniquely Name
n Pred
p = case Pred
p of
      Assert Term Bool
t
        | Name
n Name -> Term Bool -> Bool
forall a. HasVariables a => Name -> a -> Bool
`appearsIn` Term Bool
t -> Set Name -> Int
forall a. Set a -> Int
Set.size (Term Bool -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term Bool
t) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
        | Bool
otherwise -> Bool
True
      And [Pred]
ps -> (Pred -> Bool) -> [Pred] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name -> Pred -> Bool
onlyUsedUniquely Name
n) [Pred]
ps
      -- TODO: we can (and should) probably add a bunch of cases to this.
      Pred
_ -> Bool
False

    go :: FreeVars -> [SubstEntry] -> Pred -> Writer Any Pred
go FreeVars
fvs [SubstEntry]
sub Pred
pred2 = case Pred
pred2 of
      ElemPred Bool
bool Term a
t NonEmpty a
xs
        | Bool -> Bool
not (Term a -> Bool
forall a. Term a -> Bool
isLit Term a
t)
        , Lit a
a <- [SubstEntry] -> Term a -> Term a
forall a. [SubstEntry] -> Term a -> Term a
substituteAndSimplifyTerm [SubstEntry]
sub Term a
t -> do
            Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any -> WriterT Any Identity ()) -> Any -> WriterT Any Identity ()
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
            Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred -> Writer Any Pred) -> Pred -> Writer Any Pred
forall a b. (a -> b) -> a -> b
$ Bool -> Term a -> NonEmpty a -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (a -> Term a
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a) NonEmpty a
xs
        | Bool
otherwise -> Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred -> Writer Any Pred) -> Pred -> Writer Any Pred
forall a b. (a -> b) -> a -> b
$ Bool -> Term a -> NonEmpty a -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool Term a
t NonEmpty a
xs
      Subst Var a
x Term a
t Pred
p -> FreeVars -> [SubstEntry] -> Pred -> Writer Any Pred
go FreeVars
fvs [SubstEntry]
sub (Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p)
      ForAll Term t
set Binder a
b
        | Bool -> Bool
not (Term t -> Bool
forall a. Term a -> Bool
isLit Term t
set)
        , Lit t
a <- [SubstEntry] -> Term t -> Term t
forall a. [SubstEntry] -> Term a -> Term a
substituteAndSimplifyTerm [SubstEntry]
sub Term t
set -> do
            Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any -> WriterT Any Identity ()) -> Any -> WriterT Any Identity ()
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
            Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred -> Writer Any Pred) -> Pred -> Writer Any Pred
forall a b. (a -> b) -> a -> b
$ (a -> Pred) -> [a] -> Pred
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (a -> Binder a -> Pred
forall a. a -> Binder a -> Pred
`unBind` Binder a
b) (t -> [a]
forall t e. Container t e => t -> [e]
forAllToList t
a)
        | Bool
otherwise -> Term t -> Binder a -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
set (Binder a -> Pred)
-> WriterT Any Identity (Binder a) -> Writer Any Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreeVars
-> [SubstEntry] -> Binder a -> WriterT Any Identity (Binder a)
forall a.
FreeVars -> [SubstEntry] -> Binder a -> Writer Any (Binder a)
goBinder FreeVars
fvs [SubstEntry]
sub Binder a
b
      Case Term (Either a b)
t Binder a
as Binder b
bs
        | Bool -> Bool
not (Term (Either a b) -> Bool
forall a. Term a -> Bool
isLit Term (Either a b)
t)
        , Lit Either a b
a <- [SubstEntry] -> Term (Either a b) -> Term (Either a b)
forall a. [SubstEntry] -> Term a -> Term a
substituteAndSimplifyTerm [SubstEntry]
sub Term (Either a b)
t -> do
            Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any -> WriterT Any Identity ()) -> Any -> WriterT Any Identity ()
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
            Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred -> Writer Any Pred) -> Pred -> Writer Any Pred
forall a b. (a -> b) -> a -> b
$ Either a b
-> Binder a
-> Binder b
-> (forall {x}. HasSpec x => Var x -> x -> Pred -> Pred)
-> Pred
forall a b r.
Either a b
-> Binder a
-> Binder b
-> (forall x. HasSpec x => Var x -> x -> Pred -> r)
-> r
runCaseOn Either a b
a Binder a
as Binder b
bs ((forall {x}. HasSpec x => Var x -> x -> Pred -> Pred) -> Pred)
-> (forall {x}. HasSpec x => Var x -> x -> Pred -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Var x
x x
v Pred
p -> Env -> Pred -> Pred
substPred (Var x -> x -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var x
x x
v) Pred
p
        | Bool
otherwise -> Term (Either a b) -> Binder a -> Binder b -> Pred
forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
Case Term (Either a b)
t (Binder a -> Binder b -> Pred)
-> WriterT Any Identity (Binder a)
-> WriterT Any Identity (Binder b -> Pred)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FreeVars
-> [SubstEntry] -> Binder a -> WriterT Any Identity (Binder a)
forall a.
FreeVars -> [SubstEntry] -> Binder a -> Writer Any (Binder a)
goBinder FreeVars
fvs [SubstEntry]
sub Binder a
as) WriterT Any Identity (Binder b -> Pred)
-> WriterT Any Identity (Binder b) -> Writer Any Pred
forall a b.
WriterT Any Identity (a -> b)
-> WriterT Any Identity a -> WriterT Any Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (FreeVars
-> [SubstEntry] -> Binder b -> WriterT Any Identity (Binder b)
forall a.
FreeVars -> [SubstEntry] -> Binder a -> Writer Any (Binder a)
goBinder FreeVars
fvs [SubstEntry]
sub Binder b
bs)
      Let Term a
t (Var a
x :-> Pred
p)
        | (Name -> Bool) -> Set Name -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Name
n -> Name -> FreeVars -> Int
count Name
n FreeVars
fvs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1) (Term a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term a
t) -> do
            Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any -> WriterT Any Identity ()) -> Any -> WriterT Any Identity ()
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
            Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred -> Writer Any Pred) -> Pred -> Writer Any Pred
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
        | Name -> Pred -> Bool
onlyUsedUniquely (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x) Pred
p -> do
            Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any -> WriterT Any Identity ()) -> Any -> WriterT Any Identity ()
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
            Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred -> Writer Any Pred) -> Pred -> Writer Any Pred
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
        | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x Name -> Pred -> Bool
forall a. HasVariables a => Name -> a -> Bool
`appearsIn` Pred
p -> do
            Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any -> WriterT Any Identity ()) -> Any -> WriterT Any Identity ()
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
            Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pred
p
        | Bool -> Bool
not (Term a -> Bool
forall a. Term a -> Bool
isLit Term a
t)
        , Lit a
a <- [SubstEntry] -> Term a -> Term a
forall a. [SubstEntry] -> Term a -> Term a
substituteAndSimplifyTerm [SubstEntry]
sub Term a
t -> do
            Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any -> WriterT Any Identity ()) -> Any -> WriterT Any Identity ()
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
            Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred -> Writer Any Pred) -> Pred -> Writer Any Pred
forall a b. (a -> b) -> a -> b
$ a -> Binder a -> Pred
forall a. a -> Binder a -> Pred
unBind a
a (Var a
x Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
p)
        | Bool
otherwise -> Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let Term a
t (Binder a -> Pred) -> (Pred -> Binder a) -> Pred -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var a
x Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:->) (Pred -> Pred) -> Writer Any Pred -> Writer Any Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreeVars -> [SubstEntry] -> Pred -> Writer Any Pred
go (FreeVars -> Var a -> Pred -> FreeVars
forall {a} {a}.
(HasSpec a, HasVariables a) =>
FreeVars -> Var a -> a -> FreeVars
underBinder FreeVars
fvs Var a
x Pred
p) (Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
t SubstEntry -> [SubstEntry] -> [SubstEntry]
forall a. a -> [a] -> [a]
: [SubstEntry]
sub) Pred
p
      Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k (Binder a -> Pred)
-> WriterT Any Identity (Binder a) -> Writer Any Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreeVars
-> [SubstEntry] -> Binder a -> WriterT Any Identity (Binder a)
forall a.
FreeVars -> [SubstEntry] -> Binder a -> Writer Any (Binder a)
goBinder FreeVars
fvs [SubstEntry]
sub Binder a
b
      And [Pred]
ps -> [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Foldable.fold ([Pred] -> Pred) -> WriterT Any Identity [Pred] -> Writer Any Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pred -> Writer Any Pred) -> [Pred] -> WriterT Any Identity [Pred]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FreeVars -> [SubstEntry] -> Pred -> Writer Any Pred
go FreeVars
fvs [SubstEntry]
sub) [Pred]
ps
      Assert Term Bool
t
        | Bool -> Bool
not (Term Bool -> Bool
forall a. Term a -> Bool
isLit Term Bool
t)
        , Lit Bool
b <- [SubstEntry] -> Term Bool -> Term Bool
forall a. [SubstEntry] -> Term a -> Term a
substituteAndSimplifyTerm [SubstEntry]
sub Term Bool
t -> do
            Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any -> WriterT Any Identity ()) -> Any -> WriterT Any Identity ()
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
            Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred -> Writer Any Pred) -> Pred -> Writer Any Pred
forall a b. (a -> b) -> a -> b
$ Bool -> Pred
toPred Bool
b
        | Bool
otherwise -> Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pred
pred2
      DependsOn Term a
t Term b
t'
        | Bool -> Bool
not (Term a -> Bool
forall a. Term a -> Bool
isLit Term a
t)
        , Lit {} <- [SubstEntry] -> Term a -> Term a
forall a. [SubstEntry] -> Term a -> Term a
substituteAndSimplifyTerm [SubstEntry]
sub Term a
t -> do
            Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any -> WriterT Any Identity ()) -> Any -> WriterT Any Identity ()
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
            Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred -> Writer Any Pred) -> Pred -> Writer Any Pred
forall a b. (a -> b) -> a -> b
$ Pred
TruePred
        | Bool -> Bool
not (Term b -> Bool
forall a. Term a -> Bool
isLit Term b
t')
        , Lit {} <- [SubstEntry] -> Term b -> Term b
forall a. [SubstEntry] -> Term a -> Term a
substituteAndSimplifyTerm [SubstEntry]
sub Term b
t' -> do
            Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any -> WriterT Any Identity ()) -> Any -> WriterT Any Identity ()
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
            Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred -> Writer Any Pred) -> Pred -> Writer Any Pred
forall a b. (a -> b) -> a -> b
$ Pred
TruePred
        | Bool
otherwise -> Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pred
pred2
      Pred
TruePred -> Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pred
pred2
      FalsePred {} -> Pred -> Writer Any Pred
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pred
pred2

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

-- | Lifts 'propagateSpec' to take a Monadic 'Ctx'
propagateSpecM ::
  forall v a m.
  (Monad m, HasSpec v) =>
  Spec a ->
  m (Ctx v a) ->
  m (Spec v)
propagateSpecM :: forall v a (m :: * -> *).
(Monad m, HasSpec v) =>
Spec a -> m (Ctx v a) -> m (Spec v)
propagateSpecM Spec a
spec m (Ctx v a)
ctxM = do Ctx v a
ctx <- m (Ctx v a)
ctxM; Spec v -> m (Spec v)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Spec v -> m (Spec v)) -> Spec v -> m (Spec v)
forall a b. (a -> b) -> a -> b
$ Ctx v a -> Spec a -> Spec v
forall v a. HasSpec v => Ctx v a -> Spec a -> Spec v
propagateSpec Ctx v a
ctx Spec a
spec

-- | Precondition: the `Pred` defines the `Var a`
-- Runs in `GE` in order for us to have detailed context on failure.
computeSpecSimplified ::
  forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpecSimplified :: forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpecSimplified Var a
x Pred
pred3 = GE (Spec a) -> GE (Spec a)
forall {a}. GE (Spec a) -> GE (Spec a)
localGESpec (GE (Spec a) -> GE (Spec a)) -> GE (Spec a) -> GE (Spec a)
forall a b. (a -> b) -> a -> b
$ case Pred -> Pred
simplifyPred Pred
pred3 of
  And [Pred]
ps -> do
    Spec a
spec <- [Spec a] -> Spec a
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ([Spec a] -> Spec a) -> GE [Spec a] -> GE (Spec a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pred -> GE (Spec a)) -> [Pred] -> GE [Spec a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Var a -> Pred -> GE (Spec a)
forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpecSimplified Var a
x) [Pred]
ps
    case Spec a
spec of
      SuspendedSpec Var a
y Pred
ps' -> Spec a -> GE (Spec a)
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Spec a -> GE (Spec a)) -> Spec a -> GE (Spec a)
forall a b. (a -> b) -> a -> b
$ Var a -> Pred -> Spec a
forall a. HasSpec a => Var a -> Pred -> Spec a
SuspendedSpec Var a
y (Pred -> Spec a) -> Pred -> Spec a
forall a b. (a -> b) -> a -> b
$ Pred -> Pred
simplifyPred Pred
ps'
      Spec a
s -> Spec a -> GE (Spec a)
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Spec a
s
  ElemPred Bool
True Term a
t NonEmpty a
xs -> Spec a -> GE (Ctx a a) -> GE (Spec a)
forall v a (m :: * -> *).
(Monad m, HasSpec v) =>
Spec a -> m (Ctx v a) -> m (Spec v)
propagateSpecM (NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec NonEmpty a
xs) (Var a -> Term a -> GE (Ctx a a)
forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var a
x Term a
t)
  ElemPred Bool
False (Term a
t :: Term b) NonEmpty a
xs -> Spec a -> GE (Ctx a a) -> GE (Spec a)
forall v a (m :: * -> *).
(Monad m, HasSpec v) =>
Spec a -> m (Ctx v a) -> m (Spec v)
propagateSpecM (forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec @b (forall a. HasSpec a => TypeSpec a
anySpec @b) (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
xs)) (Var a -> Term a -> GE (Ctx a a)
forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var a
x Term a
t)
  Subst Var a
x' Term a
t Pred
p' -> Var a -> Pred -> GE (Spec a)
forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpec Var a
x (Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x' Term a
t Pred
p') -- NOTE: this is impossible as it should have gone away already
  Pred
TruePred -> Spec a -> GE (Spec a)
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Spec a
forall a. Monoid a => a
mempty
  FalsePred NonEmpty String
es -> NonEmpty String -> GE (Spec a)
forall a. HasCallStack => NonEmpty String -> GE a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE NonEmpty String
es
  Let Term a
t Binder a
b -> Spec a -> GE (Spec a)
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Spec a -> GE (Spec a)) -> Spec a -> GE (Spec a)
forall a b. (a -> b) -> a -> b
$ Var a -> Pred -> Spec a
forall a. HasSpec a => Var a -> Pred -> Spec a
SuspendedSpec Var a
x (Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let Term a
t Binder a
b)
  Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> Spec a -> GE (Spec a)
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Spec a -> GE (Spec a)) -> Spec a -> GE (Spec a)
forall a b. (a -> b) -> a -> b
$ Var a -> Pred -> Spec a
forall a. HasSpec a => Var a -> Pred -> Spec a
SuspendedSpec Var a
x (((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k Binder a
b)
  Assert (Lit Bool
True) -> Spec a -> GE (Spec a)
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Spec a
forall a. Monoid a => a
mempty
  Assert (Lit Bool
False) -> String -> GE (Spec a)
forall (m :: * -> *) a. MonadGenError m => String -> m a
genError (Pred -> String
forall a. Show a => a -> String
show Pred
pred3)
  Assert Term Bool
t -> Spec Bool -> GE (Ctx a Bool) -> GE (Spec a)
forall v a (m :: * -> *).
(Monad m, HasSpec v) =>
Spec a -> m (Ctx v a) -> m (Spec v)
propagateSpecM (Bool -> Spec Bool
forall a. a -> Spec a
equalSpec Bool
True) (Var a -> Term Bool -> GE (Ctx a Bool)
forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var a
x Term Bool
t)
  ForAll (Lit t
s) Binder a
b -> [Spec a] -> Spec a
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ([Spec a] -> Spec a) -> GE [Spec a] -> GE (Spec a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> GE (Spec a)) -> [a] -> GE [Spec a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\a
val -> Var a -> Pred -> GE (Spec a)
forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpec Var a
x (Pred -> GE (Spec a)) -> Pred -> GE (Spec a)
forall a b. (a -> b) -> a -> b
$ a -> Binder a -> Pred
forall a. a -> Binder a -> Pred
unBind a
val Binder a
b) (t -> [a]
forall t e. Container t e => t -> [e]
forAllToList t
s)
  ForAll Term t
t Binder a
b -> do
    Spec a
bSpec <- Binder a -> GE (Spec a)
forall a. Binder a -> GE (Spec a)
computeSpecBinderSimplified Binder a
b
    Spec t -> GE (Ctx a t) -> GE (Spec a)
forall v a (m :: * -> *).
(Monad m, HasSpec v) =>
Spec a -> m (Ctx v a) -> m (Spec v)
propagateSpecM (Spec a -> Spec t
forall t e.
(Container t e, HasSpec t, HasSpec e) =>
Spec e -> Spec t
fromForAllSpec Spec a
bSpec) (Var a -> Term t -> GE (Ctx a t)
forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var a
x Term t
t)
  Case (Lit Either a b
val) Binder a
as Binder b
bs -> Either a b
-> Binder a
-> Binder b
-> (forall {x}. HasSpec x => Var x -> x -> Pred -> GE (Spec a))
-> GE (Spec a)
forall a b r.
Either a b
-> Binder a
-> Binder b
-> (forall x. HasSpec x => Var x -> x -> Pred -> r)
-> r
runCaseOn Either a b
val Binder a
as Binder b
bs ((forall {x}. HasSpec x => Var x -> x -> Pred -> GE (Spec a))
 -> GE (Spec a))
-> (forall {x}. HasSpec x => Var x -> x -> Pred -> GE (Spec a))
-> GE (Spec a)
forall a b. (a -> b) -> a -> b
$ \Var x
va x
vaVal Pred
psa -> Var a -> Pred -> GE (Spec a)
forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpec Var a
x (Env -> Pred -> Pred
substPred (Var x -> x -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var x
va x
vaVal) Pred
psa)
  Case Term (Either a b)
t Binder a
as Binder b
bs -> do
    Spec a
simpAs <- Binder a -> GE (Spec a)
forall a. Binder a -> GE (Spec a)
computeSpecBinderSimplified Binder a
as
    Spec b
simpBs <- Binder b -> GE (Spec b)
forall a. Binder a -> GE (Spec a)
computeSpecBinderSimplified Binder b
bs
    Spec (Either a b) -> GE (Ctx a (Either a b)) -> GE (Spec a)
forall v a (m :: * -> *).
(Monad m, HasSpec v) =>
Spec a -> m (Ctx v a) -> m (Spec v)
propagateSpecM (TypeSpec (Either a b) -> Spec (Either a b)
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Spec a -> Spec b -> SumSpec (Spec a) (Spec b)
forall a b. a -> b -> SumSpec a b
SumSpec Spec a
simpAs Spec b
simpBs)) (Var a -> Term (Either a b) -> GE (Ctx a (Either a b))
forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var a
x Term (Either a b)
t)
  -- Impossible cases that should be ruled out by the dependency analysis and linearizer
  DependsOn {} ->
    NonEmpty String -> GE (Spec a)
forall a. HasCallStack => NonEmpty String -> GE a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (NonEmpty String -> GE (Spec a)) -> NonEmpty String -> GE (Spec a)
forall a b. (a -> b) -> a -> b
$
      [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
        [ String
"The impossible happened in computeSpec: DependsOn"
        , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var a -> String
forall a. Show a => a -> String
show Var a
x
        , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Pred -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Pred -> Doc ann
pretty Pred
pred3)
        ]
  where
    -- We want `genError` to turn into `ErrorSpec` and we want `FatalError` to turn into `FatalError`
    localGESpec :: GE (Spec a) -> GE (Spec a)
localGESpec GE (Spec a)
ge = case GE (Spec a)
ge of
      (GenError NonEmpty (NonEmpty String)
xs) -> Spec a -> GE (Spec a)
forall a. a -> GE a
Result (Spec a -> GE (Spec a)) -> Spec a -> GE (Spec a)
forall a b. (a -> b) -> a -> b
$ NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty (NonEmpty String) -> NonEmpty String
catMessageList NonEmpty (NonEmpty String)
xs)
      (FatalError NonEmpty (NonEmpty String)
es) -> NonEmpty (NonEmpty String) -> GE (Spec a)
forall a. NonEmpty (NonEmpty String) -> GE a
FatalError NonEmpty (NonEmpty String)
es
      (Result Spec a
v) -> Spec a -> GE (Spec a)
forall a. a -> GE a
Result Spec a
v

-- | Precondition: the `Pred fn` defines the `Var a`.
--   Runs in `GE` in order for us to have detailed context on failure.
computeSpec ::
  forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpec :: forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpec Var a
x Pred
p = Var a -> Pred -> GE (Spec a)
forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpecSimplified Var a
x (Pred -> Pred
simplifyPred Pred
p)

computeSpecBinder :: Binder a -> GE (Spec a)
computeSpecBinder :: forall a. Binder a -> GE (Spec a)
computeSpecBinder (Var a
x :-> Pred
p) = Var a -> Pred -> GE (Spec a)
forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpec Var a
x Pred
p

computeSpecBinderSimplified :: Binder a -> GE (Spec a)
computeSpecBinderSimplified :: forall a. Binder a -> GE (Spec a)
computeSpecBinderSimplified (Var a
x :-> Pred
p) = Var a -> Pred -> GE (Spec a)
forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpecSimplified Var a
x Pred
p

-- ---------------------- Building a plan -----------------------------------

substStage :: Env -> SolverStage -> SolverStage
substStage :: Env -> SolverStage -> SolverStage
substStage Env
env (SolverStage Var a
y [Pred]
ps Spec a
spec) = SolverStage -> SolverStage
normalizeSolverStage (SolverStage -> SolverStage) -> SolverStage -> SolverStage
forall a b. (a -> b) -> a -> b
$ Var a -> [Pred] -> Spec a -> SolverStage
forall a. HasSpec a => Var a -> [Pred] -> Spec a -> SolverStage
SolverStage Var a
y (Env -> Pred -> Pred
substPred Env
env (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps) Spec a
spec

normalizeSolverStage :: SolverStage -> SolverStage
normalizeSolverStage :: SolverStage -> SolverStage
normalizeSolverStage (SolverStage Var a
x [Pred]
ps Spec a
spec) = Var a -> [Pred] -> Spec a -> SolverStage
forall a. HasSpec a => Var a -> [Pred] -> Spec a -> SolverStage
SolverStage Var a
x [Pred]
ps'' (Spec a
spec Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> Spec a
spec')
  where
    ([Pred]
ps', [Pred]
ps'') = (Pred -> Bool) -> [Pred] -> ([Pred], [Pred])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((Int
1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool) -> (Pred -> Int) -> Pred -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Name -> Int
forall a. Set a -> Int
Set.size (Set Name -> Int) -> (Pred -> Set Name) -> Pred -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet) [Pred]
ps
    spec' :: Spec a
spec' = GE (Spec a) -> Spec a
forall a. HasCallStack => GE (Spec a) -> Spec a
fromGESpec (GE (Spec a) -> Spec a) -> GE (Spec a) -> Spec a
forall a b. (a -> b) -> a -> b
$ Var a -> Pred -> GE (Spec a)
forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpec Var a
x ([Pred] -> Pred
And [Pred]
ps')

type Hints = DependGraph

type DependGraph = Graph.Graph Name

dependency :: HasVariables t => Name -> t -> DependGraph
dependency :: forall t. HasVariables t => Name -> t -> Graph Name
dependency Name
x (t -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet -> Set Name
xs) = Name -> Set Name -> Graph Name
forall node. Ord node => node -> Set node -> Graph node
Graph.dependency Name
x Set Name
xs

irreflexiveDependencyOn ::
  forall t t'. (HasVariables t, HasVariables t') => t -> t' -> DependGraph
irreflexiveDependencyOn :: forall t t'.
(HasVariables t, HasVariables t') =>
t -> t' -> Graph Name
irreflexiveDependencyOn (t -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet -> Set Name
xs) (t' -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet -> Set Name
ys) = Set Name -> Set Name -> Graph Name
forall node. Ord node => Set node -> Set node -> Graph node
Graph.irreflexiveDependencyOn Set Name
xs Set Name
ys

noDependencies :: HasVariables t => t -> DependGraph
noDependencies :: forall t. HasVariables t => t -> Graph Name
noDependencies (t -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet -> Set Name
xs) = Set Name -> Graph Name
forall node. Ord node => Set node -> Graph node
Graph.noDependencies Set Name
xs

respecting :: Hints -> DependGraph -> DependGraph
respecting :: Graph Name -> Graph Name -> Graph Name
respecting Graph Name
hints Graph Name
g = Graph Name
g Graph Name -> Graph Name -> Graph Name
forall node. Ord node => Graph node -> Graph node -> Graph node
`Graph.subtractGraph` Graph Name -> Graph Name
forall node. Graph node -> Graph node
Graph.opGraph Graph Name
hints

solvableFrom :: Name -> Set Name -> DependGraph -> Bool
solvableFrom :: Name -> Set Name -> Graph Name -> Bool
solvableFrom Name
x Set Name
s Graph Name
g =
  let less :: Set Name
less = Name -> Graph Name -> Set Name
forall node. Ord node => node -> Graph node -> Set node
Graph.dependencies Name
x Graph Name
g
   in Set Name
s Set Name -> Set Name -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set Name
less Bool -> Bool -> Bool
&& Bool -> Bool
not (Name
x Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
less)

-- TODO: here we can compute both the explicit hints (i.e. constraints that
-- define the order of two variables) and any whole-program smarts.
computeHints :: [Pred] -> Hints
computeHints :: [Pred] -> Graph Name
computeHints [Pred]
ps =
  Graph Name -> Graph Name
forall node. Ord node => Graph node -> Graph node
Graph.transitiveClosure (Graph Name -> Graph Name) -> Graph Name -> Graph Name
forall a b. (a -> b) -> a -> b
$ [Graph Name] -> Graph Name
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [Term a
x Term a -> Term b -> Graph Name
forall t t'.
(HasVariables t, HasVariables t') =>
t -> t' -> Graph Name
`irreflexiveDependencyOn` Term b
y | DependsOn Term a
x Term b
y <- [Pred]
ps]

saturatePred :: Pred -> [Pred]
saturatePred :: Pred -> [Pred]
saturatePred Pred
p = [Pred
p]

-- | Linearize a predicate, turning it into a list of variables to solve and
-- their defining constraints such that each variable can be solved independently.
prepareLinearization :: Pred -> GE SolverPlan
prepareLinearization :: Pred -> GE SolverPlan
prepareLinearization Pred
p = do
  let preds :: [Pred]
preds = (Pred -> [Pred]) -> [Pred] -> [Pred]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pred -> [Pred]
saturatePred ([Pred] -> [Pred]) -> [Pred] -> [Pred]
forall a b. (a -> b) -> a -> b
$ Pred -> [Pred]
flattenPred Pred
p
      hints :: Graph Name
hints = [Pred] -> Graph Name
computeHints [Pred]
preds
      graph :: Graph Name
graph = Graph Name -> Graph Name
forall node. Ord node => Graph node -> Graph node
Graph.transitiveClosure (Graph Name -> Graph Name) -> Graph Name -> Graph Name
forall a b. (a -> b) -> a -> b
$ Graph Name
hints Graph Name -> Graph Name -> Graph Name
forall a. Semigroup a => a -> a -> a
<> Graph Name -> Graph Name -> Graph Name
respecting Graph Name
hints ((Pred -> Graph Name) -> [Pred] -> Graph Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pred -> Graph Name
computeDependencies [Pred]
preds)
  [SolverStage]
plan <-
    NonEmpty String -> GE [SolverStage] -> GE [SolverStage]
forall a. HasCallStack => NonEmpty String -> GE a -> GE a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
      ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [ String
"Linearizing"
          , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"  preds: " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> [Pred] -> Doc Any
forall ann. [Pred] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Pred]
preds
          , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"  graph: " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Graph Name -> Doc Any
forall ann. Graph Name -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Graph Name
graph
          ]
      )
      (GE [SolverStage] -> GE [SolverStage])
-> GE [SolverStage] -> GE [SolverStage]
forall a b. (a -> b) -> a -> b
$ [Pred] -> Graph Name -> GE [SolverStage]
forall (m :: * -> *).
MonadGenError m =>
[Pred] -> Graph Name -> m [SolverStage]
linearize [Pred]
preds Graph Name
graph
  SolverPlan -> GE SolverPlan
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SolverPlan -> GE SolverPlan) -> SolverPlan -> GE SolverPlan
forall a b. (a -> b) -> a -> b
$ SolverPlan -> SolverPlan
backPropagation (SolverPlan -> SolverPlan) -> SolverPlan -> SolverPlan
forall a b. (a -> b) -> a -> b
$ [SolverStage] -> Graph Name -> SolverPlan
SolverPlan [SolverStage]
plan Graph Name
graph

-- | Flatten nested `Let`, `Exists`, and `And` in a `Pred fn`. `Let` and
-- `Exists` bound variables become free in the result.
flattenPred :: Pred -> [Pred]
flattenPred :: Pred -> [Pred]
flattenPred Pred
pIn = Set Int -> [Pred] -> [Pred]
go (Pred -> Set Int
forall t. HasVariables t => t -> Set Int
freeVarNames Pred
pIn) [Pred
pIn]
  where
    go :: Set Int -> [Pred] -> [Pred]
go Set Int
_ [] = []
    go Set Int
fvs (Pred
p : [Pred]
ps) = case Pred
p of
      And [Pred]
ps' -> Set Int -> [Pred] -> [Pred]
go Set Int
fvs ([Pred]
ps' [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [Pred]
ps)
      -- NOTE: the order of the arguments to `==.` here are important.
      -- The whole point of `Let` is that it allows us to solve all of `t`
      -- before we solve the variables in `t`.
      Let Term a
t Binder a
b -> Set Int
-> Binder a
-> [Pred]
-> (HasSpec a => Var a -> [Pred] -> [Pred])
-> [Pred]
forall a.
Set Int
-> Binder a
-> [Pred]
-> (HasSpec a => Var a -> [Pred] -> [Pred])
-> [Pred]
goBinder Set Int
fvs Binder a
b [Pred]
ps (\Var a
x -> (Term Bool -> Pred
Assert (Term a
t Term a -> Term a -> Term Bool
forall a.
(HasSpec Bool, HasSpec a) =>
Term a -> Term a -> Term Bool
==. (Var a -> Term a
forall a. HasSpec a => Var a -> Term a
V Var a
x)) Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
:))
      Exists (forall b. Term b -> b) -> GE a
_ Binder a
b -> Set Int
-> Binder a
-> [Pred]
-> (HasSpec a => Var a -> [Pred] -> [Pred])
-> [Pred]
forall a.
Set Int
-> Binder a
-> [Pred]
-> (HasSpec a => Var a -> [Pred] -> [Pred])
-> [Pred]
goBinder Set Int
fvs Binder a
b [Pred]
ps (([Pred] -> [Pred]) -> Var a -> [Pred] -> [Pred]
forall a b. a -> b -> a
const [Pred] -> [Pred]
forall a. a -> a
id)
      Pred
_ -> Pred
p Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: Set Int -> [Pred] -> [Pred]
go Set Int
fvs [Pred]
ps

    goBinder ::
      Set Int ->
      Binder a ->
      [Pred] ->
      (HasSpec a => Var a -> [Pred] -> [Pred]) ->
      [Pred]
    goBinder :: forall a.
Set Int
-> Binder a
-> [Pred]
-> (HasSpec a => Var a -> [Pred] -> [Pred])
-> [Pred]
goBinder Set Int
fvs (Var a
x :-> Pred
p) [Pred]
ps HasSpec a => Var a -> [Pred] -> [Pred]
k = Var a -> [Pred] -> [Pred]
HasSpec a => Var a -> [Pred] -> [Pred]
k Var a
x' ([Pred] -> [Pred]) -> [Pred] -> [Pred]
forall a b. (a -> b) -> a -> b
$ Set Int -> [Pred] -> [Pred]
go (Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.insert (Var a -> Int
forall a. Var a -> Int
nameOf Var a
x') Set Int
fvs) (Pred
p' Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ps)
      where
        (Var a
x', Pred
p') = Var a -> Pred -> Set Int -> (Var a, Pred)
forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
x Pred
p Set Int
fvs

-- Consider: A + B = C + D
-- We want to fail if A and B are independent.
-- Consider: A + B = A + C, A <- B
-- Here we want to consider this constraint defining for A
linearize ::
  MonadGenError m => [Pred] -> DependGraph -> m [SolverStage]
linearize :: forall (m :: * -> *).
MonadGenError m =>
[Pred] -> Graph Name -> m [SolverStage]
linearize [Pred]
preds Graph Name
graph = do
  [Name]
sorted <- case Graph Name -> Either [Name] [Name]
forall node. Ord node => Graph node -> Either [node] [node]
Graph.topsort Graph Name
graph of
    Left [Name]
cycleX ->
      String -> m [Name]
forall (m :: * -> *) a. MonadGenError m => String -> m a
fatalError
        ( Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$
            Doc Any
"linearize: Dependency cycle in graph:"
              Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc Any] -> Doc Any
forall ann. [Doc ann] -> Doc ann
vsep'
                [ Doc Any
"cycle:" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Name] -> Doc Any
forall ann. [Name] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Name]
cycleX
                , Doc Any
"graph:" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
/> Graph Name -> Doc Any
forall ann. Graph Name -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Graph Name
graph
                ]
        )
    Right [Name]
sorted -> [Name] -> m [Name]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Name]
sorted
  [Name] -> [(Set Name, Pred)] -> m [SolverStage]
go [Name]
sorted [(Pred -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Pred
ps, Pred
ps) | Pred
ps <- (Pred -> Bool) -> [Pred] -> [Pred]
forall a. (a -> Bool) -> [a] -> [a]
filter Pred -> Bool
isRelevantPred [Pred]
preds]
  where
    isRelevantPred :: Pred -> Bool
isRelevantPred Pred
TruePred = Bool
False
    isRelevantPred DependsOn {} = Bool
False
    isRelevantPred (Assert (Lit Bool
True)) = Bool
False
    isRelevantPred Pred
_ = Bool
True

    go :: [Name] -> [(Set Name, Pred)] -> m [SolverStage]
go [] [] = [SolverStage] -> m [SolverStage]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    go [] [(Set Name, Pred)]
ps
      | Set Name -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Set Name -> Bool) -> Set Name -> Bool
forall a b. (a -> b) -> a -> b
$ ((Set Name, Pred) -> Set Name) -> [(Set Name, Pred)] -> Set Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Set Name, Pred) -> Set Name
forall a b. (a, b) -> a
fst [(Set Name, Pred)]
ps =
          case NonEmpty String -> Env -> [Pred] -> Maybe (NonEmpty String)
checkPredsE (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Linearizing fails") Env
forall a. Monoid a => a
mempty (((Set Name, Pred) -> Pred) -> [(Set Name, Pred)] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map (Set Name, Pred) -> Pred
forall a b. (a, b) -> b
snd [(Set Name, Pred)]
ps) of
            Maybe (NonEmpty String)
Nothing -> [SolverStage] -> m [SolverStage]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
            Just NonEmpty String
msgs -> NonEmpty String -> m [SolverStage]
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE NonEmpty String
msgs
      | Bool
otherwise =
          NonEmpty String -> m [SolverStage]
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (NonEmpty String -> m [SolverStage])
-> NonEmpty String -> m [SolverStage]
forall a b. (a -> b) -> a -> b
$
            [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
              [ String
"Dependency error in `linearize`: "
              , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Doc Any
"graph: " Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
/> Graph Name -> Doc Any
forall ann. Graph Name -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Graph Name
graph
              , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$
                  Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$
                    Doc Any
"the following left-over constraints are not defining constraints for a unique variable:"
                      Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc Any] -> Doc Any
forall ann. [Doc ann] -> Doc ann
vsep' (((Set Name, Pred) -> Doc Any) -> [(Set Name, Pred)] -> [Doc Any]
forall a b. (a -> b) -> [a] -> [b]
map (Pred -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Pred -> Doc ann
pretty (Pred -> Doc Any)
-> ((Set Name, Pred) -> Pred) -> (Set Name, Pred) -> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Name, Pred) -> Pred
forall a b. (a, b) -> b
snd) [(Set Name, Pred)]
ps)
              ]
    go (n :: Name
n@(Name Var a
x) : [Name]
ns) [(Set Name, Pred)]
ps = do
      let ([(Set Name, Pred)]
nps, [(Set Name, Pred)]
ops) = ((Set Name, Pred) -> Bool)
-> [(Set Name, Pred)] -> ([(Set Name, Pred)], [(Set Name, Pred)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Name -> Set Name -> Bool
isLastVariable Name
n (Set Name -> Bool)
-> ((Set Name, Pred) -> Set Name) -> (Set Name, Pred) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Name, Pred) -> Set Name
forall a b. (a, b) -> a
fst) [(Set Name, Pred)]
ps
      (SolverStage -> SolverStage
normalizeSolverStage (Var a -> [Pred] -> Spec a -> SolverStage
forall a. HasSpec a => Var a -> [Pred] -> Spec a -> SolverStage
SolverStage Var a
x (((Set Name, Pred) -> Pred) -> [(Set Name, Pred)] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map (Set Name, Pred) -> Pred
forall a b. (a, b) -> b
snd [(Set Name, Pred)]
nps) Spec a
forall a. Monoid a => a
mempty) SolverStage -> [SolverStage] -> [SolverStage]
forall a. a -> [a] -> [a]
:) ([SolverStage] -> [SolverStage])
-> m [SolverStage] -> m [SolverStage]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name] -> [(Set Name, Pred)] -> m [SolverStage]
go [Name]
ns [(Set Name, Pred)]
ops

    isLastVariable :: Name -> Set Name -> Bool
isLastVariable Name
n Set Name
set = Name
n Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
set Bool -> Bool -> Bool
&& Name -> Set Name -> Graph Name -> Bool
solvableFrom Name
n (Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.delete Name
n Set Name
set) Graph Name
graph

-- =================================
-- Operations on Stages and Plans

-- | Does nothing if the variable is not in the plan already.
mergeSolverStage :: SolverStage -> [SolverStage] -> [SolverStage]
mergeSolverStage :: SolverStage -> [SolverStage] -> [SolverStage]
mergeSolverStage (SolverStage Var a
x [Pred]
ps Spec a
spec) [SolverStage]
plan =
  [ case Var a -> Var a -> Maybe (a :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
y of
      Just a :~: a
Refl ->
        Var a -> [Pred] -> Spec a -> SolverStage
forall a. HasSpec a => Var a -> [Pred] -> Spec a -> SolverStage
SolverStage
          Var a
y
          ([Pred]
ps [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [Pred]
ps')
          ( NonEmpty String -> Spec a -> Spec a
forall a. NonEmpty String -> Spec a -> Spec a
addToErrorSpec
              ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
                  ( [ String
"Solving var " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var a -> String
forall a. Show a => a -> String
show Var a
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" fails."
                    , String
"Merging the Specs"
                    , String
"   1. " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
spec
                    , String
"   2. " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
spec'
                    ]
                  )
              )
              (Spec a
Spec a
spec Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> Spec a
spec')
          )
      Maybe (a :~: a)
Nothing -> SolverStage
stage
  | stage :: SolverStage
stage@(SolverStage Var a
y [Pred]
ps' Spec a
spec') <- [SolverStage]
plan
  ]

prettyPlan :: HasSpec a => Spec a -> Doc ann
prettyPlan :: forall a ann. HasSpec a => Spec a -> Doc ann
prettyPlan (Spec a -> Spec a
forall a. HasSpec a => Spec a -> Spec a
simplifySpec -> Spec a
spec)
  | SuspendedSpec Var a
_ Pred
p <- Spec a
spec
  , Result SolverPlan
plan <- Pred -> GE SolverPlan
prepareLinearization Pred
p =
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep'
        [ Doc ann
"Simplified spec:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> Spec a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Spec a -> Doc ann
pretty Spec a
spec
        , SolverPlan -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. SolverPlan -> Doc ann
pretty SolverPlan
plan
        ]
  | Bool
otherwise = Doc ann
"Simplfied spec:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> Spec a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Spec a -> Doc ann
pretty Spec a
spec

printPlan :: HasSpec a => Spec a -> IO ()
printPlan :: forall a. HasSpec a => Spec a -> IO ()
printPlan = Doc Any -> IO ()
forall a. Show a => a -> IO ()
print (Doc Any -> IO ()) -> (Spec a -> Doc Any) -> Spec a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec a -> Doc Any
forall a ann. HasSpec a => Spec a -> Doc ann
prettyPlan

isEmptyPlan :: SolverPlan -> Bool
isEmptyPlan :: SolverPlan -> Bool
isEmptyPlan (SolverPlan [SolverStage]
plan Graph Name
_) = [SolverStage] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SolverStage]
plan

stepPlan :: MonadGenError m => Env -> SolverPlan -> GenT m (Env, SolverPlan)
stepPlan :: forall (m :: * -> *).
MonadGenError m =>
Env -> SolverPlan -> GenT m (Env, SolverPlan)
stepPlan Env
env plan :: SolverPlan
plan@(SolverPlan [] Graph Name
_) = (Env, SolverPlan) -> GenT m (Env, SolverPlan)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env
env, SolverPlan
plan)
stepPlan Env
env p :: SolverPlan
p@(SolverPlan (SolverStage Var a
x [Pred]
ps Spec a
spec : [SolverStage]
pl) Graph Name
gr) = do
  (Spec a
spec', [Spec a]
specs) <- GE (Spec a, [Spec a]) -> GenT m (Spec a, [Spec a])
forall (m :: * -> *) r. MonadGenError m => GE r -> m r
runGE
    (GE (Spec a, [Spec a]) -> GenT m (Spec a, [Spec a]))
-> GE (Spec a, [Spec a]) -> GenT m (Spec a, [Spec a])
forall a b. (a -> b) -> a -> b
$ String -> GE (Spec a, [Spec a]) -> GE (Spec a, [Spec a])
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain
      (Doc Any -> String
forall a. Show a => a -> String
show (Env -> Doc Any
forall ann. Env -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Env
env) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nStep " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var a -> String
forall a. Show a => a -> String
show Var a
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (SolverPlan -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. SolverPlan -> Doc ann
pretty SolverPlan
p))
    (GE (Spec a, [Spec a]) -> GE (Spec a, [Spec a]))
-> GE (Spec a, [Spec a]) -> GE (Spec a, [Spec a])
forall a b. (a -> b) -> a -> b
$ do
      [Spec a]
ispecs <- (Pred -> GE (Spec a)) -> [Pred] -> GE [Spec a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Var a -> Pred -> GE (Spec a)
forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a)
computeSpec Var a
x) [Pred]
ps
      (Spec a, [Spec a]) -> GE (Spec a, [Spec a])
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Spec a, [Spec a]) -> GE (Spec a, [Spec a]))
-> (Spec a, [Spec a]) -> GE (Spec a, [Spec a])
forall a b. (a -> b) -> a -> b
$ ([Spec a] -> Spec a
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [Spec a]
ispecs, [Spec a]
ispecs)
  a
val <-
    Spec a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT
      ( NonEmpty String -> Spec a -> Spec a
forall a. NonEmpty String -> Spec a -> Spec a
addToErrorSpec
          ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
              ( ( String
"\nStepPlan for variable: "
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var a -> String
forall a. Show a => a -> String
show Var a
x
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" fails to produce Specification, probably overconstrained."
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"PS = "
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Pred -> String) -> [Pred] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> String
forall a. Show a => a -> String
show [Pred]
ps)
                )
                  String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String
"Original spec " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
spec)
                  String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
"Predicates"
                  String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Pred -> Spec a -> String) -> [Pred] -> [Spec a] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
                    (\Pred
pred1 Spec a
specx -> String
"  pred " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pred -> String
forall a. Show a => a -> String
show Pred
pred1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
specx)
                    [Pred]
ps
                    [Spec a]
specs
              )
          )
          (Spec a
spec Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> Spec a
spec')
      )
  let env1 :: Env
env1 = Var a -> a -> Env -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env
  (Env, SolverPlan) -> GenT m (Env, SolverPlan)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env
env1, SolverPlan -> SolverPlan
backPropagation (SolverPlan -> SolverPlan) -> SolverPlan -> SolverPlan
forall a b. (a -> b) -> a -> b
$ [SolverStage] -> Graph Name -> SolverPlan
SolverPlan (Env -> SolverStage -> SolverStage
substStage Env
env1 (SolverStage -> SolverStage) -> [SolverStage] -> [SolverStage]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SolverStage]
pl) (Name -> Graph Name -> Graph Name
forall node. Ord node => node -> Graph node -> Graph node
Graph.deleteNode (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x) Graph Name
gr))

computeDependencies :: Pred -> DependGraph
computeDependencies :: Pred -> Graph Name
computeDependencies = \case
  ElemPred Bool
_bool Term a
term NonEmpty a
_xs -> Term a -> Graph Name
forall a. Term a -> Graph Name
computeTermDependencies Term a
term
  Subst Var a
x Term a
t Pred
p -> Pred -> Graph Name
computeDependencies (Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p)
  Assert Term Bool
t -> Term Bool -> Graph Name
forall a. Term a -> Graph Name
computeTermDependencies Term Bool
t
  ForAll Term t
set Binder a
b ->
    let innerG :: Graph Name
innerG = Binder a -> Graph Name
forall a. Binder a -> Graph Name
computeBinderDependencies Binder a
b
     in Graph Name
innerG Graph Name -> Graph Name -> Graph Name
forall a. Semigroup a => a -> a -> a
<> Term t
set Term t -> Set Name -> Graph Name
forall t t'.
(HasVariables t, HasVariables t') =>
t -> t' -> Graph Name
`irreflexiveDependencyOn` Graph Name -> Set Name
forall node. Graph node -> Set node
Graph.nodes Graph Name
innerG
  DependsOn Term a
x Term b
y -> Term a
x Term a -> Term b -> Graph Name
forall t t'.
(HasVariables t, HasVariables t') =>
t -> t' -> Graph Name
`irreflexiveDependencyOn` Term b
y
  Case Term (Either a b)
t Binder a
as Binder b
bs -> Term (Either a b) -> Graph Name
forall t. HasVariables t => t -> Graph Name
noDependencies Term (Either a b)
t Graph Name -> Graph Name -> Graph Name
forall a. Semigroup a => a -> a -> a
<> Binder a -> Graph Name
forall a. Binder a -> Graph Name
computeBinderDependencies Binder a
as Graph Name -> Graph Name -> Graph Name
forall a. Semigroup a => a -> a -> a
<> Binder b -> Graph Name
forall a. Binder a -> Graph Name
computeBinderDependencies Binder b
bs
  Pred
TruePred -> Graph Name
forall a. Monoid a => a
mempty
  FalsePred {} -> Graph Name
forall a. Monoid a => a
mempty
  And [Pred]
ps -> (Pred -> Graph Name) -> [Pred] -> Graph Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pred -> Graph Name
computeDependencies [Pred]
ps
  Exists (forall b. Term b -> b) -> GE a
_ Binder a
b -> Binder a -> Graph Name
forall a. Binder a -> Graph Name
computeBinderDependencies Binder a
b
  Let Term a
t Binder a
b -> Term a -> Graph Name
forall t. HasVariables t => t -> Graph Name
noDependencies Term a
t Graph Name -> Graph Name -> Graph Name
forall a. Semigroup a => a -> a -> a
<> Binder a -> Graph Name
forall a. Binder a -> Graph Name
computeBinderDependencies Binder a
b

computeBinderDependencies :: Binder a -> DependGraph
computeBinderDependencies :: forall a. Binder a -> Graph Name
computeBinderDependencies (Var a
x :-> Pred
p) =
  Name -> Graph Name -> Graph Name
forall node. Ord node => node -> Graph node -> Graph node
Graph.deleteNode (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x) (Graph Name -> Graph Name) -> Graph Name -> Graph Name
forall a b. (a -> b) -> a -> b
$ Pred -> Graph Name
computeDependencies Pred
p

computeTermDependencies :: Term a -> DependGraph
computeTermDependencies :: forall a. Term a -> Graph Name
computeTermDependencies = (Graph Name, Set Name) -> Graph Name
forall a b. (a, b) -> a
fst ((Graph Name, Set Name) -> Graph Name)
-> (Term a -> (Graph Name, Set Name)) -> Term a -> Graph Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> (Graph Name, Set Name)
forall a. Term a -> (Graph Name, Set Name)
computeTermDependencies'

computeTermDependencies' :: Term a -> (DependGraph, Set Name)
computeTermDependencies' :: forall a. Term a -> (Graph Name, Set Name)
computeTermDependencies' = \case
  (App t dom a
_ List Term dom
args) -> List Term dom -> (Graph Name, Set Name)
forall (as :: [*]). List Term as -> (Graph Name, Set Name)
go List Term dom
args
  Lit {} -> (Graph Name
forall a. Monoid a => a
mempty, Set Name
forall a. Monoid a => a
mempty)
  (V Var a
x) -> (Name -> Graph Name
forall t. HasVariables t => t -> Graph Name
noDependencies (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x), Name -> Set Name
forall a. a -> Set a
Set.singleton (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x))
  where
    go :: List Term as -> (DependGraph, Set Name)
    go :: forall (as :: [*]). List Term as -> (Graph Name, Set Name)
go List Term as
Nil = (Graph Name
forall a. Monoid a => a
mempty, Set Name
forall a. Monoid a => a
mempty)
    go (Term a
t :> List Term as1
ts) =
      let (Graph Name
gr, Set Name
ngr) = List Term as1 -> (Graph Name, Set Name)
forall (as :: [*]). List Term as -> (Graph Name, Set Name)
go List Term as1
ts
          (Graph Name
tgr, Set Name
ntgr) = Term a -> (Graph Name, Set Name)
forall a. Term a -> (Graph Name, Set Name)
computeTermDependencies' Term a
t
       in (Set Name
ntgr Set Name -> Set Name -> Graph Name
forall t t'.
(HasVariables t, HasVariables t') =>
t -> t' -> Graph Name
`irreflexiveDependencyOn` Set Name
ngr Graph Name -> Graph Name -> Graph Name
forall a. Semigroup a => a -> a -> a
<> Graph Name
tgr Graph Name -> Graph Name -> Graph Name
forall a. Semigroup a => a -> a -> a
<> Graph Name
gr, Set Name
ngr Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Set Name
ntgr)

-- | Push as much information we can backwards through the plan.
backPropagation :: SolverPlan -> SolverPlan
-- backPropagation (SolverPlan _plan _graph) =
backPropagation :: SolverPlan -> SolverPlan
backPropagation (SolverPlan [SolverStage]
initplan Graph Name
graph) = [SolverStage] -> Graph Name -> SolverPlan
SolverPlan ([SolverStage] -> [SolverStage] -> [SolverStage]
go [] ([SolverStage] -> [SolverStage]
forall a. [a] -> [a]
reverse [SolverStage]
initplan)) Graph Name
graph
  where
    go :: [SolverStage] -> [SolverStage] -> [SolverStage]
go [SolverStage]
acc [] = [SolverStage]
acc
    go [SolverStage]
acc (s :: SolverStage
s@(SolverStage (Var a
x :: Var a) [Pred]
ps Spec a
spec) : [SolverStage]
plan) = [SolverStage] -> [SolverStage] -> [SolverStage]
go (SolverStage
s SolverStage -> [SolverStage] -> [SolverStage]
forall a. a -> [a] -> [a]
: [SolverStage]
acc) [SolverStage]
plan'
      where
        newStages :: [SolverStage]
newStages = (Pred -> [SolverStage]) -> [Pred] -> [SolverStage]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Spec a -> Pred -> [SolverStage]
newStage Spec a
spec) [Pred]
ps
        plan' :: [SolverStage]
plan' = (SolverStage -> [SolverStage] -> [SolverStage])
-> [SolverStage] -> [SolverStage] -> [SolverStage]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SolverStage -> [SolverStage] -> [SolverStage]
mergeSolverStage [SolverStage]
plan [SolverStage]
newStages
        -- Note use of the Term Pattern Equal
        newStage :: Spec a -> Pred -> [SolverStage]
newStage Spec a
specl (Assert (Equal (V Var a
x') Term a
t)) =
          Spec a -> Var a -> Term a -> [SolverStage]
forall b. HasSpec b => Spec a -> Var b -> Term b -> [SolverStage]
termVarEqCases Spec a
specl Var a
x' Term a
t
        newStage Spec a
specr (Assert (Equal Term a
t (V Var a
x'))) =
          Spec a -> Var a -> Term a -> [SolverStage]
forall b. HasSpec b => Spec a -> Var b -> Term b -> [SolverStage]
termVarEqCases Spec a
specr Var a
x' Term a
t
        newStage Spec a
_ Pred
_ = []

        termVarEqCases :: HasSpec b => Spec a -> Var b -> Term b -> [SolverStage]
        termVarEqCases :: forall b. HasSpec b => Spec a -> Var b -> Term b -> [SolverStage]
termVarEqCases (MemberSpec NonEmpty a
vs) Var b
x' Term b
t
          | Name -> Set Name
forall a. a -> Set a
Set.singleton (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x) Set Name -> Set Name -> Bool
forall a. Eq a => a -> a -> Bool
== Term b -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term b
t =
              [Var b -> [Pred] -> Spec b -> SolverStage
forall a. HasSpec a => Var a -> [Pred] -> Spec a -> SolverStage
SolverStage Var b
x' [] (Spec b -> SolverStage) -> Spec b -> SolverStage
forall a b. (a -> b) -> a -> b
$ NonEmpty b -> Spec b
forall a. NonEmpty a -> Spec a
MemberSpec (NonEmpty b -> NonEmpty b
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub ((a -> b) -> NonEmpty a -> NonEmpty b
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
v -> GE b -> b
forall a. GE a -> a
errorGE (GE b -> b) -> GE b -> b
forall a b. (a -> b) -> a -> b
$ Env -> Term b -> GE b
forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm (Var a -> a -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
v) Term b
t) NonEmpty a
vs))]
        termVarEqCases Spec a
specx Var b
x' Term b
t
          | Just a :~: b
Refl <- Var a -> Var b -> Maybe (a :~: b)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var b
x'
          , [Name Var a
y] <- Set Name -> [Name]
forall a. Set a -> [a]
Set.toList (Set Name -> [Name]) -> Set Name -> [Name]
forall a b. (a -> b) -> a -> b
$ Term b -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term b
t
          , Result Ctx a b
ctx <- Var a -> Term b -> GE (Ctx a b)
forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var a
y Term b
t =
              [Var a -> [Pred] -> Spec a -> SolverStage
forall a. HasSpec a => Var a -> [Pred] -> Spec a -> SolverStage
SolverStage Var a
y [] (Ctx a b -> Spec b -> Spec a
forall v a. HasSpec v => Ctx v a -> Spec a -> Spec v
propagateSpec Ctx a b
ctx Spec a
Spec b
specx)]
        termVarEqCases Spec a
_ Var b
_ Term b
_ = []

spec9 :: Spec (Set Integer)
spec9 :: Spec (Set Integer)
spec9 = (Term (Set Integer) -> Pred) -> Spec (Set Integer)
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term (Set Integer) -> Pred) -> Spec (Set Integer))
-> (Term (Set Integer) -> Pred) -> Spec (Set Integer)
forall a b. (a -> b) -> a -> b
$ \Term (Set Integer)
x -> Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ (Term (Set Integer) -> Term Integer
forall s. (HasSpec s, Ord s) => Term (Set s) -> Term Integer
size_ Term (Set Integer)
x Term Integer -> Term Integer -> Term Integer
+. Integer -> Term Integer
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Integer
3) Term Integer -> Term Integer -> Term Bool
<=. Integer -> Term Integer
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Integer
12