Source file databases.ml
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
let _ = Mltop.add_known_module "coq-waterproof.databases"
# 21 "src/databases.mlg"
open Pp
open Stdarg
open Hint_dataset
open Hint_dataset_declarations
let () = Vernacextend.vernac_extend ~plugin:"coq-waterproof.databases" ~command:"DatasetAddSideEff" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None
[(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Waterproof",
Vernacextend.TyTerminal ("Enable",
Vernacextend.TyTerminal ("Automation",
Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_ident),
Vernacextend.TyNil)))), (let coqpp_body dataset
() = Vernacextend.vtdefault (fun () ->
# 33 "src/databases.mlg"
let dataset_name = Names.Id.to_string dataset in
load_dataset dataset_name
) in fun dataset
?loc ~atts ()
-> coqpp_body dataset
(Attributes.unsupported_attributes atts)), None))]
let () = Vernacextend.vernac_extend ~plugin:"coq-waterproof.databases" ~command:"DatasetRemoveSideEff" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None
[(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Waterproof",
Vernacextend.TyTerminal ("Disable",
Vernacextend.TyTerminal ("Automation",
Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_ident),
Vernacextend.TyNil)))), (let coqpp_body dataset
() = Vernacextend.vtdefault (fun () ->
# 41 "src/databases.mlg"
let dataset_name = Names.Id.to_string dataset in
remove_dataset dataset_name
) in fun dataset
?loc ~atts ()
-> coqpp_body dataset
(Attributes.unsupported_attributes atts)), None))]
let () = Vernacextend.vernac_extend ~plugin:"coq-waterproof.databases" ~command:"DatasetClearSideEff" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None
[(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Waterproof",
Vernacextend.TyTerminal ("Clear",
Vernacextend.TyTerminal ("Automation",
Vernacextend.TyNil))), (let coqpp_body () =
Vernacextend.vtdefault (fun () ->
# 49 "src/databases.mlg"
clear_dataset ()
) in fun ?loc ~atts ()
-> coqpp_body (Attributes.unsupported_attributes atts)), None))]
let () = Vernacextend.vernac_extend ~plugin:"coq-waterproof.databases" ~command:"DatasetDeclareSideEff" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None
[(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Waterproof",
Vernacextend.TyTerminal ("Declare",
Vernacextend.TyTerminal ("Automation",
Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_ident),
Vernacextend.TyNil)))), (let coqpp_body dataset
() = Vernacextend.vtdefault (fun () ->
# 56 "src/databases.mlg"
create_new_dataset (Names.Id.to_string dataset)
) in fun dataset
?loc ~atts ()
-> coqpp_body dataset
(Attributes.unsupported_attributes atts)), None))]
let () = Vernacextend.vernac_extend ~plugin:"coq-waterproof.databases" ~command:"DatasetSetSideEff" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None
[(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Waterproof",
Vernacextend.TyTerminal ("Set",
Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_ident),
Vernacextend.TyTerminal ("Databases",
Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_ident),
Vernacextend.TyNonTerminal (Extend.TUlist0sep (
Extend.TUentry (Genarg.get_arg_tag wit_ident), ","),
Vernacextend.TyNil)))))), (let coqpp_body database_type
dataset_name
databases
() = Vernacextend.vtdefault (fun () ->
# 63 "src/databases.mlg"
populate_dataset (Names.Id.to_string dataset_name) (database_type_of_string @@ Names.Id.to_string database_type) (List.map Names.Id.to_string databases)
) in fun database_type
dataset_name
databases
?loc ~atts ()
-> coqpp_body database_type
dataset_name
databases
(Attributes.unsupported_attributes atts)), None))]
let () = Vernacextend.vernac_extend ~plugin:"coq-waterproof.databases" ~command:"DatabaseQuery" ~classifier:(fun _ -> Vernacextend.classify_as_query) ?entry:None
[(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Waterproof",
Vernacextend.TyTerminal ("List",
Vernacextend.TyTerminal ("Automation",
Vernacextend.TyTerminal ("Databases",
Vernacextend.TyNil)))), (let coqpp_body () =
Vernacextend.vtdefault (fun () ->
# 70 "src/databases.mlg"
Feedback.msg_notice ((str "Loaded datasets : ") ++ (List.fold_left (fun acc dataset_name -> acc ++ str " " ++ str dataset_name) (str "") !loaded_hint_dataset));
Feedback.msg_notice ((str "Main databases :") ++ List.fold_left (fun acc database_name -> acc ++ str " " ++ str database_name) (str "") (get_current_databases Main));
Feedback.msg_notice ((str "Decidability databases :") ++ List.fold_left (fun acc database_name -> acc ++ str " " ++ str database_name) (str "") (get_current_databases Decidability));
Feedback.msg_notice ((str "Shorten databases :") ++ List.fold_left (fun acc database_name -> acc ++ str " " ++ str database_name) (str "") (get_current_databases Shorten))
) in fun ?loc ~atts ()
-> coqpp_body (Attributes.unsupported_attributes atts)), None))]