aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/base_db
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-08-29 19:05:57 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-09-04 11:28:49 +0200
commit1db568d3dc88d538f975377bb4d8d3eecd87872c (patch)
treed8e35952cc8f6111875e664d8884dc2c7f908206 /dev/base_db
parent3072bd9d080984833f5eb007bf15c6e9305619e3 (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 'dev/base_db')
0 files changed, 0 insertions, 0 deletions