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
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <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) *)
(************************************************************************)
open Pp
open Util
module ArgT =
struct
module DYN = Dyn.Make ()
module Map = DYN.Map
type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag
type any = Any : ('a, 'b, 'c) tag -> any
let eq = DYN.eq
let repr = DYN.repr
let create = DYN.create
let name s = match DYN.name s with
| None -> None
| Some (DYN.Any t) ->
Some (Any (Obj.magic t)) (** All created tags are made of triples *)
end
type (_, _, _) genarg_type =
| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type ->
('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
let rec genarg_type_eq : type a1 a2 b1 b2 c1 c2.
(a1, b1, c1) genarg_type -> (a2, b2, c2) genarg_type ->
(a1 * b1 * c1, a2 * b2 * c2) CSig.eq option =
fun t1 t2 -> match t1, t2 with
| ExtraArg t1, ExtraArg t2 -> ArgT.eq t1 t2
| ListArg t1, ListArg t2 ->
begin match genarg_type_eq t1 t2 with
| None -> None
| Some Refl -> Some Refl
end
| OptArg t1, OptArg t2 ->
begin match genarg_type_eq t1 t2 with
| None -> None
| Some Refl -> Some Refl
end
| PairArg (t1, u1), PairArg (t2, u2) ->
begin match genarg_type_eq t1 t2 with
| None -> None
| Some Refl ->
match genarg_type_eq u1 u2 with
| None -> None
| Some Refl -> Some Refl
end
| _ -> None
let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> Pp.t = function
| ListArg t -> pr_genarg_type t ++ spc () ++ str "list"
| OptArg t -> pr_genarg_type t ++ spc () ++ str "opt"
| PairArg (t1, t2) ->
str "("++ pr_genarg_type t1 ++ spc () ++
str "*" ++ spc () ++ pr_genarg_type t2 ++ str ")"
| ExtraArg s -> str (ArgT.repr s)
let argument_type_eq arg1 arg2 = match arg1, arg2 with
| ArgumentType t1, ArgumentType t2 ->
match genarg_type_eq t1 t2 with
| None -> false
| Some Refl -> true
let pr_argument_type (ArgumentType t) = pr_genarg_type t
type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
(** Alias for concision *)
(* Dynamics but tagged by a type expression *)
type rlevel = [ `rlevel ]
type glevel = [ `glevel ]
type tlevel = [ `tlevel ]
type (_, _) abstract_argument_type =
| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
type raw_generic_argument = rlevel generic_argument
type glob_generic_argument = glevel generic_argument
type typed_generic_argument = tlevel generic_argument
let rawwit t = Rawwit t
let glbwit t = Glbwit t
let topwit t = Topwit t
let wit_list t = ListArg t
let wit_opt t = OptArg t
let wit_pair t1 t2 = PairArg (t1, t2)
let in_gen t o = GenArg (t, o)
let abstract_argument_type_eq :
type a b l. (a, l) abstract_argument_type -> (b, l) abstract_argument_type -> (a, b) CSig.eq option =
fun t1 t2 -> match t1, t2 with
| Rawwit t1, Rawwit t2 ->
begin match genarg_type_eq t1 t2 with
| None -> None
| Some Refl -> Some Refl
end
| Glbwit t1, Glbwit t2 ->
begin match genarg_type_eq t1 t2 with
| None -> None
| Some Refl -> Some Refl
end
| Topwit t1, Topwit t2 ->
begin match genarg_type_eq t1 t2 with
| None -> None
| Some Refl -> Some Refl
end
let out_gen (type a) (type l) (t : (a, l) abstract_argument_type) (o : l generic_argument) : a =
let GenArg (t', v) = o in
match abstract_argument_type_eq t t' with
| None -> failwith "out_gen"
| Some Refl -> v
let has_type (GenArg (t, v)) u = match abstract_argument_type_eq t u with
| None -> false
| Some _ -> true
let unquote : type l. (_, l) abstract_argument_type -> _ = function
| Rawwit t -> ArgumentType t
| Glbwit t -> ArgumentType t
| Topwit t -> ArgumentType t
let genarg_tag (GenArg (t, _)) = unquote t
type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
(** Creating args *)
module type Param = sig type ('raw, 'glb, 'top) t end
module ArgMap(M : Param) =
struct
type _ pack = Pack : ('raw, 'glb, 'top) M.t -> ('raw * 'glb * 'top) pack
include ArgT.Map(struct type 'a t = 'a pack end)
end
let create_arg name =
match ArgT.name name with
| None -> ExtraArg (ArgT.create name)
| Some _ ->
CErrors.anomaly (str "generic argument already declared: " ++ str name ++ str ".")
let make0 = create_arg
(** Registering genarg-manipulating functions *)
module type GenObj =
sig
type ('raw, 'glb, 'top) obj
val name : string
val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option
end
let get_arg_tag = function
| ExtraArg s -> s
| _ -> assert false
module Register (M : GenObj) =
struct
module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end)
let arg0_map = ref GenMap.empty
let register0 arg f =
let s = get_arg_tag arg in
if GenMap.mem s !arg0_map then
let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in
CErrors.anomaly msg
else
arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
let get_obj0 name =
try
let GenMap.Pack obj = GenMap.find name !arg0_map in obj
with Not_found ->
match M.default (ExtraArg name) with
| None ->
CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name) ++ str ".")
| Some obj -> obj
(** For now, the following function is quite dummy and should only be applied
to an extra argument type, otherwise, it will badly fail. *)
let obj t = get_obj0 @@ get_arg_tag t
end