package coq-waterproof

  1. Overview
  2. Docs
Coq proofs in a style that resembles non-mechanized mathematical proofs

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (3)

Authors

  1. J
    Jelle Wemmenhove
  2. P
    Pim Otte
  3. B
    Balthazar Pathiachvili
  4. D
    Dick Arends
  5. C
    Cosmin Manea
  6. L
    Lulof Pirée
  7. A
    Adrian Vrămuleţ
  8. T
    Tudor Voicu
  9. J
    Jim Portegies <j.w.portegies@tue.nl>

Maintainers

  1. J
    Jim Portegies <j.w.portegies@tue.nl>

Sources

3.1.0+9.1.tar.gz
md5=83359b33c0c6e1fb87f938280cd4e0a2
sha512=d0b0d674e9b5c731b54779d9b77b61f6142d561b05e8c06f2afd0a62e507afedd7696754d29c31522fee996a1f6c6a5d158b250ab04fd9dd5bd812bb99d3a97f

doc/src/coq-waterproof.plugin/databases.ml.html

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))]