Abstract away the name generation algorithm in Detyping.

For now it does not change anything, but it will make the move towards a
faster algorithm seamless.

1 files changed, 85 insertions, 53 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index fa23f7140e..e4f7295b59 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -34,6 +34,42 @@ type detyping_flags = {
   flg_isgoal : bool;
 }
 
+module Avoid :
+sig
+  type t
+  val make : Id.Set.t -> t
+  val compute_name : Evd.evar_map -> let_in:bool -> pattern:bool ->
+    detyping_flags -> t -> Name.t list * 'a -> Name.t ->
+    EConstr.constr -> Name.t * t
+  val next_name_away : detyping_flags -> Name.t -> t -> Id.t * t
+end =
+struct
+
+type t = { ids : Id.Set.t }
+let make ids = { ids = ids }
+let add id ids = { ids = Id.Set.add id ids.ids }
+
+let compute_name sigma ~let_in ~pattern flags avoid env na c =
+  let flags =
+    if flags.flg_isgoal then RenamingForGoal
+    else if pattern then RenamingForCasesPattern (fst env, c)
+    else RenamingElsewhereFor (fst env, c)
+  in
+  let na, avoid =
+    if let_in then compute_displayed_let_name_in sigma flags avoid.ids na c
+    else compute_displayed_name_in sigma flags avoid.ids na c
+  in
+  na, make avoid
+
+let next_name_away flags na avoid =
+  let id = next_name_away na avoid.ids in
+  id, add id avoid
+
+end
+
+let compute_name = Avoid.compute_name
+let next_name_away = Avoid.next_name_away
+
 type _ delay =
 | Now : 'a delay
 | Later : [ `thunk ] delay
@@ -215,7 +251,7 @@ let lookup_name_as_displayed env sigma t s =
            | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
 	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | LetIn (name,_,_,c') ->
-        (match compute_displayed_name_in sigma RenamingForGoal avoid name.binder_name c' with
+        (match Namegen.compute_displayed_name_in sigma RenamingForGoal avoid name.binder_name c' with
            | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
 	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | Cast (c,_,_) -> lookup avoid n c
@@ -225,7 +261,7 @@ let lookup_name_as_displayed env sigma t s =
 let lookup_index_as_renamed env sigma t n =
   let rec lookup n d c = match EConstr.kind sigma c with
     | Prod (name,_,c') ->
-          (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name.binder_name c' with
+          (match Namegen.compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name.binder_name c' with
                (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if Int.equal n 0 then
@@ -235,7 +271,7 @@ let lookup_index_as_renamed env sigma t n =
 		 else
 		   lookup (n-1) (d+1) c')
     | LetIn (name,_,_,c') ->
-          (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name.binder_name c' with
+          (match Namegen.compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name.binder_name c' with
              | (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if Int.equal n 0 then
@@ -345,22 +381,21 @@ let update_name sigma na ((_,(e,_)),c) =
       na
 
 let rec decomp_branch tags nal flags (avoid,env as e) sigma c =
-  let flag = if flags.flg_isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,c) in
   match tags with
   | [] -> (List.rev nal,(e,c))
   | b::tags ->
-      let na,c,f,body,t =
+      let na,c,let_in,body,t =
         match EConstr.kind sigma (strip_outer_cast sigma c), b with
-        | Lambda (na,t,c),false -> na.binder_name,c,compute_displayed_let_name_in,None,Some t
+        | Lambda (na,t,c),false -> na.binder_name,c,true,None,Some t
         | LetIn (na,b,t,c),true ->
-            na.binder_name,c,compute_displayed_name_in,Some b,Some t
+            na.binder_name,c,false,Some b,Some t
 	| _, false ->
 	  Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])),
-	    compute_displayed_name_in,None,None
+            false,None,None
 	| _, true ->
-	  Anonymous,lift 1 c,compute_displayed_name_in,None,None
+          Anonymous,lift 1 c,false,None,None
     in
-    let na',avoid' = f sigma flag avoid na c in
+    let na',avoid' = compute_name sigma ~let_in ~pattern:true flags avoid env na c in
     decomp_branch tags (na'::nal) flags
       (avoid', add_name_opt na' body t env) sigma c
 
@@ -495,37 +530,37 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       let eqnl = detype_eqns constructs constagsl bl in
       GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
-let rec share_names detype n l avoid env sigma c t =
+let rec share_names detype flags n l avoid env sigma c t =
   match EConstr.kind sigma c, EConstr.kind sigma t with
     (* factorize even when not necessary to have better presentation *)
     | Lambda (na,t,c), Prod (na',t',c') ->
         let na = Nameops.Name.pick_annot na na' in
-        let t' = detype avoid env sigma t in
-        let id = next_name_away na.binder_name avoid in
-        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
-        share_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+        let t' = detype flags avoid env sigma t in
+        let id, avoid = next_name_away flags na.binder_name avoid in
+        let env = add_name (Name id) None t env in
+        share_names detype flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
     (* May occur for fix built interactively *)
     | LetIn (na,b,t',c), _ when n > 0 ->
-        let t'' = detype avoid env sigma t' in
-        let b' = detype avoid env sigma b in
-        let id = next_name_away na.binder_name avoid in
-        let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
-        share_names detype n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
+        let t'' = detype flags avoid env sigma t' in
+        let b' = detype flags avoid env sigma b in
+        let id, avoid = next_name_away flags na.binder_name avoid in
+        let env = add_name (Name id) (Some b) t' env in
+        share_names detype flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
     (* Only if built with the f/n notation or w/o let-expansion in types *)
     | _, LetIn (_,b,_,t) when n > 0 ->
-        share_names detype n l avoid env sigma c (subst1 b t)
+        share_names detype flags n l avoid env sigma c (subst1 b t)
     (* If it is an open proof: we cheat and eta-expand *)
     | _, Prod (na',t',c') when n > 0 ->
-        let t'' = detype avoid env sigma t' in
-        let id = next_name_away na'.binder_name avoid in
-        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
+        let t'' = detype flags avoid env sigma t' in
+        let id, avoid = next_name_away flags na'.binder_name avoid in
+        let env = add_name (Name id) None t' env in
         let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-        share_names detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
+        share_names detype flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
         if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
-        let c = detype avoid env sigma c in
-        let t = detype avoid env sigma t in
+        let c = detype flags avoid env sigma c in
+        let t = detype flags avoid env sigma t in
         (List.rev l,c,t)
 
 let rec share_pattern_names detype n l avoid env sigma c t =
@@ -541,7 +576,7 @@ let rec share_pattern_names detype n l avoid env sigma c t =
           | _, Name _ -> na'
           | _ -> na in
         let t' = detype avoid env sigma t in
-        let id = next_name_away na avoid in
+        let id = Namegen.next_name_away na avoid in
         let avoid = Id.Set.add id avoid in
         let env = Name id :: env in
         share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
@@ -551,32 +586,32 @@ let rec share_pattern_names detype n l avoid env sigma c t =
         let t = detype avoid env sigma t in
         (List.rev l,c,t)
 
-let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
+let detype_fix detype flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
   let def_avoid, def_env, lfi =
     Array.fold_left2
       (fun (avoid, env, l) na ty ->
-         let id = next_name_away na.binder_name avoid in
-         (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
+         let id, avoid = next_name_away flags na.binder_name avoid in
+         (avoid, add_name (Name id) None ty env, id::l))
       (avoid, env, []) names tys in
   let n = Array.length tys in
   let v = Array.map3
-    (fun c t i -> share_names detype (i+1) [] def_avoid def_env sigma c (lift n t))
+    (fun c t i -> share_names detype flags (i+1) [] def_avoid def_env sigma c (lift n t))
     bodies tys vn in
   GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-let detype_cofix detype avoid env sigma n (names,tys,bodies) =
+let detype_cofix detype flags avoid env sigma n (names,tys,bodies) =
   let def_avoid, def_env, lfi =
     Array.fold_left2
       (fun (avoid, env, l) na ty ->
-         let id = next_name_away na.binder_name avoid in
-         (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
+         let id, avoid = next_name_away flags na.binder_name avoid in
+         (avoid, add_name (Name id) None ty env, id::l))
       (avoid, env, []) names tys in
   let ntys = Array.length tys in
   let v = Array.map2
-    (fun c t -> share_names detype 0 [] def_avoid def_env sigma c (lift ntys t))
+    (fun c t -> share_names detype flags 0 [] def_avoid def_env sigma c (lift ntys t))
     bodies tys in
   GRec(GCoFix n,Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
@@ -741,8 +776,8 @@ and detype_r d flags avoid env sigma t =
 	  (ci.ci_ind,ci.ci_pp_info.style,
 	   ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
           p c bl
-    | Fix (nvn,recdef) -> detype_fix (detype d flags) avoid env sigma nvn recdef
-    | CoFix (n,recdef) -> detype_cofix (detype d flags) avoid env sigma n recdef
+    | Fix (nvn,recdef) -> detype_fix (detype d) flags avoid env sigma nvn recdef
+    | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef
     | Int i -> GInt i
 
 and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
@@ -761,8 +796,7 @@ and detype_eqn d flags avoid env sigma constr construct_nargs branch =
     if force_wildcard () && noccurn sigma 1 b then
       DAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids
     else
-      let flag = if flags.flg_isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in
-      let na,avoid' = compute_displayed_name_in sigma flag avoid x b in
+      let na,avoid' = compute_name sigma ~let_in:false ~pattern:true flags avoid env x b in
       DAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na
   in
   let rec buildrec ids patlist avoid env l b =
@@ -799,10 +833,9 @@ and detype_eqn d flags avoid env sigma constr construct_nargs branch =
   buildrec Id.Set.empty [] avoid env construct_nargs branch
 
 and detype_binder d flags bk avoid env sigma {binder_name=na} body ty c =
-  let flag = if flags.flg_isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in
   let na',avoid' = match bk with
-  | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c
-  | _ -> compute_displayed_name_in sigma flag avoid na c in
+  | BLetIn -> compute_name sigma ~let_in:true ~pattern:false flags avoid env na c
+  | _ -> compute_name sigma ~let_in:false ~pattern:false flags avoid env na c in
   let r =  detype d flags avoid' (add_name na' body ty env) sigma c in
   match bk with
   | BProd   -> GProd (na',Explicit,detype d { flags with flg_isgoal = false } avoid env sigma ty, r)
@@ -814,8 +847,7 @@ and detype_binder d flags bk avoid env sigma {binder_name=na} body ty c =
       let t = if s != InProp  && not !Flags.raw_print then None else Some (detype d { flags with flg_isgoal = false } avoid env sigma ty) in
       GLetIn (na', c, t, r)
 
-let detype_rel_context d ?(lax=false) where avoid env sigma sign =
-  let flags = { flg_isgoal = false; flg_lax = lax } in
+let detype_rel_context d flags where avoid env sigma sign =
   let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in
   let rec aux avoid env = function
   | [] -> []
@@ -827,12 +859,8 @@ let detype_rel_context d ?(lax=false) where avoid env sigma sign =
 	match where with
 	| None -> na,avoid
 	| Some c ->
-	    if is_local_def decl then
-	      compute_displayed_let_name_in sigma
-                (RenamingElsewhereFor (fst env,c)) avoid na c
-	    else
-	      compute_displayed_name_in sigma
-                (RenamingElsewhereFor (fst env,c)) avoid na c in
+          compute_name sigma ~let_in:(is_local_def decl) ~pattern:false flags avoid env na c
+      in
       let b = match decl with
 	      | LocalAssum _ -> None
               | LocalDef (_,b,_) -> Some b
@@ -844,13 +872,17 @@ let detype_rel_context d ?(lax=false) where avoid env sigma sign =
 
 let detype_names isgoal avoid nenv env sigma t = 
   let flags = { flg_isgoal = isgoal; flg_lax = false } in
+  let avoid = Avoid.make avoid in
   detype Now flags avoid (nenv,env) sigma t
 let detype d ?(lax=false) isgoal avoid env sigma t =
   let flags = { flg_isgoal = isgoal; flg_lax = lax } in
+  let avoid = Avoid.make avoid in
   detype d flags avoid (names_of_rel_context env, env) sigma t
 
-let detype_rel_context d ?lax where avoid env sigma sign =
-  detype_rel_context d ?lax where avoid env sigma sign
+let detype_rel_context d ?(lax = false) where avoid env sigma sign =
+  let flags = { flg_isgoal = false; flg_lax = lax } in
+  let avoid = Avoid.make avoid in
+  detype_rel_context d flags where avoid env sigma sign
 
 let detype_closed_glob ?lax isgoal avoid env sigma t =
   let open Context.Rel.Declaration in