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, 37 insertions, 25 deletions

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index f6300ab7e..2e5522b83 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -134,6 +134,10 @@ let dC t = CastConv t
 let isCVar   = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false
 let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ ->
   CErrors.anomaly (str"not a CRef.")
+let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false
+let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c)
+  | _ -> CErrors.anomaly (str "not a GLambda")
+let isGHole c = match DAst.get c with GHole _ -> true | _ -> false
 let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
 let mkCLambda ?loc name ty t = CAst.make ?loc @@
    CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t)
@@ -141,10 +145,10 @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@
    CLetIn ((Loc.tag ?loc name), bo, None, t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)
 (** Constructors for rawconstr *)
-let mkRHole = CAst.make @@ GHole (InternalHole, IntroAnonymous, None)
-let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args)
-let mkRCast rc rt =  CAst.make @@ GCast (rc, dC rt)
-let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t)
+let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None)
+let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
+let mkRCast rc rt =  DAst.make @@ GCast (rc, dC rt)
+let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
 
 (* ssrterm conbinators *)
 let combineCG t1 t2 f g = match t1, t2 with
@@ -980,11 +984,10 @@ let pr_rpattern = pr_pattern
 
 type pattern = Evd.evar_map * (constr, constr) ssrpattern
 
-
-let id_of_cpattern = let open CAst in function
-  | _,(_,Some { v = CRef (Ident (_, x), _) } ) -> Some x
-  | _,(_,Some { v = CAppExpl ((_, Ident (_, x), _), []) } ) -> Some x
-  | _,({ v = GRef (VarRef x, _)} ,None) -> Some x
+let id_of_cpattern (_, (c1, c2)) = let open CAst in match DAst.get c1, c2 with
+  | _, Some { v = CRef (Ident (_, x), _) } -> Some x
+  | _, Some { v = CAppExpl ((_, Ident (_, x), _), []) } -> Some x
+  | GRef (VarRef x, _), None -> Some x
   | _ -> None
 let id_of_Cterm t = match id_of_cpattern t with
   | Some x -> x
@@ -1082,10 +1085,11 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   let eAsXInT e x t = E_As_X_In_T(e,x,t) in
   let mkG ?(k=' ') x = k,(x,None) in
   let decode ist t ?reccall f g =
-    let open CAst in
-    try match (pf_intern_term ist gl t) with
-    | { v = GCast({ v = GHole _},CastConv({ v = GLambda(Name x,_,_,c)})) } -> f x (' ',(c,None))
-    | { v = GVar id }
+    try match DAst.get (pf_intern_term ist gl t) with
+    | GCast(t,CastConv c) when isGHole t && isGLambda c->
+      let (x, c) = destGLambda c in
+      f x (' ',(c,None))
+    | GVar id
       when Id.Map.mem id ist.lfun &&
            not(Option.is_empty reccall) &&
            not(Option.is_empty wit_ssrpatternarg) ->
@@ -1126,19 +1130,27 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
         thin name sigma e)
       sigma new_evars in
     sigma in
-  let red = let rec decode_red (ist,red) = let open CAst in match red with
-    | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None))
-        when let id = Id.to_string id in let len = String.length id in
+  let red = let rec decode_red (ist,red) = match red with
+    | T(k,(t,None)) ->
+      begin match DAst.get t with
+      | GCast (c,CastConv t)
+        when isGHole c &&
+          let (id, t) = destGLambda t in
+          let id = Id.to_string id in let len = String.length id in
         (len > 8 && String.sub id 0 8 = "_ssrpat_") ->
+        let (id, t) = destGLambda t in
         let id = Id.to_string id in let len = String.length id in
-        (match String.sub id 8 (len - 8), t with
-        | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x)
-        | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id)
-        | "In", { v = GApp( _, [e; t; e_in_t]) } ->
+        (match String.sub id 8 (len - 8), DAst.get t with
+        | "In", GApp( _, [t]) -> decodeG t xInT (fun x -> T x)
+        | "In", GApp( _, [e; t]) -> decodeG t (eInXInT (mkG e)) (bad_enc id)
+        | "In", GApp( _, [e; t; e_in_t]) ->
             decodeG t (eInXInT (mkG e))
               (fun _ -> decodeG e_in_t xInT (fun _ -> assert false))
-        | "As", { v = GApp(_, [e; t]) } -> decodeG t (eAsXInT (mkG e)) (bad_enc id)
+        | "As", GApp(_, [e; t]) -> decodeG t (eAsXInT (mkG e)) (bad_enc id)
         | _ -> bad_enc id ())
+      | _ ->
+        decode ist ~reccall:decode_red (k, (t, None)) xInT (fun x -> T x)
+      end
     | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x)
     | In_T t -> decode ist t inXInT inT
     | X_In_T (e,t) -> decode ist t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x)
@@ -1163,7 +1175,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
   let mkXLetIn ?loc x (a,(g,c)) = match c with
   | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b))
-  | None -> a,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in
+  | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in
   match red with
   | T t -> let sigma, t = interp_term ist gl t in sigma, T t
   | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t
@@ -1336,10 +1348,10 @@ let pf_fill_occ_term gl occ t =
   let cl,(_,t) = fill_occ_term env concl occ sigma0 t in
   cl, t
 
-let cpattern_of_id id = ' ', (CAst.make @@ GRef (VarRef  id, None), None)
+let cpattern_of_id id = ' ', (DAst.make @@ GRef (VarRef  id, None), None)
 
-let is_wildcard : cpattern -> bool = function
-  | _,(_,Some { CAst.v = CHole _ } | { CAst.v = GHole _ } ,None) -> true
+let is_wildcard ((_, (l, r)) : cpattern) : bool = match DAst.get l, r with
+  | _, Some { CAst.v = CHole _ } | GHole _, None -> true
   | _ -> false
 
 (* "ssrpattern" *)