lambda form
This commit is contained in:
parent
d3664f6e31
commit
48f004b0ae
2 changed files with 83 additions and 15 deletions
BIN
tesi/tesi.pdf
BIN
tesi/tesi.pdf
Binary file not shown.
|
@ -1,10 +1,9 @@
|
||||||
\begin{comment}
|
\begin{comment}
|
||||||
* TODO Scaletta [1/5]
|
* TODO Scaletta [1/6]
|
||||||
- [X] Introduction
|
- [X] Introduction
|
||||||
- [-] Background [40%]
|
- [-] Background [60%]
|
||||||
- [ ] Lambda code [0%]
|
- [X] Low level representation
|
||||||
- [ ] Compiler optimizations
|
- [X] Lambda code [0%]
|
||||||
- [ ] other instructions
|
|
||||||
- [X] Pattern matching
|
- [X] Pattern matching
|
||||||
- [ ] Symbolic execution
|
- [ ] Symbolic execution
|
||||||
- [ ] Translation Validation
|
- [ ] Translation Validation
|
||||||
|
@ -320,8 +319,7 @@ set to 0.
|
||||||
https://dev.realworld.org/compiler-backend.html
|
https://dev.realworld.org/compiler-backend.html
|
||||||
CITE: realworldocaml
|
CITE: realworldocaml
|
||||||
\end{comment}
|
\end{comment}
|
||||||
*** Lambda form types
|
A Lambda code target file is produced by the compiler and consists of a
|
||||||
A Lambda form target file produced by the compiler consists of a
|
|
||||||
single s-expression. Every s-expression consist of /(/, a sequence of
|
single s-expression. Every s-expression consist of /(/, a sequence of
|
||||||
elements separated by a whitespace and a closing /)/.
|
elements separated by a whitespace and a closing /)/.
|
||||||
Elements of s-expressions are:
|
Elements of s-expressions are:
|
||||||
|
@ -330,7 +328,72 @@ Elements of s-expressions are:
|
||||||
- Strings: enclosed in double quotes and possibly escaped
|
- Strings: enclosed in double quotes and possibly escaped
|
||||||
- S-expressions: allowing arbitrary nesting
|
- S-expressions: allowing arbitrary nesting
|
||||||
|
|
||||||
There are several numeric types:
|
The Lambda form is a key stage where the compiler discards type
|
||||||
|
informations and maps the original source code to the runtime memory
|
||||||
|
model described.
|
||||||
|
In this stage of the compiler pipeline pattern match statements are
|
||||||
|
analyzed and compiled into an automata.
|
||||||
|
\begin{comment}
|
||||||
|
evidenzia centralita` rispetto alla tesi
|
||||||
|
\end{comment}
|
||||||
|
#+BEGIN_SRC
|
||||||
|
type t = | Foo | Bar | Baz | Fred
|
||||||
|
|
||||||
|
let test = function
|
||||||
|
| Foo -> "foo"
|
||||||
|
| Bar -> "bar"
|
||||||
|
| Baz -> "baz"
|
||||||
|
| Fred -> "fred"
|
||||||
|
#+END_SRC
|
||||||
|
The Lambda output for this code can be obtained by running the
|
||||||
|
compiler with the /-dlambda/ flag:
|
||||||
|
#+BEGIN_SRC
|
||||||
|
(setglobal Prova!
|
||||||
|
(let
|
||||||
|
(test/85 =
|
||||||
|
(function param/86
|
||||||
|
(switch* param/86
|
||||||
|
case int 0: "foo"
|
||||||
|
case int 1: "bar"
|
||||||
|
case int 2: "baz"
|
||||||
|
case int 3: "fred")))
|
||||||
|
(makeblock 0 test/85)))
|
||||||
|
#+END_SRC
|
||||||
|
As outlined by the example, the /makeblock/ directive is responsible
|
||||||
|
for allocating low level OCaml values and every constant constructor
|
||||||
|
ot the algebraic type /t/ is stored in memory as an integer.
|
||||||
|
The /setglobal/ directives declares a new binding in the global scope:
|
||||||
|
Every concept of modules is lost at this stage of compilation.
|
||||||
|
The pattern matching compiler uses a jump table to map every pattern
|
||||||
|
matching clauses to its target expression. Values are addressed by a
|
||||||
|
unique name.
|
||||||
|
#+BEGIN_SRC
|
||||||
|
type t = | English of p | French of q
|
||||||
|
type p = | Foo | Bar
|
||||||
|
type q = | Tata| Titi
|
||||||
|
type t = | English of p | French of q
|
||||||
|
|
||||||
|
let test = function
|
||||||
|
| English Foo -> "foo"
|
||||||
|
| English Bar -> "bar"
|
||||||
|
| French Tata -> "baz"
|
||||||
|
| French Titi -> "fred"
|
||||||
|
#+END_SRC
|
||||||
|
In the case of types with a smaller number of variants, the pattern
|
||||||
|
matching compiler may avoid the overhead of computing a jump table.
|
||||||
|
This example also highlights the fact that non constant constructor
|
||||||
|
are mapped to cons cell that are accessed using the /tag/ directive.
|
||||||
|
#+BEGIN_SRC
|
||||||
|
(setglobal Prova!
|
||||||
|
(let
|
||||||
|
(test/89 =
|
||||||
|
(function param/90
|
||||||
|
(switch* param/90
|
||||||
|
case tag 0: (if (!= (field 0 param/90) 0) "bar" "foo")
|
||||||
|
case tag 1: (if (!= (field 0 param/90) 0) "fred" "baz"))))
|
||||||
|
(makeblock 0 test/89)))
|
||||||
|
#+END_SRC
|
||||||
|
In the Lambda language are several numeric types:
|
||||||
- integers: that us either 31 or 63 bit two's complement arithmetic
|
- integers: that us either 31 or 63 bit two's complement arithmetic
|
||||||
depending on system word size, and also wrapping on overflow
|
depending on system word size, and also wrapping on overflow
|
||||||
- 32 bit and 64 bit integers: that use 32-bit and 64-bit two's complement arithmetic
|
- 32 bit and 64 bit integers: that use 32-bit and 64-bit two's complement arithmetic
|
||||||
|
@ -352,15 +415,20 @@ bindings in scope: (lambda (arg1 arg2 arg3) BODY)
|
||||||
and are applied using the following syntax: (apply FUNC ARG ARG ARG)
|
and are applied using the following syntax: (apply FUNC ARG ARG ARG)
|
||||||
Evaluation is eager.
|
Evaluation is eager.
|
||||||
|
|
||||||
begin{comment}
|
*** Other atoms
|
||||||
*** Bindings
|
The atom /let/ introduces a sequence of bindings at a smaller scope
|
||||||
The atom /let/ introduces a sequence of bindings:
|
than the global one:
|
||||||
(let BINDING BINDING BINDING ... BODY)
|
(let BINDING BINDING BINDING ... BODY)
|
||||||
|
|
||||||
*** Other atoms
|
The Lambda form supports many other directives such as /strinswitch/
|
||||||
TODO: if, switch, stringswitch...
|
that is constructs aspecialized jump tables for string, integer range
|
||||||
TODO: magari esempi
|
comparisons and so on.
|
||||||
end{comment}
|
These construct are explicitely undocumented because the Lambda code
|
||||||
|
intermediate language can change across compiler releases.
|
||||||
|
\begin{comment}
|
||||||
|
Spiega che la sintassi che supporti e` quella nella BNF
|
||||||
|
\end{comment}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
** Pattern matching
|
** Pattern matching
|
||||||
|
|
Loading…
Reference in a new issue