Trying to box everything but optimizations complaining

compiler/dcalc/ast.ml

@@ -138,12 +138,12 @@ type scope_let = {
   scope_let_var : expr Bindlib.var Pos.marked;
   scope_let_kind : scope_let_kind;
   scope_let_typ : typ Pos.marked;
-  scope_let_expr : expr Pos.marked;
+  scope_let_expr : expr Pos.marked Bindlib.box;
 }
 
 type scope_body = {
   scope_body_lets : scope_let list;
-  scope_body_result : expr Pos.marked;
+  scope_body_result : expr Pos.marked Bindlib.box;
   scope_body_arg : expr Bindlib.var;
   scope_body_input_struct : StructName.t;
   scope_body_output_struct : StructName.t;
@@ -187,12 +187,9 @@ let build_whole_scope_expr (ctx : decl_ctx) (body : scope_body) (pos_scope : Pos
       (fun scope_let acc ->
         make_let_in
           (Pos.unmark scope_let.scope_let_var)
-          scope_let.scope_let_typ
-          (Bindlib.box scope_let.scope_let_expr)
-          acc
+          scope_let.scope_let_typ scope_let.scope_let_expr acc
           (Pos.get_position scope_let.scope_let_var))
-      body.scope_body_lets
-      (Bindlib.box body.scope_body_result)
+      body.scope_body_lets body.scope_body_result
   in
   make_abs
     (Array.of_list [ body.scope_body_arg ])

compiler/dcalc/ast.mli

@@ -147,7 +147,7 @@ type scope_let = {
   scope_let_var : expr Bindlib.var Pos.marked;
   scope_let_kind : scope_let_kind;
   scope_let_typ : typ Pos.marked;
-  scope_let_expr : expr Pos.marked;
+  scope_let_expr : expr Pos.marked Bindlib.box;
 }
 (** A scope let-binding has all the information necessary to make a proper let-binding expression,
     plus an annotation for the kind of the let-binding that comes from the compilation of a
@@ -155,7 +155,7 @@ type scope_let = {
 
 type scope_body = {
   scope_body_lets : scope_let list;
-  scope_body_result : expr Pos.marked;
+  scope_body_result : expr Pos.marked Bindlib.box;
   scope_body_arg : expr Bindlib.var;
   scope_body_input_struct : StructName.t;
   scope_body_output_struct : StructName.t;

compiler/dcalc/optimizations.ml

@@ -14,56 +14,63 @@
 open Utils
 open Ast
 
-let rec peephole_expr (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
-  match Pos.unmark e with
-  | EVar (v, pos) -> Bindlib.box_apply (fun v -> (v, pos)) (Bindlib.box_var v)
-  | ETuple (args, n) ->
-      Bindlib.box_apply
-        (fun args -> (ETuple (args, n), Pos.get_position e))
-        (Bindlib.box_list (List.map peephole_expr args))
-  | ETupleAccess (e1, i, n, ts) ->
-      Bindlib.box_apply
-        (fun e1 -> (ETupleAccess (e1, i, n, ts), Pos.get_position e))
-        (peephole_expr e1)
-  | EInj (e1, i, n, ts) ->
-      Bindlib.box_apply (fun e1 -> (EInj (e1, i, n, ts), Pos.get_position e)) (peephole_expr e1)
-  | EMatch (arg, cases, n) ->
-      Bindlib.box_apply2
-        (fun arg cases -> (EMatch (arg, cases, n), Pos.get_position e))
-        (peephole_expr arg)
-        (Bindlib.box_list (List.map peephole_expr cases))
-  | EArray args ->
-      Bindlib.box_apply
-        (fun args -> (EArray args, Pos.get_position e))
-        (Bindlib.box_list (List.map peephole_expr args))
-  | EAbs ((binder, pos_binder), ts) ->
-      let vars, body = Bindlib.unmbind binder in
-      let body = peephole_expr body in
-      Bindlib.box_apply
-        (fun binder -> (EAbs ((binder, pos_binder), ts), Pos.get_position e))
-        (Bindlib.bind_mvar vars body)
-  | EApp (e1, args) ->
-      Bindlib.box_apply2
-        (fun e1 args -> (EApp (e1, args), Pos.get_position e))
-        (peephole_expr e1)
-        (Bindlib.box_list (List.map peephole_expr args))
-  | ErrorOnEmpty e1 ->
-      Bindlib.box_apply (fun e1 -> (ErrorOnEmpty e1, Pos.get_position e)) (peephole_expr e1)
-  | EAssert e1 -> Bindlib.box_apply (fun e1 -> (EAssert e1, Pos.get_position e)) (peephole_expr e1)
-  | EIfThenElse (e1, e2, e3) ->
-      Bindlib.box_apply3
-        (fun e1 e2 e3 -> (EIfThenElse (e1, e2, e3), Pos.get_position e))
-        (peephole_expr e1) (peephole_expr e2) (peephole_expr e3)
-  | EDefault (exceptions, just, cons) ->
-      Bindlib.box_apply3
-        (fun exceptions just cons ->
-          ( (match exceptions with
-            | [] -> EIfThenElse (just, cons, (ELit LEmptyError, Pos.get_position e))
-            | _ -> EDefault (exceptions, just, cons)),
-            Pos.get_position e ))
-        (Bindlib.box_list (List.map peephole_expr exceptions))
-        (peephole_expr just) (peephole_expr cons)
-  | ELit _ | EOp _ -> Bindlib.box e
+let rec peephole_expr (e : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
+  Bindlib.unbox
+    (Bindlib.box_apply
+       (fun e ->
+         match Pos.unmark e with
+         | EVar (v, pos) -> Bindlib.box_apply (fun v -> (v, pos)) (Bindlib.box_var v)
+         | ETuple (args, n) ->
+             Bindlib.box_apply
+               (fun args -> (ETuple (args, n), Pos.get_position e))
+               (Bindlib.box_list (List.map peephole_expr args))
+         | ETupleAccess (e1, i, n, ts) ->
+             Bindlib.box_apply
+               (fun e1 -> (ETupleAccess (e1, i, n, ts), Pos.get_position e))
+               (peephole_expr e1)
+         | EInj (e1, i, n, ts) ->
+             Bindlib.box_apply
+               (fun e1 -> (EInj (e1, i, n, ts), Pos.get_position e))
+               (peephole_expr e1)
+         | EMatch (arg, cases, n) ->
+             Bindlib.box_apply2
+               (fun arg cases -> (EMatch (arg, cases, n), Pos.get_position e))
+               (peephole_expr arg)
+               (Bindlib.box_list (List.map peephole_expr cases))
+         | EArray args ->
+             Bindlib.box_apply
+               (fun args -> (EArray args, Pos.get_position e))
+               (Bindlib.box_list (List.map peephole_expr args))
+         | EAbs ((binder, pos_binder), ts) ->
+             let vars, body = Bindlib.unmbind binder in
+             let body = peephole_expr body in
+             Bindlib.box_apply
+               (fun binder -> (EAbs ((binder, pos_binder), ts), Pos.get_position e))
+               (Bindlib.bind_mvar vars body)
+         | EApp (e1, args) ->
+             Bindlib.box_apply2
+               (fun e1 args -> (EApp (e1, args), Pos.get_position e))
+               (peephole_expr e1)
+               (Bindlib.box_list (List.map peephole_expr args))
+         | ErrorOnEmpty e1 ->
+             Bindlib.box_apply (fun e1 -> (ErrorOnEmpty e1, Pos.get_position e)) (peephole_expr e1)
+         | EAssert e1 ->
+             Bindlib.box_apply (fun e1 -> (EAssert e1, Pos.get_position e)) (peephole_expr e1)
+         | EIfThenElse (e1, e2, e3) ->
+             Bindlib.box_apply3
+               (fun e1 e2 e3 -> (EIfThenElse (e1, e2, e3), Pos.get_position e))
+               (peephole_expr e1) (peephole_expr e2) (peephole_expr e3)
+         | EDefault (exceptions, just, cons) ->
+             Bindlib.box_apply3
+               (fun exceptions just cons ->
+                 ( (match exceptions with
+                   | [] -> EIfThenElse (just, cons, (ELit LEmptyError, Pos.get_position e))
+                   | _ -> EDefault (exceptions, just, cons)),
+                   Pos.get_position e ))
+               (Bindlib.box_list (List.map peephole_expr exceptions))
+               (peephole_expr just) (peephole_expr cons)
+         | ELit _ | EOp _ -> Bindlib.box e)
+       e)
 
 let peephole_optimizations (p : program) : program =
   {
@@ -78,12 +85,9 @@ let peephole_optimizations (p : program) : program =
               scope_body_lets =
                 List.map
                   (fun let_binding ->
-                    {
-                      let_binding with
-                      scope_let_expr = Bindlib.unbox (peephole_expr let_binding.scope_let_expr);
-                    })
+                    { let_binding with scope_let_expr = peephole_expr let_binding.scope_let_expr })
                   body.scope_body_lets;
-              scope_body_result = Bindlib.unbox (peephole_expr body.scope_body_result);
+              scope_body_result = peephole_expr body.scope_body_result;
             } ))
         p.scopes;
   }

compiler/scopelang/scope_to_dcalc.ml

@@ -308,7 +308,7 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
           {
             Dcalc.Ast.scope_let_var = (a_var, Pos.get_position a);
             Dcalc.Ast.scope_let_typ = tau;
-            Dcalc.Ast.scope_let_expr = Bindlib.unbox merged_expr;
+            Dcalc.Ast.scope_let_expr = merged_expr;
             Dcalc.Ast.scope_let_kind = Dcalc.Ast.ScopeVarDefinition;
           };
         ],
@@ -342,7 +342,7 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
             Dcalc.Ast.scope_let_var = (a_var, Pos.get_position a_name);
             Dcalc.Ast.scope_let_typ =
               (Dcalc.Ast.TArrow ((TLit TUnit, var_def_pos), tau), var_def_pos);
-            Dcalc.Ast.scope_let_expr = Bindlib.unbox thunked_new_e;
+            Dcalc.Ast.scope_let_expr = thunked_new_e;
             Dcalc.Ast.scope_let_kind = Dcalc.Ast.SubScopeVarDefinition;
           };
         ],
@@ -438,7 +438,7 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
           Dcalc.Ast.scope_let_var = (result_tuple_var, pos_sigma);
           Dcalc.Ast.scope_let_kind = Dcalc.Ast.CallingSubScope;
           Dcalc.Ast.scope_let_typ = result_tuple_typ;
-          Dcalc.Ast.scope_let_expr = Bindlib.unbox call_expr;
+          Dcalc.Ast.scope_let_expr = call_expr;
         }
       in
       let result_bindings_lets =
@@ -449,16 +449,15 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
               Dcalc.Ast.scope_let_typ = (tau, pos_sigma);
               Dcalc.Ast.scope_let_kind = Dcalc.Ast.DestructuringSubScopeResults;
               Dcalc.Ast.scope_let_expr =
-                Bindlib.unbox
-                  (Bindlib.box_apply
-                     (fun r ->
-                       ( Dcalc.Ast.ETupleAccess
-                           ( r,
-                             i,
-                             Some called_scope_return_struct,
-                             List.map (fun (_, t, _) -> (t, pos_sigma)) all_subscope_vars_dcalc ),
-                         pos_sigma ))
-                     (Dcalc.Ast.make_var (result_tuple_var, pos_sigma)));
+                Bindlib.box_apply
+                  (fun r ->
+                    ( Dcalc.Ast.ETupleAccess
+                        ( r,
+                          i,
+                          Some called_scope_return_struct,
+                          List.map (fun (_, t, _) -> (t, pos_sigma)) all_subscope_vars_dcalc ),
+                      pos_sigma ))
+                  (Dcalc.Ast.make_var (result_tuple_var, pos_sigma));
             })
           all_subscope_vars_dcalc
       in
@@ -480,8 +479,7 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
               (Dcalc.Ast.Var.make ("_", Pos.get_position e), Pos.get_position e);
             Dcalc.Ast.scope_let_typ = (Dcalc.Ast.TLit TUnit, Pos.get_position e);
             Dcalc.Ast.scope_let_expr =
-              Bindlib.unbox
-                (Bindlib.box_apply (fun new_e -> Pos.same_pos_as (Dcalc.Ast.EAssert new_e) e) new_e);
+              Bindlib.box_apply (fun new_e -> Pos.same_pos_as (Dcalc.Ast.EAssert new_e) e) new_e;
             Dcalc.Ast.scope_let_kind = Dcalc.Ast.Assertion;
           };
         ],
@@ -538,20 +536,19 @@ let translate_scope_decl (struct_ctx : Ast.struct_ctx) (enum_ctx : Ast.enum_ctx)
           Dcalc.Ast.scope_let_var = (v, pos_sigma);
           Dcalc.Ast.scope_let_typ = (tau, pos_sigma);
           Dcalc.Ast.scope_let_expr =
-            Bindlib.unbox
-              (Bindlib.box_apply
-                 (fun r ->
-                   ( Dcalc.Ast.ETupleAccess
-                       ( r,
-                         i,
-                         Some scope_input_struct_name,
-                         List.map
-                           (fun (_, t, _) ->
-                             ( Dcalc.Ast.TArrow ((Dcalc.Ast.TLit TUnit, pos_sigma), (t, pos_sigma)),
-                               pos_sigma ))
-                           scope_variables ),
-                     pos_sigma ))
-                 (Dcalc.Ast.make_var (scope_input_var, pos_sigma)));
+            Bindlib.box_apply
+              (fun r ->
+                ( Dcalc.Ast.ETupleAccess
+                    ( r,
+                      i,
+                      Some scope_input_struct_name,
+                      List.map
+                        (fun (_, t, _) ->
+                          ( Dcalc.Ast.TArrow ((Dcalc.Ast.TLit TUnit, pos_sigma), (t, pos_sigma)),
+                            pos_sigma ))
+                        scope_variables ),
+                  pos_sigma ))
+              (Dcalc.Ast.make_var (scope_input_var, pos_sigma));
         })
       scope_variables
   in
@@ -580,7 +577,7 @@ let translate_scope_decl (struct_ctx : Ast.struct_ctx) (enum_ctx : Ast.enum_ctx)
   in
   ( {
       Dcalc.Ast.scope_body_lets = input_destructurings @ rules;
-      Dcalc.Ast.scope_body_result = return_exp;
+      Dcalc.Ast.scope_body_result = Bindlib.box return_exp;
       Dcalc.Ast.scope_body_input_struct = scope_input_struct_name;
       Dcalc.Ast.scope_body_output_struct = scope_return_struct_name;
       Dcalc.Ast.scope_body_arg = scope_input_var;