-
Notifications
You must be signed in to change notification settings - Fork 11
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #60 from CraigFe/type-attributes
Add support for extensible type attributes
- Loading branch information
Showing
19 changed files
with
312 additions
and
36 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,93 @@ | ||
include Attribute_intf | ||
open Higher | ||
|
||
module Key = struct | ||
type 'f t = { uid : int; name : string; wit : 'f Witness.t } | ||
|
||
let uid = | ||
let counter = ref (-1) in | ||
fun () -> | ||
incr counter; | ||
!counter | ||
|
||
let create ~name = | ||
let uid = uid () in | ||
let wit = Witness.make () in | ||
{ uid; name; wit } | ||
|
||
let name t = t.name | ||
|
||
type 'a ty = 'a t | ||
|
||
module Boxed = struct | ||
type t = E : _ ty -> t [@@ocaml.unboxed] | ||
|
||
let compare (E k1) (E k2) = Int.compare k1.uid k2.uid | ||
end | ||
end | ||
|
||
module Map = struct | ||
open Map.Make (Key.Boxed) | ||
|
||
type ('a, 'f) data = ('a, 'f) app | ||
type 'a binding = B : 'f Key.t * ('a, 'f) data -> 'a binding | ||
type nonrec 'a t = 'a binding t | ||
|
||
let empty = empty | ||
let is_empty = is_empty | ||
let mem t k = mem (E k) t | ||
let add t ~key ~data = add (E key) (B (key, data)) t | ||
|
||
let update : | ||
type a f. | ||
a t -> f Key.t -> ((a, f) data option -> (a, f) data option) -> a t = | ||
fun t k f -> | ||
update (E k) | ||
(fun b -> | ||
let v = | ||
f | ||
(match b with | ||
| None -> None | ||
| Some (B (k', v)) -> ( | ||
match Witness.eq k.wit k'.wit with | ||
| None -> None | ||
| Some Refl -> Some v)) | ||
in | ||
match v with None -> None | Some v -> Some (B (k, v))) | ||
t | ||
|
||
let singleton k v = singleton (E k) (B (k, v)) | ||
let iter t ~f = iter (fun _ b -> f b) t | ||
let for_all t ~f = for_all (fun _ b -> f b) t | ||
let exists t ~f = exists (fun _ b -> f b) t | ||
let cardinal t = cardinal t | ||
let bindings t = bindings t |> List.map snd | ||
|
||
let find : type a f. a t -> f Key.t -> (a, f) data option = | ||
fun t k -> | ||
match find_opt (E k) t with | ||
| None -> None | ||
| Some (B (k', v)) -> ( | ||
match Witness.eq k.wit k'.wit with None -> None | Some Refl -> Some v) | ||
end | ||
|
||
module Make1 (T : sig | ||
type 'a t | ||
|
||
val name : string | ||
end) = | ||
struct | ||
include T | ||
include Branded.Make (T) | ||
|
||
let key : br Key.t = Key.create ~name | ||
|
||
let find map = | ||
match Map.find map key with None -> None | Some x -> Some (prj x) | ||
|
||
let add data map = Map.add map ~key ~data:(inj data) | ||
end | ||
|
||
include Key | ||
|
||
module type S1 = S1 with type 'a attr := 'a t and type 'a map := 'a Map.t |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
include Attribute_intf.Attribute | ||
(** @inline *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,76 @@ | ||
open Higher | ||
|
||
(** An attribute key is a value that can be used to attach polymorphic data to a | ||
heterogeneous attribute map. *) | ||
module type S1 = sig | ||
type 'a attr | ||
type 'a map | ||
|
||
type 'a t | ||
(** The type of data associated with the {!attr} attribute key. *) | ||
|
||
val add : 'a t -> 'a map -> 'a map | ||
(** Attach data for {!attr} to a given map. *) | ||
|
||
val find : 'a map -> 'a t option | ||
(** Search for data corresponding to the key {!attr} in the given map. *) | ||
|
||
include Branded.S with type 'a t := 'a t | ||
|
||
val key : br attr | ||
end | ||
|
||
module type Attribute = sig | ||
type 'f t | ||
(** An ['f t] is an attribute key that can be used to pack polymorphic data | ||
into a heterogeneous {!Map} (and then recover it again). | ||
The type parameter ['f] is the brand of a type operator [f : * ⇒ *] | ||
which, when applied to the type parameter ['a] of a {!Map.t}, gives the | ||
type ['a f] of the associated data. This allows a single attribute key to | ||
store {i polymorphic} data. *) | ||
|
||
val create : name:string -> _ t | ||
(** [create ~name] is a fresh attribute key with the given string name. *) | ||
|
||
val name : _ t -> string | ||
(** Get the string name of an attribute key. *) | ||
|
||
module Map : sig | ||
type 'f key := 'f t | ||
|
||
type 'a t | ||
(** The type of polymorphic, heterogeneous maps. *) | ||
|
||
type ('a, 'f) data := ('a, 'f) app | ||
(** Given an ['a t] map and an ['f key] attribute key, the type of the | ||
corresponding data is [('a, 'f) Higher.app]. *) | ||
|
||
val empty : _ t | ||
val is_empty : _ t -> bool | ||
val mem : 'a t -> 'f key -> bool | ||
val add : 'a t -> key:'f key -> data:('a, 'f) data -> 'a t | ||
|
||
val update : | ||
'a t -> 'f key -> (('a, 'f) data option -> ('a, 'f) data option) -> 'a t | ||
|
||
val singleton : 'f key -> ('a, 'f) data -> 'a t | ||
|
||
type 'a binding = B : 'f key * ('a, 'f) data -> 'a binding | ||
|
||
val iter : 'a t -> f:('a binding -> unit) -> unit | ||
val for_all : 'a t -> f:('a binding -> bool) -> bool | ||
val exists : 'a t -> f:('a binding -> bool) -> bool | ||
val cardinal : 'a t -> int | ||
val find : 'a t -> 'f key -> ('a, 'f) data option | ||
val bindings : 'a t -> 'a binding list | ||
end | ||
|
||
module type S1 = S1 with type 'a attr := 'a t and type 'a map := 'a Map.t | ||
|
||
module Make1 (T : sig | ||
type 'a t | ||
|
||
val name : string | ||
end) : S1 with type 'a t = 'a T.t | ||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
(** Defunctionalised higher-kinded types. See "Lightweight Higher-Kinded | ||
Polymorphism" (Yallop and White, 2014) for more details. *) | ||
|
||
type ('a, 'f) app | ||
|
||
module Branded = struct | ||
module type S = sig | ||
type 'a t | ||
type br | ||
|
||
external inj : 'a t -> ('a, br) app = "%identity" | ||
external prj : ('a, br) app -> 'a t = "%identity" | ||
end | ||
|
||
module Make (T : sig | ||
type 'a t | ||
end) : S with type 'a t := 'a T.t = struct | ||
type 'a t = 'a T.t | ||
type br | ||
|
||
external inj : 'a t -> ('a, br) app = "%identity" | ||
external prj : ('a, br) app -> 'a t = "%identity" | ||
end | ||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.