helm/interface/cicXPath.prima_degli_identificatori.ml

   1 (******************************************************************************)
   2 (*                                                                            *)
   3 (*                               PROJECT HELM                                 *)
   4 (*                                                                            *)
   5 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
   6 (*                                 11/04/2000                                 *)
   7 (*                                                                            *)
   8 (*                                                                            *)
   9 (******************************************************************************)
  10
  11 (* functions to parse an XPath to retrieve the annotation *)
  12
  13 exception WrongXPath of string;;
  14
  15 let rec get_annotation_of_inductiveFun f xpath =
  16  let module C = Cic in
  17   match (xpath,f) with
  18      1::tl,(_,_,ty,_) -> get_annotation_of_term ty tl
  19    | 2::tl,(_,_,_,te) -> get_annotation_of_term te tl
  20    | l,_ ->
  21       raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
  22
  23 and get_annotation_of_coinductiveFun f xpath =
  24  let module C = Cic in
  25   match (xpath,f) with
  26      1::tl,(_,ty,_) -> get_annotation_of_term ty tl
  27    | 2::tl,(_,_,te) -> get_annotation_of_term te tl
  28    | l,_ ->
  29       raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
  30
  31 and get_annotation_of_inductiveType ty xpath =
  32  let module C = Cic in
  33   match (xpath,ty) with
  34      1::tl,(_,_,arity,_) -> get_annotation_of_term arity tl
  35    | n::tl,(_,_,_,cons) when n <= List.length cons + 1 ->
  36       let (_,ty,_) = List.nth cons (n-2) in
  37        get_annotation_of_term ty tl
  38    | l,_ ->
  39       raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
  40
  41 and get_annotation_of_term term xpath =
  42  let module C = Cic in
  43   match (xpath,term) with
  44      [],C.ARel (_,ann,_,_) -> ann
  45    | [],C.AVar (_,ann,_) -> ann
  46    | [],C.AMeta (_,ann,_) -> ann
  47    | [],C.ASort (_,ann,_) -> ann
  48    | [],C.AImplicit (_,ann) -> ann
  49    | [],C.ACast (_,ann,_,_) -> ann
  50    | 1::tl,C.ACast (_,_,te,_) -> get_annotation_of_term te tl
  51    | 2::tl,C.ACast (_,_,_,ty) -> get_annotation_of_term ty tl
  52    | [],C.AProd (_,ann,_,_,_) -> ann
  53    | 1::tl,C.AProd (_,_,_,so,_) -> get_annotation_of_term so tl
  54    | 2::tl,C.AProd (_,_,_,_,ta) -> get_annotation_of_term ta tl
  55    | [],C.ALambda (_,ann,_,_,_) -> ann
  56    | 1::tl,C.ALambda (_,_,_,so,_) -> get_annotation_of_term so tl
  57    | 2::tl,C.ALambda (_,_,_,_,ta) -> get_annotation_of_term ta tl
  58    | [],C.AAppl (_,ann,_) -> ann
  59    | n::tl,C.AAppl (_,_,l) when n <= List.length l ->
  60       get_annotation_of_term (List.nth l (n-1)) tl
  61    | [],C.AConst (_,ann,_,_) -> ann
  62    | [],C.AAbst (_,ann,_) -> ann
  63    | [],C.AMutInd (_,ann,_,_,_) -> ann
  64    | [],C.AMutConstruct (_,ann,_,_,_,_) -> ann
  65    | [],C.AMutCase (_,ann,_,_,_,_,_,_) -> ann
  66    | 1::tl,C.AMutCase (_,_,_,_,_,outt,_,_) -> get_annotation_of_term outt tl
  67    | 2::tl,C.AMutCase (_,_,_,_,_,_,te,_) -> get_annotation_of_term te tl
  68    | n::tl,C.AMutCase (_,_,_,_,_,_,_,pl) when n <= List.length pl ->
  69       get_annotation_of_term (List.nth pl (n-1)) tl
  70    | [],C.AFix (_,ann,_,_) -> ann
  71    | n::tl,C.AFix (_,_,_,fl) when n <= List.length fl ->
  72       get_annotation_of_inductiveFun (List.nth fl (n-1)) tl
  73    | [],C.ACoFix (_,ann,_,_) -> ann
  74    | n::tl,C.ACoFix (_,_,_,fl) when n <= List.length fl ->
  75       get_annotation_of_coinductiveFun (List.nth fl (n-1)) tl
  76    | l,_ ->
  77       raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
  78 ;;
  79
  80 let get_annotation (annobj,_) xpath =
  81  let module C = Cic in
  82   match (xpath,annobj) with
  83      [],C.ADefinition (_,ann,_,_,_,_) -> ann
  84    | 1::tl,C.ADefinition (_,_,_,bo,_,_) -> get_annotation_of_term bo tl
  85    | 2::tl,C.ADefinition (_,_,_,_,ty,_) -> get_annotation_of_term ty tl
  86    | [],C.AAxiom (_,ann,_,_,_) -> ann
  87    | 1::tl,C.AAxiom (_,_,_,ty,_) -> get_annotation_of_term ty tl
  88    | [],C.AVariable (_,ann,_,_) -> ann
  89    | 1::tl,C.AVariable (_,_,_,ty) -> get_annotation_of_term ty tl
  90    | [],C.ACurrentProof (_,ann,_,_,_,_) -> ann
  91    | n::tl,C.ACurrentProof (_,ann,_,conjs,_,_) when n <= List.length conjs ->
  92       get_annotation_of_term (snd (List.nth conjs (n-1))) tl
  93    | n::tl,C.ACurrentProof (_,ann,_,conjs,bo,_) when n = List.length conjs + 1 ->
  94       get_annotation_of_term bo tl
  95    | n::tl,C.ACurrentProof (_,ann,_,conjs,_,ty) when n = List.length conjs + 2 ->
  96       get_annotation_of_term ty tl
  97    | [],C.AInductiveDefinition (_,ann,_,_,_) -> ann
  98    | n::tl,C.AInductiveDefinition (_,_,tys,_,_) when n <= List.length tys ->
  99       get_annotation_of_inductiveType (List.nth tys (n-1)) tl
 100    | l,_ ->
 101       raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l ""))
 102 ;;