Debug flag for variable status

Author: SkySkimmer

dev/top_printers.ml

@@ -318,7 +318,7 @@ let ppelim_constraints cstrs = pp (Sorts.ElimConstraints.pr qprinter cstrs)
 let ppnamedcontextval e =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  pp (pr_named_context env sigma (named_context_of_val e))
+  pp (pr_named_context_of (Environ.reset_with_named_context e env) sigma)
 
 let ppaucontext auctx =
   let {quals = qnas; univs = unas} = AbstractContext.names auctx in

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -1087,6 +1087,12 @@ Controlling display
    after each tactic.  The information is used by the Prooftree tool in Proof
    General. (https://askra.de/software/prooftree)
 
+.. flag:: Printing Variables Status
+
+   This debug :term:`flag` prints whether each variable in the context
+   is a section variable or an hypothesis local to the current proof.
+   It is off by default.
+
 .. extracted from Gallina extensions chapter
 
 .. _printing_constructions_full:

engine/eConstr.ml

@@ -1216,8 +1216,15 @@ let match_named_context_val :
   match unsafe_eq, unsafe_relevance_eq with
   | Refl, Refl -> match_named_context_val
 
+let fold_named_context_val :
+  (named_context_val -> var_status -> named_declaration -> 'a -> 'a) ->
+  named_context_val -> init:'a -> 'a =
+  let Refl, Refl = unsafe_eq, unsafe_relevance_eq in
+  Environ.fold_named_context_val
+
 let fold_named_context :
-  (env -> var_status -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a =
+  (env -> var_status -> named_declaration -> 'a -> 'a) ->
+  env -> init:'a -> 'a =
   let Refl, Refl = unsafe_eq, unsafe_relevance_eq in
   Environ.fold_named_context
 

engine/eConstr.mli

@@ -428,8 +428,13 @@ val val_of_named_context : (var_status * named_declaration) list -> named_contex
 val named_context_of_val : named_context_val -> named_context
 val named_context_of_val_with_status : named_context_val -> (var_status * named_declaration) list
 
+val fold_named_context_val :
+  (named_context_val -> var_status -> named_declaration -> 'a -> 'a) ->
+  named_context_val -> init:'a -> 'a
+
 val fold_named_context :
-  (env -> var_status -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> var_status -> named_declaration -> 'a -> 'a) ->
+  env -> init:'a -> 'a
 
 val lookup_rel : int -> env -> rel_declaration
 val lookup_named : variable -> env -> named_declaration

ide/rocqide/idetop.ml

@@ -207,7 +207,7 @@ let process_goal short sigma g =
     if short then [] else
       let hyps =
         List.rev_map process_hyp
-          (Ppconstr.compact_named_context sigma (EConstr.named_context env))
+          (Ppconstr.compact_named_context sigma (Environ.named_context_val env))
       in
       hyps
   in

kernel/environ.ml

@@ -191,6 +191,11 @@ let set_rel_context_val v env =
 (* Named context *)
 type var_status = SecVar | ProofVar
 
+let var_status_eq a b = match a, b with
+  | SecVar, SecVar -> true
+  | ProofVar, ProofVar -> true
+  | (SecVar | ProofVar), _ -> false
+
 let push_named_context_val status d ctxt =
   let id = NamedDecl.get_id d in
   (*   assert (not (Id.Map.mem id ctxt.env_named_map)); *)
@@ -517,15 +522,18 @@ let pop_rel_context n env =
     env_rel_context = skip n ctxt;
     env_nb_rel = env.env_nb_rel - n }
 
-let fold_named_context f env ~init =
-  let rec fold_right env =
-    match match_named_context_val env.env_named_context with
+let fold_named_context_val f sign ~init =
+  let rec fold_right sign =
+    match match_named_context_val sign with
     | None -> init
     | Some (status, d, rem) ->
-        let env =
-          reset_with_named_context rem env in
-        f env status d (fold_right env)
-  in fold_right env
+      f rem status d (fold_right rem)
+  in fold_right sign
+
+let fold_named_context f env ~init =
+  fold_named_context_val (fun sign status d acc ->
+      f (reset_with_named_context sign env) status d acc)
+    (named_context_val env) ~init
 
 let fold_named_context_reverse f ~init env =
   Context.Named.fold_inside f ~init:init (named_context env)

kernel/environ.mli

@@ -113,6 +113,8 @@ val fold_rel_context :
 
 type var_status = SecVar | ProofVar
 
+val var_status_eq : var_status -> var_status -> bool
+
 val var_status_ctxt : ?check:bool -> Id.t -> named_context_val -> var_status
 val var_status : ?check:bool -> Id.t -> env -> var_status
 
@@ -149,8 +151,13 @@ val named_body : variable -> env -> constr option
 
 (** {6 Recurrence on [named_context]: older declarations processed first } *)
 
+val fold_named_context_val :
+  (named_context_val -> var_status -> Constr.named_declaration -> 'a -> 'a) ->
+  named_context_val -> init:'a -> 'a
+
 val fold_named_context :
-  (env -> var_status -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> var_status -> Constr.named_declaration -> 'a -> 'a) ->
+  env -> init:'a -> 'a
 
 val match_named_context_val : named_context_val -> (var_status * named_declaration * named_context_val) option
 

printing/ppconstr.ml

@@ -858,39 +858,40 @@ let pr_binders ~flags env sigma l : Pp.t = pr_undelimited_binders ~flags spc tru
 
 module CompactedDecl = struct
   type t =
-    | LocalAssum of Id.t EConstr.binder_annot list * EConstr.types
-    | LocalDef of Id.t EConstr.binder_annot list * EConstr.constr * EConstr.types
+    | LocalAssum of Environ.var_status * Id.t EConstr.binder_annot list * EConstr.types
+    | LocalDef of Environ.var_status * Id.t EConstr.binder_annot list * EConstr.constr * EConstr.types
 
-  let of_named_decl = function
+  let of_named_decl status = function
     | Context.Named.Declaration.LocalAssum (id,t) ->
-      LocalAssum ([id],t)
+      LocalAssum (status, [id], t)
     | Context.Named.Declaration.LocalDef (id,v,t) ->
-      LocalDef ([id],v,t)
+      LocalDef (status, [id], v, t)
 
   let to_tuple = function
-    | LocalAssum (ids, t) -> ids, None, t
-    | LocalDef (ids, b, t) -> ids, Some b, t
+    | LocalAssum (_, ids, t) -> ids, None, t
+    | LocalDef (_, ids, b, t) -> ids, Some b, t
 end
 
 let compact_named_context sigma sign =
   let module NamedDecl = Context.Named.Declaration in
-  let compact l decl =
+  let compact l status decl =
     match decl, l with
     | NamedDecl.LocalAssum (i,t), [] ->
-       [CompactedDecl.LocalAssum ([i],t)]
+      [CompactedDecl.LocalAssum (status,[i],t)]
     | NamedDecl.LocalDef (i,c,t), [] ->
-       [CompactedDecl.LocalDef ([i],c,t)]
-    | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q ->
-       if EConstr.eq_constr sigma t1 t2
-       then CompactedDecl.LocalAssum (i1::li, t2) :: q
-       else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q
-    | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q ->
-       if EConstr.eq_constr sigma c1 c2 && EConstr.eq_constr sigma t1 t2
-       then CompactedDecl.LocalDef (i1::li, c2, t2) :: q
-       else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q
+      [CompactedDecl.LocalDef (status,[i],c,t)]
+    | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (status',li,t2) :: q ->
+      if Environ.var_status_eq status status' && EConstr.eq_constr sigma t1 t2
+      then CompactedDecl.LocalAssum (status, i1::li, t2) :: q
+      else CompactedDecl.LocalAssum (status, [i1],t1) :: CompactedDecl.LocalAssum (status',li,t2) :: q
+    | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (status',li,c2,t2) :: q ->
+      if Environ.var_status_eq status status' &&
+         EConstr.eq_constr sigma c1 c2 && EConstr.eq_constr sigma t1 t2
+      then CompactedDecl.LocalDef (status, i1::li, c2, t2) :: q
+      else CompactedDecl.LocalDef (status, [i1],c1,t1) :: CompactedDecl.LocalDef (status',li,c2,t2) :: q
     | NamedDecl.LocalAssum (i,t), q ->
-       CompactedDecl.LocalAssum ([i],t) :: q
+      CompactedDecl.LocalAssum (status,[i],t) :: q
     | NamedDecl.LocalDef (i,c,t), q ->
-       CompactedDecl.LocalDef ([i],c,t) :: q
+      CompactedDecl.LocalDef (status,[i],c,t) :: q
   in
-  sign |> Context.Named.fold_inside compact ~init:[] |> List.rev
+  EConstr.fold_named_context_val (fun _ status d acc -> compact acc status d) sign ~init:[]

printing/ppconstr.mli

@@ -99,14 +99,15 @@ val modular_constr_pr :
 
 module CompactedDecl : sig
   type t =
-    | LocalAssum of Id.t EConstr.binder_annot list * EConstr.types
-    | LocalDef of Id.t EConstr.binder_annot list * EConstr.constr * EConstr.types
+    | LocalAssum of Environ.var_status * Id.t EConstr.binder_annot list * EConstr.types
+    | LocalDef of Environ.var_status * Id.t EConstr.binder_annot list * EConstr.constr * EConstr.types
 
-  val of_named_decl : EConstr.named_declaration -> t
+  val of_named_decl : Environ.var_status -> EConstr.named_declaration -> t
 
   val to_tuple : t ->
     Id.t EConstr.binder_annot list *
     EConstr.constr option *
     EConstr.types
 end
-val compact_named_context : Evd.evar_map -> EConstr.named_context -> CompactedDecl.t list
+
+val compact_named_context : Evd.evar_map -> Environ.named_context_val -> CompactedDecl.t list

printing/printer.ml

@@ -359,32 +359,40 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
 
 (* Flag for compact display of goals *)
 
-let get_compact_context,set_compact_context =
-  let compact_context = ref false in
-  (fun () -> !compact_context),(fun b  -> compact_context := b)
+let { Goptions.get = get_compact_context } =
+  Goptions.declare_bool_option_and_ref ~key:["Printing";"Compact";"Contexts"] ~value:false ()
+
+let { Goptions.get = print_var_status } =
+  Goptions.declare_bool_option_and_ref ~key:["Printing";"Variables";"Status"] ~value:false ()
 
 let pr_ecompacted_decl ?flags env sigma decl =
-  let ids, pbody, typ = match decl with
-    | CompactedDecl.LocalAssum (ids, typ) ->
-       ids, None, typ
-    | CompactedDecl.LocalDef (ids,c,typ) ->
-       (* Force evaluation *)
-       let pb = pr_leconstr_env ?flags ~inctx:true env sigma c in
-       let pb = if EConstr.isCast sigma c then surround pb else pb in
-       ids, Some pb, typ in
+  let status, ids, pbody, typ = match decl with
+    | CompactedDecl.LocalAssum (status, ids, typ) ->
+      status, ids, None, typ
+    | CompactedDecl.LocalDef (status, ids, c, typ) ->
+      (* Force evaluation *)
+      let pb = pr_leconstr_env ?flags ~inctx:true env sigma c in
+      let pb = if EConstr.isCast sigma c then surround pb else pb in
+      status, ids, Some pb, typ in
   let pids =
     hov 0 (prlist_with_sep pr_comma (fun id -> pr_id id.binder_name) ids) in
   let pt = pr_letype_env ?flags env sigma typ in
+  let pstatus = if print_var_status() then
+      match status with
+      | SecVar -> spc() ++ pr_in_comment (str "section variable")
+      | ProofVar -> spc() ++ pr_in_comment (str "hypothesis")
+    else mt()
+  in
   match pbody with
-  | None -> hov 2 (pids ++ str" :" ++ spc () ++ pt)
+  | None -> hov 2 (pids ++ str" :" ++ spc () ++ pt ++ pstatus)
   | Some pbody ->
-     hov 2 (pids ++ str" :=" ++ spc () ++ pbody ++ spc () ++ str": " ++ pt)
+    hov 2 (pids ++ str" :=" ++ spc () ++ pbody ++ spc () ++ str": " ++ pt ++ pstatus)
 
-let pr_enamed_decl ?flags env sigma decl =
-  decl |> CompactedDecl.of_named_decl |> pr_ecompacted_decl ?flags env sigma
+let pr_enamed_decl ?flags env sigma status decl =
+  decl |> CompactedDecl.of_named_decl status |> pr_ecompacted_decl ?flags env sigma
 
-let pr_named_decl ?flags env sigma (decl:Constr.named_declaration) =
-  pr_enamed_decl ?flags env sigma (EConstr.of_named_decl decl)
+let pr_named_decl ?flags env sigma status (decl:Constr.named_declaration) =
+  pr_enamed_decl ?flags env sigma status (EConstr.of_named_decl decl)
 
 let pr_rel_decl ?flags env sigma decl =
   let na = RelDecl.get_name decl in
@@ -413,18 +421,13 @@ let pr_erel_decl ?flags env sigma (decl:EConstr.rel_declaration) =
 
 (* Prints a signature, all declarations on the same line if possible *)
 let pr_named_context_of ?flags env sigma =
-  let make_decl_list env _status d pps = pr_named_decl ?flags env sigma d :: pps in
+  let make_decl_list env status d pps = pr_named_decl ?flags env sigma status d :: pps in
   let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in
   hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
 
 let pr_var_list_decl ?flags env sigma decl =
   hov 0 (pr_ecompacted_decl ?flags env sigma decl)
 
-let pr_named_context ?flags env sigma ne_context =
-  hv 0 (Context.Named.fold_outside
-          (fun d pps -> pps ++ ws 2 ++ pr_named_decl ?flags env sigma d)
-          ne_context ~init:(mt ()))
-
 let pr_rel_context ?(flags=current_combined()) env sigma rel_context =
   let ppflags = Ppconstr.of_printing_flags flags in
   let rel_context = EConstr.of_rel_context rel_context in
@@ -440,7 +443,7 @@ let pr_context_unlimited ?flags env sigma =
       (fun d pps ->
          let pidt =  pr_ecompacted_decl ?flags env sigma d in
          (pps ++ fnl () ++ pidt))
-      (compact_named_context sigma (EConstr.named_context env)) (mt ())
+      (compact_named_context sigma (Environ.named_context_val env)) (mt ())
   in
   let db_env =
     fold_rel_context
@@ -469,7 +472,7 @@ let should_compact env sigma typ =
 let rec bld_sign_env ?flags env sigma ctxt pps =
   match ctxt with
   | [] -> pps
-  | CompactedDecl.LocalAssum (ids,typ)::ctxt' when should_compact env sigma typ ->
+  | CompactedDecl.LocalAssum (_,ids,typ)::ctxt' when should_compact env sigma typ ->
     let pps',ctxt' = bld_sign_env_id ?flags env sigma ctxt (mt ()) true in
     (* putting simple hyps in a more horizontal flavor *)
     bld_sign_env ?flags env sigma ctxt' (pps ++ brk (0,0) ++ hov 0 pps')
@@ -480,7 +483,7 @@ let rec bld_sign_env ?flags env sigma ctxt pps =
 and bld_sign_env_id ?flags env sigma ctxt pps is_start =
   match ctxt with
   | [] -> pps,ctxt
- | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ ->
+ | CompactedDecl.LocalAssum(_,ids,typ) as d :: ctxt' when should_compact env sigma typ ->
     let pidt = pr_var_list_decl ?flags env sigma d in
     let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in
     bld_sign_env_id ?flags env sigma ctxt' pps' false
@@ -490,7 +493,7 @@ and bld_sign_env_id ?flags env sigma ctxt pps is_start =
 (* compact printing an env (variables and de Bruijn). Separator: three
    spaces between simple hyps, and newline otherwise *)
 let pr_context_limit_compact ?n ?flags env sigma =
-  let ctxt = EConstr.named_context env in
+  let ctxt = Environ.named_context_val env in
   let ctxt = compact_named_context sigma ctxt in
   let lgth = List.length ctxt in
   let n_capped =