diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cArray.ml | 4 | ||||
| -rw-r--r-- | lib/clib.mllib | 1 | ||||
| -rw-r--r-- | lib/dAst.ml | 41 | ||||
| -rw-r--r-- | lib/dAst.mli | 28 |
4 files changed, 72 insertions, 2 deletions
diff --git a/lib/cArray.ml b/lib/cArray.ml index d08f24d490..013585735c 100644 --- a/lib/cArray.ml +++ b/lib/cArray.ml @@ -334,7 +334,7 @@ let smartmap f (ar : 'a array) = Array.unsafe_set ans !i v; incr i; while !i < len do - let v = Array.unsafe_get ar !i in + let v = Array.unsafe_get ans !i in let v' = f v in if v != v' then Array.unsafe_set ans !i v'; incr i @@ -527,7 +527,7 @@ struct Array.unsafe_set ans !i v; incr i; while !i < len do - let v = Array.unsafe_get ar !i in + let v = Array.unsafe_get ans !i in let v' = f arg v in if v != v' then Array.unsafe_set ans !i v'; incr i diff --git a/lib/clib.mllib b/lib/clib.mllib index d5c938fe54..5c1f7d9af8 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -19,6 +19,7 @@ Flags Control Loc CAst +DAst CList CString Deque diff --git a/lib/dAst.ml b/lib/dAst.ml new file mode 100644 index 0000000000..0fe323d013 --- /dev/null +++ b/lib/dAst.ml @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open CAst + +type ('a, _) thunk = +| Value : 'a -> ('a, 'b) thunk +| Thunk : 'a Lazy.t -> ('a, [ `thunk ]) thunk + +type ('a, 'b) t = ('a, 'b) thunk CAst.t + +let map_thunk (type s) f : (_, s) thunk -> (_, s) thunk = function +| Value x -> Value (f x) +| Thunk k -> Thunk (lazy (f (Lazy.force k))) + +let get_thunk (type s) : ('a, s) thunk -> 'a = function +| Value x -> x +| Thunk k -> Lazy.force k + +let get x = get_thunk x.v + +let make ?loc v = CAst.make ?loc (Value v) + +let delay ?loc v = CAst.make ?loc (Thunk (Lazy.from_fun v)) + +let map f n = CAst.map (fun x -> map_thunk f x) n + +let map_with_loc f n = + CAst.map_with_loc (fun ?loc x -> map_thunk (fun x -> f ?loc x) x) n + +let map_from_loc f (loc, x) = + make ?loc (f ?loc x) + +let with_val f n = f (get n) + +let with_loc_val f n = f ?loc:n.CAst.loc (get n) diff --git a/lib/dAst.mli b/lib/dAst.mli new file mode 100644 index 0000000000..5b51677fc6 --- /dev/null +++ b/lib/dAst.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Lazy AST node wrapper. Only used for [glob_constr] as of today. *) + +type ('a, _) thunk = +| Value : 'a -> ('a, 'b) thunk +| Thunk : 'a Lazy.t -> ('a, [ `thunk ]) thunk + +type ('a, 'b) t = ('a, 'b) thunk CAst.t + +val get : ('a, 'b) t -> 'a +val get_thunk : ('a, 'b) thunk -> 'a + +val make : ?loc:Loc.t -> 'a -> ('a, 'b) t +val delay : ?loc:Loc.t -> (unit -> 'a) -> ('a, [ `thunk ]) t + +val map : ('a -> 'b) -> ('a, 'c) t -> ('b, 'c) t +val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> ('b, 'c) t +val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> ('b, 'c) t + +val with_val : ('a -> 'b) -> ('a, 'c) t -> 'b +val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> 'b |