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, 29 insertions, 11 deletions

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 8e6329a15..d01bdc1b9 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -184,9 +184,13 @@ let havetac ist
       mkt ct, mkt cty, mkt (mkCHole None), loc
     | _, (_, Some ct) ->
       mkt ct, mkt (mkCHole None), mkt (mkCHole None), None
-    | _, ({ loc; v = GCast (ct, CastConv cty) }, None) ->
-      mkl ct, mkl cty, mkl mkRHole, loc
-    | _, (t, None) -> mkl t, mkl mkRHole, mkl mkRHole, None in
+    | _, (t, None) ->
+      begin match DAst.get t with
+      | GCast (ct, CastConv cty) ->
+        mkl ct, mkl cty, mkl mkRHole, t.CAst.loc
+      | _ -> mkl t, mkl mkRHole, mkl mkRHole, None
+      end
+  in
   let gl, cut, sol, itac1, itac2 =
    match fk, namefst, suff with
    | FwdHave, true, true ->
@@ -323,11 +327,18 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
   let mkpats = function
   | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats
   | _ -> fun x -> x in
-  let open CAst in
   let ct = match ct with
-  | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty)
-  | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None)
-  | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" in
+  | (a, (b, Some ct)) ->
+    begin match ct.CAst.v with
+    | CCast (_, CastConv cty) -> a, (b, Some cty)
+    | _ -> anomaly "wlog: ssr cast hole deleted by typecheck"
+    end
+  | (a, (t, None)) ->
+    begin match DAst.get t with
+    | GCast (_, CastConv cty) -> a, (cty, None)
+    | _ -> anomaly "wlog: ssr cast hole deleted by typecheck"
+    end
+  in
   let cut_implies_goal = not (suff || ghave <> `NoGen) in
   let c, args, ct, gl =
     let gens = List.filter (function _, Some _ -> true | _ -> false) gens in
@@ -398,11 +409,18 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
 
 let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
   let htac = Tacticals.tclTHEN (introstac ~ist pats) (hinttac ist true hint) in
-  let open CAst in
   let c = match c with
-  | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty)
-  | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None)
-  | _ -> anomaly "suff: ssr cast hole deleted by typecheck" in
+  | (a, (b, Some ct)) ->
+    begin match ct.CAst.v with
+    | CCast (_, CastConv cty) -> a, (b, Some cty)
+    | _ -> anomaly "suff: ssr cast hole deleted by typecheck"
+    end
+  | (a, (t, None)) ->
+    begin match DAst.get t with
+    | GCast (_, CastConv cty) -> a, (cty, None)
+    | _ -> anomaly "suff: ssr cast hole deleted by typecheck"
+    end
+  in
   let ctac gl =
     let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
     basecuttac "ssr_suff" ty gl in