From 708e41e1b707c1f7bb5bf347060cf3a3aec3b73b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 12 Aug 2021 16:28:13 +0200 Subject: [PATCH] Print REVERTcast as "c :> t" in Printing All mode, and parse it. --- doc/sphinx/language/core/definitions.rst | 1 + doc/tools/docgram/common.edit_mlg | 3 +++ doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 1 + interp/constrexpr.ml | 2 +- interp/constrexpr_ops.ml | 4 ++-- interp/constrexpr_ops.mli | 2 +- interp/notation_ops.ml | 4 ++-- interp/notation_term.ml | 2 +- parsing/g_constr.mlg | 14 ++++++++------ plugins/funind/glob_term_to_relation.ml | 4 ++-- plugins/ssr/ssrcommon.ml | 4 ++-- plugins/ssr/ssrfwd.ml | 12 ++++++------ plugins/ssr/ssrparser.mlg | 13 +++++++------ plugins/ssrmatching/ssrmatching.ml | 8 ++++---- plugins/syntax/number.ml | 2 +- plugins/syntax/string_notation.ml | 2 +- pretyping/detyping.ml | 9 ++------- pretyping/glob_ops.ml | 13 +++++++------ pretyping/glob_ops.mli | 2 +- pretyping/glob_term.ml | 9 +-------- pretyping/pretyping.ml | 3 +-- pretyping/pretyping.mli | 2 +- printing/ppconstr.ml | 9 +++++---- printing/proof_diffs.ml | 2 +- vernac/comDefinition.ml | 2 +- vernac/g_proofs.mlg | 5 +++-- vernac/g_vernac.mlg | 4 +++- 28 files changed, 70 insertions(+), 69 deletions(-) diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 40aad3865fb50..9b0c33b627fc8 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -40,6 +40,7 @@ Type cast .. prodn:: term_cast ::= @term10 : @type + | @term10 :> @type | @term10 <: @type | @term10 <<: @type diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 2c85d62aac4a4..9b5fa3854f52f 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -373,6 +373,9 @@ term100: [ | REPLACE term99 ":" term200 | WITH term99 ":" type | MOVETO term_cast term99 ":" type +| REPLACE term99 ":>" term200 +| WITH term99 ":>" type +| MOVETO term_cast term99 ":>" type ] constr: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 67071d0515134..756ca5f506fef 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -74,6 +74,7 @@ term200: [ term100: [ | term99 "<:" term200 | term99 "<<:" term200 +| term99 ":>" term200 | term99 ":" term200 | term99 ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index f4117c25c813c..45b28417b9dac 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -551,6 +551,7 @@ term_generalizing: [ term_cast: [ | term10 ":" type +| term10 ":>" type | term10 "<:" type | term10 "<<:" type ] diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index fab2d51f3802c..b8fb2aeb5a377 100644 --- a/interp/constrexpr.ml +++ b/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 * Glob_term.cast_type * constr_expr + | 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 diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index c9135b0a10670..2f9fcb0b0025f 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -242,7 +242,7 @@ module EqGen (A:sig val constr_expr_eq : constr_expr -> constr_expr -> bool end) | CSort s1, CSort s2 -> sort_expr_eq s1 s2 | 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 + 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 && @@ -674,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" diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 6e1957d0adb96..ee2aea4d49650 100644 --- a/interp/constrexpr_ops.mli +++ b/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 * Glob_term.cast_type * constr_expr -> 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 diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ebf8c5e2f64ab..7651440fd81ac 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -201,7 +201,7 @@ let compare_notation_constr lt (vars1,vars2) t1 t2 = | NSort s1, NSort s2 when glob_sort_eq s1 s2 -> () | NCast (c1, k1, t1), NCast (c2, k2, t2) -> aux vars renaming c1 c2; - if not (cast_type_eq k1 k2) then raise Exit; + 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 -> () @@ -1436,7 +1436,7 @@ let rec match_ inner u alp metas sigma a1 a2 = Array.fold_left2 (match_in u alp metas) sigma bl1 bl2 | 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; + 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 *) diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 77ec695073a4f..9953c2d019bb0 100644 --- a/interp/notation_term.ml +++ b/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 * cast_type * notation_constr + | 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 diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 31dc617032c8e..2cff859b14c42 100644 --- a/parsing/g_constr.mlg +++ b/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, DEFAULTcast, ty) let binder_of_name expl { CAst.loc = loc; v = na } = CLocalAssum ([CAst.make ?loc na], Default expl, @@ -147,11 +147,13 @@ 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, VMcast, c2) } | c1 = term; "<<:"; c2 = term LEVEL "200" -> - { CAst.make ~loc @@ CCast(c1, CastNative, c2) } + { CAst.make ~loc @@ CCast(c1, NATIVEcast, c2) } + | c1 = term; ":>"; c2 = term LEVEL "200" -> + { CAst.make ~loc @@ CCast(c1, REVERTcast, c2) } | c1 = term; ":"; c2 = term LEVEL "200" -> - { CAst.make ~loc @@ CCast(c1, CastConv, c2) } ] + { CAst.make ~loc @@ CCast(c1, DEFAULTcast, c2) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA @@ -222,7 +224,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, DEFAULTcast, 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 +420,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, DEFAULTcast, t) -> [CLocalDef (id,c,Some t)] | _ -> [CLocalDef (id,c,None)] } | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" -> { [CLocalDef (id,c,Some t)] } diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 86a162f3e8f7c..d12320593bbcd 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -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, DEFAULTcast, 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 @@ -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, DEFAULTcast, t) in let not_free_in_t id = not (is_free_in id t) in let evd = Evd.from_env env in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 876de4fac70a9..8f32be30d252e 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -194,7 +194,7 @@ let rec isRHoles cl = match cl with let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) let mkRVar id = DAst.make @@ GRef (GlobRef.VarRef id,None) let mkRltacVar id = DAst.make @@ GVar (id) -let mkRCast rc rt = DAst.make @@ GCast (rc, CastConv, rt) +let mkRCast rc rt = DAst.make @@ GCast (rc, DEFAULTcast, rt) let mkRType = DAst.make @@ GSort (UAnonymous {rigid=true}) let mkRProp = DAst.make @@ GSort (UNamed [GProp,0]) let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2) @@ -905,7 +905,7 @@ let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ CProdN ([CLocalAssum([CAst.make Anonymous], Default Explicit, ty)], t) -let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv, ty) +let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, DEFAULTcast, ty) let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = [] let rec isCxHoles = function ({ CAst.v = CHole _ }, None) :: ch -> isCxHoles ch | _ -> false diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 34a3bfdde4e99..a43dc5de89654 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -157,13 +157,13 @@ let havetac ist let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc (pf_env gl) (project gl) ist t in a,b,u in let open CAst in let ct, cty, hole, loc = match Ssrcommon.ssrterm_of_ast_closure_term t with - | _, (_, Some { loc; v = CCast (ct, CastConv, cty)}) -> + | _, (_, Some { loc; v = CCast (ct, DEFAULTcast, cty)}) -> mkt ct, mkt cty, mkt (mkCHole None), loc | _, (_, Some ct) -> mkt ct, mkt (mkCHole None), mkt (mkCHole None), None | _, (t, None) -> begin match DAst.get t with - | GCast (ct, CastConv, cty) -> + | GCast (ct, DEFAULTcast, cty) -> mkl ct, mkl cty, mkl mkRHole, t.CAst.loc | _ -> mkl t, mkl mkRHole, mkl mkRHole, None end @@ -238,12 +238,12 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave = let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with | (a, (b, Some ct)) -> begin match ct.CAst.v with - | CCast (_, CastConv, cty) -> a, (b, Some cty) + | CCast (_, DEFAULTcast, cty) -> a, (b, Some cty) | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" end | (a, (t, None)) -> begin match DAst.get t with - | GCast (_, CastConv, cty) -> a, (cty, None) + | GCast (_, DEFAULTcast, cty) -> a, (cty, None) | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" end in @@ -325,12 +325,12 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = let c = match Ssrcommon.ssrterm_of_ast_closure_term c with | (a, (b, Some ct)) -> begin match ct.CAst.v with - | CCast (_, CastConv, cty) -> a, (b, Some cty) + | CCast (_, DEFAULTcast, cty) -> a, (b, Some cty) | _ -> anomaly "suff: ssr cast hole deleted by typecheck" end | (a, (t, None)) -> begin match DAst.get t with - | GCast (_, CastConv, cty) -> a, (cty, None) + | GCast (_, DEFAULTcast, cty) -> a, (cty, None) | _ -> anomaly "suff: ssr cast hole deleted by typecheck" end in diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 309df7bafc1d5..c5b95321661c1 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -12,7 +12,8 @@ { -let _vmcast = Constr.VMcast +let defaultCast = Constr.DEFAULTcast +let vmCast = Constr.VMcast open Names open Pp open Pcoq @@ -1229,7 +1230,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } -> let bs, c' = format_constr_expr h c in Bdef (x, oty, v) :: bs, c' - | [BFcast], { v = CCast (c, Glob_term.CastConv, t) } -> + | [BFcast], { v = CCast (c, defaultCast, t) } -> [Bcast t], c | BFrec (has_str, has_cast) :: h, { v = CFix ( _, [_, Some {CAst.v = CStructRec locn}, bl, t, c]) } -> @@ -1271,7 +1272,7 @@ let mkFwdCast fk ?loc ?c t = | Some c -> assert (same_ist t c); c.body in ((fk, [BFcast]), { t with annotation = `None; - body = (CAst.make ?loc @@ CCast (c, Glob_term.CastConv, t.body)) }) + body = (CAst.make ?loc @@ CCast (c, defaultCast, t.body)) }) let mkssrFwdCast fk loc t c = ((fk, [BFcast]), (c, Some t)) @@ -1386,8 +1387,8 @@ let push_binders c2 bs = | [] -> c | _ -> anomaly "binder not a lambda nor a let in" in match c2 with - | { loc; v = CCast (ct, Glob_term.CastConv, cty) } -> - CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv, (loop true cty bs))) + | { loc; v = CCast (ct, defaultCast, cty) } -> + CAst.make ?loc @@ (CCast (loop false ct bs, defaultCast, (loop true cty bs))) | ct -> loop false ct bs let rec fix_binders = let open CAst in function @@ -2213,7 +2214,7 @@ END let vmexacttac pf = Goal.enter begin fun gl -> - exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl)) + exact_no_check (EConstr.mkCast (pf, vmCast, Tacmach.New.pf_concl gl)) end } diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 054dd7b861786..c78f682631382 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -135,12 +135,12 @@ let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((CAst.make ?loc name), bo, None, t) -let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv, ty) +let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, DEFAULTcast, ty) (** Constructors for rawconstr *) let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None) let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) -let mkRCast rc rt = DAst.make @@ GCast (rc, CastConv, rt) +let mkRCast rc rt = DAst.make @@ GCast (rc, DEFAULTcast, rt) let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) let nf_evar sigma c = @@ -988,7 +988,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty = let ist_of x = x.interpretation in let decode ({interpretation=ist; _} as t) ?reccall f g = try match DAst.get (pf_intern_term env sigma0 t) with - | GCast(t, CastConv, c) when isGHole t && isGLambda c-> + | GCast(t, DEFAULTcast, c) when isGHole t && isGLambda c-> let (x, c) = destGLambda c in f x {kind = NoFlag; pattern = (c,None); interpretation = ist} | GVar id @@ -1035,7 +1035,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty = let red = let rec decode_red = function | T {kind=k; pattern=(t,None); interpretation=ist} -> begin match DAst.get t with - | GCast (c, CastConv, t) + | GCast (c, DEFAULTcast, t) when isGHole c && let (id, t) = destGLambda t in let id = Id.to_string id in let len = String.length id in diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml index 0b8ffb4f55787..8d46fccfc3a12 100644 --- a/plugins/syntax/number.ml +++ b/plugins/syntax/number.ml @@ -115,7 +115,7 @@ let locate_int63 () = else None let has_type env sigma f ty = - let c = mkCastC (mkRefC f, Glob_term.CastConv, ty) in + let c = mkCastC (mkRefC f, Constr.DEFAULTcast, ty) in try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index e6c335050b852..eebe63d49b244 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -26,7 +26,7 @@ let q_list () = qualid_of_ref "core.list.type" let q_byte () = qualid_of_ref "core.byte.type" let has_type env sigma f ty = - let c = mkCastC (mkRefC f, Glob_term.CastConv, ty) in + let c = mkCastC (mkRefC f, Constr.DEFAULTcast, ty) in try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 48842dcf8cc08..d6a24bdd8a3bf 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -562,7 +562,7 @@ let detype_case computable detype detype_eqns avoid env sigma (ci, univs, params | CaseInvert {indices} -> (* XXX use holes instead of params? *) let t = mkApp (mkIndU (ci.ci_ind,univs), Array.append params indices) in - DAst.make @@ GCast (tomatch, CastConv, detype t) + DAst.make @@ GCast (tomatch, DEFAULTcast, detype t) in let alias, aliastyp, pred= if (not !Flags.raw_print) && synth_type && computable && not (Int.equal (Array.length bl) 0) @@ -786,12 +786,7 @@ and detype_r d flags avoid env sigma t = | Cast (c1,k,c2) -> let d1 = detype d flags avoid env sigma c1 in let d2 = detype d flags avoid env sigma c2 in - let cast = match k with - | VMcast -> CastVM - | NATIVEcast -> CastNative - | DEFAULTcast | REVERTcast -> CastConv - in - GCast(d1,cast,d2) + GCast(d1,k,d2) | Prod (na,ty,c) -> detype_binder d flags BProd avoid env sigma (LocalAssum (na,ty)) c | Lambda (na,ty,c) -> detype_binder d flags BLambda avoid env sigma (LocalAssum (na,ty)) c | LetIn (na,b,ty,c) -> detype_binder d flags BLetIn avoid env sigma (LocalDef (na,b,ty)) c diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 8ac88939b9ccb..e93d14a27c6d2 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -101,11 +101,12 @@ let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with Name.equal na1 na2 | (PatVar _ | PatCstr _), _ -> false -let cast_type_eq t1 t2 = match t1, t2 with - | CastConv, CastConv - | CastVM, CastVM - | CastNative, CastNative -> true - | (CastConv | CastVM | CastNative), _ -> false +let cast_kind_eq t1 t2 = let open Constr in match t1, t2 with + | DEFAULTcast, DEFAULTcast + | REVERTcast, REVERTcast + | VMcast, VMcast + | NATIVEcast, NATIVEcast -> true + | (DEFAULTcast | REVERTcast | VMcast | NATIVEcast), _ -> false let matching_var_kind_eq k1 k2 = match k1, k2 with | FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2 @@ -170,7 +171,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with Option.equal (==) gn1 gn2 (* Only thing sensible *) && Namegen.intro_pattern_naming_eq nam1 nam2 | GCast (c1, k1, t1), GCast (c2, k2, t2) -> - f c1 c2 && cast_type_eq k1 k2 && f t1 t2 + f c1 c2 && cast_kind_eq k1 k2 && f t1 t2 | GProj ((cst1, u1), args1, c1), GProj ((cst2, u2), args2, c2) -> GlobRef.(equal (ConstRef cst1) (ConstRef cst2)) && Option.equal (List.equal glob_level_eq) u1 u2 && diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 4e9d61eed04e8..7132fb119c768 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -32,7 +32,7 @@ val alias_of_pat : 'a cases_pattern_g -> Name.t val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g -val cast_type_eq : cast_type -> cast_type -> bool +val cast_kind_eq : Constr.cast_kind -> Constr.cast_kind -> bool val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index c30a8330c7f8a..ce7a03416ef7b 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -52,13 +52,6 @@ and glob_fix_kind = | GFix of (glob_recarg array * int) | GCoFix of int -(** Casts *) - -type cast_type = - | CastConv - | CastVM - | CastNative - (** The kind of patterns that occurs in "match ... with ... end" locs here refers to the ident's location, not whole pat *) @@ -94,7 +87,7 @@ type 'a glob_constr_r = 'a glob_constr_g array * 'a glob_constr_g array | GSort of glob_sort | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option - | GCast of 'a glob_constr_g * cast_type * 'a glob_constr_g + | GCast of 'a glob_constr_g * Constr.cast_kind * 'a glob_constr_g | GProj of (Constant.t * glob_level list option) * 'a glob_constr_g list * 'a glob_constr_g | GInt of Uint63.t | GFloat of Float64.t diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index db5f5dfd6b320..c2a6c0be957aa 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -500,7 +500,7 @@ type pretyper = { pretype_rec : pretyper -> glob_fix_kind * Id.t array * glob_decl list array * glob_constr array * glob_constr array -> unsafe_judgment pretype_fun; pretype_sort : pretyper -> glob_sort -> unsafe_judgment pretype_fun; pretype_hole : pretyper -> Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option -> unsafe_judgment pretype_fun; - pretype_cast : pretyper -> glob_constr * cast_type * glob_constr -> unsafe_judgment pretype_fun; + pretype_cast : pretyper -> glob_constr * cast_kind * glob_constr -> unsafe_judgment pretype_fun; pretype_int : pretyper -> Uint63.t -> unsafe_judgment pretype_fun; pretype_float : pretyper -> Float64.t -> unsafe_judgment pretype_fun; pretype_array : pretyper -> glob_level list option * glob_constr array * glob_constr * glob_constr -> unsafe_judgment pretype_fun; @@ -1187,7 +1187,6 @@ struct fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, cj = - let k = (match k with CastVM -> VMcast | CastNative -> NATIVEcast | CastConv -> DEFAULTcast) in let sigma, tj = eval_type_pretyper self ~program_mode ~poly resolve_tc empty_valcon env sigma t in let sigma, tval = Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma tj.utj_val in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f78e1cd8c017c..70d4b6dea172e 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -160,7 +160,7 @@ type pretyper = { pretype_rec : pretyper -> glob_fix_kind * Id.t array * glob_decl list array * glob_constr array * glob_constr array -> unsafe_judgment pretype_fun; pretype_sort : pretyper -> glob_sort -> unsafe_judgment pretype_fun; pretype_hole : pretyper -> Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option -> unsafe_judgment pretype_fun; - pretype_cast : pretyper -> glob_constr * cast_type * glob_constr -> unsafe_judgment pretype_fun; + pretype_cast : pretyper -> glob_constr * Constr.cast_kind * glob_constr -> unsafe_judgment pretype_fun; pretype_int : pretyper -> Uint63.t -> unsafe_judgment pretype_fun; pretype_float : pretyper -> Float64.t -> unsafe_judgment pretype_fun; pretype_array : pretyper -> glob_level list option * glob_constr array * glob_constr * glob_constr -> unsafe_judgment pretype_fun; diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 51e25428753bd..a72ba51673b63 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -517,10 +517,11 @@ let tag_var = tag Tag.variable | _ -> pr sep inherited a - let pr_cast = function - | CastConv -> str ":" - | CastVM -> str "<:" - | CastNative -> str "<<:" + let pr_cast = let open Constr in function + | DEFAULTcast -> str ":" + | REVERTcast -> str ":>" + | VMcast-> str "<:" + | NATIVEcast -> str "<<:" let pr pr sep inherited a = let return (cmds, prec) = (tag_constr_expr a cmds, prec) in diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 47305a50b28d8..39ca94944903a 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -537,7 +537,7 @@ let match_goals ot nt = | CSort s, CSort s2 -> () | CCast (c,k,t), CCast (c2,k2,t2) -> constr_expr ogname c c2; - if not (Glob_ops.cast_type_eq k k2) + if not (Glob_ops.cast_kind_eq k k2) then raise (Diff_Failure "Unable to match goals between old and new proof states (4)"); constr_expr ogname t t2 | CNotation (_,ntn,args), CNotation (_,ntn2,args2) -> diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index d07b96df8d56a..6ef5fc42bd73c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -52,7 +52,7 @@ let protect_pattern_in_binder bl c ctypopt = | None -> CAst.make ?loc:c.CAst.loc (Constrexpr.CHole (None,Namegen.IntroAnonymous,None)) | Some t -> t in let loc = Loc.merge_opt c.CAst.loc t.CAst.loc in - let c = CAst.make ?loc @@ Constrexpr.CCast (c, Glob_term.CastConv, t) in + let c = CAst.make ?loc @@ Constrexpr.CCast (c, Constr.DEFAULTcast, t) in let loc = match List.hd bl with | Constrexpr.CLocalAssum (a::_,_,_) | Constrexpr.CLocalDef (a,_,_) -> a.CAst.loc | Constrexpr.CLocalPattern {CAst.loc} -> loc diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index b9f36acc4c35b..97d247b58108c 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -10,11 +10,12 @@ { -open Glob_term open Constrexpr open Vernacexpr open Hints +module C = Constr + open Pcoq open Pcoq.Prim open Pcoq.Constr @@ -130,7 +131,7 @@ GRAMMAR EXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> { c } - | ":"; t = lconstr; ":="; c = lconstr -> { CAst.make ~loc @@ CCast(c,CastConv, t) } ] ] + | ":"; t = lconstr; ":="; c = lconstr -> { CAst.make ~loc @@ CCast(c,C.DEFAULTcast, t) } ] ] ; mode: [ [ l = LIST1 [ "+" -> { ModeInput } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 05367c90b3d88..9be6c651410cd 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -23,6 +23,8 @@ open Decls open Declaremods open Namegen +module C = Constr + open Pcoq open Pcoq.Prim open Pcoq.Constr @@ -350,7 +352,7 @@ GRAMMAR EXTEND Gram def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> { match c.CAst.v with - | CCast(c, Glob_term.CastConv, t) -> DefineBody (bl, red, c, Some t) + | CCast(c, C.DEFAULTcast, t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None) } | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> { DefineBody (bl, red, c, Some t) }