diff options
Diffstat (limited to 'kernel')
47 files changed, 1045 insertions, 768 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 9118410549..1ba6a8c8fe 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -43,9 +43,7 @@ void init_arity () { arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= - arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]= - arity[LTFLOAT]=arity[LEFLOAT]= - arity[ISINT]=arity[AREINT2]=0; + 0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= @@ -75,9 +73,10 @@ void init_arity () { arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= - arity[ISARRAY_CAML_CALL1]=arity[ISINT_CAML_CALL2]= - arity[ISARRAY_INT_CAML_CALL2]=arity[ISARRAY_INT_CAML_CALL3]= - arity[PROJ]=2; + arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]= + arity[CHECKCAMLCALL2]=arity[CHECKCAMLCALL3_1]= + arity[PROJ]= + 2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.c index 84a3edf1c7..bea47dd47e 100644 --- a/kernel/byterun/coq_float64.h +++ b/kernel/byterun/coq_float64.c @@ -8,19 +8,40 @@ /* * (see LICENSE file for the text of the license) */ /************************************************************************/ -#ifndef _COQ_FLOAT64_ -#define _COQ_FLOAT64_ - #include <math.h> +#include <stdint.h> -#define DECLARE_FREL(name, e) \ - int coq_##name(double x, double y) { \ - return e; \ - } \ - \ - value coq_##name##_byte(value x, value y) { \ - return coq_##name(Double_val(x), Double_val(y)); \ - } +#define CAML_INTERNALS +#include <caml/alloc.h> + +#include "coq_values.h" + +union double_bits { + double d; + uint64_t u; +}; + +static double next_up(double x) { + union double_bits bits; + if (!(x < INFINITY)) return x; // x is +oo or NaN + bits.d = x; + int64_t i = bits.u; + if (i >= 0) ++bits.u; // x >= +0.0, go away from zero + else if (bits.u + bits.u == 0) bits.u = 1; // x is -0.0, should almost never happen + else --bits.u; // x < 0.0, go toward zero + return bits.d; +} + +static double next_down(double x) { + union double_bits bits; + if (!(x > -INFINITY)) return x; // x is -oo or NaN + bits.d = x; + int64_t i = bits.u; + if (i == 0) bits.u = INT64_MIN + 1; // x is +0.0 + else if (i < 0) ++bits.u; // x <= -0.0, go away from zero + else --bits.u; // x > 0.0, go toward zero + return bits.d; +} #define DECLARE_FBINOP(name, e) \ double coq_##name(double x, double y) { \ @@ -40,19 +61,14 @@ return caml_copy_double(coq_##name(Double_val(x))); \ } -DECLARE_FREL(feq, x == y) -DECLARE_FREL(flt, x < y) -DECLARE_FREL(fle, x <= y) DECLARE_FBINOP(fmul, x * y) DECLARE_FBINOP(fadd, x + y) DECLARE_FBINOP(fsub, x - y) DECLARE_FBINOP(fdiv, x / y) DECLARE_FUNOP(fsqrt, sqrt(x)) -DECLARE_FUNOP(next_up, nextafter(x, INFINITY)) -DECLARE_FUNOP(next_down, nextafter(x, -INFINITY)) +DECLARE_FUNOP(next_up, next_up(x)) +DECLARE_FUNOP(next_down, next_down(x)) value coq_is_double(value x) { return Val_long(Is_double(x)); } - -#endif /* _COQ_FLOAT64_ */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 1b6da7dd6f..6255250218 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -28,7 +28,6 @@ #include "coq_fix_code.h" #include "coq_memory.h" #include "coq_values.h" -#include "coq_float64.h" #if OCAML_VERSION < 41000 extern void caml_minor_collection(void); @@ -113,7 +112,7 @@ if (sp - num_args < coq_stack_threshold) { \ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } #define Setup_for_caml_call { *--sp = coq_env; coq_sp = sp; } -#define Restore_after_caml_call { sp = coq_sp; coq_env = *sp++; } +#define Restore_after_caml_call coq_env = *sp++; /* Register optimization. Some compilers underestimate the use of the local variables representing @@ -193,7 +192,9 @@ if (sp - num_args < coq_stack_threshold) { \ #endif #endif -#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag && Code_val(v) == accumulate) +/* We should also check "Code_val(v) == accumulate" to be sure, + but Is_accu is only used in places where closures cannot occur. */ +#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag) #define CheckPrimArgs(cond, apply_lbl) do{ \ if (cond) pc++; \ @@ -237,6 +238,9 @@ extern intnat volatile caml_pending_signals[]; extern void caml_process_pending_signals(void); #endif +extern double coq_next_up(double); +extern double coq_next_down(double); + /* The interpreter itself */ value coq_interprete @@ -712,8 +716,8 @@ value coq_interprete coq_extra_args = Long_val(sp[2]); sp += 3; } else { - /* The recursif argument is an accumulator */ - mlsize_t num_args, i; + /* The recursive argument is an accumulator */ + mlsize_t num_args, sz, i; value block; /* Construction of fixpoint applied to its [rec_pos-1] first arguments */ Alloc_small(accu, rec_pos + 3, Closure_tag); @@ -728,11 +732,22 @@ value coq_interprete accu = block; /* Construction of the accumulator */ num_args = coq_extra_args - rec_pos; - Alloc_small(block, 3 + num_args, Closure_tag); + sz = 3 + num_args; + if (sz <= Max_young_wosize) { + Alloc_small(block, sz, Closure_tag); + Field(block, 2) = accu; + for (i = 3; i < sz; ++i) + Field(block, i) = *sp++; + } else { + // too large for Alloc_small, so use caml_alloc_shr instead + // it never triggers a GC, so no need for Setup_for_gc + block = caml_alloc_shr(sz, Closure_tag); + caml_initialize(&Field(block, 2), accu); + for (i = 3; i < sz; ++i) + caml_initialize(&Field(block, i), *sp++); + } Code_val(block) = accumulate; Field(block, 1) = Val_int(2); - Field(block, 2) = accu; - for (i = 0; i < num_args; i++) Field(block, i + 3) = *sp++; accu = block; pc = (code_t)(sp[0]); coq_env = sp[1]; @@ -1126,13 +1141,25 @@ value coq_interprete /* Special operations for reduction of open term */ Instruct(ACCUMULATE) { - mlsize_t i, size; + mlsize_t i, size, sz; print_instr("ACCUMULATE"); size = Wosize_val(coq_env); - Alloc_small(accu, size + coq_extra_args + 1, Closure_tag); - for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i); - for(i = size; i <= coq_extra_args + size; i++) - Field(accu, i) = *sp++; + sz = size + coq_extra_args + 1; + if (sz <= Max_young_wosize) { + Alloc_small(accu, sz, Closure_tag); + for (i = 0; i < size; ++i) + Field(accu, i) = Field(coq_env, i); + for (i = size; i < sz; ++i) + Field(accu, i) = *sp++; + } else { + // too large for Alloc_small, so use caml_alloc_shr instead + // it never triggers a GC, so no need for Setup_for_gc + accu = caml_alloc_shr(sz, Closure_tag); + for (i = 0; i < size; ++i) + caml_initialize(&Field(accu, i), Field(coq_env, i)); + for (i = size; i < sz; ++i) + caml_initialize(&Field(accu, i), *sp++); + } pc = (code_t)(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); @@ -1236,13 +1263,24 @@ value coq_interprete Instruct(MAKEACCU) { - int i; + mlsize_t i, sz; print_instr("MAKEACCU"); - Alloc_small(accu, coq_extra_args + 4, Closure_tag); + sz = coq_extra_args + 4; + if (sz <= Max_young_wosize) { + Alloc_small(accu, sz, Closure_tag); + Field(accu, 2) = Field(coq_atom_tbl, *pc); + for (i = 3; i < sz; ++i) + Field(accu, i) = *sp++; + } else { + // too large for Alloc_small, so use caml_alloc_shr instead + // it never triggers a GC, so no need for Setup_for_gc + accu = caml_alloc_shr(sz, Closure_tag); + caml_initialize(&Field(accu, 2), Field(coq_atom_tbl, *pc)); + for (i = 3; i < sz; ++i) + caml_initialize(&Field(accu, i), *sp++); + } Code_val(accu) = accumulate; Field(accu, 1) = Val_int(2); - Field(accu, 2) = Field(coq_atom_tbl, *pc); - for (i = 2; i < coq_extra_args + 3; i++) Field(accu, i + 1) = *sp++; pc = (code_t)(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); @@ -1271,11 +1309,8 @@ value coq_interprete Instruct(CHECKADDINT63){ print_instr("CHECKADDINT63"); CheckInt2(); - } - Instruct(ADDINT63) { /* Adds the integer in the accumulator with the one ontop of the stack (which is poped)*/ - print_instr("ADDINT63"); Uint63_add(accu, *sp++); Next; } @@ -1309,9 +1344,6 @@ value coq_interprete Instruct (CHECKSUBINT63) { print_instr("CHECKSUBINT63"); CheckInt2(); - } - Instruct (SUBINT63) { - print_instr("SUBINT63"); /* returns the subtraction */ Uint63_sub(accu, *sp++); Next; @@ -1517,9 +1549,6 @@ value coq_interprete Instruct (CHECKLTINT63) { print_instr("CHECKLTINT63"); CheckInt2(); - } - Instruct (LTINT63) { - print_instr("LTINT63"); int b; Uint63_lt(b,accu,*sp++); accu = b ? coq_true : coq_false; @@ -1529,9 +1558,6 @@ value coq_interprete Instruct (CHECKLEINT63) { print_instr("CHECKLEINT63"); CheckInt2(); - } - Instruct (LEINT63) { - print_instr("LEINT63"); int b; Uint63_leq(b,accu,*sp++); accu = b ? coq_true : coq_false; @@ -1570,20 +1596,6 @@ value coq_interprete Next; } - Instruct (ISINT){ - print_instr("ISINT"); - accu = (Is_uint63(accu)) ? coq_true : coq_false; - Next; - } - - Instruct (AREINT2){ - print_instr("AREINT2"); - accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false; - sp++; - Next; - } - - Instruct (CHECKOPPFLOAT) { print_instr("CHECKOPPFLOAT"); CheckFloat1(); @@ -1601,27 +1613,21 @@ value coq_interprete Instruct (CHECKEQFLOAT) { print_instr("CHECKEQFLOAT"); CheckFloat2(); - accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + accu = Double_val(accu) == Double_val(*sp++) ? coq_true : coq_false; Next; } Instruct (CHECKLTFLOAT) { print_instr("CHECKLTFLOAT"); CheckFloat2(); - } - Instruct (LTFLOAT) { - print_instr("LTFLOAT"); - accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + accu = Double_val(accu) < Double_val(*sp++) ? coq_true : coq_false; Next; } Instruct (CHECKLEFLOAT) { print_instr("CHECKLEFLOAT"); CheckFloat2(); - } - Instruct (LEFLOAT) { - print_instr("LEFLOAT"); - accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + accu = Double_val(accu) <= Double_val(*sp++) ? coq_true : coq_false; Next; } @@ -1674,35 +1680,35 @@ value coq_interprete Instruct (CHECKADDFLOAT) { print_instr("CHECKADDFLOAT"); CheckFloat2(); - Coq_copy_double(coq_fadd(Double_val(accu), Double_val(*sp++))); + Coq_copy_double(Double_val(accu) + Double_val(*sp++)); Next; } Instruct (CHECKSUBFLOAT) { print_instr("CHECKSUBFLOAT"); CheckFloat2(); - Coq_copy_double(coq_fsub(Double_val(accu), Double_val(*sp++))); + Coq_copy_double(Double_val(accu) - Double_val(*sp++)); Next; } Instruct (CHECKMULFLOAT) { print_instr("CHECKMULFLOAT"); CheckFloat2(); - Coq_copy_double(coq_fmul(Double_val(accu), Double_val(*sp++))); + Coq_copy_double(Double_val(accu) * Double_val(*sp++)); Next; } Instruct (CHECKDIVFLOAT) { print_instr("CHECKDIVFLOAT"); CheckFloat2(); - Coq_copy_double(coq_fdiv(Double_val(accu), Double_val(*sp++))); + Coq_copy_double(Double_val(accu) / Double_val(*sp++)); Next; } Instruct (CHECKSQRTFLOAT) { print_instr("CHECKSQRTFLOAT"); CheckFloat1(); - Coq_copy_double(coq_fsqrt(Double_val(accu))); + Coq_copy_double(sqrt(Double_val(accu))); Next; } @@ -1784,11 +1790,25 @@ value coq_interprete Next; } + Instruct (CHECKNEXTUPFLOATINPLACE) { + print_instr("CHECKNEXTUPFLOATINPLACE"); + CheckFloat1(); + Store_double_val(accu, coq_next_up(Double_val(accu))); + Next; + } - Instruct(ISINT_CAML_CALL2) { + Instruct (CHECKNEXTDOWNFLOATINPLACE) { + print_instr("CHECKNEXTDOWNFLOATINPLACE"); + CheckFloat1(); + Store_double_val(accu, coq_next_down(Double_val(accu))); + Next; + } + + Instruct(CHECKCAMLCALL2_1) { + // arity-2 callback, the last argument can be an accumulator value arg; - print_instr("ISINT_CAML_CALL2"); - if (Is_uint63(accu)) { + print_instr("CHECKCAMLCALL2_1"); + if (!Is_accu(accu)) { pc++; print_int(*pc); arg = sp[0]; @@ -1801,47 +1821,50 @@ value coq_interprete Next; } - Instruct(ISARRAY_CAML_CALL1) { - print_instr("ISARRAY_CAML_CALL1"); - if (Is_coq_array(accu)) { - pc++; - Setup_for_caml_call; - print_int(*pc); - accu = caml_callback(Field(coq_global_data, *pc),accu); - Restore_after_caml_call; - pc++; - } - else pc += *pc; - Next; + Instruct(CHECKCAMLCALL1) { + // arity-1 callback, no argument can be an accumulator + print_instr("CHECKCAMLCALL1"); + if (!Is_accu(accu)) { + pc++; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback(Field(coq_global_data, *pc), accu); + Restore_after_caml_call; + pc++; + } + else pc += *pc; + Next; } - Instruct(ISARRAY_INT_CAML_CALL2) { + Instruct(CHECKCAMLCALL2) { + // arity-2 callback, no argument can be an accumulator value arg; - print_instr("ISARRAY_INT_CAML_CALL2"); - if (Is_coq_array(accu) && Is_uint63(sp[0])) { - pc++; - arg = sp[0]; - Setup_for_caml_call; - print_int(*pc); - accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); - Restore_after_caml_call; - sp += 1; - pc++; - } else pc += *pc; - Next; + print_instr("CHECKCAMLCALL2"); + if (!Is_accu(accu) && !Is_accu(sp[0])) { + pc++; + arg = sp[0]; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); + Restore_after_caml_call; + sp += 1; + pc++; + } else pc += *pc; + Next; } - Instruct(ISARRAY_INT_CAML_CALL3) { + Instruct(CHECKCAMLCALL3_1) { + // arity-3 callback, the last argument can be an accumulator value arg1; value arg2; - print_instr("ISARRAY_INT_CAML_CALL3"); - if (Is_coq_array(accu) && Is_uint63(sp[0])) { + print_instr("CHECKCAMLCALL3_1"); + if (!Is_accu(accu) && !Is_accu(sp[0])) { pc++; arg1 = sp[0]; arg2 = sp[1]; Setup_for_caml_call; print_int(*pc); - accu = caml_callback3(Field(coq_global_data, *pc),accu, arg1, arg2); + accu = caml_callback3(Field(coq_global_data, *pc), accu, arg1, arg2); Restore_after_caml_call; sp += 2; pc++; diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index ae5251c252..fe076f8f04 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -65,9 +65,10 @@ static void coq_scan_roots(scanning_action action) register value * i; /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { + if (!Is_block(*i)) continue; #ifdef NO_NAKED_POINTERS /* The VM stack may contain C-allocated bytecode */ - if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue; + if (!Is_in_heap_or_young(*i)) continue; #endif (*action) (*i, i); }; diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index f07018711b..0cdef34050 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -30,9 +30,6 @@ #define Is_double(v) (Tag_val(v) == Double_tag) #define Is_tailrec_switch(v) (Field(v,1) == Val_true) -/* coq array */ -#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1)) - /* coq values for primitive operations */ #define coq_tag_C1 2 #define coq_tag_C0 1 diff --git a/kernel/byterun/dune b/kernel/byterun/dune index 2998178be2..d3e2a2fa7f 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -4,7 +4,7 @@ (public_name coq.vm) (foreign_stubs (language c) - (names coq_fix_code coq_memory coq_values coq_interp) + (names coq_fix_code coq_float64 coq_memory coq_values coq_interp) (flags (:include %{project_root}/config/dune.c_flags)))) (rule diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index a23ef8fdca..c9326615dc 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -263,7 +263,7 @@ let assoc_defined id env = match Environ.lookup_named id env with * before the term is computed. *) -(* Norm means the term is fully normalized and cannot create a redex +(* Ntrl means the term is fully normalized and cannot create a redex when substituted Cstr means the term is in head normal form and that it can create a redex when substituted (i.e. constructor, fix, lambda) @@ -271,10 +271,10 @@ let assoc_defined id env = match Environ.lookup_named id env with create a redex when substituted Red is used for terms that might be reduced *) -type red_state = Norm | Cstr | Whnf | Red +type red_state = Ntrl | Cstr | Whnf | Red let neutr = function - | Whnf|Norm -> Whnf + | Whnf|Ntrl -> Whnf | Red|Cstr -> Red type optrel = Unknown | KnownR | KnownI @@ -293,13 +293,13 @@ module Mark : sig val neutr : t -> t - val set_norm : t -> t + val set_ntrl : t -> t end = struct type t = int let[@inline] of_state = function - | Norm -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11 + | Ntrl -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11 let[@inline] of_relevance = function | Unknown -> 0 @@ -315,15 +315,15 @@ end = struct | _ -> assert false let[@inline] red_state x = match x land 0b1100 with - | 0b0000 -> Norm + | 0b0000 -> Ntrl | 0b0100 -> Cstr | 0b1000 -> Whnf | 0b1100 -> Red | _ -> assert false - let[@inline] neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *) + let[@inline] neutr x = x lor 0b1000 (* Whnf|Ntrl -> Whnf | Red|Cstr -> Red *) - let[@inline] set_norm x = x land 0b0011 + let[@inline] set_ntrl x = x land 0b0011 end let mark = Mark.mark @@ -358,10 +358,10 @@ and fterm = and finvert = Univ.Instance.t * fconstr array let fterm_of v = v.term -let set_norm v = v.mark <- Mark.set_norm v.mark -let is_val v = match Mark.red_state v.mark with Norm -> true | Cstr | Whnf | Red -> false +let set_ntrl v = v.mark <- Mark.set_ntrl v.mark +let is_val v = match Mark.red_state v.mark with Ntrl -> true | Cstr | Whnf | Red -> false -let mk_atom c = {mark=mark Norm Unknown;term=FAtom c} +let mk_atom c = {mark=mark Ntrl Unknown;term=FAtom c} let mk_red f = {mark=mark Red Unknown;term=f} (* Could issue a warning if no is still Red, pointing out that we loose @@ -448,7 +448,7 @@ let rec lft_fconstr n ft = let r = Mark.relevance ft.mark in match ft.term with | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _|FFloat _) -> ft - | FRel i -> {mark=mark Norm r;term=FRel(i+n)} + | FRel i -> {mark=mark Ntrl r;term=FRel(i+n)} | FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))} | FFix(fx,e) -> {mark=mark Cstr r; term=FFix(fx,subs_shft(n,e))} @@ -466,7 +466,7 @@ let lift_fconstr_vect k v = let clos_rel e i = match expand_rel i e with | Inl(n,mt) -> lift_fconstr n mt - | Inr(k,None) -> {mark=mark Norm Unknown; term= FRel k} + | Inr(k,None) -> {mark=mark Ntrl Unknown; term= FRel k} | Inr(k,Some p) -> lift_fconstr (k-p) {mark=mark Red Unknown;term=FFlex(RelKey p)} @@ -488,7 +488,7 @@ let compact_stack head stk = (* Put an update mark in the stack, only if needed *) let zupdate info m s = let share = info.i_cache.i_share in - if share && begin match Mark.red_state m.mark with Red -> true | Norm | Whnf | Cstr -> false end + if share && begin match Mark.red_state m.mark with Red -> true | Ntrl | Whnf | Cstr -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -514,8 +514,8 @@ let mk_clos e t = | Rel i -> clos_rel e i | Var x -> {mark = mark Red Unknown; term = FFlex (VarKey x) } | Const c -> {mark = mark Red Unknown; term = FFlex (ConstKey c) } - | Meta _ | Sort _ -> {mark = mark Norm KnownR; term = FAtom t } - | Ind kn -> {mark = mark Norm KnownR; term = FInd kn } + | Meta _ | Sort _ -> {mark = mark Ntrl KnownR; term = FAtom t } + | Ind kn -> {mark = mark Ntrl KnownR; term = FInd kn } | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn } | Int i -> {mark = mark Cstr Unknown; term = FInt i} | Float f -> {mark = mark Cstr Unknown; term = FFloat f} @@ -734,11 +734,11 @@ let strip_update_shift_app_red head stk = strip_rec [] head 0 stk let strip_update_shift_app head stack = - assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true); + assert (match Mark.red_state head.mark with Red -> false | Ntrl | Cstr | Whnf -> true); strip_update_shift_app_red head stack let get_nth_arg head n stk = - assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true); + assert (match Mark.red_state head.mark with Red -> false | Ntrl | Cstr | Whnf -> true); let rec strip_rec rstk h n = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) n s @@ -787,7 +787,7 @@ let rec eta_expand_stack = function | Zshift _ | Zupdate _ | Zprimitive _ as e) :: s -> e :: eta_expand_stack s | [] -> - [Zshift 1; Zapp [|{mark=mark Norm Unknown; term= FRel 1}|]] + [Zshift 1; Zapp [|{mark=mark Ntrl Unknown; term= FRel 1}|]] (* Get the arguments of a native operator *) let rec skip_native_args rargs nargs = @@ -968,7 +968,7 @@ module FNativeEntries = | FArray (_u,t,_ty) -> t | _ -> raise Not_found - let dummy = {mark = mark Norm KnownR; term = FRel 0} + let dummy = {mark = mark Ntrl KnownR; term = FRel 0} let current_retro = ref Retroknowledge.empty let defined_int = ref false @@ -978,7 +978,7 @@ module FNativeEntries = match retro.Retroknowledge.retro_int63 with | Some c -> defined_int := true; - fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } + fint := { mark = mark Ntrl KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } | None -> defined_int := false let defined_float = ref false @@ -988,7 +988,7 @@ module FNativeEntries = match retro.Retroknowledge.retro_float64 with | Some c -> defined_float := true; - ffloat := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } + ffloat := { mark = mark Ntrl KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } | None -> defined_float := false let defined_bool = ref false @@ -1039,7 +1039,7 @@ module FNativeEntries = fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) }; fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) }; let (icmp, _) = cEq in - fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) } + fcmp := { mark = mark Ntrl KnownR; term = FInd (Univ.in_punivs icmp) } | None -> defined_cmp := false let defined_f_cmp = ref false @@ -1098,14 +1098,8 @@ module FNativeEntries = let defined_array = ref false - let farray = ref dummy - let init_array retro = - match retro.Retroknowledge.retro_array with - | Some c -> - defined_array := true; - farray := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } - | None -> defined_array := false + defined_array := Option.has_some retro.Retroknowledge.retro_array let init env = current_retro := env.retroknowledge; @@ -1165,7 +1159,7 @@ module FNativeEntries = let mkFloat env f = check_float env; - { mark = mark Norm KnownR; term = FFloat f } + { mark = mark Cstr KnownR; term = FFloat f } let mkBool env b = check_bool env; @@ -1328,20 +1322,24 @@ let rec knr info tab m stk = | FFlex(ConstKey (kn,_u as c)) when red_set info.i_flags (fCONST kn) -> (match ref_value_cache info tab (ConstKey c) with | Def v -> kni info tab v stk - | Primitive op when check_native_args op stk -> - let rargs, a, nargs, stk = get_native_args1 op c stk in - kni info tab a (Zprimitive(op,c,rargs,nargs)::stk) - | Undef _ | OpaqueDef _ | Primitive _ -> (set_norm m; (m,stk))) + | Primitive op -> + if check_native_args op stk then + let rargs, a, nargs, stk = get_native_args1 op c stk in + kni info tab a (Zprimitive(op,c,rargs,nargs)::stk) + else + (* Similarly to fix, partially applied primitives are not Ntrl! *) + (m, stk) + | Undef _ | OpaqueDef _ -> (set_ntrl m; (m,stk))) | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> (match ref_value_cache info tab (VarKey id) with | Def v -> kni info tab v stk | Primitive _ -> assert false - | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk))) + | OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk))) | FFlex(RelKey k) when red_set info.i_flags fDELTA -> (match ref_value_cache info tab (RelKey k) with | Def v -> kni info tab v stk | Primitive _ -> assert false - | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk))) + | OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk))) | FConstruct((_ind,c),_u) -> let use_match = red_set info.i_flags fMATCH in let use_fix = red_set info.i_flags fFIX in @@ -1525,13 +1523,18 @@ let norm_val info tab v = with_stats (lazy (kl info tab v)) let whd_stack infos tab m stk = match Mark.red_state m.mark with -| Whnf | Norm -> +| Whnf | Ntrl -> (** No need to perform [kni] nor to unlock updates because - every head subterm of [m] is [Whnf] or [Norm] *) + every head subterm of [m] is [Whnf] or [Ntrl] *) knh infos m stk | Red | Cstr -> let k = kni infos tab m stk in - let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *) + let () = + if infos.i_cache.i_share then + (* to unlock Zupdates! *) + let (m', stk') = k in + if not (m == m' && stk == stk') then ignore (zip m' stk') + in k let create_clos_infos ?univs ?(evars=fun _ -> None) flgs env = diff --git a/kernel/constr.ml b/kernel/constr.ml index 1837a39764..3157ec9f57 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -353,9 +353,9 @@ let isRef c = match kind c with let isRefX x c = let open GlobRef in match x, kind c with - | ConstRef c, Const (c', _) -> Constant.equal c c' - | IndRef i, Ind (i', _) -> eq_ind i i' - | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c' + | IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i' + | ConstructRef i, Construct (i', _) -> Construct.CanOrd.equal i i' | VarRef id, Var id' -> Id.equal id id' | _ -> false @@ -950,14 +950,14 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t let len = Array.length l1 in Int.equal len (Array.length l2) && leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 - | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2 + | Proj (p1,c1), Proj (p2,c2) -> Projection.CanOrd.equal p1 p2 && eq 0 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> (* The args length currently isn't used but may as well pass it. *) - Constant.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2 - | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2 + Constant.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> Ind.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2 | Construct (c1,u1), Construct (c2,u2) -> - eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 + Construct.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> eq 0 p1 p2 && eq_invert (eq 0) (leq_universes None) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> @@ -1139,9 +1139,9 @@ let constr_ord_int f t1 t2 = | App _, _ -> -1 | _, App _ -> 1 | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2 | Const _, _ -> -1 | _, Const _ -> 1 - | Ind (ind1, _u1), Ind (ind2, _u2) -> ind_ord ind1 ind2 + | Ind (ind1, _u1), Ind (ind2, _u2) -> Ind.CanOrd.compare ind1 ind2 | Ind _, _ -> -1 | _, Ind _ -> 1 - | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2 + | Construct (ct1,_u1), Construct (ct2,_u2) -> Construct.CanOrd.compare ct1 ct2 | Construct _, _ -> -1 | _, Construct _ -> 1 | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> let c = f p1 p2 in @@ -1158,7 +1158,7 @@ let constr_ord_int f t1 t2 = ((Int.compare =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 | CoFix _, _ -> -1 | _, CoFix _ -> 1 - | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 + | Proj (p1,c1), Proj (p2,c2) -> (Projection.CanOrd.compare =? f) p1 p2 c1 c2 | Proj _, _ -> -1 | _, Proj _ -> 1 | Int i1, Int i2 -> Uint63.compare i1 i2 | Int _, _ -> -1 | _, Int _ -> 1 @@ -1331,11 +1331,11 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Ind (ind,u) -> let u', hu = sh_instance u in (Ind (sh_ind ind, u'), - combinesmall 10 (combine (ind_syntactic_hash ind) hu)) + combinesmall 10 (combine (Ind.SyntacticOrd.hash ind) hu)) | Construct (c,u) -> let u', hu = sh_instance u in (Construct (sh_construct c, u'), - combinesmall 11 (combine (constructor_syntactic_hash c) hu)) + combinesmall 11 (combine (Construct.SyntacticOrd.hash c) hu)) | Case (ci,p,iv,c,bl) -> let p, hp = sh_rec p and iv, hiv = sh_invert iv @@ -1442,11 +1442,11 @@ let rec hash t = | Evar (e,l) -> combinesmall 8 (combine (Evar.hash e) (hash_term_list l)) | Const (c,u) -> - combinesmall 9 (combine (Constant.hash c) (Instance.hash u)) + combinesmall 9 (combine (Constant.CanOrd.hash c) (Instance.hash u)) | Ind (ind,u) -> - combinesmall 10 (combine (ind_hash ind) (Instance.hash u)) + combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u)) | Construct (c,u) -> - combinesmall 11 (combine (constructor_hash c) (Instance.hash u)) + combinesmall 11 (combine (Construct.CanOrd.hash c) (Instance.hash u)) | Case (_ , p, iv, c, bl) -> combinesmall 12 (combine4 (hash c) (hash p) (hash_invert iv) (hash_term_array bl)) | Fix (_ln ,(_, tl, bl)) -> @@ -1456,7 +1456,7 @@ let rec hash t = | Meta n -> combinesmall 15 n | Rel n -> combinesmall 16 n | Proj (p,c) -> - combinesmall 17 (combine (Projection.hash p) (hash c)) + combinesmall 17 (combine (Projection.CanOrd.hash p) (hash c)) | Int i -> combinesmall 18 (Uint63.hash i) | Float f -> combinesmall 19 (Float64.hash f) | Array(u,t,def,ty) -> @@ -1503,7 +1503,7 @@ struct let h3 = Array.fold_left hash_bool_list 0 info.cstr_tags in combine3 h1 h2 h3 let hash ci = - let h1 = ind_hash ci.ci_ind in + let h1 = Ind.CanOrd.hash ci.ci_ind in let h2 = Int.hash ci.ci_npar in let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in let h4 = Array.fold_left combine 0 ci.ci_cstr_nargs in diff --git a/kernel/context.ml b/kernel/context.ml index 6a99f201f3..ab66898b59 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -365,6 +365,15 @@ struct let ty' = f ty in if v == v' && ty == ty' then decl else LocalDef (id, v', ty') + let map_constr_het f = function + | LocalAssum (id, ty) -> + let ty' = f ty in + LocalAssum (id, ty') + | LocalDef (id, v, ty) -> + let v' = f v in + let ty' = f ty in + LocalDef (id, v', ty') + (** Perform a given action on all terms in a given declaration. *) let iter_constr f = function | LocalAssum (_, ty) -> f ty diff --git a/kernel/context.mli b/kernel/context.mli index 76c4461760..29309daf34 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -231,6 +231,9 @@ sig (** Map all terms in a given declaration. *) val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt + (** Map all terms, with an heterogeneous function. *) + val map_constr_het : ('a -> 'b) -> ('a, 'a) pt -> ('b, 'b) pt + (** Perform a given action on all terms in a given declaration. *) val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit diff --git a/kernel/cooking.ml b/kernel/cooking.ml index fdcf44c943..3707a75157 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -38,14 +38,14 @@ struct type t = my_global_reference let equal gr1 gr2 = match gr1, gr2 with | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2 - | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2 - | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2 + | IndRef i1, IndRef i2 -> Ind.SyntacticOrd.equal i1 i2 + | ConstructRef c1, ConstructRef c2 -> Construct.SyntacticOrd.equal c1 c2 | _ -> false open Hashset.Combine let hash = function | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c) - | IndRef i -> combinesmall 2 (ind_syntactic_hash i) - | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c) + | IndRef i -> combinesmall 2 (Ind.SyntacticOrd.hash i) + | ConstructRef c -> combinesmall 3 (Construct.SyntacticOrd.hash c) end module RefTable = Hashtbl.Make(RefHash) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index b9f434f179..8de7123fee 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -157,15 +157,15 @@ let hcons_const_body cb = (** {6 Inductive types } *) let eq_nested_type t1 t2 = match t1, t2 with -| NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2 +| NestedInd ind1, NestedInd ind2 -> Names.Ind.CanOrd.equal ind1 ind2 | NestedInd _, _ -> false -| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2 +| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2 | NestedPrimitive _, _ -> false let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true | Norec, _ -> false -| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 +| Mrec i1, Mrec i2 -> Names.Ind.CanOrd.equal i1 i2 | Mrec _, _ -> false | Nested ty1, Nested ty2 -> eq_nested_type ty1 ty2 | Nested _, _ -> false diff --git a/kernel/entries.ml b/kernel/entries.ml index ae64112e33..1bfc740017 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -20,6 +20,8 @@ type universes_entry = | Monomorphic_entry of Univ.ContextSet.t | Polymorphic_entry of Name.t array * Univ.UContext.t +type variance_entry = Univ.Variance.t option array + type 'a in_universes_entry = 'a * universes_entry (** {6 Declaration of inductive types. } *) @@ -50,9 +52,10 @@ type mutual_inductive_entry = { mind_entry_inds : one_inductive_entry list; mind_entry_universes : universes_entry; mind_entry_template : bool; (* Use template polymorphism *) - mind_entry_cumulative : bool; - (* universe constraints and the constraints for subtyping of - inductive types in the block. *) + mind_entry_variance : variance_entry option; + (* [None] if non-cumulative, otherwise associates each universe of + the entry to [None] if to be inferred or [Some v] if to be + checked. *) mind_entry_private : bool option; } diff --git a/kernel/environ.ml b/kernel/environ.ml index dec9e1deb8..a5f81d1e59 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -43,7 +43,6 @@ type key = int CEphemeron.key option ref type link_info = | Linked of string - | LinkedInteractive of string | NotLinked type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) @@ -104,7 +103,6 @@ type env = { env_typing_flags : typing_flags; retroknowledge : Retroknowledge.retroknowledge; indirect_pterms : Opaqueproof.opaquetab; - native_symbols : Nativevalues.symbols DPmap.t; } let empty_named_context_val = { @@ -136,7 +134,6 @@ let empty_env = { env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; indirect_pterms = Opaqueproof.empty_opaquetab; - native_symbols = DPmap.empty; } @@ -482,6 +479,9 @@ let set_typing_flags c env = let env = set_type_in_type (not c.check_universes) env in env +let update_typing_flags ?typing_flags env = + Option.cata (fun flags -> set_typing_flags flags env) env typing_flags + let set_cumulative_sprop b env = set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env @@ -571,6 +571,11 @@ let is_primitive env c = | Declarations.Primitive _ -> true | _ -> false +let is_array_type env c = + match env.retroknowledge.Retroknowledge.retro_array with + | None -> false + | Some c' -> Constant.CanOrd.equal c c' + let polymorphic_constant cst env = Declareops.constant_is_polymorphic (lookup_constant cst env) @@ -829,6 +834,65 @@ let is_type_in_type env r = let set_retroknowledge env r = { env with retroknowledge = r } -let set_native_symbols env native_symbols = { env with native_symbols } -let add_native_symbols dir syms env = - { env with native_symbols = DPmap.add dir syms env.native_symbols } +module type QNameS = +sig + type t + val equal : env -> t -> t -> bool + val compare : env -> t -> t -> int + val hash : env -> t -> int +end + +module QConstant = +struct + type t = Constant.t + let equal _env c1 c2 = Constant.CanOrd.equal c1 c2 + let compare _env c1 c2 = Constant.CanOrd.compare c1 c2 + let hash _env c = Constant.CanOrd.hash c +end + +module QMutInd = +struct + type t = MutInd.t + let equal _env c1 c2 = MutInd.CanOrd.equal c1 c2 + let compare _env c1 c2 = MutInd.CanOrd.compare c1 c2 + let hash _env c = MutInd.CanOrd.hash c +end + +module QInd = +struct + type t = Ind.t + let equal _env c1 c2 = Ind.CanOrd.equal c1 c2 + let compare _env c1 c2 = Ind.CanOrd.compare c1 c2 + let hash _env c = Ind.CanOrd.hash c +end + +module QConstruct = +struct + type t = Construct.t + let equal _env c1 c2 = Construct.CanOrd.equal c1 c2 + let compare _env c1 c2 = Construct.CanOrd.compare c1 c2 + let hash _env c = Construct.CanOrd.hash c +end + +module QProjection = +struct + type t = Projection.t + let equal _env c1 c2 = Projection.CanOrd.equal c1 c2 + let compare _env c1 c2 = Projection.CanOrd.compare c1 c2 + let hash _env c = Projection.CanOrd.hash c + module Repr = + struct + type t = Projection.Repr.t + let equal _env c1 c2 = Projection.Repr.CanOrd.equal c1 c2 + let compare _env c1 c2 = Projection.Repr.CanOrd.compare c1 c2 + let hash _env c = Projection.Repr.CanOrd.hash c + end +end + +module QGlobRef = +struct + type t = GlobRef.t + let equal _env c1 c2 = GlobRef.CanOrd.equal c1 c2 + let compare _env c1 c2 = GlobRef.CanOrd.compare c1 c2 + let hash _env c = GlobRef.CanOrd.hash c +end diff --git a/kernel/environ.mli b/kernel/environ.mli index f443ba38e1..900e2128ea 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -37,7 +37,6 @@ val dummy_lazy_val : unit -> lazy_val (** Linking information for the native compiler *) type link_info = | Linked of string - | LinkedInteractive of string | NotLinked type key = int CEphemeron.key option ref @@ -90,7 +89,6 @@ type env = private { env_typing_flags : typing_flags; retroknowledge : Retroknowledge.retroknowledge; indirect_pterms : Opaqueproof.opaquetab; - native_symbols : Nativevalues.symbols DPmap.t; } val oracle : env -> Conv_oracle.oracle @@ -251,6 +249,8 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option val is_primitive : env -> Constant.t -> bool +val is_array_type : env -> Constant.t -> bool + (** {6 Primitive projections} *) (** Checks that the number of parameters is correct. *) @@ -284,6 +284,32 @@ val template_polymorphic_ind : inductive -> env -> bool val template_polymorphic_variables : inductive -> env -> Univ.Level.t list val template_polymorphic_pind : pinductive -> env -> bool +(** {6 Name quotients} *) + +module type QNameS = +sig + type t + val equal : env -> t -> t -> bool + val compare : env -> t -> t -> int + val hash : env -> t -> int +end + +module QConstant : QNameS with type t = Constant.t + +module QMutInd : QNameS with type t = MutInd.t + +module QInd : QNameS with type t = Ind.t + +module QConstruct : QNameS with type t = Construct.t + +module QProjection : +sig + include QNameS with type t = Projection.t + module Repr : QNameS with type t = Projection.Repr.t +end + +module QGlobRef : QNameS with type t = GlobRef.t + (** {5 Modules } *) val add_modtype : module_type_body -> env -> env @@ -325,6 +351,9 @@ val set_type_in_type : bool -> env -> env val set_allow_sprop : bool -> env -> env val sprop_allowed : env -> bool +(** [update_typing_flags ?typing_flags] may update env with optional typing flags *) +val update_typing_flags : ?typing_flags:typing_flags -> env -> env + val universes_of_global : env -> GlobRef.t -> AUContext.t (** {6 Sets of referred section variables } @@ -388,6 +417,3 @@ val no_link_info : link_info (** Primitives *) val set_retroknowledge : env -> Retroknowledge.retroknowledge -> env - -val set_native_symbols : env -> Nativevalues.symbols DPmap.t -> env -val add_native_symbols : DirPath.t -> Nativevalues.symbols -> env -> env diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index f052e03cde..dc2cd349ce 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -104,11 +104,9 @@ let opcodes = "MAKEPROD"; "BRANCH"; "CHECKADDINT63"; - "ADDINT63"; "CHECKADDCINT63"; "CHECKADDCARRYCINT63"; "CHECKSUBINT63"; - "SUBINT63"; "CHECKSUBCINT63"; "CHECKSUBCARRYCINT63"; "CHECKMULINT63"; @@ -127,21 +125,15 @@ let opcodes = "CHECKLSRINT63CONST1"; "CHECKEQINT63"; "CHECKLTINT63"; - "LTINT63"; "CHECKLEINT63"; - "LEINT63"; "CHECKCOMPAREINT63"; "CHECKHEAD0INT63"; "CHECKTAIL0INT63"; - "ISINT"; - "AREINT2"; "CHECKOPPFLOAT"; "CHECKABSFLOAT"; "CHECKEQFLOAT"; "CHECKLTFLOAT"; - "LTFLOAT"; "CHECKLEFLOAT"; - "LEFLOAT"; "CHECKCOMPAREFLOAT"; "CHECKCLASSIFYFLOAT"; "CHECKADDFLOAT"; @@ -155,10 +147,12 @@ let opcodes = "CHECKLDSHIFTEXP"; "CHECKNEXTUPFLOAT"; "CHECKNEXTDOWNFLOAT"; - "ISINT_CAML_CALL2"; - "ISARRAY_CAML_CALL1"; - "ISARRAY_INT_CAML_CALL2"; - "ISARRAY_INT_CAML_CALL3"; + "CHECKNEXTUPFLOATINPLACE"; + "CHECKNEXTDOWNFLOATINPLACE"; + "CHECKCAMLCALL2_1"; + "CHECKCAMLCALL1"; + "CHECKCAMLCALL2"; + "CHECKCAMLCALL3_1"; "STOP" |] diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index b2520b780f..33ee8c325a 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -369,15 +369,20 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = data, Some None in - let variance = if not mie.mind_entry_cumulative then None - else match mie.mind_entry_universes with + let variance = match mie.mind_entry_variance with + | None -> None + | Some variances -> + match mie.mind_entry_universes with | Monomorphic_entry _ -> CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.") | Polymorphic_entry (_,uctx) -> let univs = Instance.to_array @@ UContext.instance uctx in + let univs = Array.map2 (fun a b -> a,b) univs variances in let univs = match sec_univs with | None -> univs - | Some sec_univs -> Array.append sec_univs univs + | Some sec_univs -> + let sec_univs = Array.map (fun u -> u, None) sec_univs in + Array.append sec_univs univs in let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in Some variances diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d751d9875a..ce12d65614 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -330,33 +330,45 @@ let check_allowed_sort ksort specif = let s = inductive_sort_family (snd specif) in raise (LocalArity (Some(elim_sort specif, ksort,s,error_elim_explain ksort s))) -let is_correct_arity env c pj ind specif params = +let check_correct_arity env c pj ind specif params = + (* We use l2r:true for compat with old versions which used CONV + instead of CUMUL called with arguments flipped. It is relevant + for performance eg in bedrock / Kami. *) let arsign,_ = get_instantiated_arity ind specif params in - let rec srec env pt ar = + let rec srec env ar pt = let pt' = whd_all env pt in - match kind pt', ar with - | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> - let () = - try conv env a1 a1' - with NotConvertible -> raise (LocalArity None) in - srec (push_rel (LocalAssum (na1,a1)) env) t ar' - (* The last Prod domain is the type of the scrutinee *) - | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) - let env' = push_rel (LocalAssum (na1,a1)) env in - let ksort = match kind (whd_all env' a2) with - | Sort s -> Sorts.family s - | _ -> raise (LocalArity None) in - let dep_ind = build_dependent_inductive ind specif params in - let _ = - try conv env a1 dep_ind - with NotConvertible -> raise (LocalArity None) in - check_allowed_sort ksort specif - | _, (LocalDef _ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' - | _ -> - raise (LocalArity None) + match ar, kind pt' with + | (LocalAssum (_,a1))::ar', Prod (na1,a1',t) -> + let () = + try conv_leq ~l2r:true env a1 a1' + with NotConvertible -> raise (LocalArity None) in + srec (push_rel (LocalAssum (na1,a1)) env) ar' t + (* The last Prod domain is the type of the scrutinee *) + | [], Prod (na1,a1',a2) -> + let env' = push_rel (LocalAssum (na1,a1')) env in + let ksort = match kind (whd_all env' a2) with + | Sort s -> Sorts.family s + | _ -> raise (LocalArity None) + in + let dep_ind = build_dependent_inductive ind specif params in + let () = + (* This ensures that the type of the scrutinee is <= the + inductive type declared in the predicate. *) + try conv_leq ~l2r:true env dep_ind a1' + with NotConvertible -> raise (LocalArity None) + in + let () = check_allowed_sort ksort specif in + (* We return the "higher" inductive universe instance from the predicate, + the branches must be typeable using these universes. + The find_rectype call cannot fail due to the cumulativity check above. *) + let (pind, _args) = find_rectype env a1' in + pind + | (LocalDef _ as d)::ar', _ -> + srec (push_rel d env) ar' (lift 1 pt') + | _ -> + raise (LocalArity None) in - try srec env pj.uj_type (List.rev arsign) + try srec env (List.rev arsign) pj.uj_type with LocalArity kinds -> error_elim_arity env ind c pj kinds @@ -387,24 +399,23 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let build_case_type env n p c realargs = whd_betaiota env (Term.lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c]))) -let type_case_branches env (pind,largs) pj c = - let specif = lookup_mind_specif env (fst pind) in +let type_case_branches env ((ind, _ as pind),largs) pj c = + let specif = lookup_mind_specif env ind in let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in - let () = is_correct_arity env c pj pind specif params in + let pind = check_correct_arity env c pj pind specif params in let lc = build_branches_type pind specif params p in let ty = build_case_type env (snd specif).mind_nrealdecls p c realargs in (lc, ty) - (************************************************************************) (* Checking the case annotation is relevant *) let check_case_info env (indsp,u) r ci = let (mib,mip as spec) = lookup_mind_specif env indsp in if - not (eq_ind indsp ci.ci_ind) || + not (Ind.CanOrd.equal indsp ci.ci_ind) || not (Int.equal mib.mind_nparams ci.ci_npar) || not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) || not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) || @@ -467,12 +478,12 @@ let inter_recarg r1 r2 = match r1, r2 with | Norec, _ -> None | Mrec i1, Mrec i2 | Nested (NestedInd i1), Nested (NestedInd i2) -| Mrec i1, (Nested (NestedInd i2)) -> if Names.eq_ind i1 i2 then Some r1 else None +| Mrec i1, (Nested (NestedInd i2)) -> if Names.Ind.CanOrd.equal i1 i2 then Some r1 else None | Mrec _, _ -> None -| Nested (NestedInd i1), Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None +| Nested (NestedInd i1), Mrec i2 -> if Names.Ind.CanOrd.equal i1 i2 then Some r2 else None | Nested (NestedInd _), _ -> None | Nested (NestedPrimitive c1), Nested (NestedPrimitive c2) -> - if Names.Constant.equal c1 c2 then Some r1 else None + if Names.Constant.CanOrd.equal c1 c2 then Some r1 else None | Nested (NestedPrimitive _), _ -> None let inter_wf_paths = Rtree.inter Declareops.eq_recarg inter_recarg Norec @@ -556,7 +567,7 @@ let lookup_subterms env ind = let match_inductive ind ra = match ra with - | Mrec i | Nested (NestedInd i) -> eq_ind ind i + | Mrec i | Nested (NestedInd i) -> Ind.CanOrd.equal ind i | Norec | Nested (NestedPrimitive _) -> false (* In {match c as z in ci y_s return P with |C_i x_s => t end} @@ -644,7 +655,7 @@ let abstract_mind_lc ntyps npars lc = let is_primitive_positive_container env c = match env.retroknowledge.Retroknowledge.retro_array with - | Some c' when Constant.equal c c' -> true + | Some c' when QConstant.equal env c c' -> true | _ -> false (* [get_recargs_approx env tree ind args] builds an approximation of the recargs @@ -667,13 +678,13 @@ let get_recargs_approx env tree ind args = (* When the inferred tree allows it, we consider that we have a potential nested inductive type *) begin match dest_recarg tree with - | Nested (NestedInd kn') | Mrec kn' when eq_ind (fst ind_kn) kn' -> + | Nested (NestedInd kn') | Mrec kn' when Ind.CanOrd.equal (fst ind_kn) kn' -> build_recargs_nested ienv tree (ind_kn, largs) | _ -> mk_norec end | Const (c,_) when is_primitive_positive_container env c -> begin match dest_recarg tree with - | Nested (NestedPrimitive c') when Constant.equal c c' -> + | Nested (NestedPrimitive c') when QConstant.equal env c c' -> build_recargs_nested_primitive ienv tree (c, largs) | _ -> mk_norec end diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 8191a5b0f3..d02f92ef26 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -15,30 +15,82 @@ open Univ open Variance open Util -type inferred = IrrelevantI | CovariantI - -(** Throughout this module we modify a map [variances] from local - universes to [inferred]. It starts as a trivial mapping to - [Irrelevant] and every time we encounter a local universe we - restrict it accordingly. - [Invariant] universes are removed from the map. -*) exception TrivialVariance -let maybe_trivial variances = - if LMap.is_empty variances then raise TrivialVariance - else variances +(** Not the same as Type_errors.BadVariance because we don't have the env where we raise. *) +exception BadVariance of Level.t * Variance.t * Variance.t +(* some ocaml bug is triggered if we make this an inline record *) -let infer_level_eq u variances = - maybe_trivial (LMap.remove u variances) +module Inf : sig + type variances + val infer_level_eq : Level.t -> variances -> variances + val infer_level_leq : Level.t -> variances -> variances + val start : (Level.t * Variance.t option) array -> variances + val finish : variances -> Variance.t array +end = struct + type inferred = IrrelevantI | CovariantI + type mode = Check | Infer -let infer_level_leq u variances = - (* can only set Irrelevant -> Covariant so nontrivial *) - LMap.update u (function - | None -> None - | Some CovariantI as x -> x - | Some IrrelevantI -> Some CovariantI) - variances + (** + Each local universe is either in the [univs] map or is Invariant. + + If [univs] is empty all universes are Invariant and there is nothing more to do, + so we stop by raising [TrivialVariance]. The [soft] check comes before that. + *) + type variances = { + orig_array : (Level.t * Variance.t option) array; + univs : (mode * inferred) LMap.t; + } + + let to_variance = function + | IrrelevantI -> Irrelevant + | CovariantI -> Covariant + + let to_variance_opt o = Option.cata to_variance Invariant o + + let infer_level_eq u variances = + match LMap.find_opt u variances.univs with + | None -> variances + | Some (Check, expected) -> + let expected = to_variance expected in + raise (BadVariance (u, expected, Invariant)) + | Some (Infer, _) -> + let univs = LMap.remove u variances.univs in + if LMap.is_empty univs then raise TrivialVariance; + {variances with univs} + + let infer_level_leq u variances = + (* can only set Irrelevant -> Covariant so no TrivialVariance *) + let univs = + LMap.update u (function + | None -> None + | Some (_,CovariantI) as x -> x + | Some (Infer,IrrelevantI) -> Some (Infer,CovariantI) + | Some (Check,IrrelevantI) -> + raise (BadVariance (u, Irrelevant, Covariant))) + variances.univs + in + if univs == variances.univs then variances else {variances with univs} + + let start us = + let univs = Array.fold_left (fun univs (u,variance) -> + match variance with + | None -> LMap.add u (Infer,IrrelevantI) univs + | Some Invariant -> univs + | Some Covariant -> LMap.add u (Check,CovariantI) univs + | Some Irrelevant -> LMap.add u (Check,IrrelevantI) univs) + LMap.empty us + in + if LMap.is_empty univs then raise TrivialVariance; + {univs; orig_array=us} + + let finish variances = + Array.map + (fun (u,_check) -> to_variance_opt (Option.map snd (LMap.find_opt u variances.univs))) + variances.orig_array + +end +open Inf let infer_generic_instance_eq variances u = Array.fold_left (fun variances u -> infer_level_eq u variances) @@ -204,11 +256,7 @@ let infer_arity_constructor is_arity env variances arcn = open Entries let infer_inductive_core env univs entries = - if Array.is_empty univs then raise TrivialVariance; - let variances = - Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances) - LMap.empty univs - in + let variances = Inf.start univs in let variances = List.fold_left (fun variances entry -> let variances = infer_arity_constructor true env variances entry.mind_entry_arity @@ -218,12 +266,11 @@ let infer_inductive_core env univs entries = variances entries in - Array.map (fun u -> match LMap.find u variances with - | exception Not_found -> Invariant - | IrrelevantI -> Irrelevant - | CovariantI -> Covariant) - univs + Inf.finish variances let infer_inductive ~env_params univs entries = try infer_inductive_core env_params univs entries - with TrivialVariance -> Array.make (Array.length univs) Invariant + with + | TrivialVariance -> Array.make (Array.length univs) Invariant + | BadVariance (lev, expected, actual) -> + Type_errors.error_bad_variance env_params ~lev ~expected ~actual diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli index db5539a0ff..99d8f0c98d 100644 --- a/kernel/inferCumulativity.mli +++ b/kernel/inferCumulativity.mli @@ -12,8 +12,8 @@ val infer_inductive : env_params:Environ.env (** Environment containing the polymorphic universes and the parameters. *) - -> Univ.Level.t array - (** Universes whose cumulativity we want to infer. *) + -> (Univ.Level.t * Univ.Variance.t option) array + (** Universes whose cumulativity we want to infer or check. *) -> Entries.one_inductive_entry list (** The inductive block data we want to infer cumulativity for. NB: we ignore the template bool and the names, only the terms diff --git a/kernel/names.ml b/kernel/names.ml index 592b5e65f7..be65faf234 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -44,6 +44,10 @@ struct | None -> true | Some _ -> false + let is_valid_ident_part s = match Unicode.ident_refutation ("x"^s) with + | None -> true + | Some _ -> false + let of_bytes s = let s = Bytes.to_string s in check_valid s; @@ -447,6 +451,22 @@ module KNset = KNmap.Set (** {6 Kernel pairs } *) +module type EqType = +sig + type t + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int +end + +module type QNameS = +sig + type t + module CanOrd : EqType with type t = t + module UserOrd : EqType with type t = t + module SyntacticOrd : EqType with type t = t +end + (** For constant and inductive names, we use a kernel name couple (kn1,kn2) where kn1 corresponds to the name used at toplevel (i.e. what the user see) and kn2 corresponds to the canonical kernel name i.e. in the environment @@ -529,6 +549,7 @@ module KerPair = struct end module SyntacticOrd = struct + type t = kernel_pair let compare x y = match x, y with | Same knx, Same kny -> KerName.compare knx kny | Dual (knux,kncx), Dual (knuy,kncy) -> @@ -599,100 +620,147 @@ module Mindmap = HMap.Make(MutInd.CanOrd) module Mindset = Mindmap.Set module Mindmap_env = HMap.Make(MutInd.UserOrd) +module Ind = +struct + (** Designation of a (particular) inductive type. *) + type t = MutInd.t (* the name of the inductive type *) + * int (* the position of this inductive type + within the block of mutually-recursive inductive types. + BEWARE: indexing starts from 0. *) + let modpath (mind, _) = MutInd.modpath mind + + module CanOrd = + struct + type nonrec t = t + let equal (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.CanOrd.equal m1 m2 + let compare (m1, i1) (m2, i2) = + let c = Int.compare i1 i2 in + if Int.equal c 0 then MutInd.CanOrd.compare m1 m2 else c + let hash (m, i) = + Hashset.Combine.combine (MutInd.CanOrd.hash m) (Int.hash i) + end + + module UserOrd = + struct + type nonrec t = t + let equal (m1, i1) (m2, i2) = + Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2 + let compare (m1, i1) (m2, i2) = + let c = Int.compare i1 i2 in + if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c + let hash (m, i) = + Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i) + end + + module SyntacticOrd = + struct + type nonrec t = t + let equal (m1, i1) (m2, i2) = + Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2 + + let compare (m1, i1) (m2, i2) = + let c = Int.compare i1 i2 in + if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c + + let hash (m, i) = + Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i) + end + +end + +module Construct = +struct + (** Designation of a (particular) constructor of a (particular) inductive type. *) + type t = Ind.t (* designates the inductive type *) + * int (* the index of the constructor + BEWARE: indexing starts from 1. *) + + let modpath (ind, _) = Ind.modpath ind + + module CanOrd = + struct + type nonrec t = t + let equal (ind1, j1) (ind2, j2) = Int.equal j1 j2 && Ind.CanOrd.equal ind1 ind2 + let compare (ind1, j1) (ind2, j2) = + let c = Int.compare j1 j2 in + if Int.equal c 0 then Ind.CanOrd.compare ind1 ind2 else c + let hash (ind, i) = + Hashset.Combine.combine (Ind.CanOrd.hash ind) (Int.hash i) + end + + module UserOrd = + struct + type nonrec t = t + let equal (ind1, j1) (ind2, j2) = + Int.equal j1 j2 && Ind.UserOrd.equal ind1 ind2 + let compare (ind1, j1) (ind2, j2) = + let c = Int.compare j1 j2 in + if Int.equal c 0 then Ind.UserOrd.compare ind1 ind2 else c + let hash (ind, i) = + Hashset.Combine.combine (Ind.UserOrd.hash ind) (Int.hash i) + end + + module SyntacticOrd = + struct + type nonrec t = t + let equal (ind1, j1) (ind2, j2) = + Int.equal j1 j2 && Ind.SyntacticOrd.equal ind1 ind2 + let compare (ind1, j1) (ind2, j2) = + let c = Int.compare j1 j2 in + if Int.equal c 0 then Ind.SyntacticOrd.compare ind1 ind2 else c + let hash (ind, i) = + Hashset.Combine.combine (Ind.SyntacticOrd.hash ind) (Int.hash i) + end + +end + (** Designation of a (particular) inductive type. *) -type inductive = MutInd.t (* the name of the inductive type *) - * int (* the position of this inductive type - within the block of mutually-recursive inductive types. - BEWARE: indexing starts from 0. *) +type inductive = Ind.t (** Designation of a (particular) constructor of a (particular) inductive type. *) -type constructor = inductive (* designates the inductive type *) - * int (* the index of the constructor - BEWARE: indexing starts from 1. *) +type constructor = Construct.t -let ind_modpath (mind,_) = MutInd.modpath mind -let constr_modpath (ind,_) = ind_modpath ind +let ind_modpath = Ind.modpath +let constr_modpath = Construct.modpath let ith_mutual_inductive (mind, _) i = (mind, i) let ith_constructor_of_inductive ind i = (ind, i) let inductive_of_constructor (ind, _i) = ind let index_of_constructor (_ind, i) = i -let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 -let eq_user_ind (m1, i1) (m2, i2) = - Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2 -let eq_syntactic_ind (m1, i1) (m2, i2) = - Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2 - -let ind_ord (m1, i1) (m2, i2) = - let c = Int.compare i1 i2 in - if Int.equal c 0 then MutInd.CanOrd.compare m1 m2 else c -let ind_user_ord (m1, i1) (m2, i2) = - let c = Int.compare i1 i2 in - if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c -let ind_syntactic_ord (m1, i1) (m2, i2) = - let c = Int.compare i1 i2 in - if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c - -let ind_hash (m, i) = - Hashset.Combine.combine (MutInd.hash m) (Int.hash i) -let ind_user_hash (m, i) = - Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i) -let ind_syntactic_hash (m, i) = - Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i) - -let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 -let eq_user_constructor (ind1, j1) (ind2, j2) = - Int.equal j1 j2 && eq_user_ind ind1 ind2 -let eq_syntactic_constructor (ind1, j1) (ind2, j2) = - Int.equal j1 j2 && eq_syntactic_ind ind1 ind2 - -let constructor_ord (ind1, j1) (ind2, j2) = - let c = Int.compare j1 j2 in - if Int.equal c 0 then ind_ord ind1 ind2 else c -let constructor_user_ord (ind1, j1) (ind2, j2) = - let c = Int.compare j1 j2 in - if Int.equal c 0 then ind_user_ord ind1 ind2 else c -let constructor_syntactic_ord (ind1, j1) (ind2, j2) = - let c = Int.compare j1 j2 in - if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c - -let constructor_hash (ind, i) = - Hashset.Combine.combine (ind_hash ind) (Int.hash i) -let constructor_user_hash (ind, i) = - Hashset.Combine.combine (ind_user_hash ind) (Int.hash i) -let constructor_syntactic_hash (ind, i) = - Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i) - -module InductiveOrdered = struct - type t = inductive - let compare = ind_ord -end +let eq_ind = Ind.CanOrd.equal +let eq_user_ind = Ind.UserOrd.equal +let eq_syntactic_ind = Ind.SyntacticOrd.equal -module InductiveOrdered_env = struct - type t = inductive - let compare = ind_user_ord -end +let ind_ord = Ind.CanOrd.compare +let ind_user_ord = Ind.UserOrd.compare +let ind_syntactic_ord = Ind.SyntacticOrd.compare -module Indset = Set.Make(InductiveOrdered) -module Indset_env = Set.Make(InductiveOrdered_env) -module Indmap = Map.Make(InductiveOrdered) -module Indmap_env = Map.Make(InductiveOrdered_env) +let ind_hash = Ind.CanOrd.hash +let ind_user_hash = Ind.UserOrd.hash +let ind_syntactic_hash = Ind.SyntacticOrd.hash -module ConstructorOrdered = struct - type t = constructor - let compare = constructor_ord -end +let eq_constructor = Construct.CanOrd.equal +let eq_user_constructor = Construct.UserOrd.equal +let eq_syntactic_constructor = Construct.SyntacticOrd.equal -module ConstructorOrdered_env = struct - type t = constructor - let compare = constructor_user_ord -end +let constructor_ord = Construct.CanOrd.compare +let constructor_user_ord = Construct.UserOrd.compare +let constructor_syntactic_ord = Construct.SyntacticOrd.compare + +let constructor_hash = Construct.CanOrd.hash +let constructor_user_hash = Construct.UserOrd.hash +let constructor_syntactic_hash = Construct.SyntacticOrd.hash + +module Indset = Set.Make(Ind.CanOrd) +module Indset_env = Set.Make(Ind.UserOrd) +module Indmap = Map.Make(Ind.CanOrd) +module Indmap_env = Map.Make(Ind.UserOrd) -module Constrset = Set.Make(ConstructorOrdered) -module Constrset_env = Set.Make(ConstructorOrdered_env) -module Constrmap = Map.Make(ConstructorOrdered) -module Constrmap_env = Map.Make(ConstructorOrdered_env) +module Constrset = Set.Make(Construct.CanOrd) +module Constrset_env = Set.Make(Construct.UserOrd) +module Constrmap = Map.Make(Construct.CanOrd) +module Constrmap_env = Map.Make(Construct.UserOrd) (** {6 Hash-consing of name objects } *) @@ -786,6 +854,8 @@ struct Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) module SyntacticOrd = struct + type nonrec t = t + let compare a b = let c = ind_syntactic_ord a.proj_ind b.proj_ind in if c == 0 then Int.compare a.proj_arg b.proj_arg @@ -798,6 +868,8 @@ struct Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) end module CanOrd = struct + type nonrec t = t + let compare a b = let c = ind_ord a.proj_ind b.proj_ind in if c == 0 then Int.compare a.proj_arg b.proj_arg @@ -810,6 +882,8 @@ struct Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind) end module UserOrd = struct + type nonrec t = t + let compare a b = let c = ind_user_ord a.proj_ind b.proj_ind in if c == 0 then Int.compare a.proj_arg b.proj_arg @@ -876,6 +950,7 @@ struct let hash (c, b) = (if b then 0 else 1) + Repr.hash c module SyntacticOrd = struct + type nonrec t = t let compare (c, b) (c', b') = if b = b' then Repr.SyntacticOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = @@ -883,12 +958,21 @@ struct let hash (c, b) = (if b then 0 else 1) + Repr.SyntacticOrd.hash c end module CanOrd = struct + type nonrec t = t let compare (c, b) (c', b') = if b = b' then Repr.CanOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = x == x' || b = b' && Repr.CanOrd.equal c c' let hash (c, b) = (if b then 0 else 1) + Repr.CanOrd.hash c end + module UserOrd = struct + type nonrec t = t + let compare (c, b) (c', b') = + if b = b' then Repr.UserOrd.compare c c' else -1 + let equal (c, b as x) (c', b' as x') = + x == x' || b = b' && Repr.UserOrd.equal c c' + let hash (c, b) = (if b then 0 else 1) + Repr.UserOrd.hash c + end module Self_Hashcons = struct @@ -982,31 +1066,36 @@ module GlobRef = struct (* By default, [global_reference] are ordered on their canonical part *) - module Ordered = struct - open Constant.CanOrd + module CanOrd = struct type t = GlobRefInternal.t let compare gr1 gr2 = - GlobRefInternal.global_ord_gen compare ind_ord constructor_ord gr1 gr2 - let equal gr1 gr2 = GlobRefInternal.global_eq_gen equal eq_ind eq_constructor gr1 gr2 - let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr + GlobRefInternal.global_ord_gen Constant.CanOrd.compare Ind.CanOrd.compare Construct.CanOrd.compare gr1 gr2 + let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.CanOrd.equal Ind.CanOrd.equal Construct.CanOrd.equal gr1 gr2 + let hash gr = GlobRefInternal.global_hash_gen Constant.CanOrd.hash Ind.CanOrd.hash Construct.CanOrd.hash gr end - module Ordered_env = struct - open Constant.UserOrd + module UserOrd = struct type t = GlobRefInternal.t let compare gr1 gr2 = - GlobRefInternal.global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2 - let equal gr1 gr2 = - GlobRefInternal.global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2 - let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr + GlobRefInternal.global_ord_gen Constant.UserOrd.compare Ind.UserOrd.compare Construct.UserOrd.compare gr1 gr2 + let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.UserOrd.equal Ind.UserOrd.equal Construct.UserOrd.equal gr1 gr2 + let hash gr = GlobRefInternal.global_hash_gen Constant.UserOrd.hash Ind.UserOrd.hash Construct.UserOrd.hash gr end - module Map = HMap.Make(Ordered) + module SyntacticOrd = struct + type t = GlobRefInternal.t + let compare gr1 gr2 = + GlobRefInternal.global_ord_gen Constant.SyntacticOrd.compare Ind.SyntacticOrd.compare Construct.SyntacticOrd.compare gr1 gr2 + let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.SyntacticOrd.equal Ind.SyntacticOrd.equal Construct.SyntacticOrd.equal gr1 gr2 + let hash gr = GlobRefInternal.global_hash_gen Constant.SyntacticOrd.hash Ind.SyntacticOrd.hash Construct.SyntacticOrd.hash gr + end + + module Map = HMap.Make(CanOrd) module Set = Map.Set (* Alternative sets and maps indexed by the user part of the kernel names *) - module Map_env = HMap.Make(Ordered_env) + module Map_env = HMap.Make(UserOrd) module Set_env = Map_env.Set end @@ -1026,3 +1115,5 @@ let eq_egr e1 e2 = match e1, e2 with type lident = Id.t CAst.t type lname = Name.t CAst.t type lstring = string CAst.t + +let lident_eq = CAst.eq Id.equal diff --git a/kernel/names.mli b/kernel/names.mli index ea137ad1f4..747299bb12 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -44,6 +44,9 @@ sig val is_valid : string -> bool (** Check that a string may be converted to an identifier. *) + val is_valid_ident_part : string -> bool + (** Check that a string is a valid part of an identifier *) + val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. @@ -307,6 +310,60 @@ module KNset : CSig.SetS with type elt = KerName.t module KNpred : Predicate.S with type elt = KerName.t module KNmap : Map.ExtS with type key = KerName.t and module Set := KNset +(** {6 Signature for quotiented names} *) + +module type EqType = +sig + type t + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int +end + +module type QNameS = +sig + type t + (** A type of reference that implements an implicit quotient by containing + two different names. The first one is the user name, i.e. what the user + sees when printing. The second one is the canonical name, which is the + actual absolute name of the reference. + + This mechanism is fundamentally tied to the module system of Coq. Functor + application and module inclusion are the typical ways to introduce names + where the canonical and user components differ. In particular, the two + components should be undistinguishable from the point of view of typing, + i.e. from a "kernel" ground. This aliasing only makes sense inside an + environment, but at this point this notion is not even defined so, this + dual name trick is fragile. One has to ensure many invariants when + creating such names, but the kernel is quite lenient when it comes to + checking that these invariants hold. (Read: there are soundness bugs + lurking in the module system.) + + One could enforce the invariants by splitting the names and storing that + information in the environment instead, but unfortunately, this wreaks + havoc in the upper layers. The latter are infamously not stable by + syntactic equality, in particular they might observe the difference + between canonical and user names if not packed together. + + For this reason, it is discouraged to use the canonical-accessing API + in the upper layers, notably the [CanOrd] module below. Instead, one + should use their quotiented versions defined in the [Environ] module. + Eventually all uses to [CanOrd] outside of the kernel should be removed. + + CAVEAT: name sets and maps are still exposing a canonical-accessing API + surreptitiously. *) + + module CanOrd : EqType with type t = t + (** Equality functions over the canonical name. Their use should be + restricted to the kernel. *) + + module UserOrd : EqType with type t = t + (** Equality functions over the user name. *) + + module SyntacticOrd : EqType with type t = t + (** Equality functions using both names, for low-level uses. *) +end + (** {6 Constant Names } *) module Constant: @@ -340,28 +397,12 @@ sig (** Comparisons *) - module CanOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - - module UserOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end + include QNameS with type t := t - val equal : t -> t -> bool + val equal : t -> t -> bool [@@ocaml.deprecated "Use QConstant.equal"] (** Default comparison, alias for [CanOrd.equal] *) - val hash : t -> int + val hash : t -> int [@@ocaml.deprecated "Use QConstant.hash"] (** Hashing function *) val change_label : t -> Label.t -> t @@ -430,28 +471,12 @@ sig (** Comparisons *) - module CanOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - - module UserOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end + include QNameS with type t := t - val equal : t -> t -> bool - (** Default comparison, alias for [CanOrd.equal] *) + val equal : t -> t -> bool [@@ocaml.deprecated "Use QMutInd.equal"] + (** Default comparison, alias for [CanOrd.equal] *) - val hash : t -> int + val hash : t -> int [@@ocaml.deprecated "Use QMutInd.hash"] (** Displaying *) @@ -473,16 +498,35 @@ module Mindset : CSig.SetS with type elt = MutInd.t module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset module Mindmap_env : CMap.ExtS with type key = MutInd.t -(** Designation of a (particular) inductive type. *) -type inductive = MutInd.t (* the name of the inductive type *) - * int (* the position of this inductive type - within the block of mutually-recursive inductive types. - BEWARE: indexing starts from 0. *) +module Ind : +sig + (** Designation of a (particular) inductive type. *) + type t = MutInd.t (* the name of the inductive type *) + * int (* the position of this inductive type + within the block of mutually-recursive inductive types. + BEWARE: indexing starts from 0. *) + val modpath : t -> ModPath.t + + include QNameS with type t := t + +end + +type inductive = Ind.t + +module Construct : +sig + (** Designation of a (particular) constructor of a (particular) inductive type. *) + type t = Ind.t (* designates the inductive type *) + * int (* the index of the constructor + BEWARE: indexing starts from 1. *) + + val modpath : t -> ModPath.t + + include QNameS with type t := t -(** Designation of a (particular) constructor of a (particular) inductive type. *) -type constructor = inductive (* designates the inductive type *) - * int (* the index of the constructor - BEWARE: indexing starts from 1. *) +end + +type constructor = Construct.t module Indset : CSet.S with type elt = inductive module Constrset : CSet.S with type elt = constructor @@ -494,30 +538,51 @@ module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env val ind_modpath : inductive -> ModPath.t +[@@ocaml.deprecated "Use the Ind module"] + val constr_modpath : constructor -> ModPath.t +[@@ocaml.deprecated "Use the Construct module"] val ith_mutual_inductive : inductive -> int -> inductive val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool +[@@ocaml.deprecated "Use the Ind module"] val eq_user_ind : inductive -> inductive -> bool +[@@ocaml.deprecated "Use the Ind module"] val eq_syntactic_ind : inductive -> inductive -> bool +[@@ocaml.deprecated "Use the Ind module"] val ind_ord : inductive -> inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val ind_hash : inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val ind_user_ord : inductive -> inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val ind_user_hash : inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val ind_syntactic_ord : inductive -> inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val ind_syntactic_hash : inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val eq_constructor : constructor -> constructor -> bool +[@@ocaml.deprecated "Use the Construct module"] val eq_user_constructor : constructor -> constructor -> bool +[@@ocaml.deprecated "Use the Construct module"] val eq_syntactic_constructor : constructor -> constructor -> bool +[@@ocaml.deprecated "Use the Construct module"] val constructor_ord : constructor -> constructor -> int +[@@ocaml.deprecated "Use the Construct module"] val constructor_hash : constructor -> int +[@@ocaml.deprecated "Use the Construct module"] val constructor_user_ord : constructor -> constructor -> int +[@@ocaml.deprecated "Use the Construct module"] val constructor_user_hash : constructor -> int +[@@ocaml.deprecated "Use the Construct module"] val constructor_syntactic_ord : constructor -> constructor -> int +[@@ocaml.deprecated "Use the Construct module"] val constructor_syntactic_hash : constructor -> int +[@@ocaml.deprecated "Use the Construct module"] (** {6 Hash-consing } *) @@ -558,21 +623,7 @@ module Projection : sig val make : inductive -> proj_npars:int -> proj_arg:int -> Label.t -> t - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - module CanOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - module UserOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end + include QNameS with type t := t val constant : t -> Constant.t (** Don't use this if you don't have to. *) @@ -583,9 +634,9 @@ module Projection : sig val arg : t -> int val label : t -> Label.t - val equal : t -> t -> bool - val hash : t -> int - val compare : t -> t -> int + val equal : t -> t -> bool [@@ocaml.deprecated "Use QProjection.equal"] + val hash : t -> int [@@ocaml.deprecated "Use QProjection.hash"] + val compare : t -> t -> int [@@ocaml.deprecated "Use QProjection.compare"] val map : (MutInd.t -> MutInd.t) -> t -> t val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t @@ -602,16 +653,7 @@ module Projection : sig val make : Repr.t -> bool -> t val repr : t -> Repr.t - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - module CanOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end + include QNameS with type t := t val constant : t -> Constant.t val mind : t -> MutInd.t @@ -623,14 +665,18 @@ module Projection : sig val unfold : t -> t val equal : t -> t -> bool + [@@ocaml.deprecated "Use QProjection.equal"] val hash : t -> int + [@@ocaml.deprecated "Use QProjection.hash"] val hcons : t -> t (** Hashconsing of projections. *) val repr_equal : t -> t -> bool + [@@ocaml.deprecated "Use an explicit projection of Repr"] (** Ignoring the unfolding boolean. *) val compare : t -> t -> int + [@@ocaml.deprecated "Use QProjection.compare"] val map : (MutInd.t -> MutInd.t) -> t -> t val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t @@ -656,19 +702,7 @@ module GlobRef : sig val equal : t -> t -> bool - module Ordered : sig - type nonrec t = t - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - - module Ordered_env : sig - type nonrec t = t - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end + include QNameS with type t := t module Set_env : CSig.SetS with type elt = t module Map_env : Map.ExtS @@ -693,3 +727,5 @@ val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool type lident = Id.t CAst.t type lname = Name.t CAst.t type lstring = string CAst.t + +val lident_eq : lident -> lident -> bool diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ae070e6f8e..09db29d222 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -65,11 +65,11 @@ type gname = let eq_gname gn1 gn2 = match gn1, gn2 with | Gind (s1, ind1), Gind (s2, ind2) -> - String.equal s1 s2 && eq_ind ind1 ind2 + String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2 | Gconstant (s1, c1), Gconstant (s2, c2) -> - String.equal s1 s2 && Constant.equal c1 c2 + String.equal s1 s2 && Constant.CanOrd.equal c1 c2 | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) -> - String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2 + String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2 && Int.equal i1 i2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -96,9 +96,9 @@ open Hashset.Combine let gname_hash gn = match gn with | Gind (s, ind) -> - combinesmall 1 (combine (String.hash s) (ind_hash ind)) + combinesmall 1 (combine (String.hash s) (Ind.CanOrd.hash ind)) | Gconstant (s, c) -> - combinesmall 2 (combine (String.hash s) (Constant.hash c)) + combinesmall 2 (combine (String.hash s) (Constant.CanOrd.hash c)) | Gcase (l, i) -> combinesmall 3 (combine (Option.hash Label.hash l) (Int.hash i)) | Gpred (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i)) | Gfixtype (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i)) @@ -107,7 +107,7 @@ let gname_hash gn = match gn with | Ginternal s -> combinesmall 8 (String.hash s) | Grel i -> combinesmall 9 (Int.hash i) | Gnamed id -> combinesmall 10 (Id.hash id) -| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (ind_hash p) i)) +| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (Ind.CanOrd.hash p) i)) let case_ctr = ref (-1) @@ -148,13 +148,13 @@ let eq_symbol sy1 sy2 = | SymbValue v1, SymbValue v2 -> (=) v1 v2 (** FIXME: how is this even valid? *) | SymbSort s1, SymbSort s2 -> Sorts.equal s1 s2 | SymbName n1, SymbName n2 -> Name.equal n1 n2 - | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2 + | SymbConst kn1, SymbConst kn2 -> Constant.CanOrd.equal kn1 kn2 | SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2 - | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2 + | SymbInd ind1, SymbInd ind2 -> Ind.CanOrd.equal ind1 ind2 | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2 | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 - | SymbProj (i1, k1), SymbProj (i2, k2) -> eq_ind i1 i2 && Int.equal k1 k2 + | SymbProj (i1, k1), SymbProj (i2, k2) -> Ind.CanOrd.equal i1 i2 && Int.equal k1 k2 | _, _ -> false let hash_symbol symb = @@ -162,13 +162,13 @@ let hash_symbol symb = | SymbValue v -> combinesmall 1 (Hashtbl.hash v) (** FIXME *) | SymbSort s -> combinesmall 2 (Sorts.hash s) | SymbName name -> combinesmall 3 (Name.hash name) - | SymbConst c -> combinesmall 4 (Constant.hash c) + | SymbConst c -> combinesmall 4 (Constant.CanOrd.hash c) | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw) - | SymbInd ind -> combinesmall 6 (ind_hash ind) + | SymbInd ind -> combinesmall 6 (Ind.CanOrd.hash ind) | SymbMeta m -> combinesmall 7 m | SymbEvar evk -> combinesmall 8 (Evar.hash evk) | SymbLevel l -> combinesmall 9 (Univ.Level.hash l) - | SymbProj (i, k) -> combinesmall 10 (combine (ind_hash i) k) + | SymbProj (i, k) -> combinesmall 10 (combine (Ind.CanOrd.hash i) k) module HashedTypeSymbol = struct type t = symbol @@ -438,7 +438,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 | MLconstruct (pf1, ind1, tag1, args1), MLconstruct (pf2, ind2, tag2, args2) -> String.equal pf1 pf2 && - eq_ind ind1 ind2 && + Ind.CanOrd.equal ind1 ind2 && Int.equal tag1 tag2 && Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2 | MLint i1, MLint i2 -> @@ -457,7 +457,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2 | MLisaccu (s1, ind1, ml1), MLisaccu (s2, ind2, ml2) -> - String.equal s1 s2 && eq_ind ind1 ind2 && + String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2 && eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ | @@ -527,7 +527,7 @@ let rec hash_mllambda gn n env t = combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br) | MLconstruct (pf, ind, tag, args) -> let hpf = String.hash pf in - let hcs = ind_hash ind in + let hcs = Ind.CanOrd.hash ind in let htag = Int.hash tag in combinesmall 10 (hash_mllambda_array gn n env (combine3 hpf hcs htag) args) | MLint i -> @@ -545,7 +545,7 @@ let rec hash_mllambda gn n env t = | MLarray arr -> combinesmall 15 (hash_mllambda_array gn n env 1 arr) | MLisaccu (s, ind, c) -> - combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c))) + combinesmall 16 (combine (String.hash s) (combine (Ind.CanOrd.hash ind) (hash_mllambda gn n env c))) | MLfloat f -> combinesmall 17 (Float64.hash f) @@ -689,7 +689,7 @@ let eq_global g1 g2 = eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2 | Gopen s1, Gopen s2 -> String.equal s1 s2 | Gtype (ind1, arr1), Gtype (ind2, arr2) -> - eq_ind ind1 ind2 && + Ind.CanOrd.equal ind1 ind2 && Array.equal (fun (tag1,ar1) (tag2,ar2) -> Int.equal tag1 tag2 && Int.equal ar1 ar2) arr1 arr2 | Gcomment s1, Gcomment s2 -> String.equal s1 s2 | _, _ -> false @@ -720,7 +720,7 @@ let hash_global g = let hash_aux acc (tag,ar) = combine3 acc (Int.hash tag) (Int.hash ar) in - combinesmall 6 (combine (ind_hash ind) (Array.fold_left hash_aux 0 arr)) + combinesmall 6 (combine (Ind.CanOrd.hash ind) (Array.fold_left hash_aux 0 arr)) | Gcomment s -> combinesmall 7 (String.hash s) let global_stack = ref ([] : global list) @@ -1933,7 +1933,7 @@ and compile_named env sigma univ auxdefs id = | LocalAssum _ -> Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs -let compile_constant env sigma prefix ~interactive con cb = +let compile_constant env sigma con cb = let no_univs = 0 = Univ.AUContext.size (Declareops.constant_polymorphic_context cb) in begin match cb.const_body with | Def t -> @@ -1942,10 +1942,6 @@ let compile_constant env sigma prefix ~interactive con cb = if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); let is_lazy = is_lazy t in let code = if is_lazy then mk_lazy code else code in - let name = - if interactive then LinkedInteractive prefix - else Linked prefix - in let l = Constant.label con in let auxdefs,code = if no_univs then compile_with_fv env sigma None [] (Some l) code @@ -1959,7 +1955,7 @@ let compile_constant env sigma prefix ~interactive con cb = optimize_stk (Glet(Gconstant ("", con),code)::auxdefs) in if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code"); - code, name + code | _ -> let i = push_symbol (SymbConst con) in let args = @@ -1969,9 +1965,7 @@ let compile_constant env sigma prefix ~interactive con cb = (* let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const) *) - [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)], - if interactive then LinkedInteractive prefix - else Linked prefix + [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)] end module StringOrd = struct type t = string let compare = String.compare end @@ -1984,12 +1978,9 @@ let is_loaded_native_file s = StringSet.mem s !loaded_native_files let register_native_file s = loaded_native_files := StringSet.add s !loaded_native_files -let is_code_loaded ~interactive name = +let is_code_loaded name = match !name with | NotLinked -> false - | LinkedInteractive s -> - if (interactive && is_loaded_native_file s) then true - else (name := NotLinked; false) | Linked s -> if is_loaded_native_file s then true else (name := NotLinked; false) @@ -2049,8 +2040,11 @@ let compile_mind mb mind stack = in Array.fold_left_i f stack mb.mind_packets -type code_location_update = - link_info ref * link_info +type code_location_update = { + upd_info : link_info ref; + upd_prefix : string; +} + type code_location_updates = code_location_update Mindmap_env.t * code_location_update Cmap_env.t @@ -2058,35 +2052,34 @@ type linkable_code = global list * code_location_updates let empty_updates = Mindmap_env.empty, Cmap_env.empty -let compile_mind_deps env prefix ~interactive +let compile_mind_deps env prefix (comp_stack, (mind_updates, const_updates) as init) mind = let mib,nameref = lookup_mind_key mind env in - if is_code_loaded ~interactive nameref + if is_code_loaded nameref || Mindmap_env.mem mind mind_updates then init else let comp_stack = compile_mind mib mind comp_stack in - let name = - if interactive then LinkedInteractive prefix - else Linked prefix - in - let upd = (nameref, name) in + let upd = { + upd_info = nameref; + upd_prefix = prefix; + } in let mind_updates = Mindmap_env.add mind upd mind_updates in (comp_stack, (mind_updates, const_updates)) (* This function compiles all necessary dependencies of t, and generates code in reverse order, as well as linking information updates *) -let compile_deps env sigma prefix ~interactive init t = +let compile_deps env sigma prefix init t = let rec aux env lvl init t = match kind t with - | Ind ((mind,_),_u) -> compile_mind_deps env prefix ~interactive init mind + | Ind ((mind,_),_u) -> compile_mind_deps env prefix init mind | Const c -> let c,_u = get_alias env c in let cb,(nameref,_) = lookup_constant_key c env in let (_, (_, const_updates)) = init in - if is_code_loaded ~interactive nameref + if is_code_loaded nameref || (Cmap_env.mem c const_updates) then init else @@ -2096,19 +2089,21 @@ let compile_deps env sigma prefix ~interactive init t = aux env lvl init (Mod_subst.force_constr t) | _ -> init in - let code, name = - compile_constant env sigma prefix ~interactive c cb - in + let code = compile_constant env sigma c cb in + let upd = { + upd_info = nameref; + upd_prefix = prefix; + } in let comp_stack = code@comp_stack in - let const_updates = Cmap_env.add c (nameref, name) const_updates in + let const_updates = Cmap_env.add c upd const_updates in comp_stack, (mind_updates, const_updates) - | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix ~interactive init mind + | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix init mind | Proj (p,c) -> - let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in + let init = compile_mind_deps env prefix init (Projection.mind p) in aux env lvl init c | Case (ci, _p, _iv, _c, _ac) -> let mind = fst ci.ci_ind in - let init = compile_mind_deps env prefix ~interactive init mind in + let init = compile_mind_deps env prefix init mind in fold_constr_with_binders succ (aux env) lvl init t | Var id -> let open Context.Named.Declaration in @@ -2130,11 +2125,8 @@ let compile_deps env sigma prefix ~interactive init t = in aux env 0 init t -let compile_constant_field env prefix con acc cb = - let (gl, _) = - compile_constant ~interactive:false env empty_evars prefix - con cb - in +let compile_constant_field env _prefix con acc cb = + let gl = compile_constant env empty_evars con cb in gl@acc let compile_mind_field mp l acc mb = @@ -2152,11 +2144,11 @@ let mk_conv_code env sigma prefix t1 t2 = clear_global_tbl (); let gl, (mind_updates, const_updates) = let init = ([], empty_updates) in - compile_deps env sigma prefix ~interactive:true init t1 + compile_deps env sigma prefix init t1 in let gl, (mind_updates, const_updates) = let init = (gl, (mind_updates, const_updates)) in - compile_deps env sigma prefix ~interactive:true init t2 + compile_deps env sigma prefix init t2 in let code1 = lambda_of_constr env sigma t1 in let code2 = lambda_of_constr env sigma t2 in @@ -2179,7 +2171,7 @@ let mk_norm_code env sigma prefix t = clear_global_tbl (); let gl, (mind_updates, const_updates) = let init = ([], empty_updates) in - compile_deps env sigma prefix ~interactive:true init t + compile_deps env sigma prefix init t in let code = lambda_of_constr env sigma t in let (gl,code) = compile_with_fv env sigma None gl None code in @@ -2192,13 +2184,12 @@ let mk_norm_code env sigma prefix t = [|MLglobal (Ginternal "()")|])) in header::gl, (mind_updates, const_updates) -let mk_library_header dir = - let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in - [Glet(Ginternal "symbols_tbl", - MLapp (MLglobal (Ginternal "get_library_native_symbols"), - [|MLglobal (Ginternal libname)|]))] +let mk_library_header (symbols : Nativevalues.symbols) = + let symbols = Format.sprintf "(str_decode \"%s\")" (str_encode symbols) in + [Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))] -let update_location (r,v) = r := v +let update_location r = + r.upd_info := Linked r.upd_prefix let update_locations (ind_updates,const_updates) = Mindmap_env.iter (fun _ -> update_location) ind_updates; diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 71317d188b..aab6e1d4a0 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -50,7 +50,6 @@ val get_proj : symbols -> int -> inductive * int val get_symbols : unit -> symbols -type code_location_update type code_location_updates type linkable_code = global list * code_location_updates @@ -69,7 +68,7 @@ val compile_mind_field : ModPath.t -> Label.t -> val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code val mk_norm_code : env -> evars -> string -> constr -> linkable_code -val mk_library_header : DirPath.t -> global list +val mk_library_header : Nativevalues.symbols -> global list val mod_uid_of_dirpath : DirPath.t -> string diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index fc6afb79d4..d77ee759c6 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -80,17 +80,17 @@ and conv_atom env pb lvl a1 a2 cu = | Arel i1, Arel i2 -> if Int.equal i1 i2 then cu else raise NotConvertible | Aind (ind1,u1), Aind (ind2,u2) -> - if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu + if Ind.CanOrd.equal ind1 ind2 then convert_instances ~flex:false u1 u2 cu else raise NotConvertible | Aconstant (c1,u1), Aconstant (c2,u2) -> - if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu + if Constant.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu else raise NotConvertible | Asort s1, Asort s2 -> sort_cmp_universes env pb s1 s2 cu | Avar id1, Avar id2 -> if Id.equal id1 id2 then cu else raise NotConvertible | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) -> - if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible; + if not (Ind.CanOrd.equal a1.asw_ind a2.asw_ind) then raise NotConvertible; let cu = conv_accu env CONV lvl ac1 ac2 cu in let tbl = a1.asw_reloc in let len = Array.length tbl in @@ -124,7 +124,7 @@ and conv_atom env pb lvl a1 a2 cu = let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) -> - if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible + if not (Ind.CanOrd.equal ind1 ind2 && Int.equal i1 i2) then raise NotConvertible else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ @@ -161,7 +161,7 @@ let native_conv_gen pb sigma env univs t1 t2 = let fn = compile ml_filename code ~profile:false in if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); let t0 = Sys.time () in - call_linker env ~fatal:true ~prefix fn (Some upds); + call_linker ~fatal:true ~prefix fn (Some upds); let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Feedback.msg_debug (Pp.str time_info); diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 99090f0147..18f16f427d 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -111,14 +111,12 @@ let get_mind_prefix env mind = match !name with | NotLinked -> "" | Linked s -> s - | LinkedInteractive s -> s let get_const_prefix env c = let _,(nameref,_) = lookup_constant_key c env in match !nameref with | NotLinked -> "" | Linked s -> s - | LinkedInteractive s -> s (* A generic map function *) @@ -433,8 +431,8 @@ module Cache = module ConstrHash = struct type t = constructor - let equal = eq_constructor - let hash = constructor_hash + let equal = Construct.CanOrd.equal + let hash = Construct.CanOrd.hash end module ConstrTable = Hashtbl.Make(ConstrHash) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 494282d4e1..1e1085d5ff 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -25,7 +25,8 @@ let open_header = ["Nativevalues"; let open_header = List.map mk_open open_header (* Directory where compiled files are stored *) -let output_dir = ref ".coq-native" +let dft_output_dir = ".coq-native" +let output_dir = ref dft_output_dir (* Extension of generated ml files, stored for debugging purposes *) let source_ext = ".native" @@ -92,9 +93,14 @@ let error_native_compiler_failed e = CErrors.user_err msg let call_compiler ?profile:(profile=false) ml_filename = - let load_path = !get_load_paths () in - let load_path = List.map (fun dn -> dn / !output_dir) load_path in - let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (get_include_dirs () @ load_path)) in + (* The below path is computed from Require statements, by uniquizing + the paths, see [Library.get_used_load_paths] This is in general + hacky and we should do a bit better once we move loadpath to its + own library *) + let require_load_path = !get_load_paths () in + (* We assume that installed files always go in .coq-native for now *) + let install_load_path = List.map (fun dn -> dn / dft_output_dir) require_load_path in + let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (get_include_dirs () @ install_load_path)) in let f = Filename.chop_extension ml_filename in let link_filename = f ^ ".cmo" in let link_filename = Dynlink.adapt_filename link_filename in @@ -139,8 +145,10 @@ let compile fn code ~profile:profile = if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn; r -let compile_library dir code fn = - let header = mk_library_header dir in +type native_library = Nativecode.global list * Nativevalues.symbols + +let compile_library (code, symb) fn = + let header = mk_library_header symb in let fn = fn ^ source_ext in let basename = Filename.basename fn in let dirname = Filename.dirname fn in @@ -154,19 +162,9 @@ let compile_library dir code fn = let _ = call_compiler fn in if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn -let native_symbols = ref Names.DPmap.empty - -let get_library_native_symbols dir = - try Names.DPmap.find dir !native_symbols - with Not_found -> - CErrors.user_err ~hdr:"get_library_native_symbols" - Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++ - (str "This use case is not supported, but disabling the native compiler may help.")) - (* call_linker links dynamically the code for constants in environment or a *) (* conversion test. *) -let call_linker ?(fatal=true) env ~prefix f upds = - native_symbols := env.Environ.native_symbols; +let call_linker ?(fatal=true) ~prefix f upds = rt1 := dummy_value (); rt2 := dummy_value (); if not (Sys.file_exists f) then @@ -185,6 +183,11 @@ let call_linker ?(fatal=true) env ~prefix f upds = else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); match upds with Some upds -> update_locations upds | _ -> () -let link_library env ~prefix ~dirname ~basename = - let f = dirname / !output_dir / basename in - call_linker env ~fatal:false ~prefix f None +let link_library ~prefix ~dirname ~basename = + (* We try both [output_dir] and [.coq-native], unfortunately from + [Require] we don't know if we are loading a library in the build + dir or in the installed layout *) + let install_location = dirname / dft_output_dir / basename in + let build_location = dirname / !output_dir / basename in + let f = if Sys.file_exists build_location then build_location else install_location in + call_linker ~fatal:false ~prefix f None diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 29b4d20197..0c0fe3acc9 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -27,27 +27,24 @@ val get_ml_filename : unit -> string * string whether are in byte mode or not; file is expected to be .ml file *) val compile : string -> global list -> profile:bool -> string -(** [compile_library lib code file] is similar to [compile file code] +type native_library = Nativecode.global list * Nativevalues.symbols + +(** [compile_library (code, _) file] is similar to [compile file code] but will perform some extra tweaks to handle [code] as a Coq lib. *) -val compile_library : Names.DirPath.t -> global list -> string -> unit +val compile_library : native_library -> string -> unit val call_linker : ?fatal:bool - -> Environ.env -> prefix:string -> string -> code_location_updates option -> unit val link_library - : Environ.env - -> prefix:string + : prefix:string -> dirname:string -> basename:string -> unit val rt1 : Nativevalues.t ref val rt2 : Nativevalues.t ref - -val get_library_native_symbols : Names.DirPath.t -> Nativevalues.symbols -(** Strictly for usage by code produced by native compute. *) diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 05c98e4b87..bd6241ae67 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -36,13 +36,13 @@ type annot_sw = { (* We compare only what is relevant for generation of ml code *) let eq_annot_sw asw1 asw2 = - eq_ind asw1.asw_ind asw2.asw_ind && + Ind.CanOrd.equal asw1.asw_ind asw2.asw_ind && String.equal asw1.asw_prefix asw2.asw_prefix open Hashset.Combine let hash_annot_sw asw = - combine (ind_hash asw.asw_ind) (String.hash asw.asw_prefix) + combine (Ind.CanOrd.hash asw.asw_ind) (String.hash asw.asw_prefix) type sort_annot = string * int diff --git a/kernel/primred.ml b/kernel/primred.ml index f158cfacea..f0b4d6d362 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -12,11 +12,11 @@ type _ action_kind = type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn let check_same_types typ c1 c2 = - if not (Constant.equal c1 c2) + if not (Constant.CanOrd.equal c1 c2) then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2)) let check_same_inds ind i1 i2 = - if not (eq_ind i1 i2) + if not (Ind.CanOrd.equal i1 i2) then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2)) let add_retroknowledge retro action = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 96bf370342..cf40263f61 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -280,11 +280,12 @@ let convert_constructors ctor nargs u1 u2 (s, check) = convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances ctor nargs u1 u2 s, check -let conv_table_key infos k1 k2 cuniv = +let conv_table_key infos ~nargs k1 k2 cuniv = if k1 == k2 then cuniv else match k1, k2 with - | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' -> + | ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' -> if Univ.Instance.equal u u' then cuniv + else if Int.equal nargs 1 && is_array_type (info_env infos) cst then cuniv else let flex = evaluable_constant cst (info_env infos) && RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst) @@ -301,9 +302,14 @@ let unfold_ref_with_args infos tab fl v = | Primitive op when check_native_args op v -> let c = match fl with ConstKey c -> c | _ -> assert false in let rargs, a, nargs, v = get_native_args1 op c v in - Some (whd_stack infos tab a (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v))) + Some (a, (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v))) | Undef _ | OpaqueDef _ | Primitive _ -> None +let same_args_size sk1 sk2 = + let n = CClosure.stack_args_size sk1 in + if Int.equal n (CClosure.stack_args_size sk2) then n + else raise NotConvertible + type conv_tab = { cnv_inf : clos_infos; lft_tab : clos_tab; @@ -408,26 +414,30 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try - let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in + let nargs = same_args_size v1 v2 in + let cuniv = conv_table_key infos.cnv_inf ~nargs fl1 fl2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible | Univ.UniverseInconsistency _ -> - (* else the oracle tells which constant is to be expanded *) - let oracle = CClosure.oracle_of_infos infos.cnv_inf in - let (app1,app2) = - let aux appr1 lft1 fl1 tab1 v1 appr2 lft2 fl2 tab2 v2 = - match unfold_ref_with_args infos.cnv_inf tab1 fl1 v1 with - | Some t1 -> ((lft1, t1), appr2) - | None -> match unfold_ref_with_args infos.cnv_inf tab2 fl2 v2 with - | Some t2 -> (appr1, (lft2, t2)) - | None -> raise NotConvertible - in - if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then - aux appr1 lft1 fl1 infos.lft_tab v1 appr2 lft2 fl2 infos.rgt_tab v2 - else - let (app2,app1) = aux appr2 lft2 fl2 infos.rgt_tab v2 appr1 lft1 fl1 infos.lft_tab v1 in - (app1,app2) - in - eqappr cv_pb l2r infos app1 app2 cuniv) + let r1 = unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 in + let r2 = unfold_ref_with_args infos.cnv_inf infos.rgt_tab fl2 v2 in + match r1, r2 with + | None, None -> raise NotConvertible + | Some t1, Some t2 -> + (* else the oracle tells which constant is to be expanded *) + let oracle = CClosure.oracle_of_infos infos.cnv_inf in + if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then + eqappr cv_pb l2r infos (lft1, t1) appr2 cuniv + else + eqappr cv_pb l2r infos appr1 (lft2, t2) cuniv + | Some (t1, v1), None -> + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in + let t1 = whd_stack (infos_with_reds infos.cnv_inf all) infos.lft_tab t1 v1 in + eqappr cv_pb l2r infos (lft1, t1) appr2 cuniv + | None, Some (t2, v2) -> + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in + let t2 = whd_stack (infos_with_reds infos.cnv_inf all) infos.rgt_tab t2 v2 in + eqappr cv_pb l2r infos appr1 (lft2, t2) cuniv + ) | (FProj (p1,c1), FProj (p2, c2)) -> (* Projections: prefer unfolding to first-order unification, @@ -441,7 +451,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some s2 -> eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> - if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) + if Projection.Repr.CanOrd.equal (Projection.repr p1) (Projection.repr p2) && compare_stack_shape v1 v2 then let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in @@ -568,43 +578,37 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd (ind1,u1 as pind1), FInd (ind2,u2 as pind2)) -> - if eq_ind ind1 ind2 then + if Ind.CanOrd.equal ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in - let nargs = CClosure.stack_args_size v1 in - if not (Int.equal nargs (CClosure.stack_args_size v2)) - then raise NotConvertible - else - match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with - | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - | exception MustExpand -> - let env = info_env infos.cnv_inf in - let hd1 = eta_expand_ind env pind1 in - let hd2 = eta_expand_ind env pind2 in - eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv + let nargs = same_args_size v1 v2 in + match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with + | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + | exception MustExpand -> + let env = info_env infos.cnv_inf in + let hd1 = eta_expand_ind env pind1 in + let hd2 = eta_expand_ind env pind2 in + eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv else raise NotConvertible | (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) -> - if Int.equal j1 j2 && eq_ind ind1 ind2 then + if Int.equal j1 j2 && Ind.CanOrd.equal ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in - let nargs = CClosure.stack_args_size v1 in - if not (Int.equal nargs (CClosure.stack_args_size v2)) - then raise NotConvertible - else - match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with - | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - | exception MustExpand -> - let env = info_env infos.cnv_inf in - let hd1 = eta_expand_constructor env pctor1 in - let hd2 = eta_expand_constructor env pctor2 in - eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv + let nargs = same_args_size v1 v2 in + match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with + | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + | exception MustExpand -> + let env = info_env infos.cnv_inf in + let hd1 = eta_expand_constructor env pctor1 in + let hd2 = eta_expand_constructor env pctor2 in + eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv else raise NotConvertible (* Eta expansion of records *) @@ -669,7 +673,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) -> - (if not (eq_ind ci1.ci_ind ci2.ci_ind) then raise NotConvertible); + (if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible); let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in let ccnv = ccnv CONV l2r infos el1 el2 in let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in @@ -704,14 +708,14 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> - if not (Projection.Repr.equal c1 c2) then + if not (Projection.Repr.CanOrd.equal c1 c2) then raise NotConvertible else cu1 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> let cu2 = f fx1 fx2 cu1 in cmp_rec a1 a2 cu2 | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) -> - if not (eq_ind ci1.ci_ind ci2.ci_ind) then + if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible; let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2 diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 3dee3d2b2f..a35f94e3ce 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -121,7 +121,6 @@ type compiled_library = { comp_univs : Univ.ContextSet.t; comp_deps : library_info array; comp_enga : engagement; - comp_natsymbs : Nativevalues.symbols } type reimport = compiled_library * Univ.ContextSet.t * vodigest @@ -248,6 +247,15 @@ let set_native_compiler b senv = let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env } +(* Temporary sets custom typing flags *) +let with_typing_flags ?typing_flags senv ~f = + match typing_flags with + | None -> f senv + | Some typing_flags -> + let orig_typing_flags = Environ.typing_flags senv.env in + let res, senv = f (set_typing_flags typing_flags senv) in + res, set_typing_flags orig_typing_flags senv + (** Check that the engagement [c] expected by a library matches the current (initial) one *) let check_engagement env expected_impredicative_set = @@ -672,7 +680,7 @@ let inline_side_effects env body side_eff = let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in let side_eff = List.rev side_eff in (** Most recent side-effects first in side_eff *) - if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs) + if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs, 0) else (** Second step: compute the lifts and substitutions to apply *) let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in @@ -726,10 +734,10 @@ let inline_side_effects env body side_eff = else mkLetIn (na, b, ty, accu) in let body = List.fold_right fold_arg args body in - (body, ctx, sigs) + (body, ctx, sigs, len - 1) let inline_private_constants env ((body, ctx), side_eff) = - let body, ctx',_ = inline_side_effects env body side_eff in + let body, ctx', _, _ = inline_side_effects env body side_eff in let ctx' = Univ.ContextSet.union ctx ctx' in (body, ctx') @@ -881,11 +889,11 @@ let add_constant l decl senv = match decl with | OpaqueEntry ce -> let handle env body eff = - let body, uctx, signatures = inline_side_effects env body eff in + let body, uctx, signatures, skip = inline_side_effects env body eff in let trusted = check_signatures senv signatures in let trusted, uctx = match trusted with | None -> 0, uctx - | Some univs -> List.length signatures, Univ.ContextSet.union univs uctx + | Some univs -> skip, Univ.ContextSet.union univs uctx in body, uctx, trusted in @@ -929,6 +937,9 @@ let add_constant l decl senv = in kn, senv +let add_constant ?typing_flags l decl senv = + with_typing_flags ?typing_flags senv ~f:(add_constant l decl) + let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment = let kn = Constant.make2 senv.modpath l in let cb = @@ -984,6 +995,9 @@ let add_mind l mie senv = let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in kn, add_checked_mind kn mib senv +let add_mind ?typing_flags l mie senv = + with_typing_flags ?typing_flags senv ~f:(add_mind l mie) + (** Insertion of module types *) let add_modtype l params_mte inl senv = @@ -1139,7 +1153,6 @@ let end_module l restype senv = let mb, cst = build_module_body params restype senv in let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in - let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in let newenv = set_engagement_opt newenv senv.engagement in let newenv = Environ.set_universes (Environ.universes senv.env) newenv in let senv' = propagate_loads { senv with env = newenv } in @@ -1166,7 +1179,6 @@ let end_modtype l senv = let () = check_empty_context senv in let mbids = List.rev_map fst params in let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in - let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in let newenv = set_engagement_opt newenv senv.engagement in let newenv = Environ.set_universes (Environ.universes senv.env) newenv in let senv' = propagate_loads {senv with env=newenv} in @@ -1229,8 +1241,6 @@ let module_of_library lib = lib.comp_mod let univs_of_library lib = lib.comp_univs -type native_library = Nativecode.global list - (** FIXME: MS: remove?*) let current_modpath senv = senv.modpath let current_dirpath senv = Names.ModPath.dp (current_modpath senv) @@ -1272,9 +1282,8 @@ let export ?except ~output_native_objects senv dir = comp_univs = senv.univ; comp_deps = Array.of_list (DPmap.bindings senv.required); comp_enga = Environ.engagement senv.env; - comp_natsymbs = symbols } - in - mp, lib, ast + } in + mp, lib, (ast, symbols) (* cst are the constraints that were computed by the vi2vo step and hence are * not part of the [lib.comp_univs] field (but morally should be) *) @@ -1294,7 +1303,6 @@ let import lib cst vodigest senv = let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in Modops.add_linked_module mb linkinfo env in - let env = Environ.add_native_symbols lib.comp_name lib.comp_natsymbs env in let sections = Option.map (Section.map_custom (fun custom -> {custom with rev_reimport = (lib,cst,vodigest) :: custom.rev_reimport})) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index b601279e87..287274e39a 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -93,6 +93,7 @@ val export_private_constants : (** returns the main constant *) val add_constant : + ?typing_flags:Declarations.typing_flags -> Label.t -> global_declaration -> Constant.t safe_transformer (** Similar to add_constant but also returns a certificate *) @@ -102,6 +103,7 @@ val add_private_constant : (** Adding an inductive type *) val add_mind : + ?typing_flags:Declarations.typing_flags -> Label.t -> Entries.mutual_inductive_entry -> MutInd.t safe_transformer @@ -191,8 +193,6 @@ val current_dirpath : safe_environment -> DirPath.t type compiled_library -type native_library = Nativecode.global list - val module_of_library : compiled_library -> Declarations.module_body val univs_of_library : compiled_library -> Univ.ContextSet.t @@ -201,7 +201,7 @@ val start_library : DirPath.t -> ModPath.t safe_transformer val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> safe_environment -> DirPath.t -> - ModPath.t * compiled_library * native_library + ModPath.t * compiled_library * Nativelib.native_library (* Constraints are non empty iff the file is a vi2vo *) val import : compiled_library -> Univ.ContextSet.t -> vodigest -> diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 76a1c190be..1a4c786e43 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -182,7 +182,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 begin let kn2' = kn_of_delta reso2 kn2 in if KerName.equal kn2 kn2' || - MutInd.equal (mind_of_delta_kn reso1 kn1) + MutInd.CanOrd.equal (mind_of_delta_kn reso1 kn1) (subst_mind subst2 (MutInd.make kn2 kn2')) then () else error NotEqualInductiveAliases diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index ae5c4b6880..bcb7aa88ca 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -69,6 +69,7 @@ type ('constr, 'types) ptype_error = | DisallowedSProp | BadRelevance | BadInvert + | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t } type type_error = (constr, types) ptype_error @@ -163,6 +164,9 @@ let error_bad_relevance env = let error_bad_invert env = raise (TypeError (env, BadInvert)) +let error_bad_variance env ~lev ~expected ~actual = + raise (TypeError (env, BadVariance {lev;expected;actual})) + let map_pguard_error f = function | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c) @@ -207,3 +211,4 @@ let map_ptype_error f = function | DisallowedSProp -> DisallowedSProp | BadRelevance -> BadRelevance | BadInvert -> BadInvert +| BadVariance u -> BadVariance u diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index b1f7eb8a34..bcdcab9db7 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -70,6 +70,7 @@ type ('constr, 'types) ptype_error = | DisallowedSProp | BadRelevance | BadInvert + | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t } type type_error = (constr, types) ptype_error @@ -146,5 +147,7 @@ val error_bad_relevance : env -> 'a val error_bad_invert : env -> 'a +val error_bad_variance : env -> lev:Level.t -> expected:Variance.t -> actual:Variance.t -> 'a + val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error diff --git a/kernel/typeops.ml b/kernel/typeops.ml index f86c12e1f1..85e24f87b7 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -413,7 +413,7 @@ let type_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_ind (Projection.inductive p) ind); + assert(Ind.CanOrd.equal (Projection.inductive p) ind); let ty = Vars.subst_instance_constr u pty in substl (c :: CList.rev args) ty diff --git a/kernel/vars.ml b/kernel/vars.ml index f7e28b0cfe..a446fa413c 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -348,5 +348,8 @@ let universes_of_constr c = | Array (u,_,_,_) -> let s = LSet.fold LSet.add (Instance.levels u) s in Constr.fold aux s c + | Case (_,_,CaseInvert {univs;args=_},_,_) -> + let s = LSet.fold LSet.add (Instance.levels univs) s in + Constr.fold aux s c | _ -> Constr.fold aux s c in aux LSet.empty c diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 948195797e..1432fb9310 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -95,7 +95,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = (* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with | Aind ((mi,_i) as ind1) , Aind ind2 -> - if eq_ind ind1 ind2 && compare_stack stk1 stk2 then + if Ind.CanOrd.equal ind1 ind2 && compare_stack stk1 stk2 then let ulen = Univ.AUContext.size (Environ.mind_context env mi) in if ulen = 0 then conv_stack env k stk1 stk2 cu @@ -141,7 +141,7 @@ and conv_stack env k stk1 stk2 cu = conv_stack env k stk1 stk2 !rcu else raise NotConvertible | Zproj p1 :: stk1, Zproj p2 :: stk2 -> - if Projection.Repr.equal p1 p2 then conv_stack env k stk1 stk2 cu + if Projection.Repr.CanOrd.equal p1 p2 then conv_stack env k stk1 stk2 cu else raise NotConvertible | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _ | Zproj _ :: _, _ -> raise NotConvertible diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml index c156a21c86..4977aec00a 100644 --- a/kernel/vmbytecodes.ml +++ b/kernel/vmbytecodes.ml @@ -56,13 +56,12 @@ type instruction = | Kfield of int | Ksetfield of int | Kstop - | Ksequence of bytecodes * bytecodes + | Ksequence of bytecodes | Kproj of Projection.Repr.t | Kensurestackcapacity of int | Kbranch of Label.t (* jump to label *) - | Kprim of CPrimitives.t * pconstant option + | Kprim of CPrimitives.t * pconstant | Kcamlprim of CPrimitives.t * Label.t - | Kareint of int and bytecodes = instruction list @@ -146,21 +145,19 @@ let rec pp_instr i = | Kensurestackcapacity size -> str "growstack " ++ int size | Kprim (op, id) -> str (CPrimitives.to_string op) ++ str " " ++ - (match id with Some (id,_u) -> Constant.print id | None -> str "") + (Constant.print (fst id)) | Kcamlprim (op, lbl) -> str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++ pp_lbl lbl - | Kareint n -> str "areint " ++ int n - and pp_bytecodes c = match c with | [] -> str "" | Klabel lbl :: c -> str "L" ++ int lbl ++ str ":" ++ fnl () ++ pp_bytecodes c - | Ksequence (l1, l2) :: c -> - pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c + | Ksequence l :: c -> + pp_bytecodes l ++ pp_bytecodes c | i :: c -> pp_instr i ++ fnl () ++ pp_bytecodes c diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli index b703058fb7..003a77ab78 100644 --- a/kernel/vmbytecodes.mli +++ b/kernel/vmbytecodes.mli @@ -54,14 +54,13 @@ type instruction = | Kfield of int (** accu = accu[n] *) | Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *) | Kstop - | Ksequence of bytecodes * bytecodes + | Ksequence of bytecodes | Kproj of Projection.Repr.t | Kensurestackcapacity of int | Kbranch of Label.t (** jump to label, is it needed ? *) - | Kprim of CPrimitives.t * pconstant option + | Kprim of CPrimitives.t * pconstant | Kcamlprim of CPrimitives.t * Label.t - | Kareint of int and bytecodes = instruction list diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 16a0f42664..70c92fd8f0 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -315,12 +315,10 @@ let pos_evar evk r = (* non-terminating instruction (branch, raise, return, appterm) *) (* in front of it. *) -let discard_dead_code cont = cont -(*function - [] -> [] +let rec discard_dead_code = function + | [] -> [] | (Klabel _ | Krestart ) :: _ as cont -> cont | _ :: cont -> discard_dead_code cont -*) (* Return a label to the beginning of the given continuation. *) (* If the sequence starts with a branch, use the target of that branch *) @@ -581,7 +579,7 @@ let rec compile_lam env cenv lam sz cont = let cont_fun = ensure_stack_capacity (compile_lam env r_fun body arity) [Kreturn arity] in - fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; + fun_code := Ksequence (add_grab arity lbl_fun cont_fun) :: !fun_code; let fv = fv r_fun in compile_fv cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) @@ -604,7 +602,7 @@ let rec compile_lam env cenv lam sz cont = in let lbl,fcode = label_code fcode in lbl_types.(i) <- lbl; - fun_code := [Ksequence(fcode,!fun_code)] + fun_code := Ksequence fcode :: !fun_code done; (* Compiling bodies *) for i = 0 to ndef - 1 do @@ -617,7 +615,7 @@ let rec compile_lam env cenv lam sz cont = let lbl = Label.create () in lbl_bodies.(i) <- lbl; let fcode = add_grabrec rec_args.(i) arity lbl cont1 in - fun_code := [Ksequence(fcode,!fun_code)] + fun_code := Ksequence fcode :: !fun_code done; let fv = !rfv in compile_fv cenv fv.fv_rev sz @@ -637,7 +635,7 @@ let rec compile_lam env cenv lam sz cont = in let lbl,fcode = label_code fcode in lbl_types.(i) <- lbl; - fun_code := [Ksequence(fcode,!fun_code)] + fun_code := Ksequence fcode :: !fun_code done; (* Compiling bodies *) for i = 0 to ndef - 1 do @@ -652,25 +650,13 @@ let rec compile_lam env cenv lam sz cont = in let cont = ensure_stack_capacity comp arity in lbl_bodies.(i) <- lbl; - fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)]; + fun_code := Ksequence (add_grab (arity+1) lbl cont) :: !fun_code; done; let fv = !rfv in set_max_stack_size (sz + fv.size + ndef + 2); compile_fv cenv fv.fv_rev sz (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) - | Lif(t, bt, bf) -> - let branch, cont = make_branch cont in - let lbl_true = Label.create() in - let lbl_false = Label.create() in - compile_lam env cenv t sz - (Kswitch([|lbl_true;lbl_false|],[||]) :: - Klabel lbl_false :: - compile_lam env cenv bf sz - (branch :: - Klabel lbl_true :: - compile_lam env cenv bt sz cont)) - | Lcase(ci,rtbl,t,a,branches) -> let ind = ci.ci_ind in let mib = lookup_mind (fst ind) env in @@ -688,7 +674,7 @@ let rec compile_lam env cenv lam sz cont = ensure_stack_capacity (compile_lam env cenv t sz) [Kpop sz; Kstop] in let lbl_typ,fcode = label_code fcode in - fun_code := [Ksequence(fcode,!fun_code)]; + fun_code := Ksequence fcode :: !fun_code; (* Compilation of the branches *) let lbl_sw = Label.create () in let sz_b,branch,is_tailcall = @@ -700,6 +686,7 @@ let rec compile_lam env cenv lam sz cont = | _ -> assert false in + let cont = discard_dead_code cont in let c = ref cont in (* Perform the extra match if needed (too many block constructors) *) if neblock <> 0 then begin @@ -770,7 +757,7 @@ let rec compile_lam env cenv lam sz cont = let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in comp_args (compile_lam env) cenv args sz cont - | Lprim (Some (kn,u), op, args) when is_caml_prim op -> + | Lprim ((kn,u), op, args) when is_caml_prim op -> let arity = CPrimitives.arity op in let nparams = CPrimitives.nparams op in let nargs = arity - nparams in @@ -788,7 +775,7 @@ let rec compile_lam env cenv lam sz cont = if Int.equal nparams 0 then cont else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont) in - fun_code := [Ksequence(default, !fun_code)]; + fun_code := Ksequence default :: !fun_code; comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont) | Lprim (kn, op, args) -> @@ -878,7 +865,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = ensure_stack_capacity (compile_lam env r_fun body full_arity) [Kreturn full_arity] in - fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; + fun_code := Ksequence (add_grab full_arity lbl_fun cont_fun) :: !fun_code; let fv = fv r_fun in let init_code = ensure_stack_capacity (compile_fv cenv fv.fv_rev 0) diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index ec8601edc9..c1d8fcb855 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -36,9 +36,9 @@ let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_annot _, _ -> false | Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2 | Reloc_const _, _ -> false -| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2 +| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.CanOrd.equal c1 c2 | Reloc_getglobal _, _ -> false -| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2 +| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.CanOrd.equal p1 p2 | Reloc_proj_name _, _ -> false | Reloc_caml_prim p1, Reloc_caml_prim p2 -> CPrimitives.equal p1 p2 | Reloc_caml_prim _, _ -> false @@ -48,8 +48,8 @@ let hash_reloc_info r = match r with | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw) | Reloc_const c -> combinesmall 2 (hash_structured_constant c) - | Reloc_getglobal c -> combinesmall 3 (Constant.hash c) - | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p) + | Reloc_getglobal c -> combinesmall 3 (Constant.CanOrd.hash c) + | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.CanOrd.hash p) | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p) module RelocTable = Hashtbl.Make(struct @@ -208,14 +208,6 @@ let slot_for_caml_prim env op = (* Emission of one instruction *) -let nocheck_prim_op = function - | Int63add -> opADDINT63 - | Int63sub -> opSUBINT63 - | Int63lt -> opLTINT63 - | Int63le -> opLEINT63 - | _ -> assert false - - let check_prim_op = function | Int63head0 -> opCHECKHEAD0INT63 | Int63tail0 -> opCHECKTAIL0INT63 @@ -259,11 +251,20 @@ let check_prim_op = function | Float64ldshiftexp -> opCHECKLDSHIFTEXP | Float64next_up -> opCHECKNEXTUPFLOAT | Float64next_down -> opCHECKNEXTDOWNFLOAT - | Arraymake -> opISINT_CAML_CALL2 - | Arrayget -> opISARRAY_INT_CAML_CALL2 - | Arrayset -> opISARRAY_INT_CAML_CALL3 + | Arraymake -> opCHECKCAMLCALL2_1 + | Arrayget -> opCHECKCAMLCALL2 + | Arrayset -> opCHECKCAMLCALL3_1 | Arraydefault | Arraycopy | Arraylength -> - opISARRAY_CAML_CALL1 + opCHECKCAMLCALL1 + +let inplace_prim_op = function + | Float64next_up | Float64next_down -> true + | _ -> false + +let check_prim_op_inplace = function + | Float64next_up -> opCHECKNEXTUPFLOATINPLACE + | Float64next_down -> opCHECKNEXTDOWNFLOATINPLACE + | _ -> assert false let emit_instr env = function | Klabel lbl -> define_label env lbl @@ -354,10 +355,7 @@ let emit_instr env = function | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size | Kbranch lbl -> out env opBRANCH; out_label env lbl - | Kprim (op,None) -> - out env (nocheck_prim_op op) - - | Kprim(op,Some (q,_u)) -> + | Kprim (op, (q,_u)) -> out env (check_prim_op op); slot_for_getglobal env q @@ -366,13 +364,8 @@ let emit_instr env = function out_label env lbl; slot_for_caml_prim env op - | Kareint 1 -> out env opISINT - | Kareint 2 -> out env opAREINT2; - | Kstop -> out env opSTOP - | Kareint _ -> assert false - (* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *) let rec emit env insns remaining = match insns with @@ -406,8 +399,14 @@ let rec emit env insns remaining = match insns with emit env c remaining | Kpop n :: Kjump :: c -> out env opRETURN; out_int env n; emit env c remaining - | Ksequence(c1,c2)::c -> - emit env c1 (c2::c::remaining) + | Ksequence c1 :: c -> + emit env c1 (c :: remaining) + | Kprim (op1, (q1, _)) :: Kprim (op2, (q2, _)) :: c when inplace_prim_op op2 -> + out env (check_prim_op op1); + slot_for_getglobal env q1; + out env (check_prim_op_inplace op2); + slot_for_getglobal env q2; + emit env c remaining (* Default case *) | instr :: c -> emit_instr env instr; emit env c remaining diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml index 332a331a7a..9cca204e8c 100644 --- a/kernel/vmlambda.ml +++ b/kernel/vmlambda.ml @@ -19,10 +19,8 @@ type lambda = | Llet of Name.t Context.binder_annot * lambda * lambda | Lapp of lambda * lambda array | Lconst of pconstant - | Lprim of pconstant option * CPrimitives.t * lambda array - (* No check if None *) + | Lprim of pconstant * CPrimitives.t * lambda array | Lcase of case_info * reloc_table * lambda * lambda * lam_branches - | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl | Lcofix of int * fix_decl | Lint of int @@ -112,10 +110,6 @@ let rec pp_lam lam = pp_names ids ++ str " => " ++ pp_lam c) (Array.to_list branches.nonconstant_branches))) ++ cut() ++ str "end") - | Lif (t, bt, bf) -> - v 0 (str "(if " ++ pp_lam t ++ - cut () ++ str "then " ++ pp_lam bt ++ - cut() ++ str "else " ++ pp_lam bf ++ str ")") | Lfix((t,i),(lna,tl,bl)) -> let fixl = Array.mapi (fun i id -> (id,t.(i),tl.(i),bl.(i))) lna in hov 1 @@ -148,16 +142,11 @@ let rec pp_lam lam = | Lval _ -> str "values" | Lsort s -> pp_sort s | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i - | Lprim(Some (kn,_u),_op,args) -> + | Lprim ((kn,_u),_op,args) -> hov 1 (str "(PRIM " ++ pr_con kn ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ str")") - | Lprim(None,op,args) -> - hov 1 - (str "(PRIM_NC " ++ str (CPrimitives.to_string op) ++ spc() ++ - prlist_with_sep spc pp_lam (Array.to_list args) ++ - str")") | Lproj(p,arg) -> hov 1 (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg @@ -237,11 +226,6 @@ let map_lam_with_binders g f n lam = in if t == t' && a == a' && branches == branches' then lam else Lcase(ci,rtbl,t',a',branches') - | Lif(t,bt,bf) -> - let t' = f n t in - let bt' = f n bt in - let bf' = f n bf in - if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf') | Lfix(init,(ids,ltypes,lbodies)) -> let ltypes' = Array.Smart.map (f n) ltypes in let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in @@ -312,28 +296,6 @@ let can_subst lam = | Lval _ | Lsort _ | Lind _ -> true | _ -> false - -let can_merge_if bt bf = - match bt, bf with - | Llam(_idst,_), Llam(_idsf,_) -> true - | _ -> false - -let merge_if t bt bf = - let (idst,bodyt) = decompose_Llam bt in - let (idsf,bodyf) = decompose_Llam bf in - let nt = Array.length idst in - let nf = Array.length idsf in - let common,idst,idsf = - if nt = nf then idst, [||], [||] - else - if nt < nf then idst,[||], Array.sub idsf nt (nf - nt) - else idsf, Array.sub idst nf (nt - nf), [||] in - Llam(common, - Lif(lam_lift (Array.length common) t, - mkLlam idst bodyt, - mkLlam idsf bodyf)) - - let rec simplify subst lam = match lam with | Lrel(id,i) -> lam_subst_rel lam id i subst @@ -352,14 +314,6 @@ let rec simplify subst lam = | lam' -> lam' end - | Lif(t,bt,bf) -> - let t' = simplify subst t in - let bt' = simplify subst bt in - let bf' = simplify subst bf in - if can_merge_if bt' bf' then merge_if t' bt' bf' - else - if t == t' && bt == bt' && bf == bf' then lam - else Lif(t',bt',bf') | _ -> map_lam_with_binders liftn simplify subst lam and simplify_app substf f substa args = @@ -442,9 +396,6 @@ let rec occurrence k kind lam = in Array.iter on_b branches.nonconstant_branches; !r - | Lif (t, bt, bf) -> - let kind = occurrence k kind t in - kind && occurrence k kind bt && occurrence k kind bf | Lfix(_,(ids,ltypes,lbodies)) | Lcofix(_,(ids,ltypes,lbodies)) -> let kind = occurrence_args k kind ltypes in @@ -566,7 +517,7 @@ let rec get_alias env kn = (* Compilation of primitive *) let prim kn p args = - Lprim(Some kn, p, args) + Lprim (kn, p, args) let expand_prim kn op arity = (* primitives are always Relevant *) diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli index bd11c2667f..ad5f81638f 100644 --- a/kernel/vmlambda.mli +++ b/kernel/vmlambda.mli @@ -12,10 +12,8 @@ type lambda = | Llet of Name.t Context.binder_annot * lambda * lambda | Lapp of lambda * lambda array | Lconst of pconstant - | Lprim of pconstant option * CPrimitives.t * lambda array - (* No check if None *) + | Lprim of pconstant * CPrimitives.t * lambda array | Lcase of case_info * reloc_table * lambda * lambda * lam_branches - | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl | Lcofix of int * fix_decl | Lint of int diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml index 9d80dc578b..ae0fa38571 100644 --- a/kernel/vmsymtable.ml +++ b/kernel/vmsymtable.ml @@ -85,7 +85,7 @@ module AnnotTable = Hashtbl.Make (struct let hash = hash_annot_switch end) -module ProjNameTable = Hashtbl.Make (Projection.Repr) +module ProjNameTable = Hashtbl.Make (Projection.Repr.CanOrd) let str_cst_tbl : int SConstTable.t = SConstTable.create 31 diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 2068133b10..9944458d6b 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -96,7 +96,7 @@ let hash_structured_values (v : structured_values) = let eq_structured_constant c1 c2 = match c1, c2 with | Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2 | Const_sort _, _ -> false -| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 +| Const_ind i1, Const_ind i2 -> Ind.CanOrd.equal i1 i2 | Const_ind _, _ -> false | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 | Const_b0 _, _ -> false @@ -113,7 +113,7 @@ let hash_structured_constant c = let open Hashset.Combine in match c with | Const_sort s -> combinesmall 1 (Sorts.hash s) - | Const_ind i -> combinesmall 2 (ind_hash i) + | Const_ind i -> combinesmall 2 (Ind.CanOrd.hash i) | Const_b0 t -> combinesmall 3 (Int.hash t) | Const_univ_level l -> combinesmall 4 (Univ.Level.hash l) | Const_val v -> combinesmall 5 (hash_structured_values v) @@ -250,7 +250,7 @@ type id_key = | EvarKey of Evar.t let eq_id_key (k1 : id_key) (k2 : id_key) = match k1, k2 with -| ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 +| ConstKey c1, ConstKey c2 -> Constant.CanOrd.equal c1 c2 | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey n1, RelKey n2 -> Int.equal n1 n2 | EvarKey evk1, EvarKey evk2 -> Evar.equal evk1 evk2 @@ -381,7 +381,15 @@ let rec whd_accu a stk = CErrors.anomaly Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") -external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" +[@@@warning "-37"] +type vm_closure_kind = + | VCfun (** closure, or fixpoint applied past the recursive argument *) + | VCfix (** unapplied fixpoint *) + | VCfix_partial (** partially applied fixpoint, but not sufficiently for recursion *) + | VCaccu (** accumulator *) +[@@@warning "+37"] + +external kind_of_closure : Obj.t -> vm_closure_kind = "coq_kind_of_closure" external is_accumulate : tcode -> bool = "coq_is_accumulate_code" external int_tcode : tcode -> int -> int = "coq_int_tcode" external accumulate : unit -> tcode = "accumulate_code" @@ -400,12 +408,11 @@ let whd_val (v: values) = else if Int.equal tag Obj.closure_tag && is_accumulate (fun_code o) then whd_accu o [] else if Int.equal tag Obj.closure_tag || Int.equal tag Obj.infix_tag then - (match kind_of_closure o with - | 0 -> Vfun(Obj.obj o) - | 1 -> Vfix(Obj.obj o, None) - | 2 -> Vfix(Obj.obj (Obj.field o 2), Some (Obj.obj o)) - | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) + match kind_of_closure o with + | VCfun -> Vfun (Obj.obj o) + | VCfix -> Vfix (Obj.obj o, None) + | VCfix_partial -> Vfix (Obj.obj (Obj.field o 2), Some (Obj.obj o)) + | VCaccu -> Vatom_stk (Aid (RelKey (int_tcode (fun_code o) 1)), []) else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v) else @@ -469,7 +476,7 @@ struct let equal = eq_id_key open Hashset.Combine let hash : t -> tag = function - | ConstKey c -> combinesmall 1 (Constant.hash c) + | ConstKey c -> combinesmall 1 (Constant.CanOrd.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) | EvarKey evk -> combinesmall 4 (Evar.hash evk) |