search

will62794 / tla-web

Interactive, web-based environment for exploring TLA+ specifications.
MIT License
69 stars 7 forks source link

LAMBDA expressions #22

Closed lemmy closed 1 year ago

lemmy commented 2 years ago 
---- MODULE Issue123 ----

Op(l(_), v) ==
    l(v)

VARIABLE x

Init ==
    x = FALSE

Next ==
    x' = Op(LAMBDA v: ~v, x)

Spec == Init /\ [][Next]_x

====
TypeError: Cannot read properties of undefined (reading 'val')
    at evalBoundOp (eval.js:1788:71)
    at evalExpr (eval.js:2070:16)
    at evalExpr (eval.js:2517:15)
    at eval.js:1187:31
    at lodash.min.js:98:241
    at lodash.min.js:54:66
    at ue (lodash.min.js:35:327)
    at Function.Kc [as mapValues] (lodash.min.js:98:213)
    at evalEq (eval.js:1184:30)
    at evalBoundInfix (eval.js:1338:16)

Explicitly defined op doesn't work either:

---- MODULE Issue123 ----
EXTENDS Naturals

Neg(v) ==
   v

Op(l(_), v) ==
    l(v)

VARIABLE x

Init ==
    x = FALSE

Next ==
    x' = Op(Neg, x)

Spec == Init /\ [][Next]_x

====
will62794 commented 1 year ago

Note on lambdas from TLA+ guide:

Syntactically, a lambda expression consists of the keyword lambda followed by a comma-separated list of identifiers, followed by “ : ”, followed by an expression. A lambda expression can be used only as the argument of a higher-order operator or to the right of a “←” in an instance statement.

will62794 commented 1 year ago

Initial implementation in f04eceb and 57a231c.