Changeset 12 for sizechecking/SizedExp.hs

Timestamp:

Nov 15, 2012, 12:44:36 AM (13 years ago)

Author:

gobi

Message:

code cleanup

File:

• sizechecking/SizedExp.hs (modified) (5 diffs)

sizechecking/SizedExp.hs

@@ -11 +11 @@
 import Constraints 
 import Data.Supply
-
+import Control.Arrow
+import Control.Monad
 
 class TS b => (Unify se a b)  where
@@ -19 +20 @@
 
 instance (SizedExp se, Unify se a b, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1->a) (c2->b) where
-    unify f g x = f undefined x
+    unify f g = f undefined
 
 instance (SizedExp se, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1) c2 where
-    unify f g x = g undefined x
+    unify f g = g undefined
 
 class SizedExp (se :: * -> *) where
@@ -77 +78 @@
     (s1, s2, s3) = split3 supply
     freshvars' :: (Unify Q a b) => (a -> (Size Q b, L -> L)) -> (Size Q c -> a) -> (Size Q (c -> b), L -> L)
-    freshvars' u exp = (QSynt $ sizeof $ x, \l -> f $ App l fv)
+    freshvars' u exp = (QSynt $ sizeof x, \l -> f $ App l fv)
         where
         (x, f) = u $ exp $ QSynt $ do 
-            putStrLn $ "[Bind] var="++(show fv)++" of type "++(show $ tk q)
+            putStrLn $ "[Bind] var="++ show fv ++" of type "++ show (tk q)
             return [([], fv)]
         fv = fresh (tk q) s3
 
 addConstraint :: Constraint -> [SExp] -> [SExp]
-addConstraint nc = map (\(c,l) -> (nc:c, l))
+addConstraint nc = map (first ((:) nc))
 
 concatMapM :: (a -> IO [b]) -> [a] -> IO [b]
-concatMapM f l = mapM f l >>= return.concat
+concatMapM f l = liftM concat $ mapM f l
     
 type SExp = ([Constraint], L)
@@ -99 +100 @@
             match1 (cond, ltype) = do
                     x <- sizeof l
-                    putStrLn $ "ORIGINAL is " ++ (show x)
-                    putStrLn $ "[MATCH] ==> " ++ (show $ ltype)
+                    putStrLn $ "ORIGINAL is " ++ show x
+                    putStrLn $ "[MATCH] ==> " ++ show ltype
                     let lt = rall$  App (AAbs 18 5 $ Var 18) ltype
-                    putStrLn $ " --- NIL  ---" ++ (show lt)
+                    putStrLn $ " --- NIL  ---" ++ show lt
                     nils <- sizeof nil
-                    putStrLn $ show nils
+                    print nils
                     let nilc = foldr addConstraint nils $ Zero lt:cond
                     let tx = rall $ App (AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))) ltype
                     let txs = rall $App (AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)) ltype
-                    putStrLn $ " --- CONS --- "++(show tx)++" <-> "++(show txs)
+                    putStrLn $ " --- CONS --- "++ show tx ++" <-> "++ show txs
                     conss <- sizeof $ cons (QSynt$return [([], tx)]) (QSynt$return [([], txs)])
                     print conss
@@ -151 +152 @@
     fromInteger = num
 
-prove :: Size Q b -> IO (Bool)
+prove :: Size Q b -> IO Bool
 prove (QProvable l x) = do
-    (s1,s2,s3) <- newSupply 30 (+1) >>= return.split3
+    (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1)
     c <- x s1
     putStrLn ""