Link Search Menu Expand Document
CBS-beta
% cbs-katex.sty % \newcommand{\STYLE}[2]{\htmlClass{cbs-#1}{#2}} \newcommand{\DECL}[3]{\htmlId{#1:#2}{#3}} \newcommand{\REF}[3]{\href{###1:#2}{#3}} \newcommand{\HYPER}[5]{\href{#1/#2/index.html###3:#4}{#5}} % \SHADE{MATH} can be defined to produce a shaded background to highlight % inline MATH in running text: \newcommand{\SHADE}[1]{#1} % \KEY{TEXT}, \STRING{TEXT}, \ATOM{TEXT}, \LEX{TEXT} can be used in math mode: \newcommand{\KEY}[1]{\textsf{\textit{\STYLE{Key}{#1}}}} \newcommand{\STRING}[1]{\textsf{``\texttt{#1}''}} \newcommand{\ATOM}[1]{\textsf{`\texttt{#1}'}} \newcommand{\LEX}[1]{\textsf{\STYLE{Key}{`}\texttt{#1}\STYLE{Key}{'}}} % The following commands produce ASCII characters that are treated specially by LaTeX: \newcommand{\HASH}{\char`\#} \newcommand{\DOLLAR}{\char`\$} \newcommand{\PERCENT}{\char`\%} \newcommand{\AMPERSAND}{\char`\&} \newcommand{\APOSTROPHE}{\char`\'} \newcommand{\BACKSLASH}{\char`\\} \newcommand{\CARET}{\char`\^} \newcommand{\UNDERSCORE}{\char`\_} \newcommand{\GRAVE}{\char`\`} \newcommand{\LEFTBRACE}{\char`\{} \newcommand{\RIGHTBRACE}{\char`\}} \newcommand{\TILDE}{\textasciitilde} % {\char`\~} % \NAME{name} highlights the name; % \NAMEDECL{name} declares Name.name as the target of links to name; % \NAMEREF{name} links name to the target Name.name in the current file; % \NAMEHYPER{url}{file}{name} links name to Name.name at url/file/file.pdf. % Similarly for \VAR{partvariable}, \SYN{syntaxname}, \SEM{semanticsName}, % and \SECT{sectionnumber} % The kerns in \SUB and \VAR avoid overlaps with primes: \newcommand{\SUB}[1]{_{\kern-2mu\STYLE{PartVariable}{\textsf{#1}}}} % PLAIN \newcommand{\VAR}[1]{\STYLE{PartVariable}{\textsf{\textit{#1}\kern2mu}}} \newcommand{\NAME}[1]{\STYLE{Name}{\textsf{#1}}} \newcommand{\SYN}[1]{\STYLE{SyntaxName}{\textsf{#1}}} \newcommand{\SEM}[1]{\STYLE{SemanticsName}{\textsf{#1}}} \newcommand{\SECT}[1]{\STYLE{SectionNumber}{\textsf{#1}}} % DECL \newcommand{\VARDECL}[1]{\DECL{PartVariable}{#1}{\VAR{#1}}} \newcommand{\NAMEDECL}[1]{\DECL{Name}{#1}{\NAME{#1}}} \newcommand{\SYNDECL}[1]{\DECL{SyntaxName}{#1}{\SYN{#1}}} \newcommand{\SEMDECL}[1]{\DECL{SemanticsName}{#1}{\SEM{#1}}} \newcommand{\SECTDECL}[1]{\DECL{SectionNumber}{#1}{\textsf{#1}}} % REF \newcommand{\VARREF}[1]{\REF{PartVariable}{#1}{\VAR{#1}}} \newcommand{\NAMEREF}[1]{\REF{Name}{#1}{\NAME{#1}}} \newcommand{\SYNREF}[1]{\REF{SyntaxName}{#1}{\SYN{#1}}} \newcommand{\SEMREF}[1]{\REF{SemanticsName}{#1}{\SEM{#1}}} \newcommand{\SECTREF}[1]{\REF{SectionNumber}{#1}{\SECT{#1}}} % HYPER \newcommand{\VARHYPER}[3]{\HYPER{#1}{#2}{PartVariable}{#3}{\VAR{#3}}} \newcommand{\NAMEHYPER}[3]{\HYPER{#1}{#2}{Name}{#3}{\NAME{#3}}} \newcommand{\SYNHYPER}[3]{\HYPER{#1}{#2}{SyntaxName}{#3}{\SYN{#3}}} \newcommand{\SEMHYPER}[3]{\HYPER{#1}{#2}{SemanticsName}{#3}{\SEM{#3}}} \newcommand{\SECTHYPER}[3]{\HYPER{#1}{#2}{SectionNumber}{#3}{\SECT{#3}}} % \LEFTPHRASE MATH \RIGHTPHRASE produces [[ MATH ]] with proper brackets: \newcommand{\LEFTPHRASE}{\llbracket} \newcommand{\RIGHTPHRASE}{\rrbracket} % \LEFTGROUP MATH \RIGHTGROUP produces ( MATH ) where the parentheses are % highlighted the same as keywords: \newcommand{\LEFTGROUP}{\STYLE{Key}{(}} \newcommand{\RIGHTGROUP}{\STYLE{Key}{)}} % MATH\PLUS produces a superscript + % MATH\STAR produces a superscript * % MATH\QUERY produces a superscript ? \newcommand{\PLUS}{{}^{\texttt{+}}} \newcommand{\STAR}{{}^{\texttt{*}}} \newcommand{\QUERY}{{}^{\texttt{?}}} % \RULE{& PREMISE \\ & ...}{& FORMULA ... \\ & ...} produces an inference rule % with separately aligned premises and conclusion % PREMISE % ... % ----------- % FORMULA ... % ... \newcommand{\RULE}[2] {\frac{\begin{aligned}#1\end{aligned}}{\begin{aligned}#2\end{aligned}}} % \AXIOM{& FORMULA ... \\ & ...} produces an aligned formula % % FORMULA ... % ... \newcommand{\AXIOM}[1]{\begin{aligned}#1\end{aligned}} % \TO TYPE produces => TYPE \newcommand{\TO}{\mathop{\Rightarrow}} % TERM \TRANS TERM produces TERM ---> TERM \newcommand{\TRANS}{\longrightarrow} % TERM \xrightarrow{LABEL} TERM puts the label above the long arrow %

Languages-beta : OC-L-07-Expressions.cbs | PLAIN | PDF

OUTLINE
Language“OCaml Light”\KEY{Language} \quad \STRING{OCaml Light}

7\SECT{7} Expressions

SyntaxE:expr ::=  value-path ∣  constant ∣  ‘(’ expr ‘)’ ∣  ‘begin’ expr ‘end’ ∣  ‘(’ expr ‘:’ typexpr ‘)’ ∣  expr comma-expr+ ∣  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’ exprA:argument ::=  exprPM: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 ∣  value-name ‘:’ poly-typexpr ‘=’ exprALB:and-let-binding ::=  ‘and’ let-bindingCE:comma-expr ::=  ‘,’ exprSE:semic-expr ::=  ‘;’ exprSFE:semic-field-expr ::=  ‘;’ field ‘=’ exprPE:pattern-expr ::=  ‘|’ pattern ‘->’ expr\begin{align*} \KEY{Syntax} \quad \VARDECL{E} : \SYNDECL{expr} \ ::= \ & \ \SYNHYPER{../.}{OC-L-03-Names}{value-path} \\ \ \mid \ & \ \SYNHYPER{../.}{OC-L-05-Constants}{constant} \\ \ \mid \ & \ \LEX{{(}} \ \SYNREF{expr} \ \LEX{{)}} \\ \ \mid \ & \ \LEX{begin} \ \SYNREF{expr} \ \LEX{end} \\ \ \mid \ & \ \LEX{{(}} \ \SYNREF{expr} \ \LEX{{:}} \ \SYNHYPER{../.}{OC-L-04-Type-Expressions}{typexpr} \ \LEX{{)}} \\ \ \mid \ & \ \SYNREF{expr} \ \SYNREF{comma-expr}\PLUS \\ \ \mid \ & \ \SYNREF{expr} \ \LEX{{:}{:}} \ \SYNREF{expr} \\ \ \mid \ & \ \LEX{{[}} \ \SYNREF{expr} \ \SYNREF{semic-expr}\STAR \ \LEX{{]}} \\ \ \mid \ & \ \LEX{{[}} \ \SYNREF{expr} \ \SYNREF{semic-expr}\STAR \ \LEX{{;}} \ \LEX{{]}} \\ \ \mid \ & \ \LEX{{[}{|}} \ \SYNREF{expr} \ \SYNREF{semic-expr}\STAR \ \LEX{{|}{]}} \\ \ \mid \ & \ \LEX{{[}{|}} \ \SYNREF{expr} \ \SYNREF{semic-expr}\STAR \ \LEX{{;}} \ \LEX{{|}{]}} \\ \ \mid \ & \ \LEX{{\LEFTBRACE}} \ \SYNHYPER{../.}{OC-L-03-Names}{field} \ \LEX{{=}} \ \SYNREF{expr} \ \SYNREF{semic-field-expr}\STAR \ \LEX{{\RIGHTBRACE}} \\ \ \mid \ & \ \LEX{{\LEFTBRACE}} \ \SYNHYPER{../.}{OC-L-03-Names}{field} \ \LEX{{=}} \ \SYNREF{expr} \ \SYNREF{semic-field-expr}\STAR \ \LEX{{;}} \ \LEX{{\RIGHTBRACE}} \\ \ \mid \ & \ \LEX{{\LEFTBRACE}} \ \SYNREF{expr} \ \LEX{with} \ \SYNHYPER{../.}{OC-L-03-Names}{field} \ \LEX{{=}} \ \SYNREF{expr} \ \SYNREF{semic-field-expr}\STAR \ \LEX{{\RIGHTBRACE}} \\ \ \mid \ & \ \LEX{{\LEFTBRACE}} \ \SYNREF{expr} \ \LEX{with} \ \SYNHYPER{../.}{OC-L-03-Names}{field} \ \LEX{{=}} \ \SYNREF{expr} \ \SYNREF{semic-field-expr}\STAR \ \LEX{{;}} \ \LEX{{\RIGHTBRACE}} \\ \ \mid \ & \ \SYNREF{expr} \ \SYNREF{argument}\PLUS \\ \ \mid \ & \ \SYNHYPER{../.}{OC-L-01-Lexical-Conventions}{prefix-symbol} \ \SYNREF{expr} \\ \ \mid \ & \ \LEX{{-}} \ \SYNREF{expr} \\ \ \mid \ & \ \LEX{{-}{.}} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNREF{expr} \ \SYNHYPER{../.}{OC-L-03-Names}{infix-op-1} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNREF{expr} \ \SYNHYPER{../.}{OC-L-03-Names}{infix-op-2} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNREF{expr} \ \SYNHYPER{../.}{OC-L-03-Names}{infix-op-3} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNREF{expr} \ \SYNHYPER{../.}{OC-L-03-Names}{infix-op-4} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNREF{expr} \ \SYNHYPER{../.}{OC-L-03-Names}{infix-op-5} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNREF{expr} \ \SYNHYPER{../.}{OC-L-03-Names}{infix-op-6} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNREF{expr} \ \SYNHYPER{../.}{OC-L-03-Names}{infix-op-7} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNREF{expr} \ \SYNHYPER{../.}{OC-L-03-Names}{infix-op-8} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNREF{expr} \ \LEX{{.}} \ \SYNHYPER{../.}{OC-L-03-Names}{field} \\ \ \mid \ & \ \SYNREF{expr} \ \LEX{{.}{(}} \ \SYNREF{expr} \ \LEX{{)}} \\ \ \mid \ & \ \SYNREF{expr} \ \LEX{{.}{(}} \ \SYNREF{expr} \ \LEX{{)}} \ \LEX{{<}{-}} \ \SYNREF{expr} \\ \ \mid \ & \ \LEX{if} \ \SYNREF{expr} \ \LEX{then} \ \SYNREF{expr} \ \LEFTGROUP \LEX{else} \ \SYNREF{expr} \RIGHTGROUP\QUERY \\ \ \mid \ & \ \LEX{while} \ \SYNREF{expr} \ \LEX{do} \ \SYNREF{expr} \ \LEX{done} \\ \ \mid \ & \ \LEX{for} \ \SYNHYPER{../.}{OC-L-03-Names}{value-name} \ \LEX{{=}} \ \SYNREF{expr} \ \LEFTGROUP \LEX{to} \mid \LEX{downto} \RIGHTGROUP \ \SYNREF{expr} \ \LEX{do} \ \SYNREF{expr} \ \LEX{done} \\ \ \mid \ & \ \SYNREF{expr} \ \LEX{{;}} \ \SYNREF{expr} \\ \ \mid \ & \ \LEX{match} \ \SYNREF{expr} \ \LEX{with} \ \SYNREF{pattern-matching} \\ \ \mid \ & \ \LEX{function} \ \SYNREF{pattern-matching} \\ \ \mid \ & \ \LEX{fun} \ \SYNHYPER{../.}{OC-L-06-Patterns}{pattern}\PLUS \ \LEX{{-}{>}} \ \SYNREF{expr} \\ \ \mid \ & \ \LEX{try} \ \SYNREF{expr} \ \LEX{with} \ \SYNREF{pattern-matching} \\ \ \mid \ & \ \SYNREF{let-definition} \ \LEX{in} \ \SYNREF{expr} \\ \ \mid \ & \ \LEX{assert} \ \SYNREF{expr} \\ \VARDECL{A} : \SYNDECL{argument} \ ::= \ & \ \SYNREF{expr} \\ \VARDECL{PM} : \SYNDECL{pattern-matching} \ ::= \ & \ \SYNHYPER{../.}{OC-L-06-Patterns}{pattern} \ \LEX{{-}{>}} \ \SYNREF{expr} \ \SYNREF{pattern-expr}\STAR \\ \ \mid \ & \ \LEX{{|}} \ \SYNHYPER{../.}{OC-L-06-Patterns}{pattern} \ \LEX{{-}{>}} \ \SYNREF{expr} \ \SYNREF{pattern-expr}\STAR \\ \VARDECL{LD} : \SYNDECL{let-definition} \ ::= \ & \ \LEX{let} \ \LEFTGROUP \LEX{rec} \RIGHTGROUP\QUERY \ \SYNREF{let-binding} \ \SYNREF{and-let-binding}\STAR \\ \VARDECL{LB} : \SYNDECL{let-binding} \ ::= \ & \ \SYNHYPER{../.}{OC-L-06-Patterns}{pattern} \ \LEX{{=}} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNHYPER{../.}{OC-L-03-Names}{value-name} \ \SYNHYPER{../.}{OC-L-06-Patterns}{pattern}\PLUS \ \LEX{{=}} \ \SYNREF{expr} \\ \ \mid \ & \ \SYNHYPER{../.}{OC-L-03-Names}{value-name} \ \LEX{{:}} \ \SYNHYPER{../.}{OC-L-04-Type-Expressions}{poly-typexpr} \ \LEX{{=}} \ \SYNREF{expr} \\ \VARDECL{ALB} : \SYNDECL{and-let-binding} \ ::= \ & \ \LEX{and} \ \SYNREF{let-binding} \\ \VARDECL{CE} : \SYNDECL{comma-expr} \ ::= \ & \ \LEX{{,}} \ \SYNREF{expr} \\ \VARDECL{SE} : \SYNDECL{semic-expr} \ ::= \ & \ \LEX{{;}} \ \SYNREF{expr} \\ \VARDECL{SFE} : \SYNDECL{semic-field-expr} \ ::= \ & \ \LEX{{;}} \ \SYNHYPER{../.}{OC-L-03-Names}{field} \ \LEX{{=}} \ \SYNREF{expr} \\ \VARDECL{PE} : \SYNDECL{pattern-expr} \ ::= \ & \ \LEX{{|}} \ \SYNHYPER{../.}{OC-L-06-Patterns}{pattern} \ \LEX{{-}{>}} \ \SYNREF{expr} \end{align*} 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* ⟧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) ⟧\begin{align*} \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{{(}} \ \VARREF{E} \ \LEX{{)}} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{begin} \ \VARREF{E} \ \LEX{end} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{{(}} \ \VARREF{E} \ \LEX{{:}} \ \VARHYPER{../.}{OC-L-04-Type-Expressions}{T} \ \LEX{{)}} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \VARREF{E}\SUB{2} \ \VARREF{A} \ \VARREF{A}\STAR \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEFTGROUP \LEX{{(}} \ \VAR{E}\SUB{1} \ \VAR{E}\SUB{2} \ \LEX{{)}} \RIGHTGROUP \ \VAR{A} \ \VAR{A}\STAR \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARHYPER{../.}{OC-L-01-Lexical-Conventions}{PS} \ \VARREF{E} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEFTGROUP \LEX{{(}} \ \VAR{PS} \ \LEX{{)}} \RIGHTGROUP \ \VAR{E} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{{-}} \ \VARREF{E} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEFTGROUP \LEX{{(}} \ \LEX{{\TILDE}{-}} \ \LEX{{)}} \RIGHTGROUP \ \VAR{E} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{{-}{.}} \ \VARREF{E} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEFTGROUP \LEX{{(}} \ \LEX{{\TILDE}{-}{.}} \ \LEX{{)}} \RIGHTGROUP \ \VAR{E} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \VARHYPER{../.}{OC-L-03-Names}{IO-1} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEFTGROUP \LEX{{(}} \ \VAR{IO-1} \ \LEX{{)}} \RIGHTGROUP \ \VAR{E}\SUB{1} \ \VAR{E}\SUB{2} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \VARHYPER{../.}{OC-L-03-Names}{IO-2} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEFTGROUP \LEX{{(}} \ \VAR{IO-2} \ \LEX{{)}} \RIGHTGROUP \ \VAR{E}\SUB{1} \ \VAR{E}\SUB{2} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \VARHYPER{../.}{OC-L-03-Names}{IO-3} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEFTGROUP \LEX{{(}} \ \VAR{IO-3} \ \LEX{{)}} \RIGHTGROUP \ \VAR{E}\SUB{1} \ \VAR{E}\SUB{2} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \VARHYPER{../.}{OC-L-03-Names}{IO-4} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEFTGROUP \LEX{{(}} \ \VAR{IO-4} \ \LEX{{)}} \RIGHTGROUP \ \VAR{E}\SUB{1} \ \VAR{E}\SUB{2} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \VARHYPER{../.}{OC-L-03-Names}{IO-5} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEFTGROUP \LEX{{(}} \ \VAR{IO-5} \ \LEX{{)}} \RIGHTGROUP \ \VAR{E}\SUB{1} \ \VAR{E}\SUB{2} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{\AMPERSAND}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \VAR{E}\SUB{1} \ \LEX{{\AMPERSAND}{\AMPERSAND}} \ \VAR{E}\SUB{2} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{or} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \VAR{E}\SUB{1} \ \LEX{{|}{|}} \ \VAR{E}\SUB{2} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \VARHYPER{../.}{OC-L-03-Names}{IO-8} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEFTGROUP \LEX{{(}} \ \VAR{IO-8} \ \LEX{{)}} \RIGHTGROUP \ \VAR{E}\SUB{1} \ \VAR{E}\SUB{2} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{.}{(}} \ \VARREF{E}\SUB{2} \ \LEX{{)}} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEX{array{\UNDERSCORE}get} \ \VAR{E}\SUB{1} \ \VAR{E}\SUB{2} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{.}{(}} \ \VARREF{E}\SUB{2} \ \LEX{{)}} \ \LEX{{<}{-}} \ \VARREF{E}\SUB{3} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEX{array{\UNDERSCORE}set} \ \VAR{E}\SUB{1} \ \VAR{E}\SUB{2} \ \VAR{E}\SUB{3} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{if} \ \VARREF{E}\SUB{1} \ \LEX{then} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEX{if} \ \VAR{E}\SUB{1} \ \LEX{then} \ \VAR{E}\SUB{2} \ \LEX{else} \ \LEFTGROUP \LEX{{(}} \ \LEX{{)}} \RIGHTGROUP \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{fun} \ \VARHYPER{../.}{OC-L-06-Patterns}{P} \ \LEX{{-}{>}} \ \VARREF{E} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEX{function} \ \VAR{P} \ \LEX{{-}{>}} \ \VAR{E} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{fun} \ \VARHYPER{../.}{OC-L-06-Patterns}{P} \ \VARHYPER{../.}{OC-L-06-Patterns}{P}\PLUS \ \LEX{{-}{>}} \ \VARREF{E} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEX{fun} \ \VAR{P} \ \LEX{{-}{>}} \ \LEFTGROUP \LEX{fun} \ \VAR{P}\PLUS \ \LEX{{-}{>}} \ \VAR{E} \RIGHTGROUP \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{{[}} \ \VARREF{E} \ \VARREF{SE}\STAR \ \LEX{{;}} \ \LEX{{]}} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEX{{[}} \ \VAR{E} \ \VAR{SE}\STAR \ \LEX{{]}} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{{[}{|}} \ \VARREF{E} \ \VARREF{SE}\STAR \ \LEX{{;}} \ \LEX{{|}{]}} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEX{{[}{|}} \ \VAR{E} \ \VAR{SE}\STAR \ \LEX{{|}{]}} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{{\LEFTBRACE}} \ \VARHYPER{../.}{OC-L-03-Names}{F} \ \LEX{{=}} \ \VARREF{E} \ \VARREF{SFE}\STAR \ \LEX{{;}} \ \LEX{{\RIGHTBRACE}} \ \RIGHTPHRASE : \SYNREF{expr} = \LEFTPHRASE \ \LEX{{\LEFTBRACE}} \ \VAR{F} \ \LEX{{=}} \ \VAR{E} \ \VAR{SFE}\STAR \ \LEX{{\RIGHTBRACE}} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{{\LEFTBRACE}} \ \VARREF{E}\SUB{1} \ \LEX{with} \ \VARHYPER{../.}{OC-L-03-Names}{F} \ \LEX{{=}} \ \VARREF{E}\SUB{2} \ \VARREF{SFE}\STAR \ \LEX{{;}} \ \LEX{{\RIGHTBRACE}} \ \RIGHTPHRASE : \SYNREF{expr} = \\& \LEFTPHRASE \ \LEX{{\LEFTBRACE}} \ \VAR{E}\SUB{1} \ \LEX{with} \ \VAR{F} \ \LEX{{=}} \ \VAR{E}\SUB{2} \ \VAR{SFE}\STAR \ \LEX{{\RIGHTBRACE}} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{{|}} \ \VARHYPER{../.}{OC-L-06-Patterns}{P} \ \LEX{{-}{>}} \ \VARREF{E} \ \VARREF{PE}\STAR \ \RIGHTPHRASE : \SYNREF{pattern-matching} = \LEFTPHRASE \ \VAR{P} \ \LEX{{-}{>}} \ \VAR{E} \ \VAR{PE}\STAR \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARHYPER{../.}{OC-L-03-Names}{VN} \ \LEX{{:}} \ \VARHYPER{../.}{OC-L-04-Type-Expressions}{PT} \ \LEX{{=}} \ \VARREF{E} \ \RIGHTPHRASE : \SYNREF{let-binding} = \LEFTPHRASE \ \VAR{VN} \ \LEX{{=}} \ \VAR{E} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \LEFTPHRASE \ \VARHYPER{../.}{OC-L-03-Names}{VN} \ \VARHYPER{../.}{OC-L-06-Patterns}{P}\PLUS \ \LEX{{=}} \ \VARREF{E} \ \RIGHTPHRASE : \SYNREF{let-binding} = \LEFTPHRASE \ \VAR{VN} \ \LEX{{=}} \ \LEFTGROUP \LEX{fun} \ \VAR{P}\PLUS \ \LEX{{-}{>}} \ \VAR{E} \RIGHTGROUP \ \RIGHTPHRASE \end{align*} Semanticsevaluate⟦ _:expr ⟧:⇒implemented-valuesRuleevaluate⟦ VP ⟧=bound(value-name⟦ VP ⟧)Ruleevaluate⟦ CNST ⟧=value⟦ CNST ⟧Ruleevaluate⟦ ‘(’ E ‘:’ T ‘)’ ⟧=evaluate⟦ E ⟧Ruleevaluate⟦ E1 ‘,’ E2 CE* ⟧=tuple(evaluate-comma-sequence⟦ E1 ‘,’ E2 CE* ⟧)Ruleevaluate⟦ E1 ‘::’ E2 ⟧=cons(evaluate⟦ E1 ⟧,evaluate⟦ E2 ⟧)Ruleevaluate⟦ ‘[’ E SE* ‘]’ ⟧=[evaluate-semic-sequence⟦ E SE* ⟧]Ruleevaluate⟦ ‘[|’ E SE* ‘|]’ ⟧=vector(left-to-right-map(allocate-initialised-variable(implemented-values,given),evaluate-semic-sequence⟦ E SE* ⟧))Ruleevaluate⟦ ‘[|’ ‘|]’ ⟧=vector( )Ruleevaluate⟦ ‘{’ F ‘=’ E SFE* ‘}’ ⟧=record(collateral(evaluate-field-sequence⟦ F ‘=’ E SFE* ⟧))Ruleevaluate⟦ ‘{’ E1 ‘with’ F ‘=’ E2 SFE* ‘}’ ⟧=record(map-override(evaluate-field-sequence⟦ F ‘=’ E2 SFE* ⟧,checked record-map(evaluate⟦ E1 ⟧)))Ruleevaluate⟦ CSTR E ⟧=variant(constr-name⟦ CSTR ⟧,evaluate⟦ E ⟧)Otherwiseevaluate⟦ E1 E2 ⟧=apply(evaluate⟦ E1 ⟧,evaluate⟦ E2 ⟧)Ruleevaluate⟦ E ‘.’ F ⟧=record-select(evaluate⟦ E ⟧,field-name⟦ F ⟧)Ruleevaluate⟦ E1 ‘&&’ E2 ⟧=if-true-else(evaluate⟦ E1 ⟧,evaluate⟦ E2 ⟧,false)Ruleevaluate⟦ E1 ‘||’ E2 ⟧=if-true-else(evaluate⟦ E1 ⟧,true,evaluate⟦ E2 ⟧)Ruleevaluate⟦ ‘if’ E1 ‘then’ E2 ‘else’ E3 ⟧=if-true-else(evaluate⟦ E1 ⟧,evaluate⟦ E2 ⟧,evaluate⟦ E3 ⟧)Ruleevaluate⟦ ‘while’ E1 ‘do’ E2 ‘done’ ⟧=while(evaluate⟦ E1 ⟧,effect(evaluate⟦ E2 ⟧))Ruleevaluate⟦ ‘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 ⟧)))Ruleevaluate⟦ ‘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 ⟧)))Ruleevaluate⟦ E1 ‘;’ E2 ⟧=sequential(effect(evaluate⟦ E1 ⟧),evaluate⟦ E2 ⟧)Ruleevaluate⟦ ‘match’ E ‘with’ PM ⟧=give(evaluate⟦ E ⟧,else(match⟦ PM ⟧,throw(ocaml-light-match-failure)))Ruleevaluate⟦ ‘function’ PM ⟧=function closure(else(match⟦ PM ⟧,throw(ocaml-light-match-failure)))Ruleevaluate⟦ ‘try’ E ‘with’ PM ⟧=handle-thrown(evaluate⟦ E ⟧,else(match⟦ PM ⟧,throw(given)))Ruleevaluate⟦ LD ‘in’ E ⟧=scope(define-values⟦ LD ⟧,evaluate⟦ E ⟧)Ruleevaluate⟦ ‘assert’ E ⟧=else(check-true(evaluate⟦ E ⟧),throw(ocaml-light-assert-failure))\begin{align*} \KEY{Semantics} \quad & \SEMDECL{evaluate} \LEFTPHRASE \ \_ : \SYNREF{expr} \ \RIGHTPHRASE : \TO \NAMEHYPER{../.}{OC-L-02-Values}{implemented-values} \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARHYPER{../.}{OC-L-03-Names}{VP} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{bound} ( \SEMHYPER{../.}{OC-L-03-Names}{value-name} \LEFTPHRASE \ \VAR{VP} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARHYPER{../.}{OC-L-05-Constants}{CNST} \ \RIGHTPHRASE = \SEMHYPER{../.}{OC-L-05-Constants}{value} \LEFTPHRASE \ \VAR{CNST} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{{(}} \ \VARREF{E} \ \LEX{{:}} \ \VARHYPER{../.}{OC-L-04-Type-Expressions}{T} \ \LEX{{)}} \ \RIGHTPHRASE = \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{,}} \ \VARREF{E}\SUB{2} \ \VARREF{CE}\STAR \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple} ( \SEMREF{evaluate-comma-sequence} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \LEX{{,}} \ \VAR{E}\SUB{2} \ \VAR{CE}\STAR \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{:}{:}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{cons} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{{[}} \ \VARREF{E} \ \VARREF{SE}\STAR \ \LEX{{]}} \ \RIGHTPHRASE = [ \SEMREF{evaluate-semic-sequence} \LEFTPHRASE \ \VAR{E} \ \VAR{SE}\STAR \ \RIGHTPHRASE ] \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{{[}{|}} \ \VARREF{E} \ \VARREF{SE}\STAR \ \LEX{{|}{]}} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector} ( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{left-to-right-map} ( \\&\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{allocate-initialised-variable} ( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-values}, \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ), \\&\quad\quad\quad \SEMREF{evaluate-semic-sequence} \LEFTPHRASE \ \VAR{E} \ \VAR{SE}\STAR \ \RIGHTPHRASE ) ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{{[}{|}} \ \LEX{{|}{]}} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector} ( \ ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{{\LEFTBRACE}} \ \VARHYPER{../.}{OC-L-03-Names}{F} \ \LEX{{=}} \ \VARREF{E} \ \VARREF{SFE}\STAR \ \LEX{{\RIGHTBRACE}} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Records}{record} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{collateral} ( \SEMREF{evaluate-field-sequence} \LEFTPHRASE \ \VAR{F} \ \LEX{{=}} \ \VAR{E} \ \VAR{SFE}\STAR \ \RIGHTPHRASE ) ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{{\LEFTBRACE}} \ \VARREF{E}\SUB{1} \ \LEX{with} \ \VARHYPER{../.}{OC-L-03-Names}{F} \ \LEX{{=}} \ \VARREF{E}\SUB{2} \ \VARREF{SFE}\STAR \ \LEX{{\RIGHTBRACE}} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Records}{record} ( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{map-override} ( \\&\quad\quad\quad \SEMREF{evaluate-field-sequence} \LEFTPHRASE \ \VAR{F} \ \LEX{{=}} \ \VAR{E}\SUB{2} \ \VAR{SFE}\STAR \ \RIGHTPHRASE , \\&\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \ \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Records}{record-map} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE ) ) ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARHYPER{../.}{OC-L-03-Names}{CSTR} \ \VARREF{E} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant} ( \SEMHYPER{../.}{OC-L-03-Names}{constr-name} \LEFTPHRASE \ \VAR{CSTR} \ \RIGHTPHRASE , \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE ) \\ \KEY{Otherwise} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{apply} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARREF{E} \ \LEX{{.}} \ \VARHYPER{../.}{OC-L-03-Names}{F} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Records}{record-select} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE , \SEMHYPER{../.}{OC-L-03-Names}{field-name} \LEFTPHRASE \ \VAR{F} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{\AMPERSAND}{\AMPERSAND}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE , \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{false} ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{|}{|}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{true}, \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{if} \ \VARREF{E}\SUB{1} \ \LEX{then} \ \VARREF{E}\SUB{2} \ \LEX{else} \ \VARREF{E}\SUB{3} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE , \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{3} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{while} \ \VARREF{E}\SUB{1} \ \LEX{do} \ \VARREF{E}\SUB{2} \ \LEX{done} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{while} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{effect} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{for} \ \VARHYPER{../.}{OC-L-03-Names}{VN} \ \LEX{{=}} \ \VARREF{E}\SUB{1} \ \LEX{to} \ \VARREF{E}\SUB{2} \ \LEX{do} \ \VARREF{E}\SUB{3} \ \LEX{done} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{effect} ( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{left-to-right-map} ( \\&\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Patterns}{case-match} ( \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Patterns}{pattern-bind} ( \SEMHYPER{../.}{OC-L-03-Names}{value-name} \LEFTPHRASE \ \VAR{VN} \ \RIGHTPHRASE ), \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{3} \ \RIGHTPHRASE ), \\&\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-sequence} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) ) ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{for} \ \VARHYPER{../.}{OC-L-03-Names}{VN} \ \LEX{{=}} \ \VARREF{E}\SUB{1} \ \LEX{downto} \ \VARREF{E}\SUB{2} \ \LEX{do} \ \VARREF{E}\SUB{3} \ \LEX{done} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{effect} ( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{left-to-right-map} ( \\&\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Patterns}{case-match} ( \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Patterns}{pattern-bind} ( \SEMHYPER{../.}{OC-L-03-Names}{value-name} \LEFTPHRASE \ \VAR{VN} \ \RIGHTPHRASE ), \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{3} \ \RIGHTPHRASE ), \\&\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{reverse} \ \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-sequence} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE , \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE ) ) ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{;}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{effect} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE ), \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{match} \ \VARREF{E} \ \LEX{with} \ \VARREF{PM} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{give} ( \\&\quad\quad \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE , \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else} ( \SEMREF{match} \LEFTPHRASE \ \VAR{PM} \ \RIGHTPHRASE , \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw} ( \NAMEHYPER{../.}{OC-L-12-Core-Library}{ocaml-light-match-failure} ) ) ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{function} \ \VARREF{PM} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{function} \ \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Generic}{closure} ( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else} ( \SEMREF{match} \LEFTPHRASE \ \VAR{PM} \ \RIGHTPHRASE , \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw} ( \NAMEHYPER{../.}{OC-L-12-Core-Library}{ocaml-light-match-failure} ) ) ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{try} \ \VARREF{E} \ \LEX{with} \ \VARREF{PM} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{handle-thrown} ( \\&\quad\quad \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE , \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else} ( \SEMREF{match} \LEFTPHRASE \ \VAR{PM} \ \RIGHTPHRASE , \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ) ) ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \VARREF{LD} \ \LEX{in} \ \VARREF{E} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{scope} ( \SEMREF{define-values} \LEFTPHRASE \ \VAR{LD} \ \RIGHTPHRASE , \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{evaluate} \LEFTPHRASE \ \LEX{assert} \ \VARREF{E} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{check-true} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE ), \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw} ( \NAMEHYPER{../.}{OC-L-12-Core-Library}{ocaml-light-assert-failure} ) ) \end{align*}

Expression sequences and maps

Semanticsevaluate-comma-sequence⟦ _:(expr comma-expr*) ⟧:(⇒implemented-values)+Ruleevaluate-comma-sequence⟦ E1 ‘,’ E2 CE* ⟧=evaluate⟦ E1 ⟧,evaluate-comma-sequence⟦ E2 CE* ⟧Ruleevaluate-comma-sequence⟦ E ⟧=evaluate⟦ E ⟧\begin{align*} \KEY{Semantics} \quad & \SEMDECL{evaluate-comma-sequence} \LEFTPHRASE \ \_ : \LEFTGROUP \SYNREF{expr} \ \SYNREF{comma-expr}\STAR \RIGHTGROUP \ \RIGHTPHRASE : ( \TO \NAMEHYPER{../.}{OC-L-02-Values}{implemented-values} )\PLUS \\ \KEY{Rule} \quad & \SEMREF{evaluate-comma-sequence} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{,}} \ \VARREF{E}\SUB{2} \ \VARREF{CE}\STAR \ \RIGHTPHRASE = \\&\quad \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{evaluate-comma-sequence} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \VAR{CE}\STAR \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \SEMREF{evaluate-comma-sequence} \LEFTPHRASE \ \VARREF{E} \ \RIGHTPHRASE = \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE \end{align*} Semanticsevaluate-semic-sequence⟦ _:(expr semic-expr*) ⟧:(⇒implemented-values)+Ruleevaluate-semic-sequence⟦ E1 ‘;’ E2 SE* ⟧=evaluate⟦ E1 ⟧,evaluate-semic-sequence⟦ E2 SE* ⟧Ruleevaluate-semic-sequence⟦ E ⟧=evaluate⟦ E ⟧\begin{align*} \KEY{Semantics} \quad & \SEMDECL{evaluate-semic-sequence} \LEFTPHRASE \ \_ : \LEFTGROUP \SYNREF{expr} \ \SYNREF{semic-expr}\STAR \RIGHTGROUP \ \RIGHTPHRASE : ( \TO \NAMEHYPER{../.}{OC-L-02-Values}{implemented-values} )\PLUS \\ \KEY{Rule} \quad & \SEMREF{evaluate-semic-sequence} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{;}} \ \VARREF{E}\SUB{2} \ \VARREF{SE}\STAR \ \RIGHTPHRASE = \\&\quad \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{evaluate-semic-sequence} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \VAR{SE}\STAR \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \SEMREF{evaluate-semic-sequence} \LEFTPHRASE \ \VARREF{E} \ \RIGHTPHRASE = \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE \end{align*} Semanticsevaluate-field-sequence⟦ _:(field ‘=’ expr semic-field-expr*) ⟧:(⇒envs)+Ruleevaluate-field-sequence⟦ F1 ‘=’ E1 ‘;’ F2 ‘=’ E2 SFE* ⟧={field-name⟦ F1 ⟧↦evaluate⟦ E1 ⟧},evaluate-field-sequence⟦ F2 ‘=’ E2 SFE* ⟧Ruleevaluate-field-sequence⟦ F ‘=’ E ⟧={field-name⟦ F ⟧↦evaluate⟦ E ⟧}\begin{align*} \KEY{Semantics} \quad & \SEMDECL{evaluate-field-sequence} \LEFTPHRASE \ \_ : \LEFTGROUP \SYNHYPER{../.}{OC-L-03-Names}{field} \ \LEX{{=}} \ \SYNREF{expr} \ \SYNREF{semic-field-expr}\STAR \RIGHTGROUP \ \RIGHTPHRASE : ( \TO \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{envs} )\PLUS \\ \KEY{Rule} \quad & \SEMREF{evaluate-field-sequence} \LEFTPHRASE \ \VARHYPER{../.}{OC-L-03-Names}{F}\SUB{1} \ \LEX{{=}} \ \VARREF{E}\SUB{1} \ \LEX{{;}} \ \VARHYPER{../.}{OC-L-03-Names}{F}\SUB{2} \ \LEX{{=}} \ \VARREF{E}\SUB{2} \ \VARREF{SFE}\STAR \ \RIGHTPHRASE = \\&\quad \{ \SEMHYPER{../.}{OC-L-03-Names}{field-name} \LEFTPHRASE \ \VAR{F}\SUB{1} \ \RIGHTPHRASE \mapsto \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE \}, \\&\quad \SEMREF{evaluate-field-sequence} \LEFTPHRASE \ \VAR{F}\SUB{2} \ \LEX{{=}} \ \VAR{E}\SUB{2} \ \VAR{SFE}\STAR \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \SEMREF{evaluate-field-sequence} \LEFTPHRASE \ \VARHYPER{../.}{OC-L-03-Names}{F} \ \LEX{{=}} \ \VARREF{E} \ \RIGHTPHRASE = \{ \SEMHYPER{../.}{OC-L-03-Names}{field-name} \LEFTPHRASE \ \VAR{F} \ \RIGHTPHRASE \mapsto \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE \} \end{align*}

Matching

Semanticsmatch⟦ _:pattern-matching ⟧:(implemented-values⇒implemented-values)+Rulematch⟦ P1 ‘->’ E1 ‘|’ P2 ‘->’ E2 PE* ⟧=match⟦ P1 ‘->’ E1 ⟧,match⟦ P2 ‘->’ E2 PE* ⟧Rulematch⟦ P ‘->’ E ⟧=case-match(evaluate-pattern⟦ P ⟧,evaluate⟦ E ⟧)\begin{align*} \KEY{Semantics} \quad & \SEMDECL{match} \LEFTPHRASE \ \_ : \SYNREF{pattern-matching} \ \RIGHTPHRASE : ( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-values} \TO \NAMEHYPER{../.}{OC-L-02-Values}{implemented-values} )\PLUS \\ \KEY{Rule} \quad & \SEMREF{match} \LEFTPHRASE \ \VARHYPER{../.}{OC-L-06-Patterns}{P}\SUB{1} \ \LEX{{-}{>}} \ \VARREF{E}\SUB{1} \ \LEX{{|}} \ \VARHYPER{../.}{OC-L-06-Patterns}{P}\SUB{2} \ \LEX{{-}{>}} \ \VARREF{E}\SUB{2} \ \VARREF{PE}\STAR \ \RIGHTPHRASE = \\&\quad \SEMREF{match} \LEFTPHRASE \ \VAR{P}\SUB{1} \ \LEX{{-}{>}} \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{match} \LEFTPHRASE \ \VAR{P}\SUB{2} \ \LEX{{-}{>}} \ \VAR{E}\SUB{2} \ \VAR{PE}\STAR \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \SEMREF{match} \LEFTPHRASE \ \VARHYPER{../.}{OC-L-06-Patterns}{P} \ \LEX{{-}{>}} \ \VARREF{E} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Patterns}{case-match} ( \SEMHYPER{../.}{OC-L-06-Patterns}{evaluate-pattern} \LEFTPHRASE \ \VAR{P} \ \RIGHTPHRASE , \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE ) \end{align*}

Value definitions

Semanticsdefine-values⟦ _:let-definition ⟧:⇒environmentsRuledefine-values⟦ ‘let’ LB ALB* ⟧=define-values-nonrec⟦ LB ALB* ⟧Ruledefine-values⟦ ‘let rec’ LB ALB* ⟧=recursive(set(bound-ids-sequence⟦ LB ALB* ⟧),define-values-nonrec⟦ LB ALB* ⟧)\begin{align*} \KEY{Semantics} \quad & \SEMDECL{define-values} \LEFTPHRASE \ \_ : \SYNREF{let-definition} \ \RIGHTPHRASE : \TO \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{environments} \\ \KEY{Rule} \quad & \SEMREF{define-values} \LEFTPHRASE \ \LEX{let} \ \VARREF{LB} \ \VARREF{ALB}\STAR \ \RIGHTPHRASE = \SEMREF{define-values-nonrec} \LEFTPHRASE \ \VAR{LB} \ \VAR{ALB}\STAR \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \SEMREF{define-values} \LEFTPHRASE \ \LEX{let~rec} \ \VARREF{LB} \ \VARREF{ALB}\STAR \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{recursive} ( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sets}{set} ( \SEMREF{bound-ids-sequence} \LEFTPHRASE \ \VAR{LB} \ \VAR{ALB}\STAR \ \RIGHTPHRASE ), \\&\quad\quad \SEMREF{define-values-nonrec} \LEFTPHRASE \ \VAR{LB} \ \VAR{ALB}\STAR \ \RIGHTPHRASE ) \end{align*} Semanticsdefine-values-nonrec⟦ _:(let-binding and-let-binding*) ⟧:⇒environmentsRuledefine-values-nonrec⟦ LB1 ‘and’ LB2 ALB* ⟧=collateral(define-values-nonrec⟦ LB1 ⟧,define-values-nonrec⟦ LB2 ALB* ⟧)Ruledefine-values-nonrec⟦ P ‘=’ E ⟧=else(match(evaluate⟦ E ⟧,evaluate-pattern⟦ P ⟧),throw(ocaml-light-match-failure))\begin{align*} \KEY{Semantics} \quad & \SEMDECL{define-values-nonrec} \LEFTPHRASE \ \_ : \LEFTGROUP \SYNREF{let-binding} \ \SYNREF{and-let-binding}\STAR \RIGHTGROUP \ \RIGHTPHRASE : \TO \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{environments} \\ \KEY{Rule} \quad & \SEMREF{define-values-nonrec} \LEFTPHRASE \ \VARREF{LB}\SUB{1} \ \LEX{and} \ \VARREF{LB}\SUB{2} \ \VARREF{ALB}\STAR \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{collateral} ( \SEMREF{define-values-nonrec} \LEFTPHRASE \ \VAR{LB}\SUB{1} \ \RIGHTPHRASE , \SEMREF{define-values-nonrec} \LEFTPHRASE \ \VAR{LB}\SUB{2} \ \VAR{ALB}\STAR \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{define-values-nonrec} \LEFTPHRASE \ \VARHYPER{../.}{OC-L-06-Patterns}{P} \ \LEX{{=}} \ \VARREF{E} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else} ( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Patterns}{match} ( \SEMREF{evaluate} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE , \SEMHYPER{../.}{OC-L-06-Patterns}{evaluate-pattern} \LEFTPHRASE \ \VAR{P} \ \RIGHTPHRASE ), \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw} ( \NAMEHYPER{../.}{OC-L-12-Core-Library}{ocaml-light-match-failure} ) ) \end{align*} Semanticsbound-ids-sequence⟦ _:(let-binding and-let-binding*) ⟧:ids+Rulebound-ids-sequence⟦ LB ⟧=bound-id⟦ LB ⟧Rulebound-ids-sequence⟦ LB1 ‘and’ LB2 ALB* ⟧=bound-id⟦ LB1 ⟧,bound-ids-sequence⟦ LB2 ALB* ⟧\begin{align*} \KEY{Semantics} \quad & \SEMDECL{bound-ids-sequence} \LEFTPHRASE \ \_ : \LEFTGROUP \SYNREF{let-binding} \ \SYNREF{and-let-binding}\STAR \RIGHTGROUP \ \RIGHTPHRASE : \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{ids}\PLUS \\ \KEY{Rule} \quad & \SEMREF{bound-ids-sequence} \LEFTPHRASE \ \VARREF{LB} \ \RIGHTPHRASE = \SEMREF{bound-id} \LEFTPHRASE \ \VAR{LB} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \SEMREF{bound-ids-sequence} \LEFTPHRASE \ \VARREF{LB}\SUB{1} \ \LEX{and} \ \VARREF{LB}\SUB{2} \ \VARREF{ALB}\STAR \ \RIGHTPHRASE = \\&\quad \SEMREF{bound-id} \LEFTPHRASE \ \VAR{LB}\SUB{1} \ \RIGHTPHRASE , \SEMREF{bound-ids-sequence} \LEFTPHRASE \ \VAR{LB}\SUB{2} \ \VAR{ALB}\STAR \ \RIGHTPHRASE \end{align*} Semanticsbound-id⟦ _:let-binding ⟧:idsRulebound-id⟦ VN ‘=’ E ⟧=value-name⟦ VN ⟧Otherwisebound-id⟦ LB ⟧=fail\begin{align*} \KEY{Semantics} \quad & \SEMDECL{bound-id} \LEFTPHRASE \ \_ : \SYNREF{let-binding} \ \RIGHTPHRASE : \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{ids} \\ \KEY{Rule} \quad & \SEMREF{bound-id} \LEFTPHRASE \ \VARHYPER{../.}{OC-L-03-Names}{VN} \ \LEX{{=}} \ \VARREF{E} \ \RIGHTPHRASE = \SEMHYPER{../.}{OC-L-03-Names}{value-name} \LEFTPHRASE \ \VAR{VN} \ \RIGHTPHRASE \\ \KEY{Otherwise} \quad & \SEMREF{bound-id} \LEFTPHRASE \ \VARREF{LB} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{fail} \end{align*}

From the PLanCompS Project CBS-beta issues… Suggest an improvement…

← ↑ →