Local expressions, stores, and evaluation #

Choreographic programming and associated languages (like process calculi for modelling distributed protocol implementations) are typically defined abstracting from how processes locally compute and store values [Mon23]. This module defines this interface, as well as the derived concept of global store.

Implementation notes #

The module is currently developed with minimality in mind. In the future, we plan on adding facilities for typing expressions and easy integration with Lean and other IRs/FFIs.

References #

F. Montesi, Introduction to Choreographies

source

inductive Cslib.Mech.Expr (Var : Type u_1) (Val : Type u_2) (FunId : Type u_3) :

Type (max (max u_1 u_2) u_3)

Expressions for local computation.

var {Var : Type u_1} {Val : Type u_2} {FunId : Type u_3} (x : Var) : Expr Var Val FunId
Read variable x.
val {Var : Type u_1} {Val : Type u_2} {FunId : Type u_3} (v : Val) : Expr Var Val FunId
Value v.
call {Var : Type u_1} {Val : Type u_2} {FunId : Type u_3} (f : FunId) (args : List (Expr Var Val FunId)) : Expr Var Val FunId
Call function f with arguments args.

Instances For

source

@[instance_reducible]

instance Cslib.Mech.instCoeExpr {Var : Type u_1} {Val : Type u_2} {FunId : Type u_3} :

Coe Var (Expr Var Val FunId)

Utility instance to write variables directly as expressions.

Equations

Cslib.Mech.instCoeExpr = { coe := fun (x : Var) => Cslib.Mech.Expr.var x }

source

@[instance_reducible]

instance Cslib.Mech.instCoeExpr_1 {Val : Type u_1} {Var : Type u_2} {FunId : Type u_3} :

Coe Val (Expr Var Val FunId)

Utility instance to write values directly as expressions.

Equations

Cslib.Mech.instCoeExpr_1 = { coe := fun (v : Val) => Cslib.Mech.Expr.val v }

source

@[reducible, inline]

abbrev Cslib.Mech.LocalStore (Var : Sort u_1) (Val : Sort u_2) :

Sort (imax u_1 u_2)

A local store represents the memory state of a process, mapping variables to values.

Equations

Cslib.Mech.LocalStore Var Val = (Var → Val)

Instances For

source

@[reducible, inline]

abbrev Cslib.Mech.FunCallEval (FunId : Sort u_1) (Val : Type u_2) :

Sort (max u_1 (u_2 + 1))

Type of (potentially nondeterministic) evaluation relations for local function calls at processes.

Equations

Cslib.Mech.FunCallEval FunId Val = (FunId → List Val → Val → Prop)

Instances For

source

inductive Cslib.Mech.FunCallEval.EvalExpr {FunId : Type u_1} {Val : Type u_2} (eval : FunCallEval FunId Val) {Var : Type u_3} (σ : LocalStore Var Val) (e : Expr Var Val FunId) (v : Val) :

Prop

Evaluation relation for expressions.

val {FunId : Type u_1} {Val : Type u_2} {eval : FunCallEval FunId Val} {x✝ : Type u_3} {σ : LocalStore x✝ Val} {v : Val} : eval.EvalExpr σ (Expr.val v) v
A value evaluates to itself.
var {FunId : Type u_1} {Val : Type u_2} {eval : FunCallEval FunId Val} {x✝ : Type u_3} {σ : LocalStore x✝ Val} {x : x✝} : eval.EvalExpr σ (Expr.var x) (σ x)
A variable evaluates to its mapped value in the store.
call {FunId : Type u_1} {Val : Type u_2} {eval : FunCallEval FunId Val} {x✝ : Type u_3} {σ : LocalStore x✝ Val} {args : List (Expr x✝ Val FunId)} {vals : List Val} {f : FunId} {v : Val} (hArgs : List.Forall₂ (eval.EvalExpr σ) args vals) (hFun : eval f vals v) : eval.EvalExpr σ (Expr.call f args) v
A function call first recursively evaluates its expression arguments, and then invokes the parameter for function evaluation.