]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 8721827)
New queries added:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 22 Apr 2003 10:19:42 +0000 (10:19 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 22 Apr 2003 10:19:42 +0000 (10:19 +0000)
 * Locate Inductive Principle
 * Match Conclusion (previously it was just a synonim for SearchPattern)

helm/searchEngine/html/editorpdq.html patch | blob | history
helm/searchEngine/html/index.html patch | blob | history
helm/searchEngine/html/mat_con.html patch | blob | history
helm/searchEngine/html/query_choice.html patch | blob | history
helm/searchEngine/searchEngine.ml patch | blob | history

diff --git a/helm/searchEngine/html/editorpdq.html b/helm/searchEngine/html/editorpdq.html
index 27f070964ad439b6589ffc3d52e5d8e5b5aff44a..3370ed1348c90a0e17432120409506d21ba384cf 100644 (file)
--- a/helm/searchEngine/html/editorpdq.html
+++ b/helm/searchEngine/html/editorpdq.html
@@ -37,7 +37,7 @@ function invia()
                        top.listaliases=top.listaliases+escape(top.aliasglob[i]+" ");
                        }
                //alert(top.listaliases);
-    window.open(top.ask_uwobo(top.topurl+"/searchPattern?term="+escape(document.invio.expression.value)+"&aliases="+top.listaliases),"cw");
+    window.open(top.ask_uwobo(top.topurl+"/"+top.current_query+"?term="+escape(document.invio.expression.value)+"&aliases="+top.listaliases),"cw");
         }
                //window.open(top.topurl+top.action+"templateambigpdq2.html","bw")}     
        else {alert("Please complete the query before.")}
diff --git a/helm/searchEngine/html/index.html b/helm/searchEngine/html/index.html
index 9182d26a6f7ba1f64dbec416ed8ad39c06b5b04c..1db28890a54639ff0137427063b1998da1ff27fb 100644 (file)
--- a/helm/searchEngine/html/index.html
+++ b/helm/searchEngine/html/index.html
@@ -485,7 +485,7 @@ function templateambigpdq1_listauri(document,elenco)
 function templateambigpdq1_invia(document,top,elenco,ident)
        {
        vecchiavlds=top.vlds.length;
-       stringa=top.topurl+"/searchPattern?term="+top.terminecic;
+       stringa=top.topurl+"/"+top.current_query+"?term="+top.terminecic;
        stringa=stringa+"&aliases="+top.listaliases;
        stringa=stringa+"&choices=";
         var choices = "";
@@ -550,7 +550,7 @@ function templateambigpdq2_listainterpretazioni(document,elenco,labels)
 
 function templateambigpdq2_invia(document,elenco)
        {
-       stringa=top.topurl+"/searchPattern?term="+top.terminecic;
+       stringa=top.topurl+"/"+top.current_query+"?term="+top.terminecic;
        stringa=stringa+"&aliases="+(top.listaliases==""?"":"%20");
        controllo=stringa.length;
        for (j=0;j<elenco.length;j++)
diff --git a/helm/searchEngine/html/mat_con.html b/helm/searchEngine/html/mat_con.html
index 3f4d37e41c7a35751fb03a9d09a9b98736337116..5fab873567a34cad28de3aac8c954de1c14e9df5 100644 (file)
--- a/helm/searchEngine/html/mat_con.html
+++ b/helm/searchEngine/html/mat_con.html
@@ -1,16 +1,10 @@
 <HTML>
 <HEAD>
 <SCRIPT language="Javascript">
-function checkint(grado)
-       {
-       if (isNaN(grado))
-               alert ("warning: you must enter a natural number in the grade box");
-       else if (Number(grado)<0|Number(grado)!=Math.floor(Number(grado))) alert ("warning: you must enter a natural number in the grade box");
-       }
 parent.mcq="[Alias list] [Expr]";
 parent.aggq();
 </SCRIPT>
 </HEAD>
 <BODY>
 </BODY>
-</HTML>
\ No newline at end of file
+</HTML>
diff --git a/helm/searchEngine/html/query_choice.html b/helm/searchEngine/html/query_choice.html
index 2f560bf0a0b378424b99bcea6bd5dad98a3510fe..3e1932ad2c98f3652ccd14f695289371a7a914e2 100644 (file)
--- a/helm/searchEngine/html/query_choice.html
+++ b/helm/searchEngine/html/query_choice.html
@@ -16,8 +16,9 @@ function armageddon()
 <form>
 <table><tr><td>
       <input type=radio name="qc" onFocus="top.cw.bw.location=top.topurl+top.action+'loc_obj.html';top.qw.location=top.topurl+top.action+'blank.html';top.sw.location=top.topurl+top.action+'blank.html';top.gw.location=top.topurl+top.action+'blank.html';parent.toq=1;this.blur();"> Locate Object<br>
-      <input type=radio name="qc" onFocus="top.cw.bw.location=top.topurl+top.action+'mat_con.html';top.qw.location=top.topurl+top.action+'blank.html';top.sw.location=top.topurl+top.action+'editorpdq.html';parent.toq=2;this.blur();"> Match Conclusion<br>
-      <input type=radio name="qc" onFocus="top.cw.bw.location=top.topurl+top.action+'mat_con.html';top.qw.location=top.topurl+top.action+'blank.html';top.sw.location=top.topurl+top.action+'editorpdq.html';parent.toq=3;this.blur();"> Search Pattern
+      <input type=radio name="qc" onFocus="top.cw.bw.location=top.topurl+top.action+'mat_con.html';top.qw.location=top.topurl+top.action+'blank.html';top.current_query='matchConclusion';top.sw.location=top.topurl+top.action+'editorpdq.html';parent.toq=2;this.blur();"> Match Conclusion<br>
+      <input type=radio name="qc" onFocus="top.cw.bw.location=top.topurl+top.action+'mat_con.html';top.qw.location=top.topurl+top.action+'blank.html';top.current_query='searchPattern';top.sw.location=top.topurl+top.action+'editorpdq.html';parent.toq=3;this.blur();"> Search Pattern<br>
+      <input type=radio name="qc" onFocus="top.cw.bw.location=top.topurl+top.action+'mat_con.html';top.qw.location=top.topurl+top.action+'blank.html';top.current_query='locateInductivePrinciple';top.sw.location=top.topurl+top.action+'editorpdq.html';parent.toq=3;this.blur();"> Locate Inductive Principle
 </td>
 </tr></table>
 </form>
diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 2da581bf7514799962a6f0c0eb60554a5be8abba..35270fd62c8ee31d46ca2469a819b94e57ebfeb8 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -108,6 +108,8 @@ let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE,
   Pcre.regexp "@RESULTS@", Pcre.regexp "@NEW_ALIASES@")
 let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$"
 
+exception NotAnInductiveDefinition
+
 let port =
   try
     int_of_string (Sys.getenv port_env_var)
@@ -125,7 +127,54 @@ let contype = "Content-Type", "text/html" in
 
 (* SEARCH ENGINE functions *)
 
-let refine_constraints (x, y, z) = (x, y, z), (Some x, Some y, Some z) in
+let refine_constraints (constr_obj, constr_rel, constr_sort) =
+ function
+    "/searchPattern" ->
+      (constr_obj, constr_rel, constr_sort),
+       (Some constr_obj, Some constr_rel, Some constr_sort)
+  | "/matchConclusion" ->
+      let constr_obj' =
+       List.map
+        (function (uri,pos,_) -> (uri,pos,None))
+        (List.filter
+          (function (uri,pos,depth) as constr ->
+            pos="http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
+            or
+            pos="http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
+          ) constr_obj)
+      in
+       (*CSC: we must select the must constraints here!!! *)
+       (constr_obj',[],[]),(Some constr_obj', None, None)
+  | _ -> assert false
+in
+
+let get_constraints term =
+ function
+    "/locateInductivePrinciple" ->
+      let uri = 
+       match term with
+          Cic.MutInd (uri,t,_) -> MQueryUtil.string_of_uriref (uri,[t])
+        | _ -> raise NotAnInductiveDefinition
+      in
+      let constr_obj =
+       [uri,"http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis",
+         None ;
+        uri,"http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis",
+         Some 0
+       ]
+      in
+      let constr_rel =
+       ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion",
+        None] in
+      let constr_sort =
+       ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis",
+        Some 1, "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"]
+      in
+       (constr_obj, constr_rel, constr_sort), (None,None,None)
+  | req_path ->
+     let must = MQueryLevels2.get_constraints term in
+      refine_constraints must req_path
+in
 
 (* HTTP DAEMON CALLBACK *)
 
@@ -198,7 +247,9 @@ let callback (req: Http_types.request) outchan =
         Http_daemon.respond
           ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port))
           outchan
-    | "/searchPattern" ->
+    | "/searchPattern"
+    | "/matchConclusion"
+    | "/locateInductivePrinciple" ->
         let term_string = req#param "term" in
         let lexbuf = Lexing.from_string term_string in
         let (context, metasenv) = ([], []) in
@@ -348,8 +399,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
         in
         (match metasenv' with
         | [] ->
-            let must = MQueryLevels2.get_constraints term' in
-            let must',only = refine_constraints must in
+            let must',only = get_constraints term' req#path in
             let results = MQueryGenerator.searchPattern must' only in 
             Http_daemon.send_basic_headers ~code:200 outchan ;
             Http_daemon.send_CRLF outchan ;
Unnamed repository; edit this file 'description' to name the repository.