dtlc

dependently-typed lambda calculus toy
git clone git://git.rr3.xyz/dtlc
Log | Files | Refs | README | LICENSE

uniq.ml (2220B)


      1 (* A uniq is a globally-fresh identifier. We mainly use these for variables in
      2  * the semantic domain, but they can be used any time we need a unique
      3  * identifier. *)
      4 
      5 (* TODO: Separate uniq and range? Having them in the same module is not really
      6  * consistent with what we do elsewhere. *)
      7 
      8 open Util
      9 
     10 type uniq = Uniq of int
     11 type range = Range of int * int
     12 
     13 exception Exhaustion
     14 
     15 let fresh
     16 : int -> range
     17 =
     18 	let next = ref 0 in
     19 	fun n ->
     20 		if !next > max_int - n then
     21 			raise Exhaustion (* This should never happen in practice. *)
     22 		else
     23 			let r = Range (!next, n) in
     24 			next := !next + n;
     25 			r
     26 
     27 let length
     28 : range -> int
     29 = fun (Range (_, l)) -> l
     30 
     31 let get
     32 : range -> int -> uniq
     33 = fun (Range (b, l)) i ->
     34 	if i < 0 || i >= l then
     35 		invalid_arg "Uniq.get"
     36 	else
     37 		Uniq (b + i)
     38 
     39 module UniqMap = Map.Make(struct
     40 	type t = uniq
     41 	let compare (Uniq x) (Uniq y) = Int.compare x y
     42 end)
     43 
     44 (* A RangeMap is a map which is extended with (range, value) pairs, but which
     45  * is queried at a single uniq x by "offsetting" the value stored at the range
     46  * (b, _) containing x (there can be at most one such range by uniqueness!)
     47  * by x - b. *)
     48 module RangeMap = struct
     49 	module type Value = sig
     50 		type v
     51 		type v'
     52 		val offset: v -> int -> v'
     53 	end
     54 
     55 	module Make (V: Value) = struct
     56 		module K = struct 
     57 			type t =
     58 			| Key of int * int
     59 			| Query of int
     60 
     61 			let compare k0 k1 = match k0, k1 with
     62 			| Key (b0, _), Key (b1, _) -> Int.compare b0 b1
     63 			| Key (b, l), Query x ->
     64 				if x < b      then +1 else
     65 				if x >= b + l then -1 else 0
     66 			| Query x, Key (b, l) ->
     67 				if x < b      then -1 else
     68 				if x >= b + l then +1 else 0
     69 			| Query _, Query _ -> impossible "Uniq.RangeMap.Make.K.compare"
     70 		end
     71 
     72 		(* TODO: Using a Map here is a hack, and it leads to wasted space both
     73 		 * in keys and in values. Ideally, we should use a completely custom
     74 		 * data structure. *)
     75 		module M = Map.Make(K)
     76 
     77 		type t = (V.v * int) M.t
     78 
     79 		let empty: t = M.empty
     80 
     81 		let add
     82 		: range -> V.v -> t -> t
     83 		= fun (Range (b, l)) v m -> M.add (K.Key (b, l)) (v, b) m
     84 
     85 		let find_opt
     86 		: uniq -> t -> V.v' option
     87 		= fun (Uniq x) m ->
     88 			match M.find_opt (K.Query x) m with
     89 			| Some (v, b) -> Some (V.offset v (x - b))
     90 			| None -> None
     91 	end
     92 end