Skip to content
Snippets Groups Projects
Commit 751775ba authored by François Bobot's avatar François Bobot
Browse files

[Solver] add Fast daemon not immediate with key = unit

parent 3e65ae3f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/solver.ml
+ 198
− 73
View file @ 751775ba
......@@ -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
......
src/solver.mli
+ 20
− 1
View file @ 751775ba
......@@ -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
......
src/util/bag.ml 0 → 100644
+ 166
− 0
View file @ 751775ba
(**************************************************************************)
(* *)
(* 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 []
src/util/bag.mli 0 → 100644
+ 51
− 0
View file @ 751775ba
(**************************************************************************)
(* *)
(* 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
src/util/lists.ml
+ 6
− 0
View file @ 751775ba
......@@ -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
src/util/lists.mli
+ 8
− 0
View file @ 751775ba
......@@ -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 )
*)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment