From 01f230dcce3931e1a74b603b0530448af53cac3c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 13 Jul 2018 00:21:31 +0200 Subject: Pass a proper environment to Nativelambda.lambda_of_constr. No need to roll up a new data structure when Environment has O(log n) add and lookup of rel definitions. --- kernel/nativecode.ml | 2 +- kernel/nativelambda.ml | 215 ++++++++++++++++-------------------------------- kernel/nativelambda.mli | 2 +- 3 files changed, 73 insertions(+), 146 deletions(-) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 39f7de942..8d69eacbc 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1884,7 +1884,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 diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 5843cd543..b6d75437c 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -333,54 +333,13 @@ let rec get_alias env (kn, u as p) = (*i Global environment *) -let global_env = ref empty_env - -let set_global_env env = global_env := env - let get_names decl = let decl = Array.of_list decl in Array.map fst decl -(* Rel Environment *) -module Vect = - struct - type 'a t = { - mutable elems : 'a array; - mutable size : int; - } - - let make n a = { - elems = Array.make n a; - size = 0; - } - - let extend v = - if Int.equal v.size (Array.length v.elems) then - let new_size = min (2*v.size) Sys.max_array_length in - if new_size <= v.size then invalid_arg "Vect.extend"; - let new_elems = Array.make new_size v.elems.(0) in - Array.blit v.elems 0 new_elems 0 (v.size); - v.elems <- new_elems - - let push v a = - extend v; - v.elems.(v.size) <- a; - v.size <- v.size + 1 - - let popn v n = - v.size <- max 0 (v.size - n) - - let pop v = popn v 1 - - let get_last v n = - if v.size <= n then invalid_arg "Vect.get:index out of bounds"; - v.elems.(v.size - n - 1) - - end - let empty_args = [||] -module Renv = +module Cache = struct module ConstrHash = @@ -394,45 +353,20 @@ module Renv = type constructor_info = tag * int * int (* nparam nrealargs *) - type t = { - name_rel : Name.t Vect.t; - construct_tbl : constructor_info ConstrTable.t; - - } - - - let make () = { - name_rel = Vect.make 16 Anonymous; - construct_tbl = ConstrTable.create 111 - } - - let push_rel env id = Vect.push env.name_rel id - - let push_rels env ids = - Array.iter (push_rel env) ids - - let pop env = Vect.pop env.name_rel - - let popn env n = - for _i = 1 to n do pop env done - - let get env n = - Lrel (Vect.get_last env.name_rel (n-1), n) - - let get_construct_info env c = - try ConstrTable.find env.construct_tbl c + let get_construct_info cache env c : constructor_info = + try ConstrTable.find cache c with Not_found -> let ((mind,j), i) = c in - let oib = lookup_mind mind !global_env in + let oib = lookup_mind mind env in let oip = oib.mind_packets.(j) in let tag,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in let r = (tag, nparams, arity) in - ConstrTable.add env.construct_tbl c r; + ConstrTable.add cache c r; r end -let is_lazy prefix t = +let is_lazy env prefix t = match kind t with | App (f,args) -> begin match kind f with @@ -440,7 +374,7 @@ let is_lazy prefix t = let entry = mkInd (fst c) in (try let _ = - Retroknowledge.get_native_before_match_info (!global_env).retroknowledge + Retroknowledge.get_native_before_match_info env.retroknowledge entry prefix c Llazy; in false @@ -463,73 +397,71 @@ let empty_evars = let empty_ids = [||] -let rec lambda_of_constr env sigma c = +let rec lambda_of_constr cache env sigma c = match kind c with | Meta mv -> let ty = meta_type sigma mv in - Lmeta (mv, lambda_of_constr env sigma ty) + Lmeta (mv, lambda_of_constr cache env sigma ty) | Evar (evk,args as ev) -> (match evar_value sigma ev with | None -> let ty = evar_type sigma ev in - let args = Array.map (lambda_of_constr env sigma) args in - Levar(evk, lambda_of_constr env sigma ty, args) - | Some t -> lambda_of_constr env sigma t) + let args = Array.map (lambda_of_constr cache env sigma) args in + Levar(evk, lambda_of_constr cache env sigma ty, args) + | Some t -> lambda_of_constr cache env sigma t) - | Cast (c, _, _) -> lambda_of_constr env sigma c + | Cast (c, _, _) -> lambda_of_constr cache env sigma c - | Rel i -> Renv.get env i + | Rel i -> Lrel (RelDecl.get_name (Environ.lookup_rel i env), i) | Var id -> Lvar id | Sort s -> Lsort s | Ind (ind,u as pind) -> - let prefix = get_mind_prefix !global_env (fst ind) in + let prefix = get_mind_prefix env (fst ind) in Lind (prefix, pind) | Prod(id, dom, codom) -> - let ld = lambda_of_constr env sigma dom in - Renv.push_rel env id; - let lc = lambda_of_constr env sigma codom in - Renv.pop env; + let ld = lambda_of_constr cache env sigma dom in + let env = Environ.push_rel (RelDecl.LocalAssum (id, dom)) env in + let lc = lambda_of_constr cache env sigma codom in Lprod(ld, Llam([|id|], lc)) | Lambda _ -> let params, body = Term.decompose_lam c in + let fold (na, t) env = Environ.push_rel (RelDecl.LocalAssum (na, t)) env in + let env = List.fold_right fold params env in + let lb = lambda_of_constr cache env sigma body in let ids = get_names (List.rev params) in - Renv.push_rels env ids; - let lb = lambda_of_constr env sigma body in - Renv.popn env (Array.length ids); mkLlam ids lb - | LetIn(id, def, _, body) -> - let ld = lambda_of_constr env sigma def in - Renv.push_rel env id; - let lb = lambda_of_constr env sigma body in - Renv.pop env; + | LetIn(id, def, t, body) -> + let ld = lambda_of_constr cache env sigma def in + let env = Environ.push_rel (RelDecl.LocalDef (id, def, t)) env in + let lb = lambda_of_constr cache env sigma body in Llet(id, ld, lb) - | App(f, args) -> lambda_of_app env sigma f args + | App(f, args) -> lambda_of_app cache env sigma f args - | Const _ -> lambda_of_app env sigma c empty_args + | Const _ -> lambda_of_app cache env sigma c empty_args - | Construct _ -> lambda_of_app env sigma c empty_args + | Construct _ -> lambda_of_app cache env sigma c empty_args | Proj (p, c) -> - let pb = lookup_projection p !global_env in + let pb = lookup_projection p env in let ind = pb.proj_ind in - let prefix = get_mind_prefix !global_env (fst ind) in - mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|] + let prefix = get_mind_prefix env (fst ind) in + mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr cache env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in - let mib = lookup_mind mind !global_env in + let mib = lookup_mind mind env in let oib = mib.mind_packets.(i) in let tbl = oib.mind_reloc_tbl in (* Building info *) - let prefix = get_mind_prefix !global_env mind in + let prefix = get_mind_prefix env mind in let annot_sw = { asw_ind = ind; asw_ci = ci; @@ -538,21 +470,21 @@ let rec lambda_of_constr env sigma c = asw_prefix = prefix} in (* translation of the argument *) - let la = lambda_of_constr env sigma a in + let la = lambda_of_constr cache env sigma a in let entry = mkInd ind in let la = try - Retroknowledge.get_native_before_match_info (!global_env).retroknowledge + Retroknowledge.get_native_before_match_info (env).retroknowledge entry prefix (ind,1) la with Not_found -> la in (* translation of the type *) - let lt = lambda_of_constr env sigma t in + let lt = lambda_of_constr cache env sigma t in (* translation of branches *) let mk_branch i b = let cn = (ind,i+1) in let _, arity = tbl.(i) in - let b = lambda_of_constr env sigma b in + let b = lambda_of_constr cache env sigma b in if Int.equal arity 0 then (cn, empty_ids, b) else match b with @@ -566,85 +498,83 @@ let rec lambda_of_constr env sigma c = Lcase(annot_sw, lt, la, bs) | Fix(rec_init,(names,type_bodies,rec_bodies)) -> - let ltypes = lambda_of_args env sigma 0 type_bodies in - Renv.push_rels env names; - let lbodies = lambda_of_args env sigma 0 rec_bodies in - Renv.popn env (Array.length names); + let ltypes = lambda_of_args cache env sigma 0 type_bodies in + let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in + let lbodies = lambda_of_args cache env sigma 0 rec_bodies in Lfix(rec_init, (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> - let rec_bodies = Array.map2 (Reduction.eta_expand !global_env) rec_bodies type_bodies in - let ltypes = lambda_of_args env sigma 0 type_bodies in - Renv.push_rels env names; - let lbodies = lambda_of_args env sigma 0 rec_bodies in - Renv.popn env (Array.length names); + let rec_bodies = Array.map2 (Reduction.eta_expand env) rec_bodies type_bodies in + let ltypes = lambda_of_args cache env sigma 0 type_bodies in + let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in + let lbodies = lambda_of_args cache env sigma 0 rec_bodies in Lcofix(init, (names, ltypes, lbodies)) -and lambda_of_app env sigma f args = +and lambda_of_app cache env sigma f args = match kind f with | Const (kn,u as c) -> - let kn,u = get_alias !global_env c in - let cb = lookup_constant kn !global_env in + let kn,u = get_alias env c in + let cb = lookup_constant kn env in (try - let prefix = get_const_prefix !global_env kn in + let prefix = get_const_prefix env kn in (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_native_compiling_info - (!global_env).retroknowledge (mkConst kn) prefix in - let args = lambda_of_args env sigma 0 args in + (env).retroknowledge (mkConst kn) prefix in + let args = lambda_of_args cache env sigma 0 args in f args with Not_found -> begin match cb.const_body with | Def csubst -> (* TODO optimize if f is a proj and argument is known *) if cb.const_inline_code then - lambda_of_app env sigma (Mod_subst.force_constr csubst) args + lambda_of_app cache env sigma (Mod_subst.force_constr csubst) args else - let prefix = get_const_prefix !global_env kn in + let prefix = get_const_prefix env kn in let t = - if is_lazy prefix (Mod_subst.force_constr csubst) then + if is_lazy env prefix (Mod_subst.force_constr csubst) then mkLapp Lforce [|Lconst (prefix, (kn,u))|] else Lconst (prefix, (kn,u)) in - mkLapp t (lambda_of_args env sigma 0 args) + mkLapp t (lambda_of_args cache env sigma 0 args) | OpaqueDef _ | Undef _ -> - let prefix = get_const_prefix !global_env kn in - mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args env sigma 0 args) + let prefix = get_const_prefix env kn in + mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args) end) | Construct (c,u) -> - let tag, nparams, arity = Renv.get_construct_info env c in + let tag, nparams, arity = Cache.get_construct_info cache env c in let expected = nparams + arity in let nargs = Array.length args in - let prefix = get_mind_prefix !global_env (fst (fst c)) in + let prefix = get_mind_prefix env (fst (fst c)) in if Int.equal nargs expected then try try Retroknowledge.get_native_constant_static_info - (!global_env).retroknowledge + (env).retroknowledge f args with NotClosed -> assert (Int.equal nparams 0); (* should be fine for int31 *) - let args = lambda_of_args env sigma nparams args in + let args = lambda_of_args cache env sigma nparams args in Retroknowledge.get_native_constant_dynamic_info - (!global_env).retroknowledge f prefix c args + (env).retroknowledge f prefix c args with Not_found -> - let args = lambda_of_args env sigma nparams args in - makeblock !global_env c u tag args + let args = lambda_of_args cache env sigma nparams args in + makeblock env c u tag args else - let args = lambda_of_args env sigma 0 args in + let args = lambda_of_args cache env sigma 0 args in (try Retroknowledge.get_native_constant_dynamic_info - (!global_env).retroknowledge f prefix c args + (env).retroknowledge f prefix c args with Not_found -> mkLapp (Lconstruct (prefix, (c,u))) args) | _ -> - let f = lambda_of_constr env sigma f in - let args = lambda_of_args env sigma 0 args in + let f = lambda_of_constr cache env sigma f in + let args = lambda_of_args cache env sigma 0 args in mkLapp f args -and lambda_of_args env sigma start args = +and lambda_of_args cache env sigma start args = let nargs = Array.length args in if start < nargs then Array.init (nargs - start) - (fun i -> lambda_of_constr env sigma args.(start + i)) + (fun i -> lambda_of_constr cache env sigma args.(start + i)) else empty_args let optimize lam = @@ -657,11 +587,8 @@ let optimize lam = lam let lambda_of_constr env sigma c = - set_global_env env; - let env = Renv.make () in - let ids = List.rev_map RelDecl.get_name (rel_context !global_env) in - Renv.push_rels env (Array.of_list ids); - let lam = lambda_of_constr env sigma c in + let cache = Cache.ConstrTable.create 91 in + let lam = lambda_of_constr cache env sigma c in (* if Flags.vm_draw_opt () then begin (msgerrnl (str "Constr = \n" ++ pr_constr c);flush_all()); (msgerrnl (str "Lambda = \n" ++ pp_lam lam);flush_all()); diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 26bfeb7e0..efe1700cd 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -23,7 +23,7 @@ val empty_evars : evars val decompose_Llam : lambda -> Name.t array * lambda val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda -val is_lazy : prefix -> constr -> bool +val is_lazy : env -> prefix -> constr -> bool val mk_lazy : lambda -> lambda val get_mind_prefix : env -> MutInd.t -> string -- cgit v1.2.3 From beb417ffd2ab9acb708c4e54dd28363bcb613853 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 13 Jul 2018 02:09:56 +0200 Subject: Store the {struct} inductive type in native fixpoint AST. --- kernel/nativecode.ml | 2 +- kernel/nativeinstr.mli | 2 +- kernel/nativelambda.ml | 24 ++++++++++++++++++++++-- 3 files changed, 24 insertions(+), 4 deletions(-) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 8d69eacbc..b09cd3f79 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1142,7 +1142,7 @@ let ml_of_instance instance u = 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 .. diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index eaad8ee0c..5075bd3d1 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -36,7 +36,7 @@ and lambda = | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda - | Lfix of (int array * int) * fix_decl + | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index b6d75437c..a5cdd0a19 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -397,6 +397,20 @@ let empty_evars = let empty_ids = [||] +(** Extract the inductive type over which a fixpoint is decreasing *) +let rec get_fix_struct env i t = match kind (Reduction.whd_all env t) with +| Prod (na, dom, t) -> + if Int.equal i 0 then + let dom = Reduction.whd_all env dom in + let (dom, _) = decompose_appvect dom in + match kind dom with + | Ind (ind, _) -> ind + | _ -> assert false + else + let env = Environ.push_rel (RelDecl.LocalAssum (na, dom)) env in + get_fix_struct env (i - 1) t +| _ -> assert false + let rec lambda_of_constr cache env sigma c = match kind c with | Meta mv -> @@ -497,11 +511,17 @@ let rec lambda_of_constr cache env sigma c = let bs = Array.mapi mk_branch branches in Lcase(annot_sw, lt, la, bs) - | Fix(rec_init,(names,type_bodies,rec_bodies)) -> + | Fix((pos, i), (names,type_bodies,rec_bodies)) -> let ltypes = lambda_of_args cache env sigma 0 type_bodies in + let map i t = + let ind = get_fix_struct env i t in + let prefix = get_mind_prefix env (fst ind) in + (prefix, ind) + in + let inds = Array.map2 map pos type_bodies in let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in let lbodies = lambda_of_args cache env sigma 0 rec_bodies in - Lfix(rec_init, (names, ltypes, lbodies)) + Lfix((pos, inds, i), (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> let rec_bodies = Array.map2 (Reduction.eta_expand env) rec_bodies type_bodies in -- cgit v1.2.3 From 140aa841e808f01a47e11df31cbd188d910c0b58 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 13 Jul 2018 02:41:52 +0200 Subject: Generate type-specific code for is_accu in native compilation of fixpoints. This is much more efficient than using Nativevalues.is_accu function which incurs a lot of irrelevant checks on its argument. --- kernel/nativecode.ml | 28 ++++++++++++++++++++-------- kernel/nativevalues.mli | 3 --- 2 files changed, 20 insertions(+), 11 deletions(-) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index b09cd3f79..ec6c5b297 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -278,7 +278,6 @@ type primitive = | Mk_rel of int | Mk_var of Id.t | Mk_proj - | Is_accu | Is_int | Cast_accu | Upd_cofix @@ -319,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 @@ -345,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 @@ -396,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 @@ -467,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) = @@ -542,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) = @@ -608,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 @@ -1211,8 +1217,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|])) @@ -1374,6 +1381,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 @@ -1471,7 +1479,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 @@ -1483,6 +1491,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 @@ -1645,7 +1654,11 @@ 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 @@ -1738,7 +1751,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" diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 649853f06..6bbf15160 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -110,9 +110,6 @@ type kind_of_value = val kind_of_value : t -> kind_of_value -(* *) -val is_accu : t -> bool - val str_encode : 'a -> string val str_decode : string -> 'a -- cgit v1.2.3