components/grafite_engine/grafiteSync.ml

   1 (* Copyright (C) 2004-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Printf
  29
  30 let uris_for_inductive_type uri obj =
  31   match obj with
  32     | Cic.InductiveDefinition(types,_,_,_) ->
  33         let suri = UriManager.string_of_uri uri in
  34         let uris,_ =
  35           List.fold_left
  36             (fun (acc,i) (_,_,_,constructors)->
  37                let is = string_of_int i in
  38                let newacc,_ =
  39                  List.fold_left
  40                    (fun (acc,j) _ ->
  41                       let js = string_of_int j in
  42                         UriManager.uri_of_string
  43                           (suri^"#xpointer(1/"^is^"/"^js^")")::acc,j+1)
  44                    (acc,1) constructors
  45                in
  46                newacc,i+1)
  47             ([],1) types
  48         in uris
  49     | _ -> [uri]
  50
  51 let add_obj refinement_toolkit uri obj status =
  52  let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in
  53  let add_to_universe (universe,status) uri =
  54    let term = CicUtil.term_of_uri uri in
  55    let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
  56 (* prop filtering
  57    let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph in
  58    prerr_endline (CicPp.ppterm term);
  59    prerr_endline (CicPp.ppterm sort);
  60    let tkeys =
  61      if sort = Cic.Sort(Cic.Prop) then Universe.keys [] ty
  62      else []
  63    in
  64 *)
  65    let tkeys = Universe.keys [] ty in
  66    let index_cmd =
  67      List.map
  68        (fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri))
  69        tkeys
  70    in
  71 (* prop filtering
  72    let universe =
  73      if sort = Cic.Sort(Cic.Prop) then
  74        Universe.index_term_and_unfolded_term universe [] term ty
  75      else universe
  76 *)
  77    let universe = Universe.index_term_and_unfolded_term universe [] term ty
  78    in
  79    let status = GrafiteTypes.add_moo_content index_cmd status in
  80    (universe,status)
  81  in
  82  let universe,status =
  83    List.fold_left add_to_universe
  84      (status.GrafiteTypes.universe,status)
  85      ((uris_for_inductive_type uri obj)@lemmas) in
  86   {status with
  87      GrafiteTypes.objects = uri::status.GrafiteTypes.objects;
  88      GrafiteTypes.universe = universe},
  89    lemmas
  90
  91 let add_coercion refinement_toolkit ~add_composites status uri arity =
  92  let compounds =
  93    LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity in
  94   {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
  95    compounds
  96
  97 module OrderedUri =
  98 struct
  99   type t = UriManager.uri * string
 100   let compare (u1, _) (u2, _) = UriManager.compare u1 u2
 101 end
 102
 103 module UriSet = Set.Make (OrderedUri)
 104
 105   (** @return l2 \ l1 *)
 106 let uri_list_diff l2 l1 =
 107   let module S = UriManager.UriSet in
 108   let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
 109   let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
 110   let diff = S.diff s2 s1 in
 111   S.fold (fun uri uris -> uri :: uris) diff []
 112
 113 let time_travel ~present ~past =
 114   let objs_to_remove =
 115    uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in
 116   let coercions_to_remove =
 117    uri_list_diff present.GrafiteTypes.coercions past.GrafiteTypes.coercions
 118   in
 119   List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove;
 120   List.iter LibrarySync.remove_obj objs_to_remove
 121
 122 let init () =
 123   LibrarySync.remove_all_coercions ();
 124   LibraryObjects.reset_defaults ();
 125   {
 126     GrafiteTypes.moo_content_rev = [];
 127     proof_status = GrafiteTypes.No_proof;
 128     options = GrafiteTypes.no_options;
 129     objects = [];
 130     coercions = [];
 131     universe = Universe.empty;
 132   }