package coq-waterproof

  1. Overview
  2. Docs

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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
let _ = Mltop.add_known_module "coq-waterproof.plugin"

# 21 "src/databases.mlg"
 

open Pp
open Stdarg

open Hint_dataset
open Hint_dataset_declarations


# 14 "src/databases.ml"

let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-waterproof.plugin") ~command:"DatasetAddSideEff" ~classifier:(fun ~atts:_ _ -> 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 () = Vernactypes.vtdefault (fun () -> 
# 33 "src/databases.mlg"
     
      let dataset_name = Names.Id.to_string dataset in
      load_dataset dataset_name
    
# 33 "src/databases.ml"
) in
            fun dataset ?loc ~atts () ->
            coqpp_body dataset (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-waterproof.plugin") ~command:"DatasetRemoveSideEff" ~classifier:(fun ~atts:_ _ -> 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 () = Vernactypes.vtdefault (fun () -> 
# 41 "src/databases.mlg"
     
      let dataset_name = Names.Id.to_string dataset in
      remove_dataset dataset_name
    
# 56 "src/databases.ml"
) in
            fun dataset ?loc ~atts () ->
            coqpp_body dataset (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-waterproof.plugin") ~command:"DatasetClearSideEff" ~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_sideeff) ?entry:None 
         [(Vernacextend.TyML
         (false,
          Vernacextend.TyTerminal
          ("Waterproof",
           Vernacextend.TyTerminal
           ("Clear",
            Vernacextend.TyTerminal ("Automation", Vernacextend.TyNil))),
          (let coqpp_body () = Vernactypes.vtdefault (fun () -> 
# 49 "src/databases.mlg"
     
      clear_dataset ()
    
# 75 "src/databases.ml"
) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-waterproof.plugin") ~command:"DatasetDeclareSideEff" ~classifier:(fun ~atts:_ _ -> 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 () = Vernactypes.vtdefault (fun () -> 
# 56 "src/databases.mlg"
     
      create_new_dataset (Names.Id.to_string dataset)
    
# 97 "src/databases.ml"
) in
            fun dataset ?loc ~atts () ->
            coqpp_body dataset (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-waterproof.plugin") ~command:"DatasetSetSideEff" ~classifier:(fun ~atts:_ _ -> 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 () =
            Vernactypes.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)
    
# 122 "src/databases.ml"
) in
            fun database_type dataset_name databases ?loc ~atts () ->
            coqpp_body database_type dataset_name databases
              (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-waterproof.plugin") ~command:"DatabaseQuery" ~classifier:(fun ~atts:_ _ -> 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 () = Vernactypes.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))
    
# 147 "src/databases.ml"
) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]