Mise en place possibilité de définitions locales dans les paramètres des inductifs

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

8 files changed, 76 insertions, 64 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 480ec8728c..5a18643164 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -488,7 +488,7 @@ let build_inductive env env_ar finite inds recargs cst =
   (* Check one inductive *)
   let build_one_packet (params,id,ar,cnames,issmall,isunit,lc) recarg =
     (* Arity in normal form *)
-    let nparams = rel_context_length params in
+    let nparamargs = rel_context_nhyps params in
     let (ar_sign,ar_sort) = dest_arity env ar in
     let nf_ar =
       if isArity (body_of_type ar) then ar
@@ -498,19 +498,16 @@ let build_inductive env env_ar finite inds recargs cst =
     let nf_lc =
       array_map2 (fun (d,b) c -> it_mkProd_or_LetIn b d) splayed_lc lc in
     let nf_lc = if nf_lc = lc then lc else nf_lc in
-    let carities =
-      Array.map
-        (fun (args,_) -> rel_context_length args - nparams) splayed_lc in
     (* Elimination sorts *)
     let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in
     let kelim = allowed_sorts issmall isunit ar_sort in
     (* Build the inductive packet *)
     { mind_typename = id;
-      mind_nparams = rel_context_nhyps params;
+      mind_nparams = nparamargs;
       mind_params_ctxt = params;
       mind_user_arity  = ar;
       mind_nf_arity = nf_ar;
-      mind_nrealargs = rel_context_length ar_sign - nparams;
+      mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
       mind_sort = ar_sort;
       mind_kelim = kelim;
       mind_consnames = Array.of_list cnames;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d038e7d8c3..21906628cd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -222,6 +222,9 @@ GEXTEND Gram
   oneind:
     [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; 
         ntn = OPT decl_notation ; ":="; lc = constructor_list ->
+	  let indpar = 
+	    List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t))
+	      indpar in
 	  (id,ntn,indpar,c,lc) ] ]
   ;
   simple_binders_list:
@@ -303,6 +306,9 @@ GEXTEND Gram
   gallina_ext:
     [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_token;
         indl = block_old_style ->
+	  let bl = 
+	    List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t)) bl
+	  in
 	  let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in
 	  VernacInductive (f,indl')
       | b = record_token; oc = opt_coercion; name = base_ident;
@@ -321,6 +327,9 @@ GEXTEND Gram
       | IDENT "Scheme"; l = schemes -> VernacScheme l
       | f = finite_token; s = csort; id = base_ident;
 	indpar = simple_binders_list; ":="; lc = constructor_list -> 
+	  let indpar =
+	    List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t))
+	      indpar in
           VernacInductive (f,[id,None,indpar,s,lc]) ] ]
   ;
   csort:
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 6b11d5c985..31daf4afda 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -184,7 +184,7 @@ GEXTEND Gram
     ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; 
+    [ [ id = base_ident; indpar = LIST0 binder_let; ":"; c = lconstr; 
         ntn = decl_notation; ":="; lc = constructor_list ->
 	  (id,ntn,indpar,c,lc) ] ]
   ;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 01b1bc824f..49034b1b1f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -202,7 +202,7 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
   let (mib,mip) = Inductive.lookup_mind_specif tenv indsp in
   let get_consnarg j = 
     let typi = mis_nf_constructor_type (indsp,mib,mip) (j+1) in
-    let _,t = decompose_prod_n_assum mip.mind_nparams typi in
+    let _,t = decompose_prod_n_assum (List.length mip.mind_params_ctxt) typi in
     List.rev (fst (decompose_prod_assum t)) in
   let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in
   let consnargsl = Array.map List.length consnargs in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index adc5932f18..792fe6d2d9 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -150,10 +150,16 @@ let get_constructors env (ind,params) =
   Array.init (Array.length mip.mind_consnames)
     (fun j -> get_constructor (ind,mib,mip,params) (j+1))
 
+let rec instantiate args c = match kind_of_term c, args with
+  | Prod (_,_,c), a::args -> instantiate args (subst1 a c)
+  | LetIn (_,b,_,c), args -> instantiate args (subst1 b c)
+  | _, [] -> c
+  | _ -> anomaly "too short arity"
+
 let get_arity env (ind,params) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let arity = body_of_type mip.mind_nf_arity in
-  destArity (prod_applist arity params)
+  let arity = mip.mind_nf_arity in
+  destArity (instantiate params arity)
 
 (* Functions to build standard types related to inductive *)
 let build_dependent_constructor cs =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f9de326db8..cade0b0e58 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -72,7 +72,7 @@ let rec adjust_conclusion a cs = function
 	user_err_loc (loc,"",
 	  str "Cannot infer the non constant arguments of the conclusion of "
 	  ++ pr_id cs);
-      let args = List.map (fun (id,_) -> CRef(Ident(loc,id))) params in
+      let args = List.map (fun id -> CRef(Ident(loc,id))) params in
       CAppExpl (loc,(None,Ident(loc,name)),List.rev args)
   | c -> c
 
@@ -197,30 +197,38 @@ let interp_mutual lparams lnamearconstrs finite =
       (fun acc (id,_,_,l) -> id::(List.map fst l)@acc) [] lnamearconstrs in
   if not (list_distinct allnames) then
     error "Two inductive objects have the same name";
-  let nparams = List.length lparams
+  let nparams = local_binders_length lparams
   and sigma = Evd.empty 
   and env0 = Global.env() in
   let env_params, params =
     List.fold_left
-      (fun (env, params) (id,t) ->
-	 let p = interp_binder sigma env (Name id) t in
-	 (Termops.push_rel_assum (Name id,p) env, (Name id,None,p)::params))
+      (fun (env, params) d -> match d with
+	| LocalRawAssum (nal,t) ->
+	    let t = interp_type sigma env t in
+	    let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
+	    let ctx = List.rev ctx in
+	    (push_rel_context ctx env, ctx@params)
+	| LocalRawDef ((_,na),c) ->
+	    let c = judgment_of_rawconstr sigma env c in
+	    let d = (na, Some c.uj_val, c.uj_type) in
+	    (push_rel d env,d::params))
       (env0,[]) lparams
   in
-  (* Pour permettre à terme les let-in dans les params *)
+  (* Builds the params of the inductive entry *)
   let params' =
-    List.map (fun (na,_,p) ->
+    List.map (fun (na,b,t) ->
 		let id = match na with
 		  | Name id -> id
-		  | Anonymous -> anomaly "Unnamed inductive variable"
-		in (id, LocalAssum p)) params
+		  | Anonymous -> anomaly "Unnamed inductive variable" in 
+		match b with
+		  | None -> (id, LocalAssum t)
+		  | Some b -> (id, LocalDef b)) params
   in
   let (ind_env,ind_impls,arityl) =
     List.fold_left
       (fun (env, ind_impls, arl) (recname, _, arityc, _) ->
          let arity = interp_type sigma env_params arityc in
-	 let fullarity =
-           prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params) in
+	 let fullarity = it_mkProd_or_LetIn arity params in
 	 let env' = Termops.push_rel_assum (Name recname,fullarity) env in
 	 let impls = 
 	   if Impargs.is_implicit_args()
@@ -229,12 +237,15 @@ let interp_mutual lparams lnamearconstrs finite =
 	 (env', (recname,impls)::ind_impls, (arity::arl)))
       (env0, [], []) lnamearconstrs
   in
-  let lparnames = List.map (fun (na,_,_) -> na) params in
+  (* Names of parameters as arguments of the inductive type (defs removed) *)
+  let lparargs = 
+    List.flatten
+      (List.map (function (id,LocalAssum _) -> [id] | _ -> []) params') in
   let notations = 
     List.map2 (fun (recname,ntnopt,_,_) ar ->
       option_app (fun df ->
         let larnames =
-	  List.rev_append lparnames 
+	  List.rev_append (List.map (fun id -> Name id) lparargs)
 	    (List.rev (List.map fst (fst (decompose_prod ar)))) in
 	(recname,larnames,df)) ntnopt)
       lnamearconstrs arityl in
@@ -257,7 +268,8 @@ let interp_mutual lparams lnamearconstrs finite =
 	   List.length (fst (Reductionops.splay_arity env_params Evd.empty ar))
 	 in
 	 let bodies =
-	   List.map2 (adjust_conclusion (nar,name,params')) constrnames bodies
+	   List.map2 (adjust_conclusion (nar,name,lparargs))
+	     constrnames bodies
 	 in
 
          (* Interpret the constructor types *)
@@ -286,7 +298,14 @@ let declare_mutual_with_eliminations mie =
   Indrec.declare_eliminations kn;
   kn
 
-let eq_la (id,ast) (id',ast') = id = id' & (* alpha_eq(ast,ast') *) (warning "check paramaters convertibility"; true)
+(* Very syntactical equality *)
+let eq_la d1 d2 = match d1,d2 with
+  | LocalRawAssum (nal,ast), LocalRawAssum (nal',ast') ->
+      List.for_all2 (fun (_,na) (_,na') -> na = na') nal nal'
+      & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false)
+  | LocalRawDef ((_,id),ast), LocalRawDef ((_,id'),ast') ->
+      id=id' & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false)
+  | _ -> false
 
 let extract_coe lc =
   List.fold_right
@@ -540,11 +559,6 @@ let rec generalize_rawconstr c = function
       List.fold_right (fun x b -> mkProdC([x],t,b)) idl
         (generalize_rawconstr c bl)
 
-let rec binders_length = function
-  | [] -> 0
-  | LocalRawDef _::bl -> 1 + binders_length bl
-  | LocalRawAssum (idl,_)::bl -> List.length idl + binders_length bl
-
 let start_proof id kind c hook =
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 266e6c0942..fc57d23aa8 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -127,7 +127,7 @@ type simple_binder = identifier * constr_expr
 type 'a with_coercion = coercion_flag * 'a
 type constructor_expr = simple_binder with_coercion
 type inductive_expr =
-     identifier * decl_notation * simple_binder list * constr_expr
+     identifier * decl_notation * local_binder list * constr_expr
     * constructor_expr list
 type definition_expr =
   | ProveBody of local_binder list * constr_expr
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index f5966a5ccc..0471d5d14a 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -321,26 +321,8 @@ let pr_binder pr_c ty na =
 let pr_vbinders l =
   hv 0 (pr_binders l)
 
-let length_of_valdecls n = function
-  | LocalRawAssum (nal,c) -> List.length nal + n
-  | LocalRawDef (_,c) -> n+1
-
-let length_of_vbinders =
-  List.fold_left length_of_valdecls 0
-
-let vars_of_binder l (nal,_) = 
-  List.fold_right (function (_,Name id) -> fun l -> id::l | (_,Anonymous) -> fun l -> l) nal l
-
-let vars_of_binders =
-  List.fold_left vars_of_binder []
-
-let anonymize_binder na c =
-  if Options.do_translate() then
-    Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env()))
-      (Reserve.anonymize_if_reserved na
-      (Constrintern.for_grammar
-        (Constrintern.interp_rawconstr Evd.empty (Global.env())) c))
-  else c
+let pr_binders_arg bl =
+  if bl = [] then mt () else spc () ++ pr_binders bl
 
 let pr_sbinders sbl =
   if sbl = [] then mt () else
@@ -621,12 +603,11 @@ let rec pr_vernac = function
                   let bl2,body,ty' = extract_def_binders c ty in
                   (bl2,body, spc() ++ str":" ++ spc () ++
                     pr_lconstr_env_n (Global.env())
-                    (length_of_vbinders bl + length_of_vbinders bl2)
+                    (local_binders_length bl + local_binders_length bl2)
                     false (prod_rawconstr ty bl)) in
             let bindings =
-              pr_ne_sep spc pr_vbinders bl ++
-              if bl2 = [] then mt() else (spc() ++ pr_binders bl2) in
-	    let n = length_of_vbinders bl + length_of_vbinders bl2 in
+	      pr_ne_sep spc pr_vbinders bl ++ pr_binders_arg bl2 in
+	    let n = local_binders_length bl + local_binders_length bl2 in
 	    let c',iscast = match d with None -> c, false
 	      | Some d -> CCast (dummy_loc,c,d), true in
             let ppred =
@@ -670,23 +651,28 @@ pr_vbinders bl ++ spc())
       (* Copie simplifiée de command.ml pour recalculer les implicites, *)
       (* les notations, et le contexte d'evaluation *)
       let lparams = match l with [] -> assert false | (_,_,la,_,_)::_ -> la in
-      let nparams = List.length lparams
+      let nparams = local_binders_length lparams
       and sigma = Evd.empty 
       and env0 = Global.env() in
       let (env_params,params) =
 	List.fold_left
-	  (fun (env,params) (id,t) ->
-	    let p = Constrintern.interp_binder sigma env (Name id) t in
-	    (Termops.push_rel_assum (Name id,p) env,
-	    (Name id,None,p)::params))
+	  (fun (env,params) d -> match d with
+	    | LocalRawAssum (nal,t) ->
+		let t = Constrintern.interp_type sigma env t in
+		let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal
+		in let ctx = List.rev ctx in
+		(Environ.push_rel_context ctx env, ctx@params)
+	    | LocalRawDef ((_,na),c) ->
+		let c = Constrintern.judgment_of_rawconstr sigma env c in
+		let d = (na, Some c.Environ.uj_val, c.Environ.uj_type) in
+		(Environ.push_rel d env,d::params))
 	  (env0,[]) lparams in
 
       let (ind_env,ind_impls,arityl) =
         List.fold_left
           (fun (env, ind_impls, arl) (recname, _, _, arityc, _) ->
             let arity = Constrintern.interp_type sigma env_params arityc in
-	    let fullarity =
-              Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params) in
+	    let fullarity = Termops.it_mkProd_or_LetIn arity params in
 	    let env' = Termops.push_rel_assum (Name recname,fullarity) env in
 	    let impls = 
 	      if Impargs.is_implicit_args()
@@ -747,7 +733,7 @@ pr_vbinders bl ++ spc())
       let pr_oneind key (id,ntn,indpar,s,lc) =
 	hov 0 (
           str key ++ spc() ++
-          pr_id id ++ spc() ++ pr_sbinders indpar ++ str":" ++ spc() ++
+          pr_id id ++ pr_binders_arg indpar ++ spc() ++ str":" ++ spc() ++
           pr_lconstr s ++ 
 	  pr_decl_notation ntn ++ str" :=") ++ pr_constructor_list lc in
 
@@ -822,7 +808,7 @@ pr_vbinders bl ++ spc())
             pr_id id ++ str" " ++ pr_binders bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr c) type_
             ++ pr_decl_notation ntn ++ str" :=" ++ brk(1,1) ++
-            pr_lconstr_env_n rec_sign (length_of_vbinders bl)
+            pr_lconstr_env_n rec_sign (local_binders_length bl)
 	      true (CCast (dummy_loc,def0,type_0))
       in
       hov 1 (str"Fixpoint" ++ spc() ++