diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/byterun/coq_interp.c | 21 | ||||
-rw-r--r-- | kernel/byterun/coq_interp.h | 9 | ||||
-rw-r--r-- | kernel/byterun/coq_memory.c | 72 | ||||
-rw-r--r-- | kernel/byterun/coq_memory.h | 7 | ||||
-rw-r--r-- | kernel/cClosure.ml | 4 | ||||
-rw-r--r-- | kernel/cClosure.mli | 4 | ||||
-rw-r--r-- | kernel/cbytegen.ml | 27 | ||||
-rw-r--r-- | kernel/constr.ml | 2 | ||||
-rw-r--r-- | kernel/constr.mli | 6 | ||||
-rw-r--r-- | kernel/csymtable.ml | 31 | ||||
-rw-r--r-- | kernel/csymtable.mli | 2 | ||||
-rw-r--r-- | kernel/environ.mli | 2 | ||||
-rw-r--r-- | kernel/esubst.ml | 10 | ||||
-rw-r--r-- | kernel/esubst.mli | 6 | ||||
-rw-r--r-- | kernel/kernel.mllib | 2 | ||||
-rw-r--r-- | kernel/names.mli | 19 | ||||
-rw-r--r-- | kernel/term.ml | 2 | ||||
-rw-r--r-- | kernel/term.mli | 6 | ||||
-rw-r--r-- | kernel/typeops.mli | 4 | ||||
-rw-r--r-- | kernel/uGraph.ml | 15 | ||||
-rw-r--r-- | kernel/uGraph.mli | 5 | ||||
-rw-r--r-- | kernel/univ.ml | 62 | ||||
-rw-r--r-- | kernel/univ.mli | 15 | ||||
-rw-r--r-- | kernel/vm.ml | 9 | ||||
-rw-r--r-- | kernel/vmvalues.ml | 24 | ||||
-rw-r--r-- | kernel/vmvalues.mli | 6 |
26 files changed, 161 insertions, 211 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index af89712d5..cfeb0a9ee 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -163,8 +163,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 +199,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; @@ -1460,7 +1463,7 @@ value coq_interprete Instruct(STOP){ print_instr("STOP"); coq_sp = sp; - return accu; + CAMLreturn(accu); } @@ -1512,12 +1515,16 @@ 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) { print_instr("coq_interprete"); - return coq_interprete((code_t)tcode, a, e, Long_val(ea)); + return coq_interprete((code_t)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 60865c32e..c04e9e00b 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 45cfae509..b2917a55e 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -24,10 +24,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 */ @@ -58,9 +54,6 @@ 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++) { (*action) (*i, i); @@ -79,24 +72,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,8 +91,6 @@ 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(); @@ -157,53 +134,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 cec34f566..9375b15de 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/cClosure.ml b/kernel/cClosure.ml index 5f683790c..08114abc4 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 @@ -364,7 +364,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 *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 3a7f77d52..e2f5a3b82 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 *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index dfc6ff23f..a771945dd 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -500,22 +500,19 @@ let rec compile_lam env reloc lam sz cont = | Lsort (Sorts.Prop _ as s) -> compile_structured_constant reloc (Const_sort s) sz cont | Lsort (Sorts.Type u) -> - (* We separate global and local universes in [u]. The former will be part - of the structured constant, while the later (if any) will be applied as - arguments. *) - let open Univ in begin - let u,s = Universe.compact u in - (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) - let compile_get_univ reloc idx sz cont = - set_max_stack_size sz; - compile_fv_elem reloc (FVuniv_var idx) sz cont - in - if List.is_empty s then - compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont - else - comp_app compile_structured_constant compile_get_univ reloc + (* We represent universes as a global constant with local universes + "compacted", i.e. as [u arg0 ... argn] where we will substitute (after + evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *) + let u,s = Univ.compact_univ u in + let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; + compile_fv_elem reloc (FVuniv_var idx) sz cont + in + if List.is_empty s then + compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont + else + comp_app compile_structured_constant compile_get_univ reloc (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont - end | Llet (id,def,body) -> compile_lam env reloc def sz diff --git a/kernel/constr.ml b/kernel/constr.ml index ba7fecadf..4f062d72f 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 diff --git a/kernel/constr.mli b/kernel/constr.mli index 98c0eaa28..0d464840c 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} diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 012948954..4f3cbf289 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -26,7 +26,9 @@ 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 *) @@ -164,7 +173,7 @@ and eval_to_patch env (buff,pl,fv) = 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 19b2b8b50..d32cfba36 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -18,3 +18,5 @@ 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/environ.mli b/kernel/environ.mli index 4e6ac1e72..fdd84b25b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -168,7 +168,7 @@ 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 } *) diff --git a/kernel/esubst.ml b/kernel/esubst.ml index a11a0dc00..91cc64523 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 diff --git a/kernel/esubst.mli b/kernel/esubst.mli index b82d6fdf0..a674c425a 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/kernel.mllib b/kernel/kernel.mllib index 370185a72..5d270125a 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -43,6 +43,6 @@ Subtyping Mod_typing Nativelibrary Safe_typing -Vm Csymtable +Vm Vconv diff --git a/kernel/names.mli b/kernel/names.mli index ffd96781b..96e020aed 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -547,6 +547,8 @@ 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.} *) @@ -633,27 +635,27 @@ val eq_label : Label.t -> Label.t -> bool (** {5 Unique bound module names} *) type mod_bound_id = MBId.t -(** Alias type. *) +[@@ocaml.deprecated "Same as [MBId.t]."] -val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int +val mod_bound_id_ord : MBId.t -> MBId.t -> int [@@ocaml.deprecated "Same as [MBId.compare]."] -val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool +val mod_bound_id_eq : MBId.t -> MBId.t -> bool [@@ocaml.deprecated "Same as [MBId.equal]."] -val make_mbid : DirPath.t -> Id.t -> mod_bound_id +val make_mbid : DirPath.t -> Id.t -> MBId.t [@@ocaml.deprecated "Same as [MBId.make]."] -val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t +val repr_mbid : MBId.t -> int * Id.t * DirPath.t [@@ocaml.deprecated "Same as [MBId.repr]."] -val id_of_mbid : mod_bound_id -> Id.t +val id_of_mbid : MBId.t -> Id.t [@@ocaml.deprecated "Same as [MBId.to_id]."] -val string_of_mbid : mod_bound_id -> string +val string_of_mbid : MBId.t -> string [@@ocaml.deprecated "Same as [MBId.to_string]."] -val debug_string_of_mbid : mod_bound_id -> string +val debug_string_of_mbid : MBId.t -> string [@@ocaml.deprecated "Same as [MBId.debug_to_string]."] (** {5 Names} *) @@ -745,6 +747,7 @@ 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]"] diff --git a/kernel/term.ml b/kernel/term.ml index 403ed881c..e1affb1c0 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -92,7 +92,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 type values = Vmvalues.values diff --git a/kernel/term.mli b/kernel/term.mli index 7cb3b662d..ee84dcb2b 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -155,7 +155,7 @@ val destCase : constr -> case_info * constr * constr * constr array [@@ocaml.deprecated "Alias for [Constr.destCase]"] (** Destructs a projection *) -val destProj : constr -> projection * constr +val destProj : constr -> Projection.t * constr [@@ocaml.deprecated "Alias for [Constr.destProj]"] (** Destructs the {% $ %}i{% $ %}th function of the block @@ -403,7 +403,7 @@ 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 +val mkProj : Projection.t * constr -> constr [@@ocaml.deprecated "Alias for Constr"] val mkInd : inductive -> constr [@@ocaml.deprecated "Alias for Constr"] @@ -571,7 +571,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | 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 + | Proj of Projection.t * 'constr [@@ocaml.deprecated "Alias for Constr.kind_of_term"] type values = Vmvalues.values diff --git a/kernel/typeops.mli b/kernel/typeops.mli index bff40b017..85b2cfffd 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,7 +100,7 @@ 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_projection_constant : env -> Projection.t puniverses -> types val type_of_constant_in : env -> pconstant -> types diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 5d1644614..e6b27077b 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$. @@ -557,8 +557,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: @@ -768,18 +767,18 @@ 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 (** [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 d4fba63fb..cca2eb472 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -59,7 +59,10 @@ val empty_universes : t 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 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 be21381b7..8e19fa4e5 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -490,39 +490,6 @@ struct in List.fold_right (fun a acc -> aux a acc) u [] - (** [max_var_pred p u] returns the maximum variable level in [u] satisfying - [p], -1 if not found *) - let rec max_var_pred p u = - let open Level in - match u with - | [] -> -1 - | (v, _) :: u -> - match var_index v with - | Some i when p i -> max i (max_var_pred p u) - | _ -> max_var_pred p u - - let rec remap_var u i j = - let open Level in - match u with - | [] -> [] - | (v, incr) :: u when var_index v = Some i -> - (Level.var j, incr) :: remap_var u i j - | _ :: u -> remap_var u i j - - let rec compact u max_var i = - if i >= max_var then (u,[]) else - let j = max_var_pred (fun j -> j < i) u in - if Int.equal i (j+1) then - let (u,s) = compact u max_var (i+1) in - (u, i :: s) - else - let (u,s) = compact (remap_var u i j) max_var (i+1) in - (u, j+1 :: s) - - let compact u = - let max_var = max_var_pred (fun _ -> true) u in - compact u max_var 0 - (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y @@ -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. *) @@ -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 629d83fb8..b68bbdf35 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/vm.ml b/kernel/vm.ml index 14aeb732f..d7eedc226 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 0e0cb4e58..6a41efac2 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,6 +52,8 @@ 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 *** ************************) (*******************************************) @@ -407,13 +410,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 +432,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); diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index c6e342a96..550791b2c 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 = |