BNF Syntax of FormulaOne

In the following BNF-format syntax of FormulaOne:

Bars ( | ) separate alternatives.
BNF elements in braces ({}) can be repeated zero or more times. (Braces { and } in the language itself designate the beginning and end of a comment. Comments can be nested).
BNF elements in square brackets ( [ , ] ) are optional.
"[", "|", and "]" mean those single characters, taken literally.
Capitalized identifiers are lexical elements.
Uncapitalized identifiers, and all other sequences of symbols, are tokens to be taken literally.

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

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

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

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

Call = Ident ( Term ) |

If = if Formula then Formula
     {elsif Formula ->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
Body      ::= Formula | Forwarde
Forwarded ::= external [_cdecl | _stdcall] String : String

Top

FormulaOne Language Definition

Type Conversion