diff options
| -rw-r--r-- | kernel/declarations.ml | 2 | ||||
| -rw-r--r-- | kernel/nativecode.ml | 111 | ||||
| -rw-r--r-- | kernel/nativecode.mli | 2 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 4 | ||||
| -rw-r--r-- | kernel/nativeinstr.mli | 2 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 7 | ||||
| -rw-r--r-- | kernel/nativevalues.ml | 2 | ||||
| -rw-r--r-- | kernel/nativevalues.mli | 4 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 16 |
9 files changed, 85 insertions, 65 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 913c13173..7bd70c050 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -52,7 +52,7 @@ type inline = int option type projection_body = { proj_ind : MutInd.t; proj_npars : int; - proj_arg : int; + proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) proj_eta : constr * types; (* Eta-expanded term and type *) proj_body : constr; (* For compatibility with VMs only, the match version *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 5174eeea8..8257dc8b8 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -53,7 +53,7 @@ type gname = | Gind of string * inductive (* prefix, inductive name *) | Gconstruct of string * constructor (* prefix, constructor name *) | Gconstant of string * Constant.t (* prefix, constant name *) - | Gproj of string * Constant.t (* prefix, constant name *) + | Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *) | Gcase of Label.t option * int | Gpred of Label.t option * int | Gfixtype of Label.t option * int @@ -108,7 +108,7 @@ let gname_hash gn = match gn with | Ginternal s -> combinesmall 9 (String.hash s) | Grel i -> combinesmall 10 (Int.hash i) | Gnamed id -> combinesmall 11 (Id.hash id) -| Gproj (s, p) -> combinesmall 12 (combine (String.hash s) (Constant.hash p)) +| Gproj (s, p, i) -> combinesmall 12 (combine (String.hash s) (combine (ind_hash p) i)) let case_ctr = ref (-1) @@ -152,6 +152,7 @@ type symbol = | SymbMeta of metavariable | SymbEvar of Evar.t | SymbLevel of Univ.Level.t + | SymbProj of (inductive * int) let dummy_symb = SymbValue (dummy_value ()) @@ -166,6 +167,7 @@ let eq_symbol sy1 sy2 = | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2 | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 + | SymbProj (i1, k1), SymbProj (i2, k2) -> eq_ind i1 i2 && Int.equal k1 k2 | _, _ -> false let hash_symbol symb = @@ -179,6 +181,7 @@ let hash_symbol symb = | SymbMeta m -> combinesmall 7 m | SymbEvar evk -> combinesmall 8 (Evar.hash evk) | SymbLevel l -> combinesmall 9 (Univ.Level.hash l) + | SymbProj (i, k) -> combinesmall 10 (combine (ind_hash i) k) module HashedTypeSymbol = struct type t = symbol @@ -241,6 +244,11 @@ let get_level tbl i = | SymbLevel u -> u | _ -> anomaly (Pp.str "get_level failed.") +let get_proj tbl i = + match tbl.(i) with + | SymbProj p -> p + | _ -> anomaly (Pp.str "get_proj failed.") + let push_symbol x = try HashtblSymbol.find symb_tbl x with Not_found -> @@ -885,6 +893,10 @@ let get_level_code i = MLapp (MLglobal (Ginternal "get_level"), [|MLglobal symbols_tbl_name; MLint i|]) +let get_proj_code i = + MLapp (MLglobal (Ginternal "get_proj"), + [|MLglobal symbols_tbl_name; MLint i|]) + type rlist = | Rnil | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' @@ -1070,7 +1082,7 @@ let ml_of_instance instance u = | Lconst (prefix, (c, u)) -> let args = ml_of_instance env.env_univ u in mkMLapp (MLglobal(Gconstant (prefix, c))) args - | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c)) + | Lproj (prefix, ind, i) -> MLglobal(Gproj (prefix, ind, i)) | Lprim _ -> let decl,cond,paux = extract_prim (ml_of_lam env l) t in compile_prim decl cond paux @@ -1544,8 +1556,8 @@ let string_of_gname g = Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1) | Gconstant (prefix, c) -> Format.sprintf "%sconst_%s" prefix (string_of_con c) - | Gproj (prefix, c) -> - Format.sprintf "%sproj_%s" prefix (string_of_con c) + | Gproj (prefix, (mind, n), i) -> + Format.sprintf "%sproj_%s_%i_%i" prefix (string_of_mind mind) n i | Gcase (l,i) -> Format.sprintf "case_%s_%i" (string_of_label_def l) i | Gpred (l,i) -> @@ -1858,8 +1870,6 @@ and compile_named env sigma univ auxdefs id = Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs let compile_constant env sigma prefix ~interactive con cb = - match cb.const_proj with - | false -> let no_univs = match cb.const_universes with | Monomorphic_const _ -> true @@ -1903,39 +1913,6 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix end - | true -> - let pb = lookup_projection (Projection.make con false) env in - let mind = pb.proj_ind in - let ind = (mind,0) in - let mib = lookup_mind mind env in - let oib = mib.mind_packets.(0) in - let tbl = oib.mind_reloc_tbl in - (* Building info *) - let prefix = get_mind_prefix env mind in - let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; - ci_cstr_nargs = [|0|]; - ci_cstr_ndecls = [||] (*FIXME*); - ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in - let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci; - asw_reloc = tbl; asw_finite = true } in - let c_uid = fresh_lname Anonymous in - let cf_uid = fresh_lname Anonymous in - let _, arity = tbl.(0) in - let ci_uid = fresh_lname Anonymous in - let cargs = Array.init arity - (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) - in - let i = push_symbol (SymbConst con) in - let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in - let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in - let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in - let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in - let gn = Gproj ("",con) in - let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in - let arg = fargs.(pb.proj_npars) in - Glet(Gconstant ("", con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal - arg|]))):: - [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) @@ -1962,10 +1939,12 @@ let arg_name = Name (Id.of_string "arg") let compile_mind prefix ~interactive mb mind stack = let u = Declareops.inductive_polymorphic_context mb in + (** Generate data for every block *) let f i stack ob = - let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in - let j = push_symbol (SymbInd (mind,i)) in - let name = Gind ("", (mind, i)) in + let ind = (mind, i) in + let gtype = Gtype(ind, Array.map snd ob.mind_reloc_tbl) in + let j = push_symbol (SymbInd ind) in + let name = Gind ("", ind) in let accu = let args = if Int.equal (Univ.AUContext.size u) 0 then @@ -1979,12 +1958,41 @@ let compile_mind prefix ~interactive mb mind stack = Array.init nparams (fun i -> {lname = param_name; luid = i}) in let add_construct j acc (_,arity) = let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in - let c = (mind,i), (j+1) in + let c = ind, (j+1) in Glet(Gconstruct ("", c), mkMLlam (Array.append params args) (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in - Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl + let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in + let add_proj j acc pb = + let tbl = ob.mind_reloc_tbl in + (* Building info *) + let ci = { ci_ind = ind; ci_npar = nparams; + ci_cstr_nargs = [|0|]; + ci_cstr_ndecls = [||] (*FIXME*); + ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in + let asw = { asw_ind = ind; asw_prefix = ""; asw_ci = ci; + asw_reloc = tbl; asw_finite = true } in + let c_uid = fresh_lname Anonymous in + let cf_uid = fresh_lname Anonymous in + let _, arity = tbl.(0) in + let ci_uid = fresh_lname Anonymous in + let cargs = Array.init arity + (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) + in + let i = push_symbol (SymbProj (ind, j)) in + let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in + let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in + let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in + let gn = Gproj ("", (pb.proj_ind, j), pb.proj_arg) in + Glet (gn, mkMLlam [|c_uid|] code) :: acc + in + let projs = match mb.mind_record with + | None | Some None -> [] + | Some (Some (id, kns, pbs)) -> Array.fold_left_i add_proj [] pbs + in + projs @ constructors @ gtype :: accu :: stack in Array.fold_left_i f stack mb.mind_packets @@ -2030,13 +2038,9 @@ let compile_deps env sigma prefix ~interactive init t = then init else let comp_stack, (mind_updates, const_updates) = - match cb.const_proj, cb.const_body with - | false, Def t -> + match cb.const_body with + | Def t -> aux env lvl init (Mod_subst.force_constr t) - | true, _ -> - let pb = lookup_projection (Projection.make c false) env in - let mind = pb.proj_ind in - compile_mind_deps env prefix ~interactive init mind | _ -> init in let code, name = @@ -2047,8 +2051,9 @@ let compile_deps env sigma prefix ~interactive init t = comp_stack, (mind_updates, const_updates) | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> - let term = mkApp (mkConst (Projection.constant p), [|c|]) in - aux env lvl init term + let pb = lookup_projection p env in + let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in + aux env lvl init c | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 42f2cbc2e..684983a87 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -50,6 +50,8 @@ val get_evar : symbols -> int -> Evar.t val get_level : symbols -> int -> Univ.Level.t +val get_proj : symbols -> int -> inductive * int + val get_symbols : unit -> symbols type code_location_update diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c07025660..e97dbd0d6 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -114,8 +114,8 @@ and conv_atom env pb lvl a1 a2 cu = let cu = conv_val env CONV lvl d1 d2 cu in let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu - | Aproj(p1,ac1), Aproj(p2,ac2) -> - if not (Constant.equal p1 p2) then raise NotConvertible + | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) -> + if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index c319be32d..eaad8ee0c 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -31,7 +31,7 @@ and lambda = | Llet of Name.t * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant - | Lproj of prefix * Constant.t (* prefix, projection name *) + | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) | Lprim of prefix * Constant.t * CPrimitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 6db75c89a..0325a00b4 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -519,8 +519,11 @@ let rec lambda_of_constr env sigma c = | Construct _ -> lambda_of_app env sigma c empty_args | Proj (p, c) -> - let kn = Projection.constant p in - mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|] + let pb = lookup_projection p !global_env in + (** FIXME: handle mutual records *) + let ind = (pb.proj_ind, 0) in + let prefix = get_mind_prefix !global_env (fst ind) in + mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index cfcb0a485..da4413a0a 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -64,7 +64,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t * t array - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator let accumulate_tag = 0 diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 4a58a3c7d..649853f06 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -54,7 +54,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t (* type *) * t array (* arguments *) - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator (* Constructors *) @@ -71,7 +71,7 @@ val mk_fix_accu : rec_pos -> int -> t array -> t array -> t val mk_cofix_accu : int -> t array -> t array -> t val mk_meta_accu : metavariable -> t val mk_evar_accu : Evar.t -> t -> t array -> t -val mk_proj_accu : Constant.t -> accumulator -> t +val mk_proj_accu : (inductive * int) -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t val mk_const : tag -> t diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 3fce2f3c6..4b8e0e096 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -188,6 +188,14 @@ let branch_of_switch lvl ans bs = bs ci in Array.init (Array.length tbl) branch +let get_proj env ((mind, _n), i) = + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | None | Some None -> + CErrors.anomaly (Pp.strbrk "Return type is not a primitive record") + | Some (Some (_, projs, _)) -> + Projection.make projs.(i) true + let rec nf_val env sigma v typ = match kind_of_value v with | Vaccu accu -> nf_accu env sigma accu @@ -279,9 +287,10 @@ and nf_atom env sigma atom = let codom = nf_type env sigma (codom vn) in mkProd(n,dom,codom) | Ameta (mv,_) -> mkMeta mv - | Aproj(p,c) -> + | Aproj (p, c) -> let c = nf_accu env sigma c in - mkProj(Projection.make p true,c) + let p = get_proj env p in + mkProj(p, c) | _ -> fst (nf_atom_type env sigma atom) and nf_atom_type env sigma atom = @@ -357,7 +366,8 @@ and nf_atom_type env sigma atom = | Aproj(p,c) -> let c,tc = nf_accu_type env sigma c in let cj = make_judge c tc in - let uj = Typeops.judge_of_projection env (Projection.make p true) cj in + let p = get_proj env p in + let uj = Typeops.judge_of_projection env p cj in uj.uj_val, uj.uj_type |