Source file number.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
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
open Pp
open Util
open Names
open Libnames
open Constrexpr
open Constrexpr_ops
open Notation
module CSet = CSet.Make (Constr)
module CMap = CMap.Make (Constr)
(** * Number notation *)
type number_string_via = qualid * (bool * qualid * qualid) list
type number_option =
| After of numnot_option
| Via of number_string_via
let warn_abstract_large_num_no_op =
CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
(fun f ->
strbrk "The 'abstract after' directive has no effect when " ++
strbrk "the parsing function (" ++
Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
strbrk "option type.")
let get_constructors ind =
let mib,oib = Global.lookup_inductive ind in
let mc = oib.Declarations.mind_consnames in
Array.to_list
(Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc)
let qualid_of_ref n =
n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
let q_option () = qualid_of_ref "core.option.type"
let unsafe_locate_ind q =
match Nametab.locate q with
| GlobRef.IndRef i -> i
| _ -> raise Not_found
let locate_z () =
let zn = "num.Z.type" in
let pn = "num.pos.type" in
if Coqlib.has_ref zn && Coqlib.has_ref pn
then
let q_z = qualid_of_ref zn in
let q_pos = qualid_of_ref pn in
Some ({
z_ty = unsafe_locate_ind q_z;
pos_ty = unsafe_locate_ind q_pos;
}, mkRefC q_z)
else None
let locate_number () =
let dint = "num.int.type" in
let duint = "num.uint.type" in
let dec = "num.decimal.type" in
let hint = "num.hexadecimal_int.type" in
let huint = "num.hexadecimal_uint.type" in
let hex = "num.hexadecimal.type" in
let int = "num.num_int.type" in
let uint = "num.num_uint.type" in
let num = "num.number.type" in
if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec
&& Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex
&& Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num
then
let q_dint = qualid_of_ref dint in
let q_duint = qualid_of_ref duint in
let q_dec = qualid_of_ref dec in
let q_hint = qualid_of_ref hint in
let q_huint = qualid_of_ref huint in
let q_hex = qualid_of_ref hex in
let q_int = qualid_of_ref int in
let q_uint = qualid_of_ref uint in
let q_num = qualid_of_ref num in
let int_ty = {
dec_int = unsafe_locate_ind q_dint;
dec_uint = unsafe_locate_ind q_duint;
hex_int = unsafe_locate_ind q_hint;
hex_uint = unsafe_locate_ind q_huint;
int = unsafe_locate_ind q_int;
uint = unsafe_locate_ind q_uint;
} in
let num_ty = {
int = int_ty;
decimal = unsafe_locate_ind q_dec;
hexadecimal = unsafe_locate_ind q_hex;
number = unsafe_locate_ind q_num;
} in
Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint,
num_ty, mkRefC q_num, mkRefC q_dec)
else None
let locate_int63 () =
let int63n = "num.int63.type" in
let pos_neg_int63n = "num.int63.pos_neg_int63" in
if Coqlib.has_ref int63n && Coqlib.has_ref pos_neg_int63n
then
let q_pos_neg_int63 = qualid_of_ref pos_neg_int63n in
Some ({pos_neg_int63_ty = unsafe_locate_ind q_pos_neg_int63},
mkRefC q_pos_neg_int63)
else None
let has_type env sigma f ty =
let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
try let _ = Constrintern.interp_constr env sigma c in true
with Pretype_errors.PretypeError _ -> false
let type_error_to f ty =
CErrors.user_err
(pr_qualid f ++ str " should go from Number.int to " ++
pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
fnl () ++ str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).")
let type_error_of g ty =
CErrors.user_err
(pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
str " to Number.int or (option Number.int)." ++ fnl () ++
str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).")
let error_params ind =
CErrors.user_err
(str "Wrong number of parameters for inductive" ++ spc ()
++ Printer.pr_global (GlobRef.IndRef ind) ++ str ".")
let remapping_error ?loc ty ty' ty'' =
CErrors.user_err ?loc
(Printer.pr_global ty
++ str " was already mapped to" ++ spc () ++ Printer.pr_global ty'
++ str " and cannot be remapped to" ++ spc () ++ Printer.pr_global ty''
++ str ".")
let error_missing c =
CErrors.user_err
(str "Missing mapping for constructor " ++ Printer.pr_global c ++ str ".")
let pr_constr env sigma c =
let c = Constrextern.extern_constr env sigma (EConstr.of_constr c) in
Ppconstr.pr_constr_expr env sigma c
let warn_via_remapping =
CWarnings.create ~name:"via-type-remapping" ~category:"numbers"
(fun (env, sigma, ty, ty', ty'') ->
let constr = pr_constr env sigma in
constr ty ++ str " was already mapped to" ++ spc () ++ constr ty'
++ str ", mapping it also to" ++ spc () ++ constr ty''
++ str " might yield ill typed terms when using the notation.")
let warn_via_type_mismatch =
CWarnings.create ~name:"via-type-mismatch" ~category:"numbers"
(fun (env, sigma, g, g', exp, actual) ->
let constr = pr_constr env sigma in
str "Type of" ++ spc() ++ Printer.pr_global g
++ str " seems incompatible with the type of" ++ spc ()
++ Printer.pr_global g' ++ str "." ++ spc ()
++ str "Expected type is: " ++ constr exp ++ spc ()
++ str "instead of " ++ constr actual ++ str "." ++ spc ()
++ str "This might yield ill typed terms when using the notation.")
let multiple_via_error () =
CErrors.user_err (Pp.str "Multiple 'via' options.")
let multiple_after_error () =
CErrors.user_err (Pp.str "Multiple 'warning after' or 'abstract after' options.")
let via_abstract_error () =
CErrors.user_err (Pp.str "'via' and 'abstract' cannot be used together.")
let locate_global_sort_inductive_or_constant sigma qid =
let locate_sort qid =
match Nametab.locate_extended qid with
| Globnames.TrueGlobal _ -> raise Not_found
| Globnames.SynDef kn ->
match Syntax_def.search_syntactic_definition kn with
| [], Notation_term.NSort r ->
let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family r) in
sigma,Constr.mkSort c
| _ -> raise Not_found in
try locate_sort qid
with Not_found ->
match Smartlocate.global_with_alias qid with
| GlobRef.IndRef i -> sigma, Constr.mkInd i
| _ -> sigma, Constr.mkConst (Smartlocate.global_constant_with_alias qid)
let locate_global_constructor_inductive_or_constant qid =
let g = Smartlocate.global_with_alias qid in
match g with
| GlobRef.ConstructRef c -> g, Constr.mkConstruct c
| GlobRef.IndRef i -> g, Constr.mkInd i
| _ -> g, Constr.mkConst (Smartlocate.global_constant_with_alias qid)
let get_type env sigma c =
let rec aux env acc t =
let t = Reductionops.whd_all env sigma t in
match EConstr.kind sigma t with
| Constr.Prod (na, a, b) ->
let a = Reductionops.whd_all env sigma a in
let rel = Context.Rel.Declaration.LocalAssum (na, a) in
aux (EConstr.push_rel rel env) ((na, a) :: acc) b
| _ -> List.rev acc, t in
let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
let l, t = aux env [] t in
List.map (fun (na, a) -> na, EConstr.Unsafe.to_constr a) l,
EConstr.Unsafe.to_constr t
let elaborate_to_post_params env sigma ty_ind params =
let to_post_for_constructor indc =
let sigma, c = match indc with
| GlobRef.ConstructRef c ->
let sigma,c = Evd.fresh_constructor_instance env sigma c in
sigma, Constr.mkConstructU c
| _ -> assert false in
let args, t = get_type env sigma c in
let params_indc = match Constr.kind t with
| Constr.App (_, a) -> Array.to_list a | _ -> [] in
let sz = List.length args in
let a = Array.make sz ToPostCopy in
if List.length params <> List.length params_indc then error_params ty_ind;
List.iter2 (fun param param_indc ->
match param, Constr.kind param_indc with
| Some p, Constr.Rel i when i <= sz -> a.(sz - i) <- ToPostCheck p
| _ -> ())
params params_indc;
indc, indc, Array.to_list a in
let pt_refs = get_constructors ty_ind in
let to_post_0 = List.map to_post_for_constructor pt_refs in
let to_post =
let only_copy (_, _, args) = List.for_all ((=) ToPostCopy) args in
if (List.for_all only_copy to_post_0) then [||] else [|to_post_0|] in
to_post, pt_refs
let elaborate_to_post_via env sigma ty_name ty_ind l =
let sigma, ty_name =
locate_global_sort_inductive_or_constant sigma ty_name in
let ty_ind = Constr.mkInd ty_ind in
let l =
let read (consider_implicits, cnst, indc) =
let lcnst, lindc = cnst.CAst.loc, indc.CAst.loc in
let cnst, ccnst = locate_global_constructor_inductive_or_constant cnst in
let indc, cindc =
let indc = Smartlocate.global_constructor_with_alias indc in
GlobRef.ConstructRef indc, Constr.mkConstruct indc in
let get_type_wo_params c =
let rm_params c = match Constr.kind c with
| Constr.App (c, _) when Constr.isInd c -> c
| _ -> c in
let lc, tc = get_type env sigma c in
List.map (fun (n, c) -> n, rm_params c) lc, rm_params tc in
let tcnst, tindc = get_type_wo_params ccnst, get_type_wo_params cindc in
let impls =
if not consider_implicits then [] else
Impargs.(select_stronger_impargs (implicits_of_global cnst)) in
lcnst, cnst, tcnst, lindc, indc, tindc, impls in
List.map read l in
let eq_indc indc (_, _, _, _, indc', _, _) = GlobRef.equal indc indc' in
let inds =
List.fold_left (fun s (_, _, _, _, _, tindc, _) -> CSet.add (snd tindc) s)
(CSet.singleton ty_ind) l in
let constructors =
CSet.fold (fun ind m ->
let inductive, _ = Constr.destInd ind in
CMap.add ind (get_constructors inductive) m)
inds CMap.empty in
let _ =
List.fold_left (fun already_seen (_, cnst, _, loc, indc, _, _) ->
try
let cnst' = List.assoc_f GlobRef.equal indc already_seen in
remapping_error ?loc indc cnst' cnst
with Not_found -> (indc, cnst) :: already_seen)
[] l in
let () =
CMap.iter (fun _ ->
List.iter (fun cstr ->
if not (List.exists (eq_indc cstr) l) then error_missing cstr))
constructors in
let () =
let ind2ty, ty2ind =
let add loc ckey cval m =
match CMap.find_opt ckey m with
| None -> CMap.add ckey cval m
| Some old_cval ->
if not (Constr.equal old_cval cval) then
warn_via_remapping ?loc (env, sigma, ckey, old_cval, cval);
m in
List.fold_left
(fun (ind2ty, ty2ind) (lcnst, _, (_, tcnst), lindc, _, (_, tindc), _) ->
add lcnst tindc tcnst ind2ty, add lindc tcnst tindc ty2ind)
CMap.(singleton ty_ind ty_name, singleton ty_name ty_ind) l in
let rm_impls impls (l, t) =
let rec aux impls l = match impls, l with
| Some _ :: impls, _ :: b -> aux impls b
| None :: impls, (n, a) :: b -> (n, a) :: aux impls b
| _ -> l in
aux impls l, t in
let replace m (l, t) =
let apply_m c = try CMap.find c m with Not_found -> c in
List.fold_right (fun (na, a) b -> Constr.mkProd (na, (apply_m a), b))
l (apply_m t) in
List.iter (fun (_, cnst, tcnst, loc, indc, tindc, impls) ->
let tcnst = rm_impls impls tcnst in
let tcnst' = replace CMap.empty tcnst in
if not (Constr.equal tcnst' (replace ind2ty tindc)) then
let actual = replace CMap.empty tindc in
let expected = replace ty2ind tcnst in
warn_via_type_mismatch ?loc (env, sigma, indc, cnst, expected, actual))
l in
let ind2num, num2ind, nb_ind =
CMap.fold (fun ind _ (ind2num, num2ind, i) ->
CMap.add ind i ind2num, Int.Map.add i ind num2ind, i + 1)
(CMap.remove ty_ind constructors)
(CMap.singleton ty_ind 0, Int.Map.singleton 0 ty_ind, 1) in
let to_post =
let rec map_prod impls tindc = match impls with
| Some _ :: impls -> ToPostHole :: map_prod impls tindc
| _ ->
match tindc with
| [] -> []
| (_, a) :: b ->
let t = match CMap.find_opt a ind2num with
| Some i -> ToPostAs i
| None -> ToPostCopy in
let impls = match impls with [] -> [] | _ :: t -> t in
t :: map_prod impls b in
Array.init nb_ind (fun i ->
List.map (fun indc ->
let _, cnst, _, _, _, tindc, impls = List.find (eq_indc indc) l in
indc, cnst, map_prod impls (fst tindc))
(CMap.find (Int.Map.find i num2ind) constructors)) in
let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in
to_post, pt_refs
type target_type =
| TargetInd of (inductive * GlobRef.t option list)
| TargetPrim of required_module
let locate_global_inductive_with_params allow_params qid =
if not allow_params then raise Not_found else
match Nametab.locate_extended qid with
| Globnames.TrueGlobal _ -> raise Not_found
| Globnames.SynDef kn ->
match Syntax_def.search_syntactic_definition kn with
| [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) ->
i,
List.map (function
| Notation_term.NRef (r,None) -> Some r
| Notation_term.NHole _ -> None
| _ -> raise Not_found) l
| _ -> raise Not_found
let locate_global_inductive allow_params qid =
try locate_global_inductive_with_params allow_params qid
with Not_found -> Smartlocate.global_inductive_with_alias qid, []
let locate_global_inductive_or_int63 allow_params qid =
try TargetInd (locate_global_inductive_with_params allow_params qid)
with Not_found ->
let int63n = "num.int63.type" in
if allow_params && Coqlib.has_ref int63n
&& GlobRef.equal (Smartlocate.global_with_alias qid) (Coqlib.lib_ref int63n)
then TargetPrim (Nametab.path_of_global (Coqlib.lib_ref int63n), [])
else TargetInd (Smartlocate.global_inductive_with_alias qid, [])
let vernac_number_notation local ty f g opts scope =
let rec parse_opts = function
| [] -> None, Nop
| h :: opts ->
let via, opts = parse_opts opts in
let via = match h, via with
| Via _, Some _ -> multiple_via_error ()
| Via v, None -> Some v
| _ -> via in
let opts = match h, opts with
| After _, (Warning _ | Abstract _) -> multiple_after_error ()
| After a, Nop -> a
| _ -> opts in
via, opts in
let via, opts = parse_opts opts in
(match via, opts with Some _, Abstract _ -> via_abstract_error () | _ -> ());
let env = Global.env () in
let sigma = Evd.from_env env in
let num_ty = locate_number () in
let z_pos_ty = locate_z () in
let int63_ty = locate_int63 () in
let ty_name = ty in
let ty, via =
match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in
let tyc_params = locate_global_inductive_or_int63 (via = None) ty in
let to_ty = Smartlocate.global_with_alias f in
let of_ty = Smartlocate.global_with_alias g in
let cty = mkRefC ty in
let app x y = mkAppC (x,[y]) in
let arrow x y =
mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
in
let opt r = app (mkRefC (q_option ())) r in
let to_kind =
match num_ty with
| Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
| Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
| Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct
| Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option
| Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct
| Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option
| _ ->
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct
| Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
| _ ->
match int63_ty with
| Some (pos_neg_int63_ty, cint63) when has_type env sigma f (arrow cint63 cty) -> Int63 pos_neg_int63_ty, Direct
| Some (pos_neg_int63_ty, cint63) when has_type env sigma f (arrow cint63 (opt cty)) -> Int63 pos_neg_int63_ty, Option
| _ -> type_error_to f ty
in
let cty = match tyc_params with
| TargetPrim _ -> mkRefC (qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int_wrapper")
| TargetInd _ -> cty in
let of_kind =
match num_ty with
| Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
| Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
| Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct
| Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option
| Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct
| Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option
| _ ->
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct
| Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
| _ ->
match int63_ty with
| Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty cint63) -> Int63 pos_neg_int63_ty, Direct
| Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty (opt cint63)) -> Int63 pos_neg_int63_ty, Option
| _ -> type_error_of g ty
in
let to_post, pt_required, pt_refs = match tyc_params with
| TargetPrim path -> [||], path, [Coqlib.lib_ref "num.int63.wrap_int"]
| TargetInd (tyc, params) ->
let to_post, pt_refs =
match via with
| None -> elaborate_to_post_params env sigma tyc params
| Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in
to_post, (Nametab.path_of_global (GlobRef.IndRef tyc), []), pt_refs in
let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name;
warning = opts }
in
(match opts, to_kind with
| Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty
| _ -> ());
let i =
{ pt_local = local;
pt_scope = scope;
pt_interp_info = NumberNotation o;
pt_required;
pt_refs;
pt_in_match = true }
in
enable_prim_token_interpretation i