From cc7daed14342b746825eb3a72c00d58ab0d9fb73 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 13 Feb 2024 00:27:02 +0100
Subject: Update Print.ml

---
 compiler/Print.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'compiler/Print.ml')

diff --git a/compiler/Print.ml b/compiler/Print.ml
index 8999c77d..8658a7d5 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -88,19 +88,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 +184,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 +225,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
-- 
cgit v1.2.3


From cd99485fa2493697b2b3775a5cae80bf9bf58a99 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 19:33:08 +0100
Subject: Make progress on fixing the loops

---
 compiler/Print.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'compiler/Print.ml')

diff --git a/compiler/Print.ml b/compiler/Print.ml
index 8658a7d5..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 *)
-- 
cgit v1.2.3