]> matita.cs.unibo.it Git - helm.git/blob - helm/graphs/tools/uri_set_queue.cgi
BU_Conversion + omit-conclusion is a mess. I have partially fixed the
[helm.git] / helm / graphs / tools / uri_set_queue.cgi
1 #!/usr/bin/perl
2
3 use HTTP::Daemon;
4 use HTTP::Status;
5 use HTTP::Response;
6 use CGI;
7
8 $urisetqueueport = $ENV{'URI_SET_QUEUE_PORT'} || $urisetqueueport;
9
10 my $d = new HTTP::Daemon LocalPort => $urisetqueueport
11  or die "Error: port $urisetqueueport not available.";
12 print "Please contact me at: <URL:", $d->url, ">\n";
13
14 $SIG{CHLD} = "IGNORE"; # do not accumulate defunct processes
15
16 my %uri_sets;
17 my %uri_queues;
18 my %overflowed;
19 my %size;
20
21 #NOT REENTRANT: CAN NOT FORK DUE TO THE GLOBAL VARIABLES %uri_sets & ...
22 #HENCE, THE "PID" ARGUMENT OF EVERY REQUEST MUST IDENTIFY THE SET OF URI
23 #IT WANTS TO WORK WITH. MOREOVER, EVERY CLIENT MUST WORK WITH A DIFFERENT SET
24 #OF URI, I.E. EVERY PID MUST BE UNIQUE.
25
26 #CSC: WHAT IF THE CLIENTS ARE ON DIFFERENT MACHINES AND HAVE THE SAME PID?
27
28 while (my $c = $d->accept) {
29     while (my $r = $c->get_request) {
30         if ($r->method eq 'GET' and $r->url->path eq '/add_if_not_in') {
31             my $http_query = $r->url->equery;
32             my $cgi = new CGI("$http_query");
33             my $uri = $cgi->param('uri');
34             my $pid = $cgi->param('PID');
35             print "$pid: ";
36             print(@{$uri_queues{$pid}} + 0);
37             print "/";
38             my $tot = keys(%{$uri_sets{$pid}}) + 0;
39             $tot .= "*" if defined($overflowed{$pid});
40             print "$tot $uri: ";
41
42             my $res;
43             if (!(defined($uri_sets{$pid}->{$uri}))) {
44                 if ($tot + 1 > $size{$pid}) {
45                    $res = "not_added_because_already_too_many";
46                    $overflowed{$pid} = 1;
47                 } else {
48                    $uri_sets{$pid}->{$uri} = 1;
49                    push @{$uri_queues{$pid}},$uri;
50                    $res = "added";
51                 }
52             } else {
53                 $res = "already_in";
54             }
55             print $res."\n";
56
57             my $response = new HTTP::Response;
58             $response->content("<?xml version=\"1.0\"?>\n<$res/>\n");
59             $response->content_type('text/xml');
60             $c->send_response($response);
61         } elsif ($r->method eq 'GET' and $r->url->path eq '/is_overflowed') {
62             my $http_query = $r->url->equery;
63             my $cgi = new CGI("$http_query");
64             my $pid = $cgi->param('PID');
65             print "$pid: ";
66             print(@{$uri_queues{$pid}} + 0);
67             print "/";
68             print(keys(%{$uri_sets{$pid}}) + 0);
69             print "*" if defined($overflowed{$pid});
70             my $res = defined($overflowed{$pid}) ? "true" : "false";
71             print " is_overflowed: $res\n";
72             my $response = new HTTP::Response;
73             $response->content("<?xml version=\"1.0\"?>\n<$res/>\n");
74             $response->content_type('text/xml');
75             $c->send_response($response);
76         } elsif ($r->method eq 'GET' and $r->url->path eq '/set_uri_set_size') {
77             my $http_query = $r->url->equery;
78             my $cgi = new CGI("$http_query");
79             my $pid = $cgi->param('PID');
80             my $size = $cgi->param('size');
81             print "$pid: size := $size\n";
82             $size{$pid} = $size;
83             my $response = new HTTP::Response;
84             $response->content("<?xml version=\"1.0\"?>\n<done/>\n");
85             $response->content_type('text/xml');
86             $c->send_response($response);
87         } elsif ($r->method eq 'GET' and $r->url->path eq '/get_next') {
88             my $http_query = $r->url->equery;
89             my $cgi = new CGI("$http_query");
90             my $pid = $cgi->param('PID');
91             print "$pid: ";
92             print(@{$uri_queues{$pid}} + 0);
93             print "/";
94             print(keys(%{$uri_sets{$pid}}) + 0);
95             print "*" if defined($overflowed{$pid});
96             print " ";
97
98             my $elem = shift @{$uri_queues{$pid}};
99             my $mark = $overflowed{$pid};
100
101             my $response = new HTTP::Response;
102             my $xml_header = "<?xml version=\"1.0\"?>\n";
103             if (!defined($elem)) {
104                print "is now empty\n";
105                $response->content("$xml_header<empty/>\n");
106             } elsif ($mark == 1) {
107                print "$elem (marked) removed\n";
108                $response->content("$xml_header<marked_uri value=\"$elem\"/>\n");
109             } else {
110                print "$elem removed\n";
111                $response->content("$xml_header<uri value=\"$elem\"/>\n");
112             }
113             $response->content_type('text/xml');
114             $c->send_response($response);
115         } elsif ($r->method eq 'GET' and $r->url->path eq '/reset_to_empty') {
116             my $pid = $r->url->query;
117             $pid =~ s/[^=]*=//;
118             # Next loop for debugging purposes only
119             my $count = 1;
120             while (my $e = shift @{$uri_queues{$pid}}) {
121              print "#$count $e forced out of the set\n";
122              $count++;
123             }
124             print "************\nThe URI set $pid is now empty again\n";
125             delete($uri_sets{$pid});
126             delete($overflowed{$pid});
127             delete($size{$pid});
128             my $response = new HTTP::Response;
129             $response->content("<?xml version=\"1.0\"?>\n<done/>\n");
130             $response->content_type('text/xml');
131             $c->send_response($response);
132         } elsif ($r->method eq 'GET' && $r->url->path eq "/help"){
133            print "Help requested!\n";
134            my $response = new HTTP::Response;
135            $response->content("URI-Set (Queue) Version: ???");
136            $c->send_response($response);
137         } else {
138             $c->send_error(RC_FORBIDDEN)
139         }
140     }
141     $c->close;
142     undef($c);
143 }