helm/fix_params/cic2Xml.ml

   1
   2 (* Copyright (C) 2000, HELM Team.
   3  *
   4  * This file is part of HELM, an Hypertextual, Electronic
   5  * Library of Mathematics, developed at the Computer Science
   6  * Department, University of Bologna, Italy.
   7  *
   8  * HELM is free software; you can redistribute it and/or
   9  * modify it under the terms of the GNU General Public License
  10  * as published by the Free Software Foundation; either version 2
  11  * of the License, or (at your option) any later version.
  12  *
  13  * HELM is distributed in the hope that it will be useful,
  14  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  15  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  16  * GNU General Public License for more details.
  17  *
  18  * You should have received a copy of the GNU General Public License
  19  * along with HELM; if not, write to the Free Software
  20  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  21  * MA  02111-1307, USA.
  22  *
  23  * For details, see the HELM World-Wide-Web page,
  24  * http://cs.unibo.it/helm/.
  25  *)
  26
  27 (*CSC codice cut & paste da cicPp e xmlcommand *)
  28
  29 exception ImpossiblePossible;;
  30 exception NotImplemented;;
  31 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
  32
  33 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
  34 let print_term curi =
  35  let rec aux =
  36   let module C = Cic in
  37   let module X = Xml in
  38   let module U = UriManager in
  39     function
  40        C.ARel (id,n,b) ->
  41         X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
  42      | C.AVar (id,uri) ->
  43         let vdepth = U.depth_of_uri uri
  44         and cdepth = U.depth_of_uri curi in
  45          X.xml_empty "VAR"
  46           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
  47             (U.name_of_uri uri) ;
  48            "id",id]
  49      | C.AMeta (id,n) ->
  50         X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
  51      | C.ASort (id,s) ->
  52         let string_of_sort =
  53          function
  54             C.Prop -> "Prop"
  55           | C.Set  -> "Set"
  56           | C.Type -> "Type"
  57         in
  58          X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
  59      | C.AImplicit _ -> raise NotImplemented
  60      | C.AProd (id,C.Anonimous,s,t) ->
  61         X.xml_nempty "PROD" ["id",id]
  62          [< X.xml_nempty "source" [] (aux s) ;
  63             X.xml_nempty "target" [] (aux t)
  64          >]
  65      | C.AProd (xid,C.Name id,s,t) ->
  66        X.xml_nempty "PROD" ["id",xid]
  67         [< X.xml_nempty "source" [] (aux s) ;
  68            X.xml_nempty "target" ["binder",id] (aux t)
  69         >]
  70      | C.ACast (id,v,t) ->
  71         X.xml_nempty "CAST" ["id",id]
  72          [< X.xml_nempty "term" [] (aux v) ;
  73             X.xml_nempty "type" [] (aux t)
  74          >]
  75      | C.ALambda (id,C.Anonimous,s,t) ->
  76         X.xml_nempty "LAMBDA" ["id",id]
  77          [< X.xml_nempty "source" [] (aux s) ;
  78             X.xml_nempty "target" [] (aux t)
  79          >]
  80      | C.ALambda (xid,C.Name id,s,t) ->
  81        X.xml_nempty "LAMBDA" ["id",xid]
  82         [< X.xml_nempty "source" [] (aux s) ;
  83            X.xml_nempty "target" ["binder",id] (aux t)
  84         >]
  85      | C.ALetIn (xid,C.Anonimous,s,t) ->
  86        assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
  87      | C.ALetIn (xid,C.Name id,s,t) ->
  88        X.xml_nempty "LETIN" ["id",xid]
  89         [< X.xml_nempty "term" [] (aux s) ;
  90            X.xml_nempty "letintarget" ["binder",id] (aux t)
  91         >]
  92      | C.AAppl (id,li) ->
  93         X.xml_nempty "APPLY" ["id",id]
  94          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
  95          >]
  96      | C.AConst (id,uri,_) ->
  97         X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
  98      | C.AMutInd (id,uri,_,i) ->
  99         X.xml_empty "MUTIND"
 100          ["uri", (U.string_of_uri uri) ;
 101           "noType",(string_of_int i) ;
 102           "id",id]
 103      | C.AMutConstruct (id,uri,_,i,j) ->
 104         X.xml_empty "MUTCONSTRUCT"
 105          ["uri", (U.string_of_uri uri) ;
 106           "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
 107           "id",id]
 108      | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
 109         X.xml_nempty "MUTCASE"
 110          ["uriType",(U.string_of_uri uri) ;
 111           "noType", (string_of_int typeno) ;
 112           "id", id]
 113          [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
 114             X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
 115             List.fold_right
 116              (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
 117              patterns [<>]
 118          >]
 119      | C.AFix (id, no, funs) ->
 120        X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
 121         [< List.fold_right
 122             (fun (fi,ai,ti,bi) i ->
 123               [< X.xml_nempty "FixFunction"
 124                   ["name", fi; "recIndex", (string_of_int ai)]
 125                   [< X.xml_nempty "type" [] [< aux ti >] ;
 126                      X.xml_nempty "body" [] [< aux bi >]
 127                   >] ;
 128                  i
 129               >]
 130             ) funs [<>]
 131         >]
 132      | C.ACoFix (id,no,funs) ->
 133        X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
 134         [< List.fold_right
 135             (fun (fi,ti,bi) i ->
 136               [< X.xml_nempty "CofixFunction" ["name", fi]
 137                   [< X.xml_nempty "type" [] [< aux ti >] ;
 138                      X.xml_nempty "body" [] [< aux bi >]
 139                   >] ;
 140                  i
 141               >]
 142             ) funs [<>]
 143         >]
 144  in
 145   aux
 146 ;;
 147
 148 let encode params =
 149  List.fold_right
 150   (fun (n,l) i ->
 151     match l with
 152        [] -> i
 153      | _ ->
 154        string_of_int n ^ ": " ^
 155        String.concat " " (List.map UriManager.name_of_uri l) ^
 156        i
 157   ) params ""
 158 ;;
 159
 160 let print_mutual_inductive_type curi (typename,inductive,arity,constructors) =
 161  let module C = Cic in
 162  let module X = Xml in
 163   [< X.xml_nempty "InductiveType"
 164       ["name",typename ;
 165        "inductive",(string_of_bool inductive)
 166       ]
 167       [< X.xml_nempty "arity" [] (print_term curi arity) ;
 168          (List.fold_right
 169           (fun (name,ty,_) i ->
 170             [< X.xml_nempty "Constructor" ["name",name]
 171                 (print_term curi ty) ;
 172                i
 173             >])
 174           constructors
 175           [<>]
 176          )
 177       >]
 178   >]
 179 ;;
 180
 181 let pp obj curi =
 182  let module C = Cic in
 183  let module X = Xml in
 184   match obj with
 185      C.ADefinition (xid, id, te, ty, params) ->
 186       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 187          X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 188          X.xml_nempty "Definition"
 189           (["name", id ; "id",xid] @
 190            match params with
 191               C.Possible _ -> raise ImpossiblePossible
 192               (*CSC params are kept in inverted order in the internal *)
 193               (* representation (the order of application)            *)
 194             | C.Actual fv' -> ["params",(encode (List.rev fv'))])
 195           [< X.xml_nempty "body" [] (print_term curi te) ;
 196              X.xml_nempty "type"  [] (print_term curi ty) >]
 197       >]
 198    | C.AAxiom (xid, id, ty, params) ->
 199       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 200          X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 201          X.xml_nempty "Axiom"
 202           (*CSC params are kept in inverted order in the internal *)
 203           (* representation (the order of application)            *)
 204           ["name",id ; "params",(encode (List.rev params)) ; "id",xid]
 205           [< X.xml_nempty "type" [] (print_term curi ty) >]
 206       >]
 207    | C.AVariable (xid, name, bo, ty) ->
 208       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 209          X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 210          X.xml_nempty "Variable" ["name",name ; "id",xid]
 211           [< (match bo with
 212                  None -> [<>]
 213                | Some bo -> X.xml_nempty "body" [] (print_term curi bo)
 214              ) ;
 215              X.xml_nempty "type" [] (print_term curi ty)
 216           >]
 217       >]
 218    | C.ACurrentProof (xid, name, conjs, bo, ty) ->
 219       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 220          X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n");
 221          X.xml_nempty "CurrentProof" ["name",name ; "id",xid]
 222           [< List.fold_right
 223               (fun (j,t) i ->
 224                 [< X.xml_nempty "Conjecture" ["no",(string_of_int j)]
 225                     [< print_term curi t >] ; i >])
 226               conjs [<>] ;
 227              X.xml_nempty "body" [] [< print_term curi bo >] ;
 228              X.xml_nempty "type" [] [< print_term curi ty >]
 229           >]
 230       >]
 231    | C.AInductiveDefinition (xid, tys, params, paramsno) ->
 232       let names =
 233        List.map
 234         (fun (typename,_,_,_) -> typename)
 235         tys
 236       in
 237        [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 238           X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
 239            dtdname ^ "\">\n\n") ;
 240           X.xml_nempty "InductiveDefinition"
 241            (*CSC params are kept in inverted order in the internal *)
 242            (* representation (the order of application)            *)
 243            ["noParams",string_of_int paramsno ;
 244             "params",(encode (List.rev params)) ;
 245             "id",xid]
 246           [< List.fold_right
 247               (fun x i -> [< print_mutual_inductive_type curi x ; i >])
 248               tys [< >]
 249            >]
 250        >]
 251 ;;