CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 00:15:39 +03:00
Code Issues Projects Releases Wiki Activity

Optimise away trivially-true errors-on-empty

Browse Source
This commit is contained in:
Louis Gesbert 2023-12-19 16:04:59 +01:00
parent ea4e191f27
commit fb51f58261
9 changed files with 50 additions and 198 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
compiler/shared_ast/optimizations.ml
View File

@ -215,12 +215,15 @@ let rec optimize_expr :
when StructName.equal name name1 ->
Mark.remove (StructField.Map.find field fields)
| EErrorOnEmpty
(EDefault { excepts = []; just = ELit (LBool true), _; cons }, _)
when false
(* FIXME: this optimisation is correct and useful, but currently
breaks expectations of the without-exceptions backend *) ->
( EDefault
{
excepts = [];
just = ELit (LBool true), _;
cons = EPureDefault e, _;
},
_ ) ->
(* No exceptions, always true *)
Mark.remove cons
Mark.remove e
| EErrorOnEmpty
( EDefault
{

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

@ -46,29 +46,13 @@ type S = { z: integer; }
let topval closure_f : (closure_env, integer) → integer =
λ (env: closure_env) (y: integer) →
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) → ESome if (from_closure_env env).0 then y else - y))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
if (from_closure_env env).0 then y else - y
let scope S (S_in: S_in {x_in: bool}): S {z: integer} =
let get x : bool = S_in.x_in in
let set f : ((closure_env, integer) → integer * closure_env) =
(closure_f, to_closure_env (x))
in
let set z : integer =
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) → ESome (f.0 f.1 -1)))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
in
let set z : integer = f.0 f.1 -1 in
return { S z = z; }
```

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

@ -41,21 +41,12 @@ $ catala Lcalc -s S --avoid-exceptions -O --closure-conversion
let scope S (S_in: S_in {x_in: list of integer}): S {y: integer} =
let get x : list of integer = S_in.x_in in
let set y : integer =
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) →
ESome
(reduce
(λ (potential_max_1: integer) (potential_max_2: integer) →
if potential_max_1 < potential_max_2 then potential_max_1
else potential_max_2)
-1
x)))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
reduce
(λ (potential_max_1: integer) (potential_max_2: integer) →
if potential_max_1 < potential_max_2 then potential_max_1
else potential_max_2)
-1
x
in
return { S y = y; }
```

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

@ -44,14 +44,7 @@ type S = { f: ((closure_env, integer) → integer * closure_env); }
let topval closure_f : (closure_env, integer) → integer =
λ (env: closure_env) (y: integer) →
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) → ESome if (from_closure_env env).0 then y else - y))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
if (from_closure_env env).0 then y else - y
let scope S
(S_in: S_in {x_in: bool})
: S {f: ((closure_env, integer) → integer * closure_env)}

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

@ -45,13 +45,7 @@ Invariant Dcalc__Invariants.invariant_default_no_arrow
```catala-test-inline
$ catala Lcalc -s T --avoid-exceptions -O --closure-conversion
let scope T (T_in: T_in): T {y: integer} =
let sub_set s.x : bool =
match
(handle_default_opt [] (λ (_: unit) → true) (λ (_: unit) → ESome false))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
in
let sub_set s.x : bool = false in
let call result : S {f: ((closure_env, integer) → integer * closure_env)}
=
S { S_in x_in = s.x; }
@ -59,16 +53,7 @@ let scope T (T_in: T_in): T {y: integer} =
let sub_get s.f : ((closure_env, integer) → integer * closure_env) =
result.f
in
let set y : integer =
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) → ESome (s.f.0 s.f.1 2)))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
in
let set y : integer = s.f.0 s.f.1 2 in
return { T y = y; }
```

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

@ -94,14 +94,7 @@ type Foo = { z: integer; }
let topval closure_y : (closure_env, integer) → integer =
λ (env: closure_env) (z: integer) →
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) → ESome ((from_closure_env env).0 + z)))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
(from_closure_env env).0 + z
let scope SubFoo1
(SubFoo1_in: SubFoo1_in {x_in: integer})
: SubFoo1 {
@ -117,14 +110,7 @@ let scope SubFoo1
let topval closure_y : (closure_env, integer) → integer =
λ (env: closure_env) (z: integer) →
let env1 : (integer * integer) = from_closure_env env in
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) → ESome (env1.1 + env1.0 + z)))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
((env1.1 + env1.0 + z))
let scope SubFoo2
(SubFoo2_in: SubFoo2_in {x1_in: integer; x2_in: integer})
: SubFoo2 {
@ -160,16 +146,7 @@ let scope Foo
(handle_default_opt
[b.0 b.1 ()]
(λ (_: unit) → true)
(λ (_: unit) →
ESome
(match
(handle_default_opt
[]
(λ (_1: unit) → true)
(λ (_1: unit) → ESome true))
with
| ENone _1 → raise NoValueProvided
| ESome arg → arg)))
(λ (_: unit) → ESome true))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
@ -179,51 +156,26 @@ let scope Foo
r: ((closure_env, integer) → integer * closure_env);
q: integer
} =
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) →
ESome
if b then
let f : SubFoo1 =
let result : SubFoo1 = SubFoo1 { SubFoo1_in x_in = 10; } in
{ SubFoo1
x = result.x;
y = (closure_r, to_closure_env (result));
}
in
{ Result r = f.y; q = f.x; }
else
let f : SubFoo2 =
let result : SubFoo2 =
SubFoo2 { SubFoo2_in x1_in = 10; x2_in = 10; }
in
{ SubFoo2
x1 = result.x1;
y = (closure_r, to_closure_env (result));
}
in
{ Result r = f.y; q = f.x1; }))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
if b then
let f : SubFoo1 =
let result : SubFoo1 = SubFoo1 { SubFoo1_in x_in = 10; } in
{ SubFoo1 x = result.x; y = (closure_r, to_closure_env (result)); }
in
{ Result r = f.y; q = f.x; }
else
let f : SubFoo2 =
let result : SubFoo2 =
SubFoo2 { SubFoo2_in x1_in = 10; x2_in = 10; }
in
{ SubFoo2 x1 = result.x1; y = (closure_r, to_closure_env (result)); }
in
{ Result r = f.y; q = f.x1; }
in
let set z : integer =
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) →
ESome
(let code_and_env :
((closure_env, integer) → integer * closure_env) =
r.r
in
code_and_env.0 code_and_env.1 1)))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
let code_and_env : ((closure_env, integer) → integer * closure_env) =
r.r
in
code_and_env.0 code_and_env.1 1
in
return { Foo z = z; }

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

@ -69,33 +69,13 @@ end
let scope_a (scope_a_in: ScopeA_in.t) : ScopeA.t =
let a_: bool =
try
(handle_default
{filename = ""; start_line=0; start_column=1;
end_line=0; end_column=1; law_headings=[]} ([||])
(fun (_: unit) -> true) (fun (_: unit) -> true))
with
EmptyError -> (raise (NoValueProvided
{filename = "tests/test_scope/good/191_fix_record_name_confusion.catala_en";
start_line=5; start_column=10; end_line=5; end_column=11;
law_headings=["Article"]})) in
let a_: bool = true in
{ScopeA.a = a_}
let scope_b (scope_b_in: ScopeB_in.t) : ScopeB.t =
let result_: ScopeA.t = scope_a (()) in
let scope_a_dot_a_: bool = result_.ScopeA.a in
let a_: bool =
try
(handle_default
{filename = ""; start_line=0; start_column=1;
end_line=0; end_column=1; law_headings=[]} ([||])
(fun (_: unit) -> true) (fun (_: unit) -> 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=10; end_line=8; end_column=11;
law_headings=["Article"]})) in
let a_: bool = scope_a_dot_a_ in
{ScopeB.a = a_}
Generating entry points for scopes: ScopeA ScopeB

8
tests/test_scope/good/scope_call3.catala_en
View File

@ -57,7 +57,7 @@ $ catala Interpret -t -s HousingComputation --debug
[DEBUG] Translating to default calculus...
[DEBUG] Typechecking again...
[DEBUG] Starting interpretation...
[LOG] ≔ HousingComputation.f: λ (x_90: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨(let result_91 : RentComputation = (#{→ RentComputation.direct} (λ (RentComputation_in_92: RentComputation_in) → let g_93 : integer → integer = #{≔ RentComputation.g} (λ (x1_94: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_94 +! 1⟩⟩ | false ⊢ ∅ ⟩) in let f_95 : integer → integer = #{≔ RentComputation.f} (λ (x1_96: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} g_93) #{≔ RentComputation.g.input0} (x1_96 +! 1)⟩⟩ | false ⊢ ∅ ⟩) in { RentComputation f = f_95; })) #{≔ RentComputation.direct.input} {RentComputation_in} in let result1_97 : RentComputation = { RentComputation f = λ (param0_98: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} result_91.f) #{≔ RentComputation.f.input0} param0_98; } in #{← RentComputation.direct} #{≔ RentComputation.direct.output} if #{☛ RentComputation.direct.output} true then result1_97 else result1_97).f x_90⟩⟩ | false ⊢ ∅ ⟩
[LOG] ≔ HousingComputation.f: λ (x_76: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨(let result_77 : RentComputation = (#{→ RentComputation.direct} (λ (RentComputation_in_78: RentComputation_in) → let g_79 : integer → integer = #{≔ RentComputation.g} (λ (x1_80: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_80 +! 1⟩⟩ | false ⊢ ∅ ⟩) in let f_81 : integer → integer = #{≔ RentComputation.f} (λ (x1_82: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} g_79) #{≔ RentComputation.g.input0} (x1_82 +! 1)⟩⟩ | false ⊢ ∅ ⟩) in { RentComputation f = f_81; })) #{≔ RentComputation.direct.input} {RentComputation_in} in let result1_83 : RentComputation = { RentComputation f = λ (param0_84: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} result_77.f) #{≔ RentComputation.f.input0} param0_84; } in #{← RentComputation.direct} #{≔ RentComputation.direct.output} if #{☛ RentComputation.direct.output} true then result1_83 else result1_83).f x_76⟩⟩ | false ⊢ ∅ ⟩
[LOG] ☛ Definition applied:
┌─⯈ tests/test_scope/good/scope_call3.catala_en:8.14-8.20:
└─┐
@ -72,14 +72,14 @@ $ catala Interpret -t -s HousingComputation --debug
│ ‾
[LOG] → RentComputation.direct
[LOG] ≔ RentComputation.direct.input: {RentComputation_in}
[LOG] ≔ RentComputation.g: λ (x_99: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x_99 +! 1⟩⟩ | false ⊢ ∅ ⟩
[LOG] ≔ RentComputation.f: λ (x_100: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_101: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_101 +! 1⟩⟩ | false ⊢ ∅ ⟩)) #{≔ RentComputation.g.input0} (x_100 +! 1)⟩⟩ | false ⊢ ∅ ⟩
[LOG] ≔ RentComputation.g: λ (x_85: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x_85 +! 1⟩⟩ | false ⊢ ∅ ⟩
[LOG] ≔ RentComputation.f: λ (x_86: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_87: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_87 +! 1⟩⟩ | false ⊢ ∅ ⟩)) #{≔ RentComputation.g.input0} (x_86 +! 1)⟩⟩ | false ⊢ ∅ ⟩
[LOG] ☛ Definition applied:
┌─⯈ tests/test_scope/good/scope_call3.catala_en:7.29-7.54:
└─┐
7 │ definition f of x equals (output of RentComputation).f of x
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
[LOG] ≔ RentComputation.direct.output: { RentComputation f = λ (param0_102: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} { RentComputation f = λ (x_103: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_104: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_104 +! 1⟩⟩ | false ⊢ ∅ ⟩)) #{≔ RentComputation.g.input0} (x_103 +! 1)⟩⟩ | false ⊢ ∅ ⟩; }.f) #{≔ RentComputation.f.input0} param0_102; }
[LOG] ≔ RentComputation.direct.output: { RentComputation f = λ (param0_88: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} { RentComputation f = λ (x_89: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_90: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_90 +! 1⟩⟩ | false ⊢ ∅ ⟩)) #{≔ RentComputation.g.input0} (x_89 +! 1)⟩⟩ | false ⊢ ∅ ⟩; }.f) #{≔ RentComputation.f.input0} param0_88; }
[LOG] ← RentComputation.direct
[LOG] → RentComputation.f
[LOG] ≔ RentComputation.f.input0: 1

44
tests/test_scope/good/scope_call4.catala_en
View File

@ -102,44 +102,8 @@ $ catala Interpret_Lcalc -s RentComputation --avoid-exceptions --optimize --debu
[DEBUG] Starting interpretation...
[DEBUG] End of interpretation
[RESULT] Computation successful! Results:
[RESULT]
f1 = λ (x: integer) →
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) →
ESome
(let x1 : integer = x + 1 in
match
(handle_default_opt
[]
(λ (_1: unit) → true)
(λ (_1: unit) → ESome (x1 + 1)))
with
| ENone _1 → raise NoValueProvided
| ESome arg → arg)))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
[RESULT]
f2 = λ (x: integer) →
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) →
ESome
(let x1 : integer = x + 1 in
match
(handle_default_opt
[]
(λ (_1: unit) → true)
(λ (_1: unit) → ESome (x1 + 1)))
with
| ENone _1 → raise NoValueProvided
| ESome arg → arg)))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
[RESULT] f1 = λ (x: integer) → let x1 : integer = x + 1 in
((x1 + 1))
[RESULT] f2 = λ (x: integer) → let x1 : integer = x + 1 in
((x1 + 1))
```