From 1db568d3dc88d538f975377bb4d8d3eecd87872c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Aug 2017 19:05:57 +0200
Subject: 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.
---
 interp/implicit_quantifiers.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index e498d979de..cae67c3e70 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -119,13 +119,14 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li
   in aux bound l binders
 
 let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
-  let rec vars bound vs t = match t with
-    | { loc; CAst.v = GVar id } ->
+  let rec vars bound vs c = match DAst.get c with
+    | GVar id ->
+        let loc = c.CAst.loc in
 	if is_freevar bound (Global.env ()) id then
 	  if Id.List.mem_assoc_sym id vs then vs
 	  else (Loc.tag ?loc id) :: vs
 	else vs
-    | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
+    | _ -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
   in fun rt -> 
     let vars = List.rev (vars bound [] rt) in
       List.iter (fun (loc, id) ->
@@ -253,11 +254,11 @@ let implicits_of_glob_constr ?(with_products=true) l =
     (ExplByPos (i, name), (true, true, true)) :: l
   | _ -> l
   in
-  let rec aux i { loc; CAst.v = c } =
+  let rec aux i c =
     let abs na bk b =
       add_impl i na bk (aux (succ i) b)
     in
-      match c with
+      match DAst.get c with
       | GProd (na, bk, t, b) ->
 	  if with_products then abs na bk b
 	  else
-- 
cgit v1.2.3