Merge pull request #175 from AeneasVerif/afromher/meta

Rename meta into span

1 files changed, 68 insertions, 68 deletions

diff --git a/compiler/Print.ml b/compiler/Print.ml
index 51286553..f7f1f54b 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -44,13 +44,13 @@ module Values = struct
    * typed_avalue_to_string. At some point we had done it, because [typed_value]
    * and [typed_avalue] were instances of the same general type [g_typed_value],
    * but then we removed this general type because it proved to be a bad idea. *)
-  let rec typed_value_to_string ?(meta : Meta.meta option = None)
+  let rec typed_value_to_string ?(span : Meta.span option = None)
       (env : fmt_env) (v : typed_value) : string =
     match v.value with
     | VLiteral cv -> literal_to_string cv
     | VAdt av -> (
         let field_values =
-          List.map (typed_value_to_string ~meta env) av.field_values
+          List.map (typed_value_to_string ~span env) av.field_values
         in
         match v.ty with
         | TAdt (TTuple, _) ->
@@ -86,31 +86,31 @@ module Values = struct
                 (* Happens when we aggregate values *)
                 "@Array[" ^ String.concat ", " field_values ^ "]"
             | _ ->
-                craise_opt_meta __FILE__ __LINE__ meta
+                craise_opt_span __FILE__ __LINE__ span
                   ("Inconsistent value: " ^ show_typed_value v))
-        | _ -> craise_opt_meta __FILE__ __LINE__ meta "Inconsistent typed value"
+        | _ -> craise_opt_span __FILE__ __LINE__ span "Inconsistent typed value"
         )
     | VBottom -> "⊥ : " ^ ty_to_string env v.ty
-    | VBorrow bc -> borrow_content_to_string ~meta env bc
-    | VLoan lc -> loan_content_to_string ~meta env lc
+    | VBorrow bc -> borrow_content_to_string ~span env bc
+    | VLoan lc -> loan_content_to_string ~span env lc
     | VSymbolic s -> symbolic_value_to_string env s
 
-  and borrow_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
+  and borrow_content_to_string ?(span : Meta.span option = None) (env : fmt_env)
       (bc : borrow_content) : string =
     match bc with
     | VSharedBorrow bid -> "shared_borrow@" ^ BorrowId.to_string bid
     | VMutBorrow (bid, tv) ->
         "mut_borrow@" ^ BorrowId.to_string bid ^ " ("
-        ^ typed_value_to_string ~meta env tv
+        ^ typed_value_to_string ~span env tv
         ^ ")"
     | VReservedMutBorrow bid -> "reserved_borrow@" ^ BorrowId.to_string bid
 
-  and loan_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
+  and loan_content_to_string ?(span : Meta.span option = None) (env : fmt_env)
       (lc : loan_content) : string =
     match lc with
     | VSharedLoan (loans, v) ->
         let loans = BorrowId.Set.to_string None loans in
-        "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string ~meta env v ^ ")"
+        "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string ~span env v ^ ")"
     | VMutLoan bid -> "ml@" ^ BorrowId.to_string bid
 
   let abstract_shared_borrow_to_string (env : fmt_env)
@@ -148,12 +148,12 @@ module Values = struct
     | AEndedProjBorrows _mv -> "_"
     | AIgnoredProjBorrows -> "_"
 
-  let rec typed_avalue_to_string ?(meta : Meta.meta option = None)
+  let rec typed_avalue_to_string ?(span : Meta.span option = None)
       (env : fmt_env) (v : typed_avalue) : string =
     match v.value with
     | AAdt av -> (
         let field_values =
-          List.map (typed_avalue_to_string ~meta env) av.field_values
+          List.map (typed_avalue_to_string ~span env) av.field_values
         in
         match v.ty with
         | TAdt (TTuple, _) ->
@@ -185,77 +185,77 @@ module Values = struct
             (* Assumed type *)
             match (aty, field_values) with
             | TBox, [ bv ] -> "@Box(" ^ bv ^ ")"
-            | _ -> craise_opt_meta __FILE__ __LINE__ meta "Inconsistent value")
-        | _ -> craise_opt_meta __FILE__ __LINE__ meta "Inconsistent typed value"
+            | _ -> craise_opt_span __FILE__ __LINE__ span "Inconsistent value")
+        | _ -> craise_opt_span __FILE__ __LINE__ span "Inconsistent typed value"
         )
     | ABottom -> "⊥ : " ^ ty_to_string env v.ty
-    | ABorrow bc -> aborrow_content_to_string ~meta env bc
-    | ALoan lc -> aloan_content_to_string ~meta env lc
+    | ABorrow bc -> aborrow_content_to_string ~span env bc
+    | ALoan lc -> aloan_content_to_string ~span env lc
     | ASymbolic s -> aproj_to_string env s
     | AIgnored -> "_"
 
-  and aloan_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
+  and aloan_content_to_string ?(span : Meta.span option = None) (env : fmt_env)
       (lc : aloan_content) : string =
     match lc with
     | AMutLoan (bid, av) ->
         "@mut_loan(" ^ BorrowId.to_string bid ^ ", "
-        ^ typed_avalue_to_string ~meta env av
+        ^ typed_avalue_to_string ~span env av
         ^ ")"
     | ASharedLoan (loans, v, av) ->
         let loans = BorrowId.Set.to_string None loans in
         "@shared_loan(" ^ loans ^ ", "
-        ^ typed_value_to_string ~meta env v
+        ^ typed_value_to_string ~span env v
         ^ ", "
-        ^ typed_avalue_to_string ~meta env av
+        ^ typed_avalue_to_string ~span env av
         ^ ")"
     | AEndedMutLoan ml ->
         "@ended_mut_loan{"
-        ^ typed_avalue_to_string ~meta env ml.child
+        ^ typed_avalue_to_string ~span env ml.child
         ^ "; "
-        ^ typed_avalue_to_string ~meta env ml.given_back
+        ^ typed_avalue_to_string ~span env ml.given_back
         ^ " }"
     | AEndedSharedLoan (v, av) ->
         "@ended_shared_loan("
-        ^ typed_value_to_string ~meta env v
+        ^ typed_value_to_string ~span env v
         ^ ", "
-        ^ typed_avalue_to_string ~meta env av
+        ^ typed_avalue_to_string ~span env av
         ^ ")"
     | AIgnoredMutLoan (opt_bid, av) ->
         "@ignored_mut_loan("
         ^ option_to_string BorrowId.to_string opt_bid
         ^ ", "
-        ^ typed_avalue_to_string ~meta env av
+        ^ typed_avalue_to_string ~span env av
         ^ ")"
     | AEndedIgnoredMutLoan ml ->
         "@ended_ignored_mut_loan{ "
-        ^ typed_avalue_to_string ~meta env ml.child
+        ^ typed_avalue_to_string ~span env ml.child
         ^ "; "
-        ^ typed_avalue_to_string ~meta env ml.given_back
+        ^ typed_avalue_to_string ~span env ml.given_back
         ^ "}"
     | AIgnoredSharedLoan sl ->
-        "@ignored_shared_loan(" ^ typed_avalue_to_string ~meta env sl ^ ")"
+        "@ignored_shared_loan(" ^ typed_avalue_to_string ~span env sl ^ ")"
 
-  and aborrow_content_to_string ?(meta : Meta.meta option = None)
+  and aborrow_content_to_string ?(span : Meta.span option = None)
       (env : fmt_env) (bc : aborrow_content) : string =
     match bc with
     | AMutBorrow (bid, av) ->
         "mb@" ^ BorrowId.to_string bid ^ " ("
-        ^ typed_avalue_to_string ~meta env av
+        ^ typed_avalue_to_string ~span env av
         ^ ")"
     | ASharedBorrow bid -> "sb@" ^ BorrowId.to_string bid
     | AIgnoredMutBorrow (opt_bid, av) ->
         "@ignored_mut_borrow("
         ^ option_to_string BorrowId.to_string opt_bid
         ^ ", "
-        ^ typed_avalue_to_string ~meta env av
+        ^ typed_avalue_to_string ~span env av
         ^ ")"
     | AEndedMutBorrow (_mv, child) ->
-        "@ended_mut_borrow(" ^ typed_avalue_to_string ~meta env child ^ ")"
-    | AEndedIgnoredMutBorrow { child; given_back; given_back_meta = _ } ->
+        "@ended_mut_borrow(" ^ typed_avalue_to_string ~span env child ^ ")"
+    | AEndedIgnoredMutBorrow { child; given_back; given_back_span = _ } ->
         "@ended_ignored_mut_borrow{ "
-        ^ typed_avalue_to_string ~meta env child
+        ^ typed_avalue_to_string ~span env child
         ^ "; "
-        ^ typed_avalue_to_string ~meta env given_back
+        ^ typed_avalue_to_string ~span env given_back
         ^ ")"
     | AEndedSharedBorrow -> "@ended_shared_borrow"
     | AProjSharedBorrow sb ->
@@ -285,13 +285,13 @@ module Values = struct
         ^ ")"
     | Identity -> "Identity"
 
-  let abs_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
+  let abs_to_string ?(span : Meta.span option = None) (env : fmt_env)
       (verbose : bool) (indent : string) (indent_incr : string) (abs : abs) :
       string =
     let indent2 = indent ^ indent_incr in
     let avs =
       List.map
-        (fun av -> indent2 ^ typed_avalue_to_string ~meta env av)
+        (fun av -> indent2 ^ typed_avalue_to_string ~span env av)
         abs.avalues
     in
     let avs = String.concat ",\n" avs in
@@ -335,7 +335,7 @@ module Contexts = struct
     | BVar b -> var_binder_to_string env b
     | BDummy bid -> dummy_var_id_to_string bid
 
-  let env_elem_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
+  let env_elem_to_string ?(span : Meta.span option = None) (env : fmt_env)
       (verbose : bool) (with_var_types : bool) (indent : string)
       (indent_incr : string) (ev : env_elem) : string =
     match ev with
@@ -344,18 +344,18 @@ module Contexts = struct
         let ty =
           if with_var_types then " : " ^ ty_to_string env tv.ty else ""
         in
-        indent ^ bv ^ ty ^ " -> " ^ typed_value_to_string ~meta env tv ^ " ;"
-    | EAbs abs -> abs_to_string ~meta env verbose indent indent_incr abs
+        indent ^ bv ^ ty ^ " -> " ^ typed_value_to_string ~span env tv ^ " ;"
+    | EAbs abs -> abs_to_string ~span env verbose indent indent_incr abs
     | EFrame ->
-        craise_opt_meta __FILE__ __LINE__ meta "Can't print a Frame element"
+        craise_opt_span __FILE__ __LINE__ span "Can't print a Frame element"
 
-  let opt_env_elem_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
+  let opt_env_elem_to_string ?(span : Meta.span option = None) (env : fmt_env)
       (verbose : bool) (with_var_types : bool) (indent : string)
       (indent_incr : string) (ev : env_elem option) : string =
     match ev with
     | None -> indent ^ "..."
     | Some ev ->
-        env_elem_to_string ~meta env verbose with_var_types indent indent_incr
+        env_elem_to_string ~span env verbose with_var_types indent indent_incr
           ev
 
   (** Filters "dummy" bindings from an environment, to gain space and clarity/
@@ -393,7 +393,7 @@ module Contexts = struct
       "..." to gain space and clarity.
       [with_var_types]: if true, print the type of the variables
    *)
-  let env_to_string ?(meta : Meta.meta option = None) (filter : bool)
+  let env_to_string ?(span : Meta.span option = None) (filter : bool)
       (fmt_env : fmt_env) (verbose : bool) (with_var_types : bool) (env : env) :
       string =
     let env =
@@ -403,7 +403,7 @@ module Contexts = struct
     ^ String.concat "\n"
         (List.map
            (fun ev ->
-             opt_env_elem_to_string ~meta fmt_env verbose with_var_types "  "
+             opt_env_elem_to_string ~span fmt_env verbose with_var_types "  "
                "  " ev)
            env)
     ^ "\n}"
@@ -484,7 +484,7 @@ module Contexts = struct
     let frames = split_aux [] [] env in
     frames
 
-  let eval_ctx_to_string_gen ?(meta : Meta.meta option = None) (verbose : bool)
+  let eval_ctx_to_string_gen ?(span : Meta.span option = None) (verbose : bool)
       (filter : bool) (with_var_types : bool) (ctx : eval_ctx) : string =
     let fmt_env = eval_ctx_to_fmt_env ctx in
     let ended_regions = RegionId.Set.to_string None ctx.ended_regions in
@@ -502,26 +502,26 @@ module Contexts = struct
               | EBinding (BDummy _, _) -> num_dummies := !num_abs + 1
               | EBinding (BVar _, _) -> num_bindings := !num_bindings + 1
               | EAbs _ -> num_abs := !num_abs + 1
-              | _ -> craise_opt_meta __FILE__ __LINE__ meta "Unreachable")
+              | _ -> craise_opt_span __FILE__ __LINE__ span "Unreachable")
             f;
           "\n# Frame " ^ string_of_int i ^ ":" ^ "\n- locals: "
           ^ string_of_int !num_bindings
           ^ "\n- dummy bindings: " ^ string_of_int !num_dummies
           ^ "\n- abstractions: " ^ string_of_int !num_abs ^ "\n"
-          ^ env_to_string ~meta filter fmt_env verbose with_var_types f
+          ^ env_to_string ~span filter fmt_env verbose with_var_types f
           ^ "\n")
         frames
     in
     "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames
     ^ " frame(s)\n" ^ String.concat "" frames
 
-  let eval_ctx_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) :
+  let eval_ctx_to_string ?(span : Meta.span option = None) (ctx : eval_ctx) :
       string =
-    eval_ctx_to_string_gen ~meta false true true ctx
+    eval_ctx_to_string_gen ~span false true true ctx
 
-  let eval_ctx_to_string_no_filter ?(meta : Meta.meta option = None)
+  let eval_ctx_to_string_no_filter ?(span : Meta.span option = None)
       (ctx : eval_ctx) : string =
-    eval_ctx_to_string_gen ~meta false false true ctx
+    eval_ctx_to_string_gen ~span false false true ctx
 end
 
 (** Pretty-printing for LLBC ASTs (functions based on an evaluation context) *)
@@ -559,25 +559,25 @@ module EvalCtx = struct
     let env = eval_ctx_to_fmt_env ctx in
     trait_instance_id_to_string env x
 
-  let borrow_content_to_string ?(meta : Meta.meta option = None)
+  let borrow_content_to_string ?(span : Meta.span option = None)
       (ctx : eval_ctx) (bc : borrow_content) : string =
     let env = eval_ctx_to_fmt_env ctx in
-    borrow_content_to_string ~meta env bc
+    borrow_content_to_string ~span env bc
 
-  let loan_content_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx)
+  let loan_content_to_string ?(span : Meta.span option = None) (ctx : eval_ctx)
       (lc : loan_content) : string =
     let env = eval_ctx_to_fmt_env ctx in
-    loan_content_to_string ~meta env lc
+    loan_content_to_string ~span env lc
 
-  let aborrow_content_to_string ?(meta : Meta.meta option = None)
+  let aborrow_content_to_string ?(span : Meta.span option = None)
       (ctx : eval_ctx) (bc : aborrow_content) : string =
     let env = eval_ctx_to_fmt_env ctx in
-    aborrow_content_to_string ~meta env bc
+    aborrow_content_to_string ~span env bc
 
-  let aloan_content_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx)
+  let aloan_content_to_string ?(span : Meta.span option = None) (ctx : eval_ctx)
       (lc : aloan_content) : string =
     let env = eval_ctx_to_fmt_env ctx in
-    aloan_content_to_string ~meta env lc
+    aloan_content_to_string ~span env lc
 
   let aproj_to_string (ctx : eval_ctx) (p : aproj) : string =
     let env = eval_ctx_to_fmt_env ctx in
@@ -587,15 +587,15 @@ module EvalCtx = struct
     let env = eval_ctx_to_fmt_env ctx in
     symbolic_value_to_string env sv
 
-  let typed_value_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx)
+  let typed_value_to_string ?(span : Meta.span option = None) (ctx : eval_ctx)
       (v : typed_value) : string =
     let env = eval_ctx_to_fmt_env ctx in
-    typed_value_to_string ~meta env v
+    typed_value_to_string ~span env v
 
-  let typed_avalue_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx)
+  let typed_avalue_to_string ?(span : Meta.span option = None) (ctx : eval_ctx)
       (v : typed_avalue) : string =
     let env = eval_ctx_to_fmt_env ctx in
-    typed_avalue_to_string ~meta env v
+    typed_avalue_to_string ~span env v
 
   let place_to_string (ctx : eval_ctx) (op : place) : string =
     let env = eval_ctx_to_fmt_env ctx in
@@ -636,13 +636,13 @@ module EvalCtx = struct
     let env = eval_ctx_to_fmt_env ctx in
     trait_impl_to_string env "  " "  " timpl
 
-  let env_elem_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx)
+  let env_elem_to_string ?(span : Meta.span option = None) (ctx : eval_ctx)
       (indent : string) (indent_incr : string) (ev : env_elem) : string =
     let env = eval_ctx_to_fmt_env ctx in
-    env_elem_to_string ~meta env false true indent indent_incr ev
+    env_elem_to_string ~span env false true indent indent_incr ev
 
-  let abs_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx)
+  let abs_to_string ?(span : Meta.span option = None) (ctx : eval_ctx)
       (indent : string) (indent_incr : string) (abs : abs) : string =
     let env = eval_ctx_to_fmt_env ctx in
-    abs_to_string ~meta env false indent indent_incr abs
+    abs_to_string ~span env false indent indent_incr abs
 end