CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 00:15:39 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into alain_default-option

Browse Source
This commit is contained in:
Denis Merigoux 2022-02-04 15:35:52 +01:00
commit 97f8875a39
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
299 changed files with 13982 additions and 12331 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
.gitattributes vendored
View File

@ -1,6 +1,10 @@
*.catala* linguist-language=Markdown
french_law/js/french_law.js binary
french_law/ocaml/law_source/allocations_familiales.ml binary
french_law/ocaml/law_source/unit_tests/tests_allocations_famiales.ml binary
french_law/python/src/allocations_familiales.py binary
compiler/surface/lexer*.cppo.ml text encoding=latin-1
*.ml linguist-language=OCaml
*.fst linguist-language=Fstar
*.mld linguist-documentation
*.md linguist-documentation
*.hints linguist-generated
french_law/js/french_law.js binary linguist-generated
french_law/ocaml/law_source/allocations_familiales.ml binary linguist-generated
french_law/ocaml/law_source/unit_tests/tests_allocations_famiales.ml binary linguist-generated
french_law/python/src/allocations_familiales.py binary linguist-generated

78
.github/workflows/build.yml vendored
View File

@ -1,78 +0,0 @@
# This is a basic workflow to help you get started with Actions
name: CI
# Controls when the action will run. Triggers the workflow on push or pull request
# events but only for the master branch
on:
push:
branches: [master]
pull_request:
branches: [master]
# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
build-nix-21-05:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2.3.4
- uses: cachix/install-nix-action@v14.1
with:
nix_path: nixpkgs=channel:nixos-21.05
- run: nix-build release.nix
- run: nix-shell --run "echo OK"
build-nix-unstable:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2.3.4
- uses: cachix/install-nix-action@v14.1
with:
nix_path: nixpkgs=channel:nixos-unstable
- run: nix-build release.nix
- run: nix-shell --run "echo OK"
build:
# The type of runner that the job will run on
runs-on: ubuntu-latest
# Steps represent a sequence of tasks that will be executed as part of the job
steps:
# Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
- uses: actions/checkout@v2
- name: Opam modules cache
uses: actions/cache@v1
env:
cache-name: cache-opam-modules
with:
# OCaml cache files are stored in `~/.opam` on Linux/macOS
path: ~/.opam
key: ${{ runner.os }}-build-${{ env.cache-name }}-${{ hashFiles('catala.opam', 'Makefile') }}
restore-keys: |
${{ runner.os }}-build-${{ env.cache-name }}-
${{ runner.os }}-build-
${{ runner.os }}-
- name: Set up OCaml
uses: avsm/setup-ocaml@v1
with:
# Version of the OCaml compiler to initialise
ocaml-version: 4.11.2
- name: Install dependencies
run: |
eval $(opam env)
make dependencies
sudo apt update
sudo apt install python3-dev python3-setuptools python3-pygments man2html rsync colordiff libmpc-dev
sudo python3 -m pip install --upgrade pip
sudo python3 -m pip install virtualenv
sudo make pygments
./french_law/python/setup_env.sh
- name: Make all
run: |
eval $(opam env)
export OCAMLRUNPARAM=b
make all

56
.github/workflows/run-builds.yml vendored Normal file
View File

@ -0,0 +1,56 @@
name: Builds
on:
push:
branches: [master]
workflow_dispatch:
jobs:
build-ubuntu:
runs-on: ubuntu-latest
steps:
- name: Checkout code
uses: actions/checkout@v2
- name: Set up OCaml
uses: avsm/setup-ocaml@v2
with:
ocaml-compiler: 4.11.x
dune-cache: true
- name: Install external dependencies
run: |
sudo apt-get update && sudo apt-get install python3-dev virtualenv python3-setuptools python3-pip python3-pygments man2html rsync colordiff npm nodejs libmpc-dev
sudo python3 -m pip install --upgrade pip
sudo python3 -m pip install virtualenv
sudo make pygments
./french_law/python/setup_env.sh
- name: Install OCaml dependencies
run: |
opam install . --deps-only --with-doc --with-test
- name: Make build
run: |
OCAMLRUNPARAM=b opam exec -- make build
build-nix-21-05:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2.3.4
- uses: cachix/install-nix-action@v14.1
with:
nix_path: nixpkgs=channel:nixos-21.05
- run: nix-shell -p nix-info --run "nix-info -m"
- run: nix-build release.nix
- run: nix-shell --run "echo OK"
build-nix-unstable:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2.3.4
- uses: cachix/install-nix-action@v14.1
with:
nix_path: nixpkgs=channel:nixos-unstable
- run: nix-shell -p nix-info --run "nix-info -m"
- run: nix-build release.nix
- run: nix-shell --run "echo OK"

22
.github/workflows/run-make-all.yml vendored Normal file
View File

@ -0,0 +1,22 @@
name: Harness
on:
push:
branches: [master]
pull_request:
# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
run-make-all:
# The type of runner that the job will run on
runs-on: self-hosted
# Steps represent a sequence of tasks that will be executed as part of the job
steps:
- name: Checkout code
uses: actions/checkout@v2
with:
clean: false
- name: Make all
run: |
OCAMLRUNPARAM=b opam exec -- make all -B

2
.nix/no-web.patch
View File

@ -16,7 +16,7 @@ index 31d5289..0000000
- (Contents (Js.to_string contents))
- false false false false "Interpret"
- (Some (Js.to_string language))
- None trace false
- None trace false false
- (Some (Js.to_string scope))
- None
- end)

9
CITATION.cff
View File

@ -21,6 +21,15 @@ authors:
- given-names: Emile
family-names: Rolley
affiliation: Université Paris-Diderot
- given-names: Louis
family-names: Gesbert
affiliation: OCamlPro
- given-names: Aymeric
family-names: Fromherz
affiliation: Inria
- given-names: Alain
family-names: Delaët-Tixeuil
affiliation: Inria/ENS Lyon
repository-code: 'https://github.com/CatalaLang/catala'
url: 'https://catala-lang.org/'
abstract: >-

14
INSTALL.md
View File

@ -58,21 +58,21 @@ git submodules, with
This should ensure everything is set up for developing on the Catala compiler!
Other features for generation of files and literate programming also require
the following executables to be present
Other features of the Catala repository also require the following executables
to be present
man2html virtualenv python3 rsync colordiff pygmentize
man2html virtualenv python3 pip rsync colordiff pygmentize nodejs npm
please install them if they're not here. On a Debian distribution, this can be
please install them if they're not here, otherwise you will get some errors.
On a Debian distribution, this can be
done with
sudo apt install python3-dev python3-setuptools python3-pygments man2html rsync colordiff
sudo apt install python3-dev virtualenv python3-setuptools python3-pip python3-pygments man2html rsync colordiff npm nodejs libmpc-dev
sudo python3 -m pip install --upgrade pip
sudo python3 -m pip install virtualenv
On ArchLinux :
sudo pacman -S python-virtualenv man2html rsync colordiff
sudo pacman -S python-virtualenv man2html rsync colordiff nodejs npm
## Build

47
Makefile
View File

@ -10,18 +10,13 @@ export
# Dependencies
##########################################
EXECUTABLES = man2html virtualenv python3 colordiff node pygmentize
EXECUTABLES = man2html virtualenv python3 colordiff node pygmentize nodejs npm
K := $(foreach exec,$(EXECUTABLES),\
$(if $(shell which $(exec)),some string,$(warning [WARNING] No "$(exec)" executable found. \
Please install this executable for everything to work smoothly)))
# The Zarith dependency is fixed because of https://github.com/janestreet/zarith_stubs_js/pull/8
dependencies-ocaml:
opam install \
ocamlformat ANSITerminal sedlex menhir menhirLib dune cmdliner obelisk \
re obelisk unionfind bindlib zarith.1.11 zarith_stubs_js.v0.14.0 ocamlgraph \
js_of_ocaml-compiler js_of_ocaml js_of_ocaml-ppx calendar camomile \
visitors benchmark cppo odoc
opam install . --deps-only --with-doc --with-test --yes
dependencies-js:
$(MAKE) -C $(FRENCH_LAW_JS_LIB_DIR) dependencies
@ -38,15 +33,23 @@ dependencies: dependencies-ocaml dependencies-js init-submodules
##########################################
COMPILER_DIR=compiler
BUILD_SYSTEM_DIR=build_system
format:
dune build @fmt --auto-promote 2> /dev/null | true
#> build_dev : Builds the Catala compiler, without formatting code
build_dev:
dune build @update-parser-messages --auto-promote | true
dune build $(COMPILER_DIR)/catala.exe
dune build $(BUILD_SYSTEM_DIR)/clerk.exe
#> build : Builds the Catala compiler
build:
dune build @update-parser-messages --auto-promote | true
@$(MAKE) --no-print-directory format
dune build $(COMPILER_DIR)/catala.exe
dune build $(BUILD_SYSTEM_DIR)/clerk.exe
#> js_build : Builds the Web-compatible JS versions of the Catala compiler
js_build:
@ -165,11 +168,11 @@ literate_examples: literate_allocations_familiales literate_code_general_impots
FRENCH_LAW_OCAML_LIB_DIR=french_law/ocaml
$(FRENCH_LAW_OCAML_LIB_DIR)/law_source/allocations_familiales.ml: .FORCE
$(FRENCH_LAW_OCAML_LIB_DIR)/law_source/allocations_familiales.ml:
CATALA_OPTS="$(CATALA_OPTS) -O -t" $(MAKE) -C $(ALLOCATIONS_FAMILIALES_DIR) allocations_familiales.ml
cp -f $(ALLOCATIONS_FAMILIALES_DIR)/allocations_familiales.ml $@
$(FRENCH_LAW_OCAML_LIB_DIR)/law_source/unit_tests/tests_allocations_familiales.ml: .FORCE
$(FRENCH_LAW_OCAML_LIB_DIR)/law_source/unit_tests/tests_allocations_familiales.ml:
CATALA_OPTS="$(CATALA_OPTS) -O -t" $(MAKE) -s -C $(ALLOCATIONS_FAMILIALES_DIR) tests/tests_allocations_familiales.ml
cp -f $(ALLOCATIONS_FAMILIALES_DIR)/tests/tests_allocations_familiales.ml $@
@ -211,7 +214,7 @@ build_french_law_library_js: generate_french_law_library_ocaml format
FRENCH_LAW_PYTHON_LIB_DIR=french_law/python
$(FRENCH_LAW_PYTHON_LIB_DIR)/src/allocations_familiales.py: .FORCE
$(FRENCH_LAW_PYTHON_LIB_DIR)/src/allocations_familiales.py:
CATALA_OPTS="$(CATALA_OPTS) -O -t" $(MAKE) -C $(ALLOCATIONS_FAMILIALES_DIR) allocations_familiales.py
cp -f $(ALLOCATIONS_FAMILIALES_DIR)/allocations_familiales.py $@
@ -234,13 +237,23 @@ run_french_law_library_benchmark_python: type_french_law_library_python
# High-level test and benchmarks commands
##########################################
CATALA_OPTS?=
CLERK_OPTS?=
CATALA_BIN=_build/default/compiler/catala.exe
CLERK_BIN=_build/default/build_system/clerk.exe
CLERK=$(CLERK_BIN) --exe $(CATALA_BIN) \
$(CLERK_OPTS) $(if $(CATALA_OPTS),--catala-opts=$(CATALA_OPTS),)
.FORCE:
test_suite: .FORCE
@$(MAKE) --no-print-directory -C tests pass_tests
@$(CLERK) test tests
test_examples: .FORCE
@$(MAKE) --no-print-directory -C examples tests
@$(CLERK) test examples
#> tests : Run interpreter tests
tests: test_suite test_examples
@ -302,9 +315,17 @@ clean:
inspect:
gitinspector -f ml,mli,mly,iro,tex,catala,catala_en,catala_pl,catala_fr,md,fst,mld --grading
#> help_clerk : Display the clerk man page
help_clerk:
$(CLERK_BIN) --help
#> help_catala : Display the catala man page
help_catala:
$(CATALA_BIN) --help
##########################################
# Special targets
##########################################
.PHONY: inspect clean all literate_examples english allocations_familiales pygments \
install build doc format dependencies dependencies-ocaml \
install build_dev build doc format dependencies dependencies-ocaml \
catala.html help

47
README.md
View File

@ -1,7 +1,7 @@
<div align="center">
<img src="https://github.com/CatalaLang/catala/raw/master/doc/images/logo.png" alt="Catala logo" width="120"/>
<h3 align="center">
Catala
<big>Catala</big>
</h3>
<p align="center">
<a href="https://catala-lang.org/ocaml_docs/"><strong>Explore the docs »</strong></a>
@ -15,13 +15,14 @@
<a href="https://zulip.catala-lang.org/">Join Zulip Chat</a>
</p>
![CI][ci-link] ![Opam][opam-link] ![Licence][licence-link] ![Tag][tag-link] ![LoC][loc-link] ![Language][language-link] ![Issues][issues-link] ![Contributors][contributors-link] ![Activity][activity-link]
![CI][ci-link] [![Opam][opam-link]](https://opam.ocaml.org/packages/catala/) [![Licence][licence-link]](https://www.apache.org/licenses/LICENSE-2.0) ![Tag][tag-link] ![LoC][loc-link] ![Language][language-link] [![Issues][issues-link]](https://github.com/CatalaLang/catala/issues) [![Contributors][contributors-link]](https://github.com/CatalaLang/catala/graphs/contributors) [![Activity][activity-link]](https://github.com/CatalaLang/catala/pulse)
Catala is a domain-specific language for deriving
faithful-by-construction algorithms from legislative texts. To learn quickly
about the language and its features, you can jump right to the official
[Catala tutorial](https://catala-lang.org/en/examples/tutorial).
You can join the Catala community on [Zulip][chat-link]!
</div>
<br>
@ -31,19 +32,19 @@ You can join the Catala community on [Zulip][chat-link]!
<!-- vim-markdown-toc GitLab -->
* [Concepts](#concepts)
* [Building and installation](#building-and-installation)
* [Usage](#usage)
* [Examples](#examples)
* [API](#api)
* [Contributing](#contributing)
* [Test suite](#test-suite)
* [Documentation](#documentation)
* [Formal semantics](#formal-semantics)
* [Compiler documentation](#compiler-documentation)
* [License](#license)
* [Limitations and disclaimer](#limitations-and-disclaimer)
* [Pierre Catala](#pierre-catala)
- [Concepts](#concepts)
- [Building and installation](#building-and-installation)
- [Usage](#usage)
- [Examples](#examples)
- [API](#api)
- [Contributing](#contributing)
- [Test suite](#test-suite)
- [Documentation](#documentation)
- [Formal semantics](#formal-semantics)
- [Compiler documentation](#compiler-documentation)
- [License](#license)
- [Limitations and disclaimer](#limitations-and-disclaimer)
- [Pierre Catala](#pierre-catala)
<!-- vim-markdown-toc -->
@ -104,14 +105,24 @@ want to compile it from the sources of this repository or use nix. For that, see
## Usage
Use `catala --help` to get more information about the command line
options available.
### Catala
Use `catala --help` if you have installed it to get more information about the command line
options available. To get the development version of the help, run `make help_catala`
after `make build`. The `catala` binary corresponds to the Catala compiler.
The top-level `Makefile` contains a lot of useful targets to run. To display
them, use
make help
### Clerk
Use `clerk --help` if you have installed it to get more information about the command line
options available. To get the development version of the help, run `make help_clerk`
after `make build`. The `clerk` binary corresponds to the Catala build system,
responsible for testing among other things.
## Examples
To explore the different programs written in Catala, see

334
build_system/clerk.ml Normal file
View File

@ -0,0 +1,334 @@
open Cmdliner
open Utils
(**{1 Command line interface}*)
let file_or_folder =
Arg.(required & pos 1 (some file) None & info [] ~docv:"FILE(S)" ~doc:"File or folder to process")
let command =
Arg.(
required
& pos 0 (some string) None
& info [] ~docv:"COMMAND" ~doc:"Command selection among: test, run")
let debug = Arg.(value & flag & info [ "debug"; "d" ] ~doc:"Prints debug information")
let reset_test_outputs =
Arg.(
value & flag
& info [ "r"; "reset" ]
~doc:
"Used with the `test` command, resets the test output to whatever is output by the \
Catala compiler.")
let catalac =
Arg.(
value
& opt (some string) None
& info [ "e"; "exe" ] ~docv:"EXE" ~doc:"Catala compiler executable, defaults to `catala`")
let scope =
Arg.(
value
& opt (some string) None
& info [ "s"; "scope" ] ~docv:"SCOPE"
~doc:"Used with the `run` command, selects which scope of a given Catala file to run.")
let catala_opts =
Arg.(
value
& opt (some string) None
& info [ "c"; "catala-opts" ] ~docv:"LANG" ~doc:"Options to pass to the Catala compiler")
let clerk_t f =
Term.(
const f $ file_or_folder $ command $ catalac $ catala_opts $ debug $ scope $ reset_test_outputs)
let version = "0.5.0"
let info =
let doc =
"Build system for Catala, a specification language for tax and social benefits computation \
rules."
in
let man =
[
`S Manpage.s_description;
`P
"$(b,clerk) is a build system for Catala, a specification language for tax and social \
benefits computation rules";
`S Manpage.s_commands;
`I
( "test",
"Tests a Catala source file given expected outputs provided in a directory called \
`output` at the same level that the tested file. If the tested file is `foo.catala_en`, \
then `output` should contain expected output files like `foo.catala_en.$(i,BACKEND)` \
where $(i,BACKEND) is chosen among: `Interpret`, `Dcalc`, `Scopelang`, `html`, `tex`, \
`py`, `ml` and `d` (for Makefile dependencies). For the `Interpret` backend, the scope \
to test is selected by naming the expected output file \
`foo.catala_en.$(i,SCOPE).interpret`. When the argument of $(b,clerk) is a folder, it \
recursively looks for Catala files coupled with `output` directories and matching \
expected output on which to perform tests." );
`I
("run", "Runs the Catala interpreter on a given scope of a given file. See the `-s` option.");
`S Manpage.s_authors;
`P "Denis Merigoux <denis.merigoux@inria.fr>";
`S Manpage.s_examples;
`P "Typical usage:";
`Pre "clerk test file.catala_en";
`S Manpage.s_bugs;
`P "Please file bug reports at https://github.com/CatalaLang/catala/issues";
]
in
let exits = Term.default_exits @ [ Term.exit_info ~doc:"on error." 1 ] in
Term.info "clerk" ~version ~doc ~exits ~man
(**{1 Testing}*)
let catala_backend_to_string (backend : Cli.backend_option) : string =
match backend with
| Cli.Interpret -> "Interpret"
| Cli.Makefile -> "Makefile"
| Cli.OCaml -> "Ocaml"
| Cli.Scopelang -> "Scopelang"
| Cli.Dcalc -> "Dcalc"
| Cli.Latex -> "Latex"
| Cli.Proof -> "Proof"
| Cli.Html -> "Html"
| Cli.Python -> "Python"
| Cli.Typecheck -> "Typecheck"
type expected_output_descr = {
base_filename : string;
output_dir : string;
complete_filename : string;
backend : Cli.backend_option;
scope : string option;
}
let catala_suffix_regex = Re.Pcre.regexp "\\.catala_(\\w){2}"
let filename_to_expected_output_descr (output_dir : string) (filename : string) :
expected_output_descr option =
let complete_filename = filename in
let first_extension = Filename.extension filename in
let filename = Filename.remove_extension filename in
let backend =
match String.lowercase_ascii first_extension with
| ".interpret" -> Some Cli.Interpret
| ".d" -> Some Cli.Makefile
| ".ml" -> Some Cli.OCaml
| ".scopelang" -> Some Cli.Scopelang
| ".dcalc" -> Some Cli.Dcalc
| ".tex" -> Some Cli.Latex
| ".html" -> Some Cli.Html
| ".py" -> Some Cli.Python
| ".proof" -> Some Cli.Proof
| ".typecheck" -> Some Cli.Typecheck
| _ -> None
in
match backend with
| None -> None
| Some backend ->
let second_extension = Filename.extension filename in
let base_filename, scope =
if Re.Pcre.pmatch ~rex:catala_suffix_regex second_extension then (filename, None)
else
let scope_name_regex = Re.Pcre.regexp "\\.(.+)" in
let scope_name = (Re.Pcre.extract ~rex:scope_name_regex second_extension).(1) in
(Filename.remove_extension filename, Some scope_name)
in
Some { output_dir; complete_filename; base_filename; backend; scope }
(** Given a file, looks in the relative [output] directory if there are files with the same base
name that contain expected outputs for different *)
let search_for_expected_outputs (file : string) : expected_output_descr list =
let output_dir = Filename.dirname file ^ Filename.dir_sep ^ "output/" in
let output_files = try Sys.readdir output_dir with Sys_error _ -> Array.make 0 "" in
List.filter_map
(fun output_file ->
match filename_to_expected_output_descr output_dir output_file with
| None -> None
| Some expected_output ->
if expected_output.base_filename = Filename.basename file then Some expected_output
else None)
(Array.to_list output_files)
type testing_result = { error_code : int; number_of_tests_run : int; number_correct : int }
let test_file (tested_file : string) (catala_exe : string) (catala_opts : string)
(reset_test_outputs : bool) : testing_result =
let expected_outputs = search_for_expected_outputs tested_file in
if List.length expected_outputs = 0 then (
Cli.debug_print (Format.asprintf "No expected outputs were found for test file %s" tested_file);
{ error_code = 0; number_of_tests_run = 0; number_correct = 0 })
else
List.fold_left
(fun (exit : testing_result) expected_output ->
let catala_backend = catala_backend_to_string expected_output.backend in
let reproducible_catala_command =
[
catala_exe;
catala_opts;
(match expected_output.scope with None -> "" | Some scope -> "-s " ^ scope);
catala_backend;
tested_file;
"--unstyled";
]
in
let command =
String.concat " "
(List.filter (fun s -> s <> "") reproducible_catala_command
@ (match expected_output.backend with
| Cli.Proof ->
[ "--disable_counterexamples" ]
(* Counterexamples can be different at each call because of the randomness inside
SMT solver, so we can't expect their value to remain constant. Hence we disable
the counterexamples when testing the replication of failed proofs. *)
| _ -> [])
@
match expected_output.backend with
| Cli.Interpret | Cli.Proof | Cli.Typecheck ->
if reset_test_outputs then
[
">";
Format.asprintf "%s%s" expected_output.output_dir
expected_output.complete_filename;
"2>&1 ";
]
else
[
"2>&1 ";
"|";
Format.asprintf "colordiff -u -b %s%s -" expected_output.output_dir
expected_output.complete_filename;
]
| Cli.Python | Cli.OCaml | Cli.Dcalc | Cli.Scopelang | Cli.Latex | Cli.Html
| Cli.Makefile ->
(* for those backends, the output of the Catala compiler will be written in a
temporary file which later we're going to diff with the *)
if reset_test_outputs then
[
"-o";
Format.asprintf "%s%s" expected_output.output_dir
expected_output.complete_filename;
]
else
let temp_file =
Filename.temp_file "clerk_"
("_" ^ catala_backend_to_string expected_output.backend)
in
[
"-o";
temp_file;
";";
Format.asprintf "colordiff -u -b %s%s %s" expected_output.output_dir
expected_output.complete_filename temp_file;
])
in
Cli.debug_print ("Running: " ^ command);
let result = Sys.command command in
if result <> 0 && not reset_test_outputs then (
Cli.error_print
(Format.asprintf "Test failed: %s@\nTo reproduce, run %s from folder %s"
(Cli.print_with_style [ ANSITerminal.magenta ] "%s%s" expected_output.output_dir
expected_output.complete_filename)
(Cli.print_with_style [ ANSITerminal.yellow ] "%s"
(String.concat " " (List.filter (fun s -> s <> "") reproducible_catala_command)))
(Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Sys.getcwd ())));
{
error_code = 1;
number_of_tests_run = exit.number_of_tests_run + 1;
number_correct = exit.number_correct;
})
else (
Cli.result_print
(Format.asprintf "Test %s: %s"
(if reset_test_outputs then "reset" else "passed")
(Cli.print_with_style [ ANSITerminal.magenta ] "%s%s" expected_output.output_dir
expected_output.complete_filename));
{
error_code = exit.error_code;
number_of_tests_run = exit.number_of_tests_run + 1;
number_correct = exit.number_correct + 1;
}))
{ error_code = 0; number_of_tests_run = 0; number_correct = 0 }
expected_outputs
(**{1 Running}*)
let run_file (file : string) (catala_exe : string) (catala_opts : string) (scope : string) : int =
let command =
String.concat " "
(List.filter (fun s -> s <> "") [ catala_exe; catala_opts; "-s " ^ scope; "Interpret"; file ])
in
Cli.debug_print ("Running: " ^ command);
Sys.command command
(** {1 Driver} *)
let get_catala_files_in_folder (dir : string) : string list =
let rec loop result = function
| f :: fs when Sys.is_directory f ->
Sys.readdir f |> Array.to_list
|> List.map (Filename.concat f)
|> List.append fs |> loop result
| f :: fs -> loop (f :: result) fs
| [] -> result
in
let all_files_in_folder = loop [] [ dir ] in
List.filter (Re.Pcre.pmatch ~rex:catala_suffix_regex) all_files_in_folder
let driver (file_or_folder : string) (command : string) (catala_exe : string option)
(catala_opts : string option) (debug : bool) (scope : string option) (reset_test_outputs : bool)
: int =
if debug then Cli.debug_flag := true;
let catala_exe = Option.fold ~none:"catala" ~some:Fun.id catala_exe in
let catala_opts = Option.fold ~none:"" ~some:Fun.id catala_opts in
match String.lowercase_ascii command with
| "test" ->
let results =
if Sys.is_directory file_or_folder then (
let results =
List.fold_left
(fun (exit : testing_result) file ->
let result = test_file file catala_exe catala_opts reset_test_outputs in
{
error_code =
(if result.error_code <> 0 && exit.error_code = 0 then result.error_code
else exit.error_code);
number_of_tests_run = exit.number_of_tests_run + result.number_of_tests_run;
number_correct = exit.number_correct + result.number_correct;
})
{ error_code = 0; number_of_tests_run = 0; number_correct = 0 }
(get_catala_files_in_folder file_or_folder)
in
Cli.result_print
(Format.asprintf "Number of tests passed in folder %s: %s"
(Cli.print_with_style [ ANSITerminal.magenta ] "%s" file_or_folder)
(Cli.print_with_style
[
(if results.number_correct = results.number_of_tests_run then ANSITerminal.green
else ANSITerminal.red);
]
"%d/%d" results.number_correct results.number_of_tests_run));
results)
else test_file file_or_folder catala_exe catala_opts reset_test_outputs
in
results.error_code
| "run" -> (
match scope with
| Some scope -> run_file file_or_folder catala_exe catala_opts scope
| None ->
Cli.error_print "Please provide a scope to run with the -s option";
1)
| _ ->
Cli.error_print (Format.asprintf "The command \"%s\" is unknown to clerk." command);
1
let _ =
let return_code = Cmdliner.Term.eval (clerk_t driver, info) in
match return_code with
| `Ok 0 -> Cmdliner.Term.exit (`Ok 0)
| _ -> Cmdliner.Term.exit (`Error `Term)

5
build_system/dune Normal file
View File

@ -0,0 +1,5 @@
(executable
(name clerk)
(public_name clerk)
(libraries catala.runtime catala.utils cmdliner re ANSITerminal)
(package catala))

3
catala.opam
View File

@ -31,7 +31,10 @@ depends: [
"benchmark" {>= "1.6"}
"js_of_ocaml-ppx" {>= "3.8.0"}
"camomile" {>= "1.0.2"}
"z3" {>= "4.8.11"}
"cppo" {>= "1"}
"obelisk" {dev}
"ocamlformat" {dev & = "0.19.0"}
"odoc" {with-doc}
]
build: [

2
compiler/catala_web_interpreter.ml
View File

@ -10,7 +10,7 @@ let _ =
(Contents (Js.to_string contents))
false false false false "Interpret"
(Some (Js.to_string language))
None trace false
None trace false false
(Some (Js.to_string scope))
None
end)

41
compiler/dcalc/ast.ml
View File

@ -203,8 +203,18 @@ let make_let_in (x : Var.t) (tau : typ Pos.marked) (e1 : expr Pos.marked Bindlib
(e2 : expr Pos.marked Bindlib.box) (pos : Pos.t) : expr Pos.marked Bindlib.box =
make_app (make_abs (Array.of_list [ x ]) e2 pos [ tau ] pos) [ e1 ] pos
let build_whole_scope_expr (ctx : decl_ctx) (body : scope_body) (pos_scope : Pos.t) :
expr Pos.marked Bindlib.box =
let empty_thunked_term : expr Pos.marked =
let silent = Var.make ("_", Pos.no_pos) in
Bindlib.unbox
(make_abs
(Array.of_list [ silent ])
(Bindlib.box (ELit LEmptyError, Pos.no_pos))
Pos.no_pos [ (TLit TUnit, Pos.no_pos) ] Pos.no_pos)
let is_value (e : expr Pos.marked) : bool =
match Pos.unmark e with ELit _ | EAbs _ | EOp _ -> true | _ -> false
let build_whole_scope_expr (ctx : decl_ctx) (body : scope_body) (pos_scope : Pos.t) =
let body_expr =
List.fold_right
(fun scope_let acc ->
@ -250,3 +260,30 @@ let build_whole_program_expr (p : program) (main_scope : ScopeName.t) =
(build_whole_scope_expr p.decl_ctx scope_body pos)
acc pos)
p.scopes end_result
let rec expr_size (e : expr Pos.marked) : int =
match Pos.unmark e with
| EVar _ | ELit _ | EOp _ -> 1
| ETuple (args, _) | EArray args -> List.fold_left (fun acc arg -> acc + expr_size arg) 1 args
| ETupleAccess (e1, _, _, _) | EInj (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 ->
expr_size e1 + 1
| EMatch (arg, args, _) | EApp (arg, args) ->
List.fold_left (fun acc arg -> acc + expr_size arg) (1 + expr_size arg) args
| EAbs ((binder, _), _) ->
let _, body = Bindlib.unmbind binder in
1 + expr_size body
| EIfThenElse (e1, e2, e3) -> 1 + expr_size e1 + expr_size e2 + expr_size e3
| EDefault (exceptions, just, cons) ->
List.fold_left
(fun acc except -> acc + expr_size except)
(1 + expr_size just + expr_size cons)
exceptions
let variable_types (p : program) : typ Pos.marked VarMap.t =
List.fold_left
(fun acc (_, _, scope) ->
List.fold_left
(fun acc scope_let ->
VarMap.add (Pos.unmark scope_let.scope_let_var) scope_let.scope_let_typ acc)
acc scope.scope_body_lets)
VarMap.empty p.scopes

19
compiler/dcalc/ast.mli
View File

@ -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
@ -167,7 +169,9 @@ type scope_body = {
type program = { decl_ctx : decl_ctx; scopes : (ScopeName.t * expr Bindlib.var * scope_body) list }
(** {1 Variable helpers} *)
(** {1 Helpers} *)
(** {2 Variables}*)
module Var : sig
type t = expr Bindlib.var
@ -209,6 +213,12 @@ val make_let_in :
Pos.t ->
expr Pos.marked Bindlib.box
(**{2 Other}*)
val empty_thunked_term : expr Pos.marked
val is_value : expr Pos.marked -> bool
(** {1 AST manipulation helpers}*)
val build_whole_scope_expr : decl_ctx -> scope_body -> Pos.t -> expr Pos.marked Bindlib.box
@ -218,3 +228,10 @@ val build_whole_scope_expr : decl_ctx -> scope_body -> Pos.t -> expr Pos.marked
val build_whole_program_expr : program -> ScopeName.t -> expr Pos.marked Bindlib.box
(** Usage: [build_whole_program_expr program main_scope] builds an expression corresponding to the
main program and returning the main scope as a function. *)
val expr_size : expr Pos.marked -> int
(** Used by the optimizer to know when to stop *)
val variable_types : program -> typ Pos.marked VarMap.t
(** Traverses all the scopes and retrieves all the types for the variables that may appear in scope
or subscope variable definitions, giving them as a big map. *)

33
compiler/dcalc/dcalc.mld
View File

@ -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.
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}

43
compiler/dcalc/interpreter.ml
View File

@ -22,16 +22,6 @@ module A = Ast
let is_empty_error (e : A.expr Pos.marked) : bool =
match Pos.unmark e with ELit LEmptyError -> true | _ -> false
let empty_thunked_term : Ast.expr Pos.marked =
let silent = Ast.Var.make ("_", Pos.no_pos) in
Bindlib.unbox
(Ast.make_abs
(Array.of_list [ silent ])
(Bindlib.box (Ast.ELit Ast.LEmptyError, Pos.no_pos))
Pos.no_pos
[ (Ast.TLit Ast.TUnit, Pos.no_pos) ]
Pos.no_pos)
let log_indent = ref 0
(** {1 Evaluation} *)
@ -226,10 +216,10 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
(Format.asprintf "%*s%a %a: %s" (!log_indent * 2) "" Print.format_log_entry entry
Print.format_uid_list infos
(match e' with
| Ast.EAbs _ -> Cli.print_with_style [ ANSITerminal.green ] "<function>"
(* | Ast.EAbs _ -> Cli.print_with_style [ ANSITerminal.green ] "<function>" *)
| _ ->
let expr_str =
Format.asprintf "%a" (Print.format_expr ctx) (e', Pos.no_pos)
Format.asprintf "%a" (Print.format_expr ctx ~debug:false) (e', Pos.no_pos)
in
let expr_str =
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
@ -268,7 +258,9 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
@ List.mapi
(fun i arg ->
( Some
(Format.asprintf "Argument n°%d, value %a" (i + 1) (Print.format_expr ctx) arg),
(Format.asprintf "Argument n°%d, value %a" (i + 1)
(Print.format_expr ctx ~debug:true)
arg),
Pos.get_position arg ))
args))
op
@ -299,7 +291,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
"function has not been reduced to a lambda at evaluation (should not happen if the \
term was well-typed"
(Pos.get_position e))
| EAbs _ | ELit _ | EOp _ -> e (* thse are values *)
| EAbs _ | ELit _ | EOp _ -> e (* these are values *)
| ETuple (es, s) ->
let new_es = List.map (evaluate_expr ctx) es in
if List.exists is_empty_error new_es then Pos.same_pos_as (A.ELit LEmptyError) e
@ -331,7 +323,8 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
(Format.asprintf
"The expression %a should be a tuple with %d components but is not (should not \
happen if the term was well-typed)"
(Print.format_expr ctx) e n)
(Print.format_expr ctx ~debug:true)
e n)
(Pos.get_position e1))
| EInj (e1, n, en, ts) ->
let e1' = evaluate_expr ctx e1 in
@ -363,7 +356,6 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
the term was well-typed"
(Pos.get_position e1))
| EDefault (exceptions, just, cons) -> (
let exceptions_orig = exceptions in
let exceptions = List.map (evaluate_expr ctx) exceptions in
let empty_count = List.length (List.filter is_empty_error exceptions) in
match List.length exceptions - empty_count with
@ -381,12 +373,12 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
| 1 -> List.find (fun sub -> not (is_empty_error sub)) exceptions
| _ ->
Errors.raise_multispanned_error
"There is a conflict between multiple exceptions for assigning the same variable."
"There is a conflict between multiple validd consequences for assigning the same \
variable."
(List.map
(fun (_, except) -> (Some "This justification is true:", Pos.get_position except))
(List.filter
(fun (sub, _) -> not (is_empty_error sub))
(List.map2 (fun x y -> (x, y)) exceptions exceptions_orig))))
(fun except ->
(Some "This consequence has a valid justification:", Pos.get_position except))
(List.filter (fun sub -> not (is_empty_error sub)) exceptions)))
| EIfThenElse (cond, et, ef) -> (
match Pos.unmark (evaluate_expr ctx cond) with
| ELit (LBool true) -> evaluate_expr ctx et
@ -416,8 +408,11 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
match Pos.unmark e' with
| EApp ((Ast.EOp (Binop op), pos_op), [ ((ELit _, _) as e1); ((ELit _, _) as e2) ]) ->
Errors.raise_spanned_error
(Format.asprintf "Assertion failed: %a %a %a" (Print.format_expr ctx) e1
Print.format_binop (op, pos_op) (Print.format_expr ctx) e2)
(Format.asprintf "Assertion failed: %a %a %a"
(Print.format_expr ctx ~debug:false)
e1 Print.format_binop (op, pos_op)
(Print.format_expr ctx ~debug:false)
e2)
(Pos.get_position e')
| _ ->
Errors.raise_spanned_error (Format.asprintf "Assertion failed") (Pos.get_position e'))
@ -434,7 +429,7 @@ let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Pos.marked) :
(Uid.MarkedString.info * Ast.expr Pos.marked) list =
match Pos.unmark (evaluate_expr ctx e) with
| Ast.EAbs (_, [ (Ast.TTuple (taus, Some s_in), _) ]) -> (
let application_term = List.map (fun _ -> empty_thunked_term) taus in
let application_term = List.map (fun _ -> Ast.empty_thunked_term) taus in
let to_interpret =
(Ast.EApp (e, [ (Ast.ETuple (application_term, Some s_in), Pos.no_pos) ]), Pos.no_pos)
in

8
compiler/dcalc/interpreter.mli
View File

@ -16,9 +16,11 @@
open Utils
val empty_thunked_term : Ast.expr Pos.marked
val evaluate_expr : Ast.decl_ctx -> Ast.expr Pos.marked -> Ast.expr Pos.marked
(** Evaluates an expression according to the semantics of the default calculus. *)
val interpret_program :
Ast.decl_ctx -> Ast.expr Pos.marked -> (Uid.MarkedString.info * Ast.expr Pos.marked) list
(** Interpret a program. This function expects an expression typed as a function whose argument are
all thunked. The function is executed by providing for each argument a thunked empty default. *)
(** Interprets a program. This function expects an expression typed as a function whose argument are
all thunked. The function is executed by providing for each argument a thunked empty default.
Returns a list of all the computed values for the scope variables of the executed scope. *)

230
compiler/dcalc/optimizations.ml Normal file
View File

@ -0,0 +1,230 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 2022 Inria, contributors: Alain Delaët
<alain.delaet--tixeuil@inria.fr>, Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
open Utils
open Ast
type partial_evaluation_ctx = { var_values : expr Pos.marked Ast.VarMap.t; decl_ctx : decl_ctx }
let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked) :
expr Pos.marked Bindlib.box =
let pos = Pos.get_position e in
let rec_helper = partial_evaluation ctx in
match Pos.unmark e with
| EApp
( ((EOp (Unop Not), _ | EApp ((EOp (Unop (Log _)), _), [ (EOp (Unop Not), _) ]), _) as op),
[ e1 ] ) ->
(* reduction of logical not *)
(Bindlib.box_apply (fun e1 ->
match e1 with
| ELit (LBool false), _ -> (ELit (LBool true), pos)
| ELit (LBool true), _ -> (ELit (LBool false), pos)
| _ -> (EApp (op, [ e1 ]), pos)))
(rec_helper e1)
| EApp
( ((EOp (Binop Or), _ | EApp ((EOp (Unop (Log _)), _), [ (EOp (Binop Or), _) ]), _) as op),
[ e1; e2 ] ) ->
(* reduction of logical or *)
(Bindlib.box_apply2 (fun e1 e2 ->
match (e1, e2) with
| (ELit (LBool false), _), new_e | new_e, (ELit (LBool false), _) -> new_e
| (ELit (LBool true), _), _ | _, (ELit (LBool true), _) -> (ELit (LBool true), pos)
| _ -> (EApp (op, [ e1; e2 ]), pos)))
(rec_helper e1) (rec_helper e2)
| EApp
( ((EOp (Binop And), _ | EApp ((EOp (Unop (Log _)), _), [ (EOp (Binop And), _) ]), _) as op),
[ e1; e2 ] ) ->
(* reduction of logical and *)
(Bindlib.box_apply2 (fun e1 e2 ->
match (e1, e2) with
| (ELit (LBool true), _), new_e | new_e, (ELit (LBool true), _) -> new_e
| (ELit (LBool false), _), _ | _, (ELit (LBool false), _) -> (ELit (LBool false), pos)
| _ -> (EApp (op, [ e1; e2 ]), pos)))
(rec_helper e1) (rec_helper e2)
| EVar (x, _) -> Bindlib.box_apply (fun x -> (x, pos)) (Bindlib.box_var x)
| ETuple (args, s_name) ->
Bindlib.box_apply
(fun args -> (ETuple (args, s_name), pos))
(List.map rec_helper args |> Bindlib.box_list)
| ETupleAccess (arg, i, s_name, typs) ->
Bindlib.box_apply (fun arg -> (ETupleAccess (arg, i, s_name, typs), pos)) (rec_helper arg)
| EInj (arg, i, e_name, typs) ->
Bindlib.box_apply (fun arg -> (EInj (arg, i, e_name, typs), pos)) (rec_helper arg)
| EMatch (arg, arms, e_name) ->
Bindlib.box_apply2
(fun arg arms ->
match (arg, arms) with
| (EInj (e1, i, e_name', _ts), _), _ when Ast.EnumName.compare e_name e_name' = 0 ->
(* iota reduction *)
(EApp (List.nth arms i, [ e1 ]), pos)
| _ -> (EMatch (arg, arms, e_name), pos))
(rec_helper arg)
(List.map rec_helper arms |> Bindlib.box_list)
| EArray args ->
Bindlib.box_apply
(fun args -> (EArray args, pos))
(List.map rec_helper args |> Bindlib.box_list)
| ELit l -> Bindlib.box (ELit l, pos)
| EAbs ((binder, binder_pos), typs) ->
let vars, body = Bindlib.unmbind binder in
let new_body = rec_helper body in
let new_binder = Bindlib.bind_mvar vars new_body in
Bindlib.box_apply (fun binder -> (EAbs ((binder, binder_pos), typs), pos)) new_binder
| EApp (f, args) ->
Bindlib.box_apply2
(fun f args ->
match Pos.unmark f with
| EAbs ((binder, _pos_binder), _ts) ->
(* beta reduction *)
Bindlib.msubst binder (List.map fst args |> Array.of_list)
| _ -> (EApp (f, args), pos))
(rec_helper f)
(List.map rec_helper args |> Bindlib.box_list)
| EAssert e1 -> Bindlib.box_apply (fun e1 -> (EAssert e1, pos)) (rec_helper e1)
| EOp op -> Bindlib.box (EOp op, pos)
| EDefault (exceptions, just, cons) ->
Bindlib.box_apply3
(fun exceptions just cons ->
(* TODO: mechanically prove each of these optimizations correct :) *)
match
( List.filter
(fun except -> match Pos.unmark except with ELit LEmptyError -> false | _ -> true)
exceptions
(* we can discard the exceptions that are always empty error *),
just,
cons )
with
| exceptions, just, cons
when List.fold_left
(fun nb except -> if is_value except then nb + 1 else nb)
0 exceptions
> 1 ->
(* at this point we know a conflict error will be triggered so we just feed the
expression to the interpreter that will print the beautiful right error message *)
Interpreter.evaluate_expr ctx.decl_ctx (EDefault (exceptions, just, cons), pos)
| [ except ], _, _ when is_value except ->
(* if there is only one exception and it is a non-empty value it is always chosen *)
except
| ( [],
((ELit (LBool true) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ])), _),
cons ) ->
cons
| ( [],
((ELit (LBool false) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ])), _),
_ ) ->
(ELit LEmptyError, pos)
| [], just, cons ->
(* without exceptions, a default is just an [if then else] raising an error in the
else case *)
(EIfThenElse (just, cons, (ELit LEmptyError, pos)), pos)
| exceptions, just, cons -> (EDefault (exceptions, just, cons), pos))
(List.map rec_helper exceptions |> Bindlib.box_list)
(rec_helper just) (rec_helper cons)
| EIfThenElse (e1, e2, e3) ->
Bindlib.box_apply3
(fun e1 e2 e3 ->
match (Pos.unmark e1, Pos.unmark e2, Pos.unmark e3) with
| ELit (LBool true), _, _
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ]), _, _ ->
e2
| ELit (LBool false), _, _
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]), _, _ ->
e3
| ( _,
(ELit (LBool true) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ])),
(ELit (LBool false) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ])) )
->
e1
| _ -> (EIfThenElse (e1, e2, e3), pos))
(rec_helper e1) (rec_helper e2) (rec_helper e3)
| ErrorOnEmpty e1 -> Bindlib.box_apply (fun e1 -> (ErrorOnEmpty e1, pos)) (rec_helper e1)
let optimize_expr (decl_ctx : decl_ctx) (e : expr Pos.marked) =
partial_evaluation { var_values = VarMap.empty; decl_ctx } e
let program_map (t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box) (ctx : 'a) (p : program)
: program =
{
p with
scopes =
List.map
(fun (s_name, s_var, s_body) ->
let new_s_body =
{
s_body with
scope_body_lets =
List.map
(fun scope_let ->
{
scope_let with
scope_let_expr =
Bindlib.unbox (Bindlib.box_apply (t ctx) scope_let.scope_let_expr);
})
s_body.scope_body_lets;
}
in
(s_name, s_var, new_s_body))
p.scopes;
}
let optimize_program (p : program) : program =
program_map partial_evaluation { var_values = VarMap.empty; decl_ctx = p.decl_ctx } p
let rec remove_all_logs (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position e in
let rec_helper = remove_all_logs in
match Pos.unmark e with
| EVar (x, _) -> Bindlib.box_apply (fun x -> (x, pos)) (Bindlib.box_var x)
| ETuple (args, s_name) ->
Bindlib.box_apply
(fun args -> (ETuple (args, s_name), pos))
(List.map rec_helper args |> Bindlib.box_list)
| ETupleAccess (arg, i, s_name, typs) ->
Bindlib.box_apply (fun arg -> (ETupleAccess (arg, i, s_name, typs), pos)) (rec_helper arg)
| EInj (arg, i, e_name, typs) ->
Bindlib.box_apply (fun arg -> (EInj (arg, i, e_name, typs), pos)) (rec_helper arg)
| EMatch (arg, arms, e_name) ->
Bindlib.box_apply2
(fun arg arms -> (EMatch (arg, arms, e_name), pos))
(rec_helper arg)
(List.map rec_helper arms |> Bindlib.box_list)
| EArray args ->
Bindlib.box_apply
(fun args -> (EArray args, pos))
(List.map rec_helper args |> Bindlib.box_list)
| ELit l -> Bindlib.box (ELit l, pos)
| EAbs ((binder, binder_pos), typs) ->
let vars, body = Bindlib.unmbind binder in
let new_body = rec_helper body in
let new_binder = Bindlib.bind_mvar vars new_body in
Bindlib.box_apply (fun binder -> (EAbs ((binder, binder_pos), typs), pos)) new_binder
| EApp (f, args) ->
Bindlib.box_apply2
(fun f args ->
match (Pos.unmark f, args) with
| EOp (Unop (Log _)), [ arg ] -> arg
| _ -> (EApp (f, args), pos))
(rec_helper f)
(List.map rec_helper args |> Bindlib.box_list)
| EAssert e1 -> Bindlib.box_apply (fun e1 -> (EAssert e1, pos)) (rec_helper e1)
| EOp op -> Bindlib.box (EOp op, pos)
| EDefault (exceptions, just, cons) ->
Bindlib.box_apply3
(fun exceptions just cons -> (EDefault (exceptions, just, cons), pos))
(List.map rec_helper exceptions |> Bindlib.box_list)
(rec_helper just) (rec_helper cons)
| EIfThenElse (e1, e2, e3) ->
Bindlib.box_apply3
(fun e1 e2 e3 -> (EIfThenElse (e1, e2, e3), pos))
(rec_helper e1) (rec_helper e2) (rec_helper e3)
| ErrorOnEmpty e1 -> Bindlib.box_apply (fun e1 -> (ErrorOnEmpty e1, pos)) (rec_helper e1)

24
compiler/dcalc/optimizations.mli Normal file
View File

@ -0,0 +1,24 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 2022 Inria, contributors: Alain Delaët
<alain.delaet--tixeuil@inria.fr>, Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
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
val optimize_expr : decl_ctx -> expr Pos.marked -> expr Pos.marked Bindlib.box
val optimize_program : program -> program
val remove_all_logs : expr Pos.marked -> expr Pos.marked Bindlib.box

40
compiler/dcalc/print.ml
View File

@ -35,24 +35,23 @@ let format_uid_list (fmt : Format.formatter) (infos : Uid.MarkedString.info list
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ".")
(fun fmt info ->
Format.fprintf fmt "%s"
(Utils.Cli.print_with_style
(if begins_with_uppercase (Pos.unmark info) then [ ANSITerminal.red ] else [])
"%s"
(Format.asprintf "%a" Utils.Uid.MarkedString.format_info info))))
Format.fprintf fmt "%a"
(Utils.Cli.format_with_style
(if begins_with_uppercase (Pos.unmark info) then [ ANSITerminal.red ] else []))
(Format.asprintf "%a" Utils.Uid.MarkedString.format_info info)))
infos
let format_keyword (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%s" (Utils.Cli.print_with_style [ ANSITerminal.red ] "%s" s)
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.red ]) s
let format_base_type (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%s" (Utils.Cli.print_with_style [ ANSITerminal.yellow ] "%s" s)
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.yellow ]) s
let format_punctuation (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%s" (Utils.Cli.print_with_style [ ANSITerminal.cyan ] "%s" s)
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.cyan ]) s
let format_operator (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%s" (Utils.Cli.print_with_style [ ANSITerminal.green ] "%s" s)
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.green ]) s
let format_tlit (fmt : Format.formatter) (l : typ_lit) : unit =
format_base_type fmt
@ -80,8 +79,8 @@ let rec format_typ (ctx : Ast.decl_ctx) (fmt : Format.formatter) (typ : typ Pos.
(fun fmt t -> Format.fprintf fmt "%a" format_typ t))
ts
| TTuple (args, Some s) ->
Format.fprintf fmt "%a [%a]" Ast.StructName.format_t s
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ") format_typ)
Format.fprintf fmt "%a {%a}" Ast.StructName.format_t s
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ;@ ") format_typ)
args
| TEnum (_, e) -> Format.fprintf fmt "%a" Ast.EnumName.format_t e
| TArrow (t1, t2) ->
@ -136,7 +135,7 @@ let format_ternop (fmt : Format.formatter) (op : ternop Pos.marked) : unit =
match Pos.unmark op with Fold -> format_keyword fmt "fold"
let format_log_entry (fmt : Format.formatter) (entry : log_entry) : unit =
Format.fprintf fmt "%s"
Format.fprintf fmt "@<2>%s"
(match entry with
| VarDef _ -> Utils.Cli.print_with_style [ ANSITerminal.blue ] "≔ "
| BeginCall -> Utils.Cli.print_with_style [ ANSITerminal.yellow ] "→ "
@ -166,8 +165,9 @@ let needs_parens (e : expr Pos.marked) : bool =
let format_var (fmt : Format.formatter) (v : Var.t) : unit =
Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
let rec format_expr (ctx : Ast.decl_ctx) (fmt : Format.formatter) (e : expr Pos.marked) : unit =
let format_expr = format_expr ctx in
let rec format_expr ?(debug : bool = false) (ctx : Ast.decl_ctx) (fmt : Format.formatter)
(e : expr Pos.marked) : unit =
let format_expr = format_expr ~debug ctx in
let format_with_parens (fmt : Format.formatter) (e : expr Pos.marked) =
if needs_parens e then
Format.fprintf fmt "%a%a%a" format_punctuation "(" format_expr e format_punctuation ")"
@ -218,7 +218,10 @@ let rec format_expr (ctx : Ast.decl_ctx) (fmt : Format.formatter) (e : expr Pos.
Format.fprintf fmt "@[<hov 2>%a%a@ %a@]" Ast.EnumConstructor.format_t c
format_punctuation ":" format_expr e))
(List.combine es (List.map fst (Ast.EnumMap.find e_name ctx.ctx_enums)))
| ELit l -> Format.fprintf fmt "%a" format_lit (Pos.same_pos_as l e)
| ELit l ->
Format.fprintf fmt "%s"
(Utils.Cli.print_with_style [ ANSITerminal.yellow ] "%s"
(Format.asprintf "%a" format_lit (Pos.same_pos_as l e)))
| EApp ((EAbs ((binder, _), taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
@ -247,7 +250,7 @@ let rec format_expr (ctx : Ast.decl_ctx) (fmt : Format.formatter) (e : expr Pos.
| EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1 format_binop
(op, Pos.no_pos) format_with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [ arg1 ]) -> Format.fprintf fmt "%a" format_with_parens arg1
| EApp ((EOp (Unop (Log _)), _), [ arg1 ]) when not debug -> format_expr fmt arg1
| EApp ((EOp (Unop op), _), [ arg1 ]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_unop (op, Pos.no_pos) format_with_parens arg1
| EApp (f, args) ->
@ -276,6 +279,7 @@ let rec format_expr (ctx : Ast.decl_ctx) (fmt : Format.formatter) (e : expr Pos.
Format.fprintf fmt "@[<hov 2>%a@ %a%a%a@]" format_keyword "assert" format_punctuation "("
format_expr e' format_punctuation ")"
let format_scope (ctx : decl_ctx) (fmt : Format.formatter) ((n, s) : Ast.ScopeName.t * scope_body) =
Format.fprintf fmt "@[<hov 2>let %a =@ %a@]" Ast.ScopeName.format_t n (format_expr ctx)
let format_scope ?(debug : bool = false) (ctx : decl_ctx) (fmt : Format.formatter)
((n, s) : Ast.ScopeName.t * scope_body) =
Format.fprintf fmt "@[<hov 2>let %a =@ %a@]" Ast.ScopeName.format_t n (format_expr ctx ~debug)
(Bindlib.unbox (Ast.build_whole_scope_expr ctx s (Pos.get_position (Ast.ScopeName.get_info n))))

16
compiler/dcalc/print.mli
View File

@ -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} *)
@ -42,6 +44,16 @@ val format_unop : Format.formatter -> Ast.unop Pos.marked -> unit
val format_var : Format.formatter -> Ast.Var.t -> unit
val format_expr : Ast.decl_ctx -> Format.formatter -> Ast.expr Pos.marked -> unit
val format_expr :
?debug:bool (** [true] for debug printing *) ->
Ast.decl_ctx ->
Format.formatter ->
Ast.expr Pos.marked ->
unit
val format_scope : Ast.decl_ctx -> Format.formatter -> Ast.ScopeName.t * Ast.scope_body -> unit
val format_scope :
?debug:bool (** [true] for debug printing *) ->
Ast.decl_ctx ->
Format.formatter ->
Ast.ScopeName.t * Ast.scope_body ->
unit

10
compiler/dcalc/typing.ml
View File

@ -90,11 +90,11 @@ let rec unify (ctx : Ast.decl_ctx) (t1 : typ Pos.marked UnionFind.elem)
(Format.asprintf "%a" (format_typ ctx) t2))
in
Errors.raise_multispanned_error
(Format.asprintf "Error during typechecking, incompatible types:\n%s %s\n%s %s"
(Cli.print_with_style [ ANSITerminal.blue; ANSITerminal.Bold ] "-->")
t1_s
(Cli.print_with_style [ ANSITerminal.blue; ANSITerminal.Bold ] "-->")
t2_s)
(Format.asprintf "Error during typechecking, incompatible types:\n%a %s\n%a %s"
(Cli.format_with_style [ ANSITerminal.blue; ANSITerminal.Bold ])
"-->" t1_s
(Cli.format_with_style [ ANSITerminal.blue; ANSITerminal.Bold ])
"-->" t2_s)
[
(Some (Format.asprintf "Type %s coming from expression:" t1_s), t1_pos);
(Some (Format.asprintf "Type %s coming from expression:" t2_s), t2_pos);

48
compiler/desugared/ast.ml
View File

@ -26,6 +26,12 @@ module RuleMap : Map.S with type key = RuleName.t = Map.Make (RuleName)
module RuleSet : Set.S with type elt = RuleName.t = Set.Make (RuleName)
module LabelName : Uid.Id with type info = Uid.MarkedString.info = Uid.Make (Uid.MarkedString) ()
module LabelMap : Map.S with type key = LabelName.t = Map.Make (LabelName)
module LabelSet : Set.S with type elt = LabelName.t = Set.Make (LabelName)
(** Inside a scope, a definition can refer either to a scope def, or a subscope def *)
module ScopeDef = struct
type t =
@ -67,32 +73,35 @@ module ScopeDefSet : Set.S with type elt = ScopeDef.t = Set.Make (ScopeDef)
(** {1 AST} *)
type rule = {
just : Scopelang.Ast.expr Pos.marked Bindlib.box;
cons : Scopelang.Ast.expr Pos.marked Bindlib.box;
parameter : (Scopelang.Ast.Var.t * Scopelang.Ast.typ Pos.marked) option;
exception_to_rule : RuleName.t Pos.marked option;
rule_id : RuleName.t;
rule_just : Scopelang.Ast.expr Pos.marked Bindlib.box;
rule_cons : Scopelang.Ast.expr Pos.marked Bindlib.box;
rule_parameter : (Scopelang.Ast.Var.t * Scopelang.Ast.typ Pos.marked) option;
rule_exception_to_rules : RuleSet.t Pos.marked;
}
let empty_rule (pos : Pos.t) (have_parameter : Scopelang.Ast.typ Pos.marked option) : rule =
{
just = Bindlib.box (Scopelang.Ast.ELit (Dcalc.Ast.LBool false), pos);
cons = Bindlib.box (Scopelang.Ast.ELit Dcalc.Ast.LEmptyError, pos);
parameter =
rule_just = Bindlib.box (Scopelang.Ast.ELit (Dcalc.Ast.LBool false), pos);
rule_cons = Bindlib.box (Scopelang.Ast.ELit Dcalc.Ast.LEmptyError, pos);
rule_parameter =
(match have_parameter with
| Some typ -> Some (Scopelang.Ast.Var.make ("dummy", pos), typ)
| None -> None);
exception_to_rule = None;
rule_exception_to_rules = (RuleSet.empty, pos);
rule_id = RuleName.fresh ("empty", pos);
}
let always_false_rule (pos : Pos.t) (have_parameter : Scopelang.Ast.typ Pos.marked option) : rule =
{
just = Bindlib.box (Scopelang.Ast.ELit (Dcalc.Ast.LBool true), pos);
cons = Bindlib.box (Scopelang.Ast.ELit (Dcalc.Ast.LBool false), pos);
parameter =
rule_just = Bindlib.box (Scopelang.Ast.ELit (Dcalc.Ast.LBool true), pos);
rule_cons = Bindlib.box (Scopelang.Ast.ELit (Dcalc.Ast.LBool false), pos);
rule_parameter =
(match have_parameter with
| Some typ -> Some (Scopelang.Ast.Var.make ("dummy", pos), typ)
| None -> None);
exception_to_rule = None;
rule_exception_to_rules = (RuleSet.empty, pos);
rule_id = RuleName.fresh ("always_false", pos);
}
type assertion = Scopelang.Ast.expr Pos.marked Bindlib.box
@ -105,12 +114,19 @@ type meta_assertion =
| FixedBy of reference_typ Pos.marked
| VariesWith of unit * variation_typ Pos.marked option
type scope_def = {
scope_def_rules : rule RuleMap.t;
scope_def_typ : Scopelang.Ast.typ Pos.marked;
scope_def_is_condition : bool;
scope_def_visibility : Scopelang.Ast.visibility;
scope_def_label_groups : RuleSet.t LabelMap.t;
}
type scope = {
scope_vars : Scopelang.Ast.ScopeVarSet.t;
scope_sub_scopes : Scopelang.Ast.ScopeName.t Scopelang.Ast.SubScopeMap.t;
scope_uid : Scopelang.Ast.ScopeName.t;
scope_defs :
(rule RuleMap.t * Scopelang.Ast.typ Pos.marked * bool) (* is it a condition? *) ScopeDefMap.t;
scope_defs : scope_def ScopeDefMap.t;
scope_assertions : assertion list;
scope_meta_assertions : meta_assertion list;
}
@ -138,8 +154,8 @@ let free_variables (def : rule RuleMap.t) : Pos.t ScopeDefMap.t =
(fun _ rule acc ->
let locs =
Scopelang.Ast.LocationSet.union
(Scopelang.Ast.locations_used (Bindlib.unbox rule.just))
(Scopelang.Ast.locations_used (Bindlib.unbox rule.cons))
(Scopelang.Ast.locations_used (Bindlib.unbox rule.rule_just))
(Scopelang.Ast.locations_used (Bindlib.unbox rule.rule_cons))
in
add_locs acc locs)
def ScopeDefMap.empty

26
compiler/desugared/ast.mli
View File

@ -26,6 +26,12 @@ module RuleMap : Map.S with type key = RuleName.t
module RuleSet : Set.S with type elt = RuleName.t
module LabelName : Uid.Id with type info = Uid.MarkedString.info
module LabelMap : Map.S with type key = LabelName.t
module LabelSet : Set.S with type elt = LabelName.t
(** Inside a scope, a definition can refer either to a scope def, or a subscope def *)
module ScopeDef : sig
type t =
@ -48,10 +54,11 @@ module ScopeDefSet : Set.S with type elt = ScopeDef.t
(** {1 AST} *)
type rule = {
just : Scopelang.Ast.expr Pos.marked Bindlib.box;
cons : Scopelang.Ast.expr Pos.marked Bindlib.box;
parameter : (Scopelang.Ast.Var.t * Scopelang.Ast.typ Pos.marked) option;
exception_to_rule : RuleName.t Pos.marked option;
rule_id : RuleName.t;
rule_just : Scopelang.Ast.expr Pos.marked Bindlib.box;
rule_cons : Scopelang.Ast.expr Pos.marked Bindlib.box;
rule_parameter : (Scopelang.Ast.Var.t * Scopelang.Ast.typ Pos.marked) option;
rule_exception_to_rules : RuleSet.t Pos.marked;
}
val empty_rule : Pos.t -> Scopelang.Ast.typ Pos.marked option -> rule
@ -68,12 +75,19 @@ type meta_assertion =
| FixedBy of reference_typ Pos.marked
| VariesWith of unit * variation_typ Pos.marked option
type scope_def = {
scope_def_rules : rule RuleMap.t;
scope_def_typ : Scopelang.Ast.typ Pos.marked;
scope_def_is_condition : bool;
scope_def_visibility : Scopelang.Ast.visibility;
scope_def_label_groups : RuleSet.t LabelMap.t;
}
type scope = {
scope_vars : Scopelang.Ast.ScopeVarSet.t;
scope_sub_scopes : Scopelang.Ast.ScopeName.t Scopelang.Ast.SubScopeMap.t;
scope_uid : Scopelang.Ast.ScopeName.t;
scope_defs :
(rule RuleMap.t * Scopelang.Ast.typ Pos.marked * bool) (* is it a condition? *) ScopeDefMap.t;
scope_defs : scope_def ScopeDefMap.t;
scope_assertions : assertion list;
scope_meta_assertions : meta_assertion list;
}

102
compiler/desugared/dependency.ml
View File

@ -128,7 +128,8 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
in
let g =
Ast.ScopeDefMap.fold
(fun def_key (def, _, _) g ->
(fun def_key scope_def g ->
let def = scope_def.Ast.scope_def_rules in
let fv = Ast.free_variables def in
Ast.ScopeDefMap.fold
(fun fv_def fv_def_pos g ->
@ -186,7 +187,9 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
(** {2 Graph declaration} *)
module ExceptionVertex = struct
include Ast.RuleName
include Ast.RuleSet
let hash (x : t) : int = Ast.RuleSet.fold (fun r acc -> Int.logxor (Ast.RuleName.hash r) acc) x 0
let equal x y = compare x y = 0
end
@ -202,32 +205,84 @@ module ExceptionsSCC = Graph.Components.Make (ExceptionsDependencies)
let build_exceptions_graph (def : Ast.rule Ast.RuleMap.t) (def_info : Ast.ScopeDef.t) :
ExceptionsDependencies.t =
(* first we add the vertices *)
(* first we collect all the rule sets referred by exceptions *)
let all_rule_sets_pointed_to_by_exceptions : Ast.RuleSet.t list =
Ast.RuleMap.fold
(fun _rule_name rule acc ->
if Ast.RuleSet.is_empty (Pos.unmark rule.Ast.rule_exception_to_rules) then acc
else Pos.unmark rule.Ast.rule_exception_to_rules :: acc)
def []
in
(* we make sure these sets are either disjoint or equal ; should be a syntactic invariant since
you currently can't assign two labels to a single rule but an extra check is valuable since
this is a required invariant for the graph to be sound *)
List.iter
(fun rule_set1 ->
List.iter
(fun rule_set2 ->
if Ast.RuleSet.equal rule_set1 rule_set2 then ()
else if Ast.RuleSet.disjoint rule_set1 rule_set2 then ()
else
Errors.raise_multispanned_error
"Definitions or rules grouped by different labels overlap, whereas these groups \
shoule be disjoint"
(List.of_seq
(Seq.map
(fun rule ->
( Some "Rule or definition from the first group:",
Pos.get_position (Ast.RuleName.get_info rule) ))
(Ast.RuleSet.to_seq rule_set1))
@ List.of_seq
(Seq.map
(fun rule ->
( Some "Rule or definition from the second group:",
Pos.get_position (Ast.RuleName.get_info rule) ))
(Ast.RuleSet.to_seq rule_set2))))
all_rule_sets_pointed_to_by_exceptions)
all_rule_sets_pointed_to_by_exceptions;
(* Then we add the exception graph vertices by taking all those sets of rules pointed to by
exceptions, and adding the remaining rules not pointed as separate singleton set vertices *)
let g =
List.fold_left
(fun g rule_set -> ExceptionsDependencies.add_vertex g rule_set)
ExceptionsDependencies.empty all_rule_sets_pointed_to_by_exceptions
in
let g =
Ast.RuleMap.fold
(fun rule_name _ g -> ExceptionsDependencies.add_vertex g rule_name)
def ExceptionsDependencies.empty
(fun (rule_name : Ast.RuleName.t) _ g ->
if
List.exists
(fun rule_set_pointed_to_by_exceptions ->
Ast.RuleSet.mem rule_name rule_set_pointed_to_by_exceptions)
all_rule_sets_pointed_to_by_exceptions
then g
else ExceptionsDependencies.add_vertex g (Ast.RuleSet.singleton rule_name))
def g
in
(* then we add the edges *)
let g =
Ast.RuleMap.fold
(fun rule_name rule g ->
match rule.Ast.exception_to_rule with
| None -> g
| Some (exc_r, pos) ->
if ExceptionsDependencies.mem_vertex g exc_r then
if exc_r = rule_name then
Errors.raise_spanned_error "Cannot define rule as an exception to itself" pos
else
let edge = ExceptionsDependencies.E.create rule_name pos exc_r in
ExceptionsDependencies.add_edge_e g edge
else
Errors.raise_spanned_error
(Format.asprintf
"This rule has been declared as an exception to an incorrect label: this label \
is not attached to a definition of \"%a\""
Ast.ScopeDef.format_t def_info)
pos)
(* Right now, exceptions can only consist of one rule, we may want to relax that constraint
later in the development of Catala. *)
let exception_to_ruleset, pos = rule.Ast.rule_exception_to_rules in
if Ast.RuleSet.is_empty exception_to_ruleset then g (* we don't add an edge*)
else if ExceptionsDependencies.mem_vertex g exception_to_ruleset then
if exception_to_ruleset = Ast.RuleSet.singleton rule_name then
Errors.raise_spanned_error "Cannot define rule as an exception to itself" pos
else
let edge =
ExceptionsDependencies.E.create (Ast.RuleSet.singleton rule_name) pos
exception_to_ruleset
in
ExceptionsDependencies.add_edge_e g edge
else
Errors.raise_spanned_error
(Format.asprintf
"This rule has been declared as an exception to an incorrect label: this label is \
not attached to a definition of \"%a\""
Ast.ScopeDef.format_t def_info)
pos)
def g
in
g
@ -242,11 +297,12 @@ let check_for_exception_cycle (g : ExceptionsDependencies.t) : unit =
(Format.asprintf "Cyclic dependency detected between exceptions!")
(List.flatten
(List.map
(fun (v : Ast.RuleName.t) ->
(fun (vs : Ast.RuleSet.t) ->
let v = Ast.RuleSet.choose vs in
let var_str, var_info =
(Format.asprintf "%a" Ast.RuleName.format_t v, Ast.RuleName.get_info v)
in
let succs = ExceptionsDependencies.succ_e g v in
let succs = ExceptionsDependencies.succ_e g vs in
let _, edge_pos, _ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
[
( Some

2
compiler/desugared/dependency.mli
View File

@ -61,7 +61,7 @@ val build_scope_dependencies : Ast.scope -> ScopeDependencies.t
(** {1 Exceptions dependency graph} *)
module ExceptionsDependencies : Graph.Sig.P with type V.t = Ast.RuleName.t and type E.label = Edge.t
module ExceptionsDependencies : Graph.Sig.P with type V.t = Ast.RuleSet.t and type E.label = Edge.t
val build_exceptions_graph : Ast.rule Ast.RuleMap.t -> Ast.ScopeDef.t -> ExceptionsDependencies.t

26
compiler/desugared/desugared.mld
View File

@ -1,9 +1,9 @@
{0 Desugared representation }
This representation is the second in the compilation chain
(see {{: index.html#architecture} Architecture}). Its main difference
with {{: surface.html} the surface representation} is that the legislative
text has been discarded and all the definitions of each variables have been
This representation is the second in the compilation chain
(see {{: index.html#architecture} Architecture}). Its main difference
with {{: surface.html} the surface representation} is that the legislative
text has been discarded and all the definitions of each variables have been
collected in the same place rather than being scattered across the code base.
The module describing the abstract syntax tree is:
@ -12,19 +12,19 @@ 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
a scope, there is no computational circular dependency between the variables
of the scope. When the dependency graph is a DAG,
{!module: Desugared.Desugared_to_scope} performs a topological ordering to
produce an ordered list of the scope definitions compatible with the
computation order. All the graph computations are done using the
{!module: Desugared.Desugared_to_scope} performs a topological ordering to
produce an ordered list of the scope definitions compatible with the
computation order. All the graph computations are done using the
{{:http://ocamlgraph.lri.fr/} Ocamlgraph} library.
The other important piece of work performed by
{!module: Desugared.Desugared_to_scope} is the construction of the default trees
(see {!constructor: Dcalc.Ast.EDefault}) from the list of prioritized rules.
(see {!Dcalc.Ast.EDefault}) from the list of prioritized rules.
Related modules:
{!modules: Desugared.Dependency Desugared.Desugared_to_scope}

142
compiler/desugared/desugared_to_scope.ml
View File

@ -18,7 +18,11 @@ open Utils
(** {1 Rule tree construction} *)
type rule_tree = Leaf of Ast.rule | Node of rule_tree list * Ast.rule
(** Intermediate representation for the exception tree of rules for a particular scope definition. *)
type rule_tree =
| Leaf of Ast.rule list (** Rules defining a base case piecewise. List is non-empty. *)
| Node of rule_tree list * Ast.rule list
(** A list of exceptions to a non-empty list of rules defining a base case piecewise. *)
(** Transforms a flat list of rules into a tree, taking into account the priorities declared between
rules *)
@ -33,11 +37,14 @@ let def_map_to_tree (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t) :
else base_cases)
exc_graph []
in
let rec build_tree (base_case : Ast.RuleName.t) : rule_tree =
let exceptions = Dependency.ExceptionsDependencies.pred exc_graph base_case in
let rec build_tree (base_cases : Ast.RuleSet.t) : rule_tree =
let exceptions = Dependency.ExceptionsDependencies.pred exc_graph base_cases in
let base_case_as_rule_list =
List.map (fun r -> Ast.RuleMap.find r def) (List.of_seq (Ast.RuleSet.to_seq base_cases))
in
match exceptions with
| [] -> Leaf (Ast.RuleMap.find base_case def)
| _ -> Node (List.map build_tree exceptions, Ast.RuleMap.find base_case def)
| [] -> Leaf base_case_as_rule_list
| _ -> Node (List.map build_tree exceptions, base_case_as_rule_list)
in
List.map build_tree base_cases
@ -47,14 +54,14 @@ let def_map_to_tree (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t) :
let rec rule_tree_to_expr ~(toplevel : bool) (def_pos : Pos.t)
(is_func : Scopelang.Ast.Var.t option) (tree : rule_tree) :
Scopelang.Ast.expr Pos.marked Bindlib.box =
let exceptions, rule =
let exceptions, base_rules =
match tree with Leaf r -> ([], r) | Node (exceptions, r) -> (exceptions, r)
in
(* because each rule has its own variable parameter and we want to convert the whole rule tree
into a function, we need to perform some alpha-renaming of all the expressions *)
let substitute_parameter (e : Scopelang.Ast.expr Pos.marked Bindlib.box) :
let substitute_parameter (e : Scopelang.Ast.expr Pos.marked Bindlib.box) (rule : Ast.rule) :
Scopelang.Ast.expr Pos.marked Bindlib.box =
match (is_func, rule.parameter) with
match (is_func, rule.Ast.rule_parameter) with
| Some new_param, Some (old_param, _) ->
let binder = Bindlib.bind_var old_param e in
Bindlib.box_apply2
@ -64,18 +71,39 @@ let rec rule_tree_to_expr ~(toplevel : bool) (def_pos : Pos.t)
| _ -> assert false
(* should not happen *)
in
let just = substitute_parameter rule.Ast.just in
let cons = substitute_parameter rule.Ast.cons in
let base_just_list =
List.map (fun rule -> substitute_parameter rule.Ast.rule_just rule) base_rules
in
let base_cons_list =
List.map (fun rule -> substitute_parameter rule.Ast.rule_cons rule) base_rules
in
let default_containing_base_cases =
Bindlib.box_apply2
(fun base_just_list base_cons_list ->
( Scopelang.Ast.EDefault
( List.map2
(fun base_just base_cons ->
(Scopelang.Ast.EDefault ([], base_just, base_cons), Pos.get_position base_just))
base_just_list base_cons_list,
(Scopelang.Ast.ELit (Dcalc.Ast.LBool false), def_pos),
(Scopelang.Ast.ELit Dcalc.Ast.LEmptyError, def_pos) ),
def_pos ))
(Bindlib.box_list base_just_list) (Bindlib.box_list base_cons_list)
in
let exceptions =
Bindlib.box_list (List.map (rule_tree_to_expr ~toplevel:false def_pos is_func) exceptions)
in
let default =
Bindlib.box_apply3
(fun exceptions just cons ->
(Scopelang.Ast.EDefault (exceptions, just, cons), Pos.get_position just))
exceptions just cons
Bindlib.box_apply2
(fun exceptions default_containing_base_cases ->
( Scopelang.Ast.EDefault
( exceptions,
(Scopelang.Ast.ELit (Dcalc.Ast.LBool true), def_pos),
default_containing_base_cases ),
def_pos ))
exceptions default_containing_base_cases
in
match (is_func, rule.parameter) with
match (is_func, (List.hd base_rules).Ast.rule_parameter) with
| None, None -> default
| Some new_param, Some (_, typ) ->
if toplevel then
@ -96,13 +124,15 @@ let rec rule_tree_to_expr ~(toplevel : bool) (def_pos : Pos.t)
(** Translates a definition inside a scope, the resulting expression should be an {!constructor:
Dcalc.Ast.EDefault} *)
let translate_def (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t)
(typ : Scopelang.Ast.typ Pos.marked) (is_cond : bool) : Scopelang.Ast.expr Pos.marked =
(typ : Scopelang.Ast.typ Pos.marked) ~(is_cond : bool) ~(is_subscope_var : bool) :
Scopelang.Ast.expr Pos.marked =
(* Here, we have to transform this list of rules into a default tree. *)
let is_func _ (r : Ast.rule) : bool = Option.is_some r.Ast.parameter in
let all_rules_func = Ast.RuleMap.for_all is_func def in
let all_rules_not_func = Ast.RuleMap.for_all (fun n r -> not (is_func n r)) def in
let is_def_func : Scopelang.Ast.typ Pos.marked option =
if all_rules_func && Ast.RuleMap.cardinal def > 0 then
let is_def_func = match Pos.unmark typ with Scopelang.Ast.TArrow (_, _) -> true | _ -> false in
let is_rule_func _ (r : Ast.rule) : bool = Option.is_some r.Ast.rule_parameter in
let all_rules_func = Ast.RuleMap.for_all is_rule_func def in
let all_rules_not_func = Ast.RuleMap.for_all (fun n r -> not (is_rule_func n r)) def in
let is_def_func_param_typ : Scopelang.Ast.typ Pos.marked option =
if is_def_func && all_rules_func then
match Pos.unmark typ with
| Scopelang.Ast.TArrow (t_param, _) -> Some t_param
| _ ->
@ -111,33 +141,52 @@ let translate_def (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t)
"The definitions of %a are function but its type, %a, is not a function type"
Ast.ScopeDef.format_t def_info Scopelang.Print.format_typ typ)
(Pos.get_position typ)
else if all_rules_not_func then None
else if (not is_def_func) && all_rules_not_func then None
else
Errors.raise_multispanned_error
"some definitions of the same variable are functions while others aren't"
(List.map
(fun (_, r) ->
(Some "This definition is a function:", Pos.get_position (Bindlib.unbox r.Ast.cons)))
(Ast.RuleMap.bindings (Ast.RuleMap.filter is_func def))
( Some "This definition is a function:",
Pos.get_position (Bindlib.unbox r.Ast.rule_cons) ))
(Ast.RuleMap.bindings (Ast.RuleMap.filter is_rule_func def))
@ List.map
(fun (_, r) ->
( Some "This definition is not a function:",
Pos.get_position (Bindlib.unbox r.Ast.cons) ))
(Ast.RuleMap.bindings (Ast.RuleMap.filter (fun n r -> not (is_func n r)) def)))
Pos.get_position (Bindlib.unbox r.Ast.rule_cons) ))
(Ast.RuleMap.bindings (Ast.RuleMap.filter (fun n r -> not (is_rule_func n r)) def)))
in
let top_list = def_map_to_tree def_info def in
let top_value =
(if is_cond then Ast.always_false_rule else Ast.empty_rule) Pos.no_pos is_def_func
(if is_cond then Ast.always_false_rule else Ast.empty_rule) Pos.no_pos is_def_func_param_typ
in
Bindlib.unbox
(rule_tree_to_expr ~toplevel:true
(Ast.ScopeDef.get_position def_info)
(Option.map (fun _ -> Scopelang.Ast.Var.make ("param", Pos.no_pos)) is_def_func)
(match top_list with
| [] ->
(* In this case, there are no rules to define the expression *)
Leaf top_value
| _ -> Node (top_list, top_value)))
if
Ast.RuleMap.cardinal def = 0 && is_subscope_var
(* Here we have a special case for the empty definitions. Indeed, we could use the code for the
regular case below that would create a convoluted default always returning empty error, and
this would be correct. But it gets more complicated with functions. Indeed, if we create an
empty definition for a subscope argument whose type is a function, we get something like [fun
() -> (fun real_param -> < ... >)] that is passed as an argument to the subscope. The
sub-scope de-thunks but the de-thunking does not return empty error, signalling there is not
reentrant variable, because functions are values! So the subscope does not see that there is
not reentrant variable and does not pick its internal definition instead. See
[test/test_scope/subscope_function_arg_not_defined.catala_en] for a test case exercising that
subtlety.
To avoid this complication we special case here and put an empty error for all subscope
variables that are not defined. It covers the subtlety with functions described above but
also conditions with the false default value. *)
then (ELit LEmptyError, Pos.no_pos)
else
Bindlib.unbox
(rule_tree_to_expr ~toplevel:true
(Ast.ScopeDef.get_position def_info)
(Option.map (fun _ -> Scopelang.Ast.Var.make ("param", Pos.no_pos)) is_def_func_param_typ)
(match top_list with
| [] ->
(* In this case, there are no rules to define the expression *)
Leaf [ top_value ]
| _ -> Node (top_list, [ top_value ])))
(** Translates a scope *)
let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl =
@ -150,10 +199,14 @@ let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl =
(fun vertex ->
match vertex with
| Dependency.Vertex.Var (var : Scopelang.Ast.ScopeVar.t) ->
let var_def, var_typ, is_cond =
Ast.ScopeDefMap.find (Ast.ScopeDef.Var var) scope.scope_defs
let scope_def = Ast.ScopeDefMap.find (Ast.ScopeDef.Var var) scope.scope_defs in
let var_def = scope_def.scope_def_rules in
let var_typ = scope_def.scope_def_typ in
let is_cond = scope_def.scope_def_is_condition in
let expr_def =
translate_def (Ast.ScopeDef.Var var) var_def var_typ ~is_cond
~is_subscope_var:false
in
let expr_def = translate_def (Ast.ScopeDef.Var var) var_def var_typ is_cond in
[
Scopelang.Ast.Definition
( ( Scopelang.Ast.ScopeVar
@ -170,11 +223,16 @@ let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl =
in
let sub_scope_vars_redefs =
Ast.ScopeDefMap.mapi
(fun def_key (def, def_typ, is_cond) ->
(fun def_key scope_def ->
let def = scope_def.Ast.scope_def_rules in
let def_typ = scope_def.scope_def_typ in
let is_cond = scope_def.scope_def_is_condition in
match def_key with
| Ast.ScopeDef.Var _ -> assert false (* should not happen *)
| Ast.ScopeDef.SubScopeVar (_, sub_scope_var) ->
let expr_def = translate_def def_key def def_typ is_cond in
let expr_def =
translate_def def_key def def_typ ~is_cond ~is_subscope_var:true
in
let subscop_real_name =
Scopelang.Ast.SubScopeMap.find sub_scope_index scope.scope_sub_scopes
in
@ -211,7 +269,7 @@ let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl =
let scope_sig =
Scopelang.Ast.ScopeVarSet.fold
(fun var acc ->
let _, typ, _ = Ast.ScopeDefMap.find (Ast.ScopeDef.Var var) scope.scope_defs in
let typ = (Ast.ScopeDefMap.find (Ast.ScopeDef.Var var) scope.scope_defs).scope_def_typ in
Scopelang.Ast.ScopeVarMap.add var typ acc)
scope.scope_vars Scopelang.Ast.ScopeVarMap.empty
in

41
compiler/driver.ml
View File

@ -19,7 +19,7 @@ module Pos = Utils.Pos
(** Associates a {!type: Cli.backend_lang} with its string represtation. *)
let languages = [ ("en", Cli.En); ("fr", Cli.Fr); ("pl", Cli.Pl) ]
(** Associates a file extension with its corresponding {!type: Cli.frontend_lang} string
(** Associates a file extension with its corresponding {!type: Cli.backend_lang} string
representation. *)
let extensions = [ (".catala_fr", "fr"); (".catala_en", "en"); (".catala_pl", "pl") ]
@ -27,13 +27,15 @@ let extensions = [ (".catala_fr", "fr"); (".catala_en", "en"); (".catala_pl", "p
[driver source_file debug dcalc unstyled wrap_weaved_output backend language max_prec_digits trace optimize scope_to_execute output_file]*)
let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
(wrap_weaved_output : bool) (avoid_exceptions : bool) (backend : string)
(language : string option) (max_prec_digits : int option) (trace : bool) (optimize : bool)
(ex_scope : string option) (output_file : string option) : int =
(language : string option) (max_prec_digits : int option) (trace : bool)
(disable_counterexamples : bool) (optimize : bool) (ex_scope : string option)
(output_file : string option) : int =
try
Cli.debug_flag := debug;
Cli.style_flag := not unstyled;
Cli.trace_flag := trace;
Cli.optimize_flag := optimize;
Cli.disable_counterexamples := disable_counterexamples;
Cli.debug_print "Reading files...";
let filename = ref "" in
(match source_file with FileName f -> filename := f | Contents c -> Cli.contents := c);
@ -64,11 +66,13 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
if backend = "makefile" then Cli.Makefile
else if backend = "latex" then Cli.Latex
else if backend = "html" then Cli.Html
else if backend = "interpret" then Cli.Run
else if backend = "interpret" then Cli.Interpret
else if backend = "ocaml" then Cli.OCaml
else if backend = "dcalc" then Cli.Dcalc
else if backend = "scopelang" then Cli.Scopelang
else if backend = "python" then Cli.Python
else if backend = "proof" then Cli.Proof
else if backend = "typecheck" then Cli.Typecheck
else
Errors.raise_error
(Printf.sprintf "The selected backend (%s) is not supported by Catala" backend)
@ -150,7 +154,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
let ctxt = Surface.Name_resolution.form_context prgm in
let scope_uid =
match (ex_scope, backend) with
| None, Cli.Run -> Errors.raise_error "No scope was provided for execution."
| None, Cli.Interpret -> Errors.raise_error "No scope was provided for execution."
| None, _ ->
snd
(try Desugared.Ast.IdentMap.choose ctxt.scope_idmap
@ -184,6 +188,13 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
end;
Cli.debug_print "Translating to default calculus...";
let prgm, type_ordering = Scopelang.Scope_to_dcalc.translate_program prgm in
let prgm =
if optimize then begin
Cli.debug_print "Optimizing default calculus...";
Dcalc.Optimizations.optimize_program prgm
end
else prgm
in
let prgrm_dcalc_expr = Bindlib.unbox (Dcalc.Ast.build_whole_program_expr prgm scope_uid) in
if backend = Cli.Dcalc then begin
let fmt, at_end =
@ -207,7 +218,15 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
(* Cli.debug_print (Format.asprintf "Typechecking results :@\n%a" (Dcalc.Print.format_typ
prgm.decl_ctx) typ); *)
match backend with
| Cli.Run ->
| Cli.Typecheck ->
(* That's it! *)
Cli.result_print "Typechecking successful!";
0
| Cli.Proof ->
let vcs = Verification.Conditions.generate_verification_conditions prgm in
Verification.Solver.solve_vc prgm prgm.decl_ctx vcs;
0
| Cli.Interpret ->
Cli.debug_print "Starting interpretation...";
let results = Dcalc.Interpreter.interpret_program prgm.decl_ctx prgrm_dcalc_expr in
let out_regex = Re.Pcre.regexp "\\_out$" in
@ -279,9 +298,13 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
0
| _ -> assert false
(* should not happen *))
with Errors.StructuredError (msg, pos) ->
Cli.error_print (Errors.print_structured_error msg pos);
-1
with
| Errors.StructuredError (msg, pos) ->
Cli.error_print (Errors.print_structured_error msg pos);
-1
| Sys_error msg ->
Cli.error_print ("System error: " ^ msg);
-1
let main () =
let return_code = Cmdliner.Term.eval (Cli.catala_t (fun f -> driver (FileName f)), Cli.info) in

11
compiler/dune
View File

@ -1,7 +1,16 @@
(library
(name driver)
(public_name catala.driver)
(libraries utils surface desugared literate dcalc lcalc scalc runtime)
(libraries
utils
surface
desugared
literate
dcalc
lcalc
scalc
runtime
verification)
(modules driver))
(library

30
compiler/index.mld
View File

@ -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,12 +85,20 @@ 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.html} The statement calculus}}
}
The main compilation chain is defined in:
{!modules: Driver}
Additionally, the compiler features a verification plugin that generates
verification condition for proof backends. More information can be found here:
{ul
{li {{: verification.html} Verification}}
}
Last, two more modules contain additional features for the compiler:
{ul

2
compiler/lcalc/backends.mli
View File

@ -12,6 +12,8 @@
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Helper functions common to all Catala compiler backends *)
val to_ascii : string -> string
(** Removes all non-ASCII diacritics from a string by converting them to their base letter in the
Latin alphabet *)

14
compiler/lcalc/lcalc.mld
View File

@ -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.
{1 Backends}
Related modules:
{!modules: Lcalc.To_ocaml Lcalc.To_python Lcalc.Backends}
{!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}

18
compiler/lcalc/print.ml
View File

@ -49,11 +49,10 @@ let format_uid_list (fmt : Format.formatter) (infos : Uid.MarkedString.info list
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ".")
(fun fmt info ->
Format.fprintf fmt "%s"
(Utils.Cli.print_with_style
(if begins_with_uppercase (Pos.unmark info) then [ ANSITerminal.red ] else [])
"%s"
(Format.asprintf "%a" Utils.Uid.MarkedString.format_info info))))
Format.fprintf fmt "%a"
(Utils.Cli.format_with_style
(if begins_with_uppercase (Pos.unmark info) then [ ANSITerminal.red ] else []))
(Format.asprintf "%a" Utils.Uid.MarkedString.format_info info)))
infos
let format_exception (fmt : Format.formatter) (exn : except) : unit =
@ -65,10 +64,10 @@ let format_exception (fmt : Format.formatter) (exn : except) : unit =
| NoValueProvided -> "NoValueProvided")
let format_keyword (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%s" (Utils.Cli.print_with_style [ ANSITerminal.red ] "%s" s)
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.red ]) s
let format_punctuation (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%s" (Utils.Cli.print_with_style [ ANSITerminal.cyan ] "%s" s)
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.cyan ]) s
let needs_parens (e : expr Pos.marked) : bool =
match Pos.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false
@ -159,7 +158,8 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e : exp
| EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1 Dcalc.Print.format_binop
(op, Pos.no_pos) format_with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [ arg1 ]) -> Format.fprintf fmt "%a" format_with_parens arg1
| EApp ((EOp (Unop (Log _)), _), [ arg1 ]) when not !Cli.debug_flag ->
Format.fprintf fmt "%a" format_with_parens arg1
| EApp ((EOp (Unop op), _), [ arg1 ]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" Dcalc.Print.format_unop (op, Pos.no_pos)
format_with_parens arg1
@ -176,7 +176,7 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e : exp
| ECatch (e1, exn, e2) ->
Format.fprintf fmt "@[<hov 2>try@ %a@ with@ %a ->@ %a@]" format_with_parens e1
format_exception exn format_with_parens e2
| ERaise exn -> Format.fprintf fmt "raise@ %a" format_exception exn
| ERaise exn -> Format.fprintf fmt "@[<hov 2>raise@ %a@]" format_exception exn
| EAssert e' ->
Format.fprintf fmt "@[<hov 2>%a@ %a%a%a@]" format_keyword "assert" format_punctuation "("
format_expr e' format_punctuation ")"

47
compiler/literate/latex.ml
View File

@ -24,16 +24,17 @@ module C = Cli
(** {1 Helpers} *)
(** Espaces various LaTeX-sensitive characters *)
let pre_latexify (s : string) =
let percent = R.regexp "%" in
let s = R.substitute ~rex:percent ~subst:(fun _ -> "\\%") s in
let dollar = R.regexp "\\$" in
let s = R.substitute ~rex:dollar ~subst:(fun _ -> "\\$") s in
let premier = R.regexp "1er" in
let s = R.substitute ~rex:premier ~subst:(fun _ -> "1\\textsuperscript{er}") s in
let underscore = R.regexp "\\_" in
let s = R.substitute ~rex:underscore ~subst:(fun _ -> "\\_") s in
s
let pre_latexify (s : string) : string =
let substitute s (old_s, new_s) = R.substitute ~rex:(R.regexp old_s) ~subst:(fun _ -> new_s) s in
[
("\\$", "\\$");
("%", "\\%");
("\\_", "\\_");
("\\#", "\\#");
("1er", "1\\textsuperscript{er}");
("\\^", "\\textasciicircum");
]
|> List.fold_left substitute s
(** Usage: [wrap_latex source_files custom_pygments language fmt wrapped]
@ -41,11 +42,11 @@ let pre_latexify (s : string) =
let wrap_latex (source_files : string list) (language : C.backend_lang) (fmt : Format.formatter)
(wrapped : Format.formatter -> unit) =
Format.fprintf fmt
"\\documentclass[11pt, a4paper]{article}\n\n\
"\\documentclass[%s, 11pt, a4paper]{article}\n\n\
\\usepackage[T1]{fontenc}\n\
\\usepackage[utf8]{inputenc}\n\
\\usepackage{amssymb}\n\
\\usepackage[%s]{babel}\n\
\\usepackage{babel}\n\
\\usepackage{lmodern}\n\
\\usepackage{minted}\n\
\\usepackage{newunicodechar}\n\
@ -101,22 +102,6 @@ let wrap_latex (source_files : string list) (language : C.backend_lang) (fmt : F
wrapped fmt;
Format.fprintf fmt "\n\n\\end{document}"
(** Replaces math operators by their nice unicode counterparts *)
let math_syms_replace (c : string) : string =
let date = "\\d\\d/\\d\\d/\\d\\d\\d\\d" in
let syms = R.regexp (date ^ "|!=|<=|>=|--|->|\\*|/") in
let syms2cmd = function
| "!=" -> "≠"
| "<=" -> "≤"
| ">=" -> "≥"
| "--" -> "—"
| "->" -> "→"
| "*" -> "×"
| "/" -> "÷"
| s -> s
in
R.substitute ~rex:syms ~subst:syms2cmd c
(** {1 Weaving} *)
let rec law_structure_to_latex (language : C.backend_lang) (fmt : Format.formatter)
@ -152,8 +137,7 @@ let rec law_structure_to_latex (language : C.backend_lang) (fmt : Format.formatt
\\end{minted}"
(pre_latexify (Filename.basename (Pos.get_file (Pos.get_position c))))
(Pos.get_start_line (Pos.get_position c) - 1)
(get_language_extension language)
(math_syms_replace (Pos.unmark c))
(get_language_extension language) (Pos.unmark c)
| A.CodeBlock (_, c, true) ->
let metadata_title =
match language with Fr -> "Métadonnées" | En -> "Metadata" | Pl -> "Metadane"
@ -170,8 +154,7 @@ let rec law_structure_to_latex (language : C.backend_lang) (fmt : Format.formatt
metadata_title metadata_title
(Pos.get_start_line (Pos.get_position c) - 1)
(pre_latexify (Filename.basename (Pos.get_file (Pos.get_position c))))
(get_language_extension language)
(math_syms_replace (Pos.unmark c))
(get_language_extension language) (Pos.unmark c)
(** {1 API} *)

8
compiler/literate/literate.mld
View File

@ -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.

21
compiler/scalc/compile_from_lambda.ml
View File

@ -197,15 +197,22 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) : A.bloc
let s_e_catch = translate_statements ctxt e_catch in
[ (A.STryExcept (s_e_try, except, s_e_catch), Pos.get_position block_expr) ]
| L.ERaise except -> [ (A.SRaise except, Pos.get_position block_expr) ]
| _ ->
| _ -> (
let e_stmts, new_e = translate_expr ctxt block_expr in
e_stmts
@ [
( (match ctxt.inside_definition_of with
| None -> A.SReturn (Pos.unmark new_e)
| Some x -> A.SLocalDef (Pos.same_pos_as x new_e, new_e)),
Pos.get_position block_expr );
]
@
match e_stmts with
| (A.SRaise _, _) :: _ ->
(* if the last statement raises an exception, then we don't need to return or to define
the current variable since this code will be unreachable *)
[]
| _ ->
[
( (match ctxt.inside_definition_of with
| None -> A.SReturn (Pos.unmark new_e)
| Some x -> A.SLocalDef (Pos.same_pos_as x new_e, new_e)),
Pos.get_position block_expr );
])
let translate_scope (decl_ctx : D.decl_ctx) (func_dict : A.TopLevelName.t L.VarMap.t)
(scope_expr : L.expr Pos.marked) : (A.LocalName.t Pos.marked * D.typ Pos.marked) list * A.block

13
compiler/scalc/scalc.mld
View File

@ -8,22 +8,21 @@ 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:
{!modules: Lcalc.To_python}
{!modules: Scalc.To_python}

108
compiler/scalc/to_python.ml
View File

@ -192,15 +192,13 @@ let rec format_expression (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e
| EVar v -> format_var fmt v
| EFunc f -> format_toplevel_name fmt f
| EStruct (es, s) ->
if List.length es = 0 then failwith "should not happen"
else
Format.fprintf fmt "%a(%a)" format_struct_name s
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(fun fmt (e, struct_field) ->
Format.fprintf fmt "%a = %a" format_struct_field_name struct_field
(format_expression ctx) e))
(List.combine es (List.map fst (Dcalc.Ast.StructMap.find s ctx.ctx_structs)))
Format.fprintf fmt "%a(%a)" format_struct_name s
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(fun fmt (e, struct_field) ->
Format.fprintf fmt "%a = %a" format_struct_field_name struct_field
(format_expression ctx) e))
(List.combine es (List.map fst (Dcalc.Ast.StructMap.find s ctx.ctx_structs)))
| EStructFieldAccess (e1, field, _) ->
Format.fprintf fmt "%a.%a" (format_expression ctx) e1 format_struct_field_name field
| EInj (e, cons, enum_name) ->
@ -299,52 +297,52 @@ and format_block (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (b : block)
let format_ctx (type_ordering : Scopelang.Dependency.TVertex.t list) (fmt : Format.formatter)
(ctx : D.decl_ctx) : unit =
let format_struct_decl fmt (struct_name, struct_fields) =
if List.length struct_fields = 0 then failwith "no fields in the struct"
else
Format.fprintf fmt
"class %a:@\n\
\tdef __init__(self, %a) -> None:@\n\
%a@\n\
@\n\
\tdef __eq__(self, other: object) -> bool:@\n\
\t\tif isinstance(other, %a):@\n\
\t\t\treturn @[<hov>(%a)@]@\n\
\t\telse:@\n\
\t\t\treturn False@\n\
@\n\
\tdef __ne__(self, other: object) -> bool:@\n\
\t\treturn not (self == other)@\n\
@\n\
\tdef __str__(self) -> str:@\n\
\t\t@[<hov 4>return \"%a(%a)\".format(%a)@]" format_struct_name struct_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
(fun _fmt (struct_field, struct_field_type) ->
Format.fprintf fmt "%a: %a" format_struct_field_name struct_field format_typ
struct_field_type))
struct_fields
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun _fmt (struct_field, _) ->
Format.fprintf fmt "\t\tself.%a = %a" format_struct_field_name struct_field
format_struct_field_name struct_field))
struct_fields format_struct_name struct_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " and@ ")
(fun _fmt (struct_field, _) ->
Format.fprintf fmt "self.%a == other.%a" format_struct_field_name struct_field
format_struct_field_name struct_field))
struct_fields format_struct_name struct_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",")
(fun _fmt (struct_field, _) ->
Format.fprintf fmt "%a={}" format_struct_field_name struct_field))
struct_fields
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(fun _fmt (struct_field, _) ->
Format.fprintf fmt "self.%a" format_struct_field_name struct_field))
struct_fields
Format.fprintf fmt
"class %a:@\n\
\tdef __init__(self, %a) -> None:@\n\
%a@\n\
@\n\
\tdef __eq__(self, other: object) -> bool:@\n\
\t\tif isinstance(other, %a):@\n\
\t\t\treturn @[<hov>(%a)@]@\n\
\t\telse:@\n\
\t\t\treturn False@\n\
@\n\
\tdef __ne__(self, other: object) -> bool:@\n\
\t\treturn not (self == other)@\n\
@\n\
\tdef __str__(self) -> str:@\n\
\t\t@[<hov 4>return \"%a(%a)\".format(%a)@]" format_struct_name struct_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
(fun _fmt (struct_field, struct_field_type) ->
Format.fprintf fmt "%a: %a" format_struct_field_name struct_field format_typ
struct_field_type))
struct_fields
(if List.length struct_fields = 0 then fun fmt _ -> Format.fprintf fmt "\t\tpass"
else
Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun _fmt (struct_field, _) ->
Format.fprintf fmt "\t\tself.%a = %a" format_struct_field_name struct_field
format_struct_field_name struct_field))
struct_fields format_struct_name struct_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " and@ ")
(fun _fmt (struct_field, _) ->
Format.fprintf fmt "self.%a == other.%a" format_struct_field_name struct_field
format_struct_field_name struct_field))
struct_fields format_struct_name struct_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",")
(fun _fmt (struct_field, _) ->
Format.fprintf fmt "%a={}" format_struct_field_name struct_field))
struct_fields
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(fun _fmt (struct_field, _) ->
Format.fprintf fmt "self.%a" format_struct_field_name struct_field))
struct_fields
in
let format_enum_decl fmt (enum_name, enum_cons) =
if List.length enum_cons = 0 then failwith "no constructors in the enum"

2
compiler/scopelang/ast.ml
View File

@ -123,6 +123,8 @@ type rule =
| Assertion of expr Pos.marked
| Call of ScopeName.t * SubScopeName.t
type visibility = { visibility_output : bool; visibility_input : bool }
type scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : typ Pos.marked ScopeVarMap.t;

5
compiler/scopelang/ast.mli
View File

@ -89,6 +89,11 @@ type rule =
| Assertion of expr Pos.marked
| Call of ScopeName.t * SubScopeName.t
type visibility = {
visibility_output : bool; (** True if present in the scope's output *)
visibility_input : bool; (** True if present in the scope's input (reentrant) *)
}
type scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : typ Pos.marked ScopeVarMap.t;

4
compiler/scopelang/print.ml
View File

@ -169,10 +169,12 @@ let format_scope (fmt : Format.formatter) ((name, decl) : ScopeName.t * scope_de
decl.scope_decl_rules
let format_program (fmt : Format.formatter) (p : program) : unit =
Format.fprintf fmt "%a@\n@\n%a@\n@\n%a"
Format.fprintf fmt "%a%s%a%s%a"
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n@\n") format_struct)
(StructMap.bindings p.program_structs)
(if StructMap.is_empty p.program_structs then "" else "\n\n")
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n@\n") format_enum)
(EnumMap.bindings p.program_enums)
(if EnumMap.is_empty p.program_enums then "" else "\n\n")
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n@\n") format_scope)
(ScopeMap.bindings p.program_scopes)

132
compiler/scopelang/scope_to_dcalc.ml
View File

@ -14,14 +14,22 @@
open Utils
type scope_sigs_ctx =
(* list of scope variables with their types *)
((Ast.ScopeVar.t * Dcalc.Ast.typ) list
* (* var representing the scope *) Dcalc.Ast.Var.t
* (* var representing the scope input inside the scope func *) Dcalc.Ast.Var.t
* (* scope input *) Ast.StructName.t
* (* scope output *) Ast.StructName.t)
Ast.ScopeMap.t
type scope_var_ctx = {
scope_var_name : Ast.ScopeVar.t;
scope_var_typ : Dcalc.Ast.typ;
scope_var_visibility : Ast.visibility;
}
type scope_sig_ctx = {
scope_sig_local_vars : scope_var_ctx list; (** List of scope variables *)
scope_sig_scope_var : Dcalc.Ast.Var.t; (** Var representing the scope *)
scope_sig_input_var : Dcalc.Ast.Var.t;
(** Var representing the scope input inside the scope func *)
scope_sig_input_struct : Ast.StructName.t; (** Scope input *)
scope_sig_output_struct : Ast.StructName.t; (** Scope output *)
}
type scope_sigs_ctx = scope_sig_ctx Ast.ScopeMap.t
type ctx = {
structs : Ast.struct_ctx;
@ -359,13 +367,11 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
ctx.subscope_vars;
} )
| Call (subname, subindex) ->
let ( all_subscope_vars,
scope_dcalc_var,
_,
called_scope_input_struct,
called_scope_return_struct ) =
Ast.ScopeMap.find subname ctx.scopes_parameters
in
let subscope_sig = Ast.ScopeMap.find subname ctx.scopes_parameters in
let all_subscope_vars = subscope_sig.scope_sig_local_vars in
let scope_dcalc_var = subscope_sig.scope_sig_scope_var in
let called_scope_input_struct = subscope_sig.scope_sig_input_struct in
let called_scope_return_struct = subscope_sig.scope_sig_output_struct in
let subscope_vars_defined =
try Ast.SubScopeMap.find subindex ctx.subscope_vars
with Not_found -> Ast.ScopeVarMap.empty
@ -376,11 +382,14 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
let pos_call = Pos.get_position (Ast.SubScopeName.get_info subindex) in
let subscope_args =
List.map
(fun (subvar, _) ->
if subscope_var_not_yet_defined subvar then
Bindlib.box Dcalc.Interpreter.empty_thunked_term
(fun (subvar : scope_var_ctx) ->
if subscope_var_not_yet_defined subvar.scope_var_name then
(* This is a redundant check. Normally, all subscope varaibles should have been
defined (even an empty definition, if they're not defined by any rule in the source
code) by the translation from desugared to the scope language. *)
Bindlib.box Dcalc.Ast.empty_thunked_term
else
let a_var, _ = Ast.ScopeVarMap.find subvar subscope_vars_defined in
let a_var, _ = Ast.ScopeVarMap.find subvar.scope_var_name subscope_vars_defined in
Dcalc.Ast.make_var (a_var, pos_call))
all_subscope_vars
in
@ -392,14 +401,14 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
in
let all_subscope_vars_dcalc =
List.map
(fun (subvar, tau) ->
(fun (subvar : scope_var_ctx) ->
let sub_dcalc_var =
Dcalc.Ast.Var.make
(Pos.map_under_mark
(fun s -> Pos.unmark (Ast.SubScopeName.get_info subindex) ^ "." ^ s)
(Ast.ScopeVar.get_info subvar))
(Ast.ScopeVar.get_info subvar.scope_var_name))
in
(subvar, tau, sub_dcalc_var))
(subvar, sub_dcalc_var))
all_subscope_vars
in
let subscope_func =
@ -429,7 +438,7 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
let result_tuple_var = Dcalc.Ast.Var.make ("result", pos_sigma) in
let result_tuple_typ =
( Dcalc.Ast.TTuple
( List.map (fun (_, tau, _) -> (tau, pos_sigma)) all_subscope_vars_dcalc,
( List.map (fun (subvar, _) -> (subvar.scope_var_typ, pos_sigma)) all_subscope_vars_dcalc,
Some called_scope_return_struct ),
pos_sigma )
in
@ -443,10 +452,10 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
in
let result_bindings_lets =
List.mapi
(fun i (_, tau, v) ->
(fun i (var_ctx, v) ->
{
Dcalc.Ast.scope_let_var = (v, pos_sigma);
Dcalc.Ast.scope_let_typ = (tau, pos_sigma);
Dcalc.Ast.scope_let_typ = (var_ctx.scope_var_typ, pos_sigma);
Dcalc.Ast.scope_let_kind = Dcalc.Ast.DestructuringSubScopeResults;
Dcalc.Ast.scope_let_expr =
Bindlib.box_apply
@ -455,7 +464,9 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
( r,
i,
Some called_scope_return_struct,
List.map (fun (_, t, _) -> (t, pos_sigma)) all_subscope_vars_dcalc ),
List.map
(fun (var_ctx, _) -> (var_ctx.scope_var_typ, pos_sigma))
all_subscope_vars_dcalc ),
pos_sigma ))
(Dcalc.Ast.make_var (result_tuple_var, pos_sigma));
})
@ -467,7 +478,8 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
subscope_vars =
Ast.SubScopeMap.add subindex
(List.fold_left
(fun acc (var, tau, dvar) -> Ast.ScopeVarMap.add var (dvar, tau) acc)
(fun acc (var_ctx, dvar) ->
Ast.ScopeVarMap.add var_ctx.scope_var_name (dvar, var_ctx.scope_var_typ) acc)
Ast.ScopeVarMap.empty all_subscope_vars_dcalc)
ctx.subscope_vars;
} )
@ -512,29 +524,33 @@ let translate_scope_decl (struct_ctx : Ast.struct_ctx) (enum_ctx : Ast.enum_ctx)
Dcalc.Ast.scope_body * Dcalc.Ast.struct_ctx =
let ctx = empty_ctx struct_ctx enum_ctx sctx scope_name in
let sigma_info = Ast.ScopeName.get_info sigma.scope_decl_name in
let scope_variables, _, scope_input_var, scope_input_struct_name, scope_return_struct_name =
Ast.ScopeMap.find sigma.scope_decl_name sctx
in
let scope_sig = Ast.ScopeMap.find sigma.scope_decl_name sctx in
let scope_variables = scope_sig.scope_sig_local_vars in
let scope_input_var = scope_sig.scope_sig_input_var in
let scope_input_struct_name = scope_sig.scope_sig_input_struct in
let scope_return_struct_name = scope_sig.scope_sig_output_struct in
let pos_sigma = Pos.get_position sigma_info in
let rules, return_exp, ctx =
translate_rules ctx sigma.scope_decl_rules sigma_info scope_return_struct_name
in
let scope_variables =
List.map
(fun (x, tau) ->
let dcalc_x, _ = Ast.ScopeVarMap.find x ctx.scope_vars in
(x, tau, dcalc_x))
(fun var_ctx ->
let dcalc_x, _ = Ast.ScopeVarMap.find var_ctx.scope_var_name ctx.scope_vars in
(var_ctx, dcalc_x))
scope_variables
in
(* first we create variables from the fields of the input struct *)
let input_destructurings =
List.mapi
(fun i (_, tau, v) ->
(fun i (var_ctx, v) ->
{
Dcalc.Ast.scope_let_kind = Dcalc.Ast.DestructuringInputStruct;
Dcalc.Ast.scope_let_var = (v, pos_sigma);
Dcalc.Ast.scope_let_typ =
(Dcalc.Ast.TArrow ((Dcalc.Ast.TLit TUnit, pos_sigma), (tau, pos_sigma)), pos_sigma);
( Dcalc.Ast.TArrow
((Dcalc.Ast.TLit TUnit, pos_sigma), (var_ctx.scope_var_typ, pos_sigma)),
pos_sigma );
Dcalc.Ast.scope_let_expr =
Bindlib.box_apply
(fun r ->
@ -543,8 +559,9 @@ let translate_scope_decl (struct_ctx : Ast.struct_ctx) (enum_ctx : Ast.enum_ctx)
i,
Some scope_input_struct_name,
List.map
(fun (_, t, _) ->
( Dcalc.Ast.TArrow ((Dcalc.Ast.TLit TUnit, pos_sigma), (t, pos_sigma)),
(fun (var_ctx, _) ->
( Dcalc.Ast.TArrow
((Dcalc.Ast.TLit TUnit, pos_sigma), (var_ctx.scope_var_typ, pos_sigma)),
pos_sigma ))
scope_variables ),
pos_sigma ))
@ -554,21 +571,22 @@ let translate_scope_decl (struct_ctx : Ast.struct_ctx) (enum_ctx : Ast.enum_ctx)
in
let scope_return_struct_fields =
List.map
(fun (_, tau, dvar) ->
(fun (var_ctx, dvar) ->
let struct_field_name =
Ast.StructFieldName.fresh (Bindlib.name_of dvar ^ "_out", pos_sigma)
in
(struct_field_name, (tau, pos_sigma)))
(struct_field_name, (var_ctx.scope_var_typ, pos_sigma)))
scope_variables
in
let scope_input_struct_fields =
List.map
(fun (_, tau, dvar) ->
(fun (var_ctx, dvar) ->
let struct_field_name =
Ast.StructFieldName.fresh (Bindlib.name_of dvar ^ "_in", pos_sigma)
in
( struct_field_name,
(Dcalc.Ast.TArrow ((Dcalc.Ast.TLit TUnit, pos_sigma), (tau, pos_sigma)), pos_sigma) ))
( Dcalc.Ast.TArrow ((Dcalc.Ast.TLit TUnit, pos_sigma), (var_ctx.scope_var_typ, pos_sigma)),
pos_sigma ) ))
scope_variables
in
let new_struct_ctx =
@ -623,16 +641,26 @@ let translate_program (prgm : Ast.program) : Dcalc.Ast.program * Dependency.TVer
Ast.StructName.fresh
(Pos.map_under_mark (fun s -> s ^ "_in") (Ast.ScopeName.get_info scope_name))
in
( List.map
(fun (scope_var, tau) ->
let tau = translate_typ (ctx_for_typ_translation scope_name) tau in
(scope_var, Pos.unmark tau))
(Ast.ScopeVarMap.bindings scope.scope_sig),
scope_dvar,
scope_input_var,
scope_input_struct_name,
scope_return_struct_name ))
{
scope_sig_local_vars =
List.map
(fun (scope_var, tau) ->
let tau = translate_typ (ctx_for_typ_translation scope_name) tau in
{
scope_var_name = scope_var;
scope_var_typ = Pos.unmark tau;
scope_var_visibility =
{
visibility_input = true;
visibility_output = true (* TODO: change with info from desugared *);
};
})
(Ast.ScopeVarMap.bindings scope.scope_sig);
scope_sig_scope_var = scope_dvar;
scope_sig_input_var = scope_input_var;
scope_sig_input_struct = scope_input_struct_name;
scope_sig_output_struct = scope_return_struct_name;
})
prgm.program_scopes
in
(* the resulting expression is the list of definitions of all the scopes, ending with the
@ -647,7 +675,7 @@ let translate_program (prgm : Ast.program) : Dcalc.Ast.program * Dependency.TVer
let scope_body, scope_out_struct =
translate_scope_decl struct_ctx enum_ctx sctx scope_name scope
in
let _, dvar, _, _, _ = Ast.ScopeMap.find scope_name sctx in
let dvar = (Ast.ScopeMap.find scope_name sctx).scope_sig_scope_var in
let decl_ctx =
{
decl_ctx with

2
compiler/scopelang/scope_to_dcalc.mli
View File

@ -12,6 +12,8 @@
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Scope language to default calculus translator *)
val translate_program : Ast.program -> Dcalc.Ast.program * Dependency.TVertex.t list
(** Usage [translate_program p] returns a tuple [(new_program, types_list)] where [new_program] is
the map of translated scopes. Finally, [types_list] is a list of all types (structs and enums)

29
compiler/scopelang/scopelang.mld
View File

@ -1,10 +1,10 @@
{0 The scope language }
This representation is the third in the compilation chain
(see {{: index.html#architecture} Architecture}). Its main difference
This representation is the third in the compilation chain
(see {{: index.html#architecture} Architecture}). Its main difference
with the previous {{: desugared.html} desugared representation} is that inside
a scope, the definitions are ordered according to their computational
dependency order, and each definition is a {!constructor: Dcalc.Ast.EDefault} tree
a scope, the definitions are ordered according to their computational
dependency order, and each definition is a {!Dcalc.Ast.EDefault} tree
instead of a flat list of rules.
The module describing the abstract syntax tree is:
@ -13,17 +13,13 @@ The module describing the abstract syntax tree is:
Printing helpers can be found in {!module: Scopelang.Print}.
This intermediate representation corresponds to the scope language
This intermediate representation corresponds to the scope language
presented in the {{: https://github.com/CatalaLang/catala/raw/master/doc/formalization/formalization.pdf}
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
The translation from the scope language to the
{{: dcalc.html} default calculus} involves three big features:
{ol
@ -32,7 +28,12 @@ The translation from the scope language to the
{li Transform the list of scopes into a program}
}
1 and 3 involve computing dependency graphs for respectively the structs and
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.
1 and 3 involve computing dependency graphs for respectively the structs and
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}

4
compiler/surface/ast.ml
View File

@ -433,9 +433,12 @@ type scope_use = {
name = "scope_use_iter";
}]
type scope_decl_context_item_attribute = Context | Input | Output | Internal
type scope_decl_context_scope = {
scope_decl_context_scope_name : ident Pos.marked;
scope_decl_context_scope_sub_scope : constructor Pos.marked;
scope_decl_context_scope_attribute : (scope_decl_context_item_attribute[@opaque]) Pos.marked;
}
[@@deriving
visitors
@ -454,6 +457,7 @@ type scope_decl_context_scope = {
type scope_decl_context_data = {
scope_decl_context_item_name : ident Pos.marked;
scope_decl_context_item_typ : typ Pos.marked;
scope_decl_context_item_attribute : (scope_decl_context_item_attribute[@opaque]) Pos.marked;
}
[@@deriving
visitors

213
compiler/surface/desugaring.ml
View File

@ -878,19 +878,19 @@ let merge_conditions (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option
(** Translates a surface definition into condition into a desugared {!type: Desugared.Ast.rule} *)
let process_default (ctxt : Name_resolution.context) (scope : Scopelang.Ast.ScopeName.t)
(def_key : Desugared.Ast.ScopeDef.t Pos.marked)
(def_key : Desugared.Ast.ScopeDef.t Pos.marked) (rule_id : Desugared.Ast.RuleName.t)
(param_uid : Scopelang.Ast.Var.t Pos.marked option)
(precond : Scopelang.Ast.expr Pos.marked Bindlib.box option)
(exception_to_rule : Desugared.Ast.RuleName.t Pos.marked option)
(exception_to_rules : Desugared.Ast.RuleSet.t Pos.marked)
(just : Ast.expression Pos.marked option) (cons : Ast.expression Pos.marked) :
Desugared.Ast.rule =
let just = match just with Some just -> Some (translate_expr scope ctxt just) | None -> None in
let just = merge_conditions precond just (Pos.get_position def_key) in
let cons = translate_expr scope ctxt cons in
{
just;
cons;
parameter =
rule_just = just;
rule_cons = cons;
rule_parameter =
(let def_key_typ = Name_resolution.get_def_typ ctxt (Pos.unmark def_key) in
match (Pos.unmark def_key_typ, param_uid) with
| Scopelang.Ast.TArrow (t_in, _), Some param_uid -> Some (Pos.unmark param_uid, t_in)
@ -903,7 +903,8 @@ let process_default (ctxt : Name_resolution.context) (scope : Scopelang.Ast.Scop
"This definition has a parameter but its type is not a function"
(Pos.get_position (Bindlib.unbox cons))
| _ -> None);
exception_to_rule;
rule_exception_to_rules = exception_to_rules;
rule_id;
}
(** Wrapper around {!val: process_default} that performs some name disambiguation *)
@ -916,6 +917,7 @@ let process_def (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option)
Name_resolution.get_def_key (Pos.unmark def.definition_name) scope_uid ctxt
(Pos.get_position def.definition_expr)
in
let scope_def_ctxt = Desugared.Ast.ScopeDefMap.find def_key scope_ctxt.scope_defs_contexts in
(* We add to the name resolution context the name of the parameter variable *)
let param_uid, new_ctxt =
match def.definition_parameter with
@ -925,74 +927,42 @@ let process_def (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option)
(Some (Pos.same_pos_as param_var param), ctxt)
in
let scope_updated =
let x_def, x_type, is_cond =
match Desugared.Ast.ScopeDefMap.find_opt def_key scope.scope_defs with
| Some def -> def
| None ->
( Desugared.Ast.RuleMap.empty,
Name_resolution.get_def_typ ctxt def_key,
Name_resolution.is_def_cond ctxt def_key )
in
let rule_name =
match def.Ast.definition_label with
| None -> None
| Some label -> Some (Desugared.Ast.IdentMap.find (Pos.unmark label) scope_ctxt.label_idmap)
in
let rule_name =
match rule_name with
| Some x -> x
| None ->
Desugared.Ast.RuleName.fresh
(match def.definition_label with
| None ->
Pos.map_under_mark
(fun qident -> String.concat "." (List.map (fun i -> Pos.unmark i) qident))
def.definition_name
| Some label -> label)
in
let is_exception (def : Ast.definition) =
match def.Ast.definition_exception_to with NotAnException -> false | _ -> true
in
(* If we had previously defined a rulename for this default definition during the elaboration of
default exceptions, this trumps the newly generated name. *)
let rule_name =
if is_exception def then rule_name
else
match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with
| None | Some (Name_resolution.Ambiguous _) -> rule_name
| Some (Name_resolution.Unique x) -> x
in
let parent_rule =
let scope_def = Desugared.Ast.ScopeDefMap.find def_key scope.scope_defs in
let rule_name = def.definition_id in
let parent_rules =
match def.Ast.definition_exception_to with
| NotAnException -> None
| UnlabeledException ->
Some
(match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with
(* This should have been caught previously by check_unlabeled_exception *)
| None | Some (Name_resolution.Ambiguous _) -> assert false
| Some (Name_resolution.Unique name) -> Pos.same_pos_as name def.Ast.definition_name)
| ExceptionToLabel label ->
Some
(try
Pos.same_pos_as
(Desugared.Ast.IdentMap.find (Pos.unmark label) scope_ctxt.label_idmap)
label
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Unknown label: \"%s\"" (Pos.unmark label))
(Pos.get_position label))
| NotAnException -> (Desugared.Ast.RuleSet.empty, Pos.get_position def.Ast.definition_name)
| UnlabeledException -> (
match scope_def_ctxt.default_exception_rulename with
(* This should have been caught previously by check_unlabeled_exception *)
| None | Some (Name_resolution.Ambiguous _) -> assert false (* should not happen *)
| Some (Name_resolution.Unique (name, pos)) -> (Desugared.Ast.RuleSet.singleton name, pos)
)
| ExceptionToLabel label -> (
try
let label_id =
Desugared.Ast.IdentMap.find (Pos.unmark label) scope_def_ctxt.label_idmap
in
( Desugared.Ast.LabelMap.find label_id scope_def.scope_def_label_groups,
Pos.get_position def.Ast.definition_name )
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Unknown label for the scope variable %a: \"%s\""
Desugared.Ast.ScopeDef.format_t def_key (Pos.unmark label))
(Pos.get_position label))
in
let x_def =
Desugared.Ast.RuleMap.add rule_name
(process_default new_ctxt scope_uid
(def_key, Pos.get_position def.definition_name)
param_uid precond parent_rule def.definition_condition def.definition_expr)
x_def
let scope_def =
{
scope_def with
scope_def_rules =
Desugared.Ast.RuleMap.add rule_name
(process_default new_ctxt scope_uid
(def_key, Pos.get_position def.definition_name)
rule_name param_uid precond parent_rules def.definition_condition def.definition_expr)
scope_def.scope_def_rules;
}
in
{
scope with
scope_defs = Desugared.Ast.ScopeDefMap.add def_key (x_def, x_type, is_cond) scope.scope_defs;
}
{ scope with scope_defs = Desugared.Ast.ScopeDefMap.add def_key scope_def scope.scope_defs }
in
{
prgm with
@ -1052,35 +1022,26 @@ let check_unlabeled_exception (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_r
(item : Ast.scope_use_item Pos.marked) : unit =
let scope_ctxt = Scopelang.Ast.ScopeMap.find scope ctxt.scopes in
match Pos.unmark item with
| Ast.Rule rule -> (
match rule.rule_exception_to with
| Ast.Rule _ | Ast.Definition _ -> (
let def_key, exception_to =
match Pos.unmark item with
| Ast.Rule rule ->
( Name_resolution.get_def_key (Pos.unmark rule.rule_name) scope ctxt
(Pos.get_position rule.rule_name),
rule.rule_exception_to )
| Ast.Definition def ->
( Name_resolution.get_def_key (Pos.unmark def.definition_name) scope ctxt
(Pos.get_position def.definition_name),
def.definition_exception_to )
| _ -> assert false
(* should not happen *)
in
let scope_def_ctxt = Desugared.Ast.ScopeDefMap.find def_key scope_ctxt.scope_defs_contexts in
match exception_to with
| Ast.NotAnException | Ast.ExceptionToLabel _ -> ()
(* If this is an unlabeled exception, we check that it has a unique default definition *)
| Ast.UnlabeledException -> (
let def_key =
Name_resolution.get_def_key (Pos.unmark rule.rule_name) scope ctxt
(Pos.get_position rule.rule_consequence)
in
match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with
| None ->
Errors.raise_spanned_error "This exception does not have a corresponding definition"
(Pos.get_position item)
| Some (Ambiguous pos) ->
Errors.raise_multispanned_error
"This exception can refer to several definitions. Try using labels to disambiguate"
([ (Some "Ambiguous exception", Pos.get_position item) ]
@ List.map (fun p -> (Some "Candidate definition", p)) pos)
| Some (Unique _) -> ()))
| Ast.Definition def -> (
match def.definition_exception_to with
| Ast.NotAnException | Ast.ExceptionToLabel _ -> ()
(* If this is an unlabeled exception, we check that it has a unique default definition *)
| Ast.UnlabeledException -> (
let def_key =
Name_resolution.get_def_key (Pos.unmark def.definition_name) scope ctxt
(Pos.get_position def.definition_expr)
in
match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with
match scope_def_ctxt.default_exception_rulename with
| None ->
Errors.raise_spanned_error "This exception does not have a corresponding definition"
(Pos.get_position item)
@ -1128,13 +1089,57 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) : Desu
s_context.Name_resolution.var_idmap Scopelang.Ast.ScopeVarSet.empty;
Desugared.Ast.scope_sub_scopes = s_context.Name_resolution.sub_scopes;
Desugared.Ast.scope_defs =
Desugared.Ast.IdentMap.fold
(fun _ v acc ->
let x, y = Scopelang.Ast.ScopeVarMap.find v ctxt.Name_resolution.var_typs in
Desugared.Ast.ScopeDefMap.add (Desugared.Ast.ScopeDef.Var v)
(Desugared.Ast.RuleMap.empty, x, y)
acc)
s_context.Name_resolution.var_idmap Desugared.Ast.ScopeDefMap.empty;
(* Initializing the definitions of all scopes and subscope vars, with no rules yet
inside *)
(let scope_vars_defs =
Desugared.Ast.IdentMap.fold
(fun _ v acc ->
let x, y = Scopelang.Ast.ScopeVarMap.find v ctxt.Name_resolution.var_typs in
let def_key = Desugared.Ast.ScopeDef.Var v in
Desugared.Ast.ScopeDefMap.add def_key
{
Desugared.Ast.scope_def_rules = Desugared.Ast.RuleMap.empty;
Desugared.Ast.scope_def_typ = x;
Desugared.Ast.scope_def_label_groups =
Name_resolution.label_groups ctxt s_uid def_key;
Desugared.Ast.scope_def_is_condition = y;
Desugared.Ast.scope_def_visibility =
{
Scopelang.Ast.visibility_input = true;
Scopelang.Ast.visibility_output = true;
};
}
acc)
s_context.Name_resolution.var_idmap Desugared.Ast.ScopeDefMap.empty
in
let scope_and_subscope_vars_defs =
Scopelang.Ast.SubScopeMap.fold
(fun subscope_name subscope_uid acc ->
Desugared.Ast.IdentMap.fold
(fun _ v acc ->
let x, y =
Scopelang.Ast.ScopeVarMap.find v ctxt.Name_resolution.var_typs
in
let def_key = Desugared.Ast.ScopeDef.SubScopeVar (subscope_name, v) in
Desugared.Ast.ScopeDefMap.add def_key
{
Desugared.Ast.scope_def_rules = Desugared.Ast.RuleMap.empty;
Desugared.Ast.scope_def_typ = x;
Desugared.Ast.scope_def_label_groups =
Name_resolution.label_groups ctxt subscope_uid def_key;
Desugared.Ast.scope_def_is_condition = y;
Desugared.Ast.scope_def_visibility =
{
Scopelang.Ast.visibility_input = true;
Scopelang.Ast.visibility_output = true;
};
}
acc)
(Scopelang.Ast.ScopeMap.find subscope_uid ctxt.Name_resolution.scopes)
.Name_resolution.var_idmap acc)
s_context.sub_scopes scope_vars_defs
in
scope_and_subscope_vars_defs);
Desugared.Ast.scope_assertions = [];
Desugared.Ast.scope_meta_assertions = [];
Desugared.Ast.scope_uid = s_uid;

2
compiler/surface/desugaring.mli
View File

@ -12,7 +12,7 @@
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Translation from {!module: Surface.Ast} to {!module: Desugaring.Ast}.
(** Translation from {!module: Surface.Ast} to {!module: Desugared.Ast}.
- Removes syntactic sugars
- Separate code from legislation *)

16
compiler/surface/lexer.cppo.ml
View File

@ -227,6 +227,15 @@ module R = Re.Pcre
#ifndef MR_GetYear
#define MR_GetYear MS_GetYear
#endif
#ifndef MR_INPUT
#define MR_INPUT MS_INPUT
#endif
#ifndef MR_OUTPUT
#define MR_OUTPUT MS_OUTPUT
#endif
#ifndef MR_INTERNAL
#define MR_INTERNAL MS_INTERNAL
#endif
let token_list : (string * token) list =
[
@ -292,6 +301,9 @@ let token_list : (string * token) list =
(MS_DAY, DAY);
(MS_TRUE, TRUE);
(MS_FALSE, FALSE);
(MS_INPUT, INPUT);
(MS_OUTPUT, OUTPUT);
(MS_INTERNAL, INTERNAL)
]
@ L.token_list_language_agnostic
@ -778,8 +790,8 @@ let lex_law (lexbuf : lexbuf) : token =
| Star (Compl '\n'), ('\n' | eof) -> LAW_TEXT (Utf8.lexeme lexbuf)
| _ -> L.raise_lexer_error (Pos.from_lpos prev_pos) prev_lexeme
(** Entry point of the lexer, distributes to {!val: lex_code} or {!val: lex_law} depending of {!val:
Surface.Lexer_common.is_code}. *)
(** Entry point of the lexer, distributes to {!val: lex_code} or {!val:lex_law}
depending of the current {!val: Surface.Lexer_common.context}. *)
let lexer (lexbuf : lexbuf) : token =
match !L.context with
| Law -> lex_law lexbuf

4
compiler/surface/lexer_common.ml
View File

@ -96,6 +96,6 @@ module type LocalisedLexer = sig
(** Main lexing function used outside code blocks *)
val lexer : Sedlexing.lexbuf -> Tokens.token
(** Entry point of the lexer, distributes to {!val: lex_code} or {!val: lex_law} depending of
{!val: Surface.Lexer_common.is_code}. *)
(** Entry point of the lexer, distributes to {!val: lex_code} or {!val:lex_law} depending of the
current {!val: Surface.Lexer_common.context}. *)
end

12
compiler/surface/lexer_common.mli
View File

@ -32,8 +32,8 @@ val raise_lexer_error : Utils.Pos.t -> string -> 'a
(** Error-generating helper *)
val token_list_language_agnostic : (string * Tokens.token) list
(** Associative list matching each punctuation string part of the Catala syntax with its {!module:
Surface.Parser} token. Same for all the input languages (English, French, etc.) *)
(** Associative list matching each punctuation string part of the Catala syntax with its
{!Surface.Parser} token. Same for all the input languages (English, French, etc.) *)
val calc_precedence : string -> int
(** Calculates the precedence according a matched regex of the form : '[#]+' *)
@ -43,8 +43,8 @@ val get_law_heading : Sedlexing.lexbuf -> Tokens.token
module type LocalisedLexer = sig
val token_list : (string * Tokens.token) list
(** Same as {!val: token_list_language_agnostic}, but with tokens whose string varies with the
input language. *)
(** Same as {!val: Surface.Lexer_common.token_list_language_agnostic}, but with tokens whose
string varies with the input language. *)
val lex_builtin : string -> Ast.builtin_expression option
(** Simple lexer for builtins *)
@ -56,6 +56,6 @@ module type LocalisedLexer = sig
(** Main lexing function used outside code blocks *)
val lexer : Sedlexing.lexbuf -> Tokens.token
(** Entry point of the lexer, distributes to {!val: lex_code} or {!val: lex_law} depending of
{!val: is_code}. *)
(** Entry point of the lexer, distributes to {!val: lex_code} or {!val:lex_law} depending of the
current {!val: Surface.Lexer_common.context}. *)
end

3
compiler/surface/lexer_en.cppo.ml
View File

@ -84,6 +84,9 @@
#define MS_DAY "day"
#define MS_TRUE "true"
#define MS_FALSE "false"
#define MS_INPUT "input"
#define MS_OUTPUT "output"
#define MS_INTERNAL "internal"
(* Specific delimiters *)

60
compiler/surface/lexer_fr.cppo.ml
View File

@ -23,31 +23,41 @@
#define MS_SCOPE "champ d'application"
#define MR_SCOPE "champ", space_plus, "d'application"
#define MS_CONSEQUENCE "conséquence"
#define MS_DATA "donnée"
#define MS_DEPENDS "dépend de"
#define MR_DEPENDS "dépend", space_plus, "de"
#define MS_DECLARATION "déclaration"
#define MS_CONSEQUENCE "conséquence"
#define MR_CONSEQUENCE "cons", 0xE9, "quence"
#define MS_DATA "donnée"
#define MR_DATA "donn", 0xE9, "e"
#define MS_DEPENDS "dépend de"
#define MR_DEPENDS "d", 0xE9, "pend", space_plus, "de"
#define MS_DECLARATION "déclaration"
#define MR_DECLARATION "d", 0xE9, "claration"
#define MS_CONTEXT "contexte"
#define MS_DECREASING "décroissant"
#define MS_DECREASING "décroissant"
#define MR_DECREASING "d", 0xE9, "croissant"
#define MS_INCREASING "croissant"
#define MS_OF "de"
#define MS_COLLECTION "collection"
#define MS_ENUM "énumération"
#define MS_ENUM "énumération"
#define MR_ENUM 0xE9, "num", 0xE9, "ration"
#define MS_INTEGER "entier"
#define MS_MONEY "argent"
#define MS_TEXT "texte"
#define MS_DECIMAL "décimal"
#define MS_DECIMAL "décimal"
#define MR_DECIMAL "d", 0xE9, "cimal"
#define MS_DATE "date"
#define MS_DURATION "durée"
#define MS_BOOLEAN "booléen"
#define MS_DURATION "durée"
#define MR_DURATION "dur", 0xE9, "e"
#define MS_BOOLEAN "booléen"
#define MR_BOOLEAN "bool", 0xE9, "en"
#define MS_SUM "somme"
#define MS_FILLED "rempli"
#define MS_DEFINITION "définition"
#define MS_LABEL "étiquette"
#define MS_DEFINITION "définition"
#define MR_DEFINITION "d", 0xE9, "finition"
#define MS_LABEL "étiquette"
#define MR_LABEL 0xE9, "tiquette"
#define MS_EXCEPTION "exception"
#define MS_DEFINED_AS "égal à"
#define MR_DEFINED_AS "égal", space_plus, "à"
#define MS_DEFINED_AS "égal à"
#define MR_DEFINED_AS 0xE9, "gal", space_plus, 0xE0
#define MS_MATCH "selon"
#define MS_WILDCARD "n'importe quel"
#define MR_WILDCARD "n'importe", space_plus, "quel"
@ -68,9 +78,11 @@
#define MS_ALL "tout"
#define MS_WE_HAVE "on a"
#define MR_WE_HAVE "on", space_plus, "a"
#define MS_FIXED "fixé"
#define MS_FIXED "fixé"
#define MR_FIXED "fix", 0xE9
#define MS_BY "par"
#define MS_RULE "règle"
#define MS_RULE "règle"
#define MR_RULE "r", 0xE8, "gle"
#define MS_EXISTS "existe"
#define MS_IN "dans"
#define MS_SUCH "tel"
@ -91,6 +103,10 @@
#define MS_DAY "jour"
#define MS_TRUE "vrai"
#define MS_FALSE "faux"
#define MS_INPUT "entrée"
#define MR_INPUT "entr", 0xE9, "e"
#define MS_OUTPUT "sortie"
#define MS_INTERNAL "interne"
(* Specific delimiters *)
@ -102,10 +118,14 @@
(* Builtins *)
#define MS_IntToDec "entier_vers_décimal"
#define MS_GetDay "accès_jour"
#define MS_GetMonth "accès_mois"
#define MS_GetYear "accès_année"
#define MS_IntToDec "entier_vers_décimal"
#define MR_IntToDec "entier_vers_d", 0xE9, "cimal"
#define MS_GetDay "accès_jour"
#define MR_GetDay "acc", 0xE8, "s_jour"
#define MS_GetMonth "accès_mois"
#define MR_GetMonth "acc", 0xE8, "s_mois"
#define MS_GetYear "accès_année"
#define MR_GetYear "acc", 0xE8, "s_ann", 0xE9, "e"
(* Directives *)

24
compiler/surface/lexer_pl.cppo.ml
View File

@ -31,10 +31,10 @@
#define MS_COLLECTION "kolekcja"
#define MS_ENUM "enumeracja"
#define MS_INTEGER "calkowita"
#define MS_MONEY "pieni\x01\x05dze"
#define MS_MONEY "pieniądze"
#define MR_MONEY "pieni", 0x0105, "dze"
#define MS_TEXT "tekst"
#define MS_DECIMAL "dziesi\x01\x19tny"
#define MS_DECIMAL "dziesiętny"
#define MR_DECIMAL "dziesi", 0x0119, "tny"
#define MS_DATE "czas"
#define MS_DURATION "czas trwania"
@ -44,7 +44,7 @@
#define MS_FILLED "spelnione"
#define MS_DEFINITION "definicja"
#define MS_LABEL "etykieta"
#define MS_EXCEPTION "wyj\x01\x05tek"
#define MS_EXCEPTION "wyjątek"
#define MR_EXCEPTION "wyj", 0x0105, "tek"
#define MS_DEFINED_AS "wynosi"
#define MS_MATCH "pasuje"
@ -89,6 +89,12 @@
#define MS_DAY "dzien"
#define MS_TRUE "prawda"
#define MS_FALSE "falsz"
#define MS_INPUT "wejście"
#define MR_INPUT "wej", 0x15B, "cie"
#define MS_OUTPUT "wyjście"
#define MR_OUTPUT "wyj", 0x15B, "cie"
#define MS_INTERNAL "wewnętrzny"
#define MR_INTERNAL "wewn", 0x0119, "trzny"
(* Specific delimiters *)
@ -100,10 +106,14 @@
(* Builtins *)
#define MS_IntToDec "integer_to_decimal"
#define MS_GetDay "get_day"
#define MS_GetMonth "get_month"
#define MS_GetYear "get_year"
#define MS_IntToDec "calkowita_wers_dziesiętny"
#define MR_IntToDec "calkowita_wers_dziesi", 0x0119, "tny"
#define MS_GetDay "dostęp_dzień"
#define MR_GetDay "dost", 0x0119, "p_dzie", 0x144
#define MS_GetMonth "dostęp_miesiąc"
#define MR_GetMonth "dost", 0x0119, "p_miesi", 0x0105, "c"
#define MS_GetYear "dostęp_rok"
#define MR_GetYear "dost", 0x0119, "p_rok"
(* Directives *)

240
compiler/surface/name_resolution.ml
View File

@ -23,13 +23,17 @@ type ident = string
type typ = Scopelang.Ast.typ
type unique_rulename = Ambiguous of Pos.t list | Unique of Desugared.Ast.RuleName.t
type unique_rulename = Ambiguous of Pos.t list | Unique of Desugared.Ast.RuleName.t Pos.marked
type scope_def_context = {
default_exception_rulename : unique_rulename option;
label_idmap : Desugared.Ast.LabelName.t Desugared.Ast.IdentMap.t;
label_groups : Desugared.Ast.RuleSet.t Desugared.Ast.LabelMap.t;
}
type scope_context = {
var_idmap : Scopelang.Ast.ScopeVar.t Desugared.Ast.IdentMap.t; (** Scope variables *)
label_idmap : Desugared.Ast.RuleName.t Desugared.Ast.IdentMap.t;
(** Set of rules attached to a label *)
default_rulemap : unique_rulename Desugared.Ast.ScopeDefMap.t;
scope_defs_contexts : scope_def_context Desugared.Ast.ScopeDefMap.t;
(** What is the default rule to refer to for unnamed exceptions, if any *)
sub_scopes_idmap : Scopelang.Ast.SubScopeName.t Desugared.Ast.IdentMap.t;
(** Sub-scopes variables *)
@ -137,6 +141,14 @@ let is_def_cond (ctxt : context) (def : Desugared.Ast.ScopeDef.t) : bool =
| Desugared.Ast.ScopeDef.Var x ->
is_var_cond ctxt x
let label_groups (ctxt : context) (s_uid : Scopelang.Ast.ScopeName.t)
(def : Desugared.Ast.ScopeDef.t) : Desugared.Ast.RuleSet.t Desugared.Ast.LabelMap.t =
try
(Desugared.Ast.ScopeDefMap.find def
(Scopelang.Ast.ScopeMap.find s_uid ctxt.scopes).scope_defs_contexts)
.label_groups
with Not_found -> Desugared.Ast.LabelMap.empty
(** {1 Declarations pass} *)
(** Process a subscope declaration *)
@ -148,8 +160,9 @@ let process_subscope_decl (scope : Scopelang.Ast.ScopeName.t) (ctxt : context)
match Desugared.Ast.IdentMap.find_opt subscope scope_ctxt.sub_scopes_idmap with
| Some use ->
Errors.raise_multispanned_error
(Format.asprintf "Subscope name \"%s\" already used"
(Utils.Cli.print_with_style [ ANSITerminal.yellow ] "%s" subscope))
(Format.asprintf "Subscope name \"%a\" already used"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
subscope)
[
(Some "first use", Pos.get_position (Scopelang.Ast.SubScopeName.get_info use));
(Some "second use", s_pos);
@ -203,8 +216,9 @@ let rec process_base_typ (ctxt : context) ((typ, typ_pos) : Ast.base_typ Pos.mar
| Some e_uid -> (Scopelang.Ast.TEnum e_uid, typ_pos)
| None ->
Errors.raise_spanned_error
(Format.asprintf "Unknown type \"%s\", not a struct or enum previously declared"
(Utils.Cli.print_with_style [ ANSITerminal.yellow ] "%s" ident))
(Format.asprintf "Unknown type \"%a\", not a struct or enum previously declared"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
ident)
typ_pos)))
(** Process a type (function or not) *)
@ -227,8 +241,9 @@ let process_data_decl (scope : Scopelang.Ast.ScopeName.t) (ctxt : context)
match Desugared.Ast.IdentMap.find_opt name scope_ctxt.var_idmap with
| Some use ->
Errors.raise_multispanned_error
(Format.asprintf "var name \"%s\" already used"
(Utils.Cli.print_with_style [ ANSITerminal.yellow ] "%s" name))
(Format.asprintf "var name \"%a\" already used"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
name)
[
(Some "first use", Pos.get_position (Scopelang.Ast.ScopeVar.get_info use));
(Some "second use", pos);
@ -349,8 +364,9 @@ let process_enum_decl (ctxt : context) (edecl : Ast.enum_decl) : context =
let process_name_item (ctxt : context) (item : Ast.code_item Pos.marked) : context =
let raise_already_defined_error (use : Uid.MarkedString.info) name pos msg =
Errors.raise_multispanned_error
(Format.asprintf "%s name \"%s\" already defined" msg
(Utils.Cli.print_with_style [ ANSITerminal.yellow ] "%s" name))
(Format.asprintf "%s name \"%a\" already defined" msg
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
name)
[ (Some "First definition:", Pos.get_position use); (Some "Second definition:", pos) ]
in
match Pos.unmark item with
@ -369,8 +385,7 @@ let process_name_item (ctxt : context) (item : Ast.code_item Pos.marked) : conte
Scopelang.Ast.ScopeMap.add scope_uid
{
var_idmap = Desugared.Ast.IdentMap.empty;
label_idmap = Desugared.Ast.IdentMap.empty;
default_rulemap = Desugared.Ast.ScopeDefMap.empty;
scope_defs_contexts = Desugared.Ast.ScopeDefMap.empty;
sub_scopes_idmap = Desugared.Ast.IdentMap.empty;
sub_scopes = Scopelang.Ast.SubScopeMap.empty;
}
@ -445,80 +460,123 @@ let get_def_key (name : Ast.qident) (scope_uid : Scopelang.Ast.ScopeName.t) (ctx
let process_definition (ctxt : context) (s_name : Scopelang.Ast.ScopeName.t) (d : Ast.definition) :
context =
(* Process the label map first *)
let ctxt =
match d.Ast.definition_label with
| None -> ctxt
| Some label ->
{
ctxt with
scopes =
Scopelang.Ast.ScopeMap.update s_name
(fun s_ctxt ->
match s_ctxt with
| None -> assert false (* should not happen *)
| Some s_ctxt -> (
match Desugared.Ast.IdentMap.find_opt (Pos.unmark label) s_ctxt.label_idmap with
| Some existing_label ->
Errors.raise_multispanned_error
"This label has already been given to another rule, please pick a new \
one since labels should be unique."
[
(Some "Duplicate label:", Pos.get_position label);
( Some "Existing rule with same label:",
Pos.get_position (Desugared.Ast.RuleName.get_info existing_label) );
]
| None ->
Some
{
s_ctxt with
label_idmap =
Desugared.Ast.IdentMap.add (Pos.unmark label) d.Ast.definition_id
s_ctxt.label_idmap;
}))
ctxt.scopes;
}
in
(* And update the map of default rulenames for unlabeled exceptions *)
match d.Ast.definition_exception_to with
(* If this definition is an exception, it cannot be a default definition *)
| UnlabeledException | ExceptionToLabel _ -> ctxt
(* If it is not an exception, we need to distinguish between several cases *)
| NotAnException ->
let def_key =
get_def_key (Pos.unmark d.definition_name) s_name ctxt (Pos.get_position d.definition_expr)
in
let scope_ctxt = Scopelang.Ast.ScopeMap.find s_name ctxt.scopes in
let rulemap =
match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with
(* There was already a default definition for this key. If we need it, it is ambiguous *)
| Some old ->
Desugared.Ast.ScopeDefMap.add def_key
(Ambiguous
([ Pos.get_position d.definition_name ]
@
match old with
| Ambiguous old -> old
| Unique n -> [ Pos.get_position (Desugared.Ast.RuleName.get_info n) ]))
scope_ctxt.default_rulemap
(* No definition has been set yet for this key *)
| None -> (
match d.Ast.definition_label with
(* This default definition has a label. This is not allowed for unlabeled exceptions *)
| Some _ ->
Desugared.Ast.ScopeDefMap.add def_key
(Ambiguous [ Pos.get_position d.definition_name ])
scope_ctxt.default_rulemap
(* This is a possible default definition for this key. We create and store a fresh
rulename *)
| None ->
Desugared.Ast.ScopeDefMap.add def_key
(Unique
(Desugared.Ast.RuleName.fresh (Pos.same_pos_as "default" d.definition_name)))
scope_ctxt.default_rulemap)
in
let new_scope_ctxt = { scope_ctxt with default_rulemap = rulemap } in
{ ctxt with scopes = Scopelang.Ast.ScopeMap.add s_name new_scope_ctxt ctxt.scopes }
(* We update the definition context inside the big context *)
{
ctxt with
scopes =
Scopelang.Ast.ScopeMap.update s_name
(fun (s_ctxt : scope_context option) ->
let def_key =
get_def_key (Pos.unmark d.definition_name) s_name ctxt
(Pos.get_position d.definition_expr)
in
match s_ctxt with
| None -> assert false (* should not happen *)
| Some s_ctxt ->
Some
{
s_ctxt with
scope_defs_contexts =
Desugared.Ast.ScopeDefMap.update def_key
(fun def_key_ctx ->
let def_key_ctx : scope_def_context =
Option.fold
~none:
{
(* Here, this is the first time we encounter a definition for this
definition key *)
default_exception_rulename = None;
label_idmap = Desugared.Ast.IdentMap.empty;
label_groups = Desugared.Ast.LabelMap.empty;
}
~some:(fun x -> x)
def_key_ctx
in
(* First, we update the def key context with information about the
definition's label*)
let def_key_ctx =
match d.Ast.definition_label with
| None -> def_key_ctx
| Some label ->
let new_label_idmap =
Desugared.Ast.IdentMap.update (Pos.unmark label)
(fun existing_label ->
match existing_label with
| Some existing_label -> Some existing_label
| None -> Some (Desugared.Ast.LabelName.fresh label))
def_key_ctx.label_idmap
in
let label_id =
Desugared.Ast.IdentMap.find (Pos.unmark label) new_label_idmap
in
{
def_key_ctx with
label_idmap = new_label_idmap;
label_groups =
Desugared.Ast.LabelMap.update label_id
(fun group ->
match group with
| None ->
Some (Desugared.Ast.RuleSet.singleton d.definition_id)
| Some existing_group ->
Some
(Desugared.Ast.RuleSet.add d.definition_id
existing_group))
def_key_ctx.label_groups;
}
in
(* And second, we update the map of default rulenames for unlabeled
exceptions *)
let def_key_ctx =
match d.Ast.definition_exception_to with
(* If this definition is an exception, it cannot be a default
definition *)
| UnlabeledException | ExceptionToLabel _ -> def_key_ctx
(* If it is not an exception, we need to distinguish between several
cases *)
| NotAnException -> (
match def_key_ctx.default_exception_rulename with
(* There was already a default definition for this key. If we need it,
it is ambiguous *)
| Some old ->
{
def_key_ctx with
default_exception_rulename =
Some
(Ambiguous
([ Pos.get_position d.definition_name ]
@
match old with
| Ambiguous old -> old
| Unique (_, pos) -> [ pos ]));
}
(* No definition has been set yet for this key *)
| None -> (
match d.Ast.definition_label with
(* This default definition has a label. This is not allowed for
unlabeled exceptions *)
| Some _ ->
{
def_key_ctx with
default_exception_rulename =
Some (Ambiguous [ Pos.get_position d.definition_name ]);
}
(* This is a possible default definition for this key. We create
and store a fresh rulename *)
| None ->
{
def_key_ctx with
default_exception_rulename =
Some
(Unique
(d.definition_id, Pos.get_position d.definition_name));
}))
in
Some def_key_ctx)
s_ctxt.scope_defs_contexts;
})
ctxt.scopes;
}
let process_scope_use_item (s_name : Scopelang.Ast.ScopeName.t) (ctxt : context)
(sitem : Ast.scope_use_item Pos.marked) : context =
@ -532,9 +590,9 @@ let process_scope_use (ctxt : context) (suse : Ast.scope_use) : context =
try Desugared.Ast.IdentMap.find (Pos.unmark suse.Ast.scope_use_name) ctxt.scope_idmap
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "\"%s\": this scope has not been declared anywhere, is it a typo?"
(Utils.Cli.print_with_style [ ANSITerminal.yellow ] "%s"
(Pos.unmark suse.Ast.scope_use_name)))
(Format.asprintf "\"%a\": this scope has not been declared anywhere, is it a typo?"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
(Pos.unmark suse.Ast.scope_use_name))
(Pos.get_position suse.Ast.scope_use_name)
in
List.fold_left (process_scope_use_item s_name) ctxt suse.Ast.scope_use_items

17
compiler/surface/name_resolution.mli
View File

@ -23,12 +23,17 @@ type ident = string
type typ = Scopelang.Ast.typ
type unique_rulename = Ambiguous of Pos.t list | Unique of Desugared.Ast.RuleName.t
type unique_rulename = Ambiguous of Pos.t list | Unique of Desugared.Ast.RuleName.t Pos.marked
type scope_def_context = {
default_exception_rulename : unique_rulename option;
label_idmap : Desugared.Ast.LabelName.t Desugared.Ast.IdentMap.t;
label_groups : Desugared.Ast.RuleSet.t Desugared.Ast.LabelMap.t;
}
type scope_context = {
var_idmap : Scopelang.Ast.ScopeVar.t Desugared.Ast.IdentMap.t; (** Scope variables *)
label_idmap : Desugared.Ast.RuleName.t Desugared.Ast.IdentMap.t;
default_rulemap : unique_rulename Desugared.Ast.ScopeDefMap.t;
scope_defs_contexts : scope_def_context Desugared.Ast.ScopeDefMap.t;
(** What is the default rule to refer to for unnamed exceptions, if any *)
sub_scopes_idmap : Scopelang.Ast.SubScopeName.t Desugared.Ast.IdentMap.t;
(** Sub-scopes variables *)
@ -98,6 +103,12 @@ val get_def_typ : context -> Desugared.Ast.ScopeDef.t -> typ Pos.marked
val is_def_cond : context -> Desugared.Ast.ScopeDef.t -> bool
val label_groups :
context ->
Scopelang.Ast.ScopeName.t ->
Desugared.Ast.ScopeDef.t ->
Desugared.Ast.RuleSet.t Desugared.Ast.LabelMap.t
val is_type_cond : Ast.typ Pos.marked -> bool
val add_def_local_var : context -> ident Pos.marked -> context * Scopelang.Ast.Var.t

81
compiler/surface/parser.messages
View File

@ -1,6 +1,6 @@
source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR COLON ALT CONSTRUCTOR CONTENT TEXT YEAR
##
## Ends in an error in state: 341.
## Ends in an error in state: 345.
##
## nonempty_list(enum_decl_line) -> enum_decl_line . [ SCOPE END_CODE DECLARATION ]
## nonempty_list(enum_decl_line) -> enum_decl_line . nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
@ -13,7 +13,7 @@ expected another enum case, or a new declaration or scope use
source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR COLON ALT CONSTRUCTOR CONTENT YEAR
##
## Ends in an error in state: 336.
## Ends in an error in state: 340.
##
## enum_decl_line_payload -> CONTENT . typ [ SCOPE END_CODE DECLARATION ALT ]
##
@ -25,7 +25,7 @@ expected a content type
source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR COLON ALT CONSTRUCTOR YEAR
##
## Ends in an error in state: 335.
## Ends in an error in state: 339.
##
## enum_decl_line -> ALT constructor . option(enum_decl_line_payload) [ SCOPE END_CODE DECLARATION ALT ]
##
@ -37,7 +37,7 @@ expected a payload for your enum case, or another case or declaration
source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR COLON ALT YEAR
##
## Ends in an error in state: 334.
## Ends in an error in state: 338.
##
## enum_decl_line -> ALT . constructor option(enum_decl_line_payload) [ SCOPE END_CODE DECLARATION ALT ]
##
@ -49,7 +49,7 @@ expected the name of an enum case
source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR COLON YEAR
##
## Ends in an error in state: 333.
## Ends in an error in state: 337.
##
## code_item -> DECLARATION ENUM constructor COLON . nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
##
@ -61,7 +61,7 @@ expected an enum case
source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR YEAR
##
## Ends in an error in state: 332.
## Ends in an error in state: 336.
##
## code_item -> DECLARATION ENUM constructor . COLON nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
##
@ -73,7 +73,7 @@ expected a colon
source_file: BEGIN_CODE DECLARATION ENUM YEAR
##
## Ends in an error in state: 331.
## Ends in an error in state: 335.
##
## code_item -> DECLARATION ENUM . constructor COLON nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
##
@ -85,89 +85,66 @@ expected the name of your enum
source_file: BEGIN_CODE DECLARATION SCOPE CONSTRUCTOR COLON CONTEXT IDENT CONDITION YEAR
##
## Ends in an error in state: 326.
## Ends in an error in state: 330.
##
## scope_decl_item -> CONTEXT ident CONDITION . option(struct_scope_func) [ SCOPE END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> scope_decl_item_attribute ident CONDITION . option(struct_scope_func) [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DECLARATION CONTEXT ]
##
## The known suffix of the stack is as follows:
## CONTEXT ident CONDITION
## scope_decl_item_attribute ident CONDITION
##
expected the next context item or a dependency declaration for this item
source_file: BEGIN_CODE DECLARATION SCOPE CONSTRUCTOR COLON CONTEXT IDENT CONTENT TEXT YEAR
##
## Ends in an error in state: 324.
## Ends in an error in state: 328.
##
## scope_decl_item -> CONTEXT ident CONTENT typ . option(struct_scope_func) [ SCOPE END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> scope_decl_item_attribute ident CONTENT typ . option(struct_scope_func) [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DECLARATION CONTEXT ]
##
## The known suffix of the stack is as follows:
## CONTEXT ident CONTENT typ
## scope_decl_item_attribute ident CONTENT typ
##
expected the next context item or a dependency declaration for this item
source_file: BEGIN_CODE DECLARATION SCOPE CONSTRUCTOR COLON CONTEXT IDENT CONTENT YEAR
##
## Ends in an error in state: 323.
## Ends in an error in state: 327.
##
## scope_decl_item -> CONTEXT ident CONTENT . typ option(struct_scope_func) [ SCOPE END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> scope_decl_item_attribute ident CONTENT . typ option(struct_scope_func) [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DECLARATION CONTEXT ]
##
## The known suffix of the stack is as follows:
## CONTEXT ident CONTENT
## scope_decl_item_attribute ident CONTENT
##
expected the type of this context item
source_file: BEGIN_CODE DECLARATION SCOPE CONSTRUCTOR COLON CONTEXT IDENT SCOPE CONSTRUCTOR YEAR
##
## Ends in an error in state: 328.
##
## nonempty_list(scope_decl_item) -> scope_decl_item . [ SCOPE END_CODE DECLARATION ]
## nonempty_list(scope_decl_item) -> scope_decl_item . nonempty_list(scope_decl_item) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## scope_decl_item
##
expected another scope context item or the end of the scope declaration
source_file: BEGIN_CODE DECLARATION SCOPE CONSTRUCTOR COLON CONTEXT IDENT SCOPE YEAR
##
## Ends in an error in state: 321.
##
## scope_decl_item -> CONTEXT ident SCOPE . constructor [ SCOPE END_CODE DECLARATION CONTEXT ]
##
## The known suffix of the stack is as follows:
## CONTEXT ident SCOPE
##
expected the name of the subscope for this context item
source_file: BEGIN_CODE DECLARATION SCOPE CONSTRUCTOR COLON CONTEXT IDENT YEAR
##
## Ends in an error in state: 320.
## Ends in an error in state: 324.
##
## scope_decl_item -> CONTEXT ident . CONTENT typ option(struct_scope_func) [ SCOPE END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> CONTEXT ident . SCOPE constructor [ SCOPE END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> CONTEXT ident . CONDITION option(struct_scope_func) [ SCOPE END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> scope_decl_item_attribute ident . CONTENT typ option(struct_scope_func) [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> scope_decl_item_attribute ident . SCOPE constructor [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> scope_decl_item_attribute ident . CONDITION option(struct_scope_func) [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DECLARATION CONTEXT ]
##
## The known suffix of the stack is as follows:
## CONTEXT ident
## scope_decl_item_attribute ident
##
expected the kind of this context item: is it a condition, a sub-scope or a data?
source_file: BEGIN_CODE DECLARATION SCOPE CONSTRUCTOR COLON CONTEXT YEAR
##
## Ends in an error in state: 319.
## Ends in an error in state: 323.
##
## scope_decl_item -> CONTEXT . ident CONTENT typ option(struct_scope_func) [ SCOPE END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> CONTEXT . ident SCOPE constructor [ SCOPE END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> CONTEXT . ident CONDITION option(struct_scope_func) [ SCOPE END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> scope_decl_item_attribute . ident CONTENT typ option(struct_scope_func) [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> scope_decl_item_attribute . ident SCOPE constructor [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DECLARATION CONTEXT ]
## scope_decl_item -> scope_decl_item_attribute . ident CONDITION option(struct_scope_func) [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DECLARATION CONTEXT ]
##
## The known suffix of the stack is as follows:
## CONTEXT
## scope_decl_item_attribute
##
expected the name of this new context item
@ -212,7 +189,7 @@ source_file: BEGIN_CODE DECLARATION STRUCT CONSTRUCTOR COLON CONDITION IDENT DEP
##
## Ends in an error in state: 303.
##
## typ -> collection_marked . typ [ SCOPE END_CODE DEPENDS DECLARATION DATA CONTEXT CONDITION ALT ]
## typ -> collection_marked . typ [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DEPENDS DECLARATION DATA CONTEXT CONDITION ALT ]
##
## The known suffix of the stack is as follows:
## collection_marked
@ -236,7 +213,7 @@ source_file: BEGIN_CODE DECLARATION STRUCT CONSTRUCTOR COLON CONDITION IDENT DEP
##
## Ends in an error in state: 307.
##
## struct_scope_func -> DEPENDS . typ [ SCOPE END_CODE DECLARATION DATA CONTEXT CONDITION ]
## struct_scope_func -> DEPENDS . typ [ SCOPE OUTPUT INTERNAL INPUT IDENT END_CODE DECLARATION DATA CONTEXT CONDITION ]
##
## The known suffix of the stack is as follows:
## DEPENDS
@ -1949,7 +1926,7 @@ expected the name of the scope being used
source_file: BEGIN_CODE YEAR
##
## Ends in an error in state: 359.
## Ends in an error in state: 363.
##
## source_file_item -> BEGIN_CODE . code END_CODE [ LAW_TEXT LAW_HEADING EOF BEGIN_METADATA BEGIN_DIRECTIVE BEGIN_CODE ]
##

16
compiler/surface/parser.mly
View File

@ -495,9 +495,17 @@ struct_scope:
}, Pos.from_lpos $sloc)
}
scope_decl_item_attribute:
| CONTEXT { Context, Pos.from_lpos $sloc }
| INPUT { Input, Pos.from_lpos $sloc }
| OUTPUT { Output, Pos.from_lpos $sloc }
| INTERNAL { Internal, Pos.from_lpos $sloc }
| { Context, Pos.from_lpos $sloc }
scope_decl_item:
| CONTEXT i = ident CONTENT t = typ func_typ = option(struct_scope_func) { (ContextData ({
| attr = scope_decl_item_attribute i = ident CONTENT t = typ func_typ = option(struct_scope_func) { (ContextData ({
scope_decl_context_item_name = i;
scope_decl_context_item_attribute = attr;
scope_decl_context_item_typ =
let (typ, typ_pos) = t in
match func_typ with
@ -508,15 +516,17 @@ scope_decl_item:
}, Pos.from_lpos $sloc);
}), Pos.from_lpos $sloc)
}
| CONTEXT i = ident SCOPE c = constructor {
| attr = scope_decl_item_attribute i = ident SCOPE c = constructor {
(ContextScope({
scope_decl_context_scope_name = i;
scope_decl_context_scope_sub_scope = c;
scope_decl_context_scope_attribute = attr;
}), Pos.from_lpos $sloc)
}
| CONTEXT i = ident _condition = CONDITION func_typ = option(struct_scope_func) {
| attr = scope_decl_item_attribute i = ident _condition = CONDITION func_typ = option(struct_scope_func) {
(ContextData ({
scope_decl_context_item_name = i;
scope_decl_context_item_attribute = attr;
scope_decl_context_item_typ =
match func_typ with
| None -> (Base (Condition), Pos.from_lpos $loc(_condition))

3
compiler/surface/parser_driver.ml
View File

@ -12,7 +12,8 @@
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Wrapping module around parser and lexer that offers the {!val: parse_source_file} API *)
(** Wrapping module around parser and lexer that offers the {!: Parser_driver.parse_source_file}
API. *)
open Sedlexing
open Utils

3
compiler/surface/parser_driver.mli
View File

@ -12,7 +12,8 @@
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Wrapping module around parser and lexer that offers the {!val: parse_source_file} API *)
(** Wrapping module around parser and lexer that offers the
[Surface.Parser_driver.parse_source_file] API. *)
open Utils

93
compiler/surface/surface.mld
View File

@ -1,77 +1,78 @@
{0 Catala surface representation }
This representation is the first in the compilation chain
(see {{: index.html#architecture} Architecture}). Its purpose is to
This representation is the first in the compilation chain
(see {{: index.html#architecture} Architecture}). Its purpose is to
host the output of the Catala parser, before any transformations have been made.
The module describing the abstract syntax tree is:
{!modules: Surface.Ast}
This representation can also be weaved into literate programming outputs
This representation can also be weaved into literate programming outputs
using the {{:literate.html} literate programming modules}.
{1 Lexing }
Relevant modules:
{!modules: Surface.Lexer 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
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
languages to use their favorite diacritics and symbols in their code.
While the parser of Catala is unique, three different lexers can be used to
While the parser of Catala is unique, three different lexers can be used to
produce the parser tokens.
{ul
{li {!module: Surface.Lexer} corresponds to a concise and programming-language-like
syntax for Catala. Examples of this syntax can be found in the test suite
{ul
{li {!module: Surface.Lexer_common} corresponds to a concise and programming-language-like
syntax for Catala. Examples of this syntax can be found in the test suite
of the compiler.}
{li {!module: Surface.Lexer_en} is the adaptation of {!module: Surface.Lexer}
{li {!module: Surface.Lexer_en} is the adaptation of {!module: Surface.Lexer_common}
with verbose English keywords matching legal concepts.}
{li {!module: Surface.Lexer_fr} is the adaptation of {!module: Surface.Lexer}
{li {!module: Surface.Lexer_fr} is the adaptation of {!module: Surface.Lexer_common}
with verbose French keywords matching legal concepts.}
}
Relevant modules:
{!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.
{!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}.
A [parser.messages] source file has been manually annotated with custom
error message for every potential erroneous state of the parser, and Menhir
automatically generated the {!module: Surface.Parser_errors} module containing
the function linking the erroneous parser states to the custom error message.
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.
Relevant modules:
{!modules: Surface.Parser Surface.Parser_driver Surface.Parser_errors}
The Catala compiler uses {{: http://cambium.inria.fr/~fpottier/menhir/} Menhir}
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
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}.
A [parser.messages] source file has been manually annotated with custom
error message for every potential erroneous state of the parser, and Menhir
automatically generated the {!module: Surface.Parser_errors} module containing
the function linking the erroneous parser states to the custom error message.
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.
{!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}.
The translation is implemented in
{!module: Surface.Desugaring}, but it relies on a helper module to perform the
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}
The desugaring consists of translating {!module: Surface.Ast} to
{!module: Desugared.Ast} of the {{: desugared.html} desugared representation}.
The translation is implemented in
{!module: Surface.Desugaring}, but it relies on a helper module to perform the
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}.

2
compiler/surface/tokens.mly
View File

@ -57,7 +57,7 @@
%token NOT BOOLEAN PERCENT DURATION
%token SCOPE FILLED NOT_EQUAL DEFINITION
%token STRUCT CONTENT IF THEN DEPENDS DECLARATION
%token CONTEXT ENUM ELSE DATE SUM
%token CONTEXT INPUT OUTPUT INTERNAL ENUM ELSE DATE SUM
%token BEGIN_METADATA MONEY DECIMAL
%token UNDER_CONDITION CONSEQUENCE LBRACKET RBRACKET
%token LABEL EXCEPTION LSQUARE RSQUARE SEMICOLON

105
compiler/utils/cli.ml
View File

@ -34,23 +34,32 @@ let trace_flag = ref false
let optimize_flag = ref false
let disable_counterexamples = ref false
open Cmdliner
let file =
Arg.(
required
& pos 1 (some file) None
& info [] ~docv:"FILE" ~doc:"Catala master file to be compiled")
& info [] ~docv:"FILE" ~doc:"Catala master file to be compiled.")
let debug = Arg.(value & flag & info [ "debug"; "d" ] ~doc:"Prints debug information")
let debug = Arg.(value & flag & info [ "debug"; "d" ] ~doc:"Prints debug information.")
let unstyled = Arg.(value & flag & info [ "unstyled" ] ~doc:"Removes styling from terminal output")
let unstyled =
Arg.(
value & flag
& info [ "unstyled"; "u" ] ~doc:"Removes styling (colors, etc.) from terminal output.")
let optimize = Arg.(value & flag & info [ "optimize"; "O" ] ~doc:"Run compiler optimizations")
let optimize = Arg.(value & flag & info [ "optimize"; "O" ] ~doc:"Run compiler optimizations.")
let trace_opt =
Arg.(
value & flag & info [ "trace"; "t" ] ~doc:"Displays a trace of the interpreter's computation")
value & flag
& info [ "trace"; "t" ]
~doc:
"Displays a trace of the interpreter's computation or generates logging instructions in \
translate programs.")
let avoid_exceptions =
Arg.(
@ -60,47 +69,68 @@ let avoid_exceptions =
let wrap_weaved_output =
Arg.(
value & flag
& info [ "wrap"; "w" ] ~doc:"Wraps literate programming output with a minimal preamble")
& info [ "wrap"; "w" ] ~doc:"Wraps literate programming output with a minimal preamble.")
let backend =
Arg.(
required
& pos 0 (some string) None
& info [] ~docv:"BACKEND"
~doc:
"Backend selection among: Interpret, OCaml, Python, LaTeX, Makefile, Html, Dcalc, \
Scopelang")
& info [] ~docv:"COMMAND"
~doc:"Backend selection (see the list of commands for available options).")
type backend_option = Latex | Makefile | Html | Run | OCaml | Python | Dcalc | Scopelang
type backend_option =
| Latex
| Makefile
| Html
| Interpret
| Typecheck
| OCaml
| Python
| Dcalc
| Scopelang
| Proof
let language =
Arg.(
value
& opt (some string) None
& info [ "l"; "language" ] ~docv:"LANG" ~doc:"Input language among: en, fr, pl")
& info [ "l"; "language" ] ~docv:"LANG" ~doc:"Input language among: en, fr, pl.")
let max_prec_digits_opt =
Arg.(
value
& opt (some int) None
& info [ "p"; "max_digits_printed" ] ~docv:"LANG"
~doc:"Maximum number of significant digits printed for decimal results (default 20)")
& info [ "p"; "max_digits_printed" ] ~docv:"DIGITS"
~doc:"Maximum number of significant digits printed for decimal results (default 20).")
let disable_counterexamples_opt =
Arg.(
value & flag
& info [ "disable_counterexamples" ]
~doc:
"Disables the search for counterexamples in proof mode. Useful when you want a \
deterministic output from the Catala compiler, since provers can have some randomness \
in them.")
let ex_scope =
Arg.(
value & opt (some string) None & info [ "s"; "scope" ] ~docv:"SCOPE" ~doc:"Scope to be executed")
value
& opt (some string) None
& info [ "s"; "scope" ] ~docv:"SCOPE" ~doc:"Scope to be focused on.")
let output =
Arg.(
value
& opt (some string) None
& info [ "output"; "o" ] ~docv:"OUTPUT"
~doc:"$(i, OUTPUT) is the file that will contain the output of the compiler")
~doc:
"$(i, OUTPUT) is the file that will contain the output of the compiler. Defaults to \
$(i,FILE).$(i,EXT) where $(i,EXT) depends on the chosen backend.")
let catala_t f =
Term.(
const f $ file $ debug $ unstyled $ wrap_weaved_output $ avoid_exceptions $ backend $ language
$ max_prec_digits_opt $ trace_opt $ optimize $ ex_scope $ output)
$ max_prec_digits_opt $ trace_opt $ disable_counterexamples_opt $ optimize $ ex_scope $ output)
let version = "0.5.0"
@ -114,12 +144,42 @@ let info =
`P
"Catala is a domain-specific language for deriving faithful-by-construction algorithms \
from legislative texts.";
`S Manpage.s_commands;
`I
( "$(b,Intepret)",
"Runs the interpreter on the Catala program, executing the scope specified by the \
$(b,-s) option assuming no additional external inputs." );
`I ("$(b,Typecheck)", "Parses and typechecks a Catala program, without interpreting it.");
`I
( "$(b,Proof)",
"Generates and proves verification conditions about the well-behaved execution of the \
Catala program." );
`I ("$(b,OCaml)", "Generates an OCaml translation of the Catala program.");
`I ("$(b,Python)", "Generates a Python translation of the Catala program.");
`I ("$(b,LaTeX)", "Weaves a LaTeX literate programming output of the Catala program.");
`I ("$(b,HTML)", "Weaves an HTML literate programming output of the Catala program.");
`I
( "$(b,Makefile)",
"Generates a Makefile-compatible list of the file dependencies of a Catala program." );
`I
( "$(b,Scopelang)",
"Prints a debugging verbatim of the scope language intermediate representation of the \
Catala program. Use the $(b,-s) option to restrict the output to a particular scope." );
`I
( "$(b,Dcalc)",
"Prints a debugging verbatim of the scope language intermediate representation of the \
Catala program. Use the $(b,-s) option to restrict the output to a particular scope." );
`S Manpage.s_authors;
`P "Denis Merigoux <denis.merigoux@inria.fr>";
`P "The authors are listed by alphabetical order.";
`P "Nicolas Chataing <nicolas.chataing@ens.fr>";
`P "Alain Delaët-Tixeuil <alain.delaet--tixeuil@inria.fr>";
`P "Aymeric Fromherz <aymeric.fromherz@inria.fr>";
`P "Louis Gesbert <louis.gesbert@ocamlpro.com>";
`P "Denis Merigoux <denis.merigoux@inria.fr>";
`P "Emile Rolley <erolley@tutamail.com>";
`S Manpage.s_examples;
`P "Typical usage:";
`Pre "catala LaTeX file.catala";
`Pre "catala Interpret -s Foo file.catala_en";
`Pre "catala Ocaml -o target/file.ml file.catala_en";
`S Manpage.s_bugs;
`P "Please file bug reports at https://github.com/CatalaLang/catala/issues";
]
@ -136,6 +196,11 @@ let time : float ref = ref (Unix.gettimeofday ())
let print_with_style (styles : ANSITerminal.style list) (str : ('a, unit, string) format) =
if !style_flag then ANSITerminal.sprintf styles str else Printf.sprintf str
let format_with_style (styles : ANSITerminal.style list) fmt (str : string) =
if !style_flag then
Format.pp_print_as fmt (String.length str) (ANSITerminal.sprintf styles "%s" str)
else Format.pp_print_string fmt str
let time_marker () =
let new_time = Unix.gettimeofday () in
let old_time = !time in

21
compiler/utils/cli.mli
View File

@ -35,6 +35,9 @@ val max_prec_digits : int ref
val trace_flag : bool ref
val disable_counterexamples : bool ref
(** Disables model-generated counterexamples for proofs that fail. *)
(** {2 CLI terms} *)
val file : string Cmdliner.Term.t
@ -49,7 +52,17 @@ val wrap_weaved_output : bool Cmdliner.Term.t
val backend : string Cmdliner.Term.t
type backend_option = Latex | Makefile | Html | Run | OCaml | Python | Dcalc | Scopelang
type backend_option =
| Latex
| Makefile
| Html
| Interpret
| Typecheck
| OCaml
| Python
| Dcalc
| Scopelang
| Proof
val language : string option Cmdliner.Term.t
@ -70,13 +83,13 @@ val catala_t :
int option ->
bool ->
bool ->
bool ->
string option ->
string option ->
'a) ->
'a Cmdliner.Term.t
(** Main entry point:
[catala_t file debug unstyled wrap_weaved_output avoid_exceptions backend language max_prec_digits_opt trace_opt optimize
ex_scope output] *)
[catala_t file debug unstyled wrap_weaved_output avoid_exceptions backend language max_prec_digits_opt trace_opt disable_counterexamples optimize ex_scope output] *)
val version : string
@ -88,6 +101,8 @@ val info : Cmdliner.Term.info
val print_with_style : ANSITerminal.style list -> ('a, unit, string) format -> 'a
val format_with_style : ANSITerminal.style list -> Format.formatter -> string -> unit
val debug_marker : unit -> string
val error_marker : unit -> string

38
compiler/utils/utils.mld
View File

@ -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}

309
compiler/verification/conditions.ml Normal file
View File

@ -0,0 +1,309 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 2022 Inria, contributor: Denis Merigoux
<denis.merigoux@inria.fr>, Alain Delaët <alain.delaet--tixeuil@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
open Utils
open Dcalc
open Ast
(** {1 Helpers and type definitions}*)
type vc_return = expr Pos.marked * typ Pos.marked VarMap.t
(** The return type of VC generators is the VC expression plus the types of any locally free
variable inside that expression. *)
type ctx = { decl : decl_ctx; input_vars : Var.t list }
let conjunction (args : vc_return list) (pos : Pos.t) : vc_return =
let acc, list =
match args with hd :: tl -> (hd, tl) | [] -> (((ELit (LBool true), pos), VarMap.empty), [])
in
List.fold_left
(fun (acc, acc_ty) (arg, arg_ty) ->
( (EApp ((EOp (Binop And), pos), [ arg; acc ]), pos),
VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty ))
acc list
let negation ((arg, arg_ty) : vc_return) (pos : Pos.t) : vc_return =
((EApp ((EOp (Unop Not), pos), [ arg ]), pos), arg_ty)
let disjunction (args : vc_return list) (pos : Pos.t) : vc_return =
let acc, list =
match args with hd :: tl -> (hd, tl) | [] -> (((ELit (LBool false), pos), VarMap.empty), [])
in
List.fold_left
(fun ((acc, acc_ty) : vc_return) (arg, arg_ty) ->
( (EApp ((EOp (Binop Or), pos), [ arg; acc ]), pos),
VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty ))
acc list
(** [half_product \[a1,...,an\] \[b1,...,bm\] returns \[(a1,b1),...(a1,bn),...(an,b1),...(an,bm)\]] *)
let half_product (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list =
l1
|> List.mapi (fun i ei -> List.filteri (fun j _ -> i < j) l2 |> List.map (fun ej -> (ei, ej)))
|> List.concat
(** This code skims through the topmost layers of the terms like this:
[log (error_on_empty < reentrant_variable () | true :- e1 >)] for scope variables, or
[fun () -> e1] for subscope variables. But what we really want to analyze is only [e1], so we
match this outermost structure explicitely and have a clean verification condition generator
that only runs on [e1] *)
let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Pos.marked) : expr Pos.marked =
match Pos.unmark e with
| EApp
( (EOp (Unop (Log _)), _),
[
( ErrorOnEmpty
( EDefault
( [ (EApp ((EVar (x, _), _), [ (ELit LUnit, _) ]), _) ],
(ELit (LBool true), _),
cons ),
_ ),
_ );
] )
when List.exists (fun x' -> Bindlib.eq_vars x x') ctx.input_vars ->
(* scope variables*)
cons
| EAbs ((binder, _), [ (TLit TUnit, _) ]) -> (
(* sub-scope variables *)
let _, body = Bindlib.unmbind binder in
match Pos.unmark body with
| EApp ((EOp (Unop (Log _)), _), [ arg ]) -> arg
| _ ->
Errors.raise_spanned_error
(Format.asprintf
"Internal error: this expression does not have the structure expected by the VC \
generator:\n\
%a"
(Print.format_expr ~debug:true ctx.decl)
e)
(Pos.get_position e))
| _ ->
Errors.raise_spanned_error
(Format.asprintf
"Internal error: this expression does not have the structure expected by the VC \
generator:\n\
%a"
(Print.format_expr ~debug:true ctx.decl)
e)
(Pos.get_position e)
(** {1 Verification conditions generator}*)
(** [generate_vc_must_not_return_empty e] returns the dcalc boolean expression [b] such that if [b]
is true, then [e] will never return an empty error. It also returns a map of all the types of
locally free variables inside the expression. *)
let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Pos.marked) : vc_return =
let out =
match Pos.unmark e with
| ETuple (args, _) | EArray args ->
conjunction (List.map (generate_vc_must_not_return_empty ctx) args) (Pos.get_position e)
| EMatch (arg, arms, _) ->
conjunction
(List.map (generate_vc_must_not_return_empty ctx) (arg :: arms))
(Pos.get_position e)
| ETupleAccess (e1, _, _, _) | EInj (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 ->
(generate_vc_must_not_return_empty ctx) e1
| EAbs (binder, typs) ->
(* Hot take: for a function never to return an empty error when called, it has to do
so whatever its input. So we universally quantify over the variable of the function
when inspecting the body, resulting in simply traversing through in the code here. *)
let vars, body = Bindlib.unmbind (Pos.unmark binder) in
let vc_body_expr, vc_body_ty = (generate_vc_must_not_return_empty ctx) body in
( vc_body_expr,
List.fold_left
(fun acc (var, ty) -> VarMap.add var ty acc)
vc_body_ty
(List.map2 (fun x y -> (x, y)) (Array.to_list vars) typs) )
| EApp (f, args) ->
(* We assume here that function calls never return empty error, which implies
all functions have been checked never to return empty errors. *)
conjunction
(List.map (generate_vc_must_not_return_empty ctx) (f :: args))
(Pos.get_position e)
| EIfThenElse (e1, e2, e3) ->
conjunction
(List.map (generate_vc_must_not_return_empty ctx) [ e1; e2; e3 ])
(Pos.get_position e)
| ELit LEmptyError -> (Pos.same_pos_as (ELit (LBool false)) e, VarMap.empty)
| EVar _
(* Per default calculus semantics, you cannot call a function with an argument
that evaluates to the empty error. Thus, all variable evaluate to non-empty-error terms. *)
| ELit _ | EOp _ ->
(Pos.same_pos_as (ELit (LBool true)) e, VarMap.empty)
| EDefault (exceptions, just, cons) ->
(* <e1 ... en | ejust :- econs > never returns empty if and only if:
- first we look if e1 .. en ejust can return empty;
- if no, we check that if ejust is true, whether econs can return empty.
*)
disjunction
(List.map (generate_vc_must_not_return_empty ctx) exceptions
@ [
conjunction
[
generate_vc_must_not_return_empty ctx just;
(let vc_just_expr, vc_just_ty = generate_vc_must_not_return_empty ctx cons in
( ( EIfThenElse
( just,
(* Comment from Alain: the justification is not checked for holding an default term.
In such cases, we need to encode the logic of the default terms within
the generation of the verification condition (Z3encoding.translate_expr).
Answer from Denis: Normally, there is a structural invariant from the
surface language to intermediate representation translation preventing
any default terms to appear in justifications.*)
vc_just_expr,
(ELit (LBool false), Pos.get_position e) ),
Pos.get_position e ),
vc_just_ty ));
]
(Pos.get_position e);
])
(Pos.get_position e)
in
out
[@@ocamlformat "wrap-comments=false"]
(** [generate_vs_must_not_return_confict e] returns the dcalc boolean expression [b] such that if
[b] is true, then [e] will never return a conflict error. It also returns a map of all the types
of locally free variables inside the expression. *)
let rec generate_vs_must_not_return_confict (ctx : ctx) (e : expr Pos.marked) : vc_return =
let out =
(* See the code of [generate_vc_must_not_return_empty] for a list of invariants on which this
function relies on. *)
match Pos.unmark e with
| ETuple (args, _) | EArray args ->
conjunction (List.map (generate_vs_must_not_return_confict ctx) args) (Pos.get_position e)
| EMatch (arg, arms, _) ->
conjunction
(List.map (generate_vs_must_not_return_confict ctx) (arg :: arms))
(Pos.get_position e)
| ETupleAccess (e1, _, _, _) | EInj (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 ->
generate_vs_must_not_return_confict ctx e1
| EAbs (binder, typs) ->
let vars, body = Bindlib.unmbind (Pos.unmark binder) in
let vc_body_expr, vc_body_ty = (generate_vs_must_not_return_confict ctx) body in
( vc_body_expr,
List.fold_left
(fun acc (var, ty) -> VarMap.add var ty acc)
vc_body_ty
(List.map2 (fun x y -> (x, y)) (Array.to_list vars) typs) )
| EApp (f, args) ->
conjunction
(List.map (generate_vs_must_not_return_confict ctx) (f :: args))
(Pos.get_position e)
| EIfThenElse (e1, e2, e3) ->
conjunction
(List.map (generate_vs_must_not_return_confict ctx) [ e1; e2; e3 ])
(Pos.get_position e)
| EVar _ | ELit _ | EOp _ -> (Pos.same_pos_as (ELit (LBool true)) e, VarMap.empty)
| EDefault (exceptions, just, cons) ->
(* <e1 ... en | ejust :- econs > never returns conflict if and only if:
- neither e1 nor ... nor en nor ejust nor econs return conflict
- there is no two differents ei ej that are not empty. *)
let quadratic =
negation
(disjunction
(List.map
(fun (e1, e2) ->
conjunction
[
generate_vc_must_not_return_empty ctx e1;
generate_vc_must_not_return_empty ctx e2;
]
(Pos.get_position e))
(half_product exceptions exceptions))
(Pos.get_position e))
(Pos.get_position e)
in
let others =
List.map (generate_vs_must_not_return_confict ctx) (just :: cons :: exceptions)
in
let out = conjunction (quadratic :: others) (Pos.get_position e) in
out
in
out
[@@ocamlformat "wrap-comments=false"]
(** {1 Interface}*)
type verification_condition_kind = NoEmptyError | NoOverlappingExceptions
type verification_condition = {
vc_guard : expr Pos.marked;
(* should have type bool *)
vc_kind : verification_condition_kind;
vc_scope : ScopeName.t;
vc_variable : Var.t Pos.marked;
vc_free_vars_typ : typ Pos.marked VarMap.t;
}
let generate_verification_conditions (p : program) : verification_condition list =
List.fold_left
(fun acc (s_name, _s_var, s_body) ->
let ctx = { decl = p.decl_ctx; input_vars = [] } in
let acc, _ =
List.fold_left
(fun (acc, ctx) s_let ->
match s_let.scope_let_kind with
| DestructuringInputStruct ->
(acc, { ctx with input_vars = Pos.unmark s_let.scope_let_var :: ctx.input_vars })
| ScopeVarDefinition | SubScopeVarDefinition ->
(* For scope variables, we should check both that they never evaluate to emptyError
nor conflictError. But for subscope variable definitions, what we're really doing
is adding exceptions to something defined in the subscope so we just ought to
verify only that the exceptions overlap. *)
let e =
match_and_ignore_outer_reentrant_default ctx (Bindlib.unbox s_let.scope_let_expr)
in
let vc_confl, vc_confl_typs = generate_vs_must_not_return_confict ctx e in
let vc_confl =
if !Cli.optimize_flag then
Bindlib.unbox (Optimizations.optimize_expr p.decl_ctx vc_confl)
else vc_confl
in
let vc_list =
[
{
vc_guard = Pos.same_pos_as (Pos.unmark vc_confl) e;
vc_kind = NoOverlappingExceptions;
vc_free_vars_typ = vc_confl_typs;
vc_scope = s_name;
vc_variable = s_let.scope_let_var;
};
]
in
let vc_list =
match s_let.scope_let_kind with
| ScopeVarDefinition ->
let vc_empty, vc_empty_typs = generate_vc_must_not_return_empty ctx e in
let vc_empty =
if !Cli.optimize_flag then
Bindlib.unbox (Optimizations.optimize_expr p.decl_ctx vc_empty)
else vc_empty
in
{
vc_guard = Pos.same_pos_as (Pos.unmark vc_empty) e;
vc_kind = NoEmptyError;
vc_free_vars_typ = vc_empty_typs;
vc_scope = s_name;
vc_variable = s_let.scope_let_var;
}
:: vc_list
| _ -> vc_list
in
(vc_list @ acc, ctx)
| _ -> (acc, ctx))
(acc, ctx) s_body.scope_body_lets
in
acc)
[] p.scopes

33
compiler/verification/conditions.mli Normal file
View File

@ -0,0 +1,33 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 2022 Inria, contributor: Denis Merigoux
<denis.merigoux@inria.fr>, Alain Delaët <alain.delaet--tixeuil@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Generates verification conditions from scope definitions *)
type verification_condition_kind =
| NoEmptyError
(** This verification condition checks whether a definition never returns an empty error *)
| NoOverlappingExceptions
(** This verification condition checks whether a definition never returns a conflict error *)
type verification_condition = {
vc_guard : Dcalc.Ast.expr Utils.Pos.marked; (** This expression should have type [bool]*)
vc_kind : verification_condition_kind;
vc_scope : Dcalc.Ast.ScopeName.t;
vc_variable : Dcalc.Ast.Var.t Utils.Pos.marked;
vc_free_vars_typ : Dcalc.Ast.typ Utils.Pos.marked Dcalc.Ast.VarMap.t;
(** Types of the locally free variables in [vc_guard]. The types of other free variables
linked to scope variables can be obtained with [Dcalc.Ast.variable_types]. *)
}
val generate_verification_conditions : Dcalc.Ast.program -> verification_condition list

8
compiler/verification/dune Normal file
View File

@ -0,0 +1,8 @@
(library
(name verification)
(public_name catala.verification)
(libraries bindlib utils dcalc runtime z3 calendar))
(documentation
(package catala)
(mld_files verification))

157
compiler/verification/io.ml Normal file
View File

@ -0,0 +1,157 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 2022 Inria, contributor: Aymeric Fromherz
<aymeric.fromherz@inria.fr>, Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
open Utils
open Dcalc.Ast
module type Backend = sig
val init_backend : unit -> unit
type backend_context
val make_context : decl_ctx -> typ Pos.marked VarMap.t -> backend_context
type vc_encoding
val print_encoding : vc_encoding -> string
type model
type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
val solve_vc_encoding : backend_context -> vc_encoding -> solver_result
val print_model : backend_context -> model -> string
val is_model_empty : model -> bool
val translate_expr :
backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
end
module type BackendIO = sig
val init_backend : unit -> unit
type backend_context
val make_context : decl_ctx -> typ Pos.marked VarMap.t -> backend_context
type vc_encoding
val translate_expr :
backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
type model
type vc_encoding_result = Success of vc_encoding * backend_context | Fail of string
val print_positive_result : Conditions.verification_condition -> string
val print_negative_result :
Conditions.verification_condition -> backend_context -> model option -> string
val encode_and_check_vc :
Dcalc.Ast.decl_ctx -> Conditions.verification_condition * vc_encoding_result -> unit
end
module MakeBackendIO (B : Backend) = struct
let init_backend = B.init_backend
type backend_context = B.backend_context
let make_context = B.make_context
type vc_encoding = B.vc_encoding
let translate_expr = B.translate_expr
type model = B.model
type vc_encoding_result = Success of B.vc_encoding * B.backend_context | Fail of string
let print_positive_result (vc : Conditions.verification_condition) : string =
match vc.Conditions.vc_kind with
| Conditions.NoEmptyError ->
Format.asprintf "%s This variable never returns an empty error"
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
| Conditions.NoOverlappingExceptions ->
Format.asprintf "%s No two exceptions to ever overlap for this variable"
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
let print_negative_result (vc : Conditions.verification_condition) (ctx : B.backend_context)
(model : B.model option) : string =
let var_and_pos =
match vc.Conditions.vc_kind with
| Conditions.NoEmptyError ->
Format.asprintf "%s This variable might return an empty error:\n%s"
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
(Pos.retrieve_loc_text (Pos.get_position vc.vc_variable))
| Conditions.NoOverlappingExceptions ->
Format.asprintf "%s At least two exceptions overlap for this variable:\n%s"
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
(Pos.retrieve_loc_text (Pos.get_position vc.vc_variable))
in
let counterexample : string option =
match model with
| None ->
Some
"The solver did not manage to generate a counterexample to explain the faulty behavior."
| Some model ->
if B.is_model_empty model then None
else
Some
(Format.asprintf
"The solver generated the following counterexample to explain the faulty behavior:\n\
%s"
(B.print_model ctx model))
in
var_and_pos
^ match counterexample with None -> "" | Some counterexample -> "\n" ^ counterexample
(** [encode_and_check_vc] spawns a new Z3 solver and tries to solve the expression [vc] **)
let encode_and_check_vc (decl_ctx : decl_ctx)
(vc : Conditions.verification_condition * vc_encoding_result) : unit =
let vc, z3_vc = vc in
Cli.debug_print
(Format.asprintf "For this variable:\n%s\n"
(Pos.retrieve_loc_text (Pos.get_position vc.Conditions.vc_guard)));
Cli.debug_print
(Format.asprintf "This verification condition was generated for %s:@\n%a"
(Cli.print_with_style [ ANSITerminal.yellow ] "%s"
(match vc.vc_kind with
| Conditions.NoEmptyError -> "the variable definition never to return an empty error"
| NoOverlappingExceptions -> "no two exceptions to ever overlap"))
(Dcalc.Print.format_expr decl_ctx)
vc.vc_guard);
match z3_vc with
| Success (encoding, backend_ctx) -> (
Cli.debug_print
(Format.asprintf "The translation to Z3 is the following:@\n%s"
(B.print_encoding encoding));
match B.solve_vc_encoding backend_ctx encoding with
| ProvenTrue -> Cli.result_print (print_positive_result vc)
| ProvenFalse model -> Cli.error_print (print_negative_result vc backend_ctx model)
| Unknown -> failwith "The solver failed at proving or disproving the VC")
| Fail msg -> Cli.error_print (Format.asprintf "The translation to Z3 failed:@\n%s" msg)
end

73
compiler/verification/io.mli Normal file
View File

@ -0,0 +1,73 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 2022 Inria, contributor: Aymeric Fromherz
<aymeric.fromherz@inria.fr>, Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Common code for handling the IO of all proof backends supported *)
module type Backend = sig
val init_backend : unit -> unit
type backend_context
val make_context :
Dcalc.Ast.decl_ctx -> Dcalc.Ast.typ Utils.Pos.marked Dcalc.Ast.VarMap.t -> backend_context
type vc_encoding
val print_encoding : vc_encoding -> string
type model
type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
val solve_vc_encoding : backend_context -> vc_encoding -> solver_result
val print_model : backend_context -> model -> string
val is_model_empty : model -> bool
val translate_expr :
backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
end
module type BackendIO = sig
val init_backend : unit -> unit
type backend_context
val make_context :
Dcalc.Ast.decl_ctx -> Dcalc.Ast.typ Utils.Pos.marked Dcalc.Ast.VarMap.t -> backend_context
type vc_encoding
val translate_expr :
backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
type model
type vc_encoding_result = Success of vc_encoding * backend_context | Fail of string
val print_positive_result : Conditions.verification_condition -> string
val print_negative_result :
Conditions.verification_condition -> backend_context -> model option -> string
val encode_and_check_vc :
Dcalc.Ast.decl_ctx -> Conditions.verification_condition * vc_encoding_result -> unit
end
module MakeBackendIO : functor (B : Backend) ->
BackendIO
with type vc_encoding = B.vc_encoding
and type backend_context = B.backend_context
and type model = B.model

43
compiler/verification/solver.ml Normal file
View File

@ -0,0 +1,43 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 2022 Inria, contributor: Aymeric Fromherz
<aymeric.fromherz@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
open Dcalc.Ast
(** [solve_vc] is the main entry point of this module. It takes a list of expressions [vcs]
corresponding to verification conditions that must be discharged by Z3, and attempts to solve
them **)
let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verification_condition list) :
unit =
(* Right now we only use the Z3 backend but the functorial interface should make it easy to mix
and match different proof backends. *)
Z3backend.Io.init_backend ();
let z3_vcs =
List.map
(fun vc ->
( vc,
try
let ctx, z3_vc =
Z3backend.Io.translate_expr
(Z3backend.Io.make_context decl_ctx
(VarMap.union
(fun _ _ _ ->
failwith "[Proof encoding]: A Variable cannot be both free and bound")
(variable_types prgm) vc.Conditions.vc_free_vars_typ))
(Bindlib.unbox (Dcalc.Optimizations.remove_all_logs vc.Conditions.vc_guard))
in
Z3backend.Io.Success (z3_vc, ctx)
with Failure msg -> Fail msg ))
vcs
in
List.iter (Z3backend.Io.encode_and_check_vc decl_ctx) z3_vcs

18
compiler/verification/solver.mli Normal file
View File

@ -0,0 +1,18 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 2022 Inria, contributor: Aymeric Fromherz
<aymeric.fromherz@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Solves verification conditions using various proof backends *)
val solve_vc :
Dcalc.Ast.program -> Dcalc.Ast.decl_ctx -> Conditions.verification_condition list -> unit

41
compiler/verification/verification.mld Normal file
View File

@ -0,0 +1,41 @@
{0 Verification}
{1 Generating verification conditions }
From the {{: dcalc.html} Dcalc} intermediate representation, the module
{!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: 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 {!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.
Related modules:
{!modules: Verification.Z3backend}

609
compiler/verification/z3backend.ml Normal file
View File

@ -0,0 +1,609 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 2022 Inria, contributor: Aymeric Fromherz
<aymeric.fromherz@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
open Utils
open Dcalc
open Ast
open Z3
module StringMap : Map.S with type key = String.t = Map.Make (String)
type context = {
ctx_z3 : Z3.context;
(* The Z3 context, used to create symbols and expressions *)
ctx_decl : decl_ctx;
(* The declaration context from the Catala program, containing information to precisely pretty
print Catala expressions *)
ctx_var : typ Pos.marked VarMap.t;
(* A map from Catala variables to their types, needed to create Z3 expressions of the right
sort *)
ctx_funcdecl : FuncDecl.func_decl VarMap.t;
(* A map from Catala function names (represented as variables) to Z3 function declarations, used
to only define once functions in Z3 queries *)
ctx_z3vars : Var.t StringMap.t;
(* A map from strings, corresponding to Z3 symbol names, to the Catala variable they represent.
Used when to pretty-print Z3 models when a counterexample is generated *)
ctx_z3datatypes : Sort.sort EnumMap.t;
(* A map from Catala enumeration names to the corresponding Z3 sort, from which we can retrieve
constructors and accessors *)
ctx_z3matchsubsts : Expr.expr VarMap.t;
(* A map from Catala temporary variables, generated when translating a match, to the corresponding
enum accessor call as a Z3 expression *)
ctx_z3structs : Sort.sort StructMap.t;
(* A map from Catala struct names to the corresponding Z3 sort, from which we can retrieve the
constructor and the accessors *)
}
(** The context contains all the required information to encode a VC represented as a Catala term to
Z3. The fields [ctx_decl] and [ctx_var] are computed before starting the translation to Z3, and
are thus unmodified throughout the translation. The [ctx_z3] context is an OCaml abstraction on
top of an underlying C++ imperative implementation, it is therefore only created once.
Unfortunately, the maps [ctx_funcdecl], [ctx_z3vars], and [ctx_z3datatypes] are computed
dynamically during the translation requiring us to pass the context around in a functional way **)
(** [add_funcdecl] adds the mapping between the Catala variable [v] and the Z3 function declaration
[fd] to the context **)
let add_funcdecl (v : Var.t) (fd : FuncDecl.func_decl) (ctx : context) : context =
{ ctx with ctx_funcdecl = VarMap.add v fd ctx.ctx_funcdecl }
(** [add_z3var] adds the mapping between [name] and the Catala variable [v] to the context **)
let add_z3var (name : string) (v : Var.t) (ctx : context) : context =
{ ctx with ctx_z3vars = StringMap.add name v ctx.ctx_z3vars }
(** [add_z3enum] adds the mapping between the Catala enumeration [enum] and the corresponding Z3
datatype [sort] to the context **)
let add_z3enum (enum : EnumName.t) (sort : Sort.sort) (ctx : context) : context =
{ ctx with ctx_z3datatypes = EnumMap.add enum sort ctx.ctx_z3datatypes }
(** [add_z3var] adds the mapping between temporary variable [v] and the Z3 expression [e]
representing an accessor application to the context **)
let add_z3matchsubst (v : Var.t) (e : Expr.expr) (ctx : context) : context =
{ ctx with ctx_z3matchsubsts = VarMap.add v e ctx.ctx_z3matchsubsts }
(** [add_z3struct] adds the mapping between the Catala struct [s] and the corresponding Z3 datatype
[sort] to the context **)
let add_z3struct (s : StructName.t) (sort : Sort.sort) (ctx : context) : context =
{ ctx with ctx_z3structs = StructMap.add s sort ctx.ctx_z3structs }
(** For the Z3 encoding of Catala programs, we define the "day 0" as Jan 1, 1900 **)
let base_day = CalendarLib.Date.make 1900 1 1
(** [unique_name] returns the full, unique name corresponding to variable [v], as given by Bindlib **)
let unique_name (v : Var.t) : string =
Format.asprintf "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
(** [date_to_int] translates [date] to an integer corresponding to the number of days since Jan 1,
1900 **)
let date_to_int (d : Runtime.date) : int =
(* Alternatively, could expose this from Runtime as a (noop) coercion, but would allow to break
abstraction more easily elsewhere *)
let date : CalendarLib.Date.t = CalendarLib.Printer.Date.from_string (Runtime.date_to_string d) in
let period = CalendarLib.Date.sub date base_day in
CalendarLib.Date.Period.nb_days period
(** [date_of_year] translates a [year], represented as an integer into an OCaml date corresponding
to Jan 1st of the same year *)
let date_of_year (year : int) = Runtime.date_of_numbers year 1 1
(** Returns the date (as a string) corresponding to nb days after the base day, defined here as Jan
1, 1900 **)
let nb_days_to_date (nb : int) : string =
CalendarLib.Printer.Date.to_string
(CalendarLib.Date.add base_day (CalendarLib.Date.Period.day nb))
(** [print_z3model_expr] pretty-prints the value [e] given by a Z3 model according to the Catala
type [ty], corresponding to [e] **)
let rec print_z3model_expr (ctx : context) (ty : typ Pos.marked) (e : Expr.expr) : string =
let print_lit (ty : typ_lit) =
match ty with
(* TODO: Print boolean according to current language *)
| TBool -> Expr.to_string e
| TUnit -> failwith "[Z3 model]: Pretty-printing of unit literals not supported"
| TInt -> Expr.to_string e
| TRat -> failwith "[Z3 model]: Pretty-printing of rational literals not supported"
(* TODO: Print the right money symbol according to language *)
| TMoney ->
let z3_str = Expr.to_string e in
(* The Z3 model returns an integer corresponding to the amount of cents. We reformat it as
dollars *)
let to_dollars s = Runtime.money_to_string (Runtime.money_of_cents_string s) in
if String.contains z3_str '-' then
Format.asprintf "-%s $" (to_dollars (String.sub z3_str 3 (String.length z3_str - 4)))
else Format.asprintf "%s $" (to_dollars z3_str)
(* The Z3 date representation corresponds to the number of days since Jan 1, 1900. We
pretty-print it as the actual date *)
(* TODO: Use differnt dates conventions depending on the language ? *)
| TDate -> nb_days_to_date (int_of_string (Expr.to_string e))
| TDuration -> failwith "[Z3 model]: Pretty-printing of duration literals not supported"
in
match Pos.unmark ty with
| TLit ty -> print_lit ty
| TTuple (_, Some name) ->
let s = StructMap.find name ctx.ctx_decl.ctx_structs in
let get_fieldname (fn : StructFieldName.t) : string =
Pos.unmark (StructFieldName.get_info fn)
in
let fields =
List.map2
(fun (fn, ty) e ->
Format.asprintf "-- %s : %s" (get_fieldname fn) (print_z3model_expr ctx ty e))
s (Expr.get_args e)
in
let fields_str = String.concat " " fields in
Format.asprintf "%s { %s }" (Pos.unmark (StructName.get_info name)) fields_str
| TTuple (_, None) -> failwith "[Z3 model]: Pretty-printing of unnamed structs not supported"
| TEnum (_tys, name) ->
(* The value associated to the enum is a single argument *)
let e' = List.hd (Expr.get_args e) in
let fd = Expr.get_func_decl e in
let fd_name = Symbol.to_string (FuncDecl.get_name fd) in
let enum_ctrs = EnumMap.find name ctx.ctx_decl.ctx_enums in
let case =
List.find
(fun (ctr, _) -> String.equal fd_name (Pos.unmark (EnumConstructor.get_info ctr)))
enum_ctrs
in
Format.asprintf "%s (%s)" fd_name (print_z3model_expr ctx (snd case) e')
| TArrow _ -> failwith "[Z3 model]: Pretty-printing of arrows not supported"
| TArray _ -> failwith "[Z3 model]: Pretty-printing of arrays not supported"
| TAny -> failwith "[Z3 model]: Pretty-printing of Any not supported"
(** [print_model] pretty prints a Z3 model, used to exhibit counter examples where verification
conditions are not satisfied. The context [ctx] is useful to retrieve the mapping between Z3
variables and Catala variables, and to retrieve type information about the variables that was
lost during the translation (e.g., by translating a date to an integer) **)
let print_model (ctx : context) (model : Model.model) : string =
if !Cli.disable_counterexamples then
Format.asprintf "%s counterexamples disabled"
(Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
else
let decls = Model.get_decls model in
Format.asprintf "%a"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n")
(fun fmt d ->
match Model.get_const_interp model d with
(* TODO: Better handling of this case *)
| None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution"
(* Prints "name : value\n" *)
| Some e ->
if FuncDecl.get_arity d = 0 then
(* Constant case *)
let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
let v = StringMap.find symbol_name ctx.ctx_z3vars in
Format.fprintf fmt "%s %s : %s"
(Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
(Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
(print_z3model_expr ctx (VarMap.find v ctx.ctx_var) e)
else failwith "[Z3 model]: Printing of functions is not yet supported"))
decls
(** [translate_typ_lit] returns the Z3 sort corresponding to the Catala literal type [t] **)
let translate_typ_lit (ctx : context) (t : typ_lit) : Sort.sort =
match t with
| TBool -> Boolean.mk_sort ctx.ctx_z3
| TUnit -> failwith "[Z3 encoding] TUnit type not supported"
| TInt -> Arithmetic.Integer.mk_sort ctx.ctx_z3
| TRat -> failwith "[Z3 encoding] TRat type not supported"
| TMoney -> Arithmetic.Integer.mk_sort ctx.ctx_z3
(* Dates are encoded as integers, corresponding to the number of days since Jan 1, 1900 *)
| TDate -> Arithmetic.Integer.mk_sort ctx.ctx_z3
| TDuration -> failwith "[Z3 encoding] TDuration type not supported"
(** [translate_typ] returns the Z3 sort correponding to the Catala type [t] **)
let rec translate_typ (ctx : context) (t : typ) : context * Sort.sort =
match t with
| TLit t -> (ctx, translate_typ_lit ctx t)
| TTuple (_, Some name) -> find_or_create_struct ctx name
| TTuple (_, None) -> failwith "[Z3 encoding] TTuple type of unnamed struct not supported"
| TEnum (_, e) -> find_or_create_enum ctx e
| TArrow _ -> failwith "[Z3 encoding] TArrow type not supported"
| TArray _ -> failwith "[Z3 encoding] TArray type not supported"
| TAny -> failwith "[Z3 encoding] TAny type not supported"
(** [find_or_create_enum] attempts to retrieve the Z3 sort corresponding to the Catala enumeration
[enum]. If no such sort exists yet, it constructs it by creating a Z3 constructor for each
Catala constructor of [enum], and adds it to the context *)
and find_or_create_enum (ctx : context) (enum : EnumName.t) : context * Sort.sort =
(* Creates a Z3 constructor corresponding to the Catala constructor [c] *)
let create_constructor (ctx : context) (c : EnumConstructor.t * typ Pos.marked) :
context * Datatype.Constructor.constructor =
let name, ty = c in
let name = Pos.unmark (EnumConstructor.get_info name) in
let ctx, arg_z3_ty = translate_typ ctx (Pos.unmark ty) in
(* The mk_constructor_s Z3 function is not so well documented. From my understanding, its
argument are: - a string corresponding to the name of the constructor - a recognizer as a
symbol corresponding to the name (unsure why) - a list of symbols corresponding to the
arguments of the constructor - a list of types, that must be of the same length as the list
of arguments - a list of sort_refs, of the same length as the list of arguments. I'm unsure
what this corresponds to *)
( ctx,
Datatype.mk_constructor_s ctx.ctx_z3 name
(Symbol.mk_string ctx.ctx_z3 name)
(* We need a name for the argument of the constructor, we arbitrary pick the name of the
constructor to which we append the special character "!" and the integer 0 *)
[ Symbol.mk_string ctx.ctx_z3 (name ^ "!0") ]
(* The type of the argument, translated to a Z3 sort *)
[ Some arg_z3_ty ]
[ Sort.get_id arg_z3_ty ] )
in
match EnumMap.find_opt enum ctx.ctx_z3datatypes with
| Some e -> (ctx, e)
| None ->
let ctrs = EnumMap.find enum ctx.ctx_decl.ctx_enums in
let ctx, z3_ctrs = List.fold_left_map create_constructor ctx ctrs in
let z3_enum = Datatype.mk_sort_s ctx.ctx_z3 (Pos.unmark (EnumName.get_info enum)) z3_ctrs in
(add_z3enum enum z3_enum ctx, z3_enum)
(** [find_or_create_struct] attemps to retrieve the Z3 sort corresponding to the struct [s]. If no
such sort exists yet, we construct it as a datatype with one constructor taking all the fields
as arguments, and add it to the context *)
and find_or_create_struct (ctx : context) (s : StructName.t) : context * Sort.sort =
match StructMap.find_opt s ctx.ctx_z3structs with
| Some s -> (ctx, s)
| None ->
let s_name = Pos.unmark (StructName.get_info s) in
let fields = StructMap.find s ctx.ctx_decl.ctx_structs in
let z3_fieldnames =
List.map
(fun f -> Pos.unmark (StructFieldName.get_info (fst f)) |> Symbol.mk_string ctx.ctx_z3)
fields
in
let ctx, z3_fieldtypes =
List.fold_left_map (fun ctx f -> Pos.unmark (snd f) |> translate_typ ctx) ctx fields
in
let z3_sortrefs = List.map Sort.get_id z3_fieldtypes in
let mk_struct_s = "mk!" ^ s_name in
let z3_mk_struct =
Datatype.mk_constructor_s ctx.ctx_z3 mk_struct_s
(Symbol.mk_string ctx.ctx_z3 mk_struct_s)
z3_fieldnames
(List.map (fun x -> Some x) z3_fieldtypes)
z3_sortrefs
in
let z3_struct = Datatype.mk_sort_s ctx.ctx_z3 s_name [ z3_mk_struct ] in
(add_z3struct s z3_struct ctx, z3_struct)
(** [translate_lit] returns the Z3 expression as a literal corresponding to [lit] **)
let translate_lit (ctx : context) (l : lit) : Expr.expr =
match l with
| LBool b -> if b then Boolean.mk_true ctx.ctx_z3 else Boolean.mk_false ctx.ctx_z3
| LEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
| LInt n -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.integer_to_int n)
| LRat _ -> failwith "[Z3 encoding] LRat literals not supported"
| LMoney m ->
let z3_m = Runtime.integer_to_int (Runtime.money_to_cents m) in
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 z3_m
| LUnit -> failwith "[Z3 encoding] LUnit literals not supported"
(* Encoding a date as an integer corresponding to the number of days since Jan 1, 1900 *)
| LDate d -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int d)
| LDuration _ -> failwith "[Z3 encoding] LDuration literals not supported"
(** [find_or_create_funcdecl] attempts to retrieve the Z3 function declaration corresponding to the
variable [v]. If no such function declaration exists yet, we construct it and add it to the
context, thus requiring to return a new context *)
let find_or_create_funcdecl (ctx : context) (v : Var.t) : context * FuncDecl.func_decl =
match VarMap.find_opt v ctx.ctx_funcdecl with
| Some fd -> (ctx, fd)
| None -> (
(* Retrieves the Catala type of the function [v] *)
let f_ty = VarMap.find v ctx.ctx_var in
match Pos.unmark f_ty with
| TArrow (t1, t2) ->
let ctx, z3_t1 = translate_typ ctx (Pos.unmark t1) in
let ctx, z3_t2 = translate_typ ctx (Pos.unmark t2) in
let name = unique_name v in
let fd = FuncDecl.mk_func_decl_s ctx.ctx_z3 name [ z3_t1 ] z3_t2 in
let ctx = add_funcdecl v fd ctx in
let ctx = add_z3var name v ctx in
(ctx, fd)
| _ ->
failwith
"[Z3 Encoding] Ill-formed VC, a function application does not have a function type")
(** [translate_op] returns the Z3 expression corresponding to the application of [op] to the
arguments [args] **)
let rec translate_op (ctx : context) (op : operator) (args : expr Pos.marked list) :
context * Expr.expr =
match op with
| Ternop _top ->
let _e1, _e2, _e3 =
match args with
| [ e1; e2; e3 ] -> (e1, e2, e3)
| _ ->
failwith
(Format.asprintf "[Z3 encoding] Ill-formed ternary operator application: %a"
(Print.format_expr ctx.ctx_decl)
(EApp ((EOp op, Pos.no_pos), args), Pos.no_pos))
in
failwith "[Z3 encoding] ternary operator application not supported"
| Binop bop -> (
(* Special case for GetYear comparisons *)
match (bop, args) with
| Lt KInt, [ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ] ->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let e2 = Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int (date_of_year n)) in
(* e2 corresponds to the first day of the year n. GetYear e1 < e2 can thus be directly
translated as < in the Z3 encoding using the number of days *)
(ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2)
| Lte KInt, [ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ] ->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let nb_days = if CalendarLib.Date.is_leap_year n then 365 else 364 in
(* We want that the year corresponding to e1 is smaller or equal to n. We encode this as
the day corresponding to e1 is smaller or equal than the last day of the year [n],
which is Jan 1st + 365 days if [n] is a leap year, Jan 1st + 364 else *)
let e2 =
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int (date_of_year n) + nb_days)
in
(ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2)
| Gt KInt, [ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ] ->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let nb_days = if CalendarLib.Date.is_leap_year n then 365 else 364 in
(* We want that the year corresponding to e1 is greater to n. We encode this as the day
corresponding to e1 is greater than the last day of the year [n], which is Jan 1st +
365 days if [n] is a leap year, Jan 1st + 364 else *)
let e2 =
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int (date_of_year n) + nb_days)
in
(ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2)
| Gte KInt, [ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ] ->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let e2 = Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int (date_of_year n)) in
(* e2 corresponds to the first day of the year n. GetYear e1 >= e2 can thus be directly
translated as >= in the Z3 encoding using the number of days *)
(ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
| _ -> (
let ctx, e1, e2 =
match args with
| [ e1; e2 ] ->
let ctx, e1 = translate_expr ctx e1 in
let ctx, e2 = translate_expr ctx e2 in
(ctx, e1, e2)
| _ ->
failwith
(Format.asprintf "[Z3 encoding] Ill-formed binary operator application: %a"
(Print.format_expr ctx.ctx_decl)
(EApp ((EOp op, Pos.no_pos), args), Pos.no_pos))
in
match bop with
| And -> (ctx, Boolean.mk_and ctx.ctx_z3 [ e1; e2 ])
| Or -> (ctx, Boolean.mk_or ctx.ctx_z3 [ e1; e2 ])
| Xor -> (ctx, Boolean.mk_xor ctx.ctx_z3 e1 e2)
| Add KInt -> (ctx, Arithmetic.mk_add ctx.ctx_z3 [ e1; e2 ])
| Add _ ->
failwith "[Z3 encoding] application of non-integer binary operator Add not supported"
| Sub KInt -> (ctx, Arithmetic.mk_sub ctx.ctx_z3 [ e1; e2 ])
| Sub _ ->
failwith "[Z3 encoding] application of non-integer binary operator Sub not supported"
| Mult KInt -> (ctx, Arithmetic.mk_mul ctx.ctx_z3 [ e1; e2 ])
| Mult _ ->
failwith "[Z3 encoding] application of non-integer binary operator Mult not supported"
| Div KInt -> (ctx, Arithmetic.mk_div ctx.ctx_z3 e1 e2)
| Div _ ->
failwith "[Z3 encoding] application of non-integer binary operator Div not supported"
| Lt KInt | Lt KMoney | Lt KDate -> (ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2)
| Lt _ ->
failwith
"[Z3 encoding] application of non-integer or money binary operator Lt not supported"
| Lte KInt | Lte KMoney | Lte KDate -> (ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2)
| Lte _ ->
failwith
"[Z3 encoding] application of non-integer or money binary operator Lte not \
supported"
| Gt KInt | Gt KMoney | Gt KDate -> (ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2)
| Gt _ ->
failwith
"[Z3 encoding] application of non-integer or money binary operator Gt not supported"
| Gte KInt | Gte KMoney | Gte KDate -> (ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
| Gte _ ->
failwith
"[Z3 encoding] application of non-integer or money binary operator Gte not \
supported"
| Eq -> (ctx, Boolean.mk_eq ctx.ctx_z3 e1 e2)
| Neq -> (ctx, Boolean.mk_not ctx.ctx_z3 (Boolean.mk_eq ctx.ctx_z3 e1 e2))
| Map -> failwith "[Z3 encoding] application of binary operator Map not supported"
| Concat -> failwith "[Z3 encoding] application of binary operator Concat not supported"
| Filter -> failwith "[Z3 encoding] application of binary operator Filter not supported"))
| Unop uop -> (
let ctx, e1 =
match args with
| [ e1 ] -> translate_expr ctx e1
| _ ->
failwith
(Format.asprintf "[Z3 encoding] Ill-formed unary operator application: %a"
(Print.format_expr ctx.ctx_decl)
(EApp ((EOp op, Pos.no_pos), args), Pos.no_pos))
in
match uop with
| Not -> (ctx, Boolean.mk_not ctx.ctx_z3 e1)
| Minus _ -> failwith "[Z3 encoding] application of unary operator Minus not supported"
(* Omitting the log from the VC *)
| Log _ -> (ctx, e1)
| Length -> failwith "[Z3 encoding] application of unary operator Length not supported"
| IntToRat -> failwith "[Z3 encoding] application of unary operator IntToRat not supported"
| GetDay -> failwith "[Z3 encoding] application of unary operator GetDay not supported"
| GetMonth -> failwith "[Z3 encoding] application of unary operator GetMonth not supported"
| GetYear ->
failwith "[Z3 encoding] GetYear operator only supported in comparisons with literal")
(** [translate_expr] translate the expression [vc] to its corresponding Z3 expression **)
and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr =
let translate_match_arm (head : Expr.expr) (ctx : context)
(e : expr Pos.marked * FuncDecl.func_decl list) : context * Expr.expr =
let e, accessors = e in
match Pos.unmark e with
| EAbs (e, _) ->
(* Create a fresh Catala variable to substitue and obtain the body *)
let fresh_v = Var.make ("arm!tmp", Pos.no_pos) in
let fresh_e = EVar (fresh_v, Pos.no_pos) in
(* Invariant: Catala enums always have exactly one argument *)
let accessor = List.hd accessors in
let proj = Expr.mk_app ctx.ctx_z3 accessor [ head ] in
(* The fresh variable should be substituted by a projection into the enum in the body, we
add this to the context *)
let ctx = add_z3matchsubst fresh_v proj ctx in
let body = Bindlib.msubst (Pos.unmark e) [| fresh_e |] in
translate_expr ctx body
(* Invariant: Catala match arms are always lambda*)
| _ -> failwith "[Z3 encoding] : Arms branches inside VCs should be lambdas"
in
match Pos.unmark vc with
| EVar v -> (
match VarMap.find_opt (Pos.unmark v) ctx.ctx_z3matchsubsts with
| None ->
(* We are in the standard case, where this is a true Catala variable *)
let v = Pos.unmark v in
let t = VarMap.find v ctx.ctx_var in
let name = unique_name v in
let ctx = add_z3var name v ctx in
let ctx, ty = translate_typ ctx (Pos.unmark t) in
(ctx, Expr.mk_const_s ctx.ctx_z3 name ty)
| Some e ->
(* This variable is a temporary variable generated during VC translation of a match. It
actually corresponds to applying an accessor to an enum, the corresponding Z3
expression was previously stored in the context *)
(ctx, e))
| ETuple _ -> failwith "[Z3 encoding] ETuple unsupported"
| ETupleAccess (s, idx, oname, _tys) ->
let name =
match oname with
| None -> failwith "[Z3 encoding]: ETupleAccess of unnamed struct unsupported"
| Some n -> n
in
let ctx, z3_struct = find_or_create_struct ctx name in
(* This datatype should have only one constructor, corresponding to mk_struct. The accessors
of this constructor correspond to the field accesses *)
let accessors = List.hd (Datatype.get_accessors z3_struct) in
let accessor = List.nth accessors idx in
let ctx, s = translate_expr ctx s in
(ctx, Expr.mk_app ctx.ctx_z3 accessor [ s ])
| EInj _ -> failwith "[Z3 encoding] EInj unsupported"
| EMatch (arg, arms, enum) ->
let ctx, z3_enum = find_or_create_enum ctx enum in
let ctx, z3_arg = translate_expr ctx arg in
let _ctx, z3_arms =
List.fold_left_map (translate_match_arm z3_arg) ctx
(List.combine arms (Datatype.get_accessors z3_enum))
in
let z3_arms =
List.map2
(fun r arm ->
(* Encodes A? arg ==> body *)
let is_r = Expr.mk_app ctx.ctx_z3 r [ z3_arg ] in
Boolean.mk_implies ctx.ctx_z3 is_r arm)
(Datatype.get_recognizers z3_enum)
z3_arms
in
(ctx, Boolean.mk_and ctx.ctx_z3 z3_arms)
| EArray _ -> failwith "[Z3 encoding] EArray unsupported"
| ELit l -> (ctx, translate_lit ctx l)
| EAbs _ -> failwith "[Z3 encoding] EAbs unsupported"
| EApp (head, args) -> (
match Pos.unmark head with
| EOp op -> translate_op ctx op args
| EVar v ->
let ctx, fd = find_or_create_funcdecl ctx (Pos.unmark v) in
(* Fold_right to preserve the order of the arguments: The head argument is appended at the
head *)
let ctx, z3_args =
List.fold_right
(fun arg (ctx, acc) ->
let ctx, z3_arg = translate_expr ctx arg in
(ctx, z3_arg :: acc))
args (ctx, [])
in
(ctx, Expr.mk_app ctx.ctx_z3 fd z3_args)
| _ ->
failwith
"[Z3 encoding] EApp node: Catala function calls should only include operators or \
function names")
| EAssert _ -> failwith "[Z3 encoding] EAssert unsupported"
| EOp _ -> failwith "[Z3 encoding] EOp unsupported"
| EDefault _ -> failwith "[Z3 encoding] EDefault unsupported"
| EIfThenElse (e_if, e_then, e_else) ->
(* Encode this as (e_if ==> e_then) /\ (not e_if ==> e_else) *)
let ctx, z3_if = translate_expr ctx e_if in
let ctx, z3_then = translate_expr ctx e_then in
let ctx, z3_else = translate_expr ctx e_else in
( ctx,
Boolean.mk_and ctx.ctx_z3
[
Boolean.mk_implies ctx.ctx_z3 z3_if z3_then;
Boolean.mk_implies ctx.ctx_z3 (Boolean.mk_not ctx.ctx_z3 z3_if) z3_else;
] )
| ErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
module Backend = struct
type backend_context = context
type vc_encoding = Z3.Expr.expr
let print_encoding (vc : vc_encoding) : string = Expr.to_string vc
type model = Z3.Model.model
type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
let solve_vc_encoding (ctx : backend_context) (encoding : vc_encoding) : solver_result =
let solver = Z3.Solver.mk_solver ctx.ctx_z3 None in
Z3.Solver.add solver [ Boolean.mk_not ctx.ctx_z3 encoding ];
match Z3.Solver.check solver [] with
| UNSATISFIABLE -> ProvenTrue
| SATISFIABLE -> ProvenFalse (Z3.Solver.get_model solver)
| UNKNOWN -> Unknown
let print_model (ctx : backend_context) (m : model) : string = print_model ctx m
let is_model_empty (m : model) : bool = List.length (Z3.Model.get_decls m) = 0
let translate_expr (ctx : backend_context) (e : Dcalc.Ast.expr Pos.marked) = translate_expr ctx e
let init_backend () = Cli.debug_print (Format.asprintf "Running Z3 version %s" Version.to_string)
let make_context (decl_ctx : decl_ctx) (free_vars_typ : typ Pos.marked VarMap.t) : backend_context
=
let cfg =
(if !Cli.disable_counterexamples then [] else [ ("model", "true") ]) @ [ ("proof", "false") ]
in
let z3_ctx = mk_context cfg in
{
ctx_z3 = z3_ctx;
ctx_decl = decl_ctx;
ctx_var = free_vars_typ;
ctx_funcdecl = VarMap.empty;
ctx_z3vars = StringMap.empty;
ctx_z3datatypes = EnumMap.empty;
ctx_z3matchsubsts = VarMap.empty;
ctx_z3structs = StructMap.empty;
}
end
module Io = Io.MakeBackendIO (Backend)

17
compiler/verification/z3backend.mli Normal file
View File

@ -0,0 +1,17 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 2022 Inria, contributor: Aymeric Fromherz
<aymeric.fromherz@inria.fr>, Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except
in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Interfacing with the Z3 SMT solver *)
module Io : Io.BackendIO

7
default.nix
View File

@ -1,4 +1,5 @@
{ lib
, pkgs
, fetchFromGitHub
, buildDunePackage
, ansiterminal
@ -19,6 +20,7 @@
, camomile
, cppo
, ppx_deriving
, z3
, menhirLib ? null #for nixos-unstable compatibility.
}:
@ -49,6 +51,9 @@ buildDunePackage rec {
js_of_ocaml-ppx
camomile
cppo
z3
pkgs.z3
ppx_deriving
@ -66,4 +71,4 @@ buildDunePackage rec {
license = licenses.asl20;
maintainers = with maintainers; [ ];
};
}
}

BIN
doc/syntax/syntax.pdf
View File

Binary file not shown.

2
dune
View File

@ -1 +1 @@
(dirs compiler french_law)
(dirs compiler french_law build_system)

12
dune-project
View File

@ -62,8 +62,15 @@
(>= 3.8.0))
(camomile
(>= 1.0.2))
(z3
(>= 4.8.11))
(cppo
(>= 1))))
(>= 1))
(obelisk :dev)
(ocamlformat
(and
:dev
(= 0.19.0)))))
(package
(name french_law)
@ -75,6 +82,7 @@
(ocaml
(>= 4.11.0))
(catala
(>= 0.5.0))))
(= :version))
(conf-npm :dev)))
(using menhir 2.1)

57
examples/Makefile
View File

@ -1,56 +1,23 @@
BLACK := $(shell tput -Txterm setaf 0)
RED := $(shell tput -Txterm setaf 1)
GREEN := $(shell tput -Txterm setaf 2)
YELLOW := $(shell tput -Txterm setaf 3)
LIGHTPURPLE := $(shell tput -Txterm setaf 4)
PURPLE := $(shell tput -Txterm setaf 5)
BLUE := $(shell tput -Txterm setaf 6)
WHITE := $(shell tput -Txterm setaf 7)
CATALA_OPTS?=
CLERK_OPTS?=
RESET := $(shell tput -Txterm sgr0)
CLERK=_build/default/build_system/clerk.exe --exe "_build/default/compiler/catala.exe" \
$(CLERK_OPTS) $(if $(CATALA_OPTS),--catala-opts=$(CATALA_OPTS),) test
################################
# Running legislation unit tests
################################
# Usage `make <name_of_example_folder>.<name_of_test_file>.<name_of_test_scope>.run`
# This Makefile rule assumes the following directory structure:
# foo_example
# tests/
# foo_test_file1.catala
# foo_test_file2.catala
# ...
# foo_implem.catala
# ...
%.run: .FORCE
@SCOPE="$(word 3,$(subst ., ,$*))" $(MAKE) --no-print-directory -C \
$(word 1,$(subst ., ,$*)) tests/$(word 2,$(subst ., ,$*)).run \
> /dev/null || { echo "${RED}FAIL${RESET} ${PURPLE}$@${RESET}"; exit 1; }
@echo "${GREEN}PASS${RESET} ${PURPLE}$@${RESET}"
%.catala_en %.catala_fr %.catala_pl: .FORCE
# Here we cd to the root of the Catala repository such that the paths \
# displayed in error messages start with `examples/` uniformly.
@cd ..;$(CLERK) examples/$@
TEST_FILES?=$(wildcard */tests/*.catala*)
TEST_FILES_SCOPES_EN=$(foreach TEST_FILE,$(TEST_FILES),\
$(foreach TEST_SCOPE,\
$(shell grep -Po "declaration scope [^:]*" $(TEST_FILE) | cut -d " " -f 3), \
$(word 1,$(subst /, ,$(TEST_FILE))).$(word 1,$(subst ., ,$(word 3,$(subst /, ,$(TEST_FILE))))).$(TEST_SCOPE).run \
) \
)
TEST_FILES_SCOPES_FR=$(foreach TEST_FILE,$(TEST_FILES),\
$(foreach TEST_SCOPE,\
$(shell grep -Po "déclaration champ d'application [^:]*" $(TEST_FILE) | cut -d " " -f 4), \
$(word 1,$(subst /, ,$(TEST_FILE))).$(word 1,$(subst ., ,$(word 3,$(subst /, ,$(TEST_FILE))))).$(TEST_SCOPE).run \
) \
)
TEST_FILES_SCOPES_PL=$(foreach TEST_FILE,$(TEST_FILES),\
$(foreach TEST_SCOPE,\
$(shell grep -Po "deklaracja zakres [^:]*" $(TEST_FILE) | cut -d " " -f 3), \
$(word 1,$(subst /, ,$(TEST_FILE))).$(word 1,$(subst ., ,$(word 3,$(subst /, ,$(TEST_FILE))))).$(TEST_SCOPE).run \
) \
)
tests: $(TEST_FILES_SCOPES_EN) $(TEST_FILES_SCOPES_FR) $(TEST_FILES_SCOPES_PL)
pass_tests: $(TEST_FILES)
reset_tests: CLERK_OPTS+=--reset
reset_tests: $(TEST_FILES)
.FORCE:

14
examples/README.md
View File

@ -5,6 +5,8 @@ to locate your own Catala programs in this directory, since programs in this
directory will receive first-class support during the alpha and beta stage
of the Catala programming language development.
<strong>[Browse examples online »](https://catala-lang.org/en/examples)</strong>
## List of examples
- `allocations_familiales/`: computation of the French family benefits, based
@ -42,6 +44,8 @@ file `examples/foo/foo.catala_en`) list.
When invoking any of these targets, additional options to the Catala compiler
can be passed using the `CATALA_OPTS` Makefile variable.
> **Remark**: don't forget to run `make pygments` before generating LaTex or PDF files.
## Testing examples
Unit testing is important, and we encourage Catala developers to write lots
@ -52,10 +56,10 @@ In order to enjoy the benefits of this system, you have to create a `tests/`
directory in your examples directory, for instance `examples/foo/tests`. Then,
create a test file `foo_tests.catala_en` inside that directory.
Inside `foo_tests.catala_en`, declare one ore more test scopes. It is assumed
that all these scopes should execute correctly. Include the program scope you
want to test and use assertions to provide the expected values of your test.
See existing tests in examples directory for more information.
Inside `foo_tests.catala_en`, declare one ore more test scopes. Then, you can
provide the expected output for the interpretation of these scopes or the
compilation of the whole program using the standard expected by `clerk test`:
enter `make help_clerk` from the root of the Catala repository to know more.
Once your tests are written, then will automatically be added to the regression
suite executed using
@ -64,7 +68,7 @@ suite executed using
You can isolate a part of the regression suite by invoking:
TEST_FILES=foo/tests/foo_tests.catala_en make -C examples tests
make -C examples foo/tests/foo_tests.catala_en
## Adding an example

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test1.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test10.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test11.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test12.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test13.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test2.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test3.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test4.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test5.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test6.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test7.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test8.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_allocations_familiales.catala_fr.Test9.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/allocations_familiales/tests/output/tests_ouverture_droits.catala_fr.Test1.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/droit_successions/tests/output/tests_droit_succession.catala_fr.Test1.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/droit_successions/tests/output/tests_droit_succession.catala_fr.Test2.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/droit_successions/tests/output/tests_droit_succession.catala_fr.Test3.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

1
examples/droit_successions/tests/output/tests_droit_succession.catala_fr.Test4.Interpret Normal file
View File

@ -0,0 +1 @@
[RESULT] Computation successful!

Some files were not shown because too many files have changed in this diff Show More