Experiment to cancel the difference between folded and unfolded proje…

…ctions.

To be continued when the goal is clearer (remove unfold, check
reduction, add a table to make proj opaque, ... ?).

kernel/names.ml

@@ -931,7 +931,7 @@ struct
 
   type t = Repr.t * bool
 
-  let make c b = (c, b)
+  let make c _ = (c, true)
 
   let mind (c,_) = Repr.mind c
   let inductive (c,_) = Repr.inductive c
@@ -940,7 +940,7 @@ struct
   let constant (c,_) = Repr.constant c
   let label (c,_) = Repr.label c
   let repr = fst
-  let unfolded = snd
+  let unfolded _ = true
   let unfold (c, b as p) = if b then p else (c, true)
 
   let equal (c, b) (c', b') = Repr.equal c c' && b == b'

pretyping/constr_matching.ml

@@ -299,23 +299,22 @@ let matches_core env sigma allow_bound_rels
             Array.fold_left2 (sorec ctx env) subst args1 args22
           else (* Might be a projection on the right *)
             match EConstr.kind sigma c2 with
-            | Proj (pr, c) when not (Projection.unfolded pr) ->
+            | Proj (pr, c) ->
               (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
                      sorec ctx env subst p term
                with Retyping.RetypeError _ -> raise PatternMatchingFailure)
             | _ -> raise PatternMatchingFailure)
 
       | PApp (c1,arg1), App (c2,arg2) ->
         (match c1, EConstr.kind sigma c2 with
-        | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Environ.QConstant.equal env r (Projection.constant pr))
-            || Projection.unfolded pr ->
+        | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Environ.QConstant.equal env r (Projection.constant pr)) ->
           raise PatternMatchingFailure
         | PProj (pr1,c1), Proj (pr,c) ->
           if Environ.QProjection.equal env pr1 pr then
             try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c) arg1 arg2
             with Invalid_argument _ -> raise PatternMatchingFailure
           else raise PatternMatchingFailure
-        | _, Proj (pr,c) when not (Projection.unfolded pr) ->
+        | _, Proj (pr,c) ->
           (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
                  sorec ctx env subst p term
            with Retyping.RetypeError _ -> raise PatternMatchingFailure)
@@ -324,7 +323,7 @@ let matches_core env sigma allow_bound_rels
           with Invalid_argument _ -> raise PatternMatchingFailure)
 
       | PApp (PRef (GlobRef.ConstRef c1), _), Proj (pr, c2)
-        when Projection.unfolded pr || not (Environ.QConstant.equal env c1 (Projection.constant pr)) ->
+        when not (Environ.QConstant.equal env c1 (Projection.constant pr)) ->
         raise PatternMatchingFailure
 
       | PApp (c, args), Proj (pr, c2) ->

pretyping/evarconv.ml

@@ -71,12 +71,6 @@ let coq_unit_judge env sigma =
     sigma, make_judge c t
   | exception _ -> sigma, unit_judge_fallback
 
-let unfold_projection env evd ts p c =
-  let cst = Projection.constant p in
-    if TransparentState.is_transparent_constant ts cst then
-      Some (mkProj (Projection.unfold p, c))
-    else None
-
 let eval_flexible_term ts env evd c =
   match EConstr.kind evd c with
   | Const (c, u) ->
@@ -96,9 +90,6 @@ let eval_flexible_term ts env evd c =
        with Not_found -> None)
   | LetIn (_,b,_,c) -> Some (subst1 b c)
   | Lambda _ -> Some c
-  | Proj (p, c) ->
-    if Projection.unfolded p then assert false
-    else unfold_projection env evd ts p c
   | _ -> assert false
 
 type flex_kind_of_term =
@@ -110,7 +101,7 @@ let has_arg s = Option.has_some (Stack.strip_n_app 0 s)
 
 let flex_kind_of_term flags env evd c sk =
   match EConstr.kind evd c with
-    | LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
+    | LetIn _ | Rel _ | Const _ | Var _ ->
       Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term flags.open_ts env evd c)
     | Lambda _ when has_arg sk ->
        if flags.modulo_betaiota then MaybeFlexible c
@@ -121,7 +112,7 @@ let flex_kind_of_term flags env evd c sk =
     | Construct _ | CoFix _ (* Incorrect: should check only app in sk *) -> Rigid
     | Meta _ -> Rigid
     | Fix _ -> Rigid (* happens when the fixpoint is partially applied (should check it?) *)
-    | Cast _ | App _ | Case _ -> assert false
+    | Cast _ | App _ | Case _ | Proj _ -> assert false
 
 let apprec_nohdbeta flags env evd c =
   let (t,sk as appr) = Reductionops.whd_nored_state env evd (c, []) in
@@ -958,7 +949,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
              (whd_betaiota_deltazeta_for_iota_state
                       flags.open_ts env i (subst1 b c, args))
             | Fix _ -> true (* Partially applied fix can be the result of a whd call *)
-            | Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args
+            | Proj (p, _) -> Stack.not_purely_applicative args (* ?? *)
             | Case _ | App _| Cast _ -> assert false in
           let rhs_is_stuck_and_unnamed () =
             let applicative_stack = fst (Stack.strip_app sk2) in

pretyping/tacred.ml

@@ -584,10 +584,6 @@ let match_eval_ref_value env sigma constr stack =
       Some (EConstr.of_constr (constant_value_in env (sp, u)))
     else
       None
-  | Proj (p, c) when not (Projection.unfolded p) ->
-     if is_evaluable env (EvalConstRef (Projection.constant p)) then
-       Some (mkProj (Projection.unfold p, c))
-     else None
   | Var id when is_evaluable env (EvalVarRef id) ->
      env |> lookup_named id |> NamedDecl.get_value
   | Rel n ->
@@ -774,12 +770,11 @@ and whd_simpl_stack env sigma =
 
       | Proj (p, c) ->
         (try
-           let unf = Projection.unfolded p in
-           if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then
+           if is_evaluable env (EvalConstRef (Projection.constant p)) then
              let npars = Projection.npars p in
-             (match unf, get (GlobRef.ConstRef (Projection.constant p)) with
-              | false, Some NeverUnfold -> s'
-              | false, Some (UnfoldWhen { recargs } | UnfoldWhenNoMatch { recargs })
+             (match get (GlobRef.ConstRef (Projection.constant p)) with
+              | Some NeverUnfold -> s'
+              | Some (UnfoldWhen { recargs } | UnfoldWhenNoMatch { recargs })
                 when not (List.is_empty recargs) ->
                 let l' = List.map_filter (fun i ->
                     let idx = (i - (npars + 1)) in
@@ -791,11 +786,13 @@ and whd_simpl_stack env sigma =
                  | Reduced s' -> redrec s'
                  | NotReducible -> s')
               | _ ->
-                match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with
-                | Reduced s' -> redrec s'
-                            | NotReducible -> s')
-                 else s'
-               with Redelimination -> s')
+                (match reduce_projection env sigma p ~npars
+                         (whd_construct_stack env sigma c) stack
+                 with
+                 | Reduced s' -> redrec s'
+                 | NotReducible -> s'))
+           else s'
+         with Redelimination -> s')
 
       | Const (cst, _) when is_primitive env cst ->
          (try

pretyping/unification.ml

@@ -518,8 +518,7 @@ let key_of env sigma b flags f =
   | Var id when is_transparent env (VarKey id) &&
       TransparentState.is_transparent_variable flags.modulo_delta id ->
     Some (IsKey (VarKey id))
-  | Proj (p, c) when Names.Projection.unfolded p
-    || (is_transparent env (ConstKey (Projection.constant p)) &&
+  | Proj (p, c) when (is_transparent env (ConstKey (Projection.constant p)) &&
        (TransparentState.is_transparent_constant flags.modulo_delta (Projection.constant p))) ->
     Some (IsProj (p, c))
   | _ -> None
@@ -547,10 +546,10 @@ let oracle_order env cf1 cf2 =
         match k1, k2 with
         | IsProj (p, _), IsKey (ConstKey (p',_))
           when Environ.QConstant.equal env (Projection.constant p) p' ->
-          Some (not (Projection.unfolded p))
+          Some false
         | IsKey (ConstKey (p,_)), IsProj (p', _)
           when Environ.QConstant.equal env p (Projection.constant p') ->
-          Some (Projection.unfolded p')
+          Some true
         | _ ->
           Some (Conv_oracle.oracle_order (fun x -> x)
                   (Environ.oracle env) false (translate_key k1) (translate_key k2))
@@ -942,7 +941,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       in
       let expand_proj c c' l =
         match EConstr.kind sigma c with
-        | Proj (p, t) when not (Projection.unfolded p) && needs_expansion p c' ->
+        | Proj (p, t) when needs_expansion p c' ->
           (try destApp sigma (Retyping.expand_projection curenv sigma p t (Array.to_list l))
            with RetypeError _ -> (* Unification can be called on ill-typed terms, due
                                      to FO and eta in particular, fail gracefully in that case *)