Remove REVERTcast

checker/values.ml

@@ -124,7 +124,7 @@ let v_caseinfo =
   let v_cprint = v_tuple "case_printing" [|v_boollist;Array v_boollist;v_cstyle|] in
   v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_relevance;v_cprint|]
 
-let v_cast = v_enum "cast_kind" 4
+let v_cast = v_enum "cast_kind" 3
 
 let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|]
 let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]

dev/ci/user-overlays/14773-SkySkimmer-revertcast.sh

@@ -0,0 +1,13 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi revertcast 14773
+
+overlay quickchick https://github.com/SkySkimmer/QuickChick revertcast 14773
+
+overlay aac_tactics https://github.com/SkySkimmer/aac-tactics revertcast 14773
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations revertcast 14773
+
+overlay metacoq https://github.com/SkySkimmer/metacoq revertcast 14773
+
+overlay gappa https://gitlab.inria.fr/ggilbert/gappa revertcast 14773
+
+overlay relation_algebra https://github.com/SkySkimmer/relation-algebra revertcast 14773

dev/top_printers.ml

@@ -277,7 +277,6 @@ let cast_kind_display k =
   match k with
   | VMcast -> "VMcast"
   | DEFAULTcast -> "DEFAULTcast"
-  | REVERTcast -> "REVERTcast"
   | NATIVEcast -> "NATIVEcast"
 
 let constr_display csr =

interp/constrexpr.ml

@@ -128,7 +128,7 @@ and constr_expr_r =
   | CPatVar of Pattern.patvar
   | CEvar   of Glob_term.existential_name CAst.t * (lident * constr_expr) list
   | CSort   of sort_expr
-  | CCast   of constr_expr * constr_expr Glob_term.cast_type
+  | CCast   of constr_expr * Constr.cast_kind * constr_expr
   | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
   | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
   | CPrim of prim_token

interp/constrexpr_ops.ml

@@ -178,14 +178,6 @@ module EqGen (A:sig val constr_expr_eq : constr_expr -> constr_expr -> bool end)
   let instance_eq (x1,c1) (x2,c2) =
     Id.equal x1.CAst.v x2.CAst.v && constr_expr_eq c1 c2
 
-  let cast_expr_eq c1 c2 = match c1, c2 with
-    | CastConv t1, CastConv t2
-    | CastVM t1, CastVM t2
-    | CastNative t1, CastNative t2 -> constr_expr_eq t1 t2
-    | CastConv _, _
-    | CastVM _, _
-    | CastNative _, _ -> false
-
   let constr_expr_eq e1 e2 =
     if CAst.(e1.v == e2.v) then true
     else match CAst.(e1.v, e2.v) with
@@ -249,8 +241,8 @@ module EqGen (A:sig val constr_expr_eq : constr_expr -> constr_expr -> bool end)
         Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2
       | CSort s1, CSort s2 ->
         sort_expr_eq s1 s2
-      | CCast(t1,c1), CCast(t2,c2) ->
-        constr_expr_eq t1 t2 && cast_expr_eq c1 c2
+      | CCast(c1,k1,t1), CCast(c2,k2,t2) ->
+        constr_expr_eq c1 c2 && Glob_ops.cast_kind_eq k1 k2 && constr_expr_eq t1 t2
       | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
         Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
         notation_eq n1 n2 &&
@@ -363,7 +355,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
     | CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l
     | CLetIn (na,a,t,b) ->
       f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
-    | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
+    | CCast (a,_,b) -> f n (f n acc a) b
     | CNotation (_,_,(l,ll,bl,bll)) ->
       (* The following is an approximation: we don't know exactly if
          an ident is binding nor to which subterms bindings apply *)
@@ -477,7 +469,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
       let (e,bl) = fold_map_local_binders f g e bl in CLambdaN (bl,f e b)
     | CLetIn (na,a,t,b) ->
       CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
-    | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c)
+    | CCast (a,k,c) -> CCast (f e a, k, f e c)
     | CNotation (inscope,n,(l,ll,bl,bll)) ->
       (* This is an approximation because we don't know what binds what *)
       CNotation (inscope,n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
@@ -598,7 +590,7 @@ let split_at_annot bl na =
 
 let mkIdentC id   = CAst.make @@ CRef (qualid_of_ident id,None)
 let mkRefC r      = CAst.make @@ CRef (r,None)
-let mkCastC (a,k) = CAst.make @@ CCast (a,k)
+let mkCastC (a,k,t) = CAst.make @@ CCast (a,k,t)
 let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b)
 let mkLetInC  (id,a,t,b)   = CAst.make @@ CLetIn (id,a,t,b)
 let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([CLocalAssum (idl,bk,a)],b)
@@ -682,7 +674,7 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
      CPatRecord (List.map (fun (r,p) -> (r,coerce_to_cases_pattern_expr p)) l)
   | CDelimiters (s,p) ->
      CPatDelimiters (s,coerce_to_cases_pattern_expr p)
-  | CCast (p,CastConv t) ->
+  | CCast (p,Constr.DEFAULTcast, t) ->
      CPatCast (coerce_to_cases_pattern_expr p,t)
   | _ ->
      CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr"

interp/constrexpr_ops.mli

@@ -49,7 +49,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option
 
 val mkIdentC : Id.t -> constr_expr
 val mkRefC : qualid -> constr_expr
-val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr
+val mkCastC : constr_expr * Constr.cast_kind * constr_expr -> constr_expr
 val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
 val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr
 val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr

interp/constrextern.ml

@@ -1144,9 +1144,8 @@ let rec extern inctx ?impargs scopes vars r =
 
   | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *)
 
-  | GCast (c, c') ->
-      CCast (sub_extern true scopes vars c,
-             map_cast_type (extern_typ scopes vars) c')
+  | GCast (c, k, c') ->
+    CCast (sub_extern true scopes vars c, k, extern_typ scopes vars c')
 
   | GInt i ->
      extern_prim_token_delimiter_if_required

interp/constrintern.ml

@@ -839,7 +839,7 @@ let rec adjust_env env = function
   | NLambda (_,_,c) -> adjust_env (switch_lambda_binders env) c
   | NLetIn (_,_,_,c) -> adjust_env env c
   | NVar id when Id.equal id ldots_var -> env
-  | NCast (c,_) -> adjust_env env c
+  | NCast (c,_,_) -> adjust_env env c
   | NApp _ -> restart_no_binders env
   | NVar _ | NRef _ | NHole _ | NCases _ | NLetTuple _ | NIf _
   | NRec _ | NSort _ | NProj _ | NInt _ | NFloat _ | NArray _
@@ -2305,9 +2305,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | CSort s ->
         DAst.make ?loc @@
         GSort (intern_sort ~local_univs:env.local_univs s)
-    | CCast (c1, c2) ->
+    | CCast (c1, k, c2) ->
         DAst.make ?loc @@
-        GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2)
+        GCast (intern env c1, k, intern_type (slide_binders env) c2)
     | CArray(u,t,def,ty) ->
       DAst.make ?loc @@ GArray(intern_instance ~local_univs:env.local_univs u, Array.map (intern env) t, intern env def, intern env ty)
     )

interp/notation_ops.ml

@@ -32,12 +32,6 @@ let rec alpha_var id1 id2 = function
   | _::idl -> alpha_var id1 id2 idl
   | [] -> Id.equal id1 id2
 
-let cast_type_iter2 f t1 t2 = match t1, t2 with
-  | CastConv t1, CastConv t2 -> f t1 t2
-  | CastVM t1, CastVM t2 -> f t1 t2
-  | CastNative t1, CastNative t2 -> f t1 t2
-  | (CastConv _ | CastVM _ | CastNative _), _ -> raise Exit
-
 (* used to update the notation variable with the local variables used
    in NList and NBinderList, since the iterator has its own variable *)
 let replace_var i j var = j :: List.remove Id.equal i var
@@ -205,9 +199,10 @@ let compare_notation_constr lt (vars1,vars2) t1 t2 =
     Array.iter3 (aux vars) renamings us1 us2;
     Array.iter3 (aux vars) (Array.map ((@) renaming) renamings) rs1 rs2
   | NSort s1, NSort s2 when glob_sort_eq s1 s2 -> ()
-  | NCast (t1, c1), NCast (t2, c2) ->
-    aux vars renaming t1 t2;
-    cast_type_iter2 (aux vars renaming) c1 c2
+  | NCast (c1, k1, t1), NCast (c2, k2, t2) ->
+    aux vars renaming c1 c2;
+    if not (cast_kind_eq k1 k2) then raise Exit;
+    aux vars renaming t1 t2
   | NInt i1, NInt i2 when Uint63.equal i1 i2 -> ()
   | NFloat f1, NFloat f2 when Float64.equal f1 f2 -> ()
   | NArray(t1,def1,ty1), NArray(t2,def2,ty2) ->
@@ -399,7 +394,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
           (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
       let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
       GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
-  | NCast (c,k) -> GCast (f e c,map_cast_type (f (h.slide e)) k)
+  | NCast (c,k,t) -> GCast (f e c, k, f (h.slide e) t)
   | NSort x -> GSort x
   | NHole (x, naming, arg)  -> GHole (x, naming, arg)
   | NRef (x,u) -> GRef (x,u)
@@ -631,7 +626,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
            user_err Pp.(str "Binders marked as implicit not allowed in notations.");
          add_name found na; (na,Option.map aux oc,aux b))) dll in
       NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
-  | GCast (c,k) -> NCast (aux c,map_cast_type aux k)
+  | GCast (c,k,t) -> NCast (aux c, k, aux t)
   | GSort s -> NSort s
   | GInt i -> NInt i
   | GFloat f -> NFloat f
@@ -850,10 +845,10 @@ let rec subst_notation_constr subst bound raw =
     if nsolve == solve && nknd == knd then raw
     else NHole (nknd, naming, nsolve)
 
-  | NCast (r1,k) ->
+  | NCast (r1,k,t) ->
       let r1' = subst_notation_constr subst bound r1 in
-      let k' = smartmap_cast_type (subst_notation_constr subst bound) k in
-      if r1' == r1 && k' == k then raw else NCast(r1',k')
+      let t' = subst_notation_constr subst bound t in
+      if r1' == r1 && t' == t then raw else NCast(r1',k,t')
 
   | NArray (t,def,ty) ->
       let def' = subst_notation_constr subst bound def
@@ -1326,16 +1321,6 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert =
   else
     bind_termlist_env alp sigma x l
 
-let match_cast match_fun sigma c1 c2 =
-  match c1, c2 with
-  | CastConv t1, CastConv t2
-  | CastVM t1, CastVM t2
-  | CastNative t1, CastNative t2 ->
-    match_fun sigma t1 t2
-  | CastConv _, _
-  | CastVM _, _
-  | CastNative _, _ -> raise No_match
-
 let does_not_come_from_already_eta_expanded_var glob =
   (* This is hack to avoid looping on a rule with rhs of the form *)
   (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *)
@@ -1449,8 +1434,10 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let alp,sigma = Array.fold_right2 (fun id1 id2 alsig ->
         match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
       Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
-  | GCast(t1, c1), NCast(t2, c2) ->
-    match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
+  | GCast(c1, k1, t1), NCast(c2, k2, t2) ->
+    let sigma = match_in u alp metas sigma c1 c2 in
+    if not (cast_kind_eq k1 k2) then raise No_match;
+    match_in u alp metas sigma t1 t2
 
   (* Next pair of lines useful only if not coming from detyping *)
   | GSort (UNamed [(GProp|GSet),0]), NSort (UAnonymous _) -> raise No_match

interp/notation_term.ml

@@ -43,7 +43,7 @@ type notation_constr =
       (Name.t * notation_constr option * notation_constr) list array *
       notation_constr array * notation_constr array
   | NSort of glob_sort
-  | NCast of notation_constr * notation_constr cast_type
+  | NCast of notation_constr * Constr.cast_kind * notation_constr
   | NInt of Uint63.t
   | NFloat of Float64.t
   | NArray of notation_constr array * notation_constr * notation_constr

interp/smartlocate.ml

@@ -28,7 +28,7 @@ let global_of_extended_global_head = function
       let rec head_of = function
         | NRef (ref,None) -> ref
         | NApp (rc, _) -> head_of rc
-        | NCast (rc, _) -> head_of rc
+        | NCast (rc, _, _) -> head_of rc
         | NLetIn (_, _, _, rc) -> head_of rc
         | _ -> raise Not_found in
       head_of syn_def

kernel/constr.ml

@@ -34,9 +34,7 @@ type existential_key = Evar.t
 type metavariable = int
 
 (* This defines the strategy to use for verifiying a Cast *)
-(* Warning: REVERTcast is not exported to vo-files; as of r14492, it has to *)
-(* come after the vo-exported cast_kind so as to be compatible with coqchk *)
-type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast
 
 (* This defines Cases annotations *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
@@ -1256,7 +1254,6 @@ let hash_cast_kind = function
 | VMcast -> 0
 | NATIVEcast -> 1
 | DEFAULTcast -> 2
-| REVERTcast -> 3
 
 let sh_instance = Univ.Instance.share
 

kernel/constr.mli

@@ -106,7 +106,7 @@ val mkType : Univ.Universe.t -> types
 
 
 (** This defines the strategy to use for verifiying a Cast *)
-type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast
 
 (** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the
    type t{_ 2} (that means t2 is declared as the type of t1). *)

kernel/reduction.ml

@@ -954,7 +954,7 @@ let infer_conv_universes cv_pb ?(l2r=false) ?(evars=fun _ -> None) ?(ts=Transpar
 let infer_conv = infer_conv_universes CONV
 let infer_conv_leq = infer_conv_universes CUMUL
 
-let default_conv cv_pb ?l2r:_ env t1 t2 =
+let default_conv cv_pb env t1 t2 =
     gen_conv cv_pb env t1 t2
 
 let default_conv_leq = default_conv CUMUL

kernel/reduction.mli

@@ -87,8 +87,8 @@ val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) ->
 val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
   TransparentState.t -> (constr,'a) generic_conversion_function
 
-val default_conv     : conv_pb -> ?l2r:bool -> types kernel_conversion_function
-val default_conv_leq : ?l2r:bool -> types kernel_conversion_function
+val default_conv     : conv_pb -> types kernel_conversion_function
+val default_conv_leq : types kernel_conversion_function
 
 (************************************************************************)
 

kernel/term_typing.ml

@@ -67,7 +67,7 @@ type typing_context =
 
 let check_primitive_type env op_t u t =
   let inft = Typeops.type_of_prim_or_type env u op_t in
-  try Reduction.default_conv ~l2r:false Reduction.CONV env inft t
+  try Reduction.default_conv Reduction.CONV env inft t
   with Reduction.NotConvertible ->
     Type_errors.error_incorrect_primitive env (make_judge op_t inft) t
 

kernel/typeops.ml

@@ -28,12 +28,12 @@ module NamedDecl = Context.Named.Declaration
 
 exception NotConvertibleVect of int
 
-let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y
+let conv_leq env x y = default_conv CUMUL env x y
 
 let conv_leq_vecti env v1 v2 =
   Array.fold_left2_i
     (fun i _ t1 t2 ->
-      try conv_leq false env t1 t2
+      try conv_leq env t1 t2
       with NotConvertible -> raise (NotConvertibleVect i))
     ()
     v1
@@ -197,7 +197,7 @@ let type_of_apply env func funt argsv argstv =
         let arg = argsv.(i) in
         let argt = argstv.(i) in
         let c1 = term_of_fconstr c1 in
-        begin match conv_leq false env argt c1 with
+        begin match conv_leq env argt c1 with
         | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons (inject arg) e) c2)
         | exception NotConvertible ->
           error_cant_apply_bad_type env
@@ -295,9 +295,7 @@ let check_cast env c ct k expected_type =
     | VMcast ->
       Vconv.vm_conv CUMUL env ct expected_type
     | DEFAULTcast ->
-      default_conv ~l2r:false CUMUL env ct expected_type
-    | REVERTcast ->
-      default_conv ~l2r:true CUMUL env ct expected_type
+      default_conv CUMUL env ct expected_type
     | NATIVEcast ->
       let sigma = Nativelambda.empty_evars in
       Nativeconv.native_conv CUMUL sigma env ct expected_type
@@ -557,7 +555,7 @@ let rec execute env cstr =
             let args = Array.append pms indices in
             let ct' = mkApp (mkIndU (ci.ci_ind,u), args) in
             let (ct', _) : constr * Sorts.t = execute_is_type env ct' in
-            let () = conv_leq false env ct ct' in
+            let () = conv_leq env ct ct' in
             let _, args' = decompose_appvect ct' in
             if args == args' then iv
             else CaseInvert {indices=Array.sub args' (Array.length pms) (Array.length indices)}
@@ -669,7 +667,7 @@ let check_context env rels =
       | LocalDef (x,bd,ty) ->
         let j1 = infer env bd in
         let jty = infer_type env ty in
-        conv_leq false env j1.uj_type ty;
+        conv_leq env j1.uj_type ty;
         let x = check_binder_annot jty.utj_type x in
         push_rel d env, LocalDef (x,j1.uj_val,jty.utj_val) :: rels)
     rels ~init:(env,[])
@@ -708,7 +706,7 @@ let judge_of_apply env funj argjv =
 
 let judge_of_cast env cj k tj =
   let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in
-  let c = match k with | REVERTcast -> cj.uj_val | _ -> mkCast (cj.uj_val, k, tj.utj_val) in
+  let c = mkCast (cj.uj_val, k, tj.utj_val) in
   make_judge c tj.utj_val
 
 let judge_of_inductive env indu =