CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-20 08:47:14 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into allocations_logement

Browse Source
This commit is contained in:
Denis Merigoux 2022-03-14 10:46:57 +01:00
commit 88bf577db6
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
16 changed files with 183 additions and 92 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.github/workflows/run-builds.yml vendored
View File

@ -27,7 +27,7 @@ jobs:
./french_law/python/setup_env.sh
- name: Install OCaml dependencies
run: |
opam install . --deps-only --with-doc --with-test
make dependencies-ocaml-with-z3
- name: Make build
run: |
OCAMLRUNPARAM=b opam exec -- make build

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

@ -19,4 +19,4 @@ jobs:
clean: false
- name: Make all
run: |
OCAMLRUNPARAM=b opam exec -- make all -B
OCAMLRUNPARAM=b opam exec -- make dependencies all -B

38
.nix/no-web.patch
View File

@ -1,33 +1,45 @@
diff --git a/compiler/catala_web_interpreter.ml b/compiler/catala_web_interpreter.ml
deleted file mode 100644
index 31d5289..0000000
index cc842a5d..00000000
--- a/compiler/catala_web_interpreter.ml
+++ /dev/null
@@ -1,16 +0,0 @@
@@ -1,28 +0,0 @@
-open Driver
-open Js_of_ocaml
-
-let _ =
- Js.export_all
- (object%js
- method interpret (contents : Js.js_string Js.t) (scope : Js.js_string Js.t)
- (language : Js.js_string Js.t) (trace : bool) =
- method interpret
- (contents : Js.js_string Js.t)
- (scope : Js.js_string Js.t)
- (language : Js.js_string Js.t)
- (trace : bool) =
- driver
- (Contents (Js.to_string contents))
- false false false false "Interpret"
- (Some (Js.to_string language))
- None trace false false
- (Some (Js.to_string scope))
- None
- {
- Utils.Cli.debug = false;
- unstyled = false;
- wrap_weaved_output = false;
- avoid_exceptions = false;
- backend = "Interpret";
- language = Some (Js.to_string language);
- max_prec_digits = None;
- trace = false;
- disable_counterexamples = false;
- optimize = false;
- ex_scope = Some (Js.to_string scope);
- output_file = None;
- }
- end)
diff --git a/compiler/dune b/compiler/dune
index d192291..994c528 100644
index 2c5a1996..f6c38809 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -10,16 +10,6 @@
@@ -19,16 +19,6 @@
(libraries calendar zarith zarith_stubs_js)
(modules runtime))
-(executable
- (name catala_web_interpreter)
- (modes byte js)
@ -40,4 +52,4 @@ index d192291..994c528 100644
-
(executable
(name catala)
(modes native)
(modes native js)

5
INSTALL.md
View File

@ -58,6 +58,11 @@ git submodules, with
This should ensure everything is set up for developing on the Catala compiler!
**Warning**: this command does not include the `z3` dependency required to enable
the proof platform feature of Catala. If you wish to enable support for the
proof platform and the `Proof` command of the Catala compiler, you should
instead execute `make dependencies-with-ocaml` prior to building the compiler.
Other features of the Catala repository also require the following executables
to be present

9
Makefile
View File

@ -18,15 +18,20 @@ K := $(foreach exec,$(EXECUTABLES),\
dependencies-ocaml:
opam install . --deps-only --with-doc --with-test --yes
dependencies-ocaml-with-z3:
opam install . z3 --deps-only --with-doc --with-test --yes
dependencies-js:
$(MAKE) -C $(FRENCH_LAW_JS_LIB_DIR) dependencies
init-submodules:
git submodule update --init
#> dependencies : Install the Catala OCaml, JS and Git dependencies
dependencies: dependencies-ocaml dependencies-js init-submodules
dependencies-with-z3: dependencies-ocaml-with-z3 dependencies-js init-submodules
##########################################
# Catala compiler rules
@ -285,7 +290,7 @@ catala.html: $(COMPILER_DIR)/utils/cli.ml
| tac | sed "1,20d" | tac > $@
#> website-assets : Builds all the assets necessary for the Catala website
website-assets: doc literate_examples grammar.html catala.html js_build build_french_law_library_js
website-assets: doc literate_examples grammar.html catala.html build_french_law_library_js
##########################################
# Misceallenous
@ -293,7 +298,7 @@ website-assets: doc literate_examples grammar.html catala.html js_build build_fr
#> all : Run all make commands
all: \
dependencies build doc website-assets\
build doc website-assets\
tests \
generate_french_law_library_ocaml build_french_law_library_ocaml \
tests_ocaml bench_ocaml \

27
build_system/clerk_driver.ml
View File

@ -130,21 +130,6 @@ let info =
(**{1 Testing}*)
let catala_backend_to_string (backend : Cli.backend_option) : string =
match backend with
| Cli.Dcalc -> "Dcalc"
| Cli.Html -> "Html"
| Cli.Interpret -> "Interpret"
| Cli.Latex -> "Latex"
| Cli.Lcalc -> "Lcalc"
| Cli.Makefile -> "Makefile"
| Cli.OCaml -> "OCaml"
| Cli.Proof -> "Proof"
| Cli.Python -> "Python"
| Cli.Scalc -> "Scalc"
| Cli.Scopelang -> "Scopelang"
| Cli.Typecheck -> "Typecheck"
type expected_output_descr = {
base_filename : string;
output_dir : string;
@ -421,7 +406,8 @@ let collect_all_ninja_build
let vars =
[
( "catala_cmd",
Nj.Expr.Lit (catala_backend_to_string expected_output.backend)
Nj.Expr.Lit
(Cli.catala_backend_option_to_string expected_output.backend)
);
("tested_file", Nj.Expr.Lit tested_file);
( "expected_output",
@ -429,12 +415,9 @@ let collect_all_ninja_build
(expected_output.output_dir
^ expected_output.complete_filename) );
]
in
let output_build_kind =
if reset_test_outputs then "reset" else "test"
in
let catala_backend =
catala_backend_to_string expected_output.backend
and output_build_kind = if reset_test_outputs then "reset" else "test"
and catala_backend =
Cli.catala_backend_option_to_string expected_output.backend
in
let get_rule_infos ?(rule_postfix = "") :

5
catala.opam
View File

@ -36,11 +36,14 @@ depends: [
"benchmark" {>= "1.6"}
"js_of_ocaml-ppx" {>= "3.8.0"}
"camomile" {>= "1.0.2"}
"z3" {>= "4.8.11"}
"cppo" {>= "1"}
"alcotest" {with-test & >= "1.5.0"}
"odoc" {with-doc}
]
depopts: ["z3"]
conflicts: [
"z3" {< "4.8.11"}
]
build: [
["dune" "subst"] {dev}
[

21
compiler/driver.ml
View File

@ -62,22 +62,11 @@ let driver source_file (options : Cli.options) : int =
Cli.locale_lang := language;
let backend = options.backend in
let backend =
let backend = String.lowercase_ascii backend in
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.Interpret
else if backend = "ocaml" then Cli.OCaml
else if backend = "dcalc" then Cli.Dcalc
else if backend = "scopelang" then Cli.Scopelang
else if backend = "python" then Cli.Python
else if backend = "proof" then Cli.Proof
else if backend = "typecheck" then Cli.Typecheck
else if backend = "lcalc" then Cli.Lcalc
else if backend = "scalc" then Cli.Scalc
else
Errors.raise_error
"The selected backend (%s) is not supported by Catala" 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
in
let prgm =
Surface.Parser_driver.parse_top_level_file source_file language

6
compiler/lcalc/ast.ml
View File

@ -121,7 +121,8 @@ let make_none (pos : Pos.t) : expr Pos.marked Bindlib.box =
let make_some (e : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position @@ Bindlib.unbox e in
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
let+ e = e in
let+ e = e [@ocamlformat "disable"] in
mark @@ EInj (e, 1, option_enum, [ (D.TLit D.TUnit, pos); (D.TAny, pos) ])
(** [make_matchopt_with_abs_arms arg e_none e_some] build an expression
@ -133,8 +134,7 @@ let make_matchopt_with_abs_arms
(e_some : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position @@ Bindlib.unbox arg in
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
let+ arg = arg and+ e_none = e_none and+ e_some = e_some in
let+ arg = arg and+ e_none = e_none and+ e_some = e_some [@ocamlformat "disable"] in
mark @@ EMatch (arg, [ e_none; e_some ], option_enum)

58
compiler/utils/cli.ml
View File

@ -17,6 +17,50 @@
type backend_lang = En | Fr | Pl
type backend_option =
| Dcalc
| Html
| Interpret
| Latex
| Lcalc
| Makefile
| OCaml
| Proof
| Python
| Scalc
| Scopelang
| Typecheck
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"
let catala_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
(** Source files to be compiled *)
let source_files : string list ref = ref []
@ -85,20 +129,6 @@ let backend =
~doc:
"Backend selection (see the list of commands for available options).")
type backend_option =
| Dcalc
| Html
| Interpret
| Latex
| Lcalc
| Makefile
| OCaml
| Proof
| Python
| Scalc
| Scopelang
| Typecheck
let language =
Arg.(
value

37
compiler/utils/cli.mli
View File

@ -17,6 +17,28 @@
type backend_lang = En | Fr | Pl
type backend_option =
| Dcalc
| Html
| Interpret
| Latex
| Lcalc
| Makefile
| OCaml
| Proof
| Python
| Scalc
| Scopelang
| Typecheck
val catala_backend_option_to_string : backend_option -> string
(** [catala_backend_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} corresponding to the [backend] string. *)
(** {2 Configuration globals} *)
val source_files : string list ref
@ -50,21 +72,6 @@ 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
type backend_option =
| Dcalc
| Html
| Interpret
| Latex
| Lcalc
| Makefile
| OCaml
| Proof
| Python
| Scalc
| Scopelang
| Typecheck
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

12
compiler/verification/dune
View File

@ -1,7 +1,17 @@
(library
(name verification)
(public_name catala.verification)
(libraries bindlib utils dcalc runtime z3 calendar))
(libraries
bindlib
utils
dcalc
runtime
calendar
(select
z3backend.ml
from
(z3 -> z3backend.real.ml)
(-> z3backend.dummy.ml))))
(documentation
(package catala)

42
compiler/verification/z3backend.dummy.ml Normal file
View File

@ -0,0 +1,42 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2022 Inria, contributor:
Aymeric Fromherz <aymeric.fromherz@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
(** Replicating the interface, with no actual implementation for compiling
without the expected backend. All functions print an error message and exit *)
let dummy () =
Utils.Cli.error_print
"This instance of Catala was compiled without Z3 support.";
exit 124
module Io = struct
let init_backend () = dummy ()
type backend_context = unit
let make_context _ _ = dummy ()
type vc_encoding = unit
let translate_expr _ _ = dummy ()
type model = unit
type vc_encoding_result = Success of model * model | Fail of string
let print_positive_result _ = dummy ()
let print_negative_result _ _ _ = dummy ()
let encode_and_check_vc _ _ = dummy ()
end

0
compiler/verification/z3backend.ml → compiler/verification/z3backend.real.ml
View File

3
default.nix
View File

@ -21,6 +21,7 @@
, cppo
, ppx_deriving
, z3
, alcotest
, menhirLib ? null #for nixos-unstable compatibility.
}:
@ -57,6 +58,8 @@ buildDunePackage rec {
ppx_deriving
alcotest
unionfind
bindlib
] ++ (if isNull menhirLib then [ ] else [ menhirLib ]);

8
dune-project
View File

@ -68,8 +68,6 @@
(>= 3.8.0))
(camomile
(>= 1.0.2))
(z3
(>= 4.8.11))
(cppo
(>= 1))
(obelisk :dev)
@ -80,7 +78,11 @@
(ocamlformat
(and
:dev
(= 0.20.1)))))
(= 0.20.1))))
(depopts
z3)
(conflicts
(z3 (< 4.8.11))))
(package
(name french_law)