1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
open Pp
open Names
open Printer
open Tacmach
open Ssrmatching_plugin
open Ssrast
let pr_spc () = str " "
let pr_bar () = Pp.cut() ++ str "|"
let pr_list = prlist_with_sep
let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs ->
hd ++ List.fold_left (fun acc x -> acc ++ sep ++ x) x xs
let pp_term gl t =
let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t
(* FIXME *)
(* terms are pre constr, the kind is parsing/printing flag to distinguish
* between x, @x and (x). It affects automatic clear and let-in preservation.
* Cpattern is a temporary flag that becomes InParens ASAP. *)
(* type ssrtermkind = InParens | WithAt | NoFlag | Cpattern *)
let xInParens = '('
let xWithAt = '@'
let xNoFlag = ' '
let xCpattern = 'x'
(* Term printing utilities functions for deciding bracketing. *)
let pr_paren prx x = hov 1 (str "(" ++ prx x ++ str ")")
(* String lexing utilities *)
let skip_wschars s =
let rec loop i = match s.[i] with '\n'..' ' -> loop (i + 1) | _ -> i in loop
(* We also guard characters that might interfere with the ssreflect *)
(* tactic syntax. *)
let guard_term ch1 s i = match s.[i] with
| '(' -> false
| '{' | '/' | '=' -> true
| _ -> ch1 = xInParens
(* We also guard characters that might interfere with the ssreflect *)
(* tactic syntax. *)
let pr_guarded guard prc c =
pp_with Format.str_formatter (prc c);
let s = Format.flush_str_formatter () ^ "$" in
if guard s (skip_wschars s 0) then pr_paren prc c else prc c
let prl_constr_expr = Ppconstr.pr_lconstr_expr
let pr_glob_constr c = Printer.pr_glob_constr_env (Global.env ()) c
let prl_glob_constr c = Printer.pr_lglob_constr_env (Global.env ()) c
let pr_glob_constr_and_expr = function
| _, Some c -> Ppconstr.pr_constr_expr c
| c, None -> pr_glob_constr c
let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
let pr_hyp (SsrHyp (_, id)) = Id.print id
let pr_hyps = pr_list pr_spc pr_hyp
let pr_occ = function
| Some (true, occ) -> str "{-" ++ pr_list pr_spc int occ ++ str "}"
| Some (false, occ) -> str "{+" ++ pr_list pr_spc int occ ++ str "}"
| None -> str "{}"
let pr_clear_ne clr = str "{" ++ pr_hyps clr ++ str "}"
let pr_clear sep clr = if clr = [] then mt () else sep () ++ pr_clear_ne clr
let pr_dir = function L2R -> str "->" | R2L -> str "<-"
let pr_simpl = function
| Simpl -1 -> str "/="
| Cut -1 -> str "//"
| Simpl n -> str "/" ++ int n ++ str "="
| Cut n -> str "/" ++ int n ++ str"/"
| SimplCut (-1,-1) -> str "//="
| SimplCut (n,-1) -> str "/" ++ int n ++ str "/="
| SimplCut (-1,n) -> str "//" ++ int n ++ str "="
| SimplCut (n,m) -> str "/" ++ int n ++ str "/" ++ int m ++ str "="
| Nop -> mt ()
(* New terms *)
let pr_ast_closure_term { body } = Ppconstr.pr_constr_expr body
let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c)
let rec pr_ipat p =
match p with
| IPatId id -> Id.print id
| IPatSimpl sim -> pr_simpl sim
| IPatClear clr -> pr_clear mt clr
| IPatCase iorpat -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]")
| IPatDispatch iorpat -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ str "]")
| IPatInj iorpat -> hov 1 (str "[=" ++ pr_iorpat iorpat ++ str "]")
| IPatRewrite (occ, dir) -> pr_occ occ ++ pr_dir dir
| IPatAnon All -> str "*"
| IPatAnon Drop -> str "_"
| IPatAnon One -> str "?"
| IPatView v -> pr_view2 v
| IPatNoop -> str "-"
| IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]"
| IPatTac _ -> str "<tac>"
(* TODO | IPatAnon Temporary -> str "+" *)
and pr_ipats ipats = pr_list spc pr_ipat ipats
and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat
(* 0 cost pp function. Active only if Debug Ssreflect is Set *)
let ppdebug_ref = ref (fun _ -> ())
let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s)
let _ =
Goptions.declare_bool_option
{ Goptions.optname = "ssreflect debugging";
Goptions.optkey = ["Debug";"Ssreflect"];
Goptions.optdepr = false;
Goptions.optread = (fun _ -> !ppdebug_ref == ssr_pp);
Goptions.optwrite = (fun b ->
Ssrmatching.debug b;
if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) }
let ppdebug s = !ppdebug_ref s
|
