diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-10-19 14:46:25 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-10-19 14:49:57 +0200 |
commit | 6fbe3c850bac9cbdfa64dbdcca7bd60dc7862190 (patch) | |
tree | 0e1ffc91f1ba28428c8908995108d05bd9835c33 /kernel | |
parent | 1124ff6dd8fe4d04de8321375de101a42a2131f8 (diff) |
More comments in VM.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/byterun/coq_instruct.h | 2 | ||||
-rw-r--r-- | kernel/byterun/coq_interp.c | 15 | ||||
-rw-r--r-- | kernel/cbytegen.ml | 1 | ||||
-rw-r--r-- | kernel/make-opcodes | 3 | ||||
-rw-r--r-- | kernel/vconv.ml | 1 |
5 files changed, 14 insertions, 8 deletions
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 8c5ab0ecb..885594ac7 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -14,6 +14,8 @@ /* Nota: this list of instructions is parsed to produce derived files */ /* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase */ /* and alone on lines starting by two spaces. */ +/* If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c */ +/* with the arity of the instruction and maybe coq_tcode_of_code. */ enum instructions { ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC, diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index df5fdce75..ddf40e2eb 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -539,6 +539,7 @@ value coq_interprete pc++;/* On saute le Restart */ } else { if (coq_extra_args < rec_pos) { + /* Partial application */ mlsize_t num_args, i; num_args = 1 + coq_extra_args; /* arg1 + extra args */ Alloc_small(accu, num_args + 2, Closure_tag); @@ -553,10 +554,10 @@ value coq_interprete } else { /* The recursif argument is an accumulator */ mlsize_t num_args, i; - /* Construction of partially applied PF */ + /* Construction of fixpoint applied to its [rec_pos-1] first arguments */ Alloc_small(accu, rec_pos + 2, Closure_tag); - Field(accu, 1) = coq_env; - for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; + Field(accu, 1) = coq_env; // We store the fixpoint in the first field + for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args Code_val(accu) = pc; sp += rec_pos; *--sp = accu; @@ -1024,7 +1025,7 @@ value coq_interprete annot = *pc++; sz = *pc++; *--sp=Field(coq_global_data, annot); - /* On sauve la pile */ + /* We save the stack */ if (sz == 0) accu = Atom(0); else { Alloc_small(accu, sz, Default_tag); @@ -1035,17 +1036,17 @@ value coq_interprete } } *--sp = accu; - /* On cree le zipper switch */ + /* We create the switch zipper */ Alloc_small(accu, 5, Default_tag); Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; Field(accu, 4) = coq_env; sp++;sp[0] = accu; - /* On cree l'atome */ + /* We create the atom */ Alloc_small(accu, 2, ATOM_SWITCH_TAG); Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; sp++;sp[0] = accu; - /* On cree l'accumulateur */ + /* We create the accumulator */ Alloc_small(accu, 2, Accu_tag); Code_val(accu) = accumulate; Field(accu,1) = *sp++; diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 008955d80..7d08f9e2d 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -506,6 +506,7 @@ let comp_args comp_expr reloc args sz cont = done; !c +(* Precondition: args not empty *) let comp_app comp_fun comp_arg reloc f args sz cont = let nargs = Array.length args in match is_tailcall cont with diff --git a/kernel/make-opcodes b/kernel/make-opcodes index c8f573c68..e1371b3d0 100644 --- a/kernel/make-opcodes +++ b/kernel/make-opcodes @@ -1,2 +1,3 @@ $1=="enum" {n=0; next; } - {for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} + {printf("(* THIS FILE IS GENERATED. DON'T EDIT. *)\n\n"); + for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 894f5296a..74d956bef 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -77,6 +77,7 @@ and conv_whd env pb k whd1 whd2 cu = | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> + (* on the fly eta expansion *) conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ |