Move Reftable to liquidhaskell

src/Language/Fixpoint/Solver/UniqifyBinds.hs

@@ -47,7 +47,7 @@ dropUnusedBinds fi = fi {bs = filterBindEnv isUsed (bs fi)}-- { bs = mapBindEnv
     -- _tx i (x, r)
     -- | isUsed i    = (x, r)
     -- | otherwise   = (x, top r)
-    isUsed i _x r  = {- tracepp (unwords ["isUsed", show i, showpp _x]) $ -} memberIBindEnv i usedBinds || isTauto r
+    isUsed i _x r  = memberIBindEnv i usedBinds || isTautoReft (sr_reft r)
     usedBinds      = L.foldl' unionIBindEnv emptyIBindEnv (cEnvs ++ wEnvs)
     wEnvs          = wenv <$> M.elems (ws fi)
     cEnvs          = senv <$> M.elems (cm fi)

src/Language/Fixpoint/Solver/UniqifyKVars.hs

@@ -105,7 +105,7 @@ accumBinds k a (fi, ids) i = (fi', i' : ids)
 newTopBind :: Symbol -> SortedReft -> a -> SInfo a -> (BindId, SInfo a)
 newTopBind x sr a fi = (i', fi {bs = be'})
   where
-    (i', be')        = insertBindEnv x (top sr) a (bs fi)
+    (i', be')        = insertBindEnv x (sr {sr_reft = trueReft}) a (bs fi)
 
 --------------------------------------------------------------
 

src/Language/Fixpoint/Types/Refinements.hs

@@ -51,7 +51,6 @@ module Language.Fixpoint.Types.Refinements (
   , Expression (..)
   , Predicate (..)
   , Subable (..)
-  , Reftable (..)
 
   -- * Constructors
   , reft                    -- "smart
@@ -72,6 +71,7 @@ module Language.Fixpoint.Types.Refinements (
   , isNonTrivial
   , isContraPred
   , isTautoPred
+  , isTautoReft
   , isSingletonExpr
   , isSingletonReft
   , isFalse
@@ -970,8 +970,11 @@ mapPredReft f (Reft (v, p)) = Reft (v, f p)
 isFunctionSortedReft :: SortedReft -> Bool
 isFunctionSortedReft = isJust . functionSort . sr_sort
 
-isNonTrivial :: Reftable r => r -> Bool
-isNonTrivial = not . isTauto
+isNonTrivial :: SortedReft -> Bool
+isNonTrivial = not . isTautoReft . sr_reft
+
+isTautoReft :: Reft -> Bool
+isTautoReft = all isTautoPred . conjuncts . reftPred
 
 reftPred :: Reft -> Expr
 reftPred (Reft (_, p)) = p
@@ -1058,19 +1061,5 @@ instance Subable a => Subable (Located a) where
   substf f (Loc l l' x) = Loc l l' (substf f x)
   subst su (Loc l l' x) = Loc l l' (subst su x)
 
-
-class (Monoid r, Subable r) => Reftable r where
-  isTauto :: r -> Bool
-  ppTy    :: r -> Doc -> Doc
-
-  top     :: r -> r
-  top _   =  mempty
-
-  meet    :: r -> r -> r
-  meet    = mappend
-
-  toReft  :: r -> Reft
-  ofReft  :: Reft -> r
-
 instance Fixpoint Doc where
   toFix = id

src/Language/Fixpoint/Types/Substitutions.hs

@@ -16,6 +16,8 @@ module Language.Fixpoint.Types.Substitutions (
   , filterSubst
   , catSubst
   , exprSymbolsSet
+  , meetReft
+  , pprReft
   ) where
 
 import           Data.Maybe
@@ -218,39 +220,17 @@ instance Subable SortedReft where
   substf f (RR so r) = RR so $ substf f r
   substa f (RR so r) = RR so $ substa f r
 
-instance Reftable () where
-  isTauto _ = True
-  ppTy _  d = d
-  top  _    = ()
-  meet _ _  = ()
-  toReft _  = mempty
-  ofReft _  = mempty
-
-instance Reftable Reft where
-  isTauto  = all isTautoPred . conjuncts . reftPred
-  ppTy     = pprReft
-  toReft   = id
-  ofReft   = id
-  top (Reft(v,_)) = Reft (v, mempty)
-
 pprReft :: Reft -> Doc -> Doc
 pprReft (Reft (v, p)) d
   | isTautoPred p
   = d
   | otherwise
   = braces (toFix v <+> colon <+> d <+> text "|" <+> ppRas [p])
 
-instance Reftable SortedReft where
-  isTauto  = isTauto . toReft
-  ppTy     = ppTy . toReft
-  toReft   = sr_reft
-  ofReft   = errorstar "No instance of ofReft for SortedReft"
-  top s    = s { sr_reft = trueReft }
-
 -- RJ: this depends on `isTauto` hence, here.
 instance PPrint Reft where
   pprintTidy k r
-    | isTauto r        = text "true"
+    | isTautoReft r        = text "true"
     | otherwise        = pprintReft k r
 
 instance PPrint SortedReft where