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/xml/acic.ml | 16 ++++++++-------- plugins/xml/acic2Xml.ml4 | 20 ++++++++++---------- plugins/xml/cic2acic.ml | 24 ++++++++++++------------ plugins/xml/xmlcommand.ml | 22 +++++++++++----------- 4 files changed, 41 insertions(+), 41 deletions(-) (limited to 'plugins/xml') 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