diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-29 19:05:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-04 11:28:49 +0200 |
| commit | 1db568d3dc88d538f975377bb4d8d3eecd87872c (patch) | |
| tree | d8e35952cc8f6111875e664d8884dc2c7f908206 /interp/constrextern.mli | |
| parent | 3072bd9d080984833f5eb007bf15c6e9305619e3 (diff) | |
Making detyping potentially lazy.
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
Diffstat (limited to 'interp/constrextern.mli')
| -rw-r--r-- | interp/constrextern.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index ffa891c50..593580fb7 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -23,9 +23,9 @@ open Misctypes (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) -val extern_cases_pattern : Id.Set.t -> cases_pattern -> cases_pattern_expr -val extern_glob_constr : Id.Set.t -> glob_constr -> constr_expr -val extern_glob_type : Id.Set.t -> glob_constr -> constr_expr +val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr +val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr +val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob_constr -> constr_expr |