{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- The pattern completeness checker is much weaker before ghc-9.0. Rather than introducing redundant
-- cases and turning off the overlap check in newer ghc versions we disable the check for old
-- versions.
#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
#endif

module Constrained.Spec.SumProd (
  IsNormalType,
  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.Base (
  BaseW (..),
  Binder (..),
  Forallable (..),
  Fun (..),
  HasSpec (..),
  IsPred (..),
  Pred (..),
  Specification (..),
  Term (..),
  Weighted (..),
  appTerm,
  bind,
  constrained,
  fromGeneric_,
  toGeneric_,
 )
import Constrained.Conformance (
  conformsToSpec,
  satisfies,
 )
import Constrained.Core (
  Evidence (..),
 )
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 (
  CountCases,
  FoldSpec (..),
  FunW (..),
  PairSpec (..),
  ProdW (..),
  SumW (..),
  ifElse,
  injLeft_,
  injRight_,
  preMapFoldSpec,
  prodFst_,
  prodSnd_,
  prod_,
 )

import Data.Typeable (Typeable)
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 = (forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> 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) = (forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term a
prodFst_ Term (Prod a b)
p) forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall p. (IsProd p, HasSpec p) => Term p -> List Term (Args p)
toArgs (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 = (Cases a ~ '[a], 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
  , Cases (SimpleRep a) ~ '[SimpleRep a]
  , SimpleRep a ~ SumOver (Cases (SimpleRep a))
  , IsProd (SimpleRep a)
  , HasSpec (SimpleRep a)
  , TypeSpec a ~ TypeSpec (SimpleRep a)
  , All HasSpec (ProductAsList 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_ = 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_ = 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_ = forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term b -> Term (Sum a b)
injRight_ 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
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_ = 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_ = 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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) =
    forall {k} (f :: k -> *) (a :: k). Maybe Int -> f a -> Weighted f a
Weighted forall a. Maybe a
Nothing (forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term b -> Pred
k)
      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
mapListC @HasSpec (\Const () a
_ -> forall {k} (f :: k -> *) (a :: k). Maybe Int -> f a -> Weighted f a
Weighted forall a. Maybe a
Nothing (forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind 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) = forall {k} (f :: k -> *) (a :: k). Maybe Int -> f a -> Weighted f a
Weighted forall a. Maybe a
Nothing (forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term b -> Pred
k) forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> 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 = forall {k} (f :: k -> *) (a :: k). Maybe Int -> f a -> Weighted f a
Weighted forall a. Maybe a
Nothing (forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind (forall a. Term a -> Pred
r @(ProdOver as))) 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 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_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm (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 forall b b1. (HasSpec b, HasSpec b1) => ProdW '[Prod b b1] b
ProdFstW 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_ = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm (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 forall a1 b. (HasSpec a1, HasSpec b) => ProdW '[Prod a1 b] b
ProdSndW 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 = (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 forall b b1. (HasSpec b, HasSpec b1) => ProdW '[Prod b b1] b
ProdFstW 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 = (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 forall a1 b. (HasSpec a1, HasSpec b) => ProdW '[Prod a1 b] b
ProdSndW 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 =
    forall a. HasCallStack => [Gen a] -> Gen a
oneof
      [ forall a b. HasSpec a => Fun '[a] b -> FoldSpec b -> FoldSpec a
preMapFoldSpec (forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun forall a b. (HasSpec a, HasSpec b) => FunW '[(a, b)] a
fstW) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
      , forall a b. HasSpec a => Fun '[a] b -> FoldSpec b -> FoldSpec a
preMapFoldSpec (forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun forall a b. (HasSpec a, HasSpec b) => FunW '[(a, b)] b
sndW) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
      , forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. FoldSpec a
NoFold
      ]
  shrink :: FoldSpec (a, b) -> [FoldSpec (a, b)]
shrink FoldSpec (a, b)
NoFold = []
  shrink FoldSpec {} = [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 = forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ forall a b. (a -> b) -> 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_ = forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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_ = forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term b -> Term (Sum a b)
injRight_

caseOn ::
  forall a.
  ( HasSpec a
  , HasSpec (SimpleRep a)
  , HasSimpleRep a
  , TypeSpec a ~ TypeSpec (SimpleRep a)
  , SimpleRep a ~ SumOver (Cases (SimpleRep a))
  , TypeList (Cases (SimpleRep a))
  ) =>
  Term a ->
  FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn :: forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep 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)) (forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
mkCase (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 = forall p. IsPred p => p -> Pred
toPred FunTy (MapList Term as) p
bd
buildBranch FunTy (MapList Term as) p
bd (Term a
t :> List Term as1
args) =
  forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind Term a
t 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
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.
  forall {k} (f :: k -> *) (a :: k). Maybe Int -> f a -> Weighted f a
Weighted forall a. Maybe a
Nothing (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 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 =
  forall {k} (f :: k -> *) (a :: k). Maybe Int -> f a -> Weighted f a
Weighted (forall a. a -> Maybe a
Just Int
w) (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. (IsProd p, HasSpec p) => Term p -> List Term (Args p)
toArgs @a))

match ::
  forall p a.
  ( HasSpec a
  , IsProductType a
  , IsPred p
  ) =>
  Term a ->
  FunTy (MapList Term (ProductAsList a)) p ->
  Pred
match :: forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term a
p FunTy (MapList Term (Args (SimpleRep a))) p
m = forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep 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))
  , HasSpec a
  , HasSimpleRep a
  , r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a)
  , ResultType r ~ Term a
  , SOPTerm c (TheSop a)
  , ConstrTerm (ConstrOf c (TheSop a))
  ) =>
  r
con :: forall (c :: Symbol) a r.
(SimpleRep a ~ SOP (TheSop a),
 TypeSpec a ~ TypeSpec (SOP (TheSop a)),
 TypeList (ConstrOf c (TheSop a)), HasSpec a, HasSimpleRep a,
 r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a),
 ResultType r ~ Term a, SOPTerm c (TheSop a),
 ConstrTerm (ConstrOf c (TheSop 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 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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)), HasSpec a, HasSimpleRep a,
 r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a),
 ResultType r ~ Term a, SOPTerm c (TheSop a),
 ConstrTerm (ConstrOf c (TheSop 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)), HasSpec a, HasSimpleRep a,
 r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a),
 ResultType r ~ Term a, SOPTerm c (TheSop a),
 ConstrTerm (ConstrOf c (TheSop a))) =>
r
con @"Nothing" (forall a. (Typeable a, Eq a, Show a) => a -> Term 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
  ) =>
  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) =>
Term a -> Term (At n as)
sel = forall (n :: Natural) (as :: [*]).
Select n as =>
Term (ProdOver as) -> Term (At n as)
select_ @n @as forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
  , HasSpec a
  ) =>
  Term t ->
  FunTy (MapList Term (Args (SimpleRep 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term t
xs FunTy (MapList Term (Args (SimpleRep a))) p
f = forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term t
xs forall a b. (a -> b) -> a -> b
$ \Term a
x -> forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
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
  , IsPred p
  ) =>
  FunTy (MapList Term (Args (SimpleRep 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, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' FunTy (MapList Term (Args (SimpleRep a))) p
f = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
x -> forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
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
  , IsPred p
  ) =>
  Term a ->
  (a -> b) ->
  FunTy (MapList Term (Args (SimpleRep 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, IsPred p) =>
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 = 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 forall a b. (a -> b) -> a -> b
$ \Term b
x -> forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
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) = forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> Term (Prod a b)
prod_ Term a
a (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)
  , TypeSpec a ~ TypeSpec (SimpleRep a)
  , HasSimpleRep a
  , HasSpec a
  , HasSpec (SimpleRep 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),
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a,
 HasSpec (SimpleRep 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 =
  forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case
    (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)
        (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Term Bool -> Pred
Assert (forall a. (Typeable a, Eq a, Show a) => a -> Term 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
  , TypeSpec a ~ TypeSpec (SimpleRep a)
  , HasSimpleRep a
  , HasSpec a
  , HasSpec (SimpleRep a)
  , SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a
  , All HasSpec (Cases (SOP (TheSop a)))
  , HasSpec (ProdOver (ConstrOf c (TheSop a)))
  ) =>
  Term a ->
  Pred
isCon :: forall (c :: Symbol) a.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a,
 HasSpec (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> Pred
isCon Term a
tm =
  forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case
    (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)
        (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Term Bool -> Pred
Assert (forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Bool
False))
        (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Term Bool -> Pred
Assert (forall a. (Typeable a, Eq a, Show a) => a -> Term 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),
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a,
 HasSpec (SimpleRep 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),
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a,
 HasSpec (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop 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') =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
x ->
    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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall b. Term b -> b
eval Term a
x forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
s) forall a b. (a -> b) -> a -> b
$ \Term Bool
b ->
      [ forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
          Term Bool
b
          (Term a
x forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
s)
          (Term a
x forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
s')
      , forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn
          Term Bool
b
          (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' forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
          (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 forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
      ]