better checks on elim input, two conditions are now required for an

input to elim to be valid:
1) before the disambiguation an indentifier has been given by the user
2) after the disambiguation a MutInd Cic term has been created

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index cef70799e6c1a39c55c88b13f91ec225ccdc26db..d8af6b10e566bb8e3e2c46c9881e6adaf8edaac1 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -33,6 +33,9 @@ exception Chat_unfinished
 exception Unbound_identifier of string
 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"
 
@@ -115,6 +118,7 @@ let add_param_substs params =
       params)
 
 let page_RE = Pcre.regexp "&param\\.page=\\d+"
+let identifier_RE = Pcre.regexp "^\\s*\\w+\\s*$"
 
 let query_kind_of_req (req: Http_types.request) =
   match req#path with
@@ -227,123 +231,132 @@ let send_results results
 
 let exec_action dbd (req: Http_types.request) outchan =
   let term_str = req#param "expression" in
-  let (context, metasenv) = ([], []) in
-  let id_to_uris_raw = 
-    try req#param "aliases" 
-    with Http_types.Param_not_found _ -> ""
-  in
-  let parse_interpretation_choices choices =
-    List.map int_of_string (Pcre.split ~pat:" " choices) in
-  let parse_choices choices_raw =
-    let choices = Pcre.split ~pat:";" choices_raw in
-    List.fold_left
-      (fun f x ->
-         match Pcre.split ~pat:"\\s" x with
-           | ""::id::tail
-           | id::tail when id<>"" ->
-               (fun id' ->
-                  if id = id' then
-                    Some (List.map (fun u -> Netencoding.Url.decode u) tail)
-                  else
-                    f id')
-           | _ -> failwith "Can't parse choices")
-      (fun _ -> None)
-      choices
-  in
-  let id_to_uris = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in
-  let id_to_choices =
-    try
-      parse_choices (req#param "choices")
-    with Http_types.Param_not_found _ -> (fun _ -> None)
-  in
-  let interpretation_choices =
-    try
-      let choices_raw = req#param "interpretation_choices" in
-      if choices_raw = "" then None 
-      else Some (parse_interpretation_choices choices_raw)
-    with Http_types.Param_not_found _ -> None
-  in 
-  let module Chat: DisambiguateTypes.Callbacks =
-    struct
-      let interactive_user_uri_choice ~selection_mode ?ok
-        ?enable_button_for_non_vars ~(title: string) ~(msg: string)
-        ~(id: string) (choices: string list)
-      =
-        match id_to_choices id with
-        | Some choices -> choices
-        | None -> List.filter nonvar choices
+  try
+    if req#path = "/elim" && not (Pcre.pmatch ~rex:identifier_RE term_str) then
+      raise Not_a_MutInd;
+    let (context, metasenv) = ([], []) in
+    let id_to_uris_raw = 
+      try req#param "aliases" 
+      with Http_types.Param_not_found _ -> ""
+    in
+    let parse_interpretation_choices choices =
+      List.map int_of_string (Pcre.split ~pat:" " choices) in
+    let parse_choices choices_raw =
+      let choices = Pcre.split ~pat:";" choices_raw in
+      List.fold_left
+        (fun f x ->
+           match Pcre.split ~pat:"\\s" x with
+             | ""::id::tail
+             | id::tail when id<>"" ->
+                 (fun id' ->
+                    if id = id' then
+                      Some (List.map (fun u -> Netencoding.Url.decode u) tail)
+                    else
+                      f id')
+             | _ -> failwith "Can't parse choices")
+        (fun _ -> None)
+        choices
+    in
+    let id_to_uris = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in
+    let id_to_choices =
+      try
+        parse_choices (req#param "choices")
+      with Http_types.Param_not_found _ -> (fun _ -> None)
+    in
+    let interpretation_choices =
+      try
+        let choices_raw = req#param "interpretation_choices" in
+        if choices_raw = "" then None 
+        else Some (parse_interpretation_choices choices_raw)
+      with Http_types.Param_not_found _ -> None
+    in 
+    let module Chat: DisambiguateTypes.Callbacks =
+      struct
+        let interactive_user_uri_choice ~selection_mode ?ok
+          ?enable_button_for_non_vars ~(title: string) ~(msg: string)
+          ~(id: string) (choices: string list)
+        =
+          match id_to_choices id with
+          | Some choices -> choices
+          | None -> List.filter nonvar choices
 
-      let interactive_interpretation_choice interpretations =
-        match interpretation_choices with
-        | Some l -> l
-        | None ->
-            let html_interpretations =
-              MooglePp.html_of_interpretations interpretations
-            in
-            Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
-            Http_daemon.send_CRLF outchan ;
-            let advanced =
-              try
-                req#param "advanced"
-              with Http_types.Param_not_found _ -> "no"
-            in
-            let query_kind = query_kind_of_req req in
-            iter_file
-              (fun line ->
-                 let processed_line =
-                   apply_substs
-                     [ tag "SEARCH_ENGINE_URL", my_own_url;
-                       tag "ADVANCED", advanced;
-                       tag "INTERPRETATIONS", html_interpretations;
-                       tag "CURRENT_CHOICES", req#param "choices";
-                       tag "EXPRESSION", html_encode (req#param "expression");
-                       tag "QUERY_KIND", query_kind;
-                       tag "QUERY_SUMMARY", "disambiguation";
-                       tag "ACTION", string_tail req#path ]
-                     line
-                 in
-                 output_string outchan (processed_line ^ "\n"))
-              choices_TPL;
-            raise Chat_unfinished
+        let interactive_interpretation_choice interpretations =
+          match interpretation_choices with
+          | Some l -> l
+          | None ->
+              let html_interpretations =
+                MooglePp.html_of_interpretations interpretations
+              in
+              Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
+              Http_daemon.send_CRLF outchan ;
+              let advanced =
+                try
+                  req#param "advanced"
+                with Http_types.Param_not_found _ -> "no"
+              in
+              let query_kind = query_kind_of_req req in
+              iter_file
+                (fun line ->
+                   let processed_line =
+                     apply_substs
+                       [ tag "SEARCH_ENGINE_URL", my_own_url;
+                         tag "ADVANCED", advanced;
+                         tag "INTERPRETATIONS", html_interpretations;
+                         tag "CURRENT_CHOICES", req#param "choices";
+                         tag "EXPRESSION", html_encode (req#param "expression");
+                         tag "QUERY_KIND", query_kind;
+                         tag "QUERY_SUMMARY", "disambiguation";
+                         tag "ACTION", string_tail req#path ]
+                       line
+                   in
+                   output_string outchan (processed_line ^ "\n"))
+                choices_TPL;
+              raise Chat_unfinished
 
-      let input_or_locate_uri ~title ?id () =
-        match id with
-        | Some id -> raise (Unbound_identifier id)
-        | None -> assert false
-    end
-  in
-  let module Disambiguate' = Disambiguate.Make(Chat) in
-  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
-    with
-    | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
-    | _ -> assert false
-  in
-  let uris =
-    match req#path with
-    | "/match" -> MetadataQuery.match_term ~dbd term
-    | "/hint" ->
-        let status = ProofEngineTypes.initial_status term metasenv in
-        let intros = PrimitiveTactics.intros_tac () in
-        let subgoals = ProofEngineTypes.apply_tactic intros status in
-        (match subgoals with
-        | proof, [goal] ->
-            let (uri,metasenv,bo,ty) = proof in
-            List.map fst (MetadataQuery.hint ~dbd (proof, goal))
-        | _ -> assert false)
-    | "/elim" ->
-        let uri =
-          match term with
-          | Cic.MutInd (uri, typeno, _) ->
-              UriManager.string_of_uriref (uri, [typeno])
-          | _ -> assert false
-        in
-        MetadataQuery.elim ~dbd uri
-    | _ -> assert false
-  in
-  send_results ~id_to_uris (`Results uris) req outchan
+        let input_or_locate_uri ~title ?id () =
+          match id with
+          | Some id -> raise (Unbound_identifier id)
+          | None -> assert false
+      end
+    in
+    let module Disambiguate' = Disambiguate.Make(Chat) in
+    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
+      with
+      | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
+      | _ -> assert false
+    in
+    let uris =
+      match req#path with
+      | "/match" -> MetadataQuery.match_term ~dbd term
+      | "/hint" ->
+          let status = ProofEngineTypes.initial_status term metasenv in
+          let intros = PrimitiveTactics.intros_tac () in
+          let subgoals = ProofEngineTypes.apply_tactic intros status in
+          (match subgoals with
+          | proof, [goal] ->
+              let (uri,metasenv,bo,ty) = proof in
+              List.map fst (MetadataQuery.hint ~dbd (proof, goal))
+          | _ -> assert false)
+      | "/elim" ->
+          let uri =
+            match term with
+            | Cic.MutInd (uri, typeno, _) ->
+                UriManager.string_of_uriref (uri, [typeno])
+            | _ -> raise Not_a_MutInd
+          in
+          MetadataQuery.elim ~dbd uri
+      | _ -> assert false
+    in
+    send_results ~id_to_uris (`Results uris) req outchan
+  with
+  | Not_a_MutInd ->
+      send_results (`Error (MooglePp.pp_error "Not an inductive type"
+        ("elim requires as input an identifier corresponding to an inductive"
+         ^ " type")))
+        req outchan
 
 let callback dbd (req: Http_types.request) outchan =
   try
@@ -406,7 +419,7 @@ let callback dbd (req: Http_types.request) outchan =
   | Http_types.Param_not_found attr_name ->
       bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
   | CicTextualParser2.Parse_error (_, msg) ->
-      send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan
+      send_results (`Error (MooglePp.pp_error "Parse error" msg)) req outchan
   | Unbound_identifier id ->
       send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
         outchan