diff options
Diffstat (limited to '')
-rw-r--r-- | compiler/Extract.ml | 45 |
1 files changed, 22 insertions, 23 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index afd722e5..6b6a2686 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -234,26 +234,20 @@ let assumed_adts () : (assumed_ty * string) list = (Array, "Array"); (Slice, "Slice"); (Str, "Str"); + (RawPtr Mut, "MutRawPtr"); + (RawPtr Const, "ConstRawPtr"); ] - | Coq | FStar -> + | Coq | FStar | HOL4 -> [ (State, "state"); (Result, "result"); (Error, "error"); - (Fuel, "nat"); - (Array, "array"); - (Slice, "slice"); - (Str, "str"); - ] - | HOL4 -> - [ - (State, "state"); - (Result, "result"); - (Error, "error"); - (Fuel, "num"); + (Fuel, if !backend = HOL4 then "num" else "nat"); (Array, "array"); (Slice, "slice"); (Str, "str"); + (RawPtr Mut, "mut_raw_ptr"); + (RawPtr Const, "const_raw_ptr"); ] let assumed_struct_constructors () : (assumed_ty * string) list = @@ -1378,7 +1372,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : let def_name = match info with | None -> ctx.fmt.type_name def.name - | Some info -> String.concat "." info.rust_name + | Some info -> info.extract_name in let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in (* Compute and register: @@ -4281,16 +4275,9 @@ let extract_trait_decl_method_names (ctx : extraction_ctx) string * (RegionGroupId.id option * string) list = let compute_fun_name (f : fun_decl) : RegionGroupId.id option * string = - (* We do something special: we use the base name but remove everything - but the crate (because [get_name] removes it) and the last ident. - This allows us to reuse the [ctx_compute_fun_decl] function. - *) - let basename : name = - match (f.basename : name) with - | Ident crate :: name -> - Ident crate :: [ Collections.List.last name ] - | _ -> raise (Failure "Unexpected") - in + (* We do something special to reuse the [ctx_compute_fun_decl] + function. TODO: make it cleaner. *) + let basename : name = [ Ident item_name ] in let f = { f with basename } in let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in let name = ctx_compute_fun_name trans f ctx in @@ -4503,6 +4490,17 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) extract_generic_params ctx fmt TypeDeclId.Set.empty generics type_params cg_params trait_clauses; + (* Add the parent clauses as local clauses, so that we can refer to them *) + let ctx = + List.fold_left + (fun ctx clause -> + let item_name = + ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx + in + ctx_add (LocalTraitClauseId clause.clause_id) item_name ctx) + ctx decl.generics.trait_clauses + in + F.pp_print_space fmt (); (match !backend with | Lean -> F.pp_print_string fmt "where" @@ -4522,6 +4520,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx in let ty () = + F.pp_print_space fmt (); extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause in extract_trait_decl_item ctx fmt item_name ty) |