{-# 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 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,
  IsProductType,
  ProductAsList,
  caseOn,
  branch,
  branchW,
  forAll',
  constrained',
  reify',
  con,
  onCon,
  isCon,
  sel,
  match,
  onJust,
  isJust,
  chooseSpec,
  left_,
  right_,
  cJust_,
  cNothing_,
  fst_,
  snd_,
  fstW,
  sndW,
  pair_,
  leftFn,
  rightFn,
  prodFst_,
  prodSnd_,
  prod_,
  PairSpec (..),
) where

import Constrained.Base
import Constrained.Conformance (conformsToSpec, satisfies)
import Constrained.Core (Evidence (..), NonEmpty ((:|)))
import Constrained.Generic
import Constrained.List
import Constrained.Spec.ListFoldy
import Constrained.Syntax (exists, forAll, letBind, mkCase, reify)
import Constrained.TheKnot
import qualified Data.List.NonEmpty as NE
import Data.Typeable (Typeable)
import GHC.TypeLits (Symbol)
import GHC.TypeNats
import Test.QuickCheck (Arbitrary (..), oneof)

-- ==================================================================
-- The HasSpec instance for Sum is in TheKnot.
-- Here are the Logic Instances for Sum
-- ===================================================================

-- ============= InjLeftW ====

instance (HasSpec a, HasSpec b, KnownNat (CountCases b)) => Logic "leftFn" BaseW '[a] (Sum a b) where
  propagate :: forall hole.
Context "leftFn" BaseW '[a] (Sum a b) hole
-> Specification (Sum a b) -> Specification hole
propagate Context "leftFn" BaseW '[a] (Sum a b) hole
ctxt (ExplainSpec [] Specification (Sum a b)
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "leftFn" BaseW '[a] (Sum a b) hole
ctxt Specification (Sum a b)
s
  propagate Context "leftFn" BaseW '[a] (Sum a b) hole
ctxt (ExplainSpec [String]
es Specification (Sum a b)
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "leftFn" BaseW '[a] (Sum a b) hole
ctxt Specification (Sum a b)
s
  propagate Context "leftFn" BaseW '[a] (Sum a b) hole
_ Specification (Sum a b)
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "leftFn" BaseW '[a] (Sum a b) hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context BaseW "leftFn" '[a] (Sum a b)
InjLeftW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var (Sum a b)
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a b. BaseW "leftFn" '[a] (Sum a b)
InjLeftW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var (Sum a b)
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context BaseW "leftFn" '[a] (Sum a b)
InjLeftW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (TypeSpec (SumSpec Maybe (Int, Int)
_ Specification hole
sl Specification b
_) [Sum a b]
cant) =
    Specification hole
sl forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasSpec a => a -> Specification a
notEqualSpec [a
a | SumLeft a
a <- [Sum a b]
cant]
  propagate (Context BaseW "leftFn" '[a] (Sum a b)
InjLeftW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (MemberSpec NonEmpty (Sum a b)
es) =
    case [a
a | SumLeft a
a <- forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Sum a b)
es] of
      (a
x : [a]
xs) -> forall a. NonEmpty a -> Specification a
MemberSpec (a
x forall a. a -> [a] -> NonEmpty a
:| [a]
xs)
      [] ->
        forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            String
"propMemberSpec (sumleft_ HOLE) on (MemberSpec es) with no SumLeft in es: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Sum a b)
es)
  propagate Context "leftFn" BaseW '[a] (Sum a b) hole
ctx Specification (Sum a b)
_ =
    forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for InjLeftW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "leftFn" BaseW '[a] (Sum a b) hole
ctx)

  -- NOTE: this function over-approximates and returns a liberal spec.
  mapTypeSpec :: forall a b.
('[a] ~ '[a], Sum a b ~ b, HasSpec a, HasSpec b) =>
BaseW "leftFn" '[a] b -> TypeSpec a -> Specification b
mapTypeSpec BaseW "leftFn" '[a] b
f TypeSpec a
ts = case BaseW "leftFn" '[a] b
f of
    BaseW "leftFn" '[a] b
InjLeftW -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a b.
Maybe (Int, Int)
-> Specification a -> Specification b -> SumSpec a b
SumSpec forall a. Maybe a
Nothing (forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
ts) (forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"mapTypeSpec InjLeftW"))

leftFn :: (HasSpec a, HasSpec b, KnownNat (CountCases b)) => Term a -> Term (Sum a b)
leftFn :: forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term a -> Term (Sum a b)
leftFn = forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a b. BaseW "leftFn" '[a] (Sum a b)
InjLeftW

-- ============= InjRightW ====

instance
  (HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
  Logic "rightFn" BaseW '[b] (Sum a b)
  where
  propagate :: forall hole.
Context "rightFn" BaseW '[b] (Sum a b) hole
-> Specification (Sum a b) -> Specification hole
propagate Context "rightFn" BaseW '[b] (Sum a b) hole
ctxt (ExplainSpec [] Specification (Sum a b)
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "rightFn" BaseW '[b] (Sum a b) hole
ctxt Specification (Sum a b)
s
  propagate Context "rightFn" BaseW '[b] (Sum a b) hole
ctxt (ExplainSpec [String]
es Specification (Sum a b)
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "rightFn" BaseW '[b] (Sum a b) hole
ctxt Specification (Sum a b)
s
  propagate Context "rightFn" BaseW '[b] (Sum a b) hole
_ Specification (Sum a b)
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "rightFn" BaseW '[b] (Sum a b) hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context BaseW "rightFn" '[b] (Sum a b)
InjRightW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var (Sum a b)
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a b. BaseW "rightFn" '[b] (Sum a b)
InjRightW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var (Sum a b)
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context BaseW "rightFn" '[b] (Sum a b)
InjRightW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (TypeSpec (SumSpec Maybe (Int, Int)
_ Specification a
_ Specification hole
sr) [Sum a b]
cant) =
    Specification hole
sr forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasSpec a => a -> Specification a
notEqualSpec [b
a | SumRight b
a <- [Sum a b]
cant]
  propagate (Context BaseW "rightFn" '[b] (Sum a b)
InjRightW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (MemberSpec NonEmpty (Sum a b)
es) =
    case [b
a | SumRight b
a <- forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Sum a b)
es] of
      (b
x : [b]
xs) -> forall a. NonEmpty a -> Specification a
MemberSpec (b
x forall a. a -> [a] -> NonEmpty a
:| [b]
xs)
      [] ->
        forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            String
"propagate(InjRight HOLE) on (MemberSpec es) with no SumLeft in es: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Sum a b)
es)
  propagate Context "rightFn" BaseW '[b] (Sum a b) hole
ctx Specification (Sum a b)
_ =
    forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for InjRightW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "rightFn" BaseW '[b] (Sum a b) hole
ctx)

  -- NOTE: this function over-approximates and returns a liberal spec.
  mapTypeSpec :: forall a b.
('[b] ~ '[a], Sum a b ~ b, HasSpec a, HasSpec b) =>
BaseW "rightFn" '[a] b -> TypeSpec a -> Specification b
mapTypeSpec BaseW "rightFn" '[a] b
f TypeSpec a
ts = case BaseW "rightFn" '[a] b
f of
    BaseW "rightFn" '[a] b
InjRightW -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a b.
Maybe (Int, Int)
-> Specification a -> Specification b -> SumSpec a b
SumSpec forall a. Maybe a
Nothing (forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"mapTypeSpec InjRightW")) (forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
ts)

rightFn :: (HasSpec a, HasSpec b, KnownNat (CountCases b)) => Term b -> Term (Sum a b)
rightFn :: forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term b -> Term (Sum a b)
rightFn = forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a b. BaseW "rightFn" '[b] (Sum a b)
InjRightW

-- ==================================================================
-- 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)
leftFn -- app injLeftFn

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)
rightFn 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 (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm (forall b (s1 :: Symbol) (s2 :: Symbol)
       (t1 :: Symbol -> [*] -> * -> *) (t2 :: Symbol -> [*] -> * -> *) a
       rng.
(Logic s1 t1 '[b] rng, Logic s2 t2 '[a] b, HasSpec b) =>
t1 s1 '[b] rng -> t2 s2 '[a] b -> FunW "composeFn" '[a] rng
ComposeW forall rng b. BaseW "prodFst_" '[Prod rng b] rng
ProdFstW forall a.
GenericRequires a =>
BaseW "toGenericFn" '[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 (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm (forall b (s1 :: Symbol) (s2 :: Symbol)
       (t1 :: Symbol -> [*] -> * -> *) (t2 :: Symbol -> [*] -> * -> *) a
       rng.
(Logic s1 t1 '[b] rng, Logic s2 t2 '[a] b, HasSpec b) =>
t1 s1 '[b] rng -> t2 s2 '[a] b -> FunW "composeFn" '[a] rng
ComposeW forall a rng. BaseW "prodSnd_" '[Prod a rng] rng
ProdSndW forall a.
GenericRequires a =>
BaseW "toGenericFn" '[a] (SimpleRep a)
ToGenericW)

fstW :: (HasSpec a, HasSpec b) => FunW "composeFn" '[(a, b)] a
fstW :: forall a b. (HasSpec a, HasSpec b) => FunW "composeFn" '[(a, b)] a
fstW = (forall b (s1 :: Symbol) (s2 :: Symbol)
       (t1 :: Symbol -> [*] -> * -> *) (t2 :: Symbol -> [*] -> * -> *) a
       rng.
(Logic s1 t1 '[b] rng, Logic s2 t2 '[a] b, HasSpec b) =>
t1 s1 '[b] rng -> t2 s2 '[a] b -> FunW "composeFn" '[a] rng
ComposeW forall rng b. BaseW "prodFst_" '[Prod rng b] rng
ProdFstW forall a.
GenericRequires a =>
BaseW "toGenericFn" '[a] (SimpleRep a)
ToGenericW)

sndW :: (HasSpec a, HasSpec b) => FunW "composeFn" '[(a, b)] b
sndW :: forall a b. (HasSpec a, HasSpec b) => FunW "composeFn" '[(a, b)] b
sndW = (forall b (s1 :: Symbol) (s2 :: Symbol)
       (t1 :: Symbol -> [*] -> * -> *) (t2 :: Symbol -> [*] -> * -> *) a
       rng.
(Logic s1 t1 '[b] rng, Logic s2 t2 '[a] b, HasSpec b) =>
t1 s1 '[b] rng -> t2 s2 '[a] b -> FunW "composeFn" '[a] rng
ComposeW forall a rng. BaseW "prodSnd_" '[Prod a rng] rng
ProdSndW forall a.
GenericRequires a =>
BaseW "toGenericFn" '[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 (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun forall a b. (HasSpec a, HasSpec b) => FunW "composeFn" '[(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 (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun forall a b. (HasSpec a, HasSpec b) => FunW "composeFn" '[(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 "fromGenericFn" 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 "fromGenericFn" 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)
leftFn

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 "fromGenericFn" 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)
rightFn

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 "fromGenericFn" 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. Literal 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. Literal 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. Literal 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. Literal 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)
      ]