]> matita.cs.unibo.it Git - helm.git/blob - helm/annotationHelper/cicAnnotationHinter.ml
mathql_db_map.txt now retrieved by Helm_registry.
[helm.git] / helm / annotationHelper / cicAnnotationHinter.ml
1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
24  *)
25
26 (******************************************************************************)
27 (*                                                                            *)
28 (*                               PROJECT HELM                                 *)
29 (*                                                                            *)
30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
31 (*                                 14/06/2000                                 *)
32 (*                                                                            *)
33 (*                                                                            *)
34 (******************************************************************************)
35
36 let deactivate_hints_from annotation_window n =
37  let annotation_hints = annotation_window#annotation_hints in
38   for i = n to Array.length annotation_hints - 1 do
39    annotation_hints.(i)#misc#hide ()
40   done
41 ;;
42
43 (* CSC: orripilante *)
44 (* the list of the signal ids *)
45 let sig_ids = ref ([] : GtkSignal.id list);;
46
47 let disconnect_hint annotation_window buttonno =
48  match !sig_ids with
49     id::ids ->
50      annotation_window#annotation_hints.(buttonno)#misc#disconnect id ;
51      sig_ids := ids
52   | _ -> assert false
53 ;;
54
55 (* link_hint annotation_window n label hint *)
56 (* set the label of the nth hint button of annotation_window to label *)
57 (* and the correspondent hint to hint                                 *)
58 let link_hint annotation_window buttonno label hint =
59  let button = annotation_window#annotation_hints.(buttonno) in
60   sig_ids :=
61    (button#connect#clicked
62     ~callback:(fun () -> (annotation_window#annotation : GEdit.text)#insert hint)
63    ) :: !sig_ids ;
64   button#misc#show () ;
65   match button#children with
66      [labelw] -> (GMisc.label_cast labelw)#set_text label
67    | _ -> assert false
68 ;;
69
70 exception TooManyHints;;
71
72 let link_hints annotation_window a =
73  if Array.length a > Array.length annotation_window#annotation_hints then
74   raise TooManyHints ;
75  for i = List.length !sig_ids - 1 downto 0 do
76   disconnect_hint annotation_window i
77  done ;
78  Array.iteri
79   (fun i (label,hint) -> link_hint annotation_window i label hint) a ;
80  deactivate_hints_from annotation_window (Array.length a)
81 ;;
82
83 let list_mapi f =
84  let rec aux n =
85   function
86      [] -> []
87    | he::tl -> (f n he)::(aux (n + 1) tl)
88  in
89   aux 0
90 ;;
91
92 let get_id annterm =
93  let module C = Cic in
94   match annterm with
95      C.ARel (id,_,_)
96    | C.AVar (id,_)
97    | C.AMeta (id,_,_)
98    | C.ASort (id,_)
99    | C.AImplicit id
100    | C.ACast (id,_,_)
101    | C.AProd (id,_,_,_)
102    | C.ALambda (id,_,_,_)
103    | C.ALetIn (id,_,_,_)
104    | C.AAppl (id,_)
105    | C.AConst (id,_,_)
106    | C.AMutInd (id,_,_,_)
107    | C.AMutConstruct (id,_,_,_,_)
108    | C.AMutCase (id,_,_,_,_,_,_)
109    | C.AFix (id,_,_)
110    | C.ACoFix (id,_,_) -> id
111 ;;
112
113 let create_hint_from_term annotation_window annterm =
114  let module C = Cic in
115   match annterm with
116      C.ARel (id,_,_) ->
117       link_hints annotation_window
118        [| "Binder", "<attribute name = 'binder' id = '" ^ id ^ "'/>" |]
119    | C.AVar (id,_) ->
120       link_hints annotation_window
121        [| "relURI???", "<attribute name = 'relUri' id = '" ^ id ^ "'/>" |]
122    | C.AMeta (id,_,subst) ->
123       let res =
124        Array.append
125         [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
126         (Array.mapi
127           (fun i s ->
128             match s with
129                None ->
130                 "Argument " ^ string_of_int i, "_"
131              | Some t ->
132                 "Argument " ^ string_of_int i, "<node id ='" ^ get_id t ^ "'/>"
133           ) (Array.of_list subst)
134         )
135       in
136        link_hints annotation_window res
137    | C.ASort (id,_) ->
138       link_hints annotation_window
139        [| "Value", "<attribute name = 'value' id = '" ^ id ^ "'/>" |]
140    | C.AImplicit id ->
141       link_hints annotation_window [| |]
142    | C.ACast (id,bo,ty) ->
143       let boid = get_id bo
144       and tyid = get_id ty in
145        link_hints annotation_window
146         [| "Body", "<node id = '" ^ boid ^ "'/>" ;
147            "Type", "<node id = '" ^ tyid ^ "'/>"
148         |]
149    | C.AProd (id,_,ty,bo) ->
150       let boid = get_id bo
151       and tyid = get_id ty in
152        link_hints annotation_window
153         [| "Binder",
154             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
155            "Body", "<node id = '" ^ boid ^ "'/>" ;
156            "Type", "<node id = '" ^ tyid ^ "'/>"
157         |]
158    | C.ALambda (id,_,ty,bo) ->
159       let boid = get_id bo
160       and tyid = get_id ty in
161        link_hints annotation_window
162         [| "Binder",
163             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
164            "Body", "<node id = '" ^ boid ^ "'/>" ;
165            "Type", "<node id = '" ^ tyid ^ "'/>"
166         |]
167    | C.ALetIn (id,_,ty,bo) ->
168       let boid = get_id bo
169       and tyid = get_id ty in
170        link_hints annotation_window
171         [| "Binder",
172             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
173            "Term", "<node id = '" ^ boid ^ "'/>" ;
174            "Target", "<node id = '" ^ tyid ^ "'/>"
175         |]
176    | C.AAppl (id,args) ->
177       let argsid =
178        Array.mapi
179         (fun i te -> "Argument " ^ string_of_int i, "<node id ='" ^
180           get_id te ^ "'/>")
181         (Array.of_list args)
182       in
183        link_hints annotation_window argsid
184    | C.AConst (id,_,_) ->
185       link_hints annotation_window
186        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
187    | C.AMutInd (id,_,_,_) ->
188       link_hints annotation_window
189        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
190    | C.AMutConstruct (id,_,_,_,_) ->
191       link_hints annotation_window
192        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
193    | C.AMutCase (id,_,_,_,outty,te,pl) ->
194       let outtyid = get_id outty
195       and teid = get_id te
196       and plid =
197        Array.mapi
198         (fun i te -> "Pattern " ^ string_of_int i, "<node id ='" ^
199           get_id te ^ "'/>")
200         (Array.of_list pl)
201       in
202        link_hints annotation_window
203         (Array.append
204          [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" ;
205             "Case Type", "<node id = '" ^ outtyid ^ "'/>" ;
206             "Term", "<node id = '" ^ teid ^ "'/>" ;
207          |]
208          plid)
209    | C.AFix (id,_,funl) ->
210       let funtylid =
211        Array.mapi
212         (fun i (_,_,ty,_) ->
213           "Type " ^ string_of_int i, "<node id ='" ^
214           get_id ty ^ "'/>")
215         (Array.of_list funl)
216       and funbolid =
217        Array.mapi
218         (fun i (_,_,_,bo) ->
219           "Body " ^ string_of_int i, "<node id ='" ^
220           get_id bo ^ "'/>")
221         (Array.of_list funl)
222       and funnamel =
223        Array.mapi
224         (fun i (_,_,_,_) ->
225           "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
226            "' name = 'name' child='" ^ string_of_int i ^ "'/>")
227         (Array.of_list funl)
228       and funrecindexl =
229        Array.mapi
230         (fun i (_,_,_,_) ->
231           "Recursive Index??? " ^ string_of_int i, "<attribute id = '" ^ id ^
232            "' name = 'recIndex' child='" ^ string_of_int i ^ "'/>")
233         (Array.of_list funl)
234       in
235        link_hints annotation_window
236         (Array.concat
237          [ funtylid ;
238            funbolid ;
239            funnamel ;
240            funrecindexl ;
241            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
242          ]
243         )
244    | C.ACoFix (id,_,funl) ->
245       let funtylid =
246        Array.mapi
247         (fun i (_,ty,_) ->
248           "Type " ^ string_of_int i, "<node id ='" ^
249           get_id ty ^ "'/>")
250         (Array.of_list funl)
251       and funbolid =
252        Array.mapi
253         (fun i (_,_,bo) ->
254           "Body " ^ string_of_int i, "<node id ='" ^
255           get_id bo ^ "'/>")
256         (Array.of_list funl)
257       and funnamel =
258        Array.mapi
259         (fun i (_,_,_) ->
260           "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
261            "' name = 'name' child='" ^ string_of_int i ^ "'/>")
262         (Array.of_list funl)
263       in
264        link_hints annotation_window
265         (Array.concat
266          [ funtylid ;
267            funbolid ;
268            funnamel ;
269            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
270          ]
271         )
272 ;;
273
274 (*CSC: da riscrivere completamente eliminando il paciugo degli array - liste *)
275 let create_hint_from_obj annotation_window annobj =
276  let module C = Cic in
277   match annobj with
278      C.ADefinition (id,_,bo,ty,_) ->
279       let boid = get_id bo
280       and tyid = get_id ty in
281        link_hints annotation_window
282         [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
283            "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
284            "Body", "<node id = '" ^ boid ^ "'/>" ;
285            "Type", "<node id = '" ^ tyid ^ "'/>"
286         |]
287    | C.AAxiom (id,_,ty,_) ->
288       let tyid = get_id ty in
289        link_hints annotation_window
290         [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
291            "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
292            "Type", "<node id = '" ^ tyid ^ "'/>"
293         |]
294    | C.AVariable (id,_,bo,ty) ->
295       let tyid = get_id ty in
296        link_hints annotation_window
297         (match bo with
298             None ->
299              [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
300                 "Type", "<node id = '" ^ tyid ^ "'/>"
301              |]
302           | Some bo ->
303              let boid = get_id bo in
304               [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
305                  "Body", "<node id = '" ^ boid ^ "'/>" ;
306                  "Type", "<node id = '" ^ tyid ^ "'/>"
307               |]
308         )
309    | C.ACurrentProof (id,_,conjs,bo,ty) ->
310       let boid = get_id bo
311       and tyid = get_id ty
312       and conjsid = List.map (fun (id,_,_,_) -> id) conjs in
313        link_hints annotation_window
314 (*CSC: never tested since the introduction of the new Metas *)
315         (Array.append
316           [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
317              "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
318              "Body", "<node id = '" ^ boid ^ "'/>" ;
319              "Type", "<node id = '" ^ tyid ^ "'/>"
320           |]
321           (Array.mapi
322             (fun i id ->
323               "Conjecture " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
324             ) (Array.of_list conjsid)
325           )
326         )
327    | C.AInductiveDefinition (id,itl,_,_) ->
328       let itlids =
329        List.map
330         (fun (_,_,arity,cons) ->
331           get_id arity,
332           List.map (fun (_,ty,_) -> get_id ty) cons
333         ) itl
334       in
335        link_hints annotation_window
336         (Array.concat
337           [
338            [| "Ingredients","<attribute name = 'params' id = '" ^ id ^ "'/>" |];
339            (Array.mapi
340              (fun i _ ->
341                "Type Name " ^ string_of_int i,
342                "<attribute name = 'name' child = '" ^ string_of_int i ^
343                 "' id = '" ^ id ^ "'/>"
344              ) (Array.of_list itlids)
345            ) ;
346            (Array.mapi
347              (fun i (id,_) ->
348                "Type " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
349              ) (Array.of_list itlids)
350            ) ;
351            (Array.concat
352             (list_mapi
353              (fun i (_,consid) ->
354               (Array.mapi
355                 (fun j _ ->
356                   "Constructor Name " ^ string_of_int i ^ " " ^ string_of_int j,
357                   "<attribute name = 'name' id = '" ^ id ^ 
358                    "' child = '" ^ string_of_int i ^ "' grandchild = '" ^
359                    string_of_int j ^ "'/>"
360                 ) (Array.of_list consid)
361               ) ;
362              ) itlids
363             )
364            ) ;
365            (Array.concat
366             (list_mapi
367              (fun i (_,consid) ->
368               (Array.mapi
369                 (fun j id ->
370                   "Constructor " ^ string_of_int i ^ " " ^ string_of_int j,
371                   "<node id = '" ^ id ^ "'/>"
372                 ) (Array.of_list consid)
373               ) ;
374              ) itlids
375             )
376            )
377           ]
378         )
379 ;;
380
381 exception IdUnknown of string;;
382
383 let create_hints annotation_window ids_to_targets xpath =
384  try
385   match Hashtbl.find ids_to_targets xpath with
386      Cic.Object annobj -> create_hint_from_obj annotation_window annobj
387    | Cic.Term annterm -> create_hint_from_term annotation_window annterm
388 (*CSC: never tested since the introduction of the new Metas *)
389    | Cic.Hypothesis _
390    | Cic.Conjecture _ -> assert false
391  with
392   Not_found -> raise (IdUnknown xpath)
393 ;;