ocaml runtime values

tesi/files/ocamlcompilation

@@ -0,0 +1 @@
+<mxfile host="app.diagrams.net" modified="2020-03-29T20:12:08.312Z" agent="5.0 (X11)" etag="fcHPT_k2mPux3BFoY6VV" version="12.9.4" type="device"><diagram id="ABCdpev2R_g67oYsKgJW" name="Page-1">7VrbctowEP0aHtuxfIM8cjGBSbgMuNPSl47BCrgRFjUi4Hx9pVjGWDIxSTGQ0BeQVvc9R7taySWtPt/cBs5i1sEuRCVVcTclrVFSVaCrCv1jkjCSVACIBNPAc3mlRDD0niEX8nbTlefCZaoiwRgRb5EWTrDvwwlJyZwgwOt0tQeM0qMunCmUBMOJg2Tpd88lM74KQ0nkLehNZ/HIQOElcyeuzAXLmePi9Y5Is0paPcCYRKn5pg4RU16sl6hdc0/pdmIB9MkhDR6NWiP8Y4SkZQx/9Z/HzrJf/aJGvTw5aMUX3K8Ohu3uLZ8zCWNFBHjlu5D1BUpabT3zCBwunAkrXVPoqWxG5ogXP2CfNJ25hxjqLYieIPEmDi8Y8k75Cp5gQOBm76LAVlWUYxDPIQlCWoU30DSu3XCr/yi/TsACOpfNdoAqc5nD+THddp2okCa4Ft+gUU3SqKRK6LtVRk2amyBnufQmB2oPbjzyg8qUrwbPjXgTlm4wnShxJuSZaHToSjQXVExniFfBBOaRRYZiR9VGhqZjWQCRQ7yn9DSy1M9H6GOPTjBBupxGWtcFBKPp81a7+0DoSFfSHaliR8QJppBIHb2wYbvs9xNEL5IgPp3bDkNYdhSzgmUSjrzk3k6SSDmXShIRW+O9HFHT/Wg3p+WIIXGEb07m6FwoEYYaUJKmyJIE+BHWMcIBlfjYh4w3HkKCyEHe1Gc8o0BDKq8xc0zJhKq8YO65Lhsm0+QnTkF5jZZHMPQisqZs5ysZvFKLMvNmxi42EQNhTBNTlrBHfYtWqbes+t2LR+XlQVwhltAJjBNZIX73GK5W32M3d12tmoGBWRQG5XwM7qudWqNKKzV7gw4Do9fpt++rdrvX/Wx4aBlb4rR43OTjURvZVr3XsLZQWIOPjoMq+Aq9cm4c4jPwa0A0tzuj17fbnfbPjw+EboJLAwLkA7GzI9pd2xr0B5b98bEQN4WpnB0LOdSVvUW7e8d0r1S7DfY7HFqd2icwUbp5cWhcWphcfOSUG17zI2VuhFXOxvpEYXhlz6njzSGWcHOjAaGjgkMsIMdYrzGQh0v/EoSDI1HpUoLro93A6GKUVjT0WcHbsYzP1aCoVvace0+FYlb4dzQXcv6LNKB8CpqYgp03tBPTpPL/pLEnUM+n4FktFRBiiLLoJg6lIBCeDkzx8adoCmZdjFw5BePTXj4H1bNyUHByhkidg72laAZPfOaJh9vh4DefhAsanrJA15YIeQVPCiANiZoRFZsZ1CrsTUGVr4tsjpAdwKt89REg0lQZIsM4JUTyvUVv/Jt9eKIqVM9weYUgGcJDhJHxEHHafSQ/sddCAq/05RTc5MOT9YXMO+Ch2eR7pshzJV+FadZf</diagram></mxfile>

tesi/tesi_unicode.org

@@ -20,7 +20,8 @@
   - [ ] Statement of correctness
   - [ ] Proof of correctness
   - [ ] Practical results 
-TODO: talk about compiler stuff
+
+Magari prima pattern matching poi compilatore?
   
 \end{comment}
 
@@ -253,35 +254,72 @@ inheritance, subtyping and dynamic binding, and modules, that
 provide a way to encapsulate definitions. Modules are checked
 statically and can be reifycated through functors.
 
-** Lambda form compilation
-\begin{comment}
-https://dev.realworld.org/compiler-backend.html
-\end{comment}
+** Compiling OCaml code
 
- provides compilation in form of a bytecode executable with an
-optionally embeddable interpreter and a native executable that could
+The OCaml compiler provides compilation of source files in form of a bytecode executable with an
+optionally embeddable interpreter or as a native executable that could
 be statically linked to provide a single file executable.
-
+Every source file is treated as a separate /compilation unit/ that is
+advanced through different states.
+The first stage of compilation is the parsing of the input code that
+is trasformed into an untyped syntax tree. Code with syntax errors is
+rejected at this stage.
+After that the AST is processed by the type checker that performs
+three steps at once:
+- type inference, using the classical /Algorithm W/
+- perform subtyping and gathers type information from the module system
+- ensures that the code obeys the rule of the OCaml type system
+At this stage, incorrectly typed code is rejected. In case of success,
+the untyped AST in trasformed into a /Typed Tree/.
 After the  typechecker has proven that the program is type safe,
 the  compiler lower the code to /Lambda/, an s-expression based
 language that assumes that its input has already been proved safe.
-On the /Lambda/ representation of the source program, the compiler
-performs a series of optimization passes before translating the
-lambda form to assembly code.
+After the  Lambda pass, the Lambda code is either translated into
+bytecode or goes through a series of optimization steps performed by
+the /Flambda/ optimizer before being translated into assembly.
+\begin{comment}
+TODO: Talk about flambda passes?
+\end{comment}
 
-***  OCaml Native Datatypes
-
-Most native data types in , such as integers, tuples, lists,
-records, can be seen as instances of the following definition
+This is an overview of the different compiler steps.
+[[./files/ocamlcompilation.png]]
 
+** Memory representation of OCaml values
+An usual OCaml source program contains few to none explicit type
+signatures.
+This is possible because of type inference that allows to annotate the
+AST with type informations. However, since the OCaml typechecker guarantes that a program is well typed
+before being transformed into Lambda code, values at runtime contains
+only a minimal subset of type informations needed to distinguish
+polymorphic values.
+For runtime values, OCaml uses a uniform memory representation in
+which every variable is stored as a value in a contiguous block of
+memory.
+Every value is a single word that is either a concrete integer or a
+pointer to another block of memory, that is called /cell/ or /box/.
+We can abstract the type of OCaml runtime values as the following:
 #+BEGIN_SRC 
-type t = Nil | One of int | Cons of int * t 
+type t = Constant | Cell of int * t 
 #+END_SRC
-that is a type /t/ with three constructors that define its complete
-signature.
-Every constructor has an arity. Nil, a constructor of arity 0, is
-called a constant constructor. 
+where a one bit tag is used to distinguish between Constant or Cell.
+In particular this bit of metadata is stored as the lowest bit of a
+memory block.
 
+Given that all the OCaml target architectures guarantee that all
+pointers are divisible by four and that means that two lowest bits are
+always 00 storing this bit of metadata at the lowest bit allows an
+optimization. Constant values in OCaml, such as integers, empty lists,
+Unit values and constructors of arity zero (/constant/ constructors)
+are unboxed at runtime while pointers are recognized by the lowest bit
+set to 0.
+
+
+
+** Lambda form compilation
+\begin{comment}
+https://dev.realworld.org/compiler-backend.html
+CITE: realworldocaml
+\end{comment}
 *** Lambda form types
 A Lambda form target file produced by the  compiler consists of a
 single s-expression. Every s-expression consist of /(/, a sequence of