Merge pull request #719 from ucsd-progsys/fd/less-monoids

Fd/less monoids

src/Language/Fixpoint/Parse.hs

@@ -1099,7 +1099,7 @@ pred0P =  trueP -- constant "true"
 makeUniquePGrad :: Parser Expr
 makeUniquePGrad
   = do uniquePos <- getSourcePos
-       return $ PGrad (KV $ symbol $ show uniquePos) mempty (srcGradInfo uniquePos) mempty
+       return $ PGrad (KV $ symbol $ show uniquePos) mempty (srcGradInfo uniquePos) PTrue
 
 -- qmP    = reserved "?" <|> reserved "Bexp"
 
@@ -1435,7 +1435,7 @@ defsFInfo defs = {- SCC "defsFI" -} Types.FI cm ws bs ebs lts dts kts qs binfo a
                    "defs-ws"        [(i, w)              | Wfc w    <- defs, let i = Misc.thd3 (wrft w)]
     bs         = bindEnvFromList  $ exBinds ++ [(n,(x,r,a)) | IBind n x r a <- defs]
     ebs        =                    [ n                  | (n,_) <- exBinds]
-    exBinds    =                    [(n, (x, RR t mempty, a)) | EBind n x t a <- defs]
+    exBinds    =                    [(n, (x, RR t trueReft, a)) | EBind n x t a <- defs]
     lts        = fromListSEnv       [(x, t)             | Con x t     <- defs]
     dts        = fromListSEnv       [(x, t)             | Dis x t     <- defs]
     kts        = KS $ S.fromList    [k                  | Kut k       <- defs]

src/Language/Fixpoint/Solver/TrivialSort.hs

@@ -173,7 +173,7 @@ simplifySubC tm (i, c)
 simplifySortedReft :: NonTrivSorts -> SortedReft -> SortedReft
 simplifySortedReft tm sr
   | nonTrivial = sr
-  | otherwise  = sr { sr_reft = mempty }
+  | otherwise  = sr { sr_reft = trueReft }
   where
     nonTrivial = isNonTrivialSort tm (sr_sort sr)
 

src/Language/Fixpoint/Types/Constraints.hs

@@ -524,7 +524,7 @@ instance FromJSON Rewrite     where
 
 
 trueQual :: Qualifier
-trueQual = Q (symbol ("QTrue" :: String)) [] mempty (dummyPos "trueQual")
+trueQual = Q (symbol ("QTrue" :: String)) [] PTrue (dummyPos "trueQual")
 
 instance Loc Qualifier where
   srcSpan q = SS l l

src/Language/Fixpoint/Types/Solutions.hs

@@ -381,7 +381,7 @@ instance Loc EQual where
   srcSpan = srcSpan . eqQual
 
 trueEqual :: EQual
-trueEqual = EQL trueQual mempty []
+trueEqual = EQL trueQual PTrue []
 
 instance PPrint EQual where
   pprintTidy k = pprintTidy k . eqPred

src/Language/Fixpoint/Types/Sorts.hs

@@ -623,17 +623,6 @@ instance NFData DataCtor
 instance NFData DataDecl
 instance NFData Sub
 
-instance Semigroup Sort where
-  t1 <> t2
-    | t1 == mempty  = t2
-    | t2 == mempty  = t1
-    | t1 == t2      = t1
-    | otherwise     = errorstar $ "mappend-sort: conflicting sorts t1 =" ++ show t1 ++ " t2 = " ++ show t2
-
-instance Monoid Sort where
-  mempty  = FObj "any"
-  mappend = (<>)
-
 -------------------------------------------------------------------------------
 -- | Embedding stuff as Sorts
 -------------------------------------------------------------------------------

src/Language/Fixpoint/Types/Substitutions.hs

@@ -179,33 +179,11 @@ disjoint (Su su) bs = S.null $ suSyms `S.intersection` bsSyms
     suSyms = S.fromList $ syms (M.elems su) ++ syms (M.keys su)
     bsSyms = S.fromList $ syms $ fst <$> bs
 
-instance Semigroup Expr where
-  p <> q = pAnd [p, q]
-
-instance Monoid Expr where
-  mempty  = PTrue
-  mappend = (<>)
-  mconcat = pAnd
-
-instance Semigroup Reft where
-  (<>) = meetReft
-
-instance Monoid Reft where
-  mempty  = trueReft
-  mappend = (<>)
-
 meetReft :: Reft -> Reft -> Reft
 meetReft (Reft (v, ra)) (Reft (v', ra'))
-  | v == v'          = Reft (v , ra  `mappend` ra')
-  | v == dummySymbol = Reft (v', ra' `mappend` (ra `subst1`  (v , EVar v')))
-  | otherwise        = Reft (v , ra  `mappend` (ra' `subst1` (v', EVar v )))
-
-instance Semigroup SortedReft where
-  t1 <> t2 = RR (mappend (sr_sort t1) (sr_sort t2)) (mappend (sr_reft t1) (sr_reft t2))
-
-instance Monoid SortedReft where
-  mempty  = RR mempty mempty
-  mappend = (<>)
+  | v == v'          = Reft (v , pAnd [ra, ra'])
+  | v == dummySymbol = Reft (v', pAnd [ra', ra `subst1`  (v , EVar v')])
+  | otherwise        = Reft (v , pAnd [ra, ra' `subst1` (v', EVar v )])
 
 instance Subable Reft where
   syms (Reft (v, ras))      = v : syms ras