]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/experiment.ml
Requires and Provides now fixed
[helm.git] / 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();;