From 50dbeaeb018ab2cb44df3f557f1958eb15351f31 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Fri, 24 May 2024 12:47:43 +0200
Subject: Rename span into raw_span
---
compiler/Errors.ml | 8 ++++----
compiler/Extract.ml | 14 +++++++-------
compiler/ExtractTypes.ml | 16 ++++++++--------
compiler/Pure.ml | 2 +-
4 files changed, 20 insertions(+), 20 deletions(-)
(limited to 'compiler')
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.
--
cgit v1.2.3