X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2Xml.ml;h=564493cb83e9d9d2ae42908e3970b21fbb5107be;hb=70f855932359e26ca89deb11c22f9c9d26154827;hp=f04df2f2f6bf4cce1e4b0f376723920dd9f76058;hpb=ee35bf33520d92753899985329cc4bfee141b808;p=helm.git

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index f04df2f2f..564493cb8 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -1,4 +1,3 @@
-
 (* Copyright (C) 2000, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
@@ -28,27 +27,35 @@
 
 exception ImpossiblePossible;;
 exception NotImplemented;;
-let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
+
+let dtdname ~ask_dtd_to_the_getter dtd =
+ if ask_dtd_to_the_getter then
+  Configuration.getter_url ^ "getdtd?uri=" ^ dtd
+ else
+  "http://mowgli.cs.unibo.it/dtd/" ^ dtd
+;;
+
+let param_attribute_of_params params =
+ String.concat " " (List.map UriManager.string_of_uri params)
+;;
 
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term curi ids_to_inner_sorts =
+let print_term ~ids_to_inner_sorts =
  let rec aux =
   let module C = Cic in
   let module X = Xml in
   let module U = UriManager in
     function
-       C.ARel (id,n,b) ->
+       C.ARel (id,idref,n,b) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
          X.xml_empty "REL"
-          ["value",(string_of_int n) ; "binder",b ; "id",id ; "sort",sort]
-     | C.AVar (id,uri) ->
-        let vdepth = U.depth_of_uri uri
-        and cdepth = U.depth_of_uri curi
-        and sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_empty "VAR"
-          ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
-            (U.name_of_uri uri) ;
-           "id",id ; "sort",sort]
+          ["value",(string_of_int n) ; "binder",b ; "id",id ; "idref",idref ;
+           "sort",sort]
+     | C.AVar (id,uri,exp_named_subst) ->
+        let sort = Hashtbl.find ids_to_inner_sorts id in
+         aux_subst uri
+          (X.xml_empty "VAR" ["uri",U.string_of_uri uri;"id",id;"sort",sort])
+          exp_named_subst
      | C.AMeta (id,n,l) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
          X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
@@ -69,66 +76,117 @@ let print_term curi ids_to_inner_sorts =
         in
          X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
      | C.AImplicit _ -> raise NotImplemented
-     | C.AProd (id,C.Anonimous,s,t) ->
-        let ty = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "PROD" ["id",id ; "type",ty]
-          [< X.xml_nempty "source" [] (aux s) ;
-             X.xml_nempty "target" [] (aux t)
-          >]
-     | C.AProd (xid,C.Name id,s,t) ->
-        let ty = Hashtbl.find ids_to_inner_sorts xid in
-         X.xml_nempty "PROD" ["id",xid ; "type",ty]
-          [< X.xml_nempty "source" [] (aux s) ;
-             X.xml_nempty "target" ["binder",id] (aux t)
-          >]
+     | C.AProd (last_id,_,_,_) as prods ->
+        let rec eat_prods =
+         function
+            C.AProd (id,n,s,t) ->
+             let prods,t' = eat_prods t in
+              (id,n,s)::prods,t'
+          | t -> [],t
+        in
+         let prods,t = eat_prods prods in
+          let sort = Hashtbl.find ids_to_inner_sorts last_id in
+           X.xml_nempty "PROD" ["type",sort]
+            [< List.fold_left
+                (fun i (id,binder,s) ->
+                  let sort =
+                   Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
+                  in
+                   let attrs =
+                    ("id",id)::("type",sort)::
+                    match binder with
+                       C.Anonymous -> []
+                     | C.Name b -> ["binder",b]
+                   in
+                    [< i ; X.xml_nempty "decl" attrs (aux s) >]
+                ) [< >] prods ;
+               X.xml_nempty "target" [] (aux t)
+            >]
      | C.ACast (id,v,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
          X.xml_nempty "CAST" ["id",id ; "sort",sort]
           [< X.xml_nempty "term" [] (aux v) ;
              X.xml_nempty "type" [] (aux t)
           >]
-     | C.ALambda (id,C.Anonimous,s,t) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "LAMBDA" ["id",id ; "sort",sort]
-          [< X.xml_nempty "source" [] (aux s) ;
-             X.xml_nempty "target" [] (aux t)
-          >]
-     | C.ALambda (xid,C.Name id,s,t) ->
-        let sort = Hashtbl.find ids_to_inner_sorts xid in
-         X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort]
-          [< X.xml_nempty "source" [] (aux s) ;
-             X.xml_nempty "target" ["binder",id] (aux t)
-          >]
-     | C.ALetIn (xid,C.Anonimous,s,t) ->
+     | C.ALambda (last_id,_,_,_) as lambdas ->
+        let rec eat_lambdas =
+         function
+            C.ALambda (id,n,s,t) ->
+             let lambdas,t' = eat_lambdas t in
+              (id,n,s)::lambdas,t'
+          | t -> [],t
+        in
+         let lambdas,t = eat_lambdas lambdas in
+          let sort = Hashtbl.find ids_to_inner_sorts last_id in
+           X.xml_nempty "LAMBDA" ["sort",sort]
+            [< List.fold_left
+                (fun i (id,binder,s) ->
+                  let sort =
+                   Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
+                  in
+                   let attrs =
+                    ("id",id)::("type",sort)::
+                    match binder with
+                       C.Anonymous -> []
+                     | C.Name b -> ["binder",b]
+                   in
+                    [< i ; X.xml_nempty "decl" attrs (aux s) >]
+                ) [< >] lambdas ;
+               X.xml_nempty "target" [] (aux t)
+            >]
+     | C.ALetIn (xid,C.Anonymous,s,t) ->
        assert false
-     | C.ALetIn (xid,C.Name id,s,t) ->
-        let sort = Hashtbl.find ids_to_inner_sorts xid in
-         X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
-          [< X.xml_nempty "term" [] (aux s) ;
-             X.xml_nempty "letintarget" ["binder",id] (aux t)
-          >]
+     | C.ALetIn (last_id,C.Name _,_,_) as letins ->
+        let rec eat_letins =
+         function
+            C.ALetIn (id,n,s,t) ->
+             let letins,t' = eat_letins t in
+              (id,n,s)::letins,t'
+          | t -> [],t
+        in
+         let letins,t = eat_letins letins in
+          let sort = Hashtbl.find ids_to_inner_sorts last_id in
+           X.xml_nempty "LETIN" ["sort",sort]
+            [< List.fold_left
+                (fun i (id,binder,s) ->
+                  let sort = Hashtbl.find ids_to_inner_sorts id in
+                   let attrs =
+                    ("id",id)::("sort",sort)::
+                    match binder with
+                       C.Anonymous -> []
+                     | C.Name b -> ["binder",b]
+                   in
+                    [< i ; X.xml_nempty "def" attrs (aux s) >]
+                ) [< >] letins ;
+               X.xml_nempty "target" [] (aux t)
+            >]
      | C.AAppl (id,li) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
          X.xml_nempty "APPLY" ["id",id ; "sort",sort]
           [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
           >]
-     | C.AConst (id,uri,_) ->
+     | C.AConst (id,uri,exp_named_subst) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_empty "CONST"
-          ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
-     | C.AAbst (id,uri) -> raise NotImplemented
-     | C.AMutInd (id,uri,_,i) ->
-        X.xml_empty "MUTIND"
-         ["uri", (U.string_of_uri uri) ;
-          "noType",(string_of_int i) ;
-          "id",id]
-     | C.AMutConstruct (id,uri,_,i,j) ->
+         aux_subst uri
+          (X.xml_empty "CONST"
+            ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
+          ) exp_named_subst
+     | C.AMutInd (id,uri,i,exp_named_subst) ->
+        aux_subst uri
+         (X.xml_empty "MUTIND"
+           ["uri", (U.string_of_uri uri) ;
+            "noType",(string_of_int i) ;
+            "id",id]
+         ) exp_named_subst
+     | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_empty "MUTCONSTRUCT"
-          ["uri", (U.string_of_uri uri) ;
-           "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
-           "id",id ; "sort",sort]
-     | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
+         aux_subst uri
+          (X.xml_empty "MUTCONSTRUCT"
+            ["uri", (U.string_of_uri uri) ;
+             "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
+             "id",id ; "sort",sort]
+          ) exp_named_subst
+     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
          X.xml_nempty "MUTCASE"
           ["uriType",(U.string_of_uri uri) ;
@@ -145,9 +203,9 @@ let print_term curi ids_to_inner_sorts =
          X.xml_nempty "FIX"
           ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
           [< List.fold_right
-              (fun (fi,ai,ti,bi) i ->
+              (fun (id,fi,ai,ti,bi) i ->
                 [< X.xml_nempty "FixFunction"
-                    ["name", fi; "recIndex", (string_of_int ai)]
+                    ["id",id ; "name", fi ; "recIndex", (string_of_int ai)]
                     [< X.xml_nempty "type" [] [< aux ti >] ;
                        X.xml_nempty "body" [] [< aux bi >]
                     >] ;
@@ -160,8 +218,8 @@ let print_term curi ids_to_inner_sorts =
          X.xml_nempty "COFIX"
           ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
           [< List.fold_right
-              (fun (fi,ti,bi) i ->
-                [< X.xml_nempty "CofixFunction" ["name", fi]
+              (fun (id,fi,ti,bi) i ->
+                [< X.xml_nempty "CofixFunction" ["id",id ; "name", fi]
                     [< X.xml_nempty "type" [] [< aux ti >] ;
                        X.xml_nempty "body" [] [< aux bi >]
                     >] ;
@@ -169,80 +227,202 @@ let print_term curi ids_to_inner_sorts =
                 >]
               ) funs [<>]
           >]
- in
-  aux
+ and aux_subst buri target subst =
+(*CSC: I have now no way to assign an ID to the explicit named substitution *)
+  let id = None in
+   if subst = [] then
+    target
+   else
+    Xml.xml_nempty "instantiate"
+     (match id with None -> [] | Some id -> ["id",id])
+     [< target ;
+        List.fold_left
+         (fun i (uri,arg) ->
+           let relUri =
+            let buri_frags =
+             Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in
+            let uri_frags = 
+             Str.split (Str.regexp "/") (UriManager.string_of_uri uri)  in
+             let rec find_relUri buri_frags uri_frags =
+              match buri_frags,uri_frags with
+                 [_], _ -> String.concat "/" uri_frags
+               | he1::tl1, he2::tl2 ->
+                  assert (he1 = he2) ;
+                  find_relUri tl1 tl2
+               | _,_ -> assert false (* uri is not relative to buri *)
+             in
+              find_relUri buri_frags uri_frags
+           in
+            [< i ; Xml.xml_nempty "arg" ["relUri", relUri] (aux arg) >]
+         ) [<>] subst
+     >]
+  in
+   aux
 ;;
 
-exception NotImplemented;;
-
-(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_object curi ids_to_inner_sorts =
- let rec aux =
-  let module C = Cic in
-  let module X = Xml in
-  let module U = UriManager in
-    function
-       C.ACurrentProof (id,n,conjectures,bo,ty) ->
-        X.xml_nempty "CurrentProof" ["name",n ; "id", id]
-         [< List.fold_left
-             (fun i (n,canonical_context,t) ->
-               [< i ;
-                  X.xml_nempty "Conjecture" ["no",(string_of_int n)]
-                   [< List.fold_left
-                       (fun i t ->
-                         [< (match t with
-                               Some (n,C.ADecl t) ->
-                                X.xml_nempty "Decl"
-                                 (match n with
-                                     C.Name n' -> ["name",n']
-                                   | C.Anonimous -> [])
-                                 (print_term curi ids_to_inner_sorts t)
-                             | Some (n,C.ADef t) ->
-                                X.xml_nempty "Def"
-                                 (match n with
-                                     C.Name n' -> ["name",n']
-                                   | C.Anonimous -> [])
-                                 (print_term curi ids_to_inner_sorts t)
-                             | None -> X.xml_empty "Hidden" []
-                            ) ;
-                            i
-                         >]
-                       ) [< >] canonical_context ;
-                      X.xml_nempty "Goal" []
-                       (print_term curi ids_to_inner_sorts t)
-                   >]
-               >])
-             [<>] conjectures ;
-            X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
-            X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty)  >]
-     | C.ADefinition (id,n,bo,ty,C.Actual params) ->
-        let params' =
-         List.fold_right
-          (fun (_,x) i ->
-            List.fold_right
-             (fun x i ->
-               U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
-             ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
-          ) params ""
+let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
+ let module C = Cic in
+ let module X = Xml in
+ let module U = UriManager in
+  let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
+   match obj with
+       C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
+        let params' = param_attribute_of_params params in
+        let xml_for_current_proof_body =
+(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
+(*CSC: I think so. Not implemented yet.                                       *)
+         X.xml_nempty "CurrentProof"
+          ["of",UriManager.string_of_uri uri ; "id", id]
+          [< List.fold_left
+              (fun i (cid,n,canonical_context,t) ->
+                [< i ;
+                   X.xml_nempty "Conjecture"
+                    ["id", cid ; "no",(string_of_int n)]
+                    [< List.fold_left
+                        (fun i (hid,t) ->
+                          [< (match t with
+                                 Some (n,C.ADecl t) ->
+                                  X.xml_nempty "Decl"
+                                   (match n with
+                                       C.Name n' -> ["id",hid;"name",n']
+                                     | C.Anonymous -> ["id",hid])
+                                   (print_term ids_to_inner_sorts t)
+                               | Some (n,C.ADef t) ->
+                                  X.xml_nempty "Def"
+                                   (match n with
+                                       C.Name n' -> ["id",hid;"name",n']
+                                     | C.Anonymous -> ["id",hid])
+                                   (print_term ids_to_inner_sorts t)
+                              | None -> X.xml_empty "Hidden" ["id",hid]
+                             ) ;
+                             i
+                          >]
+                        ) [< >] canonical_context ;
+                       X.xml_nempty "Goal" []
+                        (print_term ids_to_inner_sorts t)
+                    >]
+                >])
+              [<>] conjectures ;
+             X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
+        in
+        let xml_for_current_proof_type =
+         X.xml_nempty "ConstantType" ["name",n ; "params",params' ; "id", id]
+          (print_term ids_to_inner_sorts ty)
+        in
+        let xmlbo =
+         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+            X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
+            xml_for_current_proof_body
+         >] in
+        let xmlty =
+         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
+            xml_for_current_proof_type
+         >]
+        in
+         xmlty, Some xmlbo
+     | C.AConstant (id,idbody,n,bo,ty,params) ->
+        let params' = param_attribute_of_params params in
+        let xmlbo =
+         match bo with
+            None -> None
+          | Some bo ->
+             Some
+              [< X.xml_cdata
+                  "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+                 X.xml_cdata
+                  ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
+                 X.xml_nempty "ConstantBody"
+                  ["for",UriManager.string_of_uri uri ; "params",params' ;
+                   "id", id]
+                  [< print_term ids_to_inner_sorts bo >]
+              >]
+        in
+        let xmlty =
+         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
+             X.xml_nempty "ConstantType"
+              ["name",n ; "params",params' ; "id", id]
+              [< print_term ids_to_inner_sorts ty >]
+         >]
+        in
+         xmlty, xmlbo
+     | C.AVariable (id,n,bo,ty,params) ->
+        let params' = param_attribute_of_params params in
+        let xmlbo =
+         match bo with
+            None -> [< >]
+          | Some bo ->
+             X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >]
+        in
+        let aobj =
+         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+            X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
+             X.xml_nempty "Variable"
+              ["name",n ; "params",params' ; "id", id]
+              [< xmlbo ;
+                 X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
+              >]
+         >]
         in
-         X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id]
-          [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
-             X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty)  >]
-     | C.ADefinition _ -> assert false
-     | _ -> raise NotImplemented
- in
-  aux
+         aobj, None
+     | C.AInductiveDefinition (id,tys,params,nparams) ->
+        let params' = param_attribute_of_params params in
+         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+            X.xml_cdata
+             ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
+            X.xml_nempty "InductiveDefinition"
+             ["noParams",string_of_int nparams ;
+              "id",id ;
+              "params",params']
+             [< (List.fold_left
+                  (fun i (id,typename,finite,arity,cons) ->
+                    [< i ;
+                       X.xml_nempty "InductiveType"
+                        ["id",id ; "name",typename ;
+                         "inductive",(string_of_bool finite)
+                        ]
+                        [< X.xml_nempty "arity" []
+                            (print_term ids_to_inner_sorts arity) ;
+                           (List.fold_left
+                            (fun i (name,lc) ->
+                              [< i ;
+                                 X.xml_nempty "Constructor"
+                                  ["name",name]
+                                  (print_term ids_to_inner_sorts lc)
+                              >]) [<>] cons
+                           )
+                        >]
+                    >]
+                  ) [< >] tys
+                )
+             >]
+         >], None
 ;;
 
-let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
+let
+ print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
+  ~ask_dtd_to_the_getter
+=
+ let module C2A = Cic2acic in
  let module X = Xml in
-  X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
-   (Hashtbl.fold
-     (fun id ty x ->
-       [< x ;
-          X.xml_nempty "TYPE" ["of",id]
-           (print_term curi ids_to_inner_sorts ty)
-       >]
-     ) ids_to_inner_types [<>]
-   )
+  let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
+   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+      X.xml_cdata
+       ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
+      X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
+       (Hashtbl.fold
+         (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
+           [< x ;
+              X.xml_nempty "TYPE" ["of",id]
+               [< X.xml_nempty "synthesized" []
+	         [< print_term ids_to_inner_sorts synty >] ;
+                 match expty with
+                   None -> [<>]
+                 | Some expty' -> X.xml_nempty "expected" [] [< print_term ids_to_inner_sorts expty' >]
+               >]
+           >]
+         ) ids_to_inner_types [<>]
+       )
+   >]
 ;;