matita/components/ng_extraction/ocamlExtraction.ml

   1 open OcamlExtractionTable
   2 open Coq
   3
   4 let print_ocaml_of_obj0 status ((_uri,_,_,_,_) as obj) =
   5  try
   6   let status,res,resl = Extraction.extract status obj in
   7   let status,_ =
   8    map_status status
   9     (fun status ml ->
  10       let status,cmds = Ocaml.pp_spec status ml in
  11       print_ppcmds ~in_ml:false status (cmds ++ fnl () ++ fnl ());
  12       status,()) resl in
  13   match res with
  14      None ->
  15 (*    print_ppcmds status
  16        (str("(* " ^ NUri.string_of_uri uri ^ " non informative *)\n")++ fnl ());*)
  17       status
  18    | Some ml ->
  19       let status,std_ppcmds = Ocaml.pp_decl status ml in
  20       print_ppcmds status ~in_ml:true (std_ppcmds ++ fnl ());
  21       status
  22  with
  23   HExtlib.Localized (_,exn) ->
  24    prerr_endline (Printexc.to_string exn); assert false
  25
  26 let do_if_ocaml_set f status =
  27  if try ignore (Helm_registry.get "extract_ocaml"); true
  28     with Helm_registry.Key_not_found _ -> false
  29  then f status else status
  30
  31 let print_open status uris =
  32  do_if_ocaml_set
  33   (fun status ->
  34     let status,uris =
  35      map_status status
  36       (fun status uri ->
  37         let status,b = to_be_included status uri in
  38          status, if b then Some uri else None
  39       ) uris in
  40     let uris = HExtlib.filter_map (fun x -> x) uris in
  41     let fnames =
  42      List.map (fun uri -> Filename.basename (NUri.string_of_uri uri)) uris in
  43     let status,cmds = map_status status Ocaml.pp_open fnames in
  44     List.iter (print_ppcmds status ~in_ml:true) cmds;
  45     List.iter (print_ppcmds status ~in_ml:false) cmds;
  46     status
  47   ) status
  48
  49 let print_ocaml_of_obj status cmds =
  50  do_if_ocaml_set (fun status -> print_ocaml_of_obj0 status cmds) status
  51
  52 let open_file status ~baseuri fname =
  53  do_if_ocaml_set
  54   (fun status -> OcamlExtractionTable.open_file status ~baseuri fname) status
  55
  56 let close_file status =
  57  do_if_ocaml_set OcamlExtractionTable.close_file status