exception Not_a_MutInd
let daemon_name = "Whelp"
-let configuration_file = "/projects/helm/etc/whelp.conf.xml"
+let configuration_file = "searchEngine.conf.xml"
let placeholders = [
"ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES";
let key' = (Pcre.extract ~pat:"param\\.(.*)" key).(1) in
Pcre.regexp ("@" ^ key' ^ "@"), value)
(List.filter
- (fun ((key,_) as p) -> Pcre.pmatch ~pat:"^param\\." key)
+ (fun (key,_) -> Pcre.pmatch ~pat:"^param\\." key)
params)
let page_RE = Pcre.regexp "¶m\\.page=\\d+"
aux acc n
let send_results results
- ?(id_to_uris = DisambiguateTypes.empty_environment)
+ ?(id_to_uris = DisambiguateTypes.Environment.empty)
(req: Http_types.request) outchan
=
let query_kind = query_kind_of_req req in
moogle_TPL
let exec_action dbd (req: Http_types.request) outchan =
+ let dbd = dbd () in
let term_str = req#param "expression" in
try
if req#path = "/elim" &&
(fun _ -> None)
choices
in
- let id_to_uris = DisambiguatePp.parse_environment id_to_uris_raw in
+ let id_to_uris,_ =
+ CicNotation2.parse_environment id_to_uris_raw ~include_paths:[]
+ in
let id_to_choices =
try
parse_choices (req#param "choices")
| Some choices -> choices
| None -> List.filter nonvar choices
- let interactive_interpretation_choice interpretations =
+ let interactive_interpretation_choice _ _ interpretations =
match interpretation_choices with
| Some l -> l
| None ->
end
in
let module Disambiguate' = Disambiguate.Make(Chat) in
- let ast = Grammar.Entry.parse CicNotationParser.term (Stream.of_string term_str) in
+ let ast =
+ CicNotationParser.parse_term (Ulexing.from_utf8_string term_str) in
let (id_to_uris, metasenv, term) =
match
Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
- ~aliases:id_to_uris ast
+ ~aliases:id_to_uris ~universe:None ("",0,ast)
with
- | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
+ | [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
- | "/instance" -> MetadataQuery.instance ~dbd term
+ | "/match" -> Whelp.match_term ~dbd term
+ | "/instance" -> Whelp.instance ~dbd term
| "/hint" ->
- let status = ProofEngineTypes.initial_status term metasenv in
+ 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" ->
UriManager.uri_of_uriref uri typeno None
| _ -> raise Not_a_MutInd
in
- MetadataQuery.elim ~dbd uri
+ Whelp.elim ~dbd uri
| _ -> assert false
in
let uris = List.map UriManager.string_of_uri uris in
+ let id_to_uris =
+ List.fold_left
+ (fun env (k,v) -> DisambiguateTypes.Environment.add k v env)
+ DisambiguateTypes.Environment.empty id_to_uris
+ in
send_results ~id_to_uris (`Results uris) req outchan
with
| Not_a_MutInd ->
if expression = "" then
send_results (`Results []) req outchan
else begin
- let results = MetadataQuery.locate ~dbd expression in
+ let results = Whelp.locate ~dbd:(dbd ()) expression in
let results = List.map UriManager.string_of_uri results in
send_results (`Results results) req outchan
end
| Chat_unfinished -> ()
| Http_types.Param_not_found attr_name ->
bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
- | CicNotationParser.Parse_error (_, msg) ->
+ | CicNotationParser.Parse_error msg ->
send_results (`Error (MooglePp.pp_error "Parse error" msg)) req outchan
+ | Stdpp.Exc_located (floc, Stream.Error msg) ->
+ send_results (`Error (MooglePp.pp_error "Parse error" msg)) req outchan
+ | Stdpp.Exc_located (floc, exn) ->
+ let msg = Printexc.to_string exn in
+ send_results (`Error (MooglePp.pp_error "Unknown error" msg)) req outchan
| Unbound_identifier id ->
send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
outchan
printf "done!\n"; flush stdout
let read_notation () =
- CicNotation.load_notation (Helm_registry.get "search_engine.notations");
- CicNotation.load_notation (Helm_registry.get "search_engine.interpretations")
-
+ ignore (CicNotation2.load_notation ~include_paths:[]
+ (Helm_registry.get "search_engine.notations"));
+ ignore (CicNotation2.load_notation ~include_paths:[]
+ (Helm_registry.get "search_engine.interpretations"))
+
let _ =
printf "%s started and listening on port %d\n" daemon_name port;
printf "Current directory is %s\n" (Sys.getcwd ());
printf "HTML directory is %s\n" pages_dir;
flush stdout;
Unix.putenv "http_proxy" "";
- let dbd =
- Mysql.quick_connect
- ~host:(Helm_registry.get "db.host")
- ~database:(Helm_registry.get "db.database")
- ~user:(Helm_registry.get "db.user")
- ()
+ let dbd () =
+ let dbd = LibraryDb.instance () in
+ MetadataTypes.ownerize_tables "searchEngine";
+ LibraryDb.create_owner_environment ();
+ dbd
in
restore_environment ();
read_notation ();
- Http_daemon.start' ~port (callback dbd);
+ let d_spec = Http_daemon.daemon_spec ~port ~callback:(callback dbd) ~auto_close:true () in
+ Http_daemon.main d_spec;
printf "%s is terminating, bye!\n" daemon_name
projects / helm.git / blobdiff