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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
|
module PGF.Check (checkPGF,checkLin) where
import PGF.CId
import PGF.Data
import PGF.Macros
import GF.Data.ErrM
import qualified Data.Map as Map
import Control.Monad
import Data.Maybe(fromMaybe)
import Debug.Trace
checkPGF :: PGF -> Err (PGF,Bool)
checkPGF pgf = return (pgf,True) {- do
(cs,bs) <- mapM (checkConcrete pgf)
(Map.assocs (concretes pgf)) >>= return . unzip
return (pgf {concretes = Map.fromAscList cs}, and bs)
-}
-- errors are non-fatal; replace with 'fail' to change this
msg s = trace s (return ())
andMapM :: Monad m => (a -> m Bool) -> [a] -> m Bool
andMapM f xs = mapM f xs >>= return . and
labelBoolErr :: String -> Err (x,Bool) -> Err (x,Bool)
labelBoolErr ms iob = do
(x,b) <- iob
if b then return (x,b) else (msg ms >> return (x,b))
{-
checkConcrete :: PGF -> (CId,Concr) -> Err ((CId,Concr),Bool)
checkConcrete pgf (lang,cnc) =
labelBoolErr ("happened in language " ++ showCId lang) $ do
(rs,bs) <- mapM checkl (Map.assocs (lins cnc)) >>= return . unzip
return ((lang,cnc{lins = Map.fromAscList rs}),and bs)
where
checkl = checkLin pgf lang
-}
type PGFSig = (Map.Map CId (Type,Int,[Equation]),Map.Map CId Term,Map.Map CId Term)
checkLin :: PGFSig -> CId -> (CId,Term) -> Err ((CId,Term),Bool)
checkLin pgf lang (f,t) =
labelBoolErr ("happened in function " ++ showCId f) $ do
(t',b) <- checkTerm (lintype pgf lang f) t --- $ inline pgf lang t
return ((f,t'),b)
inferTerm :: [CType] -> Term -> Err (Term,CType)
inferTerm args trm = case trm of
K _ -> returnt str
C i -> returnt $ ints i
V i -> do
testErr (i < length args) ("too large index " ++ show i)
returnt $ args !! i
S ts -> do
(ts',tys) <- mapM infer ts >>= return . unzip
let tys' = filter (/=str) tys
testErr (null tys')
("expected Str in " ++ show trm ++ " not " ++ unwords (map show tys'))
return (S ts',str)
R ts -> do
(ts',tys) <- mapM infer ts >>= return . unzip
return $ (R ts',tuple tys)
P t u -> do
(t',tt) <- infer t
(u',tu) <- infer u
case tt of
R tys -> case tu of
R vs -> infer $ foldl P t' [P u' (C i) | i <- [0 .. length vs - 1]]
--- R [v] -> infer $ P t v
--- R (v:vs) -> infer $ P (head tys) (R vs)
C i -> do
testErr (i < length tys)
("required more than " ++ show i ++ " fields in " ++ show (R tys))
return (P t' u', tys !! i) -- record: index must be known
_ -> do
let typ = head tys
testErr (all (==typ) tys) ("different types in table " ++ show trm)
return (P t' u', typ) -- table: types must be same
_ -> Bad $ "projection from " ++ show t ++ " : " ++ show tt
FV [] -> returnt tm0 ----
FV (t:ts) -> do
(t',ty) <- infer t
(ts',tys) <- mapM infer ts >>= return . unzip
testErr (all (eqType True ty) tys) ("different types in variants " ++ show trm)
return (FV (t':ts'),ty)
W s r -> infer r
_ -> Bad ("no type inference for " ++ show trm)
where
returnt ty = return (trm,ty)
infer = inferTerm args
checkTerm :: LinType -> Term -> Err (Term,Bool)
checkTerm (args,val) trm = case inferTerm args trm of
Ok (t,ty) -> if eqType False ty val
then return (t,True)
else do
msg ("term: " ++ show trm ++
"\nexpected type: " ++ show val ++
"\ninferred type: " ++ show ty)
return (t,False)
Bad s -> do
msg s
return (trm,False)
-- symmetry in (Ints m == Ints n) is all we can use in variants
eqType :: Bool -> CType -> CType -> Bool
eqType symm inf exp = case (inf,exp) of
(C k, C n) -> if symm then True else k <= n -- only run-time corr.
(R rs,R ts) -> length rs == length ts && and [eqType symm r t | (r,t) <- zip rs ts]
(TM _, _) -> True ---- for variants [] ; not safe
_ -> inf == exp
-- should be in a generic module, but not in the run-time DataGFCC
type CType = Term
type LinType = ([CType],CType)
tuple :: [CType] -> CType
tuple = R
ints :: Int -> CType
ints = C
str :: CType
str = S []
lintype :: PGFSig -> CId -> CId -> LinType
lintype pgf lang fun = case typeSkeleton (lookFun pgf fun) of
(cs,c) -> (map vlinc cs, linc c) ---- HOAS
where
linc = lookLincat pgf lang
vlinc (0,c) = linc c
vlinc (i,c) = case linc c of
R ts -> R (ts ++ replicate i str)
inline :: PGFSig -> CId -> Term -> Term
inline pgf lang t = case t of
F c -> inl $ look c
_ -> composSafeOp inl t
where
inl = inline pgf lang
look = lookLin pgf lang
composOp :: Monad m => (Term -> m Term) -> Term -> m Term
composOp f trm = case trm of
R ts -> liftM R $ mapM f ts
S ts -> liftM S $ mapM f ts
FV ts -> liftM FV $ mapM f ts
P t u -> liftM2 P (f t) (f u)
W s t -> liftM (W s) $ f t
_ -> return trm
composSafeOp :: (Term -> Term) -> Term -> Term
composSafeOp f = maybe undefined id . composOp (return . f)
-- from GF.Data.Oper
maybeErr :: String -> Maybe a -> Err a
maybeErr s = maybe (Bad s) Ok
testErr :: Bool -> String -> Err ()
testErr cond msg = if cond then return () else Bad msg
errVal :: a -> Err a -> a
errVal a = err (const a) id
errIn :: String -> Err a -> Err a
errIn msg = err (\s -> Bad (s ++ "\nOCCURRED IN\n" ++ msg)) return
err :: (String -> b) -> (a -> b) -> Err a -> b
err d f e = case e of
Ok a -> f a
Bad s -> d s
lookFun (abs,lin,lincats) f = (\(a,b,c) -> a) $ fromMaybe (error "No abs") (Map.lookup f abs)
lookLincat (abs,lin,lincats) _ c = fromMaybe (error "No lincat") (Map.lookup c lincats)
lookLin (abs,lin,lincats) _ f = fromMaybe (error "No lin") (Map.lookup f lin)
|
