Register the option type in ctx when used in lcalc

This commit is contained in:
Louis Gesbert 2023-12-18 14:21:46 +01:00
parent a1c1a7756f
commit a2efc94fd2
26 changed files with 222 additions and 410 deletions

View File

@ -237,14 +237,14 @@ module Passes = struct
"Option --avoid-exceptions is not compatible with option --trace"
| true, _, Untyped _ ->
Program.untype
(Lcalc.Compile_without_exceptions.translate_program
(Lcalc.From_dcalc.translate_program_without_exceptions
(Shared_ast.Typing.program ~leave_unresolved:false prg))
| true, _, Typed _ ->
Lcalc.Compile_without_exceptions.translate_program prg
Lcalc.From_dcalc.translate_program_without_exceptions prg
| false, _, Typed _ ->
Program.untype (Lcalc.Compile_with_exceptions.translate_program prg)
Program.untype (Lcalc.From_dcalc.translate_program_with_exceptions prg)
| false, _, Untyped _ ->
Lcalc.Compile_with_exceptions.translate_program prg
Lcalc.From_dcalc.translate_program_with_exceptions prg
| _, _, Custom _ -> invalid_arg "Driver.Passes.lcalc"
in
let prg =

View File

@ -14,8 +14,21 @@
License for the specific language governing permissions and limitations under
the License. *)
open Shared_ast
let add_option_type ctx =
{
ctx with
ctx_enums =
EnumName.Map.add Expr.option_enum Expr.option_enum_config ctx.ctx_enums;
}
let add_option_type_program prg =
{ prg with decl_ctx = add_option_type prg.decl_ctx }
let translate_program_with_exceptions =
Compile_with_exceptions.translate_program
let translate_program_without_exceptions =
Compile_without_exceptions.translate_program
let translate_program_without_exceptions prg =
let prg = add_option_type_program prg in
Compile_without_exceptions.translate_program prg

View File

@ -14,12 +14,14 @@
License for the specific language governing permissions and limitations under
the License. *)
open Shared_ast
val translate_program_with_exceptions : 'm Dcalc.Ast.program -> 'm Ast.program
(** Translation from the default calculus to the lambda calculus. This
translation uses exceptions to handle empty default terms. *)
val translate_program_without_exceptions :
Shared_ast.typed Dcalc.Ast.program -> Shared_ast.untyped Ast.program
typed Dcalc.Ast.program -> untyped Ast.program
(** Translation from the default calculus to the lambda calculus. This
translation uses an option monad to handle empty defaults terms. This
transformation is one piece to permit to compile toward legacy languages

View File

@ -262,8 +262,8 @@ let none_constr = EnumConstructor.fresh ("ENone", Pos.no_pos)
let some_constr = EnumConstructor.fresh ("ESome", Pos.no_pos)
let option_enum_config =
EnumConstructor.Map.singleton none_constr (TLit TUnit, Pos.no_pos)
|> EnumConstructor.Map.add some_constr (TAny, Pos.no_pos)
EnumConstructor.Map.of_list
[none_constr, (TLit TUnit, Pos.no_pos); some_constr, (TAny, Pos.no_pos)]
(* - Traversal functions - *)

View File

@ -26,7 +26,7 @@ $ catala Typecheck --check-invariants
```catala-test-inline
$ catala Lcalc --avoid-exceptions -O --closure-conversion
type Eoption = | ENone of unit | ESome of any
type S_in = { x_in: bool; }

View File

@ -24,7 +24,7 @@ $ catala Typecheck --check-invariants
```catala-test-inline
$ catala Lcalc --avoid-exceptions -O --closure-conversion
type Eoption = | ENone of unit | ESome of any
type S_in = { x_in: bool; }

View File

@ -21,24 +21,12 @@ scope A:
```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] Invariant typing_defaults checked. result: [68/68]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [2/2]
[RESULT] Invariant no_return_a_function checked. result: [0/0]
[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
[RESULT] Invariant default_no_arrow checked. result: [10/10]
[RESULT] Typechecking successful!
```

View File

@ -18,24 +18,12 @@ scope B:
```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] Invariant typing_defaults checked. result: [34/34]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [1/1]
[RESULT] Invariant no_return_a_function checked. result: [0/0]
[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
[RESULT] Invariant default_no_arrow checked. result: [4/4]
[RESULT] Typechecking successful!
```

View File

@ -24,24 +24,12 @@ scope B:
```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] Invariant typing_defaults checked. result: [63/63]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [2/2]
[RESULT] Invariant no_return_a_function checked. result: [1/1]
[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
[RESULT] Invariant default_no_arrow checked. result: [9/9]
[RESULT] Typechecking successful!
```

View File

@ -31,24 +31,12 @@ 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] Invariant typing_defaults checked. result: [19/19]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [1/1]
[RESULT] Invariant no_return_a_function checked. result: [0/0]
[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
[RESULT] Invariant default_no_arrow checked. result: [3/3]
[RESULT] Typechecking successful!
```

View File

@ -31,24 +31,12 @@ 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] Invariant typing_defaults checked. result: [19/19]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [1/1]
[RESULT] Invariant no_return_a_function checked. result: [0/0]
[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
[RESULT] Invariant default_no_arrow checked. result: [3/3]
[RESULT] Typechecking successful!
```

View File

@ -32,24 +32,12 @@ scope S2:
```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] Invariant typing_defaults checked. result: [40/40]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [2/2]
[RESULT] Invariant no_return_a_function checked. result: [0/0]
[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
[RESULT] Invariant default_no_arrow checked. result: [6/6]
[RESULT] Typechecking successful!
```

View File

@ -31,24 +31,12 @@ scope S:
```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] Invariant typing_defaults checked. result: [24/24]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [0/0]
[RESULT] Invariant no_return_a_function checked. result: [1/1]
[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
[RESULT] Invariant default_no_arrow checked. result: [4/4]
[RESULT] Typechecking successful!
```

View File

@ -60,24 +60,12 @@ scope Stest:
```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] Invariant typing_defaults checked. result: [207/207]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [18/18]
[RESULT] Invariant no_return_a_function checked. result: [17/17]
[RESULT] Invariant no_partial_evaluation checked. result: [18/18]
[RESULT] Invariant default_no_arrow checked. result: [22/22]
[RESULT] Typechecking successful!
```

View File

@ -21,24 +21,12 @@ scope S:
```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] Invariant typing_defaults checked. result: [65/65]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [4/4]
[RESULT] Invariant no_return_a_function checked. result: [2/2]
[RESULT] Invariant no_partial_evaluation checked. result: [4/4]
[RESULT] Invariant default_no_arrow checked. result: [7/7]
[RESULT] Typechecking successful!
```

View File

@ -27,24 +27,12 @@ scope T2:
```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] Invariant typing_defaults checked. result: [74/74]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [2/2]
[RESULT] Invariant no_return_a_function checked. result: [0/0]
[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
[RESULT] Invariant default_no_arrow checked. result: [8/8]
[RESULT] Typechecking successful!
```

View File

@ -19,24 +19,12 @@ scope T:
```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] Invariant typing_defaults checked. result: [49/49]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [1/1]
[RESULT] Invariant no_return_a_function checked. result: [1/1]
[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
[RESULT] Invariant default_no_arrow checked. result: [8/8]
[RESULT] Typechecking successful!
```

View File

@ -23,24 +23,12 @@ scope T:
```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] Invariant typing_defaults checked. result: [49/49]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [1/1]
[RESULT] Invariant no_return_a_function checked. result: [1/1]
[RESULT] Invariant no_partial_evaluation checked. result: [1/1]
[RESULT] Invariant default_no_arrow checked. result: [8/8]
[RESULT] Typechecking successful!
```

View File

@ -44,24 +44,12 @@ scope TestCall:
```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] Invariant typing_defaults checked. result: [146/146]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [15/15]
[RESULT] Invariant no_return_a_function checked. result: [16/16]
[RESULT] Invariant no_partial_evaluation checked. result: [15/15]
[RESULT] Invariant default_no_arrow checked. result: [13/13]
[RESULT] Typechecking successful!
```

View File

@ -30,12 +30,15 @@ let s (s_in: S_in.t) : S.t =
let sr_: money =
try
(handle_default
{filename = ""; start_line=0; start_column=1;
end_line=0; end_column=1; law_headings=[]}
{filename = "tests/test_modules/good/mod_def.catala_en";
start_line=16; start_column=10; end_line=16; end_column=12;
law_headings=["Test modules + inclusions 1"]}
([|(fun (_: unit) ->
handle_default
{filename = ""; start_line=0; start_column=1;
end_line=0; end_column=1; law_headings=[]} ([||])
{filename = "tests/test_modules/good/mod_def.catala_en";
start_line=16; start_column=10;
end_line=16; end_column=12;
law_headings=["Test modules + inclusions 1"]} ([||])
(fun (_: unit) -> true)
(fun (_: unit) -> money_of_cents_string "100000"))|])
(fun (_: unit) -> false) (fun (_: unit) -> raise EmptyError))
@ -47,12 +50,15 @@ let s (s_in: S_in.t) : S.t =
let e1_: Enum1.t =
try
(handle_default
{filename = ""; start_line=0; start_column=1;
end_line=0; end_column=1; law_headings=[]}
{filename = "tests/test_modules/good/mod_def.catala_en";
start_line=17; start_column=10; end_line=17; end_column=12;
law_headings=["Test modules + inclusions 1"]}
([|(fun (_: unit) ->
handle_default
{filename = ""; start_line=0; start_column=1;
end_line=0; end_column=1; law_headings=[]} ([||])
{filename = "tests/test_modules/good/mod_def.catala_en";
start_line=17; start_column=10;
end_line=17; end_column=12;
law_headings=["Test modules + inclusions 1"]} ([||])
(fun (_: unit) -> true) (fun (_: unit) -> Enum1.Maybe ()))|])
(fun (_: unit) -> false) (fun (_: unit) -> raise EmptyError))
with

View File

@ -15,24 +15,12 @@ scope A:
```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] Invariant typing_defaults checked. result: [25/25]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [0/0]
[RESULT] Invariant no_return_a_function checked. result: [0/0]
[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
[RESULT] Invariant default_no_arrow checked. result: [4/4]
[RESULT] Typechecking successful!
```

View File

@ -16,24 +16,12 @@ scope A:
```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] Invariant typing_defaults checked. result: [61/61]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [3/3]
[RESULT] Invariant no_return_a_function checked. result: [0/0]
[RESULT] Invariant no_partial_evaluation checked. result: [3/3]
[RESULT] Invariant default_no_arrow checked. result: [9/9]
[RESULT] Typechecking successful!
```

View File

@ -29,24 +29,12 @@ scope S:
```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] Invariant typing_defaults checked. result: [62/62]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [5/5]
[RESULT] Invariant no_return_a_function checked. result: [3/3]
[RESULT] Invariant no_partial_evaluation checked. result: [5/5]
[RESULT] Invariant default_no_arrow checked. result: [6/6]
[RESULT] Typechecking successful!
```

View File

@ -17,24 +17,12 @@ scope S:
```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] Invariant typing_defaults checked. result: [27/27]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [3/3]
[RESULT] Invariant no_return_a_function checked. result: [2/2]
[RESULT] Invariant no_partial_evaluation checked. result: [3/3]
[RESULT] Invariant default_no_arrow checked. result: [3/3]
[RESULT] Typechecking successful!
```
@ -75,19 +63,23 @@ let s (s_in: S_in.t) : S.t =
let a_: bool =
try
(handle_default
{filename = ""; start_line=0; start_column=1;
end_line=0; end_column=1; law_headings=[]}
([|(fun (_: unit) -> a_ ())|]) (fun (_: unit) -> true)
{filename = "tests/test_name_resolution/good/let_in2.catala_en";
start_line=7; start_column=18; end_line=7; end_column=19;
law_headings=["Article"]} ([|(fun (_: unit) -> a_ ())|])
(fun (_: unit) -> true)
(fun (_: unit) ->
try
(handle_default
{filename = ""; start_line=0; start_column=1;
end_line=0; end_column=1; law_headings=[]}
{filename = "tests/test_name_resolution/good/let_in2.catala_en";
start_line=7; start_column=18; end_line=7; end_column=19;
law_headings=["Article"]}
([|(fun (_: unit) ->
handle_default
{filename = ""; start_line=0; start_column=1;
end_line=0; end_column=1; law_headings=[]} (
[||]) (fun (_: unit) -> true)
{filename = "tests/test_name_resolution/good/let_in2.catala_en";
start_line=7; start_column=18;
end_line=7; end_column=19;
law_headings=["Article"]} ([||])
(fun (_: unit) -> true)
(fun (_: unit) -> (let a_ : bool = false
in
(let a_ : bool = (o_or a_ true) in

View File

@ -22,24 +22,12 @@ scope S:
```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] Invariant typing_defaults checked. result: [41/41]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [2/2]
[RESULT] Invariant no_return_a_function checked. result: [0/0]
[RESULT] Invariant no_partial_evaluation checked. result: [2/2]
[RESULT] Invariant default_no_arrow checked. result: [6/6]
[RESULT] Typechecking successful!
```

View File

@ -23,24 +23,12 @@ scope S:
```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] Invariant typing_defaults checked. result: [29/29]
[RESULT] Invariant match_inversion checked. result: [0/0]
[RESULT] Invariant app_inversion checked. result: [0/0]
[RESULT] Invariant no_return_a_function checked. result: [0/0]
[RESULT] Invariant no_partial_evaluation checked. result: [0/0]
[RESULT] Invariant default_no_arrow checked. result: [4/4]
[RESULT] Typechecking successful!
```
@ -454,18 +442,21 @@ def s2(s2_in:S2In):
decimal_of_string("100."))
def temp_a_4(_:Unit):
return True
return handle_default(SourcePosition(filename="", start_line=0,
start_column=1, end_line=0, end_column=1,
law_headings=[]), [], temp_a_4, temp_a_3)
temp_a_5 = handle_default(SourcePosition(filename="", start_line=0,
start_column=1, end_line=0, end_column=1,
law_headings=[]), [temp_a_2], temp_a_1,
temp_a)
return handle_default(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=50, start_column=10,
end_line=50, end_column=11,
law_headings=["Test toplevel function defs"]), [],
temp_a_4, temp_a_3)
temp_a_5 = handle_default(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=50, start_column=10,
end_line=50, end_column=11,
law_headings=["Test toplevel function defs"]), [temp_a_2],
temp_a_1, temp_a)
except EmptyError:
temp_a_5 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=62, start_column=10,
end_line=62, end_column=11,
start_line=50, start_column=10,
end_line=50, end_column=11,
law_headings=["Test toplevel function defs"]))
a = temp_a_5
return S2(a = a)
@ -483,18 +474,21 @@ def s3(s3_in:S3In):
decimal_of_string("55.")))
def temp_a_10(_:Unit):
return True
return handle_default(SourcePosition(filename="", start_line=0,
start_column=1, end_line=0, end_column=1,
law_headings=[]), [], temp_a_10, temp_a_9)
temp_a_11 = handle_default(SourcePosition(filename="", start_line=0,
start_column=1, end_line=0, end_column=1,
law_headings=[]), [temp_a_8], temp_a_7,
temp_a_6)
return handle_default(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=70, start_column=10,
end_line=70, end_column=11,
law_headings=["Test function def with two args"]), [],
temp_a_10, temp_a_9)
temp_a_11 = handle_default(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=70, start_column=10,
end_line=70, end_column=11,
law_headings=["Test function def with two args"]), [temp_a_8],
temp_a_7, temp_a_6)
except EmptyError:
temp_a_11 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=82, start_column=10,
end_line=82, end_column=11,
start_line=70, start_column=10,
end_line=70, end_column=11,
law_headings=["Test function def with two args"]))
a_1 = temp_a_11
return S3(a = a_1)
@ -510,18 +504,21 @@ def s4(s4_in:S4In):
return (glob5_1 + decimal_of_string("1."))
def temp_a_16(_:Unit):
return True
return handle_default(SourcePosition(filename="", start_line=0,
start_column=1, end_line=0, end_column=1,
law_headings=[]), [], temp_a_16, temp_a_15)
temp_a_17 = handle_default(SourcePosition(filename="", start_line=0,
start_column=1, end_line=0, end_column=1,
law_headings=[]), [temp_a_14], temp_a_13,
temp_a_12)
return handle_default(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=93, start_column=10,
end_line=93, end_column=11,
law_headings=["Test inline defs in toplevel defs"]), [],
temp_a_16, temp_a_15)
temp_a_17 = handle_default(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=93, start_column=10,
end_line=93, end_column=11,
law_headings=["Test inline defs in toplevel defs"]), [temp_a_14],
temp_a_13, temp_a_12)
except EmptyError:
temp_a_17 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=105, start_column=10,
end_line=105, end_column=11,
start_line=93, start_column=10,
end_line=93, end_column=11,
law_headings=["Test inline defs in toplevel defs"]))
a_2 = temp_a_17
return S4(a = a_2)
@ -537,13 +534,16 @@ def s(s_in:SIn):
return (glob1 * glob1)
def temp_a_22(_:Unit):
return True
return handle_default(SourcePosition(filename="", start_line=0,
start_column=1, end_line=0, end_column=1,
law_headings=[]), [], temp_a_22, temp_a_21)
temp_a_23 = handle_default(SourcePosition(filename="", start_line=0,
start_column=1, end_line=0, end_column=1,
law_headings=[]), [temp_a_20], temp_a_19,
temp_a_18)
return handle_default(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=7, start_column=10,
end_line=7, end_column=11,
law_headings=["Test basic toplevel values defs"]), [],
temp_a_22, temp_a_21)
temp_a_23 = handle_default(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=7, start_column=10,
end_line=7, end_column=11,
law_headings=["Test basic toplevel values defs"]), [temp_a_20],
temp_a_19, temp_a_18)
except EmptyError:
temp_a_23 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
@ -561,13 +561,16 @@ def s(s_in:SIn):
return glob2
def temp_b_4(_:Unit):
return True
return handle_default(SourcePosition(filename="", start_line=0,
start_column=1, end_line=0, end_column=1,
law_headings=[]), [], temp_b_4, temp_b_3)
temp_b_5 = handle_default(SourcePosition(filename="", start_line=0,
start_column=1, end_line=0, end_column=1,
law_headings=[]), [temp_b_2], temp_b_1,
temp_b)
return handle_default(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=8, start_column=10,
end_line=8, end_column=11,
law_headings=["Test basic toplevel values defs"]), [],
temp_b_4, temp_b_3)
temp_b_5 = handle_default(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",
start_line=8, start_column=10,
end_line=8, end_column=11,
law_headings=["Test basic toplevel values defs"]), [temp_b_2],
temp_b_1, temp_b)
except EmptyError:
temp_b_5 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en",