CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Update tests

Browse Source
This commit is contained in:
Denis Merigoux 2023-06-03 18:02:57 +02:00
parent ddee094783
commit 09bcefbcc1
65 changed files with 402 additions and 920 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

58
compiler/desugared/linting.ml
View File

@ -255,8 +255,66 @@ let detect_unused_enum_constructors (p : program) : unit =
constructors)
p.program_ctx.ctx_enums
(* Reachability in a graph can be implemented as a simple fixpoint analysis with
backwards propagation. *)
module Reachability =
Graph.Fixpoint.Make
(Dependency.ScopeDependencies)
(struct
type vertex = Dependency.ScopeDependencies.vertex
type edge = Dependency.ScopeDependencies.E.t
type g = Dependency.ScopeDependencies.t
type data = bool
let direction = Graph.Fixpoint.Backward
let equal = ( = )
let join = ( || )
let analyze _ x = x
end)
let detect_dead_code (p : program) : unit =
(* Dead code detection for scope variables based on an intra-scope dependency
analysis. *)
ScopeName.Map.iter
(fun scope_name scope ->
let scope_dependencies = Dependency.build_scope_dependencies scope in
let is_alive (v : Dependency.ScopeDependencies.vertex) =
match v with
| Assertion _ -> true
| SubScope _ -> true
| Var (var, state) ->
let scope_def =
ScopeDef.Map.find (Var (var, state)) scope.scope_defs
in
Mark.remove scope_def.scope_def_io.io_output
(* A variable is initially alive if it is an output*)
in
let is_alive = Reachability.analyze is_alive scope_dependencies in
ScopeVar.Map.iter
(fun var states ->
let emit_unused_warning () =
Messages.emit_spanned_warning
(Mark.get (ScopeVar.get_info var))
"This variable is dead code; it does not contribute to computing \
any of scope %a outputs. Did you forget something?"
(Cli.format_with_style [ANSITerminal.yellow])
("\"" ^ Mark.remove (ScopeName.get_info scope_name) ^ "\"")
in
match states with
| WholeVar ->
if not (is_alive (Var (var, None))) then emit_unused_warning ()
| States states ->
List.iter
(fun state ->
if not (is_alive (Var (var, Some state))) then
emit_unused_warning ())
states)
scope.scope_vars)
p.program_scopes
let lint_program (p : program) : unit =
detect_empty_definitions p;
detect_dead_code p;
detect_unused_scope_vars p;
detect_unused_struct_fields p;
detect_unused_enum_constructors p;

78
tests/test_arithmetic/bad/division_by_zero.catala_en
View File

@ -4,7 +4,7 @@
```catala
declaration scope Int:
context i content decimal
output i content decimal
scope Int:
definition i equals 1 / 0
@ -14,7 +14,7 @@ scope Int:
```catala
declaration scope Dec:
context i content decimal
output i content decimal
scope Dec:
definition i equals 1. / 0.
@ -24,7 +24,7 @@ scope Dec:
```catala
declaration scope Money:
context i content decimal
output i content decimal
scope Money:
definition i equals $10.0 / $0.0
@ -33,30 +33,6 @@ scope Money:
```catala-test-inline
$ catala Interpret -s Dec
[WARNING] In scope "Int", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:7.11-7.12:
└─┐
7 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with integers
[WARNING] In scope "Dec", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:17.11-17.12:
└──┐
17 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with decimals
[WARNING] In scope "Money", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:27.11-27.12:
└──┐
27 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with money
[ERROR] division by zero at runtime
The division operator:
@ -79,30 +55,6 @@ The null denominator:
```catala-test-inline
$ catala Interpret -s Int
[WARNING] In scope "Int", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:7.11-7.12:
└─┐
7 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with integers
[WARNING] In scope "Dec", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:17.11-17.12:
└──┐
17 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with decimals
[WARNING] In scope "Money", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:27.11-27.12:
└──┐
27 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with money
[ERROR] division by zero at runtime
The division operator:
@ -125,30 +77,6 @@ The null denominator:
```catala-test-inline
$ catala Interpret -s Money
[WARNING] In scope "Int", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:7.11-7.12:
└─┐
7 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with integers
[WARNING] In scope "Dec", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:17.11-17.12:
└──┐
17 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with decimals
[WARNING] In scope "Money", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:27.11-27.12:
└──┐
27 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with money
[ERROR] division by zero at runtime
The division operator:

8
tests/test_bool/bad/bad_assert.catala_en
View File

@ -2,7 +2,7 @@
```catala
declaration scope Foo:
internal x content integer
output x content integer
scope Foo:
definition x equals 0
@ -24,10 +24,10 @@ Error coming from typechecking the following expression:
└─ Test
Type integer coming from expression:
┌─⯈ tests/test_bool/bad/bad_assert.catala_en:5.22-5.29:
┌─⯈ tests/test_bool/bad/bad_assert.catala_en:5.20-5.27:
└─┐
5 │ internal x content integer
│ ‾‾‾‾‾‾‾
5 │ output x content integer
│ ‾‾‾‾‾‾‾
└─ Test
Type bool coming from expression:

13
tests/test_date/bad/rounding_option.catala_en
View File

@ -1,8 +1,8 @@
```catala
declaration scope Test:
context bday content date
context today content date
context ambiguous content boolean
internal bday content date
internal today content date
output ambiguous content boolean
scope Test:
definition bday equals |2000-02-29|
@ -12,13 +12,6 @@ scope Test:
```catala-test-inline
$ catala Interpret -s Test
[WARNING] In scope "Test", the variable "ambiguous" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/rounding_option.catala_en:5.11-5.20:
└─┐
5 │ context ambiguous content boolean
│ ‾‾‾‾‾‾‾‾‾
catala: internal error, uncaught exception:
Dates_calc.Dates.AmbiguousComputation

13
tests/test_date/bad/rounding_option.catala_fr
View File

@ -1,8 +1,8 @@
```catala
déclaration champ d'application Test:
contexte bday contenu date
contexte today contenu date
contexte ambiguité contenu booléen
interne bday contenu date
interne today contenu date
résultat ambiguité contenu booléen
champ d'application Test:
définition bday égal à |2000-02-29|
@ -12,13 +12,6 @@ champ d'application Test:
```catala-test-inline
$ catala Interpret -s Test
[WARNING] In scope "Test", the variable "ambiguité" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/rounding_option.catala_fr:5.12-5.21:
└─┐
5 │ contexte ambiguité contenu booléen
│ ‾‾‾‾‾‾‾‾‾
catala: internal error, uncaught exception:
Dates_calc.Dates.AmbiguousComputation

136
tests/test_date/bad/uncomparable_duration.catala_en
View File

@ -4,7 +4,7 @@
```catala
declaration scope Lt:
context d content boolean
output d content boolean
scope Lt:
definition d equals 1 month < 2 day
@ -14,7 +14,7 @@ scope Lt:
```catala
declaration scope Le:
context d content boolean
output d content boolean
scope Le:
definition d equals 1 month <= 2 day
@ -24,7 +24,7 @@ scope Le:
```catala
declaration scope Gt:
context d content boolean
output d content boolean
scope Gt:
definition d equals 1 month > 2 day
@ -34,7 +34,7 @@ scope Gt:
```catala
declaration scope Ge:
context d content boolean
output d content boolean
scope Ge:
definition d equals 1 month >= 2 day
@ -42,38 +42,6 @@ scope Ge:
```catala-test-inline
$ catala Interpret -s Ge
[WARNING] In scope "Lt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:7.11-7.12:
└─┐
7 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<` operator
[WARNING] In scope "Le", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:17.11-17.12:
└──┐
17 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Gt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:27.11-27.12:
└──┐
27 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Ge", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:37.11-37.12:
└──┐
37 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `>=` operator
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:40.23-40.30:
@ -94,38 +62,6 @@ $ catala Interpret -s Ge
```catala-test-inline
$ catala Interpret -s Gt
[WARNING] In scope "Lt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:7.11-7.12:
└─┐
7 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<` operator
[WARNING] In scope "Le", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:17.11-17.12:
└──┐
17 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Gt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:27.11-27.12:
└──┐
27 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Ge", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:37.11-37.12:
└──┐
37 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `>=` operator
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:30.23-30.30:
@ -146,38 +82,6 @@ $ catala Interpret -s Gt
```catala-test-inline
$ catala Interpret -s Le
[WARNING] In scope "Lt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:7.11-7.12:
└─┐
7 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<` operator
[WARNING] In scope "Le", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:17.11-17.12:
└──┐
17 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Gt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:27.11-27.12:
└──┐
27 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Ge", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:37.11-37.12:
└──┐
37 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `>=` operator
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:20.23-20.30:
@ -198,38 +102,6 @@ $ catala Interpret -s Le
```catala-test-inline
$ catala Interpret -s Lt
[WARNING] In scope "Lt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:7.11-7.12:
└─┐
7 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<` operator
[WARNING] In scope "Le", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:17.11-17.12:
└──┐
17 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Gt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:27.11-27.12:
└──┐
27 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Ge", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:37.11-37.12:
└──┐
37 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `>=` operator
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:10.23-10.30:

9
tests/test_default/bad/conflict.catala_en
View File

@ -2,7 +2,7 @@
```catala
declaration scope A:
context x content integer
output x content integer
scope A:
definition x under condition true consequence equals 1
@ -11,13 +11,6 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_default/bad/conflict.catala_en:5.11-5.12:
└─┐
5 │ context x content integer
│ ‾
└─ Article
[ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
This consequence has a valid justification:

25
tests/test_default/bad/empty.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content integer
context y content boolean
output x content integer
output y content boolean
scope A:
definition x equals 1
@ -11,26 +11,19 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
[WARNING] In scope "A", the variable "y" is declared but never defined; did you forget something?
┌─⯈ tests/test_default/bad/empty.catala_en:5.11-5.12:
┌─⯈ tests/test_default/bad/empty.catala_en:6.10-6.11:
└─┐
5 │ context x content integer
│ ‾
└─ Article
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_default/bad/empty.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Article
[ERROR] This variable evaluated to an empty term (no rule that defined it applied in this situation)
┌─⯈ tests/test_default/bad/empty.catala_en:6.11-6.12:
┌─⯈ tests/test_default/bad/empty.catala_en:6.10-6.11:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Article
#return code 255#
```

17
tests/test_default/bad/empty_with_rules.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content integer
context y content integer
output x content integer
output y content integer
scope A:
definition y equals 1
@ -14,19 +14,12 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_default/bad/empty_with_rules.catala_en:5.11-5.12:
└─┐
5 │ context x content integer
│ ‾
└─ Article
[ERROR] This variable evaluated to an empty term (no rule that defined it applied in this situation)
┌─⯈ tests/test_default/bad/empty_with_rules.catala_en:5.11-5.12:
┌─⯈ tests/test_default/bad/empty_with_rules.catala_en:5.10-5.11:
└─┐
5 │ context x content integer
│ ‾
5 │ output x content integer
│ ‾
└─ Article
#return code 255#
```

11
tests/test_enum/bad/missing_case.catala_en
View File

@ -7,8 +7,8 @@ declaration enumeration E:
-- Case3
declaration scope A:
context e content E
context out content boolean
input e content E
output out content boolean
scope A:
definition out equals match e with pattern
@ -18,13 +18,6 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "out" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_enum/bad/missing_case.catala_en:11.11-11.14:
└──┐
11 │ context out content boolean
│ ‾‾‾
└─ Article
[WARNING] The constructor "Case3" of enumeration "E" is never used; maybe it's unnecessary?
┌─⯈ tests/test_enum/bad/missing_case.catala_en:7.6-7.11:

9
tests/test_exception/bad/exceptions_cycle.catala_en
View File

@ -2,7 +2,7 @@
```catala
declaration scope A:
context x content integer
output x content integer
scope A:
label base_x
@ -20,13 +20,6 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_exception/bad/exceptions_cycle.catala_en:5.11-5.12:
└─┐
5 │ context x content integer
│ ‾
└─ Test
[ERROR] Exception cycle detected when defining x: each of these 3 exceptions applies over the previous one, and the first applies over the last
┌─⯈ tests/test_exception/bad/exceptions_cycle.catala_en:8.3-10.15:

9
tests/test_exception/bad/self_exception.catala_en
View File

@ -2,7 +2,7 @@
```catala
declaration scope A:
context y content integer
output y content integer
scope A:
label base_y
@ -12,13 +12,6 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_exception/bad/self_exception.catala_en:5.11-5.12:
└─┐
5 │ context y content integer
│ ‾
└─ Test
[ERROR] Cannot define rule as an exception to itself
┌─⯈ tests/test_exception/bad/self_exception.catala_en:9.13-9.19:

9
tests/test_exception/bad/two_exceptions.catala_en
View File

@ -2,7 +2,7 @@
```catala
declaration scope A:
context x content integer
output x content integer
scope A:
label base_x
@ -17,13 +17,6 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_exception/bad/two_exceptions.catala_en:5.11-5.12:
└─┐
5 │ context x content integer
│ ‾
└─ Test
[ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
This consequence has a valid justification:

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

@ -2,7 +2,7 @@
```catala
declaration scope A:
context f content integer depends on x content integer
output f content integer depends on x content integer
declaration scope B:
input b content boolean
@ -17,51 +17,81 @@ scope B:
```catala-test-inline
$ catala Scopelang -s B
[WARNING] In scope "A", the variable "f" is never used anywhere; maybe it's unnecessary?
[ERROR] It is impossible to give a definition to a subscope variable not tagged as input or context.
┌─⯈ tests/test_func/good/context_func.catala_en:5.11-5.12:
Incriminated subscope:
┌─⯈ tests/test_func/good/context_func.catala_en:9.3-9.4:
└─┐
5 │ context f content integer depends on x content integer
│ ‾
9 │ a scope A
│ ‾
└─ Test
let scope B (b: bool|input) =
let a.f : integer → integer = λ (x: integer) → ⟨b && x > 0 ⊢ x - 1⟩;
call A[a]
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 255#
```
```catala-test-inline
$ catala Dcalc -s A
[WARNING] In scope "A", the variable "f" is never used anywhere; maybe it's unnecessary?
[ERROR] It is impossible to give a definition to a subscope variable not tagged as input or context.
┌─⯈ tests/test_func/good/context_func.catala_en:5.11-5.12:
Incriminated subscope:
┌─⯈ tests/test_func/good/context_func.catala_en:9.3-9.4:
└─┐
5 │ context f content integer depends on x content integer
│ ‾
9 │ a scope A
│ ‾
└─ Test
let scope A (A_in: A_in {f_in: integer → integer}): A =
let get f : integer → integer = A_in.f_in in
let set f : integer → integer =
λ (x: integer) →
error_empty ⟨ f x | true ⊢ ⟨true ⊢ x + 1⟩ ⟩
in
return {A}
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 255#
```
```catala-test-inline
$ catala Dcalc -s B
[WARNING] In scope "A", the variable "f" is never used anywhere; maybe it's unnecessary?
[ERROR] It is impossible to give a definition to a subscope variable not tagged as input or context.
┌─⯈ tests/test_func/good/context_func.catala_en:5.11-5.12:
Incriminated subscope:
┌─⯈ tests/test_func/good/context_func.catala_en:9.3-9.4:
└─┐
5 │ context f content integer depends on x content integer
│ ‾
9 │ a scope A
│ ‾
└─ Test
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⟩
in
let call result : A = A { A_in f_in = a.f; } in
return {B}
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 255#
```

15
tests/test_io/bad/redefining_input.catala_en
View File

@ -2,27 +2,20 @@
```catala
declaration scope A:
input a content integer
input output a content integer
scope A:
definition a equals 0
```
```catala-test-inline
$ catala Typecheck
[WARNING] In scope "A", the variable "a" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_io/bad/redefining_input.catala_en:5.9-5.10:
└─┐
5 │ input a content integer
│ ‾
└─ Test
[ERROR] It is impossible to give a definition to a scope variable tagged as input.
Incriminated variable:
┌─⯈ tests/test_io/bad/redefining_input.catala_en:5.9-5.10:
┌─⯈ tests/test_io/bad/redefining_input.catala_en:5.16-5.17:
└─┐
5 │ input a content integer
│ ‾
5 │ input output a content integer
│ ‾
└─ Test
Incriminated variable definition:

7
tests/test_io/bad/using_non_output.catala_en
View File

@ -15,6 +15,13 @@ scope B:
```
```catala-test-inline
$ catala Typecheck
[WARNING] This variable is dead code; it does not contribute to computing any of scope "A" outputs. Did you forget something?
┌─⯈ tests/test_io/bad/using_non_output.catala_en:5.12-5.13:
└─┐
5 │ internal a content integer
│ ‾
└─ Test
[WARNING] In scope "A", the variable "a" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_io/bad/using_non_output.catala_en:5.12-5.13:

17
tests/test_proof/bad/array_length-empty.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content collection integer
context y content boolean
internal x content collection integer
output y content boolean
scope A:
definition x equals [0; 5]
@ -12,18 +12,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/array_length-empty.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/array_length-empty.catala_en:6.11-6.12:
┌─⯈ tests/test_proof/bad/array_length-empty.catala_en:6.10-6.11:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/array_length-overlap.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content collection integer
context y content boolean
internal x content collection integer
output y content boolean
scope A:
definition x equals [0; 5]
@ -13,18 +13,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/array_length-overlap.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/array_length-overlap.catala_en:6.11-6.12:
┌─⯈ tests/test_proof/bad/array_length-overlap.catala_en:6.10-6.11:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

26
tests/test_proof/bad/dates_get_year-empty.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content date
context y content boolean
input x content date
output y content boolean
scope A:
definition x equals |2022-01-16|
@ -15,18 +15,20 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
[ERROR] It is impossible to give a definition to a scope variable tagged as input.
┌─⯈ tests/test_proof/bad/dates_get_year-empty.catala_en:6.11-6.12:
Incriminated variable:
┌─⯈ tests/test_proof/bad/dates_get_year-empty.catala_en:5.9-5.10:
└─┐
6 │ context y content boolean
│ ‾
5 │ input x content date
│ ‾
└─ Test
[WARNING] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/dates_get_year-empty.catala_en:6.11-6.12:
Incriminated variable definition:
┌─⯈ tests/test_proof/bad/dates_get_year-empty.catala_en:9.3-9.15:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
9 │ definition x equals |2022-01-16|
│ ‾‾‾‾‾‾‾‾‾‾‾‾
#return code 255#
```

17
tests/test_proof/bad/dates_get_year-overlap.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content date
context y content boolean
internal x content date
output y content boolean
scope A:
definition x equals |2022-01-16|
@ -15,18 +15,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/dates_get_year-overlap.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/dates_get_year-overlap.catala_en:6.11-6.12:
┌─⯈ tests/test_proof/bad/dates_get_year-overlap.catala_en:6.10-6.11:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/dates_simple-empty.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content date
context y content boolean
internal x content date
output y content boolean
scope A:
definition x equals |2022-01-16|
@ -14,18 +14,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/dates_simple-empty.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/dates_simple-empty.catala_en:6.11-6.12:
┌─⯈ tests/test_proof/bad/dates_simple-empty.catala_en:6.10-6.11:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/dates_simple-overlap.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content date
context y content boolean
internal x content date
output y content boolean
scope A:
definition x equals |2022-01-16|
@ -15,18 +15,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/dates_simple-overlap.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/dates_simple-overlap.catala_en:6.11-6.12:
┌─⯈ tests/test_proof/bad/dates_simple-overlap.catala_en:6.10-6.11:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/duration-empty.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content duration
context y content boolean
internal x content duration
output y content boolean
scope A:
definition x equals 94 day
@ -12,18 +12,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/duration-empty.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/duration-empty.catala_en:6.11-6.12:
┌─⯈ tests/test_proof/bad/duration-empty.catala_en:6.10-6.11:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/duration-overlap.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content duration
context y content boolean
internal x content duration
output y content boolean
scope A:
definition x equals 94 day
@ -13,18 +13,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/duration-overlap.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/duration-overlap.catala_en:6.11-6.12:
┌─⯈ tests/test_proof/bad/duration-overlap.catala_en:6.10-6.11:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/enums-empty.catala_en
View File

@ -12,8 +12,8 @@ declaration enumeration S:
-- B content T
declaration scope A:
context x content integer
context y content S
output x content integer
internal y content S
scope A:
definition y equals B content (D content 1)
@ -23,13 +23,6 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-empty.catala_en:15.11-15.12:
└──┐
15 │ context x content integer
│ ‾
└─ Test
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-empty.catala_en:7.7-7.8:
@ -38,10 +31,10 @@ $ catala Proof --disable_counterexamples
│ ‾
└─ Test
[WARNING] [A.x] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/enums-empty.catala_en:15.11-15.12:
┌─⯈ tests/test_proof/bad/enums-empty.catala_en:15.10-15.11:
└──┐
15 │ context x content integer
│ ‾
15 │ output x content integer
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/enums-nonbool-empty.catala_en
View File

@ -10,8 +10,8 @@ declaration enumeration S:
-- B content T
declaration scope A:
context x content integer
context y content S
output x content integer
internal y content S
scope A:
definition y equals B content (D content 1)
@ -21,13 +21,6 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-nonbool-empty.catala_en:13.11-13.12:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-nonbool-empty.catala_en:5.7-5.8:
@ -36,10 +29,10 @@ $ catala Proof --disable_counterexamples
│ ‾
└─ Test
[WARNING] [A.x] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/enums-nonbool-empty.catala_en:13.11-13.12:
┌─⯈ tests/test_proof/bad/enums-nonbool-empty.catala_en:13.10-13.11:
└──┐
13 │ context x content integer
│ ‾
13 │ output x content integer
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/enums-nonbool-overlap.catala_en
View File

@ -10,8 +10,8 @@ declaration enumeration S:
-- B content T
declaration scope A:
context x content integer
context y content S
output x content integer
internal y content S
scope A:
definition y equals B content (D content 1)
@ -21,13 +21,6 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-nonbool-overlap.catala_en:13.11-13.12:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-nonbool-overlap.catala_en:5.7-5.8:
@ -36,10 +29,10 @@ $ catala Proof --disable_counterexamples
│ ‾
└─ Test
[WARNING] [A.x] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/enums-nonbool-overlap.catala_en:13.11-13.12:
┌─⯈ tests/test_proof/bad/enums-nonbool-overlap.catala_en:13.10-13.11:
└──┐
13 │ context x content integer
│ ‾
13 │ output x content integer
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/enums-overlap.catala_en
View File

@ -12,8 +12,8 @@ declaration enumeration S:
-- B content T
declaration scope A:
context x content integer
context y content S
output x content integer
internal y content S
scope A:
definition y equals B content (D content 1)
@ -23,13 +23,6 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-overlap.catala_en:15.11-15.12:
└──┐
15 │ context x content integer
│ ‾
└─ Test
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-overlap.catala_en:7.7-7.8:
@ -38,10 +31,10 @@ $ catala Proof --disable_counterexamples
│ ‾
└─ Test
[WARNING] [A.x] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/enums-overlap.catala_en:15.11-15.12:
┌─⯈ tests/test_proof/bad/enums-overlap.catala_en:15.10-15.11:
└──┐
15 │ context x content integer
│ ‾
15 │ output x content integer
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/enums_inj-empty.catala_en
View File

@ -6,8 +6,8 @@ declaration enumeration E:
-- C2
declaration scope A:
context x content E
context y content integer
internal x content E
output y content integer
scope A:
definition x equals C1
@ -16,13 +16,6 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums_inj-empty.catala_en:10.11-10.12:
└──┐
10 │ context y content integer
│ ‾
└─ Article
[WARNING] The constructor "C2" of enumeration "E" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums_inj-empty.catala_en:6.6-6.8:
@ -31,10 +24,10 @@ $ catala Proof --disable_counterexamples
│ ‾‾
└─ Article
[WARNING] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/enums_inj-empty.catala_en:10.11-10.12:
┌─⯈ tests/test_proof/bad/enums_inj-empty.catala_en:10.10-10.11:
└──┐
10 │ context y content integer
│ ‾
10 │ output y content integer
│ ‾
└─ Article
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/enums_inj-overlap.catala_en
View File

@ -6,8 +6,8 @@ declaration enumeration E:
-- C2
declaration scope A:
context x content E
context y content integer
internal x content E
output y content integer
scope A:
definition x equals C1
@ -18,18 +18,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums_inj-overlap.catala_en:10.11-10.12:
└──┐
10 │ context y content integer
│ ‾
└─ Article
[WARNING] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/enums_inj-overlap.catala_en:10.11-10.12:
┌─⯈ tests/test_proof/bad/enums_inj-overlap.catala_en:10.10-10.11:
└──┐
10 │ context y content integer
│ ‾
10 │ output y content integer
│ ‾
└─ Article
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/enums_unit-empty.catala_en
View File

@ -6,8 +6,8 @@ declaration enumeration E:
-- Case2
declaration scope A:
context x content E
context y content integer
internal x content E
output y content integer
scope A:
definition x equals Case1 content 2
@ -21,18 +21,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums_unit-empty.catala_en:10.11-10.12:
└──┐
10 │ context y content integer
│ ‾
└─ Article
[WARNING] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/enums_unit-empty.catala_en:10.11-10.12:
┌─⯈ tests/test_proof/bad/enums_unit-empty.catala_en:10.10-10.11:
└──┐
10 │ context y content integer
│ ‾
10 │ output y content integer
│ ‾
└─ Article
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/enums_unit-overlap.catala_en
View File

@ -6,8 +6,8 @@ declaration enumeration E:
-- Case2
declaration scope A:
context x content E
context y content integer
internal x content E
output y content integer
scope A:
definition x equals Case1 content 2
@ -21,18 +21,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums_unit-overlap.catala_en:10.11-10.12:
└──┐
10 │ context y content integer
│ ‾
└─ Article
[WARNING] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/enums_unit-overlap.catala_en:10.11-10.12:
┌─⯈ tests/test_proof/bad/enums_unit-overlap.catala_en:10.10-10.11:
└──┐
10 │ context y content integer
│ ‾
10 │ output y content integer
│ ‾
└─ Article
Counterexample generation is disabled so none was generated.
```

15
tests/test_proof/bad/let_in_condition-empty.catala_en
View File

@ -2,7 +2,7 @@
```catala
declaration scope A:
context x content boolean
output x content boolean
scope A:
definition x under condition
@ -13,18 +13,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/let_in_condition-empty.catala_en:5.11-5.12:
└─┐
5 │ context x content boolean
│ ‾
└─ Test
[WARNING] [A.x] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/let_in_condition-empty.catala_en:5.11-5.12:
┌─⯈ tests/test_proof/bad/let_in_condition-empty.catala_en:5.10-5.11:
└─┐
5 │ context x content boolean
│ ‾
5 │ output x content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/money-empty.catala_en
View File

@ -4,8 +4,8 @@ The case x < $1000 is not handled
```catala
declaration scope A:
context x content money
context y content boolean
internal x content money
output y content boolean
scope A:
definition x equals $20,000
@ -16,18 +16,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/money-empty.catala_en:8.11-8.12:
└─┐
8 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/money-empty.catala_en:8.11-8.12:
┌─⯈ tests/test_proof/bad/money-empty.catala_en:8.10-8.11:
└─┐
8 │ context y content boolean
│ ‾
8 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/money-overlap.catala_en
View File

@ -4,8 +4,8 @@ Overlap when x = $1000
```catala
declaration scope A:
context x content money
context y content boolean
internal x content money
output y content boolean
scope A:
definition x equals $20,000
@ -17,18 +17,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/money-overlap.catala_en:8.11-8.12:
└─┐
8 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/money-overlap.catala_en:8.11-8.12:
┌─⯈ tests/test_proof/bad/money-overlap.catala_en:8.10-8.11:
└─┐
8 │ context y content boolean
│ ‾
8 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/no_vars-conflict.catala_en
View File

@ -4,8 +4,8 @@ Should fail since y has two definitions when x = 0
```catala
declaration scope A:
context x content integer
context y content integer
internal x content integer
output y content integer
scope A:
definition x under condition (6*7 = 42) and (false or (true and 1458 / 27 = 54.))
@ -17,18 +17,11 @@ scope A:
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/no_vars-conflict.catala_en:8.11-8.12:
└─┐
8 │ context y content integer
│ ‾
└─ Test
[WARNING] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/no_vars-conflict.catala_en:8.11-8.12:
┌─⯈ tests/test_proof/bad/no_vars-conflict.catala_en:8.10-8.11:
└─┐
8 │ context y content integer
│ ‾
8 │ output y content integer
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/no_vars-empty.catala_en
View File

@ -3,8 +3,8 @@
```catala
declaration scope A:
context x content integer
context y content integer
internal x content integer
output y content integer
scope A:
definition x under condition (6*7 = 42) and (false or (true and 1458 / 27 = 54.))
@ -16,18 +16,11 @@ scope A:
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/no_vars-empty.catala_en:7.11-7.12:
└─┐
7 │ context y content integer
│ ‾
└─ Test
[WARNING] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/no_vars-empty.catala_en:7.11-7.12:
┌─⯈ tests/test_proof/bad/no_vars-empty.catala_en:7.10-7.11:
└─┐
7 │ context y content integer
│ ‾
7 │ output y content integer
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

67
tests/test_proof/bad/prolala_motivating_example.catala_en
View File

@ -6,8 +6,8 @@ Demo: https://asciinema.org/a/461790
```catala-metadata
declaration scope Eligibility:
context is_student content boolean
context is_professor content boolean
internal is_student content boolean
internal is_professor content boolean
output is_eligible content boolean
output is_eligible_correct condition
@ -54,11 +54,11 @@ scope Eligibility:
```catala-metadata
declaration scope Amount:
eligibility scope Eligibility
context is_student content boolean
context is_professor content boolean
context number_of_advisors content integer
context amount content integer
context correct_amount content integer
internal is_student content boolean
internal is_professor content boolean
internal number_of_advisors content integer
output amount content integer
output correct_amount content integer
scope Amount:
definition eligibility.is_student equals is_student
@ -123,44 +123,29 @@ scope Amount:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "Amount", the variable "amount" is never used anywhere; maybe it's unnecessary?
[ERROR] It is impossible to give a definition to a subscope variable not tagged as input or context.
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:60.11-60.17:
Incriminated subscope:
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:56.3-56.14:
└──┐
60 │ context amount content integer
│ ‾‾‾‾‾‾
56 │ eligibility scope Eligibility
│ ‾‾‾‾‾‾‾‾‾‾‾
└┬ ProLaLa 2022 Super Cash Bonus
└─ Amount
[WARNING] In scope "Amount", the variable "correct_amount" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:61.11-61.25:
Incriminated variable:
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:9.12-9.22:
└─┐
9 │ internal is_student content boolean
│ ‾‾‾‾‾‾‾‾‾‾
└┬ ProLaLa 2022 Super Cash Bonus
└─ Eligibility
Incriminated subscope variable definition:
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:64.3-64.36:
└──┐
61 │ context correct_amount content integer
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ ProLaLa 2022 Super Cash Bonus
└─ Amount
[WARNING] [Amount.amount] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:60.11-60.17:
└──┐
60 │ context amount content integer
│ ‾‾‾‾‾‾
└┬ ProLaLa 2022 Super Cash Bonus
└─ Amount
Counterexample generation is disabled so none was generated.
[WARNING] [Eligibility.is_eligible] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:11.10-11.21:
└──┐
11 │ output is_eligible content boolean
│ ‾‾‾‾‾‾‾‾‾‾‾
└┬ ProLaLa 2022 Super Cash Bonus
└─ Eligibility
Counterexample generation is disabled so none was generated.
[WARNING] [Eligibility.is_eligible] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:11.10-11.21:
└──┐
11 │ output is_eligible content boolean
│ ‾‾‾‾‾‾‾‾‾‾‾
└┬ ProLaLa 2022 Super Cash Bonus
└─ Eligibility
Counterexample generation is disabled so none was generated.
64 │ definition eligibility.is_student equals is_student
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
#return code 255#
```

17
tests/test_proof/bad/rationals-empty.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content decimal
context y content boolean
internal x content decimal
output y content boolean
scope A:
definition x equals 1.
@ -12,18 +12,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/rationals-empty.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/rationals-empty.catala_en:6.11-6.12:
┌─⯈ tests/test_proof/bad/rationals-empty.catala_en:6.10-6.11:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/rationals-overlap.catala_en
View File

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content decimal
context y content boolean
internal x content decimal
output y content boolean
scope A:
definition x equals 1.
@ -13,18 +13,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/rationals-overlap.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[WARNING] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/rationals-overlap.catala_en:6.11-6.12:
┌─⯈ tests/test_proof/bad/rationals-overlap.catala_en:6.10-6.11:
└─┐
6 │ context y content boolean
│ ‾
6 │ output y content boolean
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

33
tests/test_proof/bad/sat_solving.catala_en
View File

@ -3,16 +3,16 @@
```catala
declaration scope A:
context x1 content boolean
context x2 content boolean
context x3 content boolean
context x4 content boolean
context x5 content boolean
context x6 content boolean
context x7 content boolean
context x8 content boolean
context x9 content boolean
context x10 content boolean
internal x1 content boolean
internal x2 content boolean
internal x3 content boolean
internal x4 content boolean
internal x5 content boolean
internal x6 content boolean
internal x7 content boolean
internal x8 content boolean
internal x9 content boolean
output x10 content boolean
scope A:
definition x1 equals true
@ -40,18 +40,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x10" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/sat_solving.catala_en:15.11-15.14:
└──┐
15 │ context x10 content boolean
│ ‾‾‾
└─ Test
[WARNING] [A.x10] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/sat_solving.catala_en:15.11-15.14:
┌─⯈ tests/test_proof/bad/sat_solving.catala_en:15.10-15.13:
└──┐
15 │ context x10 content boolean
│ ‾‾‾
15 │ output x10 content boolean
│ ‾‾‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/structs-empty.catala_en
View File

@ -10,8 +10,8 @@ declaration structure S:
data b content T
declaration scope A:
context x content integer
context y content S
output x content integer
internal y content S
scope A:
definition y equals S { -- a : 0 -- b : T { -- c : false -- d: 0}}
@ -21,18 +21,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/structs-empty.catala_en:13.11-13.12:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[WARNING] [A.x] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/structs-empty.catala_en:13.11-13.12:
┌─⯈ tests/test_proof/bad/structs-empty.catala_en:13.10-13.11:
└──┐
13 │ context x content integer
│ ‾
13 │ output x content integer
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

17
tests/test_proof/bad/structs-overlap.catala_en
View File

@ -10,8 +10,8 @@ declaration structure S:
data b content T
declaration scope A:
context x content integer
context y content S
output x content integer
internal y content S
scope A:
definition y equals S { -- a : 0 -- b : T { -- c : false -- d: 0}}
@ -21,18 +21,11 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/structs-overlap.catala_en:13.11-13.12:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[WARNING] [A.x] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/structs-overlap.catala_en:13.11-13.12:
┌─⯈ tests/test_proof/bad/structs-overlap.catala_en:13.10-13.11:
└──┐
13 │ context x content integer
│ ‾
13 │ output x content integer
│ ‾
└─ Test
Counterexample generation is disabled so none was generated.
```

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

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content collection integer
context y content boolean
internal x content collection integer
output y content boolean
scope A:
definition x equals [0; 5]
@ -13,12 +13,5 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/array_length.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

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

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content date
context y content boolean
internal x content date
output y content boolean
scope A:
definition x equals |2022-01-16|
@ -15,12 +15,5 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/dates_get_year.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

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

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content duration
context y content boolean
internal x content duration
output y content boolean
scope A:
definition x equals 94 day
@ -13,12 +13,5 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/duration.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

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

@ -10,8 +10,8 @@ declaration enumeration S:
-- B content T
declaration scope A:
context x content integer
context y content S
output x content integer
internal y content S
scope A:
definition y equals B content (D content 1)
@ -21,13 +21,6 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/enums-arith.catala_en:13.11-13.12:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[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:

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

@ -10,8 +10,8 @@ declaration enumeration S:
-- B content T
declaration scope A:
context x content integer
context y content S
output x content integer
internal y content S
scope A:
definition y equals B content (D content 1)
@ -21,13 +21,6 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/enums-nonbool.catala_en:13.11-13.12:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[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:

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

@ -10,8 +10,8 @@ declaration enumeration S:
-- B content T
declaration scope A:
context x content integer
context y content S
output x content integer
internal y content S
scope A:
definition y equals B content (D content 1)
@ -20,13 +20,6 @@ scope A:
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/enums.catala_en:13.11-13.12:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[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:

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

@ -6,8 +6,8 @@ declaration enumeration E:
-- C2
declaration scope A:
context x content E
context y content integer
internal x content E
output y content integer
scope A:
definition x equals C1
@ -17,12 +17,5 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/enums_inj.catala_en:10.11-10.12:
└──┐
10 │ context y content integer
│ ‾
└─ Article
[RESULT] No errors found during the proof mode run.
```

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

@ -6,8 +6,8 @@ declaration enumeration E:
-- Case2
declaration scope A:
context x content E
context y content integer
internal x content E
output y content integer
scope A:
definition x equals Case1 content 2
@ -21,12 +21,5 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/enums_unit.catala_en:10.11-10.12:
└──┐
10 │ context y content integer
│ ‾
└─ Article
[RESULT] No errors found during the proof mode run.
```

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

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content integer depends on y content boolean
context z content integer
internal x content integer depends on y content boolean
output z content integer
scope A:
definition x of y under condition y consequence equals 0
@ -14,12 +14,5 @@ scope A:
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "z" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/functions.catala_en:6.11-6.12:
└─┐
6 │ context z content integer
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

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

@ -2,7 +2,7 @@
```catala
declaration scope A:
context x content boolean
output x content boolean
scope A:
definition x under condition
@ -13,12 +13,5 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/let_in_condition.catala_en:5.11-5.12:
└─┐
5 │ context x content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

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

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content money
context y content boolean
internal x content money
output y content boolean
scope A:
definition x equals $20,000
@ -15,12 +15,5 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/money.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

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

@ -2,7 +2,7 @@
```catala
declaration scope A:
context x content integer
output x content integer
scope A:
definition x under condition (6*7 = 42) and (false or (true and 1458 / 27 = 54.))
@ -10,12 +10,5 @@ scope A:
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/no_vars.catala_en:5.11-5.12:
└─┐
5 │ context x content integer
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

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

@ -2,8 +2,8 @@
```catala
declaration scope A:
context x content decimal
context y content boolean
internal x content decimal
output y content boolean
scope A:
definition x equals 1.
@ -13,12 +13,5 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/rationals.catala_en:6.11-6.12:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

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

@ -2,9 +2,9 @@
```catala
declaration scope A:
context x content integer
context y content boolean
context z content integer
internal x content integer
internal y content boolean
output z content integer
scope A:
definition y equals true
@ -16,12 +16,5 @@ scope A:
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "z" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/simple_vars.catala_en:7.11-7.12:
└─┐
7 │ context z content integer
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

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

@ -10,8 +10,8 @@ declaration structure S:
data b content T
declaration scope A:
context x content integer
context y content S
output x content integer
internal y content S
scope A:
definition y equals S { -- a : 0 -- b : T { -- c : false -- d: 0}}
@ -20,12 +20,5 @@ scope A:
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/structs.catala_en:13.11-13.12:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

6
tests/test_scope/bad/cycle_in_scope.catala_en
View File

@ -2,9 +2,9 @@
```catala
declaration scope A:
context x content integer
context y content integer
context z content integer
output x content integer
output y content integer
output z content integer
scope A:
definition y under condition x < 0 consequence equals - x

20
tests/test_scope/bad/scope.catala_en
View File

@ -2,9 +2,9 @@
```catala
declaration scope A:
context a content integer
context b content integer
context c content boolean
output a content integer
output b content integer
internal c content boolean
scope A:
definition c equals false
@ -16,20 +16,6 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "a" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_scope/bad/scope.catala_en:5.11-5.12:
└─┐
5 │ context a content integer
│ ‾
└─ Article
[WARNING] In scope "A", the variable "b" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_scope/bad/scope.catala_en:6.11-6.12:
└─┐
6 │ context b content integer
│ ‾
└─ Article
[ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
This consequence has a valid justification:

17
tests/test_scope/bad/scope_call_missing.catala_en
View File

@ -1,7 +1,7 @@
```catala
declaration scope Toto:
context bar content integer
input baz content decimal
internal bar content integer
input output baz content decimal
output foo content integer
scope Toto:
@ -16,13 +16,6 @@ scope Titi:
```catala-test-inline
$ catala dcalc -s Titi
[WARNING] In scope "Toto", the variable "baz" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_scope/bad/scope_call_missing.catala_en:4.9-4.12:
└─┐
4 │ input baz content decimal
│ ‾‾‾
[ERROR] Definition of input variable 'baz' missing in this scope call
┌─⯈ tests/test_scope/bad/scope_call_missing.catala_en:14.26-14.56:
@ -32,10 +25,10 @@ $ catala dcalc -s Titi
Declaration of the missing input variable
┌─⯈ tests/test_scope/bad/scope_call_missing.catala_en:4.9-4.12:
┌─⯈ tests/test_scope/bad/scope_call_missing.catala_en:4.16-4.19:
└─┐
4 │ input baz content decimal
│ ‾‾‾
4 │ input output baz content decimal
│ ‾‾‾
#return code 255#
```

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

@ -2,10 +2,10 @@
```catala
declaration scope ScopeA:
context output a content boolean
output a content boolean
declaration scope ScopeB:
context a content boolean
output a content boolean
scopeA scope ScopeA
scope ScopeA:
@ -17,13 +17,6 @@ scope ScopeB:
```catala-test-inline
$ catala OCaml -O
[WARNING] In scope "ScopeB", the variable "a" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_scope/good/191_fix_record_name_confusion.catala_en:8.11-8.12:
└─┐
8 │ context a content boolean
│ ‾
└─ Article
(** This file has been generated by the Catala compiler, do not edit! *)
open Runtime_ocaml.Runtime
@ -35,37 +28,34 @@ module ScopeA = struct
end
module ScopeB = struct
type t = unit
type t = {a: bool}
end
module ScopeAIn = struct
type t = {a_in: unit -> bool}
type t = unit
end
module ScopeBIn = struct
type t = {a_in: unit -> bool}
type t = unit
end
let scope_a (scope_a_in: ScopeAIn.t) : ScopeA.t =
let a_: unit -> bool = scope_a_in.ScopeAIn.a_in in
let a_: bool = try (try (a_ ()) with EmptyError -> true) with
let a_: bool = try true with
EmptyError -> (raise (NoValueProvided
{filename = "tests/test_scope/good/191_fix_record_name_confusion.catala_en";
start_line=5; start_column=18; end_line=5; end_column=19;
start_line=5; start_column=10; end_line=5; end_column=11;
law_headings=["Article"]})) in
{ScopeA.a = a_}
let scope_b (scope_b_in: ScopeBIn.t) : ScopeB.t =
let a_: unit -> bool = scope_b_in.ScopeBIn.a_in in
let scope_a_dot_a_: unit -> bool = fun (_: unit) -> raise EmptyError in
let result_: ScopeA.t = scope_a ({ScopeAIn.a_in = scope_a_dot_a_}) in
let result_: ScopeA.t = scope_a (()) in
let scope_a_dot_a_: bool = result_.ScopeA.a in
let a_: bool = try (try (a_ ()) with EmptyError -> scope_a_dot_a_) with
let a_: bool = try scope_a_dot_a_ with
EmptyError -> (raise (NoValueProvided
{filename = "tests/test_scope/good/191_fix_record_name_confusion.catala_en";
start_line=8; start_column=11; end_line=8; end_column=12;
start_line=8; start_column=10; end_line=8; end_column=11;
law_headings=["Article"]})) in
()
{ScopeB.a = a_}
```

9
tests/test_struct/bad/nested.catala_en
View File

@ -6,7 +6,7 @@ declaration enumeration E:
-- Rec content E
declaration scope A:
context y content E
output y content E
scope A:
definition y equals E.Empty
@ -14,13 +14,6 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_struct/bad/nested.catala_en:9.11-9.12:
└─┐
9 │ context y content E
│ ‾
└─ Article
[WARNING] The constructor "Rec" of enumeration "E" is never used; maybe it's unnecessary?
┌─⯈ tests/test_struct/bad/nested.catala_en:6.6-6.9:

10
tests/test_struct/bad/nested2.catala_en
View File

@ -10,17 +10,17 @@ declaration enumeration E:
-- Case2 content S
declaration scope A:
context x content E
output x content E
```
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
[WARNING] In scope "A", the variable "x" is declared but never defined; did you forget something?
┌─⯈ tests/test_struct/bad/nested2.catala_en:13.11-13.12:
┌─⯈ tests/test_struct/bad/nested2.catala_en:13.10-13.11:
└──┐
13 │ context x content E
│ ‾
13 │ output x content E
│ ‾
└─ Article
[WARNING] The structure "S" is never used; maybe it's unnecessary?

24
tests/test_struct/good/ambiguous_fields.catala_en
View File

@ -8,8 +8,8 @@ declaration structure Bar:
data f content integer
declaration scope A:
context x content Foo
context y content integer
internal x content Foo
output y content integer
scope A:
definition x equals Foo { -- f: 1 }
@ -18,13 +18,6 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_struct/good/ambiguous_fields.catala_en:12.11-12.12:
└──┐
12 │ context y content integer
│ ‾
└─ Article
[WARNING] The structure "Bar" is never used; maybe it's unnecessary?
┌─⯈ tests/test_struct/good/ambiguous_fields.catala_en:7.23-7.26:
@ -32,17 +25,11 @@ $ catala Interpret -s A
7 │ declaration structure Bar:
│ ‾‾‾
└─ Article
[RESULT] Computation successful!
[RESULT] Computation successful! Results:
[RESULT] y = 1
```
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_struct/good/ambiguous_fields.catala_en:12.11-12.12:
└──┐
12 │ context y content integer
│ ‾
└─ Article
[WARNING] The structure "Bar" is never used; maybe it's unnecessary?
┌─⯈ tests/test_struct/good/ambiguous_fields.catala_en:7.23-7.26:
@ -50,5 +37,6 @@ $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
7 │ declaration structure Bar:
│ ‾‾‾
└─ Article
[RESULT] Computation successful!
[RESULT] Computation successful! Results:
[RESULT] y = ESome 1
```