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   let status,_ =
  14    map_status status
  15     (fun status ml ->
  16       let status,cmds = Ocaml.pp_decl status ml in
  17       print_ppcmds ~in_ml:true status (cmds ++ fnl () ++ fnl ());
  18       status,()) res in
  19   status
  20  with
  21     HExtlib.Localized (_,exn)
  22   | exn ->
  23      prerr_endline (Printexc.to_string exn); assert false
  24
  25 let do_if_ocaml_set f status =
  26  if try ignore (Helm_registry.get "extract_ocaml"); true
  27     with Helm_registry.Key_not_found _ -> false
  28  then f status else status
  29
  30 let print_open status uris =
  31  do_if_ocaml_set
  32   (fun status ->
  33     let status,uris =
  34      map_status status
  35       (fun status uri ->
  36         let status,b = to_be_included status uri in
  37          status, if b then Some uri else None
  38       ) uris in
  39     let uris = HExtlib.filter_map (fun x -> x) uris in
  40     let fnames =
  41      List.map (fun uri -> Filename.basename (NUri.string_of_uri uri)) uris in
  42     let status,cmds = map_status status Ocaml.pp_open fnames in
  43     List.iter (print_ppcmds status ~in_ml:true) cmds;
  44     List.iter (print_ppcmds status ~in_ml:false) cmds;
  45     status
  46   ) status
  47
  48 let print_ocaml_of_obj status cmds =
  49  do_if_ocaml_set (fun status -> print_ocaml_of_obj0 status cmds) status
  50
  51 let open_file status ~baseuri fname =
  52  do_if_ocaml_set
  53   (fun status -> OcamlExtractionTable.open_file status ~baseuri fname) status
  54
  55 let close_file status =
  56  do_if_ocaml_set OcamlExtractionTable.close_file status