Skip to content

Commit 7deddf5

Browse files
SkySkimmerSkySkimmer
committed
Polymorphic maps
1 parent 99a61d6 commit 7deddf5

File tree

4 files changed

+175
-35
lines changed

4 files changed

+175
-35
lines changed

‎clib/polyMap.ml

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * Copyright INRIA, CNRS and contributors *)
4+
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
5+
(* \VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
module type ValueS =
12+
sig
13+
type 'a t
14+
end
15+
16+
module type Tag = sig type _ tag = .. end
17+
18+
module Make (Tag:Tag) = struct
19+
open Tag
20+
21+
module type OneTag = sig
22+
type a
23+
type _ tag += T : a tag
24+
end
25+
type 'a onetag = (module OneTag with type a = 'a)
26+
27+
let refl = Some CSig.Refl
28+
29+
let eq_onetag (type a b) (tag:a onetag) (tag':b tag) : (a,b) CSig.eq option =
30+
let module T = (val tag) in
31+
match tag' with
32+
| T.T -> refl
33+
| _ -> None
34+
35+
let make (type a) () : a onetag =
36+
(module struct type nonrec a = a type _ tag += T : a tag end)
37+
38+
let tag_of_onetag (type a) (tag:a onetag) : a tag =
39+
let module T = (val tag) in
40+
T.T
41+
42+
module type MapS = sig
43+
type t
44+
type _ value
45+
46+
val empty : t
47+
48+
val find : 'a tag -> t -> 'a value
49+
50+
val add : 'a onetag -> 'a value -> t -> t
51+
52+
val mem : 'a tag -> t -> bool
53+
54+
val modify : 'a tag -> ('a value -> 'a value) -> t -> t
55+
56+
end
57+
58+
module Map (V:ValueS) = struct
59+
60+
type key = Key : 'a tag -> key [@@unboxed]
61+
type v = V : 'a onetag * 'a V.t -> v
62+
63+
let onekey t = Key (tag_of_onetag t)
64+
65+
module Key = struct
66+
type t = key
67+
let compare : t -> t -> int = compare
68+
let hash : t -> int = Hashtbl.hash
69+
end
70+
module M = HMap.Make (Key)
71+
type t = v M.t
72+
73+
let empty = M.empty
74+
75+
let find (type a) (tag:a tag) m : a V.t =
76+
let V (tag', v) = M.find (Key tag) m in
77+
let module T = (val tag') in
78+
match tag with
79+
| T.T -> v
80+
| _ -> assert false
81+
82+
let add tag v m = M.add (onekey tag) (V (tag, v)) m
83+
84+
let mem tag m = M.mem (Key tag) m
85+
86+
let modify (type a) (tag:a tag) (f:a V.t -> a V.t) m =
87+
M.modify (Key tag) (fun _ (V (tag', v)) ->
88+
let module T = (val tag') in
89+
match tag with
90+
| T.T -> V (tag', f v)
91+
| _ -> assert false) m
92+
93+
end
94+
end

‎clib/polyMap.mli

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * Copyright INRIA, CNRS and contributors *)
4+
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
5+
(* \VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
module type ValueS =
12+
sig
13+
type 'a t
14+
end
15+
16+
(** Polymorphic maps over an extensible GADT tag type *)
17+
18+
module type Tag = sig type _ tag = .. end
19+
20+
module Make (Tag:Tag) : sig
21+
open Tag
22+
23+
module type OneTag = sig
24+
type a
25+
type _ tag += T : a tag
26+
end
27+
type 'a onetag = (module OneTag with type a = 'a)
28+
(** ['a onetag] can recognize ['b tag] values *)
29+
30+
val eq_onetag : 'a onetag -> 'b tag -> ('a,'b) CSig.eq option
31+
32+
val make : unit -> 'a onetag
33+
34+
val tag_of_onetag : 'a onetag -> 'a tag
35+
36+
module type MapS = sig
37+
type t
38+
type _ value
39+
40+
val empty : t
41+
42+
val find : 'a tag -> t -> 'a value
43+
44+
val add : 'a onetag -> 'a value -> t -> t
45+
46+
val mem : 'a tag -> t -> bool
47+
48+
val modify : 'a tag -> ('a value -> 'a value) -> t -> t
49+
50+
end
51+
module Map(V:ValueS) : MapS with type 'a value := 'a V.t
52+
53+
end

‎gramlib/grammar.ml

Lines changed: 15 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,6 @@ open Gramext
66
open Format
77
open Util
88

9-
module type DMapS = Dyn.MapS
10-
module Dyn = Dyn.Make()
11-
129
(* Functorial interface *)
1310

1411
type norec
@@ -161,7 +158,6 @@ module type ExtS = sig
161158
end
162159

163160
(* Implementation *)
164-
165161
module GMake (L : Plexing.S) : ExtS
166162
with type keyword_state := L.keyword_state
167163
and type te := L.te
@@ -184,10 +180,10 @@ type ('a, 'b, 'c, 'd) ty_and_rec3 =
184180
| NoRec3 : (norec, norec, norec, norec) ty_and_rec3
185181
| MayRec3 : ('a, 'b, 'c, mayrec) ty_and_rec3
186182

183+
type _ tag = ..
187184
type 'a ty_entry = {
188185
ename : string;
189-
euid : int; (* not sure if useful *)
190-
etag : 'a Dyn.tag;
186+
etag : 'a tag;
191187
}
192188

193189
and 'a ty_desc =
@@ -246,10 +242,11 @@ type ('t,'a) entry_data = {
246242
econtinue : 't -> int -> int -> 'a -> 'a parser_t;
247243
}
248244

249-
module rec EState : DMapS
250-
with type 'a key = 'a Dyn.tag
251-
and type 'a value = (GState.t, 'a) entry_data
252-
= Dyn.Map(struct type 'a t = (GState.t, 'a) entry_data end)
245+
module DMap = PolyMap.Make (struct type nonrec 'a tag = 'a tag = .. end)
246+
247+
module rec EState : DMap.MapS
248+
with type 'a value := (GState.t, 'a) entry_data
249+
= DMap.Map(struct type 'a t = (GState.t, 'a) entry_data end)
253250

254251
and GState : sig
255252
type t = {
@@ -1599,7 +1596,7 @@ let make_entry_data entry desc = {
15991596

16001597
let modify_entry estate e f = try EState.modify e.etag f estate with Not_found -> assert false
16011598

1602-
let add_entry estate e v = assert (not (EState.mem e.etag estate)); EState.add e.etag v estate
1599+
let add_entry otag estate e v = assert (not (EState.mem e.etag estate)); EState.add otag v estate
16031600

16041601
let extend_entry add_kw estate kwstate entry statement =
16051602
let kwstate = ref kwstate in
@@ -1685,12 +1682,13 @@ end
16851682
module Entry = struct
16861683
type 'a t = 'a ty_entry
16871684

1688-
let cnt = ref 0
1685+
let fresh n =
1686+
let otag = DMap.make () in
1687+
{ ename = n; etag = DMap.tag_of_onetag otag }, otag
16891688

16901689
let make n estate =
1691-
incr cnt;
1692-
let e = { ename = n; euid = !cnt; etag = Dyn.anonymous !cnt } in
1693-
let estate = add_entry estate e {
1690+
let e, otag = fresh n in
1691+
let estate = add_entry otag estate e {
16941692
edesc = Dlevels [];
16951693
estart = empty_entry n;
16961694
econtinue = (fun _ _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
@@ -1706,9 +1704,8 @@ module Entry = struct
17061704
let name e = e.ename
17071705
type 'a parser_fun = { parser_fun : L.keyword_state -> (L.keyword_state,te) LStream.t -> 'a }
17081706
let of_parser n { parser_fun = p } estate =
1709-
incr cnt;
1710-
let e = { ename = n; euid = !cnt; etag = Dyn.anonymous !cnt } in
1711-
let estate = add_entry estate e {
1707+
let e, otag = fresh n in
1708+
let estate = add_entry otag estate e {
17121709
estart = (fun gstate _ (strm:_ LStream.t) -> p gstate.kwstate strm);
17131710
econtinue = (fun _ _ _ _ (strm__ : _ LStream.t) -> raise Stream.Failure);
17141711
edesc = Dparser p;

‎lib/cWarnings.ml

Lines changed: 13 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -17,19 +17,19 @@ type t = {
1717
status : status;
1818
}
1919

20-
type w = ..
20+
type _ tag = ..
21+
22+
type w = W : 'a tag * 'a -> w
2123
exception WarnError of w
2224

23-
let printers = ref []
25+
module DMap = PolyMap.Make (struct type nonrec 'a tag = 'a tag = .. end)
26+
module PrintMap = DMap.Map(struct type 'a t = 'a -> Pp.t end)
2427

25-
let print w =
26-
let rec fold = function
27-
| [] -> CErrors.anomaly Pp.(str "Cannot print unknown warning")
28-
| pp :: rest -> match pp w with
29-
| Some pp -> pp
30-
| None -> fold rest
31-
in
32-
fold !printers
28+
let printers = ref PrintMap.empty
29+
30+
let print (W (tag, w)) =
31+
let pp = try PrintMap.find tag !printers with Not_found -> assert false in
32+
pp w
3333

3434
let () = CErrors.register_handler (function
3535
| WarnError w -> Some (print w)
@@ -178,12 +178,8 @@ let create (type a) ~name ~category ?(default=Enabled) (pp:a -> Pp.t) =
178178
pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
179179
str category ++ str "]"
180180
in
181-
let module M = struct type w += W of a end in
182-
let ppthis = function
183-
| M.W x -> Some (pp x)
184-
| _ -> None
185-
in
186-
printers := ppthis :: !printers;
181+
let tag = DMap.make () in
182+
printers := PrintMap.add tag pp !printers;
187183
Hashtbl.replace warnings name { default; category; status = default };
188184
add_warning_in_category ~name ~category;
189185
if default <> Disabled then
@@ -195,7 +191,7 @@ let create (type a) ~name ~category ?(default=Enabled) (pp:a -> Pp.t) =
195191
let w = Hashtbl.find warnings name in
196192
match w.status with
197193
| Disabled -> ()
198-
| AsError -> Loc.raise ?loc (WarnError (M.W x))
194+
| AsError -> Loc.raise ?loc (WarnError (W (DMap.tag_of_onetag tag, x)))
199195
| Enabled -> Feedback.msg_warning ?loc (pp x)
200196

201197
(* Remark: [warn] does not need to start with a comma, but if present

0 commit comments

Comments
 (0)