From c9f3a6cbe5c410256fe88580019f5c7183bab097 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 7 Feb 2018 18:58:16 +0100 Subject: Fix #6677: Critical bug with VM and universes This bug was present since the first patch adding universe polymorphism handling in the VM (Coq 8.5). Note that unsoundness can probably be observed even without universe polymorphism. --- kernel/univ.ml | 37 +++++++++++++++++++++++++++++++++++-- 1 file changed, 35 insertions(+), 2 deletions(-) (limited to 'kernel/univ.ml') diff --git a/kernel/univ.ml b/kernel/univ.ml index f72f6f26a..835dbee08 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -266,7 +266,7 @@ struct module Expr = struct type t = Level.t * int - + (* Hashing of expressions *) module ExprHash = struct @@ -487,7 +487,40 @@ struct | [] -> cons a l 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 -- cgit v1.2.3