package coq-core

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

Source file internals.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
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Constr
open EConstr
open EConstr.Vars
open Names
open Tacexpr
open CErrors
open Util
open Termops
open Tactypes
open Tactics
open Proofview.Notations

let assert_succeeds tac =
  let open Proofview in
  let exception Succeeded in
  tclORELSE (tclONCE tac <*> tclZERO Succeeded) (function
      | Succeeded, _ -> tclUNIT ()
      | exn, info -> tclZERO ~info exn)

let mytclWithHoles tac with_evars c =
  Proofview.Goal.enter begin fun gl ->
    let env = Tacmach.pf_env gl in
    let sigma = Tacmach.project gl in
    let sigma',c = Tactics.force_destruction_arg with_evars env sigma c in
    Tacticals.tclWITHHOLES with_evars (tac with_evars (Some c)) sigma'
  end

(**********************************************************************)
(* replace, discriminate, injection, simplify_eq                      *)
(* dependent rewrite                                      *)

let with_delayed_uconstr ist c tac =
  let flags = Pretyping.{
    use_coercions = true;
    use_typeclasses = NoUseTC;
    solve_unification_constraints = true;
    fail_evar = false;
    expand_evars = true;
    program_mode = false;
    polymorphic = false;
    undeclared_evars_patvars = false;
    patvars_abstract = false;
    unconstrained_sorts = false;
 } in
  let c = Tacinterp.type_uconstr ~flags ist c in
  Tacticals.tclDELAYEDWITHHOLES false c tac

let replace_in_clause_maybe_by ist dir_opt c1 c2 cl tac =
  with_delayed_uconstr ist c1
  (fun c1 -> Equality.replace_in_clause_maybe_by dir_opt c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))

let replace_term ist dir_opt c cl =
  with_delayed_uconstr ist c (fun c -> Equality.replace_term dir_opt c cl)

let elimOnConstrWithHoles tac with_evars c =
  Tacticals.tclDELAYEDWITHHOLES with_evars c
    (fun c -> tac with_evars (Some (None,ElimOnConstr c)))

let discr_main c = elimOnConstrWithHoles Equality.discr_tac false c

let discrHyp id =
  Proofview.tclEVARMAP >>= fun sigma ->
  discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))

let injection_main with_evars c =
 elimOnConstrWithHoles (Equality.injClause None None) with_evars c

let injHyp id =
  Proofview.tclEVARMAP >>= fun sigma ->
  injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))

let constr_flags () = Pretyping.{
  use_coercions = true;
  use_typeclasses = UseTC;
  solve_unification_constraints = Proof.use_unification_heuristics ();
  fail_evar = false;
  expand_evars = true;
  program_mode = false;
  polymorphic = false;
  undeclared_evars_patvars = false;
  patvars_abstract = false;
  unconstrained_sorts = false;
}

let refine_tac ist ~simple ~with_classes c =
  let with_classes = if with_classes then Pretyping.UseTC else Pretyping.NoUseTC in
  Proofview.Goal.enter begin fun gl ->
    let concl = Proofview.Goal.concl gl in
    let env = Proofview.Goal.env gl in
    let flags =
      { (constr_flags ()) with Pretyping.use_typeclasses = with_classes } in
    let expected_type = Pretyping.OfType concl in
    let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
    let update = begin fun sigma ->
      c env sigma
    end in
    let refine = Refine.refine ~typecheck:false update in
    if simple then refine
    else refine <*>
           Tactics.reduce_after_refine <*>
           Proofview.shelve_unifiable
  end

(**********************************************************************)

(**********************************************************************)
(* A tactic that reduces one match t with ... by doing destruct t.    *)
(* if t is not a variable, the tactic does                            *)
(* case_eq t;intros ... heq;rewrite heq in *|-. (but heq itself is    *)
(* preserved).                                                        *)
(* Contributed by Julien Forest and Pierre Courtieu (july 2010)       *)
(**********************************************************************)

let induction_arg_of_quantified_hyp = function
  | AnonHyp n -> None,ElimOnAnonHyp n
  | NamedHyp id -> None,ElimOnIdent id

exception Found of unit Proofview.tactic

let rewrite_except h =
  Proofview.Goal.enter begin fun gl ->
  let hyps = Tacmach.pf_ids_of_hyps gl in
  Tacticals.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else
      Tacticals.tclTRY (Equality.general_rewrite ~where:(Some id) ~l2r:true Locus.AllOccurrences ~freeze:true ~dep:true ~with_evars:false (mkVar h, NoBindings)))
    hyps
  end


let refl_equal () = Coqlib.lib_ref "core.eq.type"

(* This is simply an implementation of the case_eq tactic.  this code
  should be replaced by a call to the tactic but I don't know how to
  call it before it is defined. *)
let  mkCaseEq a  : unit Proofview.tactic =
  Proofview.Goal.enter begin fun gl ->
    let type_of_a = Tacmach.pf_get_type_of gl a in
    Tacticals.pf_constr_of_global (delayed_force refl_equal) >>= fun req ->
    Tacticals.tclTHENLIST
         [Generalize.generalize [(mkApp(req, [| type_of_a; a|]))];
          Proofview.Goal.enter begin fun gl ->
            let concl = Proofview.Goal.concl gl in
            let env = Proofview.Goal.env gl in
            (* FIXME: this looks really wrong. Does anybody really use
               this tactic? *)
            let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in
            change_concl c
          end;
          simplest_case a]
  end


let case_eq_intros_rewrite x =
  Proofview.Goal.enter begin fun gl ->
  let n = nb_prod (Tacmach.project gl) (Proofview.Goal.concl gl) in
  (* Pp.msgnl (Printer.pr_lconstr x); *)
  Tacticals.tclTHENLIST [
      mkCaseEq x;
    Proofview.Goal.enter begin fun gl ->
      let concl = Proofview.Goal.concl gl in
      let hyps = Tacmach.pf_ids_set_of_hyps gl in
      let n' = nb_prod (Tacmach.project gl) concl in
      let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl)  in
      Tacticals.tclTHENLIST [
                    Tacticals.tclDO (n'-n-1) intro;
                    introduction h;
                    rewrite_except h]
    end
  ]
  end

let rec find_a_destructable_match sigma t =
  let cl = induction_arg_of_quantified_hyp (NamedHyp (CAst.make @@ Id.of_string "x")) in
  let cl = [cl, (None, None), None], None in
  let dest = CAst.make @@ TacAtom (TacInductionDestruct(false, false, cl)) in
  match EConstr.kind sigma t with
    | Case (_,_,_,_,_,x,_) when closed0 sigma x ->
        if isVar sigma x then
          (* TODO check there is no rel n. *)
          raise (Found (Tacinterp.eval_tactic dest))
        else
          (* let _ = Pp.msgnl (Printer.pr_lconstr x)  in *)
          raise (Found (case_eq_intros_rewrite x))
    | _ -> EConstr.iter sigma (fun c -> find_a_destructable_match sigma c) t


let destauto0 t =
  Proofview.tclEVARMAP >>= fun sigma ->
  try find_a_destructable_match sigma t;
    Tacticals.tclZEROMSG (Pp.str "No destructable match found")
  with Found tac -> tac

let destauto =
  Proofview.Goal.enter begin fun gl -> destauto0 (Proofview.Goal.concl gl) end

let destauto_in id =
  Proofview.Goal.enter begin fun gl ->
  let ctype = Tacmach.pf_get_type_of gl (mkVar id) in
(*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
(*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
  destauto0 ctype
  end

(** Term introspection *)

let is_evar x =
  Proofview.tclEVARMAP >>= fun sigma ->
  match EConstr.kind sigma x with
    | Evar _ -> Proofview.tclUNIT ()
    | _ -> Tacticals.tclFAIL (Pp.str "Not an evar")

let has_evar x =
  Proofview.tclEVARMAP >>= fun sigma ->
  if Evarutil.has_undefined_evars sigma x
  then Proofview.tclUNIT ()
  else Tacticals.tclFAIL (Pp.str "No evars")

let is_var x =
  Proofview.tclEVARMAP >>= fun sigma ->
  match EConstr.kind sigma x with
    | Var _ ->  Proofview.tclUNIT ()
    | _ -> Tacticals.tclFAIL (Pp.str "Not a variable or hypothesis")

let is_fix x =
  Proofview.tclEVARMAP >>= fun sigma ->
  match EConstr.kind sigma x with
    | Fix _ -> Proofview.tclUNIT ()
    | _ -> Tacticals.tclFAIL (Pp.str "not a fix definition")

let is_cofix x =
  Proofview.tclEVARMAP >>= fun sigma ->
  match EConstr.kind sigma x with
    | CoFix _ -> Proofview.tclUNIT ()
    | _ -> Tacticals.tclFAIL (Pp.str "not a cofix definition")

let is_ind x =
  Proofview.tclEVARMAP >>= fun sigma ->
  match EConstr.kind sigma x with
    | Ind _ -> Proofview.tclUNIT ()
    | _ -> Tacticals.tclFAIL (Pp.str "not an (co)inductive datatype")

let is_constructor x =
  Proofview.tclEVARMAP >>= fun sigma ->
  match EConstr.kind sigma x with
    | Construct _ -> Proofview.tclUNIT ()
    | _ -> Tacticals.tclFAIL (Pp.str "not a constructor")

let is_proj x =
  Proofview.tclEVARMAP >>= fun sigma ->
  match EConstr.kind sigma x with
    | Proj _ -> Proofview.tclUNIT ()
    | _ -> Tacticals.tclFAIL (Pp.str "not a primitive projection")

let is_const x =
  Proofview.tclEVARMAP >>= fun sigma ->
  match EConstr.kind sigma x with
    | Const _ -> Proofview.tclUNIT ()
    | _ -> Tacticals.tclFAIL (Pp.str "not a constant")

let unshelve ist t =
  Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) ->
  let gls = List.map Proofview.with_empty_state gls in
  Proofview.Unsafe.tclGETGOALS >>= fun ogls ->
  Proofview.Unsafe.tclSETGOALS (gls @ ogls)

(** tactic analogous to "OPTIMIZE HEAP" *)

let tclOPTIMIZE_HEAP =
  Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ()))

let onSomeWithHoles tac = function
  | None -> tac None
  | Some c -> Tacticals.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c))

let decompose l c =
  Proofview.Goal.enter begin fun gl ->
    let sigma = Tacmach.project gl in
    let to_ind c =
      if isInd sigma c then fst (destInd sigma c)
      else user_err Pp.(str "not an inductive type")
    in
    let l = List.map to_ind l in
    Elim.h_decompose l c
  end

let exact ist (c : Ltac_pretype.closed_glob_constr) =
  let open Tacmach in
  Proofview.Goal.enter begin fun gl ->
  let expected_type = Pretyping.OfType (pf_concl gl) in
  let sigma, c = Tacinterp.type_uconstr ~expected_type ist c (pf_env gl) (project gl) in
  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tactics.exact_no_check c)
  end

(** ProofGeneral specific command *)

(* Execute tac, show the names of new hypothesis names created by tac
   in the "as" format and then forget everything. From the logical
   point of view [infoH tac] is therefore equivalent to idtac,
   except that it takes the time and memory of tac and prints "as"
   information. The resulting (unchanged) goals are printed *after*
   the as-expression, which forces pg to some gymnastic.
   TODO: Have something similar (better?) in the xml protocol.
   NOTE: some tactics delete hypothesis and reuse names (induction,
   destruct), this is not detected by this tactical. *)
let infoH ~pstate (tac : raw_tactic_expr) : unit =
  let (_, oldhyps) = Declare.Proof.get_current_goal_context pstate in
  let oldhyps = List.map Context.Named.Declaration.get_id @@ Environ.named_context oldhyps in
  let tac = Tacinterp.interp tac in
  let tac =
    let open Proofview.Notations in
    tac <*>
    Proofview.Unsafe.tclGETGOALS >>= fun gls ->
    Proofview.tclEVARMAP >>= fun sigma ->
    let map gl =
      let gl = Proofview_monad.drop_state gl in
      let hyps = Evd.evar_filtered_context (Evd.find_undefined sigma gl) in
      List.map Context.Named.Declaration.get_id @@ hyps
    in
    let hyps = List.map map gls in
    let newhyps = List.map (fun hypl -> List.subtract Names.Id.equal hypl oldhyps) hyps in
    let s =
      let frst = ref true in
      List.fold_left
      (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
        ^ (List.fold_left
            (fun acc d -> (Names.Id.to_string d) ^ " " ^ acc)
            "" lh))
      "" newhyps in
    let () = Feedback.msg_notice
      Pp.(str "<infoH>"
        ++  (hov 0 (str s))
        ++  (str "</infoH>")) in
    Proofview.tclUNIT ()
  in
  ignore (Declare.Proof.by tac pstate)

let declare_equivalent_keys c c' =
  let get_key c =
    let env = Global.env () in
    let evd = Evd.from_env env in
    let (evd, c) = Constrintern.interp_open_constr env evd c in
    let kind c = EConstr.kind evd c in
    Keys.constr_key env kind c
  in
  let k1 = get_key c in
  let k2 = get_key c' in
    match k1, k2 with
    | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2
    | _ -> ()
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