components/cic/libraryObjects.ml

   1 (* Copyright (C) 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 (**** TABLES ****)
  29
  30 let default_eq_URIs = []
  31 let default_true_URIs = []
  32 let default_false_URIs = []
  33 let default_absurd_URIs = []
  34
  35 (* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
  36 let eq_URIs_ref = ref default_eq_URIs;;
  37
  38 let true_URIs_ref = ref default_true_URIs
  39 let false_URIs_ref = ref default_false_URIs
  40 let absurd_URIs_ref = ref default_absurd_URIs
  41
  42
  43 (**** SET_DEFAULT ****)
  44
  45 exception NotRecognized of string;;
  46
  47 (* insert an element in front of the list, removing from the list all the
  48    previous elements with the same key associated *)
  49 let insert_unique e extract l =
  50  let uri = extract e in
  51  let l' =
  52   List.filter (fun x -> let uri' = extract x in not (UriManager.eq uri uri')) l
  53  in
  54   e :: l'
  55
  56 let set_default what l =
  57   match what,l with
  58   "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;
  59               eq_ind_r_URI;eq_f_URI;eq_f_sym_URI] ->
  60       eq_URIs_ref :=
  61        insert_unique
  62          (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,
  63           eq_ind_r_URI,eq_f_URI,eq_f_sym_URI)
  64         (fun x,_,_,_,_,_,_ -> x) !eq_URIs_ref
  65   | "true",[true_URI] ->
  66       true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref
  67   | "false",[false_URI] ->
  68       false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
  69   | "absurd",[absurd_URI] ->
  70       absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
  71   | _,l ->
  72       raise
  73         (NotRecognized (what^" with "^string_of_int(List.length l)^" params"))
  74 ;;
  75
  76 let reset_defaults () =
  77   eq_URIs_ref := default_eq_URIs;
  78   true_URIs_ref := default_true_URIs;
  79   false_URIs_ref := default_false_URIs;
  80   absurd_URIs_ref := default_absurd_URIs
  81
  82
  83 (**** LOOKUP FUNCTIONS ****)
  84 let eq_URI () =
  85  try let eq,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
  86  with Failure "hd" -> None
  87
  88 let is_eq_URI uri =
  89  List.exists (fun (eq,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
  90
  91 let is_eq_refl_URI uri =
  92   let urieq = UriManager.strip_xpointer uri in
  93   is_eq_URI urieq &&
  94   not (UriManager.eq urieq uri)
  95 ;;
  96
  97 let is_eq_ind_URI uri =
  98  List.exists (fun (_,_,_,eq_ind,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
  99 let is_eq_ind_r_URI uri =
 100  List.exists (fun (_,_,_,_,eq_ind_r,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
 101 let is_trans_eq_URI uri =
 102  List.exists (fun (_,_,trans_eq,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
 103 let is_sym_eq_URI uri =
 104  List.exists (fun (_,sym_eq,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
 105 let is_eq_f_URI uri =
 106  List.exists (fun (_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref
 107 let is_eq_f_sym_URI uri =
 108  List.exists (fun (_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref
 109
 110 let in_eq_URIs uri =
 111   is_eq_URI uri || is_eq_refl_URI uri || is_eq_ind_URI uri ||
 112   is_eq_ind_r_URI uri || is_trans_eq_URI uri || is_sym_eq_URI uri ||
 113   is_eq_f_URI uri || is_eq_f_sym_URI uri
 114
 115
 116
 117 let eq_refl_URI ~eq:uri =
 118   let uri = UriManager.strip_xpointer uri in
 119   UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)")
 120
 121 let sym_eq_URI ~eq:uri =
 122  try
 123   let _,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 124  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 125
 126 let trans_eq_URI ~eq:uri =
 127  try
 128   let _,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 129  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 130
 131 let eq_ind_URI ~eq:uri =
 132  try
 133   let _,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 134  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 135
 136 let eq_ind_r_URI ~eq:uri =
 137  try
 138   let _,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 139  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 140
 141 let eq_f_URI ~eq:uri =
 142  try
 143   let _,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 144  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 145
 146 let eq_f_sym_URI ~eq:uri =
 147  try
 148   let _,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 149  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 150
 151
 152 let eq_URI_of_eq_f_URI eq_f_URI =
 153   try
 154   let x,_,_,_,_,_,_ =
 155     List.find (fun _,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref
 156   in x
 157  with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI))
 158
 159 let true_URI () =
 160  try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
 161 let false_URI () =
 162  try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
 163 let absurd_URI () =
 164  try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None