Better optimizations with values instead of literals

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

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

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

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), _) ])), _),

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