F1: BNF Syntax

Query     ::= [ all | one | min | max ]
              [ Var { , Var } ] [ in [ Ident | String ] ] Formula [ end ]

Prog      ::= { Typedecl | Constdecl } { Pred }

Formula   ::= Formula2 { "|" Formula2 }
Formula2  ::= Formula3 { & Formula3 }
Formula3  ::= If | Case | All | false | true | ~Formula3 |
              Call | Term Oper Term  | ( Formula ) | Vdecl

Oper      ::= < | > | <= | >= | <> | = | := | in

Call      ::= Ident ( Term )

If        ::= if Formula then Formula
              {elsif Formula then Formula} }
              [ else Formula ]
              end

Case      ::= case Term  of
              Term { "|" Term } => Formula
              { ; Term { "|" Term } => Formula } [ ; ]
              [ else Formula ]
              end

All       ::= all Var { , Var } in Var Formula end |
              [ one | min | max ] Var { , Var } Formula end

Term      ::= Term1 [ ,Term ]
Terml     ::= [ - ] Term2 {Addop Term2 }
Addop     ::= + | -
Term2     ::= Term3 { Multop Term3 }
Multop    ::= * | / | mod
Term3     ::= _ | Ident | Call | Number | String | Charconst |
              Selection | ( Term ) | Array | Term3 : Type
Selection ::= [ Var | Ident ] { . Var | ( Term ) }
Array     ::= "[" [Term ] "]"
Number    ::= DecimalDigit { DecimalDigit } | Radix RadixDigit {RadixDigit}
Radix     ::= 0x | 0b | 0o | 0d
String    ::= 'Char { Char }'
Charconst ::= " Char "

Type      ::= Ptype [ Arrows Type ]
Arrows    ::= -> | ->>
Ptype     ::= ( Tuple ) | [ Ident ] "[" [ Term ]..[Term] "]" |
              list Ptype | rel Ptype | file Ptype | Ident
Tuple     ::= Named | Unnamed
Named     ::= Var : Type { , Unnamed }
Unnamed   ::= Type { , Unnamed }

Vdecl     ::= Var Mode Type
Mode      ::= :< | :> | :. | ::

Typedecl  ::= [ local ] Ident = Td
Td        ::= Tuple | Union
Constdecl ::= [ local ] Ident :< Type = Term
Union     ::= Unionelem "|" Unionelem { "|" Unionelem }
Unionelem   = Ident | Ident ( Tuple )

Pred      ::= [ local ] Kind Ident ( Vdecl { , Vdecl } ) iff Body
Kind      ::= pred | proc | subr
Body      ::= Formula | Forwarded
Forwarded ::= external [_cdecl | _stdcall] String : String