{-# LANGUAGE BlockArguments, LambdaCase, OverloadedStrings #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.Derivation.Expression.Internal (
	Exp(..), ExpType(..), constraint, varBool ) where

import Prelude hiding ((<>), log)

import Outputable (Outputable(..), SDoc, (<>), (<+>), text)
import Control.Arrow (first, second)
import Control.Monad.Try (Try, throw, tell, partial)
import Data.Map.Strict (Map, (!?), empty, singleton, insert)
import Data.Maybe (fromJust)
import Data.List (find)
import Data.String (IsString, fromString)
import Data.Log (Log, (.+.), logVar, Loggable(..))
import Data.Derivation.Constraint (
	Constraint, equal, greatEqualThan, greatThan, Poly, (.+), (.-) )

---------------------------------------------------------------------------

-- * DATA EXP
--	+ DATA
--	+ INSTANCE
-- * CONSTRAINT
--	+ CONSTRAINT
--	+ PROCESS EQUATION
-- * POLYNOMIAL
-- * MAP FROM VARIABLE TO BOOL

---------------------------------------------------------------------------
-- DATA EXP
---------------------------------------------------------------------------

-- DATA

data Exp v t where
	Bool :: Bool -> Exp v 'Boolean; Var :: v -> Exp v t
	Const :: Integer -> Exp v 'Number
	(:==) :: Exp v t -> Exp v t -> Exp v 'Boolean
	(:<=) :: Exp v 'Number -> Exp v 'Number -> Exp v 'Boolean
	(:+) :: Exp v 'Number -> Exp v 'Number -> Exp v 'Number
	(:-) :: Exp v 'Number -> Exp v 'Number -> Exp v 'Number

data ExpType = Boolean | Number deriving Int -> ExpType -> ShowS
[ExpType] -> ShowS
ExpType -> String
(Int -> ExpType -> ShowS)
-> (ExpType -> String) -> ([ExpType] -> ShowS) -> Show ExpType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExpType] -> ShowS
$cshowList :: [ExpType] -> ShowS
show :: ExpType -> String
$cshow :: ExpType -> String
showsPrec :: Int -> ExpType -> ShowS
$cshowsPrec :: Int -> ExpType -> ShowS
Show

-- INSTANCE

deriving instance Show v => Show (Exp v t)

instance Outputable v => Outputable (Exp v t) where
	ppr :: Exp v t -> SDoc
ppr = \case
		Bool Bool
b -> String -> SDoc
text String
"(Bool" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
b SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
")"
		Var v
v -> String -> SDoc
text String
"(Var" SDoc -> SDoc -> SDoc
<+> v -> SDoc
forall a. Outputable a => a -> SDoc
ppr v
v SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
")"
		Const Integer
n -> String -> SDoc
text String
"(Const" SDoc -> SDoc -> SDoc
<+> Integer -> SDoc
forall a. Outputable a => a -> SDoc
ppr Integer
n SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
")"
		Exp v t
l :== Exp v t
r -> String -> Exp v t -> Exp v t -> SDoc
forall v (t :: ExpType).
Outputable v =>
String -> Exp v t -> Exp v t -> SDoc
pprOp String
":==" Exp v t
l Exp v t
r; Exp v 'Number
l :<= Exp v 'Number
r -> String -> Exp v 'Number -> Exp v 'Number -> SDoc
forall v (t :: ExpType).
Outputable v =>
String -> Exp v t -> Exp v t -> SDoc
pprOp String
":<=" Exp v 'Number
l Exp v 'Number
r
		Exp v 'Number
l :+ Exp v 'Number
r -> String -> Exp v 'Number -> Exp v 'Number -> SDoc
forall v (t :: ExpType).
Outputable v =>
String -> Exp v t -> Exp v t -> SDoc
pprOp String
":+" Exp v 'Number
l Exp v 'Number
r; Exp v 'Number
l :- Exp v 'Number
r -> String -> Exp v 'Number -> Exp v 'Number -> SDoc
forall v (t :: ExpType).
Outputable v =>
String -> Exp v t -> Exp v t -> SDoc
pprOp String
":-" Exp v 'Number
l Exp v 'Number
r

pprOp :: Outputable v => String -> Exp v t -> Exp v t -> SDoc
pprOp :: String -> Exp v t -> Exp v t -> SDoc
pprOp String
op Exp v t
l Exp v t
r = String -> SDoc
text String
"(" SDoc -> SDoc -> SDoc
<> Exp v t -> SDoc
forall a. Outputable a => a -> SDoc
ppr Exp v t
l SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
op SDoc -> SDoc -> SDoc
<+> Exp v t -> SDoc
forall a. Outputable a => a -> SDoc
ppr Exp v t
r SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
")"

instance IsString s => Loggable s v (Exp v t) where
	log :: Exp v t -> Log s v
log = \case
		Bool Bool
b -> String -> Log s v
forall a. IsString a => String -> a
fromString (String -> Log s v) -> String -> Log s v
forall a b. (a -> b) -> a -> b
$ String
"(Bool " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
		Var v
v -> String -> Log s v
forall a. IsString a => String -> a
fromString String
"(Var " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. v -> Log s v
forall v s. v -> Log s v
logVar v
v Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. String -> Log s v
forall a. IsString a => String -> a
fromString String
")"
		Const Integer
n -> String -> Log s v
forall a. IsString a => String -> a
fromString (String -> Log s v) -> String -> Log s v
forall a b. (a -> b) -> a -> b
$ String
"(Const " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
		Exp v t
l :== Exp v t
r -> String -> Exp v t -> Exp v t -> Log s v
forall s v (t :: ExpType).
IsString s =>
String -> Exp v t -> Exp v t -> Log s v
logOp String
":==" Exp v t
l Exp v t
r; Exp v 'Number
l :<= Exp v 'Number
r -> String -> Exp v 'Number -> Exp v 'Number -> Log s v
forall s v (t :: ExpType).
IsString s =>
String -> Exp v t -> Exp v t -> Log s v
logOp String
":<=" Exp v 'Number
l Exp v 'Number
r
		Exp v 'Number
l :+ Exp v 'Number
r -> String -> Exp v 'Number -> Exp v 'Number -> Log s v
forall s v (t :: ExpType).
IsString s =>
String -> Exp v t -> Exp v t -> Log s v
logOp String
":+" Exp v 'Number
l Exp v 'Number
r; Exp v 'Number
l :- Exp v 'Number
r -> String -> Exp v 'Number -> Exp v 'Number -> Log s v
forall s v (t :: ExpType).
IsString s =>
String -> Exp v t -> Exp v t -> Log s v
logOp String
":-" Exp v 'Number
l Exp v 'Number
r

logOp :: IsString s => String -> Exp v t -> Exp v t -> Log s v
logOp :: String -> Exp v t -> Exp v t -> Log s v
logOp String
op Exp v t
l Exp v t
r = String -> Log s v
forall a. IsString a => String -> a
fromString String
"(" Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+.
	Exp v t -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Exp v t
l Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. String -> Log s v
forall a. IsString a => String -> a
fromString (String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ") Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Exp v t -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Exp v t
r Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. String -> Log s v
forall a. IsString a => String -> a
fromString String
")"

---------------------------------------------------------------------------
-- CONSTRAINT
---------------------------------------------------------------------------

-- CONSTRAINT

constraint :: (Monoid w, IsString s, Ord v) => VarBool v -> Exp v 'Boolean ->
	Try (Log s v) w (Either (Log s v) (Constraint v), [Constraint v])
constraint :: VarBool v
-> Exp v 'Boolean
-> Try
     (Log s v) w (Either (Log s v) (Constraint v), [Constraint v])
constraint VarBool v
vb Exp v 'Boolean
ex = Try (Log s v) ([Constraint v], w) (Constraint v)
-> Try
     (Log s v) w (Either (Log s v) (Constraint v), [Constraint v])
forall e w ws a. Try e (w, ws) a -> Try e ws (Either e a, w)
partial (Try (Log s v) ([Constraint v], w) (Constraint v)
 -> Try
      (Log s v) w (Either (Log s v) (Constraint v), [Constraint v]))
-> Try (Log s v) ([Constraint v], w) (Constraint v)
-> Try
     (Log s v) w (Either (Log s v) (Constraint v), [Constraint v])
forall a b. (a -> b) -> a -> b
$ VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w s v.
(Monoid w, IsString s, Ord v) =>
VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
procEq VarBool v
vb Exp v 'Boolean
ex Bool
True

-- PROCCESS EQUATION

procEq :: (Monoid w, IsString s, Ord v) => VarBool v -> Exp v 'Boolean ->
	Bool -> Try (Log s v) ([Constraint v], w) (Constraint v)
procEq :: VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
procEq VarBool v
_ b :: Exp v 'Boolean
b@(Bool Bool
_) Bool
_ = Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w e a. Monoid w => e -> Try e w a
throw (Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v))
-> Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall a b. (a -> b) -> a -> b
$ Log s v
"procEq: only Boolean value: " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Exp v 'Boolean -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Exp v 'Boolean
b
procEq VarBool v
_ v :: Exp v 'Boolean
v@(Var v
_) Bool
_ = Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w e a. Monoid w => e -> Try e w a
throw (Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v))
-> Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall a b. (a -> b) -> a -> b
$ Log s v
"procEq: only Variable: " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Exp v 'Boolean -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Exp v 'Boolean
v
procEq VarBool v
_ (Exp v 'Number
l :<= Exp v 'Number
r) Bool
False = Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
greatThan (Poly v -> Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v 'Number
l Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v 'Number
r
procEq VarBool v
_ (Exp v 'Number
l :<= Exp v 'Number
r) Bool
True = Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
greatEqualThan (Poly v -> Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v 'Number
r Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v 'Number
l
procEq VarBool v
vb (Exp v t
l :== Bool Bool
r) Bool
b = VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w s v.
(Monoid w, IsString s, Ord v) =>
VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
procEq VarBool v
vb Exp v t
Exp v 'Boolean
l (Bool
r Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b)
procEq VarBool v
vb (Bool Bool
l :== Exp v t
r) Bool
b = VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w s v.
(Monoid w, IsString s, Ord v) =>
VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
procEq VarBool v
vb Exp v t
Exp v 'Boolean
r (Bool
l Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b)
procEq VarBool v
vb e :: Exp v 'Boolean
e@(Exp v t
l :== Var v
r) Bool
b | Just Bool
br <- VarBool v
vb VarBool v -> v -> Maybe Bool
forall k a. Ord k => Map k a -> k -> Maybe a
!? v
r = case Exp v t
l of
	Exp v t
_ :== Exp v t
_ -> VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w s v.
(Monoid w, IsString s, Ord v) =>
VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
procEq VarBool v
vb Exp v t
Exp v 'Boolean
l (Bool
br Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b); Exp v 'Number
_ :<= Exp v 'Number
_ -> VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w s v.
(Monoid w, IsString s, Ord v) =>
VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
procEq VarBool v
vb Exp v t
Exp v 'Boolean
l (Bool
br Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b)
	Exp v t
_ -> Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w e a. Monoid w => e -> Try e w a
throw (Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v))
-> Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall a b. (a -> b) -> a -> b
$ Log s v
"procEq: can't interpret: " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Exp v 'Boolean -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Exp v 'Boolean
e
procEq VarBool v
vb e :: Exp v 'Boolean
e@(Var v
l :== Exp v t
r) Bool
b | Just Bool
bl <- VarBool v
vb VarBool v -> v -> Maybe Bool
forall k a. Ord k => Map k a -> k -> Maybe a
!? v
l = case Exp v t
r of
	Exp v t
_ :== Exp v t
_ -> VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w s v.
(Monoid w, IsString s, Ord v) =>
VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
procEq VarBool v
vb Exp v t
Exp v 'Boolean
r (Bool
bl Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b); Exp v 'Number
_ :<= Exp v 'Number
_ -> VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w s v.
(Monoid w, IsString s, Ord v) =>
VarBool v
-> Exp v 'Boolean
-> Bool
-> Try (Log s v) ([Constraint v], w) (Constraint v)
procEq VarBool v
vb Exp v t
Exp v 'Boolean
r (Bool
bl Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b)
	Exp v t
_ -> Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w e a. Monoid w => e -> Try e w a
throw (Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v))
-> Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall a b. (a -> b) -> a -> b
$ Log s v
"procEq: can't interpret: " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Exp v 'Boolean -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Exp v 'Boolean
e
procEq VarBool v
_ e :: Exp v 'Boolean
e@(Exp v t
l :== Exp v t
r) Bool
True = case (Exp v t
l, Exp v t
r) of
	(Const Integer
_, Exp v t
_) -> Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
equal (Poly v -> Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
l Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
r
	(Exp v 'Number
_ :+ Exp v 'Number
_, Exp v t
_) -> Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
equal (Poly v -> Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
l Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
r
	(Exp v 'Number
_ :- Exp v 'Number
_, Exp v t
_) -> Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
equal (Poly v -> Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
l Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
r
	(Exp v t
_, Const Integer
_) -> Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
equal (Poly v -> Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
l Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
r
	(Exp v t
_, Exp v 'Number
_ :+ Exp v 'Number
_) -> Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
equal (Poly v -> Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
l Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
r
	(Exp v t
_, Exp v 'Number
_ :- Exp v 'Number
_) -> Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
equal (Poly v -> Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
l Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v t
Exp v 'Number
r
	(Var v
v, Var v
w) -> Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
equal (Poly v -> Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly (v -> Exp v 'Number
forall v (t :: ExpType). v -> Exp v t
Var v
v) Try (Log s v) ([Constraint v], w) (Poly v -> Constraint v)
-> Try (Log s v) ([Constraint v], w) (Poly v)
-> Try (Log s v) ([Constraint v], w) (Constraint v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try (Log s v) ([Constraint v], w) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly (v -> Exp v 'Number
forall v (t :: ExpType). v -> Exp v t
Var v
w)
	(Exp v t, Exp v t)
_ -> Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w e a. Monoid w => e -> Try e w a
throw (Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v))
-> Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall a b. (a -> b) -> a -> b
$ Log s v
"procEq: can't interpret: " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Exp v 'Boolean -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Exp v 'Boolean
e Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v
" == True"
procEq VarBool v
_ e :: Exp v 'Boolean
e@(Exp v t
_ :== Exp v t
_) Bool
False =
	Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall w e a. Monoid w => e -> Try e w a
throw (Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v))
-> Log s v -> Try (Log s v) ([Constraint v], w) (Constraint v)
forall a b. (a -> b) -> a -> b
$ Log s v
"procEq: can't interpret: " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Exp v 'Boolean -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Exp v 'Boolean
e Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v
" == False"

---------------------------------------------------------------------------
-- POLYNOMIAL
---------------------------------------------------------------------------

poly :: (Monoid s, IsString e, Ord v) =>
	Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly :: Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly = \case
	Const Integer
n	| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 -> e -> Try e ([Constraint v], s) (Poly v)
forall w e a. Monoid w => e -> Try e w a
throw
			(e -> Try e ([Constraint v], s) (Poly v))
-> (String -> e) -> String -> Try e ([Constraint v], s) (Poly v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> e
forall a. IsString a => String -> a
fromString (String -> Try e ([Constraint v], s) (Poly v))
-> String -> Try e ([Constraint v], s) (Poly v)
forall a b. (a -> b) -> a -> b
$ String
"poly: Negative constant " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
		| Integer
0 <- Integer
n -> Poly v -> Try e ([Constraint v], s) (Poly v)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Poly v
forall k a. Map k a
empty
		| Bool
otherwise -> Poly v -> Try e ([Constraint v], s) (Poly v)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Poly v -> Try e ([Constraint v], s) (Poly v))
-> Poly v -> Try e ([Constraint v], s) (Poly v)
forall a b. (a -> b) -> a -> b
$ Maybe v -> Integer -> Poly v
forall k a. k -> a -> Map k a
singleton Maybe v
forall a. Maybe a
Nothing Integer
n
	Var v
v -> let p :: Poly v
p = Maybe v -> Integer -> Poly v
forall k a. k -> a -> Map k a
singleton (v -> Maybe v
forall a. a -> Maybe a
Just v
v) Integer
1 in
		Poly v
p Poly v
-> Try e ([Constraint v], s) ()
-> Try e ([Constraint v], s) (Poly v)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Constraint v] -> Try e ([Constraint v], s) ()
forall w ws e. Set w ws => w -> Try e ws ()
tell [Poly v
p Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
`greatEqualThan` Poly v
forall k a. Map k a
empty]
	Exp v 'Number
l :+ Exp v 'Number
r -> Poly v -> Poly v -> Poly v
forall v. Ord v => Poly v -> Poly v -> Poly v
(.+) (Poly v -> Poly v -> Poly v)
-> Try e ([Constraint v], s) (Poly v)
-> Try e ([Constraint v], s) (Poly v -> Poly v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v 'Number
l Try e ([Constraint v], s) (Poly v -> Poly v)
-> Try e ([Constraint v], s) (Poly v)
-> Try e ([Constraint v], s) (Poly v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v 'Number
r
	Exp v 'Number
l :- Exp v 'Number
r -> (,) (Poly v -> Poly v -> (Poly v, Poly v))
-> Try e ([Constraint v], s) (Poly v)
-> Try e ([Constraint v], s) (Poly v -> (Poly v, Poly v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v 'Number
l Try e ([Constraint v], s) (Poly v -> (Poly v, Poly v))
-> Try e ([Constraint v], s) (Poly v)
-> Try e ([Constraint v], s) (Poly v, Poly v)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
forall s e v.
(Monoid s, IsString e, Ord v) =>
Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
poly Exp v 'Number
r Try e ([Constraint v], s) (Poly v, Poly v)
-> ((Poly v, Poly v) -> Try e ([Constraint v], s) (Poly v))
-> Try e ([Constraint v], s) (Poly v)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Poly v
pl, Poly v
pr) ->
		Poly v
pl Poly v -> Poly v -> Poly v
forall v. Ord v => Poly v -> Poly v -> Poly v
.- Poly v
pr Poly v
-> Try e ([Constraint v], s) ()
-> Try e ([Constraint v], s) (Poly v)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Constraint v] -> Try e ([Constraint v], s) ()
forall w ws e. Set w ws => w -> Try e ws ()
tell [Poly v
pl Poly v -> Poly v -> Constraint v
forall v. Ord v => Poly v -> Poly v -> Constraint v
`greatEqualThan` Poly v
pr]

---------------------------------------------------------------------------
-- MAP FROM VARIABLES TO BOOL
---------------------------------------------------------------------------

type VarBool v = Map v Bool

varBool :: Ord v => [Exp v 'Boolean] -> VarBool v
varBool :: [Exp v 'Boolean] -> VarBool v
varBool = ([(v, v)], VarBool v) -> VarBool v
forall a b. (a, b) -> b
snd (([(v, v)], VarBool v) -> VarBool v)
-> ([Exp v 'Boolean] -> ([(v, v)], VarBool v))
-> [Exp v 'Boolean]
-> VarBool v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([(v, v)], VarBool v) -> ([(v, v)], VarBool v))
-> ([(v, v)], VarBool v) -> ([(v, v)], VarBool v)
forall a. Eq a => (a -> a) -> a -> a
untilFixed (([(v, v)] -> VarBool v -> ([(v, v)], VarBool v))
-> ([(v, v)], VarBool v) -> ([(v, v)], VarBool v)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
forall v. Ord v => [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
vbStep) (([(v, v)], VarBool v) -> ([(v, v)], VarBool v))
-> ([Exp v 'Boolean] -> ([(v, v)], VarBool v))
-> [Exp v 'Boolean]
-> ([(v, v)], VarBool v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Exp v 'Boolean] -> ([(v, v)], VarBool v)
forall v. Ord v => [Exp v 'Boolean] -> ([(v, v)], VarBool v)
vbInit

vbInit :: Ord v => [Exp v 'Boolean] -> ([(v, v)], VarBool v)
vbInit :: [Exp v 'Boolean] -> ([(v, v)], VarBool v)
vbInit [] = ([], VarBool v
forall k a. Map k a
empty)
vbInit (Var v
l :== Var v
r : [Exp v 'Boolean]
es) = ((v
l, v
r) (v, v) -> [(v, v)] -> [(v, v)]
forall a. a -> [a] -> [a]
:) ([(v, v)] -> [(v, v)])
-> ([(v, v)], VarBool v) -> ([(v, v)], VarBool v)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
`first` [Exp v 'Boolean] -> ([(v, v)], VarBool v)
forall v. Ord v => [Exp v 'Boolean] -> ([(v, v)], VarBool v)
vbInit [Exp v 'Boolean]
es
vbInit (Var v
l :== Bool Bool
r : [Exp v 'Boolean]
es) = v -> Bool -> VarBool v -> VarBool v
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert v
l Bool
r (VarBool v -> VarBool v)
-> ([(v, v)], VarBool v) -> ([(v, v)], VarBool v)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
`second` [Exp v 'Boolean] -> ([(v, v)], VarBool v)
forall v. Ord v => [Exp v 'Boolean] -> ([(v, v)], VarBool v)
vbInit [Exp v 'Boolean]
es
vbInit (Bool Bool
l :== Var v
r : [Exp v 'Boolean]
es) = v -> Bool -> VarBool v -> VarBool v
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert v
r Bool
l (VarBool v -> VarBool v)
-> ([(v, v)], VarBool v) -> ([(v, v)], VarBool v)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
`second` [Exp v 'Boolean] -> ([(v, v)], VarBool v)
forall v. Ord v => [Exp v 'Boolean] -> ([(v, v)], VarBool v)
vbInit [Exp v 'Boolean]
es
vbInit (Exp v 'Boolean
_ : [Exp v 'Boolean]
es) = [Exp v 'Boolean] -> ([(v, v)], VarBool v)
forall v. Ord v => [Exp v 'Boolean] -> ([(v, v)], VarBool v)
vbInit [Exp v 'Boolean]
es

vbStep :: Ord v => [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
vbStep :: [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
vbStep [] VarBool v
vb = ([], VarBool v
vb)
vbStep ((v
l, v
r) : [(v, v)]
vs) VarBool v
vb = case (VarBool v
vb VarBool v -> v -> Maybe Bool
forall k a. Ord k => Map k a -> k -> Maybe a
!? v
l, VarBool v
vb VarBool v -> v -> Maybe Bool
forall k a. Ord k => Map k a -> k -> Maybe a
!? v
r) of
	(Just Bool
bl, Maybe Bool
_) -> [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
forall v. Ord v => [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
vbStep [(v, v)]
vs (VarBool v -> ([(v, v)], VarBool v))
-> VarBool v -> ([(v, v)], VarBool v)
forall a b. (a -> b) -> a -> b
$ v -> Bool -> VarBool v -> VarBool v
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert v
r Bool
bl VarBool v
vb
	(Maybe Bool
Nothing, Just Bool
br) -> [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
forall v. Ord v => [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
vbStep [(v, v)]
vs (VarBool v -> ([(v, v)], VarBool v))
-> VarBool v -> ([(v, v)], VarBool v)
forall a b. (a -> b) -> a -> b
$ v -> Bool -> VarBool v -> VarBool v
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert v
l Bool
br VarBool v
vb
	(Maybe Bool
Nothing, Maybe Bool
Nothing) -> ((v
l, v
r) (v, v) -> [(v, v)] -> [(v, v)]
forall a. a -> [a] -> [a]
:) ([(v, v)] -> [(v, v)])
-> ([(v, v)], VarBool v) -> ([(v, v)], VarBool v)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
`first` [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
forall v. Ord v => [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
vbStep [(v, v)]
vs VarBool v
vb

untilFixed :: Eq a => (a -> a) -> a -> a
untilFixed :: (a -> a) -> a -> a
untilFixed a -> a
f a
x = (a, a) -> a
forall a b. (a, b) -> a
fst ((a, a) -> a) -> ([(a, a)] -> (a, a)) -> [(a, a)] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (a, a) -> (a, a)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (a, a) -> (a, a))
-> ([(a, a)] -> Maybe (a, a)) -> [(a, a)] -> (a, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, a) -> Bool) -> [(a, a)] -> Maybe (a, a)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((a -> a -> Bool) -> (a, a) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)) ([(a, a)] -> a) -> [(a, a)] -> a
forall a b. (a -> b) -> a -> b
$ [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs ([a] -> [a]
forall a. [a] -> [a]
tail [a]
xs)
	where xs :: [a]
xs = (a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate a -> a
f a
x