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
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
{
open Class_tactics
open Stdarg
open Classes
}
DECLARE PLUGIN "rocq-runtime.plugins.ltac"
(** Options: depth, debug and transparency settings. *)
VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
| #[ locality = Attributes.hint_locality ]
[ "Typeclasses" "Transparent" ne_reference_list(cl) ] -> {
set_typeclass_transparency_com ~locality cl true
}
END
VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF
| #[ locality = Attributes.hint_locality ]
[ "Typeclasses" "Opaque" ne_reference_list(cl) ] -> {
set_typeclass_transparency_com ~locality cl false
}
END
{
let pr_debug _prc _prlc _prt b =
if b then Pp.str "debug" else Pp.mt()
}
ARGUMENT EXTEND debug TYPED AS bool PRINTED BY { pr_debug }
| [ "debug" ] -> { true }
| [ ] -> { false }
END
{
let pr_search_strategy_name _prc _prlc _prt = function
| Dfs -> Pp.str "dfs"
| Bfs -> Pp.str "bfs"
let pr_search_strategy _prc _prlc _prt = function
| Some s -> pr_search_strategy_name _prc _prlc _prt s
| None -> Pp.mt ()
}
ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name }
| [ "bfs" ] -> { Bfs }
| [ "dfs" ] -> { Dfs }
END
ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy }
| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s }
| [ ] -> { None }
END
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
| [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> {
set_typeclasses_debug d;
Option.iter set_typeclasses_strategy s;
set_typeclasses_depth depth
}
END
TACTIC EXTEND typeclasses_eauto
| [ "typeclasses" "eauto" "dfs" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d ~strategy:Dfs l }
| [ "typeclasses" "eauto" "bfs" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d ~strategy:Bfs l }
| [ "typeclasses" "eauto" "best_effort" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d ~best_effort:true l }
| [ "typeclasses" "eauto" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d l }
| [ "typeclasses" "eauto" "bfs" nat_or_var_opt(d) ] -> {
typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] }
| [ "typeclasses" "eauto" "dfs" nat_or_var_opt(d) ] -> {
typeclasses_eauto ~depth:d ~strategy:Dfs ~only_classes:true [Class_tactics.typeclasses_db] }
| [ "typeclasses" "eauto" "best_effort" nat_or_var_opt(d) ] -> {
typeclasses_eauto ~depth:d ~only_classes:true ~best_effort:true [Class_tactics.typeclasses_db] }
| [ "typeclasses" "eauto" nat_or_var_opt(d) ] -> {
typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] }
END
TACTIC EXTEND head_of_constr
| [ "head_of_constr" ident(h) constr(c) ] -> { head_of_constr h c }
END
TACTIC EXTEND not_evar
| [ "not_evar" constr(ty) ] -> { not_evar ty }
END
TACTIC EXTEND is_ground
| [ "is_ground" constr(ty) ] -> { is_ground ty }
END
TACTIC EXTEND autoapply
| [ "autoapply" constr(c) "with" preident(i) ] -> { autoapply c i }
END
|
