helm/gTopLevel/cic2Xml.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 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
  31
  32 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
  33 let print_term curi ~ids_to_inner_sorts =
  34  let rec aux =
  35   let module C = Cic in
  36   let module X = Xml in
  37   let module U = UriManager in
  38     function
  39        C.ARel (id,n,b) ->
  40         let sort = Hashtbl.find ids_to_inner_sorts id in
  41          X.xml_empty "REL"
  42           ["value",(string_of_int n) ; "binder",b ; "id",id ; "sort",sort]
  43      | C.AVar (id,uri) ->
  44         let vdepth = U.depth_of_uri uri
  45         and cdepth = U.depth_of_uri curi
  46         and sort = Hashtbl.find ids_to_inner_sorts id in
  47          X.xml_empty "VAR"
  48           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
  49             (U.name_of_uri uri) ;
  50            "id",id ; "sort",sort]
  51      | C.AMeta (id,n,l) ->
  52         let sort = Hashtbl.find ids_to_inner_sorts id in
  53          X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
  54           (List.fold_left
  55             (fun i t ->
  56               match t with
  57                  Some t' ->
  58                   [< i ; X.xml_nempty "substitution" [] (aux t') >]
  59                | None ->
  60                   [< i ; X.xml_empty "substitution" [] >]
  61             ) [< >] l)
  62      | C.ASort (id,s) ->
  63         let string_of_sort =
  64          function
  65             C.Prop -> "Prop"
  66           | C.Set  -> "Set"
  67           | C.Type -> "Type"
  68         in
  69          X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
  70      | C.AImplicit _ -> raise NotImplemented
  71      | C.AProd (id,C.Anonimous,s,t) ->
  72         let ty = Hashtbl.find ids_to_inner_sorts id in
  73          X.xml_nempty "PROD" ["id",id ; "type",ty]
  74           [< X.xml_nempty "source" [] (aux s) ;
  75              X.xml_nempty "target" [] (aux t)
  76           >]
  77      | C.AProd (xid,C.Name id,s,t) ->
  78         let ty = Hashtbl.find ids_to_inner_sorts xid in
  79          X.xml_nempty "PROD" ["id",xid ; "type",ty]
  80           [< X.xml_nempty "source" [] (aux s) ;
  81              X.xml_nempty "target" ["binder",id] (aux t)
  82           >]
  83      | C.ACast (id,v,t) ->
  84         let sort = Hashtbl.find ids_to_inner_sorts id in
  85          X.xml_nempty "CAST" ["id",id ; "sort",sort]
  86           [< X.xml_nempty "term" [] (aux v) ;
  87              X.xml_nempty "type" [] (aux t)
  88           >]
  89      | C.ALambda (id,C.Anonimous,s,t) ->
  90         let sort = Hashtbl.find ids_to_inner_sorts id in
  91          X.xml_nempty "LAMBDA" ["id",id ; "sort",sort]
  92           [< X.xml_nempty "source" [] (aux s) ;
  93              X.xml_nempty "target" [] (aux t)
  94           >]
  95      | C.ALambda (xid,C.Name id,s,t) ->
  96         let sort = Hashtbl.find ids_to_inner_sorts xid in
  97          X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort]
  98           [< X.xml_nempty "source" [] (aux s) ;
  99              X.xml_nempty "target" ["binder",id] (aux t)
 100           >]
 101      | C.ALetIn (xid,C.Anonimous,s,t) ->
 102        assert false
 103      | C.ALetIn (xid,C.Name id,s,t) ->
 104         let sort = Hashtbl.find ids_to_inner_sorts xid in
 105          X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
 106           [< X.xml_nempty "term" [] (aux s) ;
 107              X.xml_nempty "letintarget" ["binder",id] (aux t)
 108           >]
 109      | C.AAppl (id,li) ->
 110         let sort = Hashtbl.find ids_to_inner_sorts id in
 111          X.xml_nempty "APPLY" ["id",id ; "sort",sort]
 112           [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
 113           >]
 114      | C.AConst (id,uri,_) ->
 115         let sort = Hashtbl.find ids_to_inner_sorts id in
 116          X.xml_empty "CONST"
 117           ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
 118      | C.AMutInd (id,uri,_,i) ->
 119         X.xml_empty "MUTIND"
 120          ["uri", (U.string_of_uri uri) ;
 121           "noType",(string_of_int i) ;
 122           "id",id]
 123      | C.AMutConstruct (id,uri,_,i,j) ->
 124         let sort = Hashtbl.find ids_to_inner_sorts id in
 125          X.xml_empty "MUTCONSTRUCT"
 126           ["uri", (U.string_of_uri uri) ;
 127            "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
 128            "id",id ; "sort",sort]
 129      | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
 130         let sort = Hashtbl.find ids_to_inner_sorts id in
 131          X.xml_nempty "MUTCASE"
 132           ["uriType",(U.string_of_uri uri) ;
 133            "noType", (string_of_int typeno) ;
 134            "id", id ; "sort",sort]
 135           [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
 136              X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
 137              List.fold_right
 138               (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
 139               patterns [<>]
 140           >]
 141      | C.AFix (id, no, funs) ->
 142         let sort = Hashtbl.find ids_to_inner_sorts id in
 143          X.xml_nempty "FIX"
 144           ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
 145           [< List.fold_right
 146               (fun (fi,ai,ti,bi) i ->
 147                 [< X.xml_nempty "FixFunction"
 148                     ["name", fi; "recIndex", (string_of_int ai)]
 149                     [< X.xml_nempty "type" [] [< aux ti >] ;
 150                        X.xml_nempty "body" [] [< aux bi >]
 151                     >] ;
 152                    i
 153                 >]
 154               ) funs [<>]
 155           >]
 156      | C.ACoFix (id,no,funs) ->
 157         let sort = Hashtbl.find ids_to_inner_sorts id in
 158          X.xml_nempty "COFIX"
 159           ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
 160           [< List.fold_right
 161               (fun (fi,ti,bi) i ->
 162                 [< X.xml_nempty "CofixFunction" ["name", fi]
 163                     [< X.xml_nempty "type" [] [< aux ti >] ;
 164                        X.xml_nempty "body" [] [< aux bi >]
 165                     >] ;
 166                    i
 167                 >]
 168               ) funs [<>]
 169           >]
 170  in
 171   aux
 172 ;;
 173
 174 exception NotImplemented;;
 175
 176 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
 177 let print_object curi ~ids_to_inner_sorts =
 178  let rec aux =
 179   let module C = Cic in
 180   let module X = Xml in
 181   let module U = UriManager in
 182     function
 183        C.ACurrentProof (id,n,conjectures,bo,ty) ->
 184         X.xml_nempty "CurrentProof" ["name",n ; "id", id]
 185          [< List.fold_left
 186              (fun i (cid,n,canonical_context,t) ->
 187                [< i ;
 188                   X.xml_nempty "Conjecture"
 189                    ["id", cid ; "no",(string_of_int n)]
 190                    [< List.fold_left
 191                        (fun i (hid,t) ->
 192                          [< (match t with
 193                                Some (n,C.ADecl t) ->
 194                                 X.xml_nempty "Decl"
 195                                  (match n with
 196                                      C.Name n' -> ["id",hid;"name",n']
 197                                    | C.Anonimous -> ["id",hid])
 198                                  (print_term curi ids_to_inner_sorts t)
 199                              | Some (n,C.ADef t) ->
 200                                 X.xml_nempty "Def"
 201                                  (match n with
 202                                      C.Name n' -> ["id",hid;"name",n']
 203                                    | C.Anonimous -> ["id",hid])
 204                                  (print_term curi ids_to_inner_sorts t)
 205                              | None -> X.xml_empty "Hidden" ["id",hid]
 206                             ) ;
 207                             i
 208                          >]
 209                        ) [< >] canonical_context ;
 210                       X.xml_nempty "Goal" []
 211                        (print_term curi ids_to_inner_sorts t)
 212                    >]
 213                >])
 214              [<>] conjectures ;
 215             X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
 216             X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty)  >]
 217      | C.ADefinition (id,n,bo,ty,C.Actual params) ->
 218         let params' =
 219          List.fold_right
 220           (fun (_,x) i ->
 221             List.fold_right
 222              (fun x i ->
 223                U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
 224              ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
 225           ) params ""
 226         in
 227          X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id]
 228           [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
 229              X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty)  >]
 230      | C.ADefinition _ -> assert false
 231      | _ -> raise NotImplemented
 232  in
 233   aux
 234 ;;
 235
 236 let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types =
 237  let module C2A = Cic2acic in
 238  let module X = Xml in
 239   X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
 240    (Hashtbl.fold
 241      (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
 242        [< x ;
 243           X.xml_nempty "TYPE" ["of",id]
 244            [< print_term curi ids_to_inner_sorts synty ;
 245               match expty with
 246                  None -> [<>]
 247                | Some expty' -> print_term curi ids_to_inner_sorts expty'
 248            >]
 249        >]
 250      ) ids_to_inner_types [<>]
 251    )
 252 ;;