(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* coqmktop is a script to link Coq, analogous to ocamlmktop.
   The command line contains options specific to coqmktop, options for the
   Ocaml linker and files to link (in addition to the default Coq files). *)

open Unix

(* In Win32 outside cygwin, Sys.command calls cmd.exe. When it executes
   a command that may contains many double-quote, we should double-quote
   the whole ! *)

let safe_sys_command =
  if Sys.os_type = "Win32" then
    fun cmd -> Sys.command ("\""^cmd^"\"")
  else Sys.command

(* Objects to link *)

(* 1. Core objects *)
let ocamlobjs = ["str.cma";"unix.cma";"nums.cma"]
let dynobjs = ["dynlink.cma"]
let camlp4objs =
  if Coq_config.camlp4 = "camlp5" then ["gramlib.cma"] else ["camlp4lib.cma"]
let libobjs = ocamlobjs @ camlp4objs

let spaces = Str.regexp "[ \t\n]+"
let split_list l = Str.split spaces l

let copts     = split_list Tolink.copts
let core_objs = split_list Tolink.core_objs
let core_libs = split_list Tolink.core_libs

(* 3. Toplevel objects *)
let camlp4topobjs =
  if Coq_config.camlp4 = "camlp5" then
    ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
  else
    [ "Camlp4Top.cmo";
      "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
      "Camlp4Parsers/Camlp4OCamlParser.cmo";
      "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
let topobjs = camlp4topobjs

let gramobjs = []
let notopobjs = gramobjs

(* 4. High-level tactics objects *)

(* environment *)
let opt        = ref false
let full       = ref false
let top        = ref false
let echo       = ref false
let no_start   = ref false

let is_ocaml4 = Coq_config.caml_version.[0] <> '3'

(* Since the .cma are given with their relative paths (e.g. "lib/clib.cma"),
   we only need to include directories mentionned in the temp main ml file
   below (for accessing the corresponding .cmi). *)

let src_dirs =
  [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"]; ]

let includes () =
  let coqlib = if !Flags.boot then "." else Envars.coqlib () in
  let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
  (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs [])
  @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""]
  @ (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])

(* Transform bytecode object file names in native object file names *)
let native_suffix f =
  if Filename.check_suffix f ".cmo" then
    (Filename.chop_suffix f ".cmo") ^ ".cmx"
  else if Filename.check_suffix f ".cma" then
    (Filename.chop_suffix f ".cma") ^ ".cmxa"
  else
    if Filename.check_suffix f ".a" then f
    else
      failwith ("File "^f^" has not extension .cmo, .cma or .a")

(* Transforms a file name in the corresponding Caml module name. *)
let rem_ext_regexpr = Str.regexp "\\(.*\\)\\.\\(cm..?\\|ml\\)"

let module_of_file name =
  let s = Str.replace_first rem_ext_regexpr "\\1" (Filename.basename name) in
  String.capitalize s

(* Build the list of files to link and the list of modules names *)
let files_to_link userfiles =
  let dyn_objs =
    if not !opt || Coq_config.has_natdynlink then dynobjs else [] in
  let toplevel_objs =
    if !top then topobjs else if !opt then notopobjs else [] in
  let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs in
  let modules = List.map module_of_file (objs @ userfiles)
  in
  let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs in
  let libstolink =
    (if !opt then List.map native_suffix libs else libs) @ userfiles
  in
  (modules, libstolink)

(* Gives the list of all the directories under [dir].
   Uses [Unix] (it is hard to do without it). *)
let all_subdirs dir =
  let l = ref [dir] in
  let add f = l := f :: !l in
  let rec traverse dir =
    let dirh =
      try opendir dir with Unix_error _ -> invalid_arg "all_subdirs"
    in
    try
      while true do
	let f = readdir dirh in
	if f <> "." && f <> ".." then
	  let file = Filename.concat dir f in
	  if (stat file).st_kind = S_DIR then begin
	    add file;
	    traverse file
	  end
      done
    with End_of_file ->
      closedir dirh
  in
  traverse dir; List.rev !l

(* usage *)
let usage () =
  prerr_endline "Usage: coqmktop <options> <ocaml options> files\
\nFlags are:\
\n  -coqlib dir    Specify where the Coq object files are\
\n  -camlbin dir   Specify where the OCaml binaries are\
\n  -camlp4bin dir Specify where the Camlp4/5 binaries are\
\n  -o exec-file   Specify the name of the resulting toplevel\
\n  -boot          Run in boot mode\
\n  -echo          Print calls to external commands\
\n  -full          Link high level tactics\
\n  -opt           Compile in native code\
\n  -top           Build Coq on a OCaml toplevel (incompatible with -opt)\
\n  -R dir         Add recursively dir to OCaml search path\
\n";
  exit 1

(* parsing of the command line *)
let parse_args () =
  let rec parse (op,fl) = function
    | [] -> List.rev op, List.rev fl
    | "-coqlib" :: d :: rem ->
	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
    | "-coqlib" :: _        -> usage ()
    | "-camlbin" :: d :: rem ->
	Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
    | "-camlbin" :: _        -> usage ()
    | "-camlp4bin" :: d :: rem ->
	Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
    | "-camlp4bin" :: _        -> usage ()
    | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem
    | "-opt" :: rem -> opt := true ; parse (op,fl) rem
    | "-full" :: rem -> full := true ; parse (op,fl) rem
    | "-top" :: rem -> top := true ; parse (op,fl) rem
    | "-v8" :: rem ->
	Printf.eprintf "warning: option -v8 deprecated";
	parse (op,fl) rem
    | "-echo" :: rem -> echo := true ; parse (op,fl) rem
    | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' ->
	begin
	  match rem' with
	    | a :: rem -> parse (a::o::op,fl) rem
	    | []       -> usage ()
	end
    | "-R" :: a :: rem ->
        parse ((List.rev(List.flatten (List.map (fun d -> ["-I";d])
					 (all_subdirs a))))@op,fl) rem
    | "-R" :: [] -> usage ()
    | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
        parse (o::op,fl) rem
    | ("-h"|"--help") :: _ -> usage ()
    | ("-no-start") :: rem -> no_start:=true; parse (op, fl) rem
    | f :: rem ->
	if Filename.check_suffix f ".ml"
	  or Filename.check_suffix f ".cmx"
	  or Filename.check_suffix f ".cmo"
	  or Filename.check_suffix f ".cmxa"
	  or Filename.check_suffix f ".cma"
	  or Filename.check_suffix f ".c" then
	    parse (op,f::fl) rem
	else begin
	  prerr_endline ("Don't know what to do with " ^ f);
	  exit 1
	end
  in
  parse ([Coq_config.osdeplibs],[]) (List.tl (Array.to_list Sys.argv))

let clean file =
  let rm f = if Sys.file_exists f then Sys.remove f in
  let basename = Filename.chop_suffix file ".ml" in
  if not !echo then begin
    rm file;
    rm (basename ^ ".o");
    rm (basename ^ ".cmi");
    rm (basename ^ ".cmo");
    rm (basename ^ ".cmx")
  end

(* Creates another temporary file for Dynlink if needed *)
let tmp_dynlink()=
  let tmp = Filename.temp_file "coqdynlink" ".ml" in
  let _ = Sys.command ("echo \"Dynlink.init();;\" > "^tmp) in
  tmp

(* Initializes the kind of loading in the main program *)
let declare_loading_string () =
  if not !top then
    "Mltop.remove ();;"
  else
    "begin try\
\n       (* Enable rectypes in the toplevel if it has the directive #rectypes *)\
\n       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\
\n         | Toploop.Directive_none f -> f ()\
\n         | _ -> ()\
\n       end\
\n     with\
\n       | Not_found -> ()\
\n     end;;\
\n\
\n     let ppf = Format.std_formatter;;\
\n     Mltop.set_top\
\n       {Mltop.load_obj=\
\n         (fun f -> if not (Topdirs.load_file ppf f) then Util.error (\"Could not load plugin \"^f));\
\n        Mltop.use_file=Topdirs.dir_use ppf;\
\n        Mltop.add_dir=Topdirs.dir_directory;\
\n        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\
\n"

(* create a temporary main file to link *)
let create_tmp_main_file modules =
  let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in
  try
    (* Add the pre-linked modules *)
    output_string oc "List.iter Mltop.add_known_module [\"";
    output_string oc (String.concat "\";\"" modules);
    output_string oc "\"];;\n";
    (* Initializes the kind of loading *)
    output_string oc (declare_loading_string());
    (* Start the toplevel loop *)
    if not !no_start then
    output_string oc "Coqtop.start();;\n";
    close_out oc;
    main_name
  with reraise ->
    clean main_name; raise reraise

(* main part *)
let main () =
  let (options, userfiles) = parse_args () in
  (* which ocaml command to invoke *)
  let camlbin = Envars.camlbin () in
  let prog =
    if !opt then begin
      (* native code *)
      if !top then failwith "no custom toplevel in native code !";
      let ocamloptexec = Filename.quote (Filename.concat camlbin "ocamlopt") in
        ocamloptexec^" -linkall"
    end else
      (* bytecode (we shunt ocamlmktop script which fails on win32) *)
      let ocamlmktoplib = if is_ocaml4
	then " ocamlcommon.cma ocamlbytecomp.cma ocamltoplevel.cma"
	else " toplevellib.cma" in
      let ocamlcexec = Filename.quote (Filename.concat camlbin "ocamlc") in
      let ocamlccustom = Printf.sprintf "%s %s -linkall "
        ocamlcexec Coq_config.coqrunbyteflags in
      (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
  in
  (* files to link *)
  let (modules, tolink) = files_to_link userfiles in
  (*file for dynlink *)
  let dynlink=
    if not (!opt || !top) then
      [tmp_dynlink()]
    else
      []
  in
  (* the list of the loaded modules *)
  let main_file = create_tmp_main_file modules in
  try
    let args = options @ includes () @ copts @ tolink @ dynlink in
    let args = args @ [ Filename.quote main_file ] in
      (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
    let args = if !top then args @ [ "topstart.cmo" ] else args in
      (* Now, with the .cma, we MUST use the -linkall option *)
    let command = String.concat " " (prog::"-rectypes"::args) in
      if !echo then
	begin
	  print_endline command;
	  print_endline
	    ("(command length is " ^
	       (string_of_int (String.length command)) ^ " characters)");
	  flush Pervasives.stdout
	end;
      let retcode = safe_sys_command command in
	clean main_file;
	(* command gives the exit code in HSB, and signal in LSB !!! *)
	if retcode > 255 then retcode lsr 8 else retcode
  with reraise ->
    clean main_file; raise reraise

let retcode =
  try Printexc.print main () with any -> 1

let _ = exit retcode