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
128
129
130
|
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
R [v] -> infer $ P t v
R (v:vs) -> infer $ P (head tys) (R vs) -----
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)
|
