A small-step semantics for LExpr.
Currently only defined for expressions paremeterized by LMonoTy, but it will
be expanded to an arbitrary type in the future.
The order of constructors matter because the constructor tactic will rely on
it.
This small-step definitions faithfully follows the behavior of LExpr.eval,
except that:
-
This inductive definition may get stuck early when there is no
assignment to a free variable available.
-
This semantics does not describe how metadata must change, because
metadata must not affect evaluation semantics. Different concrete evaluators
like LExpr.eval can have different strategy for updating metadata.
Constructors
expand_fvar {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
{F : Factory Tbase} {rf : Env Tbase}
{m : Tbase.mono.base.Metadata}
{ty : Option Tbase.mono.TypeType} (x : Tbase.Identifier)
(e : LExpr Tbase.mono) :
rf x = some e → Step F rf (LExpr.fvar m x ty) e
A free variable. Stuck if fvar does not exist in FreeVarMap.
beta {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
{F : Factory Tbase} {rf : Env Tbase}
{m1 m2 : Tbase.mono.base.Metadata}
{ty : Option Tbase.mono.TypeType}
(e1 v2 eres : LExpr Tbase.mono) :
LExpr.isCanonicalValue F v2 = true →
eres = LExpr.subst (fun x => v2) e1 →
Step F rf (LExpr.app m1 (LExpr.abs m2 ty e1) v2) eres
Call-by-value semantics: beta reduction.
reduce_2 {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
{F : Factory Tbase} {rf : Env Tbase}
{m m' : Tbase.mono.base.Metadata}
(v1 e2 e2' : LExpr Tbase.mono) :
LExpr.isCanonicalValue F v1 = true →
Step F rf e2 e2' →
Step F rf (LExpr.app m v1 e2) (LExpr.app m' v1 e2')
Call-by-value semantics: argument evaluation.
ite_reduce_then {Tbase : LExprParams}
[DecidableEq Tbase.IDMeta] {F : Factory Tbase}
{rf : Env Tbase} {m mc : Tbase.mono.base.Metadata}
(ethen eelse : LExpr Tbase.mono) :
Step F rf
(LExpr.ite m (LExpr.const mc (LConst.boolConst true))
ethen eelse)
ethen
Lazy evaluation of ite: condition is true. To evaluate ite x e1 e2, do
not first evaluate e1 and e2. In other words, ite x e1 e2 is interpreted
as ite x (λ.e1) (λ.e2).
ite_reduce_else {Tbase : LExprParams}
[DecidableEq Tbase.IDMeta] {F : Factory Tbase}
{rf : Env Tbase} {m mc : Tbase.mono.base.Metadata}
(ethen eelse : LExpr Tbase.mono) :
Step F rf
(LExpr.ite m (LExpr.const mc (LConst.boolConst false))
ethen eelse)
eelse
Lazy evaluation of ite: condition is false. To evaluate ite x e1 e2, do
not first evaluate e1 and e2. In other words, ite x e1 e2 is interpreted
as ite x (λ.e1) (λ.e2).
ite_reduce_cond {Tbase : LExprParams}
[DecidableEq Tbase.IDMeta] {F : Factory Tbase}
{rf : Env Tbase} {m m' : Tbase.mono.base.Metadata}
(econd econd' ethen eelse : LExpr Tbase.mono) :
Step F rf econd econd' →
Step F rf (LExpr.ite m econd ethen eelse)
(LExpr.ite m' econd' ethen eelse)
Evaluation of ite condition.
eq_reduce {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
{F : Factory Tbase} {rf : Env Tbase}
{mc m : Tbase.mono.base.Metadata}
(e1 e2 eres : LExpr Tbase.mono)
(H1 : LExpr.isCanonicalValue F e1 = true)
(H2 : LExpr.isCanonicalValue F e2 = true) :
eres =
LExpr.const mc
(LConst.boolConst (LExpr.eql F e1 e2 H1 H2)) →
Step F rf (LExpr.eq m e1 e2) eres
Evaluation of equality. Reduce after both operands evaluate to values.
eq_reduce_rhs {Tbase : LExprParams}
[DecidableEq Tbase.IDMeta] {F : Factory Tbase}
{rf : Env Tbase} {m m' : Tbase.mono.base.Metadata}
(v1 e2 e2' : LExpr Tbase.mono) :
LExpr.isCanonicalValue F v1 = true →
Step F rf e2 e2' →
Step F rf (LExpr.eq m v1 e2) (LExpr.eq m' v1 e2')
Evaluation of the right-hand side of an equality.
expand_fn {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
{F : Factory Tbase} {rf : Env Tbase}
(e callee fnbody new_body : LExpr Tbase.mono)
(args :
List (LExpr { base := Tbase, TypeType := LMonoTy }))
(fn : LFunc Tbase) :
F.callOfLFunc e = some (callee, args, fn) →
fn.body = some fnbody →
new_body =
fnbody.substFvars (fn.inputs.keys.zip args) →
Step F rf e new_body
Evaluate a built-in function when a body expression is available in the
Factory argument F. This is consistent with what LExpr.eval does (modulo
the inline flag). Note that it might also be possible to evaluate with
eval_fn. A key correctness property is that doing so will yield the same
result. Note that this rule does not enforce an evaluation order.
eval_fn {Tbase : LExprParams} [DecidableEq Tbase.IDMeta]
{F : Factory Tbase} {rf : Env Tbase} {m : Tbase.Metadata}
(e callee e' : LExpr Tbase.mono)
(args :
List (LExpr { base := Tbase, TypeType := LMonoTy }))
(fn : LFunc Tbase)
(denotefn :
Tbase.Metadata →
List (LExpr Tbase.mono) → Option (LExpr Tbase.mono)) :
F.callOfLFunc e = some (callee, args, fn) →
fn.concreteEval = some denotefn →
some e' = denotefn m args → Step F rf e e'
Evaluate a built-in function when a concrete evaluation function is
available in the Factory argument F. Note that it might also be possible to
evaluate with expand_fn. A key correctness property is that doing so will
yield the same result. Note that this rule does not enforce an evaluation
order.
