Conservative use of fin constraints

src/Cryptol/TypeCheck/Solve.hs

@@ -37,7 +37,7 @@ import qualified Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr as Num
 import qualified Cryptol.TypeCheck.Solver.CrySAT as Num
 import           Cryptol.TypeCheck.Solver.CrySAT (debugBlock, DebugLog(..))
 import           Cryptol.TypeCheck.Solver.Simplify
-                    (Fins,filterFins,tryRewritePropAsSubst)
+                    (Fins,tryRewritePropAsSubst)
 import           Cryptol.Utils.PP (text)
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.Misc(anyJust)
@@ -318,7 +318,7 @@ computeImprovements :: Num.Solver -> [Goal] -> IO (Either [Goal] Subst)
 computeImprovements s gs
   -- Find things of the form: `x = t`.  We might do some rewriting to put
   -- it in this form, if needed.
-  | (x,t) : _ <- mapMaybe (improveByDefn (filterFins gs)) gs =
+  | (x,t) : _ <- mapMaybe (improveByDefn fins) gs =
     do let su = singleSubst x t
        debugLog s ("Improve by definition: " ++ show (pp su))
        return (Right su)
@@ -340,6 +340,12 @@ computeImprovements s gs
                                                 (map Num.knownDefined nums)
             return (Left bad)
 
+  where
+
+  -- XXX remove this once the interval analysis is done
+  fins = Set.fromList [ tv | Goal { .. } <- gs
+                           , Just tv     <- [ tIsVar =<< pIsFin goal ] ]
+
 
 improveByDefn :: Fins -> Goal -> Maybe (TVar,Type)
 improveByDefn fins Goal { .. } =

src/Cryptol/TypeCheck/Solver/Simplify.hs

@@ -1,16 +1,18 @@
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Cryptol.TypeCheck.Solver.Simplify (
-    Fins, filterFins,
+    Fins,
     tryRewritePropAsSubst
   ) where
 
 
 import Cryptol.Prims.Syntax (TFun(..))
-import Cryptol.TypeCheck.AST (Type(..),Prop,TVar,pIsEq,isFreeTV,TCon(..),pIsFin)
+import Cryptol.TypeCheck.AST (Type(..),Prop,TVar,pIsEq,isFreeTV,TCon(..))
 import Cryptol.TypeCheck.InferTypes (Goal(..))
 import Cryptol.TypeCheck.Subst (fvs)
+import Cryptol.TypeCheck.PP (pp)
 
 import           Control.Monad (msum,guard,mzero)
 import           Data.Function (on)
@@ -18,16 +20,14 @@ import           Data.List (sortBy)
 import           Data.Maybe (catMaybes,listToMaybe)
 import qualified Data.Set as Set
 
+import Debug.Trace
+
 
 -- | Type variables that are known to have a `fin` constraint. This set is used
 -- to justify the addition of a subtraction on the rhs of an equality
 -- constraint.
 type Fins = Set.Set TVar
 
-filterFins :: [Goal] -> Fins
-filterFins gs = Set.unions [ fvs ty | Goal { .. } <- gs
-                                    , Just ty     <- [pIsFin goal] ]
-
 
 -- | When given an equality constraint, attempt to rewrite it to the form `?x =
 -- ...`, by moving all occurrences of `?x` to the LHS, and any other variables
@@ -37,6 +37,9 @@ tryRewritePropAsSubst :: Fins -> Prop -> Maybe (TVar,Type)
 tryRewritePropAsSubst fins p =
   do (x,y) <- pIsEq p
 
+     () <- traceShowM (map pp (Set.toList fins))
+     () <- traceShowM (pp p)
+
      let vars = Set.toList (Set.filter isFreeTV (fvs p))
 
      listToMaybe $ sortBy (flip compare `on` rank)
@@ -57,7 +60,15 @@ rank (_,ty) = go ty
 
 
 -- | Rewrite an equation with respect to a unification variable ?x, into the
--- form `?x = t`.
+-- form `?x = t`.  There are two interesting cases to consider (four with
+-- symmetry):
+--
+--  * ?x = ty
+--  * expr containing ?x = expr
+--
+-- In the first case, we just return the type variable and the type, but in the
+-- second we try to rewrite the equation until it's in the form of the first
+-- case.
 tryRewriteEq :: Fins -> TVar -> Type -> Type -> Maybe (TVar,Type)
 tryRewriteEq fins uvar l r =
   msum [ do guard (uvarTy == l && uvar `Set.notMember` rfvs)
@@ -88,7 +99,14 @@ allFin :: Fins -> Type -> Bool
 allFin fins ty = fvs ty `Set.isSubsetOf` fins
 
 
--- | Rewrite an equality until the LHS is just uvar. Return the rewritten RHS.
+-- | Rewrite an equality until the LHS is just `uvar`. Return the rewritten RHS.
+--
+-- There are a few interesting cases when rewriting the equality:
+--
+--  A o B = R  when `uvar` is only present in A
+--  A o B = R  when `uvar` is only present in B
+--
+-- Each of these cases ...
 rewriteLHS :: Fins -> TVar -> Type -> Type -> Maybe Type
 rewriteLHS fins uvar = go
   where
@@ -102,8 +120,6 @@ rewriteLHS fins uvar = go
            inX  = Set.member uvar xfvs
            inY  = Set.member uvar yfvs
 
-       -- for now, don't handle the complicated case where the variable shows up
-       -- multiple times in an expression
        if | inX && inY -> mzero
           | inX        -> balanceR x tf y rhs
           | inY        -> balanceL x tf y rhs
@@ -121,7 +137,7 @@ rewriteLHS fins uvar = go
 
   -- invert the type function to balance the equation, when the variable occurs
   -- on the LHS of the expression `x tf y`
-  balanceR x TCAdd y rhs = do guardSubtract y
+  balanceR x TCAdd y rhs = do guardFin y
                               go x (TCon (TF TCSub) [rhs,y])
   balanceR x TCSub y rhs = go x (TCon (TF TCAdd) [rhs,y])
   balanceR _ _     _ _   = mzero
@@ -129,14 +145,14 @@ rewriteLHS fins uvar = go
 
   -- invert the type function to balance the equation, when the variable occurs
   -- on the RHS of the expression `x tf y`
-  balanceL x TCAdd y rhs = do guardSubtract y
+  balanceL x TCAdd y rhs = do guardFin y
                               go y (TCon (TF TCSub) [rhs,x])
   balanceL x TCSub y rhs = go (TCon (TF TCAdd) [rhs,y]) x
   balanceL _ _     _ _   = mzero
 
 
-  -- guard that it's OK to subtract this type from something else.
+  -- guard that the type is finite
   --
   -- XXX this ignores things like `min x inf` where x is finite, and just
   -- assumes that it won't work.
-  guardSubtract ty = guard (allFin fins ty)
+  guardFin ty = guard (allFin fins ty)