added the support for the "Locate Inductive Principles" query

[helm.git] / helm / searchEngine / searchEngine.ml

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index e4e33c629c4f808204dd2b48dcb03057fc6b8240..622f10bd5a618979fcf19551b1c32a659536cd99 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -155,8 +155,6 @@ 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://([^/]+)/.*$"
 
-exception NotAnInductiveDefinition
-
 let port =
   try
     int_of_string (Sys.getenv port_env_var)
@@ -180,29 +178,20 @@ let contype = "Content-Type", "text/html";;
 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 =
-       [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)]
-      in
-      let constr_rel = [`MainConclusion None] in
-      let constr_sort = [(`MainHypothesis (Some 1), T.Prop)] in
-       U.universe_for_search_pattern,
-        (constr_obj, constr_rel, constr_sort), (None,None,None)
+      CGLocateInductive.universe,
+      (CGLocateInductive.get_constraints term),
+      (None,None,None)
     | "/searchPattern" ->
      let constr_obj, constr_rel, constr_sort =
        CGSearchPattern.get_constraints term in
-      U.universe_for_search_pattern,
+      CGSearchPattern.universe,
        (constr_obj, constr_rel, constr_sort),
        (Some constr_obj, Some constr_rel, Some constr_sort)
     | "/matchConclusion" ->
      let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in
 (* FG: there is no way to choose the block number ***************************)
      let block = pred (List.length list_of_must) in 
-      U.universe_for_match_conclusion, 
+      CGMatchConclusion.universe, 
       (List.nth list_of_must block, [], []), (Some only, None, None)
     | _ -> assert false
 ;;