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