Quelle namegen.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    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
   nameops.ml, Nov 2009 *)

(* This file is about generating new or fresh names and dealing with
   alpha-renaming *)

open Util
open Names
open Term
open Constr
open Context
open Environ
open EConstr
open Vars
open Nameops
open Libnames
open Context.Rel.Declaration

module RelDecl = Context.Rel.Declaration

(** General evar naming using intro patterns  *)
type intro_pattern_naming_expr =
  | IntroIdentifier of Id.t
  | IntroFresh of Id.t
  | IntroAnonymous

let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
| IntroAnonymous, IntroAnonymous -> true
| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
| _ -> false

(**********************************************************************)
(* Conventional names *)

let default_prop_string = "H"
let default_prop_ident = Id.of_string default_prop_string

let default_small_string = "H"
let default_small_ident = Id.of_string default_small_string

let default_type_string = "X"
let default_type_ident = Id.of_string default_type_string

let default_non_dependent_string = "H"
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 *)

let is_imported_modpath = function
  | MPfile dp ->
    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 = let open GlobRef in function
  | VarRef _ -> false
  | IndRef (kn,_)
  | ConstructRef ((kn,_),_) ->
      let mp = MutInd.modpath kn in is_imported_modpath mp
  | ConstRef kn ->
      let mp = Constant.modpath kn in is_imported_modpath mp

let locate id =
  match Nametab.locate_extended_nowarn (qualid_of_ident id) with
  | TrueGlobal r -> r
  | Abbrev _ -> raise Not_found

let is_global id =
  try
    let ref = locate id in
    not (is_imported_ref ref)
  with Not_found ->
    false

let is_constructor id =
  try
    match locate id with
      | GlobRef.ConstructRef _ -> true
      | _ -> false
  with Not_found ->
    false

let is_section_variable env id =
  try let _ = Environ.lookup_named id env in true
  with Not_found -> false

(**********************************************************************)
(* Generating "intuitive" names from its type *)

let global_of_constr = let open GlobRef in 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 EConstr.kind sigma c with
    | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
    | Cast (c,_,_) | App (c,_) -> hdrec c
    | Proj (kn,_,_) -> Some (Label.to_id (Constant.label (Projection.constant kn)))
    | Const _ | Ind _ | Construct _ | Var _ as c ->
        Some (Nametab.basename_of_global (global_of_constr c))
    | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
        Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
    | Sort _ | Rel _ | Meta _ | Evar _ | Case _
    | Int _ | Float _ | String _ | Array _ -> None
  in
  hdrec c

let lowercase_first_char id = (* First character of a constr *)
  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
  | SProp -> "P"
  | Prop -> "P"
  | Set -> "S"
  | Type _ | QSort _ -> "T"

let hdchar env sigma c =
  let rec hdrec k c =
    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 (Constant.label (Projection.constant kn)))
    | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn))
    | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
    | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
    | Var id  -> lowercase_first_char id
    | 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 let d = lookup_rel (n-k) env in get_name d, get_type d 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).binder_name with Name id -> id | _ -> assert false in
        lowercase_first_char id
    | Evar _ (* We could do better... *)
    | Meta _ | Case _ -> "y"
    | Int _ -> "i"
    | Float _ -> "f"
    | String _ -> "s"
    | Array _ -> "a"
  in
  hdrec 0 c

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 sigma a = function
  | Anonymous -> Name (Id.of_string (hdchar env sigma a))
  | x         -> x

let mkProd_name   env sigma (n,a,b) = mkProd (map_annot (named_hd env sigma a) n, a, b)
let mkLambda_name env sigma (n,a,b) = mkLambda (map_annot (named_hd env sigma a) n, a, b)

let lambda_name = mkLambda_name
let prod_name = mkProd_name

let prod_create   env sigma (r,a,b) =
  mkProd (make_annot (named_hd env sigma a Anonymous) r, a, b)
let lambda_create env sigma (r,a,b) =
  mkLambda (make_annot (named_hd env sigma a Anonymous) r, a, b)

let name_assumption env sigma = function
    | LocalAssum (na,t) -> LocalAssum (map_annot (named_hd env sigma t) na, t)
    | LocalDef (na,c,t) -> LocalDef (map_annot (named_hd env sigma c) na, c, t)

let name_context env sigma hyps =
  snd
    (List.fold_left
       (fun (env,hyps) d ->
          let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps))
       (env,[]) (List.rev hyps))

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 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.
   We also supply a version which only adds a prefix. *)

let { Goptions.get = get_mangle_names } =
  Goptions.declare_bool_option_and_ref
    ~key:["Mangle";"Names"]
    ~value:false
    ()

let { Goptions.get = get_mangle_names_light } =
  Goptions.declare_bool_option_and_ref
    ~key:["Mangle";"Names";"Light"]
    ~value:false
    ()

let { Goptions.get = mangle_names_prefix } =
  Goptions.declare_interpreted_string_option_and_ref
    ~key:["Mangle";"Names";"Prefix"]
    ~value:("_")
    (fun x ->
      Id.to_string
      (try
         Id.of_string x
       with
       | CErrors.UserError _ ->
         CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))
      )
    )
    (fun x -> x)
    ()

(** The name "foo" becomes "_0" if we get_mangle_names and "_foo" if
    get_mangle_names_light is also set. Otherwise it is left alone. *)

let mangle_id id =
  let prfx = mangle_names_prefix () in
  if get_mangle_names () then
    if get_mangle_names_light () then
      Id.of_string (prfx ^ Id.to_string id)
    else Id.of_string (prfx ^ "0")
  else id

(* Looks for next "good" name by lifting subscript *)

let next_ident_away_from_post_mangling id bad =
  let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in
  name_rec id

let next_ident_away_from id bad =
  let id = mangle_id id in
  next_ident_away_from_post_mangling id bad

(* 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

module Generator =
struct

type _ t =
| Fresh : Fresh.t t
| IdSet : Id.Set.t t

type 'a input = 'a t * 'a

let fresh = Fresh
let idset = IdSet

let max_map (type a) (gen : a t) (avoid : a) =
match gen with
| Fresh -> Fresh.max_map avoid
| IdSet ->
  let fold id accu =
    let id, ss = get_subscript id in
    match Id.Map.find_opt id accu with
    | Some old_ss when Subscript.compare ss old_ss <= 0 -> accu
    | _ -> Id.Map.add id ss accu
  in
  Id.Set.fold fold avoid Id.Map.empty

let is_fresh (type a) (gen : a t) id (avoid : a) = match gen with
| Fresh -> not (Fresh.mem id avoid)
| IdSet -> not (Id.Set.mem id avoid)

let gen_ident (type a) ?(mangle = true) ?(filter = (fun _ -> false)) (gen : a t) id (state : a) : Id.t * a =
  let id = if mangle then mangle_id id else id in
  match gen with
  | Fresh ->
    let rec gen state id =
      let (id, state) = Fresh.fresh id state in
      if filter id then gen state id else id
    in
    let id = gen state id in
    (id, Fresh.add id state)
  | IdSet ->
    let rec gen id = if Id.Set.mem id state || filter id then gen (increment_subscript id) else id in
    let id = gen id in
    (id, Id.Set.add id state)

let next_name_away gen na avoid =
  let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in
  let id = mangle_id id in
  let id = if is_fresh gen id avoid then id else restart_subscript id in
  gen_ident ~mangle:false gen id avoid

end

let visible_ids sigma (nenv, c) =
  let accu = ref (GlobRef.Set_env.empty, Int.Set.empty, Id.Set.empty) in
  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 (GlobRef.Set_env.mem g gseen) then
      let gseen = GlobRef.Set_env.add g gseen in
      let ids = match Nametab.shortest_qualid_of_global Id.Set.empty g with
      | short ->
        let dir, id = repr_qualid short in
        if DirPath.is_empty dir then Id.Set.add id ids else ids
      | exception Not_found ->
        (* This may happen if given pathological terms or when manipulating
           open modules *)
        ids
      in
      accu := (gseen, vseen, ids)
  | Rel p ->
    let (gseen, vseen, ids) = !accu in
    if p > n && not (Int.Set.mem (p - n) vseen) then
      let vseen = Int.Set.add (p - n) vseen in
      let name =
        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 *)
          None
      in
      let ids = match name with
      | Some (Name id) -> Id.Set.add id ids
      | _ -> ids
      in
      accu := (gseen, vseen, ids)
  | Evar (_,args as ev) ->
    (* Useful for at least debugger: do the same as in iter_with_binders *)
    (* except that Not_found is not fatal *)
    begin match Evd.expand_existential sigma ev with
    | args -> List.iter (visible_ids n) args
    | exception Not_found when !Flags.in_debugger ->
      SList.Skip.iter (visible_ids n) args
    end
  | _ -> EConstr.iter_with_binders sigma succ visible_ids n c
  in
  let () = visible_ids 1 c in (* n = 1 to count the binder to rename *)
  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 gen sigma env_t na avoid =
  let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
  let visible = visible_ids sigma env_t in
  let bad id = is_constructor id || Id.Set.mem id visible in
  Generator.gen_ident ~filter:bad gen id avoid

(* 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 env id avoid =
  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 env id)) in
  next_ident_away_from id bad

let next_name_away_in_goal (type a) (gen : a Generator.t) env na (avoid : a) =
  let id = match na with
    | Name id -> id
    | Anonymous -> default_non_dependent_ident in
  let id = if Generator.is_fresh gen id avoid then id else restart_subscript id in
  let bad id = is_global id && not (is_section_variable env id) in
  Generator.gen_ident ~filter:bad gen 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 senv id avoid =
  let id = if Id.Set.mem id avoid then restart_subscript id else id in
  let bad id = Id.Set.mem id avoid || Safe_typing.exists_objlabel (Label.of_id id) senv 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 =
  let id = mangle_id id in
  if Id.Set.mem id avoid then
    next_ident_away_from_post_mangling (restart_subscript id) (fun id -> Id.Set.mem 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_rel_context_name_different env sigma ctx =
  let avoid = ref (Id.Set.union (Context.Rel.to_vars (Environ.rel_context env)) (ids_of_named_context_val (named_context_val env))) in
  Context.Rel.fold_outside
    (fun decl (newenv,ctx) ->
       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.Set.add id !avoid;
       let decl = RelDecl.set_name (Name id) decl in
       push_rel decl newenv, decl :: ctx)
    ctx ~init:(env,[])

let make_all_name_different env sigma =
  (* FIXME: this is inefficient, but only used in printing *)
  let sign = named_context_val env in
  let rels = rel_context env in
  let env0 = reset_with_named_context sign env in
  let env,_ = make_all_rel_context_name_different env0 sigma rels in
  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 gen sigma env_t id avoid =
  let visible = visible_ids sigma env_t in
  let bad id = Id.Set.mem id visible in
  Generator.gen_ident ~filter:bad gen id avoid

let next_name_away_for_default_printing gen sigma 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 gen sigma 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 =
  (* The term is the body of a binder and the environment excludes this binder *)
  (* so, there is a missing binder in the environment *)
  | RenamingForCasesPattern of (Name.t list * constr)
  | RenamingForGoal
  | RenamingElsewhereFor of (Name.t list * constr)

let next_name_for_display gen env sigma flags na avoid =
  match flags with
  | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern gen sigma env_t na avoid
  | RenamingForGoal -> next_name_away_in_goal gen env na avoid
  | RenamingElsewhereFor env_t -> next_name_away_for_default_printing gen sigma env_t na avoid

(* Remark: Anonymous var may be dependent in Evar's contexts *)
let compute_displayed_name_in_gen_poly gen noccurn_fun env sigma flags avoid na c =
  let noccurs =
    try noccurn_fun sigma 1 c
    with _ when !Flags.in_debugger -> false
  in
  if noccurs then Anonymous, avoid
  else
    let fresh_id, avoid = next_name_for_display gen env sigma flags na avoid in
    Name fresh_id, avoid

let compute_displayed_name_in gen = compute_displayed_name_in_gen_poly gen noccurn

let compute_displayed_name_in_gen gen f env sigma =
  (* only flag which does not need a constr, maybe to be refined *)
  let flag = RenamingForGoal in
  compute_displayed_name_in_gen_poly gen f env sigma flag

let compute_displayed_let_name_in gen env sigma flags avoid na =
  let fresh_id, avoid = next_name_for_display gen env sigma flags na avoid in
  (Name fresh_id, avoid)

quality100%

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.