{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module Constrained.Spec.SumProd (
  IsNormalType,
  ProdAsListComputes,
  IsProductType,
  caseOn,
  branch,
  branchW,
  forAll',
  constrained',
  reify',
  con,
  onCon,
  isCon,
  sel,
  match,
  onJust,
  isJust,
  chooseSpec,
  left_,
  right_,
  cJust_,
  cNothing_,
  fst_,
  snd_,
  fstW,
  sndW,
  pair_,
  injLeft_,
  injRight_,
  prodFst_,
  prodSnd_,
  prod_,
  PairSpec (..),
  SumW (..),
) where

import Constrained.AbstractSyntax
import Constrained.Base (
  BaseW (..),
  Binder,
  Forallable (..),
  Fun (..),
  GenericRequires,
  HasSpec (..),
  IsPred (..),
  Pred,
  Specification,
  Term,
  appTerm,
  bind,
  constrained,
  fromGeneric_,
  toGeneric_,
 )
import Constrained.Conformance (
  conformsToSpec,
  satisfies,
 )
import Constrained.Core (
  Evidence (..),
 )
import Constrained.Generation
import Constrained.Generic (
  ConstrOf,
  HasSimpleRep (..),
  Prod,
  ProdOver,
  SOP,
  SimpleRep,
  Sum,
  SumOver,
  TheSop,
  (:::),
 )
import Constrained.List (
  All,
  FunTy,
  List (..),
  MapList,
  TypeList,
  curryList,
  listShape,
  mapListC,
 )
import Constrained.Syntax (
  exists,
  forAll,
  letBind,
  mkCase,
  reify,
 )
import Constrained.TheKnot (
  FoldSpec (..),
  FunW (..),
  PairSpec (..),
  ProdW (..),
  preMapFoldSpec,
  prodFst_,
  prodSnd_,
  prod_,
 )
import Constrained.TypeErrors
import Data.Typeable (Typeable)
import GHC.Generics
import GHC.TypeLits (Symbol)
import GHC.TypeNats
import Test.QuickCheck (Arbitrary (..), oneof)

-- ==================================================================
-- Generics
-- HasSpec for various types that are Sums of Products
-- ==================================================================

instance (Typeable a, Typeable b) => HasSimpleRep (a, b)

instance (Typeable a, Typeable b, Typeable c) => HasSimpleRep (a, b, c)

instance (Typeable a, Typeable b, Typeable c, Typeable d) => HasSimpleRep (a, b, c, d)

instance (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => HasSimpleRep (a, b, c, d, e)

instance
  (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable g) =>
  HasSimpleRep (a, b, c, d, e, g)

instance
  (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable g, Typeable h) =>
  HasSimpleRep (a, b, c, d, e, g, h)

instance Typeable a => HasSimpleRep (Maybe a)

instance (Typeable a, Typeable b) => HasSimpleRep (Either a b)

instance
  ( HasSpec a
  , HasSpec b
  ) =>
  HasSpec (a, b)

instance
  ( HasSpec a
  , HasSpec b
  , HasSpec c
  ) =>
  HasSpec (a, b, c)

instance
  ( HasSpec a
  , HasSpec b
  , HasSpec c
  , HasSpec d
  ) =>
  HasSpec (a, b, c, d)

instance
  ( HasSpec a
  , HasSpec b
  , HasSpec c
  , HasSpec d
  , HasSpec e
  ) =>
  HasSpec (a, b, c, d, e)

instance
  ( HasSpec a
  , HasSpec b
  , HasSpec c
  , HasSpec d
  , HasSpec e
  , HasSpec g
  ) =>
  HasSpec (a, b, c, d, e, g)

instance
  ( HasSpec a
  , HasSpec b
  , HasSpec c
  , HasSpec d
  , HasSpec e
  , HasSpec g
  , HasSpec h
  ) =>
  HasSpec (a, b, c, d, e, g, h)

instance
  (IsNormalType a, HasSpec a) =>
  HasSpec (Maybe a)

instance
  ( HasSpec a
  , IsNormalType a
  , HasSpec b
  , IsNormalType b
  ) =>
  HasSpec (Either a b)

-- ====================================================
-- All the magic for things like 'caseOn', 'match', forAll' etc. lives here.
-- Classes and type families about Sum, Prod, construtors, selectors
-- These let us express the types of things like 'match' and 'caseOn'

class IsProd p where
  toArgs ::
    HasSpec p => Term p -> List Term (Args p)

instance {-# OVERLAPPABLE #-} Args a ~ '[a] => IsProd a where
  toArgs :: HasSpec a => Term a -> List Term (Args a)
toArgs = (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)

instance IsProd b => IsProd (Prod a b) where
  toArgs :: HasSpec (Prod a b) =>
Term (Prod a b) -> List Term (Args (Prod a b))
toArgs (Term (Prod a b)
p :: Term (Prod a b))
    | Evidence (Prerequisites (Prod a b))
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @(Prod a b) = Term (Prod a b) -> Term a
forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term a
prodFst_ Term (Prod a b)
p Term a -> List Term (Args b) -> List Term (a : Args b)
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term b -> List Term (Args b)
forall p. (IsProd p, HasSpec p) => Term p -> List Term (Args p)
toArgs (Term (Prod a b) -> Term b
forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term b
prodSnd_ Term (Prod a b)
p)

type family Args t where
  Args (Prod a b) = a : Args b
  Args a = '[a]

type family ResultType t where
  ResultType (a -> b) = ResultType b
  ResultType a = a

type IsNormalType a =
  ( AssertComputes
      (Cases a)
      ( Text "Failed to compute Cases in a use of IsNormalType for "
          :$$: ShowType a
          :<>: Text ", are you missing an IsNormalType constraint?"
      )
  , Cases a ~ '[a]
  , AssertComputes
      (Args a)
      ( Text "Failed to compute Args in a use of IsNormalType for "
          :<>: ShowType a
          :<>: Text ", are you missing an IsNormalType constraint?"
      )
  , Args a ~ '[a]
  , IsProd a
  , CountCases a ~ 1
  )

type family Cases t where
  Cases (Sum a b) = a : Cases b
  Cases a = '[a]

type IsProductType a =
  ( HasSimpleRep a
  , AssertComputes
      (Cases (SimpleRep a))
      ( Text "Failed to compute Cases in a use of IsProductType for "
          :$$: ShowType a
          :<>: Text ", are you missing an IsProductType constraint?"
      )
  , Cases (SimpleRep a) ~ '[SimpleRep a]
  , SimpleRep a ~ SumOver (Cases (SimpleRep a))
  , IsProd (SimpleRep a)
  , HasSpec (SimpleRep a)
  , TypeSpec a ~ TypeSpec (SimpleRep a)
  , All HasSpec (Args (SimpleRep a))
  )

type ProductAsList a = Args (SimpleRep a)

class HasSpec (SOP sop) => SOPTerm c sop where
  inj_ :: Term (ProdOver (ConstrOf c sop)) -> Term (SOP sop)

instance HasSpec (ProdOver constr) => SOPTerm c (c ::: constr : '[]) where
  inj_ :: Term (ProdOver (ConstrOf c '[c ::: constr]))
-> Term (SOP '[c ::: constr])
inj_ = Term (ProdOver constr) -> Term (ProdOver constr)
Term (ProdOver (ConstrOf c '[c ::: constr]))
-> Term (SOP '[c ::: constr])
forall a. a -> a
id

instance
  ( HasSpec (SOP (con : sop))
  , HasSpec (ProdOver constr)
  , KnownNat (CountCases (SOP (con : sop)))
  ) =>
  SOPTerm c (c ::: constr : con : sop)
  where
  inj_ :: Term (ProdOver (ConstrOf c ((c ::: constr) : con : sop)))
-> Term (SOP ((c ::: constr) : con : sop))
inj_ = Term (ProdOver constr)
-> Term (Sum (ProdOver constr) (SOP (con : sop)))
Term (ProdOver (ConstrOf c ((c ::: constr) : con : sop)))
-> Term (SOP ((c ::: constr) : con : sop))
forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term a -> Term (Sum a b)
injLeft_

instance
  {-# OVERLAPPABLE #-}
  ( HasSpec (ProdOver con)
  , SOPTerm c (con' : sop)
  , ConstrOf c (con' : sop) ~ ConstrOf c ((c' ::: con) : con' : sop)
  , KnownNat (CountCases (SOP (con' : sop)))
  ) =>
  SOPTerm c ((c' ::: con) : con' : sop)
  where
  inj_ :: Term (ProdOver (ConstrOf c ((c' ::: con) : con' : sop)))
-> Term (SOP ((c' ::: con) : con' : sop))
inj_ = Term (SOP (con' : sop))
-> Term (Sum (ProdOver con) (SOP (con' : sop)))
forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term b -> Term (Sum a b)
injRight_ (Term (SOP (con' : sop))
 -> Term (Sum (ProdOver con) (SOP (con' : sop))))
-> (Term (ProdOver (ConstrOf c ((c' ::: con) : con' : sop)))
    -> Term (SOP (con' : sop)))
-> Term (ProdOver (ConstrOf c ((c' ::: con) : con' : sop)))
-> Term (Sum (ProdOver con) (SOP (con' : sop)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: Symbol) (sop :: [*]).
SOPTerm c sop =>
Term (ProdOver (ConstrOf c sop)) -> Term (SOP sop)
inj_ @c @(con' : sop)

class HasSpec (ProdOver constr) => ConstrTerm constr where
  prodOver_ :: List Term constr -> Term (ProdOver constr)

instance HasSpec a => ConstrTerm '[a] where
  prodOver_ :: List Term '[a] -> Term (ProdOver '[a])
prodOver_ (Term a
a :> List Term as1
Nil) = Term a
Term (ProdOver '[a])
a

type family At n as where
  At 0 (a : as) = a
  At n (a : as) = At (n - 1) as

class Select n as where
  select_ :: Term (ProdOver as) -> Term (At n as)

instance Select 0 (a : '[]) where
  select_ :: Term (ProdOver '[a]) -> Term (At 0 '[a])
select_ = Term a -> Term a
Term (ProdOver '[a]) -> Term (At 0 '[a])
forall a. a -> a
id

instance (HasSpec a, HasSpec (ProdOver (a' : as))) => Select 0 (a : a' : as) where
  select_ :: Term (ProdOver (a : a' : as)) -> Term (At 0 (a : a' : as))
select_ = Term (ProdOver (a : a' : as)) -> Term (At 0 (a : a' : as))
Term (Prod a (ProdOver (a' : as))) -> Term a
forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term a
prodFst_

instance
  {-# OVERLAPPABLE #-}
  ( HasSpec a
  , HasSpec (ProdOver (a' : as))
  , At (n - 1) (a' : as) ~ At n (a : a' : as)
  , Select (n - 1) (a' : as)
  ) =>
  Select n (a : a' : as)
  where
  select_ :: Term (ProdOver (a : a' : as)) -> Term (At n (a : a' : as))
select_ = forall (n :: Natural) (as :: [*]).
Select n as =>
Term (ProdOver as) -> Term (At n as)
select_ @(n - 1) @(a' : as) (Term (ProdOver (a' : as)) -> Term (At n (a : a' : as)))
-> (Term (Prod a (ProdOver (a' : as)))
    -> Term (ProdOver (a' : as)))
-> Term (Prod a (ProdOver (a' : as)))
-> Term (At n (a : a' : as))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (Prod a (ProdOver (a' : as))) -> Term (ProdOver (a' : as))
forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term b
prodSnd_

class IsConstrOf (c :: Symbol) b sop where
  mkCases ::
    (HasSpec b, All HasSpec (Cases (SOP sop))) =>
    (forall a. Term a -> Pred) ->
    (Term b -> Pred) ->
    List (Weighted Binder) (Cases (SOP sop))

instance
  ( b ~ ProdOver as
  , TypeList (Cases (SOP (con : sop)))
  ) =>
  IsConstrOf c b ((c ::: as) : con : sop)
  where
  mkCases :: (HasSpec b, All HasSpec (Cases (SOP ((c ::: as) : con : sop)))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred)
-> List (Weighted Binder) (Cases (SOP ((c ::: as) : con : sop)))
mkCases forall a. Term a -> Pred
r (Term b -> Pred
k :: Term b -> Pred) =
    Maybe Int -> Binder b -> Weighted Binder b
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
forall a. Maybe a
Nothing ((Term b -> Pred) -> Binder b
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term b -> Pred
k)
      Weighted Binder b
-> List (Weighted Binder) (Cases (SOP (con : sop)))
-> List (Weighted Binder) (b : Cases (SOP (con : sop)))
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *).
All c as =>
(forall (a :: k). c a => f a -> g a) -> List f as -> List g as
forall (c :: * -> Constraint) (as :: [*]) (f :: * -> *)
       (g :: * -> *).
All c as =>
(forall a. c a => f a -> g a) -> List f as -> List g as
mapListC @HasSpec (\Const () a
_ -> Maybe Int -> Binder a -> Weighted Binder a
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
forall a. Maybe a
Nothing ((Term a -> Pred) -> Binder a
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term a -> Pred
forall a. Term a -> Pred
r)) (forall (as :: [*]). TypeList as => List (Const ()) as
listShape @(Cases (SOP (con : sop))))

instance
  ( b ~ ProdOver as
  , IsNormalType b
  ) =>
  IsConstrOf c b '[c ::: as]
  where
  mkCases :: (HasSpec b, All HasSpec (Cases (SOP '[c ::: as]))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred)
-> List (Weighted Binder) (Cases (SOP '[c ::: as]))
mkCases forall a. Term a -> Pred
_ (Term b -> Pred
k :: Term b -> Pred) = Maybe Int -> Binder b -> Weighted Binder b
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
forall a. Maybe a
Nothing ((Term b -> Pred) -> Binder b
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term b -> Pred
k) Weighted Binder b
-> List (Weighted Binder) '[] -> List (Weighted Binder) '[b]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List (Weighted Binder) '[]
forall {k} (f :: k -> *). List f '[]
Nil

instance
  {-# OVERLAPPABLE #-}
  ( Cases (SOP ((c' ::: as) : cs)) ~ (ProdOver as : Cases (SOP cs))
  , IsConstrOf c b cs
  ) =>
  IsConstrOf c b ((c' ::: as) : cs)
  where
  mkCases :: (HasSpec b, All HasSpec (Cases (SOP ((c' ::: as) : cs)))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred)
-> List (Weighted Binder) (Cases (SOP ((c' ::: as) : cs)))
mkCases forall a. Term a -> Pred
r Term b -> Pred
k = Maybe Int -> Binder (ProdOver as) -> Weighted Binder (ProdOver as)
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
forall a. Maybe a
Nothing ((Term (ProdOver as) -> Pred) -> Binder (ProdOver as)
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind (forall a. Term a -> Pred
r @(ProdOver as))) Weighted Binder (ProdOver as)
-> List (Weighted Binder) (Cases (SOP cs))
-> List (Weighted Binder) (ProdOver as : Cases (SOP cs))
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall (c :: Symbol) b (sop :: [*]).
(IsConstrOf c b sop, HasSpec b, All HasSpec (Cases (SOP sop))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred) -> List (Weighted Binder) (Cases (SOP sop))
mkCases @c @_ @cs Term a -> Pred
forall a. Term a -> Pred
r Term b -> Pred
k

------------------------------------------------------------------------
-- Syntax
------------------------------------------------------------------------

fst_ :: (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ :: forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ = FunW '[(x, y)] x -> FunTy (MapList Term '[(x, y)]) (TermD Deps x)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm (ProdW '[Prod x y] x
-> BaseW '[(x, y)] (Prod x y) -> FunW '[(x, y)] x
forall b (t1 :: [*] -> * -> *) (t2 :: [*] -> * -> *) a rng.
(AppRequires t1 '[b] rng, AppRequires t2 '[a] b, HasSpec b) =>
t1 '[b] rng -> t2 '[a] b -> FunW '[a] rng
ComposeW ProdW '[Prod x y] x
forall b b1. (HasSpec b, HasSpec b1) => ProdW '[Prod b b1] b
ProdFstW BaseW '[(x, y)] (SimpleRep (x, y))
BaseW '[(x, y)] (Prod x y)
forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW)

snd_ :: (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ :: forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ = FunW '[(x, y)] y -> FunTy (MapList Term '[(x, y)]) (TermD Deps y)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm (ProdW '[Prod x y] y
-> BaseW '[(x, y)] (Prod x y) -> FunW '[(x, y)] y
forall b (t1 :: [*] -> * -> *) (t2 :: [*] -> * -> *) a rng.
(AppRequires t1 '[b] rng, AppRequires t2 '[a] b, HasSpec b) =>
t1 '[b] rng -> t2 '[a] b -> FunW '[a] rng
ComposeW ProdW '[Prod x y] y
forall a1 b. (HasSpec a1, HasSpec b) => ProdW '[Prod a1 b] b
ProdSndW BaseW '[(x, y)] (SimpleRep (x, y))
BaseW '[(x, y)] (Prod x y)
forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW)

fstW :: (HasSpec a, HasSpec b) => FunW '[(a, b)] a
fstW :: forall a b. (HasSpec a, HasSpec b) => FunW '[(a, b)] a
fstW = ProdW '[Prod a b] a
-> BaseW '[(a, b)] (Prod a b) -> FunW '[(a, b)] a
forall b (t1 :: [*] -> * -> *) (t2 :: [*] -> * -> *) a rng.
(AppRequires t1 '[b] rng, AppRequires t2 '[a] b, HasSpec b) =>
t1 '[b] rng -> t2 '[a] b -> FunW '[a] rng
ComposeW ProdW '[Prod a b] a
forall b b1. (HasSpec b, HasSpec b1) => ProdW '[Prod b b1] b
ProdFstW BaseW '[(a, b)] (SimpleRep (a, b))
BaseW '[(a, b)] (Prod a b)
forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW

sndW :: (HasSpec a, HasSpec b) => FunW '[(a, b)] b
sndW :: forall a b. (HasSpec a, HasSpec b) => FunW '[(a, b)] b
sndW = ProdW '[Prod a b] b
-> BaseW '[(a, b)] (Prod a b) -> FunW '[(a, b)] b
forall b (t1 :: [*] -> * -> *) (t2 :: [*] -> * -> *) a rng.
(AppRequires t1 '[b] rng, AppRequires t2 '[a] b, HasSpec b) =>
t1 '[b] rng -> t2 '[a] b -> FunW '[a] rng
ComposeW ProdW '[Prod a b] b
forall a1 b. (HasSpec a1, HasSpec b) => ProdW '[Prod a1 b] b
ProdSndW BaseW '[(a, b)] (SimpleRep (a, b))
BaseW '[(a, b)] (Prod a b)
forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW

instance
  (HasSpec a, HasSpec b, Arbitrary (FoldSpec a), Arbitrary (FoldSpec b)) =>
  Arbitrary (FoldSpec (a, b))
  where
  arbitrary :: Gen (FoldSpec (a, b))
arbitrary =
    [Gen (FoldSpec (a, b))] -> Gen (FoldSpec (a, b))
forall a. HasCallStack => [Gen a] -> Gen a
oneof
      [ Fun '[(a, b)] a -> FoldSpec a -> FoldSpec (a, b)
forall a b. HasSpec a => Fun '[a] b -> FoldSpec b -> FoldSpec a
preMapFoldSpec (FunW '[(a, b)] a -> Fun '[(a, b)] a
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun FunW '[(a, b)] a
forall a b. (HasSpec a, HasSpec b) => FunW '[(a, b)] a
fstW) (FoldSpec a -> FoldSpec (a, b))
-> Gen (FoldSpec a) -> Gen (FoldSpec (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (FoldSpec a)
forall a. Arbitrary a => Gen a
arbitrary
      , Fun '[(a, b)] b -> FoldSpec b -> FoldSpec (a, b)
forall a b. HasSpec a => Fun '[a] b -> FoldSpec b -> FoldSpec a
preMapFoldSpec (FunW '[(a, b)] b -> Fun '[(a, b)] b
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun FunW '[(a, b)] b
forall a b. (HasSpec a, HasSpec b) => FunW '[(a, b)] b
sndW) (FoldSpec b -> FoldSpec (a, b))
-> Gen (FoldSpec b) -> Gen (FoldSpec (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (FoldSpec b)
forall a. Arbitrary a => Gen a
arbitrary
      , FoldSpec (a, b) -> Gen (FoldSpec (a, b))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec (a, b)
forall a. FoldSpec a
NoFold
      ]
  shrink :: FoldSpec (a, b) -> [FoldSpec (a, b)]
shrink FoldSpec (a, b)
NoFold = []
  shrink FoldSpec {} = [FoldSpec (a, b)
forall a. FoldSpec a
NoFold]

pair_ ::
  ( HasSpec a
  , HasSpec b
  , IsNormalType a
  , IsNormalType b
  ) =>
  Term a ->
  Term b ->
  Term (a, b)
pair_ :: forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term a
x Term b
y = Term (SimpleRep (a, b)) -> Term (a, b)
forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ (Term (SimpleRep (a, b)) -> Term (a, b))
-> Term (SimpleRep (a, b)) -> Term (a, b)
forall a b. (a -> b) -> a -> b
$ Term a -> Term b -> Term (Prod a b)
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> Term (Prod a b)
prod_ Term a
x Term b
y

left_ ::
  ( HasSpec a
  , HasSpec b
  , IsNormalType a
  , IsNormalType b
  ) =>
  Term a ->
  Term (Either a b)
left_ :: forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term (Either a b)
left_ = Term (SimpleRep (Either a b)) -> Term (Either a b)
TermD Deps (Sum a b) -> Term (Either a b)
forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ (TermD Deps (Sum a b) -> Term (Either a b))
-> (Term a -> TermD Deps (Sum a b)) -> Term a -> Term (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> TermD Deps (Sum a b)
forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term a -> Term (Sum a b)
injLeft_

right_ ::
  ( HasSpec a
  , HasSpec b
  , IsNormalType a
  , IsNormalType b
  ) =>
  Term b ->
  Term (Either a b)
right_ :: forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term b -> Term (Either a b)
right_ = Term (SimpleRep (Either a b)) -> Term (Either a b)
TermD Deps (Sum a b) -> Term (Either a b)
forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ (TermD Deps (Sum a b) -> Term (Either a b))
-> (Term b -> TermD Deps (Sum a b)) -> Term b -> Term (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term b -> TermD Deps (Sum a b)
forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term b -> Term (Sum a b)
injRight_

caseOn ::
  forall a.
  ( GenericRequires a
  , SimpleRep a ~ SumOver (Cases (SimpleRep a))
  , TypeList (Cases (SimpleRep a))
  ) =>
  Term a ->
  FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn :: forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term a
tm = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
curryList @(Cases (SimpleRep a)) (Term (SumOver (Cases (SimpleRep a)))
-> List (Weighted Binder) (Cases (SimpleRep a)) -> Pred
forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
mkCase (Term a -> Term (SimpleRep a)
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term a
tm))

buildBranch ::
  forall p as.
  ( All HasSpec as
  , IsPred p
  ) =>
  FunTy (MapList Term as) p ->
  List Term as ->
  Pred
buildBranch :: forall p (as :: [*]).
(All HasSpec as, IsPred p) =>
FunTy (MapList Term as) p -> List Term as -> Pred
buildBranch FunTy (MapList Term as) p
bd List Term as
Nil = p -> Pred
forall p. IsPred p => p -> Pred
toPred p
FunTy (MapList Term as) p
bd
buildBranch FunTy (MapList Term as) p
bd (Term a
t :> List Term as1
args) =
  Term a -> (Term a -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind Term a
t ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x -> forall p (as :: [*]).
(All HasSpec as, IsPred p) =>
FunTy (MapList Term as) p -> List Term as -> Pred
buildBranch @p (FunTy (MapList Term as) p
Term a -> FunTy (MapList Term as1) p
bd Term a
x) List Term as1
args

branch ::
  forall p a.
  ( HasSpec a
  , All HasSpec (Args a)
  , IsPred p
  , IsProd a
  ) =>
  FunTy (MapList Term (Args a)) p ->
  Weighted Binder a
branch :: forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch FunTy (MapList Term (Args a)) p
body =
  -- NOTE: It's not sufficient to simply apply `body` to all the arguments
  -- with `uncurryList` because that will mean that `var` is repeated in the
  -- body. For example, consider `branch $ \ i j -> i <=. j`. If we don't
  -- build the lets this will boil down to `p :-> fst p <=. snd p` which
  -- will blow up at generation time. If we instead do: `p :-> Let x (fst p) (Let y (snd p) (x <=. y))`
  -- the solver will solve `x` and `y` separately (`y` before `x` in this case) and things
  -- will work just fine.
  Maybe Int -> Binder a -> Weighted Binder a
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
forall a. Maybe a
Nothing ((Term a -> Pred) -> Binder a
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind (forall p (as :: [*]).
(All HasSpec as, IsPred p) =>
FunTy (MapList Term as) p -> List Term as -> Pred
buildBranch @p FunTy (MapList Term (Args a)) p
body (List Term (Args a) -> Pred)
-> (Term a -> List Term (Args a)) -> Term a -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. (IsProd p, HasSpec p) => Term p -> List Term (Args p)
toArgs @a))

branchW ::
  forall p a.
  ( HasSpec a
  , All HasSpec (Args a)
  , IsPred p
  , IsProd a
  ) =>
  Int ->
  FunTy (MapList Term (Args a)) p ->
  Weighted Binder a
branchW :: forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
w FunTy (MapList Term (Args a)) p
body =
  Maybe Int -> Binder a -> Weighted Binder a
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
w) ((Term a -> Pred) -> Binder a
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind (forall p (as :: [*]).
(All HasSpec as, IsPred p) =>
FunTy (MapList Term as) p -> List Term as -> Pred
buildBranch @p FunTy (MapList Term (Args a)) p
body (List Term (Args a) -> Pred)
-> (Term a -> List Term (Args a)) -> Term a -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. (IsProd p, HasSpec p) => Term p -> List Term (Args p)
toArgs @a))

-- | ProdAsListComputes is here to make sure that in situations like this:
--
-- > type family Foobar k
-- >
-- > ex :: HasSpec (Foobar k) => Specification (Int, Foobar k)
-- > ex = constrained $ \ p -> match p $ \ i _ -> (i ==. 10)
--
-- Where you're trying to work with an unevaluated type family in constraints.
-- You get reasonable type errors prompting you to add the @IsNormalType (Foobar k)@ constraint
-- like this:
--
-- >     • Type list computation is stuck on
-- >         Args (Foobar k)
-- >       Have you considered adding an IsNormalType or ProdAsListComputes constraint?
-- >     • In the first argument of ‘($)’, namely ‘match p’
-- >       In the expression: match p $ \ i _ -> (i ==. 10)
-- >       In the second argument of ‘($)’, namely
-- >         ‘\ p -> match p $ \ i _ -> (i ==. 10)’
-- >     |
-- > 503 | ex = constrained $ \ p -> match p $ \ i _ -> (i ==. 10)
-- >     |                           ^^^^^
--
-- Which should help you come to the conclusion that you need to do something
-- like this for everything to compile:
--
-- > ex :: (HasSpec (Foobar k), IsNormalType (Foobar k)) => Specification (Int, Foobar k)
type ProdAsListComputes a =
  AssertSpineComputes
    (Text "Have you considered adding an IsNormalType or ProdAsListComputes constraint?")
    (ProductAsList a)

match ::
  forall p a.
  ( IsProductType a
  , IsPred p
  , GenericRequires a
  , ProdAsListComputes a
  ) =>
  Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match :: forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term a
p FunTy (MapList Term (Args (SimpleRep a))) p
m = Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term a
p (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch @p FunTy (MapList Term (Args (SimpleRep a))) p
m)

-- NOTE: `ResultType r ~ Term a` is NOT a redundant constraint,
-- removing it causes type inference to break elsewhere
con ::
  forall c a r.
  ( SimpleRep a ~ SOP (TheSop a)
  , TypeSpec a ~ TypeSpec (SOP (TheSop a))
  , TypeList (ConstrOf c (TheSop a))
  , r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a)
  , ResultType r ~ Term a
  , SOPTerm c (TheSop a)
  , ConstrTerm (ConstrOf c (TheSop a))
  , GenericRequires a
  ) =>
  r
con :: forall (c :: Symbol) a r.
(SimpleRep a ~ SOP (TheSop a),
 TypeSpec a ~ TypeSpec (SOP (TheSop a)),
 TypeList (ConstrOf c (TheSop a)),
 r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a),
 ResultType r ~ Term a, SOPTerm c (TheSop a),
 ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) =>
r
con =
  forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
curryList @(ConstrOf c (TheSop a)) @Term
    (forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ @a (TermD Deps (SOP (TheSop a)) -> Term a)
-> (List Term (ConstrOf c (TheSop a))
    -> TermD Deps (SOP (TheSop a)))
-> List Term (ConstrOf c (TheSop a))
-> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: Symbol) (sop :: [*]).
SOPTerm c sop =>
Term (ProdOver (ConstrOf c sop)) -> Term (SOP sop)
inj_ @c @(TheSop a) (Term (ProdOver (ConstrOf c (TheSop a)))
 -> TermD Deps (SOP (TheSop a)))
-> (List Term (ConstrOf c (TheSop a))
    -> Term (ProdOver (ConstrOf c (TheSop a))))
-> List Term (ConstrOf c (TheSop a))
-> TermD Deps (SOP (TheSop a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List Term (ConstrOf c (TheSop a))
-> Term (ProdOver (ConstrOf c (TheSop a)))
forall (constr :: [*]).
ConstrTerm constr =>
List Term constr -> Term (ProdOver constr)
prodOver_)

cJust_ :: (HasSpec a, IsNormalType a) => Term a -> Term (Maybe a)
cJust_ :: forall a. (HasSpec a, IsNormalType a) => Term a -> Term (Maybe a)
cJust_ = forall (c :: Symbol) a r.
(SimpleRep a ~ SOP (TheSop a),
 TypeSpec a ~ TypeSpec (SOP (TheSop a)),
 TypeList (ConstrOf c (TheSop a)),
 r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a),
 ResultType r ~ Term a, SOPTerm c (TheSop a),
 ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) =>
r
con @"Just"

cNothing_ :: (HasSpec a, IsNormalType a) => Term (Maybe a)
cNothing_ :: forall a. (HasSpec a, IsNormalType a) => Term (Maybe a)
cNothing_ = forall (c :: Symbol) a r.
(SimpleRep a ~ SOP (TheSop a),
 TypeSpec a ~ TypeSpec (SOP (TheSop a)),
 TypeList (ConstrOf c (TheSop a)),
 r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a),
 ResultType r ~ Term a, SOPTerm c (TheSop a),
 ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) =>
r
con @"Nothing" (() -> TermD Deps ()
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit ())

sel ::
  forall n a c as.
  ( SimpleRep a ~ ProdOver as
  , -- TODO: possibly investigate deriving this from the actual SOP of SimpleRep, as currently it's buggy if you define
    -- your own custom SOP-like SimpleRep by defining SimpleRep rather than TheSop (it's stupid I know)
    TheSop a ~ '[c ::: as]
  , TypeSpec a ~ TypeSpec (ProdOver as)
  , Select n as
  , HasSpec a
  , HasSpec (ProdOver as)
  , HasSimpleRep a
  , GenericRequires a
  ) =>
  Term a ->
  Term (At n as)
sel :: forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel = forall (n :: Natural) (as :: [*]).
Select n as =>
Term (ProdOver as) -> Term (At n as)
select_ @n @as (Term (ProdOver as) -> Term (At n as))
-> (Term a -> Term (ProdOver as)) -> Term a -> Term (At n as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> Term (SimpleRep a)
Term a -> Term (ProdOver as)
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_

-- | Like `forAll` but pattern matches on the `Term a`
forAll' ::
  forall t a p.
  ( Forallable t a
  , Cases (SimpleRep a) ~ '[SimpleRep a]
  , TypeSpec a ~ TypeSpec (SimpleRep a)
  , HasSpec t
  , HasSpec (SimpleRep a)
  , HasSimpleRep a
  , All HasSpec (Args (SimpleRep a))
  , IsPred p
  , IsProd (SimpleRep a)
  , IsProductType a
  , HasSpec a
  , GenericRequires a
  , ProdAsListComputes a
  ) =>
  Term t ->
  FunTy (MapList Term (ProductAsList a)) p ->
  Pred
forAll' :: forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term t
xs FunTy (MapList Term (Args (SimpleRep a))) p
f = Term t -> (Term a -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term t
xs ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x -> forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match @p Term a
x FunTy (MapList Term (Args (SimpleRep a))) p
f

-- | Like `constrained` but pattern matches on the bound `Term a`
constrained' ::
  forall a p.
  ( Cases (SimpleRep a) ~ '[SimpleRep a]
  , TypeSpec a ~ TypeSpec (SimpleRep a)
  , HasSpec (SimpleRep a)
  , HasSimpleRep a
  , All HasSpec (Args (SimpleRep a))
  , IsProd (SimpleRep a)
  , HasSpec a
  , IsProductType a
  , IsPred p
  , GenericRequires a
  , ProdAsListComputes a
  ) =>
  FunTy (MapList Term (ProductAsList a)) p ->
  Specification a
constrained' :: forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' FunTy (MapList Term (Args (SimpleRep a))) p
f = (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x -> forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match @p Term a
x FunTy (MapList Term (Args (SimpleRep a))) p
f

-- | Like `reify` but pattern matches on the bound `Term b`
reify' ::
  forall a b p.
  ( Cases (SimpleRep b) ~ '[SimpleRep b]
  , TypeSpec b ~ TypeSpec (SimpleRep b)
  , HasSpec (SimpleRep b)
  , HasSimpleRep b
  , All HasSpec (Args (SimpleRep b))
  , IsProd (SimpleRep b)
  , HasSpec a
  , HasSpec b
  , IsProductType b
  , IsProd a
  , IsPred p
  , GenericRequires b
  , ProdAsListComputes b
  ) =>
  Term a ->
  (a -> b) ->
  FunTy (MapList Term (ProductAsList b)) p ->
  Pred
reify' :: forall a b p.
(Cases (SimpleRep b) ~ '[SimpleRep b],
 TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b),
 HasSimpleRep b, All HasSpec (Args (SimpleRep b)),
 IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b,
 IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) =>
Term a
-> (a -> b) -> FunTy (MapList Term (Args (SimpleRep b))) p -> Pred
reify' Term a
a a -> b
r FunTy (MapList Term (Args (SimpleRep b))) p
f = Term a -> (a -> b) -> (Term b -> Pred) -> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term a
a a -> b
r ((Term b -> Pred) -> Pred) -> (Term b -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term b
x -> forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match @p Term b
x FunTy (MapList Term (Args (SimpleRep b))) p
f

instance
  ( HasSpec a
  , HasSpec (ProdOver (a : b : as))
  , ConstrTerm (b : as)
  ) =>
  ConstrTerm (a : b : as)
  where
  prodOver_ :: List Term (a : b : as) -> Term (ProdOver (a : b : as))
prodOver_ (Term a
a :> List Term as1
as) = Term a
-> Term (ProdOver (b : as)) -> Term (Prod a (ProdOver (b : as)))
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> Term (Prod a b)
prod_ Term a
a (List Term as1 -> Term (ProdOver as1)
forall (constr :: [*]).
ConstrTerm constr =>
List Term constr -> Term (ProdOver constr)
prodOver_ List Term as1
as)

-- TODO: the constraints around this are horrible!! We should figure out a way to make these things nicer.
onCon ::
  forall c a p.
  ( IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a)
  , GenericRequires a
  , SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a
  , All HasSpec (Cases (SOP (TheSop a)))
  , HasSpec (ProdOver (ConstrOf c (TheSop a)))
  , IsPred p
  , Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a)
  , All HasSpec (ConstrOf c (TheSop a))
  , IsProd (ProdOver (ConstrOf c (TheSop a)))
  ) =>
  Term a ->
  FunTy (MapList Term (ConstrOf c (TheSop a))) p ->
  Pred
onCon :: forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon Term a
tm FunTy (MapList Term (ConstrOf c (TheSop a))) p
p =
  TermD Deps (SumOver (Cases (SOP (TheSop a))))
-> List (Weighted Binder) (Cases (SOP (TheSop a))) -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case
    (Term a -> Term (SimpleRep a)
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term a
tm)
    ( forall (c :: Symbol) b (sop :: [*]).
(IsConstrOf c b sop, HasSpec b, All HasSpec (Cases (SOP sop))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred) -> List (Weighted Binder) (Cases (SOP sop))
mkCases @c @(ProdOver (ConstrOf c (TheSop a))) @(TheSop a)
        (Pred -> Term a -> Pred
forall a b. a -> b -> a
const (Pred -> Term a -> Pred) -> Pred -> Term a -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Bool -> TermD Deps Bool
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit Bool
True))
        (forall p (as :: [*]).
(All HasSpec as, IsPred p) =>
FunTy (MapList Term as) p -> List Term as -> Pred
buildBranch @p FunTy (MapList Term (ConstrOf c (TheSop a))) p
p (List Term (ConstrOf c (TheSop a)) -> Pred)
-> (Term (ProdOver (ConstrOf c (TheSop a)))
    -> List Term (ConstrOf c (TheSop a)))
-> Term (ProdOver (ConstrOf c (TheSop a)))
-> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (ProdOver (ConstrOf c (TheSop a)))
-> List Term (ConstrOf c (TheSop a))
Term (ProdOver (ConstrOf c (TheSop a)))
-> List Term (Args (ProdOver (ConstrOf c (TheSop a))))
forall p. (IsProd p, HasSpec p) => Term p -> List Term (Args p)
toArgs)
    )

isCon ::
  forall c a.
  ( IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a)
  , SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a
  , All HasSpec (Cases (SOP (TheSop a)))
  , HasSpec (ProdOver (ConstrOf c (TheSop a)))
  , GenericRequires a
  ) =>
  Term a ->
  Pred
isCon :: forall (c :: Symbol) a.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) =>
Term a -> Pred
isCon Term a
tm =
  TermD Deps (SumOver (Cases (SOP (TheSop a))))
-> List (Weighted Binder) (Cases (SOP (TheSop a))) -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case
    (Term a -> Term (SimpleRep a)
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term a
tm)
    ( forall (c :: Symbol) b (sop :: [*]).
(IsConstrOf c b sop, HasSpec b, All HasSpec (Cases (SOP sop))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred) -> List (Weighted Binder) (Cases (SOP sop))
mkCases @c @(ProdOver (ConstrOf c (TheSop a))) @(TheSop a)
        (Pred -> Term a -> Pred
forall a b. a -> b -> a
const (Pred -> Term a -> Pred) -> Pred -> Term a -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Bool -> TermD Deps Bool
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit Bool
False))
        (Pred -> Term (ProdOver (ConstrOf c (TheSop a))) -> Pred
forall a b. a -> b -> a
const (Pred -> Term (ProdOver (ConstrOf c (TheSop a))) -> Pred)
-> Pred -> Term (ProdOver (ConstrOf c (TheSop a))) -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Bool -> TermD Deps Bool
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit Bool
True))
    )

onJust ::
  forall a p.
  (HasSpec a, IsNormalType a, IsPred p) =>
  Term (Maybe a) ->
  (Term a -> p) ->
  Pred
onJust :: forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust = forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"Just"

isJust ::
  forall a.
  (HasSpec a, IsNormalType a) =>
  Term (Maybe a) ->
  Pred
isJust :: forall a. (HasSpec a, IsNormalType a) => Term (Maybe a) -> Pred
isJust = forall (c :: Symbol) a.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) =>
Term a -> Pred
isCon @"Just"

-- |  ChooseSpec is one of the ways we can 'Or' two Specs together
--    This works for any kind of type that has a HasSpec instance.
--    If your type is a Sum type. One can use CaseOn which is much easier.
chooseSpec ::
  HasSpec a =>
  (Int, Specification a) ->
  (Int, Specification a) ->
  Specification a
chooseSpec :: forall a.
HasSpec a =>
(Int, Specification a) -> (Int, Specification a) -> Specification a
chooseSpec (Int
w, Specification a
s) (Int
w', Specification a
s') =
  (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x ->
    ((forall b. Term b -> b) -> GE Picky)
-> (Term Picky -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> Picky -> GE Picky
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Picky -> GE Picky) -> Picky -> GE Picky
forall a b. (a -> b) -> a -> b
$ if Term a -> a
forall b. Term b -> b
eval Term a
x a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
s then Picky
PickFirst else Picky
PickSecond) ((Term Picky -> Pred) -> Pred) -> (Term Picky -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Picky
p ->
      Term Picky
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep Picky))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn
        Term Picky
p
        (Int -> FunTy (MapList Term (Args ())) Pred -> Weighted Binder ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
w' (FunTy (MapList Term (Args ())) Pred -> Weighted Binder ())
-> FunTy (MapList Term (Args ())) Pred -> Weighted Binder ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> (Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
s))
        (Int -> FunTy (MapList Term (Args ())) Pred -> Weighted Binder ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
w (FunTy (MapList Term (Args ())) Pred -> Weighted Binder ())
-> FunTy (MapList Term (Args ())) Pred -> Weighted Binder ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> (Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
s'))

data Picky = PickFirst | PickSecond deriving (Eq Picky
Eq Picky =>
(Picky -> Picky -> Ordering)
-> (Picky -> Picky -> Bool)
-> (Picky -> Picky -> Bool)
-> (Picky -> Picky -> Bool)
-> (Picky -> Picky -> Bool)
-> (Picky -> Picky -> Picky)
-> (Picky -> Picky -> Picky)
-> Ord Picky
Picky -> Picky -> Bool
Picky -> Picky -> Ordering
Picky -> Picky -> Picky
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Picky -> Picky -> Ordering
compare :: Picky -> Picky -> Ordering
$c< :: Picky -> Picky -> Bool
< :: Picky -> Picky -> Bool
$c<= :: Picky -> Picky -> Bool
<= :: Picky -> Picky -> Bool
$c> :: Picky -> Picky -> Bool
> :: Picky -> Picky -> Bool
$c>= :: Picky -> Picky -> Bool
>= :: Picky -> Picky -> Bool
$cmax :: Picky -> Picky -> Picky
max :: Picky -> Picky -> Picky
$cmin :: Picky -> Picky -> Picky
min :: Picky -> Picky -> Picky
Ord, Picky -> Picky -> Bool
(Picky -> Picky -> Bool) -> (Picky -> Picky -> Bool) -> Eq Picky
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Picky -> Picky -> Bool
== :: Picky -> Picky -> Bool
$c/= :: Picky -> Picky -> Bool
/= :: Picky -> Picky -> Bool
Eq, Int -> Picky -> ShowS
[Picky] -> ShowS
Picky -> String
(Int -> Picky -> ShowS)
-> (Picky -> String) -> ([Picky] -> ShowS) -> Show Picky
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Picky -> ShowS
showsPrec :: Int -> Picky -> ShowS
$cshow :: Picky -> String
show :: Picky -> String
$cshowList :: [Picky] -> ShowS
showList :: [Picky] -> ShowS
Show, (forall x. Picky -> Rep Picky x)
-> (forall x. Rep Picky x -> Picky) -> Generic Picky
forall x. Rep Picky x -> Picky
forall x. Picky -> Rep Picky x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Picky -> Rep Picky x
from :: forall x. Picky -> Rep Picky x
$cto :: forall x. Rep Picky x -> Picky
to :: forall x. Rep Picky x -> Picky
Generic)

instance HasSimpleRep Picky

instance HasSpec Picky