helm/interface/annotation2Xml.ml

   1 (*CSC codice cut & paste da cicPp e xmlcommand *)
   2
   3 exception ImpossiblePossible;;
   4 exception NotImplemented;;
   5 exception BinderNotSpecified;;
   6
   7 let dtdname = "http://localhost:8081/getdtd?url=annotations.dtd";;
   8
   9 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
  10 let print_term =
  11  let rec aux =
  12   let module C = Cic in
  13   let module X = Xml in
  14   let module U = UriManager in
  15     function
  16        C.ARel (id,ann,_,_) ->
  17         (match !ann with
  18             None -> [<>]
  19           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  20         )
  21      | C.AVar (id,ann,_) ->
  22         (match !ann with
  23             None -> [<>]
  24           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  25         )
  26      | C.AMeta (id,ann,_) ->
  27         (match !ann with
  28             None -> [<>]
  29           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  30         )
  31      | C.ASort (id,ann,_) ->
  32         (match !ann with
  33             None -> [<>]
  34           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  35         )
  36      | C.AImplicit _ -> raise NotImplemented
  37      | C.AProd (id,ann,_,s,t) ->
  38         [< (match !ann with
  39                None -> [<>]
  40              | Some ann ->
  41                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  42            ) ;
  43            aux s ;
  44            aux t
  45         >]
  46      | C.ACast (id,ann,v,t) ->
  47         [< (match !ann with
  48                None -> [<>]
  49              | Some ann ->
  50                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  51            ) ;
  52            aux v ;
  53            aux t
  54         >]
  55      | C.ALambda (id,ann,_,s,t) ->
  56         [< (match !ann with
  57                None -> [<>]
  58              | Some ann ->
  59                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  60            ) ;
  61            aux s ;
  62            aux t
  63         >]
  64      | C.ALetIn (id,ann,_,s,t) ->
  65         [< (match !ann with
  66                None -> [<>]
  67              | Some ann ->
  68                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  69            ) ;
  70            aux s ;
  71            aux t
  72         >]
  73      | C.AAppl (id,ann,li) ->
  74         [< (match !ann with
  75                None -> [<>]
  76              | Some ann ->
  77                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  78            ) ;
  79            List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
  80         >]
  81      | C.AConst (id,ann,_,_) ->
  82         (match !ann with
  83             None -> [<>]
  84           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  85         )
  86      | C.AAbst (id,ann,_) -> raise NotImplemented
  87      | C.AMutInd (id,ann,_,_,_) ->
  88         (match !ann with
  89             None -> [<>]
  90           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  91         )
  92      | C.AMutConstruct (id,ann,_,_,_,_) ->
  93         (match !ann with
  94             None -> [<>]
  95           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  96         )
  97      | C.AMutCase (id,ann,_,_,_,ty,te,patterns) ->
  98         [< (match !ann with
  99                None -> [<>]
 100              | Some ann ->
 101                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 102            ) ;
 103            aux ty ;
 104            aux te ;
 105            List.fold_right
 106             (fun x i -> [< aux x ; i>])
 107             patterns [<>]
 108         >]
 109      | C.AFix (id, ann, _, funs) ->
 110         [< (match !ann with
 111                None -> [<>]
 112              | Some ann ->
 113                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 114            ) ;
 115            List.fold_right
 116             (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
 117         >]
 118      | C.ACoFix (id, ann,no,funs) ->
 119         [< (match !ann with
 120                None -> [<>]
 121              | Some ann ->
 122                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 123            ) ;
 124            List.fold_right
 125             (fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
 126         >]
 127  in
 128   aux
 129 ;;
 130
 131 let print_mutual_inductive_type (_,_,arity,constructors) =
 132  [< print_term arity ;
 133     List.fold_right
 134      (fun (name,ty,_) i -> [< print_term ty ; i >]) constructors [<>]
 135  >]
 136 ;;
 137
 138 let target_uri_of_annotation_uri uri =
 139  Str.replace_first (Str.regexp "\.ann$") "" (UriManager.string_of_uri uri)
 140 ;;
 141
 142 let pp_annotation obj curi =
 143  let module C = Cic in
 144  let module X = Xml in
 145   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 146      X.xml_cdata ("<!DOCTYPE Annotations SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 147      X.xml_nempty "Annotations" ["of", target_uri_of_annotation_uri curi]
 148       begin
 149        match obj with
 150          C.ADefinition (xid, ann, _, te, ty, _) ->
 151           [< (match !ann with
 152                  None -> [<>]
 153                | Some ann ->
 154                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 155              ) ;
 156              print_term te ;
 157              print_term ty
 158           >]
 159        | C.AAxiom (xid, ann, _, ty, _) ->
 160           [< (match !ann with
 161                  None -> [<>]
 162                | Some ann ->
 163                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 164              ) ;
 165              print_term ty
 166           >]
 167        | C.AVariable (xid, ann, _, bo, ty) ->
 168           [< (match !ann with
 169                  None -> [<>]
 170                | Some ann ->
 171                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 172              ) ;
 173              (match bo with
 174                  None -> [<>]
 175                | Some bo -> print_term bo
 176              ) ;
 177              print_term ty
 178           >]
 179        | C.ACurrentProof (xid, ann, _, conjs, bo, ty) ->
 180           [< (match !ann with
 181                  None -> [<>]
 182                | Some ann ->
 183                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 184              ) ;
 185              List.fold_right
 186               (fun (_,t) i -> [< print_term t ; i >])
 187               conjs [<>] ;
 188              print_term bo ;
 189              print_term ty
 190           >]
 191        | C.AInductiveDefinition (xid, ann, tys, params, paramsno) ->
 192           [< (match !ann with
 193                  None -> [<>]
 194                | Some ann ->
 195                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 196              ) ;
 197              List.fold_right
 198               (fun x i -> [< print_mutual_inductive_type x ; i >])
 199               tys [< >]
 200           >]
 201       end
 202   >]
 203 ;;