Logical Constraints

liquidhaskell.cabal

@@ -158,6 +158,7 @@ Library
                     Language.Haskell.Liquid.List, 
                     Language.Haskell.Liquid.PrettyPrint, 
                     Language.Haskell.Liquid.Bare,
+                    Language.Haskell.Liquid.Constraint.Constraint, 
                     Language.Haskell.Liquid.Constraint.Types, 
                     Language.Haskell.Liquid.Constraint.Generate, 
                     Language.Haskell.Liquid.Constraint.ToFixpoint, 

src/Language/Haskell/Liquid/Bare.hs

@@ -383,7 +383,7 @@ expandAlias l = go
     go _ (ROth s)         = return $ ROth s
     go _ (RExprArg e)     = return $ RExprArg e
     go _ (RHole r)        = RHole <$> resolve l r
-    go _ (RRTy _ _ _ _)   = errorstar "Bare.expandAlias called on RRTy" 
+    go s (RRTy e r o t)   = RRTy <$> mapM (mapSndM (go s)) e <*> resolve l r <*> return o <*> go s t 
 
 
 lookupExpandRTApp l s (RApp lc@(Loc _ c) ts rs r) = do
@@ -661,6 +661,8 @@ mapTyVars τ (RAllS _ t)
   = mapTyVars τ t 
 mapTyVars τ (RAllE _ _ t)   
   = mapTyVars τ t 
+mapTyVars τ (RRTy _ _ _ t)   
+  = mapTyVars τ t 
 mapTyVars τ (REx _ _ t)
   = mapTyVars τ t 
 mapTyVars _ (RExprArg _)
@@ -901,6 +903,7 @@ plugHoles tce tyi x f t (Loc l st)
     go (RAllT a t)      t'                 = RAllT a <$> go t t'
     go t                (RAllE b a t')     = RAllE b a <$> go t t'
     go t                (REx b x t')       = REx b x <$> go t t'
+    go t                (RRTy e r o t')    = RRTy e r o <$> go t t'
     go (RAppTy t1 t2 _) (RAppTy t1' t2' r) = RAppTy <$> go t1 t1' <*> go t2 t2' <*> return r
     go (RApp _ t _ _)   (RApp c t' p r)    = RApp c <$> (zipWithM go t t') <*> return p <*> return r
     go t                st                 = throwError err

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

@@ -0,0 +1,49 @@
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances    #-}
+
+module Language.Haskell.Liquid.Constraint.Constraint  where
+
+import Data.Monoid
+import Data.Maybe
+import Control.Applicative 
+
+import Language.Haskell.Liquid.Types
+import Language.Haskell.Liquid.Constraint.Types
+
+import Language.Fixpoint.Types           
+
+
+instance Monoid LConstraint where
+	mempty  = LC []
+	mappend (LC cs1) (LC cs2) = LC (cs1 ++ cs2) 
+
+typeToConstraint t = LC [t]
+
+
+addConstraints t γ = γ {lcs = mappend (typeToConstraint t) (lcs γ)}
+
+constraintToLogic γ (LC ts) = pAnd (constraintToLogicOne γ  <$> ts)
+
+constraintToLogicOne γ t
+  =  pAnd [subConstraintToLogicOne (zip xs xts) (last xs, (last $ (fst <$> xts), r))  | xts <- xss]
+  	where rep = toRTypeRep t
+  	      ts  = ty_args  rep
+  	      r   = ty_res   rep 
+  	      xs  = ty_binds rep 
+  	      xss = combinations ((\t -> [(x, t) | x <- grapBindsWithType t γ]) <$> ts)
+
+subConstraintToLogicOne xts (x', (x, t)) = PImp (pAnd rs) r
+  where
+  	(rs , su) = foldl go ([], []) xts
+  	([r], _ ) = go ([], su) (x', (x, t))
+  	go (acc, su) (x', (x, t)) = let (Reft(v, rr)) = toReft (fromMaybe mempty (stripRTypeBase t)) in
+                                let su' = (x', EVar x):(v, EVar x):su in
+                                (subst (mkSubst su') (pAnd [p | RConc p <- rr]):acc, su')
+
+
+
+combinations :: [[a]] -> [[a]]
+combinations []           = [[]]
+combinations ([]:_)       = []
+combinations ((y:ys):yss) = [y:xs | xs <- combinations yss] ++ combinations (ys:yss)
+

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

@@ -69,6 +69,7 @@ import Language.Haskell.Liquid.Literals
 import Control.DeepSeq
 
 import Language.Haskell.Liquid.Constraint.Types
+import Language.Haskell.Liquid.Constraint.Constraint
 
 -----------------------------------------------------------------------
 ------------- Constraint Generation: Toplevel -------------------------
@@ -179,6 +180,7 @@ measEnv sp xts cbs lts asms hs
         , trec  = Nothing
         , lcb   = M.empty
         , holes = fromListHEnv hs
+        , lcs   = mempty
         } 
     where
       tce = tcEmbeds sp
@@ -328,11 +330,11 @@ splitS (SubC γ (RAllE _ _ t1) t2)
 splitS (SubC γ t1 (RAllE _ _ t2))
   = splitS (SubC γ t1 t2)
 
-splitS (SubC γ (RRTy e r o t1) t2) 
-  = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ e 
-       c1 <- splitS (SubR γ' o r)
-       c2 <- splitS (SubC γ t1 t2)
-       return $ c1 ++ c2
+splitS (SubC γ (RRTy _ _ _ t1) t2) 
+  = splitS (SubC γ t1 t2)
+
+splitS (SubC γ t1 (RRTy _ _ _ t2)) 
+  = splitS (SubC γ t1 t2)
 
 splitS (SubC γ t1@(RFun x1 r1 r1' _) t2@(RFun x2 r2 r2' _)) 
   =  do cs       <- bsplitS t1 t2 
@@ -447,6 +449,20 @@ splitC (SubC γ t1 (RAllE x tx t2))
   = do γ' <- (γ, "addExBind 2") += (x, forallExprRefType γ tx)
        splitC (SubC γ' t1 t2)
 
+splitC (SubC γ (RRTy [(_, t)] _ OCons t1) t2)
+  = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ (zip xs ts)
+       c1 <- splitC (SubC γ' t1' t2')
+       c2 <- splitC (SubC γ  t1  t2 )
+       return $ c1 ++ c2
+  where
+    trep = toRTypeRep t
+    xs   = init $ ty_binds trep
+    ts   = init $ ty_args  trep
+    t2'  = ty_res   trep
+    t1'  = last $ ty_args trep
+
+
+
 splitC (SubC γ (RRTy e r o t1) t2) 
   = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ e 
        c1 <- splitC (SubR γ' o  r )
@@ -531,7 +547,14 @@ rsplitsCWithVariance γ t1s t2s variants
 
 
 bsplitC γ t1 t2
-  = checkStratum γ t1 t2 >> pruneRefs <$> get >>= return . bsplitC' γ t1 t2
+  = do checkStratum γ t1 t2 
+       pflag <- pruneRefs <$> get
+       γ' <- γ ++= ("bsplitC", v, t1) 
+       let r = (mempty :: UReft F.Reft){ur_reft = F.Reft (F.dummySymbol,  [F.RConc $ constraintToLogic γ' (lcs γ')])}
+       let t1' = t1 `strengthen` r
+       return $ bsplitC' γ' t1' t2 pflag
+  where
+    F.Reft(v, _) = ur_reft (fromMaybe mempty (stripRTypeBase t1))
 
 checkStratum γ t1 t2
   | s1 <:= s2 = return ()
@@ -541,9 +564,9 @@ checkStratum γ t1 t2
 
 bsplitC' γ t1 t2 pflag
   | F.isFunctionSortedReft r1' && F.isNonTrivialSortedReft r2'
-  = F.subC γ' F.PTrue (r1' {F.sr_reft = mempty}) r2' Nothing tag ci
+  = F.subC γ' grd (r1' {F.sr_reft = mempty}) r2' Nothing tag ci
   | F.isNonTrivialSortedReft r2'
-  = F.subC γ' F.PTrue r1'  r2' Nothing tag ci
+  = F.subC γ' grd r1'  r2' Nothing tag ci
   | otherwise
   = []
   where 
@@ -555,6 +578,7 @@ bsplitC' γ t1 t2 pflag
     err    = Just $ ErrSubType src (text "subtype") g t1 t2 
     src    = loc γ
     REnv g = renv γ 
+    grd    = F.PTrue
 
 
 
@@ -734,9 +758,13 @@ addPost γ (RRTy e r OInv t)
   = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("addPost", x,t)) γ e 
        addC (SubR γ' OInv r) "precondition" >> return t
 
-addPost γ (RRTy e r o t) 
+addPost γ (RRTy e r OTerm t) 
   = do γ' <- foldM (\γ (x, t) -> γ ++= ("addPost", x,t)) γ e 
-       addC (SubR γ' o r) "precondition" >> return t
+       addC (SubR γ' OTerm r) "precondition" >> return t
+
+addPost _ (RRTy _ _ OCons t) 
+  = return t
+
 addPost _ t  
   = return t
 
@@ -1171,6 +1199,10 @@ cconsE γ e@(Let b@(NonRec x _) ee) t
   where
        isDefLazyVar = L.isPrefixOf "fail" . showPpr
 
+
+cconsE γ e (RRTy [(_, cs)] _ OCons t)
+  = cconsE (addConstraints cs γ) e t
+
 cconsE γ (Let b e) t    
   = do γ'  <- consCBLet γ b
        cconsE γ' e t 
@@ -1269,7 +1301,8 @@ consE γ e'@(App e a)
   = do ([], πs, ls, te) <- bkUniv <$> consE γ e
        te0              <- instantiatePreds γ e' $ foldr RAllP te πs 
        te'              <- instantiateStrata ls te0
-       (γ', te'')       <- dropExists γ te'
+       (γ', te''')      <- dropExists γ te'
+       te''             <- dropConstraints γ te'''
        updateLocA πs (exprLoc e) te'' 
        let RFun x tx t _ = checkFun ("Non-fun App with caller ", e') te''
        pushConsBind      $ cconsE γ' a tx 
@@ -1363,6 +1396,20 @@ checkUnbound γ e x t
 dropExists γ (REx x tx t) = liftM (, t) $ (γ, "dropExists") += (x, tx)
 dropExists γ t            = return (γ, t)
 
+
+dropConstraints γ (RRTy [(_, ct)] _ OCons t) 
+  = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ (zip xs ts)
+       addC (SubC  γ' t1 t2)  "dropConstraints"
+       dropConstraints γ  t
+  where
+    trep = toRTypeRep ct
+    xs   = init $ ty_binds trep
+    ts   = init $ ty_args  trep
+    t2   = ty_res   trep
+    t1   = last $ ty_args trep
+
+dropConstraints _ t = return t
+
 -------------------------------------------------------------------------------------
 cconsCase :: CGEnv -> Var -> SpecType -> [AltCon] -> (AltCon, [Var], CoreExpr) -> CG ()
 -------------------------------------------------------------------------------------
@@ -1532,7 +1579,7 @@ subsTyVar_meet' (α, t) = subsTyVar_meet (α, toRSort t, t)
 -----------------------------------------------------------------------
 
 instance NFData CGEnv where
-  rnf (CGE x1 x2 x3 x5 x6 x7 x8 x9 _ _ x10 _ _ _ _)
+  rnf (CGE x1 x2 x3 x5 x6 x7 x8 x9 _ _ x10 _ _ _ _ _)
     = x1 `seq` rnf x2 `seq` seq x3 `seq` rnf x5 `seq` 
       rnf x6  `seq` x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10
 
@@ -1601,9 +1648,6 @@ forallExprReftLookup γ x = snap <$> F.lookupSEnv x (syenv γ)
   where 
     snap                 = mapThd3 ignoreOblig . bkArrow . fourth4 . bkUniv . (γ ?=) . F.symbol
 
-grapBindsWithType tx γ 
-  = fst <$> toListREnv (filterREnv ((== toRSort tx) . toRSort) (renv γ))
-
 splitExistsCases z xs tx
   = fmap $ fmap (exrefAddEq z xs tx)
 
@@ -1666,19 +1710,5 @@ extendγ γ xts
   = foldr (\(x,t) m -> M.insert x t m) γ xts
 
 
----------------------------------------------------------------
------ Refinement Type Environments ----------------------------
----------------------------------------------------------------
-
 instance NFData REnv where
   rnf (REnv _) = () -- rnf m
-
-toListREnv (REnv env)     = M.toList env
-filterREnv f (REnv env)   = REnv $ M.filter f env
-fromListREnv              = REnv . M.fromList
-deleteREnv x (REnv env)   = REnv (M.delete x env)
-insertREnv x y (REnv env) = REnv (M.insert x y env)
-lookupREnv x (REnv env)   = M.lookup x env
-memberREnv x (REnv env)   = M.member x env
-
-

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

@@ -19,6 +19,7 @@ import Data.Maybe               (catMaybes)
 
 import Var
 
+
 import Language.Haskell.Liquid.Types
 import Language.Haskell.Liquid.Strata
 import Language.Haskell.Liquid.Misc     (fourth4)
@@ -30,7 +31,6 @@ import Language.Fixpoint.Misc
 
 import qualified Language.Haskell.Liquid.CTags      as Tg
 
-
 data CGEnv 
   = CGE { loc    :: !SrcSpan           -- ^ Location in original source file
         , renv   :: !REnv              -- ^ SpecTypes for Bindings in scope
@@ -48,8 +48,13 @@ data CGEnv
         , trec  :: !(Maybe (M.HashMap F.Symbol SpecType)) -- ^ Type of recursive function with decreasing constraints
         , lcb   :: !(M.HashMap F.Symbol CoreExpr) -- ^ Let binding that have not been checked
         , holes :: !HEnv               -- ^ Types with holes, will need refreshing
+        , lcs   :: !LConstraint  -- ^ Logical Constraints
         } -- deriving (Data, Typeable)
 
+
+data LConstraint = LC [SpecType]
+
+
 instance PPrint CGEnv where
   pprint = pprint . renv
 
@@ -215,6 +220,27 @@ conjoinInvariant t _
   = t
 
 
+
+grapBindsWithType tx γ 
+  = fst <$> toListREnv (filterREnv ((== toRSort tx) . toRSort) (renv γ))
+
+---------------------------------------------------------------
+----- Refinement Type Environments ----------------------------
+---------------------------------------------------------------
+
+
+
+toListREnv (REnv env)     = M.toList env
+filterREnv f (REnv env)   = REnv $ M.filter f env
+fromListREnv              = REnv . M.fromList
+deleteREnv x (REnv env)   = REnv (M.delete x env)
+insertREnv x y (REnv env) = REnv (M.insert x y env)
+lookupREnv x (REnv env)   = M.lookup x env
+memberREnv x (REnv env)   = M.member x env
+
+
+
+
 ------------------------------------------------------------------------------
 ------------------------------------------------------------------------------
 ------------------------ Fixpoint Environment --------------------------------

src/Language/Haskell/Liquid/Errors.hs

@@ -146,6 +146,9 @@ blankLine    = sizedText 5 " "
 ppError' :: (PPrint a) => Tidy -> Doc -> TError a -> Doc
 -----------------------------------------------------------------------
 
+ppError' _ dSp (ErrAssType _ OCons _ _)
+  = dSp <+> text "Constraint Check"
+
 ppError' _ dSp (ErrAssType _ OTerm _ _)
   = dSp <+> text "Termination Check"
 

src/Language/Haskell/Liquid/Parse.hs

@@ -164,6 +164,7 @@ bareTypeP
  <|> bareAllS
  <|> bareAllExprP
  <|> bareExistsP
+ <|> try bareConstraintP
  <|> try bareFunP
  <|> bareAtomP (refBindP bindP)
  <|> try (angles (do t <- parens $ bareTypeP
@@ -228,6 +229,18 @@ bareAllExprP
        t  <- bareTypeP
        return $ foldr (uncurry RAllE) t zs
 
+bareConstraintP
+  = do ct   <- braces bareTypeP
+       t    <- bareTypeP 
+       return $ rrTy ct t 
+
+
+rrTy ct t = RRTy [(dummySymbol, ct)] mempty OCons t -- fromRTypeRep rep{ty_res = t'}
+--   where 
+--     rep = toRTypeRep t
+--     t'  = RRTy [(dummySymbol, ct)] mempty OCons (ty_res rep) 
+
+
 bareExistsP 
   = do reserved "exists"
        zs <- brackets $ sepBy1 exBindP comma 

src/Language/Haskell/Liquid/RefType.hs

@@ -512,6 +512,7 @@ freeTyVars (REx _ _ t)     = freeTyVars t
 freeTyVars (RExprArg _)    = []
 freeTyVars (RAppTy t t' _) = freeTyVars t `L.union` freeTyVars t'
 freeTyVars (RHole _)       = []
+freeTyVars (RRTy e _ _ t)  = L.nub $ concatMap freeTyVars (t:(snd <$> e))
 freeTyVars t               = errorstar ("RefType.freeTyVars cannot handle" ++ show t)