GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-08 08:49:44 +03:00
Code Issues Projects Releases Wiki Activity

Document additional invariant on 'Subst' type.

Browse Source
This commit is contained in:
Brian Huffman 2020-05-15 07:06:15 -07:00
parent 1c38465ca8
commit 2f21e65d0e
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/Cryptol/TypeCheck/Subst.hs
View File

@ -53,6 +53,13 @@ import Cryptol.Utils.Misc(anyJust)
-- variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of
-- @tps@. This ensures that applying the substitution will not permit
-- any type parameter to escape from its scope.
--
-- Invariant: The substitution must be idempotent, in that applying a
-- substitution to any 'Type' in the map should leave that 'Type'
-- unchanged. In other words, 'Type' values in the range of a 'Subst'
-- should not mention any 'TVar' in the domain of the 'Subst'. In
-- particular, this implies that a substitution must not contain any
-- recursive variable mappings.
data Subst = S { suFreeMap :: !(IntMap.IntMap (TVar, Type))
, suBoundMap :: !(IntMap.IntMap (TVar, Type))