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.

5 files changed, 23 insertions, 22 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index b847aadf21..99e4440102 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -626,19 +626,19 @@ END
 let subst_var_with_hole occ tid t = 
   let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
   let locref = ref 0 in
-  let rec substrec = function
-    | { CAst.v = GVar id } as x -> 
+  let rec substrec x = match DAst.get x with
+    | GVar id ->
         if Id.equal id tid 
         then
 	  (decr occref;
 	   if Int.equal !occref 0 then x
            else
 	     (incr locref;
-              CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
+              DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
 	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
                      Misctypes.IntroAnonymous, None)))
         else x
-    | c -> map_glob_constr_left_to_right substrec c in
+    | _ -> map_glob_constr_left_to_right substrec x in
   let t' = substrec t
   in
   if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t'
@@ -646,15 +646,15 @@ let subst_var_with_hole occ tid t =
 let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
-  let rec substrec = function
-    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } ->
+  let rec substrec c = match DAst.get c with
+    | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
-           CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
+           DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
 	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s))
-    | c -> map_glob_constr_left_to_right substrec c
+    | _ -> map_glob_constr_left_to_right substrec c
   in
   substrec t
 
@@ -666,8 +666,8 @@ let hResolve id c occ t =
   let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
   let concl = Proofview.Goal.concl gl in
   let env_ids = Termops.ids_of_context env in
-  let c_raw = Detyping.detype true env_ids env sigma c in
-  let t_raw = Detyping.detype true env_ids env sigma t in
+  let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in
+  let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in
   let rec resolve_hole t_hole =
     try 
       Pretyping.understand env sigma t_hole
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c874f8d5a3..c22e683235 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -123,7 +123,7 @@ END
 
 let clsubstitute o c =
   Proofview.Goal.enter begin fun gl ->
-  let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in
+  let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in
   let hyps = Tacmach.New.pf_ids_of_hyps gl in
     Tacticals.New.tclMAP
       (fun cl ->
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index cb7d9b9c02..f4e3ba633f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1040,7 +1040,7 @@ type 'a extra_genarg_printer =
   let strip_prod_binders_glob_constr n (ty,_) =
     let rec strip_ty acc n ty =
       if Int.equal n 0 then (List.rev acc, (ty,None)) else
-        match ty.CAst.v with
+        match DAst.get ty with
             Glob_term.GProd(na,Explicit,a,b) ->
               strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
           | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 0554d43641..fc6ee6aab6 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -106,12 +106,12 @@ let intern_ltac_variable ist = function
 
 let intern_constr_reference strict ist = function
   | Ident (_,id) as r when not strict && find_hyp id ist ->
-      (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
+      (DAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
   | Ident (_,id) as r when find_var id ist ->
-      (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
+      (DAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
-      CAst.make @@ GRef (locate_global_with_alias lqid,None), 
+      DAst.make @@ GRef (locate_global_with_alias lqid,None), 
 	if strict then None else Some (CAst.make @@ CRef (r,None))
 
 (* Internalize an isolated reference in position of tactic *)
@@ -264,9 +264,10 @@ let intern_destruction_arg ist = function
   | clear,ElimOnIdent (loc,id) ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-	match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with
-	| {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id)
-	| c -> clear,ElimOnConstr (c,NoBindings)
+	let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in
+	match DAst.get c with
+	| GVar id -> clear,ElimOnIdent (c.CAst.loc,id)
+	| _ -> clear,ElimOnConstr ((c, p), NoBindings)
       else
 	clear,ElimOnIdent (loc,id)
 
@@ -348,7 +349,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
         ltac_extra = ist.extra;
       } in
       let c = Constrintern.interp_reference sign r in
-      match c.CAst.v with
+      match DAst.get c with
       | GRef (r,None) ->
           Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
       | GVar id ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 2a1e2b6829..8fa95ffb02 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -679,8 +679,8 @@ let interp_typed_pattern ist env sigma (_,c,_) =
 (* Interprets a constr expression *)
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
   let try_expand_ltac_var sigma x =
-    try match dest_fun x with
-    | { CAst.v = GVar id }, _ ->
+    try match DAst.get (fst (dest_fun x)) with
+    | GVar id ->
       let v = Id.Map.find id ist.lfun in
       sigma, List.map inj_fun (coerce_to_constr_list env v)
     | _ ->
@@ -1043,7 +1043,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (loc,id)
 	else
-          let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
+          let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
           let f env sigma =
             let (sigma,c) = interp_open_constr ist env sigma c in
             (sigma, (c,NoBindings))