helm/interface/annotationParser2.ml

   1 exception IllFormedXml of int;;
   2
   3 (* Utility functions that transform a Pxp attribute into something useful *)
   4
   5 let string_of_attr a =
   6  let module T = Pxp_types in
   7   match a with
   8      T.Value s -> s
   9    | _ -> raise (IllFormedXml 0)
  10 ;;
  11
  12 exception DontKnowWhatToDo;;
  13
  14 let rec string_of_annotations n =
  15  let module D = Pxp_document in
  16  let module T = Pxp_types in
  17   match n#node_type with
  18      D.T_element s ->
  19       "<" ^ s ^
  20       List.fold_right
  21        (fun att i ->
  22          match n#attribute att with
  23             T.Value s -> " " ^ att ^ "=\"" ^ s ^ "\"" ^ i
  24           | T.Implied_value -> i
  25           | T.Valuelist l -> " " ^ att ^ "=\"" ^ String.concat " " l ^ "\"" ^ i
  26        ) (n#attribute_names) "" ^
  27       (match n#sub_nodes with
  28           [] -> "/>"
  29         | l ->
  30            ">" ^
  31            String.concat "" (List.map string_of_annotations l) ^
  32            "</" ^ s ^ ">"
  33       )
  34    | D.T_data -> n#data
  35    | _ -> raise DontKnowWhatToDo
  36 ;;
  37
  38 let get_annotation n =
  39  String.concat "" (List.map string_of_annotations (n#sub_nodes))
  40 ;;
  41
  42 let annotate_object ann obj =
  43  let module C = Cic in
  44   let rann =
  45    match obj with
  46       C.ADefinition (_, rann, _, _, _, _) -> rann
  47     | C.AAxiom (_, rann, _, _, _) -> rann
  48     | C.AVariable (_, rann, _, _, _) -> rann
  49     | C.ACurrentProof (_, rann, _, _, _, _) -> rann
  50     | C.AInductiveDefinition (_, rann, _, _, _) -> rann
  51   in
  52    rann := Some ann
  53 ;;
  54
  55 let annotate_term ann term =
  56  let module C = Cic in
  57   let rann =
  58    match term with
  59       C.ARel (_, rann, _, _) -> rann
  60     | C.AVar (_, rann, _) -> rann
  61     | C.AMeta (_, rann, _) -> rann
  62     | C.ASort (_, rann, _) -> rann
  63     | C.AImplicit (_, rann) -> rann
  64     | C.ACast (_, rann, _, _) -> rann
  65     | C.AProd (_, rann, _, _, _) -> rann
  66     | C.ALambda (_, rann, _, _, _) -> rann
  67     | C.ALetIn (_, rann, _, _, _) -> rann
  68     | C.AAppl (_, rann, _) -> rann
  69     | C.AConst (_, rann, _, _) -> rann
  70     | C.AAbst (_, rann, _) -> rann
  71     | C.AMutInd (_, rann, _, _, _) -> rann
  72     | C.AMutConstruct (_, rann, _, _, _, _) -> rann
  73     | C.AMutCase (_, rann, _, _, _, _, _, _) -> rann
  74     | C.AFix (_, rann, _, _) -> rann
  75     | C.ACoFix (_, rann, _, _) -> rann
  76   in
  77    rann := Some ann
  78 ;;
  79
  80 let annotate ids_to_targets n =
  81  let module D = Pxp_document in
  82  let module C = Cic in
  83   let annotate_elem n =
  84    let ntype = n # node_type in
  85    match ntype with
  86      D.T_element "Annotation" ->
  87        let of_uri = string_of_attr (n # attribute "of") in
  88         begin
  89          try
  90           match Hashtbl.find ids_to_targets of_uri with
  91              C.Object o -> annotate_object (get_annotation n) o
  92            | C.Term t -> annotate_term (get_annotation n) t
  93          with
  94           Not_found -> assert false
  95         end
  96    | D.T_element _ | D.T_data ->
  97       raise (IllFormedXml 1)
  98    | _ -> raise DontKnowWhatToDo
  99   in
 100    match n # node_type with
 101       D.T_element "Annotations" ->
 102        List.iter annotate_elem (n # sub_nodes)
 103     | _ -> raise (IllFormedXml 2)
 104 ;;