From 622feec9a5be1987c39748f37e81f017c4c9c4bb Mon Sep 17 00:00:00 2001
From: adelaett <90894311+adelaett@users.noreply.github.com>
Date: Fri, 14 Apr 2023 11:32:49 +0200
Subject: [PATCH] change Invariants choice to --check_invariants flag

---
 compiler/catala_utils/cli.ml       | 15 +++++++++++---
 compiler/catala_utils/cli.mli      |  8 ++++++--
 compiler/catala_web_interpreter.ml |  1 +
 compiler/driver.ml                 | 32 ++++++++++++++----------------
 4 files changed, 34 insertions(+), 22 deletions(-)

diff --git a/compiler/catala_utils/cli.ml b/compiler/catala_utils/cli.ml
index 087a17ee..4ce00ab0 100644
--- a/compiler/catala_utils/cli.ml
+++ b/compiler/catala_utils/cli.ml
@@ -30,7 +30,6 @@ type backend_option_builtin =
   | `Dcalc
   | `Scopelang
   | `Proof
-  | `DcalcInvariants
   | `Interpret_Lcalc ]
 
 type 'a backend_option = [ backend_option_builtin | `Plugin of 'a ]
@@ -56,7 +55,6 @@ let backend_option_to_string = function
   | `Typecheck -> "Typecheck"
   | `Scalc -> "Scalc"
   | `Lcalc -> "Lcalc"
-  | `DcalcInvariants -> "invariants"
   | `Plugin s -> s
 
 let backend_option_of_string backend =
@@ -74,7 +72,6 @@ let backend_option_of_string backend =
   | "typecheck" -> `Typecheck
   | "scalc" -> `Scalc
   | "lcalc" -> `Lcalc
-  | "invariants" -> `DcalcInvariants
   | s -> `Plugin s
 
 (** Source files to be compiled *)
@@ -96,6 +93,7 @@ let disable_warnings_flag = ref false
 let optimize_flag = ref false
 let disable_counterexamples = ref false
 let avoid_exceptions_flag = ref false
+let check_invariants_flag = ref false
 
 open Cmdliner
 
@@ -149,6 +147,12 @@ let disable_warnings_opt =
     & info ["disable_warnings"]
         ~doc:"Disable all the warnings emitted by the compiler.")
 
+let check_invariants_opt =
+  Arg.(
+    value
+    & flag
+    & info ["check_invariants"] ~doc:"Check structural invariants on the AST.")
+
 let avoid_exceptions =
   Arg.(
     value
@@ -259,6 +263,7 @@ type options = {
   trace : bool;
   disable_warnings : bool;
   disable_counterexamples : bool;
+  check_invariants : bool;
   optimize : bool;
   ex_scope : string option;
   output_file : string option;
@@ -282,6 +287,7 @@ let options =
       trace
       disable_counterexamples
       optimize
+      check_invariants
       ex_scope
       output_file
       print_only_law : options =
@@ -298,6 +304,7 @@ let options =
       trace;
       disable_counterexamples;
       optimize;
+      check_invariants;
       ex_scope;
       output_file;
       closure_conversion;
@@ -320,6 +327,7 @@ let options =
     $ trace_opt
     $ disable_counterexamples_opt
     $ optimize
+    $ check_invariants_opt
     $ ex_scope
     $ output
     $ print_only_law)
@@ -339,6 +347,7 @@ let set_option_globals options : unit =
   disable_warnings_flag := options.disable_warnings;
   trace_flag := options.trace;
   optimize_flag := options.optimize;
+  check_invariants_flag := options.check_invariants;
   disable_counterexamples := options.disable_counterexamples;
   avoid_exceptions_flag := options.avoid_exceptions
 
diff --git a/compiler/catala_utils/cli.mli b/compiler/catala_utils/cli.mli
index ecf63021..4c4cf181 100644
--- a/compiler/catala_utils/cli.mli
+++ b/compiler/catala_utils/cli.mli
@@ -30,8 +30,7 @@ type backend_option_builtin =
   | `Lcalc
   | `Dcalc
   | `Scopelang
-  | `Proof
-  | `DcalcInvariants ]
+  | `Proof ]
 
 type 'a backend_option = [ backend_option_builtin | `Plugin of 'a ]
 
@@ -68,6 +67,9 @@ val max_prec_digits : int ref
 val trace_flag : bool ref
 val disable_warnings_flag : bool ref
 
+val check_invariants_flag : bool ref
+(** Check structural invariants on the AST. *)
+
 val disable_counterexamples : bool ref
 (** Disables model-generated counterexamples for proofs that fail. *)
 
@@ -80,6 +82,7 @@ val file : string Cmdliner.Term.t
 val debug : bool Cmdliner.Term.t
 val unstyled : bool Cmdliner.Term.t
 val trace_opt : bool Cmdliner.Term.t
+val check_invariants_opt : bool Cmdliner.Term.t
 val wrap_weaved_output : bool Cmdliner.Term.t
 val print_only_law : bool Cmdliner.Term.t
 val backend : string Cmdliner.Term.t
@@ -104,6 +107,7 @@ type options = {
   trace : bool;
   disable_warnings : bool;
   disable_counterexamples : bool;
+  check_invariants : bool;
   optimize : bool;
   ex_scope : string option;
   output_file : string option;
diff --git a/compiler/catala_web_interpreter.ml b/compiler/catala_web_interpreter.ml
index e565181f..e1843ef7 100644
--- a/compiler/catala_web_interpreter.ml
+++ b/compiler/catala_web_interpreter.ml
@@ -26,6 +26,7 @@ let _ =
              disable_warnings = true;
              disable_counterexamples = false;
              optimize = false;
+             check_invariants = false;
              ex_scope = Some (Js.to_string scope);
              output_file = None;
              print_only_law = false;
diff --git a/compiler/driver.ml b/compiler/driver.ml
index 76f33922..a16337b0 100644
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@@ -140,8 +140,7 @@ let driver source_file (options : Cli.options) : int =
                 language fmt (fun fmt -> weave_output fmt prgm)
           else weave_output fmt prgm)
     | ( `Interpret | `Interpret_Lcalc | `Typecheck | `OCaml | `Python | `Scalc
-      | `Lcalc | `Dcalc | `Scopelang | `Proof | `DcalcInvariants | `Plugin _ )
-      as backend -> (
+      | `Lcalc | `Dcalc | `Scopelang | `Proof | `Plugin _ ) as backend -> (
       Cli.debug_print "Name resolution...";
       let ctxt = Desugared.Name_resolution.form_context prgm in
       let scope_uid =
@@ -191,8 +190,7 @@ let driver source_file (options : Cli.options) : int =
             (Scopelang.Print.program ~debug:options.debug)
             prgm
       | ( `Interpret | `Interpret_Lcalc | `Typecheck | `OCaml | `Python | `Scalc
-        | `Lcalc | `Dcalc | `Proof | `DcalcInvariants | `Plugin _ ) as backend
-        -> (
+        | `Lcalc | `Dcalc | `Proof | `Plugin _ ) as backend -> (
         Cli.debug_print "Typechecking...";
         let type_ordering =
           Scopelang.Dependency.check_type_cycles prgm.program_ctx.ctx_structs
@@ -250,7 +248,7 @@ let driver source_file (options : Cli.options) : int =
               (Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx)
               prgrm_dcalc_expr
         | ( `Interpret | `OCaml | `Python | `Scalc | `Lcalc | `Proof | `Plugin _
-          | `Interpret_Lcalc | `DcalcInvariants ) as backend -> (
+          | `Interpret_Lcalc ) as backend -> (
           Cli.debug_print "Typechecking again...";
           let prgm =
             try Shared_ast.Typing.program ~leave_unresolved:false prgm
@@ -262,17 +260,7 @@ let driver source_file (options : Cli.options) : int =
               in
               raise (Errors.StructuredError (msg, details))
           in
-          match backend with
-          | `Proof ->
-            let vcs =
-              Verification.Conditions.generate_verification_conditions prgm
-                (match options.ex_scope with
-                | None -> None
-                | Some _ -> Some scope_uid)
-            in
-
-            Verification.Solver.solve_vc prgm.decl_ctx vcs
-          | `DcalcInvariants ->
+          if !Cli.check_invariants_flag then (
             Cli.debug_format "Checking invariants";
             let open Dcalc.Invariants in
             let result =
@@ -287,7 +275,17 @@ let driver source_file (options : Cli.options) : int =
             in
 
             if result then Cli.debug_format "Finished checking invariants"
-            else raise (Errors.raise_error "Invariant invalid")
+            else raise (Errors.raise_error "Invariant invalid"));
+          match backend with
+          | `Proof ->
+            let vcs =
+              Verification.Conditions.generate_verification_conditions prgm
+                (match options.ex_scope with
+                | None -> None
+                | Some _ -> Some scope_uid)
+            in
+
+            Verification.Solver.solve_vc prgm.decl_ctx vcs
           | `Interpret ->
             Cli.debug_print "Starting interpretation (dcalc)...";
             let results =