expr.bnf 2.55 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
\begin{syntax}
  expr ::= integer                                ; integer constant
       | real 			                  ; real constant
       | lqualid 		                  ; symbol
       | prefix-op expr 	                  ;
       | expr infix-op expr 	                  ;
       | expr "[" expr "]"                        ; brackets
       | expr "[" expr "]" "<-" expr              ; brackets assignment
       | expr "[" expr infix-op-1 expr "]" 	  ; ternary brackets
       | expr expr+ 		                  ; function application
       | "fun" type-v-param+ "->" triple          ; lambda abstraction
       | "let" "rec" recfun ("with" recfun)*      ; recursive functions
       | "if" expr "then" expr ("else" expr)?     ; conditional
       | expr ";" expr                            ; sequence
       | "loop" loop-annot "end"                  ; infinite loop
       | "while" expr "do" loop-annot expr "done" ; while loop
       | "for" lident "=" expr to-downto expr     ; for loop
         "do" loop-inv expr "done"                ;
       | assert annotation                        ; assertion
       | "absurd"                                 ;
       | "raise" uqualid                          ; exception raising
       | "raise" "(" uqualid expr ")"             ;
       | "try" expr "with" ("|" handler)+ "end"   ; exception catching
       | "any" type-c                             ; 
       | "let" pattern "=" expr "in" expr         ; local binding
       | "match" expr ("," expr)* "with"          ; pattern matching
         ("|" expr-case)+ "end"                   ;
       | "(" expr ("," expr)+ ")"                 ; tuple
       | "{|" field-value+ "|}"                   ; record
       | exopr "." lqualid                        ; field access
       | expr "." lqualid "<-" expr               ; field assignment
       | "{|" expr "with" field-value+ "|}"       ; field update
       | expr ":" type 	                          ; cast
34 35
       | label expr 	                          ; label
       | "'" uident ":" expr                      ; code mark
36 37 38 39
       | "(" expr ")" 	      	                  ; parentheses
  \
  expr-case ::= pattern "->" expr                 ;
  \
40
  field-value ::= lqualid "=" expr ";"            ;
41 42 43 44 45 46 47 48 49 50 51 52 53
  \
  triple ::= expr                                 ;
    | pre expr post                               ; Hoare triple
  \
  assert ::= "assert" | "assume" | "check"
  \
  to-downto ::= "to" | "downto"
  \
  loop-annot ::= loop-inv? variant?
  \
  loop-inv ::= "invariant" annotation
  \
  variant ::= "variant" "{" term "}" ("with" lqualid)?
54
\end{syntax}