Glob_term.cast_type is just an enum

With CastCoerce removed we can take the constr out of cast_type.

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 * Glob_term.cast_type * 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_type_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,CastConv, 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 * Glob_term.cast_type * 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

@@ -1149,9 +1149,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_type_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_type_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 * cast_type * 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

parsing/g_constr.mlg

@@ -30,7 +30,7 @@ let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) ->
     let loc = Loc.merge_opt (constr_loc c) (constr_loc ty)
-    in CAst.make ?loc @@ CCast(c, CastConv ty)
+    in CAst.make ?loc @@ CCast(c, CastConv, ty)
 
 let binder_of_name expl { CAst.loc = loc; v = na } =
   CLocalAssum ([CAst.make ?loc na], Default expl,
@@ -147,11 +147,11 @@ GRAMMAR EXTEND Gram
       [ c = binder_constr -> { c } ]
     | "100" RIGHTA
       [ c1 = term; "<:"; c2 = term LEVEL "200" ->
-                 { CAst.make ~loc @@ CCast(c1, CastVM c2) }
+                 { CAst.make ~loc @@ CCast(c1, CastVM, c2) }
       | c1 = term; "<<:"; c2 = term LEVEL "200" ->
-                 { CAst.make ~loc @@ CCast(c1, CastNative c2) }
+                 { CAst.make ~loc @@ CCast(c1, CastNative, c2) }
       | c1 = term; ":"; c2 = term LEVEL "200" ->
-                 { CAst.make ~loc @@ CCast(c1, CastConv c2) } ]
+                 { CAst.make ~loc @@ CCast(c1, CastConv, c2) } ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
@@ -222,7 +222,7 @@ GRAMMAR EXTEND Gram
       | "let"; id=name; bl = binders; ty = let_type_cstr; ":=";
         c1 = term LEVEL "200"; "in"; c2 = term LEVEL "200" ->
         { let ty,c1 = match ty, c1 with
-          | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
+          | (_,None), { CAst.v = CCast(c, CastConv, t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
           | _, _ -> ty, c1 in
           CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1,
                  Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) }
@@ -418,7 +418,7 @@ GRAMMAR EXTEND Gram
         { [CLocalAssum ([id],Default Explicit,c)] }
       | "("; id = name; ":="; c = lconstr; ")" ->
         { match c.CAst.v with
-          | CCast(c, CastConv t) -> [CLocalDef (id,c,Some t)]
+          | CCast(c, CastConv, t) -> [CLocalDef (id,c,Some t)]
           | _ -> [CLocalDef (id,c,None)] }
       | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" ->
         { [CLocalDef (id,c,Some t)] }

plugins/funind/gen_principle.ml

@@ -85,7 +85,7 @@ let is_rec names =
     | GVar id -> check_id id names
     | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ ->
       false
-    | GCast (b, _) -> lookup names b
+    | GCast (b, _, _) -> lookup names b
     | GRec _ -> CErrors.user_err (Pp.str "GRec not handled")
     | GIf (b, _, lhs, rhs) ->
       lookup names b || lookup names lhs || lookup names rhs
@@ -2027,10 +2027,8 @@ let rec add_args id new_args =
         , add_args id new_args b2
         , add_args id new_args b3 )
     | (CHole _ | CPatVar _ | CEvar _ | CPrim _ | CSort _) as b -> b
-    | CCast (b1, b2) ->
-      CCast
-        ( add_args id new_args b1
-        , Glob_ops.map_cast_type (add_args id new_args) b2 )
+    | CCast (b1, k, b2) ->
+      CCast (add_args id new_args b1, k, add_args id new_args b2)
     | CRecord pars ->
       CRecord (List.map (fun (e, o) -> (e, add_args id new_args o)) pars)
     | CNotation _ -> CErrors.anomaly ~label:"add_args " (Pp.str "CNotation.")

plugins/funind/glob_term_to_relation.ml

@@ -560,7 +560,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
       *)
       let f_res = build_entry_lc env sigma funnames args_res.to_avoid f in
       combine_results combine_app f_res args_res
-    | GCast (b, _) ->
+    | GCast (b, _, _) ->
       (* for an applied cast we just trash the cast part
          and restart the work.
 
@@ -626,7 +626,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
     let v =
       match typ with
       | None -> v
-      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, CastConv t)
+      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, CastConv, t)
     in
     let v_res = build_entry_lc env sigma funnames avoid v in
     let v_as_constr, ctx = Pretyping.understand env (Evd.from_env env) v in
@@ -688,7 +688,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
     let match_expr = mkGCases (None, [(b, (Anonymous, None))], [br]) in
     build_entry_lc env sigma funnames avoid match_expr
   | GRec _ -> user_err Pp.(str "Not handled GRec")
-  | GCast (b, _) -> build_entry_lc env sigma funnames avoid b
+  | GCast (b, _, _) -> build_entry_lc env sigma funnames avoid b
   | GArray _ -> user_err Pp.(str "Not handled GArray")
 
 and build_entry_lc_from_case env sigma funname make_discr (el : tomatch_tuples)
@@ -1130,7 +1130,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     let t =
       match t with
       | None -> v
-      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, CastConv t)
+      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, CastConv, t)
     in
     let not_free_in_t id = not (is_free_in id t) in
     let evd = Evd.from_env env in

plugins/funind/glob_termops.ml

@@ -108,10 +108,8 @@ let change_vars =
         | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported")
         | GSort _ as x -> x | GHole _ as x -> x | GInt _ as x -> x
         | GFloat _ as x -> x
-        | GCast (b, c) ->
-          GCast
-            ( change_vars mapping b
-            , Glob_ops.map_cast_type (change_vars mapping) c )
+        | GCast (b, k, c) ->
+          GCast (change_vars mapping b, k, change_vars mapping c)
         | GArray (u, t, def, ty) ->
           GArray
             ( u
@@ -286,8 +284,8 @@ let rec alpha_rt excluded rt =
         , alpha_rt excluded rhs )
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | (GSort _ | GInt _ | GFloat _ | GHole _) as rt -> rt
-    | GCast (b, c) ->
-      GCast (alpha_rt excluded b, Glob_ops.map_cast_type (alpha_rt excluded) c)
+    | GCast (b, k, c) ->
+      GCast (alpha_rt excluded b, k, alpha_rt excluded c)
     | GApp (f, args) ->
       GApp (alpha_rt excluded f, List.map (alpha_rt excluded) args)
     | GProj (f, args, c) ->
@@ -345,7 +343,7 @@ let is_free_in id =
           is_free_in cond || is_free_in br1 || is_free_in br2
         | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ -> false
         | GHole _ -> false
-        | GCast (b, (CastConv t | CastVM t | CastNative t)) ->
+        | GCast (b, _, t) ->
           is_free_in b || is_free_in t
         | GInt _ | GFloat _ -> false
         | GArray (_u, t, def, ty) ->
@@ -430,10 +428,8 @@ let replace_var_by_term x_id term =
             , Array.map replace_var_by_pattern t
             , replace_var_by_pattern def
             , replace_var_by_pattern ty )
-        | GCast (b, c) ->
-          GCast
-            ( replace_var_by_pattern b
-            , Glob_ops.map_cast_type replace_var_by_pattern c ))
+        | GCast (b, k, c) ->
+          GCast (replace_var_by_pattern b, k, replace_var_by_pattern c))
       x
   and replace_var_by_pattern_br ({CAst.loc; v = idl, patl, res} as br) =
     if List.exists (fun id -> Id.compare id x_id == 0) idl then br
@@ -532,8 +528,8 @@ let expand_as =
           , expand_as map br1
           , expand_as map br2 )
       | GRec _ -> user_err Pp.(str "Not handled GRec")
-      | GCast (b, c) ->
-        GCast (expand_as map b, Glob_ops.map_cast_type (expand_as map) c)
+      | GCast (b, k, c) ->
+        GCast (expand_as map b, k, expand_as map c)
       | GCases (sty, po, el, brl) ->
         GCases
           ( sty

plugins/ltac/g_ltac.mlg

@@ -14,7 +14,6 @@ DECLARE PLUGIN "ltac_plugin"
 
 open Util
 open Pp
-open Glob_term
 open Constrexpr
 open Tacexpr
 open Namegen
@@ -244,7 +243,7 @@ GRAMMAR EXTEND Gram
         { let t, ty =
             match mpv with
             | Term t -> (match t with
-              | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty)
+              | { CAst.v = CCast (t, _, ty) } -> Term t, Some (Term ty)
               | _ -> mpv, None)
             | _ -> mpv, None
           in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) }