Ignore:
Timestamp:
Nov 16, 2012, 10:38:01 AM (13 years ago)
Author:
gobi
Message:

removing some debug

File:
1 edited

Legend:

Unmodified
Added
Removed
  • sizechecking/SizedExp.hs

    r12 r14  
    8181        where 
    8282        (x, f) = u $ exp $ QSynt $ do  
    83             putStrLn $ "[Bind] var="++ show fv ++" of type "++ show (tk q) 
     83--            putStrLn $ "[Bind] var="++ show fv ++" of type "++ show (tk q) 
    8484            return [([], fv)] 
    8585        fv = fresh (tk q) s3 
     
    9090concatMapM :: (a -> IO [b]) -> [a] -> IO [b] 
    9191concatMapM f l = liftM concat $ mapM f l 
    92      
     92 
    9393type SExp = ([Constraint], L) 
    9494newtype Q a = Q { unQ :: () } 
    9595instance SizedExp Q where 
    96     data Size Q a = QSynt (IO [SExp]) | QProvable L (Supply Int -> IO [Condition])  
     96    data Size Q a = QSynt (IO [SExp]) | QProvable L (Supply Int -> IO [Condition]) 
    9797    known l = QSynt $return [([], l)] 
    9898    true = QSynt $ return [] 
     
    100100            match1 (cond, ltype) = do 
    101101                    x <- sizeof l 
    102                     putStrLn $ "ORIGINAL is " ++ show x 
    103                     putStrLn $ "[MATCH] ==> " ++ show ltype 
     102--                    putStrLn $ "ORIGINAL is " ++ show x 
     103--                    putStrLn $ "[MATCH] ==> " ++ show ltype 
    104104                    let lt = rall$  App (AAbs 18 5 $ Var 18) ltype 
    105                     putStrLn $ " --- NIL  ---" ++ show lt 
     105--                    putStrLn $ " --- NIL  ---" ++ show lt 
    106106                    nils <- sizeof nil 
    107                     print nils 
     107--                    print nils 
    108108                    let nilc = foldr addConstraint nils $ Zero lt:cond 
    109109                    let tx = rall $ App (AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))) ltype 
    110110                    let txs = rall $App (AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)) ltype 
    111                     putStrLn $ " --- CONS --- "++ show tx ++" <-> "++ show txs 
     111--                    putStrLn $ " --- CONS --- "++ show tx ++" <-> "++ show txs 
    112112                    conss <- sizeof $ cons (QSynt$return [([], tx)]) (QSynt$return [([], txs)]) 
    113                     print conss 
     113--                    print conss 
    114114                    let consc = foldr addConstraint conss $ lt `GEC` Num 1:cond 
    115                     print "END MATCH" 
    116                     print  $ nilc ++ consc 
     115--                    print "END MATCH" 
     116--                    print  $ nilc ++ consc 
    117117                    return $ nilc ++ consc 
    118118        in QSynt $ sizeof l >>= concatMapM match1  
     
    139139            in do  
    140140                l3 <- sizeof sexp  
    141                 print l 
    142                 print ll 
     141--                print l 
     142--                print ll 
    143143                return $ map (\(c,l2) -> Condition (map rr c) ll (rall l2)) l3 
    144144 
     
    151151    signum = undefined 
    152152    fromInteger = num 
     153 
     154conditions :: Size Q b -> IO () 
     155conditions (QProvable l x) = do 
     156    (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1) 
     157    c <- x s1 
     158    print c 
    153159 
    154160prove :: Size Q b -> IO Bool 
     
    178184        print y 
    179185        return False 
    180  
Note: See TracChangeset for help on using the changeset viewer.