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, 61 insertions, 45 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8cf5e8442..7087a195e 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -34,10 +34,10 @@ type glob_context = (binder_type*glob_constr) list
 
 
 let rec solve_trivial_holes pat_as_term e =
-  match pat_as_term.CAst.v,e.CAst.v with
+  match DAst.get pat_as_term, DAst.get e with
   | GHole _,_ -> e
   | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe ->
-       CAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse))
+       DAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse))
   | _,_ -> pat_as_term
                                               
 (*
@@ -361,7 +361,7 @@ let add_pat_variables pat typ env : Environ.env =
   let rec add_pat_variables env pat typ  : Environ.env =
     observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
 
-    match pat.CAst.v with
+    match DAst.get pat with
       | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
       | PatCstr(c,patl,na) ->
 	  let Inductiveops.IndType(indf,indargs) =
@@ -411,7 +411,7 @@ let add_pat_variables pat typ env : Environ.env =
 
 
 
-let rec pattern_to_term_and_type env typ  = CAst.with_val (function
+let rec pattern_to_term_and_type env typ  = DAst.with_val (function
   | PatVar Anonymous -> assert false
   | PatVar (Name id) ->
 	mkGVar id
@@ -434,7 +434,7 @@ let rec pattern_to_term_and_type env typ  = CAst.with_val (function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype false [] env (Evd.from_env env) (EConstr.of_constr csta.(i)))
+	     (fun i -> Detyping.detype Detyping.Now false [] env (Evd.from_env env) (EConstr.of_constr csta.(i)))
 	  )
       in
       let patl_as_term =
@@ -480,7 +480,7 @@ let rec pattern_to_term_and_type env typ  = CAst.with_val (function
 let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
   observe (str " Entering : " ++ Printer.pr_glob_constr rt);
   let open CAst in
-  match rt.v with
+  match DAst.get rt with
     | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ ->
 	(* do nothing (except changing type of course) *)
 	mk_result [] rt avoid
@@ -496,13 +496,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	    (mk_result [] [] avoid)
 	in
 	begin
-	  match f.v with
+	  match DAst.get f with
 	    | GLambda _  -> 
 		let rec aux t l = 
 		  match l with 
 		    | [] -> t
-		    | u::l -> CAst.make @@
-			match t.v with 
+		    | u::l -> DAst.make @@
+			match DAst.get t with 
 			  | GLambda(na,_,nat,b) -> 
 			      GLetIn(na,u,None,aux b l)
 			  | _ -> 
@@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
 		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
-		let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
+		let res_raw_type = Detyping.detype Detyping.Now false [] env (Evd.from_env env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
 		let res_rt = mkGVar res in
@@ -564,7 +564,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 			let new_b =
 			  replace_var_by_term
 			    id
-			    (CAst.make @@ GVar id)
+			    (DAst.make @@ GVar id)
 			    b
 			in
 			(Name new_id,new_b,new_avoid)
@@ -626,7 +626,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	   then the one corresponding to the value [t]
 	   and combine the two result
 	*)
-        let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
+        let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
 	let v_res = build_entry_lc env funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
 	let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
@@ -773,7 +773,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
 			in
 			let raw_typ_of_id =
-			  Detyping.detype false []
+			  Detyping.detype Detyping.Now false []
 			    env_with_pat_ids (Evd.from_env env) typ_of_id
 			in
 			mkGProd (Name id,raw_typ_of_id,acc))
@@ -819,7 +819,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
 		 let typ_as_constr = EConstr.of_constr typ_as_constr in
-		 let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in
+		 let typ = Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
                  (* removing trivial holes *) 
                  let pat_as_term = solve_trivial_holes pat_as_term e in 
@@ -833,7 +833,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
 		      let raw_typ_of_id =
-			Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
+			Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_of_id
 		      in
 		      raw_typ_of_id
 			   )::acc
@@ -875,15 +875,23 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	{ brl'_res with result = this_branch_res@brl'_res.result }
 
 
-let is_res id =
-  try
+let is_res r = match DAst.get r with
+| GVar id ->
+  begin try
     String.equal (String.sub (Id.to_string id) 0 4) "_res"
-  with Invalid_argument _ -> false
+  with Invalid_argument _ -> false end
+| _ -> false
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
 
+let is_gvar c = match DAst.get c with
+| GVar id -> true
+| _ -> false
 
 let same_raw_term rt1 rt2 = 
-  match CAst.(rt1.v, rt2.v) with 
+  match DAst.get rt1, DAst.get rt2 with 
     | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2
     | GHole _, GHole _ -> true
     | _ -> false
@@ -917,23 +925,24 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
   observe (str "rebuilding : " ++ pr_glob_constr rt);
   let open Context.Rel.Declaration in
   let open CAst in
-  match rt.v with
+  match DAst.get rt with
     | GProd(n,k,t,b) ->
 	let not_free_in_t id = not (is_free_in id t) in
 	let new_crossed_types = t::crossed_types in
 	begin
-	  match t with
-	    | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id ->
+	  match DAst.get t with
+	    | GApp(res_rt ,args') when is_res res_rt ->
 		begin
-		  match args' with
-		    | { v = GVar this_relname }::args' ->
+                  let arg = List.hd args' in
+		  match DAst.get arg with
+		    | GVar this_relname ->
 			(*i The next call to mk_rel_id is
 			  valid since we are constructing the graph
 			  Ensures by: obvious
 			  i*)
 
 			let new_t =
-			  mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
+			  mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt])
 			in
 			let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
 			let new_env = Environ.push_rel (LocalAssum (n,t')) env in
@@ -948,9 +957,13 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    | _ -> (* the first args is the name of the function! *)
 			assert false
 		end
-	    | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) }
-		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
+	    | GApp(eq_as_ref,[ty; id ;rt])
+		when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
 		  ->
+                let loc1 = rt.CAst.loc in
+                let loc2 = eq_as_ref.CAst.loc in
+                let loc3 = id.CAst.loc in
+                let id = match DAst.get id with GVar id -> id | _ -> assert false in
 		begin
 		  try
 		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
@@ -985,10 +998,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let params,arg' =
 		      ((Util.List.chop nparam args'))
 		    in
-		    let rt_typ = CAst.make @@
-		       GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None),
+		    let rt_typ = DAst.make @@
+		       GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None),
 			    (List.map
-			      (fun p -> Detyping.detype false []
+			      (fun p -> Detyping.detype Detyping.Now false []
 				 env (Evd.from_env env)
 				 (EConstr.of_constr p)) params)@(Array.to_list
 				      (Array.make
@@ -996,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 					 (mkGHole ()))))
 		    in
 		    let eq' =
-		      CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
+		      DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
 		    in
 		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
 		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
@@ -1015,12 +1028,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 				   match na with
 				     | Anonymous -> acc
 				     | Name id' ->
-					 (id',Detyping.detype false []
+					 (id',Detyping.detype Detyping.Now false []
 					    env
                                             (Evd.from_env env)
 					    arg)::acc
 				 else if isVar var_as_constr
-				 then (destVar var_as_constr,Detyping.detype false []
+				 then (destVar var_as_constr,Detyping.detype Detyping.Now false []
 					 env
                                          (Evd.from_env env)
 					 arg)::acc
@@ -1065,8 +1078,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     mkGProd(n,t,new_b),id_to_exclude
 		     else new_b, Id.Set.add id id_to_exclude
 		  *)
-	    | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) }
-		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
+	    | GApp(eq_as_ref,[ty;rt1;rt2])
+		when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
 		  ->
 	      begin
 		try 
@@ -1077,7 +1090,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      List.fold_left 
 			(fun acc (lhs,rhs) -> 
 			  mkGProd(Anonymous,
-				  mkGApp(mkGRef(eq_as_ref),[mkGHole ();lhs;rhs]),acc)
+				  mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc)
 			)
 			b
 			l
@@ -1135,14 +1148,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		then
 		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 		else
-		  CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
+		  DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	    | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
 	end
     | GLetIn(n,v,t,b) ->
 	begin
-          let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
+          let t = match t with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let evd = (Evd.from_env env) in
 	  let t',ctx = Pretyping.understand env evd t in
@@ -1158,7 +1171,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  match n with
 	    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
-	    | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
+	    | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
 		Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLetTuple(nal,(na,rto),t,b) ->
@@ -1184,7 +1197,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 (* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
 (* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
 (* 	    | _ -> *)
-	  CAst.make @@ GLetTuple(nal,(na,None),t,new_b),
+	  DAst.make @@ GLetTuple(nal,(na,None),t,new_b),
 		Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
 
 	end
@@ -1210,12 +1223,15 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 
    TODO: Find a valid way to deal with implicit arguments here!
 *)
-let rec compute_cst_params relnames params gt = CAst.with_val (function
+let rec compute_cst_params relnames params gt = DAst.with_val (function
   | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
-  | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames ->
-      compute_cst_params_from_app [] (params,rtl)
   | GApp(f,args) ->
+    begin match DAst.get f with
+    | GVar relname' when Id.Set.mem relname' relnames ->
+      compute_cst_params_from_app [] (params,args)
+    | _ ->
       List.fold_left (compute_cst_params relnames) params (f::args)
+    end
   | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) ->
       let t_params = compute_cst_params relnames params t in
       compute_cst_params relnames t_params b
@@ -1232,10 +1248,10 @@ let rec compute_cst_params relnames params gt = CAst.with_val (function
       raise (UserError(Some "compute_cst_params", str "Not handled case"))
   ) gt
 and compute_cst_params_from_app acc (params,rtl) =
+  let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
-    | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl'
-	when Id.compare id id' == 0 ->
+    | ((Name id,_,None) as param)::params', c::rtl' when is_gid id c ->
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc