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/xml/cic2acic.ml | 55 +++++++++++++++++++++++++---------------------- plugins/xml/xmlcommand.ml | 41 +++++++++++++++++++---------------- 2 files changed, 51 insertions(+), 45 deletions(-) (limited to 'plugins/xml') 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