From: Claudio Sacerdoti Coen Date: Tue, 22 Apr 2003 10:19:42 +0000 (+0000) Subject: New queries added: X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=718bc0ea70defa418c23850dbb8f2850b0c3a542;p=helm.git New queries added: * Locate Inductive Principle * Match Conclusion (previously it was just a synonim for SearchPattern) --- diff --git a/helm/searchEngine/html/editorpdq.html b/helm/searchEngine/html/editorpdq.html index 27f070964..3370ed134 100644 --- 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 9182d26a6..1db28890a 100644 --- 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 - \ No newline at end of file + diff --git a/helm/searchEngine/html/query_choice.html b/helm/searchEngine/html/query_choice.html index 2f560bf0a..3e1932ad2 100644 --- a/helm/searchEngine/html/query_choice.html +++ b/helm/searchEngine/html/query_choice.html @@ -16,8 +16,9 @@ function armageddon() diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 2da581bf7..35270fd62 100644 --- 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 ;