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/cbytegen.ml | 4 | ||||
-rw-r--r-- | kernel/cbytegen.mli | 3 | ||||
-rw-r--r-- | kernel/clambda.ml | 4 | ||||
-rw-r--r-- | kernel/clambda.mli | 3 | ||||
-rw-r--r-- | kernel/csymtable.ml | 31 | ||||
-rw-r--r-- | kernel/csymtable.mli | 2 | ||||
-rw-r--r-- | kernel/kernel.mllib | 2 | ||||
-rw-r--r-- | kernel/uGraph.ml | 15 | ||||
-rw-r--r-- | kernel/uGraph.mli | 5 | ||||
-rw-r--r-- | kernel/univ.ml | 15 | ||||
-rw-r--r-- | kernel/univ.mli | 2 | ||||
-rw-r--r-- | kernel/vm.ml | 9 | ||||
-rw-r--r-- | kernel/vmvalues.ml | 24 | ||||
-rw-r--r-- | kernel/vmvalues.mli | 6 |
18 files changed, 102 insertions, 132 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/cbytegen.ml b/kernel/cbytegen.ml index 70dc6867a..a771945dd 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -829,6 +829,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 () ++ @@ -872,7 +874,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = reloc, init_code in let fv = List.rev (!(reloc.in_env).fv_rev) in - (if !Flags.dump_bytecode then + (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 -> diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index abab58b60..1c4cdcbeb 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -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/clambda.ml b/kernel/clambda.ml index 7b637c20e..641d424e2 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -807,7 +807,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 +819,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 89b7fd8e3..6cf46163e 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -25,3 +25,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/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/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/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 ea3a52295..8e19fa4e5 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -541,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. *) @@ -1235,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 aaed899bf..b68bbdf35 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -205,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 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 = |