Omega 0.2.0 → 0.2.1

raw patch · 3 files changed

+39/−18 lines, 3 filessetup-changed

Files

• Data/Presburger/Omega/Expr.hs +32/−11
• Omega.cabal +2/−2
• Setup.hs +5/−5

@@ -515,7 +515,8 @@ appPrec = 10 mulPrec = 7 addPrec = 6-cmpPrec = 5                     -- Less-than, equal+cmpPrec = 4                     -- Less-than, equal+andPrec = 3 lamPrec = 0  -- An environment for showing expressions.@@ -594,20 +595,16 @@     case expression     of CAUE Conj lit es            | lit        -> let texts = map (showsBoolExprPrec env 0) es-                           in texts `showSepBy` showString " |&&| "+                           in showParen (n >= andPrec) $+                              texts `showSepBy` showString " |&&| "            | otherwise  -> showString "falseE"        CAUE Disj lit es            | lit        -> showString "trueE"            | otherwise  -> let texts = map (showsBoolExprPrec env 0) es                            in showParen (n >= appPrec) $                               showString "disjE " . showsList texts-       PredE IsGEZ e    -> showParen (n >= appPrec) $ showGEZ env e-       PredE p e        -> let operator =-                                   case p-                                   of IsZero -> showString "isZeroE "-                                      IsGEZ  -> showString "isNonnegativeE "-                           in showParen (n >= appPrec) $-                              operator . showsIntExprPrec env appPrec e+       PredE IsGEZ e    -> showGEZ env n e+       PredE IsZero e   -> showEQZ env n e        NotE e           -> showString "notE " . showsBoolExprPrec env appPrec e        LitE True        -> showString "trueE"        LitE False       -> showString "falseE"@@ -622,8 +619,15 @@ -- Use ">" if it gets rid of a term, otherwise use ">=". -- If the left side of the inequality is an integer literal, -- then move it to the right -showGEZ :: ShowsEnv -> IntExpr -> ShowS-showGEZ env (CAUE Sum lit es) =+showGEZ :: ShowsEnv -> Int -> IntExpr -> ShowS+showGEZ env prec e =+    showParen (prec >= cmpPrec) $+    case e+    of LitE n          -> showGEZ' env n []+       CAUE Sum lit es -> showGEZ' env lit es+       _               -> showGEZ' env 0 [e]++showGEZ' env lit es =     -- Partition into terms that will go on the left (positive) and right     -- (negative) sides of the inequality.  Try to get rid of a '1' by     -- using a greater-than sign.@@ -659,6 +663,23 @@       gt = showString " |>| "       le = showString " |<=| "       lt = showString " |<| "+++-- Show a comparison-to-zero prettily.+-- If it is a summation with only one term, then we show it as+--   "term |==| literal"+-- Otherwise we show it as an application of "isZeroE".+showEQZ :: ShowsEnv -> Int -> IntExpr -> ShowS+showEQZ env prec (CAUE Sum lit [e]) =+    showParen (prec >= cmpPrec) $+    (showsIntExprPrec env cmpPrec e .+     showString " |==| " .+     showsIntExprPrec env cmpPrec (LitE lit)+    )++showEQZ env prec e =+    showParen (prec >= appPrec) $+    showString "isZeroE " . showsIntExprPrec env appPrec e  -- Partition a sum term based on the sign it is displayed with. -- Negative-signed terms are multiplied by -1 to make them positive.

@@ -1,6 +1,6 @@-Cabal-Version:		>= 1.2.3 && < 1.8+Cabal-Version:		>= 1.2.3 && < 1.9 Name:			Omega-Version:		0.2.0+Version:		0.2.1 Build-Type:		Custom License:		BSD3 License-File:		LICENSE

@@ -142,8 +142,7 @@    -- Get 'ar' and 'ld' programs   let verb = fromFlagOrDefault Verbosity.normal $ buildVerbosity flags-  (arPgm, _) <- requireProgram verb arProgram AnyVersion (withPrograms lbi)-  let runAr = rawSystemProgram verb arPgm+  let runAr = rawSystemProgramConf verb arProgram (withPrograms lbi)    -- Build the C++ source file (and Omega library, if configured)   -- Makefile's behavior is controlled by output of 'configure'@@ -214,9 +213,10 @@   let verb = fromFlagOrDefault Verbosity.normal $ cleanVerbosity flags    -- run 'make clean', which will clean the Omega library if appropriate-  case mlbi of-    Just lbi -> rawSystemProgramConf verb makeProgram (withPrograms lbi) ["clean"]-    Nothing -> return ()+  pgmConf <- configureProgram verb makeProgram defaultProgramConfiguration+  makeExists <- doesFileExist "Makefile"+  when makeExists $+       rawSystemProgramConf verb makeProgram pgmConf ["clean"]    -- Clean extra files if we don't need to save configuration   -- (Other temp files are automatically cleaned)