Skip to content

Commit

Permalink
Merge pull request #884 from GaloisInc/eval-intmap
Browse files Browse the repository at this point in the history
Switch evaluation environment from Data.Map to Data.IntMap.
  • Loading branch information
brianhuffman authored Sep 10, 2020
2 parents 8bfad53 + 976ff8f commit 0000ffb
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 20 deletions.
23 changes: 12 additions & 11 deletions src/Cryptol/Eval.hs
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ import Cryptol.Utils.RecordMap
import Control.Monad
import Data.List
import Data.Maybe
import qualified Data.IntMap.Strict as IntMap
import qualified Data.Map.Strict as Map
import Data.Semigroup

Expand Down Expand Up @@ -275,7 +276,7 @@ evalDeclGroup sym env dg = do
-- declare a "hole" for each declaration
-- and extend the evaluation environment
holes <- mapM (declHole sym) ds
let holeEnv = Map.fromList $ [ (nm,h) | (nm,_,h,_) <- holes ]
let holeEnv = IntMap.fromList $ [ (nameUnique nm, h) | (nm,_,h,_) <- holes ]
let env' = env `mappend` emptyEnv{ envVars = holeEnv }

-- evaluate the declaration bodies, building a new evaluation environment
Expand Down Expand Up @@ -643,24 +644,24 @@ evalSetSel sym _tyv e sel v =
-- name is bound to a list of values, one for each element in the list
-- comprehension.
data ListEnv sym = ListEnv
{ leVars :: !(Map.Map Name (Integer -> SEval sym (GenValue sym)))
{ leVars :: !(IntMap.IntMap (Integer -> SEval sym (GenValue sym)))
-- ^ Bindings whose values vary by position
, leStatic :: !(Map.Map Name (SEval sym (GenValue sym)))
, leStatic :: !(IntMap.IntMap (SEval sym (GenValue sym)))
-- ^ Bindings whose values are constant
, leTypes :: !TypeEnv
}

instance Semigroup (ListEnv sym) where
l <> r = ListEnv
{ leVars = Map.union (leVars l) (leVars r)
, leStatic = Map.union (leStatic l) (leStatic r)
{ leVars = IntMap.union (leVars l) (leVars r)
, leStatic = IntMap.union (leStatic l) (leStatic r)
, leTypes = Map.union (leTypes l) (leTypes r)
}

instance Monoid (ListEnv sym) where
mempty = ListEnv
{ leVars = Map.empty
, leStatic = Map.empty
{ leVars = IntMap.empty
, leStatic = IntMap.empty
, leTypes = Map.empty
}

Expand All @@ -681,7 +682,7 @@ toListEnv e =
evalListEnv :: ListEnv sym -> Integer -> GenEvalEnv sym
evalListEnv (ListEnv vm st tm) i =
let v = fmap ($i) vm
in EvalEnv{ envVars = Map.union v st
in EvalEnv{ envVars = IntMap.union v st
, envTypes = tm
}
{-# INLINE evalListEnv #-}
Expand All @@ -692,7 +693,7 @@ bindVarList ::
(Integer -> SEval sym (GenValue sym)) ->
ListEnv sym ->
ListEnv sym
bindVarList n vs lenv = lenv { leVars = Map.insert n vs (leVars lenv) }
bindVarList n vs lenv = lenv { leVars = IntMap.insert (nameUnique n) vs (leVars lenv) }
{-# INLINE bindVarList #-}

-- List Comprehensions ---------------------------------------------------------
Expand Down Expand Up @@ -778,8 +779,8 @@ evalMatch sym lenv m = case m of
-- `leVars` elements of the comprehension environment into `leStatic` elements
-- by selecting out the 0th element.
Inf -> do
let allvars = Map.union (fmap ($0) (leVars lenv)) (leStatic lenv)
let lenv' = lenv { leVars = Map.empty
let allvars = IntMap.union (fmap ($0) (leVars lenv)) (leStatic lenv)
let lenv' = lenv { leVars = IntMap.empty
, leStatic = allvars
}
let env = EvalEnv allvars (leTypes lenv)
Expand Down
19 changes: 10 additions & 9 deletions src/Cryptol/Eval/Env.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ import Cryptol.TypeCheck.Solver.InfNat
import Cryptol.Utils.PP


import qualified Data.IntMap.Strict as IntMap
import qualified Data.Map.Strict as Map
import Data.Semigroup

Expand All @@ -35,29 +36,29 @@ import Prelude.Compat
-- Evaluation Environment ------------------------------------------------------

data GenEvalEnv sym = EvalEnv
{ envVars :: !(Map.Map Name (SEval sym (GenValue sym)))
{ envVars :: !(IntMap.IntMap (SEval sym (GenValue sym)))
, envTypes :: !TypeEnv
} deriving Generic

instance Semigroup (GenEvalEnv sym) where
l <> r = EvalEnv
{ envVars = Map.union (envVars l) (envVars r)
, envTypes = Map.union (envTypes l) (envTypes r)
{ envVars = IntMap.union (envVars l) (envVars r)
, envTypes = Map.union (envTypes l) (envTypes r)
}

instance Monoid (GenEvalEnv sym) where
mempty = EvalEnv
{ envVars = Map.empty
{ envVars = IntMap.empty
, envTypes = Map.empty
}

mappend l r = l <> r

ppEnv :: Backend sym => sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc
ppEnv sym opts env = brackets . fsep <$> mapM bind (Map.toList (envVars env))
ppEnv sym opts env = brackets . fsep <$> mapM bind (IntMap.toList (envVars env))
where
bind (k,v) = do vdoc <- ppValue sym opts =<< v
return (pp k <+> text "->" <+> vdoc)
return (int k <+> text "->" <+> vdoc)

-- | Evaluation environment with no bindings
emptyEnv :: GenEvalEnv sym
Expand All @@ -74,7 +75,7 @@ bindVar ::
bindVar sym n val env = do
let nm = show $ ppLocName n
val' <- sDelay sym (Just nm) val
return $ env{ envVars = Map.insert n val' (envVars env) }
return $ env{ envVars = IntMap.insert (nameUnique n) val' (envVars env) }

-- | Bind a variable to a value in the evaluation environment, without
-- creating a thunk.
Expand All @@ -85,12 +86,12 @@ bindVarDirect ::
GenEvalEnv sym ->
GenEvalEnv sym
bindVarDirect n val env = do
env{ envVars = Map.insert n (pure val) (envVars env) }
env{ envVars = IntMap.insert (nameUnique n) (pure val) (envVars env) }

-- | Lookup a variable in the environment.
{-# INLINE lookupVar #-}
lookupVar :: Name -> GenEvalEnv sym -> Maybe (SEval sym (GenValue sym))
lookupVar n env = Map.lookup n (envVars env)
lookupVar n env = IntMap.lookup (nameUnique n) (envVars env)

-- | Bind a type variable of kind *.
{-# INLINE bindType #-}
Expand Down

0 comments on commit 0000ffb

Please sign in to comment.