We do not longer generate inner-types and inner-sorts for XML files generated

[helm.git] / helm / ocaml / cic / cicParser.ml

diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml
index 4b7c940e9ceb9d133448e3d82e3b72cd12fb2fb5..887ed975f74f00a5ffff420e9f46eb201042a15d 100644 (file)
--- a/helm/ocaml/cic/cicParser.ml
+++ b/helm/ocaml/cic/cicParser.ml
@@ -349,6 +349,7 @@ let end_element ctxt tag =
   | "REL" ->
       push ctxt (Cic_term
         (match pop_tag_attrs ctxt with
+        | ["binder", binder; "id", id; "idref", idref; "value", value]
         | ["binder", binder; "id", id; "idref", idref; "sort", _;
            "value", value] ->
             Cic.ARel (id, idref, int_of_string value, binder)
@@ -356,12 +357,14 @@ let end_element ctxt tag =
   | "VAR" ->
       push ctxt (Cic_term
         (match pop_tag_attrs ctxt with
+        | ["id", id; "uri", uri]
         | ["id", id; "sort", _; "uri", uri] ->
             Cic.AVar (id, uri_of_string uri, [])
         | _ -> attribute_error ()))
   | "CONST" ->
       push ctxt (Cic_term
         (match pop_tag_attrs ctxt with
+        | ["id", id; "uri", uri]
         | ["id", id; "sort", _; "uri", uri] ->
             Cic.AConst (id, uri_of_string uri, [])
         | _ -> attribute_error ()))
@@ -374,22 +377,27 @@ let end_element ctxt tag =
       let args = pop_cics ctxt in
       push ctxt (Cic_term
         (match pop_tag_attrs ctxt with
+        | ["id", id ]
         | ["id", id; "sort", _] -> Cic.AAppl (id, args)
         | _ -> attribute_error ()))
   | "decl" ->
       let source = pop_cic ctxt in
       push ctxt
         (match pop_tag_attrs ctxt with
+        | ["binder", binder; "id", id ]
         | ["binder", binder; "id", id; "type", _] ->
             Decl (id, Cic.Name binder, source)
+        | ["id", id]
         | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
         | _ -> attribute_error ())
   | "def" ->  (* same as "decl" above *)
       let source = pop_cic ctxt in
       push ctxt
         (match pop_tag_attrs ctxt with
+        | ["binder", binder; "id", id]
         | ["binder", binder; "id", id; "sort", _] ->
             Def (id, Cic.Name binder, source)
+        | ["id", id]
         | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
         | _ -> attribute_error ())
   | "arity"           (* transparent elements (i.e. which contain a CIC) *)
@@ -422,6 +430,7 @@ let end_element ctxt tag =
       in
       let term = add_decl target ctxt.stack in
       (match pop_tag_attrs ctxt with
+        []
       | ["type", _] -> ()
       | _ -> attribute_error ());
       push ctxt (Cic_term term)
@@ -436,6 +445,7 @@ let end_element ctxt tag =
       in
       let term = add_decl target ctxt.stack in
       (match pop_tag_attrs ctxt with
+        []
       | ["sort", _] -> ()
       | _ -> attribute_error ());
       push ctxt (Cic_term term)
@@ -450,6 +460,7 @@ let end_element ctxt tag =
       in
       let term = add_def target ctxt.stack in
       (match pop_tag_attrs ctxt with
+        []
       | ["sort", _] -> ()
       | _ -> attribute_error ());
       push ctxt (Cic_term term)
@@ -458,6 +469,7 @@ let end_element ctxt tag =
       let term = pop_cic ctxt in
       push ctxt (Cic_term
         (match pop_tag_attrs ctxt with
+          ["id", id]
         | ["id", id; "sort", _] -> Cic.ACast (id, term, typ)
         | _ -> attribute_error ()));
   | "IMPLICIT" ->
@@ -478,6 +490,7 @@ let end_element ctxt tag =
       let meta_substs = pop_meta_substs ctxt in
       push ctxt (Cic_term
         (match pop_tag_attrs ctxt with
+        | ["id", id; "no", no]
         | ["id", id; "no", no; "sort", _] ->
             Cic.AMeta (id, int_of_string no, meta_substs)
         | _ -> attribute_error ()));
@@ -490,6 +503,7 @@ let end_element ctxt tag =
   | "MUTCONSTRUCT" ->
       push ctxt (Cic_term
         (match pop_tag_attrs ctxt with
+        | ["id", id; "noConstr", noConstr; "noType", noType; "uri", uri]
         | ["id", id; "noConstr", noConstr; "noType", noType; "sort", _;
            "uri", uri] ->
             Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType,
@@ -515,6 +529,7 @@ let end_element ctxt tag =
       let fix_funs = pop_fix_funs ctxt in
       push ctxt (Cic_term
         (match pop_tag_attrs ctxt with
+        | ["id", id; "noFun", noFun]
         | ["id", id; "noFun", noFun; "sort", _] ->
             Cic.AFix (id, int_of_string noFun, fix_funs)
         | _ -> attribute_error ()))
@@ -522,6 +537,7 @@ let end_element ctxt tag =
       let cofix_funs = pop_cofix_funs ctxt in
       push ctxt (Cic_term
         (match pop_tag_attrs ctxt with
+        | ["id", id; "noFun", noFun]
         | ["id", id; "noFun", noFun; "sort", _] ->
             Cic.ACoFix (id, int_of_string noFun, cofix_funs)
         | _ -> attribute_error ()))
@@ -530,6 +546,7 @@ let end_element ctxt tag =
       | patternsType :: inductiveTerm :: patterns ->
           push ctxt (Cic_term
             (match pop_tag_attrs ctxt with
+            | ["id", id; "noType", noType; "uriType", uriType]
             | ["id", id; "noType", noType; "sort", _; "uriType", uriType] ->
                 Cic.AMutCase (id, uri_of_string uriType, int_of_string noType,
                   patternsType, inductiveTerm, patterns)