Changeset 14 for sizechecking/SizedExp.hs
- Timestamp:
- Nov 16, 2012, 10:38:01 AM (13 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
sizechecking/SizedExp.hs
r12 r14 81 81 where 82 82 (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) 84 84 return [([], fv)] 85 85 fv = fresh (tk q) s3 … … 90 90 concatMapM :: (a -> IO [b]) -> [a] -> IO [b] 91 91 concatMapM f l = liftM concat $ mapM f l 92 92 93 93 type SExp = ([Constraint], L) 94 94 newtype Q a = Q { unQ :: () } 95 95 instance 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]) 97 97 known l = QSynt $return [([], l)] 98 98 true = QSynt $ return [] … … 100 100 match1 (cond, ltype) = do 101 101 x <- sizeof l 102 putStrLn $ "ORIGINAL is " ++ show x103 putStrLn $ "[MATCH] ==> " ++ show ltype102 -- putStrLn $ "ORIGINAL is " ++ show x 103 -- putStrLn $ "[MATCH] ==> " ++ show ltype 104 104 let lt = rall$ App (AAbs 18 5 $ Var 18) ltype 105 putStrLn $ " --- NIL ---" ++ show lt105 -- putStrLn $ " --- NIL ---" ++ show lt 106 106 nils <- sizeof nil 107 print nils107 -- print nils 108 108 let nilc = foldr addConstraint nils $ Zero lt:cond 109 109 let tx = rall $ App (AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))) ltype 110 110 let txs = rall $App (AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)) ltype 111 putStrLn $ " --- CONS --- "++ show tx ++" <-> "++ show txs111 -- putStrLn $ " --- CONS --- "++ show tx ++" <-> "++ show txs 112 112 conss <- sizeof $ cons (QSynt$return [([], tx)]) (QSynt$return [([], txs)]) 113 print conss113 -- print conss 114 114 let consc = foldr addConstraint conss $ lt `GEC` Num 1:cond 115 print "END MATCH"116 print $ nilc ++ consc115 -- print "END MATCH" 116 -- print $ nilc ++ consc 117 117 return $ nilc ++ consc 118 118 in QSynt $ sizeof l >>= concatMapM match1 … … 139 139 in do 140 140 l3 <- sizeof sexp 141 print l142 print ll141 -- print l 142 -- print ll 143 143 return $ map (\(c,l2) -> Condition (map rr c) ll (rall l2)) l3 144 144 … … 151 151 signum = undefined 152 152 fromInteger = num 153 154 conditions :: Size Q b -> IO () 155 conditions (QProvable l x) = do 156 (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1) 157 c <- x s1 158 print c 153 159 154 160 prove :: Size Q b -> IO Bool … … 178 184 print y 179 185 return False 180
Note: See TracChangeset
for help on using the changeset viewer.