parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic_acic / cic2Xml.ml

diff --git a/helm/software/components/cic_acic/cic2Xml.ml b/helm/software/components/cic_acic/cic2Xml.ml
index 31765f0552e8005d3c9168138a981026514dd38a..0708a839f49439ddb424e5201f2ce75272b44198 100644 (file)
--- a/helm/software/components/cic_acic/cic2Xml.ml
+++ b/helm/software/components/cic_acic/cic2Xml.ml
@@ -137,21 +137,21 @@ let print_term ?ids_to_inner_sorts =
                 ) [< >] lambdas ;
                X.xml_nempty "target" [] (aux t)
             >]
-     | C.ALetIn (xid,C.Anonymous,s,t) ->
+     | C.ALetIn (xid,C.Anonymous,s,ty,t) ->
        assert false
-     | C.ALetIn (last_id,C.Name _,_,_) as letins ->
+     | C.ALetIn (last_id,C.Name _,_,_,_) as letins ->
         let rec eat_letins =
          function
-            C.ALetIn (id,n,s,t) ->
+            C.ALetIn (id,n,s,ty,t) ->
              let letins,t' = eat_letins t in
-              (id,n,s)::letins,t'
+              (id,n,s,ty)::letins,t'
           | t -> [],t
         in
          let letins,t = eat_letins letins in
           let sort = find_sort "sort" last_id in
            X.xml_nempty "LETIN" sort
             [< List.fold_left
-                (fun i (id,binder,s) ->
+                (fun i (id,binder,s,ty) ->
                   let sort = find_sort "sort" id in
                    let attrs =
                     sort @ ((None,"id",id)::
@@ -159,7 +159,7 @@ let print_term ?ids_to_inner_sorts =
                         C.Anonymous -> []
                       | C.Name b -> [None,"binder",b])
                    in
-                    [< i ; X.xml_nempty "def" attrs (aux s) >]
+                    [< i ; X.xml_nempty "def" attrs [< aux s ; aux ty >] >]
                 ) [< >] letins ;
                X.xml_nempty "target" [] (aux t)
             >]
@@ -267,7 +267,7 @@ let print_term ?ids_to_inner_sorts =
    aux
 ;;
 
-let xml_of_attrs attributes =
+let xml_of_attrs generate_attributes attributes =
   let class_of = function
     | `Coercion n -> 
         Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
@@ -290,9 +290,12 @@ let xml_of_attrs attributes =
               res >]
            ) field_names [<>])
     | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
+    | `InversionPrinciple -> Xml.xml_empty "class" [None,"value","inversion"]
   in
   let flavour_of = function
     | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
+    | `MutualDefinition ->
+        Xml.xml_empty "flavour" [None, "value", "mutual_definition"]
     | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
     | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
     | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
@@ -309,9 +312,10 @@ let xml_of_attrs attributes =
    List.fold_right 
     (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
   in
-   Xml.xml_nempty "attributes" [] xml_attrs
+   if generate_attributes then Xml.xml_nempty "attributes" [] xml_attrs else [<>]
 
-let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
+let print_object uri 
+  ?ids_to_inner_sorts ?(generate_attributes=true) ~ask_dtd_to_the_getter obj =
  let module C = Cic in
  let module X = Xml in
  let module U = UriManager in
@@ -319,7 +323,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
    match obj with
        C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
         let params' = param_attribute_of_params params in
-        let xml_attrs = xml_of_attrs obj_attrs in
+        let xml_attrs = xml_of_attrs generate_attributes obj_attrs 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.                                       *)
@@ -341,7 +345,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
                                         [None,"id",hid;None,"name",n']
                                      | C.Anonymous -> [None,"id",hid])
                                    (print_term ?ids_to_inner_sorts t)
-                               | Some (n,C.ADef t) ->
+                               | Some (n,C.ADef (t,_)) ->
                                   X.xml_nempty "Def"
                                    (match n with
                                        C.Name n' ->
@@ -379,7 +383,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
          xmlty, Some xmlbo
      | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
         let params' = param_attribute_of_params params in
-        let xml_attrs = xml_of_attrs obj_attrs in
+        let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
         let xmlbo =
          match bo with
             None -> None
@@ -406,7 +410,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
          xmlty, xmlbo
      | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
         let params' = param_attribute_of_params params in
-        let xml_attrs = xml_of_attrs obj_attrs in
+        let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
         let xmlbo =
          match bo with
             None -> [< >]
@@ -426,7 +430,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
          aobj, None
      | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
         let params' = param_attribute_of_params params in
-        let xml_attrs = xml_of_attrs obj_attrs in
+        let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
             X.xml_cdata
              ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;