diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | kernel/cbytecodes.ml | 1 | ||||
| -rw-r--r-- | kernel/cbytecodes.mli | 1 | ||||
| -rw-r--r-- | kernel/cbytegen.ml | 31 | ||||
| -rw-r--r-- | test-suite/bugs/closed/7723.v | 58 |
5 files changed, 84 insertions, 9 deletions
@@ -88,6 +88,8 @@ Kernel - Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333). - Fix a critical bug with inlining of polymorphic constants (#7615). +- Fix a critical bug with universe polymorphism and vm_compute (#7723). Was + present since 8.5. Notations diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 487385a78..3095ce148 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -217,6 +217,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (* number of universes on the stack, *) (* universes are always at the bottom. *) nb_stack : int; (* number of variables on the stack *) diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 238edc0af..de21401b3 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -159,6 +159,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (** number of universes on the stack *) nb_stack : int; (** number of variables on the stack *) in_stack : int list; (** position in the stack *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 881bfae19..6677db2fd 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -112,8 +112,9 @@ let push_fv d e = { let fv r = !(r.in_env) -let empty_comp_env ?(univs=0) ()= - { nb_uni_stack = univs; +let empty_comp_env ()= + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -148,7 +149,8 @@ let rec add_param n sz l = if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l) let comp_env_fun ?(univs=0) arity = - { nb_uni_stack = univs ; + { arity; + nb_uni_stack = univs ; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = 0; @@ -159,7 +161,8 @@ let comp_env_fun ?(univs=0) arity = let comp_env_fix_type rfv = - { nb_uni_stack = 0; + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -173,7 +176,8 @@ let comp_env_fix ndef curr_pos arity rfv = for i = ndef downto 1 do prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec done; - { nb_uni_stack = 0; + { arity; + nb_uni_stack = 0; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; @@ -183,7 +187,8 @@ let comp_env_fix ndef curr_pos arity rfv = } let comp_env_cofix_type ndef rfv = - { nb_uni_stack = 0; + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -197,7 +202,8 @@ let comp_env_cofix ndef arity rfv = for i = 1 to ndef do prec := Kenvacc i :: !prec done; - { nb_uni_stack = 0; + { arity; + nb_uni_stack = 0; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; @@ -249,8 +255,15 @@ let pos_rel i r sz = Kenvacc(r.offset + pos) let pos_universe_var i r sz = - if i < r.nb_uni_stack then - Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) + (* Compilation of a universe variable can happen either at toplevel (the + current closure correspond to a constant and has local universes) or in a + local closure (which has no local universes). *) + if r.nb_uni_stack != 0 then + (* Universe variables are represented by De Bruijn levels (not indices), + starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq] + with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access + the last universe. *) + Kacc (sz - r.arity - (r.nb_uni_stack - i)) else let env = !(r.in_env) in let db = FVuniv_var i in diff --git a/test-suite/bugs/closed/7723.v b/test-suite/bugs/closed/7723.v new file mode 100644 index 000000000..216290123 --- /dev/null +++ b/test-suite/bugs/closed/7723.v @@ -0,0 +1,58 @@ +Set Universe Polymorphism. + +Module Segfault. + +Inductive decision_tree : Type := . + +Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B + := match ls with + | nil => None + | cons x xs + => match f x with + | Some v => Some v + | None => first_satisfying_helper f xs + end + end. + +Axiom admit : forall {T}, T. +Definition dtree4 : option decision_tree := + match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil) + with + | Some _ => admit + | None => admit + end +. +Definition dtree'' := Eval vm_compute in dtree4. (* segfault *) + +End Segfault. + +Module OtherExample. + +Definition bar@{i} := Type@{i}. +Definition foo@{i j} (x y z : nat) := + @id Type@{j} bar@{i}. +Eval vm_compute in foo. + +End OtherExample. + +Module LocalClosure. + +Definition bar@{i} := Type@{i}. + +Definition foo@{i j} (x y z : nat) := + @id (nat -> Type@{j}) (fun _ => Type@{i}). +Eval vm_compute in foo. + +End LocalClosure. + +Require Import Hurkens. +Polymorphic Inductive unit := tt. + +Polymorphic Definition foo := + let x := id tt in (x, x, Type). + +Lemma bad : False. + refine (TypeNeqSmallType.paradox (snd foo) _). + vm_compute. + Fail reflexivity. +Abort. |