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 (**** LOOKUP FUNCTIONS ****)
  83
  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
 100 let is_eq_ind_r_URI uri =
 101  List.exists (fun (_,_,_,_,eq_ind_r,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
 102 let is_trans_eq_URI uri =
 103  List.exists (fun (_,_,trans_eq,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
 104 let is_sym_eq_URI uri =
 105  List.exists (fun (_,sym_eq,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
 106 let is_eq_f_URI uri =
 107  List.exists (fun (_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref
 108 let is_eq_f_sym_URI uri =
 109  List.exists (fun (_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref
 110
 111
 112
 113 let eq_refl_URI ~eq:uri =
 114   let uri = UriManager.strip_xpointer uri in
 115   UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)")
 116
 117 let sym_eq_URI ~eq:uri =
 118  try
 119   let _,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 120  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 121
 122 let trans_eq_URI ~eq:uri =
 123  try
 124   let _,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 125  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 126
 127 let eq_ind_URI ~eq:uri =
 128  try
 129   let _,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 130  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 131
 132 let eq_ind_r_URI ~eq:uri =
 133  try
 134   let _,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 135  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 136
 137 let eq_f_URI ~eq:uri =
 138  try
 139   let _,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 140  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 141
 142 let eq_f_sym_URI ~eq:uri =
 143  try
 144   let _,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 145  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 146
 147
 148 let eq_URI_of_eq_f_URI eq_f_URI =
 149   try
 150   let x,_,_,_,_,_,_ =
 151     List.find (fun _,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref
 152   in x
 153  with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI))
 154
 155 let true_URI () =
 156  try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
 157 let false_URI () =
 158  try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
 159 let absurd_URI () =
 160  try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None