First very partial implementation of LetIn and bodyed Variables

[helm.git] / helm / interface / cic2Xml.ml

diff --git a/helm/interface/cic2Xml.ml b/helm/interface/cic2Xml.ml
index ff16e2f701f168deff3e8259ecbd6e8555c6c8d9..9f0cdef0666def33f3310d76e49bc7e08db344d7 100644 (file)
--- a/helm/interface/cic2Xml.ml
+++ b/helm/interface/cic2Xml.ml
@@ -59,6 +59,13 @@ let print_term curi =
         [< X.xml_nempty "source" [] (aux s) ;
            X.xml_nempty "target" ["binder",id] (aux t)
         >]
+     | C.ALetIn (xid,_,C.Anonimous,s,t) ->
+       assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
+     | C.ALetIn (xid,_,C.Name id,s,t) ->
+       X.xml_nempty "LETIN" ["id",xid]
+        [< X.xml_nempty "term" [] (aux s) ;
+           X.xml_nempty "letintarget" ["binder",id] (aux t)
+        >]
      | C.AAppl (id,_,li) ->
         X.xml_nempty "APPLY" ["id",id]
          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
@@ -175,11 +182,16 @@ let pp obj curi =
           ["name",id ; "params",(encode (List.rev params)) ; "id",xid]
           [< X.xml_nempty "type" [] (print_term curi ty) >]
       >]
-   | C.AVariable (xid, _, name, ty) ->
+   | C.AVariable (xid, _, name, bo, ty) ->
       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
          X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
          X.xml_nempty "Variable" ["name",name ; "id",xid]
-          [< X.xml_nempty "type" [] (print_term curi ty) >]
+          [< (match bo with
+                 None -> [<>]
+               | Some bo -> X.xml_nempty "body" [] (print_term curi bo)
+             ) ;
+             X.xml_nempty "type" [] (print_term curi ty)
+          >]
       >]
    | C.ACurrentProof (xid, _, name, conjs, bo, ty) ->
       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;