From 67e36dcf424bd060887730b45d74a5760894c2dd Mon Sep 17 00:00:00 2001 From: adelaett <90894311+adelaett@users.noreply.github.com> Date: Mon, 4 Dec 2023 16:47:52 +0100 Subject: [PATCH 1/9] Adding Typing Invariant for TDefault Added a new type safety invariant to ensure that the type `TDefault` can only appear in certain positions, * 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). This is crucial to maintain the safety of the type system, as demonstrated in the formal development. The invariant was checked on all tests cases and on family and housing benefits. Adjusted inversion invariant about app to handle external objects as well. --- compiler/dcalc/invariants.ml | 84 +++++++++++++++++++++++++++++++++--- 1 file changed, 77 insertions(+), 7 deletions(-) diff --git a/compiler/dcalc/invariants.ml b/compiler/dcalc/invariants.ml index 4024f103..f15f710c 100644 --- a/compiler/dcalc/invariants.ml +++ b/compiler/dcalc/invariants.ml @@ -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,74 @@ 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). + + 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 -> true + | TClosureEnv -> + assert false (* we should not check this one. It is at least an warning *) + +let rec check_type ctx ty = + match Mark.remove ty with + | TStruct n -> + let s = StructName.Map.find n ctx.ctx_structs in + StructField.Map.for_all (fun _k ty -> check_type ctx ty) s + | TArrow (args, res) -> + List.exists Fun.id + [ + (match args with + | [(TStruct n, _)] -> + ScopeName.Map.exists + (fun _k info -> StructName.equal info.in_struct_name n) + ctx.ctx_scopes + && + let s = StructName.Map.find n ctx.ctx_structs in + StructField.Map.for_all (fun _k ty -> check_type ctx ty) s + | _ -> false) + && check_typ_no_default ctx 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); + ] + | TDefault arg -> check_typ_no_default ctx arg + | _ -> check_typ_no_default ctx ty + +let invariant_typing_defaults () : string * invariant_expr = + ( __FUNCTION__, + fun ctx e -> + if check_type 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 +198,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; ] From 030705eacdbe0404d95f690246130cc1a23cbcaa Mon Sep 17 00:00:00 2001 From: adelaett <90894311+adelaett@users.noreply.github.com> Date: Tue, 5 Dec 2023 13:33:22 +0100 Subject: [PATCH 2/9] Make the typing invariant more precise. --- compiler/dcalc/invariants.ml | 76 ++++++++++++++++++++++++------------ 1 file changed, 51 insertions(+), 25 deletions(-) diff --git a/compiler/dcalc/invariants.ml b/compiler/dcalc/invariants.ml index f15f710c..4ce4db08 100644 --- a/compiler/dcalc/invariants.ml +++ b/compiler/dcalc/invariants.ml @@ -133,6 +133,14 @@ let invariant_match_inversion () : string * invariant_expr = * 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 -> ; S_in {x: int -> } -> S {y: bool} + + While the following types does not follow the invariant: + + <>; >; -> int; S_in {x: int -> } -> S {y: } + This is crucial to maintain the safety of the type system, as demonstrated in the formal development. *) @@ -151,41 +159,59 @@ let rec check_typ_no_default ctx ty = 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 -> true + | TAny -> + Message.emit_warning + "The typing default invariant was checked too late in the compilation \ + scheme. It is impossible to check whenever the type verify this \ + invariant."; + true | TClosureEnv -> - assert false (* we should not check this one. It is at least an warning *) + Message.emit_warning + "In the compilation process, the default invariant for typing was not \ + checked early enough. Since it's impossible to verify this invariant at \ + any point due to the closure environment holding an existential type."; + true (* we should not check this one. *) -let rec check_type ctx ty = +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 - StructField.Map.for_all (fun _k ty -> check_type ctx ty) s - | TArrow (args, res) -> - List.exists Fun.id - [ - (match args with - | [(TStruct n, _)] -> - ScopeName.Map.exists - (fun _k info -> StructName.equal info.in_struct_name n) - ctx.ctx_scopes - && - let s = StructName.Map.find n ctx.ctx_structs in - StructField.Map.for_all (fun _k ty -> check_type ctx ty) s - | _ -> false) - && check_typ_no_default ctx 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); - ] + 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 - | _ -> check_typ_no_default ctx ty + | _ -> false let invariant_typing_defaults () : string * invariant_expr = ( __FUNCTION__, fun ctx e -> - if check_type ctx (Expr.ty e) then Pass + if check_type_root ctx (Expr.ty e) then Pass else ( Message.emit_warning "typing error %a@." (Print.typ ctx) (Expr.ty e); Fail) ) From e1bda33e0755fb4ed0b99fa39d802a2d275430e9 Mon Sep 17 00:00:00 2001 From: adelaett <90894311+adelaett@users.noreply.github.com> Date: Tue, 5 Dec 2023 16:50:25 +0100 Subject: [PATCH 3/9] fmt --- compiler/dcalc/invariants.ml | 19 +++++++++++-------- compiler/dcalc/invariants.mli | 11 ++++++++--- 2 files changed, 19 insertions(+), 11 deletions(-) diff --git a/compiler/dcalc/invariants.ml b/compiler/dcalc/invariants.ml index 4ce4db08..d02b5fea 100644 --- a/compiler/dcalc/invariants.ml +++ b/compiler/dcalc/invariants.ml @@ -135,11 +135,13 @@ let invariant_match_inversion () : string * invariant_expr = For instance, the following types do follow the invariant: - int; bool; int -> bool; ; bool>; int -> ; S_in {x: int -> } -> S {y: bool} + int; bool; int -> bool; ; bool>; int -> ; S_in {x: int -> + } -> S {y: bool} While the following types does not follow the invariant: - <>; >; -> int; S_in {x: int -> } -> S {y: } + <>; >; -> int; S_in {x: int -> } -> S {y: + } This is crucial to maintain the safety of the type system, as demonstrated in the formal development. *) @@ -160,16 +162,17 @@ let rec check_typ_no_default ctx ty = | TArray ty -> check_typ_no_default ctx ty | TDefault _t -> false | TAny -> + (* found TAny *) Message.emit_warning - "The typing default invariant was checked too late in the compilation \ - scheme. It is impossible to check whenever the type verify this \ - invariant."; + "Internal error: the type was not fully resolved, it is not possible to \ + verify whenever the typing_default invariant holds."; true | TClosureEnv -> Message.emit_warning - "In the compilation process, the default invariant for typing was not \ - checked early enough. Since it's impossible to verify this invariant at \ - any point due to the closure environment holding an existential type."; + "Internal error: In the compilation process, the default invariant for \ + typing was not checked early enough. Since it's impossible to verify \ + this invariant at any point due to the closure environment holding an \ + existential type."; true (* we should not check this one. *) let check_type_thunked_or_nodefault ctx ty = diff --git a/compiler/dcalc/invariants.mli b/compiler/dcalc/invariants.mli index ac2f9bb1..89001f86 100644 --- a/compiler/dcalc/invariants.mli +++ b/compiler/dcalc/invariants.mli @@ -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.*) From 934ab328ecf17e0b6fa6709cb0e2c5e930299ca1 Mon Sep 17 00:00:00 2001 From: adelaett <90894311+adelaett@users.noreply.github.com> Date: Tue, 5 Dec 2023 16:50:58 +0100 Subject: [PATCH 4/9] invariant checking is now available without printing the ast using the typecheck subprogram --- compiler/driver.ml | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/compiler/driver.ml b/compiler/driver.ml index a4362364..df6b3e75 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -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,27 @@ 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 + let prg = + Shared_ast.Typing.program ~leave_unresolved:false (Program.untype prg) + in + (* Additionally, we might want to check the invariants. *) + if check_invariants then ( + 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 = From a69776e6b56ee17692649f382f6732ff8131384b Mon Sep 17 00:00:00 2001 From: adelaett <90894311+adelaett@users.noreply.github.com> Date: Tue, 5 Dec 2023 16:54:14 +0100 Subject: [PATCH 5/9] checking invariants on all tests as well as on social benefits of french law --- ...ts_calcul_al_accession_propriete.catala_fr | 23 ++++++++++++ .../tests/tests_calcul_al_locatif.catala_fr | 23 ++++++++++++ .../tests_calcul_al_logement_foyer.catala_fr | 23 ++++++++++++ .../tests/tests_invariants.catala_fr | 27 ++++++++++++++ .../tests/test_invariants.catala_fr | 27 ++++++++++++++ .../test_arithmetic/good/priorities.catala_en | 25 +++++++++++++ tests/test_arithmetic/good/trivial.catala_en | 25 +++++++++++++ tests/test_array/good/aggregation.catala_en | 25 +++++++++++++ tests/test_array/good/aggregation_2.catala_en | 25 +++++++++++++ tests/test_array/good/aggregation_3.catala_en | 25 +++++++++++++ tests/test_array/good/concatenation.catala_en | 25 +++++++++++++ tests/test_array/good/filter.catala_en | 25 +++++++++++++ tests/test_array/good/filter_map.catala_en | 25 +++++++++++++ tests/test_array/good/fold.catala_en | 25 +++++++++++++ tests/test_array/good/map.catala_en | 25 +++++++++++++ tests/test_array/good/simple.catala_en | 25 +++++++++++++ tests/test_array/good/simpler.catala_en | 25 +++++++++++++ tests/test_array/good/simplest.catala_en | 25 +++++++++++++ tests/test_bool/good/test_bool.catala_en | 25 +++++++++++++ .../test_bool/good/test_precedence.catala_en | 25 +++++++++++++ tests/test_bool/good/test_xor.catala_en | 25 +++++++++++++ tests/test_date/good/durations.catala_en | 25 +++++++++++++ .../good/rounding_option_en.catala_en | 25 +++++++++++++ .../good/rounding_option_fr.catala_fr | 25 +++++++++++++ tests/test_date/good/simple.catala_en | 25 +++++++++++++ .../good/infinite_precision.catala_en | 25 +++++++++++++ tests/test_dec/good/rounding.catala_en | 25 +++++++++++++ tests/test_dec/good/simple.catala_en | 25 +++++++++++++ .../test_dec/good/zero_after_comma.catala_en | 25 +++++++++++++ .../good/disambiguated_cases.catala_en | 25 +++++++++++++ .../good/quick_pattern_check.catala_en | 25 +++++++++++++ tests/test_enum/good/simple.catala_en | 25 +++++++++++++ tests/test_enum/good/wildcard.catala_en | 25 +++++++++++++ .../good/context_with_default.catala_en | 25 +++++++++++++ .../good/duplicate_labels.catala_en | 25 +++++++++++++ tests/test_exception/good/exception.catala_en | 25 +++++++++++++ .../good/exceptions_squared.catala_en | 25 +++++++++++++ .../good/grouped_exceptions.catala_en | 25 +++++++++++++ .../good/groups_of_exceptions.catala_en | 25 +++++++++++++ .../good/same_label_two_variables.catala_en | 25 +++++++++++++ .../good/split_unlabeled_exception.catala_en | 25 +++++++++++++ .../two_exceptions_same_outcome.catala_en | 25 +++++++++++++ .../good/two_unlabeled_exceptions.catala_en | 25 +++++++++++++ .../good/unlabeled_exception.catala_en | 25 +++++++++++++ .../unsorted_unlabeled_exceptions.catala_en | 25 +++++++++++++ .../good/closure_conversion.catala_en | 25 +++++++++++++ .../good/closure_conversion_reduce.catala_en | 25 +++++++++++++ tests/test_func/good/closure_return.catala_en | 25 +++++++++++++ .../good/closure_through_scope.catala_en | 25 +++++++++++++ tests/test_func/good/func.catala_en | 25 +++++++++++++ .../good/param_consistency.catala_en | 25 +++++++++++++ .../scope_call_func_struct_closure.catala_en | 25 +++++++++++++ tests/test_io/good/all_io.catala_en | 25 +++++++++++++ .../good/condition_only_input.catala_en | 25 +++++++++++++ tests/test_io/good/subscope.catala_en | 25 +++++++++++++ .../good/test_grave_char_en.catala_en | 25 +++++++++++++ .../good/test_grave_char_fr.catala_fr | 25 +++++++++++++ .../good/test_markup_refactoring.catala_en | 25 +++++++++++++ tests/test_modules/good/mod_def.catala_en | 25 +++++++++++++ .../good/mod_def_context.catala_en | 25 +++++++++++++ tests/test_modules/good/mod_middle.catala_en | 25 +++++++++++++ tests/test_modules/good/mod_use.catala_en | 25 +++++++++++++ tests/test_modules/good/mod_use2.catala_en | 25 +++++++++++++ tests/test_modules/good/mod_use3.catala_en | 25 +++++++++++++ .../good/mod_use_context.catala_en | 25 +++++++++++++ .../test_money/good/literal_parsing.catala_en | 25 +++++++++++++ tests/test_money/good/simple.catala_en | 25 +++++++++++++ .../good/let_in.catala_en | 25 +++++++++++++ .../good/let_in2.catala_en | 25 +++++++++++++ .../good/out_of_order.catala_en | 25 +++++++++++++ .../good/toplevel_defs.catala_en | 37 ++++++++++++++++--- .../good/toplevel_defs_simple.catala_en | 25 +++++++++++++ tests/test_proof/good/array_length.catala_en | 25 +++++++++++++ tests/test_proof/good/assert.catala_en | 25 +++++++++++++ .../test_proof/good/dates_get_year.catala_en | 25 +++++++++++++ tests/test_proof/good/dates_simple.catala_en | 25 +++++++++++++ .../good/direct_scope_call.catala_en | 25 +++++++++++++ .../direct_scope_call_with_context.catala_en | 25 +++++++++++++ tests/test_proof/good/duration.catala_en | 25 +++++++++++++ tests/test_proof/good/enums_inj.catala_en | 25 +++++++++++++ tests/test_proof/good/enums_unit.catala_en | 25 +++++++++++++ tests/test_proof/good/functions.catala_en | 25 +++++++++++++ .../good/let_in_condition.catala_en | 25 +++++++++++++ tests/test_proof/good/money.catala_en | 25 +++++++++++++ tests/test_proof/good/no_vars.catala_en | 25 +++++++++++++ tests/test_proof/good/rationals.catala_en | 25 +++++++++++++ tests/test_proof/good/simple_vars.catala_en | 25 +++++++++++++ tests/test_proof/good/structs.catala_en | 25 +++++++++++++ .../191_fix_record_name_confusion.catala_en | 25 +++++++++++++ .../good/grand_parent_caller.catala_en | 25 +++++++++++++ tests/test_scope/good/nothing.catala_en | 32 ++++++++++++++++ tests/test_scope/good/scope_call.catala_en | 25 +++++++++++++ tests/test_scope/good/scope_call2.catala_en | 25 +++++++++++++ tests/test_scope/good/scope_call3.catala_en | 25 +++++++++++++ tests/test_scope/good/scope_call4.catala_en | 25 +++++++++++++ tests/test_scope/good/simple.catala_en | 25 +++++++++++++ tests/test_scope/good/sub_scope.catala_en | 25 +++++++++++++ tests/test_scope/good/sub_sub_scope.catala_en | 25 +++++++++++++ ...ubscope_function_arg_not_defined.catala_en | 25 +++++++++++++ ...bscope_function_arg_not_defined2.catala_en | 25 +++++++++++++ tests/test_struct/good/nested3.catala_en | 25 +++++++++++++ tests/test_struct/good/simple.catala_en | 25 +++++++++++++ tests/test_typing/good/overload.catala_en | 25 +++++++++++++ .../test_variable_state/good/simple.catala_en | 25 +++++++++++++ .../good/subscope.catala_en | 25 +++++++++++++ 105 files changed, 2636 insertions(+), 6 deletions(-) create mode 100644 examples/aides_logement/tests/tests_invariants.catala_fr create mode 100644 examples/allocations_familiales/tests/test_invariants.catala_fr diff --git a/examples/aides_logement/tests/tests_calcul_al_accession_propriete.catala_fr b/examples/aides_logement/tests/tests_calcul_al_accession_propriete.catala_fr index 02a3bc08..29db6ac2 100644 --- a/examples/aides_logement/tests/tests_calcul_al_accession_propriete.catala_fr +++ b/examples/aides_logement/tests/tests_calcul_al_accession_propriete.catala_fr @@ -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: diff --git a/examples/aides_logement/tests/tests_calcul_al_locatif.catala_fr b/examples/aides_logement/tests/tests_calcul_al_locatif.catala_fr index 973f3148..65765b40 100644 --- a/examples/aides_logement/tests/tests_calcul_al_locatif.catala_fr +++ b/examples/aides_logement/tests/tests_calcul_al_locatif.catala_fr @@ -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: diff --git a/examples/aides_logement/tests/tests_calcul_al_logement_foyer.catala_fr b/examples/aides_logement/tests/tests_calcul_al_logement_foyer.catala_fr index 226c9190..34cc9e9a 100644 --- a/examples/aides_logement/tests/tests_calcul_al_logement_foyer.catala_fr +++ b/examples/aides_logement/tests/tests_calcul_al_logement_foyer.catala_fr @@ -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: diff --git a/examples/aides_logement/tests/tests_invariants.catala_fr b/examples/aides_logement/tests/tests_invariants.catala_fr new file mode 100644 index 00000000..0aacff2d --- /dev/null +++ b/examples/aides_logement/tests/tests_invariants.catala_fr @@ -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! +``` diff --git a/examples/allocations_familiales/tests/test_invariants.catala_fr b/examples/allocations_familiales/tests/test_invariants.catala_fr new file mode 100644 index 00000000..b2d25ae4 --- /dev/null +++ b/examples/allocations_familiales/tests/test_invariants.catala_fr @@ -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! +``` \ No newline at end of file diff --git a/tests/test_arithmetic/good/priorities.catala_en b/tests/test_arithmetic/good/priorities.catala_en index 33681752..fa4cd3fa 100644 --- a/tests/test_arithmetic/good/priorities.catala_en +++ b/tests/test_arithmetic/good/priorities.catala_en @@ -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: diff --git a/tests/test_arithmetic/good/trivial.catala_en b/tests/test_arithmetic/good/trivial.catala_en index 161000fb..84af8eae 100644 --- a/tests/test_arithmetic/good/trivial.catala_en +++ b/tests/test_arithmetic/good/trivial.catala_en @@ -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: diff --git a/tests/test_array/good/aggregation.catala_en b/tests/test_array/good/aggregation.catala_en index faccaf00..2463d2c9 100644 --- a/tests/test_array/good/aggregation.catala_en +++ b/tests/test_array/good/aggregation.catala_en @@ -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: diff --git a/tests/test_array/good/aggregation_2.catala_en b/tests/test_array/good/aggregation_2.catala_en index ba22d2ff..13688594 100644 --- a/tests/test_array/good/aggregation_2.catala_en +++ b/tests/test_array/good/aggregation_2.catala_en @@ -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: diff --git a/tests/test_array/good/aggregation_3.catala_en b/tests/test_array/good/aggregation_3.catala_en index f8e7cc0b..56724de9 100644 --- a/tests/test_array/good/aggregation_3.catala_en +++ b/tests/test_array/good/aggregation_3.catala_en @@ -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) = diff --git a/tests/test_array/good/concatenation.catala_en b/tests/test_array/good/concatenation.catala_en index ad5b0452..c019e110 100644 --- a/tests/test_array/good/concatenation.catala_en +++ b/tests/test_array/good/concatenation.catala_en @@ -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: diff --git a/tests/test_array/good/filter.catala_en b/tests/test_array/good/filter.catala_en index b007e438..43c5d1ff 100644 --- a/tests/test_array/good/filter.catala_en +++ b/tests/test_array/good/filter.catala_en @@ -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: diff --git a/tests/test_array/good/filter_map.catala_en b/tests/test_array/good/filter_map.catala_en index bb8fe221..dfac0106 100644 --- a/tests/test_array/good/filter_map.catala_en +++ b/tests/test_array/good/filter_map.catala_en @@ -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: diff --git a/tests/test_array/good/fold.catala_en b/tests/test_array/good/fold.catala_en index ba22d2ff..13688594 100644 --- a/tests/test_array/good/fold.catala_en +++ b/tests/test_array/good/fold.catala_en @@ -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: diff --git a/tests/test_array/good/map.catala_en b/tests/test_array/good/map.catala_en index 7ee14341..13003dc6 100644 --- a/tests/test_array/good/map.catala_en +++ b/tests/test_array/good/map.catala_en @@ -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: diff --git a/tests/test_array/good/simple.catala_en b/tests/test_array/good/simple.catala_en index d5bea45c..6a558db3 100644 --- a/tests/test_array/good/simple.catala_en +++ b/tests/test_array/good/simple.catala_en @@ -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: diff --git a/tests/test_array/good/simpler.catala_en b/tests/test_array/good/simpler.catala_en index 647c421c..8086a506 100644 --- a/tests/test_array/good/simpler.catala_en +++ b/tests/test_array/good/simpler.catala_en @@ -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: diff --git a/tests/test_array/good/simplest.catala_en b/tests/test_array/good/simplest.catala_en index 120fb71a..51e7ecf1 100644 --- a/tests/test_array/good/simplest.catala_en +++ b/tests/test_array/good/simplest.catala_en @@ -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: diff --git a/tests/test_bool/good/test_bool.catala_en b/tests/test_bool/good/test_bool.catala_en index 920d5f4e..ab6bf8fa 100644 --- a/tests/test_bool/good/test_bool.catala_en +++ b/tests/test_bool/good/test_bool.catala_en @@ -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 = diff --git a/tests/test_bool/good/test_precedence.catala_en b/tests/test_bool/good/test_precedence.catala_en index 2ea8ebdf..9a6d9135 100644 --- a/tests/test_bool/good/test_precedence.catala_en +++ b/tests/test_bool/good/test_precedence.catala_en @@ -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: diff --git a/tests/test_bool/good/test_xor.catala_en b/tests/test_bool/good/test_xor.catala_en index 68fd6d39..1e1c0abf 100644 --- a/tests/test_bool/good/test_xor.catala_en +++ b/tests/test_bool/good/test_xor.catala_en @@ -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: diff --git a/tests/test_date/good/durations.catala_en b/tests/test_date/good/durations.catala_en index a5eac80f..d0bf816b 100644 --- a/tests/test_date/good/durations.catala_en +++ b/tests/test_date/good/durations.catala_en @@ -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: diff --git a/tests/test_date/good/rounding_option_en.catala_en b/tests/test_date/good/rounding_option_en.catala_en index f89f9421..41c4b91b 100644 --- a/tests/test_date/good/rounding_option_en.catala_en +++ b/tests/test_date/good/rounding_option_en.catala_en @@ -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: diff --git a/tests/test_date/good/rounding_option_fr.catala_fr b/tests/test_date/good/rounding_option_fr.catala_fr index 5568d4ad..144e017a 100644 --- a/tests/test_date/good/rounding_option_fr.catala_fr +++ b/tests/test_date/good/rounding_option_fr.catala_fr @@ -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: diff --git a/tests/test_date/good/simple.catala_en b/tests/test_date/good/simple.catala_en index 30f41bb6..30b4e514 100644 --- a/tests/test_date/good/simple.catala_en +++ b/tests/test_date/good/simple.catala_en @@ -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: diff --git a/tests/test_dec/good/infinite_precision.catala_en b/tests/test_dec/good/infinite_precision.catala_en index 2726bfd9..18ba253d 100644 --- a/tests/test_dec/good/infinite_precision.catala_en +++ b/tests/test_dec/good/infinite_precision.catala_en @@ -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: diff --git a/tests/test_dec/good/rounding.catala_en b/tests/test_dec/good/rounding.catala_en index c5d86abb..9533ac2c 100644 --- a/tests/test_dec/good/rounding.catala_en +++ b/tests/test_dec/good/rounding.catala_en @@ -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: diff --git a/tests/test_dec/good/simple.catala_en b/tests/test_dec/good/simple.catala_en index 67b3652c..4b917a8c 100644 --- a/tests/test_dec/good/simple.catala_en +++ b/tests/test_dec/good/simple.catala_en @@ -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: diff --git a/tests/test_dec/good/zero_after_comma.catala_en b/tests/test_dec/good/zero_after_comma.catala_en index 96dfc9a0..45ca5cb4 100644 --- a/tests/test_dec/good/zero_after_comma.catala_en +++ b/tests/test_dec/good/zero_after_comma.catala_en @@ -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: diff --git a/tests/test_enum/good/disambiguated_cases.catala_en b/tests/test_enum/good/disambiguated_cases.catala_en index ce05e5f3..893af97d 100644 --- a/tests/test_enum/good/disambiguated_cases.catala_en +++ b/tests/test_enum/good/disambiguated_cases.catala_en @@ -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: diff --git a/tests/test_enum/good/quick_pattern_check.catala_en b/tests/test_enum/good/quick_pattern_check.catala_en index 8503514c..cddeff8c 100644 --- a/tests/test_enum/good/quick_pattern_check.catala_en +++ b/tests/test_enum/good/quick_pattern_check.catala_en @@ -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: diff --git a/tests/test_enum/good/simple.catala_en b/tests/test_enum/good/simple.catala_en index 4967bb98..4b3ad5d9 100644 --- a/tests/test_enum/good/simple.catala_en +++ b/tests/test_enum/good/simple.catala_en @@ -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: diff --git a/tests/test_enum/good/wildcard.catala_en b/tests/test_enum/good/wildcard.catala_en index bfd60e67..a45bf7dd 100644 --- a/tests/test_enum/good/wildcard.catala_en +++ b/tests/test_enum/good/wildcard.catala_en @@ -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: diff --git a/tests/test_exception/good/context_with_default.catala_en b/tests/test_exception/good/context_with_default.catala_en index f1a13a92..807628bf 100644 --- a/tests/test_exception/good/context_with_default.catala_en +++ b/tests/test_exception/good/context_with_default.catala_en @@ -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! diff --git a/tests/test_exception/good/duplicate_labels.catala_en b/tests/test_exception/good/duplicate_labels.catala_en index b49ce86b..56fed0ed 100644 --- a/tests/test_exception/good/duplicate_labels.catala_en +++ b/tests/test_exception/good/duplicate_labels.catala_en @@ -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: diff --git a/tests/test_exception/good/exception.catala_en b/tests/test_exception/good/exception.catala_en index 5aff744b..d1b00e24 100644 --- a/tests/test_exception/good/exception.catala_en +++ b/tests/test_exception/good/exception.catala_en @@ -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: diff --git a/tests/test_exception/good/exceptions_squared.catala_en b/tests/test_exception/good/exceptions_squared.catala_en index b39e6467..bdf6afea 100644 --- a/tests/test_exception/good/exceptions_squared.catala_en +++ b/tests/test_exception/good/exceptions_squared.catala_en @@ -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: diff --git a/tests/test_exception/good/grouped_exceptions.catala_en b/tests/test_exception/good/grouped_exceptions.catala_en index e2ac8e22..ce193623 100644 --- a/tests/test_exception/good/grouped_exceptions.catala_en +++ b/tests/test_exception/good/grouped_exceptions.catala_en @@ -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: diff --git a/tests/test_exception/good/groups_of_exceptions.catala_en b/tests/test_exception/good/groups_of_exceptions.catala_en index 6144ba7f..ab3edff8 100644 --- a/tests/test_exception/good/groups_of_exceptions.catala_en +++ b/tests/test_exception/good/groups_of_exceptions.catala_en @@ -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: diff --git a/tests/test_exception/good/same_label_two_variables.catala_en b/tests/test_exception/good/same_label_two_variables.catala_en index df3626be..07ea2d50 100644 --- a/tests/test_exception/good/same_label_two_variables.catala_en +++ b/tests/test_exception/good/same_label_two_variables.catala_en @@ -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: diff --git a/tests/test_exception/good/split_unlabeled_exception.catala_en b/tests/test_exception/good/split_unlabeled_exception.catala_en index 10fd25f7..f9ea6570 100644 --- a/tests/test_exception/good/split_unlabeled_exception.catala_en +++ b/tests/test_exception/good/split_unlabeled_exception.catala_en @@ -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: diff --git a/tests/test_exception/good/two_exceptions_same_outcome.catala_en b/tests/test_exception/good/two_exceptions_same_outcome.catala_en index 9af9e5a4..c4bd1266 100644 --- a/tests/test_exception/good/two_exceptions_same_outcome.catala_en +++ b/tests/test_exception/good/two_exceptions_same_outcome.catala_en @@ -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: diff --git a/tests/test_exception/good/two_unlabeled_exceptions.catala_en b/tests/test_exception/good/two_unlabeled_exceptions.catala_en index 57cff4f3..ada46683 100644 --- a/tests/test_exception/good/two_unlabeled_exceptions.catala_en +++ b/tests/test_exception/good/two_unlabeled_exceptions.catala_en @@ -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: diff --git a/tests/test_exception/good/unlabeled_exception.catala_en b/tests/test_exception/good/unlabeled_exception.catala_en index 10bb1bb6..7d488a1a 100644 --- a/tests/test_exception/good/unlabeled_exception.catala_en +++ b/tests/test_exception/good/unlabeled_exception.catala_en @@ -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: diff --git a/tests/test_exception/good/unsorted_unlabeled_exceptions.catala_en b/tests/test_exception/good/unsorted_unlabeled_exceptions.catala_en index 363f8488..7500f312 100644 --- a/tests/test_exception/good/unsorted_unlabeled_exceptions.catala_en +++ b/tests/test_exception/good/unsorted_unlabeled_exceptions.catala_en @@ -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: diff --git a/tests/test_func/good/closure_conversion.catala_en b/tests/test_func/good/closure_conversion.catala_en index 2e0f5e52..d55f9da5 100644 --- a/tests/test_func/good/closure_conversion.catala_en +++ b/tests/test_func/good/closure_conversion.catala_en @@ -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 diff --git a/tests/test_func/good/closure_conversion_reduce.catala_en b/tests/test_func/good/closure_conversion_reduce.catala_en index 97473ea3..d87764c0 100644 --- a/tests/test_func/good/closure_conversion_reduce.catala_en +++ b/tests/test_func/good/closure_conversion_reduce.catala_en @@ -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} = diff --git a/tests/test_func/good/closure_return.catala_en b/tests/test_func/good/closure_return.catala_en index 84a8bc40..cb69b33c 100644 --- a/tests/test_func/good/closure_return.catala_en +++ b/tests/test_func/good/closure_return.catala_en @@ -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 diff --git a/tests/test_func/good/closure_through_scope.catala_en b/tests/test_func/good/closure_through_scope.catala_en index f2f9d2f9..fc773d97 100644 --- a/tests/test_func/good/closure_through_scope.catala_en +++ b/tests/test_func/good/closure_through_scope.catala_en @@ -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} = diff --git a/tests/test_func/good/func.catala_en b/tests/test_func/good/func.catala_en index f0ce6b76..fd16429f 100644 --- a/tests/test_func/good/func.catala_en +++ b/tests/test_func/good/func.catala_en @@ -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: diff --git a/tests/test_func/good/param_consistency.catala_en b/tests/test_func/good/param_consistency.catala_en index 9805230c..184b95f8 100644 --- a/tests/test_func/good/param_consistency.catala_en +++ b/tests/test_func/good/param_consistency.catala_en @@ -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! diff --git a/tests/test_func/good/scope_call_func_struct_closure.catala_en b/tests/test_func/good/scope_call_func_struct_closure.catala_en index 5632cbc4..9c080530 100644 --- a/tests/test_func/good/scope_call_func_struct_closure.catala_en +++ b/tests/test_func/good/scope_call_func_struct_closure.catala_en @@ -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 diff --git a/tests/test_io/good/all_io.catala_en b/tests/test_io/good/all_io.catala_en index c6265e1f..3087c185 100644 --- a/tests/test_io/good/all_io.catala_en +++ b/tests/test_io/good/all_io.catala_en @@ -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 diff --git a/tests/test_io/good/condition_only_input.catala_en b/tests/test_io/good/condition_only_input.catala_en index 087ee740..912ecc1b 100644 --- a/tests/test_io/good/condition_only_input.catala_en +++ b/tests/test_io/good/condition_only_input.catala_en @@ -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 = diff --git a/tests/test_io/good/subscope.catala_en b/tests/test_io/good/subscope.catala_en index 9432378f..75e024bf 100644 --- a/tests/test_io/good/subscope.catala_en +++ b/tests/test_io/good/subscope.catala_en @@ -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 = diff --git a/tests/test_literate/good/test_grave_char_en.catala_en b/tests/test_literate/good/test_grave_char_en.catala_en index d73e130c..feb9bb35 100644 --- a/tests/test_literate/good/test_grave_char_en.catala_en +++ b/tests/test_literate/good/test_grave_char_en.catala_en @@ -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: diff --git a/tests/test_literate/good/test_grave_char_fr.catala_fr b/tests/test_literate/good/test_grave_char_fr.catala_fr index 0c324411..b9a6db0c 100644 --- a/tests/test_literate/good/test_grave_char_fr.catala_fr +++ b/tests/test_literate/good/test_grave_char_fr.catala_fr @@ -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: diff --git a/tests/test_metadata/good/test_markup_refactoring.catala_en b/tests/test_metadata/good/test_markup_refactoring.catala_en index 0bead969..06c0bd23 100644 --- a/tests/test_metadata/good/test_markup_refactoring.catala_en +++ b/tests/test_metadata/good/test_markup_refactoring.catala_en @@ -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: diff --git a/tests/test_modules/good/mod_def.catala_en b/tests/test_modules/good/mod_def.catala_en index 5b8936d1..ee5fdf93 100644 --- a/tests/test_modules/good/mod_def.catala_en +++ b/tests/test_modules/good/mod_def.catala_en @@ -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! diff --git a/tests/test_modules/good/mod_def_context.catala_en b/tests/test_modules/good/mod_def_context.catala_en index 4384f148..f3793ede 100644 --- a/tests/test_modules/good/mod_def_context.catala_en +++ b/tests/test_modules/good/mod_def_context.catala_en @@ -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: diff --git a/tests/test_modules/good/mod_middle.catala_en b/tests/test_modules/good/mod_middle.catala_en index 5d44ef03..c3c9462a 100644 --- a/tests/test_modules/good/mod_middle.catala_en +++ b/tests/test_modules/good/mod_middle.catala_en @@ -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! diff --git a/tests/test_modules/good/mod_use.catala_en b/tests/test_modules/good/mod_use.catala_en index 6bf3245a..f1cb86d2 100644 --- a/tests/test_modules/good/mod_use.catala_en +++ b/tests/test_modules/good/mod_use.catala_en @@ -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: diff --git a/tests/test_modules/good/mod_use2.catala_en b/tests/test_modules/good/mod_use2.catala_en index 09f86c56..c74ed061 100644 --- a/tests/test_modules/good/mod_use2.catala_en +++ b/tests/test_modules/good/mod_use2.catala_en @@ -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: diff --git a/tests/test_modules/good/mod_use3.catala_en b/tests/test_modules/good/mod_use3.catala_en index b907cccd..5733c529 100644 --- a/tests/test_modules/good/mod_use3.catala_en +++ b/tests/test_modules/good/mod_use3.catala_en @@ -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: diff --git a/tests/test_modules/good/mod_use_context.catala_en b/tests/test_modules/good/mod_use_context.catala_en index 4c65031d..b916405e 100644 --- a/tests/test_modules/good/mod_use_context.catala_en +++ b/tests/test_modules/good/mod_use_context.catala_en @@ -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: diff --git a/tests/test_money/good/literal_parsing.catala_en b/tests/test_money/good/literal_parsing.catala_en index de6ebe90..0148b35e 100644 --- a/tests/test_money/good/literal_parsing.catala_en +++ b/tests/test_money/good/literal_parsing.catala_en @@ -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: diff --git a/tests/test_money/good/simple.catala_en b/tests/test_money/good/simple.catala_en index f2781785..b67fc059 100644 --- a/tests/test_money/good/simple.catala_en +++ b/tests/test_money/good/simple.catala_en @@ -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: diff --git a/tests/test_name_resolution/good/let_in.catala_en b/tests/test_name_resolution/good/let_in.catala_en index d1e68934..a600298a 100644 --- a/tests/test_name_resolution/good/let_in.catala_en +++ b/tests/test_name_resolution/good/let_in.catala_en @@ -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: diff --git a/tests/test_name_resolution/good/let_in2.catala_en b/tests/test_name_resolution/good/let_in2.catala_en index 06248a7f..081bab39 100644 --- a/tests/test_name_resolution/good/let_in2.catala_en +++ b/tests/test_name_resolution/good/let_in2.catala_en @@ -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: diff --git a/tests/test_name_resolution/good/out_of_order.catala_en b/tests/test_name_resolution/good/out_of_order.catala_en index a59e958d..ddb91c27 100644 --- a/tests/test_name_resolution/good/out_of_order.catala_en +++ b/tests/test_name_resolution/good/out_of_order.catala_en @@ -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: diff --git a/tests/test_name_resolution/good/toplevel_defs.catala_en b/tests/test_name_resolution/good/toplevel_defs.catala_en index b9034462..2e5f39f5 100644 --- a/tests/test_name_resolution/good/toplevel_defs.catala_en +++ b/tests/test_name_resolution/good/toplevel_defs.catala_en @@ -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=43, start_column=10, + end_line=43, 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=63, start_column=10, + end_line=63, 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=86, start_column=10, + end_line=86, end_column=11, law_headings=["Test inline defs in toplevel defs"])) a_2 = temp_a_17 return S4(a = a_2) diff --git a/tests/test_name_resolution/good/toplevel_defs_simple.catala_en b/tests/test_name_resolution/good/toplevel_defs_simple.catala_en index 35bf34fc..6fe152e5 100644 --- a/tests/test_name_resolution/good/toplevel_defs_simple.catala_en +++ b/tests/test_name_resolution/good/toplevel_defs_simple.catala_en @@ -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: diff --git a/tests/test_proof/good/array_length.catala_en b/tests/test_proof/good/array_length.catala_en index 55c4cb8a..bd9a775f 100644 --- a/tests/test_proof/good/array_length.catala_en +++ b/tests/test_proof/good/array_length.catala_en @@ -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. diff --git a/tests/test_proof/good/assert.catala_en b/tests/test_proof/good/assert.catala_en index 9da9d222..fc9325ed 100644 --- a/tests/test_proof/good/assert.catala_en +++ b/tests/test_proof/good/assert.catala_en @@ -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. diff --git a/tests/test_proof/good/dates_get_year.catala_en b/tests/test_proof/good/dates_get_year.catala_en index 4c2c385c..bf20bdc8 100644 --- a/tests/test_proof/good/dates_get_year.catala_en +++ b/tests/test_proof/good/dates_get_year.catala_en @@ -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. diff --git a/tests/test_proof/good/dates_simple.catala_en b/tests/test_proof/good/dates_simple.catala_en index 11b893c4..41fabb16 100644 --- a/tests/test_proof/good/dates_simple.catala_en +++ b/tests/test_proof/good/dates_simple.catala_en @@ -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. diff --git a/tests/test_proof/good/direct_scope_call.catala_en b/tests/test_proof/good/direct_scope_call.catala_en index d5bf6623..a4362032 100644 --- a/tests/test_proof/good/direct_scope_call.catala_en +++ b/tests/test_proof/good/direct_scope_call.catala_en @@ -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. diff --git a/tests/test_proof/good/direct_scope_call_with_context.catala_en b/tests/test_proof/good/direct_scope_call_with_context.catala_en index 58301249..90a8bbdb 100644 --- a/tests/test_proof/good/direct_scope_call_with_context.catala_en +++ b/tests/test_proof/good/direct_scope_call_with_context.catala_en @@ -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. diff --git a/tests/test_proof/good/duration.catala_en b/tests/test_proof/good/duration.catala_en index 01a2e840..2fe9b0b0 100644 --- a/tests/test_proof/good/duration.catala_en +++ b/tests/test_proof/good/duration.catala_en @@ -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. diff --git a/tests/test_proof/good/enums_inj.catala_en b/tests/test_proof/good/enums_inj.catala_en index 4e2c7b46..28603262 100644 --- a/tests/test_proof/good/enums_inj.catala_en +++ b/tests/test_proof/good/enums_inj.catala_en @@ -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. diff --git a/tests/test_proof/good/enums_unit.catala_en b/tests/test_proof/good/enums_unit.catala_en index d74268a2..9920e082 100644 --- a/tests/test_proof/good/enums_unit.catala_en +++ b/tests/test_proof/good/enums_unit.catala_en @@ -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. diff --git a/tests/test_proof/good/functions.catala_en b/tests/test_proof/good/functions.catala_en index c4de65b4..34ec5309 100644 --- a/tests/test_proof/good/functions.catala_en +++ b/tests/test_proof/good/functions.catala_en @@ -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. diff --git a/tests/test_proof/good/let_in_condition.catala_en b/tests/test_proof/good/let_in_condition.catala_en index a37062d6..3eb11672 100644 --- a/tests/test_proof/good/let_in_condition.catala_en +++ b/tests/test_proof/good/let_in_condition.catala_en @@ -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. diff --git a/tests/test_proof/good/money.catala_en b/tests/test_proof/good/money.catala_en index 039fb1dd..f087332d 100644 --- a/tests/test_proof/good/money.catala_en +++ b/tests/test_proof/good/money.catala_en @@ -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. diff --git a/tests/test_proof/good/no_vars.catala_en b/tests/test_proof/good/no_vars.catala_en index 93244be9..da131d57 100644 --- a/tests/test_proof/good/no_vars.catala_en +++ b/tests/test_proof/good/no_vars.catala_en @@ -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. diff --git a/tests/test_proof/good/rationals.catala_en b/tests/test_proof/good/rationals.catala_en index 11c66a40..c095f6c1 100644 --- a/tests/test_proof/good/rationals.catala_en +++ b/tests/test_proof/good/rationals.catala_en @@ -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. diff --git a/tests/test_proof/good/simple_vars.catala_en b/tests/test_proof/good/simple_vars.catala_en index 211082b1..3ac1b332 100644 --- a/tests/test_proof/good/simple_vars.catala_en +++ b/tests/test_proof/good/simple_vars.catala_en @@ -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. diff --git a/tests/test_proof/good/structs.catala_en b/tests/test_proof/good/structs.catala_en index 30ae8e7d..c915d092 100644 --- a/tests/test_proof/good/structs.catala_en +++ b/tests/test_proof/good/structs.catala_en @@ -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. diff --git a/tests/test_scope/good/191_fix_record_name_confusion.catala_en b/tests/test_scope/good/191_fix_record_name_confusion.catala_en index ddaf265f..69f76ea0 100644 --- a/tests/test_scope/good/191_fix_record_name_confusion.catala_en +++ b/tests/test_scope/good/191_fix_record_name_confusion.catala_en @@ -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 diff --git a/tests/test_scope/good/grand_parent_caller.catala_en b/tests/test_scope/good/grand_parent_caller.catala_en index 544d47d4..f0379ebd 100644 --- a/tests/test_scope/good/grand_parent_caller.catala_en +++ b/tests/test_scope/good/grand_parent_caller.catala_en @@ -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: diff --git a/tests/test_scope/good/nothing.catala_en b/tests/test_scope/good/nothing.catala_en index 5ab14826..ecfb468b 100644 --- a/tests/test_scope/good/nothing.catala_en +++ b/tests/test_scope/good/nothing.catala_en @@ -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? diff --git a/tests/test_scope/good/scope_call.catala_en b/tests/test_scope/good/scope_call.catala_en index b2c7fe0f..e12dfee5 100644 --- a/tests/test_scope/good/scope_call.catala_en +++ b/tests/test_scope/good/scope_call.catala_en @@ -20,6 +20,31 @@ scope Foo: else 0 ``` + + +```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: [0/0] +[RESULT] +Invariant Dcalc__Invariants.invariant_app_inversion + checked. result: [12/12] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_return_a_function + checked. result: [5/5] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_partial_evaluation + checked. result: [12/12] +[RESULT] +Invariant Dcalc__Invariants.invariant_default_no_arrow + checked. result: [6/6] +[RESULT] Typechecking successful! +``` + ```catala-test-inline $ catala interpret -s Foo [RESULT] Computation successful! Results: diff --git a/tests/test_scope/good/scope_call2.catala_en b/tests/test_scope/good/scope_call2.catala_en index a11868d7..f9050e41 100644 --- a/tests/test_scope/good/scope_call2.catala_en +++ b/tests/test_scope/good/scope_call2.catala_en @@ -18,6 +18,31 @@ scope Titi: definition fuzz equals output of Toto with {--bar: 111} ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[RESULT] +Invariant Dcalc__Invariants.invariant_typing_defaults + checked. result: [94/94] +[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: [7/7] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_partial_evaluation + checked. result: [9/9] +[RESULT] +Invariant Dcalc__Invariants.invariant_default_no_arrow + checked. result: [11/11] +[RESULT] Typechecking successful! +``` + ```catala-test-inline $ catala Interpret -s Titi [RESULT] Computation successful! Results: diff --git a/tests/test_scope/good/scope_call3.catala_en b/tests/test_scope/good/scope_call3.catala_en index b2c8b69e..19614eea 100644 --- a/tests/test_scope/good/scope_call3.catala_en +++ b/tests/test_scope/good/scope_call3.catala_en @@ -16,6 +16,31 @@ scope RentComputation: definition f of x equals g of (x + 1) ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[RESULT] +Invariant Dcalc__Invariants.invariant_typing_defaults + checked. result: [69/69] +[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: [6/6] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_partial_evaluation + checked. result: [9/9] +[RESULT] +Invariant Dcalc__Invariants.invariant_default_no_arrow + checked. result: [8/8] +[RESULT] Typechecking successful! +``` + ```catala-test-inline $ catala Interpret -t -s HousingComputation --debug [DEBUG] = INIT = diff --git a/tests/test_scope/good/scope_call4.catala_en b/tests/test_scope/good/scope_call4.catala_en index c9e5ba3f..243bd29f 100644 --- a/tests/test_scope/good/scope_call4.catala_en +++ b/tests/test_scope/good/scope_call4.catala_en @@ -22,6 +22,31 @@ scope RentComputation: ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[RESULT] +Invariant Dcalc__Invariants.invariant_typing_defaults + checked. result: [129/129] +[RESULT] +Invariant Dcalc__Invariants.invariant_match_inversion + checked. result: [0/0] +[RESULT] +Invariant Dcalc__Invariants.invariant_app_inversion + checked. result: [19/19] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_return_a_function + checked. result: [13/13] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_partial_evaluation + checked. result: [19/19] +[RESULT] +Invariant Dcalc__Invariants.invariant_default_no_arrow + checked. result: [13/13] +[RESULT] Typechecking successful! +``` + ```catala-test-inline $ catala Interpret -s RentComputation --debug [DEBUG] = INIT = diff --git a/tests/test_scope/good/simple.catala_en b/tests/test_scope/good/simple.catala_en index 36d88281..250567bd 100644 --- a/tests/test_scope/good/simple.catala_en +++ b/tests/test_scope/good/simple.catala_en @@ -8,6 +8,31 @@ scope Foo: definition bar equals 0 ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[RESULT] +Invariant Dcalc__Invariants.invariant_typing_defaults + checked. result: [10/10] +[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 Lcalc -s Foo let scope Foo (Foo_in: Foo_in): Foo {bar: integer} = diff --git a/tests/test_scope/good/sub_scope.catala_en b/tests/test_scope/good/sub_scope.catala_en index 95b27d87..cdede37d 100644 --- a/tests/test_scope/good/sub_scope.catala_en +++ b/tests/test_scope/good/sub_scope.catala_en @@ -23,6 +23,31 @@ scope B: definition scopeA.a under condition a > 0 consequence equals scopeAbis.a_base ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[RESULT] +Invariant Dcalc__Invariants.invariant_typing_defaults + checked. result: [140/140] +[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: [6/6] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_partial_evaluation + checked. result: [9/9] +[RESULT] +Invariant Dcalc__Invariants.invariant_default_no_arrow + checked. result: [17/17] +[RESULT] Typechecking successful! +``` + ```catala-test-inline $ catala Interpret -s A [RESULT] Computation successful! Results: diff --git a/tests/test_scope/good/sub_sub_scope.catala_en b/tests/test_scope/good/sub_sub_scope.catala_en index 2e37380a..83e58860 100644 --- a/tests/test_scope/good/sub_sub_scope.catala_en +++ b/tests/test_scope/good/sub_sub_scope.catala_en @@ -30,6 +30,31 @@ scope C: definition z equals 2 ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[RESULT] +Invariant Dcalc__Invariants.invariant_typing_defaults + checked. result: [153/153] +[RESULT] +Invariant Dcalc__Invariants.invariant_match_inversion + checked. result: [0/0] +[RESULT] +Invariant Dcalc__Invariants.invariant_app_inversion + checked. result: [11/11] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_return_a_function + checked. result: [7/7] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_partial_evaluation + checked. result: [11/11] +[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: diff --git a/tests/test_scope/good/subscope_function_arg_not_defined.catala_en b/tests/test_scope/good/subscope_function_arg_not_defined.catala_en index a62973f2..cca93d55 100644 --- a/tests/test_scope/good/subscope_function_arg_not_defined.catala_en +++ b/tests/test_scope/good/subscope_function_arg_not_defined.catala_en @@ -17,6 +17,31 @@ scope Caller: definition y equals sub.output_v ``` + + +```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: [6/6] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_return_a_function + checked. result: [3/3] +[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 Caller [RESULT] Computation successful! Results: diff --git a/tests/test_scope/good/subscope_function_arg_not_defined2.catala_en b/tests/test_scope/good/subscope_function_arg_not_defined2.catala_en index cba7a310..95357a68 100644 --- a/tests/test_scope/good/subscope_function_arg_not_defined2.catala_en +++ b/tests/test_scope/good/subscope_function_arg_not_defined2.catala_en @@ -19,6 +19,31 @@ scope Caller: assertion callee.output_v ``` + + +```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: [6/6] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_return_a_function + checked. result: [4/4] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_partial_evaluation + checked. result: [6/6] +[RESULT] +Invariant Dcalc__Invariants.invariant_default_no_arrow + checked. result: [16/16] +[RESULT] Typechecking successful! +``` + ```catala-test-inline $ catala Interpret -s Caller [RESULT] Computation successful! diff --git a/tests/test_struct/good/nested3.catala_en b/tests/test_struct/good/nested3.catala_en index 5a506672..289ce7f7 100644 --- a/tests/test_struct/good/nested3.catala_en +++ b/tests/test_struct/good/nested3.catala_en @@ -34,6 +34,31 @@ scope B: definition out equals if t.a.y then t.a.x else (if t.b.y then t.b.x else 42) ``` + + +```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: [4/4] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_return_a_function + checked. result: [1/1] +[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: diff --git a/tests/test_struct/good/simple.catala_en b/tests/test_struct/good/simple.catala_en index d57c9d9d..98239b6b 100644 --- a/tests/test_struct/good/simple.catala_en +++ b/tests/test_struct/good/simple.catala_en @@ -17,6 +17,31 @@ scope A: definition z equals s.x + s.y ``` + + +```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: [0/0] +[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 Interpret -s A [RESULT] Computation successful! Results: diff --git a/tests/test_typing/good/overload.catala_en b/tests/test_typing/good/overload.catala_en index 37582b4c..819e6a28 100644 --- a/tests/test_typing/good/overload.catala_en +++ b/tests/test_typing/good/overload.catala_en @@ -57,6 +57,31 @@ scope S: ) ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[RESULT] +Invariant Dcalc__Invariants.invariant_typing_defaults + checked. result: [581/581] +[RESULT] +Invariant Dcalc__Invariants.invariant_match_inversion + checked. result: [0/0] +[RESULT] +Invariant Dcalc__Invariants.invariant_app_inversion + checked. result: [148/148] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_return_a_function + checked. result: [0/0] +[RESULT] +Invariant Dcalc__Invariants.invariant_no_partial_evaluation + checked. result: [148/148] +[RESULT] +Invariant Dcalc__Invariants.invariant_default_no_arrow + checked. result: [32/32] +[RESULT] Typechecking successful! +``` + ```catala-test-inline $ catala Interpret -s S [RESULT] Computation successful! Results: diff --git a/tests/test_variable_state/good/simple.catala_en b/tests/test_variable_state/good/simple.catala_en index ad254b9a..a052374d 100644 --- a/tests/test_variable_state/good/simple.catala_en +++ b/tests/test_variable_state/good/simple.catala_en @@ -15,6 +15,31 @@ scope A: definition foo state fizz equals foo + 1 ``` + + +```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: [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 A [RESULT] Computation successful! Results: diff --git a/tests/test_variable_state/good/subscope.catala_en b/tests/test_variable_state/good/subscope.catala_en index ec7cf764..f625b3d5 100644 --- a/tests/test_variable_state/good/subscope.catala_en +++ b/tests/test_variable_state/good/subscope.catala_en @@ -30,6 +30,31 @@ scope B: definition foofoofoo equals b.foo ``` + + +```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: [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: [15/15] +[RESULT] Typechecking successful! +``` + ```catala-test-inline $ catala Scopelang -s A let scope A (foo_bar: ⟨integer⟩|context) (foo_baz: integer|internal) From d7327e53c09936c368f32285a3df2dabe8f279ab Mon Sep 17 00:00:00 2001 From: adelaett <90894311+adelaett@users.noreply.github.com> Date: Tue, 5 Dec 2023 16:56:59 +0100 Subject: [PATCH 6/9] /!\ problematic tests --- .../good/mutliple_definitions.catala_en | 36 ++++++++++++ .../good/double_definition.catala_en | 38 +++++++++++++ tests/test_func/good/context_func.catala_en | 29 ++++++++++ tests/test_proof/good/enums-arith.catala_en | 32 +++++++++++ tests/test_proof/good/enums-nonbool.catala_en | 32 +++++++++++ tests/test_proof/good/enums.catala_en | 32 +++++++++++ .../good/ambiguous_fields.catala_en | 32 +++++++++++ .../good/same_name_fields.catala_en | 32 +++++++++++ tests/test_typing/good/common.catala_en | 55 +++++++++++++++++++ 9 files changed, 318 insertions(+) diff --git a/tests/test_default/good/mutliple_definitions.catala_en b/tests/test_default/good/mutliple_definitions.catala_en index 23da3b31..c059d778 100644 --- a/tests/test_default/good/mutliple_definitions.catala_en +++ b/tests/test_default/good/mutliple_definitions.catala_en @@ -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? diff --git a/tests/test_exception/good/double_definition.catala_en b/tests/test_exception/good/double_definition.catala_en index e9203bc5..bf8bf779 100644 --- a/tests/test_exception/good/double_definition.catala_en +++ b/tests/test_exception/good/double_definition.catala_en @@ -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? diff --git a/tests/test_func/good/context_func.catala_en b/tests/test_func/good/context_func.catala_en index 467b95b5..7e3b5f3d 100644 --- a/tests/test_func/good/context_func.catala_en +++ b/tests/test_func/good/context_func.catala_en @@ -15,6 +15,35 @@ scope B: definition a.f of x under condition b and x > 0 consequence equals x - 1 ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[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# +``` + ```catala-test-inline $ catala Scopelang -s B [ERROR] diff --git a/tests/test_proof/good/enums-arith.catala_en b/tests/test_proof/good/enums-arith.catala_en index 4fe972ee..e8270e60 100644 --- a/tests/test_proof/good/enums-arith.catala_en +++ b/tests/test_proof/good/enums-arith.catala_en @@ -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? diff --git a/tests/test_proof/good/enums-nonbool.catala_en b/tests/test_proof/good/enums-nonbool.catala_en index 227d7d4e..4b7fea61 100644 --- a/tests/test_proof/good/enums-nonbool.catala_en +++ b/tests/test_proof/good/enums-nonbool.catala_en @@ -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? diff --git a/tests/test_proof/good/enums.catala_en b/tests/test_proof/good/enums.catala_en index dbd08291..b9be652c 100644 --- a/tests/test_proof/good/enums.catala_en +++ b/tests/test_proof/good/enums.catala_en @@ -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? diff --git a/tests/test_struct/good/ambiguous_fields.catala_en b/tests/test_struct/good/ambiguous_fields.catala_en index 6254803e..5208690e 100644 --- a/tests/test_struct/good/ambiguous_fields.catala_en +++ b/tests/test_struct/good/ambiguous_fields.catala_en @@ -16,6 +16,38 @@ scope A: definition y equals x.f ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[WARNING] The structure "Bar" is never used; maybe it's unnecessary? + +┌─⯈ tests/test_struct/good/ambiguous_fields.catala_en:7.23-7.26: +└─┐ +7 │ declaration structure Bar: + │ ‾‾‾ + └─ Article +[RESULT] +Invariant Dcalc__Invariants.invariant_typing_defaults + checked. result: [20/20] +[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: [4/4] +[RESULT] Typechecking successful! +``` + ```catala-test-inline $ catala Interpret -s A [WARNING] The structure "Bar" is never used; maybe it's unnecessary? diff --git a/tests/test_struct/good/same_name_fields.catala_en b/tests/test_struct/good/same_name_fields.catala_en index 95822f97..4f263f85 100644 --- a/tests/test_struct/good/same_name_fields.catala_en +++ b/tests/test_struct/good/same_name_fields.catala_en @@ -16,6 +16,38 @@ scope A: definition y equals x.Foo.f ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[WARNING] The structure "Bar" is never used; maybe it's unnecessary? + +┌─⯈ tests/test_struct/good/same_name_fields.catala_en:7.23-7.26: +└─┐ +7 │ declaration structure Bar: + │ ‾‾‾ + └─ Article +[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: [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 A [WARNING] The structure "Bar" is never used; maybe it's unnecessary? diff --git a/tests/test_typing/good/common.catala_en b/tests/test_typing/good/common.catala_en index b2f764d1..180c255d 100644 --- a/tests/test_typing/good/common.catala_en +++ b/tests/test_typing/good/common.catala_en @@ -15,6 +15,61 @@ declaration scope S: output a content decimal ``` + + +```catala-test-inline +$ catala Typecheck --check_invariants +[WARNING] In scope "S", the variable "z" is declared but never defined; did you forget something? + +┌─⯈ tests/test_typing/good/common.catala_en:14.10-14.11: +└──┐ +14 │ output z content collection Structure + │ ‾ +[WARNING] In scope "S", the variable "a" is declared but never defined; did you forget something? + +┌─⯈ tests/test_typing/good/common.catala_en:15.10-15.11: +└──┐ +15 │ output a content decimal + │ ‾ +[WARNING] This variable is dead code; it does not contribute to computing any of scope "S" outputs. Did you forget something? + +┌─⯈ tests/test_typing/good/common.catala_en:12.9-12.10: +└──┐ +12 │ input x content integer + │ ‾ +[WARNING] The structure "Structure" is never used; maybe it's unnecessary? + +┌─⯈ tests/test_typing/good/common.catala_en:7.23-7.32: +└─┐ +7 │ declaration structure Structure: + │ ‾‾‾‾‾‾‾‾‾ +[WARNING] The enumeration "Enum" is never used; maybe it's unnecessary? + +┌─⯈ tests/test_typing/good/common.catala_en:2.25-2.29: +└─┐ +2 │ declaration enumeration Enum: + │ ‾‾‾‾ +[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: [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 Typecheck --disable_warning [RESULT] Typechecking successful! From f63c3d3fc336edce6cdedd64cd9a46044adfa76c Mon Sep 17 00:00:00 2001 From: adelaett <90894311+adelaett@users.noreply.github.com> Date: Wed, 6 Dec 2023 14:46:36 +0100 Subject: [PATCH 7/9] fix error in a test --- tests/test_func/good/context_func.catala_en | 137 ++++++------------ .../good/toplevel_defs.catala_en | 12 +- 2 files changed, 50 insertions(+), 99 deletions(-) diff --git a/tests/test_func/good/context_func.catala_en b/tests/test_func/good/context_func.catala_en index 7e3b5f3d..ecd6c832 100644 --- a/tests/test_func/good/context_func.catala_en +++ b/tests/test_func/good/context_func.catala_en @@ -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 @@ -19,108 +19,59 @@ scope B: ```catala-test-inline $ catala Typecheck --check_invariants -[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# +[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} ``` diff --git a/tests/test_name_resolution/good/toplevel_defs.catala_en b/tests/test_name_resolution/good/toplevel_defs.catala_en index 2e5f39f5..794a7cfc 100644 --- a/tests/test_name_resolution/good/toplevel_defs.catala_en +++ b/tests/test_name_resolution/good/toplevel_defs.catala_en @@ -464,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=43, start_column=10, - end_line=43, 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) @@ -493,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=63, start_column=10, - end_line=63, 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) @@ -520,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=86, start_column=10, - end_line=86, 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) From 9f4a238a4a313978b795810a3e45b3698a736c61 Mon Sep 17 00:00:00 2001 From: adelaett <90894311+adelaett@users.noreply.github.com> Date: Thu, 7 Dec 2023 13:44:50 +0100 Subject: [PATCH 8/9] Fix error messages for unexpected types. do not retype the terms in the cases where checking invariant is not mandatory. --- compiler/dcalc/invariants.ml | 17 ++++++----------- compiler/driver.ml | 7 ++++--- 2 files changed, 10 insertions(+), 14 deletions(-) diff --git a/compiler/dcalc/invariants.ml b/compiler/dcalc/invariants.ml index d02b5fea..2314afa7 100644 --- a/compiler/dcalc/invariants.ml +++ b/compiler/dcalc/invariants.ml @@ -162,18 +162,13 @@ let rec check_typ_no_default ctx ty = | TArray ty -> check_typ_no_default ctx ty | TDefault _t -> false | TAny -> - (* found TAny *) - Message.emit_warning - "Internal error: the type was not fully resolved, it is not possible to \ - verify whenever the typing_default invariant holds."; - true + Message.raise_internal_error + "Some Dcalc invariants are invalid: TAny was found wheras it the term \ + was supposed to be well typed." | TClosureEnv -> - Message.emit_warning - "Internal error: In the compilation process, the default invariant for \ - typing was not checked early enough. Since it's impossible to verify \ - this invariant at any point due to the closure environment holding an \ - existential type."; - true (* we should not check this one. *) + Message.raise_internal_error + "Some Dcalc invariants are invalid: TClosureEnv was found wheras it \ + should only appear later in the compilation process." let check_type_thunked_or_nodefault ctx ty = check_typ_no_default ctx ty diff --git a/compiler/driver.ml b/compiler/driver.ml index df6b3e75..51a1fc73 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -542,11 +542,12 @@ module Commands = struct 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 = - Shared_ast.Typing.program ~leave_unresolved:false (Program.untype 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 From b5e7b297aaa622a341ed163d20586aa7c9b62c4b Mon Sep 17 00:00:00 2001 From: adelaett <90894311+adelaett@users.noreply.github.com> Date: Thu, 7 Dec 2023 13:48:46 +0100 Subject: [PATCH 9/9] typo fixing --- compiler/dcalc/invariants.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/compiler/dcalc/invariants.ml b/compiler/dcalc/invariants.ml index 2314afa7..36e82d66 100644 --- a/compiler/dcalc/invariants.ml +++ b/compiler/dcalc/invariants.ml @@ -163,11 +163,11 @@ let rec check_typ_no_default ctx ty = | TDefault _t -> false | TAny -> Message.raise_internal_error - "Some Dcalc invariants are invalid: TAny was found wheras it the term \ - was supposed to be well typed." + "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 wheras it \ + "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 =