{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RecordWildCards #-}
module Test.IOTasks.Constraints (
  SimpleConstraint(..),
  Constraint(..),
  ConstraintType(..),
  ConstraintTree(..),
  constraintTree,
  SimplePath(..), simplePaths,
  appendPath, addEnvToPath, canBeInjected, injectionPoints,
  Path, SymbolicInfo(..),
  storedValues,
  completePath, partitionPath,
  pathDepth,
  numberOfPaths,
  showSimplePath, showSimpleConstraint, showSomeSimpleConstraint,
  showPath, showConstraint, showSomeConstraint,
  ix
  ) where

import Test.IOTasks.ValueSet
import Test.IOTasks.Internal.Term
import Test.IOTasks.Var (Var, SomeVar, someVar, varname)
import Test.IOTasks.Term.Prelude (not')
import Test.IOTasks.Internal.Specification
import Test.IOTasks.OutputPattern (valueTerms)

import Data.List (intersperse)
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Set as Set (toList)
import Data.Maybe (catMaybes, mapMaybe)
import Data.Tuple.Extra (fst3)
import Data.Typeable
import Data.Some

data SimpleConstraint (t :: ConstraintType) where
  SimpleInput :: Typeable v => StorageType -> Var v -> ValueSet v -> SimpleConstraint 'Input
  SimpleCondition :: Term 'Transparent Bool -> SimpleConstraint 'Condition
  SimpleOverflow :: [Term 'Transparent Integer] -> SimpleConstraint 'Overflow

data StorageType = KeepInput | DropInput
  deriving Int -> StorageType -> ShowS
[StorageType] -> ShowS
StorageType -> String
(Int -> StorageType -> ShowS)
-> (StorageType -> String)
-> ([StorageType] -> ShowS)
-> Show StorageType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> StorageType -> ShowS
showsPrec :: Int -> StorageType -> ShowS
$cshow :: StorageType -> String
show :: StorageType -> String
$cshowList :: [StorageType] -> ShowS
showList :: [StorageType] -> ShowS
Show

data Constraint (t :: ConstraintType) where
  InputConstraint :: Typeable v => (Var v, Int) -> ValueSet v -> Map SomeVar SymbolicInfo -> Constraint 'Input
  ConditionConstraint :: Term 'Transparent Bool -> Map SomeVar SymbolicInfo -> Constraint 'Condition
  OverflowConstraints :: [Term 'Transparent Integer] -> Map SomeVar SymbolicInfo -> Constraint 'Overflow

data ConstraintType = Input | Condition | Overflow

data ConstraintTree where
  Choice :: ConstraintTree -> ConstraintTree -> ConstraintTree
  Assert :: (SimpleConstraint t) -> ConstraintTree -> ConstraintTree
  Unfold :: ConstraintTree -> ConstraintTree -- marker for counting path lengths
  InjectionPoint :: (SimpleConstraint 'Input) -> ConstraintTree -> ConstraintTree  -- position for injecting the the given constraint 0 to n many times
  Empty :: ConstraintTree

constraintTree :: Specification -> ConstraintTree
constraintTree :: Specification -> ConstraintTree
constraintTree =
  (forall v.
 (Typeable v, Read v, Show v) =>
 ()
 -> Var v
 -> ValueSet v
 -> InputMode
 -> RecStruct
      (SimpleConstraint 'Input, SimpleConstraint 'Input, InputMode)
      (ConstraintTree -> ConstraintTree)
      ()
      ConstraintTree)
-> (RecStruct
      (SimpleConstraint 'Input, SimpleConstraint 'Input, InputMode)
      ()
      ConstraintTree
      ConstraintTree
    -> ConstraintTree)
-> (forall (k :: PatternKind).
    ()
    -> OptFlag
    -> Set (OutputPattern k)
    -> ConstraintTree
    -> ConstraintTree)
-> (()
    -> Term 'Transparent Bool
    -> ConstraintTree
    -> ConstraintTree
    -> ConstraintTree)
-> (Action -> ConstraintTree -> ConstraintTree)
-> (ConstraintTree -> ConstraintTree)
-> ConstraintTree
-> ()
-> Specification
-> ConstraintTree
forall st p a.
(forall v.
 (Typeable v, Read v, Show v) =>
 st
 -> Var v -> ValueSet v -> InputMode -> RecStruct p (a -> a) st a)
-> (RecStruct p () a a -> a)
-> (forall (k :: PatternKind).
    st -> OptFlag -> Set (OutputPattern k) -> a -> a)
-> (st -> Term 'Transparent Bool -> a -> a -> a)
-> (Action -> a -> a)
-> (a -> a)
-> a
-> st
-> Specification
-> a
sem
    (\() Var v
x ValueSet v
vs InputMode
mode ->
      let
        p :: (SimpleConstraint 'Input, SimpleConstraint 'Input, InputMode)
p = (StorageType -> Var v -> ValueSet v -> SimpleConstraint 'Input
forall v.
Typeable v =>
StorageType -> Var v -> ValueSet v -> SimpleConstraint 'Input
SimpleInput StorageType
KeepInput Var v
x ValueSet v
vs
            ,StorageType -> Var v -> ValueSet v -> SimpleConstraint 'Input
forall v.
Typeable v =>
StorageType -> Var v -> ValueSet v -> SimpleConstraint 'Input
SimpleInput StorageType
DropInput Var v
x (ValueSet v -> ValueSet v
forall a. ValueSet a -> ValueSet a
complement ValueSet v
vs)
            , InputMode
mode)
      in (SimpleConstraint 'Input, SimpleConstraint 'Input, InputMode)
-> (ConstraintTree -> ConstraintTree)
-> ()
-> RecStruct
     (SimpleConstraint 'Input, SimpleConstraint 'Input, InputMode)
     (ConstraintTree -> ConstraintTree)
     ()
     ConstraintTree
forall p x a r. p -> x -> a -> RecStruct p x a r
RecSub (SimpleConstraint 'Input, SimpleConstraint 'Input, InputMode)
p ConstraintTree -> ConstraintTree
forall a. a -> a
id ()
    )
    (\case
      RecSub (SimpleConstraint 'Input
vsP,SimpleConstraint 'Input
_, InputMode
AssumeValid) () ConstraintTree
s' -> SimpleConstraint 'Input -> ConstraintTree -> ConstraintTree
forall (v :: ConstraintType).
SimpleConstraint v -> ConstraintTree -> ConstraintTree
Assert SimpleConstraint 'Input
vsP ConstraintTree
s'
      RecSub (SimpleConstraint 'Input
vsP,SimpleConstraint 'Input
vsN, InputMode
UntilValid) () ConstraintTree
s' -> SimpleConstraint 'Input -> ConstraintTree -> ConstraintTree
InjectionPoint SimpleConstraint 'Input
vsN (ConstraintTree -> ConstraintTree)
-> ConstraintTree -> ConstraintTree
forall a b. (a -> b) -> a -> b
$ SimpleConstraint 'Input -> ConstraintTree -> ConstraintTree
forall (v :: ConstraintType).
SimpleConstraint v -> ConstraintTree -> ConstraintTree
Assert SimpleConstraint 'Input
vsP ConstraintTree
s'
      RecSub (SimpleConstraint 'Input
vsP,SimpleConstraint 'Input
vsN, InputMode
ElseAbort) () ConstraintTree
s' -> ConstraintTree -> ConstraintTree -> ConstraintTree
Choice
        (SimpleConstraint 'Input -> ConstraintTree -> ConstraintTree
forall (v :: ConstraintType).
SimpleConstraint v -> ConstraintTree -> ConstraintTree
Assert SimpleConstraint 'Input
vsN ConstraintTree
Empty)
        (SimpleConstraint 'Input -> ConstraintTree -> ConstraintTree
forall (v :: ConstraintType).
SimpleConstraint v -> ConstraintTree -> ConstraintTree
Assert SimpleConstraint 'Input
vsP ConstraintTree
s')
      RecBoth{} -> String -> ConstraintTree
forall a. HasCallStack => String -> a
error String
"constraintTree: impossible"
      NoRec ConstraintTree
_ -> String -> ConstraintTree
forall a. HasCallStack => String -> a
error String
"constraintTree: impossible"
      RecSame{} -> String -> ConstraintTree
forall a. HasCallStack => String -> a
error String
"constraintTree: impossible"
    )
    (\() OptFlag
_ Set (OutputPattern k)
ps ConstraintTree
t -> SimpleConstraint 'Overflow -> ConstraintTree -> ConstraintTree
forall (v :: ConstraintType).
SimpleConstraint v -> ConstraintTree -> ConstraintTree
Assert ([Term 'Transparent Integer] -> SimpleConstraint 'Overflow
SimpleOverflow ([Maybe (Term 'Transparent Integer)] -> [Term 'Transparent Integer]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Term 'Transparent Integer)]
 -> [Term 'Transparent Integer])
-> [Maybe (Term 'Transparent Integer)]
-> [Term 'Transparent Integer]
forall a b. (a -> b) -> a -> b
$ [ forall a.
Typeable a =>
SomeTerm 'Transparent -> Maybe (Term 'Transparent a)
forall {k :: TermKind} a.
Typeable a =>
SomeTerm k -> Maybe (Term k a)
castTerm @Integer SomeTerm 'Transparent
t | OutputPattern k
p <- Set (OutputPattern k) -> [OutputPattern k]
forall a. Set a -> [a]
Set.toList Set (OutputPattern k)
ps, SomeTermK
vt <- OutputPattern k -> [SomeTermK]
forall (k :: PatternKind). OutputPattern k -> [SomeTermK]
valueTerms OutputPattern k
p, SomeTerm 'Transparent
t <- SomeTermK
-> (forall (k :: TermKind) a.
    Typeable a =>
    Term k a -> [SomeTerm 'Transparent])
-> [SomeTerm 'Transparent]
forall r.
SomeTermK
-> (forall (k :: TermKind) a. Typeable a => Term k a -> r) -> r
withSomeTermK SomeTermK
vt Term k a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
forall (k :: TermKind) a.
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms])) ConstraintTree
t)
    (\() Term 'Transparent Bool
c ConstraintTree
l ConstraintTree
r -> SimpleConstraint 'Overflow -> ConstraintTree -> ConstraintTree
forall (v :: ConstraintType).
SimpleConstraint v -> ConstraintTree -> ConstraintTree
Assert ([Term 'Transparent Integer] -> SimpleConstraint 'Overflow
SimpleOverflow ((SomeTerm 'Transparent -> Maybe (Term 'Transparent Integer))
-> [SomeTerm 'Transparent] -> [Term 'Transparent Integer]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall a.
Typeable a =>
SomeTerm 'Transparent -> Maybe (Term 'Transparent a)
forall {k :: TermKind} a.
Typeable a =>
SomeTerm k -> Maybe (Term k a)
castTerm @Integer) ([SomeTerm 'Transparent] -> [Term 'Transparent Integer])
-> [SomeTerm 'Transparent] -> [Term 'Transparent Integer]
forall a b. (a -> b) -> a -> b
$ Term 'Transparent Bool -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term 'Transparent Bool
c)) (ConstraintTree -> ConstraintTree)
-> ConstraintTree -> ConstraintTree
forall a b. (a -> b) -> a -> b
$ ConstraintTree -> ConstraintTree -> ConstraintTree
Choice (SimpleConstraint 'Condition -> ConstraintTree -> ConstraintTree
forall (v :: ConstraintType).
SimpleConstraint v -> ConstraintTree -> ConstraintTree
Assert (Term 'Transparent Bool -> SimpleConstraint 'Condition
SimpleCondition Term 'Transparent Bool
c) ConstraintTree
l) (SimpleConstraint 'Condition -> ConstraintTree -> ConstraintTree
forall (v :: ConstraintType).
SimpleConstraint v -> ConstraintTree -> ConstraintTree
Assert (Term 'Transparent Bool -> SimpleConstraint 'Condition
SimpleCondition (Term 'Transparent Bool -> Term 'Transparent Bool
forall (k :: TermKind). Term k Bool -> Term k Bool
not' Term 'Transparent Bool
c)) ConstraintTree
r))
    (\case {Action
End -> ConstraintTree -> ConstraintTree
Unfold ; Action
Exit -> ConstraintTree -> ConstraintTree
forall a. a -> a
id})
    ConstraintTree -> ConstraintTree
Unfold
    ConstraintTree
Empty
    ()

data SimplePath where
  ClosedPath :: [Some SimpleConstraint] -> SimplePath
  OpenPath :: [Some SimpleConstraint] -> (SimpleConstraint t) -> SimplePath -> SimplePath

prependPath :: Some SimpleConstraint -> SimplePath -> SimplePath
prependPath :: Some SimpleConstraint -> SimplePath -> SimplePath
prependPath Some SimpleConstraint
c (ClosedPath [Some SimpleConstraint]
cs) = [Some SimpleConstraint] -> SimplePath
ClosedPath (Some SimpleConstraint
cSome SimpleConstraint
-> [Some SimpleConstraint] -> [Some SimpleConstraint]
forall a. a -> [a] -> [a]
:[Some SimpleConstraint]
cs)
prependPath Some SimpleConstraint
c (OpenPath [Some SimpleConstraint]
cs SimpleConstraint t
ic SimplePath
t) = [Some SimpleConstraint]
-> SimpleConstraint t -> SimplePath -> SimplePath
forall (v :: ConstraintType).
[Some SimpleConstraint]
-> SimpleConstraint v -> SimplePath -> SimplePath
OpenPath (Some SimpleConstraint
cSome SimpleConstraint
-> [Some SimpleConstraint] -> [Some SimpleConstraint]
forall a. a -> [a] -> [a]
:[Some SimpleConstraint]
cs) SimpleConstraint t
ic SimplePath
t

appendPath :: SimplePath -> SimplePath -> SimplePath
appendPath :: SimplePath -> SimplePath -> SimplePath
appendPath (ClosedPath [Some SimpleConstraint]
xs) (ClosedPath [Some SimpleConstraint]
ys) = [Some SimpleConstraint] -> SimplePath
ClosedPath ([Some SimpleConstraint] -> SimplePath)
-> [Some SimpleConstraint] -> SimplePath
forall a b. (a -> b) -> a -> b
$ [Some SimpleConstraint]
xs [Some SimpleConstraint]
-> [Some SimpleConstraint] -> [Some SimpleConstraint]
forall a. [a] -> [a] -> [a]
++ [Some SimpleConstraint]
ys
appendPath (ClosedPath [Some SimpleConstraint]
xs) (OpenPath [Some SimpleConstraint]
ys SimpleConstraint t
cy SimplePath
y) = [Some SimpleConstraint]
-> SimpleConstraint t -> SimplePath -> SimplePath
forall (v :: ConstraintType).
[Some SimpleConstraint]
-> SimpleConstraint v -> SimplePath -> SimplePath
OpenPath ([Some SimpleConstraint]
xs [Some SimpleConstraint]
-> [Some SimpleConstraint] -> [Some SimpleConstraint]
forall a. [a] -> [a] -> [a]
++ [Some SimpleConstraint]
ys) SimpleConstraint t
cy SimplePath
y
appendPath (OpenPath [Some SimpleConstraint]
xs SimpleConstraint t
cx SimplePath
x) SimplePath
y = [Some SimpleConstraint]
-> SimpleConstraint t -> SimplePath -> SimplePath
forall (v :: ConstraintType).
[Some SimpleConstraint]
-> SimpleConstraint v -> SimplePath -> SimplePath
OpenPath [Some SimpleConstraint]
xs SimpleConstraint t
cx (SimplePath -> SimplePath) -> SimplePath -> SimplePath
forall a b. (a -> b) -> a -> b
$ SimplePath -> SimplePath -> SimplePath
appendPath SimplePath
x SimplePath
y

canBeInjected :: SimplePath -> Bool
canBeInjected :: SimplePath -> Bool
canBeInjected ClosedPath{} = Bool
False
canBeInjected OpenPath{} = Bool
True

-- paths n t returns all terminating paths in t that use at most n unfoldings of iterations
simplePaths :: Int -> ConstraintTree -> [SimplePath]
simplePaths :: Int -> ConstraintTree -> [SimplePath]
simplePaths Int
_ ConstraintTree
Empty = [[Some SimpleConstraint] -> SimplePath
ClosedPath []]
simplePaths Int
n ConstraintTree
_ | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = []
simplePaths Int
n (Choice ConstraintTree
lt ConstraintTree
rt) = [SimplePath] -> [SimplePath] -> [SimplePath]
mergePaths (Int -> ConstraintTree -> [SimplePath]
simplePaths Int
n ConstraintTree
lt) (Int -> ConstraintTree -> [SimplePath]
simplePaths Int
n ConstraintTree
rt)
simplePaths Int
n (Assert SimpleConstraint t
c ConstraintTree
t) = Some SimpleConstraint -> SimplePath -> SimplePath
prependPath (SimpleConstraint t -> Some SimpleConstraint
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some SimpleConstraint t
c) (SimplePath -> SimplePath) -> [SimplePath] -> [SimplePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ConstraintTree -> [SimplePath]
simplePaths Int
n ConstraintTree
t
simplePaths Int
n (InjectionPoint SimpleConstraint 'Input
c ConstraintTree
t) = [Some SimpleConstraint]
-> SimpleConstraint 'Input -> SimplePath -> SimplePath
forall (v :: ConstraintType).
[Some SimpleConstraint]
-> SimpleConstraint v -> SimplePath -> SimplePath
OpenPath [] SimpleConstraint 'Input
c (SimplePath -> SimplePath) -> [SimplePath] -> [SimplePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ConstraintTree -> [SimplePath]
simplePaths Int
n ConstraintTree
t
simplePaths Int
n (Unfold ConstraintTree
t)
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Int -> ConstraintTree -> [SimplePath]
simplePaths (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ConstraintTree
t
  | Bool
otherwise = []

mergePaths :: [SimplePath] -> [SimplePath] -> [SimplePath]
mergePaths :: [SimplePath] -> [SimplePath] -> [SimplePath]
mergePaths [SimplePath]
xs [] = [SimplePath]
xs
mergePaths [] [SimplePath]
ys = [SimplePath]
ys
mergePaths (SimplePath
x:[SimplePath]
xs) (SimplePath
y:[SimplePath]
ys) = SimplePath
xSimplePath -> [SimplePath] -> [SimplePath]
forall a. a -> [a] -> [a]
:SimplePath
ySimplePath -> [SimplePath] -> [SimplePath]
forall a. a -> [a] -> [a]
:[SimplePath] -> [SimplePath] -> [SimplePath]
mergePaths [SimplePath]
xs [SimplePath]
ys

type Path = [Some Constraint]

completePath :: [Int] -> SimplePath -> Path
completePath :: [Int] -> SimplePath -> Path
completePath = [Some SimpleConstraint] -> Path
addEnvToPath ([Some SimpleConstraint] -> Path)
-> ([Int] -> SimplePath -> [Some SimpleConstraint])
-> [Int]
-> SimplePath
-> Path
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.: Int -> [Int] -> SimplePath -> [Some SimpleConstraint]
forall {a}.
(Eq a, Num a) =>
a -> [a] -> SimplePath -> [Some SimpleConstraint]
go Int
1 where
  go :: a -> [a] -> SimplePath -> [Some SimpleConstraint]
go a
_ [a]
_ (ClosedPath [Some SimpleConstraint]
cs) = [Some SimpleConstraint]
cs
  go a
n [] (OpenPath [Some SimpleConstraint]
cs SimpleConstraint t
_ SimplePath
p) = [Some SimpleConstraint]
cs [Some SimpleConstraint]
-> [Some SimpleConstraint] -> [Some SimpleConstraint]
forall a. [a] -> [a] -> [a]
++ a -> [a] -> SimplePath -> [Some SimpleConstraint]
go (a
na -> a -> a
forall a. Num a => a -> a -> a
+a
1) [] SimplePath
p
  go a
n (a
i:[a]
is) (OpenPath [Some SimpleConstraint]
cs SimpleConstraint t
c SimplePath
p)
    | a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
i = [Some SimpleConstraint]
cs [Some SimpleConstraint]
-> [Some SimpleConstraint] -> [Some SimpleConstraint]
forall a. [a] -> [a] -> [a]
++ (SimpleConstraint t -> Some SimpleConstraint
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some SimpleConstraint t
cSome SimpleConstraint
-> [Some SimpleConstraint] -> [Some SimpleConstraint]
forall a. a -> [a] -> [a]
: a -> [a] -> SimplePath -> [Some SimpleConstraint]
go a
n [a]
is ([Some SimpleConstraint]
-> SimpleConstraint t -> SimplePath -> SimplePath
forall (v :: ConstraintType).
[Some SimpleConstraint]
-> SimpleConstraint v -> SimplePath -> SimplePath
OpenPath [] SimpleConstraint t
c SimplePath
p))
    | Bool
otherwise = [Some SimpleConstraint]
cs [Some SimpleConstraint]
-> [Some SimpleConstraint] -> [Some SimpleConstraint]
forall a. [a] -> [a] -> [a]
++ a -> [a] -> SimplePath -> [Some SimpleConstraint]
go (a
na -> a -> a
forall a. Num a => a -> a -> a
+a
1) (a
ia -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
is) SimplePath
p

(.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d
.: :: forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
(.:) = ((b -> c) -> b -> d) -> (a -> b -> c) -> a -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) (((b -> c) -> b -> d) -> (a -> b -> c) -> a -> b -> d)
-> ((c -> d) -> (b -> c) -> b -> d)
-> (c -> d)
-> (a -> b -> c)
-> a
-> b
-> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> d) -> (b -> c) -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)

injectionPoints :: SimplePath -> Int
injectionPoints :: SimplePath -> Int
injectionPoints (ClosedPath [Some SimpleConstraint]
_) = Int
0
injectionPoints (OpenPath [Some SimpleConstraint]
_ SimpleConstraint t
_ SimplePath
p) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ SimplePath -> Int
injectionPoints SimplePath
p

addEnvToPath :: [Some SimpleConstraint] -> Path
addEnvToPath :: [Some SimpleConstraint] -> Path
addEnvToPath = ((Map SomeVar SymbolicInfo, Int), Path) -> Path
forall a b. (a, b) -> b
snd (((Map SomeVar SymbolicInfo, Int), Path) -> Path)
-> ([Some SimpleConstraint]
    -> ((Map SomeVar SymbolicInfo, Int), Path))
-> [Some SimpleConstraint]
-> Path
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Map SomeVar SymbolicInfo, Int), Path)
 -> Some SimpleConstraint
 -> ((Map SomeVar SymbolicInfo, Int), Path))
-> ((Map SomeVar SymbolicInfo, Int), Path)
-> [Some SimpleConstraint]
-> ((Map SomeVar SymbolicInfo, Int), Path)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\((Map SomeVar SymbolicInfo
e,Int
k),Path
p) (Some SimpleConstraint a
c) -> let (Map SomeVar SymbolicInfo
e',Constraint a
c') = Map SomeVar SymbolicInfo
-> Int
-> SimpleConstraint a
-> (Map SomeVar SymbolicInfo, Constraint a)
forall (t :: ConstraintType).
Map SomeVar SymbolicInfo
-> Int
-> SimpleConstraint t
-> (Map SomeVar SymbolicInfo, Constraint t)
addEnvToConstraint Map SomeVar SymbolicInfo
e Int
k SimpleConstraint a
c in ((Map SomeVar SymbolicInfo
e',Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1), Path
p Path -> Path -> Path
forall a. [a] -> [a] -> [a]
++ [Constraint a -> Some Constraint
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some Constraint a
c']) ) ((Map SomeVar SymbolicInfo
forall k a. Map k a
Map.empty,Int
1),[])

addEnvToConstraint :: Map SomeVar SymbolicInfo -> Int -> SimpleConstraint t -> (Map SomeVar SymbolicInfo, Constraint t)
addEnvToConstraint :: forall (t :: ConstraintType).
Map SomeVar SymbolicInfo
-> Int
-> SimpleConstraint t
-> (Map SomeVar SymbolicInfo, Constraint t)
addEnvToConstraint Map SomeVar SymbolicInfo
e Int
k (SimpleInput StorageType
ty Var v
x ValueSet v
vs) = (Map SomeVar SymbolicInfo
e', (Var v, Int)
-> ValueSet v -> Map SomeVar SymbolicInfo -> Constraint 'Input
forall v.
Typeable v =>
(Var v, Int)
-> ValueSet v -> Map SomeVar SymbolicInfo -> Constraint 'Input
InputConstraint (Var v
x,SomeVar -> Map SomeVar SymbolicInfo -> Int
ix (Var v -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var v
x) Map SomeVar SymbolicInfo
e') ValueSet v
vs Map SomeVar SymbolicInfo
e')
  where
    e' :: Map SomeVar SymbolicInfo
e' = StorageType
-> SomeVar
-> Int
-> Map SomeVar SymbolicInfo
-> Map SomeVar SymbolicInfo
inc StorageType
ty (Var v -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var v
x) Int
k Map SomeVar SymbolicInfo
e
addEnvToConstraint Map SomeVar SymbolicInfo
e Int
_ (SimpleCondition Term 'Transparent Bool
c) = (Map SomeVar SymbolicInfo
e, Term 'Transparent Bool
-> Map SomeVar SymbolicInfo -> Constraint 'Condition
ConditionConstraint Term 'Transparent Bool
c Map SomeVar SymbolicInfo
e)
addEnvToConstraint Map SomeVar SymbolicInfo
e Int
_ (SimpleOverflow [Term 'Transparent Integer]
ts) = (Map SomeVar SymbolicInfo
e, [Term 'Transparent Integer]
-> Map SomeVar SymbolicInfo -> Constraint 'Overflow
OverflowConstraints [Term 'Transparent Integer]
ts Map SomeVar SymbolicInfo
e)

data SymbolicInfo = SymbolicInfo
  { SymbolicInfo -> Int
currentIndex :: Int
  , SymbolicInfo -> [Int]
negativeIndices :: [Int]
  , SymbolicInfo -> [Int]
chronology :: [Int]
  }

ix :: SomeVar -> Map SomeVar SymbolicInfo -> Int
ix :: SomeVar -> Map SomeVar SymbolicInfo -> Int
ix SomeVar
x Map SomeVar SymbolicInfo
m = Int -> (SymbolicInfo -> Int) -> Maybe SymbolicInfo -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 SymbolicInfo -> Int
currentIndex (SomeVar -> Map SomeVar SymbolicInfo -> Maybe SymbolicInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeVar
x Map SomeVar SymbolicInfo
m)

inc :: StorageType -> SomeVar -> Int -> Map SomeVar SymbolicInfo -> Map SomeVar SymbolicInfo
inc :: StorageType
-> SomeVar
-> Int
-> Map SomeVar SymbolicInfo
-> Map SomeVar SymbolicInfo
inc StorageType
ty SomeVar
x Int
k Map SomeVar SymbolicInfo
m
  | SomeVar
x SomeVar -> [SomeVar] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map SomeVar SymbolicInfo -> [SomeVar]
forall k a. Map k a -> [k]
Map.keys Map SomeVar SymbolicInfo
m = (SymbolicInfo -> Maybe SymbolicInfo)
-> SomeVar -> Map SomeVar SymbolicInfo -> Map SomeVar SymbolicInfo
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (\(SymbolicInfo Int
c [Int]
ns [Int]
ks) -> SymbolicInfo -> Maybe SymbolicInfo
forall a. a -> Maybe a
Just (Int -> [Int] -> [Int] -> SymbolicInfo
SymbolicInfo (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> [Int] -> [Int]
updateNegs (Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [Int]
ns) (Int
kInt -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[Int]
ks))) SomeVar
x Map SomeVar SymbolicInfo
m
  | Bool
otherwise = SomeVar
-> SymbolicInfo
-> Map SomeVar SymbolicInfo
-> Map SomeVar SymbolicInfo
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SomeVar
x (Int -> [Int] -> [Int] -> SymbolicInfo
SymbolicInfo Int
1 (Int -> [Int] -> [Int]
updateNegs Int
1 []) [Int
k]) Map SomeVar SymbolicInfo
m
  where
    updateNegs :: Int -> [Int] -> [Int]
updateNegs Int
c = case StorageType
ty of
      StorageType
KeepInput -> [Int] -> [Int]
forall a. a -> a
id
      StorageType
DropInput -> (Int
c:)

-- indices of symbolic values stored and their chronological position
storedValues :: SymbolicInfo -> [(Int,Int)]
storedValues :: SymbolicInfo -> [(Int, Int)]
storedValues SymbolicInfo{Int
[Int]
currentIndex :: SymbolicInfo -> Int
negativeIndices :: SymbolicInfo -> [Int]
chronology :: SymbolicInfo -> [Int]
currentIndex :: Int
negativeIndices :: [Int]
chronology :: [Int]
..} = ((Int, Int) -> Bool) -> [(Int, Int)] -> [(Int, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int]
negativeIndices)(Int -> Bool) -> ((Int, Int) -> Int) -> (Int, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int, Int) -> Int
forall a b. (a, b) -> a
fst) ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
currentIndex,Int
currentIndexInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1..Int
1] [Int]
chronology

pathDepth :: Path -> Int
pathDepth :: Path -> Int
pathDepth =  [Constraint 'Input] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Constraint 'Input] -> Int)
-> (Path -> [Constraint 'Input]) -> Path -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Constraint 'Input], [Constraint 'Condition],
 [Constraint 'Overflow])
-> [Constraint 'Input]
forall a b c. (a, b, c) -> a
fst3 (([Constraint 'Input], [Constraint 'Condition],
  [Constraint 'Overflow])
 -> [Constraint 'Input])
-> (Path
    -> ([Constraint 'Input], [Constraint 'Condition],
        [Constraint 'Overflow]))
-> Path
-> [Constraint 'Input]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Path
-> ([Constraint 'Input], [Constraint 'Condition],
    [Constraint 'Overflow])
partitionPath

partitionPath :: Path -> ([Constraint 'Input],[Constraint 'Condition],[Constraint 'Overflow])
partitionPath :: Path
-> ([Constraint 'Input], [Constraint 'Condition],
    [Constraint 'Overflow])
partitionPath = (Some Constraint
 -> ([Constraint 'Input], [Constraint 'Condition],
     [Constraint 'Overflow]))
-> Path
-> ([Constraint 'Input], [Constraint 'Condition],
    [Constraint 'Overflow])
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Some Constraint
-> ([Constraint 'Input], [Constraint 'Condition],
    [Constraint 'Overflow])
phi where
  phi :: Some Constraint -> ([Constraint 'Input],[Constraint 'Condition],[Constraint 'Overflow])
  phi :: Some Constraint
-> ([Constraint 'Input], [Constraint 'Condition],
    [Constraint 'Overflow])
phi (Some c :: Constraint a
c@InputConstraint{}) = ([Constraint a
Constraint 'Input
c],[Constraint 'Condition]
forall a. Monoid a => a
mempty,[Constraint 'Overflow]
forall a. Monoid a => a
mempty)
  phi (Some c :: Constraint a
c@ConditionConstraint{}) = ([Constraint 'Input]
forall a. Monoid a => a
mempty,[Constraint a
Constraint 'Condition
c],[Constraint 'Overflow]
forall a. Monoid a => a
mempty)
  phi (Some c :: Constraint a
c@OverflowConstraints{}) = ([Constraint 'Input]
forall a. Monoid a => a
mempty,[Constraint 'Condition]
forall a. Monoid a => a
mempty,[Constraint a
Constraint 'Overflow
c])


showSimplePath :: SimplePath -> String
showSimplePath :: SimplePath -> String
showSimplePath (ClosedPath [Some SimpleConstraint]
cs) = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
" |" ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Some SimpleConstraint -> String)
-> [Some SimpleConstraint] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Some SimpleConstraint -> String
showSomeSimpleConstraint [Some SimpleConstraint]
cs
showSimplePath (OpenPath [Some SimpleConstraint]
cs SimpleConstraint t
c SimplePath
p) =
  ([String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
" |" ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Some SimpleConstraint -> String)
-> [Some SimpleConstraint] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Some SimpleConstraint -> String
showSomeSimpleConstraint [Some SimpleConstraint]
cs)
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if [Some SimpleConstraint] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Some SimpleConstraint]
cs then String
"" else String
" |\n") String -> ShowS
forall a. [a] -> [a] -> [a]
++ SimpleConstraint t -> String
forall (t :: ConstraintType). SimpleConstraint t -> String
showSimpleConstraint SimpleConstraint t
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n |\n"
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ SimplePath -> String
showSimplePath SimplePath
p

showSomeSimpleConstraint :: Some SimpleConstraint -> String
showSomeSimpleConstraint :: Some SimpleConstraint -> String
showSomeSimpleConstraint (Some SimpleConstraint a
c) = SimpleConstraint a -> String
forall (t :: ConstraintType). SimpleConstraint t -> String
showSimpleConstraint SimpleConstraint a
c

showSimpleConstraint :: SimpleConstraint t -> String
showSimpleConstraint :: forall (t :: ConstraintType). SimpleConstraint t -> String
showSimpleConstraint (SimpleInput StorageType
KeepInput Var v
x ValueSet v
vs) = [String] -> String
unwords [Var v -> String
forall a. Var a -> String
varname Var v
x,String
":",ValueSet v -> String
forall a. Typeable a => ValueSet a -> String
showValueSet ValueSet v
vs, String
"(kept)"]
showSimpleConstraint (SimpleInput StorageType
DropInput Var v
x ValueSet v
vs) = [String] -> String
unwords [Var v -> String
forall a. Var a -> String
varname Var v
x,String
":",ValueSet v -> String
forall a. Typeable a => ValueSet a -> String
showValueSet ValueSet v
vs, String
"(dropped)"]
showSimpleConstraint (SimpleCondition Term 'Transparent Bool
c) = Term 'Transparent Bool -> String
forall a (k :: TermKind). Typeable a => Term k a -> String
showTerm Term 'Transparent Bool
c
showSimpleConstraint (SimpleOverflow [Term 'Transparent Integer]
_) = String
"**some overflow checks**"

showPath :: Path -> String
showPath :: Path -> String
showPath = [String] -> String
unlines ([String] -> String) -> (Path -> [String]) -> Path -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
" |" ([String] -> [String]) -> (Path -> [String]) -> Path -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Some Constraint -> String) -> Path -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Some Constraint -> String
showSomeConstraint

showSomeConstraint :: Some Constraint -> String
showSomeConstraint :: Some Constraint -> String
showSomeConstraint (Some Constraint a
c) = Constraint a -> String
forall (t :: ConstraintType). Constraint t -> String
showConstraint Constraint a
c

showConstraint :: Constraint t -> String
showConstraint :: forall (t :: ConstraintType). Constraint t -> String
showConstraint (InputConstraint (Var v
x,Int
i) ValueSet v
vs Map SomeVar SymbolicInfo
_) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Var v -> String
forall a. Var a -> String
varname Var v
x,String
"_",Int -> String
forall a. Show a => a -> String
show Int
i,String
" : ",ValueSet v -> String
forall a. Typeable a => ValueSet a -> String
showValueSet ValueSet v
vs]
showConstraint (ConditionConstraint Term 'Transparent Bool
t Map SomeVar SymbolicInfo
_) = Term 'Transparent Bool -> String
forall a (k :: TermKind). Typeable a => Term k a -> String
showTerm Term 'Transparent Bool
t
showConstraint (OverflowConstraints [Term 'Transparent Integer]
_ Map SomeVar SymbolicInfo
_) = String
"**some overflow checks**"

numberOfPaths :: Integer -> Specification -> Integer
numberOfPaths :: Integer -> Specification -> Integer
numberOfPaths Integer
maxIterationDepth Specification
s =
  case Specification -> Integer -> (Integer, Integer)
go Specification
s Integer
maxIterationDepth of
    (Integer
i,Integer
0) -> Integer
i
    (Integer, Integer)
_ -> String -> Integer
forall a. HasCallStack => String -> a
error String
"numberOfPaths: unbound top-level exit marker"
  where
  go :: Specification -> Integer -> (Integer, Integer)
  go :: Specification -> Integer -> (Integer, Integer)
go (ReadInput Var a
_ ValueSet a
_  InputMode
_ Specification
s') Integer
n = Specification -> Integer -> (Integer, Integer)
go Specification
s' Integer
n
  go (WriteOutput OptFlag
_ Set (OutputPattern k)
_ Specification
s') Integer
n = Specification -> Integer -> (Integer, Integer)
go Specification
s' Integer
n
  go (Branch Term 'Transparent Bool
_ Specification
t Specification
e Specification
s') Integer
n =
    let
      (Integer
it,Integer
kt) = Specification -> Integer -> (Integer, Integer)
go Specification
t Integer
n
      (Integer
ie,Integer
ke) = Specification -> Integer -> (Integer, Integer)
go Specification
e Integer
n
      (Integer
i,Integer
k) = Specification -> Integer -> (Integer, Integer)
go Specification
s' Integer
n
    in ((Integer
itInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
ie)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
i,Integer
ktInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
keInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
k)
  go (TillE Specification
bdy Specification
s') Integer
n
    | Specification -> Bool
hasIteration Specification
bdy = String -> (Integer, Integer)
forall a. HasCallStack => String -> a
error String
"numberOfPaths: can't compute number of paths for nested iterations, yet"
    | Specification -> Bool
hasIteration Specification
s' =
      let
        rs :: [(Integer, Integer)]
rs = do
          (Integer
n1,Integer
n2) <- [ (Integer
n1,Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
n1) | Integer
n1 <- [Integer
0..Integer
n] ]
          let
            (Integer
ib, Integer
kb) = Specification -> Integer -> (Integer, Integer)
go Specification
bdy Integer
n1
            (Integer
i,Integer
k) = Specification -> Integer -> (Integer, Integer)
go Specification
s' Integer
n2
          (Integer, Integer) -> [(Integer, Integer)]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> Integer -> Integer
p' Integer
ib Integer
kb Integer
n1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
i,Integer
k)
      in ((Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> (Integer, Integer) -> [(Integer, Integer)] -> (Integer, Integer)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Integer
i,Integer
k) (Integer
si,Integer
sk) -> (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
si,Integer
kInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
sk)) (Integer
0,Integer
0) [(Integer, Integer)]
rs
    | Bool
otherwise =
      let
        (Integer
ib,Integer
kb) = Specification -> Integer -> (Integer, Integer)
go Specification
bdy Integer
n
        (Integer
i,Integer
k) = Specification -> Integer -> (Integer, Integer)
go Specification
s' Integer
n
      in (Integer -> Integer -> Integer -> Integer
p Integer
ib Integer
kb Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
i,Integer
k)
  go Specification
Nop Integer
_ = (Integer
1,Integer
0)
  go Specification
E Integer
_ = (Integer
0,Integer
1)
  -- path with length (<=n) in an iteration with i paths to Nop and k paths to E under the iteration
  p :: Integer -> Integer -> Integer -> Integer
  p :: Integer -> Integer -> Integer -> Integer
p Integer
0 Integer
k Integer
_ = Integer
k
  p Integer
1 Integer
k Integer
n = Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
  p Integer
i Integer
k Integer
n = Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (Integer
i Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
  -- path with length (=n) in an iteration with i paths to Nop and k paths to E under the iteration
  p' :: Integer -> Integer -> Integer -> Integer
  p' :: Integer -> Integer -> Integer -> Integer
p' Integer
i Integer
k Integer
n = Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
i Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
n