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 /pretyping/detyping.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 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 59f3f967d..67c852af3 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -16,6 +16,10 @@ open Mod_subst open Misctypes open Evd +type _ delay = +| Now : 'a delay +| Later : [ `thunk ] delay + (** Should we keep details of universes during detyping ? *) val print_universes : bool ref @@ -33,12 +37,12 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr -val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr +val detype : 'a delay -> ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> 'a glob_constr_g val detype_sort : evar_map -> sorts -> glob_sort -val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> - evar_map -> rel_context -> glob_decl list +val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> + evar_map -> rel_context -> 'a glob_decl_g list val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr @@ -47,7 +51,7 @@ val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option (* XXX: This is a hack and should go away *) -val set_detype_anonymous : (?loc:Loc.t -> int -> glob_constr) -> unit +val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool |