helm/ocaml/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  [HelmLibraryObjects.Logic.eq_URI,
  32       HelmLibraryObjects.Logic.sym_eq_URI,
  33       HelmLibraryObjects.Logic.trans_eq_URI,
  34       HelmLibraryObjects.Logic.eq_ind_URI,
  35       HelmLibraryObjects.Logic.eq_ind_r_URI];;
  36
  37 let default_true_URIs = [HelmLibraryObjects.Logic.true_URI]
  38 let default_false_URIs = [HelmLibraryObjects.Logic.false_URI]
  39 let default_absurd_URIs = [HelmLibraryObjects.Logic.absurd_URI]
  40
  41 (* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
  42 let eq_URIs_ref =
  43  ref [HelmLibraryObjects.Logic.eq_URI,
  44       HelmLibraryObjects.Logic.sym_eq_URI,
  45       HelmLibraryObjects.Logic.trans_eq_URI,
  46       HelmLibraryObjects.Logic.eq_ind_URI,
  47       HelmLibraryObjects.Logic.eq_ind_r_URI];;
  48
  49 let true_URIs_ref = ref [HelmLibraryObjects.Logic.true_URI]
  50 let false_URIs_ref = ref [HelmLibraryObjects.Logic.false_URI]
  51 let absurd_URIs_ref = ref [HelmLibraryObjects.Logic.absurd_URI]
  52
  53
  54 (**** SET_DEFAULT ****)
  55
  56 exception NotRecognized;;
  57
  58 (* insert an element in front of the list, removing from the list all the
  59    previous elements with the same key associated *)
  60 let insert_unique e extract l =
  61  let uri = extract e in
  62  let l' =
  63   List.filter (fun x -> let uri' = extract x in not (UriManager.eq uri uri')) l
  64  in
  65   e :: l'
  66
  67 let set_default what l =
  68   match what,l with
  69     "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;eq_ind_r_URI] ->
  70       eq_URIs_ref :=
  71        insert_unique (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,eq_ind_r_URI)
  72         (fun x,_,_,_,_ -> x) !eq_URIs_ref
  73   | "true",[true_URI] ->
  74       true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref
  75   | "false",[false_URI] ->
  76       false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
  77   | "absurd",[absurd_URI] ->
  78       absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
  79   | _,_ -> raise NotRecognized
  80
  81 let reset_defaults () =
  82   eq_URIs_ref := default_eq_URIs;
  83   true_URIs_ref := default_true_URIs;
  84   false_URIs_ref := default_false_URIs;
  85   absurd_URIs_ref := default_absurd_URIs
  86
  87 (**** LOOKUP FUNCTIONS ****)
  88
  89 let eq_URI () = let eq,_,_,_,_ = List.hd !eq_URIs_ref in eq
  90
  91 let is_eq_URI uri =
  92  List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
  93
  94 let sym_eq_URI ~eq:uri =
  95  try
  96   let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
  97  with Not_found -> raise NotRecognized
  98
  99 let trans_eq_URI ~eq:uri =
 100  try
 101   let _,_,x,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 102  with Not_found -> raise NotRecognized
 103
 104 let eq_ind_URI ~eq:uri =
 105  try
 106   let _,_,_,x,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 107  with Not_found -> raise NotRecognized
 108
 109 let eq_ind_r_URI ~eq:uri =
 110  try
 111   let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 112  with Not_found -> raise NotRecognized
 113
 114 let true_URI () = List.hd !true_URIs_ref
 115 let false_URI () = List.hd !false_URIs_ref
 116 let absurd_URI () = List.hd !absurd_URIs_ref