diff options
Diffstat (limited to 'kernel')
68 files changed, 1316 insertions, 2214 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index d5feafbf91..be2b05da8d 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -18,6 +18,7 @@ #include <caml/misc.h> #include <caml/mlvalues.h> #include <caml/fail.h> +#include <caml/alloc.h> #include <caml/memory.h> #include "coq_instruct.h" #include "coq_fix_code.h" @@ -78,38 +79,41 @@ void * coq_stat_alloc (asize_t sz) } value coq_makeaccu (value i) { - code_t q; - code_t res = coq_stat_alloc(2 * sizeof(opcode_t)); - q = res; + CAMLparam1(i); + CAMLlocal1(res); + code_t q = coq_stat_alloc(2 * sizeof(opcode_t)); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = q; *q++ = VALINSTR(MAKEACCU); *q = (opcode_t)Int_val(i); - return (value)res; + CAMLreturn(res); } value coq_pushpop (value i) { - code_t res; - int n; - n = Int_val(i); + CAMLparam1(i); + CAMLlocal1(res); + code_t q; + res = caml_alloc_small(1, Abstract_tag); + int n = Int_val(i); if (n == 0) { - res = coq_stat_alloc(sizeof(opcode_t)); - *res = VALINSTR(STOP); - return (value)res; + q = coq_stat_alloc(sizeof(opcode_t)); + Code_val(res) = q; + *q = VALINSTR(STOP); + CAMLreturn(res); } else { - code_t q; - res = coq_stat_alloc(3 * sizeof(opcode_t)); - q = res; + q = coq_stat_alloc(3 * sizeof(opcode_t)); + Code_val(res) = q; *q++ = VALINSTR(POP); *q++ = (opcode_t)n; *q = VALINSTR(STOP); - return (value)res; + CAMLreturn(res); } } value coq_is_accumulate_code(value code){ - code_t q; + code_t q = Code_val(code); int res; - q = (code_t)code; res = Is_instruction(q,ACCUMULATE); return Val_bool(res); } @@ -132,11 +136,14 @@ value coq_is_accumulate_code(value code){ #define COPY32(dst,src) (*dst=*src) #endif /* ARCH_BIG_ENDIAN */ -value coq_tcode_of_code (value code, value size) { - code_t p, q, res; - asize_t len = (asize_t) Long_val(size); - res = coq_stat_alloc(len); - q = res; +value coq_tcode_of_code (value code) { + CAMLparam1 (code); + CAMLlocal1 (res); + code_t p, q; + asize_t len = (asize_t) caml_string_length(code); + res = caml_alloc_small(1, Abstract_tag); + q = coq_stat_alloc(len); + Code_val(res) = q; len /= sizeof(opcode_t); for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) { opcode_t instr; @@ -166,5 +173,5 @@ value coq_tcode_of_code (value code, value size) { for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; }; } } - return (value)res; + CAMLreturn(res); } diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index 5c85389dd5..638d6b5ab5 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -26,7 +26,7 @@ void init_arity(); #define Is_instruction(pc,instr) (*pc == VALINSTR(instr)) -value coq_tcode_of_code(value code, value len); +value coq_tcode_of_code(value code); value coq_makeaccu (value i); value coq_pushpop (value i); value coq_is_accumulate_code(value code); diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index af89712d5e..a944dbb06c 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -16,6 +16,7 @@ #include <stdio.h> #include <signal.h> #include <stdint.h> +#include <caml/memory.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -163,8 +164,11 @@ extern void caml_process_pending_signals(void); /* The interpreter itself */ value coq_interprete -(code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args) +(code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args) { + /* coq_accu is not allocated on the OCaml heap */ + CAMLparam2(coq_atom_tbl, coq_global_data); + /*Declaration des variables */ #ifdef PC_REG register code_t pc PC_REG; @@ -196,7 +200,7 @@ value coq_interprete coq_instr_table = (char **) coq_jumptable; coq_instr_base = coq_Jumptbl_base; #endif - return Val_unit; + CAMLreturn(Val_unit); } #if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32) coq_jumptbl_base = coq_Jumptbl_base; @@ -626,7 +630,7 @@ value coq_interprete print_instr("CLOSUREREC"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ - Alloc_small(accu, nfuncs, 0); + Alloc_small(accu, nfuncs, Abstract_tag); for(i = 0; i < nfuncs; i++) { Field(accu,i) = (value)(pc+pc[i]); } @@ -662,7 +666,7 @@ value coq_interprete print_instr("CLOSURECOFIX"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ - Alloc_small(accu, nfunc, 0); + Alloc_small(accu, nfunc, Abstract_tag); for(i = 0; i < nfunc; i++) { Field(accu,i) = (value)(pc+pc[i]); } @@ -1028,7 +1032,7 @@ value coq_interprete CHECK_STACK(nargs+1); sp -= nargs; for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); - *--sp = accu; // Last argument is the pointer to the suspension + *--sp = accu; // Leftmost argument is the pointer to the suspension print_lint(nargs); coq_extra_args = nargs; pc = Code_val(coq_env); // Trigger evaluation @@ -1068,12 +1072,22 @@ value coq_interprete } } *--sp = accu; - /* We create the switch zipper */ - Alloc_small(accu, 5, Default_tag); - Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; - Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; - Field(accu, 4) = coq_env; - sp++;sp[0] = accu; + /* Create bytecode wrappers */ + Alloc_small(accu, 1, Abstract_tag); + Code_val(accu) = typlbl; + *--sp = accu; + Alloc_small(accu, 1, Abstract_tag); + Code_val(accu) = swlbl; + *--sp = accu; + /* We create the switch zipper */ + Alloc_small(accu, 5, Default_tag); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; + Field(accu, 2) = sp[3]; + Field(accu, 3) = sp[2]; + Field(accu, 4) = coq_env; + sp += 3; + sp[0] = accu; /* We create the atom */ Alloc_small(accu, 2, ATOM_SWITCH_TAG); Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; @@ -1460,7 +1474,7 @@ value coq_interprete Instruct(STOP){ print_instr("STOP"); coq_sp = sp; - return accu; + CAMLreturn(accu); } @@ -1473,7 +1487,8 @@ value coq_interprete #endif } -value coq_push_ra(value tcode) { +value coq_push_ra(value code) { + code_t tcode = Code_val(code); print_instr("push_ra"); coq_sp -= 3; coq_sp[0] = (value) tcode; @@ -1512,12 +1527,18 @@ value coq_push_vstack(value stk, value max_stack_size) { return Val_unit; } -value coq_interprete_ml(value tcode, value a, value e, value ea) { +value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) { + // Registering the other arguments w.r.t. the OCaml GC is done by coq_interprete + CAMLparam1(tcode); print_instr("coq_interprete"); - return coq_interprete((code_t)tcode, a, e, Long_val(ea)); + CAMLreturn (coq_interprete(Code_val(tcode), a, t, g, e, Long_val(ea))); print_instr("end coq_interprete"); } -value coq_eval_tcode (value tcode, value e) { - return coq_interprete_ml(tcode, Val_unit, e, 0); +value coq_interprete_byte(value* argv, int argn){ + return coq_interprete_ml(argv[0], argv[1], argv[2], argv[3], argv[4], argv[5]); +} + +value coq_eval_tcode (value tcode, value t, value g, value e) { + return coq_interprete_ml(tcode, Val_unit, t, g, e, 0); } diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h index 60865c32ec..c04e9e00b2 100644 --- a/kernel/byterun/coq_interp.h +++ b/kernel/byterun/coq_interp.h @@ -17,11 +17,10 @@ value coq_push_arguments(value args); value coq_push_vstack(value stk); -value coq_interprete_ml(value tcode, value a, value e, value ea); +value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea); +value coq_interprete_byte(value* argv, int argn); value coq_interprete - (code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args); - -value coq_eval_tcode (value tcode, value e); - + (code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args); +value coq_eval_tcode (value tcode, value t, value g, value e); diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 45cfae509d..542a05fd25 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -10,6 +10,8 @@ #include <stdio.h> #include <string.h> +#include <caml/alloc.h> +#include <caml/address_class.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -24,10 +26,6 @@ value * coq_stack_threshold; asize_t coq_max_stack_size = Coq_max_stack_size; /* global_data */ - -value coq_global_data; -value coq_atom_tbl; - int drawinstr; /* interp state */ @@ -50,7 +48,11 @@ value coq_static_alloc(value size) /* ML */ value accumulate_code(value unit) /* ML */ { - return (value) accumulate; + CAMLparam1(unit); + CAMLlocal1(res); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = accumulate; + CAMLreturn(res); } static void (*coq_prev_scan_roots_hook) (scanning_action); @@ -58,11 +60,12 @@ static void (*coq_prev_scan_roots_hook) (scanning_action); static void coq_scan_roots(scanning_action action) { register value * i; - /* Scan the global variables */ - (*action)(coq_global_data, &coq_global_data); - (*action)(coq_atom_tbl, &coq_atom_tbl); /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { +#ifdef NO_NAKED_POINTERS + /* The VM stack may contain C-allocated bytecode */ + if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue; +#endif (*action) (*i, i); }; /* Hook */ @@ -79,24 +82,10 @@ void init_coq_stack() coq_max_stack_size = Coq_max_stack_size; } -void init_coq_global_data(long requested_size) -{ - int i; - coq_global_data = alloc_shr(requested_size, 0); - for (i = 0; i < requested_size; i++) - Field (coq_global_data, i) = Val_unit; -} - -void init_coq_atom_tbl(long requested_size){ - int i; - coq_atom_tbl = alloc_shr(requested_size, 0); - for (i = 0; i < requested_size; i++) Field (coq_atom_tbl, i) = Val_unit; -} - void init_coq_interpreter() { coq_sp = coq_stack_high; - coq_interprete(NULL, Val_unit, Val_unit, 0); + coq_interprete(NULL, Val_unit, Atom(0), Atom(0), Val_unit, 0); } static int coq_vm_initialized = 0; @@ -112,13 +101,15 @@ value init_coq_vm(value unit) /* ML */ #endif /* THREADED_CODE */ /* Allocate the table of global and the stack */ init_coq_stack(); - init_coq_global_data(Coq_global_data_Size); - init_coq_atom_tbl(40); /* Initialing the interpreter */ init_coq_interpreter(); - /* Some predefined pointer code */ - accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t)); + /* Some predefined pointer code. + * It is typically contained in accumlator blocks whose tag is 0 and thus + * scanned by the GC, so make it look like an OCaml block. */ + value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); + Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ + accumulate = (code_t) Val_hp(accu_block); *accumulate = VALINSTR(ACCUMULATE); /* Initialize GC */ @@ -157,53 +148,6 @@ void realloc_coq_stack(asize_t required_space) #undef shift } -value get_coq_global_data(value unit) /* ML */ -{ - return coq_global_data; -} - -value get_coq_atom_tbl(value unit) /* ML */ -{ - return coq_atom_tbl; -} - -value realloc_coq_global_data(value size) /* ML */ -{ - mlsize_t requested_size, actual_size, i; - value new_global_data; - requested_size = Long_val(size); - actual_size = Wosize_val(coq_global_data); - if (requested_size >= actual_size) { - requested_size = (requested_size + 0x100) & 0xFFFFFF00; - new_global_data = alloc_shr(requested_size, 0); - for (i = 0; i < actual_size; i++) - initialize(&Field(new_global_data, i), Field(coq_global_data, i)); - for (i = actual_size; i < requested_size; i++){ - Field (new_global_data, i) = Val_long (0); - } - coq_global_data = new_global_data; - } - return Val_unit; -} - -value realloc_coq_atom_tbl(value size) /* ML */ -{ - mlsize_t requested_size, actual_size, i; - value new_atom_tbl; - requested_size = Long_val(size); - actual_size = Wosize_val(coq_atom_tbl); - if (requested_size >= actual_size) { - requested_size = (requested_size + 0x100) & 0xFFFFFF00; - new_atom_tbl = alloc_shr(requested_size, 0); - for (i = 0; i < actual_size; i++) - initialize(&Field(new_atom_tbl, i), Field(coq_atom_tbl, i)); - for (i = actual_size; i < requested_size; i++) - Field (new_atom_tbl, i) = Val_long (0); - coq_atom_tbl = new_atom_tbl; - } - return Val_unit; -} - value coq_set_drawinstr(value unit) { drawinstr = 1; diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index cec34f566c..9375b15de2 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -20,7 +20,6 @@ #define Coq_stack_size (4096 * sizeof(value)) #define Coq_stack_threshold (256 * sizeof(value)) -#define Coq_global_data_Size (4096 * sizeof(value)) #define Coq_max_stack_size (256 * 1024) #define TRANSP 0 @@ -34,9 +33,7 @@ extern value * coq_stack_threshold; /* global_data */ -extern value coq_global_data; extern int coq_all_transp; -extern value coq_atom_tbl; extern int drawinstr; /* interp state */ @@ -53,10 +50,6 @@ value init_coq_vm(value unit); /* ML */ value re_init_coq_vm(value unit); /* ML */ void realloc_coq_stack(asize_t required_space); -value get_coq_global_data(value unit); /* ML */ -value realloc_coq_global_data(value size); /* ML */ -value get_coq_atom_tbl(value unit); /* ML */ -value realloc_coq_atom_tbl(value size); /* ML */ value coq_set_transp_value(value transp); /* ML */ value get_coq_transp_value(value unit); /* ML */ #endif /* _COQ_MEMORY_ */ diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index 528babebfc..e05f3fb82e 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -9,6 +9,7 @@ /***********************************************************************/ #include <stdio.h> +#include <caml/memory.h> #include "coq_fix_code.h" #include "coq_instruct.h" #include "coq_memory.h" @@ -58,10 +59,36 @@ value coq_offset_closure(value v, value offset){ return (value)&Field(v, Int_val(offset)); } +value coq_set_bytecode_field(value v, value i, value code) { + // No write barrier because the bytecode does not live on the OCaml heap + Field(v, Long_val(i)) = (value) Code_val(code); + return Val_unit; +} + value coq_offset_tcode(value code,value offset){ - return((value)((code_t)code + Int_val(offset))); + CAMLparam1(code); + CAMLlocal1(res); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = Code_val(code) + Int_val(offset); + CAMLreturn(res); } -value coq_int_tcode(value code, value offset) { +value coq_int_tcode(value pc, value offset) { + code_t code = Code_val(pc); return Val_int(*((code_t) code + Int_val(offset))); } + +value coq_tcode_array(value tcodes) { + CAMLparam1(tcodes); + CAMLlocal2(res, tmp); + int i; + /* Assumes that the vector of types is small. This was implicit in the + previous code which was building the type array using Alloc_small. */ + res = caml_alloc_small(Wosize_val(tcodes), Default_tag); + for (i = 0; i < Wosize_val(tcodes); i++) { + tmp = caml_alloc_small(1, Abstract_tag); + Code_val(tmp) = (code_t) Field(tcodes, i); + Store_field(res, i, tmp); + } + CAMLreturn(res); +} diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 5f683790c1..1d8861cbc0 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -96,7 +96,7 @@ module type RedFlagsSig = sig val red_transparent : reds -> transparent_state val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool - val red_projection : reds -> projection -> bool + val red_projection : reds -> Projection.t -> bool end module RedFlags = (struct @@ -265,7 +265,7 @@ type 'a infos_cache = { i_repr : 'a infos -> 'a infos_tab -> constr -> 'a; i_env : env; i_sigma : existential -> constr option; - i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t; + i_rels : (Context.Rel.Declaration.t * lazy_val) Range.t; } and 'a infos = { @@ -314,12 +314,11 @@ let evar_value cache ev = cache.i_sigma ev let create mk_cl flgs env evars = - let open Pre_env in let cache = { i_repr = mk_cl; i_env = env; i_sigma = evars; - i_rels = (Environ.pre_env env).env_rel_context.env_rel_map; + i_rels = env.env_rel_context.env_rel_map; } in { i_flags = flgs; i_cache = cache } @@ -364,7 +363,7 @@ and fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) @@ -482,7 +481,7 @@ let rec lft_fconstr n ft = let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = - if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v + if Int.equal k 0 then v else Array.Fun1.map lft_fconstr k v let clos_rel e i = match expand_rel i e with @@ -547,7 +546,7 @@ let mk_clos_vect env v = match v with | [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|] | [|v0; v1; v2; v3|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] -| v -> CArray.Fun1.map mk_clos env v +| v -> Array.Fun1.map mk_clos env v (* Translate the head constructor of t from constr to fconstr. This function is parameterized by the function to apply on the direct @@ -562,7 +561,7 @@ let mk_clos_deep clos_fun env t = term = FCast (clos_fun env a, k, clos_fun env b)} | App (f,v) -> { norm = Red; - term = FApp (clos_fun env f, CArray.Fun1.map clos_fun env v) } + term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) } | Proj (p,c) -> { norm = Red; term = FProj (p, clos_fun env c) } @@ -605,21 +604,21 @@ let rec to_constr constr_fun lfts v = Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve) | FFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in - let ftys = CArray.Fun1.map mk_clos e tys in - let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in + let ftys = Array.Fun1.map mk_clos e tys in + let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in let lfts' = el_liftn n lfts in - mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys, - CArray.Fun1.map constr_fun lfts' fbds)) + mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, + Array.Fun1.map constr_fun lfts' fbds)) | FCoFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in - let ftys = CArray.Fun1.map mk_clos e tys in - let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in + let ftys = Array.Fun1.map mk_clos e tys in + let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys, - CArray.Fun1.map constr_fun lfts' fbds)) + mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, + Array.Fun1.map constr_fun lfts' fbds)) | FApp (f,ve) -> mkApp (constr_fun lfts f, - CArray.Fun1.map constr_fun lfts ve) + Array.Fun1.map constr_fun lfts ve) | FProj (p,c) -> mkProj (p,constr_fun lfts c) @@ -1024,14 +1023,14 @@ and norm_head info tab m = | FProd(na,dom,rng) -> mkProd(na, kl info tab dom, kl info tab rng) | FCoFix((n,(na,tys,bds)),e) -> - let ftys = CArray.Fun1.map mk_clos e tys in + let ftys = Array.Fun1.map mk_clos e tys in let fbds = - CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in + Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) | FFix((n,(na,tys,bds)),e) -> - let ftys = CArray.Fun1.map mk_clos e tys in + let ftys = Array.Fun1.map mk_clos e tys in let fbds = - CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in + Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) | FEvar((i,args),env) -> mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args) @@ -1052,7 +1051,12 @@ let norm_val info tab v = let inject c = mk_clos (subs_id 0) c -let whd_stack infos tab m stk = +let whd_stack infos tab m stk = match m.norm with +| Whnf | Norm -> + (** No need to perform [kni] nor to unlock updates because + every head subterm of [m] is [Whnf] or [Norm] *) + knh infos m stk +| Red | Cstr -> let k = kni infos tab m stk in let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 3a7f77d521..63daa4a7c3 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -74,7 +74,7 @@ module type RedFlagsSig = sig (** This tests if the projection is in unfolded state already or is unfodable due to delta. *) - val red_projection : reds -> projection -> bool + val red_projection : reds -> Projection.t -> bool end module RedFlags : RedFlagsSig @@ -132,7 +132,7 @@ type fterm = | FInd of inductive Univ.puniverses | FConstruct of constructor Univ.puniverses | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) @@ -239,9 +239,6 @@ val lift_fconstr_vect : int -> fconstr array -> fconstr array val mk_clos : fconstr subs -> constr -> fconstr val mk_clos_vect : fconstr subs -> constr array -> fconstr array -val mk_clos_deep : - (fconstr subs -> constr -> fconstr) -> - fconstr subs -> constr -> fconstr val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 5ed9b6c675..521f540d22 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -36,7 +36,6 @@ let last_variant_tag = 245 type structured_constant = | Const_sort of Sorts.t | Const_ind of inductive - | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t @@ -51,8 +50,6 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_sort _, _ -> false | Const_ind i1, Const_ind i2 -> eq_ind i1 i2 | Const_ind _, _ -> false -| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 -| Const_proj _, _ -> false | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 | Const_b0 _, _ -> false | Const_bn (t1, a1), Const_bn (t2, a2) -> @@ -66,13 +63,12 @@ let rec hash_structured_constant c = match c with | Const_sort s -> combinesmall 1 (Sorts.hash s) | Const_ind i -> combinesmall 2 (ind_hash i) - | Const_proj p -> combinesmall 3 (Constant.hash p) - | Const_b0 t -> combinesmall 4 (Int.hash t) + | Const_b0 t -> combinesmall 3 (Int.hash t) | Const_bn (t, a) -> let fold h c = combine h (hash_structured_constant c) in let h = Array.fold_left fold 0 a in - combinesmall 5 (combine (Int.hash t) h) - | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) + combinesmall 4 (combine (Int.hash t) h) + | Const_univ_level l -> combinesmall 5 (Univ.Level.hash l) let eq_annot_switch asw1 asw2 = let eq_ci ci1 ci2 = @@ -246,7 +242,6 @@ let pp_sort s = let rec pp_struct_const = function | Const_sort s -> pp_sort s | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i - | Const_proj p -> Constant.print p | Const_b0 i -> int i | Const_bn (i,t) -> int i ++ surround (prvect_with_sep pr_comma pp_struct_const t) @@ -309,7 +304,7 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblb)) | Kpushfields n -> str "pushfields " ++ int n | Kfield n -> str "field " ++ int n - | Ksetfield n -> str "set field" ++ int n + | Ksetfield n -> str "setfield " ++ int n | Kstop -> str "stop" diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 03b6bc619d..238edc0af5 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -30,7 +30,6 @@ val last_variant_tag : tag type structured_constant = | Const_sort of Sorts.t | Const_ind of inductive - | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 0766f49b39..7a27a3d206 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -20,7 +20,7 @@ open Cinstr open Clambda open Constr open Declarations -open Pre_env +open Environ (* Compilation of variables + computing free variables *) @@ -77,6 +77,7 @@ open Pre_env (* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) (* If such a block is matched against, we have to force evaluation, *) (* function [fcofixi] is then applied to [ai'] [arg1] ... [argp] *) +(* (note that [ai'] is a pointer to the closure, passed as argument) *) (* Once evaluation is completed [ai'] is updated with the result: *) (* ai' <-- *) (* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) @@ -398,55 +399,55 @@ let code_makeblock ~stack_size ~arity ~tag cont = Kpush :: nest_block tag arity cont end -let compile_structured_constant reloc sc sz cont = +let compile_structured_constant cenv sc sz cont = set_max_stack_size sz; Kconst sc :: cont (* compiling application *) -let comp_args comp_expr reloc args sz cont = +let comp_args comp_expr cenv args sz cont = let nargs_m_1 = Array.length args - 1 in - let c = ref (comp_expr reloc args.(0) (sz + nargs_m_1) cont) in + let c = ref (comp_expr cenv args.(0) (sz + nargs_m_1) cont) in for i = 1 to nargs_m_1 do - c := comp_expr reloc args.(i) (sz + nargs_m_1 - i) (Kpush :: !c) + c := comp_expr cenv args.(i) (sz + nargs_m_1 - i) (Kpush :: !c) done; !c -let comp_app comp_fun comp_arg reloc f args sz cont = +let comp_app comp_fun comp_arg cenv f args sz cont = let nargs = Array.length args in - if Int.equal nargs 0 then comp_fun reloc f sz cont + if Int.equal nargs 0 then comp_fun cenv f sz cont else match is_tailcall cont with | Some k -> - comp_args comp_arg reloc args sz + comp_args comp_arg cenv args sz (Kpush :: - comp_fun reloc f (sz + nargs) + comp_fun cenv f (sz + nargs) (Kappterm(nargs, k + nargs) :: (discard_dead_code cont))) | None -> if nargs < 4 then - comp_args comp_arg reloc args sz - (Kpush :: (comp_fun reloc f (sz+nargs) (Kapply nargs :: cont))) + comp_args comp_arg cenv args sz + (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont))) else let lbl,cont1 = label_code cont in Kpush_retaddr lbl :: - (comp_args comp_arg reloc args (sz + 3) - (Kpush :: (comp_fun reloc f (sz+3+nargs) (Kapply nargs :: cont1)))) + (comp_args comp_arg cenv args (sz + 3) + (Kpush :: (comp_fun cenv f (sz+3+nargs) (Kapply nargs :: cont1)))) (* Compiling free variables *) -let compile_fv_elem reloc fv sz cont = +let compile_fv_elem cenv fv sz cont = match fv with - | FVrel i -> pos_rel i reloc sz :: cont - | FVnamed id -> pos_named id reloc :: cont - | FVuniv_var i -> pos_universe_var i reloc sz :: cont - | FVevar evk -> pos_evar evk reloc :: cont + | FVrel i -> pos_rel i cenv sz :: cont + | FVnamed id -> pos_named id cenv :: cont + | FVuniv_var i -> pos_universe_var i cenv sz :: cont + | FVevar evk -> pos_evar evk cenv :: cont -let rec compile_fv reloc l sz cont = +let rec compile_fv cenv l sz cont = match l with | [] -> cont - | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem reloc fvn sz cont + | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem cenv fvn sz cont | fvn :: tl -> - compile_fv_elem reloc fvn sz - (Kpush :: compile_fv reloc tl (sz + 1) cont) + compile_fv_elem cenv fvn sz + (Kpush :: compile_fv cenv tl (sz + 1) cont) (* Compiling constants *) @@ -471,61 +472,58 @@ let make_areconst n else_lbl cont = Kareconst (n, else_lbl)::cont (* sz is the size of the local stack *) -let rec compile_lam env reloc lam sz cont = +let rec compile_lam env cenv lam sz cont = set_max_stack_size sz; match lam with - | Lrel(_, i) -> pos_rel i reloc sz :: cont + | Lrel(_, i) -> pos_rel i cenv sz :: cont - | Lval v -> compile_structured_constant reloc v sz cont + | Lval v -> compile_structured_constant cenv v sz cont | Lproj (n,kn,arg) -> - compile_lam env reloc arg sz (Kproj (n,kn) :: cont) + compile_lam env cenv arg sz (Kproj (n,kn) :: cont) - | Lvar id -> pos_named id reloc :: cont + | Lvar id -> pos_named id cenv :: cont | Levar (evk, args) -> if Array.is_empty args then - compile_fv_elem reloc (FVevar evk) sz cont + compile_fv_elem cenv (FVevar evk) sz cont else - comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz cont + comp_app compile_fv_elem (compile_lam env) cenv (FVevar evk) args sz cont - | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont + | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont | Lind (ind,u) -> if Univ.Instance.is_empty u then - compile_structured_constant reloc (Const_ind ind) sz cont - else comp_app compile_structured_constant compile_universe reloc + compile_structured_constant cenv (Const_ind ind) sz cont + else comp_app compile_structured_constant compile_universe cenv (Const_ind ind) (Univ.Instance.to_array u) sz cont | Lsort (Sorts.Prop _ as s) -> - compile_structured_constant reloc (Const_sort s) sz cont + compile_structured_constant cenv (Const_sort s) sz cont | Lsort (Sorts.Type u) -> - (* We separate global and local universes in [u]. The former will be part - of the structured constant, while the later (if any) will be applied as - arguments. *) - let open Univ in begin - let u,s = Universe.compact u in - (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) - let compile_get_univ reloc idx sz cont = - set_max_stack_size sz; - compile_fv_elem reloc (FVuniv_var idx) sz cont - in - if List.is_empty s then - compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont - else - comp_app compile_structured_constant compile_get_univ reloc + (* We represent universes as a global constant with local universes + "compacted", i.e. as [u arg0 ... argn] where we will substitute (after + evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *) + let u,s = Univ.compact_univ u in + let compile_get_univ cenv idx sz cont = + set_max_stack_size sz; + compile_fv_elem cenv (FVuniv_var idx) sz cont + in + if List.is_empty s then + compile_structured_constant cenv (Const_sort (Sorts.Type u)) sz cont + else + comp_app compile_structured_constant compile_get_univ cenv (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont - end | Llet (id,def,body) -> - compile_lam env reloc def sz + compile_lam env cenv def sz (Kpush :: - compile_lam env (push_local sz reloc) body (sz+1) (add_pop 1 cont)) + compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont)) | Lprod (dom,codom) -> let cont1 = - Kpush :: compile_lam env reloc dom (sz+1) (Kmakeprod :: cont) in - compile_lam env reloc codom sz cont1 + Kpush :: compile_lam env cenv dom (sz+1) (Kmakeprod :: cont) in + compile_lam env cenv codom sz cont1 | Llam (ids,body) -> let arity = Array.length ids in @@ -536,12 +534,12 @@ let rec compile_lam env reloc lam sz cont = in fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; let fv = fv r_fun in - compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) + compile_fv cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) | Lapp (f, args) -> begin match f with - | Lconst (kn,u) -> compile_constant env reloc kn u args sz cont - | _ -> comp_app (compile_lam env) (compile_lam env) reloc f args sz cont + | Lconst (kn,u) -> compile_constant env cenv kn u args sz cont + | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont end | Lfix ((rec_args, init), (decl, types, bodies)) -> @@ -573,7 +571,7 @@ let rec compile_lam env reloc lam sz cont = fun_code := [Ksequence(fcode,!fun_code)] done; let fv = !rfv in - compile_fv reloc fv.fv_rev sz + compile_fv cenv fv.fv_rev sz (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) @@ -609,7 +607,7 @@ let rec compile_lam env reloc lam sz cont = done; let fv = !rfv in set_max_stack_size (sz + fv.size + ndef + 2); - compile_fv reloc fv.fv_rev sz + compile_fv cenv fv.fv_rev sz (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) @@ -627,7 +625,7 @@ let rec compile_lam env reloc lam sz cont = let branch1, cont = make_branch cont in (* Compilation of the return type *) let fcode = - ensure_stack_capacity (compile_lam env reloc t sz) [Kpop sz; Kstop] + 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)]; @@ -655,7 +653,7 @@ let rec compile_lam env reloc lam sz cont = (* Compilation of constant branches *) for i = nconst - 1 downto 0 do let aux = - compile_lam env reloc branches.constant_branches.(i) sz_b (branch::!c) + compile_lam env cenv branches.constant_branches.(i) sz_b (branch::!c) in let lbl_b,code_b = label_code aux in lbl_consts.(i) <- lbl_b; @@ -667,7 +665,7 @@ let rec compile_lam env reloc lam sz cont = let (ids, body) = branches.nonconstant_branches.(i) in let arity = Array.length ids in let code_b = - compile_lam env (push_param arity sz_b reloc) + compile_lam env (push_param arity sz_b cenv) body (sz_b+arity) (add_pop arity (branch::!c)) in let code_b = if tag < last_variant_tag then begin @@ -705,25 +703,25 @@ let rec compile_lam env reloc lam sz cont = | Kbranch lbl -> Kpush_retaddr lbl :: !c | _ -> !c in - compile_lam env reloc a sz code_sw + compile_lam env cenv a sz code_sw | Lmakeblock (tag,args) -> let arity = Array.length args in let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in - comp_args (compile_lam env) reloc args sz cont + comp_args (compile_lam env) cenv args sz cont | Lprim (kn, ar, op, args) -> - op_compilation env ar op kn reloc args sz cont + op_compilation env ar op kn cenv args sz cont | Luint v -> (match v with - | UintVal i -> compile_structured_constant reloc (Const_b0 (Uint31.to_int i)) sz cont + | UintVal i -> compile_structured_constant cenv (Const_b0 (Uint31.to_int i)) sz cont | UintDigits ds -> let nargs = Array.length ds in if Int.equal nargs 31 then let (escape,labeled_cont) = make_branch cont in let else_lbl = Label.create() in - comp_args (compile_lam env) reloc ds sz + comp_args (compile_lam env) cenv ds sz ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont) else let code_construct cont = (* spiwack: variant of the global code_construct @@ -739,40 +737,40 @@ let rec compile_lam env reloc lam sz cont = Kclosure(lbl,0) :: cont in comp_app (fun _ _ _ cont -> code_construct cont) - (compile_lam env) reloc () ds sz cont + (compile_lam env) cenv () ds sz cont | UintDecomp t -> let escape_lbl, labeled_cont = label_code cont in - compile_lam env reloc t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont)) + compile_lam env cenv t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont)) (* spiwack : compilation of constants with their arguments. Makes a special treatment with 31-bit integer addition *) -and compile_get_global reloc (kn,u) sz cont = +and compile_get_global cenv (kn,u) sz cont = set_max_stack_size sz; if Univ.Instance.is_empty u then Kgetglobal kn :: cont else comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) - compile_universe reloc () (Univ.Instance.to_array u) sz cont + compile_universe cenv () (Univ.Instance.to_array u) sz cont -and compile_universe reloc uni sz cont = +and compile_universe cenv uni sz cont = set_max_stack_size sz; match Univ.Level.var_index uni with - | None -> compile_structured_constant reloc (Const_univ_level uni) sz cont - | Some idx -> pos_universe_var idx reloc sz :: cont + | None -> compile_structured_constant cenv (Const_univ_level uni) sz cont + | Some idx -> pos_universe_var idx cenv sz :: cont -and compile_constant env reloc kn u args sz cont = +and compile_constant env cenv kn u args sz cont = set_max_stack_size sz; if Univ.Instance.is_empty u then (* normal compilation *) comp_app (fun _ _ sz cont -> - compile_get_global reloc (kn,u) sz cont) - (compile_lam env) reloc () args sz cont + compile_get_global cenv (kn,u) sz cont) + (compile_lam env) cenv () args sz cont else - let compile_arg reloc constr_or_uni sz cont = + let compile_arg cenv constr_or_uni sz cont = match constr_or_uni with - | ArgLambda t -> compile_lam env reloc t sz cont - | ArgUniv uni -> compile_universe reloc uni sz cont + | ArgLambda t -> compile_lam env cenv t sz cont + | ArgUniv uni -> compile_universe cenv uni sz cont in let u = Univ.Instance.to_array u in let lu = Array.length u in @@ -781,7 +779,7 @@ and compile_constant env reloc kn u args sz cont = (fun i -> if i < lu then ArgUniv u.(i) else ArgLambda args.(i-lu)) in comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) - compile_arg reloc () all sz cont + compile_arg cenv () all sz cont (*template for n-ary operation, invariant: n>=1, the operations does the following : @@ -790,34 +788,34 @@ and compile_constant env reloc kn u args sz cont = 3/ if at least one is not, branches to the normal behavior: Kgetglobal (get_alias !global_env kn) *) and op_compilation env n op = - let code_construct reloc kn sz cont = + let code_construct cenv kn sz cont = let f_cont = let else_lbl = Label.create () in Kareconst(n, else_lbl):: Kacc 0:: Kpop 1:: op:: Kreturn 0:: Klabel else_lbl:: (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*) - compile_get_global reloc kn sz ( + compile_get_global cenv kn sz ( Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *) in let lbl = Label.create () in fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)]; Kclosure(lbl, 0)::cont in - fun kn reloc args sz cont -> + fun kn cenv args sz cont -> let nargs = Array.length args in if Int.equal nargs n then (*if it is a fully applied addition*) let (escape, labeled_cont) = make_branch cont in let else_lbl = Label.create () in assert (n < 4); - comp_args (compile_lam env) reloc args sz + comp_args (compile_lam env) cenv args sz (Kisconst else_lbl::(make_areconst (n-1) else_lbl (*Kaddint31::escape::Klabel else_lbl::Kpush::*) (op::escape::Klabel else_lbl::Kpush:: (* works as comp_app with nargs < 4 and non-tailcall cont*) - compile_get_global reloc kn (sz+n) (Kapply n::labeled_cont)))) + compile_get_global cenv kn (sz+n) (Kapply n::labeled_cont)))) else - comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont) - (compile_lam env) reloc () args sz cont + comp_app (fun cenv _ sz cont -> code_construct cenv kn sz cont) + (compile_lam env) cenv () args sz cont let is_univ_copy max u = @@ -832,6 +830,8 @@ let is_univ_copy max u = else false +let dump_bytecode = ref false + let dump_bytecodes init code fvs = let open Pp in (str "code =" ++ fnl () ++ @@ -846,11 +846,11 @@ let compile ~fail_on_error ?universes:(universes=0) env c = Label.reset_label_counter (); let cont = [Kstop] in try - let reloc, init_code = + let cenv, init_code = if Int.equal universes 0 then let lam = lambda_of_constr ~optimize:true env c in - let reloc = empty_comp_env () in - reloc, ensure_stack_capacity (compile_lam env reloc lam 0) cont + let cenv = empty_comp_env () in + cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont else (* We are going to generate a lambda, but merge the universe closure * with the function closure if it exists. @@ -858,7 +858,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = let lam = lambda_of_constr ~optimize:true env c in let params, body = decompose_Llam lam in let arity = Array.length params in - let reloc = empty_comp_env () in + let cenv = empty_comp_env () in let full_arity = arity + universes in let r_fun = comp_env_fun ~univs:universes arity in let lbl_fun = Label.create () in @@ -869,13 +869,13 @@ let compile ~fail_on_error ?universes:(universes=0) env c = 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 reloc fv.fv_rev 0) + ensure_stack_capacity (compile_fv cenv fv.fv_rev 0) (Kclosure(lbl_fun,fv.size) :: cont) in - reloc, init_code + cenv, init_code in - let fv = List.rev (!(reloc.in_env).fv_rev) in - (if !Flags.dump_bytecode then + let fv = List.rev (!(cenv.in_env).fv_rev) in + (if !dump_bytecode then Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive msg -> @@ -922,13 +922,13 @@ let op2_compilation op = fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)]; Kclosure(lbl, 0)::cont in - fun normal fc _ reloc args sz cont -> + fun normal fc _ cenv args sz cont -> if not fc then raise Not_found else let nargs = Array.length args in if nargs=2 then (*if it is a fully applied addition*) let (escape, labeled_cont) = make_branch cont in let else_lbl = Label.create () in - comp_args compile_constr reloc args sz + comp_args compile_constr cenv args sz (Kisconst else_lbl::(make_areconst 1 else_lbl (*Kaddint31::escape::Klabel else_lbl::Kpush::*) (op::escape::Klabel else_lbl::Kpush:: @@ -940,5 +940,5 @@ let op2_compilation op = code_construct normal cont else comp_app (fun _ _ _ cont -> code_construct normal cont) - compile_constr reloc () args sz cont *) + compile_constr cenv () args sz cont *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index abab58b60b..57d3e6fc27 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -12,7 +12,7 @@ open Cbytecodes open Cemitcodes open Constr open Declarations -open Pre_env +open Environ (** Should only be used for monomorphic terms *) val compile : fail_on_error:bool -> @@ -25,3 +25,6 @@ val compile_constant_body : fail_on_error:bool -> (** Shortcut of the previous function used during module strengthening *) val compile_alias : Names.Constant.t -> body_code + +(** Dump the bytecode after compilation (for debugging purposes) *) +val dump_bytecode : bool ref diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 14f4f27c09..2426255e48 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -13,20 +13,21 @@ (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) open Names -open Term +open Constr open Cbytecodes open Copcodes open Mod_subst type emitcodes = String.t -external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code" +external tcode_of_code : Bytes.t -> Vmvalues.tcode = "coq_tcode_of_code" (* Relocation information *) type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant | Reloc_getglobal of Names.Constant.t + | Reloc_proj_name of Constant.t let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2 @@ -35,6 +36,8 @@ let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_const _, _ -> false | Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2 | Reloc_getglobal _, _ -> false +| Reloc_proj_name p1, Reloc_proj_name p2 -> Constant.equal p1 p2 +| Reloc_proj_name _, _ -> false let hash_reloc_info r = let open Hashset.Combine in @@ -42,6 +45,7 @@ let hash_reloc_info r = | 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 (Constant.hash p) module RelocTable = Hashtbl.Make(struct type t = reloc_info @@ -82,7 +86,7 @@ let patch buff pl f = (** Order seems important here? *) let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in let buff = patch_int buff reloc in - tcode_of_code buff (Bytes.length buff) + tcode_of_code buff (* Buffering of bytecode *) @@ -187,6 +191,9 @@ let slot_for_getglobal env p = enter env (Reloc_getglobal p); out_int env 0 +let slot_for_proj_name env p = + enter env (Reloc_proj_name p); + out_int env 0 (* Emission of one instruction *) @@ -277,7 +284,7 @@ let emit_instr env = function if n <= 1 then out env (opSETFIELD0+n) else (out env opSETFIELD;out_int env n) | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" - | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_const env (Const_proj p) + | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_proj_name env p | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size (* spiwack *) | Kbranch lbl -> out env opBRANCH; out_label env lbl @@ -353,7 +360,6 @@ type to_patch = emitcodes * patches * fv let rec subst_strcst s sc = match sc with | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc - | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) @@ -365,6 +371,7 @@ let subst_reloc s ri = Reloc_annot {a with ci = ci} | Reloc_const sc -> Reloc_const (subst_strcst s sc) | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) + | Reloc_proj_name p -> Reloc_proj_name (subst_constant s p) let subst_patches subst p = let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 03920dc1a3..696721c375 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -5,6 +5,7 @@ type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant | Reloc_getglobal of Constant.t + | Reloc_proj_name of Constant.t type patches type emitcodes diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 4a3c03d85e..f42c46175c 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -31,7 +31,7 @@ and lambda = | Lprim of pconstant * int (* arity *) * instruction * lambda array | Lcase of case_info * reloc_table * lambda * lambda * lam_branches | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl + | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of int * lambda array | Lval of structured_constant | Lsort of Sorts.t @@ -39,6 +39,10 @@ and lambda = | Lproj of int * Constant.t * lambda | Luint of uint +(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation +to be correct. Otherwise, memoization of previous evaluations will be applied +again to extra arguments (see #7333). *) + and lam_branches = { constant_branches : lambda array; nonconstant_branches : (Name.t array * lambda) array } diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 7b637c20e6..b722e42008 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -6,7 +6,7 @@ open Constr open Declarations open Cbytecodes open Cinstr -open Pre_env +open Environ open Pp let pr_con sp = str(Names.Label.to_string (Constant.label sp)) @@ -152,7 +152,7 @@ let rec map_lam_with_binders g f n lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam | Levar (evk, args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') | Lprod(dom,codom) -> let dom' = f n dom in @@ -167,19 +167,19 @@ let rec map_lam_with_binders g f n lam = if body == body' && def == def' then lam else Llet(id,def',body') | Lapp(fct,args) -> let fct' = f n fct in - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if fct == fct' && args == args' then lam else mkLapp fct' args' | Lcase(ci,rtbl,t,a,branches) -> let const = branches.constant_branches in let nonconst = branches.nonconstant_branches in let t' = f n t in let a' = f n a in - let const' = Array.smartmap (f n) const in + let const' = Array.Smart.map (f n) const in let on_b b = let (ids,body) = b in let body' = f (g (Array.length ids) n) body in if body == body' then b else (ids,body') in - let nonconst' = Array.smartmap on_b nonconst in + let nonconst' = Array.Smart.map on_b nonconst in let branches' = if const == const' && nonconst == nonconst' then branches @@ -190,20 +190,20 @@ let rec map_lam_with_binders g f n lam = if t == t' && a == a' && branches == branches' then lam else Lcase(ci,rtbl,t',a',branches') | Lfix(init,(ids,ltypes,lbodies)) -> - let ltypes' = Array.smartmap (f n) ltypes in - let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + let ltypes' = Array.Smart.map (f n) ltypes in + let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in if ltypes == ltypes' && lbodies == lbodies' then lam else Lfix(init,(ids,ltypes',lbodies')) | Lcofix(init,(ids,ltypes,lbodies)) -> - let ltypes' = Array.smartmap (f n) ltypes in - let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + let ltypes' = Array.Smart.map (f n) ltypes in + let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in if ltypes == ltypes' && lbodies == lbodies' then lam else Lcofix(init,(ids,ltypes',lbodies')) | Lmakeblock(tag,args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then lam else Lmakeblock(tag,args') | Lprim(kn,ar,op,args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then lam else Lprim(kn,ar,op,args') | Lproj(i,kn,arg) -> let arg' = f n arg in @@ -216,7 +216,7 @@ and map_uint g f n u = match u with | UintVal _ -> u | UintDigits(args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then u else UintDigits(args') | UintDecomp(a) -> let a' = f n a in @@ -250,7 +250,7 @@ let rec lam_exsubst subst lam = let lam_subst_args subst args = if is_subs_id subst then args - else Array.smartmap (lam_exsubst subst) args + else Array.Smart.map (lam_exsubst subst) args (** Simplification of lambda expression *) @@ -316,7 +316,7 @@ and simplify_app substf f substa args = simplify_app substf f subst_id args | _ -> mkLapp (simplify substf f) (simplify_args substa args) -and simplify_args subst args = Array.smartmap (simplify subst) args +and simplify_args subst args = Array.Smart.map (simplify subst) args and reduce_lapp substf lids body substa largs = match lids, largs with @@ -700,6 +700,7 @@ let rec lambda_of_constr env c = Lfix(rec_init, (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> + let rec_bodies = Array.map2 (Reduction.eta_expand env.global_env) rec_bodies type_bodies in let ltypes = lambda_of_args env 0 type_bodies in Renv.push_rels env names; let lbodies = lambda_of_args env 0 rec_bodies in @@ -707,12 +708,10 @@ let rec lambda_of_constr env c = Lcofix(init, (names, ltypes, lbodies)) | Proj (p,c) -> - let kn = Projection.constant p in - let cb = lookup_constant kn env.global_env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p env.global_env in let n = pb.proj_arg in let lc = lambda_of_constr env c in - Lproj (n,kn,lc) + Lproj (n,Projection.constant p,lc) and lambda_of_app env f args = match Constr.kind f with @@ -807,7 +806,7 @@ and lambda_of_args env start args = (*********************************) - +let dump_lambda = ref false let optimize_lambda lam = let lam = simplify subst_id lam in @@ -819,7 +818,7 @@ let lambda_of_constr ~optimize genv c = Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env c in let lam = if optimize then optimize_lambda lam else lam in - if !Flags.dump_lambda then + if !dump_lambda then Feedback.msg_debug (pp_lam lam); lam diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 89b7fd8e3b..8ff10b4549 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -1,13 +1,14 @@ open Names open Cinstr +open Environ exception TooLargeInductive of Pp.t -val lambda_of_constr : optimize:bool -> Pre_env.env -> Constr.t -> lambda +val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda val decompose_Llam : lambda -> Name.t array * lambda -val get_alias : Pre_env.env -> Constant.t -> Constant.t +val get_alias : env -> Constant.t -> Constant.t val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda @@ -25,3 +26,6 @@ val dynamic_int31_compilation : bool -> lambda array -> lambda (*spiwack: compiling function to insert dynamic decompilation before matching integers (in case they are in processor representation) *) val int31_escape_before_match : bool -> lambda -> lambda + +(** Dump the VM lambda code after compilation (for debugging purposes) *) +val dump_lambda : bool ref diff --git a/kernel/constr.ml b/kernel/constr.ml index ba7fecadf8..c11b9ebf46 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -100,7 +100,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr + | Proj of Projection.t * 'constr (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) type t = (t, t, Sorts.t, Instance.t) kind_of_term @@ -468,16 +468,44 @@ let iter_with_binders g f n c = match kind c with | Prod (_,t,c) -> f n t; f (g n) c | Lambda (_,t,c) -> f n t; f (g n) c | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c - | App (c,l) -> f n c; CArray.Fun1.iter f n l - | Evar (_,l) -> CArray.Fun1.iter f n l - | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl + | App (c,l) -> f n c; Array.Fun1.iter f n l + | Evar (_,l) -> Array.Fun1.iter f n l + | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl | Proj (p,c) -> f n c | Fix (_,(_,tl,bl)) -> - CArray.Fun1.iter f n tl; - CArray.Fun1.iter f (iterate g (Array.length tl) n) bl + Array.Fun1.iter f n tl; + Array.Fun1.iter f (iterate g (Array.length tl) n) bl | CoFix (_,(_,tl,bl)) -> - CArray.Fun1.iter f n tl; - CArray.Fun1.iter f (iterate g (Array.length tl) n) bl + Array.Fun1.iter f n tl; + Array.Fun1.iter f (iterate g (Array.length tl) n) bl + +(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate + subterms of [c] starting from [acc] and proceeding from left to + right according to the usual representation of the constructions as + [fold_constr] but it carries an extra data [n] (typically a lift + index) which is processed by [g] (which typically add 1 to [n]) at + each binder traversal; it is not recursive *) + +let fold_constr_with_binders g f n acc c = + match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g n) (f n acc t) c + | Lambda (na,t,c) -> f (g n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (p,c) -> f n acc c + | Evar (_,l) -> Array.fold_left (f n) acc l + | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd (* [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is @@ -509,7 +537,7 @@ let map f c = match kind c with else mkLetIn (na, b', t', k') | App (b,l) -> let b' = f b in - let l' = Array.smartmap f l in + let l' = Array.Smart.map f l in if b'==b && l'==l then c else mkApp (b', l') | Proj (p,t) -> @@ -517,23 +545,23 @@ let map f c = match kind c with if t' == t then c else mkProj (p, t') | Evar (e,l) -> - let l' = Array.smartmap f l in + let l' = Array.Smart.map f l in if l'==l then c else mkEvar (e, l') | Case (ci,p,b,bl) -> let b' = f b in let p' = f p in - let bl' = Array.smartmap f bl in + let bl' = Array.Smart.map f bl in if b'==b && p'==p && bl'==bl then c else mkCase (ci, p', b', bl') | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap f tl in - let bl' = Array.smartmap f bl in + let tl' = Array.Smart.map f tl in + let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.smartmap f tl in - let bl' = Array.smartmap f bl in + let tl' = Array.Smart.map f tl in + let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkCoFix (ln,(lna,tl',bl')) @@ -565,7 +593,7 @@ let fold_map f accu c = match kind c with else accu, mkLetIn (na, b', t', k') | App (b,l) -> let accu, b' = f accu b in - let accu, l' = Array.smartfoldmap f accu l in + let accu, l' = Array.Smart.fold_left_map f accu l in if b'==b && l'==l then accu, c else accu, mkApp (b', l') | Proj (p,t) -> @@ -573,23 +601,23 @@ let fold_map f accu c = match kind c with if t' == t then accu, c else accu, mkProj (p, t') | Evar (e,l) -> - let accu, l' = Array.smartfoldmap f accu l in + let accu, l' = Array.Smart.fold_left_map f accu l in if l'==l then accu, c else accu, mkEvar (e, l') | Case (ci,p,b,bl) -> let accu, b' = f accu b in let accu, p' = f accu p in - let accu, bl' = Array.smartfoldmap f accu bl in + let accu, bl' = Array.Smart.fold_left_map f accu bl in if b'==b && p'==p && bl'==bl then accu, c else accu, mkCase (ci, p', b', bl') | Fix (ln,(lna,tl,bl)) -> - let accu, tl' = Array.smartfoldmap f accu tl in - let accu, bl' = Array.smartfoldmap f accu bl in + let accu, tl' = Array.Smart.fold_left_map f accu tl in + let accu, bl' = Array.Smart.fold_left_map f accu bl in if tl'==tl && bl'==bl then accu, c else accu, mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let accu, tl' = Array.smartfoldmap f accu tl in - let accu, bl' = Array.smartfoldmap f accu bl in + let accu, tl' = Array.Smart.fold_left_map f accu tl in + let accu, bl' = Array.Smart.fold_left_map f accu bl in if tl'==tl && bl'==bl then accu, c else accu, mkCoFix (ln,(lna,tl',bl')) @@ -625,7 +653,7 @@ let map_with_binders g f l c0 = match kind c0 with else mkLetIn (na, b', t', c') | App (c, al) -> let c' = f l c in - let al' = CArray.Fun1.smartmap f l al in + let al' = Array.Fun1.Smart.map f l al in if c' == c && al' == al then c0 else mkApp (c', al') | Proj (p, t) -> @@ -633,28 +661,28 @@ let map_with_binders g f l c0 = match kind c0 with if t' == t then c0 else mkProj (p, t') | Evar (e, al) -> - let al' = CArray.Fun1.smartmap f l al in + let al' = Array.Fun1.Smart.map f l al in if al' == al then c0 else mkEvar (e, al') | Case (ci, p, c, bl) -> let p' = f l p in let c' = f l c in - let bl' = CArray.Fun1.smartmap f l bl in + let bl' = Array.Fun1.Smart.map f l bl in if p' == p && c' == c && bl' == bl then c0 else mkCase (ci, p', c', bl') | Fix (ln, (lna, tl, bl)) -> - let tl' = CArray.Fun1.smartmap f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.smartmap f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in if tl' == tl && bl' == bl then c0 else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = CArray.Fun1.smartmap f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.smartmap f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) -type instance_compare_fn = global_reference -> int -> +type instance_compare_fn = GlobRef.t -> int -> Univ.Instance.t -> Univ.Instance.t -> bool type constr_compare_fn = int -> constr -> constr -> bool @@ -692,10 +720,10 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.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 (ConstRef c1) nargs u1 u2 - | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (IndRef c1) nargs u1 u2 + Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (GlobRef.IndRef c1) nargs u1 u2 | Construct (c1,u1), Construct (c2,u2) -> - eq_constructor c1 c2 && leq_universes (ConstructRef c1) nargs u1 u2 + eq_constructor c1 c2 && leq_universes (GlobRef.ConstructRef c1) nargs u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> diff --git a/kernel/constr.mli b/kernel/constr.mli index 98c0eaa28d..742a13919a 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -122,7 +122,7 @@ val mkConst : Constant.t -> constr val mkConstU : pconstant -> constr (** Constructs a projection application *) -val mkProj : (projection * constr) -> constr +val mkProj : (Projection.t * constr) -> constr (** Inductive types *) @@ -220,7 +220,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr + | Proj of Projection.t * 'constr (** User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative @@ -318,7 +318,7 @@ where [info] is pretty-printing information *) val destCase : constr -> case_info * constr * constr * constr array (** Destructs a projection *) -val destProj : constr -> projection * constr +val destProj : constr -> Projection.t * constr (** Destructs the {% $ %}i{% $ %}th function of the block [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} @@ -402,6 +402,15 @@ val iter : (constr -> unit) -> constr -> unit val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +(** [iter_with_binders g f n c] iters [f n] on the immediate + subterms of [c]; it carries an extra data [n] (typically a lift + index) which is processed by [g] (which typically add 1 to [n]) at + each binder traversal; it is not recursive and the order with which + subterms are processed is not specified *) + +val fold_constr_with_binders : + ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b + type constr_compare_fn = int -> constr -> constr -> bool (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare @@ -413,7 +422,7 @@ val compare_head : constr_compare_fn -> constr_compare_fn (** Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .*) -type instance_compare_fn = global_reference -> int -> +type instance_compare_fn = GlobRef.t -> int -> Univ.Instance.t -> Univ.Instance.t -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to diff --git a/kernel/context.ml b/kernel/context.ml index 4f3f649c14..5d4a101840 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -192,7 +192,7 @@ struct let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given rel-context. *) - let map f = List.smartmap (Declaration.map_constr f) + let map f = List.Smart.map (Declaration.map_constr f) (** Perform a given action on every declaration in a given rel-context. *) let iter f = List.iter (Declaration.iter_constr f) @@ -392,7 +392,7 @@ struct let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given named-context. *) - let map f = List.smartmap (Declaration.map_constr f) + let map f = List.Smart.map (Declaration.map_constr f) (** Perform a given action on every declaration in a given named-context. *) let iter f = List.iter (Declaration.iter_constr f) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 6f4541e956..5783453e66 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -156,7 +156,7 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; + cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; @@ -227,28 +227,10 @@ let cook_constant ~hcons env { from = cb; info } = hyps) hyps ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in - let projection pb = - let c' = abstract_constant_body (expmod pb.proj_body) hyps in - let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in - let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in - let ((mind, _), _), n' = - try - let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in - match kind c' with - | App (f,l) -> (destInd f, Array.length l) - | Ind ind -> ind, 0 - | _ -> assert false - with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0) - in - let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in - { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; - proj_eta = etab, etat; - proj_type = ty'; proj_body = c' } - in { cook_body = body; cook_type = typ; - cook_proj = Option.map projection cb.const_proj; + cook_proj = cb.const_proj; cook_universes = univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7bd0ae5663..0d907f3dea 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,7 +21,7 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; + cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 0129489542..bbe0937820 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -20,13 +20,15 @@ open Vmvalues open Cemitcodes open Cbytecodes open Declarations -open Pre_env +open Environ open Cbytegen module NamedDecl = Context.Named.Declaration module RelDecl = Context.Rel.Declaration -external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" +external eval_tcode : tcode -> atom array -> vm_global -> values array -> values = "coq_eval_tcode" + +type global_data = { mutable glob_len : int; mutable glob_val : values array } (*******************) (* Linkage du code *) @@ -37,21 +39,28 @@ external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" (* [global_data] contient les valeurs des constantes globales (axiomes,definitions), les annotations des switch et les structured constant *) -external global_data : unit -> values array = "get_coq_global_data" +let global_data = { + glob_len = 0; + glob_val = Array.make 4096 crazy_val; +} -(* [realloc_global_data n] augmente de n la taille de [global_data] *) -external realloc_global_data : int -> unit = "realloc_coq_global_data" +let get_global_data () = Vmvalues.vm_global global_data.glob_val -let check_global_data n = - if n >= Array.length (global_data()) then realloc_global_data n +let realloc_global_data n = + let n = min (2 * n + 0x100) Sys.max_array_length in + let ans = Array.make n crazy_val in + let src = global_data.glob_val in + let () = Array.blit src 0 ans 0 (Array.length src) in + global_data.glob_val <- ans -let num_global = ref 0 +let check_global_data n = + if n >= Array.length global_data.glob_val then realloc_global_data n let set_global v = - let n = !num_global in + let n = global_data.glob_len in check_global_data n; - (global_data()).(n) <- v; - incr num_global; + global_data.glob_val.(n) <- v; + global_data.glob_len <- global_data.glob_len + 1; n (* table pour les structured_constant et les annotations des switchs *) @@ -68,11 +77,19 @@ module AnnotTable = Hashtbl.Make (struct let hash = hash_annot_switch end) +module ProjNameTable = Hashtbl.Make (struct + type t = Constant.t + let equal = Constant.equal + let hash = Constant.hash +end) + let str_cst_tbl : int SConstTable.t = SConstTable.create 31 let annot_tbl : int AnnotTable.t = AnnotTable.create 31 (* (annot_switch * int) Hashtbl.t *) +let proj_name_tbl : int ProjNameTable.t = ProjNameTable.create 31 + (*************************************************************) (*** Mise a jour des valeurs des variables et des constantes *) (*************************************************************) @@ -106,6 +123,13 @@ let slot_for_annot key = AnnotTable.add annot_tbl key n; n +let slot_for_proj_name key = + try ProjNameTable.find proj_name_tbl key + with Not_found -> + let n = set_global (val_of_proj_name key) in + ProjNameTable.add proj_name_tbl key n; + n + let rec slot_for_getglobal env kn = let (cb,(_,rk)) = lookup_constant_key kn env in try key rk @@ -133,23 +157,23 @@ and slot_for_fv env fv = | None -> v_of_id id, Id.Set.empty | Some c -> val_of_constr (env_of_id id env) c, - Environ.global_vars_set (Environ.env_of_pre_env env) c in + Environ.global_vars_set env c in build_lazy_val cache (v, d); v in let val_of_rel i = val_of_rel (nb_rel env - i) in let idfun _ x = x in match fv with | FVnamed id -> - let nv = Pre_env.lookup_named_val id env in + let nv = lookup_named_val id env in begin match force_lazy_val nv with | None -> - env |> Pre_env.lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun + env |> lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> - let rv = Pre_env.lookup_rel_val i env in + let rv = lookup_rel_val i env in begin match force_lazy_val rv with | None -> - env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel + env |> lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end | FVevar evk -> val_of_evar evk @@ -161,10 +185,11 @@ and eval_to_patch env (buff,pl,fv) = | Reloc_annot a -> slot_for_annot a | Reloc_const sc -> slot_for_str_cst sc | Reloc_getglobal kn -> slot_for_getglobal env kn + | Reloc_proj_name p -> slot_for_proj_name p in let tc = patch buff pl slots in let vm_env = Array.map (slot_for_fv env) fv in - eval_tcode tc vm_env + eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env and val_of_constr env c = match compile ~fail_on_error:true env c with diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 19b2b8b50a..72c96b0b9f 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -12,9 +12,11 @@ open Names open Constr -open Pre_env +open Environ val val_of_constr : env -> constr -> Vmvalues.values val set_opaque_const : Constant.t -> unit val set_transparent_const : Constant.t -> unit + +val get_global_data : unit -> Vmvalues.vm_global diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b7427d20a7..7bd70c0502 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -52,7 +52,7 @@ type inline = int option type projection_body = { proj_ind : MutInd.t; proj_npars : int; - proj_arg : int; + proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) proj_eta : constr * types; (* Eta-expanded term and type *) proj_body : constr; (* For compatibility with VMs only, the match version *) @@ -87,7 +87,7 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : projection_body option; + const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 3652a1ce44..75c0e5b4cc 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -42,7 +42,7 @@ let map_decl_arity f g = function let hcons_template_arity ar = { template_param_levels = ar.template_param_levels; - (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *) + (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) template_level = Univ.hcons_univ ar.template_level } (** {6 Constants } *) @@ -70,7 +70,7 @@ let is_opaque cb = match cb.const_body with let subst_rel_declaration sub = RelDecl.map_constr (subst_mps sub) -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) +let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub) let subst_const_type sub arity = if is_empty_subst sub then arity @@ -94,14 +94,13 @@ let subst_const_body sub cb = else let body' = subst_const_def sub cb.const_body in let type' = subst_const_type sub cb.const_type in - let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type - && proj' == cb.const_proj then cb + then cb else { const_hyps = []; const_body = body'; const_type = type'; - const_proj = proj'; + const_proj = cb.const_proj; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; @@ -117,7 +116,7 @@ let subst_const_body sub cb = let hcons_rel_decl = RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Constr.hcons %> RelDecl.map_type Constr.hcons -let hcons_rel_context l = List.smartmap hcons_rel_decl l +let hcons_rel_context l = List.Smart.map hcons_rel_decl l let hcons_const_def = function | Undef inl -> Undef inl @@ -178,7 +177,7 @@ let recarg_length p j = let (_,cstrs) = Rtree.dest_node p in Array.length (snd (Rtree.dest_node cstrs.(j-1))) -let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p +let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p (** {7 Substitution of inductive declarations } *) @@ -198,10 +197,10 @@ let subst_mind_packet sub mbp = mind_consnrealdecls = mbp.mind_consnrealdecls; mind_consnrealargs = mbp.mind_consnrealargs; mind_typename = mbp.mind_typename; - mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_ind_arity sub mbp.mind_arity; - mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; + mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealdecls = mbp.mind_nrealdecls; mind_kelim = mbp.mind_kelim; @@ -211,13 +210,13 @@ let subst_mind_packet sub mbp = mind_reloc_tbl = mbp.mind_reloc_tbl } let subst_mind_record sub (id, ps, pb as r) = - let ps' = Array.smartmap (subst_constant sub) ps in - let pb' = Array.smartmap (subst_const_proj sub) pb in + let ps' = Array.Smart.map (subst_constant sub) ps in + let pb' = Array.Smart.map (subst_const_proj sub) pb in if ps' == ps && pb' == pb then r else (id, ps', pb') let subst_mind_body sub mib = - { mind_record = Option.smartmap (Option.smartmap (subst_mind_record sub)) mib.mind_record ; + { mind_record = Option.Smart.map (Option.Smart.map (subst_mind_record sub)) mib.mind_record ; mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); @@ -225,7 +224,7 @@ let subst_mind_body sub mib = mind_nparams_rec = mib.mind_nparams_rec; mind_params_ctxt = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; - mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; + mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ; mind_universes = mib.mind_universes; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; @@ -263,15 +262,15 @@ let hcons_ind_arity = (** Substitution of inductive declarations *) let hcons_mind_packet oib = - let user = Array.smartmap Constr.hcons oib.mind_user_lc in - let nf = Array.smartmap Constr.hcons oib.mind_nf_lc in + let user = Array.Smart.map Constr.hcons oib.mind_user_lc in + let nf = Array.Smart.map Constr.hcons oib.mind_nf_lc in (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *) let nf = if Array.equal (==) user nf then user else nf in { oib with mind_typename = Names.Id.hcons oib.mind_typename; mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; mind_arity = hcons_ind_arity oib.mind_arity; - mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames; + mind_consnames = Array.Smart.map Names.Id.hcons oib.mind_consnames; mind_user_lc = user; mind_nf_lc = nf } @@ -283,7 +282,7 @@ let hcons_mind_universes miu = let hcons_mind mib = { mib with - mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; + mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; mind_universes = hcons_mind_universes mib.mind_universes } @@ -331,7 +330,7 @@ and hcons_structure_body sb = let sfb' = hcons_structure_field_body sfb in if l == l' && sfb == sfb' then fb else (l', sfb') in - List.smartmap map sb + List.Smart.map map sb and hcons_module_signature ms = hcons_functorize hcons_module_type hcons_structure_body hcons_module_signature ms diff --git a/kernel/environ.ml b/kernel/environ.ml index 9d4063e433..fb89576dd0 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -28,26 +28,206 @@ open Names open Constr open Vars open Declarations -open Pre_env open Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* The type of environments. *) -type named_context_val = Pre_env.named_context_val +(* The key attached to each constant is used by the VM to retrieve previous *) +(* evaluations of the constant. It is essentially an index in the symbols table *) +(* used by the VM. *) +type key = int CEphemeron.key option ref + +(** Linking information for the native compiler. *) + +type link_info = + | Linked of string + | LinkedInteractive of string + | NotLinked + +type constant_key = constant_body * (link_info ref * key) + +type mind_key = mutual_inductive_body * link_info ref + +type globals = { + env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; + env_inductives : mind_key Mindmap_env.t; + env_modules : module_body MPmap.t; + env_modtypes : module_type_body MPmap.t} + +type stratification = { + env_universes : UGraph.t; + env_engagement : engagement +} + +type val_kind = + | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key + | VKnone + +type lazy_val = val_kind ref + +let force_lazy_val vk = match !vk with +| VKnone -> None +| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None + +let dummy_lazy_val () = ref VKnone +let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) + +type named_context_val = { + env_named_ctx : Context.Named.t; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} + +type rel_context_val = { + env_rel_ctx : Context.Rel.t; + env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; +} + +type env = { + env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_named_context : named_context_val; (* section variables *) + env_rel_context : rel_context_val; + env_nb_rel : int; + env_stratification : stratification; + env_typing_flags : typing_flags; + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} + +let empty_named_context_val = { + env_named_ctx = []; + env_named_map = Id.Map.empty; +} + +let empty_rel_context_val = { + env_rel_ctx = []; + env_rel_map = Range.empty; +} + +let empty_env = { + env_globals = { + env_constants = Cmap_env.empty; + env_projections = Cmap_env.empty; + env_inductives = Mindmap_env.empty; + env_modules = MPmap.empty; + env_modtypes = MPmap.empty}; + env_named_context = empty_named_context_val; + env_rel_context = empty_rel_context_val; + env_nb_rel = 0; + env_stratification = { + env_universes = UGraph.initial_universes; + env_engagement = PredicativeSet }; + env_typing_flags = Declareops.safe_flags Conv_oracle.empty; + retroknowledge = Retroknowledge.initial_retroknowledge; + indirect_pterms = Opaqueproof.empty_opaquetab } + + +(* Rel context *) + +let push_rel_context_val d ctx = { + env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx; + env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map; +} + +let match_rel_context_val ctx = match ctx.env_rel_ctx with +| [] -> None +| decl :: rem -> + let (_, lval) = Range.hd ctx.env_rel_map in + let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in + Some (decl, lval, ctx) + +let push_rel d env = + { env with + env_rel_context = push_rel_context_val d env.env_rel_context; + env_nb_rel = env.env_nb_rel + 1 } + +let lookup_rel n env = + try fst (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + +let lookup_rel_val n env = + try snd (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + +let rel_skipn n ctx = { + env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx; + env_rel_map = Range.skipn n ctx.env_rel_map; +} + +let env_of_rel n env = + { env with + env_rel_context = rel_skipn n env.env_rel_context; + env_nb_rel = env.env_nb_rel - n + } + +(* Named context *) + +let push_named_context_val_val d rval ctxt = +(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) + { + env_named_ctx = Context.Named.add d ctxt.env_named_ctx; + env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; + } + +let push_named_context_val d ctxt = + push_named_context_val_val d (ref VKnone) ctxt + +let match_named_context_val c = match c.env_named_ctx with +| [] -> None +| decl :: ctx -> + let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in + let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in + let cval = { env_named_ctx = ctx; env_named_map = map } in + Some (decl, v, cval) + +let map_named_val f ctxt = + let open Context.Named.Declaration in + let fold accu d = + let d' = map_constr f d in + let accu = + if d == d' then accu + else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu + in + (accu, d') + in + let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in + if map == ctxt.env_named_map then ctxt + else { env_named_ctx = ctx; env_named_map = map } + +let push_named d env = + {env with env_named_context = push_named_context_val d env.env_named_context} + +let lookup_named id env = + fst (Id.Map.find id env.env_named_context.env_named_map) + +let lookup_named_val id env = + snd(Id.Map.find id env.env_named_context.env_named_map) + +let lookup_named_ctxt id ctxt = + fst (Id.Map.find id ctxt.env_named_map) + +(* Global constants *) -type env = Pre_env.env +let lookup_constant_key kn env = + Cmap_env.find kn env.env_globals.env_constants + +let lookup_constant kn env = + fst (Cmap_env.find kn env.env_globals.env_constants) + +(* Mutual Inductives *) +let lookup_mind kn env = + fst (Mindmap_env.find kn env.env_globals.env_inductives) + +let lookup_mind_key kn env = + Mindmap_env.find kn env.env_globals.env_inductives -let pre_env env = env -let env_of_pre_env env = env let oracle env = env.env_typing_flags.conv_oracle let set_oracle env o = let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in { env with env_typing_flags } -let empty_named_context_val = empty_named_context_val - -let empty_env = empty_env - let engagement env = env.env_stratification.env_engagement let typing_flags env = env.env_typing_flags @@ -72,15 +252,11 @@ let empty_context env = | _ -> false (* Rel context *) -let lookup_rel = lookup_rel - let evaluable_rel n env = is_local_def (lookup_rel n env) let nb_rel env = env.env_nb_rel -let push_rel = push_rel - let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = @@ -105,24 +281,14 @@ let named_context_of_val c = c.env_named_ctx let ids_of_named_context_val c = Id.Map.domain c.env_named_map -(* [map_named_val f ctxt] apply [f] to the body and the type of - each declarations. - *** /!\ *** [f t] should be convertible with t *) -let map_named_val = map_named_val - let empty_named_context = Context.Named.empty -let push_named = push_named let push_named_context = List.fold_right push_named -let push_named_context_val = push_named_context_val let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named = lookup_named -let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) - let eq_named_context_val c1 c2 = c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2) @@ -181,7 +347,10 @@ let map_universes f env = let s = env.env_stratification in { env with env_stratification = { s with env_universes = f s.env_universes } } - + +let set_universes env u = + { env with env_stratification = { env.env_stratification with env_universes = u } } + let add_constraints c env = if Univ.Constraint.is_empty c then env else map_universes (UGraph.merge_constraints c) env @@ -221,8 +390,6 @@ let set_typing_flags c env = (* Unsafe *) (* Global constants *) -let lookup_constant = lookup_constant - let no_link_info = NotLinked let add_constant_key kn cb linkinfo env = @@ -320,18 +487,12 @@ let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes let lookup_projection cst env = - match (lookup_constant (Projection.constant cst) env).const_proj with - | Some pb -> pb - | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.") + Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - match (lookup_constant cst env).const_proj with - | Some _ -> true - | None -> false + (lookup_constant cst env).const_proj (* Mutual Inductives *) -let lookup_mind = lookup_mind - let polymorphic_ind (mind,i) env = Declareops.inductive_is_polymorphic (lookup_mind mind env) @@ -351,11 +512,18 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn mind_key env = +let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_projections = match mind.mind_record with + | None | Some None -> env.env_globals.env_projections + | Some (Some (id, kns, pbs)) -> + Array.fold_left2 (fun projs kn pb -> + Cmap_env.add kn pb projs) + env.env_globals.env_projections kns pbs + in let new_globals = { env.env_globals with - env_inductives = new_inds } in + env_inductives = new_inds; env_projections = new_projections; } in { env with env_globals = new_globals } let add_mind kn mib env = @@ -468,10 +636,6 @@ type 'types punsafe_type_judgment = { type unsafe_type_judgment = types punsafe_type_judgment -(*s Compilation of global declaration *) - -let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false - exception Hyp_not_found let apply_to_hyp ctxt id f = @@ -530,121 +694,3 @@ let register env field entry = in register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry | field -> register_one env field entry - -(* the Environ.register function syncrhonizes the proactive and reactive - retroknowledge. *) -let dispatch = - - (* subfunction used for static decompilation of int31 (after a vm_compute, - see pretyping/vnorm.ml for more information) *) - let constr_of_int31 = - let nth_digit_plus_one i n = (* calculates the nth (starting with 0) - digit of i and adds 1 to it - (nth_digit_plus_one 1 3 = 2) *) - if Int.equal (i land (1 lsl n)) 0 then - 1 - else - 2 - in - fun ind -> fun digit_ind -> fun tag -> - let array_of_int i = - Array.init 31 (fun n -> mkConstruct - (digit_ind, nth_digit_plus_one i (30-n))) - in - (* We check that no bit above 31 is set to one. This assertion used to - fail in the VM, and led to conversion tests failing at Qed. *) - assert (Int.equal (tag lsr 31) 0); - mkApp(mkConstruct(ind, 1), array_of_int tag) - in - - (* subfunction which dispatches the compiling information of an - int31 operation which has a specific vm instruction (associates - it to the name of the coq definition in the reactive retroknowledge) *) - let int31_op n op prim kn = - { empty_reactive_info with - vm_compiling = Some (Clambda.compile_prim n op kn); - native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); - } - in - -fun rk value field -> - (* subfunction which shortens the (very common) dispatch of operations *) - let int31_op_from_const n op prim = - match kind value with - | Const kn -> int31_op n op prim kn - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") - in - let int31_binop_from_const op prim = int31_op_from_const 2 op prim in - let int31_unop_from_const op prim = int31_op_from_const 1 op prim in - match field with - | KInt31 (grp, Int31Type) -> - let int31bit = - (* invariant : the type of bits is registered, otherwise the function - would raise Not_found. The invariant is enforced in safe_typing.ml *) - match field with - | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) - | _ -> anomaly ~label:"Environ.register" - (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") - in - let i31bit_type = - match kind int31bit with - | Ind (i31bit_type,_) -> i31bit_type - | _ -> anomaly ~label:"Environ.register" - (Pp.str "Int31Bits should be an inductive type.") - in - let int31_decompilation = - match kind value with - | Ind (i31t,_) -> - constr_of_int31 i31t i31bit_type - | _ -> anomaly ~label:"Environ.register" - (Pp.str "should be an inductive type.") - in - { empty_reactive_info with - vm_decompile_const = Some int31_decompilation; - vm_before_match = Some Clambda.int31_escape_before_match; - native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); - } - | KInt31 (_, Int31Constructor) -> - { empty_reactive_info with - vm_constant_static = Some Clambda.compile_structured_int31; - vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; - native_constant_static = Some Nativelambda.compile_static_int31; - native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; - } - | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 - CPrimitives.Int31add - | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 - CPrimitives.Int31addc - | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 - CPrimitives.Int31addcarryc - | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 - CPrimitives.Int31sub - | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 - CPrimitives.Int31subc - | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const - Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc - | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 - CPrimitives.Int31mul - | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 - CPrimitives.Int31mulc - | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 - CPrimitives.Int31div21 - | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 - CPrimitives.Int31diveucl - | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 - CPrimitives.Int31addmuldiv - | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 - CPrimitives.Int31compare - | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 - CPrimitives.Int31head0 - | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 - CPrimitives.Int31tail0 - | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 - CPrimitives.Int31lor - | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 - CPrimitives.Int31land - | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 - CPrimitives.Int31lxor - | _ -> empty_reactive_info - -let _ = Hook.set Retroknowledge.dispatch_hook dispatch diff --git a/kernel/environ.mli b/kernel/environ.mli index 4e6ac1e725..8928b32f1b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -28,16 +28,61 @@ open Declarations - a set of universe constraints - a flag telling if Set is, can be, or cannot be set impredicative *) +type lazy_val + +val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit +val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option +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 + +type constant_key = constant_body * (link_info ref * key) + +type mind_key = mutual_inductive_body * link_info ref + +type globals = { + env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; + env_inductives : mind_key Mindmap_env.t; + env_modules : module_body MPmap.t; + env_modtypes : module_type_body MPmap.t +} + +type stratification = { + env_universes : UGraph.t; + env_engagement : engagement +} + +type named_context_val = private { + env_named_ctx : Context.Named.t; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} + +type rel_context_val = private { + env_rel_ctx : Context.Rel.t; + env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; +} + +type env = private { + env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_named_context : named_context_val; (* section variables *) + env_rel_context : rel_context_val; + env_nb_rel : int; + env_stratification : stratification; + env_typing_flags : typing_flags; + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} - - -type env -val pre_env : env -> Pre_env.env -val env_of_pre_env : Pre_env.env -> env val oracle : env -> Conv_oracle.oracle val set_oracle : env -> Conv_oracle.oracle -> env -type named_context_val val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env @@ -70,7 +115,9 @@ val push_rec_types : rec_declaration -> env -> env (** Looks up in the context of local vars referred by indice ([rel_context]) raises [Not_found] if the index points out of the context *) val lookup_rel : int -> env -> Context.Rel.Declaration.t +val lookup_rel_val : int -> env -> lazy_val val evaluable_rel : int -> env -> bool +val env_of_rel : int -> env -> env (** {6 Recurrence on [rel_context] } *) @@ -102,7 +149,8 @@ val push_named_context_val : raises [Not_found] if the Id.t is not found *) val lookup_named : variable -> env -> Context.Named.Declaration.t -val lookup_named_val : variable -> named_context_val -> Context.Named.Declaration.t +val lookup_named_val : variable -> env -> lazy_val +val lookup_named_ctxt : variable -> named_context_val -> Context.Named.Declaration.t val evaluable_named : variable -> env -> bool val named_type : variable -> env -> types val named_body : variable -> env -> constr option @@ -112,6 +160,8 @@ val named_body : variable -> env -> constr option val fold_named_context : (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a +val set_universes : env -> UGraph.t -> env + (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a @@ -129,8 +179,9 @@ val pop_rel_context : int -> env -> env {6 Add entries to global environment } *) val add_constant : Constant.t -> constant_body -> env -> env -val add_constant_key : Constant.t -> constant_body -> Pre_env.link_info -> +val add_constant_key : Constant.t -> constant_body -> link_info -> env -> env +val lookup_constant_key : Constant.t -> env -> constant_key (** Looks up in the context of global constant names raises [Not_found] if the required path is not found *) @@ -168,11 +219,12 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option (** {6 Primitive projections} *) -val lookup_projection : Names.projection -> env -> projection_body +val lookup_projection : Names.Projection.t -> env -> projection_body val is_projection : Constant.t -> env -> bool (** {5 Inductive types } *) -val add_mind_key : MutInd.t -> Pre_env.mind_key -> env -> env +val lookup_mind_key : MutInd.t -> env -> mind_key +val add_mind_key : MutInd.t -> mind_key -> env -> env val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names @@ -251,10 +303,6 @@ type 'types punsafe_type_judgment = { type unsafe_type_judgment = types punsafe_type_judgment -(** {6 Compilation of global declaration } *) - -val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option - exception Hyp_not_found (** [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and @@ -264,7 +312,7 @@ val apply_to_hyp : named_context_val -> variable -> (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) -> named_context_val -val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val +val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val @@ -278,4 +326,4 @@ val registered : env -> field -> bool val register : env -> field -> Retroknowledge.entry -> env (** Native compiler *) -val no_link_info : Pre_env.link_info +val no_link_info : link_info diff --git a/kernel/esubst.ml b/kernel/esubst.ml index a11a0dc00c..4b8edf63fa 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -19,6 +19,8 @@ open Util (*********************) (* Explicit lifts and basic operations *) +(* Invariant to preserve in this module: no lift contains two consecutive + [ELSHFT] nor two consecutive [ELLFT]. *) type lift = | ELID | ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *) @@ -28,15 +30,15 @@ type lift = let el_id = ELID (* compose a relocation of magnitude n *) -let rec el_shft_rec n = function - | ELSHFT(el,k) -> el_shft_rec (k+n) el +let el_shft_rec n = function + | ELSHFT(el,k) -> ELSHFT(el,k+n) | el -> ELSHFT(el,n) let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el (* cross n binders *) -let rec el_liftn_rec n = function +let el_liftn_rec n = function | ELID -> ELID - | ELLFT(k,el) -> el_liftn_rec (n+k) el + | ELLFT(k,el) -> ELLFT(n+k, el) | el -> ELLFT(n, el) let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el @@ -138,7 +140,7 @@ let rec comp mk_cl s1 s2 = | ESID _, _ -> s2 | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2) | _, CONS(x,s') -> - CONS(CArray.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s') + CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s') | CONS(x,s), SHIFT(k,s') -> let lg = Array.length x in if k == lg then comp mk_cl s s' diff --git a/kernel/esubst.mli b/kernel/esubst.mli index b82d6fdf02..a674c425a7 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -56,7 +56,11 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs (** {6 Compact representation } *) (** Compact representation of explicit relocations - [ELSHFT(l,n)] == lift of [n], then apply [lift l]. - - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *) + - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. + + Invariant ensured by the private flag: no lift contains two consecutive + [ELSHFT] nor two consecutive [ELLFT]. +*) type lift = private | ELID | ELSHFT of lift * int diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9bed598bb7..090acdf16e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -803,9 +803,7 @@ let rec subterm_specif renv stack t = (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p renv.env in let n = pb.proj_arg in spec_of_tree (List.nth wf_args n) | Dead_code -> Dead_code diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 370185a721..50713b9579 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -22,15 +22,17 @@ CPrimitives Declareops Retroknowledge Conv_oracle -Pre_env +Environ +CClosure +Reduction Clambda Nativelambda Cbytegen Nativecode Nativelib -Environ -CClosure -Reduction +Csymtable +Vm +Vconv Nativeconv Type_errors Modops @@ -43,6 +45,3 @@ Subtyping Mod_typing Nativelibrary Safe_typing -Vm -Csymtable -Vconv diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 9c2fa05465..0027ebecfc 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -367,7 +367,7 @@ let rec map_kn f f' c = in let p' = func p in let ct' = func ct in - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (ci.ci_ind==ci_ind && p'==p && l'==l && ct'==ct)then c else @@ -396,21 +396,21 @@ let rec map_kn f f' c = else mkLetIn (na, b', t', ct') | App (ct,l) -> let ct' = func ct in - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (ct'== ct && l'==l) then c else mkApp (ct',l') | Evar (e,l) -> - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (l'==l) then c else mkEvar (e,l') | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap func tl in - let bl' = Array.smartmap func bl in + let tl' = Array.Smart.map func tl in + let bl' = Array.Smart.map func bl in if (bl == bl'&& tl == tl') then c else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.smartmap func tl in - let bl' = Array.smartmap func bl in + let tl' = Array.Smart.map func tl in + let bl' = Array.Smart.map func bl in if (bl == bl'&& tl == tl') then c else mkCoFix (ln,(lna,tl',bl')) | _ -> c diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 1baab7c98c..d63dc057b4 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -120,7 +120,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = const_body = def; const_universes = univs ; const_body_code = Option.map Cemitcodes.from_val - (compile_constant_body env' cb.const_universes def) } + (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else diff --git a/kernel/modops.ml b/kernel/modops.ml index bbf160db21..2038171183 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -130,10 +130,10 @@ let destr_nofunctor = function |NoFunctor a -> a |MoreFunctor _ -> error_is_a_functor () -let rec functor_smartmap fty f0 funct = match funct with +let rec functor_smart_map fty f0 funct = match funct with |MoreFunctor (mbid,ty,e) -> let ty' = fty ty in - let e' = functor_smartmap fty f0 e in + let e' = functor_smart_map fty f0 e in if ty==ty' && e==e' then funct else MoreFunctor (mbid,ty',e') |NoFunctor a -> let a' = f0 a in if a==a' then funct else NoFunctor a' @@ -197,7 +197,7 @@ let rec subst_structure sub do_delta sign = let mtb' = subst_modtype sub do_delta mtb in if mtb==mtb' then orig else (l,SFBmodtype mtb') in - List.smartmap subst_body sign + List.Smart.map subst_body sign and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = fun is_mod sub subst_impl do_delta mb -> @@ -210,7 +210,7 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> in let ty' = subst_signature sub do_delta ty in let me' = subst_impl sub me in - let aty' = Option.smartmap (subst_expression sub id_delta) aty in + let aty' = Option.Smart.map (subst_expression sub id_delta) aty in let delta' = do_delta mb.mod_delta sub in if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta then mb @@ -245,12 +245,12 @@ and subst_expr sub do_delta seb = match seb with if meb==meb' && wdb==wdb' then seb else MEwith(meb',wdb') and subst_expression sub do_delta = - functor_smartmap + functor_smart_map (subst_modtype sub do_delta) (subst_expr sub do_delta) and subst_signature sub do_delta = - functor_smartmap + functor_smart_map (subst_modtype sub do_delta) (subst_structure sub do_delta) @@ -595,13 +595,13 @@ and clean_field l field = match field with if mb==mb' then field else (lab,SFBmodule mb') |_ -> field -and clean_structure l = List.smartmap (clean_field l) +and clean_structure l = List.Smart.map (clean_field l) and clean_signature l = - functor_smartmap (clean_module_type l) (clean_structure l) + functor_smart_map (clean_module_type l) (clean_structure l) and clean_expression l = - functor_smartmap (clean_module_type l) (fun me -> me) + functor_smart_map (clean_module_type l) (fun me -> me) let rec collect_mbid l sign = match sign with |MoreFunctor (mbid,ty,m) -> diff --git a/kernel/modops.mli b/kernel/modops.mli index cb41a5123a..ac76d28cf3 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -52,7 +52,7 @@ val add_module : module_body -> env -> env (** same as add_module, but for a module whose native code has been linked by the native compiler. The linking information is updated. *) -val add_linked_module : module_body -> Pre_env.link_info -> env -> env +val add_linked_module : module_body -> link_info -> env -> env (** same, for a module type *) val add_module_type : ModPath.t -> module_type_body -> env -> env diff --git a/kernel/names.ml b/kernel/names.ml index a3aa71f24f..597061278d 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -701,22 +701,6 @@ end module Constrmap = Map.Make(ConstructorOrdered) module Constrmap_env = Map.Make(ConstructorOrdered_env) -type global_reference = - | VarRef of variable (** A reference to the section-context. *) - | ConstRef of Constant.t (** A reference to the environment. *) - | IndRef of inductive (** A reference to an inductive type. *) - | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) - -(* Better to have it here that in closure, since used in grammar.cma *) -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -let eq_egr e1 e2 = match e1, e2 with - EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 - | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 - | _, _ -> false - (** {6 Hash-consing of name objects } *) module Hind = Hashcons.Make( @@ -776,55 +760,8 @@ let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 (*******************************************************************) (** Compatibility layers *) -(** Backward compatibility for [Id] *) - -type identifier = Id.t - -let id_eq = Id.equal -let id_ord = Id.compare -let string_of_id = Id.to_string -let id_of_string = Id.of_string - -module Idset = Id.Set -module Idmap = Id.Map -module Idpred = Id.Pred - -(** Compatibility layer for [Name] *) - -let name_eq = Name.equal - -(** Compatibility layer for [DirPath] *) - -type dir_path = DirPath.t -let dir_path_ord = DirPath.compare -let dir_path_eq = DirPath.equal -let make_dirpath = DirPath.make -let repr_dirpath = DirPath.repr -let empty_dirpath = DirPath.empty -let is_empty_dirpath = DirPath.is_empty -let string_of_dirpath = DirPath.to_string -let initial_dir = DirPath.initial - -(** Compatibility layer for [MBId] *) - type mod_bound_id = MBId.t -let mod_bound_id_ord = MBId.compare -let mod_bound_id_eq = MBId.equal -let make_mbid = MBId.make -let repr_mbid = MBId.repr -let debug_string_of_mbid = MBId.debug_to_string -let string_of_mbid = MBId.to_string -let id_of_mbid = MBId.to_id - -(** Compatibility layer for [Label] *) - -type label = Id.t -let mk_label = Label.make -let string_of_label = Label.to_string -let pr_label = Label.print -let id_of_label = Label.to_id -let label_of_id = Label.of_id -let eq_label = Label.equal +let eq_constant_key = Constant.UserOrd.equal (** Compatibility layer for [ModPath] *) @@ -832,32 +769,13 @@ type module_path = ModPath.t = | MPfile of DirPath.t | MPbound of MBId.t | MPdot of module_path * Label.t -let check_bound_mp = ModPath.is_bound -let string_of_mp = ModPath.to_string -let mp_ord = ModPath.compare -let mp_eq = ModPath.equal -let initial_path = ModPath.initial - -(** Compatibility layer for [KerName] *) - -type kernel_name = KerName.t -let make_kn = KerName.make -let repr_kn = KerName.repr -let modpath = KerName.modpath -let label = KerName.label -let string_of_kn = KerName.to_string -let pr_kn = KerName.print -let kn_ord = KerName.compare (** Compatibility layer for [Constant] *) -type constant = Constant.t - +module Projection = +struct + type t = Constant.t * bool -module Projection = -struct - type t = constant * bool - let make c b = (c, b) let constant = fst @@ -904,39 +822,39 @@ end type projection = Projection.t -let constant_of_kn = Constant.make1 -let constant_of_kn_equiv = Constant.make -let make_con = Constant.make3 -let repr_con = Constant.repr3 -let canonical_con = Constant.canonical -let user_con = Constant.user -let con_label = Constant.label -let con_modpath = Constant.modpath -let eq_constant = Constant.equal -let eq_constant_key = Constant.UserOrd.equal -let con_ord = Constant.CanOrd.compare -let con_user_ord = Constant.UserOrd.compare -let string_of_con = Constant.to_string -let pr_con = Constant.print -let debug_string_of_con = Constant.debug_to_string -let debug_pr_con = Constant.debug_print -let con_with_label = Constant.change_label - -(** Compatibility layer for [MutInd] *) - -type mutual_inductive = MutInd.t -let mind_of_kn = MutInd.make1 -let mind_of_kn_equiv = MutInd.make -let make_mind = MutInd.make3 -let canonical_mind = MutInd.canonical -let user_mind = MutInd.user -let repr_mind = MutInd.repr3 -let mind_label = MutInd.label -let mind_modpath = MutInd.modpath -let eq_mind = MutInd.equal -let mind_ord = MutInd.CanOrd.compare -let mind_user_ord = MutInd.UserOrd.compare -let string_of_mind = MutInd.to_string -let pr_mind = MutInd.print -let debug_string_of_mind = MutInd.debug_to_string -let debug_pr_mind = MutInd.debug_print +module GlobRef = struct + + type t = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + + let equal gr1 gr2 = + gr1 == gr2 || match gr1,gr2 with + | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2 + | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 + | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 + | VarRef v1, VarRef v2 -> Id.equal v1 v2 + | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false + +end + +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] + +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + +(* Better to have it here that in closure, since used in grammar.cma *) +let eq_egr e1 e2 = match e1, e2 with + EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 + | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 + | _, _ -> false + +(** Located identifiers and objects with syntax. *) + +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t diff --git a/kernel/names.mli b/kernel/names.mli index ffd96781b3..4eb5adb62f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -500,21 +500,6 @@ val constructor_user_hash : constructor -> int val constructor_syntactic_ord : constructor -> constructor -> int val constructor_syntactic_hash : constructor -> int -(** {6 Global reference is a kernel side type for all references together } *) -type global_reference = - | VarRef of variable (** A reference to the section-context. *) - | ConstRef of Constant.t (** A reference to the environment. *) - | IndRef of inductive (** A reference to an inductive type. *) - | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) - -(** Better to have it here that in Closure, since required in grammar.cma *) -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -val eq_egr : evaluable_global_reference -> evaluable_global_reference - -> bool - (** {6 Hash-consing } *) val hcons_con : Constant.t -> Constant.t @@ -547,120 +532,14 @@ val eq_constant_key : Constant.t -> Constant.t -> bool (** equalities on constant and inductive names (for the checker) *) val eq_con_chk : Constant.t -> Constant.t -> bool +[@@ocaml.deprecated "Same as [Constant.UserOrd.equal]."] + val eq_ind_chk : inductive -> inductive -> bool (** {6 Deprecated functions. For backward compatibility.} *) -(** {5 Identifiers} *) - -type identifier = Id.t -[@@ocaml.deprecated "Alias for [Id.t]"] - -val string_of_id : Id.t -> string -[@@ocaml.deprecated "Same as [Id.to_string]."] - -val id_of_string : string -> Id.t -[@@ocaml.deprecated "Same as [Id.of_string]."] - -val id_ord : Id.t -> Id.t -> int -[@@ocaml.deprecated "Same as [Id.compare]."] - -val id_eq : Id.t -> Id.t -> bool -[@@ocaml.deprecated "Same as [Id.equal]."] - -module Idset : Set.S with type elt = Id.t and type t = Id.Set.t -[@@ocaml.deprecated "Same as [Id.Set]."] - -module Idpred : Predicate.S with type elt = Id.t and type t = Id.Pred.t -[@@ocaml.deprecated "Same as [Id.Pred]."] - -module Idmap : module type of Id.Map -[@@ocaml.deprecated "Same as [Id.Map]."] - -(** {5 Directory paths} *) - -type dir_path = DirPath.t -[@@ocaml.deprecated "Alias for [DirPath.t]."] - -val dir_path_ord : DirPath.t -> DirPath.t -> int -[@@ocaml.deprecated "Same as [DirPath.compare]."] - -val dir_path_eq : DirPath.t -> DirPath.t -> bool -[@@ocaml.deprecated "Same as [DirPath.equal]."] - -val make_dirpath : module_ident list -> DirPath.t -[@@ocaml.deprecated "Same as [DirPath.make]."] - -val repr_dirpath : DirPath.t -> module_ident list -[@@ocaml.deprecated "Same as [DirPath.repr]."] - -val empty_dirpath : DirPath.t -[@@ocaml.deprecated "Same as [DirPath.empty]."] - -val is_empty_dirpath : DirPath.t -> bool -[@@ocaml.deprecated "Same as [DirPath.is_empty]."] - -val string_of_dirpath : DirPath.t -> string -[@@ocaml.deprecated "Same as [DirPath.to_string]."] - -val initial_dir : DirPath.t -[@@ocaml.deprecated "Same as [DirPath.initial]."] - -(** {5 Labels} *) - -type label = Label.t -[@@ocaml.deprecated "Same as [Label.t]."] -(** Alias type *) - -val mk_label : string -> Label.t -[@@ocaml.deprecated "Same as [Label.make]."] - -val string_of_label : Label.t -> string -[@@ocaml.deprecated "Same as [Label.to_string]."] - -val pr_label : Label.t -> Pp.t -[@@ocaml.deprecated "Same as [Label.print]."] - -val label_of_id : Id.t -> Label.t -[@@ocaml.deprecated "Same as [Label.of_id]."] - -val id_of_label : Label.t -> Id.t -[@@ocaml.deprecated "Same as [Label.to_id]."] - -val eq_label : Label.t -> Label.t -> bool -[@@ocaml.deprecated "Same as [Label.equal]."] - -(** {5 Unique bound module names} *) - type mod_bound_id = MBId.t -(** Alias type. *) - -val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int -[@@ocaml.deprecated "Same as [MBId.compare]."] - -val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool -[@@ocaml.deprecated "Same as [MBId.equal]."] - -val make_mbid : DirPath.t -> Id.t -> mod_bound_id -[@@ocaml.deprecated "Same as [MBId.make]."] - -val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t -[@@ocaml.deprecated "Same as [MBId.repr]."] - -val id_of_mbid : mod_bound_id -> Id.t -[@@ocaml.deprecated "Same as [MBId.to_id]."] - -val string_of_mbid : mod_bound_id -> string -[@@ocaml.deprecated "Same as [MBId.to_string]."] - -val debug_string_of_mbid : mod_bound_id -> string -[@@ocaml.deprecated "Same as [MBId.debug_to_string]."] - -(** {5 Names} *) - -val name_eq : Name.t -> Name.t -> bool -[@@ocaml.deprecated "Same as [Name.equal]."] - +[@@ocaml.deprecated "Same as [MBId.t]."] (** {5 Module paths} *) type module_path = ModPath.t = @@ -669,52 +548,6 @@ type module_path = ModPath.t = | MPdot of ModPath.t * Label.t [@@ocaml.deprecated "Alias type"] -val mp_ord : ModPath.t -> ModPath.t -> int -[@@ocaml.deprecated "Same as [ModPath.compare]."] - -val mp_eq : ModPath.t -> ModPath.t -> bool -[@@ocaml.deprecated "Same as [ModPath.equal]."] - -val check_bound_mp : ModPath.t -> bool -[@@ocaml.deprecated "Same as [ModPath.is_bound]."] - -val string_of_mp : ModPath.t -> string -[@@ocaml.deprecated "Same as [ModPath.to_string]."] - -val initial_path : ModPath.t -[@@ocaml.deprecated "Same as [ModPath.initial]."] - -(** {5 Kernel names} *) - -type kernel_name = KerName.t -[@@ocaml.deprecated "Alias type"] - -val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t -[@@ocaml.deprecated "Same as [KerName.make]."] - -val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [KerName.repr]."] - -val modpath : KerName.t -> ModPath.t -[@@ocaml.deprecated "Same as [KerName.modpath]."] - -val label : KerName.t -> Label.t -[@@ocaml.deprecated "Same as [KerName.label]."] - -val string_of_kn : KerName.t -> string -[@@ocaml.deprecated "Same as [KerName.to_string]."] - -val pr_kn : KerName.t -> Pp.t -[@@ocaml.deprecated "Same as [KerName.print]."] - -val kn_ord : KerName.t -> KerName.t -> int -[@@ocaml.deprecated "Same as [KerName.compare]."] - -(** {5 Constant names} *) - -type constant = Constant.t -[@@ocaml.deprecated "Alias type"] - module Projection : sig type t @@ -745,101 +578,36 @@ module Projection : sig end type projection = Projection.t +[@@ocaml.deprecated "Alias for [Projection.t]"] -val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make]"] - -val constant_of_kn : KerName.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make1]"] - -val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make3]"] - -val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [Constant.repr3]"] - -val user_con : Constant.t -> KerName.t -[@@ocaml.deprecated "Same as [Constant.user]"] - -val canonical_con : Constant.t -> KerName.t -[@@ocaml.deprecated "Same as [Constant.canonical]"] - -val con_modpath : Constant.t -> ModPath.t -[@@ocaml.deprecated "Same as [Constant.modpath]"] - -val con_label : Constant.t -> Label.t -[@@ocaml.deprecated "Same as [Constant.label]"] - -val eq_constant : Constant.t -> Constant.t -> bool -[@@ocaml.deprecated "Same as [Constant.equal]"] - -val con_ord : Constant.t -> Constant.t -> int -[@@ocaml.deprecated "Same as [Constant.CanOrd.compare]"] - -val con_user_ord : Constant.t -> Constant.t -> int -[@@ocaml.deprecated "Same as [Constant.UserOrd.compare]"] - -val con_with_label : Constant.t -> Label.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.change_label]"] - -val string_of_con : Constant.t -> string -[@@ocaml.deprecated "Same as [Constant.to_string]"] - -val pr_con : Constant.t -> Pp.t -[@@ocaml.deprecated "Same as [Constant.print]"] - -val debug_pr_con : Constant.t -> Pp.t -[@@ocaml.deprecated "Same as [Constant.debug_print]"] - -val debug_string_of_con : Constant.t -> string -[@@ocaml.deprecated "Same as [Constant.debug_to_string]"] - -(** {5 Mutual Inductive names} *) - -type mutual_inductive = MutInd.t -[@@ocaml.deprecated "Alias type"] - -val mind_of_kn : KerName.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make1]"] - -val mind_of_kn_equiv : KerName.t -> KerName.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make]"] - -val make_mind : ModPath.t -> DirPath.t -> Label.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make3]"] - -val user_mind : MutInd.t -> KerName.t -[@@ocaml.deprecated "Same as [MutInd.user]"] - -val canonical_mind : MutInd.t -> KerName.t -[@@ocaml.deprecated "Same as [MutInd.canonical]"] - -val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [MutInd.repr3]"] +(** {6 Global reference is a kernel side type for all references together } *) -val eq_mind : MutInd.t -> MutInd.t -> bool -[@@ocaml.deprecated "Same as [MutInd.equal]"] +(* XXX: Should we define GlobRefCan GlobRefUser? *) +module GlobRef : sig -val mind_ord : MutInd.t -> MutInd.t -> int -[@@ocaml.deprecated "Same as [MutInd.CanOrd.compare]"] + type t = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) -val mind_user_ord : MutInd.t -> MutInd.t -> int -[@@ocaml.deprecated "Same as [MutInd.UserOrd.compare]"] + val equal : t -> t -> bool -val mind_label : MutInd.t -> Label.t -[@@ocaml.deprecated "Same as [MutInd.label]"] +end -val mind_modpath : MutInd.t -> ModPath.t -[@@ocaml.deprecated "Same as [MutInd.modpath]"] +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] -val string_of_mind : MutInd.t -> string -[@@ocaml.deprecated "Same as [MutInd.to_string]"] +(** Better to have it here that in Closure, since required in grammar.cma *) +(* XXX: Move to a module *) +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t -val pr_mind : MutInd.t -> Pp.t -[@@ocaml.deprecated "Same as [MutInd.print]"] +val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool -val debug_pr_mind : MutInd.t -> Pp.t -[@@ocaml.deprecated "Same as [MutInd.debug_print]"] +(** Located identifiers and objects with syntax. *) -val debug_string_of_mind : MutInd.t -> string -[@@ocaml.deprecated "Same as [MutInd.debug_to_string]"] +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c82d982b4b..8257dc8b84 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -16,7 +16,7 @@ open Util open Nativevalues open Nativeinstr open Nativelambda -open Pre_env +open Environ [@@@ocaml.warning "-32-37"] @@ -53,7 +53,7 @@ type gname = | Gind of string * inductive (* prefix, inductive name *) | Gconstruct of string * constructor (* prefix, constructor name *) | Gconstant of string * Constant.t (* prefix, constant name *) - | Gproj of string * Constant.t (* prefix, constant name *) + | Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *) | Gcase of Label.t option * int | Gpred of Label.t option * int | Gfixtype of Label.t option * int @@ -108,7 +108,7 @@ let gname_hash gn = match gn with | Ginternal s -> combinesmall 9 (String.hash s) | Grel i -> combinesmall 10 (Int.hash i) | Gnamed id -> combinesmall 11 (Id.hash id) -| Gproj (s, p) -> combinesmall 12 (combine (String.hash s) (Constant.hash p)) +| Gproj (s, p, i) -> combinesmall 12 (combine (String.hash s) (combine (ind_hash p) i)) let case_ctr = ref (-1) @@ -152,6 +152,7 @@ type symbol = | SymbMeta of metavariable | SymbEvar of Evar.t | SymbLevel of Univ.Level.t + | SymbProj of (inductive * int) let dummy_symb = SymbValue (dummy_value ()) @@ -166,6 +167,7 @@ let eq_symbol sy1 sy2 = | 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 | _, _ -> false let hash_symbol symb = @@ -179,6 +181,7 @@ let hash_symbol symb = | 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) module HashedTypeSymbol = struct type t = symbol @@ -241,6 +244,11 @@ let get_level tbl i = | SymbLevel u -> u | _ -> anomaly (Pp.str "get_level failed.") +let get_proj tbl i = + match tbl.(i) with + | SymbProj p -> p + | _ -> anomaly (Pp.str "get_proj failed.") + let push_symbol x = try HashtblSymbol.find symb_tbl x with Not_found -> @@ -885,6 +893,10 @@ let get_level_code i = MLapp (MLglobal (Ginternal "get_level"), [|MLglobal symbols_tbl_name; MLint i|]) +let get_proj_code i = + MLapp (MLglobal (Ginternal "get_proj"), + [|MLglobal symbols_tbl_name; MLint i|]) + type rlist = | Rnil | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' @@ -1070,7 +1082,7 @@ let ml_of_instance instance u = | Lconst (prefix, (c, u)) -> let args = ml_of_instance env.env_univ u in mkMLapp (MLglobal(Gconstant (prefix, c))) args - | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c)) + | Lproj (prefix, ind, i) -> MLglobal(Gproj (prefix, ind, i)) | Lprim _ -> let decl,cond,paux = extract_prim (ml_of_lam env l) t in compile_prim decl cond paux @@ -1544,8 +1556,8 @@ let string_of_gname g = Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1) | Gconstant (prefix, c) -> Format.sprintf "%sconst_%s" prefix (string_of_con c) - | Gproj (prefix, c) -> - Format.sprintf "%sproj_%s" prefix (string_of_con c) + | Gproj (prefix, (mind, n), i) -> + Format.sprintf "%sproj_%s_%i_%i" prefix (string_of_mind mind) n i | Gcase (l,i) -> Format.sprintf "case_%s_%i" (string_of_label_def l) i | Gpred (l,i) -> @@ -1837,7 +1849,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = and compile_rel env sigma univ auxdefs n = let open Context.Rel.Declaration in - let decl = Pre_env.lookup_rel n env in + let decl = lookup_rel n env in let n = List.length env.env_rel_context.env_rel_ctx - n in match decl with | LocalDef (_,t,_) -> @@ -1858,8 +1870,6 @@ and compile_named env sigma univ auxdefs id = Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs let compile_constant env sigma prefix ~interactive con cb = - match cb.const_proj with - | None -> let no_univs = match cb.const_universes with | Monomorphic_const _ -> true @@ -1903,38 +1913,6 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix end - | Some pb -> - let mind = pb.proj_ind in - let ind = (mind,0) in - let mib = lookup_mind mind env in - let oib = mib.mind_packets.(0) in - let tbl = oib.mind_reloc_tbl in - (* Building info *) - let prefix = get_mind_prefix env mind in - let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; - ci_cstr_nargs = [|0|]; - ci_cstr_ndecls = [||] (*FIXME*); - ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in - let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci; - asw_reloc = tbl; asw_finite = true } in - let c_uid = fresh_lname Anonymous in - let cf_uid = fresh_lname Anonymous in - let _, arity = tbl.(0) in - let ci_uid = fresh_lname Anonymous in - let cargs = Array.init arity - (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) - in - let i = push_symbol (SymbConst con) in - let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in - let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in - let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in - let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in - let gn = Gproj ("",con) in - let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in - let arg = fargs.(pb.proj_npars) in - Glet(Gconstant ("", con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal - arg|]))):: - [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) @@ -1961,10 +1939,12 @@ let arg_name = Name (Id.of_string "arg") let compile_mind prefix ~interactive mb mind stack = let u = Declareops.inductive_polymorphic_context mb in + (** Generate data for every block *) let f i stack ob = - let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in - let j = push_symbol (SymbInd (mind,i)) in - let name = Gind ("", (mind, i)) in + let ind = (mind, i) in + let gtype = Gtype(ind, Array.map snd ob.mind_reloc_tbl) in + let j = push_symbol (SymbInd ind) in + let name = Gind ("", ind) in let accu = let args = if Int.equal (Univ.AUContext.size u) 0 then @@ -1978,12 +1958,41 @@ let compile_mind prefix ~interactive mb mind stack = Array.init nparams (fun i -> {lname = param_name; luid = i}) in let add_construct j acc (_,arity) = let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in - let c = (mind,i), (j+1) in + let c = ind, (j+1) in Glet(Gconstruct ("", c), mkMLlam (Array.append params args) (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in - Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl + let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in + let add_proj j acc pb = + let tbl = ob.mind_reloc_tbl in + (* Building info *) + let ci = { ci_ind = ind; ci_npar = nparams; + ci_cstr_nargs = [|0|]; + ci_cstr_ndecls = [||] (*FIXME*); + ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in + let asw = { asw_ind = ind; asw_prefix = ""; asw_ci = ci; + asw_reloc = tbl; asw_finite = true } in + let c_uid = fresh_lname Anonymous in + let cf_uid = fresh_lname Anonymous in + let _, arity = tbl.(0) in + let ci_uid = fresh_lname Anonymous in + let cargs = Array.init arity + (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) + in + let i = push_symbol (SymbProj (ind, j)) in + let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in + let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in + let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in + let gn = Gproj ("", (pb.proj_ind, j), pb.proj_arg) in + Glet (gn, mkMLlam [|c_uid|] code) :: acc + in + let projs = match mb.mind_record with + | None | Some None -> [] + | Some (Some (id, kns, pbs)) -> Array.fold_left_i add_proj [] pbs + in + projs @ constructors @ gtype :: accu :: stack in Array.fold_left_i f stack mb.mind_packets @@ -2016,24 +2025,22 @@ let compile_mind_deps env prefix ~interactive (* This function compiles all necessary dependencies of t, and generates code in reverse order, as well as linking information updates *) -let rec compile_deps env sigma prefix ~interactive init t = +let compile_deps env sigma prefix ~interactive init t = + let rec aux env lvl init t = match kind t with | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive 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 - || (Cmap_env.mem c const_updates) - then init - else + 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 + || (Cmap_env.mem c const_updates) + then init + else let comp_stack, (mind_updates, const_updates) = - match cb.const_proj, cb.const_body with - | None, Def t -> - compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) - | Some pb, _ -> - let mind = pb.proj_ind in - compile_mind_deps env prefix ~interactive init mind + match cb.const_body with + | Def t -> + aux env lvl init (Mod_subst.force_constr t) | _ -> init in let code, name = @@ -2044,13 +2051,32 @@ let rec compile_deps env sigma prefix ~interactive init t = comp_stack, (mind_updates, const_updates) | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> - let term = mkApp (mkConst (Projection.constant p), [|c|]) in - compile_deps env sigma prefix ~interactive init term + let pb = lookup_projection p env in + let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in + aux env lvl init c | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in - Constr.fold (compile_deps env sigma prefix ~interactive) init t - | _ -> Constr.fold (compile_deps env sigma prefix ~interactive) init t + fold_constr_with_binders succ (aux env) lvl init t + | Var id -> + let open Context.Named.Declaration in + begin match lookup_named id env with + | LocalDef (_,t,_) -> + aux env lvl init t + | _ -> init + end + | Rel n when n > lvl -> + let open Context.Rel.Declaration in + let decl = lookup_rel n env in + let env = env_of_rel n env in + begin match decl with + | LocalDef (_,t,_) -> + aux env lvl init t + | LocalAssum _ -> init + end + | _ -> fold_constr_with_binders succ (aux env) lvl init t + in + aux env 0 init t let compile_constant_field env prefix con acc cb = let (gl, _) = diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 4b23cc5f8b..684983a876 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -10,7 +10,7 @@ open Names open Constr open Declarations -open Pre_env +open Environ open Nativelambda (** This file defines the mllambda code generation phase of the native @@ -50,6 +50,8 @@ val get_evar : symbols -> int -> Evar.t val get_level : symbols -> int -> Univ.Level.t +val get_proj : symbols -> int -> inductive * int + val get_symbols : unit -> symbols type code_location_update diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c71f746bec..e97dbd0d67 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -114,8 +114,8 @@ and conv_atom env pb lvl a1 a2 cu = let cu = conv_val env CONV lvl d1 d2 cu in let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu - | Aproj(p1,ac1), Aproj(p2,ac2) -> - if not (Constant.equal p1 p2) then raise NotConvertible + | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) -> + if not (eq_ind 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 _, _ @@ -136,9 +136,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu = aux 0 cu let native_conv_gen pb sigma env univs t1 t2 = - let penv = Environ.pre_env env in let ml_filename, prefix = get_ml_filename () in - let code, upds = mk_conv_code penv sigma prefix t1 t2 in + let code, upds = mk_conv_code env sigma prefix t1 t2 in match compile ml_filename code ~profile:false with | (true, fn) -> begin @@ -163,7 +162,7 @@ let warn_no_native_compiler = let native_conv cv_pb sigma env t1 t2 = if not Coq_config.native_compiler then begin warn_no_native_compiler (); - vm_conv cv_pb env t1 t2 + Vconv.vm_conv cv_pb env t1 t2 end else let univs = Environ.universes env in diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 9c17cc2b5f..eaad8ee0c2 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -31,13 +31,13 @@ and lambda = | Llet of Name.t * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant - | Lproj of prefix * Constant.t (* prefix, projection name *) + | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) | Lprim of prefix * Constant.t * CPrimitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl + | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) (* A fully applied constructor *) @@ -50,6 +50,10 @@ and lambda = | Llazy | Lforce +(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation +to be correct. Otherwise, memoization of previous evaluations will be applied +again to extra arguments (see #7333). *) + and lam_branches = (constructor * Name.t array * lambda) array and fix_decl = Name.t array * lambda array * lambda array diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 01ddffe3ef..0325a00b47 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -12,7 +12,7 @@ open Names open Esubst open Constr open Declarations -open Pre_env +open Environ open Nativevalues open Nativeinstr @@ -102,10 +102,10 @@ let rec map_lam_with_binders g f n lam = if body == body' && def == def' then lam else Llet(id,def',body') | Lapp(fct,args) -> let fct' = f n fct in - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if fct == fct' && args == args' then lam else mkLapp fct' args' | Lprim(prefix,kn,op,args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then lam else Lprim(prefix,kn,op,args') | Lcase(annot,t,a,br) -> let t' = f n t in @@ -116,7 +116,7 @@ let rec map_lam_with_binders g f n lam = if Array.is_empty ids then f n body else f (g (Array.length ids) n) body in if body == body' then b else (cn,ids,body') in - let br' = Array.smartmap on_b br in + let br' = Array.Smart.map on_b br in if t == t' && a == a' && br == br' then lam else Lcase(annot,t',a',br') | Lif(t,bt,bf) -> let t' = f n t in @@ -124,17 +124,17 @@ let rec map_lam_with_binders g f n lam = 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.smartmap (f n) ltypes in - let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + let ltypes' = Array.Smart.map (f n) ltypes in + let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in if ltypes == ltypes' && lbodies == lbodies' then lam else Lfix(init,(ids,ltypes',lbodies')) | Lcofix(init,(ids,ltypes,lbodies)) -> - let ltypes' = Array.smartmap (f n) ltypes in - let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + let ltypes' = Array.Smart.map (f n) ltypes in + let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in if ltypes == ltypes' && lbodies == lbodies' then lam else Lcofix(init,(ids,ltypes',lbodies')) | Lmakeblock(prefix,cn,tag,args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then lam else Lmakeblock(prefix,cn,tag,args') | Luint u -> let u' = map_uint g f n u in @@ -144,7 +144,7 @@ and map_uint g f n u = match u with | UintVal _ -> u | UintDigits(prefix,c,args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then u else UintDigits(prefix,c,args') | UintDecomp(prefix,c,a) -> let a' = f n a in @@ -177,7 +177,7 @@ let rec lam_exsubst subst lam = let lam_subst_args subst args = if is_subs_id subst then args - else Array.smartmap (lam_exsubst subst) args + else Array.Smart.map (lam_exsubst subst) args (** Simplification of lambda expression *) @@ -272,7 +272,7 @@ and simplify_app substf f substa args = (* TODO | Lproj -> simplify if the argument is known or a known global *) | _ -> mkLapp (simplify substf f) (simplify_args substa args) -and simplify_args subst args = Array.smartmap (simplify subst) args +and simplify_args subst args = Array.Smart.map (simplify subst) args and reduce_lapp substf lids body substa largs = match lids, largs with @@ -296,15 +296,17 @@ let is_value lc = match lc with | Lval _ -> true | Lmakeblock(_,_,_,args) when Array.is_empty args -> true + | Luint (UintVal _) -> true | _ -> false - + let get_value lc = match lc with | Lval v -> v - | Lmakeblock(_,_,tag,args) when Array.is_empty args -> + | Lmakeblock(_,_,tag,args) when Array.is_empty args -> Nativevalues.mk_int tag + | Luint (UintVal i) -> Nativevalues.mk_uint i | _ -> raise Not_found - + let make_args start _end = Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) @@ -517,8 +519,11 @@ let rec lambda_of_constr env sigma c = | Construct _ -> lambda_of_app env sigma c empty_args | Proj (p, c) -> - let kn = Projection.constant p in - mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|] + let pb = lookup_projection p !global_env in + (** FIXME: handle mutual records *) + let ind = (pb.proj_ind, 0) in + let prefix = get_mind_prefix !global_env (fst ind) in + mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in @@ -570,6 +575,7 @@ let rec lambda_of_constr env sigma c = Lfix(rec_init, (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> + let rec_bodies = Array.map2 (Reduction.eta_expand !global_env) rec_bodies type_bodies in let ltypes = lambda_of_args env sigma 0 type_bodies in Renv.push_rels env names; let lbodies = lambda_of_args env sigma 0 rec_bodies in diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 9a1e19b3cb..26bfeb7e0e 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -9,7 +9,7 @@ (************************************************************************) open Names open Constr -open Pre_env +open Environ open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index c69cf722bc..8bff436322 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -10,7 +10,6 @@ open Names open Declarations -open Environ open Mod_subst open Modops open Nativecode @@ -32,7 +31,7 @@ and translate_field prefix mp env acc (l,x) = (if !Flags.debug then let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in Feedback.msg_debug (Pp.str msg)); - compile_constant_field (pre_env env) prefix con acc cb + compile_constant_field env prefix con acc cb | SFBmind mb -> (if !Flags.debug then let id = mb.mind_packets.(0).mind_typename in diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index cfcb0a485b..da4413a0ad 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -64,7 +64,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t * t array - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator let accumulate_tag = 0 diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 4a58a3c7da..649853f069 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -54,7 +54,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t (* type *) * t array (* arguments *) - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator (* Constructors *) @@ -71,7 +71,7 @@ val mk_fix_accu : rec_pos -> int -> t array -> t array -> t val mk_cofix_accu : int -> t array -> t array -> t val mk_meta_accu : metavariable -> t val mk_evar_accu : Evar.t -> t -> t array -> t -val mk_proj_accu : Constant.t -> accumulator -> t +val mk_proj_accu : (inductive * int) -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t val mk_const : tag -> t diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml deleted file mode 100644 index 8ebe48e202..0000000000 --- a/kernel/pre_env.ml +++ /dev/null @@ -1,213 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* Created by Benjamin Grégoire out of environ.ml for better - modularity in the design of the bytecode virtual evaluation - machine, Dec 2005 *) -(* Bug fix by Jean-Marc Notin *) - -(* This file defines the type of kernel environments *) - -open Util -open Names -open Declarations - -module NamedDecl = Context.Named.Declaration - -(* The type of environments. *) - -(* The key attached to each constant is used by the VM to retrieve previous *) -(* evaluations of the constant. It is essentially an index in the symbols table *) -(* used by the VM. *) -type key = int CEphemeron.key option ref - -(** Linking information for the native compiler. *) - -type link_info = - | Linked of string - | LinkedInteractive of string - | NotLinked - -type constant_key = constant_body * (link_info ref * key) - -type mind_key = mutual_inductive_body * link_info ref - -type globals = { - env_constants : constant_key Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t} - -type stratification = { - env_universes : UGraph.t; - env_engagement : engagement -} - -type val_kind = - | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key - | VKnone - -type lazy_val = val_kind ref - -let force_lazy_val vk = match !vk with -| VKnone -> None -| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None - -let dummy_lazy_val () = ref VKnone -let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) - -type named_context_val = { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; -} - -type rel_context_val = { - env_rel_ctx : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; -} - -type env = { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) - env_named_context : named_context_val; (* section variables *) - env_rel_context : rel_context_val; - env_nb_rel : int; - env_stratification : stratification; - env_typing_flags : typing_flags; - retroknowledge : Retroknowledge.retroknowledge; - indirect_pterms : Opaqueproof.opaquetab; -} - -let empty_named_context_val = { - env_named_ctx = []; - env_named_map = Id.Map.empty; -} - -let empty_rel_context_val = { - env_rel_ctx = []; - env_rel_map = Range.empty; -} - -let empty_env = { - env_globals = { - env_constants = Cmap_env.empty; - env_inductives = Mindmap_env.empty; - env_modules = MPmap.empty; - env_modtypes = MPmap.empty}; - env_named_context = empty_named_context_val; - env_rel_context = empty_rel_context_val; - env_nb_rel = 0; - env_stratification = { - env_universes = UGraph.initial_universes; - env_engagement = PredicativeSet }; - env_typing_flags = Declareops.safe_flags Conv_oracle.empty; - retroknowledge = Retroknowledge.initial_retroknowledge; - indirect_pterms = Opaqueproof.empty_opaquetab } - - -(* Rel context *) - -let nb_rel env = env.env_nb_rel - -let push_rel_context_val d ctx = { - env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx; - env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map; -} - -let match_rel_context_val ctx = match ctx.env_rel_ctx with -| [] -> None -| decl :: rem -> - let (_, lval) = Range.hd ctx.env_rel_map in - let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in - Some (decl, lval, ctx) - -let push_rel d env = - { env with - env_rel_context = push_rel_context_val d env.env_rel_context; - env_nb_rel = env.env_nb_rel + 1 } - -let lookup_rel n env = - try fst (Range.get env.env_rel_context.env_rel_map (n - 1)) - with Invalid_argument _ -> raise Not_found - -let lookup_rel_val n env = - try snd (Range.get env.env_rel_context.env_rel_map (n - 1)) - with Invalid_argument _ -> raise Not_found - -let rel_skipn n ctx = { - env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx; - env_rel_map = Range.skipn n ctx.env_rel_map; -} - -let env_of_rel n env = - { env with - env_rel_context = rel_skipn n env.env_rel_context; - env_nb_rel = env.env_nb_rel - n - } - -(* Named context *) - -let push_named_context_val_val d rval ctxt = -(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) - { - env_named_ctx = Context.Named.add d ctxt.env_named_ctx; - env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; - } - -let push_named_context_val d ctxt = - push_named_context_val_val d (ref VKnone) ctxt - -let match_named_context_val c = match c.env_named_ctx with -| [] -> None -| decl :: ctx -> - let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in - let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in - let cval = { env_named_ctx = ctx; env_named_map = map } in - Some (decl, v, cval) - -let map_named_val f ctxt = - let open Context.Named.Declaration in - let fold accu d = - let d' = map_constr f d in - let accu = - if d == d' then accu - else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu - in - (accu, d') - in - let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in - if map == ctxt.env_named_map then ctxt - else { env_named_ctx = ctx; env_named_map = map } - -let push_named d env = - {env with env_named_context = push_named_context_val d env.env_named_context} - -let lookup_named id env = - fst (Id.Map.find id env.env_named_context.env_named_map) - -let lookup_named_val id env = - snd(Id.Map.find id env.env_named_context.env_named_map) - -(* Warning all the names should be different *) -let env_of_named id env = env - -(* Global constants *) - -let lookup_constant_key kn env = - Cmap_env.find kn env.env_globals.env_constants - -let lookup_constant kn env = - fst (Cmap_env.find kn env.env_globals.env_constants) - -(* Mutual Inductives *) -let lookup_mind kn env = - fst (Mindmap_env.find kn env.env_globals.env_inductives) - -let lookup_mind_key kn env = - Mindmap_env.find kn env.env_globals.env_inductives diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli deleted file mode 100644 index b05074814b..0000000000 --- a/kernel/pre_env.mli +++ /dev/null @@ -1,108 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constr -open Declarations - -(** The type of environments. *) - -type link_info = - | Linked of string - | LinkedInteractive of string - | NotLinked - -type key = int CEphemeron.key option ref - -type constant_key = constant_body * (link_info ref * key) - -type mind_key = mutual_inductive_body * link_info ref - -type globals = { - env_constants : constant_key Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t} - -type stratification = { - env_universes : UGraph.t; - env_engagement : engagement -} - -type lazy_val - -val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option -val dummy_lazy_val : unit -> lazy_val -val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit - -type named_context_val = private { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; -} - -type rel_context_val = private { - env_rel_ctx : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; -} - -type env = { - env_globals : globals; - env_named_context : named_context_val; - env_rel_context : rel_context_val; - env_nb_rel : int; - env_stratification : stratification; - env_typing_flags : typing_flags; - retroknowledge : Retroknowledge.retroknowledge; - indirect_pterms : Opaqueproof.opaquetab; -} - -val empty_named_context_val : named_context_val - -val empty_env : env - -(** Rel context *) - -val empty_rel_context_val : rel_context_val -val push_rel_context_val : - Context.Rel.Declaration.t -> rel_context_val -> rel_context_val -val match_rel_context_val : - rel_context_val -> (Context.Rel.Declaration.t * lazy_val * rel_context_val) option - -val nb_rel : env -> int -val push_rel : Context.Rel.Declaration.t -> env -> env -val lookup_rel : int -> env -> Context.Rel.Declaration.t -val lookup_rel_val : int -> env -> lazy_val -val env_of_rel : int -> env -> env - -(** Named context *) - -val push_named_context_val : - Context.Named.Declaration.t -> named_context_val -> named_context_val -val push_named_context_val_val : - Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val -val match_named_context_val : - named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option -val map_named_val : - (constr -> constr) -> named_context_val -> named_context_val - -val push_named : Context.Named.Declaration.t -> env -> env -val lookup_named : Id.t -> env -> Context.Named.Declaration.t -val lookup_named_val : Id.t -> env -> lazy_val -val env_of_named : Id.t -> env -> env - -(** Global constants *) - - -val lookup_constant_key : Constant.t -> env -> constant_key -val lookup_constant : Constant.t -> env -> constant_body - -(** Mutual Inductives *) -val lookup_mind_key : MutInd.t -> env -> mind_key -val lookup_mind : MutInd.t -> env -> mutual_inductive_body diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 81fbd4f5ef..f4af313867 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -84,7 +84,7 @@ let map_lift (l : lift) (v : fconstr array) = match v with | [|c0; c1|] -> [|(l, c0); (l, c1)|] | [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|] | [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|] -| v -> CArray.Fun1.map (fun l t -> (l, t)) l v +| v -> Array.Fun1.map (fun l t -> (l, t)) l v let pure_stack lfts stk = let rec pure_rec lfts stk = @@ -648,25 +648,24 @@ let check_leq univs u u' = let check_sort_cmp_universes env pb s0 s1 univs = let open Sorts in - match (s0,s1) with + if not (type_in_type env) then + match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with - | Null, _ | _, Pos -> () (* Prop <= Set *) - | _ -> raise NotConvertible + | Null, _ | _, Pos -> () (* Prop <= Set *) + | _ -> raise NotConvertible end | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible | (Prop c1, Type u) -> - if not (type_in_type env) then - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> check_leq univs u0 u - | CONV -> check_eq univs u0 u) + let u0 = univ_of_sort s0 in + (match pb with + | CUMUL -> check_leq univs u0 u + | CONV -> check_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then - (match pb with - | CUMUL -> check_leq univs u1 u2 - | CONV -> check_eq univs u1 u2) + (match pb with + | CUMUL -> check_leq univs u1 u2 + | CONV -> check_eq univs u1 u2) let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs @@ -699,25 +698,25 @@ let infer_leq (univs, cstrs as cuniv) u u' = let infer_cmp_universes env pb s0 s1 univs = let open Sorts in - match (s0,s1) with + if type_in_type env then univs + else + match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with - | Null, _ | _, Pos -> univs (* Prop <= Set *) - | _ -> raise NotConvertible + | Null, _ | _, Pos -> univs (* Prop <= Set *) + | _ -> raise NotConvertible end | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible | (Prop c1, Type u) -> let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> infer_leq univs u0 u - | CONV -> infer_eq univs u0 u) + (match pb with + | CUMUL -> infer_leq univs u0 u + | CONV -> infer_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then - (match pb with - | CUMUL -> infer_leq univs u1 u2 - | CONV -> infer_eq univs u1 u2) - else univs + (match pb with + | CUMUL -> infer_leq univs u1 u2 + | CONV -> infer_eq univs u1 u2) let infer_convert_instances ~flex u u' (univs,cstrs) = let cstrs' = @@ -789,24 +788,6 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 -(* This reference avoids always having to link C code with the kernel *) -let vm_conv = ref (fun cv_pb env -> - gen_conv cv_pb env ~evars:((fun _->None), universes env)) - -let warn_bytecode_compiler_failed = - let open Pp in - CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler" - (fun () -> strbrk "Bytecode compiler failed, " ++ - strbrk "falling back to standard conversion") - -let set_vm_conv (f:conv_pb -> types kernel_conversion_function) = vm_conv := f -let vm_conv cv_pb env t1 t2 = - try - !vm_conv cv_pb env t1 t2 - with Not_found | Invalid_argument _ -> - warn_bytecode_compiler_failed (); - gen_conv cv_pb env t1 t2 - let default_conv cv_pb ?(l2r=false) env t1 t2 = gen_conv cv_pb env t1 t2 @@ -880,6 +861,17 @@ let dest_prod env = in decrec env Context.Rel.empty +let dest_lam env = + let rec decrec env m c = + let t = whd_all env c in + match kind t with + | Lambda (n,a,c0) -> + let d = LocalAssum (n,a) in + decrec (push_rel d env) (Context.Rel.add d m) c0 + | _ -> m,t + in + decrec env Context.Rel.empty + (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = @@ -925,3 +917,12 @@ let is_arity env c = let _ = dest_arity env c in true with NotArity -> false + +let eta_expand env t ty = + let ctxt, codom = dest_prod env ty in + let ctxt',t = dest_lam env t in + let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in + let eta_args = List.rev_map mkRel (List.interval 1 d) in + let t = Term.applistc (Vars.lift d t) eta_args in + let t = Term.it_mkLambda_or_LetIn t (List.firstn d ctxt) in + Term.it_mkLambda_or_LetIn t ctxt' diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 14e4270b7c..e53ab6aefb 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -87,10 +87,6 @@ val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function -(** option for conversion *) -val set_vm_conv : (conv_pb -> types kernel_conversion_function) -> unit -val vm_conv : conv_pb -> types kernel_conversion_function - val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function val default_conv_leq : ?l2r:bool -> types kernel_conversion_function @@ -122,6 +118,7 @@ val betazeta_appvect : int -> constr -> constr array -> constr val dest_prod : env -> types -> Context.Rel.t * types val dest_prod_assum : env -> types -> Context.Rel.t * types +val dest_lam : env -> types -> Context.Rel.t * constr val dest_lam_assum : env -> types -> Context.Rel.t * types exception NotArity @@ -129,4 +126,4 @@ exception NotArity val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *) val is_arity : env -> types -> bool -val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit +val eta_expand : env -> constr -> types -> constr diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 0334e7a9e9..281c37b851 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -134,7 +134,7 @@ val get_native_before_match_info : retroknowledge -> entry -> Nativeinstr.lambda -> Nativeinstr.lambda -(** the following functions are solely used in Pre_env and Environ to implement +(** the following functions are solely used in Environ and Safe_typing to implement the functions register and unregister (and mem) of Environ *) val add_field : retroknowledge -> field -> entry -> retroknowledge val mem : retroknowledge -> field -> bool diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index de2a890fb5..12c82e20de 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -59,6 +59,7 @@ etc. *) +open CErrors open Util open Names open Declarations @@ -914,16 +915,12 @@ let register field value by_clause senv = but it is meant to become a replacement for environ.register *) let register_inline kn senv = let open Environ in - let open Pre_env in if not (evaluable_constant kn senv.env) then CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); - let env = pre_env senv.env in + let env = senv.env in let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in - let new_constants = Cmap_env.add kn (cb,r) env.env_globals.env_constants in - let new_globals = { env.env_globals with env_constants = new_constants } in - let env = { env with env_globals = new_globals } in - { senv with env = env_of_pre_env env } + let env = add_constant kn cb env in { senv with env} let add_constraints c = add_constraints @@ -953,3 +950,125 @@ Would this be correct with respect to undo's and stuff ? let set_strategy e k l = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } + +(** Register retroknowledge hooks *) + +open Retroknowledge + +(* the Environ.register function synchronizes the proactive and reactive + retroknowledge. *) +let dispatch = + + (* subfunction used for static decompilation of int31 (after a vm_compute, + see pretyping/vnorm.ml for more information) *) + let constr_of_int31 = + let nth_digit_plus_one i n = (* calculates the nth (starting with 0) + digit of i and adds 1 to it + (nth_digit_plus_one 1 3 = 2) *) + if Int.equal (i land (1 lsl n)) 0 then + 1 + else + 2 + in + fun ind -> fun digit_ind -> fun tag -> + let array_of_int i = + Array.init 31 (fun n -> Constr.mkConstruct + (digit_ind, nth_digit_plus_one i (30-n))) + in + (* We check that no bit above 31 is set to one. This assertion used to + fail in the VM, and led to conversion tests failing at Qed. *) + assert (Int.equal (tag lsr 31) 0); + Constr.mkApp(Constr.mkConstruct(ind, 1), array_of_int tag) + in + + (* subfunction which dispatches the compiling information of an + int31 operation which has a specific vm instruction (associates + it to the name of the coq definition in the reactive retroknowledge) *) + let int31_op n op prim kn = + { empty_reactive_info with + vm_compiling = Some (Clambda.compile_prim n op kn); + native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); + } + in + +fun rk value field -> + (* subfunction which shortens the (very common) dispatch of operations *) + let int31_op_from_const n op prim = + match Constr.kind value with + | Constr.Const kn -> int31_op n op prim kn + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") + in + let int31_binop_from_const op prim = int31_op_from_const 2 op prim in + let int31_unop_from_const op prim = int31_op_from_const 1 op prim in + match field with + | KInt31 (grp, Int31Type) -> + let int31bit = + (* invariant : the type of bits is registered, otherwise the function + would raise Not_found. The invariant is enforced in safe_typing.ml *) + match field with + | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) + | _ -> anomaly ~label:"Environ.register" + (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") + in + let i31bit_type = + match Constr.kind int31bit with + | Constr.Ind (i31bit_type,_) -> i31bit_type + | _ -> anomaly ~label:"Environ.register" + (Pp.str "Int31Bits should be an inductive type.") + in + let int31_decompilation = + match Constr.kind value with + | Constr.Ind (i31t,_) -> + constr_of_int31 i31t i31bit_type + | _ -> anomaly ~label:"Environ.register" + (Pp.str "should be an inductive type.") + in + { empty_reactive_info with + vm_decompile_const = Some int31_decompilation; + vm_before_match = Some Clambda.int31_escape_before_match; + native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); + } + | KInt31 (_, Int31Constructor) -> + { empty_reactive_info with + vm_constant_static = Some Clambda.compile_structured_int31; + vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; + native_constant_static = Some Nativelambda.compile_static_int31; + native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; + } + | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 + CPrimitives.Int31add + | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 + CPrimitives.Int31addc + | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 + CPrimitives.Int31addcarryc + | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 + CPrimitives.Int31sub + | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 + CPrimitives.Int31subc + | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const + Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc + | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 + CPrimitives.Int31mul + | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 + CPrimitives.Int31mulc + | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 + CPrimitives.Int31div21 + | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 + CPrimitives.Int31diveucl + | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 + CPrimitives.Int31addmuldiv + | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 + CPrimitives.Int31compare + | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 + CPrimitives.Int31head0 + | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 + CPrimitives.Int31tail0 + | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 + CPrimitives.Int31lor + | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 + CPrimitives.Int31land + | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 + CPrimitives.Int31lxor + | _ -> empty_reactive_info + +let _ = Hook.set Retroknowledge.dispatch_hook dispatch diff --git a/kernel/term.ml b/kernel/term.ml index 403ed881c5..b44e038e9f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -15,219 +15,17 @@ open Names open Vars open Constr -(**********************************************************************) -(** Redeclaration of types from module Constr *) -(**********************************************************************) - +(* Deprecated *) type contents = Sorts.contents = Pos | Null - -type sorts = Sorts.t = - | Prop of contents (** Prop and Set *) - | Type of Univ.Universe.t (** Type *) +[@@ocaml.deprecated "Alias for Sorts.contents"] type sorts_family = Sorts.family = InProp | InSet | InType +[@@ocaml.deprecated "Alias for Sorts.family"] -type constr = Constr.t -(** Alias types, for compatibility. *) - -type types = Constr.t -(** Same as [constr], for documentation purposes. *) - -type existential_key = Evar.t -type existential = Constr.existential - -type metavariable = Constr.metavariable - -type case_style = Constr.case_style = - LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle - -type case_printing = Constr.case_printing = - { ind_tags : bool list; cstr_tags : bool list array; style : case_style } - -type case_info = Constr.case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; - ci_cstr_nargs : int array; - ci_pp_info : case_printing - } - -type cast_kind = Constr.cast_kind = - VMcast | NATIVEcast | DEFAULTcast | REVERTcast - -(********************************************************************) -(* Constructions as implemented *) -(********************************************************************) - -type rec_declaration = Constr.rec_declaration -type fixpoint = Constr.fixpoint -type cofixpoint = Constr.cofixpoint -type 'constr pexistential = 'constr Constr.pexistential -type ('constr, 'types) prec_declaration = - ('constr, 'types) Constr.prec_declaration -type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint -type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -type 'a puniverses = 'a Univ.puniverses - -(** Simply type aliases *) -type pconstant = Constant.t puniverses -type pinductive = inductive puniverses -type pconstructor = constructor puniverses - -type ('constr, 'types, 'sort, 'univs) kind_of_term = - ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = - | Rel of int - | Var of Id.t - | Meta of metavariable - | Evar of 'constr pexistential - | Sort of 'sort - | Cast of 'constr * cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr - | App of 'constr * 'constr array - | Const of (Constant.t * 'univs) - | Ind of (inductive * 'univs) - | Construct of (constructor * 'univs) - | Case of case_info * 'constr * 'constr * 'constr array - | Fix of ('constr, 'types) pfixpoint - | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr - -type values = Vmvalues.values - -(**********************************************************************) -(** Redeclaration of functions from module Constr *) -(**********************************************************************) - -let set_sort = Sorts.set -let prop_sort = Sorts.prop -let type1_sort = Sorts.type1 -let sorts_ord = Sorts.compare -let is_prop_sort = Sorts.is_prop -let family_of_sort = Sorts.family -let univ_of_sort = Sorts.univ_of_sort -let sort_of_univ = Sorts.sort_of_univ - -(** {6 Term constructors. } *) - -let mkRel = Constr.mkRel -let mkVar = Constr.mkVar -let mkMeta = Constr.mkMeta -let mkEvar = Constr.mkEvar -let mkSort = Constr.mkSort -let mkProp = Constr.mkProp -let mkSet = Constr.mkSet -let mkType = Constr.mkType -let mkCast = Constr.mkCast -let mkProd = Constr.mkProd -let mkLambda = Constr.mkLambda -let mkLetIn = Constr.mkLetIn -let mkApp = Constr.mkApp -let mkConst = Constr.mkConst -let mkProj = Constr.mkProj -let mkInd = Constr.mkInd -let mkConstruct = Constr.mkConstruct -let mkConstU = Constr.mkConstU -let mkIndU = Constr.mkIndU -let mkConstructU = Constr.mkConstructU -let mkConstructUi = Constr.mkConstructUi -let mkCase = Constr.mkCase -let mkFix = Constr.mkFix -let mkCoFix = Constr.mkCoFix - -(**********************************************************************) -(** Aliases of functions from module Constr *) -(**********************************************************************) - -let eq_constr = Constr.equal -let eq_constr_univs = Constr.eq_constr_univs -let leq_constr_univs = Constr.leq_constr_univs -let eq_constr_nounivs = Constr.eq_constr_nounivs - -let kind_of_term = Constr.kind -let compare = Constr.compare -let constr_ord = compare -let fold_constr = Constr.fold -let map_puniverses = Constr.map_puniverses -let map_constr = Constr.map -let map_constr_with_binders = Constr.map_with_binders -let iter_constr = Constr.iter -let iter_constr_with_binders = Constr.iter_with_binders -let compare_constr = Constr.compare_head -let hash_constr = Constr.hash -let hcons_sorts = Sorts.hcons -let hcons_constr = Constr.hcons -let hcons_types = Constr.hcons - -(**********************************************************************) -(** HERE BEGINS THE INTERESTING STUFF *) -(**********************************************************************) - -(**********************************************************************) -(* Non primitive term destructors *) -(**********************************************************************) - -exception DestKO = DestKO -(* Destructs a de Bruijn index *) -let destRel = destRel -let destMeta = destRel -let isMeta = isMeta -let destVar = destVar -let isSort = isSort -let destSort = destSort -let isprop = isprop -let is_Prop = is_Prop -let is_Set = is_Set -let is_Type = is_Type -let is_small = is_small -let iskind = iskind -let isEvar = isEvar -let isEvar_or_Meta = isEvar_or_Meta -let destCast = destCast -let isCast = isCast -let isRel = isRel -let isRelN = isRelN -let isVar = isVar -let isVarId = isVarId -let isInd = isInd -let destProd = destProd -let isProd = isProd -let destLambda = destLambda -let isLambda = isLambda -let destLetIn = destLetIn -let isLetIn = isLetIn -let destApp = destApp -let destApplication = destApp -let isApp = isApp -let destConst = destConst -let isConst = isConst -let destEvar = destEvar -let destInd = destInd -let destConstruct = destConstruct -let isConstruct = isConstruct -let destCase = destCase -let isCase = isCase -let isProj = isProj -let destProj = destProj -let destFix = destFix -let isFix = isFix -let destCoFix = destCoFix -let isCoFix = isCoFix - -(******************************************************************) -(* Flattening and unflattening of embedded applications and casts *) -(******************************************************************) - -let decompose_app c = - match kind_of_term c with - | App (f,cl) -> (f, Array.to_list cl) - | _ -> (c,[]) - -let decompose_appvect c = - match kind_of_term c with - | App (f,cl) -> (f, cl) - | _ -> (c,[||]) +type sorts = Sorts.t = + | Prop of Sorts.contents (** Prop and Set *) + | Type of Univ.Universe.t (** Type *) +[@@ocaml.deprecated "Alias for Sorts.t"] (****************************************************************************) (* Functions for dealing with constr terms *) @@ -321,7 +119,7 @@ let rec to_lambda n prod = if Int.equal n 0 then prod else - match kind_of_term prod with + match kind prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) | Cast (c,_,_) -> to_lambda n c | _ -> user_err ~hdr:"to_lambda" (mt ()) @@ -330,7 +128,7 @@ let rec to_prod n lam = if Int.equal n 0 then lam else - match kind_of_term lam with + match kind lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) | Cast (c,_,_) -> to_prod n c | _ -> user_err ~hdr:"to_prod" (mt ()) @@ -342,7 +140,7 @@ let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) let lambda_applist c l = let rec app subst c l = - match kind_of_term c, l with + match kind c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c | _ -> anomaly (Pp.str "Not enough lambda's.") in @@ -355,7 +153,7 @@ let lambda_applist_assum n c l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") - else match kind_of_term t, l with + else match kind t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") @@ -367,7 +165,7 @@ let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) let prod_applist c l = let rec app subst c l = - match kind_of_term c, l with + match kind c, l with | Prod(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c | _ -> anomaly (Pp.str "Not enough prod's.") in @@ -381,7 +179,7 @@ let prod_applist_assum n c l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") - else match kind_of_term t, l with + else match kind t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") @@ -397,7 +195,7 @@ let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v) (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a product *) let decompose_prod = - let rec prodec_rec l c = match kind_of_term c with + let rec prodec_rec l c = match kind c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c @@ -407,7 +205,7 @@ let decompose_prod = (* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) let decompose_lam = - let rec lamdec_rec l c = match kind_of_term c with + let rec lamdec_rec l c = match kind c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c @@ -420,7 +218,7 @@ let decompose_prod_n n = if n < 0 then user_err (str "decompose_prod_n: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with + else match kind c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | _ -> user_err (str "decompose_prod_n: not enough products") @@ -433,7 +231,7 @@ let decompose_lam_n n = if n < 0 then user_err (str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with + else match kind c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c | _ -> user_err (str "decompose_lam_n: not enough abstractions") @@ -445,7 +243,7 @@ let decompose_lam_n n = let decompose_prod_assum = let open Context.Rel.Declaration in let rec prodec_rec l c = - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec l c @@ -458,7 +256,7 @@ let decompose_prod_assum = let decompose_lam_assum = let rec lamdec_rec l c = let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> lamdec_rec l c @@ -477,7 +275,7 @@ let decompose_prod_n_assum n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c @@ -498,7 +296,7 @@ let decompose_lam_n_assum n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c @@ -514,7 +312,7 @@ let decompose_lam_n_decls n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c @@ -541,12 +339,12 @@ let strip_lam_n n t = snd (decompose_lam_n n t) Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * sorts +type arity = Context.Rel.t * Sorts.t let destArity = let open Context.Rel.Declaration in let rec prodec_rec l c = - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c @@ -558,7 +356,7 @@ let destArity = let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign let rec isArity c = - match kind_of_term c with + match kind c with | Prod (_,_,c) -> isArity c | LetIn (_,b,_,c) -> isArity (subst1 b c) | Cast (c,_,_) -> isArity c @@ -569,13 +367,13 @@ let rec isArity c = (* Experimental, used in Presburger contrib *) type ('constr, 'types) kind_of_type = - | SortType of sorts + | SortType of Sorts.t | CastType of 'types * 'types | ProdType of Name.t * 'types * 'types | LetInType of Name.t * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array -let kind_of_type t = match kind_of_term t with +let kind_of_type t = match kind t with | Sort s -> SortType s | Cast (c,_,t) -> CastType (c, t) | Prod (na,t,c) -> ProdType (na, t, c) diff --git a/kernel/term.mli b/kernel/term.mli index 7cb3b662d4..f651d1a580 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -11,166 +11,6 @@ open Names open Constr -(** {5 Redeclaration of types from module Constr and Sorts} - - This reexports constructors of inductive types defined in module [Constr], - for compatibility purposes. Refer to this module for further info. - -*) - -exception DestKO -[@@ocaml.deprecated "Alias for [Constr.DestKO]"] - -(** {5 Simple term case analysis. } *) -val isRel : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isRel]"] -val isRelN : int -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isRelN]"] -val isVar : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isVar]"] -val isVarId : Id.t -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isVarId]"] -val isInd : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isInd]"] -val isEvar : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isEvar]"] -val isMeta : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isMeta]"] -val isEvar_or_Meta : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isEvar_or_Meta]"] -val isSort : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isSort]"] -val isCast : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCast]"] -val isApp : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isApp]"] -val isLambda : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isLambda]"] -val isLetIn : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isletIn]"] -val isProd : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isProp]"] -val isConst : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isConst]"] -val isConstruct : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isConstruct]"] -val isFix : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isFix]"] -val isCoFix : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCoFix]"] -val isCase : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCase]"] -val isProj : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isProj]"] - -val is_Prop : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Prop]"] -val is_Set : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Set]"] -val isprop : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isprop]"] -val is_Type : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Type]"] -val iskind : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_kind]"] -val is_small : Sorts.t -> bool -[@@ocaml.deprecated "Alias for [Constr.is_small]"] - - -(** {5 Term destructors } *) -(** Destructor operations are partial functions and - @raise DestKO if the term has not the expected form. *) - -(** Destructs a de Bruijn index *) -val destRel : constr -> int -[@@ocaml.deprecated "Alias for [Constr.destRel]"] - -(** Destructs an existential variable *) -val destMeta : constr -> metavariable -[@@ocaml.deprecated "Alias for [Constr.destMeta]"] - -(** Destructs a variable *) -val destVar : constr -> Id.t -[@@ocaml.deprecated "Alias for [Constr.destVar]"] - -(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether - [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) -val destSort : constr -> Sorts.t -[@@ocaml.deprecated "Alias for [Constr.destSort]"] - -(** Destructs a casted term *) -val destCast : constr -> constr * cast_kind * constr -[@@ocaml.deprecated "Alias for [Constr.destCast]"] - -(** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) -val destProd : types -> Name.t * types * types -[@@ocaml.deprecated "Alias for [Constr.destProd]"] - -(** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) -val destLambda : constr -> Name.t * types * constr -[@@ocaml.deprecated "Alias for [Constr.destLambda]"] - -(** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) -val destLetIn : constr -> Name.t * constr * types * constr -[@@ocaml.deprecated "Alias for [Constr.destLetIn]"] - -(** Destructs an application *) -val destApp : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destApp]"] - -(** Obsolete synonym of destApp *) -val destApplication : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destApplication]"] - -(** Decompose any term as an applicative term; the list of args can be empty *) -val decompose_app : constr -> constr * constr list -[@@ocaml.deprecated "Alias for [Constr.decompose_app]"] - -(** Same as [decompose_app], but returns an array. *) -val decompose_appvect : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.decompose_appvect]"] - -(** Destructs a constant *) -val destConst : constr -> Constant.t Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destConst]"] - -(** Destructs an existential variable *) -val destEvar : constr -> existential -[@@ocaml.deprecated "Alias for [Constr.destEvar]"] - -(** Destructs a (co)inductive type *) -val destInd : constr -> inductive Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destInd]"] - -(** Destructs a constructor *) -val destConstruct : constr -> constructor Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destConstruct]"] - -(** Destructs a [match c as x in I args return P with ... | -Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args -return P in t1], or [if c then t1 else t2]) -@return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] -where [info] is pretty-printing information *) -val destCase : constr -> case_info * constr * constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destCase]"] - -(** Destructs a projection *) -val destProj : constr -> projection * constr -[@@ocaml.deprecated "Alias for [Constr.destProj]"] - -(** Destructs the {% $ %}i{% $ %}th function of the block - [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} - with f{_ 2} ctx{_ 2} = b{_ 2} - ... - with f{_ n} ctx{_ n} = b{_ n}], - where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. -*) -val destFix : constr -> fixpoint -[@@ocaml.deprecated "Alias for [Constr.destFix]"] - -val destCoFix : constr -> cofixpoint -[@@ocaml.deprecated "Alias for [Constr.destCoFix]"] - (** {5 Derived constructors} *) (** non-dependent product [t1 -> t2], an alias for @@ -349,242 +189,14 @@ type ('constr, 'types) kind_of_type = val kind_of_type : types -> (constr, types) kind_of_type -(** {5 Redeclaration of stuff from module [Sorts]} *) - -val set_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.set"] - -val prop_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.prop"] - -val type1_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.type1"] - -val sorts_ord : Sorts.t -> Sorts.t -> int -[@@ocaml.deprecated "Alias for Sorts.compare"] - -val is_prop_sort : Sorts.t -> bool -[@@ocaml.deprecated "Alias for Sorts.is_prop"] - -val family_of_sort : Sorts.t -> Sorts.family -[@@ocaml.deprecated "Alias for Sorts.family"] - -(** {5 Redeclaration of stuff from module [Constr]} - - See module [Constr] for further info. *) - -(** {6 Term constructors. } *) - -val mkRel : int -> constr -[@@ocaml.deprecated "Alias for Constr.mkRel"] -val mkVar : Id.t -> constr -[@@ocaml.deprecated "Alias for Constr.mkVar"] -val mkMeta : metavariable -> constr -[@@ocaml.deprecated "Alias for Constr.mkMeta"] -val mkEvar : existential -> constr -[@@ocaml.deprecated "Alias for Constr.mkEvar"] -val mkSort : Sorts.t -> types -[@@ocaml.deprecated "Alias for Constr.mkSort"] -val mkProp : types -[@@ocaml.deprecated "Alias for Constr.mkProp"] -val mkSet : types -[@@ocaml.deprecated "Alias for Constr.mkSet"] -val mkType : Univ.Universe.t -> types -[@@ocaml.deprecated "Alias for Constr.mkType"] -val mkCast : constr * cast_kind * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkProd : Name.t * types * types -> types -[@@ocaml.deprecated "Alias for Constr"] -val mkLambda : Name.t * types * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkLetIn : Name.t * constr * types * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkApp : constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConst : Constant.t -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkProj : projection * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkInd : inductive -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstruct : constructor -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstU : Constant.t Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkIndU : inductive Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstructU : constructor Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstructUi : (pinductive * int) -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkCase : case_info * constr * constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr.mkCase"] -val mkFix : fixpoint -> constr -[@@ocaml.deprecated "Alias for Constr.mkFix"] -val mkCoFix : cofixpoint -> constr -[@@ocaml.deprecated "Alias for Constr.mkCoFix"] - -(** {6 Aliases} *) - -val eq_constr : constr -> constr -> bool -[@@ocaml.deprecated "Alias for Constr.equal"] - -(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [u]. *) -val eq_constr_univs : constr UGraph.check_function -[@@ocaml.deprecated "Alias for Constr.eq_constr_univs"] - -(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe constraints in [u]. *) -val leq_constr_univs : constr UGraph.check_function -[@@ocaml.deprecated "Alias for Constr.leq_constr_univs"] - -(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and ignoring universe instances. *) -val eq_constr_nounivs : constr -> constr -> bool -[@@ocaml.deprecated "Alias for Constr.qe_constr_nounivs"] - -val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -[@@ocaml.deprecated "Alias for Constr.kind"] - -val compare : constr -> constr -> int -[@@ocaml.deprecated "Alias for [Constr.compare]"] - -val constr_ord : constr -> constr -> int -[@@ocaml.deprecated "Alias for [Term.compare]"] - -val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a -[@@ocaml.deprecated "Alias for [Constr.fold]"] - -val map_constr : (constr -> constr) -> constr -> constr -[@@ocaml.deprecated "Alias for [Constr.map]"] - -val map_constr_with_binders : - ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr -[@@ocaml.deprecated "Alias for [Constr.map_with_binders]"] - -val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.map_puniverses]"] -val univ_of_sort : Sorts.t -> Univ.Universe.t -[@@ocaml.deprecated "Alias for [Sorts.univ_of_sort]"] -val sort_of_univ : Univ.Universe.t -> Sorts.t -[@@ocaml.deprecated "Alias for [Sorts.sort_of_univ]"] - -val iter_constr : (constr -> unit) -> constr -> unit -[@@ocaml.deprecated "Alias for [Constr.iter]"] - -val iter_constr_with_binders : - ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit -[@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"] - -val compare_constr : (int -> constr -> constr -> bool) -> int -> constr -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.compare_head]"] - -type constr = Constr.constr -[@@ocaml.deprecated "Alias for Constr.t"] - -(** Alias types, for compatibility. *) - -type types = Constr.types -[@@ocaml.deprecated "Alias for Constr.types"] - +(* Deprecated *) type contents = Sorts.contents = Pos | Null [@@ocaml.deprecated "Alias for Sorts.contents"] +type sorts_family = Sorts.family = InProp | InSet | InType +[@@ocaml.deprecated "Alias for Sorts.family"] + type sorts = Sorts.t = | Prop of Sorts.contents (** Prop and Set *) | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] - -type sorts_family = Sorts.family = InProp | InSet | InType -[@@ocaml.deprecated "Alias for Sorts.family"] - -type 'a puniverses = 'a Univ.puniverses -[@@ocaml.deprecated "Alias for Constr.puniverses"] - -(** Simply type aliases *) -type pconstant = Constr.pconstant -[@@ocaml.deprecated "Alias for Constr.pconstant"] -type pinductive = Constr.pinductive -[@@ocaml.deprecated "Alias for Constr.pinductive"] -type pconstructor = Constr.pconstructor -[@@ocaml.deprecated "Alias for Constr.pconstructor"] -type existential_key = Evar.t -[@@ocaml.deprecated "Alias for Evar.t"] -type existential = Constr.existential -[@@ocaml.deprecated "Alias for Constr.existential"] -type metavariable = Constr.metavariable -[@@ocaml.deprecated "Alias for Constr.metavariable"] - -type case_style = Constr.case_style = - LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle -[@@ocaml.deprecated "Alias for Constr.case_style"] - -type case_printing = Constr.case_printing = - { ind_tags : bool list; cstr_tags : bool list array; style : Constr.case_style } -[@@ocaml.deprecated "Alias for Constr.case_printing"] - -type case_info = Constr.case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; - ci_cstr_nargs : int array; - ci_pp_info : Constr.case_printing - } -[@@ocaml.deprecated "Alias for Constr.case_info"] - -type cast_kind = Constr.cast_kind = - VMcast | NATIVEcast | DEFAULTcast | REVERTcast -[@@ocaml.deprecated "Alias for Constr.cast_kind"] - -type rec_declaration = Constr.rec_declaration -[@@ocaml.deprecated "Alias for Constr.rec_declaration"] -type fixpoint = Constr.fixpoint -[@@ocaml.deprecated "Alias for Constr.fixpoint"] -type cofixpoint = Constr.cofixpoint -[@@ocaml.deprecated "Alias for Constr.cofixpoint"] -type 'constr pexistential = 'constr Constr.pexistential -[@@ocaml.deprecated "Alias for Constr.pexistential"] -type ('constr, 'types) prec_declaration = - ('constr, 'types) Constr.prec_declaration -[@@ocaml.deprecated "Alias for Constr.prec_declaration"] -type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint -[@@ocaml.deprecated "Alias for Constr.pfixpoint"] -type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -[@@ocaml.deprecated "Alias for Constr.pcofixpoint"] - -type ('constr, 'types, 'sort, 'univs) kind_of_term = - ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = - | Rel of int - | Var of Id.t - | Meta of Constr.metavariable - | Evar of 'constr Constr.pexistential - | Sort of 'sort - | Cast of 'constr * Constr.cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr - | App of 'constr * 'constr array - | Const of (Constant.t * 'univs) - | Ind of (inductive * 'univs) - | Construct of (constructor * 'univs) - | Case of Constr.case_info * 'constr * 'constr * 'constr array - | Fix of ('constr, 'types) Constr.pfixpoint - | CoFix of ('constr, 'types) Constr.pcofixpoint - | Proj of projection * 'constr -[@@ocaml.deprecated "Alias for Constr.kind_of_term"] - -type values = Vmvalues.values -[@@ocaml.deprecated "Alias for Vmvalues.values"] - -val hash_constr : Constr.constr -> int -[@@ocaml.deprecated "Alias for Constr.hash"] - -val hcons_sorts : Sorts.t -> Sorts.t -[@@ocaml.deprecated "Alias for [Sorts.hcons]"] - -val hcons_constr : Constr.constr -> Constr.constr -[@@ocaml.deprecated "Alias for [Constr.hcons]"] - -val hcons_types : Constr.types -> Constr.types -[@@ocaml.deprecated "Alias for [Constr.hcons]"] diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index e621a61c76..db1109e75e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -250,7 +250,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Undef nl; cook_type = t; - cook_proj = None; + cook_proj = false; cook_universes = univs; cook_inline = false; cook_context = ctx; @@ -291,7 +291,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; + cook_proj = false; cook_universes = Monomorphic_const univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -343,7 +343,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; + cook_proj = false; cook_universes = univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -370,7 +370,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); cook_type = typ; - cook_proj = Some pb; + cook_proj = true; cook_universes = univs; cook_inline = false; cook_context = None; @@ -458,30 +458,8 @@ let build_constant_declaration kn env result = check declared inferred) lc) in let univs = result.cook_universes in let tps = - let res = - match result.cook_proj with - | None -> compile_constant_body env univs def - | Some pb -> - (* The compilation of primitive projections is a bit tricky, because - they refer to themselves (the body of p looks like fun c => - Proj(p,c)). We break the cycle by building an ad-hoc compilation - environment. A cleaner solution would be that kernel projections are - simply Proj(i,c) with i an int and c a constr, but we would have to - get rid of the compatibility layer. *) - let cb = - { const_hyps = hyps; - const_body = def; - const_type = typ; - const_proj = result.cook_proj; - const_body_code = None; - const_universes = univs; - const_inline_code = result.cook_inline; - const_typing_flags = Environ.typing_flags env; - } - in - let env = add_constant kn cb env in - compile_constant_body env univs def - in Option.map Cemitcodes.from_val res + let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in + Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index be4c0e1ecc..325d5cecd7 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -221,7 +221,7 @@ let check_cast env c ct k expected_type = try match k with | VMcast -> - vm_conv CUMUL env ct expected_type + Vconv.vm_conv CUMUL env ct expected_type | DEFAULTcast -> default_conv ~l2r:false CUMUL env ct expected_type | REVERTcast -> @@ -528,13 +528,3 @@ let judge_of_case env ci pj cj lfj = let lf, lft = dest_judgev lfj in make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) - -let type_of_projection_constant env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if Declareops.constant_is_polymorphic cb then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") diff --git a/kernel/typeops.mli b/kernel/typeops.mli index bff40b017f..546f2d2b4d 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -60,7 +60,7 @@ val judge_of_constant : env -> pconstant -> unsafe_judgment (** {6 type of an applied projection } *) -val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment +val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment (** {6 Type of application. } *) val judge_of_apply : @@ -100,8 +100,6 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_projection_constant : env -> Names.projection puniverses -> types - val type_of_constant_in : env -> pconstant -> types (** Check that hyps are included in env and fails with error otherwise *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 5d1644614d..4a9467de52 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -21,7 +21,7 @@ open Univ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *) -let error_inconsistency o u v (p:explanation option) = +let error_inconsistency o u v p = raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p)) (* Universes are stratified by a partial ordering $\le$. @@ -503,7 +503,7 @@ let insert_edge strict ucan vcan g = let () = cleanup_universes g in raise e -let add_universe vlev strict g = +let add_universe_gen vlev g = try let _arcv = UMap.find vlev g.entries in raise AlreadyDeclared @@ -520,8 +520,14 @@ let add_universe vlev strict g = } in let entries = UMap.add vlev (Canonical v) g.entries in - let g = { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } in - insert_edge strict (get_set_arc g) v g + { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }, v + +let add_universe vlev strict g = + let g, v = add_universe_gen vlev g in + insert_edge strict (get_set_arc g) v g + +let add_universe_unconstrained vlev g = + fst (add_universe_gen vlev g) exception Found_explanation of explanation @@ -557,8 +563,7 @@ let get_explanation strict u v g = else match traverse strict u with Some exp -> exp | None -> assert false let get_explanation strict u v g = - if !Flags.univ_print then Some (get_explanation strict u v g) - else None + Some (lazy (get_explanation strict u v g)) (* To compare two nodes, we simply do a forward search. We implement two improvements: @@ -697,6 +702,9 @@ let enforce_univ_lt u v g = error_inconsistency Lt u v (get_explanation false v u g) let empty_universes = + { entries = UMap.empty; index = 0; n_nodes = 0; n_edges = 0 } + +let initial_universes = let set_arc = Canonical { univ = Level.set; ltle = LMap.empty; @@ -719,9 +727,6 @@ let empty_universes = let empty = { entries; index = (-2); n_nodes = 2; n_edges = 0 } in enforce_univ_lt Level.prop Level.set empty -(* Prop = Set is forbidden here. *) -let initial_universes = empty_universes - let is_initial_universes g = UMap.equal (==) g.entries initial_universes.entries let enforce_constraint cst g = @@ -768,18 +773,54 @@ let normalize_universes g = g.entries g let constraints_of_universes g = + let module UF = Unionfind.Make (LSet) (LMap) in + let uf = UF.create () in let constraints_of u v acc = match v with | Canonical {univ=u; ltle} -> UMap.fold (fun v strict acc-> let typ = if strict then Lt else Le in Constraint.add (u,typ,v) acc) ltle acc - | Equiv v -> Constraint.add (u,Eq,v) acc + | Equiv v -> UF.union u v uf; acc in - UMap.fold constraints_of g.entries Constraint.empty - -let constraints_of_universes g = - constraints_of_universes (normalize_universes g) + let csts = UMap.fold constraints_of g.entries Constraint.empty in + csts, UF.partition uf + +(* domain g.entries = kept + removed *) +let constraints_for ~kept g = + (* rmap: partial map from canonical universes to kept universes *) + let rmap, csts = LSet.fold (fun u (rmap,csts) -> + let arcu = repr g u in + if LSet.mem arcu.univ kept then + LMap.add arcu.univ arcu.univ rmap, enforce_eq_level u arcu.univ csts + else + match LMap.find arcu.univ rmap with + | v -> rmap, enforce_eq_level u v csts + | exception Not_found -> LMap.add arcu.univ u rmap, csts) + kept (LMap.empty,Constraint.empty) + in + let rec add_from u csts todo = match todo with + | [] -> csts + | (v,strict)::todo -> + let v = repr g v in + (match LMap.find v.univ rmap with + | v -> + let d = if strict then Lt else Le in + let csts = Constraint.add (u,d,v) csts in + add_from u csts todo + | exception Not_found -> + (* v is not equal to any kept universe *) + let todo = LMap.fold (fun v' strict' todo -> + (v',strict || strict') :: todo) + v.ltle todo + in + add_from u csts todo) + in + LSet.fold (fun u csts -> + let arc = repr g u in + LMap.fold (fun v strict csts -> add_from u csts [v,strict]) + arc.ltle csts) + kept csts (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index d4fba63fb3..e6dd629e45 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -49,17 +49,28 @@ exception AlreadyDeclared val add_universe : Level.t -> bool -> t -> t +(** Add a universe without (Prop,Set) <= u *) +val add_universe_unconstrained : Level.t -> t -> t + (** {6 Pretty-printing of universes. } *) val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t (** The empty graph of universes *) val empty_universes : t -[@@ocaml.deprecated "Use UGraph.initial_universes"] val sort_universes : t -> t -val constraints_of_universes : t -> Constraint.t +(** [constraints_of_universes g] returns [csts] and [partition] where + [csts] are the non-Eq constraints and [partition] is the partition + of the universes into equivalence classes. *) +val constraints_of_universes : t -> Constraint.t * LSet.t list + +(** [constraints_for ~kept g] returns the constraints about the + universes [kept] in [g] up to transitivity. + + eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *) +val constraints_for : kept:LSet.t -> t -> Constraint.t val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of diff --git a/kernel/univ.ml b/kernel/univ.ml index be21381b71..9782312cae 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -456,10 +456,10 @@ struct let super l = if is_small l then type1 else - List.smartmap (fun x -> Expr.successor x) l + List.Smart.map (fun x -> Expr.successor x) l let addn n l = - List.smartmap (fun x -> Expr.addn n x) l + List.Smart.map (fun x -> Expr.addn n x) l let rec merge_univs l1 l2 = match l1, l2 with @@ -490,39 +490,6 @@ struct in List.fold_right (fun a acc -> aux a acc) u [] - (** [max_var_pred p u] returns the maximum variable level in [u] satisfying - [p], -1 if not found *) - let rec max_var_pred p u = - let open Level in - match u with - | [] -> -1 - | (v, _) :: u -> - match var_index v with - | Some i when p i -> max i (max_var_pred p u) - | _ -> max_var_pred p u - - let rec remap_var u i j = - let open Level in - match u with - | [] -> [] - | (v, incr) :: u when var_index v = Some i -> - (Level.var j, incr) :: remap_var u i j - | _ :: u -> remap_var u i j - - let rec compact u max_var i = - if i >= max_var then (u,[]) else - let j = max_var_pred (fun j -> j < i) u in - if Int.equal i (j+1) then - let (u,s) = compact u max_var (i+1) in - (u, i :: s) - else - let (u,s) = compact (remap_var u i j) max_var (i+1) in - (u, j+1 :: s) - - let compact u = - let max_var = max_var_pred (fun _ -> true) u in - compact u max_var 0 - (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y @@ -533,7 +500,7 @@ struct let for_all = List.for_all - let smartmap = List.smartmap + let smart_map = List.Smart.map let map = List.map end @@ -574,11 +541,11 @@ let constraint_type_ord c1 c2 = match c1, c2 with (* Universe inconsistency: error raised when trying to enforce a relation that would create a cycle in the graph of universes. *) -type univ_inconsistency = constraint_type * universe * universe * explanation option +type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option exception UniverseInconsistency of univ_inconsistency -let error_inconsistency o u v (p:explanation option) = +let error_inconsistency o u v p = raise (UniverseInconsistency (o,make u,make v,p)) (* Constraints and sets of constraints. *) @@ -886,7 +853,7 @@ struct let length a = Array.length a let subst_fn fn t = - let t' = CArray.smartmap fn t in + let t' = CArray.Smart.map fn t in if t' == t then t else of_array t' let levels x = LSet.of_array x @@ -923,11 +890,11 @@ let subst_instance_level s l = | _ -> l let subst_instance_instance s i = - Array.smartmap (fun l -> subst_instance_level s l) i + Array.Smart.map (fun l -> subst_instance_level s l) i let subst_instance_universe s u = let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' @@ -1133,7 +1100,7 @@ let subst_univs_level_level subst l = let subst_univs_level_universe subst u = let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' @@ -1208,6 +1175,20 @@ let abstract_cumulativity_info (univs, variance) = let subst, univs = abstract_universes univs in subst, (univs, variance) +let rec compact_univ s vars i u = + match u with + | [] -> (s, List.rev vars) + | (lvl, _) :: u -> + match Level.var_index lvl with + | Some k when not (LMap.mem lvl s) -> + let lvl' = Level.var i in + compact_univ (LMap.add lvl lvl' s) (k :: vars) (i+1) u + | _ -> compact_univ s vars i u + +let compact_univ u = + let (s, s') = compact_univ LMap.empty [] 0 u in + (subst_univs_level_universe s u, s') + (** Pretty-printing *) let pr_constraints prl = Constraint.pr prl @@ -1254,13 +1235,16 @@ let explain_universe_inconsistency prl (o,u,v,p) = | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" in let reason = match p with - | None | Some [] -> mt() + | None -> mt() | Some p -> - str " because" ++ spc() ++ pr_uni v ++ + let p = Lazy.force p in + if p = [] then mt () + else + str " because" ++ spc() ++ pr_uni v ++ prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v) - p ++ + p ++ (if Universe.equal (snd (List.last p)) u then mt() else - (spc() ++ str "= " ++ pr_uni u)) + (spc() ++ str "= " ++ pr_uni u)) in str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ pr_rel o ++ spc() ++ pr_uni v ++ reason diff --git a/kernel/univ.mli b/kernel/univ.mli index 629d83fb86..b68bbdf359 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -128,12 +128,6 @@ sig val map : (Level.t * int -> 'a) -> t -> 'a list - (** [compact u] remaps local variables in [u] such that their indices become - consecutive. It returns the new universe and the mapping. - Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] = - [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2] - *) - val compact : t -> t * int list end type universe = Universe.t @@ -211,7 +205,7 @@ val enforce_leq_level : Level.t constraint_function Constraint.t... *) type explanation = (constraint_type * Universe.t) list -type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option +type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option exception UniverseInconsistency of univ_inconsistency @@ -504,6 +498,13 @@ val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativit val make_abstract_instance : AUContext.t -> Instance.t +(** [compact_univ u] remaps local variables in [u] such that their indices become + consecutive. It returns the new universe and the mapping. + Example: compact_univ [(Var 0, i); (Prop, 0); (Var 2; j))] = + [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2] +*) +val compact_univ : Universe.t -> Universe.t * int list + (** {6 Pretty-printing of universes. } *) val pr_constraint_type : constraint_type -> Pp.t diff --git a/kernel/vconv.ml b/kernel/vconv.ml index f11803b67c..4e4168922d 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -6,9 +6,6 @@ open Vm open Vmvalues open Csymtable -let val_of_constr env c = - val_of_constr (pre_env env) c - (* Test la structure des piles *) let compare_zipper z1 z2 = @@ -185,8 +182,18 @@ and conv_arguments env ?from:(from=0) k args1 args2 cu = !rcu else raise NotConvertible +let warn_bytecode_compiler_failed = + let open Pp in + CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler" + (fun () -> strbrk "Bytecode compiler failed, " ++ + strbrk "falling back to standard conversion") + let vm_conv_gen cv_pb env univs t1 t2 = - try + if not Coq_config.bytecode_compiler then + Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) + full_transparent_state env univs t1 t2 + else + try let v1 = val_of_constr env t1 in let v2 = val_of_constr env t2 in fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) @@ -204,5 +211,3 @@ let vm_conv cv_pb env t1 t2 = if not b then let univs = (univs, checked_universes) in let _ = vm_conv_gen cv_pb env univs t1 t2 in () - -let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 620f6b5e8a..1a31848989 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -9,7 +9,6 @@ (************************************************************************) open Constr -open Environ open Reduction (********************************************************************** @@ -19,6 +18,3 @@ val vm_conv : conv_pb -> types kernel_conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function - -(** Precompute a VM value from a constr *) -val val_of_constr : env -> constr -> Vmvalues.values diff --git a/kernel/vm.ml b/kernel/vm.ml index 14aeb732f9..d7eedc226c 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -42,8 +42,11 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack" (* interpreteur *) -external interprete : tcode -> values -> vm_env -> int -> values = - "coq_interprete_ml" +external coq_interprete : tcode -> values -> atom array -> vm_global -> vm_env -> int -> values = + "coq_interprete_byte" "coq_interprete_ml" + +let interprete code v env k = + coq_interprete code v (get_atom_rel ()) (Csymtable.get_global_data ()) env k (* Functions over arguments *) @@ -184,6 +187,6 @@ let apply_whd k whd = push_val v; interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0 | Vatom_stk(a,stk) -> - apply_stack (val_of_atom a) stk v + apply_stack (val_of_atom a) stk v | Vuniv_level lvl -> assert false diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 0e0cb4e584..8524c44d21 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -43,6 +43,7 @@ let fix_val v = (Obj.magic v : values) let cofix_upd_val v = (Obj.magic v : values) type vm_env +type vm_global let fun_env v = (Obj.magic v : vm_env) let fix_env v = (Obj.magic v : vm_env) let cofix_env v = (Obj.magic v : vm_env) @@ -51,19 +52,24 @@ type vstack = values array let fun_of_val v = (Obj.magic v : vfun) +let vm_global (v : values array) = (Obj.magic v : vm_global) + (*******************************************) (* Machine code *** ************************) (*******************************************) type tcode +(** A block whose first field is a C-allocated VM bytecode, encoded as char*. + This is compatible with the representation of the Coq VM closures. *) + +type tcode_array external mkAccuCode : int -> tcode = "coq_makeaccu" external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" -let tcode_of_obj v = ((Obj.obj v):tcode) -let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) -let fix_code v = fun_code v -let cofix_upd_code v = fun_code v +let fun_code v = (Obj.magic v : tcode) +let fix_code = fun_code +let cofix_upd_code = fun_code type vswitch = { @@ -252,6 +258,7 @@ external kind_of_closure : Obj.t -> int = "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" +external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field" let accumulate = accumulate () let whd_val : values -> whd = @@ -281,7 +288,7 @@ let whd_val : values -> whd = let obj_of_atom : atom -> Obj.t = fun a -> let res = Obj.new_block accu_tag 2 in - Obj.set_field res 0 (Obj.repr accumulate); + set_bytecode_field res 0 accumulate; Obj.set_field res 1 (Obj.repr a); res @@ -290,7 +297,6 @@ let rec obj_of_str_const str = match str with | Const_sort s -> obj_of_atom (Asort s) | Const_ind ind -> obj_of_atom (Aind ind) - | Const_proj p -> Obj.repr p | Const_b0 tag -> Obj.repr tag | Const_bn(tag, args) -> let len = Array.length args in @@ -348,6 +354,7 @@ let val_of_constant c = val_of_idkey (ConstKey c) let val_of_evar evk = val_of_idkey (EvarKey evk) external val_of_annot_switch : annot_switch -> values = "%identity" +external val_of_proj_name : Constant.t -> values = "%identity" (*************************************************) (** Operations manipulating data types ***********) @@ -367,17 +374,20 @@ external closure_arity : vfun -> int = "coq_closure_arity" external offset : Obj.t -> int = "coq_offset" external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" +external tcode_array : tcode_array -> tcode array = "coq_tcode_array" let first o = (offset_closure o (offset o)) let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix) let last o = (Obj.field o (Obj.size o - 1)) -let fix_types (v:vfix) = (Obj.magic (last (Obj.repr v)) : tcode array) -let cofix_types (v:vcofix) = (Obj.magic (last (Obj.repr v)) : tcode array) +let fix_types (v:vfix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array) +let cofix_types (v:vcofix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array) let current_fix vf = - (offset (Obj.repr vf) / 2) -let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) +let unsafe_fb_code fb i = + let off = (2 * i) * (Sys.word_size / 8) in + Obj.obj (Obj.add_offset (Obj.repr fb) (Int32.of_int off)) let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 @@ -407,13 +417,20 @@ let check_fix f1 f2 = else false else false -external atom_rel : unit -> atom array = "get_coq_atom_tbl" -external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" +let atom_rel : atom array ref = + let init i = Aid (RelKey i) in + ref (Array.init 40 init) + +let get_atom_rel () = !atom_rel + +let realloc_atom_rel n = + let n = min (2 * n + 0x100) Sys.max_array_length in + let init i = Aid (RelKey i) in + let ans = Array.init n init in + atom_rel := ans let relaccu_tbl = - let atom_rel = atom_rel() in - let len = Array.length atom_rel in - for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; + let len = Array.length !atom_rel in ref (Array.init len mkAccuCode) let relaccu_code i = @@ -422,9 +439,7 @@ let relaccu_code i = else begin realloc_atom_rel i; - let atom_rel = atom_rel () in - let nl = Array.length atom_rel in - for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done; + let nl = Array.length !atom_rel in relaccu_tbl := Array.init nl (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); @@ -434,13 +449,12 @@ let relaccu_code i = let mk_fix_body k ndef fb = let e = Obj.dup (Obj.repr fb) in for i = 0 to ndef - 1 do - Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) + set_bytecode_field e (2 * i) (relaccu_code (k + i)) done; let fix_body i = - let jump_grabrec c = offset_tcode c 2 in - let c = jump_grabrec (unsafe_fb_code fb i) in + let c = offset_tcode (unsafe_fb_code fb i) 2 in let res = Obj.new_block Obj.closure_tag 2 in - Obj.set_field res 0 (Obj.repr c); + set_bytecode_field res 0 c; Obj.set_field res 1 (offset_closure e (2*i)); ((Obj.obj res) : vfun) in Array.init ndef fix_body @@ -478,7 +492,7 @@ let mk_cofix_body apply_varray k ndef vcf = Obj.set_field e 0 c; let atom = Obj.new_block cofix_tag 1 in let self = Obj.new_block accu_tag 2 in - Obj.set_field self 0 (Obj.repr accumulate); + set_bytecode_field self 0 accumulate; Obj.set_field self 1 (Obj.repr atom); apply_varray (Obj.obj e) [|Obj.obj self|] in Array.init ndef cofix_body diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index c6e342a965..08d05a038c 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -15,6 +15,7 @@ open Cbytecodes type values type vm_env +type vm_global type vprod type vfun type vfix @@ -33,6 +34,8 @@ val fix_env : vfix -> vm_env val cofix_env : vcofix -> vm_env val cofix_upd_env : to_update -> vm_env +val vm_global : values array -> vm_global + (** Cast a value known to be a function, unsafe in general *) val fun_of_val : values -> vfun @@ -69,6 +72,9 @@ type atom = | Aind of inductive | Asort of Sorts.t +val get_atom_rel : unit -> atom array +(** Global table of rels *) + (** Zippers *) type zipper = @@ -106,6 +112,7 @@ val val_of_proj : Constant.t -> values -> values val val_of_atom : atom -> values external val_of_annot_switch : annot_switch -> values = "%identity" +external val_of_proj_name : Constant.t -> values = "%identity" (** Destructors *) |