aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--configure.ml3
-rw-r--r--ide/gtk_parsing.ml7
-rw-r--r--interp/constrintern.ml2
-rw-r--r--kernel/nativecode.ml32
-rw-r--r--kernel/nativeinstr.mli2
-rw-r--r--kernel/nativelambda.ml239
-rw-r--r--kernel/nativelambda.mli2
-rw-r--r--kernel/nativevalues.mli3
-rw-r--r--plugins/funind/recdef.mli2
-rw-r--r--plugins/micromega/mutils.mli2
-rw-r--r--vernac/proof_using.ml10
11 files changed, 128 insertions, 176 deletions
diff --git a/configure.ml b/configure.ml
index c08e8dfcc..7fd900d99 100644
--- a/configure.ml
+++ b/configure.ml
@@ -475,6 +475,7 @@ let coq_bin_annot_flag = if !prefs.bin_annot then "-bin-annot" else ""
(* This variable can be overriden only for debug purposes, use with
care. *)
let coq_safe_string = "-safe-string"
+let coq_strict_sequence = "-strict-sequence"
let cflags = "-Wall -Wno-unused -g -O2"
@@ -661,7 +662,7 @@ let coq_warn_error =
(* Flags used to compile Coq and plugins (via coq_makefile) *)
let caml_flags =
- Printf.sprintf "-thread -rectypes %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string
+ Printf.sprintf "-thread -rectypes %s %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string coq_strict_sequence
(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *)
let coq_caml_flags =
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index 9f5c99244..d554bebdd 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -35,8 +35,11 @@ let find_word_start (it:GText.iter) =
(Minilib.log "find_word_start: cannot backward"; it)
else if is_word_char it#char
then step_to_start it
- else (it#nocopy#forward_char;
- Minilib.log ("Word start at: "^(string_of_int it#offset));it)
+ else begin
+ ignore(it#nocopy#forward_char);
+ Minilib.log ("Word start at: "^(string_of_int it#offset));
+ it
+ end
in
step_to_start it#copy
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 18d6c1a5b..9a4f2177f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -552,7 +552,7 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id =
let is_var store pat =
match DAst.get pat with
- | PatVar na -> store na; true
+ | PatVar na -> ignore(store na); true
| _ -> false
let out_var pat =
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 39f7de942..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
@@ -1142,7 +1148,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
..
@@ -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"
@@ -1884,7 +1896,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/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 5843cd543..a5cdd0a19 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,85 @@ let empty_evars =
let empty_ids = [||]
-let rec lambda_of_constr env sigma c =
+(** 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 ->
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 +484,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
@@ -565,86 +511,90 @@ let rec lambda_of_constr 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)) ->
- 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);
- Lfix(rec_init, (names, ltypes, lbodies))
+ | 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((pos, inds, i), (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 +607,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
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
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index b95d64ce9..549f1fc0e 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -14,6 +14,6 @@ bool ->
int -> Constrexpr.constr_expr -> (pconstant ->
Indfun_common.tcc_lemma_value ref ->
pconstant ->
- pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+ pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit
diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli
index 7b7a090de..094429ea1 100644
--- a/plugins/micromega/mutils.mli
+++ b/plugins/micromega/mutils.mli
@@ -30,7 +30,7 @@ end
module TagSet : CSig.SetS with type elt = Tag.t
-val pp_list : (out_channel -> 'a -> 'b) -> out_channel -> 'a list -> unit
+val pp_list : (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit
module CamlToCoq : sig
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 74e53bef1..3e2bd9872 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -18,14 +18,6 @@ module NamedDecl = Context.Named.Declaration
let known_names = Summary.ref [] ~name:"proofusing-nameset"
-let in_nameset =
- let open Libobject in
- declare_object { (default_object "proofusing-nameset") with
- cache_function = (fun (_,x) -> known_names := x :: !known_names);
- classify_function = (fun _ -> Dispose);
- discharge_function = (fun _ -> None)
- }
-
let rec close_fwd e s =
let s' =
List.fold_left (fun s decl ->
@@ -73,7 +65,7 @@ let process_expr env e ty =
let s = Id.Set.union v_ty (process_expr env e ty) in
Id.Set.elements s
-let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
+let name_set id expr = known_names := (id,expr) :: !known_names
let minimize_hyps env ids =
let rec aux ids =
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 18:53:47 +0000