]> matita.cs.unibo.it Git - helm.git/commitdiff
- non empty metasenv after the parsing phase are now accepted
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 9 Mar 2004 10:43:54 +0000 (10:43 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 9 Mar 2004 10:43:54 +0000 (10:43 +0000)
- still many bugs open (due to the new aliases for symbols)

helm/searchEngine/searchEngine.ml

index 2d8a7067c5fbe5e4edcd2df82ee1a0c7c7a1b43e..e5cb733bfe179401ba3a9fe8aa584bec940ef40a 100644 (file)
@@ -30,7 +30,7 @@ module C = MQIConn
 
 open Http_types ;;
 
-let debug = false;;
+let debug = true;;
 let debug_print s = if debug then prerr_endline s;;
 Http_common.debug := true;;
 (* Http_common.debug := true;; *)
@@ -59,6 +59,11 @@ let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";;
 
 exception Chat_unfinished
 
+let javascript_quote =
+ let rex = Pcre.regexp "'" in
+  Pcre.replace ~rex ~templ:"\\'"
+;;
+
   (* build a bool from a 1-character-string *)
 let bool_of_string' = function
   | "0" -> false
@@ -430,7 +435,9 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id
                       (String.concat "<br />"
                         (List.map
                           (fun (id, value) ->
-                            (sprintf "alias id %s = %s" id value))
+                            let id = javascript_quote id in
+                            let value = javascript_quote value in
+                             sprintf "alias id %s = %s" id value)
                           l)) ^
                       "\'")
                   interpretations)
@@ -443,10 +450,12 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id
                       (String.concat " "
                         (List.map
                           (fun (id, value) ->
-                            (sprintf "alias id %s = %s"
+                            let id = javascript_quote id in
+                            let value = javascript_quote value in
+                             sprintf "alias id %s = %s"
                               id
                               (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
-                                value)))
+                                value))
                           l)) ^
                       "\'")
                     interpretations)
@@ -479,124 +488,117 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id
             [id_to_uris',metasenv',term'] -> id_to_uris',metasenv',term'
           | _ -> assert false
         in
-        (match metasenv' with
-        | [] ->
-            let universe,
-                ((must_obj, must_rel, must_sort) as must'),
-                ((only_obj, only_rel, only_sort) as only) =
-              get_constraints term' req#path
-            in
-            let must'', only' =
-              (try
-                add_user_constraints
-                  ~constraints:(req#param "constraints")
-                  (must', only)
-              with Http_types.Param_not_found _ ->
-                let variables =
-                 "var aliases = '" ^ id_to_uris_raw ^ "';\n" ^
-                 "var constr_obj_len = " ^
-                  string_of_int (List.length must_obj) ^ ";\n" ^
-                 "var constr_rel_len = " ^
-                  string_of_int (List.length must_rel) ^ ";\n" ^
-                 "var constr_sort_len = " ^
-                  string_of_int (List.length must_sort) ^ ";\n" in
-                let form =
-                  (if must_obj = [] then "" else
-                    "<h4>Obj constraints</h4>" ^
-                    "<table>" ^
-                    (String.concat "\n" (List.map html_of_r_obj must_obj)) ^
-                    "</table>" ^
-                    (* The following three lines to make Javascript create *)
-                    (* the constr_obj[] and obj_depth[] arrays even if we  *)
-                    (* have only one real entry.                           *)
-                    "<input type=\"hidden\" name=\"constr_obj\" />" ^
-                    "<input type=\"hidden\" name=\"obj_depth\" />") ^
-                  (if must_rel = [] then "" else
-                   "<h4>Rel constraints</h4>" ^
-                   "<table>" ^
-                   (String.concat "\n" (List.map html_of_r_rel must_rel)) ^
-                   "</table>" ^
-                    (* The following two lines to make Javascript create *)
-                    (* the constr_rel[] and rel_depth[] arrays even if   *)
-                    (* we have only one real entry.                      *)
-                    "<input type=\"hidden\" name=\"constr_rel\" />" ^
-                    "<input type=\"hidden\" name=\"rel_depth\" />") ^
-                  (if must_sort = [] then "" else
-                    "<h4>Sort constraints</h4>" ^
-                    "<table>" ^
-                    (String.concat "\n" (List.map html_of_r_sort must_sort)) ^
-                    "</table>" ^
-                    (* The following two lines to make Javascript create *)
-                    (* the constr_sort[] and sort_depth[] arrays even if *)
-                    (* we have only one real entry.                      *)
-                    "<input type=\"hidden\" name=\"constr_sort\" />" ^
-                    "<input type=\"hidden\" name=\"sort_depth\" />") ^
-                    "<h4>Only constraints</h4>" ^
-                    "Enforce Only constraints for objects: " ^
-                      "<input type='checkbox' name='only_obj'" ^
-                      (if only_obj = None then "" else " checked='yes'") ^ " /><br />" ^
-                    "Enforce Rel constraints for objects: " ^
-                      "<input type='checkbox' name='only_rel'" ^
-                      (if only_rel = None then "" else " checked='yes'") ^ " /><br />" ^
-                    "Enforce Sort constraints for objects: " ^
-                      "<input type='checkbox' name='only_sort'" ^
-                      (if only_sort = None then "" else " checked='yes'") ^ " /><br />"
-                in
-                Http_daemon.send_basic_headers ~code:200 outchan ;
-                Http_daemon.send_CRLF outchan ;
-                iter_file
-                  (fun line ->
-                    let processed_line =
-                      apply_substs
-                       [form_RE, form ;
-                        variables_initialization_RE, variables] line
-                    in
-                    output_string outchan (processed_line ^ "\n"))
-                  constraints_choice_TPL;
-                  raise Chat_unfinished)
-            in
-            let query =
-             G.query_of_constraints universe must'' only'
-            in
-                 let results = MQueryInterpreter.execute mqi_handle query in 
-             Http_daemon.send_basic_headers ~code:200 outchan ;
-             Http_daemon.send_CRLF outchan ;
-             iter_file
-               (fun line ->
-                 let new_aliases =
-                  DisambiguatingParser.EnvironmentP3.to_string id_to_uris' in
+          let universe,
+              ((must_obj, must_rel, must_sort) as must'),
+              ((only_obj, only_rel, only_sort) as only) =
+            get_constraints term' req#path
+          in
+          let must'', only' =
+            (try
+              add_user_constraints
+                ~constraints:(req#param "constraints")
+                (must', only)
+            with Http_types.Param_not_found _ ->
+              let variables =
+               "var aliases = '" ^ id_to_uris_raw ^ "';\n" ^
+               "var constr_obj_len = " ^
+                string_of_int (List.length must_obj) ^ ";\n" ^
+               "var constr_rel_len = " ^
+                string_of_int (List.length must_rel) ^ ";\n" ^
+               "var constr_sort_len = " ^
+                string_of_int (List.length must_sort) ^ ";\n" in
+              let form =
+                (if must_obj = [] then "" else
+                  "<h4>Obj constraints</h4>" ^
+                  "<table>" ^
+                  (String.concat "\n" (List.map html_of_r_obj must_obj)) ^
+                  "</table>" ^
+                  (* The following three lines to make Javascript create *)
+                  (* the constr_obj[] and obj_depth[] arrays even if we  *)
+                  (* have only one real entry.                           *)
+                  "<input type=\"hidden\" name=\"constr_obj\" />" ^
+                  "<input type=\"hidden\" name=\"obj_depth\" />") ^
+                (if must_rel = [] then "" else
+                 "<h4>Rel constraints</h4>" ^
+                 "<table>" ^
+                 (String.concat "\n" (List.map html_of_r_rel must_rel)) ^
+                 "</table>" ^
+                  (* The following two lines to make Javascript create *)
+                  (* the constr_rel[] and rel_depth[] arrays even if   *)
+                  (* we have only one real entry.                      *)
+                  "<input type=\"hidden\" name=\"constr_rel\" />" ^
+                  "<input type=\"hidden\" name=\"rel_depth\" />") ^
+                (if must_sort = [] then "" else
+                  "<h4>Sort constraints</h4>" ^
+                  "<table>" ^
+                  (String.concat "\n" (List.map html_of_r_sort must_sort)) ^
+                  "</table>" ^
+                  (* The following two lines to make Javascript create *)
+                  (* the constr_sort[] and sort_depth[] arrays even if *)
+                  (* we have only one real entry.                      *)
+                  "<input type=\"hidden\" name=\"constr_sort\" />" ^
+                  "<input type=\"hidden\" name=\"sort_depth\" />") ^
+                  "<h4>Only constraints</h4>" ^
+                  "Enforce Only constraints for objects: " ^
+                    "<input type='checkbox' name='only_obj'" ^
+                    (if only_obj = None then "" else " checked='yes'") ^ " /><br />" ^
+                  "Enforce Rel constraints for objects: " ^
+                    "<input type='checkbox' name='only_rel'" ^
+                    (if only_rel = None then "" else " checked='yes'") ^ " /><br />" ^
+                  "Enforce Sort constraints for objects: " ^
+                    "<input type='checkbox' name='only_sort'" ^
+                    (if only_sort = None then "" else " checked='yes'") ^ " /><br />"
+              in
+              Http_daemon.send_basic_headers ~code:200 outchan ;
+              Http_daemon.send_CRLF outchan ;
+              iter_file
+                (fun line ->
+                  let processed_line =
+                    apply_substs
+                     [form_RE, form ;
+                      variables_initialization_RE, variables] line
+                  in
+                  output_string outchan (processed_line ^ "\n"))
+                constraints_choice_TPL;
+                raise Chat_unfinished)
+          in
+          let query =
+           G.query_of_constraints universe must'' only'
+          in
+          let results = MQueryInterpreter.execute mqi_handle query in 
+           Http_daemon.send_basic_headers ~code:200 outchan ;
+           Http_daemon.send_CRLF outchan ;
+           iter_file
+             (fun line ->
+               let new_aliases =
+                DisambiguatingParser.EnvironmentP3.to_string id_to_uris' in
 (*XXX
-                   match id_to_uris' with
-                   | (domain, f) ->
-                       String.concat ", "
-                         (List.map
-                           (fun name ->
-                             sprintf "\'alias %s cic:%s\'"
-                               (match name with
-                                   CicTextualParser0.Id name -> name
-                                 | _ -> assert false (*CSC: completare *))
-                               (match f name with
-                               | None -> assert false
-                               | Some (CicTextualParser0.Uri t) ->
-                                   MQueryMisc.string_of_cic_textual_parser_uri
-                                     t
-                               | _ -> assert false (*CSC: completare *)))
-                           domain)
-                 in
+                 match id_to_uris' with
+                 | (domain, f) ->
+                     String.concat ", "
+                       (List.map
+                         (fun name ->
+                           sprintf "\'alias %s cic:%s\'"
+                             (match name with
+                                 CicTextualParser0.Id name -> name
+                               | _ -> assert false (*CSC: completare *))
+                             (match f name with
+                             | None -> assert false
+                             | Some (CicTextualParser0.Uri t) ->
+                                 MQueryMisc.string_of_cic_textual_parser_uri
+                                   t
+                             | _ -> assert false (*CSC: completare *)))
+                         domain)
+               in
 *)
-                 let processed_line =
-                   apply_substs
-                     [results_RE, theory_of_result results ;
-                      new_aliases_RE, new_aliases]
-                     line
-                 in
-                 output_string outchan (processed_line ^ "\n"))
-               final_results_TPL
-        | _ -> (* unable to instantiate some implicit variable *)
-            Http_daemon.respond
-              ~headers:[contype]
-              ~body:"some implicit variables are still unistantiated :-("
-              outchan)
+               let processed_line =
+                 apply_substs
+                   [results_RE, theory_of_result results ;
+                    new_aliases_RE, new_aliases]
+                   line
+               in
+               output_string outchan (processed_line ^ "\n"))
+             final_results_TPL
     | invalid_request ->
         Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
     debug_print (sprintf "%s done!" req#path)
@@ -605,9 +607,9 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id
   | Http_types.Param_not_found attr_name ->
       bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
   | exc ->
-      Http_daemon.respond
-        ~body:(pp_error ("Uncaught exception: " ^ (Printexc.to_string exc)))
-        outchan
+      let msg = sprintf "Uncaught exception: %s" (Printexc.to_string exc) in
+       debug_print msg ;
+       Http_daemon.respond ~body:(pp_error msg) outchan
 in
 printf "%s started and listening on port %d\n" daemon_name port;
 printf "Current directory is %s\n" (Sys.getcwd ());