diff options
| author | Gaëtan Gilbert | 2018-11-15 13:30:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-21 13:42:14 +0100 |
| commit | d079ec262eacc2149fa46b45ac23097a3333b5fe (patch) | |
| tree | 4bd801060b02da1efa9ef2169890e78333ca7805 /checker/values.ml | |
| parent | e0db7f1baef37bb60db2dd1c963572f175392783 (diff) | |
More informative error on vo validation failure
Now that the checker shares code with the kernel using md5 cic.mli
doesn't work. We could md5 declarations.ml but this would miss changes
to constr (and cic.mli already missed changes to names, univs).
Instead we just print a bit of information (the last seen type
name/annotation) when validate fails. This should help debugging when
forgetting to update values.ml without the full verbosity of -debug.
As such there is no need to -debug in the makefile validate
target (NB: CI has an independent implementation of the validate rule
since the vos are installed there).
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 24 |
1 files changed, 6 insertions, 18 deletions
diff --git a/checker/values.ml b/checker/values.ml index e21acd8179..0de8a3e03f 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -10,28 +10,15 @@ (** Abstract representations of values in a vo *) -(** NB: UPDATE THIS FILE EACH TIME cic.mli IS MODIFIED ! +(** NB: This needs updating when the types in declarations.ml and + their dependencies are changed. *) -To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli -with a copy we maintain here: - -MD5 b8f0139f14e3370cd0a45d4cf69882ea checker/cic.mli - -*) - -(** We reify here the types of values present in a vo (see cic.mli), +(** We reify here the types of values present in a vo. in order to validate its structure. Maybe this reification could become automatically generated someday ? - - [Any] stands for a value that we won't check, - - [Fail] means a value that shouldn't be there at all, - - [Tuple] provides a name and sub-values in this block - - [Sum] provides a name, a number of constant constructors, - and sub-values at each position of each possible constructed - variant - - [List] and [Opt] could have been defined via [Sum], but - having them here helps defining some recursive values below - - [Annot] is a no-op, just there for improving debug messages *) + See values.mli for the meaning of each constructor. +*) type value = | Any @@ -45,6 +32,7 @@ type value = | String | Annot of string * value | Dyn + | Proxy of value ref let fix (f : value -> value) : value = |