From 0d90dcea005f1365431f7f4095d69041d4522509 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Wed, 2 Feb 2022 10:30:39 +0100 Subject: [PATCH] Better optimizations with values instead of literals --- compiler/dcalc/ast.ml | 3 +++ compiler/dcalc/ast.mli | 8 +++++++- compiler/dcalc/interpreter.ml | 2 +- compiler/dcalc/optimizations.ml | 6 +++--- french_law/python/main.py | 2 +- 5 files changed, 15 insertions(+), 6 deletions(-) diff --git a/compiler/dcalc/ast.ml b/compiler/dcalc/ast.ml index 3f2161b2..0458772c 100644 --- a/compiler/dcalc/ast.ml +++ b/compiler/dcalc/ast.ml @@ -189,6 +189,9 @@ let empty_thunked_term : expr Pos.marked = (Bindlib.box (ELit LEmptyError, Pos.no_pos)) Pos.no_pos [ (TLit TUnit, Pos.no_pos) ] Pos.no_pos) +let is_value (e : expr Pos.marked) : bool = + match Pos.unmark e with ELit _ | EAbs _ | EOp _ -> true | _ -> false + let build_whole_scope_expr (ctx : decl_ctx) (body : scope_body) (pos_scope : Pos.t) = let body_expr = List.fold_right diff --git a/compiler/dcalc/ast.mli b/compiler/dcalc/ast.mli index 0cbdf867..200ee715 100644 --- a/compiler/dcalc/ast.mli +++ b/compiler/dcalc/ast.mli @@ -168,7 +168,9 @@ type scope_body = { type program = { decl_ctx : decl_ctx; scopes : (ScopeName.t * expr Bindlib.var * scope_body) list } -(** {1 Variable helpers} *) +(** {1 Helpers} *) + +(** {2 Variables}*) module Var : sig type t = expr Bindlib.var @@ -206,8 +208,12 @@ val make_let_in : Pos.t -> expr Pos.marked Bindlib.box +(**{2 Other}*) + val empty_thunked_term : expr Pos.marked +val is_value : expr Pos.marked -> bool + (** {1 AST manipulation helpers}*) val build_whole_scope_expr : decl_ctx -> scope_body -> Pos.t -> expr Pos.marked Bindlib.box diff --git a/compiler/dcalc/interpreter.ml b/compiler/dcalc/interpreter.ml index 219b7227..286ad44b 100644 --- a/compiler/dcalc/interpreter.ml +++ b/compiler/dcalc/interpreter.ml @@ -291,7 +291,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark "function has not been reduced to a lambda at evaluation (should not happen if the \ term was well-typed" (Pos.get_position e)) - | EAbs _ | ELit _ | EOp _ -> e (* thse are values *) + | EAbs _ | ELit _ | EOp _ -> e (* these are values *) | ETuple (es, s) -> let new_es = List.map (evaluate_expr ctx) es in if List.exists is_empty_error new_es then Pos.same_pos_as (A.ELit LEmptyError) e diff --git a/compiler/dcalc/optimizations.ml b/compiler/dcalc/optimizations.ml index abcf95da..d7d7ff3c 100644 --- a/compiler/dcalc/optimizations.ml +++ b/compiler/dcalc/optimizations.ml @@ -106,14 +106,14 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked) with | exceptions, just, cons when List.fold_left - (fun nb except -> match Pos.unmark except with ELit _ -> nb + 1 | _ -> nb) + (fun nb except -> if is_value except then nb + 1 else nb) 0 exceptions > 1 -> (* 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 *) Interpreter.evaluate_expr ctx.decl_ctx (EDefault (exceptions, just, cons), pos) - | [ ((ELit _, _) as except) ], _, _ -> - (* if there is only one exception and it is a non-empty literal it is always chosen *) + | [ except ], _, _ when is_value except -> + (* if there is only one exception and it is a non-empty value it is always chosen *) except | ( [], ((ELit (LBool true) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ])), _), diff --git a/french_law/python/main.py b/french_law/python/main.py index dfdcdc32..08f24d4a 100755 --- a/french_law/python/main.py +++ b/french_law/python/main.py @@ -60,7 +60,7 @@ if __name__ == '__main__': args = parser.parse_args() action = args.action[0] if action == "bench": - iterations = 10000 + iterations = 1000 print("Iterating {} iterations of the family benefits computation. Total time (s):".format( iterations)) print(timeit.timeit(benchmark_iteration, number=iterations))