helm/interface/cic2Xml.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=cic.dtd";;
   8
   9 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
  10 let print_term curi =
  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,_,n,Some b) ->
  17         X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
  18      | C.ARel _ -> raise BinderNotSpecified
  19      | C.AVar (id,_,uri) ->
  20         let vdepth = U.depth_of_uri uri
  21         and cdepth = U.depth_of_uri curi in
  22          X.xml_empty "VAR"
  23           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
  24             (U.name_of_uri uri) ;
  25            "id",id]
  26      | C.AMeta (id,_,n) ->
  27         X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
  28      | C.ASort (id,_,s) ->
  29         let string_of_sort =
  30          function
  31             C.Prop -> "Prop"
  32           | C.Set  -> "Set"
  33           | C.Type -> "Type"
  34         in
  35          X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
  36      | C.AImplicit _ -> raise NotImplemented
  37      | C.AProd (id,_,C.Anonimous,s,t) ->
  38         X.xml_nempty "PROD" ["id",id]
  39          [< X.xml_nempty "source" [] (aux s) ;
  40             X.xml_nempty "target" [] (aux t)
  41          >]
  42      | C.AProd (xid,_,C.Name id,s,t) ->
  43        X.xml_nempty "PROD" ["id",xid]
  44         [< X.xml_nempty "source" [] (aux s) ;
  45            X.xml_nempty "target" ["binder",id] (aux t)
  46         >]
  47      | C.ACast (id,_,v,t) ->
  48         X.xml_nempty "CAST" ["id",id]
  49          [< X.xml_nempty "term" [] (aux v) ;
  50             X.xml_nempty "type" [] (aux t)
  51          >]
  52      | C.ALambda (id,_,C.Anonimous,s,t) ->
  53         X.xml_nempty "LAMBDA" ["id",id]
  54          [< X.xml_nempty "source" [] (aux s) ;
  55             X.xml_nempty "target" [] (aux t)
  56          >]
  57      | C.ALambda (xid,_,C.Name id,s,t) ->
  58        X.xml_nempty "LAMBDA" ["id",xid]
  59         [< X.xml_nempty "source" [] (aux s) ;
  60            X.xml_nempty "target" ["binder",id] (aux t)
  61         >]
  62      | C.AAppl (id,_,li) ->
  63         X.xml_nempty "APPLY" ["id",id]
  64          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
  65          >]
  66      | C.AConst (id,_,uri,_) ->
  67         X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
  68      | C.AAbst (id,_,uri) -> raise NotImplemented
  69      | C.AMutInd (id,_,uri,_,i) ->
  70         X.xml_empty "MUTIND"
  71          ["uri", (U.string_of_uri uri) ;
  72           "noType",(string_of_int i) ;
  73           "id",id]
  74      | C.AMutConstruct (id,_,uri,_,i,j) ->
  75         X.xml_empty "MUTCONSTRUCT"
  76          ["uri", (U.string_of_uri uri) ;
  77           "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
  78           "id",id]
  79      | C.AMutCase (id,_,uri,_,typeno,ty,te,patterns) ->
  80         X.xml_nempty "MUTCASE"
  81          ["uriType",(U.string_of_uri uri) ;
  82           "noType", (string_of_int typeno) ;
  83           "id", id]
  84          [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
  85             X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
  86             List.fold_right
  87              (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
  88              patterns [<>]
  89          >]
  90      | C.AFix (id, _, no, funs) ->
  91        X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
  92         [< List.fold_right
  93             (fun (fi,ai,ti,bi) i ->
  94               [< X.xml_nempty "FixFunction"
  95                   ["name", fi; "recIndex", (string_of_int ai)]
  96                   [< X.xml_nempty "type" [] [< aux ti >] ;
  97                      X.xml_nempty "body" [] [< aux bi >]
  98                   >] ;
  99                  i
 100               >]
 101             ) funs [<>]
 102         >]
 103      | C.ACoFix (id,_,no,funs) ->
 104        X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
 105         [< List.fold_right
 106             (fun (fi,ti,bi) i ->
 107               [< X.xml_nempty "CofixFunction" ["name", fi]
 108                   [< X.xml_nempty "type" [] [< aux ti >] ;
 109                      X.xml_nempty "body" [] [< aux bi >]
 110                   >] ;
 111                  i
 112               >]
 113             ) funs [<>]
 114         >]
 115  in
 116   aux
 117 ;;
 118
 119 let encode params =
 120  List.fold_right
 121   (fun (n,l) i ->
 122     match l with
 123        [] -> i
 124      | _ ->
 125        string_of_int n ^ ": " ^
 126        String.concat " " (List.map UriManager.name_of_uri l) ^
 127        i
 128   ) params ""
 129 ;;
 130
 131 let print_mutual_inductive_type curi (typename,inductive,arity,constructors) =
 132  let module C = Cic in
 133  let module X = Xml in
 134   [< X.xml_nempty "InductiveType"
 135       ["name",typename ;
 136        "inductive",(string_of_bool inductive)
 137       ]
 138       [< X.xml_nempty "arity" [] (print_term curi arity) ;
 139          (List.fold_right
 140           (fun (name,ty,_) i ->
 141             [< X.xml_nempty "Constructor" ["name",name]
 142                 (print_term curi ty) ;
 143                i
 144             >])
 145           constructors
 146           [<>]
 147          )
 148       >]
 149   >]
 150 ;;
 151
 152 let pp obj curi =
 153  let module C = Cic in
 154  let module X = Xml in
 155   match obj with
 156      C.ADefinition (xid, _, id, te, ty, params) ->
 157       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 158          X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 159          X.xml_nempty "Definition"
 160           (["name", id ; "id",xid] @
 161            match params with
 162               C.Possible _ -> raise ImpossiblePossible
 163               (*CSC params are kept in inverted order in the internal *)
 164               (* representation (the order of application)            *)
 165             | C.Actual fv' -> ["params",(encode (List.rev fv'))])
 166           [< X.xml_nempty "body" [] (print_term curi te) ;
 167              X.xml_nempty "type"  [] (print_term curi ty) >]
 168       >]
 169    | C.AAxiom (xid, _, id, ty, params) ->
 170       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 171          X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 172          X.xml_nempty "Axiom"
 173           (*CSC params are kept in inverted order in the internal *)
 174           (* representation (the order of application)            *)
 175           ["name",id ; "params",(encode (List.rev params)) ; "id",xid]
 176           [< X.xml_nempty "type" [] (print_term curi ty) >]
 177       >]
 178    | C.AVariable (xid, _, name, ty) ->
 179       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 180          X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 181          X.xml_nempty "Variable" ["name",name ; "id",xid]
 182           [< X.xml_nempty "type" [] (print_term curi ty) >]
 183       >]
 184    | C.ACurrentProof (xid, _, name, conjs, bo, ty) ->
 185       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 186          X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n");
 187          X.xml_nempty "CurrentProof" ["name",name ; "id",xid]
 188           [< List.fold_right
 189               (fun (j,t) i ->
 190                 [< X.xml_nempty "Conjecture" ["no",(string_of_int j)]
 191                     [< print_term curi t >] ; i >])
 192               conjs [<>] ;
 193              X.xml_nempty "body" [] [< print_term curi bo >] ;
 194              X.xml_nempty "type" [] [< print_term curi ty >]
 195           >]
 196       >]
 197    | C.AInductiveDefinition (xid, _, tys, params, paramsno) ->
 198       let names =
 199        List.map
 200         (fun (typename,_,_,_) -> typename)
 201         tys
 202       in
 203        [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 204           X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
 205            dtdname ^ "\">\n\n") ;
 206           X.xml_nempty "InductiveDefinition"
 207            (*CSC params are kept in inverted order in the internal *)
 208            (* representation (the order of application)            *)
 209            ["noParams",string_of_int paramsno ;
 210             "params",(encode (List.rev params)) ;
 211             "id",xid]
 212           [< List.fold_right
 213               (fun x i -> [< print_mutual_inductive_type curi x ; i >])
 214               tys [< >]
 215            >]
 216        >]
 217 ;;