From b294639a5cbd2a51fc5bb5e55e0c386ee568ca8c Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 24 May 2024 13:28:12 +0200 Subject: Rename meta into span --- compiler/Print.ml | 136 +++++++++++++++++++++++++++--------------------------- 1 file changed, 68 insertions(+), 68 deletions(-) (limited to 'compiler/Print.ml') 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 -- cgit v1.2.3