Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilation

3 files changed, 33 insertions, 54 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 0766f49b3..70dc6867a 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -500,22 +500,19 @@ let rec compile_lam env reloc lam sz cont =
   | Lsort (Sorts.Prop _ as s) ->
     compile_structured_constant reloc (Const_sort s) sz cont
   | Lsort (Sorts.Type u) ->
-    (* We separate global and local universes in [u]. The former will be part
-       of the structured constant, while the later (if any) will be applied as
-       arguments. *)
-    let open Univ in begin
-      let u,s = Universe.compact u in
-      (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
-      let compile_get_univ reloc idx sz cont =
-        set_max_stack_size sz;
-        compile_fv_elem reloc (FVuniv_var idx) sz cont
-      in
-      if List.is_empty s then
-        compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont
-      else
-        comp_app compile_structured_constant compile_get_univ reloc
+    (* We represent universes as a global constant with local universes
+       "compacted", i.e. as [u arg0 ... argn] where we will substitute (after
+       evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *)
+    let u,s = Univ.compact_univ u in
+    let compile_get_univ reloc idx sz cont =
+      set_max_stack_size sz;
+      compile_fv_elem reloc (FVuniv_var idx) sz cont
+    in
+    if List.is_empty s then
+      compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont
+    else
+      comp_app compile_structured_constant compile_get_univ reloc
         (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont
-    end
 
   | Llet (id,def,body) ->
       compile_lam env reloc def sz
diff --git a/kernel/univ.ml b/kernel/univ.ml
index be21381b7..ea3a52295 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -490,39 +490,6 @@ struct
     in 
       List.fold_right (fun a acc -> aux a acc) u []
 
-  (** [max_var_pred p u] returns the maximum variable level in [u] satisfying
-      [p], -1 if not found *)
-  let rec max_var_pred p u =
-    let open Level in
-    match u with
-    | [] -> -1
-    | (v, _) :: u ->
-      match var_index v with
-      | Some i when p i -> max i (max_var_pred p u)
-      | _ -> max_var_pred p u
-
-  let rec remap_var u i j =
-    let open Level in
-    match u with
-    | [] -> []
-    | (v, incr) :: u when var_index v = Some i ->
-      (Level.var j, incr) :: remap_var u i j
-    | _ :: u -> remap_var u i j
-
-  let rec compact u max_var i =
-    if i >= max_var then (u,[]) else
-    let j = max_var_pred (fun j -> j < i) u in
-    if Int.equal i (j+1) then
-      let (u,s) = compact u max_var (i+1) in
-      (u, i :: s)
-    else
-      let (u,s) = compact (remap_var u i j) max_var (i+1) in
-      (u, j+1 :: s)
-
-  let compact u =
-    let max_var = max_var_pred (fun _ -> true) u in
-    compact u max_var 0
-
   (* Returns the formal universe that is greater than the universes u and v.
      Used to type the products. *)
   let sup x y = merge_univs x y
@@ -1208,6 +1175,20 @@ let abstract_cumulativity_info (univs, variance) =
   let subst, univs = abstract_universes univs in
   subst, (univs, variance)
 
+let rec compact_univ s vars i u =
+  match u with
+  | [] -> (s, List.rev vars)
+  | (lvl, _) :: u ->
+    match Level.var_index lvl with
+    | Some k when not (LMap.mem lvl s) ->
+      let lvl' = Level.var i in
+      compact_univ (LMap.add lvl lvl' s) (k :: vars) (i+1) u
+    | _ -> compact_univ s vars i u
+
+let compact_univ u =
+  let (s, s') = compact_univ LMap.empty [] 0 u in
+  (subst_univs_level_universe s u, s')
+
 (** Pretty-printing *)
 
 let pr_constraints prl = Constraint.pr prl
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 629d83fb8..aaed899bf 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -128,12 +128,6 @@ sig
 
   val map : (Level.t * int -> 'a) -> t -> 'a list
 
-  (** [compact u] remaps local variables in [u] such that their indices become
-       consecutive. It returns the new universe and the mapping.
-       Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] =
-         [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
-  *)
-  val compact : t -> t * int list
 end
 
 type universe = Universe.t
@@ -504,6 +498,13 @@ val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativit
 
 val make_abstract_instance : AUContext.t -> Instance.t
 
+(** [compact_univ u] remaps local variables in [u] such that their indices become
+     consecutive. It returns the new universe and the mapping.
+     Example: compact_univ [(Var 0, i); (Prop, 0); (Var 2; j))] =
+       [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
+*)
+val compact_univ : Universe.t -> Universe.t * int list
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_constraint_type : constraint_type -> Pp.t