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/notation.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/notation.mli')
| -rw-r--r-- | interp/notation.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index f9f247fe1..75c8d5aa5 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -70,7 +70,7 @@ type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr type 'a prim_token_uninterpreter = - glob_constr list * (glob_constr -> 'a option) * cases_pattern_status + glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign @@ -96,9 +96,9 @@ val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> un raise [No_match] if no such token *) val uninterp_prim_token : - glob_constr -> scope_name * prim_token + 'a glob_constr_g -> scope_name * prim_token val uninterp_prim_token_cases_pattern : - cases_pattern -> Name.t * scope_name * prim_token + 'a cases_pattern_g -> Name.t * scope_name * prim_token val uninterp_prim_token_ind_pattern : inductive -> cases_pattern list -> scope_name * prim_token @@ -124,8 +124,8 @@ val interp_notation : ?loc:Loc.t -> notation -> local_scopes -> type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : glob_constr -> notation_rule list -val uninterp_cases_pattern_notations : cases_pattern -> notation_rule list +val uninterp_notations : 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list val uninterp_ind_pattern_notations : inductive -> notation_rule list (** Test if a notation is available in the scopes |