snapshot (first version in which some extensions work, e.g. infix +)

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

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index d8af6b10e566bb8e3e2c46c9881e6adaf8edaac1..655235c1e538121ca0b72bc124a90bc47db2b139 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -36,8 +36,8 @@ exception Invalid_action of string  (* invalid action for "/search" method *)
   (** raised by elim when a MutInd is required but not found *)
 exception Not_a_MutInd
 
-let daemon_name = "Moogle"
-let configuration_file = "/projects/helm/etc/moogle.conf.xml"
+let daemon_name = "Whelp"
+let configuration_file = "/projects/helm/etc/whelp.conf.xml"
 
 let placeholders = [
   "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES";
@@ -126,6 +126,7 @@ let query_kind_of_req (req: Http_types.request) =
   | "/hint" -> "Hint"
   | "/locate" -> "Locate"
   | "/elim" -> "Elim"
+  | "/instance" -> "Instance"
   | _ -> ""
 
   (* given a uri with a query part in input try to find in it a string
@@ -323,7 +324,8 @@ let exec_action dbd (req: Http_types.request) outchan =
     let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
     let (id_to_uris, metasenv, term) =
       match
-        Disambiguate'.disambiguate_term dbd context metasenv ast id_to_uris
+        Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
+          ~aliases:id_to_uris ast
       with
       | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
       | _ -> assert false
@@ -331,6 +333,7 @@ let exec_action dbd (req: Http_types.request) outchan =
     let uris =
       match req#path with
       | "/match" -> MetadataQuery.match_term ~dbd term
+      | "/instance" -> MetadataQuery.instance ~dbd term
       | "/hint" ->
           let status = ProofEngineTypes.initial_status term metasenv in
           let intros = PrimitiveTactics.intros_tac () in
@@ -338,7 +341,7 @@ let exec_action dbd (req: Http_types.request) outchan =
           (match subgoals with
           | proof, [goal] ->
               let (uri,metasenv,bo,ty) = proof in
-              List.map fst (MetadataQuery.hint ~dbd (proof, goal))
+              List.map fst (MetadataQuery.experimental_hint ~dbd (proof, goal))
           | _ -> assert false)
       | "/elim" ->
           let uri =
@@ -409,6 +412,7 @@ let callback dbd (req: Http_types.request) outchan =
         end
     | "/hint"
     | "/elim"
+    | "/instance"
     | "/match" -> exec_action dbd req outchan
     | invalid_request ->
         Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))