Language "OCaml Light"

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))

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 ]] }

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 ]])

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