diff options
| author | Pierre-Marie Pédrot | 2016-08-20 01:11:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-22 13:49:14 +0200 |
| commit | 5ede69c8e67e6de34af2850695ae7ee24f8588ea (patch) | |
| tree | abf323d73101b2d2d6910bc580e5dd9a4f7f80fc /kernel/cbytecodes.mli | |
| 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.mli')
| -rw-r--r-- | kernel/cbytecodes.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 6fa0841af9..5f1f09d00c 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 *) } |
