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

Merge branch 'master' into c_backend

Browse Source
This commit is contained in:
Denis Merigoux 2022-04-04 18:01:51 +02:00
commit 3f49824150
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
16 changed files with 126 additions and 50 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
.nix/no-web.patch
View File

@ -25,7 +25,7 @@ index cc842a5d..00000000
- backend = "Interpret";
- language = Some (Js.to_string language);
- max_prec_digits = None;
- trace = false;
- trace;
- disable_counterexamples = false;
- optimize = false;
- ex_scope = Some (Js.to_string scope);
@ -39,7 +39,7 @@ index 2c5a1996..f6c38809 100644
@@ -19,16 +19,6 @@
(libraries calendar zarith zarith_stubs_js)
(modules runtime))
-(executable
- (name catala_web_interpreter)
- (modes byte js)

2
compiler/catala_web_interpreter.ml
View File

@ -19,7 +19,7 @@ let _ =
backend = "Interpret";
language = Some (Js.to_string language);
max_prec_digits = None;
trace = false;
trace;
disable_counterexamples = false;
optimize = false;
ex_scope = Some (Js.to_string scope);

12
compiler/surface/name_resolution.ml
View File

@ -377,6 +377,12 @@ let process_struct_decl (ctxt : context) (sdecl : Ast.struct_decl) : context =
let s_uid =
Desugared.Ast.IdentMap.find (fst sdecl.struct_decl_name) ctxt.struct_idmap
in
if List.length sdecl.struct_decl_fields = 0 then
Errors.raise_spanned_error
(Pos.get_position sdecl.struct_decl_name)
"The struct %s does not have any fields; give it some for Catala to be \
able to accept it."
(Pos.unmark sdecl.struct_decl_name);
List.fold_left
(fun ctxt (fdecl, _) ->
let f_uid =
@ -420,6 +426,12 @@ let process_enum_decl (ctxt : context) (edecl : Ast.enum_decl) : context =
let e_uid =
Desugared.Ast.IdentMap.find (fst edecl.enum_decl_name) ctxt.enum_idmap
in
if List.length edecl.enum_decl_cases = 0 then
Errors.raise_spanned_error
(Pos.get_position edecl.enum_decl_name)
"The enum %s does not have any cases; give it some for Catala to be able \
to accept it."
(Pos.unmark edecl.enum_decl_name);
List.fold_left
(fun ctxt (cdecl, cdecl_pos) ->
let c_uid =

11
compiler/surface/parser.messages
View File

@ -2,8 +2,7 @@ source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR COLON ALT CONSTRUCTOR CONTE
##
## Ends in an error in state: 358.
##
## nonempty_list(enum_decl_line) -> enum_decl_line . [ SCOPE END_CODE DECLARATION ]
## nonempty_list(enum_decl_line) -> enum_decl_line . nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
## list(enum_decl_line) -> enum_decl_line . list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## enum_decl_line
@ -51,7 +50,7 @@ source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR COLON YEAR
##
## Ends in an error in state: 350.
##
## code_item -> DECLARATION ENUM constructor COLON . nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION ENUM constructor COLON . list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION ENUM constructor COLON
@ -63,7 +62,7 @@ source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR YEAR
##
## Ends in an error in state: 349.
##
## code_item -> DECLARATION ENUM constructor . COLON nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION ENUM constructor . COLON list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION ENUM constructor
@ -75,7 +74,7 @@ source_file: BEGIN_CODE DECLARATION ENUM YEAR
##
## Ends in an error in state: 348.
##
## code_item -> DECLARATION ENUM . constructor COLON nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION ENUM . constructor COLON list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION ENUM
@ -264,7 +263,7 @@ source_file: BEGIN_CODE DECLARATION YEAR
##
## code_item -> DECLARATION . STRUCT constructor COLON list(struct_scope) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . SCOPE constructor COLON nonempty_list(scope_decl_item) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . ENUM constructor COLON nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . ENUM constructor COLON list(enum_decl_line) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION

2
compiler/surface/parser.mly
View File

@ -617,7 +617,7 @@ code_item:
scope_decl_context = context;
}, Pos.from_lpos $sloc)
}
| DECLARATION ENUM c = constructor COLON cases = nonempty_list(enum_decl_line) {
| DECLARATION ENUM c = constructor COLON cases = list(enum_decl_line) {
(EnumDecl {
enum_decl_name = c;
enum_decl_cases = cases;

56
compiler/verification/z3backend.real.ml
View File

@ -153,9 +153,7 @@ let rec print_z3model_expr (ctx : context) (ty : typ Pos.marked) (e : Expr.expr)
1900. We pretty-print it as the actual date *)
(* TODO: Use differnt dates conventions depending on the language ? *)
| TDate -> nb_days_to_date (int_of_string (Expr.to_string e))
| TDuration ->
failwith
"[Z3 model]: Pretty-printing of duration literals not supported"
| TDuration -> Format.asprintf "%s days" (Expr.to_string e)
in
match Pos.unmark ty with
@ -261,7 +259,7 @@ let translate_typ_lit (ctx : context) (t : typ_lit) : Sort.sort =
(* Dates are encoded as integers, corresponding to the number of days since
Jan 1, 1900 *)
| TDate -> Arithmetic.Integer.mk_sort ctx.ctx_z3
| TDuration -> failwith "[Z3 encoding] TDuration type not supported"
| TDuration -> Arithmetic.Integer.mk_sort ctx.ctx_z3
(** [translate_typ] returns the Z3 sort correponding to the Catala type [t] **)
let rec translate_typ (ctx : context) (t : typ) : context * Sort.sort =
@ -378,7 +376,13 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr =
(* Encoding a date as an integer corresponding to the number of days since Jan
1, 1900 *)
| LDate d -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int d)
| LDuration _ -> failwith "[Z3 encoding] LDuration literals not supported"
| LDuration d ->
let y, m, d = Runtime.duration_to_years_months_days d in
if y <> 0 || m <> 0 then
failwith
"[Z3 encoding]: Duration literals containing years or months not \
supported";
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 d
(** [find_or_create_funcdecl] attempts to retrieve the Z3 function declaration
corresponding to the variable [v]. If no such function declaration exists
@ -524,54 +528,26 @@ let rec translate_op
| And -> (ctx, Boolean.mk_and ctx.ctx_z3 [ e1; e2 ])
| Or -> (ctx, Boolean.mk_or ctx.ctx_z3 [ e1; e2 ])
| Xor -> (ctx, Boolean.mk_xor ctx.ctx_z3 e1 e2)
| Add KInt | Add KRat | Add KMoney ->
| Add KInt | Add KRat | Add KMoney | Add KDate | Add KDuration ->
(ctx, Arithmetic.mk_add ctx.ctx_z3 [ e1; e2 ])
| Add _ ->
failwith
"[Z3 encoding] application of non-integer binary operator Add \
not supported"
| Sub KInt | Sub KRat | Sub KMoney ->
| Sub KInt | Sub KRat | Sub KMoney | Sub KDate | Sub KDuration ->
(ctx, Arithmetic.mk_sub ctx.ctx_z3 [ e1; e2 ])
| Sub _ ->
failwith
"[Z3 encoding] application of non-integer binary operator Sub \
not supported"
| Mult KInt | Mult KRat | Mult KMoney ->
| Mult KInt | Mult KRat | Mult KMoney | Mult KDate | Mult KDuration ->
(ctx, Arithmetic.mk_mul ctx.ctx_z3 [ e1; e2 ])
| Mult _ ->
failwith
"[Z3 encoding] application of non-integer binary operator Mult \
not supported"
| Div KInt | Div KRat | Div KMoney ->
(ctx, Arithmetic.mk_div ctx.ctx_z3 e1 e2)
| Div _ ->
failwith
"[Z3 encoding] application of non-integer binary operator Div \
not supported"
| Lt KInt | Lt KRat | Lt KMoney | Lt KDate ->
| Lt KInt | Lt KRat | Lt KMoney | Lt KDate | Lt KDuration ->
(ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2)
| Lt _ ->
failwith
"[Z3 encoding] application of non-integer or money binary \
operator Lt not supported"
| Lte KInt | Lte KRat | Lte KMoney | Lte KDate ->
| Lte KInt | Lte KRat | Lte KMoney | Lte KDate | Lte KDuration ->
(ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2)
| Lte _ ->
failwith
"[Z3 encoding] application of non-integer or money binary \
operator Lte not supported"
| Gt KInt | Gt KRat | Gt KMoney | Gt KDate ->
| Gt KInt | Gt KRat | Gt KMoney | Gt KDate | Gt KDuration ->
(ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2)
| Gt _ ->
failwith
"[Z3 encoding] application of non-integer or money binary \
operator Gt not supported"
| Gte KInt | Gte KRat | Gte KMoney | Gte KDate ->
| Gte KInt | Gte KRat | Gte KMoney | Gte KDate | Gte KDuration ->
(ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
| Gte _ ->
failwith
"[Z3 encoding] application of non-integer or money binary \
operator Gte not supported"
| Eq -> (ctx, Boolean.mk_eq ctx.ctx_z3 e1 e2)
| Neq ->
(ctx, Boolean.mk_not ctx.ctx_z3 (Boolean.mk_eq ctx.ctx_z3 e1 e2))

8
tests/test_enum/bad/empty.catala_en Normal file
View File

@ -0,0 +1,8 @@
## Test
```catala
declaration enumeration Foo:
declaration scope Bar:
internal foo content Foo
```

7
tests/test_enum/bad/output/empty.catala_en.Typecheck Normal file
View File

@ -0,0 +1,7 @@
[ERROR] The enum Foo does not have any cases; give it some for Catala to be able to accept it.
--> tests/test_enum/bad/empty.catala_en
|
4 | declaration enumeration Foo:
| ^^^
+ Test

11
tests/test_proof/bad/duration-empty.catala_en Normal file
View File

@ -0,0 +1,11 @@
## Test
```catala
declaration scope A:
context x content duration
context y content boolean
scope A:
definition x equals 94 day
definition y under condition (x +^ x) >^ 100 day consequence equals true
```

12
tests/test_proof/bad/duration-overlap.catala_en Normal file
View File

@ -0,0 +1,12 @@
## Test
```catala
declaration scope A:
context x content duration
context y content boolean
scope A:
definition x equals 94 day
definition y under condition (x +^ x) >=^ 100 day consequence equals true
definition y under condition (x +^ x) <=^ 100 day consequence equals false
```

10
tests/test_proof/bad/output/duration-empty.catala_en.Proof Normal file
View File

@ -0,0 +1,10 @@
[RESULT] [A.x] This variable never returns an empty error
[RESULT] [A.x] No two exceptions to ever overlap for this variable
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/duration-empty.catala_en
|
6 | context y content boolean
| ^
+ Test
Counterexample generation is disabled so none was generated.
[RESULT] [A.y] No two exceptions to ever overlap for this variable

10
tests/test_proof/bad/output/duration-overlap.catala_en.Proof Normal file
View File

@ -0,0 +1,10 @@
[RESULT] [A.x] This variable never returns an empty error
[RESULT] [A.x] No two exceptions to ever overlap for this variable
[RESULT] [A.y] This variable never returns an empty error
[ERROR] [A.y] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/duration-overlap.catala_en
|
6 | context y content boolean
| ^
+ Test
Counterexample generation is disabled so none was generated.

12
tests/test_proof/good/duration.catala_en Normal file
View File

@ -0,0 +1,12 @@
## Test
```catala
declaration scope A:
context x content duration
context y content boolean
scope A:
definition x equals 94 day
definition y under condition (x +^ x) >^ 100 day consequence equals true
definition y under condition (x +^ x) <=^ 100 day consequence equals false
```

4
tests/test_proof/good/output/duration.catala_en.Proof Normal file
View File

@ -0,0 +1,4 @@
[RESULT] [A.x] This variable never returns an empty error
[RESULT] [A.x] No two exceptions to ever overlap for this variable
[RESULT] [A.y] This variable never returns an empty error
[RESULT] [A.y] No two exceptions to ever overlap for this variable

8
tests/test_struct/bad/empty_struct.catala_en Normal file
View File

@ -0,0 +1,8 @@
## Test
```catala
declaration structure Foo:
declaration scope Bar:
internal foo content Foo
```

7
tests/test_struct/bad/output/empty_struct.catala_en.Typecheck Normal file
View File

@ -0,0 +1,7 @@
[ERROR] The struct Foo does not have any fields; give it some for Catala to be able to accept it.
--> tests/test_struct/bad/empty_struct.catala_en
|
4 | declaration structure Foo:
| ^^^
+ Test