unboxing scope_let and scope_body in dcalc

[adelaett]

Currently in dcalc, we have an anotation on each scope let biding indicating what kind is it. This was required for the compilation without exceptions (#158) since some but not all of the let in could raise empty errors. We hence have something in the form :

type scope_let_kind =
  | DestructuringInputStruct
  | ScopeVarDefinition
  | SubScopeVarDefinition
  | CallingSubScope
  | DestructuringSubScopeResults
  | Assertion

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 Bindlib.box;
}

type scope_body = {
  scope_body_lets : scope_let list;
  scope_body_result : expr Pos.marked Bindlib.box;
  (* {x1 = x1; x2 = x2; x3 = x3; ... } *)
  scope_body_arg : expr Bindlib.var;
  (* x: input_struct *)
  scope_body_input_struct : StructName.t;
  scope_body_output_struct : StructName.t;
}

However, this form contains expr Bindlib.box and expr Bindlib.var at some places, making it hard to match on the expressions.

The idea of this change is to have an other representation of scope_let and scope_body using Bindlib.binder.

type scope_lets =
  | Result of D.expr Pos.marked
  | ScopeLet of {
      scope_let_kind : D.scope_let_kind;
      scope_let_typ : D.typ Pos.marked;
      scope_let_expr : D.expr Pos.marked;
      scope_let_next : (D.expr, scope_lets) Bindlib.binder;
      scope_let_pos : Pos.t;
    }

type scope_body = {
  scope_body_input_struct : D.StructName.t;
  scope_body_output_struct : D.StructName.t;
  scope_body_result : (D.expr, scope_lets) Bindlib.binder;
}

This is used inside the compilation_without_exception.ml of #158 and it is possible to convert to

let translate_and_bind_lets (acc : scope_lets Bindlib.box) (scope_let : D.scope_let) :
    scope_lets Bindlib.box =
  let pos = snd scope_let.D.scope_let_var in

  let binder = Bindlib.bind_var (fst scope_let.D.scope_let_var) acc in
  Bindlib.box_apply2
    (fun expr binder ->
      ScopeLet
        {
          scope_let_kind = scope_let.D.scope_let_kind;
          scope_let_typ = scope_let.D.scope_let_typ;
          scope_let_expr = expr;
          scope_let_next = binder;
          scope_let_pos = pos;
        })
    scope_let.D.scope_let_expr binder

let translate_and_bind (body : D.scope_body) : scope_body Bindlib.box =
  let body_result =
    ListLabels.fold_right body.D.scope_body_lets
      ~init:(Bindlib.box_apply (fun e -> Result e) body.D.scope_body_result)
      ~f:(Fun.flip translate_and_bind_lets)
  in

  Bindlib.box_apply
    (fun scope_body_result ->
      {
        scope_body_output_struct = body.D.scope_body_output_struct;
        scope_body_input_struct = body.D.scope_body_input_struct;
        scope_body_result;
      })
    scope_body_result

To make this change, we need to update code that uses this form

• [ ] make the actual change
• [ ] update the build_whole_term function
• [ ] update dcalc/optimizer
• [ ] update the proof platform

[AltGr]

Hasn't ths been done already ? The structure is not the one proposed exactly, but uses binders in the current AST