diff options
60 files changed, 655 insertions, 213 deletions
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v index 4f7fdb34c..0d42dabfd 100644 --- a/contrib/ring/ArithRing.v +++ b/contrib/ring/ArithRing.v @@ -16,7 +16,7 @@ Require Import Eqdep_dec. Open Local Scope nat_scope. -Fixpoint nateq (n m:nat) {struct m} : bool := +Unboxed Fixpoint nateq (n m:nat) {struct m} : bool := match n, m with | O, O => true | S n', S m' => nateq n' m' diff --git a/contrib/ring/NArithRing.v b/contrib/ring/NArithRing.v index ebc6a69ca..41e3a7d7b 100644 --- a/contrib/ring/NArithRing.v +++ b/contrib/ring/NArithRing.v @@ -15,7 +15,7 @@ Require Export ZArith_base. Require Import NArith. Require Import Eqdep_dec. -Definition Neq (n m:N) := +Unboxed Definition Neq (n m:N) := match (n ?= m)%N with | Datatypes.Eq => true | _ => false @@ -41,4 +41,4 @@ Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq. apply Neq_prop. Qed. -Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
\ No newline at end of file +Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ]. diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v index b89a850bf..9a11a70b9 100644 --- a/contrib/ring/Quote.v +++ b/contrib/ring/Quote.v @@ -26,6 +26,7 @@ ***********************************************************************) Set Implicit Arguments. +Unset Boxed Definitions. Section variables_map. @@ -81,4 +82,4 @@ Qed. End variables_map. -Unset Implicit Arguments.
\ No newline at end of file +Unset Implicit Arguments. diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index ef58f51c9..5d5046393 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -12,6 +12,8 @@ Require Import Ring_theory. Require Import Quote. Require Import Ring_normalize. +Unset Boxed Definitions. + Section abstract_semi_rings. Inductive aspolynomial : Type := @@ -701,4 +703,4 @@ Proof. rewrite H; reflexivity. Qed. -End abstract_rings.
\ No newline at end of file +End abstract_rings. diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index fb194e52a..bd22fa39a 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -12,6 +12,7 @@ Require Import Ring_theory. Require Import Quote. Set Implicit Arguments. +Unset Boxed Definitions. Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. Proof. @@ -898,4 +899,4 @@ Infix "*" := Pmult : ring_scope. Notation "- x" := (Popp x) : ring_scope. Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope. -Delimit Scope ring_scope with ring.
\ No newline at end of file +Delimit Scope ring_scope with ring. diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v index 2a2ec3720..aa6d95eab 100644 --- a/contrib/ring/Setoid_ring_normalize.v +++ b/contrib/ring/Setoid_ring_normalize.v @@ -12,7 +12,8 @@ Require Import Setoid_ring_theory. Require Import Quote. Set Implicit Arguments. - +Unset Boxed Definitions. + Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. Proof. simple induction n; simple induction m; simpl in |- *; diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v index c726f7eea..9324fb602 100644 --- a/contrib/ring/ZArithRing.v +++ b/contrib/ring/ZArithRing.v @@ -14,7 +14,7 @@ Require Export ArithRing. Require Export ZArith_base. Require Import Eqdep_dec. -Definition Zeq (x y:Z) := +Unboxed Definition Zeq (x y:Z) := match (x ?= y)%Z with | Datatypes.Eq => true | _ => false diff --git a/dev/base_include b/dev/base_include index 969637c42..4c8bd9c48 100644 --- a/dev/base_include +++ b/dev/base_include @@ -24,9 +24,14 @@ #install_printer (* section_path *) prsp;; #install_printer (* qualid *) prqualid;; #install_printer (* kernel_name *) prkn;; -#install_printer (* constr *) print_pure_constr;; +#install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; -(* parsing of names *) +#install_printer (* values *) ppvalues;; +#install_printer ppzipper;; +#install_printer ppstack;; +#install_printer ppatom;; +#install_printer ppwhd;; +#install_printer ppvblock;; let qid = Libnames.qualid_of_string;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 70aaccf0c..870d382f8 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -224,11 +224,12 @@ let print_pure_constr csr = print_string "end"; close_box() | Fix ((t,i),(lna,tl,bl)) -> - print_string "Fix("; print_int i; print_string ")"; + print_string "Fix" +(* "("; print_int i; print_string ")"; print_cut(); open_vbox 0; let rec print_fix () = - for k = 0 to Array.length tl do + for k = 0 to (Array.length tl) - 1 do open_vbox 0; name_display lna.(k); print_string "/"; print_int t.(k); print_cut(); print_string ":"; @@ -236,13 +237,13 @@ let print_pure_constr csr = box_display bl.(k); close_box (); print_cut() done - in print_string"{"; print_fix(); print_string"}" + in print_string"{"; print_fix(); print_string"}" *) | CoFix(i,(lna,tl,bl)) -> print_string "CoFix("; print_int i; print_string ")"; print_cut(); open_vbox 0; let rec print_fix () = - for k = 0 to Array.length tl do + for k = 0 to (Array.length tl) - 1 do open_vbox 1; name_display lna.(k); print_cut(); print_string ":"; box_display tl.(k) ; print_cut(); print_string ":="; @@ -274,7 +275,12 @@ let print_pure_constr csr = print_string (string_of_kn sp) in + try box_display csr; print_flush() + with e -> + print_string (Printexc.to_string e);print_flush (); + raise e + (* let _ = Vernacentries.add "PrintConstr" @@ -297,8 +303,11 @@ let _ = let ppfconstr c = ppterm (Closure.term_of_fconstr c) +open Names open Cbytecodes open Cemitcodes +open Vm + let ppripos (ri,pos) = (match ri with | Reloc_annot a -> @@ -310,3 +319,85 @@ let ppripos (ri,pos) = | Reloc_getglobal kn -> print_string ("getglob "^(string_of_kn kn)^"\n")); print_flush () + +let print_vfix () = print_string "vfix" +let print_vfix_app () = print_string "vfix_app" +let print_vswith () = print_string "switch" + +let ppsort = function + | Prop(Pos) -> print_string "Set" + | Prop(Null) -> print_string "Prop" + | Type u -> print_string "Type" + + + +let print_idkey idk = + match idk with + | ConstKey sp -> + print_string "Cons("; + print_string (string_of_kn sp); + print_string ")" + | VarKey id -> print_string (string_of_id id) + | RelKey i -> print_string "~";print_int i + +let rec ppzipper z = + match z with + | Zapp args -> + let n = nargs args in + open_hbox (); + for i = 0 to n-2 do + ppvalues (arg args i);print_string ";";print_space() + done; + if n-1 >= 0 then ppvalues (arg args (n-1)); + close_box() + | Zfix _ -> print_string "Zfix" + | Zswitch _ -> print_string "Zswitch" + +and ppstack s = + open_hovbox 0; + print_string "["; + List.iter (fun z -> ppzipper z;print_string " | ") s; + print_string "]"; + close_box() + +and ppatom a = + match a with + | Aid idk -> print_idkey idk + | Aiddef(idk,_) -> print_string "&";print_idkey idk + | Aind(sp,i) -> print_string "Ind("; + print_string (string_of_kn sp); + print_string ","; print_int i; + print_string ")" + | Afix_app _ -> print_vfix_app () + | Aswitch _ -> print_vswith() + +and ppwhd whd = + match whd with + | Vsort s -> ppsort s + | Vprod _ -> print_string "product" + | Vfun _ -> print_string "function" + | Vfix _ -> print_vfix() + | Vfix_app _ -> print_vfix_app() + | Vcofix _ -> print_string "cofix" + | Vcofix_app _ -> print_string "cofix_app" + | Vconstr_const i -> print_string "C(";print_int i;print_string")" + | Vconstr_block b -> ppvblock b + | Vatom_stk(a,s) -> + open_hbox();ppatom a;close_box(); + print_string"@";ppstack s + +and ppvblock b = + open_hbox(); + print_string "Cb(";print_int (btag b); + let n = bsize b in + for i = 0 to n -1 do + print_string ",";ppvalues (bfield b i) + done; + print_string")"; + close_box() + +and ppvalues v = + open_hovbox 0;ppwhd (whd_val v);close_box(); + print_flush() + + diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 55ad3aa5e..446c76498 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -39,6 +39,26 @@ value coq_makeaccu (value i) { return (value)res; } +value coq_accucond (value i) { + code_t q; + code_t res = coq_stat_alloc(8); + q = res; + *q++ = (opcode_t)(coq_instr_table[ACCUMULATECOND] - coq_instr_base); + *q = (opcode_t)Int_val(i); + return (value)res; +} + +value coq_is_accumulate_code(value code){ + code_t q; + int res; + q = (code_t)code; + res = + (*q == (opcode_t)(coq_instr_table[ACCUMULATECOND] - coq_instr_base)) + || + (*q == (opcode_t)(coq_instr_table[ACCUMULATE] - coq_instr_base)); + return Val_bool(res); +} + value coq_pushpop (value i) { code_t res; int n; @@ -91,9 +111,10 @@ code_t coq_thread_code (code_t code, asize_t len){ case GRAB: case COGRAB: case OFFSETCLOSURE: case PUSHOFFSETCLOSURE: case GETGLOBAL: case PUSHGETGLOBAL: - case GETGLOBALBOXED: case PUSHGETGLOBALBOXED: + /* case GETGLOBALBOXED: case PUSHGETGLOBALBOXED: */ case MAKEBLOCK1: case MAKEBLOCK2: case MAKEBLOCK3: case MAKEACCU: case CONSTINT: case PUSHCONSTINT: case GRABREC: case PUSHFIELD: + case ACCUMULATECOND: *q++ = *p++; break; @@ -148,6 +169,25 @@ value coq_makeaccu (value i) { return (value)res; } +value coq_accucond (value i) { + code_t q; + code_t res = coq_stat_alloc(8); + q = res; + *q++ = (opcode_t)ACCUMULATECOND; + *q = (opcode_t)Int_val(i); + return (value)res; +} + +value coq_is_accumulate_code(value code){ + code_t q; + int res; + q = (code_t)code; + res = + (*q == ACCUMULATECOND) || + (*q == ACCUMULATE); + return Val_bool(res); +} + value coq_pushpop (value i) { code_t res; int n; diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index bceb104e9..e3296c0da 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -27,4 +27,6 @@ extern char * coq_instr_base; value coq_tcode_of_code(value code, value len); value coq_makeaccu (value i); value coq_pushpop (value i); +value coq_accucond (value i); +value coq_is_accumulate_code(value code); #endif /* _COQ_FIX_CODE_ */ diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 2c23a4c89..d3b07526f 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -28,13 +28,12 @@ enum instructions { PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, PUSHOFFSETCLOSURE, GETGLOBAL, PUSHGETGLOBAL, - GETGLOBALBOXED, PUSHGETGLOBALBOXED, MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, FORCE, SWITCH, PUSHFIELD, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, - ACCUMULATE, STOP + ACCUMULATE, ACCUMULATECOND, STOP }; #endif /* _COQ_INSTRUCT_ */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a5f6f01d7..692baa7e7 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -51,10 +51,20 @@ sp is a local copy of the global variable extern_sp. */ # endif # endif #else -# define Instruct(name) case name: print_instr(name); +# define Instruct(name) case name: # define Next break #endif +/*#define _COQ_DEBUG_*/ + +#ifdef _COQ_DEBUG_ +# define print_instr(s) if (drawinstr) printf("%s\n",s) +# define print_int(i) if (drawinstr) printf("%d\n",i) +# else +# define print_instr(s) +# define print_int(i) +#endif + /* GC interface */ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } @@ -154,8 +164,6 @@ value coq_interprete #else opcode_t curr_instr; #endif - value * global_transp; - if (coq_pc == NULL) { /* Interpreter is initializing */ #ifdef THREADED_CODE coq_instr_table = (char **) coq_jumptable; @@ -168,8 +176,6 @@ value coq_interprete #endif /* Initialisation */ - if (default_transp == BOXED) global_transp = &coq_global_boxed; - else global_transp = &coq_global_transp; sp = coq_sp; pc = coq_pc; accu = coq_accu; @@ -183,107 +189,138 @@ value coq_interprete /* Basic stack operations */ Instruct(ACC0){ + print_instr("ACC0"); accu = sp[0]; Next; } Instruct(ACC1){ + print_instr("ACC1"); accu = sp[1]; Next; } Instruct(ACC2){ + print_instr("ACC2"); accu = sp[2]; Next; } Instruct(ACC3){ + print_instr("ACC3"); accu = sp[3]; Next; } Instruct(ACC4){ + print_instr("ACC4"); accu = sp[4]; Next; } Instruct(ACC5){ + print_instr("ACC5"); accu = sp[5]; Next; } Instruct(ACC6){ + print_instr("ACC6"); accu = sp[6]; Next; } Instruct(ACC7){ + print_instr("ACC7"); accu = sp[7]; Next; } Instruct(PUSH){ + print_instr("PUSH"); *--sp = accu; Next; } Instruct(PUSHACC0) { + print_instr("PUSHACC0"); *--sp = accu; Next; } Instruct(PUSHACC1){ + print_instr("PUSHACC1"); *--sp = accu; accu = sp[1]; Next; } Instruct(PUSHACC2){ + print_instr("PUSHACC2"); *--sp = accu; accu = sp[2]; Next; } Instruct(PUSHACC3){ + print_instr("PUSHACC3"); *--sp = accu; accu = sp[3]; Next; } Instruct(PUSHACC4){ + print_instr("PUSHACC4"); *--sp = accu; accu = sp[4]; Next; } Instruct(PUSHACC5){ + print_instr("PUSHACC5"); *--sp = accu; accu = sp[5]; Next; } Instruct(PUSHACC6){ + print_instr("PUSHACC5"); *--sp = accu; accu = sp[6]; Next; } Instruct(PUSHACC7){ + print_instr("PUSHACC7"); *--sp = accu; accu = sp[7]; Next; } Instruct(PUSHACC){ + print_instr("PUSHACC"); *--sp = accu; } /* Fallthrough */ Instruct(ACC){ + print_instr("ACC"); accu = sp[*pc++]; Next; } Instruct(POP){ + print_instr("POP"); sp += *pc++; Next; } /* Access in heap-allocated environment */ Instruct(ENVACC1){ + print_instr("ENVACC1"); accu = Field(coq_env, 1); Next; } Instruct(ENVACC2){ + print_instr("ENVACC2"); accu = Field(coq_env, 2); Next; } Instruct(ENVACC3){ + print_instr("ENVACC3"); accu = Field(coq_env, 3); Next; } Instruct(ENVACC4){ + print_instr("ENVACC4"); accu = Field(coq_env, 4); Next; } Instruct(PUSHENVACC1){ + print_instr("PUSHENVACC1"); *--sp = accu; accu = Field(coq_env, 1); Next; } Instruct(PUSHENVACC2){ + print_instr("PUSHENVACC2"); *--sp = accu; accu = Field(coq_env, 2); Next; } Instruct(PUSHENVACC3){ + print_instr("PUSHENVACC3"); *--sp = accu; accu = Field(coq_env, 3); Next; } Instruct(PUSHENVACC4){ + print_instr("PUSHENVACC4"); *--sp = accu; accu = Field(coq_env, 4); Next; } Instruct(PUSHENVACC){ + print_instr("PUSHENVACC"); *--sp = accu; } /* Fallthrough */ Instruct(ENVACC){ + print_instr("ENVACC"); accu = Field(coq_env, *pc++); Next; } /* Function application */ Instruct(PUSH_RETADDR) { + print_instr("PUSH_RETADDR"); sp -= 3; sp[0] = (value) (pc + *pc); sp[1] = coq_env; @@ -293,6 +330,7 @@ value coq_interprete Next; } Instruct(APPLY) { + print_instr("APPLY"); coq_extra_args = *pc - 1; pc = Code_val(accu); coq_env = accu; @@ -300,6 +338,7 @@ value coq_interprete } Instruct(APPLY1) { value arg1 = sp[0]; + print_instr("APPLY1"); sp -= 3; sp[0] = arg1; sp[1] = (value)pc; @@ -313,6 +352,7 @@ value coq_interprete Instruct(APPLY2) { value arg1 = sp[0]; value arg2 = sp[1]; + print_instr("APPLY2"); sp -= 3; sp[0] = arg1; sp[1] = arg2; @@ -328,6 +368,7 @@ value coq_interprete value arg1 = sp[0]; value arg2 = sp[1]; value arg3 = sp[2]; + print_instr("APPLY3"); sp -= 3; sp[0] = arg1; sp[1] = arg2; @@ -346,6 +387,7 @@ value coq_interprete int slotsize = *pc; value * newsp; int i; + print_instr("APPTERM"); /* Slide the nargs bottom words of the current frame to the top of the frame, and discard the remainder of the frame */ newsp = sp + slotsize - nargs; @@ -358,6 +400,7 @@ value coq_interprete } Instruct(APPTERM1) { value arg1 = sp[0]; + print_instr("APPTERM1"); sp = sp + *pc - 1; sp[0] = arg1; pc = Code_val(accu); @@ -367,6 +410,7 @@ value coq_interprete Instruct(APPTERM2) { value arg1 = sp[0]; value arg2 = sp[1]; + print_instr("APPTERM2"); sp = sp + *pc - 2; sp[0] = arg1; sp[1] = arg2; @@ -379,6 +423,7 @@ value coq_interprete value arg1 = sp[0]; value arg2 = sp[1]; value arg3 = sp[2]; + print_instr("APPTERM3"); sp = sp + *pc - 3; sp[0] = arg1; sp[1] = arg2; @@ -390,6 +435,7 @@ value coq_interprete } Instruct(RETURN) { + print_instr("RETURN"); sp += *pc++; if (coq_extra_args > 0) { coq_extra_args--; @@ -407,6 +453,7 @@ value coq_interprete Instruct(RESTART) { int num_args = Wosize_val(coq_env) - 2; int i; + print_instr("RESTART"); sp -= num_args; for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2); coq_env = Field(coq_env, 1); @@ -416,6 +463,8 @@ value coq_interprete Instruct(GRAB) { int required = *pc++; + print_instr("GRAB"); + /* printf("GRAB %d\n",required); */ if (coq_extra_args >= required) { coq_extra_args -= required; } else { @@ -436,10 +485,13 @@ value coq_interprete Instruct(COGRAB){ int required = *pc++; + print_instr("COGRAB"); if(forcable == Val_true) { + print_instr("true"); /* L'instruction précédante est FORCE */ if (coq_extra_args > 0) coq_extra_args--; pc++; + forcable = Val_false; } else { /* L'instruction précédante est APPLY */ mlsize_t num_args, i; num_args = 1 + coq_extra_args; /* arg1 + extra args */ @@ -457,6 +509,7 @@ value coq_interprete } Instruct(GRABREC) { int rec_pos = *pc++; /* commence a zero */ + print_instr("GRABREC"); if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) { pc++;/* On saute le Restart */ } else { @@ -506,6 +559,8 @@ value coq_interprete Instruct(CLOSURE) { int nvars = *pc++; int i; + print_instr("CLOSURE"); + print_int(nvars); if (nvars > 0) *--sp = accu; Alloc_small(accu, 1 + nvars, Closure_tag); Code_val(accu) = pc + *pc; @@ -521,6 +576,7 @@ value coq_interprete int start = *pc++; int i; value * p; + print_instr("CLOSUREREC"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ Alloc_small(accu, nfuncs, 0); @@ -551,51 +607,52 @@ value coq_interprete } Instruct(PUSHOFFSETCLOSURE) { + print_instr("PUSHOFFSETCLOSURE"); *--sp = accu; } /* fallthrough */ Instruct(OFFSETCLOSURE) { + print_instr("OFFSETCLOSURE"); accu = coq_env + *pc++ * sizeof(value); Next; } Instruct(PUSHOFFSETCLOSUREM2) { + print_instr("PUSHOFFSETCLOSUREM2"); *--sp = accu; } /* fallthrough */ Instruct(OFFSETCLOSUREM2) { + print_instr("OFFSETCLOSUREM2"); accu = coq_env - 2 * sizeof(value); Next; } Instruct(PUSHOFFSETCLOSURE0) { + print_instr("PUSHOFFSETCLOSURE0"); *--sp = accu; }/* fallthrough */ Instruct(OFFSETCLOSURE0) { + print_instr("OFFSETCLOSURE0"); accu = coq_env; Next; } Instruct(PUSHOFFSETCLOSURE2){ + print_instr("PUSHOFFSETCLOSURE2"); *--sp = accu; /* fallthrough */ } Instruct(OFFSETCLOSURE2) { + print_instr("OFFSETCLOSURE2"); accu = coq_env + 2 * sizeof(value); Next; } /* Access to global variables */ Instruct(PUSHGETGLOBAL) { + print_instr("PUSHGETGLOBAL"); *--sp = accu; } /* Fallthrough */ Instruct(GETGLOBAL){ + print_instr("GETGLOBAL"); accu = Field(coq_global_data, *pc); pc++; Next; } - Instruct(PUSHGETGLOBALBOXED) { - *--sp = accu; - } - /* Fallthrough */ - Instruct(GETGLOBALBOXED){ - accu = Field(*global_transp, *pc); - pc++; - Next; - } /* Allocation of blocks */ Instruct(MAKEBLOCK) { @@ -603,6 +660,7 @@ value coq_interprete tag_t tag = *pc++; mlsize_t i; value block; + print_instr("MAKEBLOCK"); Alloc_small(block, wosize, tag); Field(block, 0) = accu; for (i = 1; i < wosize; i++) Field(block, i) = *sp++; @@ -613,6 +671,7 @@ value coq_interprete tag_t tag = *pc++; value block; + print_instr("MAKEBLOCK1"); Alloc_small(block, 1, tag); Field(block, 0) = accu; accu = block; @@ -622,6 +681,7 @@ value coq_interprete tag_t tag = *pc++; value block; + print_instr("MAKEBLOCK2"); Alloc_small(block, 2, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -632,6 +692,7 @@ value coq_interprete Instruct(MAKEBLOCK3) { tag_t tag = *pc++; value block; + print_instr("MAKEBLOCK3"); Alloc_small(block, 3, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -647,7 +708,9 @@ value coq_interprete /* Branches and conditional branches */ Instruct(FORCE) { + print_instr("FORCE"); if (Is_block(accu) && Tag_val(accu) == Closure_tag) { + forcable = Val_true; /* On pousse l'addresse de retour et l'argument */ sp -= 3; sp[0] = (value) (pc); @@ -658,6 +721,9 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; goto check_stacks; + } else { + if (Is_block(accu)) print_int(Tag_val(accu)); + else print_instr("Not a block"); } Next; } @@ -665,11 +731,17 @@ value coq_interprete Instruct(SWITCH) { uint32 sizes = *pc++; + print_instr("SWITCH"); + print_int(sizes); if (Is_block(accu)) { long index = Tag_val(accu); + print_instr("block"); + print_int(index); pc += pc[(sizes & 0xFFFF) + index]; } else { long index = Long_val(accu); + print_instr("constant"); + print_int(index); pc += pc[index]; } Next; @@ -677,6 +749,7 @@ value coq_interprete Instruct(PUSHFIELD){ int i; int size = *pc++; + print_instr("PUSHFIELD"); sp -= size; for(i=0;i<size;i++)sp[i] = Field(accu,i); Next; @@ -686,6 +759,7 @@ value coq_interprete mlsize_t sz; int i, annot; code_t typlbl,swlbl; + print_instr("MAKESWITCHBLOCK"); typlbl = (code_t)pc + *pc; pc++; swlbl = (code_t)pc + *pc; @@ -725,6 +799,7 @@ value coq_interprete /* Stack checks */ check_stacks: + print_instr("check_stacks"); if (sp < coq_stack_threshold) { coq_sp = sp; realloc_coq_stack(Coq_stack_threshold); @@ -736,32 +811,42 @@ value coq_interprete /* Integer constants */ Instruct(CONST0){ + print_instr("CONST0"); accu = Val_int(0); Next;} Instruct(CONST1){ + print_instr("CONST1"); accu = Val_int(1); Next;} Instruct(CONST2){ + print_instr("CONST2"); accu = Val_int(2); Next;} Instruct(CONST3){ + print_instr("CONST3"); accu = Val_int(3); Next;} Instruct(PUSHCONST0){ + print_instr("PUSHCONST0"); *--sp = accu; accu = Val_int(0); Next; } Instruct(PUSHCONST1){ + print_instr("PUSHCONST1"); *--sp = accu; accu = Val_int(1); Next; } Instruct(PUSHCONST2){ + print_instr("PUSHCONST2"); *--sp = accu; accu = Val_int(2); Next; } Instruct(PUSHCONST3){ + print_instr("PUSHCONST3"); *--sp = accu; accu = Val_int(3); Next; } Instruct(PUSHCONSTINT){ + print_instr("PUSHCONSTINT"); *--sp = accu; } /* Fallthrough */ Instruct(CONSTINT) { + print_instr("CONSTINT"); accu = Val_int(*pc); pc++; Next; @@ -770,12 +855,34 @@ value coq_interprete /* Debugging and machine control */ Instruct(STOP){ + print_instr("STOP"); coq_sp = sp; return accu; } + Instruct(ACCUMULATECOND) { + int i, num; + print_instr("ACCUMULATECOND"); + num = *pc; + pc++; + if (Field(coq_global_boxed, num) == Val_false || coq_all_transp) { + /* printf ("false\n"); + printf ("tag = %d", Tag_val(Field(accu,1))); */ + num = Wosize_val(coq_env); + for(i = 2; i < num; i++) *--sp = Field(accu,i); + coq_extra_args = coq_extra_args + (num - 2); + coq_env = Field(Field(accu,1),1); + pc = Code_val(coq_env); + accu = coq_env; + /* printf ("end\n"); */ + Next; + }; + /* printf ("true\n"); */ + } + Instruct(ACCUMULATE) { mlsize_t i, size; + print_instr("ACCUMULATE"); size = Wosize_val(coq_env); Alloc_small(accu, size + coq_extra_args + 1, Accu_tag); for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i); @@ -786,10 +893,11 @@ value coq_interprete coq_extra_args = Long_val(sp[2]); sp += 3; Next; - } - + } + Instruct(MAKEACCU) { int i; + print_instr("MAKEACCU"); Alloc_small(accu, coq_extra_args + 3, Accu_tag); Code_val(accu) = accumulate; Field(accu,1) = Field(coq_atom_tbl, *pc); @@ -802,6 +910,7 @@ value coq_interprete } Instruct(MAKEPROD) { + print_instr("MAKEPROD"); *--sp=accu; Alloc_small(accu,2,0); Field(accu, 0) = sp[0]; @@ -820,6 +929,7 @@ value coq_interprete } value coq_push_ra(value tcode) { + print_instr("push_ra"); coq_sp -= 3; coq_sp[0] = (value) tcode; coq_sp[1] = Val_unit; @@ -828,6 +938,7 @@ value coq_push_ra(value tcode) { } value coq_push_val(value v) { + print_instr("push_val"); *--coq_sp = v; return Val_unit; } @@ -836,6 +947,7 @@ value coq_push_arguments(value args) { int nargs,i; nargs = Wosize_val(args) - 2; coq_sp -= nargs; + print_instr("push_args");print_int(nargs); for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2); return Val_unit; } @@ -844,11 +956,13 @@ value coq_push_vstack(value stk) { int len,i; len = Wosize_val(stk); coq_sp -= len; - for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i); + print_instr("push_vstack");print_int(len); + for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i); return Val_unit; } value coq_interprete_ml(value tcode, value a, value e, value ea) { + print_instr("coq_interprete"); return coq_interprete((code_t)tcode, a, e, Long_val(ea)); } diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 233397b02..f94d2fb9e 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -25,11 +25,11 @@ asize_t coq_max_stack_size = Coq_max_stack_size; value coq_global_data; -value coq_global_transp; value coq_global_boxed; -int default_transp; +int coq_all_transp; value coq_atom_tbl; +int drawinstr; /* interp state */ long coq_saved_sp_offset; @@ -68,7 +68,6 @@ static void coq_scan_roots(scanning_action action) register value * i; /* Scan the global variables */ (*action)(coq_global_data, &coq_global_data); - (*action)(coq_global_transp, &coq_global_transp); (*action)(coq_global_boxed, &coq_global_boxed); (*action)(coq_atom_tbl, &coq_atom_tbl); /* Scan the stack */ @@ -92,20 +91,17 @@ void init_coq_stack() 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; - - default_transp = BOXED; +} - coq_global_transp = alloc_shr(requested_size, 0); - for (i = 0; i < requested_size; i++) - Field (coq_global_transp, i) = Val_unit; - +void init_coq_global_boxed(long requested_size) +{ + int i; coq_global_boxed = alloc_shr(requested_size, 0); for (i = 0; i < requested_size; i++) - Field (coq_global_boxed, i) = Val_unit; + Field (coq_global_boxed, i) = Val_true; } void init_coq_atom_tbl(long requested_size){ @@ -130,11 +126,14 @@ value init_coq_vm(value unit) /* ML */ else { /* Allocate the table of global and the stack */ + drawinstr=0; init_coq_stack(); init_coq_global_data(Coq_global_data_Size); + init_coq_global_boxed(40); init_coq_atom_tbl(40); /* Initialing the interpreter */ - forcable = Val_true; + coq_all_transp = 0; + forcable = Val_false; init_coq_interpreter(); /* Some predefined pointer code */ @@ -189,11 +188,6 @@ value get_coq_atom_tbl(value unit) /* ML */ return coq_atom_tbl; } -value get_coq_global_transp(value unit) /* ML */ -{ - return coq_global_transp; -} - value get_coq_global_boxed(value unit) /* ML */ { return coq_global_boxed; @@ -221,23 +215,16 @@ value realloc_coq_global_data(value size) /* ML */ value realloc_coq_global_boxed(value size) /* ML */ { mlsize_t requested_size, actual_size, i; - value new_global_transp, new_global_boxed; + value new_global_boxed; requested_size = Long_val(size); - actual_size = Wosize_val(coq_global_transp); + actual_size = Wosize_val(coq_global_boxed); if (requested_size >= actual_size) { requested_size = (requested_size + 0x100) & 0xFFFFFF00; - new_global_transp = alloc_shr(requested_size, 0); new_global_boxed = alloc_shr(requested_size, 0); - for (i = 0; i < actual_size; i++){ - initialize(&Field(new_global_transp, i), Field(coq_global_transp, i)); - initialize(&Field(new_global_boxed, i), - Field(coq_global_boxed, i)); - } - for (i = actual_size; i < requested_size; i++){ - Field (new_global_transp, i) = Val_long (0); + for (i = 0; i < actual_size; i++) + initialize(&Field(new_global_boxed, i), Field(coq_global_boxed, i)); + for (i = actual_size; i < requested_size; i++) Field (new_global_boxed, i) = Val_long (0); - } - coq_global_transp = new_global_transp; coq_global_boxed = new_global_boxed; } return Val_unit; @@ -254,17 +241,33 @@ value realloc_coq_atom_tbl(value size) /* ML */ 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++){ + 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 swap_coq_global_transp (value unit){ - if (default_transp==BOXED) default_transp = TRANSP; - else default_transp = BOXED; + +value coq_set_transp_value(value transp) +{ + coq_all_transp = (transp == Val_true); + return Val_unit; +} + +value get_coq_transp_value(value unit) +{ + return Val_bool(coq_all_transp); +} + +value coq_set_drawinstr(value unit) +{ + drawinstr = 1; return Val_unit; } +value coq_set_forcable (value unit) +{ + forcable = Val_true; + return Val_unit; +} diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index 0884f06a8..7c96e684e 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -35,10 +35,11 @@ extern value * coq_stack_threshold; /* global_data */ extern value coq_global_data; -extern value coq_global_transp; extern value coq_global_boxed; -extern int default_transp; +extern int coq_all_transp; extern value coq_atom_tbl; + +extern int drawinstr; /* interp state */ extern value * coq_sp; @@ -57,12 +58,13 @@ 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_global_transp(value unit); /* ML */ value get_coq_global_boxed(value unit); value realloc_coq_global_boxed(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_ */ +value coq_set_drawinstr(value unit); diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 48331a687..0d4a246a0 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -61,4 +61,60 @@ type fv_elem = FVnamed of identifier | FVrel of int type fv = fv_elem array +(* --- Pretty print *) +open Format +let rec instruction ppf = function + | Klabel lbl -> fprintf ppf "L%i:" lbl + | Kacc n -> fprintf ppf "\tacc %i" n + | Kenvacc n -> fprintf ppf "\tenvacc %i" n + | Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n + | Kpush -> fprintf ppf "\tpush" + | Kpop n -> fprintf ppf "\tpop %i" n + | Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl + | Kapply n -> fprintf ppf "\tapply %i" n + | Kappterm(n, m) -> + fprintf ppf "\tappterm %i, %i" n m + | Kreturn n -> fprintf ppf "\treturn %i" n + | Kjump -> fprintf ppf "\tjump" + | Krestart -> fprintf ppf "\trestart" + | Kgrab n -> fprintf ppf "\tgrab %i" n + | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n + | Kcograb n -> fprintf ppf "\tcograb %i" n + | Kclosure(lbl, n) -> + fprintf ppf "\tclosure L%i, %i" lbl n + | Kclosurerec(fv,init,lblt,lblb) -> + fprintf ppf "\tclosurerec"; + fprintf ppf "%i , %i, " fv init; + print_string "types = "; + Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt; + print_string " bodies = "; + Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; + (* nb fv, init, lbl types, lbl bodies *) + | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_kn id) + | Kconst cst -> + fprintf ppf "\tconst" + | Kmakeblock(n, m) -> + fprintf ppf "\tmakeblock %i, %i" n m + | Kmakeprod -> fprintf ppf "\tmakeprod" + | Kmakeswitchblock(lblt,lbls,_,sz) -> + fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz + | Kforce -> fprintf ppf "\tforce" + | Kswitch(lblc,lblb) -> + fprintf ppf "\tswitch"; + Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc; + Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; + | Kpushfield n -> + fprintf ppf "\tpushfield %i" n + | Kstop -> fprintf ppf "\tstop" + | Ksequence (c1,c2) -> + fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 +and instruction_list ppf = function + [] -> () + | Klabel lbl :: il -> + fprintf ppf "L%i:%a" lbl instruction_list il + | instr :: il -> + fprintf ppf "%a@ %a" instruction instr instruction_list il + +let draw_instr c = + fprintf std_formatter "@[<v 0>%a@]" instruction_list c diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 84882358a..a996f7505 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -58,3 +58,4 @@ type fv_elem = FVnamed of identifier | FVrel of int type fv = fv_elem array +val draw_instr : bytecodes -> unit diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 033f07319..022f913ba 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -48,7 +48,6 @@ let push_local sz r = nb_stack = r.nb_stack + 1; in_stack = (sz + 1) :: r.in_stack } - (* Table de relocation initiale *) let empty () = { nb_stack = 0; in_stack = []; @@ -128,7 +127,7 @@ let label_code = function let make_branch cont = match cont with - | (Kreturn _ as return) :: _ -> return, cont + | (Kreturn _ as return) :: cont' -> return, cont' | Klabel lbl as b :: _ -> b, cont | _ -> let b = Klabel(Label.create()) in b,b::cont @@ -467,8 +466,11 @@ let compile env c = let reloc = empty () in let init_code = compile_constr reloc c 0 [Kstop] in let fv = List.rev (!(reloc.in_env).fv_rev) in + if Options.print_bytecodes() then + (draw_instr init_code; draw_instr !fun_code); init_code,!fun_code, Array.of_list fv + let compile_constant_body env kn body opaque boxed = if opaque then BCconstant else match body with @@ -477,7 +479,16 @@ let compile_constant_body env kn body opaque boxed = let body = Declarations.force sb in match kind_of_term body with | Const kn' -> BCallias (get_allias env kn') + | Construct _ -> + let res = compile env body in + let to_patch = to_memory res in + BCdefined (false,to_patch) + | _ -> - let to_patch = to_memory (compile env body) in - BCdefined (boxed,to_patch) + let res = compile env body in + let to_patch = to_memory res in + (*if Options.print_bytecodes() then + (let init,fun_code,_= res in + draw_instr init; draw_instr fun_code);*) + BCdefined (boxed && Options.boxed_definitions (),to_patch) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index ab1f00d11..421949163 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -17,26 +17,7 @@ let patch_int buff pos n = String.unsafe_set buff (pos + 2) (Char.unsafe_chr (n asr 16)); String.unsafe_set buff (pos + 3) (Char.unsafe_chr (n asr 24)) -let cGETGLOBALBOXED = Char.unsafe_chr opGETGLOBALBOXED -let cGETGLOBAL = Char.unsafe_chr opGETGLOBAL - -let cPUSHGETGLOBALBOXED = Char.unsafe_chr opPUSHGETGLOBALBOXED -let cPUSHGETGLOBAL = Char.unsafe_chr opPUSHGETGLOBAL - -let is_PUSHGET c = - c = cPUSHGETGLOBAL || c = cPUSHGETGLOBALBOXED - -let patch_getglobal buff pos (boxed,n) = - let posinstr = pos - 4 in - let c = String.unsafe_get buff posinstr in - begin match is_PUSHGET c, boxed with - | true, true -> String.unsafe_set buff posinstr cPUSHGETGLOBALBOXED - | true, false -> String.unsafe_set buff posinstr cPUSHGETGLOBAL - | false, true -> String.unsafe_set buff posinstr cGETGLOBALBOXED - | false,false -> String.unsafe_set buff posinstr cGETGLOBAL - end; - patch_int buff pos n - + (* Buffering of bytecode *) let out_buffer = ref(String.create 1024) diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index fed577158..438da15dd 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -15,7 +15,6 @@ type emitcodes val length : emitcodes -> int val patch_int : emitcodes -> (*pos*)int -> int -> unit -val patch_getglobal : emitcodes -> (*pos*)int -> (bool*int) -> unit type to_patch = emitcodes * (patch list) * fv diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 3cc6f49d5..402a0fb97 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -43,8 +43,7 @@ let set_global v = [global_transp] contient la version transparente. [global_boxed] contient la version gelees. *) -external global_transp : unit -> values array = "get_coq_global_transp" -external global_boxed : unit -> values array = "get_coq_global_boxed" +external global_boxed : unit -> bool array = "get_coq_global_boxed" (* [realloc_global_data n] augmente de n la taille de [global_data] *) external realloc_global_boxed : int -> unit = "realloc_coq_global_boxed" @@ -54,14 +53,19 @@ let check_global_boxed n = let num_boxed = ref 0 -let set_boxed kn v = +let boxed_tbl = Hashtbl.create 53 + +let cst_opaque = ref KNpred.full + +let is_opaque kn = KNpred.mem kn !cst_opaque + +let set_global_boxed kn v = let n = !num_boxed in check_global_boxed n; - (global_transp()).(n) <- v; - let vb = val_of_constant_def kn v in - (global_boxed()).(n) <- vb; + (global_boxed()).(n) <- (is_opaque kn); + Hashtbl.add boxed_tbl kn n ; incr num_boxed; - n + set_global (val_of_constant_def n kn v) (* table pour les structured_constant et les annotations des switchs *) @@ -99,21 +103,19 @@ let rec slot_for_getglobal env kn = | BCdefined(boxed,(code,pl,fv)) -> let v = eval_to_patch env (code,pl,fv) in let pos = - if boxed then set_boxed kn v + if boxed then set_global_boxed kn v else set_global v in - let bpos = boxed,pos in - set_pos_constant ck bpos; - bpos + set_pos_constant ck pos; + pos | BCallias kn' -> - let bpos = slot_for_getglobal env kn' in - set_pos_constant ck bpos; - bpos + let pos = slot_for_getglobal env kn' in + set_pos_constant ck pos; + pos | BCconstant -> let v = val_of_constant kn in let pos = set_global v in - let bpos = false,pos in - set_pos_constant ck bpos; - bpos + set_pos_constant ck pos; + pos and slot_for_fv env fv= match fv with @@ -148,7 +150,7 @@ and eval_to_patch env (buff,pl,fv) = | Reloc_annot a, pos -> patch_int buff pos (slot_for_annot a) | Reloc_const sc, pos -> patch_int buff pos (slot_for_str_cst sc) | Reloc_getglobal kn, pos -> - patch_getglobal buff pos (slot_for_getglobal env kn) + patch_int buff pos (slot_for_getglobal env kn) in List.iter patch pl; let nfv = Array.length fv in @@ -160,4 +162,14 @@ and val_of_constr env c = let (_,fun_code,_ as ccfv) = compile env c in eval_to_patch env (to_memory ccfv) - +let set_transparent_const kn = + cst_opaque := KNpred.remove kn !cst_opaque; + List.iter (fun n -> (global_boxed()).(n) <- false) + (Hashtbl.find_all boxed_tbl kn) + +let set_opaque_const kn = + cst_opaque := KNpred.add kn !cst_opaque; + List.iter (fun n -> (global_boxed()).(n) <- true) + (Hashtbl.find_all boxed_tbl kn) + + diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 8bb0b890c..5fafbac49 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -4,3 +4,5 @@ open Environ val val_of_constr : env -> constr -> values +val set_opaque_const : kernel_name -> unit +val set_transparent_const : kernel_name -> unit diff --git a/kernel/environ.ml b/kernel/environ.ml index 3563a1340..d9569bca6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -23,7 +23,7 @@ type compilation_unit_name = dir_path * checksum type global = Constant | Inductive -type key = (bool*int) option ref +type key = int option ref type constant_key = constant_body * key type engagement = ImpredicativeSet diff --git a/kernel/environ.mli b/kernel/environ.mli index d570655ee..5be23b490 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -112,9 +112,9 @@ type constant_key exception NotEvaluated exception AllReadyEvaluated -val constant_key_pos : constant_key -> bool*int +val constant_key_pos : constant_key -> int val constant_key_body : constant_key -> constant_body -val set_pos_constant : constant_key -> (bool*int) -> unit +val set_pos_constant : constant_key -> int -> unit val lookup_constant_key : constant -> env -> constant_key val lookup_constant : constant -> env -> constant_body diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 1ca0fec4a..7e5e91944 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -514,7 +514,7 @@ let import (dp,mb,depends,engmt) digest senv = loads = (mp,mb)::senv.loads } -(** Remove the body of opaque constants in modules *) +(* Remove the body of opaque constants in modules *) let rec lighten_module mb = { mb with diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 41817c3e0..841bed98f 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -12,7 +12,7 @@ open Univ open Cbytecodes -(**** Test la structure des piles ****) +(* Test la structure des piles *) let compare_zipper z1 z2 = match z1, z2 with @@ -29,7 +29,7 @@ let rec compare_stack stk1 stk2 = else false | _, _ -> false -(**** Conversion ****) +(* Conversion *) let conv_vect fconv vect1 vect2 cu = let n = Array.length vect1 in if n = Array.length vect2 then @@ -247,7 +247,7 @@ let vconv pb env t1 t2 = let _ = Reduction.set_vm_conv_cmp vconv (*******************************************) -(**** Calcul de la forme normal d'un terme *) +(* Calcul de la forme normal d'un terme *) (*******************************************) let crazy_type = mkSet @@ -271,7 +271,7 @@ let invert_tag cst tag reloc_tbl = else () done;raise Not_found with Find_at j -> (j+1) - (*** Argggg, ces constructeurs de ... qui commencent a 1*) + (* Argggg, ces constructeurs de ... qui commencent a 1*) (* Build the substitution that replaces Rels by the appropriate inductives *) @@ -289,7 +289,7 @@ let constructor_instantiate mind mib params ctyp = if nparams = 0 then ctyp1 else let _,ctyp2 = decompose_prod_n nparams ctyp1 in - let sp = Array.to_list params in substl sp ctyp2 + let sp = List.rev (Array.to_list params) in substl sp ctyp2 let destApplication t = try destApplication t @@ -358,7 +358,7 @@ let build_branches_type (mind,_ as ind) mib mip params dep p rtbl = decl, codom in Array.mapi build_one_branch mip.mind_nf_lc -(** La fonction de normalisation *) +(* La fonction de normalisation *) let rec nf_val env v t = nf_whd env (whd_val v) t @@ -398,9 +398,8 @@ and nf_whd env whd typ = | Vatom_stk(Aid idkey, stk) -> let c,typ = constr_type_of_idkey env idkey in nf_stk env c typ stk - | Vatom_stk(Aiddef(idkey,_), stk) -> - let c,typ = constr_type_of_idkey env idkey in - nf_stk env c typ stk + | Vatom_stk(Aiddef(idkey,v), stk) -> + nf_whd env (whd_stack v stk) typ | Vatom_stk(Aind ind, stk) -> nf_stk env (mkInd ind) (type_of_ind env ind) stk | Vatom_stk(_,stk) -> assert false @@ -421,7 +420,6 @@ and nf_stk env c t stk = let _,_,codom = decompose_prod env typ in nf_stk env (mkApp(mkApp(fd,args),[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> - let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env t) in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mip.mind_nparams in @@ -489,11 +487,19 @@ and nf_args env vargs t = and nf_bargs env b t = let t = ref t in let len = bsize b in - Array.init len + let args = Array.create len crazy_type in + for i = 0 to len - 1 do + let _,dom,codom = decompose_prod env !t in + let c = nf_val env (bfield b i) dom in + args.(i) <- c; + t := subst1 c codom + done; + args +(* Array.init len (fun i -> let _,dom,codom = decompose_prod env !t in let c = nf_val env (bfield b i) dom in - t := subst1 c codom; c) + t := subst1 c codom; c) *) and nf_fun env f typ = let k = nb_rel env in @@ -527,11 +533,14 @@ and nf_cofix env cf = let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in mkCoFix (init,(name,cft,cfb)) + + let cbv_vm env c t = - if not (transp_values ()) then swap_global_transp (); + let transp = transp_values () in + if not transp then set_transp_values true; let v = val_of_constr env c in let c = nf_val env v t in - if not (transp_values ()) then swap_global_transp (); + if not transp then set_transp_values false; c diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 21fd4601b..ea84a4ea8 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -12,3 +12,25 @@ val vconv : conv_pb -> types conversion_function (***********************************************************************) (*s Reduction functions *) val cbv_vm : env -> constr -> types -> constr + + + + + +val nf_val : env -> values -> types -> constr + +val nf_whd : env -> Vm.whd -> types -> constr + +val nf_stk : env -> constr -> types -> Vm.stack -> constr + +val nf_args : env -> Vm.arguments -> types -> types * constr array + +val nf_bargs : env -> Vm.vblock -> types -> constr array + +val nf_fun : env -> Vm.vfun -> types -> constr + +val nf_fix : env -> Vm.vfix -> constr + +val nf_cofix : env -> Vm.vcofix -> constr + + diff --git a/kernel/vm.ml b/kernel/vm.ml index 80ecdf369..4482696ae 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -4,28 +4,13 @@ open Term open Conv_oracle open Cbytecodes -(* use transparant constant or not *) - -external swap_global_transp : unit -> unit = "swap_coq_global_transp" - -let transp_values = ref false - -let set_transp_values b = - if b = !transp_values then () - else ( - transp_values := not !(transp_values); - swap_global_transp ()) - -let transp_values _ = !transp_values - +external set_drawinstr : unit -> unit = "coq_set_drawinstr" (******************************************) (* Fonctions en plus du module Obj ********) (******************************************) - - external offset_closure : t -> int -> t = "coq_offset_closure" external offset : t -> int = "coq_offset" let first o = (offset_closure o (offset o)) @@ -41,6 +26,9 @@ external init_vm : unit -> unit = "init_coq_vm" let _ = init_vm () +external transp_values : unit -> bool = "get_coq_transp_value" +external set_transp_values : bool -> unit = "coq_set_transp_value" + (*******************************************) (* Le code machine ************************) (*******************************************) @@ -51,6 +39,7 @@ let fun_code v = tcode_of_obj (field (repr v) 0) external mkAccuCode : int -> tcode = "coq_makeaccu" external mkPopStopCode : int -> tcode = "coq_pushpop" +external mkAccuCond : int -> tcode = "coq_accucond" external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" external int_tcode : tcode -> int -> int = "coq_int_tcode" @@ -58,6 +47,8 @@ external int_tcode : tcode -> int -> int = "coq_int_tcode" external accumulate : unit -> tcode = "accumulate_code" let accumulate = accumulate () +external is_accumulate : tcode -> bool = "coq_is_accumulate_code" + let popstop_tbl = ref (Array.init 30 mkPopStopCode) let popstop_code i = @@ -313,7 +304,12 @@ let val_of_named id = val_of_idkey (VarKey id) let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v)) let val_of_constant c = val_of_idkey (ConstKey c) -let val_of_constant_def c v = val_of_atom(Aiddef(ConstKey c, v)) +let val_of_constant_def n c v = + let res = Obj.new_block accu_tag 2 in + set_field res 0 (repr (mkAccuCond n)); + set_field res 1 (repr (Aiddef(ConstKey c, v))); + val_of_obj res + (*************************************************) @@ -326,8 +322,7 @@ let rec whd_accu a stk = let stk = if nargs_of_accu a = 0 then stk else Zapp (args_of_accu a) :: stk in - - let at = atom_of_accu a in + let at = atom_of_accu a in match at with | Aid _ | Aiddef _ | Aind _ -> Vatom_stk(at, stk) | Afix_app(a,fa) -> whd_accu a (Zfix fa :: stk) @@ -335,7 +330,6 @@ let rec whd_accu a stk = external kind_of_closure : t -> int = "coq_kind_of_closure" - let whd_val : values -> whd = fun v -> let o = repr v in @@ -343,7 +337,7 @@ let whd_val : values -> whd = else let tag = tag o in if tag = accu_tag then - if fun_code o == accumulate then whd_accu (obj o) [] + if is_accumulate (fun_code o) then whd_accu (obj o) [] else if size o = 1 then Vsort(obj (field o 0)) else Vprod(obj o) @@ -405,8 +399,17 @@ let apply_fix_app vfa arg = push_arguments vargs; interprete (fun_code vf) (magic vf) (magic vf) (nargs vargs) -let apply_switch sw arg = +external set_forcable : unit -> unit = "coq_set_forcable" +let force_cofix v = + match whd_val v with + | Vcofix _ | Vcofix_app _ -> + push_ra stop; + set_forcable (); + interprete (fun_code v) (magic v) (magic v) 0 + | _ -> v +let apply_switch sw arg = + let arg = force_cofix arg in let tc = sw.sw_annot.tailcall in if tc then (push_ra stop;push_vstack sw.sw_stk) diff --git a/kernel/vm.mli b/kernel/vm.mli index d6e7f6eee..a4651cf7d 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -3,10 +3,11 @@ open Term open Cbytecodes open Cemitcodes -(* option for virtual machine *) + +val set_drawinstr : unit -> unit + val transp_values : unit -> bool val set_transp_values : bool -> unit -val swap_global_transp : unit -> unit (* le code machine *) type tcode @@ -60,7 +61,7 @@ val val_of_named : identifier -> values val val_of_named_def : identifier -> values -> values val val_of_constant : constant -> values -val val_of_constant_def : constant -> values -> values +val val_of_constant_def : int -> constant -> values -> values (* Destructors *) val whd_val : values -> whd diff --git a/lib/options.ml b/lib/options.ml index 2e8c53517..ec9f0cb13 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -108,3 +108,14 @@ let dump_it () = let _ = at_exit dump_it +(* Options for the virtual machine *) + +let print_bytecodes = ref false +let set_print_bytecodes b = print_bytecodes := b +let print_bytecodes _ = !print_bytecodes + + +let boxed_definitions = ref true +let set_boxed_definitions b = boxed_definitions := b +let boxed_definitions _ = !boxed_definitions + diff --git a/lib/options.mli b/lib/options.mli index d999425e9..bf935c76d 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -62,3 +62,13 @@ val dump : bool ref val dump_into_file : string -> unit val dump_string : string -> unit +(* Options for the virtual machine *) + + +val set_print_bytecodes : bool -> unit +val print_bytecodes : unit -> bool + +val set_boxed_definitions : bool -> unit +val boxed_definitions : unit -> bool + + diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 43e6b81cc..d09e167b1 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -111,8 +111,13 @@ GEXTEND Gram def_token: [ [ IDENT "Boxed";"Definition" -> (fun _ _ -> ()), (Global, Definition true) - | "Definition" -> (fun _ _ -> ()), (Global, Definition false) - | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition true) + | IDENT "Unboxed";"Definition" -> + (fun _ _ -> ()), (Global, Definition false) + | "Definition" -> + (fun _ _ -> ()), (Global, Definition false) + (*(Options.boxed_definitions())) *) + | IDENT "Local" -> + (fun _ _ -> ()), (Local, Definition (Options.boxed_definitions())) | IDENT "SubClass" -> Class.add_subclass_hook, (Global, SubClass) | IDENT "Local"; IDENT "SubClass" -> Class.add_subclass_hook, (Local, SubClass) ] ] @@ -319,10 +324,16 @@ GEXTEND Gram VernacInductive (f,indl) | IDENT "Boxed"; "Fixpoint"; recs = specifrec -> VernacFixpoint (recs,true) - | "Fixpoint"; recs = specifrec -> VernacFixpoint (recs,false) - | IDENT "Boxed"; "CoFixpoint"; corecs = specifcorec -> + | IDENT "Unboxed"; "Fixpoint"; recs = specifrec -> + VernacFixpoint (recs,false) + | "Fixpoint"; recs = specifrec -> + VernacFixpoint (recs,Options.boxed_definitions()) +(* | IDENT "Boxed"; "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint (corecs,true) - | "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint (corecs,false) + | IDENT "Unboxed"; "CoFixpoint"; corecs = specifcorec -> + VernacCoFixpoint (corecs,false) *) + | "CoFixpoint"; corecs = specifcorec -> + VernacCoFixpoint (corecs,false (*Options.boxed_definitions()*)) | IDENT "Scheme"; l = schemes -> VernacScheme l | f = finite_token; s = csort; id = identref; indpar = simple_binders_list; ":="; lc = constructor_list -> diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 9cf0d3a21..45237e101 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -103,6 +103,8 @@ GEXTEND Gram VernacAssumption (stre, bl) | IDENT "Boxed";"Definition";id = identref; b = def_body -> VernacDefinition ((Global,Definition true), id, b, (fun _ _ -> ())) + | IDENT "Unboxed";"Definition";id = identref; b = def_body -> + VernacDefinition ((Global,Definition false), id, b, (fun _ _ -> ())) | (f,d) = def_token; id = identref; b = def_body -> VernacDefinition (d, id, b, f) (* Gallina inductive declarations *) @@ -111,13 +113,18 @@ GEXTEND Gram VernacInductive (f,indl) | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (recs,true) - | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (recs,false) - | IDENT "Boxed"; "CoFixpoint"; + | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (recs,Options.boxed_definitions()) + (* | IDENT "Boxed"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> VernacCoFixpoint (corecs,true) + | IDENT "Unboxed"; "CoFixpoint"; + corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (corecs,false) *) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (corecs,false) + VernacCoFixpoint (corecs,false (*Options.boxed_definitions()*)) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ] ; gallina_ext: @@ -140,8 +147,10 @@ GEXTEND Gram | IDENT "Remark" -> Remark ] ] ; def_token: - [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition false) - | IDENT "Let" -> (fun _ _ -> ()), (Local, Definition false) + [ [ "Definition" -> + (fun _ _ -> ()), (Global, Definition (Options.boxed_definitions())) + | IDENT "Let" -> + (fun _ _ -> ()), (Local, Definition (Options.boxed_definitions())) | IDENT "SubClass" -> Class.add_subclass_hook, (Global, SubClass) | IDENT "Local"; IDENT "SubClass" -> Class.add_subclass_hook, (Local, SubClass) ] ] diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 9ec71866b..e91ea75b7 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -26,7 +26,10 @@ open Rawterm exception Elimconst exception Redelimination -let set_opaque_const = Conv_oracle.set_opaque_const +let set_opaque_const sp = + Conv_oracle.set_opaque_const sp; + Csymtable.set_opaque_const sp + let set_transparent_const sp = let cb = Global.lookup_constant sp in if cb.const_body <> None & cb.const_opaque then @@ -34,7 +37,8 @@ let set_transparent_const sp = (str "Cannot make" ++ spc () ++ Nametab.pr_global_env Idset.empty (ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); - Conv_oracle.set_transparent_const sp + Conv_oracle.set_transparent_const sp; + Csymtable.set_transparent_const sp let set_opaque_var = Conv_oracle.set_opaque_var let set_transparent_var = Conv_oracle.set_transparent_var diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 77d9233d1..1a221dd16 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -245,10 +245,11 @@ let add_inversion_lemma name env sigma t sort dep inv_op = let invProof = inversion_scheme env sigma t sort dep inv_op in let _ = declare_constant name - (DefinitionEntry { const_entry_body = invProof; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = true}, + (DefinitionEntry + { const_entry_body = invProof; + const_entry_type = None; + const_entry_opaque = false; + const_entry_boxed = true && (Options.boxed_definitions())}, IsProof Lemma) in () diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index b374a1845..e278ec243 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -687,8 +687,8 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) = apply_to_rels mext quantifiers_rev |])); const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = false}, - IsDefinition)) ; + const_entry_boxed = Options.boxed_definitions()}, + IsDefinition)) ; mext in let mmor = current_constant mor_name in @@ -994,7 +994,7 @@ let int_add_relation id a aeq refl sym trans = a_quantifiers_rev); const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = false}, + const_entry_boxed = Options.boxed_definitions()}, IsDefinition) in let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in let xreflexive_relation_class = @@ -1011,7 +1011,7 @@ let int_add_relation id a aeq refl sym trans = Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev; const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = false }, + const_entry_boxed = Options.boxed_definitions() }, IsDefinition) in let aeq_rel = { aeq_rel with @@ -1071,7 +1071,7 @@ let int_add_relation id a aeq refl sym trans = {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev; const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = false}, + const_entry_boxed = Options.boxed_definitions()}, IsDefinition) in let a_quantifiers_rev = diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 9f7de8503..987d42eea 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -15,7 +15,7 @@ Open Local Scope nat_scope. (** Factorial *) -Boxed Fixpoint fact (n:nat) : nat := +Fixpoint fact (n:nat) : nat := match n with | O => 1 | S n => S n * fact n diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index c575ba583..b4ce93819 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -26,6 +26,7 @@ Require Import Notations. Require Import Datatypes. Require Import Logic. +Unset Boxed Definitions. Open Scope nat_scope. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 0fd846b2f..6676ea3bf 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -9,6 +9,7 @@ (*i $Id$ i*) Require Import BinPos. +Unset Boxed Definitions. (**********************************************************************) (** Binary natural numbers *) diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 8e709a489..189e1d15e 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -12,6 +12,7 @@ (** Binary positive numbers *) (** Original development by Pierre Crégut, CNET, Lannion, France *) +Unset Boxed Definitions. Inductive positive : Set := | xI : positive -> positive diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index 85a3102a0..5c25ae966 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -13,7 +13,7 @@ Require Import Rfunctions. Require Import PartSum. Open Local Scope R_scope. -Boxed Definition C (n p:nat) : R := +Definition C (n p:nat) : R := INR (fact n) / (INR (fact p) * INR (fact (n - p))). Lemma pascal_step1 : forall n i:nat, (i <= n)%nat -> C n i = C n (n - i). diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 2f2a52d08..47fc4b016 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -13,7 +13,7 @@ Require Import Rfunctions. Require Import Rsqrt_def. Open Local Scope R_scope. (* Here is a continuous extension of Rsqrt on R *) -Boxed Definition sqrt (x:R) : R := +Definition sqrt (x:R) : R := match Rcase_abs x with | left _ => 0 | right a => Rsqrt (mknonnegreal x (Rge_le _ _ a)) diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 1acd611d5..1fdf145e9 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -107,7 +107,7 @@ Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real. (**********************************************************) (**********) -Boxed Fixpoint INR (n:nat) : R := +Fixpoint INR (n:nat) : R := match n with | O => 0 | S O => 1 @@ -121,7 +121,7 @@ Arguments Scope INR [nat_scope]. (**********************************************************) (**********) -Boxed Definition IZR (z:Z) : R := +Definition IZR (z:Z) : R := match z with | Z0 => 0 | Zpos n => INR (nat_of_P n) diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 3e1a9262d..324ebb98f 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -63,7 +63,7 @@ Qed. (* Power *) (*******************************) (*********) -Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R := +Fixpoint pow (r:R) (n:nat) {struct n} : R := match n with | O => 1 | S n => r * pow r n @@ -527,7 +527,7 @@ Qed. Ltac case_eq name := generalize (refl_equal name); pattern name at -1 in |- *; case name. -Boxed Definition powerRZ (x:R) (n:Z) := +Definition powerRZ (x:R) (n:Z) := match n with | Z0 => 1 | Zpos p => x ^ nat_of_P p @@ -670,7 +670,7 @@ Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z). (** Sum of n first naturals *) (*******************************) (*********) -Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := +Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := match n with | O => f 0%nat | S n' => (sum_nat_f_O f n' + f (S n'))%nat @@ -690,7 +690,7 @@ Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x). (** Sum *) (*******************************) (*********) -Boxed Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R := +Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R := match N with | O => f 0%nat | S i => sum_f_R0 f i + f (S i) diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 7f86f3f42..fe0ed965e 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -461,7 +461,7 @@ assert (H5 := IZN _ H4); elim H5; clear H5; intros N H5; elim (Rlt_irrefl _ H7) ] ]. Qed. -Boxed Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist := +Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist := match N with | O => cons y nil | S p => cons x (SubEquiN p (x + del) y del) diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index d35672404..4dcdebdd1 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -142,12 +142,12 @@ Record StepFun (a b:R) : Type := mkStepFun Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f). -Boxed Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := +Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := match projT2 (pre f) with | existT a b => a end. -Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R := +Fixpoint Int_SF (l k:Rlist) {struct l} : R := match l with | nil => 0 | cons a l' => @@ -159,7 +159,7 @@ Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R := end. (* Integral of step functions *) -Boxed Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R := +Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R := match Rle_dec a b with | left _ => Int_SF (subdivision_val f) (subdivision f) | right _ => - Int_SF (subdivision_val f) (subdivision f) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 30dfa6274..d850d7f89 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -195,13 +195,13 @@ apply Rinv_neq_0_compat; red in |- *; intro; rewrite H3 in H; Qed. (* Definition of log R+* -> R *) -Boxed Definition Rln (y:posreal) : R := +Definition Rln (y:posreal) : R := match ln_exists (pos y) (cond_pos y) with | existT a b => a end. (* Extension on R *) -Boxed Definition ln (x:R) : R := +Definition ln (x:R) : R := match Rlt_dec 0 x with | left a => Rln (mkposreal x a) | right a => 0 @@ -377,7 +377,7 @@ Qed. (* Definition of Rpower *) (******************************************************************) -Boxed Definition Rpower (x y:R) := exp (y * ln x). +Definition Rpower (x y:R) := exp (y * ln x). Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope. diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index b29fb6a98..85f5af5e0 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -17,7 +17,7 @@ Require Import Binomial. Open Local Scope R_scope. (* TT Ak; 1<=k<=N *) -Boxed Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R := +Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R := match N with | O => 1 | S p => prod_f_SO An p * An (S p) diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 6d3457229..9bab638af 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -28,7 +28,7 @@ Section sequence. Variable Un : nat -> R. (*********) -Boxed Fixpoint Rmax_N (N:nat) : R := +Fixpoint Rmax_N (N:nat) : R := match N with | O => Un 0 | S n => Rmax (Un (S n)) (Rmax_N n) diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index df750b9c6..1be5cacc6 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -15,7 +15,7 @@ Require Import SeqSeries. Require Import Ranalysis1. Open Local Scope R_scope. -Boxed Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := +Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := match N with | O => x | S n => diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 3d848a948..f8204834e 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -35,7 +35,7 @@ unfold Pser, exp_in in |- *. trivial. Defined. -Boxed Definition exp (x:R) : R := projT1 (exist_exp x). +Definition exp (x:R) : R := projT1 (exist_exp x). Lemma pow_i : forall i:nat, (0 < i)%nat -> 0 ^ i = 0. intros; apply pow_ne_zero. @@ -235,7 +235,7 @@ Qed. (* Definition of cosinus *) (*************************) -Boxed Definition cos (x:R) : R := +Definition cos (x:R) : R := match exist_cos (Rsqr x) with | existT a b => a end. @@ -356,7 +356,7 @@ Qed. (***********************) (* Definition of sinus *) -Boxed Definition sin (x:R) : R := +Definition sin (x:R) : R := match exist_sin (Rsqr x) with | existT a b => x * a end. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 10e7def9e..16e2ff325 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -17,6 +17,8 @@ Require Export Pnat. Require Import BinNat. Require Import Plus. Require Import Mult. + +Unset Boxed Definitions. (**********************************************************************) (** Binary integer numbers *) @@ -1035,4 +1037,4 @@ Definition Zabs_N (z:Z) := Definition Z_of_N (x:N) := match x with | N0 => Z0 | Npos p => Zpos p - end.
\ No newline at end of file + end. diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index bc92eca14..d49bbfc68 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -15,6 +15,8 @@ Require Import Zcompare. Require Import ZArith_dec. Require Import Sumbool. +Unset Boxed Definitions. + (** The decidability of equality and order relations over type [Z] give some boolean functions with the adequate specification. *) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index c4dca7121..025e03d4a 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -36,7 +36,7 @@ Open Local Scope Z_scope. *) -Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : +Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : Z * Z := match a with | xH => if Zge_bool b 2 then (0, 1) else (1, 0) diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 25b05cdc7..c45355133 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -36,6 +36,7 @@ Fixpoint log_inf (p:positive) : Z := | xO q => Zsucc (log_inf q) (* 2n *) | xI q => Zsucc (log_inf q) (* 2n+1 *) end. + Fixpoint log_sup (p:positive) : Z := match p with | xH => 0 (* 1 *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 62a6aaf14..d7ebad149 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -19,7 +19,7 @@ Open Local Scope Z_scope. (**********************************************************************) (** Minimum on binary integer numbers *) -Definition Zmin (n m:Z) := +Unboxed Definition Zmin (n m:Z) := match n ?= m return Z with | Eq => n | Lt => n diff --git a/toplevel/class.ml b/toplevel/class.ml index e0339768e..3d468d328 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -270,7 +270,7 @@ let build_id_coercion idf_opt source = { const_entry_body = mkCast (val_f, typ_f); const_entry_type = Some typ_f; const_entry_opaque = false; - const_entry_boxed = false} in + const_entry_boxed = Options.boxed_definitions()} in let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in ConstRef kn diff --git a/toplevel/command.ml b/toplevel/command.ml index a0cf3c40e..8eaab89d3 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -198,7 +198,7 @@ let declare_one_elimination ind = { const_entry_body = c; const_entry_type = t; const_entry_opaque = false; - const_entry_boxed = true }, + const_entry_boxed = Options.boxed_definitions() }, Decl_kinds.IsDefinition) in definition_message id; kn @@ -620,7 +620,7 @@ let build_scheme lnamedepindsort = let ce = { const_entry_body = decl; const_entry_type = Some decltype; const_entry_opaque = false; - const_entry_boxed = true } in + const_entry_boxed = Options.boxed_definitions() } in let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in ConstRef kn :: lrecref in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 1a90139b4..c79ff8421 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -142,6 +142,14 @@ let re_exec is_ide = Unix.handle_unix_error (Unix.execvp newprog) Sys.argv end +(*s options for the virtual machine *) +let unb_val = ref (fun _ -> ()) +let unb_def = ref (fun _ -> ()) +let no_vm = ref (fun _ -> ()) + +let set_vm_opt () = + !unb_val true;!unb_def false;!no_vm false + (*s Parsing of the command line. We no longer use [Arg.parse], in order to use share [Usage.print_usage] between coqtop and coqc. *) @@ -227,8 +235,13 @@ let parse_args is_ide = | "-unsafe" :: [] -> usage () | "-debug" :: rem -> set_debug (); parse rem - | "-unboxed-values" :: rem -> Vm.set_transp_values true; parse rem - | "-no-vm" :: rem -> Reduction.use_vm := false;parse rem + + | "-unboxed-values" :: rem -> + unb_val := Vm.set_transp_values ; parse rem + | "-unboxed-definitions" :: rem -> + unb_def := Options.set_boxed_definitions; parse rem + | "-no-vm" :: rem -> no_vm := (fun b -> Reduction.use_vm := b);parse rem + | "-draw-vm-instr" :: rem -> Vm.set_drawinstr ();parse rem | "-emacs" :: rem -> Options.print_emacs := true; parse rem | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0 @@ -297,6 +310,7 @@ let init is_ide = if_verbose print_header (); init_load_path (); inputstate (); + set_vm_opt (); engage (); if not !batch_mode then Declaremods.start_library !toplevel_name; init_library_roots (); diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c4e15b68b..e5a0681d8 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -753,6 +753,14 @@ let _ = let _ = declare_bool_option { optsync = false; + optname = "print the bytecode of global definitions"; + optkey = (SecondaryTable ("Print","Bytecode")); + optread = Options.print_bytecodes; + optwrite = (fun b -> Options.set_print_bytecodes b) } + +let _ = + declare_bool_option + { optsync = true; optname = "use of virtual machine inside the kernel"; optkey = (SecondaryTable ("Virtual","Machine")); optread = (fun () -> !Reduction.use_vm); @@ -760,11 +768,19 @@ let _ = let _ = declare_bool_option - { optsync = false; - optname = "transparent values for virtual machine"; + { optsync = true; + optname = "use of boxed definitions"; + optkey = (SecondaryTable ("Boxed","Definitions")); + optread = Options.boxed_definitions; + optwrite = (fun b -> Options.set_boxed_definitions b) } + +let _ = + declare_bool_option + { optsync = true; + optname = "use of boxed values"; optkey = (SecondaryTable ("Boxed","Values")); optread = Vm.transp_values; - optwrite = (fun b -> Vm.set_transp_values b) } + optwrite = (fun b -> Vm.set_transp_values (not b)) } let _ = declare_int_option |