diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-28 15:43:40 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-28 15:43:40 +0000 |
| commit | 13cab8364beb03586e0e6972f00c20664d83a4b7 (patch) | |
| tree | a2760dfd863d18f29ddae4b59d79495f12de8ac6 /checker/check.ml | |
| parent | 568fe8d4f87b5deffe781fe81185c678f8d2684e (diff) | |
Safe_typing+Libary: use some arrays instead of lists in vo structures
Very little space saved this way, but it would hurt either...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16375 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/checker/check.ml b/checker/check.ml index 03a18280a..eb4016f5f 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -42,8 +42,8 @@ type library_disk = { md_name : compilation_unit_name; md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library; md_objects : library_objects; - md_deps : (compilation_unit_name * Digest.t) list; - md_imports : compilation_unit_name list } + md_deps : (compilation_unit_name * Digest.t) array; + md_imports : compilation_unit_name array } (************************************************************************) (*s Modules on disk contain the following informations (after the magic @@ -56,7 +56,7 @@ type library_t = { library_name : compilation_unit_name; library_filename : CUnix.physical_path; library_compiled : Safe_typing.compiled_library; - library_deps : (compilation_unit_name * Digest.t) list; + library_deps : (compilation_unit_name * Digest.t) array; library_digest : Digest.t } module LibraryOrdered = @@ -330,8 +330,9 @@ let rec intern_library seen (dir, f) needed = let m = intern_from_file (dir,f) in let seen' = LibrarySet.add dir seen in let deps = - List.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps in - (dir,m) :: List.fold_right (intern_library seen') deps needed + Array.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps + in + (dir,m) :: Array.fold_right (intern_library seen') deps needed (* Compute the reflexive transitive dependency closure *) let rec fold_deps seen ff (dir,f) (s,acc) = @@ -339,9 +340,9 @@ let rec fold_deps seen ff (dir,f) (s,acc) = if LibrarySet.mem dir s then (s,acc) else let deps = get_deps (dir,f) in - let deps = List.map (fun (d,_) -> try_locate_absolute_library d) deps in + let deps = Array.map (fun (d,_) -> try_locate_absolute_library d) deps in let seen' = LibrarySet.add dir seen in - let (s',acc') = List.fold_right (fold_deps seen' ff) deps (s,acc) in + let (s',acc') = Array.fold_right (fold_deps seen' ff) deps (s,acc) in (LibrarySet.add dir s', ff dir acc') and fold_deps_list seen ff modl needed = |