From 3a94d620b1c135342c9f88ae943f256b9a9f96c9 Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Mon, 30 Dec 2019 21:51:40 +0000
Subject: [PATCH] Implement -d (debug) option.

---
 src/cmdline.ml  | 15 +++++++++++++--
 src/cmdline.mli |  7 +++++++
 src/eval.ml     |  8 ++++++++
 src/main.ml     |  3 ++-
 4 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/src/cmdline.ml b/src/cmdline.ml
index b7063af..cc20d76 100644
--- a/src/cmdline.ml
+++ b/src/cmdline.ml
@@ -49,8 +49,10 @@ let () =
     failwithf "%s: cannot find the standard library directory, expected %s.  If the standard library directory is in a non-standard location then set GOALS_DATADIR.  If you can trying to run goals from the build directory then use ‘./run goals ...’"
       Sys.executable_name stdlibdir
 
-let input_file, directory, includes, use_prelude, anon_vars, targets =
+let input_file,
+    debug_flag, directory, includes, use_prelude, anon_vars, targets =
   let args = ref [] in
+  let debug_flag = ref false in
   let directory = ref "." in
   let input_file = ref "Goalfile" in
   let includes = ref [stdlibdir] in
@@ -60,6 +62,8 @@ let input_file, directory, includes, use_prelude, anon_vars, targets =
   let argspec = [
     "-C",          Arg.Set_string directory,
                    "directory Change to directory before running";
+    "-d",          Arg.Set debug_flag,
+                   " Print debug information.";
     "--directory", Arg.Set_string directory,
                    "directory Change to directory before running";
     "-f",          Arg.Set_string input_file,
@@ -82,6 +86,7 @@ let input_file, directory, includes, use_prelude, anon_vars, targets =
   Arg.parse argspec anon_fun usage;
 
   let args = List.rev !args in
+  let debug_flag = !debug_flag in
   let directory = !directory in
   let input_file = absolute_path !input_file in
   (* Don't reverse includes - we want newer -I options to take precedence. *)
@@ -102,4 +107,10 @@ let input_file, directory, includes, use_prelude, anon_vars, targets =
         (name, expr)
     ) anon_vars in
 
-  input_file, directory, includes, use_prelude, anon_vars, targets
+  input_file,
+  debug_flag, directory, includes, use_prelude, anon_vars, targets
+
+(* Create the debug function. *)
+let debug fs =
+  let display str = if debug_flag then prerr_endline str in
+  ksprintf display fs
diff --git a/src/cmdline.mli b/src/cmdline.mli
index e9ab8f1..cb6265d 100644
--- a/src/cmdline.mli
+++ b/src/cmdline.mli
@@ -27,6 +27,13 @@ val input_file : string
 (** Get the name of the input Goalfile.
     This is an absolute path. *)
 
+val debug : ('a, unit, string, unit) format4 -> 'a
+(** If debugging is enabled (-d option) then print the formatted
+    output.  If debugging was not enabled then nothing is printed. *)
+
+val debug_flag : bool
+(** If debugging is enabled. *)
+
 val directory : string
 (** Get the name of working directory (-C option). *)
 
diff --git a/src/eval.ml b/src/eval.ml
index 27aa971..66b0164 100644
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -59,6 +59,9 @@ and evaluate_target env = function
 
 (* Run a goal by name. *)
 and run_goal env loc name args (params, patterns, deps, code) =
+  Cmdline.debug "%a: running goal %s %a"
+    Ast.string_loc loc name Ast.string_expr (Ast.EList (Ast.noloc, args));
+
   (* Create a new environment which maps the parameter names to
    * the args.
    *)
@@ -118,6 +121,9 @@ and run_goal env loc name args (params, patterns, deps, code) =
 
 (* Return whether the target (pattern) needs to be rebuilt. *)
 and needs_rebuild env loc deps pattern =
+  Cmdline.debug "%a: testing if %a needs rebuild"
+    Ast.string_loc loc Ast.string_pattern pattern;
+
   match pattern with
   | Ast.PTactic (loc, tactic, targs) ->
      (* Look up the tactic. *)
@@ -163,6 +169,8 @@ and needs_rebuild env loc deps pattern =
  * cargs is a list of parameters (all constants).
  *)
 and run_tactic env loc tactic cargs =
+  Cmdline.debug "%a: running tactic %s" Ast.string_loc loc tactic;
+
   (* Find all goals in the environment.  Returns a list of (name, goal). *)
   let goals =
     let env = Ast.Env.bindings env in
diff --git a/src/main.ml b/src/main.ml
index 127c24c..6546fd5 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -49,7 +49,8 @@ let main () =
     if targets <> [] then targets
     else [Ast.ECallGoal (Ast.noloc, "all", [])] in
 
-  Ast.print_env stderr env;
+  if Cmdline.debug_flag then
+    Ast.print_env stderr env;
 
   (* Evaluate the target expressions in turn. *)
   Eval.evaluate_targets env targets
-- 
1.8.3.1