diff --git a/src/solver.ml b/src/solver.ml
index 2c552813428a3c5d1efe5acd426380d3cf10713d..c01b8722593207464c2fb7e49c2dc7f9525c2fb4 100644
--- a/src/solver.ml
+++ b/src/solver.ml
@@ -264,6 +264,24 @@ module type Dem' = sig
end
+module type DemFast' = sig
+ type delayed
+ type d
+
+ module Data: sig
+ type t = d
+ val print: Format.formatter -> t -> unit
+ end
+
+ val key: (unit, Data.t) dem
+
+ (** not immediate and never killed *)
+ val throttle: int (** todo int ref? *)
+ (** number of time run in a row *)
+ val wakeup: delayed -> Data.t Events.Fired.event -> unit
+
+end
+
module DecTag = DInt
module type DomTable' = sig
@@ -311,12 +329,15 @@ module type DemTable' = sig
end
+
+type ('k,'d,'delayed) demtable' =
+| DemT': (module DemTable' with type delayed = 'delayed
+ and type dk = 'k
+ and type dd = 'd) -> ('k,'d,'delayed) demtable'
+| DemFastT': 'd Events.Fired.event list -> (unit,'d,'delayed) demtable'
+
module VDemTable = Dem.MkVector
- (struct type ('k,'d,'delayed) t =
- (module DemTable' with type delayed = 'delayed
- and type dk = 'k
- and type dd = 'd)
- end)
+ (struct type ('k,'d,'delayed) t = ('k,'d,'delayed) demtable' end)
type decdone =
| NoDec
@@ -355,8 +376,15 @@ and delayed_t = {
todo_ext_action : action_ext Queue.t;
sched_daemon : daemon_key -> unit;
sched_decision : decision -> unit;
+ (** dem fast *)
+ mutable dem_fast_todo : dem_fast_todo;
}
+and dem_fast_todo =
+| DemFastTodo:
+ (unit,'d) dem * int ref * 'd Events.Fired.event Queue.t -> dem_fast_todo
+| DemFastNone
+
and action_dom =
| SetDom : pexp * 'a dom * Cl.t * 'a -> action_dom
| UnsetDom : pexp * 'a dom * Cl.t -> action_dom
@@ -397,7 +425,8 @@ let mk_dumb_delayed () = { env = Obj.magic 0;
sched_daemon = (fun _ -> (assert false : unit));
(* should never be called *)
sched_decision = (fun _ -> (assert false : unit));
- (* should never be called *)
+ (* should never be called *)
+ dem_fast_todo = DemFastNone;
}
let dumb_delayed = mk_dumb_delayed ()
@@ -436,6 +465,7 @@ let new_handler t =
module type Dom = Dom' with type delayed := delayed_t
module type Sem = Sem' with type delayed := delayed_t
module type Dem = Dem' with type delayed := delayed_t
+module type DemFast = DemFast' with type delayed := delayed_t
module VDom = Dom.MkVector
(struct type ('a,'unedeed) t =
@@ -445,11 +475,13 @@ module VSem = Sem.MkVector
(struct type ('a,'unedeed) t =
(module Sem with type t = 'a)
end)
+
+type ('k,'d) demmod =
+| Dem: (module Dem with type k = 'k and type d = 'd) -> ('k,'d) demmod
+| DemFast: (module DemFast with type d = 'd) -> (unit,'d) demmod
+
module VDem = Dem.MkVector
- (struct type ('k,'d,'unedeed) t =
- (module Dem with type k = 'k
- and type d = 'd)
- end)
+ (struct type ('k,'d,'unedeed) t = ('k,'d) demmod end)
let defined_dom : unit VDom.t = VDom.create 8
let defined_sem : unit VSem.t = VSem.create 8
@@ -484,7 +516,19 @@ module RegisterDem (D:Dem) = struct
assert (if not (VDem.is_uninitialized defined_dem D.key)
then raise AlreadyRegisteredKey else true);
let dem = (module D: Dem with type k = D.k and type d = D.d) in
- VDem.set defined_dem D.key dem
+ VDem.set defined_dem D.key (Dem dem)
+
+end
+
+module RegisterDemFast (D:DemFast) = struct
+
+ let () =
+ assert (D.throttle > 0);
+ VDem.inc_size D.key defined_dem;
+ assert (if not (VDem.is_uninitialized defined_dem D.key)
+ then raise AlreadyRegisteredKey else true);
+ let dem = (module D: DemFast with type d = D.d) in
+ VDem.set defined_dem D.key (DemFast dem)
end
@@ -498,13 +542,12 @@ let get_sem k =
then raise UnregisteredKey else true);
VSem.get defined_sem k
-let get_dem : ('k,'d) dem -> (module Dem with type k = 'k and type d = 'd)
+let get_dem : ('k,'d) dem -> ('k,'d) demmod
= fun (k: ('k,'d) dem) ->
assert (if VDem.is_uninitialized defined_dem k
then raise UnregisteredKey else true);
VDem.get defined_dem k
-
let print_dom (type a) (k : a dom) fmt s =
let dom = get_dom k in
let module D = (val dom : Dom with type t = a) in
@@ -519,15 +562,24 @@ let () = Print.psem.Print.psem <- print_sem
let print_dem_key (type k) (type d) (k : (k,d) dem) fmt s =
let dem = get_dem k in
- let module S = (val dem : Dem with type k = k and type d = d) in
- S.Key.print fmt s
+ match dem with
+ | Dem dem ->
+ let module S = (val dem : Dem with type k = k and type d = d) in
+ S.Key.print fmt s
+ | DemFast _ ->
+ DUnit.print fmt ( () : k)
let () = Print.pdem_key.Print.pdem_key <- print_dem_key
let print_dem_data (type k) (type d) (k : (k,d) dem) fmt s =
let dem = get_dem k in
- let module S = (val dem : Dem with type k = k and type d = d) in
- S.Data.print fmt s
+ match dem with
+ | Dem dem ->
+ let module S = (val dem : Dem with type k = k and type d = d) in
+ S.Data.print fmt s
+ | DemFast dem ->
+ let module S = (val dem : DemFast with type d = d) in
+ S.Data.print fmt s
let () = Print.pdem_data.Print.pdem_data <- print_dem_data
@@ -535,7 +587,6 @@ let () = Print.pdem_data.Print.pdem_data <- print_dem_data
module type DomTable = DomTable' with type delayed = delayed_t
module type SemTable = SemTable' with type delayed = delayed_t
-module type DemTable = DemTable' with type delayed = delayed_t
let get_table_dom : t -> 'a dom -> (module DomTable with type dt = 'a)
= fun (type a) t k ->
@@ -578,27 +629,26 @@ let get_table_sem : t -> 'a sem -> (module SemTable with type dt = 'a)
: SemTable' with type dt = a and type delayed = delayed_t)
: SemTable with type dt = a)
-let get_table_dem : t -> ('k,'d) dem -> (module DemTable with type dk = 'k
- and type dd = 'd)
- = fun (type k) (type d) t k ->
+let get_table_dem : type k d. t -> (k,d) dem -> (k,d,delayed_t) demtable'
+ = fun t k ->
assert (if VDem.is_uninitialized defined_dem k
then raise UnregisteredKey else true);
VDemTable.inc_size k t.dem;
if VDemTable.is_uninitialized t.dem k then
let dem = get_dem k in
- let module DemTable = struct
- type delayed = delayed_t
- type dk = k
- type dd = d
- module D = (val dem : Dem with type k = dk and type d = dd)
- let state = D.Key.M.empty
- end in
- (module DemTable : DemTable with type dk = k and type dd = d)
+ match dem with
+ | Dem dem ->
+ let module DemTable = struct
+ type delayed = delayed_t
+ type dk = k
+ type dd = d
+ module D = (val dem : Dem with type k = dk and type d = dd)
+ let state = D.Key.M.empty
+ end in
+ DemT' (module DemTable)
+ | DemFast _ -> DemFastT' []
else
- (module (val VDemTable.get t.dem k
- : DemTable' with type dk = k and type dd = d
- and type delayed = delayed_t)
- : DemTable with type dk = k and type dd = d)
+ VDemTable.get t.dem k
exception NotNormalized
@@ -784,11 +834,14 @@ module Delayed = struct
List.iter (fun wevent ->
match wevent with
| Events.Wait.Event (dem,k,d) ->
- let f (type k) (type d) (dem:(k,d)dem) (k:k) (d:d) =
- let event = translate.Events.Fired.translate info d in
- let demtable = get_table_dem t.env dem in
- let module DemTable =
- (val demtable : DemTable with type dk = k and type dd = d) in
+ let f (type k) (type d) (dem:(k,d)dem) (k:k) (d:d) event =
+ match get_table_dem t.env dem with
+ | DemFastT' events ->
+ if events = [] then
+ t.sched_daemon (DaemonKey (dem,k));
+ VDemTable.set t.env.dem dem (DemFastT'(event::events))
+ | DemT' demtable ->
+ let module DemTable = (val demtable) in
try
let rec update_state k =
let module LE = struct exception ToRedirect of k end in
@@ -820,9 +873,21 @@ module Delayed = struct
include DemTable
let state = update_state k
end in
- VDemTable.set t.env.dem dem (module DemTable')
+ VDemTable.set t.env.dem dem (DemT'(module DemTable'))
with Exit -> () in
- f dem k d
+ let event = translate.Events.Fired.translate info d in
+ match t.dem_fast_todo with
+ | DemFastNone -> f dem k d event
+ | DemFastTodo(_,nb,q) when !nb == 0 ->
+ assert (Queue.is_empty q); f dem k d event
+ | DemFastTodo(dem',nb,q) ->
+ match Dem.Eq.eq_type dem' dem with
+ | None -> f dem k d event
+ | Some (Eqtype.Eq, Eqtype.Eq) ->
+ Queue.add event q;
+ decr nb;
+ assert (!nb >= 0);
+
) events
@@ -830,10 +895,11 @@ module Delayed = struct
let mark_dem :
type k d. t -> (k,d) dem -> k -> unit =
fun t dem k ->
+ match get_table_dem t.env dem with
+ | DemFastT' _ -> ()
+ | DemT' demtable ->
try
- let demtable = get_table_dem t.env dem in
- let module DemTable =
- (val demtable : DemTable with type dk = k and type dd = d) in
+ let module DemTable = (val demtable) in
let module DemTable' = struct
include DemTable
let state = DemTable.D.Key.M.change (function
@@ -843,7 +909,7 @@ module Delayed = struct
| Some (Alive _) -> raise Exit)
k DemTable.state
end in
- VDemTable.set t.env.dem dem (module DemTable')
+ VDemTable.set t.env.dem dem (DemT' (module DemTable'))
with Exit -> ()
let attach_events :
@@ -1015,20 +1081,24 @@ module Delayed = struct
| SRedirected of 'k
let is_attached (type k) (type d) t (dem: (k,d) dem) (k:k) =
- let demtable = get_table_dem t.env dem in
- let module DemTable =
- (val demtable : DemTable with type dk = k and type dd = d) in
+ match get_table_dem t.env dem with
+ | DemFastT' _ -> SAlive
+ | DemT' demtable ->
+ let module DemTable = (val demtable) in
match DemTable.D.Key.M.find_opt k DemTable.state with
| None -> SUnborn
| Some (Alive _) -> SAlive
| Some Dead -> SDead
| Some (Redirected k') -> SRedirected k'
+ exception CantBeKilled
+
let kill_dem (type k) (type d) t (dem: (k,d) dem) (k:k) =
+ match get_table_dem t.env dem with
+ | DemFastT' _ -> raise CantBeKilled
+ | DemT' demtable ->
try
- let demtable = get_table_dem t.env dem in
- let module DemTable =
- (val demtable : DemTable with type dk = k and type dd = d) in
+ let module DemTable = (val demtable) in
Debug.dprintf4 debug "[Solver] @[Kill dem %a %a@]@."
Dem.print dem DemTable.D.Key.print k;
let module DemTable' = struct
@@ -1038,7 +1108,7 @@ module Delayed = struct
| _ -> Some Dead)
k DemTable.state
end in
- VDemTable.set t.env.dem dem (module DemTable')
+ VDemTable.set t.env.dem dem (DemT' (module DemTable'))
with Exit -> ()
let are_waiting_cl_change
@@ -1514,6 +1584,48 @@ module Delayed = struct
add_pending_unset_dom d pexp dom cl
+(**
+ DemFast
+*)
+
+
+ let rec do_pending_daemon_fast :
+ type d. t -> (unit,d) dem -> d Events.Fired.t -> unit =
+ fun delayed dem events ->
+ assert (events != []);
+ match get_dem dem with
+ | Dem _ -> assert false
+ | DemFast demfast ->
+ let module S = (val demfast) in
+ let rec last_rev q n = function
+ | [] -> [],n
+ | a::l ->
+ let rem,n = last_rev q n l in
+ if n > 0 then begin
+ assert (rem == []);
+ Queue.add a q;
+ rem,(n-1)
+ end
+ else a::rem, n in
+ let q = Queue.create () in
+ let events,n = last_rev q S.throttle events in
+ VDemTable.set delayed.env.dem dem (DemFastT' events);
+ assert (delayed.dem_fast_todo == DemFastNone);
+ delayed.dem_fast_todo <- DemFastTodo(dem,ref n,q);
+ let rec run_one () =
+ match delayed.dem_fast_todo with
+ | DemFastNone -> assert false
+ | DemFastTodo(dem',r,q) when Queue.is_empty q ->
+ delayed.dem_fast_todo <- DemFastNone
+ | DemFastTodo(dem',r,q) ->
+ assert (!r >= 0);
+ match Dem.Eq.coerce_type dem' dem with
+ | Eqtype.Eq, Eqtype.Eq ->
+ S.wakeup delayed (Queue.pop q);
+ flush delayed;
+ run_one () in
+ run_one ()
+
(** TODO: WakeUp what they modify (not efficient) but for now simple
can perhaps first apply what the daemon does first, then
readd it to watch list then apply the others pending
@@ -1522,10 +1634,13 @@ module Delayed = struct
Deamons modify and add wait what todo is it currently a
problem?
*)
- let do_pending_daemon (type k) (type d) delayed (dem : (k,d) dem) (k : k) =
- let demtable = get_table_dem delayed.env dem in
- let module DemTable =
- (val demtable : DemTable with type dk = k and type dd = d) in
+ and do_pending_daemon' : type k d. t -> (k,d) dem -> k -> unit =
+ fun delayed dem k ->
+ match get_table_dem delayed.env dem with
+ | DemFastT' [] -> ()
+ | DemFastT' events -> do_pending_daemon_fast delayed dem events
+ | DemT' demtable ->
+ let module DemTable = (val demtable) in
match DemTable.D.Key.M.find k (DemTable.state) with
| Dead ->
Debug.dprintf4 debug "[Solver] @[Daemon %a for %a is dead@]@."
@@ -1546,7 +1661,7 @@ module Delayed = struct
let state = DemTable.D.Key.M.add k (Alive []) (DemTable.state)
end
in
- VDemTable.set delayed.env.dem dem (module DemTable');
+ VDemTable.set delayed.env.dem dem (DemT' (module DemTable'));
(** wakeup *)
let alive = DemTable.D.wakeup delayed k events in
(** delayed can be modified *)
@@ -1557,25 +1672,27 @@ module Delayed = struct
| AliveRedirected k' -> mark_dem delayed dem k'; Redirected k'
| AliveReattached -> assert false in
Debug.dprintf0 debug "[Solver] @[Stop daemon@]@.";
- let demtable = get_table_dem delayed.env dem in
- let module DemTable =
- (val demtable : DemTable with type dk = k and type dd = d) in
- (** Dead even if event have been added *)
- let state' = DemTable.D.Key.M.add k demstate (DemTable.state) in
- let module DemTable' = struct
- include DemTable
- let state = state'
+ begin match get_table_dem delayed.env dem with
+ | DemFastT' _ -> assert false
+ | DemT' demtable ->
+ let module DemTable = (val demtable) in
+ (** Dead even if event have been added *)
+ let state' = DemTable.D.Key.M.add k demstate (DemTable.state) in
+ let module DemTable' = struct
+ include DemTable
+ let state = state'
+ end
+ in
+ VDemTable.set delayed.env.dem dem (DemT' (module DemTable'))
end
- in
- VDemTable.set delayed.env.dem dem (module DemTable')
| AliveReattached ->
Debug.dprintf0 debug "[Solver] @[Reattach daemon@]@.";
end
- let do_pending_daemon delayed (DaemonKey (dem,k)) =
- do_pending_daemon delayed dem k
+ and do_pending_daemon delayed (DaemonKey (dem,k)) =
+ do_pending_daemon' delayed dem k
- let nothing_todo t =
+ and nothing_todo t =
Queue.is_empty t.todo_dom
&& Queue.is_empty t.todo_sem
&& Queue.is_empty t.todo_immediate_dem
@@ -1583,7 +1700,7 @@ module Delayed = struct
&& Queue.is_empty t.todo_merge
&& Queue.is_empty t.todo_ext_action
- let rec do_pending t =
+ and do_pending t =
draw_graph t.env;
if not (Queue.is_empty t.todo_dom) then
match Queue.pop t.todo_dom with
@@ -1650,9 +1767,15 @@ module Delayed = struct
else
Debug.dprintf0 debug "[Solver] Nothing to do@."
- let flush d =
+ and flush d =
assert (d.env.current_delayed == d);
- do_pending d;
+ if not (Queue.is_empty d.todo_ext_action) then
+ let saved_ext_action = Queue.create () in
+ Queue.transfer d.todo_ext_action saved_ext_action;
+ do_pending d;
+ Queue.transfer saved_ext_action d.todo_ext_action;
+ else
+ do_pending d;
assert (nothing_todo d)
@@ -1696,7 +1819,9 @@ let new_delayed ~sched_daemon ~sched_decision t =
todo_merge_dom = Queue.create ();
todo_merge = Queue.create ();
todo_ext_action = Queue.create ();
- sched_daemon; sched_decision } in
+ sched_daemon; sched_decision;
+ dem_fast_todo = DemFastNone
+ } in
t.current_delayed <- d;
d
diff --git a/src/solver.mli b/src/solver.mli
index e8e1884512b61d9c4625d8aaf63defeb71328fd8..5a5dccf124ad0684f37b12be5854bd8bd70ac47f 100644
--- a/src/solver.mli
+++ b/src/solver.mli
@@ -214,12 +214,31 @@ module type Dem = sig
val immediate: bool
val wakeup: Delayed.t -> Key.t -> Data.t Events.Fired.t -> Key.t alive
- (** the Events.t in wakeup is a subset of the one given in watch *)
end
module RegisterDem(D:Dem) : sig end
+module type DemFast = sig
+ type d
+
+ module Data: sig
+ type t = d
+ val print: Format.formatter -> t -> unit
+ end
+
+ val key: (unit, Data.t) dem
+
+ (** not immediate and never killed *)
+ val throttle: int (** todo int ref? *)
+ (** number of time run in a row *)
+ val wakeup: Delayed.t -> Data.t Events.Fired.event -> unit
+
+end
+
+module RegisterDemFast(D:DemFast) : sig end
+
+
(** {2 External use of the solver} *)
type t
diff --git a/src/util/bag.ml b/src/util/bag.ml
new file mode 100644
index 0000000000000000000000000000000000000000..af76fb3c9472232ee596f645f41e1a746b5e5e20
--- /dev/null
+++ b/src/util/bag.ml
@@ -0,0 +1,166 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2013 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* ------------------------------------------------------------------------ *)
+(* --- List with constant-time concat --- *)
+(* ------------------------------------------------------------------------ *)
+
+type 'a t =
+ | Empty
+ | Elt of 'a
+ | Add of 'a * 'a t
+ | App of 'a t * 'a
+ | List of 'a list
+ | Concat of 'a t * 'a t
+
+let empty = Empty
+let elt x = Elt x
+
+let length t =
+ let rec scan n = function
+ | Empty -> n
+ | Elt _ -> succ n
+ | Add(_,t) | App(t,_) -> scan (succ n) t
+ | List xs -> n + List.length xs
+ | Concat(a,b) -> scan (scan n a) b
+ in scan 0 t
+
+let add x = function
+ | Empty -> Elt x
+ | t -> Add(x,t)
+
+let append t x = match t with
+ | Empty -> Elt x
+ | t -> App(t,x)
+
+let list = function
+ | [] -> Empty
+ | [x] -> Elt x
+ | xs -> List xs
+
+let concat a b =
+ match a,b with
+ | Empty,c | c,Empty -> c
+ | Elt x,t -> Add(x,t)
+ | t,Elt x -> App(t,x)
+ | Concat(a,b),c -> Concat(a,Concat(b,c)) (* 1-time optim *)
+ | _ -> Concat(a,b)
+
+let rec ulist = function
+ | [] -> Empty
+ | x::xs -> concat x (ulist xs)
+
+let rec map f = function
+ | Empty -> Empty
+ | Elt x -> Elt (f x)
+ | Add(x,t) -> Add(f x,map f t)
+ | App(t,x) -> App(map f t,f x)
+ | List xs -> List(List.map f xs)
+ | Concat(a,b) -> Concat(map f a,map f b)
+
+let rec umap f = function
+ | Empty -> Empty
+ | Elt x -> f x
+ | Add(x,t) -> concat (f x) (umap f t)
+ | App(t,x) -> concat (umap f t) (f x)
+ | List xs -> umap_list f xs
+ | Concat(a,b) -> concat (umap f a) (umap f b)
+
+and umap_list f = function
+ | [] -> Empty
+ | x::xs -> concat (f x) (umap_list f xs)
+
+let rec iter f = function
+ | Empty -> ()
+ | Elt x -> f x
+ | Add(x,t) -> f x ; iter f t
+ | App(t,x) -> iter f t ; f x
+ | List xs -> List.iter f xs
+ | Concat(a,b) -> iter f a ; iter f b
+
+let rec fold_left f w = function
+ | Empty -> w
+ | Elt x -> f w x
+ | Add(x,t) -> fold_left f (f w x) t
+ | App(t,x) -> f (fold_left f w t) x
+ | List xs -> List.fold_left f w xs
+ | Concat(a,b) -> fold_left f (fold_left f w a) b
+
+let rec fold_right f t w = match t with
+ | Empty -> w
+ | Elt x -> f x w
+ | Add(x,t) -> f x (fold_right f t w)
+ | App(t,x) -> fold_right f t (f x w)
+ | List xs -> List.fold_right f xs w
+ | Concat(a,b) -> fold_right f a (fold_right f b w)
+
+let rec filter f = function
+ | Empty -> Empty
+ | Elt x as e -> if f x then e else Empty
+ | Add(x,ts) -> if f x then add x (filter f ts) else filter f ts
+ | App(ts,x) -> let ts = filter f ts in if f x then append ts x else ts
+ | List xs -> list (List.filter f xs)
+ | Concat(a,b) -> concat (filter f a) (filter f b)
+
+let rec partition f = function
+ | Empty -> Empty , Empty
+ | Elt x as e -> if f x then e,Empty else Empty,e
+ | Add(x,ts) ->
+ let pos,neg = partition f ts in
+ if f x then add x pos , neg else pos , add x neg
+ | App(ts,x) ->
+ let ok = f x in
+ let pos,neg = partition f ts in
+ if ok then append pos x , neg else pos , append neg x
+ | List xs ->
+ let pos,neg = List.partition f xs in
+ list pos , list neg
+ | Concat(a,b) ->
+ let apos,aneg = partition f a in
+ let bpos,bneg = partition f b in
+ concat apos bpos , concat aneg bneg
+
+let rec is_empty = function
+ | Empty | List [] -> true
+ | Add _ | App _ | Elt _ | List _ -> false
+ | Concat(a,b) -> is_empty a && is_empty b
+
+let rec singleton = function
+ | Elt x | List [x] -> Some x
+ | Empty | List _ -> None
+ | Add(x,t) | App(t,x) -> if is_empty t then Some x else None
+ | Concat(a,b) ->
+ match singleton a with
+ | Some x -> if is_empty b then Some x else None
+ | None -> if is_empty a then singleton b else None
+
+let rec collect t xs =
+ match t with
+ | Elt x -> x :: xs
+ | Empty -> xs
+ | Add(x,t) -> x :: collect t xs
+ | App(t,x) -> collect t (x::xs)
+ | List ys -> ys @ xs
+ | Concat(a,b) -> collect a (collect b xs)
+
+let elements t = collect t []
+
diff --git a/src/util/bag.mli b/src/util/bag.mli
new file mode 100644
index 0000000000000000000000000000000000000000..7f807d416cd2c823603d47b89f7d3555b395c0ac
--- /dev/null
+++ b/src/util/bag.mli
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2013 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** List with constant-time concat operation.
+ @since Carbon-20101201
+*)
+
+type 'a t
+
+val empty : 'a t
+val elt : 'a -> 'a t
+val add : 'a -> 'a t -> 'a t
+val append : 'a t -> 'a -> 'a t
+val list : 'a list -> 'a t
+val ulist : 'a t list -> 'a t
+val concat : 'a t -> 'a t -> 'a t
+
+val map : ('a -> 'b) -> 'a t -> 'b t
+val umap : ('a -> 'b t) -> 'a t -> 'b t
+
+val iter : ('a -> unit) -> 'a t -> unit
+val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
+val fold_right : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+
+val filter : ('a -> bool) -> 'a t -> 'a t
+val partition : ('a -> bool) -> 'a t -> 'a t * 'a t
+
+val length : 'a t -> int
+
+val is_empty : 'a t -> bool
+val singleton : 'a t -> 'a option
+val elements : 'a t -> 'a list
diff --git a/src/util/lists.ml b/src/util/lists.ml
index 7089c5c79d199593adf7821a718a61147e4c4963..f4c6dbb191afb342e131837708612f9eb4e1390b 100644
--- a/src/util/lists.ml
+++ b/src/util/lists.ml
@@ -129,3 +129,9 @@ let rec chop_last = function
| [r] -> [], r
| x :: s -> let s, r = chop_last s in x :: s, r
+let rec last_rev n = function
+ | [] -> [],[],n
+ | a::l ->
+ let rev,rem,n = last_rev n l in
+ if n > 0 then a::rev,(assert (rem == []); rem),(n-1)
+ else rev,a::rem, n
diff --git a/src/util/lists.mli b/src/util/lists.mli
index fa561adafd432c0d4c09061596bff36ea1ed22b4..76f9c0927465947c0547e30be6b4aff80eefe494 100644
--- a/src/util/lists.mli
+++ b/src/util/lists.mli
@@ -70,3 +70,11 @@ val chop : int -> 'a list -> 'a list
val chop_last : 'a list -> 'a list * 'a
(** removes (and returns) the last element of a list *)
+
+val last_rev : int -> 'a list -> 'a list * 'a list * int
+(** return :
+ - the reverse the last n elements of a list;
+ - return the remaining part of the list.
+ - if the list is not long enough return the number
+ of elements needed ( [0] otherwise )
+*)