module Feldspar.Core.Constructs.Logic
( Logic (..)
) where
import Language.Syntactic
import Language.Syntactic.Constructs.Binding
import Feldspar.Core.Types
import Feldspar.Core.Interpretation
import Feldspar.Core.Constructs.Eq
import Feldspar.Core.Constructs.Ord
data Logic a
where
And :: Logic (Bool :-> Bool :-> Full Bool)
Or :: Logic (Bool :-> Bool :-> Full Bool)
Not :: Logic (Bool :-> Full Bool)
instance Semantic Logic
where
semantics And = Sem "(&&)" (&&)
semantics Or = Sem "(||)" (||)
semantics Not = Sem "not" not
instance Equality Logic where equal = equalDefault; exprHash = exprHashDefault
instance Render Logic where renderArgs = renderArgsDefault
instance ToTree Logic
instance Eval Logic where evaluate = evaluateDefault
instance EvalBind Logic where evalBindSym = evalBindSymDefault
instance Sharable Logic
instance AlphaEq dom dom dom env => AlphaEq Logic Logic dom env
where
alphaEqSym = alphaEqSymDefault
instance SizeProp (Logic :|| Type)
where
sizeProp a@(C' _) args = sizePropDefault a args
instance ( (Logic :|| Type) :<: dom
, (EQ :|| Type) :<: dom
, (ORD :|| Type) :<: dom
, OptimizeSuper dom
)
=> Optimize (Logic :|| Type) dom
where
constructFeatOpt (C' And) (a :* b :* Nil)
| Just True <- viewLiteral a = return b
| Just False <- viewLiteral a = return a
| Just True <- viewLiteral b = return a
| Just False <- viewLiteral b = return b
| a `alphaEq` b = return a
constructFeatOpt (C' Or) (a :* b :* Nil)
| Just True <- viewLiteral a = return a
| Just False <- viewLiteral a = return b
| Just True <- viewLiteral b = return b
| Just False <- viewLiteral b = return a
| a `alphaEq` b = return a
constructFeatOpt (C' Not) ((op :$ a) :* Nil)
| Just (C' Not) <- prjF op = return a
constructFeatOpt (C' Not) ((op :$ a :$ b) :* Nil)
| Just (C' Equal) <- prjF op = constructFeat (c' NotEqual) (a :* b :* Nil)
| Just (C' NotEqual) <- prjF op = constructFeat (c' Equal) (a :* b :* Nil)
| Just (C' LTH) <- prjF op = constructFeat (c' GTE) (a :* b :* Nil)
| Just (C' GTH) <- prjF op = constructFeat (c' LTE) (a :* b :* Nil)
| Just (C' LTE) <- prjF op = constructFeat (c' GTH) (a :* b :* Nil)
| Just (C' GTE) <- prjF op = constructFeat (c' LTH) (a :* b :* Nil)
constructFeatOpt a args = constructFeatUnOpt a args
constructFeatUnOpt x@(C' _) = constructFeatUnOptDefault x