GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-12 04:17:04 +03:00
Code Issues Projects Releases Wiki Activity

Solving fin constraints direclty.

Browse Source
This commit is contained in:
Iavor S. Diatchki 2015-08-13 16:38:48 -07:00
parent b6fa8d9473
commit ad6f0fb8aa
1 changed files with 76 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

76
src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs Normal file
View File

@ -0,0 +1,76 @@
-- | Simplification of `fin` constraints.
module Cryptol.TypeCheck.Solver.Numeric.Fin where
import Data.Map (Map)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.Solver.Numeric.Interval
import Cryptol.TypeCheck.Solver.InfNat
cryIsFin :: Map TVar Interval -> Goal -> Solved
cryIsFin varInfo g =
case tNoUser (goal g) of
TCon (TC tc) [] | TCNum _ <- tc -> solved []
TCon (TF f) ts ->
case (f,ts) of
(TCAdd,[t1,t2]) -> solved [ pFin t1, pFin t2 ]
(TCSub,[t1,_ ]) -> solved [ pFin t1 ]
-- fin (x * y)
(TCMul,[t1,t2])
| iLower i1 >= Nat 1 && iIsFin i1 -> solved [ pFin t2 ]
| iLower i2 >= Nat 1 && iIsFin i2 -> solved [ pFin t1 ]
| iLower i1 >= Nat 1 &&
iLower i2 >= Nat 1 -> solved [ pFin t1, pFin t2 ]
| iIsFin i1 && iIsFin i2 -> solved []
where
i1 = typeInterval varInfo t1
i2 = typeInterval varInfo t2
(TCDiv, [t1,_]) -> solved [ pFin t1 ]
(TCMod, [_,_]) -> solved []
-- fin (x ^ y)
(TCExp, [t1,t2])
| iLower i1 == Inf -> solved [ t2 =#= tZero ]
| iLower i2 == Inf -> solved [ tOne >== t1 ]
| iLower i1 >= Nat 2 -> solved [ pFin t1, pFin t2 ]
| iLower i2 >= Nat 1 -> solved [ pFin t1, pFin t2 ]
| Just x <- iUpper i1, x <= Nat 1 -> solved []
| Just (Nat 0) <- iUpper i2 -> solved []
where
i1 = typeInterval varInfo t1
i2 = typeInterval varInfo t2
-- fin (min x y)
(TCMin, [t1,t2])
| iIsFin i1 -> solved []
| iIsFin i2 -> solved []
| Just x <- iUpper i1, x <= iLower i2 -> solved [ pFin t1 ]
| Just x <- iUpper i2, x <= iLower i1 -> solved [ pFin t2 ]
where
i1 = typeInterval varInfo t1
i2 = typeInterval varInfo t2
(TCMax, [t1,t2]) -> solved [ pFin t1, pFin t2 ]
(TCWidth, [t1]) -> solved [ pFin t1 ]
(TCLenFromThen,[_,_,_]) -> solved []
(TCLenFromThenTo,[_,_,_]) -> solved []
_ -> Unsolved
_ -> Unsolved
where
solved ps = Solved Nothing [ g { goal = p } | p <- ps ]