Make minor modifications

6 files changed, 41 insertions, 52 deletions

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 9d22a643..df77959e 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -333,9 +333,21 @@ type eval_ctx = {
 }
 [@@deriving show]
 
+let lookup_type_var_opt (ctx : eval_ctx) (vid : TypeVarId.id) : type_var option
+    =
+  if TypeVarId.to_int vid < List.length ctx.type_vars then
+    Some (TypeVarId.nth ctx.type_vars vid)
+  else None
+
 let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
   TypeVarId.nth ctx.type_vars vid
 
+let lookup_const_generic_var_opt (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
+    const_generic_var option =
+  if ConstGenericVarId.to_int vid < List.length ctx.const_generic_vars then
+    Some (ConstGenericVarId.nth ctx.const_generic_vars vid)
+  else None
+
 let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
     const_generic_var =
   ConstGenericVarId.nth ctx.const_generic_vars vid
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 1ea16e58..97fb80f4 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1198,7 +1198,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
         log#ldebug
           (lazy
             ("trait method call:\n- call: " ^ call_to_string ctx call
-           ^ "\n- method name: " ^ method_name ^ "\n- generics:\n"
+           ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n"
             ^ egeneric_args_to_string ctx call.generics
             ^ "\n- trait and method generics:\n"
             ^ egeneric_args_to_string ctx
@@ -1273,7 +1273,10 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
                   (lazy
                     ("provided method call:" ^ "\n- method name: " ^ method_name
                    ^ "\n- generics:\n"
-                    ^ egeneric_args_to_string ctx generics));
+                    ^ egeneric_args_to_string ctx generics
+                    ^ "\n- parent params info: "
+                    ^ Print.option_to_string A.show_params_info
+                        method_def.signature.parent_params_info));
                 let tr_self =
                   T.TraitRef (etrait_ref_no_regions_to_gr_trait_ref trait_ref)
                 in
@@ -1303,6 +1306,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
                 (List.append trait_decl.required_methods provided)
             in
             let method_def = C.ctx_lookup_fun_decl ctx method_id in
+            log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def));
             (* Instantiate *)
             let tr_self = T.TraitRef trait_ref in
             let tr_self =
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 8a7e8c52..8525be29 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -39,8 +39,12 @@ let typed_avalue_to_string = PA.typed_avalue_to_string
 let place_to_string = PA.place_to_string
 let operand_to_string = PA.operand_to_string
 let egeneric_args_to_string = PA.egeneric_args_to_string
+let fun_decl_to_string = PA.fun_decl_to_string
 let call_to_string = PA.call_to_string
-let trait_impl_to_string = PA.trait_impl_to_string
+
+let trait_impl_to_string ctx =
+  PA.trait_impl_to_string { ctx with type_vars = []; const_generic_vars = [] }
+
 let statement_to_string ctx = PA.statement_to_string ctx "" "  "
 let statement_to_string_with_tab ctx = PA.statement_to_string ctx "  " "  "
 let env_elem_to_string ctx = PA.env_elem_to_string ctx "" "  "
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 55aa0c53..92743bc1 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -479,19 +479,23 @@ module Contexts = struct
     PV.value_to_rtype_formatter fmt
 
   let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter =
-    (* We shouldn't use rvar_to_string *)
-    let rvar_to_string _r =
-      raise (Failure "Unexpected use of rvar_to_string")
+    let rvar_to_string r =
+      (* In theory we shouldn't use rvar_to_string, but it can happen
+         when printing definitions for instance... *)
+      T.RegionVarId.to_string r
     in
     let r_to_string r = PT.region_id_to_string r in
 
     let type_var_id_to_string vid =
-      let v = C.lookup_type_var ctx vid in
-      v.name
+      (* The context may be invalid *)
+      match C.lookup_type_var_opt ctx vid with
+      | None -> T.TypeVarId.to_string vid
+      | Some v -> v.name
     in
     let const_generic_var_id_to_string vid =
-      let v = C.lookup_const_generic_var ctx vid in
-      v.name
+      match C.lookup_const_generic_var_opt ctx vid with
+      | None -> T.ConstGenericVarId.to_string vid
+      | Some v -> v.name
     in
     let type_decl_id_to_string def_id =
       let def = C.ctx_lookup_type_decl ctx def_id in
@@ -702,6 +706,10 @@ module EvalCtxLlbcAst = struct
     let fmt = PC.eval_ctx_to_ast_formatter ctx in
     PA.call_to_string fmt "" call
 
+  let fun_decl_to_string (ctx : C.eval_ctx) (f : A.fun_decl) : string =
+    let fmt = PC.eval_ctx_to_ast_formatter ctx in
+    PA.fun_decl_to_string fmt "" "  " f
+
   let statement_to_string (ctx : C.eval_ctx) (indent : string)
       (indent_incr : string) (e : A.statement) : string =
     let fmt = PC.eval_ctx_to_ast_formatter ctx in
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 1da0521d..4c5b99c3 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -346,43 +346,6 @@ let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id)
   let id = (A.Regular def_id, back_id) in
   (RegularFunIdNotLoopMap.find id ctx.fun_context.fun_sigs).sg
 
-let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
-    (args : texpression list) (ctx : bs_ctx) : bs_ctx =
-  let calls = ctx.calls in
-  assert (not (V.FunCallId.Map.mem call_id calls));
-  let info =
-    { forward; forward_inputs = args; backwards = T.RegionGroupId.Map.empty }
-  in
-  let calls = V.FunCallId.Map.add call_id info calls in
-  { ctx with calls }
-
-(** [back_args]: the *additional* list of inputs received by the backward function *)
-let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
-    (back_id : T.RegionGroupId.id) (back_args : texpression list) (ctx : bs_ctx)
-    : bs_ctx * fun_or_op_id =
-  (* Insert the abstraction in the call informations *)
-  let info = V.FunCallId.Map.find call_id ctx.calls in
-  assert (not (T.RegionGroupId.Map.mem back_id info.backwards));
-  let backwards =
-    T.RegionGroupId.Map.add back_id (abs, back_args) info.backwards
-  in
-  let info = { info with backwards } in
-  let calls = V.FunCallId.Map.add call_id info ctx.calls in
-  (* Insert the abstraction in the abstractions map *)
-  let abstractions = ctx.abstractions in
-  assert (not (V.AbstractionId.Map.mem abs.abs_id abstractions));
-  let abstractions =
-    V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions
-  in
-  (* Retrieve the fun_id *)
-  let fun_id =
-    match info.forward.call_id with
-    | S.Fun (fid, _) -> Fun (FromLlbc (fid, None, Some back_id))
-    | S.Unop _ | S.Binop _ -> raise (Failure "Unreachable")
-  in
-  (* Update the context and return *)
-  ({ ctx with calls; abstractions }, fun_id)
-
 (* Some generic translation functions (we need to translate different "flavours"
    of types: sty, forward types, backward types, etc.) *)
 let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index ab95b854..6bc821d3 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -303,19 +303,17 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
    | some _ => nhm.len_s = hm.len_s) := by
   rw [insert_no_resize]
   simp only [hash_key, bind_tc_ret] -- TODO: annoying
-  have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint
+  have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by
    intro
    simp_all [inv]
-  progress keep _ as ⟨ hash_mod, hhm ⟩
-  have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac
+  progress as ⟨ hash_mod, hhm ⟩
+  have _ : 0 ≤ hash_mod.val := by scalar_tac
   have _ : hash_mod.val < Vec.length hm.slots := by
     have : 0 < hm.slots.val.len := by
       simp [inv] at hinv
       simp [hinv]
     -- TODO: we want to automate that
     simp [*, Int.emod_lt_of_pos]
-  -- TODO: change the spec of Vec.index_mut to introduce a let-binding.
-  -- or: make progress introduce the let-binding by itself (this is clearer)
   progress as ⟨ l, h_leq ⟩
   -- TODO: make progress use the names written in the goal
   progress as ⟨ inserted ⟩