diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-20 01:11:55 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-22 13:49:14 +0200 |
commit | 5ede69c8e67e6de34af2850695ae7ee24f8588ea (patch) | |
tree | abf323d73101b2d2d6910bc580e5dd9a4f7f80fc /kernel/cbytecodes.ml | |
parent | 687d510cb43db5029fb4545c3b12ac20cf99197a (diff) |
Use a better data structure for VM compilation of free vars.
This fixes #3450 and probably provides a huge speed-up to many instances.
Diffstat (limited to 'kernel/cbytecodes.ml')
-rw-r--r-- | kernel/cbytecodes.ml | 20 |
1 files changed, 19 insertions, 1 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 *) } |