Changeset 6 for sizechecking


Ignore:
Timestamp:
Nov 12, 2012, 4:06:50 AM (13 years ago)
Author:
gobi
Message:

hlint

Location:
sizechecking
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • sizechecking/Constraints.hs

    r5 r6  
    1212import Data.SBV ( (.==), (.<), (.>=)) 
    1313import Control.Monad 
    14 import Data.IORef 
     14import Data.IORef() 
    1515import Data.Supply as S 
    1616 
    1717asType :: a -> a -> a 
    18 asType a b = a 
     18asType a _ = a 
    1919 
    2020data D = D { var::Int, cond::[Condition] }  
    … …  
    3636 
    3737appall :: Int -> [L] -> L 
    38 appall var l = foldl (App) (Var $ var) $  l 
     38appall var = foldl App (Var var) 
    3939 
    4040 
    … …  
    7676            [] -> (Num 0, b) 
    7777            _  -> (expr, b) 
    78         (_, _)   -> error $ "Expression in condition" ++ (show c) 
     78        (_, _)   -> error $ "Expression in condition" ++ show c 
    7979    where 
    8080    nonzero = List.sortBy (Ord.comparing snd) $ filter ((/=0).fst) a 
    … …  
    111111norm (AAbs a b e)  = ([], 0, [AAbs a b (normalize e)], []) 
    112112norm (Shift a b c) = ([], 0, [Shift (normalize a) (normalize b) (normalize c)], []) 
    113 norm (Aggr a b c)  = ([], 0, [Aggr a (normalize b) (normalize c)], []) 
    114113norm (Unsized)     = ([], 0, [Unsized], []) 
    115114norm (Bottom)      = ([], 0, [Bottom], []) 
    … …  
    159158        l1 <- checkCond1 v1 (Condition ((h `LTC` f):d) e' x) 
    160159        l2 <- checkCond1 v2 (Condition ((h `GEC` f):d) g' x) 
    161         putStrLn $ " -> " ++ (show l1) 
    162         putStrLn $ " -> " ++ (show l2) 
     160        putStrLn $ " -> " ++ show l1 
     161        putStrLn $ " -> " ++ show l2 
    163162        return $ l1 ++ l2 
    164     checkCond1 v z@(Condition d (App (Var a) x) (App (Var b) y)) | a==b = do 
     163    checkCond1 v z@(Condition d (App (Var a) x) (App (Var b) y)) | a==b = 
    165164        checkCond1 v (Condition d x y) 
    166     checkCond1 v p@(Condition d x z@(App (Shift e f g) h)) = do 
     165    checkCond1 v p@(Condition d x z@(App (Shift e f g) h)) = 
    167166        checkCond1 v (Condition d z x) 
    168     checkCond1 v z@(Condition d a b) = return $ [Condition dd (normalize a) (normalize b)] 
     167    checkCond1 v z@(Condition d a b) = return [Condition dd (normalize a) (normalize b)] 
    169168        where 
    170169        dd = normalizecs d 
    … …  
    174173subst ndl hst (AAbs a b e)  = AAbs a b (subst ndl hst e) 
    175174subst ndl hst (Shift a b c) = Shift (subst ndl hst a) (subst ndl hst b) (subst ndl hst c) 
    176 subst ndl hst (Aggr a b c)  = Aggr a (subst ndl hst b) (subst ndl hst c) 
    177175subst ndl hst (Unsized)     = Unsized 
    178176subst ndl hst (Bottom)      = Bottom 
    … …  
    201199solve l supply = do 
    202200    ll <- forM (zip l $ split supply) (\(c,s) -> do 
    203         putStrLn $ "\nSOLVING "++(show c) 
     201        putStrLn $ "\nSOLVING " ++ show c  
    204202        solve1 s c 
    205203        ) 
    … …  
    227225 
    228226    checkConds [] = False 
    229     checkConds ((LTC a b):xs) | (elem (GEC a b) xs)            = True 
    230     checkConds ((GEC a b):xs) | (elem (LTC a b) xs)            = True 
    231     checkConds ((LTC a (Num b)):xs) | b<=0 && elem (Zero a) xs = True 
    232     checkConds ((GEC a (Num b)):xs) | b>0  && elem (Zero a) xs = True 
     227    checkConds (LTC a b : xs) | GEC a b `elem` xs            = True 
     228    checkConds (GEC a b : xs) | LTC a b `elem` xs            = True 
     229    checkConds (LTC a (Num b) : xs) | b<=0 && elem (Zero a) xs = True 
     230    checkConds (GEC a (Num b) : xs) | b>0  && elem (Zero a) xs = True 
    233231    checkConds (_:xs) = checkConds xs 
    234232 
    … …  
    259257            return [] 
    260258        | a==b = do 
    261             putStrLn $ "Equals" 
     259            putStrLn "Equals" 
    262260            return [] 
    263261        | Just (var, nl) <- searchzero d = do 
    264             let x = (Condition (Prelude.map (normalizec.substc var (Num 0)) nl) 
     262            let x = Condition (Prelude.map (normalizec.substc var (Num 0)) nl) 
    265263                        (normalize$subst var (Num 0) a) 
    266264                        (normalize$subst var (Num 0) b) 
    267                     ) 
    268             putStrLn $ (show $ Var var) ++" is zero:\n" ++ (show x) 
     265 
     266            putStrLn $ show (Var var) ++ " is zero:\n" ++ show x 
    269267            solve1 supp x  
    270268        | Just (var, exp, nl) <- searcheq d [] = do 
    271             putStrLn $ "Found equation "++(show $ Var var) ++ " = "++(show exp) 
    272             let x = (Condition (Prelude.map (normalizec.substc var exp) nl ) 
     269            putStrLn $ "Found equation " ++ show (Var var) ++ " = " ++ show exp 
     270            let x = Condition (Prelude.map (normalizec.substc var exp) nl ) 
    273271                        (normalize$subst var exp a) 
    274272                        (normalize$subst var exp b) 
    275                     ) 
    276             putStrLn $ "New equations:\n" ++ (show x) 
     273            putStrLn $ "New equations:\n" ++ show x 
    277274            solve1 supp x  
    278275        | App p q <- a, App r s <- b = do 
    279             putStrLn $ "Branching!" 
     276            putStrLn "Branching!" 
    280277            nc <- checkCond supp [Condition d p r, Condition d q s]  
    281278            solve nc supp 
    … …  
    291288--        | Abs  _ _   <- a, AAbs _ _ _ <- b = applyList a b d supp 
    292289--        | AAbs _ _ _ <- a, AAbs _ _ _ <- b = applyList a b d supp 
    293         | Just dd <- reorder d = do  
    294             putStrLn $ "Reorder " ++ (show dd) 
     290        | Just dd <- reorder d = do 
     291            putStrLn $ "Reorder " ++ show dd 
    295292            solve1 supp $ Condition dd a b 
    296293        | otherwise = do 
    … …  
    309306compiletosolver :: L -> L -> [Constraint] -> SBV.Symbolic SBV.SBool 
    310307compiletosolver a b d = do 
    311     let fvs = Set.toList $ Set.unions $ (fv a):(fv b):(map fvc d) 
    312     (vars::[SBV.SInteger]) <- mapM SBV.free $ map (flip showVar "") fvs 
     308    let fvs = Set.toList $ Set.unions $ fv a : fv b : map fvc d 
     309    (vars::[SBV.SInteger]) <- mapM (SBV.free . flip showVar "") fvs 
    313310    let varmap = Map.fromList $ zip fvs vars 
    314     mapM SBV.constrain $ map (compilec varmap) d 
    315     return $ (compilel varmap a) .== (compilel varmap b) 
     311    mapM_ (SBV.constrain . compilec varmap) d 
     312    return $ compilel varmap a .== compilel varmap b 
    316313 
    317314compilec v (Zero a)  = compilel v a .== (0::SBV.SInteger) 
    … …  
    329326compilel v (Var a) | Just x<-Map.lookup a v = x 
    330327compilel v (Num a) = SBV.literal $ fromIntegral a 
    331 compilel v a = error $ "Cannot compile "++(show a) 
     328compilel v a = error $ "Cannot compile " ++ show a 

  • sizechecking/Lambda.hs

    r5 r6  
    1212 
    1313data L = Abs Int L | App L L | Var Int | Num Int | Op L Char L | List L L | AAbs Int Int L 
    14     | Shift L L L | Unsized | Bottom | Aggr String L L 
     14    | Shift L L L | Unsized | Bottom  
    1515    deriving Eq 
    1616 
    1717showVar x = if x>28  
    18     then showVar (x `div` 29) . (showChar $ chr $ ord 'a' + (x `mod` 29)) 
     18    then showVar (x `div` 29) . showChar (chr $ ord 'a' + (x `mod` 29)) 
    1919    else showChar $ chr $ ord 'a' + x 
    2020 
    … …  
    2424getPrec '*' = (5,5,6) 
    2525getPrec '/' = (5,5,6) 
     26getPrec c   = error $ "Unknown operator "++[c] 
    2627 
    2728instance Show L where 
    28     showsPrec p (Abs s l) = showParen (p>0) $ showChar 'λ' . showVar s . showChar '.' . showsPrec 0 l 
    29     showsPrec p (AAbs f s l) = showParen (p>0) $ showChar 'Λ' . showVar f . showChar ',' . showVar s . showChar '.' . showsPrec 0 l 
     29    showsPrec p (Abs s l) = showParen (p>0) $ showChar 'λ' . showVar s . showChar '.' . shows l 
     30    showsPrec p (AAbs f s l) = showParen (p>0) $ showChar 'Λ' . showVar f . showChar ',' . showVar s . showChar '.' . shows l 
    3031    showsPrec p (App m n) = showParen (p>6) $ showsPrec 6 m . showChar ' ' . showsPrec 7 n 
    31     showsPrec p (Var s) = showVar s 
    32     showsPrec p (Num i) = shows i 
     32    showsPrec _ (Var s) = showVar s 
     33    showsPrec _ (Num i) = shows i 
    3334    showsPrec p (Op m op n) = showParen (p>prec) $ showsPrec lprec m . showChar op . showsPrec rprec n 
    3435        where (prec,lprec,rprec)=getPrec op 
    … …  
    3637    showsPrec p (Shift e1 s e2) = showParen (p>0) $ showString "Shift " .showsPrec 2 e1 . 
    3738        showChar ' ' . showsPrec 2 s . showChar ' ' . showsPrec 2 e2 
    38     showsPrec p Bottom = showChar '┮' 
    39     showsPrec p Unsized = showChar 'U' 
    40     showsPrec p (Aggr name e1 e2) = showParen (p>0) $ showString name .showChar ' ' . showsPrec 2 e1 . showChar ' ' . showsPrec 2 e2 
     39    showsPrec _ Bottom = showChar '┮' 
     40    showsPrec _ Unsized = showChar 'U' 
    4141 
    4242t3s = Abs 1 $ Abs 0 $ App t (App t (App t x)) 
    … …  
    4747subs (List s f)  var exp = List (subs s var exp) (subs f var exp) 
    4848subs (Shift e1 e2 e3) var exp = Shift (subs e1 var exp) (subs e2 var exp) (subs e3 var exp) 
    49 subs (Aggr name e1 e2) var exp = Aggr name (subs e1 var exp) (subs e2 var exp) 
    5049subs (Op x c z)  var exp = Op (subs x var exp) c (subs z var exp) 
    5150subs e@(Var v)   var exp | v==var    = exp 
    … …  
    5554subs x@(AAbs s f e) var exp | s==var||f==var = x 
    5655                            | otherwise = AAbs s f (subs e var exp) 
    57 subs x@(Num _)   var exp = x 
    58 subs x@Bottom   var exp = x 
    59 subs x@Unsized   var exp = x 
     56subs x@(Num _)   _ _ = x 
     57subs x@Bottom    _ _ = x 
     58subs x@Unsized   _ _ = x 
    6059 
    6160 
    … …  
    6867alpha e@Bottom   _    _  = e 
    6968alpha e@Unsized   _    _  = e 
    70 alpha x@(Abs v e) from to | v==from   = Abs to (alpha' e from to) 
    71                           | otherwise = Abs v (alpha e from to) 
    72 alpha x@(AAbs v1 v2 e) from to | v1==from  = AAbs to v2 (alpha' e from to) 
    73                                | v2==from  = AAbs v1 to (alpha' e from to) 
    74                                | otherwise = AAbs v1 v2 (alpha e from to) 
     69alpha (Abs v e) from to | v==from   = Abs to (alpha' e from to) 
     70                        | otherwise = Abs v (alpha e from to) 
     71alpha (AAbs v1 v2 e) from to | v1==from  = AAbs to v2 (alpha' e from to) 
     72                             | v2==from  = AAbs v1 to (alpha' e from to) 
     73                             | otherwise = AAbs v1 v2 (alpha e from to) 
    7574 
    7675alpha' (App x z)   from to = App (alpha' x from to) (alpha' z from to) 
    … …  
    8079alpha' e@(Var v)   from to | v==from   = Var to 
    8180                           | otherwise = e 
    82 alpha' x@(Abs v e) from to | v==from   = Abs to (alpha' e from to) 
    83                            | otherwise = Abs v (alpha' e from to) 
    84 alpha' x@(AAbs v1 v2 e) from to | v1==from  = AAbs to v2 (alpha' e from to) 
    85                                 | v2==from  = AAbs v1 to (alpha' e from to) 
    86                                 | otherwise = AAbs v1 v2 (alpha' e from to) 
     81alpha' (Abs v e) from to | v==from   = Abs to (alpha' e from to) 
     82                         | otherwise = Abs v (alpha' e from to) 
     83alpha' (AAbs v1 v2 e) from to | v1==from  = AAbs to v2 (alpha' e from to) 
     84                              | v2==from  = AAbs v1 to (alpha' e from to) 
     85                              | otherwise = AAbs v1 v2 (alpha' e from to) 
    8786alpha' x@(Num _)   _    _  = x 
    8887alpha' x@Bottom   _    _  = x 
    … …  
    9594fv (AAbs x y e) = x `Set.delete` ( y `Set.delete` fv e) 
    9695fv (List s e) = fv s `Set.union` fv e 
    97 fv (Num i) = Set.empty 
     96fv (Num _) = Set.empty 
    9897fv (Shift e1 e2 e3) = fv e1 `Set.union` fv e2 `Set.union` fv e3 
    99 fv (Aggr _ e1 e2) = fv e1 `Set.union` fv e2  
    10098fv Unsized = Set.empty 
    10199fv Bottom = Set.empty 
    102100 
    103 bv (Var x) = Set.empty 
     101bv (Var _) = Set.empty 
    104102bv (App x y) = bv x `Set.union` bv y 
    105103bv (Op x _ y) = bv x `Set.union` bv y 
    … …  
    108106bv (AAbs v1 v2 e) = v1 `Set.insert` (v2 `Set.insert` bv e) 
    109107bv (Shift e1 e2 e3) = bv e1 `Set.union` bv e2 `Set.union` bv e3 
    110 bv (Aggr _ e1 e2) = bv e1 `Set.union` bv e2  
    111 bv (Num i)   = Set.empty 
     108bv (Num _)   = Set.empty 
    112109bv Unsized = Set.empty 
    113110bv Bottom = Set.empty 
    114111 
    115112maxv (Var x)   = x 
    116 maxv (Num i)   = 0 
     113maxv (Num _)   = 0 
    117114maxv Unsized = 0 
    118115maxv Bottom = 0 
    … …  
    126123rsubs oexp var exp = subs renamed var exp 
    127124    where 
    128     dvar = (fv exp) `Set.intersection` (bv oexp) 
     125    dvar = fv exp `Set.intersection` bv oexp 
    129126    m = maxv exp `max` maxv oexp 
    130127    renames = zip (Set.toList dvar) [m+1..] 
    131128    renamed = foldr rename oexp renames 
    132     rename (from,to) exp = alpha oexp from to 
    133      
     129    rename (from,to) _ = alpha oexp from to 
     130 
    134131 
    135132reduce (App (Abs var exp) z) = return $ rsubs exp var z 
    … …  
    152149            Just e' -> return $ Shift e1 e' e3 
    153150            _       -> reduce e3 >>= \e' -> return $ Shift e1 e2 e' 
    154 reduce (Aggr name e1 e2) = case reduce e1 of 
    155         Just e -> return $ Aggr name e e2 
    156         Nothing -> do 
    157             e <- reduce e2 
    158             return $ Aggr name e1 e 
    159151reduce (Op m c n) = case c of 
    160152    '+' | (Num i, Num j) <- (m,n) -> return $ Num $ i+j 
    … …  
    177169it f x = it' f (Just x) 
    178170    where 
    179     it' f Nothing  = [] 
     171    it' _ Nothing  = [] 
    180172    it' f (Just x) = x:it' f (f x) 
    181173 
    182174rchain :: L -> [L] 
    183 rchain exp = it reduce exp 
     175rchain = it reduce 
    184176 
    185177pchain = putStrLn . intercalate "\n-> " . map show . rchain 
    … …  
    205197lfalse = Abs 0 $ Abs 1 $ Var 1 
    206198 
    207 liszero = Abs n $ App (App (Var n) (Abs x $ lfalse)) ltrue 
     199liszero = Abs n $ App (App (Var n) (Abs x lfalse)) ltrue 
    208200    where (n,x) = (0,1) 
    209201 
    … …  
    229221y = Abs 18 $ App (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) 
    230222-- Λs,g.List s (λi.(λx.Λt,f.List (1+t) (Shift f (t-1) x)) U (g i)) 
    231 transposes = AAbs 18 5 $ List ( App (AAbs 15 6 $ Var 15) (Aggr "max" (Var 18) (Var 5)) )-- (App (Var 5) (Num 0)) )  
    232     (Abs 8 $ List (Var 18) $ Abs 9 $ App (AAbs 15 6 $ App (Var 6) (Var 8)) (App (Var 5) (Var 9))) 
    233223reverses = AAbs 18 5 $ List (Var 18) (Abs 8 $ App (Var 5) $ Op (Op (Var 18) '-' (Num 1)) '-' (Var 8) ) 
    234224reverse' l = case l of 
Note: See TracChangeset for help on using the changeset viewer.