2022-01-07 20:36:56 +03:00
|
|
|
(* This file is part of the Catala compiler, a specification language for tax
|
2022-01-10 12:59:30 +03:00
|
|
|
and social benefits computation rules. Copyright (C) 2022 Inria,
|
2022-01-07 20:36:56 +03:00
|
|
|
contributors: Alain Delaët <alain.delaet--tixeuil@inria.fr>, Denis Merigoux
|
|
|
|
<denis.merigoux@inria.fr>
|
|
|
|
|
|
|
|
Licensed under the Apache License, Version 2.0 (the "License"); you may not
|
|
|
|
use this file except in compliance with the License. You may obtain a copy of
|
|
|
|
the License at
|
|
|
|
|
|
|
|
http://www.apache.org/licenses/LICENSE-2.0
|
|
|
|
|
|
|
|
Unless required by applicable law or agreed to in writing, software
|
|
|
|
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
|
|
|
|
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
|
|
|
|
License for the specific language governing permissions and limitations under
|
|
|
|
the License. *)
|
|
|
|
open Utils
|
2022-08-12 23:42:39 +03:00
|
|
|
open Shared_ast
|
2022-01-07 20:36:56 +03:00
|
|
|
open Ast
|
|
|
|
|
2022-01-31 16:30:42 +03:00
|
|
|
type partial_evaluation_ctx = {
|
2022-08-25 20:46:13 +03:00
|
|
|
var_values : (typed expr, typed expr) Var.Map.t;
|
2022-01-31 16:30:42 +03:00
|
|
|
decl_ctx : decl_ctx;
|
|
|
|
}
|
2022-01-07 20:36:56 +03:00
|
|
|
|
2022-08-25 17:35:08 +03:00
|
|
|
let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
|
2022-11-17 19:13:35 +03:00
|
|
|
(dcalc, 'm mark) boxed_gexpr =
|
|
|
|
(* We proceed bottom-up, first apply on the subterms *)
|
|
|
|
let e = Expr.map ~f:(partial_evaluation ctx) e in
|
2022-09-27 17:27:26 +03:00
|
|
|
let mark = Marked.get_mark e in
|
2022-11-17 19:13:35 +03:00
|
|
|
(* Then reduce the parent node *)
|
|
|
|
let reduce e =
|
|
|
|
(* Todo: improve the handling of eapp(log,elit) cases here, it obfuscates
|
|
|
|
the matches and the log calls are not preserved, which would be a good
|
|
|
|
property *)
|
|
|
|
match Marked.unmark e with
|
|
|
|
| EApp
|
|
|
|
{
|
|
|
|
f =
|
|
|
|
( EOp (Unop Not), _
|
|
|
|
| ( EApp { f = EOp (Unop (Log _)), _; args = [(EOp (Unop Not), _)] },
|
|
|
|
_ ) ) as op;
|
|
|
|
args = [e1];
|
|
|
|
} -> (
|
|
|
|
(* reduction of logical not *)
|
|
|
|
match e1 with
|
|
|
|
| ELit (LBool false), _ -> ELit (LBool true)
|
|
|
|
| ELit (LBool true), _ -> ELit (LBool false)
|
|
|
|
| e1 -> EApp { f = op; args = [e1] })
|
|
|
|
| EApp
|
|
|
|
{
|
|
|
|
f =
|
|
|
|
( EOp (Binop Or), _
|
|
|
|
| ( EApp { f = EOp (Unop (Log _)), _; args = [(EOp (Binop Or), _)] },
|
|
|
|
_ ) ) as op;
|
|
|
|
args = [e1; e2];
|
|
|
|
} -> (
|
|
|
|
(* reduction of logical or *)
|
|
|
|
match e1, e2 with
|
|
|
|
| (ELit (LBool false), _), new_e | new_e, (ELit (LBool false), _) ->
|
|
|
|
Marked.unmark new_e
|
|
|
|
| (ELit (LBool true), _), _ | _, (ELit (LBool true), _) ->
|
|
|
|
ELit (LBool true)
|
|
|
|
| _ -> EApp { f = op; args = [e1; e2] })
|
|
|
|
| EApp
|
|
|
|
{
|
|
|
|
f =
|
|
|
|
( EOp (Binop And), _
|
|
|
|
| ( EApp { f = EOp (Unop (Log _)), _; args = [(EOp (Binop And), _)] },
|
|
|
|
_ ) ) as op;
|
|
|
|
args = [e1; e2];
|
|
|
|
} -> (
|
|
|
|
(* reduction of logical and *)
|
|
|
|
match e1, e2 with
|
|
|
|
| (ELit (LBool true), _), new_e | new_e, (ELit (LBool true), _) ->
|
|
|
|
Marked.unmark new_e
|
|
|
|
| (ELit (LBool false), _), _ | _, (ELit (LBool false), _) ->
|
|
|
|
ELit (LBool false)
|
|
|
|
| _ -> EApp { f = op; args = [e1; e2] })
|
|
|
|
| EMatch { e = EInj { e; name = name1; cons }, _; cases; name }
|
|
|
|
when EnumName.equal name name1 ->
|
|
|
|
(* iota reduction *)
|
2022-11-21 12:12:45 +03:00
|
|
|
EApp { f = EnumConstructor.Map.find cons cases; args = [e] }
|
2022-11-17 19:13:35 +03:00
|
|
|
| EApp { f = EAbs { binder; _ }, _; args } ->
|
|
|
|
(* beta reduction *)
|
|
|
|
Marked.unmark (Bindlib.msubst binder (List.map fst args |> Array.of_list))
|
|
|
|
| EDefault { excepts; just; cons } -> (
|
|
|
|
(* TODO: mechanically prove each of these optimizations correct :) *)
|
|
|
|
let excepts =
|
|
|
|
List.filter
|
|
|
|
(fun except -> Marked.unmark except <> ELit LEmptyError)
|
|
|
|
excepts
|
|
|
|
(* we can discard the exceptions that are always empty error *)
|
|
|
|
in
|
|
|
|
let value_except_count =
|
|
|
|
List.fold_left
|
|
|
|
(fun nb except -> if Expr.is_value except then nb + 1 else nb)
|
|
|
|
0 excepts
|
|
|
|
in
|
|
|
|
if value_except_count > 1 then
|
|
|
|
(* at this point we know a conflict error will be triggered so we just
|
|
|
|
feed the expression to the interpreter that will print the beautiful
|
|
|
|
right error message *)
|
|
|
|
Marked.unmark (Interpreter.evaluate_expr ctx.decl_ctx e)
|
|
|
|
else
|
|
|
|
match excepts, just with
|
|
|
|
| [except], _ when Expr.is_value except ->
|
2022-01-09 21:16:34 +03:00
|
|
|
(* if there is only one exception and it is a non-empty value it is
|
|
|
|
always chosen *)
|
2022-11-17 19:13:35 +03:00
|
|
|
Marked.unmark except
|
2022-01-09 21:16:34 +03:00
|
|
|
| ( [],
|
|
|
|
( ( ELit (LBool true)
|
2022-11-17 19:13:35 +03:00
|
|
|
| EApp
|
|
|
|
{ f = EOp (Unop (Log _)), _; args = [(ELit (LBool true), _)] }
|
|
|
|
),
|
|
|
|
_ ) ) ->
|
|
|
|
Marked.unmark cons
|
2022-05-04 18:40:55 +03:00
|
|
|
| ( [],
|
2022-01-09 21:16:34 +03:00
|
|
|
( ( ELit (LBool false)
|
2022-11-17 19:13:35 +03:00
|
|
|
| EApp
|
|
|
|
{
|
|
|
|
f = EOp (Unop (Log _)), _;
|
|
|
|
args = [(ELit (LBool false), _)];
|
|
|
|
} ),
|
|
|
|
_ ) ) ->
|
|
|
|
ELit LEmptyError
|
|
|
|
| [], just when not !Cli.avoid_exceptions_flag ->
|
2022-01-31 16:30:42 +03:00
|
|
|
(* without exceptions, a default is just an [if then else] raising an
|
2022-02-24 18:46:02 +03:00
|
|
|
error in the else case. This exception is only valid in the context
|
|
|
|
of compilation_with_exceptions, so we desactivate with a global
|
2022-01-07 20:36:56 +03:00
|
|
|
flag to know if we will be compiling using exceptions or the option
|
2022-11-17 19:13:35 +03:00
|
|
|
monad. FIXME: move this optimisation somewhere else to avoid this
|
|
|
|
check *)
|
|
|
|
EIfThenElse
|
|
|
|
{ cond = just; etrue = cons; efalse = ELit LEmptyError, mark }
|
|
|
|
| excepts, just -> EDefault { excepts; just; cons })
|
|
|
|
| EIfThenElse
|
|
|
|
{
|
|
|
|
cond =
|
|
|
|
( ELit (LBool true), _
|
|
|
|
| ( EApp
|
|
|
|
{ f = EOp (Unop (Log _)), _; args = [(ELit (LBool true), _)] },
|
|
|
|
_ ) );
|
|
|
|
etrue;
|
|
|
|
_;
|
|
|
|
} ->
|
|
|
|
Marked.unmark etrue
|
|
|
|
| EIfThenElse
|
|
|
|
{
|
|
|
|
cond =
|
|
|
|
( ( ELit (LBool false)
|
|
|
|
| EApp
|
|
|
|
{
|
|
|
|
f = EOp (Unop (Log _)), _;
|
|
|
|
args = [(ELit (LBool false), _)];
|
|
|
|
} ),
|
|
|
|
_ );
|
|
|
|
efalse;
|
|
|
|
_;
|
|
|
|
} ->
|
|
|
|
Marked.unmark efalse
|
|
|
|
| EIfThenElse
|
|
|
|
{
|
|
|
|
cond;
|
|
|
|
etrue =
|
|
|
|
( ( ELit (LBool btrue)
|
|
|
|
| EApp
|
|
|
|
{
|
|
|
|
f = EOp (Unop (Log _)), _;
|
|
|
|
args = [(ELit (LBool btrue), _)];
|
|
|
|
} ),
|
|
|
|
_ );
|
|
|
|
efalse =
|
|
|
|
( ( ELit (LBool bfalse)
|
|
|
|
| EApp
|
|
|
|
{
|
|
|
|
f = EOp (Unop (Log _)), _;
|
|
|
|
args = [(ELit (LBool bfalse), _)];
|
|
|
|
} ),
|
|
|
|
_ );
|
|
|
|
} ->
|
|
|
|
if btrue && not bfalse then Marked.unmark cond
|
|
|
|
else if (not btrue) && bfalse then
|
|
|
|
EApp { f = EOp (Unop Not), mark; args = [cond] }
|
|
|
|
(* note: this last call eliminates the condition & might skip log calls
|
|
|
|
as well *)
|
|
|
|
else (* btrue = bfalse *) ELit (LBool btrue)
|
|
|
|
| e -> e
|
|
|
|
in
|
|
|
|
Expr.Box.app1 e reduce mark
|
2022-01-07 20:36:56 +03:00
|
|
|
|
2022-08-25 17:35:08 +03:00
|
|
|
let optimize_expr (decl_ctx : decl_ctx) (e : 'm expr) =
|
2022-07-28 11:36:36 +03:00
|
|
|
partial_evaluation { var_values = Var.Map.empty; decl_ctx } e
|
2022-01-07 20:36:56 +03:00
|
|
|
|
2022-04-02 15:51:11 +03:00
|
|
|
let rec scope_lets_map
|
2022-11-17 19:13:35 +03:00
|
|
|
(t : 'a -> 'm expr -> (dcalc, 'm mark) boxed_gexpr)
|
2022-01-07 20:36:56 +03:00
|
|
|
(ctx : 'a)
|
2022-08-25 20:46:13 +03:00
|
|
|
(scope_body_expr : 'm expr scope_body_expr) :
|
|
|
|
'm expr scope_body_expr Bindlib.box =
|
2022-04-02 15:51:11 +03:00
|
|
|
match scope_body_expr with
|
2022-11-17 19:13:35 +03:00
|
|
|
| Result e ->
|
|
|
|
Bindlib.box_apply (fun e' -> Result e') (Expr.Box.lift (t ctx e))
|
2022-04-02 15:51:11 +03:00
|
|
|
| ScopeLet scope_let ->
|
|
|
|
let var, next = Bindlib.unbind scope_let.scope_let_next in
|
2022-11-17 19:13:35 +03:00
|
|
|
let new_scope_let_expr = Expr.Box.lift (t ctx scope_let.scope_let_expr) in
|
2022-04-02 15:51:11 +03:00
|
|
|
let new_next = scope_lets_map t ctx next in
|
|
|
|
let new_next = Bindlib.bind_var var new_next in
|
|
|
|
Bindlib.box_apply2
|
|
|
|
(fun new_scope_let_expr new_next ->
|
|
|
|
ScopeLet
|
2022-01-07 20:36:56 +03:00
|
|
|
{
|
2022-04-02 15:51:11 +03:00
|
|
|
scope_let with
|
|
|
|
scope_let_expr = new_scope_let_expr;
|
|
|
|
scope_let_next = new_next;
|
|
|
|
})
|
|
|
|
new_scope_let_expr new_next
|
|
|
|
|
|
|
|
let rec scopes_map
|
2022-11-17 19:13:35 +03:00
|
|
|
(t : 'a -> 'm expr -> (dcalc, 'm mark) boxed_gexpr)
|
2022-04-02 15:51:11 +03:00
|
|
|
(ctx : 'a)
|
2022-08-25 20:46:13 +03:00
|
|
|
(scopes : 'm expr scopes) : 'm expr scopes Bindlib.box =
|
2022-04-02 15:51:11 +03:00
|
|
|
match scopes with
|
|
|
|
| Nil -> Bindlib.box Nil
|
|
|
|
| ScopeDef scope_def ->
|
|
|
|
let scope_var, scope_next = Bindlib.unbind scope_def.scope_next in
|
|
|
|
let scope_arg_var, scope_body_expr =
|
|
|
|
Bindlib.unbind scope_def.scope_body.scope_body_expr
|
|
|
|
in
|
|
|
|
let new_scope_body_expr = scope_lets_map t ctx scope_body_expr in
|
|
|
|
let new_scope_body_expr =
|
|
|
|
Bindlib.bind_var scope_arg_var new_scope_body_expr
|
|
|
|
in
|
|
|
|
let new_scope_next = scopes_map t ctx scope_next in
|
|
|
|
let new_scope_next = Bindlib.bind_var scope_var new_scope_next in
|
|
|
|
Bindlib.box_apply2
|
|
|
|
(fun new_scope_body_expr new_scope_next ->
|
|
|
|
ScopeDef
|
|
|
|
{
|
|
|
|
scope_def with
|
|
|
|
scope_next = new_scope_next;
|
|
|
|
scope_body =
|
|
|
|
{
|
|
|
|
scope_def.scope_body with
|
|
|
|
scope_body_expr = new_scope_body_expr;
|
|
|
|
};
|
|
|
|
})
|
|
|
|
new_scope_body_expr new_scope_next
|
|
|
|
|
|
|
|
let program_map
|
2022-11-17 19:13:35 +03:00
|
|
|
(t : 'a -> 'm expr -> (dcalc, 'm mark) boxed_gexpr)
|
2022-04-02 15:51:11 +03:00
|
|
|
(ctx : 'a)
|
2022-05-31 19:38:14 +03:00
|
|
|
(p : 'm program) : 'm program Bindlib.box =
|
2022-04-02 15:51:11 +03:00
|
|
|
Bindlib.box_apply
|
|
|
|
(fun new_scopes -> { p with scopes = new_scopes })
|
|
|
|
(scopes_map t ctx p.scopes)
|
2022-01-07 20:36:56 +03:00
|
|
|
|
2022-09-27 17:27:26 +03:00
|
|
|
let optimize_program (p : 'm program) : 'm program =
|
2022-04-02 15:51:11 +03:00
|
|
|
Bindlib.unbox
|
|
|
|
(program_map partial_evaluation
|
2022-07-28 11:36:36 +03:00
|
|
|
{ var_values = Var.Map.empty; decl_ctx = p.decl_ctx }
|
2022-04-02 15:51:11 +03:00
|
|
|
p)
|