diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-29 19:05:57 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-04 11:28:49 +0200 |
commit | 1db568d3dc88d538f975377bb4d8d3eecd87872c (patch) | |
tree | d8e35952cc8f6111875e664d8884dc2c7f908206 /lib/dAst.ml | |
parent | 3072bd9d080984833f5eb007bf15c6e9305619e3 (diff) |
Making detyping potentially lazy.
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
Diffstat (limited to 'lib/dAst.ml')
-rw-r--r-- | lib/dAst.ml | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/lib/dAst.ml b/lib/dAst.ml new file mode 100644 index 000000000..0fe323d01 --- /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) |