<commit_before>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Names
open Namegen
open Errors
open Util
open Constrexpr
open Tacexpr
open Genarg
open Constrarg
open Libnames
open Ppextend
open Misctypes
open Locus
open Decl_kinds
open Genredexpr
open Ppconstr
open Printer

let pr_global x = Nametab.pr_global_env Id.Set.empty x

type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list

type pp_tactic = {
  pptac_level : int;
  pptac_prods : grammar_terminals;
}

(* Tactic notations *)
let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty

let declare_notation_tactic_pprule kn pt =
  prnotation_tab := KNmap.add kn pt !prnotation_tab

type 'a raw_extra_genarg_printer =
    (constr_expr -> std_ppcmds) ->
    (constr_expr -> std_ppcmds) ->
    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
    'a -> std_ppcmds

type 'a glob_extra_genarg_printer =
    (glob_constr_and_expr -> std_ppcmds) ->
    (glob_constr_and_expr -> std_ppcmds) ->
    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
    'a -> std_ppcmds

type 'a extra_genarg_printer =
    (Term.constr -> std_ppcmds) ->
    (Term.constr -> std_ppcmds) ->
    (tolerability -> Val.t -> std_ppcmds) ->
    'a -> std_ppcmds

let genarg_pprule = ref String.Map.empty

let declare_extra_genarg_pprule wit f g h =
  let s = match wit with
    | ExtraArg s -> ArgT.repr s
    | _ -> error
      "Can declare a pretty-printing rule only for extra argument types."
  in
  let f prc prlc prtac x = f prc prlc prtac (out_gen (rawwit wit) x) in
  let g prc prlc prtac x = g prc prlc prtac (out_gen (glbwit wit) x) in
  let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in
  genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule

module Make
  (Ppconstr : Ppconstrsig.Pp)
  (Taggers : sig
      val tag_keyword
        : std_ppcmds -> std_ppcmds
      val tag_primitive
        : std_ppcmds -> std_ppcmds
      val tag_string
        : std_ppcmds -> std_ppcmds
      val tag_glob_tactic_expr
        : glob_tactic_expr -> std_ppcmds -> std_ppcmds
      val tag_glob_atomic_tactic_expr
        : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
      val tag_raw_tactic_expr
        : raw_tactic_expr -> std_ppcmds -> std_ppcmds
      val tag_raw_atomic_tactic_expr
        : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
      val tag_atomic_tactic_expr
        : atomic_tactic_expr -> std_ppcmds -> std_ppcmds
  end)
= struct

  open Taggers

  let keyword x = tag_keyword (str x)
  let primitive x = tag_primitive (str x)

  let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with
  | Val.List tag ->
    pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x
  | Val.Opt tag -> pr_opt_no_spc (fun x -> pr_value lev (Val.Dyn (tag, x))) x
  | Val.Pair (tag1, tag2) ->
    str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++
      pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")"
  | Val.Base t ->
    let name = Val.repr t in
    let default = str "<" ++ str name ++ str ">" in
    match ArgT.name name with
    | None -> default
    | Some (ArgT.Any arg) ->
      let wit = ExtraArg arg in
      match Val.eq (val_tag (Topwit wit)) (Val.Base t) with
      | None -> default
      | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)

  let pr_with_occurrences pr (occs,c) =
    match occs with
      | AllOccurrences ->
        pr c
      | NoOccurrences ->
        failwith "pr_with_occurrences: no occurrences"
      | OnlyOccurrences nl ->
        hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
                 hov 0 (prlist_with_sep spc (pr_or_var int) nl))
      | AllOccurrencesBut nl ->
        hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
                 hov 0 (prlist_with_sep spc (pr_or_var int) nl))

  exception ComplexRedFlag

  let pr_short_red_flag pr r =
    if not r.rBeta ||  not r.rIota ||  not r.rZeta then raise ComplexRedFlag
    else if List.is_empty r.rConst then
      if r.rDelta then mt () else raise ComplexRedFlag
    else (if r.rDelta then str "-" else mt ()) ++
	   hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")

  let pr_red_flag pr r =
    try pr_short_red_flag pr r
    with complexRedFlags ->
      (if r.rBeta then pr_arg str "beta" else mt ()) ++
	(if r.rIota then pr_arg str "iota" else mt ()) ++
	(if r.rZeta then pr_arg str "zeta" else mt ()) ++
	(if List.is_empty r.rConst then
	   if r.rDelta then pr_arg str "delta"
	   else mt ()
	 else
	   pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
	     hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))

  let pr_union pr1 pr2 = function
    | Inl a -> pr1 a
    | Inr b -> pr2 b

  let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
    | Red false -> keyword "red"
    | Hnf -> keyword "hnf"
    | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
		     ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
    | Cbv f ->
      if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then
        keyword "compute"
      else
        hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
    | Lazy f ->
      hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
    | Cbn f ->
      hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
    | Unfold l ->
      hov 1 (keyword "unfold" ++ spc() ++
               prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l)
    | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
    | Pattern l ->
      hov 1 (keyword "pattern" ++
               pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l)

    | Red true ->
      error "Shouldn't be accessible from user."
    | ExtraRedExpr s ->
      str s
    | CbvVm o ->
      keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
    | CbvNative o ->
      keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o

  let pr_may_eval test prc prlc pr2 pr3 = function
    | ConstrEval (r,c) ->
      hov 0
        (keyword "eval" ++ brk (1,1) ++
           pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
           keyword "in" ++ spc() ++ prc c)
    | ConstrContext ((_,id),c) ->
      hov 0
        (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
           str "[" ++ prlc c ++ str "]")
    | ConstrTypeOf c ->
      hov 1 (keyword "type of" ++ spc() ++ prc c)
    | ConstrTerm c when test c ->
      h 0 (str "(" ++ prc c ++ str ")")
    | ConstrTerm c ->
      prc c

  let pr_may_eval a =
    pr_may_eval (fun _ -> false) a

  let pr_arg pr x = spc () ++ pr x

  let pr_or_var pr = function
    | ArgArg x -> pr x
    | ArgVar (_,s) -> pr_id s

  let pr_and_short_name pr (c,_) = pr c

  let pr_or_by_notation f = function
    | AN v -> f v
    | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
<commit_msg>Protect printing of ltac's "context [...]" from possible collision with user-level notations by inserting spaces.<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Names
open Namegen
open Errors
open Util
open Constrexpr
open Tacexpr
open Genarg
open Constrarg
open Libnames
open Ppextend
open Misctypes
open Locus
open Decl_kinds
open Genredexpr
open Ppconstr
open Printer

let pr_global x = Nametab.pr_global_env Id.Set.empty x

type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list

type pp_tactic = {
  pptac_level : int;
  pptac_prods : grammar_terminals;
}

(* Tactic notations *)
let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty

let declare_notation_tactic_pprule kn pt =
  prnotation_tab := KNmap.add kn pt !prnotation_tab

type 'a raw_extra_genarg_printer =
    (constr_expr -> std_ppcmds) ->
    (constr_expr -> std_ppcmds) ->
    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
    'a -> std_ppcmds

type 'a glob_extra_genarg_printer =
    (glob_constr_and_expr -> std_ppcmds) ->
    (glob_constr_and_expr -> std_ppcmds) ->
    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
    'a -> std_ppcmds

type 'a extra_genarg_printer =
    (Term.constr -> std_ppcmds) ->
    (Term.constr -> std_ppcmds) ->
    (tolerability -> Val.t -> std_ppcmds) ->
    'a -> std_ppcmds

let genarg_pprule = ref String.Map.empty

let declare_extra_genarg_pprule wit f g h =
  let s = match wit with
    | ExtraArg s -> ArgT.repr s
    | _ -> error
      "Can declare a pretty-printing rule only for extra argument types."
  in
  let f prc prlc prtac x = f prc prlc prtac (out_gen (rawwit wit) x) in
  let g prc prlc prtac x = g prc prlc prtac (out_gen (glbwit wit) x) in
  let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in
  genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule

module Make
  (Ppconstr : Ppconstrsig.Pp)
  (Taggers : sig
      val tag_keyword
        : std_ppcmds -> std_ppcmds
      val tag_primitive
        : std_ppcmds -> std_ppcmds
      val tag_string
        : std_ppcmds -> std_ppcmds
      val tag_glob_tactic_expr
        : glob_tactic_expr -> std_ppcmds -> std_ppcmds
      val tag_glob_atomic_tactic_expr
        : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
      val tag_raw_tactic_expr
        : raw_tactic_expr -> std_ppcmds -> std_ppcmds
      val tag_raw_atomic_tactic_expr
        : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
      val tag_atomic_tactic_expr
        : atomic_tactic_expr -> std_ppcmds -> std_ppcmds
  end)
= struct

  open Taggers

  let keyword x = tag_keyword (str x)
  let primitive x = tag_primitive (str x)

  let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with
  | Val.List tag ->
    pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x
  | Val.Opt tag -> pr_opt_no_spc (fun x -> pr_value lev (Val.Dyn (tag, x))) x
  | Val.Pair (tag1, tag2) ->
    str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++
      pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")"
  | Val.Base t ->
    let name = Val.repr t in
    let default = str "<" ++ str name ++ str ">" in
    match ArgT.name name with
    | None -> default
    | Some (ArgT.Any arg) ->
      let wit = ExtraArg arg in
      match Val.eq (val_tag (Topwit wit)) (Val.Base t) with
      | None -> default
      | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)

  let pr_with_occurrences pr (occs,c) =
    match occs with
      | AllOccurrences ->
        pr c
      | NoOccurrences ->
        failwith "pr_with_occurrences: no occurrences"
      | OnlyOccurrences nl ->
        hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
                 hov 0 (prlist_with_sep spc (pr_or_var int) nl))
      | AllOccurrencesBut nl ->
        hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
                 hov 0 (prlist_with_sep spc (pr_or_var int) nl))

  exception ComplexRedFlag

  let pr_short_red_flag pr r =
    if not r.rBeta ||  not r.rIota ||  not r.rZeta then raise ComplexRedFlag
    else if List.is_empty r.rConst then
      if r.rDelta then mt () else raise ComplexRedFlag
    else (if r.rDelta then str "-" else mt ()) ++
	   hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")

  let pr_red_flag pr r =
    try pr_short_red_flag pr r
    with complexRedFlags ->
      (if r.rBeta then pr_arg str "beta" else mt ()) ++
	(if r.rIota then pr_arg str "iota" else mt ()) ++
	(if r.rZeta then pr_arg str "zeta" else mt ()) ++
	(if List.is_empty r.rConst then
	   if r.rDelta then pr_arg str "delta"
	   else mt ()
	 else
	   pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
	     hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))

  let pr_union pr1 pr2 = function
    | Inl a -> pr1 a
    | Inr b -> pr2 b

  let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
    | Red false -> keyword "red"
    | Hnf -> keyword "hnf"
    | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
		     ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
    | Cbv f ->
      if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then
        keyword "compute"
      else
        hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
    | Lazy f ->
      hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
    | Cbn f ->
      hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
    | Unfold l ->
      hov 1 (keyword "unfold" ++ spc() ++
               prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l)
    | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
    | Pattern l ->
      hov 1 (keyword "pattern" ++
               pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l)

    | Red true ->
      error "Shouldn't be accessible from user."
    | ExtraRedExpr s ->
      str s
    | CbvVm o ->
      keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
    | CbvNative o ->
      keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o

  let pr_may_eval test prc prlc pr2 pr3 = function
    | ConstrEval (r,c) ->
      hov 0
        (keyword "eval" ++ brk (1,1) ++
           pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
           keyword "in" ++ spc() ++ prc c)
    | ConstrContext ((_,id),c) ->
      hov 0
        (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
           str "[ " ++ prlc c ++ str " ]")
    | ConstrTypeOf c ->
      hov 1 (keyword "type of" ++ spc() ++ prc c)
    | ConstrTerm c when test c ->
      h 0 (str "(" ++ prc c ++ str ")")
    | ConstrTerm c ->
      prc c

  let pr_may_eval a =
    pr_may_eval (fun _ -> false) a

  let pr_arg pr x = spc () ++ pr x

  let pr_or_var pr = function
    | ArgArg x -> pr x
    | ArgVar (_,s) -> pr_id s

  let pr_and_short_name pr (c,_) = pr c

  let pr_or_by_notation f = function
    | AN v -> f v
    | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc

{'fraction_non_alphanumeric': 0.13994876634757988, 'fraction_numerical': 0.005393016044222732, 'mean_word_length': 2.586798839458414, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 165, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4698694', 'n_tokens_mistral': 5640, 'n_tokens_neox': 5416, 'n_words': 1585}