Merge PR #21342: Stop directly checking Printing All while printing constr

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

Author: coqbot-app[bot]

dev/ci/user-overlays/21342-SkySkimmer-print-raw.sh

@@ -0,0 +1 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi print-raw 21342

interp/constrextern.ml

@@ -9,7 +9,6 @@
 (************************************************************************)
 
 (*i*)
-open Pp
 open CErrors
 open Util
 open Names
@@ -40,7 +39,7 @@ module NamedDecl = Context.Named.Declaration
 let hole = CAst.make @@ CHole (None)
 
 let is_reserved_type ~flags na t =
-  not flags.ExternFlags.raw && flags.ExternFlags.use_implicit_types &&
+  flags.ExternFlags.use_implicit_types &&
   match na with
   | Anonymous -> false
   | Name id ->
@@ -53,49 +52,6 @@ let is_reserved_type ~flags na t =
       true
     with Not_found | No_match -> false
 
-(**********************************************************************)
-(* Control printing of records *)
-
-let is_record indsp =
-  try
-    let _ = Structure.find (Global.env ()) indsp in
-    true
-  with Not_found -> false
-
-let encode_record r =
-  let indsp = Nametab.global_inductive r in
-  if not (is_record indsp) then
-    user_err ?loc:r.CAst.loc
-      (str "This type is not a structure type.");
-  indsp
-
-module PrintingRecordRecord =
-  PrintingInductiveMake (struct
-    let encode _env = encode_record
-    let field = "Record"
-    let title = "Types leading to pretty-printing using record notation: "
-    let member_message s b =
-      str "Terms of " ++ s ++
-      str
-      (if b then " are printed using record notation"
-      else " are not printed using record notation")
-  end)
-
-module PrintingRecordConstructor =
-  PrintingInductiveMake (struct
-    let encode _env = encode_record
-    let field = "Constructor"
-    let title = "Types leading to pretty-printing using constructor form: "
-    let member_message s b =
-      str "Terms of " ++ s ++
-      str
-      (if b then " are printed using constructor form"
-      else " are not printed using constructor form")
-  end)
-
-module PrintingRecord = Goptions.MakeRefTable(PrintingRecordRecord)
-module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor)
-
 (**********************************************************************)
 (* Various externalisation functions *)
 
@@ -222,8 +178,8 @@ let drop_implicits_in_patt ~flags cst nb_expl ?(tags=[]) args =
   in
   let try_impls_fit (imps,args,tags) =
     if not !Constrintern.parsing_explicit &&
-       ((flags.ExternFlags.raw || flags.ExternFlags.implicits) &&
-        List.exists is_status_implicit imps)
+       flags.ExternFlags.implicits &&
+       List.exists is_status_implicit imps
        (* Note: !print_implicits_explicit_args=true not supported for patterns *)
     then None
     else impls_fit [] (imps,args,tags)
@@ -296,20 +252,16 @@ let pattern_printable_in_both_syntax ~flags (ind,_ as c) =
   List.exists (fun (_,impls) ->
     (List.length impls >= nb_params) &&
       let params,args = Util.List.chop nb_params impls in
-      not flags.ExternFlags.raw && not flags.ExternFlags.implicits &&
+      not flags.ExternFlags.implicits &&
       (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
   ) impl_st
 
 let extern_record_pattern ~flags cstrsp args =
+  if not (ExternFlags.Records.use_record_syntax flags.ExternFlags.records (fst cstrsp))
+  then None
+  else
   try
-    if flags.ExternFlags.raw then raise_notrace Exit;
     let projs = Structure.find_projections (Global.env ()) (fst cstrsp) in
-    if PrintingRecord.active (fst cstrsp) then
-      ()
-    else if PrintingConstructor.active (fst cstrsp) then
-      raise_notrace Exit
-    else if not flags.ExternFlags.records then
-      raise_notrace Exit;
     let rec ip projs args acc =
       match projs, args with
       | [], [] -> acc
@@ -333,7 +285,7 @@ let extern_record_pattern ~flags cstrsp args =
 (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope ~flags ((custom,(lev_after:int option)),scopes as allscopes) vars pat =
   try
-    if !Flags.in_debugger || flags.ExternFlags.raw || flags.ExternFlags.raw_literals then raise No_match;
+    if !Flags.in_debugger || flags.ExternFlags.raw_literals then raise No_match;
     let (na,p,key) = uninterp_prim_token_cases_pattern ~print_float:flags.float pat scopes in
     match availability_of_entry_coercion custom constr_lowest_level with
       | None -> raise No_match
@@ -343,7 +295,7 @@ let rec extern_cases_pattern_in_scope ~flags ((custom,(lev_after:int option)),sc
           (insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na)
   with No_match ->
     try
-      if !Flags.in_debugger || flags.ExternFlags.raw || not flags.ExternFlags.notations then raise No_match;
+      if !Flags.in_debugger || not flags.ExternFlags.notations then raise No_match;
       extern_notation_pattern ~flags allscopes vars pat
         (uninterp_cases_pattern_notations (Global.env ()) pat)
     with No_match ->
@@ -483,7 +435,7 @@ let extern_ind_pattern_in_scope ~flags (custom,scopes as allscopes) vars ind arg
     CAst.make @@ CPatCstr (c, Some args, [])
   else
     try
-      if flags.ExternFlags.raw || not flags.ExternFlags.notations || Inductiveops.inductive_has_local_defs (Global.env()) ind
+      if not flags.ExternFlags.notations || Inductiveops.inductive_has_local_defs (Global.env()) ind
         then raise No_match;
       extern_notation_ind_pattern ~flags allscopes vars ind args
           (uninterp_ind_pattern_notations (Global.env ()) ind)
@@ -511,7 +463,7 @@ let is_gvar id c = match DAst.get c with
 | _ -> false
 
 let is_projection ~flags nargs r =
-  if not !Flags.in_debugger && not flags.ExternFlags.raw && flags.ExternFlags.projections then
+  if not !Flags.in_debugger && flags.ExternFlags.projections then
     try
       match r with
       | GlobRef.ConstRef c ->
@@ -546,7 +498,6 @@ let adjust_implicit_arguments ~flags inctx n args impl =
     | a::args, imp::impl when is_status_implicit imp ->
         let tail = exprec (args,impl) in
         let visible =
-          flags.ExternFlags.raw ||
           (flags.ExternFlags.implicits && flags.ExternFlags.implicits_explicit_args) ||
           (is_needed_for_correct_partial_application tail imp) ||
           (flags.ExternFlags.implicits_defensive &&
@@ -583,15 +534,11 @@ let is_start_implicit = function
 
 let extern_record ~flags ref args =
   try
-    if flags.ExternFlags.raw then raise_notrace Exit;
     let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
+    if not (ExternFlags.Records.use_record_syntax flags.ExternFlags.records (fst cstrsp))
+    then None
+    else
     let struc = Structure.find (Global.env ()) (fst cstrsp) in
-    if PrintingRecord.active (fst cstrsp) then
-      ()
-    else if PrintingConstructor.active (fst cstrsp) then
-      raise_notrace Exit
-    else if not flags.ExternFlags.records then
-      raise_notrace Exit;
     let projs = struc.Structure.projections in
     let rec cut args n =
       if Int.equal n 0 then args
@@ -633,9 +580,9 @@ let extern_global impl f us =
 let extern_applied_ref ~flags inctx impl (cf,f) us args =
   try
     if not !Constrintern.parsing_explicit &&
-       ((flags.ExternFlags.raw ||
-         (flags.ExternFlags.implicits && not flags.ExternFlags.implicits_explicit_args)) &&
-        List.exists is_status_implicit impl)
+       flags.ExternFlags.implicits &&
+       not flags.ExternFlags.implicits_explicit_args &&
+       List.exists is_status_implicit impl
     then raise Expl;
     let impl = if !Constrintern.parsing_explicit then [] else impl in
     let n = List.length args in
@@ -706,7 +653,7 @@ let match_coercion_app c = match DAst.get c with
 
 let remove_one_coercion ~flags inctx c =
   try match match_coercion_app c with
-  | Some (loc,r,args) when not (flags.ExternFlags.raw || flags.ExternFlags.coercions) ->
+  | Some (loc,r,args) when not flags.ExternFlags.coercions ->
       let nargs = List.length args in
       (match Coercionops.hide_coercion r with
           | Some nparams when
@@ -1232,22 +1179,16 @@ and extern_local_binder depth scopes eenv = function
          (na::assums,na::ids,
           CLocalAssum([CAst.make na],extern_relevance_info eenv.uvars r,Default bk,ty) :: l))
 
-    | GLocalPattern ((p,_),_,bk,ty) ->
-      let ty =
-        if eenv.flags.raw then Some (extern_typ depth scopes eenv ty) else None in
+    | GLocalPattern ((p,_),_,bk,_) ->
       let p = mkCPatOr (List.map (extern_cases_pattern ~flags:eenv.flags eenv.vars) p) in
       let (assums,ids,l) = extern_local_binder depth scopes eenv l in
-      let p = match ty with
-        | None -> p
-        | Some ty -> CAst.make @@ (CPatCast (p,ty)) in
       (assums,ids, CLocalPattern p :: l)
 
 and extern_eqn depth inctx scopes eenv {CAst.loc;v=(ids,pll,c)} =
   let pll = List.map (List.map (extern_cases_pattern_in_scope ~flags:eenv.flags scopes eenv.vars)) pll in
   make ?loc (pll,extern depth inctx scopes eenv c)
 
 and extern_notations depth inctx scopes eenv nargs t =
-  if eenv.flags.raw then raise No_match;
   try extern_possible_prim_token ~flags:eenv.flags scopes t
   with No_match ->
     if not eenv.flags.notations then raise No_match;

plugins/funind/indfun_common.ml

@@ -99,13 +99,11 @@ let without_implicit_declarations f () =
 
 let full_detype_flags () =
   let flags = PrintingFlags.Detype.current() in
-  { flags with raw = true; universes = true; }
+  PrintingFlags.Detype.make_raw { flags with universes = true; }
 
 let full_extern_flags () =
   let flags = PrintingFlags.Extern.current() in
-  { flags with raw = true; factorize_eqns = {
-        flags.factorize_eqns with
-        allow_match_default_clause = false } }
+  PrintingFlags.Extern.make_raw flags
 
 let extern_env_full_printing () =
   Constrextern.empty_extern_env ~flags:(full_extern_flags())

pretyping/detyping.ml

@@ -24,7 +24,6 @@ open Glob_term
 open Glob_ops
 open Termops
 open Namegen
-open Libnames
 open Globnames
 open Mod_subst
 open Context.Rel.Declaration
@@ -244,28 +243,8 @@ let encode_tuple env ({CAst.loc} as r) =
       (str "This type cannot be seen as a tuple type.");
   x
 
-module PrintingInductiveMake =
-  functor (Test : sig
-     val encode : Environ.env -> qualid -> inductive
-     val member_message : Pp.t -> bool -> Pp.t
-     val field : string
-     val title : string
-  end) ->
-  struct
-    type t = inductive
-    module Set = Indset_env
-    let encode env ind = Environ.QInd.canonize env (Test.encode env ind)
-    let subst subst obj = subst_ind subst obj
-    let check_local _ _ = ()
-    let discharge (i:t) = i
-    let printer ind = Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind)
-    let key = ["Printing";Test.field]
-    let title = Test.title
-    let member_message x = Test.member_message (printer x)
-  end
-
 module PrintingCasesIf =
-  PrintingInductiveMake (struct
+  PrintingFlags.PrintingInductiveMake (struct
     let encode = encode_bool
     let field = "If"
     let title = "Types leading to pretty-printing of Cases using a `if' form:"
@@ -277,7 +256,7 @@ module PrintingCasesIf =
   end)
 
 module PrintingCasesLet =
-  PrintingInductiveMake (struct
+  PrintingFlags.PrintingInductiveMake (struct
     let encode = encode_tuple
     let field = "Let"
     let title =
@@ -408,7 +387,7 @@ let lookup_index_as_renamed env sigma t n =
 let rec join_eqns ~flags (ids,rhs as x) patll = function
   | ({CAst.loc; v=(ids',patl',rhs')} as eqn')::rest ->
     let open ExternFlags.FactorizeEqns in
-     if not flags.raw && flags.factorize_match_patterns &&
+     if flags.factorize_match_patterns &&
         List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs'
      then
        join_eqns  ~flags x (patl'::patll) rest
@@ -455,7 +434,7 @@ let factorize_eqns ~flags eqns =
   let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in
   let open CAst in
   let open ExternFlags.FactorizeEqns in
-  if not flags.raw && flags.allow_match_default_clause && eqns <> [] then
+  if flags.allow_match_default_clause && eqns <> [] then
     match select_default_clause eqns with
     (* At least two clauses and the last one is disjunctive with no variables *)
     | Some {loc=gloc;v=([],patl::_::_,rhs)}, (_::_ as eqns) ->
@@ -615,7 +594,7 @@ let detype_case ~flags computable detype detype_eqns avoid env sigma (ci, univs,
         DAst.make @@ GCast (tomatch, None, detype t)
   in
   let alias, aliastyp, pred =
-    if (not flags.flg.raw) && synth_type && computable && not (Int.equal (Array.length bl) 0)
+    if synth_type && computable && not (Int.equal (Array.length bl) 0)
     then
       Anonymous, None, None
     else
@@ -635,7 +614,7 @@ let detype_case ~flags computable detype detype_eqns avoid env sigma (ci, univs,
   let constructs = Array.init (Array.length bl) (fun i -> (ci.ci_ind,i+1)) in
   let tag = let st = ci.ci_pp_info.style in
     try
-      if flags.flg.raw then
+      if flags.flg.always_regular_match_style then
         RegularStyle
       else if st == LetPatternStyle then
         st
@@ -948,7 +927,7 @@ and detype_r d flags avoid env sigma t =
 
 and detype_eqns d flags avoid env sigma computable constructs bl =
   try
-    if flags.flg.raw || not flags.flg.matching then raise_notrace Exit;
+    if not flags.flg.matching then raise_notrace Exit;
     let mat = build_tree ~flags Anonymous flags (avoid,env) sigma bl in
     List.map (fun (ids,pat,((avoid,env),c)) ->
         CAst.make (Id.Set.elements ids,[pat],detype d flags avoid env sigma c))
@@ -1010,9 +989,12 @@ and detype_binder d flags bk avoid env sigma decl c =
           try Retyping.get_sort_quality_of (snd env) sigma ty
           with Retyping.RetypeError _ -> UnivGen.QualityOrSet.qtype
       in
-      let t = if not (UnivGen.QualityOrSet.is_prop s) && not flags.flg.raw
-              then None
-              else Some (detype d (nongoal flags) avoid env sigma ty) in
+      let t =
+        (* XXX also sprop? *)
+        if flags.flg.nonpropositional_letin_types || UnivGen.QualityOrSet.is_prop s
+        then Some (detype d (nongoal flags) avoid env sigma ty)
+        else None
+      in
       GLetIn (na', rinfo, c, t, r)
 
 let detype_rel_context d flags avoid env sigma sign =

pretyping/detyping.mli

@@ -56,11 +56,3 @@ val detype_closed_glob : flags:PrintingFlags.Detype.t -> ?isgoal:bool ->
 (** look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_displayed  : env -> evar_map -> constr -> Id.t -> int option
 val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
-
-module PrintingInductiveMake :
-  functor (_ : sig
-    val encode : Environ.env -> Libnames.qualid -> Names.inductive
-    val member_message : Pp.t -> bool -> Pp.t
-    val field : string
-    val title : string
-  end) -> Goptions.RefConvertArg with type t = inductive