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 "***********************************************************************"
--- /dev/null
+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
+ ->
| 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
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)
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)
+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 \
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)
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
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 =
* 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
--- /dev/null
+(* 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 <fguidi@cs.unibo.it>
+ *)
+
+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
--- /dev/null
+(* 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 <fguidi@cs.unibo.it>
+ *)
+
+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
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-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))
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-val init : unit -> Postgres.connection option
+val init : string -> Postgres.connection option
val close : Postgres.connection option -> unit
module P = MQIPostgres
module C = MQIConn
module U = MQIUtil
+module A = MQIMap
let not_supported s =
raise (Failure ("MQIProperty: feature not supported: " ^ s))
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
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
(* 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])
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
;;
(*
projects / helm.git / commitdiff