Skip to content

Commit

Permalink
Symbolic mut vars partially work
Browse files Browse the repository at this point in the history
  • Loading branch information
Bill Hallahan committed Jul 31, 2024
1 parent 2be453a commit 318aa17
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions src/G2/Execution/PrimitiveEval.hs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ import qualified Data.HashMap.Lazy as M
import qualified Data.List as L
import Data.Maybe
import qualified G2.Language.ExprEnv as E
import G2.Language.ExprEnv (deepLookupExpr)

evalPrims :: ASTContainer m Expr => TypeEnv -> KnownValues -> m -> m
evalPrims tenv kv = modifyContainedASTs (evalPrims' tenv kv . simplifyCasts)
Expand Down Expand Up @@ -64,15 +65,17 @@ evalPrimMutVar :: State t -- ^ Context to evaluate expression `e` in
-> Expr -- ^ The expression `e` to evaluate
-> Maybe (State t, NameGen) -- ^ `Just` if `e` is a primitive operation on mutable variable, `Nothing` otherwise
evalPrimMutVar s ng (App (App (App (App (Prim NewMutVar _) (Type t)) (Type ts)) e) _) = Just $ newMutVar s ng ts t e
evalPrimMutVar s ng (App (App (App (App (Prim ReadMutVar _) _) _) (Prim (MutVar mv) _)) _) =
evalPrimMutVar s ng (App (App (App (App (Prim ReadMutVar _) _) _) mv_e) _)
| Just (Prim (MutVar mv) _) <- deepLookupExpr mv_e (expr_env s)=
let
i = M.lookup mv (mutvar_env s)
s' = maybe (error "evalPrimMutVar: MutVar not found")
(\i' -> s { curr_expr = CurrExpr Evaluate (Var i') })
i
in
Just (s', ng)
evalPrimMutVar s ng (App (App (App (App (App (Prim WriteMutVar _) _) (Type t)) (Prim (MutVar mv) _)) e) pr_s) =
evalPrimMutVar s ng (App (App (App (App (App (Prim WriteMutVar _) _) (Type t)) mv_e) e) pr_s)
| Just (Prim (MutVar mv) _) <- deepLookupExpr mv_e (expr_env s) =
let
(i, ng') = freshId t ng
s' = s { expr_env = E.insert (idName i) e (expr_env s)
Expand Down

0 comments on commit 318aa17

Please sign in to comment.