CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-09 22:16:10 +03:00
Code Issues Projects Releases Wiki Activity

Adelaett invariant typing default (#541)

Browse Source
This commit is contained in:
Louis Gesbert 2023-12-07 15:02:20 +01:00 committed by GitHub
commit 10ba1d6e7b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
117 changed files with 3101 additions and 89 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

108
compiler/dcalc/invariants.ml
View File

@ -19,7 +19,7 @@ open Ast
open Catala_utils
type invariant_status = Fail | Pass | Ignore
type invariant_expr = typed expr -> invariant_status
type invariant_expr = decl_ctx -> typed expr -> invariant_status
let check_invariant (inv : string * invariant_expr) (p : typed program) : bool =
(* TODO: add a Program.fold_left_map_exprs to get rid of the mutable
@ -33,7 +33,7 @@ let check_invariant (inv : string * invariant_expr) (p : typed program) : bool =
(* let currente = e in *)
let rec f e =
let r =
match inv e with
match inv p.decl_ctx e with
| Ignore -> true
| Fail ->
Message.raise_spanned_error (Expr.pos e) "%s failed\n\n%a" name
@ -58,7 +58,7 @@ let check_invariant (inv : string * invariant_expr) (p : typed program) : bool =
(* Structural invariant: no default can have as type A -> B *)
let invariant_default_no_arrow () : string * invariant_expr =
( __FUNCTION__,
fun e ->
fun _ctx e ->
match Mark.remove e with
| EDefault _ -> begin
match Mark.remove (Expr.ty e) with TArrow _ -> Fail | _ -> Pass
@ -68,7 +68,7 @@ let invariant_default_no_arrow () : string * invariant_expr =
(* Structural invariant: no partial evaluation *)
let invariant_no_partial_evaluation () : string * invariant_expr =
( __FUNCTION__,
fun e ->
fun _ctx e ->
match Mark.remove e with
| EApp { f = EOp { op = Op.Log _; _ }, _; _ } ->
(* logs are differents. *) Pass
@ -80,7 +80,7 @@ let invariant_no_partial_evaluation () : string * invariant_expr =
(* Structural invariant: no function can return an function *)
let invariant_no_return_a_function () : string * invariant_expr =
( __FUNCTION__,
fun e ->
fun _ctx e ->
match Mark.remove e with
| EAbs _ -> begin
match Mark.remove (Expr.ty e) with
@ -91,7 +91,7 @@ let invariant_no_return_a_function () : string * invariant_expr =
let invariant_app_inversion () : string * invariant_expr =
( __FUNCTION__,
fun e ->
fun _ctx e ->
match Mark.remove e with
| EApp { f = EOp _, _; _ } -> Pass
| EApp { f = EAbs { binder; _ }, _; args } ->
@ -101,13 +101,14 @@ let invariant_app_inversion () : string * invariant_expr =
| EApp { f = EApp { f = EOp { op = Op.Log _; _ }, _; args = _ }, _; _ } ->
Pass
| EApp { f = EStructAccess _, _; _ } -> Pass
| EApp { f = EExternal _, _; _ } -> Pass
| EApp _ -> Fail
| _ -> Ignore )
(** the arity of constructors when matching is always one. *)
let invariant_match_inversion () : string * invariant_expr =
( __FUNCTION__,
fun e ->
fun _ctx e ->
match Mark.remove e with
| EMatch { cases; _ } ->
if
@ -121,6 +122,98 @@ let invariant_match_inversion () : string * invariant_expr =
else Fail
| _ -> Ignore )
(* The purpose of these functions is to determine whether the type `TDefault`
can only appear in certain positions, such as:
* On the left-hand side of an arrow with arity 1, as the type of a scope (for
scope calls).
* At the root of the type tree (outside a default).
* On the right-hand side of the arrow at the root of the type (occurs for
rentrant variables).
For instance, the following types do follow the invariant:
int; bool; int -> bool; <bool>; <int -> bool>; int -> <bool>; S_in {x: int ->
<bool>} -> S {y: bool}
While the following types does not follow the invariant:
<<int>>; <int -> <bool>>; <bool> -> int; S_in {x: int -> <bool>} -> S {y:
<bool>}
This is crucial to maintain the safety of the type system, as demonstrated in
the formal development. *)
let rec check_typ_no_default ctx ty =
match Mark.remove ty with
| TLit _ -> true
| TTuple ts -> List.for_all (check_typ_no_default ctx) ts
| TStruct n ->
let s = StructName.Map.find n ctx.ctx_structs in
StructField.Map.for_all (fun _k ty -> check_typ_no_default ctx ty) s
| TEnum n ->
let s = EnumName.Map.find n ctx.ctx_enums in
EnumConstructor.Map.for_all (fun _k ty -> check_typ_no_default ctx ty) s
| TOption ty -> check_typ_no_default ctx ty
| TArrow (args, res) ->
List.for_all (check_typ_no_default ctx) args && check_typ_no_default ctx res
| TArray ty -> check_typ_no_default ctx ty
| TDefault _t -> false
| TAny ->
Message.raise_internal_error
"Some Dcalc invariants are invalid: TAny was found whereas it should be \
fully resolved."
| TClosureEnv ->
Message.raise_internal_error
"Some Dcalc invariants are invalid: TClosureEnv was found whereas it \
should only appear later in the compilation process."
let check_type_thunked_or_nodefault ctx ty =
check_typ_no_default ctx ty
||
match Mark.remove ty with
| TArrow (args, res) -> (
List.for_all (check_typ_no_default ctx) args
&&
match Mark.remove res with
| TDefault ty -> check_typ_no_default ctx ty
| _ -> check_typ_no_default ctx ty)
| _ -> false
let check_type_root ctx ty =
check_type_thunked_or_nodefault ctx ty
||
match Mark.remove ty with
| TStruct n ->
let s = StructName.Map.find n ctx.ctx_structs in
ScopeName.Map.exists
(fun _k info -> StructName.equal info.in_struct_name n)
ctx.ctx_scopes
&& StructField.Map.for_all
(fun _k ty -> check_type_thunked_or_nodefault ctx ty)
s
| TArrow ([(TStruct n, _)], res) ->
let s = StructName.Map.find n ctx.ctx_structs in
ScopeName.Map.exists
(fun _k info -> StructName.equal info.in_struct_name n)
ctx.ctx_scopes
&& StructField.Map.for_all
(fun _k ty -> check_type_thunked_or_nodefault ctx ty)
s
&& check_typ_no_default ctx res
| TDefault arg -> check_typ_no_default ctx arg
| _ -> false
let invariant_typing_defaults () : string * invariant_expr =
( __FUNCTION__,
fun ctx e ->
if check_type_root ctx (Expr.ty e) then Pass
else (
Message.emit_warning "typing error %a@." (Print.typ ctx) (Expr.ty e);
Fail) )
let check_all_invariants prgm =
List.fold_left ( && ) true
[
@ -129,4 +222,5 @@ let check_all_invariants prgm =
check_invariant (invariant_no_return_a_function ()) prgm;
check_invariant (invariant_app_inversion ()) prgm;
check_invariant (invariant_match_inversion ()) prgm;
check_invariant (invariant_typing_defaults ()) prgm;
]

11
compiler/dcalc/invariants.mli
View File

@ -31,8 +31,13 @@ val check_all_invariants : typed program -> bool
- [invariant_no_partial_evaluation] check there is no partial function.
- [invariant_no_return_a_function] check no function return a function.
- [invariant_app_inversion] : if the term is an function application, then
there is only 5 possibility : it is a let binding, it is an operator
there is only 6 possibility : it is a let binding, it is an operator
application, it is an variable application, it is a struct access function
application (sub-scope call), or it is a operator application with trace.
application (sub-scope call), it is a operator application with trace, or
an external function.
- [invariant_match_inversion] : if a term is a match, then every branch is
an function abstraction. *)
an function abstraction.
- [invariant_typing_default]: the type TDefault can only appear in some
positions.
The function prints as a side effect the different errors.*)

20
compiler/driver.ml
View File

@ -529,7 +529,7 @@ module Commands = struct
$ Cli.Flags.output
$ Cli.Flags.ex_scope_opt)
let typecheck options includes =
let typecheck options check_invariants includes =
let prg = Passes.scopelang options ~includes in
Message.emit_debug "Typechecking...";
let _type_ordering =
@ -541,14 +541,28 @@ module Commands = struct
(* Strictly type-checking could stop here, but we also want this pass to
check full name-resolution and cycle detection. These are checked during
translation to dcalc so we run it here and drop the result. *)
let _prg = Dcalc.From_scopelang.translate_program prg in
let prg = Dcalc.From_scopelang.translate_program prg in
(* Additionally, we might want to check the invariants. *)
if check_invariants then (
let prg =
Shared_ast.Typing.program ~leave_unresolved:false (Program.untype prg)
in
Message.emit_debug "Checking invariants...";
let result = Dcalc.Invariants.check_all_invariants prg in
if not result then
raise (Message.raise_internal_error "Some Dcalc invariants are invalid"));
Message.emit_result "Typechecking successful!"
let typecheck_cmd =
Cmd.v
(Cmd.info "typecheck"
~doc:"Parses and typechecks a Catala program, without interpreting it.")
Term.(const typecheck $ Cli.Flags.Global.options $ Cli.Flags.include_dirs)
Term.(
const typecheck
$ Cli.Flags.Global.options
$ Cli.Flags.check_invariants
$ Cli.Flags.include_dirs)
let dcalc typed options includes output optimize ex_scope_opt check_invariants
=

23
examples/aides_logement/tests/tests_calcul_al_accession_propriete.catala_fr
View File

@ -72,6 +72,29 @@ champ d'application Exemple2:
assertion montant = 85,00 €
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [29344/29344]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [771/771]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4573/4573]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [3046/3046]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4573/4573]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [1396/1396]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s Exemple1
[RESULT] Computation successful! Results:

23
examples/aides_logement/tests/tests_calcul_al_locatif.catala_fr
View File

@ -125,6 +125,29 @@ champ d'application Exemple4 :
assertion montant = 230,63 €
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [29687/29687]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [771/771]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4576/4576]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [3046/3046]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4576/4576]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [1460/1460]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s Exemple1 --disable_warnings
[RESULT] Computation successful! Results:

23
examples/aides_logement/tests/tests_calcul_al_logement_foyer.catala_fr
View File

@ -31,6 +31,29 @@ champ d'application CasTest1:
assertion montant = 76,38 €
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [29117/29117]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [771/771]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4565/4565]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [3046/3046]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4565/4565]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [1356/1356]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s CasTest1 --disable_warnings
[RESULT] Computation successful! Results:

27
examples/aides_logement/tests/tests_invariants.catala_fr Normal file
View File

@ -0,0 +1,27 @@
> Inclusion: ../aides_logement.catala_fr
# Ce fichier est uniquement là pour vérifier que les invariants structurels sont bien garanties par les differences phases de compilation.
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [28966/28966]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [771/771]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4559/4559]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [3046/3046]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4559/4559]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [1332/1332]
[RESULT] Typechecking successful!
```

27
examples/allocations_familiales/tests/test_invariants.catala_fr Normal file
View File

@ -0,0 +1,27 @@
> Inclusion: ../allocations_familiales.catala_fr
# Ce fichier est uniquement là pour vérifier que les invariants structurels sont bien garanties par les differences phases de compilation.
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [3971/3971]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [18/18]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [802/802]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [96/96]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [802/802]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [284/284]
[RESULT] Typechecking successful!
```

25
tests/test_arithmetic/good/priorities.catala_en
View File

@ -12,6 +12,31 @@ scope A:
definition z equals 200 / 2 * 4. - 50. / - (5. - 20 / 2)
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [75/75]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [13/13]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [13/13]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [8/8]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_arithmetic/good/trivial.catala_en
View File

@ -6,6 +6,31 @@ scope A:
definition w equals 1 + 2 + 3
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [16/16]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [2/2]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_array/good/aggregation.catala_en
View File

@ -23,6 +23,31 @@ scope B:
definition z equals number of m among a.x such that m >= $8.95
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [121/121]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [18/18]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [18/18]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [10/10]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_array/good/aggregation_2.catala_en
View File

@ -29,6 +29,31 @@ scope B:
or if collection empty then S { -- id: -1 --income: $20 })
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [115/115]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [16/16]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [16/16]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [7/7]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_array/good/aggregation_3.catala_en
View File

@ -31,6 +31,31 @@ scope S:
= 2
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [225/225]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [46/46]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [14/14]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [46/46]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [2/2]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala scopelang -s S
let scope S (x: integer|internal|output) =

25
tests/test_array/good/concatenation.catala_en
View File

@ -10,6 +10,31 @@ scope A:
definition y equals x ++ ([7; 8; 9] ++ [10])
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [39/39]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_array/good/filter.catala_en
View File

@ -16,6 +16,31 @@ scope B:
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [41/41]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_array/good/filter_map.catala_en
View File

@ -17,6 +17,31 @@ scope B:
definition z equals (m >= $4.95) for m among a.x
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [57/57]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [6/6]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_array/good/fold.catala_en
View File

@ -29,6 +29,31 @@ scope B:
or if collection empty then S { -- id: -1 --income: $20 })
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [115/115]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [16/16]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [16/16]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [7/7]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_array/good/map.catala_en
View File

@ -10,6 +10,31 @@ scope B:
definition z equals (m >= $4.95) for m among x
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [28/28]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s B
[RESULT] Computation successful! Results:

25
tests/test_array/good/simple.catala_en
View File

@ -21,6 +21,31 @@ scope B:
definition z equals for all m among a.x we have m > 0
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [96/96]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [13/13]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [13/13]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [10/10]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_array/good/simpler.catala_en
View File

@ -10,6 +10,31 @@ scope A:
definition w equals for all m among x we have m > 0
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [39/39]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_array/good/simplest.catala_en
View File

@ -8,6 +8,31 @@ scope A:
definition x equals [0; 4; 8]
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [13/13]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [2/2]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_bool/good/test_bool.catala_en
View File

@ -11,6 +11,31 @@ scope TestBool:
definition foo under condition bar < 0 consequence equals false
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [47/47]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [7/7]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Dcalc
let TestBool : TestBool_in → TestBool =

25
tests/test_bool/good/test_precedence.catala_en
View File

@ -8,6 +8,31 @@ scope TestBool:
definition foo equals true and not false and false = false
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [30/30]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [3/3]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s TestBool
[RESULT] Computation successful! Results:

25
tests/test_bool/good/test_xor.catala_en
View File

@ -14,6 +14,31 @@ scope TestXor:
definition f_xor_f equals false xor false
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [85/85]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [8/8]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [8/8]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [12/12]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s TestXor
[RESULT] Computation successful! Results:

25
tests/test_date/good/durations.catala_en
View File

@ -23,6 +23,31 @@ scope A:
definition m2 equals (2 month) * 3
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [85/85]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [14/14]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_date/good/rounding_option_en.catala_en
View File

@ -22,6 +22,31 @@ scope Test:
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [51/51]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s Test
[RESULT] Computation successful! Results:

25
tests/test_date/good/rounding_option_fr.catala_fr
View File

@ -22,6 +22,31 @@ champ d'application Test:
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [51/51]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s Test
[RESULT] Computation successful! Results:

25
tests/test_date/good/simple.catala_en
View File

@ -12,6 +12,31 @@ scope A:
definition z equals x - y
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [58/58]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [9/9]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_dec/good/infinite_precision.catala_en
View File

@ -14,6 +14,31 @@ scope A:
definition a equals x / (y * (x + y) * (x * x * z * z))
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [96/96]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [12/12]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [12/12]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [12/12]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_dec/good/rounding.catala_en
View File

@ -14,6 +14,31 @@ scope A:
definition y1 equals round of y
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [41/41]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [8/8]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_dec/good/simple.catala_en
View File

@ -14,6 +14,31 @@ scope A:
definition k equals 1/3
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [70/70]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [11/11]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_dec/good/zero_after_comma.catala_en
View File

@ -11,6 +11,31 @@ scope A:
assertion y = 1.04
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [48/48]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [6/6]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

36
tests/test_default/good/mutliple_definitions.catala_en
View File

@ -9,6 +9,42 @@ scope A:
definition w equals 3
```
```catala-test-inline
$ catala Typecheck --check_invariants
[WARNING] These definitions have identical justifications and consequences; is it a mistake?
┌─⯈ tests/test_default/good/mutliple_definitions.catala_en:9.3-9.15:
└─┐
9 │ definition w equals 3
│ ‾‾‾‾‾‾‾‾‾‾‾‾
┌─⯈ tests/test_default/good/mutliple_definitions.catala_en:6.3-6.15:
└─┐
6 │ definition w equals 3
│ ‾‾‾‾‾‾‾‾‾‾‾‾
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [14/14]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [3/3]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[WARNING] These definitions have identical justifications and consequences; is it a mistake?

25
tests/test_enum/good/disambiguated_cases.catala_en
View File

@ -21,6 +21,31 @@ scope A:
-- Case2 : 3
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [62/62]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [9/9]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_enum/good/quick_pattern_check.catala_en
View File

@ -16,6 +16,31 @@ scope A:
definition z equals x with pattern Case2
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [66/66]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [9/9]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_enum/good/simple.catala_en
View File

@ -16,6 +16,31 @@ scope A:
-- Case2 : 43
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [43/43]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [6/6]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_enum/good/wildcard.catala_en
View File

@ -36,6 +36,31 @@ scope Simple_case_2:
-- anything : 31
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [90/90]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [6/6]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [12/12]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s Simple_case_2
[RESULT] Computation successful! Results:

25
tests/test_exception/good/context_with_default.catala_en
View File

@ -15,6 +15,31 @@ scope Bar:
assertion foo.x
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [48/48]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [8/8]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s Bar
[RESULT] Computation successful!

38
tests/test_exception/good/double_definition.catala_en
View File

@ -10,6 +10,44 @@ scope Foo:
```
```catala-test-inline
$ catala Typecheck --check_invariants
[WARNING] These definitions have identical justifications and consequences; is it a mistake?
┌─⯈ tests/test_exception/good/double_definition.catala_en:9.3-9.15:
└─┐
9 │ definition x equals 1
│ ‾‾‾‾‾‾‾‾‾‾‾‾
└─ Foo
┌─⯈ tests/test_exception/good/double_definition.catala_en:8.3-8.15:
└─┐
8 │ definition x equals 1
│ ‾‾‾‾‾‾‾‾‾‾‾‾
└─ Foo
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [14/14]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [3/3]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Scopelang -s Foo
[WARNING] These definitions have identical justifications and consequences; is it a mistake?

25
tests/test_exception/good/duplicate_labels.catala_en
View File

@ -18,6 +18,31 @@ scope A:
definition y equals 0
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [59/59]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [10/10]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_exception/good/exception.catala_en
View File

@ -12,6 +12,31 @@ scope A:
definition x equals 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [28/28]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [6/6]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_exception/good/exceptions_squared.catala_en
View File

@ -16,6 +16,31 @@ scope A:
definition x equals 2
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [37/37]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [9/9]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_exception/good/grouped_exceptions.catala_en
View File

@ -46,6 +46,31 @@ scope Benefit:
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [61/61]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [10/10]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s Benefit
[RESULT] Computation successful! Results:

25
tests/test_exception/good/groups_of_exceptions.catala_en
View File

@ -40,6 +40,31 @@ scope Test:
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [84/84]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [15/15]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala interpret -s Test
[RESULT] Computation successful! Results:

25
tests/test_exception/good/same_label_two_variables.catala_en
View File

@ -19,6 +19,31 @@ scope A:
definition z equals 0
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [67/67]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [12/12]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_exception/good/split_unlabeled_exception.catala_en
View File

@ -14,6 +14,31 @@ scope A:
definition x equals 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [28/28]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [6/6]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_exception/good/two_exceptions_same_outcome.catala_en
View File

@ -20,6 +20,31 @@ scope A:
definition x under condition z = 0 consequence equals 0
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [45/45]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [10/10]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_exception/good/two_unlabeled_exceptions.catala_en
View File

@ -17,6 +17,31 @@ scope A:
definition y equals 3
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [55/55]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [12/12]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_exception/good/unlabeled_exception.catala_en
View File

@ -11,6 +11,31 @@ scope A:
definition x equals 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [28/28]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [6/6]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_exception/good/unsorted_unlabeled_exceptions.catala_en
View File

@ -17,6 +17,31 @@ scope A:
definition y equals 3
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [55/55]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [12/12]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_func/good/closure_conversion.catala_en
View File

@ -11,6 +11,31 @@ scope S:
definition z equals f of -1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [28/28]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Lcalc --avoid_exceptions -O --closure_conversion

25
tests/test_func/good/closure_conversion_reduce.catala_en
View File

@ -11,6 +11,31 @@ scope S:
potential_max among x such that potential_max is minimum or if collection empty then -1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [29/29]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [2/2]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Lcalc -s S --avoid_exceptions -O --closure_conversion
let scope S (S_in: S_in {x_in: collection integer}): S {y: integer} =

25
tests/test_func/good/closure_return.catala_en
View File

@ -9,6 +9,31 @@ scope S:
definition f of y equals if x then y else - y
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [18/18]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [2/2]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Lcalc --avoid_exceptions -O --closure_conversion

25
tests/test_func/good/closure_through_scope.catala_en
View File

@ -17,6 +17,31 @@ scope T:
definition y equals s.f of 2
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [44/44]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [6/6]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Lcalc -s T --avoid_exceptions -O --closure_conversion
let scope T (T_in: T_in): T {y: integer} =

120
tests/test_func/good/context_func.catala_en
View File

@ -2,7 +2,7 @@
```catala
declaration scope A:
output f content integer depends on x content integer
context output f content integer depends on x content integer
declaration scope B:
input b content boolean
@ -15,83 +15,63 @@ scope B:
definition a.f of x under condition b and x > 0 consequence equals x - 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [49/49]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [6/6]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [6/6]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Scopelang -s B
[ERROR]
It is impossible to give a definition to a subscope variable not tagged as input or context.
Incriminated subscope:
┌─⯈ tests/test_func/good/context_func.catala_en:9.3-9.4:
└─┐
9 │ a scope A
│ ‾
└─ Test
Incriminated variable:
┌─⯈ tests/test_func/good/context_func.catala_en:5.10-5.11:
└─┐
5 │ output f content integer depends on x content integer
│ ‾
└─ Test
Incriminated subscope variable definition:
┌─⯈ tests/test_func/good/context_func.catala_en:15.3-15.17:
└──┐
15 │ definition a.f of x under condition b and x > 0 consequence equals x - 1
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾
#return code 123#
let scope B (b: bool|input) =
let a.f : integer → ⟨integer⟩ = λ (x: integer) →
⟨ ⟨b && x > 0 ⊢ ⟨x - 1⟩⟩ | false ⊢ ∅ ⟩;
call A[a]
```
```catala-test-inline
$ catala Dcalc -s A
[ERROR]
It is impossible to give a definition to a subscope variable not tagged as input or context.
Incriminated subscope:
┌─⯈ tests/test_func/good/context_func.catala_en:9.3-9.4:
└─┐
9 │ a scope A
│ ‾
└─ Test
Incriminated variable:
┌─⯈ tests/test_func/good/context_func.catala_en:5.10-5.11:
└─┐
5 │ output f content integer depends on x content integer
│ ‾
└─ Test
Incriminated subscope variable definition:
┌─⯈ tests/test_func/good/context_func.catala_en:15.3-15.17:
└──┐
15 │ definition a.f of x under condition b and x > 0 consequence equals x - 1
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾
#return code 123#
let scope A
(A_in: A_in {f_in: integer → ⟨integer⟩})
: A {f: integer → integer}
=
let get f : integer → ⟨integer⟩ = A_in.f_in in
let set f : integer → integer =
λ (x: integer) →
error_empty
⟨ f x | true ⊢ ⟨error_empty ⟨ ⟨true ⊢ ⟨x + 1⟩⟩ | false ⊢ ∅ ⟩⟩ ⟩
in
return { A f = f; }
```
```catala-test-inline
$ catala Dcalc -s B
[ERROR]
It is impossible to give a definition to a subscope variable not tagged as input or context.
Incriminated subscope:
┌─⯈ tests/test_func/good/context_func.catala_en:9.3-9.4:
└─┐
9 │ a scope A
│ ‾
└─ Test
Incriminated variable:
┌─⯈ tests/test_func/good/context_func.catala_en:5.10-5.11:
└─┐
5 │ output f content integer depends on x content integer
│ ‾
└─ Test
Incriminated subscope variable definition:
┌─⯈ tests/test_func/good/context_func.catala_en:15.3-15.17:
└──┐
15 │ definition a.f of x under condition b and x > 0 consequence equals x - 1
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾
#return code 123#
let scope B (B_in: B_in {b_in: bool}): B =
let get b : bool = B_in.b_in in
let sub_set a.f : integer → ⟨integer⟩ =
λ (x: integer) →
⟨ ⟨b && x > 0 ⊢ ⟨x - 1⟩⟩ | false ⊢ ∅ ⟩
in
let call result : A {f: integer → integer} = A { A_in f_in = a.f; } in
let sub_get a.f : integer → integer = result.f in
return {B}
```

25
tests/test_func/good/func.catala_en
View File

@ -21,6 +21,31 @@ scope R:
definition r equals s.out
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [116/116]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [12/12]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [12/12]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [15/15]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s R
[RESULT] Computation successful! Results:

25
tests/test_func/good/param_consistency.catala_en
View File

@ -12,6 +12,31 @@ scope S:
definition out equals f1 of 10
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [37/37]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala typecheck
[RESULT] Typechecking successful!

25
tests/test_func/good/scope_call_func_struct_closure.catala_en
View File

@ -40,6 +40,31 @@ scope Foo:
This test case is tricky because it creates a situation where the type of the
two closures in Foo.r are different even with optimizations enabled.
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [133/133]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [15/15]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [10/10]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [15/15]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [11/11]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Lcalc --avoid_exceptions -O --closure_conversion

25
tests/test_io/good/all_io.catala_en
View File

@ -17,6 +17,31 @@ scope A:
definition f equals e + 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [73/73]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [10/10]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Dcalc -s A
let scope A

25
tests/test_io/good/condition_only_input.catala_en
View File

@ -14,6 +14,31 @@ scope A:
scope B:
assertion a.y = 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [35/35]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Dcalc -s B
let scope B (B_in: B_in): B =

25
tests/test_io/good/subscope.catala_en
View File

@ -20,6 +20,31 @@ scope B:
assertion a.c = 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [66/66]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [9/9]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Dcalc -s B
let scope B (B_in: B_in): B =

25
tests/test_literate/good/test_grave_char_en.catala_en
View File

@ -27,6 +27,31 @@ Even after `Catala` code block:
int main(void) { return 0; }
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [19/19]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [3/3]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_literate/good/test_grave_char_fr.catala_fr
View File

@ -27,6 +27,31 @@ Even after `Catala` code block:
int main(void) { return 0; }
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [19/19]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [3/3]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_metadata/good/test_markup_refactoring.catala_en
View File

@ -28,6 +28,31 @@ scope S2:
definition b equals B
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [40/40]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [6/6]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s S2
[RESULT] Computation successful! Results:

25
tests/test_modules/good/mod_def.catala_en
View File

@ -27,6 +27,31 @@ scope S:
definition e1 equals Maybe
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [25/25]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala typecheck --disable_warnings
[RESULT] Typechecking successful!

25
tests/test_modules/good/mod_def_context.catala_en
View File

@ -56,6 +56,31 @@ scope Stest:
definition x22 equals o2.cfun2 of 24
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [210/210]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [21/21]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [17/17]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [21/21]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [22/22]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala interpret -s Stest
[RESULT] Computation successful! Results:

25
tests/test_modules/good/mod_middle.catala_en
View File

@ -17,6 +17,31 @@ scope S:
definition o3 equals $44 * (decimal of x)
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [70/70]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [9/9]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [9/9]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [7/7]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala typecheck
[RESULT] Typechecking successful!

25
tests/test_modules/good/mod_use.catala_en
View File

@ -23,6 +23,31 @@ scope T2:
assertion o4 = 5.0
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [79/79]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [8/8]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala interpret -s T2
[RESULT] Computation successful! Results:

25
tests/test_modules/good/mod_use2.catala_en
View File

@ -15,6 +15,31 @@ scope T:
definition o3 equals t1.o3
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [49/49]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [8/8]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala interpret -s T
[RESULT] Computation successful! Results:

25
tests/test_modules/good/mod_use3.catala_en
View File

@ -19,6 +19,31 @@ scope T:
definition o3 equals t1.o3
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [49/49]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [8/8]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala interpret -s T
[RESULT] Computation successful! Results:

25
tests/test_modules/good/mod_use_context.catala_en
View File

@ -40,6 +40,31 @@ scope TestCall:
definition x22 equals o_override.cfun2 of 24
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [148/148]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [17/17]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [16/16]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [17/17]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [13/13]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala interpret -sTestCall
[RESULT] Computation successful! Results:

25
tests/test_money/good/literal_parsing.catala_en
View File

@ -11,6 +11,31 @@ scope A:
assertion x = y
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [27/27]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_money/good/simple.catala_en
View File

@ -12,6 +12,31 @@ scope A:
definition z equals $250,000,000 * ((x / y) * 0.2 %)
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [64/64]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [6/6]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [6/6]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [9/9]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

25
tests/test_name_resolution/good/let_in.catala_en
View File

@ -25,6 +25,31 @@ scope S:
A { -- x: a -- y : b }
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [64/64]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [6/6]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s S
[RESULT] Computation successful! Results:

25
tests/test_name_resolution/good/let_in2.catala_en
View File

@ -11,6 +11,31 @@ scope S:
a
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [28/28]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [3/3]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s S
[RESULT] Computation successful! Results:

25
tests/test_name_resolution/good/out_of_order.catala_en
View File

@ -18,6 +18,31 @@ scope S:
definition a equals A { -- x: 0 -- y : b }
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [41/41]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [6/6]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s S
[RESULT] Computation successful! Results:

37
tests/test_name_resolution/good/toplevel_defs.catala_en
View File

@ -19,6 +19,31 @@ scope S:
definition b equals glob2
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [32/32]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s S
[RESULT] Computation successful! Results:
@ -439,8 +464,8 @@ def s2(s2_in:S2In):
except EmptyError:
temp_a_5 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=37, start_column=10,
end_line=37, end_column=11,
start_line=62, start_column=10,
end_line=62, end_column=11,
law_headings=["Test toplevel function defs"]))
a = temp_a_5
return S2(a = a)
@ -468,8 +493,8 @@ def s3(s3_in:S3In):
except EmptyError:
temp_a_11 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=57, start_column=10,
end_line=57, end_column=11,
start_line=82, start_column=10,
end_line=82, end_column=11,
law_headings=["Test function def with two args"]))
a_1 = temp_a_11
return S3(a = a_1)
@ -495,8 +520,8 @@ def s4(s4_in:S4In):
except EmptyError:
temp_a_17 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=80, start_column=10,
end_line=80, end_column=11,
start_line=105, start_column=10,
end_line=105, end_column=11,
law_headings=["Test inline defs in toplevel defs"]))
a_2 = temp_a_17
return S4(a = a_2)

25
tests/test_name_resolution/good/toplevel_defs_simple.catala_en
View File

@ -10,6 +10,31 @@ scope S:
definition a equals glob1 >= 30.
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [14/14]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [2/2]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s S
[RESULT] Computation successful! Results:

25
tests/test_proof/good/array_length.catala_en
View File

@ -11,6 +11,31 @@ scope A:
definition y under condition (number of x) = 0 consequence equals false
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [34/34]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/assert.catala_en
View File

@ -22,6 +22,31 @@ scope Foo:
3
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [58/58]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [12/12]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [12/12]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/dates_get_year.catala_en
View File

@ -13,6 +13,31 @@ scope A:
definition y under condition get_year of x >= 2020 consequence equals false
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [66/66]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [14/14]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [14/14]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [7/7]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/dates_simple.catala_en
View File

@ -13,6 +13,31 @@ scope A:
definition y under condition x >= |2020-01-01| consequence equals false
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [54/54]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [8/8]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [8/8]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [7/7]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/direct_scope_call.catala_en
View File

@ -14,6 +14,31 @@ scope Foo:
(output of SubFoo with { -- x: 1 }).y
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [40/40]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof -s Foo
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/direct_scope_call_with_context.catala_en
View File

@ -15,6 +15,31 @@ scope Foo:
(output of SubFoo with {}).y
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [56/56]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [5/5]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [7/7]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof -s Foo
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/duration.catala_en
View File

@ -11,6 +11,31 @@ scope A:
definition y under condition (x + x) <= 100 day consequence equals false
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [34/34]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

32
tests/test_proof/good/enums-arith.catala_en
View File

@ -19,6 +19,38 @@ scope A:
definition x under condition match y with pattern -- A of a: a < 0 -- B of b: true consequence equals 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/enums-arith.catala_en:5.7-5.8:
└─┐
5 │ -- C content boolean
│ ‾
└─ Test
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [40/40]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?

32
tests/test_proof/good/enums-nonbool.catala_en
View File

@ -19,6 +19,38 @@ scope A:
definition x under condition match y with pattern -- A of a: false -- B of b: true consequence equals 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/enums-nonbool.catala_en:5.7-5.8:
└─┐
5 │ -- C content boolean
│ ‾
└─ Test
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [37/37]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?

32
tests/test_proof/good/enums.catala_en
View File

@ -18,6 +18,38 @@ scope A:
definition x under condition match y with pattern -- A of a: true -- B of b: false consequence equals 0
definition x under condition match y with pattern -- A of a: false -- B of b: true consequence equals 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/enums.catala_en:5.7-5.8:
└─┐
5 │ -- C content boolean
│ ‾
└─ Test
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [34/34]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?

25
tests/test_proof/good/enums_inj.catala_en
View File

@ -15,6 +15,31 @@ scope A:
definition y under condition x = C2 consequence equals 2
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [31/31]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/enums_unit.catala_en
View File

@ -19,6 +19,31 @@ scope A:
-- Case2 : true consequence equals 2
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [33/33]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [2/2]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/functions.catala_en
View File

@ -12,6 +12,31 @@ scope A:
definition z under condition x of true < 0 consequence equals -1
definition z under condition x of true > 0 consequence equals 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [48/48]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [7/7]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/let_in_condition.catala_en
View File

@ -11,6 +11,31 @@ scope A:
consequence equals true
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [13/13]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [2/2]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/money.catala_en
View File

@ -13,6 +13,31 @@ scope A:
definition y under condition x >= $100,000 consequence equals false
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [54/54]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [8/8]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [8/8]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [7/7]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/no_vars.catala_en
View File

@ -8,6 +8,31 @@ scope A:
definition x under condition (6*7 = 42) and (false or (true and 1458 / 27 = 54.))
consequence equals 0
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [31/31]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [2/2]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/rationals.catala_en
View File

@ -11,6 +11,31 @@ scope A:
definition y under condition x <= 1./3. consequence equals false
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [34/34]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/simple_vars.catala_en
View File

@ -14,6 +14,31 @@ scope A:
definition z under condition x < 0 consequence equals -1
definition z under condition x > 0 consequence equals 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [49/49]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [4/4]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [9/9]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_proof/good/structs.catala_en
View File

@ -18,6 +18,31 @@ scope A:
definition x under condition (y.a = 0) and y.b.c consequence equals 0
definition x under condition not (y.a = 0) or not y.b.c consequence equals 1
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [48/48]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [6/6]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [6/6]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [5/5]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[RESULT] No errors found during the proof mode run.

25
tests/test_scope/good/191_fix_record_name_confusion.catala_en
View File

@ -15,6 +15,31 @@ scope ScopeB:
definition a equals scopeA.a
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [25/25]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [1/1]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [4/4]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala OCaml -O

25
tests/test_scope/good/grand_parent_caller.catala_en
View File

@ -29,6 +29,31 @@ scope C:
definition z2 equals b.y2
```
```catala-test-inline
$ catala Typecheck --check_invariants
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [126/126]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [3/3]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [7/7]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [19/19]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:

32
tests/test_scope/good/nothing.catala_en
View File

@ -5,6 +5,38 @@ declaration scope Foo2:
output bar content integer
```
```catala-test-inline
$ catala Typecheck --check_invariants
[WARNING] In scope "Foo2", the variable "bar" is declared but never defined; did you forget something?
┌─⯈ tests/test_scope/good/nothing.catala_en:5.10-5.13:
└─┐
5 │ output bar content integer
│ ‾‾‾
└─ Test
[RESULT]
Invariant Dcalc__Invariants.invariant_typing_defaults
checked. result: [6/6]
[RESULT]
Invariant Dcalc__Invariants.invariant_match_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_app_inversion
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_return_a_function
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_no_partial_evaluation
checked. result: [0/0]
[RESULT]
Invariant Dcalc__Invariants.invariant_default_no_arrow
checked. result: [1/1]
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Scalc -s Foo2 -O -t
[WARNING] In scope "Foo2", the variable "bar" is declared but never defined; did you forget something?

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