module Language.LTL
(
N, B, R, F, E
, Directive (..)
, checkVCD
) where
import Data.VCD
data N
data B
data R
data F
class BF a
instance BF B
instance BF F
class BR a
instance BR B
instance BR R
class NB a
instance NB N
instance NB B
data E a where
Var :: NB a => [String] -> E a
Add :: E N -> E N -> E N
Sub :: E N -> E N -> E N
Mul :: E N -> E N -> E N
Eq :: NB a => E a -> E a -> E B
Lt :: E N -> E N -> E B
Sequence :: (BR a, BR b) => E a -> E b -> E R
Infusion :: (BR a, BR b) => E a -> E b -> E R
Not :: BF a => E a -> E a
And :: E a -> E a -> E a
Or :: E a -> E a -> E a
Empty :: E R
Many :: BR a => E a -> E R
Formula' :: BR a => E a -> E F
Formula :: BR a => E a -> E F
Next' :: E F -> E F
Until' :: E F -> E F -> E F
Imply :: E R -> E F
data Directive
= Assert String (E F)
| Assume String (E F)
| Cover String (E R)
checkVCD :: String -> Int -> [Directive] -> [(Directive, Maybe Int)]
checkVCD vcd period formulas = []
where
VCD _ defs samples = parseVCD vcd