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