*** empty log message ***

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

3 files changed, 235 insertions, 60 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 14375e04ec..2d86e00c93 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -147,6 +147,9 @@ let pr_binder pr (nal,t) =
 let pr_binders pr bl =
   hv 0 (prlist_with_sep sep (pr_binder pr) bl)
 
+let pr_arg_binders pr bl =
+  if bl = [] then mt() else (spc() ++ pr_binders pr bl)
+
 let pr_global vars ref = pr_global_env vars ref
 
 let split_lambda = function
@@ -162,6 +165,158 @@ let split_product = function
   | CProdN (loc,(na::nal,t)::bl,c) -> (na,t,CProdN(loc,(nal,t)::bl,c))
   | _ -> anomaly "ill-formed fixpoint body"
 
+let rec extract_lam_binders c =
+  match c with
+      CLambdaN(loc,bl1,c') ->
+        let (bl,bd) = extract_lam_binders c' in
+        (bl1@bl, bd)
+    | _ -> ([],c)
+
+let rec extract_prod_binders c =
+  match c with
+      CProdN(loc,bl1,c') ->
+        let (bl,bd) = extract_prod_binders c' in
+        (bl1@bl, bd)
+    | _ -> ([],c)
+
+let rec check_same_pattern p1 p2 =
+  match p1, p2 with
+    | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when i1=i2 ->
+        check_same_pattern a1 a2
+    | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 ->
+        List.iter2 check_same_pattern a1 a2
+    | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> ()
+    | CPatNumeral(_,i1), CPatNumeral(_,i2) when i1=i2 -> ()
+    | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 ->
+        check_same_pattern e1 e2
+    | _ -> failwith "not same pattern"
+
+let check_same_ref r1 r2 =
+  match r1,r2 with
+  | Qualid(_,q1), Qualid(_,q2) when q1=q2 -> ()
+  | Ident(_,i1), Ident(_,i2) when i1=i2 -> ()
+  | _ -> failwith "not same ref"
+
+let rec check_same_type ty1 ty2 =
+  match ty1, ty2 with
+  | CRef r1, CRef r2 -> check_same_ref r1 r2
+  | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 ->
+      List.iter2 (fun (id1,i1,a1,b1) (id2,i2,a2,b2) ->
+        if id1<>id2 || i1<>i2 then failwith "not same fix";
+        check_same_type a1 a2;
+        check_same_type b1 b2)
+        fl1 fl2
+  | CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 ->
+      List.iter2 (fun (id1,a1,b1) (id2,a2,b2) ->
+        if id1<>id2 then failwith "not same fix";
+        check_same_type a1 a2;
+        check_same_type b1 b2)
+        fl1 fl2
+  | CArrow(_,a1,b1), CArrow(_,a2,b2) ->
+      check_same_type a1 a2;
+      check_same_type b1 b2
+  | CProdN(_,bl1,a1), CProdN(_,bl2,a2) ->
+      List.iter2 check_same_binder bl1 bl2;
+      check_same_type a1 a2
+  | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
+      List.iter2 check_same_binder bl1 bl2;
+      check_same_type a1 a2
+  | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 ->
+      check_same_type a1 a2;
+      check_same_type b1 b2
+  | CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 ->
+      List.iter2 check_same_type al1 al2
+  | CApp(_,e1,al1), CApp(_,e2,al2) ->
+      check_same_type e1 e2;
+      List.iter2 (fun (a1,e1) (a2,e2) ->
+                    if e1<>e2 then failwith "not same expl";
+                    check_same_type a1 a2) al1 al2
+  | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) ->
+      List.iter2 check_same_type a1 a2;
+      List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
+        List.iter2 check_same_pattern pl1 pl2;
+        check_same_type r1 r2) brl1 brl2
+  | COrderedCase(_,_,_,a1,bl1), COrderedCase(_,_,_,a2,bl2) ->
+      check_same_type a1 a2;
+      List.iter2 check_same_type bl1 bl2
+  | CHole _, CHole _ -> ()
+  | CMeta(_,i1), CMeta(_,i2) when i1=i2 -> ()
+  | CSort(_,s1), CSort(_,s2) when s1=s2 -> ()
+  | CCast(_,a1,b1), CCast(_,a2,b2) ->
+      check_same_type a1 a2;
+      check_same_type b1 b2
+  | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
+      List.iter2 check_same_type e1 e2
+  | CNumeral(_,i1), CNumeral(_,i2) when i1=i2 -> ()
+  | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
+      check_same_type e1 e2
+  | _ when ty1=ty2 -> ()
+  | _ -> failwith "not same type"
+
+and check_same_binder (nal1,e1) (nal2,e2) =
+  List.iter2 (fun (_,na1) (_,na2) ->
+    if na1<>na2 then failwith "not same name") nal1 nal2;
+  check_same_type e1 e2
+
+let merge_binders (na1,ty1) (na2,ty2) =
+  let na =
+    match snd na1, snd na2 with
+        Anonymous, Name id -> na2
+      | Name id, Anonymous -> na1
+      | Anonymous, Anonymous -> na1
+      | Name id1, Name id2 ->
+          if id1 <> id2 then failwith "not same name" else na1 in
+  let ty =
+    match ty1, ty2 with
+        CHole _, _ -> ty2
+      | _, CHole _ -> ty1
+      | _ ->
+          check_same_type ty1 ty2;
+          ty2 in
+  ([na],ty)
+            
+let rec strip_domain bvar c =
+  match c with
+    | CArrow(loc,a,b) ->
+        (merge_binders bvar ((dummy_loc,Anonymous),a), b)
+    | CProdN(loc,[([na],ty)],c') ->
+        (merge_binders bvar (na,ty), c')
+    | CProdN(loc,([na],ty)::bl,c') ->
+        (merge_binders bvar (na,ty), CProdN(loc,bl,c'))
+    | CProdN(loc,(na::nal,ty)::bl,c') ->
+        (merge_binders bvar (na,ty), CProdN(loc,(nal,ty)::bl,c'))
+    | _ -> failwith "not a product"
+
+(* Note: binder sharing is lost *)
+let rec strip_domains (nal,ty) c =
+  match nal with
+      [] -> assert false
+    | [na] ->
+        let bnd, c' = strip_domain (na,ty) c in
+        ([bnd],None,c')
+    | na::nal ->
+        let bnd, c1 = strip_domain (na,ty) c in
+        (try
+          let bl, rest, c2 = strip_domains (nal,ty) c1 in
+          (bnd::bl, rest, c2)
+        with Failure _ -> ([bnd],Some (nal,ty), c1))
+
+let rec extract_def_binders c ty =
+  match c with
+    | CLambdaN(loc,bvar::lams,b) ->
+        (try
+          let bvar', rest, ty' = strip_domains bvar ty in
+          let c' =
+            match rest, lams with
+                None,[] -> b
+              | None, _ -> CLambdaN(loc,lams,b)
+              | Some bvar,_ -> CLambdaN(loc,bvar::lams,b) in
+          let (bl,c2,ty2) = extract_def_binders c' ty' in
+          (bvar'@bl, c2, ty2)
+        with Failure _ ->
+          ([],c,ty))
+    | _ -> ([],c,ty)
+
 let rec split_fix n typ def =
   if n = 0 then ([],typ,def)
   else
@@ -174,8 +329,10 @@ let pr_recursive_decl pr id b t c =
   pr_id id ++ b ++ pr_opt_type_spc pr t ++ str " :=" ++
   brk(1,2) ++ pr ltop c
 
-let pr_fixdecl pr (id,n,t,c) =
-  let (bl,t,c) = split_fix (n+1) t c in
+let pr_fixdecl pr (id,n,t0,c0) =
+  let (bl,t,c) = extract_def_binders t0 c0 in
+  let (bl,t,c) =
+    if List.length bl <= n then split_fix (n+1) t0 c0 else (bl,t,c) in
   let annot =
     let ids = List.flatten (List.map fst bl) in
     if List.length ids > 1 then 
@@ -193,10 +350,6 @@ let pr_recursive pr_decl id = function
       prlist_with_sep (fun () -> fnl() ++ str "with ") pr_decl dl ++
       fnl() ++ str "for " ++ pr_id id
 
-let rec pr_arrow pr = function
-  | CArrow (_,a,b) -> pr (larrow,L) a ++ str " ->" ++ brk(1,0) ++ pr_arrow pr b
-  | a -> pr (-larrow,E) a
-
 let pr_annotation pr po =
   match po with
       None -> mt()
@@ -211,18 +364,24 @@ let rec pr inherited a =
   | CCoFix (_,id,cofix) ->
       hov 0 (str "cofix " ++ pr_recursive (pr_cofixdecl pr) (snd id) cofix),
       lfix
-  | CArrow _ -> hv 0 (pr_arrow pr a), larrow
-  | CProdN (_,bl,a) ->
-      hv 1 (
-	str "!" ++ pr_binders pr bl ++ str "." ++ spc()  ++ pr ltop a), lprod
-  | CLambdaN (_,bl,a) ->
+  | CArrow (_,a,b) ->
+      hov 0 (pr (larrow,L) a ++ str " ->" ++ brk(1,0) ++ pr (-larrow,E) b),
+      larrow
+  | CProdN _ ->
+      let (bl,a) = extract_prod_binders a in
+      hv 0 (str "!" ++ pr_binders pr bl ++ str "." ++ spc() ++ pr ltop a),
+      lprod
+  | CLambdaN _ ->
+      let (bl,a) = extract_lam_binders a in
       hov 2 (
 	str "fun" ++ spc () ++ pr_binders pr bl ++
         str " =>" ++ spc() ++ pr ltop a),
       llambda
   | CLetIn (_,x,a,b) ->
+      let (bl,a) = extract_lam_binders a in
       hv 0 (
-        hov 2 (str "let " ++ pr_name (snd x) ++ str " :=" ++ spc() ++
+        hov 2 (str "let " ++ pr_located pr_name x ++
+               pr_arg_binders pr bl ++ str " :=" ++ spc() ++
                pr ltop a ++ str " in") ++
         spc () ++ pr ltop b),
       lletin
@@ -285,18 +444,6 @@ let rec pr inherited a =
   if prec_less prec inherited then strm
   else str"(" ++ strm ++ str")"
 
-
-let rec fact_constr c =
-  match c with
-      CLambdaN(loc,bl1,CLambdaN(_,bl2,b)) ->
-        fact_constr (CLambdaN(loc,bl1@bl2,b))
-    | CProdN(loc,bl1,CProdN(_,bl2,b)) ->
-        fact_constr (CProdN(loc,bl1@bl2,b))
-    | _ -> map_constr_expr_with_binders
-        (fun _ -> fact_constr) (fun _ _ -> ()) () c
-let pr l c = pr l (fact_constr c)
-
-
 let transf env c =
   if Options.do_translate() then
     Constrextern.extern_rawconstr (Termops.vars_of_env env)
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 27e1307c59..fe1c560ca0 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -20,10 +20,18 @@ open Topconstr
 open Names
 open Util
 
-val prec_less : int -> int * Ppextend.parenRelation -> bool
+val extract_lam_binders :
+  constr_expr -> (name located list * constr_expr) list * constr_expr
+val extract_prod_binders :
+  constr_expr -> (name located list * constr_expr) list * constr_expr
+val extract_def_binders :
+  constr_expr -> constr_expr ->
+  (name located list * constr_expr) list *  constr_expr * constr_expr
+val split_fix :
+  int -> constr_expr -> constr_expr -> 
+  (name located list * constr_expr) list *  constr_expr * constr_expr
 
-val split_fix : int -> constr_expr -> constr_expr ->
-  (name located list * constr_expr) list * constr_expr * constr_expr
+val prec_less : int -> int * Ppextend.parenRelation -> bool
  
 val pr_global : Idset.t -> global_reference -> std_ppcmds
  
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 9a0bc64f8d..2ba13bb793 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -189,6 +189,10 @@ let rec pr_module_type pr_c = function
       pr_module_type pr_c mty ++ spc() ++ str" with" ++
       pr_with_declaration pr_c decl
 
+let pr_of_module_type prc (mty,b) =
+  str (if b then ":" else "<:") ++
+  pr_module_type prc mty
+
 let pr_module_vardecls pr_c (l,mty) =
   prlist
     (fun id ->
@@ -203,7 +207,10 @@ let pr_module_binders_list l pr_c = pr_module_binders l pr_c
 
 let rec pr_module_expr = function
   | CMEident qid -> pr_located pr_qualid qid
-  | CMEapply (me1,me2) -> pr_module_expr me1 ++ spc() ++ pr_module_expr me2
+  | CMEapply (me1,(CMEident _ as me2)) ->
+      pr_module_expr me1 ++ spc() ++ pr_module_expr me2
+  | CMEapply (me1,me2) ->
+      pr_module_expr me1 ++ spc() ++ str"(" ++ pr_module_expr me2 ++ str")"
 
 let pr_opt_casted_constr pr_c = function
   | CCast (loc,c,t) -> pr_c c ++ str":" ++ pr_c t
@@ -440,17 +447,18 @@ let rec pr_vernac = function
             str" in" ++ spc() in
       let pr_def_body = function
         | DefineBody (bl,red,c,d) ->
-            let (binds,body) = match c with
-              | CLambdaN (_,bl2,a) when d=None ->
-                  (pr_ne_sep spc (pr_vbinders pr_lconstr) bl ++
-                   spc() ++ pr_binders bl2, a)
-              | _ -> (pr_ne_sep spc (pr_vbinders pr_lconstr) bl, c) in
-            let ty =
-              match d with
-                | None -> mt()
-                | Some t -> spc() ++ str":" ++ pr_lconstrarg t in
+            let (bl2,body,ty) = match d with
+              | None ->
+                  let bl2,body = extract_lam_binders c in
+                  (bl2,body,mt())
+              | Some ty ->
+                  let bl2,body,ty = extract_def_binders c ty in
+                  (bl2,body, spc() ++ str":" ++ pr_lconstrarg ty) in
+            let bindings =
+              pr_ne_sep spc (pr_vbinders pr_lconstr) bl ++
+              if bl2 = [] then mt() else (spc() ++ pr_binders bl2) in
             let ppred = Some (pr_reduce red ++ pr_lconstr body) in
-            (binds,ty,ppred)
+            (bindings,ty,ppred)
         | ProveBody (bl,t) ->
             (pr_vbinders pr_lconstr bl, str" :" ++ pr_lconstrarg t, None) in
       let (binds,typ,c) = pr_def_body b in
@@ -475,8 +483,9 @@ let rec pr_vernac = function
         (pr_assumption_token stre ++ spc() ++ pr_ne_params_list pr_lconstr l)
   | VernacInductive (f,l) ->
       let pr_constructor (coe,(id,c)) =
-        pr_id id ++ spc() ++ (if coe then str":>" else str":")
-        ++ pr_lconstrarg c in
+        hov 2 (pr_id id ++ str" " ++
+               (if coe then str":>" else str":") ++
+               pr_lconstrarg c) in
       let pr_constructor_list l = match l with
         | [] -> mt()
         | _ ->
@@ -490,16 +499,28 @@ let rec pr_vernac = function
         prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_oneind l)
   | VernacFixpoint recs ->
       let pr_onerec = function
-        | (id,_,CProdN(_,bl,type_),CLambdaN(_,_,def)) ->
-            pr_id id ++ spc() ++ pr_binders bl ++ spc()
+        | (id,n,type_0,def0) ->
+            let (bl,def,type_) = extract_def_binders def0 type_0 in
+            let ids = List.flatten (List.map fst bl) in
+            let (bl,def,type_) =
+              if List.length ids <= n then split_fix (n+1) def0 type_0
+              else (bl,def,type_) in
+            let ids = List.flatten (List.map fst bl) in
+            let annot =
+              if List.length ids > 1 then 
+                spc() ++ str "{struct " ++
+                pr_name (snd (List.nth ids n)) ++ str"}"
+              else mt() in
+            pr_id id ++ str" " ++ pr_binders bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr c) type_
-            ++ str" :=" ++ brk(1,1) ++ pr_lconstr def 
-        | _ -> mt() in
+            ++ str" :=" ++ brk(1,1) ++ pr_lconstr def in
       hov 1 (str"Fixpoint" ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)  
   | VernacCoFixpoint corecs ->
       let pr_onecorec (id,c,def) =
-        pr_id id ++ spc() ++ str":" ++ pr_lconstrarg c ++
+        let (bl,def,c) = extract_def_binders def c in
+        pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+        pr_lconstrarg c ++
         str" :=" ++ brk(1,1) ++ pr_lconstr def in
       hov 1 (str"CoFixpoint" ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)  
@@ -549,14 +570,20 @@ let rec pr_vernac = function
   | VernacIdentityCoercion (s,id,c1,c2) -> hov 1 (str"Identity Coercion" ++ (match s with | Decl_kinds.Local -> spc() ++ str"Local" ++ spc() | Decl_kinds.Global -> spc()) ++ pr_id id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
 
   (* Modules and Module Types *)
-  | VernacDeclareModule (id,l,m1,m2) -> hov 1 (str"Module" ++ spc() ++ pr_id id ++ spc() ++ pr_module_binders_list l pr_lconstr ++ (match m1 with
-    | None -> mt()
-    | Some n1 -> str" : " ++ str"TODO" (* pr_module_type pr_constr n1 *) ) ++ (match m2 with
-      | None -> mt()
-      | Some n2 -> str" := " ++ pr_module_expr n2))
-  | VernacDeclareModuleType (id,l,m) -> hov 1 (str"Module Type" ++ spc() ++ pr_id id ++ spc() ++ pr_module_binders_list l pr_lconstr ++ (match m with
-    | None -> mt()
-    | Some n -> str" := " ++ pr_module_type pr_lconstr n))
+  | VernacDefineModule (m,bl,ty,bd) ->
+      hov 2 (str"Module " ++ pr_id m ++ spc() ++
+             pr_module_binders_list bl pr_lconstr ++
+             pr_opt (pr_of_module_type pr_lconstr) ty ++
+             pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd)
+  | VernacDeclareModule (id,l,m1,m2) ->
+      hov 2 (str"Declare Module " ++ pr_id id ++ spc() ++
+             pr_module_binders_list l pr_lconstr ++
+             pr_opt (pr_of_module_type pr_lconstr) m1 ++
+             pr_opt (fun me -> str ":= " ++ pr_module_expr me) m2)
+  | VernacDeclareModuleType (id,l,m) ->
+      hov 2 (str"Module Type " ++ pr_id id ++ spc() ++
+             pr_module_binders_list l pr_lconstr ++
+             pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m)
 
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
@@ -692,13 +719,6 @@ let rec pr_vernac = function
   | VernacV7only _ -> mt()
   | VernacV8only com -> pr_vernac com
   | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te 
-  | VernacDefineModule (m,bl,ty,bd) ->
-      hov 2 (str"Module " ++ pr_id m ++
-      pr_module_binders bl pr_lconstr ++
-      (match ty with
-          None -> mt()
-        | Some(t,_) -> pr_module_type pr_lconstr t) ++
-      pr_opt pr_module_expr bd)
 
 and pr_extend s cl =
   let pr_arg a =