From 67f5c70a480c95cfb819fc68439781b5e5e95794 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 15:56:25 +0000 Subject: Modulification of identifier git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/cc/ccalgo.ml | 14 ++-- plugins/cc/ccalgo.mli | 18 ++--- plugins/cc/cctac.ml | 18 ++--- plugins/decl_mode/decl_expr.mli | 10 +-- plugins/decl_mode/decl_interp.ml | 2 +- plugins/decl_mode/decl_mode.ml | 10 +-- plugins/decl_mode/decl_mode.mli | 12 ++-- plugins/decl_mode/decl_proof_instr.ml | 64 +++++++++--------- plugins/decl_mode/decl_proof_instr.mli | 42 ++++++------ plugins/extraction/common.ml | 32 ++++----- plugins/extraction/common.mli | 16 ++--- plugins/extraction/extract_env.ml | 6 +- plugins/extraction/extract_env.mli | 2 +- plugins/extraction/extraction.ml | 2 +- plugins/extraction/extraction.mli | 2 +- plugins/extraction/g_extraction.ml4 | 2 +- plugins/extraction/haskell.ml | 8 +-- plugins/extraction/miniml.mli | 26 +++---- plugins/extraction/mlutil.ml | 6 +- plugins/extraction/mlutil.mli | 8 +-- plugins/extraction/ocaml.ml | 6 +- plugins/extraction/scheme.ml | 6 +- plugins/extraction/table.ml | 34 +++++----- plugins/extraction/table.mli | 8 +-- plugins/firstorder/formula.ml | 2 +- plugins/firstorder/ground.ml | 2 +- plugins/firstorder/instances.ml | 2 +- plugins/firstorder/rules.mli | 2 +- plugins/fourier/fourierR.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 64 +++++++++--------- plugins/funind/functional_principles_types.ml | 14 ++-- plugins/funind/functional_principles_types.mli | 6 +- plugins/funind/g_indfun.ml4 | 6 +- plugins/funind/glob_term_to_relation.ml | 94 +++++++++++++------------- plugins/funind/glob_term_to_relation.mli | 2 +- plugins/funind/glob_termops.ml | 69 +++++++++---------- plugins/funind/glob_termops.mli | 34 ++++------ plugins/funind/indfun.ml | 30 ++++---- plugins/funind/indfun_common.ml | 14 ++-- plugins/funind/indfun_common.mli | 28 ++++---- plugins/funind/invfun.ml | 60 ++++++++-------- plugins/funind/merge.ml | 62 ++++++++--------- plugins/funind/recdef.ml | 70 +++++++++---------- plugins/funind/recdef.mli | 4 +- plugins/micromega/coq_micromega.ml | 10 +-- plugins/omega/coq_omega.ml | 30 ++++---- plugins/omega/g_omega.ml4 | 2 +- plugins/quote/quote.ml | 4 +- plugins/romega/const_omega.ml | 10 +-- plugins/romega/g_romega.ml4 | 2 +- plugins/romega/refl_omega.ml | 8 +-- plugins/rtauto/refl_tauto.mli | 4 +- plugins/setoid_ring/newring.ml4 | 40 +++++------ plugins/syntax/ascii_syntax.ml | 6 +- plugins/syntax/numbers_syntax.ml | 4 +- plugins/syntax/r_syntax.ml | 6 +- plugins/syntax/z_syntax.ml | 10 +-- plugins/xml/acic.ml | 16 ++--- plugins/xml/acic2Xml.ml4 | 20 +++--- plugins/xml/cic2acic.ml | 24 +++---- plugins/xml/xmlcommand.ml | 22 +++--- 61 files changed, 566 insertions(+), 573 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 2155171c9..f029c053a 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -98,7 +98,7 @@ type cinfo= type term= Symb of constr | Product of sorts_family * sorts_family - | Eps of identifier + | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) @@ -106,7 +106,7 @@ let rec term_equal t1 t2 = match t1, t2 with | Symb c1, Symb c2 -> eq_constr c1 c2 | Product (s1, t1), Product (s2, t2) -> s1 = s2 && t1 = t2 - | Eps i1, Eps i2 -> id_ord i1 i2 = 0 + | Eps i1, Eps i2 -> Id.compare i1 i2 = 0 | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2 | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1}, Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} -> @@ -149,7 +149,7 @@ type patt_kind = | Creates_variables type quant_eq = - {qe_hyp_id: identifier; + {qe_hyp_id: Id.t; qe_pol: bool; qe_nvars:int; qe_lhs: ccpattern; @@ -203,7 +203,7 @@ module Termhash = Hashtbl.Make end) module Identhash = Hashtbl.Make - (struct type t = identifier + (struct type t = Id.t let equal = Pervasives.(=) let hash = Hashtbl.hash end) @@ -356,8 +356,8 @@ let new_representative typ = (* rebuild a constr from an applicative term *) -let _A_ = Name (id_of_string "A") -let _B_ = Name (id_of_string "A") +let _A_ = Name (Id.of_string "A") +let _B_ = Name (Id.of_string "A") let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2) let cc_product s1 s2 = @@ -722,7 +722,7 @@ let one_step state = true with Not_found -> false -let __eps__ = id_of_string "_eps_" +let __eps__ = Id.of_string "_eps_" let new_state_var typ state = let id = pf_get_new_id __eps__ state.gls in diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 6232b126e..5d286c732 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -18,7 +18,7 @@ type cinfo = type term = Symb of constr | Product of sorts_family * sorts_family - | Eps of identifier + | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) @@ -87,7 +87,7 @@ val add_equality : state -> constr -> term -> term -> unit val add_disequality : state -> from -> term -> term -> unit -val add_quant : state -> identifier -> bool -> +val add_quant : state -> Id.t -> bool -> int * patt_kind * ccpattern * patt_kind * ccpattern -> unit val tail_pac : pa_constructor -> pa_constructor @@ -106,7 +106,7 @@ val join_path : forest -> int -> int -> ((int * int) * equality) list * ((int * int) * equality) list type quant_eq= - {qe_hyp_id: identifier; + {qe_hyp_id: Id.t; qe_pol: bool; qe_nvars:int; qe_lhs: ccpattern; @@ -161,7 +161,7 @@ type term = type rule = Congruence - | Axiom of Names.identifier + | Axiom of Names.Id.t | Injection of int*int*int*int type equality = @@ -207,19 +207,19 @@ val process_rec : UF.t -> equality list -> int list val cc : UF.t -> unit val make_uf : - (Names.identifier * (term * term)) list -> UF.t + (Names.Id.t * (term * term)) list -> UF.t val add_one_diseq : UF.t -> (term * term) -> int * int val add_disaxioms : - UF.t -> (Names.identifier * (term * term)) list -> - (Names.identifier * (int * int)) list + UF.t -> (Names.Id.t * (term * term)) list -> + (Names.Id.t * (int * int)) list val check_equal : UF.t -> int * int -> bool val find_contradiction : UF.t -> - (Names.identifier * (int * int)) list -> - (Names.identifier * (int * int)) + (Names.Id.t * (int * int)) list -> + (Names.Id.t * (int * int)) *) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 7d4d1728a..9a2f23d64 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -238,7 +238,7 @@ let build_projection intype outtype (cstr:constructor) special default gls= let pred=mkLambda(Anonymous,intype,outtype) in let case_info=make_case_info (pf_env gls) ind RegularStyle in let body= mkCase(case_info, pred, casee, branches) in - let id=pf_get_new_id (id_of_string "t") gls in + let id=pf_get_new_id (Id.of_string "t") gls in mkLambda(Name id,intype,body) (* generate an adhoc tactic following the proof tree *) @@ -275,7 +275,7 @@ let rec proof_tac p gls = let typf = Termops.refresh_universes (pf_type_of gls tf1) in let typx = Termops.refresh_universes (pf_type_of gls tx1) in let typfx = Termops.refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in - let id = pf_get_new_id (id_of_string "f") gls in + let id = pf_get_new_id (Id.of_string "f") gls in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = mkApp(Lazy.force _f_equal, @@ -316,7 +316,7 @@ let refute_tac c t1 t2 p gls = let neweq= mkApp(Lazy.force _eq, [|intype;tt1;tt2|]) in - let hid=pf_get_new_id (id_of_string "Heq") gls in + let hid=pf_get_new_id (Id.of_string "Heq") gls in let false_t=mkApp (c,[|mkVar hid|]) in tclTHENS (assert_tac (Name hid) neweq) [proof_tac p; simplest_elim false_t] gls @@ -325,8 +325,8 @@ let convert_to_goal_tac c t1 t2 p gls = let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort = Termops.refresh_universes (pf_type_of gls tt2) in let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in - let e=pf_get_new_id (id_of_string "e") gls in - let x=pf_get_new_id (id_of_string "X") gls in + let e=pf_get_new_id (Id.of_string "e") gls in + let x=pf_get_new_id (Id.of_string "X") gls in let identity=mkLambda (Name x,sort,mkRel 1) in let endt=mkApp (Lazy.force _eq_rect, [|sort;tt1;identity;c;tt2;mkVar e|]) in @@ -335,7 +335,7 @@ let convert_to_goal_tac c t1 t2 p gls = let convert_to_hyp_tac c1 t1 c2 t2 p gls = let tt2=constr_of_term t2 in - let h=pf_get_new_id (id_of_string "H") gls in + let h=pf_get_new_id (Id.of_string "H") gls in let false_t=mkApp (c2,[|mkVar h|]) in tclTHENS (assert_tac (Name h) tt2) [convert_to_goal_tac c1 t1 t2 p; @@ -346,13 +346,13 @@ let discriminate_tac cstr p gls = let intype = Termops.refresh_universes (pf_type_of gls t1) in let concl=pf_concl gls in let outsort = mkType (Termops.new_univ ()) in - let xid=pf_get_new_id (id_of_string "X") gls in - let tid=pf_get_new_id (id_of_string "t") gls in + let xid=pf_get_new_id (Id.of_string "X") gls in + let tid=pf_get_new_id (Id.of_string "t") gls in let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in let trivial=pf_type_of gls identity in let outtype = mkType (Termops.new_univ ()) in let pred=mkLambda(Name xid,outtype,mkRel 1) in - let hid=pf_get_new_id (id_of_string "Heq") gls in + let hid=pf_get_new_id (Id.of_string "Heq") gls in let proj=build_projection intype outtype cstr trivial concl gls in let injt=mkApp (Lazy.force _f_equal, [|intype;outtype;proj;t1;t2;mkVar hid|]) in diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 966429682..966ebff40 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -16,7 +16,7 @@ type 'it statement = type thesis_kind = Plain - | For of identifier + | For of Id.t type 'this or_thesis = This of 'this @@ -60,8 +60,8 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr = | Pconsider of 'constr*('hyp,'constr) hyp list | Pclaim of 'constr statement | Pfocus of 'constr statement - | Pdefine of identifier * 'hyp list * 'constr - | Pcast of identifier or_thesis * 'constr + | Pdefine of Id.t * 'hyp list * 'constr + | Pcast of Id.t or_thesis * 'constr | Psuppose of ('hyp,'constr) hyp list | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) | Ptake of 'constr list @@ -77,13 +77,13 @@ type ('hyp,'constr,'pat,'tac) gen_proof_instr= type raw_proof_instr = - ((identifier*(Constrexpr.constr_expr option)) Loc.located, + ((Id.t*(Constrexpr.constr_expr option)) Loc.located, Constrexpr.constr_expr, Constrexpr.cases_pattern_expr, raw_tactic_expr) gen_proof_instr type glob_proof_instr = - ((identifier*(Genarg.glob_constr_and_expr option)) Loc.located, + ((Id.t*(Genarg.glob_constr_and_expr option)) Loc.located, Genarg.glob_constr_and_expr, Constrexpr.cases_pattern_expr, Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 5e185f7e3..eb7d9e8e4 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -219,7 +219,7 @@ let interp_hyps_gen inject blend sigma env hyps head = let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop) -let dummy_prefix= id_of_string "__" +let dummy_prefix= Id.of_string "__" let rec deanonymize ids = function diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 1f55257e5..4bab801b1 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -24,11 +24,11 @@ let get_daimon_flag () = !daimon_flag open Store.Field type split_tree= - Skip_patt of Idset.t * split_tree - | Split_patt of Idset.t * inductive * - (bool array * (Idset.t * split_tree) option) array + Skip_patt of Id.Set.t * split_tree + | Split_patt of Id.Set.t * inductive * + (bool array * (Id.Set.t * split_tree) option) array | Close_patt of split_tree - | End_patt of (identifier * (int * int)) + | End_patt of (Id.t * (int * int)) type elim_kind = EK_dep of split_tree @@ -48,7 +48,7 @@ type per_info = per_wf:recpath} type stack_info = - Per of Decl_expr.elim_type * per_info * elim_kind * identifier list + Per of Decl_expr.elim_type * per_info * elim_kind * Id.t list | Suppose_case | Claim | Focus_claim diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index f23a97b4e..853135f10 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -27,11 +27,11 @@ val get_current_mode : unit -> command_mode val check_not_proof_mode : string -> unit type split_tree= - Skip_patt of Idset.t * split_tree - | Split_patt of Idset.t * inductive * - (bool array * (Idset.t * split_tree) option) array + Skip_patt of Id.Set.t * split_tree + | Split_patt of Id.Set.t * inductive * + (bool array * (Id.Set.t * split_tree) option) array | Close_patt of split_tree - | End_patt of (identifier * (int * int)) + | End_patt of (Id.t * (int * int)) type elim_kind = EK_dep of split_tree @@ -51,7 +51,7 @@ type per_info = per_wf:recpath} type stack_info = - Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list + Per of Decl_expr.elim_type * per_info * elim_kind * Names.Id.t list | Suppose_case | Claim | Focus_claim @@ -69,7 +69,7 @@ val get_stack : Proof.proof -> stack_info list val get_top_stack : Proof.proof -> stack_info list -val get_last: Environ.env -> identifier +val get_last: Environ.env -> Id.t val focus : Proof.proof -> unit diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 8075f05e9..a42e0cb3e 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -91,7 +91,7 @@ let mk_evd metalist gls = meta_declare meta typ evd in List.fold_right add_one metalist evd0 -let is_tmp id = (string_of_id id).[0] = '_' +let is_tmp id = (Id.to_string id).[0] = '_' let tmp_ids gls = let ctx = pf_hyps gls in @@ -210,27 +210,27 @@ let filter_hyps f gls = tclTRY (clear [id]) in tclMAP filter_aux (pf_hyps gls) gls -let local_hyp_prefix = id_of_string "___" +let local_hyp_prefix = Id.of_string "___" let add_justification_hyps keep items gls = let add_aux c gls= match kind_of_term c with Var id -> - keep:=Idset.add id !keep; + keep:=Id.Set.add id !keep; tclIDTAC gls | _ -> let id=pf_get_new_id local_hyp_prefix gls in - keep:=Idset.add id !keep; + keep:=Id.Set.add id !keep; tclTHEN (letin_tac None (Names.Name id) c None Locusops.nowhere) (thin_body [id]) gls in tclMAP add_aux items gls let prepare_goal items gls = - let tokeep = ref Idset.empty in + let tokeep = ref Id.Set.empty in let auxres = add_justification_hyps tokeep items gls in tclTHENLIST [ (fun _ -> auxres); - filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep)] gls + filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls let my_automation_tac = ref (fun gls -> anomaly "No automation registered") @@ -474,7 +474,7 @@ let instr_cut mkstat _thus _then cut gls0 = let stat = cut.cut_stat in let (c_id,_) = match stat.st_label with Anonymous -> - pf_get_new_id (id_of_string "_fact") gls0,false + pf_get_new_id (Id.of_string "_fact") gls0,false | Name id -> id,true in let c_stat = mkstat info gls0 stat.st_it in let thus_tac gls= @@ -520,7 +520,7 @@ let instr_rew _thus rew_side cut gls0 = justification (tclTHEN items_tac method_tac) gls in let (c_id,_) = match cut.cut_stat.st_label with Anonymous -> - pf_get_new_id (id_of_string "_eq") gls0,false + pf_get_new_id (Id.of_string "_eq") gls0,false | Name id -> id,true in let thus_tac new_eq gls= if _thus then @@ -549,7 +549,7 @@ let instr_rew _thus rew_side cut gls0 = let instr_claim _thus st gls0 = let info = get_its_info gls0 in let (id,_) = match st.st_label with - Anonymous -> pf_get_new_id (id_of_string "_claim") gls0,false + Anonymous -> pf_get_new_id (Id.of_string "_claim") gls0,false | Name id -> id,true in let thus_tac gls= if _thus then @@ -566,7 +566,7 @@ let instr_claim _thus st gls0 = let push_intro_tac coerce nam gls = let (hid,_) = match nam with - Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false + Anonymous -> pf_get_new_id (Id.of_string "_hyp") gls,false | Name id -> id,true in tclTHENLIST [intro_mustbe_force hid; @@ -640,7 +640,7 @@ let rec build_applist prod = function let instr_suffices _then cut gls0 = let info = get_its_info gls0 in - let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in + let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in let ctx,hd = cut.cut_stat in let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in let metas = metas_from 1 ctx in @@ -677,7 +677,7 @@ let rec intron_then n ids ltac gls = if n<=0 then ltac ids gls else - let id = pf_get_new_id (id_of_string "_tmp") gls in + let id = pf_get_new_id (Id.of_string "_tmp") gls in tclTHEN (intro_mustbe_force id) (intron_then (pred n) (id::ids) ltac) gls @@ -692,7 +692,7 @@ let rec consider_match may_intro introduced available expected gls = | [],hyps -> if may_intro then begin - let id = pf_get_new_id (id_of_string "_tmp") gls in + let id = pf_get_new_id (Id.of_string "_tmp") gls in tclIFTHENELSE (intro_mustbe_force id) (consider_match true [] [id] hyps) @@ -732,7 +732,7 @@ let consider_tac c hyps gls = Var id -> consider_match false [] [id] hyps gls | _ -> - let id = pf_get_new_id (id_of_string "_tmp") gls in + let id = pf_get_new_id (Id.of_string "_tmp") gls in tclTHEN (forward None (Some (Loc.ghost, IntroIdentifier id)) c) (consider_match false [] [id] hyps) gls @@ -823,7 +823,7 @@ let map_tree id_fun mapi = function let start_tree env ind rp = - init_tree Idset.empty ind rp (fun _ _ -> None) + init_tree Id.Set.empty ind rp (fun _ _ -> None) let build_per_info etype casee gls = let concl=pf_concl gls in @@ -872,7 +872,7 @@ let per_tac etype casee gls= Per(etype,per_info,ek,[])::info.pm_stack} gls | Virtual cut -> assert (cut.cut_stat.st_label=Anonymous); - let id = pf_get_new_id (id_of_string "anonymous_matched") gls in + let id = pf_get_new_id (Id.of_string "anonymous_matched") gls in let c = mkVar id in let modified_cut = {cut with cut_stat={cut.cut_stat with st_label=Name id}} in @@ -901,7 +901,7 @@ let register_nodep_subcase id= function let suppose_tac hyps gls0 = let info = get_its_info gls0 in let thesis = pf_concl gls0 in - let id = pf_get_new_id (id_of_string "subcase_") gls0 in + let id = pf_get_new_id (Id.of_string "subcase_") gls0 in let clause = build_product hyps thesis in let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let old_clauses,stack = register_nodep_subcase id info.pm_stack in @@ -931,17 +931,17 @@ let rec tree_of_pats ((id,_) as cpl) pats = | (patt,rp) :: rest_args -> match patt with PatVar (_,v) -> - Skip_patt (Idset.singleton id, + Skip_patt (Id.Set.singleton id, tree_of_pats cpl (rest_args::stack)) | PatCstr (_,(ind,cnum),args,nam) -> let nexti i ati = if i = pred cnum then let nargs = List.map_i (fun j a -> (a,ati.(j))) 0 args in - Some (Idset.singleton id, + Some (Id.Set.singleton id, tree_of_pats cpl (nargs::rest_args::stack)) else None - in init_tree Idset.empty ind rp nexti + in init_tree Id.Set.empty ind rp nexti let rec add_branch ((id,_) as cpl) pats tree= match pats with @@ -967,10 +967,10 @@ let rec add_branch ((id,_) as cpl) pats tree= begin match tree with Skip_patt (ids,t) -> - Skip_patt (Idset.add id ids, + Skip_patt (Id.Set.add id ids, add_branch cpl (rest_args::stack) t) | Split_patt (_,_,_) -> - map_tree (Idset.add id) + map_tree (Id.Set.add id) (fun i bri -> append_branch cpl 1 (rest_args::stack) bri) tree @@ -983,7 +983,7 @@ let rec add_branch ((id,_) as cpl) pats tree= if i = pred cnum then let nargs = List.map_i (fun j a -> (a,ati.(j))) 0 args in - Some (Idset.add id ids, + Some (Id.Set.add id ids, add_branch cpl (nargs::rest_args::stack) (skip_args t ids (Array.length ati))) else @@ -1005,19 +1005,19 @@ let rec add_branch ((id,_) as cpl) pats tree= | _ -> anomaly "No pop/stop expected here" and append_branch ((id,_) as cpl) depth pats = function Some (ids,tree) -> - Some (Idset.add id ids,append_tree cpl depth pats tree) + Some (Id.Set.add id ids,append_tree cpl depth pats tree) | None -> - Some (Idset.singleton id,tree_of_pats cpl pats) + Some (Id.Set.singleton id,tree_of_pats cpl pats) and append_tree ((id,_) as cpl) depth pats tree = if depth<=0 then add_branch cpl pats tree else match tree with Close_patt t -> Close_patt (append_tree cpl (pred depth) pats t) | Skip_patt (ids,t) -> - Skip_patt (Idset.add id ids,append_tree cpl depth pats t) + Skip_patt (Id.Set.add id ids,append_tree cpl depth pats t) | End_patt _ -> anomaly "Premature end of branch" | Split_patt (_,_,_) -> - map_tree (Idset.add id) + map_tree (Id.Set.add id) (fun i bri -> append_branch cpl (succ depth) pats bri) tree (* suppose it is *) @@ -1101,7 +1101,7 @@ let rec register_dep_subcase id env per_info pat = function let case_tac params pat_info hyps gls0 = let info = get_its_info gls0 in - let id = pf_get_new_id (id_of_string "subcase_") gls0 in + let id = pf_get_new_id (Id.of_string "subcase_") gls0 in let et,per_info,ek,old_clauses,rest = match info.pm_stack with Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) @@ -1139,7 +1139,7 @@ let push_arg arg stacks = let push_one_head c ids (id,stack) = - let head = if Idset.mem id ids then Some c else None in + let head = if Id.Set.mem id ids then Some c else None in id,(head,[]) :: stack let push_head c ids stacks = @@ -1251,7 +1251,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = | Some (sub_ids,tree) -> let br_args = List.filter - (fun (id,_) -> Idset.mem id sub_ids) args in + (fun (id,_) -> Id.Set.mem id sub_ids) args in let construct = applist (mkConstruct(ind,succ i),params) in let p_args = @@ -1333,9 +1333,9 @@ let end_tac et2 gls = begin fun gls0 -> let fix_id = - pf_get_new_id (id_of_string "_fix") gls0 in + pf_get_new_id (Id.of_string "_fix") gls0 in let c_id = - pf_get_new_id (id_of_string "_main_arg") gls0 in + pf_get_new_id (Id.of_string "_main_arg") gls0 in tclTHENLIST [fix (Some fix_id) (succ nargs); tclDO nargs introf; diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli index 775d2f535..fb7e5c29a 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -31,24 +31,24 @@ val execute_cases : Names.name -> Decl_mode.per_info -> (Term.constr -> Proof_type.tactic) -> - (Names.Idset.elt * (Term.constr option * Term.constr list) list) list -> + (Names.Id.Set.elt * (Term.constr option * Term.constr list) list) list -> Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic val tree_of_pats : - identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> + Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> split_tree val add_branch : - identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> + Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> split_tree -> split_tree val append_branch : - identifier *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> - (Names.Idset.t * Decl_mode.split_tree) option -> - (Names.Idset.t * Decl_mode.split_tree) option + Id.t *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> + (Names.Id.Set.t * Decl_mode.split_tree) option -> + (Names.Id.Set.t * Decl_mode.split_tree) option val append_tree : - identifier * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> + Id.t * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> split_tree -> split_tree val build_dep_clause : Term.types Decl_expr.statement list -> @@ -58,7 +58,7 @@ val build_dep_clause : Term.types Decl_expr.statement list -> Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types val register_dep_subcase : - Names.identifier * (int * int) -> + Names.Id.t * (int * int) -> Environ.env -> Decl_mode.per_info -> Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind @@ -69,41 +69,41 @@ val thesis_for : Term.constr -> val close_previous_case : Proof.proof -> unit val pop_stacks : - (Names.identifier * + (Names.Id.t * (Term.constr option * Term.constr list) list) list -> - (Names.identifier * + (Names.Id.t * (Term.constr option * Term.constr list) list) list val push_head : Term.constr -> - Names.Idset.t -> - (Names.identifier * + Names.Id.Set.t -> + (Names.Id.t * (Term.constr option * Term.constr list) list) list -> - (Names.identifier * + (Names.Id.t * (Term.constr option * Term.constr list) list) list val push_arg : Term.constr -> - (Names.identifier * + (Names.Id.t * (Term.constr option * Term.constr list) list) list -> - (Names.identifier * + (Names.Id.t * (Term.constr option * Term.constr list) list) list val hrec_for: - Names.identifier -> + Names.Id.t -> Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> - Names.identifier -> Term.constr + Names.Id.t -> Term.constr val consider_match : bool -> - (Names.Idset.elt*bool) list -> - Names.Idset.elt list -> + (Names.Id.Set.elt*bool) list -> + Names.Id.Set.elt list -> (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list -> Proof_type.tactic val init_tree: - Names.Idset.t -> + Names.Id.Set.t -> Names.inductive -> int option * Declarations.wf_paths -> (int -> (int option * Declarations.recarg Rtree.t) array -> - (Names.Idset.t * Decl_mode.split_tree) option) -> + (Names.Id.Set.t * Decl_mode.split_tree) option) -> Decl_mode.split_tree diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 04cc167a8..3269befdb 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -18,7 +18,7 @@ open Miniml open Mlutil let string_of_id id = - let s = Names.string_of_id id in + let s = Names.Id.to_string id in for i = 0 to String.length s - 2 do if s.[i] = '_' && s.[i+1] = '_' then warning_id s done; @@ -109,12 +109,12 @@ let pseudo_qualify = qualify "__" let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false -let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id)) +let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id)) let uppercase_id id = let s = string_of_id id in assert (s<>""); - if s.[0] = '_' then id_of_string ("Coq_"^s) - else id_of_string (String.capitalize s) + if s.[0] = '_' then Id.of_string ("Coq_"^s) + else Id.of_string (String.capitalize s) type kind = Term | Type | Cons | Mod @@ -128,12 +128,12 @@ let kindcase_id k id = (*s de Bruijn environments for programs *) -type env = identifier list * Idset.t +type env = Id.t list * Id.Set.t (*s Generic renaming issues for local variable names. *) let rec rename_id id avoid = - if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id + if Id.Set.mem id avoid then rename_id (lift_subscript id) avoid else id let rec rename_vars avoid = function | [] -> @@ -145,14 +145,14 @@ let rec rename_vars avoid = function | id :: idl -> let (idl, avoid) = rename_vars avoid idl in let id = rename_id (lowercase_id id) avoid in - (id :: idl, Idset.add id avoid) + (id :: idl, Id.Set.add id avoid) let rename_tvars avoid l = let rec rename avoid = function | [] -> [],avoid | id :: idl -> let id = rename_id (lowercase_id id) avoid in - let idl, avoid = rename (Idset.add id avoid) idl in + let idl, avoid = rename (Id.Set.add id avoid) idl in (id :: idl, avoid) in fst (rename avoid l) @@ -162,7 +162,7 @@ let push_vars ids (db,avoid) = let get_db_name n (db,_) = let id = List.nth db (pred n) in - if id = dummy_name then id_of_string "__" else id + if id = dummy_name then Id.of_string "__" else id (*S Renamings of global objects. *) @@ -179,13 +179,13 @@ let set_phase, get_phase = let ph = ref Impl in ((:=) ph), (fun () -> !ph) let set_keywords, get_keywords = - let k = ref Idset.empty in + let k = ref Id.Set.empty in ((:=) k), (fun () -> !k) let add_global_ids, get_global_ids = - let ids = ref Idset.empty in + let ids = ref Id.Set.empty in register_cleanup (fun () -> ids := get_keywords ()); - let add s = ids := Idset.add s !ids + let add s = ids := Id.Set.add s !ids and get () = !ids in (add,get) @@ -309,7 +309,7 @@ let modular_rename k id = if upperkind k then "Coq_",is_upper else "coq_",is_lower in if not (is_ok s) || - (Idset.mem id (get_keywords ())) || + (Id.Set.mem id (get_keywords ())) || (String.length s >= 4 && String.sub s 0 4 = prefix) then prefix ^ s else s @@ -320,7 +320,7 @@ let modular_rename k id = let modfstlev_rename = let add_prefixes,get_prefixes,_ = mktable true in fun l -> - let coqid = id_of_string "Coq" in + let coqid = Id.of_string "Coq" in let id = id_of_label l in try let coqset = get_prefixes id in @@ -372,12 +372,12 @@ let ref_renaming_fun (k,r) = let idg = safe_basename_of_global r in if l = [""] (* this happens only at toplevel of the monolithic case *) then - let globs = Idset.elements (get_global_ids ()) in + let globs = Id.Set.elements (get_global_ids ()) in let id = next_ident_away (kindcase_id k idg) globs in string_of_id id else modular_rename k idg in - add_global_ids (id_of_string s); + add_global_ids (Id.of_string s); s::l (* Cached version of the last function *) diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 7233b8c2b..9ddd0f2af 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -33,17 +33,17 @@ val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -val pr_binding : identifier list -> std_ppcmds +val pr_binding : Id.t list -> std_ppcmds -val rename_id : identifier -> Idset.t -> identifier +val rename_id : Id.t -> Id.Set.t -> Id.t -type env = identifier list * Idset.t +type env = Id.t list * Id.Set.t val empty_env : unit -> env -val rename_vars: Idset.t -> identifier list -> env -val rename_tvars: Idset.t -> identifier list -> identifier list -val push_vars : identifier list -> env -> identifier list * env -val get_db_name : int -> env -> identifier +val rename_vars: Id.Set.t -> Id.t list -> env +val rename_tvars: Id.Set.t -> Id.t list -> Id.t list +val push_vars : Id.t list -> env -> Id.t list * env +val get_db_name : int -> env -> Id.t type phase = Pre | Impl | Intf @@ -69,7 +69,7 @@ type reset_kind = AllButExternal | Everything val reset_renaming_tables : reset_kind -> unit -val set_keywords : Idset.t -> unit +val set_keywords : Id.Set.t -> unit (** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 0b4047f17..3cd3f7f8a 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -388,7 +388,7 @@ let descr () = match lang () with (* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" Works similarly for the other languages. *) -let default_id = id_of_string "Main" +let default_id = Id.of_string "Main" let mono_filename f = let d = descr () in @@ -402,7 +402,7 @@ let mono_filename f = in let id = if lang () <> Haskell then default_id - else try id_of_string (Filename.basename f) + else try Id.of_string (Filename.basename f) with _ -> error "Extraction: provided filename is not a valid identifier" in Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id @@ -412,7 +412,7 @@ let mono_filename f = let module_filename mp = let f = file_of_modfile mp in let d = descr () in - Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f + Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f (*s Extraction of one decl to stdout. *) diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 5e14214b9..6c648b981 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -15,7 +15,7 @@ open Globnames val simple_extraction : reference -> unit val full_extraction : string option -> reference list -> unit val separate_extraction : reference list -> unit -val extraction_library : bool -> identifier -> unit +val extraction_library : bool -> Id.t -> unit (* For debug / external output via coqtop.byte + Drop : *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6645f1d5d..5b31db3f9 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -192,7 +192,7 @@ let parse_ind_args si args relmax = in parse 1 1 si let oib_equal o1 o2 = - id_ord o1.mind_typename o2.mind_typename = 0 && + Id.compare o1.mind_typename o2.mind_typename = 0 && List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && begin match o1.mind_arity, o2.mind_arity with | Monomorphic {mind_user_arity=c1; mind_sort=s1}, diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 1eb9ca8e5..3a5fc9794 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -19,7 +19,7 @@ val extract_constant : env -> constant -> constant_body -> ml_decl val extract_constant_spec : env -> constant -> constant_body -> ml_spec -val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option +val extract_with_type : env -> constant_body -> ( Id.t list * ml_type ) option val extract_fixpoint : env -> constant array -> (constr, types) prec_declaration -> ml_decl diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index bdb102b18..5295e2cf9 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -33,7 +33,7 @@ let pr_int_or_id _ _ _ = function ARGUMENT EXTEND int_or_id TYPED AS int_or_id PRINTED BY pr_int_or_id -| [ preident(id) ] -> [ ArgId (id_of_string id) ] +| [ preident(id) ] -> [ ArgId (Id.of_string id) ] | [ integer(i) ] -> [ ArgInt i ] END diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 5de13e53c..3925a2a2f 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -21,16 +21,16 @@ open Common (*s Haskell renaming issues. *) -let pr_lower_id id = str (String.uncapitalize (string_of_id id)) -let pr_upper_id id = str (String.capitalize (string_of_id id)) +let pr_lower_id id = str (String.uncapitalize (Id.to_string id)) +let pr_upper_id id = str (String.capitalize (Id.to_string id)) let keywords = - List.fold_right (fun s -> Idset.add (id_of_string s)) + List.fold_right (fun s -> Id.Set.add (Id.of_string s)) [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else"; "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__"; "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ] - Idset.empty + Id.Set.empty let pp_comment s = str "-- " ++ s ++ fnl () let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}" diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index d170acbb0..14a30ae79 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -65,11 +65,11 @@ type inductive_kind = *) type ml_ind_packet = { - ip_typename : identifier; - ip_consnames : identifier array; + ip_typename : Id.t; + ip_consnames : Id.t array; ip_logical : bool; ip_sign : signature; - ip_vars : identifier list; + ip_vars : Id.t list; ip_types : (ml_type list) array } @@ -91,8 +91,8 @@ type ml_ind = { type ml_ident = | Dummy - | Id of identifier - | Tmp of identifier + | Id of Id.t + | Tmp of Id.t (** We now store some typing information on constructors and cases to avoid type-unsafe optimisations. This will be @@ -116,7 +116,7 @@ and ml_ast = | MLcons of ml_type * global_reference * ml_ast list | MLtuple of ml_ast list | MLcase of ml_type * ml_ast * ml_branch array - | MLfix of int * identifier array * ml_ast array + | MLfix of int * Id.t array * ml_ast array | MLexn of string | MLdummy | MLaxiom @@ -133,13 +133,13 @@ and ml_pattern = type ml_decl = | Dind of mutual_inductive * ml_ind - | Dtype of global_reference * identifier list * ml_type + | Dtype of global_reference * Id.t list * ml_type | Dterm of global_reference * ml_ast * ml_type | Dfix of global_reference array * ml_ast array * ml_type array type ml_spec = | Sind of mutual_inductive * ml_ind - | Stype of global_reference * identifier list * ml_type option + | Stype of global_reference * Id.t list * ml_type option | Sval of global_reference * ml_type type ml_specif = @@ -154,8 +154,8 @@ and ml_module_type = | MTwith of ml_module_type * ml_with_declaration and ml_with_declaration = - | ML_With_type of identifier list * identifier list * ml_type - | ML_With_module of identifier list * module_path + | ML_With_type of Id.t list * Id.t list * ml_type + | ML_With_module of Id.t list * module_path and ml_module_sig = (label * ml_specif) list @@ -191,13 +191,13 @@ type unsafe_needs = { } type language_descr = { - keywords : Idset.t; + keywords : Id.Set.t; (* Concerning the source file *) file_suffix : string; (* the second argument is a comment to add to the preamble *) preamble : - identifier -> std_ppcmds option -> module_path list -> unsafe_needs -> + Id.t -> std_ppcmds option -> module_path list -> unsafe_needs -> std_ppcmds; pp_struct : ml_structure -> std_ppcmds; @@ -205,7 +205,7 @@ type language_descr = { sig_suffix : string option; (* the second argument is a comment to add to the preamble *) sig_preamble : - identifier -> std_ppcmds option -> module_path list -> unsafe_needs -> + Id.t -> std_ppcmds option -> module_path list -> unsafe_needs -> std_ppcmds; pp_sig : ml_signature -> std_ppcmds; diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 18c3f840e..d8d1d1eae 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -22,8 +22,8 @@ exception Impossible (*S Names operations. *) -let anonymous_name = id_of_string "x" -let dummy_name = id_of_string "_" +let anonymous_name = Id.of_string "x" +let dummy_name = Id.of_string "_" let anonymous = Id anonymous_name @@ -857,7 +857,7 @@ let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false let is_program_branch = function | Id id -> - let s = string_of_id id in + let s = Id.to_string id in let br = "program_branch_" in let n = String.length br in (try diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index be32ba6ed..1c70908b6 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -77,10 +77,10 @@ val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast (*s Special identifiers. [dummy_name] is to be used for dead code and will be printed as [_] in concrete (Caml) code. *) -val anonymous_name : identifier -val dummy_name : identifier -val id_of_name : name -> identifier -val id_of_mlid : ml_ident -> identifier +val anonymous_name : Id.t +val dummy_name : Id.t +val id_of_name : name -> Id.t +val id_of_mlid : ml_ident -> Id.t val tmp_id : ml_ident -> ml_ident (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 7640416fd..b8d75d445 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -24,7 +24,7 @@ open Common (*s Some utility functions. *) let pp_tvar id = - let s = string_of_id id in + let s = Id.to_string id in if String.length s < 2 || s.[1]<>'\'' then str ("'"^s) else str ("' "^s) @@ -48,7 +48,7 @@ let pp_letin pat def body = (*s Ocaml renaming issues. *) let keywords = - List.fold_right (fun s -> Idset.add (id_of_string s)) + List.fold_right (fun s -> Id.Set.add (Id.of_string s)) [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do"; "done"; "downto"; "else"; "end"; "exception"; "external"; "false"; "for"; "fun"; "function"; "functor"; "if"; "in"; "include"; @@ -57,7 +57,7 @@ let keywords = "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true"; "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod"; "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] - Idset.empty + Id.Set.empty let pp_open mp = str ("open "^ string_of_modfile mp ^"\n") diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index bfbcc7b0a..8125b4757 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -20,11 +20,11 @@ open Common (*s Scheme renaming issues. *) let keywords = - List.fold_right (fun s -> Idset.add (id_of_string s)) + List.fold_right (fun s -> Id.Set.add (Id.of_string s)) [ "define"; "let"; "lambda"; "lambdas"; "match"; "apply"; "car"; "cdr"; "error"; "delay"; "force"; "_"; "__"] - Idset.empty + Id.Set.empty let pp_comment s = str";; "++h 0 s++fnl () @@ -40,7 +40,7 @@ let preamble _ comment _ usf = (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ()) let pr_id id = - let s = string_of_id id in + let s = Id.to_string id in for i = 0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done; diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index dd3b65b90..c7d8d42de 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -56,7 +56,7 @@ let is_modfile = function | _ -> false let raw_string_of_modfile = function - | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f))) + | MPfile f -> String.capitalize (Id.to_string (List.hd (repr_dirpath f))) | _ -> assert false let current_toplevel () = fst (Lib.current_prefix ()) @@ -256,8 +256,8 @@ let safe_basename_of_global r = | VarRef _ -> assert false let string_of_global r = - try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) - with _ -> string_of_id (safe_basename_of_global r) + try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r) + with _ -> Id.to_string (safe_basename_of_global r) let safe_pr_global r = str (string_of_global r) @@ -273,7 +273,7 @@ let safe_pr_long_global r = let pr_long_mp mp = let lid = repr_dirpath (Nametab.dirpath_of_module mp) in - str (String.concat "." (List.map string_of_id (List.rev lid))) + str (String.concat "." (List.map Id.to_string (List.rev lid))) let pr_long_global ref = pr_path (Nametab.path_of_global ref) @@ -411,7 +411,7 @@ let error_MPfile_as_mod mp b = let msg_non_implicit r n id = let name = match id with | Anonymous -> "" - | Name id -> "(" ^ string_of_id id ^ ") " + | Name id -> "(" ^ Id.to_string id ^ ") " in "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r) @@ -652,7 +652,7 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) (*s Extraction Implicit *) -type int_or_id = ArgInt of int | ArgId of identifier +type int_or_id = ArgInt of int | ArgId of Id.t let implicits_table = ref Refmap'.empty @@ -704,21 +704,21 @@ let extraction_implicit r l = (*s Extraction Blacklist of filenames not to use while extracting *) -let blacklist_table = ref Idset.empty +let blacklist_table = ref Id.Set.empty let modfile_ids = ref [] let modfile_mps = ref MPmap.empty let reset_modfile () = - modfile_ids := Idset.elements !blacklist_table; + modfile_ids := Id.Set.elements !blacklist_table; modfile_mps := MPmap.empty let string_of_modfile mp = try MPmap.find mp !modfile_mps with Not_found -> - let id = id_of_string (raw_string_of_modfile mp) in + let id = Id.of_string (raw_string_of_modfile mp) in let id' = next_ident_away id !modfile_ids in - let s' = string_of_id id' in + let s' = Id.to_string id' in modfile_ids := id' :: !modfile_ids; modfile_mps := MPmap.add mp s' !modfile_mps; s' @@ -727,7 +727,7 @@ let string_of_modfile mp = let file_of_modfile mp = let s0 = match mp with - | MPfile f -> string_of_id (List.hd (repr_dirpath f)) + | MPfile f -> Id.to_string (List.hd (repr_dirpath f)) | _ -> assert false in let s = String.copy (string_of_modfile mp) in @@ -736,7 +736,7 @@ let file_of_modfile mp = let add_blacklist_entries l = blacklist_table := - List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s))) + List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s))) l !blacklist_table (* Registration of operations for rollback. *) @@ -752,26 +752,26 @@ let blacklist_extraction : string list -> obj = let _ = declare_summary "Extraction Blacklist" { freeze_function = (fun () -> !blacklist_table); unfreeze_function = ((:=) blacklist_table); - init_function = (fun () -> blacklist_table := Idset.empty) } + init_function = (fun () -> blacklist_table := Id.Set.empty) } (* Grammar entries. *) let extraction_blacklist l = - let l = List.rev_map string_of_id l in + let l = List.rev_map Id.to_string l in Lib.add_anonymous_leaf (blacklist_extraction l) (* Printing part *) let print_extraction_blacklist () = - prlist_with_sep fnl pr_id (Idset.elements !blacklist_table) + prlist_with_sep fnl pr_id (Id.Set.elements !blacklist_table) (* Reset part *) let reset_blacklist : unit -> obj = declare_object {(default_object "Reset Extraction Blacklist") with - cache_function = (fun (_,_)-> blacklist_table := Idset.empty); - load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)} + cache_function = (fun (_,_)-> blacklist_table := Id.Set.empty); + load_function = (fun _ (_,_)-> blacklist_table := Id.Set.empty)} let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ()) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 16c2275f1..fbf48889f 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -15,7 +15,7 @@ open Declarations module Refset' : Set.S with type elt = global_reference module Refmap' : Map.S with type key = global_reference -val safe_basename_of_global : global_reference -> identifier +val safe_basename_of_global : global_reference -> Id.t (*s Warning and Error messages. *) @@ -30,7 +30,7 @@ val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : module_path -> module_path -> 'a val error_no_module_expr : module_path -> 'a -val error_singleton_become_prop : identifier -> 'a +val error_singleton_become_prop : Id.t -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a @@ -193,12 +193,12 @@ val extract_inductive : reference -> string -> string list -> string option -> unit -type int_or_id = ArgInt of int | ArgId of identifier +type int_or_id = ArgInt of int | ArgId of Id.t val extraction_implicit : reference -> int_or_id list -> unit (*s Table of blacklisted filenames *) -val extraction_blacklist : identifier list -> unit +val extraction_blacklist : Id.t list -> unit val reset_extraction_blacklist : unit -> unit val print_extraction_blacklist : unit -> Pp.std_ppcmds diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index d224f87df..093087511 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -116,7 +116,7 @@ type side = Hyp | Concl | Hint let no_atoms = (false,{positive=[];negative=[]}) -let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *) +let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *) let build_atoms gl metagen side cciterm = let trivial =ref false diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 753fdda72..48e60d798 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -25,7 +25,7 @@ let update_flags ()= red_flags:= Closure.RedFlags.red_add_transparent Closure.betaiotazeta - (Names.Idpred.full,Names.Cpred.complement !predref) + (Names.Id.Pred.full,Names.Cpred.complement !predref) let ground_tac solver startseq gl= update_flags (); diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 414afad46..c7a582a0e 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -98,7 +98,7 @@ let rec collect_quantified seq= let dummy_constr=mkMeta (-1) -let dummy_bvid=id_of_string "x" +let dummy_bvid=Id.of_string "x" let mk_open_instance id gl m t= let env=pf_env gl in diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 78a70ff51..bfebbaaf8 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -19,7 +19,7 @@ type 'a with_backtracking = tactic -> 'a val wrap : int -> bool -> seqtac -val basename_of_global: global_reference -> identifier +val basename_of_global: global_reference -> Id.t val clear_global: global_reference -> tactic diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 429a0a4a8..f8b1927a3 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -463,7 +463,7 @@ let mkAppL a = let rec fourier gl= Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; let goal = strip_outer_cast (pf_concl gl) in - let fhyp=id_of_string "new_hyp_for_fourier" in + let fhyp=Id.of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) try (let tac = diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c129306d2..ca73799c1 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -105,17 +105,17 @@ let make_refl_eq constructor type_of_t t = type pte_info = { - proving_tac : (identifier list -> Tacmach.tactic); + proving_tac : (Id.t list -> Tacmach.tactic); is_valid : constr -> bool } -type ptes_info = pte_info Idmap.t +type ptes_info = pte_info Id.Map.t type 'a dynamic_info = { nb_rec_hyps : int; - rec_hyps : identifier list ; - eq_hyps : identifier list; + rec_hyps : Id.t list ; + eq_hyps : Id.t list; info : 'a } @@ -361,7 +361,7 @@ let is_property (ptes_info:ptes_info) t_x full_type_of_hyp = if isVar pte && Array.for_all closed0 args then try - let info = Idmap.find (destVar pte) ptes_info in + let info = Id.Map.find (destVar pte) ptes_info in info.is_valid full_type_of_hyp with Not_found -> false else false @@ -406,7 +406,7 @@ let rewrite_until_var arg_num eq_ids : tactic = do_rewrite eq_ids -let rec_pte_id = id_of_string "Hrec" +let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let coq_False = Coqlib.build_coq_False () in let coq_True = Coqlib.build_coq_True () in @@ -430,7 +430,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = if is_property ptes_infos t_x actual_real_type_of_hyp then begin let pte,pte_args = (destApp t_x) in - let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in + let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar pte) ptes_infos).proving_tac in let popped_t' = Termops.pop t' in let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in let prove_new_type_of_hyp = @@ -579,7 +579,7 @@ let clean_goal_with_heq ptes_infos continue_tac (dyn_infos:body_info) = ] g -let heq_id = id_of_string "Heq" +let heq_id = Id.of_string "Heq" let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = fun g -> @@ -632,7 +632,7 @@ let my_orelse tac1 tac2 g = (* observe (str "using snd tac since : " ++ Errors.print e); *) tac2 g -let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = +let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = let args = Array.of_list (List.map mkVar args_id) in let instanciate_one_hyp hid = my_orelse @@ -672,10 +672,10 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id tclMAP instanciate_one_hyp hyps; (fun g -> let all_g_hyps_id = - List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty + List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in let remaining_hyps = - List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps + List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps in do_prove remaining_hyps g ) @@ -885,7 +885,7 @@ let build_proof type static_fix_info = { idx : int; - name : identifier; + name : Id.t; types : types; offset : int; nb_realargs : int; @@ -1042,7 +1042,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : (fun na -> let new_id = match na with - Name id -> fresh_id !avoid (string_of_id id) + Name id -> fresh_id !avoid (Id.to_string id) | Anonymous -> fresh_id !avoid "H" in avoid := new_id :: !avoid; @@ -1183,14 +1183,14 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in (* observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++ *) (* str " to " ++ Ppconstr.pr_id info.name); *) - (Idmap.add (Nameops.out_name pte) info acc_map,info::acc_info) + (Id.Map.add (Nameops.out_name pte) info acc_map,info::acc_info) ) 0 - (Idmap.empty,[]) + (Id.Map.empty,[]) (List.rev princ_info.predicates) in pte_to_fix,List.rev rev_info - | _ -> Idmap.empty,[] + | _ -> Id.Map.empty,[] in let mk_fixes : tactic = let pre_info,infos = list_chop fun_num infos in @@ -1224,7 +1224,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let pte,pte_args = (decompose_app pte_app) in try let pte = try destVar pte with _ -> anomaly "Property is not a variable" in - let fix_info = Idmap.find pte ptes_to_fix in + let fix_info = Id.Map.find pte ptes_to_fix in let nb_args = fix_info.nb_realargs in tclTHENSEQ [ @@ -1262,7 +1262,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : build_proof interactive_proof (Array.to_list fnames) - (Idmap.map prove_rec_hyp ptes_to_fix) + (Id.Map.map prove_rec_hyp ptes_to_fix) in let prove_tac branches = let dyn_infos = @@ -1272,7 +1272,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : } in observe_tac "cleaning" (clean_goal_with_heq - (Idmap.map prove_rec_hyp ptes_to_fix) + (Id.Map.map prove_rec_hyp ptes_to_fix) do_prove dyn_infos) in @@ -1316,7 +1316,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : build_proof interactive_proof (Array.to_list fnames) - (Idmap.map prove_rec_hyp ptes_to_fix) + (Id.Map.map prove_rec_hyp ptes_to_fix) in let prove_tac branches = let dyn_infos = @@ -1326,7 +1326,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : } in clean_goal_with_heq - (Idmap.map prove_rec_hyp ptes_to_fix) + (Id.Map.map prove_rec_hyp ptes_to_fix) do_prove dyn_infos in @@ -1413,7 +1413,7 @@ let rec rewrite_eqs_in_eqs eqs = (tclMAP (fun id gl -> observe_tac - (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) + (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id)) (tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true (* dep proofs also: *) true id (mkVar eq) false)) gl @@ -1427,7 +1427,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = (tclTHENSEQ [ backtrack_eqs_until_hrec hrec eqs; - (* observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" ) *) + (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *) (tclTHENS (* We must have exactly ONE subgoal !*) (apply (mkVar hrec)) [ tclTHENSEQ @@ -1463,13 +1463,13 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = let is_valid_hypothesis predicates_name = - let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in + let predicates_name = List.fold_right Id.Set.add predicates_name Id.Set.empty in let is_pte typ = if isApp typ then let pte,_ = destApp typ in if isVar pte - then Idset.mem (destVar pte) predicates_name + then Id.Set.mem (destVar pte) predicates_name else false else false in @@ -1491,7 +1491,7 @@ let prove_principle_for_gen fun na -> let new_id = match na with - | Name id -> fresh_id !avoid (string_of_id id) + | Name id -> fresh_id !avoid (Id.to_string id) | Anonymous -> fresh_id !avoid "H" in avoid := new_id :: !avoid; @@ -1534,9 +1534,9 @@ let prove_principle_for_gen let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in - let wf_thm_id = Nameops.out_name (fresh_id (Name (id_of_string "wf_R"))) in + let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in let acc_rec_arg_id = - Nameops.out_name (fresh_id (Name (id_of_string ("Acc_"^(string_of_id rec_arg_id))))) + Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) in let revert l = tclTHEN (h_generalize (List.map mkVar l)) (clear l) @@ -1580,7 +1580,7 @@ let prove_principle_for_gen let hyps = pf_ids_of_hyps gls in let hid = next_ident_away_in_goal - (id_of_string "prov") + (Id.of_string "prov") hyps in tclTHENSEQ @@ -1669,14 +1669,14 @@ let prove_principle_for_gen is_valid = is_valid_hypothesis predicates_names } in - let ptes_info : pte_info Idmap.t = + let ptes_info : pte_info Id.Map.t = List.fold_left (fun map pte_id -> - Idmap.add pte_id + Id.Map.add pte_id pte_info map ) - Idmap.empty + Id.Map.empty predicates_names in let make_proof rec_hyps = diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 533fbfaaa..1d30ce9a6 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -41,7 +41,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let env = Global.env () in let env_with_params = Environ.push_rel_context princ_type_info.params env in let tbl = Hashtbl.create 792 in - let rec change_predicates_names (avoid:identifier list) (predicates:rel_context) : rel_context = + let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context) : rel_context = match predicates with | [] -> [] |(Name x,v,t)::predicates -> @@ -83,10 +83,10 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in let is_pte = - let set = List.fold_right Idset.add ptes_vars Idset.empty in + let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in fun t -> match kind_of_term t with - | Var id -> Idset.mem id set + | Var id -> Id.Set.mem id set | _ -> false in let pre_princ = @@ -114,7 +114,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Construct((_,num),_) -> num | _ -> assert false in - let dummy_var = mkVar (id_of_string "________") in + let dummy_var = mkVar (Id.of_string "________") in let mk_replacement c i args = let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in (* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *) @@ -284,7 +284,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *) observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); let new_princ_name = - next_ident_away_in_goal (id_of_string "___________princ_________") [] + next_ident_away_in_goal (Id.of_string "___________princ_________") [] in begin Lemmas.start_proof @@ -366,7 +366,7 @@ let generate_functional_principle begin try let id = Pfedit.get_current_proof_name () in - let s = string_of_id id in + let s = Id.to_string id in let n = String.length "___________princ_________" in if String.length s >= n then if String.sub s 0 n = "___________princ_________" @@ -519,7 +519,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis begin try let id = Pfedit.get_current_proof_name () in - let s = string_of_id id in + let s = Id.to_string id in let n = String.length "___________princ_________" in if String.length s >= n then if String.sub s 0 n = "___________princ_________" diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 00d130d28..a16b834f8 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -10,7 +10,7 @@ val generate_functional_principle : (* *) sorts array option -> (* Name of the new principle *) - (identifier) option -> + (Id.t) option -> (* the compute functions to use *) constant array -> (* We prove the nth- principle *) @@ -29,6 +29,6 @@ exception No_graph_found val make_scheme : (constant*glob_sort) list -> Entries.definition_entry list -val build_scheme : (identifier*Libnames.reference*glob_sort) list -> unit -val build_case_scheme : (identifier*Libnames.reference*glob_sort) -> unit +val build_scheme : (Id.t*Libnames.reference*glob_sort) list -> unit +val build_case_scheme : (Id.t*Libnames.reference*glob_sort) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 2fdf62d26..ef2276134 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -368,7 +368,7 @@ let find_fapp (test:constr -> bool) g : fapp_info list = an occurence of function [id] in the conclusion of goal [g]. If [id]=[None] then calls to any function are selected. In any case [heuristic] is used to select the most pertinent occurrence. *) -let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list) +let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list) (nexttac:Proof_type.tactic) g = let test = match oid with | Some id -> @@ -468,10 +468,10 @@ VERNAC COMMAND EXTEND MergeFunind let ar2 = List.length (fst (decompose_prod f2type)) in let _ = if ar1 <> List.length cl1 then - Errors.error ("not the right number of arguments for " ^ string_of_id id1) in + Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in let _ = if ar2 <> List.length cl2 then - Errors.error ("not the right number of arguments for " ^ string_of_id id2) in + Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id ] END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 593e274fb..cf7d8e8fe 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -57,7 +57,7 @@ type 'a build_entry_pre_return = type 'a build_entry_return = { result : 'a build_entry_pre_return list; - to_avoid : identifier list + to_avoid : Id.t list } (* @@ -114,9 +114,9 @@ let ids_of_binder = function let rec change_vars_in_binder mapping = function [] -> [] | (bt,t)::l -> - let new_mapping = List.fold_right Idmap.remove (ids_of_binder bt) mapping in + let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in (bt,change_vars mapping t):: - (if idmap_is_empty new_mapping + (if Id.Map.is_empty new_mapping then l else change_vars_in_binder new_mapping l ) @@ -138,23 +138,23 @@ let apply_args ctxt body args = let need_convert avoid bt = List.exists (need_convert_id avoid) (ids_of_binder bt) in - let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) = + let next_name_away (na:name) (mapping: Id.t Id.Map.t) (avoid: Id.t list) = match na with | Name id when List.mem id avoid -> let new_id = Namegen.next_ident_away id avoid in - Name new_id,Idmap.add id new_id mapping,new_id::avoid + Name new_id,Id.Map.add id new_id mapping,new_id::avoid | _ -> na,mapping,avoid in - let next_bt_away bt (avoid:identifier list) = + let next_bt_away bt (avoid:Id.t list) = match bt with | LetIn na -> - let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in + let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in LetIn new_na,mapping,new_avoid | Prod na -> - let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in + let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in Prod new_na,mapping,new_avoid | Lambda na -> - let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in + let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in Lambda new_na,mapping,new_avoid in let rec do_apply avoid ctxt body args = @@ -173,7 +173,7 @@ let apply_args ctxt body args = let new_avoid = id::avoid in let new_id = Namegen.next_ident_away id new_avoid in let new_avoid' = new_id :: new_avoid in - let mapping = Idmap.add id new_id Idmap.empty in + let mapping = Id.Map.add id new_id Id.Map.empty in let new_ctxt' = change_vars_in_binder mapping ctxt' in let new_body = change_vars mapping body in new_avoid',new_ctxt',new_body,new_id @@ -477,7 +477,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = GApp(Loc.ghost,t,l) in build_entry_lc env funnames avoid (aux f args) - | GVar(_,id) when Idset.mem id funnames -> + | GVar(_,id) when Id.Set.mem id funnames -> (* if we have [f t1 ... tn] with [f]$\in$[fnames] then we create a fresh variable [res], add [res] and its "value" (i.e. [res v1 ... vn]) to each @@ -725,7 +725,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (will be used in the following recursive calls) *) let new_env = List.fold_right2 add_pat_variables patl types env in - let not_those_patterns : (identifier list -> glob_constr -> glob_constr) list = + let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list = List.map2 (fun pat typ -> fun avoid pat'_as_term -> @@ -787,7 +787,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let pat_as_term = pattern_to_term pat in List.fold_right (fun id acc -> - if Idset.mem id this_pat_ids + if Id.Set.mem id this_pat_ids then (Prod (Name id), let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in let raw_typ_of_id = @@ -835,7 +835,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let is_res id = try - String.sub (string_of_id id) 0 4 = "_res" + String.sub (Id.to_string id) 0 4 = "_res" with Invalid_argument _ -> false @@ -901,7 +901,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (depth + 1) b in mkGProd(n,new_t,new_b), - Idset.filter not_free_in_t id_to_exclude + Id.Set.filter not_free_in_t id_to_exclude | _ -> (* the first args is the name of the function! *) assert false end @@ -1019,7 +1019,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* J.F:. keep this comment it explain how to remove some meaningless equalities if keep_eq then mkGProd(n,t,new_b),id_to_exclude - else new_b, Idset.add id id_to_exclude + else new_b, Id.Set.add id id_to_exclude *) | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2]) when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous @@ -1051,10 +1051,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (depth + 1) b in match n with - | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> - new_b,Idset.remove id - (Idset.filter not_free_in_t id_to_exclude) - | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude + | 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) + | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); @@ -1067,10 +1067,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (depth + 1) b in match n with - | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> - new_b,Idset.remove id - (Idset.filter not_free_in_t id_to_exclude) - | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude + | 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) + | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end | GLambda(_,n,k,t,b) -> begin @@ -1087,11 +1087,11 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (args@[mkGVar id])new_crossed_types (depth + 1 ) b in - if Idset.mem id id_to_exclude && depth >= nb_args + if Id.Set.mem id id_to_exclude && depth >= nb_args then - new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude) + new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else - GProd(Loc.ghost,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude + GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude | _ -> anomaly "Should not have an anonymous function here" (* We have renamed all the anonymous functions during alpha_renaming phase *) @@ -1108,10 +1108,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = args (t::crossed_types) (depth + 1 ) b in match n with - | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> - new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) + | 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) | _ -> GLetIn(Loc.ghost,n,t,new_b), - Idset.filter not_free_in_t id_to_exclude + Id.Set.filter not_free_in_t id_to_exclude end | GLetTuple(_,nal,(na,rto),t,b) -> assert (rto=None); @@ -1133,15 +1133,15 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (depth + 1) b in (* match n with *) -(* | Name id when Idset.mem id id_to_exclude -> *) -(* new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *) +(* | 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) *) (* | _ -> *) GLetTuple(Loc.ghost,nal,(na,None),t,new_b), - Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude') + Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') end - | _ -> mkGApp(mkGVar relname,args@[rt]),Idset.empty + | _ -> mkGApp(mkGVar relname,args@[rt]),Id.Set.empty (* debuging wrapper *) @@ -1164,7 +1164,7 @@ let rebuild_cons env nb_args relname args crossed_types rt = *) let rec compute_cst_params relnames params = function | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp(_,GVar(_,relname'),rtl) when Idset.mem relname' relnames -> + | GApp(_,GVar(_,relname'),rtl) when Id.Set.mem relname' relnames -> compute_cst_params_from_app [] (params,rtl) | GApp(_,f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) @@ -1182,7 +1182,7 @@ and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl' - when id_ord id id' == 0 && not is_defined -> + when Id.compare id id' == 0 && not is_defined -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc @@ -1233,7 +1233,7 @@ let do_build_inductive (rtl:glob_constr list) = let _time1 = System.get_time () in (* Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *) - let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in + let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in let funnames = Array.of_list funnames in let funsargs = Array.of_list funsargs in let returned_types = Array.of_list returned_types in @@ -1244,7 +1244,7 @@ let do_build_inductive Ensures by: obvious i*) let relnames = Array.map mk_rel_id funnames in - let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in + let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in (* Construction of the pseudo constructors *) let env = Array.fold_right @@ -1264,12 +1264,12 @@ let do_build_inductive (fun (n,t,is_defined) acc -> if is_defined then - Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Idset.empty t, + Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t, acc) else Constrexpr.CProdN (Loc.ghost, - [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], + [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t], acc ) ) @@ -1307,9 +1307,9 @@ let do_build_inductive (*i The next call to mk_rel_id is valid since we are constructing the graph Ensures by: obvious i*) - id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id)) + Id.of_string ((Id.to_string (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id)) in - let rel_constructors i rt : (identifier*glob_constr) list = + let rel_constructors i rt : (Id.t*glob_constr) list = next_constructor_id := (-1); List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt) in @@ -1330,12 +1330,12 @@ let do_build_inductive (fun (n,t,is_defined) acc -> if is_defined then - Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Idset.empty t, + Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t, acc) else Constrexpr.CProdN (Loc.ghost, - [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], + [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t], acc ) ) @@ -1352,10 +1352,10 @@ let do_build_inductive (fun (n,t,is_defined) -> if is_defined then - Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Idset.empty t) + Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t) else Constrexpr.LocalRawAssum - ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t) + ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) rels_params in @@ -1365,7 +1365,7 @@ let do_build_inductive false,((Loc.ghost,id), Flags.with_option Flags.raw_print - (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t) + (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) t) ) )) (rel_constructors) diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index b8e7b3ab4..87fcb1022 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -8,7 +8,7 @@ *) val build_inductive : - Names.identifier list -> (* The list of function name *) + Names.Id.t list -> (* The list of function name *) (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *) Constrexpr.constr_expr list -> (* The list of function returned type *) Glob_term.glob_constr list -> (* the list of body *) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index f678b898b..7785cbe59 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -6,9 +6,6 @@ open Names open Decl_kinds open Misctypes -(* Ocaml 3.06 Map.S does not handle is_empty *) -let idmap_is_empty m = m = Idmap.empty - (* Some basic functions to rebuild glob_constr In each of them the location is Loc.ghost @@ -119,7 +116,7 @@ let rec glob_make_or_list = function let remove_name_from_mapping mapping na = match na with | Anonymous -> mapping - | Name id -> Idmap.remove id mapping + | Name id -> Id.Map.remove id mapping let change_vars = let rec change_vars mapping rt = @@ -128,7 +125,7 @@ let change_vars = | GVar(loc,id) -> let new_id = try - Idmap.find id mapping + Id.Map.find id mapping with Not_found -> id in GVar(loc,new_id) @@ -187,8 +184,8 @@ let change_vars = GCast(loc,change_vars mapping b, Miscops.map_cast_type (change_vars mapping) c) and change_vars_br mapping ((loc,idl,patl,res) as br) = - let new_mapping = List.fold_right Idmap.remove idl mapping in - if idmap_is_empty new_mapping + let new_mapping = List.fold_right Id.Map.remove idl mapping in + if Id.Map.is_empty new_mapping then br else (loc,idl,patl,change_vars new_mapping res) in @@ -200,27 +197,27 @@ let rec alpha_pat excluded pat = match pat with | PatVar(loc,Anonymous) -> let new_id = Indfun_common.fresh_id excluded "_x" in - PatVar(loc,Name new_id),(new_id::excluded),Idmap.empty + PatVar(loc,Name new_id),(new_id::excluded),Id.Map.empty | PatVar(loc,Name id) -> if List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in PatVar(loc,Name new_id),(new_id::excluded), - (Idmap.add id new_id Idmap.empty) - else pat,excluded,Idmap.empty + (Id.Map.add id new_id Id.Map.empty) + else pat,excluded,Id.Map.empty | PatCstr(loc,constr,patl,na) -> let new_na,new_excluded,map = match na with | Name id when List.mem id excluded -> let new_id = Namegen.next_ident_away id excluded in - Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty - | _ -> na,excluded,Idmap.empty + Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty + | _ -> na,excluded,Id.Map.empty in let new_patl,new_excluded,new_map = List.fold_left (fun (patl,excluded,map) pat -> let new_pat,new_excluded,new_map = alpha_pat excluded pat in - (new_pat::patl,new_excluded,Idmap.fold Idmap.add new_map map) + (new_pat::patl,new_excluded,Id.Map.fold Id.Map.add new_map map) ) ([],new_excluded,map) patl @@ -232,9 +229,9 @@ let alpha_patl excluded patl = List.fold_left (fun (patl,excluded,map) pat -> let new_pat,new_excluded,new_map = alpha_pat excluded pat in - new_pat::patl,new_excluded,(Idmap.fold Idmap.add new_map map) + new_pat::patl,new_excluded,(Id.Map.fold Id.Map.add new_map map) ) - ([],excluded,Idmap.empty) + ([],excluded,Id.Map.empty) patl in (List.rev patl,new_excluded,map) @@ -266,7 +263,7 @@ let rec alpha_rt excluded rt = match rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt | GLambda(loc,Anonymous,k,t,b) -> - let new_id = Namegen.next_ident_away (id_of_string "_x") excluded in + let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in let new_excluded = new_id :: excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in @@ -285,7 +282,7 @@ let rec alpha_rt excluded rt = if new_id = id then t,b else - let replace = change_vars (Idmap.add id new_id Idmap.empty) in + let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in (t,replace b) in let new_excluded = new_id::excluded in @@ -299,7 +296,7 @@ let rec alpha_rt excluded rt = if new_id = id then t,b else - let replace = change_vars (Idmap.add id new_id Idmap.empty) in + let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in (t,replace b) in let new_t = alpha_rt new_excluded t in @@ -311,7 +308,7 @@ let rec alpha_rt excluded rt = if new_id = id then t,b else - let replace = change_vars (Idmap.add id new_id Idmap.empty) in + let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in (t,replace b) in let new_excluded = new_id::excluded in @@ -332,14 +329,14 @@ let rec alpha_rt excluded rt = then na::nal,id::excluded,mapping else - (Name new_id)::nal,id::excluded,(Idmap.add id new_id mapping) + (Name new_id)::nal,id::excluded,(Id.Map.add id new_id mapping) ) - ([],excluded,Idmap.empty) + ([],excluded,Id.Map.empty) nal in let new_nal = List.rev rev_new_nal in let new_rto,new_t,new_b = - if idmap_is_empty mapping + if Id.Map.is_empty mapping then rto,t,b else let replace = change_vars mapping in (Option.map replace rto, t,replace b) @@ -387,14 +384,14 @@ and alpha_br excluded (loc,ids,patl,res) = let is_free_in id = let rec is_free_in = function | GRef _ -> false - | GVar(_,id') -> id_ord id' id == 0 + | GVar(_,id') -> Id.compare id' id == 0 | GEvar _ -> false | GPatVar _ -> false | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) -> let check_in_b = match n with - | Name id' -> id_ord id' id <> 0 + | Name id' -> Id.compare id' id <> 0 | _ -> true in is_free_in t || (check_in_b && is_free_in b) @@ -451,7 +448,7 @@ let replace_var_by_term x_id term = let rec replace_var_by_pattern rt = match rt with | GRef _ -> rt - | GVar(_,id) when id_ord id x_id == 0 -> term + | GVar(_,id) when Id.compare id x_id == 0 -> term | GVar _ -> rt | GEvar _ -> rt | GPatVar _ -> rt @@ -460,7 +457,7 @@ let replace_var_by_term x_id term = replace_var_by_pattern rt', List.map replace_var_by_pattern rtl ) - | GLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | GLambda(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt | GLambda(loc,name,k,t,b) -> GLambda(loc, name, @@ -468,7 +465,7 @@ let replace_var_by_term x_id term = replace_var_by_pattern t, replace_var_by_pattern b ) - | GProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | GProd(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt | GProd(loc,name,k,t,b) -> GProd(loc, name, @@ -476,7 +473,7 @@ let replace_var_by_term x_id term = replace_var_by_pattern t, replace_var_by_pattern b ) - | GLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt + | GLetIn(_,Name id,_,_) when Id.compare id x_id == 0 -> rt | GLetIn(loc,name,def,b) -> GLetIn(loc, name, @@ -512,7 +509,7 @@ let replace_var_by_term x_id term = GCast(loc,replace_var_by_pattern b, Miscops.map_cast_type replace_var_by_pattern c) and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = - if List.exists (fun id -> id_ord id x_id == 0) idl + if List.exists (fun id -> Id.compare id x_id == 0) idl then br else (loc,idl,patl,replace_var_by_pattern res) in @@ -573,13 +570,13 @@ let eq_cases_pattern pat1 pat2 = let ids_of_pat = let rec ids_of_pat ids = function | PatVar(_,Anonymous) -> ids - | PatVar(_,Name id) -> Idset.add id ids + | PatVar(_,Name id) -> Id.Set.add id ids | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl in - ids_of_pat Idset.empty + ids_of_pat Id.Set.empty let id_of_name = function - | Names.Anonymous -> id_of_string "x" + | Names.Anonymous -> Id.of_string "x" | Names.Name x -> x (* TODO: finish Rec caes *) @@ -604,7 +601,7 @@ let ids_of_glob_constr c = | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> [] in (* build the set *) - List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_glob_constr [] c) + List.fold_left (fun acc x -> Id.Set.add x acc) Id.Set.empty (ids_of_glob_constr [] c) @@ -678,7 +675,7 @@ let expand_as = match pat with | PatVar _ -> map | PatCstr(_,_,patl,Name id) -> - Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl) + Id.Map.add id (pattern_to_term pat) (List.fold_left add_as map patl) | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl in let rec expand_as map rt = @@ -687,7 +684,7 @@ let expand_as = | GVar(_,id) -> begin try - Idmap.find id map + Id.Map.find id map with Not_found -> rt end | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) @@ -710,4 +707,4 @@ let expand_as = and expand_as_br map (loc,idl,cpl,rt) = (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) in - expand_as Idmap.empty + expand_as Id.Map.empty diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 9cf83df15..55d793e03 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,12 +1,8 @@ open Glob_term open Misctypes -(* Ocaml 3.06 Map.S does not handle is_empty *) -val idmap_is_empty : 'a Names.Idmap.t -> bool - - (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) -val get_pattern_id : cases_pattern -> Names.identifier list +val get_pattern_id : cases_pattern -> Names.Id.t list (* [pattern_to_term pat] returns a glob_constr corresponding to [pat]. [pat] must not contain occurences of anonymous pattern @@ -18,7 +14,7 @@ val pattern_to_term : cases_pattern -> glob_constr In each of them the location is Util.Loc.ghost *) val mkGRef : Globnames.global_reference -> glob_constr -val mkGVar : Names.identifier -> glob_constr +val mkGVar : Names.Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr val mkGProd : Names.name * glob_constr * glob_constr -> glob_constr @@ -61,7 +57,7 @@ val glob_make_or_list : glob_constr list -> glob_constr (* Replace the var mapped in the glob_constr/context *) -val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr +val change_vars : Names.Id.t Names.Id.Map.t -> glob_constr -> glob_constr @@ -73,27 +69,27 @@ val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr [avoid] with the variables appearing in the result. *) val alpha_pat : - Names.Idmap.key list -> + Names.Id.Map.key list -> Glob_term.cases_pattern -> - Glob_term.cases_pattern * Names.Idmap.key list * - Names.identifier Names.Idmap.t + Glob_term.cases_pattern * Names.Id.Map.key list * + Names.Id.t Names.Id.Map.t (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt conventions and does not share bound variables with avoid *) -val alpha_rt : Names.identifier list -> glob_constr -> glob_constr +val alpha_rt : Names.Id.t list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) -val alpha_br : Names.identifier list -> - Loc.t * Names.identifier list * Glob_term.cases_pattern list * +val alpha_br : Names.Id.t list -> + Loc.t * Names.Id.t list * Glob_term.cases_pattern list * Glob_term.glob_constr -> - Loc.t * Names.identifier list * Glob_term.cases_pattern list * + Loc.t * Names.Id.t list * Glob_term.cases_pattern list * Glob_term.glob_constr (* Reduction function *) val replace_var_by_term : - Names.identifier -> + Names.Id.t -> Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr @@ -101,7 +97,7 @@ val replace_var_by_term : (* [is_free_in id rt] checks if [id] is a free variable in [rt] *) -val is_free_in : Names.identifier -> glob_constr -> bool +val is_free_in : Names.Id.t -> glob_constr -> bool val are_unifiable : cases_pattern -> cases_pattern -> bool @@ -110,13 +106,13 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool (* - ids_of_pat : cases_pattern -> Idset.t + ids_of_pat : cases_pattern -> Id.Set.t returns the set of variables appearing in a pattern *) -val ids_of_pat : cases_pattern -> Names.Idset.t +val ids_of_pat : cases_pattern -> Names.Id.Set.t (* TODO: finish this function (Fix not treated) *) -val ids_of_glob_constr: glob_constr -> Names.Idset.t +val ids_of_glob_constr: glob_constr -> Names.Id.Set.t (* removing let_in construction in a glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 22da1a966..f922b2f60 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -85,19 +85,19 @@ let functional_induction with_clean c princl pat = let princ_vars = List.fold_right (fun a acc -> - try Idset.add (destVar a) acc + try Id.Set.add (destVar a) acc with _ -> acc ) args - Idset.empty + Id.Set.empty in - let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in - let old_idl = Idset.diff old_idl princ_vars in + let old_idl = List.fold_right Id.Set.add (Tacmach.pf_ids_of_hyps g) Id.Set.empty in + let old_idl = Id.Set.diff old_idl princ_vars in let subst_and_reduce g = if with_clean then let idl = - List.filter (fun id -> not (Idset.mem id old_idl)) + List.filter (fun id -> not (Id.Set.mem id old_idl)) (Tacmach.pf_ids_of_hyps g) in let flag = @@ -152,7 +152,7 @@ let build_newrecursive let arityc = Constrexpr_ops.prod_constr_expr arityc bl in let arity = Constrintern.interp_type sigma env0 arityc in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in - (Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls)) + (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) @@ -185,8 +185,8 @@ let build_newrecursive l = (* Checks whether or not the mutual bloc is recursive *) let is_rec names = - let names = List.fold_right Idset.add names Idset.empty in - let check_id id names = Idset.mem id names in + let names = List.fold_right Id.Set.add names Id.Set.empty in + let check_id id names = Id.Set.mem id names in let rec lookup names = function | GVar(_,id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false @@ -195,11 +195,11 @@ let is_rec names = | GIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b) -> - lookup names t || lookup (Nameops.name_fold Idset.remove na names) b + lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b | GLetTuple(_,nal,_,t,b) -> lookup names t || lookup (List.fold_left - (fun acc na -> Nameops.name_fold Idset.remove na acc) + (fun acc na -> Nameops.name_fold Id.Set.remove na acc) names nal ) @@ -209,7 +209,7 @@ let is_rec names = List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl and lookup_br names (_,idl,_,rt) = - let new_names = List.fold_right Idset.remove idl names in + let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt in lookup names @@ -460,9 +460,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas match wf_rel_expr_opt with | None -> let ltof = - let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in + let make_dir l = make_dirpath (List.map Id.of_string (List.rev l)) in Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path - (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof"))) + (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) in let fun_from_mes = let applied_mes = @@ -475,8 +475,8 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas wf_rel_from_mes,true | Some wf_rel_expr -> let wf_rel_with_mes = - let a = Names.id_of_string "___a" in - let b = Names.id_of_string "___b" in + let a = Names.Id.of_string "___a" in + let b = Names.Id.of_string "___b" in Constrexpr_ops.mkLambdaC( [Loc.ghost,Name a;Loc.ghost,Name b], Constrexpr.Default Explicit, diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index fb9116cc2..2d50adf00 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -4,7 +4,7 @@ open Libnames open Globnames open Refiner open Hiddentac -let mk_prefix pre id = id_of_string (pre^(string_of_id id)) +let mk_prefix pre id = Id.of_string (pre^(Id.to_string id)) let mk_rel_id = mk_prefix "R_" let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct" let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete" @@ -16,7 +16,7 @@ let msgnl m = let invalid_argument s = raise (Invalid_argument s) -let fresh_id avoid s = Namegen.next_ident_away_in_goal (id_of_string s) avoid +let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid let fresh_name avoid s = Name (fresh_id avoid s) @@ -116,7 +116,7 @@ let const_of_id id = qualid_of_reference (Libnames.Ident (Loc.ghost,id)) in try Nametab.locate_constant princ_ref - with Not_found -> Errors.error ("cannot find "^ string_of_id id) + with Not_found -> Errors.error ("cannot find "^ Id.to_string id) let def_of_const t = match (Term.kind_of_term t) with @@ -133,8 +133,8 @@ let coq_constant s = let find_reference sl s = (Nametab.locate (make_qualid(Names.make_dirpath - (List.map id_of_string (List.rev sl))) - (id_of_string s)));; + (List.map Id.of_string (List.rev sl))) + (Id.of_string s)));; let eq = lazy(coq_constant "eq") let refl_equal = lazy(coq_constant "eq_refl") @@ -510,8 +510,8 @@ let jmeq_refl () = let h_intros l = tclMAP h_intro l -let h_id = id_of_string "h" -let hrec_id = id_of_string "hrec" +let h_id = Id.of_string "h" +let hrec_id = Id.of_string "hrec" let well_founded = function () -> (coq_constant "well_founded") let acc_rel = function () -> (coq_constant "Acc") let acc_inv_id = function () -> (coq_constant "Acc_inv") diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 8f80c072c..7d0f5a00e 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -5,23 +5,23 @@ open Pp The mk_?_id function build different name w.r.t. a function Each of their use is justified in the code *) -val mk_rel_id : identifier -> identifier -val mk_correct_id : identifier -> identifier -val mk_complete_id : identifier -> identifier -val mk_equation_id : identifier -> identifier +val mk_rel_id : Id.t -> Id.t +val mk_correct_id : Id.t -> Id.t +val mk_complete_id : Id.t -> Id.t +val mk_equation_id : Id.t -> Id.t val msgnl : std_ppcmds -> unit val invalid_argument : string -> 'a -val fresh_id : identifier list -> string -> identifier -val fresh_name : identifier list -> string -> name -val get_name : identifier list -> ?default:string -> name -> name +val fresh_id : Id.t list -> string -> Id.t +val fresh_name : Id.t list -> string -> name +val get_name : Id.t list -> ?default:string -> name -> name val array_get_start : 'a array -> 'a array -val id_of_name : name -> identifier +val id_of_name : name -> Id.t val locate_ind : Libnames.reference -> inductive val locate_constant : Libnames.reference -> constant @@ -44,7 +44,7 @@ val chop_rprod_n : int -> Glob_term.glob_constr -> val def_of_const : Term.constr -> Term.constr val eq : Term.constr Lazy.t val refl_equal : Term.constr Lazy.t -val const_of_id: identifier -> constant +val const_of_id: Id.t -> constant val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr @@ -54,14 +54,14 @@ val jmeq_refl : unit -> Term.constr val new_save_named : bool -> unit -val save : bool -> identifier -> Entries.definition_entry -> Decl_kinds.goal_kind -> +val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> unit Tacexpr.declaration_hook -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and abort the proof *) val get_proof_clean : bool -> - Names.identifier * + Names.Id.t * (Entries.definition_entry * Decl_kinds.goal_kind * unit Tacexpr.declaration_hook) @@ -113,9 +113,9 @@ exception ToShow of exn val is_strict_tcc : unit -> bool -val h_intros: Names.identifier list -> Proof_type.tactic -val h_id : Names.identifier -val hrec_id : Names.identifier +val h_intros: Names.Id.t list -> Proof_type.tactic +val h_id : Names.Id.t +val hrec_id : Names.Id.t val acc_inv_id : Term.constr Util.delayed val ltof_ref : Globnames.global_reference Util.delayed val well_founded_ltof : Term.constr Util.delayed diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 517a1ce9c..4a466175f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -126,8 +126,8 @@ let generate_type g_to_f f graph i = (*i We need to name the vars [res] and [fv] i*) let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in let named_ctxt = List.map_filter filter fun_ctxt in - let res_id = Namegen.next_ident_away_in_goal (id_of_string "_res") named_ctxt in - let fv_id = Namegen.next_ident_away_in_goal (id_of_string "fv") (res_id :: named_ctxt) in + let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in + let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in (*i we can then type the argument to be applied to the function [f] i*) let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in (*i @@ -242,13 +242,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let princ_infos = Tactics.compute_elim_sig princ_type in (* The number of args of the function is then easilly computable *) let nb_fun_args = nb_prod (pf_concl g) - 2 in - let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in + let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in (* Since we cannot ensure that the funcitonnal principle is defined in the environement and due to the bug #1174, we will need to pose the principle using a name *) - let principle_id = Namegen.next_ident_away_in_goal (id_of_string "princ") ids in + let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in let ids = principle_id :: ids in (* We get the branches of the principle *) let branches = List.rev princ_infos.branches in @@ -258,7 +258,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (fun (_,_,br_type) -> List.map (fun id -> Loc.ghost, IntroIdentifier id) - (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) + (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) ) branches in @@ -276,16 +276,16 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_right (fun (_,pat) acc -> match pat with - | Genarg.IntroIdentifier id -> Idset.add id acc + | Genarg.IntroIdentifier id -> Id.Set.add id acc | _ -> anomaly "Not an identifier" ) (List.nth intro_pats (pred i)) - Idset.empty + Id.Set.empty in let pre_args g = List.fold_right (fun (id,b,t) pre_args -> - if Idset.mem id this_branche_ids + if Id.Set.mem id this_branche_ids then match b with | None -> id::pre_args @@ -299,7 +299,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let pre_tac g = List.fold_right (fun (id,b,t) pre_tac -> - if Idset.mem id this_branche_ids + if Id.Set.mem id this_branche_ids then match b with | None -> pre_tac @@ -383,7 +383,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let app_constructor g = applist((mkConstruct(constructor)),constructor_args g) in (* an apply the tactic *) let res,hres = - match generate_fresh_id (id_of_string "z") (ids(* @this_branche_ids *)) 2 with + match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with | [res;hres] -> res,hres | _ -> assert false in @@ -466,7 +466,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem princ_type (h_exact f_principle)); observe_tac "intro args_names" (tclMAP h_intro args_names); - (* observe_tac "titi" (pose_proof (Name (id_of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *) + (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *) observe_tac "idtac" tclIDTAC; tclTHEN_i (observe_tac "functional_induction" ( @@ -506,13 +506,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let princ_infos = Tactics.compute_elim_sig princ_type in (* The number of args of the function is then easilly computable *) let nb_fun_args = nb_prod (pf_concl g) - 2 in - let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in + let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in (* Since we cannot ensure that the funcitonnal principle is defined in the environement and due to the bug #1174, we will need to pose the principle using a name *) - let principle_id = Namegen.next_ident_away_in_goal (id_of_string "princ") ids in + let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in let ids = principle_id :: ids in (* We get the branches of the principle *) let branches = List.rev princ_infos.branches in @@ -522,7 +522,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (fun (_,_,br_type) -> List.map (fun id -> Loc.ghost, Genarg.IntroIdentifier id) - (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) + (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) ) branches in @@ -540,17 +540,17 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_right (fun (_,pat) acc -> match pat with - | Genarg.IntroIdentifier id -> Idset.add id acc + | Genarg.IntroIdentifier id -> Id.Set.add id acc | _ -> anomaly "Not an identifier" ) (List.nth intro_pats (pred i)) - Idset.empty + Id.Set.empty in (* and get the real args of the branch by unfolding the defined constant *) let pre_args,pre_tac = List.fold_right (fun (id,b,t) (pre_args,pre_tac) -> - if Idset.mem id this_branche_ids + if Id.Set.mem id this_branche_ids then match b with | None -> (id::pre_args,pre_tac) @@ -624,7 +624,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let app_constructor = applist((mkConstruct(constructor)),constructor_args) in (* an apply the tactic *) let res,hres = - match generate_fresh_id (id_of_string "z") (ids(* @this_branche_ids *)) 2 with + match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with | [res;hres] -> res,hres | _ -> assert false in @@ -735,7 +735,7 @@ and intros_with_rewrite_aux : tactic = | App(eq,args) when (eq_constr eq eq_ind) -> if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2) then - let id = pf_get_new_id (id_of_string "y") g in + let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) then tclTHENSEQ[ @@ -753,7 +753,7 @@ and intros_with_rewrite_aux : tactic = ] g else if isVar args.(1) then - let id = pf_get_new_id (id_of_string "y") g in + let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ [ h_intro id; generalize_dependent_of (destVar args.(1)) id; tclTRY (Equality.rewriteLR (mkVar id)); @@ -762,7 +762,7 @@ and intros_with_rewrite_aux : tactic = g else if isVar args.(2) then - let id = pf_get_new_id (id_of_string "y") g in + let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ [ h_intro id; generalize_dependent_of (destVar args.(2)) id; tclTRY (Equality.rewriteRL (mkVar id)); @@ -771,7 +771,7 @@ and intros_with_rewrite_aux : tactic = g else begin - let id = pf_get_new_id (id_of_string "y") g in + let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ[ h_intro id; tclTRY (Equality.rewriteLR (mkVar id)); @@ -797,7 +797,7 @@ and intros_with_rewrite_aux : tactic = intros_with_rewrite ] g | _ -> - let id = pf_get_new_id (id_of_string "y") g in + let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ [ h_intro id;intros_with_rewrite] g end | LetIn _ -> @@ -904,11 +904,11 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = and compute a fresh name for each of them *) let nb_fun_args = nb_prod (pf_concl g) - 2 in - let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in + let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in (* and fresh names for res H and the principle (cf bug bug #1174) *) let res,hres,graph_principle_id = - match generate_fresh_id (id_of_string "z") ids 3 with + match generate_fresh_id (Id.of_string "z") ids 3 with | [res;hres;graph_principle_id] -> res,hres,graph_principle_id | _ -> assert false in @@ -920,7 +920,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (fun (_,_,br_type) -> List.map (fun id -> id) - (generate_fresh_id (id_of_string "y") ids (nb_prod br_type)) + (generate_fresh_id (Id.of_string "y") ids (nb_prod br_type)) ) branches in @@ -1059,7 +1059,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (fst lemmas_types_infos.(i)) (fun _ _ -> ()); Pfedit.by - (observe_tac ("prove correctness ("^(string_of_id f_id)^")") + (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)); do_save (); let finfo = find_Function_infos f_as_constant in @@ -1110,7 +1110,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (fst lemmas_types_infos.(i)) (fun _ _ -> ()); Pfedit.by - (observe_tac ("prove completeness ("^(string_of_id f_id)^")") + (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)); do_save (); let finfo = find_Function_infos f_as_constant in @@ -1187,7 +1187,7 @@ let revert_graph kn post_tac hid g = let functional_inversion kn hid fconst f_correct : tactic = fun g -> - let old_ids = List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty in + let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in let type_of_h = pf_type_of g (mkVar hid) in match kind_of_term type_of_h with | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> @@ -1206,7 +1206,7 @@ let functional_inversion kn hid fconst f_correct : tactic = h_intro hid; Inv.inv FullInversion None (NamedHyp hid); (fun g -> - let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in + let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g ); ] g diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 485b5b280..089493079 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -53,10 +53,10 @@ let understand = Pretyping.understand Evd.empty (Global.env()) (** Operations on names and identifiers *) let id_of_name = function - Anonymous -> id_of_string "H" + Anonymous -> Id.of_string "H" | Name id -> id;; -let name_of_string str = Name (id_of_string str) -let string_of_name nme = string_of_id (id_of_name nme) +let name_of_string str = Name (Id.of_string str) +let string_of_name nme = Id.to_string (id_of_name nme) (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = @@ -75,7 +75,7 @@ let ident_global_exist id = (** [next_ident_fresh id] returns a fresh identifier (ie not linked in global env) with base [id]. *) -let next_ident_fresh (id:identifier) = +let next_ident_fresh (id:Id.t) = let res = ref id in while ident_global_exist !res do res := Nameops.lift_subscript !res done; !res @@ -129,7 +129,7 @@ let prNamedRLDecl s lc = prstr "\n"; end -let showind (id:identifier) = +let showind (id:Id.t) = let cstrid = Constrintern.global_reference id in let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in @@ -247,7 +247,7 @@ type 'a merged_arg = type merge_infos = { - ident:identifier; (** new inductive name *) + ident:Id.t; (** new inductive name *) mib1: mutual_inductive_body; oib1: one_inductive_body; mib2: mutual_inductive_body; @@ -350,8 +350,8 @@ let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list = (** {1 Utilities for merging} *) -let ind1name = id_of_string "__ind1" -let ind2name = id_of_string "__ind2" +let ind1name = Id.of_string "__ind1" +let ind2name = Id.of_string "__ind2" (** Performs verifications on two graphs before merging: they must not be co-inductive, and for the moment they must not be mutual @@ -374,11 +374,11 @@ let build_raw_params prms_decl avoid = let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in let res,_ = glob_decompose_prod dummy_glob_constr in let comblist = List.combine prms_decl res in - comblist, res , (avoid @ (Idset.elements (ids_of_glob_constr dummy_glob_constr))) + comblist, res , (avoid @ (Id.Set.elements (ids_of_glob_constr dummy_glob_constr))) *) let ids_of_rawlist avoid rawl = - List.fold_left Idset.union avoid (List.map ids_of_glob_constr rawl) + List.fold_left Id.Set.union avoid (List.map ids_of_glob_constr rawl) @@ -456,7 +456,7 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array ([],[],[],[]) arity_ctxt in (* let arity_ctxt2 = build_raw_params oib2.mind_arity_ctxt - (Idset.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*) + (Id.Set.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*) let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in let _ = prstr "\n\n\n" in let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in @@ -564,7 +564,7 @@ let build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift = List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec -let find_app (nme:identifier) ltyp = +let find_app (nme:Id.t) ltyp = try ignore (List.map @@ -650,16 +650,16 @@ let rec merge_types shift accrec1 linked args [allargs2] to target args of [allargs1] as specified in [shift]. [allargs1] and [allargs2] are in reverse order. Also returns the list of unlinked vars of [allargs2]. *) -let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array) +let build_link_map_aux (allargs1:Id.t array) (allargs2:Id.t array) (lnk:int merged_arg array) = Array.fold_left_i (fun i acc e -> if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *) else match e with - | Prm_linked j | Arg_linked j -> Idmap.add allargs2.(i) allargs1.(j) acc + | Prm_linked j | Arg_linked j -> Id.Map.add allargs2.(i) allargs1.(j) acc | _ -> acc) - Idmap.empty lnk + Id.Map.empty lnk let build_link_map allargs1 allargs2 lnk = let allargs1 = @@ -742,18 +742,18 @@ let fresh_cstror_suffix , cstror_suffix_init = (** [merge_constructor_id id1 id2 shift] returns the identifier of the new constructor from the id of the two merged constructor and the merging info. *) -let merge_constructor_id id1 id2 shift:identifier = - let id = string_of_id shift.ident ^ "_" ^ fresh_cstror_suffix () in - next_ident_fresh (id_of_string id) +let merge_constructor_id id1 id2 shift:Id.t = + let id = Id.to_string shift.ident ^ "_" ^ fresh_cstror_suffix () in + next_ident_fresh (Id.of_string id) (** [merge_constructors lnk shift avoid] merges the two list of constructor [(name*type)]. These are translated to glob_constr first, each of them having distinct var names. *) -let merge_constructors (shift:merge_infos) (avoid:Idset.t) - (typcstr1:(identifier * glob_constr) list) - (typcstr2:(identifier * glob_constr) list) : (identifier * glob_constr) list = +let merge_constructors (shift:merge_infos) (avoid:Id.Set.t) + (typcstr1:(Id.t * glob_constr) list) + (typcstr2:(Id.t * glob_constr) list) : (Id.t * glob_constr) list = List.flatten (List.map (fun (id1,rawtyp1) -> @@ -775,14 +775,14 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let mkrawcor nme avoid typ = (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in - Detyping.detype false (Idset.elements avoid) [] substindtyp in + Detyping.detype false (Id.Set.elements avoid) [] substindtyp in let lcstr1: glob_constr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in (* add to avoid all indentifiers of lcstr1 *) - let avoid2 = Idset.union avoid (ids_of_rawlist avoid lcstr1) in + let avoid2 = Id.Set.union avoid (ids_of_rawlist avoid lcstr1) in let lcstr2 = Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in - let avoid3 = Idset.union avoid (ids_of_rawlist avoid lcstr2) in + let avoid3 = Id.Set.union avoid (ids_of_rawlist avoid lcstr2) in let params1 = try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) @@ -806,11 +806,11 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let merge_mutual_inductive_body (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) = (* Mutual not treated, we take first ind body of each. *) - merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0) + merge_inductive_body shift Id.Set.empty mib1.mind_packets.(0) mib2.mind_packets.(0) let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *) - Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Idset.empty) x + Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Id.Set.empty) x let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let params = prms2 @ prms1 in @@ -842,7 +842,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = [rawlist], named ident. FIXME: params et cstr_expr (arity) *) let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift - (rawlist:(identifier * glob_constr) list) = + (rawlist:(Id.t * glob_constr) list) = let lident = Loc.ghost, shift.ident in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in @@ -875,7 +875,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in let _ = prstr "\nrawlist : " in let _ = - List.iter (fun (nm,tp) -> prNamedRConstr (string_of_id nm) tp;prstr "\n") rawlist in + List.iter (fun (nm,tp) -> prNamedRConstr (Id.to_string nm) tp;prstr "\n") rawlist in let _ = prstr "\nend rawlist\n" in (* FIX: retransformer en constr ici let shift_prm = @@ -892,7 +892,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Find infos on identifier id. *) -let find_Function_infos_safe (id:identifier): Indfun_common.function_info = +let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = let kn_of_id x = let f_ref = Libnames.Ident (Loc.ghost,x) in locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref) @@ -909,8 +909,8 @@ let find_Function_infos_safe (id:identifier): Indfun_common.function_info = Warning: For the moment, repetitions of an id in [args1] or [args2] are not supported. *) -let merge (id1:identifier) (id2:identifier) (args1:identifier array) - (args2:identifier array) id : unit = +let merge (id1:Id.t) (id2:Id.t) (args1:Id.t array) + (args2:Id.t array) id : unit = let finfo1 = find_Function_infos_safe id1 in let finfo2 = find_Function_infos_safe id2 in (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a2f16dc6d..28752fe4f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -51,11 +51,11 @@ let coq_base_constant s = let find_reference sl s = (locate (make_qualid(Names.make_dirpath - (List.map id_of_string (List.rev sl))) - (id_of_string s)));; + (List.map Id.of_string (List.rev sl))) + (Id.of_string s)));; -let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = +let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) = fun f_id kind value -> let ce = {const_entry_body = value; const_entry_secctx = None; @@ -73,7 +73,7 @@ let def_of_const t = | _ -> assert false) with _ -> anomaly ("Cannot find definition of constant "^ - (string_of_id (id_of_label (con_label sp)))) + (Id.to_string (id_of_label (con_label sp)))) ) |_ -> assert false @@ -86,8 +86,8 @@ let type_of_const t = let constant sl s = constr_of_global (locate (make_qualid(Names.make_dirpath - (List.map id_of_string (List.rev sl))) - (id_of_string s)));; + (List.map Id.of_string (List.rev sl))) + (Id.of_string s)));; let const_of_ref = function ConstRef kn -> kn | _ -> anomaly "ConstRef expected" @@ -120,15 +120,15 @@ let pf_get_new_ids idl g = let compute_renamed_type gls c = rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] (pf_type_of gls c) -let h'_id = id_of_string "h'" -let teq_id = id_of_string "teq" -let ano_id = id_of_string "anonymous" -let x_id = id_of_string "x" -let k_id = id_of_string "k" -let v_id = id_of_string "v" -let def_id = id_of_string "def" -let p_id = id_of_string "p" -let rec_res_id = id_of_string "rec_res";; +let h'_id = Id.of_string "h'" +let teq_id = Id.of_string "teq" +let ano_id = Id.of_string "anonymous" +let x_id = Id.of_string "x" +let k_id = Id.of_string "k" +let v_id = Id.of_string "v" +let def_id = Id.of_string "def" +let p_id = Id.of_string "p" +let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_base_constant "lt") let le = function () -> (coq_base_constant "le") let ex = function () -> (coq_base_constant "ex") @@ -202,7 +202,7 @@ let (value_f:constr list -> global_reference -> constr) = let body = understand Evd.empty env glob_body in it_mkLambda_or_LetIn body context -let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) = +let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -300,7 +300,7 @@ let check_not_nested forbidden e = let rec check_not_nested e = match kind_of_term e with | Rel _ -> () - | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^string_of_id x) + | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^Id.to_string x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t | Prod(_,t,b) -> check_not_nested t;check_not_nested b @@ -324,21 +324,21 @@ let check_not_nested forbidden e = type 'a infos = { nb_arg : int; (* function number of arguments *) concl_tac : tactic; (* final tactic to finish proofs *) - rec_arg_id : identifier; (*name of the declared recursive argument *) + rec_arg_id : Id.t; (*name of the declared recursive argument *) is_mes : bool; (* type of recursion *) - ih : identifier; (* induction hypothesis name *) - f_id : identifier; (* function name *) + ih : Id.t; (* induction hypothesis name *) + f_id : Id.t; (* function name *) f_constr : constr; (* function term *) f_terminate : constr; (* termination proof term *) func : global_reference; (* functionnal reference *) info : 'a; is_main_branch : bool; (* on the main branch or on a matched expression *) is_final : bool; (* final first order term or not *) - values_and_bounds : (identifier*identifier) list; - eqs : identifier list; - forbidden_ids : identifier list; + values_and_bounds : (Id.t*Id.t) list; + eqs : Id.t list; + forbidden_ids : Id.t list; acc_inv : constr lazy_t; - acc_id : identifier; + acc_id : Id.t; args_assoc : ((constr list)*constr) list; } @@ -651,7 +651,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info = introduced back later; the result is the pair of the tactic and the list of hypotheses that have been generalized and cleared. *) let mkDestructEq : - identifier list -> constr -> goal sigma -> tactic * identifier list = + Id.t list -> constr -> goal sigma -> tactic * Id.t list = fun not_on_hyp expr g -> let hyps = pf_hyps g in let to_revert = @@ -1031,10 +1031,10 @@ let termination_proof_header is_mes input_type ids args_id relation in let relation = substl pre_rec_args relation in let input_type = substl pre_rec_args input_type in - let wf_thm = next_ident_away_in_goal (id_of_string ("wf_R")) ids in + let wf_thm = next_ident_away_in_goal (Id.of_string ("wf_R")) ids in let wf_rec_arg = next_ident_away_in_goal - (id_of_string ("Acc_"^(string_of_id rec_arg_id))) + (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))) (wf_thm::ids) in let hrec = next_ident_away_in_goal hrec_id @@ -1206,8 +1206,8 @@ let build_and_l l = let is_rec_res id = - let rec_res_name = string_of_id rec_res_id in - let id_name = string_of_id id in + let rec_res_name = Id.to_string rec_res_id in + let id_name = Id.to_string id in try String.sub id_name 0 (String.length rec_res_name) = rec_res_name with _ -> false @@ -1384,7 +1384,7 @@ let com_terminate let start_equation (f:global_reference) (term_f:global_reference) - (cont_tactic:identifier list -> tactic) g = + (cont_tactic:Id.t list -> tactic) g = let ids = pf_ids_of_hyps g in let terminate_constr = constr_of_global term_f in let nargs = nb_prod (type_of_const terminate_constr) in @@ -1397,7 +1397,7 @@ let start_equation (f:global_reference) (term_f:global_reference) Array.of_list (List.map mkVar x)))); observe_tac (str "prove_eq") (cont_tactic x)] g;; -let (com_eqn : int -> identifier -> +let (com_eqn : int -> Id.t -> global_reference -> global_reference -> global_reference -> constr -> unit) = fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> @@ -1430,12 +1430,12 @@ let (com_eqn : int -> identifier -> eqs = []; forbidden_ids = []; acc_inv = lazy (assert false); - acc_id = id_of_string "____"; + acc_id = Id.of_string "____"; args_assoc = []; - f_id = id_of_string "______"; - rec_arg_id = id_of_string "______"; + f_id = Id.of_string "______"; + rec_arg_id = Id.of_string "______"; is_mes = false; - ih = id_of_string "______"; + ih = Id.of_string "______"; } ) ); diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 1117e2597..2ef685203 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -4,11 +4,11 @@ val tclUSER_if_not_mes : Proof_type.tactic -> bool -> - Names.identifier list option -> + Names.Id.t list option -> Proof_type.tactic val recursive_definition : bool -> - Names.identifier -> + Names.Id.t -> Constrintern.internalization_env -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index aab237a23..d2d6a7b63 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -66,7 +66,7 @@ type 'cst formula = | C of 'cst formula * 'cst formula | D of 'cst formula * 'cst formula | N of 'cst formula - | I of 'cst formula * Names.identifier option * 'cst formula + | I of 'cst formula * Names.Id.t option * 'cst formula (** * Formula pretty-printer. @@ -83,7 +83,7 @@ let rec pp_formula o f = | I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)" pp_formula f1 (match n with - | Some id -> Names.string_of_id id + | Some id -> Names.Id.to_string id | None -> "") pp_formula f2 | N(f) -> Printf.fprintf o "N(%a)" pp_formula f @@ -1158,7 +1158,7 @@ struct | (e::l) -> let (name,expr,typ) = e in xset (Term.mkNamedLetIn - (Names.id_of_string name) + (Names.Id.of_string name) expr typ acc) l in xset concl l @@ -1185,7 +1185,7 @@ let same_proof sg cl1 cl2 = let tags_of_clause tgs wit clause = let rec xtags tgs = function - | Mc.PsatzIn n -> Names.Idset.union tgs + | Mc.PsatzIn n -> Names.Id.Set.union tgs (snd (List.nth clause (CoqToCaml.nat n) )) | Mc.PsatzMulC(e,w) -> xtags tgs w | Mc.PsatzMulE (w1,w2) | Mc.PsatzAdd(w1,w2) -> xtags (xtags tgs w1) w2 @@ -1194,7 +1194,7 @@ let tags_of_clause tgs wit clause = (*let tags_of_cnf wits cnf = List.fold_left2 (fun acc w cl -> tags_of_clause acc w cl) - Names.Idset.empty wits cnf *) + Names.Id.Set.empty wits cnf *) let find_witness prover polys1 = try_any prover polys1 diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 9bfebe348..851516945 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -85,7 +85,7 @@ let generalize_time = timing "Generalize" let new_identifier = let cpt = ref 0 in - (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; id_of_string s) + (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s) let new_identifier_state = let cpt = ref 0 in @@ -93,7 +93,7 @@ let new_identifier_state = let new_identifier_var = let cpt = ref 0 in - (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s) + (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s) let new_id = let cpt = ref 0 in fun () -> incr cpt; !cpt @@ -109,7 +109,7 @@ let display_var i = Printf.sprintf "X%d" i let intern_id,unintern_id = let cpt = ref 0 in let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in - (fun (name : identifier) -> + (fun (name : Id.t) -> try Hashtbl.find table name with Not_found -> let idx = !cpt in Hashtbl.add table name idx; @@ -136,13 +136,13 @@ let rev_assoc k = loop let tag_hypothesis,tag_of_hyp, hyp_of_tag = - let l = ref ([]:(identifier * int) list) in + let l = ref ([]:(Id.t * int) list) in (fun h id -> l := (h,id):: !l), (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"), (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis") let hide_constr,find_constr,clear_tables,dump_tables = - let l = ref ([]:(constr * (identifier * identifier * bool)) list) in + let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in (fun h id eg b -> l := (h,(id,eg,b)):: !l), (fun h -> try List.assoc_f eq_constr h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), @@ -329,7 +329,7 @@ let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge) let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt) let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ()))) -let mk_var v = mkVar (id_of_string v) +let mk_var v = mkVar (Id.of_string v) let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |]) let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |]) let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |]) @@ -370,7 +370,7 @@ type omega_proposition = | Kn type result = - | Kvar of identifier + | Kvar of Id.t | Kapp of omega_constant * constr list | Kimp of constr * constr | Kufo @@ -527,7 +527,7 @@ let occurence path (t : constr) = let abstract_path typ path t = let term_occur = ref (mkRel 0) in let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in - mkLambda (Name (id_of_string "x"), typ, abstract), !term_occur + mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur let focused_simpl path gl = let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in @@ -539,7 +539,7 @@ type oformula = | Oplus of oformula * oformula | Oinv of oformula | Otimes of oformula * oformula - | Oatom of identifier + | Oatom of Id.t | Oz of bigint | Oufo of constr @@ -551,7 +551,7 @@ let rec oprint = function | Otimes (t1,t2) -> print_string "("; oprint t1; print_string "*"; oprint t2; print_string ")" - | Oatom s -> print_string (string_of_id s) + | Oatom s -> print_string (Id.to_string s) | Oz i -> print_string (string_of_bigint i) | Oufo f -> print_string "?" @@ -597,10 +597,10 @@ let clever_rewrite_base_poly typ p result theorem gl = let t = applist (mkLambda - (Name (id_of_string "P"), + (Name (Id.of_string "P"), mkArrow typ mkProp, mkLambda - (Name (id_of_string "H"), + (Name (Id.of_string "H"), applist (mkRel 1,[result]), mkApp (Lazy.force coq_eq_ind_r, [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), @@ -1007,9 +1007,9 @@ let rec clear_zero p = function | t -> [],t let replay_history tactic_normalisation = - let aux = id_of_string "auxiliary" in - let aux1 = id_of_string "auxiliary_1" in - let aux2 = id_of_string "auxiliary_2" in + let aux = Id.of_string "auxiliary" in + let aux1 = Id.of_string "auxiliary_1" in + let aux2 = Id.of_string "auxiliary_2" in let izero = mk_integer zero in let rec loop t = match t with diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index ee341cbc2..d94a7136a 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -39,7 +39,7 @@ END TACTIC EXTEND omega' | [ "omega" "with" ne_ident_list(l) ] -> - [ omega_tactic (List.map Names.string_of_id l) ] + [ omega_tactic (List.map Names.Id.to_string l) ] | [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ] END diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 61a464c1c..4238037e7 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -189,10 +189,10 @@ let decomp_term c = kind_of_term (strip_outer_cast c) type [typ] *) let coerce_meta_out id = - let s = string_of_id id in + let s = Id.to_string id in int_of_string (String.sub s 1 (String.length s - 1)) let coerce_meta_in n = - id_of_string ("M" ^ string_of_int n) + Id.of_string ("M" ^ string_of_int n) let compute_lhs typ i nargsi = match kind_of_term typ with diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 5b57a0d17..92135d497 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -22,10 +22,10 @@ let string_of_global r = let prefix = match Names.repr_dirpath dp with | [] -> "" | m::_ -> - let s = Names.string_of_id m in + let s = Names.Id.to_string m in if List.mem s meaningful_submodule then s^"." else "" in - prefix^(Names.string_of_id (Nametab.basename_of_global r)) + prefix^(Names.Id.to_string (Nametab.basename_of_global r)) let destructurate t = let c, args = Term.decompose_app t in @@ -36,7 +36,7 @@ let destructurate t = Kapp (string_of_global (Globnames.ConstructRef csp), args) | Term.Ind isp, args -> Kapp (string_of_global (Globnames.IndRef isp), args) - | Term.Var id,[] -> Kvar(Names.string_of_id id) + | Term.Var id,[] -> Kvar(Names.Id.to_string id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) | Term.Prod (Names.Name _,_,_),[] -> Errors.error "Omega: Not a quantifier-free goal" @@ -296,13 +296,13 @@ let coq_Zneg = lazy (bin_constant "Zneg") let recognize t = let rec loop t = let f,l = dest_const_apply t in - match Names.string_of_id f,l with + match Names.Id.to_string f,l with "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t)) | "xO",[t] -> Bigint.mult Bigint.two (loop t) | "xH",[] -> Bigint.one | _ -> failwith "not a number" in let f,l = dest_const_apply t in - match Names.string_of_id f,l with + match Names.Id.to_string f,l with "Zpos",[t] -> loop t | "Zneg",[t] -> Bigint.neg (loop t) | "Z0",[] -> Bigint.zero diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 5a843e2b7..a68196e8c 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -37,6 +37,6 @@ END TACTIC EXTEND romega' | [ "romega" "with" ne_ident_list(l) ] -> - [ romega_tactic (List.map Names.string_of_id l) ] + [ romega_tactic (List.map Names.Id.to_string l) ] | [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ] END diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e573f2006..e3674fae0 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -40,7 +40,7 @@ type occ_path = occ_step list (* chemin identifiant une proposition sous forme du nom de l'hypothèse et d'une liste de pas à partir de la racine de l'hypothèse *) -type occurence = {o_hyp : Names.identifier; o_path : occ_path} +type occurence = {o_hyp : Names.Id.t; o_path : occ_path} (* \subsection{refiable formulas} *) type oformula = @@ -137,7 +137,7 @@ type context_content = (* \section{Specific utility functions to handle base types} *) (* Nom arbitraire de l'hypothèse codant la négation du but final *) -let id_concl = Names.id_of_string "__goal__" +let id_concl = Names.Id.of_string "__goal__" (* Initialisation de l'environnement de réification de la tactique *) let new_environment () = { @@ -746,7 +746,7 @@ let reify_gl env gl = (i,t) :: lhyps -> let t' = oproposition_of_constr env (false,[],i,[]) gl t in if !debug then begin - Printf.printf " %s: " (Names.string_of_id i); + Printf.printf " %s: " (Names.Id.to_string i); pprint stdout t'; Printf.printf "\n" end; @@ -840,7 +840,7 @@ let display_systems syst_list = (List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M") oformula_eq.e_origin.o_path)); Printf.printf "\n Origin: %s (negated : %s)\n\n" - (Names.string_of_id oformula_eq.e_origin.o_hyp) + (Names.Id.to_string oformula_eq.e_origin.o_hyp) (if oformula_eq.e_negated then "yes" else "no") in let display_system syst = diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index e5fb646a4..f7e6ec020 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -18,7 +18,7 @@ val make_hyps : atom_env -> Proof_type.goal Tacmach.sigma -> Term.types list -> - (Names.identifier * Term.types option * Term.types) list -> - (Names.identifier * Proof_search.form) list + (Names.Id.t * Term.types option * Term.types) list -> + (Names.Id.t * Proof_search.form) list val rtauto_tac : Proof_type.tactic diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 717b19e2c..17ea6f2bf 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -119,19 +119,19 @@ END;;*) (* let closed_term_ast l = - TacFun([Some(id_of_string"t")], + TacFun([Some(Id.of_string"t")], TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", - [Genarg.in_gen Genarg.wit_constr (mkVar(id_of_string"t")); + [Genarg.in_gen Genarg.wit_constr (mkVar(Id.of_string"t")); Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l]))) *) let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in - TacFun([Some(id_of_string"t")], + TacFun([Some(Id.of_string"t")], TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", - [Genarg.in_gen Genarg.globwit_constr (GVar(Loc.ghost,id_of_string"t"),None); + [Genarg.in_gen Genarg.globwit_constr (GVar(Loc.ghost,Id.of_string"t"),None); Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l]))) (* -let _ = add_tacdef false ((Loc.ghost,id_of_string"ring_closed_term" +let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) (****************************************************************************) @@ -143,7 +143,7 @@ let ic c = let ty c = Typing.type_of (Global.env()) Evd.empty c let decl_constant na c = - mkConst(declare_constant (id_of_string na) (DefinitionEntry + mkConst(declare_constant (Id.of_string na) (DefinitionEntry { const_entry_body = c; const_entry_secctx = None; const_entry_type = None; @@ -156,17 +156,17 @@ let ltac_call tac (args:glob_tactic_arg list) = (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, id_of_string tac),args)) + TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args)) let ltac_letin (x, e1) e2 = - TacLetIn(false,[(Loc.ghost,id_of_string x),e1],e2) + TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2) let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) = Tacinterp.eval_tactic (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args)) let ltac_record flds = - TacFun([Some(id_of_string"proj")], ltac_lcall "proj" flds) + TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds) let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c) @@ -178,7 +178,7 @@ let dummy_goal env = Evd.sigma = sigma} let exec_tactic env n f args = - let lid = List.tabulate(fun i -> id_of_string("x"^string_of_int i)) n in + let lid = List.tabulate(fun i -> Id.of_string("x"^string_of_int i)) n in let res = ref [||] in let get_res ist = let l = List.map (fun id -> List.assoc id ist.lfun) lid in @@ -244,11 +244,11 @@ let my_constant c = lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c) let new_ring_path = - make_dirpath (List.map id_of_string ["Ring_tac";plugin_dir;"Coq"]) + make_dirpath (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) let ltac s = lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s)) let znew_ring_path = - make_dirpath (List.map id_of_string ["InitialRing";plugin_dir;"Coq"]) + make_dirpath (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s)) @@ -689,8 +689,8 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = let lemma1 = constr_of params.(3) in let lemma2 = constr_of params.(4) in - let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in - let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in + let lemma1 = decl_constant (Id.to_string name^"_ring_lemma1") lemma1 in + let lemma2 = decl_constant (Id.to_string name^"_ring_lemma2") lemma2 in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = @@ -826,7 +826,7 @@ END (***********************************************************************) let new_field_path = - make_dirpath (List.map id_of_string ["Field_tac";plugin_dir;"Coq"]) + make_dirpath (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) let field_ltac s = lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s)) @@ -1049,11 +1049,11 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi match inj with | Some thm -> mkApp(constr_of params.(8),[|thm|]) | None -> constr_of params.(7) in - let lemma1 = decl_constant (string_of_id name^"_field_lemma1") lemma1 in - let lemma2 = decl_constant (string_of_id name^"_field_lemma2") lemma2 in - let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in - let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in - let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in + let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") lemma1 in + let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") lemma2 in + let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") lemma3 in + let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") lemma4 in + let cond_lemma = decl_constant (Id.to_string name^"_lemma5") cond_lemma in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 03fbc7e98..958fdc649 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -16,9 +16,9 @@ open Coqlib exception Non_closed_ascii -let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let make_kn dir id = Globnames.encode_mind (make_dir dir) (id_of_string id) -let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) +let make_dir l = make_dirpath (List.map Id.of_string (List.rev l)) +let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id) +let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) let ascii_module = ["Coq";"Strings";"Ascii"] diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 94d4e0713..f86b56bc7 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -14,8 +14,8 @@ open Glob_term (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***) -let make_dir l = Names.make_dirpath (List.map Names.id_of_string (List.rev l)) -let make_path dir id = Libnames.make_path (make_dir dir) (Names.id_of_string id) +let make_dir l = Names.make_dirpath (List.map Names.Id.of_string (List.rev l)) +let make_path dir id = Libnames.make_path (make_dir dir) (Names.Id.of_string id) let make_mind mp id = Names.make_mind mp Names.empty_dirpath (Names.mk_label id) let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index a40c966fe..f7d0091f3 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -19,14 +19,14 @@ exception Non_closed_number open Glob_term open Bigint -let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) +let make_dir l = make_dirpath (List.map Id.of_string (List.rev l)) let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"] -let make_path dir id = Libnames.make_path dir (id_of_string id) +let make_path dir id = Libnames.make_path dir (Id.of_string id) let r_path = make_path rdefinitions "R" (* TODO: temporary hack *) -let make_path dir id = Globnames.encode_con dir (id_of_string id) +let make_path dir id = Globnames.encode_con dir (Id.of_string id) let r_kn = make_path rdefinitions "R" let glob_R = ConstRef r_kn diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 8e5a07e0d..9faa6edd1 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -23,15 +23,15 @@ open Glob_term let binnums = ["Coq";"Numbers";"BinNums"] -let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) +let make_dir l = make_dirpath (List.map Id.of_string (List.rev l)) +let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) let positive_path = make_path binnums "positive" (* TODO: temporary hack *) let make_kn dir id = Globnames.encode_mind dir id -let positive_kn = make_kn (make_dir binnums) (id_of_string "positive") +let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive") let glob_positive = IndRef (positive_kn,0) let path_of_xI = ((positive_kn,0),1) let path_of_xO = ((positive_kn,0),2) @@ -93,7 +93,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope" (* Parsing N via scopes *) (**********************************************************************) -let n_kn = make_kn (make_dir binnums) (id_of_string "N") +let n_kn = make_kn (make_dir binnums) (Id.of_string "N") let glob_n = IndRef (n_kn,0) let path_of_N0 = ((n_kn,0),1) let path_of_Npos = ((n_kn,0),2) @@ -144,7 +144,7 @@ let _ = Notation.declare_numeral_interpreter "N_scope" (**********************************************************************) let z_path = make_path binnums "Z" -let z_kn = make_kn (make_dir binnums) (id_of_string "Z") +let z_kn = make_kn (make_dir binnums) (Id.of_string "Z") let glob_z = IndRef (z_kn,0) let path_of_ZERO = ((z_kn,0),1) let path_of_POS = ((z_kn,0),2) diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml index 653c2b7bd..3e2c8ade7 100644 --- a/plugins/xml/acic.ml +++ b/plugins/xml/acic.ml @@ -34,7 +34,7 @@ type 'constr context_entry = (* is not present in the DTD, but is needed *) (* to use Coq functions during exportation. *) -type 'constr hypothesis = identifier * 'constr context_entry +type 'constr hypothesis = Id.t * 'constr context_entry type context = constr hypothesis list type conjecture = existential_key * context * constr @@ -57,13 +57,13 @@ type obj = inductiveType list * (* inductive types , *) params * int (* parameters,n ind. pars*) and inductiveType = - identifier * bool * constr * (* typename, inductive, arity *) + Id.t * bool * constr * (* typename, inductive, arity *) constructor list (* constructors *) and constructor = - identifier * constr (* id, type *) + Id.t * constr (* id, type *) type aconstr = - | ARel of id * int * id * identifier + | ARel of id * int * id * Id.t | AVar of id * uri | AEvar of id * existential_key * aconstr list | ASort of id * sorts @@ -79,9 +79,9 @@ type aconstr = | AFix of id * int * ainductivefun list | ACoFix of id * int * acoinductivefun list and ainductivefun = - id * identifier * int * aconstr * aconstr + id * Id.t * int * aconstr * aconstr and acoinductivefun = - id * identifier * aconstr * aconstr + id * Id.t * aconstr * aconstr and explicit_named_substitution = id option * (uri * aconstr) list type acontext = (id * aconstr hypothesis) list @@ -102,7 +102,7 @@ type aobj = anninductiveType list * (* inductive types , *) params * int (* parameters,n ind. pars*) and anninductiveType = - id * identifier * bool * aconstr * (* typename, inductive, arity *) + id * Id.t * bool * aconstr * (* typename, inductive, arity *) annconstructor list (* constructors *) and annconstructor = - identifier * aconstr (* id, type *) + Id.t * aconstr (* id, type *) diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 index c03b13b5a..34bb1d51f 100644 --- a/plugins/xml/acic2Xml.ml4 +++ b/plugins/xml/acic2Xml.ml4 @@ -37,7 +37,7 @@ let print_term ids_to_inner_sorts = A.ARel (id,n,idref,b) -> let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_empty "REL" - ["value",(string_of_int n) ; "binder",(N.string_of_id b) ; + ["value",(string_of_int n) ; "binder",(N.Id.to_string b) ; "id",id ; "idref",idref; "sort",sort] | A.AVar (id,uri) -> let sort = Hashtbl.find ids_to_inner_sorts id in @@ -71,7 +71,7 @@ let print_term ids_to_inner_sorts = ("id",id)::("type",sort):: match binder with Names.Anonymous -> [] - | Names.Name b -> ["binder",Names.string_of_id b] + | Names.Name b -> ["binder",Names.Id.to_string b] in [< X.xml_nempty "decl" attrs (aux s) ; i >] ) [< >] prods ; @@ -96,7 +96,7 @@ let print_term ids_to_inner_sorts = ("id",id)::("type",sort):: match binder with Names.Anonymous -> [] - | Names.Name b -> ["binder",Names.string_of_id b] + | Names.Name b -> ["binder",Names.Id.to_string b] in [< X.xml_nempty "decl" attrs (aux s) ; i >] ) [< >] lambdas ; @@ -115,7 +115,7 @@ let print_term ids_to_inner_sorts = ("id",id)::("sort",sort):: match binder with Names.Anonymous -> assert false - | Names.Name b -> ["binder",Names.string_of_id b] + | Names.Name b -> ["binder",Names.Id.to_string b] in [< X.xml_nempty "def" attrs (aux s) ; i >] ) [< >] letins ; @@ -161,7 +161,7 @@ let print_term ids_to_inner_sorts = (fun i (id,fi,ai,ti,bi) -> [< i ; X.xml_nempty "FixFunction" - ["id",id ; "name", (Names.string_of_id fi) ; + ["id",id ; "name", (Names.Id.to_string fi) ; "recIndex", (string_of_int ai)] [< X.xml_nempty "type" [] [< aux ti >] ; X.xml_nempty "body" [] [< aux bi >] @@ -177,7 +177,7 @@ let print_term ids_to_inner_sorts = (fun i (id,fi,ti,bi) -> [< i ; X.xml_nempty "CofixFunction" - ["id",id ; "name", Names.string_of_id fi] + ["id",id ; "name", Names.Id.to_string fi] [< X.xml_nempty "type" [] [< aux ti >] ; X.xml_nempty "body" [] [< aux bi >] >] @@ -229,11 +229,11 @@ let print_object uri ids_to_inner_sorts = [< (match t with n,A.Decl t -> X.xml_nempty "Decl" - ["id",hid;"name",Names.string_of_id n] + ["id",hid;"name",Names.Id.to_string n] (print_term ids_to_inner_sorts t) | n,A.Def (t,_) -> X.xml_nempty "Def" - ["id",hid;"name",Names.string_of_id n] + ["id",hid;"name",Names.Id.to_string n] (print_term ids_to_inner_sorts t) ) ; i @@ -315,7 +315,7 @@ let print_object uri ids_to_inner_sorts = (fun i (id,typename,finite,arity,cons) -> [< i ; X.xml_nempty "InductiveType" - ["id",id ; "name",Names.string_of_id typename ; + ["id",id ; "name",Names.Id.to_string typename ; "inductive",(string_of_bool finite) ] [< X.xml_nempty "arity" [] @@ -324,7 +324,7 @@ let print_object uri ids_to_inner_sorts = (fun i (name,lc) -> [< i ; X.xml_nempty "Constructor" - ["name",Names.string_of_id name] + ["name",Names.Id.to_string name] (print_term ids_to_inner_sorts lc) >]) [<>] cons ) diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 62f7cc7cf..d817396f1 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -62,7 +62,7 @@ let get_uri_of_var v pvars = [] -> Errors.error ("Variable "^v^" not found") | he::tl as modules -> let dirpath = N.make_dirpath modules in - if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then + if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then modules else search_in_open_sections tl @@ -75,7 +75,7 @@ let get_uri_of_var v pvars = in "cic:" ^ List.fold_left - (fun i x -> "/" ^ N.string_of_id x ^ i) "" path + (fun i x -> "/" ^ N.Id.to_string x ^ i) "" path ;; type tag = @@ -120,8 +120,8 @@ let subtract l1 l2 = let token_list_of_path dir id tag = let module N = Names in let token_list_of_dirpath dirpath = - List.rev_map N.string_of_id (N.repr_dirpath dirpath) in - token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)] + List.rev_map N.Id.to_string (N.repr_dirpath dirpath) in + token_list_of_dirpath dir @ [N.Id.to_string id ^ "." ^ (ext_of_tag tag)] let token_list_of_kernel_name tag = let module N = Names in @@ -202,7 +202,7 @@ let typeur sigma metamap = let (_,_,ty) = Environ.lookup_named id env in ty with Not_found -> - Errors.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound")) + Errors.anomaly ("type_of: variable "^(Names.Id.to_string id)^" unbound")) | T.Const c -> let cb = Environ.lookup_constant c env in Typeops.type_of_constant_type env (cb.Declarations.const_type) @@ -455,8 +455,8 @@ print_endline "PASSATO" ; flush stdout ; let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in let he1'' = String.concat "/" - (List.map Names.string_of_id (List.rev he1')) ^ "/" - ^ (Names.string_of_id he1_id) ^ ".var" + (List.map Names.Id.to_string (List.rev he1')) ^ "/" + ^ (Names.Id.to_string he1_id) ^ ".var" in (he1'',he2)::subst, extra_args, uninst in @@ -501,13 +501,13 @@ print_endline "PASSATO" ; flush stdout ; A.ARel (fresh_id'', n, List.nth idrefs (n-1), id) | T.Var id -> let pvars = Termops.ids_of_named_context (E.named_context env) in - let pvars = List.map N.string_of_id pvars in - let path = get_uri_of_var (N.string_of_id id) pvars in + let pvars = List.map N.Id.to_string pvars in + let path = get_uri_of_var (N.Id.to_string id) pvars in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then add_inner_type fresh_id'' ; A.AVar - (fresh_id'', path ^ "/" ^ (N.string_of_id id) ^ ".var") + (fresh_id'', path ^ "/" ^ (N.Id.to_string id) ^ ".var") | T.Evar (n,l) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then @@ -610,7 +610,7 @@ print_endline "PASSATO" ; flush stdout ; | T.LetIn (n,s,t,d) -> let id = match n with - N.Anonymous -> N.id_of_string "_X" + N.Anonymous -> N.Id.of_string "_X" | N.Name id -> id in let n' = @@ -886,7 +886,7 @@ let acic_object_of_cic_object sigma obj = in let dummy_never_used = let s = "dummy_never_used" in - A.ARel (s,99,s,Names.id_of_string s) + A.ARel (s,99,s,Names.Id.of_string s) in final_env,final_idrefs, (hid,(n,A.Def (at,dummy_never_used)))::atl diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 8259266af..35760a51d 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -35,7 +35,7 @@ let filter_params pvars hyps = let ids' = id::ids in let ids'' = "cic:/" ^ - String.concat "/" (List.rev (List.map Names.string_of_id ids')) in + String.concat "/" (List.rev (List.map Names.Id.to_string ids')) in let he' = ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in let tl' = aux ids' tl in @@ -44,7 +44,7 @@ let filter_params pvars hyps = | _,_ -> he'::tl' in let cwd = Lib.cwd () in - let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in + let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in aux (Names.repr_dirpath modulepath) (List.rev pvars) ;; @@ -55,7 +55,7 @@ let filter_params pvars hyps = let search_variables () = let module N = Names in let cwd = Lib.cwd () in - let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in + let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in let rec aux = function @@ -63,7 +63,7 @@ let search_variables () = | he::tl as modules -> let one_section_variables = let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in - let t = List.map N.string_of_id (Decls.last_section_hyps dirpath) in + let t = List.map N.Id.to_string (Decls.last_section_hyps dirpath) in [he,t] in one_section_variables @ aux tl @@ -113,7 +113,7 @@ let theory_filename xml_library_root = match xml_library_root with None -> None (* stdout *) | Some xml_library_root' -> - let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in + let toks = List.map N.Id.to_string (N.repr_dirpath (Lib.library_dp ())) in (* theory from A/B/C/F.v goes into A/B/C/F.theory *) let alltoks = List.rev toks in Some (join_dirs xml_library_root' alltoks ^ ".theory") @@ -153,7 +153,7 @@ let print_object uri obj sigma filename = let string_list_of_named_context_list = List.map - (function (n,_,_) -> Names.string_of_id n) + (function (n,_,_) -> Names.Id.to_string n) ;; (* Function to collect the variables that occur in a term. *) @@ -212,11 +212,11 @@ let mk_variable_obj id body typ = | Some bo -> find_hyps bo, Some (Unshare.unshare bo) in let hyps' = find_hyps typ @ hyps in - let hyps'' = List.map Names.string_of_id hyps' in + let hyps'' = List.map Names.Id.to_string hyps' in let variables = search_variables () in let params = filter_params variables hyps'' in Acic.Variable - (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params) + (Names.Id.to_string id, unsharedbody, Unshare.unshare typ, params) ;; @@ -226,10 +226,10 @@ let mk_constant_obj id bo ty variables hyps = let params = filter_params variables hyps in match bo with None -> - Acic.Constant (Names.string_of_id id,None,ty,params) + Acic.Constant (Names.Id.to_string id,None,ty,params) | Some c -> Acic.Constant - (Names.string_of_id id, Some (Unshare.unshare (Declarations.force c)), + (Names.Id.to_string id, Some (Unshare.unshare (Declarations.force c)), ty,params) ;; @@ -531,7 +531,7 @@ let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ; let uri_of_dirpath dir = "/" ^ String.concat "/" - (List.map Names.string_of_id (List.rev (Names.repr_dirpath dir))) + (List.map Names.Id.to_string (List.rev (Names.repr_dirpath dir))) ;; let _ = -- cgit v1.2.3