package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file polyMap.ml

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct