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.

1 files changed, 12 insertions, 12 deletions

diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index bd9e111f5..bacc8fbe4 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -11,21 +11,21 @@ open Glob_term
 
 (** Equalities *)
 
-val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
+val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
 val cast_type_eq : ('a -> 'a -> bool) ->
   'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
 
-val glob_constr_eq : glob_constr -> glob_constr -> bool
+val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool
 
 (** Operations on [glob_constr] *)
 
-val cases_pattern_loc : cases_pattern -> Loc.t option
+val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option
 
-val cases_predicate_names : tomatch_tuples -> Name.t list
+val cases_predicate_names : 'a tomatch_tuples_g -> Name.t list
 
 (** Apply one argument to a glob_constr *)
-val mkGApp : ?loc:Loc.t -> glob_constr -> glob_constr -> glob_constr
+val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_constr_g
 
 val map_glob_constr :
   (glob_constr -> glob_constr) -> glob_constr -> glob_constr
@@ -42,12 +42,12 @@ val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) ->
 val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
-val occur_glob_constr : Id.t -> glob_constr -> bool
-val free_glob_vars : glob_constr -> Id.t list
+val occur_glob_constr : Id.t -> 'a glob_constr_g -> bool
+val free_glob_vars : 'a glob_constr_g -> Id.t list
 val bound_glob_vars : glob_constr -> Id.Set.t
 (* Obsolete *)
-val loc_of_glob_constr : glob_constr -> Loc.t option
-val glob_visible_short_qualid : glob_constr -> Id.t list
+val loc_of_glob_constr : 'a glob_constr_g -> Loc.t option
+val glob_visible_short_qualid : 'a glob_constr_g -> Id.t list
 
 (* Renaming free variables using a renaming map; fails with
    [UnsoundRenaming] if applying the renaming would introduce
@@ -57,7 +57,7 @@ val glob_visible_short_qualid : glob_constr -> Id.t list
 
 exception UnsoundRenaming
 val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t
-val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr
+val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_g
 
 (** [map_pattern_binders f m c] applies [f] to all the binding names
     in a pattern-matching expression ({!Glob_term.GCases}) represented
@@ -80,9 +80,9 @@ val map_pattern : (glob_constr -> glob_constr) ->
     @raise Not_found if translation is impossible *)
 val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
 
-val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr
+val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g
 
-val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list
+val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
 
 val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name
 val empty_lvar : Glob_term.ltac_var_map