package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file g_ground.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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224

# 11 "plugins/firstorder/g_ground.mlg"
 

open Ltac_plugin
open Sequent
open Ground
open Goptions
open Tacmach
open Tacticals
open Tacinterp
open Stdarg
open Tacarg
open Pcoq.Prim



let _ = Mltop.add_known_module "coq-core.plugins.firstorder"

# 30 "plugins/firstorder/g_ground.mlg"
 

let { Goptions.get = ground_depth } =
  declare_nat_option_and_ref
    ~key:["Firstorder";"Depth"]
    ~value:3
    ()

let default_intuition_tac =
  let tac _ _ = Auto.h_auto None [] (Some []) in
  let name = { Tacexpr.mltac_plugin = "coq-core.plugins.firstorder"; mltac_tactic = "auto_with"; } in
  let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
  Tacenv.register_ml_tactic name [| tac |];
  CAst.make (Tacexpr.TacML (entry, []))

let (set_default_solver, default_solver, print_default_solver) =
  Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"



let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-core.plugins.firstorder") ~command:"Firstorder_Set_Solver" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None 
         [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Set", 
                                     Vernacextend.TyTerminal ("Firstorder", 
                                     Vernacextend.TyTerminal ("Solver", 
                                     Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_tactic), 
                                     Vernacextend.TyNil)))), (let coqpp_body t
                                                             locality = 
                                                             Vernactypes.vtdefault (fun () -> 
                                                             
# 51 "plugins/firstorder/g_ground.mlg"
                                                                                                   
      set_default_solver
        locality
        (Tacintern.glob_tactic t)
  
                                                             ) in fun t
                                                             ?loc ~atts ()
                                                             -> coqpp_body t
                                                             (Attributes.parse Tactic_option.tac_option_locality atts)), None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-core.plugins.firstorder") ~command:"Firstorder_Print_Solver" ~classifier:(fun _ -> Vernacextend.classify_as_query) ?entry:None 
         [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Print", 
                                     Vernacextend.TyTerminal ("Firstorder", 
                                     Vernacextend.TyTerminal ("Solver", 
                                     Vernacextend.TyNil))), (let coqpp_body () = 
                                                            Vernactypes.vtdefault (fun () -> 
                                                            
# 59 "plugins/firstorder/g_ground.mlg"
                                        
    Feedback.msg_notice
      (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) 
                                                            ) in fun ?loc ~atts ()
                                                            -> coqpp_body (Attributes.unsupported_attributes atts)), None))]


# 64 "plugins/firstorder/g_ground.mlg"
 

let gen_ground_tac flag taco ids bases =
  let flags = Ground.get_flags flag in
  Proofview.tclOR begin
  Proofview.Goal.enter begin fun gl ->
      let solver=
        match taco with
        | Some tac -> tac
        | None-> default_solver ()
      in
      let startseq k =
        Proofview.Goal.enter begin fun gl ->
        let seq=empty_seq (ground_depth ()) in
        let seq, sigma = extend_with_ref_list ~flags (pf_env gl) (project gl) ids seq in
        let seq, sigma = extend_with_auto_hints ~flags (pf_env gl) sigma bases seq in
        tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
        end
      in
      let result=ground_tac ~flags solver startseq in
      result
  end
  end
  (fun (e, info) -> Proofview.tclZERO ~info e)

(* special for compatibility with Intuition

let constant str = Coqlib.get_constr str

let defined_connectives=lazy
  [[],EvalConstRef (destConst (constant "core.not.type"));
   [],EvalConstRef (destConst (constant "core.iff.type"))]

let normalize_evaluables=
  onAllHypsAndConcl
    (function
         None->unfold_in_concl (Lazy.force defined_connectives)
       | Some id->
           unfold_in_hyp (Lazy.force defined_connectives)
           (Tacexpr.InHypType id)) *)

open Ppconstr
open Printer
let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid
let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (Pputils.pr_or_var (fun x -> pr_global (snd x)))
let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global



let (wit_firstorder_using, firstorder_using) = Tacentries.argument_extend ~plugin:"coq-core.plugins.firstorder" ~name:"firstorder_using" 
                                               {
                                               Tacentries.arg_parsing = 
                                               Vernacextend.Arg_rules (
                                               [(Pcoq.Production.make
                                                 (Pcoq.Rule.stop)
                                                 (fun loc -> 
# 119 "plugins/firstorder/g_ground.mlg"
           [] 
                                                             ));
                                               (Pcoq.Production.make
                                                (Pcoq.Rule.next (Pcoq.Rule.next 
                                                                (Pcoq.Rule.stop)
                                                                ((Pcoq.Symbol.token (Pcoq.terminal "using"))))
                                                                ((Pcoq.Symbol.list1sep ((Pcoq.Symbol.nterm reference)) ((Pcoq.Symbol.rules 
                                                                [Pcoq.Rules.make 
                                                                (Pcoq.Rule.next_norec 
                                                                (Pcoq.Rule.stop)
                                                                ((Pcoq.Symbol.token (Pcoq.terminal ","))))
                                                                (fun _ loc ->
                                                                ())])) false)))
                                                (fun l _ loc -> 
# 118 "plugins/firstorder/g_ground.mlg"
                                                l 
                                                                ))]);
                                               Tacentries.arg_tag = Some
                                                                    (Geninterp.Val.List 
                                                                    (Geninterp.val_tag (Genarg.topwit wit_reference)));
                                               Tacentries.arg_intern = 
                                               Tacentries.ArgInternWit (Genarg.ListArg 
                                               (wit_reference));
                                               Tacentries.arg_subst = 
                                               Tacentries.ArgSubstWit (Genarg.ListArg 
                                               (wit_reference));
                                               Tacentries.arg_interp = 
                                               Tacentries.ArgInterpWit (Genarg.ListArg 
                                               (wit_reference));
                                               Tacentries.arg_printer = 
                                               ((fun env sigma -> 
# 116 "plugins/firstorder/g_ground.mlg"
                   pr_firstorder_using_raw 
                                               ), (fun env sigma -> 
# 117 "plugins/firstorder/g_ground.mlg"
                    pr_firstorder_using_glob 
                                               ), (fun env sigma -> 
# 115 "plugins/firstorder/g_ground.mlg"
               pr_firstorder_using_typed 
                                               ));
                                               }
let _ = (wit_firstorder_using, firstorder_using)

let () = Tacentries.tactic_extend "coq-core.plugins.firstorder" "firstorder" ~level:0 
         [(Tacentries.TyML (Tacentries.TyIdent ("firstorder", Tacentries.TyArg (
                                                              Extend.TUopt (
                                                              Extend.TUentry (Genarg.get_arg_tag wit_tactic)), 
                                                              Tacentries.TyArg (
                                                              Extend.TUentry (Genarg.get_arg_tag wit_firstorder_using), 
                                                              Tacentries.TyNil))), 
           (fun t l ist -> 
# 124 "plugins/firstorder/g_ground.mlg"
        gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] 
           )));
         (Tacentries.TyML (Tacentries.TyIdent ("firstorder", Tacentries.TyArg (
                                                             Extend.TUopt (
                                                             Extend.TUentry (Genarg.get_arg_tag wit_tactic)), 
                                                             Tacentries.TyIdent ("with", 
                                                             Tacentries.TyArg (
                                                             Extend.TUlist1 (
                                                             Extend.TUentry (Genarg.get_arg_tag wit_preident)), 
                                                             Tacentries.TyNil)))), 
          (fun t l ist -> 
# 126 "plugins/firstorder/g_ground.mlg"
        gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l 
          )));
         (Tacentries.TyML (Tacentries.TyIdent ("firstorder", Tacentries.TyArg (
                                                             Extend.TUopt (
                                                             Extend.TUentry (Genarg.get_arg_tag wit_tactic)), 
                                                             Tacentries.TyArg (
                                                             Extend.TUentry (Genarg.get_arg_tag wit_firstorder_using), 
                                                             Tacentries.TyIdent ("with", 
                                                             Tacentries.TyArg (
                                                             Extend.TUlist1 (
                                                             Extend.TUentry (Genarg.get_arg_tag wit_preident)), 
                                                             Tacentries.TyNil))))), 
          (fun t l l' ist -> 
# 129 "plugins/firstorder/g_ground.mlg"
        gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' 
          )))]

let () = Tacentries.tactic_extend "coq-core.plugins.firstorder" "gintuition" ~level:0 
         [(Tacentries.TyML (Tacentries.TyIdent ("gintuition", Tacentries.TyArg (
                                                              Extend.TUopt (
                                                              Extend.TUentry (Genarg.get_arg_tag wit_tactic)), 
                                                              Tacentries.TyNil)), 
           (fun t ist -> 
# 134 "plugins/firstorder/g_ground.mlg"
       gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] 
           )))]
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