More prettier things

compiler/dcalc/optimizations.ml

@@ -1,5 +1,5 @@
 (* This file is part of the Catala compiler, a specification language for tax and social benefits
-   computation rules. Copyright (C) 2020 Inria, contributors: Alain Delaët
+   computation rules. Copyright (C) 2022 Inria, 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

compiler/dcalc/optimizations.mli

@@ -0,0 +1,20 @@
+(* This file is part of the Catala compiler, a specification language for tax and social benefits
+   computation rules. Copyright (C) 2022 Inria, 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
+open Ast
+
+val optimize_expr : expr Pos.marked -> expr Pos.marked Bindlib.box
+
+val optimize_program : program -> program

compiler/driver.ml

@@ -217,24 +217,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
         match backend with
         | Cli.Proof ->
             let vcs = Verification.Conditions.generate_verification_conditions prgm in
-            List.iter
-              (fun (vc : Verification.Conditions.verification_condition) ->
-                Cli.result_print
-                  (Format.asprintf
-                     "For this variable:\n\
-                      %s\n\
-                      This verification condition was generated for %s:@\n\
-                      %a"
-                     (Pos.retrieve_loc_text (Pos.get_position vc.vc_guard))
-                     (Cli.print_with_style [ ANSITerminal.yellow ] "%s"
-                        (match vc.vc_kind with
-                        | Verification.Conditions.NoEmptyError ->
-                            "the variable definition never to return an empty error"
-                        | NoOverlappingExceptions -> "no two exceptions to ever overlap"))
-                     (Dcalc.Print.format_expr prgm.decl_ctx)
-                     vc.vc_guard))
-              vcs;
-            Verification.Z3encoding.solve_vc vcs;
+            Verification.Z3encoding.solve_vc prgm.decl_ctx vcs;
             0
         | Cli.Run ->
             Cli.debug_print "Starting interpretation...";

compiler/index.mld

@@ -81,6 +81,11 @@ The main compilation chain is defined in:
 
 {!modules: Driver}
 
+Additionally, the compiler features a verification plugin that generates
+verification condition for proof backends. More information can be found here:
+
+{!modules: Verification}
+
 Last, two more modules contain additional features for the compiler:
 
 {ul

compiler/verification/z3encoding.ml

@@ -119,10 +119,12 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : Expr.expr =
         ]
   | ErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
 
+type vc_encoding_result = Success of Expr.expr | Fail of string
+
 (** [solve_vc] is the main entry point of this module. It takes a list of expressions [vcs]
     corresponding to verification conditions that must be discharged by Z3, and attempts to solve
     them **)
-let solve_vc (vcs : Conditions.verification_condition list) : unit =
+let solve_vc (decl_ctx : decl_ctx) (vcs : Conditions.verification_condition list) : unit =
   Printf.printf "Running Z3 version %s\n" Version.to_string;
 
   let cfg = [ ("model", "true"); ("proof", "false") ] in
@@ -130,13 +132,37 @@ let solve_vc (vcs : Conditions.verification_condition list) : unit =
 
   let solver = Solver.mk_solver ctx None in
 
-  let z3_vcs = List.map (fun vc -> translate_expr ctx vc.Conditions.vc_guard) vcs in
+  let z3_vcs =
+    List.map
+      (fun vc ->
+        (vc, try Success (translate_expr ctx vc.Conditions.vc_guard) with Failure msg -> Fail msg))
+      vcs
+  in
 
-  List.iter (fun vc -> Printf.printf "Generated VC: %s\n" (Expr.to_string vc)) z3_vcs;
+  List.iter
+    (fun (vc, z3_vc) ->
+      Cli.result_print
+        (Format.asprintf
+           "For this variable:\n%s\nThis verification condition was generated for %s:@\n%a"
+           (Pos.retrieve_loc_text (Pos.get_position vc.Conditions.vc_guard))
+           (Cli.print_with_style [ ANSITerminal.yellow ] "%s"
+              (match vc.vc_kind with
+              | Conditions.NoEmptyError -> "the variable definition never to return an empty error"
+              | NoOverlappingExceptions -> "no two exceptions to ever overlap"))
+           (Dcalc.Print.format_expr decl_ctx)
+           vc.vc_guard);
+      match z3_vc with
+      | Success z3_vc ->
+          let z3_vc_string = Expr.to_string z3_vc in
+          Cli.result_print
+            (Format.asprintf "The translation to Z3 is the following:@\n%s" z3_vc_string)
+      | Fail msg -> Cli.error_print (Format.asprintf "The translation to Z3 failed:@\n%s" msg))
+    z3_vcs;
 
-  Solver.add solver z3_vcs;
+  Solver.add solver
+    (List.filter_map (fun (_, vc) -> match vc with Success e -> Some e | _ -> None) z3_vcs);
 
-  if Solver.check solver [] = SATISFIABLE then Printf.printf "Success: Empty unreachable\n"
+  if Solver.check solver [] = SATISFIABLE then Cli.result_print "Success: Empty unreachable\n"
   else
     (* TODO: Print model as error message for Catala debugging purposes *)
-    Printf.printf "Failure: Empty reachable\n"
+    Cli.error_print "Failure: Empty reachable\n"