- Utilisation d'abbréviations pour les types intervenant dans RCases

- Factorisation du procédé de transformation Cases -> RCases dans Detyping
- Rebranchement de la traduction XML pour Cases (interrompue depuis
  suppression traducteur)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8741 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 24 insertions, 9 deletions

diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 8b3661dbe6..23fdfdaa29 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -19,6 +19,7 @@ open Tacexpr
 open Libnames
 
 open Nametab
+open Detyping
 
 (* Generic xml parser without raw data *)
 
@@ -95,7 +96,9 @@ let sort_of_cdata (loc,a) = match a with
 
 let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
 
-let get_xml_inductive_kn al = inductive_of_cdata (get_xml_attr "uri" al)
+let get_xml_inductive_kn al =
+  inductive_of_cdata (* uriType apparent synonym of uri *)
+    (try get_xml_attr "uri" al with _ -> get_xml_attr "uriType" al)
 
 let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
 
@@ -113,6 +116,16 @@ let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al)
 
 let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al)
 
+(* A leak in the xml dtd: arities of constructor need to know global env *)
+
+let compute_branches_lengths ind =
+  let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+  mip.Declarations.mind_consnrealdecls
+
+let compute_predicate_length ind =
+  let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+  mip.Declarations.mind_nrealargs
+
 (* Interpreting constr as a rawconstr *)
 
 let rec interp_xml_constr = function
@@ -134,14 +147,16 @@ let rec interp_xml_constr = function
       failwith "META: TODO"
   | XmlTag (loc,"CONST",al,[]) ->
       RRef (loc, ConstRef (get_xml_constant al))
-  | XmlTag (loc,"MUTCASE",al,x::y::yl) -> (* BUGGE *)
-      failwith "XML MUTCASE TO DO";
-(*
-      ROrderedCase (loc,RegularStyle,Some (interp_xml_patternsType x),
-      interp_xml_inductiveTerm y,
-      Array.of_list (List.map interp_xml_pattern yl),
-      ref None)
-*)
+  | XmlTag (loc,"MUTCASE",al,x::y::yl) ->
+      let ind = get_xml_inductive al in
+      let p = interp_xml_patternsType x in
+      let tm = interp_xml_inductiveTerm y in
+      let brs = List.map interp_xml_pattern yl in
+      let brns = Array.to_list (compute_branches_lengths ind) in
+      let mat = simple_cases_matrix_of_branches ind brns brs in
+      let n = compute_predicate_length ind in
+      let nal,rtn = return_type_of_predicate ind n p in
+      RCases (loc,rtn,[tm,nal],mat)
   | XmlTag (loc,"MUTIND",al,[]) ->
       RRef (loc, IndRef (get_xml_inductive al))
   | XmlTag (loc,"MUTCONSTRUCT",al,[]) ->