Small optimisations (#553)

This commit is contained in:
Louis Gesbert 2023-12-19 17:17:36 +01:00 committed by GitHub
commit 50730ab8ff
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 81 additions and 232 deletions

View File

@ -802,8 +802,7 @@ and partially_evaluate_expr_for_assertion_failure_message :
Mark.get e )
| _ -> evaluate_expr ctx lang e
(* Typing shenanigan to add custom terms to the AST type. This is an identity
and could be optimised into [Obj.magic]. *)
(* Typing shenanigan to add custom terms to the AST type. *)
let addcustom e =
let rec f :
type c d e.
@ -824,7 +823,16 @@ let addcustom e =
Expr.map ~f e
| _ -> .
in
Expr.unbox (f e)
let open struct
external id :
(('d, 'e, 'c) interpr_kind, 't) gexpr ->
(('d, 'e, yes) interpr_kind, 't) gexpr = "%identity"
end in
if false then Expr.unbox (f e)
(* We keep the implementation as a typing proof, but bypass the AST
traversal for performance. Note that it's not completely 1-1 since the
traversal would do a reboxing of all bound variables *)
else id e
let delcustom e =
let rec f :
@ -846,6 +854,9 @@ let delcustom e =
Expr.map ~f e
| _ -> .
in
(* /!\ don't be tempted to use the same trick here, the function does one
thing: validate at runtime that the term does not contain [ECustom]
nodes. *)
Expr.unbox (f e)
let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list

View File

@ -207,19 +207,23 @@ let rec optimize_expr :
in
EMatch { e = arg; cases; name = n1 }
| EApp { f = EAbs { binder; _ }, _; args }
when binder_vars_used_at_most_once binder ->
(* beta reduction when variables not used. *)
when binder_vars_used_at_most_once binder
|| List.for_all (function EVar _, _ -> true | _ -> false) args ->
(* beta reduction when variables not used, and for variable aliases *)
Mark.remove (Bindlib.msubst binder (List.map fst args |> Array.of_list))
| 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 *) ->
( EDefault
{
excepts = [];
just = ELit (LBool true), _;
cons = EPureDefault e, _;
},
_ ) ->
(* No exceptions, always true *)
Mark.remove cons
Mark.remove e
| EErrorOnEmpty
( EDefault
{

View File

@ -686,7 +686,7 @@ module ExprGen (C : EXPR_PARAM) = struct
StructField.format field
| EInj { e; cons; _ } ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]" EnumConstructor.format cons
(rhs exprc) e
(paren ~rhs:false exprc) e
| EMatch { e; cases; _ } ->
Format.fprintf fmt "@[<v 0>@[<hv 2>%a@ %a@;<1 -2>%a@]@ %a@]" keyword
"match" (lhs exprc) e keyword "with"

View File

@ -46,35 +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
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
in
let set z : integer = f.0 f.1 -1 in
return { S z = z; }
```

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; }
```
@ -83,18 +74,18 @@ let scope S (S_in: S_in {x_in: list of integer}): S {y: integer} =
(λ (_: unit) → true)
(λ (_: unit) →
ESome
reduce
(λ (potential_max_1: integer) (potential_max_2: integer) →
if
(let potential_max : integer = potential_max_1 in
potential_max)
< let potential_max : integer = potential_max_2 in
potential_max
then
potential_max_1
else potential_max_2)
-1
x)
(reduce
(λ (potential_max_1: integer) (potential_max_2: integer) →
if
(let potential_max : integer = potential_max_1 in
potential_max)
< let potential_max : integer = potential_max_2 in
potential_max
then
potential_max_1
else potential_max_2)
-1
x))
]
(λ (_: unit) → false)
(λ (_: unit) → ENone ()))

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

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,22 +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
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
in
let set y : integer = s.f.0 s.f.1 2 in
return { T y = y; }
```

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 {
@ -158,21 +144,9 @@ let scope Foo
let set b : bool =
match
(handle_default_opt
[
let code_and_env : ((any, unit) → eoption bool * any) = b in
code_and_env.0 code_and_env.1 ()
]
[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
@ -182,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; }

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

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

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