2022-03-08 17:03:14 +03:00
|
|
|
(* This file is part of the Catala compiler, a specification language for tax
|
|
|
|
and social benefits computation rules. Copyright (C) 2020 Inria,
|
|
|
|
contributors: Denis Merigoux <denis.merigoux@inria.fr>, Emile Rolley
|
|
|
|
<emile.rolley@tuta.io>
|
2020-03-08 02:21:55 +03:00
|
|
|
|
2022-03-08 17:03:14 +03:00
|
|
|
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
|
2020-03-08 02:21:55 +03:00
|
|
|
|
2020-03-09 14:01:56 +03:00
|
|
|
http://www.apache.org/licenses/LICENSE-2.0
|
2020-03-08 02:21:55 +03:00
|
|
|
|
2022-03-08 17:03:14 +03:00
|
|
|
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
|
2020-03-09 14:01:56 +03:00
|
|
|
the License. *)
|
2020-03-08 02:21:55 +03:00
|
|
|
|
2021-05-26 22:18:18 +03:00
|
|
|
type backend_lang = En | Fr | Pl
|
2021-01-09 23:03:32 +03:00
|
|
|
|
|
|
|
(** Source files to be compiled *)
|
2020-03-08 02:21:55 +03:00
|
|
|
let source_files : string list ref = ref []
|
|
|
|
|
2021-05-26 22:18:18 +03:00
|
|
|
let locale_lang : backend_lang ref = ref En
|
2020-12-26 19:37:41 +03:00
|
|
|
let contents : string ref = ref ""
|
|
|
|
|
2020-03-08 02:21:55 +03:00
|
|
|
(** Prints debug information *)
|
|
|
|
let debug_flag = ref false
|
|
|
|
|
2020-08-07 18:37:28 +03:00
|
|
|
(* Styles the terminal output *)
|
|
|
|
let style_flag = ref true
|
|
|
|
|
2020-12-09 18:45:23 +03:00
|
|
|
(* Max number of digits to show for decimal results *)
|
|
|
|
let max_prec_digits = ref 20
|
2020-12-11 12:51:46 +03:00
|
|
|
let trace_flag = ref false
|
2021-04-03 14:44:11 +03:00
|
|
|
let optimize_flag = ref false
|
2022-01-26 18:24:09 +03:00
|
|
|
let disable_counterexamples = ref false
|
2022-02-24 18:46:02 +03:00
|
|
|
let avoid_exceptions_flag = ref false
|
|
|
|
|
2020-03-08 03:52:31 +03:00
|
|
|
open Cmdliner
|
|
|
|
|
2020-04-19 19:39:16 +03:00
|
|
|
let file =
|
|
|
|
Arg.(
|
|
|
|
required
|
|
|
|
& pos 1 (some file) None
|
2022-01-19 13:20:25 +03:00
|
|
|
& info [] ~docv:"FILE" ~doc:"Catala master file to be compiled.")
|
2020-03-08 03:52:31 +03:00
|
|
|
|
2022-03-08 17:03:14 +03:00
|
|
|
let debug =
|
|
|
|
Arg.(value & flag & info [ "debug"; "d" ] ~doc:"Prints debug information.")
|
2020-03-08 03:52:31 +03:00
|
|
|
|
2022-01-19 13:20:25 +03:00
|
|
|
let unstyled =
|
|
|
|
Arg.(
|
|
|
|
value & flag
|
2022-03-08 17:03:14 +03:00
|
|
|
& info [ "unstyled"; "u" ]
|
|
|
|
~doc:"Removes styling (colors, etc.) from terminal output.")
|
2020-08-07 18:37:28 +03:00
|
|
|
|
2022-03-08 17:03:14 +03:00
|
|
|
let optimize =
|
|
|
|
Arg.(
|
|
|
|
value & flag & info [ "optimize"; "O" ] ~doc:"Run compiler optimizations.")
|
2021-04-03 14:44:11 +03:00
|
|
|
|
2020-12-11 12:51:46 +03:00
|
|
|
let trace_opt =
|
2021-05-09 23:55:50 +03:00
|
|
|
Arg.(
|
2022-01-19 13:20:25 +03:00
|
|
|
value & flag
|
|
|
|
& info [ "trace"; "t" ]
|
|
|
|
~doc:
|
2022-03-08 17:03:14 +03:00
|
|
|
"Displays a trace of the interpreter's computation or generates \
|
|
|
|
logging instructions in translate programs.")
|
2020-12-11 12:51:46 +03:00
|
|
|
|
2021-11-24 17:51:49 +03:00
|
|
|
let avoid_exceptions =
|
|
|
|
Arg.(
|
|
|
|
value & flag
|
2022-03-08 17:03:14 +03:00
|
|
|
& info [ "avoid_exceptions" ]
|
|
|
|
~doc:"Compiles the default calculus without exceptions")
|
2021-11-24 17:51:49 +03:00
|
|
|
|
2020-04-29 10:55:49 +03:00
|
|
|
let wrap_weaved_output =
|
|
|
|
Arg.(
|
|
|
|
value & flag
|
2022-03-08 17:03:14 +03:00
|
|
|
& info [ "wrap"; "w" ]
|
|
|
|
~doc:"Wraps literate programming output with a minimal preamble.")
|
2020-04-17 13:29:30 +03:00
|
|
|
|
2020-03-08 03:52:31 +03:00
|
|
|
let backend =
|
|
|
|
Arg.(
|
|
|
|
required
|
2020-04-19 19:39:16 +03:00
|
|
|
& pos 0 (some string) None
|
2022-01-19 13:20:25 +03:00
|
|
|
& info [] ~docv:"COMMAND"
|
2022-03-08 17:03:14 +03:00
|
|
|
~doc:
|
|
|
|
"Backend selection (see the list of commands for available options).")
|
2020-03-08 03:52:31 +03:00
|
|
|
|
2022-01-11 17:39:20 +03:00
|
|
|
type backend_option =
|
2022-02-17 18:45:49 +03:00
|
|
|
| Dcalc
|
2022-01-11 17:39:20 +03:00
|
|
|
| Html
|
|
|
|
| Interpret
|
2022-02-17 18:45:49 +03:00
|
|
|
| Latex
|
|
|
|
| Lcalc
|
|
|
|
| Makefile
|
2022-01-11 17:39:20 +03:00
|
|
|
| OCaml
|
2022-02-17 18:45:49 +03:00
|
|
|
| Proof
|
2022-01-11 17:39:20 +03:00
|
|
|
| Python
|
2022-02-14 19:01:34 +03:00
|
|
|
| Scalc
|
2022-01-11 17:39:20 +03:00
|
|
|
| Scopelang
|
2022-02-17 18:45:49 +03:00
|
|
|
| Typecheck
|
2020-04-20 09:13:57 +03:00
|
|
|
|
2020-04-19 20:16:04 +03:00
|
|
|
let language =
|
|
|
|
Arg.(
|
2020-04-19 20:25:46 +03:00
|
|
|
value
|
|
|
|
& opt (some string) None
|
2022-03-08 17:03:14 +03:00
|
|
|
& info [ "l"; "language" ] ~docv:"LANG"
|
|
|
|
~doc:"Input language among: en, fr, pl.")
|
2020-04-19 20:16:04 +03:00
|
|
|
|
2020-12-09 18:45:23 +03:00
|
|
|
let max_prec_digits_opt =
|
|
|
|
Arg.(
|
|
|
|
value
|
|
|
|
& opt (some int) None
|
2022-03-08 17:03:14 +03:00
|
|
|
& info
|
|
|
|
[ "p"; "max_digits_printed" ]
|
|
|
|
~docv:"DIGITS"
|
|
|
|
~doc:
|
|
|
|
"Maximum number of significant digits printed for decimal results \
|
|
|
|
(default 20).")
|
2020-12-09 18:45:23 +03:00
|
|
|
|
2022-01-26 18:24:09 +03:00
|
|
|
let disable_counterexamples_opt =
|
|
|
|
Arg.(
|
|
|
|
value & flag
|
2022-03-08 17:03:14 +03:00
|
|
|
& info
|
|
|
|
[ "disable_counterexamples" ]
|
2022-01-26 18:24:09 +03:00
|
|
|
~doc:
|
2022-03-08 17:03:14 +03:00
|
|
|
"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.")
|
2022-01-26 18:24:09 +03:00
|
|
|
|
2020-08-06 16:44:51 +03:00
|
|
|
let ex_scope =
|
|
|
|
Arg.(
|
2022-01-19 13:20:25 +03:00
|
|
|
value
|
|
|
|
& opt (some string) None
|
|
|
|
& info [ "s"; "scope" ] ~docv:"SCOPE" ~doc:"Scope to be focused on.")
|
2020-08-06 16:44:51 +03:00
|
|
|
|
2020-03-08 03:52:31 +03:00
|
|
|
let output =
|
|
|
|
Arg.(
|
2020-04-19 19:39:16 +03:00
|
|
|
value
|
2020-03-08 03:52:31 +03:00
|
|
|
& opt (some string) None
|
|
|
|
& info [ "output"; "o" ] ~docv:"OUTPUT"
|
2022-01-19 13:20:25 +03:00
|
|
|
~doc:
|
2022-03-08 17:03:14 +03:00
|
|
|
"$(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.")
|
2020-03-08 03:52:31 +03:00
|
|
|
|
2020-04-17 16:53:23 +03:00
|
|
|
let catala_t f =
|
2020-08-06 16:44:51 +03:00
|
|
|
Term.(
|
2022-03-08 17:03:14 +03:00
|
|
|
const f $ file $ debug $ unstyled $ wrap_weaved_output $ avoid_exceptions
|
|
|
|
$ backend $ language $ max_prec_digits_opt $ trace_opt
|
|
|
|
$ disable_counterexamples_opt $ optimize $ ex_scope $ output)
|
2020-03-08 03:52:31 +03:00
|
|
|
|
2021-11-07 03:38:17 +03:00
|
|
|
let version = "0.5.0"
|
2020-12-26 19:37:41 +03:00
|
|
|
|
2020-03-08 03:52:31 +03:00
|
|
|
let info =
|
|
|
|
let doc =
|
2022-03-08 17:03:14 +03:00
|
|
|
"Compiler for Catala, a specification language for tax and social benefits \
|
|
|
|
computation rules."
|
2020-03-08 03:52:31 +03:00
|
|
|
in
|
|
|
|
let man =
|
|
|
|
[
|
|
|
|
`S Manpage.s_description;
|
|
|
|
`P
|
2022-03-08 17:03:14 +03:00
|
|
|
"Catala is a domain-specific language for deriving \
|
|
|
|
faithful-by-construction algorithms from legislative texts.";
|
2022-01-19 13:20:25 +03:00
|
|
|
`S Manpage.s_commands;
|
|
|
|
`I
|
|
|
|
( "$(b,Intepret)",
|
2022-03-08 17:03:14 +03:00
|
|
|
"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." );
|
2022-01-19 13:20:25 +03:00
|
|
|
`I
|
|
|
|
( "$(b,Proof)",
|
2022-03-08 17:03:14 +03:00
|
|
|
"Generates and proves verification conditions about the well-behaved \
|
|
|
|
execution of the Catala program." );
|
2022-01-19 13:20:25 +03:00
|
|
|
`I ("$(b,OCaml)", "Generates an OCaml translation of the Catala program.");
|
|
|
|
`I ("$(b,Python)", "Generates a Python translation of the Catala program.");
|
2022-03-08 17:03:14 +03:00
|
|
|
`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." );
|
2022-01-19 13:20:25 +03:00
|
|
|
`I
|
|
|
|
( "$(b,Makefile)",
|
2022-03-08 17:03:14 +03:00
|
|
|
"Generates a Makefile-compatible list of the file dependencies of a \
|
|
|
|
Catala program." );
|
2022-01-19 13:20:25 +03:00
|
|
|
`I
|
|
|
|
( "$(b,Scopelang)",
|
2022-03-08 17:03:14 +03:00
|
|
|
"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." );
|
2022-01-19 13:20:25 +03:00
|
|
|
`I
|
|
|
|
( "$(b,Dcalc)",
|
2022-03-08 17:03:14 +03:00
|
|
|
"Prints a debugging verbatim of the default calculus intermediate \
|
|
|
|
representation of the Catala program. Use the $(b,-s) option to \
|
|
|
|
restrict the output to a particular scope." );
|
2022-02-14 19:01:34 +03:00
|
|
|
`I
|
|
|
|
( "$(b,Lcalc)",
|
2022-03-08 17:03:14 +03:00
|
|
|
"Prints a debugging verbatim of the lambda calculus intermediate \
|
|
|
|
representation of the Catala program. Use the $(b,-s) option to \
|
|
|
|
restrict the output to a particular scope." );
|
2022-02-14 19:01:34 +03:00
|
|
|
`I
|
|
|
|
( "$(b,Scalc)",
|
2022-03-08 17:03:14 +03:00
|
|
|
"Prints a debugging verbatim of the statement calculus intermediate \
|
|
|
|
representation of the Catala program. Use the $(b,-s) option to \
|
|
|
|
restrict the output to a particular scope." );
|
2020-03-08 03:52:31 +03:00
|
|
|
`S Manpage.s_authors;
|
2022-01-19 13:20:25 +03:00
|
|
|
`P "The authors are listed by alphabetical order.";
|
2020-12-11 12:51:46 +03:00
|
|
|
`P "Nicolas Chataing <nicolas.chataing@ens.fr>";
|
2022-01-11 18:36:38 +03:00
|
|
|
`P "Alain Delaët-Tixeuil <alain.delaet--tixeuil@inria.fr>";
|
2022-01-19 13:20:25 +03:00
|
|
|
`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>";
|
2020-03-08 03:52:31 +03:00
|
|
|
`S Manpage.s_examples;
|
2022-01-19 13:20:25 +03:00
|
|
|
`Pre "catala Interpret -s Foo file.catala_en";
|
|
|
|
`Pre "catala Ocaml -o target/file.ml file.catala_en";
|
2020-03-08 03:52:31 +03:00
|
|
|
`S Manpage.s_bugs;
|
2022-03-08 17:03:14 +03:00
|
|
|
`P
|
|
|
|
"Please file bug reports at https://github.com/CatalaLang/catala/issues";
|
2020-03-08 02:21:55 +03:00
|
|
|
]
|
|
|
|
in
|
2022-02-21 16:49:58 +03:00
|
|
|
let exits = Term.default_exits @ [ Term.exit_info ~doc:"on error." 1 ] in
|
|
|
|
Term.info "catala" ~version ~doc ~exits ~man
|
2020-03-08 02:21:55 +03:00
|
|
|
|
2020-03-09 14:01:56 +03:00
|
|
|
(**{1 Terminal formatting}*)
|
2020-03-08 02:21:55 +03:00
|
|
|
|
|
|
|
(**{2 Markers}*)
|
|
|
|
|
2021-02-28 13:15:18 +03:00
|
|
|
let time : float ref = ref (Unix.gettimeofday ())
|
|
|
|
|
2022-03-08 17:03:14 +03:00
|
|
|
let with_style
|
|
|
|
(styles : ANSITerminal.style list) (str : ('a, unit, string) format) =
|
2021-10-28 16:24:39 +03:00
|
|
|
if !style_flag then ANSITerminal.sprintf styles str else Printf.sprintf str
|
|
|
|
|
2022-01-10 17:00:36 +03:00
|
|
|
let format_with_style (styles : ANSITerminal.style list) fmt (str : string) =
|
2022-01-10 20:36:14 +03:00
|
|
|
if !style_flag then
|
2022-03-08 17:03:14 +03:00
|
|
|
Format.pp_print_as fmt (String.length str)
|
|
|
|
(ANSITerminal.sprintf styles "%s" str)
|
2022-01-10 17:00:36 +03:00
|
|
|
else Format.pp_print_string fmt str
|
|
|
|
|
2021-02-28 13:15:18 +03:00
|
|
|
let time_marker () =
|
|
|
|
let new_time = Unix.gettimeofday () in
|
|
|
|
let old_time = !time in
|
|
|
|
time := new_time;
|
|
|
|
let delta = (new_time -. old_time) *. 1000. in
|
|
|
|
if delta > 50. then
|
2021-10-28 16:24:39 +03:00
|
|
|
Printf.printf "%s"
|
2022-03-08 17:03:14 +03:00
|
|
|
(with_style
|
|
|
|
[ ANSITerminal.Bold; ANSITerminal.black ]
|
|
|
|
"[TIME] %.0f ms\n" delta)
|
2020-08-07 18:37:28 +03:00
|
|
|
|
2020-03-09 14:01:56 +03:00
|
|
|
(** Prints [\[DEBUG\]] in purple on the terminal standard output *)
|
2021-02-28 13:15:18 +03:00
|
|
|
let debug_marker () =
|
|
|
|
time_marker ();
|
2022-03-08 15:04:27 +03:00
|
|
|
with_style [ ANSITerminal.Bold; ANSITerminal.magenta ] "[DEBUG] "
|
2020-03-08 02:21:55 +03:00
|
|
|
|
2020-03-09 14:01:56 +03:00
|
|
|
(** Prints [\[ERROR\]] in red on the terminal error output *)
|
2022-03-08 17:03:14 +03:00
|
|
|
let error_marker () =
|
|
|
|
with_style [ ANSITerminal.Bold; ANSITerminal.red ] "[ERROR] "
|
2020-03-08 02:21:55 +03:00
|
|
|
|
2020-03-09 14:01:56 +03:00
|
|
|
(** Prints [\[WARNING\]] in yellow on the terminal standard output *)
|
2022-03-08 17:03:14 +03:00
|
|
|
let warning_marker () =
|
|
|
|
with_style [ ANSITerminal.Bold; ANSITerminal.yellow ] "[WARNING] "
|
2020-03-08 02:21:55 +03:00
|
|
|
|
2020-03-09 14:01:56 +03:00
|
|
|
(** Prints [\[RESULT\]] in green on the terminal standard output *)
|
2022-03-08 17:03:14 +03:00
|
|
|
let result_marker () =
|
|
|
|
with_style [ ANSITerminal.Bold; ANSITerminal.green ] "[RESULT] "
|
2020-03-08 02:21:55 +03:00
|
|
|
|
2020-12-11 12:51:46 +03:00
|
|
|
(** Prints [\[LOG\]] in red on the terminal error output *)
|
2022-03-08 17:03:14 +03:00
|
|
|
let log_marker () =
|
|
|
|
with_style [ ANSITerminal.Bold; ANSITerminal.black ] "[LOG] "
|
2020-12-11 12:51:46 +03:00
|
|
|
|
2020-03-08 02:21:55 +03:00
|
|
|
(**{2 Printers}*)
|
|
|
|
|
|
|
|
(** All the printers below print their argument after the correct marker *)
|
|
|
|
|
2022-03-08 17:03:14 +03:00
|
|
|
let concat_with_line_depending_prefix_and_suffix
|
|
|
|
(prefix : int -> string) (suffix : int -> string) (ss : string list) =
|
2020-04-26 19:32:03 +03:00
|
|
|
match ss with
|
|
|
|
| hd :: rest ->
|
|
|
|
let out, _ =
|
|
|
|
List.fold_left
|
|
|
|
(fun (acc, i) s ->
|
2022-03-08 17:03:14 +03:00
|
|
|
( (acc ^ prefix i ^ s
|
|
|
|
^ if i = List.length ss - 1 then "" else suffix i),
|
|
|
|
i + 1 ))
|
2020-04-26 19:32:03 +03:00
|
|
|
((prefix 0 ^ hd ^ if 0 = List.length ss - 1 then "" else suffix 0), 1)
|
|
|
|
rest
|
|
|
|
in
|
|
|
|
out
|
|
|
|
| [] -> prefix 0
|
|
|
|
|
|
|
|
(** The int argument of the prefix corresponds to the line number, starting at 0 *)
|
|
|
|
let add_prefix_to_each_line (s : string) (prefix : int -> string) =
|
|
|
|
concat_with_line_depending_prefix_and_suffix
|
|
|
|
(fun i -> prefix i)
|
|
|
|
(fun _ -> "\n")
|
|
|
|
(String.split_on_char '\n' s)
|
2020-04-26 14:39:01 +03:00
|
|
|
|
2022-03-08 15:04:27 +03:00
|
|
|
let debug_print (format : ('a, out_channel, unit) format) =
|
|
|
|
if !debug_flag then Printf.printf ("%s" ^^ format ^^ "\n%!") (debug_marker ())
|
|
|
|
else Printf.ifprintf stdout format
|
|
|
|
|
|
|
|
let debug_format (format : ('a, Format.formatter, unit) format) =
|
2022-03-08 17:03:14 +03:00
|
|
|
if !debug_flag then
|
|
|
|
Format.printf ("%s@[<hov>" ^^ format ^^ "@]@.") (debug_marker ())
|
2022-03-08 15:04:27 +03:00
|
|
|
else Format.ifprintf Format.std_formatter format
|
|
|
|
|
|
|
|
let error_print (format : ('a, out_channel, unit) format) =
|
|
|
|
Printf.eprintf ("%s" ^^ format ^^ "\n%!") (error_marker ())
|
|
|
|
|
|
|
|
let warning_print (format : ('a, out_channel, unit) format) =
|
|
|
|
Printf.printf ("%s" ^^ format ^^ "\n%!") (warning_marker ())
|
|
|
|
|
|
|
|
let result_print (format : ('a, out_channel, unit) format) =
|
|
|
|
Printf.printf ("%s" ^^ format ^^ "\n%!") (result_marker ())
|
|
|
|
|
|
|
|
let result_format (format : ('a, Format.formatter, unit) format) =
|
|
|
|
Format.printf ("%s" ^^ format ^^ "\n%!") (result_marker ())
|
|
|
|
|
|
|
|
let log_print (format : ('a, out_channel, unit) format) =
|
|
|
|
Printf.printf ("%s" ^^ format ^^ "\n%!") (log_marker ())
|
|
|
|
|
|
|
|
let log_format (format : ('a, Format.formatter, unit) format) =
|
|
|
|
Format.printf ("%s@[<hov>" ^^ format ^^ "@]@.") (log_marker ())
|