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