(*
 * Author: Kaustuv Chaudhuri <kaustuv.chaudhuri@inria.fr>
 * Copyright (C) 2023  Inria (Institut National de Recherche
 *                     en Informatique et en Automatique)
 * See LICENSE for licensing details.
 *)

(* Dependency generator for Abella *)

open Extensions

let dep_tab : (string, string list option) Hashtbl.t = Hashtbl.create 19

let rec add_input_file recursive file =
  match Unix.stat file with
  | { st_kind = S_DIR ; _ } when recursive -> begin
      let dir = file in
      let fs = Sys.readdir dir in
      Array.fast_sort String.compare fs ;
      Array.iter begin fun file ->
        let file = Filename.concat dir file in
        add_input_file recursive file
      end fs
    end
  | { st_kind = S_REG ; _ } when Filename.check_suffix file ".thm" -> begin
      let thmfile = file in
      match Hashtbl.find dep_tab thmfile with
      | None ->
          failwithf "Circular dependencies detected for %S" thmfile
      | Some _ -> ()
      | exception Not_found -> begin
          let base = Filename.chop_suffix thmfile ".thm" in
          let thcfile = base ^ ".thc" in
          Hashtbl.replace dep_tab thcfile None ;
          let (specs, deps) = Depend.thm_dependencies base in
          let deps = List.map (fun f -> f ^ ".thc") deps in
          let deps = specs @ deps in
          Hashtbl.replace dep_tab thcfile (Some deps)
        end
    end
  | { st_kind = S_REG ; _ } ->
      if not recursive then
        failwithf "Illegal file %S; input files must have suffix .thm" file
  | _ ->
      failwithf "Cannot process: %s" file

type conf = {
  abella : string ;
  makefile : string ;
  clobber : bool ;
  recursive : bool ;
}

let mk_conf abella makefile clobber recursive =
  { abella ; makefile ; clobber ; recursive }

let abella_dep conf files =
  List.iter (add_input_file conf.recursive) files ;
  if not conf.clobber && conf.makefile <> "-" &&
     Sys.file_exists conf.makefile
  then failwithf "Would clobber %S but not given option -c" conf.makefile ;
  if Hashtbl.length dep_tab = 0 then () else
  let (out, close) = match conf.makefile with
    | "-" -> (stdout, fun () -> ())
    | f ->
        let ch = open_out_bin f in
        (ch, fun () -> close_out ch)
  in
  Printf.fprintf out "# DO NOT EDIT! This file was autogenerated by abella_dep.\n" ;
  let time =
    let tm = Unix.time () |> Unix.gmtime in
    Printf.sprintf "%4d-%02d-%02d %02d:%02d:%02dZ"
      (tm.tm_year + 1900) (tm.tm_mon + 1) tm.tm_mday
      tm.tm_hour tm.tm_min tm.tm_sec in
  Printf.fprintf out "# Generated on: %s\n" time ;
  Printf.fprintf out ".PHONY: all\n" ;
  Printf.fprintf out "%%.thc: %%.thm\n" ;
  Printf.fprintf out "\t%s --non-recursive --output=${<:%%.thm=%%.out} $<\n" conf.abella ;
  Hashtbl.iter begin fun file deps ->
    if not @@ Filename.check_suffix file ".thc" then () else
    Printf.fprintf out "all: %s\n" file ;
    match deps with
    | None ->
        failwithf "BUG: incomplete dependencies for %S" file
    | Some deps ->
        if deps = [] then () else
        let deps = String.concat " " deps in
        Printf.fprintf out "%s: %s\n" file deps
  end dep_tab ;
  close ()

(******************************************************************************)
(* Command line parsing *)

let () =
  let open Cmdliner in
  let conf =
    let abella =
      let default =
        let dir = Filename.dirname Sys.executable_name in
        let ab1 = Filename.concat dir "abella" in
        let ab2 = Filename.concat dir "abella.exe" in
        let ab3 = Filename.concat dir "abella.bc" in
        if Sys.file_exists ab1 then ab1
        else if Sys.file_exists ab2 then ab2
        else ab3 in
      let env = Cmd.Env.info "ABELLA"
          ~doc:"Abella command to run (overriden by $(b,--abella))" in
      let doc = "Set the Abella command to $(docv)." in
      Arg.(value @@ opt string default @@
           info ["a" ; "abella"] ~doc ~env
             ~docv:"CMD"
             ~absent:"$(b,abella[.exe])")
    in
    let makefile =
      let doc = "Output dependencies to $(docv) as a makefile. \
                 If $(docv) is $(b,-), then send the output to \
                 the standard output." in
      Arg.(value @@ opt string "-" @@
           info ["o" ; "output"] ~doc
             ~docv:"FILE"
             ~absent:"standard output")
    in
    let clobber =
      let doc = "Clobber (overwrite) an existing file specified with $(b,-o)." in
      Arg.(value @@ flag @@ info ["c" ; "clobber"] ~doc)
    in
    let recursive =
      let doc = "Process directories recursively." in
      Arg.(value @@ flag @@ info ["r"] ~doc)
    in
    Term.(const mk_conf $ abella $ makefile $ clobber $ recursive) in
  let files =
    let doc = "An Abella $(b,.thm) file or a directory" in
    Arg.(value @@ pos_all string [] @@ info [] ~docv:"SOURCE" ~doc)
  in
  let cmd =
    let doc = "Generate makefiles for a collection of Abella sources" in
    let man = [
      `S Manpage.s_examples ;
      `Blocks [
        `P "To create a Makefile from a.thm, d/b.thm, and c/*.thm" ;
        `Pre "  \\$ $(tname) a.thm d/b.thm c/*.thm" ;
        `P "To create a Makefile recursively from all .thm files in d/" ;
        `Pre "  \\$ $(tname) -r d" ;
      ] ;
      `S Manpage.s_see_also ;
      `P "$(b,abella)(1)" ;
      `S Manpage.s_bugs ;
      `P "File bug reports at <$(b,https://github.com/abella-prover/abella/issues)>" ;
    ] in
    let info = Cmd.info "abella_dep" ~doc ~man ~exits:[] in
    Cmd.v info @@ Term.(const abella_dep $ conf $ files)
  in
  exit (Cmd.eval cmd)
