{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
-- Not sure why (Logic "sizeOf_" SizeW '[t] Integer) is an orphan instance
-- 'data SizeW', is defined in the same file as the instance.
{-# OPTIONS_GHC -Wno-orphans #-}

-- 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.Size where

import Constrained.Base
import Constrained.Conformance (satisfies)
import Constrained.GenT
import Constrained.Generic
import Constrained.List
import Constrained.NumSpec
import Constrained.Syntax
import Constrained.TheKnot (genFromSpecT, (<=.), (==.))
import Data.Kind
import qualified Data.List.NonEmpty as NE
import GHC.TypeLits

-- ======================================================================
-- Size and its 'generic' operations over Sized types.
-- ======================================================================

-- | Because Sizes should always be >= 0, We provide this alternate generator
--   that can be used to replace (genFromSpecT @Integer), to ensure this important property
genFromSizeSpec :: MonadGenError m => Specification Integer -> GenT m Integer
genFromSizeSpec :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer -> GenT m Integer
genFromSizeSpec Specification Integer
integerSpec = forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT (Specification Integer
integerSpec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec Integer
0)

data SizeW (s :: Symbol) (dom :: [Type]) rng :: Type where
  SizeOfW :: forall n. Sized n => SizeW "sizeOf_" '[n] Integer

deriving instance Eq (SizeW s ds r)

instance Show (SizeW s d r) where
  show :: SizeW s d r -> String
show SizeW s d r
SizeOfW = String
"sizeOf_"

instance Semantics SizeW where
  semantics :: forall (s :: Symbol) (d :: [*]) r. SizeW s d r -> FunTy d r
semantics SizeW s d r
SizeOfW = forall t. Sized t => t -> Integer
sizeOf -- From the Sized class.

instance Syntax SizeW

instance (Sized t, HasSpec t) => Logic "sizeOf_" SizeW '[t] Integer where
  propagate :: forall hole.
Context "sizeOf_" SizeW '[t] Integer hole
-> Specification Integer -> Specification hole
propagate Context "sizeOf_" SizeW '[t] Integer hole
ctxt (ExplainSpec [] Specification Integer
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 "sizeOf_" SizeW '[t] Integer hole
ctxt Specification Integer
s
  propagate Context "sizeOf_" SizeW '[t] Integer hole
ctxt (ExplainSpec [String]
es Specification Integer
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 "sizeOf_" SizeW '[t] Integer hole
ctxt Specification Integer
s
  propagate Context "sizeOf_" SizeW '[t] Integer hole
_ Specification Integer
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "sizeOf_" SizeW '[t] Integer hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context SizeW "sizeOf_" '[t] Integer
SizeOfW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var Integer
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 n. Sized n => SizeW "sizeOf_" '[n] Integer
SizeOfW (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 Integer
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context SizeW "sizeOf_" '[t] Integer
SizeOfW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (TypeSpec TypeSpec Integer
ts [Integer]
cant) =
    forall t.
(Sized t, HasSpec t) =>
NumSpec Integer -> [Integer] -> Specification t
liftSizeSpec TypeSpec Integer
ts [Integer]
cant
  propagate (Context SizeW "sizeOf_" '[t] Integer
SizeOfW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (MemberSpec NonEmpty Integer
es) =
    forall t. (Sized t, HasSpec t) => [Integer] -> Specification t
liftMemberSpec (forall a. NonEmpty a -> [a]
NE.toList NonEmpty Integer
es)
  propagate Context "sizeOf_" SizeW '[t] Integer hole
ctx Specification Integer
_ =
    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 SizeOfW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "sizeOf_" SizeW '[t] Integer hole
ctx)

  mapTypeSpec :: forall a b.
('[t] ~ '[a], Integer ~ b, HasSpec a, HasSpec b) =>
SizeW "sizeOf_" '[a] b -> TypeSpec a -> Specification b
mapTypeSpec (SizeW "sizeOf_" '[a] b
SizeOfW :: SizeW "sizeOf_" '[a] b) TypeSpec a
ts =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term b
x ->
      forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists forall a b. (a -> b) -> a -> b
$ \Term a
x' -> Term Bool -> Pred
Assert (Term b
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall t. (HasSpec t, Sized t) => Term t -> Term Integer
sizeOf_ Term a
x') forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds @a Term a
x' TypeSpec a
ts

sizeOfFn :: forall a. (HasSpec a, Sized a) => Fun '[a] Integer
sizeOfFn :: forall a. (HasSpec a, Sized a) => Fun '[a] Integer
sizeOfFn = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun forall n. Sized n => SizeW "sizeOf_" '[n] Integer
SizeOfW

sizeOf_ :: (HasSpec t, Sized t) => Term t -> Term Integer
sizeOf_ :: forall t. (HasSpec t, Sized t) => Term t -> Term Integer
sizeOf_ = forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall n. Sized n => SizeW "sizeOf_" '[n] Integer
SizeOfW

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

rangeSize :: Integer -> Integer -> SizeSpec
rangeSize :: Integer -> Integer -> NumSpec Integer
rangeSize Integer
a Integer
b | Integer
a forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Integer
b forall a. Ord a => a -> a -> Bool
< Integer
0 = forall a. HasCallStack => String -> a
error (String
"Negative Int in call to rangeSize: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
a forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
b)
rangeSize Integer
a Integer
b = forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just Integer
a) (forall a. a -> Maybe a
Just Integer
b)

between :: (HasSpec a, TypeSpec a ~ NumSpec a) => a -> a -> Specification a
between :: forall a.
(HasSpec a, TypeSpec a ~ NumSpec a) =>
a -> a -> Specification a
between a
lo a
hi = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just a
lo) (forall a. a -> Maybe a
Just a
hi)) []

-- | The widest interval whose largest element is admitted by the original spec
maxSpec :: Specification Integer -> Specification Integer
maxSpec :: Specification Integer -> Specification Integer
maxSpec (ExplainSpec [String]
es Specification Integer
s) = forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (Specification Integer -> Specification Integer
maxSpec Specification Integer
s)
maxSpec Specification Integer
TrueSpec = forall a. Specification a
TrueSpec
maxSpec s :: Specification Integer
s@(SuspendedSpec Var Integer
_ Pred
_) =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Integer
x -> forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists forall a b. (a -> b) -> a -> b
$ \Term Integer
y -> [Term Integer
y forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification Integer
s, NonEmpty String -> Pred -> Pred
Explain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"maxSpec on SuspendedSpec") forall a b. (a -> b) -> a -> b
$ Term Bool -> Pred
Assert (Term Integer
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
y)]
maxSpec (ErrorSpec NonEmpty String
xs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
xs
maxSpec (MemberSpec NonEmpty Integer
xs) = forall a. OrdLike a => a -> Specification a
leqSpec (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum NonEmpty Integer
xs)
maxSpec (TypeSpec (NumSpecInterval Maybe Integer
_ Maybe Integer
hi) [Integer]
bad) = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval forall a. Maybe a
Nothing Maybe Integer
hi) [Integer]
bad

-- ================
-- Sized
-- ================

type SizeSpec = NumSpec Integer

class Sized t where
  sizeOf :: t -> Integer
  default sizeOf :: (HasSimpleRep t, Sized (SimpleRep t)) => t -> Integer
  sizeOf = forall t. Sized t => t -> Integer
sizeOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep

  liftSizeSpec :: HasSpec t => SizeSpec -> [Integer] -> Specification t
  default liftSizeSpec ::
    ( HasSpec t
    , HasSimpleRep t
    , Sized (SimpleRep t)
    , HasSpec (SimpleRep t)
    , TypeSpec t ~ TypeSpec (SimpleRep t)
    ) =>
    SizeSpec -> [Integer] -> Specification t
  liftSizeSpec NumSpec Integer
sz [Integer]
cant = forall a.
(HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec forall a b. (a -> b) -> a -> b
$ forall t.
(Sized t, HasSpec t) =>
NumSpec Integer -> [Integer] -> Specification t
liftSizeSpec NumSpec Integer
sz [Integer]
cant

  liftMemberSpec :: HasSpec t => [Integer] -> Specification t
  default liftMemberSpec ::
    ( HasSpec t
    , HasSpec (SimpleRep t)
    , HasSimpleRep t
    , Sized (SimpleRep t)
    , TypeSpec t ~ TypeSpec (SimpleRep t)
    ) =>
    [Integer] -> Specification t
  liftMemberSpec = forall a.
(HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. (Sized t, HasSpec t) => [Integer] -> Specification t
liftMemberSpec

  sizeOfTypeSpec :: HasSpec t => TypeSpec t -> Specification Integer
  default sizeOfTypeSpec ::
    ( HasSpec (SimpleRep t)
    , Sized (SimpleRep t)
    , TypeSpec t ~ TypeSpec (SimpleRep t)
    ) =>
    TypeSpec t -> Specification Integer
  sizeOfTypeSpec = forall t.
(Sized t, HasSpec t) =>
TypeSpec t -> Specification Integer
sizeOfTypeSpec @(SimpleRep t)

-- How to constrain the size of any type, with a Sized instance
hasSize :: (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize :: forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize NumSpec Integer
sz = forall t.
(Sized t, HasSpec t) =>
NumSpec Integer -> [Integer] -> Specification t
liftSizeSpec NumSpec Integer
sz []