Add a boolean to indicate the unfolding state of a primitive projection,

so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.

18 files changed, 112 insertions, 46 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 36a022fd9..6fd1c689f 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -501,11 +501,12 @@ let rec compile_constr reloc c sz cont =
   | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
   | Proj (p,c) -> 
     (* compile_const reloc p [|c|] sz cont *)
-    let cb = lookup_constant p !global_env in
+    let kn = Projection.constant p in
+    let cb = lookup_constant kn !global_env in
       (* TODO: better representation of projections *)
     let pb = Option.get cb.const_proj in
     let args = Array.make pb.proj_npars mkProp in
-      compile_const reloc p Univ.Instance.empty (Array.append args [|c|]) sz cont
+      compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont
 
   | Cast(c,_,_) -> compile_constr reloc c sz cont
 
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 14afcc4db..23861347a 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -88,6 +88,7 @@ module type RedFlagsSig = sig
   val red_add_transparent : reds -> transparent_state -> reds
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
+  val red_projection : reds -> projection -> bool
 end
 
 module RedFlags = (struct
@@ -168,6 +169,10 @@ module RedFlags = (struct
     | DELTA -> (* Used for Rel/Var defined in context *)
 	incr_cnt red.r_delta delta
 
+  let red_projection red p = 
+    if Projection.unfolded p then true
+    else red_set red (fCONST (Projection.constant p))
+
 end : RedFlagsSig)
 
 open RedFlags
@@ -338,7 +343,7 @@ and fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCases of case_info * fconstr * fconstr * fconstr array
@@ -708,7 +713,7 @@ let rec zip m stk rem = match stk with
   let t = FCases(ci, p, m, br) in
   zip {norm=neutr m.norm; term=t} s rem
 | Zproj (i,j,cst) :: s -> 
-  zip {norm=neutr m.norm; term=FProj (cst,m)} s rem
+  zip {norm=neutr m.norm; term=FProj (Projection.make cst true,m)} s rem
 | Zfix(fx,par)::s ->
   zip fx par ((Zapp [|m|] :: s) :: rem)
 | Zshift(n)::s ->
@@ -876,7 +881,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
       (** 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
+					 term = FProj (Projection.make p true, right) }) projs in
 	argss, [Zapp hstack]	
     | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
@@ -932,11 +937,13 @@ let rec knh info m stk =
            | (None, stk') -> (m,stk'))
     | FCast(t,_,_) -> knh info t stk
     | FProj (p,c) ->
-        if red_set info.i_flags (fCONST p) then
+      let unf = Projection.unfolded p in
+        if unf || red_set info.i_flags (fCONST (Projection.constant p)) then
           (match try Some (lookup_projection p (info_env info)) with Not_found -> None with
 	  | None -> (m, stk)
 	  | Some pb ->
-	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p)
+	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
+				Projection.constant p)
 			 :: zupdate m stk))
 	else (m,stk)
 
@@ -1033,7 +1040,7 @@ let rec zip_term zfun m stk =
         let t = mkCase(ci, zfun p, m, Array.map zfun br) in
         zip_term zfun t s
     | Zproj(_,_,p)::s -> 
-        let t = mkProj (p, m) in 
+        let t = mkProj (Projection.make p true, m) in 
 	zip_term zfun t s
     | Zfix(fx,par)::s ->
         let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 1062d0e61..445fcb7bc 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -64,7 +64,10 @@ module type RedFlagsSig = sig
 
   (** Tests if a reduction kind is set *)
   val red_set : reds -> red_kind -> bool
-
+    
+  (** This tests if the projection is in unfolded state already or
+      is unfodable due to delta. *)
+  val red_projection : reds -> projection -> bool
 end
 
 module RedFlags : RedFlagsSig
@@ -113,7 +116,7 @@ type fterm =
   | FInd of inductive puniverses
   | FConstruct of constructor puniverses
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCases of case_info * fconstr * fconstr * fconstr array
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 2a13f938b..912067629 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -85,7 +85,7 @@ type ('constr, 'types) kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of constant * 'constr
+  | Proj      of projection * 'constr
 (* constr is the fixpoint of the previous type. Requires option
    -rectypes of the Caml compiler to be set *)
 type t = (t,t) kind_of_term
@@ -486,7 +486,7 @@ let compare_head_gen eq_universes eq_sorts f t1 t2 =
     Int.equal (Array.length l1) (Array.length l2) &&
       f c1 c2 && Array.equal f l1 l2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal f l1 l2
-  | Proj (p1,c1), Proj (p2,c2) -> eq_constant p1 p2 && f c1 c2
+  | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && f c1 c2
   | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
   | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
   | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2
@@ -523,7 +523,7 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
   | App (c1,l1), App (c2,l2) ->
     Int.equal (Array.length l1) (Array.length l2) &&
       eq c1 c2 && Array.equal eq l1 l2
-  | Proj (p1,c1), Proj (p2,c2) -> eq_constant p1 p2 && eq c1 c2
+  | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2
   | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
   | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
@@ -657,7 +657,7 @@ let constr_ord_int f t1 t2 =
     | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2
     | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
     | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
-    | Proj (p1,c1), Proj (p2,c2) -> (con_ord =? f) p1 p2 c1 c2
+    | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
     | Evar (e1,l1), Evar (e2,l2) ->
         (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
     | Const (c1,u1), Const (c2,u2) -> con_ord c1 c2
@@ -820,8 +820,8 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
 	(Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
       | Proj (p,c) ->
         let c, hc = sh_rec c in
-	let p' = sh_con p in
-	  (Proj (p', c), combinesmall 17 (combine (Constant.hash p') hc))
+	let p' = Projection.hashcons p in
+	  (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc))
       | Const (c,u) ->
 	let c' = sh_con c in
 	let u', hu = sh_instance u in
@@ -906,7 +906,7 @@ let rec hash t =
     | App (c,l) ->
       combinesmall 7 (combine (hash_term_array l) (hash c))
     | Proj (p,c) ->
-      combinesmall 17 (combine (Constant.hash p) (hash c))
+      combinesmall 17 (combine (Projection.hash p) (hash c))
     | Evar (e,l) ->
       combinesmall 8 (combine (Evar.hash e) (hash_term_array l))
     | Const (c,u) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 58f248b03..da7ac6a0d 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -103,7 +103,7 @@ val mkConst : constant -> constr
 val mkConstU : pconstant -> constr
 
 (** Constructs a projection application *)
-val mkProj : (constant * constr) -> constr
+val mkProj : (projection * constr) -> constr
 
 (** Inductive types *)
 
@@ -190,7 +190,7 @@ type ('constr, 'types) kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of constant * 'constr
+  | Proj      of projection * 'constr
 
 (** User view of [constr]. For [App], it is ensured there is at
    least one argument and the function is not itself an applicative
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 2d316fc1d..5f6aebc4e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -123,12 +123,13 @@ let expmod_constr cache modlist c =
 
       | Proj (p, c') ->
           (try 
-	     let p' = share_univs (ConstRef p) Univ.Instance.empty modlist in
+	     let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in
+	     let make c = Projection.make c (Projection.unfolded p) in
 	     match kind_of_term p' with
-	     | Const (p',_) -> mkProj (p', substrec c')
+	     | Const (p',_) -> mkProj (make p', substrec c')
 	     | App (f, args) -> 
 	       (match kind_of_term f with 
-	       | Const (p', _) -> mkProj (p', substrec c')
+	       | Const (p', _) -> mkProj (make p', substrec c')
 	       | _ -> assert false)
 	     | _ -> assert false
 	   with Not_found -> map_constr substrec c)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 6b0b0bdba..b331d8da7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -328,7 +328,7 @@ let template_polymorphic_pconstant (cst,u) env =
   else template_polymorphic_constant cst env
 
 let lookup_projection cst env =
-  match (lookup_constant cst env).const_proj with 
+  match (lookup_constant (Projection.constant cst) env).const_proj with 
   | Some pb -> pb
   | None -> anomaly (Pp.str "lookup_projection: constant is not a projection")
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4feec40e8..73a23ef05 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -692,14 +692,15 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params
       | Name id ->
 	let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
 	let ty = substl subst (liftn 1 j t) in
-	let term = mkProj (kn, mkRel 1) in
+	let term = mkProj (Projection.make kn true, mkRel 1) in
+	let fterm = mkProj (Projection.make kn false, mkRel 1) in
 	let compat = compat_body ty (j - 1) in
 	let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in
 	let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in
 	let body = { proj_ind = fst ind; proj_npars = nparamargs;
 		     proj_arg = i; proj_type = ty; proj_eta = etab, etat; 
 		     proj_body = compat } in
-	  (i + 1, j + 1, kn :: kns, body :: pbs, term :: subst)
+	  (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst)
       | Anonymous -> raise UndefinableExpansion
   in
   let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index cfe46152e..b65fdb3ac 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -342,13 +342,15 @@ let rec map_kn f f' c =
   let func = map_kn f f' in
     match kind_of_term c with
       | Const kn -> (try snd (f' kn) with No_subst -> c)
-      | Proj (kn,t) -> 
-          let kn' = try fst (f' (kn,Univ.Instance.empty))
-	    with No_subst -> kn 
+      | Proj (p,t) -> 
+          let p' = 
+	    try
+	      Projection.map (fun kn -> fst (f' (kn,Univ.Instance.empty))) p
+	    with No_subst -> p
 	  in
 	  let t' = func t in
-	    if kn' == kn && t' == t then c
-	    else mkProj (kn', t')
+	    if p' == p && t' == t then c
+	    else mkProj (p', t')
       | Ind ((kn,i),u) ->
 	  let kn' = f kn in
 	  if kn'==kn then c else mkIndU ((kn',i),u)
diff --git a/kernel/names.ml b/kernel/names.ml
index c76d95937..5d73bd520 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -782,7 +782,33 @@ let kn_ord = KerName.compare
 (** Compatibility layer for [Constant] *)
 
 type constant = Constant.t
-type projection = constant
+
+
+module Projection = 
+struct 
+  type t = constant * bool
+    
+  let make c b = (c, b)
+
+  let constant = fst
+  let unfolded = snd
+  let unfold (c, b as p) = if b then p else (c, true)
+  let equal (c, b) (c', b') = Constant.equal c c' && b == b'
+  let hash (c, b) = (if b then 0 else 1) + Constant.hash c
+  let hashcons (c, b as x) = 
+    let c' = hcons_con c in 
+      if c' == c then x else (c', b)
+
+  let compare (c, b) (c', b') =
+    if b == b' then Constant.CanOrd.compare c c'
+    else if b then 1 else -1
+
+  let map f (c, b as x) =
+    let c' = f c in
+      if c' == c then x else (c', b)
+end
+
+type projection = Projection.t
 
 let constant_of_kn = Constant.make1
 let constant_of_kn_equiv = Constant.make
diff --git a/kernel/names.mli b/kernel/names.mli
index 49a838ae5..893cad09d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -634,7 +634,25 @@ val kn_ord : kernel_name -> kernel_name -> int
 type constant = Constant.t
 (** @deprecated Alias type *)
 
-type projection = constant
+module Projection : sig
+  type t
+    
+  val make : constant -> bool -> t
+
+  val constant : t -> constant
+  val unfolded : t -> bool
+  val unfold : t -> t
+
+  val equal : t -> t -> bool
+  val hash : t -> int
+  val hashcons : t -> t
+
+  val compare : t -> t -> int
+    
+  val map : (constant -> constant) -> t -> t
+end
+
+type projection = Projection.t
 
 val constant_of_kn_equiv : KerName.t -> KerName.t -> constant
 (** @deprecated Same as [Constant.make] *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index bd659a471..041751ecf 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1923,7 +1923,8 @@ let rec compile_deps env sigma prefix ~interactive init t =
       comp_stack, (mind_updates, const_updates)
   | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
-      compile_deps env sigma prefix ~interactive init (mkApp (mkConst p, [|c|]))
+    let term = mkApp (mkConst (Projection.constant p), [|c|]) in
+      compile_deps env sigma prefix ~interactive init term
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 34ed33f94..ba45c329f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -586,7 +586,8 @@ let rec lambda_of_constr env sigma c =
   | Construct _ ->  lambda_of_app env sigma c empty_args
 
   | Proj (p, c) ->
-      mkLapp (Lproj (get_const_prefix !global_env p, p)) [|lambda_of_constr env sigma c|]
+    let kn = Projection.constant p in
+      mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|]
 
   | Case(ci,t,a,branches) ->  
       let (mind,i as ind) = ci.ci_ind in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 802d2b67b..9a7146890 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -275,12 +275,14 @@ let in_whnf (t,stk) =
     | FLOCKED -> assert false
 
 let unfold_projection infos p c =
-  if RedFlags.red_set infos.i_flags (RedFlags.fCONST p) then
-    (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with
-    | Some pb -> 
-      let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in
-	Some (c, s)
-    | None -> None)
+  let unf = Projection.unfolded p in
+    if unf || RedFlags.red_set infos.i_flags (RedFlags.fCONST (Projection.constant p)) then
+      (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with
+      | Some pb -> 
+	let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
+		       Projection.constant p) in
+	  Some (c, s)
+      | None -> None)
   else None
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
@@ -368,7 +370,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	| Some (def2,s2) ->
 	  eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
 	| None -> 
-          if eq_constant p1 p2 && compare_stack_shape v1 v2 then
+          if Projection.equal p1 p2 && compare_stack_shape v1 v2 then
 	    let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
 	      convert_stacks l2r infos lft1 lft2 v1 v2 u1
 	  else (* Two projections in WHNF: unfold *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 3b6b69a28..ab678666f 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -89,7 +89,7 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of constant * 'constr
+  | Proj      of projection * 'constr
 
 type values = Constr.values
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 5ff5f9ba1..28ebc41e2 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -86,7 +86,7 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of constant * 'constr
+  | Proj      of projection * 'constr
 
 type values = Constr.values
 
@@ -405,7 +405,7 @@ val mkLambda : Name.t * types * constr -> constr
 val mkLetIn : Name.t * constr * types * constr -> constr
 val mkApp : constr * constr array -> constr
 val mkConst : constant -> constr
-val mkProj : (constant * constr) -> constr
+val mkProj : projection * constr -> constr
 val mkInd : inductive -> constr
 val mkConstruct : constructor -> constr
 val mkConstU : constant puniverses -> constr
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index fa7dd105c..5421020d2 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -184,7 +184,8 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) args =
 let judge_of_constant env cst =
   judge_of_constant_knowing_parameters env cst [||]
 
-let type_of_projection env (cst,u) =
+let type_of_projection env (p,u) =
+  let cst = Projection.constant p in
   let cb = lookup_constant cst env in
   match cb.const_proj with
   | Some pb -> 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 976380ede..3f9345ff8 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -203,7 +203,9 @@ let rec conv_eq env pb t1 t2 cu =
 	else raise NotConvertible
     | Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu
     | Proj (p1,c1), Proj (p2,c2) ->
-	if eq_constant p1 p2 then conv_eq env pb c1 c2 cu else raise NotConvertible
+	if eq_constant (Projection.constant p1) (Projection.constant p2) then
+	  conv_eq env pb c1 c2 cu 
+	else raise NotConvertible
     | Ind c1, Ind c2 ->
        eq_puniverses eq_ind c1 c2 cu
     | Construct c1, Construct c2 ->