diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-07-06 17:04:10 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-07-06 17:04:10 +0200 |
commit | 139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (patch) | |
tree | a650355330521a776719279328e82a47527d15a5 /kernel | |
parent | 7ad2fe2bd30a07eb2495ea8cf902a24ef13a3627 (diff) | |
parent | 2face8d77628ded64f7d0a824f4b377694b9d7fd (diff) |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/byterun/coq_fix_code.c | 2 | ||||
-rw-r--r-- | kernel/byterun/coq_instruct.h | 1 | ||||
-rw-r--r-- | kernel/byterun/coq_interp.c | 28 | ||||
-rw-r--r-- | kernel/byterun/coq_values.h | 9 | ||||
-rw-r--r-- | kernel/cbytecodes.ml | 6 | ||||
-rw-r--r-- | kernel/cbytecodes.mli | 3 | ||||
-rw-r--r-- | kernel/cbytegen.ml | 14 | ||||
-rw-r--r-- | kernel/cemitcodes.ml | 1 | ||||
-rw-r--r-- | kernel/csymtable.ml | 7 | ||||
-rw-r--r-- | kernel/declarations.mli | 6 | ||||
-rw-r--r-- | kernel/nativeconv.ml | 22 | ||||
-rw-r--r-- | kernel/term_typing.ml | 20 | ||||
-rw-r--r-- | kernel/vconv.ml | 17 | ||||
-rw-r--r-- | kernel/vm.ml | 22 | ||||
-rw-r--r-- | kernel/vm.mli | 1 |
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 |