From 21758b512843088d19e81830d9fb121725c8a16e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 15 Oct 2004 14:12:17 +0000 Subject: [PATCH] added helm-metadata module --- helm/ocaml/METAS/meta.helm-metadata.src | 4 + helm/ocaml/Makefile.in | 1 + helm/ocaml/metadata/.cvsignore | 2 + helm/ocaml/metadata/.depend | 8 + helm/ocaml/metadata/Makefile | 15 ++ helm/ocaml/metadata/metadataDb.ml | 137 +++++++++++++++ helm/ocaml/metadata/metadataDb.mli | 47 +++++ helm/ocaml/metadata/metadataExtractor.ml | 203 ++++++++++++++++++++++ helm/ocaml/metadata/metadataExtractor.mli | 32 ++++ helm/ocaml/metadata/metadataPp.ml | 77 ++++++++ helm/ocaml/metadata/metadataPp.mli | 45 +++++ helm/ocaml/metadata/metadataTypes.ml | 42 +++++ helm/ocaml/metadata/test.ml | 23 +++ 13 files changed, 636 insertions(+) create mode 100644 helm/ocaml/METAS/meta.helm-metadata.src create mode 100644 helm/ocaml/metadata/.cvsignore create mode 100644 helm/ocaml/metadata/.depend create mode 100644 helm/ocaml/metadata/Makefile create mode 100644 helm/ocaml/metadata/metadataDb.ml create mode 100644 helm/ocaml/metadata/metadataDb.mli create mode 100644 helm/ocaml/metadata/metadataExtractor.ml create mode 100644 helm/ocaml/metadata/metadataExtractor.mli create mode 100644 helm/ocaml/metadata/metadataPp.ml create mode 100644 helm/ocaml/metadata/metadataPp.mli create mode 100644 helm/ocaml/metadata/metadataTypes.ml create mode 100644 helm/ocaml/metadata/test.ml diff --git a/helm/ocaml/METAS/meta.helm-metadata.src b/helm/ocaml/METAS/meta.helm-metadata.src new file mode 100644 index 000000000..773e8fbd2 --- /dev/null +++ b/helm/ocaml/METAS/meta.helm-metadata.src @@ -0,0 +1,4 @@ +requires="dbi helm-cic_proof_checking" +version="0.0.1" +archive(byte)="metadata.cma" +archive(native)="metadata.cmxa" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 1fb18a90e..980990db6 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -23,6 +23,7 @@ MODULES = \ cic_omdoc \ tactics \ hbugs \ + metadata \ cic_transformations \ cic_textual_parser2 diff --git a/helm/ocaml/metadata/.cvsignore b/helm/ocaml/metadata/.cvsignore new file mode 100644 index 000000000..702e58bb7 --- /dev/null +++ b/helm/ocaml/metadata/.cvsignore @@ -0,0 +1,2 @@ +*.cm[aiox] *.cmxa *.[ao] +test diff --git a/helm/ocaml/metadata/.depend b/helm/ocaml/metadata/.depend new file mode 100644 index 000000000..f25f462cb --- /dev/null +++ b/helm/ocaml/metadata/.depend @@ -0,0 +1,8 @@ +metadataExtractor.cmi: metadataTypes.cmo +metadataPp.cmi: metadataTypes.cmo +metadataExtractor.cmo: metadataTypes.cmo metadataExtractor.cmi +metadataExtractor.cmx: metadataTypes.cmx metadataExtractor.cmi +metadataPp.cmo: metadataPp.cmi +metadataPp.cmx: metadataPp.cmi +metadataDb.cmo: metadataExtractor.cmi metadataPp.cmi metadataDb.cmi +metadataDb.cmx: metadataExtractor.cmx metadataPp.cmx metadataDb.cmi diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile new file mode 100644 index 000000000..5acf3b87a --- /dev/null +++ b/helm/ocaml/metadata/Makefile @@ -0,0 +1,15 @@ +PACKAGE = metadata +REQUIRES = dbi helm-cic_proof_checking +PREDICATES = + +INTERFACE_FILES = metadataExtractor.mli metadataPp.mli metadataDb.mli +IMPLEMENTATION_FILES = metadataTypes.ml $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = + +all: + +test: test.ml metadata.cma + $(OCAMLFIND) ocamlc -thread -package dbi.mysql,helm-metadata -linkpkg -o $@ $< + +include ../Makefile.common diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml new file mode 100644 index 000000000..3d618a52c --- /dev/null +++ b/helm/ocaml/metadata/metadataDb.ml @@ -0,0 +1,137 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +open Printf + +module DB = Dbi_mysql + +let sort_tbl = "refSort" +let rel_tbl = "refRel" +let obj_tbl = "refObj" +let owners_tbl = "owners" +let conclno_tbl = "no_inconcl_aux" +let conclno_hyp_tbl = "no_concl_hyp" +let name_tbl = "objectName" + +(* let baseuri = "http://www.cs.unibo.it/helm/schemas/schema-helm#" *) +let baseuri = "" +let inconcl_uri = baseuri ^ "InConclusion" +let mainconcl_uri = baseuri ^ "MainConclusion" +let mainhyp_uri = baseuri ^ "MainHypothesis" +let inhyp_uri = baseuri ^ "InHypothesis" +let inbody_uri = baseuri ^ "InBody" + +let prepare_insert (dbh: Dbi.connection) = + let insert_owner = + dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\")" owners_tbl) + in + let insert_sort = + dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",?,\"?\")" sort_tbl) + in + let insert_rel = + dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",?)" rel_tbl) + in + let insert_obj = + dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",\"?\",?)" obj_tbl) + in + (insert_owner, insert_sort, insert_rel, insert_obj) + +let execute_insert dbh (insert_owner, insert_sort, insert_rel, insert_obj) + uri owner (sort_cols, rel_cols, obj_cols) += + insert_owner#execute [`String uri; `String owner]; + List.iter insert_sort#execute sort_cols; + List.iter insert_rel#execute rel_cols; + List.iter insert_obj#execute obj_cols + +let insert_const_no dbh uri = + let inconcl_no = + sprintf "INSERT INTO %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\"" + conclno_tbl uri obj_tbl inconcl_uri mainconcl_uri uri + in + let concl_hyp = + sprintf "INSERT INTO %s + SELECT \"%s\",COUNT(DISTINCT h_occurrence) + FROM %s + WHERE NOT (h_position=\"%s\") AND (source = \"%s\")" + conclno_hyp_tbl uri obj_tbl inbody_uri uri + in + (dbh#prepare inconcl_no)#execute []; + (dbh#prepare concl_hyp)#execute [] + +let insert_name ~dbh ~uri ~name = + let query = + dbh#prepare + (sprintf "INSERT INTO %s VALUES (\"%s\", \"%s\")" name_tbl uri name) + in + query#execute [] + +type dbi_columns = + Dbi.sql_t list list * Dbi.sql_t list list * Dbi.sql_t list list + +let index_constant ~dbh = + let query = prepare_insert dbh in + fun ~owner ~uri ~body ~ty -> + let name = UriManager.name_of_uri uri in + let uri = UriManager.string_of_uri uri in + let metadata = MetadataExtractor.compute ~body ~ty in + let columns = MetadataPp.columns_of_metadata ~about:uri metadata in + execute_insert dbh query uri owner (columns :> dbi_columns); + insert_const_no dbh uri; + insert_name ~dbh ~uri ~name + +let index_inductive_def ~dbh = + let query = prepare_insert dbh in + fun ~owner ~uri ~types -> + let metadata = MetadataExtractor.compute_ind ~uri ~types in + let uri_of (a,b,c) = a in + let uris = UriManager.string_of_uri uri :: List.map uri_of metadata in + let uri = UriManager.string_of_uri uri in + let columns = MetadataPp.columns_of_ind_metadata metadata in + execute_insert dbh query uri owner (columns :> dbi_columns); + List.iter (insert_const_no dbh) uris; + List.iter (fun (uri, name, _) -> insert_name ~dbh ~uri ~name) metadata + +let clean ~(dbh: Dbi.connection) ~owner = + let owned_uris = (* list of uris in list-of-columns format *) + let query = + dbh#prepare (sprintf + "SELECT source FROM %s WHERE owner = \"%s\"" owners_tbl owner) + in + query#execute []; + List.map + (function [source_col] -> source_col | _ -> assert false) + (query#fetchall ()) + in + let del_from tbl = + let query = + dbh#prepare (sprintf "DELETE FROM %s WHERE source LIKE \"?%%\"" tbl) + in + query#execute owned_uris + in + List.iter del_from + [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl; + owners_tbl] + diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli new file mode 100644 index 000000000..074ff7214 --- /dev/null +++ b/helm/ocaml/metadata/metadataDb.mli @@ -0,0 +1,47 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + + (** index a Cic.Constant object and insert resulting metadata into the db + * PRE_EVAL(dbh) *) +val index_constant: + dbh:Dbi.connection -> + owner:string -> + uri:UriManager.uri -> body:Cic.term option -> ty:Cic.term -> + unit + + (** index a Cic.InductiveDefinition object and insert resulting metadata into + * the db + * PRE_EVAL(dbh) *) +val index_inductive_def: + dbh:Dbi.connection -> + owner:string -> + uri:UriManager.uri -> types:Cic.inductiveType list -> + unit + +(* TODO Zack indexing of variables and (perhaps?) incomplete proofs *) + + (** remove from the db all metadata pertaining to a given owner *) +val clean: dbh:Dbi.connection -> owner:string -> unit + diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml new file mode 100644 index 000000000..0bd5eaed3 --- /dev/null +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -0,0 +1,203 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +open Printf + +open MetadataTypes + +let is_main_pos = function + | `MainConclusion + | `MainHypothesis -> true + | _ -> false + +let main_pos (pos: position): main_position = + match pos with + | `MainConclusion -> `MainConclusion + | `MainHypothesis -> `MainHypothesis + | _ -> assert false + +let next_pos = function + | `MainConclusion -> `InConclusion + | `MainHypothesis -> `InHypothesis + | pos -> pos + +let string_of_uri = UriManager.string_of_uri + +module OrderedMetadata = + struct + type t = MetadataTypes.metadata + let compare m1 m2 = (* ignore universes in Cic.Type sort *) + match (m1, m2) with + | `Sort (Cic.Type _, p1, d1), `Sort (Cic.Type _, p2, d2) -> + Pervasives.compare (p1, d2) (p2, d2) + | _ -> Pervasives.compare m1 m2 + end + +module MetadataSet = Set.Make (OrderedMetadata) +module StringSet = Set.Make (String) + +module S = MetadataSet + +let unopt = function Some x -> x | None -> assert false + +let incr_depth = function + | None -> assert false + | Some x -> Some (x + 1) + +let compute_term pos term = + let rec aux (pos: position) pi_depth set = function + | Cic.Rel _ -> + if is_main_pos pos then + S.add (`Rel (main_pos pos, unopt pi_depth)) set + else + set + | Cic.Var _ -> set + | Cic.Meta (_, local_context) -> + List.fold_left + (fun set context -> + match context with + | None -> set + | Some term -> aux pos pi_depth set term) + set + local_context + | Cic.Sort sort -> + if is_main_pos pos then + S.add (`Sort (sort, main_pos pos, unopt pi_depth)) set + else + set + | Cic.Implicit _ -> assert false + | Cic.Cast (term, ty) -> + (* TODO consider also ty? *) + aux pos pi_depth set term + | Cic.Prod (_, source, target) -> + (match pos with + | `MainConclusion -> + let set = aux `MainHypothesis (Some 0) set source in + aux pos (incr_depth pi_depth) set target + | `MainHypothesis -> + let set = aux `InHypothesis None set source in + aux pos (incr_depth pi_depth) set target + | `InConclusion + | `InHypothesis + | `InBody -> + let set = aux pos None set source in + aux pos None set target) + | Cic.Lambda (_, source, target) -> + assert (not (is_main_pos pos)); + let set = aux pos None set source in + aux pos None set target + | Cic.LetIn (_, term, target) -> + if is_main_pos pos then + aux pos pi_depth set (CicSubstitution.subst term target) + else + let set = aux pos None set term in + aux pos None set target + | Cic.Appl [] -> assert false + | Cic.Appl (hd :: tl) -> + let set = aux pos pi_depth set hd in + List.fold_left + (fun set term -> aux (next_pos pos) None set term) + set tl + | Cic.Const (uri, subst) -> + let set = S.add (`Obj (string_of_uri uri, pos, pi_depth)) set in + List.fold_left + (fun set (_, term) -> aux (next_pos pos) None set term) + set subst + | Cic.MutInd (uri, typeno, subst) -> + let uri = UriManager.string_of_uriref (uri, [typeno]) in + let set = S.add (`Obj (uri, pos, pi_depth)) set in + List.fold_left (fun set (_, term) -> aux (next_pos pos) None set term) + set subst + | Cic.MutConstruct (uri, typeno, consno, subst) -> + let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in + let set = S.add (`Obj (uri, pos, pi_depth)) set in + List.fold_left (fun set (_, term) -> aux (next_pos pos) None set term) + set subst + | Cic.MutCase (uri, _, outtype, term, pats) -> + let pos = next_pos pos in + let set = aux pos None set term in + let set = aux pos None set outtype in + List.fold_left (fun set term -> aux pos None set term) set pats + | Cic.Fix (_, funs) -> + let pos = next_pos pos in + List.fold_left + (fun set (_, _, ty, body) -> + let set = aux pos None set ty in + aux pos None set body) + set funs + | Cic.CoFix (_, funs) -> + let pos = next_pos pos in + List.fold_left + (fun set (_, ty, body) -> + let set = aux pos None set ty in + aux pos None set body) + set funs + in + aux pos (Some 0) S.empty term + +let compute_type uri typeno (name, _, ty, constructors) = + let consno = ref 0 in + let type_metadata = + (UriManager.string_of_uriref (uri, [typeno]), name, + S.elements (compute_term `MainConclusion ty)) + in + let constructors_metadata = + List.map + (fun (name, term) -> + incr consno; + let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in + (uri, name, S.elements (compute_term `MainConclusion term))) + constructors + in + type_metadata :: constructors_metadata + +let compute_ind ~uri ~types = + let idx = ref ~-1 in + List.concat (List.map (fun ty -> incr idx; compute_type uri !idx ty) types) + +let compute ~body ~ty = + let type_metadata = compute_term `MainConclusion ty in + let body_metadata = + match body with + | None -> S.empty + | Some body -> compute_term `InBody body + in + let uris = + S.fold + (fun metadata uris -> + match metadata with + | `Obj (uri, _, _) -> StringSet.add uri uris + | _ -> uris) + type_metadata StringSet.empty + in + S.elements + (S.union + (S.filter + (function + | `Obj (uri, _, _) when StringSet.mem uri uris -> false + | _ -> true) + body_metadata) + type_metadata) + diff --git a/helm/ocaml/metadata/metadataExtractor.mli b/helm/ocaml/metadata/metadataExtractor.mli new file mode 100644 index 000000000..ef7ea763c --- /dev/null +++ b/helm/ocaml/metadata/metadataExtractor.mli @@ -0,0 +1,32 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +val compute: body:Cic.term option -> ty:Cic.term -> MetadataTypes.metadata list + + (** @return tuples *) +val compute_ind: + uri:UriManager.uri -> types:Cic.inductiveType list -> + (string * string * MetadataTypes.metadata list) list + diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml new file mode 100644 index 000000000..5b8ae4e7a --- /dev/null +++ b/helm/ocaml/metadata/metadataPp.ml @@ -0,0 +1,77 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +open Printf + +let pp_position = function + | `MainConclusion -> "MainConclusion" + | `MainHypothesis -> "MainHypothesis" + | `InConclusion -> "InConclusion" + | `InHypothesis -> "InHypothesis" + | `InBody -> "InBody" + +let metadata_ns = "http://www.cs.unibo.it/helm/schemas/schema-helm" +let uri_of_pos pos = String.concat "#" [metadata_ns; pp_position pos] + +let pp_sort = function + | Cic.Prop -> "Prop" + | Cic.Set -> "Set" + | Cic.Type _ -> "Type" + | Cic.CProp -> "CProp" + +type t = [ `Int of int | `String of string | `Null ] + +let columns_of_metadata ~about metadatas = + let position p = `String (pp_position p) in + let sort s = `String (pp_sort s) in + let source = `String about in + let depth d = `Int d in + let depth_opt = function None -> `Null | Some d -> `Int d in + let occurrence u = `String u in + List.fold_left + (fun (sort_cols, rel_cols, obj_cols) metadata -> + match metadata with + | `Sort (s, p, d) -> + [source; position p; depth d; sort s] :: sort_cols, rel_cols, obj_cols + | `Rel (p, d) -> + sort_cols, [source; position p; depth d] :: rel_cols, obj_cols + | `Obj (o, p, d) -> + sort_cols, rel_cols, + [source; occurrence o; position p; depth_opt d] :: obj_cols) + ([], [], []) metadatas + +let columns_of_ind_metadata ind_metadata = + List.fold_left + (fun (sort_cols, rel_cols, obj_cols) (uri, _, metadatas) -> + let (s, r, o) = columns_of_metadata ~about:uri metadatas in + (List.append sort_cols s, List.append rel_cols r, List.append obj_cols o)) + ([], [], []) ind_metadata + +let pp_columns ?(sep = "\n") (sort_cols, rel_cols, obj_cols) = + String.concat sep + ([ "Sort" ] @ List.map Dbi.sdebug (sort_cols :> Dbi.sql_t list list) @ + [ "Rel" ] @ List.map Dbi.sdebug (rel_cols :> Dbi.sql_t list list) @ + [ "Obj" ] @ List.map Dbi.sdebug (obj_cols :> Dbi.sql_t list list)) + diff --git a/helm/ocaml/metadata/metadataPp.mli b/helm/ocaml/metadata/metadataPp.mli new file mode 100644 index 000000000..bd044c713 --- /dev/null +++ b/helm/ocaml/metadata/metadataPp.mli @@ -0,0 +1,45 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +(** Pretty printer and OCamlDBI friendly interface *) + +type t = + [ `Int of int + | `String of string + | `Null ] + + (** @param about uri of object whose metadata are about + * @return columns for Sort, Rel, and Obj respectively *) +val columns_of_metadata: + about:string -> MetadataTypes.metadata list -> + t list list * t list list * t list list + + (** @return columns for Sort, Rel, and Obj respectively *) +val columns_of_ind_metadata: + (string * string * MetadataTypes.metadata list) list -> + t list list * t list list * t list list + +val pp_columns: ?sep:string -> t list list * t list list * t list list -> string + diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml new file mode 100644 index 000000000..dbe94695e --- /dev/null +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -0,0 +1,42 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +type main_position = [ `MainConclusion | `MainHypothesis ] + +type position = + [ main_position + | `InConclusion + | `InHypothesis + | `InBody + ] + +type pi_depth = int + +type metadata = + [ `Sort of Cic.sort * main_position * pi_depth + | `Rel of main_position * pi_depth + | `Obj of string * position * pi_depth option + ] + diff --git a/helm/ocaml/metadata/test.ml b/helm/ocaml/metadata/test.ml new file mode 100644 index 000000000..27be47c23 --- /dev/null +++ b/helm/ocaml/metadata/test.ml @@ -0,0 +1,23 @@ + +module DB = Dbi_mysql + +let _ = Helm_registry.set "getter.mode" "remote"; +let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in +let dbh = new DB.connection ~host:"mowgli.cs.unibo.it" ~user:"helm" "matita" in +let owner = + try + Sys.argv.(2) + with Invalid_argument _ -> "matita_test" +in +if Sys.argv.(1) = "clean" then + MetadataDb.clean ~dbh ~owner +else + let uri_str = Sys.argv.(1) in + let uri = UriManager.uri_of_string uri_str in + match CicEnvironment.get_obj uri with + | Cic.Constant (_, body, ty, _) -> + MetadataDb.index_constant ~body ~ty ~uri ~owner ~dbh + | Cic.InductiveDefinition (types, _, _) -> + MetadataDb.index_inductive_def ~dbh ~owner ~uri ~types + | _ -> assert false + -- 2.39.2