X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FannotationHelper%2FcicAnnotationHinter.ml;h=7cf3cddbb8841b44010e1bfe03bb3afae4662ffe;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=86bcb4588b163202ed176b4a7855d749182777d5;hpb=ff6eee275d22bd158f9ccd451aaae0cb61659a6e;p=helm.git
diff --git a/helm/annotationHelper/cicAnnotationHinter.ml b/helm/annotationHelper/cicAnnotationHinter.ml
index 86bcb4588..7cf3cddbb 100644
--- a/helm/annotationHelper/cicAnnotationHinter.ml
+++ b/helm/annotationHelper/cicAnnotationHinter.ml
@@ -59,7 +59,7 @@ let link_hint annotation_window buttonno label hint =
let button = annotation_window#annotation_hints.(buttonno) in
sig_ids :=
(button#connect#clicked
- (fun () -> (annotation_window#annotation : GEdit.text)#insert hint)
+ ~callback:(fun () -> (annotation_window#annotation : GEdit.text)#insert hint)
) :: !sig_ids ;
button#misc#show () ;
match button#children with
@@ -92,50 +92,61 @@ let list_mapi f =
let get_id annterm =
let module C = Cic in
match annterm with
- C.ARel (id,_,_,_) -> id
- | C.AVar (id,_,_) -> id
- | C.AMeta (id,_,_) -> id
- | C.ASort (id,_,_) -> id
- | C.AImplicit (id,_) -> id
- | C.ACast (id,_,_,_) -> id
- | C.AProd (id,_,_,_,_) -> id
- | C.ALambda (id,_,_,_,_) -> id
- | C.ALetIn (id,_,_,_,_) -> id
- | C.AAppl (id,_,_) -> id
- | C.AConst (id,_,_,_) -> id
- | C.AAbst (id,_,_) -> id
- | C.AMutInd (id,_,_,_,_) -> id
- | C.AMutConstruct (id,_,_,_,_,_)-> id
- | C.AMutCase (id,_,_,_,_,_,_,_) -> id
- | C.AFix (id,_,_,_) -> id
- | C.ACoFix (id,_,_,_) -> id
+ C.ARel (id,_,_)
+ | C.AVar (id,_)
+ | C.AMeta (id,_,_)
+ | C.ASort (id,_)
+ | C.AImplicit id
+ | C.ACast (id,_,_)
+ | C.AProd (id,_,_,_)
+ | C.ALambda (id,_,_,_)
+ | C.ALetIn (id,_,_,_)
+ | C.AAppl (id,_)
+ | C.AConst (id,_,_)
+ | C.AMutInd (id,_,_,_)
+ | C.AMutConstruct (id,_,_,_,_)
+ | C.AMutCase (id,_,_,_,_,_,_)
+ | C.AFix (id,_,_)
+ | C.ACoFix (id,_,_) -> id
;;
let create_hint_from_term annotation_window annterm =
let module C = Cic in
match annterm with
- C.ARel (id,_,_,_) ->
+ C.ARel (id,_,_) ->
link_hints annotation_window
[| "Binder", "" |]
- | C.AVar (id,_,_) ->
+ | C.AVar (id,_) ->
link_hints annotation_window
[| "relURI???", "" |]
- | C.AMeta (id,_,_) ->
- link_hints annotation_window
- [| "Number", "" |]
- | C.ASort (id,_,_) ->
+ | C.AMeta (id,_,subst) ->
+ let res =
+ Array.append
+ [| "Number", "" |]
+ (Array.mapi
+ (fun i s ->
+ match s with
+ None ->
+ "Argument " ^ string_of_int i, "_"
+ | Some t ->
+ "Argument " ^ string_of_int i, ""
+ ) (Array.of_list subst)
+ )
+ in
+ link_hints annotation_window res
+ | C.ASort (id,_) ->
link_hints annotation_window
[| "Value", "" |]
- | C.AImplicit (id,_) ->
+ | C.AImplicit id ->
link_hints annotation_window [| |]
- | C.ACast (id,_,bo,ty) ->
+ | C.ACast (id,bo,ty) ->
let boid = get_id bo
and tyid = get_id ty in
link_hints annotation_window
[| "Body", "" ;
"Type", ""
|]
- | C.AProd (id,_,_,ty,bo) ->
+ | C.AProd (id,_,ty,bo) ->
let boid = get_id bo
and tyid = get_id ty in
link_hints annotation_window
@@ -144,7 +155,7 @@ let create_hint_from_term annotation_window annterm =
"Body", "" ;
"Type", ""
|]
- | C.ALambda (id,_,_,ty,bo) ->
+ | C.ALambda (id,_,ty,bo) ->
let boid = get_id bo
and tyid = get_id ty in
link_hints annotation_window
@@ -153,7 +164,7 @@ let create_hint_from_term annotation_window annterm =
"Body", "" ;
"Type", ""
|]
- | C.ALetIn (id,_,_,ty,bo) ->
+ | C.ALetIn (id,_,ty,bo) ->
let boid = get_id bo
and tyid = get_id ty in
link_hints annotation_window
@@ -162,7 +173,7 @@ let create_hint_from_term annotation_window annterm =
"Term", "" ;
"Target", ""
|]
- | C.AAppl (id,_,args) ->
+ | C.AAppl (id,args) ->
let argsid =
Array.mapi
(fun i te -> "Argument " ^ string_of_int i, "" |]
- | C.AAbst (id,_,_) ->
+ | C.AConst (id,_,_) ->
link_hints annotation_window
[| "Uri???", "" |]
- | C.AMutInd (id,_,_,_,_) ->
+ | C.AMutInd (id,_,_,_) ->
link_hints annotation_window
[| "Uri???", "" |]
- | C.AMutConstruct (id,_,_,_,_,_) ->
+ | C.AMutConstruct (id,_,_,_,_) ->
link_hints annotation_window
[| "Uri???", "" |]
- | C.AMutCase (id,_,_,_,_,outty,te,pl) ->
+ | C.AMutCase (id,_,_,_,outty,te,pl) ->
let outtyid = get_id outty
and teid = get_id te
and plid =
@@ -198,7 +206,7 @@ let create_hint_from_term annotation_window annterm =
"Term", "" ;
|]
plid)
- | C.AFix (id,_,_,funl) ->
+ | C.AFix (id,_,funl) ->
let funtylid =
Array.mapi
(fun i (_,_,ty,_) ->
@@ -233,7 +241,7 @@ let create_hint_from_term annotation_window annterm =
[| "NoFun???", "" |]
]
)
- | C.ACoFix (id,_,_,funl) ->
+ | C.ACoFix (id,_,funl) ->
let funtylid =
Array.mapi
(fun i (_,ty,_) ->
@@ -267,7 +275,7 @@ let create_hint_from_term annotation_window annterm =
let create_hint_from_obj annotation_window annobj =
let module C = Cic in
match annobj with
- C.ADefinition (id,_,_,bo,ty,_) ->
+ C.ADefinition (id,_,bo,ty,_) ->
let boid = get_id bo
and tyid = get_id ty in
link_hints annotation_window
@@ -276,14 +284,14 @@ let create_hint_from_obj annotation_window annobj =
"Body", "" ;
"Type", ""
|]
- | C.AAxiom (id,_,_,ty,_) ->
+ | C.AAxiom (id,_,ty,_) ->
let tyid = get_id ty in
link_hints annotation_window
[| "Name", "" ;
"Ingredients", "" ;
"Type", ""
|]
- | C.AVariable (id,_,_,bo,ty) ->
+ | C.AVariable (id,_,bo,ty) ->
let tyid = get_id ty in
link_hints annotation_window
(match bo with
@@ -298,11 +306,12 @@ let create_hint_from_obj annotation_window annobj =
"Type", ""
|]
)
- | C.ACurrentProof (id,_,_,conjs,bo,ty) ->
+ | C.ACurrentProof (id,_,conjs,bo,ty) ->
let boid = get_id bo
and tyid = get_id ty
- and conjsid = List.map (fun (_,te) -> get_id te) conjs in
+ and conjsid = List.map (fun (id,_,_,_) -> id) conjs in
link_hints annotation_window
+(*CSC: never tested since the introduction of the new Metas *)
(Array.append
[| "Name", "" ;
"Ingredients", "" ;
@@ -315,7 +324,7 @@ let create_hint_from_obj annotation_window annobj =
) (Array.of_list conjsid)
)
)
- | C.AInductiveDefinition (id,_,itl,_,_) ->
+ | C.AInductiveDefinition (id,itl,_,_) ->
let itlids =
List.map
(fun (_,_,arity,cons) ->
@@ -371,11 +380,14 @@ let create_hint_from_obj annotation_window annobj =
exception IdUnknown of string;;
-let create_hints annotation_window (annobj,ids_to_targets) xpath =
+let create_hints annotation_window ids_to_targets xpath =
try
match Hashtbl.find ids_to_targets xpath with
Cic.Object annobj -> create_hint_from_obj annotation_window annobj
| Cic.Term annterm -> create_hint_from_term annotation_window annterm
+(*CSC: never tested since the introduction of the new Metas *)
+ | Cic.Hypothesis _
+ | Cic.Conjecture _ -> assert false
with
Not_found -> raise (IdUnknown xpath)
;;