Documentation pass

compiler/dcalc/ast.mli

@@ -12,6 +12,8 @@
    or implied. See the License for the specific language governing permissions and limitations under
    the License. *)
 
+(** Abstract syntax tree of the default calculus intermediate representation *)
+
 open Utils
 
 module ScopeName : Uid.Id with type info = Uid.MarkedString.info

compiler/dcalc/dcalc.mld

@@ -7,30 +7,26 @@ have been lowered into regular functions, and enums and structs have been
 lowered to sum and product types. The default calculus can be later compiled
 to a {{: lcalc.html} lambda calculus}.
 
-The module describing the abstract syntax tree is:
-
-{!modules: Dcalc.Ast}
-
+The module describing the abstract syntax tree is {!module: Dcalc.Ast}.
 Printing helpers can be found in {!module: Dcalc.Print}.
-
 This intermediate representation corresponds to the default calculus
 presented in the {{: https://arxiv.org/abs/2103.03198} Catala formalization}.
 
-{1 Typing }
-
 Related modules:
 
-{!modules: Dcalc.Typing}
+{!modules: Dcalc.Ast}
+
+{1 Typing }
 
 This representation is where the typing is performed. Indeed, {!module: Dcalc.Typing}
 implements the classical {{: https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system} W algorithm}
 corresponding to a Hindley-Milner type system, without type constraints.
 
-{1 Interpreter}
-
 Related modules:
 
-{!modules: Dcalc.Interpreter}
+{!modules: Dcalc.Typing}
+
+{1 Interpreter}
 
 Since this representation is currently the last of the compilation chain,
 an {!module: Dcalc.Interpreter} module is provided to match the execution
@@ -38,3 +34,16 @@ semantics of the default calculus.
 
 Later, translations to a regular lambda calculus and/or a simple imperative
 language are bound to be added.
+
+Related modules:
+
+{!modules: Dcalc.Interpreter}
+
+{1 Optimizations}
+
+Classical optimizations passes can be performed on the Dcalc AST: partial
+evaluation, beta and iota-reduction, etc.
+
+Related modules:
+
+{!modules: Dcalc.Optimizations}

compiler/dcalc/optimizations.mli

@@ -12,6 +12,8 @@
    or implied. See the License for the specific language governing permissions and limitations under
    the License. *)
 
+(** Optimization passes for default calculus programs and expressions *)
+
 open Utils
 open Ast
 

compiler/dcalc/print.mli

@@ -12,6 +12,8 @@
    or implied. See the License for the specific language governing permissions and limitations under
    the License. *)
 
+(** Printing functions for the default calculus AST *)
+
 open Utils
 
 (** {1 Helpers} *)

compiler/desugared/desugared.mld

@@ -12,10 +12,6 @@ The module describing the abstract syntax tree is:
 
 {1 Translation to the scope language}
 
-Related modules:
-
-{!modules: Desugared.Dependency Desugared.Desugared_to_scope}
-
 Before the translation to the {{: scopelang.html} scope language},
 {!module: Desugared.Dependency} checks that within
 a scope, there is no computational circular dependency between the variables
@@ -28,3 +24,7 @@ computation order. All the graph computations are done using the
 The other important piece of work performed by
 {!module: Desugared.Desugared_to_scope} is the construction of the default trees
 (see {!Dcalc.Ast.EDefault}) from the list of prioritized rules.
+
+Related modules:
+
+{!modules: Desugared.Dependency Desugared.Desugared_to_scope}

compiler/index.mld

@@ -21,11 +21,11 @@ Catala compiler (made with an {{: https://textik.com/#c1c1fecda5209492} ASCII di
          * Separate code from legislation    |
          * Remove syntactic sugars           |
                                              v
-                                     +---------------+
+                                   +------------------+
                                    |                  |
                                    |  Desugared AST   |
                                    |                  |
-                                     +---------------+
+                                   +------------------+
                                              |
                                              |
  * Build rule trees for each definition      |
@@ -58,6 +58,16 @@ Catala compiler (made with an {{: https://textik.com/#c1c1fecda5209492} ASCII di
                                  | Lambda calculus AST  |
                                  |                      |
                                  +----------------------+
+                                             |
+                                             |
+        * Turn expressions into statements   |
+                                             |
+                                             v
+                               +--------------------------+
+                               |                          |
+                               |  Statement calculus AST  |
+                               |                          |
+                               +--------------------------+
 v}
 
 {1 List of top-level modules }
@@ -65,7 +75,7 @@ v}
 Each of those intermediate representation is bundled into its own `dune` bundle
 module. Click on the items below if you want to dive straight into the signatures.
 
-{!modules: Surface Desugared Scopelang Dcalc Lcalc }
+{!modules: Surface Desugared Scopelang Dcalc Lcalc Scalc }
 
 More documentation can be found on each intermediate representations here.
 
@@ -75,6 +85,7 @@ More documentation can be found on each intermediate representations here.
 {li {{: scopelang.html} The scope language }}
 {li {{: dcalc.html} The default calculus}}
 {li {{: lcalc.html} The lambda calculus}}
+{li {{: scalc} The statement calculus}}
 }
 
 The main compilation chain is defined in:

compiler/lcalc/lcalc.mld

@@ -14,20 +14,20 @@ presented in the {{: https://arxiv.org/abs/2103.03198} Catala formalization}.
 
 {1 Compilation from default calculus }
 
-Related modules:
-
-{!modules: Lcalc.Compile_with_exceptions}
-
 {!module: Lcalc.Compile_with_exceptions} compiles the default term of the
 default calculus using catchable exceptions. This compilation scheme has been
 certified.
 
+Related modules:
+
+{!modules: Lcalc.Compile_with_exceptions}
+
 {1 Backends}
 
+The OCaml backend of the lambda calculus is merely a syntactic formatting,
+since the core of the OCaml value language is effectively a lambda calculus.
+
 Related modules:
 
 {!modules: Lcalc.To_ocaml Scalc.To_python Lcalc.Backends}
 
-The OCaml backend of the lambda calculus is merely a syntactic formatting,
-since the core of the OCaml value language is effectively a lambda calculus.
-

compiler/literate/literate.mld

@@ -1,9 +1,9 @@
 {0 Literate programming}
 
-Related modules:
-
-{!modules: Literate.Html Literate.Latex}
-
 These module take the {{:surface.html} surface representation} of the Catala
 program and process it into different literate programming outputs, like
 an HTML page or a LaTeX document.
+
+Related modules:
+
+{!modules: Literate.Html Literate.Latex}

compiler/scalc/scalc.mld

@@ -8,19 +8,18 @@ rules in the language, every local variable has a unique id.
 
 The module describing the abstract syntax tree is:
 
-{!modules: Dcalc.Ast}
-
+{!modules: Scalc.Ast}
 
 {1 Compilation from lambda calculus }
 
-Related modules:
-
-{!modules: Scalc.Compile_from_lambda}
-
 {!module: Scalc.Compile_from_lambda} Performs the classical translation
 from an expression-based language to a statement-based language. Union types
 are eliminated in favor of tagged unions.
 
+Related modules:
+
+{!modules: Scalc.Compile_from_lambda}
+
 {1 Backends}
 
 Related modules:

compiler/scopelang/scopelang.mld

@@ -19,10 +19,6 @@ Catala formalization}.
 
 {1 Translation to the default calculus}
 
-Related modules:
-
-{!modules: Scopelang.Dependency Scopelang.Scope_to_dcalc}
-
 The translation from the scope language to the
 {{: dcalc.html} default calculus} involves three big features:
 
@@ -36,3 +32,8 @@ The translation from the scope language to the
 enums on one hand, and the inter-scope dependencies on the other hand. Both
 can be found in {!module: Scopelang.Dependency}, while
 {!module: Scopelang.Scope_to_dcalc} is mostly responsible for 2.
+
+
+Related modules:
+
+{!modules: Scopelang.Dependency Scopelang.Scope_to_dcalc}

compiler/surface/surface.mld

@@ -13,10 +13,6 @@ using the {{:literate.html} literate programming modules}.
 
 {1 Lexing }
 
-Relevant modules:
-
-{!modules: Surface.Lexer_common Surface.Lexer_fr Surface.Lexer_en}
-
 The lexing in the Catala compiler is done using
 {{: https://github.com/ocaml-community/sedlex} sedlex}, the modern OCaml lexer
 that offers full support for UTF-8. This support enables users of non-English
@@ -35,11 +31,12 @@ produce the parser tokens.
     with verbose French keywords matching legal concepts.}
 }
 
-{1 Parsing }
-
 Relevant modules:
 
-{!modules: Surface.Parser Surface.Parser_driver Surface.Parser_errors}
+{!modules: Surface.Lexer_common Surface.Lexer_fr Surface.Lexer_en}
+
+
+{1 Parsing }
 
 The Catala compiler uses {{: http://cambium.inria.fr/~fpottier/menhir/} Menhir}
 to perform its parsing.
@@ -61,11 +58,11 @@ To wrap it up, {!module: Surface.Parser_driver} glues all the parsing and
 lexing together to perform the translation from source code to abstract syntax
 tree, with meaningful error messages.
 
-{1 Name resolution and translation }
-
 Relevant modules:
 
-{!modules: Surface.Name_resolution Surface.Desugaring}
+{!modules: Surface.Parser Surface.Parser_driver Surface.Parser_errors}
+
+{1 Name resolution and translation }
 
 The desugaring consists of translating {!module: Surface.Ast} to
 {!module: Desugared.Ast} of the {{: desugared.html} desugared representation}.
@@ -75,3 +72,7 @@ name resolution: {!module: Surface.Name_resolution}. Indeed, in
 {!module: Surface.Ast}, the variables identifiers are just [string], whereas in
 {!module: Desugared.Ast} they have been turned into well-categorized types
 with an unique identifier like {!type: Scopelang.Ast.ScopeName.t}.
+
+Relevant modules:
+
+{!modules: Surface.Name_resolution Surface.Desugaring}

compiler/utils/utils.mld

@@ -2,10 +2,6 @@
 
 {1 Unique identifiers}
 
-Related modules:
-
-{!modules: Utils.Uid}
-
 In {{: desugared.html} the desugared representation} or in the
 {{: scopelang.html} the scope language}, a number of things are named using
 global identifiers. These identifiers use OCaml's type system to statically
@@ -14,21 +10,23 @@ distinguish e.g. a scope identifier from a struct identifier.
 The {!module: Utils.Uid} module provides a generative functor whose output is
 a fresh sort of global identifiers.
 
-{1 Source code positions}
-
 Related modules:
 
-{!modules: Utils.Pos}
+{!modules: Utils.Uid}
+
+{1 Source code positions}
 
 This module is used throughout the compiler to annotate the abstract syntax
 trees with information about the position of the element in the original source
 code. These annotations are critical to produce readable error messages.
 
-{1 Error messages}
-
 Related modules:
 
-{!modules: Utils.Errors}
+{!modules: Utils.Pos}
+
+
+{1 Error messages}
+
 
 Error handling is critical in a compiler. The Catala compiler uses an architecture
 of error messages inspired by the Rust compiler, where error messages all
@@ -36,3 +34,7 @@ correspond to the same exception. This exception carries messages and positions
 that are displayed in the end in a nicely-formatted error message.
 
 Hence, all error thrown by the compiler should use {!module: Utils.Errors}
+
+Related modules:
+
+{!modules: Utils.Errors}

compiler/verification/verification.mld

@@ -3,21 +3,39 @@
 {1 Generating verification conditions }
 
 From the {{: dcalc.html} Dcalc} intermediate representation, the module
-{!module: Conditions} provides functions to generate
+{!module: Verification.Conditions} provides functions to generate
 verification conditions for each scope definition present in the program.
 These verification conditions, if proven true, can assert the well-behaved
 execution of the scope definition: absence of empty or conflict errors.
 
 Related modules:
 
-{!modules: Conditions}
+{!modules: Verification.Conditions}
+
+{1 Generic solver}
+
+As Catala ambitions to mix and match different proof backends to solve the
+verification conditions, the compiler features a functorial interface
+common to all backends to rationalize the inputs and outputs. More precisely,
+it is sufficient for a proof backend to implement {!module-type: Verification.Io.Backend}
+to enjoy the normalized input/output (I/O) of {!module-type: Verification.Io.BackendIO}
+through the functor {!module: Verification.Io.MakeBackendIO}.
+
+Finally, the {!module: Verification.Solver} calls the I/O functions of the different
+backends to perform the solving of the various verification conditions.
+
+Related modules
+
+{!modules: Verification.Io Verification.Solver}
 
 {1 Z3 proof backend}
 
-One of the way to prove the {Conditions.verification_condition}s
+One of the way to prove the {!type: Verification.Conditions.verification_condition}s
 true is to encode them into a Z3 query. The Catala compiler features a
 complete encoding of the {{: dcalc.html} Dcalc} intermediate representation
 into Z3, which can be used to launch Z3 queries and collect results to
 inform potential Dcalc program optimizations.
 
-{!modules: Z3encoding}
+Related modules:
+
+{!modules: Verification.Z3backend}