]> matita.cs.unibo.it Git - helm.git/blob - components/cic/libraryObjects.ml
added generation of quick reference card of tactic syntax
[helm.git] / 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_ind_URI uri =
86  List.exists (fun (_,_,_,eq_ind,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
87
88 let is_eq_ind_r_URI uri =
89  List.exists (fun (_,_,_,_,eq_ind_r) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
90 let is_trans_eq_URI uri = 
91  List.exists (fun (_,_,trans_eq,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
92 let is_sym_eq_URI uri =
93  List.exists (fun (_,sym_eq,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
94
95 let sym_eq_URI ~eq:uri =
96  try
97   let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
98  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
99
100 let trans_eq_URI ~eq:uri =
101  try
102   let _,_,x,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
103  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
104
105 let eq_ind_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 eq_ind_r_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 true_URI () =
116  try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
117 let false_URI () =
118  try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
119 let absurd_URI () =
120  try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None