Stuffs
This commit is contained in:
parent
d236ebf9c7
commit
47c4aef6c6
1
.gitignore
vendored
1
.gitignore
vendored
@ -2,3 +2,4 @@
|
||||
*.log
|
||||
*.out
|
||||
*.pdf
|
||||
_build
|
||||
|
42
.ocamlformat
Normal file
42
.ocamlformat
Normal file
@ -0,0 +1,42 @@
|
||||
version=0.24.1
|
||||
assignment-operator=end-line
|
||||
break-cases=fit
|
||||
break-fun-decl=wrap
|
||||
break-fun-sig=wrap
|
||||
break-infix=wrap
|
||||
break-infix-before-func=false
|
||||
break-separators=before
|
||||
break-sequences=true
|
||||
cases-exp-indent=2
|
||||
cases-matching-exp-indent=normal
|
||||
doc-comments=before
|
||||
doc-comments-padding=2
|
||||
doc-comments-tag-only=default
|
||||
dock-collection-brackets=false
|
||||
exp-grouping=preserve
|
||||
field-space=loose
|
||||
if-then-else=compact
|
||||
indicate-multiline-delimiters=space
|
||||
indicate-nested-or-patterns=unsafe-no
|
||||
infix-precedence=indent
|
||||
leading-nested-match-parens=false
|
||||
let-and=sparse
|
||||
let-binding-spacing=compact
|
||||
let-module=compact
|
||||
margin=80
|
||||
max-indent=68
|
||||
module-item-spacing=sparse
|
||||
ocp-indent-compat=false
|
||||
parens-ite=false
|
||||
parens-tuple=always
|
||||
parse-docstrings=true
|
||||
sequence-blank-line=preserve-one
|
||||
sequence-style=terminator
|
||||
single-case=compact
|
||||
space-around-arrays=true
|
||||
space-around-lists=true
|
||||
space-around-records=true
|
||||
space-around-variants=true
|
||||
type-decl=sparse
|
||||
wrap-comments=false
|
||||
wrap-fun-args=true
|
3
dune-project
Normal file
3
dune-project
Normal file
@ -0,0 +1,3 @@
|
||||
(lang dune 3.0)
|
||||
|
||||
(using mdx 0.2)
|
81
figure_ocaml_bit1.mps
Normal file
81
figure_ocaml_bit1.mps
Normal file
@ -0,0 +1,81 @@
|
||||
%!PS
|
||||
%%BoundingBox: -19 -38 738 77
|
||||
%%HiResBoundingBox: -18.67961 -37.97945 737.37283 76.11877
|
||||
%%Creator: MetaPost 2.02
|
||||
%%CreationDate: 2023.07.12:1752
|
||||
%%Pages: 1
|
||||
%*Font: cmr10 82.71204 9.96265 2e:bff8000000001536ee2
|
||||
%*Font: cmmi10 82.71204 9.96265 3a:8000000001a4082
|
||||
%*Font: cmr7 57.89838 6.97385 30:e
|
||||
%*Font: cmmi7 57.89838 6.97385 6e:8
|
||||
%*Font: cmsy7 57.89838 6.97385 00:8
|
||||
%%BeginProlog
|
||||
%%EndProlog
|
||||
%%Page: 1 1
|
||||
0 0 0 setrgbcolor
|
||||
0 0 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
35.497 -12.40683 moveto
|
||||
(n) cmmi7 57.89838 fshow
|
||||
76.38454 -12.40683 moveto
|
||||
(\000) cmsy7 57.89838 fshow
|
||||
128.07906 -12.40683 moveto
|
||||
(1) cmr7 57.89838 fshow
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop [] 0 setdash
|
||||
1 setlinejoin 10 setmiterlimit
|
||||
newpath 181.78896 -35.90388 moveto
|
||||
181.78896 74.04321 lineto
|
||||
-16.60405 74.04321 lineto
|
||||
-16.60405 -35.90388 lineto
|
||||
closepath stroke
|
||||
198.39389 0 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
233.89088 -12.40683 moveto
|
||||
(n) cmmi7 57.89838 fshow
|
||||
274.77843 -12.40683 moveto
|
||||
(\000) cmsy7 57.89838 fshow
|
||||
326.47295 -12.40683 moveto
|
||||
(2) cmr7 57.89838 fshow
|
||||
newpath 380.18246 -35.90388 moveto
|
||||
380.18246 74.04321 lineto
|
||||
181.78946 74.04321 lineto
|
||||
181.78946 -35.90388 lineto
|
||||
closepath stroke
|
||||
396.78778 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
433.5483 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
470.3097 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
newpath 523.67413 -35.90388 moveto
|
||||
523.67413 74.04321 lineto
|
||||
380.18297 74.04321 lineto
|
||||
380.18297 -35.90388 lineto
|
||||
closepath stroke
|
||||
540.2783 -3.44638 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
575.7753 -15.85321 moveto
|
||||
(1) cmr7 57.89838 fshow
|
||||
newpath 629.48558 -35.90388 moveto
|
||||
629.48558 74.04321 lineto
|
||||
523.67387 74.04321 lineto
|
||||
523.67387 -35.90388 lineto
|
||||
closepath stroke
|
||||
0.67844 0.84706 0.90196 setrgbcolor
|
||||
newpath 735.29727 -35.90388 moveto
|
||||
735.29727 74.04321 lineto
|
||||
629.48558 74.04321 lineto
|
||||
629.48558 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
646.09001 -3.44638 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
681.58699 -15.85321 moveto
|
||||
(0) cmr7 57.89838 fshow
|
||||
newpath 735.29727 -35.90388 moveto
|
||||
735.29727 74.04321 lineto
|
||||
629.48558 74.04321 lineto
|
||||
629.48558 -35.90388 lineto
|
||||
closepath stroke
|
||||
showpage
|
||||
%%EOF
|
167
figure_ocaml_bit2.mps
Normal file
167
figure_ocaml_bit2.mps
Normal file
@ -0,0 +1,167 @@
|
||||
%!PS
|
||||
%%BoundingBox: -19 -38 1565 77
|
||||
%%HiResBoundingBox: -18.67961 -37.97945 1564.63359 76.11877
|
||||
%%Creator: MetaPost 2.02
|
||||
%%CreationDate: 2023.07.12:1752
|
||||
%%Pages: 1
|
||||
%*Font: cmr10 82.71204 9.96265 2e:bff8000000001536ee2
|
||||
%*Font: cmmi10 82.71204 9.96265 3a:8000000001a4082
|
||||
%*Font: cmr7 57.89838 6.97385 30:e
|
||||
%*Font: cmmi7 57.89838 6.97385 6e:8
|
||||
%*Font: cmsy7 57.89838 6.97385 00:8
|
||||
%%BeginProlog
|
||||
%%EndProlog
|
||||
%%Page: 1 1
|
||||
0 0 0 setrgbcolor
|
||||
0 0 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
35.497 -12.40683 moveto
|
||||
(n) cmmi7 57.89838 fshow
|
||||
76.38454 -12.40683 moveto
|
||||
(\000) cmsy7 57.89838 fshow
|
||||
128.07906 -12.40683 moveto
|
||||
(1) cmr7 57.89838 fshow
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop [] 0 setdash
|
||||
1 setlinejoin 10 setmiterlimit
|
||||
newpath 181.78896 -35.90388 moveto
|
||||
181.78896 74.04321 lineto
|
||||
-16.60405 74.04321 lineto
|
||||
-16.60405 -35.90388 lineto
|
||||
closepath stroke
|
||||
198.39389 0 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
233.89088 -12.40683 moveto
|
||||
(n) cmmi7 57.89838 fshow
|
||||
274.77843 -12.40683 moveto
|
||||
(\000) cmsy7 57.89838 fshow
|
||||
326.47295 -12.40683 moveto
|
||||
(2) cmr7 57.89838 fshow
|
||||
newpath 380.18246 -35.90388 moveto
|
||||
380.18246 74.04321 lineto
|
||||
181.78946 74.04321 lineto
|
||||
181.78946 -35.90388 lineto
|
||||
closepath stroke
|
||||
396.78778 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
433.5483 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
470.3097 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
newpath 523.67413 -35.90388 moveto
|
||||
523.67413 74.04321 lineto
|
||||
380.18297 74.04321 lineto
|
||||
380.18297 -35.90388 lineto
|
||||
closepath stroke
|
||||
540.2783 -3.44638 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
575.7753 -15.85321 moveto
|
||||
(1) cmr7 57.89838 fshow
|
||||
newpath 629.48558 -35.90388 moveto
|
||||
629.48558 74.04321 lineto
|
||||
523.67387 74.04321 lineto
|
||||
523.67387 -35.90388 lineto
|
||||
closepath stroke
|
||||
1 0.5 0.5 setrgbcolor
|
||||
newpath 704.05084 -35.90388 moveto
|
||||
704.05084 74.04321 lineto
|
||||
629.48595 74.04321 lineto
|
||||
629.48595 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
646.09001 -7.58191 moveto
|
||||
(0) cmr10 82.71204 fshow
|
||||
newpath 704.05084 -35.90388 moveto
|
||||
704.05084 74.04321 lineto
|
||||
629.48595 74.04321 lineto
|
||||
629.48595 -35.90388 lineto
|
||||
closepath stroke
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath 1040.29614 -35.90388 moveto
|
||||
1040.29614 74.04321 lineto
|
||||
841.90314 74.04321 lineto
|
||||
841.90314 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
858.50719 0 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
894.00418 -12.40683 moveto
|
||||
(n) cmmi7 57.89838 fshow
|
||||
934.89172 -12.40683 moveto
|
||||
(\000) cmsy7 57.89838 fshow
|
||||
986.58624 -12.40683 moveto
|
||||
(1) cmr7 57.89838 fshow
|
||||
newpath 1040.29614 -35.90388 moveto
|
||||
1040.29614 74.04321 lineto
|
||||
841.90314 74.04321 lineto
|
||||
841.90314 -35.90388 lineto
|
||||
closepath stroke
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath 1238.68965 -35.90388 moveto
|
||||
1238.68965 74.04321 lineto
|
||||
1040.29665 74.04321 lineto
|
||||
1040.29665 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
1056.90108 0 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
1092.39807 -12.40683 moveto
|
||||
(n) cmmi7 57.89838 fshow
|
||||
1133.28561 -12.40683 moveto
|
||||
(\000) cmsy7 57.89838 fshow
|
||||
1184.98013 -12.40683 moveto
|
||||
(2) cmr7 57.89838 fshow
|
||||
newpath 1238.68965 -35.90388 moveto
|
||||
1238.68965 74.04321 lineto
|
||||
1040.29665 74.04321 lineto
|
||||
1040.29665 -35.90388 lineto
|
||||
closepath stroke
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath 1382.18132 -35.90388 moveto
|
||||
1382.18132 74.04321 lineto
|
||||
1238.69016 74.04321 lineto
|
||||
1238.69016 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
1255.29497 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
1292.05548 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
1328.81688 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
newpath 1382.18132 -35.90388 moveto
|
||||
1382.18132 74.04321 lineto
|
||||
1238.69016 74.04321 lineto
|
||||
1238.69016 -35.90388 lineto
|
||||
closepath stroke
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath 1487.99277 -35.90388 moveto
|
||||
1487.99277 74.04321 lineto
|
||||
1382.18106 74.04321 lineto
|
||||
1382.18106 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
1398.78549 -3.44638 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
1434.28249 -15.85321 moveto
|
||||
(1) cmr7 57.89838 fshow
|
||||
newpath 1487.99277 -35.90388 moveto
|
||||
1487.99277 74.04321 lineto
|
||||
1382.18106 74.04321 lineto
|
||||
1382.18106 -35.90388 lineto
|
||||
closepath stroke
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath 1562.55803 -35.90388 moveto
|
||||
1562.55803 74.04321 lineto
|
||||
1487.99313 74.04321 lineto
|
||||
1487.99313 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
1504.5972 -7.58191 moveto
|
||||
(0) cmr10 82.71204 fshow
|
||||
newpath 1562.55803 -35.90388 moveto
|
||||
1562.55803 74.04321 lineto
|
||||
1487.99313 74.04321 lineto
|
||||
1487.99313 -35.90388 lineto
|
||||
closepath stroke
|
||||
showpage
|
||||
%%EOF
|
167
figure_ocaml_bit3.mps
Normal file
167
figure_ocaml_bit3.mps
Normal file
@ -0,0 +1,167 @@
|
||||
%!PS
|
||||
%%BoundingBox: -19 -38 1565 77
|
||||
%%HiResBoundingBox: -18.67961 -37.97945 1564.63359 76.11877
|
||||
%%Creator: MetaPost 2.02
|
||||
%%CreationDate: 2023.07.12:1752
|
||||
%%Pages: 1
|
||||
%*Font: cmr10 82.71204 9.96265 2e:bff8000000001536ee2
|
||||
%*Font: cmmi10 82.71204 9.96265 3a:8000000001a4082
|
||||
%*Font: cmr7 57.89838 6.97385 30:e
|
||||
%*Font: cmmi7 57.89838 6.97385 6e:8
|
||||
%*Font: cmsy7 57.89838 6.97385 00:8
|
||||
%%BeginProlog
|
||||
%%EndProlog
|
||||
%%Page: 1 1
|
||||
0 0 0 setrgbcolor
|
||||
0 0 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
35.497 -12.40683 moveto
|
||||
(n) cmmi7 57.89838 fshow
|
||||
76.38454 -12.40683 moveto
|
||||
(\000) cmsy7 57.89838 fshow
|
||||
128.07906 -12.40683 moveto
|
||||
(1) cmr7 57.89838 fshow
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop [] 0 setdash
|
||||
1 setlinejoin 10 setmiterlimit
|
||||
newpath 181.78896 -35.90388 moveto
|
||||
181.78896 74.04321 lineto
|
||||
-16.60405 74.04321 lineto
|
||||
-16.60405 -35.90388 lineto
|
||||
closepath stroke
|
||||
198.39389 0 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
233.89088 -12.40683 moveto
|
||||
(n) cmmi7 57.89838 fshow
|
||||
274.77843 -12.40683 moveto
|
||||
(\000) cmsy7 57.89838 fshow
|
||||
326.47295 -12.40683 moveto
|
||||
(2) cmr7 57.89838 fshow
|
||||
newpath 380.18246 -35.90388 moveto
|
||||
380.18246 74.04321 lineto
|
||||
181.78946 74.04321 lineto
|
||||
181.78946 -35.90388 lineto
|
||||
closepath stroke
|
||||
396.78778 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
433.5483 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
470.3097 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
newpath 523.67413 -35.90388 moveto
|
||||
523.67413 74.04321 lineto
|
||||
380.18297 74.04321 lineto
|
||||
380.18297 -35.90388 lineto
|
||||
closepath stroke
|
||||
540.2783 -3.44638 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
575.7753 -15.85321 moveto
|
||||
(1) cmr7 57.89838 fshow
|
||||
newpath 629.48558 -35.90388 moveto
|
||||
629.48558 74.04321 lineto
|
||||
523.67387 74.04321 lineto
|
||||
523.67387 -35.90388 lineto
|
||||
closepath stroke
|
||||
1 0.5 1 setrgbcolor
|
||||
newpath 704.05084 -35.90388 moveto
|
||||
704.05084 74.04321 lineto
|
||||
629.48595 74.04321 lineto
|
||||
629.48595 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
646.09001 -7.58191 moveto
|
||||
(1) cmr10 82.71204 fshow
|
||||
newpath 704.05084 -35.90388 moveto
|
||||
704.05084 74.04321 lineto
|
||||
629.48595 74.04321 lineto
|
||||
629.48595 -35.90388 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 1040.29614 -35.90388 moveto
|
||||
1040.29614 74.04321 lineto
|
||||
841.90314 74.04321 lineto
|
||||
841.90314 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
858.50719 0 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
894.00418 -12.40683 moveto
|
||||
(n) cmmi7 57.89838 fshow
|
||||
934.89172 -12.40683 moveto
|
||||
(\000) cmsy7 57.89838 fshow
|
||||
986.58624 -12.40683 moveto
|
||||
(1) cmr7 57.89838 fshow
|
||||
newpath 1040.29614 -35.90388 moveto
|
||||
1040.29614 74.04321 lineto
|
||||
841.90314 74.04321 lineto
|
||||
841.90314 -35.90388 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 1238.68965 -35.90388 moveto
|
||||
1238.68965 74.04321 lineto
|
||||
1040.29665 74.04321 lineto
|
||||
1040.29665 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
1056.90108 0 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
1092.39807 -12.40683 moveto
|
||||
(n) cmmi7 57.89838 fshow
|
||||
1133.28561 -12.40683 moveto
|
||||
(\000) cmsy7 57.89838 fshow
|
||||
1184.98013 -12.40683 moveto
|
||||
(2) cmr7 57.89838 fshow
|
||||
newpath 1238.68965 -35.90388 moveto
|
||||
1238.68965 74.04321 lineto
|
||||
1040.29665 74.04321 lineto
|
||||
1040.29665 -35.90388 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 1382.18132 -35.90388 moveto
|
||||
1382.18132 74.04321 lineto
|
||||
1238.69016 74.04321 lineto
|
||||
1238.69016 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
1255.29497 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
1292.05548 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
1328.81688 14.70433 moveto
|
||||
(.) cmr10 82.71204 fshow
|
||||
newpath 1382.18132 -35.90388 moveto
|
||||
1382.18132 74.04321 lineto
|
||||
1238.69016 74.04321 lineto
|
||||
1238.69016 -35.90388 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 1487.99277 -35.90388 moveto
|
||||
1487.99277 74.04321 lineto
|
||||
1382.18106 74.04321 lineto
|
||||
1382.18106 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
1398.78549 -3.44638 moveto
|
||||
(b) cmmi10 82.71204 fshow
|
||||
1434.28249 -15.85321 moveto
|
||||
(1) cmr7 57.89838 fshow
|
||||
newpath 1487.99277 -35.90388 moveto
|
||||
1487.99277 74.04321 lineto
|
||||
1382.18106 74.04321 lineto
|
||||
1382.18106 -35.90388 lineto
|
||||
closepath stroke
|
||||
1 0.5 1 setrgbcolor
|
||||
newpath 1562.55803 -35.90388 moveto
|
||||
1562.55803 74.04321 lineto
|
||||
1487.99313 74.04321 lineto
|
||||
1487.99313 -35.90388 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
1504.5972 -7.58191 moveto
|
||||
(1) cmr10 82.71204 fshow
|
||||
newpath 1562.55803 -35.90388 moveto
|
||||
1562.55803 74.04321 lineto
|
||||
1487.99313 74.04321 lineto
|
||||
1487.99313 -35.90388 lineto
|
||||
closepath stroke
|
||||
showpage
|
||||
%%EOF
|
191
figure_ocaml_float1.mps
Normal file
191
figure_ocaml_float1.mps
Normal file
@ -0,0 +1,191 @@
|
||||
%!PS
|
||||
%%BoundingBox: -542 -495 764 46
|
||||
%%HiResBoundingBox: -541.88895 -494.06215 763.49677 45.33156
|
||||
%%Creator: MetaPost 2.02
|
||||
%%CreationDate: 2023.07.12:1752
|
||||
%%Pages: 1
|
||||
%*Font: cmr10 82.71204 9.96265 30:ffe000000000549098
|
||||
%*Font: cmmi10 82.71204 9.96265 3a:8
|
||||
%%BeginProlog
|
||||
%%EndProlog
|
||||
%%Page: 1 1
|
||||
0.67844 0.84706 0.90196 setrgbcolor
|
||||
newpath 33.20886 -43.256 moveto
|
||||
33.20886 43.256 lineto
|
||||
-33.20886 43.256 lineto
|
||||
-33.20886 -43.256 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor 0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
[] 0 setdash 1 setlinejoin 10 setmiterlimit
|
||||
newpath 33.20886 -43.256 moveto
|
||||
33.20886 43.256 lineto
|
||||
-33.20886 43.256 lineto
|
||||
-33.20886 -43.256 lineto
|
||||
closepath stroke
|
||||
49.8133 -26.65157 moveto
|
||||
(12) cmr10 82.71204 fshow
|
||||
132.52583 -26.65157 moveto
|
||||
(:) cmmi10 82.71204 fshow
|
||||
155.50134 -26.65157 moveto
|
||||
(13) cmr10 82.71204 fshow
|
||||
newpath 254.81833 -43.256 moveto
|
||||
254.81833 43.256 lineto
|
||||
33.20886 43.256 lineto
|
||||
33.20886 -43.256 lineto
|
||||
closepath stroke
|
||||
0.67844 0.84706 0.90196 setrgbcolor
|
||||
newpath -473.39566 -257.57466 moveto
|
||||
-473.39566 -191.1567 lineto
|
||||
-539.81339 -191.1567 lineto
|
||||
-539.81339 -257.57466 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath -473.39566 -257.57466 moveto
|
||||
-473.39566 -191.1567 lineto
|
||||
-539.81339 -191.1567 lineto
|
||||
-539.81339 -257.57466 lineto
|
||||
closepath stroke
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath -373.76907 -257.57466 moveto
|
||||
-373.76907 -191.1567 lineto
|
||||
-473.39566 -191.1567 lineto
|
||||
-473.39566 -257.57466 lineto
|
||||
closepath fill
|
||||
1 0.5 0.5 setrgbcolor
|
||||
newpath -373.76907 -240.97023 moveto
|
||||
-373.76907 -207.76112 lineto
|
||||
-406.97794 -207.76112 lineto
|
||||
-406.97794 -240.97023 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath -373.76907 -257.57466 moveto
|
||||
-373.76907 -191.1567 lineto
|
||||
-473.39566 -191.1567 lineto
|
||||
-473.39566 -257.57466 lineto
|
||||
closepath stroke
|
||||
newpath -373.76907 -257.57466 moveto
|
||||
-373.76907 -191.1567 lineto
|
||||
-473.39566 -191.1567 lineto
|
||||
-473.39566 -257.57466 lineto
|
||||
closepath stroke
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath -274.14249 -257.57466 moveto
|
||||
-274.14249 -191.1567 lineto
|
||||
-373.76907 -191.1567 lineto
|
||||
-373.76907 -257.57466 lineto
|
||||
closepath fill
|
||||
1 0.5 0.5 setrgbcolor
|
||||
newpath -274.14249 -240.97023 moveto
|
||||
-274.14249 -207.76112 lineto
|
||||
-307.35135 -207.76112 lineto
|
||||
-307.35135 -240.97023 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath -274.14249 -257.57466 moveto
|
||||
-274.14249 -191.1567 lineto
|
||||
-373.76907 -191.1567 lineto
|
||||
-373.76907 -257.57466 lineto
|
||||
closepath stroke
|
||||
newpath -274.14249 -257.57466 moveto
|
||||
-274.14249 -191.1567 lineto
|
||||
-373.76907 -191.1567 lineto
|
||||
-373.76907 -257.57466 lineto
|
||||
closepath stroke
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath -174.5159 -257.57466 moveto
|
||||
-174.5159 -191.1567 lineto
|
||||
-274.14249 -191.1567 lineto
|
||||
-274.14249 -257.57466 lineto
|
||||
closepath fill
|
||||
1 0.5 0.5 setrgbcolor
|
||||
newpath -174.5159 -240.97023 moveto
|
||||
-174.5159 -207.76112 lineto
|
||||
-207.72476 -207.76112 lineto
|
||||
-207.72476 -240.97023 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath -174.5159 -257.57466 moveto
|
||||
-174.5159 -191.1567 lineto
|
||||
-274.14249 -191.1567 lineto
|
||||
-274.14249 -257.57466 lineto
|
||||
closepath stroke
|
||||
newpath -174.5159 -257.57466 moveto
|
||||
-174.5159 -191.1567 lineto
|
||||
-274.14249 -191.1567 lineto
|
||||
-274.14249 -257.57466 lineto
|
||||
closepath stroke
|
||||
0.67844 0.84706 0.90196 setrgbcolor
|
||||
newpath -39.17152 -267.62167 moveto
|
||||
-39.17152 -181.10968 lineto
|
||||
-105.58925 -181.10968 lineto
|
||||
-105.58925 -267.62167 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath -39.17152 -267.62167 moveto
|
||||
-39.17152 -181.10968 lineto
|
||||
-105.58925 -181.10968 lineto
|
||||
-105.58925 -267.62167 lineto
|
||||
closepath stroke
|
||||
-22.5671 -251.01724 moveto
|
||||
(6) cmr10 82.71204 fshow
|
||||
18.78868 -251.01724 moveto
|
||||
(:) cmmi10 82.71204 fshow
|
||||
41.76431 -251.01724 moveto
|
||||
(28318530717958623) cmr10 82.71204 fshow
|
||||
newpath 761.4212 -267.62167 moveto
|
||||
761.4212 -181.10968 lineto
|
||||
-39.17152 -181.10968 lineto
|
||||
-39.17152 -267.62167 lineto
|
||||
closepath stroke
|
||||
0.67844 0.84706 0.90196 setrgbcolor
|
||||
newpath 53.88687 -491.98659 moveto
|
||||
53.88687 -405.47461 lineto
|
||||
-12.53085 -405.47461 lineto
|
||||
-12.53085 -491.98659 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 53.88687 -491.98659 moveto
|
||||
53.88687 -405.47461 lineto
|
||||
-12.53085 -405.47461 lineto
|
||||
-12.53085 -491.98659 lineto
|
||||
closepath stroke
|
||||
70.4913 -475.38216 moveto
|
||||
(42) cmr10 82.71204 fshow
|
||||
153.20384 -475.38216 moveto
|
||||
(:) cmmi10 82.71204 fshow
|
||||
176.17935 -475.38216 moveto
|
||||
(0) cmr10 82.71204 fshow
|
||||
newpath 234.13956 -491.98659 moveto
|
||||
234.13956 -405.47461 lineto
|
||||
53.88687 -405.47461 lineto
|
||||
53.88687 -491.98659 lineto
|
||||
closepath stroke
|
||||
0 33.20886 dtransform truncate idtransform setlinewidth pop 1 setlinecap
|
||||
newpath -440.1868 -224.36568 moveto 0 0 rlineto stroke
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
newpath -440.1868 -224.36568 moveto
|
||||
-58.92336 -30.03346 lineto stroke
|
||||
newpath -51.16765 -45.09288 moveto
|
||||
-33.20341 -17.16234 lineto
|
||||
-66.37402 -15.5702 lineto
|
||||
closepath fill
|
||||
0 33.20886 dtransform truncate idtransform setlinewidth pop
|
||||
newpath -340.56021 -224.36568 moveto 0 0 rlineto stroke
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
newpath -340.56021 -224.36568 moveto
|
||||
-37.05315 -412.8737 lineto stroke
|
||||
newpath -45.71716 -426.72066 moveto
|
||||
-12.52908 -427.89372 lineto
|
||||
-28.10713 -398.56615 lineto
|
||||
closepath fill
|
||||
0 33.20886 dtransform truncate idtransform setlinewidth pop
|
||||
newpath -240.93362 -224.36568 moveto 0 0 rlineto stroke
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
newpath -240.93362 -224.36568 moveto
|
||||
-134.3469 -224.36568 lineto stroke
|
||||
newpath -134.34727 -240.97011 moveto
|
||||
-105.5876 -224.36568 lineto
|
||||
-134.34727 -207.76125 lineto
|
||||
closepath fill
|
||||
showpage
|
||||
%%EOF
|
80
figure_ocaml_float2.mps
Normal file
80
figure_ocaml_float2.mps
Normal file
@ -0,0 +1,80 @@
|
||||
%!PS
|
||||
%%BoundingBox: -36 -46 1238 46
|
||||
%%HiResBoundingBox: -35.28442 -45.33156 1237.74081 45.33156
|
||||
%%Creator: MetaPost 2.02
|
||||
%%CreationDate: 2023.07.12:1752
|
||||
%%Pages: 1
|
||||
%*Font: cmr10 82.71204 9.96265 30:ffe000000000549098
|
||||
%*Font: cmmi10 82.71204 9.96265 3a:8
|
||||
%%BeginProlog
|
||||
%%EndProlog
|
||||
%%Page: 1 1
|
||||
0.49803 0 0.49803 setrgbcolor
|
||||
newpath 33.20886 -43.256 moveto
|
||||
33.20886 43.256 lineto
|
||||
-33.20886 43.256 lineto
|
||||
-33.20886 -43.256 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor 0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
[] 0 setdash 1 setlinejoin 10 setmiterlimit
|
||||
newpath 33.20886 -43.256 moveto
|
||||
33.20886 43.256 lineto
|
||||
-33.20886 43.256 lineto
|
||||
-33.20886 -43.256 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 254.81833 -43.256 moveto
|
||||
254.81833 43.256 lineto
|
||||
33.20886 43.256 lineto
|
||||
33.20886 -43.256 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
49.8133 -26.65157 moveto
|
||||
(12) cmr10 82.71204 fshow
|
||||
132.52583 -26.65157 moveto
|
||||
(:) cmmi10 82.71204 fshow
|
||||
155.50134 -26.65157 moveto
|
||||
(13) cmr10 82.71204 fshow
|
||||
newpath 254.81833 -43.256 moveto
|
||||
254.81833 43.256 lineto
|
||||
33.20886 43.256 lineto
|
||||
33.20886 -43.256 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 435.07013 -43.256 moveto
|
||||
435.07013 43.256 lineto
|
||||
254.81744 43.256 lineto
|
||||
254.81744 -43.256 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
271.42188 -26.65157 moveto
|
||||
(42) cmr10 82.71204 fshow
|
||||
354.13441 -26.65157 moveto
|
||||
(:) cmmi10 82.71204 fshow
|
||||
377.10992 -26.65157 moveto
|
||||
(0) cmr10 82.71204 fshow
|
||||
newpath 435.07013 -43.256 moveto
|
||||
435.07013 43.256 lineto
|
||||
254.81744 43.256 lineto
|
||||
254.81744 -43.256 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 1235.66525 -43.256 moveto
|
||||
1235.66525 43.256 lineto
|
||||
435.07253 43.256 lineto
|
||||
435.07253 -43.256 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
451.67456 -26.65157 moveto
|
||||
(6) cmr10 82.71204 fshow
|
||||
493.03032 -26.65157 moveto
|
||||
(:) cmmi10 82.71204 fshow
|
||||
516.00595 -26.65157 moveto
|
||||
(28318530717958623) cmr10 82.71204 fshow
|
||||
newpath 1235.66525 -43.256 moveto
|
||||
1235.66525 43.256 lineto
|
||||
435.07253 43.256 lineto
|
||||
435.07253 -43.256 lineto
|
||||
closepath stroke
|
||||
showpage
|
||||
%%EOF
|
365
figure_ocaml_layout.mps
Normal file
365
figure_ocaml_layout.mps
Normal file
@ -0,0 +1,365 @@
|
||||
%!PS
|
||||
%%BoundingBox: -88 -669 1107 144
|
||||
%%HiResBoundingBox: -87.95122 -668.42198 1106.51346 143.19992
|
||||
%%Creator: MetaPost 2.02
|
||||
%%CreationDate: 2023.07.12:1752
|
||||
%%Pages: 1
|
||||
%*Font: cmr10 82.71204 9.96265 2e:bff8000000001536ee2
|
||||
%*Font: cmtt10 82.71204 9.96265 31:c000000000008081418
|
||||
%%BeginProlog
|
||||
%%EndProlog
|
||||
%%Page: 1 1
|
||||
0 0 0 setrgbcolor
|
||||
0 0 moveto
|
||||
(stac) cmr10 82.71204 fshow
|
||||
140.61041 0 moveto
|
||||
(k:) cmr10 82.71204 fshow
|
||||
-87.95122 -221.60858 moveto
|
||||
(array1) cmtt10 82.71204 fshow
|
||||
172.58894 -221.60858 moveto
|
||||
(:) cmr10 82.71204 fshow
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath 311.79547 -238.73482 moveto
|
||||
311.79547 -172.31683 lineto
|
||||
212.16888 -172.31683 lineto
|
||||
212.16888 -238.73482 lineto
|
||||
closepath fill
|
||||
1 0.5 0.5 setrgbcolor
|
||||
newpath 311.79547 -222.13039 moveto
|
||||
311.79547 -188.92126 lineto
|
||||
278.58661 -188.92126 lineto
|
||||
278.58661 -222.13039 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor 0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
[] 0 setdash 1 setlinejoin 10 setmiterlimit
|
||||
newpath 311.79547 -238.73482 moveto
|
||||
311.79547 -172.31683 lineto
|
||||
212.16888 -172.31683 lineto
|
||||
212.16888 -238.73482 lineto
|
||||
closepath stroke
|
||||
-87.95122 -323.7441 moveto
|
||||
(array2) cmtt10 82.71204 fshow
|
||||
172.58894 -323.7441 moveto
|
||||
(:) cmr10 82.71204 fshow
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath 311.79547 -340.87033 moveto
|
||||
311.79547 -274.45235 lineto
|
||||
212.16888 -274.45235 lineto
|
||||
212.16888 -340.87033 lineto
|
||||
closepath fill
|
||||
1 0.5 0.5 setrgbcolor
|
||||
newpath 311.79547 -324.2659 moveto
|
||||
311.79547 -291.05678 lineto
|
||||
278.58661 -291.05678 lineto
|
||||
278.58661 -324.2659 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 311.79547 -340.87033 moveto
|
||||
311.79547 -274.45235 lineto
|
||||
212.16888 -274.45235 lineto
|
||||
212.16888 -340.87033 lineto
|
||||
closepath stroke
|
||||
-1.10428 -425.87961 moveto
|
||||
(pair) cmtt10 82.71204 fshow
|
||||
172.5897 -425.87961 moveto
|
||||
(:) cmr10 82.71204 fshow
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath 311.79547 -443.00584 moveto
|
||||
311.79547 -376.58788 lineto
|
||||
212.16888 -376.58788 lineto
|
||||
212.16888 -443.00584 lineto
|
||||
closepath fill
|
||||
1 0.5 0.5 setrgbcolor
|
||||
newpath 311.79547 -426.40141 moveto
|
||||
311.79547 -393.1923 lineto
|
||||
278.58661 -393.1923 lineto
|
||||
278.58661 -426.40141 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 311.79547 -443.00584 moveto
|
||||
311.79547 -376.58788 lineto
|
||||
212.16888 -376.58788 lineto
|
||||
212.16888 -443.00584 lineto
|
||||
closepath stroke
|
||||
46.45331 -538.53073 moveto
|
||||
(x) cmtt10 82.71204 fshow
|
||||
89.8764 -538.53073 moveto
|
||||
(:) cmr10 82.71204 fshow
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 311.79471 -580.58514 moveto
|
||||
311.79471 -460.8643 lineto
|
||||
129.45659 -460.8643 lineto
|
||||
129.45659 -580.58514 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
162.6652 -547.37628 moveto
|
||||
(42) cmr10 82.71204 fshow
|
||||
1 0.5 1 setrgbcolor
|
||||
newpath 311.79547 -537.32928 moveto
|
||||
311.79547 -504.12016 lineto
|
||||
278.58661 -504.12016 lineto
|
||||
278.58661 -537.32928 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 311.79471 -580.58514 moveto
|
||||
311.79471 -460.8643 lineto
|
||||
129.45659 -460.8643 lineto
|
||||
129.45659 -580.58514 lineto
|
||||
closepath stroke
|
||||
680.54593 85.76102 moveto
|
||||
(heap:) cmr10 82.71204 fshow
|
||||
0.67844 0.84706 0.90196 setrgbcolor
|
||||
newpath 598.77817 -204.50084 moveto
|
||||
598.77817 -84.78 lineto
|
||||
532.36044 -84.78 lineto
|
||||
532.36044 -204.50084 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 598.77817 -204.50084 moveto
|
||||
598.77817 -84.78 lineto
|
||||
532.36044 -84.78 lineto
|
||||
532.36044 -204.50084 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 739.76115 -204.50084 moveto
|
||||
739.76115 -84.78 lineto
|
||||
598.77855 -84.78 lineto
|
||||
598.77855 -204.50084 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
631.98703 -171.29198 moveto
|
||||
(1) cmr10 82.71204 fshow
|
||||
1 0.5 1 setrgbcolor
|
||||
newpath 739.76053 -161.24498 moveto
|
||||
739.76053 -128.03586 lineto
|
||||
706.55167 -128.03586 lineto
|
||||
706.55167 -161.24498 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 739.76115 -204.50084 moveto
|
||||
739.76115 -84.78 lineto
|
||||
598.77855 -84.78 lineto
|
||||
598.77855 -204.50084 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 880.74352 -204.50084 moveto
|
||||
880.74352 -84.78 lineto
|
||||
739.76091 -84.78 lineto
|
||||
739.76091 -204.50084 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
772.96939 -171.29198 moveto
|
||||
(2) cmr10 82.71204 fshow
|
||||
1 0.5 1 setrgbcolor
|
||||
newpath 880.74287 -161.24498 moveto
|
||||
880.74287 -128.03586 lineto
|
||||
847.53401 -128.03586 lineto
|
||||
847.53401 -161.24498 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 880.74352 -204.50084 moveto
|
||||
880.74352 -84.78 lineto
|
||||
739.76091 -84.78 lineto
|
||||
739.76091 -204.50084 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 1021.72586 -204.50084 moveto
|
||||
1021.72586 -84.78 lineto
|
||||
880.74326 -84.78 lineto
|
||||
880.74326 -204.50084 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
913.95276 -171.29198 moveto
|
||||
(3) cmr10 82.71204 fshow
|
||||
1 0.5 1 setrgbcolor
|
||||
newpath 1021.72624 -161.24498 moveto
|
||||
1021.72624 -128.03586 lineto
|
||||
988.51738 -128.03586 lineto
|
||||
988.51738 -161.24498 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 1021.72586 -204.50084 moveto
|
||||
1021.72586 -84.78 lineto
|
||||
880.74326 -84.78 lineto
|
||||
880.74326 -204.50084 lineto
|
||||
closepath stroke
|
||||
0.67844 0.84706 0.90196 setrgbcolor
|
||||
newpath 710.62549 -408.77226 moveto
|
||||
710.62549 -342.35428 lineto
|
||||
644.20776 -342.35428 lineto
|
||||
644.20776 -408.77226 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 710.62549 -408.77226 moveto
|
||||
710.62549 -342.35428 lineto
|
||||
644.20776 -342.35428 lineto
|
||||
644.20776 -408.77226 lineto
|
||||
closepath stroke
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath 810.25208 -408.77226 moveto
|
||||
810.25208 -342.35428 lineto
|
||||
710.62549 -342.35428 lineto
|
||||
710.62549 -408.77226 lineto
|
||||
closepath fill
|
||||
1 0.5 0.5 setrgbcolor
|
||||
newpath 810.25208 -392.16783 moveto
|
||||
810.25208 -358.95871 lineto
|
||||
777.04321 -358.95871 lineto
|
||||
777.04321 -392.16783 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 810.25208 -408.77226 moveto
|
||||
810.25208 -342.35428 lineto
|
||||
710.62549 -342.35428 lineto
|
||||
710.62549 -408.77226 lineto
|
||||
closepath stroke
|
||||
newpath 810.25208 -408.77226 moveto
|
||||
810.25208 -342.35428 lineto
|
||||
710.62549 -342.35428 lineto
|
||||
710.62549 -408.77226 lineto
|
||||
closepath stroke
|
||||
0.56471 0.93333 0.56471 setrgbcolor
|
||||
newpath 909.87866 -408.77226 moveto
|
||||
909.87866 -342.35428 lineto
|
||||
810.25208 -342.35428 lineto
|
||||
810.25208 -408.77226 lineto
|
||||
closepath fill
|
||||
1 0.5 0.5 setrgbcolor
|
||||
newpath 909.87866 -392.16783 moveto
|
||||
909.87866 -358.95871 lineto
|
||||
876.6698 -358.95871 lineto
|
||||
876.6698 -392.16783 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 909.87866 -408.77226 moveto
|
||||
909.87866 -342.35428 lineto
|
||||
810.25208 -342.35428 lineto
|
||||
810.25208 -408.77226 lineto
|
||||
closepath stroke
|
||||
newpath 909.87866 -408.77226 moveto
|
||||
909.87866 -342.35428 lineto
|
||||
810.25208 -342.35428 lineto
|
||||
810.25208 -408.77226 lineto
|
||||
closepath stroke
|
||||
0.67844 0.84706 0.90196 setrgbcolor
|
||||
newpath 516.06575 -666.34642 moveto
|
||||
516.06575 -546.62556 lineto
|
||||
449.64803 -546.62556 lineto
|
||||
449.64803 -666.34642 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 516.06575 -666.34642 moveto
|
||||
516.06575 -546.62556 lineto
|
||||
449.64803 -546.62556 lineto
|
||||
449.64803 -666.34642 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 698.40387 -666.34642 moveto
|
||||
698.40387 -546.62556 lineto
|
||||
516.06575 -546.62556 lineto
|
||||
516.06575 -666.34642 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
549.27461 -633.13756 moveto
|
||||
(42) cmr10 82.71204 fshow
|
||||
1 0.5 1 setrgbcolor
|
||||
newpath 698.40488 -623.09055 moveto
|
||||
698.40488 -589.88144 lineto
|
||||
665.19601 -589.88144 lineto
|
||||
665.19601 -623.09055 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 698.40387 -666.34642 moveto
|
||||
698.40387 -546.62556 lineto
|
||||
516.06575 -546.62556 lineto
|
||||
516.06575 -666.34642 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 880.743 -666.34642 moveto
|
||||
880.743 -546.62556 lineto
|
||||
698.40488 -546.62556 lineto
|
||||
698.40488 -666.34642 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
731.61374 -633.13756 moveto
|
||||
(99) cmr10 82.71204 fshow
|
||||
1 0.5 1 setrgbcolor
|
||||
newpath 880.74402 -623.09055 moveto
|
||||
880.74402 -589.88144 lineto
|
||||
847.53516 -589.88144 lineto
|
||||
847.53516 -623.09055 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 880.743 -666.34642 moveto
|
||||
880.743 -546.62556 lineto
|
||||
698.40488 -546.62556 lineto
|
||||
698.40488 -666.34642 lineto
|
||||
closepath stroke
|
||||
0.87843 1 1 setrgbcolor
|
||||
newpath 1104.4379 -666.34642 moveto
|
||||
1104.4379 -546.62556 lineto
|
||||
880.743 -546.62556 lineto
|
||||
880.743 -666.34642 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
913.95186 -633.13756 moveto
|
||||
(666) cmr10 82.71204 fshow
|
||||
1 0.5 1 setrgbcolor
|
||||
newpath 1104.4379 -623.09055 moveto
|
||||
1104.4379 -589.88144 lineto
|
||||
1071.22903 -589.88144 lineto
|
||||
1071.22903 -623.09055 lineto
|
||||
closepath fill
|
||||
0 0 0 setrgbcolor
|
||||
newpath 1104.4379 -666.34642 moveto
|
||||
1104.4379 -546.62556 lineto
|
||||
880.743 -546.62556 lineto
|
||||
880.743 -666.34642 lineto
|
||||
closepath stroke
|
||||
0 33.20886 dtransform truncate idtransform setlinewidth pop 1 setlinecap
|
||||
newpath 245.37775 -205.52544 moveto 0 0 rlineto stroke
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
newpath 245.37775 -205.52544 moveto
|
||||
504.01566 -156.34467 lineto stroke
|
||||
newpath 507.4073 -173.35524 moveto
|
||||
532.36209 -151.44398 lineto
|
||||
500.91005 -140.78815 lineto
|
||||
closepath fill
|
||||
0 33.20886 dtransform truncate idtransform setlinewidth pop
|
||||
newpath 245.37775 -307.66096 moveto 0 0 rlineto stroke
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
newpath 245.37775 -307.66096 moveto
|
||||
431.84949 -542.30128 lineto stroke
|
||||
newpath 418.74718 -552.73328 moveto
|
||||
449.6522 -564.88687 lineto
|
||||
444.7248 -532.04501 lineto
|
||||
closepath fill
|
||||
0 33.20886 dtransform truncate idtransform setlinewidth pop
|
||||
newpath 245.37775 -409.79648 moveto 0 0 rlineto stroke
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
newpath 245.37775 -409.79648 moveto
|
||||
615.49243 -380.46991 lineto stroke
|
||||
newpath 617.03897 -397.74753 moveto
|
||||
644.20549 -378.64822 lineto
|
||||
614.08171 -364.67067 lineto
|
||||
closepath fill
|
||||
0 33.20886 dtransform truncate idtransform setlinewidth pop
|
||||
newpath 743.83449 -375.56314 moveto 0 0 rlineto stroke
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
newpath 743.83449 -375.56314 moveto
|
||||
616.23808 -210.27614 lineto stroke
|
||||
newpath 629.5014 -200.02606 moveto
|
||||
598.77652 -187.42413 lineto
|
||||
603.22482 -220.33327 lineto
|
||||
closepath fill
|
||||
0 33.20886 dtransform truncate idtransform setlinewidth pop
|
||||
newpath 843.46361 -375.56314 moveto 0 0 rlineto stroke
|
||||
0 4.15111 dtransform truncate idtransform setlinewidth pop
|
||||
newpath 843.46361 -375.56314 moveto
|
||||
540.37408 -569.6539 lineto stroke
|
||||
newpath 531.24133 -555.48303 moveto
|
||||
516.06322 -585.02066 lineto
|
||||
549.2323 -583.39673 lineto
|
||||
closepath fill
|
||||
showpage
|
||||
%%EOF
|
6
layout.ml.tex
Normal file
6
layout.ml.tex
Normal file
@ -0,0 +1,6 @@
|
||||
\begin{BVerbatim}[commandchars=\\\{\}]
|
||||
\PY{k}{let} \PY{n}{array1} \PY{o}{=} \PY{o}{[|} \PY{l+m+mi}{1}\PY{o}{;} \PY{l+m+mi}{2}\PY{o}{;} \PY{l+m+mi}{3} \PY{o}{|]}
|
||||
\PY{k}{let} \PY{n}{array2} \PY{o}{=} \PY{o}{[|} \PY{l+m+mi}{42}\PY{o}{;} \PY{l+m+mi}{99}\PY{o}{;} \PY{l+m+mi}{666} \PY{o}{|]}
|
||||
\PY{k}{let} \PY{n}{pair} \PY{o}{=} \PY{o}{(}\PY{n}{array1}\PY{o}{,} \PY{n}{array2}\PY{o}{)}
|
||||
\PY{k}{let} \PY{n}{x} \PY{o}{=} \PY{l+m+mi}{42}
|
||||
\end{BVerbatim}
|
112
styledef.tex
Normal file
112
styledef.tex
Normal file
@ -0,0 +1,112 @@
|
||||
|
||||
\makeatletter
|
||||
\def\PY@reset{\let\PY@it=\relax \let\PY@bf=\relax%
|
||||
\let\PY@ul=\relax \let\PY@tc=\relax%
|
||||
\let\PY@bc=\relax \let\PY@ff=\relax}
|
||||
\def\PY@tok#1{\csname PY@tok@#1\endcsname}
|
||||
\def\PY@toks#1+{\ifx\relax#1\empty\else%
|
||||
\PY@tok{#1}\expandafter\PY@toks\fi}
|
||||
\def\PY@do#1{\PY@bc{\PY@tc{\PY@ul{%
|
||||
\PY@it{\PY@bf{\PY@ff{#1}}}}}}}
|
||||
\def\PY#1#2{\PY@reset\PY@toks#1+\relax+\PY@do{#2}}
|
||||
|
||||
\@namedef{PY@tok@}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@p}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@pm}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@k}{\def\PY@tc##1{\textcolor[rgb]{0.78,0.47,0.87}{##1}}}
|
||||
\@namedef{PY@tok@kc}{\def\PY@tc##1{\textcolor[rgb]{0.90,0.75,0.48}{##1}}}
|
||||
\@namedef{PY@tok@kd}{\def\PY@tc##1{\textcolor[rgb]{0.78,0.47,0.87}{##1}}}
|
||||
\@namedef{PY@tok@kn}{\def\PY@tc##1{\textcolor[rgb]{0.78,0.47,0.87}{##1}}}
|
||||
\@namedef{PY@tok@kr}{\def\PY@tc##1{\textcolor[rgb]{0.78,0.47,0.87}{##1}}}
|
||||
\@namedef{PY@tok@kt}{\def\PY@tc##1{\textcolor[rgb]{0.90,0.75,0.48}{##1}}}
|
||||
\@namedef{PY@tok@n}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@na}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@nb}{\def\PY@tc##1{\textcolor[rgb]{0.90,0.75,0.48}{##1}}}
|
||||
\@namedef{PY@tok@nc}{\def\PY@tc##1{\textcolor[rgb]{0.90,0.75,0.48}{##1}}}
|
||||
\@namedef{PY@tok@nf}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.38,0.69,0.94}{##1}}}
|
||||
\@namedef{PY@tok@fm}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.34,0.71,0.76}{##1}}}
|
||||
\@namedef{PY@tok@nx}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@nt}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@nd}{\def\PY@tc##1{\textcolor[rgb]{0.38,0.69,0.94}{##1}}}
|
||||
\@namedef{PY@tok@nv}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@vc}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@l}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@s}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@m}{\def\PY@tc##1{\textcolor[rgb]{0.82,0.60,0.40}{##1}}}
|
||||
\@namedef{PY@tok@o}{\def\PY@tc##1{\textcolor[rgb]{0.34,0.71,0.76}{##1}}}
|
||||
\@namedef{PY@tok@c}{\def\PY@tc##1{\textcolor[rgb]{0.50,0.52,0.56}{##1}}}
|
||||
\@namedef{PY@tok@w}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@esc}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@err}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@x}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@kp}{\def\PY@tc##1{\textcolor[rgb]{0.78,0.47,0.87}{##1}}}
|
||||
\@namedef{PY@tok@bp}{\def\PY@tc##1{\textcolor[rgb]{0.90,0.75,0.48}{##1}}}
|
||||
\@namedef{PY@tok@no}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@ni}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@ne}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@py}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@nl}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@nn}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@vg}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@vi}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@vm}{\def\PY@tc##1{\textcolor[rgb]{0.88,0.42,0.46}{##1}}}
|
||||
\@namedef{PY@tok@ld}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@sa}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@sb}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@sc}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@dl}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@sd}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@s2}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@se}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@sh}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@si}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@sx}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@sr}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@s1}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@ss}{\def\PY@tc##1{\textcolor[rgb]{0.60,0.76,0.47}{##1}}}
|
||||
\@namedef{PY@tok@mb}{\def\PY@tc##1{\textcolor[rgb]{0.82,0.60,0.40}{##1}}}
|
||||
\@namedef{PY@tok@mf}{\def\PY@tc##1{\textcolor[rgb]{0.82,0.60,0.40}{##1}}}
|
||||
\@namedef{PY@tok@mh}{\def\PY@tc##1{\textcolor[rgb]{0.82,0.60,0.40}{##1}}}
|
||||
\@namedef{PY@tok@mi}{\def\PY@tc##1{\textcolor[rgb]{0.82,0.60,0.40}{##1}}}
|
||||
\@namedef{PY@tok@il}{\def\PY@tc##1{\textcolor[rgb]{0.82,0.60,0.40}{##1}}}
|
||||
\@namedef{PY@tok@mo}{\def\PY@tc##1{\textcolor[rgb]{0.82,0.60,0.40}{##1}}}
|
||||
\@namedef{PY@tok@ow}{\def\PY@tc##1{\textcolor[rgb]{0.34,0.71,0.76}{##1}}}
|
||||
\@namedef{PY@tok@ch}{\def\PY@tc##1{\textcolor[rgb]{0.50,0.52,0.56}{##1}}}
|
||||
\@namedef{PY@tok@cm}{\def\PY@tc##1{\textcolor[rgb]{0.50,0.52,0.56}{##1}}}
|
||||
\@namedef{PY@tok@cp}{\def\PY@tc##1{\textcolor[rgb]{0.50,0.52,0.56}{##1}}}
|
||||
\@namedef{PY@tok@cpf}{\def\PY@tc##1{\textcolor[rgb]{0.50,0.52,0.56}{##1}}}
|
||||
\@namedef{PY@tok@c1}{\def\PY@tc##1{\textcolor[rgb]{0.50,0.52,0.56}{##1}}}
|
||||
\@namedef{PY@tok@cs}{\def\PY@tc##1{\textcolor[rgb]{0.50,0.52,0.56}{##1}}}
|
||||
\@namedef{PY@tok@g}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@gd}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@ge}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@gr}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@gh}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@gi}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@go}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@gp}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@gs}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@gu}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
\@namedef{PY@tok@gt}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.70,0.75}{##1}}}
|
||||
|
||||
\def\PYZbs{\char`\\}
|
||||
\def\PYZus{\char`\_}
|
||||
\def\PYZob{\char`\{}
|
||||
\def\PYZcb{\char`\}}
|
||||
\def\PYZca{\char`\^}
|
||||
\def\PYZam{\char`\&}
|
||||
\def\PYZlt{\char`\<}
|
||||
\def\PYZgt{\char`\>}
|
||||
\def\PYZsh{\char`\#}
|
||||
\def\PYZpc{\char`\%}
|
||||
\def\PYZdl{\char`\$}
|
||||
\def\PYZhy{\char`\-}
|
||||
\def\PYZsq{\char`\'}
|
||||
\def\PYZdq{\char`\"}
|
||||
\def\PYZti{\char`\~}
|
||||
% for compatibility with earlier versions
|
||||
\def\PYZat{@}
|
||||
\def\PYZlb{[}
|
||||
\def\PYZrb{]}
|
||||
\makeatother
|
||||
|
370
wasocaml.tex
370
wasocaml.tex
@ -7,10 +7,13 @@
|
||||
\usepackage{authblk} % author affiliation handling
|
||||
\renewcommand\Affilfont{\itshape\small}
|
||||
\usepackage{bbding}
|
||||
\usepackage{fancyvrb} % source code
|
||||
\input{styledef.tex} % source code
|
||||
\usepackage[most]{tcolorbox}
|
||||
\setmainfont{Linux Libertine O}
|
||||
\setsansfont{Linux Biolinum O}
|
||||
%\setsansfont{TeX Gyre Heros}
|
||||
\setmonofont[Scale=MatchLowercase]{RobotoMono Nerd Font}
|
||||
%% \setmonofont[Scale=MatchLowercase]{RobotoMono Nerd Font}
|
||||
|
||||
\title{Wasocaml: a compiler from OCaml to WebAssembly}
|
||||
|
||||
@ -25,31 +28,362 @@
|
||||
\maketitle
|
||||
|
||||
\begin{abstract}
|
||||
In this presentation, we will explore the compilation of garbage-collected languages, such as Java or OCaml, to WebAssembly (Wasm). The limitations of JavaScript as the web's default language led to the development of Wasm, a secure and predictable-performance modular language. However, compiling garbage-collected languages to Wasm presents challenges, including the need to compile or re-implement the runtime and difficulties in transferring verified properties. Various techniques for representing values in memory are discussed, with a focus on OCaml's approach. An extension called Wasm-GC is introduced, enabling the compilation of garbage-collected languages to Wasm by incorporating features like int31 and garbage-collected structs. The paper presents Wasocaml, a complete OCaml compiler for Wasm-GC, and discusses benchmarks and future work in compiling garbage-collected languages to WebAssembly.
|
||||
In this presentation, we will explore the compilation of garbage-collected languages, such as Java or OCaml, to WebAssembly (Wasm). The limitations of JavaScript as the web's default language led to the development of Wasm, a secure and predictable-performance modular language. However, compiling garbage-collected languages to Wasm presents challenges, including the need to compile or re-implement the runtime. Various techniques for representing values in memory are discussed, with a focus on OCaml's approach. An extension called Wasm-GC is introduced, enabling the compilation of garbage-collected languages to Wasm by incorporating features like int31 and garbage-collected structs. The paper presents Wasocaml, a complete OCaml compiler for Wasm-GC, and discusses benchmarks and future work in compiling garbage-collected languages to WebAssembly.
|
||||
\end{abstract}
|
||||
|
||||
\section{Javascript}
|
||||
Javascript is widely thought as being the de facto language of the web. However, it does show its limitations when it comes to performance, security and safety. In order to remedy this, WebAssembly (Wasm) has been developped as a secure modular language of predictable performance. Its usage has expanded beyond the web: finding applications in the cloud (Fastly, Cloudflare), in the creation of portable binaries as well as interfacing with C.
|
||||
\section{Context}
|
||||
\subsection{WASM}
|
||||
Javascript is widely thought as being the de facto language of the
|
||||
web. However, it does show its limitations when it comes to
|
||||
performance, security and safety. In order to remedy this, WebAssembly
|
||||
(Wasm) has been developped as a secure modular language of predictable
|
||||
performance. Its usage is expanding beyond the web: finding
|
||||
applications in the cloud (Fastly, Cloudflare), in the creation of
|
||||
portable binaries.
|
||||
|
||||
\section{Compiling Runtime-free Languages}
|
||||
The direct compilation of languages such as C, C++ or Rust to Wasm is rather simple and straightforward. Some primitives, such as malloc, have to be implemented manually in Wasm.
|
||||
Parler de JS\_of\_ocaml ici
|
||||
|
||||
\section{Compiling Garbage-Collected Languages}
|
||||
Compiling languages that use a Garbage Collector (GC) like Java or OCaml is trickier. It requires either: compiling the runtime (written in C) to Wasm or manually re-implementing the runtime is Wasm. Furthermore, generating code that is compatible with the compiled runtime of a third party compiler (for example, emscripten) is a challenge indeed. Since Wasm is a statically typed language with very specific static verifications, it is difficult to easily transfer the properties verified and guaranteed by the OCaml type-checker. This difficulty leads to a hardly maintainable and slower code because it has to conform to the Wasm type system. Any interaction with a host environment (for example, Javascript in a web browser) which also uses a GC can lead to further hurdles.
|
||||
The first version of WASM was meant to compile libraries in languages
|
||||
such as C, C++ or Rust to expose them for consumption by a Javascript
|
||||
program. It was designed with the explicit aim that future versions
|
||||
would catter to the specific needs of other languages and uses.
|
||||
|
||||
\section{Different Ways of Representing Values in Memory}
|
||||
Different approaches to handling polymorphism and the representation of values in memory will be presented. These techniques are linked to the way GCs work. We will present monomorphisation (Rust, C++), uniform representation by boxing everything (Python), uniform representation by boxing only polymorphic operations (Java), pointer tagging (OCaml) and runtime monomorphisation (F\#). We will especially focus on the representation used by OCaml, and there will be examples to illustrate the hardships of generating well-typed code from the IR (Intermediate Representations) of the compiler.
|
||||
The current version of WASM can be seen as simplified C.
|
||||
|
||||
\section{Wasm-GC: An extension to WebAssembly for Garbage-Collected languages}
|
||||
An extended version of Wasm, named Wasm-GC, will be presented which allows the compilation of different garbage-collected languages. This extension is comprised of features such as int31, sub-typing, garbage-collected structs and arrays.
|
||||
%% (func $fact (param $x i32) (result i32)
|
||||
%% (if (i32.eq (local.get $x) (i32.const 0)) (then (i32.const 1))
|
||||
%% (else (i32.mul (local.get $x) (call $fact (i32.sub (local.get $x) (i32.const 1))))
|
||||
%% ))
|
||||
|
||||
\section{IR et Flambda1 IR}
|
||||
The different IRs of OCaml will be briefly mentionned followed by a detailled analysis of Flambda1. We will then present the small-steps semantics of a subset of Flambda1 and show the formalisation of the compilation of that subset towards Wasm-GC.
|
||||
For instance a WASM program could only manipulate integers and floating
|
||||
point values, not garbage collected ones, like Javascript
|
||||
objects. This would have obviously been useful in a browser context,
|
||||
but would have required some interaction with the GC of the runtime
|
||||
environment.
|
||||
|
||||
\section{Compiling Flambda1}
|
||||
Eventually, we will present Wasmocaml. A complete compiler for OCaml based on Flambda1 targetting Wasm-GC. We will take the time to show the different strategies we tested and the problems we faced.
|
||||
This led to various extensions, in particular some that matter to
|
||||
OCaml.
|
||||
|
||||
\section{Benchmarks, future work}
|
||||
We will present different benchmarks to evaluate the performance of the compilation techniques discussed. To conclude, we will discuss the future works and other such possible improvements of the compilation of garbage-collected languages towards WebAssembly.
|
||||
\subsection{Extensions}
|
||||
|
||||
We will discuss the most notable ones, the reference, gc, and exception extensions
|
||||
|
||||
\subsubsection{References and GC}
|
||||
|
||||
The aim of those proposal is to allow the program to manipulate
|
||||
references to different kind of values like, opaque objects, functions
|
||||
and garbage collected values. Since WASM has to be memory safe, those
|
||||
can't be exposed as direct pointers, hence there is a type system
|
||||
verifying the proper manipulation of such values.
|
||||
|
||||
%% \texttt{
|
||||
%% (type $f1 (func (param i32) (result i32)))
|
||||
%% (type $t1 (array (ref i31))
|
||||
%% (type $t2 (struct ((field $a (ref $t1)) (field $b (ref $f1)) (field $c i32))))
|
||||
|
||||
%% (func (param $x (ref $t2)) (result i32)
|
||||
%% (i31.get_u (array.get $t1 (i32.const 0) (struct.get $t2 $a (local.get $x))))
|
||||
%% }
|
||||
|
||||
But WASM being a compilation target rather than a programming
|
||||
language, it needs to be able to represent the values of any kind of
|
||||
source language. It was not deemed possible to have a type system
|
||||
powerful enough to do that. Instead the decision was to have a simple
|
||||
one, but to rely on dynamic cast to fill the gaps, but garanty that
|
||||
those cast are very efficient.
|
||||
|
||||
Il n'y a que des struct des array des i31 des externref et des funcref
|
||||
|
||||
There is a subtyping type hierarchy that controls which cast are
|
||||
allowed. Some types are predefined by WASM: any, eq, extern, func,
|
||||
i31. Other are user defined: array and struct. There is a structural
|
||||
subtyping relation between user ones. Upcasts are implicits, downcasts
|
||||
are explicits and incorrect ones leads to runtime errors.
|
||||
It is possible to dynamically test for type compatibility.
|
||||
|
||||
\paragraph{Contribution to the proposals}
|
||||
|
||||
The general rule for the WASM comittee is to only include features
|
||||
with a demonstrated use case. As there are currently very few
|
||||
compilers targeting the GC-proposal some features where lacking
|
||||
conclusive evidence of their usefullness. In particular the i31
|
||||
reference type which was not required by the Dart compiler which was
|
||||
the only one targeting the GC-proposal at the time.
|
||||
|
||||
Wasocaml was written to validate the GC-proposal on a functionnal
|
||||
language and among other things demonstrate the usefulness of i31.
|
||||
|
||||
\subsubsection{Exception}
|
||||
|
||||
Another serious limitation is the absence of an exception
|
||||
mechanism. This was not a problem for compiling either C or Rust, but
|
||||
C++ does require them. It is of course possible to encode those, but
|
||||
this has a significative runtime cost and limits the interractions
|
||||
with Javascript (that do have exceptions).
|
||||
|
||||
\subsubsection{Tail-calls}
|
||||
|
||||
WASM 1 didn't include the possibility to tail-call functions. This is
|
||||
obviously required for correct compilation of functionnal languages
|
||||
|
||||
\section{Compiling OCaml to WASM}
|
||||
|
||||
\subsection{Targeting WASM 1}
|
||||
|
||||
There have been attempts at targeting the early versions of WASM from OCAML.
|
||||
The first obvious one being just compiling the OCaml runtime (including the GC) and interpreter using emscripten (a C to WASM compiler),
|
||||
and WASICAML a smarter and more efficient version of this approach.
|
||||
|
||||
Both suffer from the same problem as C programs running on WASM: they
|
||||
can't natively manipulate external values, like DOM objects in the
|
||||
browser.
|
||||
|
||||
\subsection{With WASM-GC}
|
||||
|
||||
To properly interract with the embedder (TODO define before), we need to leverage the reference extensions.
|
||||
This requires a completely different compilation strategy.
|
||||
|
||||
\subsubsection{Native OCaml value representation}
|
||||
|
||||
OCaml uses an uniform representation of values known as pointer
|
||||
tagging. One bit is used to indicate if the value is a small scalar or
|
||||
a pointer to a heap allocated block. Granted we are working on $n$
|
||||
bits values, we have to choose one bit that will be the \emph{tag
|
||||
bit}. For instance, if we choose the least significant bit, we start
|
||||
by testing its value:
|
||||
|
||||
\begin{center}
|
||||
\includegraphics[width=10em]{figure_ocaml_bit1.mps}
|
||||
\end{center}
|
||||
|
||||
If $b_{0} = 0$, then the whole value is a pointer:
|
||||
|
||||
\begin{center}
|
||||
\includegraphics[width=20em]{figure_ocaml_bit2.mps}
|
||||
\end{center}
|
||||
|
||||
If $b_{1} = 1$, then the $n - 1$ most significant bits are a small scalar and $b_{0}$ is ignored:
|
||||
|
||||
\begin{center}
|
||||
\includegraphics[width=20em]{figure_ocaml_bit3.mps}
|
||||
\end{center}
|
||||
|
||||
In the second case, we talk about \emph{small scalars} instead of
|
||||
scalars because we can only represents $2^{n - 1}$ values instead of
|
||||
the $2^n$ that are representable when all bits are available. For
|
||||
pointers, we do not lose anything as they need to be \emph{aligned}
|
||||
anyway and the last bit is always zero.
|
||||
|
||||
\begin{tcolorbox}[breakable]
|
||||
\input{layout.ml.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{center}
|
||||
\includegraphics[width=13em]{figure_ocaml_layout.mps}
|
||||
\end{center}
|
||||
|
||||
\subsubsection{OCaml value representation in WASM}
|
||||
|
||||
As in native code we need a uniform representation. We of course can't
|
||||
use integers, as they can't be used as pointers. We need to use a
|
||||
reference type. The most general one would be anyref. But we can be a
|
||||
bit more precise and use eqref. This is the type of all values that
|
||||
can be tested for physical equality. It is a super type of OCaml
|
||||
values. This also allows us to test for equality without requireing an
|
||||
additionnal cast.
|
||||
|
||||
\paragraph{Small scalars}
|
||||
|
||||
All OCaml values that would be represented as integers in the native
|
||||
OCaml are represented as i31ref. This includes the int and char types,
|
||||
but also all constant constructors of sum types.
|
||||
|
||||
\paragraph{Arrays}
|
||||
|
||||
The OCaml array type is directly represented as a WASM array.
|
||||
|
||||
\paragraph{Blocks}
|
||||
|
||||
For other kinds of blocks there are two possible choices. We can
|
||||
either use a struct with a field for the tag and one field per OCaml
|
||||
value field. The other choice is to use arrays of eqref with the tag
|
||||
stored at position 0.
|
||||
|
||||
\paragraph{Block as struct}
|
||||
|
||||
A block of size one would be represented using the type \$block1
|
||||
|
||||
% (type $block1 (struct (field $tag i8) (field $field0 (ref eq))))
|
||||
|
||||
And for size two it would be \$block2
|
||||
|
||||
% (type $block2 (struct (field $tag i8) (field $field0 (ref eq)) (field $field1 (ref eq))))
|
||||
|
||||
We need \$block2 to be a subtype of \$block1. As we are using upstream
|
||||
OCaml as the base for Wasocaml. In the OCaml IRs the primitives for
|
||||
accessing a block field is untyped, thus the when accessing the n-th
|
||||
field of the block the only information is that the block has size at
|
||||
least n+1.
|
||||
|
||||
%% (func snd (param $x (ref eq)) (result (ref eq))
|
||||
%% (struct.get $block2 1 (ref.cast $block2 (local.get $x))))
|
||||
|
||||
OCaml blocks can be arbitrarilly large, and very large ones do appear
|
||||
in practice. In particular modules are compiled as blocks, and tends
|
||||
to be on the larger side. We have seen in the wild some examples
|
||||
containing thousands of fields.
|
||||
|
||||
WASM allows a subtyping chain of length 64, which is far from
|
||||
sufficient for this encoding. But a variant can be devised to
|
||||
circumvent that limitation: It is possible to represent those as trees
|
||||
of structs.
|
||||
|
||||
\paragraph{Block as arrays}
|
||||
|
||||
With the array representation defined as type \$block
|
||||
|
||||
%% (type $block (array (ref eq)))
|
||||
|
||||
accessign the field 1 of the OCaml block amount to accesing the field 2 of the array
|
||||
|
||||
%% (func snd (param $x (ref eq)) (result (ref eq))
|
||||
%% (array.get $block (i32.const 2) (ref.cast $block (local.get $x))))
|
||||
|
||||
and reading the tag is implemented by reading the field 0 and casting to an integer
|
||||
|
||||
%% (func tag (param $x (ref eq)) (result i32)
|
||||
%% (i31.get_u (ref.cast i31ref
|
||||
%% (array.get $block (i32.const 0) (ref.cast $block (local.get $x))))))
|
||||
|
||||
\paragraph{Block representation tradeoff}
|
||||
|
||||
The array representation is simpler, but requires (implicit) bound checks at each
|
||||
field access and a cast to read the tag.
|
||||
|
||||
While the struct representation requires a more complex cast for the
|
||||
WASM runtime (a subtyping test). A compiler propagating more types
|
||||
could use finer WASM type information, providing a precise type to
|
||||
each struct field. This could allowing fewer casts.
|
||||
|
||||
Notice that in practice we could measure an upper bound on the actual
|
||||
runtime cost of cast. The V8 runtime allows to consider cast as noop
|
||||
(only for test purpose). The measured speedup is around 10\%
|
||||
|
||||
\paragraph{Boxed numbers}
|
||||
|
||||
Ocaml boxed numbers are structs containing the number
|
||||
|
||||
%% (type $float (struct (field f64)))
|
||||
%% (type $int32 (struct (field i32)))
|
||||
|
||||
\paragraph{Closures}
|
||||
|
||||
WASM ref func are functions, not closures, hence we need to produce
|
||||
values containing both the function and its environment. The only WASM
|
||||
type construction that can contain both func ref and other values are
|
||||
the structs.
|
||||
|
||||
Hence a closure is a struct containing a func ref and the captured
|
||||
variables
|
||||
|
||||
%% (type $closure1 (struct (field (ref func)) (field $fv1 (ref eq)) (field $fv2 (ref eq))))
|
||||
|
||||
The actual representation is a bit more complex, to reduce casts and
|
||||
handle mutualy recursive functions. This is the only place where we
|
||||
need recursive WASM types.
|
||||
|
||||
\subsubsection{code representation}
|
||||
|
||||
The translation from OCaml expression to WASM is quite
|
||||
straightforward. Most of the work revolves around translating from let
|
||||
bound expressions to a stack based language without producing too
|
||||
naive code. In practice the fine details of the code don't matter much
|
||||
as we can use Binaryen (a quite efficient WASM to WASM optimizer) to
|
||||
clean up dirty code.
|
||||
|
||||
WASM exceptions can be used quite directly to represent OCaml ones.
|
||||
|
||||
\subsubsection{FFI}
|
||||
|
||||
We have plans to provide ways to interract with both standard C
|
||||
libraries using the usual OCaml FFI and Javascript libraries using
|
||||
js\_of\_ocaml FFI.
|
||||
|
||||
\paragraph{C}
|
||||
|
||||
Very recently, some extension to Clang where added that would allow
|
||||
compiling C code with almost no change to the binding. We could
|
||||
provide modified mlvalue.h headers files to use instead of the
|
||||
standard ones replacing the usual macros with hand written WASM
|
||||
functions. The only limitation that we forsee is that the Field macro
|
||||
couldn't be an Lvalue anymore, a new Set\_field macro would be needed
|
||||
instead (as was originaly proposed for OCaml 5)
|
||||
|
||||
\paragraph{js\_of\_ocaml}
|
||||
|
||||
To interract with Javascript code, we would need one more extension
|
||||
(the string ref proposal).
|
||||
|
||||
Almost all external calls in jsoo goes through the
|
||||
Js.Unsafe.meth\_call (of type 'a -> string -> any array -> 'b) function
|
||||
which can be exposed to the WASM module as a function of type
|
||||
|
||||
%% (func (param $obj externref) (param $method stringref) (param $args $anyarray) (result externref))
|
||||
|
||||
This calls a method of name \$method on the object \$obj with the
|
||||
arguments \$args . The javascript side is the one managing all the
|
||||
dynamic typing.
|
||||
|
||||
\section{Expected performances}
|
||||
|
||||
We can't produce yet benchmarks on real sized programs. But
|
||||
preliminary ones are quite convincing. While we of course don't expect
|
||||
to be competitive with the native code compiler, the performance
|
||||
degradation seems to be almost constant (around twice slower).
|
||||
|
||||
Compared to Javascript VM, a WASM compiler is a much simpler beast
|
||||
that can compile ahead of time. There are none of the wild
|
||||
impredictability that browser tend to demonstrate on Javascript. Also
|
||||
various engines are expected to behave quite similarly.
|
||||
|
||||
\section{Future extensions}
|
||||
|
||||
Our compiler is base on OCaml 4.14. So effect handlers where out of
|
||||
the scope. There are three strategies to handle them.
|
||||
|
||||
\paragraph{CPS compilation}
|
||||
|
||||
In an OCaml only program, with a whole program CPS transformation it
|
||||
is possible to represent effect handlers as continuations. This
|
||||
strategy has been proved to be effective by jsoo.
|
||||
|
||||
This is not ideal because this prevents the use of the target language
|
||||
stack and instead stores it in the heap, with a non negligible
|
||||
cost. It can be mitigated by only applying the transformation to the
|
||||
code that can't be proved to not use effect handlers.
|
||||
|
||||
\paragraph{js promise}
|
||||
|
||||
\paragraph{WASM stack switching}
|
||||
|
||||
stack switching/effect handlers
|
||||
|
||||
\section{Related works other compilers}
|
||||
|
||||
\subsection{Dart}
|
||||
\subsection{Scheme}
|
||||
|
||||
\subsection{OCaml}
|
||||
js\_of\_ocaml / wasm\_of\_ocaml
|
||||
|
||||
\section{Current state}
|
||||
|
||||
Our current implementation only provides some part of the OCaml stdlib
|
||||
externals as hand written WASM.
|
||||
|
||||
|
||||
\section{conclusion}
|
||||
|
||||
discuttions i31, subtyping chain, GC proposal ça marche bien pour nous
|
||||
|
||||
\end{document}
|
||||
|
Loading…
x
Reference in New Issue
Block a user