diff options
| -rw-r--r-- | compiler/Errors.ml | 8 | ||||
| -rw-r--r-- | compiler/Extract.ml | 14 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 16 | ||||
| -rw-r--r-- | compiler/Pure.ml | 2 |
4 files changed, 20 insertions, 20 deletions
diff --git a/compiler/Errors.ml b/compiler/Errors.ml index 30887593..d084df51 100644 --- a/compiler/Errors.ml +++ b/compiler/Errors.ml @@ -1,13 +1,13 @@ let log = Logging.errors_log let meta_to_string (meta : Meta.meta) = - let span = meta.span in - let file = match span.file with Virtual s | Local s -> s in + let raw_span = meta.span in + let file = match raw_span.file with Virtual s | Local s -> s in let loc_to_string (l : Meta.loc) : string = string_of_int l.line ^ ":" ^ string_of_int l.col in - "Source: '" ^ file ^ "', lines " ^ loc_to_string span.beg_loc ^ "-" - ^ loc_to_string span.end_loc + "Source: '" ^ file ^ "', lines " ^ loc_to_string raw_span.beg_loc ^ "-" + ^ loc_to_string raw_span.end_loc let format_error_message (meta : Meta.meta option) (msg : string) = let meta = diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 8efb59fb..65f7b06e 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1249,7 +1249,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) Some def.llbc_name else None in - extract_comment_with_span ctx fmt + extract_comment_with_raw_span ctx fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ] name def.meta.span); F.pp_print_space fmt (); @@ -1316,7 +1316,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) (* 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_with_span ctx fmt + extract_comment_with_raw_span ctx fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ] None def.meta.span; F.pp_print_space fmt (); @@ -1371,7 +1371,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) let def_name = ctx_get_decreases_proof def.meta def.def_id def.loop_id ctx in (* syntax <def_name> term ... term : tactic *) F.pp_print_break fmt 0 0; - extract_comment_with_span ctx fmt + extract_comment_with_raw_span ctx fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ] None def.meta.span; F.pp_print_space fmt (); @@ -1418,7 +1418,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) Some def.llbc_name else None in - extract_comment_with_span ctx fmt comment name def.meta.span + extract_comment_with_raw_span ctx fmt comment name def.meta.span (** Extract a function declaration. @@ -1892,7 +1892,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) Some global.llbc_name else None in - extract_comment_with_span ctx fmt + extract_comment_with_raw_span ctx fmt [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ] name global.meta.span; F.pp_print_space fmt (); @@ -2354,7 +2354,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) Some decl.llbc_name else None in - extract_comment_with_span ctx fmt + extract_comment_with_raw_span ctx fmt [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ] name decl.meta.span); F.pp_print_break fmt 0 0; @@ -2653,7 +2653,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) Some (trait_decl.llbc_generics, decl_ref.decl_generics) ) else (None, None) in - extract_comment_with_span ctx fmt + extract_comment_with_raw_span ctx fmt [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ] (* TODO: why option option for the generics? Looks like a bug in OCaml!? *) name ?generics:(Some generics) impl.meta.span); diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 6a6067de..44744577 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1146,17 +1146,17 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit = F.pp_print_string fmt rd; F.pp_close_box fmt () -let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter) +let extract_comment_with_raw_span (ctx : extraction_ctx) (fmt : F.formatter) (sl : string list) (name : Types.name option) ?(generics : (Types.generic_params * Types.generic_args) option = None) - (span : Meta.span) : unit = - let file = match span.file with Virtual s | Local s -> s in + (raw_span : Meta.raw_span) : unit = + let file = match raw_span.file with Virtual s | Local s -> s in let loc_to_string (l : Meta.loc) : string = string_of_int l.line ^ ":" ^ string_of_int l.col in - let span = - "Source: '" ^ file ^ "', lines " ^ loc_to_string span.beg_loc ^ "-" - ^ loc_to_string span.end_loc + let raw_span = + "Source: '" ^ file ^ "', lines " ^ loc_to_string raw_span.beg_loc ^ "-" + ^ loc_to_string raw_span.end_loc in let name = match (name, generics) with @@ -1169,7 +1169,7 @@ let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter) ^ name_with_generics_to_pattern_string ctx.trans_ctx name params args; ] in - extract_comment fmt (sl @ [ span ] @ name) + extract_comment fmt (sl @ [ raw_span ] @ name) let extract_trait_clause_type (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) @@ -1414,7 +1414,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) Some def.llbc_name else None in - extract_comment_with_span ctx fmt + extract_comment_with_raw_span ctx fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ] name def.meta.span); F.pp_print_break fmt 0 0; diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 451767f8..a07167a8 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -50,7 +50,7 @@ type region_group_id = T.region_group_id [@@deriving show, ord] type mutability = Mut | Const [@@deriving show, ord] type loc = Meta.loc [@@deriving show, ord] type file_name = Meta.file_name [@@deriving show, ord] -type span = Meta.span [@@deriving show, ord] +type raw_span = Meta.raw_span [@@deriving show, ord] type meta = Meta.meta [@@deriving show, ord] (** The assumed types for the pure AST. |