1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
module GF.Canon.GFCC.CheckGFCC where
import GF.Canon.GFCC.DataGFCC
import GF.Canon.GFCC.AbsGFCC
import GF.Canon.GFCC.PrintGFCC
import GF.Canon.GFCC.ErrM
import qualified Data.Map as Map
import Control.Monad
andMapM :: Monad m => (a -> m Bool) -> [a] -> m Bool
andMapM f xs = mapM f xs >>= return . and
labelBoolIO :: String -> IO Bool -> IO Bool
labelBoolIO msg iob = do
b <- iob
if b then return b else (putStrLn msg >> return b)
checkGFCC :: GFCC -> IO Bool
checkGFCC gfcc = andMapM (checkConcrete gfcc) $ Map.assocs $ concretes gfcc
checkConcrete :: GFCC -> (CId,Map.Map CId Term) -> IO Bool
checkConcrete gfcc (lang,cnc) =
labelBoolIO ("happened in language " ++ printTree lang) $
andMapM (checkLin gfcc lang) $ linRules cnc
checkLin :: GFCC -> CId -> (CId,Term) -> IO Bool
checkLin gfcc lang (f,t) =
labelBoolIO ("happened in function " ++ printTree f) $
checkTerm (lintype gfcc lang f) $ inline gfcc lang t
inferTerm :: [Tpe] -> Term -> Maybe Tpe
inferTerm args trm = case trm of
K _ -> return str
C i -> return $ ints i
V i -> if i < length args
then (return $ args !! i)
else error ("index " ++ show i)
S ts -> do
tys <- mapM infer ts
if all (==str) tys
then return str
else error ("only strings expected in: " ++ printTree trm
++ " instead of " ++ unwords (map printTree tys)
)
R ts -> do
tys <- mapM infer ts
return $ tuple tys
P t u -> do
R tys <- infer t
case u of
C i -> if (i < length tys)
then (return $ tys !! i) -- record: index must be known
else error ("too few fields in " ++ printTree (R tys))
_ -> if all (==head tys) tys -- table: must be same
then return (head tys)
else error ("projection " ++ printTree trm)
FV ts -> return $ head ts ---- empty variants; check equality
W s r -> infer r
_ -> error ("no type inference for " ++ printTree trm)
where
infer = inferTerm args
checkTerm :: LinType -> Term -> IO Bool
checkTerm (args,val) trm = case inferTerm args trm of
Just ty -> if eqType ty val then return True else do
putStrLn $ "term: " ++ printTree trm ++
"\nexpected type: " ++ printTree val ++
"\ninferred type: " ++ printTree ty
return False
_ -> do
putStrLn $ "cannot infer type of " ++ printTree trm
return False
eqType :: Tpe -> Tpe -> Bool
eqType inf exp = case (inf,exp) of
(C k, C n) -> k <= n -- only run-time corr.
(R rs,R ts) -> length rs == length ts && and [eqType r t | (r,t) <- zip rs ts]
_ -> inf == exp
-- should be in a generic module, but not in the run-time DataGFCC
type Tpe = Term
type LinType = ([Tpe],Tpe)
tuple :: [Tpe] -> Tpe
tuple = R
ints :: Int -> Tpe
ints = C
str :: Tpe
str = S []
lintype :: GFCC -> CId -> CId -> LinType
lintype gfcc lang fun = case lookType gfcc fun of
Typ cs c -> (map linc cs, linc c)
where
linc = lookLincat gfcc lang
lookLincat :: GFCC -> CId -> CId -> Term
lookLincat gfcc lang (CId cat) = lookLin gfcc lang (CId ("__" ++ cat))
linRules :: Map.Map CId Term -> [(CId,Term)]
linRules cnc = [(f,t) | (f@(CId (c:_)),t) <- Map.assocs cnc, c /= '_'] ----
inline :: GFCC -> CId -> Term -> Term
inline gfcc lang t = case t of
F c -> inl $ look c
_ -> composSafeOp inl t
where
inl = inline gfcc lang
look = lookLin gfcc lang
composOp :: Monad m => (Term -> m Term) -> Term -> m Term
composOp f trm = case trm of
R ts -> liftM R $ mapM comp ts
S ts -> liftM S $ mapM comp ts
FV ts -> liftM FV $ mapM comp ts
P t u -> liftM2 P (comp t) (comp u)
W s t -> liftM (W s) $ comp t
_ -> return trm
where
comp = composOp f
composSafeOp :: (Term -> Term) -> Term -> Term
composSafeOp f = maybe undefined id . composOp (return . f)
|
