Copyright | (c) Kimiyuki Onaka 2021 |
---|---|
License | Apache License 2.0 |
Maintainer | kimiyuki95@gmail.com |
Stability | experimental |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
Jikka.RestrictedPython.Evaluate
Contents
Description
Synopsis
- run :: MonadError Error m => Program -> [Value] -> m Value
- makeGlobal :: MonadError Error m => Program -> m Global
- runWithGlobal :: MonadError Error m => Global -> Expr' -> m Value
- evalExpr :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Expr' -> m Value
- evalStatement :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Statement -> m (Maybe Value)
- evalStatements :: (MonadReader Global m, MonadState Local m, MonadError Error m) => [Statement] -> m (Maybe Value)
- execToplevelStatement :: (MonadState Global m, MonadError Error m) => ToplevelStatement -> m ()
Documentation
internal functions
makeGlobal :: MonadError Error m => Program -> m Global Source #
makeGlobal
packs toplevel definitions into Global
.
This assumes doesntHaveLeakOfLoopCounters
.
runWithGlobal :: MonadError Error m => Global -> Expr' -> m Value Source #
evalExpr :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Expr' -> m Value Source #
evalExpr
evaluates exprs of our restricted Python-like language.
Rules for e1boolope2
e1∣μ⇓falsee1 and e2∣μ⇓false e1∣μ⇓truee2∣μ⇓ve1 and e2∣μ⇓v ⋮
Rules for e1binope2
e1∣μ⇓v1e2∣μ⇓v2e1+e2∣μ⇓(v1+v2) ⋮
Rules for unaryope
Rules for λxτxτ…xτ.e
λx0τ0x1τ1…xn−1τn−1.e∣μ⇓λμx0x1…xn−1.e
Rules for if e then e else e
Rules for [e for y in e (if e)?]
Rules for ecmpope
Rules for e(e,e,…,e)
e∣μ⇓λμ′x0x1…xn−1.e′e0∣μ⇓v0e1∣μ⇓v1…en−1∣μ⇓vn−1e′∣(x0↦v0;x1↦v1;…;xn−1↦vn−1;μ′)⇓ve(e0,e1,…,en−1)∣μ⇓v
e∣μ⇓be0∣μ⇓v0e1∣μ⇓v1…en−1∣μ⇓vn−1e(e0,e1,…,en−1)∣μ⇓b(e0,e1,…,en−1)(b is a builtin function)
Rules for constant
Rules for e[e]
Rules for x
x∣μ⇓μ(x)
Rules for [e,e,…,e]τ
Rules for e[e?:e?:e?]
evalStatement :: (MonadReader Global m, MonadState Local m, MonadError Error m) => Statement -> m (Maybe Value) Source #
evalStatement
evaluates statements of our restricted Python-like language.
When a statement is evaluated, it returns a value v, doesn't return anything stop, or fails err.
Also it updates the environment function μ from variables to values.
Rules for return e
e∣μ⇓vreturn e∣μ⇓v∣μ
Rules for ybinop=e
ybinope∣μ⇓vybinop=e∣μ⇓stop∣(y↦v;μ)
Rules for y:=e
e∣μ⇓vybinop=e∣μ⇓stop∣(y↦v;μ)
Rules for for y in e:stmt;stmt;…;stmt
e∣μ⇓nil(for y in e: →stmt)∣μ⇓stop∣μ
e∣μ⇓cons(v1,v2)→stmt∣(y↦v1;μ)⇓v∣μ′(for y in e: →stmt)∣μ⇓v∣μ′
e∣μ⇓cons(v1,v2)→stmt∣(y↦v1;μ)⇓stop∣μ′(for y in v2: →stmt)∣μ′⇓a∣μ″(for y in e: →stmt)∣μ⇓a∣μ″(a∈{v,stop})
It assumes the program is properly alpha-converted, i.e. doesntHaveLeakOfLoopCounters
. So it leaks loop counters to out of loops.
Rules for if e:stmt;stmt;…;stmt;else:stmt;stmt;…;stmt
e∣μ⇓true→stmt1∣μ⇓a∣μ′(if e: →stmt1 else: →stmt2)∣μ⇓a∣μ′(a∈{v,stop})
e∣μ⇓false→stmt2∣μ⇓a∣μ′(if e: →stmt1 else: →stmt2)∣μ⇓a∣μ′(a∈{v,stop})
Rules for assert e
e∣μ⇓trueassert e∣μ⇓stop
e∣μ⇓falseassert e∣μ⇓err
Rules for e
e∣μ⇓vx.append(e)∣μ⇓stop∣(x↦snoc(μ(x),v);μ)
evalStatements :: (MonadReader Global m, MonadState Local m, MonadError Error m) => [Statement] -> m (Maybe Value) Source #
evalStatements
evaluates sequences of statements of our restricted Python-like language.
stmt0∣μ⇓v∣μ′stmt0;stmt1;…;stmtn−1∣μ⇓v∣μ′
stmt0∣μ⇓stop∣μ′stmt1;…;stmtn−1∣μ′⇓a∣μ″stmt0;stmt1;…;stmtn−1∣μ⇓a∣μ″(a∈{v,stop})
ϵ∣μ⇓stop∣μ
execToplevelStatement :: (MonadState Global m, MonadError Error m) => ToplevelStatement -> m () Source #