aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytecodes.ml20
-rw-r--r--kernel/cbytecodes.mli5
-rw-r--r--kernel/cbytegen.ml33
3 files changed, 37 insertions, 21 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index a705e3004..8d4de523a 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -142,11 +142,29 @@ type fv = fv_elem array
exception NotClosed
+module Fv_elem =
+struct
+type t = fv_elem
+
+let compare e1 e2 = match e1, e2 with
+| FVnamed id1, FVnamed id2 -> Id.compare id1 id2
+| FVnamed _, _ -> -1
+| FVrel _, FVnamed _ -> 1
+| FVrel r1, FVrel r2 -> Int.compare r1 r2
+| FVrel _, FVuniv_var _ -> -1
+| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2
+| FVuniv_var i1, _ -> 1
+
+end
+
+module FvMap = Map.Make(Fv_elem)
+
(*spiwack: both type have been moved from Cbytegen because I needed then
for the retroknowledge *)
type vm_env = {
size : int; (* longueur de la liste [n] *)
- fv_rev : fv_elem list (* [fvn; ... ;fv1] *)
+ fv_rev : fv_elem list; (* [fvn; ... ;fv1] *)
+ fv_fwd : int FvMap.t; (* reverse mapping *)
}
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 6fa0841af..5f1f09d00 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -139,11 +139,14 @@ type fv = fv_elem array
closed terms. *)
exception NotClosed
+module FvMap : Map.S with type key = fv_elem
+
(*spiwack: both type have been moved from Cbytegen because I needed them
for the retroknowledge *)
type vm_env = {
size : int; (** length of the list [n] *)
- fv_rev : fv_elem list (** [fvn; ... ;fv1] *)
+ fv_rev : fv_elem list; (** [fvn; ... ;fv1] *)
+ fv_fwd : int FvMap.t; (** reverse mapping *)
}
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 2d1ae68f4..008955d80 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -93,7 +93,12 @@ open Pre_env
type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t
-let empty_fv = { size= 0; fv_rev = [] }
+let empty_fv = { size= 0; fv_rev = []; fv_fwd = FvMap.empty }
+let push_fv d e = {
+ size = e.size + 1;
+ fv_rev = d :: e.fv_rev;
+ fv_fwd = FvMap.add d e.size e.fv_fwd;
+}
let fv r = !(r.in_env)
@@ -184,20 +189,15 @@ let push_local sz r =
in_stack = (sz + 1) :: r.in_stack }
(*i Compilation of variables *)
-let find_at f l =
- let rec aux n = function
- | [] -> raise Not_found
- | hd :: tl -> if f hd then n else aux (n + 1) tl
- in aux 1 l
+let find_at fv env = FvMap.find fv env.fv_fwd
let pos_named id r =
let env = !(r.in_env) in
let cid = FVnamed id in
- let f = function FVnamed id' -> Id.equal id id' | _ -> false in
- try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
+ try Kenvacc(r.offset + find_at cid env)
with Not_found ->
let pos = env.size in
- r.in_env := { size = pos+1; fv_rev = cid:: env.fv_rev};
+ r.in_env := push_fv cid env;
Kenvacc (r.offset + pos)
let pos_rel i r sz =
@@ -212,11 +212,10 @@ let pos_rel i r sz =
let i = i - r.nb_rec in
let db = FVrel(i) in
let env = !(r.in_env) in
- let f = function FVrel j -> Int.equal i j | _ -> false in
- try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
+ try Kenvacc(r.offset + find_at db env)
with Not_found ->
let pos = env.size in
- r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev};
+ r.in_env := push_fv db env;
Kenvacc(r.offset + pos)
let pos_universe_var i r sz =
@@ -224,15 +223,11 @@ let pos_universe_var i r sz =
Kacc (sz - r.nb_stack - (r.nb_uni_stack - i))
else
let env = !(r.in_env) in
- let f = function
- | FVuniv_var u -> Int.equal i u
- | _ -> false
- in
- try Kenvacc (r.offset + env.size - (find_at f env.fv_rev))
+ let db = FVuniv_var i in
+ try Kenvacc (r.offset + find_at db env)
with Not_found ->
let pos = env.size in
- let db = FVuniv_var i in
- r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ;
+ r.in_env := push_fv db env;
Kenvacc(r.offset + pos)
(*i Examination of the continuation *)