Optimizations for defaults in Dcalc

compiler/dcalc/interpreter.mli

@@ -16,7 +16,11 @@
 
 open Utils
 
+val evaluate_expr : Ast.decl_ctx -> Ast.expr Pos.marked -> Ast.expr Pos.marked
+(** Evaluates an expression according to the semantics of the default calculus. *)
+
 val interpret_program :
   Ast.decl_ctx -> Ast.expr Pos.marked -> (Uid.MarkedString.info * Ast.expr Pos.marked) list
-(** Interpret a program. This function expects an expression typed as a function whose argument are
-    all thunked. The function is executed by providing for each argument a thunked empty default. *)
+(** Interprets a program. This function expects an expression typed as a function whose argument are
+    all thunked. The function is executed by providing for each argument a thunked empty default.
+    Returns a list of all the computed values for the scope variables of the executed scope. *)

compiler/dcalc/optimizations.ml

@@ -14,7 +14,7 @@
 open Utils
 open Ast
 
-type partial_evaluation_ctx = expr Pos.marked Ast.VarMap.t
+type partial_evaluation_ctx = { var_values : expr Pos.marked Ast.VarMap.t; decl_ctx : decl_ctx }
 
 let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked) :
     expr Pos.marked Bindlib.box =
@@ -94,7 +94,40 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked)
   | EOp op -> Bindlib.box (EOp op, pos)
   | EDefault (exceptions, just, cons) ->
       Bindlib.box_apply3
-        (fun exceptions just cons -> (EDefault (exceptions, just, cons), pos))
+        (fun exceptions just cons ->
+          (* TODO: mechanically prove each of these optimizations correct :) *)
+          match
+            ( List.filter
+                (fun except -> match Pos.unmark except with ELit LEmptyError -> false | _ -> true)
+                exceptions
+              (* we can discard the exceptions that are always empty error *),
+              just,
+              cons )
+          with
+          | exceptions, just, cons
+            when List.fold_left
+                   (fun nb except -> match Pos.unmark except with ELit _ -> nb + 1 | _ -> 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
+          | ( [],
+              ((ELit (LBool true) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ])), _),
+              cons ) ->
+              cons
+          | ( [],
+              ((ELit (LBool false) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ])), _),
+              _ ) ->
+              (ELit LEmptyError, pos)
+          | [], just, cons ->
+              (* without exceptions, a default is just an [if then else] raising an error in the
+                 else case *)
+              (EIfThenElse (just, cons, (ELit LEmptyError, pos)), pos)
+          | exceptions, just, cons -> (EDefault (exceptions, just, cons), pos))
         (List.map rec_helper exceptions |> Bindlib.box_list)
         (rec_helper just) (rec_helper cons)
   | EIfThenElse (e1, e2, e3) ->
@@ -116,7 +149,8 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked)
         (rec_helper e1) (rec_helper e2) (rec_helper e3)
   | ErrorOnEmpty e1 -> Bindlib.box_apply (fun e1 -> (ErrorOnEmpty e1, pos)) (rec_helper e1)
 
-let optimize_expr = partial_evaluation VarMap.empty
+let optimize_expr (decl_ctx : decl_ctx) (e : expr Pos.marked) =
+  partial_evaluation { var_values = VarMap.empty; decl_ctx } e
 
 let program_map (t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box) (ctx : 'a) (p : program)
     : program =
@@ -143,7 +177,8 @@ let program_map (t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box) (ctx
         p.scopes;
   }
 
-let optimize_program (p : program) : program = program_map partial_evaluation VarMap.empty p
+let optimize_program (p : program) : program =
+  program_map partial_evaluation { var_values = VarMap.empty; decl_ctx = p.decl_ctx } p
 
 let rec remove_all_logs (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
   let pos = Pos.get_position e in

compiler/dcalc/optimizations.mli

@@ -17,7 +17,7 @@
 open Utils
 open Ast
 
-val optimize_expr : expr Pos.marked -> expr Pos.marked Bindlib.box
+val optimize_expr : decl_ctx -> expr Pos.marked -> expr Pos.marked Bindlib.box
 
 val optimize_program : program -> program
 

compiler/verification/conditions.ml

@@ -267,7 +267,8 @@ let generate_verification_conditions (p : program) : verification_condition list
                 in
                 let vc_confl, vc_confl_typs = generate_vs_must_not_return_confict ctx e in
                 let vc_confl =
-                  if !Cli.optimize_flag then Bindlib.unbox (Optimizations.optimize_expr vc_confl)
+                  if !Cli.optimize_flag then
+                    Bindlib.unbox (Optimizations.optimize_expr p.decl_ctx vc_confl)
                   else vc_confl
                 in
                 let vc_list =
@@ -287,7 +288,7 @@ let generate_verification_conditions (p : program) : verification_condition list
                       let vc_empty, vc_empty_typs = generate_vc_must_not_return_empty ctx e in
                       let vc_empty =
                         if !Cli.optimize_flag then
-                          Bindlib.unbox (Optimizations.optimize_expr vc_empty)
+                          Bindlib.unbox (Optimizations.optimize_expr p.decl_ctx vc_empty)
                         else vc_empty
                       in
                       {

french_law/js/package-lock.json

@@ -1,8 +1,40 @@
 {
   "name": "french_law",
   "version": "0.5.0",
-  "lockfileVersion": 1,
+  "lockfileVersion": 2,
   "requires": true,
+  "packages": {
+    "": {
+      "name": "french_law",
+      "version": "0.5.0",
+      "license": "Apache-2.0",
+      "dependencies": {
+        "benchmark": "^2.1.4",
+        "lodash": "^4.17.21",
+        "platform": "^1.3.6"
+      },
+      "devDependencies": {}
+    },
+    "node_modules/benchmark": {
+      "version": "2.1.4",
+      "resolved": "https://registry.npmjs.org/benchmark/-/benchmark-2.1.4.tgz",
+      "integrity": "sha1-CfPeMckWQl1JjMLuVloOvzwqVik=",
+      "dependencies": {
+        "lodash": "^4.17.4",
+        "platform": "^1.3.3"
+      }
+    },
+    "node_modules/lodash": {
+      "version": "4.17.21",
+      "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.17.21.tgz",
+      "integrity": "sha512-v2kDEe57lecTulaDIuNTPy3Ry4gLGJ6Z1O3vE1krgXZNrsQ+LFTGHVxVjcXPs17LhbZVGedAJv8XZ1tvj5FvSg=="
+    },
+    "node_modules/platform": {
+      "version": "1.3.6",
+      "resolved": "https://registry.npmjs.org/platform/-/platform-1.3.6.tgz",
+      "integrity": "sha512-fnWVljUchTro6RiCFvCXBbNhJc2NijN7oIQxbwsyL0buWJPG85v81ehlHI9fXrJsMNgTofEoWIQeClKpgxFLrg=="
+    }
+  },
   "dependencies": {
     "benchmark": {
       "version": "2.1.4",