From 6da011a8677676462b24940a6171fb22615c3fbb Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 24 Oct 2013 21:29:41 +0000 Subject: More monomorphic List.mem + List.assoc + ... To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/decl_mode/decl_interp.ml | 5 +-- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/extraction/extraction.ml | 8 ++-- plugins/extraction/mlutil.ml | 2 +- plugins/firstorder/unify.ml | 6 +-- plugins/funind/functional_principles_proofs.ml | 4 +- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 6 +-- plugins/funind/glob_termops.ml | 6 +-- plugins/funind/recdef.ml | 6 ++- plugins/omega/coq_omega.ml | 5 +-- plugins/omega/omega.ml | 18 ++++----- plugins/romega/const_omega.ml | 2 +- plugins/xml/cic2acic.ml | 55 ++++++++++++++------------ plugins/xml/xmlcommand.ml | 41 ++++++++++--------- 15 files changed, 88 insertions(+), 80 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 01f90f6c6..bbac10f0f 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -278,8 +278,7 @@ let rec bind_primary_aliases map pat = List.fold_left bind_primary_aliases map1 lpat let bind_secondary_aliases map subst = - Id.Map.fold - (fun ids idp map -> (ids,List.assoc_f Id.equal idp map)::map) subst map + Id.Map.fold (fun ids idp map -> (ids,Id.List.assoc idp map)::map) subst map let bind_aliases patvars subst patt = let map = bind_primary_aliases [] patt in @@ -349,7 +348,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let inject = function Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp) | Thesis (For rec_occ) -> - if not (List.mem rec_occ pat_vars) then + if not (Id.List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 673b749e1..30ed01c49 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1189,7 +1189,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls | End_patt (id,(nparams,nhyps)),[] -> begin - match List.assoc_f Id.equal id args with + match Id.List.assoc id args with [None,br_args] -> let all_metas = List.init (nparams + nhyps) (fun n -> mkMeta (succ n)) in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 947a1a482..c6bb9faa0 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -141,7 +141,8 @@ let sign_with_implicits r s nb_params = | [] -> [] | sign::s -> let sign' = - if sign == Keep && List.mem i implicits then Kill Kother else sign + if sign == Keep && Int.List.mem i implicits + then Kill Kother else sign in sign' :: add_impl (succ i) s in add_impl (1+nb_params) s @@ -657,7 +658,8 @@ and extract_cst_app env mle mlt kn args = (* Can we instantiate types variables for this constant ? *) (* In Ocaml, inside the definition of this constant, the answer is no. *) let instantiated = - if lang () == Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema) + if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints + then var2var' (snd schema) else instantiation schema in (* Then the expected type of this constant. *) @@ -1048,7 +1050,7 @@ let extract_inductive env kn = | [] -> [] | t::l -> let l' = filter (succ i) l in - if isDummy (expand env t) || List.mem i implicits then l' + if isDummy (expand env t) || Int.List.mem i implicits then l' else t::l' in filter (1+ind.ind_nparams) l in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 1e6a1fffc..22e7080e1 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1005,7 +1005,7 @@ let kill_some_lams bl (ids,c) = let kill_dummy_lams c = let ids,c = collect_lams c in let bl = List.map sign_of_id ids in - if not (List.mem Keep bl) then raise Impossible; + if not (List.memq Keep bl) then raise Impossible; let rec fst_kill n = function | [] -> raise Impossible | Kill _ :: bl -> n diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 083108bef..2556460f5 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -32,7 +32,7 @@ let unif t1 t2= match kind_of_term t with Meta i-> (try - head_reduce (List.assoc_f Int.equal i !sigma) + head_reduce (Int.List.assoc i !sigma) with Not_found->t) | _->t in Queue.add (t1,t2) bige; @@ -105,7 +105,7 @@ let mk_rel_inst t= match kind_of_term t with Meta n-> (try - mkRel (d+(List.assoc_f Int.equal n !rel_env)) + mkRel (d+(Int.List.assoc n !rel_env)) with Not_found-> let m= !new_rel in incr new_rel; @@ -117,7 +117,7 @@ let mk_rel_inst t= let unif_atoms i dom t1 t2= try - let t=List.assoc_f Int.equal i (unif t1 t2) in + let t=Int.List.assoc i (unif t1 t2) in if isMeta t then Some (Phantom dom) else Some (Real(mk_rel_inst t,value i t1)) with diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 95aaf4518..8edb16850 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -766,7 +766,7 @@ let build_proof } in build_proof_args do_finalize new_infos g - | Const c when not (List.mem c fnames) -> + | Const c when not (List.mem_f Constant.equal c fnames) -> let new_infos = { dyn_infos with info = (f,args) @@ -915,7 +915,7 @@ let generalize_non_dep hyp g = let hyp_typ = pf_type_of g (mkVar hyp) in let to_revert,_ = Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> - if List.mem hyp hyps + if Id.List.mem hyp hyps || List.exists (Termops.occur_var_in_decl env hyp) keep || Termops.occur_var env hyp hyp_typ || Termops.is_section_variable hyp (* should be dangerous *) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index cb9d12c5e..e65ca94f0 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -367,7 +367,7 @@ let poseq_list_ids lcstr gl = let find_fapp (test:constr -> bool) g : fapp_info list = let pre_res = hdMatchSub (Tacmach.pf_concl g) test in let res = - List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in + List.fold_right (List.add_set Pervasives.(=)) pre_res [] in (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res); res) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 91ea714c1..dd02dfe8d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -126,7 +126,7 @@ let rec replace_var_by_term_in_binder x_id term = function | [] -> [] | (bt,t)::l -> (bt,replace_var_by_term x_id term t):: - if List.mem x_id (ids_of_binder bt) + if Id.List.mem x_id (ids_of_binder bt) then l else replace_var_by_term_in_binder x_id term l @@ -134,14 +134,14 @@ let add_bt_names bt = List.append (ids_of_binder bt) let apply_args ctxt body args = let need_convert_id avoid id = - List.exists (is_free_in id) args || List.mem id avoid + List.exists (is_free_in id) args || Id.List.mem id avoid in let need_convert avoid bt = List.exists (need_convert_id avoid) (ids_of_binder bt) in let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) = match na with - | Name id when List.mem id avoid -> + | Name id when Id.List.mem id avoid -> let new_id = Namegen.next_ident_away id avoid in Name new_id,Id.Map.add id new_id mapping,new_id::avoid | _ -> na,mapping,avoid diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index a16b5f0fe..79cba2c7c 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -199,7 +199,7 @@ let rec alpha_pat excluded pat = let new_id = Indfun_common.fresh_id excluded "_x" in PatVar(loc,Name new_id),(new_id::excluded),Id.Map.empty | PatVar(loc,Name id) -> - if List.mem id excluded + if Id.List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in PatVar(loc,Name new_id),(new_id::excluded), @@ -208,7 +208,7 @@ let rec alpha_pat excluded pat = | PatCstr(loc,constr,patl,na) -> let new_na,new_excluded,map = match na with - | Name id when List.mem id excluded -> + | Name id when Id.List.mem id excluded -> let new_id = Namegen.next_ident_away id excluded in Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty | _ -> na,excluded,Id.Map.empty @@ -412,7 +412,7 @@ let is_free_in id = | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (_,b,CastCoerce) -> is_free_in b and is_free_in_br (_,ids,_,rt) = - (not (List.mem id ids)) && is_free_in rt + (not (Id.List.mem id ids)) && is_free_in rt in is_free_in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 57019b3fa..a77968092 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -294,7 +294,9 @@ 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 "^Id.to_string x) + | Var x -> + if Id.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 @@ -652,7 +654,7 @@ let mkDestructEq : let to_revert = Util.List.map_filter (fun (id, _, t) -> - if List.mem id not_on_hyp || not (Termops.occur_term expr t) + if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in let type_of_expr = pf_type_of g expr in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 5c057231a..4f96d7209 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -140,8 +140,7 @@ let rev_assoc k = let tag_hypothesis,tag_of_hyp, hyp_of_tag = let l = ref ([]:(Id.t * int) list) in (fun h id -> l := (h,id):: !l), - (fun h -> - try List.assoc_f Id.equal h !l with Not_found -> failwith "tag_hypothesis"), + (fun h -> try Id.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 = @@ -1022,7 +1021,7 @@ let replay_history tactic_normalisation = begin try tclTHEN - (List.assoc_f Id.equal (hyp_of_tag e.id) tactic_normalisation) + (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation) (loop l) with Not_found -> loop l end | NEGATE_CONTRADICT (e2,e1,b) :: l -> diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index b74faf30b..4e9ca6ffc 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -546,30 +546,30 @@ let rec depend relie_on accu = function | act :: l -> begin match act with | DIVIDE_AND_APPROX (e,_,_,_) -> - if List.mem e.id relie_on then depend relie_on (act::accu) l + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l | EXACT_DIVIDE (e,_) -> - if List.mem e.id relie_on then depend relie_on (act::accu) l + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l | WEAKEN (e,_) -> - if List.mem e relie_on then depend relie_on (act::accu) l + if Int.List.mem e relie_on then depend relie_on (act::accu) l else depend relie_on accu l | SUM (e,(_,e1),(_,e2)) -> - if List.mem e relie_on then + if Int.List.mem e relie_on then depend (e1.id::e2.id::relie_on) (act::accu) l else depend relie_on accu l | STATE {st_new_eq=e;st_orig=o} -> - if List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l + if Int.List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l else depend relie_on accu l | HYP e -> - if List.mem e.id relie_on then depend relie_on (act::accu) l + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l | FORGET_C _ -> depend relie_on accu l | FORGET _ -> depend relie_on accu l | FORGET_I _ -> depend relie_on accu l | MERGE_EQ (e,e1,e2) -> - if List.mem e relie_on then + if Int.List.mem e relie_on then depend (e1.id::e2::relie_on) (act::accu) l else depend relie_on accu l @@ -673,7 +673,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = try let _ = loop2 sys in raise NO_CONTRADICTION with UNSOLVABLE -> let relie_on,path = depend [] [] (history ()) in - let dc,_ = List.partition (fun (_,id,_) -> List.mem id relie_on) decomp in + let dc,_ = List.partition (fun (_,id,_) -> Int.List.mem id relie_on) decomp in let red = List.map (fun (x,_,_) -> x) dc in (red,relie_on,decomp,path)) sys_exploded @@ -705,7 +705,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = let s2' = List.map remove_int s2 in let (r1,relie1) = solve s1' and (r2,relie2) = solve s2' in - let (eq,id1,id2) = Util.List.assoc_f Int.equal id explode_map in + let (eq,id1,id2) = Int.List.assoc id explode_map in [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.List.union Int.equal relie1 relie2 with FULL_SOLUTION (x0,x1) -> (x0,x1) diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index af833dacb..5416e936c 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -23,7 +23,7 @@ let string_of_global r = | [] -> "" | m::_ -> let s = Names.Id.to_string m in - if List.mem s meaningful_submodule then s^"." else "" + if Util.String.List.mem s meaningful_submodule then s^"." else "" in prefix^(Names.Id.to_string (Nametab.basename_of_global r)) diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 26fab4ac2..bf46065d0 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -13,6 +13,8 @@ (************************************************************************) open Pp +open Util +open Names (* Utility Functions *) @@ -37,7 +39,7 @@ let get_module_path_of_full_path path = (*CSC: not exist two modules whose dir_paths are one a prefix of the other *) let remove_module_dirpath_from_dirpath ~basedir dir = if Libnames.is_dirpath_prefix_of basedir dir then - let ids = Names.DirPath.repr dir in + let ids = DirPath.repr dir in let rec remove_firsts n l = match n,l with (0,l) -> l @@ -47,11 +49,11 @@ let remove_module_dirpath_from_dirpath ~basedir dir = let ids' = List.rev (remove_firsts - (List.length (Names.DirPath.repr basedir)) + (List.length (DirPath.repr basedir)) (List.rev ids)) in ids' - else Names.DirPath.repr dir + else DirPath.repr dir ;; @@ -60,21 +62,22 @@ let get_uri_of_var v pvars = function [] -> Errors.error ("Variable "^v^" not found") | he::tl as modules -> - let dirpath = Names.DirPath.make modules in - if List.mem (Names.Id.of_string v) (Decls.last_section_hyps dirpath) then + let dirpath = DirPath.make modules in + if Id.List.mem (Id.of_string v) (Decls.last_section_hyps dirpath) + then modules - else + else search_in_open_sections tl in let path = - if List.mem v pvars then + if String.List.mem v pvars then [] else - search_in_open_sections (Names.DirPath.repr (Lib.cwd ())) + search_in_open_sections (DirPath.repr (Lib.cwd ())) in "cic:" ^ List.fold_left - (fun i x -> "/" ^ Names.Id.to_string x ^ i) "" path + (fun i x -> "/" ^ Id.to_string x ^ i) "" path ;; type tag = @@ -105,31 +108,31 @@ let ext_of_tag = exception FunctorsXMLExportationNotImplementedYet;; let subtract l1 l2 = - let l1' = List.rev (Names.DirPath.repr l1) in - let l2' = List.rev (Names.DirPath.repr l2) in + let l1' = List.rev (DirPath.repr l1) in + let l2' = List.rev (DirPath.repr l2) in let rec aux = function he::tl when tl = l2' -> [he] | he::tl -> he::(aux tl) | [] -> assert (l2' = []) ; [] in - Names.DirPath.make (List.rev (aux l1')) + DirPath.make (List.rev (aux l1')) ;; let token_list_of_path dir id tag = let token_list_of_dirpath dirpath = - List.rev_map Names.Id.to_string (Names.DirPath.repr dirpath) in - token_list_of_dirpath dir @ [Names.Id.to_string id ^ "." ^ (ext_of_tag tag)] + List.rev_map Id.to_string (DirPath.repr dirpath) in + token_list_of_dirpath dir @ [Id.to_string id ^ "." ^ (ext_of_tag tag)] let token_list_of_kernel_name tag = let id,dir = match tag with | Variable kn -> - Names.Label.to_id (Names.label kn), Lib.cwd () + Label.to_id (Names.label kn), Lib.cwd () | Constant con -> - Names.Label.to_id (Names.con_label con), + Label.to_id (Names.con_label con), Lib.remove_section_part (Globnames.ConstRef con) | Inductive kn -> - Names.Label.to_id (Names.mind_label kn), + Label.to_id (Names.mind_label kn), Lib.remove_section_part (Globnames.IndRef (kn,0)) in token_list_of_path dir id (etag_of_tag tag) @@ -188,7 +191,7 @@ let typeur sigma metamap = let rec type_of env cstr= match Term.kind_of_term cstr with | T.Meta n -> - (try T.strip_outer_cast (Util.List.assoc_f Int.equal n metamap) + (try T.strip_outer_cast (Int.List.assoc n metamap) with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term")) | T.Rel n -> let (_,_,ty) = Environ.lookup_rel n env in @@ -198,7 +201,7 @@ let typeur sigma metamap = let (_,_,ty) = Environ.lookup_named id env in ty with Not_found -> - Errors.anomaly ~label:"type_of" (str "variable " ++ Names.Id.print id ++ str " unbound")) + Errors.anomaly ~label:"type_of" (str "variable " ++ Id.print id ++ str " unbound")) | T.Const c -> let cb = Environ.lookup_constant c env in Typeops.type_of_constant_type env (cb.Declarations.const_type) @@ -447,8 +450,8 @@ print_endline "PASSATO" ; flush stdout ; let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in let he1'' = String.concat "/" - (List.rev_map Names.Id.to_string he1') ^ "/" - ^ (Names.Id.to_string he1_id) ^ ".var" + (List.rev_map Id.to_string he1') ^ "/" + ^ (Id.to_string he1_id) ^ ".var" in (he1'',he2)::subst, extra_args, uninst in @@ -493,13 +496,13 @@ print_endline "PASSATO" ; flush stdout ; Acic.ARel (fresh_id'', n, List.nth idrefs (n-1), id) | Term.Var id -> let pvars = Termops.ids_of_named_context (Environ.named_context env) in - let pvars = List.map Names.Id.to_string pvars in - let path = get_uri_of_var (Names.Id.to_string id) pvars in + let pvars = List.map Id.to_string pvars in + let path = get_uri_of_var (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'' ; Acic.AVar - (fresh_id'', path ^ "/" ^ (Names.Id.to_string id) ^ ".var") + (fresh_id'', path ^ "/" ^ (Id.to_string id) ^ ".var") | Term.Evar (n,l) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then @@ -602,7 +605,7 @@ print_endline "PASSATO" ; flush stdout ; | Term.LetIn (n,s,t,d) -> let id = match n with - Names.Anonymous -> Names.Id.of_string "_X" + Names.Anonymous -> Id.of_string "_X" | Names.Name id -> id in let n' = @@ -877,7 +880,7 @@ let acic_object_of_cic_object sigma obj = in let dummy_never_used = let s = "dummy_never_used" in - Acic.ARel (s,99,s,Names.Id.of_string s) + Acic.ARel (s,99,s,Id.of_string s) in final_env,final_idrefs, (hid,(n,Acic.Def (at,dummy_never_used)))::atl diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index abd6b3b73..83a4d425b 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -21,6 +21,8 @@ let verbose = ref false;; let print_if_verbose s = if !verbose then print_string s;; open Decl_kinds +open Names +open Util (* filter_params pvars hyps *) (* filters out from pvars (which is a list of lists) all the variables *) @@ -35,18 +37,19 @@ let filter_params pvars hyps = let ids' = id::ids in let ids'' = "cic:/" ^ - String.concat "/" (List.rev_map Names.Id.to_string ids') in + String.concat "/" (List.rev_map Id.to_string ids') in let he' = - ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in + ids'', List.rev (List.filter (function x -> String.List.mem x hyps) he) + in let tl' = aux ids' tl in match he' with _,[] -> tl' | _,_ -> 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 (Id.of_string "dummy") in let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in - aux (Names.DirPath.repr modulepath) (List.rev pvars) + aux (DirPath.repr modulepath) (List.rev pvars) ;; (* The computation is very inefficient, but we can't do anything *) @@ -54,15 +57,15 @@ let filter_params pvars hyps = (* module. *) let search_variables () = let cwd = Lib.cwd () in - let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in + let cwdsp = Libnames.make_path cwd (Id.of_string "dummy") in let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in let rec aux = function [] -> [] | he::tl as modules -> let one_section_variables = - let dirpath = Names.DirPath.make (modules @ Names.DirPath.repr modulepath) in - let t = List.map Names.Id.to_string (Decls.last_section_hyps dirpath) in + let dirpath = DirPath.make (modules @ DirPath.repr modulepath) in + let t = List.map Id.to_string (Decls.last_section_hyps dirpath) in [he,t] in one_section_variables @ aux tl @@ -110,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 Names.Id.to_string (Names.DirPath.repr (Lib.library_dp ())) in + let toks = List.map Id.to_string (DirPath.repr (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") @@ -150,7 +153,7 @@ let print_object uri obj sigma filename = let string_list_of_named_context_list = List.map - (function (n,_,_) -> Names.Id.to_string n) + (function (n,_,_) -> Id.to_string n) ;; (* Function to collect the variables that occur in a term. *) @@ -159,7 +162,7 @@ let string_list_of_named_context_list = let find_hyps t = let rec aux l t = match Term.kind_of_term t with - Term.Var id when not (List.mem id l) -> + Term.Var id when not (Id.List.mem id l) -> let (_,bo,ty) = Global.lookup_named id in let boids = match bo with @@ -193,7 +196,7 @@ let find_hyps t = and map_and_filter l = function [] -> [] - | (n,_,_)::tl when not (List.mem n l) -> n::(map_and_filter l tl) + | (n,_,_)::tl when not (Id.List.mem n l) -> n::(map_and_filter l tl) | _::tl -> map_and_filter l tl in aux [] t @@ -208,11 +211,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.Id.to_string hyps' in + let hyps'' = List.map Id.to_string hyps' in let variables = search_variables () in let params = filter_params variables hyps'' in Acic.Variable - (Names.Id.to_string id, unsharedbody, Unshare.unshare typ, params) + (Id.to_string id, unsharedbody, Unshare.unshare typ, params) ;; @@ -222,10 +225,10 @@ let mk_constant_obj id bo ty variables hyps = let params = filter_params variables hyps in match bo with None -> - Acic.Constant (Names.Id.to_string id,None,ty,params) + Acic.Constant (Id.to_string id,None,ty,params) | Some c -> Acic.Constant - (Names.Id.to_string id, Some (Unshare.unshare c), ty,params) + (Id.to_string id, Some (Unshare.unshare c), ty,params) ;; let mk_inductive_obj sp mib packs variables nparams hyps finite = @@ -371,7 +374,7 @@ let print internal glob_ref kind xml_library_root = let (_,body,typ) = Global.lookup_named id in Cic2acic.Variable kn,mk_variable_obj id body typ | Globnames.ConstRef kn -> - let id = Names.Label.to_id (Names.con_label kn) in + let id = Label.to_id (Names.con_label kn) in let cb = Global.lookup_constant kn in let val0 = Declareops.body_of_constant cb in let typ = cb.Declarations.const_type in @@ -444,7 +447,7 @@ let _ = (* I saved in the Pfedit.set_xml_cook_proof callback. *) let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in show_pftreestate internal fn pftreestate - (Names.Label.to_id (Names.con_label kn)) ; + (Label.to_id (Names.con_label kn)) ; proof_to_export := None) ;; @@ -508,7 +511,7 @@ let _ = Hook.set Lexer.xml_output_comment (theory_output_string ~do_not_quote:tr let uri_of_dirpath dir = "/" ^ String.concat "/" - (List.rev_map Names.Id.to_string (Names.DirPath.repr dir)) + (List.rev_map Id.to_string (DirPath.repr dir)) ;; let _ = @@ -527,5 +530,5 @@ let _ = Hook.set Library.xml_require (fun d -> theory_output_string (Printf.sprintf "Require %s.
" - (uri_of_dirpath d) (Names.DirPath.to_string d))) + (uri_of_dirpath d) (DirPath.to_string d))) ;; -- cgit v1.2.3