helm/interface/experiment.ml

   1 (******************************************************************************)
   2 (*                                                                            *)
   3 (*                               PROJECT HELM                                 *)
   4 (*                                                                            *)
   5 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
   6 (*                                 24/01/2000                                 *)
   7 (*                                                                            *)
   8 (* This is a textual interface to the Coq-like pretty printer cicPp for cic   *)
   9 (* terms exported in xml. It uses directly the modules cicPp and cache and    *)
  10 (* indirectly all the other modules (cicParser, cicParser2, cicParser3,       *)
  11 (* getter). The syntax is  "experiment[.opt] filename1 ... filenamen" where   *)
  12 (* filenamei is the path-name of an xml file describing a cic term. On stdout *)
  13 (* are pretty-printed all the n terms                                         *)
  14 (*                                                                            *)
  15 (******************************************************************************)
  16
  17 let pretty_print    = ref true;;
  18 let read_from_stdin = ref false;;
  19 let uris_in_input   = ref false;;
  20
  21 let parse uri =
  22  if !pretty_print then
  23   begin
  24    print_endline ("^^^" ^ uri ^ "^^^") ;
  25    print_string (CicPp.ppobj (CicCache.get_obj (UriManager.uri_of_string uri)));
  26    print_endline ("\n$$$" ^ uri ^ "$$$\n")
  27   end
  28  else
  29   begin
  30    print_string uri ;
  31    let _ = CicCache.get_obj  (UriManager.uri_of_string uri) in
  32     print_endline " OK!" ;
  33     flush stdout
  34   end
  35 ;;
  36
  37 let uri_of_filename fn =
  38  if !uris_in_input then fn
  39  else
  40   let uri =
  41    Str.replace_first (Str.regexp (Str.quote Configuration.helm_dir)) "cic:" fn
  42   in
  43    let uri' = Str.replace_first (Str.regexp "\.xml$") "" uri in
  44     uri'
  45 ;;
  46
  47 let read_filenames_from_stdin () =
  48  let files = ref [] in
  49   try
  50    while true do
  51     let l = Str.split (Str.regexp " ") (read_line ()) in
  52      List.iter (fun x -> files := (uri_of_filename x) :: !files) l
  53    done
  54   with
  55    End_of_file ->
  56     files := List.rev !files ;
  57     List.iter parse !files
  58 ;;
  59
  60 (* filenames are read from command line and converted to uris via *)
  61 (* uri_of_filenames; then the cic terms are load in cache via     *)
  62 (* CicCache.get_obj  and then pretty printed via CicPp.ppobj      *)
  63
  64 let main() =
  65   let files = ref [] in
  66   Arg.parse
  67    ["-nopp", Arg.Clear pretty_print, "Do not pretty print, parse only" ;
  68     "-stdin", Arg.Set read_from_stdin, "Read from stdin" ;
  69     "-uris", Arg.Set uris_in_input, "Read uris, not filenames" ;
  70     "-update", Arg.Unit Getter.update, "Update the getter view of the world"]
  71    (fun x -> files := (uri_of_filename x) :: !files)
  72    "
  73 usage: experiment file ...
  74
  75 List of options:";
  76   if !read_from_stdin then read_filenames_from_stdin ()
  77   else
  78    begin
  79     files := List.rev !files;
  80     List.iter parse !files
  81    end
  82 ;;
  83
  84 main();;