1 (******************************************************************************)
5 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
9 (******************************************************************************)
11 let deactivate_hints_from annotation_window n =
12 let annotation_hints = annotation_window#annotation_hints in
13 for i = n to Array.length annotation_hints - 1 do
14 annotation_hints.(i)#misc#hide ()
18 (* CSC: orripilante *)
19 (* the list of the signal ids *)
20 let sig_ids = ref ([] : GtkSignal.id list);;
22 let disconnect_hint annotation_window buttonno =
25 annotation_window#annotation_hints.(buttonno)#misc#disconnect id ;
30 (* link_hint annotation_window n label hint *)
31 (* set the label of the nth hint button of annotation_window to label *)
32 (* and the correspondent hint to hint *)
33 let link_hint annotation_window buttonno label hint =
34 let button = annotation_window#annotation_hints.(buttonno) in
36 (button#connect#clicked
37 (fun () -> (annotation_window#annotation : GEdit.text)#insert hint)
40 match button#children with
41 [labelw] -> (GMisc.label_cast labelw)#set_text label
45 exception TooManyHints;;
47 let link_hints annotation_window a =
48 if Array.length a > Array.length annotation_window#annotation_hints then
50 for i = List.length !sig_ids - 1 downto 0 do
51 disconnect_hint annotation_window i
54 (fun i (label,hint) -> link_hint annotation_window i label hint) a ;
55 deactivate_hints_from annotation_window (Array.length a)
62 | he::tl -> (f n he)::(aux (n + 1) tl)
70 C.ARel (id,_,_,_) -> id
71 | C.AVar (id,_,_) -> id
72 | C.AMeta (id,_,_) -> id
73 | C.ASort (id,_,_) -> id
74 | C.AImplicit (id,_) -> id
75 | C.ACast (id,_,_,_) -> id
76 | C.AProd (id,_,_,_,_) -> id
77 | C.ALambda (id,_,_,_,_) -> id
78 | C.AAppl (id,_,_) -> id
79 | C.AConst (id,_,_,_) -> id
80 | C.AAbst (id,_,_) -> id
81 | C.AMutInd (id,_,_,_,_) -> id
82 | C.AMutConstruct (id,_,_,_,_,_)-> id
83 | C.AMutCase (id,_,_,_,_,_,_,_) -> id
84 | C.AFix (id,_,_,_) -> id
85 | C.ACoFix (id,_,_,_) -> id
88 let create_hint_from_term annotation_window annterm =
92 link_hints annotation_window
93 [| "Binder", "<attribute name = 'binder' id = '" ^ id ^ "'/>" |]
95 link_hints annotation_window
96 [| "relURI???", "<attribute name = 'relUri' id = '" ^ id ^ "'/>" |]
98 link_hints annotation_window
99 [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
100 | C.ASort (id,_,_) ->
101 link_hints annotation_window
102 [| "Value", "<attribute name = 'value' id = '" ^ id ^ "'/>" |]
103 | C.AImplicit (id,_) ->
104 link_hints annotation_window [| |]
105 | C.ACast (id,_,bo,ty) ->
107 and tyid = get_id ty in
108 link_hints annotation_window
109 [| "Body", "<node id = '" ^ boid ^ "'/>" ;
110 "Type", "<node id = '" ^ tyid ^ "'/>"
112 | C.AProd (id,_,_,ty,bo) ->
114 and tyid = get_id ty in
115 link_hints annotation_window
117 "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
118 "Body", "<node id = '" ^ boid ^ "'/>" ;
119 "Type", "<node id = '" ^ tyid ^ "'/>"
121 | C.ALambda (id,_,_,ty,bo) ->
123 and tyid = get_id ty in
124 link_hints annotation_window
126 "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
127 "Body", "<node id = '" ^ boid ^ "'/>" ;
128 "Type", "<node id = '" ^ tyid ^ "'/>"
130 | C.AAppl (id,_,args) ->
133 (fun i te -> "Argument " ^ string_of_int i, "<node id ='" ^
137 link_hints annotation_window argsid
138 | C.AConst (id,_,_,_) ->
139 link_hints annotation_window
140 [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
141 | C.AAbst (id,_,_) ->
142 link_hints annotation_window
143 [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
144 | C.AMutInd (id,_,_,_,_) ->
145 link_hints annotation_window
146 [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
147 | C.AMutConstruct (id,_,_,_,_,_) ->
148 link_hints annotation_window
149 [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
150 | C.AMutCase (id,_,_,_,_,outty,te,pl) ->
151 let outtyid = get_id outty
155 (fun i te -> "Pattern " ^ string_of_int i, "<node id ='" ^
159 link_hints annotation_window
161 [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" ;
162 "Case Type", "<node id = '" ^ outtyid ^ "'/>" ;
163 "Term", "<node id = '" ^ teid ^ "'/>" ;
166 | C.AFix (id,_,_,funl) ->
170 "Type " ^ string_of_int i, "<node id ='" ^
176 "Body " ^ string_of_int i, "<node id ='" ^
182 "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
183 "' name = 'name' child='" ^ string_of_int i ^ "'/>")
188 "Recursive Index??? " ^ string_of_int i, "<attribute id = '" ^ id ^
189 "' name = 'recIndex' child='" ^ string_of_int i ^ "'/>")
192 link_hints annotation_window
198 [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
201 | C.ACoFix (id,_,_,funl) ->
205 "Type " ^ string_of_int i, "<node id ='" ^
211 "Body " ^ string_of_int i, "<node id ='" ^
217 "Name " ^ string_of_int i, "<attribute id ='" ^ id ^
218 "' name = 'name' child='" ^ string_of_int i ^ "'/>")
221 link_hints annotation_window
226 [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
231 (*CSC: da riscrivere completamente eliminando il paciugo degli array - liste *)
232 let create_hint_from_obj annotation_window annobj =
233 let module C = Cic in
235 C.ADefinition (id,_,_,bo,ty,_) ->
237 and tyid = get_id ty in
238 link_hints annotation_window
239 [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
240 "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
241 "Body", "<node id = '" ^ boid ^ "'/>" ;
242 "Type", "<node id = '" ^ tyid ^ "'/>"
244 | C.AAxiom (id,_,_,ty,_) ->
245 let tyid = get_id ty in
246 link_hints annotation_window
247 [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
248 "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
249 "Type", "<node id = '" ^ tyid ^ "'/>"
251 | C.AVariable (id,_,_,ty) ->
252 let tyid = get_id ty in
253 link_hints annotation_window
254 [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
255 "Type", "<node id = '" ^ tyid ^ "'/>"
257 | C.ACurrentProof (id,_,_,conjs,bo,ty) ->
260 and conjsid = List.map (fun (_,te) -> get_id te) conjs in
261 link_hints annotation_window
263 [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
264 "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
265 "Body", "<node id = '" ^ boid ^ "'/>" ;
266 "Type", "<node id = '" ^ tyid ^ "'/>"
270 "Conjecture " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
271 ) (Array.of_list conjsid)
274 | C.AInductiveDefinition (id,_,itl,_,_) ->
277 (fun (_,_,arity,cons) ->
279 List.map (fun (_,ty,_) -> get_id ty) cons
282 link_hints annotation_window
285 [| "Ingredients","<attribute name = 'params' id = '" ^ id ^ "'/>" |];
288 "Type Name " ^ string_of_int i,
289 "<attribute name = 'name' child = '" ^ string_of_int i ^
290 "' id = '" ^ id ^ "'/>"
291 ) (Array.of_list itlids)
295 "Type " ^ string_of_int i, "<node id = '" ^ id ^ "'/>"
296 ) (Array.of_list itlids)
303 "Constructor Name " ^ string_of_int i ^ " " ^ string_of_int j,
304 "<attribute name = 'name' id = '" ^ id ^
305 "' child = '" ^ string_of_int i ^ "' grandchild = '" ^
306 string_of_int j ^ "'/>"
307 ) (Array.of_list consid)
317 "Constructor " ^ string_of_int i ^ " " ^ string_of_int j,
318 "<node id = '" ^ id ^ "'/>"
319 ) (Array.of_list consid)
328 exception IdUnknown of string;;
330 let create_hints annotation_window (annobj,ids_to_targets) xpath =
332 match Hashtbl.find ids_to_targets xpath with
333 Cic.Object annobj -> create_hint_from_obj annotation_window annobj
334 | Cic.Term annterm -> create_hint_from_term annotation_window annterm
336 Not_found -> raise (IdUnknown xpath)