diff options
Diffstat (limited to 'engine/namegen.ml')
| -rw-r--r-- | engine/namegen.ml | 286 |
1 files changed, 167 insertions, 119 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index 84eb9868..d66b77b5 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created from contents that was formerly in termops.ml and @@ -15,15 +17,17 @@ open Util open Names open Term +open Environ +open EConstr open Vars open Nametab open Nameops open Libnames open Globnames -open Environ -open Termops open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (**********************************************************************) (* Conventional names *) @@ -41,6 +45,8 @@ let default_non_dependent_ident = Id.of_string default_non_dependent_string let default_dependent_ident = Id.of_string "x" +let default_generated_non_letter_string = "x" + (**********************************************************************) (* Globality of identifiers *) @@ -57,9 +63,9 @@ let is_imported_ref = function | VarRef _ -> false | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - let (mp,_,_) = repr_mind kn in is_imported_modpath mp + let (mp,_,_) = MutInd.repr3 kn in is_imported_modpath mp | ConstRef kn -> - let (mp,_,_) = repr_con kn in is_imported_modpath mp + let (mp,_,_) = Constant.repr3 kn in is_imported_modpath mp let is_global id = try @@ -76,16 +82,27 @@ let is_constructor id = with Not_found -> false +let is_section_variable id = + try let _ = Global.lookup_named id in true + with Not_found -> false + (**********************************************************************) (* Generating "intuitive" names from its type *) -let head_name c = (* Find the head constant of a constr if any *) +let global_of_constr = function +| Const (c, _) -> ConstRef c +| Ind (i, _) -> IndRef i +| Construct (c, _) -> ConstructRef c +| Var id -> VarRef id +| _ -> assert false + +let head_name sigma c = (* Find the head constant of a constr if any *) let rec hdrec c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) | Cast (c,_,_) | App (c,_) -> hdrec c - | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn))) - | Const _ | Ind _ | Construct _ | Var _ -> + | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn))) + | Const _ | Ind _ | Construct _ | Var _ as c -> Some (basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i) with Name id -> id | _ -> assert false) @@ -94,29 +111,39 @@ let head_name c = (* Find the head constant of a constr if any *) hdrec c let lowercase_first_char id = (* First character of a constr *) - Unicode.lowercase_first_char (Id.to_string id) + let s = Id.to_string id in + match Unicode.split_at_first_letter s with + | None -> + (* General case: nat -> n *) + Unicode.lowercase_first_char s + | Some (s,s') -> + if String.length s' = 0 then + (* No letter, e.g. __, or __'_, etc. *) + default_generated_non_letter_string + else + s ^ Unicode.lowercase_first_char s' let sort_hdchar = function | Prop(_) -> "P" | Type(_) -> "T" -let hdchar env c = +let hdchar env sigma c = let rec hdrec k c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c | Cast (c,_,_) | App (c,_) -> hdrec k c - | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn))) - | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn)) - | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x)) - | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x)) + | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn))) + | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn)) + | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") | Var id -> lowercase_first_char id - | Sort s -> sort_hdchar s + | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else - try match Environ.lookup_rel (n-k) env |> to_tuple with - | (Name id,_,_) -> lowercase_first_char id - | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) + try match lookup_rel (n-k) env with + | LocalAssum (Name id,_) | LocalDef (Name id,_,_) -> lowercase_first_char id + | LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) with Not_found -> "y") | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> let id = match lna.(i) with Name id -> id | _ -> assert false in @@ -126,49 +153,85 @@ let hdchar env c = in hdrec 0 c -let id_of_name_using_hdchar env a = function - | Anonymous -> Id.of_string (hdchar env a) +let id_of_name_using_hdchar env sigma a = function + | Anonymous -> Id.of_string (hdchar env sigma a) | Name id -> id -let named_hd env a = function - | Anonymous -> Name (Id.of_string (hdchar env a)) +let named_hd env sigma a = function + | Anonymous -> Name (Id.of_string (hdchar env sigma a)) | x -> x -let mkProd_name env (n,a,b) = mkProd (named_hd env a n, a, b) -let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b) +let mkProd_name env sigma (n,a,b) = mkProd (named_hd env sigma a n, a, b) +let mkLambda_name env sigma (n,a,b) = mkLambda (named_hd env sigma a n, a, b) let lambda_name = mkLambda_name let prod_name = mkProd_name -let prod_create env (a,b) = mkProd (named_hd env a Anonymous, a, b) -let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous, a, b) +let prod_create env sigma (a,b) = mkProd (named_hd env sigma a Anonymous, a, b) +let lambda_create env sigma (a,b) = mkLambda (named_hd env sigma a Anonymous, a, b) -let name_assumption env = function - | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) - | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) +let name_assumption env sigma = function + | LocalAssum (na,t) -> LocalAssum (named_hd env sigma t na, t) + | LocalDef (na,c,t) -> LocalDef (named_hd env sigma c na, c, t) -let name_context env hyps = +let name_context env sigma hyps = snd (List.fold_left (fun (env,hyps) d -> - let d' = name_assumption env d in (push_rel d' env, d' :: hyps)) + let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps)) (env,[]) (List.rev hyps)) -let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b -let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b +let mkProd_or_LetIn_name env sigma b d = mkProd_or_LetIn (name_assumption env sigma d) b +let mkLambda_or_LetIn_name env sigma b d = mkLambda_or_LetIn (name_assumption env sigma d) b -let it_mkProd_or_LetIn_name env b hyps = - it_mkProd_or_LetIn b (name_context env hyps) -let it_mkLambda_or_LetIn_name env b hyps = - it_mkLambda_or_LetIn b (name_context env hyps) +let it_mkProd_or_LetIn_name env sigma b hyps = + it_mkProd_or_LetIn b (name_context env sigma hyps) +let it_mkLambda_or_LetIn_name env sigma b hyps = + it_mkLambda_or_LetIn b (name_context env sigma hyps) (**********************************************************************) (* Fresh names *) +(* Introduce a mode where auto-generated names are mangled + to test dependence of scripts on auto-generated names *) + +let mangle_names = ref false + +let _ = Goptions.( + declare_bool_option + { optdepr = false; + optname = "mangle auto-generated names"; + optkey = ["Mangle";"Names"]; + optread = (fun () -> !mangle_names); + optwrite = (:=) mangle_names; }) + +let mangle_names_prefix = ref (Id.of_string "_0") +let set_prefix x = mangle_names_prefix := forget_subscript x + +let set_mangle_names_mode x = begin + set_prefix x; + mangle_names := true + end + +let _ = Goptions.( + declare_string_option + { optdepr = false; + optname = "mangled names prefix"; + optkey = ["Mangle";"Names";"Prefix"]; + optread = (fun () -> Id.to_string !mangle_names_prefix); + optwrite = begin fun x -> + set_prefix + (try Id.of_string x + with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) + end }) + +let mangle_id id = if !mangle_names then !mangle_names_prefix else id + (* Looks for next "good" name by lifting subscript *) let next_ident_away_from id bad = - let rec name_rec id = if bad id then name_rec (lift_subscript id) else id in + let id = mangle_id id in + let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in name_rec id (* Restart subscript from x0 if name starts with xN, or x00 if name @@ -180,14 +243,10 @@ let restart_subscript id = *** make_ident id (Some 0) *** but compatibility would be lost... *) forget_subscript id -let rec to_avoid id = function -| [] -> false -| id' :: avoid -> Id.equal id id' || to_avoid id avoid - -let visible_ids (nenv, c) = +let visible_ids sigma (nenv, c) = let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in - let rec visible_ids n c = match kind_of_term c with - | Const _ | Ind _ | Construct _ | Var _ -> + let rec visible_ids n c = match EConstr.kind sigma c with + | Const _ | Ind _ | Construct _ | Var _ as c -> let (gseen, vseen, ids) = !accu in let g = global_of_constr c in if not (Refset_env.mem g gseen) then @@ -205,8 +264,8 @@ let visible_ids (nenv, c) = if p > n && not (Int.Set.mem p vseen) then let vseen = Int.Set.add p vseen in let name = - try Some (lookup_name_of_rel (p - n) nenv) - with Not_found -> + try Some (List.nth nenv (p - n - 1)) + with Invalid_argument _ | Failure _ -> (* Unbound index: may happen in debug and actually also while computing temporary implicit arguments of an inductive type *) @@ -217,7 +276,7 @@ let visible_ids (nenv, c) = | _ -> ids in accu := (gseen, vseen, ids) - | _ -> Constr.iter_with_binders succ visible_ids n c + | _ -> EConstr.iter_with_binders sigma succ visible_ids n c in let () = visible_ids 1 c in let (_, _, ids) = !accu in @@ -227,11 +286,11 @@ let visible_ids (nenv, c) = (* 1- Looks for a fresh name for printing in cases pattern *) -let next_name_away_in_cases_pattern env_t na avoid = +let next_name_away_in_cases_pattern sigma env_t na avoid = let id = match na with Name id -> id | Anonymous -> default_dependent_ident in - let visible = visible_ids env_t in - let bad id = to_avoid id avoid || is_constructor id - || Id.Set.mem id visible in + let visible = visible_ids sigma env_t in + let bad id = Id.Set.mem id avoid || is_constructor id + || Id.Set.mem id visible in next_ident_away_from id bad (* 2- Looks for a fresh name for introduction in goal *) @@ -244,8 +303,8 @@ let next_name_away_in_cases_pattern env_t na avoid = name is taken by finding a free subscript starting from 0 *) let next_ident_away_in_goal id avoid = - let id = if to_avoid id avoid then restart_subscript id else id in - let bad id = to_avoid id avoid || (is_global id && not (is_section_variable id)) in + let id = if Id.Set.mem id avoid then restart_subscript id else id in + let bad id = Id.Set.mem id avoid || (is_global id && not (is_section_variable id)) in next_ident_away_from id bad let next_name_away_in_goal na avoid = @@ -262,16 +321,17 @@ let next_name_away_in_goal na avoid = beyond the current subscript *) let next_global_ident_away id avoid = - let id = if to_avoid id avoid then restart_subscript id else id in - let bad id = to_avoid id avoid || is_global id in + let id = if Id.Set.mem id avoid then restart_subscript id else id in + let bad id = Id.Set.mem id avoid || is_global id in next_ident_away_from id bad (* 4- Looks for next fresh name outside a list; if name already used, looks for same name with lower available subscript *) let next_ident_away id avoid = - if to_avoid id avoid then - next_ident_away_from (restart_subscript id) (fun id -> to_avoid id avoid) + let id = mangle_id id in + if Id.Set.mem id avoid then + next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid) else id let next_name_away_with_default default na avoid = @@ -291,28 +351,31 @@ let next_name_away_with_default_using_types default na avoid t = let next_name_away = next_name_away_with_default default_non_dependent_string -let make_all_name_different env = - let avoid = ref (ids_of_named_context (named_context env)) in - process_rel_context +let make_all_name_different env sigma = + (** FIXME: this is inefficient, but only used in printing *) + let avoid = ref (ids_of_named_context_val (named_context_val env)) in + let sign = named_context_val env in + let rels = rel_context env in + let env0 = reset_with_named_context sign env in + Context.Rel.fold_outside (fun decl newenv -> - let (na,_,t) = to_tuple decl in - let na = named_hd newenv t na in + let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in - avoid := id::!avoid; - push_rel (set_name (Name id) decl) newenv) - env + avoid := Id.Set.add id !avoid; + push_rel (RelDecl.set_name (Name id) decl) newenv) + rels ~init:env0 (* 5- Looks for next fresh name outside a list; avoids also to use names that would clash with short name of global references; if name is already used, looks for name of same base with lower available subscript beyond current subscript *) -let next_ident_away_for_default_printing env_t id avoid = - let visible = visible_ids env_t in - let bad id = to_avoid id avoid || Id.Set.mem id visible in +let next_ident_away_for_default_printing sigma env_t id avoid = + let visible = visible_ids sigma env_t in + let bad id = Id.Set.mem id avoid || Id.Set.mem id visible in next_ident_away_from id bad -let next_name_away_for_default_printing env_t na avoid = +let next_name_away_for_default_printing sigma env_t na avoid = let id = match na with | Name id -> id | Anonymous -> @@ -320,7 +383,7 @@ let next_name_away_for_default_printing env_t na avoid = (* taken into account by the function compute_displayed_name_in; *) (* just in case, invent a valid name *) default_non_dependent_ident in - next_ident_away_for_default_printing env_t id avoid + next_ident_away_for_default_printing sigma env_t id avoid (**********************************************************************) (* Displaying terms avoiding bound variables clashes *) @@ -345,70 +408,55 @@ type renaming_flags = | RenamingForGoal | RenamingElsewhereFor of (Name.t list * constr) -let next_name_for_display flags = +let next_name_for_display sigma flags = match flags with - | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t + | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern sigma env_t | RenamingForGoal -> next_name_away_in_goal - | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t + | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t (* Remark: Anonymous var may be dependent in Evar's contexts *) -let compute_displayed_name_in flags avoid na c = +let compute_displayed_name_in_gen_poly noccurn_fun sigma flags avoid na c = match na with - | Anonymous when noccurn 1 c -> + | Anonymous when noccurn_fun sigma 1 c -> (Anonymous,avoid) | _ -> - let fresh_id = next_name_for_display flags na avoid in - let idopt = if noccurn 1 c then Anonymous else Name fresh_id in - (idopt, fresh_id::avoid) + let fresh_id = next_name_for_display sigma flags na avoid in + let idopt = if noccurn_fun sigma 1 c then Anonymous else Name fresh_id in + (idopt, Id.Set.add fresh_id avoid) + +let compute_displayed_name_in = compute_displayed_name_in_gen_poly noccurn -let compute_and_force_displayed_name_in flags avoid na c = +let compute_displayed_name_in_gen f sigma = + (* only flag which does not need a constr, maybe to be refined *) + let flag = RenamingForGoal in + compute_displayed_name_in_gen_poly f sigma flag + +let compute_and_force_displayed_name_in sigma flags avoid na c = match na with - | Anonymous when noccurn 1 c -> + | Anonymous when noccurn sigma 1 c -> (Anonymous,avoid) | _ -> - let fresh_id = next_name_for_display flags na avoid in - (Name fresh_id, fresh_id::avoid) + let fresh_id = next_name_for_display sigma flags na avoid in + (Name fresh_id, Id.Set.add fresh_id avoid) -let compute_displayed_let_name_in flags avoid na c = - let fresh_id = next_name_for_display flags na avoid in - (Name fresh_id, fresh_id::avoid) +let compute_displayed_let_name_in sigma flags avoid na c = + let fresh_id = next_name_for_display sigma flags na avoid in + (Name fresh_id, Id.Set.add fresh_id avoid) -let rename_bound_vars_as_displayed avoid env c = +let rename_bound_vars_as_displayed sigma avoid env c = let rec rename avoid env c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (na,c1,c2) -> let na',avoid' = - compute_displayed_name_in + compute_displayed_name_in sigma (RenamingElsewhereFor (env,c2)) avoid na c2 in - mkProd (na', c1, rename avoid' (add_name na' env) c2) + mkProd (na', c1, rename avoid' (na' :: env) c2) | LetIn (na,c1,t,c2) -> let na',avoid' = - compute_displayed_let_name_in + compute_displayed_let_name_in sigma (RenamingElsewhereFor (env,c2)) avoid na c2 in - mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2) + mkLetIn (na',c1,t, rename avoid' (na' :: env) c2) | Cast (c,k,t) -> mkCast (rename avoid env c, k,t) | _ -> c in rename avoid env c - -(**********************************************************************) -(* "H"-based naming strategy introduced June 2014 for hypotheses in - Prop produced by case/elim/destruct/induction, in place of the - strategy that was using the first letter of the type, leading to - inelegant "n:~A", "e:t=u", etc. when eliminating sumbool or similar - types *) - -let h_based_elimination_names = ref false - -let use_h_based_elimination_names () = - !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4 - -open Goptions - -let _ = declare_bool_option - { optsync = true; - optdepr = false; - optname = "use of \"H\"-based proposition names in elimination tactics"; - optkey = ["Standard";"Proposition";"Elimination";"Names"]; - optread = (fun () -> !h_based_elimination_names); - optwrite = (:=) h_based_elimination_names } |