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
|
(************************************************************************)
(* * 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 Pp
open Names
open Libnames
open Constrexpr
open Constrexpr_ops
open Notation
open Number
(** * String notation *)
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 q_list () = qualid_of_ref "core.list.type"
let q_byte () = qualid_of_ref "core.byte.type"
let has_type env sigma f ty =
let c = mkCastC (mkRefC f, Constr.DEFAULTcast, 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 Byte.byte or (list Byte.byte) to " ++
pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ").")
let type_error_of g ty =
CErrors.user_err
(pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).")
let vernac_string_notation local ty f g via scope =
let env = Global.env () in
let sigma = Evd.from_env env in
let app x y = mkAppC (x,[y]) in
let cref q = mkRefC q in
let cbyte = cref (q_byte ()) in
let clist = cref (q_list ()) in
let coption = cref (q_option ()) in
let opt r = app coption r in
let clist_byte = app clist cbyte 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 (via = None) ty in
let to_ty = Smartlocate.global_with_alias f in
let of_ty = Smartlocate.global_with_alias g in
let cty = cref ty in
let arrow x y =
mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
in
(* Check the type of f *)
let to_kind =
if has_type env sigma f (arrow clist_byte cty) then ListByte, Direct
else if has_type env sigma f (arrow clist_byte (opt cty)) then ListByte, Option
else if has_type env sigma f (arrow cbyte cty) then Byte, Direct
else if has_type env sigma f (arrow cbyte (opt cty)) then Byte, Option
else type_error_to f ty
in
(* Check the type of g *)
let of_kind =
if has_type env sigma g (arrow cty clist_byte) then ListByte, Direct
else if has_type env sigma g (arrow cty (opt clist_byte)) then ListByte, Option
else if has_type env sigma g (arrow cty cbyte) then Byte, Direct
else if has_type env sigma g (arrow cty (opt cbyte)) then Byte, Option
else type_error_of g ty
in
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
let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name;
warning = () }
in
let i =
{ pt_local = local;
pt_scope = scope;
pt_interp_info = StringNotation o;
pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
pt_refs;
pt_in_match = true }
in
enable_prim_token_interpretation i
|
