Make minor modifications

2 files changed, 38 insertions, 79 deletions

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index c3716001..34f3ef72 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -886,13 +886,13 @@ type inputs_info = {
 }
 [@@deriving show]
 
-type 'a back_info =
-  | SingleBack of 'a option
+type ('a, 'b) back_info =
+  | SingleBack of 'a
       (** Information about a single backward function, if pertinent.
 
           We use this variant if we split the forward and the backward functions.
        *)
-  | AllBacks of 'a RegionGroupId.Map.t
+  | AllBacks of 'b RegionGroupId.Map.t
       (** Information about the various backward functions.
 
           We use this if we *do not* split the forward and the backward functions.
@@ -900,7 +900,8 @@ type 'a back_info =
        *)
 [@@deriving show]
 
-type back_inputs_info = inputs_info back_info [@@deriving show]
+type back_inputs_info = (inputs_info option, inputs_info) back_info
+[@@deriving show]
 
 (** Meta information about a function signature *)
 type fun_sig_info = {
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 86c80f87..eba44e3e 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -308,20 +308,6 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
   let indent_incr = "  " in
   Print.Values.abs_to_string env verbose indent indent_incr abs
 
-let get_instantiated_fun_sig (fun_id : A.fun_id)
-    (back_id : T.RegionGroupId.id option) (generics : generic_args)
-    (ctx : bs_ctx) : inst_fun_sig =
-  (* Lookup the non-instantiated function signature *)
-  let sg =
-    (RegularFunIdNotLoopMap.find (fun_id, back_id) ctx.fun_context.fun_sigs).sg
-  in
-  (* Create the substitution *)
-  (* There shouldn't be any reference to Self *)
-  let tr_self = UnknownTrait __FUNCTION__ in
-  let subst = make_subst_from_generics sg.generics generics tr_self in
-  (* Apply *)
-  fun_sig_substitute subst sg
-
 let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
     T.type_decl =
   TypeDeclId.Map.find id ctx.type_context.llbc_type_decls
@@ -330,12 +316,6 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
     A.fun_decl =
   A.FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls
 
-(* TODO: move *)
-let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id)
-    (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
-  let id = (E.FRegular def_id, back_id) in
-  (RegularFunIdNotLoopMap.find id ctx.fun_context.fun_sigs).sg
-
 (* Some generic translation functions (we need to translate different "flavours"
    of types: forward types, backward types, etc.) *)
 let rec translate_generic_args (translate_ty : T.ty -> ty)
@@ -994,35 +974,44 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
     List.concat [ fuel; fwd_inputs; fwd_state_ty; back_inputs; back_state_ty ]
   in
   (* Outputs *)
+  let compute_back_outputs_for_gid (gid : RegionGroupId.id) :
+      string option list * ty list =
+    (* The outputs are the borrows inside the regions of the abstractions
+       and which are present in the input values. For instance, see:
+       {[
+         fn f<'a>(x : &'a mut u32) -> ...;
+       ]}
+       Upon ending the abstraction for 'a, we give back the borrow which
+       was consumed through the [x] parameter.
+    *)
+    let outputs =
+      List.map
+        (fun (name, input_ty) -> (name, translate_back_ty_for_gid gid input_ty))
+        (List.combine input_names sg.inputs)
+    in
+    (* Filter *)
+    let outputs =
+      List.filter (fun (_, opt_ty) -> Option.is_some opt_ty) outputs
+    in
+    let outputs =
+      List.map (fun (name, opt_ty) -> (name, Option.get opt_ty)) outputs
+    in
+    List.split outputs
+  in
   let output_names, doutputs =
     match gid with
     | None ->
-        (* This is a forward function: there is one (unnamed) output *)
+        (* This is a forward function: there is one (unnamed) output.
+
+           If we merge the fwd/back functions we might need to compute
+           the information about the back outputs.
+        *)
+        (* TODO: *)
+        assert (not !Config.return_back_funs);
         ([ None ], [ translate_fwd_ty type_infos sg.output ])
     | Some gid ->
-        (* This is a backward function: there might be several outputs.
-           The outputs are the borrows inside the regions of the abstractions
-           and which are present in the input values. For instance, see:
-           {[
-             fn f<'a>(x : &'a mut u32) -> ...;
-           ]}
-           Upon ending the abstraction for 'a, we give back the borrow which
-           was consumed through the [x] parameter.
-        *)
-        let outputs =
-          List.map
-            (fun (name, input_ty) ->
-              (name, translate_back_ty_for_gid gid input_ty))
-            (List.combine input_names sg.inputs)
-        in
-        (* Filter *)
-        let outputs =
-          List.filter (fun (_, opt_ty) -> Option.is_some opt_ty) outputs
-        in
-        let outputs =
-          List.map (fun (name, opt_ty) -> (name, Option.get opt_ty)) outputs
-        in
-        List.split outputs
+        (* This is a backward function: there might be several outputs. *)
+        compute_back_outputs_for_gid gid
   in
   (* Create the return type *)
   let output =
@@ -2016,37 +2005,6 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     | None -> output
     | Some nstate -> mk_simpl_tuple_pattern [ nstate; output ]
   in
-  (* Sanity check: there is the proper number of inputs and outputs, and they have the proper type *)
-  (if (* TODO: normalize the types *) !Config.type_check_pure_code then
-     match fun_id with
-     | FunId fun_id ->
-         let inst_sg =
-           get_instantiated_fun_sig fun_id (Some rg_id) generics ctx
-         in
-         log#ldebug
-           (lazy
-             ("\n- fun_id: " ^ A.show_fun_id fun_id ^ "\n- inputs ("
-             ^ string_of_int (List.length inputs)
-             ^ "): "
-             ^ String.concat ", " (List.map (texpression_to_string ctx) inputs)
-             ^ "\n- inst_sg.inputs ("
-             ^ string_of_int (List.length inst_sg.inputs)
-             ^ "): "
-             ^ String.concat ", "
-                 (List.map (pure_ty_to_string ctx) inst_sg.inputs)));
-         List.iter
-           (fun (x, ty) -> assert ((x : texpression).ty = ty))
-           (List.combine inputs inst_sg.inputs);
-         log#ldebug
-           (lazy
-             ("\n- outputs: "
-             ^ string_of_int (List.length outputs)
-             ^ "\n- expected outputs: "
-             ^ string_of_int (List.length inst_sg.doutputs)));
-         List.iter
-           (fun (x, ty) -> assert ((x : typed_pattern).ty = ty))
-           (List.combine outputs inst_sg.doutputs)
-     | _ -> (* TODO: trait methods *) ());
   (* Retrieve the function id, and register the function call in the context
    * if necessary *)
   let ctx, func =