Index: /sizechecking/Constraints.hs =================================================================== --- /sizechecking/Constraints.hs (revision 5) +++ /sizechecking/Constraints.hs (revision 6) @@ -12,9 +12,9 @@ import Data.SBV ( (.==), (.<), (.>=)) import Control.Monad -import Data.IORef +import Data.IORef() import Data.Supply as S asType :: a -> a -> a -asType a b = a +asType a _ = a data D = D { var::Int, cond::[Condition] } @@ -36,5 +36,5 @@ appall :: Int -> [L] -> L -appall var l = foldl (App) (Var $ var) $ l +appall var = foldl App (Var var) @@ -76,5 +76,5 @@ [] -> (Num 0, b) _ -> (expr, b) - (_, _) -> error $ "Expression in condition" ++ (show c) + (_, _) -> error $ "Expression in condition" ++ show c where nonzero = List.sortBy (Ord.comparing snd) $ filter ((/=0).fst) a @@ -111,5 +111,4 @@ norm (AAbs a b e) = ([], 0, [AAbs a b (normalize e)], []) norm (Shift a b c) = ([], 0, [Shift (normalize a) (normalize b) (normalize c)], []) -norm (Aggr a b c) = ([], 0, [Aggr a (normalize b) (normalize c)], []) norm (Unsized) = ([], 0, [Unsized], []) norm (Bottom) = ([], 0, [Bottom], []) @@ -159,12 +158,12 @@ l1 <- checkCond1 v1 (Condition ((h `LTC` f):d) e' x) l2 <- checkCond1 v2 (Condition ((h `GEC` f):d) g' x) - putStrLn $ " -> " ++ (show l1) - putStrLn $ " -> " ++ (show l2) + putStrLn $ " -> " ++ show l1 + putStrLn $ " -> " ++ show l2 return $ l1 ++ l2 - checkCond1 v z@(Condition d (App (Var a) x) (App (Var b) y)) | a==b = do + checkCond1 v z@(Condition d (App (Var a) x) (App (Var b) y)) | a==b = checkCond1 v (Condition d x y) - checkCond1 v p@(Condition d x z@(App (Shift e f g) h)) = do + checkCond1 v p@(Condition d x z@(App (Shift e f g) h)) = checkCond1 v (Condition d z x) - checkCond1 v z@(Condition d a b) = return $ [Condition dd (normalize a) (normalize b)] + checkCond1 v z@(Condition d a b) = return [Condition dd (normalize a) (normalize b)] where dd = normalizecs d @@ -174,5 +173,4 @@ subst ndl hst (AAbs a b e) = AAbs a b (subst ndl hst e) subst ndl hst (Shift a b c) = Shift (subst ndl hst a) (subst ndl hst b) (subst ndl hst c) -subst ndl hst (Aggr a b c) = Aggr a (subst ndl hst b) (subst ndl hst c) subst ndl hst (Unsized) = Unsized subst ndl hst (Bottom) = Bottom @@ -201,5 +199,5 @@ solve l supply = do ll <- forM (zip l $ split supply) (\(c,s) -> do - putStrLn $ "\nSOLVING "++(show c) + putStrLn $ "\nSOLVING " ++ show c solve1 s c ) @@ -227,8 +225,8 @@ checkConds [] = False - checkConds ((LTC a b):xs) | (elem (GEC a b) xs) = True - checkConds ((GEC a b):xs) | (elem (LTC a b) xs) = True - checkConds ((LTC a (Num b)):xs) | b<=0 && elem (Zero a) xs = True - checkConds ((GEC a (Num b)):xs) | b>0 && elem (Zero a) xs = True + checkConds (LTC a b : xs) | GEC a b `elem` xs = True + checkConds (GEC a b : xs) | LTC a b `elem` xs = True + checkConds (LTC a (Num b) : xs) | b<=0 && elem (Zero a) xs = True + checkConds (GEC a (Num b) : xs) | b>0 && elem (Zero a) xs = True checkConds (_:xs) = checkConds xs @@ -259,23 +257,22 @@ return [] | a==b = do - putStrLn $ "Equals" + putStrLn "Equals" return [] | Just (var, nl) <- searchzero d = do - let x = (Condition (Prelude.map (normalizec.substc var (Num 0)) nl) + let x = Condition (Prelude.map (normalizec.substc var (Num 0)) nl) (normalize$subst var (Num 0) a) (normalize$subst var (Num 0) b) - ) - putStrLn $ (show $ Var var) ++" is zero:\n" ++ (show x) + + putStrLn $ show (Var var) ++ " is zero:\n" ++ show x solve1 supp x | Just (var, exp, nl) <- searcheq d [] = do - putStrLn $ "Found equation "++(show $ Var var) ++ " = "++(show exp) - let x = (Condition (Prelude.map (normalizec.substc var exp) nl ) + putStrLn $ "Found equation " ++ show (Var var) ++ " = " ++ show exp + let x = Condition (Prelude.map (normalizec.substc var exp) nl ) (normalize$subst var exp a) (normalize$subst var exp b) - ) - putStrLn $ "New equations:\n" ++ (show x) + putStrLn $ "New equations:\n" ++ show x solve1 supp x | App p q <- a, App r s <- b = do - putStrLn $ "Branching!" + putStrLn "Branching!" nc <- checkCond supp [Condition d p r, Condition d q s] solve nc supp @@ -291,6 +288,6 @@ -- | Abs _ _ <- a, AAbs _ _ _ <- b = applyList a b d supp -- | AAbs _ _ _ <- a, AAbs _ _ _ <- b = applyList a b d supp - | Just dd <- reorder d = do - putStrLn $ "Reorder " ++ (show dd) + | Just dd <- reorder d = do + putStrLn $ "Reorder " ++ show dd solve1 supp $ Condition dd a b | otherwise = do @@ -309,9 +306,9 @@ compiletosolver :: L -> L -> [Constraint] -> SBV.Symbolic SBV.SBool compiletosolver a b d = do - let fvs = Set.toList $ Set.unions $ (fv a):(fv b):(map fvc d) - (vars::[SBV.SInteger]) <- mapM SBV.free $ map (flip showVar "") fvs + let fvs = Set.toList $ Set.unions $ fv a : fv b : map fvc d + (vars::[SBV.SInteger]) <- mapM (SBV.free . flip showVar "") fvs let varmap = Map.fromList $ zip fvs vars - mapM SBV.constrain $ map (compilec varmap) d - return $ (compilel varmap a) .== (compilel varmap b) + mapM_ (SBV.constrain . compilec varmap) d + return $ compilel varmap a .== compilel varmap b compilec v (Zero a) = compilel v a .== (0::SBV.SInteger) @@ -329,3 +326,3 @@ compilel v (Var a) | Just x<-Map.lookup a v = x compilel v (Num a) = SBV.literal $ fromIntegral a -compilel v a = error $ "Cannot compile "++(show a) +compilel v a = error $ "Cannot compile " ++ show a Index: /sizechecking/Lambda.hs =================================================================== --- /sizechecking/Lambda.hs (revision 5) +++ /sizechecking/Lambda.hs (revision 6) @@ -12,9 +12,9 @@ data L = Abs Int L | App L L | Var Int | Num Int | Op L Char L | List L L | AAbs Int Int L - | Shift L L L | Unsized | Bottom | Aggr String L L + | Shift L L L | Unsized | Bottom deriving Eq showVar x = if x>28 - then showVar (x `div` 29) . (showChar $ chr $ ord 'a' + (x `mod` 29)) + then showVar (x `div` 29) . showChar (chr $ ord 'a' + (x `mod` 29)) else showChar $ chr $ ord 'a' + x @@ -24,11 +24,12 @@ getPrec '*' = (5,5,6) getPrec '/' = (5,5,6) +getPrec c = error $ "Unknown operator "++[c] instance Show L where - showsPrec p (Abs s l) = showParen (p>0) $ showChar 'λ' . showVar s . showChar '.' . showsPrec 0 l - showsPrec p (AAbs f s l) = showParen (p>0) $ showChar 'Λ' . showVar f . showChar ',' . showVar s . showChar '.' . showsPrec 0 l + showsPrec p (Abs s l) = showParen (p>0) $ showChar 'λ' . showVar s . showChar '.' . shows l + showsPrec p (AAbs f s l) = showParen (p>0) $ showChar 'Λ' . showVar f . showChar ',' . showVar s . showChar '.' . shows l showsPrec p (App m n) = showParen (p>6) $ showsPrec 6 m . showChar ' ' . showsPrec 7 n - showsPrec p (Var s) = showVar s - showsPrec p (Num i) = shows i + showsPrec _ (Var s) = showVar s + showsPrec _ (Num i) = shows i showsPrec p (Op m op n) = showParen (p>prec) $ showsPrec lprec m . showChar op . showsPrec rprec n where (prec,lprec,rprec)=getPrec op @@ -36,7 +37,6 @@ showsPrec p (Shift e1 s e2) = showParen (p>0) $ showString "Shift " .showsPrec 2 e1 . showChar ' ' . showsPrec 2 s . showChar ' ' . showsPrec 2 e2 - showsPrec p Bottom = showChar '┮' - showsPrec p Unsized = showChar 'U' - showsPrec p (Aggr name e1 e2) = showParen (p>0) $ showString name .showChar ' ' . showsPrec 2 e1 . showChar ' ' . showsPrec 2 e2 + showsPrec _ Bottom = showChar '┮' + showsPrec _ Unsized = showChar 'U' t3s = Abs 1 $ Abs 0 $ App t (App t (App t x)) @@ -47,5 +47,4 @@ subs (List s f) var exp = List (subs s var exp) (subs f var exp) subs (Shift e1 e2 e3) var exp = Shift (subs e1 var exp) (subs e2 var exp) (subs e3 var exp) -subs (Aggr name e1 e2) var exp = Aggr name (subs e1 var exp) (subs e2 var exp) subs (Op x c z) var exp = Op (subs x var exp) c (subs z var exp) subs e@(Var v) var exp | v==var = exp @@ -55,7 +54,7 @@ subs x@(AAbs s f e) var exp | s==var||f==var = x | otherwise = AAbs s f (subs e var exp) -subs x@(Num _) var exp = x -subs x@Bottom var exp = x -subs x@Unsized var exp = x +subs x@(Num _) _ _ = x +subs x@Bottom _ _ = x +subs x@Unsized _ _ = x @@ -68,9 +67,9 @@ alpha e@Bottom _ _ = e alpha e@Unsized _ _ = e -alpha x@(Abs v e) from to | v==from = Abs to (alpha' e from to) - | otherwise = Abs v (alpha e from to) -alpha x@(AAbs v1 v2 e) from to | v1==from = AAbs to v2 (alpha' e from to) - | v2==from = AAbs v1 to (alpha' e from to) - | otherwise = AAbs v1 v2 (alpha e from to) +alpha (Abs v e) from to | v==from = Abs to (alpha' e from to) + | otherwise = Abs v (alpha e from to) +alpha (AAbs v1 v2 e) from to | v1==from = AAbs to v2 (alpha' e from to) + | v2==from = AAbs v1 to (alpha' e from to) + | otherwise = AAbs v1 v2 (alpha e from to) alpha' (App x z) from to = App (alpha' x from to) (alpha' z from to) @@ -80,9 +79,9 @@ alpha' e@(Var v) from to | v==from = Var to | otherwise = e -alpha' x@(Abs v e) from to | v==from = Abs to (alpha' e from to) - | otherwise = Abs v (alpha' e from to) -alpha' x@(AAbs v1 v2 e) from to | v1==from = AAbs to v2 (alpha' e from to) - | v2==from = AAbs v1 to (alpha' e from to) - | otherwise = AAbs v1 v2 (alpha' e from to) +alpha' (Abs v e) from to | v==from = Abs to (alpha' e from to) + | otherwise = Abs v (alpha' e from to) +alpha' (AAbs v1 v2 e) from to | v1==from = AAbs to v2 (alpha' e from to) + | v2==from = AAbs v1 to (alpha' e from to) + | otherwise = AAbs v1 v2 (alpha' e from to) alpha' x@(Num _) _ _ = x alpha' x@Bottom _ _ = x @@ -95,11 +94,10 @@ fv (AAbs x y e) = x `Set.delete` ( y `Set.delete` fv e) fv (List s e) = fv s `Set.union` fv e -fv (Num i) = Set.empty +fv (Num _) = Set.empty fv (Shift e1 e2 e3) = fv e1 `Set.union` fv e2 `Set.union` fv e3 -fv (Aggr _ e1 e2) = fv e1 `Set.union` fv e2 fv Unsized = Set.empty fv Bottom = Set.empty -bv (Var x) = Set.empty +bv (Var _) = Set.empty bv (App x y) = bv x `Set.union` bv y bv (Op x _ y) = bv x `Set.union` bv y @@ -108,11 +106,10 @@ bv (AAbs v1 v2 e) = v1 `Set.insert` (v2 `Set.insert` bv e) bv (Shift e1 e2 e3) = bv e1 `Set.union` bv e2 `Set.union` bv e3 -bv (Aggr _ e1 e2) = bv e1 `Set.union` bv e2 -bv (Num i) = Set.empty +bv (Num _) = Set.empty bv Unsized = Set.empty bv Bottom = Set.empty maxv (Var x) = x -maxv (Num i) = 0 +maxv (Num _) = 0 maxv Unsized = 0 maxv Bottom = 0 @@ -126,10 +123,10 @@ rsubs oexp var exp = subs renamed var exp where - dvar = (fv exp) `Set.intersection` (bv oexp) + dvar = fv exp `Set.intersection` bv oexp m = maxv exp `max` maxv oexp renames = zip (Set.toList dvar) [m+1..] renamed = foldr rename oexp renames - rename (from,to) exp = alpha oexp from to - + rename (from,to) _ = alpha oexp from to + reduce (App (Abs var exp) z) = return $ rsubs exp var z @@ -152,9 +149,4 @@ Just e' -> return $ Shift e1 e' e3 _ -> reduce e3 >>= \e' -> return $ Shift e1 e2 e' -reduce (Aggr name e1 e2) = case reduce e1 of - Just e -> return $ Aggr name e e2 - Nothing -> do - e <- reduce e2 - return $ Aggr name e1 e reduce (Op m c n) = case c of '+' | (Num i, Num j) <- (m,n) -> return $ Num $ i+j @@ -177,9 +169,9 @@ it f x = it' f (Just x) where - it' f Nothing = [] + it' _ Nothing = [] it' f (Just x) = x:it' f (f x) rchain :: L -> [L] -rchain exp = it reduce exp +rchain = it reduce pchain = putStrLn . intercalate "\n-> " . map show . rchain @@ -205,5 +197,5 @@ lfalse = Abs 0 $ Abs 1 $ Var 1 -liszero = Abs n $ App (App (Var n) (Abs x $ lfalse)) ltrue +liszero = Abs n $ App (App (Var n) (Abs x lfalse)) ltrue where (n,x) = (0,1) @@ -229,6 +221,4 @@ y = Abs 18 $ App (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) -- Λs,g.List s (λi.(λx.Λt,f.List (1+t) (Shift f (t-1) x)) U (g i)) -transposes = AAbs 18 5 $ List ( App (AAbs 15 6 $ Var 15) (Aggr "max" (Var 18) (Var 5)) )-- (App (Var 5) (Num 0)) ) - (Abs 8 $ List (Var 18) $ Abs 9 $ App (AAbs 15 6 $ App (Var 6) (Var 8)) (App (Var 5) (Var 9))) reverses = AAbs 18 5 $ List (Var 18) (Abs 8 $ App (Var 5) $ Op (Op (Var 18) '-' (Num 1)) '-' (Var 8) ) reverse' l = case l of