Lark grammar for alloy

alloy.lark

// ================================================
// Alloy core (minimal but practical) - Lark v3
// Parser:   LALR (recommended)  -or-  Earley
// Lexer:    contextual (recommended)
// Notes:
//  - Unique terminal definitions (no duplicates).
//  - _NL imported & ignored for IDEs.
//  - Adds SUM token for quantifier & unary aggregator.
//  - Adds unary + / - support.
// ================================================

%import common.NEWLINE          -> _NL
%import common.WS_INLINE
%ignore WS_INLINE
%ignore _NL
%ignore /\/\/[^\n]*/                       // // line comments
%ignore /\/\*([^*]|\*+[^*\/])*\*+\//       // /* block comments */

// ---------- Punctuation ----------
LPAREN: "("
RPAREN: ")"
LBRACE: "{"
RBRACE: "}"
LBRACKET: "["
RBRACKET: "]"
COMMA: ","
COLON: ":"
BAR: "|"
DOT: "."
SEMI: ";"
AT: "@"
QUOTE: "'"
SLASH: "/"

// ---------- Symbol operators ----------
PLUS: "+"
MINUS: "-"
STAR: "*"
CARET: "^"
TILDE: "~"
AMP: "&"
ARROW: "->"
DOMAIN: "<:"
RANGE: ":>"
EQ: "="
NEQ: "!="
LT: "<"
LTE: "<=" | "=<"
GT: ">"
GTE: ">="
SHL: "<<"
SHA: ">>"
SHR: ">>>"
PLUSPLUS: "++"

// ---------- Keywords ----------
MODULE: "module"i
OPEN: "open"i
AS: "as"i
ENUM: "enum"i
SIG: "sig"i
ABSTRACT: "abstract"i
PRIVATE: "private"i
VAR: "var"i
PRED: "pred"i
FUN: "fun"i
FACT: "fact"i
ASSERT: "assert"i
RUN: "run"i
CHECK: "check"i
FOR: "for"i
BUT: "but"i
EXACTLY: "exactly"i
EXPECT: "expect"i

THIS: "this"i
UNIV: "univ"i
NONE: "none"i
STRINGKW: "string"i
INTKW: "int"i
SIGINTKW: "Int"i
SEQKW: "seq"i
STEPS: "steps"i
IDEN: "iden"i

SET: "set"i
ALL: "all"i
SOME: "some"i
ONE: "one"i
LONE: "lone"i
NO: "no"i
SUM: "sum"i                // <--- added
IN: "in"i
NOT: "not"i | "!"
AND: "and"i | "&&"
OR:  "or"i  | "||"
IMPLIES: "implies"i | "=>"
IFF: "iff"i | "<=>"
DISJ: "disj"i
EXTENDS: "extends"i

// ---------- Basic atoms ----------
%import common.CNAME            -> NAME
%import common.SIGNED_NUMBER    -> NUMBER
%import common.ESCAPED_STRING   -> STRING

// ========== Start ==========
start: spec
spec: item*
item: module_decl
    | open_decl
    | enum_decl
    | sig_decl
    | fact_decl
    | assert_decl
    | pred_decl
    | fun_decl
    | command

// ========== Module / open / enum ==========
module_decl: MODULE qname (LBRACKET name_list RBRACKET)?
open_decl:   PRIVATE? OPEN qname (LBRACKET sigref_list RBRACKET)? (AS NAME)?
enum_decl:   PRIVATE? ENUM NAME LBRACE name_list? RBRACE

qname: NAME (SLASH NAME)*

// ========== Sigs & fields ==========
sig_decl: sig_quals? SIG name_list sig_in? LBRACE field_decls? RBRACE sig_where?
sig_quals: (ABSTRACT | LONE | ONE | SOME | PRIVATE | VAR)*
sig_in: EXTENDS sigref
      | (IN | EQ) sigref_u

sigref: qname
      | UNIV
      | STRINGKW
      | SIGINTKW
      | SEQKW SLASH SIGINTKW     -> seq_int
      | STEPS
      | NONE

sigref_list: (sigref (COMMA sigref)*)?
sigref_u: sigref (PLUS sigref)*

name_list: NAME (COMMA NAME)*

field_decls: field_decl (COMMA field_decl)*
field_decl: field_head name_list COLON expr
          | field_head name_list EQ expr
field_head: PRIVATE? DISJ? VAR? DISJ?

sig_where: super_block?
super_block: LBRACE expr_plus RBRACE
expr_plus: expr (expr)*                   // sequence treated as conjunction

// ========== Facts / asserts / preds / funs ==========
fact_decl:   FACT (NAME | STRING)? super_block
assert_decl: ASSERT (NAME | STRING)? super_block expects?
pred_decl:   PRIVATE? PRED qual_name fun_params? super_block
fun_decl:    PRIVATE? FUN  qual_name fun_params? COLON expr super_block

qual_name: (sigref DOT)? NAME
fun_params: LPAREN decls? RPAREN
decls: decl (COMMA decl)*
decl: decl_head name_list COLON expr
decl_head: PRIVATE? DISJ? VAR?

// ========== Commands & scopes (simplified) ==========
command: (RUN | CHECK) NAME? super_block? scope? expects?
expects: EXPECT NUMBER

scope: FOR scope_one (BUT type_scopes)?
     | FOR type_scopes
     |                               -> empty_scope

scope_one: NUMBER
type_scopes: type_scope (COMMA type_scope)*
type_scope: type_num ( NAME | SIGINTKW | INTKW | STRINGKW | STEPS | UNIV | NONE )
type_num:   EXACTLY NUMBER
          | NUMBER

// ========== Expressions (pared down, Alloy-like precedence) ==========
?expr: or_expr
     | expr_no_seq SEMI expr               -> seq_and_after

?expr_no_seq: or_expr

?or_expr: or_expr OR eqv_expr              -> or
        | eqv_expr

?eqv_expr: eqv_expr IFF impl_expr          -> iff
         | impl_expr

?impl_expr: and_expr
          | and_expr IMPLIES impl_expr     -> implies

?and_expr: and_expr AND not_expr           -> and
         | not_expr

?not_expr: NOT not_expr                    -> not
         | quant                           // allow typed quantifiers at expr-start
         | cmp_expr

// quantifiers: all/some/lone/one/no/sum
quant: quant_head decls BAR expr_no_seq
quant_head: ALL | NO | SOME | LONE | ONE | SUM

// comparisons + quantifier-like unary keywords in expression position
?cmp_expr: sum_expr
         | cmp_expr IN   sum_expr          -> in
         | cmp_expr EQ   sum_expr          -> eq
         | cmp_expr NEQ  sum_expr          -> neq
         | cmp_expr NOT EQ sum_expr        -> neq     // accept "not ="
         | cmp_expr LT   sum_expr          -> lt
         | cmp_expr LTE  sum_expr          -> lte
         | cmp_expr GT   sum_expr          -> gt
         | cmp_expr GTE  sum_expr          -> gte
         | NO   sum_expr                   -> no_of
         | SOME sum_expr                   -> some_of
         | LONE sum_expr                   -> lone_of
         | ONE  sum_expr                   -> one_of
         | SET  sum_expr                   -> setof

// union/diff/intersect (no integer precedence here)
?sum_expr: sum_expr PLUS   term            -> plus
         | sum_expr MINUS  term            -> minus
         | term

?term: term AMP join                       -> intersect
     | join

// relational composition, arrows, domain/range
?join: join DOT atom                       -> dot
     | join ARROW join                     -> arrow
     | join DOMAIN join                    -> domain
     | join RANGE  join                    -> range
     | atom

// unary relational & numeric ops + atoms
?atom: base
     | MINUS atom                          -> neg       // unary -
     | PLUS  atom                          -> pos       // unary +
     | SUM   atom                          -> sum_unop  // unary sum aggregator
     | TILDE atom                          -> transpose
     | CARET atom                          -> closure
     | STAR  atom                          -> rclosure
     | LPAREN expr RPAREN                  -> paren

?base: NUMBER                              -> number
     | STRING                              -> string
     | IDEN                                -> iden
     | THIS                                -> this_kw
     | sigref
     | AT qname                            -> at_name
     | comp

// set comprehension { decls | expr } or { decls }
comp: LBRACE decls (BAR expr_no_seq)? RBRACE