diff options
| author | Alasdair Armstrong | 2018-11-16 18:28:17 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-11-16 18:28:17 +0000 |
| commit | 626c68dad5ea79da7776b4628e5ae22ca742669e (patch) | |
| tree | 4942f0b4783f9f10987c514dc61859eb73d930a1 /src/finite_map.ml | |
| parent | b3ea287bcf8be43714595b6921a0c47d25a67eee (diff) | |
Canonicalise functions types in val specs
This brings Sail closer to MiniSail, and means that
type my_range 'n 'm = {'o, 'n <= 'o <= 'm. int('o)}
will work on the left hand side of a function type in the same way as
a regular built-in range type. This means that in principle neither
range nor int need be built-in types, as both can be implemented in
terms of int('n) (atom internally). It also means we can easily
identify type variables that need to be made into implict arguments,
with the criterion for that being simply any type variable that
doesn't appear in a base type on the LHS of the function, or only
appears on the RHS.
Diffstat (limited to 'src/finite_map.ml')
0 files changed, 0 insertions, 0 deletions
