Safe Haskell | None |
---|
Execution state for the interpreter
- data MapRepr
- emptyMap :: MapRepr
- stored :: MapRepr -> Map [Value] Value
- data Value
- valueFromInteger :: Type -> Integer -> Value
- vnot :: Value -> Value
- unValueBool :: Value -> Bool
- unValueMap :: Value -> MapRepr
- flattenMap :: Heap Value -> Ref -> (Ref, Map [Value] Value)
- mapSource :: Heap Value -> Ref -> Ref
- mapValues :: Heap Value -> Ref -> Map [Value] Value
- refIdTypeName :: [Char]
- ucTypeName :: [Char]
- deepDeref :: Heap Value -> Value -> Value
- objectEq :: Heap Value -> Value -> Value -> Maybe Bool
- mustAgree :: Ord k => Heap Value -> Map k Value -> Map k Value -> Bool
- mustDisagree :: Ord k => Heap Value -> Map k Value -> Map k Value -> Bool
- valueDoc :: Value -> Doc
- type Store = Map Id Value
- emptyStore :: Store
- functionConst :: [Char] -> [Char]
- userStore :: Heap Value -> Store -> Store
- storeDoc :: Store -> Doc
- data Memory
- type StoreLens = SimpleLens Memory Store
- memLocals :: Lens Memory Memory Store Store
- memGlobals :: Lens Memory Memory Store Store
- memOld :: Lens Memory Memory Store Store
- memConstants :: Lens Memory Memory Store Store
- memHeap :: Lens Memory Memory (Heap Value) (Heap Value)
- emptyMemory :: Memory
- visibleVariables :: Memory -> Store
- memoryDoc :: Bool -> Memory -> Doc
- data AbstractMemory
- amLocals :: Lens AbstractMemory AbstractMemory AbstractStore AbstractStore
- amGlobals :: Lens AbstractMemory AbstractMemory AbstractStore AbstractStore
- amHeap :: Lens AbstractMemory AbstractMemory (Map Ref ConstraintSet) (Map Ref ConstraintSet)
- data Environment m
- envMemory :: forall m. Lens (Environment m) (Environment m) Memory Memory
- envProcedures :: forall m. Lens (Environment m) (Environment m) (Map Id [PDef]) (Map Id [PDef])
- envConstraints :: forall m. Lens (Environment m) (Environment m) AbstractMemory AbstractMemory
- envTypeContext :: forall m. Lens (Environment m) (Environment m) Context Context
- envGenerator :: forall m m. Lens (Environment m) (Environment m) (Generator m) (Generator m)
- envCustomCount :: forall m. Lens (Environment m) (Environment m) (Map Id Int) (Map Id Int)
- envQBound :: forall m. Lens (Environment m) (Environment m) (Maybe Integer) (Maybe Integer)
- envInOld :: forall m. Lens (Environment m) (Environment m) Bool Bool
- initEnv :: Context -> Generator m -> Maybe Integer -> Environment m
- lookupProcedure :: Id -> Environment m -> [PDef]
- lookupNameConstraints :: Id -> Environment m -> ConstraintSet
- lookupMapConstraints :: Ref -> Environment m -> ConstraintSet
- lookupCustomCount :: Id -> Environment m -> Int
- addProcedureImpl :: Id -> PDef -> Environment m -> Environment m
- addGlobalDefinition :: Id -> FDef -> Environment m -> Environment m
- addMapDefinition :: Ref -> FDef -> Environment m -> Environment m
- addMapConstraint :: Ref -> FDef -> Environment m -> Environment m
- setCustomCount :: Id -> Int -> Environment m -> Environment m
- withHeap :: (Heap Value -> (t, Heap Value)) -> Environment m -> (t, Environment m)
Documentation
Representation of a map value
stored :: MapRepr -> Map [Value] ValueSource
Key-value pairs stored explicitly in a map representation
Run-time value
IntValue Integer | Integer value |
BoolValue Bool | Boolean value |
CustomValue Id Int | Value of a user-defined type |
MapValue MapRepr | Value of a map type: consists of an optional reference to the base map (if derived from base by updating) and key-value pairs that override base |
Reference Ref | Reference to a map stored in the heap |
valueFromInteger :: Type -> Integer -> ValueSource
valueFromInteger
t n
: value of type t
with an integer code n
unValueBool :: Value -> BoolSource
unValueMap :: Value -> MapReprSource
flattenMap :: Heap Value -> Ref -> (Ref, Map [Value] Value)Source
Source reference and key-value pairs of a reference in a heap
refIdTypeName :: [Char]Source
Dummy user-defined type used to differentiate map values
ucTypeName :: [Char]Source
Dummy user-defined type used to mark entities whose definitions are currently being evaluated
deepDeref :: Heap Value -> Value -> ValueSource
deepDeref
h v
: Completely dereference value v
given heap h
(so that no references are left in v
)
objectEq :: Heap Value -> Value -> Value -> Maybe BoolSource
objectEq
h v1 v2
: is v1
equal to v2
in the Boogie semantics? Nothing if cannot be determined.
A store with no variables
functionConst :: [Char] -> [Char]Source
functionConst
name
: name of a map constant that corresponds function name
(must be distinct from all global names)
userStore :: Heap Value -> Store -> StoreSource
userStore
heap store
: store
with all reference values completely dereferenced given heap
, and all auxiliary values removed
Memory: stores concrete values associated with names and references
type StoreLens = SimpleLens Memory StoreSource
Lens that selects a store from memory
Empty memory
visibleVariables :: Memory -> StoreSource
Visible values of all identifiers in a memory (locals shadow globals)
memoryDoc :: Bool -> Memory -> DocSource
memoryDoc
debug mem
: either user or debug representation of mem
, depending on debug
data AbstractMemory Source
Abstract memory: stores constraints associated with names and references
data Environment m Source
Execution state
envMemory :: forall m. Lens (Environment m) (Environment m) Memory MemorySource
envProcedures :: forall m. Lens (Environment m) (Environment m) (Map Id [PDef]) (Map Id [PDef])Source
envConstraints :: forall m. Lens (Environment m) (Environment m) AbstractMemory AbstractMemorySource
envTypeContext :: forall m. Lens (Environment m) (Environment m) Context ContextSource
envGenerator :: forall m m. Lens (Environment m) (Environment m) (Generator m) (Generator m)Source
envCustomCount :: forall m. Lens (Environment m) (Environment m) (Map Id Int) (Map Id Int)Source
envQBound :: forall m. Lens (Environment m) (Environment m) (Maybe Integer) (Maybe Integer)Source
envInOld :: forall m. Lens (Environment m) (Environment m) Bool BoolSource
initEnv :: Context -> Generator m -> Maybe Integer -> Environment mSource
initEnv
tc gen
: Initial environment in a type context tc
with a value generator gen
lookupProcedure :: Id -> Environment m -> [PDef]Source
lookupNameConstraints :: Id -> Environment m -> ConstraintSetSource
lookupMapConstraints :: Ref -> Environment m -> ConstraintSetSource
lookupCustomCount :: Id -> Environment m -> IntSource
addProcedureImpl :: Id -> PDef -> Environment m -> Environment mSource
addGlobalDefinition :: Id -> FDef -> Environment m -> Environment mSource
addMapDefinition :: Ref -> FDef -> Environment m -> Environment mSource
addMapConstraint :: Ref -> FDef -> Environment m -> Environment mSource
setCustomCount :: Id -> Int -> Environment m -> Environment mSource
withHeap :: (Heap Value -> (t, Heap Value)) -> Environment m -> (t, Environment m)Source