Aesthetic improvements

compiler/dcalc/print.ml

@@ -160,8 +160,8 @@ let format_unop (fmt : Format.formatter) (op : unop Pos.marked) : unit =
     | GetMonth -> "get_month"
     | GetYear -> "get_year")
 
-let needs_parens (_e : expr Pos.marked) : bool = true
-(* match Pos.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false *)
+let needs_parens (e : expr Pos.marked) : bool =
+  match Pos.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false
 
 let format_var (fmt : Format.formatter) (v : Var.t) : unit =
   Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
@@ -218,7 +218,10 @@ let rec format_expr (ctx : Ast.decl_ctx) (fmt : Format.formatter) (e : expr Pos.
              Format.fprintf fmt "@[<hov 2>%a%a@ %a@]" Ast.EnumConstructor.format_t c
                format_punctuation ":" format_expr e))
         (List.combine es (List.map fst (Ast.EnumMap.find e_name ctx.ctx_enums)))
-  | ELit l -> Format.fprintf fmt "%a" format_lit (Pos.same_pos_as l e)
+  | ELit l ->
+      Format.fprintf fmt "%s"
+        (Utils.Cli.print_with_style [ ANSITerminal.yellow ] "%s"
+           (Format.asprintf "%a" format_lit (Pos.same_pos_as l e)))
   | EApp ((EAbs ((binder, _), taus), _), args) ->
       let xs, body = Bindlib.unmbind binder in
       let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in

compiler/driver.ml

@@ -218,13 +218,21 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
         | Cli.Proof ->
             let vcs = Verification.Conditions.generate_verification_conditions prgm in
             List.iter
-              (fun vc ->
+              (fun (vc : Verification.Conditions.verification_condition) ->
                 Cli.result_print
                   (Format.asprintf
-                     "For this variable:\n%s\nThis verification condition was generated:\n%a"
-                     (Pos.retrieve_loc_text (Pos.get_position vc))
+                     "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.vc_guard))
               vcs;
             Verification.Z3encoding.solve_vc vcs;
             0

compiler/verification/conditions.ml

@@ -97,7 +97,15 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Pos.marked) : ex
   out
   [@@ocamlformat "wrap-comments=false"]
 
-let generate_verification_conditions (p : program) : expr Pos.marked list =
+type verification_condition_kind = NoEmptyError | NoOverlappingExceptions
+
+type verification_condition = {
+  vc_guard : expr Pos.marked;
+  (* should have type bool *)
+  vc_kind : verification_condition_kind;
+}
+
+let generate_verification_conditions (p : program) : verification_condition list =
   List.fold_left
     (fun acc (_s_name, _s_var, s_body) ->
       let ctx = { decl = p.decl_ctx; input_vars = [] } in
@@ -113,8 +121,8 @@ let generate_verification_conditions (p : program) : expr Pos.marked list =
                 let vc =
                   if !Cli.optimize_flag then Bindlib.unbox (Optimizations.optimize_expr vc) else vc
                 in
-                (* TODO: drop logs for Aymeric *)
-                (Pos.same_pos_as (Pos.unmark vc) e :: acc, ctx)
+                ( { vc_guard = Pos.same_pos_as (Pos.unmark vc) e; vc_kind = NoEmptyError } :: acc,
+                  ctx )
             | _ -> (acc, ctx))
           (acc, ctx) s_body.scope_body_lets
       in

compiler/verification/z3encoding.ml

@@ -122,7 +122,7 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : Expr.expr =
 (** [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 : expr Pos.marked list) : unit =
+let solve_vc (vcs : Conditions.verification_condition list) : unit =
   Printf.printf "Running Z3 version %s\n" Version.to_string;
 
   let cfg = [ ("model", "true"); ("proof", "false") ] in
@@ -130,7 +130,7 @@ let solve_vc (vcs : expr Pos.marked list) : unit =
 
   let solver = Solver.mk_solver ctx None in
 
-  let z3_vcs = List.map (translate_expr ctx) vcs in
+  let z3_vcs = List.map (fun vc -> translate_expr ctx vc.Conditions.vc_guard) vcs in
 
   List.iter (fun vc -> Printf.printf "Generated VC: %s\n" (Expr.to_string vc)) z3_vcs;