From 09bcefbcc17c0f7149d667376319a25fd372ee00 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Sat, 3 Jun 2023 18:02:57 +0200 Subject: [PATCH] Update tests --- compiler/desugared/linting.ml | 58 ++++++++ .../bad/division_by_zero.catala_en | 78 +--------- tests/test_bool/bad/bad_assert.catala_en | 8 +- tests/test_date/bad/rounding_option.catala_en | 13 +- tests/test_date/bad/rounding_option.catala_fr | 13 +- .../bad/uncomparable_duration.catala_en | 136 +----------------- tests/test_default/bad/conflict.catala_en | 9 +- tests/test_default/bad/empty.catala_en | 25 ++-- .../bad/empty_with_rules.catala_en | 17 +-- tests/test_enum/bad/missing_case.catala_en | 11 +- .../bad/exceptions_cycle.catala_en | 9 +- .../bad/self_exception.catala_en | 9 +- .../bad/two_exceptions.catala_en | 9 +- tests/test_func/good/context_func.catala_en | 92 ++++++++---- tests/test_io/bad/redefining_input.catala_en | 15 +- tests/test_io/bad/using_non_output.catala_en | 7 + .../bad/array_length-empty.catala_en | 17 +-- .../bad/array_length-overlap.catala_en | 17 +-- .../bad/dates_get_year-empty.catala_en | 26 ++-- .../bad/dates_get_year-overlap.catala_en | 17 +-- .../bad/dates_simple-empty.catala_en | 17 +-- .../bad/dates_simple-overlap.catala_en | 17 +-- tests/test_proof/bad/duration-empty.catala_en | 17 +-- .../test_proof/bad/duration-overlap.catala_en | 17 +-- tests/test_proof/bad/enums-empty.catala_en | 17 +-- .../bad/enums-nonbool-empty.catala_en | 17 +-- .../bad/enums-nonbool-overlap.catala_en | 17 +-- tests/test_proof/bad/enums-overlap.catala_en | 17 +-- .../test_proof/bad/enums_inj-empty.catala_en | 17 +-- .../bad/enums_inj-overlap.catala_en | 17 +-- .../test_proof/bad/enums_unit-empty.catala_en | 17 +-- .../bad/enums_unit-overlap.catala_en | 17 +-- .../bad/let_in_condition-empty.catala_en | 15 +- tests/test_proof/bad/money-empty.catala_en | 17 +-- tests/test_proof/bad/money-overlap.catala_en | 17 +-- .../test_proof/bad/no_vars-conflict.catala_en | 17 +-- tests/test_proof/bad/no_vars-empty.catala_en | 17 +-- .../bad/prolala_motivating_example.catala_en | 67 ++++----- .../test_proof/bad/rationals-empty.catala_en | 17 +-- .../bad/rationals-overlap.catala_en | 17 +-- tests/test_proof/bad/sat_solving.catala_en | 33 ++--- tests/test_proof/bad/structs-empty.catala_en | 17 +-- .../test_proof/bad/structs-overlap.catala_en | 17 +-- tests/test_proof/good/array_length.catala_en | 11 +- .../test_proof/good/dates_get_year.catala_en | 11 +- tests/test_proof/good/duration.catala_en | 11 +- tests/test_proof/good/enums-arith.catala_en | 11 +- tests/test_proof/good/enums-nonbool.catala_en | 11 +- tests/test_proof/good/enums.catala_en | 11 +- tests/test_proof/good/enums_inj.catala_en | 11 +- tests/test_proof/good/enums_unit.catala_en | 11 +- tests/test_proof/good/functions.catala_en | 11 +- .../good/let_in_condition.catala_en | 9 +- tests/test_proof/good/money.catala_en | 11 +- tests/test_proof/good/no_vars.catala_en | 9 +- tests/test_proof/good/rationals.catala_en | 11 +- tests/test_proof/good/simple_vars.catala_en | 13 +- tests/test_proof/good/structs.catala_en | 11 +- tests/test_scope/bad/cycle_in_scope.catala_en | 6 +- tests/test_scope/bad/scope.catala_en | 20 +-- .../bad/scope_call_missing.catala_en | 17 +-- .../191_fix_record_name_confusion.catala_en | 32 ++--- tests/test_struct/bad/nested.catala_en | 9 +- tests/test_struct/bad/nested2.catala_en | 10 +- .../good/ambiguous_fields.catala_en | 24 +--- 65 files changed, 402 insertions(+), 920 deletions(-) diff --git a/compiler/desugared/linting.ml b/compiler/desugared/linting.ml index 530aafb1..16d94692 100644 --- a/compiler/desugared/linting.ml +++ b/compiler/desugared/linting.ml @@ -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; diff --git a/tests/test_arithmetic/bad/division_by_zero.catala_en b/tests/test_arithmetic/bad/division_by_zero.catala_en index 0a48801a..32c2929b 100644 --- a/tests/test_arithmetic/bad/division_by_zero.catala_en +++ b/tests/test_arithmetic/bad/division_by_zero.catala_en @@ -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: diff --git a/tests/test_bool/bad/bad_assert.catala_en b/tests/test_bool/bad/bad_assert.catala_en index 2dba3b02..fe95049d 100644 --- a/tests/test_bool/bad/bad_assert.catala_en +++ b/tests/test_bool/bad/bad_assert.catala_en @@ -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: diff --git a/tests/test_date/bad/rounding_option.catala_en b/tests/test_date/bad/rounding_option.catala_en index 12415f13..4430aeb0 100644 --- a/tests/test_date/bad/rounding_option.catala_en +++ b/tests/test_date/bad/rounding_option.catala_en @@ -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 diff --git a/tests/test_date/bad/rounding_option.catala_fr b/tests/test_date/bad/rounding_option.catala_fr index 947a776f..7cbea53d 100644 --- a/tests/test_date/bad/rounding_option.catala_fr +++ b/tests/test_date/bad/rounding_option.catala_fr @@ -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 diff --git a/tests/test_date/bad/uncomparable_duration.catala_en b/tests/test_date/bad/uncomparable_duration.catala_en index d0bc1a7b..8101bad8 100644 --- a/tests/test_date/bad/uncomparable_duration.catala_en +++ b/tests/test_date/bad/uncomparable_duration.catala_en @@ -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: diff --git a/tests/test_default/bad/conflict.catala_en b/tests/test_default/bad/conflict.catala_en index 34a819c7..b9c26328 100644 --- a/tests/test_default/bad/conflict.catala_en +++ b/tests/test_default/bad/conflict.catala_en @@ -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: diff --git a/tests/test_default/bad/empty.catala_en b/tests/test_default/bad/empty.catala_en index a155498f..541d8d82 100644 --- a/tests/test_default/bad/empty.catala_en +++ b/tests/test_default/bad/empty.catala_en @@ -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# ``` diff --git a/tests/test_default/bad/empty_with_rules.catala_en b/tests/test_default/bad/empty_with_rules.catala_en index 0dd26944..c04cefc6 100644 --- a/tests/test_default/bad/empty_with_rules.catala_en +++ b/tests/test_default/bad/empty_with_rules.catala_en @@ -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# ``` diff --git a/tests/test_enum/bad/missing_case.catala_en b/tests/test_enum/bad/missing_case.catala_en index c4338af2..4efbbbaf 100644 --- a/tests/test_enum/bad/missing_case.catala_en +++ b/tests/test_enum/bad/missing_case.catala_en @@ -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: diff --git a/tests/test_exception/bad/exceptions_cycle.catala_en b/tests/test_exception/bad/exceptions_cycle.catala_en index 3258872f..38bbb256 100644 --- a/tests/test_exception/bad/exceptions_cycle.catala_en +++ b/tests/test_exception/bad/exceptions_cycle.catala_en @@ -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: diff --git a/tests/test_exception/bad/self_exception.catala_en b/tests/test_exception/bad/self_exception.catala_en index e53a3052..428dcef6 100644 --- a/tests/test_exception/bad/self_exception.catala_en +++ b/tests/test_exception/bad/self_exception.catala_en @@ -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: diff --git a/tests/test_exception/bad/two_exceptions.catala_en b/tests/test_exception/bad/two_exceptions.catala_en index c188137e..ac11f22f 100644 --- a/tests/test_exception/bad/two_exceptions.catala_en +++ b/tests/test_exception/bad/two_exceptions.catala_en @@ -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: diff --git a/tests/test_func/good/context_func.catala_en b/tests/test_func/good/context_func.catala_en index e74a8e80..d2846b48 100644 --- a/tests/test_func/good/context_func.catala_en +++ b/tests/test_func/good/context_func.catala_en @@ -2,7 +2,7 @@ ```catala declaration scope A: - 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# ``` diff --git a/tests/test_io/bad/redefining_input.catala_en b/tests/test_io/bad/redefining_input.catala_en index ca484f67..51dd5665 100644 --- a/tests/test_io/bad/redefining_input.catala_en +++ b/tests/test_io/bad/redefining_input.catala_en @@ -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: diff --git a/tests/test_io/bad/using_non_output.catala_en b/tests/test_io/bad/using_non_output.catala_en index 09019c0f..b304f32b 100644 --- a/tests/test_io/bad/using_non_output.catala_en +++ b/tests/test_io/bad/using_non_output.catala_en @@ -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: diff --git a/tests/test_proof/bad/array_length-empty.catala_en b/tests/test_proof/bad/array_length-empty.catala_en index 74e1d66f..72066f25 100644 --- a/tests/test_proof/bad/array_length-empty.catala_en +++ b/tests/test_proof/bad/array_length-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/array_length-overlap.catala_en b/tests/test_proof/bad/array_length-overlap.catala_en index 0d56b860..981b663e 100644 --- a/tests/test_proof/bad/array_length-overlap.catala_en +++ b/tests/test_proof/bad/array_length-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/dates_get_year-empty.catala_en b/tests/test_proof/bad/dates_get_year-empty.catala_en index 4abfabb2..a9932432 100644 --- a/tests/test_proof/bad/dates_get_year-empty.catala_en +++ b/tests/test_proof/bad/dates_get_year-empty.catala_en @@ -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# ``` diff --git a/tests/test_proof/bad/dates_get_year-overlap.catala_en b/tests/test_proof/bad/dates_get_year-overlap.catala_en index 32e710d9..dca3c26a 100644 --- a/tests/test_proof/bad/dates_get_year-overlap.catala_en +++ b/tests/test_proof/bad/dates_get_year-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/dates_simple-empty.catala_en b/tests/test_proof/bad/dates_simple-empty.catala_en index 1781d0c1..21c8ee2e 100644 --- a/tests/test_proof/bad/dates_simple-empty.catala_en +++ b/tests/test_proof/bad/dates_simple-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/dates_simple-overlap.catala_en b/tests/test_proof/bad/dates_simple-overlap.catala_en index 69b1ea1f..ad495241 100644 --- a/tests/test_proof/bad/dates_simple-overlap.catala_en +++ b/tests/test_proof/bad/dates_simple-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/duration-empty.catala_en b/tests/test_proof/bad/duration-empty.catala_en index 0928ffc8..ac710b8a 100644 --- a/tests/test_proof/bad/duration-empty.catala_en +++ b/tests/test_proof/bad/duration-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/duration-overlap.catala_en b/tests/test_proof/bad/duration-overlap.catala_en index 338abc63..e3bad00d 100644 --- a/tests/test_proof/bad/duration-overlap.catala_en +++ b/tests/test_proof/bad/duration-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/enums-empty.catala_en b/tests/test_proof/bad/enums-empty.catala_en index db0b70d5..81d1ca84 100644 --- a/tests/test_proof/bad/enums-empty.catala_en +++ b/tests/test_proof/bad/enums-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/enums-nonbool-empty.catala_en b/tests/test_proof/bad/enums-nonbool-empty.catala_en index e9fc7a5b..5e19edb3 100644 --- a/tests/test_proof/bad/enums-nonbool-empty.catala_en +++ b/tests/test_proof/bad/enums-nonbool-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/enums-nonbool-overlap.catala_en b/tests/test_proof/bad/enums-nonbool-overlap.catala_en index 57b90567..abf9f561 100644 --- a/tests/test_proof/bad/enums-nonbool-overlap.catala_en +++ b/tests/test_proof/bad/enums-nonbool-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/enums-overlap.catala_en b/tests/test_proof/bad/enums-overlap.catala_en index 7b8ac788..89e3ef2f 100644 --- a/tests/test_proof/bad/enums-overlap.catala_en +++ b/tests/test_proof/bad/enums-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/enums_inj-empty.catala_en b/tests/test_proof/bad/enums_inj-empty.catala_en index 19e52648..b6b2d602 100644 --- a/tests/test_proof/bad/enums_inj-empty.catala_en +++ b/tests/test_proof/bad/enums_inj-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/enums_inj-overlap.catala_en b/tests/test_proof/bad/enums_inj-overlap.catala_en index fd340294..1f6bf5ae 100644 --- a/tests/test_proof/bad/enums_inj-overlap.catala_en +++ b/tests/test_proof/bad/enums_inj-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/enums_unit-empty.catala_en b/tests/test_proof/bad/enums_unit-empty.catala_en index 88675f29..6a28690c 100644 --- a/tests/test_proof/bad/enums_unit-empty.catala_en +++ b/tests/test_proof/bad/enums_unit-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/enums_unit-overlap.catala_en b/tests/test_proof/bad/enums_unit-overlap.catala_en index f52f241e..6e60e55b 100644 --- a/tests/test_proof/bad/enums_unit-overlap.catala_en +++ b/tests/test_proof/bad/enums_unit-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/let_in_condition-empty.catala_en b/tests/test_proof/bad/let_in_condition-empty.catala_en index a8822196..341e041e 100644 --- a/tests/test_proof/bad/let_in_condition-empty.catala_en +++ b/tests/test_proof/bad/let_in_condition-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/money-empty.catala_en b/tests/test_proof/bad/money-empty.catala_en index 80bfb57b..5de7fe03 100644 --- a/tests/test_proof/bad/money-empty.catala_en +++ b/tests/test_proof/bad/money-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/money-overlap.catala_en b/tests/test_proof/bad/money-overlap.catala_en index 2078af7a..aa60442b 100644 --- a/tests/test_proof/bad/money-overlap.catala_en +++ b/tests/test_proof/bad/money-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/no_vars-conflict.catala_en b/tests/test_proof/bad/no_vars-conflict.catala_en index 1eb287ff..178a790c 100644 --- a/tests/test_proof/bad/no_vars-conflict.catala_en +++ b/tests/test_proof/bad/no_vars-conflict.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/no_vars-empty.catala_en b/tests/test_proof/bad/no_vars-empty.catala_en index 795f0884..6de8f150 100644 --- a/tests/test_proof/bad/no_vars-empty.catala_en +++ b/tests/test_proof/bad/no_vars-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/prolala_motivating_example.catala_en b/tests/test_proof/bad/prolala_motivating_example.catala_en index 93b06785..1136b06b 100644 --- a/tests/test_proof/bad/prolala_motivating_example.catala_en +++ b/tests/test_proof/bad/prolala_motivating_example.catala_en @@ -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# ``` diff --git a/tests/test_proof/bad/rationals-empty.catala_en b/tests/test_proof/bad/rationals-empty.catala_en index effa44c5..528f013f 100644 --- a/tests/test_proof/bad/rationals-empty.catala_en +++ b/tests/test_proof/bad/rationals-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/rationals-overlap.catala_en b/tests/test_proof/bad/rationals-overlap.catala_en index 27dee7f1..3f7a92ec 100644 --- a/tests/test_proof/bad/rationals-overlap.catala_en +++ b/tests/test_proof/bad/rationals-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/sat_solving.catala_en b/tests/test_proof/bad/sat_solving.catala_en index c52c6617..7b5ce646 100644 --- a/tests/test_proof/bad/sat_solving.catala_en +++ b/tests/test_proof/bad/sat_solving.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/structs-empty.catala_en b/tests/test_proof/bad/structs-empty.catala_en index 5a2faf4f..4f2b1cc0 100644 --- a/tests/test_proof/bad/structs-empty.catala_en +++ b/tests/test_proof/bad/structs-empty.catala_en @@ -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. ``` diff --git a/tests/test_proof/bad/structs-overlap.catala_en b/tests/test_proof/bad/structs-overlap.catala_en index 16cffaf5..5bd9d0c4 100644 --- a/tests/test_proof/bad/structs-overlap.catala_en +++ b/tests/test_proof/bad/structs-overlap.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/array_length.catala_en b/tests/test_proof/good/array_length.catala_en index d4047d91..55c4cb8a 100644 --- a/tests/test_proof/good/array_length.catala_en +++ b/tests/test_proof/good/array_length.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/dates_get_year.catala_en b/tests/test_proof/good/dates_get_year.catala_en index d3abf4fd..4c2c385c 100644 --- a/tests/test_proof/good/dates_get_year.catala_en +++ b/tests/test_proof/good/dates_get_year.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/duration.catala_en b/tests/test_proof/good/duration.catala_en index e2295f58..01a2e840 100644 --- a/tests/test_proof/good/duration.catala_en +++ b/tests/test_proof/good/duration.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/enums-arith.catala_en b/tests/test_proof/good/enums-arith.catala_en index 1f5970a2..4fe972ee 100644 --- a/tests/test_proof/good/enums-arith.catala_en +++ b/tests/test_proof/good/enums-arith.catala_en @@ -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: diff --git a/tests/test_proof/good/enums-nonbool.catala_en b/tests/test_proof/good/enums-nonbool.catala_en index dd8a307a..227d7d4e 100644 --- a/tests/test_proof/good/enums-nonbool.catala_en +++ b/tests/test_proof/good/enums-nonbool.catala_en @@ -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: diff --git a/tests/test_proof/good/enums.catala_en b/tests/test_proof/good/enums.catala_en index 6125d0d1..dbd08291 100644 --- a/tests/test_proof/good/enums.catala_en +++ b/tests/test_proof/good/enums.catala_en @@ -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: diff --git a/tests/test_proof/good/enums_inj.catala_en b/tests/test_proof/good/enums_inj.catala_en index 31749c42..4e2c7b46 100644 --- a/tests/test_proof/good/enums_inj.catala_en +++ b/tests/test_proof/good/enums_inj.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/enums_unit.catala_en b/tests/test_proof/good/enums_unit.catala_en index e88591c5..d74268a2 100644 --- a/tests/test_proof/good/enums_unit.catala_en +++ b/tests/test_proof/good/enums_unit.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/functions.catala_en b/tests/test_proof/good/functions.catala_en index 88eccebb..c4de65b4 100644 --- a/tests/test_proof/good/functions.catala_en +++ b/tests/test_proof/good/functions.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/let_in_condition.catala_en b/tests/test_proof/good/let_in_condition.catala_en index 1cb2a5a9..a37062d6 100644 --- a/tests/test_proof/good/let_in_condition.catala_en +++ b/tests/test_proof/good/let_in_condition.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/money.catala_en b/tests/test_proof/good/money.catala_en index 990a0c0c..039fb1dd 100644 --- a/tests/test_proof/good/money.catala_en +++ b/tests/test_proof/good/money.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/no_vars.catala_en b/tests/test_proof/good/no_vars.catala_en index 5c6f309d..93244be9 100644 --- a/tests/test_proof/good/no_vars.catala_en +++ b/tests/test_proof/good/no_vars.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/rationals.catala_en b/tests/test_proof/good/rationals.catala_en index 83483784..11c66a40 100644 --- a/tests/test_proof/good/rationals.catala_en +++ b/tests/test_proof/good/rationals.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/simple_vars.catala_en b/tests/test_proof/good/simple_vars.catala_en index c32fc910..211082b1 100644 --- a/tests/test_proof/good/simple_vars.catala_en +++ b/tests/test_proof/good/simple_vars.catala_en @@ -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. ``` diff --git a/tests/test_proof/good/structs.catala_en b/tests/test_proof/good/structs.catala_en index 7d60b0cc..30ae8e7d 100644 --- a/tests/test_proof/good/structs.catala_en +++ b/tests/test_proof/good/structs.catala_en @@ -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. ``` diff --git a/tests/test_scope/bad/cycle_in_scope.catala_en b/tests/test_scope/bad/cycle_in_scope.catala_en index 41348c49..423116b8 100644 --- a/tests/test_scope/bad/cycle_in_scope.catala_en +++ b/tests/test_scope/bad/cycle_in_scope.catala_en @@ -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 diff --git a/tests/test_scope/bad/scope.catala_en b/tests/test_scope/bad/scope.catala_en index 341ecbbf..2fd80e41 100644 --- a/tests/test_scope/bad/scope.catala_en +++ b/tests/test_scope/bad/scope.catala_en @@ -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: diff --git a/tests/test_scope/bad/scope_call_missing.catala_en b/tests/test_scope/bad/scope_call_missing.catala_en index 59edf133..46fd4b20 100644 --- a/tests/test_scope/bad/scope_call_missing.catala_en +++ b/tests/test_scope/bad/scope_call_missing.catala_en @@ -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# ``` diff --git a/tests/test_scope/good/191_fix_record_name_confusion.catala_en b/tests/test_scope/good/191_fix_record_name_confusion.catala_en index 35afc652..e3cc4b66 100644 --- a/tests/test_scope/good/191_fix_record_name_confusion.catala_en +++ b/tests/test_scope/good/191_fix_record_name_confusion.catala_en @@ -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_} ``` diff --git a/tests/test_struct/bad/nested.catala_en b/tests/test_struct/bad/nested.catala_en index 5dca2ac4..f5d6cbcb 100644 --- a/tests/test_struct/bad/nested.catala_en +++ b/tests/test_struct/bad/nested.catala_en @@ -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: diff --git a/tests/test_struct/bad/nested2.catala_en b/tests/test_struct/bad/nested2.catala_en index 3dee6f91..f3e09dbd 100644 --- a/tests/test_struct/bad/nested2.catala_en +++ b/tests/test_struct/bad/nested2.catala_en @@ -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? diff --git a/tests/test_struct/good/ambiguous_fields.catala_en b/tests/test_struct/good/ambiguous_fields.catala_en index e40f9e38..d73190c0 100644 --- a/tests/test_struct/good/ambiguous_fields.catala_en +++ b/tests/test_struct/good/ambiguous_fields.catala_en @@ -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 ```