From: Enrico Tassi Date: Tue, 9 May 2006 13:41:00 +0000 (+0000) Subject: half ported to the "new" module organization. X-Git-Tag: make_still_working~7383 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3b875dad94c1835059450dc0de3b1e2779aff454;p=helm.git half ported to the "new" module organization. --- diff --git a/helm/software/daemons/graphs/tools/Makefile b/helm/software/daemons/graphs/tools/Makefile index 072667031..bef00fca3 100644 --- a/helm/software/daemons/graphs/tools/Makefile +++ b/helm/software/daemons/graphs/tools/Makefile @@ -6,8 +6,9 @@ SED=cat REQUIRES = http helm-registry PREDICATES = mt OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLFIND = OCAMLPATH=../../../components/METAS/ ocamlfind +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) EXECUTABLES = uriSetQueue drawGraph EXECUTABLES_OPT = $(patsubst %,%.opt,$(EXECUTABLES)) diff --git a/helm/software/daemons/proofChecker/Makefile b/helm/software/daemons/proofChecker/Makefile index af48d0a5d..ae957785c 100644 --- a/helm/software/daemons/proofChecker/Makefile +++ b/helm/software/daemons/proofChecker/Makefile @@ -2,12 +2,13 @@ BIN_DIR = /usr/local/bin REQUIRES = helm-cic_proof_checking http PREDICATES = OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -g -OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLFIND = OCAMLPATH=../../components/METAS/ ocamlfind +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) -g +OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) OCAMLDEP = ocamldep -LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) +LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) +LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) all: $(PROOFCHECKEROBJS) proofChecker opt: $(PROOFCHECKEROBJS:.cmo=.cmx) proofChecker.opt diff --git a/helm/software/daemons/rdfly/Makefile b/helm/software/daemons/rdfly/Makefile index 779bb7b44..87ef3be5f 100644 --- a/helm/software/daemons/rdfly/Makefile +++ b/helm/software/daemons/rdfly/Makefile @@ -2,7 +2,7 @@ BIN_DIR = /usr/local/bin REQUIRES = mysql http helm-registry PREDICATES = OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -OCAMLFIND = ocamlfind +OCAMLFIND = OCAMLPATH=../../components/METAS/ ocamlfind OCAMLC = $(OCAMLFIND) ocamlc -thread $(OCAMLOPTIONS) OCAMLOPT = $(OCAMLFIND) ocamlopt -thread $(OCAMLOPTIONS) OCAMLDEP = ocamldep -pp camlp4o diff --git a/helm/software/daemons/uwobo/Makefile b/helm/software/daemons/uwobo/Makefile index 00b578aca..dc571a6b9 100644 --- a/helm/software/daemons/uwobo/Makefile +++ b/helm/software/daemons/uwobo/Makefile @@ -3,7 +3,7 @@ DISTDIR = uwobo-$(VERSION) DISTTARBALL = $(DISTDIR).tar.gz REQUIRES = http gdome2 gdome2-xslt pcre unix helm-registry COMMONOPTS = -package "$(REQUIRES)" -pp camlp4o -OCAMLFIND = ocamlfind +OCAMLFIND = OCAMLPATH=../../components/METAS ocamlfind OCAMLC = $(OCAMLFIND) ocamlc $(COMMONOPTS) OCAMLOPT = $(OCAMLFIND) ocamlopt $(COMMONOPTS) OCAMLDEP = $(OCAMLFIND) ocamldep $(COMMONOPTS) diff --git a/helm/software/daemons/whelp/Makefile b/helm/software/daemons/whelp/Makefile index 2ae59df91..c57e6e1f3 100644 --- a/helm/software/daemons/whelp/Makefile +++ b/helm/software/daemons/whelp/Makefile @@ -1,8 +1,9 @@ -REQUIRES = http helm-cic_textual_parser2 helm-logger helm-tactics +REQUIRES = http helm-grafite_parser helm-logger helm-tactics helm-cic_disambiguation OCAMLOPTIONS = -thread -package "$(REQUIRES)" -pp camlp4o -OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) -OCAMLDEP = ocamlfind ocamldep -package "$(REQUIRES)" -pp camlp4o +OCAMLFIND = OCAMLPATH=../../components/METAS ocamlfind +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = $(OCAMLFIND) ocamldep -package "$(REQUIRES)" -pp camlp4o MODULES = mooglePp SRCS = $(patsubst %,%.ml,$(MODULES)) $(patsubst %,%.mli,$(MODULES)) \ diff --git a/helm/software/daemons/whelp/mooglePp.ml b/helm/software/daemons/whelp/mooglePp.ml index 3af0afb40..026200b20 100644 --- a/helm/software/daemons/whelp/mooglePp.ml +++ b/helm/software/daemons/whelp/mooglePp.ml @@ -62,7 +62,7 @@ let html_of_interpretations interps = sprintf "\n%s\n
" (String.concat "\n" (List.map - (fun (k, v) -> + (fun (_, k, v) -> sprintf "%s%s" k v) interp)) in diff --git a/helm/software/daemons/whelp/mooglePp.mli b/helm/software/daemons/whelp/mooglePp.mli index f3e2e5952..b01b504f2 100644 --- a/helm/software/daemons/whelp/mooglePp.mli +++ b/helm/software/daemons/whelp/mooglePp.mli @@ -31,5 +31,5 @@ val pp_error : string -> string -> string * QUERY_SUMMARY and QUERY_RESULTS tag in moogle's main template *) val theory_of_result : int -> string list -> string * string -val html_of_interpretations: (string * string) list list -> string +val html_of_interpretations: ('a * string * string) list list -> string diff --git a/helm/software/daemons/whelp/searchEngine.ml b/helm/software/daemons/whelp/searchEngine.ml index c42c01043..26c1def3e 100644 --- a/helm/software/daemons/whelp/searchEngine.ml +++ b/helm/software/daemons/whelp/searchEngine.ml @@ -115,7 +115,7 @@ let add_param_substs params = 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+" @@ -155,7 +155,7 @@ let fold_n_to_m f n m acc = 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 @@ -292,7 +292,9 @@ let exec_action dbd (req: Http_types.request) outchan = (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") @@ -315,7 +317,7 @@ let exec_action dbd (req: Http_types.request) outchan = | 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 -> @@ -359,22 +361,21 @@ let exec_action dbd (req: Http_types.request) outchan = 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 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" -> @@ -384,10 +385,15 @@ let exec_action dbd (req: Http_types.request) outchan = 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 -> @@ -442,7 +448,7 @@ let callback dbd (req: Http_types.request) outchan = if expression = "" then send_results (`Results []) req outchan else begin - let results = MetadataQuery.locate ~dbd expression in + let results = Whelp.locate ~dbd expression in let results = List.map UriManager.string_of_uri results in send_results (`Results results) req outchan end @@ -458,7 +464,7 @@ let callback dbd (req: Http_types.request) outchan = | 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 | Unbound_identifier id -> send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req @@ -482,9 +488,12 @@ let restore_environment () = 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") - + let _ = assert false in () + (* + CicNotation.load_notation (Helm_registry.get "search_engine.notations"); + CicNotation.load_notation (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 ()); @@ -492,7 +501,7 @@ let _ = flush stdout; Unix.putenv "http_proxy" ""; let dbd = - Mysql.quick_connect + HMysql.quick_connect ~host:(Helm_registry.get "db.host") ~database:(Helm_registry.get "db.database") ~user:(Helm_registry.get "db.user")