diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytecodes.ml | 20 | ||||
| -rw-r--r-- | kernel/cbytecodes.mli | 5 | ||||
| -rw-r--r-- | kernel/cbytegen.ml | 33 |
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 *) |