doc: syntax of terms

parent 275deafa
...@@ -61,6 +61,11 @@ and syntax = parse ...@@ -61,6 +61,11 @@ and syntax = parse
print_string s; print_string s;
print_string "} \\sep{}"; print_string "} \\sep{}";
syntax lexbuf } syntax lexbuf }
| ";" ([^ '\n']* as s) "%\n" {
print_string "& \\textrm{";
print_string s;
print_string "}";
syntax lexbuf }
| ";" ([^ '\n']* as s) '\n' { | ";" ([^ '\n']* as s) '\n' {
print_string "& \\textrm{"; print_string "& \\textrm{";
print_string s; print_string s;
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
This chapter gives the grammar for the input files This chapter gives the grammar for the input files
\input{./term_bnf.tex} \framebox{\input{./term_bnf.tex}}
%%% Local Variables: %%% Local Variables:
%%% mode: latex %%% mode: latex
......
\begin{syntax} \begin{syntax}
bin-op ::= "+" | "-" | "*" | "/" | "%" ; term ::= integer ; integer constant
| "==" | "!=" | "<=" | ">=" | ">" | "<" ; | real ; real constant
| "&&" | "||" | ; boolean operations | qualid ; symbol
| "&" | "|" | "-->" ; | prefix-op term ;
| "<-->" | "^"; bitwise operations | term infix-op term ;
\ | lqualid term+ ; function application
unary-op ::= "+" | "-" ; unary plus and minus | "if" formula "then" term "else" term ; conditional
| "!" ; boolean negation | "let" pattern "=" term "in" term ; local binding
| "~" ; bitwise complementation | "match" ("," term)+ "with" "|"? match-cases "end" ;
| "*" ; pointer dereferencing | "(" term ("," term)* ")" ; tuple
| "&" ; address-of operator | term ":" type ; cast
\ | label term ; label
term ::= "\true" | "\false" ; | "(" term ")" ; parentheses%
| integer ; integer constants
| real ; real constants
| id ; variables
| unary-op term ;
| term bin-op term ;
| term "[" term "]" ; array access
| "{" term "\with" "[" term "]" "=" term "}" ; array functional modifier
| term "." id ; structure field access
| "{" term "\with" "."id "=" term "}" ; field functional modifier
| term "->" id ;
| "(" type-expr ")" term ; cast
| id "(" term ("," term)* ")" ; function application
| "(" term ")" ; parentheses
| term "?" term ":" term ; ternary condition
| "\let" id "=" term ";" term ; local binding
| "sizeof" "(" term ")" ;
| "sizeof" "(" C-type-expr ")" ;
| id ":" term ; syntactic naming
\end{syntax} \end{syntax}
...@@ -4,6 +4,10 @@ theory List ...@@ -4,6 +4,10 @@ theory List
type list 'a = Nil | Cons 'a (list 'a) type list 'a = Nil | Cons 'a (list 'a)
use import bool.Bool
logic x : int = if true then 1 else 3
end end
theory Length theory Length
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment