module UniqueLogic.ST.Example.Verify {-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-} where import qualified UniqueLogic.ST.Example.Term as Term import qualified UniqueLogic.ST.Expression as Expr import qualified UniqueLogic.ST.System as Sys import qualified UniqueLogic.ST.Duplicate as Duplicate import qualified UniqueLogic.ST.MonadTrans as UMT import UniqueLogic.ST.Expression ((=:=)) import qualified Control.Monad.Exception.Synchronous as ME import qualified Control.Monad.Trans.Writer as MW import qualified Control.Monad.Trans.Class as MT import Control.Monad.Trans.Writer (writer, ) import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT, ) import Control.Monad.ST (ST, runST, ) import Control.Monad (liftM, liftM2, ap, ) import Control.Applicative (Applicative, pure, (<*>), ) import qualified Prelude as P import Prelude hiding (max, log) data Assign = Assign Term.Name Term.T deriving (Int -> Assign -> ShowS [Assign] -> ShowS Assign -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Assign] -> ShowS $cshowList :: [Assign] -> ShowS show :: Assign -> String $cshow :: Assign -> String showsPrec :: Int -> Assign -> ShowS $cshowsPrec :: Int -> Assign -> ShowS Show) type Assigns = [Assign] data TrackedNumber a = TrackedNumber Term.T a deriving (Int -> TrackedNumber a -> ShowS forall a. Show a => Int -> TrackedNumber a -> ShowS forall a. Show a => [TrackedNumber a] -> ShowS forall a. Show a => TrackedNumber a -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [TrackedNumber a] -> ShowS $cshowList :: forall a. Show a => [TrackedNumber a] -> ShowS show :: TrackedNumber a -> String $cshow :: forall a. Show a => TrackedNumber a -> String showsPrec :: Int -> TrackedNumber a -> ShowS $cshowsPrec :: forall a. Show a => Int -> TrackedNumber a -> ShowS Show) tn1 :: (Term.T -> Term.T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b tn1 :: forall a b. (T -> T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b tn1 T -> T f a -> b g (TrackedNumber T xt a xn) = forall a. T -> a -> TrackedNumber a TrackedNumber (T -> T f T xt) (a -> b g a xn) tn2 :: (Term.T -> Term.T -> Term.T) -> (a -> b -> c) -> TrackedNumber a -> TrackedNumber b -> TrackedNumber c tn2 :: forall a b c. (T -> T -> T) -> (a -> b -> c) -> TrackedNumber a -> TrackedNumber b -> TrackedNumber c tn2 T -> T -> T f a -> b -> c g (TrackedNumber T xt a xn) (TrackedNumber T yt b yn) = forall a. T -> a -> TrackedNumber a TrackedNumber (T -> T -> T f T xt T yt) (a -> b -> c g a xn b yn) instance Num a => Num (TrackedNumber a) where fromInteger :: Integer -> TrackedNumber a fromInteger Integer n = forall a. T -> a -> TrackedNumber a TrackedNumber (forall a. Num a => Integer -> a fromInteger Integer n) (forall a. Num a => Integer -> a fromInteger Integer n) + :: TrackedNumber a -> TrackedNumber a -> TrackedNumber a (+) = forall a b c. (T -> T -> T) -> (a -> b -> c) -> TrackedNumber a -> TrackedNumber b -> TrackedNumber c tn2 forall a. Num a => a -> a -> a (+) forall a. Num a => a -> a -> a (+) (-) = forall a b c. (T -> T -> T) -> (a -> b -> c) -> TrackedNumber a -> TrackedNumber b -> TrackedNumber c tn2 (-) (-) * :: TrackedNumber a -> TrackedNumber a -> TrackedNumber a (*) = forall a b c. (T -> T -> T) -> (a -> b -> c) -> TrackedNumber a -> TrackedNumber b -> TrackedNumber c tn2 forall a. Num a => a -> a -> a (*) forall a. Num a => a -> a -> a (*) abs :: TrackedNumber a -> TrackedNumber a abs = forall a b. (T -> T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b tn1 forall a. Num a => a -> a abs forall a. Num a => a -> a abs signum :: TrackedNumber a -> TrackedNumber a signum = forall a b. (T -> T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b tn1 forall a. Num a => a -> a signum forall a. Num a => a -> a signum instance Fractional a => Fractional (TrackedNumber a) where fromRational :: Rational -> TrackedNumber a fromRational Rational n = forall a. T -> a -> TrackedNumber a TrackedNumber (forall a. Fractional a => Rational -> a fromRational Rational n) (forall a. Fractional a => Rational -> a fromRational Rational n) / :: TrackedNumber a -> TrackedNumber a -> TrackedNumber a (/) = forall a b c. (T -> T -> T) -> (a -> b -> c) -> TrackedNumber a -> TrackedNumber b -> TrackedNumber c tn2 forall a. Fractional a => a -> a -> a (/) forall a. Fractional a => a -> a -> a (/) instance Eq a => Duplicate.C (TrackedNumber a) where accept :: TrackedNumber a -> TrackedNumber a -> Bool accept (TrackedNumber T _ a x) (TrackedNumber T _ a y) = a xforall a. Eq a => a -> a -> Bool ==a y instance (Monad m) => Functor (Track m) where fmap :: forall a b. (a -> b) -> Track m a -> Track m b fmap = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r liftM instance (Monad m) => Applicative (Track m) where pure :: forall a. a -> Track m a pure = forall (m :: * -> *) a. ExceptionalT Exception (WriterT [Assign] m) a -> Track m a Track forall b c a. (b -> c) -> (a -> b) -> a -> c . forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (C t, Monad m) => a -> t m a UMT.point <*> :: forall a b. Track m (a -> b) -> Track m a -> Track m b (<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b ap instance (Monad m) => Monad (Track m) where return :: forall a. a -> Track m a return = forall (f :: * -> *) a. Applicative f => a -> f a pure Track m a x >>= :: forall a b. Track m a -> (a -> Track m b) -> Track m b >>= a -> Track m b k = forall (m :: * -> *) a. ExceptionalT Exception (WriterT [Assign] m) a -> Track m a Track forall a b. (a -> b) -> a -> b $ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b. (C t, Monad m) => t m a -> (a -> t m b) -> t m b UMT.bind (forall (m :: * -> *) a. Track m a -> ExceptionalT Exception (WriterT [Assign] m) a runTrack Track m a x) (forall (m :: * -> *) a. Track m a -> ExceptionalT Exception (WriterT [Assign] m) a runTrack forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> Track m b k) instance MT.MonadTrans Track where lift :: forall (m :: * -> *) a. Monad m => m a -> Track m a lift = forall (m :: * -> *) a. ExceptionalT Exception (WriterT [Assign] m) a -> Track m a Track forall b c a. (b -> c) -> (a -> b) -> a -> c . forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a MT.lift forall b c a. (b -> c) -> (a -> b) -> a -> c . forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a MT.lift instance UMT.C Track where point :: forall (m :: * -> *) a. Monad m => a -> Track m a point = forall (m :: * -> *) a. Monad m => a -> m a return bind :: forall (m :: * -> *) a b. Monad m => Track m a -> (a -> Track m b) -> Track m b bind = forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b (>>=) instance Sys.C Track where doUpdate :: forall a s. C a => Updater Track s a doUpdate = forall (w :: (* -> *) -> * -> *) a s. (C w, C a) => (a -> a -> Wrap w (ST s) ()) -> Updater w s a Sys.updateAndCheck forall a b. (a -> b) -> a -> b $ \a _ a _ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. t m a -> Wrap t m a UMT.wrap forall a b. (a -> b) -> a -> b $ forall (m :: * -> *) a. ExceptionalT Exception (WriterT [Assign] m) a -> Track m a Track forall a b. (a -> b) -> a -> b $ forall (m :: * -> *) e a. Monad m => e -> ExceptionalT e m a ME.throwT Exception AnonymousException newtype Track m a = Track {forall (m :: * -> *) a. Track m a -> ExceptionalT Exception (WriterT [Assign] m) a runTrack :: ME.ExceptionalT Exception (MW.WriterT Assigns m) a} data Exception = Exception Term.Name (TrackedNumber Rational) (TrackedNumber Rational) | AnonymousException deriving (Int -> Exception -> ShowS [Exception] -> ShowS Exception -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Exception] -> ShowS $cshowList :: [Exception] -> ShowS show :: Exception -> String $cshow :: Exception -> String showsPrec :: Int -> Exception -> ShowS $cshowsPrec :: Int -> Exception -> ShowS Show) type Variable s = Sys.Variable Track s (TrackedNumber Rational) globalVariable :: Term.Name -> ST s (Variable s) globalVariable :: forall s. String -> ST s (Variable s) globalVariable String name = forall (w :: (* -> *) -> * -> *) a s. (C w, C a) => SimpleUpdater w s a -> ST s (Variable w s a) Sys.globalVariable (\STRef s [Update Track s] al STRef s (Maybe (TrackedNumber Rational)) av -> forall (w :: (* -> *) -> * -> *) a s. (C w, C a) => (a -> a -> Wrap w (ST s) ()) -> Updater w s a Sys.updateAndCheck (forall (m :: * -> *). Monad m => String -> TrackedNumber Rational -> TrackedNumber Rational -> Wrap Track m () inconsistency String name) STRef s [Update Track s] al STRef s (Maybe (TrackedNumber Rational)) av forall b c a. (b -> c) -> (a -> b) -> a -> c . forall s a. String -> MaybeT (ST s) (TrackedNumber a) -> MaybeT (Wrap Track (ST s)) (TrackedNumber a) update String name) inconsistency :: Monad m => Term.Name -> TrackedNumber Rational -> TrackedNumber Rational -> UMT.Wrap Track m () inconsistency :: forall (m :: * -> *). Monad m => String -> TrackedNumber Rational -> TrackedNumber Rational -> Wrap Track m () inconsistency String name TrackedNumber Rational old TrackedNumber Rational new = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. t m a -> Wrap t m a UMT.wrap forall a b. (a -> b) -> a -> b $ forall (m :: * -> *) a. ExceptionalT Exception (WriterT [Assign] m) a -> Track m a Track forall a b. (a -> b) -> a -> b $ forall (m :: * -> *) e a. Monad m => e -> ExceptionalT e m a ME.throwT forall a b. (a -> b) -> a -> b $ String -> TrackedNumber Rational -> TrackedNumber Rational -> Exception Exception String name TrackedNumber Rational old TrackedNumber Rational new update :: Term.Name -> MaybeT (ST s) (TrackedNumber a) -> MaybeT (UMT.Wrap Track (ST s)) (TrackedNumber a) update :: forall s a. String -> MaybeT (ST s) (TrackedNumber a) -> MaybeT (Wrap Track (ST s)) (TrackedNumber a) update String name MaybeT (ST s) (TrackedNumber a) act = do (TrackedNumber T t a x) <- forall (m :: * -> *) a (n :: * -> *) b. (m (Maybe a) -> n (Maybe b)) -> MaybeT m a -> MaybeT n b mapMaybeT forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (C t, Monad m) => m a -> Wrap t m a UMT.lift MaybeT (ST s) (TrackedNumber a) act forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a MT.lift forall a b. (a -> b) -> a -> b $ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. t m a -> Wrap t m a UMT.wrap forall a b. (a -> b) -> a -> b $ forall (m :: * -> *) a. ExceptionalT Exception (WriterT [Assign] m) a -> Track m a Track forall a b. (a -> b) -> a -> b $ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a MT.lift forall a b. (a -> b) -> a -> b $ forall (m :: * -> *) a w. Monad m => (a, w) -> WriterT w m a writer (forall a. T -> a -> TrackedNumber a TrackedNumber (String -> T Term.Var String name) a x, [String -> T -> Assign Assign String name T t]) example :: (ME.Exceptional Exception (Maybe (TrackedNumber Rational), Maybe (TrackedNumber Rational)), Assigns) example :: (Exceptional Exception (Maybe (TrackedNumber Rational), Maybe (TrackedNumber Rational)), [Assign]) example = forall a. (forall s. ST s a) -> a runST (do Variable s xv <- forall s. String -> ST s (Variable s) globalVariable String "x" Variable s yv <- forall s. String -> ST s (Variable s) globalVariable String "y" forall w (m :: * -> *) a. WriterT w m a -> m (a, w) MW.runWriterT forall a b. (a -> b) -> a -> b $ forall e (m :: * -> *) a. ExceptionalT e m a -> m (Exceptional e a) ME.runExceptionalT forall a b. (a -> b) -> a -> b $ forall (m :: * -> *) a. Track m a -> ExceptionalT Exception (WriterT [Assign] m) a runTrack forall a b. (a -> b) -> a -> b $ do forall (w :: (* -> *) -> * -> *) s a. C w => T w s a -> w (ST s) a Sys.solve forall a b. (a -> b) -> a -> b $ do let x :: T Track s (TrackedNumber Rational) x = forall (w :: (* -> *) -> * -> *) s a. Variable w s a -> T w s a Expr.fromVariable Variable s xv y :: T Track s (TrackedNumber Rational) y = forall (w :: (* -> *) -> * -> *) s a. Variable w s a -> T w s a Expr.fromVariable Variable s yv T Track s (TrackedNumber Rational) xforall a. Num a => a -> a -> a *T Track s (TrackedNumber Rational) 3 forall (w :: (* -> *) -> * -> *) s a. C w => T w s a -> T w s a -> T w s () =:= T Track s (TrackedNumber Rational) yforall a. Fractional a => a -> a -> a /T Track s (TrackedNumber Rational) 2 T Track s (TrackedNumber Rational) 5 forall (w :: (* -> *) -> * -> *) s a. C w => T w s a -> T w s a -> T w s () =:= T Track s (TrackedNumber Rational) 2forall a. Num a => a -> a -> a +T Track s (TrackedNumber Rational) x forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a MT.lift forall a b. (a -> b) -> a -> b $ forall (m :: * -> *) a1 a2 r. Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r liftM2 (,) (forall (w :: (* -> *) -> * -> *) s a. Variable w s a -> ST s (Maybe a) Sys.query Variable s xv) (forall (w :: (* -> *) -> * -> *) s a. Variable w s a -> ST s (Maybe a) Sys.query Variable s yv))