packages feed

unique-logic-tf (empty) → 0.4

raw patch · 15 files changed

+1261/−0 lines, 15 filesdep +QuickCheckdep +basedep +containerssetup-changed

Dependencies added: QuickCheck, base, containers, explicit-exception, non-empty, transformers, unique-logic-tf, utility-ht

Files

+ LICENSE view
@@ -0,0 +1,31 @@+Copyright (c) 2013, Henning Thielemann++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * The names of contributors may not be used to endorse or promote+      products derived from this software without specific prior+      written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.lhs view
@@ -0,0 +1,3 @@+#! /usr/bin/env runhaskell+> import Distribution.Simple+> main = defaultMain
+ src/UniqueLogic/ST/TF/Example/Expression.hs view
@@ -0,0 +1,26 @@+module UniqueLogic.ST.TF.Example.Expression+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}+ where++import qualified UniqueLogic.ST.TF.Expression as Expr+import qualified UniqueLogic.ST.TF.System.Simple as Sys+import UniqueLogic.ST.TF.Expression ((=:=))++import Control.Monad.ST (runST, )+import Control.Monad (liftM2, )+++example :: (Maybe Double, Maybe Double)+example =+   runST (do+      xv <- Sys.globalVariable+      yv <- Sys.globalVariable+      Sys.solve $ do+         let x = Expr.fromVariable xv+             y = Expr.fromVariable yv+         x*3 =:= y/2+         5 =:= 2+x+      liftM2+         (,)+         (Sys.query xv)+         (Sys.query yv))
+ src/UniqueLogic/ST/TF/Example/Label.hs view
@@ -0,0 +1,79 @@+module UniqueLogic.ST.TF.Example.Label+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}+ where++import qualified UniqueLogic.ST.TF.Example.Term as Term+import qualified UniqueLogic.ST.TF.Expression as Expr+import qualified UniqueLogic.ST.TF.Rule as Rule+import qualified UniqueLogic.ST.TF.System.Label as Sys+import UniqueLogic.ST.TF.Expression ((=:=))++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.ST (ST, runST, )+import Control.Monad (liftM2, liftM3, )++import qualified Prelude as P+import Prelude hiding (max, log)++++data Assign = Assign Term.Name Term.T+   deriving (Show)++type Assigns = [Assign]++type Variable s = Sys.Variable Assigns s Term.T++globalVariable :: Term.Name -> ST s (Variable s)+globalVariable name =+   Sys.globalVariable $+      \x -> writer (Term.Var name, [Assign name x])++constant :: Rational -> Sys.T Assigns s (Variable s)+constant = Sys.constant . fromRational+++{- |+> x=1+> y=2+> z=3++> x+y=3+> y*z=6+> z=3+-}+rule :: ((Maybe Term.T, Maybe Term.T, Maybe Term.T), Assigns)+rule =+   runST (do+      x <- globalVariable "x"+      y <- globalVariable "y"+      z <- globalVariable "z"+      MW.runWriterT $ do+         Sys.solve $ do+            c3 <- constant 3+            c6 <- constant 6+            Rule.add x y c3+            Rule.mul y z c6+            Rule.equ z c3+         MT.lift $ liftM3+            (,,)+            (Sys.query x)+            (Sys.query y)+            (Sys.query z))++expression :: ((Maybe Term.T, Maybe Term.T), Assigns)+expression =+   runST (do+      xv <- globalVariable "x"+      yv <- globalVariable "y"+      MW.runWriterT $ do+         Sys.solve $ do+            let x = Expr.fromVariable xv+                y = Expr.fromVariable yv+            x*3 =:= y/2+            5 =:= 2+x+         MT.lift $ liftM2 (,)+            (Sys.query xv)+            (Sys.query yv))
+ src/UniqueLogic/ST/TF/Example/Rule.hs view
@@ -0,0 +1,46 @@+module UniqueLogic.ST.TF.Example.Rule+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}+ where++import qualified UniqueLogic.ST.TF.Rule as Rule+import qualified UniqueLogic.ST.TF.System.Simple as Sys++import Control.Monad.ST (runST, )+import Control.Monad (liftM4, )++import qualified Prelude as P+import Prelude hiding (max)+++{- |+> x=1+> y=2+> z=3+> w=3++> x+y=3+> y*z=6+> z=3+> y^w=8+-}+example :: (Maybe Double, Maybe Double, Maybe Double, Maybe Double)+example =+   runST (do+      x <- Sys.globalVariable+      y <- Sys.globalVariable+      z <- Sys.globalVariable+      w <- Sys.globalVariable+      Sys.solve $ do+         c3 <- Sys.constant 3+         c6 <- Sys.constant 6+         c8 <- Sys.constant 8+         Rule.add x y c3+         Rule.mul y z c6+         Rule.equ z c3+         Rule.pow y w c8+      liftM4+         (,,,)+         (Sys.query x)+         (Sys.query y)+         (Sys.query z)+         (Sys.query w))
+ src/UniqueLogic/ST/TF/Example/Term.hs view
@@ -0,0 +1,32 @@+{- |+This module is intended for documentation purposes. Do not import it!+-}+module UniqueLogic.ST.TF.Example.Term where+++data T =+     Const Rational+   | Var Name+   | Max T T+   | Add T T+   | Sub T T+   | Mul T T+   | Div T T+   | Abs T+   | Signum T+   deriving (Show)++type Name = String+++instance Num T where+   fromInteger n = Const $ fromInteger n+   (+) = Add+   (-) = Sub+   (*) = Mul+   abs = Abs+   signum = Signum++instance Fractional T where+   fromRational x = Const x+   (/) = Div
+ src/UniqueLogic/ST/TF/Example/Verify.hs view
@@ -0,0 +1,159 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+module UniqueLogic.ST.TF.Example.Verify+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}+ where++import qualified UniqueLogic.ST.TF.Example.Term as Term+import qualified UniqueLogic.ST.TF.Expression as Expr+import qualified UniqueLogic.ST.TF.System as Sys+import qualified UniqueLogic.ST.TF.MonadTrans as UMT+import UniqueLogic.ST.TF.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, when, )+import Control.Applicative (Applicative, pure, (<*>), )++import qualified Prelude as P+import Prelude hiding (max, log)++++data Assign = Assign Term.Name (TrackedNumber Rational)+   deriving (Show)++type Assigns = [Assign]++data TrackedNumber a = TrackedNumber Term.T a+   deriving (Show)++instance Functor TrackedNumber where+   fmap f (TrackedNumber term a) = TrackedNumber term $ f a+++tn1 :: (Term.T -> Term.T) -> (a -> b) -> TrackedNumber a -> TrackedNumber b+tn1 f g (TrackedNumber xt xn) = TrackedNumber (f xt) (g xn)++tn2 :: (Term.T -> Term.T -> Term.T) -> (a -> b -> c) -> TrackedNumber a -> TrackedNumber b -> TrackedNumber c+tn2 f g (TrackedNumber xt xn) (TrackedNumber yt yn) =+   TrackedNumber (f xt yt) (g xn yn)++instance Num a => Num (TrackedNumber a) where+   fromInteger n = TrackedNumber (fromInteger n) (fromInteger n)+   (+) = tn2 (+) (+)+   (-) = tn2 (-) (-)+   (*) = tn2 (*) (*)+   abs = tn1 abs abs+   signum = tn1 signum signum++instance Fractional a => Fractional (TrackedNumber a) where+   fromRational n = TrackedNumber (fromRational n) (fromRational n)+   (/) = tn2 (/) (/)+++instance (Monad m) => Functor (Track m) where+   fmap = liftM++instance (Monad m) => Applicative (Track m) where+   pure = return+   (<*>) = ap++instance (Monad m) => Monad (Track m) where+   return = Track . UMT.point+   x >>= k  =  Track $ UMT.bind (runTrack x) (runTrack . k)+++instance MT.MonadTrans Track where+   lift = Track . MT.lift . MT.lift++instance UMT.C Track where+   point = return+   bind = (>>=)++class ToTrackedNumber a where+   toTrackedNumber :: a -> TrackedNumber Rational++instance (Real a) => ToTrackedNumber (TrackedNumber a) where+   toTrackedNumber (TrackedNumber term a) =+      TrackedNumber term $ toRational a++instance (ToTrackedNumber tn) => Sys.Value Track tn where+   data ValueConstraint Track tn =+           (ToTrackedNumber tn) => VerifyConstraint+   valueConstraint _ _ = VerifyConstraint++instance Sys.C Track where+   update al av act =+      case Sys.valueConstraint al av of+         VerifyConstraint ->+            Sys.updateAndCheck+               (\old new ->+                  inconsistency Nothing (toTrackedNumber old) (toTrackedNumber new))+               al av act+++newtype+   Track m a =+      Track {runTrack :: ME.ExceptionalT Exception (MW.WriterT Assigns m) a}++data+   Exception =+      Exception (Maybe Term.Name) (TrackedNumber Rational) (TrackedNumber Rational)+   deriving (Show)++type Variable s = Sys.Variable Track s (TrackedNumber Rational)++globalVariable :: Term.Name -> ST s (Variable s)+globalVariable name =+   Sys.globalVariable+      (\al av -> Sys.updateAndCheck (inconsistency $ Just name) al av . logUpdate name)+++match :: (Eq a) => TrackedNumber a -> TrackedNumber a -> Bool+match (TrackedNumber _ x) (TrackedNumber _ y)  =  x==y++inconsistency ::+   Monad m =>+   Maybe Term.Name ->+   TrackedNumber Rational ->+   TrackedNumber Rational ->+   UMT.Wrap Track m ()+inconsistency name old new =+   when (not $ match old new) $+   UMT.wrap $ Track $ ME.throwT $ Exception name old new++logUpdate ::+   (Real a) =>+   Term.Name ->+   MaybeT (ST s) (TrackedNumber a) ->+   MaybeT (UMT.Wrap Track (ST s)) (TrackedNumber a)+logUpdate name act = do+   tn@(TrackedNumber _ x) <- mapMaybeT UMT.lift act+   MT.lift $ UMT.wrap $ Track $ MT.lift $+      writer (TrackedNumber (Term.Var name) x, [Assign name $ fmap toRational tn])+++example ::+   (ME.Exceptional Exception+       (Maybe (TrackedNumber Rational),+        Maybe (TrackedNumber Rational)),+    Assigns)+example =+   runST (do+      xv <- globalVariable "x"+      yv <- globalVariable "y"+      MW.runWriterT $ ME.runExceptionalT $ runTrack $ do+         Sys.solve $ do+            let x = Expr.fromVariable xv+                y = Expr.fromVariable yv+            x*3 =:= y/2+            5 =:= 2+x+         MT.lift $ liftM2 (,)+            (Sys.query xv)+            (Sys.query yv))
+ src/UniqueLogic/ST/TF/Expression.hs view
@@ -0,0 +1,181 @@+{-# LANGUAGE FlexibleContexts #-}+module UniqueLogic.ST.TF.Expression (+   T,+   -- * Construct primitive expressions+   constant, fromVariable,+   -- * Operators from rules with small numbers of arguments+   fromRule1, fromRule2, fromRule3,+   -- * Operators from rules with any number of arguments+   Apply, arg, runApply,+   -- * Predicates on expressions+   (=:=),+   -- * Common operators (see also 'Num' and 'Fractional' instances)+   (=!=),+   sqr, sqrt,+   max, maximum,+   pair,+   ) where++import qualified UniqueLogic.ST.TF.Rule as Rule+import qualified UniqueLogic.ST.TF.System as Sys++import Control.Monad (ap, )+import Control.Applicative (Applicative, pure, liftA, liftA2, (<*>), )++-- import Control.Category ((.))+-- import Data.Maybe (Maybe)++-- import Prelude (Double, Eq, Ord, (+), (*), (/))+import qualified Prelude as P+import Prelude hiding (max, maximum, sqrt)+++{- |+An expression is defined by a set of equations+and the variable at the top-level.+The value of the expression equals the value of the top variable.+-}+newtype T w s a = Cons (Sys.T w s (Sys.Variable w s a))+++{- |+Make a constant expression of a simple numeric value.+-}+constant :: (Sys.C w, Sys.Value w a) => a -> T w s a+constant = Cons . Sys.constant++fromVariable :: Sys.Variable w s a -> T w s a+fromVariable = Cons . return+++fromRule1 ::+   (Sys.C w, Sys.Value w a) =>+   (Sys.Variable w s a -> Sys.T w s ()) ->+   (T w s a)+fromRule1 rule = Cons $ do+   xv <- Sys.localVariable+   rule xv+   return xv++fromRule2, _fromRule2 ::+   (Sys.C w, Sys.Value w b) =>+   (Sys.Variable w s a -> Sys.Variable w s b -> Sys.T w s ()) ->+   (T w s a -> T w s b)+fromRule2 rule (Cons x) = Cons $ do+   xv <- x+   yv <- Sys.localVariable+   rule xv yv+   return yv++fromRule3, _fromRule3 ::+   (Sys.C w, Sys.Value w c) =>+   (Sys.Variable w s a -> Sys.Variable w s b -> Sys.Variable w s c -> Sys.T w s ()) ->+   (T w s a -> T w s b -> T w s c)+fromRule3 rule (Cons x) (Cons y) = Cons $ do+   xv <- x+   yv <- y+   zv <- Sys.localVariable+   rule xv yv zv+   return zv+++newtype Apply w s f = Apply (Sys.T w s f)++instance Functor (Apply w s) where+   fmap f (Apply a) = Apply $ fmap f a++instance Applicative (Apply w s) where+   pure a = Apply $ return a+   Apply f <*> Apply a = Apply $ ap f a+++{- |+This function allows to generalize 'fromRule2' and 'fromRule3' to more arguments+using 'Applicative' combinators.++Example:++> fromRule3 rule x y+>    = runApply $ liftA2 rule (arg x) (arg y)+>    = runApply $ pure rule <*> arg x <*> arg y++Building rules with 'arg' provides more granularity+than using auxiliary 'pair' rules!+-}+arg ::+   T w s a -> Apply w s (Sys.Variable w s a)+arg (Cons x) = Apply x++runApply ::+   (Sys.C w, Sys.Value w a) =>+   Apply w s (Sys.Variable w s a -> Sys.T w s ()) ->+   T w s a+runApply (Apply rule) = Cons $ do+   f <- rule+   xv <- Sys.localVariable+   f xv+   return xv++{-+examples of how to use 'arg' and 'runApply'+-}+_fromRule2 rule x = runApply $ liftA rule $ arg x+_fromRule3 rule x y = runApply $ liftA2 rule (arg x) (arg y)+++instance (Sys.C w, Sys.Value w a, P.Fractional a) => P.Num (T w s a) where+   fromInteger = constant . fromInteger+   (+) = fromRule3 Rule.add+   (-) = fromRule3 (\z x y -> Rule.add x y z)+   (*) = fromRule3 Rule.mul+   abs = fromRule2 (Sys.assignment2 abs)+   signum = fromRule2 (Sys.assignment2 signum)++instance (Sys.C w, Sys.Value w a, P.Fractional a) => P.Fractional (T w s a) where+   fromRational = constant . fromRational+   (/) = fromRule3 (\z x y -> Rule.mul x y z)++sqr :: (Sys.C w, Sys.Value w a, P.Floating a) => T w s a -> T w s a+sqr = fromRule2 Rule.square++sqrt :: (Sys.C w, Sys.Value w a, P.Floating a) => T w s a -> T w s a+sqrt = fromRule2 (flip Rule.square)+++infixl 4 =!=++(=!=) :: (Sys.C w) => T w s a -> T w s a -> T w s a+(=!=) (Cons x) (Cons y) = Cons $ do+   xv <- x+   yv <- y+   Rule.equ xv yv+   return xv++infix 0 =:=++(=:=) :: (Sys.C w) => T w s a -> T w s a -> Sys.T w s ()+(=:=) (Cons x) (Cons y) = do+   xv <- x+   yv <- y+   Rule.equ xv yv+++{- |+We are not able to implement a full Ord instance+including Eq superclass and comparisons,+but we need to compute maxima.+-}+max :: (Sys.C w, Ord a, Sys.Value w a) => T w s a -> T w s a -> T w s a+max = fromRule3 Rule.max++maximum :: (Sys.C w, Ord a, Sys.Value w a) => [T w s a] -> T w s a+maximum = foldl1 max+++{- |+Construct or decompose a pair.+-}+pair ::+   (Sys.C w, Sys.Value w a, Sys.Value w b, Sys.Value w (a,b)) =>+   T w s a -> T w s b -> T w s (a,b)+pair = fromRule3 Rule.pair
+ src/UniqueLogic/ST/TF/MonadTrans.hs view
@@ -0,0 +1,68 @@+{-+This module could also be part of 'transformers'.+-}+module UniqueLogic.ST.TF.MonadTrans where++import qualified Control.Monad.Exception.Synchronous as E++import qualified Control.Monad.Trans.Class as MT+import qualified Control.Monad.Trans.Writer as MW+import qualified Control.Monad.Trans.Maybe as MM+import qualified Control.Monad.Trans.Identity as MI++import Control.Applicative (Applicative, pure, (<*>), Const(Const))+import Control.Monad (liftM, ap, )+import Data.Monoid (Monoid, )+++{- |+Provide the methods that make a transformed monad a monad.+-}+class MT.MonadTrans t => C t where+   point :: Monad m => a -> t m a+   bind :: Monad m => t m a -> (a -> t m b) -> t m b++instance C MI.IdentityT where+   point = return+   bind = (>>=)++instance (Monoid w) => C (MW.WriterT w) where+   point = return+   bind = (>>=)++instance C (E.ExceptionalT e) where+   point = return+   bind = (>>=)++instance C MM.MaybeT where+   point = return+   bind = (>>=)+++{- |+Build a regular monad for generic monad transformer and monad.+The 'Const' type allows us to force the kind (m :: * -> *)+without using ExplicitKindSignatures.+-}+newtype Wrap t m a = Wrap (Const (t m a) (m a))++wrap :: t m a -> Wrap t m a+wrap = Wrap . Const++unwrap :: Wrap t m a -> t m a+unwrap (Wrap (Const m)) = m++lift :: (C t, Monad m) => m a -> Wrap t m a+lift = wrap . MT.lift+++instance (C t, Monad m) => Functor (Wrap t m) where+   fmap = liftM++instance (C t, Monad m) => Applicative (Wrap t m) where+   pure = return+   (<*>) = ap++instance (C t, Monad m) => Monad (Wrap t m) where+   return = wrap . point+   x >>= k  =  wrap $ bind (unwrap x) (unwrap . k)
+ src/UniqueLogic/ST/TF/Rule.hs view
@@ -0,0 +1,80 @@+module UniqueLogic.ST.TF.Rule (+   -- * Custom rules+   generic2,+   generic3,+   -- * Common rules+   equ, pair, max, add, mul, square, pow,+   ) where++import qualified UniqueLogic.ST.TF.System as Sys+import qualified UniqueLogic.ST.TF.MonadTrans as UMT++import qualified Prelude as P+import Prelude hiding (max)+++generic2 ::+   (UMT.C w) =>+   (b -> a) -> (a -> b) ->+   Sys.Variable w s a -> Sys.Variable w s b -> Sys.T w s ()+generic2 f g x y =+   sequence_ $+   Sys.assignment2 f y x :+   Sys.assignment2 g x y :+   []++generic3 ::+   (UMT.C w) =>+   (b -> c -> a) -> (c -> a -> b) -> (a -> b -> c) ->+   Sys.Variable w s a -> Sys.Variable w s b -> Sys.Variable w s c -> Sys.T w s ()+generic3 f g h x y z =+   sequence_ $+   Sys.assignment3 f y z x :+   Sys.assignment3 g z x y :+   Sys.assignment3 h x y z :+   []+++equ ::+   (UMT.C w) =>+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()+equ = generic2 id id++max ::+   (Ord a, UMT.C w) =>+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()+max =+   Sys.assignment3 P.max++{- |+You might be tempted to use the 'pair' rule to collect parameters+for rules with more than three arguments.+This is generally not a good idea since this way you lose granularity.+For building rules with more than three arguments,+please build according assignments with 'Sys.arg' and 'Sys.runApply'+and bundle these assignments to rules.+This is the way, 'generic2' and 'generic3' work.+-}+pair ::+   (UMT.C w) =>+   Sys.Variable w s a -> Sys.Variable w s b -> Sys.Variable w s (a,b) -> Sys.T w s ()+pair x y xy =+   Sys.assignment3 (,) x y xy >>+   Sys.assignment2 fst xy x >>+   Sys.assignment2 snd xy y++add :: (Num a, UMT.C w) =>+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()+add = generic3 subtract (-) (+)++mul :: (Fractional a, UMT.C w) =>+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()+mul = generic3 (flip (/)) (/) (*)++square :: (Floating a, UMT.C w) =>+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()+square = generic2 sqrt (^(2::Int))++pow :: (Floating a, UMT.C w) =>+   Sys.Variable w s a -> Sys.Variable w s a -> Sys.Variable w s a -> Sys.T w s ()+pow = generic3 (\x y -> y ** recip x) (flip logBase) (**)
+ src/UniqueLogic/ST/TF/System.hs view
@@ -0,0 +1,280 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+module UniqueLogic.ST.TF.System (+   -- * Preparation+   Variable,+   globalVariable,+   -- * Handle duplicates+   C, update,+   simpleUpdate, -- should be private in future+   updateIfNew, -- should be private or with special type+   updateAndCheck,+   Fragile(break),+   Value, ValueConstraint, valueConstraint,+   -- * Posing statements+   T,+   localVariable,+   constant,+   assignment2,+   assignment3,+   Apply, arg, runApply,+   -- * Solution+   solve, solveDepthFirst, solveBreadthFirst,+   query,+   ) where++import qualified Control.Monad.Exception.Synchronous as E+import qualified Control.Monad.Trans.Writer as MW+import qualified Control.Monad.Trans.Class  as MT+import qualified UniqueLogic.ST.TF.MonadTrans as UMT+import qualified Data.Sequence as Seq+import qualified Data.Foldable as Fold+import Control.Monad.Trans.Writer (WriterT, )+import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT, mapMaybeT, )+import Control.Monad.Trans.Identity (IdentityT, )+import Control.Monad.ST (ST, )+import Control.Monad (when, liftM2, ap, guard, )+import Control.Applicative (Applicative, pure, (<*>), )+import Data.Sequence (Seq, (|>), ViewL((:<)), )+import Data.Functor.Compose (Compose(Compose))++import Data.STRef (STRef, newSTRef, modifySTRef, readSTRef, writeSTRef, )+import Data.Maybe (isNothing, )+import Data.Monoid (Monoid, mempty, mappend, mconcat, )++import Prelude hiding (break)+++data Variable w s a =+   Variable {+      varUpdate :: MaybeT (ST s) a -> Update w s,+      dependsRef :: STRef s (Updates w s),+      valueRef :: STRef s (Maybe a)+   }++type Update w s = UMT.Wrap w (ST s) (Updates w s)+newtype Updates w s = Updates {unpackUpdates :: Seq (Update w s)}++instance Monoid (Updates w s) where+   mempty = Updates Seq.empty+   mappend (Updates x) (Updates y) = Updates $ mappend x y++addUpdate :: Update w s -> Updates w s -> Updates w s+addUpdate x (Updates xs) = Updates $ xs |> x+++type Updater w s a =+        STRef s (Updates w s) -> STRef s (Maybe a) ->+        MaybeT (UMT.Wrap w (ST s)) a -> Update w s++type SimpleUpdater w s a =+        STRef s (Updates w s) -> STRef s (Maybe a) ->+        MaybeT (ST s) a -> Update w s++newtype T w s a =+   Cons {run :: WriterT [STRef s (Updates w s)] (ST s) a}++instance Functor (T w s) where+   fmap f (Cons x) = Cons (fmap f x)++instance Applicative (T w s) where+   pure = Cons . return+   (<*>) = ap++instance Monad (T w s) where+   return = Cons . return+   Cons x >>= k  = Cons $ run . k =<< x+++lift :: ST s a -> T w s a+lift = Cons . MT.lift++globalVariable ::+   (UMT.C w, Value w a) =>+   SimpleUpdater w s a -> ST s (Variable w s a)+globalVariable triggerUpdate = object triggerUpdate Nothing++localVariable :: (C w, Value w a) => T w s (Variable w s a)+localVariable = lift $ globalVariable simpleUpdate++constant ::+   (C w, Value w a) =>+   a -> T w s (Variable w s a)+constant a =+   do v <- lift $ object simpleUpdate $ Just a+      Cons $ MW.tell [dependsRef v]+      return v++object ::+   SimpleUpdater w s a ->+   Maybe a -> ST s (Variable w s a)+object updater ma = do+   al <- newSTRef mempty+   av <- newSTRef ma+   return $ Variable (updater al av) al av+++solve, solveDepthFirst, solveBreadthFirst ::+   UMT.C w =>+   T w s a -> w (ST s) a+solve = solveDepthFirst++data Order = DepthFirst | BreadthFirst+   deriving (Eq, Enum)++solveDepthFirst   = solveOrder DepthFirst+solveBreadthFirst = solveOrder BreadthFirst++solveOrder ::+   UMT.C w =>+   Order -> T w s a -> w (ST s) a+solveOrder order (Cons m) = UMT.unwrap $ do+   let resolve updates =+          case Seq.viewl updates of+             Seq.EmptyL -> return ()+             currentUpdate :< remUpdates -> do+                Updates newUpdates <- currentUpdate+                resolve $+                   case order of+                      DepthFirst -> mappend newUpdates remUpdates+                      BreadthFirst -> mappend remUpdates newUpdates++   (a, w) <- UMT.lift $ MW.runWriterT m+   resolve . unpackUpdates . mconcat =<< mapM (UMT.lift . readSTRef) w+   return a++query :: Variable w s a -> ST s (Maybe a)+query = readSTRef . valueRef+++updateIfNew :: (C w) => Updater w s a+updateIfNew al av act = do+   as <- UMT.lift $ readSTRef av+   fmap Fold.fold $ runMaybeT $ do+      guard $ isNothing as+      MT.lift . UMT.lift . writeSTRef av . Just =<< act+      MT.lift $ UMT.lift $ readSTRef al+++class Inconsistency e where+   inconsistency :: e++instance+   Inconsistency e =>+      Fragile (E.ExceptionalT e) where+   break =+      UMT.wrap $ E.throwT inconsistency++class C t => Fragile t where+   break :: Monad m => UMT.Wrap t m a++updateAndCheck ::+   (UMT.C w) =>+   (a -> a -> UMT.Wrap w (ST s) ()) ->+   Updater w s a+updateAndCheck customBreak al av act = do+   maold <- UMT.lift $ readSTRef av+   manew <- runMaybeT act+   case manew of+      Nothing -> return mempty+      Just anew -> do+         UMT.lift . writeSTRef av . Just $ anew+         case maold of+            Just aold -> customBreak aold anew >> return mempty+            Nothing -> UMT.lift $ readSTRef al+++class C w => Value w a where+   data ValueConstraint w a :: *+   valueConstraint ::+      STRef s (Updates w s) -> STRef s (Maybe a) -> ValueConstraint w a++class UMT.C w => C w where+   update :: (Value w a) => Updater w s a++instance Value IdentityT a where+   data ValueConstraint IdentityT a = IdentityConstraint+   valueConstraint _ _ = IdentityConstraint++instance C IdentityT where+   update = updateIfNew++instance (Monoid w) => Value (MW.WriterT w) a where+   data ValueConstraint (MW.WriterT w) a = WriterConstraint+   valueConstraint _ _ = WriterConstraint++instance (Monoid w) => C (MW.WriterT w) where+   update = updateIfNew++instance (Inconsistency e, Eq a) => Value (E.ExceptionalT e) a where+   data ValueConstraint (E.ExceptionalT e) a =+           Eq a => ExceptionConstraint+   valueConstraint _ _ = ExceptionConstraint++instance (Inconsistency e) => C (E.ExceptionalT e) where+   update al av act =+      case valueConstraint al av of+         ExceptionConstraint ->+            updateAndCheck (\aold anew -> when (aold /= anew) break) al av act++simpleUpdate :: (C w, Value w a) => SimpleUpdater w s a+simpleUpdate al av = update al av . mapMaybeT UMT.lift+++readSTRefM :: STRef s (Maybe a) -> MaybeT (ST s) a+readSTRefM = MaybeT . readSTRef+++assignment2 ::+   UMT.C w =>+   (a -> b) ->+   Variable w s a -> Variable w s b ->+   T w s ()+assignment2 f (Variable _ al av) b =+   let triggerUpdate =+          varUpdate b $ fmap f $ readSTRefM av+   in  lift $+       modifySTRef al (addUpdate triggerUpdate)++assignment3 ::+   UMT.C w =>+   (a -> b -> c) ->+   Variable w s a -> Variable w s b -> Variable w s c ->+   T w s ()+assignment3 f (Variable _ al av) (Variable _ bl bv) c =+   let triggerUpdate =+          varUpdate c $+          liftM2 f (readSTRefM av) (readSTRefM bv)+   in  lift $+       modifySTRef al (addUpdate triggerUpdate) >>+       modifySTRef bl (addUpdate triggerUpdate)+++newtype Apply w s a =+   Apply (Compose (MW.Writer [STRef s (Updates w s)]) (MaybeT (ST s)) a)+++{- |+This function allows to generalize 'assignment2' and 'assignment3' to more arguments.+You could achieve the same with nested applications of @assignment3 (,)@.+-}+arg :: Variable w s a -> Apply w s a+arg (Variable _update al av) =+   Apply $ Compose $ MW.writer (MaybeT $ readSTRef av, [al])++instance Functor (Apply w s) where+   fmap f (Apply a) = Apply $ fmap f a++instance Applicative (Apply w s) where+   pure a = Apply $ pure a+   Apply f <*> Apply a = Apply $ f <*> a+++runApply ::+   UMT.C w =>+   Apply w s a -> Variable w s a -> T w s ()+runApply (Apply (Compose w)) a =+   case MW.runWriter w of+      (f, refs) ->+         lift $ Fold.forM_ refs $ flip modifySTRef (addUpdate $ varUpdate a f)
+ src/UniqueLogic/ST/TF/System/Label.hs view
@@ -0,0 +1,47 @@+module UniqueLogic.ST.TF.System.Label (+   -- * Preparation+   Variable,+   globalVariable,+   -- * Posing statements+   T,+   Sys.localVariable,+   Sys.constant,+   Sys.assignment2,+   Sys.assignment3,+   Sys.Apply, Sys.arg, Sys.runApply,+   -- * Solution+   Sys.solve,+   Sys.query,+   ) where++import qualified UniqueLogic.ST.TF.System as Sys+import qualified UniqueLogic.ST.TF.MonadTrans as UMT++import qualified Control.Monad.Trans.Writer as MW+import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT, )+import Control.Monad.ST (ST, )++import Data.Monoid (Monoid, )+import Data.Traversable (traverse, )++import Prelude hiding (log, )+++type T w = Sys.T (MW.WriterT w)+type Variable w = Sys.Variable (MW.WriterT w)++globalVariable ::+   (Monoid w) =>+   (a -> MW.Writer w a) -> ST s (Variable w s a)+globalVariable log =+   Sys.globalVariable+      (\al av -> Sys.updateIfNew al av . wrap log)++wrap ::+   (Monoid w) =>+   (a -> MW.Writer w b) ->+   MaybeT (ST s) a -> MaybeT (UMT.Wrap (MW.WriterT w) (ST s)) b+wrap log =+   mapMaybeT $+      UMT.wrap . MW.WriterT . fmap (MW.runWriter . traverse log)+--      UMT.wrap . MW.writer . MW.runWriter . traverse log <=< UMT.lift
+ src/UniqueLogic/ST/TF/System/Simple.hs view
@@ -0,0 +1,42 @@+module UniqueLogic.ST.TF.System.Simple (+   -- * Preparation+   Variable,+   globalVariable,+   -- * Posing statements+   T,+   localVariable,+   constant,+   Sys.assignment2,+   Sys.assignment3,+   Sys.Apply, Sys.arg, Sys.runApply,+   -- * Solution+   solve,+   query,+   ) where++import qualified UniqueLogic.ST.TF.System as Sys++import Control.Monad.Trans.Identity (IdentityT, runIdentityT, )+import Control.Monad.ST (ST, )+++type T = Sys.T IdentityT++type Variable s a = Sys.Variable IdentityT s a+++globalVariable :: ST s (Variable s a)+globalVariable =+   Sys.globalVariable Sys.simpleUpdate++localVariable :: T s (Variable s a)+localVariable = Sys.localVariable++constant :: a -> T s (Variable s a)+constant = Sys.constant++solve :: T s a -> ST s a+solve = runIdentityT . Sys.solve++query :: Variable s a -> ST s (Maybe a)+query = Sys.query
+ src/UniqueLogic/ST/TF/Test.hs view
@@ -0,0 +1,78 @@+module Main where++import qualified UniqueLogic.ST.TF.Expression as Expr+import qualified UniqueLogic.ST.TF.System.Simple as Sys+import UniqueLogic.ST.TF.Expression ((=:=))++import qualified Control.Monad.Trans.Class as MT+import qualified Control.Monad.Trans.Writer as MW+import Control.Monad.Trans.Identity (IdentityT, )+import Control.Monad.ST (ST, runST, )+import Control.Monad (join, liftM2, )+import Data.Monoid (Monoid(mempty, mappend))++import Data.List (sortBy, )+import Data.Ord.HT (comparing, )++import qualified Data.NonEmpty as NonEmpty+import qualified Test.QuickCheck as QC+++shuffle :: NonEmpty.T [] Int -> [a] -> [a]+shuffle order =+   map snd . sortBy (comparing fst) .+   zip (NonEmpty.flatten $ NonEmpty.cycle order)++newtype Check s = Check {runCheck :: ST s Bool}++instance Monoid (Check s) where+   mempty = Check $ return True+   mappend (Check x) (Check y) = Check $ liftM2 (&&) x y++{-+Take a system of six equations and seven variables+where one variable is randomly chosen and initialized with the correct value.+The other six variables must be determined by the solver.+Then we pose the six equations and+finally check whether all variables got the right value.+-}+example :: Int -> NonEmpty.T [] Int -> Bool+example var order =+   runST+      (join . fmap runCheck . Sys.solve $ MW.execWriterT $ do+         let variable ::+                Int -> Rational ->+                MW.WriterT (Check s) (Sys.T s)+                   (Expr.T IdentityT s Rational)+             variable n x = do+                v <-+                   MT.lift $+                   if mod var 7 == n+                     then Sys.constant x+                     else Sys.localVariable+                MW.tell $ Check $ fmap (Just x ==) $ Sys.query v+                return $ Expr.fromVariable v++         c  <- variable 0 1+         x0 <- variable 1 2+         x1 <- variable 2 3+         y0 <- variable 3 4+         y1 <- variable 4 5+         z0 <- variable 5 6+         z1 <- variable 6 7++         MT.lift $ sequence_ $ shuffle order $+            (c+1 =:= x0) :+            (x1*2 =:= x0*3) :+            (2*c + y0/2 =:= 4) :+            (y0 =:= subtract 1 y1) :+            (c =:= z0/6) :+            (z0*z1 =:= 42) :+            [] )+++tests :: [(String, IO ())]+tests = [("example", QC.quickCheck example)]++main :: IO ()+main = mapM_ (\(msg, test) -> putStr (msg ++ " ") >> test) tests
+ unique-logic-tf.cabal view
@@ -0,0 +1,109 @@+Name:             unique-logic-tf+Version:          0.4+License:          BSD3+License-File:     LICENSE+Author:           Henning Thielemann+Maintainer:       Henning Thielemann <haskell@henning-thielemann.de>+Homepage:         http://code.haskell.org/~thielema/unique-logic-tf/+Category:         Logic programming+Synopsis:         Solve simple simultaneous equations+Description:+  Solve a number of equations simultaneously.+  This is not Computer Algebra,+  better think of a kind of type inference algorithm+  or logic programming with only one allowed solution.+  .+  Only one solution is computed.+  Simultaneous equations with multiple solutions are not allowed.+  However, variables may remain undefined.+  The solver may optionally check for consistency.+  It does not do so by default+  since with floating point numbers or symbolic expressions+  even simple rules may not be consistent.+  .+  The modules ordered with respect to abstraction level are:+  .+  * "UniqueLogic.ST.TF.System":+    Construct and solve sets of functional dependencies.+    Example: @assignment3 (+) a b c@ meaning dependency @a+b -> c@.+  .+  * "UniqueLogic.ST.TF.Rule":+    Combine functional dependencies to rules+    that can apply in multiple directions.+    Example: @add a b c@ means relation @a+b = c@+    which resolves to dependencies @a+b -> c, c-a -> b, c-b -> a@.+    For an executable example see "UniqueLogic.ST.TF.Example.Rule".+  .+  * "UniqueLogic.ST.TF.Expression":+    Allows to write rules using arithmetic operators.+    It creates temporary variables automatically.+    Example: @(a+b)*c =:= d@ resolves to @a+b = x, x*c = d@.+    For an executable example see "UniqueLogic.ST.TF.Example.Expression".+  .+  * "UniqueLogic.ST.TF.System.Simple":+    Provides specialised functions from "UniqueLogic.ST.TF.System"+    for the case of a system without labels and consistency checks.+  .+  * "UniqueLogic.ST.TF.System.Label":+    Provides a custom constructor for variables.+    When creating a variable you decide whether and how+    an assignment to this variable shall be logged.+    There is an example that shows how to solve a logic system+    using symbolic expressions.+    The naming and logging allows us to observe shared intermediate results.+    For an executable example see "UniqueLogic.ST.TF.Example.Label".+  .+  * By using more sophisticated monad transformers,+    we can check the equations for consistency,+    report inconsistencies and how they arised.+    We demonstrate that in "UniqueLogic.ST.TF.Example.Verify".+  .+  This variant of the package requires type families.+Tested-With:       GHC==7.4.2+Cabal-Version:     >=1.8+Build-Type:        Simple++Source-Repository this+  Tag:         0.4+  Type:        darcs+  Location:    http://code.haskell.org/~thielema/unique-logic-tf/++Source-Repository head+  Type:        darcs+  Location:    http://code.haskell.org/~thielema/unique-logic-tf/++Library+  Build-Depends:+    explicit-exception >=0.1.7 && <0.2,+    transformers >=0.2 && <0.4,+    containers >=0.4 && <0.6,+    utility-ht >=0.0.9 && <0.1,+    base >= 4 && <5+  GHC-Options:      -Wall+  Hs-Source-Dirs:   src++  Exposed-Modules:+    UniqueLogic.ST.TF.MonadTrans+    UniqueLogic.ST.TF.System+    UniqueLogic.ST.TF.System.Simple+    UniqueLogic.ST.TF.System.Label+    UniqueLogic.ST.TF.Rule+    UniqueLogic.ST.TF.Expression+    -- example modules+    UniqueLogic.ST.TF.Example.Rule+    UniqueLogic.ST.TF.Example.Label+    UniqueLogic.ST.TF.Example.Expression+    UniqueLogic.ST.TF.Example.Verify+    UniqueLogic.ST.TF.Example.Term++Test-Suite test-unique-logic+  Type:    exitcode-stdio-1.0+  Main-Is: src/UniqueLogic/ST/TF/Test.hs+  GHC-Options: -Wall+  Build-Depends:+    unique-logic-tf,+    QuickCheck >=2.4 && <2.6,+    non-empty >=0.0 && <0.1,+    transformers,+    utility-ht,+    base