From d2977b48ce0ab4526a0eb4e95eb1bfe4c969729a Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Wed, 19 Jan 2022 10:54:16 +0100 Subject: [PATCH] Documentation pass --- compiler/dcalc/ast.mli | 2 ++ compiler/dcalc/dcalc.mld | 33 ++++++++++++++-------- compiler/dcalc/optimizations.mli | 2 ++ compiler/dcalc/print.mli | 2 ++ compiler/desugared/desugared.mld | 8 +++--- compiler/index.mld | 23 ++++++++++++---- compiler/lcalc/lcalc.mld | 14 +++++----- compiler/literate/literate.mld | 8 +++--- compiler/scalc/scalc.mld | 11 ++++---- compiler/scopelang/scopelang.mld | 9 +++--- compiler/surface/surface.mld | 33 +++++++++++----------- compiler/utils/utils.mld | 38 ++++++++++++++------------ compiler/verification/verification.mld | 26 +++++++++++++++--- 13 files changed, 128 insertions(+), 81 deletions(-) diff --git a/compiler/dcalc/ast.mli b/compiler/dcalc/ast.mli index 4300788e..faae0419 100644 --- a/compiler/dcalc/ast.mli +++ b/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 diff --git a/compiler/dcalc/dcalc.mld b/compiler/dcalc/dcalc.mld index 38c73b9f..c639daca 100644 --- a/compiler/dcalc/dcalc.mld +++ b/compiler/dcalc/dcalc.mld @@ -7,34 +7,43 @@ 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 semantics of the default calculus. Later, translations to a regular lambda calculus and/or a simple imperative -language are bound to be added. \ No newline at end of file +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} \ No newline at end of file diff --git a/compiler/dcalc/optimizations.mli b/compiler/dcalc/optimizations.mli index f47cd48e..a5e37ad5 100644 --- a/compiler/dcalc/optimizations.mli +++ b/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 diff --git a/compiler/dcalc/print.mli b/compiler/dcalc/print.mli index 774ca951..232d9465 100644 --- a/compiler/dcalc/print.mli +++ b/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} *) diff --git a/compiler/desugared/desugared.mld b/compiler/desugared/desugared.mld index ddae3282..53460f24 100644 --- a/compiler/desugared/desugared.mld +++ b/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} diff --git a/compiler/index.mld b/compiler/index.mld index 74f49376..bfb2d709 100644 --- a/compiler/index.mld +++ b/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 | - | | - +---------------+ + +------------------+ + | | + | 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: diff --git a/compiler/lcalc/lcalc.mld b/compiler/lcalc/lcalc.mld index 2884a307..9f1b5b13 100644 --- a/compiler/lcalc/lcalc.mld +++ b/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. - diff --git a/compiler/literate/literate.mld b/compiler/literate/literate.mld index f76aff78..7a7dbf8e 100644 --- a/compiler/literate/literate.mld +++ b/compiler/literate/literate.mld @@ -1,9 +1,9 @@ {0 Literate programming} +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} - -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. \ No newline at end of file diff --git a/compiler/scalc/scalc.mld b/compiler/scalc/scalc.mld index 728c0003..11f6d944 100644 --- a/compiler/scalc/scalc.mld +++ b/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: diff --git a/compiler/scopelang/scopelang.mld b/compiler/scopelang/scopelang.mld index b1e255c6..72840a26 100644 --- a/compiler/scopelang/scopelang.mld +++ b/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} diff --git a/compiler/surface/surface.mld b/compiler/surface/surface.mld index b9b03271..b704bad1 100644 --- a/compiler/surface/surface.mld +++ b/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,22 +31,23 @@ 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. +to perform its parsing. -{!module: Surface.Parser} is the main file where the parser tokens and the -grammar is declared. It is automatically translated into its parsing automata +{!module: Surface.Parser} is the main file where the parser tokens and the +grammar is declared. It is automatically translated into its parsing automata equivalent by Menhir. -In order to provide decent syntax error messages, the Catala compiler uses the -novel error handling provided by Menhir and detailed in Section 11 of the -{{: http://cambium.inria.fr/~fpottier/menhir/manual.pdf} Menhir manual}. +In order to provide decent syntax error messages, the Catala compiler uses the +novel error handling provided by Menhir and detailed in Section 11 of the +{{: http://cambium.inria.fr/~fpottier/menhir/manual.pdf} Menhir manual}. A [parser.messages] source file has been manually annotated with custom error message for every potential erroneous state of the parser, and Menhir @@ -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} diff --git a/compiler/utils/utils.mld b/compiler/utils/utils.mld index ba7a92a1..70c6bede 100644 --- a/compiler/utils/utils.mld +++ b/compiler/utils/utils.mld @@ -2,37 +2,39 @@ {1 Unique identifiers} +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 +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. + 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 -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} +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. + Related modules: {!modules: Utils.Pos} -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} + +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 +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} - -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 -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} \ No newline at end of file diff --git a/compiler/verification/verification.mld b/compiler/verification/verification.mld index d8fcfe89..e1c6a094 100644 --- a/compiler/verification/verification.mld +++ b/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} \ No newline at end of file +Related modules: + +{!modules: Verification.Z3backend} \ No newline at end of file