helm/software/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;eq_ind_r_URI] ->
  59       eq_URIs_ref :=
  60        insert_unique (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,eq_ind_r_URI)
  61         (fun x,_,_,_,_ -> x) !eq_URIs_ref
  62   | "true",[true_URI] ->
  63       true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref
  64   | "false",[false_URI] ->
  65       false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
  66   | "absurd",[absurd_URI] ->
  67       absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
  68   | _,_ -> raise (NotRecognized what)
  69
  70 let reset_defaults () =
  71   eq_URIs_ref := default_eq_URIs;
  72   true_URIs_ref := default_true_URIs;
  73   false_URIs_ref := default_false_URIs;
  74   absurd_URIs_ref := default_absurd_URIs
  75
  76 (**** LOOKUP FUNCTIONS ****)
  77
  78 let eq_URI () =
  79  try let eq,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
  80  with Failure "hd" -> None
  81
  82 let is_eq_URI uri =
  83  List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
  84
  85 let is_eq_refl_URI uri =
  86   let urieq = UriManager.strip_xpointer uri in
  87   is_eq_URI urieq &&
  88   not (UriManager.eq urieq uri)
  89 ;;
  90
  91 let is_eq_ind_URI uri =
  92  List.exists (fun (_,_,_,eq_ind,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
  93
  94 let is_eq_ind_r_URI uri =
  95  List.exists (fun (_,_,_,_,eq_ind_r) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
  96 let is_trans_eq_URI uri =
  97  List.exists (fun (_,_,trans_eq,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
  98 let is_sym_eq_URI uri =
  99  List.exists (fun (_,sym_eq,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
 100
 101 let eq_refl_URI ~eq:uri =
 102   let uri = UriManager.strip_xpointer uri in
 103   UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)")
 104
 105 let sym_eq_URI ~eq:uri =
 106  try
 107   let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 108  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 109
 110 let trans_eq_URI ~eq:uri =
 111  try
 112   let _,_,x,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 113  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 114
 115 let eq_ind_URI ~eq:uri =
 116  try
 117   let _,_,_,x,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 118  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 119
 120 let eq_ind_r_URI ~eq:uri =
 121  try
 122   let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 123  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 124
 125 let true_URI () =
 126  try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
 127 let false_URI () =
 128  try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
 129 let absurd_URI () =
 130  try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None