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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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) *)
(************************************************************************)
(* This file defines standard combinators to build ml expressions *)
type argument_type =
| ListArgType of argument_type
| OptArgType of argument_type
| PairArgType of argument_type * argument_type
| ExtraArgType of string
type user_symbol =
| Ulist1 of user_symbol
| Ulist1sep of user_symbol * string
| Ulist0 of user_symbol
| Ulist0sep of user_symbol * string
| Uopt of user_symbol
| Uentry of string
| Uentryl of string * int
type extend_token =
| ExtTerminal of string
| ExtNonTerminal of user_symbol * string option
let mlexpr_of_list f l =
List.fold_right
(fun e1 e2 ->
let e1 = f e1 in
let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
<:expr< [$e1$ :: $e2$] >>)
l (let loc = Ploc.dummy in <:expr< [] >>)
let mlexpr_of_pair m1 m2 (a1,a2) =
let e1 = m1 a1 and e2 = m2 a2 in
let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
<:expr< ($e1$, $e2$) >>
(* We don't give location for tactic quotation! *)
let loc = Ploc.dummy
let mlexpr_of_bool = function
| true -> <:expr< True >>
| false -> <:expr< False >>
let mlexpr_of_int n = <:expr< $int:string_of_int n$ >>
let mlexpr_of_string s = <:expr< $str:s$ >>
let mlexpr_of_option f = function
| None -> <:expr< None >>
| Some e -> <:expr< Some $f e$ >>
let mlexpr_of_name f = function
| None -> <:expr< Names.Name.Anonymous >>
| Some e -> <:expr< Names.Name.Name $f e$ >>
let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >>
let rec mlexpr_of_prod_entry_key f = function
| Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >>
| Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
| Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
| Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
| Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
| Uentry e -> <:expr< Extend.Aentry ($f e$) >>
| Uentryl (e, l) ->
(** Keep in sync with Pcoq! *)
assert (e = "tactic");
if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >>
else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >>
let rec type_of_user_symbol = function
| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) ->
ListArgType (type_of_user_symbol s)
| Uopt s ->
OptArgType (type_of_user_symbol s)
| Uentry e | Uentryl (e, _) -> ExtraArgType e
let coincide s pat off =
let len = String.length pat in
let break = ref true in
let i = ref 0 in
while !break && !i < len do
let c = Char.code s.[off + !i] in
let d = Char.code pat.[!i] in
break := c = d;
incr i
done;
!break
let check_separator sep =
if sep <> "" then failwith "Separator is only for arguments with suffix _list_sep."
let rec parse_user_entry s sep =
let l = String.length s in
if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
check_separator sep;
Ulist1 entry
else if l > 12 && coincide s "ne_" 0 &&
coincide s "_list_sep" (l-9) then
let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
Ulist1sep (entry, sep)
else if l > 5 && coincide s "_list" (l-5) then
let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
check_separator sep;
Ulist0 entry
else if l > 9 && coincide s "_list_sep" (l-9) then
let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
Ulist0sep (entry, sep)
else if l > 4 && coincide s "_opt" (l-4) then
let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
check_separator sep;
Uopt entry
else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
let n = Char.code s.[6] - 48 in
check_separator sep;
Uentryl ("tactic", n)
else
let s = match s with "hyp" -> "var" | _ -> s in
check_separator sep;
Uentry s
|
