From a27efd1ed08bc9583752445d9eda7a693c0c7379 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 16 Nov 2023 10:13:28 +0100 Subject: [PATCH] Finish propagating the changes to the names and cleaning --- compiler/Contexts.ml | 2 +- compiler/Driver.ml | 21 ++--- compiler/Extract.ml | 40 ++++----- compiler/ExtractTypes.ml | 155 ++++++++++++++++++++++++----------- compiler/FunsAnalysis.ml | 4 +- compiler/Print.ml | 1 - compiler/Pure.ml | 1 + compiler/PureMicroPasses.ml | 29 ++++--- compiler/SymbolicToPure.ml | 6 +- compiler/Translate.ml | 159 ++++++++++++++++++------------------ compiler/TranslateCore.ml | 3 + compiler/TypesAnalysis.ml | 2 +- 12 files changed, 244 insertions(+), 179 deletions(-) diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index 41c841412..a2ae4f16d 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -525,7 +525,7 @@ let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id) let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool = let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in - match decl_group with Rec _ -> true | NonRec _ -> false + match decl_group with RecGroup _ -> true | NonRecGroup _ -> false (** Visitor to iterate over the values in the *current* frame *) class ['self] iter_frame = diff --git a/compiler/Driver.ml b/compiler/Driver.ml index aa2934690..94e50a083 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -1,15 +1,10 @@ open Aeneas.LlbcOfJson open Aeneas.Logging -module T = Aeneas.Types -module A = Aeneas.LlbcAst -module I = Aeneas.Interpreter +open Aeneas.LlbcAst +open Aeneas.Interpreter module EL = Easy_logging.Logging -module TA = Aeneas.TypesAnalysis -module Micro = Aeneas.PureMicroPasses -module Print = Aeneas.Print -module PrePasses = Aeneas.PrePasses -module Translate = Aeneas.Translate open Aeneas.Config +open Aeneas (** The local logger *) let log = main_log @@ -227,7 +222,9 @@ let () = if !backend = Lean && !extract_decreases_clauses && List.exists - (function Aeneas.LlbcAst.Fun (Rec (_ :: _)) -> true | _ -> false) + (function + | Aeneas.LlbcAst.FunGroup (RecGroup (_ :: _)) -> true + | _ -> false) m.declarations then ( log#error @@ -237,15 +234,15 @@ let () = fail ()); (* Apply the pre-passes *) - let m = PrePasses.apply_passes m in + let m = Aeneas.PrePasses.apply_passes m in (* Some options for the execution *) (* Test the unit functions with the concrete interpreter *) - if !test_unit_functions then I.Test.test_unit_functions m; + if !test_unit_functions then Test.test_unit_functions m; (* Translate the functions *) - Translate.translate_crate filename dest_dir m; + Aeneas.Translate.translate_crate filename dest_dir m; (* Print total elapsed time *) log#linfo diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 04f6c2c3b..cd62c15c3 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -27,7 +27,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) let builtin = let open ExtractBuiltin in let funs_map = builtin_funs_map () in - let sname = name_to_simple_name def.fwd.f.basename in + let sname = name_to_simple_name def.fwd.f.llbc_name in SimpleNameMap.find_opt sname funs_map in (* Use the builtin names if necessary *) @@ -65,7 +65,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) raise (Failure ("Not found: " - ^ Names.name_to_string f.basename + ^ name_to_string ctx f.llbc_name ^ ", " ^ Print.option_to_string Pure.show_loop_id f.loop_id ^ Print.option_to_string Pure.show_region_group_id @@ -212,7 +212,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list) let decl = FunDeclId.Map.find id ctx.trans_funs in let err = "Ill-formed builtin information for function " - ^ Names.name_to_string decl.fwd.f.basename + ^ name_to_string ctx decl.fwd.f.llbc_name ^ ": " ^ string_of_int (List.length filter) ^ " filtering arguments provided for " @@ -1137,7 +1137,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) extract_comment fmt - [ "[" ^ Print.fun_name_to_string def.basename ^ "]: decreases clause" ]; + [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]; F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on * one line *) @@ -1199,7 +1199,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) extract_comment fmt - [ "[" ^ Print.fun_name_to_string def.basename ^ "]: termination measure" ]; + [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]; F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on * one line *) @@ -1253,7 +1253,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) (* syntax term ... term : tactic *) F.pp_print_break fmt 0 0; extract_comment fmt - [ "[" ^ Print.fun_name_to_string def.basename ^ "]: decreases_by tactic" ]; + [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]; F.pp_print_space fmt (); F.pp_open_hvbox fmt 0; F.pp_print_string fmt "syntax \""; @@ -1289,7 +1289,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) (Pure.FunId (FRegular def.def_id), def.loop_id, def.back_id) ctx.fun_name_info in - let comment_pre = "[" ^ Print.fun_name_to_string def.basename ^ "]: " in + let comment_pre = "[" ^ name_to_string ctx def.llbc_name ^ "]: " in let comment = let loop_comment = match def.loop_id with @@ -1766,13 +1766,13 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; - extract_comment fmt [ "[" ^ Print.global_name_to_string global.name ^ "]" ]; + extract_comment fmt [ "[" ^ name_to_string ctx global.name ^ "]" ]; F.pp_print_space fmt (); let decl_name = ctx_get_global global.def_id ctx in let body_name = ctx_get_function - (FromLlbc (Pure.FunId (FRegular global.body_id), None, None)) + (FromLlbc (Pure.FunId (FRegular global.body), None, None)) ctx in @@ -1958,8 +1958,10 @@ let extract_trait_decl_method_names (ctx : extraction_ctx) = (* 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 llbc_name : Types.name = + [ Types.PeIdent (item_name, Disambiguator.zero) ] + in + let f = { f with llbc_name } in let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in let name = ctx_compute_fun_name trans f ctx in (* Add a prefix if necessary *) @@ -1991,7 +1993,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx) | None -> let err = "Ill-formed builtin information for trait decl \"" - ^ Names.name_to_string trait_decl.name + ^ name_to_string ctx trait_decl.llbc_name ^ "\", method \"" ^ item_name ^ "\": could not find name for region " ^ Print.option_to_string Pure.show_region_group_id @@ -2022,7 +2024,7 @@ let extract_trait_decl_register_names (ctx : extraction_ctx) (trait_decl : trait_decl) : extraction_ctx = (* Lookup the information if this is a builtin trait *) let open ExtractBuiltin in - let sname = name_to_simple_name trait_decl.name in + let sname = name_to_simple_name trait_decl.llbc_name in let builtin_info = SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) in @@ -2059,8 +2061,8 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) (* Check if the trait implementation is builtin *) let builtin_info = let open ExtractBuiltin in - let type_sname = name_to_simple_name trait_impl.name in - let trait_sname = name_to_simple_name trait_decl.name in + let type_sname = name_to_simple_name trait_impl.llbc_name in + let trait_sname = name_to_simple_name trait_decl.llbc_name in SimpleNamePairMap.find_opt (type_sname, trait_sname) (builtin_trait_impls_map ()) in @@ -2185,7 +2187,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) extract_comment fmt - [ "Trait declaration: [" ^ Print.name_to_string decl.name ^ "]" ]; + [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]; F.pp_print_break fmt 0 0; (* Open two outer boxes for the definition, so that whenever possible it gets printed on one line and indents are correct. @@ -2466,14 +2468,14 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) (** Extract a trait implementation *) let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (impl : trait_impl) : unit = - log#ldebug (lazy ("extract_trait_impl: " ^ Names.name_to_string impl.name)); + log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name)); (* Retrieve the impl name *) let impl_name = ctx_get_trait_impl impl.def_id ctx in (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) extract_comment fmt - [ "Trait implementation: [" ^ Print.name_to_string impl.name ^ "]" ]; + [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]; F.pp_print_break fmt 0 0; (* Open two outer boxes for the definition, so that whenever possible it gets printed on @@ -2640,7 +2642,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_break fmt 0 0; (* Print a comment *) extract_comment fmt - [ "Unit test for [" ^ Print.fun_name_to_string def.basename ^ "]" ]; + [ "Unit test for [" ^ name_to_string ctx def.llbc_name ^ "]" ]; F.pp_print_space fmt (); (* Open a box for the test *) F.pp_open_hovbox fmt ctx.indent_incr; diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 553d5863f..e4617d2c6 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -309,7 +309,6 @@ let assumed_llbc_functions () : (SliceIndexShared, None, "slice_index_usize"); (SliceIndexMut, None, "slice_index_usize"); (SliceIndexMut, rg0, "slice_update_usize"); - (SliceLen, None, "slice_len"); ] | Lean -> [ @@ -323,7 +322,6 @@ let assumed_llbc_functions () : (SliceIndexShared, None, "Slice.index_usize"); (SliceIndexMut, None, "Slice.index_usize"); (SliceIndexMut, rg0, "Slice.update_usize"); - (SliceLen, None, "Slice.len"); ] let assumed_pure_functions () : (pure_assumed_fun_id * string) list = @@ -538,6 +536,11 @@ let type_keyword () = | Coq | Lean -> "Type" | HOL4 -> raise (Failure "Unexpected") +let name_last_elem_as_ident (n : llbc_name) : string = + match Collections.List.last n with + | PeIdent (s, _) -> s + | PeImpl _ -> raise (Failure "Unexpected") + (** [ctx]: we use the context to lookup type definitions, to retrieve type names. This is used to compute variable names, when they have no basenames: in this @@ -579,34 +582,90 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) let int_name = int_name in (* Prepare a name. - * The first id elem is always the crate: if it is the local crate, - * we remove it. - * We also remove all the disambiguators, then convert everything to strings. - * **Rmk:** because we remove the disambiguators, there may be name collisions - * (which is ok, because we check for name collisions and fail if there is any). - *) - let get_name (name : name) : string list = + The first id elem is always the crate: if it is the local crate, + we remove it. We ignore disambiguators (there may be collisions, but we + check if there are). + *) + let rec name_to_simple_name (name : llbc_name) : string list = (* Rmk.: initially we only filtered the disambiguators equal to 0 *) - let name = Names.filter_disambiguators name in match name with - | Ident crate :: name -> - let name = if crate = crate_name then name else Ident crate :: name in + | (PeIdent (crate, _) as id) :: name -> + let name = if crate = crate_name then name else id :: name in + let open Types in let name = List.map (function - | Names.Ident s -> s - | Disambiguator d -> Names.Disambiguator.to_string d) + | PeIdent (s, _) -> s + | PeImpl impl -> impl_elem_to_simple_name impl) name in name | _ -> - raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name)) + raise + (Failure + ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name)) + and impl_elem_to_simple_name (impl : Types.impl_elem) : string = + (* We do something simple for now. + TODO: we might want to do something different for impl elements which are + actually trait implementations, in order to prevent name collisions (it + is possible to define several times the same trait for the same type, + but with different instantiations of the type, or different trait + requirements *) + ty_to_simple_name impl.generics impl.ty + and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) : + string = + (* We do something simple for now. + TODO: find a more principled way of converting types to names. + In particular, we might want to do something different for impl elements which are + actually trait implementations, in order to prevent name collisions (it + is possible to define several times the same trait for the same type, + but with different instantiations of the type, or different trait + requirements *) + match ty with + | TAdt (id, args) -> ( + match id with + | TAdtId id -> + let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in + name_last_elem_as_ident def.name + | TTuple -> + (* TODO *) + "Tuple" + ^ String.concat "" + (List.map (ty_to_simple_name generics) args.types) + | TAssumed id -> Types.show_assumed_ty id) + | TVar vid -> + (* Use the variable name *) + (List.find (fun (v : type_var) -> v.index = vid) generics.types).name + | TLiteral lty -> + StringUtils.capitalize_first_letter + (Print.Types.literal_type_to_string lty) + | TNever -> raise (Failure "Unreachable") + | TRef (_, rty, rk) -> ( + let rty = ty_to_simple_name generics rty in + match rk with + | RMut -> "MutBorrow" ^ rty + | RShared -> "SharedBorrow" ^ rty) + | TRawPtr (rty, rk) -> ( + let rty = ty_to_simple_name generics rty in + match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty) + | TTraitType (tr, _, name) -> + (* TODO: this is way too simple *) + let trait_decl = + TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id + ctx.trait_decls_ctx.trait_decls + in + name_last_elem_as_ident trait_decl.name ^ name + | TArrow (inputs, output) -> + "Arrow" + ^ String.concat "" + (List.map (ty_to_simple_name generics) (inputs @ [ output ])) in let flatten_name (name : string list) : string = match !backend with | FStar | Coq | HOL4 -> String.concat "_" name | Lean -> String.concat "." name in + let get_name name : string list = name_to_simple_name name in let get_type_name = get_name in let get_type_name_no_suffix name = match !backend with @@ -620,7 +679,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | Coq | HOL4 -> get_type_name_no_suffix name ^ "_t" | Lean -> get_type_name_no_suffix name in - let field_name (def_name : name) (field_id : FieldId.id) + let field_name (def_name : llbc_name) (field_id : FieldId.id) (field_name : string option) : string = let field_name_s = match field_name with @@ -639,7 +698,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | Lean | HOL4 -> def_name | Coq | FStar -> StringUtils.lowercase_first_letter def_name in - let variant_name (def_name : name) (variant : string) : string = + let variant_name (def_name : llbc_name) (variant : string) : string = match !backend with | FStar | Coq | HOL4 -> let variant = to_camel_case variant in @@ -649,7 +708,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) else variant | Lean -> variant in - let struct_constructor (basename : name) : string = + let struct_constructor (basename : llbc_name) : string = let tname = type_name basename in ExtractBuiltin.mk_struct_constructor tname in @@ -661,15 +720,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname | Lean -> fname in - let global_name (name : global_name) : string = + let global_name (name : llbc_name) : string = (* Converting to snake case also lowercases the letters (in Rust, global * names are written in capital letters). *) let parts = List.map to_snake_case (get_name name) in String.concat "_" parts in - let fun_name (fname : fun_name) (num_loops : int) (loop_id : LoopId.id option) - (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int) - : string = + let fun_name (fname : llbc_name) (num_loops : int) + (loop_id : LoopId.id option) (num_rgs : int) + (rg : region_group_info option) (filter_info : bool * int) : string = let fname = get_fun_name fname in (* Compute the suffix *) let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in @@ -678,7 +737,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) in let trait_decl_name (trait_decl : trait_decl) : string = - type_name trait_decl.name + type_name trait_decl.llbc_name in let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) : @@ -686,12 +745,14 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) (* TODO: provisional: we concatenate the trait impl name (which is its type) with the trait decl name *) let trait_decl = - let name = trait_decl.name in + let name = trait_decl.llbc_name in let name = get_type_name_no_suffix name ^ "Inst" in (* Remove the occurrences of '.' *) String.concat "" (String.split_on_char '.' name) in - let name = flatten_name (get_type_name trait_impl.name @ [ trait_decl ]) in + let name = + flatten_name (get_type_name trait_impl.llbc_name @ [ trait_decl ]) + in match !backend with | FStar -> StringUtils.lowercase_first_letter name | Coq | HOL4 | Lean -> name @@ -745,7 +806,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) ^ TraitClauseId.to_string clause.clause_id in - let termination_measure_name (_fid : A.FunDeclId.id) (fname : fun_name) + let termination_measure_name (_fid : A.FunDeclId.id) (fname : llbc_name) (num_loops : int) (loop_id : LoopId.id option) : string = let fname = get_fun_name fname in let lp_suffix = default_fun_loop_suffix num_loops loop_id in @@ -760,7 +821,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) fname ^ lp_suffix ^ suffix in - let decreases_proof_name (_fid : A.FunDeclId.id) (fname : fun_name) + let decreases_proof_name (_fid : A.FunDeclId.id) (fname : llbc_name) (num_loops : int) (loop_id : LoopId.id option) : string = let fname = get_fun_name fname in let lp_suffix = default_fun_loop_suffix num_loops loop_id in @@ -815,12 +876,12 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | TAdtId adt_id -> let def = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in (* Derive the var name from the last ident of the type name - * Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm" - *) + Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm" + *) (* The name shouldn't be empty, and its last element should * be an ident *) - let cl = List.nth def.name (List.length def.name - 1) in - name_from_type_ident (Names.as_ident cl)) + let cl = Collections.List.last def.name in + name_from_type_ident (TypesUtils.as_ident cl)) | TVar _ -> ( (* TODO: use "t" also for F* *) match !backend with @@ -866,31 +927,31 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) match cv with | VScalar sv -> ( match !backend with - | FStar -> F.pp_print_string fmt (Z.to_string sv.PV.value) + | FStar -> F.pp_print_string fmt (Z.to_string sv.value) | Coq | HOL4 | Lean -> let print_brackets = inside && !backend = HOL4 in if print_brackets then F.pp_print_string fmt "("; (match !backend with | Coq | Lean -> () | HOL4 -> - F.pp_print_string fmt ("int_to_" ^ int_name sv.PV.int_ty); + F.pp_print_string fmt ("int_to_" ^ int_name sv.int_ty); F.pp_print_space fmt () | _ -> raise (Failure "Unreachable")); (* We need to add parentheses if the value is negative *) - if sv.PV.value >= Z.of_int 0 then - F.pp_print_string fmt (Z.to_string sv.PV.value) + if sv.value >= Z.of_int 0 then + F.pp_print_string fmt (Z.to_string sv.value) else if !backend = Lean then (* TODO: parsing issues with Lean because there are ambiguous interpretations between int values and nat values *) F.pp_print_string fmt - ("(-(" ^ Z.to_string (Z.neg sv.PV.value) ^ ":Int))") - else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")"); + ("(-(" ^ Z.to_string (Z.neg sv.value) ^ ":Int))") + else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")"); (match !backend with | Coq -> - let iname = int_name sv.PV.int_ty in + let iname = int_name sv.int_ty in F.pp_print_string fmt ("%" ^ iname) | Lean -> - let iname = String.lowercase_ascii (int_name sv.PV.int_ty) in + let iname = String.lowercase_ascii (int_name sv.int_ty) in F.pp_print_string fmt ("#" ^ iname) | HOL4 -> () | _ -> raise (Failure "Unreachable")); @@ -1426,7 +1487,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : extraction_ctx = (* Lookup the builtin information, if there is *) let open ExtractBuiltin in - let sname = name_to_simple_name def.name in + let sname = name_to_simple_name def.llbc_name in let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in (* Register the filtering information, if there is *) let ctx = @@ -1442,7 +1503,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : (* Compute and register the type def name *) let def_name = match info with - | None -> ctx.fmt.type_name def.name + | None -> ctx.fmt.type_name def.llbc_name | Some info -> info.extract_name in let ctx = ctx_add (TypeId (TAdtId def.def_id)) def_name ctx in @@ -1460,10 +1521,10 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : let field_names = FieldId.mapi (fun fid (field : field) -> - (fid, ctx.fmt.field_name def.name fid field.field_name)) + (fid, ctx.fmt.field_name def.llbc_name fid field.field_name)) fields in - let cons_name = ctx.fmt.struct_constructor def.name in + let cons_name = ctx.fmt.struct_constructor def.llbc_name in (field_names, cons_name) | Some { body_info = Some (Struct (cons_name, field_names)); _ } -> let field_names = @@ -1499,12 +1560,12 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : VariantId.mapi (fun variant_id (variant : variant) -> let name = - ctx.fmt.variant_name def.name variant.variant_name + ctx.fmt.variant_name def.llbc_name variant.variant_name in (* Add the type name prefix for Lean *) let name = if !Config.backend = Lean then - let type_name = ctx.fmt.type_name def.name in + let type_name = ctx.fmt.type_name def.llbc_name in type_name ^ "." ^ name else name in @@ -1648,7 +1709,7 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter) let print_variant _variant_id (v : variant) = (* We don't lookup the name, because it may have a prefix for the type id (in the case of Lean) *) - let cons_name = ctx.fmt.variant_name def.name v.variant_name in + let cons_name = ctx.fmt.variant_name def.llbc_name v.variant_name in let fields = v.fields in extract_type_decl_variant ctx fmt type_decl_group def_name type_params cg_params cons_name fields @@ -2030,7 +2091,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) if !backend <> HOL4 || not (decl_is_first_from_group kind) then F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment fmt [ "[" ^ Print.name_to_string def.name ^ "]" ]; + extract_comment fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]; F.pp_print_break fmt 0 0; (* Open a box for the definition, so that whenever possible it gets printed on * one line. Note however that in the case of Lean line breaks are important diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 57aa9e121..a07ad35ae 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -164,7 +164,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let analyze_fun_decl_group (d : fun_declaration_group) : unit = (* Retrieve the function declarations *) - let funs = match d with NonRec id -> [ id ] | Rec ids -> ids in + let funs = match d with NonRecGroup id -> [ id ] | RecGroup ids -> ids in let funs = List.map (fun id -> FunDeclId.Map.find id funs_map) funs in let fun_ids = List.map (fun (d : fun_decl) -> d.def_id) funs in let fun_ids = FunDeclId.Set.of_list fun_ids in @@ -183,7 +183,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) | GlobalGroup id :: decls' -> (* Analyze a global by analyzing its body function *) let global = GlobalDeclId.Map.find id globals_map in - analyze_fun_decl_group (NonRec global.body); + analyze_fun_decl_group (NonRecGroup global.body); analyze_decl_groups decls' in diff --git a/compiler/Print.ml b/compiler/Print.ml index cd83a5898..48a5a20b8 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -1,6 +1,5 @@ include Charon.PrintUtils include Charon.PrintLlbcAst -open Charon.PrintPrimitiveValues open Charon.PrintTypes open Charon.PrintExpressions open Charon.PrintLlbcAst.Ast diff --git a/compiler/Pure.ml b/compiler/Pure.ml index fa059499a..40711e53f 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -14,6 +14,7 @@ module GlobalDeclId = A.GlobalDeclId module TraitDeclId = T.TraitDeclId module TraitImplId = T.TraitImplId module TraitClauseId = T.TraitClauseId +module Disambiguator = T.Disambiguator (** We redefine identifiers for loop: in {!Values}, the identifiers are global (they monotonically increase across functions) while in {!module:Pure} we want diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index d2747a4b7..2106c2063 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -3,10 +3,13 @@ open Pure open PureUtils open TranslateCore -module V = Values (** The local logger *) -let log = L.pure_micro_passes_log +let log = Logging.pure_micro_passes_log + +let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = + let fmt = trans_ctx_to_pure_fmt_env ctx in + PrintPure.fun_decl_to_string fmt def (** Small utility. @@ -597,8 +600,8 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = match TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls_groups with - | NonRec _ -> false - | Rec _ -> true + | NonRecGroup _ -> false + | RecGroup _ -> true in (* Convert, if possible - note that for now for Lean and Coq we don't support the structure syntax on recursive structures *) @@ -1420,14 +1423,15 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = let loop_body = { inputs; inputs_lvs; body = loop_body } in - let loop_def = + let loop_def : fun_decl = { def_id = def.def_id; kind = def.kind; num_loops; loop_id = Some loop.loop_id; back_id = def.back_id; - basename = def.basename; + llbc_name = def.llbc_name; + name = def.name; signature = loop_sig; is_global_decl_body = def.is_global_decl_body; body = Some loop_body; @@ -1539,10 +1543,12 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = mk_unit_rvalue | ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut - | ArrayRepeat | SliceLen ), + | ArrayRepeat ), _ ) -> super#visit_texpression env e) - | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> ( + | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> + failwith "TODO" + (* (* Lookup the function name *) let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in match @@ -1570,7 +1576,8 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = | _ -> raise (Failure "Unreachable") in mk_apps arg args - | _ -> super#visit_texpression env e) + | _ -> super#visit_texpression env e + *) | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e end @@ -1918,9 +1925,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : (* Debug *) log#ldebug (lazy - ("PureMicroPasses.apply_passes_to_def: " - ^ Print.fun_name_to_string def.basename - ^ " (" + ("PureMicroPasses.apply_passes_to_def: " ^ def.name ^ " (" ^ Print.option_to_string T.RegionGroupId.to_string def.back_id ^ ")")); diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 2460e0409..4e12d31e3 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3036,9 +3036,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = (* return *) def -let translate_type_decls (ctx : Contexts.decls_ctx) - (type_decls : T.type_decl list) : type_decl list = - List.map (translate_type_decl ctx) type_decls +let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = + List.map (translate_type_decl ctx) + (TypeDeclId.Map.values ctx.type_ctx.type_decls) (** Translates function signatures. diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 2aedb5445..cf23fd449 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -1,11 +1,11 @@ -open InterpreterStatements open Interpreter -module L = Logging -module T = Types -module A = LlbcAst +open Expressions +open Types +open Values +open LlbcAst +open Contexts module SA = SymbolicAst module Micro = PureMicroPasses -module C = Contexts open PureUtils open TranslateCore @@ -16,18 +16,17 @@ let log = TranslateCore.log - the list of symbolic values used for the input values - the generated symbolic AST *) -type symbolic_fun_translation = V.symbolic_value list * SA.expression +type symbolic_fun_translation = symbolic_value list * SA.expression (** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs, for the forward function and the backward functions. *) -let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl) - : symbolic_fun_translation option = +let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : + symbolic_fun_translation option = (* Debug *) log#ldebug (lazy - ("translate_function_to_symbolics: " - ^ Print.fun_name_to_string fdef.A.name)); + ("translate_function_to_symbolics: " ^ name_to_string trans_ctx fdef.name)); match fdef.body with | None -> None @@ -45,12 +44,11 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl) *) let translate_function_to_pure (trans_ctx : trans_ctx) (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdNotLoopMap.t) - (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl) - : pure_fun_translation_no_loops = + (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : fun_decl) : + pure_fun_translation_no_loops = (* Debug *) log#ldebug - (lazy - ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name)); + (lazy ("translate_function_to_pure: " ^ name_to_string trans_ctx fdef.name)); let def_id = fdef.def_id in @@ -61,22 +59,24 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Initialize the context *) let forward_sig = - RegularFunIdNotLoopMap.find (E.FRegular def_id, None) fun_sigs + RegularFunIdNotLoopMap.find (FRegular def_id, None) fun_sigs in - let sv_to_var = V.SymbolicValueId.Map.empty in + let sv_to_var = SymbolicValueId.Map.empty in let var_counter = Pure.VarId.generator_zero in let state_var, var_counter = Pure.VarId.fresh var_counter in let back_state_var, var_counter = Pure.VarId.fresh var_counter in let fuel0, var_counter = Pure.VarId.fresh var_counter in let fuel, var_counter = Pure.VarId.fresh var_counter in - let calls = V.FunCallId.Map.empty in - let abstractions = V.AbstractionId.Map.empty in + let calls = FunCallId.Map.empty in + let abstractions = AbstractionId.Map.empty in let recursive_type_decls = - T.TypeDeclId.Set.of_list + TypeDeclId.Set.of_list (List.filter_map (fun (tid, g) -> - match g with Charon.GAst.NonRec _ -> None | Rec _ -> Some tid) - (T.TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups)) + match g with + | Charon.GAst.NonRecGroup _ -> None + | RecGroup _ -> Some tid) + (TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups)) in let type_context = { @@ -104,9 +104,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx) *) let loop_ids_map = match symbolic_trans with - | None -> V.LoopId.Map.empty + | None -> LoopId.Map.empty | Some (_, ast) -> - let m = ref V.LoopId.Map.empty in + let m = ref LoopId.Map.empty in let _, fresh_loop_id = Pure.LoopId.fresh_stateful_generator () in let visitor = @@ -115,10 +115,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx) method! visit_loop env loop = let _ = - match V.LoopId.Map.find_opt loop.loop_id !m with + match LoopId.Map.find_opt loop.loop_id !m with | Some _ -> () - | None -> - m := V.LoopId.Map.add loop.loop_id (fresh_loop_id ()) !m + | None -> m := LoopId.Map.add loop.loop_id (fresh_loop_id ()) !m in super#visit_loop env loop end @@ -148,9 +147,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx) fun_decl = fdef; forward_inputs = []; (* Empty for now *) - backward_inputs = T.RegionGroupId.Map.empty; + backward_inputs = RegionGroupId.Map.empty; (* Empty for now *) - backward_outputs = T.RegionGroupId.Map.empty; + backward_outputs = RegionGroupId.Map.empty; loop_backward_outputs = None; (* Empty for now *) calls; @@ -171,7 +170,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | Some body, Some (input_svs, _) -> let forward_input_vars = LlbcAstUtils.fun_body_get_input_vars body in let forward_input_varnames = - List.map (fun (v : A.var) -> v.name) forward_input_vars + List.map (fun (v : var) -> v.name) forward_input_vars in let input_svs = List.combine forward_input_varnames input_svs in let ctx, forward_inputs = @@ -189,7 +188,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) in (* Translate the backward functions *) - let translate_backward (rg : T.region_group) : Pure.fun_decl = + let translate_backward (rg : region_group) : Pure.fun_decl = (* For the backward inputs/outputs initialization: we use the fact that * there are no nested borrows for now, and so that the region groups * can't have parents *) @@ -244,10 +243,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx) SymbolicToPure.fresh_vars backward_outputs ctx in let backward_inputs = - T.RegionGroupId.Map.singleton back_id backward_inputs + RegionGroupId.Map.singleton back_id backward_inputs in let backward_outputs = - T.RegionGroupId.Map.singleton back_id backward_outputs + RegionGroupId.Map.singleton back_id backward_outputs in (* Put everything in the context *) @@ -274,7 +273,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (pure_forward, pure_backwards) (* TODO: factor out the return type *) -let translate_crate_to_pure (crate : A.crate) : +let translate_crate_to_pure (crate : crate) : trans_ctx * Pure.type_decl list * pure_fun_translation list @@ -287,9 +286,7 @@ let translate_crate_to_pure (crate : A.crate) : let trans_ctx = compute_contexts crate in (* Translate all the type definitions *) - let type_decls = - SymbolicToPure.translate_type_decls (T.TypeDeclId.Map.values crate.types) - in + let type_decls = SymbolicToPure.translate_type_decls trans_ctx in (* Compute the type definition map *) let type_decls_map = @@ -301,24 +298,24 @@ let translate_crate_to_pure (crate : A.crate) : let assumed_sigs = List.map (fun (info : Assumed.assumed_fun_info) -> - ( E.FAssumed info.fun_id, + ( FAssumed info.fun_id, List.map (fun _ -> None) info.fun_sig.inputs, info.fun_sig )) Assumed.assumed_fun_infos in let local_sigs = List.map - (fun (fdef : A.fun_decl) -> + (fun (fdef : fun_decl) -> let input_names = match fdef.body with | None -> List.map (fun _ -> None) fdef.signature.inputs | Some body -> List.map - (fun (v : A.var) -> v.name) + (fun (v : var) -> v.name) (LlbcAstUtils.fun_body_get_input_vars body) in - (E.FRegular fdef.def_id, input_names, fdef.signature)) - (A.FunDeclId.Map.values crate.functions) + (FRegular fdef.def_id, input_names, fdef.signature)) + (FunDeclId.Map.values crate.fun_decls) in let sigs = List.append assumed_sigs local_sigs in let fun_sigs = SymbolicToPure.translate_fun_signatures trans_ctx sigs in @@ -327,22 +324,21 @@ let translate_crate_to_pure (crate : A.crate) : let pure_translations = List.map (translate_function_to_pure trans_ctx fun_sigs type_decls_map) - (A.FunDeclId.Map.values crate.functions) + (FunDeclId.Map.values crate.fun_decls) in (* Translate the trait declarations *) - let type_infos = trans_ctx.type_ctx.type_infos in let trait_decls = List.map - (SymbolicToPure.translate_trait_decl type_infos) - (T.TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) + (SymbolicToPure.translate_trait_decl trans_ctx) + (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) in (* Translate the trait implementations *) let trait_impls = List.map - (SymbolicToPure.translate_trait_impl type_infos) - (T.TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) + (SymbolicToPure.translate_trait_impl trans_ctx) + (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) in (* Apply the micro-passes *) @@ -401,9 +397,9 @@ let crate_has_opaque_non_builtin_decls (ctx : gen_ctx) (filter_assumed : bool) : log#ldebug (lazy ("Opaque decls:" ^ "\n- types:\n" - ^ String.concat ",\n" (List.map T.show_type_decl types) + ^ String.concat ",\n" (List.map show_type_decl types) ^ "\n- functions:\n" - ^ String.concat ",\n" (List.map A.show_fun_decl funs))); + ^ String.concat ",\n" (List.map show_fun_decl funs))); (types <> [], funs <> []) (** Export a type declaration. @@ -481,7 +477,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) let types_map = builtin_types_map () in List.map (fun (def : Pure.type_decl) -> - let sname = name_to_simple_name def.name in + let sname = name_to_simple_name def.llbc_name in SimpleNameMap.find_opt sname types_map <> None) defs in @@ -531,10 +527,10 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) TODO: check correct behavior with opaque globals. *) let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) - (id : A.GlobalDeclId.id) : unit = + (id : GlobalDeclId.id) : unit = let global_decls = ctx.trans_ctx.global_ctx.global_decls in - let global = A.GlobalDeclId.Map.find id global_decls in - let trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in + let global = GlobalDeclId.Map.find id global_decls in + let trans = FunDeclId.Map.find global.body ctx.trans_funs in assert (trans.fwd.loops = []); assert (trans.backs = []); let body = trans.fwd.f in @@ -665,7 +661,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let funs_map = builtin_funs_map () in List.map (fun (trans : pure_fun_translation) -> - let sname = name_to_simple_name trans.fwd.f.basename in + let sname = name_to_simple_name trans.fwd.f.llbc_name in SimpleNameMap.find_opt sname funs_map <> None) pure_ls in @@ -756,10 +752,10 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let export_trait_decl (fmt : Format.formatter) (_config : gen_config) (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) (extract_decl : bool) (extract_extra_info : bool) : unit = - let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in + let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in (* Check if the trait declaration is builtin, in which case we ignore it *) let open ExtractBuiltin in - let sname = name_to_simple_name trait_decl.name in + let sname = name_to_simple_name trait_decl.llbc_name in if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then ( let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in if extract_decl then Extract.extract_trait_decl ctx fmt trait_decl; @@ -771,7 +767,7 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config) let export_trait_impl (fmt : Format.formatter) (_config : gen_config) (ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit = (* Lookup the definition *) - let trait_impl = T.TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in + let trait_impl = TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in let trait_decl = Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id ctx.trans_trait_decls @@ -779,8 +775,8 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config) (* Check if the trait implementation is builtin *) let builtin_info = let open ExtractBuiltin in - let type_sname = name_to_simple_name trait_impl.name in - let trait_sname = name_to_simple_name trait_decl.name in + let type_sname = name_to_simple_name trait_impl.llbc_name in + let trait_sname = name_to_simple_name trait_decl.llbc_name in SimpleNamePairMap.find_opt (type_sname, trait_sname) (builtin_trait_impls_map ()) in @@ -817,14 +813,15 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) Extract.extract_state_type fmt ctx kind in - let export_decl_group (dg : A.declaration_group) : unit = + let export_decl_group (dg : declaration_group) : unit = match dg with - | Type (NonRec id) -> + | TypeGroup (NonRecGroup id) -> if config.extract_types then export_types_group false [ id ] - | Type (Rec ids) -> if config.extract_types then export_types_group true ids - | Fun (NonRec id) -> ( + | TypeGroup (RecGroup ids) -> + if config.extract_types then export_types_group true ids + | FunGroup (NonRecGroup id) -> ( (* Lookup *) - let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in + let pure_fun = FunDeclId.Map.find id ctx.trans_funs in (* Special case: we skip trait method *declarations* (we will extract their type directly in the records we generate for the trait declarations themselves, there is no point in having @@ -834,21 +831,21 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) | _ -> (* Translate *) export_functions_group [ pure_fun ]) - | Fun (Rec ids) -> + | FunGroup (RecGroup ids) -> (* General case of mutually recursive functions *) (* Lookup *) let pure_funs = - List.map (fun id -> A.FunDeclId.Map.find id ctx.trans_funs) ids + List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids in (* Translate *) export_functions_group pure_funs - | Global id -> export_global id - | TraitDecl id -> + | GlobalGroup id -> export_global id + | TraitDeclGroup id -> (* TODO: update to extract groups *) if config.extract_trait_decls && config.extract_transparent then ( export_trait_decl_group id; export_trait_decl_group_extra_info id) - | TraitImpl id -> + | TraitImplGroup id -> if config.extract_trait_impls && config.extract_transparent then export_trait_impl id in @@ -986,7 +983,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) close_out out (** Translate a crate and write the synthesized code to an output file. *) -let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : +let translate_crate (filename : string) (dest_dir : string) (crate : crate) : unit = (* Translate the module to the pure AST *) let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls = @@ -1036,8 +1033,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : Pure.TypeDeclId.Map.of_list (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types) in - let trans_funs : pure_fun_translation A.FunDeclId.Map.t = - A.FunDeclId.Map.of_list + let trans_funs : pure_fun_translation FunDeclId.Map.t = + FunDeclId.Map.of_list (List.map (fun (trans : pure_fun_translation) -> (trans.fwd.f.def_id, trans)) trans_funs) @@ -1046,13 +1043,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (* Put everything in the context *) let ctx = let trans_trait_decls = - T.TraitDeclId.Map.of_list + TraitDeclId.Map.of_list (List.map (fun (d : Pure.trait_decl) -> (d.def_id, d)) trans_trait_decls) in let trans_trait_impls = - T.TraitImplId.Map.of_list + TraitImplId.Map.of_list (List.map (fun (d : Pure.trait_impl) -> (d.def_id, d)) trans_trait_impls) @@ -1107,12 +1104,12 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : if is_global then ctx else Extract.extract_fun_decl_register_names ctx gen_decr_clause trans) ctx - (A.FunDeclId.Map.values trans_funs) + (FunDeclId.Map.values trans_funs) in let ctx = List.fold_left Extract.extract_global_decl_register_names ctx - (A.GlobalDeclId.Map.values crate.globals) + (GlobalDeclId.Map.values crate.global_decls) in let ctx = @@ -1291,7 +1288,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : namespace; in_namespace = true; crate_name; - rust_module_name = crate.A.name; + rust_module_name = crate.name; module_name = types_module; custom_msg = ": type definitions"; custom_imports = []; @@ -1319,7 +1316,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : namespace; in_namespace = true; crate_name; - rust_module_name = crate.A.name; + rust_module_name = crate.name; module_name = template_clauses_module; custom_msg = ": templates for the decreases clauses"; custom_imports = [ types_module ]; @@ -1369,7 +1366,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : namespace; in_namespace = false; crate_name; - rust_module_name = crate.A.name; + rust_module_name = crate.name; module_name = opaque_module; custom_msg; custom_imports = []; @@ -1408,7 +1405,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : namespace; in_namespace = true; crate_name; - rust_module_name = crate.A.name; + rust_module_name = crate.name; module_name = fun_module; custom_msg = ": function definitions"; custom_imports = []; @@ -1441,7 +1438,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : namespace; in_namespace = true; crate_name; - rust_module_name = crate.A.name; + rust_module_name = crate.name; module_name = crate_name; custom_msg = ""; custom_imports = []; diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml index a148175d3..a974cdeec 100644 --- a/compiler/TranslateCore.ml +++ b/compiler/TranslateCore.ml @@ -26,3 +26,6 @@ let trans_ctx_to_fmt_env (ctx : trans_ctx) : Print.fmt_env = let trans_ctx_to_pure_fmt_env (ctx : trans_ctx) : PrintPure.fmt_env = PrintPure.decls_ctx_to_fmt_env ctx + +let name_to_string (ctx : trans_ctx) = + Print.Types.name_to_string (trans_ctx_to_fmt_env ctx) diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml index 659eac591..5371a3d71 100644 --- a/compiler/TypesAnalysis.ml +++ b/compiler/TypesAnalysis.ml @@ -283,7 +283,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos) let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t) (infos : type_infos) (decl : A.type_declaration_group) : type_infos = (* Collect the identifiers used in the declaration group *) - let ids = match decl with NonRec id -> [ id ] | Rec ids -> ids in + let ids = match decl with NonRecGroup id -> [ id ] | RecGroup ids -> ids in (* Retrieve the type definitions *) let decl_defs = List.map (fun id -> TypeDeclId.Map.find id type_decls) ids in (* Initialize the type information for the current definitions *)