down to four errors in HACL

lib/AstToMiniRust.ml

@@ -494,6 +494,10 @@ let translate_lid env lid =
   else
     allocate name
 
+let translate_binder_name (b: Ast.binder) =
+  let open Ast in
+  if snd !(b.node.mark) = AtMost 0 then "_" ^ b.node.name else b.node.name
+
 
 (* Trying to compile a *reference* to variable, who originates from a split of `v_base`, and whose
    original path in the tree is `path`. *)
@@ -948,7 +952,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let env, e = translate_expr env e in
       let branches = List.map (fun (binders, pat, e) ->
         let binders = List.map (fun (b: Ast.binder) ->
-          { MiniRust.name = b.node.name; typ = translate_type env b.typ; mut = false; ref = false }
+          { MiniRust.name = translate_binder_name b; typ = translate_type env b.typ; mut = false; ref = false }
         ) binders in
         let env = List.fold_left push env binders in
         let pat = translate_pat env pat in
@@ -1236,7 +1240,7 @@ let translate_decl env (d: Ast.decl): MiniRust.decl option =
         | _ -> failwith "impossible"
       in
       let body, args = if parameters = [] then DeBruijn.subst Helpers.eunit 0 body, [] else body, args in
-      let parameters = List.map2 (fun typ a -> { MiniRust.mut = false; name = a.Ast.node.Ast.name; typ; ref = false }) parameters args in
+      let parameters = List.map2 (fun typ a -> { MiniRust.mut = false; name = translate_binder_name a; typ; ref = false }) parameters args in
       let env = List.fold_left push env parameters in
       let _, body = translate_expr_with_type env body return_type in
       let meta = translate_meta flags in

lib/OptimizeMiniRust.ml

@@ -146,13 +146,13 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Let (b, e1, e2) ->
       (* KPrint.bprintf "[infer-mut,let] %a\n" pexpr e; *)
       let a, e2 = open_ b e2 in
-      (* KPrint.bprintf "[infer-mut,let] opened %s[%s]\n" b.name (show_atom_t a); *)
+      KPrint.bprintf "[infer-mut,let] opened %s[%s]\n" b.name (show_atom_t a);
       let known, e2 = infer env expected known e2 in
       let mut_var = want_mut_var a known in
       let mut_borrow = want_mut_borrow a known in
-      (* KPrint.bprintf "[infer-mut,let-done-e2] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name
+      KPrint.bprintf "[infer-mut,let-done-e2] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name
         (show_atom_t a)
-        ptyp b.typ mut_var mut_borrow; *)
+        ptyp b.typ mut_var mut_borrow;
       let t1 = if mut_borrow then make_mut_borrow b.typ else b.typ in
       let known, e1 = infer env t1 known e1 in
       known, Let ({ b with mut = mut_var; typ = t1 }, e1, close a (Var 0) (lift 1 e2))
@@ -365,9 +365,9 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
          in known. *)
       known, e
 
-  | Match (e, t, arms) as e_match ->
+  | Match (e_scrut, t, arms) as e_match ->
       (* We have the expected type of the scrutinee: recurse *)
-      let known, e = infer env t known e in
+      let known, e = infer env t known e_scrut in
       let known, arms = List.fold_left_map (fun known ((bs, _, _) as branch) ->
         let atoms, pat, e = open_branch branch in
         let known, e = infer env expected known e in
@@ -428,13 +428,19 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
                   | OpenP open_var ->
                       let { atom; _ } = open_var in
                       let mut = VarSet.mem atom known.r in
-                      let ref = match typ with Ref _ -> true | _ -> false in
+                      let ref = match typ with Ref _ -> true | _ -> mut (* something mutated relying on an implicit conversion to ref *) in
                       KPrint.bprintf "In match:\n%a\nPattern variable %s: mut=%b, ref=%b\n"
                         pexpr e_match open_var.name mut ref;
                       (* i., above *)
                       let known = if mut then add_mut_field (Some t) f known else known in
                       (* ii.b. *)
-                      let known = match e with Open { atom; _ } when mut -> add_mut_var atom known | _ -> known in
+                      let known = match e_scrut with
+                        | Open { atom; _ } when mut -> add_mut_var atom known
+                        | Deref (Open { atom; _ }) when mut -> add_mut_borrow atom known
+                        | _ ->
+                            KPrint.bprintf "%a is not open or deref\n" pexpr e;
+                            known
+                      in
                       (* ii.a *)
                       let known = if ref then { known with p = VarSet.add atom known.p } else known in
                       known, (f, OpenP open_var) :: fieldpats
@@ -454,7 +460,11 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
           |  _ -> Warn.failwith "TODO: Match %a" ppat pat
         in
         let known, pat = update_fields known pat t in
-        let bs = List.map2 (fun a b -> if VarSet.mem a known.p then { b with ref = true } else b) atoms bs in
+        let bs = List.map2 (fun a b ->
+          let ref = VarSet.mem a known.p in
+          let mut = VarSet.mem a known.r in
+          { b with ref; mut }
+        ) atoms bs in
         let branch = close_branch atoms (bs, pat, e) in
         known, branch
       ) known arms in

lib/PrintMiniRust.ml

@@ -225,6 +225,16 @@ let print_op = function
   | Constant.BNot -> string "!"
   | op -> print_op op
 
+let rec is_ignored_pattern env = function
+  | Wildcard -> true
+  | VarP v ->
+      begin match lookup env v with
+      | Bound b -> b.name.[0] = '_'
+      | _ -> failwith "incorrect bound var in pattern"
+      end
+  | StructP (_, fields) -> List.for_all (fun (_, p) -> is_ignored_pattern env p) fields
+  | _ -> false
+
 (* print a block *and* the expression within it *)
 let rec print_block_expression env e =
   braces_with_nesting (print_statements env e)
@@ -479,10 +489,13 @@ and print_pat env (p: pat) =
   | Literal c -> print_constant c
   | Wildcard -> underscore
   | StructP (name, fields) ->
+      (* Not printing those ignored patterns makes a semantic difference! It prevents move-outs... *)
+      let ignored, fields = List.partition (fun (_, p) -> is_ignored_pattern env p) fields in
+      let trailing = if ignored <> [] then comma ^/^ dot ^^ dot else empty in
       print_name env name ^^ braces_with_nesting (
         separate_map (comma ^^ break1) (fun (name, pat) ->
           group (group (string name ^^ colon) ^/^ group (print_pat env pat))
-        ) fields
+        ) fields ^^ trailing
       )
   | VarP v ->
       begin match lookup env v with