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