aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-01-24 17:33:14 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-01-26 14:20:52 +0100
commit724c9c9f922e50afc24651e2e07390c3dd7babf6 (patch)
treed4ce6a7d63c18a137aec5dc2415ef1d5046a0b5a /pretyping/classops.ml
parent8c0f9b63cb923a6cb6682124cd48db5da391075c (diff)
Coercions: avoid imperative data structure
Diffstat (limited to 'pretyping/classops.ml')
-rw-r--r--pretyping/classops.ml16
1 files changed, 7 insertions, 9 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 956e777b2..fd5081fa3 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -68,6 +68,8 @@ end
module ClTypMap = Map.Make(ClTyp)
+module IntMap = Map.Make(Int)
+
let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
type cl_index = int
@@ -79,17 +81,13 @@ type inheritance_path = coe_index list
(* table des classes, des coercions et graphe d'heritage *)
module Bijint = struct
- type 'a t = { v : (cl_typ * 'a) array; s : int; inv : int ClTypMap.t }
- let empty = { v = [||]; s = 0; inv = ClTypMap.empty }
+ type 'a t = { v : (cl_typ * 'a) IntMap.t; s : int; inv : int ClTypMap.t }
+ let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty }
let mem y b = ClTypMap.mem y b.inv
- let map x b = if 0 <= x && x < b.s then b.v.(x) else raise Not_found
- let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (b.v.(n)))
+ let map x b = IntMap.find x b.v
+ let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (IntMap.find n b.v))
let add x y b =
- let v =
- if Int.equal b.s (Array.length b.v) then
- (let v = Array.make (b.s + 8) (x,y) in Array.blit b.v 0 v 0 b.s; v)
- else b.v in
- v.(b.s) <- (x,y); { v = v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
+ { v = IntMap.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
end