Made pretty printing without logs for dcalc

compiler/dcalc/interpreter.ml

@@ -229,7 +229,7 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
                    | Ast.EAbs _ -> Cli.print_with_style [ ANSITerminal.green ] "<function>"
                    | _ ->
                        let expr_str =
-                         Format.asprintf "%a" (Print.format_expr ctx) (e', Pos.no_pos)
+                         Format.asprintf "%a" (Print.format_expr ctx ~debug:false) (e', Pos.no_pos)
                        in
                        let expr_str =
                          Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
@@ -268,7 +268,9 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
           @ List.mapi
               (fun i arg ->
                 ( Some
-                    (Format.asprintf "Argument n°%d, value %a" (i + 1) (Print.format_expr ctx) arg),
+                    (Format.asprintf "Argument n°%d, value %a" (i + 1)
+                       (Print.format_expr ctx ~debug:true)
+                       arg),
                   Pos.get_position arg ))
               args))
     op
@@ -331,7 +333,8 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
             (Format.asprintf
                "The expression %a should be a tuple with %d components but is not (should not \
                 happen if the term was well-typed)"
-               (Print.format_expr ctx) e n)
+               (Print.format_expr ctx ~debug:true)
+               e n)
             (Pos.get_position e1))
   | EInj (e1, n, en, ts) ->
       let e1' = evaluate_expr ctx e1 in
@@ -415,8 +418,11 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
           match Pos.unmark e' with
           | EApp ((Ast.EOp (Binop op), pos_op), [ ((ELit _, _) as e1); ((ELit _, _) as e2) ]) ->
               Errors.raise_spanned_error
-                (Format.asprintf "Assertion failed: %a %a %a" (Print.format_expr ctx) e1
+                (Format.asprintf "Assertion failed: %a %a %a"
-                   Print.format_binop (op, pos_op) (Print.format_expr ctx) e2)
+                   (Print.format_expr ctx ~debug:false)
+                   e1 Print.format_binop (op, pos_op)
+                   (Print.format_expr ctx ~debug:false)
+                   e2)
                 (Pos.get_position e')
           | _ ->
               Errors.raise_spanned_error (Format.asprintf "Assertion failed") (Pos.get_position e'))

compiler/dcalc/print.ml

@@ -166,8 +166,9 @@ let needs_parens (e : expr Pos.marked) : bool =
 let format_var (fmt : Format.formatter) (v : Var.t) : unit =
   Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
 
-let rec format_expr (ctx : Ast.decl_ctx) (fmt : Format.formatter) (e : expr Pos.marked) : unit =
+let rec format_expr ?(debug : bool = false) (ctx : Ast.decl_ctx) (fmt : Format.formatter)
-  let format_expr = format_expr ctx in
+    (e : expr Pos.marked) : unit =
+  let format_expr = format_expr ~debug ctx in
   let format_with_parens (fmt : Format.formatter) (e : expr Pos.marked) =
     if needs_parens e then
       Format.fprintf fmt "%a%a%a" format_punctuation "(" format_expr e format_punctuation ")"
@@ -250,6 +251,7 @@ let rec format_expr (ctx : Ast.decl_ctx) (fmt : Format.formatter) (e : expr Pos.
   | EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
       Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1 format_binop
         (op, Pos.no_pos) format_with_parens arg2
+  | EApp ((EOp (Unop (Log _)), _), [ arg1 ]) when not debug -> format_expr fmt arg1
   | EApp ((EOp (Unop op), _), [ arg1 ]) ->
       Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_unop (op, Pos.no_pos) format_with_parens arg1
   | EApp (f, args) ->
@@ -278,6 +280,7 @@ let rec format_expr (ctx : Ast.decl_ctx) (fmt : Format.formatter) (e : expr Pos.
       Format.fprintf fmt "@[<hov 2>%a@ %a%a%a@]" format_keyword "assert" format_punctuation "("
         format_expr e' format_punctuation ")"
 
-let format_scope (ctx : decl_ctx) (fmt : Format.formatter) ((n, s) : Ast.ScopeName.t * scope_body) =
+let format_scope ?(debug : bool = false) (ctx : decl_ctx) (fmt : Format.formatter)
-  Format.fprintf fmt "@[<hov 2>let %a =@ %a@]" Ast.ScopeName.format_t n (format_expr ctx)
+    ((n, s) : Ast.ScopeName.t * scope_body) =
+  Format.fprintf fmt "@[<hov 2>let %a =@ %a@]" Ast.ScopeName.format_t n (format_expr ctx ~debug)
     (Bindlib.unbox (Ast.build_whole_scope_expr ctx s (Pos.get_position (Ast.ScopeName.get_info n))))

compiler/dcalc/print.mli

@@ -42,6 +42,16 @@ val format_unop : Format.formatter -> Ast.unop Pos.marked -> unit
 
 val format_var : Format.formatter -> Ast.Var.t -> unit
 
-val format_expr : Ast.decl_ctx -> Format.formatter -> Ast.expr Pos.marked -> unit
+val format_expr :
+  ?debug:bool (** [true] for debug printing *) ->
+  Ast.decl_ctx ->
+  Format.formatter ->
+  Ast.expr Pos.marked ->
+  unit
 
-val format_scope : Ast.decl_ctx -> Format.formatter -> Ast.ScopeName.t * Ast.scope_body -> unit
+val format_scope :
+  ?debug:bool (** [true] for debug printing *) ->
+  Ast.decl_ctx ->
+  Format.formatter ->
+  Ast.ScopeName.t * Ast.scope_body ->
+  unit