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
let _ = Mltop.add_known_module "coq-waterproof.plugin"

# 21 "src/databases.mlg"
 

open Pp
open Stdarg

open Hint_dataset
open Hint_dataset_declarations



let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-waterproof.plugin") ~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
                                                             () = Vernactypes.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.static_vernac_extend ~plugin:(Some "coq-waterproof.plugin") ~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
                                                             () = Vernactypes.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.static_vernac_extend ~plugin:(Some "coq-waterproof.plugin") ~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 () = 
                                                            Vernactypes.vtdefault (fun () -> 
                                                            
# 49 "src/databases.mlg"
     
      clear_dataset ()
    
                                                            ) 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 _ -> 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)
    
                                                                  ) 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 _ -> 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)
    
                                                                    ) 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 _ -> 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))
    
                                                             ) in fun ?loc ~atts ()
                                                             -> coqpp_body (Attributes.unsupported_attributes atts)), None))]
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct