{-# LANGUAGE OverloadedStrings #-}
module Language.While.Syntax.Sugar where
import Data.SBV (AlgReal)
import Data.Vinyl.Curry
import Language.Expression
import Language.Expression.GeneralOp
import Language.Expression.Util
import Language.While.Hoare
import Language.While.Syntax
infix 1 .=.
infixr 0 \\
infix 3 ^^^
infix 8 .<
infix 8 .<=
infix 8 .>
infix 8 .>=
infixr 7 .&&
infixr 6 .||
(.=.) :: l -> WhileExpr l AlgReal -> Command l a
(.=.) = CAssign
(\\) :: Command l a -> Command l a -> Command l a
(\\) = CSeq
(^^^) :: WhileProp l Bool -> AnnCommand l () -> AnnCommand l ()
prop ^^^ command = CAnn (PropAnn prop ()) command
(.==) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
(.==) = HWrap ... rcurry (Op OpEq)
(.<) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
(.<) = HWrap ... rcurry (Op OpLT)
(.>) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
(.>) = HWrap ... rcurry (Op OpGT)
(.<=) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
(.<=) = HWrap ... rcurry (Op OpLE)
(.>=) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
(.>=) = HWrap ... rcurry (Op OpGE)
(.&&) :: WhileExpr l Bool -> WhileExpr l Bool -> WhileExpr l Bool
(.&&) = HWrap ... rcurry (Op OpAnd)
(.||) :: WhileExpr l Bool -> WhileExpr l Bool -> WhileExpr l Bool
(.||) = HWrap ... rcurry (Op OpOr)
wenot :: WhileExpr l Bool -> WhileExpr l Bool
wenot = HWrap . rcurry (Op OpNot)