Rename eta_expand_ind_stacks, fix the one from the checker and adapt

it to the new representation of projections and the new mind_finite
type.

9 files changed, 64 insertions, 57 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index cd6d0afee..c1d7b0d73 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -196,6 +196,7 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int;
   proj_type : constr; (* Type under params *)
+  proj_eta : constr * constr; (* Eta-expanded term and type *)
   proj_body : constr; (* For compatibility, the match version *)
 }
 
@@ -232,6 +233,11 @@ type regular_inductive_arity = {
   mind_sort : sorts;
 }
 
+type recursivity_kind =
+  | Finite (** = inductive *)
+  | CoFinite (** = coinductive *)
+  | BiFinite (** = non-recursive, like in "Record" definitions *)
+
 type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity
 
 type one_inductive_body = {
@@ -283,11 +289,11 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : (constr * constant array) option;  
+    mind_record : (constant array * projection_body array) option;  
     (** Whether the inductive type has been declared as a record, 
 	In that case we get its canonical eta-expansion and list of projections. *)
 
-    mind_finite : bool;  (** Whether the type is inductive or coinductive *)
+    mind_finite : recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
     mind_ntypes : int;  (** Number of types in the block *)
 
diff --git a/checker/closure.ml b/checker/closure.ml
index 5bd636b16..6f19fc59f 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -689,18 +689,26 @@ let rec reloc_rargs_rec depth stk =
 let reloc_rargs depth stk =
   if depth = 0 then stk else reloc_rargs_rec depth stk
 
-let rec drop_parameters depth n stk =
-  match stk with
+let rec try_drop_parameters depth n argstk =
+  match argstk with
       Zapp args::s ->
         let q = Array.length args in
-        if n > q then drop_parameters depth (n-q) s
-        else if n = q then reloc_rargs depth s
+        if n > q then try_drop_parameters depth (n-q) s
+        else if Int.equal n q then reloc_rargs depth s
         else
           let aft = Array.sub args n (q-n) in
           reloc_rargs depth (append_stack aft s)
-    | Zshift(k)::s -> drop_parameters (depth-k) n s
-    | [] -> assert (n=0); []
-    | _ -> assert false (* we know that n < stack_args_size(stk) *)
+    | Zshift(k)::s -> try_drop_parameters (depth-k) n s
+    | [] -> 
+	if Int.equal n 0 then []
+	else raise Not_found
+    | _ -> assert false
+	(* strip_update_shift_app only produces Zapp and Zshift items *)
+
+let drop_parameters depth n argstk =
+  try try_drop_parameters depth n argstk
+  with Not_found -> assert false
+    (* we know that n < stack_args_size(argstk) (if well-typed term) *) 
 
 (** Projections and eta expansion *)
 
@@ -720,37 +728,22 @@ let rec get_parameters depth n argstk =
     | _ -> assert false
 	(* strip_update_shift_app only produces Zapp and Zshift items *)
 
-let eta_expand_ind_stack env lft (ind,u) m s (lft, h) =
-  let mib = lookup_mind (fst ind) env in
-    match mib.mind_record with
-    | None -> raise Not_found
-    | Some (exp,_) -> 
-      let pars = mib.mind_nparams in
-      let h' = fapp_stack h in
-      let (depth, args, _) = strip_update_shift_app m s in
-      let paramargs = get_parameters depth pars args in
-      let subs = subs_cons (Array.append paramargs [|h'|], subs_id 0) in
-      let fexp = mk_clos subs exp in
-	(lft, (fexp, []))
-
-let eta_expand_ind_stacks env ind m s h =
+let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.mind_record with
-    | Some (exp,projs) when Array.length projs > 0 -> 
+    | Some (projs,pbs) when Array.length projs > 0 
+      && mib.mind_finite <> CoFinite -> 
+	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
+	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.mind_nparams in
-      let h' = fapp_stack h in
-      let (depth, args, _) = strip_update_shift_app m s in
-      let primitive = Environ.is_projection projs.(0) env in
-	if primitive then
-	  let s' = drop_parameters depth pars args in
-      (* Construct, pars1 .. parsm :: arg1...argn :: s ~= (t, []) ->
-	 arg1..argn :: s ~= (proj1 t...projn t) s
-      *)
-	  let hstack = Array.map (fun p -> { norm = Red;
-					     term = FProj (p, h') }) projs in
-	    s', [Zapp hstack]
-	else raise Not_found (* disallow eta-exp for non-primitive records *)
-    | _ -> raise Not_found
+      let right = fapp_stack (f, s') in
+      let (depth, args, s) = strip_update_shift_app m s in
+      (** Try to drop the params, might fail on partially applied constructors. *)
+      let argss = try_drop_parameters depth pars args in
+      let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
+					 term = FProj (p, right) }) projs in
+	argss, [Zapp hstack]	
+    | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
diff --git a/checker/closure.mli b/checker/closure.mli
index 9b152eb6a..03970fc9f 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -124,11 +124,8 @@ and stack = stack_member list
 
 val append_stack : fconstr array -> stack -> stack
 val eta_expand_stack : stack -> stack
-
-val eta_expand_ind_stack : env -> lift -> pinductive -> fconstr -> stack -> 
-  (lift * (fconstr * stack)) -> lift * (fconstr * stack)
  
-val eta_expand_ind_stacks : env -> inductive -> fconstr -> stack -> 
+val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
    (fconstr * stack) -> stack * stack
 
 (* To lazy reduce a constr, create a [clos_infos] with
diff --git a/checker/inductive.ml b/checker/inductive.ml
index f60094cfb..adb9e0347 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -40,14 +40,14 @@ let find_inductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match t with
     | Ind (ind,_)
-        when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
+        when (fst (lookup_mind_specif env ind)).mind_finite != CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match t with
     | Ind (ind,_)
-        when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
+        when (fst (lookup_mind_specif env ind)).mind_finite == CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let inductive_params (mib,_) = mib.mind_nparams
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 7bdc96283..403d27779 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -357,7 +357,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 	     | FConstruct ((ind2,j2),u2) ->
 	       (try
  	     	  let v2, v1 = 
- 		    eta_expand_ind_stacks (infos_env infos) ind2 hd2 v2 (snd appr1)
+ 		    eta_expand_ind_stack (infos_env infos) ind2 hd2 v2 (snd appr1)
  		  in convert_stacks univ infos lft1 lft2 v1 v2
  	     	with Not_found -> raise NotConvertible)
 	     | _ -> raise NotConvertible)
@@ -370,7 +370,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 	     match c1 with 
 	     | FConstruct ((ind1,j1),u1) ->
  	       (try let v1, v2 = 
-		      eta_expand_ind_stacks (infos_env infos) ind1 hd1 v1 (snd appr2)
+		      eta_expand_ind_stack (infos_env infos) ind1 hd1 v1 (snd appr2)
 		    in convert_stacks univ infos lft1 lft2 v1 v2
 		with Not_found -> raise NotConvertible)
 	     | _ -> raise NotConvertible)
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index c4688e190..a9a037bce 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -91,7 +91,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       | IndType ((_,0), mib) -> mib
       | _ -> error ()
   in
-  let mib2 =  subst_mind subst2 mib2 in
+  let mib2 = subst_mind subst2 mib2 in
   let check eq f = if not (eq (f mib1) (f mib2)) then error () in
   let bool_equal (x : bool) (y : bool) = x = y in
   let u = 
@@ -101,6 +101,16 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       Univ.UContext.instance mib1.mind_universes)
     else Univ.Instance.empty
   in
+  let eq_projection_body p1 p2 =
+    let check eq f = if not (eq (f p1) (f p2)) then error () in
+    check eq_mind (fun x -> x.proj_ind);
+    check (==) (fun x -> x.proj_npars);
+    check (==) (fun x -> x.proj_arg);
+    check (eq_constr) (fun x -> x.proj_type);
+    check (eq_constr) (fun x -> fst x.proj_eta);
+    check (eq_constr) (fun x -> snd x.proj_eta);
+    check (eq_constr) (fun x -> x.proj_body); true
+  in
   let check_inductive_type env t1 t2 =
 
     (* Due to sort-polymorphism in inductive types, the conclusions of
@@ -161,7 +171,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       (arities_of_specif (kn,u) (mib1,p1))
       (arities_of_specif (kn,u) (mib2,p2))
   in
-  check bool_equal (fun mib -> mib.mind_finite);
+  check (==) (fun mib -> mib.mind_finite);
   check Int.equal (fun mib -> mib.mind_ntypes);
   assert (Array.length mib1.mind_packets >= 1
 	    && Array.length mib2.mind_packets >= 1);
@@ -188,8 +198,9 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let record_equal x y =
     match x, y with
     | None, None -> true
-    | Some (r1,p1), Some (r2,p2) ->
-      eq_constr r1 r2 && Array.for_all2 eq_con_chk p1 p2
+    | Some (p1,pb1), Some (p2,pb2) ->
+      Array.for_all2 eq_con_chk p1 p2 &&
+      Array.for_all2 eq_projection_body pb1 pb2
     | _, _ -> false
   in
   check record_equal (fun mib -> mib.mind_record);
diff --git a/kernel/closure.ml b/kernel/closure.ml
index d0a9ffd64..8851ea2b6 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -854,7 +854,7 @@ let rec get_parameters depth n argstk =
 	(* strip_update_shift_app only produces Zapp and Zshift items *)
 
 
-(** [eta_expand_ind_stacks env ind c s t] computes stacks correspoding 
+(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
     to the conversion of the eta expansion of t, considered as an inhabitant 
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
@@ -863,7 +863,7 @@ let rec get_parameters depth n argstk =
     @raises Not_found if the inductive is not a primitive record, or if the 
     constructor is partially applied.
  *)
-let eta_expand_ind_stacks env ind m s (f, s') =
+let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (projs,pbs) when Array.length projs > 0 
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 8c3eb81f4..adcf25857 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -187,7 +187,7 @@ val whd_val : clos_infos -> fconstr -> constr
 val whd_stack :
   clos_infos -> fconstr -> stack -> fconstr * stack
 
-(** [eta_expand_ind_stacks env ind c s t] computes stacks correspoding 
+(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
     to the conversion of the eta expansion of t, considered as an inhabitant 
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
@@ -196,7 +196,7 @@ val whd_stack :
     @raises Not_found if the inductive is not a primitive record, or if the 
     constructor is partially applied.
  *)
-val eta_expand_ind_stacks : env -> inductive -> fconstr -> stack -> 
+val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
    (fconstr * stack) -> stack * stack
 
 (** Conversion auxiliary functions to do step by step normalisation *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 78d2105ab..ebba23165 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -434,7 +434,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	     | FConstruct ((ind2,j2),u2) ->
 	       (try
  	     	  let v2, v1 =
- 	     	    eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1)
+ 	     	    eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
  	     	  in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
  	     	with Not_found -> raise NotConvertible)
 	     | _ -> raise NotConvertible)
@@ -447,7 +447,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	     match c1 with
 	     | FConstruct ((ind1,j1),u1) ->
  	       (try let v1, v2 =
-	     	      eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2)
+	     	      eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
 	     	    in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
 	     	with Not_found -> raise NotConvertible)
 	     | _ -> raise NotConvertible)
@@ -472,14 +472,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FConstruct ((ind1,j1),u1), _) ->
       (try
     	 let v1, v2 =
-    	   eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2)
+    	   eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
     	 in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (_, FConstruct ((ind2,j2),u2)) ->
       (try
     	 let v2, v1 =
-    	   eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1)
+    	   eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
     	 in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)