Implement -d (debug) option.

diff --git a/src/cmdline.ml b/src/cmdline.ml
index b7063af..cc20d76 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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