diff options
author | Son HO | 2024-06-04 14:05:44 +0200 |
---|---|---|
committer | GitHub | 2024-06-04 14:05:44 +0200 |
commit | afc4e62ce7a584da0bb0a7350533e321388be545 (patch) | |
tree | 89f3b6999e1697595f1c3fbb2d9c4d8c60a69e49 /compiler/Print.ml | |
parent | 4a31acdff7a5dfdc26bf25ad25bb8266b790f891 (diff) | |
parent | 3ad6c4712fd41efec55f29af5ccc31f68a0e12cf (diff) |
Merge pull request #228 from AeneasVerif/son/loops2
Add support for projection markers when joining environments
Diffstat (limited to 'compiler/Print.ml')
-rw-r--r-- | compiler/Print.ml | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/compiler/Print.ml b/compiler/Print.ml index f7f1f54b..7495d6bf 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -148,6 +148,13 @@ module Values = struct | AEndedProjBorrows _mv -> "_" | AIgnoredProjBorrows -> "_" + (** Wrap a value inside its marker, if there is one *) + let add_proj_marker (pm : proj_marker) (s : string) : string = + match pm with + | PNone -> s + | PLeft -> "|" ^ s ^ "|" + | PRight -> "︙" ^ s ^ "︙" + let rec typed_avalue_to_string ?(span : Meta.span option = None) (env : fmt_env) (v : typed_avalue) : string = match v.value with @@ -197,17 +204,19 @@ module Values = struct and aloan_content_to_string ?(span : Meta.span option = None) (env : fmt_env) (lc : aloan_content) : string = match lc with - | AMutLoan (bid, av) -> + | AMutLoan (pm, bid, av) -> "@mut_loan(" ^ BorrowId.to_string bid ^ ", " ^ typed_avalue_to_string ~span env av ^ ")" - | ASharedLoan (loans, v, av) -> + |> add_proj_marker pm + | ASharedLoan (pm, loans, v, av) -> let loans = BorrowId.Set.to_string None loans in "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string ~span env v ^ ", " ^ typed_avalue_to_string ~span env av ^ ")" + |> add_proj_marker pm | AEndedMutLoan ml -> "@ended_mut_loan{" ^ typed_avalue_to_string ~span env ml.child @@ -238,11 +247,13 @@ module Values = struct and aborrow_content_to_string ?(span : Meta.span option = None) (env : fmt_env) (bc : aborrow_content) : string = match bc with - | AMutBorrow (bid, av) -> + | AMutBorrow (pm, bid, av) -> "mb@" ^ BorrowId.to_string bid ^ " (" ^ typed_avalue_to_string ~span env av ^ ")" - | ASharedBorrow bid -> "sb@" ^ BorrowId.to_string bid + |> add_proj_marker pm + | ASharedBorrow (pm, bid) -> + "sb@" ^ BorrowId.to_string bid |> add_proj_marker pm | AIgnoredMutBorrow (opt_bid, av) -> "@ignored_mut_borrow(" ^ option_to_string BorrowId.to_string opt_bid |