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, 43 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 63775d7373..7455587c0a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -94,7 +94,7 @@ let msg_may_need_inversion () =
 
 (* Utils *)
 let make_anonymous_patvars n =
-  List.make n (CAst.make @@ PatVar Anonymous)
+  List.make n (DAst.make @@ PatVar Anonymous)
 
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
@@ -177,7 +177,7 @@ and build_glob_pattern args = function
   | Top -> args
   | MakeConstructor (pci, rh) ->
       glob_pattern_of_partial_history
-	[CAst.make @@ PatCstr (pci, args, Anonymous)] rh
+	[DAst.make @@ PatCstr (pci, args, Anonymous)] rh
 
 let complete_history = glob_pattern_of_partial_history []
 
@@ -187,12 +187,12 @@ let pop_history_pattern = function
   | Continuation (0, l, Top) ->
       Result (List.rev l)
   | Continuation (0, l, MakeConstructor (pci, rh)) ->
-      feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh
+      feed_history (DAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh
   | _ ->
       anomaly (Pp.str "Constructor not yet filled with its arguments.")
 
 let pop_history h =
-  feed_history (CAst.make @@ PatVar Anonymous) h
+  feed_history (DAst.make @@ PatVar Anonymous) h
 
 (* Builds a continuation expecting [n] arguments and building [ci] applied
    to this [n] arguments *)
@@ -273,8 +273,10 @@ type 'a pattern_matching_problem =
 
 let rec find_row_ind = function
     [] -> None
-  | { CAst.v = PatVar _ } :: l -> find_row_ind l
-  | { CAst.v = PatCstr(c,_,_) ; loc } :: _ -> Some (loc,c)
+  | p :: l ->
+    match DAst.get p with
+    | PatVar _ -> find_row_ind l
+    | PatCstr(c,_,_) -> Some (p.CAst.loc,c)
 
 let inductive_template evdref env tmloc ind =
   let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in
@@ -348,7 +350,7 @@ let find_tomatch_tycon evdref env loc = function
       empty_tycon,None
 
 let make_return_predicate_ltac_lvar sigma na tm c lvar =
-  match na, tm.CAst.v with
+  match na, DAst.get tm with
   | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' ->
      if Id.Map.mem id lvar.ltac_genargs then
        let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in
@@ -447,7 +449,7 @@ let current_pattern eqn =
     | pat::_ -> pat
     | [] -> anomaly (Pp.str "Empty list of patterns.")
 
-let alias_of_pat = CAst.with_val (function
+let alias_of_pat = DAst.with_val (function
   | PatVar name -> name
   | PatCstr(_,_,name) -> name
   )
@@ -493,13 +495,14 @@ let rec adjust_local_defs ?loc = function
   | (pat :: pats, LocalAssum _ :: decls) ->
       pat :: adjust_local_defs ?loc (pats,decls)
   | (pats, LocalDef _ :: decls) ->
-      (CAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls)
+      (DAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls)
   | [], [] -> []
   | _ -> raise NotAdjustable
 
-let check_and_adjust_constructor env ind cstrs = function
-  | { CAst.v = PatVar _ } as pat -> pat
-  | { CAst.v = PatCstr (((_,i) as cstr),args,alias) ; loc } as pat ->
+let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with
+  | PatVar _ -> pat
+  | PatCstr (((_,i) as cstr),args,alias) ->
+      let loc = pat.CAst.loc in
       (* Check it is constructor of the right type *)
       let ind' = inductive_of_constructor cstr in
       if eq_ind ind' ind then
@@ -510,7 +513,7 @@ let check_and_adjust_constructor env ind cstrs = function
 	else
 	  try
 	    let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args)
-	    in CAst.make ?loc @@ PatCstr (cstr, args', alias)
+	    in DAst.make ?loc @@ PatCstr (cstr, args', alias)
 	  with NotAdjustable ->
 	    error_wrong_numarg_constructor ?loc env cstr nb_args_constr
       else
@@ -522,9 +525,12 @@ let check_and_adjust_constructor env ind cstrs = function
 
 let check_all_variables env sigma typ mat =
   List.iter
-    (fun eqn -> match current_pattern eqn with
-       | { CAst.v = PatVar id } -> ()
-       | { CAst.v = PatCstr (cstr_sp,_,_); loc } ->
+    (fun eqn ->
+      let pat = current_pattern eqn in
+      match DAst.get pat with
+       | PatVar id -> ()
+       | PatCstr (cstr_sp,_,_) ->
+          let loc = pat.CAst.loc in
 	   error_bad_pattern ?loc env sigma cstr_sp typ)
     mat
 
@@ -549,9 +555,9 @@ let occur_in_rhs na rhs =
     | Anonymous -> false
     | Name id -> Id.List.mem id rhs.rhs_vars
 
-let is_dep_patt_in eqn = function
-  | { CAst.v = PatVar name } -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
-  | { CAst.v = PatCstr _ } -> true
+let is_dep_patt_in eqn pat = match DAst.get pat with
+  | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
+  | PatCstr _ -> true
 
 let mk_dep_patt_row (pats,_,eqn) =
   List.map (is_dep_patt_in eqn) pats
@@ -771,7 +777,7 @@ let recover_and_adjust_alias_names names sign =
   | x::names, LocalAssum (_,t)::sign ->
       (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign)
   | names, (LocalDef (na,_,_) as decl)::sign ->
-      (CAst.make @@ PatVar na, decl) :: aux (names,sign)
+      (DAst.make @@ PatVar na, decl) :: aux (names,sign)
   | _ -> assert false
   in
   List.split (aux (names,sign))
@@ -987,7 +993,7 @@ let use_unit_judge evd =
     evd', j
 
 let add_assert_false_case pb tomatch =
-  let pats = List.map (fun _ -> CAst.make @@ PatVar Anonymous) tomatch in
+  let pats = List.map (fun _ -> DAst.make @@ PatVar Anonymous) tomatch in
   let aliasnames =
     List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch
   in
@@ -1184,9 +1190,9 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
 (************************************************************************)
 (* Sorting equations by constructor *)
 
-let rec irrefutable env = function
-  | { CAst.v = PatVar name } -> true
-  | { CAst.v = PatCstr (cstr,args,_) } ->
+let rec irrefutable env pat = match DAst.get pat with
+  | PatVar name -> true
+  | PatCstr (cstr,args,_) ->
       let ind = inductive_of_constructor cstr in
       let (_,mip) = Inductive.lookup_mind_specif env ind in
       let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in
@@ -1206,15 +1212,15 @@ let group_equations pb ind current cstrs mat =
       (fun eqn () ->
 	 let rest = remove_current_pattern eqn in
 	 let pat = current_pattern eqn in
-	 match check_and_adjust_constructor pb.env ind cstrs pat with
-	   | { CAst.v = PatVar name } ->
+	 match DAst.get (check_and_adjust_constructor pb.env ind cstrs pat) with
+	   | PatVar name ->
 	       (* This is a default clause that we expand *)
 	       for i=1 to Array.length cstrs do
 		 let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in
 		 brs.(i-1) <- (args, name, rest) :: brs.(i-1)
 	       done;
 	       if !only_default == None then only_default := Some true
-	   | { CAst.v = PatCstr (((_,i)),args,name) ; loc } ->
+	   | PatCstr (((_,i)),args,name) ->
 	       (* This is a regular clause *)
 	       only_default := Some false;
 	       brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in
@@ -1745,16 +1751,16 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
 let build_inversion_problem loc env sigma tms t =
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd env sigma t Anonymous) avoid in
-    CAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in
+    DAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
     match EConstr.kind sigma (whd_all env sigma t) with
-    | Construct (cstr,u) -> CAst.make (PatCstr (cstr,[],Anonymous)), acc
+    | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc
     | App (f,v) when isConstruct sigma f ->
 	let cstr,u = destConstruct sigma f in
 	let n = constructor_nrealargs_env env cstr in
 	let l = List.lastn n (Array.to_list v) in
 	let l,acc = List.fold_right_map reveal_pattern l acc in
-	CAst.make (PatCstr (cstr,l,Anonymous)), acc
+	DAst.make (PatCstr (cstr,l,Anonymous)), acc
     | _ -> make_patvar t acc in
   let rec aux n env acc_sign tms acc =
     match tms with
@@ -1830,7 +1836,7 @@ let build_inversion_problem loc env sigma tms t =
       (* No need for a catch all clause *)
       []
     else
-      [ { patterns = List.map (fun _ -> CAst.make @@ PatVar Anonymous) patl;
+      [ { patterns = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl;
           alias_stack = [];
           eqn_loc = None;
           used = ref false;
@@ -2094,14 +2100,14 @@ let mk_JMeq evdref typ x typ' y =
 let mk_JMeq_refl evdref typ x = 
   papp evdref coq_JMeq_refl [| typ; x |]
 
-let hole na = CAst.make @@
+let hole na = DAst.make @@
   GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
          Misctypes.IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
     let loc = pat.CAst.loc in
-    match pat.CAst.v with
+    match DAst.get pat with
     | PatVar name ->
 	let name, avoid = match name with
 	    Name n -> name, avoid
@@ -2109,7 +2115,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	      let previd, id = prime avoid (Name (Id.of_string "wildcard")) in
 		Name id, id :: avoid
 	in
-	  ((CAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
+	  ((DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
 	   (List.map (fun x -> mkRel 1) realargs), 1, avoid)
     | PatCstr (((_, i) as cstr),args,alias) ->
 	let cind = inductive_of_constructor cstr in
@@ -2140,7 +2146,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	in
 	let args = List.rev args in
 	let patargs = List.rev patargs in
-	let pat' = CAst.make ?loc @@ PatCstr (cstr, patargs, alias) in
+	let pat' = DAst.make ?loc @@ PatCstr (cstr, patargs, alias) in
 	let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in
 	let app = applist (cstr, List.map (lift (List.length sign)) params) in
 	let app = applist (app, args) in
@@ -2196,18 +2202,18 @@ let vars_of_ctx sigma ctx =
       match decl with
 	| LocalDef (na,t',t) when is_topvar sigma t' ->
 	    prev,
-	    (CAst.make @@ GApp (
-		(CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), 
-		   [hole na; CAst.make @@ GVar prev])) :: vars
+	    (DAst.make @@ GApp (
+		(DAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), 
+		   [hole na; DAst.make @@ GVar prev])) :: vars
 	| _ ->
 	    match RelDecl.get_name decl with
 		Anonymous -> invalid_arg "vars_of_ctx"
-	      | Name n -> n, (CAst.make @@ GVar n) :: vars)
+	      | Name n -> n, (DAst.make @@ GVar n) :: vars)
       ctx (Id.of_string "vars_of_ctx_error", [])
   in List.rev y
 
 let rec is_included x y =
-  match CAst.(x.v, y.v) with
+  match DAst.get x, DAst.get y with
     | PatVar _, _ -> true
     | _, PatVar _ -> true
     | PatCstr ((_, i), args, alias), PatCstr ((_, i'), args', alias')  ->
@@ -2325,13 +2331,13 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in
 	 let branch =
-	   let bref = CAst.make @@ GVar branch_name in
+	   let bref = DAst.make @@ GVar branch_name in
 	     match vars_of_ctx !evdref rhs_rels with
 		 [] -> bref
-	       | l  -> CAst.make @@ GApp (bref, l)
+	       | l  -> DAst.make @@ GApp (bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ])
+	     Some _ -> DAst.make @@ GApp (branch, [ hole Anonymous ])
 	   | None -> branch
 	 in
 	 incr i;