Merge pull request #292 from Nadrieril/cleanup-itemkind

Author: Nadrieril

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-ee335659fe378b51f04b6701632acbc56a205228
+177eece7e95be78567500a9aec967f1433492a54

compiler/Extract.ml

@@ -20,7 +20,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
      only use their type for the fields of the records we generate for the trait
      declarations *)
   match def.f.kind with
-  | TraitItemDecl _ -> ctx
+  | TraitDeclItem (_, _, false) -> ctx
   | _ -> (
       (* Check if the function is builtin *)
       let builtin =
@@ -1160,7 +1160,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
   *)
   let ctx, trait_decl =
     match def.kind with
-    | TraitItemProvided (decl_id, _) ->
+    | TraitDeclItem (decl_id, _, true) ->
         let trait_decl = T.TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
         let ctx, _ = ctx_add_trait_self_clause def.item_meta.span ctx in
         let ctx = { ctx with is_provided_method = true } in

compiler/ExtractBase.ml

@@ -2061,7 +2061,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
          in the trait declaration *)
       let suffix =
         match def.kind with
-        | TraitItemProvided _ -> "_default"
+        | TraitDeclItem (_, _, true) -> "_default"
         | _ -> ""
       in
       let ctx = ctx_add def.item_meta.span decl (name ^ suffix) ctx in
@@ -2080,7 +2080,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
   *)
   let item_meta =
     match def.kind with
-    | TraitItemImpl (_, trait_decl_id, item_name, _) -> (
+    | TraitImplItem (_, trait_decl_id, item_name, _) -> (
         if Option.is_some def.item_meta.attr_info.rename then def.item_meta
         else
           (* Lookup the declaration. TODO: the trait item impl info

compiler/Interpreter.ml

@@ -74,8 +74,8 @@ let symbolic_instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
     eval_ctx * inst_fun_sig =
   let tr_self =
     match kind with
-    | RegularKind | TraitItemImpl _ -> UnknownTrait __FUNCTION__
-    | TraitItemDecl _ | TraitItemProvided _ -> Self
+    | RegularItem | TraitImplItem _ -> UnknownTrait __FUNCTION__
+    | TraitDeclItem _ -> Self
   in
   let generics =
     let { regions; types; const_generics; trait_clauses; _ } = sg.generics in

compiler/LlbcAstUtils.ml

@@ -45,7 +45,7 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
     (* Something to pay attention to: we must ignore trait method *declarations*
        (which don't have a body but must not be considered as opaque) *)
     && (match d.kind with
-       | TraitItemDecl _ -> false
+       | TraitDeclItem (_, _, false) -> false
        | _ -> true)
     && ((not filter_assumed)
        || (not (NameMatcherMap.mem ctx d.item_meta.name builtin_globals_map))

compiler/Translate.ml

@@ -807,7 +807,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         match pure_fun with
         | Some pure_fun -> (
             match pure_fun.f.Pure.kind with
-            | TraitItemDecl _ -> ()
+            | TraitDeclItem (_, _, false) -> ()
             | _ ->
                 (* Translate *)
                 export_functions_group [ pure_fun ])

flake.lock

@@ -228,6 +228,9 @@
             pkgs.ocamlPackages.ocamlformat
             pkgs.ocamlPackages.menhir
             pkgs.ocamlPackages.odoc
+            # ocaml-lsp's version must match the ocaml version used. Pinning
+            # this here to save everyone a headache.
+            pkgs.ocamlPackages.ocaml-lsp
             pkgs.jq
             pkgs.rustup
           ];