diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cList.ml | 10 | ||||
| -rw-r--r-- | lib/cList.mli | 3 | ||||
| -rw-r--r-- | lib/flags.ml | 17 | ||||
| -rw-r--r-- | lib/flags.mli | 10 | ||||
| -rw-r--r-- | lib/profile.ml | 42 | ||||
| -rw-r--r-- | lib/profile.mli | 4 |
6 files changed, 80 insertions, 6 deletions
diff --git a/lib/cList.ml b/lib/cList.ml index 36dad32352..93ba0637e6 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -479,14 +479,14 @@ let rec find_map f = function let uniquize l = let visited = Hashtbl.create 23 in - let rec aux acc = function - | h::t -> if Hashtbl.mem visited h then aux acc t else + let rec aux acc changed = function + | h::t -> if Hashtbl.mem visited h then aux acc true t else begin Hashtbl.add visited h h; - aux (h::acc) t + aux (h::acc) changed t end - | [] -> List.rev acc - in aux [] l + | [] -> if changed then List.rev acc else l + in aux [] false l (** [sort_uniquize] might be an alternative to the hashtbl-based [uniquize], when the order of the elements is irrelevant *) diff --git a/lib/cList.mli b/lib/cList.mli index 15900260ce..01ae839601 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -127,7 +127,8 @@ sig there is none. *) val uniquize : 'a list -> 'a list - (** Return the list of elements without duplicates. *) + (** Return the list of elements without duplicates. + This is the list unchanged if there was none. *) val sort_uniquize : 'a cmp -> 'a list -> 'a list (** Return a sorted and de-duplicated version of a list, diff --git a/lib/flags.ml b/lib/flags.ml index 9b932946ca..530617b0cb 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -60,6 +60,8 @@ let async_proofs_is_worker () = let debug = ref false +let profile = false + let print_emacs = ref false let term_quality = ref false @@ -134,6 +136,21 @@ let auto_intros = ref true let make_auto_intros flag = auto_intros := flag let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros +let universe_polymorphism = ref false +let make_universe_polymorphism b = universe_polymorphism := b +let is_universe_polymorphism () = !universe_polymorphism + +let local_polymorphic_flag = ref None +let use_polymorphic_flag () = + match !local_polymorphic_flag with + | Some p -> local_polymorphic_flag := None; p + | None -> is_universe_polymorphism () +let make_polymorphic_flag b = + local_polymorphic_flag := Some b + +(** [program_mode] tells that Program mode has been activated, either + globally via [Set Program] or locally via the Program command prefix. *) + let program_mode = ref false let is_program_mode () = !program_mode diff --git a/lib/flags.mli b/lib/flags.mli index ebd11ee774..57e31394e6 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -24,6 +24,8 @@ val async_proofs_is_worker : unit -> bool val debug : bool ref +val profile : bool + val print_emacs : bool ref val term_quality : bool ref @@ -72,6 +74,14 @@ val is_term_color : unit -> bool val program_mode : bool ref val is_program_mode : unit -> bool +(** Global universe polymorphism flag. *) +val make_universe_polymorphism : bool -> unit +val is_universe_polymorphism : unit -> bool + +(** Local universe polymorphism flag. *) +val make_polymorphic_flag : bool -> unit +val use_polymorphic_flag : unit -> bool + val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit diff --git a/lib/profile.ml b/lib/profile.ml index 6a1b45a397..798f895fa3 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -657,6 +657,48 @@ let profile7 e f a b c d g h i = last_alloc := get_alloc (); raise reraise +let profile8 e f a b c d g h i j = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g h i j in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + let print_logical_stats a = let (c, s, d) = CObj.obj_stats a in Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d diff --git a/lib/profile.mli b/lib/profile.mli index 812fd8b1e4..a7d9cabe5c 100644 --- a/lib/profile.mli +++ b/lib/profile.mli @@ -100,6 +100,10 @@ val profile7 : profile_key -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h +val profile8 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) + -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i (** Some utilities to compute the logical and physical sizes and depth |