freshVV type aliases to prevend shadowing

src/Language/Haskell/Liquid/Constraint/Fresh.hs

@@ -38,11 +38,25 @@ import           Language.Haskell.Liquid.Types
 -- import           Language.Haskell.Liquid.Types.Fresh
 import           Language.Haskell.Liquid.Constraint.Types
 import qualified Language.Haskell.Liquid.GHC.Misc as GM 
-import           Language.Haskell.Liquid.GHC.API as Ghc
+import Language.Haskell.Liquid.GHC.API as Ghc
+    ( Type,
+      Var(varType),
+      CoreExpr,
+      exprType,
+      Bind(..),
+      Expr(Var, Let, Lam, Tick),
+      isTyVar )
 
 --------------------------------------------------------------------------------
 -- | This is all hardwiring stuff to CG ----------------------------------------
 --------------------------------------------------------------------------------
+instance Freshable CG F.Symbol where
+  fresh = do s <- get
+             let n = freshIndex s
+             put $ s { freshIndex = n + 1 }
+             return (F.tempSymbol (F.symbol ("x" :: String)) n)
+
+
 instance Freshable CG Integer where
   fresh = do s <- get
              let n = freshIndex s

src/Language/Haskell/Liquid/Parse.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE OverloadedStrings         #-}
 {-# LANGUAGE DeriveDataTypeable        #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE MultiParamTypeClasses     #-}
 
 module Language.Haskell.Liquid.Parse
   ( hsSpecificationP
@@ -45,7 +46,7 @@ import qualified Language.Fixpoint.Misc                 as Misc
 import qualified Language.Haskell.Liquid.Misc           as Misc
 import qualified Language.Haskell.Liquid.Measure        as Measure
 import           Language.Fixpoint.Parse                hiding (defineP, dataDeclP, refBindP, refP, refDefP, parseTest')
-
+import           Language.Haskell.Liquid.Types.Fresh
 import Control.Monad.State
 
 -- import Debug.Trace
@@ -1272,21 +1273,21 @@ embedP = do
 
 
 aliasP :: Parser (Located (RTAlias Symbol BareType))
-aliasP  = rtAliasP id     bareTypeP <?> "aliasP"
+aliasP  = rtAliasP id (bareTypeP >>= refreshVV) <?> "aliasP"
 
 ealiasP :: Parser (Located (RTAlias Symbol Expr))
 ealiasP = try (rtAliasP symbol predP)
       <|> rtAliasP symbol exprP
       <?> "ealiasP"
 
 -- | Parser for a LH type synonym.
-rtAliasP :: (Symbol -> tv) -> Parser ty -> Parser (Located (RTAlias tv ty))
+rtAliasP :: (Freshable Parser ty, Show ty, PPrint ty) =>  (Symbol -> tv) -> Parser ty -> Parser (Located (RTAlias tv ty))
 rtAliasP f bodyP
   = do pos  <- getSourcePos
        name <- upperIdP
        args <- many aliasIdP
        reservedOp "="
-       body <- bodyP
+       body <- bodyP 
        posE <- getSourcePos
        let (tArgs, vArgs) = partition (isSmall . headSym) args
        return $ Loc pos posE (RTA name (f <$> tArgs) vArgs body)
@@ -1420,6 +1421,12 @@ locBinderP :: Parser (Located Symbol)
 locBinderP =
   located binderP -- TODO
 
+
+instance Freshable Parser Symbol where
+  fresh = do s <- getSourcePos
+             return $ symbol (show s)
+
+
 -- | LHS of the thing being defined
 --
 -- TODO, Andres: this is still very broken

src/Language/Haskell/Liquid/Types/Fresh.hs

@@ -48,36 +48,43 @@ class (Applicative m, Monad m) => Freshable m a where
   refresh _ = return
 
 
-instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Symbol where
-  fresh = F.tempSymbol "x" <$> fresh
+-- instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Symbol where
+--   fresh = F.tempSymbol "x" <$> fresh
 
-instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Expr where
+instance (Freshable m F.Symbol, Monad m, Applicative m) => Freshable m F.Expr where
   fresh  = kv <$> fresh
     where
-      kv = (`F.PKVar` mempty) . F.intKvar
+      kv = (`F.PKVar` mempty) . F.KV
 
-instance (Freshable m Integer, Monad m, Applicative m) => Freshable m [F.Expr] where
+instance (Freshable m F.Symbol, Monad m, Applicative m) => Freshable m [F.Expr] where
   fresh = single <$> fresh
 
-instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Reft where
+instance (Freshable m F.Symbol, Monad m, Applicative m) => Freshable m F.Reft where
   fresh                  = panic Nothing "fresh Reft"
   true    _ (F.Reft (v,_)) = return $ F.Reft (v, mempty)
   refresh _ (F.Reft (_,_)) = (F.Reft .) . (,) <$> freshVV <*> fresh
     where
-      freshVV            = F.vv . Just <$> fresh
+      freshVV            = F.mappendSym F.vv_ <$> fresh
 
-instance Freshable m Integer => Freshable m RReft where
+instance Freshable m F.Symbol => Freshable m RReft where
   fresh             = panic Nothing "fresh RReft"
   true allowTC (MkUReft r _)    = MkUReft <$> true allowTC r    <*> return mempty
   refresh allowTC (MkUReft r _) = MkUReft <$> refresh allowTC r <*> return mempty
 
-instance (Freshable m Integer, Freshable m r, F.Reftable r ) => Freshable m (RRType r) where
+instance (Freshable m F.Symbol, Freshable m r, F.Reftable r ) => Freshable m (RRType r) where
   fresh   = panic Nothing "fresh RefType"
   refresh = refreshRefType
   true    = trueRefType
 
+
+instance (Freshable m F.Symbol) => Freshable m BareType where
+  fresh   = panic Nothing "fresh RefType"
+  refresh = refreshRefType
+  true    = panic Nothing "fresh true"
+
+
 -----------------------------------------------------------------------------------------------
-trueRefType :: (Freshable m Integer, Freshable m r, F.Reftable r) => Bool -> RRType r -> m (RRType r)
+trueRefType :: (Freshable m F.Symbol, Freshable m r, F.Reftable r) => Bool -> RRType r -> m (RRType r)
 -----------------------------------------------------------------------------------------------
 trueRefType allowTC (RAllT α t r)
   = RAllT α <$> true allowTC t <*> true allowTC r 
@@ -122,14 +129,14 @@ trueRefType _ t@(RExprArg _)
 trueRefType _ t@(RHole _)
   = return t
 
-trueRef :: (F.Reftable r, Freshable f r, Freshable f Integer)
+trueRef :: (F.Reftable r, Freshable f r, Freshable f F.Symbol)
         => Bool -> Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
 trueRef _ (RProp _ (RHole _)) = panic Nothing "trueRef: unexpected RProp _ (RHole _))"
 trueRef allowTC (RProp s t) = RProp s <$> trueRefType allowTC t
 
 
 -----------------------------------------------------------------------------------------------
-refreshRefType :: (Freshable m Integer, Freshable m r, F.Reftable r) => Bool -> RRType r -> m (RRType r)
+refreshRefType :: (Freshable m F.Symbol, Freshable m r, F.Reftable r, TyConable c, Freshable m (RType c v r)) => Bool -> RType c v r -> m (RType c v r)
 -----------------------------------------------------------------------------------------------
 refreshRefType allowTC (RAllT α t r)
   = RAllT α <$> refresh allowTC t <*> true allowTC r
@@ -169,8 +176,8 @@ refreshRefType allowTC (RRTy e o r t)
 refreshRefType _ t
   = return t
 
-refreshRef :: (F.Reftable r, Freshable f r, Freshable f Integer)
-           => Bool -> Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
+refreshRef :: (F.Reftable r, Freshable f r, Freshable f F.Symbol, TyConable c, Freshable f (RType c v r))
+           => Bool -> Ref τ (RType c v r) -> f (Ref τ (RType c v r))
 refreshRef _ (RProp _ (RHole _)) = panic Nothing "refreshRef: unexpected (RProp _ (RHole _))"
 refreshRef allowTC (RProp s t) = RProp <$> mapM freshSym s <*> refreshRefType allowTC t
 
@@ -184,52 +191,52 @@ refreshTy :: (FreshM m) => SpecType -> m SpecType
 refreshTy t = refreshVV t >>= refreshArgs
 
 --------------------------------------------------------------------------------
-type FreshM m = Freshable m Integer
+type FreshM m = Freshable m F.Symbol
 --------------------------------------------------------------------------------
 
 --------------------------------------------------------------------------------
-refreshVV :: FreshM m => SpecType -> m SpecType
+refreshVV :: (FreshM m, F.Reftable (r F.Reft), Functor r, TyConable c, Freshable m (r F.Reft)) => RType c tv (r F.Reft) -> m (RType c tv (r F.Reft))
 --------------------------------------------------------------------------------
 refreshVV (RAllT a t r) = 
   RAllT a <$> refreshVV t <*> return r 
 
 refreshVV (RAllP p t) = 
   RAllP p <$> refreshVV t
 
-refreshVV (REx x t1 t2) = do 
+refreshVV t@(REx x t1 t2) = do 
   t1' <- refreshVV t1
   t2' <- refreshVV t2
-  shiftVV (REx x t1' t2') <$> fresh
+  shiftVV (REx x t1' t2') <$> refresh False (rTypeValueVar t)
 
-refreshVV (RImpF x i t1 t2 r) = do
+refreshVV t@(RImpF x i t1 t2 r) = do
   t1' <- refreshVV t1
   t2' <- refreshVV t2
-  shiftVV (RImpF x i t1' t2' r) <$> fresh
+  shiftVV (RImpF x i t1' t2' r) <$> refresh False (rTypeValueVar t)
 
-refreshVV (RFun x i t1 t2 r) = do
+refreshVV t@(RFun x i t1 t2 r) = do
   t1' <- refreshVV t1
   t2' <- refreshVV t2
-  shiftVV (RFun x i t1' t2' r) <$> fresh
+  shiftVV (RFun x i t1' t2' r) <$> refresh False (rTypeValueVar t)
 
-refreshVV (RAppTy t1 t2 r) = do 
+refreshVV t@(RAppTy t1 t2 r) = do 
   t1' <- refreshVV t1
   t2' <- refreshVV t2
-  shiftVV (RAppTy t1' t2' r) <$> fresh
+  shiftVV (RAppTy t1' t2' r) <$> refresh False (rTypeValueVar t)
 
-refreshVV (RApp c ts rs r) = do 
+refreshVV t@(RApp c ts rs r) = do 
   ts' <- mapM refreshVV    ts
   rs' <- mapM refreshVVRef rs
-  shiftVV (RApp c ts' rs' r) <$> fresh
+  shiftVV (RApp c ts' rs' r) <$> refresh False (rTypeValueVar t)
 
 refreshVV t = 
-  shiftVV t <$> fresh
+  shiftVV t <$> refresh False (rTypeValueVar t)
 
-refreshVVRef :: Freshable m Integer => Ref b SpecType -> m (Ref b SpecType)
+refreshVVRef :: (FreshM m, F.Reftable (r F.Reft), Functor r, TyConable c, Freshable m (r F.Reft)) => Ref b (RType c tv (r F.Reft)) -> m (Ref b (RType c tv (r F.Reft)))
 refreshVVRef (RProp ss (RHole r))
   = return $ RProp ss (RHole r)
 
 refreshVVRef (RProp ss t)
-  = do xs    <- mapM (const fresh) (fst <$> ss)
+  = do xs    <- mapM (refresh False) (fst <$> ss)
        let su = F.mkSubst $ zip (fst <$> ss) (F.EVar <$> xs)
        (RProp (zip xs (snd <$> ss)) . F.subst su) <$> refreshVV t
 

tests/neg/TyAlias.hs

@@ -0,0 +1,53 @@
+module Foo where 
+
+{-@ measure listLength @-}
+{-@ listLength :: xs:_ -> {v:Nat | v == len xs } @-}
+listLength :: [a] -> Int
+listLength [] = 0
+listLength (_x:xs) = 1 + listLength xs
+
+data Set a = Set [a] 
+{-@ data Set a = Set [a]<{\x y -> x < y}> @-}
+
+
+{-@ measure setSize @-}
+{-@ setSize :: Set a -> Nat @-}
+setSize :: Set a -> Int
+setSize (Set xs) = listLength xs
+
+type BinaryRelation a b = Set (a, b)
+{-@ type BinaryRelationGT a b P = Set { p:(a, b) | P < p } @-}
+
+-- | Given (a,b), for every (x,y) in the relation if b==x add (a,y) to the
+-- result or if y==a add (x,b) to the result.
+--
+-- >>> brTransitivitySweep (1,2) (Set [(2,3)])
+-- {(1,3),(2,3)}
+--
+-- >>> brTransitivitySweep (2,3) $ Set [(2,999)]
+-- {(2,999)}
+--
+-- >>> brTransitivitySweep (1,2) $ Set [(2,999)]
+-- {(1,999),(2,999)}
+--
+-- >>> brTransitivitySweep (1,2) $ Set [(2,3),(2,999)] -- BUG
+-- {(1,3),(2,3),(1,999),(2,999)}
+--
+{-@
+brTransitivitySweep
+    ::  p:(a, a)
+    -> br:BinaryRelationGT a a {p}
+    ->    BinaryRelationGT a a {p}
+    / [setSize br]
+@-}
+brTransitivitySweep :: Eq a => (a, a) -> BinaryRelation a a -> BinaryRelation a a
+brTransitivitySweep _ (Set []) = Set []
+brTransitivitySweep (a,b) (Set ((x,y):rest0))
+    | b == x    = Set ((a,y):(x,y):rest1) -- a->b, x->y, b==x implies a->y | (a,b) < (x,y) && b == x  => (a,y) < (x,y)
+    | y == a    = Set ((x,b):(x,y):rest1) -- x->y, a->b, y==a implies x->b
+    | otherwise = Set (      (x,y):rest1)
+  where
+    Set rest1 = brTransitivitySweep (a,b) (Set rest0)
+
+
+-- bar = brTransitivitySweep (1,2) $ Set [(2,3),(2,999)]