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, 49 insertions, 33 deletions

diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index dd122b972..757ba5786 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -24,66 +24,82 @@ type existential_name = Id.t
 (**  The kind of patterns that occurs in "match ... with ... end"
 
      locs here refers to the ident's location, not whole pat *)
-type cases_pattern_r =
+type 'a cases_pattern_r =
   | PatVar  of Name.t
-  | PatCstr of constructor * cases_pattern list * Name.t
+  | PatCstr of constructor * 'a cases_pattern_g list * Name.t
       (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
-and cases_pattern = cases_pattern_r CAst.t
+and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t
+
+type cases_pattern = [ `any ] cases_pattern_g
 
 (** Representation of an internalized (or in other words globalized) term. *)
-type glob_constr_r =
+type 'a glob_constr_r =
   | GRef of global_reference * glob_level list option
       (** An identifier that represents a reference to an object defined
           either in the (global) environment or in the (local) context. *)
   | GVar of Id.t
       (** An identifier that cannot be regarded as "GRef".
           Bound variables are typically represented this way. *)
-  | GEvar   of existential_name * (Id.t * glob_constr) list
+  | GEvar   of existential_name * (Id.t * 'a glob_constr_g) list
   | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *)
-  | GApp    of glob_constr * glob_constr list
-  | GLambda of Name.t * binding_kind *  glob_constr * glob_constr
-  | GProd   of Name.t * binding_kind * glob_constr * glob_constr
-  | GLetIn  of Name.t * glob_constr * glob_constr option * glob_constr
-  | GCases  of case_style * glob_constr option * tomatch_tuples * cases_clauses
+  | GApp    of 'a glob_constr_g * 'a glob_constr_g list
+  | GLambda of Name.t * binding_kind *  'a glob_constr_g * 'a glob_constr_g
+  | GProd   of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g
+  | GLetIn  of Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g
+  | GCases  of case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g
       (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
-  | GLetTuple of Name.t list * (Name.t * glob_constr option) * glob_constr * glob_constr
-  | GIf   of glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr
-  | GRec  of fix_kind * Id.t array * glob_decl list array *
-             glob_constr array * glob_constr array
+  | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
+  | GIf   of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
+  | GRec  of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array *
+             'a glob_constr_g array * 'a glob_constr_g array
   | GSort of glob_sort
   | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option
-  | GCast of glob_constr * glob_constr cast_type
-and glob_constr = glob_constr_r CAst.t
+  | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
+and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
 
-and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr
+and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
 
-and fix_recursion_order =
+and 'a fix_recursion_order_g =
   | GStructRec
-  | GWfRec of glob_constr
-  | GMeasureRec of glob_constr * glob_constr option
+  | GWfRec of 'a glob_constr_g
+  | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option
 
-and fix_kind =
-  | GFix of ((int option * fix_recursion_order) array * int)
+and 'a fix_kind_g =
+  | GFix of ((int option * 'a fix_recursion_order_g) array * int)
   | GCoFix of int
 
-and predicate_pattern =
+and 'a predicate_pattern_g =
     Name.t * (inductive * Name.t list) Loc.located option
       (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
 
-and tomatch_tuple = (glob_constr * predicate_pattern)
+and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g)
 
-and tomatch_tuples = tomatch_tuple list
+and 'a tomatch_tuples_g = 'a tomatch_tuple_g list
 
-and cases_clause = (Id.t list * cases_pattern list * glob_constr) Loc.located
+and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) Loc.located
 (** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables
     of [t] are members of [il]. *)
-and cases_clauses = cases_clause list
-
-type extended_glob_local_binder_r =
-  | GLocalAssum   of Name.t * binding_kind * glob_constr
-  | GLocalDef     of Name.t * binding_kind * glob_constr * glob_constr option
-  | GLocalPattern of (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr
-and extended_glob_local_binder = extended_glob_local_binder_r CAst.t
+and 'a cases_clauses_g = 'a cases_clause_g list
+
+type glob_constr = [ `any ] glob_constr_g
+type tomatch_tuple = [ `any ] tomatch_tuple_g
+type tomatch_tuples = [ `any ] tomatch_tuples_g
+type cases_clause = [ `any ] cases_clause_g
+type cases_clauses = [ `any ] cases_clauses_g
+type glob_decl = [ `any ] glob_decl_g
+type fix_kind = [ `any ] fix_kind_g
+type predicate_pattern = [ `any ] predicate_pattern_g
+type fix_recursion_order = [ `any ] fix_recursion_order_g
+
+type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr
+
+type 'a extended_glob_local_binder_r =
+  | GLocalAssum   of Name.t * binding_kind * 'a glob_constr_g
+  | GLocalDef     of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option
+  | GLocalPattern of ('a cases_pattern_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g
+and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t
+
+type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g
 
 (** A globalised term together with a closure representing the value
     of its free variables. Intended for use when these variables are taken