diff options
Diffstat (limited to 'src/spec_analysis.mli')
| -rw-r--r-- | src/spec_analysis.mli | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli index 94698954..1b1197dd 100644 --- a/src/spec_analysis.mli +++ b/src/spec_analysis.mli @@ -5,4 +5,15 @@ open Type_internal type typ = Type_internal.t +(*Returns the declared default order of a set of definitions, defaulting to Inc if no default is provided *) val default_order : tannot defs -> order + +(*Determines if the first typ is within the range of the the second typ, + using the constraints provided when the first typ contains variables. + It is an error for second typ to be anything other than a range type + If the first typ is a vector, then determines if the max representable + number is in the range of the second; it is an error for the first typ + to be anything other than a vector, a range, an atom, or a bit (after + suitable unwrapping of abbreviations, reg, and registers). +*) +val is_within_range: typ -> typ -> nexp_range list -> triple |