packages feed

unique-logic (empty) → 0.2

raw patch · 7 files changed

+629/−0 lines, 7 filesdep +QuickCheckdep +basedep +non-emptysetup-changed

Dependencies added: QuickCheck, base, non-empty, transformers, unique-logic, utility-ht

Files

+ LICENSE view
@@ -0,0 +1,31 @@+Copyright (c) 2012, 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/Expression.hs view
@@ -0,0 +1,191 @@+module UniqueLogic.ST.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.Rule as Rule+import qualified UniqueLogic.ST.System as Sys++import Control.Monad.ST (runST, )+import Control.Monad (liftM2, 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 s a = Cons (Sys.M s (Sys.Variable s a))+++{- |+Make a constant expression of a simple numeric value.+-}+constant :: a -> T s a+constant = Cons . Sys.constant++fromVariable :: Sys.Variable s a -> T s a+fromVariable = Cons . return+++fromRule1 ::+   (Sys.Variable s a -> Sys.M s ()) ->+   (T s a)+fromRule1 rule = Cons $ do+   xv <- Sys.localVariable+   rule xv+   return xv++fromRule2, _fromRule2 ::+   (Sys.Variable s a -> Sys.Variable s b -> Sys.M s ()) ->+   (T s a -> T s b)+fromRule2 rule (Cons x) = Cons $ do+   xv <- x+   yv <- Sys.localVariable+   rule xv yv+   return yv++fromRule3, _fromRule3 ::+   (Sys.Variable s a -> Sys.Variable s b -> Sys.Variable s c -> Sys.M s ()) ->+   (T s a -> T s b -> T 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 s f = Apply (Sys.M s f)++instance Functor (Apply s) where+   fmap f (Apply a) = Apply $ fmap f a++instance Applicative (Apply 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 s a -> Apply s (Sys.Variable s a)+arg (Cons x) = Apply x++runApply ::+   Apply s (Sys.Variable s a -> Sys.M s ()) ->+   T 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 (P.Fractional a) => P.Num (T 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" abs)+   signum = fromRule2 (Sys.assignment2 "signum" signum)++instance (P.Fractional a) => P.Fractional (T s a) where+   fromRational = constant . fromRational+   (/) = fromRule3 (\z x y -> Rule.mul x y z)++sqr :: P.Floating a => T s a -> T s a+sqr = fromRule2 Rule.square++sqrt :: P.Floating a => T s a -> T s a+sqrt = fromRule2 (flip Rule.square)+++infixl 4 =!=++(=!=) :: (Eq a) => T s a -> T s a -> T s a+(=!=) (Cons x) (Cons y) = Cons $ do+   xv <- x+   yv <- y+   Rule.equ xv yv+   return xv++infix 0 =:=++(=:=) :: (Eq a) => T s a -> T s a -> Sys.M 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 :: (Ord a) => T s a -> T s a -> T s a+max = fromRule3 Rule.max++maximum :: (Ord a) => [T s a] -> T s a+maximum = foldl1 max+++{- |+Construct or decompose a pair.+-}+pair :: T s a -> T s b -> T s (a,b)+pair = fromRule3 Rule.pair+++_example :: (Maybe Double, Maybe Double)+_example =+   runST (do+      xv <- Sys.globalVariable+      yv <- Sys.globalVariable+      Sys.solve $ do+         let x = fromVariable xv+             y = fromVariable yv+         x*3 =:= y/2+         5 =:= 2+x+      liftM2+         (,)+         (Sys.query xv)+         (Sys.query yv))
+ src/UniqueLogic/ST/Rule.hs view
@@ -0,0 +1,102 @@+module UniqueLogic.ST.Rule (+   -- * Custom rules+   generic2, generic3,+   -- * Common rules+   equ, pair, max, add, mul, square, pow,+   ) where++import qualified UniqueLogic.ST.System as Sys++import Control.Monad.ST (runST, )+import Control.Monad (liftM4, )++import qualified Prelude as P+import Prelude hiding (max)+++generic2 :: String ->+   (b -> a) -> (a -> b) ->+   Sys.Variable s a -> Sys.Variable s b -> Sys.M s ()+generic2 name f g x y =+   sequence_ $+   Sys.assignment2 (name++"0") f y x :+   Sys.assignment2 (name++"1") g x y :+   []++generic3 :: String ->+   (b -> c -> a) -> (c -> a -> b) -> (a -> b -> c) ->+   Sys.Variable s a -> Sys.Variable s b -> Sys.Variable s c -> Sys.M s ()+generic3 name f g h x y z =+   sequence_ $+   Sys.assignment3 (name++"0") f y z x :+   Sys.assignment3 (name++"1") g z x y :+   Sys.assignment3 (name++"2") h x y z :+   []++equ :: (Eq a) =>+   Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()+equ = generic2 "Equ" id id++max :: (Ord a) =>+   Sys.Variable s a -> Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()+max =+   Sys.assignment3 "Max" P.max++pair ::+   Sys.Variable s a -> Sys.Variable s b -> Sys.Variable s (a,b) -> Sys.M s ()+pair x y xy =+   Sys.assignment3 "Pair" (,) x y xy >>+   Sys.assignment2 "Fst" fst xy x >>+   Sys.assignment2 "Snd" snd xy y++add :: (Num a) =>+   Sys.Variable s a -> Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()+add = generic3 "Add" subtract (-) (+)++mul :: (Fractional a) =>+   Sys.Variable s a -> Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()+mul = generic3 "Mul" (flip (/)) (/) (*)++square :: (Floating a) =>+   Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()+square = generic2 "Square" sqrt (^(2::Int))++pow :: (Floating a) =>+   Sys.Variable s a -> Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()+pow = generic3 "Pow" (\x y -> y ** recip x) (flip logBase) (**)+++-- * Example equation system++{- |+> 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+         add x y c3+         mul y z c6+         equ z c3+         pow y w c8+      liftM4+         (,,,)+         (Sys.query x)+         (Sys.query y)+         (Sys.query z)+         (Sys.query w))
+ src/UniqueLogic/ST/System.hs view
@@ -0,0 +1,152 @@+module UniqueLogic.ST.System (+   -- * Preparation+   Variable,+   globalVariable,+   -- * Posing statements+   M,+   localVariable,+   constant,+   assignment2,+   assignment3,+   Apply, arg, runApply,+   -- * Solution+   solve,+   query,+   ) where++import qualified Control.Monad.Trans.Writer as MW+import qualified Control.Monad.Trans.Class  as MT+import qualified Data.Foldable as Fold+import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT, )+import Control.Monad.ST (ST, )+import Control.Monad.HT ((<=<), )+import Control.Monad (when, liftM2, ap, void, )+import Control.Applicative (Applicative, pure, liftA, liftA2, (<*>), )+import Data.Functor.Compose (Compose(Compose))++import Data.STRef (STRef, newSTRef, modifySTRef, readSTRef, writeSTRef, )+import Data.Maybe (isNothing, )+++data Variable s a =+   Variable {+      dependsRef :: STRef s [ST s ()],+      valueRef :: STRef s (Maybe a)+   }++newtype M s a =+   M {runM :: MW.WriterT [STRef s [ST s ()]] (ST s) a}++instance Functor (M s) where+   fmap f (M x) = M (fmap f x)++instance Applicative (M s) where+   pure = M . return+   (<*>) = ap++instance Monad (M s) where+   return = M . return+   M x >>= k  = M $ runM . k =<< x+++lift :: ST s a -> M s a+lift = M . MT.lift++localVariable :: M s (Variable s a)+localVariable = lift globalVariable++globalVariable :: ST s (Variable s a)+globalVariable = object Nothing++constant :: a -> M s (Variable s a)+constant a =+   do v <- lift $ object $ Just a+      M $ MW.tell [dependsRef v]+      return v++object :: Maybe a -> ST s (Variable s a)+object ma =+   liftM2 Variable (newSTRef []) (newSTRef ma)++resolve ::+   STRef s [ST s ()] -> ST s ()+resolve =+   sequence_ <=< readSTRef++solve :: M s a -> ST s a+solve (M m) =+   do (a,w) <- MW.runWriterT m+      mapM_ resolve w+      return a++query :: Variable s a -> ST s (Maybe a)+query = readSTRef . valueRef++++updateIfNew :: Variable s a -> MaybeT (ST s) a -> ST s ()+updateIfNew (Variable al av) act = do+   as <- readSTRef av+   when (isNothing as) $ void $ runMaybeT $ do+      MT.lift . writeSTRef av . Just =<< act+      MT.lift $ resolve al++readSTRefM :: STRef s (Maybe a) -> MaybeT (ST s) a+readSTRefM = MaybeT . readSTRef++assignment2, _assignment2 ::+   String ->+   (a -> b) ->+   Variable s a -> Variable s b ->+   M s ()+assignment2 _ f (Variable al av) b =+   let update =+          updateIfNew b $ fmap f $ readSTRefM av+   in  lift $+       modifySTRef al (update :)++assignment3, _assignment3 ::+   String ->+   (a -> b -> c) ->+   Variable s a -> Variable s b -> Variable s c ->+   M s ()+assignment3 _ f (Variable al av) (Variable bl bv) c =+   let update =+          updateIfNew c $+          liftM2 f (readSTRefM av) (readSTRefM bv)+   in  lift $+       modifySTRef al (update :) >>+       modifySTRef bl (update :)+++newtype Apply s a =+   Apply (Compose (MW.Writer [STRef s [ST s ()]]) (MaybeT (ST s)) a)++instance Functor (Apply s) where+   fmap f (Apply a) = Apply $ fmap f a++instance Applicative (Apply s) where+   pure a = Apply $ pure a+   Apply f <*> Apply a = Apply $ f <*> a+++{- |+This function allows to generalize 'assignment2' and 'assignment3' to more arguments.+You could achieve the same with nested applications of @assignment3 (,)@.+-}+arg :: Variable s a -> Apply s a+arg (Variable al av) =+   Apply $ Compose $ MW.writer (readSTRefM av, [al])++runApply :: String -> Apply s a -> Variable s a -> M s ()+runApply _ (Apply (Compose w)) a =+   case MW.runWriter w of+      (f, refs) ->+         lift $ Fold.forM_ refs $ flip modifySTRef (updateIfNew a f :)+++{-+examples of how to use 'arg' and 'runApply'+-}+_assignment2 msg f x = runApply msg (liftA f $ arg x)+_assignment3 msg f x y = runApply msg (liftA2 f (arg x) (arg y))
+ src/UniqueLogic/ST/Test.hs view
@@ -0,0 +1,76 @@+module Main where++import qualified UniqueLogic.ST.Expression as Expr+import qualified UniqueLogic.ST.System as Sys+import UniqueLogic.ST.Expression ((=:=))++import qualified Control.Monad.Trans.Class as MT+import qualified Control.Monad.Trans.Writer as MW+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.M s) (Expr.T 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.cabal view
@@ -0,0 +1,74 @@+Name:             unique-logic+Version:          0.2+License:          BSD3+License-File:     LICENSE+Author:           Henning Thielemann+Maintainer:       Henning Thielemann <haskell@henning-thielemann.de>+Homepage:         http://code.haskell.org/~thielema/unique-logic/+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.+  We do not even check for consistency,+  since with floating point numbers even simple rules may not be consistent.+  .+  The modules ordered with respect to abstraction level:+  .+  * "UniqueLogic.ST.System":+    Construct and solve sets of functional dependencies.+    Example: @assignment3 (+) a b c@ meaning dependency @a+b -> c@.+  .+  * "UniqueLogic.ST.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@.+  .+  * "UniqueLogic.ST.Expression":+    Allow to write rules using arithmetic operators.+    It creates temporary variables automatically.+    Example: @(a+b)*c =:= d@ resolves to @a+b = x, x*c = d@.+Tested-With:       GHC==7.4.2+Cabal-Version:     >=1.8+Build-Type:        Simple++Source-Repository this+  Tag:         0.2+  Type:        darcs+  Location:    http://code.haskell.org/~thielema/unique-logic/++Source-Repository head+  Type:        darcs+  Location:    http://code.haskell.org/~thielema/unique-logic/++Library+  Build-Depends:+    transformers >=0.2 && <0.4,+    utility-ht >=0.0.1 && <0.1,+    base >= 4 && <5+  GHC-Options:      -Wall+  Hs-Source-Dirs:   src++  Exposed-modules:+    UniqueLogic.ST.System+    UniqueLogic.ST.Rule+    UniqueLogic.ST.Expression++Test-Suite test-unique-logic+  Type:    exitcode-stdio-1.0+  Main-Is: src/UniqueLogic/ST/Test.hs+  GHC-Options: -Wall+  Build-Depends:+    QuickCheck >=2.4 && <2.6,+    unique-logic,+    non-empty >=0.0 && <0.1,+    transformers,+    utility-ht,+    base