uncurrying performed in CheckGFCC

This commit is contained in:
aarne
2007-10-03 11:49:46 +00:00
parent 156d0e321e
commit 7933d12f06
3 changed files with 55 additions and 42 deletions

View File

@@ -11,81 +11,88 @@ import Control.Monad
andMapM :: Monad m => (a -> m Bool) -> [a] -> m Bool andMapM :: Monad m => (a -> m Bool) -> [a] -> m Bool
andMapM f xs = mapM f xs >>= return . and andMapM f xs = mapM f xs >>= return . and
labelBoolIO :: String -> IO Bool -> IO Bool labelBoolIO :: String -> IO (x,Bool) -> IO (x,Bool)
labelBoolIO msg iob = do labelBoolIO msg iob = do
b <- iob (x,b) <- iob
if b then return b else (putStrLn msg >> return b) if b then return (x,b) else (putStrLn msg >> return (x,b))
checkGFCC :: GFCC -> IO Bool checkGFCC :: GFCC -> IO (GFCC,Bool)
checkGFCC gfcc = andMapM (checkConcrete gfcc) $ Map.assocs $ concretes gfcc checkGFCC gfcc = do
(cs,bs) <- mapM (checkConcrete gfcc)
(Map.assocs (concretes gfcc)) >>= return . unzip
return (gfcc {concretes = Map.fromAscList cs}, and bs)
checkConcrete :: GFCC -> (CId,Map.Map CId Term) -> IO Bool checkConcrete :: GFCC -> (CId,Concr) -> IO ((CId,Concr),Bool)
checkConcrete gfcc (lang,cnc) = checkConcrete gfcc (lang,cnc) =
labelBoolIO ("happened in language " ++ printTree lang) $ labelBoolIO ("happened in language " ++ printTree lang) $ do
andMapM (checkLin gfcc lang) $ linRules cnc (rs,bs) <- mapM (checkLin gfcc lang) (linRules cnc) >>= return . unzip
return ((lang,Map.fromAscList rs),and bs)
checkLin :: GFCC -> CId -> (CId,Term) -> IO Bool checkLin :: GFCC -> CId -> (CId,Term) -> IO ((CId,Term),Bool)
checkLin gfcc lang (f,t) = checkLin gfcc lang (f,t) =
labelBoolIO ("happened in function " ++ printTree f) $ labelBoolIO ("happened in function " ++ printTree f) $ do
checkTerm (lintype gfcc lang f) $ inline gfcc lang t (t',b) <- checkTerm (lintype gfcc lang f) t --- $ inline gfcc lang t
return ((f,t'),b)
inferTerm :: [Tpe] -> Term -> Err Tpe inferTerm :: [Tpe] -> Term -> Err (Term,Tpe)
inferTerm args trm = case trm of inferTerm args trm = case trm of
K _ -> return str K _ -> returnt str
C i -> return $ ints i C i -> returnt $ ints i
V i -> do V i -> do
testErr (i < length args) ("too large index " ++ show i) testErr (i < length args) ("too large index " ++ show i)
return $ args !! i returnt $ args !! i
S ts -> do S ts -> do
tys <- mapM infer ts (ts',tys) <- mapM infer ts >>= return . unzip
let tys' = filter (/=str) tys let tys' = filter (/=str) tys
testErr (null tys') testErr (null tys')
("expected Str in " ++ prt trm ++ " not " ++ unwords (map prt tys')) ("expected Str in " ++ prt trm ++ " not " ++ unwords (map prt tys'))
return str return (S ts',str)
R ts -> do R ts -> do
tys <- mapM infer ts (ts',tys) <- mapM infer ts >>= return . unzip
return $ tuple tys return $ (R ts',tuple tys)
P t u -> do P t u -> do
tt <- infer t (t',tt) <- infer t
tu <- infer u (u',tu) <- infer u
case tt of case tt of
R tys -> case tu of R tys -> case tu of
R [v] -> infer $ P t v R vs -> infer $ foldl P t' [P u' (C i) | i <- [0 .. length vs - 1]]
R (v:vs) -> infer $ P (head tys) (R vs) ----- --- R [v] -> infer $ P t v
--- R (v:vs) -> infer $ P (head tys) (R vs)
C i -> do C i -> do
testErr (i < length tys) testErr (i < length tys)
("required more than " ++ show i ++ " fields in " ++ prt (R tys)) ("required more than " ++ show i ++ " fields in " ++ prt (R tys))
(return $ tys !! i) -- record: index must be known (returnt $ tys !! i) -- record: index must be known
_ -> do _ -> do
let typ = head tys let typ = head tys
testErr (all (==typ) tys) ("different types in table " ++ prt trm) testErr (all (==typ) tys) ("different types in table " ++ prt trm)
return typ -- table: must be same returnt typ -- table: must be same
_ -> Bad $ "projection from " ++ prt t ++ " : " ++ prt tt _ -> Bad $ "projection from " ++ prt t ++ " : " ++ prt tt
FV [] -> return str ---- FV [] -> returnt str ----
FV (t:ts) -> do FV (t:ts) -> do
ty <- infer t (t',ty) <- infer t
tys <- mapM infer ts (ts',tys) <- mapM infer ts >>= return . unzip
testErr (all (==ty) tys) ("different types in variants " ++ prt trm) testErr (all (==ty) tys) ("different types in variants " ++ prt trm)
return ty return (FV (t':ts'),ty)
W s r -> infer r W s r -> infer r
_ -> Bad ("no type inference for " ++ prt trm) _ -> Bad ("no type inference for " ++ prt trm)
where where
returnt ty = return (trm,ty)
infer = inferTerm args infer = inferTerm args
prt = printTree prt = printTree
checkTerm :: LinType -> Term -> IO Bool checkTerm :: LinType -> Term -> IO (Term,Bool)
checkTerm (args,val) trm = case inferTerm args trm of checkTerm (args,val) trm = case inferTerm args trm of
Ok ty -> if eqType ty val Ok (t,ty) -> if eqType ty val
then return True then return (t,True)
else do else do
putStrLn $ "term: " ++ printTree trm ++ putStrLn $ "term: " ++ printTree trm ++
"\nexpected type: " ++ printTree val ++ "\nexpected type: " ++ printTree val ++
"\ninferred type: " ++ printTree ty "\ninferred type: " ++ printTree ty
return False return (trm,False)
Bad s -> do Bad s -> do
putStrLn s putStrLn s
return False return (trm,False)
eqType :: Tpe -> Tpe -> Bool eqType :: Tpe -> Tpe -> Bool
eqType inf exp = case (inf,exp) of eqType inf exp = case (inf,exp) of

View File

@@ -139,3 +139,10 @@ mkGFCC (Grm (Hdr a cs) ab@(Abs funs) ccs) = GFCC {
where where
mkCnc lins = fromList [(fun,lin) | Lin fun lin <- lins] ---- Asc mkCnc lins = fromList [(fun,lin) | Lin fun lin <- lins] ---- Asc
printGFCC :: GFCC -> String
printGFCC gfcc = printTree $ Grm
(Hdr (absname gfcc) (cncnames gfcc))
(Abs [Fun f ty (Tr (AC f) []) | (f,ty) <- assocs (funs (abstract gfcc))])
[Cnc lang [Lin f t | (f,t) <- assocs lins] |
(lang,lins) <- assocs (concretes gfcc)]

View File

@@ -20,19 +20,18 @@ main = do
_ | oElem (iOpt "-make") opts -> do _ | oElem (iOpt "-make") opts -> do
gr <- batchCompile opts fs gr <- batchCompile opts fs
let name = justModuleName (last fs) let name = justModuleName (last fs)
let (abs,gc) = mkCanon2gfcc opts name gr let (abs,gc0) = mkCanon2gfcc opts name gr
gc <- check gc0
if oElem (iOpt "check") opts then (check gc) else return ()
let target = abs ++ ".gfcc" let target = abs ++ ".gfcc"
writeFile target (printTree gc) writeFile target (printGFCC gc)
putStrLn $ "wrote file " ++ target putStrLn $ "wrote file " ++ target
_ -> do _ -> do
mapM_ (batchCompile opts) (map return fs) mapM_ (batchCompile opts) (map return fs)
putStrLn "Done." putStrLn "Done."
check gc = do check gc0 = do
let gfcc = mkGFCC gc let gfcc = mkGFCC gc0
b <- checkGFCC gfcc (gc,b) <- checkGFCC gfcc
putStrLn $ if b then "OK" else "Corrupted GFCC" putStrLn $ if b then "OK" else "Corrupted GFCC"
return gc