invariant mli

compiler/dcalc/invariants.ml

@@ -1,3 +1,19 @@
+(* This file is part of the Catala compiler, a specification language for tax
+   and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
+   Alain Delaët <alain.delaet--tixeuil@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 Shared_ast
 open Ast
 open Catala_utils
@@ -5,6 +21,43 @@ open Catala_utils
 type invariant_status = Fail | Pass | Ignore
 type invariant_expr = typed expr -> invariant_status
 
+let check_invariant (inv : string * invariant_expr) (p : typed program) : bool =
+  (* TODO: add a Program.fold_exprs to get rid of the reference 0:-)? *)
+  let result = ref true in
+  let name, inv = inv in
+  let _ = name in
+  let total = ref 0 in
+  let ok = ref 0 in
+  let p' =
+    Program.map_exprs p ~varf:Fun.id ~f:(fun e ->
+        (* let currente = e in *)
+        let rec f e =
+          let r =
+            match inv e with
+            | Ignore -> true
+            | Fail ->
+              Cli.error_format "%s failed in %s.\n\n %a" name
+                (Pos.to_string_short (Expr.pos e))
+                (Print.expr ~debug:true p.decl_ctx)
+                e;
+              incr total;
+              false
+            | Pass ->
+              incr ok;
+              incr total;
+              true
+          in
+          Expr.map_gather e ~acc:r ~join:( && ) ~f
+        in
+
+        let res, e' = f e in
+        result := res && !result;
+        e')
+  in
+  assert (Bindlib.free_vars p' = Bindlib.empty_ctxt);
+  Cli.result_print "Invariant %s\n   checked. result: [%d/%d]" name !ok !total;
+  !result
+
 (* Structural invariant: no default can have as type A -> B *)
 let invariant_default_no_arrow () : string * invariant_expr =
   ( __FUNCTION__,
@@ -70,40 +123,3 @@ let invariant_match_inversion () : string * invariant_expr =
         then Pass
         else Fail
       | _ -> Ignore )
-
-let check_invariant (inv : string * invariant_expr) (p : typed program) : bool =
-  (* TODO: add a Program.fold_exprs to get rid of the reference 0:-)? *)
-  let result = ref true in
-  let name, inv = inv in
-  let _ = name in
-  let total = ref 0 in
-  let ok = ref 0 in
-  let p' =
-    Program.map_exprs p ~varf:Fun.id ~f:(fun e ->
-        (* let currente = e in *)
-        let rec f e =
-          let r =
-            match inv e with
-            | Ignore -> true
-            | Fail ->
-              Cli.error_format "%s failed in %s.\n\n %a" name
-                (Pos.to_string_short (Expr.pos e))
-                (Print.expr ~debug:true p.decl_ctx)
-                e;
-              incr total;
-              false
-            | Pass ->
-              incr ok;
-              incr total;
-              true
-          in
-          Expr.map_gather e ~acc:r ~join:( && ) ~f
-        in
-
-        let res, e' = f e in
-        result := res && !result;
-        e')
-  in
-  assert (Bindlib.free_vars p' = Bindlib.empty_ctxt);
-  Cli.result_print "Invariant %s\n   checked. result: [%d/%d]" name !ok !total;
-  !result

compiler/dcalc/invariants.mli

@@ -0,0 +1,50 @@
+(* This file is part of the Catala compiler, a specification language for tax
+   and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
+   Alain Delaët <alain.delaet--tixeuil@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. *)
+
+(** This file makes explicit few structural invariants of the dcalc asbtract
+    syntax tree. Those invariants have been checked on all tests and examples of
+    catala. The behavior of the compiler on programs that don't follow those
+    invariant in undefined. *)
+
+open Shared_ast
+open Ast
+open Catala_utils
+
+type invariant_status = Fail | Pass | Ignore
+type invariant_expr = typed expr -> invariant_status
+
+val check_invariant : string * invariant_expr -> typed program -> bool
+(** Expression invariants are then lifted toward program invariants using
+    catala's utility combinators using the [check invariant] function. *)
+
+val invariant_default_no_arrow : unit -> string * invariant_expr
+(** [invariant_default_no_arrow] check no default term has a function type. *)
+
+val invariant_no_partial_evaluation : unit -> string * invariant_expr
+(** [invariant_no_partial_evaluation] check there is no partial function. *)
+
+val invariant_no_return_a_function : unit -> string * invariant_expr
+(** [invariant_no_return_a_function] check no function return a function. *)
+
+val invariant_app_inversion : unit -> string * invariant_expr
+(** [invariant_app_inversion] : if the term is an function application, then
+    there is only 5 possibility : it is a let binding, it is an operator
+    application, it is an variable application, it is a struct access function
+    application (sub-scope call), or it is a operator application with trace. *)
+
+val invariant_match_inversion : unit -> string * invariant_expr
+(** [invariant_match_inversion] : if a term is a match, then every branch is an
+    function abstraction. *)