CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Fixes #79

Browse Source
This commit is contained in:
Denis Merigoux 2021-03-19 17:49:56 +01:00
parent 86e7c4ff34
commit e5d4dd21f3
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
5 changed files with 98 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/catala/dcalc/dcalc.mld
View File

@ -1,10 +1,11 @@
{0 Default calculus}
This representation is the fourth in the compilation chain
(see {{: index.html#architecture} Architecture}). Its main difference
with the previous {{: desugared.html} desugared representation} is that scopes
This representation is the fourth in the compilation chain
(see {{: index.html#architecture} Architecture}). Its main difference
with the previous {{: desugared.html} desugared representation} is that scopes
have been lowered into regular functions, and enums and structs have been
lowered to sum and product types.
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:
@ -12,9 +13,8 @@ The module describing the abstract syntax tree is:
Printing helpers can be found in {!module: Dcalc.Print}.
This intermediate representation corresponds to the default calculus
presented in the {{: https://github.com/CatalaLang/catala/raw/master/doc/formalization/formalization.pdf}
Catala formalization}.
This intermediate representation corresponds to the default calculus
presented in the {{: https://arxiv.org/abs/2103.03198} Catala formalization}.
{1 Typing }
@ -34,7 +34,7 @@ Related modules:
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.
semantics of the default calculus.
Later, translations to a regular lambda calculus and/or a simple imperative
Later, translations to a regular lambda calculus and/or a simple imperative
language are bound to be added.

88
src/catala/index.mld
View File

@ -2,63 +2,79 @@
{1 Architecture}
The architecture of the Catala compiler is inspired by
The architecture of the Catala compiler is inspired by
{{: https://compcert.org/} CompCert} or the {{: https://nanopass.org/} Nanopass}
framework, and is structured around many intermediate representations connected
framework, and is structured around many intermediate representations connected
by successive translations passes.
Here is the recap picture of the different intermediate representations of the
Here is the recap picture of the different intermediate representations of the
Catala compiler (made with an {{: https://textik.com/#c1c1fecda5209492} ASCII diagram tool}):
{v
+---------------+
| |
| Surface AST |
| |
+---------------+
|
* Separate code from legislation |
* Remove syntactic sugars |
v
+---------------+
| |
| Desugared AST |
| |
+---------------+
|
* Build rule trees for each definition |
* Order variable computations inside scope |
v
+--------------------+
| |
| Scope language AST |
| |
+--------------------+
|
* Convert scopes into functions |
* Thunking of subscope arguments |
|
v
{v
+---------------+
| |
| Surface AST |
| |
+---------------+
|
|
* Separate code from legislation |
* Remove syntactic sugars |
v
+---------------+
| |
| Desugared AST |
| |
+---------------+
|
|
* Build rule trees for each definition |
* Order variable computations inside scope |
v
+--------------------+
| |
| Scope language AST |
| |
+--------------------+
|
|
* Convert scopes into functions |
* Thunking of subscope arguments |
|
v
+----------------------+
| |
| Default calculus AST |
| |
+----------------------+ v}
+----------------------+
|
|
|
* Compile the default term |
|
v
+----------------------+
| |
| Lambda calculus AST |
| |
+----------------------+
v}
{1 List of top-level modules }
Each of those intermediate representation is bundled into its own `dune` bundle
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 }
{!modules: Surface Desugared Scopelang Dcalc Lcalc }
More documentation can be found on each intermediate representations here.
{ul
{ul
{li {{: surface.html} The surface representation}}
{li {{: desugared.html} The desugared representation}}
{li {{: scopelang.html} The scope language }}
{li {{: dcalc.html} The default calculus}}
{li {{: lcalc.html} The lambda calculus}}
}
The main compilation chain is defined in:

2
src/catala/lcalc/compile_with_exceptions.mli
View File

@ -12,4 +12,6 @@
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Translation from the default calculus to the lambda calculus *)
val translate_program : Dcalc.Ast.program -> Ast.program

32
src/catala/lcalc/lcalc.mld Normal file
View File

@ -0,0 +1,32 @@
{0 Lambda calculus}
This representation is the fifth in the compilation chain
(see {{: index.html#architecture} Architecture}). Its main difference
with the previous {{: Lcalc.html} default calculus} is the absence of the
default term, which has been eliminated through diverse compilation schemes.
The module describing the abstract syntax tree is:
{!modules: Lcalc.Ast}
This intermediate representation corresponds to the lambda calculus
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.
{1 OCaml backend}
Related modules:
{!modules: Lcalc.To_ocaml}
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.

3
src/catala/lcalc/to_ocaml.mli
View File

@ -12,4 +12,7 @@
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Formats a lambda calculus program into a valid OCaml program *)
val format_program : Format.formatter -> Ast.program -> Scopelang.Dependency.TVertex.t list -> unit
(** Usage [format_program fmt p type_dependencies_ordering] *)