]> matita.cs.unibo.it Git - helm.git/commitdiff
- ported to Helm_registry
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 17 Feb 2004 16:33:19 +0000 (16:33 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 17 Feb 2004 16:33:19 +0000 (16:33 +0000)
- ported to the new disambiguating parser of Zack & Andrea

helm/searchEngine/Makefile
helm/searchEngine/html/aliaslist.html
helm/searchEngine/html/expr.html
helm/searchEngine/html/grammarpdq.html
helm/searchEngine/searchEngine.conf.xml.sample [new file with mode: 0644]
helm/searchEngine/searchEngine.ml

index c3617f46ad0fd228fae492d24a08bbd620ae9cb8..809a5abf7f6283c3dfd18fa895825d08bdb2423a 100644 (file)
@@ -1,11 +1,12 @@
-REQUIRES = http helm-cic_textual_parser helm-cic_proof_checking \
+REQUIRES = http helm-cic_textual_parser2 helm-cic_proof_checking \
            helm-xml gdome2-xslt helm-cic_unification helm-mathql \
-           helm-mathql_interpreter helm-mathql_generator helm-logger
-OCAMLOPTIONS = -package "$(REQUIRES)" -pp camlp4o -I ../gTopLevel
+           helm-mathql_interpreter helm-mathql_generator helm-logger \
+           helm-tex_cic_textual_parser
+OCAMLOPTIONS = -thread -package "$(REQUIRES)" -pp camlp4o -I ../gTopLevel
 OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
 OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
 
-GTOPLEVEL_MODULES = disambiguate
+GTOPLEVEL_MODULES = oldDisambiguate disambiguatingParser
 MODULES =
 CMOS = $(patsubst %,%.cmo,$(MODULES))
 CMXS = $(patsubst %,%.cmx,$(MODULES))
index d030ea41e4ee1c00584c0696f97877980bc70591..27497acf895748d05578b3a7479a9999d6962061 100644 (file)
@@ -60,7 +60,7 @@ function addalias()
        {
        if (top.idcheck(document.aliaslist.idi.value)==1 && top.uricheck(document.aliaslist.uri.value)==1)
                {
-               top.aliasglob[top.aliasglob.length]="alias "+document.aliaslist.idi.value+" "+document.aliaslist.uri.value;
+               top.aliasglob[top.aliasglob.length]="alias id "+document.aliaslist.idi.value+" = "+document.aliaslist.uri.value;
                //parent.aggiorna();
                top.window.open(top.topurl+top.action+"aliaslist.html",(top.cw.frames.length==0?"cw":"bw"));
                }
@@ -68,15 +68,16 @@ function addalias()
 function istruzioni()
        {       
        top.hw.document.close();
-       top.hw.document.write("You must now enter a list of alias. An Alias is the word 'alias' followed by an <a href='grammarpdq.html#Id' target='gw'>Id</a>, followed by an <a href='grammarpdq.html#Uri' target='gw'>Uri</a>.You may enter as many of them as you want, after each one click the button 'add alias' or press enter and it will be added. When you are done, click 'done'.");
+       top.hw.document.write("You must now enter a list of alias. An Alias is the word 'alias' followed by 'id', an <a href='grammarpdq.html#Id' target='gw'>Id</a>, the equality sign '=', an <a href='grammarpdq.html#Uri' target='gw'>Uri</a>.You may enter as many of them as you want, after each one click the button 'add alias' or press enter and it will be added. When you are done, click 'done'.");
        }
 istruzioni();
 </SCRIPT>
 </HEAD>
 <BODY>
 <form name="aliaslist" action="Javascript:addalias();" method="get">
-alias
+alias id
 <input name="idi" type=text size="15" value="">
+=
 <input name="uri" type=text size="45" value="cic:/"><br>
 <input type=submit value="add alias"><input type=button value="delete selected" onClick="rimuovialias()";><br>
 <select name="elenco" multiple size=7>
index 3e302b8b24fc366fed1119c6803856acbdd6c35d..dea29bc52a8a9a93eab408b37a6e30f9fc9426ff 100644 (file)
@@ -5,12 +5,13 @@ function choice()
        {
 with (document.form1) {        
        stadd="";top.qw.document.close();quanti=0;
-       if (selopt[0].checked) {stadd="\[Genid]"+document.form1.ex1.value+"[Expr].[Expr]"}
-       if (selopt[1].checked) {stadd="![Genid]:[Expr].[Expr]"}
-       if (selopt[2].checked) {stadd="[Expr]-&gt;[Expr]"}
-       if (selopt[3].checked) {stadd="([Expr])-&gt;[Expr]"}
-       if (selopt[4].checked) {stadd=document.form1.ex2.value}
-       if (selopt[5].checked) {
+       if (selopt[0].checked) {stadd="\\lambda [Genid] : [Expr].[Expr]"}
+       if (selopt[1].checked) {stadd="let [Genid] = [Expr] in [Expr]"}
+       if (selopt[2].checked) {stadd="\\forall [Genid]:[Expr].[Expr]"}
+       if (selopt[3].checked) {stadd="[Expr] \\to [Expr]"}
+  if (selopt[4].checked) {stadd="?"}
+       if (selopt[5].checked) {stadd=document.form1.ex2.value}
+       if (selopt[6].checked) {
                                while (quanti<1)
                                        {
                                        quanti=prompt("How many expressions in the list?","1");//alert(quanti);
@@ -21,7 +22,7 @@ with (document.form1) {
                                {stadd=stadd+"[Expr] "}
                                stadd=stadd+")";
                               }
-       if (selopt[6].checked) {
+       if (selopt[7].checked) {
                                stadd=document.form1.id_or_uri.value;
                                //alert(stadd.substring(0,5));
                                if (stadd.substring(0,5)=="cic:/") 
@@ -39,13 +40,11 @@ with (document.form1) {
 <BODY>
 You are entering an expression. Select one of the following.
 <form name="form1" action="Javascript:choice();" method="get">
-<input type="radio" name="selopt">\[Genid]<select name="ex1" onFocus="selopt[0].checked=true;">
-<option value=":">:
-<option value=":=">:=
-</select>[Expr].[Expr] <br>
-<input type="radio" name="selopt">![Genid]:[Expr].[Expr] <br>
-<input type="radio" name="selopt">[Expr]-&gt;[Expr]<br>
-<input type="radio" name="selopt">([Expr])-&gt;[Expr]<br>
+<input type="radio" name="selopt">\lambda [Genid]:[Expr].[Expr] <br>
+<input type="radio" name="selopt">let [Genid] = [Expr] in [Expr] <br>
+<input type="radio" name="selopt">\forall [Genid]:[Expr].[Expr] <br>
+<input type="radio" name="selopt">[Expr] \to [Expr]<br>
+<input type="radio" name="selopt">?<br>
 <input type="radio" name="selopt"> <select name="ex2" onFocus="selopt[4].checked=true;">
 <option value="Prop"> Prop 
 <option value="Set"> Set
@@ -57,4 +56,4 @@ You are entering an expression. Select one of the following.
 <input type=submit value="Select">
 </form>
 </BODY>
-</HTML>
\ No newline at end of file
+</HTML>
index bd3835bf90eeb3005ec6ad7d4264a78b447f62dd..309e5b5925fcf7d180ef33a2e5dcc0f5f03759bf 100644 (file)
@@ -19,7 +19,7 @@
 <a name="Exp_Named_Subst">
 <p><b>&lt;Exp_Named_Subst&gt;</b>::= &quot;{&quot; [ [ [&lt;<a href="#Id">Id</a>&gt; | &lt;<a href="#Varuri">Varuri</a>&gt; ] &quot;:=&quot; &lt;Expression&gt; &quot;;&quot; ]* [ [&lt;<a href="#Id">Id</a>&gt; | &lt;<a href="#Varuri">Varuri</a>&gt; ] &quot;:=&quot; &lt;Expression&gt; ] ]? &quot;}&quot;</a>
 <a name="Alias">
-<p><b>&lt;Alias&gt;</b>::= &quot;alias&quot; &lt;<a href="#Id">Id</a>&gt; &lt;<a href="#Uri">Uri</a>&gt;
+<p><b>&lt;Alias&gt;</b>::= &quot;alias&quot; &quot;id&quot; &lt;<a href="#Id">Id</a>&gt; = &lt;<a href="#Uri">Uri</a>&gt;
 <a name="Genid">
 <p><b>&lt;Genid&gt;</b>::= [ &lt;<a href="#Id">Id</a>&gt; | &lt;<a href="#Varuri">Varuri</a>&gt; | &lt;<a href="#Indtyuri">Indtyuri</a>&gt; | &lt;<a href="#Indconuri">Indconuri</a>&gt; ] &lt;<a href="#Exp_Named_Subst">Exp_Named_Subst</a>&gt;
 <a name="Expr">
@@ -35,4 +35,4 @@
 <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
 ::= &quot;Prop&quot; | &quot;Set&quot; | &quot;Type&quot; | &quot;?&quot; | &lt;<a href="#Uri">Uri</a>&gt; | &lt;<a href="#Id">Id</a>&gt;
 </BODY>
-</HTML>
\ No newline at end of file
+</HTML>
diff --git a/helm/searchEngine/searchEngine.conf.xml.sample b/helm/searchEngine/searchEngine.conf.xml.sample
new file mode 100644 (file)
index 0000000..0bfbbcf
--- /dev/null
@@ -0,0 +1,12 @@
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+  <section name="getter">
+    <key name="mode">remote</key>
+    <key name="url">http://localhost:58081/</key>
+  </section>
+  <section name="search_engine">
+    <key name="html_dir">html</key>
+    <key name="port">58085</key>
+    <key name="valid_servers">mowgli.cs.unibo.it:58080 mowgli.cs.unibo.it localhost:58080</key>
+  </section>
+</helm_registry>
index a140666aca5d3d2434f78bcd6d3bac75592ed246..625f43f5b2136df6d9ae096837dce26e54578428 100644 (file)
@@ -30,28 +30,29 @@ module C = MQIConn
 
 open Http_types ;;
 
-let debug = true;;
+let debug = false;;
 let debug_print s = if debug then prerr_endline s;;
 Http_common.debug := true;;
 (* Http_common.debug := true;; *)
 
-  (** accepted HTTP servers for ask_uwobo method forwarding *)
-let valid_servers =
- [ "mowgli.cs.unibo.it:58080" ; "mowgli.cs.unibo.it" ; "localhost:58080" ];;
-
 let mqi_flags = [] (* default MathQL interpreter options *)
 
 open Printf;;
 
 let daemon_name = "Search Engine";;
-let default_port = 58085;;
-let port_env_var = "SEARCH_ENGINE_PORT";;
 
-let pages_dir =
-  try
-    Sys.getenv "SEARCH_ENGINE_HTML_DIR"
-  with Not_found -> "html"  (* relative to searchEngine's document root *)
+  (* First of all we load the configuration *)
+let _ =
+ let configuration_file = "/projects/helm/etc/searchEngine.conf.xml" in
+  Helm_registry.load_from configuration_file
 ;;
+
+let pages_dir = Helm_registry.get "search_engine.html_dir";;
+
+  (** accepted HTTP servers for ask_uwobo method forwarding *)
+let valid_servers= Helm_registry.get_string_list "search_engine.valid_servers";;
+
+
 let interactive_user_uri_choice_TPL = pages_dir ^ "/templateambigpdq1.html";;
 let interactive_interpretation_choice_TPL =
   pages_dir ^ "/templateambigpdq2.html";;
@@ -155,15 +156,7 @@ let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE,
   Pcre.regexp "@VARIABLES_INITIALIZATION@")
 let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$"
 
-let port =
-  try
-    int_of_string (Sys.getenv port_env_var)
-  with
-  | Not_found -> default_port
-  | Failure "int_of_string" ->
-      prerr_endline "Warning: invalid port, reverting to default";
-      default_port
-;;
+let port = Helm_registry.get_int "search_engine.port";;
 
 let pp_error = sprintf "<html><body><h1>Error: %s</h1></body></html>";;
 
@@ -356,13 +349,9 @@ let callback (req: Http_types.request) outchan =
     | "/locateInductivePrinciple" ->
         let mqi_handle = C.init mqi_flags debug_print in
         let term_string = req#param "term" in
-        let lexbuf = Lexing.from_string term_string in
         let (context, metasenv) = ([], []) in
-        let (dom, mk_metasenv_and_expr) =
-          CicTextualParserContext.main
-            ~context ~metasenv CicTextualLexer.token lexbuf
-        in
         let id_to_uris_raw = req#param "aliases" in
+(*XXX
         let tokens = Pcre.split ~pat:"\\s" id_to_uris_raw in
         let rec parse_tokens keys lookup = function (* TODO spostarla fuori *)
           | [] -> keys, lookup
@@ -378,6 +367,7 @@ let callback (req: Http_types.request) outchan =
                  rest
           | _ -> failwith "Can't parse aliases"
         in
+*)
         let parse_choices choices_raw =
           let choices = Pcre.split ~pat:";" choices_raw in
           List.fold_left
@@ -386,8 +376,6 @@ let callback (req: Http_types.request) outchan =
               | ""::id::tail
               | id::tail when id<>"" ->
                   (fun id' ->
-prerr_endline ("#### " ^ id ^ " :=");
-List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
                     if id = id' then
                       Some (List.map (fun u -> Netencoding.Url.decode u) tail)
                     else
@@ -396,34 +384,19 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
             (fun _ -> None)
             choices
         in
-        let (id_to_uris : Disambiguate.domain_and_interpretation) =
-         parse_tokens [] (fun _ -> None) tokens in
+        let id_to_uris =
+         DisambiguatingParser.EnvironmentP3.of_string id_to_uris_raw in
+print_endline ("id_to_uris_raw: " ^ id_to_uris_raw) ;
+print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id_to_uris)) ;
         let id_to_choices =
           try
             let choices_raw = req#param "choices" in
             parse_choices choices_raw
           with Http_types.Param_not_found _ -> (fun _ -> None)
         in
-        let module Chat: Disambiguate.Callbacks =
+        let module Chat: DisambiguateTypes.Callbacks =
           struct
 
-            let get_metasenv () =
-             !CicTextualParser0.metasenv
-
-            let set_metasenv metasenv =
-              CicTextualParser0.metasenv := metasenv
-
-            let output_html ?(append_NL = true) html_msg =
-              let rec collect_string = function
-                | `BR -> "\n"
-                | `T s -> s
-                | `L tags -> String.concat "" (List.map collect_string tags)
-              in
-              match html_msg with
-              | `Error msg | `Msg msg ->
-                  (if append_NL then prerr_endline else prerr_string)
-                    (collect_string msg ^ (if append_NL then "\n" else ""))
-
             let interactive_user_uri_choice
               ~selection_mode ?ok
               ?enable_button_for_non_vars ~(title: string) ~(msg: string)
@@ -466,7 +439,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
                       (String.concat "<br />"
                         (List.map
                           (fun (id, value) ->
-                            (sprintf "alias %s %s" id value))
+                            (sprintf "alias id %s = %s" id value))
                           l)) ^
                       "\'")
                   interpretations)
@@ -479,7 +452,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
                       (String.concat " "
                         (List.map
                           (fun (id, value) ->
-                            (sprintf "alias %s %s"
+                            (sprintf "alias id %s = %s"
                               id
                               (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
                                 value)))
@@ -506,10 +479,10 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
 
           end
         in
-        let module Disambiguate' = Disambiguate.Make (Chat) in
+        let module Disambiguate' = DisambiguatingParser.Make(Chat) in
         let (id_to_uris', metasenv', term') =
-          Disambiguate'.disambiguate_input mqi_handle
-            context metasenv dom mk_metasenv_and_expr id_to_uris
+          Disambiguate'.disambiguate_term mqi_handle
+            context metasenv term_string id_to_uris
         in
         (match metasenv' with
         | [] ->
@@ -596,6 +569,8 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
              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 ", "
@@ -613,6 +588,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
                                | _ -> assert false (*CSC: completare *)))
                            domain)
                  in
+*)
                  let processed_line =
                    apply_substs
                      [results_RE, theory_of_result results ;