mutable relevance marks in fconstr

3 files changed, 176 insertions, 102 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 405d0b4223..922fce957e 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -29,6 +29,7 @@ open Pp
 open Names
 open Constr
 open Declarations
+open Context
 open Environ
 open Vars
 open Esubst
@@ -282,12 +283,63 @@ let assoc_defined id env = match Environ.lookup_named id env with
 type red_state = Norm | Cstr | Whnf | Red
 
 let neutr = function
-  | (Whnf|Norm) -> Whnf
-  | (Red|Cstr) -> Red
+  | Whnf|Norm -> Whnf
+  | Red|Cstr -> Red
+
+type optrel = Unknown | KnownR | KnownI
+
+let opt_of_rel = function
+  | Sorts.Relevant -> KnownR
+  | Sorts.Irrelevant -> KnownI
+
+module Mark : sig
+
+  type t
+
+  val mark : red_state -> optrel -> t
+  val relevance : t -> optrel
+  val red_state : t -> red_state
+
+  val neutr : t -> t
+
+  val set_norm : t -> t
+
+end = struct
+  type t = int
+
+  let of_state = function
+    | Norm -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11
+
+  let of_relevance = function
+    | Unknown -> 0
+    | KnownR -> 0b01
+    | KnownI -> 0b10
+
+  let mark state relevance = (of_state state) * 4 + (of_relevance relevance)
+
+  let relevance x = match x land 0b11 with
+    | 0b00 -> Unknown
+    | 0b01 -> KnownR
+    | 0b10 -> KnownI
+    | _ -> assert false
+
+  let red_state x = match x land 0b1100 with
+    | 0b0000 -> Norm
+    | 0b0100 -> Cstr
+    | 0b1000 -> Whnf
+    | 0b1100 -> Red
+    | _ -> assert false
+
+  let neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *)
+
+  let set_norm x = x land 0b0011
+end
+let mark = Mark.mark
 
 type fconstr = {
-  mutable norm: red_state;
-  mutable term: fterm }
+  mutable mark : Mark.t;
+  mutable term: fterm;
+}
 
 and fterm =
   | FRel of int
@@ -310,20 +362,20 @@ and fterm =
   | FLOCKED
 
 let fterm_of v = v.term
-let set_norm v = v.norm <- Norm
-let is_val v = match v.norm with Norm -> true | Cstr | Whnf | Red -> false
+let set_norm v = v.mark <- Mark.set_norm v.mark
+let is_val v = match Mark.red_state v.mark with Norm -> true | Cstr | Whnf | Red -> false
 
-let mk_atom c = {norm=Norm;term=FAtom c}
-let mk_red f = {norm=Red;term=f}
+let mk_atom c = {mark=mark Norm Unknown;term=FAtom c}
+let mk_red f = {mark=mark Red Unknown;term=f}
 
 (* Could issue a warning if no is still Red, pointing out that we loose
    sharing. *)
-let update ~share v1 no t =
+let update ~share v1 mark t =
   if share then
-    (v1.norm <- no;
+    (v1.mark <- mark;
      v1.term <- t;
      v1)
-  else {norm=no;term=t}
+  else {mark;term=t;}
 
 (** Reduction cache *)
 
@@ -383,16 +435,19 @@ let rec stack_args_size = function
    lft_fconstr always create a new cell, while lift_fconstr avoids it
    when the lift is 0. *)
 let rec lft_fconstr n ft =
+  let r = Mark.relevance ft.mark in
   match ft.term with
     | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _) -> ft
-    | FRel i -> {norm=Norm;term=FRel(i+n)}
-    | FLambda(k,tys,f,e) -> {norm=Cstr; term=FLambda(k,tys,f,subs_shft(n,e))}
-    | FFix(fx,e) -> {norm=Cstr; term=FFix(fx,subs_shft(n,e))}
-    | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))}
+    | FRel i -> {mark=mark Norm r;term=FRel(i+n)}
+    | FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))}
+    | FFix(fx,e) ->
+      {mark=mark Cstr r; term=FFix(fx,subs_shft(n,e))}
+    | FCoFix(cfx,e) ->
+      {mark=mark Cstr r; term=FCoFix(cfx,subs_shft(n,e))}
     | FLIFT(k,m) -> lft_fconstr (n+k) m
     | FLOCKED -> assert false
     | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _
-      | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)}
+      | FLetIn _ | FEvar _ | FCLOS _ -> {mark=ft.mark; term=FLIFT(n,ft)}
 let lift_fconstr k f =
   if Int.equal k 0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
@@ -401,9 +456,9 @@ let lift_fconstr_vect k v =
 let clos_rel e i =
   match expand_rel i e with
     | Inl(n,mt) -> lift_fconstr n mt
-    | Inr(k,None) -> {norm=Norm; term= FRel k}
+    | Inr(k,None) -> {mark=mark Norm Unknown; term= FRel k}
     | Inr(k,Some p) ->
-        lift_fconstr (k-p) {norm=Red;term=FFlex(RelKey p)}
+        lift_fconstr (k-p) {mark=mark Red Unknown;term=FFlex(RelKey p)}
 
 (* since the head may be reducible, we might introduce lifts of 0 *)
 let compact_stack head stk =
@@ -414,7 +469,7 @@ let compact_stack head stk =
            lost by the update operation *)
         let h' = lft_fconstr depth head in
         (** The stack contains [Zupdate] marks only if in sharing mode *)
-        let _ = update ~share:true m h'.norm h'.term in
+        let _ = update ~share:true m h'.mark h'.term in
         strip_rec depth s
     | ((ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zprimitive _) :: _ | []) as stk -> zshift depth stk
   in
@@ -423,7 +478,7 @@ let compact_stack head stk =
 (* Put an update mark in the stack, only if needed *)
 let zupdate info m s =
   let share = info.i_cache.i_share in
-  if share && begin match m.norm with Red -> true | Norm | Whnf | Cstr -> false end
+  if share && begin match Mark.red_state m.mark with Red -> true  | Norm | Whnf | Cstr -> false end
   then
     let s' = compact_stack m s in
     let _ = m.term <- FLOCKED in
@@ -436,25 +491,25 @@ let mk_lambda env t =
 
 let destFLambda clos_fun t =
   match [@ocaml.warning "-4"] t.term with
-  | FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b)
-  | FLambda(n,(na,ty)::tys,b,e) ->
-    (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)})
-  | _ -> assert false
-(* t must be a FLambda and binding list cannot be empty *)
+      FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b)
+    | FLambda(n,(na,ty)::tys,b,e) ->
+        (na,clos_fun e ty,{mark=t.mark;term=FLambda(n-1,tys,b,subs_lift e)})
+    | _ -> assert false
+        (* t must be a FLambda and binding list cannot be empty *)
 
 (* Optimization: do not enclose variables in a closure.
    Makes variable access much faster *)
 let mk_clos e t =
   match kind t with
     | Rel i -> clos_rel e i
-    | Var x -> { norm = Red; term = FFlex (VarKey x) }
-    | Const c -> { norm = Red; term = FFlex (ConstKey c) }
-    | Meta _ | Sort _ ->  { norm = Norm; term = FAtom t }
-    | Ind kn -> { norm = Norm; term = FInd kn }
-    | Construct kn -> { norm = Cstr; term = FConstruct kn }
-    | Int i -> {norm = Cstr; term = FInt i}
+    | Var x -> {mark = mark Red Unknown; term = FFlex (VarKey x) }
+    | Const c -> {mark = mark Red Unknown; term = FFlex (ConstKey c) }
+    | Meta _ | Sort _ ->  {mark = mark Norm KnownR; term = FAtom t }
+    | Ind kn -> {mark = mark Norm KnownR; term = FInd kn }
+    | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn }
+    | Int i -> {mark = mark Cstr Unknown; term = FInt i}
     | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
-        {norm = Red; term = FCLOS(t,e)}
+        {mark = mark Red Unknown; term = FCLOS(t,e)}
 
 let inject c = mk_clos (subs_id 0) c
 
@@ -606,23 +661,25 @@ let rec fstrong unfreeze_fun lfts v =
 let rec zip m stk =
   match stk with
     | [] -> m
-    | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s
+    | Zapp args :: s -> zip {mark=Mark.neutr m.mark; term=FApp(m, args)} s
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
-        zip {norm=neutr m.norm; term=t} s
+        let mark = mark (neutr (Mark.red_state m.mark)) Unknown  in
+        zip {mark; term=t} s
     | Zproj p :: s ->
-        zip {norm=neutr m.norm; term=FProj(Projection.make p true,m)} s
+        let mark = mark (neutr (Mark.red_state m.mark)) Unknown in
+        zip {mark; term=FProj(Projection.make p true,m)} s
     | Zfix(fx,par)::s ->
         zip fx (par @ append_stack [|m|] s)
     | Zshift(n)::s ->
         zip (lift_fconstr n m) s
     | Zupdate(rf)::s ->
       (** The stack contains [Zupdate] marks only if in sharing mode *)
-        zip (update ~share:true rf m.norm m.term) s
+        zip (update ~share:true rf m.mark m.term) s
     | Zprimitive(_op,c,rargs,kargs)::s ->
       let args = List.rev_append rargs (m::List.map snd kargs) in
-      let f = {norm = Red;term = FFlex (ConstKey c)} in
-      zip {norm=neutr m.norm; term = FApp (f, Array.of_list args)} s
+      let f = {mark = mark Red Unknown;term = FFlex (ConstKey c)} in
+      zip {mark=mark (neutr (Mark.red_state m.mark)) KnownR; term = FApp (f, Array.of_list args)} s
 
 let fapp_stack (m,stk) = zip m stk
 
@@ -640,21 +697,21 @@ let strip_update_shift_app_red head stk =
         strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s
     | (Zapp args :: s) ->
         strip_rec (Zapp args :: rstk)
-          {norm=h.norm;term=FApp(h,args)} depth s
+          {mark=h.mark;term=FApp(h,args)} depth s
     | Zupdate(m)::s ->
       (** The stack contains [Zupdate] marks only if in sharing mode *)
-        strip_rec rstk (update ~share:true m h.norm h.term) depth s
+        strip_rec rstk (update ~share:true m h.mark h.term) depth s
     | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk ->
       (depth,List.rev rstk, stk)
   in
   strip_rec [] head 0 stk
 
 let strip_update_shift_app head stack =
-  assert (match head.norm with Red -> false | Norm | Cstr | Whnf -> true);
+  assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true);
   strip_update_shift_app_red head stack
 
 let get_nth_arg head n stk =
-  assert (match head.norm with Red -> false | Norm | Cstr | Whnf -> true);
+  assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true);
   let rec strip_rec rstk h n = function
     | Zshift(k) as e :: s ->
         strip_rec (e::rstk) (lift_fconstr k h) n s
@@ -662,7 +719,7 @@ let get_nth_arg head n stk =
         let q = Array.length args in
         if n >= q
         then
-          strip_rec (Zapp args::rstk) {norm=h.norm;term=FApp(h,args)} (n-q) s'
+          strip_rec (Zapp args::rstk) {mark=h.mark;term=FApp(h,args)} (n-q) s'
         else
           let bef = Array.sub args 0 n in
           let aft = Array.sub args (n+1) (q-n-1) in
@@ -671,7 +728,7 @@ let get_nth_arg head n stk =
           (Some (stk', args.(n)), append_stack aft s')
     | Zupdate(m)::s ->
         (** The stack contains [Zupdate] mark only if in sharing mode *)
-        strip_rec rstk (update ~share:true m h.norm h.term) n s
+        strip_rec rstk (update ~share:true m h.mark h.term) n s
     | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as s -> (None, List.rev rstk @ s) in
   strip_rec [] head n stk
 
@@ -680,7 +737,7 @@ let get_nth_arg head n stk =
 let rec get_args n tys f e = function
     | Zupdate r :: s ->
         (** The stack contains [Zupdate] mark only if in sharing mode *)
-        let _hd = update ~share:true r Cstr (FLambda(n,tys,f,e)) in
+        let _hd = update ~share:true r (mark Cstr (Mark.relevance r.mark)) (FLambda(n,tys,f,e)) in
         get_args n tys f e s
     | Zshift k :: s ->
         get_args n tys f (subs_shft (k,e)) s
@@ -695,7 +752,7 @@ let rec get_args n tys f e = function
           let etys = List.skipn na tys in
           get_args (n-na) etys f (subs_cons(l,e)) s
     | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk ->
-      (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
+      (Inr {mark=mark Cstr Unknown;term=FLambda(n,tys,f,e)}, stk)
 
 (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
 let rec eta_expand_stack = function
@@ -703,7 +760,7 @@ let rec eta_expand_stack = function
         | Zshift _ | Zupdate _ | Zprimitive _ as e) :: s ->
       e :: eta_expand_stack s
   | [] ->
-      [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
+      [Zshift 1; Zapp [|{mark=mark Norm Unknown; term= FRel 1}|]]
 
 (* Get the arguments of a native operator *)
 let rec skip_native_args rargs nargs =
@@ -731,12 +788,12 @@ let get_native_args op c stk =
           (skip_native_args [] (List.rev rnargs),
            Zapp (Array.of_list eargs) :: s')
         | rnargs, kargs, _ ->
-          strip_rec rnargs {norm = h.norm;term=FApp(h, args)} depth kargs s'
+          strip_rec rnargs {mark = h.mark;term=FApp(h, args)} depth kargs s'
       end
     | Zupdate(m) :: s ->
-      strip_rec rnargs (update ~share:true m h.norm h.term) depth  kargs s
+      strip_rec rnargs (update ~share:true m h.mark h.term) depth  kargs s
     | (Zprimitive _ | ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> assert false
-  in strip_rec [] {norm = Red;term = FFlex(ConstKey c)} 0 kargs stk
+  in strip_rec [] {mark = mark Red Unknown;term = FFlex(ConstKey c)} 0 kargs stk
 
 let get_native_args1 op c stk =
   match get_native_args op c stk with
@@ -807,7 +864,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 *)
+        { mark = mark Red Unknown; (* right can't be a constructor though *)
           term = FProj (Projection.make p true, right) })
         projs
     in
@@ -835,13 +892,15 @@ let rec project_nth_arg n = function
 let contract_fix_vect fix =
   let (thisbody, make_body, env, nfix) =
     match [@ocaml.warning "-4"] fix with
-      | FFix (((reci,i),(_,_,bds as rdcl)),env) ->
+      | FFix (((reci,i),(nas,_,bds as rdcl)),env) ->
           (bds.(i),
-	   (fun j -> { norm = Cstr; term = FFix (((reci,j),rdcl),env) }),
+           (fun j -> { mark = mark Cstr (opt_of_rel nas.(j).binder_relevance);
+                       term = FFix (((reci,j),rdcl),env) }),
 	   env, Array.length bds)
-      | FCoFix ((i,(_,_,bds as rdcl)),env) ->
+      | FCoFix ((i,(nas,_,bds as rdcl)),env) ->
           (bds.(i),
-	   (fun j -> { norm = Cstr; term = FCoFix ((j,rdcl),env) }),
+           (fun j -> { mark = mark Cstr (opt_of_rel nas.(j).binder_relevance);
+                       term = FCoFix ((j,rdcl),env) }),
 	   env, Array.length bds)
       | _ -> assert false
   in
@@ -886,18 +945,18 @@ and knht info e t stk =
         knht info e a (append_stack (mk_clos_vect e b) stk)
     | Case(ci,p,t,br) ->
         knht info e t (ZcaseT(ci, p, br, e)::stk)
-    | Fix fx -> knh info { norm = Cstr; term = FFix (fx, e) } stk
+    | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk
     | Cast(a,_,_) -> knht info e a stk
     | Rel n -> knh info (clos_rel e n) stk
-    | Proj (p, c) -> knh info { norm = Red; term = FProj (p, mk_clos e c) } stk
+    | Proj (p, c) -> knh info { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk
     | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _) -> (mk_clos e t, stk)
-    | CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk
-    | Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk
+    | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk
+    | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk
     | Prod (n, t, c) ->
-      { norm = Whnf; term = FProd (n, mk_clos e t, c, e) }, stk
+      { mark = mark Whnf KnownR; term = FProd (n, mk_clos e t, c, e) }, stk
     | LetIn (n,b,t,c) ->
-      { norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk
-    | Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk
+      { mark = mark Red Unknown; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk
+    | Evar ev -> { mark = mark Red Unknown; term = FEvar (ev, e) }, stk
 
 let inject c = mk_clos (subs_id 0) c
 
@@ -919,7 +978,7 @@ module FNativeEntries =
       | FInt i -> i
       | _ -> raise Primred.NativeDestKO
 
-    let dummy = {norm = Norm; term = FRel 0}
+    let dummy = {mark = mark Norm KnownR; term = FRel 0}
 
     let current_retro = ref Retroknowledge.empty
     let defined_int = ref false
@@ -929,7 +988,7 @@ module FNativeEntries =
       match retro.Retroknowledge.retro_int63 with
       | Some c ->
         defined_int := true;
-        fint := { norm = Norm; term = FFlex (ConstKey (Univ.in_punivs c)) }
+        fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
       | None -> defined_int := false
 
     let defined_bool = ref false
@@ -940,8 +999,8 @@ module FNativeEntries =
       match retro.Retroknowledge.retro_bool with
       | Some (ct,cf) ->
         defined_bool := true;
-        ftrue := { norm = Cstr; term = FConstruct (Univ.in_punivs ct) };
-        ffalse := { norm = Cstr; term = FConstruct (Univ.in_punivs cf) }
+        ftrue := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs ct) };
+        ffalse := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cf) }
       | None -> defined_bool :=false
 
     let defined_carry = ref false
@@ -952,8 +1011,8 @@ module FNativeEntries =
       match retro.Retroknowledge.retro_carry with
       | Some(c0,c1) ->
         defined_carry := true;
-        fC0 := { norm = Cstr; term = FConstruct (Univ.in_punivs c0) };
-        fC1 := { norm = Cstr; term = FConstruct (Univ.in_punivs c1) }
+        fC0 := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs c0) };
+        fC1 := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs c1) }
       | None -> defined_carry := false
 
     let defined_pair = ref false
@@ -963,7 +1022,7 @@ module FNativeEntries =
       match retro.Retroknowledge.retro_pair with
       | Some c ->
         defined_pair := true;
-        fPair := { norm = Cstr; term = FConstruct (Univ.in_punivs c) }
+        fPair := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs c) }
       | None -> defined_pair := false
 
     let defined_cmp = ref false
@@ -975,9 +1034,9 @@ module FNativeEntries =
       match retro.Retroknowledge.retro_cmp with
       | Some (cEq, cLt, cGt) ->
         defined_cmp := true;
-        fEq := { norm = Cstr; term = FConstruct (Univ.in_punivs cEq) };
-        fLt := { norm = Cstr; term = FConstruct (Univ.in_punivs cLt) };
-        fGt := { norm = Cstr; term = FConstruct (Univ.in_punivs cGt) }
+        fEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cEq) };
+        fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) };
+        fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) }
       | None -> defined_cmp := false
 
     let defined_refl = ref false
@@ -988,7 +1047,7 @@ module FNativeEntries =
       match retro.Retroknowledge.retro_refl with
       | Some crefl ->
         defined_refl := true;
-        frefl := { norm = Cstr; term = FConstruct (Univ.in_punivs crefl) }
+        frefl := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs crefl) }
       | None -> defined_refl := false
 
     let init env =
@@ -1025,7 +1084,7 @@ module FNativeEntries =
 
     let mkInt env i =
       check_int env;
-      { norm = Norm; term = FInt i }
+      { mark = mark Norm KnownR; term = FInt i }
 
     let mkBool env b =
       check_bool env;
@@ -1033,12 +1092,12 @@ module FNativeEntries =
 
     let mkCarry env b e =
       check_carry env;
-      {norm = Cstr;
+      {mark = mark Cstr KnownR;
        term = FApp ((if b then !fC1 else !fC0),[|!fint;e|])}
 
     let mkIntPair env e1 e2 =
       check_pair env;
-      { norm = Cstr; term = FApp(!fPair, [|!fint;!fint;e1;e2|]) }
+      { mark = mark Cstr KnownR; term = FApp(!fPair, [|!fint;!fint;e1;e2|]) }
 
     let mkLt env =
       check_cmp env;
@@ -1124,8 +1183,8 @@ let rec knr info tab m stk =
            begin match FredNative.red_prim (info_env info) () op args with
              | Some m -> kni info tab m s
              | None ->
-               let f = {norm = Whnf; term = FFlex (ConstKey c)} in
-               let m = {norm = Whnf; term = FApp(f,args)} in
+               let f = {mark = mark Whnf KnownR; term = FFlex (ConstKey c)} in
+               let m = {mark = mark Whnf KnownR; term = FApp(f,args)} in
                (m,s)
            end
          | (kd,a)::nargs ->
@@ -1232,7 +1291,7 @@ let whd_val info tab v =
 let norm_val info tab v =
   with_stats (lazy (kl info tab v))
 
-let whd_stack infos tab m stk = match m.norm with
+let whd_stack infos tab m stk = match Mark.red_state m.mark with
 | Whnf | Norm ->
   (** No need to perform [kni] nor to unlock updates because
       every head subterm of [m] is [Whnf] or [Norm] *)
@@ -1269,3 +1328,6 @@ let unfold_reference info tab key =
       ref_value_cache info tab key
     else Undef None
   | RelKey _ -> ref_value_cache info tab key
+
+let relevance_of f = Mark.relevance f.mark
+let set_relevance r f = f.mark <- Mark.mark (Mark.red_state f.mark) (opt_of_rel r)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 2852d48a5d..b1b69dded8 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -167,6 +167,11 @@ val term_of_fconstr : fconstr -> constr
 val destFLambda :
   (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t Context.binder_annot * fconstr * fconstr
 
+type optrel = Unknown | KnownR | KnownI
+
+val relevance_of : fconstr -> optrel
+val set_relevance : Sorts.relevance -> fconstr -> unit
+
 (** Global and local constant cache *)
 type clos_infos
 type clos_tab
diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml
index 61fabfee9f..204dec3eda 100644
--- a/kernel/retypeops.ml
+++ b/kernel/retypeops.ml
@@ -50,30 +50,37 @@ let relevance_of_flex env extra lft = function
 
 let rec relevance_of_fterm env extra lft f =
   let open CClosure in
-  match fterm_of f with
-  | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)
-  | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c
-  | FFlex key -> relevance_of_flex env extra lft key
-  | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *)
-  | FConstruct (c,_) -> relevance_of_constructor env c
-  | FApp (f, _) -> relevance_of_fterm env extra lft f
-  | FProj (p, _) -> relevance_of_projection env p
-  | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance
-  | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance
-  | FCaseT (ci, _, _, _, _) -> ci.ci_relevance
-  | FLambda (len, tys, bdy, e) ->
-    let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in
-    let lft = Esubst.el_liftn len lft in
-    relevance_of_term_extra env extra lft e bdy
-  | FLetIn (x, _, _, bdy, e) ->
-    relevance_of_term_extra env (x.binder_relevance :: extra)
-      (Esubst.el_lift lft) (Esubst.subs_lift e) bdy
-  | FInt _ -> Sorts.Relevant
-  | FLIFT (k, f) -> relevance_of_fterm env extra (Esubst.el_shft k lft) f
-  | FCLOS (c, e) -> relevance_of_term_extra env extra lft e c
+  match CClosure.relevance_of f with
+  | KnownR -> Sorts.Relevant
+  | KnownI -> Sorts.Irrelevant
+  | Unknown ->
+    let r = match fterm_of f with
+      | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)
+      | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c
+      | FFlex key -> relevance_of_flex env extra lft key
+      | FInt _ -> Sorts.Relevant
+      | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *)
+      | FConstruct (c,_) -> relevance_of_constructor env c
+      | FApp (f, _) -> relevance_of_fterm env extra lft f
+      | FProj (p, _) -> relevance_of_projection env p
+      | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance
+      | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance
+      | FCaseT (ci, _, _, _, _) -> ci.ci_relevance
+      | FLambda (len, tys, bdy, e) ->
+        let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in
+        let lft = Esubst.el_liftn len lft in
+        relevance_of_term_extra env extra lft e bdy
+      | FLetIn (x, _, _, bdy, e) ->
+        relevance_of_term_extra env (x.binder_relevance :: extra)
+          (Esubst.el_lift lft) (Esubst.subs_lift e) bdy
+      | FLIFT (k, f) -> relevance_of_fterm env extra (Esubst.el_shft k lft) f
+      | FCLOS (c, e) -> relevance_of_term_extra env extra lft e c
 
-  | FEvar (_, _) -> Sorts.Relevant (* let's assume evars are relevant for now *)
-  | FLOCKED -> assert false
+      | FEvar (_, _) -> Sorts.Relevant (* let's assume evars are relevant for now *)
+      | FLOCKED -> assert false
+    in
+    CClosure.set_relevance r f;
+    r
 
 and relevance_of_term_extra env extra lft subs c =
   match kind c with