diff --git a/Data/Presburger/Omega/Expr.hs b/Data/Presburger/Omega/Expr.hs --- a/Data/Presburger/Omega/Expr.hs +++ b/Data/Presburger/Omega/Expr.hs @@ -299,7 +299,7 @@ of CAUE Sum lit es -> sumE lit $ map (rec env) es CAUE Prod lit es -> prodE lit $ map (rec env) es LitE n -> litE n - VarE (Bound i) -> env `index` i + VarE (Bound i) -> env `genericIndex` i VarE _ -> error "Expr.fold: unexpected variable" -- Like (!!), but throws a useful error message @@ -595,7 +595,7 @@ case expression of CAUE Conj lit es | lit -> let texts = map (showsBoolExprPrec env 0) es - in showParen (n >= andPrec) $ + in showParen (n >= fromIntegral andPrec) $ texts `showSepBy` showString " |&&| " | otherwise -> showString "falseE" CAUE Disj lit es @@ -1105,4 +1105,5 @@ check' (VarE (Quantified _)) = quantifiedVar check' (QuantE _ e) = check (n+1) e + quantifiedVar :: Bool quantifiedVar = error "variablesWithinRange: unexpected variable" diff --git a/Data/Presburger/Omega/LowLevel.hsc b/Data/Presburger/Omega/LowLevel.hsc --- a/Data/Presburger/Omega/LowLevel.hsc +++ b/Data/Presburger/Omega/LowLevel.hsc @@ -804,24 +804,35 @@ fromPtr =<< withPresburger2 rel1 rel2 hsw_composition | otherwise = error "composition: argument arities do not agree" +-- | Restrict the domain of a relation. +-- If @domain r@ is @d@, then @domain =<< restrictDomain r s@ +-- is @intersection d s@. restrictDomain :: OmegaRel -> OmegaSet -> IO OmegaRel restrictDomain rel1 set | length (rDom rel1) == length (sDom set) = fromPtr =<< withPresburger2 rel1 set hsw_restrict_domain | otherwise = error "restrictDomain: argument arities do not agree" +-- | Restrict the range of a relation. +-- If @range r@ is @d@, then @range =<< restrictRange r s@ +-- is @intersection d s@. restrictRange :: OmegaRel -> OmegaSet -> IO OmegaRel restrictRange rel1 set | length (rDom rel1) == length (sDom set) = fromPtr =<< withPresburger2 rel1 set hsw_restrict_range | otherwise = error "restrictRange: argument arities do not agree" +-- | Compute the difference of two relations or sets. +-- The members of @difference x y@ are the members of @x@ that are not +-- members of @y@. difference :: Presburger a => a -> a -> IO a difference rel1 rel2 | sameArity rel1 rel2 = fromPtr =<< withPresburger2 rel1 rel2 hsw_difference | otherwise = error "difference: arguments have different arities" +-- | Compute the cross product of two sets. +-- The cross product relates every element of @s@ to every element of @y@. crossProduct :: OmegaSet -> OmegaSet -> IO OmegaRel crossProduct set1 set2 = fromPtr =<< withPresburger2 set1 set2 hsw_cross_product diff --git a/Data/Presburger/Omega/Rel.hs b/Data/Presburger/Omega/Rel.hs --- a/Data/Presburger/Omega/Rel.hs +++ b/Data/Presburger/Omega/Rel.hs @@ -243,12 +243,15 @@ definiteTautology :: Rel -> Bool definiteTautology = useRel L.definiteTautology +-- | True if the relation has no UNKNOWN constraints. exact :: Rel -> Bool exact = useRel L.exact +-- | True if the relation has UNKNOWN constraints. inexact :: Rel -> Bool inexact = useRel L.inexact +-- | True if the relation is entirely UNKNOWN. unknown :: Rel -> Bool unknown = useRel L.unknown @@ -295,11 +298,17 @@ join :: Rel -> Rel -> Rel join r1 r2 = composition r2 r1 +-- | Restrict the domain of a relation. +-- +-- > domain (restrictDomain r s) === intersection (domain r) s restrictDomain :: Rel -> Set -> Rel restrictDomain r s = unsafePerformIO $ omegaRelToRel (relInpDim r) (relOutDim r) =<< L.restrictDomain (relOmegaRel r) (Set.toOmegaSet s) +-- | Restrict the range of a relation. +-- +-- > range (restrictRange r s) === intersection (range r) s restrictRange :: Rel -> Set -> Rel restrictRange r s = unsafePerformIO $ omegaRelToRel (relInpDim r) (relOutDim r) =<< @@ -332,18 +341,26 @@ gist effort r1 r2 = useRel2Rel (L.gist effort) (relInpDim r1) (relOutDim r1) r1 r2 +-- | Get the transitive closure of a relation. In some cases, the transitive +-- closure cannot be computed exactly, in which case a lower bound is +-- returned. transitiveClosure :: Rel -> Rel transitiveClosure r = useRelRel L.transitiveClosure (relInpDim r) (relOutDim r) r +-- | Invert a relation, swapping the domain and range. inverse :: Rel -> Rel inverse s = useRelRel L.inverse (relOutDim s) (relInpDim s) s +-- | Get the complement of a relation. complement :: Rel -> Rel complement s = useRelRel L.complement (relInpDim s) (relOutDim s) s deltas :: Rel -> Set deltas = useRel (\wrel -> Set.fromOmegaSet =<< L.deltas wrel) +-- | Approximate a relation by allowing all existentially quantified +-- variables to take on rational values. This allows these variables to be +-- eliminated from the formula. approximate :: Rel -> Rel approximate s = useRelRel L.approximate (relInpDim s) (relOutDim s) s diff --git a/Data/Presburger/Omega/Set.hs b/Data/Presburger/Omega/Set.hs --- a/Data/Presburger/Omega/Set.hs +++ b/Data/Presburger/Omega/Set.hs @@ -150,9 +150,13 @@ toOmegaSet :: Set -> OmegaSet toOmegaSet = setOmegaSet +-- | Compute the upper bound of a set by setting all UNKNOWN +-- constraints to true. upperBound :: Set -> Set upperBound s = useSetSet L.upperBound (setDim s) s +-- | Compute the lower bound of a set by setting all UNKNOWN +-- constraints to false. lowerBound :: Set -> Set lowerBound s = useSetSet L.lowerBound (setDim s) s @@ -168,12 +172,15 @@ definiteTautology :: Set -> Bool definiteTautology = useSet L.definiteTautology +-- | True if the set has no UNKNOWN constraints. exact :: Set -> Bool exact = useSet L.exact +-- | True if the set has UNKNOWN constraints. inexact :: Set -> Bool inexact = useSet L.inexact +-- | True if the set is completely UNKNOWN. unknown :: Set -> Bool unknown = useSet L.unknown diff --git a/Omega.cabal b/Omega.cabal --- a/Omega.cabal +++ b/Omega.cabal @@ -1,6 +1,6 @@ -Cabal-Version: >= 1.2.3 && < 1.9 +Cabal-Version: >= 1.2.3 Name: Omega -Version: 0.2.2 +Version: 1.0 Build-Type: Custom License: BSD3 License-File: LICENSE @@ -30,7 +30,7 @@ Default: False Library - Build-Depends: base >= 3 && < 4, containers + Build-Depends: base >= 4 && < 5, containers Exposed-Modules: Data.Presburger.Omega.Expr Data.Presburger.Omega.LowLevel