summaryrefslogtreecommitdiff
path: root/src/Print.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-21 10:16:56 +0100
committerSon Ho2022-01-21 10:16:56 +0100
commit67c48a5b989323d9e1ba79ff257cb113736b7ef3 (patch)
treec3fc226856a9b6cd3d310e2741a7b48c79f557b0 /src/Print.ml
parent4c25aa1864a4b72ffea7b641b4473029b46b4216 (diff)
Update AProjLoans and AEndedProjLoans to take a list of given back
values
Diffstat (limited to '')
-rw-r--r--src/Print.ml23
1 files changed, 17 insertions, 6 deletions
diff --git a/src/Print.ml b/src/Print.ml
index 6c39366c..024d835d 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -309,14 +309,25 @@ module Values = struct
let rec aproj_to_string (fmt : value_formatter) (pv : V.aproj) : string =
match pv with
- | AProjLoans sv ->
- "[" ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv ^ "]"
+ | AProjLoans (sv, given_back) ->
+ let given_back =
+ if given_back = [] then ""
+ else
+ let given_back = List.map snd given_back in
+ let given_back = List.map (aproj_to_string fmt) given_back in
+ " (" ^ String.concat "," given_back ^ ") "
+ in
+ "["
+ ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv
+ ^ given_back ^ "]"
| AProjBorrows (sv, rty) ->
"(" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"
- | AEndedProjLoans (_mv, aproj_opt) -> (
- match aproj_opt with
- | None -> "_"
- | Some aproj -> aproj_to_string fmt aproj)
+ | AEndedProjLoans given_back ->
+ if given_back = [] then "_"
+ else
+ let given_back = List.map snd given_back in
+ let given_back = List.map (aproj_to_string fmt) given_back in
+ "ended_aproj_loans (" ^ String.concat "," given_back ^ ")"
| AEndedProjBorrows _mv -> "_"
| AIgnoredProjBorrows -> "_"