Merge branch 'master' into proof_platform

This commit is contained in:
Denis Merigoux 2022-01-11 15:39:20 +01:00
commit d705334d9e
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
165 changed files with 683 additions and 284 deletions

8
.gitattributes vendored
View File

@ -1,6 +1,6 @@
*.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
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 binarylinguist-generated
french_law/python/src/allocations_familiales.py binary linguist-generated
compiler/surface/lexer*.cppo.ml text encoding=latin-1

View File

@ -38,6 +38,7 @@ 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
@ -47,6 +48,7 @@ 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:
@ -234,13 +236,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,6 +314,14 @@ 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
##########################################

View File

@ -22,6 +22,7 @@ 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

325
build_system/clerk.ml Normal file
View File

@ -0,0 +1,325 @@
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>";
`P "Nicolas Chataing <nicolas.chataing@ens.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"
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
| _ -> 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.Interpret | Cli.Proof ->
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))

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
@ -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 ] ""

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);

View File

@ -64,7 +64,7 @@ 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
@ -151,7 +151,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
@ -219,7 +219,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
let vcs = Verification.Conditions.generate_verification_conditions prgm in
Verification.Z3encoding.solve_vc prgm prgm.decl_ctx vcs;
0
| Cli.Run ->
| 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

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

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)

View File

@ -158,8 +158,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);
@ -213,8 +214,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) *)
@ -237,8 +239,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);
@ -359,8 +362,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
@ -584,9 +588,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

View File

@ -66,7 +66,16 @@ let backend =
"Backend selection among: Interpret, OCaml, Python, LaTeX, Makefile, Html, Dcalc, \
Scopelang")
type backend_option = Latex | Makefile | Html | Run | OCaml | Python | Dcalc | Scopelang | Proof
type backend_option =
| Latex
| Makefile
| Html
| Interpret
| OCaml
| Python
| Dcalc
| Scopelang
| Proof
let language =
Arg.(
@ -131,6 +140,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

View File

@ -49,7 +49,16 @@ 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 | Proof
type backend_option =
| Latex
| Makefile
| Html
| Interpret
| OCaml
| Python
| Dcalc
| Scopelang
| Proof
val language : string option Cmdliner.Term.t
@ -87,6 +96,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

View File

@ -209,8 +209,7 @@ let generate_verification_conditions (p : program) : verification_condition list
vc_guard = Pos.same_pos_as (Pos.unmark vc_confl) e;
vc_kind = NoOverlappingExceptions;
}
::
{ vc_guard = Pos.same_pos_as (Pos.unmark vc_empty) e; vc_kind = NoEmptyError }
:: { vc_guard = Pos.same_pos_as (Pos.unmark vc_empty) e; vc_kind = NoEmptyError }
:: acc,
ctx )
| _ -> (acc, ctx))

View File

@ -20,7 +20,8 @@ open Z3
type context = { ctx_z3 : Z3.context; ctx_decl : decl_ctx; ctx_var : typ Pos.marked VarMap.t }
(** [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
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
@ -30,7 +31,8 @@ let translate_typ_lit (ctx : context) (t : typ_lit) : Sort.sort = match t with
| TDuration -> failwith "[Z3 encoding] TDuration type not supported"
(** [translate_typ] returns the Z3 sort correponding to the Catala type [t] **)
let translate_typ (ctx : context) (t : typ) : Sort.sort = match t with
let translate_typ (ctx : context) (t : typ) : Sort.sort =
match t with
| TLit t -> translate_typ_lit ctx t
| TTuple _ -> failwith "[Z3 encoding] TTuple type not supported"
| TEnum _ -> failwith "[Z3 encoding] TEnum type not supported"
@ -38,7 +40,6 @@ let translate_typ (ctx : context) (t : typ) : Sort.sort = match t with
| TArray _ -> failwith "[Z3 encoding] TArray type not supported"
| TAny -> failwith "[Z3 encoding] TAny type not supported"
(** [translate_lit] returns the Z3 expression as a literal corresponding to [lit] **)
let translate_lit (ctx : context) (l : lit) : Expr.expr =
match l with
@ -95,7 +96,8 @@ let rec translate_op (ctx : context) (op : operator) (args : expr Pos.marked lis
| Lte _ -> failwith "[Z3 encoding] application of binary operator Lte not supported"
| Gt _ -> failwith "[Z3 encoding] application of binary operator Gt not supported"
| Gte KInt -> Arithmetic.mk_ge ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2)
| Gte _ -> failwith "[Z3 encoding] application of non-integer binary operator Gte not supported"
| Gte _ ->
failwith "[Z3 encoding] application of non-integer binary operator Gte not supported"
| Eq -> failwith "[Z3 encoding] application of binary operator Eq not supported"
| Neq -> failwith "[Z3 encoding] application of binary operator New not supported"
| Map -> failwith "[Z3 encoding] application of binary operator Map not supported"
@ -128,7 +130,6 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : Expr.expr =
let v = Pos.unmark v in
let name = Format.asprintf "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v) in
Expr.mk_const_s ctx.ctx_z3 name (translate_typ ctx (Pos.unmark t))
| ETuple _ -> failwith "[Z3 encoding] ETuple unsupported"
| ETupleAccess _ -> failwith "[Z3 encoding] ETupleAccess unsupported"
| EInj _ -> failwith "[Z3 encoding] EInj unsupported"
@ -159,7 +160,8 @@ type vc_encoding_result = Success of Expr.expr | Fail of string
(** [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 =
let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verification_condition list) :
unit =
Printf.printf "Running Z3 version %s\n" Version.to_string;
let cfg = [ ("model", "true"); ("proof", "false") ] in
@ -172,10 +174,10 @@ let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verificati
(fun vc ->
( vc,
try
Success (translate_expr
{ ctx_z3 = z3_ctx; ctx_decl = decl_ctx; ctx_var = variable_types prgm }
vc.Conditions.vc_guard
)
Success
(translate_expr
{ ctx_z3 = z3_ctx; ctx_decl = decl_ctx; ctx_var = variable_types prgm }
vc.Conditions.vc_guard)
with Failure msg -> Fail msg ))
vcs
in

2
dune
View File

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

View File

@ -1,56 +1,21 @@
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
@$(CLERK) $@
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:

View File

@ -56,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
@ -68,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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@ -1,6 +1,6 @@
> Include: ../podatek_od_czynnosci_cywilnoprawnych/rozdzial_3.catala_pl
## [Test - Art. 7 ustęp 1 punkt 1]
## Test - Art. 7 ustęp 1 punkt 1
```catala
deklaracja zakres Test_A7_U1_P1_PPa:

View File

@ -1,6 +1,6 @@
> Include: ../podatek_od_czynnosci_cywilnoprawnych/rozdzial_3.catala_pl
## [Test - Art. 7 ustęp 1 punkt 2]
## Test - Art. 7 ustęp 1 punkt 2
```catala
deklaracja zakres Test_A7_U1_P2_PPa:

View File

@ -1,6 +1,6 @@
> Include: ../podatek_od_czynnosci_cywilnoprawnych/rozdzial_3.catala_pl
## [Test - Art. 7 ustęp 1 punkt 3]
## Test - Art. 7 ustęp 1 punkt 3
```catala
deklaracja zakres Test_A7_U1_P3:

View File

@ -1,6 +1,6 @@
> Include: ../podatek_od_czynnosci_cywilnoprawnych/rozdzial_3.catala_pl
## [Test - Art. 7 ustęp 1 punkt 4]
## Test - Art. 7 ustęp 1 punkt 4
```catala
deklaracja zakres Test_A7_U1_P4:

View File

@ -1,6 +1,6 @@
> Include: ../podatek_od_czynnosci_cywilnoprawnych/rozdzial_3.catala_pl
## [Test - Art. 7 ustęp 1 punkt 7]
## Test - Art. 7 ustęp 1 punkt 7
```catala
deklaracja zakres Test_A7_U1_P7:

View File

@ -1,6 +1,6 @@
> Include: ../podatek_od_czynnosci_cywilnoprawnych/rozdzial_3.catala_pl
## [Test - Art. 7 ustęp 1 punkt 9]
## Test - Art. 7 ustęp 1 punkt 9
```catala
deklaracja zakres Test_A7_U1_P9:

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@ -2,47 +2,14 @@
# Preamble
############################################
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)
RESET := $(shell tput -Txterm sgr0)
CATALA_OPTS?=
CLERK_OPTS?=
CATALA=../_build/default/compiler/catala.exe Interpret $(CATALA_OPTS)
pass_tests: $(wildcard */*/output/*.out)
reset_tests: $(subst output/,,$(subst .out,.in,$(wildcard */*/output/*.out)))
CLERK=../_build/default/build_system/clerk.exe --exe "../_build/default/compiler/catala.exe" \
$(CLERK_OPTS) $(if $(CATALA_OPTS),--catala-opts=$(CATALA_OPTS),) test
# Forces all the tests to be redone
.FORCE:
%.run: .FORCE
$(CATALA) $(word 1,$(subst ., ,$*)).$(word 2, $(subst ., ,$*)) -s $(word 3,$(subst ., ,$*))
# Usage: make <test_dir>/output/<test_name>.catala_<language>.<scope_name>.out
# This rule runs the test and compares against the expected output. If the
# Catala program is <test_dir>/<test_name>.catala_<language>
# and the scope to run is <scope_name>, then the expected output should be in the file
# <test_dir>/output/<test_name>.catala_<language>.<scope_name>.out
%.out: .FORCE
@$(CATALA) --unstyled \
$(word 1, $(subst /, , $*))/$(word 2, $(subst /, , $*))/$(word 1, $(subst ., ,$(word 4, $(subst /, , $*)))).$(word 2, $(subst ., , $*)) \
-s $(word 3, $(subst ., ,$*)) 2>&1 | \
colordiff -u -b $@ - || { echo "${RED}FAIL${RESET} ${PURPLE}$*${RESET}"; exit 1; }
@echo "${GREEN}PASS${RESET} ${PURPLE}$*${RESET}"
# Usage: make <test_dir>/<test_name>.catala_<language>.<scope_name>.in
# This rule runs the test <test_dir>/<test_name>.catala_<language>, prints its output and
# writes this output to the <test_dir>/output/<test_name>.catala_<language>.<scope_name>.out file
%.in: .FORCE
@-$(CATALA) $(word 1,$(subst ., ,$*)).$(word 2, $(subst ., , $*)) -s $(word 3,$(subst ., ,$*))
@-$(CATALA) --unstyled $(word 1,$(subst ., ,$*)).$(word 2, $(subst ., , $*)) -s $(word 3,$(subst ., ,$*)) \
> $(dir $*)output/$(lastword $(subst /, ,$*)).out 2>&1
%.catala_en %.catala_fr %.catala_pl: .FORCE
@$(CLERK) $@

View File

@ -3,11 +3,8 @@
This folder contains Catala source files designed to test the features of the
language.
It uses `make pass_tests` to launch tests and compare the test terminal output
with an expected output.
Expected outputs are stored using the convention
`<name_of_test>.catala_<language>.<name_of_scope>.out` in the corresponding test output folder.
`<name_of_test>.catala_<language>.<name_of_scope>.Interpret` in the corresponding test output folder.
For both workflows: use `CATALA_OPTS="..." make ...` to pass in Catala compiler
options when debugging.
@ -17,27 +14,36 @@ options when debugging.
1. Create a new test file in `foo/{good,bad}/bar.catala_<language>` (pick the right directory and
an informative name for your test)
2. Write your test, and pick a toplevel scope `A` to run.
3. From this directory, launch `make foo/{good,bad}/bar.catala_<language>.A.run` to get the output of
your test.
4. When you're happy with the output, launch `make foo/{good,bad}/bar.catala_<language>.A.in`. This
3. From this directory, create `mkdir -p foo/{good,bad}/output` and the empty expected
output file `touch foo/{good,bad}/output/bar.catala_<language>.A.Interpret`.
4. From the root of the Catala repository, Run `make -C tests foo/{good,bad}/bar.catala_<language>` to get the output of
your test (compared with the empty file). The failing test will give you the command to use to reproduce
the fail from the `tests` directory.
5. When you're happy with the output, launch `CLERK_OPTS=--reset make -C tests foo/{good,bad}/bar.catala_<language>`
from the root of the Catala repository. This
will record the content of the output of your test into a file.
5. Check that your test pass with `make foo/{good,bad}/output/bar.catala_<language>.A.out`.
6. That's it, you've added a new test for the Catala language!
6. Check that your test pass with `make -C tests foo/{good,bad}/bar.catala_<language>`
from the root of the Catala repository.
7. That's it, you've added a new test for the Catala language!
## Workflow for fixing regressions
1. Run `make`, if a test fails you should see something like
`[FAIL foo/{good,bad}/output/bar.catala_<language>.A]`.
2. Compare the computed and expected output with `make foo/{good,bad}/output/bar.catala_<language>.A.out`.
3. Debug the compiler and/or the test, running `make foo/{good,bad}/bar.catala_<language>.A.run`
periodically to check the output of Catala on the test case.
1. Run `make test_suite` from the root of the Catala repository,
if a test fails you should see something like
`[ERROR] Test failed: foo/{good,bad}/output/bar.catala_<language>.A.Interpret]`.
2. Compare the computed and expected output with `make -C tests foo/{good,bad}/bar.catala_<language>`
from the root of the Catala repository.
3. Debug the compiler and/or the test, running `make -C tests foo/{good,bad}/bar.catala_<language>`
from the root of the Catala repository periodically to check the output of Catala
on the test case.
4. When you're finished debugging, record the new test output with
`make foo/{good,bad}/bar.catala_<language>.A.in`.
5. Re-run `make` to check that everything passes.
`CLERK_OPTS=--reset make foo/{good,bad}/bar.catala_<language>`.
5. Re-run `make test_suite` from the root of the Catala repository
to check that everything passes.
6. That's it, you've fixed the Catala test suite to adapt for changes in the
language.
If a compiler change causes a lot of regressions (error message formatting changes
for instance), you can mass-reset the expected the outputs with `make reset_tests`.
for instance), you can mass-reset the expected the outputs with `CLERK_OPTS=--reset make test_suite`.
**Caution**: use at your own risk, regressions should be fixed one by one in
general.

View File

@ -1,7 +1,7 @@
[ERROR] division by zero at runtime
The division operator:
--> test_arithmetic/bad/division_by_zero.catala_en
--> tests/test_arithmetic/bad/division_by_zero.catala_en
|
20 | definition i equals 1. /. 0.
| ^^
@ -9,7 +9,7 @@ The division operator:
+-+ with decimals
The null denominator:
--> test_arithmetic/bad/division_by_zero.catala_en
--> tests/test_arithmetic/bad/division_by_zero.catala_en
|
20 | definition i equals 1. /. 0.
| ^^

View File

@ -1,7 +1,7 @@
[ERROR] division by zero at runtime
The division operator:
--> test_arithmetic/bad/division_by_zero.catala_en
--> tests/test_arithmetic/bad/division_by_zero.catala_en
|
40 | definition i equals 10 day /^ 0 day
| ^^
@ -9,7 +9,7 @@ The division operator:
+-+ with duration
The null denominator:
--> test_arithmetic/bad/division_by_zero.catala_en
--> tests/test_arithmetic/bad/division_by_zero.catala_en
|
40 | definition i equals 10 day /^ 0 day
| ^^^^^

View File

@ -1,7 +1,7 @@
[ERROR] division by zero at runtime
The division operator:
--> test_arithmetic/bad/division_by_zero.catala_en
--> tests/test_arithmetic/bad/division_by_zero.catala_en
|
10 | definition i equals 1 / 0
| ^
@ -9,7 +9,7 @@ The division operator:
+-+ with integers
The null denominator:
--> test_arithmetic/bad/division_by_zero.catala_en
--> tests/test_arithmetic/bad/division_by_zero.catala_en
|
10 | definition i equals 1 / 0
| ^

View File

@ -1,7 +1,7 @@
[ERROR] division by zero at runtime
The division operator:
--> test_arithmetic/bad/division_by_zero.catala_en
--> tests/test_arithmetic/bad/division_by_zero.catala_en
|
30 | definition i equals $10.0 /$ $0.0
| ^^
@ -9,7 +9,7 @@ The division operator:
+-+ with money
The null denominator:
--> test_arithmetic/bad/division_by_zero.catala_en
--> tests/test_arithmetic/bad/division_by_zero.catala_en
|
30 | definition i equals $10.0 /$ $0.0
| ^^^^

View File

@ -3,21 +3,21 @@
--> integer
Error coming from typechecking the following expression:
--> test_array/bad/fold_error.catala_en
--> tests/test_array/bad/fold_error.catala_en
|
10 | definition list_high_count equals number for m in list of (m >=$ $7)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ Article
Type money coming from expression:
--> test_array/bad/fold_error.catala_en
--> tests/test_array/bad/fold_error.catala_en
|
10 | definition list_high_count equals number for m in list of (m >=$ $7)
| ^^^
+ Article
Type integer coming from expression:
--> test_array/bad/fold_error.catala_en
--> tests/test_array/bad/fold_error.catala_en
|
5 | context list content collection integer
| ^^^^^^^^^^^^^^^^^^

View File

@ -3,21 +3,21 @@
--> integer
Error coming from typechecking the following expression:
--> test_bool/bad/test_xor_with_int.catala_en
--> tests/test_bool/bad/test_xor_with_int.catala_en
|
8 | definition test_var equals 10 xor 20
| ^^^^^^^^^
+ 'xor' should be a boolean operator
Type bool coming from expression:
--> test_bool/bad/test_xor_with_int.catala_en
--> tests/test_bool/bad/test_xor_with_int.catala_en
|
8 | definition test_var equals 10 xor 20
| ^^^
+ 'xor' should be a boolean operator
Type integer coming from expression:
--> test_bool/bad/test_xor_with_int.catala_en
--> tests/test_bool/bad/test_xor_with_int.catala_en
|
8 | definition test_var equals 10 xor 20
| ^^

View File

@ -0,0 +1,21 @@
let
TestBool_6 :
TestBool_in [unit → bool | unit → integer] → TestBool_out [bool |
integer] =
λ (TestBool_in_7: TestBool_in [unit → bool | unit → integer]) →
let foo_8 : unit → bool = TestBool_in_7."foo_in"
in
let bar_9 : unit → integer = TestBool_in_7."bar_in"
in
let bar_10 : integer = error_empty
⟨bar_9 () | true ⊢
⟨⟨true ⊢ ⟨⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩
in
let foo_11 : bool = error_empty
⟨foo_8 () | true ⊢
⟨⟨true ⊢ ⟨⟨bar_10 < 0 false | false ,
⟨true ⊢ ⟨⟨bar_10 >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩
in
TestBool_out {"foo_out": foo_11, "bar_out": bar_10}

View File

@ -0,0 +1,11 @@
let scope TestBool (foo: bool) (bar: integer) =
let bar : integer =
reentrant or by default
⟨⟨true ⊢ ⟨⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ |
true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in;
let foo : bool =
reentrant or by default
⟨⟨true ⊢ ⟨⟨bar < 0 false | false ,
⟨true ⊢ ⟨⟨bar >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
end scope

View File

@ -0,0 +1,2 @@
[RESULT] Computation successful! Results:
[RESULT] foo = true

View File

@ -1,13 +1,13 @@
[ERROR] Cannot divide durations that cannot be converted to a precise number of days
--> test_date/bad/indivisable_durations.catala_en
--> tests/test_date/bad/indivisable_durations.catala_en
|
10 | definition d equals 1 day /^ 2 month
| ^^^^^
+ `Runtime.IndivisableDurations` exception handling
+-+ Day divided by months
--> test_date/bad/indivisable_durations.catala_en
--> tests/test_date/bad/indivisable_durations.catala_en
|
10 | definition d equals 1 day /^ 2 month
| ^^^^^^^

View File

@ -1,13 +1,13 @@
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
--> test_date/bad/uncomparable_duration.catala_en
--> tests/test_date/bad/uncomparable_duration.catala_en
|
40 | definition d equals 1 month >=^ 2 day
| ^^^^^^^
+ `UncomparableDurations` exception management
+-+ `>=^` operator
--> test_date/bad/uncomparable_duration.catala_en
--> tests/test_date/bad/uncomparable_duration.catala_en
|
40 | definition d equals 1 month >=^ 2 day
| ^^^^^

View File

@ -1,13 +1,13 @@
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
--> test_date/bad/uncomparable_duration.catala_en
--> tests/test_date/bad/uncomparable_duration.catala_en
|
30 | definition d equals 1 month >^ 2 day
| ^^^^^^^
+ `UncomparableDurations` exception management
+-+ `<=^` operator
--> test_date/bad/uncomparable_duration.catala_en
--> tests/test_date/bad/uncomparable_duration.catala_en
|
30 | definition d equals 1 month >^ 2 day
| ^^^^^

View File

@ -1,13 +1,13 @@
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
--> test_date/bad/uncomparable_duration.catala_en
--> tests/test_date/bad/uncomparable_duration.catala_en
|
20 | definition d equals 1 month <=^ 2 day
| ^^^^^^^
+ `UncomparableDurations` exception management
+-+ `<=^` operator
--> test_date/bad/uncomparable_duration.catala_en
--> tests/test_date/bad/uncomparable_duration.catala_en
|
20 | definition d equals 1 month <=^ 2 day
| ^^^^^

View File

@ -1,13 +1,13 @@
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
--> test_date/bad/uncomparable_duration.catala_en
--> tests/test_date/bad/uncomparable_duration.catala_en
|
10 | definition d equals 1 month <^ 2 day
| ^^^^^^^
+ `UncomparableDurations` exception management
+-+ `<^` operator
--> test_date/bad/uncomparable_duration.catala_en
--> tests/test_date/bad/uncomparable_duration.catala_en
|
10 | definition d equals 1 month <^ 2 day
| ^^^^^

View File

@ -1,14 +1,14 @@
[ERROR] There is a conflict between multiple validd consequences for assigning the same variable.
This consequence has a valid justification:
--> test_default/bad/conflict.catala_en
--> tests/test_default/bad/conflict.catala_en
|
9 | definition x under condition true consequence equals 0
| ^
+ Article
This consequence has a valid justification:
--> test_default/bad/conflict.catala_en
--> tests/test_default/bad/conflict.catala_en
|
8 | definition x under condition true consequence equals 1
| ^

View File

@ -1,6 +1,6 @@
[ERROR] This variable evaluated to an empty term (no rule that defined it applied in this situation)
--> test_default/bad/empty.catala_en
--> tests/test_default/bad/empty.catala_en
|
6 | context y content boolean
| ^

View File

@ -1,6 +1,6 @@
[ERROR] This variable evaluated to an empty term (no rule that defined it applied in this situation)
--> test_default/bad/empty_with_rules.catala_en
--> tests/test_default/bad/empty_with_rules.catala_en
|
5 | context x content integer
| ^

View File

@ -1,6 +1,6 @@
[ERROR] This constructor name is ambiguous, it can belong to E or F. Desambiguate it by prefixing it with the enum name.
--> test_enum/bad/ambiguous_cases.catala_en
--> tests/test_enum/bad/ambiguous_cases.catala_en
|
14 | definition e equals Case1
| ^^^^^

View File

@ -1,6 +1,6 @@
[ERROR] Couldn't infer the enumeration name from lonely wildcard (wildcard cannot be used as single match case)
--> test_enum/bad/ambiguous_wildcard.catala_en
--> tests/test_enum/bad/ambiguous_wildcard.catala_en
|
15 | -- anything : 31
| ^^^^^^^^^^^^^

View File

@ -1,12 +1,12 @@
[ERROR] The constructor Case3 has been matched twice:
--> test_enum/bad/duplicate_case.catala_en
--> tests/test_enum/bad/duplicate_case.catala_en
|
18 | -- Case3 : true
| ^^^^
+ Article
--> test_enum/bad/duplicate_case.catala_en
--> tests/test_enum/bad/duplicate_case.catala_en
|
17 | -- Case3 : false
| ^^^^^

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