Start working logging and make progress on printing ASTs

9 files changed, 188 insertions, 12 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
index f13043d0..b18cfe22 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -1,8 +1,6 @@
 open Types
 open Values
-open Expressions
 open CfimAst
-open Errors
 
 (** Environment value: mapping from variable to value, abstraction (only
     used in symbolic mode) or stack frame delimiter.
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 8072b316..b858360d 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -1,5 +1,3 @@
-open Errors
-
 (** Signature for a module describing an identifier.
     
     We often need identifiers (for definitions, variables, etc.) and in
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 07c43c10..47b389a3 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -6,6 +6,7 @@ open Errors
 module C = Contexts
 module Subst = Substitute
 module A = CfimAst
+module L = Logging
 
 (* TODO: Change state-passing style to : st -> ... -> (st, v) *)
 (* TODO: check that the value types are correct when evaluating *)
diff --git a/src/Logging.ml b/src/Logging.ml
new file mode 100644
index 00000000..b1512af7
--- /dev/null
+++ b/src/Logging.ml
@@ -0,0 +1,3 @@
+let _ = Easy_logging.Logging.make_logger "MainLogger" Debug [ Cli Debug ]
+
+let log = Easy_logging.Logging.get_logger "MainLogger"
diff --git a/src/Print.ml b/src/Print.ml
index 8d3e8745..9c9a7a5b 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -1,5 +1,8 @@
-open Errors
+(* TODO: use one letter abbreviations for modules *)
+
 open Identifiers
+module T = Types
+module V = Values
 
 open Types
 (** Pretty-printing for types *)
@@ -73,7 +76,8 @@ module Types = struct
         let params = params_to_string fmt regions tys in
         match aty with Box -> "std::boxed::Box" ^ params)
 
-  and params_to_string fmt (regions : 'r list) (types : 'r ty list) : string =
+  and params_to_string (fmt : 'r type_formatter) (regions : 'r list)
+      (types : 'r ty list) : string =
     if List.length regions + List.length types > 0 then
       let regions = List.map fmt.r_to_string regions in
       let types = List.map (ty_to_string fmt) types in
@@ -145,6 +149,7 @@ end
 (** Pretty-printing for values *)
 
 open Values
+module PT = Types (* local module *)
 
 module Values = struct
   open Types (* local module *)
@@ -159,7 +164,7 @@ module Values = struct
 
   let value_to_etype_formatter (fmt : value_formatter) : etype_formatter =
     {
-      Types.r_to_string = erased_region_to_string;
+      Types.r_to_string = PT.erased_region_to_string;
       Types.type_var_id_to_string = fmt.type_var_id_to_string;
       Types.type_def_id_to_string = fmt.type_def_id_to_string;
     }
@@ -465,3 +470,171 @@ module Contexts = struct
     in
     "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames
 end
+
+module E = Expressions
+module A = CfimAst
+
+module CfimAst = struct
+  module PV = Values
+  module PC = Contexts
+  module PT = Types
+
+  type ast_formatter = {
+    r_to_string : RegionVarId.id -> string;
+    type_var_id_to_string : TypeVarId.id -> string;
+    type_def_id_to_string : TypeDefId.id -> string;
+    (* TODO: rename to something like adt_variant_to_string *)
+    type_def_id_variant_id_to_string : TypeDefId.id -> VariantId.id -> string;
+    adt_field_to_string :
+      TypeDefId.id -> VariantId.id option -> FieldId.id -> string;
+    var_id_to_string : VarId.id -> string;
+    fun_def_id_to_string : A.FunDefId.id -> string;
+  }
+
+  let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter =
+    {
+      PV.r_to_string = fmt.r_to_string;
+      PV.type_var_id_to_string = fmt.type_var_id_to_string;
+      PV.type_def_id_to_string = fmt.type_def_id_to_string;
+      PV.type_def_id_variant_id_to_string = fmt.type_def_id_variant_id_to_string;
+      PV.var_id_to_string = fmt.var_id_to_string;
+    }
+
+  let ast_to_etype_formatter (fmt : ast_formatter) : PT.etype_formatter =
+    {
+      PT.r_to_string = PT.erased_region_to_string;
+      PT.type_var_id_to_string = fmt.type_var_id_to_string;
+      PT.type_def_id_to_string = fmt.type_def_id_to_string;
+    }
+
+  let rec projection_to_string (fmt : ast_formatter) (inside : string)
+      (p : E.projection) : string =
+    match p with
+    | [] -> inside
+    | pe :: p' -> (
+        let s = projection_to_string fmt inside p' in
+        match pe with
+        | E.Deref -> "*(" ^ s ^ ")"
+        | E.DerefBox -> "deref_box(" ^ s ^ ")"
+        | E.Field (E.ProjTuple _, fid) -> "(" ^ s ^ ")." ^ FieldId.to_string fid
+        | E.Field (E.ProjAdt (adt_id, opt_variant_id), fid) -> (
+            let field_name =
+              fmt.adt_field_to_string adt_id opt_variant_id fid
+            in
+            match opt_variant_id with
+            | None -> "(" ^ s ^ ")." ^ field_name
+            | Some variant_id ->
+                let variant_name =
+                  fmt.type_def_id_variant_id_to_string adt_id variant_id
+                in
+                "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name))
+
+  let place_to_string (fmt : ast_formatter) (p : E.place) : string =
+    let var = fmt.var_id_to_string p.E.var_id in
+    projection_to_string fmt var p.E.projection
+
+  let unop_to_string (unop : E.unop) : string =
+    match unop with E.Not -> "¬" | E.Neg -> "-"
+
+  let binop_to_string (binop : E.binop) : string =
+    match binop with
+    | E.BitXor -> "^"
+    | E.BitAnd -> "&"
+    | E.BitOr -> "|"
+    | E.Eq -> "=="
+    | E.Lt -> "<"
+    | E.Le -> "<="
+    | E.Ne -> "!="
+    | E.Ge -> ">="
+    | E.Gt -> ">"
+    | E.Div -> "/"
+    | E.Rem -> "%"
+    | E.Add -> "+"
+    | E.Sub -> "-"
+    | E.Mul -> "*"
+    | E.Shl -> "<<"
+    | E.Shr -> ">>"
+
+  let operand_constant_value_to_string (fmt : ast_formatter)
+      (cv : E.operand_constant_value) : string =
+    match cv with
+    | E.ConstantValue cv -> PV.constant_value_to_string cv
+    | E.ConstantAdt def_id -> fmt.type_def_id_to_string def_id
+    | E.Unit -> "()"
+
+  let operand_to_string (fmt : ast_formatter) (op : E.operand) : string =
+    match op with
+    | E.Copy p -> "copy " ^ place_to_string fmt p
+    | E.Move p -> "move " ^ place_to_string fmt p
+    | E.Constant (_ty, cv) -> operand_constant_value_to_string fmt cv
+
+  let rvalue_to_string (fmt : ast_formatter) (rv : E.rvalue) : string =
+    match rv with
+    | E.Use op -> operand_to_string fmt op
+    | E.Ref (p, bk) -> (
+        let p = place_to_string fmt p in
+        match bk with
+        | E.Shared -> "&" ^ p
+        | E.Mut -> "&mut " ^ p
+        | E.TwoPhaseMut -> "&two-phase " ^ p)
+    | E.UnaryOp (unop, op) ->
+        unop_to_string unop ^ " " ^ operand_to_string fmt op
+    | E.BinaryOp (binop, op1, op2) ->
+        operand_to_string fmt op1 ^ " " ^ binop_to_string binop ^ " "
+        ^ operand_to_string fmt op2
+    | E.Discriminant p -> "discriminant(" ^ place_to_string fmt p ^ ")"
+    | E.Aggregate (akind, ops) -> (
+        let ops = List.map (operand_to_string fmt) ops in
+        match akind with
+        | E.AggregatedTuple -> "(" ^ String.concat ", " ops ^ ")"
+        | E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) -> (
+            let adt_name = fmt.type_def_id_to_string def_id in
+            match opt_variant_id with
+            | None -> adt_name ^ "{ " ^ String.concat ", " ops ^ " }"
+            | Some variant_id ->
+                let variant_name =
+                  fmt.type_def_id_variant_id_to_string def_id variant_id
+                in
+                adt_name ^ "::" ^ variant_name ^ "(" ^ String.concat ", " ops
+                ^ ")"))
+
+  let statement_to_string (fmt : ast_formatter) (st : A.statement) : string =
+    match st with
+    | A.Assign (p, rv) ->
+        place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
+    | A.FakeRead p -> "fake_read " ^ place_to_string fmt p
+    | A.SetDiscriminant (p, variant_id) ->
+        (* TODO: improve this to lookup the variant name by using the def id *)
+        "set_discriminant(" ^ place_to_string fmt p ^ ", "
+        ^ T.VariantId.to_string variant_id
+        ^ ")"
+    | A.Drop p -> "drop(" ^ place_to_string fmt p ^ ")"
+    | A.Assert a ->
+        let cond = operand_to_string fmt a.A.cond in
+        if a.A.expected then "assert(" ^ cond ^ ")"
+        else "assert(¬" ^ cond ^ ")"
+    | A.Call call -> (
+        let ty_fmt = ast_to_etype_formatter fmt in
+        let params =
+          if List.length call.A.type_params > 0 then
+            "<"
+            ^ String.concat ","
+                (List.map (PT.ty_to_string ty_fmt) call.A.type_params)
+            ^ ">"
+          else ""
+        in
+        match call.A.func with
+        | A.Local fid -> fmt.fun_def_id_to_string fid ^ params
+        | A.Assumed fid -> (
+            match fid with
+            | A.BoxNew -> "alloc::boxed::Box" ^ params ^ "::new"
+            | A.BoxDeref -> "core::ops::deref::Deref<Box" ^ params ^ ">::deref"
+            | A.BoxDerefMut ->
+                "core::ops::deref::DerefMut<Box" ^ params ^ ">::deref_mut"
+            | A.BoxFree -> "alloc::alloc::box_free<" ^ params ^ ">"))
+    | A.Panic -> "panic"
+    | A.Return -> "return"
+    | A.Break i -> "break " ^ string_of_int i
+    | A.Continue i -> "continue " ^ string_of_int i
+    | A.Nop -> "nop"
+end
diff --git a/src/Substitute.ml b/src/Substitute.ml
index dc2821f0..8cb92587 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -36,7 +36,7 @@ let rec ty_substitute (rsubst : 'r1 -> 'r2)
 (** Erase the regions in a type and substitute the type variables *)
 let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
     (ty : T.rty) : T.ety =
-  let rsubst (r : T.RegionVarId.id T.region) : T.erased_region = T.Erased in
+  let rsubst (_ : T.RegionVarId.id T.region) : T.erased_region = T.Erased in
   ty_substitute rsubst tsubst ty
 
 (** Create a type substitution from a list of type variable ids and a list of
diff --git a/src/Types.ml b/src/Types.ml
index 6f979718..abcd0e28 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -99,7 +99,10 @@ type type_def = {
   kind : type_def_kind;
 }
 
-(** Convert an [rty] to an [ety] by erasing the region variables *)
+(** Convert an [rty] to an [ety] by erasing the region variables
+    
+    TODO: this can be done through a substitution
+*)
 let rec erase_regions (ty : rty) : ety =
   match ty with
   | Adt (def_id, regions, tys) ->
@@ -115,7 +118,7 @@ let rec erase_regions (ty : rty) : ety =
   | Str -> Str
   | Array ty -> Array (erase_regions ty)
   | Slice ty -> Slice (erase_regions ty)
-  | Ref (r, ty, ref_kind) -> Ref (Erased, erase_regions ty, ref_kind)
+  | Ref (_, ty, ref_kind) -> Ref (Erased, erase_regions ty, ref_kind)
   | Assumed (aty, regions, tys) ->
       let regions = List.map (fun _ -> Erased) regions in
       let tys = List.map erase_regions tys in
diff --git a/src/dune b/src/dune
index eb2966f4..c565d9fa 100644
--- a/src/dune
+++ b/src/dune
@@ -1,6 +1,6 @@
 (executable
  (name main)
- (libraries yojson zarith))
+ (libraries yojson zarith easy_logging))
 
 (env
   (dev (flags
diff --git a/src/main.ml b/src/main.ml
index 4fb91cea..8c05c33b 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,5 +1,5 @@
 open CfimOfJson
-open Interpreter
+open Logging
 open Print
 
 (* This is necessary to have a backtrace when raising exceptions - for some