aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-07-06 17:04:10 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-07-06 17:04:10 +0200
commit139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (patch)
treea650355330521a776719279328e82a47527d15a5 /kernel
parent7ad2fe2bd30a07eb2495ea8cf902a24ef13a3627 (diff)
parent2face8d77628ded64f7d0a824f4b377694b9d7fd (diff)
Merge branch 'v8.5' into trunk
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_fix_code.c2
-rw-r--r--kernel/byterun/coq_instruct.h1
-rw-r--r--kernel/byterun/coq_interp.c28
-rw-r--r--kernel/byterun/coq_values.h9
-rw-r--r--kernel/cbytecodes.ml6
-rw-r--r--kernel/cbytecodes.mli3
-rw-r--r--kernel/cbytegen.ml14
-rw-r--r--kernel/cemitcodes.ml1
-rw-r--r--kernel/csymtable.ml7
-rw-r--r--kernel/declarations.mli6
-rw-r--r--kernel/nativeconv.ml22
-rw-r--r--kernel/term_typing.ml20
-rw-r--r--kernel/vconv.ml17
-rw-r--r--kernel/vm.ml22
-rw-r--r--kernel/vm.mli1
15 files changed, 115 insertions, 44 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1be3e6511..29e33d349 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -60,7 +60,7 @@ void init_arity () {
arity[BRANCH]=arity[ISCONST]= 1;
/* instruction with two operands */
arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
- arity[ARECONST]=2;
+ arity[ARECONST]=arity[PROJ]=2;
/* instruction with four operands */
arity[MAKESWITCHBLOCK]=4;
/* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 9cbf4077e..8c5ab0ecb 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -36,6 +36,7 @@ enum instructions {
SWITCH, PUSHFIELDS,
GETFIELD0, GETFIELD1, GETFIELD,
SETFIELD0, SETFIELD1, SETFIELD,
+ PROJ,
CONST0, CONST1, CONST2, CONST3, CONSTINT,
PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
ACCUMULATE,
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ddbde9d38..0a121dc32 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -878,8 +878,32 @@ value coq_interprete
caml_modify(&Field(accu, *pc),*sp);
sp++; pc++;
Next;
- }
-
+ }
+
+
+ Instruct(PROJ){
+ print_instr("PROJ");
+ if (Is_accu (accu)) {
+ /* Skip over the index of projected field */
+ pc++;
+ /* Save the argument on the stack */
+ *--sp = accu;
+ /* Create atom */
+ Alloc_small(accu, 2, ATOM_PROJ_TAG);
+ Field(accu, 0) = Field(coq_global_data, *pc);
+ Field(accu, 1) = sp[0];
+ sp[0] = accu;
+ /* Create accumulator */
+ Alloc_small(accu, 2, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu,1) = *sp++;
+ } else {
+ accu = Field(accu, *pc++);
+ }
+ pc++;
+ Next;
+ }
+
/* Integer constants */
Instruct(CONST0){
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1bf493e2c..1590a2141 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -22,10 +22,11 @@
#define ATOM_ID_TAG 0
#define ATOM_IDDEF_TAG 1
#define ATOM_INDUCTIVE_TAG 2
-#define ATOM_FIX_TAG 3
-#define ATOM_SWITCH_TAG 4
-#define ATOM_COFIX_TAG 5
-#define ATOM_COFIXEVALUATED_TAG 6
+#define ATOM_PROJ_TAG 3
+#define ATOM_FIX_TAG 4
+#define ATOM_SWITCH_TAG 5
+#define ATOM_COFIX_TAG 6
+#define ATOM_COFIXEVALUATED_TAG 7
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 93fd61f02..3271ac145 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -31,6 +31,7 @@ let last_variant_tag = 245
type structured_constant =
| Const_sorts of sorts
| Const_ind of pinductive
+ | Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
@@ -81,6 +82,8 @@ type instruction =
| Ksetfield of int
| Kstop
| Ksequence of bytecodes * bytecodes
+ | Kproj of int * Constant.t (* index of the projected argument,
+ name of projection *)
(* spiwack: instructions concerning integers *)
| Kbranch of Label.t (* jump to label *)
| Kaddint31 (* adds the int31 in the accu
@@ -167,6 +170,7 @@ let pp_sort s =
let rec pp_struct_const = function
| Const_sorts s -> pp_sort s
| Const_ind ((mind, i), u) -> pr_mind mind ++ str"#" ++ int i
+ | Const_proj p -> Constant.print p
| Const_b0 i -> int i
| Const_bn (i,t) ->
int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
@@ -228,6 +232,8 @@ let rec pp_instr i =
| Kbranch lbl -> str "branch " ++ pp_lbl lbl
+ | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p
+
| Kaddint31 -> str "addint31"
| Kaddcint31 -> str "addcint31"
| Kaddcarrycint31 -> str "addcarrycint31"
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index d9998c89e..745ef311b 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -25,6 +25,7 @@ val last_variant_tag : tag
type structured_constant =
| Const_sorts of sorts
| Const_ind of pinductive
+ | Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
@@ -72,6 +73,8 @@ type instruction =
| Ksetfield of int
| Kstop
| Ksequence of bytecodes * bytecodes
+ | Kproj of int * Constant.t (** index of the projected argument,
+ name of projection *)
(** spiwack: instructions concerning integers *)
| Kbranch of Label.t (** jump to label, is it needed ? *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index ac46dc583..d5435f0c3 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -540,14 +540,12 @@ let rec compile_constr reloc c sz cont =
match kind_of_term c with
| Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
| Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
- | Proj (p,c) ->
- (* compile_const reloc p [|c|] sz cont *)
- let kn = Projection.constant p in
- let cb = lookup_constant kn !global_env in
- (* TODO: better representation of projections *)
- let pb = Option.get cb.const_proj in
- let args = Array.make pb.proj_npars mkProp in
- compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont
+ | Proj (p,c) ->
+ let kn = Projection.constant p in
+ let cb = lookup_constant kn !global_env in
+ let pb = Option.get cb.const_proj in
+ let n = pb.proj_arg in
+ compile_constr reloc c sz (Kproj (n,kn) :: cont)
| Cast(c,_,_) -> compile_constr reloc c sz cont
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 2535a64d3..0d9334a50 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -225,6 +225,7 @@ let emit_instr = function
if n <= 1 then out (opSETFIELD0+n)
else (out opSETFIELD;out_int n)
| Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
+ | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
(* spiwack *)
| Kbranch lbl -> out opBRANCH; out_label lbl
| Kaddint31 -> out opADDINT31
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 49ab68bea..8fd90ec36 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -60,6 +60,8 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
| Const_sorts _, _ -> false
| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
| Const_ind _, _ -> false
+| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
+| Const_proj _, _ -> false
| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
| Const_b0 _, _ -> false
| Const_bn (t1, a1), Const_bn (t2, a2) ->
@@ -71,11 +73,12 @@ let rec hash_structured_constant c =
match c with
| Const_sorts s -> combinesmall 1 (Sorts.hash s)
| Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u))
- | Const_b0 t -> combinesmall 3 (Int.hash t)
+ | Const_proj p -> combinesmall 3 (Constant.hash p)
+ | Const_b0 t -> combinesmall 4 (Int.hash t)
| Const_bn (t, a) ->
let fold h c = combine h (hash_structured_constant c) in
let h = Array.fold_left fold 0 a in
- combinesmall 4 (combine (Int.hash t) h)
+ combinesmall 5 (combine (Int.hash t) h)
module SConstTable = Hashtbl.Make (struct
type t = structured_constant
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 27c1c3f3f..c1c19a757 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -142,12 +142,10 @@ type one_inductive_body = {
mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
mind_consnrealargs : int array;
- (** Number of expected proper arguments of the constructors (w/o params)
- (not used in the kernel) *)
+ (** Number of expected proper arguments of the constructors (w/o params) *)
mind_consnrealdecls : int array;
- (** Length of the signature of the constructors (with let, w/o params)
- (not used in the kernel) *)
+ (** Length of the signature of the constructors (with let, w/o params) *)
mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 1f8bfc984..d0aa96fd1 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -20,11 +20,15 @@ let rec conv_val env pb lvl cu v1 v2 =
if v1 == v2 then ()
else
match kind_of_value v1, kind_of_value v2 with
- | Vaccu k1, Vaccu k2 ->
- conv_accu env pb lvl cu k1 k2
| Vfun f1, Vfun f2 ->
let v = mk_rel_accu lvl in
conv_val env CONV (lvl+1) cu (f1 v) (f2 v)
+ | Vfun f1, _ ->
+ conv_val env CONV lvl cu v1 (fun x -> v2 x)
+ | _, Vfun f2 ->
+ conv_val env CONV lvl cu (fun x -> v1 x) v2
+ | Vaccu k1, Vaccu k2 ->
+ conv_accu env pb lvl cu k1 k2
| Vconst i1, Vconst i2 ->
if not (Int.equal i1 i2) then raise NotConvertible
| Vblock b1, Vblock b2 ->
@@ -40,11 +44,7 @@ let rec conv_val env pb lvl cu v1 v2 =
aux lvl max b1 b2 (i+1) cu)
in
aux lvl (n1-1) b1 b2 0 cu
- | Vfun f1, _ ->
- conv_val env CONV lvl cu v1 (fun x -> v2 x)
- | _, Vfun f2 ->
- conv_val env CONV lvl cu (fun x -> v1 x) v2
- | _, _ -> raise NotConvertible
+ | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible
and conv_accu env pb lvl cu k1 k2 =
let n1 = accu_nargs k1 in
@@ -60,6 +60,7 @@ and conv_atom env pb lvl a1 a2 cu =
if a1 == a2 then ()
else
match a1, a2 with
+ | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
| Arel i1, Arel i2 ->
if not (Int.equal i1 i2) then raise NotConvertible
| Aind ind1, Aind ind2 ->
@@ -104,7 +105,12 @@ and conv_atom env pb lvl a1 a2 cu =
conv_val env CONV lvl cu d1 d2;
let v = mk_rel_accu lvl in
conv_val env pb (lvl + 1) cu (d1 v) (d2 v)
- | _, _ -> raise NotConvertible
+ | Aproj(p1,ac1), Aproj(p2,ac2) ->
+ if not (Constant.equal p1 p2) then raise NotConvertible
+ else conv_accu env CONV lvl cu ac1 ac2
+ | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
+ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
+ | Aproj _, _ -> raise NotConvertible
(* Precondition length t1 = length f1 = length f2 = length t2 *)
and conv_fix env lvl t1 f1 t2 f2 cu =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b4492..83e566041 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -251,7 +251,24 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
match proj with
| None -> compile_constant_body env def
| Some pb ->
- compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))
+ (* The compilation of primitive projections is a bit tricky, because
+ they refer to themselves (the body of p looks like fun c =>
+ Proj(p,c)). We break the cycle by building an ad-hoc compilation
+ environment. A cleaner solution would be that kernel projections are
+ simply Proj(i,c) with i an int and c a constr, but we would have to
+ get rid of the compatibility layer. *)
+ let cb =
+ { const_hyps = hyps;
+ const_body = def;
+ const_type = typ;
+ const_proj = proj;
+ const_body_code = None;
+ const_polymorphic = poly;
+ const_universes = univs;
+ const_inline_code = inline_code }
+ in
+ let env = add_constant kn cb env in
+ compile_constant_body env def
in Option.map Cemitcodes.from_val res
in
{ const_hyps = hyps;
@@ -263,7 +280,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
const_universes = univs;
const_inline_code = inline_code }
-
(*s Global and local constant declaration. *)
let translate_constant env kn ce =
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 1c31cc041..a03a67db8 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -18,8 +18,8 @@ let compare_zipper z1 z2 =
match z1, z2 with
| Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2)
| Zfix(f1,args1), Zfix(f2,args2) -> Int.equal (nargs args1) (nargs args2)
- | Zswitch _, Zswitch _ -> true
- | _ , _ -> false
+ | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true
+ | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false
let rec compare_stack stk1 stk2 =
match stk1, stk2 with
@@ -81,7 +81,10 @@ and conv_whd env pb k whd1 whd2 cu =
conv_whd env pb k whd1 (force_whd v stk) cu
| Vatom_stk(Aiddef(_,v),stk), _ ->
conv_whd env pb k (force_whd v stk) whd2 cu
- | _, _ -> raise NotConvertible
+
+ | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _
+ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
+
and conv_atom env pb k a1 stk1 a2 stk2 cu =
match a1, a2 with
@@ -110,7 +113,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
| _, Aiddef(ik2,v2) ->
conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
- | _, _ -> raise NotConvertible
+ | Aind _, _ | Aid _, _ -> raise NotConvertible
and conv_stack env k stk1 stk2 cu =
match stk1, stk2 with
@@ -131,7 +134,11 @@ and conv_stack env k stk1 stk2 cu =
done;
conv_stack env k stk1 stk2 !rcu
else raise NotConvertible
- | _, _ -> raise NotConvertible
+ | Zproj p1 :: stk1, Zproj p2 :: stk2 ->
+ if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu
+ else raise NotConvertible
+ | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
+ | Zproj _ :: _, _ -> raise NotConvertible
and conv_fun env pb k f1 f2 cu =
if f1 == f2 then cu
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d4bf461b3..a822f92eb 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -127,10 +127,11 @@ type vswitch = {
(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *)
(* - representation of [accu] : tag_[....] *)
(* -- tag <= 2 : encoding atom type (sorts, free vars, etc.) *)
-(* -- 3_[accu|fix_app] : a fixpoint blocked by an accu *)
-(* -- 4_[accu|vswitch] : a match blocked by an accu *)
-(* -- 5_[fcofix] : a cofix function *)
-(* -- 6_[fcofix|val] : a cofix function, val represent the value *)
+(* -- 3_[accu|proj name] : a projection blocked by an accu *)
+(* -- 4_[accu|fix_app] : a fixpoint blocked by an accu *)
+(* -- 5_[accu|vswitch] : a match blocked by an accu *)
+(* -- 6_[fcofix] : a cofix function *)
+(* -- 7_[fcofix|val] : a cofix function, val represent the value *)
(* of the function applied to arg1 ... argn *)
(* The [arguments] type, which is abstracted as an array, represents : *)
(* tag[ _ | _ |v1|... | vn] *)
@@ -149,6 +150,7 @@ type zipper =
| Zapp of arguments
| Zfix of vfix*arguments (* Possibly empty *)
| Zswitch of vswitch
+ | Zproj of Constant.t (* name of the projection *)
type stack = zipper list
@@ -176,15 +178,18 @@ let rec whd_accu a stk =
match Obj.tag at with
| i when i <= 2 ->
Vatom_stk(Obj.magic at, stk)
- | 3 (* fix_app tag *) ->
+ | 3 (* proj tag *) ->
+ let zproj = Zproj (Obj.obj (Obj.field at 0)) in
+ whd_accu (Obj.field at 1) (zproj :: stk)
+ | 4 (* fix_app tag *) ->
let fa = Obj.field at 1 in
let zfix =
Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
whd_accu (Obj.field at 0) (zfix :: stk)
- | 4 (* switch tag *) ->
+ | 5 (* switch tag *) ->
let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
whd_accu (Obj.field at 0) (zswitch :: stk)
- | 5 (* cofix_tag *) ->
+ | 6 (* cofix_tag *) ->
let vcfx = Obj.obj (Obj.field at 0) in
let to_up = Obj.obj a in
begin match stk with
@@ -192,7 +197,7 @@ let rec whd_accu a stk =
| [Zapp args] -> Vcofix(vcfx, to_up, Some args)
| _ -> assert false
end
- | 6 (* cofix_evaluated_tag *) ->
+ | 7 (* cofix_evaluated_tag *) ->
let vcofix = Obj.obj (Obj.field at 0) in
let res = Obj.obj a in
begin match stk with
@@ -289,6 +294,7 @@ let rec obj_of_str_const str =
match str with
| Const_sorts s -> Obj.repr (Vsort s)
| Const_ind ind -> obj_of_atom (Aind ind)
+ | Const_proj p -> Obj.repr p
| Const_b0 tag -> Obj.repr tag
| Const_bn(tag, args) ->
let len = Array.length args in
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 519035682..d31448ee1 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -34,6 +34,7 @@ type zipper =
| Zapp of arguments
| Zfix of vfix * arguments (** might be empty *)
| Zswitch of vswitch
+ | Zproj of Constant.t (* name of the projection *)
type stack = zipper list