diff options
author | Son Ho | 2022-01-21 10:16:56 +0100 |
---|---|---|
committer | Son Ho | 2022-01-21 10:16:56 +0100 |
commit | 67c48a5b989323d9e1ba79ff257cb113736b7ef3 (patch) | |
tree | c3fc226856a9b6cd3d310e2741a7b48c79f557b0 /src/Print.ml | |
parent | 4c25aa1864a4b72ffea7b641b4473029b46b4216 (diff) |
Update AProjLoans and AEndedProjLoans to take a list of given back
values
Diffstat (limited to '')
-rw-r--r-- | src/Print.ml | 23 |
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 -> "_" |