<commit_before>(* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
(* Licensed under the Apache 2.0 License. *)

(** Decorate each file with a little bit of boilerplate, then print it *)

open Utils
open PPrint

let mk_includes =
  separate_map hardline (fun x -> string "#include " ^^ string x)

let filter_includes file includes =
  KList.filter_some (List.rev_map (function
    | Some file', h when file = file' -> Some h
    | None, h -> Some h
    | _ -> None
  ) includes)

let kremlib_include () =
  if !Options.minimal then
    empty
  else
    mk_includes [ "\"kremlib.h\"" ]

(* A Pprint document with:
 * - #include X for X in the dependencies of the file, followed by
 * - #include Y for each -add-include Y passed on the command-line
 *)
let includes_for file files =
  let extra_includes = mk_includes (filter_includes file !Options.add_include) in
  let includes = mk_includes (List.rev_map (Printf.sprintf "\"%s.h\"") files) in
  separate hardline [ includes; extra_includes ]

let invocation (): string =
  KPrint.bsprintf
{|
  This file was generated by KreMLin <https://github.com/FStarLang/kremlin>
  KreMLin invocation: %s
  F* version: %s
  KreMLin version: %s
|}
    (String.concat " " (Array.to_list Sys.argv))
    !Driver.fstar_rev
    !Driver.krml_rev

let header (): string =
  let default = invocation () in
  if !Options.header = "" then
    "/* " ^ default ^ " */"
  else
    let fmt = Utils.file_get_contents !Options.header in
    try
      let fmt = Scanf.format_from_string fmt "%s" in
      KPrint.bsprintf fmt default
    with Scanf.Scan_failure _ ->
      fmt

(* A pair of a header, containing:
 * - the boilerplate specified on the command-line by -header
 * - #include Y for each -add-early-include Y passed on the command-line
 * - #include "kremlib.h"
 * - the #ifndef #define guard,
 * and a footer, containing:
 * - the #endif
 *)
let prefix_suffix name =
  Driver.detect_fstar_if ();
  Driver.detect_kremlin_if ();
  let if_cpp doc =
    string "#if defined(__cplusplus)" ^^ hardline ^^
    doc ^^ hardline ^^
    string "#endif" ^^ hardline
  in
  let prefix =
    string (header ()) ^^ hardline ^^
    (if !Options.extern_c then hardline ^^ if_cpp (string "extern \"C\" {") ^^ hardline else empty) ^^
    mk_includes (filter_includes name !Options.add_early_include) ^^ hardline ^^
    kremlib_include () ^^ hardline ^^ hardline ^^
    string (Printf.sprintf "#ifndef __%s_H" name) ^^ hardline ^^
    string (Printf.sprintf "#define __%s_H" name) ^^ hardline
  in
  let suffix =
    hardline ^^
    string (Printf.sprintf "#define __%s_H_DEFINED" name) ^^ hardline ^^
    string "#endif" ^^
    (if !Options.extern_c then hardline ^^ hardline ^^ if_cpp (string "}") else empty)
  in
  prefix, suffix

let in_tmp_dir name =
  Driver.mk_tmpdir_if ();
  let open Driver in
  if !Options.tmpdir <> "" then
    !Options.tmpdir ^^ name
  else
    name

let write_one name prefix program suffix =
  with_open_out_bin (in_tmp_dir name) (fun oc ->
    let doc =
      prefix ^^
      separate_map (hardline ^^ hardline) PrintC.p_decl_or_function program ^^
      hardline ^^
      suffix ^^ hardline
    in
    PPrint.ToChannel.pretty 0.95 100 oc doc
  )

let write_c files =<commit_msg>Revert "Revert "Fix the position of the extern declarations (again). This fixes project-everest/hacl-star#337""<commit_after>(* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
(* Licensed under the Apache 2.0 License. *)

(** Decorate each file with a little bit of boilerplate, then print it *)

open Utils
open PPrint

let mk_includes =
  separate_map hardline (fun x -> string "#include " ^^ string x)

let filter_includes file includes =
  KList.filter_some (List.rev_map (function
    | Some file', h when file = file' -> Some h
    | None, h -> Some h
    | _ -> None
  ) includes)

let kremlib_include () =
  if !Options.minimal then
    empty
  else
    mk_includes [ "\"kremlib.h\"" ] ^^ hardline

(* A Pprint document with:
 * - #include X for X in the dependencies of the file, followed by
 * - #include Y for each -add-include Y passed on the command-line
 *)
let includes_for file files =
  let extra_includes = mk_includes (filter_includes file !Options.add_include) in
  let includes = mk_includes (List.rev_map (Printf.sprintf "\"%s.h\"") files) in
  separate hardline [ includes; extra_includes ]

let invocation (): string =
  KPrint.bsprintf
{|
  This file was generated by KreMLin <https://github.com/FStarLang/kremlin>
  KreMLin invocation: %s
  F* version: %s
  KreMLin version: %s
|}
    (String.concat " " (Array.to_list Sys.argv))
    !Driver.fstar_rev
    !Driver.krml_rev

let header (): string =
  let default = invocation () in
  if !Options.header = "" then
    "/* " ^ default ^ " */"
  else
    let fmt = Utils.file_get_contents !Options.header in
    try
      let fmt = Scanf.format_from_string fmt "%s" in
      KPrint.bsprintf fmt default
    with Scanf.Scan_failure _ ->
      fmt

(* A pair of a header, containing:
 * - the boilerplate specified on the command-line by -header
 * - #include Y for each -add-early-include Y passed on the command-line
 * - #include "kremlib.h"
 * - the #ifndef #define guard,
 * and a footer, containing:
 * - the #endif
 *)
let prefix_suffix name =
  Driver.detect_fstar_if ();
  Driver.detect_kremlin_if ();
  let if_cpp doc =
    string "#if defined(__cplusplus)" ^^ hardline ^^
    doc ^^ hardline ^^
    string "#endif" ^^ hardline
  in
  let prefix =
    string (header ()) ^^ hardline ^^ hardline ^^
    string (Printf.sprintf "#ifndef __%s_H" name) ^^ hardline ^^
    string (Printf.sprintf "#define __%s_H" name) ^^ hardline ^^
    (if !Options.extern_c then hardline ^^ if_cpp (string "extern \"C\" {") ^^ hardline else empty) ^^
    mk_includes (filter_includes name !Options.add_early_include) ^^ hardline ^^
    kremlib_include () ^^ hardline
  in
  let suffix =
    hardline ^^
    (if !Options.extern_c then if_cpp (string "}") else empty) ^^ hardline ^^
    string (Printf.sprintf "#define __%s_H_DEFINED" name) ^^ hardline ^^
    string "#endif"
  in
  prefix, suffix

let in_tmp_dir name =
  Driver.mk_tmpdir_if ();
  let open Driver in
  if !Options.tmpdir <> "" then
    !Options.tmpdir ^^ name
  else
    name

let write_one name prefix program suffix =
  with_open_out_bin (in_tmp_dir name) (fun oc ->
    let doc =
      prefix ^^
      separate_map (hardline ^^ hardline) PrintC.p_decl_or_function program ^^
      hardline ^^
      suffix ^^ hardline
    in
    PPrint.ToChannel.pretty 0.95 100 oc doc
  )

let write_c files =
{'fraction_non_alphanumeric': 0.11635315533980582, 'fraction_numerical': 0.0028822815533980583, 'mean_word_length': 3.212779552715655, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 19, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1944887', 'n_tokens_mistral': 2240, 'n_tokens_neox': 2217, 'n_words': 684}