{-# 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
.=. :: forall l a. l -> WhileExpr l AlgReal -> Command l a
(.=.) = l -> WhileExpr l AlgReal -> Command l a
forall l a. l -> WhileExpr l AlgReal -> Command l a
CAssign

(\\) :: Command l a -> Command l a -> Command l a
\\ :: forall l a. Command l a -> Command l a -> Command l a
(\\) = Command l a -> Command l a -> Command l a
forall l a. Command l a -> Command l a -> Command l a
CSeq

(^^^) :: WhileProp l Bool -> AnnCommand l () -> AnnCommand l ()
WhileProp l Bool
prop ^^^ :: forall l. WhileProp l Bool -> AnnCommand l () -> AnnCommand l ()
^^^ AnnCommand l ()
command = PropAnn l () -> AnnCommand l () -> AnnCommand l ()
forall l a. a -> Command l a -> Command l a
CAnn (WhileProp l Bool -> () -> PropAnn l ()
forall l a. WhileProp l Bool -> a -> PropAnn l a
PropAnn WhileProp l Bool
prop ()) AnnCommand l ()
command

(.==) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.== :: forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
(.==) = WhileOp (HFree WhileOp (WhileVar l)) Bool
-> HFree WhileOp (WhileVar l) Bool
forall {k} (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (WhileOp (HFree WhileOp (WhileVar l)) Bool
 -> HFree WhileOp (WhileVar l) Bool)
-> (WhileExpr l AlgReal
    -> WhileExpr l AlgReal
    -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
-> HFree WhileOp (WhileVar l) Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... (Rec (HFree WhileOp (WhileVar l)) '[AlgReal, AlgReal]
 -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> CurriedF
     (HFree WhileOp (WhileVar l))
     '[AlgReal, AlgReal]
     (WhileOp (HFree WhileOp (WhileVar l)) Bool)
forall {u} (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[AlgReal, AlgReal] Bool
-> Rec (HFree WhileOp (WhileVar l)) '[AlgReal, AlgReal]
-> WhileOp (HFree WhileOp (WhileVar l)) Bool
forall {u} {k} (as :: [u]) (op :: [u] -> k -> *) (r :: k)
       (t :: u -> *).
RMap as =>
op as r -> Rec t as -> GeneralOp op t r
Op WhileOpKind '[AlgReal, AlgReal] Bool
OpEq)

(.<) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.< :: forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
(.<) = WhileOp (HFree WhileOp (WhileVar l)) Bool
-> HFree WhileOp (WhileVar l) Bool
forall {k} (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (WhileOp (HFree WhileOp (WhileVar l)) Bool
 -> HFree WhileOp (WhileVar l) Bool)
-> (WhileExpr l AlgReal
    -> WhileExpr l AlgReal
    -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
-> HFree WhileOp (WhileVar l) Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... (Rec (HFree WhileOp (WhileVar l)) '[AlgReal, AlgReal]
 -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> CurriedF
     (HFree WhileOp (WhileVar l))
     '[AlgReal, AlgReal]
     (WhileOp (HFree WhileOp (WhileVar l)) Bool)
forall {u} (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[AlgReal, AlgReal] Bool
-> Rec (HFree WhileOp (WhileVar l)) '[AlgReal, AlgReal]
-> WhileOp (HFree WhileOp (WhileVar l)) Bool
forall {u} {k} (as :: [u]) (op :: [u] -> k -> *) (r :: k)
       (t :: u -> *).
RMap as =>
op as r -> Rec t as -> GeneralOp op t r
Op WhileOpKind '[AlgReal, AlgReal] Bool
OpLT)

(.>) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.> :: forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
(.>) = WhileOp (HFree WhileOp (WhileVar l)) Bool
-> HFree WhileOp (WhileVar l) Bool
forall {k} (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (WhileOp (HFree WhileOp (WhileVar l)) Bool
 -> HFree WhileOp (WhileVar l) Bool)
-> (WhileExpr l AlgReal
    -> WhileExpr l AlgReal
    -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
-> HFree WhileOp (WhileVar l) Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... (Rec (HFree WhileOp (WhileVar l)) '[AlgReal, AlgReal]
 -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> CurriedF
     (HFree WhileOp (WhileVar l))
     '[AlgReal, AlgReal]
     (WhileOp (HFree WhileOp (WhileVar l)) Bool)
forall {u} (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[AlgReal, AlgReal] Bool
-> Rec (HFree WhileOp (WhileVar l)) '[AlgReal, AlgReal]
-> WhileOp (HFree WhileOp (WhileVar l)) Bool
forall {u} {k} (as :: [u]) (op :: [u] -> k -> *) (r :: k)
       (t :: u -> *).
RMap as =>
op as r -> Rec t as -> GeneralOp op t r
Op WhileOpKind '[AlgReal, AlgReal] Bool
OpGT)

(.<=) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.<= :: forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
(.<=) = WhileOp (HFree WhileOp (WhileVar l)) Bool
-> HFree WhileOp (WhileVar l) Bool
forall {k} (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (WhileOp (HFree WhileOp (WhileVar l)) Bool
 -> HFree WhileOp (WhileVar l) Bool)
-> (WhileExpr l AlgReal
    -> WhileExpr l AlgReal
    -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
-> HFree WhileOp (WhileVar l) Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... (Rec (HFree WhileOp (WhileVar l)) '[AlgReal, AlgReal]
 -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> CurriedF
     (HFree WhileOp (WhileVar l))
     '[AlgReal, AlgReal]
     (WhileOp (HFree WhileOp (WhileVar l)) Bool)
forall {u} (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[AlgReal, AlgReal] Bool
-> Rec (HFree WhileOp (WhileVar l)) '[AlgReal, AlgReal]
-> WhileOp (HFree WhileOp (WhileVar l)) Bool
forall {u} {k} (as :: [u]) (op :: [u] -> k -> *) (r :: k)
       (t :: u -> *).
RMap as =>
op as r -> Rec t as -> GeneralOp op t r
Op WhileOpKind '[AlgReal, AlgReal] Bool
OpLE)

(.>=) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.>= :: forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
(.>=) = WhileOp (HFree WhileOp (WhileVar l)) Bool
-> HFree WhileOp (WhileVar l) Bool
forall {k} (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (WhileOp (HFree WhileOp (WhileVar l)) Bool
 -> HFree WhileOp (WhileVar l) Bool)
-> (WhileExpr l AlgReal
    -> WhileExpr l AlgReal
    -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
-> HFree WhileOp (WhileVar l) Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... (Rec (HFree WhileOp (WhileVar l)) '[AlgReal, AlgReal]
 -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> CurriedF
     (HFree WhileOp (WhileVar l))
     '[AlgReal, AlgReal]
     (WhileOp (HFree WhileOp (WhileVar l)) Bool)
forall {u} (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[AlgReal, AlgReal] Bool
-> Rec (HFree WhileOp (WhileVar l)) '[AlgReal, AlgReal]
-> WhileOp (HFree WhileOp (WhileVar l)) Bool
forall {u} {k} (as :: [u]) (op :: [u] -> k -> *) (r :: k)
       (t :: u -> *).
RMap as =>
op as r -> Rec t as -> GeneralOp op t r
Op WhileOpKind '[AlgReal, AlgReal] Bool
OpGE)

(.&&) :: WhileExpr l Bool -> WhileExpr l Bool -> WhileExpr l Bool
.&& :: forall l. WhileExpr l Bool -> WhileExpr l Bool -> WhileExpr l Bool
(.&&) = WhileOp (HFree WhileOp (WhileVar l)) Bool
-> HFree WhileOp (WhileVar l) Bool
forall {k} (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (WhileOp (HFree WhileOp (WhileVar l)) Bool
 -> HFree WhileOp (WhileVar l) Bool)
-> (HFree WhileOp (WhileVar l) Bool
    -> HFree WhileOp (WhileVar l) Bool
    -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> HFree WhileOp (WhileVar l) Bool
-> HFree WhileOp (WhileVar l) Bool
-> HFree WhileOp (WhileVar l) Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... (Rec (HFree WhileOp (WhileVar l)) '[Bool, Bool]
 -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> CurriedF
     (HFree WhileOp (WhileVar l))
     '[Bool, Bool]
     (WhileOp (HFree WhileOp (WhileVar l)) Bool)
forall {u} (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[Bool, Bool] Bool
-> Rec (HFree WhileOp (WhileVar l)) '[Bool, Bool]
-> WhileOp (HFree WhileOp (WhileVar l)) Bool
forall {u} {k} (as :: [u]) (op :: [u] -> k -> *) (r :: k)
       (t :: u -> *).
RMap as =>
op as r -> Rec t as -> GeneralOp op t r
Op WhileOpKind '[Bool, Bool] Bool
OpAnd)

(.||) :: WhileExpr l Bool -> WhileExpr l Bool -> WhileExpr l Bool
.|| :: forall l. WhileExpr l Bool -> WhileExpr l Bool -> WhileExpr l Bool
(.||) = WhileOp (HFree WhileOp (WhileVar l)) Bool
-> HFree WhileOp (WhileVar l) Bool
forall {k} (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (WhileOp (HFree WhileOp (WhileVar l)) Bool
 -> HFree WhileOp (WhileVar l) Bool)
-> (HFree WhileOp (WhileVar l) Bool
    -> HFree WhileOp (WhileVar l) Bool
    -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> HFree WhileOp (WhileVar l) Bool
-> HFree WhileOp (WhileVar l) Bool
-> HFree WhileOp (WhileVar l) Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... (Rec (HFree WhileOp (WhileVar l)) '[Bool, Bool]
 -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> CurriedF
     (HFree WhileOp (WhileVar l))
     '[Bool, Bool]
     (WhileOp (HFree WhileOp (WhileVar l)) Bool)
forall {u} (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[Bool, Bool] Bool
-> Rec (HFree WhileOp (WhileVar l)) '[Bool, Bool]
-> WhileOp (HFree WhileOp (WhileVar l)) Bool
forall {u} {k} (as :: [u]) (op :: [u] -> k -> *) (r :: k)
       (t :: u -> *).
RMap as =>
op as r -> Rec t as -> GeneralOp op t r
Op WhileOpKind '[Bool, Bool] Bool
OpOr)

wenot :: WhileExpr l Bool -> WhileExpr l Bool
wenot :: forall l. WhileExpr l Bool -> WhileExpr l Bool
wenot = WhileOp (HFree WhileOp (WhileVar l)) Bool
-> HFree WhileOp (WhileVar l) Bool
forall {k} (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (WhileOp (HFree WhileOp (WhileVar l)) Bool
 -> HFree WhileOp (WhileVar l) Bool)
-> (HFree WhileOp (WhileVar l) Bool
    -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> HFree WhileOp (WhileVar l) Bool
-> HFree WhileOp (WhileVar l) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rec (HFree WhileOp (WhileVar l)) '[Bool]
 -> WhileOp (HFree WhileOp (WhileVar l)) Bool)
-> CurriedF
     (HFree WhileOp (WhileVar l))
     '[Bool]
     (WhileOp (HFree WhileOp (WhileVar l)) Bool)
forall {u} (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[Bool] Bool
-> Rec (HFree WhileOp (WhileVar l)) '[Bool]
-> WhileOp (HFree WhileOp (WhileVar l)) Bool
forall {u} {k} (as :: [u]) (op :: [u] -> k -> *) (r :: k)
       (t :: u -> *).
RMap as =>
op as r -> Rec t as -> GeneralOp op t r
Op WhileOpKind '[Bool] Bool
OpNot)