From b283c7674c4bff8ac2be52e896a40ba155c3d994 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 27 Jul 2016 09:03:42 +0200 Subject: Exporting the renaming API for evar declaration. --- engine/evarutil.mli | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'engine/evarutil.mli') diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 111d0f3e8c..a4200d762b 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -199,6 +199,13 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> Id.Set.t -> named_context_val * types * types +val push_rel_decl_to_named_context : + Context.Rel.Declaration.t -> + Vars.substl * (Names.Id.t * Constr.constr) list * + Names.Id.t list * Environ.env -> + Term.constr list * (Names.Id.t * Constr.constr) list * + Names.Id.t list * Environ.env + val push_rel_context_to_named_context : Environ.env -> types -> named_context_val * types * constr list * constr list * (identifier*constr) list -- cgit v1.2.3 From 62d5ef53da153394c69b52cc707b72d53eaeac44 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 4 Aug 2016 15:32:48 +0200 Subject: Simplifying code in evar generation. We remove in particular a dubious use of an environment in fresh name generation. The code was using the wrong environment in a function only depending on the rel context which was resetted most of the time. This might change the generated names in extremely rare occurences. --- engine/evarutil.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/evarutil.mli') diff --git a/engine/evarutil.mli b/engine/evarutil.mli index a4200d762b..95b8b3e0bb 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -202,9 +202,9 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty val push_rel_decl_to_named_context : Context.Rel.Declaration.t -> Vars.substl * (Names.Id.t * Constr.constr) list * - Names.Id.t list * Environ.env -> + Names.Id.t list * Context.Named.t -> Term.constr list * (Names.Id.t * Constr.constr) list * - Names.Id.t list * Environ.env + Names.Id.t list * Context.Named.t val push_rel_context_to_named_context : Environ.env -> types -> named_context_val * types * constr list * constr list * (identifier*constr) list -- cgit v1.2.3 From 118572b57a6f15ad4342e8a75ca0836e7896d465 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 4 Aug 2016 18:46:05 +0200 Subject: Use sets instead of lists for names to avoid in evar generation. --- engine/evarutil.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'engine/evarutil.mli') diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 95b8b3e0bb..45f0d6b078 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -201,10 +201,10 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty val push_rel_decl_to_named_context : Context.Rel.Declaration.t -> - Vars.substl * (Names.Id.t * Constr.constr) list * - Names.Id.t list * Context.Named.t -> - Term.constr list * (Names.Id.t * Constr.constr) list * - Names.Id.t list * Context.Named.t + Vars.substl * (Id.t * Constr.constr) list * + Id.Set.t * Context.Named.t -> + Term.constr list * (Id.t * Constr.constr) list * + Id.Set.t * Context.Named.t val push_rel_context_to_named_context : Environ.env -> types -> named_context_val * types * constr list * constr list * (identifier*constr) list -- cgit v1.2.3 From 26e5194bc252e4ac71c74f8ac73a0e2cbe82edf6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 4 Aug 2016 19:18:48 +0200 Subject: Using the extended contexts in pretyping. In addition to sharing, we also delay the computation of the environment in a by-need fashion. --- engine/evarutil.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'engine/evarutil.mli') diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 45f0d6b078..429ea73de1 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -199,13 +199,13 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> Id.Set.t -> named_context_val * types * types -val push_rel_decl_to_named_context : - Context.Rel.Declaration.t -> +type ext_named_context = Vars.substl * (Id.t * Constr.constr) list * - Id.Set.t * Context.Named.t -> - Term.constr list * (Id.t * Constr.constr) list * Id.Set.t * Context.Named.t +val push_rel_decl_to_named_context : + Context.Rel.Declaration.t -> ext_named_context -> ext_named_context + val push_rel_context_to_named_context : Environ.env -> types -> named_context_val * types * constr list * constr list * (identifier*constr) list -- cgit v1.2.3 From f1e1b7f735c8cd4a1f3cc52e7f9a7cdf1481ffe5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 5 Aug 2016 12:38:12 +0200 Subject: Using a dedicated kind of substitutions in evar name generation. This saves a quadratic allocation by replacing arrays with maps. --- engine/evarutil.mli | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'engine/evarutil.mli') diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 429ea73de1..c0c81442d5 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -199,15 +199,20 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> Id.Set.t -> named_context_val * types * types +type csubst + +val empty_csubst : csubst +val csubst_subst : csubst -> Constr.t -> Constr.t + type ext_named_context = - Vars.substl * (Id.t * Constr.constr) list * + csubst * (Id.t * Constr.constr) list * Id.Set.t * Context.Named.t val push_rel_decl_to_named_context : Context.Rel.Declaration.t -> ext_named_context -> ext_named_context val push_rel_context_to_named_context : Environ.env -> types -> - named_context_val * types * constr list * constr list * (identifier*constr) list + named_context_val * types * constr list * csubst * (identifier*constr) list val generalize_evar_over_rels : evar_map -> existential -> types * constr list -- cgit v1.2.3