Initial revision

[helm.git] / helm / interface / cicXPath.prima_degli_identificatori.ml

diff --git a/helm/interface/cicXPath.prima_degli_identificatori.ml b/helm/interface/cicXPath.prima_degli_identificatori.ml
new file mode 100644 (file)
index 0000000..8a69d1a
--- /dev/null
+++ b/helm/interface/cicXPath.prima_degli_identificatori.ml
@@ -0,0 +1,102 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 11/04/2000                                 *)
+(*                                                                            *)
+(*                                                                            *)
+(******************************************************************************)
+
+(* functions to parse an XPath to retrieve the annotation *)
+
+exception WrongXPath of string;;
+
+let rec get_annotation_of_inductiveFun f xpath =
+ let module C = Cic in
+  match (xpath,f) with
+     1::tl,(_,_,ty,_) -> get_annotation_of_term ty tl
+   | 2::tl,(_,_,_,te) -> get_annotation_of_term te tl
+   | l,_ ->
+      raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
+
+and get_annotation_of_coinductiveFun f xpath =
+ let module C = Cic in
+  match (xpath,f) with
+     1::tl,(_,ty,_) -> get_annotation_of_term ty tl
+   | 2::tl,(_,_,te) -> get_annotation_of_term te tl
+   | l,_ ->
+      raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
+
+and get_annotation_of_inductiveType ty xpath =
+ let module C = Cic in
+  match (xpath,ty) with
+     1::tl,(_,_,arity,_) -> get_annotation_of_term arity tl
+   | n::tl,(_,_,_,cons) when n <= List.length cons + 1 ->
+      let (_,ty,_) = List.nth cons (n-2) in
+       get_annotation_of_term ty tl
+   | l,_ ->
+      raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
+
+and get_annotation_of_term term xpath =
+ let module C = Cic in
+  match (xpath,term) 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
+   | 1::tl,C.ACast (_,_,te,_) -> get_annotation_of_term te tl
+   | 2::tl,C.ACast (_,_,_,ty) -> get_annotation_of_term ty tl
+   | [],C.AProd (_,ann,_,_,_) -> ann
+   | 1::tl,C.AProd (_,_,_,so,_) -> get_annotation_of_term so tl
+   | 2::tl,C.AProd (_,_,_,_,ta) -> get_annotation_of_term ta tl
+   | [],C.ALambda (_,ann,_,_,_) -> ann
+   | 1::tl,C.ALambda (_,_,_,so,_) -> get_annotation_of_term so tl
+   | 2::tl,C.ALambda (_,_,_,_,ta) -> get_annotation_of_term ta tl
+   | [],C.AAppl (_,ann,_) -> ann
+   | n::tl,C.AAppl (_,_,l) when n <= List.length l ->
+      get_annotation_of_term (List.nth l (n-1)) tl
+   | [],C.AConst (_,ann,_,_) -> ann
+   | [],C.AAbst (_,ann,_) -> ann
+   | [],C.AMutInd (_,ann,_,_,_) -> ann
+   | [],C.AMutConstruct (_,ann,_,_,_,_) -> ann
+   | [],C.AMutCase (_,ann,_,_,_,_,_,_) -> ann
+   | 1::tl,C.AMutCase (_,_,_,_,_,outt,_,_) -> get_annotation_of_term outt tl
+   | 2::tl,C.AMutCase (_,_,_,_,_,_,te,_) -> get_annotation_of_term te tl
+   | n::tl,C.AMutCase (_,_,_,_,_,_,_,pl) when n <= List.length pl ->
+      get_annotation_of_term (List.nth pl (n-1)) tl
+   | [],C.AFix (_,ann,_,_) -> ann
+   | n::tl,C.AFix (_,_,_,fl) when n <= List.length fl ->
+      get_annotation_of_inductiveFun (List.nth fl (n-1)) tl
+   | [],C.ACoFix (_,ann,_,_) -> ann
+   | n::tl,C.ACoFix (_,_,_,fl) when n <= List.length fl ->
+      get_annotation_of_coinductiveFun (List.nth fl (n-1)) tl
+   | l,_ ->
+      raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
+;;
+
+let get_annotation (annobj,_) xpath =
+ let module C = Cic in
+  match (xpath,annobj) with
+     [],C.ADefinition (_,ann,_,_,_,_) -> ann
+   | 1::tl,C.ADefinition (_,_,_,bo,_,_) -> get_annotation_of_term bo tl
+   | 2::tl,C.ADefinition (_,_,_,_,ty,_) -> get_annotation_of_term ty tl
+   | [],C.AAxiom (_,ann,_,_,_) -> ann
+   | 1::tl,C.AAxiom (_,_,_,ty,_) -> get_annotation_of_term ty tl
+   | [],C.AVariable (_,ann,_,_) -> ann
+   | 1::tl,C.AVariable (_,_,_,ty) -> get_annotation_of_term ty tl
+   | [],C.ACurrentProof (_,ann,_,_,_,_) -> ann
+   | n::tl,C.ACurrentProof (_,ann,_,conjs,_,_) when n <= List.length conjs ->
+      get_annotation_of_term (snd (List.nth conjs (n-1))) tl
+   | n::tl,C.ACurrentProof (_,ann,_,conjs,bo,_) when n = List.length conjs + 1 ->
+      get_annotation_of_term bo tl
+   | n::tl,C.ACurrentProof (_,ann,_,conjs,_,ty) when n = List.length conjs + 2 ->
+      get_annotation_of_term ty tl
+   | [],C.AInductiveDefinition (_,ann,_,_,_) -> ann
+   | n::tl,C.AInductiveDefinition (_,_,tys,_,_) when n <= List.length tys ->
+      get_annotation_of_inductiveType (List.nth tys (n-1)) tl
+   | l,_ ->
+      raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
+;;