package coq-core

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

Source file taccoerce.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
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
(************************************************************************)
(*         *   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 Util
open Names
open Constr
open EConstr
open Namegen
open Tactypes
open Genarg
open Stdarg
open Tacarg
open Geninterp
open Pp

exception CannotCoerceTo of string

let base_val_typ wit =
  match val_tag (topwit wit) with Val.Base t -> t | _ -> CErrors.anomaly (Pp.str "Not a base val.")

let (wit_constr_context : (Empty.t, Empty.t, Constr_matching.context) Genarg.genarg_type) =
  let wit = Genarg.create_arg "constr_context" in
  let () = register_val0 wit None in
  let pr env sigma lev c : Pp.t = Printer.pr_econstr_n_env env sigma lev (Constr_matching.repr_context c) in
  let () = Genprint.register_val_print0 (base_val_typ wit) (Pptactic.make_constr_printer pr) in
  wit

(* includes idents known to be bound and references *)
let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) =
  let wit = Genarg.create_arg "constr_under_binders" in
  let () = register_val0 wit None in
  let () = Genprint.register_val_print0 (base_val_typ wit)
             (fun c ->
               Genprint.TopPrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in
  wit

(** All the types considered here are base types *)
let val_tag wit = match val_tag wit with
| Val.Base t -> t
| _ -> assert false

let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
  let Val.Dyn (t, _) = v in
  match Val.eq t (val_tag wit) with
  | None -> false
  | Some Refl -> true

let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
  let Val.Dyn (t', x) = v in
  match Val.eq t t' with
  | None -> None
  | Some Refl -> Some x

let in_gen wit v = Val.Dyn (val_tag wit, v)
let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x

module Value =
struct

type t = Val.t

let of_constr c = in_gen (topwit wit_constr) c

let to_constr v =
  if has_type v (topwit wit_constr) then
    let c = out_gen (topwit wit_constr) v in
    Some c
  else if has_type v (topwit wit_constr_under_binders) then
    let vars, c = out_gen (topwit wit_constr_under_binders) v in
    match vars with [] -> Some c | _ -> None
  else None

let of_uconstr c = in_gen (topwit wit_uconstr) c

let to_uconstr v =
  if has_type v (topwit wit_uconstr) then
    Some (out_gen (topwit wit_uconstr) v)
  else None

let of_int i = in_gen (topwit wit_int) i

let to_int v =
  if has_type v (topwit wit_int) then
    Some (out_gen (topwit wit_int) v)
  else None

let of_ident id = in_gen (topwit wit_ident) id

let to_ident v =
  if has_type v (topwit wit_ident) then
    Some (out_gen (topwit wit_ident) v)
  else None

let to_list v = prj Val.typ_list v

let to_option v = prj Val.typ_opt v

let to_pair v = prj Val.typ_pair v

let cast_error wit v =
  let pr_v = Pptactic.pr_value Pptactic.ltop v in
  let Val.Dyn (tag, _) = v in
  let tag = Val.pr tag in
  CErrors.user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
    ++ str " while type " ++ Val.pr wit ++ str " was expected.")

let unbox wit v ans = match ans with
| None -> cast_error wit v
| Some x -> x

let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with
| Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v))
| Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v))
| Val.Pair (tag1, tag2) ->
  let (x, y) = unbox Val.typ_pair v (to_pair v) in
  (prj tag1 x, prj tag2 y)
| Val.Base t ->
  let Val.Dyn (t', x) = v in
  match Val.eq t t' with
  | None -> cast_error t v
  | Some Refl -> x
let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with
| ExtraArg _ -> Geninterp.val_tag (topwit wit)
| ListArg t -> Val.List (tag_of_arg t)
| OptArg t -> Val.Opt (tag_of_arg t)
| PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)

let val_cast arg v = prj (tag_of_arg arg) v

let cast (Topwit wit) v = val_cast wit v

end

let is_variable env id =
  Id.List.mem id (Termops.ids_of_named_context (Environ.named_context env))

(* Transforms an id into a constr if possible, or fails with Not_found *)
let constr_of_id env id =
  EConstr.mkVar (let _ = Environ.lookup_named id env in id)

(* Gives the constr corresponding to a Constr_context tactic_arg *)
let coerce_to_constr_context v =
  if has_type v (topwit wit_constr_context) then
    out_gen (topwit wit_constr_context) v
  else raise (CannotCoerceTo "a term context")

let is_intro_pattern v =
  if has_type v (topwit wit_intro_pattern) then
    Some (out_gen (topwit wit_intro_pattern) v).CAst.v
  else
    None

(* Interprets an identifier which must be fresh *)
let coerce_var_to_ident fresh env sigma v =
  let fail () = raise (CannotCoerceTo "a fresh identifier") in
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) -> id
  | Some _ -> fail ()
  | None ->
  if has_type v (topwit wit_intro_pattern) then
    match out_gen (topwit wit_intro_pattern) v with
    | { CAst.v=IntroNaming (IntroIdentifier id)} -> id
    | _ -> fail ()
  else if has_type v (topwit wit_hyp) then
    out_gen (topwit wit_hyp) v
  else match Value.to_constr v with
  | None -> fail ()
  | Some c ->
    (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
    if isVar sigma c && not (fresh && is_variable env (destVar sigma c)) then
      destVar sigma c
    else fail ()


(* Interprets, if possible, a constr to an identifier which may not
   be fresh but suitable to be given to the fresh tactic. Works for
   vars, constants, inductive, constructors and sorts. *)
let coerce_to_ident_not_fresh sigma v =
let id_of_name = function
  | Name.Anonymous -> Id.of_string "x"
  | Name.Name x -> x in
  let fail () = raise (CannotCoerceTo "an identifier") in
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) -> id
  | Some _ -> fail ()
  | None ->
  if has_type v (topwit wit_hyp) then
    out_gen (topwit wit_hyp) v
  else
    match Value.to_constr v with
    | None -> fail ()
    | Some c ->
       match EConstr.kind sigma c with
       | Var id -> id
       | Meta m -> id_of_name (Evd.meta_name sigma m)
       | Evar (kn,_) ->
        begin match Evd.evar_ident kn sigma with
        | None -> fail ()
        | Some id -> id
        end
       | Const (cst,_) -> Label.to_id (Constant.label cst)
       | Construct (cstr,_) ->
          let ref = GlobRef.ConstructRef cstr in
          let basename = Nametab.basename_of_global ref in
          basename
       | Ind (ind,_) ->
          let ref = GlobRef.IndRef ind in
          let basename = Nametab.basename_of_global ref in
          basename
       | Sort s ->
          begin
            match ESorts.kind sigma s with
            | Sorts.SProp -> Label.to_id (Label.make "SProp")
            | Sorts.Prop -> Label.to_id (Label.make "Prop")
            | Sorts.Set -> Label.to_id (Label.make "Set")
            | Sorts.Type _ -> Label.to_id (Label.make "Type")
          end
       | _ -> fail()


let coerce_to_intro_pattern sigma v =
  match is_intro_pattern v with
  | Some pat -> pat
  | None ->
  if has_type v (topwit wit_hyp) then
    let id = out_gen (topwit wit_hyp) v in
    IntroNaming (IntroIdentifier id)
  else match Value.to_constr v with
  | Some c when isVar sigma c ->
      (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
      (* but also in "destruct H as (H,H')" *)
      IntroNaming (IntroIdentifier (destVar sigma c))
  | _ -> raise (CannotCoerceTo "an introduction pattern")

let coerce_to_intro_pattern_naming sigma v =
  match coerce_to_intro_pattern sigma v with
  | IntroNaming pat -> pat
  | _ -> raise (CannotCoerceTo "a naming introduction pattern")

let coerce_to_hint_base v =
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) -> Id.to_string id
  | Some _ | None -> raise (CannotCoerceTo "a hint base name")

let coerce_to_int v =
  if has_type v (topwit wit_int) then
    out_gen (topwit wit_int) v
  else raise (CannotCoerceTo "an integer")

let coerce_to_constr env v =
  let fail () = raise (CannotCoerceTo "a term") in
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) ->
      (try ([], constr_of_id env id) with Not_found -> fail ())
  | Some _ -> fail ()
  | None ->
  if has_type v (topwit wit_constr) then
    let c = out_gen (topwit wit_constr) v in
    ([], c)
  else if has_type v (topwit wit_constr_under_binders) then
    out_gen (topwit wit_constr_under_binders) v
  else if has_type v (topwit wit_hyp) then
    let id = out_gen (topwit wit_hyp) v in
    (try [], constr_of_id env id with Not_found -> fail ())
  else fail ()

let coerce_to_uconstr v =
  if has_type v (topwit wit_uconstr) then
    out_gen (topwit wit_uconstr) v
  else
    raise (CannotCoerceTo "an untyped term")

let coerce_to_closed_constr env v =
  let ids,c = coerce_to_constr env v in
  let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
  c

let coerce_to_evaluable_ref env sigma v =
  let open Tacred in
  let fail () = raise (CannotCoerceTo "an evaluable reference") in
  let ev =
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id
  | Some _ -> fail ()
  | None ->
  if has_type v (topwit wit_hyp) then
    let id = out_gen (topwit wit_hyp) v in
    if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
    else fail ()
  else if has_type v (topwit wit_ref) then
    let open GlobRef in
    let r = out_gen (topwit wit_ref) v in
    match r with
    | VarRef var -> EvalVarRef var
    | ConstRef c -> EvalConstRef c
    | IndRef _ | ConstructRef _ -> fail ()
  else if has_type v (topwit wit_smart_global) then
    let open GlobRef in
    let r = out_gen (topwit wit_smart_global) v in
    match r with
    | VarRef var -> EvalVarRef var
    | ConstRef c -> EvalConstRef c
    | IndRef _ | ConstructRef _ -> fail ()
  else
    match Value.to_constr v with
    | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c))
    | Some c when isVar sigma c -> EvalVarRef (destVar sigma c)
    | _ -> fail ()
  in if Tacred.is_evaluable env ev then ev else fail ()

let coerce_to_constr_list env v =
  let v = Value.to_list v in
  match v with
  | Some l ->
    let map v = coerce_to_closed_constr env v in
    List.map map l
  | None -> raise (CannotCoerceTo "a term list")

let coerce_to_intro_pattern_list ?loc sigma v =
  match Value.to_list v with
  | None -> raise (CannotCoerceTo "an intro pattern list")
  | Some l ->
    let map v = CAst.make ?loc @@ coerce_to_intro_pattern sigma v in
    List.map map l

let coerce_to_hyp env sigma v =
  let fail () = raise (CannotCoerceTo "a variable") in
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id
  | Some _ -> fail ()
  | None ->
  if has_type v (topwit wit_hyp) then
    let id = out_gen (topwit wit_hyp) v in
    if is_variable env id then id else fail ()
  else match Value.to_constr v with
  | Some c when isVar sigma c -> destVar sigma c
  | _ -> fail ()

let coerce_to_hyp_list env sigma v =
  let v = Value.to_list v in
  match v with
  | Some l ->
    let map n = coerce_to_hyp env sigma n in
    List.map map l
  | None -> raise (CannotCoerceTo "a variable list")

(* Interprets a qualified name *)
let coerce_to_reference sigma v =
  match Value.to_constr v with
  | Some c ->
    begin
      try fst (EConstr.destRef sigma c)
      with DestKO -> raise (CannotCoerceTo "a reference")
    end
  | None -> raise (CannotCoerceTo "a reference")

(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
let coerce_to_quantified_hypothesis sigma v =
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) -> NamedHyp (CAst.make id)
  | Some _ -> raise (CannotCoerceTo "a quantified hypothesis")
  | None ->
  if has_type v (topwit wit_hyp) then
    let id = out_gen (topwit wit_hyp) v in
    NamedHyp (CAst.make id)
  else if has_type v (topwit wit_int) then
    AnonHyp (out_gen (topwit wit_int) v)
  else match Value.to_constr v with
  | Some c when isVar sigma c -> NamedHyp (CAst.make @@ destVar sigma c)
  | _ -> raise (CannotCoerceTo "a quantified hypothesis")

(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
let coerce_to_decl_or_quant_hyp sigma v =
  if has_type v (topwit wit_int) then
    AnonHyp (out_gen (topwit wit_int) v)
  else
    try coerce_to_quantified_hypothesis sigma v
    with CannotCoerceTo _ ->
      raise (CannotCoerceTo "a declared or quantified hypothesis")

let coerce_to_int_or_var_list v =
  match Value.to_list v with
  | None -> raise (CannotCoerceTo "an int list")
  | Some l ->
    let map n = Locus.ArgArg (coerce_to_int n) in
    List.map map l

(** Abstract application, to print ltac functions *)
type appl =
  | UnnamedAppl (** For generic applications: nothing is printed *)
  | GlbAppl of (Names.KerName.t * Val.t list) list
       (** For calls to global constants, some may alias other. *)

(* Values for interpretation *)
type tacvalue =
  | VFun of
      appl *
      Tacexpr.ltac_trace *
      Loc.t option * (* when executing a global Ltac function: the location where this function was called *)
      Val.t Id.Map.t * (* closure *)
      Name.t list * (* binders *)
      Tacexpr.glob_tactic_expr (* body *)
  | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr

let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
  let wit = Genarg.create_arg "tacvalue" in
  let () = register_val0 wit None in
  let () = Genprint.register_val_print0 (base_val_typ wit)
             (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in
  wit

let pr_argument_type arg =
  let Val.Dyn (tag, _) = arg in
  Val.pr tag

(** TODO: unify printing of generic Ltac values in case of coercion failure. *)

(* Displays a value *)
let pr_value env v =
  let pr_with_env pr =
    match env with
    | Some (env,sigma) -> pr env sigma
    | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
  let open Genprint in
  match generic_val_print v with
  | TopPrinterBasic pr -> pr ()
  | TopPrinterNeedsContext pr -> pr_with_env pr
  | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
     pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)

exception CoercionError of Id.t * (Environ.env * Evd.evar_map) option * Val.t * string

let () = CErrors.register_handler begin function
| CoercionError (id, env, v, s) ->
  Some (str "Ltac variable " ++ Id.print id ++
   strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
   strbrk "which cannot be coerced to " ++ str s ++ str".")
| _ -> None
end

let error_ltac_variable ?loc id env v s =
  Loc.raise ?loc (CoercionError (id, env, v, s))