% 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-12-Core-Library.cbs | PLAIN | PDF
OUTLINE
Language “ OCaml Light ” \KEY{Language} \quad \STRING{OCaml Light} Language “ OCaml Light ”
12 \SECT{12} 12
[ Funcon ocaml-light-core-library Funcon ocaml-light-match-failure Funcon ocaml-light-is-structurally-equal Funcon ocaml-light-to-string Funcon ocaml-light-define-and-display Funcon ocaml-light-evaluate-and-display ] \begin{align*}
[ \
\KEY{Funcon} \quad & \NAMEREF{ocaml-light-core-library} \\
\KEY{Funcon} \quad & \NAMEREF{ocaml-light-match-failure} \\
\KEY{Funcon} \quad & \NAMEREF{ocaml-light-is-structurally-equal} \\
\KEY{Funcon} \quad & \NAMEREF{ocaml-light-to-string} \\
\KEY{Funcon} \quad & \NAMEREF{ocaml-light-define-and-display} \\
\KEY{Funcon} \quad & \NAMEREF{ocaml-light-evaluate-and-display}
\ ]
\end{align*} [ Funcon Funcon Funcon Funcon Funcon Funcon ocaml-light-core-library ocaml-light-match-failure ocaml-light-is-structurally-equal ocaml-light-to-string ocaml-light-define-and-display ocaml-light-evaluate-and-display ] Meta-variables R , S , S 1 , S 2 , S 3 , T , U < : values S * < : values * T + < : values + \begin{align*}
\KEY{Meta-variables} \quad
& \VAR{R}, \VAR{S}, \VAR{S}\SUB{1}, \VAR{S}\SUB{2}, \VAR{S}\SUB{3}, \VAR{T}, \VAR{U} <: \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values} \qquad \\& \VAR{S}\STAR <: \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values}\STAR \qquad \\& \VAR{T}\PLUS <: \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values}\PLUS
\end{align*} Meta-variables R , S , S 1 , S 2 , S 3 , T , U <: values S * <: values * T + <: values +
The following funcons take computations X \SHADE{\VAR{X}} X X \SHADE{\VAR{X}} X arg \SHADE{\NAMEREF{arg}} arg arg-1 \SHADE{\NAMEREF{arg-1}} arg-1 arg-2 \SHADE{\NAMEREF{arg-2}} arg-2 arg-3 \SHADE{\NAMEREF{arg-3}} arg-3
Auxiliary Funcon op-1 ( X : S ⇒ T ) : ⇒ functions ( S , T ) ⇝ function abstraction X \begin{align*}
\KEY{Auxiliary Funcon} \quad
& \NAMEDECL{op-1}(
\VAR{X} : \VAR{S} \TO \VAR{T})
: \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \VAR{S},
\VAR{T} ) \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{function} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Generic}{abstraction} \
\VAR{X}
\end{align*} Auxiliary Funcon op-1 ( X : S ⇒ T ) : ⇒ functions ( S , T ) ⇝ function abstraction X Auxiliary Funcon op-2 ( X : tuples ( S 1 , S 2 ) ⇒ T ) : ⇒ functions ( S 1 , functions ( S 2 , T ) ) ⇝ curry function abstraction X \begin{align*}
\KEY{Auxiliary Funcon} \quad
& \NAMEDECL{op-2}(
\VAR{X} : \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuples}
( \VAR{S}\SUB{1},
\VAR{S}\SUB{2} ) \TO \VAR{T})
: \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \VAR{S}\SUB{1},
\NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \VAR{S}\SUB{2},
\VAR{T} ) ) \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{curry} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{function} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Generic}{abstraction} \
\VAR{X}
\end{align*} Auxiliary Funcon op-2 ( X : tuples ( S 1 , S 2 ) ⇒ T ) : ⇒ functions ( S 1 , functions ( S 2 , T )) ⇝ curry function abstraction X Auxiliary Funcon op-3 ( X : tuples ( S 1 , S 2 , S 3 ) ⇒ T ) : ⇒ functions ( S 1 , functions ( S 2 , functions ( S 3 , T ) ) ) ⇝ function abstraction ( curry partial-apply-first ( function abstraction X , given ) ) \begin{align*}
\KEY{Auxiliary Funcon} \quad
& \NAMEDECL{op-3}(
\VAR{X} : \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuples}
( \VAR{S}\SUB{1},
\VAR{S}\SUB{2},
\VAR{S}\SUB{3} ) \TO \VAR{T})
: \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \VAR{S}\SUB{1},
\NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \VAR{S}\SUB{2},
\NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \VAR{S}\SUB{3},
\VAR{T} ) ) ) \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{function} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Generic}{abstraction}
( \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{curry} \
\NAMEREF{partial-apply-first}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{function} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Generic}{abstraction} \
\VAR{X},
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ) )
\end{align*} Auxiliary Funcon op-3 ( X : tuples ( S 1 , S 2 , S 3 ) ⇒ T ) : ⇒ functions ( S 1 , functions ( S 2 , functions ( S 3 , T ))) ⇝ function abstraction ( curry partial-apply-first ( function abstraction X , given )) Auxiliary Funcon partial-apply-first ( F : functions ( tuples ( R , S , T + ) , U ) , V : R ) : ⇒ functions ( tuples ( S , T + ) , U ) ⇝ function abstraction ( apply ( F , tuple ( V , tuple-elements given ) ) ) \begin{align*}
\KEY{Auxiliary Funcon} \quad
& \NAMEDECL{partial-apply-first}(
\VAR{F} : \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuples}
( \VAR{R},
\VAR{S},
\VAR{T}\PLUS ),
\VAR{U} ), \VAR{V} : \VAR{R}) \\&\quad
: \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuples}
( \VAR{S},
\VAR{T}\PLUS ),
\VAR{U} ) \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{function} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Generic}{abstraction}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{apply}
( \VAR{F},
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \VAR{V},
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple-elements} \
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ) ) )
\end{align*} Auxiliary Funcon partial-apply-first ( F : functions ( tuples ( R , S , T + ) , U ) , V : R ) : ⇒ functions ( tuples ( S , T + ) , U ) ⇝ function abstraction ( apply ( F , tuple ( V , tuple-elements given ))) partial-apply-first ( F , V ) \SHADE{\NAMEREF{partial-apply-first}
( \VAR{F},
\VAR{V} )} partial-apply-first ( F , V ) V \SHADE{\VAR{V}} V
Auxiliary Funcon arg : T ⇒ T ⇝ given \begin{align*}
\KEY{Auxiliary Funcon} \quad
& \NAMEDECL{arg}
: \VAR{T} \TO \VAR{T} \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given}
\end{align*} Auxiliary Funcon arg : T ⇒ T ⇝ given Auxiliary Funcon arg-1 : tuples ( S 1 , S * ) ⇒ S 1 ⇝ checked index ( 1 , tuple-elements given ) \begin{align*}
\KEY{Auxiliary Funcon} \quad
& \NAMEDECL{arg-1}
: \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuples}
( \VAR{S}\SUB{1},
\VAR{S}\STAR ) \TO \VAR{S}\SUB{1} \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{index}
( 1,
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple-elements} \
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} )
\end{align*} Auxiliary Funcon arg-1 : tuples ( S 1 , S * ) ⇒ S 1 ⇝ checked index ( 1 , tuple-elements given ) Auxiliary Funcon arg-2 : tuples ( S 1 , S 2 , S * ) ⇒ S 2 ⇝ checked index ( 2 , tuple-elements given ) \begin{align*}
\KEY{Auxiliary Funcon} \quad
& \NAMEDECL{arg-2}
: \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuples}
( \VAR{S}\SUB{1},
\VAR{S}\SUB{2},
\VAR{S}\STAR ) \TO \VAR{S}\SUB{2} \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{index}
( 2,
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple-elements} \
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} )
\end{align*} Auxiliary Funcon arg-2 : tuples ( S 1 , S 2 , S * ) ⇒ S 2 ⇝ checked index ( 2 , tuple-elements given ) Auxiliary Funcon arg-3 : tuples ( S 1 , S 2 , S 3 , S * ) ⇒ S 3 ⇝ checked index ( 3 , tuple-elements given ) \begin{align*}
\KEY{Auxiliary Funcon} \quad
& \NAMEDECL{arg-3}
: \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuples}
( \VAR{S}\SUB{1},
\VAR{S}\SUB{2},
\VAR{S}\SUB{3},
\VAR{S}\STAR ) \TO \VAR{S}\SUB{3} \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{index}
( 3,
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple-elements} \
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} )
\end{align*} Auxiliary Funcon arg-3 : tuples ( S 1 , S 2 , S 3 , S * ) ⇒ S 3 ⇝ checked index ( 3 , tuple-elements given )
The ocaml-light-core-library \SHADE{\NAMEREF{ocaml-light-core-library}} ocaml-light-core-library https://caml.inria.fr/pub/docs/manual-ocaml-4.06/core.html for further
details and comments.
It also maps some other names defined in the OCaml Standard Libarary to
funcon terms (to support tests using them without opening those modules).
Funcon ocaml-light-core-library : ⇒ environments ⇝ { “ Match_failure ” ↦ op-1 ( variant ( “ Match_failure ” , arg ) ) , “ Invalid_argument ” ↦ op-1 ( variant ( “ Invalid_argument ” , arg ) ) , “ Division_by_zero ” ↦ variant ( “ Division_by_zero ” , tuple ( ) ) , “ raise ” ↦ op-1 ( throw ( arg ) ) , “ (=) ” ↦ op-2 ( ocaml-light-is-structurally-equal ( arg-1 , arg-2 ) ) , “ (<>) ” ↦ op-2 ( not ( ocaml-light-is-structurally-equal ( arg-1 , arg-2 ) ) ) , “ (<) ” ↦ op-2 ( is-less ( arg-1 , arg-2 ) ) , “ (>) ” ↦ op-2 ( is-greater ( arg-1 , arg-2 ) ) , “ (<=) ” ↦ op-2 ( is-less-or-equal ( arg-1 , arg-2 ) ) , “ (>=) ” ↦ op-2 ( is-greater-or-equal ( arg-1 , arg-2 ) ) , “ min ” ↦ op-2 ( if-true-else ( is-less ( arg-1 , arg-2 ) , arg-1 , arg-2 ) ) , “ max ” ↦ op-2 ( if-true-else ( is-greater ( arg-1 , arg-2 ) , arg-1 , arg-2 ) ) , “ (==) ” ↦ op-2 ( if-true-else ( and ( is-in-type ( arg-1 , ground-values ) , is-in-type ( arg-2 , ground-values ) ) , is-equal ( arg-1 , arg-2 ) , throw ( variant ( “ Invalid_argument ” , “ equal: functional value ” ) ) ) ) , “ (!=) ” ↦ op-2 ( if-true-else ( and ( is-in-type ( arg-1 , ground-values ) , is-in-type ( arg-2 , ground-values ) ) , not is-equal ( arg-1 , arg-2 ) , throw ( variant ( “ Invalid_argument ” , “ equal: functional value ” ) ) ) ) , “ not ” ↦ op-1 ( not ( arg ) ) , “ (~-) ” ↦ op-1 ( implemented-integer integer-negate ( arg ) ) , “ (~+) ” ↦ op-1 ( implemented-integer arg ) , “ succ ” ↦ op-1 ( implemented-integer integer-add ( arg , 1 ) ) , “ pred ” ↦ op-1 ( implemented-integer integer-subtract ( arg , 1 ) ) , “ (+) ” ↦ op-2 ( implemented-integer integer-add ( arg-1 , arg-2 ) ) , “ (-) ” ↦ op-2 ( implemented-integer integer-subtract ( arg-1 , arg-2 ) ) , “ (*) ” ↦ op-2 ( implemented-integer integer-multiply ( arg-1 , arg-2 ) ) , “ (/) ” ↦ op-2 ( implemented-integer if-true-else ( is-equal ( arg-2 , 0 ) , throw ( variant ( “ Division_by_zero ” , tuple ( ) ) ) , checked integer-divide ( arg-1 , arg-2 ) ) ) , “ (mod) ” ↦ op-2 ( implemented-integer checked integer-modulo ( arg-1 , arg-2 ) ) , “ abs ” ↦ op-1 ( implemented-integer integer-absolute-value ( arg ) ) , “ max_int ” ↦ op-1 ( signed-bit-vector-maximum ( implemented-integers-width ) ) , “ min_int ” ↦ op-1 ( signed-bit-vector-minimum ( implemented-integers-width ) ) , “ (land) ” ↦ op-2 ( bit-vector-to-integer bit-vector-and ( implemented-bit-vector arg-1 , implemented-bit-vector arg-2 ) ) , “ (lor) ” ↦ op-2 ( bit-vector-to-integer bit-vector-or ( implemented-bit-vector arg-1 , implemented-bit-vector arg-2 ) ) , “ (lxor) ” ↦ op-2 ( bit-vector-to-integer bit-vector-xor ( implemented-bit-vector arg-1 , implemented-bit-vector arg-2 ) ) , “ lnot ” ↦ op-1 ( bit-vector-to-integer bit-vector-not ( implemented-bit-vector arg ) ) , “ (lsl) ” ↦ op-2 ( bit-vector-to-integer bit-vector-shift-left ( implemented-bit-vector arg-1 , arg-2 ) ) , “ (lsr) ” ↦ op-2 ( bit-vector-to-integer bit-vector-logical-shift-right ( implemented-bit-vector arg-1 , arg-2 ) ) , “ (asr) ” ↦ op-2 ( bit-vector-to-integer bit-vector-arithmetic-shift-right ( implemented-bit-vector arg-1 , arg-2 ) ) , “ (~-.) ” ↦ op-1 ( float-negate ( implemented-floats-format , arg ) ) , “ (~+.) ” ↦ op-1 ( arg ) , “ (+.) ” ↦ op-2 ( float-add ( implemented-floats-format , arg-1 , arg-2 ) ) , “ (-.) ” ↦ op-2 ( float-subtract ( implemented-floats-format , arg-1 , arg-2 ) ) , “ (*.) ” ↦ op-2 ( float-multiply ( implemented-floats-format , arg-1 , arg-2 ) ) , “ (/.) ” ↦ op-2 ( float-divide ( implemented-floats-format , arg-1 , arg-2 ) ) , “ (**) ” ↦ op-2 ( float-float-power ( implemented-floats-format , arg-1 , arg-2 ) ) , “ sqrt ” ↦ op-1 ( float-sqrt ( implemented-floats-format , arg ) ) , “ exp ” ↦ op-1 ( float-exp ( implemented-floats-format , arg ) ) , “ log ” ↦ op-1 ( float-log ( implemented-floats-format , arg ) ) , “ log10 ” ↦ op-1 ( float-log10 ( implemented-floats-format , arg ) ) , “ cos ” ↦ op-1 ( float-cos ( implemented-floats-format , arg ) ) , “ sin ” ↦ op-1 ( float-sin ( implemented-floats-format , arg ) ) , “ tan ” ↦ op-1 ( float-tan ( implemented-floats-format , arg ) ) , “ acos ” ↦ op-1 ( float-acos ( implemented-floats-format , arg ) ) , “ asin ” ↦ op-1 ( float-asin ( implemented-floats-format , arg ) ) , “ atan ” ↦ op-1 ( float-atan ( implemented-floats-format , arg ) ) , “ atan2 ” ↦ op-2 ( float-atan2 ( implemented-floats-format , arg-1 , arg-2 ) ) , “ cosh ” ↦ op-1 ( float-cosh ( implemented-floats-format , arg ) ) , “ sinh ” ↦ op-1 ( float-sinh ( implemented-floats-format , arg ) ) , “ tanh ” ↦ op-1 ( float-tanh ( implemented-floats-format , arg ) ) , “ ceil ” ↦ op-1 ( implemented-integer float-ceiling ( implemented-floats-format , arg ) ) , “ floor ” ↦ op-1 ( implemented-integer float-floor ( implemented-floats-format , arg ) ) , “ abs_float ” ↦ op-1 ( float-absolute-value ( implemented-floats-format , arg ) ) , “ mod_float ” ↦ op-2 ( float-remainder ( implemented-floats-format , arg-1 , arg-2 ) ) , “ int_of_float ” ↦ op-1 ( implemented-integer float-truncate ( implemented-floats-format , arg ) ) , “ float_of_int ” ↦ op-1 ( implemented-float-literal ( string-append ( to-string ( arg ) , “ .0 ” ) ) ) , “ (^) ” ↦ op-2 ( string-append ( arg-1 , arg-2 ) ) , “ string_of_int ” ↦ op-1 ( to-string ( arg ) ) , “ int_of_string ” ↦ op-1 ( implemented-integer implemented-integer-literal ( arg ) ) , “ string_of_float ” ↦ op-1 ( to-string ( arg ) ) , “ float_of_string ” ↦ op-1 ( implemented-float-literal ( arg ) ) , “ (@) ” ↦ op-2 ( list-append ( arg-1 , arg-2 ) ) , “ print_char ” ↦ op-1 ( print ( to-string ( arg ) ) ) , “ print_string ” ↦ op-1 ( print ( arg ) ) , “ print_int ” ↦ op-1 ( print ( to-string ( arg ) ) ) , “ print_float ” ↦ op-1 ( print ( to-string ( arg ) ) ) , “ print_newline ” ↦ op-1 ( print “ \n ” ) , “ read_line ” ↦ op-1 ( read ) , “ read_int ” ↦ op-1 ( implemented-integer-literal ( read ) ) , “ read_float ” ↦ op-1 ( implemented-float-literal ( read ) ) , “ ref ” ↦ op-1 ( allocate-initialised-variable ( implemented-values , arg ) ) , “ (!) ” ↦ op-1 ( assigned ( arg ) ) , “ (:=) ” ↦ op-2 ( assign ( arg-1 , arg-2 ) ) , “ length ” ↦ op-1 ( implemented-integer list-length ( arg ) ) , “ cons ” ↦ op-2 ( cons ( arg-1 , arg-2 ) ) , “ hd ” ↦ op-1 ( else ( head ( arg ) , throw ( variant ( “ Failure ” , “ hd ” ) ) ) ) , “ tl ” ↦ op-1 ( else ( tail ( arg ) , throw ( variant ( “ Failure ” , “ tl ” ) ) ) ) , “ rev ” ↦ op-1 ( list ( reverse ( list-elements ( arg ) ) ) ) , “ array_length ” ↦ op-1 ( implemented-integer length ( vector-elements ( arg ) ) ) , “ array_make ” ↦ op-2 ( if-true-else ( is-greater-or-equal ( arg-1 , 0 ) , vector ( interleave-map ( allocate-initialised-variable ( values , arg ) , n-of ( arg-1 , arg-2 ) ) ) , throw ( variant ( “ Invalid_argument ” , “ array_make ” ) ) ) ) , “ array_append ” ↦ op-2 ( vector ( vector-elements ( arg-1 ) , vector-elements ( arg-2 ) ) ) , “ array_get ” ↦ op-2 ( else ( assigned ( checked index ( nat-succ arg-2 , vector-elements ( arg-1 ) ) ) , throw ( variant ( “ Invalid_argument ” , “ array_get ” ) ) ) ) , “ array_set ” ↦ op-3 ( else ( assign ( checked index ( nat-succ arg-2 , vector-elements ( arg-1 ) ) , arg-3 ) , throw ( variant ( “ Invalid_argument ” , “ array_set ” ) ) ) ) } \begin{align*}
\KEY{Funcon} \quad
& \NAMEDECL{ocaml-light-core-library}
: \TO \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{environments} \\&\quad
\leadsto \{ \STRING{Match{\UNDERSCORE}failure} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Match{\UNDERSCORE}failure},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{Invalid{\UNDERSCORE}argument} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Invalid{\UNDERSCORE}argument},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{Division{\UNDERSCORE}by{\UNDERSCORE}zero} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Division{\UNDERSCORE}by{\UNDERSCORE}zero},
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ) ), \\&\quad\quad\quad\quad
\STRING{raise} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{=}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{<}{>}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{not}
( \NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ) ), \\&\quad\quad\quad\quad
\STRING{{(}{<}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{is-less}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{>}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{is-greater}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{<}{=}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{is-less-or-equal}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{>}{=}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{is-greater-or-equal}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{min} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{is-less}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ),
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{max} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{is-greater}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ),
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{=}{=}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else}
( \\&\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{and}
( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-in-type}
( \NAMEREF{arg-1},
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{ground-values} ),
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-in-type}
( \NAMEREF{arg-2},
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{ground-values} ) ), \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ), \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Invalid{\UNDERSCORE}argument},
\STRING{equal{:}~functional~value} ) ) ) ), \\&\quad\quad\quad\quad
\STRING{{(}{!}{=}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else}
( \\&\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{and}
( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-in-type}
( \NAMEREF{arg-1},
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{ground-values} ),
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-in-type}
( \NAMEREF{arg-2},
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{ground-values} ) ), \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{not} \
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ), \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Invalid{\UNDERSCORE}argument},
\STRING{equal{:}~functional~value} ) ) ) ), \\&\quad\quad\quad\quad
\STRING{not} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{not}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{\TILDE}{-}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-negate}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{\TILDE}{+}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEREF{arg} ), \\&\quad\quad\quad\quad
\STRING{succ} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-add}
( \NAMEREF{arg},
1 ) ), \\&\quad\quad\quad\quad
\STRING{pred} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-subtract}
( \NAMEREF{arg},
1 ) ), \\&\quad\quad\quad\quad
\STRING{{(}{+}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-add}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{-}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-subtract}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{*}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-multiply}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{/}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else}
( \\&\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \NAMEREF{arg-2},
0 ), \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Division{\UNDERSCORE}by{\UNDERSCORE}zero},
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ) ) ), \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-divide}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ) ), \\&\quad\quad\quad\quad
\STRING{{(}mod{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-modulo}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{abs} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integer-absolute-value}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{max{\UNDERSCORE}int} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{signed-bit-vector-maximum}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integers-width} ) ), \\&\quad\quad\quad\quad
\STRING{min{\UNDERSCORE}int} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{signed-bit-vector-minimum}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integers-width} ) ), \\&\quad\quad\quad\quad
\STRING{{(}land{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-to-integer} \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-and}
( \\&\quad\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../.}{OC-L-02-Values}{implemented-bit-vector} \
\NAMEREF{arg-1}, \\&\quad\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../.}{OC-L-02-Values}{implemented-bit-vector} \
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}lor{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-to-integer} \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-or}
( \\&\quad\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../.}{OC-L-02-Values}{implemented-bit-vector} \
\NAMEREF{arg-1}, \\&\quad\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../.}{OC-L-02-Values}{implemented-bit-vector} \
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}lxor{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-to-integer} \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-xor}
( \\&\quad\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../.}{OC-L-02-Values}{implemented-bit-vector} \
\NAMEREF{arg-1}, \\&\quad\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../.}{OC-L-02-Values}{implemented-bit-vector} \
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{lnot} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-to-integer} \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-not}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-bit-vector} \
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{{(}lsl{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-to-integer} \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-shift-left}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-bit-vector} \
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}lsr{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-to-integer} \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-logical-shift-right}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-bit-vector} \
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}asr{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-to-integer} \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Bits}{bit-vector-arithmetic-shift-right}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-bit-vector} \
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{\TILDE}{-}{.}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-negate}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{\TILDE}{+}{.}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEREF{arg} ), \\&\quad\quad\quad\quad
\STRING{{(}{+}{.}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-add}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{-}{.}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-subtract}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{*}{.}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-multiply}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{/}{.}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-divide}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{*}{*}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-float-power}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{sqrt} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-sqrt}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{exp} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-exp}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{log} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-log}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{log10} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-log10}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{cos} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-cos}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{sin} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-sin}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{tan} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-tan}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{acos} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-acos}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{asin} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-asin}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{atan} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-atan}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{atan2} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-atan2}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{cosh} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-cosh}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{sinh} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-sinh}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{tanh} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-tanh}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{ceil} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-ceiling}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{floor} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-floor}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{abs{\UNDERSCORE}float} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-absolute-value}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{mod{\UNDERSCORE}float} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-remainder}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{int{\UNDERSCORE}of{\UNDERSCORE}float} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Floats}{float-truncate}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats-format},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{float{\UNDERSCORE}of{\UNDERSCORE}int} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-float-literal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{to-string}
( \NAMEREF{arg} ),
\STRING{{.}0} ) ) ), \\&\quad\quad\quad\quad
\STRING{{(}{\CARET}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{string{\UNDERSCORE}of{\UNDERSCORE}int} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{to-string}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{int{\UNDERSCORE}of{\UNDERSCORE}string} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer-literal}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{string{\UNDERSCORE}of{\UNDERSCORE}float} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{to-string}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{float{\UNDERSCORE}of{\UNDERSCORE}string} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-float-literal}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{@}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{list-append}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{print{\UNDERSCORE}char} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Interacting}{print}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{to-string}
( \NAMEREF{arg} ) ) ), \\&\quad\quad\quad\quad
\STRING{print{\UNDERSCORE}string} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Interacting}{print}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{print{\UNDERSCORE}int} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Interacting}{print}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{to-string}
( \NAMEREF{arg} ) ) ), \\&\quad\quad\quad\quad
\STRING{print{\UNDERSCORE}float} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Interacting}{print}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{to-string}
( \NAMEREF{arg} ) ) ), \\&\quad\quad\quad\quad
\STRING{print{\UNDERSCORE}newline} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Interacting}{print} \
\STRING{{\BACKSLASH}n} ), \\&\quad\quad\quad\quad
\STRING{read{\UNDERSCORE}line} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Interacting}{read} ), \\&\quad\quad\quad\quad
\STRING{read{\UNDERSCORE}int} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer-literal}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Interacting}{read} ) ), \\&\quad\quad\quad\quad
\STRING{read{\UNDERSCORE}float} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-float-literal}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Interacting}{read} ) ), \\&\quad\quad\quad\quad
\STRING{ref} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{allocate-initialised-variable}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-values},
\NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{!}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{{(}{:}{=}{)}} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assign}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{length} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{list-length}
( \NAMEREF{arg} ) ), \\&\quad\quad\quad\quad
\STRING{cons} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{cons}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\STRING{hd} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{head}
( \NAMEREF{arg} ),
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Failure},
\STRING{hd} ) ) ) ), \\&\quad\quad\quad\quad
\STRING{tl} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{tail}
( \NAMEREF{arg} ),
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Failure},
\STRING{tl} ) ) ) ), \\&\quad\quad\quad\quad
\STRING{rev} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{list}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{reverse}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{list-elements}
( \NAMEREF{arg} ) ) ) ), \\&\quad\quad\quad\quad
\STRING{array{\UNDERSCORE}length} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-1}
( \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integer} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{length}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector-elements}
( \NAMEREF{arg} ) ) ), \\&\quad\quad\quad\quad
\STRING{array{\UNDERSCORE}make} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else}
( \\&\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{is-greater-or-equal}
( \NAMEREF{arg-1},
0 ), \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector}
( \\&\quad\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{interleave-map}
( \\&\quad\quad\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{allocate-initialised-variable}
( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values},
\NAMEREF{arg} ), \\&\quad\quad\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{n-of}
( \NAMEREF{arg-1},
\NAMEREF{arg-2} ) ) ), \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Invalid{\UNDERSCORE}argument},
\STRING{array{\UNDERSCORE}make} ) ) ) ), \\&\quad\quad\quad\quad
\STRING{array{\UNDERSCORE}append} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector-elements}
( \NAMEREF{arg-1} ),
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector-elements}
( \NAMEREF{arg-2} ) ) ), \\&\quad\quad\quad\quad
\STRING{array{\UNDERSCORE}get} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-2}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else}
( \\&\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{index}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{nat-succ} \
\NAMEREF{arg-2},
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector-elements}
( \NAMEREF{arg-1} ) ) ), \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Invalid{\UNDERSCORE}argument},
\STRING{array{\UNDERSCORE}get} ) ) ) ), \\&\quad\quad\quad\quad
\STRING{array{\UNDERSCORE}set} \mapsto \\&\quad\quad\quad\quad\quad
\NAMEREF{op-3}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else}
( \\&\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assign}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{index}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{nat-succ} \
\NAMEREF{arg-2},
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector-elements}
( \NAMEREF{arg-1} ) ),
\NAMEREF{arg-3} ), \\&\quad\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Invalid{\UNDERSCORE}argument},
\STRING{array{\UNDERSCORE}set} ) ) ) ) \}
\end{align*} Funcon ocaml-light-core-library : ⇒ environments ⇝ { “ Match _ failure ” ↦ op-1 ( variant ( “ Match _ failure ” , arg )) , “ Invalid _ argument ” ↦ op-1 ( variant ( “ Invalid _ argument ” , arg )) , “ Division _ by _ zero ” ↦ variant ( “ Division _ by _ zero ” , tuple ( )) , “ raise ” ↦ op-1 ( throw ( arg )) , “ ( = ) ” ↦ op-2 ( ocaml-light-is-structurally-equal ( arg-1 , arg-2 )) , “ ( < > ) ” ↦ op-2 ( not ( ocaml-light-is-structurally-equal ( arg-1 , arg-2 ))) , “ ( < ) ” ↦ op-2 ( is-less ( arg-1 , arg-2 )) , “ ( > ) ” ↦ op-2 ( is-greater ( arg-1 , arg-2 )) , “ ( < = ) ” ↦ op-2 ( is-less-or-equal ( arg-1 , arg-2 )) , “ ( > = ) ” ↦ op-2 ( is-greater-or-equal ( arg-1 , arg-2 )) , “ min ” ↦ op-2 ( if-true-else ( is-less ( arg-1 , arg-2 ) , arg-1 , arg-2 )) , “ max ” ↦ op-2 ( if-true-else ( is-greater ( arg-1 , arg-2 ) , arg-1 , arg-2 )) , “ ( = = ) ” ↦ op-2 ( if-true-else ( and ( is-in-type ( arg-1 , ground-values ) , is-in-type ( arg-2 , ground-values )) , is-equal ( arg-1 , arg-2 ) , throw ( variant ( “ Invalid _ argument ” , “ equal : functional value ” )))) , “ ( ! = ) ” ↦ op-2 ( if-true-else ( and ( is-in-type ( arg-1 , ground-values ) , is-in-type ( arg-2 , ground-values )) , not is-equal ( arg-1 , arg-2 ) , throw ( variant ( “ Invalid _ argument ” , “ equal : functional value ” )))) , “ not ” ↦ op-1 ( not ( arg )) , “ ( ~ - ) ” ↦ op-1 ( implemented-integer integer-negate ( arg )) , “ ( ~ + ) ” ↦ op-1 ( implemented-integer arg ) , “ succ ” ↦ op-1 ( implemented-integer integer-add ( arg , 1 )) , “ pred ” ↦ op-1 ( implemented-integer integer-subtract ( arg , 1 )) , “ ( + ) ” ↦ op-2 ( implemented-integer integer-add ( arg-1 , arg-2 )) , “ ( - ) ” ↦ op-2 ( implemented-integer integer-subtract ( arg-1 , arg-2 )) , “ ( * ) ” ↦ op-2 ( implemented-integer integer-multiply ( arg-1 , arg-2 )) , “ ( / ) ” ↦ op-2 ( implemented-integer if-true-else ( is-equal ( arg-2 , 0 ) , throw ( variant ( “ Division _ by _ zero ” , tuple ( ))) , checked integer-divide ( arg-1 , arg-2 ))) , “ ( mod ) ” ↦ op-2 ( implemented-integer checked integer-modulo ( arg-1 , arg-2 )) , “ abs ” ↦ op-1 ( implemented-integer integer-absolute-value ( arg )) , “ max _ int ” ↦ op-1 ( signed-bit-vector-maximum ( implemented-integers-width )) , “ min _ int ” ↦ op-1 ( signed-bit-vector-minimum ( implemented-integers-width )) , “ ( land ) ” ↦ op-2 ( bit-vector-to-integer bit-vector-and ( implemented-bit-vector arg-1 , implemented-bit-vector arg-2 )) , “ ( lor ) ” ↦ op-2 ( bit-vector-to-integer bit-vector-or ( implemented-bit-vector arg-1 , implemented-bit-vector arg-2 )) , “ ( lxor ) ” ↦ op-2 ( bit-vector-to-integer bit-vector-xor ( implemented-bit-vector arg-1 , implemented-bit-vector arg-2 )) , “ lnot ” ↦ op-1 ( bit-vector-to-integer bit-vector-not ( implemented-bit-vector arg )) , “ ( lsl ) ” ↦ op-2 ( bit-vector-to-integer bit-vector-shift-left ( implemented-bit-vector arg-1 , arg-2 )) , “ ( lsr ) ” ↦ op-2 ( bit-vector-to-integer bit-vector-logical-shift-right ( implemented-bit-vector arg-1 , arg-2 )) , “ ( asr ) ” ↦ op-2 ( bit-vector-to-integer bit-vector-arithmetic-shift-right ( implemented-bit-vector arg-1 , arg-2 )) , “ ( ~ - . ) ” ↦ op-1 ( float-negate ( implemented-floats-format , arg )) , “ ( ~ + . ) ” ↦ op-1 ( arg ) , “ ( + . ) ” ↦ op-2 ( float-add ( implemented-floats-format , arg-1 , arg-2 )) , “ ( - . ) ” ↦ op-2 ( float-subtract ( implemented-floats-format , arg-1 , arg-2 )) , “ ( * . ) ” ↦ op-2 ( float-multiply ( implemented-floats-format , arg-1 , arg-2 )) , “ ( / . ) ” ↦ op-2 ( float-divide ( implemented-floats-format , arg-1 , arg-2 )) , “ ( * * ) ” ↦ op-2 ( float-float-power ( implemented-floats-format , arg-1 , arg-2 )) , “ sqrt ” ↦ op-1 ( float-sqrt ( implemented-floats-format , arg )) , “ exp ” ↦ op-1 ( float-exp ( implemented-floats-format , arg )) , “ log ” ↦ op-1 ( float-log ( implemented-floats-format , arg )) , “ log10 ” ↦ op-1 ( float-log10 ( implemented-floats-format , arg )) , “ cos ” ↦ op-1 ( float-cos ( implemented-floats-format , arg )) , “ sin ” ↦ op-1 ( float-sin ( implemented-floats-format , arg )) , “ tan ” ↦ op-1 ( float-tan ( implemented-floats-format , arg )) , “ acos ” ↦ op-1 ( float-acos ( implemented-floats-format , arg )) , “ asin ” ↦ op-1 ( float-asin ( implemented-floats-format , arg )) , “ atan ” ↦ op-1 ( float-atan ( implemented-floats-format , arg )) , “ atan2 ” ↦ op-2 ( float-atan2 ( implemented-floats-format , arg-1 , arg-2 )) , “ cosh ” ↦ op-1 ( float-cosh ( implemented-floats-format , arg )) , “ sinh ” ↦ op-1 ( float-sinh ( implemented-floats-format , arg )) , “ tanh ” ↦ op-1 ( float-tanh ( implemented-floats-format , arg )) , “ ceil ” ↦ op-1 ( implemented-integer float-ceiling ( implemented-floats-format , arg )) , “ floor ” ↦ op-1 ( implemented-integer float-floor ( implemented-floats-format , arg )) , “ abs _ float ” ↦ op-1 ( float-absolute-value ( implemented-floats-format , arg )) , “ mod _ float ” ↦ op-2 ( float-remainder ( implemented-floats-format , arg-1 , arg-2 )) , “ int _ of _ float ” ↦ op-1 ( implemented-integer float-truncate ( implemented-floats-format , arg )) , “ float _ of _ int ” ↦ op-1 ( implemented-float-literal ( string-append ( to-string ( arg ) , “ . 0 ” ))) , “ ( ^ ) ” ↦ op-2 ( string-append ( arg-1 , arg-2 )) , “ string _ of _ int ” ↦ op-1 ( to-string ( arg )) , “ int _ of _ string ” ↦ op-1 ( implemented-integer implemented-integer-literal ( arg )) , “ string _ of _ float ” ↦ op-1 ( to-string ( arg )) , “ float _ of _ string ” ↦ op-1 ( implemented-float-literal ( arg )) , “ ( @ ) ” ↦ op-2 ( list-append ( arg-1 , arg-2 )) , “ print _ char ” ↦ op-1 ( print ( to-string ( arg ))) , “ print _ string ” ↦ op-1 ( print ( arg )) , “ print _ int ” ↦ op-1 ( print ( to-string ( arg ))) , “ print _ float ” ↦ op-1 ( print ( to-string ( arg ))) , “ print _ newline ” ↦ op-1 ( print “ \ n ” ) , “ read _ line ” ↦ op-1 ( read ) , “ read _ int ” ↦ op-1 ( implemented-integer-literal ( read )) , “ read _ float ” ↦ op-1 ( implemented-float-literal ( read )) , “ ref ” ↦ op-1 ( allocate-initialised-variable ( implemented-values , arg )) , “ ( ! ) ” ↦ op-1 ( assigned ( arg )) , “ ( : = ) ” ↦ op-2 ( assign ( arg-1 , arg-2 )) , “ length ” ↦ op-1 ( implemented-integer list-length ( arg )) , “ cons ” ↦ op-2 ( cons ( arg-1 , arg-2 )) , “ hd ” ↦ op-1 ( else ( head ( arg ) , throw ( variant ( “ Failure ” , “ hd ” )))) , “ tl ” ↦ op-1 ( else ( tail ( arg ) , throw ( variant ( “ Failure ” , “ tl ” )))) , “ rev ” ↦ op-1 ( list ( reverse ( list-elements ( arg )))) , “ array _ length ” ↦ op-1 ( implemented-integer length ( vector-elements ( arg ))) , “ array _ make ” ↦ op-2 ( if-true-else ( is-greater-or-equal ( arg-1 , 0 ) , vector ( interleave-map ( allocate-initialised-variable ( values , arg ) , n-of ( arg-1 , arg-2 ))) , throw ( variant ( “ Invalid _ argument ” , “ array _ make ” )))) , “ array _ append ” ↦ op-2 ( vector ( vector-elements ( arg-1 ) , vector-elements ( arg-2 ))) , “ array _ get ” ↦ op-2 ( else ( assigned ( checked index ( nat-succ arg-2 , vector-elements ( arg-1 ))) , throw ( variant ( “ Invalid _ argument ” , “ array _ get ” )))) , “ array _ set ” ↦ op-3 ( else ( assign ( checked index ( nat-succ arg-2 , vector-elements ( arg-1 )) , arg-3 ) , throw ( variant ( “ Invalid _ argument ” , “ array _ set ” ))))}
Funcon ocaml-light-match-failure : ⇒ variants ( tuples ( strings , integers , integers ) ) ⇝ variant ( “ Match_failure ” , tuple ( “ ” , 0 , 0 ) ) \begin{align*}
\KEY{Funcon} \quad
& \NAMEDECL{ocaml-light-match-failure}
: \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variants}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuples}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{strings},
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integers},
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integers} ) ) \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Match{\UNDERSCORE}failure},
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \STRING{},
0,
0 ) )
\end{align*} Funcon ocaml-light-match-failure : ⇒ variants ( tuples ( strings , integers , integers )) ⇝ variant ( “ Match _ failure ” , tuple ( “ ” , 0 , 0 )) ocaml-light-match-failure \SHADE{\NAMEREF{ocaml-light-match-failure}} ocaml-light-match-failure
Funcon ocaml-light-assert-failure : ⇒ variants ( tuples ( strings , integers , integers ) ) ⇝ variant ( “ Assert_failure ” , tuple ( “ ” , 0 , 0 ) ) \begin{align*}
\KEY{Funcon} \quad
& \NAMEDECL{ocaml-light-assert-failure}
: \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variants}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuples}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{strings},
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integers},
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integers} ) ) \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Assert{\UNDERSCORE}failure},
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \STRING{},
0,
0 ) )
\end{align*} Funcon ocaml-light-assert-failure : ⇒ variants ( tuples ( strings , integers , integers )) ⇝ variant ( “ Assert _ failure ” , tuple ( “ ” , 0 , 0 )) ocaml-light-assert-failure \SHADE{\NAMEREF{ocaml-light-assert-failure}} ocaml-light-assert-failure
Funcon ocaml-light-is-structurally-equal ( _ : implemented-values , _ : implemented-values ) : ⇒ booleans \begin{align*}
\KEY{Funcon} \quad
& \NAMEDECL{ocaml-light-is-structurally-equal}(
\_ : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-values}, \_ : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-values}) \\&\quad
: \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{booleans}
\end{align*} Funcon ocaml-light-is-structurally-equal ( _ : implemented-values , _ : implemented-values ) : ⇒ booleans ocaml-light-is-structurally-equal ( V 1 , V 2 ) \SHADE{\NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{V}\SUB{1},
\VAR{V}\SUB{2} )} ocaml-light-is-structurally-equal ( V 1 , V 2 ) V 1 \SHADE{\VAR{V}\SUB{1}} V 1 V 2 \SHADE{\VAR{V}\SUB{2}} V 2
Unit Type
Rule ocaml-light-is-structurally-equal ( null-value , null-value ) ⇝ true \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-value},
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-value} ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{true}
\end{align*} Rule ocaml-light-is-structurally-equal ( null-value , null-value ) ⇝ true Booleans
Rule ocaml-light-is-structurally-equal ( B 1 : booleans , B 2 : booleans ) ⇝ is-equal ( B 1 , B 2 ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{B}\SUB{1} : \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{booleans},
\VAR{B}\SUB{2} : \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{booleans} ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \VAR{B}\SUB{1},
\VAR{B}\SUB{2} )
\end{align*} Rule ocaml-light-is-structurally-equal ( B 1 : booleans , B 2 : booleans ) ⇝ is-equal ( B 1 , B 2 ) Integers
Rule ocaml-light-is-structurally-equal ( I 1 : implemented-integers , I 2 : implemented-integers ) ⇝ is-equal ( I 1 , I 2 ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{I}\SUB{1} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integers},
\VAR{I}\SUB{2} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-integers} ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \VAR{I}\SUB{1},
\VAR{I}\SUB{2} )
\end{align*} Rule ocaml-light-is-structurally-equal ( I 1 : implemented-integers , I 2 : implemented-integers ) ⇝ is-equal ( I 1 , I 2 ) Floats
Rule ocaml-light-is-structurally-equal ( F 1 : implemented-floats , F 2 : implemented-floats ) ⇝ is-equal ( F 1 , F 2 ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{F}\SUB{1} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats},
\VAR{F}\SUB{2} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats} ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \VAR{F}\SUB{1},
\VAR{F}\SUB{2} )
\end{align*} Rule ocaml-light-is-structurally-equal ( F 1 : implemented-floats , F 2 : implemented-floats ) ⇝ is-equal ( F 1 , F 2 ) Characters
Rule ocaml-light-is-structurally-equal ( C 1 : implemented-characters , C 2 : implemented-characters ) ⇝ is-equal ( C 1 , C 2 ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{C}\SUB{1} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-characters},
\VAR{C}\SUB{2} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-characters} ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \VAR{C}\SUB{1},
\VAR{C}\SUB{2} )
\end{align*} Rule ocaml-light-is-structurally-equal ( C 1 : implemented-characters , C 2 : implemented-characters ) ⇝ is-equal ( C 1 , C 2 ) Strings
Rule ocaml-light-is-structurally-equal ( S 1 : implemented-strings , S 2 : implemented-strings ) ⇝ is-equal ( S 1 , S 2 ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{S}\SUB{1} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-strings},
\VAR{S}\SUB{2} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-strings} ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \VAR{S}\SUB{1},
\VAR{S}\SUB{2} )
\end{align*} Rule ocaml-light-is-structurally-equal ( S 1 : implemented-strings , S 2 : implemented-strings ) ⇝ is-equal ( S 1 , S 2 ) Tuples
Rule ocaml-light-is-structurally-equal ( tuple ( ) , tuple ( ) ) ⇝ true Rule ocaml-light-is-structurally-equal ( tuple ( ) , tuple ( V + ) ) ⇝ false Rule ocaml-light-is-structurally-equal ( tuple ( V + ) , tuple ( ) ) ⇝ false Rule ocaml-light-is-structurally-equal ( tuple ( V , V * ) , tuple ( W , W * ) ) ⇝ and ( ocaml-light-is-structurally-equal ( V , W ) , ocaml-light-is-structurally-equal ( tuple ( V * ) , tuple ( W * ) ) ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ),
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ) ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{true}
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ),
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \VAR{V}\PLUS ) ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{false}
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \VAR{V}\PLUS ),
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ) ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{false}
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \VAR{V},
\VAR{V}\STAR ),
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \VAR{W},
\VAR{W}\STAR ) ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{and}
( \\&\quad\quad \NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{V},
\VAR{W} ), \\&\quad\quad
\NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \VAR{V}\STAR ),
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \VAR{W}\STAR ) ) )
\end{align*} Rule Rule Rule Rule ocaml-light-is-structurally-equal ( tuple ( ) , tuple ( )) ⇝ true ocaml-light-is-structurally-equal ( tuple ( ) , tuple ( V + )) ⇝ false ocaml-light-is-structurally-equal ( tuple ( V + ) , tuple ( )) ⇝ false ocaml-light-is-structurally-equal ( tuple ( V , V * ) , tuple ( W , W * )) ⇝ and ( ocaml-light-is-structurally-equal ( V , W ) , ocaml-light-is-structurally-equal ( tuple ( V * ) , tuple ( W * ))) Lists
Rule ocaml-light-is-structurally-equal ( [ ] , [ ] ) ⇝ true Rule ocaml-light-is-structurally-equal ( [ ] , [ V + ] ) ⇝ false Rule ocaml-light-is-structurally-equal ( [ V + ] , [ ] ) ⇝ false Rule ocaml-light-is-structurally-equal ( [ V , V * ] , [ W , W * ] ) ⇝ and ( ocaml-light-is-structurally-equal ( V , W ) , ocaml-light-is-structurally-equal ( [ V * ] , [ W * ] ) ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( [ \ ],
[ \ ] ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{true}
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( [ \ ],
[ \VAR{V}\PLUS ] ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{false}
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( [ \VAR{V}\PLUS ],
[ \ ] ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{false}
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( [ \VAR{V},
\VAR{V}\STAR ],
[ \VAR{W},
\VAR{W}\STAR ] ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{and}
( \\&\quad\quad \NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{V},
\VAR{W} ), \\&\quad\quad
\NAMEREF{ocaml-light-is-structurally-equal}
( [ \VAR{V}\STAR ],
[ \VAR{W}\STAR ] ) )
\end{align*} Rule Rule Rule Rule ocaml-light-is-structurally-equal ([ ] , [ ]) ⇝ true ocaml-light-is-structurally-equal ([ ] , [ V + ]) ⇝ false ocaml-light-is-structurally-equal ([ V + ] , [ ]) ⇝ false ocaml-light-is-structurally-equal ([ V , V * ] , [ W , W * ]) ⇝ and ( ocaml-light-is-structurally-equal ( V , W ) , ocaml-light-is-structurally-equal ([ V * ] , [ W * ])) Records
Rule dom ( Map 1 ) = = dom ( Map 2 ) ocaml-light-is-structurally-equal ( record ( Map 1 : maps ( _ , _ ) ) , record ( Map 2 : maps ( _ , _ ) ) ) ⇝ not ( is-in-set ( false , set ( interleave-map ( ocaml-light-is-structurally-equal ( checked lookup ( Map 1 , given ) , checked lookup ( Map 2 , given ) ) , set-elements ( dom ( Map 1 ) ) ) ) ) ) \begin{align*}
\KEY{Rule} \quad
& \RULE{
& \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{dom}
( \VAR{Map}\SUB{1} )
== \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{dom}
( \VAR{Map}\SUB{2} )
}{
& \NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Records}{record}
( \VAR{Map}\SUB{1} : \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{maps}
( \_,
\_ ) ),
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Records}{record}
( \VAR{Map}\SUB{2} : \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{maps}
( \_,
\_ ) ) ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{not}
( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sets}{is-in-set}
( \\&\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{false}, \\&\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sets}{set}
( \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{interleave-map}
( \\&\quad\quad\quad\quad\quad \NAMEREF{ocaml-light-is-structurally-equal}
( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{lookup}
( \VAR{Map}\SUB{1},
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ), \\&\quad\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{lookup}
( \VAR{Map}\SUB{2},
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ) ), \\&\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sets}{set-elements}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{dom}
( \VAR{Map}\SUB{1} ) ) ) ) ) )
}
\end{align*} Rule ocaml-light-is-structurally-equal ( record ( Map 1 : maps ( _ , _ )) , record ( Map 2 : maps ( _ , _ ))) ⇝ not ( is-in-set ( false , set ( interleave-map ( ocaml-light-is-structurally-equal ( checked lookup ( Map 1 , given ) , checked lookup ( Map 2 , given )) , set-elements ( dom ( Map 1 )))))) dom ( Map 1 ) == dom ( Map 2 ) References
Rule ocaml-light-is-structurally-equal ( V 1 : variables , V 2 : variables ) ⇝ ocaml-light-is-structurally-equal ( assigned ( V 1 ) , assigned ( V 2 ) ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{V}\SUB{1} : \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{variables},
\VAR{V}\SUB{2} : \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{variables} ) \leadsto \\&\quad
\NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned}
( \VAR{V}\SUB{1} ),
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned}
( \VAR{V}\SUB{2} ) )
\end{align*} Rule ocaml-light-is-structurally-equal ( V 1 : variables , V 2 : variables ) ⇝ ocaml-light-is-structurally-equal ( assigned ( V 1 ) , assigned ( V 2 )) Vectors
Rule ocaml-light-is-structurally-equal ( Vec 1 : vectors ( values ) , Vec 2 : vectors ( values ) ) ⇝ ocaml-light-is-structurally-equal ( [ vector-elements ( Vec 1 ) ] , [ vector-elements ( Vec 2 ) ] ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{Vec}\SUB{1} : \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vectors}
( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values} ),
\VAR{Vec}\SUB{2} : \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vectors}
( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values} ) ) \leadsto \\&\quad
\NAMEREF{ocaml-light-is-structurally-equal}
( [ \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector-elements}
( \VAR{Vec}\SUB{1} ) ],
[ \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector-elements}
( \VAR{Vec}\SUB{2} ) ] )
\end{align*} Rule ocaml-light-is-structurally-equal ( Vec 1 : vectors ( values ) , Vec 2 : vectors ( values )) ⇝ ocaml-light-is-structurally-equal ([ vector-elements ( Vec 1 )] , [ vector-elements ( Vec 2 )]) Variants
Rule ocaml-light-is-structurally-equal ( variant ( Con 1 , V 1 ) , variant ( Con 2 , V 2 ) ) ⇝ if-true-else ( is-equal ( Con 1 , Con 2 ) , if-true-else ( or ( is-equal ( tuple ( ) , V 1 ) , is-equal ( tuple ( ) , V 2 ) ) , and ( is-equal ( tuple ( ) , V 1 ) , is-equal ( tuple ( ) , V 2 ) ) , ocaml-light-is-structurally-equal ( V 1 , V 2 ) ) , false ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \VAR{Con}\SUB{1},
\VAR{V}\SUB{1} ),
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \VAR{Con}\SUB{2},
\VAR{V}\SUB{2} ) ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else}
( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \VAR{Con}\SUB{1},
\VAR{Con}\SUB{2} ), \\&\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else}
( \\&\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{or}
( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ),
\VAR{V}\SUB{1} ),
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ),
\VAR{V}\SUB{2} ) ), \\&\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{and}
( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ),
\VAR{V}\SUB{1} ),
\NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ),
\VAR{V}\SUB{2} ) ), \\&\quad\quad\quad
\NAMEREF{ocaml-light-is-structurally-equal}
( \VAR{V}\SUB{1},
\VAR{V}\SUB{2} ) ), \\&\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{false} )
\end{align*} Rule ocaml-light-is-structurally-equal ( variant ( Con 1 , V 1 ) , variant ( Con 2 , V 2 )) ⇝ if-true-else ( is-equal ( Con 1 , Con 2 ) , if-true-else ( or ( is-equal ( tuple ( ) , V 1 ) , is-equal ( tuple ( ) , V 2 )) , and ( is-equal ( tuple ( ) , V 1 ) , is-equal ( tuple ( ) , V 2 )) , ocaml-light-is-structurally-equal ( V 1 , V 2 )) , false ) Functions
Rule ocaml-light-is-structurally-equal ( _ : functions ( _ , _ ) , _ : functions ( _ , _ ) ) ⇝ throw ( variant ( “ Invalid_argument ” , “ equal: functional value ” ) ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-is-structurally-equal}
( \_ : \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \_,
\_ ),
\_ : \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \_,
\_ ) ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Throwing}{throw}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \STRING{Invalid{\UNDERSCORE}argument},
\STRING{equal{:}~functional~value} ) )
\end{align*} Rule ocaml-light-is-structurally-equal ( _ : functions ( _ , _ ) , _ : functions ( _ , _ )) ⇝ throw ( variant ( “ Invalid _ argument ” , “ equal : functional value ” ))
Funcon ocaml-light-to-string ( _ : values ) : ⇒ strings \begin{align*}
\KEY{Funcon} \quad
& \NAMEDECL{ocaml-light-to-string}(
\_ : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values})
: \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{strings}
\end{align*} Funcon ocaml-light-to-string ( _ : values ) : ⇒ strings ocaml-light-to-string ( V ) \SHADE{\NAMEREF{ocaml-light-to-string}
( \VAR{V} )} ocaml-light-to-string ( V )
Rule ocaml-light-to-string ( null-value ) ⇝ “ () ” Rule ocaml-light-to-string ( B : booleans ) ⇝ to-string ( B ) Rule ocaml-light-to-string ( I : integers ) ⇝ to-string ( I ) Rule ocaml-light-to-string ( F : implemented-floats ) ⇝ to-string ( F ) Rule ocaml-light-to-string ( C : implemented-characters ) ⇝ string-append ( “ ’ ” , to-string ( C ) , “ ’ ” ) Rule S ≠ [ ] ocaml-light-to-string ( S : implemented-strings ) ⇝ string-append ( “ " ” , S , “ " ” ) Rule ocaml-light-to-string ( _ : functions ( _ , _ ) ) ⇝ “ <fun> ” Rule ocaml-light-to-string ( V : variables ) ⇝ string-append ( “ ref ” , ocaml-light-to-string ( assigned ( V ) ) ) Rule ocaml-light-to-string ( variant ( Con , Arg ) ) ⇝ if-true-else ( is-equal ( tuple ( ) , Arg ) , Con , string-append ( Con , “ ” , ocaml-light-to-string ( Arg ) ) ) Rule ocaml-light-to-string ( tuple ( V : values , V + : values + ) ) ⇝ string-append ( “ ( ” , intersperse ( “ , ” , interleave-map ( ocaml-light-to-string ( given ) , V , V + ) ) , “ ) ” ) Rule ocaml-light-to-string ( [ V * : values * ] ) ⇝ string-append ( “ [ ” , intersperse ( “ ; ” , interleave-map ( ocaml-light-to-string ( given ) , V * ) ) , “ ] ” ) Rule ocaml-light-to-string ( V : implemented-vectors ) ⇝ string-append ( “ [| ” , intersperse ( “ ; ” , interleave-map ( ocaml-light-to-string ( assigned ( given ) ) , vector-elements ( V ) ) ) , “ |] ” ) Rule ocaml-light-to-string ( record ( M : maps ( _ , _ ) ) ) ⇝ string-append ( “ { ” , intersperse ( “ ; ” , interleave-map ( string-append ( arg-1 , “ = ” , ocaml-light-to-string ( arg-2 ) ) , map-elements ( M ) ) ) , “ } ” ) \begin{align*}
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-value} ) \leadsto
\STRING{{(}{)}}
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \VAR{B} : \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{booleans} ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{to-string}
( \VAR{B} )
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \VAR{I} : \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integers} ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{to-string}
( \VAR{I} )
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \VAR{F} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-floats} ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{to-string}
( \VAR{F} )
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \VAR{C} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-characters} ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \STRING{{\APOSTROPHE}},
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{to-string}
( \VAR{C} ),
\STRING{{\APOSTROPHE}} )
\\
\KEY{Rule} \quad
& \RULE{
& \VAR{S}
\neq [ \ ]
}{
& \NAMEREF{ocaml-light-to-string}
( \VAR{S} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-strings} ) \leadsto
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \STRING{{"}},
\VAR{S},
\STRING{{"}} )
}
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \_ : \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions}
( \_,
\_ ) ) \leadsto
\STRING{{<}fun{>}}
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \VAR{V} : \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{variables} ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \STRING{ref~},
\NAMEREF{ocaml-light-to-string}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned}
( \VAR{V} ) ) )
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Variants}{variant}
( \VAR{Con},
\VAR{Arg} ) ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else}
( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \ ),
\VAR{Arg} ), \\&\quad\quad
\VAR{Con}, \\&\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \VAR{Con},
\STRING{~},
\NAMEREF{ocaml-light-to-string}
( \VAR{Arg} ) ) )
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple}
( \VAR{V} : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values},
\VAR{V}\PLUS : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values}\PLUS ) ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \\&\quad\quad \STRING{{(}}, \\&\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{intersperse}
( \STRING{{,}~},
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{interleave-map}
( \NAMEREF{ocaml-light-to-string}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ),
\VAR{V},
\VAR{V}\PLUS ) ), \\&\quad\quad
\STRING{{)}} )
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( [ \VAR{V}\STAR : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values}\STAR ] ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \\&\quad\quad \STRING{{[}}, \\&\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{intersperse}
( \STRING{{;}~},
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{interleave-map}
( \NAMEREF{ocaml-light-to-string}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ),
\VAR{V}\STAR ) ), \\&\quad\quad
\STRING{{]}} )
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \VAR{V} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-vectors} ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \\&\quad\quad \STRING{{[}{|}}, \\&\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{intersperse}
( \\&\quad\quad\quad \STRING{{;}~}, \\&\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{interleave-map}
( \\&\quad\quad\quad\quad \NAMEREF{ocaml-light-to-string}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned}
( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ) ), \\&\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Vectors}{vector-elements}
( \VAR{V} ) ) ), \\&\quad\quad
\STRING{{|}{]}} )
\\
\KEY{Rule} \quad
& \NAMEREF{ocaml-light-to-string}
( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Records}{record}
( \VAR{M} : \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{maps}
( \_,
\_ ) ) ) \leadsto \\&\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \\&\quad\quad \STRING{{\LEFTBRACE}}, \\&\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Sequences}{intersperse}
( \\&\quad\quad\quad \STRING{{;}~}, \\&\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{interleave-map}
( \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Strings}{string-append}
( \NAMEREF{arg-1},
\STRING{~{=}~},
\NAMEREF{ocaml-light-to-string}
( \NAMEREF{arg-2} ) ), \\&\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{map-elements}
( \VAR{M} ) ) ), \\&\quad\quad
\STRING{{\RIGHTBRACE}} )
\end{align*} Rule Rule Rule Rule Rule Rule Rule Rule Rule Rule Rule Rule Rule ocaml-light-to-string ( null-value ) ⇝ “ ( ) ” ocaml-light-to-string ( B : booleans ) ⇝ to-string ( B ) ocaml-light-to-string ( I : integers ) ⇝ to-string ( I ) ocaml-light-to-string ( F : implemented-floats ) ⇝ to-string ( F ) ocaml-light-to-string ( C : implemented-characters ) ⇝ string-append ( “ ’ ” , to-string ( C ) , “ ’ ” ) ocaml-light-to-string ( S : implemented-strings ) ⇝ string-append ( “ " ” , S , “ " ” ) S = [ ] ocaml-light-to-string ( _ : functions ( _ , _ )) ⇝ “ < fun > ” ocaml-light-to-string ( V : variables ) ⇝ string-append ( “ ref ” , ocaml-light-to-string ( assigned ( V ))) ocaml-light-to-string ( variant ( Con , Arg )) ⇝ if-true-else ( is-equal ( tuple ( ) , Arg ) , Con , string-append ( Con , “ ” , ocaml-light-to-string ( Arg ))) ocaml-light-to-string ( tuple ( V : values , V + : values + )) ⇝ string-append ( “ ( ” , intersperse ( “ , ” , interleave-map ( ocaml-light-to-string ( given ) , V , V + )) , “ ) ” ) ocaml-light-to-string ([ V * : values * ]) ⇝ string-append ( “ [ ” , intersperse ( “ ; ” , interleave-map ( ocaml-light-to-string ( given ) , V * )) , “ ] ” ) ocaml-light-to-string ( V : implemented-vectors ) ⇝ string-append ( “ [ | ” , intersperse ( “ ; ” , interleave-map ( ocaml-light-to-string ( assigned ( given )) , vector-elements ( V ))) , “ | ] ” ) ocaml-light-to-string ( record ( M : maps ( _ , _ ))) ⇝ string-append ( “ { ” , intersperse ( “ ; ” , interleave-map ( string-append ( arg-1 , “ = ” , ocaml-light-to-string ( arg-2 )) , map-elements ( M ))) , “ } ” ) Funcon ocaml-light-define-and-display ( Env : envs ) : ⇒ envs ⇝ sequential ( effect left-to-right-map ( print ( arg-1 , “ = ” , ocaml-light-to-string arg-2 , “ \n ” ) , map-elements Env ) , Env ) \begin{align*}
\KEY{Funcon} \quad
& \NAMEDECL{ocaml-light-define-and-display}(
\VAR{Env} : \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{envs})
: \TO \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{envs} \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential}
( \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{effect} \
\NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{left-to-right-map}
( \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Interacting}{print}
( \NAMEREF{arg-1},
\STRING{~{=}~},
\NAMEREF{ocaml-light-to-string} \
\NAMEREF{arg-2},
\STRING{{\BACKSLASH}n} ), \\&\quad\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{map-elements} \
\VAR{Env} ), \\&\quad\quad\quad\quad
\VAR{Env} )
\end{align*} Funcon ocaml-light-define-and-display ( Env : envs ) : ⇒ envs ⇝ sequential ( effect left-to-right-map ( print ( arg-1 , “ = ” , ocaml-light-to-string arg-2 , “ \ n ” ) , map-elements Env ) , Env ) Funcon ocaml-light-evaluate-and-display ( V : implemented-values ) : ⇒ envs ⇝ sequential ( print ( “ - = ” , ocaml-light-to-string V , “ \n ” ) , map ( ) ) \begin{align*}
\KEY{Funcon} \quad
& \NAMEDECL{ocaml-light-evaluate-and-display}(
\VAR{V} : \NAMEHYPER{../.}{OC-L-02-Values}{implemented-values})
: \TO \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{envs} \\&\quad
\leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential}
( \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Interacting}{print}
( \STRING{{-}~{=}~},
\NAMEREF{ocaml-light-to-string} \
\VAR{V},
\STRING{{\BACKSLASH}n} ), \\&\quad\quad\quad\quad
\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Maps}{map}
( \ ) )
\end{align*} Funcon ocaml-light-evaluate-and-display ( V : implemented-values ) : ⇒ envs ⇝ sequential ( print ( “ - = ” , ocaml-light-to-string V , “ \ n ” ) , map ( ))
←
↑
→