From 6482ca75a39709e65de676d533b3d115ad2b1153 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 3 Jul 2015 01:14:17 +0200 Subject: Fix convertibility of primitive projections for native_compute. Stuck primitive projections were never convertible. --- kernel/nativeconv.ml | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'kernel') diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 1f8bfc984f..d0aa96fd15 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 = -- cgit v1.2.3 From a51cce369b9c634a93120092d4c7685a242d55b1 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 4 Jul 2015 14:22:08 +0200 Subject: Fix handling of primitive projections in VM. I'm pushing this patch now because the previous treatment of such projections in the VM was already unsound. It should however be carefully reviewed. --- kernel/byterun/coq_fix_code.c | 2 +- kernel/byterun/coq_instruct.h | 1 + kernel/byterun/coq_interp.c | 28 ++++++++++++++++++++++++++-- kernel/byterun/coq_values.h | 9 +++++---- kernel/cbytecodes.ml | 6 ++++++ kernel/cbytecodes.mli | 3 +++ kernel/cbytegen.ml | 14 ++++++-------- kernel/cemitcodes.ml | 1 + kernel/csymtable.ml | 7 +++++-- kernel/term_typing.ml | 20 ++++++++++++++++++-- kernel/vconv.ml | 17 ++++++++++++----- kernel/vm.ml | 22 ++++++++++++++-------- kernel/vm.mli | 1 + 13 files changed, 99 insertions(+), 32 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 1be3e65113..29e33d349b 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 9cbf4077e2..8c5ab0ecbd 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 ddbde9d385..0a121dc32e 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 1bf493e2c0..1590a2141d 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 93fd61f02a..3271ac1458 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 d9998c89e8..745ef311b0 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 ac46dc5833..d5435f0c37 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 2535a64d3c..0d9334a50c 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 49ab68beae..8fd90ec364 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/term_typing.ml b/kernel/term_typing.ml index a316b4492b..83e566041f 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 1c31cc0414..a03a67db8b 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 d4bf461b39..a822f92eb3 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 5190356828..d31448ee13 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 -- cgit v1.2.3 From 7df4e7d5fb011ff4dbb26884bb80ece20950b178 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 5 Jul 2015 19:08:17 +0200 Subject: Fixing documentation (see Maxime's mail on coqdev, July 3). --- kernel/declarations.mli | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 27c1c3f3f0..c1c19a757c 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 *) -- cgit v1.2.3