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

Add a rule for multiplication

Browse Source 
When the constraint is of the form, `k1 * x = k2 * y`, and `gcd k1 k2 /= 1`,
simplify the constraint to `(k1 / gcd k1 k2) * x = (k2 / gcd k1 k2) * y`.
(NOTE: this doesn't produce a new constraint that uses division, but
evaluates the two two constants.)
This commit is contained in:
Trevor Elliott 2017-03-24 16:41:12 -07:00
parent d498212684
commit 1e723d5265
1 changed files with 34 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
src/Cryptol/TypeCheck/Solver/Numeric.hs
View File

@ -5,10 +5,11 @@ module Cryptol.TypeCheck.Solver.Numeric
import Control.Applicative(Alternative(..))
import Control.Monad (guard,mzero)
import Data.Foldable (asum)
import Cryptol.Utils.Patterns
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.Type hiding (tMul)
import Cryptol.TypeCheck.TypePat
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.InfNat
@ -27,6 +28,7 @@ cryIsEqual ctxt t1 t2 =
<|> ( guard (t1 == t2) >> return (SolvedIf []))
<|> tryEqMin t1 t2
<|> tryEqMin t2 t1
<|> tryEqMulConst t1 t2
@ -200,4 +202,35 @@ tryEqK ctxt ty lk =
tryEqMulConst :: Type -> Type -> Match Solved
tryEqMulConst l r =
do (l1,l2) <- aMul l
(r1,r2) <- aMul r
asum [ do l1' <- aNat l1
r1' <- aNat r1
return (build l1' l2 r1' r2)
, do l2' <- aNat l2
r1' <- aNat r1
return (build l2' l1 r1' r2)
, do l1' <- aNat l1
r2' <- aNat r2
return (build l1' l2 r2' r1)
, do l2' <- aNat l2
r2' <- aNat r2
return (build l2' l1 r2' r1)
]
where
build lk l' rk r' =
let d = gcd lk rk
lk' = lk `div` d
rk' = rk `div` d
in if d == 1
then Unsolved
else (SolvedIf [ tMul (tNum lk') l' =#= tMul (tNum rk') r' ])