diff options
author | Son HO | 2024-03-09 01:12:20 +0100 |
---|---|---|
committer | GitHub | 2024-03-09 01:12:20 +0100 |
commit | 14171474f9a4a45874d181cdb6567c7af7dc32cd (patch) | |
tree | f4c7dcd5b172e8922487dec83070e2c38e7b441a /compiler/Print.ml | |
parent | 169d011cbfa83d853d0148bbf6b946e6ccbe4c4c (diff) | |
parent | 46f2f1c0c4c37f089e42c82d76d79817101c5407 (diff) |
Merge pull request #85 from AeneasVerif/son/fix_loops3
Fix some issues with the loops
Diffstat (limited to '')
-rw-r--r-- | compiler/Print.ml | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/compiler/Print.ml b/compiler/Print.ml index 8999c77d..0c69bd05 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -16,6 +16,10 @@ module Expressions = Charon.PrintExpressions let list_to_string (to_string : 'a -> string) (ls : 'a list) : string = "[" ^ String.concat "; " (List.map to_string ls) ^ "]" +let pair_to_string (to_string0 : 'a -> string) (to_string1 : 'b -> string) + ((x, y) : 'a * 'b) : string = + "(" ^ to_string0 x ^ ", " ^ to_string1 y ^ ")" + let bool_to_string (b : bool) : string = if b then "true" else "false" (** Pretty-printing for values *) @@ -88,19 +92,19 @@ module Values = struct and borrow_content_to_string (env : fmt_env) (bc : borrow_content) : string = match bc with - | VSharedBorrow bid -> "⌊shared@" ^ BorrowId.to_string bid ^ "⌋" + | VSharedBorrow bid -> "shared_borrow@" ^ BorrowId.to_string bid | VMutBorrow (bid, tv) -> - "&mut@" ^ BorrowId.to_string bid ^ " (" + "mut_borrow@" ^ BorrowId.to_string bid ^ " (" ^ typed_value_to_string env tv ^ ")" - | VReservedMutBorrow bid -> "⌊reserved_mut@" ^ BorrowId.to_string bid ^ "⌋" + | VReservedMutBorrow bid -> "reserved_borrow@" ^ BorrowId.to_string bid and loan_content_to_string (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 env v ^ ")" - | VMutLoan bid -> "⌊mut@" ^ BorrowId.to_string bid ^ "⌋" + | VMutLoan bid -> "ml@" ^ BorrowId.to_string bid let abstract_shared_borrow_to_string (env : fmt_env) (abs : abstract_shared_borrow) : string = @@ -184,9 +188,9 @@ module Values = struct and aloan_content_to_string (env : fmt_env) (lc : aloan_content) : string = match lc with | AMutLoan (bid, av) -> - "⌊mut@" ^ BorrowId.to_string bid ^ ", " + "@mut_loan(" ^ BorrowId.to_string bid ^ ", " ^ typed_avalue_to_string env av - ^ "⌋" + ^ ")" | ASharedLoan (loans, v, av) -> let loans = BorrowId.Set.to_string None loans in "@shared_loan(" ^ loans ^ ", " @@ -225,10 +229,10 @@ module Values = struct = match bc with | AMutBorrow (bid, av) -> - "&mut@" ^ BorrowId.to_string bid ^ " (" + "mb@" ^ BorrowId.to_string bid ^ " (" ^ typed_avalue_to_string env av ^ ")" - | ASharedBorrow bid -> "⌊shared@" ^ BorrowId.to_string bid ^ "⌋" + | ASharedBorrow bid -> "sb@" ^ BorrowId.to_string bid | AIgnoredMutBorrow (opt_bid, av) -> "@ignored_mut_borrow(" ^ option_to_string BorrowId.to_string opt_bid |