UniqueLogic.ST.TF.Example.Verify

Warning: This module is intended for documentation purposes. Do not import it!

Documentation

data Assign

Constructors

Assign Name (TrackedNumber Rational)

Instances

Show Assign

Methods

showsPrec :: Int -> Assign -> ShowS

show :: Assign -> String

showList :: [Assign] -> ShowS

type Assigns = [Assign]

data TrackedNumber a

Constructors

TrackedNumber T a

Instances

Functor TrackedNumber

Methods

fmap :: (a -> b) -> TrackedNumber a -> TrackedNumber b

(<$) :: a -> TrackedNumber b -> TrackedNumber a

Fractional a => Fractional (TrackedNumber a)

Methods

(/) :: TrackedNumber a -> TrackedNumber a -> TrackedNumber a

recip :: TrackedNumber a -> TrackedNumber a

fromRational :: Rational -> TrackedNumber a

Num a => Num (TrackedNumber a)

Methods

(+) :: TrackedNumber a -> TrackedNumber a -> TrackedNumber a

(-) :: TrackedNumber a -> TrackedNumber a -> TrackedNumber a

(*) :: TrackedNumber a -> TrackedNumber a -> TrackedNumber a

negate :: TrackedNumber a -> TrackedNumber a

abs :: TrackedNumber a -> TrackedNumber a

signum :: TrackedNumber a -> TrackedNumber a

fromInteger :: Integer -> TrackedNumber a

Show a => Show (TrackedNumber a)

Methods

showsPrec :: Int -> TrackedNumber a -> ShowS

show :: TrackedNumber a -> String

showList :: [TrackedNumber a] -> ShowS

C a => C (TrackedNumber a)

Methods

multiply :: TrackedNumber a -> Maybe (TrackedNumber a)

divide :: TrackedNumber a -> TrackedNumber a -> Maybe (TrackedNumber a)

Real a => ToTrackedNumber (TrackedNumber a)

Methods

toTrackedNumber :: TrackedNumber a -> TrackedNumber Rational

tn1 :: (T -> T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b

tn2 :: (T -> T -> T) -> (a -> b -> c) -> TrackedNumber a -> TrackedNumber b -> TrackedNumber c

class ToTrackedNumber a where

Minimal complete definition

toTrackedNumber

Methods

toTrackedNumber :: a -> TrackedNumber Rational

Instances

Real a => ToTrackedNumber (TrackedNumber a)

Methods

toTrackedNumber :: TrackedNumber a -> TrackedNumber Rational

newtype Track m a

Constructors

Track

Fields

• runTrack :: ExceptT Exception (WriterT Assigns m) a

Instances

MonadTrans Track

Methods

lift :: Monad m => m a -> Track m a

C Track

Methods

point :: Monad m => a -> Track m a

bind :: Monad m => Track m a -> (a -> Track m b) -> Track m b

C Track

Methods

update :: (Value Track a, C s) => Updater Track s a

ToTrackedNumber tn => Value Track tn

Associated Types

data ValueConstraint (Track :: (* -> *) -> * -> *) tn :: *

Methods

valueConstraint :: T s (Updates Track s) -> T s (Maybe tn) -> ValueConstraint Track tn

Monad m => Monad (Track m)

Methods

(>>=) :: Track m a -> (a -> Track m b) -> Track m b

(>>) :: Track m a -> Track m b -> Track m b

return :: a -> Track m a

fail :: String -> Track m a

Monad m => Functor (Track m)

Methods

fmap :: (a -> b) -> Track m a -> Track m b

(<$) :: a -> Track m b -> Track m a

Monad m => Applicative (Track m)

Methods

pure :: a -> Track m a

(<*>) :: Track m (a -> b) -> Track m a -> Track m b

liftA2 :: (a -> b -> c) -> Track m a -> Track m b -> Track m c

(*>) :: Track m a -> Track m b -> Track m b

(<*) :: Track m a -> Track m b -> Track m a

data ValueConstraint Track

data ValueConstraint Track where

• VerifyConstraint :: ValueConstraint Track tn

data Exception

Constructors

Exception (Maybe Name) (TrackedNumber Rational) (TrackedNumber Rational)

Instances

Show Exception

Methods

showsPrec :: Int -> Exception -> ShowS

show :: Exception -> String

showList :: [Exception] -> ShowS

type Variable s = Variable Track s (TrackedNumber Rational)

globalVariable :: C s => Name -> s (Variable s)

match :: Eq a => TrackedNumber a -> TrackedNumber a -> Bool

inconsistency :: Monad m => Maybe Name -> TrackedNumber Rational -> TrackedNumber Rational -> Wrap Track m ()

logUpdate :: (Real a, C s) => Name -> MaybeT s (TrackedNumber a) -> MaybeT (Wrap Track s) (TrackedNumber a)

example :: (Either Exception (Maybe (TrackedNumber Rational), Maybe (TrackedNumber Rational)), Assigns)