diff options
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 185 |
1 files changed, 106 insertions, 79 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 123e7a6d..eed25a4c 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -16,7 +16,7 @@ open Util open Nativevalues open Nativeinstr open Nativelambda -open Pre_env +open Environ [@@@ocaml.warning "-32-37"] @@ -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 @@ -71,8 +71,8 @@ let eq_gname gn1 gn2 = String.equal s1 s2 && eq_constructor c1 c2 | Gconstant (s1, c1), Gconstant (s2, c2) -> String.equal s1 s2 && Constant.equal c1 c2 - | Gproj (s1, c1), Gproj (s2, c2) -> - String.equal s1 s2 && Constant.equal c1 c2 + | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) -> + String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -112,7 +112,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) @@ -156,6 +156,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 ()) @@ -170,6 +171,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 = @@ -183,6 +185,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 @@ -245,6 +248,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 -> @@ -270,7 +278,6 @@ type primitive = | Mk_rel of int | Mk_var of Id.t | Mk_proj - | Is_accu | Is_int | Cast_accu | Upd_cofix @@ -311,7 +318,6 @@ let eq_primitive p1 p2 = | Mk_cofix i1, Mk_cofix i2 -> Int.equal i1 i2 | Mk_rel i1, Mk_rel i2 -> Int.equal i1 i2 | Mk_var id1, Mk_var id2 -> Id.equal id1 id2 - | Is_accu, Is_accu -> true | Cast_accu, Cast_accu -> true | Upd_cofix, Upd_cofix -> true | Force_cofix, Force_cofix -> true @@ -337,7 +343,6 @@ let primitive_hash = function combinesmall 8 (Int.hash i) | Mk_var id -> combinesmall 9 (Id.hash id) - | Is_accu -> 10 | Is_int -> 11 | Cast_accu -> 12 | Upd_cofix -> 13 @@ -388,6 +393,7 @@ type mllambda = | MLsetref of string * mllambda | MLsequence of mllambda * mllambda | MLarray of mllambda array + | MLisaccu of string * inductive * mllambda and mllam_branches = ((constructor * lname option array) list * mllambda) array @@ -459,7 +465,12 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = | MLarray arr1, MLarray arr2 -> Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2 - | _, _ -> false + | MLisaccu (s1, ind1, ml1), MLisaccu (s2, ind2, ml2) -> + String.equal s1 s2 && eq_ind ind1 ind2 && + eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 + | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ | + MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ | + MLsetref _ | MLsequence _ | MLarray _ | MLisaccu _), _ -> false and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 = let eq_def (_,args1,ml1) (_,args2,ml2) = @@ -534,6 +545,8 @@ let rec hash_mllambda gn n env t = combinesmall 14 (combine hml hml') | MLarray arr -> combinesmall 15 (hash_mllambda_array gn n env 1 arr) + | MLisaccu (s, ind, c) -> + combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c))) and hash_mllambda_letrec gn n env init defs = let hash_def (_,args,ml) = @@ -600,6 +613,7 @@ let fv_lam l = | MLsetref(_,l) -> aux l bind fv | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv) | MLarray arr -> Array.fold_right (fun a fv -> aux a bind fv) arr fv + | MLisaccu (_, _, body) -> aux body bind fv in aux l LNset.empty LNset.empty @@ -618,6 +632,14 @@ let mkMLapp f args = | MLapp(f,args') -> MLapp(f,Array.append args' args) | _ -> MLapp(f,args) +let mkForceCofix prefix ind arg = + let name = fresh_lname Anonymous in + MLlet (name, arg, + MLif ( + MLisaccu (prefix, ind, MLlocal name), + MLapp (MLprimitive Force_cofix, [|MLlocal name|]), + MLlocal name)) + let empty_params = [||] let decompose_MLlam c = @@ -889,6 +911,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' @@ -1049,12 +1075,11 @@ let ml_of_instance instance u = let tyn = fresh_lname Anonymous in let i = push_symbol (SymbMeta mv) in MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|]) - | Levar(evk,ty,args) -> - let tyn = fresh_lname Anonymous in + | Levar(evk, args) -> let i = push_symbol (SymbEvar evk) in + (** Arguments are *not* reversed in evar instances in native compilation *) let args = MLarray(Array.map (ml_of_lam env l) args) in - MLlet(tyn, ml_of_lam env l ty, - MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn; args|])) + MLapp(MLprimitive Mk_evar, [|get_evar_code i; args|]) | Lprod(dom,codom) -> let dom = ml_of_lam env l dom in let codom = ml_of_lam env l codom in @@ -1074,7 +1099,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 @@ -1126,11 +1151,11 @@ let ml_of_instance instance u = let arg = ml_of_lam env l a in let force = if annot.asw_finite then arg - else MLapp(MLprimitive Force_cofix, [|arg|]) in + else mkForceCofix annot.asw_prefix annot.asw_ind arg in mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|] | Lif(t,bt,bf) -> MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf) - | Lfix ((rec_pos,start), (ids, tt, tb)) -> + | Lfix ((rec_pos, inds, start), (ids, tt, tb)) -> (* let type_f fvt = [| type fix |] let norm_f1 fv f1 .. fn params1 = body1 .. @@ -1199,8 +1224,9 @@ let ml_of_instance instance u = let paramsi = t_params.(i) in let reci = MLlocal (paramsi.(rec_pos.(i))) in let pargsi = Array.map (fun id -> MLlocal id) paramsi in + let (prefix, ind) = inds.(i) in let body = - MLif(MLapp(MLprimitive Is_accu,[|reci|]), + MLif(MLisaccu (prefix, ind, reci), mkMLapp (MLapp(MLprimitive (Mk_fix(rec_pos,i)), [|mk_type; mk_norm|])) @@ -1362,6 +1388,7 @@ let subst s l = | MLsetref(s,l1) -> MLsetref(s,aux l1) | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2) | MLarray arr -> MLarray (Array.map aux arr) + | MLisaccu (s, ind, l) -> MLisaccu (s, ind, aux l) in aux l @@ -1459,7 +1486,7 @@ let optimize gdef l = let b1 = optimize s b1 in let b2 = optimize s b2 in begin match t, b2 with - | MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs) + | MLisaccu (_, _, l1), MLmatch(annot, l2, _, bs) when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs) | _, _ -> MLif(t, b1, b2) end @@ -1471,6 +1498,7 @@ let optimize gdef l = | MLsetref(r,l) -> MLsetref(r, optimize s l) | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2) | MLarray arr -> MLarray (Array.map (optimize s) arr) + | MLisaccu (pf, ind, l) -> MLisaccu (pf, ind, optimize s l) in optimize LNmap.empty l @@ -1548,8 +1576,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) -> @@ -1633,19 +1661,23 @@ let pp_mllam fmt l = pp_mllam fmt arr.(len-1) end; Format.fprintf fmt "|]@]" - + | MLisaccu (prefix, (mind, i), c) -> + let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in + Format.fprintf fmt + "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n true@\n| _ ->@\n false@\nend@]" + pp_mllam c accu and pp_letrec fmt defs = let len = Array.length defs in - let pp_one_rec i (fn, argsn, body) = + let pp_one_rec (fn, argsn, body) = Format.fprintf fmt "%a%a =@\n %a" pp_lname fn pp_ldecls argsn pp_mllam body in Format.fprintf fmt "@[let rec "; - pp_one_rec 0 defs.(0); + pp_one_rec defs.(0); for i = 1 to len - 1 do Format.fprintf fmt "@\nand "; - pp_one_rec i defs.(i) + pp_one_rec defs.(i) done; and pp_blam fmt l = @@ -1726,7 +1758,6 @@ let pp_mllam fmt l = | Mk_var id -> Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id) | Mk_proj -> Format.fprintf fmt "mk_proj_accu" - | Is_accu -> Format.fprintf fmt "is_accu" | Is_int -> Format.fprintf fmt "is_int" | Cast_accu -> Format.fprintf fmt "cast_accu" | Upd_cofix -> Format.fprintf fmt "upd_cofix" @@ -1833,7 +1864,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = in let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in let auxdefs = List.fold_right get_named_val fv_named auxdefs in - let lvl = Context.Rel.length env.env_rel_context.env_rel_ctx in + let lvl = Context.Rel.length (rel_context env) in let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in let aux_name = fresh_lname Anonymous in @@ -1841,8 +1872,8 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = and compile_rel env sigma univ auxdefs n = let open Context.Rel.Declaration in - let decl = Pre_env.lookup_rel n env in - let n = List.length env.env_rel_context.env_rel_ctx - n in + let decl = lookup_rel n env in + let n = List.length (rel_context env) - n in match decl with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in @@ -1862,8 +1893,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 - | None -> let no_univs = match cb.const_universes with | Monomorphic_const _ -> true @@ -1874,7 +1903,7 @@ let compile_constant env sigma prefix ~interactive con cb = let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); - let is_lazy = is_lazy prefix t in + let is_lazy = is_lazy env prefix t in let code = if is_lazy then mk_lazy code else code in let name = if interactive then LinkedInteractive prefix @@ -1907,38 +1936,6 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix end - | Some pb -> - 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) @@ -1963,12 +1960,14 @@ let is_code_loaded ~interactive name = let param_name = Name (Id.of_string "params") let arg_name = Name (Id.of_string "arg") -let compile_mind prefix ~interactive mb mind stack = +let compile_mind 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 @@ -1982,12 +1981,43 @@ 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 proj_arg 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 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, mkForceCofix "" ind (MLlocal c_uid), code) in + let gn = Gproj ("", ind, proj_arg) in + Glet (gn, mkMLlam [|c_uid|] code) :: acc + in + let projs = match mb.mind_record with + | NotRecord | FakeRecord -> [] + | PrimRecord info -> + let _, _, pbs = info.(i) in + Array.fold_left_i add_proj [] pbs + in + projs @ constructors @ gtype :: accu :: stack in Array.fold_left_i f stack mb.mind_packets @@ -2008,7 +2038,7 @@ let compile_mind_deps env prefix ~interactive then init else let comp_stack = - compile_mind prefix ~interactive mib mind comp_stack + compile_mind mib mind comp_stack in let name = if interactive then LinkedInteractive prefix @@ -2033,12 +2063,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 - | None, Def t -> + match cb.const_body with + | Def t -> aux env lvl init (Mod_subst.force_constr t) - | Some pb, _ -> - let mind = pb.proj_ind in - compile_mind_deps env prefix ~interactive init mind | _ -> init in let code, name = @@ -2049,8 +2076,8 @@ 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 init = compile_mind_deps env prefix ~interactive init (Projection.mind p) 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 @@ -2082,9 +2109,9 @@ let compile_constant_field env prefix con acc cb = in gl@acc -let compile_mind_field prefix mp l acc mb = +let compile_mind_field mp l acc mb = let mind = MutInd.make2 mp l in - compile_mind prefix ~interactive:false mb mind acc + compile_mind mb mind acc let mk_open s = Gopen s |