Omega 0.2.2 → 1.0

raw patch · 5 files changed

+41/−5 lines, 5 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• Data/Presburger/Omega/Expr.hs +3/−2
• Data/Presburger/Omega/LowLevel.hsc +11/−0
• Data/Presburger/Omega/Rel.hs +17/−0
• Data/Presburger/Omega/Set.hs +7/−0
• Omega.cabal +3/−3

@@ -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"

@@ -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

@@ -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

@@ -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 

@@ -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