updates the structure of fix (struct argument added) and if

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

3 files changed, 34 insertions, 20 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 4647c0c8b..3b45f86a5 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -218,7 +218,7 @@ and ct_FIX_BINDER =
 and ct_FIX_BINDER_LIST =
     CT_fix_binder_list of ct_FIX_BINDER * ct_FIX_BINDER list
 and ct_FIX_REC =
-    CT_fix_rec of ct_ID * ct_BINDER_NE_LIST * ct_FORMULA * ct_FORMULA
+    CT_fix_rec of ct_ID * ct_BINDER_NE_LIST * ct_ID_OPT * ct_FORMULA * ct_FORMULA
 and ct_FIX_REC_LIST =
     CT_fix_rec_list of ct_FIX_REC * ct_FIX_REC list
 and ct_FIX_TAC_LIST =
@@ -237,7 +237,7 @@ and ct_FORMULA =
   | CT_elimc of ct_CASE * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA_LIST
   | CT_existvarc
   | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
-  | CT_if of ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA * ct_FORMULA
+  | CT_if of ct_FORMULA * ct_ID_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
   | CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
   | CT_let_tuple of ct_ID_OPT_NE_LIST * ct_ID_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 296061c1f..f04c4beaf 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -555,12 +555,13 @@ and fFIX_BINDER_LIST = function
    (List.iter fFIX_BINDER l);
    fNODE "fix_binder_list" (1 + (List.length l))
 and fFIX_REC = function
-| CT_fix_rec(x1, x2, x3, x4) ->
+| CT_fix_rec(x1, x2, x3, x4, x5) ->
    fID x1;
    fBINDER_NE_LIST x2;
-   fFORMULA x3;
+   fID_OPT x3;
    fFORMULA x4;
-   fNODE "fix_rec" 4
+   fFORMULA x5;
+   fNODE "fix_rec" 5
 and fFIX_REC_LIST = function
 | CT_fix_rec_list(x,l) ->
    fFIX_REC x;
@@ -608,12 +609,13 @@ and fFORMULA = function
    fID x1;
    fFIX_BINDER_LIST x2;
    fNODE "fixc" 2
-| CT_if(x1, x2, x3, x4) ->
-   fFORMULA_OPT x1;
-   fFORMULA x2;
-   fFORMULA x3;
+| CT_if(x1, x2, x3, x4, x5) ->
+   fFORMULA x1;
+   fID_OPT x2;
+   fFORMULA_OPT x3;
    fFORMULA x4;
-   fNODE "if" 4
+   fFORMULA x5;
+   fNODE "if" 5
 | CT_inductive_let(x1, x2, x3, x4) ->
    fFORMULA_OPT x1;
    fID_OPT_NE_LIST x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 9d81b2fd2..a11d75d4d 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -291,6 +291,14 @@ let rec decompose_last = function
   | [a] -> [], a
   | a::tl -> let rl, b = decompose_last tl in (a::rl), b;;
 
+let rec make_fix_struct b = function
+    0, CProdN(_, [([na],_)], CProdN(_, _,_)) -> xlate_id_opt na
+  | 0, CProdN(_, [([na],_)], _) ->
+      if b then xlate_id_opt na else ctv_ID_OPT_NONE
+  | n, CProdN(_, [([_],_)],body) -> make_fix_struct true ((n-1),body)
+  | _, _ -> xlate_error "unexpected result of parsing for Fixpoint";;
+
+
 let rec xlate_binder = function
     (l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
 and xlate_formula_opt =
@@ -360,8 +368,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		xlate_formula_opt ret_type,
                 CT_eqn_list (List.map (fun x -> translate_one_equation x) eqns))
    | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> 
-		   CT_if(xlate_formula_opt po,
-                   xlate_formula c,xlate_formula b1,xlate_formula b2)		
+       xlate_error "No more COrderedCase"
    | CLetTuple (_,a::l, (na,po), c, b) -> 
       CT_let_tuple(CT_id_opt_ne_list(xlate_id_opt_aux a,
 				     List.map xlate_id_opt_aux l),
@@ -370,10 +377,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		   xlate_formula c,
 		   xlate_formula b)
    | CLetTuple (_, [], _, _, _) -> xlate_error "NOT parsed: Let with ()"
-   | CIf (_,c, (na,None), b1, b2) ->
-		   CT_if(ctv_FORMULA_OPT_NONE,
-                   xlate_formula c,xlate_formula b1,xlate_formula b2)
-   | CIf (_,c, (na,Some p), b1, b2) -> xlate_error "If: TODO"
+   | CIf (_,c, (na, p), b1, b2) -> 
+       CT_if
+	 (xlate_formula c, xlate_id_opt_aux na, xlate_formula_opt p,
+	  xlate_formula b1, xlate_formula b2)
 
    | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
        CT_inductive_let(xlate_formula_opt po,
@@ -409,13 +416,14 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
    | CFix (_, (_, id), lm::lmi) ->       
      let strip_mutrec (fid, n, arf, ardef) =
+       let struct_arg = make_fix_struct false (n, arf) in
         let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match cvt_fixpoint_binders bl with
 	  | CT_binder_list (b :: bl) ->
 	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
-                arf, ardef)
+			  struct_arg, arf, ardef)
           | _ -> xlate_error "mutual recursive" in
        CT_fixc (xlate_ident id, 
          	CT_fix_binder_list
@@ -1640,14 +1648,18 @@ let xlate_vernac =
    | VernacFixpoint [] -> xlate_error "mutual recursive"
    | VernacFixpoint (lm :: lmi) ->
       let strip_mutrec ((fid, n, arf, ardef), ntn) =
-	(* TODO: handle ntn in mutual recursive *)
+(* The boolean argument should be false if a name is not really necessary, 
+   for instance if there is only one argument.  On the other hand, all
+   recursive calls in this function should have the boolean argument to true,
+   because recursive calls mean that there is more than one argument. *)
+	let struct_arg = make_fix_struct false (n, arf) in
         let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match cvt_fixpoint_binders bl with
 	  | CT_binder_list (b :: bl) ->
-	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
-                arf, ardef)
+	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl), 
+			  struct_arg, arf, ardef)
           | _ -> xlate_error "mutual recursive" in
         CT_fix_decl
 	  (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))