helm/interface/annotation2Xml.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (*CSC codice cut & paste da cicPp e xmlcommand *)
  27
  28 exception ImpossiblePossible;;
  29 exception NotImplemented;;
  30 exception BinderNotSpecified;;
  31
  32 let dtdname = "http://localhost:8081/getdtd?url=annotations.dtd";;
  33
  34 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
  35 let print_term =
  36  let rec aux =
  37   let module C = Cic in
  38   let module X = Xml in
  39   let module U = UriManager in
  40     function
  41        C.ARel (id,ann,_,_) ->
  42         (match !ann with
  43             None -> [<>]
  44           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  45         )
  46      | C.AVar (id,ann,_) ->
  47         (match !ann with
  48             None -> [<>]
  49           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  50         )
  51      | C.AMeta (id,ann,_) ->
  52         (match !ann with
  53             None -> [<>]
  54           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  55         )
  56      | C.ASort (id,ann,_) ->
  57         (match !ann with
  58             None -> [<>]
  59           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  60         )
  61      | C.AImplicit _ -> raise NotImplemented
  62      | C.AProd (id,ann,_,s,t) ->
  63         [< (match !ann with
  64                None -> [<>]
  65              | Some ann ->
  66                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  67            ) ;
  68            aux s ;
  69            aux t
  70         >]
  71      | C.ACast (id,ann,v,t) ->
  72         [< (match !ann with
  73                None -> [<>]
  74              | Some ann ->
  75                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  76            ) ;
  77            aux v ;
  78            aux t
  79         >]
  80      | C.ALambda (id,ann,_,s,t) ->
  81         [< (match !ann with
  82                None -> [<>]
  83              | Some ann ->
  84                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  85            ) ;
  86            aux s ;
  87            aux t
  88         >]
  89      | C.ALetIn (id,ann,_,s,t) ->
  90         [< (match !ann with
  91                None -> [<>]
  92              | Some ann ->
  93                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  94            ) ;
  95            aux s ;
  96            aux t
  97         >]
  98      | C.AAppl (id,ann,li) ->
  99         [< (match !ann with
 100                None -> [<>]
 101              | Some ann ->
 102                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 103            ) ;
 104            List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
 105         >]
 106      | C.AConst (id,ann,_,_) ->
 107         (match !ann with
 108             None -> [<>]
 109           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 110         )
 111      | C.AAbst (id,ann,_) -> raise NotImplemented
 112      | C.AMutInd (id,ann,_,_,_) ->
 113         (match !ann with
 114             None -> [<>]
 115           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 116         )
 117      | C.AMutConstruct (id,ann,_,_,_,_) ->
 118         (match !ann with
 119             None -> [<>]
 120           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 121         )
 122      | C.AMutCase (id,ann,_,_,_,ty,te,patterns) ->
 123         [< (match !ann with
 124                None -> [<>]
 125              | Some ann ->
 126                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 127            ) ;
 128            aux ty ;
 129            aux te ;
 130            List.fold_right
 131             (fun x i -> [< aux x ; i>])
 132             patterns [<>]
 133         >]
 134      | C.AFix (id, ann, _, funs) ->
 135         [< (match !ann with
 136                None -> [<>]
 137              | Some ann ->
 138                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 139            ) ;
 140            List.fold_right
 141             (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
 142         >]
 143      | C.ACoFix (id, ann,no,funs) ->
 144         [< (match !ann with
 145                None -> [<>]
 146              | Some ann ->
 147                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 148            ) ;
 149            List.fold_right
 150             (fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
 151         >]
 152  in
 153   aux
 154 ;;
 155
 156 let print_mutual_inductive_type (_,_,arity,constructors) =
 157  [< print_term arity ;
 158     List.fold_right
 159      (fun (name,ty,_) i -> [< print_term ty ; i >]) constructors [<>]
 160  >]
 161 ;;
 162
 163 let target_uri_of_annotation_uri uri =
 164  Str.replace_first (Str.regexp "\.ann$") "" (UriManager.string_of_uri uri)
 165 ;;
 166
 167 let pp_annotation obj curi =
 168  let module C = Cic in
 169  let module X = Xml in
 170   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 171      X.xml_cdata ("<!DOCTYPE Annotations SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 172      X.xml_nempty "Annotations" ["of", target_uri_of_annotation_uri curi]
 173       begin
 174        match obj with
 175          C.ADefinition (xid, ann, _, te, ty, _) ->
 176           [< (match !ann with
 177                  None -> [<>]
 178                | Some ann ->
 179                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 180              ) ;
 181              print_term te ;
 182              print_term ty
 183           >]
 184        | C.AAxiom (xid, ann, _, ty, _) ->
 185           [< (match !ann with
 186                  None -> [<>]
 187                | Some ann ->
 188                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 189              ) ;
 190              print_term ty
 191           >]
 192        | C.AVariable (xid, ann, _, bo, ty) ->
 193           [< (match !ann with
 194                  None -> [<>]
 195                | Some ann ->
 196                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 197              ) ;
 198              (match bo with
 199                  None -> [<>]
 200                | Some bo -> print_term bo
 201              ) ;
 202              print_term ty
 203           >]
 204        | C.ACurrentProof (xid, ann, _, conjs, bo, ty) ->
 205           [< (match !ann with
 206                  None -> [<>]
 207                | Some ann ->
 208                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 209              ) ;
 210              List.fold_right
 211               (fun (_,t) i -> [< print_term t ; i >])
 212               conjs [<>] ;
 213              print_term bo ;
 214              print_term ty
 215           >]
 216        | C.AInductiveDefinition (xid, ann, tys, params, paramsno) ->
 217           [< (match !ann with
 218                  None -> [<>]
 219                | Some ann ->
 220                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 221              ) ;
 222              List.fold_right
 223               (fun x i -> [< print_mutual_inductive_type x ; i >])
 224               tys [< >]
 225           >]
 226       end
 227   >]
 228 ;;