From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- engine/namegen.ml | 414 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 414 insertions(+) create mode 100644 engine/namegen.ml (limited to 'engine/namegen.ml') diff --git a/engine/namegen.ml b/engine/namegen.ml new file mode 100644 index 00000000..84eb9868 --- /dev/null +++ b/engine/namegen.ml @@ -0,0 +1,414 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let rec find_prefix = function + |MPfile dp1 -> not (DirPath.equal dp1 dp) + |MPdot(mp,_) -> find_prefix mp + |MPbound(_) -> false + in find_prefix (Lib.current_mp ()) + | _ -> false + +let is_imported_ref = function + | VarRef _ -> false + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> + let (mp,_,_) = repr_mind kn in is_imported_modpath mp + | ConstRef kn -> + let (mp,_,_) = repr_con kn in is_imported_modpath mp + +let is_global id = + try + let ref = locate (qualid_of_ident id) in + not (is_imported_ref ref) + with Not_found -> + false + +let is_constructor id = + try + match locate (qualid_of_ident id) with + | ConstructRef _ -> true + | _ -> false + with Not_found -> + false + +(**********************************************************************) +(* Generating "intuitive" names from its type *) + +let head_name c = (* Find the head constant of a constr if any *) + let rec hdrec c = + match kind_of_term 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 _ -> + Some (basename_of_global (global_of_constr c)) + | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> + Some (match lna.(i) with Name id -> id | _ -> assert false) + | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None + in + hdrec c + +let lowercase_first_char id = (* First character of a constr *) + Unicode.lowercase_first_char (Id.to_string id) + +let sort_hdchar = function + | Prop(_) -> "P" + | Type(_) -> "T" + +let hdchar env c = + let rec hdrec k c = + match kind_of_term 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)) + | Var id -> lowercase_first_char id + | Sort s -> sort_hdchar 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) + with Not_found -> "y") + | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> + let id = match lna.(i) with Name id -> id | _ -> assert false in + lowercase_first_char id + | Evar _ (* We could do better... *) + | Meta _ | Case (_, _, _, _) -> "y" + in + hdrec 0 c + +let id_of_name_using_hdchar env a = function + | Anonymous -> Id.of_string (hdchar env a) + | Name id -> id + +let named_hd env a = function + | Anonymous -> Name (Id.of_string (hdchar env 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 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 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_context env hyps = + snd + (List.fold_left + (fun (env,hyps) d -> + let d' = name_assumption env 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 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) + +(**********************************************************************) +(* Fresh names *) + +(* 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 + name_rec id + +(* Restart subscript from x0 if name starts with xN, or x00 if name + starts with x0N, etc *) + +let restart_subscript id = + if not (has_subscript id) then id else + (* It would probably be better with something in the spirit of + *** 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 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 (gseen, vseen, ids) = !accu in + let g = global_of_constr c in + if not (Refset_env.mem g gseen) then + begin + try + let gseen = Refset_env.add g gseen in + let short = shortest_qualid_of_global Id.Set.empty g in + let dir, id = repr_qualid short in + let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in + accu := (gseen, vseen, ids) + with Not_found when !Flags.in_debugger || !Flags.in_toplevel -> () + end + | Rel p -> + let (gseen, vseen, ids) = !accu in + 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 -> + (* Unbound index: may happen in debug and actually also + while computing temporary implicit arguments of an + inductive type *) + None + in + let ids = match name with + | Some (Name id) -> Id.Set.add id ids + | _ -> ids + in + accu := (gseen, vseen, ids) + | _ -> Constr.iter_with_binders succ visible_ids n c + in + let () = visible_ids 1 c in + let (_, _, ids) = !accu in + ids + +(* Now, there are different renaming strategies... *) + +(* 1- Looks for a fresh name for printing in cases pattern *) + +let next_name_away_in_cases_pattern 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 + next_ident_away_from id bad + +(* 2- Looks for a fresh name for introduction in goal *) + +(* The legacy strategy for renaming introduction variables is not very uniform: + - if the name to use is fresh in the context but used as a global + name, then a fresh name is taken by finding a free subscript + starting from the current subscript; + - but if the name to use is not fresh in the current context, the fresh + 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 + next_ident_away_from id bad + +let next_name_away_in_goal na avoid = + let id = match na with + | Name id -> id + | Anonymous -> default_non_dependent_ident in + next_ident_away_in_goal id avoid + +(* 3- Looks for next fresh name outside a list that is moreover valid + as a global identifier; the legacy algorithm is that if the name is + already used in the list, one looks for a name of same base with + lower available subscript; if the name is not in the list but is + used globally, one looks for a name of same base with lower subscript + 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 + 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) + else id + +let next_name_away_with_default default na avoid = + let id = match na with Name id -> id | Anonymous -> Id.of_string default in + next_ident_away id avoid + +let reserved_type_name = ref (fun t -> Anonymous) +let set_reserved_typed_name f = reserved_type_name := f + +let next_name_away_with_default_using_types default na avoid t = + let id = match na with + | Name id -> id + | Anonymous -> match !reserved_type_name t with + | Name id -> id + | Anonymous -> Id.of_string default in + next_ident_away id avoid + +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 + (fun decl newenv -> + let (na,_,t) = to_tuple decl in + let na = named_hd newenv t na in + let id = next_name_away na !avoid in + avoid := id::!avoid; + push_rel (set_name (Name id) decl) newenv) + env + +(* 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 + next_ident_away_from id bad + +let next_name_away_for_default_printing env_t na avoid = + let id = match na with + | Name id -> id + | Anonymous -> + (* In principle, an anonymous name is not dependent and will not be *) + (* 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 + +(**********************************************************************) +(* Displaying terms avoiding bound variables clashes *) + +(* Renaming strategy introduced in December 1998: + + - Rule number 1: all names, even if unbound and not displayed, contribute + to the list of names to avoid + - Rule number 2: only the dependency status is used for deciding if + a name is displayed or not + + Example: + bool_ind: "forall (P:bool->Prop)(f:(P true))(f:(P false))(b:bool), P b" is + displayed "forall P:bool->Prop, P true -> P false -> forall b:bool, P b" + but f and f0 contribute to the list of variables to avoid (knowing + that f and f0 are how the f's would be named if introduced, assuming + no other f and f0 are already used). +*) + +type renaming_flags = + | RenamingForCasesPattern of (Name.t list * constr) + | RenamingForGoal + | RenamingElsewhereFor of (Name.t list * constr) + +let next_name_for_display flags = + match flags with + | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t + | RenamingForGoal -> next_name_away_in_goal + | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t + +(* Remark: Anonymous var may be dependent in Evar's contexts *) +let compute_displayed_name_in flags avoid na c = + match na with + | Anonymous when noccurn 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 compute_and_force_displayed_name_in flags avoid na c = + match na with + | Anonymous when noccurn 1 c -> + (Anonymous,avoid) + | _ -> + let fresh_id = next_name_for_display flags na avoid in + (Name fresh_id, 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 rename_bound_vars_as_displayed avoid env c = + let rec rename avoid env c = + match kind_of_term c with + | Prod (na,c1,c2) -> + let na',avoid' = + compute_displayed_name_in + (RenamingElsewhereFor (env,c2)) avoid na c2 in + mkProd (na', c1, rename avoid' (add_name na' env) c2) + | LetIn (na,c1,t,c2) -> + let na',avoid' = + compute_displayed_let_name_in + (RenamingElsewhereFor (env,c2)) avoid na c2 in + mkLetIn (na',c1,t, rename avoid' (add_name 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 } -- cgit v1.2.3