Include Bindlib_ext to Expr.Box

compiler/catala_utils/bindlib_ext.ml

@@ -1,49 +0,0 @@
-(* 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. *)
-
-module Ren = struct
-  module Set = Set.Make (String)
-
-  type ctxt = Set.t
-
-  let skip_constant_binders = true
-  let reset_context_for_closed_terms = true
-  let constant_binder_name = None
-  let empty_ctxt = Set.empty
-  let reserve_name n s = Set.add n s
-  let new_name n s = n, Set.add n s
-end
-
-module Ctx = Bindlib.Ctxt (Ren)
-
-let fv b = Ren.Set.elements (Ctx.free_vars b)
-
-let assert_closed b =
-  match fv b with
-  | [] -> ()
-  | [h] ->
-    Errors.raise_internal_error
-      "The boxed term is not closed the variable %s is free in the global \
-       context"
-      h
-  | l ->
-    Errors.raise_internal_error
-      "The boxed term is not closed the variables %a is free in the global \
-       context"
-      (Format.pp_print_list
-         ~pp_sep:(fun fmt () -> Format.pp_print_string fmt "; ")
-         Format.pp_print_string)
-      l

compiler/catala_utils/bindlib_ext.mli

@@ -1,22 +0,0 @@
-(* 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. *)
-
-val fv : 'b Bindlib.box -> string list
-(** [fv] return the list of free variables from a boxed term. *)
-
-val assert_closed : 'b Bindlib.box -> unit
-(** [assert_closed b] check there is no free variables in then [b] boxed term.
-    It raises an internal error if it not the case, printing all free variables. *)

compiler/lcalc/compile_without_exceptions.ml

@@ -844,7 +844,7 @@ let translate_program (prgm : typed D.program) : untyped A.program =
 
   let code_items = trans_code_items Var.Map.empty prgm.code_items in
 
-  Bindlib_ext.assert_closed code_items;
+  Expr.Box.assert_closed code_items;
 
   (* program is closed here. *)
   let code_items = Bindlib.unbox code_items in

compiler/lcalc/optimizations.ml

@@ -189,7 +189,7 @@ let rec fix_opti
     expression of the program [p]. *)
 let lift_optim f p =
   let code_items = Scope.map_exprs ~f ~varf:(fun v -> v) p.code_items in
-  Bindlib_ext.assert_closed code_items;
+  Expr.Box.assert_closed code_items;
   let prgm = { p with code_items = Bindlib.unbox code_items } in
   prgm
 

compiler/shared_ast/expr.ml

@@ -68,6 +68,40 @@ module Box = struct
   module LiftScopeVars = Bindlib.Lift (ScopeVar.Map)
 
   let lift_scope_vars = LiftScopeVars.lift_box
+
+  module Ren = struct
+    module Set = Set.Make (String)
+
+    type ctxt = Set.t
+
+    let skip_constant_binders = true
+    let reset_context_for_closed_terms = true
+    let constant_binder_name = None
+    let empty_ctxt = Set.empty
+    let reserve_name n s = Set.add n s
+    let new_name n s = n, Set.add n s
+  end
+
+  module Ctx = Bindlib.Ctxt (Ren)
+
+  let fv b = Ren.Set.elements (Ctx.free_vars b)
+
+  let assert_closed b =
+    match fv b with
+    | [] -> ()
+    | [h] ->
+      Errors.raise_internal_error
+        "The boxed term is not closed the variable %s is free in the global \
+         context"
+        h
+    | l ->
+      Errors.raise_internal_error
+        "The boxed term is not closed the variables %a is free in the global \
+         context"
+        (Format.pp_print_list
+           ~pp_sep:(fun fmt () -> Format.pp_print_string fmt "; ")
+           Format.pp_print_string)
+        l
 end
 
 let bind vars e = Bindlib.bind_mvar vars (Box.lift e)

compiler/shared_ast/expr.mli

@@ -437,4 +437,12 @@ module Box : sig
     ('a, 't) naked_gexpr) ->
     't ->
     ('a, 't) boxed_gexpr
+
+  val fv : 'b Bindlib.box -> string list
+  (** [fv] return the list of free variables from a boxed term. *)
+
+  val assert_closed : 'b Bindlib.box -> unit
+  (** [assert_closed b] check there is no free variables in then [b] boxed term.
+      It raises an internal error if it not the case, printing all free
+      variables. *)
 end

compiler/shared_ast/program.ml

@@ -70,7 +70,7 @@ let to_expr p main_scope =
       (Scope.get_body_mark main_scope_body)
       (ScopeName main_scope)
   in
-  Catala_utils.Bindlib_ext.assert_closed (Expr.Box.lift res);
+  Expr.Box.assert_closed (Expr.Box.lift res);
   res
 
 let equal p p' =