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

Merge pull request #213 from AltGr/plugin-support

Browse Source 
Add backend plugin support
This commit is contained in:
Louis Gesbert 2022-05-25 18:31:30 +02:00 committed by GitHub
commit 4c43b533b0
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
27 changed files with 658 additions and 308 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
.github/workflows/run-make-all.yml vendored
View File

@ -15,18 +15,14 @@ jobs:
steps:
- name: Checkout code
uses: actions/checkout@v2
with:
clean: false
- name: Re-initialize python dependencies
run: |
rm -rf french_law/python/env
./french_law/python/setup_env.sh
- name: Install dependencies
run: |
opam exec -- make dependencies
opam exec -- make dependencies pygments
- name: Check promoted files
run: |
rm -f bad-promote
opam exec -- make check-promoted > promotion.out 2>&1 || touch bad-promote
- name: Make all
run: |

7
CONTRIBUTING.md
View File

@ -158,6 +158,13 @@ To add support for a new language:
Feel free to open a pull request for discussion even if you couldn't go through
all these steps, the `lexer_xx.cppo.ml` file is the important part.
### Example: writing custom backends as plugins
Catala has support for dynamically-loaded plugins to use as alternative
backends. See `compiler/plugins` for examples, and [the
documentation](https://catala-lang.org/ocaml_docs/catala/plugins.html) for more
detail.
### Automatic formatting
Please ensure to submit commits formatted using the included `ocamlformat`

14
Makefile
View File

@ -61,6 +61,11 @@ doc:
install:
dune build @install
#> plugins : Builds the demonstration plugins
plugins:
dune build compiler/plugins/
@echo "define CATALA_PLUGINS=_build/default/compiler/plugins to test the plugins"
##########################################
# Rules related to promoted files
##########################################
@ -85,15 +90,15 @@ SYNTAX_HIGHLIGHTING_PL=${CURDIR}/syntax_highlighting/pl
pygmentize_fr: $(SYNTAX_HIGHLIGHTING_FR)/set_up_pygments.sh
chmod +x $<
sudo $<
$<
pygmentize_en: $(SYNTAX_HIGHLIGHTING_EN)/set_up_pygments.sh
chmod +x $<
sudo $<
$<
pygmentize_pl: $(SYNTAX_HIGHLIGHTING_PL)/set_up_pygments.sh
chmod +x $<
sudo $<
$<
#> pygments : Extends your pygmentize executable with Catala lexers
pygments: pygmentize_fr pygmentize_en pygmentize_pl
@ -306,6 +311,7 @@ website-assets: doc js_build literate_examples grammar.html catala.html build_fr
all: \
build js_build doc website-assets\
tests \
plugins \
generate_french_law_library_ocaml build_french_law_library_ocaml \
tests_ocaml bench_ocaml \
build_french_law_library_js \
@ -340,4 +346,4 @@ help_catala:
##########################################
.PHONY: inspect clean all literate_examples english allocations_familiales pygments \
install build_dev build doc format dependencies dependencies-ocaml \
catala.html help parser-messages
catala.html help parser-messages plugins

39
build_system/clerk_driver.ml
View File

@ -143,7 +143,7 @@ type expected_output_descr = {
base_filename : string;
output_dir : string;
complete_filename : string;
backend : Cli.backend_option;
backend : string Cli.backend_option;
scope : string option;
}
@ -156,18 +156,18 @@ let filename_to_expected_output_descr (output_dir : string) (filename : string)
let filename = Filename.remove_extension filename in
let backend =
match String.lowercase_ascii first_extension with
| ".dcalc" -> Some Cli.Dcalc
| ".d" -> Some Cli.Makefile
| ".html" -> Some Cli.Html
| ".interpret" -> Some Cli.Interpret
| ".lcalc" -> Some Cli.Lcalc
| ".ml" -> Some Cli.OCaml
| ".proof" -> Some Cli.Proof
| ".py" -> Some Cli.Python
| ".scalc" -> Some Cli.Scalc
| ".scopelang" -> Some Cli.Scopelang
| ".tex" -> Some Cli.Latex
| ".typecheck" -> Some Cli.Typecheck
| ".dcalc" -> Some `Dcalc
| ".d" -> Some `Makefile
| ".html" -> Some `Html
| ".interpret" -> Some `Interpret
| ".lcalc" -> Some `Lcalc
| ".ml" -> Some `OCaml
| ".proof" -> Some `Proof
| ".py" -> Some `Python
| ".scalc" -> Some `Scalc
| ".scopelang" -> Some `Scopelang
| ".tex" -> Some `Latex
| ".typecheck" -> Some `Typecheck
| _ -> None
in
match backend with
@ -419,8 +419,7 @@ let collect_all_ninja_build
[
( "catala_cmd",
Nj.Expr.Lit
(Cli.catala_backend_option_to_string expected_output.backend)
);
(Cli.backend_option_to_string expected_output.backend) );
"tested_file", Nj.Expr.Lit tested_file;
( "expected_output",
Nj.Expr.Lit
@ -429,7 +428,7 @@ let collect_all_ninja_build
]
and output_build_kind = if reset_test_outputs then "reset" else "test"
and catala_backend =
Cli.catala_backend_option_to_string expected_output.backend
Cli.backend_option_to_string expected_output.backend
in
let get_rule_infos ?(rule_postfix = "") :
@ -465,14 +464,14 @@ let collect_all_ninja_build
in
match expected_output.backend with
| Cli.Interpret | Cli.Proof | Cli.Typecheck | Cli.Dcalc
| Cli.Scopelang | Cli.Scalc | Cli.Lcalc ->
| `Interpret | `Proof | `Typecheck | `Dcalc | `Scopelang | `Scalc
| `Lcalc ->
let rule_output, rule_name, rule_vars =
get_rule_infos expected_output.scope
in
let rule_vars =
match expected_output.backend with
| Cli.Proof ->
| `Proof ->
("extra_flags", Nj.Expr.Lit "--disable_counterexamples")
:: rule_vars
(* Counterexamples can be different at each call because of the
@ -483,7 +482,7 @@ let collect_all_ninja_build
in
( ninja_add_new_rule rule_output rule_name rule_vars ninja,
test_names ^ " $\n " ^ rule_output )
| Cli.Python | Cli.OCaml | Cli.Latex | Cli.Html | Cli.Makefile ->
| `Python | `OCaml | `Latex | `Html | `Makefile | `Plugin _ ->
let tmp_file = Filename.temp_file "clerk_" ("_" ^ catala_backend) in
let rule_output, rule_name, rule_vars =
get_rule_infos ~rule_postfix:"_and_output" expected_output.scope

1
compiler/catala_web_interpreter.ml
View File

@ -17,6 +17,7 @@ let _ =
wrap_weaved_output = false;
avoid_exceptions = false;
backend = "Interpret";
plugins_dirs = [];
language = Some (Js.to_string language);
max_prec_digits = None;
closure_conversion = false;

401
compiler/driver.ml
View File

@ -31,6 +31,13 @@ let extensions = [".catala_fr", "fr"; ".catala_en", "en"; ".catala_pl", "pl"]
error. Usage: [driver source_file options]*)
let driver source_file (options : Cli.options) : int =
try
List.iter
(fun d ->
match Sys.is_directory d with
| true -> Plugin.load_dir d
| false -> ()
| exception Sys_error _ -> ())
options.plugins_dirs;
Cli.set_option_globals options;
Cli.debug_print "Reading files...";
let filename = ref "" in
@ -62,18 +69,20 @@ let driver source_file (options : Cli.options) : int =
Cli.locale_lang := language;
let backend = options.backend in
let backend =
match Cli.catala_backend_option_of_string backend with
| Some b -> b
| None ->
Errors.raise_error
"The selected backend (%s) is not supported by Catala" backend
match Cli.backend_option_of_string backend with
| #Cli.backend_option_builtin as backend -> backend
| `Plugin s -> (
try `Plugin (Plugin.find s)
with Not_found ->
Errors.raise_error
"The selected backend (%s) is not supported by Catala" backend)
in
let prgm =
Surface.Parser_driver.parse_top_level_file source_file language
in
let prgm = Surface.Fill_positions.fill_pos_with_legislative_info prgm in
match backend with
| Cli.Makefile ->
(match backend with
| `Makefile ->
let backend_extensions_list = [".tex"] in
let source_file =
match source_file with
@ -88,7 +97,7 @@ let driver source_file (options : Cli.options) : int =
| None -> Filename.remove_extension source_file ^ ".d"
in
Cli.debug_print "Writing list of dependencies to %s..." output_file;
let oc = open_out output_file in
File.with_out_channel output_file @@ fun oc ->
Printf.fprintf oc "%s:\\\n%s\n%s:"
(String.concat "\\\n"
(output_file
@ -96,9 +105,8 @@ let driver source_file (options : Cli.options) : int =
(fun ext -> Filename.remove_extension source_file ^ ext)
backend_extensions_list))
(String.concat "\\\n" prgm.program_source_files)
(String.concat "\\\n" prgm.program_source_files);
0
| Cli.Latex | Cli.Html ->
(String.concat "\\\n" prgm.program_source_files)
| (`Latex | `Html) as backend ->
let source_file =
match source_file with
| FileName f -> f
@ -108,48 +116,37 @@ let driver source_file (options : Cli.options) : int =
a file"
in
Cli.debug_print "Weaving literate program into %s"
(match backend with
| Cli.Latex -> "LaTeX"
| Cli.Html -> "HTML"
| _ -> assert false (* should not happen *));
(match backend with `Latex -> "LaTeX" | `Html -> "HTML");
let output_file =
match options.output_file with
| Some f -> f
| None -> (
Filename.remove_extension source_file
^
match backend with
| Cli.Latex -> ".tex"
| Cli.Html -> ".html"
| _ -> assert false
(* should not happen *))
^ match backend with `Latex -> ".tex" | `Html -> ".html")
in
File.with_formatter_of_file output_file (fun fmt ->
let weave_output =
match backend with
| Cli.Latex -> Literate.Latex.ast_to_latex language
| Cli.Html -> Literate.Html.ast_to_html language
| _ -> assert false
(* should not happen *)
| `Latex -> Literate.Latex.ast_to_latex language
| `Html -> Literate.Html.ast_to_html language
in
Cli.debug_print "Writing to %s" output_file;
if options.wrap_weaved_output then
match backend with
| Cli.Latex ->
| `Latex ->
Literate.Latex.wrap_latex prgm.Surface.Ast.program_source_files
language fmt (fun fmt -> weave_output fmt prgm)
| Cli.Html ->
| `Html ->
Literate.Html.wrap_html prgm.Surface.Ast.program_source_files
language fmt (fun fmt -> weave_output fmt prgm)
| _ -> assert false (* should not happen *)
else weave_output fmt prgm;
0)
| _ -> (
else weave_output fmt prgm)
| ( `Interpret | `Typecheck | `OCaml | `Python | `Scalc | `Lcalc | `Dcalc
| `Scopelang | `Proof | `Plugin _ ) as backend -> (
Cli.debug_print "Name resolution...";
let ctxt = Surface.Name_resolution.form_context prgm in
let scope_uid =
match options.ex_scope, backend with
| None, Cli.Interpret ->
| None, `Interpret ->
Errors.raise_error "No scope was provided for execution."
| None, _ ->
snd
@ -167,125 +164,128 @@ let driver source_file (options : Cli.options) : int =
let prgm = Surface.Desugaring.desugar_program ctxt prgm in
Cli.debug_print "Collecting rules...";
let prgm = Desugared.Desugared_to_scope.translate_program prgm in
if backend = Cli.Scopelang then
File.with_formatter_of_opt_file options.output_file (fun fmt ->
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
(Scopelang.Print.format_scope ~debug:options.debug)
( scope_uid,
Scopelang.Ast.ScopeMap.find scope_uid prgm.program_scopes )
else
Format.fprintf fmt "%a\n"
(Scopelang.Print.format_program ~debug:options.debug)
prgm;
exit 0);
Cli.debug_print "Translating to default calculus...";
let prgm, type_ordering =
Scopelang.Scope_to_dcalc.translate_program prgm
in
let prgm =
if options.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
File.with_formatter_of_opt_file options.output_file (fun fmt ->
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
(Dcalc.Print.format_scope ~debug:options.debug prgm.decl_ctx)
( scope_uid,
Option.get
(Dcalc.Ast.fold_left_scope_defs ~init:None
~f:(fun acc scope_def _ ->
if
Dcalc.Ast.ScopeName.compare scope_def.scope_name
scope_uid
= 0
then Some scope_def.scope_body
else acc)
prgm.scopes) )
else
Format.fprintf fmt "%a\n"
(Dcalc.Print.format_expr prgm.decl_ctx)
prgrm_dcalc_expr;
exit 0);
Cli.debug_print "Typechecking...";
let _typ = Dcalc.Typing.infer_type prgm.decl_ctx prgrm_dcalc_expr in
(* Cli.debug_format "Typechecking results :@\n%a" (Dcalc.Print.format_typ
prgm.decl_ctx) typ; *)
match backend with
| Cli.Typecheck ->
(* That's it! *)
Cli.result_print "Typechecking successful!";
0
| Cli.Proof ->
let vcs =
Verification.Conditions.generate_verification_conditions prgm
(match options.ex_scope with
| None -> None
| Some _ -> Some scope_uid)
in
Verification.Solver.solve_vc 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
let results =
List.map
(fun ((v1, v1_pos), e1) ->
let v1 =
Re.Pcre.substitute ~rex:out_regex ~subst:(fun _ -> "") v1
in
(v1, v1_pos), e1)
results
in
let results =
List.sort
(fun ((v1, _), _) ((v2, _), _) -> String.compare v1 v2)
results
in
Cli.debug_print "End of interpretation";
Cli.result_print "Computation successful!%s"
(if List.length results > 0 then " Results:" else "");
List.iter
(fun ((var, _), result) ->
Cli.result_format "@[<hov 2>%s@ =@ %a@]" var
(Dcalc.Print.format_expr prgm.decl_ctx)
result)
results;
0
| Cli.OCaml | Cli.Python | Cli.Lcalc | Cli.Scalc ->
Cli.debug_print "Compiling program into lambda calculus...";
let prgm =
if options.avoid_exceptions then
Lcalc.Compile_without_exceptions.translate_program prgm
else Lcalc.Compile_with_exceptions.translate_program prgm
| `Scopelang ->
File.with_formatter_of_opt_file options.output_file @@ fun fmt ->
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
(Scopelang.Print.format_scope ~debug:options.debug)
( scope_uid,
Scopelang.Ast.ScopeMap.find scope_uid prgm.program_scopes )
else
Format.fprintf fmt "%a\n"
(Scopelang.Print.format_program ~debug:options.debug)
prgm
| ( `Interpret | `Typecheck | `OCaml | `Python | `Scalc | `Lcalc | `Dcalc
| `Proof | `Plugin _ ) as backend -> (
Cli.debug_print "Translating to default calculus...";
let prgm, type_ordering =
Scopelang.Scope_to_dcalc.translate_program prgm
in
let prgm =
if options.optimize then begin
Cli.debug_print "Optimizing lambda calculus...";
Lcalc.Optimizations.optimize_program prgm
Cli.debug_print "Optimizing default calculus...";
Dcalc.Optimizations.optimize_program prgm
end
else prgm
in
let prgm =
if options.closure_conversion then (
Cli.debug_print "Performing closure conversion...";
let prgm = Lcalc.Closure_conversion.closure_conversion prgm in
let prgm = Bindlib.unbox prgm in
prgm)
else prgm
let prgrm_dcalc_expr =
Bindlib.unbox (Dcalc.Ast.build_whole_program_expr prgm scope_uid)
in
if backend = Cli.Lcalc then
File.with_formatter_of_opt_file options.output_file (fun fmt ->
match backend with
| `Dcalc ->
File.with_formatter_of_opt_file options.output_file @@ fun fmt ->
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
(Dcalc.Print.format_scope ~debug:options.debug prgm.decl_ctx)
( scope_uid,
Option.get
(Dcalc.Ast.fold_left_scope_defs ~init:None
~f:(fun acc scope_def _ ->
if
Dcalc.Ast.ScopeName.compare scope_def.scope_name
scope_uid
= 0
then Some scope_def.scope_body
else acc)
prgm.scopes) )
else
Format.fprintf fmt "%a\n"
(Dcalc.Print.format_expr prgm.decl_ctx)
prgrm_dcalc_expr
| ( `Interpret | `Typecheck | `OCaml | `Python | `Scalc | `Lcalc
| `Proof | `Plugin _ ) as backend -> (
Cli.debug_print "Typechecking...";
let _typ = Dcalc.Typing.infer_type prgm.decl_ctx prgrm_dcalc_expr in
(* Cli.debug_print (Format.asprintf "Typechecking results :@\n%a"
(Dcalc.Print.format_typ prgm.decl_ctx) typ); *)
match backend with
| `Typecheck ->
(* That's it! *)
Cli.result_print "Typechecking successful!"
| `Proof ->
let vcs =
Verification.Conditions.generate_verification_conditions prgm
(match options.ex_scope with
| None -> None
| Some _ -> Some scope_uid)
in
Verification.Solver.solve_vc prgm.decl_ctx vcs
| `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
let results =
List.map
(fun ((v1, v1_pos), e1) ->
let v1 =
Re.Pcre.substitute ~rex:out_regex ~subst:(fun _ -> "") v1
in
(v1, v1_pos), e1)
results
in
let results =
List.sort
(fun ((v1, _), _) ((v2, _), _) -> String.compare v1 v2)
results
in
Cli.debug_print "End of interpretation";
Cli.result_print "Computation successful!%s"
(if List.length results > 0 then " Results:" else "");
List.iter
(fun ((var, _), result) ->
Cli.result_format "@[<hov 2>%s@ =@ %a@]" var
(Dcalc.Print.format_expr ~debug:options.debug prgm.decl_ctx)
result)
results
| (`OCaml | `Python | `Lcalc | `Scalc | `Plugin _) as backend -> (
Cli.debug_print "Compiling program into lambda calculus...";
let prgm =
if options.avoid_exceptions then
Lcalc.Compile_without_exceptions.translate_program prgm
else Lcalc.Compile_with_exceptions.translate_program prgm
in
let prgm =
if options.optimize then begin
Cli.debug_print "Optimizing lambda calculus...";
Lcalc.Optimizations.optimize_program prgm
end
else prgm
in
let prgm =
if options.closure_conversion then (
Cli.debug_print "Performing closure conversion...";
let prgm = Lcalc.Closure_conversion.closure_conversion prgm in
let prgm = Bindlib.unbox prgm in
prgm)
else prgm
in
match backend with
| `Lcalc ->
File.with_formatter_of_opt_file options.output_file @@ fun fmt ->
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
(Lcalc.Print.format_scope ~debug:options.debug prgm.decl_ctx)
@ -309,58 +309,70 @@ let driver source_file (options : Cli.options) : int =
(Lcalc.Print.format_scope prgm.decl_ctx)
(scope_uid, scope_def.scope_body);
i + 1)
prgm.scopes);
exit 0);
let source_file =
match source_file with
| FileName f -> f
| Contents _ ->
Errors.raise_error
"This backend does not work if the input is not a file"
in
let new_output_file (extension : string) : string =
match options.output_file with
| Some f -> f
| None -> Filename.remove_extension source_file ^ extension
in
(match backend with
| Cli.OCaml ->
let output_file = new_output_file ".ml" in
Cli.debug_print "Writing to %s..." output_file;
File.with_formatter_of_file output_file (fun fmt ->
Cli.debug_print "Compiling program into OCaml...";
Lcalc.To_ocaml.format_program fmt prgm type_ordering)
| Cli.Python | Cli.Scalc ->
let prgm = Scalc.Compile_from_lambda.translate_program prgm in
if backend = Cli.Scalc then
File.with_formatter_of_opt_file options.output_file (fun fmt ->
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
(Scalc.Print.format_scope ~debug:options.debug prgm.decl_ctx)
(let body =
List.find
prgm.scopes)
| (`OCaml | `Python | `Scalc | `Plugin _) as backend -> (
let source_file =
match source_file with
| FileName f -> f
| Contents _ ->
Errors.raise_error
"This backend does not work if the input is not a file"
in
let new_output_file (extension : string) : string =
match options.output_file with
| Some f -> f
| None -> Filename.remove_extension source_file ^ extension
in
match backend with
| `OCaml ->
let output_file = new_output_file ".ml" in
File.with_out_channel output_file @@ fun oc ->
let fmt = Format.formatter_of_out_channel oc in
Cli.debug_print "Compiling program into OCaml...";
Cli.debug_print "Writing to %s..." output_file;
Lcalc.To_ocaml.format_program fmt prgm type_ordering
| `Plugin (Plugin.Lcalc p) ->
let output_file = new_output_file p.Plugin.extension in
Cli.debug_print "Compiling program through backend \"%s\"..."
p.Plugin.name;
Cli.debug_print "Writing to %s..." output_file;
p.Plugin.apply output_file prgm type_ordering
| (`Python | `Scalc | `Plugin (Plugin.Scalc _)) as backend -> (
let prgm = Scalc.Compile_from_lambda.translate_program prgm in
match backend with
| `Scalc ->
File.with_formatter_of_opt_file options.output_file
@@ fun fmt ->
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
(Scalc.Print.format_scope ~debug:options.debug
prgm.decl_ctx)
(List.find
(fun body ->
body.Scalc.Ast.scope_body_name = scope_uid)
prgm.scopes
in
body)
else
Format.fprintf fmt "%a\n"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n\n")
(fun fmt scope ->
(Scalc.Print.format_scope prgm.decl_ctx) fmt scope))
prgm.scopes;
exit 0);
let output_file = new_output_file ".py" in
Cli.debug_print "Compiling program into Python...";
Cli.debug_print "Writing to %s..." output_file;
File.with_formatter_of_file output_file (fun fmt ->
Scalc.To_python.format_program fmt prgm type_ordering)
| _ -> assert false (* should not happen *));
0
| _ -> assert false
(* should not happen *))
prgm.scopes)
else
Format.fprintf fmt "%a\n"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n\n")
(fun fmt scope ->
(Scalc.Print.format_scope prgm.decl_ctx) fmt scope))
prgm.scopes
| `Python ->
let output_file = new_output_file ".py" in
Cli.debug_print "Compiling program into Python...";
Cli.debug_print "Writing to %s..." output_file;
File.with_out_channel output_file @@ fun oc ->
let fmt = Format.formatter_of_out_channel oc in
Scalc.To_python.format_program fmt prgm type_ordering
| `Plugin (Plugin.Lcalc _) -> assert false
| `Plugin (Plugin.Scalc p) ->
let output_file = new_output_file p.Plugin.extension in
Cli.debug_print "Compiling program through backend \"%s\"..."
p.Plugin.name;
Cli.debug_print "Writing to %s..." output_file;
p.Plugin.apply output_file prgm type_ordering)))))));
0
with
| Errors.StructuredError (msg, pos) ->
Cli.error_print "%s" (Errors.print_structured_error msg pos);
@ -375,3 +387,6 @@ let main () =
(Cmdliner.Cmd.v Cli.info (Cli.catala_t (fun f -> driver (FileName f))))
in
exit return_code
(* Export module PluginAPI, hide parent module Plugin *)
module Plugin = Plugin.PluginAPI

2
compiler/driver.mli
View File

@ -15,6 +15,8 @@
License for the specific language governing permissions and limitations under
the License. *)
module Plugin = Plugin.PluginAPI
val driver : Utils.Pos.input_file -> Utils.Cli.options -> int
(** Entry function for the executable. Returns a negative number in case of
error. *)

3
compiler/dune
View File

@ -2,6 +2,7 @@
(name driver)
(public_name catala.driver)
(libraries
dynlink
utils
surface
desugared
@ -11,7 +12,7 @@
scalc
runtime
verification)
(modules driver))
(modules plugin driver))
(library
(name runtime)

13
compiler/index.mld
View File

@ -99,9 +99,20 @@ verification condition for proof backends. More information can be found here:
{li {{: verification.html} Verification}}
}
Last, two more modules contain additional features for the compiler:
Two more modules contain additional features for the compiler:
{ul
{li {{: literate.html} Literate programming}}
{li {{: utils.html} Compiler utilities}}
}
Last, it is possible to customize the backend to the compiler using a plugin
mechanism. The API is defined inside the following module:
{!modules: Driver.Plugin}
See the examples in the [plugins/] subdirectory:
{ul
{li {{: plugins.html} Backend plugin examples}}
}

2
compiler/literate/html.ml
View File

@ -28,7 +28,7 @@ module C = Cli
(** {1 Helpers} *)
(** Converts double lines into HTML newlines. *)
let pre_html (s : string) = run_pandoc s Cli.Html
let pre_html (s : string) = run_pandoc s `Html
(** Raise an error if pygments cannot be found *)
let raise_failed_pygments (command : string) (error_code : int) : 'a =

2
compiler/literate/latex.ml
View File

@ -30,7 +30,7 @@ module C = Cli
let pre_latexify (s : string) : string =
(* Then we send to pandoc, to ensure the markdown features used in the
original document are correctly printed! *)
run_pandoc s Cli.Latex
run_pandoc s `Latex
(** Usage: [wrap_latex source_files custom_pygments language fmt wrapped]

7
compiler/literate/literate_common.ml
View File

@ -68,7 +68,7 @@ let raise_failed_pandoc (command : string) (error_code : int) : 'a =
"Weaving failed: pandoc command \"%s\" returned with error code %d" command
error_code
let run_pandoc (s : string) (backend : Utils.Cli.backend_option) : string =
let run_pandoc (s : string) (backend : [ `Html | `Latex ]) : string =
let pandoc = "pandoc" in
let tmp_file_in = Filename.temp_file "catala_pandoc" "in" in
let tmp_file_out = Filename.temp_file "catala_pandoc" "out" in
@ -80,10 +80,7 @@ let run_pandoc (s : string) (backend : Utils.Cli.backend_option) : string =
"-f";
"markdown+multiline_tables";
"-t";
(match backend with
| Cli.Html -> "html"
| Cli.Latex -> "latex"
| _ -> failwith "should not happen");
(match backend with `Html -> "html" | `Latex -> "latex");
"-o";
tmp_file_out;
|]

2
compiler/literate/literate_common.mli
View File

@ -41,7 +41,7 @@ val get_language_extension : Cli.backend_lang -> string
(** Return the file extension corresponding to the given
{!type:Utils.Cli.backend_lang}. *)
val run_pandoc : string -> Cli.backend_option -> string
val run_pandoc : string -> [ `Html | `Latex ] -> string
(** Runs the [pandoc] on a string to pretty-print markdown features into the
desired format. *)

57
compiler/plugin.ml Normal file
View File

@ -0,0 +1,57 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2022 Inria, OCamlPro;
contributors: Louis Gesbert <louis.gesbert@ocamlpro.com>
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. *)
type 'ast gen = {
name : string;
extension : string;
apply : string -> 'ast -> Scopelang.Dependency.TVertex.t list -> unit;
}
type t = Lcalc of Lcalc.Ast.program gen | Scalc of Scalc.Ast.program gen
let name = function Lcalc { name; _ } | Scalc { name; _ } -> name
let backend_plugins : (string, t) Hashtbl.t = Hashtbl.create 17
let register t =
Hashtbl.replace backend_plugins (String.lowercase_ascii (name t)) t
module PluginAPI = struct
let register_lcalc ~name ~extension apply =
register (Lcalc { name; extension; apply })
let register_scalc ~name ~extension apply =
register (Scalc { name; extension; apply })
end
let find name = Hashtbl.find backend_plugins (String.lowercase_ascii name)
let load_file f =
try
Dynlink.loadfile f;
Utils.Cli.debug_print "Plugin %S loaded" f
with e ->
Utils.Errors.format_warning "Could not load plugin %S: %s" f
(Printexc.to_string e)
let load_dir d =
let dynlink_exts =
if Dynlink.is_native then [".cmxs"] else [".cmo"; ".cma"]
in
Array.iter
(fun f ->
if List.exists (Filename.check_suffix f) dynlink_exts then
load_file (Filename.concat d f))
(Sys.readdir d)

54
compiler/plugin.mli Normal file
View File

@ -0,0 +1,54 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2022 Inria, OCamlPro;
contributors: Louis Gesbert <louis.gesbert@ocamlpro.com>
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. *)
(** {2 catala-facing API} *)
type 'ast gen = {
name : string;
extension : string;
apply : string -> 'ast -> Scopelang.Dependency.TVertex.t list -> unit;
}
type t = Lcalc of Lcalc.Ast.program gen | Scalc of Scalc.Ast.program gen
val find : string -> t
(** Find a registered plugin *)
val load_file : string -> unit
(** Load the given plugin (cmo/cma or cmxs file) *)
val load_dir : string -> unit
(** Load all plugins found in the given directory *)
(** {2 plugin-facing API} *)
module PluginAPI : sig
val register_lcalc :
name:string ->
extension:string ->
(string -> Lcalc.Ast.program -> Scopelang.Dependency.TVertex.t list -> unit) ->
unit
val register_scalc :
name:string ->
extension:string ->
(string -> Scalc.Ast.program -> Scopelang.Dependency.TVertex.t list -> unit) ->
unit
end
(**/*)
val register : t -> unit

15
compiler/plugins/dune Normal file
View File

@ -0,0 +1,15 @@
(executable
(name python)
(modes plugin)
(modules python)
(libraries catala.driver))
(executable
(name jsoo)
(modes plugin)
(modules jsoo)
(libraries catala.driver catala.runtime))
(documentation
(package catala)
(mld_files plugins))

76
compiler/plugins/jsoo.ml Normal file
View File

@ -0,0 +1,76 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Louis Gesbert <louis.gesbert@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. *)
(** This file demonstrates the use of backend plugins for Catala. It's a simple
wrapper on top of the OCaml backend that calls js_of_ocaml on the generated
code. Not for production use. *)
let name = "jsoo"
let extension = ".js"
let finalise e f =
let bt = Printexc.get_raw_backtrace () in
f ();
Printexc.raise_with_backtrace e bt
let finally f k =
match k () with
| r ->
f ();
r
| exception e -> finalise e f
let with_open_out file f =
let oc = open_out file in
finally (fun () -> close_out oc) (fun () -> f oc)
let with_temp_file pfx sfx f =
let tmp = Filename.temp_file pfx sfx in
match f tmp with
| r ->
Sys.remove tmp;
r
| exception e ->
let bt = Printexc.get_raw_backtrace () in
Sys.remove tmp;
Printexc.raise_with_backtrace e bt
let apply output_file prgm type_ordering =
with_temp_file "catala_jsoo_" ".ml" @@ fun ml_file ->
with_open_out ml_file (fun oc ->
Lcalc.To_ocaml.format_program
(Format.formatter_of_out_channel oc)
prgm type_ordering;
with_temp_file "catala_jsoo_" ".byte" @@ fun bytecode_file ->
if
Sys.command
(Printf.sprintf
"ocamlfind ocamlc -package catala.runtime -linkpkg %S -o %S"
ml_file bytecode_file)
<> 0
then failwith "ocaml err";
Utils.Cli.debug_print "OCaml compil ok";
if
Sys.command
(Printf.sprintf
"js_of_ocaml +zarith_stubs_js/biginteger.js \
+zarith_stubs_js/runtime.js %S -o %S"
bytecode_file output_file)
<> 0
then failwith "jsoo err";
Utils.Cli.debug_print "Jsoo compil ok, output in %s" output_file)
let () = Driver.Plugin.register_lcalc ~name ~extension apply

51
compiler/plugins/plugins.mld Normal file
View File

@ -0,0 +1,51 @@
{0 Example backend plugins }
This directory contains backend plugins that demonstrate how those can be
written and used with Catala. They probably don't provide much value otherwise.
Use [make plugins] from the root of the source tree to build them.
A plugin is created by writing an OCaml module that calls
[Driver.Plugin.register_lcalc] or [Driver.Plugin.register_scalc] and that links
against [catala.driver]. Here is an example dune stanza to compile it:
{v
(executable
(name my-plugin)
(modes plugin)
(modules my_plugin_main_module)
(libraries catala.driver))
v}
See the following module for the registration interface:
{!modules: Driver.Plugin}
{1 Using plugins}
Plugins are dynamically loaded. The Catala compiler will be looking for them at
startup within [<prefix>/lib/catala/plugins] (assuming that the compiler is
installed into [<prefix>/bin]), or any other directory specified through the
`--plugin-dir` command-line flag or by setting the [CATALA_PLUGINS] environment
variable.
The plugin of your choice can then be called just like the built-in backends, using:
{v
$ catala MyPlugin <file> [options]
v}
{1 Examples}
{2 python example}
This trivial example registers a plugin that uses the [scalc] format as input.
It simply calls the code of the built-in Python backend, and should be no
different to using the normal Catala Python output mode.
{2 jsoo example}
This slightly more involved plugin reads the [lcalc] format, applies the code of
the [OCaml] backend normally, but then calls the [ocamlc] and [js_of_ocaml]
compiler successively on the output in order to give a Javascript output.
Note that this output remains a library, it won't provide user-facing features,
and no efforts are made to make it callable from normal JavaScript code.

32
compiler/plugins/python.ml Normal file
View File

@ -0,0 +1,32 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Louis Gesbert <louis.gesbert@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. *)
(** This file is only for demonstration purposes, showing a trivial use of
backend plugins for Catala.
The code for the Python backend already has first-class support, so there
would be no reason to use this plugin instead *)
let name = "python-plugin"
let extension = ".py"
let apply output_file prgm type_ordering =
let oc = open_out output_file in
let fmt = Format.formatter_of_out_channel oc in
Scalc.To_python.format_program fmt prgm type_ordering;
close_out oc
let () = Driver.Plugin.register_scalc ~name ~extension apply

100
compiler/utils/cli.ml
View File

@ -17,49 +17,52 @@
type backend_lang = En | Fr | Pl
type backend_option =
| Dcalc
| Html
| Interpret
| Latex
| Lcalc
| Makefile
| OCaml
| Proof
| Python
| Scalc
| Scopelang
| Typecheck
type backend_option_builtin =
[ `Latex
| `Makefile
| `Html
| `Interpret
| `Typecheck
| `OCaml
| `Python
| `Scalc
| `Lcalc
| `Dcalc
| `Scopelang
| `Proof ]
let catala_backend_option_to_string = function
| Dcalc -> "Dcalc"
| Html -> "Html"
| Interpret -> "Interpret"
| Latex -> "Latex"
| Lcalc -> "Lcalc"
| Makefile -> "Makefile"
| OCaml -> "OCaml"
| Proof -> "Proof"
| Python -> "Python"
| Scalc -> "Scalc"
| Scopelang -> "Scopelang"
| Typecheck -> "Typecheck"
type 'a backend_option = [ backend_option_builtin | `Plugin of 'a ]
let catala_backend_option_of_string backend =
let backend_option_to_string = function
| `Interpret -> "Interpret"
| `Makefile -> "Makefile"
| `OCaml -> "Ocaml"
| `Scopelang -> "Scopelang"
| `Dcalc -> "Dcalc"
| `Latex -> "Latex"
| `Proof -> "Proof"
| `Html -> "Html"
| `Python -> "Python"
| `Typecheck -> "Typecheck"
| `Scalc -> "Scalc"
| `Lcalc -> "Lcalc"
| `Plugin s -> s
let backend_option_of_string backend =
match String.lowercase_ascii backend with
| "dcalc" -> Some Dcalc
| "html" -> Some Html
| "interpret" -> Some Interpret
| "latex" -> Some Latex
| "lcalc" -> Some Lcalc
| "makefile" -> Some Makefile
| "ocaml" -> Some OCaml
| "proof" -> Some Proof
| "python" -> Some Python
| "scalc" -> Some Scalc
| "scopelang" -> Some Scopelang
| "typecheck" -> Some Typecheck
| _ -> None
| "interpret" -> `Interpret
| "makefile" -> `Makefile
| "ocaml" -> `OCaml
| "scopelang" -> `Scopelang
| "dcalc" -> `Dcalc
| "latex" -> `Latex
| "proof" -> `Proof
| "html" -> `Html
| "python" -> `Python
| "typecheck" -> `Typecheck
| "scalc" -> `Scalc
| "lcalc" -> `Lcalc
| s -> `Plugin s
(** Source files to be compiled *)
let source_files : string list ref = ref []
@ -134,6 +137,15 @@ let backend =
~doc:
"Backend selection (see the list of commands for available options).")
let plugins_dirs =
let doc = "Set the given directory to be searched for backend plugins." in
let env = Cmd.Env.info "CATALA_PLUGINS" ~doc in
let default =
let ( / ) = Filename.concat in
[Sys.executable_name / ".." / "lib" / "catala" / "plugins"]
in
Arg.(value & opt_all dir default & info ["plugin-dir"] ~docv:"DIR" ~env ~doc)
let language =
Arg.(
value
@ -184,6 +196,7 @@ type options = {
wrap_weaved_output : bool;
avoid_exceptions : bool;
backend : string;
plugins_dirs : string list;
language : string option;
max_prec_digits : int option;
trace : bool;
@ -202,6 +215,7 @@ let options =
avoid_exceptions
closure_conversion
backend
plugins_dirs
language
max_prec_digits
trace
@ -215,6 +229,7 @@ let options =
wrap_weaved_output;
avoid_exceptions;
backend;
plugins_dirs;
language;
max_prec_digits;
trace;
@ -227,8 +242,9 @@ let options =
in
Term.(
const make $ debug $ unstyled $ wrap_weaved_output $ avoid_exceptions
$ closure_conversion $ backend $ language $ max_prec_digits_opt $ trace_opt
$ disable_counterexamples_opt $ optimize $ ex_scope $ output)
$ closure_conversion $ backend $ plugins_dirs $ language
$ max_prec_digits_opt $ trace_opt $ disable_counterexamples_opt $ optimize
$ ex_scope $ output)
let catala_t f = Term.(const f $ file $ options)

38
compiler/utils/cli.mli
View File

@ -17,26 +17,28 @@
type backend_lang = En | Fr | Pl
type backend_option =
| Dcalc
| Html
| Interpret
| Latex
| Lcalc
| Makefile
| OCaml
| Proof
| Python
| Scalc
| Scopelang
| Typecheck
type backend_option_builtin =
[ `Latex
| `Makefile
| `Html
| `Interpret
| `Typecheck
| `OCaml
| `Python
| `Scalc
| `Lcalc
| `Dcalc
| `Scopelang
| `Proof ]
val catala_backend_option_to_string : backend_option -> string
(** [catala_backend_to_string backend] returns the string representation of the
type 'a backend_option = [ backend_option_builtin | `Plugin of 'a ]
val backend_option_to_string : string backend_option -> string
(** [backend_option_to_string backend] returns the string representation of the
given [backend].*)
val catala_backend_option_of_string : string -> backend_option option
(** [catala_backend_option_of_string backend] returns the {!type:backend_option}
val backend_option_of_string : string -> string backend_option
(** [backend_option_of_string backend] returns the {!type:backend_option}
corresponding to the [backend] string. *)
(** {2 Configuration globals} *)
@ -72,6 +74,7 @@ val unstyled : bool Cmdliner.Term.t
val trace_opt : bool Cmdliner.Term.t
val wrap_weaved_output : bool Cmdliner.Term.t
val backend : string Cmdliner.Term.t
val plugins_dirs : string list Cmdliner.Term.t
val language : string option Cmdliner.Term.t
val max_prec_digits_opt : int option Cmdliner.Term.t
val ex_scope : string option Cmdliner.Term.t
@ -83,6 +86,7 @@ type options = {
wrap_weaved_output : bool;
avoid_exceptions : bool;
backend : string;
plugins_dirs : string list;
language : string option;
max_prec_digits : int option;
trace : bool;

32
compiler/utils/file.ml
View File

@ -1,6 +1,6 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Emile Rolley <emile.rolley@tuta.io>
Emile Rolley <emile.rolley@tuta.io>, Louis Gesbert <louis.gesbert@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
@ -14,24 +14,30 @@
License for the specific language governing permissions and limitations under
the License. *)
let with_formatter_of_out_channel oc f =
let fmt = Format.formatter_of_out_channel oc in
match f fmt with
(** Run finaliser [f] unconditionally after running [k ()], propagating any
raised exception. *)
let finally f k =
match k () with
| exception e ->
let bt = Printexc.get_raw_backtrace () in
Format.pp_print_flush fmt ();
f ();
Printexc.raise_with_backtrace e bt
| res ->
Format.pp_print_flush fmt ();
res
| r ->
f ();
r
let with_out_channel filename f =
let oc = open_out filename in
finally (fun () -> close_out oc) (fun () -> f oc)
let with_formatter_of_out_channel oc f =
let fmt = Format.formatter_of_out_channel oc in
finally (fun () -> Format.pp_print_flush fmt ()) @@ fun () -> f fmt
let with_formatter_of_file filename f =
let oc = open_out filename in
let res = with_formatter_of_out_channel oc f in
close_out oc;
res
with_out_channel filename (fun oc -> with_formatter_of_out_channel oc f)
let with_formatter_of_opt_file filename_opt f =
match filename_opt with
| None -> f Format.std_formatter
| None -> finally (fun () -> flush stdout) (fun () -> f Format.std_formatter)
| Some filename -> with_formatter_of_file filename f

4
compiler/utils/file.mli
View File

@ -16,6 +16,10 @@
(** Utility functions used for file manipulation. *)
val with_out_channel : string -> (out_channel -> 'a) -> 'a
(** Runs the given function with the provided file opened, ensuring it is
properly closed afterwards. May raise just as [open_out]. *)
(** {2 Formatter wrappers} *)
val with_formatter_of_out_channel :

2
dune
View File

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

2
syntax_highlighting/en/set_up_pygments.sh
View File

@ -1,4 +1,4 @@
#! /usr/bin/env bash
cd "$(dirname "$0")"
cd pygments && python3 setup.py develop
cd pygments && python3 setup.py develop --user

2
syntax_highlighting/fr/set_up_pygments.sh
View File

@ -1,4 +1,4 @@
#! /usr/bin/env bash
cd "$(dirname "$0")"
cd pygments && python3 setup.py develop
cd pygments && python3 setup.py develop --user

2
syntax_highlighting/pl/set_up_pygments.sh
View File

@ -1,4 +1,4 @@
#! /usr/bin/env bash
cd "$(dirname "$0")"
cd pygments && python3 setup.py develop
cd pygments && python3 setup.py develop --user