- in
- let universe,
- ((must_obj, must_rel, must_sort) as must'),
- ((only_obj, only_rel, only_sort) as only) =
- get_constraints term' req#path
- in
- let must'', only' =
- (try
- add_user_constraints
- ~constraints:(req#param "constraints")
- (must', only)
- with Http_types.Param_not_found _ ->
- if req#param "advanced" = "no" then
- (must',only)
- else
- let variables =
- "var aliases = '" ^ id_to_uris_raw ^ "';\n" ^
- "var constr_obj_len = " ^
- string_of_int (List.length must_obj) ^ ";\n" ^
- "var constr_rel_len = " ^
- string_of_int (List.length must_rel) ^ ";\n" ^
- "var constr_sort_len = " ^
- string_of_int (List.length must_sort) ^ ";\n" in
- let form =
- (if must_obj = [] then "" else
- "<h4>Obj constraints</h4>" ^
- "<table>" ^
- (String.concat "\n" (List.map html_of_r_obj must_obj)) ^
- "</table>" ^
- (* The following three lines to make Javascript create *)
- (* the constr_obj[] and obj_depth[] arrays even if we *)
- (* have only one real entry. *)
- "<input type=\"hidden\" name=\"constr_obj\" />" ^
- "<input type=\"hidden\" name=\"obj_depth\" />") ^
- (if must_rel = [] then "" else
- "<h4>Rel constraints</h4>" ^
- "<table>" ^
- (String.concat "\n" (List.map html_of_r_rel must_rel)) ^
- "</table>" ^
- (* The following two lines to make Javascript create *)
- (* the constr_rel[] and rel_depth[] arrays even if *)
- (* we have only one real entry. *)
- "<input type=\"hidden\" name=\"constr_rel\" />" ^
- "<input type=\"hidden\" name=\"rel_depth\" />") ^
- (if must_sort = [] then "" else
- "<h4>Sort constraints</h4>" ^
- "<table>" ^
- (String.concat "\n" (List.map html_of_r_sort must_sort)) ^
- "</table>" ^
- (* The following two lines to make Javascript create *)
- (* the constr_sort[] and sort_depth[] arrays even if *)
- (* we have only one real entry. *)
- "<input type=\"hidden\" name=\"constr_sort\" />" ^
- "<input type=\"hidden\" name=\"sort_depth\" />") ^
- "<h4>Only constraints</h4>" ^
- "Enforce Only constraints for objects: " ^
- "<input type='checkbox' name='only_obj'" ^
- (if only_obj = None then "" else " checked='yes'") ^
- " /><br />" ^
- "Enforce Rel constraints for objects: " ^
- "<input type='checkbox' name='only_rel'" ^
- (if only_rel = None then "" else " checked='yes'") ^
- " /><br />" ^
- "Enforce Sort constraints for objects: " ^
- "<input type='checkbox' name='only_sort'" ^
- (if only_sort = None then "" else " checked='yes'") ^
- " /><br />"
- in
- Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
- Http_daemon.send_CRLF outchan ;
- iter_file
- (fun line ->
- let processed_line =
- apply_substs
- [form_RE, form ;
- variables_initialization_RE, variables;
- advanced_tag_RE, req#param "advanced";
- current_choices_tag_RE, req#param "choices";
- interpretations_RE, req#param "interpretation_choices";
- expression_tag_RE, req#param "expression";
- action_tag_RE, string_tail req#path] line
- in
- output_string outchan (processed_line ^ "\n"))
- constraints_choice_TPL;
- raise Chat_unfinished)
- in
- let query =
- G.query_of_constraints universe must'' only'
- in
- let results = MQueryInterpreter.execute mqi_handle query in
- send_results results ~id_to_uris:id_to_uris' req outchan
-in
-
-(* HTTP DAEMON CALLBACK *)
-
-let build_dynamic_uri url params =
- let p =
- String.concat "&" (List.map (fun (key,value) -> (key ^ "=" ^ (Netencoding.Url.encode value))) params) in
- url ^ "?" ^ p
-in
-
-let build_uwobo_request (req: Http_types.request) outchan =
- prerr_endline ("ECCOLO: " ^ req#param "param.SEARCH_ENGINE_URL");
- let xmluri = build_dynamic_uri ((req#param "param.SEARCH_ENGINE_URL") ^ "/search") req#params in
- prerr_endline ("xmluri: " ^ xmluri);
- (*let xmluri = Netencoding.Url.encode xmluri in*)
- let server_and_port = req#param "param.processorURL" in
- let newreq =
- build_dynamic_uri
- (server_and_port ^ "apply")
- (("xmluri",xmluri)::("keys",(req#param "param.thkeys"))::req#params) in
- (* if List.mem server_and_port valid_servers then *)
- prerr_endline newreq;
- if true then
- Http_daemon.respond
- ~headers:["Content-Type", "text/html"]
- ~body:(Http_client.http_get newreq)
- outchan
- else
- Http_daemon.respond
- ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port ^
- (String.concat "\n" valid_servers)))
- outchan
-in
-
-let proxy url outchan =
- let server_and_port =
- (Pcre.extract ~rex:server_and_port_url_RE url).(1)
- in
- if List.mem server_and_port valid_servers then
- Http_daemon.respond
- ~headers:["Content-Type", "text/html"]
- ~body:(Http_client.http_get url)
- outchan
- else
- Http_daemon.respond
- ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port))
- outchan
-in
+ in
+ 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
+ let subgoals = ProofEngineTypes.apply_tactic intros status in
+ (match subgoals with
+ | proof, [goal] ->
+ let (uri,metasenv,bo,ty) = proof in
+ List.map fst (MetadataQuery.experimental_hint ~dbd (proof, goal))
+ | _ -> assert false)
+ | "/elim" ->
+ let uri =
+ match term with
+ | Cic.MutInd (uri, typeno, _) ->
+ UriManager.uri_of_uriref uri typeno None
+ | _ -> raise Not_a_MutInd
+ in
+ MetadataQuery.elim ~dbd uri
+ | _ -> assert false
+ in
+ let uris = List.map UriManager.string_of_uri uris 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