]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/cicAnnotationHinter.ml
...
[helm.git] / helm / interface / 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     (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,_,_,_)             -> id
96    | C.AVar (id,_,_)               -> id
97    | C.AMeta (id,_,_)              -> id
98    | C.ASort (id,_,_)              -> id
99    | C.AImplicit (id,_)            -> id
100    | C.ACast (id,_,_,_)            -> id
101    | C.AProd (id,_,_,_,_)          -> id
102    | C.ALambda (id,_,_,_,_)        -> id
103    | C.ALetIn (id,_,_,_,_)         -> id
104    | C.AAppl (id,_,_)              -> id
105    | C.AConst (id,_,_,_)           -> id
106    | C.AAbst (id,_,_)              -> id
107    | C.AMutInd (id,_,_,_,_)        -> id
108    | C.AMutConstruct (id,_,_,_,_,_)-> id
109    | C.AMutCase (id,_,_,_,_,_,_,_) -> id
110    | C.AFix (id,_,_,_)             -> id
111    | C.ACoFix (id,_,_,_)           -> id
112 ;;
113
114 let create_hint_from_term annotation_window annterm =
115  let module C = Cic in
116   match annterm with
117      C.ARel (id,_,_,_) ->
118       link_hints annotation_window
119        [| "Binder", "<attribute name = 'binder' id = '" ^ id ^ "'/>" |]
120    | C.AVar (id,_,_) ->
121       link_hints annotation_window
122        [| "relURI???", "<attribute name = 'relUri' id = '" ^ id ^ "'/>" |]
123    | C.AMeta (id,_,_) ->
124       link_hints annotation_window
125        [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
126    | C.ASort (id,_,_) ->
127       link_hints annotation_window
128        [| "Value", "<attribute name = 'value' id = '" ^ id ^ "'/>" |]
129    | C.AImplicit (id,_) ->
130       link_hints annotation_window [| |]
131    | C.ACast (id,_,bo,ty) ->
132       let boid = get_id bo
133       and tyid = get_id ty in
134        link_hints annotation_window
135         [| "Body", "<node id = '" ^ boid ^ "'/>" ;
136            "Type", "<node id = '" ^ tyid ^ "'/>"
137         |]
138    | C.AProd (id,_,_,ty,bo) ->
139       let boid = get_id bo
140       and tyid = get_id ty in
141        link_hints annotation_window
142         [| "Binder",
143             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
144            "Body", "<node id = '" ^ boid ^ "'/>" ;
145            "Type", "<node id = '" ^ tyid ^ "'/>"
146         |]
147    | C.ALambda (id,_,_,ty,bo) ->
148       let boid = get_id bo
149       and tyid = get_id ty in
150        link_hints annotation_window
151         [| "Binder",
152             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
153            "Body", "<node id = '" ^ boid ^ "'/>" ;
154            "Type", "<node id = '" ^ tyid ^ "'/>"
155         |]
156    | C.ALetIn (id,_,_,ty,bo) ->
157       let boid = get_id bo
158       and tyid = get_id ty in
159        link_hints annotation_window
160         [| "Binder",
161             "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
162            "Term", "<node id = '" ^ boid ^ "'/>" ;
163            "Target", "<node id = '" ^ tyid ^ "'/>"
164         |]
165    | C.AAppl (id,_,args) ->
166       let argsid =
167        Array.mapi
168         (fun i te -> "Argument " ^ string_of_int i, "<node id ='" ^
169           get_id te ^ "'/>")
170         (Array.of_list args)
171       in
172        link_hints annotation_window argsid
173    | C.AConst (id,_,_,_) ->
174       link_hints annotation_window
175        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
176    | C.AAbst (id,_,_) ->
177       link_hints annotation_window
178        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
179    | C.AMutInd (id,_,_,_,_) ->
180       link_hints annotation_window
181        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
182    | C.AMutConstruct (id,_,_,_,_,_) ->
183       link_hints annotation_window
184        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
185    | C.AMutCase (id,_,_,_,_,outty,te,pl) ->
186       let outtyid = get_id outty
187       and teid = get_id te
188       and plid =
189        Array.mapi
190         (fun i te -> "Pattern " ^ string_of_int i, "<node id ='" ^
191           get_id te ^ "'/>")
192         (Array.of_list pl)
193       in
194        link_hints annotation_window
195         (Array.append
196          [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" ;
197             "Case Type", "<node id = '" ^ outtyid ^ "'/>" ;
198             "Term", "<node id = '" ^ teid ^ "'/>" ;
199          |]
200          plid)
201    | C.AFix (id,_,_,funl) ->
202       let funtylid =
203        Array.mapi
204         (fun i (_,_,ty,_) ->
205           "Type " ^ string_of_int i, "<node id ='" ^
206           get_id ty ^ "'/>")
207         (Array.of_list funl)
208       and funbolid =
209        Array.mapi
210         (fun i (_,_,_,bo) ->
211           "Body " ^ string_of_int i, "<node id ='" ^
212           get_id bo ^ "'/>")
213         (Array.of_list funl)
214       and funnamel =
215        Array.mapi
216         (fun i (_,_,_,_) ->
217           "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
218            "' name = 'name' child='" ^ string_of_int i ^ "'/>")
219         (Array.of_list funl)
220       and funrecindexl =
221        Array.mapi
222         (fun i (_,_,_,_) ->
223           "Recursive Index??? " ^ string_of_int i, "<attribute id = '" ^ id ^
224            "' name = 'recIndex' child='" ^ string_of_int i ^ "'/>")
225         (Array.of_list funl)
226       in
227        link_hints annotation_window
228         (Array.concat
229          [ funtylid ;
230            funbolid ;
231            funnamel ;
232            funrecindexl ;
233            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
234          ]
235         )
236    | C.ACoFix (id,_,_,funl) ->
237       let funtylid =
238        Array.mapi
239         (fun i (_,ty,_) ->
240           "Type " ^ string_of_int i, "<node id ='" ^
241           get_id ty ^ "'/>")
242         (Array.of_list funl)
243       and funbolid =
244        Array.mapi
245         (fun i (_,_,bo) ->
246           "Body " ^ string_of_int i, "<node id ='" ^
247           get_id bo ^ "'/>")
248         (Array.of_list funl)
249       and funnamel =
250        Array.mapi
251         (fun i (_,_,_) ->
252           "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
253            "' name = 'name' child='" ^ string_of_int i ^ "'/>")
254         (Array.of_list funl)
255       in
256        link_hints annotation_window
257         (Array.concat
258          [ funtylid ;
259            funbolid ;
260            funnamel ;
261            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
262          ]
263         )
264 ;;
265
266 (*CSC: da riscrivere completamente eliminando il paciugo degli array - liste *)
267 let create_hint_from_obj annotation_window annobj =
268  let module C = Cic in
269   match annobj with
270      C.ADefinition (id,_,_,bo,ty,_) ->
271       let boid = get_id bo
272       and tyid = get_id ty in
273        link_hints annotation_window
274         [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
275            "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
276            "Body", "<node id = '" ^ boid ^ "'/>" ;
277            "Type", "<node id = '" ^ tyid ^ "'/>"
278         |]
279    | C.AAxiom (id,_,_,ty,_) ->
280       let 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            "Type", "<node id = '" ^ tyid ^ "'/>"
285         |]
286    | C.AVariable (id,_,_,bo,ty) ->
287       let tyid = get_id ty in
288        link_hints annotation_window
289         (match bo with
290             None ->
291              [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
292                 "Type", "<node id = '" ^ tyid ^ "'/>"
293              |]
294           | Some bo ->
295              let boid = get_id bo in
296               [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
297                  "Body", "<node id = '" ^ boid ^ "'/>" ;
298                  "Type", "<node id = '" ^ tyid ^ "'/>"
299               |]
300         )
301    | C.ACurrentProof (id,_,_,conjs,bo,ty) ->
302       let boid = get_id bo
303       and tyid = get_id ty
304       and conjsid = List.map (fun (_,te) -> get_id te) conjs in
305        link_hints annotation_window
306         (Array.append
307           [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
308              "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
309              "Body", "<node id = '" ^ boid ^ "'/>" ;
310              "Type", "<node id = '" ^ tyid ^ "'/>"
311           |]
312           (Array.mapi
313             (fun i id ->
314               "Conjecture " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
315             ) (Array.of_list conjsid)
316           )
317         )
318    | C.AInductiveDefinition (id,_,itl,_,_) ->
319       let itlids =
320        List.map
321         (fun (_,_,arity,cons) ->
322           get_id arity,
323           List.map (fun (_,ty,_) -> get_id ty) cons
324         ) itl
325       in
326        link_hints annotation_window
327         (Array.concat
328           [
329            [| "Ingredients","<attribute name = 'params' id = '" ^ id ^ "'/>" |];
330            (Array.mapi
331              (fun i _ ->
332                "Type Name " ^ string_of_int i,
333                "<attribute name = 'name' child = '" ^ string_of_int i ^
334                 "' id = '" ^ id ^ "'/>"
335              ) (Array.of_list itlids)
336            ) ;
337            (Array.mapi
338              (fun i (id,_) ->
339                "Type " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
340              ) (Array.of_list itlids)
341            ) ;
342            (Array.concat
343             (list_mapi
344              (fun i (_,consid) ->
345               (Array.mapi
346                 (fun j _ ->
347                   "Constructor Name " ^ string_of_int i ^ " " ^ string_of_int j,
348                   "<attribute name = 'name' id = '" ^ id ^ 
349                    "' child = '" ^ string_of_int i ^ "' grandchild = '" ^
350                    string_of_int j ^ "'/>"
351                 ) (Array.of_list consid)
352               ) ;
353              ) itlids
354             )
355            ) ;
356            (Array.concat
357             (list_mapi
358              (fun i (_,consid) ->
359               (Array.mapi
360                 (fun j id ->
361                   "Constructor " ^ string_of_int i ^ " " ^ string_of_int j,
362                   "<node id = '" ^ id ^ "'/>"
363                 ) (Array.of_list consid)
364               ) ;
365              ) itlids
366             )
367            )
368           ]
369         )
370 ;;
371
372 exception IdUnknown of string;;
373
374 let create_hints annotation_window (annobj,ids_to_targets) xpath =
375  try
376   match Hashtbl.find ids_to_targets xpath with
377      Cic.Object annobj -> create_hint_from_obj annotation_window annobj
378    | Cic.Term annterm -> create_hint_from_term annotation_window annterm
379  with
380   Not_found -> raise (IdUnknown xpath)
381 ;;