Module Eval

This module provides operations to evaluate FlatCurry programs to (head) normal form based on the natural semantics.

Author: Jan Tikovsky

Version: December 2017

Summary of exported operations:

initCEState
                  ::  CCTOpts -> FM Int (AExpr (TypeExpr,Maybe Int,Bool)) -> [AFuncDecl (TypeExpr,Maybe Int,Bool)] -> Int -> CEState

Initial state for concolic evaluation

choice
                  ::  CEM a -> CEM a -> CEM a

Combine two evaluations within a choice

(<|>)
                  ::  CEM a -> CEM a -> CEM a

Infix version of non-deterministic choice.

gets
                  ::  (CEState -> a) -> CEM a

get
                  ::  CEM CEState

put
                  ::  CEState -> CEM ()

modify
                  ::  (CEState -> CEState) -> CEM ()

fromSubst
                  ::  FM Int (AExpr (TypeExpr,Maybe Int,Bool)) -> FM Int Binding

Generate a Heap from a given Substitution

traceStep
                  ::  String -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool)) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Trace a single evaluation step

traceSym
                  ::  CEState -> a -> a

getOpts
                  ::  CEM CCTOpts

Get the ccti options

getHeap
                  ::  CEM (FM Int Binding)

Heap operations Get the current heap

modifyHeap
                  ::  (FM Int Binding -> FM Int Binding) -> CEM ()

Modify the current heap

lookupBinding
                  ::  Int -> CEM (Maybe Binding)

Lookup the binding for a variable in the current heap

bindBH
                  ::  Int -> CEM ()

Bind a variable as a "black hole"

bindE
                  ::  Int -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM ()

Bind a variable to an expression

bindLE
                  ::  Int -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM ()

Bind a variable lazily to an expression

bindF
                  ::  Int -> CEM ()

Bind a variable as "free"

bindLF
                  ::  Int -> CEM ()

Bind a variable lazily as "free"

bindArg
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Bind an argument of a constructor or function call For let expressions and declarations of free variables the corresponding bindings are directly performed in the heap and thus preventing nested let expressions in the heap.

lookupRule
                  ::  (String,String) -> CEM (Maybe ([Int],AExpr (TypeExpr,Maybe Int,Bool)))

Lookup the parameters and the rhs for a given function

freshVar
                  ::  CEM Int

Get the next fresh variable

freshVars
                  ::  Int -> CEM [Int]

Get n fresh variables

getTraceFlag
                  ::  CEM Bool

setTraceFlag
                  ::  Bool -> CEM ()

Set the trace flag to the given boolean

withLitTracing
                  ::  CEM a -> CEM a

Perform the given action with tracing of constraints on literals

getTrace
                  ::  CEM [Decision]

Get the trace of symbolic information

mkDecision
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> Int -> BranchNr -> Int -> ((String,String),(TypeExpr,Maybe Int,Bool)) -> [Int] -> CEM ()

Add a decision with symbolic information for case expression cid to the trace

countStep
                  ::  CEM Int

setLConstr
                  ::  Maybe (AExpr (TypeExpr,Maybe Int,Bool)) -> CEM ()

getResetLConstr
                  ::  CEM (Maybe (AExpr (TypeExpr,Maybe Int,Bool)))

traceConstr
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEM ()

getSymConstr
                  ::  (String,String) -> Maybe (AExpr (TypeExpr,Maybe Int,Bool)) -> CEM (Maybe (Int,SymObj))

getOrigVI
                  ::  Int -> CEM (Maybe (Int,Binding))

ceval
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEState -> ([AExpr (TypeExpr,Maybe Int,Bool)],[[Decision]],Int)

concolic evaluation

prepExpr
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> Int -> (AExpr (TypeExpr,Maybe Int,Bool),[Int])

Prepare expression for narrowing

norm
                  ::  Int -> AExpr (TypeExpr,Maybe Int,Bool) -> (FM Int (AExpr (TypeExpr,Maybe Int,Bool)),AExpr (TypeExpr,Maybe Int,Bool),Int)

Normalize FlatCurry function call

fromResult
                  ::  Result (AExpr (TypeExpr,Maybe Int,Bool),CEState) -> ([AExpr (TypeExpr,Maybe Int,Bool)],[[Decision]],Int)

Select the result, the symbolic trace and the next free index from the search tree of non-deterministic results

nf
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Evaluate given FlatCurry expression to normal form

hnf
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Evaluate given FlatCurry expression to head normal form

hnfVar
                  ::  (TypeExpr,Maybe Int,Bool) -> Int -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a variable

hnfLit
                  ::  (TypeExpr,Maybe Int,Bool) -> Literal -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a literal

hnfComb
                  ::  (TypeExpr,Maybe Int,Bool) -> CombType -> ((String,String),(TypeExpr,Maybe Int,Bool)) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a combination:

flattened function calls: check if function is builtin or user-defined and start corresponding concolic evaluation
non-flattened function/constructor calls: flatten them

hnfLet
                  ::  [((Int,(TypeExpr,Maybe Int,Bool)),AExpr (TypeExpr,Maybe Int,Bool))] -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a let expression

addBindings
                  ::  [((Int,(TypeExpr,Maybe Int,Bool)),AExpr (TypeExpr,Maybe Int,Bool))] -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Add a list of local bindings to the heap

hnfFree
                  ::  [(Int,(TypeExpr,Maybe Int,Bool))] -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a declaration of free variables

addFrees
                  ::  [(Int,(TypeExpr,Maybe Int,Bool))] -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Add a list of free variables to the heap

hnfOr
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a non-deterministic choice

hnfCase
                  ::  (TypeExpr,Maybe Int,Bool) -> CaseType -> AExpr (TypeExpr,Maybe Int,Bool) -> [ABranchExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a case expression

failS
                  ::  (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Failing evaluation

succeedS
                  ::  CEM (AExpr (TypeExpr,Maybe Int,Bool))

Evaluation to True

unknownS
                  ::  (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Evaluation which yields a free variable

ceBuiltin
                  ::  (TypeExpr,Maybe Int,Bool) -> ((String,String),(TypeExpr,Maybe Int,Bool)) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

unary
                  ::  (AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

binary
                  ::  (AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

ceBuiltinApply
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a higher order application

ceBuiltinCond
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a conditional expression (&>) / cond

ceBuiltinEnsureNotFree
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of ensureNotFree

ceBuiltinFailed
                  ::  (TypeExpr,Maybe Int,Bool) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of failed

ceBuiltinError
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of error

ceBuiltinSuccess
                  ::  [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of success

ceBuiltinUnknown
                  ::  (TypeExpr,Maybe Int,Bool) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of unknown

ceBuiltinChoice
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of (?)

ceBuiltinAmp
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a concurrent conjunction (&)

ceBuiltinNegFloat
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of negateFloat

ceBuiltinOrd
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of ord

ceBuiltinChr
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of chr

ceBuiltinI2F
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of i2f

ceBuiltinDollarBangs
                  ::  (AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))) -> AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of (&&) Concolic evaluation of (||) Concolic evaluation of ($!) / ($!!)

ceBuiltinDollarHashHash
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of ($##)

ceBuiltinUni
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of (=:=)

ceBuiltinLazyUni
                  ::  AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of (=:<=)

occurCheck
                  ::  Int -> AExpr (TypeExpr,Maybe Int,Bool) -> FM Int Binding -> Bool

Occur check for strict unification

ceBuiltinIntOp
                  :: ToFCY a => (Int -> Int -> a) -> AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of binary operations on integers (arithmetic, logical)

ceBuiltinCharOp
                  :: ToFCY a => (Char -> Char -> a) -> AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of binary operations on characters (arithmetic, logical)

ceBuiltinFloatOp
                  :: ToFCY a => (Float -> Float -> a) -> AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of binary operations on floats (arithmetic, logical)

builtin
                  ::  (TypeExpr,Maybe Int,Bool) -> String -> [AExpr (TypeExpr,Maybe Int,Bool)] -> AExpr (TypeExpr,Maybe Int,Bool)

FlatCurry representation of a call to a builtin function

Exported datatypes:

Result

Monad for non-deterministic results

Constructors:

Return :: a -> Result a : single result
Choice :: (Result a) -> (Result a) -> Result a : non-deterministic choice

CEM

Concolic evaluation monad

Constructors:

CE :: (CEState -> Result (a,CEState)) -> CEM a
Fields:
- runCEM :: (CEState -> Result (a,CEState))

CEState

Internal state for concolic evaluation, consisting of

the current ccti options,
the concrete heap containing variable bindings,
a list of all defined function declarations,
an index for fresh variables,
a flag which indicates whether a boolean case expression is evaluated: This is required for the collection of constraints
a trace of symbolic information for case branches and
a counter of the remaining number of evaluation steps

Constructors:

CEState :: CCTOpts -> Heap -> [AFuncDecl TypeAnn] -> VarIndex -> Bool -> Trace -> Int -> Heap -> (Maybe (AExpr TypeAnn)) -> CEState
Fields:
- cesCCTOpts :: CCTOpts
- cesHeap :: Heap
- cesFuncs :: [AFuncDecl TypeAnn]
- cesFresh :: VarIndex
- cesTraceFlag :: Bool
- cesTrace :: Trace
- cesSteps :: Int
- cesSymHeap :: Heap
- cesLConstr :: (Maybe (AExpr TypeAnn))

Exported operations:

initCEState :: CCTOpts -> FM Int (AExpr (TypeExpr,Maybe Int,Bool)) -> [AFuncDecl (TypeExpr,Maybe Int,Bool)] -> Int -> CEState

Initial state for concolic evaluation

choice :: CEM a -> CEM a -> CEM a

Combine two evaluations within a choice

(<|>) :: CEM a -> CEM a -> CEM a

Infix version of non-deterministic choice.

Further infos:

defined as left-associative infix operator with precedence 3

gets :: (CEState -> a) -> CEM a

get :: CEM CEState

put :: CEState -> CEM ()

modify :: (CEState -> CEState) -> CEM ()

fromSubst :: FM Int (AExpr (TypeExpr,Maybe Int,Bool)) -> FM Int Binding

Generate a Heap from a given Substitution

traceStep :: String -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool)) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Trace a single evaluation step

traceSym :: CEState -> a -> a

getOpts :: CEM CCTOpts

Get the ccti options

getHeap :: CEM (FM Int Binding)

Heap operations Get the current heap

modifyHeap :: (FM Int Binding -> FM Int Binding) -> CEM ()

Modify the current heap

lookupBinding :: Int -> CEM (Maybe Binding)

Lookup the binding for a variable in the current heap

bindBH :: Int -> CEM ()

Bind a variable as a "black hole"

bindE :: Int -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM ()

Bind a variable to an expression

bindLE :: Int -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM ()

Bind a variable lazily to an expression

bindF :: Int -> CEM ()

Bind a variable as "free"

bindLF :: Int -> CEM ()

Bind a variable lazily as "free"

bindArg :: AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

lookupRule :: (String,String) -> CEM (Maybe ([Int],AExpr (TypeExpr,Maybe Int,Bool)))

Lookup the parameters and the rhs for a given function

freshVar :: CEM Int

Get the next fresh variable

freshVars :: Int -> CEM [Int]

Get n fresh variables

getTraceFlag :: CEM Bool

setTraceFlag :: Bool -> CEM ()

Set the trace flag to the given boolean

withLitTracing :: CEM a -> CEM a

Perform the given action with tracing of constraints on literals

getTrace :: CEM [Decision]

Get the trace of symbolic information

mkDecision :: AExpr (TypeExpr,Maybe Int,Bool) -> Int -> BranchNr -> Int -> ((String,String),(TypeExpr,Maybe Int,Bool)) -> [Int] -> CEM ()

Add a decision with symbolic information for case expression cid to the trace

countStep :: CEM Int

setLConstr :: Maybe (AExpr (TypeExpr,Maybe Int,Bool)) -> CEM ()

getResetLConstr :: CEM (Maybe (AExpr (TypeExpr,Maybe Int,Bool)))

traceConstr :: AExpr (TypeExpr,Maybe Int,Bool) -> CEM ()

getSymConstr :: (String,String) -> Maybe (AExpr (TypeExpr,Maybe Int,Bool)) -> CEM (Maybe (Int,SymObj))

getOrigVI :: Int -> CEM (Maybe (Int,Binding))

ceval :: AExpr (TypeExpr,Maybe Int,Bool) -> CEState -> ([AExpr (TypeExpr,Maybe Int,Bool)],[[Decision]],Int)

concolic evaluation

prepExpr :: AExpr (TypeExpr,Maybe Int,Bool) -> Int -> (AExpr (TypeExpr,Maybe Int,Bool),[Int])

Prepare expression for narrowing

norm :: Int -> AExpr (TypeExpr,Maybe Int,Bool) -> (FM Int (AExpr (TypeExpr,Maybe Int,Bool)),AExpr (TypeExpr,Maybe Int,Bool),Int)

Normalize FlatCurry function call

fromResult :: Result (AExpr (TypeExpr,Maybe Int,Bool),CEState) -> ([AExpr (TypeExpr,Maybe Int,Bool)],[[Decision]],Int)

Select the result, the symbolic trace and the next free index from the search tree of non-deterministic results

nf :: AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Evaluate given FlatCurry expression to normal form

hnf :: AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Evaluate given FlatCurry expression to head normal form

hnfVar :: (TypeExpr,Maybe Int,Bool) -> Int -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a variable

hnfLit :: (TypeExpr,Maybe Int,Bool) -> Literal -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a literal

hnfComb :: (TypeExpr,Maybe Int,Bool) -> CombType -> ((String,String),(TypeExpr,Maybe Int,Bool)) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a combination:

flattened function calls: check if function is builtin or user-defined and start corresponding concolic evaluation
non-flattened function/constructor calls: flatten them

hnfLet :: [((Int,(TypeExpr,Maybe Int,Bool)),AExpr (TypeExpr,Maybe Int,Bool))] -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a let expression

addBindings :: [((Int,(TypeExpr,Maybe Int,Bool)),AExpr (TypeExpr,Maybe Int,Bool))] -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Add a list of local bindings to the heap

hnfFree :: [(Int,(TypeExpr,Maybe Int,Bool))] -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a declaration of free variables

addFrees :: [(Int,(TypeExpr,Maybe Int,Bool))] -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Add a list of free variables to the heap

hnfOr :: AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a non-deterministic choice

hnfCase :: (TypeExpr,Maybe Int,Bool) -> CaseType -> AExpr (TypeExpr,Maybe Int,Bool) -> [ABranchExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a case expression

failS :: (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Failing evaluation

succeedS :: CEM (AExpr (TypeExpr,Maybe Int,Bool))

Evaluation to True

unknownS :: (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Evaluation which yields a free variable

ceBuiltin :: (TypeExpr,Maybe Int,Bool) -> ((String,String),(TypeExpr,Maybe Int,Bool)) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

unary :: (AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

binary :: (AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

ceBuiltinApply :: AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a higher order application

ceBuiltinCond :: AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a conditional expression (&>) / cond

ceBuiltinEnsureNotFree :: AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of ensureNotFree

ceBuiltinFailed :: (TypeExpr,Maybe Int,Bool) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of failed

ceBuiltinError :: AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of error

ceBuiltinSuccess :: [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of success

ceBuiltinUnknown :: (TypeExpr,Maybe Int,Bool) -> [AExpr (TypeExpr,Maybe Int,Bool)] -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of unknown

ceBuiltinChoice :: AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of (?)

ceBuiltinAmp :: AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of a concurrent conjunction (&)

ceBuiltinNegFloat :: AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of negateFloat

ceBuiltinOrd :: AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of ord

ceBuiltinChr :: AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of chr

ceBuiltinI2F :: AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of i2f

ceBuiltinDollarBangs :: (AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))) -> AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of (&&) Concolic evaluation of (||) Concolic evaluation of ($!) / ($!!)

ceBuiltinDollarHashHash :: AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of ($##)

ceBuiltinUni :: AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of (=:=)

ceBuiltinLazyUni :: AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of (=:<=)

occurCheck :: Int -> AExpr (TypeExpr,Maybe Int,Bool) -> FM Int Binding -> Bool

Occur check for strict unification

ceBuiltinIntOp :: ToFCY a => (Int -> Int -> a) -> AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of binary operations on integers (arithmetic, logical)

ceBuiltinCharOp :: ToFCY a => (Char -> Char -> a) -> AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of binary operations on characters (arithmetic, logical)

ceBuiltinFloatOp :: ToFCY a => (Float -> Float -> a) -> AExpr (TypeExpr,Maybe Int,Bool) -> AExpr (TypeExpr,Maybe Int,Bool) -> CEM (AExpr (TypeExpr,Maybe Int,Bool))

Concolic evaluation of binary operations on floats (arithmetic, logical)

builtin :: (TypeExpr,Maybe Int,Bool) -> String -> [AExpr (TypeExpr,Maybe Int,Bool)] -> AExpr (TypeExpr,Maybe Int,Bool)

FlatCurry representation of a call to a builtin function