DECLARE PLUGIN "coq-quickchick.plugin"

{
open Pp
open Names
open Declare
open Libnames
open Util
open Constrintern
open Constrexpr
open Error
open Stdarg

let mk_ref s = CAst.make @@ CRef (qualid_of_string s, None)

(* Names corresponding to QuickChick's .v files *)
let show = mk_ref "QuickChick.Show.show"
let quickCheck = mk_ref "QuickChick.Test.quickCheck"
let quickCheckWith = mk_ref "QuickChick.Test.quickCheckWith"
let mutateCheck = mk_ref "QuickChick.MutateCheck.mutateCheck"
let mutateCheckWith = mk_ref "QuickChick.MutateCheck.mutateCheckWith"
let mutateCheckMany = mk_ref "QuickChick.MutateCheck.mutateCheckMany"
let mutateCheckManyWith = mk_ref "QuickChick.MutateCheck.mutateCheckManyWith"
let sample = mk_ref "QuickChick.Generators.sampleGen"
let sample1 = mk_ref "QuickChick.Generators.sample1"

(* Handle extra ocaml directory to be copied *)
let empty_slist : string list = []           
let extra_dir : string list ref =
  Summary.ref ~name:"QC_ocaml_dir" empty_slist
let add_extra_dir s = extra_dir := s :: !extra_dir

let extra_pkg : string list ref =
  Summary.ref ~name:"QC_ocaml_pkg" ["zarith"]
let add_extra_pkg s = extra_pkg := s :: !extra_pkg

let extract_dir : string option ref =
  Summary.ref ~name:"QC_extract_dir" None
let set_extract_dir s = extract_dir := Some s

let dune_file : string option ref =
  Summary.ref ~name:"QC_dune_file" None
let set_dune_file s = dune_file := Some s

let modules_to_open : string list ref =
  Summary.ref ~name:"QC_modules_to_open" empty_slist
let add_module_to_open s = modules_to_open := s :: !modules_to_open  

(* [mkdir -p]: recursively make the parent directories if they do not exist. *)
let rec mkdir_ dname =
  let cmd () = Unix.mkdir dname 0o755 in
  try cmd () with
  | Unix.Unix_error (Unix.EEXIST, _, _) -> ()
  | Unix.Unix_error (Unix.ENOENT, _, _) ->
    (* If the parent directory doesn't exist, try making it first. *)
    mkdir_ (Filename.dirname dname);
    cmd ()

(* Interface with OCaml compiler *)
let temp_dirname () =
  match !extract_dir with
  | None -> 
    let dname = Filename.(concat (get_temp_dir_name ()) "QuickChick") in
    mkdir_ dname;
    dname
  | Some s ->
    mkdir_ s;
    s

(* Rewrite a file line by line *)
let sed_file file f =
  let src = open_in file in
  let tmpfile = file ^ ".tmp" in
  let tmp = open_out tmpfile in
  let rec go () =
    match input_line src with
    | line -> output_string tmp (f line); output_char tmp '\n'; go ()
    | exception End_of_file ->
        close_in src;
        close_out tmp;
        Sys.rename tmpfile file
  in go ()

let read_all chan =
  let buf = Buffer.create 1024 in
  let rec go () =
    match Buffer.add_channel buf chan 1024 with
    | () -> go ()
    | exception End_of_file -> Buffer.contents buf
  in go ()

let read_file file =
  let h = open_in file in
  let s = read_all h in
  close_in h;
  s

let fresh_name n =
    let base = Id.of_string n in

    (* [is_visible_name id] returns [true] if [id] is already used on
       the Coq side. *)
    let is_visible_name id =
      try
        ignore (Nametab.locate (Libnames.qualid_of_ident id));
        true
      with Not_found -> false
    in
    (* Safe fresh name generation. *)
    Namegen.next_ident_away_from base is_visible_name

(** [define c] introduces a fresh constant name for the term [c]. *)
let define c env evd =
  let (evd,_) = Typing.type_of env evd c in
  let univs = Evd.univ_entry ~poly:true evd in
  let fn = fresh_name "quickchick" in
  (* TODO: Maxime - which of the new internal flags should be used here? The names aren't as clear :) *)
  let _ : Constant.t = declare_constant ~name:fn ~kind:Decls.(IsDefinition Definition)
      (DefinitionEntry (definition_entry ~univs (EConstr.to_constr ~abort_on_undefined_evars:false evd c))) in
  fn

(* [$TMP/QuickChick/$TIME/QuickChick.ml],
   where [$TIME] is the current time in format [HHMMSS]. *)
let new_ml_file () : string =
  let tm = Unix.localtime (Unix.time ()) in
  let ts = Printf.sprintf "%02d%02d%02d_" tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec in
  let base_tmp_dir = temp_dirname () in
  let temp_dir = CUnix.mktemp_dir ~temp_dir:base_tmp_dir ts "" in
  mkdir_ temp_dir;
  Filename.temp_file ~temp_dir "QuickChick" ".ml"

let tmp_int_re = Str.regexp "type int =[ ]*int"

#if COQ_VERSION >= (8, 20, 0)
let define_and_run ~opaque_access c env evd =
#else
let define_and_run c env evd =
#endif
  (* Extract the term and its dependencies *)
  let main = define c env evd in
  let mlf   : string = new_ml_file () in
  let execn : string = Filename.chop_extension mlf ^ ".native" in
  let mlif  : string = Filename.chop_extension mlf ^ ".mli"    in
  let dir   : string = Filename.dirname mlf in
  let warnings = CWarnings.get_flags () in
  let mute_extraction = warnings ^ (if warnings = "" then "" else ",") ^ "-extraction-opaque-accessed" in
  CWarnings.set_flags mute_extraction;
#if COQ_VERSION >= (8, 20, 0)
  Flags.silently (Extraction_plugin.Extract_env.full_extraction ~opaque_access (Some mlf)) [qualid_of_ident main];
#else
  Flags.silently (Extraction_plugin.Extract_env.full_extraction (Some mlf)) [qualid_of_ident main];
#endif
  CWarnings.set_flags warnings;
  (* Add a main function to get some output *)
  let oc = open_out_gen [Open_append;Open_text] 0o666 mlf in
  let for_output =
    "\nlet _ = print_string (\n" ^
    "let l = (" ^ (Id.to_string main) ^ ") in\n"^
    "let s = Bytes.create (List.length l) in\n" ^
    "let rec copy i = function\n" ^
    "| [] -> s\n" ^
    "| c :: l -> Bytes.set s i c; copy (i+1) l\n" ^
    "in Bytes.to_string (copy 0 l))" in
  Printf.fprintf oc "%s" for_output;
  close_out oc;

  (* Add any modules that have been marked "open" *)
  let open_cmd s = Printf.sprintf "awk -v n=1 -v s=\"open %s\" 'NR == n {print s} {print}' %s > %s/__qc_tmp && mv %s/__qc_tmp %s" s mlf dir dir mlf in
  List.iter (fun s -> ignore (Sys.command (open_cmd s))) !modules_to_open;
  
  (* Before compiling, fix stupid cyclic dependencies like "type int = int".
     Introduced by "Definition int := int." possibly inside a module, so just
     removing it might break other definitions that depend on it.
     TODO: Generalize (.) \g1\b or something *)
  sed_file mlf (fun line ->
    if Str.string_match tmp_int_re line 0 then
      "type tmptmptmp = int;; type int = tmptmptmp"
    else line);
  (* Compile the extracted code *)
  (* Extraction sometimes produces ML code that does not implement its interface.
     We circumvent this problem by erasing the interface. **)
  Sys.remove mlif;
  (* TODO: Maxime, thoughts? *)
  (* LEO: However, sometimes the inferred types are too abstract. So we touch the .mli to close the weak types. **)
  let _exit_code = Sys.command ("touch " ^ mlif) in
  (*
  msg_debug (str "Extracted ML file: " ++ str mlf);
  msg_debug (str "Compile command: " ++ str (comp_ml_cmd mlf execn));
  Printf.printf "Extracted ML file: %s\n" mlf;
  Printf.printf "Compile command: %s\n" (comp_ml_cmd mlf execn);
  flush_all ();
  *)
  (* Compile the (empty) .mli *)
  (*
  if Sys.command (comp_mli_cmd mlif) <> 0 then CErrors.user_err (str "Could not compile mli file" ++ fnl ());
  if Sys.command (comp_ml_cmd mlf execn) <> 0 then
    CErrors.user_err (str "Could not compile test program" ++ fnl ())
   *)

  (* Copy over the contents of the ocaml directory *)
  let ocaml_dir_cps = List.map (fun s -> Printf.sprintf "cp -rL %s %s" s dir) !extra_dir in
  List.iter print_endline ocaml_dir_cps;
  List.iter (fun cmd -> ignore (Sys.command cmd)) ocaml_dir_cps;

  let packages =
    match !extra_pkg with
    | [] -> ""
    | x -> "-pkgs '" ^ (String.concat "," x) ^ "'"
  in
  let exec_command =
    match !dune_file with
    | None -> "cd " ^ dir ^ " && ocamlbuild -use-ocamlfind " ^ packages ^ " -lib unix -cflags \"-w -3\" " ^ Filename.basename execn ^ " -quiet > build.log 2> build.err"
    | Some s ->
       (* Modify the dune file to add the executable name and put it in the output dir *) 
       let awk_cmd = Printf.sprintf "awk -v n=2 -v s=\"   (name %s)\" 'NR == n {print s} {print}' %s > %s" (Filename.chop_extension (Filename.basename mlf)) s (dir ^ "/" ^ s) in
       (*       let sed_cmd = Printf.sprintf "sed '2i   (name %s)' %s > %s" (Filename.chop_extension (Filename.basename mlf)) s (dir ^ "/" ^ s) in *)
       ignore (Sys.command awk_cmd);
       (* The command is just dune build *)
       Printf.sprintf "cd %s && dune build --root=. --display=quiet > build.log 2> build.err" dir
  in
  (* Overwrite execn in case of dune *)
  let execn =
    let (</>) = Filename.concat in
    match !dune_file with
    | None -> Filename.dirname execn </> "_build" </> Filename.basename execn
    | Some _ -> dir ^ "/_build/default/" ^ (Filename.chop_extension (Filename.basename execn)) ^ ".exe" in

  if Sys.command exec_command <> 0 then 
    let build_log = read_file (dir ^ "/build.log") in
    let build_err = read_file (dir ^ "/build.err") in
    let msg = str "Could not compile test program: " ++ str mlf ++ fnl () in
    let msg = if build_log = "" then msg else
      msg ++ fnl () ++ str "Build stdout:" ++ fnl () ++ str build_log ++ fnl () in
    let msg = if build_err = "" then msg else
      msg ++ fnl () ++ str "Build stderr:" ++ fnl () ++ str build_err ++ fnl () in
    CErrors.user_err msg

  (* Run the test *)
  else
    let execn = "time " ^ execn in 
    (* Should really be shared across this and the tool *)
    (*
    let (p_out, _, p_err) as process = Unix.open_process_full execn (Unix.environment ()) in
    let rec process_otl_aux () =
      let e = input_line p_out in
      Feedback.msg_notice (Pp.str e);
      process_otl_aux() in
    try process_otl_aux ()
    with End_of_file ->
         let err_msg = read_all p_err in
         let err descr = CErrors.user_err (str (execn ^ ": " ^ descr) ++ fnl () ++ fnl () ++ str err_msg ++ fnl ()) in
         let stat = Unix.close_process_full process in
         begin match stat with
         | Unix.WEXITED 0 -> ()
         | Unix.WEXITED i -> err (Printf.sprintf "Exited with status %d" i)
         | Unix.WSIGNALED i -> err (Printf.sprintf "Killed (%d)" i)
         | Unix.WSTOPPED i -> err (Printf.sprintf "Stopped (%d)" i)
         end
     *)
    let start = Unix.gettimeofday () in
    let (p_out, _, p_err) as process = Unix.open_process_full execn (Unix.environment ()) in
    let process_out () =
(*      let rec process_err_aux () =
        let e = input_line p_err in
        Feedback.msg_notice (Pp.str e);
        process_err_aux() in
*)        
      let rec process_otl_aux () =
        let e = input_line p_out in
        Feedback.msg_notice (Pp.str e);
        process_otl_aux() in
      try process_otl_aux ()
      with End_of_file ->
             let stop = Unix.gettimeofday () in
             let timeElapsed = stop -. start in
             Feedback.msg_notice (Pp.str (Printf.sprintf "Time Elapsed: %fs\n" timeElapsed));
            (* try process_err_aux ()
            with End_of_file ->  *)
              let err_msg = read_all p_err in
              let err descr = CErrors.user_err (str (execn ^ ": " ^ descr) ++ fnl () ++ fnl () ++ str err_msg ++ fnl ()) in
              let stat = Unix.close_process_full process in
              begin match stat with
              | Unix.WEXITED 0 -> ()
              | Unix.WEXITED i -> err (Printf.sprintf "Exited with status %d" i)
              | Unix.WSIGNALED i -> err (Printf.sprintf "Killed (%d)" i)
              | Unix.WSTOPPED i -> err (Printf.sprintf "Stopped (%d)" i)
              end
    in process_out ()

(*
    (** If we want to print the time spent in tests *)
(*    let execn = "time " ^ execn in  *)
    if Sys.command execn <> 0 then
      CErrors.user_err (str "Could not run test" ++ fnl ())
 *)

;;

(* TODO: clean leftover files *)
#if COQ_VERSION >= (8, 20, 0)
let runTest ~opaque_access c env evd : unit =
#else
let runTest c env evd : unit =
#endif
  (* [c] is a constr_expr representing the test to run,
     so we first build a new constr_expr representing
     show c **)
  let c = CAst.make @@ CApp (show, [(c, None)])
  in
  (* Build the kernel term from the const_expr *)

  (*  Printf.printf "Before interp constr\n"; flush stdout; *)

  let (c,_evd) = interp_constr env evd c in

  (* Printf.printf "So far so good?\n"; flush stdout; *)
#if COQ_VERSION >= (8, 20, 0)
  define_and_run ~opaque_access c env evd
#else
  define_and_run c env evd
#endif

let rec last = function
  | [] -> None
  | x :: [] -> Some x
  | _ :: xs -> last xs

#if COQ_VERSION >= (8, 20, 0)
let run ~opaque_access f args =
#else
let run f args =
#endif
  let env = Global.env () in
  let evd = Evd.from_env env in
  begin match last args with
  | Some qc_text ->
    let msg = "QuickChecking " ^ Pp.string_of_ppcmds (Ppconstr.pr_constr_expr env evd qc_text) in
    Feedback.msg_notice (Pp.str msg)
  | None -> failwith "run called with no arguments"
  end;
  let args = List.map (fun x -> (x,None)) args in
  let c = CAst.make @@ CApp (f, args) in
#if COQ_VERSION >= (8,20, 0)
  runTest ~opaque_access c env evd
#else
  runTest c env evd
#endif

let set_debug_flag (flag_name : string) (mode : string) =
  let toggle =
    match mode with
    | "On"  -> true
    | "Off" -> false
  in
  let reference =
    match flag_name with
    | "Debug" -> flag_debug
(*    | "Warn"  -> flag_warn
    | "Error" -> flag_error *)
  in
  reference := toggle 

let extract_manually : qualid list ref =
  Summary.ref ~name:"QC_manual_extracts" []
let add_manual_extract cs =
  let convert_reference_to_qualid c : qualid =
    match c with
    | {CAst.v = CRef (r, _) ; _ } -> r 
    | _ -> failwith "Usage: Extract Manually failed." in
  let refs : qualid list =
    match cs with
    | { CAst.v = CNotation (_,_,([a],[b],_,_)) ; _ } -> begin
         let q = convert_reference_to_qualid a in
         let qs = List.map convert_reference_to_qualid b in
         q :: qs
       end
    | _ -> [convert_reference_to_qualid cs] in 
  extract_manually := refs @ !extract_manually

#if COQ_VERSION >= (8, 20, 0)
let extract_prop_and_deps ~opaque_access prop =
#else
let extract_prop_and_deps prop =
#endif
  let env = Global.env () in
  let evd = Evd.from_env env in
  let (prop_expr, evd') = interp_constr env evd prop in
  let prop_def = define prop_expr env evd in
  let prop_mlf = new_ml_file () in
  let temp_dir = Filename.dirname prop_mlf in
  let execn = Filename.chop_extension prop_mlf in
  let prop_mlif = execn ^ ".mli" in
  let warnings = CWarnings.get_flags () in
  let mute_extraction = warnings ^ (if warnings = "" then "" else ",") ^ "-extraction-opaque-accessed" in
  CWarnings.set_flags mute_extraction;
#if COQ_VERSION >= (8, 20, 0)
  Flags.silently (Extraction_plugin.Extract_env.full_extraction ~opaque_access (Some prop_mlf)) [qualid_of_ident prop_def];
#else
  Flags.silently (Extraction_plugin.Extract_env.full_extraction (Some prop_mlf)) [qualid_of_ident prop_def];
#endif
  CWarnings.set_flags warnings;
  (prop_def, temp_dir, execn, prop_mlf, prop_mlif, warnings)

#if COQ_VERSION >= (8, 20, 0)
let qcFuzz_main ~opaque_access prop_def temp_dir execn prop_mlf prop_mlif warnings prop fuzzLoop =
#else
let qcFuzz_main prop_def temp_dir execn prop_mlf prop_mlif warnings prop fuzzLoop =
#endif

  (* Override extraction to use the new, instrumented property *)
  let qualify s = Printf.sprintf "%s.%s" (Filename.basename execn) s in
  let prop_name = qualify (Id.to_string prop_def) in
  let prop_ref =
    match prop with
    | { CAst.v = CRef (r,_) ; _ } -> r
    | _ -> failwith "Not a reference"
  in
  Extraction_plugin.Table.extract_constant_inline false prop_ref [] prop_name;

(*
  List.iter (fun x -> print_endline (string_of_qualid
                                       ((match qualid_of_reference x with {CAst.v = q; _} -> q)))) !extract_manually;
                                       *)      
  List.iter (fun r ->
      match GenericLib.sdt_rep_from_mib (GenericLib.qualid_to_mib r) with
      | Some (ty_ctr, ty_params, ctrs) -> begin
          (*          print_endline "Extracting inductive..."; *)
          let ty_ctr_name = qualify (String.uncapitalize_ascii (GenericLib.ty_ctr_to_string ty_ctr)) in
          (*          print_endline ty_ctr_name; *)
          let ctr_names =
            match ctrs with
            | [ctr,ctr_ty] ->
               if GenericLib.coq_type_size ctr_ty = 1 then [""]
               else [qualify (GenericLib.constructor_to_string ctr)]
            | _ -> List.map (fun (ctr,_) -> qualify (GenericLib.constructor_to_string ctr)) ctrs in
          (* List.iter print_endline ctr_names; *)
          Extraction_plugin.Table.extract_inductive 
            (GenericLib.tyCtrToQualid ty_ctr)
            ty_ctr_name
            ctr_names
            None
        end
      | None -> failwith "Can't be represented..."
    ) !extract_manually;

  (* Define fuzzLoop applied appropriately *)
  let unit_type =
    CAst.make @@ CRef (qualid_of_string "Coq.Init.Datatypes.unit", None) in
  let unit_arg =
#if COQ_VERSION >= (8, 20, 0)
    CLocalAssum ( [ CAst.make (Name (fresh_name "x")) ], None, Default Glob_term.Explicit, unit_type ) in
#else
    CLocalAssum ( [ CAst.make (Name (fresh_name "x")) ], Default Glob_term.Explicit, unit_type ) in
#endif
  let pair_ctr =
    CAst.make @@ CRef (qualid_of_string "Coq.Init.Datatypes.pair", None) in
  let show_expr cexpr =
    CAst.make @@ CApp (show, [(cexpr,None)]) in
  let show_and_c_fun : constr_expr =
    Constrexpr_ops.mkCLambdaN [unit_arg] 
      (let fx = fresh_name "_qc_res" in
       let fx_expr = (CAst.make @@ CRef (qualid_of_ident fx,None)) in

       CAst.make @@ CLetIn (CAst.make @@ Name fx, fuzzLoop, None, 
                            CAst.make @@ CApp (pair_ctr,
                                               [(fx_expr, None);
                                                (show_expr fx_expr, None)]))) in
    (* Build the kernel term from the const_expr *)
  let env = Global.env () in
  let evd = Evd.from_env env in
  let (show_and_c_fun, evd') = interp_constr env evd show_and_c_fun in

  let show_and_c_fun_def = define show_and_c_fun env evd in
  let mlf = Filename.temp_file ~temp_dir "QuickChick" ".ml" in
  let execn = Filename.chop_extension mlf in
  let mlif = execn ^ ".mli" in
  let mute_extraction = warnings ^ (if warnings = "" then "" else ",") ^ "-extraction-opaque-accessed" in
  CWarnings.set_flags mute_extraction;
#if COQ_VERSION >= (8, 20, 0)
  Flags.silently (Extraction_plugin.Extract_env.full_extraction ~opaque_access (Some mlf)) [qualid_of_ident show_and_c_fun_def];
#else
  Flags.silently (Extraction_plugin.Extract_env.full_extraction (Some mlf)) [qualid_of_ident show_and_c_fun_def];
#endif

  (* Add a main function to get some output *)
  let oc = open_out_gen [Open_append;Open_text] 0o666 mlf in
  Printf.fprintf oc "let _ = \n\
    Printf.printf \"Entering main of qc_exec\\n\"; flush stdout;\n\
    setup_shm_aux ();\n\
(*  Printexc.record_backtrace true;  *)\n\
    let toStr l = \n\
     let s = Bytes.create (List.length l) in\n\
     let rec copy i = function\n\
     | [] -> s\n\
     | c :: l -> Bytes.set s i c; copy (i+1) l\n\
     in Bytes.to_string (copy 0 l) in\n\
    print_string (toStr (snd ((%s) ()))); flush stdout;\n"
  (Id.to_string show_and_c_fun_def);
  close_out oc;

  (* Append the appropriate definitions in the beginning *)
  let user_contrib = "$(opam var lib)/coq/user-contrib/QuickChick" in
  (* Add preamble *)
  let echo_cmd =
    Printf.sprintf "cat %s/Stub.ml | cat - %s > temp && mv temp %s" user_contrib mlf mlf in
  print_endline echo_cmd;
  ignore (Sys.command echo_cmd);

  (* HORRIBLE. HORRIBLE. Perl hack to ensure tail recursion... *)
  (* First copy them over from contrib... *)
  ignore (Sys.command (Printf.sprintf "cp %s/cmdprefix.pl %s" user_contrib temp_dir));
  ignore (Sys.command (Printf.sprintf "cp %s/cmdsuffix.pl %s" user_contrib temp_dir));
  (* ... then execute them ... *)
  ignore (Sys.command (Printf.sprintf "%s/cmdprefix.pl %s" temp_dir mlf));
  ignore (Sys.command (Printf.sprintf "%s/cmdsuffix.pl %s" temp_dir mlf));
  
  (* Copy fuzz-related files to temp directory *)
  ignore (Sys.command (Printf.sprintf "cp %s/alloc-inl.h %s" user_contrib temp_dir));
  ignore (Sys.command (Printf.sprintf "cp %s/debug.h %s" user_contrib temp_dir));
  ignore (Sys.command (Printf.sprintf "cp %s/types.h %s" user_contrib temp_dir));
  ignore (Sys.command (Printf.sprintf "cp %s/config.h %s" user_contrib temp_dir));
  ignore (Sys.command (Printf.sprintf "cp %s/SHM.c %s" user_contrib temp_dir));

  (* Compile. Prop with instrumentation, rest without *)
  (*
  let path = Lazy.force path in
  let link_files = List.map (Filename.concat path) link_files in
  let link_files = String.concat " " link_files in
  let afl_path = eval_command "opam config var lib" ^ "/afl-persistent/" in
  let afl_link = afl_path ^ "afl-persistent.cmxa" in
  let extra_link_files =
    String.concat " " (List.map (fun (s : string * string) -> temp_dir ^ "/" ^ fst s) !extra_files) in
  print_endline ("Extra: " ^ extra_link_files);
   *)
  let zarith = "-I $(opam var lib)/zarith $(opam var lib)/zarith/zarith.cmxa" in
  
  let ocamlopt = "ocamlopt -ccopt -Wno-error=implicit-function-declaration" in
  let comp_mli_cmd instr_flag fn =
    Printf.sprintf "%s %s unix.cmxa %s -rectypes -w a -I %s %s" ocamlopt instr_flag zarith
      (Filename.dirname fn) fn
  in

  let comp_prop_ml_cmd fn = 
    Printf.sprintf "%s -afl-instrument unix.cmxa str.cmxa %s -rectypes -w a -I %s %s"
      ocamlopt zarith (Filename.dirname fn) fn
  in 

  let comp_exec_ml_cmd fn prop_fn execn =
    Printf.sprintf "%s unix.cmxa str.cmxa %s -rectypes -w a -I %s %s -o %s %s %s/SHM.c"
      ocamlopt zarith (Filename.dirname fn) (Filename.chop_extension prop_fn ^ ".cmx") execn fn temp_dir
  in  
(*  let comp_mli_cmd instr_flag fn =
    Printf.sprintf "%s %s unix.cmxa %s -rectypes -w a -I %s -I %s %s %s" ocamlopt instr_flag afl_link
      (Filename.dirname fn) path link_files fn
  in

  let comp_prop_ml_cmd fn = 
    Printf.sprintf "%s -afl-instrument unix.cmxa str.cmxa %s -rectypes -w a -I %s -I %s -I %s %s %s %s"
      ocamlopt afl_link (Filename.dirname fn) afl_path path link_files extra_link_files fn
  in 

  let comp_exec_ml_cmd fn prop_fn execn =
    Printf.sprintf "%s unix.cmxa str.cmxa %s -rectypes -w a -I %s -I %s -I %s %s %s %s -o %s %s %s/SHM.c"
      ocamlopt afl_link (Filename.dirname fn) afl_path path link_files extra_link_files (Filename.chop_extension prop_fn ^ ".cmx") execn fn temp_dir
  in
 *)

  (* Compile the .mli *)
  if Sys.command (comp_mli_cmd "-afl-instrument" prop_mlif) <> 0 then CErrors.user_err (str "Could not compile mli file: " ++ str (comp_mli_cmd "-afl-instrument" prop_mlif) ++ fnl ());
  (* Compile the instrumented property .ml *)
  if Sys.command (comp_prop_ml_cmd prop_mlf) <> 0 then
    (CErrors.user_err (str "Could not compile test program: " ++ str (comp_prop_ml_cmd prop_mlf) ++ fnl ()));

  (* Compile the executable .mli, no instrumentation *)
  if Sys.command (comp_mli_cmd " " mlif) <> 0 then CErrors.user_err (str "Could not compile exec mli file" ++ fnl ());
  (* Compile the actual executable *)
  let cmp_cmd = comp_exec_ml_cmd mlf prop_mlf (temp_dir ^ "/qc_exec") in
  Printf.printf "Compile Command: %s\n" cmp_cmd; flush stdout;
  if Sys.command (cmp_cmd) <> 0 then
    (CErrors.user_err (str "Could not compile exec program" ++ fnl ()));

  (* Copy over the main file that actually sets up the shm... *)
  ignore (Sys.command (Printf.sprintf "cp %s/Main.ml %s" user_contrib temp_dir));
  let comp_main_cmd fn execn : string = 
    Printf.sprintf "%s unix.cmxa str.cmxa -rectypes -w a -I %s -o %s %s %s/SHM.c"
      ocamlopt (Filename.dirname fn) execn fn temp_dir in
  let cmp_cmd_main = comp_main_cmd (temp_dir ^ "/Main.ml") (temp_dir ^ "/main_exec") in
  Printf.printf "Compile Main Command: %s\n" cmp_cmd_main;
  if (Sys.command cmp_cmd_main <> 0) then
    (CErrors.user_err (str "Could not compile main program" ++ fnl ()));

  (* Run the FuzzQC command, parse the output, search for "Passed" or "Failed" *)
  let found_result = ref (None : bool option) in
  let run_and_show_output command =
    let chan = Unix.open_process_in command in
    let res = ref ([] : string list) in
    let str_success = Str.regexp_string "Passed" in
    let str_failure = Str.regexp_string "Failed" in
    let contains r s =
      try let ix = Str.search_forward r s 0 in ix >= 0
      with _ -> false in
    let rec process_otl_aux () =
      let e = input_line chan in
      res := e::!res;
      if contains str_success e then found_result := Some true;
      if contains str_failure e then found_result := Some false;
      process_otl_aux() in
    try process_otl_aux ()
    with End_of_file ->
          let stat = Unix.close_process_in chan in
          let result =
            match stat with
              Unix.WEXITED 0 -> List.rev !res
            | Unix.WEXITED i -> List.rev (Printf.sprintf "Exited with status %d" i :: !res)
            | Unix.WSIGNALED i -> List.rev (Printf.sprintf "Killed (%d)" i :: !res)
            | Unix.WSTOPPED i -> List.rev (Printf.sprintf "Stopped (%d)" i :: !res) in
          List.iter (fun s -> (print_string s; print_newline())) result
       | _ -> failwith "LOL"
  in
    
  run_and_show_output ("time " ^ temp_dir ^ "/main_exec " ^ temp_dir ^ "/qc_exec");
  print_endline (match !found_result with
                 | Some true -> "Found success!"
                 | Some false -> "Found failure!"
                 | _ -> "Found nothing..."
    );
  !found_result
  (* open linked ocaml files 
  List.iter (fun (s : string * string) ->
      let (fn, c) = s in
      let sed_cmd = (Printf.sprintf "sed -i '1s;^;open %s\\n;' %s" c mlf) in
      print_endline ("Sed cmd: " ^ sed_cmd);
      ignore (Sys.command sed_cmd);
      ignore (Sys.command (Printf.sprintf "cp %s %s" fn temp_dir));
    ) !extra_files;
   *)

#if COQ_VERSION >= (8, 20, 0)
let qcFuzz ~opaque_access prop fuzzLoop =
  let (prop_def, temp_dir, execn, prop_mlf, prop_mlif, warnings) =
    extract_prop_and_deps ~opaque_access prop in
  qcFuzz_main ~opaque_access prop_def temp_dir execn prop_mlf prop_mlif warnings prop fuzzLoop
#else
let qcFuzz prop fuzzLoop =
  let (prop_def, temp_dir, execn, prop_mlf, prop_mlif, warnings) =
    extract_prop_and_deps prop in
  qcFuzz_main prop_def temp_dir execn prop_mlf prop_mlif warnings prop fuzzLoop
#endif

}


#if COQ_VERSION >= (8, 20, 0)
VERNAC COMMAND EXTEND QuickCheck CLASSIFIED AS SIDEFF STATE opaque_access
#else
VERNAC COMMAND EXTEND QuickCheck CLASSIFIED AS SIDEFF
#endif
  | ["QuickCheck" constr(c)] ->     {run quickCheck [c]}
  | ["QuickCheckWith" constr(c1) constr(c2)] ->     {run quickCheckWith [c1;c2]}
END

#if COQ_VERSION >= (8, 20, 0)
VERNAC COMMAND EXTEND QuickChick CLASSIFIED AS SIDEFF STATE opaque_access
#else
VERNAC COMMAND EXTEND QuickChick CLASSIFIED AS SIDEFF
#endif
  | ["QuickChick" constr(c)] ->     {run quickCheck [c]}
  | ["QuickChickWith" constr(c1) constr(c2)] ->     {run quickCheckWith [c1;c2]}
END

#if COQ_VERSION >= (8, 20, 0)
VERNAC COMMAND EXTEND MutateCheck CLASSIFIED AS SIDEFF STATE opaque_access
#else
VERNAC COMMAND EXTEND MutateCheck CLASSIFIED AS SIDEFF
#endif
  | ["MutateCheck" constr(c1) constr(c2)] ->     {run mutateCheck [c1;c2]}
  | ["MutateCheckWith" constr(c1) constr(c2) constr(c3)] ->     {run mutateCheckWith [c1;c2;c3]}
END

#if COQ_VERSION >= (8, 20, 0)
VERNAC COMMAND EXTEND MutateChick CLASSIFIED AS SIDEFF STATE opaque_access
#else
VERNAC COMMAND EXTEND MutateChick CLASSIFIED AS SIDEFF
#endif
  | ["MutateChick" constr(c1) constr(c2)] ->     {run mutateCheck [c1;c2]}
  | ["MutateChickWith" constr(c1) constr(c2) constr(c3)] ->     {run mutateCheckWith [c1;c2;c3]}
END

#if COQ_VERSION >= (8, 20, 0)
VERNAC COMMAND EXTEND MutateCheckMany CLASSIFIED AS SIDEFF STATE opaque_access
#else
VERNAC COMMAND EXTEND MutateCheckMany CLASSIFIED AS SIDEFF
#endif
  | ["MutateCheckMany" constr(c1) constr(c2)] ->     {run mutateCheckMany [c1;c2]}
  | ["MutateCheckManyWith" constr(c1) constr(c2) constr(c3)] ->     {run mutateCheckManyWith [c1;c2;c3]}
END

#if COQ_VERSION >= (8, 20, 0)
VERNAC COMMAND EXTEND MutateChickMany CLASSIFIED AS SIDEFF STATE opaque_access
#else
VERNAC COMMAND EXTEND MutateChickMany CLASSIFIED AS SIDEFF
#endif
  | ["MutateChickMany" constr(c1) constr(c2)] ->     {run mutateCheckMany [c1;c2]}
  | ["MutateChickManyWith" constr(c1) constr(c2) constr(c3)] ->     {run mutateCheckManyWith [c1;c2;c3]}
END

VERNAC COMMAND EXTEND QuickChickDebug CLASSIFIED AS SIDEFF
  | ["QuickChickDebug" ident(s1) ident(s2)] ->
     { let s1' = Id.to_string s1 in
       let s2' = Id.to_string s2 in
       set_debug_flag s1' s2' }
END

#if COQ_VERSION >= (8, 20, 0)
VERNAC COMMAND EXTEND Sample CLASSIFIED AS SIDEFF STATE opaque_access
#else
VERNAC COMMAND EXTEND Sample CLASSIFIED AS SIDEFF
#endif
  | ["Sample" constr(c)] -> {run sample [c]}
END

#if COQ_VERSION >= (8, 20, 0)
VERNAC COMMAND EXTEND Sample1 CLASSIFIED AS SIDEFF STATE opaque_access
#else
VERNAC COMMAND EXTEND Sample1 CLASSIFIED AS SIDEFF
#endif
  | ["Sample1" constr(c)] -> {run sample1 [c]}
END

VERNAC COMMAND EXTEND QCInclude CLASSIFIED AS SIDEFF
  | ["QCInclude" string(s)] -> { add_extra_dir s }
END

VERNAC COMMAND EXTEND QCOpen CLASSIFIED AS SIDEFF
  | ["QCOpen" string(s)] -> { add_module_to_open s }
END

VERNAC COMMAND EXTEND QCPackage CLASSIFIED AS SIDEFF
  | ["QCPackage" string(s)] -> { add_extra_pkg s }
END

VERNAC COMMAND EXTEND QCdune CLASSIFIED AS SIDEFF
  | ["QCDune" string(s)] -> { set_dune_file s }
END

VERNAC COMMAND EXTEND ManualExtract CLASSIFIED AS SIDEFF
   | ["ManualExtract" constr(inductives) ] -> { add_manual_extract inductives }
END

#if COQ_VERSION >= (8, 20, 0)
VERNAC COMMAND EXTEND FuzzQC CLASSIFIED AS SIDEFF STATE opaque_access
| ["FuzzChick" constr(prop) constr(fuzzLoop) ] ->  { fun ~opaque_access ->
       ignore (qcFuzz prop ~opaque_access fuzzLoop) }
END
#else
VERNAC COMMAND EXTEND FuzzQC CLASSIFIED AS SIDEFF
  | ["FuzzChick" constr(prop) constr(fuzzLoop) ] ->  { ignore (qcFuzz prop fuzzLoop) }
END
#endif

VERNAC COMMAND EXTEND QCExtractDir CLASSIFIED AS SIDEFF
  | ["QCExtractDir" string(s)] -> { set_extract_dir s }
END