From: Stefano Zacchiroli Date: Wed, 27 Apr 2005 12:32:02 +0000 (+0000) Subject: better checks on elim input, two conditions are now required for an X-Git-Tag: after_svn_merge~11 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=16065a413f4be50761d73be9dca3953ff9bfc1eb;p=helm.git 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 cef70799e..d8af6b10e 100644 --- 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 "¶m\\.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