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_rec_URI;eq_rec_r_URI;eq_rect_URI;
  60               eq_rect_r_URI;eq_f_URI;eq_f_sym_URI] ->
  61       eq_URIs_ref :=
  62        insert_unique
  63          (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,
  64           eq_ind_r_URI,eq_rec_URI,eq_rec_r_URI,eq_rect_URI,
  65           eq_rect_r_URI,eq_f_URI,eq_f_sym_URI)
  66         (fun x,_,_,_,_,_,_,_,_,_,_ -> x) !eq_URIs_ref
  67   | "true",[true_URI] ->
  68       true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref
  69   | "false",[false_URI] ->
  70       false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
  71   | "absurd",[absurd_URI] ->
  72       absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
  73   | _,l ->
  74       raise
  75         (NotRecognized (what^" with "^string_of_int(List.length l)^" params"))
  76 ;;
  77
  78 let reset_defaults () =
  79   eq_URIs_ref := default_eq_URIs;
  80   true_URIs_ref := default_true_URIs;
  81   false_URIs_ref := default_false_URIs;
  82   absurd_URIs_ref := default_absurd_URIs
  83
  84
  85 (**** LOOKUP FUNCTIONS ****)
  86 let eq_URI () =
  87  try let eq,_,_,_,_,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
  88  with Failure "hd" -> None
  89
  90 let is_eq_URI uri =
  91  List.exists (fun (eq,_,_,_,_,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
  92
  93 let is_eq_refl_URI uri =
  94   let urieq = UriManager.strip_xpointer uri in
  95   is_eq_URI urieq &&
  96   not (UriManager.eq urieq uri)
  97 ;;
  98
  99 let is_eq_ind_URI uri =
 100  List.exists (fun (_,_,_,eq_ind,_,_,_,_,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
 101 let is_eq_ind_r_URI uri =
 102  List.exists (fun (_,_,_,_,eq_ind_r,_,_,_,_,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
 103 let is_eq_rec_URI uri =
 104  List.exists (fun (_,_,_,_,_,eq_rec,_,_,_,_,_) -> UriManager.eq eq_rec uri) !eq_URIs_ref
 105 let is_eq_rec_r_URI uri =
 106  List.exists (fun (_,_,_,_,_,_,eq_rec_r,_,_,_,_) -> UriManager.eq eq_rec_r uri) !eq_URIs_ref
 107 let is_eq_rect_URI uri =
 108  List.exists (fun (_,_,_,_,_,_,_,eq_rect,_,_,_) -> UriManager.eq eq_rect uri) !eq_URIs_ref
 109 let is_eq_rect_r_URI uri =
 110  List.exists (fun (_,_,_,_,_,_,_,_,eq_rect_r,_,_) -> UriManager.eq eq_rect_r uri) !eq_URIs_ref
 111 let is_trans_eq_URI uri =
 112  List.exists (fun (_,_,trans_eq,_,_,_,_,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
 113 let is_sym_eq_URI uri =
 114  List.exists (fun (_,sym_eq,_,_,_,_,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
 115 let is_eq_f_URI uri =
 116  List.exists (fun (_,_,_,_,_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref
 117 let is_eq_f_sym_URI uri =
 118  List.exists (fun (_,_,_,_,_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref
 119
 120 let in_eq_URIs uri =
 121   is_eq_URI uri || is_eq_refl_URI uri || is_eq_ind_URI uri ||
 122   is_eq_ind_r_URI uri || is_eq_rec_URI uri || is_eq_rec_r_URI uri ||
 123   is_eq_rect_URI uri || is_eq_rect_r_URI uri ||
 124   is_trans_eq_URI uri || is_sym_eq_URI uri || is_eq_f_URI uri ||
 125   is_eq_f_sym_URI uri
 126
 127
 128
 129 let eq_refl_URI ~eq:uri =
 130   let uri = UriManager.strip_xpointer uri in
 131   UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)")
 132
 133 let sym_eq_URI ~eq:uri =
 134  try
 135   let _,x,_,_,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 136  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 137
 138 let trans_eq_URI ~eq:uri =
 139  try
 140   let _,_,x,_,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 141  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 142
 143 let eq_ind_URI ~eq:uri =
 144  try
 145   let _,_,_,x,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 146  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 147
 148 let eq_ind_r_URI ~eq:uri =
 149  try
 150   let _,_,_,_,x,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 151  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 152
 153 let eq_rec_URI ~eq:uri =
 154  try
 155   let _,_,_,_,_,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 156  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 157
 158 let eq_rec_r_URI ~eq:uri =
 159  try
 160   let _,_,_,_,_,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 161  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 162
 163 let eq_rect_URI ~eq:uri =
 164  try
 165   let _,_,_,_,_,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 166  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 167
 168 let eq_rect_r_URI ~eq:uri =
 169  try
 170   let _,_,_,_,_,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 171  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 172
 173 let eq_f_URI ~eq:uri =
 174  try
 175   let _,_,_,_,_,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 176  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 177
 178 let eq_f_sym_URI ~eq:uri =
 179  try
 180   let _,_,_,_,_,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
 181  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 182
 183
 184 let eq_URI_of_eq_f_URI eq_f_URI =
 185   try
 186   let x,_,_,_,_,_,_,_,_,_,_ =
 187     List.find (fun _,_,_,_,_,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref
 188   in x
 189  with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI))
 190
 191 let true_URI () =
 192  try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
 193 let false_URI () =
 194  try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
 195 let absurd_URI () =
 196  try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None
 197
 198 let nat_URI = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind"
 199
 200 let zero = Cic.MutConstruct (nat_URI,0,1,[])
 201 let succ = Cic.MutConstruct (nat_URI,0,2,[])
 202
 203 let is_zero = function
 204   | Cic.AMutConstruct (_, uri, 0, 1, _) when UriManager.eq uri nat_URI -> true
 205   | _ -> false
 206
 207 let is_succ = function
 208   | Cic.AMutConstruct (_, uri, 0, 2, _) when UriManager.eq uri nat_URI -> true
 209   | _ -> false
 210
 211 let build_nat n =
 212   if n < 0 then assert false;
 213   let rec aux = function
 214     | 0 -> zero
 215     | n -> Cic.Appl [ succ; (aux (n - 1)) ]
 216   in
 217   aux n
 218
 219 let destroy_nat annterm =
 220   let rec aux acc = function
 221     | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl
 222     | t when is_zero t -> Some acc
 223     | _ -> None in
 224   aux 0 annterm
 225