Language "OCaml Light"
#7 Expressions
Syntax
E : expr
::= value-path
| constant
| '(' expr ')'
| 'begin' expr 'end'
| '(' expr ':' typexpr ')'
| expr comma-expr+
// | constr expr // ambiguous!
| expr '::' expr
| '[' expr semic-expr* ']'
| '[' expr semic-expr* ';' ']'
| '[|' expr semic-expr* '|]'
| '[|' expr semic-expr* ';' '|]'
| '{' field '=' expr semic-field-expr* '}'
| '{' field '=' expr semic-field-expr* ';' '}'
| '{' expr 'with' field '=' expr semic-field-expr* '}'
| '{' expr 'with' field '=' expr semic-field-expr* ';' '}'
| expr argument+
| prefix-symbol expr
| '-' expr
| '-.' expr
| expr infix-op-1 expr
| expr infix-op-2 expr
| expr infix-op-3 expr
| expr infix-op-4 expr
| expr infix-op-5 expr
| expr infix-op-6 expr
| expr infix-op-7 expr
| expr infix-op-8 expr
| expr '.' field
| expr '.(' expr ')'
| expr '.(' expr ')' '<-' expr
| 'if' expr 'then' expr ( 'else' expr )?
| 'while' expr 'do' expr 'done'
| 'for' value-name '=' expr ('to'|'downto') expr 'do' expr 'done'
| expr ';' expr
| 'match' expr 'with' pattern-matching
| 'function' pattern-matching
| 'fun' pattern+ '->' expr
| 'try' expr 'with' pattern-matching
| let-definition 'in' expr
| 'assert' expr
A : argument ::= expr
PM : pattern-matching
::= pattern '->' expr pattern-expr*
| '|' pattern '->' expr pattern-expr*
LD : let-definition ::= 'let' ('rec')? let-binding and-let-binding*
LB : let-binding
::= pattern '=' expr
| value-name pattern+ '=' expr // using pattern* was ambiguous!
| value-name ':' poly-typexpr '=' expr
ALB : and-let-binding ::= 'and' let-binding
CE : comma-expr ::= ',' expr
SE : semic-expr ::= ';' expr
SFE : semic-field-expr ::= ';' field '=' expr
PE : pattern-expr ::= '|' pattern '->' expr
Rule
[[ '(' E ')' ]] : expr = [[ E ]]
Rule
[[ 'begin' E 'end' ]] : expr = [[ E ]]
Rule
[[ '(' E ':' T ')' ]] : expr = [[ E ]]
Rule
[[ E1 E2 A A* ]] : expr = [[ ( '(' E1 E2 ')' ) A A* ]]
// FIX-ME: "... E+" not yet supported
Rule
[[ PS E ]] : expr = [[ ( '(' PS ')' ) E ]]
Rule
[[ '-' E ]] : expr = [[ ( '(' '~-' ')' ) E ]]
Rule
[[ '-.' E ]] : expr = [[ ( '(' '~-.' ')' ) E ]]
Rule
[[ E1 IO-1 E2 ]] : expr = [[ ( '(' IO-1 ')' ) E1 E2 ]]
Rule
[[ E1 IO-2 E2 ]] : expr = [[ ( '(' IO-2 ')' ) E1 E2 ]]
Rule
[[ E1 IO-3 E2 ]] : expr = [[ ( '(' IO-3 ')' ) E1 E2 ]]
Rule
[[ E1 IO-4 E2 ]] : expr = [[ ( '(' IO-4 ')' ) E1 E2 ]]
Rule
[[ E1 IO-5 E2 ]] : expr = [[ ( '(' IO-5 ')' ) E1 E2 ]]
Rule
[[ E1 '&' E2 ]] : expr = [[ E1 '&&' E2 ]]
Rule
[[ E1 'or' E2 ]] : expr = [[ E1 '||' E2 ]]
Rule
[[ E1 IO-8 E2 ]] : expr = [[ ( '(' IO-8 ')' ) E1 E2 ]]
Rule
[[ E1 '.(' E2 ')' ]] : expr = [[ 'array_get' E1 E2 ]]
Rule
[[ E1 '.(' E2 ')' '<-' E3 ]] : expr = [[ 'array_set' E1 E2 E3 ]]
Rule
[[ 'if' E1 'then' E2 ]] : expr = [[ 'if' E1 'then' E2 'else' ( '(' ')' ) ]]
Rule
[[ 'fun' P '->' E ]] : expr = [[ 'function' P '->' E ]]
Rule
[[ 'fun' P P+ '->' E ]] : expr = [[ 'fun' P '->' ( 'fun' P+ '->' E ) ]]
Rule
[[ '[' E SE* ';' ']' ]] : expr = [[ '[' E SE* ']' ]]
Rule
[[ '[|' E SE* ';' '|]' ]] : expr = [[ '[|' E SE* '|]' ]]
Rule
[[ '{' F '=' E SFE* ';' '}' ]] : expr = [[ '{' F '=' E SFE* '}' ]]
Rule
[[ '{' E1 'with' F '=' E2 SFE* ';' '}' ]] : expr =
[[ '{' E1 'with' F '=' E2 SFE* '}' ]]
Rule
[[ '|' P '->' E PE* ]] : pattern-matching = [[ P '->' E PE* ]]
Rule
[[ VN ':' PT '=' E ]] : let-binding = [[ VN '=' E ]]
Rule
[[ VN P+ '=' E ]] : let-binding = [[ VN '=' ( 'fun' P+ '->' E ) ]]
Semantics
evaluate[[ _:expr ]] : =>implemented-values
Rule
evaluate[[ VP ]] = bound(value-name[[ VP ]])
Rule
evaluate[[ CNST ]] = value[[ CNST ]]
Rule
evaluate[[ '(' E ':' T ')' ]] = evaluate[[ E ]]
Rule
evaluate[[ E1 ',' E2 CE* ]] =
tuple( evaluate-comma-sequence[[ E1 ',' E2 CE* ]] )
Rule
evaluate[[ E1 '::' E2 ]] = cons(evaluate[[ E1 ]], evaluate[[ E2 ]])
Rule
evaluate[[ '[' E SE* ']' ]] = [ evaluate-semic-sequence [[ E SE* ]] ]
Rule
evaluate[[ '[|' E SE* '|]' ]] =
vector(left-to-right-map(
allocate-initialised-variable(implemented-values, given),
evaluate-semic-sequence[[ E SE* ]]))
Rule
evaluate[[ '[|' '|]' ]] = vector( )
Rule
evaluate[[ '{' F '=' E SFE* '}' ]] =
record(collateral( evaluate-field-sequence[[ F '=' E SFE* ]] ))
Rule
evaluate[[ '{' E1 'with' F '=' E2 SFE* '}' ]] =
record(
map-override(
evaluate-field-sequence[[ F '=' E2 SFE* ]],
checked record-map(evaluate[[E1]])))
Rule
evaluate[[ CSTR E ]] =
variant(constr-name[[ CSTR ]], evaluate[[ E ]])
Otherwise
evaluate[[ E1 E2 ]] =
apply(evaluate[[ E1 ]], evaluate[[ E2 ]])
Rule
evaluate[[ E '.' F ]] =
record-select(evaluate[[ E ]], field-name[[ F ]])
Rule
evaluate[[ E1 '&&' E2 ]] =
if-true-else(evaluate[[ E1 ]], evaluate[[ E2 ]], false)
Rule
evaluate[[ E1 '||' E2 ]] =
if-true-else(evaluate[[ E1 ]], true, evaluate[[ E2 ]])
Rule
evaluate[[ 'if' E1 'then' E2 'else' E3 ]] =
if-true-else(evaluate[[ E1 ]], evaluate[[ E2 ]], evaluate[[ E3 ]])
Rule
evaluate[[ 'while' E1 'do' E2 'done' ]] =
while(evaluate[[ E1 ]], effect(evaluate[[ E2 ]]))
Rule
evaluate[[ 'for' VN '=' E1 'to' E2 'do' E3 'done' ]] =
effect(left-to-right-map(
case-match(pattern-bind(value-name[[ VN ]]), evaluate[[ E3 ]]),
integer-sequence(evaluate[[ E1 ]], evaluate[[ E2 ]])))
Rule
evaluate[[ 'for' VN '=' E1 'downto' E2 'do' E3 'done' ]] =
effect(left-to-right-map(
case-match(pattern-bind(value-name[[ VN ]]), evaluate[[ E3 ]]),
reverse integer-sequence(evaluate[[ E2 ]], evaluate[[ E1 ]])))
Rule
evaluate[[ E1 ';' E2 ]] =
sequential(effect(evaluate[[ E1 ]]), evaluate[[ E2 ]])
Rule
evaluate[[ 'match' E 'with' PM ]] =
give(evaluate[[ E ]],
else(match[[ PM ]], throw(ocaml-light-match-failure)))
Rule
evaluate[[ 'function' PM ]] =
function closure(
else(match[[ PM ]], throw(ocaml-light-match-failure)))
Rule
evaluate[[ 'try' E 'with' PM ]] =
handle-thrown(
evaluate[[ E ]],
else(match[[ PM ]], throw(given)))
Rule
evaluate[[ LD 'in' E ]] = scope(define-values[[ LD ]], evaluate[[ E ]])
Rule
evaluate [[ 'assert' E ]] =
else(check-true(evaluate[[ E ]]), throw(ocaml-light-assert-failure))
## Expression sequences and maps
Semantics
evaluate-comma-sequence[[ _:(expr comma-expr*) ]] : (=>implemented-values)+
Rule
evaluate-comma-sequence[[ E1 ',' E2 CE* ]] =
evaluate[[ E1 ]], evaluate-comma-sequence[[ E2 CE* ]]
Rule
evaluate-comma-sequence[[ E ]] = evaluate[[ E ]]
Semantics
evaluate-semic-sequence[[ _:(expr semic-expr*) ]] : (=>implemented-values)+
Rule
evaluate-semic-sequence[[ E1 ';' E2 SE* ]] =
evaluate[[ E1 ]], evaluate-semic-sequence[[ E2 SE* ]]
Rule
evaluate-semic-sequence[[ E ]] = evaluate[[ E ]]
Semantics
evaluate-field-sequence[[ _:(field '=' expr semic-field-expr*) ]] : (=>envs)+
Rule
evaluate-field-sequence[[ F1 '=' E1 ';' F2 '=' E2 SFE* ]] =
{ field-name[[ F1 ]] |-> evaluate[[ E1 ]] },
evaluate-field-sequence[[ F2 '=' E2 SFE* ]]
Rule
evaluate-field-sequence[[ F '=' E ]] = { field-name[[ F ]] |-> evaluate[[ E ]] }
## Matching
Semantics
match[[ _:pattern-matching ]] : (implemented-values=>implemented-values)+
Rule
match[[ P1 '->' E1 '|' P2 '->' E2 PE* ]] =
match[[ P1 '->' E1 ]], match[[ P2 '->' E2 PE* ]]
Rule
match[[ P '->' E ]] = case-match(evaluate-pattern[[ P ]], evaluate[[ E ]])
## Value definitions
Semantics
define-values[[ _:let-definition ]] : =>environments
Rule
define-values[[ 'let' LB ALB* ]] = define-values-nonrec[[ LB ALB* ]]
Rule
define-values[[ 'let rec' LB ALB* ]] =
recursive(
set(bound-ids-sequence[[ LB ALB* ]]),
define-values-nonrec[[ LB ALB* ]])
Semantics
define-values-nonrec[[ _:(let-binding and-let-binding*) ]] : =>environments
Rule
define-values-nonrec[[ LB1 'and' LB2 ALB* ]] =
collateral(define-values-nonrec[[ LB1 ]], define-values-nonrec[[ LB2 ALB* ]])
Rule
define-values-nonrec[[ P '=' E ]] =
else(
match(evaluate[[ E ]], evaluate-pattern[[ P ]]),
throw(ocaml-light-match-failure))
Semantics
bound-ids-sequence[[ _:(let-binding and-let-binding*) ]] : ids+
Rule
bound-ids-sequence[[ LB ]] = bound-id[[ LB ]]
Rule
bound-ids-sequence[[ LB1 'and' LB2 ALB* ]] =
bound-id[[ LB1 ]], bound-ids-sequence[[ LB2 ALB* ]]
Semantics
bound-id[[ _:let-binding ]] : ids
Rule
bound-id[[ VN '=' E ]] = value-name[[ VN ]]
Otherwise
bound-id[[ LB ]] = fail
// implementation-dependent