new invariant option when launching the compiler

compiler/catala_utils/cli.ml

@@ -29,7 +29,8 @@ type backend_option_builtin =
   | `Lcalc
   | `Dcalc
   | `Scopelang
-  | `Proof ]
+  | `Proof
+  | `DcalcInvariants ]
 
 type 'a backend_option = [ backend_option_builtin | `Plugin of 'a ]
 
@@ -46,6 +47,7 @@ let backend_option_to_string = function
   | `Typecheck -> "Typecheck"
   | `Scalc -> "Scalc"
   | `Lcalc -> "Lcalc"
+  | `DcalcInvariants -> "invariants"
   | `Plugin s -> s
 
 let backend_option_of_string backend =
@@ -62,6 +64,7 @@ let backend_option_of_string backend =
   | "typecheck" -> `Typecheck
   | "scalc" -> `Scalc
   | "lcalc" -> `Lcalc
+  | "invariants" -> `DcalcInvariants
   | s -> `Plugin s
 
 (** Source files to be compiled *)

compiler/catala_utils/cli.mli

@@ -29,7 +29,8 @@ type backend_option_builtin =
   | `Lcalc
   | `Dcalc
   | `Scopelang
-  | `Proof ]
+  | `Proof
+  | `DcalcInvariants ]
 
 type 'a backend_option = [ backend_option_builtin | `Plugin of 'a ]
 

compiler/dcalc/invariant.ml

@@ -41,6 +41,7 @@ let check_invariant
     (inv : invariant_expr)
     (p : typed program) =
   let result = ref true in
+  let _ = name in
   let p' =
     Program.map_exprs p ~varf:Fun.id ~f:(fun e ->
         let rec f e =
@@ -48,12 +49,13 @@ let check_invariant
             match inv e with
             | None -> true
             | Some false ->
-              Errors.format_spanned_warning (Expr.pos e)
+              Cli.error_print "%s Invariant failed."
-                "Internal Error: Invalid structural invariant %a. The \
+                (Pos.to_string_short (Expr.pos e));
-                 expression with type  %a. Full term: %a"
+              (* Errors.format_spanned_warning (Expr.pos e) "Internal Error:
-                Format.(pp_print_option (fun fmt -> Format.fprintf fmt "(%s)"))
+                 Invalid structural invariant %a. The \ expression with type %a.
-                name (Print.typ p.decl_ctx) (Expr.ty e) (Print.expr p.decl_ctx)
+                 Full term: %a" Format.(pp_print_option (fun fmt ->
-                e;
+                 Format.fprintf fmt "(%s)")) name (Print.typ p.decl_ctx)
+                 (Expr.ty e) (Print.expr p.decl_ctx) e; *)
               false
             | Some true ->
               (* Cli.result_format "Structural invariant verified %a"
@@ -68,7 +70,4 @@ let check_invariant
         result := res && !result;
         e')
   in
-  assert (Bindlib.free_vars p' = Bindlib.empty_ctxt);
+  assert (Bindlib.free_vars p' = Bindlib.empty_ctxt)
-  if not !result then
-    Errors.raise_internal_error
-      "Structural invariant not valid! See above for more informations."

compiler/driver.ml

@@ -146,7 +146,7 @@ let driver source_file (options : Cli.options) : int =
                 language fmt (fun fmt -> weave_output fmt prgm)
           else weave_output fmt prgm)
     | ( `Interpret | `Typecheck | `OCaml | `Python | `Scalc | `Lcalc | `Dcalc
-      | `Scopelang | `Proof | `Plugin _ ) as backend -> (
+      | `Scopelang | `Proof | `DcalcInvariants | `Plugin _ ) as backend -> (
       Cli.debug_print "Name resolution...";
       let ctxt = Desugared.Name_resolution.form_context prgm in
       let scope_uid =
@@ -194,7 +194,7 @@ let driver source_file (options : Cli.options) : int =
             (Scopelang.Print.program ~debug:options.debug)
             prgm
       | ( `Interpret | `Typecheck | `OCaml | `Python | `Scalc | `Lcalc | `Dcalc
-        | `Proof | `Plugin _ ) as backend -> (
+        | `Proof | `DcalcInvariants | `Plugin _ ) as backend -> (
         Cli.debug_print "Typechecking...";
         let type_ordering =
           Scopelang.Dependency.check_type_cycles prgm.program_ctx.ctx_structs
@@ -251,8 +251,8 @@ let driver source_file (options : Cli.options) : int =
             Format.fprintf fmt "%a\n"
               (Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx)
               prgrm_dcalc_expr
-        | (`Interpret | `OCaml | `Python | `Scalc | `Lcalc | `Proof | `Plugin _)
+        | ( `Interpret | `OCaml | `Python | `Scalc | `Lcalc | `Proof
-          as backend -> (
+          | `DcalcInvariants | `Plugin _ ) as backend -> (
           Cli.debug_print "Typechecking again...";
           let prgm =
             try Shared_ast.Typing.program prgm
@@ -274,6 +274,16 @@ let driver source_file (options : Cli.options) : int =
             in
 
             Verification.Solver.solve_vc prgm.decl_ctx vcs
+          | `DcalcInvariants ->
+            Cli.debug_format "Checking invariants";
+            let open Dcalc.Invariant in
+            check_invariant ~name:"default_no_arrow" invariant_default_no_arrow
+              prgm;
+            check_invariant ~name:"no_partial_evaluation"
+              invariant_no_partial_evaluation prgm;
+            check_invariant ~name:"no_return_a_function"
+              invariant_no_return_a_function prgm;
+            Cli.debug_format "Finished checking invariants"
           | `Interpret ->
             Cli.debug_print "Starting interpretation...";
             let prgrm_dcalc_expr =