first moogle template checkin

[helm.git] / helm / ocaml / cic_annotations / cicXPath.ml

diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml
index 776d229afaf826ecfa4216157352e89516577d5b..75a598d91990728b4361452e750bc7669778cd6c 100644 (file)
--- a/helm/ocaml/cic_annotations/cicXPath.ml
+++ b/helm/ocaml/cic_annotations/cicXPath.ml
@@ -33,45 +33,114 @@
 (*                                                                            *)
 (******************************************************************************)
 
-let get_annotation_from_term annterm =
- let module C = Cic in
-  match annterm with
-     C.ARel (_,ann,_,_)             -> ann
-   | C.AVar (_,ann,_)               -> ann
-   | C.AMeta (_,ann,_)              -> ann
-   | C.ASort (_,ann,_)              -> ann
-   | C.AImplicit (_,ann)            -> ann
-   | C.ACast (_,ann,_,_)            -> ann
-   | C.AProd (_,ann,_,_,_)          -> ann
-   | C.ALambda (_,ann,_,_,_)        -> ann
-   | C.ALetIn (_,ann,_,_,_)         -> ann
-   | C.AAppl (_,ann,_)              -> ann
-   | C.AConst (_,ann,_,_)           -> ann
-   | C.AAbst (_,ann,_)              -> ann
-   | C.AMutInd (_,ann,_,_,_)        -> ann
-   | C.AMutConstruct (_,ann,_,_,_,_)-> ann
-   | C.AMutCase (_,ann,_,_,_,_,_,_) -> ann
-   | C.AFix (_,ann,_,_)             -> ann
-   | C.ACoFix (_,ann,_,_)           -> ann
-;;
-
-let get_annotation_from_obj annobj =
- let module C = Cic in
-  match annobj with
-     C.ADefinition (_,ann,_,_,_,_)        -> ann
-   | C.AAxiom (_,ann,_,_,_)               -> ann
-   | C.AVariable (_,ann,_,_,_)            -> ann
-   | C.ACurrentProof (_,ann,_,_,_,_)      -> ann
-   | C.AInductiveDefinition (_,ann,_,_,_) -> ann
+let get_annotation ids_to_annotations xpath =
+ try
+  Some (Hashtbl.find ids_to_annotations xpath)
+ with
+  Not_found -> None
 ;;
 
-exception IdUnknown of string;;
+exception MoreThanOneTargetFor of Cic.id;;
 
-let get_annotation (annobj,ids_to_targets) xpath =
- try
-  match Hashtbl.find ids_to_targets xpath with
-     Cic.Object annobj -> get_annotation_from_obj annobj
-   | Cic.Term annterm -> get_annotation_from_term annterm
- with
-  Not_found -> raise (IdUnknown xpath)
+(* creates a hashtable mapping each unique id to a node of the annotated 
+object *)
+let get_ids_to_targets annobj =
+ let module C = Cic in
+  let ids_to_targets = Hashtbl.create 503 in
+   let set_target id target =
+    try
+     ignore (Hashtbl.find ids_to_targets id) ;
+     raise (MoreThanOneTargetFor id)
+    with
+     Not_found -> Hashtbl.add ids_to_targets id target
+   in
+    let rec add_target_term t =
+     match t with
+        C.ARel (id,_,_,_)
+      | C.AMeta (id,_,_)
+      | C.ASort (id,_)
+      | C.AImplicit (id, _) ->
+         set_target id (C.Term t)
+      | C.ACast (id,va,ty) ->
+         set_target id (C.Term t) ;
+         add_target_term va ;
+         add_target_term ty
+      | C.AProd (id,_,so,ta)
+      | C.ALambda (id,_,so,ta)
+      | C.ALetIn (id,_,so,ta) ->
+         set_target id (C.Term t) ;
+         add_target_term so ;
+         add_target_term ta
+      | C.AAppl (id,l) ->
+         set_target id (C.Term t) ;
+         List.iter add_target_term l
+      | C.AVar (id,_,exp_named_subst)
+      | C.AConst (id,_,exp_named_subst)
+      | C.AMutInd (id,_,_,exp_named_subst)
+      | C.AMutConstruct (id,_,_,_,exp_named_subst) ->
+         set_target id (C.Term t) ;
+         List.iter (function (_,t) -> add_target_term t) exp_named_subst
+      | C.AMutCase (id,_,_,ot,it,pl) ->
+         set_target id (C.Term t) ;
+         List.iter add_target_term (ot::it::pl)
+      | C.AFix (id,_,ifl) ->
+         set_target id (C.Term t) ;
+         List.iter
+          (function (_,_,_,ty,bo) ->
+            add_target_term ty ;
+            add_target_term bo
+          ) ifl
+      | C.ACoFix (id,_,cfl) ->
+         set_target id (C.Term t) ;
+         List.iter
+          (function (_,_,ty,bo) ->
+            add_target_term ty ;
+            add_target_term bo
+          ) cfl
+    in
+     let add_target_obj annobj =
+      match annobj with
+        C.AConstant (id,idbody,_,bo,ty,_) ->
+         set_target id (C.Object annobj) ;
+         (match idbody,bo with
+             Some idbody,Some bo ->
+              set_target idbody (C.ConstantBody annobj) ;
+              add_target_term bo
+           | None, None -> ()
+           | _,_ -> assert false
+         ) ;
+         add_target_term ty
+      | C.AVariable (id,_,None,ty,_) ->
+         set_target id (C.Object annobj) ;
+         add_target_term ty
+      | C.AVariable (id,_,Some bo,ty,_) ->
+         set_target id (C.Object annobj) ;
+         add_target_term bo ;
+         add_target_term ty
+      | C.ACurrentProof (id,idbody,_,cl,bo,ty,_) ->
+         set_target id (C.Object annobj) ;
+         set_target idbody (C.ConstantBody annobj) ;
+         List.iter (function (cid,_,context, t) as annconj ->
+           set_target cid (C.Conjecture annconj) ;
+          List.iter 
+            (function ((hid,h) as annhyp) ->
+               set_target hid (C.Hypothesis annhyp) ;
+               match h with
+                 Some (_,C.ADecl at) -> add_target_term at
+               | Some (_,C.ADef at) -> add_target_term at
+               | None -> ()
+            ) context;
+          add_target_term t) cl ;
+         add_target_term bo ;
+         add_target_term ty
+      | C.AInductiveDefinition (id,itl,_,_) ->
+         set_target id (C.Object annobj) ;
+         List.iter
+          (function (_,_,_,arity,cl) ->
+            add_target_term arity ;
+            List.iter (function (_,ty) -> add_target_term ty) cl
+          ) itl
+     in
+      add_target_obj annobj ;
+      ids_to_targets
 ;;