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.AAppl (id,ann,li) ->
  65         [< (match !ann with
  66                None -> [<>]
  67              | Some ann ->
  68                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  69            ) ;
  70            List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
  71         >]
  72      | C.AConst (id,ann,_,_) ->
  73         (match !ann with
  74             None -> [<>]
  75           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  76         )
  77      | C.AAbst (id,ann,_) -> raise NotImplemented
  78      | C.AMutInd (id,ann,_,_,_) ->
  79         (match !ann with
  80             None -> [<>]
  81           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  82         )
  83      | C.AMutConstruct (id,ann,_,_,_,_) ->
  84         (match !ann with
  85             None -> [<>]
  86           | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  87         )
  88      | C.AMutCase (id,ann,_,_,_,ty,te,patterns) ->
  89         [< (match !ann with
  90                None -> [<>]
  91              | Some ann ->
  92                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
  93            ) ;
  94            aux ty ;
  95            aux te ;
  96            List.fold_right
  97             (fun x i -> [< aux x ; i>])
  98             patterns [<>]
  99         >]
 100      | C.AFix (id, ann, _, funs) ->
 101         [< (match !ann with
 102                None -> [<>]
 103              | Some ann ->
 104                 (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
 105            ) ;
 106            List.fold_right
 107             (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
 108         >]
 109      | C.ACoFix (id, ann,no,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  in
 119   aux
 120 ;;
 121
 122 let print_mutual_inductive_type (_,_,arity,constructors) =
 123  [< print_term arity ;
 124     List.fold_right
 125      (fun (name,ty,_) i -> [< print_term ty ; i >]) constructors [<>]
 126  >]
 127 ;;
 128
 129 let target_uri_of_annotation_uri uri =
 130  Str.replace_first (Str.regexp "\.ann$") "" (UriManager.string_of_uri uri)
 131 ;;
 132
 133 let pp_annotation obj curi =
 134  let module C = Cic in
 135  let module X = Xml in
 136   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 137      X.xml_cdata ("<!DOCTYPE Annotations SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 138      X.xml_nempty "Annotations" ["of", target_uri_of_annotation_uri curi]
 139       begin
 140        match obj with
 141          C.ADefinition (xid, ann, _, te, ty, _) ->
 142           [< (match !ann with
 143                  None -> [<>]
 144                | Some ann ->
 145                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 146              ) ;
 147              print_term te ;
 148              print_term ty
 149           >]
 150        | C.AAxiom (xid, ann, _, 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 ty
 157           >]
 158        | C.AVariable (xid, ann, _, ty) ->
 159           [< (match !ann with
 160                  None -> [<>]
 161                | Some ann ->
 162                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 163              ) ;
 164              print_term ty
 165           >]
 166        | C.ACurrentProof (xid, ann, _, conjs, bo, ty) ->
 167           [< (match !ann with
 168                  None -> [<>]
 169                | Some ann ->
 170                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 171              ) ;
 172              List.fold_right
 173               (fun (_,t) i -> [< print_term t ; i >])
 174               conjs [<>] ;
 175              print_term bo ;
 176              print_term ty
 177           >]
 178        | C.AInductiveDefinition (xid, ann, tys, params, paramsno) ->
 179           [< (match !ann with
 180                  None -> [<>]
 181                | Some ann ->
 182                   X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
 183              ) ;
 184              List.fold_right
 185               (fun x i -> [< print_mutual_inductive_type x ; i >])
 186               tys [< >]
 187           >]
 188       end
 189   >]
 190 ;;