{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Constrained.Examples.Map where

import Constrained.API
import Constrained.Examples.Basic
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Word

mapElemSpec :: Specification (Map Int (Bool, Int))
mapElemSpec :: Specification (Map Int (Bool, Int))
mapElemSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Int (Bool, Int))
m ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Map Int (Bool, Int))
m forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit forall a. Monoid a => a
mempty
  , 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 k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int (Bool, Int))
m) forall a b. (a -> b) -> a -> b
$ \Term Bool
_ Term Int
b ->
      [Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
b, Term Int
b forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
10]
  ]

mapPairSpec :: Specification (Map Int Int, Set Int)
mapPairSpec :: Specification (Map Int Int, Set Int)
mapPairSpec = 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 b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m Term (Set Int)
s ->
  forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (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 Int Int)
m) Term (Set Int)
s

mapEmptyDomainSpec :: Specification (Map Int Int)
mapEmptyDomainSpec :: Specification (Map Int Int)
mapEmptyDomainSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m ->
  forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (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 Int Int)
m) forall a. Monoid a => a
mempty -- mempty in the Monoid instance (Term fn (Set a))

mapSubSize :: Specification (Map Int Int)
mapSubSize :: Specification (Map Int Int)
mapSubSize = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
s ->
  Term Integer
2 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
12 forall a. Num a => a -> a -> a
- (forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map Int Int)
s)

knownDomainMap :: Specification (Map Int Int)
knownDomainMap :: Specification (Map Int Int)
knownDomainMap = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m ->
  [ 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 Int Int)
m forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit (forall a. Ord a => [a] -> Set a
Set.fromList [Int
1, Int
2])
  , Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ Term Int
0 forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int Int)
m
  ]

mapSizeConstrained :: Specification (Map Three Int)
mapSizeConstrained :: Specification (Map Three Int)
mapSizeConstrained = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Three Int)
m -> forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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 Three Int)
m) forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
3

sumRange :: Specification (Map Word64 Word64)
sumRange :: Specification (Map Word64 Word64)
sumRange = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Word64 Word64)
m -> forall a. Foldy a => Term [a] -> Term a
sum_ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Word64 Word64)
m) forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Word64
10

fixedRange :: Specification (Map Int Int)
fixedRange :: Specification (Map Int Int)
fixedRange = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m ->
  [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int Int)
m) (\Term Int
x -> Term Int
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
5)
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ (forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map Int Int)
m) forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
1
  ]

rangeHint :: Specification (Map Int Int)
rangeHint :: Specification (Map Int Int)
rangeHint = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m ->
  forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
10 (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int Int)
m)

rangeSumSize :: Specification (Map Int Int)
rangeSumSize :: Specification (Map Int Int)
rangeSumSize = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map Int Int)
m forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
0
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. Foldy a => Term [a] -> Term a
sum_ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int Int)
m) forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
0
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ (-Term Int
1) forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. forall a. Foldy a => Term [a] -> Term a
sum_ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int Int)
m)
  , 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 (Map Int Int)
m forall a b. (a -> b) -> a -> b
$ \Term Int
k Term Int
v ->
      [ Term Int
k forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (-Term Int
1)
      , Term Int
v forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
1
      ]
  ]

elemSpec :: Specification (Int, Int, Map Int Int)
elemSpec :: Specification (Int, Int, Map Int Int)
elemSpec = 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 b. (a -> b) -> a -> b
$ \ Term Int
[var|key|] Term Int
[var|val|] Term (Map Int Int)
[var|mapp|] ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
key forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` 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 Int Int)
mapp
  , 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 (Map Int Int)
mapp forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|k'|] Term Int
[var|v'|] ->
      forall p. IsPred p => Term Bool -> p -> Pred
whenTrue (Term Int
k' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
key) (Term Int
v' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
val)
  , Term (Map Int Int)
mapp forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
key
  ]

lookupSpecific :: Specification (Int, Int, Map Int Int)
lookupSpecific :: Specification (Int, Int, Map Int Int)
lookupSpecific = 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 b. (a -> b) -> a -> b
$ \ Term Int
[var|k|] Term Int
[var|v|] Term (Map Int Int)
[var|m|] ->
  [ Term (Map Int Int)
m forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
k
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term Int
k Term (Map Int Int)
m forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. (HasSpec a, IsNormalType a) => Term a -> Term (Maybe a)
cJust_ Term Int
v
  ]

mapRestrictedValues :: Specification (Map (Either Int ()) Int)
mapRestrictedValues :: Specification (Map (Either Int ()) Int)
mapRestrictedValues = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map (Either Int ()) Int)
m ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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 (Either Int ()) Int)
m) forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
6
  , 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 (Map (Either Int ()) Int)
m forall a b. (a -> b) -> a -> b
$ \Term (Either Int ())
k Term Int
v ->
      [ 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 (Either Int ())
k
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> Term Int
20 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
v)
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
      , Term Int
v forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Either Int ())
k
      ]
  ]

-- NOTE: this fails if you pick the values of the map first - you're unlikely to generate
-- three values such that two of them are <= -100 and >= 100 respectively even though
-- you take satisfiability of the whole elem constraint into account. This can't be fixed
-- with a `dependsOn v k` because the issue is that we've generated a bunch of values
-- before we ever go to generate the keys.
mapRestrictedValuesThree :: Specification (Map Three Int)
mapRestrictedValuesThree :: Specification (Map Three Int)
mapRestrictedValuesThree = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Three Int)
m ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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 Three Int)
m) forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
3
  , 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 (Map Three Int)
m forall a b. (a -> b) -> a -> b
$ \Term Three
k Term Int
v ->
      [ 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 Three
k
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Term Int
v forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. (-Term Int
100))
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Term Int
100 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
v)
          (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
      , -- This is important to demonstrate the point that keys sometimes need to be solved before
        -- values
        Term Int
v forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Three
k
      ]
  ]

mapRestrictedValuesBool :: Specification (Map Bool Int)
mapRestrictedValuesBool :: Specification (Map Bool Int)
mapRestrictedValuesBool = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map Bool Int)
m ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (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 Bool Int)
m) forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
2
  , 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 (Map Bool Int)
m forall a b. (a -> b) -> a -> b
$ \Term Bool
k Term Int
v -> [Term Int
v forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Bool
k, forall p. IsPred p => Term Bool -> p -> Pred
whenTrue Term Bool
k (Term Int
100 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
v)]
  ]

mapSetSmall :: Specification (Map (Set Int) Int)
mapSetSmall :: Specification (Map (Set Int) Int)
mapSetSmall = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map (Set Int) Int)
x ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (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 (Set Int) Int)
x) forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
d ->
    forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set Int)
d forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => a -> Term a
lit (forall a. Ord a => [a] -> Set a
Set.fromList [Int
3 .. Int
4])

-- | this tests the function saturatePred
mapIsJust :: Specification (Int, Int)
mapIsJust :: Specification (Int, Int)
mapIsJust = 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 b. (a -> b) -> a -> b
$ \ Term Int
[var| x |] Term Int
[var| y |] ->
  forall a. (HasSpec a, IsNormalType a) => Term a -> Term (Maybe a)
cJust_ Term Int
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term Int
y (forall a. HasSpec a => a -> Term a
lit forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int
z, Int
z) | Int
z <- [Int
100 .. Int
102]])