From: Ferruccio Guidi Date: Tue, 29 Jul 2003 11:41:25 +0000 (+0000) Subject: - the mathql interpreter is not helm-dependent any more X-Git-Tag: LucaOK~18 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git - the mathql interpreter is not helm-dependent any more - fixed a bug in the "match conclusion" query of the search engine - gTopLevel/Makefile improved --- diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 076fef910..5f8063939 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -17,17 +17,17 @@ LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PRED all: styles gTopLevel opt: styles gTopLevel.opt -DEPOBJS = \ - proofEngine.ml proofEngine.mli logicalOperations.ml \ - logicalOperations.mli disambiguate.ml disambiguate.mli termEditor.ml \ - termEditor.mli texTermEditor.ml texTermEditor.mli xmlDiff.ml \ - xmlDiff.mli termViewer.ml termViewer.mli invokeTactics.ml \ - invokeTactics.mli hbugs.ml hbugs.mli gTopLevel.ml - -TOPLEVELOBJS = \ - proofEngine.cmo logicalOperations.cmo \ - disambiguate.cmo termEditor.cmo texTermEditor.cmo xmlDiff.cmo \ - termViewer.cmo invokeTactics.cmo hbugs.cmo gTopLevel.cmo +INTERFACE_FILES = \ + proofEngine.mli logicalOperations.mli disambiguate.mli \ + termEditor.mli texTermEditor.mli xmlDiff.mli termViewer.mli \ + invokeTactics.mli hbugs.mli + +DEPOBJS = $INTERFACE_FILES $(INTERFACE_FILES:%.mli=%.ml) gTopLevel.ml + +TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo + +$(INTERFACE_FILES:%.mli=%.cmo): $(LIBRARIES) +$(INTERFACE_FILES:%.mli=%.cmx): $(LIBRARIES_OPT) styles: @echo "***********************************************************************" diff --git a/helm/mathql_db_map.txt b/helm/mathql_db_map.txt new file mode 100644 index 000000000..33db1f0c8 --- /dev/null +++ b/helm/mathql_db_map.txt @@ -0,0 +1,26 @@ +dbname=mowgli user=helm + +objectname source <+ +objectname value <- objectName +refobj <- refObj +refobj source <- +refobj h_occurrence <- refObj h:occurrence +refobj h_position <- refObj h:position +refobj h_depth <- refObj h:depth +refrel <- refRel +refrel source <- +refrel h_position <- refRel h:position +refrel h_depth <- refRel h:depth +refsort <- refSort +refsort source <- +refsort h_sort <- refSort h:sort +refsort h_position <- refSort h:position +refsort h_depth <- refSort h:depth +backpointer <- backPointer +backpointer source <- backPointer h:occurrence +backpointer h_occurrence <- +backpointer h_position <- backPointer h:position +backpointer h_depth <- backPointer h:depth + +backpointer -> refobj + -> diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index 3b16bb6b0..349c2ac55 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -152,7 +152,6 @@ let text_of_query out x sep = | M.StatQuery x -> out "stat "; txt_set x | M.Keep b l x -> out "keep "; txt_allbut b; txt_path_list l; txt_set x - in txt_set x; out sep @@ -187,6 +186,36 @@ let stop_time (s0, u0) = let u1 = Unix.time () in Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0) +(* operations on lists *****************************************************) + +type 'a comparison = Lt + | Gt + | Eq of 'a + +let list_join f l1 l2 = + let rec aux = function + | [], v + | v, [] -> v + | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin + match f h1 h2 with + | Lt -> h1 :: aux (t1, v2) + | Gt -> h2 :: aux (v1, t2) + | Eq h -> h :: aux (t1, t2) + end + in aux (l1, l2) + +let list_meet f l1 l2 = + let rec aux = function + | [], v + | v, [] -> [] + | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin + match f h1 h2 with + | Lt -> aux (t1, v2) + | Gt -> aux (v1, t2) + | Eq h -> h :: aux (t1, t2) + end + in aux (l1, l2) + (* conversion functions *****************************************************) type uriref = UriManager.uri * (int list) diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli index 69aaebd77..bb38dc91d 100644 --- a/helm/ocaml/mathql/mQueryUtil.mli +++ b/helm/ocaml/mathql/mQueryUtil.mli @@ -40,6 +40,14 @@ val start_time : unit -> time val stop_time : time -> string +type 'a comparison = Lt + | Gt + | Eq of 'a + +val list_join : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list + +val list_meet : ('a -> 'a -> 'a comparison) -> 'a list -> 'a list -> 'a list + type uriref = UriManager.uri * (int list) diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index 927d5dcd0..962eaf63a 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -1,15 +1,20 @@ +mQIConn.cmi: mQIMap.cmi mQIProperty.cmi: mQIConn.cmi mQueryInterpreter.cmi: mQIConn.cmi mQueryMisc.cmo: mQueryMisc.cmi mQueryMisc.cmx: mQueryMisc.cmi -mQIPostgres.cmo: mQIPostgres.cmi -mQIPostgres.cmx: mQIPostgres.cmi -mQIConn.cmo: mQIPostgres.cmi mQIConn.cmi -mQIConn.cmx: mQIPostgres.cmx mQIConn.cmi mQIUtil.cmo: mQIUtil.cmi mQIUtil.cmx: mQIUtil.cmi -mQIProperty.cmo: mQIConn.cmi mQIPostgres.cmi mQIUtil.cmi mQIProperty.cmi -mQIProperty.cmx: mQIConn.cmx mQIPostgres.cmx mQIUtil.cmx mQIProperty.cmi +mQIPostgres.cmo: mQIPostgres.cmi +mQIPostgres.cmx: mQIPostgres.cmi +mQIMap.cmo: mQIMap.cmi +mQIMap.cmx: mQIMap.cmi +mQIConn.cmo: mQIMap.cmi mQIPostgres.cmi mQIConn.cmi +mQIConn.cmx: mQIMap.cmx mQIPostgres.cmx mQIConn.cmi +mQIProperty.cmo: mQIConn.cmi mQIMap.cmi mQIPostgres.cmi mQIUtil.cmi \ + mQIProperty.cmi +mQIProperty.cmx: mQIConn.cmx mQIMap.cmx mQIPostgres.cmx mQIUtil.cmx \ + mQIProperty.cmi mQueryInterpreter.cmo: mQIConn.cmi mQIProperty.cmi mQIUtil.cmi \ mQueryInterpreter.cmi mQueryInterpreter.cmx: mQIConn.cmx mQIProperty.cmx mQIUtil.cmx \ diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index 18fcd5512..be32ff48c 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -4,9 +4,9 @@ REQUIRES = helm-cic helm-cic_textual_parser helm-mathql postgres PREDICATES = -INTERFACE_FILES = mQueryMisc.mli mQIPostgres.mli mQIConn.mli \ - mQIUtil.mli mQIProperty.mli \ - mQueryInterpreter.mli +INTERFACE_FILES = mQueryMisc.mli mQIUtil.mli \ + mQIPostgres.mli mQIMap.mli mQIConn.mli \ + mQIProperty.mli mQueryInterpreter.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/mathql_interpreter/mQIConn.ml b/helm/ocaml/mathql_interpreter/mQIConn.ml index a51242bef..11dbd1674 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.ml +++ b/helm/ocaml/mathql_interpreter/mQIConn.ml @@ -28,10 +28,19 @@ type flag = Postgres | Galax | Stat | Quiet | Warn | Log -type handle = {log : string -> unit; (* logging function *) - set : flag list; (* options *) - pgc : Postgres.connection option (* Postgres connection *) - } +type handle = { + log : string -> unit; (* logging function *) + set : flag list; (* options *) + pgc : Postgres.connection option; (* PG connection *) + pgm : MQIMap.pg_map; (* PG conversion function *) + pga : MQIMap.pg_alias (* PG table aliases *) +} + +let tables handle p = MQIMap.get_tables handle.pgm p + +let field handle p t = MQIMap.get_field handle.pgm p t + +let resolve handle a = MQIMap.resolve handle.pga a let log handle = handle.log @@ -70,9 +79,15 @@ let flags_of_string s = string_fold_left (fun l c -> l @ flag_of_char c) [] s let init myflags mylog = + let s, m, a = + let g = + if List.mem Galax myflags + then MQIMap.empty_map else MQIMap.read_map + in g () + in {log = mylog; set = myflags; - pgc = if List.mem Galax myflags - then None else MQIPostgres.init () + pgc = if List.mem Galax myflags then None else MQIPostgres.init s; + pgm = m; pga = a } let close handle = diff --git a/helm/ocaml/mathql_interpreter/mQIConn.mli b/helm/ocaml/mathql_interpreter/mQIConn.mli index 405e405d1..649b54854 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.mli +++ b/helm/ocaml/mathql_interpreter/mQIConn.mli @@ -43,7 +43,10 @@ val init_if_connected : flag list -> (string -> unit) -> handle * For exclusive use of the interpreter. *) -val log : handle -> string -> unit -val set : handle -> flag -> bool -val pgc : handle -> Postgres.connection option -val flags : handle -> flag list +val log : handle -> string -> unit +val set : handle -> flag -> bool +val pgc : handle -> Postgres.connection option +val flags : handle -> flag list +val tables : handle -> MathQL.path -> MQIMap.pg_tables +val field : handle -> MathQL.path -> string -> string +val resolve : handle -> string -> string diff --git a/helm/ocaml/mathql_interpreter/mQIMap.ml b/helm/ocaml/mathql_interpreter/mQIMap.ml new file mode 100644 index 000000000..20923f982 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQIMap.ml @@ -0,0 +1,94 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +module U = MQueryUtil + +type pg_map = (MathQL.path * (bool * string * string option)) list + +type pg_tables = (bool * string) list + +type pg_alias = (string * string) list + +let empty_map () = "", [], [] + +let read_map () = + let default_map = "mathql_db_map.txt" in + let map = + try Sys.getenv "MATHQL_DB_MAP" + with Not_found -> default_map + in + let ich = open_in map in + let pgs = input_line ich in + let rec aux r s = + let d = input_line ich in + match Str.split (Str.regexp "[ \t]+") d with + | [] -> aux r s + | t :: "<-" :: p -> aux ((p, (false, t, None)) :: r) s + | t :: c :: "<-" :: p -> aux ((p, (false, t, Some c)) :: r) s + | t :: c :: "<+" :: p -> aux ((p, (true, t, Some c)) :: r) s + | [a; "->"; t] -> aux r ((a, t) :: s) + | ["->"] -> r, s + | _ -> raise (Failure "MQIMap.read_map") + in + let pgm, pga = aux [] [] in + close_in ich; + pgs, pgm, pga + +let comp c1 c2 = match c1, c2 with + | (_, t1), (_, t2) when t1 < t2 -> U.Lt + | (_, t1), (_, t2) when t1 > t2 -> U.Gt + | (b1, t), (b2, _) -> U.Eq (b1 || b2, t) + +let get_tables pgm p = + let aux l = function + | q, (b, t, _) when q = p -> U.list_join comp l [(b, t)] + | _, _ -> l + in + List.fold_left aux [] pgm + +let rec refine_tables l1 l2 = + U.list_meet comp l1 l2 + +let default_table = function + | [(_, a)] -> a + | l -> + try List.assoc true l + with Not_found -> raise (Failure "MQIMap.default_table") + +let get_field pgm p t = + let aux = function + | q, (_, u, _) when q = p && u = t -> true + | _ -> false + in + match List.filter aux pgm with + | [_, (_, _, None)] -> "" + | [_, (_, _, Some c)] -> c + | _ -> raise (Failure "MQIMap.get_field") + +let resolve pga a = + try List.assoc a pga with Not_found -> a diff --git a/helm/ocaml/mathql_interpreter/mQIMap.mli b/helm/ocaml/mathql_interpreter/mQIMap.mli new file mode 100644 index 000000000..bf78f6d62 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mQIMap.mli @@ -0,0 +1,47 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +type pg_map (* mathql path map for postgres *) + +type pg_tables + +type pg_alias + +val empty_map : unit -> string * pg_map * pg_alias + +val read_map : unit -> string * pg_map * pg_alias + +val get_tables : pg_map -> MathQL.path -> pg_tables + +val refine_tables : pg_tables -> pg_tables -> pg_tables + +val default_table : pg_tables -> string + +val get_field : pg_map -> MathQL.path -> string -> string + +val resolve : pg_alias -> string -> string diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.ml b/helm/ocaml/mathql_interpreter/mQIPostgres.ml index 7c4abcbf6..6f8a6f7ba 100644 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.ml +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.ml @@ -26,14 +26,7 @@ (* AUTOR: Ferruccio Guidi *) -let default_connection_string = - "dbname=mowgli user=helm" - -let connection_string = - try Sys.getenv "POSTGRESQL_CONNECTION_STRING" - with Not_found -> default_connection_string - -let init () = +let init connection_string = try Some (new Postgres.connection connection_string) with _ -> raise (Failure ("MQIPostgres.init: " ^ connection_string)) diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.mli b/helm/ocaml/mathql_interpreter/mQIPostgres.mli index 8acd2a2fd..342c91eaa 100644 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.mli +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.mli @@ -26,7 +26,7 @@ (* AUTOR: Ferruccio Guidi *) -val init : unit -> Postgres.connection option +val init : string -> Postgres.connection option val close : Postgres.connection option -> unit diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml index 026e11b48..be559adc7 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.ml +++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml @@ -30,6 +30,7 @@ module M = MathQL module P = MQIPostgres module C = MQIConn module U = MQIUtil +module A = MQIMap let not_supported s = raise (Failure ("MQIProperty: feature not supported: " ^ s)) @@ -112,53 +113,16 @@ let pg_result distinct subj el res = in compose mk_avs res -let get_table mc ct cfl el = - let fst = function - | [] -> None - | head :: tail -> Some head - in - let comp n1 n2 = match n1, n2 with - | None, _ -> n2 - | Some h, Some k when h = k -> n2 - | _, None -> n1 - | _ -> not_supported "comp" - in - let rec get_c prev = function - | [] -> prev - | (_, p, _) :: tail -> get_c (comp prev (fst p)) tail - in - let rec get_e prev = function - | [] -> prev - | (p, _) :: tail -> get_e (comp prev (fst p)) tail - in - get_e (get_c (get_c (fst mc) ct) (List.concat cfl)) el - -let rec decolon s = - let l = String.length s in - try - let i = String.index s ':' in - String.sub s 0 i ^ "_" ^ decolon (String.sub s (succ i) (l - succ i)) - with Not_found -> s - -let conv_bp = function - | [] -> "h_occurrence" - | [t] -> "" - | [_; "h:occurrence"] -> "source" - | [_; t] -> decolon t - | _ -> not_supported "conv_bp" - -let conv_gen = function - | [] -> "source" - | ["objectName"] -> "value" - | [t] -> "" - | [_; t] -> decolon t - | _ -> not_supported "conv" - -let exec_single h mc ct cfl el t = - let table = match t with Some t -> decolon t | None -> "objectName" in - let table, conv = - if table = "backPointer" then "refObj", conv_bp else table, conv_gen - in +let get_table h mc ct cfl el = + let aux_c ts (_, p, _) = A.refine_tables ts (C.tables h p) in + let aux_e ts (p, _) = A.refine_tables ts (C.tables h p) in + let fst = C.tables h mc in + let snd = List.fold_left aux_c fst (ct @ (List.concat cfl)) in + let trd = List.fold_left aux_e snd el in + A.default_table trd + +let exec_single h mc ct cfl el table = + let conv p = C.field h p table in let first = conv mc in let mk_con l = List.map (fun (pat, p, v) -> (pat, conv p, v)) l in let cons_true = mk_con ct in @@ -166,13 +130,14 @@ let exec_single h mc ct cfl el t = let other_cols = List.map (fun (p, _) -> conv p) el in let cols = if first = "" then other_cols else first :: other_cols in let low_level = if C.set h C.Galax then gx_query else pg_query in - pg_result false first el (low_level h table cols cons_true cons_false) + let result = low_level h (C.resolve h table) cols cons_true cons_false in + pg_result false first el result let deadline = 100 let exec h refine mc ct cfl el = if refine <> M.RefineExact then not_supported "exec"; - let table = get_table mc ct cfl el in + let table = get_table h mc ct cfl el in let rec exec_aux ct = match ct with | (pat, p, v) :: tail when List.length v > deadline -> let single s = exec_aux ((pat, p, [s]) :: tail) in diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 35650c8c6..e4e33c629 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -177,29 +177,9 @@ let contype = "Content-Type", "text/html";; (* SEARCH ENGINE functions *) -let refine_constraints ((constr_obj:T.r_obj list), (constr_rel:T.r_rel list), (constr_sort:T.r_sort list)) = - function - "/searchPattern" -> - U.universe_for_search_pattern, - (constr_obj, constr_rel, constr_sort), - (Some constr_obj, Some constr_rel, Some constr_sort) - | "/matchConclusion" -> - let constr_obj' = - List.map - (function (pos, uri) -> U.set_full_position pos None, uri) - (List.filter - (function (pos, _) -> U.is_conclusion pos) - constr_obj) - in - U.universe_for_match_conclusion, - (*CSC: we must select the must constraints here!!! *) - (constr_obj',[],[]),(Some constr_obj', None, None) - | _ -> assert false -;; - let get_constraints term = function - "/locateInductivePrinciple" -> + | "/locateInductivePrinciple" -> let uri = match term with Cic.MutInd (uri,t,_) -> MQueryUtil.string_of_uriref (uri,[t]) @@ -212,9 +192,19 @@ let get_constraints term = let constr_sort = [(`MainHypothesis (Some 1), T.Prop)] in U.universe_for_search_pattern, (constr_obj, constr_rel, constr_sort), (None,None,None) - | req_path -> - let must = CGSearchPattern.get_constraints term in - refine_constraints must req_path + | "/searchPattern" -> + let constr_obj, constr_rel, constr_sort = + CGSearchPattern.get_constraints term in + U.universe_for_search_pattern, + (constr_obj, constr_rel, constr_sort), + (Some constr_obj, Some constr_rel, Some constr_sort) + | "/matchConclusion" -> + let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in +(* FG: there is no way to choose the block number ***************************) + let block = pred (List.length list_of_must) in + U.universe_for_match_conclusion, + (List.nth list_of_must block, [], []), (Some only, None, None) + | _ -> assert false ;; (*