val maybe_external_types_krml (g: Deps.dep_graph) (m: string) : Tot (list string)
let maybe_external_types_krml
  (g: Deps.dep_graph)
  (m: string)
: Tot (list string)
= if has_external_types_fsti g m
  then [mk_filename (Printf.sprintf "%s_ExternalTypes" m) "krml"]
  else []
val maybe_external_types_krml (g: Deps.dep_graph) (m: string) : Tot (list string)
let maybe_external_types_krml (g: Deps.dep_graph) (m: string) : Tot (list string) =
if has_external_types_fsti g m
then [mk_filename (Printf.sprintf "%s_ExternalTypes" m) "krml"]
else []
GenMakefile.fst.checked
prims.fst.checked OS.fsti.checked Options.fsti.checked HashingOptions.fst.checked FStar.String.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked Deps.fsti.checked
GenMakefile.fst
Deps.dep_graph Prims.string GenMakefile.has_external_types_fsti Prims.Cons GenMakefile.mk_filename FStar.Printf.sprintf Prims.Nil Prims.bool Prims.list
module GenMakefile
module OS = OS

type rule_type =
  | EverParse
  | CC
  | Nop (* to simulate multiple-target rules *)

type rule_t = {
  ty: rule_type;
  from: list string;
  to: string;
  args: string;
}

let input_dir = "$(EVERPARSE_INPUT_DIR)"
let output_dir = "$(EVERPARSE_OUTPUT_DIR)"

let print_gnu_make_rule
  input_stream_binding
  (r: rule_t)
: Tot string
= 
  let rule = Printf.sprintf "%s : %s\n" r.to (String.concat " " r.from) in
  match r.ty with
  | Nop -> Printf.sprintf "%s\n" rule
  | _ ->
    let cmd =
      match r.ty with
      | EverParse -> Printf.sprintf "$(EVERPARSE_CMD) --odir %s" output_dir
      | CC ->
        let ddd_home = "$(EVERPARSE_HOME)" `OS.concat` "src" `OS.concat` "3d" in
        let ddd_actions_home = ddd_home `OS.concat` "prelude" `OS.concat` (HashingOptions.string_of_input_stream_binding input_stream_binding) in
        Printf.sprintf "$(CC) $(CFLAGS) -I %s -I %s -c" ddd_home ddd_actions_home
    in
    let rule = Printf.sprintf "%s\t%s %s\n\n" rule cmd r.args in
    rule

let mk_input_filename
  (file: string)
: Tot string
= input_dir `OS.concat` OS.basename file

let mk_filename
  (modul: string)
  (ext: string)
: Tot string
= output_dir `OS.concat` (Printf.sprintf "%s.%s" modul ext)

let add_cfg_file_dep ext deps
  : FStar.All.ML (list string)
  = match Options.config_module_name () with
    | None -> deps
    | Some module_name -> deps `List.Tot.append` [mk_filename module_name ext]
  
let produce_config_fst_file_rule ()
: FStar.All.ML (list rule_t)
= match Options.config_module_name (), Options.get_config_file() with
  | Some module_name, Some cfg_file_name ->
    let fst_file_name = mk_filename module_name "fst" in
    let checked_file_name = mk_filename module_name "fst.checked" in
    let krml_file_name = mk_filename module_name "krml" in
    let fst_rule = {
      ty = EverParse;
      from = [cfg_file_name];
      to = fst_file_name;
      args = "--__micro_step emit_config"
    } in
    let fst_checked_rule = {
      ty = EverParse;
      from = [fst_file_name];
      to =  checked_file_name;
      args = Printf.sprintf "--__micro_step verify %s" fst_file_name;
    } in
    let krml_rule = {
      ty = EverParse;
      from = [checked_file_name];
      to =  krml_file_name;
      args = Printf.sprintf "--__micro_step extract %s" fst_file_name;        
    } in
    [fst_rule; fst_checked_rule; krml_rule]
  | _ -> []

let has_external_types_fsti
  (g: Deps.dep_graph)
  (modul: string)
: Tot bool
= 
  (Deps.has_output_types g modul ||
    Deps.has_extern_types g modul)

let maybe_external_types_fsti_checked
  (g: Deps.dep_graph)
  (modul: string)
: Tot (list string)
= if has_external_types_fsti g modul
  then [mk_filename modul "ExternalTypes.fsti.checked"]
  else []

let has_external_api_fsti
  (g: Deps.dep_graph)
  (modul: string)
: Tot bool
=
  Deps.has_out_exprs g modul ||
  Deps.has_extern_types g modul ||
  Deps.has_extern_functions g modul

let produce_external_api_fsti_checked_rule
  (g: Deps.dep_graph)
  (modul: string)
: list rule_t
= if not (has_external_api_fsti g modul) then []
  else
    let external_api_fsti = mk_filename modul "ExternalAPI.fsti" in
    [{
       ty = EverParse;
       from = external_api_fsti :: (maybe_external_types_fsti_checked g modul `List.Tot.append` List.Tot.map (fun m -> mk_filename m "fsti.checked") (Deps.dependencies g modul));
       to = mk_filename modul "ExternalAPI.fsti.checked";
       args = Printf.sprintf "--__micro_step verify %s" external_api_fsti;
     }]

let produce_external_types_fsti_checked_rule
  (g: Deps.dep_graph)
  (modul: string)
: list rule_t
= if not (has_external_types_fsti g modul) then []
  else
    let external_types_fsti = mk_filename modul "ExternalTypes.fsti" in 
    [{
       ty = EverParse;
       from = external_types_fsti :: List.Tot.map (fun m -> mk_filename m "ExternalTypes.fsti.checked") (Deps.dependencies g modul);
       to = mk_filename modul "ExternalTypes.fsti.checked";
       args = Printf.sprintf "--__micro_step verify %s" external_types_fsti;
     }]

let maybe_external_api_fsti_checked
  (g: Deps.dep_graph)
  (modul: string)
: Tot (list string)
= if has_external_api_fsti g modul
  then [mk_filename modul "ExternalAPI.fsti.checked"]
  else []

let external_deps
  (g: Deps.dep_graph)
  (modul: string)
: Tot (list string)
= maybe_external_types_fsti_checked g modul `List.Tot.append`
  maybe_external_api_fsti_checked g modul

let produce_fsti_checked_rule
  (g: Deps.dep_graph)
  (modul: string)
: Tot rule_t
= let fsti = mk_filename modul "fsti" in
  {
    ty = EverParse;
    from = fsti :: (external_deps g modul `List.Tot.append` List.Tot.map (fun m -> mk_filename m "fsti.checked") (Deps.dependencies g modul));
    to = mk_filename modul "fsti.checked";
    args = Printf.sprintf "--__micro_step verify %s" fsti;
  }

let produce_fst_checked_rule
  (g: Deps.dep_graph)
  (modul: string)
: FStar.All.ML rule_t
= let fst = mk_filename modul "fst" in
  {
    ty = EverParse;
    from = add_cfg_file_dep "fst.checked" (fst :: mk_filename modul "fsti.checked" :: List.Tot.map (fun m -> mk_filename m "fsti.checked") (Deps.dependencies g modul));
    to = mk_filename modul "fst.checked";
    args = Printf.sprintf "--__micro_step verify %s" fst;
  }

let produce_external_types_krml_rule
  (g: Deps.dep_graph)
  (modul: string)
: list rule_t
= if not (has_external_types_fsti g modul) then []
  else
    let external_types_fsti_checked = mk_filename modul "ExternalTypes.fsti.checked" in 
    [{
       ty = EverParse;
       from = external_types_fsti_checked :: List.Tot.map (fun m -> mk_filename m "fst.checked") (Deps.dependencies g modul);
       to = mk_filename (Printf.sprintf "%s_ExternalTypes" modul) "krml";
       args = Printf.sprintf "--__micro_step extract %s" (mk_filename modul "ExternalTypes.fsti");
     }]

let produce_external_api_krml_rule
  (g: Deps.dep_graph)
  (modul: string)
: list rule_t
= if not (has_external_api_fsti g modul) then []
  else
    let external_api_fsti_checked = mk_filename modul "ExternalAPI.fsti.checked" in 
    [{
       ty = EverParse;
       from = external_api_fsti_checked :: List.Tot.map (fun m -> mk_filename m "fst.checked") (Deps.dependencies g modul);
       to = mk_filename (Printf.sprintf "%s_ExternalAPI" modul) "krml";
       args = Printf.sprintf "--__micro_step extract %s" (mk_filename modul "ExternalAPI.fsti");
     }]

let produce_krml_rule
  (g: Deps.dep_graph)
  (modul: string)
: FStar.All.ML rule_t
=
  {
    ty = EverParse;
    from = add_cfg_file_dep "fst.checked" 
            (mk_filename modul "fst.checked" :: 
              List.Tot.map (fun m -> mk_filename m "fst.checked") (Deps.dependencies g modul));
    to = mk_filename modul "krml";
    args = Printf.sprintf "--__micro_step extract %s" (mk_filename modul "fst");
  }

let produce_nop_rule
  (from: list string)
  (to: string)
: Tot rule_t
=
  {
    ty = Nop;
    from = from;
    to = to;
    args = "";
  }

let maybe_external_typedefs_h
  (emit_output_types_defs: bool)
  (g:Deps.dep_graph)
  (modul: string)
: Tot (list string)
= if (Deps.has_output_types g modul && not (Deps.has_extern_types g modul)) && emit_output_types_defs
  then [mk_filename (Printf.sprintf "%s_ExternalTypedefs" modul) "h"]
  else []

let produce_fst_rules
  (emit_output_types_defs: bool)
  (g: Deps.dep_graph)
  (clang_format: bool)
  (file: string)
: FStar.All.ML (list rule_t)
=
  let modul = Options.get_module_name file in
  (* follow the order prescribed by Main.process_file *)
  (* fst* files generated by 3d (cf. Main.emit_fstar_code_for_interpreter) *)
  let first_fst :: other_fst =
    begin
      if has_external_types_fsti g modul
      then [mk_filename modul "ExternalTypes.fsti"]
      else []
    end `List.Tot.append`
    begin
      if has_external_api_fsti g modul
      then [mk_filename modul "ExternalAPI.fsti"]
      else []
    end `List.Tot.append`
      [
        mk_filename modul "fst";
        mk_filename modul "fsti";
      ]
  in
  (* C files generated by 3d (as opposed to F*, cf. Main.emit_entrypoint) *)
  let produced_c =
    begin
      if Deps.has_entrypoint g modul
      then
        [
          mk_filename (Printf.sprintf "%sWrapper" modul) "c";
          mk_filename (Printf.sprintf "%sWrapper" modul) "h";
        ]
      else []
    end `List.Tot.append`
    begin
      if emit_output_types_defs
      then
        if Deps.has_output_types g modul
        then
          mk_filename (Printf.sprintf "%s_OutputTypesDefs" modul) "h" ::
          begin
            if not (Deps.has_extern_types g modul)
            then [mk_filename (Printf.sprintf "%s_ExternalTypedefs" modul) "h"]
            else []
          end
        else []
      else []
    end `List.Tot.append`
    begin
      if Deps.has_out_exprs g modul
      then [mk_filename (Printf.sprintf "%s_OutputTypes" modul) "c"]
      else []
    end `List.Tot.append`
    begin
      if Deps.has_static_assertions g modul
      then [mk_filename (Printf.sprintf "%sStaticAssertions" modul) "c"]
      else []
    end
  in
  (* produce the actual rules *)
    {
      ty = EverParse;
      from =
        (if clang_format then [mk_filename "" "clang-format"] else []) `List.Tot.append`
        (if OS.file_exists (Printf.sprintf "%s.copyright.txt" file) then [mk_input_filename (Printf.sprintf "%s.copyright.txt" file)] else []) `List.Tot.append`
        [mk_input_filename file];
      to = first_fst;
      args = Printf.sprintf "--no_batch %s" (mk_input_filename file);
    } ::
    List.Tot.map (produce_nop_rule [first_fst]) (other_fst `List.Tot.append` produced_c)

let maybe_external_api_krml
  (g: Deps.dep_graph)
  (m: string)
: Tot (list string)
= if has_external_api_fsti g m
  then [mk_filename (Printf.sprintf "%s_ExternalAPI" m) "krml"]
  else []

let maybe_external_types_krml
  (g: Deps.dep_graph)
  (m: string)
val maybe_external_types_krml (g: Deps.dep_graph) (m: string) : Tot (list string)
g: Deps.dep_graph -> m: Prims.string -> Prims.list Prims.string