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

Fix default optimisation

Browse Source
This commit is contained in:
Denis Merigoux 2023-12-18 14:42:58 +01:00
parent 10d8c0b19f
commit 35f829cd65
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
10 changed files with 107 additions and 272 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

90
compiler/scalc/to_c.ml
View File

@ -598,58 +598,62 @@ let rec format_statement
| SLocalDef { name; _ }, _ | SLocalInit { name; _ }, _ -> Mark.remove name
| _ -> failwith "should not happen"
in
Format.fprintf fmt "@[<hov 2>%a = {%a_%a,@ {none_cons: NULL}};@]@,"
(format_typ ctx (fun fmt -> format_var fmt exception_acc_var))
return_typ format_enum_name e_name format_enum_cons_name none_cons;
Format.fprintf fmt "%a;@,"
(format_typ ctx (fun fmt -> format_var fmt exception_current))
return_typ;
Format.fprintf fmt "char %a = 0;@," format_var exception_conflict;
List.iter
(fun except ->
Format.fprintf fmt
"%a = %a;@,\
@[<v 2>if (%a.code == %a_%a) {@,\
@[<v 2>if (%a.code == %a_%a) {@,\
%a = 1;@]@,\
@[<v 2>} else {@,\
%a = %a;@]@,\
}@]@,\
}@,"
format_var exception_current (format_expression ctx) except format_var
exception_current format_enum_name e_name format_enum_cons_name
some_cons format_var exception_acc_var format_enum_name e_name
format_enum_cons_name some_cons format_var exception_conflict
format_var exception_acc_var format_var exception_current)
exceptions;
if exceptions <> [] then begin
Format.fprintf fmt "@[<hov 2>%a = {%a_%a,@ {none_cons: NULL}};@]@,"
(format_typ ctx (fun fmt -> format_var fmt exception_acc_var))
return_typ format_enum_name e_name format_enum_cons_name none_cons;
Format.fprintf fmt "%a;@,"
(format_typ ctx (fun fmt -> format_var fmt exception_current))
return_typ;
Format.fprintf fmt "char %a = 0;@," format_var exception_conflict;
List.iter
(fun except ->
Format.fprintf fmt
"%a = %a;@,\
@[<v 2>if (%a.code == %a_%a) {@,\
@[<v 2>if (%a.code == %a_%a) {@,\
%a = 1;@]@,\
@[<v 2>} else {@,\
%a = %a;@]@,\
}@]@,\
}@,"
format_var exception_current (format_expression ctx) except
format_var exception_current format_enum_name e_name
format_enum_cons_name some_cons format_var exception_acc_var
format_enum_name e_name format_enum_cons_name some_cons format_var
exception_conflict format_var exception_acc_var format_var
exception_current)
exceptions;
Format.fprintf fmt
"@[<v 2>if (%a) {@,\
catala_fatal_error_raised.code = catala_conflict;@,\
catala_fatal_error_raised.position.filename = \"%s\";@,\
catala_fatal_error_raised.position.start_line = %d;@,\
catala_fatal_error_raised.position.start_column = %d;@,\
catala_fatal_error_raised.position.end_line = %d;@,\
catala_fatal_error_raised.position.end_column = %d;@,\
longjmp(catala_fatal_error_jump_buffer, 0);@]@,\
}@,"
format_var exception_conflict (Pos.get_file pos)
(Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos);
Format.fprintf fmt
"@[<v 2>if (%a.code == %a_%a) {@,%a = %a;@]@,@[<v 2>} else {@,"
format_var exception_acc_var format_enum_name e_name
format_enum_cons_name some_cons format_var variable_defined_in_cons
format_var exception_acc_var
end;
Format.fprintf fmt
"@[<v 2>if (%a) {@,\
catala_fatal_error_raised.code = catala_conflict;@,\
catala_fatal_error_raised.position.filename = \"%s\";@,\
catala_fatal_error_raised.position.start_line = %d;@,\
catala_fatal_error_raised.position.start_column = %d;@,\
catala_fatal_error_raised.position.end_line = %d;@,\
catala_fatal_error_raised.position.end_column = %d;@,\
longjmp(catala_fatal_error_jump_buffer, 0);@]@,\
}@,"
format_var exception_conflict (Pos.get_file pos) (Pos.get_start_line pos)
(Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos);
Format.fprintf fmt
"@[<v 2>if (%a.code == %a_%a) {@,\
%a = %a;@]@,\
@[<v 2>} else {@,\
@[<v 2>if (%a) {@,\
%a@]@,\
@[<v 2>} else {@,\
%a.code = %a_%a;@,\
%a.payload.none_cons = NULL;@]@,\
}@]@,\
}"
format_var exception_acc_var format_enum_name e_name format_enum_cons_name
some_cons format_var variable_defined_in_cons format_var exception_acc_var
(format_expression ctx) just (format_block ctx) cons format_var
variable_defined_in_cons format_enum_name e_name format_enum_cons_name
none_cons format_var variable_defined_in_cons
none_cons format_var variable_defined_in_cons;
if exceptions <> [] then Format.fprintf fmt "@]@,}"
and format_block (ctx : decl_ctx) (fmt : Format.formatter) (b : block) : unit =
Format.pp_print_list

42
compiler/shared_ast/optimizations.ml
View File

@ -213,26 +213,7 @@ let rec optimize_expr :
| EStructAccess { name; field; e = EStruct { name = name1; fields }, _ }
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 *) ->
(* No exceptions, always true *)
Mark.remove cons
| EErrorOnEmpty
( EDefault
{
excepts =
[
( EDefault { excepts = []; just = ELit (LBool true), _; cons },
_ );
];
_;
},
_ ) ->
(* Single, always true exception *)
Mark.remove cons
| EErrorOnEmpty (EPureDefault (e, _), _) -> e
| EDefault { excepts; just; cons } -> (
(* TODO: mechanically prove each of these optimizations correct *)
let excepts =
@ -257,13 +238,10 @@ let rec optimize_expr :
assert false
else
match excepts, just with
| ( [
( (EDefault { excepts = []; just = ELit (LBool true), _; _ } as dft),
_ );
],
_ ) ->
(* Single exception with condition [true] *)
dft
| [(EDefault { excepts = []; just = ELit (LBool true), _; cons }, _)], _
->
(* No exceptions with condition [true] *)
Mark.remove cons
| ( [],
( ( ELit (LBool false)
| EApp
@ -274,6 +252,16 @@ let rec optimize_expr :
_ ) ) ->
(* No exceptions and condition false *)
EEmptyError
| ( [except],
( ( ELit (LBool false)
| EApp
{
f = EOp { op = Log _; _ }, _;
args = [(ELit (LBool false), _)];
} ),
_ ) ) ->
(* Single exception and condition false *)
Mark.remove except
| excepts, just -> EDefault { excepts; just; cons })
| EIfThenElse
{

6
tests/test_backends/simple.catala_en
View File

@ -20,8 +20,4 @@ scope Baz:
exception definition b under condition
a with pattern No
consequence equals 42.0
exception definition b under condition
a with pattern No
consequence equals 43.0
```
```

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

@ -46,34 +46,17 @@ 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
let code_and_env :
((closure_env, integer) → integer * closure_env) =
f
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) =
f
in
code_and_env.0 code_and_env.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: collection integer}): S {y: integer} =
let get x : collection 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)}

26
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; }
@ -60,20 +54,10 @@ let scope T (T_in: T_in): T {y: integer} =
result.f
in
let set y : integer =
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) →
ESome
let code_and_env :
((closure_env, integer) → integer * closure_env) =
s.f
in
code_and_env.0 code_and_env.1 2))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
let code_and_env : ((closure_env, integer) → integer * closure_env) =
s.f
in
code_and_env.0 code_and_env.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 {
@ -163,16 +149,7 @@ let scope Foo
code_and_env.0 code_and_env.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
@ -182,51 +159,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

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))
```