aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/byterun/coq_fix_code.c246
-rw-r--r--kernel/byterun/coq_fix_code.h12
-rw-r--r--kernel/byterun/coq_interp.c8
-rw-r--r--kernel/byterun/coq_memory.c10
-rw-r--r--kernel/cbytegen.ml32
-rw-r--r--kernel/cbytegen.mli3
-rw-r--r--kernel/csymtable.ml9
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/reduction.ml19
-rw-r--r--kernel/reduction.mli4
-rw-r--r--kernel/term_typing.ml2
-rw-r--r--kernel/vconv.ml144
-rw-r--r--kernel/vconv.mli2
-rw-r--r--kernel/vm.ml5
-rw-r--r--kernel/vm.mli2
-rw-r--r--parsing/g_vernacnew.ml48
-rw-r--r--scripts/coqc.ml4
-rw-r--r--theories/Arith/Factorial.v2
-rw-r--r--theories/Reals/Raxioms.v2
-rw-r--r--theories/Reals/Rfunctions.v4
-rw-r--r--theories/Reals/RiemannInt_SF.v2
-rw-r--r--theories/Reals/Rprod.v2
-rw-r--r--theories/Reals/Rseries.v2
-rw-r--r--theories/Reals/Rsqrt_def.v2
-rw-r--r--toplevel/coqtop.ml22
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/vernacentries.ml6
27 files changed, 266 insertions, 292 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 446c76498..4616580df 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -18,6 +18,45 @@
#include "coq_instruct.h"
#include "coq_fix_code.h"
+#ifdef THREADED_CODE
+char ** coq_instr_table;
+char * coq_instr_base;
+int arity[STOP+1];
+
+void init_arity () {
+ /* instruction with zero operand */
+ arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]=
+ arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]=
+ arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=arity[PUSHACC6]=
+ arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]=arity[ENVACC4]=
+ arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]=arity[PUSHENVACC4]=
+ arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
+ arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]=
+ arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]=
+ arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
+ arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
+ arity[ACCUMULATE]=arity[STOP]=arity[FORCE]=arity[MAKEPROD]= 0;
+ /* instruction with one operand */
+ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
+ arity[PUSH_RETADDR]=
+ arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=arity[APPTERM3]=arity[RETURN]=
+ arity[GRAB]=arity[COGRAB]=
+ arity[OFFSETCLOSURE]=arity[PUSHOFFSETCLOSURE]=
+ arity[GETGLOBAL]=arity[PUSHGETGLOBAL]=
+ arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEACCU]=
+ arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=arity[PUSHFIELD]=
+ arity[ACCUMULATECOND]= 1;
+ /* instruction with two operands */
+ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=2;
+ /* instruction with four operands */
+ arity[MAKESWITCHBLOCK]=4;
+ /* instruction with arbitrary operands */
+ arity[CLOSUREREC]=arity[SWITCH]=0;
+}
+
+#endif /* THREADED_CODE */
+
+
void * coq_stat_alloc (asize_t sz)
{
void * result = malloc (sz);
@@ -25,16 +64,11 @@ void * coq_stat_alloc (asize_t sz)
return result;
}
-#ifdef THREADED_CODE
-
-char ** coq_instr_table;
-char * coq_instr_base;
-
value coq_makeaccu (value i) {
code_t q;
code_t res = coq_stat_alloc(8);
q = res;
- *q++ = (opcode_t)(coq_instr_table[MAKEACCU] - coq_instr_base);
+ *q++ = VALINSTR(MAKEACCU);
*q = (opcode_t)Int_val(i);
return (value)res;
}
@@ -43,178 +77,90 @@ 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++ = VALINSTR(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 == (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;
n = Int_val(i);
if (n == 0) {
res = coq_stat_alloc(4);
- *res = (opcode_t)(coq_instr_table[STOP] - coq_instr_base);
+ *res = VALINSTR(STOP);
return (value)res;
}
else {
code_t q;
res = coq_stat_alloc(12);
q = res;
- *q++ = (opcode_t)(coq_instr_table[POP] - coq_instr_base);
+ *q++ = VALINSTR(POP);
*q++ = (opcode_t)n;
- *q = (opcode_t)(coq_instr_table[STOP] - coq_instr_base);
+ *q = VALINSTR(STOP);
return (value)res;
}
}
-
-code_t coq_thread_code (code_t code, asize_t len){
- opcode_t instr;
- code_t p, q;
- code_t res = coq_stat_alloc(len);
- int i;
- q = res;
- len /= sizeof(opcode_t);
- for (p=code; p < code + len; /*nothing*/) {
- instr = *p++;
- *q++ = (opcode_t)(coq_instr_table[instr] - coq_instr_base);
- switch(instr){
- /* instruction with zero operand */
- case ACC0: case ACC1: case ACC2: case ACC3: case ACC4: case ACC5:
- case ACC6: case ACC7: case PUSH: case PUSHACC0: case PUSHACC1:
- case PUSHACC2: case PUSHACC3: case PUSHACC4: case PUSHACC5: case PUSHACC6:
- case PUSHACC7: case ENVACC1: case ENVACC2: case ENVACC3: case ENVACC4:
- case PUSHENVACC1: case PUSHENVACC2: case PUSHENVACC3: case PUSHENVACC4:
- case APPLY1: case APPLY2: case APPLY3: case RESTART: case OFFSETCLOSUREM2:
- case OFFSETCLOSURE0: case OFFSETCLOSURE2: case PUSHOFFSETCLOSUREM2:
- case PUSHOFFSETCLOSURE0: case PUSHOFFSETCLOSURE2:
- case CONST0: case CONST1: case CONST2: case CONST3:
- case PUSHCONST0: case PUSHCONST1: case PUSHCONST2: case PUSHCONST3:
- case ACCUMULATE: case STOP: case FORCE: case MAKEPROD:
- break;
-
- /* instruction with one operand */
- case ACC: case PUSHACC: case POP: case ENVACC: case PUSHENVACC:
- case PUSH_RETADDR:
- case APPLY: case APPTERM1: case APPTERM2: case APPTERM3: case RETURN:
- case GRAB: case COGRAB:
- case OFFSETCLOSURE: case PUSHOFFSETCLOSURE:
- case GETGLOBAL: case PUSHGETGLOBAL:
- /* 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;
-
- /* instruction with two operands */
- case APPTERM: case MAKEBLOCK: case CLOSURE:
- *q++ = *p++; *q++ = *p++;
- break;
-
- /* instruction with four operands */
- case MAKESWITCHBLOCK:
- *q++ = *p++; *q++ = *p++; *q++ = *p++; *q++ = *p++;
- break;
-
- /* instruction with arbitrary operands */
- case CLOSUREREC: {
- int i;
- uint32 n = 2*(*p) + 3; /* ndefs, nvars, start, typlbls,lbls*/
- for(i=0; i < n; i++) *q++ = *p++;
- }
- break;
-
- case SWITCH: {
- int i;
- uint32 sizes = *p;
- uint32 const_size = sizes & 0xFFFF;
- uint32 block_size = sizes >> 16;
- sizes = const_size + block_size + 1 ;/* sizes */
- for(i=0; i < sizes; i++) *q++ = *p++;
- }
- break;
-
- default:
- invalid_argument("Fatal error in coq_thread_code : bad opcode");
- break;
- }
- }
- if (p != code + len) fprintf(stderr, "error thread code\n");
- return res;
-}
-
-value coq_tcode_of_code(value code, value len){
- return (value)coq_thread_code((code_t)code,(asize_t) Long_val(len));
-}
-#else
-
-value coq_makeaccu (value i) {
- code_t q;
- code_t res = coq_stat_alloc(8);
- q = res;
- *q++ = (opcode_t)MAKEACCU;
- *q = (opcode_t)Int_val(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);
+ res = Is_instruction(q,ACCUMULATECOND) || Is_instruction(q,ACCUMULATE);
return Val_bool(res);
}
-value coq_pushpop (value i) {
- code_t res;
- int n;
- n = Int_val(i);
- if (n == 0) {
- res = coq_stat_alloc(4);
- *res = (opcode_t)STOP;
- return (value)res;
- }
- else {
- res = coq_stat_alloc(12);
- q = res;
- *q++ = (opcode_t)POP;
- *q++ = (opcode_t)n;
- *q = (opcode_t)STOP;
- return (value)res;
- }
+#ifdef ARCH_BIG_ENDIAN
+#define Reverse_32(dst,src) { \
+ char * _p, * _q; \
+ char _a, _b; \
+ _p = (char *) (src); \
+ _q = (char *) (dst); \
+ _a = _p[0]; \
+ _b = _p[1]; \
+ _q[0] = _p[3]; \
+ _q[1] = _p[2]; \
+ _q[3] = _a; \
+ _q[2] = _b; \
}
+#define COPY32(dst,src) Reverse_32(dst,src)
+#else
+#define COPY32(dst,src) (*dst=*src)
+#endif /* ARCH_BIG_ENDIAN */
-value coq_tcode_of_code(value s, value size)
-{
- void * new_s = coq_stat_alloc(Int_val(size));
- memmove(new_s, &Byte(s, 0), Int_val(size));
- return (value)new_s;
+value coq_tcode_of_code (value code, value size) {
+ code_t p, q, res;
+ asize_t len = (asize_t) Long_val(size);
+ res = coq_stat_alloc(len);
+ q = res;
+ len /= sizeof(opcode_t);
+ for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {
+ opcode_t instr;
+ COPY32(&instr,p);
+ p++;
+ if (instr < 0 || instr > STOP){
+ instr = STOP;
+ };
+ *q++ = VALINSTR(instr);
+ if (instr == SWITCH) {
+ uint32 i, sizes, const_size, block_size;
+ COPY32(q,p); p++;
+ sizes=*q++;
+ const_size = sizes & 0xFFFF;
+ block_size = sizes >> 16;
+ sizes = const_size + block_size;
+ for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; };
+ } else if (instr == CLOSUREREC) {
+ uint32 i, n;
+ COPY32(q,p); p++; /* ndefs */
+ n = 3 + 2*(*q); /* ndefs, nvars, start, typlbls,lbls*/
+ q++;
+ for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
+ } else {
+ uint32 i, ar;
+ ar = arity[instr];
+ for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
+ }
+ }
+ return (value)res;
}
-
-#endif /* THREADED_CODE */
-
-
-
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index e3296c0da..035d5b9b1 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -18,11 +18,13 @@ void * coq_stat_alloc (asize_t sz);
#ifdef THREADED_CODE
extern char ** coq_instr_table;
extern char * coq_instr_base;
-#define Is_instruction(i1,i2) \
- (*i1 == (opcode_t)(coq_instr_table[i2] - coq_instr_base))
-#else
-#define Is_instruction(i1,i2) (*i1 == i2)
-#endif
+void init_arity();
+#define VALINSTR(instr) ((opcode_t)(coq_instr_table[instr] - coq_instr_base))
+#else
+#define VALINSTR(instr) instr
+#endif /* THREADED_CODE */
+
+#define Is_instruction(pc,instr) (*pc == VALINSTR(instr))
value coq_tcode_of_code(value code, value len);
value coq_makeaccu (value i);
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 692baa7e7..48d91e4dc 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -55,11 +55,11 @@ sp is a local copy of the global variable extern_sp. */
# define Next break
#endif
-/*#define _COQ_DEBUG_*/
+/*#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)
+# 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)
@@ -164,7 +164,9 @@ value coq_interprete
#else
opcode_t curr_instr;
#endif
+ print_instr("Enter Interpreter");
if (coq_pc == NULL) { /* Interpreter is initializing */
+ print_instr("Interpreter is initializing");
#ifdef THREADED_CODE
coq_instr_table = (char **) coq_jumptable;
coq_instr_base = coq_Jumptbl_base;
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index f94d2fb9e..db6aacb92 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -124,9 +124,11 @@ value init_coq_vm(value unit) /* ML */
if (coq_vm_initialized == 1) {
fprintf(stderr,"already open \n");fflush(stderr);}
else {
-
- /* Allocate the table of global and the stack */
drawinstr=0;
+#ifdef THREADED_CODE
+ init_arity();
+#endif /* THREADED_CODE */
+ /* Allocate the table of global and the stack */
init_coq_stack();
init_coq_global_data(Coq_global_data_Size);
init_coq_global_boxed(40);
@@ -138,9 +140,7 @@ value init_coq_vm(value unit) /* ML */
/* Some predefined pointer code */
accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t));
- *accumulate = ACCUMULATE;
- accumulate =
- (code_t) coq_tcode_of_code((value)accumulate, Val_int(sizeof(opcode_t)));
+ *accumulate = VALINSTR(ACCUMULATE);
/* Initialize GC */
if (coq_prev_scan_roots_hook == NULL)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 108dadbb7..40965d2f5 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -466,29 +466,27 @@ 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 body opaque boxed =
if opaque then BCconstant
else match body with
| None -> BCconstant
| Some sb ->
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 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)
+ if boxed then
+ let res = compile env body in
+ let to_patch = to_memory res in
+ BCdefined(true, to_patch)
+ else
+ 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 res = compile env body in
+ let to_patch = to_memory res in
+ BCdefined (false, to_patch)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 0e7434e53..135afb1e2 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -12,5 +12,6 @@ val compile : env -> constr -> bytecodes * bytecodes * fv
val compile_constant_body :
env -> constr_substituted option -> bool -> bool -> body_code
- (* opaque *) (* boxed *)
+ (* opaque *) (* boxed *)
+
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index f9f03e348..73e10df65 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -8,6 +8,9 @@ open Environ
open Cbytegen
open Cemitcodes
+
+open Format
+
external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
external free_tcode : tcode -> unit = "coq_static_free"
external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
@@ -95,6 +98,8 @@ let slot_for_annot key =
Hashtbl.add annot_tbl key n;
n
+open Format
+
let rec slot_for_getglobal env kn =
let ck = lookup_constant_key kn env in
try constant_key_pos ck
@@ -159,7 +164,9 @@ and eval_to_patch env (buff,pl,fv) =
eval_tcode tc vm_env
and val_of_constr env c =
- let (_,fun_code,_ as ccfv) = compile env c in
+ let (_,fun_code,_ as ccfv) =
+ try compile env c
+ with e -> print_string "can not compile \n";print_flush();raise e in
eval_to_patch env (to_memory ccfv)
let set_transparent_const kn =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a6d7ff65b..6d16632cd 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -149,7 +149,6 @@ let lookup_named id env =
Sign.lookup_named id env.env_named_context
-
(* A local const is evaluable if it is defined *)
let evaluable_named id env =
try
@@ -165,6 +164,7 @@ let push_named d env =
match body with
| None -> ref (VKaxiom id)
| Some c -> ref (VKdef(c,env))
+
in
{ env with
env_named_context = Sign.add_named_decl d env.env_named_context;
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 85d668f7a..156e3a44a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -341,19 +341,19 @@ let conv_leq_vecti env v1 v2 =
v2
(* option for conversion *)
-let use_vm = ref true
-let vm_fconv = ref (fun _ _ _ _ -> error "VM not installed")
+
+let vm_fconv = ref fconv
+
+let set_default_vm_conv _ = vm_fconv := fconv
let set_vm_conv_cmp f = vm_fconv := f
-let vm_conv cv_pb env t1 t2 =
- if eq_constr t1 t2 then
- Constraint.empty
- else if !use_vm then
- try !vm_fconv cv_pb env t1 t2
- with Not_found | Invalid_argument _ ->
+let vm_conv cv_pb env t1 t2 =
+ try
+ !vm_fconv cv_pb env t1 t2
+ with Not_found | Invalid_argument _ ->
(* If compilation fails, fall-back to closure conversion *)
clos_fconv cv_pb env t1 t2
- else clos_fconv cv_pb env t1 t2
+
let vm_conv_leq_vecti env v1 v2 =
array_fold_left2_i
@@ -366,6 +366,7 @@ let vm_conv_leq_vecti env v1 v2 =
v1
v2
+let vm_conv_leq = vm_conv CUMUL
(*
let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";;
let conv_leq env t1 t2 =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index ca4ab8c94..5d383e61e 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -44,10 +44,12 @@ val conv_leq : types conversion_function
val conv_leq_vecti : types array conversion_function
(* option for conversion *)
-val use_vm : bool ref
+
+val set_default_vm_conv : unit -> unit
val set_vm_conv_cmp : (conv_pb -> types conversion_function) -> unit
val vm_conv : conv_pb -> types conversion_function
val vm_conv_leq_vecti : types array conversion_function
+val vm_conv_leq : types conversion_function
(************************************************************************)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 57c1710ff..360d3d94c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -29,7 +29,7 @@ let constrain_type env j cst1 = function
| Some t ->
let (tj,cst2) = infer_type env t in
let cst3 =
- try conv_leq env j.uj_type tj.utj_val
+ try vm_conv_leq env j.uj_type tj.utj_val
with NotConvertible -> error_actual_type env j tj.utj_val in
let typ =
if t = tj.utj_val then t else
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 841bed98f..8105bcae4 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -12,6 +12,7 @@ open Univ
open Cbytecodes
+
(* Test la structure des piles *)
let compare_zipper z1 z2 =
@@ -40,31 +41,33 @@ let conv_vect fconv vect1 vect2 cu =
!rcu
else raise NotConvertible
-let rec conv_val infos pb k v1 v2 cu =
- if v1 == v2 then cu else conv_whd infos pb k (whd_val v1) (whd_val v2) cu
+let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
+
+let rec conv_val pb k v1 v2 cu =
+ if v1 == v2 then cu else conv_whd pb k (whd_val v1) (whd_val v2) cu
-and conv_whd infos pb k whd1 whd2 cu =
+and conv_whd pb k whd1 whd2 cu =
match whd1, whd2 with
| Vsort s1, Vsort s2 -> sort_cmp pb s1 s2 cu
| Vprod p1, Vprod p2 ->
- let cu = conv_val infos CONV k (dom p1) (dom p2) cu in
- conv_fun infos pb k (codom p1) (codom p2) cu
- | Vfun f1, Vfun f2 -> conv_fun infos CONV k f1 f2 cu
- | Vfix f1, Vfix f2 -> conv_fix infos k f1 f2 cu
+ let cu = conv_val CONV k (dom p1) (dom p2) cu in
+ conv_fun pb k (codom p1) (codom p2) cu
+ | Vfun f1, Vfun f2 -> conv_fun CONV k f1 f2 cu
+ | Vfix f1, Vfix f2 -> conv_fix k f1 f2 cu
| Vfix_app fa1, Vfix_app fa2 ->
let f1 = fix fa1 in
let args1 = args_of_fix fa1 in
let f2 = fix fa2 in
let args2 = args_of_fix fa2 in
- conv_arguments infos k args1 args2 (conv_fix infos k f1 f2 cu)
+ conv_arguments k args1 args2 (conv_fix k f1 f2 cu)
| Vcofix cf1, Vcofix cf2 ->
- conv_cofix infos k cf1 cf2 cu
+ conv_cofix k cf1 cf2 cu
| Vcofix_app cfa1, Vcofix_app cfa2 ->
let cf1 = cofix cfa1 in
let args1 = args_of_cofix cfa1 in
let cf2 = cofix cfa2 in
let args2 = args_of_cofix cfa2 in
- conv_arguments infos k args1 args2 (conv_cofix infos k cf1 cf2 cu)
+ conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu)
| Vconstr_const i1, Vconstr_const i2 ->
if i1 = i2 then cu else raise NotConvertible
| Vconstr_block b1, Vconstr_block b2 ->
@@ -72,113 +75,111 @@ and conv_whd infos pb k whd1 whd2 cu =
if btag b1 = btag b2 && sz = bsize b2 then
let rcu = ref cu in
for i = 0 to sz - 1 do
- rcu := conv_val infos CONV k (bfield b1 i) (bfield b2 i) !rcu
+ rcu := conv_val CONV k (bfield b1 i) (bfield b2 i) !rcu
done;
!rcu
else raise NotConvertible
| Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
- conv_atom infos pb k a1 stk1 a2 stk2 cu
- | _, Vatom_stk(Aiddef(_,v),stk) ->
- conv_whd infos pb k whd1 (whd_stack v stk) cu
- | Vatom_stk(Aiddef(_,v),stk), _ ->
- conv_whd infos pb k (whd_stack v stk) whd2 cu
+ conv_atom pb k a1 stk1 a2 stk2 cu
+ | _, Vatom_stk(Aiddef(_,v) as a2,stk) ->
+ conv_whd pb k whd1 (force_whd v stk) cu
+ | Vatom_stk(Aiddef(_,v) as a1,stk), _ ->
+ conv_whd pb k (force_whd v stk) whd2 cu
| _, _ -> raise NotConvertible
-and conv_atom infos pb k a1 stk1 a2 stk2 cu =
+and conv_atom pb k a1 stk1 a2 stk2 cu =
match a1, a2 with
| Aind (kn1,i1), Aind(kn2,i2) ->
- if i1 = i2 && mind_equiv infos kn1 kn2 then
- conv_stack infos k stk1 stk2 cu
+ if i1 = i2 && mind_equiv !infos kn1 kn2 && compare_stack stk1 stk2 then
+ conv_stack k stk1 stk2 cu
else raise NotConvertible
| Aid ik1, Aid ik2 ->
- if ik1 = ik2 then conv_stack infos k stk1 stk2 cu
+ if ik1 = ik2 && compare_stack stk1 stk2 then
+ conv_stack k stk1 stk2 cu
else raise NotConvertible
| Aiddef(ik1,v1), Aiddef(ik2,v2) ->
begin
try
- if ik1 = ik2 then conv_stack infos k stk1 stk2 cu
+ if ik1 = ik2 && compare_stack stk1 stk2 then
+ conv_stack k stk1 stk2 cu
else raise NotConvertible
with NotConvertible ->
if oracle_order ik1 ik2 then
- conv_whd infos pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
- else conv_whd infos pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
+ conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
+ else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
end
| Aiddef(ik1,v1), _ ->
- conv_whd infos pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
+ conv_whd pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
| _, Aiddef(ik2,v2) ->
- conv_whd infos pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
+ conv_whd pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
| Afix_app _, _ | _, Afix_app _ | Aswitch _, _ | _, Aswitch _ ->
Util.anomaly "Vconv.conv_atom : Vm.whd_val doesn't work"
| _, _ -> raise NotConvertible
+
+and conv_stack k stk1 stk2 cu =
+ match stk1, stk2 with
+ | [], [] -> cu
+ | Zapp args1 :: stk1, Zapp args2 :: stk2 ->
+ conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu)
+ | Zfix fa1 :: stk1, Zfix fa2 :: stk2 ->
+ let f1 = fix fa1 in
+ let args1 = args_of_fix fa1 in
+ let f2 = fix fa2 in
+ let args2 = args_of_fix fa2 in
+ conv_stack k stk1 stk2
+ (conv_arguments k args1 args2 (conv_fix k f1 f2 cu))
+ | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
+ if eq_tbl sw1 sw2 then
+ let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
+ let rcu = ref (conv_val CONV k vt1 vt2 cu) in
+ let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
+ for i = 0 to Array.length b1 - 1 do
+ rcu :=
+ conv_val CONV (k + fst b1.(i))
+ (snd b1.(i)) (snd b2.(i)) !rcu
+ done;
+ conv_stack k stk1 stk2 !rcu
+ else raise NotConvertible
+ | _, _ -> raise NotConvertible
-and conv_stack infos k stk1 stk2 cu =
- if compare_stack stk1 stk2 then
- let rec conv_rec stk1 stk2 cu =
- match stk1, stk2 with
- | [], [] -> cu
- | Zapp args1 :: stk1, Zapp args2 :: stk2 ->
- conv_rec stk1 stk2 (conv_arguments infos k args1 args2 cu)
- | Zfix fa1 :: stk1, Zfix fa2 :: stk2 ->
- let f1 = fix fa1 in
- let args1 = args_of_fix fa1 in
- let f2 = fix fa2 in
- let args2 = args_of_fix fa2 in
- conv_rec stk1 stk2
- (conv_arguments infos k args1 args2 (conv_fix infos k f1 f2 cu))
- | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
- if eq_tbl sw1 sw2 then
- let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
- let rcu = ref (conv_val infos CONV k vt1 vt2 cu) in
- let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
- for i = 0 to Array.length b1 - 1 do
- rcu :=
- conv_val infos CONV (k + fst b1.(i))
- (snd b1.(i)) (snd b2.(i)) !rcu
- done;
- conv_rec stk1 stk2 !rcu
- else raise NotConvertible
- | _, _ -> raise NotConvertible
- in conv_rec stk1 stk2 cu
- else raise NotConvertible
-
-and conv_fun infos pb k f1 f2 cu =
+and conv_fun pb k f1 f2 cu =
if f1 == f2 then cu
else
let arity,b1,b2 = decompose_vfun2 k f1 f2 in
- conv_val infos pb (k+arity) b1 b2 cu
+ conv_val pb (k+arity) b1 b2 cu
-and conv_fix infos k f1 f2 cu =
+and conv_fix k f1 f2 cu =
if f1 == f2 then cu
else
if check_fix f1 f2 then
let tf1 = types_of_fix f1 in
let tf2 = types_of_fix f2 in
- let cu = conv_vect (conv_val infos CONV k) tf1 tf2 cu in
+ let cu = conv_vect (conv_val CONV k) tf1 tf2 cu in
let bf1 = bodies_of_fix k f1 in
let bf2 = bodies_of_fix k f2 in
- conv_vect (conv_fun infos CONV (k + (fix_ndef f1))) bf1 bf2 cu
+ conv_vect (conv_fun CONV (k + (fix_ndef f1))) bf1 bf2 cu
else raise NotConvertible
-and conv_cofix infos k cf1 cf2 cu =
+and conv_cofix k cf1 cf2 cu =
if cf1 == cf2 then cu
else
if check_cofix cf1 cf2 then
let tcf1 = types_of_cofix cf1 in
let tcf2 = types_of_cofix cf2 in
- let cu = conv_vect (conv_val infos CONV k) tcf1 tcf2 cu in
+ let cu = conv_vect (conv_val CONV k) tcf1 tcf2 cu in
let bcf1 = bodies_of_cofix k cf1 in
let bcf2 = bodies_of_cofix k cf2 in
- conv_vect (conv_val infos CONV (k + (cofix_ndef cf1))) bcf1 bcf2 cu
+ conv_vect (conv_val CONV (k + (cofix_ndef cf1))) bcf1 bcf2 cu
else raise NotConvertible
-and conv_arguments infos k args1 args2 cu =
+and conv_arguments k args1 args2 cu =
if args1 == args2 then cu
else
let n = nargs args1 in
if n = nargs args2 then
let rcu = ref cu in
for i = 0 to n - 1 do
- rcu := conv_val infos CONV k (arg args1 i) (arg args2 i) !rcu
+ rcu := conv_val CONV k (arg args1 i) (arg args2 i) !rcu
done;
!rcu
else raise NotConvertible
@@ -237,14 +238,21 @@ let vconv pb env t1 t2 =
let cu =
try conv_eq pb t1 t2 Constraint.empty
with NotConvertible ->
- let infos = create_clos_infos betaiotazeta env in
+ infos := create_clos_infos betaiotazeta env;
let v1 = val_of_constr env t1 in
let v2 = val_of_constr env t2 in
- let cu = conv_val infos pb (nb_rel env) v1 v2 Constraint.empty in
+ let cu = conv_val pb (nb_rel env) v1 v2 Constraint.empty in
cu
in cu
-
+
+let use_vm = ref true
let _ = Reduction.set_vm_conv_cmp vconv
+let set_use_vm b =
+ use_vm := b;
+ if b then Reduction.set_vm_conv_cmp vconv
+ else Reduction.set_default_vm_conv ()
+
+let use_vm _ = !use_vm
(*******************************************)
(* Calcul de la forme normal d'un terme *)
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index ea84a4ea8..fa6026509 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -7,6 +7,8 @@ open Reduction
(***********************************************************************)
(*s conversion functions *)
+val use_vm : unit -> bool
+val set_use_vm : bool -> unit
val vconv : conv_pb -> types conversion_function
(***********************************************************************)
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 4482696ae..0aa4f1ff4 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -432,6 +432,11 @@ let rec whd_stack v stk =
if is_accu v then whd_accu (magic v) stk
else whd_stack (apply_switch sw v) stkt
+let rec force_whd v stk =
+ match whd_stack v stk with
+ | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk
+ | res -> res
+
(* Function *)
diff --git a/kernel/vm.mli b/kernel/vm.mli
index a4651cf7d..b5fd9b9db 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -104,6 +104,6 @@ val arg : arguments -> int -> values
(* Evaluation *)
val whd_stack : values -> stack -> whd
-
+val force_whd : values -> stack -> whd
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 1ce6f16ba..c2aa50580 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -117,14 +117,8 @@ GEXTEND Gram
VernacFixpoint (recs,false)
| "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 (*Options.boxed_definitions()*))
+ VernacCoFixpoint (corecs,false)
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
;
gallina_ext:
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index a7b1fd355..82fc01bb2 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -154,7 +154,9 @@ let parse_args () =
|"-batch"|"-nois"
|"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
|"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate" |"-strict-implicit"
- |"-dont-load-proofs"|"-impredicative-set"|"-no-vm" as o) :: rem ->
+ |"-dont-load-proofs"|"-impredicative-set"|"-no-vm"
+ | "-unboxed-values" | "-unboxed-definitions" | "-draw-vm-instr"
+ as o) :: rem ->
parse (cfiles,o::args) rem
| ("-v"|"--version") :: _ ->
Usage.version ()
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 987d42eea..9f7de8503 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -15,7 +15,7 @@ Open Local Scope nat_scope.
(** Factorial *)
-Fixpoint fact (n:nat) : nat :=
+Boxed Fixpoint fact (n:nat) : nat :=
match n with
| O => 1
| S n => S n * fact n
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 1fdf145e9..cb9086317 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.
(**********************************************************)
(**********)
-Fixpoint INR (n:nat) : R :=
+Boxed Fixpoint INR (n:nat) : R :=
match n with
| O => 0
| S O => 1
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 324ebb98f..295c59ca1 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -63,7 +63,7 @@ Qed.
(* Power *)
(*******************************)
(*********)
-Fixpoint pow (r:R) (n:nat) {struct n} : R :=
+Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R :=
match n with
| O => 1
| S n => r * pow r n
@@ -670,7 +670,7 @@ Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z).
(** Sum of n first naturals *)
(*******************************)
(*********)
-Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat :=
+Boxed 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
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 4dcdebdd1..9370530a0 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -147,7 +147,7 @@ Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=
| existT a b => a
end.
-Fixpoint Int_SF (l k:Rlist) {struct l} : R :=
+Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R :=
match l with
| nil => 0
| cons a l' =>
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 85f5af5e0..b29fb6a98 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 *)
-Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R :=
+Boxed 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 9bab638af..6d3457229 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -28,7 +28,7 @@ Section sequence.
Variable Un : nat -> R.
(*********)
-Fixpoint Rmax_N (N:nat) : R :=
+Boxed 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 1be5cacc6..df750b9c6 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.
-Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
+Boxed Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
match N with
| O => x
| S n =>
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c79ff8421..77c7e9793 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -143,12 +143,15 @@ let re_exec is_ide =
end
(*s options for the virtual machine *)
-let unb_val = ref (fun _ -> ())
-let unb_def = ref (fun _ -> ())
-let no_vm = ref (fun _ -> ())
+
+let boxed_val = ref true
+let boxed_def = ref true
+let use_vm = ref true
let set_vm_opt () =
- !unb_val true;!unb_def false;!no_vm false
+ Vm.set_transp_values (not !boxed_val);
+ Options.set_boxed_definitions !boxed_def;
+ Vconv.set_use_vm !use_vm
(*s Parsing of the command line.
We no longer use [Arg.parse], in order to use share [Usage.print_usage]
@@ -237,11 +240,12 @@ let parse_args is_ide =
| "-debug" :: rem -> set_debug (); 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
+ boxed_val := false; parse rem
+ | "-boxed-definitions" :: rem ->
+ boxed_def := true; parse rem
+ | "-no-vm" :: rem -> use_vm := false; parse rem
+ | "-draw-vm-instr" :: rem -> Vm.set_drawinstr ();
+ Options.set_print_bytecodes true; parse rem
| "-emacs" :: rem -> Options.print_emacs := true; parse rem
| "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ee189377d..c05220989 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -182,7 +182,7 @@ let declare_projections indsp coers fields =
const_entry_body = proj;
const_entry_type = Some projtyp;
const_entry_opaque = false;
- const_entry_boxed = false } in
+ const_entry_boxed = Options.boxed_definitions() } in
let k = (DefinitionEntry cie,IsDefinition) in
let kn = declare_internal_constant fid k in
Options.if_verbose message (string_of_id fid ^" is defined");
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a7df13785..9df803dfd 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -776,12 +776,12 @@ let _ =
{ optsync = true;
optname = "use of virtual machine inside the kernel";
optkey = (SecondaryTable ("Virtual","Machine"));
- optread = (fun () -> !Reduction.use_vm);
- optwrite = (fun b -> Reduction.use_vm := b) }
+ optread = (fun () -> Vconv.use_vm ());
+ optwrite = (fun b -> Vconv.set_use_vm b) }
let _ =
declare_bool_option
- { optsync = true;
+ { optsync = false;
optname = "use of boxed definitions";
optkey = (SecondaryTable ("Boxed","Definitions"));
optread = Options.boxed_definitions;
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 18:48:59 +0000