--- /dev/null
+requires="dbi helm-cic_proof_checking"
+version="0.0.1"
+archive(byte)="metadata.cma"
+archive(native)="metadata.cmxa"
cic_omdoc \
tactics \
hbugs \
+ metadata \
cic_transformations \
cic_textual_parser2
--- /dev/null
+*.cm[aiox] *.cmxa *.[ao]
+test
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+(* 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]
+
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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)
+
--- /dev/null
+(* 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 <uri, name, metadata> *)
+val compute_ind:
+ uri:UriManager.uri -> types:Cic.inductiveType list ->
+ (string * string * MetadataTypes.metadata list) list
+
--- /dev/null
+(* 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))
+
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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
+ ]
+
--- /dev/null
+
+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
+
projects / helm.git / commitdiff