Improve formatting

3 files changed, 11 insertions, 8 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index a49b2f3f..38da6c25 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2146,7 +2146,7 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
   L.log#ldebug
     (lazy
       ("\n" ^ eval_ctx_to_string ctx ^ "\nAbout to evaluate statement: "
-     ^ statement_to_string ctx st));
+     ^ statement_to_string ctx st ^ "\n"));
   (* Evaluate *)
   match st with
   | A.Assign (p, rvalue) -> (
@@ -2275,7 +2275,7 @@ and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) :
   L.log#ldebug
     (lazy
       ("\n" ^ eval_ctx_to_string ctx ^ "\nAbout to evaluate expression: \n"
-     ^ expression_to_string ctx e));
+     ^ expression_to_string ctx e ^ "\n"));
   (* Evaluate *)
   match e with
   | A.Statement st -> eval_statement config ctx st
diff --git a/src/Print.ml b/src/Print.ml
index b9d7372c..9cdde188 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -213,6 +213,7 @@ module Values = struct
 
   let rec typed_value_to_string (fmt : value_formatter) (v : V.typed_value) :
       string =
+    let ety_fmt = value_to_etype_formatter fmt in
     match v.value with
     | Concrete cv -> constant_value_to_string cv
     | Adt av ->
@@ -244,7 +245,7 @@ module Values = struct
           String.concat ", " (List.map (typed_value_to_string fmt) values)
         in
         "(" ^ values ^ ")"
-    | Bottom -> "⊥"
+    | Bottom -> "⊥ : " ^ PT.ety_to_string ety_fmt v.ty
     | Assumed av -> (
         match av with Box bv -> "@Box(" ^ typed_value_to_string fmt bv ^ ")")
     | Borrow bc -> borrow_content_to_string fmt bc
@@ -292,6 +293,7 @@ module Values = struct
 
   let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) :
       string =
+    let rty_fmt = value_to_rtype_formatter fmt in
     match v.avalue with
     | AConcrete cv -> constant_value_to_string cv
     | AAdt av ->
@@ -314,7 +316,7 @@ module Values = struct
           String.concat ", " (List.map (typed_avalue_to_string fmt) values)
         in
         "(" ^ values ^ ")"
-    | ABottom -> "⊥"
+    | ABottom -> "⊥ : " ^ PT.rty_to_string rty_fmt v.aty
     | ALoan lc -> aloan_content_to_string fmt lc
     | ABorrow bc -> aborrow_content_to_string fmt bc
     | AAssumed av -> (
@@ -408,13 +410,13 @@ module Contexts = struct
       =
     match ev with
     | Var (var, tv) ->
-        PV.var_to_string var ^ " -> " ^ PV.typed_value_to_string fmt tv
+        PV.var_to_string var ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
     | Abs abs -> PV.abs_to_string fmt abs
     | Frame -> failwith "Can't print a Frame element"
 
   let env_to_string (fmt : PV.value_formatter) (env : C.env) : string =
     "{\n"
-    ^ String.concat ";\n"
+    ^ String.concat "\n"
         (List.map (fun ev -> "  " ^ env_value_to_string fmt ev) env)
     ^ "\n}"
 
@@ -477,7 +479,8 @@ module Contexts = struct
   let split_env_according_to_frames (env : C.env) : C.env list =
     let rec split_aux (frames : C.env list) (curr_frame : C.env) (env : C.env) =
       match env with
-      | [] -> frames
+      | [] ->
+          if List.length curr_frame > 0 then curr_frame :: frames else frames
       | Frame :: env' -> split_aux (curr_frame :: frames) [] env'
       | ev :: env' -> split_aux frames (ev :: curr_frame) env'
     in
diff --git a/src/main.ml b/src/main.ml
index 39f1cf0c..36b5dd71 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -15,7 +15,7 @@ let () =
   | Error s -> log#error "error: %s\n" s
   | Ok m ->
       (* Print the module *)
-      log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m));
+      log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
 
       (* Test the unit functions *)
       I.test_all_unit_functions m.types m.functions