Skip to content

TLAPM parser silently drops expressions of form e \in S when parsing finite set literals #235

@ahelwer

Description

@ahelwer

Another case of sets being quite difficult to parse in TLA+ in the presence of set map and set filter syntax, similar to tlaplus/tlaplus#1021. The TLAPM syntax parser will parse set literals of the form {e \in S} as the empty set {} - as in, the \in expressions will be silently dropped! Here is some code reproducing the issue:

let _ =
  let open Tlapm_lib in
  let open OUnit2 in
  let (mule : Module.T.mule) =
    "---- MODULE Test ----\nop == {e \\in S}\n===="
    |> module_of_string
    |> Option.get
  in let (set : Expr.T.expr list) =
    match (List.hd mule.core.body).core with
    | Definition ((defn : Expr.T.defn), _, _, _) -> (
      match defn.core with
      | Operator (_, expr) -> (
        match expr.core with
        | SetEnum elements -> elements
        | _ -> failwith "Expected finite set expression"
      )
      | _ -> failwith "Expected operator"
    )
    | _ -> failwith "Expected definition"
  in assert_equal 1 (List.length set) ~printer:Int.to_string

When run using dune runtest, this will produce OUnitTest.OUnit_failure("expected: 1 but got: 0"). This happens no matter how many e \in S expressions you add to the set.

Found during work on #229

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugAn error, usually in the code.syntax parserIssues relating to TLAPM's syntax parser

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions