{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Constrained.Spec.Map where

import Constrained.AbstractSyntax
import Constrained.Base
import Constrained.Conformance
import Constrained.Core
import Constrained.FunctionSymbol
import Constrained.GenT
import Constrained.Generic (Prod (..))
import Constrained.List
import Constrained.NumSpec (cardinality, geqSpec, leqSpec, nubOrd)
import Constrained.PrettyUtils
import Constrained.Spec.Set
import Constrained.Spec.SumProd
import Constrained.Syntax
import Constrained.TheKnot
import Control.Monad
import Data.Foldable
import Data.Kind
import Data.List (nub)
import qualified Data.List.NonEmpty as NE
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics
import Prettyprinter
import Test.QuickCheck hiding (Fun, Witness, forAll)

------------------------------------------------------------------------
-- HasSpec
------------------------------------------------------------------------

instance Ord a => Sized (Map.Map a b) where
  sizeOf :: Map a b -> Integer
sizeOf = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> (Map a b -> Int) -> Map a b -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a b -> Int
forall k a. Map k a -> Int
Map.size
  liftSizeSpec :: HasSpec (Map a b) =>
SizeSpec -> [Integer] -> Specification (Map a b)
liftSizeSpec SizeSpec
sz [Integer]
cant = TypeSpec (Map a b) -> Specification (Map a b)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Map a b) -> Specification (Map a b))
-> TypeSpec (Map a b) -> Specification (Map a b)
forall a b. (a -> b) -> a -> b
$ MapSpec a b
forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecSize = TypeSpec sz cant}
  liftMemberSpec :: HasSpec (Map a b) => [Integer] -> Specification (Map a b)
liftMemberSpec [Integer]
xs = case [Integer] -> Maybe (NonEmpty Integer)
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty ([Integer] -> [Integer]
forall a. Ord a => [a] -> [a]
nubOrd [Integer]
xs) of
    Maybe (NonEmpty Integer)
Nothing -> NonEmpty String -> Specification (Map a b)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"In liftMemberSpec for the (Sized Map) instance, xs is the empty list")
    Just NonEmpty Integer
ys -> TypeSpec (Map a b) -> Specification (Map a b)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Map a b) -> Specification (Map a b))
-> TypeSpec (Map a b) -> Specification (Map a b)
forall a b. (a -> b) -> a -> b
$ MapSpec a b
forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecSize = MemberSpec ys}
  sizeOfTypeSpec :: HasSpec (Map a b) => TypeSpec (Map a b) -> Specification Integer
sizeOfTypeSpec (MapSpec Maybe Integer
_ Set a
mustk [b]
mustv Specification Integer
size Specification (a, b)
_ FoldSpec b
_) =
    Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec (Set a -> Integer
forall t. Sized t => t -> Integer
sizeOf Set a
mustk)
      Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec ([b] -> Integer
forall t. Sized t => t -> Integer
sizeOf [b]
mustv)
      Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
size

data MapSpec k v = MapSpec
  { forall k v. MapSpec k v -> Maybe Integer
mapSpecHint :: Maybe Integer
  , forall k v. MapSpec k v -> Set k
mapSpecMustKeys :: Set k
  , forall k v. MapSpec k v -> [v]
mapSpecMustValues :: [v]
  , forall k v. MapSpec k v -> Specification Integer
mapSpecSize :: Specification Integer
  , forall k v. MapSpec k v -> Specification (k, v)
mapSpecElem :: Specification (k, v)
  , forall k v. MapSpec k v -> FoldSpec v
mapSpecFold :: FoldSpec v
  }
  deriving ((forall x. MapSpec k v -> Rep (MapSpec k v) x)
-> (forall x. Rep (MapSpec k v) x -> MapSpec k v)
-> Generic (MapSpec k v)
forall x. Rep (MapSpec k v) x -> MapSpec k v
forall x. MapSpec k v -> Rep (MapSpec k v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k v x. Rep (MapSpec k v) x -> MapSpec k v
forall k v x. MapSpec k v -> Rep (MapSpec k v) x
$cfrom :: forall k v x. MapSpec k v -> Rep (MapSpec k v) x
from :: forall x. MapSpec k v -> Rep (MapSpec k v) x
$cto :: forall k v x. Rep (MapSpec k v) x -> MapSpec k v
to :: forall x. Rep (MapSpec k v) x -> MapSpec k v
Generic)

-- | emptySpec without all the constraints
defaultMapSpec :: Ord k => MapSpec k v
defaultMapSpec :: forall k v. Ord k => MapSpec k v
defaultMapSpec = Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec Maybe Integer
forall a. Maybe a
Nothing Set k
forall a. Monoid a => a
mempty [v]
forall a. Monoid a => a
mempty Specification Integer
forall deps a. SpecificationD deps a
TrueSpec Specification (k, v)
forall deps a. SpecificationD deps a
TrueSpec FoldSpec v
forall a. FoldSpec a
NoFold

-- TODO: consider making this more interesting to get fewer discarded tests
-- in `prop_gen_sound`
instance
  ( Arbitrary k
  , Arbitrary v
  , Arbitrary (TypeSpec k)
  , Arbitrary (TypeSpec v)
  , Ord k
  , HasSpec k
  , Foldy v
  ) =>
  Arbitrary (MapSpec k v)
  where
  arbitrary :: Gen (MapSpec k v)
arbitrary =
    Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
      (Maybe Integer
 -> Set k
 -> [v]
 -> Specification Integer
 -> Specification (k, v)
 -> FoldSpec v
 -> MapSpec k v)
-> Gen (Maybe Integer)
-> Gen
     (Set k
      -> [v]
      -> Specification Integer
      -> Specification (k, v)
      -> FoldSpec v
      -> MapSpec k v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Maybe Integer)
forall a. Arbitrary a => Gen a
arbitrary
      Gen
  (Set k
   -> [v]
   -> Specification Integer
   -> Specification (k, v)
   -> FoldSpec v
   -> MapSpec k v)
-> Gen (Set k)
-> Gen
     ([v]
      -> Specification Integer
      -> Specification (k, v)
      -> FoldSpec v
      -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Set k)
forall a. Arbitrary a => Gen a
arbitrary
      Gen
  ([v]
   -> Specification Integer
   -> Specification (k, v)
   -> FoldSpec v
   -> MapSpec k v)
-> Gen [v]
-> Gen
     (Specification Integer
      -> Specification (k, v) -> FoldSpec v -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen [v]
forall a. Arbitrary a => Gen a
arbitrary
      Gen
  (Specification Integer
   -> Specification (k, v) -> FoldSpec v -> MapSpec k v)
-> Gen (Specification Integer)
-> Gen (Specification (k, v) -> FoldSpec v -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification Integer)
forall a. Arbitrary a => Gen a
arbitrary
      Gen (Specification (k, v) -> FoldSpec v -> MapSpec k v)
-> Gen (Specification (k, v)) -> Gen (FoldSpec v -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification (k, v))
forall a. Arbitrary a => Gen a
arbitrary
      Gen (FoldSpec v -> MapSpec k v)
-> Gen (FoldSpec v) -> Gen (MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [(Int, Gen (FoldSpec v))] -> Gen (FoldSpec v)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1, FoldSpec v -> Gen (FoldSpec v)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec v
forall a. FoldSpec a
NoFold), (Int
1, Gen (FoldSpec v)
forall a. Arbitrary a => Gen a
arbitrary)]
  shrink :: MapSpec k v -> [MapSpec k v]
shrink = MapSpec k v -> [MapSpec k v]
forall a.
(Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) =>
a -> [a]
genericShrink

instance Arbitrary (FoldSpec (Map k v)) where
  arbitrary :: Gen (FoldSpec (Map k v))
arbitrary = FoldSpec (Map k v) -> Gen (FoldSpec (Map k v))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec (Map k v)
forall a. FoldSpec a
NoFold

instance
  ( HasSpec (k, v)
  , HasSpec k
  , HasSpec v
  , HasSpec [v]
  ) =>
  Pretty (WithPrec (MapSpec k v))
  where
  pretty :: forall ann. WithPrec (MapSpec k v) -> Doc ann
pretty (WithPrec Int
d MapSpec k v
s) =
    Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
      Doc ann
"MapSpec"
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
          [ Doc ann
"hint       =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Maybe Integer -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (MapSpec k v -> Maybe Integer
forall k v. MapSpec k v -> Maybe Integer
mapSpecHint MapSpec k v
s)
          , Doc ann
"mustKeys   =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Set k -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (MapSpec k v -> Set k
forall k v. MapSpec k v -> Set k
mapSpecMustKeys MapSpec k v
s)
          , Doc ann
"mustValues =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [v] -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (MapSpec k v -> [v]
forall k v. MapSpec k v -> [v]
mapSpecMustValues MapSpec k v
s)
          , Doc ann
"size       =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification Integer -> Doc ann
pretty (MapSpec k v -> Specification Integer
forall k v. MapSpec k v -> Specification Integer
mapSpecSize MapSpec k v
s)
          , Doc ann
"elem       =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification (k, v) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification (k, v) -> Doc ann
pretty (MapSpec k v -> Specification (k, v)
forall k v. MapSpec k v -> Specification (k, v)
mapSpecElem MapSpec k v
s)
          , Doc ann
"fold       =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FoldSpec v -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FoldSpec v -> Doc ann
pretty (MapSpec k v -> FoldSpec v
forall k v. MapSpec k v -> FoldSpec v
mapSpecFold MapSpec k v
s)
          ]

instance
  ( HasSpec (k, v)
  , HasSpec k
  , HasSpec v
  , HasSpec [v]
  ) =>
  Show (MapSpec k v)
  where
  showsPrec :: Int -> MapSpec k v -> ShowS
showsPrec Int
d = Doc Any -> ShowS
forall a. Show a => a -> ShowS
shows (Doc Any -> ShowS)
-> (MapSpec k v -> Doc Any) -> MapSpec k v -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> MapSpec k v -> Doc Any
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
d

instance Ord k => Forallable (Map k v) (k, v) where
  fromForAllSpec :: (HasSpec (Map k v), HasSpec (k, v)) =>
Specification (k, v) -> Specification (Map k v)
fromForAllSpec Specification (k, v)
kvs = TypeSpec (Map k v) -> Specification (Map k v)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Map k v) -> Specification (Map k v))
-> TypeSpec (Map k v) -> Specification (Map k v)
forall a b. (a -> b) -> a -> b
$ MapSpec k v
forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecElem = kvs}
  forAllToList :: Map k v -> [(k, v)]
forAllToList = Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList

-- ============================================================
-- We will need to take projections on (Specification (a,b))

fstSpec :: forall k v. (HasSpec k, HasSpec v) => Specification (k, v) -> Specification k
fstSpec :: forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification k
fstSpec Specification (k, v)
s = ProdW '[Prod k v] k -> Specification (Prod k v) -> Specification k
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec ProdW '[Prod k v] k
forall b b1. (HasSpec b, HasSpec b1) => ProdW '[Prod b b1] b
ProdFstW (BaseW '[(k, v)] (Prod k v)
-> Specification (k, v) -> Specification (Prod k v)
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec BaseW '[(k, v)] (SimpleRep (k, v))
BaseW '[(k, v)] (Prod k v)
forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW Specification (k, v)
s)

sndSpec :: forall k v. (HasSpec k, HasSpec v) => Specification (k, v) -> Specification v
sndSpec :: forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification v
sndSpec Specification (k, v)
s = ProdW '[Prod k v] v -> Specification (Prod k v) -> Specification v
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec ProdW '[Prod k v] v
forall a1 b. (HasSpec a1, HasSpec b) => ProdW '[Prod a1 b] b
ProdSndW (BaseW '[(k, v)] (Prod k v)
-> Specification (k, v) -> Specification (Prod k v)
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec BaseW '[(k, v)] (SimpleRep (k, v))
BaseW '[(k, v)] (Prod k v)
forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW Specification (k, v)
s)

-- ======================================================================
-- The HasSpec instance for Maps

instance
  (Ord k, HasSpec (Prod k v), HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) =>
  HasSpec (Map k v)
  where
  type TypeSpec (Map k v) = MapSpec k v
  type Prerequisites (Map k v) = (HasSpec k, HasSpec v)

  emptySpec :: TypeSpec (Map k v)
emptySpec = TypeSpec (Map k v)
MapSpec k v
forall k v. Ord k => MapSpec k v
defaultMapSpec

  combineSpec :: TypeSpec (Map k v) -> TypeSpec (Map k v) -> Specification (Map k v)
combineSpec
    (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification Integer
size Specification (k, v)
kvs FoldSpec v
foldSpec)
    (MapSpec Maybe Integer
mHint' Set k
mustKeys' [v]
mustVals' Specification Integer
size' Specification (k, v)
kvs' FoldSpec v
foldSpec') = case FoldSpec v -> FoldSpec v -> Either [String] (FoldSpec v)
forall a. FoldSpec a -> FoldSpec a -> Either [String] (FoldSpec a)
combineFoldSpec FoldSpec v
foldSpec FoldSpec v
foldSpec' of
      Left [String]
msgs ->
        NonEmpty String -> Specification (Map k v)
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String -> Specification (Map k v))
-> NonEmpty String -> Specification (Map k v)
forall a b. (a -> b) -> a -> b
$
          [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList ([String] -> NonEmpty String) -> [String] -> NonEmpty String
forall a b. (a -> b) -> a -> b
$
            [ String
"Error in combining FoldSpec in combineSpec for Map"
            , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FoldSpec v -> String
forall a. Show a => a -> String
show FoldSpec v
foldSpec
            , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FoldSpec v -> String
forall a. Show a => a -> String
show FoldSpec v
foldSpec'
            ]
              [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
msgs
      Right FoldSpec v
foldSpec'' ->
        TypeSpec (Map k v) -> Specification (Map k v)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Map k v) -> Specification (Map k v))
-> TypeSpec (Map k v) -> Specification (Map k v)
forall a b. (a -> b) -> a -> b
$
          Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
            -- This is min because that allows more compositionality - if a spec specifies a
            -- low upper bound because some part of the spec will be slow it doesn't make sense
            -- to increase it somewhere else because that part isn't slow.
            ((Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Maybe Integer
mHint Maybe Integer
mHint')
            (Set k
mustKeys Set k -> Set k -> Set k
forall a. Semigroup a => a -> a -> a
<> Set k
mustKeys')
            ([v] -> [v]
forall a. Eq a => [a] -> [a]
nub ([v] -> [v]) -> [v] -> [v]
forall a b. (a -> b) -> a -> b
$ [v]
mustVals [v] -> [v] -> [v]
forall a. Semigroup a => a -> a -> a
<> [v]
mustVals')
            (Specification Integer
size Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
size')
            (Specification (k, v)
kvs Specification (k, v)
-> Specification (k, v) -> Specification (k, v)
forall a. Semigroup a => a -> a -> a
<> Specification (k, v)
kvs')
            FoldSpec v
foldSpec''

  conformsTo :: HasCallStack => Map k v -> TypeSpec (Map k v) -> Bool
conformsTo Map k v
m (MapSpec Maybe Integer
_ Set k
mustKeys [v]
mustVals Specification Integer
size Specification (k, v)
kvs FoldSpec v
foldSpec) =
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ Set k
mustKeys Set k -> Set k -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Map k v -> Set k
forall k a. Map k a -> Set k
Map.keysSet Map k v
m
      , (v -> Bool) -> [v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (v -> [v] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map k v -> [v]
forall k a. Map k a -> [a]
Map.elems Map k v
m) [v]
mustVals
      , Map k v -> Integer
forall t. Sized t => t -> Integer
sizeOf Map k v
m Integer -> Specification Integer -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size
      , ((k, v) -> Bool) -> [(k, v)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((k, v) -> Specification (k, v) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification (k, v)
kvs) (Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m)
      , Map k v -> [v]
forall k a. Map k a -> [a]
Map.elems Map k v
m [v] -> FoldSpec v -> Bool
forall a. [a] -> FoldSpec a -> Bool
`conformsToFoldSpec` FoldSpec v
foldSpec
      ]

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Map k v) -> GenT m (Map k v)
genFromTypeSpec (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification Integer
size (Specification (k, v) -> Specification (k, v)
forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification (k, v)
kvs) FoldSpec v
NoFold)
    | Set k -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set k
mustKeys
    , [v] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [v]
mustVals = do
        let size' :: Specification Integer
size' =
              [Specification Integer] -> Specification Integer
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
                [ Specification Integer
-> (Integer -> Specification Integer)
-> Maybe Integer
-> Specification Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Specification Integer
forall deps a. SpecificationD deps a
TrueSpec (Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
leqSpec (Integer -> Specification Integer)
-> (Integer -> Integer) -> Integer -> Specification Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0) Maybe Integer
mHint
                , Specification Integer
size
                , Specification Integer -> Specification Integer
maxSpec (Specification k -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality (Specification (k, v) -> Specification k
forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification k
fstSpec Specification (k, v)
kvs)) -- (mapSpec FstW  (mapSpec ToGenericW kvs)))
                , Specification Integer -> Specification Integer
maxSpec (forall a. HasSpec a => Specification Integer
cardinalTrueSpec @k)
                , Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec Integer
0
                ]
        Integer
n <- Specification Integer -> GenT m Integer
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification Integer
size'
        let go :: Integer -> Specification (k, v) -> Map k v -> GenT m (Map k v)
go Integer
0 Specification (k, v)
_ Map k v
m = Map k v -> GenT m (Map k v)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map k v
m
            go Integer
n' Specification (k, v)
kvs' Map k v
m = do
              Maybe (k, v)
mkv <- GenT GE (k, v) -> GenT m (Maybe (k, v))
forall (m :: * -> *) a.
MonadGenError m =>
GenT GE a -> GenT m (Maybe a)
tryGenT (GenT GE (k, v) -> GenT m (Maybe (k, v)))
-> GenT GE (k, v) -> GenT m (Maybe (k, v))
forall a b. (a -> b) -> a -> b
$ Specification (k, v) -> GenT GE (k, v)
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification (k, v)
kvs'
              case Maybe (k, v)
mkv of
                Maybe (k, v)
Nothing
                  | Map k v -> Integer
forall t. Sized t => t -> Integer
sizeOf Map k v
m Integer -> Specification Integer -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size -> Map k v -> GenT m (Map k v)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map k v
m
                Just (k
k, v
v) ->
                  Integer -> Specification (k, v) -> Map k v -> GenT m (Map k v)
go
                    (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
                    (Specification (k, v)
kvs' Specification (k, v)
-> Specification (k, v) -> Specification (k, v)
forall a. Semigroup a => a -> a -> a
<> TypeSpec (k, v) -> Specification (k, v)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Specification k -> Specification v -> PairSpec k v
forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian (k -> Specification k
forall a. HasSpec a => a -> Specification a
notEqualSpec k
k) Specification v
forall a. Monoid a => a
mempty))
                    (k -> v -> Map k v -> Map k v
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k v
v Map k v
m)
                Maybe (k, v)
_ ->
                  NonEmpty String -> GenT m (Map k v)
forall a. HasCallStack => NonEmpty String -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genErrorNE
                    ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
                        [ String
"Failed to generate enough elements for the map:"
                        , String
"  m = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map k v -> String
forall a. Show a => a -> String
show Map k v
m
                        , String
"  n' = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n'
                        , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"  kvs' = " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Specification (k, v) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification (k, v) -> Doc ann
pretty Specification (k, v)
kvs'
                        , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"  simplifySpec kvs' = " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Specification (k, v) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification (k, v) -> Doc ann
pretty (Specification (k, v) -> Specification (k, v)
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification (k, v)
kvs')
                        ]
                    )
        String -> GenT m (Map k v) -> GenT m (Map k v)
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain (String
"  n = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n) (GenT m (Map k v) -> GenT m (Map k v))
-> GenT m (Map k v) -> GenT m (Map k v)
forall a b. (a -> b) -> a -> b
$ Integer -> Specification (k, v) -> Map k v -> GenT m (Map k v)
go Integer
n Specification (k, v)
kvs Map k v
forall a. Monoid a => a
mempty
  genFromTypeSpec (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification Integer
size (Specification (k, v) -> Specification (k, v)
forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification (k, v)
kvs) FoldSpec v
foldSpec) = do
    ![(k, v)]
mustMap <- String -> GenT m [(k, v)] -> GenT m [(k, v)]
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"Make the mustMap" (GenT m [(k, v)] -> GenT m [(k, v)])
-> GenT m [(k, v)] -> GenT m [(k, v)]
forall a b. (a -> b) -> a -> b
$ [k] -> (k -> GenT m (k, v)) -> GenT m [(k, v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Set k -> [k]
forall a. Set a -> [a]
Set.toList Set k
mustKeys) ((k -> GenT m (k, v)) -> GenT m [(k, v)])
-> (k -> GenT m (k, v)) -> GenT m [(k, v)]
forall a b. (a -> b) -> a -> b
$ \k
k -> do
      let vSpec :: Specification v
vSpec = (Term v -> Pred) -> Specification v
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term v -> Pred) -> Specification v)
-> (Term v -> Pred) -> Specification v
forall a b. (a -> b) -> a -> b
$ \Term v
v -> Term (k, v) -> Specification (k, v) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term k -> Term v -> Term (k, v)
forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ (k -> Term k
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit k
k) Term v
v) Specification (k, v)
kvs
      v
v <- String -> GenT m v -> GenT m v
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain (Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"vSpec =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification v -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification v -> Doc ann
pretty Specification v
vSpec) (GenT m v -> GenT m v) -> GenT m v -> GenT m v
forall a b. (a -> b) -> a -> b
$ Specification v -> GenT m v
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification v
vSpec
      (k, v) -> GenT m (k, v)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (k
k, v
v)
    let haveVals :: [v]
haveVals = ((k, v) -> v) -> [(k, v)] -> [v]
forall a b. (a -> b) -> [a] -> [b]
map (k, v) -> v
forall a b. (a, b) -> b
snd [(k, v)]
mustMap
        mustVals' :: [v]
mustVals' = (v -> Bool) -> [v] -> [v]
forall a. (a -> Bool) -> [a] -> [a]
filter (v -> [v] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [v]
haveVals) [v]
mustVals
        size' :: Specification Integer
size' = Specification Integer -> Specification Integer
forall a. HasSpec a => Specification a -> Specification a
simplifySpec (Specification Integer -> Specification Integer)
-> Specification Integer -> Specification Integer
forall a b. (a -> b) -> a -> b
$ (Term Integer -> Pred) -> Specification Integer
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Integer -> Pred) -> Specification Integer)
-> (Term Integer -> Pred) -> Specification Integer
forall a b. (a -> b) -> a -> b
$ \Term Integer
sz ->
          -- TODO, we should make sure size' is greater than or equal to 0
          Term Integer -> Specification Integer -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
            (Term Integer
sz Term Integer -> Term Integer -> Term Integer
forall a. Num a => a -> a -> a
+ Integer -> Term Integer
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit ([(k, v)] -> Integer
forall t. Sized t => t -> Integer
sizeOf [(k, v)]
mustMap))
            ( Specification Integer
-> (Integer -> Specification Integer)
-> Maybe Integer
-> Specification Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Specification Integer
forall deps a. SpecificationD deps a
TrueSpec (Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
leqSpec (Integer -> Specification Integer)
-> (Integer -> Integer) -> Integer -> Specification Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0) Maybe Integer
mHint
                Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
size
                Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer -> Specification Integer
maxSpec (Specification k -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality (Specification (k, v) -> Specification k
forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification k
fstSpec Specification (k, v)
kvs)) -- (mapSpec FstW $ mapSpec ToGenericW kvs))
                Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer -> Specification Integer
maxSpec (forall a. HasSpec a => Specification Integer
cardinalTrueSpec @k)
            )
        !foldSpec' :: FoldSpec v
foldSpec' = case FoldSpec v
foldSpec of
          FoldSpec v
NoFold -> FoldSpec v
forall a. FoldSpec a
NoFold
          FoldSpec fn :: Fun '[v] b
fn@(Fun t '[v] b
symbol) Specification b
sumSpec -> Fun '[v] b -> Specification b -> FoldSpec v
forall b a.
(HasSpec a, HasSpec b, Foldy b) =>
Fun '[a] b -> Specification b -> FoldSpec a
FoldSpec Fun '[v] b
fn (Specification b -> FoldSpec v) -> Specification b -> FoldSpec v
forall a b. (a -> b) -> a -> b
$ IntW '[b, b] b
-> ListCtx Value '[b, b] (HOLE b)
-> Specification b
-> Specification b
forall (as :: [*]) b a.
(AppRequires IntW as b, HasSpec a) =>
IntW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate IntW '[b, b] b
forall a. Foldy a => IntW '[a, a] a
theAddFn (HOLE b b
forall {k} (a :: k). HOLE a a
HOLE HOLE b b -> List Value '[b] -> ListCtx Value '[b, b] (HOLE b)
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? b -> Value b
forall a. Show a => a -> Value a
Value b
mustSum Value b -> List Value '[] -> List Value '[b]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Value '[]
forall {k} (f :: k -> *). List f '[]
Nil) Specification b
sumSpec
            where
              mustSum :: b
mustSum = [b] -> b
forall a. Foldy a => [a] -> a
adds ((v -> b) -> [v] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (t '[v] b -> FunTy '[v] b
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[v] b
symbol) [v]
haveVals)
    let !valsSpec :: ListSpec v
valsSpec =
          Maybe Integer
-> [v]
-> Specification Integer
-> Specification v
-> FoldSpec v
-> ListSpec v
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec
            Maybe Integer
forall a. Maybe a
Nothing
            [v]
mustVals'
            Specification Integer
size'
            (Specification v -> Specification v
forall a. HasSpec a => Specification a -> Specification a
simplifySpec (Specification v -> Specification v)
-> Specification v -> Specification v
forall a b. (a -> b) -> a -> b
$ (Term v -> Pred) -> Specification v
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term v -> Pred) -> Specification v)
-> (Term v -> Pred) -> Specification v
forall a b. (a -> b) -> a -> b
$ \Term v
v -> (Term k -> Pred) -> Pred
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists ((Term k -> Pred) -> Pred) -> (Term k -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term k
k -> Term k -> Term v -> Term (k, v)
forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term k
k Term v
v Term (k, v) -> Specification (k, v) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (k, v)
kvs)
            FoldSpec v
foldSpec'

    ![v]
restVals <-
      NonEmpty String -> GenT m [v] -> GenT m [v]
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
        ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
            [ String
"Make the restVals"
            , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"  valsSpec =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ListSpec v -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. ListSpec v -> Doc ann
pretty ListSpec v
valsSpec
            , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"  mustMap =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [(k, v)] -> Doc Any
forall a ann. Show a => a -> Doc ann
viaShow [(k, v)]
mustMap
            , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"  size' =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification Integer -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification Integer -> Doc ann
pretty Specification Integer
size'
            ]
        )
        (GenT m [v] -> GenT m [v]) -> GenT m [v] -> GenT m [v]
forall a b. (a -> b) -> a -> b
$ TypeSpec [v] -> GenT m [v]
forall a (m :: * -> *).
(HasSpec a, HasCallStack, MonadGenError m) =>
TypeSpec a -> GenT m a
forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec [v] -> GenT m [v]
genFromTypeSpec
        (TypeSpec [v] -> GenT m [v]) -> TypeSpec [v] -> GenT m [v]
forall a b. (a -> b) -> a -> b
$ TypeSpec [v]
ListSpec v
valsSpec
    let go :: Map k v -> [v] -> GenT m (Map k v)
go Map k v
m [] = Map k v -> GenT m (Map k v)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map k v
m
        go Map k v
m (v
v : [v]
restVals') = do
          let keySpec :: Specification k
keySpec = Set k -> Specification k
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec (Map k v -> Set k
forall k a. Map k a -> Set k
Map.keysSet Map k v
m) Specification k -> Specification k -> Specification k
forall a. Semigroup a => a -> a -> a
<> (Term k -> Pred) -> Specification k
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (\Term k
k -> Term k -> Term v -> Term (k, v)
forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term k
k (v -> Term v
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit v
v) Term (k, v) -> Specification (k, v) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (k, v)
kvs)
          k
k <-
            NonEmpty String -> GenT m k -> GenT m k
forall a. HasCallStack => NonEmpty String -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE
              ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
                  [ String
"Make a key"
                  , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Doc Any
"keySpec =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification k -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification k -> Doc ann
pretty Specification k
keySpec
                  ]
              )
              (GenT m k -> GenT m k) -> GenT m k -> GenT m k
forall a b. (a -> b) -> a -> b
$ Specification k -> GenT m k
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification k
keySpec
          Map k v -> [v] -> GenT m (Map k v)
go (k -> v -> Map k v -> Map k v
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k v
v Map k v
m) [v]
restVals'

    Map k v -> [v] -> GenT m (Map k v)
go ([(k, v)] -> Map k v
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(k, v)]
mustMap) [v]
restVals

  cardinalTypeSpec :: TypeSpec (Map k v) -> Specification Integer
cardinalTypeSpec TypeSpec (Map k v)
_ = Specification Integer
forall deps a. SpecificationD deps a
TrueSpec

  shrinkWithTypeSpec :: TypeSpec (Map k v) -> Map k v -> [Map k v]
shrinkWithTypeSpec (MapSpec Maybe Integer
_ Set k
_ [v]
_ Specification Integer
_ Specification (k, v)
kvs FoldSpec v
_) Map k v
m = ([(k, v)] -> Map k v) -> [[(k, v)]] -> [Map k v]
forall a b. (a -> b) -> [a] -> [b]
map [(k, v)] -> Map k v
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([[(k, v)]] -> [Map k v]) -> [[(k, v)]] -> [Map k v]
forall a b. (a -> b) -> a -> b
$ ((k, v) -> [(k, v)]) -> [(k, v)] -> [[(k, v)]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (Specification (k, v) -> (k, v) -> [(k, v)]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification (k, v)
kvs) (Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m)

  toPreds :: Term (Map k v) -> TypeSpec (Map k v) -> Pred
toPreds Term (Map k v)
m (MapSpec Maybe Integer
mHint Set k
mustKeys [v]
mustVals Specification Integer
size Specification (k, v)
kvs FoldSpec v
foldSpec) =
    [Pred] -> Pred
forall p. IsPred p => p -> Pred
toPred
      [ Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Set k -> TermD Deps (Set k)
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit Set k
mustKeys TermD Deps (Set k) -> TermD Deps (Set k) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Map k v) -> TermD Deps (Set k)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map k v)
m
      , Term [v] -> (Term v -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll ([v] -> Term [v]
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit [v]
mustVals) ((Term v -> Term Bool) -> Pred) -> (Term v -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term v
val ->
          Term v
val Term v -> Term [v] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term (Map k v) -> Term [v]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map k v)
m
      , Term [v] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map k v) -> Term [v]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map k v)
m) Term Integer -> Specification Integer -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification Integer
size
      , Term (Map k v) -> (Term (k, v) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map k v)
m ((Term (k, v) -> Pred) -> Pred) -> (Term (k, v) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (k, v)
kv -> Term (k, v) -> Specification (k, v) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (k, v)
kv Specification (k, v)
kvs
      , Term [v] -> FoldSpec v -> Pred
forall a. HasSpec a => Term [a] -> FoldSpec a -> Pred
toPredsFoldSpec (Term (Map k v) -> Term [v]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map k v)
m) FoldSpec v
foldSpec
      , Pred -> (Integer -> Pred) -> Maybe Integer -> Pred
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pred
forall deps. PredD deps
TruePred (Hint (Map k v) -> Term (Map k v) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
`genHint` Term (Map k v)
m) Maybe Integer
mHint
      ]

instance
  (Ord k, HasSpec k, HasSpec v, HasSpec [v], IsNormalType k, IsNormalType v) =>
  HasGenHint (Map k v)
  where
  type Hint (Map k v) = Integer
  giveHint :: Hint (Map k v) -> Specification (Map k v)
giveHint Hint (Map k v)
h = TypeSpec (Map k v) -> Specification (Map k v)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Map k v) -> Specification (Map k v))
-> TypeSpec (Map k v) -> Specification (Map k v)
forall a b. (a -> b) -> a -> b
$ MapSpec k v
forall k v. Ord k => MapSpec k v
defaultMapSpec {mapSpecHint = Just h}

------------------------------------------------------------------------
-- Logic instances for
------------------------------------------------------------------------

data MapW (dom :: [Type]) (rng :: Type) where
  DomW :: (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[Map k v] (Set k)
  RngW :: (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[Map k v] [v]
  LookupW ::
    (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) => MapW '[k, Map k v] (Maybe v)

deriving instance Eq (MapW dom rng)

mapSem :: MapW d r -> FunTy d r
mapSem :: forall (d :: [*]) r. MapW d r -> FunTy d r
mapSem MapW d r
DomW = FunTy d r
Map k v -> Set k
forall k a. Map k a -> Set k
Map.keysSet
mapSem MapW d r
RngW = FunTy d r
Map k v -> [v]
forall k a. Map k a -> [a]
Map.elems
mapSem MapW d r
LookupW = FunTy d r
k -> Map k v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup

instance Semantics MapW where
  semantics :: forall (d :: [*]) r. MapW d r -> FunTy d r
semantics = MapW d r -> FunTy d r
forall (d :: [*]) r. MapW d r -> FunTy d r
mapSem

instance Syntax MapW

instance Show (MapW d r) where
  show :: MapW d r -> String
show MapW d r
DomW = String
"dom_"
  show MapW d r
RngW = String
"rng_"
  show MapW d r
LookupW = String
"lookup_"

-- ============ DomW

instance Logic MapW where
  propagate :: forall (as :: [*]) b a.
(AppRequires MapW as b, HasSpec a) =>
MapW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate MapW as b
f ListCtx Value as (HOLE a)
ctxt (ExplainSpec [String]
es SpecificationD Deps b
s) = [String] -> Specification a -> Specification a
forall a. [String] -> Specification a -> Specification a
explainSpec [String]
es (Specification a -> Specification a)
-> Specification a -> Specification a
forall a b. (a -> b) -> a -> b
$ MapW as b
-> ListCtx Value as (HOLE a)
-> SpecificationD Deps b
-> Specification a
forall (as :: [*]) b a.
(AppRequires MapW as b, HasSpec a) =>
MapW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate MapW as b
f ListCtx Value as (HOLE a)
ctxt SpecificationD Deps b
s
  propagate MapW as b
_ ListCtx Value as (HOLE a)
_ SpecificationD Deps b
TrueSpec = Specification a
forall deps a. SpecificationD deps a
TrueSpec
  propagate MapW as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
msgs) = NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec NonEmpty String
msgs
  propagate MapW as b
f ListCtx Value as (HOLE a)
ctx (SuspendedSpec Var b
v Pred
ps) = (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> TermD Deps b -> BinderD Deps b -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (MapW as b -> List Term as -> TermD Deps b
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App MapW as b
f (ListCtx Value as (HOLE a) -> Term a -> List Term as
forall (as :: [*]) a.
All HasSpec as =>
ListCtx Value as (HOLE a) -> Term a -> List Term as
fromListCtx ListCtx Value as (HOLE a)
ctx Term a
v')) (Var b
v Var b -> Pred -> BinderD Deps b
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred
ps)
  propagate MapW as b
DomW (Unary HOLE a (Map k v)
HOLE) SpecificationD Deps b
spec =
    case SpecificationD Deps b
spec of
      MemberSpec (b
s :| []) ->
        TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$
          Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec Maybe Integer
forall a. Maybe a
Nothing b
Set k
s [] (Integer -> Specification Integer
forall a. a -> Specification a
equalSpec (Integer -> Specification Integer)
-> Integer -> Specification Integer
forall a b. (a -> b) -> a -> b
$ b -> Integer
forall t. Sized t => t -> Integer
sizeOf b
s) Specification (k, v)
forall deps a. SpecificationD deps a
TrueSpec FoldSpec v
forall a. FoldSpec a
NoFold
      TypeSpec (SetSpec Set k
must Specification k
elemspec Specification Integer
size) [] ->
        TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$
          Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
            Maybe Integer
forall a. Maybe a
Nothing
            Set k
must
            []
            Specification Integer
size
            ((Term (k, v) -> Pred) -> Specification (k, v)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (k, v) -> Pred) -> Specification (k, v))
-> (Term (k, v) -> Pred) -> Specification (k, v)
forall a b. (a -> b) -> a -> b
$ \Term (k, v)
kv -> Term k -> Specification k -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (k, v) -> Term k
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (k, v)
kv) Specification k
elemspec)
            FoldSpec v
forall a. FoldSpec a
NoFold
      SpecificationD Deps b
_ -> NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"Dom on bad map spec", SpecificationD Deps b -> String
forall a. Show a => a -> String
show SpecificationD Deps b
spec])
  propagate MapW as b
RngW (Unary HOLE a (Map k v)
HOLE) SpecificationD Deps b
spec =
    case SpecificationD Deps b
spec of
      TypeSpec (ListSpec Maybe Integer
listHint [v]
must Specification Integer
size Specification v
elemspec FoldSpec v
foldspec) [] ->
        TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$
          Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
            Maybe Integer
listHint
            Set k
forall a. Set a
Set.empty
            [v]
must
            Specification Integer
size
            ((Term (k, v) -> Pred) -> Specification (k, v)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (k, v) -> Pred) -> Specification (k, v))
-> (Term (k, v) -> Pred) -> Specification (k, v)
forall a b. (a -> b) -> a -> b
$ \Term (k, v)
kv -> Term v -> Specification v -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (k, v) -> Term v
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (k, v)
kv) Specification v
elemspec)
            FoldSpec v
foldspec
      -- NOTE: you'd think `MemberSpec [r]` was a safe and easy case. However, that
      -- requires not only that the elements of the map are fixed to what is in `r`,
      -- but they appear in the order that they are in `r`. That's
      -- very difficult to achieve!
      SpecificationD Deps b
_ -> NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"Rng on bad map spec", SpecificationD Deps b -> String
forall a. Show a => a -> String
show SpecificationD Deps b
spec])
  propagate MapW as b
LookupW (Value a
k :! Unary HOLE a (Map k v)
HOLE) SpecificationD Deps b
spec =
    (Term a -> [Pred]) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> [Pred]) -> Specification a)
-> (Term a -> [Pred]) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
m ->
      [Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ a -> TermD Deps a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
k TermD Deps a -> Term (Set a) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Term (Map a v) -> Term (Set a)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term a
Term (Map a v)
m | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe v
forall a. Maybe a
Nothing Maybe v -> Specification (Maybe v) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` SpecificationD Deps b
Specification (Maybe v)
spec]
        [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [ Term a -> (Term (a, v) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term a
m ((Term (a, v) -> Pred) -> Pred) -> (Term (a, v) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (a, v)
kv ->
               TermD Deps a -> (TermD Deps a -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (Term (a, v) -> TermD Deps a
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (a, v)
kv) ((TermD Deps a -> Pred) -> Pred) -> (TermD Deps a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps a
k' ->
                 Term v -> (Term v -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (Term (a, v) -> Term v
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (a, v)
kv) ((Term v -> Pred) -> Pred) -> (Term v -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term v
v ->
                   Term Bool -> Pred -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue (a -> TermD Deps a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
k TermD Deps a -> TermD Deps a -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. TermD Deps a
k') (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
                     -- TODO: What you want to write is `cJust_ v `satisfies` spec` but we can't
                     -- do that because we don't have access to `IsNormalType v` here. When
                     -- we refactor the `IsNormalType` machinery we will be able to make
                     -- this nicer.
                     case SpecificationD Deps b
spec of
                       MemberSpec NonEmpty b
as -> Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term v
v Term v -> Term [v] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [v] -> Term [v]
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit [v
a | Just v
a <- NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
as]
                       TypeSpec (SumSpec Maybe (Int, Int)
_ Specification ()
_ Specification v
vspec) [b]
cant ->
                         Term v
v Term v -> Specification v -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` (Specification v
vspec Specification v -> Specification v -> Specification v
forall a. Semigroup a => a -> a -> a
<> [v] -> Specification v
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [v
a | Just v
a <- [b]
cant])
           ]
  propagate MapW as b
LookupW (HOLE a a
HOLE :? Value a
m :> List Value as1
Nil) SpecificationD Deps b
spec =
    if Maybe v
forall a. Maybe a
Nothing Maybe v -> Specification (Maybe v) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` SpecificationD Deps b
Specification (Maybe v)
spec
      then [a] -> Specification a
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [a
k | (a
k, v
v) <- Map a v -> [(a, v)]
forall k a. Map k a -> [(k, a)]
Map.toList a
Map a v
m, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ v -> Maybe v
forall a. a -> Maybe a
Just v
v Maybe v -> Specification (Maybe v) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` SpecificationD Deps b
Specification (Maybe v)
spec]
      else
        [a] -> NonEmpty String -> Specification a
forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
          (Map a v -> [a]
forall k a. Map k a -> [k]
Map.keys (Map a v -> [a]) -> Map a v -> [a]
forall a b. (a -> b) -> a -> b
$ (v -> Bool) -> Map a v -> Map a v
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter ((b -> SpecificationD Deps b -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` SpecificationD Deps b
spec) (b -> Bool) -> (v -> b) -> v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> b
v -> Maybe v
forall a. a -> Maybe a
Just) a
Map a v
m)
          ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
              [ String
"propagate (lookup HOLE ms) on (MemberSpec ms)"
              , String
"forall pairs (d,r) in ms, no 'd' conforms to spec"
              , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SpecificationD Deps b -> String
forall a. Show a => a -> String
show SpecificationD Deps b
spec
              ]
          )

  mapTypeSpec :: forall a b.
(HasSpec a, HasSpec b) =>
MapW '[a] b -> TypeSpec a -> Specification b
mapTypeSpec MapW '[a] b
DomW (MapSpec Maybe Integer
_ Set k
mustSet [v]
_ Specification Integer
sz Specification (k, v)
kvSpec FoldSpec v
_) = TypeSpec b -> Specification b
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec b -> Specification b) -> TypeSpec b -> Specification b
forall a b. (a -> b) -> a -> b
$ Set k -> Specification k -> Specification Integer -> SetSpec k
forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set k
mustSet (Specification (k, v) -> Specification k
forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification k
fstSpec Specification (k, v)
kvSpec) Specification Integer
sz
  mapTypeSpec MapW '[a] b
RngW (MapSpec Maybe Integer
_ Set k
_ [v]
mustList Specification Integer
sz Specification (k, v)
kvSpec FoldSpec v
foldSpec) = TypeSpec b -> Specification b
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec b -> Specification b) -> TypeSpec b -> Specification b
forall a b. (a -> b) -> a -> b
$ Maybe Integer
-> [v]
-> Specification Integer
-> Specification v
-> FoldSpec v
-> ListSpec v
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [v]
mustList Specification Integer
sz (Specification (k, v) -> Specification v
forall k v.
(HasSpec k, HasSpec v) =>
Specification (k, v) -> Specification v
sndSpec Specification (k, v)
kvSpec) FoldSpec v
foldSpec

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

dom_ ::
  (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) =>
  Term (Map k v) ->
  Term (Set k)
dom_ :: forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ = MapW '[Map k v] (Set k)
-> FunTy (MapList Term '[Map k v]) (TermD Deps (Set k))
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm MapW '[Map k v] (Set k)
forall k v.
(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) =>
MapW '[Map k v] (Set k)
DomW

rng_ ::
  (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
  Term (Map k v) ->
  Term [v]
rng_ :: forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ = MapW '[Map k v] [v]
-> FunTy (MapList Term '[Map k v]) (TermD Deps [v])
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm MapW '[Map k v] [v]
forall k v.
(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) =>
MapW '[Map k v] [v]
RngW

lookup_ ::
  (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
  Term k ->
  Term (Map k v) ->
  Term (Maybe v)
lookup_ :: forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ = MapW '[k, Map k v] (Maybe v)
-> FunTy (MapList Term '[k, Map k v]) (TermD Deps (Maybe v))
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm MapW '[k, Map k v] (Maybe v)
forall k v.
(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) =>
MapW '[k, Map k v] (Maybe v)
LookupW