Ensures that let-in's in arities of inductive types work well. Maybe not

very useful in practice but as soon as let-in's were not forbidden in
the internal data structure, better to do it. Moreover, this gets
closer to the view were inductive definitions are uniformly built from
"contexts". (checker not changed!)

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

6 files changed, 96 insertions, 17 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 057f342aa..1f9cc0f1f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -954,14 +954,18 @@ let adjust_impossible_cases pb pred tomatch submat =
 (* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*)
 (*                                                                           *)
 (*****************************************************************************)
-let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
+let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl =
   (* Assume some gamma st: gamma, (X,x:=realargs,copt), tms |- ccl *)
   let nrealargs = List.length names in
   let k = nrealargs + (if depna<>Anonymous then 1 else 0) in
   (* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt), tms |- ccl' *)
   let n = cs.cs_nargs in
   let ccl' = liftn_predicate n (k+1) ccl tms in
-  let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in
+  let argsi =
+    if nrealargs <> 0 then
+      adjust_subst_to_rel_context arsign (Array.to_list cs.cs_concl_realargs)
+    else
+      [] in
   let copti = if depna<>Anonymous then Some (build_dependent_constructor cs) else None in
   (* The substituends argsi, copti are all defined in gamma, x1...xn *)
   (* We need _parallel_ bindings to get gamma, x1...xn, tms |- ccl'' *)
@@ -1063,7 +1067,7 @@ let shift_problem ((current,t),_,(nadep,_)) pb =
      mat = List.map remove_current_pattern pb.mat }
 
 (* Building the sub-pattern-matching problem for a given branch *)
-let build_branch current deps (realnames,dep) pb eqns const_info =
+let build_branch current deps (realnames,dep) pb arsign eqns const_info =
   (* We remember that we descend through a constructor *)
   let alias_type =
     if Array.length const_info.cs_concl_realargs = 0
@@ -1120,7 +1124,7 @@ let build_branch current deps (realnames,dep) pb eqns const_info =
       1 typs' (List.rev dep_sign) in
 
   let pred = 
-    specialize_predicate typs'' (realnames,dep) const_info tomatch pb.pred in
+    specialize_predicate typs'' (realnames,dep) arsign const_info tomatch pb.pred in
 
   let currents = List.map (fun x -> Pushed x) typs'' in
 
@@ -1179,6 +1183,7 @@ and match_current pb tomatch =
     | IsInd (_,(IndType(indf,realargs) as indt),names) ->
 	let mind,_ = dest_ind_family indf in
 	let cstrs = get_constructors pb.env indf in
+	let arsign, _ = get_arity pb.env indf in
 	let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in
 	if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt  then
 	  compile (shift_problem ct pb)
@@ -1189,7 +1194,7 @@ and match_current pb tomatch =
 	  let pb = generalize_problem (names,dep) pb deps in
 
 	  (* We compile branches *)
-	  let brs = array_map2 (compile_branch current (names,dep) deps pb) eqns cstrs in
+	  let brs = array_map2 (compile_branch current (names,dep) deps pb arsign) eqns cstrs in
 
 	  (* We build the (elementary) case analysis *)
 	  let brvals = Array.map (fun (v,_) -> v) brs in
@@ -1202,8 +1207,8 @@ and match_current pb tomatch =
 	  { uj_val = applist (case, inst);
 	    uj_type = substl inst typ }
 
-and compile_branch current names deps pb eqn cstr =
-  let sign, pb = build_branch current deps names pb eqn cstr in
+and compile_branch current names deps pb arsign eqn cstr =
+  let sign, pb = build_branch current deps names pb arsign eqn cstr in
   let j = compile pb in
   (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
 
@@ -1550,19 +1555,19 @@ let extract_arity_signature env0 tomatchl tmsign =
 	    str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = lift_inductive_family n indf in
-	  let (ind,params) = dest_ind_family indf' in
-	  let nrealargs = List.length realargs in
+	  let (ind,_) = dest_ind_family indf' in
+	  let nparams_ctxt,nrealargs_ctxt = inductive_nargs env0 ind in
+	  let arsign = fst (get_arity env0 indf') in
 	  let realnal =
 	    match t with
 	      | Some (loc,ind',nparams,realnal) ->
 		  if ind <> ind' then
 		    user_err_loc (loc,"",str "Wrong inductive type.");
-		  if List.length params <> nparams
-		    or nrealargs <> List.length realnal then
+		  if nparams_ctxt <> nparams
+		    or nrealargs_ctxt <> List.length realnal then
 		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
-	      | None -> list_make nrealargs Anonymous in
-	  let arsign = fst (get_arity env0 indf') in
+	      | None -> list_make nrealargs_ctxt Anonymous in
 (* 	  let na =  *)
 (* 	    match na with  *)
 (* 	      | Name _ -> na *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 6a4c066ce..0b07bc859 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -58,7 +58,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
       (RecursionSchemeError
 	 (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
 
-  let ndepar = mip.mind_nrealargs + 1 in
+  let ndepar = mip.mind_nrealargs_ctxt + 1 in
 
   (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
   (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
@@ -594,3 +594,56 @@ let lookup_eliminator ind_sp s =
        pr_global_env Idset.empty (IndRef ind_sp) ++ 
        strbrk " on sort " ++ pr_sort_family s ++
        strbrk " is probably not allowed.")
+
+(* Build the congruence lemma associated to an inductive type 
+   I p1..pn a1..am with one constructor C : I q1..qn b1..bm *)
+
+(* TODO: extend it to types with more than one index *)
+
+let build_congr env (eq,refl) ind (mib,mip) =
+  if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+    error "Not an inductive type with a single constructor.";
+  if mip.mind_nrealargs <> 1 then
+    error "Expect an inductive type with one predicate parameter.";
+  let i = 1 in
+  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  if List.exists (fun (_,b,_) -> b <> None) realsign then
+    error "Inductive equalities with local definitions in arity not supported";
+  let env_with_arity = push_rel_context mip.mind_arity_ctxt env in
+  let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
+  let _,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let _,constrargs = decompose_app ccl in
+  let c = List.nth constrargs (i - 1) in
+  let varB = id_of_string "B" in
+  let varH = id_of_string "H" in
+  let varf = id_of_string "f" in
+  let ci = make_case_info (Global.env()) ind RegularStyle in
+  let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn ~init:c s in
+  let my_it_mkLambda_or_LetIn_name s c = it_mkLambda_or_LetIn_name env c s in
+  my_it_mkLambda_or_LetIn mib.mind_params_ctxt
+     (mkNamedLambda varB (new_Type ())
+     (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB))
+     (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign)
+     (mkNamedLambda varH
+        (applist
+           (mkInd ind,
+	    extended_rel_list (mip.mind_nrealargs+2) mib.mind_params_ctxt @
+	    extended_rel_list 0 realsign))
+     (mkCase (ci,
+       my_it_mkLambda_or_LetIn_name
+	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
+         (mkLambda
+           (Anonymous,
+            applist
+             (mkInd ind,
+	        extended_rel_list (2*mip.mind_nrealargs+3) mib.mind_params_ctxt
+	        @ extended_rel_list 0 realsign),
+            mkApp (eq, 
+	      [|mkVar varB;
+                mkApp (mkVar varf, [|lift (2*mip.mind_nrealargs+3) c|]);
+		mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
+       mkVar varH,
+       [|mkApp (refl,
+          [|mkVar varB;
+	    mkApp (mkVar varf, [|lift (mip.mind_nrealargs+2) c|])|])|]))))))
+ 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 45fbe3227..3150ed63b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -129,7 +129,7 @@ let get_full_arity_sign env ind =
 
 let inductive_nargs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  mib.mind_nparams, mip.mind_nrealargs
+  (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt)
 
 let allowed_sorts env (kn,i as ind) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -138,7 +138,7 @@ let allowed_sorts env (kn,i as ind) =
 (* Annotation for cases *)
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let print_info = { ind_nargs = mip.mind_nrealargs; style = style } in
+  let print_info = { ind_nargs = mip.mind_nrealargs_ctxt; style = style } in
   { ci_ind     = ind;
     ci_npar    = mib.mind_nparams;
     ci_cstr_nargs = mip.mind_consnrealdecls;
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 357fb0908..cc1bb7f41 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -58,7 +58,7 @@ val mis_nf_constructor_type :
 val mis_constr_nargs : inductive -> int array
 val mis_constr_nargs_env : env -> inductive -> int array
 
-(* Return number of expected parameters and of expected real arguments *)
+(* Return the lengths of parameters signature and real arguments signature *)
 val inductive_nargs : env -> inductive -> int * int
 
 val mis_constructor_nargs_env : env -> constructor -> int
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 4034d8667..47bc97251 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -1096,6 +1096,25 @@ let substl_rel_context l =
 let lift_rel_context n =
   map_rel_context_with_binders (liftn n)
 
+let smash_rel_context sign =
+  let rec aux acc = function
+  | [] -> acc
+  | (_,None,_ as d) :: l -> aux (d::acc) l
+  | (_,Some b,_) :: l ->
+      (* Quadratic in the number of let but there are probably a few of them *)
+      aux (List.rev (substl_rel_context [b] (List.rev acc))) l
+  in List.rev (aux [] sign)
+
+let adjust_subst_to_rel_context sign l =
+  let rec aux subst sign l =
+    match sign, l with 
+    | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args'
+    | (_,Some c,_)::sign', args' ->
+	aux (substl (List.rev subst) c :: subst) sign' args'
+    | [], [] -> List.rev subst
+    | _ -> anomaly "Instance and signature do not match"
+  in aux [] (List.rev sign) l
+
 let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init
 
 let rec mem_named_context id = function
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index f9d432907..3d167ebb0 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -267,6 +267,8 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : rel_context -> (name * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
 val substl_rel_context : constr list -> rel_context -> rel_context
+val smash_rel_context : rel_context -> rel_context (* expand lets in context *)
+val adjust_subst_to_rel_context : rel_context -> constr list -> constr list
 val map_rel_context_in_env :
   (env -> constr -> constr) -> env -> rel_context -> rel_context
 val map_rel_context_with_binders :