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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
module type ValueS =
sig
type 'a t
end
module type Tag = sig type _ tag = .. end
module Make (Tag:Tag) = struct
open Tag
module type OneTag = sig
type a
type _ tag += T : a tag
end
type 'a onetag = (module OneTag with type a = 'a)
let refl = Some CSig.Refl
let eq_onetag (type a b) (tag:a onetag) (tag':b tag) : (a,b) CSig.eq option =
let module T = (val tag) in
match tag' with
| T.T -> refl
| _ -> None
let make (type a) () : a onetag =
(module struct type nonrec a = a type _ tag += T : a tag end)
let tag_of_onetag (type a) (tag:a onetag) : a tag =
let module T = (val tag) in
T.T
module type MapS = sig
type t
type _ value
val empty : t
val find : 'a tag -> t -> 'a value
val add : 'a onetag -> 'a value -> t -> t
val mem : 'a tag -> t -> bool
val modify : 'a tag -> ('a value -> 'a value) -> t -> t
end
module Map (V:ValueS) = struct
type v = V : 'a onetag * 'a V.t -> v
let key t = Obj.Extension_constructor.(id (of_val t))
let onekey t = key (tag_of_onetag t)
module M = Int.Map
type t = v M.t
let empty = M.empty
let find (type a) (tag:a tag) m : a V.t =
let V (tag', v) = M.find (key tag) m in
let module T = (val tag') in
match tag with
| T.T -> v
| _ -> assert false
let add tag v m = M.add (onekey tag) (V (tag, v)) m
let mem tag m = M.mem (key tag) m
let modify (type a) (tag:a tag) (f:a V.t -> a V.t) m =
M.modify (key tag) (fun _ (V (tag', v)) ->
let module T = (val tag') in
match tag with
| T.T -> V (tag', f v)
| _ -> assert false) m
end
end
|