summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-22 09:43:23 +0100
committerSon Ho2021-11-22 09:43:23 +0100
commit6d21462223fe26a92ee565deb56e48670a74f16a (patch)
tree8c8637b8eb213cc559cb6c54ba9899f293ebf180
parent5f3983a77fde2ccd7005cd72f373a4b75b01440f (diff)
Finish the function typed_value_to_string
Diffstat (limited to '')
-rw-r--r--src/Print.ml28
1 files changed, 26 insertions, 2 deletions
diff --git a/src/Print.ml b/src/Print.ml
index 2ae88836..1ad2f5cb 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -248,8 +248,32 @@ module Values = struct
| Bottom -> "⊥"
| Assumed av -> (
match av with Box bv -> "@Box(" ^ typed_value_to_string fmt bv ^ ")")
- | Borrow bc -> "" (* TODO *)
- | Loan lc -> "" (* TODO *)
+ | Borrow bc -> borrow_content_to_string fmt bc
+ | Loan lc -> loan_content_to_string fmt lc
| Symbolic sp ->
symbolic_proj_comp_to_string (value_to_rtype_formatter fmt) sp
+
+ and borrow_content_to_string (fmt : value_formatter) (bc : borrow_content) :
+ string =
+ match bc with
+ | SharedBorrow bid -> "⌊shared@" ^ BorrowId.to_string bid ^ "⌋"
+ | MutBorrow (bid, tv) ->
+ "&mut@" ^ BorrowId.to_string bid ^ " ("
+ ^ typed_value_to_string fmt tv
+ ^ ")"
+ | InactivatedMutBorrow bid ->
+ "⌊inactivated_mut@" ^ BorrowId.to_string bid ^ "⌋"
+
+ and loan_content_to_string (fmt : value_formatter) (lc : loan_content) :
+ string =
+ match lc with
+ | SharedLoan (loans, v) ->
+ let loans =
+ BorrowId.Set.fold
+ (fun lid loans -> BorrowId.to_string lid :: loans)
+ loans []
+ in
+ let loans = String.concat ", " (List.rev loans) in
+ "@shared_loan({" ^ loans ^ "}, " ^ typed_value_to_string fmt v ^ ")"
+ | MutLoan bid -> "⌊mut@" ^ BorrowId.to_string bid ^ "⌋"
end