diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-16 15:58:48 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-16 15:58:48 +0000 |
commit | 3c248785237d8dea037da274f4acc0229894de93 (patch) | |
tree | 4501aca5e725d5f62ffd9f959a8956f30bf432eb | |
parent | 649e7e98e0067a7ae2a3990b9629dcec66b47497 (diff) |
ident au lieu de string pour le nom de base de qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/omega/coq_omega.ml | 12 | ||||
-rw-r--r-- | contrib/ring/quote.ml | 5 | ||||
-rw-r--r-- | contrib/ring/ring.ml | 5 | ||||
-rw-r--r-- | contrib/xml/xmlcommand.ml | 3 | ||||
-rw-r--r-- | kernel/names.ml | 2 | ||||
-rw-r--r-- | kernel/names.mli | 4 | ||||
-rw-r--r-- | library/declare.ml | 2 | ||||
-rw-r--r-- | library/global.ml | 4 | ||||
-rw-r--r-- | library/library.ml | 2 | ||||
-rwxr-xr-x | library/nametab.ml | 40 | ||||
-rwxr-xr-x | library/nametab.mli | 4 | ||||
-rw-r--r-- | parsing/astterm.ml | 22 | ||||
-rw-r--r-- | parsing/coqlib.ml | 5 | ||||
-rw-r--r-- | parsing/pretty.ml | 5 | ||||
-rw-r--r-- | parsing/termast.ml | 4 | ||||
-rw-r--r-- | proofs/tacinterp.ml | 6 | ||||
-rw-r--r-- | tactics/auto.ml | 8 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 13 |
18 files changed, 77 insertions, 69 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index fec7fb701..00ce6d207 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -213,10 +213,11 @@ let recognize_number t = let constant dir s = let dir = "Coq"::dir in + let id = id_of_string s in try - Declare.global_reference_in_absolute_module dir (id_of_string s) + Declare.global_reference_in_absolute_module dir id with Not_found -> - anomaly ("Coq_omega: cannot find "^(string_of_qualid (make_qualid dir s))) + anomaly ("Coq_omega: cannot find "^(string_of_qualid (make_qualid dir id))) let zarith_constant dir = constant ("Zarith"::dir) @@ -368,15 +369,16 @@ let build_coq_eq = build_coq_eq_data.eq open Closure let make_coq_path dir s = let dir = "Coq"::dir in + let id = id_of_string s in let ref = - try Nametab.locate_in_absolute_module dir (id_of_string s) + try Nametab.locate_in_absolute_module dir id with Not_found -> - anomaly("Coq_omega: cannot find "^(string_of_qualid (make_qualid dir s))) + anomaly("Coq_omega: cannot find "^(string_of_qualid(make_qualid dir id))) in match ref with | ConstRef sp -> EvalConstRef sp | _ -> anomaly ("Coq_omega: "^ - (string_of_qualid (make_qualid dir s))^ + (string_of_qualid (make_qualid dir id))^ " is not a constant") let sp_Zs = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zs") diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 44cbd7868..efc8d78d8 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -114,10 +114,11 @@ open Proof_type let constant dir s = let dir = "Coq"::"ring"::dir in + let id = id_of_string s in try - Declare.global_reference_in_absolute_module dir (id_of_string s) + Declare.global_reference_in_absolute_module dir id with Not_found -> - anomaly ("Quote: cannot find "^(string_of_qualid (make_qualid dir s))) + anomaly ("Quote: cannot find "^(string_of_qualid (make_qualid dir id))) let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index b3421c969..7b3b8f6f6 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -27,10 +27,11 @@ let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com let constant dir s = let dir = "Coq"::"ring"::dir in + let id = id_of_string s in try - Declare.global_reference_in_absolute_module dir (id_of_string s) + Declare.global_reference_in_absolute_module dir id with Not_found -> - anomaly ("Ring: cannot find "^(string_of_qualid (make_qualid dir s))) + anomaly ("Ring: cannot find "^(string_of_qualid (make_qualid dir id))) (* Ring_theory *) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index a3c1af98d..4d4b05d78 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -699,8 +699,7 @@ let print sp fn = let module N = Names in let module T = Term in let module X = Xml in - let (_,str) = N.repr_qualid sp in - let id = Names.id_of_string str in + let (_,id) = N.repr_qualid sp in let glob_ref = Nametab.locate sp in let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in reset_ids () ; diff --git a/kernel/names.ml b/kernel/names.ml index fc3453611..83cea889a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -256,7 +256,7 @@ let kind_of_string = function (*s Section paths *) -type qualid = string list * string +type qualid = string list * identifier let make_qualid p s = (p,s) let repr_qualid q = q diff --git a/kernel/names.mli b/kernel/names.mli index edcadf634..6912d6665 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -60,8 +60,8 @@ val string_of_dirpath : dir_path -> string (*s Qualified idents are names relative to the current visilibity of names *) type qualid -val make_qualid : dir_path -> string -> qualid -val repr_qualid : qualid -> dir_path * string +val make_qualid : dir_path -> identifier -> qualid +val repr_qualid : qualid -> dir_path * identifier val string_of_qualid : qualid -> string val pr_qualid : qualid -> std_ppcmds diff --git a/library/declare.ml b/library/declare.ml index 57e58256e..853a22d12 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -420,7 +420,7 @@ let dirpath_of_global = function let is_global id = try - let osp = Nametab.locate (make_qualid [] (string_of_id id)) in + let osp = Nametab.locate (make_qualid [] id) in list_prefix_of (dirpath_of_global osp) (Lib.cwd()) with Not_found -> false diff --git a/library/global.ml b/library/global.ml index c07452988..cdc7fdb18 100644 --- a/library/global.ml +++ b/library/global.ml @@ -63,9 +63,9 @@ let sp_of_global id = Environ.sp_of_global (env_of_safe_env !global_env) id let qualid_of_global ref = let sp = sp_of_global ref in - let s = string_of_id (basename sp) in + let id = basename sp in let rec find_visible dir qdir = - let qid = make_qualid qdir s in + let qid = make_qualid qdir id in if (try Nametab.locate qid = ref with Not_found -> false) then qid else match dir with | [] -> qualid_of_sp sp diff --git a/library/library.ml b/library/library.ml index b0c1a2ecd..0ec028963 100644 --- a/library/library.ml +++ b/library/library.ml @@ -117,7 +117,7 @@ let rec open_module force s = if force or not m.module_opened then begin List.iter (fun (m,_,exp) -> if exp then open_module force m) m.module_deps; open_objects m.module_declarations; - Nametab.open_module_contents (make_qualid [] s); + Nametab.open_module_contents (make_qualid [] (id_of_string s)); m.module_opened <- true end diff --git a/library/nametab.ml b/library/nametab.ml index c8e10a1ed..046a9518c 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -17,22 +17,22 @@ let coq_root = "Coq" let default_root = "Scratch" (* Names tables *) -type cci_table = global_reference Stringmap.t -type obj_table = (section_path * obj) Stringmap.t +type cci_table = global_reference Idmap.t +type obj_table = (section_path * obj) Idmap.t type mod_table = (section_path * module_contents) Stringmap.t and module_contents = Closed of cci_table * obj_table * mod_table let empty = - Closed (Stringmap.empty, Stringmap.empty, Stringmap.empty) + Closed (Idmap.empty, Idmap.empty, Stringmap.empty) let persistent_nametab = ref (empty : module_contents) let local_nametab = ref (empty : module_contents) let push_cci (Closed (ccitab, objtab, modtab)) s ref = - Closed (Stringmap.add s ref ccitab, objtab, modtab) + Closed (Idmap.add s ref ccitab, objtab, modtab) let push_obj (Closed (ccitab, objtab, modtab)) s obj = - Closed (ccitab, Stringmap.add s obj objtab, modtab) + Closed (ccitab, Idmap.add s obj objtab, modtab) let push_mod (Closed (ccitab, objtab, modtab)) s mc = (* devrait pas mais ca plante en décommentant la ligne ci-dessous *) @@ -78,6 +78,7 @@ let push_object sp obj = let push_module sp mc = let dir, s = repr_qualid (qualid_of_sp sp) in + let s = string_of_id s in push_mod_absolute dir s (sp,mc); if List.mem s !roots then warning ("Cannot allow access to "^s^" by relative paths: it is already registered as a root of the Coq library") @@ -86,7 +87,7 @@ let push_module sp mc = (* Sections are not accessible by basename *) let push_section sp mc = let dir, s = repr_qualid (qualid_of_sp sp) in - push_mod_absolute dir s (sp,mc) + push_mod_absolute dir (string_of_id s) (sp,mc) (* This is an entry point for local declarations at toplevel *) (* Do not use with "open" since it pushes an absolute name too *) @@ -113,7 +114,7 @@ let locate qid = let (dir,id) = repr_qualid qid in let rec search (Closed (ccitab,_,modtab)) = function | id :: dir' -> search (snd (Stringmap.find id modtab)) dir' - | [] -> Stringmap.find id ccitab + | [] -> Idmap.find id ccitab in try search !local_nametab dir with Not_found -> search !persistent_nametab dir @@ -122,16 +123,17 @@ let locate_obj qid = let (dir,id) = repr_qualid qid in let rec search (Closed (_,objtab,modtab)) = function | id :: dir' -> search (snd (Stringmap.find id modtab)) dir' - | [] -> Stringmap.find id objtab + | [] -> Idmap.find id objtab in try search !local_nametab dir with Not_found -> search !persistent_nametab dir let locate_module qid = let (dir,id) = repr_qualid qid in + let s = string_of_id id in let rec search (Closed (_,_,modtab)) = function | id :: dir' -> search (snd (Stringmap.find id modtab)) dir' - | [] -> Stringmap.find id modtab + | [] -> Stringmap.find s modtab in try search !local_nametab dir with Not_found -> search !persistent_nametab dir @@ -141,10 +143,10 @@ let locate_constant qid = | ConstRef sp -> sp | _ -> raise Not_found -let sp_of_id _ id = locate (make_qualid [] (string_of_id id)) +let sp_of_id _ id = locate (make_qualid [] id) let constant_sp_of_id id = - match locate (make_qualid [] (string_of_id id)) with + match locate (make_qualid [] id) with | ConstRef sp -> sp | _ -> raise Not_found @@ -160,7 +162,7 @@ let absolute_reference sp = exception Found of global_reference let locate_in_module dir id = let rec exists_in id (Closed (ccitab,_,modtab)) = - try raise (Found (Stringmap.find id ccitab)) + try raise (Found (Idmap.find id ccitab)) with Not_found -> Stringmap.iter (fun _ (sp,mc) -> exists_in id mc) modtab in @@ -174,28 +176,28 @@ let locate_in_module dir id = let locate_in_absolute_module dir id = check_absoluteness dir; - locate_in_module dir (string_of_id id) + locate_in_module dir id (* These are entry points to make the contents of a module/section visible *) (* in the current env (does not affect the absolute name space `coq_root') *) let open_module_contents qid = let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in - Stringmap.iter push_cci_current ccitab; -(* Stringmap.iter (fun _ -> Libobject.open_object) objtab;*) + Idmap.iter push_cci_current ccitab; +(* Idmap.iter (fun _ -> Libobject.open_object) objtab;*) Stringmap.iter push_mod_current modtab let conditional_push ref = push_cci_current ref (* TODO *) let open_section_contents qid = let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in - Stringmap.iter push_cci_current ccitab; -(* Stringmap.iter (fun _ -> Libobject.open_object) objtab;*) + Idmap.iter push_cci_current ccitab; +(* Idmap.iter (fun _ -> Libobject.open_object) objtab;*) Stringmap.iter push_mod_current modtab let rec rec_open_module_contents qid = let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in - Stringmap.iter push_cci_current ccitab; -(* Stringmap.iter (fun _ -> Libobject.open_object) objtab;*) + Idmap.iter push_cci_current ccitab; +(* Idmap.iter (fun _ -> Libobject.open_object) objtab;*) Stringmap.iter (fun m (sp,_ as mt) -> push_mod_current m mt; diff --git a/library/nametab.mli b/library/nametab.mli index 08aea7ccc..a9a466bb3 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -10,8 +10,8 @@ open Term (* This module contains the table for globalization, which associates global names (section paths) to identifiers. *) -type cci_table = global_reference Stringmap.t -type obj_table = (section_path * Libobject.obj) Stringmap.t +type cci_table = global_reference Idmap.t +type obj_table = (section_path * Libobject.obj) Idmap.t type mod_table = (section_path * module_contents) Stringmap.t and module_contents = Closed of cci_table * obj_table * mod_table diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 1e33ea049..a915148a3 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -129,7 +129,11 @@ let interp_qualid p = | [] -> anomaly "interp_qualid: empty qualified identifier" | l -> let p, r = list_chop (List.length l -1) (List.map outnvar l) in - make_qualid p (List.hd r) + make_qualid p (id_of_string (List.hd r)) + +let maybe_variable = function + | [Nvar (_,s)] -> Some s + | _ -> None let ids_of_ctxt ctxt = Array.to_list @@ -153,16 +157,16 @@ let maybe_constructor env = function | IsMutConstruct ((spi,j),cl) -> IsConstrPat (loc,((spi,j),ids_of_ctxt cl)) | _ -> - (match repr_qualid qid with - | [], s -> + (match maybe_variable l with + | Some s -> warning ("Defined reference "^(string_of_qualid qid) ^" is here considered as a matching variable"); IsVarPat (loc,s) | _ -> error ("This reference does not denote a constructor: " ^(string_of_qualid qid))) with Not_found -> - match repr_qualid qid with - | [], s -> IsVarPat (loc,s) + match maybe_variable l with + | Some s -> IsVarPat (loc,s) | _ -> error ("Unknown qualified constructor: " ^(string_of_qualid qid))) @@ -230,7 +234,7 @@ let ast_to_var (env,impls) (vars1,vars2) loc s = let _ = lookup_id id vars2 in (* Car Fixpoint met les fns définies tmporairement comme vars de sect *) try - let ref = Nametab.locate (make_qualid [] s) in + let ref = Nametab.locate (make_qualid [] (id_of_string s)) in implicits_of_global ref with _ -> [] in RVar (loc, id), [], imps @@ -249,7 +253,7 @@ let translate_qualid act qid = (* Is it a bound variable? *) try match repr_qualid qid with - | [],s -> act.parse_var s, [] + | [],s -> act.parse_var (string_of_id s), [] | _ -> raise Not_found with Not_found -> (* Is it a global reference? *) @@ -276,7 +280,7 @@ let rawconstr_of_qualid env vars loc qid = (* Is it a bound variable? *) try match repr_qualid qid with - | [],s -> ast_to_var env vars loc s + | [],s -> ast_to_var env vars loc (string_of_id s) | _ -> raise Not_found with Not_found -> (* Is it a global reference? *) @@ -589,7 +593,7 @@ let ast_adjust_consts sigma = let id = id_of_string s in if isMeta s then ast else if Idset.mem id env then ast - else adjust_qualid env loc ast (make_qualid [] s) + else adjust_qualid env loc ast (make_qualid [] (id_of_string s)) | Node (loc, "QUALID", p) as ast -> adjust_qualid env loc ast (interp_qualid p) | Slam (loc, None, t) -> Slam (loc, None, dbrec env t) diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml index 94c23ef19..b0a7f3a8a 100644 --- a/parsing/coqlib.ml +++ b/parsing/coqlib.ml @@ -20,10 +20,11 @@ let glob_My_special_variable_nat = ConstRef myvar_path let reference dir s = let dir = "Coq"::"Init"::[dir] in + let id = id_of_string s in try - Nametab.locate_in_absolute_module dir (id_of_string s) + Nametab.locate_in_absolute_module dir id with Not_found -> - anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir s))) + anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir id))) let constant dir s = Declare.constr_of_reference Evd.empty (Global.env()) (reference dir s) diff --git a/parsing/pretty.ml b/parsing/pretty.ml index af94577af..34d3d2980 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -416,9 +416,8 @@ let print_name qid = try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if dir <> [] then raise Not_found; - let name = id_of_string str in - let (c,typ) = Global.lookup_named name in - [< print_named_decl (name,c,typ) >] + let (c,typ) = Global.lookup_named str in + [< print_named_decl (str,c,typ) >] with Not_found -> try let sp = Syntax_def.locate_syntactic_definition qid in diff --git a/parsing/termast.ml b/parsing/termast.ml index b1a2d18d1..026e79324 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -94,7 +94,7 @@ let ast_of_ref = function let ast_of_qualid p = let dir, s = repr_qualid p in - let args = List.map nvar (dir@[s]) in + let args = List.map nvar (dir@[string_of_id s]) in ope ("QUALID", args) (**********************************************************************) @@ -179,7 +179,7 @@ let rec ast_of_raw = function | RVar (_,id) -> let imp = try - let ref = Nametab.locate (make_qualid [] (string_of_id id)) in + let ref = Nametab.locate (make_qualid [] id) in implicits_of_global ref with Not_found -> [] in ast_of_app imp astf astargs diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index c98840d73..9f68b896f 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -186,12 +186,12 @@ let glob_const_nvar loc env qid = try (* We first look for a variable of the current proof *) match repr_qualid qid with - | [],s -> - let id = id_of_string s in + | [],id -> (* lookup_value may raise Not_found *) (match Environ.lookup_named_value id env with | Some _ -> EvalVarRef id - | None -> error (s^" does not denote an evaluable constant")) + | None -> error ((string_of_id id)^ + " does not denote an evaluable constant")) | _ -> raise Not_found with Not_found -> try diff --git a/tactics/auto.ml b/tactics/auto.ml index 7a9ba72b9..e2e719a1d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -421,7 +421,7 @@ let _ = let hyps = Declare.implicit_section_args ref in let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in let _,i = repr_qualid qid in - (id_of_string i, applist (c,section_args)) + (i, applist (c,section_args)) | _-> bad_vernac_args "HintsResolve") lh in let dbnames = if l = [] then ["core"] else List.map (function VARG_IDENTIFIER i -> string_of_id i @@ -438,7 +438,7 @@ let _ = List.map (function | VARG_QUALID qid -> let _,n = repr_qualid qid in - (id_of_string n, global qid) + (n, global qid) | _ -> bad_vernac_args "HintsUnfold") lh in let dbnames = if l = [] then ["core"] else List.map (function @@ -462,7 +462,7 @@ let _ = let c = Declare.constr_of_reference Evd.empty env ref in let hyps = Declare.implicit_section_args ref in let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in - (id_of_string n, applist (c, section_args)) + (n, applist (c, section_args)) | _ -> bad_vernac_args "HintsImmediate") lh in let dbnames = if l = [] then ["core"] else List.map (function @@ -956,7 +956,7 @@ let cvt_autoArgs = let interp_to_add gl = function | (Qualid qid) -> let _,id = repr_qualid qid in - (next_ident_away (id_of_string id) (pf_ids_of_hyps gl), + (next_ident_away id (pf_ids_of_hyps gl), Declare.constr_of_reference Evd.empty (Global.env()) (global qid)) | _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "Qualid expected" >] diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0ce99f904..49042811a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -181,7 +181,7 @@ let _ = (fun () -> add_path dir [Nametab.default_root]) | [VARG_STRING dir ; VARG_QUALID alias] -> let aliasdir,aliasname = repr_qualid alias in - (fun () -> add_path dir (aliasdir@[aliasname])) + (fun () -> add_path dir (aliasdir@[string_of_id aliasname])) | _ -> bad_vernac_args "ADDPATH") (* For compatibility *) @@ -199,7 +199,7 @@ let _ = | [VARG_STRING dir ; VARG_QUALID alias] -> let aliasdir,aliasname = repr_qualid alias in (fun () -> - let alias = aliasdir@[aliasname] in + let alias = aliasdir@[string_of_id aliasname] in add_rec_path dir alias; Nametab.push_library_root (List.hd alias)) | _ -> bad_vernac_args "RECADDPATH") @@ -1369,8 +1369,8 @@ let _ = let cl_of_qualid qid = match repr_qualid qid with - | [], "FUNCLASS" -> Classops.CL_FUN - | [], "SORTCLASS" -> Classops.CL_SORT + | [], id when string_of_id id = "FUNCLASS" -> Classops.CL_FUN + | [], id when string_of_id id = "SORTCLASS" -> Classops.CL_SORT | _ -> Class.class_of_ref (locate_qualid dummy_loc qid) let _ = @@ -1389,8 +1389,7 @@ let _ = let source = cl_of_qualid qids in fun () -> if isid then match repr_qualid qid with - | [], s -> - let id = id_of_string s in + | [], id -> Class.try_add_new_identity_coercion id stre source target | _ -> bad_vernac_args "COERCION" else @@ -1686,7 +1685,7 @@ let _ = if (string_of_id t) = "Tables" then print_tables () else - mSG(print_name (make_qualid [] (string_of_id t)))) + mSG(print_name (make_qualid [] t))) | _ -> bad_vernac_args "TableField") |