Better beta-reduction

This commit is contained in:
Denis Merigoux 2023-12-18 14:49:43 +01:00
parent 35f829cd65
commit 91f8451899
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
4 changed files with 13 additions and 18 deletions

View File

@ -206,9 +206,17 @@ let rec optimize_expr :
cases1 cases2
in
EMatch { e = arg; cases; name = n1 }
| EApp { f = EAbs { binder; _ }, _; args = [(ELit _, _)] as args } ->
(* beta reduction when let-binding a literal *)
Mark.remove (Bindlib.msubst binder (List.map fst args |> Array.of_list))
| EApp { f = EAbs { binder; _ }, _; args = [(EVar _, _)] as args } ->
(* beta reduction when let-binding a variable *)
Mark.remove (Bindlib.msubst binder (List.map fst args |> Array.of_list))
| 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
(* when variables not used *)
|| match args with [((EVar _ | ELit _), _)] -> true | _ -> false ->
(* beta reduction for special cases *)
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 ->

View File

@ -52,12 +52,7 @@ let scope S (S_in: S_in {x_in: bool}): S {z: integer} =
let set f : ((closure_env, integer) → integer * closure_env) =
(closure_f, to_closure_env (x))
in
let set z : integer =
let code_and_env : ((closure_env, integer) → integer * closure_env) =
f
in
code_and_env.0 code_and_env.1 -1
in
let set z : integer = f.0 f.1 -1 in
return { S z = z; }
```

View File

@ -53,12 +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 =
let code_and_env : ((closure_env, integer) → integer * closure_env) =
s.f
in
code_and_env.0 code_and_env.1 2
in
let set y : integer = s.f.0 s.f.1 2 in
return { T y = y; }
```

View File

@ -144,10 +144,7 @@ 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 true))
with