diff options
| author | Arnaud Spiwack | 2014-08-01 19:14:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-01 19:18:59 +0200 |
| commit | 94b201b0a7b03978d96b8f8c9d631e4fa4bda4b0 (patch) | |
| tree | 998601ebfb4ad8163bd6c3fb81fabe331c154947 | |
| parent | b240b7d0cfd6233dcb0ba0e3b98354c78c23a0d4 (diff) | |
Faster uconstr.
Detyping was called on every typed constr in the Ltac context which was costly as most of the context is likely not to be refered to in a particular uconstr. This commit calls detyping lazily instead.
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 | ||||
| -rw-r--r-- | tactics/taccoerce.ml | 4 | ||||
| -rw-r--r-- | tactics/taccoerce.mli | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 95d902fd40..04e9fceff6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -654,7 +654,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = GVar (loc,id), [], [], [] (* Is [id] bound to a glob_constr in the the ltac context *) else if Id.Map.mem id ltacsubst then - Id.Map.find id ltacsubst, [], [], [] + Lazy.force (Id.Map.find id ltacsubst), [], [], [] (* Is [id] a notation variable *) else if Id.Map.mem id ntnvars then @@ -1769,7 +1769,7 @@ let scope_of_type_kind = function | OfType typ -> compute_type_scope typ | WithoutTypeConstraint -> None -type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Id.Map.t +type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Lazy.t Id.Map.t let empty_ltac_sign = (Id.Set.empty, Id.Set.empty, Id.Map.empty) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 2b61c51dc9..46697253bd 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -67,7 +67,7 @@ val compute_internalization_env : env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env -type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Id.Map.t +type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Lazy.t Id.Map.t type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 4152218197..0697ae5529 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -150,10 +150,10 @@ let coerce_to_constr env v = let coerce_to_uconstr env v = let v = Value.normalize v in if has_type v (topwit wit_uconstr) then - out_gen (topwit wit_uconstr) v + Lazy.lazy_from_val (out_gen (topwit wit_uconstr) v) else let (_ctx,c) = coerce_to_constr env v in - Detyping.detype false [] [] c + lazy (Detyping.detype false [] [] c) let coerce_to_closed_constr env v = let ids,c = coerce_to_constr env v in diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index b4c0283c92..171269f929 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -58,7 +58,7 @@ val coerce_to_int : Value.t -> int val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders -val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.glob_constr +val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.glob_constr Lazy.t val coerce_to_closed_constr : Environ.env -> Value.t -> constr |