module UniqueLogic.ST.Example.Label
{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
 where

import qualified UniqueLogic.ST.Expression as Expr
import qualified UniqueLogic.ST.Rule as Rule
import qualified UniqueLogic.ST.SystemLabel as Sys
import UniqueLogic.ST.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 Name Term
   deriving (Show)

type Assigns = [Assign]

data Term =
     Const Rational
   | Var Name
   | Max Term Term
   | Add Term Term
   | Sub Term Term
   | Mul Term Term
   | Div Term Term
   | Abs Term
   | Signum Term
   deriving (Show)

type Name = String


instance Num Term where
   fromInteger n = Const $ fromInteger n
   (+) = Add
   (-) = Sub
   (*) = Mul
   abs = Abs
   signum = Signum

instance Fractional Term where
   fromRational x = Const x
   (/) = Div

globalVariable ::
   Name -> ST s (Sys.Variable Assigns s Term)
globalVariable name =
   Sys.globalVariable $
      \x -> writer (Var name, [Assign name x])

constant ::
   Rational -> Sys.T Assigns s (Sys.Variable Assigns s Term)
constant = Sys.constant . Const


{- |
> x=1
> y=2
> z=3

> x+y=3
> y*z=6
> z=3
-}
rule :: ((Maybe Term, Maybe Term, Maybe Term), 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, Maybe Term), 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))