{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE DeriveTraversable     #-} 
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeSynonymInstances  #-}


module Language.While.Syntax where

import           Data.String                     (IsString (..))
import           Data.Typeable                   ((:~:) (..))

import           Data.SBV
import           Data.SBV.Internals              (SBV (..))
import           Data.Vinyl                      (Rec (RNil))
import           Data.Vinyl.Curry

import           Control.Lens                    hiding ((...), (.>))
import           Control.Monad.State
import           Data.Map                        (Map)
import qualified Data.Map                        as Map

import           Language.Expression
import           Language.Expression.GeneralOp
import           Language.Expression.Pretty
import           Language.Expression.Util
import           Language.Verification

--------------------------------------------------------------------------------
--  Operator kind
--------------------------------------------------------------------------------

data WhileOpKind as r where
  OpLit                        :: AlgReal -> WhileOpKind '[]      AlgReal
  OpAdd, OpSub, OpMul          :: WhileOpKind '[AlgReal, AlgReal] AlgReal
  OpEq, OpLT, OpLE, OpGT, OpGE :: WhileOpKind '[AlgReal, AlgReal] Bool
  OpAnd, OpOr                  :: WhileOpKind '[Bool   , Bool]    Bool
  OpNot                        :: WhileOpKind '[Bool]             Bool


instance EvalOpAt Identity WhileOpKind where

  evalMany :: WhileOpKind as r -> Rec Identity as -> Identity r
evalMany = \case
    OpLit AlgReal
x -> \Rec Identity as
_ -> AlgReal -> Identity AlgReal
forall (f :: * -> *) a. Applicative f => a -> f a
pure AlgReal
x

    WhileOpKind as r
OpAdd -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' Curried as r
forall a. Num a => a -> a -> a
(+)
    WhileOpKind as r
OpSub -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' (-)
    WhileOpKind as r
OpMul -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' Curried as r
forall a. Num a => a -> a -> a
(*)

    WhileOpKind as r
OpEq -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' Curried as r
forall a. Eq a => a -> a -> Bool
(==)
    WhileOpKind as r
OpLT -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' Curried as r
forall a. Ord a => a -> a -> Bool
(<)
    WhileOpKind as r
OpLE -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' Curried as r
forall a. Ord a => a -> a -> Bool
(<=)
    WhileOpKind as r
OpGT -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' Curried as r
forall a. Ord a => a -> a -> Bool
(>)
    WhileOpKind as r
OpGE -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' Curried as r
forall a. Ord a => a -> a -> Bool
(>=)

    WhileOpKind as r
OpAnd -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' Curried as r
Bool -> Bool -> Bool
(&&)
    WhileOpKind as r
OpOr  -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' Curried as r
Bool -> Bool -> Bool
(||)

    WhileOpKind as r
OpNot -> Curried as r -> Rec Identity as -> Identity r
forall (f :: * -> *) (ts :: [*]) a.
Applicative f =>
Curried ts a -> Rec f ts -> f a
runcurryA' Curried as r
Bool -> Bool
not

instance EvalOpAt SBV WhileOpKind where
  evalMany :: WhileOpKind as r -> Rec SBV as -> SBV r
evalMany = \case
    OpLit AlgReal
x -> \Rec SBV as
_ -> AlgReal -> SBV AlgReal
forall a. SymVal a => a -> SBV a
literal AlgReal
x

    WhileOpKind as r
OpAdd -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF SBV as (SBV r)
forall a. Num a => a -> a -> a
(+)
    WhileOpKind as r
OpSub -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry (-)
    WhileOpKind as r
OpMul -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF SBV as (SBV r)
forall a. Num a => a -> a -> a
(*)

    WhileOpKind as r
OpEq -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF SBV as (SBV r)
forall a. EqSymbolic a => a -> a -> SBool
(.==)
    WhileOpKind as r
OpLT -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF SBV as (SBV r)
forall a. OrdSymbolic a => a -> a -> SBool
(.<)
    WhileOpKind as r
OpLE -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF SBV as (SBV r)
forall a. OrdSymbolic a => a -> a -> SBool
(.<=)
    WhileOpKind as r
OpGT -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF SBV as (SBV r)
forall a. OrdSymbolic a => a -> a -> SBool
(.>)
    WhileOpKind as r
OpGE -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF SBV as (SBV r)
forall a. OrdSymbolic a => a -> a -> SBool
(.>=)

    WhileOpKind as r
OpAnd -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF SBV as (SBV r)
SBool -> SBool -> SBool
(.&&)
    WhileOpKind as r
OpOr -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF SBV as (SBV r)
SBool -> SBool -> SBool
(.||)

    WhileOpKind as r
OpNot -> CurriedF SBV as (SBV r) -> Rec SBV as -> SBV r
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry CurriedF SBV as (SBV r)
SBool -> SBool
sNot

-- instance EqOpMany WhileOpKind where
--   liftEqMany (OpLit x) (OpLit y) _ = \_ _ -> x == y
--   liftEqMany OpAdd OpAdd k = k
--   liftEqMany OpSub OpSub k = k
--   liftEqMany OpMul OpMul k = k
--   liftEqMany OpEq  OpEq  k = k
--   liftEqMany OpLT  OpLT  k = k
--   liftEqMany OpLE  OpLE  k = k
--   liftEqMany OpGT  OpGT  k = k
--   liftEqMany OpGE  OpGE  k = k
--   liftEqMany OpAnd OpAnd k = k
--   liftEqMany OpOr  OpOr  k = k
--   liftEqMany OpNot OpNot k = k
--   liftEqMany _ _ _ = \_ _ -> False

prettys1Binop ::
  (Pretty1 t) =>
  Int -> String -> (Int -> t a -> t b -> ShowS)
prettys1Binop :: Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
prec String
opStr = \Int
p t a
x t b
y ->
  Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> t a -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec (Int
prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) t a
x
                       ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
opStr
                       ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t b -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec (Int
prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) t b
y

instance PrettyOp WhileOpKind where
  prettysPrecOp :: Int -> WhileOpKind as a -> Rec t as -> ShowS
prettysPrecOp = (WhileOpKind as a -> Int -> Rec t as -> ShowS)
-> Int -> WhileOpKind as a -> Rec t as -> ShowS
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((WhileOpKind as a -> Int -> Rec t as -> ShowS)
 -> Int -> WhileOpKind as a -> Rec t as -> ShowS)
-> (WhileOpKind as a -> Int -> Rec t as -> ShowS)
-> Int
-> WhileOpKind as a
-> Rec t as
-> ShowS
forall a b. (a -> b) -> a -> b
$ \case
    WhileOpKind as a
OpAdd -> (t AlgReal -> t AlgReal -> ShowS)
-> Rec t '[AlgReal, AlgReal] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry ((t AlgReal -> t AlgReal -> ShowS)
 -> Rec t '[AlgReal, AlgReal] -> ShowS)
-> (Int -> t AlgReal -> t AlgReal -> ShowS)
-> Int
-> Rec t '[AlgReal, AlgReal]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> Int -> t AlgReal -> t AlgReal -> ShowS
forall (t :: * -> *) a b.
Pretty1 t =>
Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
5 String
" + "
    WhileOpKind as a
OpSub -> (t AlgReal -> t AlgReal -> ShowS)
-> Rec t '[AlgReal, AlgReal] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry ((t AlgReal -> t AlgReal -> ShowS)
 -> Rec t '[AlgReal, AlgReal] -> ShowS)
-> (Int -> t AlgReal -> t AlgReal -> ShowS)
-> Int
-> Rec t '[AlgReal, AlgReal]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> Int -> t AlgReal -> t AlgReal -> ShowS
forall (t :: * -> *) a b.
Pretty1 t =>
Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
5 String
" - "
    WhileOpKind as a
OpMul -> (t AlgReal -> t AlgReal -> ShowS)
-> Rec t '[AlgReal, AlgReal] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry ((t AlgReal -> t AlgReal -> ShowS)
 -> Rec t '[AlgReal, AlgReal] -> ShowS)
-> (Int -> t AlgReal -> t AlgReal -> ShowS)
-> Int
-> Rec t '[AlgReal, AlgReal]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> Int -> t AlgReal -> t AlgReal -> ShowS
forall (t :: * -> *) a b.
Pretty1 t =>
Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
6 String
" * "

    WhileOpKind as a
OpEq -> (t AlgReal -> t AlgReal -> ShowS)
-> Rec t '[AlgReal, AlgReal] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry ((t AlgReal -> t AlgReal -> ShowS)
 -> Rec t '[AlgReal, AlgReal] -> ShowS)
-> (Int -> t AlgReal -> t AlgReal -> ShowS)
-> Int
-> Rec t '[AlgReal, AlgReal]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> Int -> t AlgReal -> t AlgReal -> ShowS
forall (t :: * -> *) a b.
Pretty1 t =>
Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
4 String
" = "

    WhileOpKind as a
OpLT -> (t AlgReal -> t AlgReal -> ShowS)
-> Rec t '[AlgReal, AlgReal] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry ((t AlgReal -> t AlgReal -> ShowS)
 -> Rec t '[AlgReal, AlgReal] -> ShowS)
-> (Int -> t AlgReal -> t AlgReal -> ShowS)
-> Int
-> Rec t '[AlgReal, AlgReal]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> Int -> t AlgReal -> t AlgReal -> ShowS
forall (t :: * -> *) a b.
Pretty1 t =>
Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
4 String
" < "
    WhileOpKind as a
OpLE -> (t AlgReal -> t AlgReal -> ShowS)
-> Rec t '[AlgReal, AlgReal] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry ((t AlgReal -> t AlgReal -> ShowS)
 -> Rec t '[AlgReal, AlgReal] -> ShowS)
-> (Int -> t AlgReal -> t AlgReal -> ShowS)
-> Int
-> Rec t '[AlgReal, AlgReal]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> Int -> t AlgReal -> t AlgReal -> ShowS
forall (t :: * -> *) a b.
Pretty1 t =>
Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
4 String
" <= "
    WhileOpKind as a
OpGT -> (t AlgReal -> t AlgReal -> ShowS)
-> Rec t '[AlgReal, AlgReal] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry ((t AlgReal -> t AlgReal -> ShowS)
 -> Rec t '[AlgReal, AlgReal] -> ShowS)
-> (Int -> t AlgReal -> t AlgReal -> ShowS)
-> Int
-> Rec t '[AlgReal, AlgReal]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> Int -> t AlgReal -> t AlgReal -> ShowS
forall (t :: * -> *) a b.
Pretty1 t =>
Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
4 String
" > "
    WhileOpKind as a
OpGE -> (t AlgReal -> t AlgReal -> ShowS)
-> Rec t '[AlgReal, AlgReal] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry ((t AlgReal -> t AlgReal -> ShowS)
 -> Rec t '[AlgReal, AlgReal] -> ShowS)
-> (Int -> t AlgReal -> t AlgReal -> ShowS)
-> Int
-> Rec t '[AlgReal, AlgReal]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> Int -> t AlgReal -> t AlgReal -> ShowS
forall (t :: * -> *) a b.
Pretty1 t =>
Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
4 String
" >= "

    WhileOpKind as a
OpNot ->
      \Int
p ->
        CurriedF t '[Bool] ShowS -> Rec t '[Bool] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry (CurriedF t '[Bool] ShowS -> Rec t '[Bool] -> ShowS)
-> CurriedF t '[Bool] ShowS -> Rec t '[Bool] -> ShowS
forall a b. (a -> b) -> a -> b
$ \t Bool
x -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
8) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"! " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t Bool -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
9 t Bool
x
    WhileOpKind as a
OpAnd -> (t Bool -> t Bool -> ShowS) -> Rec t '[Bool, Bool] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry ((t Bool -> t Bool -> ShowS) -> Rec t '[Bool, Bool] -> ShowS)
-> (Int -> t Bool -> t Bool -> ShowS)
-> Int
-> Rec t '[Bool, Bool]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> Int -> t Bool -> t Bool -> ShowS
forall (t :: * -> *) a b.
Pretty1 t =>
Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
3 String
" && "
    WhileOpKind as a
OpOr -> (t Bool -> t Bool -> ShowS) -> Rec t '[Bool, Bool] -> ShowS
forall u (f :: u -> *) (ts :: [u]) a.
CurriedF f ts a -> Rec f ts -> a
runcurry ((t Bool -> t Bool -> ShowS) -> Rec t '[Bool, Bool] -> ShowS)
-> (Int -> t Bool -> t Bool -> ShowS)
-> Int
-> Rec t '[Bool, Bool]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> Int -> t Bool -> t Bool -> ShowS
forall (t :: * -> *) a b.
Pretty1 t =>
Int -> String -> Int -> t a -> t b -> ShowS
prettys1Binop Int
2 String
" || "

    OpLit AlgReal
x -> \Int
_ Rec t '[]
_ -> AlgReal -> ShowS
forall a. Show a => a -> ShowS
shows AlgReal
x

--------------------------------------------------------------------------------
--  Operators
--------------------------------------------------------------------------------

type WhileOp = GeneralOp WhileOpKind

--------------------------------------------------------------------------------
--  Variables
--------------------------------------------------------------------------------

data WhileVar l a where
  WhileVar :: l -> WhileVar l AlgReal

instance Pretty l => Pretty1 (WhileVar l) where
  pretty1 :: WhileVar l a -> String
pretty1 (WhileVar l
l) = l -> String
forall a. Pretty a => a -> String
pretty l
l

instance VerifiableVar (WhileVar String) where
  type VarKey (WhileVar String) = String
  type VarSym (WhileVar String) = SBV
  type VarEnv (WhileVar String) = ()
 
  symForVar :: WhileVar String a
-> VarEnv (WhileVar String)
-> Symbolic (VarSym (WhileVar String) a)
symForVar (WhileVar String
x) = Symbolic (SBV AlgReal) -> () -> Symbolic (SBV AlgReal)
forall a b. a -> b -> a
const (Symbolic (SBV AlgReal) -> () -> Symbolic (SBV AlgReal))
-> Symbolic (SBV AlgReal) -> () -> Symbolic (SBV AlgReal)
forall a b. (a -> b) -> a -> b
$ String -> Symbolic (SBV AlgReal)
forall a. SymVal a => String -> Symbolic (SBV a)
symbolic String
x
  varKey :: WhileVar String a -> VarKey (WhileVar String)
varKey (WhileVar String
x) = String
VarKey (WhileVar String)
x
  eqVarTypes :: WhileVar String a -> WhileVar String b -> Maybe (a :~: b)
eqVarTypes (WhileVar String
_) (WhileVar String
_) = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
  castVarSym :: WhileVar String a
-> VarSym (WhileVar String) b -> Maybe (VarSym (WhileVar String) a)
castVarSym (WhileVar String
_) (SBV x) = SBV AlgReal -> Maybe (SBV AlgReal)
forall a. a -> Maybe a
Just (SVal -> SBV AlgReal
forall a. SVal -> SBV a
SBV SVal
x)

--------------------------------------------------------------------------------
--  Expressions
--------------------------------------------------------------------------------

type WhileExpr l = HFree WhileOp (WhileVar l)

instance Num (WhileExpr l AlgReal) where
  fromInteger :: Integer -> WhileExpr l AlgReal
fromInteger Integer
x = GeneralOp
  WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
-> WhileExpr l AlgReal
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (WhileOpKind '[] AlgReal
-> Rec (HFree (GeneralOp WhileOpKind) (WhileVar l)) '[]
-> GeneralOp
     WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
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 (AlgReal -> WhileOpKind '[] AlgReal
OpLit (Integer -> AlgReal
forall a. Num a => Integer -> a
fromInteger Integer
x)) Rec (HFree (GeneralOp WhileOpKind) (WhileVar l)) '[]
forall u (a :: u -> *). Rec a '[]
RNil)

  + :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal
(+) = GeneralOp
  WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
-> WhileExpr l AlgReal
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (GeneralOp
   WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
 -> WhileExpr l AlgReal)
-> (WhileExpr l AlgReal
    -> WhileExpr l AlgReal
    -> GeneralOp
         WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal)
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... (Rec
   (HFree (GeneralOp WhileOpKind) (WhileVar l)) '[AlgReal, AlgReal]
 -> GeneralOp
      WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal)
-> CurriedF
     (HFree (GeneralOp WhileOpKind) (WhileVar l))
     '[AlgReal, AlgReal]
     (GeneralOp
        WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal)
forall u (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[AlgReal, AlgReal] AlgReal
-> Rec
     (HFree (GeneralOp WhileOpKind) (WhileVar l)) '[AlgReal, AlgReal]
-> GeneralOp
     WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
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] AlgReal
OpAdd)
  * :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal
(*) = GeneralOp
  WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
-> WhileExpr l AlgReal
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (GeneralOp
   WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
 -> WhileExpr l AlgReal)
-> (WhileExpr l AlgReal
    -> WhileExpr l AlgReal
    -> GeneralOp
         WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal)
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... (Rec
   (HFree (GeneralOp WhileOpKind) (WhileVar l)) '[AlgReal, AlgReal]
 -> GeneralOp
      WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal)
-> CurriedF
     (HFree (GeneralOp WhileOpKind) (WhileVar l))
     '[AlgReal, AlgReal]
     (GeneralOp
        WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal)
forall u (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[AlgReal, AlgReal] AlgReal
-> Rec
     (HFree (GeneralOp WhileOpKind) (WhileVar l)) '[AlgReal, AlgReal]
-> GeneralOp
     WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
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] AlgReal
OpMul)
  (-) = GeneralOp
  WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
-> WhileExpr l AlgReal
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (GeneralOp
   WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
 -> WhileExpr l AlgReal)
-> (WhileExpr l AlgReal
    -> WhileExpr l AlgReal
    -> GeneralOp
         WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal)
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
-> WhileExpr l AlgReal
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
... (Rec
   (HFree (GeneralOp WhileOpKind) (WhileVar l)) '[AlgReal, AlgReal]
 -> GeneralOp
      WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal)
-> CurriedF
     (HFree (GeneralOp WhileOpKind) (WhileVar l))
     '[AlgReal, AlgReal]
     (GeneralOp
        WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal)
forall u (ts :: [u]) (f :: u -> *) a.
RecordCurry ts =>
(Rec f ts -> a) -> CurriedF f ts a
rcurry (WhileOpKind '[AlgReal, AlgReal] AlgReal
-> Rec
     (HFree (GeneralOp WhileOpKind) (WhileVar l)) '[AlgReal, AlgReal]
-> GeneralOp
     WhileOpKind (HFree (GeneralOp WhileOpKind) (WhileVar l)) AlgReal
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] AlgReal
OpSub)
  abs :: WhileExpr l AlgReal -> WhileExpr l AlgReal
abs = String -> WhileExpr l AlgReal -> WhileExpr l AlgReal
forall a. HasCallStack => String -> a
error String
"can't take abs of expressions"
  signum :: WhileExpr l AlgReal -> WhileExpr l AlgReal
signum = String -> WhileExpr l AlgReal -> WhileExpr l AlgReal
forall a. HasCallStack => String -> a
error String
"can't take signum of expressions"

instance IsString s => IsString (WhileExpr s AlgReal) where
  fromString :: String -> WhileExpr s AlgReal
fromString = WhileVar s AlgReal -> WhileExpr s AlgReal
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
t a -> HFree h t a
HPure (WhileVar s AlgReal -> WhileExpr s AlgReal)
-> (String -> WhileVar s AlgReal) -> String -> WhileExpr s AlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> WhileVar s AlgReal
forall l. l -> WhileVar l AlgReal
WhileVar (s -> WhileVar s AlgReal)
-> (String -> s) -> String -> WhileVar s AlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> s
forall a. IsString a => String -> a
fromString

--------------------------------------------------------------------------------
--  Commands
--------------------------------------------------------------------------------

data Command l a
  = CAnn a (Command l a)
  | CSeq (Command l a) (Command l a)
  | CSkip
  | CAssign l (WhileExpr l AlgReal)
  | CIf (WhileExpr l Bool) (Command l a) (Command l a)
  | CWhile (WhileExpr l Bool) (Command l a)

instance (Pretty l, Pretty a) => Pretty (Command l a) where
  prettysPrec :: Int -> Command l a -> ShowS
prettysPrec Int
p = \case
    CAnn a
ann Command l a
c ->
      Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"{ "
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ShowS
forall a. Pretty a => a -> ShowS
prettys a
ann
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" }\n"
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Command l a -> ShowS
forall a. Pretty a => a -> ShowS
prettys Command l a
c
    CSeq Command l a
c1 Command l a
c2 ->
      Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Command l a -> ShowS
forall a. Pretty a => a -> ShowS
prettys Command l a
c1 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
";\n" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Command l a -> ShowS
forall a. Pretty a => a -> ShowS
prettys Command l a
c2
    Command l a
CSkip -> String -> ShowS
showString String
"()"
    CAssign l
v WhileExpr l AlgReal
e ->
      Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ l -> ShowS
forall a. Pretty a => a -> ShowS
prettys l
v ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" := " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WhileExpr l AlgReal -> ShowS
forall a. Pretty a => a -> ShowS
prettys WhileExpr l AlgReal
e
    CIf WhileExpr l Bool
cond Command l a
c1 Command l a
c2 ->
      Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"if "
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> WhileExpr l Bool -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
11 WhileExpr l Bool
cond
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" then\n"
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Command l a -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
11 Command l a
c1
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"\nelse\n"
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Command l a -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
11 Command l a
c2
    CWhile WhileExpr l Bool
cond Command l a
body ->
      Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"while "
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> WhileExpr l Bool -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
11 WhileExpr l Bool
cond
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" do\n"
                         ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Command l a -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
11 Command l a
body

--------------------------------------------------------------------------------
--  Running Commands
--------------------------------------------------------------------------------

data StepResult a
  = Terminated
  | Failed
  | Progress a
  deriving (a -> StepResult b -> StepResult a
(a -> b) -> StepResult a -> StepResult b
(forall a b. (a -> b) -> StepResult a -> StepResult b)
-> (forall a b. a -> StepResult b -> StepResult a)
-> Functor StepResult
forall a b. a -> StepResult b -> StepResult a
forall a b. (a -> b) -> StepResult a -> StepResult b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> StepResult b -> StepResult a
$c<$ :: forall a b. a -> StepResult b -> StepResult a
fmap :: (a -> b) -> StepResult a -> StepResult b
$cfmap :: forall a b. (a -> b) -> StepResult a -> StepResult b
Functor)

evalWhileExpr
  :: (Applicative f)
  => (forall x. WhileVar l x -> f x)
  -> WhileExpr l a -> f a
evalWhileExpr :: (forall x. WhileVar l x -> f x) -> WhileExpr l a -> f a
evalWhileExpr forall x. WhileVar l x -> f x
f
  = (Identity a -> a) -> f (Identity a) -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Identity a -> a
forall a. Identity a -> a
runIdentity
  (f (Identity a) -> f a)
-> (WhileExpr l a -> f (Identity a)) -> WhileExpr l a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall b. WhileVar l b -> f (Identity b))
-> WhileExpr l a -> f (Identity a)
forall u (k :: u -> *) (h :: (u -> *) -> u -> *) (f :: * -> *)
       (t :: u -> *) (a :: u).
(HFoldableAt k h, HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (k b)) -> h t a -> f (k a)
hfoldTraverse ((b -> Identity b) -> f b -> f (Identity b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Identity b
forall a. a -> Identity a
Identity (f b -> f (Identity b))
-> (WhileVar l b -> f b) -> WhileVar l b -> f (Identity b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WhileVar l b -> f b
forall x. WhileVar l x -> f x
f)

oneStep
  :: (Ord l)
  => Command l a
  -> State (Map l AlgReal) (StepResult (Command l a))
oneStep :: Command l a -> State (Map l AlgReal) (StepResult (Command l a))
oneStep = \case
  CAnn a
ann Command l a
c -> (Command l a -> Command l a)
-> StepResult (Command l a) -> StepResult (Command l a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> Command l a -> Command l a
forall l a. a -> Command l a -> Command l a
CAnn a
ann) (StepResult (Command l a) -> StepResult (Command l a))
-> State (Map l AlgReal) (StepResult (Command l a))
-> State (Map l AlgReal) (StepResult (Command l a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Command l a -> State (Map l AlgReal) (StepResult (Command l a))
forall l a.
Ord l =>
Command l a -> State (Map l AlgReal) (StepResult (Command l a))
oneStep Command l a
c

  CSeq Command l a
c1 Command l a
c2 ->
    do StepResult (Command l a)
s <- Command l a -> State (Map l AlgReal) (StepResult (Command l a))
forall l a.
Ord l =>
Command l a -> State (Map l AlgReal) (StepResult (Command l a))
oneStep Command l a
c1
       case StepResult (Command l a)
s of
         StepResult (Command l a)
Terminated -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Command l a -> StepResult (Command l a)
forall a. a -> StepResult a
Progress Command l a
c2)
         StepResult (Command l a)
Failed -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return StepResult (Command l a)
forall a. StepResult a
Failed
         Progress Command l a
c1' -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Command l a -> StepResult (Command l a)
forall a. a -> StepResult a
Progress (Command l a
c1' Command l a -> Command l a -> Command l a
forall l a. Command l a -> Command l a -> Command l a
`CSeq` Command l a
c2))

  Command l a
CSkip -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return StepResult (Command l a)
forall a. StepResult a
Terminated

  CAssign l
loc WhileExpr l AlgReal
expr ->
    do Map l AlgReal
env <- StateT (Map l AlgReal) Identity (Map l AlgReal)
forall s (m :: * -> *). MonadState s m => m s
get
       if l -> Map l AlgReal -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member l
loc Map l AlgReal
env then
         case (forall x. WhileVar l x -> Maybe x)
-> WhileExpr l AlgReal -> Maybe AlgReal
forall (f :: * -> *) l a.
Applicative f =>
(forall x. WhileVar l x -> f x) -> WhileExpr l a -> f a
evalWhileExpr (Map l AlgReal -> WhileVar l x -> Maybe x
forall l a. Ord l => Map l AlgReal -> WhileVar l a -> Maybe a
lookupVar Map l AlgReal
env) WhileExpr l AlgReal
expr of
           Just AlgReal
val ->
             do Index (Map l AlgReal)
-> Lens' (Map l AlgReal) (Maybe (IxValue (Map l AlgReal)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at l
Index (Map l AlgReal)
loc ((Maybe AlgReal -> Identity (Maybe AlgReal))
 -> Map l AlgReal -> Identity (Map l AlgReal))
-> Maybe AlgReal -> StateT (Map l AlgReal) Identity ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= AlgReal -> Maybe AlgReal
forall a. a -> Maybe a
Just AlgReal
val
                StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return StepResult (Command l a)
forall a. StepResult a
Terminated
           Maybe AlgReal
Nothing -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return StepResult (Command l a)
forall a. StepResult a
Failed
         -- Can't assign a memory location that doesn't exist
         else StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return StepResult (Command l a)
forall a. StepResult a
Failed

  CIf WhileExpr l Bool
cond Command l a
c1 Command l a
c2 ->
    do Map l AlgReal
env <- StateT (Map l AlgReal) Identity (Map l AlgReal)
forall s (m :: * -> *). MonadState s m => m s
get
       case (forall x. WhileVar l x -> Maybe x)
-> WhileExpr l Bool -> Maybe Bool
forall (f :: * -> *) l a.
Applicative f =>
(forall x. WhileVar l x -> f x) -> WhileExpr l a -> f a
evalWhileExpr (Map l AlgReal -> WhileVar l x -> Maybe x
forall l a. Ord l => Map l AlgReal -> WhileVar l a -> Maybe a
lookupVar Map l AlgReal
env) WhileExpr l Bool
cond of
         Just Bool
True -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Command l a -> StepResult (Command l a)
forall a. a -> StepResult a
Progress Command l a
c1)
         Just Bool
False -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Command l a -> StepResult (Command l a)
forall a. a -> StepResult a
Progress Command l a
c2)
         Maybe Bool
_ -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return StepResult (Command l a)
forall a. StepResult a
Failed

  CWhile WhileExpr l Bool
cond Command l a
body ->
    do Map l AlgReal
env <- StateT (Map l AlgReal) Identity (Map l AlgReal)
forall s (m :: * -> *). MonadState s m => m s
get
       case (forall x. WhileVar l x -> Maybe x)
-> WhileExpr l Bool -> Maybe Bool
forall (f :: * -> *) l a.
Applicative f =>
(forall x. WhileVar l x -> f x) -> WhileExpr l a -> f a
evalWhileExpr (Map l AlgReal -> WhileVar l x -> Maybe x
forall l a. Ord l => Map l AlgReal -> WhileVar l a -> Maybe a
lookupVar Map l AlgReal
env) WhileExpr l Bool
cond of
         Just Bool
True -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Command l a -> StepResult (Command l a)
forall a. a -> StepResult a
Progress (Command l a
body Command l a -> Command l a -> Command l a
forall l a. Command l a -> Command l a -> Command l a
`CSeq` (WhileExpr l Bool -> Command l a -> Command l a
forall l a. WhileExpr l Bool -> Command l a -> Command l a
CWhile WhileExpr l Bool
cond Command l a
body)))
         Just Bool
False -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return StepResult (Command l a)
forall a. StepResult a
Terminated
         Maybe Bool
_ -> StepResult (Command l a)
-> State (Map l AlgReal) (StepResult (Command l a))
forall (m :: * -> *) a. Monad m => a -> m a
return StepResult (Command l a)
forall a. StepResult a
Failed


runCommand :: (Ord l) => Command l a -> State (Map l AlgReal) Bool
runCommand :: Command l a -> State (Map l AlgReal) Bool
runCommand Command l a
command =
  do StepResult (Command l a)
s <- Command l a -> State (Map l AlgReal) (StepResult (Command l a))
forall l a.
Ord l =>
Command l a -> State (Map l AlgReal) (StepResult (Command l a))
oneStep Command l a
command
     case StepResult (Command l a)
s of
       StepResult (Command l a)
Terminated -> Bool -> State (Map l AlgReal) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       StepResult (Command l a)
Failed -> Bool -> State (Map l AlgReal) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
       Progress Command l a
command' -> Command l a -> State (Map l AlgReal) Bool
forall l a. Ord l => Command l a -> State (Map l AlgReal) Bool
runCommand Command l a
command'

--------------------------------------------------------------------------------
--  Combinators
--------------------------------------------------------------------------------

lookupVar :: (Ord l) => Map l AlgReal -> WhileVar l a -> Maybe a
lookupVar :: Map l AlgReal -> WhileVar l a -> Maybe a
lookupVar Map l AlgReal
env (WhileVar l
s) = l -> Map l AlgReal -> Maybe AlgReal
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup l
s Map l AlgReal
env