--- /dev/null
+(* Copyright (C) 2004-2005, 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/
+ *)
+
+(* $Id$ *)
+
+open Printf
+
+let is_a_variant obj =
+ match obj with
+ | Cic.Constant(_,_,_,_,attrs) ->
+ List.exists (fun x -> x = `Flavour `Variant) attrs
+ | _ -> false
+
+let uris_for_inductive_type uri obj =
+ match obj with
+ | Cic.InductiveDefinition(types,_,_,_) ->
+ let suri = UriManager.string_of_uri uri in
+ let uris,_ =
+ List.fold_left
+ (fun (acc,i) (_,_,_,constructors)->
+ let is = string_of_int i in
+ let newacc,_ =
+ List.fold_left
+ (fun (acc,j) _ ->
+ let js = string_of_int j in
+ UriManager.uri_of_string
+ (suri^"#xpointer(1/"^is^"/"^js^")")::acc,j+1)
+ (acc,1) constructors
+ in
+ newacc,i+1)
+ ([],1) types
+ in uris
+ | _ -> [uri]
+
+let add_obj refinement_toolkit uri obj status =
+ let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in
+ let add_to_universe (universe,status) uri =
+ let term = CicUtil.term_of_uri uri in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
+(* prop filtering
+ let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph in
+ prerr_endline (CicPp.ppterm term);
+ prerr_endline (CicPp.ppterm sort);
+ let tkeys =
+ if sort = Cic.Sort(Cic.Prop) then Universe.keys [] ty
+ else []
+ in
+*)
+ let tkeys = Universe.keys [] ty in
+ let index_cmd =
+ List.map
+ (fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri))
+ tkeys
+ in
+(* prop filtering
+ let universe =
+ if sort = Cic.Sort(Cic.Prop) then
+ Universe.index_term_and_unfolded_term universe [] term ty
+ else universe
+*)
+ let universe = Universe.index_term_and_unfolded_term universe [] term ty
+ in
+ let status = GrafiteTypes.add_moo_content index_cmd status in
+ (universe,status)
+ in
+ let uris_to_index =
+ if is_a_variant obj then []
+ else (uris_for_inductive_type uri obj)@lemmas
+ in
+ let universe,status =
+ List.fold_left add_to_universe
+ (status.GrafiteTypes.universe,status)
+ uris_to_index
+ in
+ {status with
+ GrafiteTypes.objects = uri::status.GrafiteTypes.objects;
+ GrafiteTypes.universe = universe},
+ lemmas
+
+let add_coercion refinement_toolkit ~add_composites status uri arity
+ saturations baseuri
+=
+ let compounds =
+ LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity
+ saturations baseuri in
+ {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
+ compounds
+
+module OrderedUri =
+struct
+ type t = UriManager.uri * string
+ let compare (u1, _) (u2, _) = UriManager.compare u1 u2
+end
+
+module UriSet = Set.Make (OrderedUri)
+
+ (** @return l2 \ l1 *)
+let uri_list_diff l2 l1 =
+ let module S = UriManager.UriSet in
+ let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
+ let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
+ let diff = S.diff s2 s1 in
+ S.fold (fun uri uris -> uri :: uris) diff []
+
+let time_travel ~present ~past =
+ let objs_to_remove =
+ uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in
+ let coercions_to_remove =
+ uri_list_diff present.GrafiteTypes.coercions past.GrafiteTypes.coercions
+ in
+ List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove;
+ List.iter LibrarySync.remove_obj objs_to_remove
+
+let initial_status baseuri = {
+ GrafiteTypes.moo_content_rev = [];
+ proof_status = GrafiteTypes.No_proof;
+(* options = GrafiteTypes.no_options; *)
+ objects = [];
+ coercions = [];
+ universe = Universe.empty;
+ baseuri = baseuri;
+ }
+
+
+let init baseuri =
+ LibrarySync.remove_all_coercions ();
+ LibraryObjects.reset_defaults ();
+ initial_status baseuri
+ ;;
+let pop () =
+ LibrarySync.pop ();
+ LibraryObjects.pop ()
+;;
+
+let push () =
+ LibrarySync.push ();
+ LibraryObjects.push ()
+;;
+