]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/searchEngine.ml
- new generated query "unreferred" implemented at server side
[helm.git] / helm / searchEngine / searchEngine.ml
1 (* Copyright (C) 2002, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 module T = MQGTypes
27 module U = MQGUtil
28 module G = MQueryGenerator
29 module C = MQIConn
30
31 open Http_types ;;
32
33 let debug = true;;
34 let debug_print s = if debug then prerr_endline s;;
35 Http_common.debug := true;;
36 (* Http_common.debug := true;; *)
37
38   (** accepted HTTP servers for ask_uwobo method forwarding *)
39 let valid_servers =
40  [ "mowgli.cs.unibo.it:58080" ; "mowgli.cs.unibo.it" ; "localhost:58080" ];;
41
42 let mqi_flags = [] (* default MathQL interpreter options *)
43
44 open Printf;;
45
46 let daemon_name = "Search Engine";;
47 let default_port = 58085;;
48 let port_env_var = "SEARCH_ENGINE_PORT";;
49
50 let pages_dir =
51   try
52     Sys.getenv "SEARCH_ENGINE_HTML_DIR"
53   with Not_found -> "html"  (* relative to searchEngine's document root *)
54 ;;
55 let interactive_user_uri_choice_TPL = pages_dir ^ "/templateambigpdq1.html";;
56 let interactive_interpretation_choice_TPL =
57   pages_dir ^ "/templateambigpdq2.html";;
58 let constraints_choice_TPL = pages_dir ^ "/constraints_choice_template.html";;
59 let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";;
60
61 exception Chat_unfinished
62
63   (* build a bool from a 1-character-string *)
64 let bool_of_string' = function
65   | "0" -> false
66   | "1" -> true
67   | s -> failwith ("Can't parse a boolean from string: " ^ s)
68 ;;
69
70   (* build an int option from a string *)
71 let int_of_string' = function
72   | "_" -> None
73   | s ->
74       try
75         Some (int_of_string s)
76       with Failure "int_of_string" ->
77         failwith ("Can't parse an int option from string: " ^ s)
78 ;;
79
80   (* HTML pretty printers for mquery_generator types *)
81
82 let html_of_r_obj (pos, uri) =
83   sprintf
84     "<tr><td><input type='checkbox' name='constr_obj' checked='on'/></td><td>%s</td><td>%s</td><td>%s</td></tr>"
85     uri (U.text_of_position pos)
86     (if U.is_main_position pos then
87       sprintf "<input name='obj_depth' size='2' type='text' value='%s' />"
88         (U.text_of_depth pos "")
89     else
90       "<input type=\"hidden\" name=\"obj_depth\" />")
91 ;;
92
93 let html_of_r_rel pos =
94   sprintf
95     "<tr><td><input type='checkbox' name='constr_rel' checked='on'/></td><td>%s</td><td><input name='rel_depth' size='2' type='text' value='%s' /></td></tr>"
96     (U.text_of_position (pos:>T.full_position)) (U.text_of_depth (pos:>T.full_position) "")
97 ;;
98
99 let html_of_r_sort (pos, sort) =
100   sprintf
101     "<tr><td><input type='checkbox' name='constr_sort' checked='on'/></td><td>%s</td><td>%s</td><td><input name='sort_depth' size='2' type='text' value='%s'/></td></tr>"
102     (U.text_of_sort sort) (U.text_of_position (pos:>T.full_position)) (U.text_of_depth (pos:>T.full_position) "")
103 ;;
104
105   (** pretty print a MathQL query result to an HELM theory file *)
106 let theory_of_result result =
107  let results_no = List.length result in
108   if results_no > 0 then
109    let mode = if results_no > 10 then "linkonly" else "typeonly" in
110    let results =
111     let idx = ref (results_no + 1) in
112      List.fold_right
113       (fun (uri,attrs) i ->
114         decr idx ;
115         "<tr><td valign=\"top\">" ^ string_of_int !idx ^ ".</td><td><ht:OBJECT uri=\"" ^ uri ^ "\" mode=\"" ^ mode ^ "\"/></td></tr>" ^  i
116       ) result ""
117    in
118     "<h1>Query Results:</h1><table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">" ^ results ^ "</table>"
119   else
120     "<h1>Query Results:</h1><p>No results found!</p>"
121 ;;
122
123 let pp_result result =
124  "<html xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">\n<head><title>Query Results</title><style> A { text-decoration: none } </style></head>\n<body>" ^ theory_of_result result ^ "</body></html>"
125 ;;
126
127   (** chain application of Pcre substitutions *)
128 let rec apply_substs substs line =
129   match substs with
130   | [] -> line
131   | (rex, templ) :: rest -> apply_substs rest (Pcre.replace ~rex ~templ line)
132   (** fold like function on files *)
133 let fold_file f init fname =
134   let inchan = open_in fname in
135   let rec fold_lines' value =
136     try 
137       let line = input_line inchan in 
138       fold_lines' (f value line)
139     with End_of_file -> value
140   in
141   let res = (try fold_lines' init with e -> (close_in inchan; raise e)) in
142   close_in inchan;
143   res
144   (** iter like function on files *)
145 let iter_file f = fold_file (fun _ line -> f line) ()
146
147 let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE,
148     interpretations_RE, interpretations_labels_RE, results_RE, new_aliases_RE,
149     form_RE, variables_initialization_RE)
150   =
151   (Pcre.regexp "@TITLE@", Pcre.regexp "@CHOICES@", Pcre.regexp "@MSG@",
152   Pcre.regexp "@ID_TO_URIS@", Pcre.regexp "@ID@",
153   Pcre.regexp "@INTERPRETATIONS@", Pcre.regexp "@INTERPRETATIONS_LABELS@",
154   Pcre.regexp "@RESULTS@", Pcre.regexp "@NEW_ALIASES@", Pcre.regexp "@FORM@",
155   Pcre.regexp "@VARIABLES_INITIALIZATION@")
156 let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$"
157
158 exception NotAnInductiveDefinition
159
160 let port =
161   try
162     int_of_string (Sys.getenv port_env_var)
163   with
164   | Not_found -> default_port
165   | Failure "int_of_string" ->
166       prerr_endline "Warning: invalid port, reverting to default";
167       default_port
168 ;;
169
170 let pp_error = sprintf "<html><body><h1>Error: %s</h1></body></html>";;
171
172 let bad_request body outchan =
173   Http_daemon.respond_error ~status:(`Client_error `Bad_request) ~body outchan
174 ;;
175
176 let contype = "Content-Type", "text/html";;
177
178 (* SEARCH ENGINE functions *)
179
180 let refine_constraints ((constr_obj:T.r_obj list), (constr_rel:T.r_rel list), (constr_sort:T.r_sort list)) =
181  function
182     "/searchPattern" ->
183       U.universe_for_search_pattern,
184        (constr_obj, constr_rel, constr_sort),
185        (Some constr_obj, Some constr_rel, Some constr_sort)
186   | "/matchConclusion" ->
187       let constr_obj' =
188        List.map
189         (function (pos, uri) -> U.set_full_position pos None, uri)
190         (List.filter
191           (function (pos, _) -> U.is_conclusion pos)
192           constr_obj)
193       in
194        U.universe_for_match_conclusion,
195        (*CSC: we must select the must constraints here!!! *)
196        (constr_obj',[],[]),(Some constr_obj', None, None)
197   | _ -> assert false
198 ;;
199
200 let get_constraints term =
201  function
202     "/locateInductivePrinciple" ->
203       let uri = 
204        match term with
205           Cic.MutInd (uri,t,_) -> MQueryUtil.string_of_uriref (uri,[t])
206         | _ -> raise NotAnInductiveDefinition
207       in
208       let constr_obj =
209        [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)]
210       in
211       let constr_rel = [`MainConclusion None] in
212       let constr_sort = [(`MainHypothesis (Some 1), T.Prop)] in
213        U.universe_for_search_pattern,
214         (constr_obj, constr_rel, constr_sort), (None,None,None)
215   | req_path ->
216      let must = CGSearchPattern.get_constraints term in
217       refine_constraints must req_path
218 ;;
219
220 (*
221   format:
222     <must_obj> ':' <must_rel> ':' <must_sort> ':' <only_obj> ':' <only_rel> ':' <only_sort>
223
224     <must_*> ::= ('0'|'1') ('_'|<int>) (',' ('0'|'1') ('_'|<int>))*
225     <only> ::= '0'|'1'
226 *)
227 let add_user_constraints ~constraints
228  ((obj, rel, sort), (only_obj, only_rel, only_sort))
229 =
230   let parse_must s =
231     let l = Pcre.split ~pat:"," s in
232     (try
233       List.map
234         (fun s ->
235           let subs = Pcre.extract ~pat:"^(.)(\\d+|_)$" s in
236           (bool_of_string' subs.(1), int_of_string' subs.(2)))
237         l
238      with
239       Not_found -> failwith ("Can't parse constraint string: " ^ constraints)
240     )
241   in
242     (* to be used on "obj" *)
243   let add_user_must33 user_must must =
244     List.map2
245      (fun (b, i) (p, u) ->
246        if b then Some (U.set_full_position p i, u) else None)
247      user_must must
248   in
249     (* to be used on "rel" *)
250   let add_user_must22 user_must must =
251     List.map2
252      (fun (b, i) p -> if b then Some (U.set_main_position p i) else None)
253      user_must must
254   in
255     (* to be used on "sort" *)
256   let add_user_must32 user_must must =
257     List.map2
258      (fun (b, i) (p, s)-> if b then Some (U.set_main_position p i, s) else None)
259      user_must must
260   in
261   match Pcre.split ~pat:":" constraints with
262   | [user_obj;user_rel;user_sort;user_only_obj;user_only_rel;user_only_sort] ->
263       let
264        (user_obj,user_rel,user_sort,user_only_obj,user_only_rel,user_only_sort)
265       =
266         (parse_must user_obj,
267         parse_must user_rel,
268         parse_must user_sort,
269         bool_of_string' user_only_obj,
270         bool_of_string' user_only_rel,
271         bool_of_string' user_only_sort)
272       in
273       let only' =
274        (if user_only_obj  then only_obj else None),
275        (if user_only_rel  then only_rel else None),
276        (if user_only_sort then only_sort else None)
277       in
278       let must' =
279        let rec filter_some =
280         function
281            [] -> []
282          | None::tl -> filter_some tl
283          | (Some x)::tl -> x::(filter_some tl) 
284        in
285         filter_some (add_user_must33 user_obj obj),
286         filter_some (add_user_must22 user_rel rel),
287         filter_some (add_user_must32 user_sort sort)
288       in
289       (must', only')
290   | _ -> failwith ("Can't parse constraint string: " ^ constraints)
291 in
292
293 (* HTTP DAEMON CALLBACK *)
294
295 let callback (req: Http_types.request) outchan =
296   try
297     debug_print (sprintf "Received request: %s" req#path);
298     (match req#path with
299     | "/execute" ->
300         let mqi_handle = C.init mqi_flags debug_print in 
301         let query_string = req#param "query" in
302         let lexbuf = Lexing.from_string query_string in
303         let query = MQueryUtil.query_of_text lexbuf in
304         let result = MQueryInterpreter.execute mqi_handle query in
305         let result_string = pp_result result in
306               C.close mqi_handle;
307         Http_daemon.respond ~body:result_string ~headers:[contype] outchan
308     | "/locate" ->
309         let mqi_handle = C.init mqi_flags debug_print in
310         let id = req#param "id" in
311         let query = G.locate id in
312         let result = MQueryInterpreter.execute mqi_handle query in
313               C.close mqi_handle;
314         Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
315     | "/unreferred" ->
316         let mqi_handle = C.init mqi_flags debug_print in
317         let target = req#param "target" in
318         let source = req#param "source" in
319         let query = G.unreferred target source in
320         let result = MQueryInterpreter.execute mqi_handle query in
321               C.close mqi_handle;
322         Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
323     | "/getpage" ->
324         (* TODO implement "is_permitted" *)
325         (let is_permitted _ = true in
326         let remove_fragment uri = Pcre.replace ~pat:"#.*" uri in
327         let page = remove_fragment (req#param "url") in
328         let preprocess =
329           (try
330             bool_of_string (req#param "preprocess")
331           with Invalid_argument _ | Http_types.Param_not_found _ -> false)
332         in
333         (match page with
334         | page when is_permitted page ->
335             (let fname = sprintf "%s/%s" pages_dir (remove_fragment page) in
336             Http_daemon.send_basic_headers ~code:200 outchan;
337             Http_daemon.send_header "Content-Type" "text/html" outchan;
338             Http_daemon.send_CRLF outchan;
339             if preprocess then begin
340               iter_file
341                 (fun line ->
342                   output_string outchan
343                     ((apply_substs
344                        (List.map
345                          (function (key,value) ->
346                            let key' =
347                             (Pcre.extract ~pat:"param\\.(.*)" key).(1)
348                            in
349                             Pcre.regexp ("@" ^ key' ^ "@"), value
350                          )
351                          (List.filter
352                            (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key)
353                            req#params)
354                        )
355                        line) ^
356                     "\n"))
357                 fname
358             end else
359               Http_daemon.send_file ~src:(FileSrc fname) outchan)
360         | page -> Http_daemon.respond_forbidden ~url:page outchan))
361     | "/ask_uwobo" ->
362       let url = req#param "url" in
363       let server_and_port =
364         (Pcre.extract ~rex:server_and_port_url_RE url).(1)
365       in
366       if List.mem server_and_port valid_servers then
367         Http_daemon.respond
368           ~headers:["Content-Type", "text/html"]
369           ~body:(Http_client.Convenience.http_get url)
370           outchan
371       else
372         Http_daemon.respond
373           ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port))
374           outchan
375     | "/searchPattern"
376     | "/matchConclusion"
377     | "/locateInductivePrinciple" ->
378         let mqi_handle = C.init mqi_flags debug_print in
379         let term_string = req#param "term" in
380         let lexbuf = Lexing.from_string term_string in
381         let (context, metasenv) = ([], []) in
382         let (dom, mk_metasenv_and_expr) =
383           CicTextualParserContext.main
384             ~context ~metasenv CicTextualLexer.token lexbuf
385         in
386         let id_to_uris_raw = req#param "aliases" in
387         let tokens = Pcre.split ~pat:"\\s" id_to_uris_raw in
388         let rec parse_tokens keys lookup = function (* TODO spostarla fuori *)
389           | [] -> keys, lookup
390           | "alias" :: key :: value :: rest ->
391               let key' = CicTextualParser0.Id key in
392                parse_tokens
393                  (key'::keys)
394                  (fun id ->
395                    if id = key' then
396                      Some
397                       (CicTextualParser0.Uri (MQueryMisc.cic_textual_parser_uri_of_string value))
398                    else lookup id)
399                  rest
400           | _ -> failwith "Can't parse aliases"
401         in
402         let parse_choices choices_raw =
403           let choices = Pcre.split ~pat:";" choices_raw in
404           List.fold_left
405             (fun f x ->
406               match Pcre.split ~pat:"\\s" x with
407               | ""::id::tail
408               | id::tail when id<>"" ->
409                   (fun id' ->
410 prerr_endline ("#### " ^ id ^ " :=");
411 List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
412                     if id = id' then
413                       Some (List.map (fun u -> Netencoding.Url.decode u) tail)
414                     else
415                       f id')
416               | _ -> failwith "Can't parse choices")
417             (fun _ -> None)
418             choices
419         in
420         let (id_to_uris : Disambiguate.domain_and_interpretation) =
421          parse_tokens [] (fun _ -> None) tokens in
422         let id_to_choices =
423           try
424             let choices_raw = req#param "choices" in
425             parse_choices choices_raw
426           with Http_types.Param_not_found _ -> (fun _ -> None)
427         in
428         let module Chat: Disambiguate.Callbacks =
429           struct
430
431             let get_metasenv () =
432              !CicTextualParser0.metasenv
433
434             let set_metasenv metasenv =
435               CicTextualParser0.metasenv := metasenv
436
437             let output_html = prerr_endline
438
439             let interactive_user_uri_choice
440               ~selection_mode ?ok
441               ?enable_button_for_non_vars ~(title: string) ~(msg: string)
442               ~(id: string) (choices: string list)
443               =
444                 (match id_to_choices id with
445                 | Some choices -> choices
446                 | None ->
447                   let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in
448                   (match selection_mode with
449                   | `SINGLE -> assert false
450                   | `EXTENDED ->
451                       Http_daemon.send_basic_headers ~code:200 outchan ;
452                       Http_daemon.send_CRLF outchan ;
453                       iter_file
454                         (fun line ->
455                           let formatted_choices =
456                             String.concat ","
457                               (List.map (fun uri -> sprintf "\'%s\'" uri) choices)
458                           in
459                           let processed_line =
460                             apply_substs
461                               [title_tag_RE, title;
462                                choices_tag_RE, formatted_choices;
463                                msg_tag_RE, msg;
464                                id_to_uris_RE, id_to_uris_raw;
465                                id_RE, id]
466                               line
467                           in
468                           output_string outchan (processed_line ^ "\n"))
469                         interactive_user_uri_choice_TPL;
470                       raise Chat_unfinished))
471
472             let interactive_interpretation_choice interpretations =
473               let html_interpretations_labels =
474                 String.concat ", "
475                   (List.map
476                     (fun l ->
477                       "\'" ^
478                       (String.concat "<br />"
479                         (List.map
480                           (fun (id, value) ->
481                             (sprintf "alias %s %s" id value))
482                           l)) ^
483                       "\'")
484                   interpretations)
485               in
486               let html_interpretations =
487                 String.concat ", "
488                   (List.map
489                     (fun l ->
490                       "\'" ^
491                       (String.concat " "
492                         (List.map
493                           (fun (id, value) ->
494                             (sprintf "alias %s %s"
495                               id
496                               (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
497                                 value)))
498                           l)) ^
499                       "\'")
500                     interpretations)
501               in
502               Http_daemon.send_basic_headers ~code:200 outchan ;
503               Http_daemon.send_CRLF outchan ;
504               iter_file
505                 (fun line ->
506                   let processed_line =
507                     apply_substs
508                       [interpretations_RE, html_interpretations;
509                        interpretations_labels_RE, html_interpretations_labels]
510                       line
511                   in
512                   output_string outchan (processed_line ^ "\n"))
513                 interactive_interpretation_choice_TPL;
514               raise Chat_unfinished
515
516             let input_or_locate_uri ~title =
517               UriManager.uri_of_string "cic:/Coq/Init/DataTypes/nat_ind.con"
518
519           end
520         in
521         let module Disambiguate' = Disambiguate.Make (Chat) in
522         let (id_to_uris', metasenv', term') =
523           Disambiguate'.disambiguate_input mqi_handle
524             context metasenv dom mk_metasenv_and_expr id_to_uris
525         in
526         (match metasenv' with
527         | [] ->
528             let universe,
529                 ((must_obj, must_rel, must_sort) as must'),
530                 ((only_obj, only_rel, only_sort) as only) =
531               get_constraints term' req#path
532             in
533             let must'', only' =
534               (try
535                 add_user_constraints
536                   ~constraints:(req#param "constraints")
537                   (must', only)
538               with Http_types.Param_not_found _ ->
539                 let variables =
540                  "var aliases = '" ^ id_to_uris_raw ^ "';\n" ^
541                  "var constr_obj_len = " ^
542                   string_of_int (List.length must_obj) ^ ";\n" ^
543                  "var constr_rel_len = " ^
544                   string_of_int (List.length must_rel) ^ ";\n" ^
545                  "var constr_sort_len = " ^
546                   string_of_int (List.length must_sort) ^ ";\n" in
547                 let form =
548                   (if must_obj = [] then "" else
549                     "<h4>Obj constraints</h4>" ^
550                     "<table>" ^
551                     (String.concat "\n" (List.map html_of_r_obj must_obj)) ^
552                     "</table>" ^
553                     (* The following three lines to make Javascript create *)
554                     (* the constr_obj[] and obj_depth[] arrays even if we  *)
555                     (* have only one real entry.                           *)
556                     "<input type=\"hidden\" name=\"constr_obj\" />" ^
557                     "<input type=\"hidden\" name=\"obj_depth\" />") ^
558                   (if must_rel = [] then "" else
559                    "<h4>Rel constraints</h4>" ^
560                    "<table>" ^
561                    (String.concat "\n" (List.map html_of_r_rel must_rel)) ^
562                    "</table>" ^
563                     (* The following two lines to make Javascript create *)
564                     (* the constr_rel[] and rel_depth[] arrays even if   *)
565                     (* we have only one real entry.                      *)
566                     "<input type=\"hidden\" name=\"constr_rel\" />" ^
567                     "<input type=\"hidden\" name=\"rel_depth\" />") ^
568                   (if must_sort = [] then "" else
569                     "<h4>Sort constraints</h4>" ^
570                     "<table>" ^
571                     (String.concat "\n" (List.map html_of_r_sort must_sort)) ^
572                     "</table>" ^
573                     (* The following two lines to make Javascript create *)
574                     (* the constr_sort[] and sort_depth[] arrays even if *)
575                     (* we have only one real entry.                      *)
576                     "<input type=\"hidden\" name=\"constr_sort\" />" ^
577                     "<input type=\"hidden\" name=\"sort_depth\" />") ^
578                     "<h4>Only constraints</h4>" ^
579                     "Enforce Only constraints for objects: " ^
580                       "<input type='checkbox' name='only_obj'" ^
581                       (if only_obj = None then "" else " checked='yes'") ^ " /><br />" ^
582                     "Enforce Rel constraints for objects: " ^
583                       "<input type='checkbox' name='only_rel'" ^
584                       (if only_rel = None then "" else " checked='yes'") ^ " /><br />" ^
585                     "Enforce Sort constraints for objects: " ^
586                       "<input type='checkbox' name='only_sort'" ^
587                       (if only_sort = None then "" else " checked='yes'") ^ " /><br />"
588                 in
589                 Http_daemon.send_basic_headers ~code:200 outchan ;
590                 Http_daemon.send_CRLF outchan ;
591                 iter_file
592                   (fun line ->
593                     let processed_line =
594                       apply_substs
595                        [form_RE, form ;
596                         variables_initialization_RE, variables] line
597                     in
598                     output_string outchan (processed_line ^ "\n"))
599                   constraints_choice_TPL;
600                   raise Chat_unfinished)
601             in
602             let query =
603              G.query_of_constraints (Some universe) must'' only'
604             in
605                   let results = MQueryInterpreter.execute mqi_handle query in 
606              Http_daemon.send_basic_headers ~code:200 outchan ;
607              Http_daemon.send_CRLF outchan ;
608              iter_file
609                (fun line ->
610                  let new_aliases =
611                    match id_to_uris' with
612                    | (domain, f) ->
613                        String.concat ", "
614                          (List.map
615                            (fun name ->
616                              sprintf "\'alias %s cic:%s\'"
617                                (match name with
618                                    CicTextualParser0.Id name -> name
619                                  | _ -> assert false (*CSC: completare *))
620                                (match f name with
621                                | None -> assert false
622                                | Some (CicTextualParser0.Uri t) ->
623                                    MQueryMisc.string_of_cic_textual_parser_uri
624                                      t
625                                | _ -> assert false (*CSC: completare *)))
626                            domain)
627                  in
628                  let processed_line =
629                    apply_substs
630                      [results_RE, theory_of_result results ;
631                       new_aliases_RE, new_aliases]
632                      line
633                  in
634                  output_string outchan (processed_line ^ "\n"))
635                final_results_TPL
636         | _ -> (* unable to instantiate some implicit variable *)
637             Http_daemon.respond
638               ~headers:[contype]
639               ~body:"some implicit variables are still unistantiated :-("
640               outchan);
641             C.close mqi_handle
642     | invalid_request ->
643         Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
644     debug_print (sprintf "%s done!" req#path)
645   with
646   | Chat_unfinished -> prerr_endline "Chat unfinished, Try again!"
647   | Http_types.Param_not_found attr_name ->
648       bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
649   | exc ->
650       Http_daemon.respond
651         ~body:(pp_error ("Uncaught exception: " ^ (Printexc.to_string exc)))
652         outchan
653 in
654 printf "%s started and listening on port %d\n" daemon_name port;
655 printf "Current directory is %s\n" (Sys.getcwd ());
656 printf "HTML directory is %s\n" pages_dir;
657 flush stdout;
658 Unix.putenv "http_proxy" "";
659 Http_daemon.start' ~port callback;
660 printf "%s is terminating, bye!\n" daemon_name
661