From 1e723d52659abfd2ff2dd00512f3fc69f327cd78 Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Fri, 24 Mar 2017 16:41:12 -0700
Subject: [PATCH] Add a rule for multiplication

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.)
---
 src/Cryptol/TypeCheck/Solver/Numeric.hs | 35 ++++++++++++++++++++++++-
 1 file changed, 34 insertions(+), 1 deletion(-)

diff --git a/src/Cryptol/TypeCheck/Solver/Numeric.hs b/src/Cryptol/TypeCheck/Solver/Numeric.hs
index afdd1576..3a99b3bf 100644
--- a/src/Cryptol/TypeCheck/Solver/Numeric.hs
+++ b/src/Cryptol/TypeCheck/Solver/Numeric.hs
@@ -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' ])