{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Test.IOTasks.Var (
  Varname,
  Var(..), pattern Var,
  Embeddable(..), Embedded(..),
  SomeVar(..), someVar, someVarname, withSomeVar,
  SomeConsistentVars(..), someConsistentVars, withSomeConsistentVars,
  withConsistentList,
  filterType,
  intVar, stringVar, boolVar, embeddedVar,
  varname, varTypeRep,
  VarExp(..),
  MergedVars, merge,
  ) where

import Type.Reflection
import Data.GADT.Compare
import Data.List (sort, nub)
import Data.Bifunctor (first)
import Type.Match (inCaseOfE', matchTypeOfMaybe)
import Data.Maybe (mapMaybe)

type Varname = String

data Var a where
  IntVar :: Varname -> Var Integer
  BoolVar :: Varname -> Var Bool
  StringVar :: Varname -> Var String
  EmbeddedVar :: (Embeddable a, Show a, Read a) => TypeRep a -> Varname -> Var (Embedded a)

deriving instance Show (Var a)

-- | Values embeddable into a finite set of integers
--
-- Laws:
--
-- > asInteger . asOriginal = id
--
-- For types with Eq instances that induce non-trivial equivalence classes, at least the weaker
--
-- > asOriginal (asInteger x) == x = True
--
-- should hold. However program coverage is weakened in such scenarios, as generated inputs will only
-- ever contain values from the co-domain of 'asOriginal'.
class Embeddable a where
  asInteger :: a -> Integer
  asOriginal :: Integer -> a
  embeddingRange :: [Integer]

data Embedded a where
  Embedded :: (Show a, Embeddable a) => Integer -> Embedded a

deriving instance Eq (Embedded a)
instance Show a => Show (Embedded a) where
  show :: Embedded a -> Varname
show (Embedded Integer
i) = Varname
"Embedded (asInteger "Varname -> ShowS
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Varname
show @a (Integer -> a
forall a. Embeddable a => Integer -> a
asOriginal Integer
i) Varname -> ShowS
forall a. [a] -> [a] -> [a]
++ Varname
")"

instance (Show a, Read a, Embeddable a) => Read (Embedded a) where
  readsPrec :: Int -> ReadS (Embedded a)
readsPrec Int
p Varname
x = (a -> Embedded a) -> (a, Varname) -> (Embedded a, Varname)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Integer -> Embedded a
forall a. (Show a, Embeddable a) => Integer -> Embedded a
Embedded (Integer -> Embedded a) -> (a -> Integer) -> a -> Embedded a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Embeddable a => a -> Integer
asInteger)  ((a, Varname) -> (Embedded a, Varname))
-> [(a, Varname)] -> [(Embedded a, Varname)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Read a => Int -> ReadS a
readsPrec @a Int
p Varname
x

{-# COMPLETE Var #-}
pattern Var :: (Varname, TypeRep a) -> Var a
pattern $mVar :: forall {r} {a}.
Var a -> ((Varname, TypeRep a) -> r) -> ((# #) -> r) -> r
Var x <- ((\Var a
v -> (Var a -> Varname
forall a. Var a -> Varname
varname Var a
v, Var a -> TypeRep a
forall a. Var a -> TypeRep a
varTypeRep Var a
v)) -> x)

data SomeVar where
  SomeVar :: Typeable a => Var a -> SomeVar

someVar :: Typeable a => Var a -> SomeVar
someVar :: forall a. Typeable a => Var a -> SomeVar
someVar = Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
SomeVar

withSomeVar :: SomeVar -> (forall a. Typeable a => Var a -> r) -> r
withSomeVar :: forall r. SomeVar -> (forall a. Typeable a => Var a -> r) -> r
withSomeVar (SomeVar Var a
x) forall a. Typeable a => Var a -> r
f = Var a -> r
forall a. Typeable a => Var a -> r
f Var a
x

withConsistentList :: [SomeVar] -> (forall a. Typeable a => [Var a] -> r) -> Maybe r
withConsistentList :: forall r.
[SomeVar] -> (forall a. Typeable a => [Var a] -> r) -> Maybe r
withConsistentList [SomeVar]
xs forall a. Typeable a => [Var a] -> r
f = do
  SomeConsistentVars
same <- [SomeVar] -> Maybe SomeConsistentVars
someConsistentVars [SomeVar]
xs
  r -> Maybe r
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (r -> Maybe r) -> r -> Maybe r
forall a b. (a -> b) -> a -> b
$ SomeConsistentVars -> (forall a. Typeable a => [Var a] -> r) -> r
forall r.
SomeConsistentVars -> (forall a. Typeable a => [Var a] -> r) -> r
withSomeConsistentVars SomeConsistentVars
same [Var a] -> r
forall a. Typeable a => [Var a] -> r
f

data SomeConsistentVars where
  SomeConsistentVars :: Typeable a => [Var a] -> SomeConsistentVars

withSomeConsistentVars :: SomeConsistentVars -> (forall a. Typeable a => [Var a] -> r) -> r
withSomeConsistentVars :: forall r.
SomeConsistentVars -> (forall a. Typeable a => [Var a] -> r) -> r
withSomeConsistentVars (SomeConsistentVars [Var a]
xs) forall a. Typeable a => [Var a] -> r
f = [Var a] -> r
forall a. Typeable a => [Var a] -> r
f [Var a]
xs

someConsistentVars :: [SomeVar] -> Maybe SomeConsistentVars
someConsistentVars :: [SomeVar] -> Maybe SomeConsistentVars
someConsistentVars [] = Maybe SomeConsistentVars
forall a. Maybe a
Nothing
someConsistentVars (SomeVar
x:[SomeVar]
xs) = (SomeVar -> Maybe SomeConsistentVars -> Maybe SomeConsistentVars)
-> Maybe SomeConsistentVars
-> [SomeVar]
-> Maybe SomeConsistentVars
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\SomeVar
y Maybe SomeConsistentVars
mys -> SomeVar -> SomeConsistentVars -> Maybe SomeConsistentVars
addSome SomeVar
y (SomeConsistentVars -> Maybe SomeConsistentVars)
-> Maybe SomeConsistentVars -> Maybe SomeConsistentVars
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe SomeConsistentVars
mys) (SomeVar
-> (forall a. Typeable a => Var a -> Maybe SomeConsistentVars)
-> Maybe SomeConsistentVars
forall r. SomeVar -> (forall a. Typeable a => Var a -> r) -> r
withSomeVar SomeVar
x (SomeConsistentVars -> Maybe SomeConsistentVars
forall a. a -> Maybe a
Just (SomeConsistentVars -> Maybe SomeConsistentVars)
-> (Var a -> SomeConsistentVars)
-> Var a
-> Maybe SomeConsistentVars
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var a] -> SomeConsistentVars
forall a. Typeable a => [Var a] -> SomeConsistentVars
SomeConsistentVars ([Var a] -> SomeConsistentVars)
-> (Var a -> [Var a]) -> Var a -> SomeConsistentVars
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var a -> [Var a]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure)) [SomeVar]
xs

addSome :: SomeVar -> SomeConsistentVars -> Maybe SomeConsistentVars
addSome :: SomeVar -> SomeConsistentVars -> Maybe SomeConsistentVars
addSome (SomeVar (Var a
x :: Var a)) (SomeConsistentVars ([Var a]
ys :: [Var b])) =
  case TypeRep a -> TypeRep a -> Maybe (a :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b) of
    Just a :~~: a
HRefl -> SomeConsistentVars -> Maybe SomeConsistentVars
forall a. a -> Maybe a
Just (SomeConsistentVars -> Maybe SomeConsistentVars)
-> SomeConsistentVars -> Maybe SomeConsistentVars
forall a b. (a -> b) -> a -> b
$ [Var a] -> SomeConsistentVars
forall a. Typeable a => [Var a] -> SomeConsistentVars
SomeConsistentVars (Var a
xVar a -> [Var a] -> [Var a]
forall a. a -> [a] -> [a]
:[Var a]
[Var a]
ys)
    Maybe (a :~~: a)
Nothing -> Maybe SomeConsistentVars
forall a. Maybe a
Nothing

filterType :: forall a. Typeable a => [SomeVar] -> [Var a]
filterType :: forall a. Typeable a => [SomeVar] -> [Var a]
filterType = (SomeVar -> Maybe (Var a)) -> [SomeVar] -> [Var a]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(SomeVar Var a
x) -> Var a -> [Case (Var a) (Var a)] -> Maybe (Var a)
forall a r. Typeable a => a -> [Case a r] -> Maybe r
matchTypeOfMaybe Var a
x [forall {k1} {k} (a :: k1) (x :: k) r.
Typeable a =>
((a :~~: x) -> r) -> Case x r
forall a x r. Typeable a => ((a :~~: x) -> r) -> Case x r
inCaseOfE' @(Var a) (((Var a :~~: Var a) -> Var a) -> Case (Var a) (Var a))
-> ((Var a :~~: Var a) -> Var a) -> Case (Var a) (Var a)
forall a b. (a -> b) -> a -> b
$ \Var a :~~: Var a
HRefl -> Var a
Var a
x])

instance Eq (Var a) where
  == :: Var a -> Var a -> Bool
(==) = Var a -> Var a -> Bool
forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq

instance Ord (Var a) where
  compare :: Var a -> Var a -> Ordering
compare = Var a -> Var a -> Ordering
forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare

instance GEq Var where
  geq :: forall a b. Var a -> Var b -> Maybe (a :~: b)
geq Var a
x Var b
y = case Var a -> Var b -> GOrdering a b
forall a b. Var a -> Var b -> GOrdering a b
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare Var a
x Var b
y of
    GOrdering a b
GEQ -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    GOrdering a b
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing

instance GCompare Var where
  gcompare :: forall a b. Var a -> Var b -> GOrdering a b
gcompare (Var (Varname
x,TypeRep a
tx)) (Var (Varname
y,TypeRep b
ty)) =
    case Varname -> Varname -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Varname
x Varname
y of
      Ordering
LT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
      Ordering
EQ -> TypeRep a -> TypeRep b -> GOrdering a b
forall a b. TypeRep a -> TypeRep b -> GOrdering a b
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare TypeRep a
tx TypeRep b
ty
      Ordering
GT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT

instance Eq SomeVar where
  SomeVar
x == :: SomeVar -> SomeVar -> Bool
== SomeVar
y = SomeVar -> SomeVar -> Ordering
forall a. Ord a => a -> a -> Ordering
compare SomeVar
x SomeVar
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ
instance Ord SomeVar where
  compare :: SomeVar -> SomeVar -> Ordering
compare (SomeVar Var a
x) (SomeVar Var a
y) = case Var a -> Var a -> GOrdering a a
forall a b. Var a -> Var b -> GOrdering a b
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare Var a
x Var a
y of
    GOrdering a a
GLT -> Ordering
LT
    GOrdering a a
GEQ -> Ordering
EQ
    GOrdering a a
GGT -> Ordering
GT
deriving instance Show SomeVar

varname :: Var a -> Varname
varname :: forall a. Var a -> Varname
varname (IntVar Varname
x) = Varname
x
varname (BoolVar Varname
x) = Varname
x
varname (StringVar Varname
x) = Varname
x
varname (EmbeddedVar TypeRep a
_ Varname
x) = Varname
x

varTypeRep :: Var a -> TypeRep a
varTypeRep :: forall a. Var a -> TypeRep a
varTypeRep IntVar{} = TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
varTypeRep BoolVar{} = TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
varTypeRep StringVar{} = TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
varTypeRep (EmbeddedVar TypeRep a
ty Varname
_) = TypeRep Embedded -> TypeRep a -> TypeRep a
forall k2 (t :: k2) k1 (a :: k1 -> k2) (b :: k1).
(t ~ a b) =>
TypeRep a -> TypeRep b -> TypeRep t
App (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> *). Typeable a => TypeRep a
typeRep @Embedded) TypeRep a
ty

someVarname :: SomeVar -> Varname
someVarname :: SomeVar -> Varname
someVarname (SomeVar Var a
x) = Var a -> Varname
forall a. Var a -> Varname
varname Var a
x

intVar :: Varname -> Var Integer
intVar :: Varname -> Var Integer
intVar = Varname -> Var Integer
IntVar

boolVar :: Varname -> Var Bool
boolVar :: Varname -> Var Bool
boolVar = Varname -> Var Bool
BoolVar

stringVar :: Varname -> Var String
stringVar :: Varname -> Var Varname
stringVar = Varname -> Var Varname
StringVar

embeddedVar :: (Typeable a, Embeddable a, Show a, Read a) => Varname -> Var (Embedded a)
embeddedVar :: forall a.
(Typeable a, Embeddable a, Show a, Read a) =>
Varname -> Var (Embedded a)
embeddedVar = TypeRep a -> Varname -> Var (Embedded a)
forall a.
(Embeddable a, Show a, Read a) =>
TypeRep a -> Varname -> Var (Embedded a)
EmbeddedVar TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep

-- | Abstraction over different types of variable-expressions.
--
-- A variable-expression references one or more specification variables and
-- can be used to access the values assigned to these specific variables.
--
-- If an expression references more than one variable, the values of these
-- variables are interleaved chronologically. I.e., 'currentValue' will provide
-- access to the current value of the last modified variable from the list and
-- 'allValues' gives a list where values appear in the order they were given to the program.
--
-- Additionally, all referenced variables must be of the same type.
--
-- Instances need to make sure that the resulting list is sorted!
class VarExp e where
  toVarList :: e a -> [Var a]
  -- ^ Computes the list of variables referenced by the variable expression.

instance VarExp Var where
  toVarList :: forall a. Var a -> [Var a]
toVarList = Var a -> [Var a]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure

newtype MergedVars a = MergedVars { forall a. MergedVars a -> [Var a]
mergedVars :: [Var a] }
  deriving (MergedVars a -> MergedVars a -> Bool
(MergedVars a -> MergedVars a -> Bool)
-> (MergedVars a -> MergedVars a -> Bool) -> Eq (MergedVars a)
forall a. MergedVars a -> MergedVars a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. MergedVars a -> MergedVars a -> Bool
== :: MergedVars a -> MergedVars a -> Bool
$c/= :: forall a. MergedVars a -> MergedVars a -> Bool
/= :: MergedVars a -> MergedVars a -> Bool
Eq, Int -> MergedVars a -> ShowS
[MergedVars a] -> ShowS
MergedVars a -> Varname
(Int -> MergedVars a -> ShowS)
-> (MergedVars a -> Varname)
-> ([MergedVars a] -> ShowS)
-> Show (MergedVars a)
forall a. Int -> MergedVars a -> ShowS
forall a. [MergedVars a] -> ShowS
forall a. MergedVars a -> Varname
forall a.
(Int -> a -> ShowS) -> (a -> Varname) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Int -> MergedVars a -> ShowS
showsPrec :: Int -> MergedVars a -> ShowS
$cshow :: forall a. MergedVars a -> Varname
show :: MergedVars a -> Varname
$cshowList :: forall a. [MergedVars a] -> ShowS
showList :: [MergedVars a] -> ShowS
Show)

merge :: [Var a] -> MergedVars a
merge :: forall a. [Var a] -> MergedVars a
merge = [Var a] -> MergedVars a
forall a. [Var a] -> MergedVars a
MergedVars

instance VarExp MergedVars where
  toVarList :: forall a. MergedVars a -> [Var a]
toVarList = [Var a] -> [Var a]
forall a. Ord a => [a] -> [a]
sort ([Var a] -> [Var a])
-> (MergedVars a -> [Var a]) -> MergedVars a -> [Var a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var a] -> [Var a]
forall a. Eq a => [a] -> [a]
nub ([Var a] -> [Var a])
-> (MergedVars a -> [Var a]) -> MergedVars a -> [Var a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MergedVars a -> [Var a]
forall a. MergedVars a -> [Var a]
mergedVars