mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-15 06:02:55 -06:00
reorganize the directories under src, and rescue the JavaScript interpreter from deprecated
This commit is contained in:
krasimir
158
src/compiler/GF/Compile/Concrete/AppPredefined.hs
Normal file
158
src/compiler/GF/Compile/Concrete/AppPredefined.hs
Normal file
@@ -0,0 +1,158 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : AppPredefined
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/10/06 14:21:34 $
|
||||
-- > CVS $Author: aarne $
|
||||
-- > CVS $Revision: 1.13 $
|
||||
--
|
||||
-- Predefined function type signatures and definitions.
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module GF.Compile.Concrete.AppPredefined (isInPredefined, typPredefined, appPredefined
|
||||
) where
|
||||
|
||||
import GF.Infra.Ident
|
||||
import GF.Data.Operations
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.Grammar
|
||||
import GF.Grammar.Macros
|
||||
import GF.Grammar.Printer
|
||||
import qualified Data.ByteString.Char8 as BS
|
||||
import Text.PrettyPrint
|
||||
|
||||
-- predefined function type signatures and definitions. AR 12/3/2003.
|
||||
|
||||
isInPredefined :: Ident -> Bool
|
||||
isInPredefined = err (const True) (const False) . typPredefined
|
||||
|
||||
typPredefined :: Ident -> Err Type
|
||||
typPredefined f
|
||||
| f == cInt = return typePType
|
||||
| f == cFloat = return typePType
|
||||
| f == cErrorType = return typeType
|
||||
| f == cInts = return $ mkFunType [typeInt] typePType
|
||||
| f == cPBool = return typePType
|
||||
| f == cError = return $ mkFunType [typeStr] typeError -- non-can. of empty set
|
||||
| f == cPFalse = return $ typePBool
|
||||
| f == cPTrue = return $ typePBool
|
||||
| f == cDp = return $ mkFunType [typeInt,typeTok] typeTok
|
||||
| f == cDrop = return $ mkFunType [typeInt,typeTok] typeTok
|
||||
| f == cEqInt = return $ mkFunType [typeInt,typeInt] typePBool
|
||||
| f == cLessInt = return $ mkFunType [typeInt,typeInt] typePBool
|
||||
| f == cEqStr = return $ mkFunType [typeTok,typeTok] typePBool
|
||||
| f == cLength = return $ mkFunType [typeTok] typeInt
|
||||
| f == cOccur = return $ mkFunType [typeTok,typeTok] typePBool
|
||||
| f == cOccurs = return $ mkFunType [typeTok,typeTok] typePBool
|
||||
| f == cPlus = return $ mkFunType [typeInt,typeInt] (typeInt)
|
||||
---- "read" -> (P : Type) -> Tok -> P
|
||||
| f == cShow = return $ mkProd -- (P : PType) -> P -> Tok
|
||||
[(Explicit,varP,typePType),(Explicit,identW,Vr varP)] typeStr []
|
||||
| f == cToStr = return $ mkProd -- (L : Type) -> L -> Str
|
||||
[(Explicit,varL,typeType),(Explicit,identW,Vr varL)] typeStr []
|
||||
| f == cMapStr = return $ mkProd -- (L : Type) -> (Str -> Str) -> L -> L
|
||||
[(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)] (Vr varL) []
|
||||
| f == cTake = return $ mkFunType [typeInt,typeTok] typeTok
|
||||
| f == cTk = return $ mkFunType [typeInt,typeTok] typeTok
|
||||
| otherwise = Bad (render (text "unknown in Predef:" <+> ppIdent f))
|
||||
|
||||
varL :: Ident
|
||||
varL = identC (BS.pack "L")
|
||||
|
||||
varP :: Ident
|
||||
varP = identC (BS.pack "P")
|
||||
|
||||
appPredefined :: Term -> Err (Term,Bool)
|
||||
appPredefined t = case t of
|
||||
App f x0 -> do
|
||||
(x,_) <- appPredefined x0
|
||||
case f of
|
||||
-- one-place functions
|
||||
Q mod f | mod == cPredef ->
|
||||
case x of
|
||||
(K s) | f == cLength -> retb $ EInt $ toInteger $ length s
|
||||
_ -> retb t
|
||||
|
||||
-- two-place functions
|
||||
App (Q mod f) z0 | mod == cPredef -> do
|
||||
(z,_) <- appPredefined z0
|
||||
case (norm z, norm x) of
|
||||
(EInt i, K s) | f == cDrop -> retb $ K (drop (fi i) s)
|
||||
(EInt i, K s) | f == cTake -> retb $ K (take (fi i) s)
|
||||
(EInt i, K s) | f == cTk -> retb $ K (take (max 0 (length s - fi i)) s)
|
||||
(EInt i, K s) | f == cDp -> retb $ K (drop (max 0 (length s - fi i)) s)
|
||||
(K s, K t) | f == cEqStr -> retb $ if s == t then predefTrue else predefFalse
|
||||
(K s, K t) | f == cOccur -> retb $ if substring s t then predefTrue else predefFalse
|
||||
(K s, K t) | f == cOccurs -> retb $ if any (flip elem t) s then predefTrue else predefFalse
|
||||
(EInt i, EInt j) | f == cEqInt -> retb $ if i==j then predefTrue else predefFalse
|
||||
(EInt i, EInt j) | f == cLessInt -> retb $ if i<j then predefTrue else predefFalse
|
||||
(EInt i, EInt j) | f == cPlus -> retb $ EInt $ i+j
|
||||
(_, t) | f == cShow -> retb $ foldr C Empty $ map K $ words $ render (ppTerm Unqualified 0 t)
|
||||
(_, K s) | f == cRead -> retb $ Cn (identC (BS.pack s)) --- because of K, only works for atomic tags
|
||||
(_, t) | f == cToStr -> trm2str t >>= retb
|
||||
_ -> retb t ---- prtBad "cannot compute predefined" t
|
||||
|
||||
-- three-place functions
|
||||
App (App (Q mod f) z0) y0 | mod == cPredef -> do
|
||||
(y,_) <- appPredefined y0
|
||||
(z,_) <- appPredefined z0
|
||||
case (z, y, x) of
|
||||
(ty,op,t) | f == cMapStr -> retf $ mapStr ty op t
|
||||
_ -> retb t ---- prtBad "cannot compute predefined" t
|
||||
|
||||
_ -> retb t ---- prtBad "cannot compute predefined" t
|
||||
_ -> retb t
|
||||
---- should really check the absence of arg variables
|
||||
where
|
||||
retb t = return (retc t,True) -- no further computing needed
|
||||
retf t = return (retc t,False) -- must be computed further
|
||||
retc t = case t of
|
||||
K [] -> t
|
||||
K s -> foldr1 C (map K (words s))
|
||||
_ -> t
|
||||
norm t = case t of
|
||||
Empty -> K []
|
||||
C u v -> case (norm u,norm v) of
|
||||
(K x,K y) -> K (x +++ y)
|
||||
_ -> t
|
||||
_ -> t
|
||||
fi = fromInteger
|
||||
|
||||
-- read makes variables into constants
|
||||
|
||||
predefTrue = QC cPredef cPTrue
|
||||
predefFalse = QC cPredef cPFalse
|
||||
|
||||
substring :: String -> String -> Bool
|
||||
substring s t = case (s,t) of
|
||||
(c:cs, d:ds) -> (c == d && substring cs ds) || substring s ds
|
||||
([],_) -> True
|
||||
_ -> False
|
||||
|
||||
trm2str :: Term -> Err Term
|
||||
trm2str t = case t of
|
||||
R ((_,(_,s)):_) -> trm2str s
|
||||
T _ ((_,s):_) -> trm2str s
|
||||
V _ (s:_) -> trm2str s
|
||||
C _ _ -> return $ t
|
||||
K _ -> return $ t
|
||||
S c _ -> trm2str c
|
||||
Empty -> return $ t
|
||||
_ -> Bad (render (text "cannot get Str from term" <+> ppTerm Unqualified 0 t))
|
||||
|
||||
-- simultaneous recursion on type and term: type arg is essential!
|
||||
-- But simplify the task by assuming records are type-annotated
|
||||
-- (this has been done in type checking)
|
||||
mapStr :: Type -> Term -> Term -> Term
|
||||
mapStr ty f t = case (ty,t) of
|
||||
_ | elem ty [typeStr,typeTok] -> App f t
|
||||
(_, R ts) -> R [(l,mapField v) | (l,v) <- ts]
|
||||
(Table a b,T ti cs) -> T ti [(p,mapStr b f v) | (p,v) <- cs]
|
||||
_ -> t
|
||||
where
|
||||
mapField (mty,te) = case mty of
|
||||
Just ty -> (mty,mapStr ty f te)
|
||||
_ -> (mty,te)
|
||||
456
src/compiler/GF/Compile/Concrete/Compute.hs
Normal file
456
src/compiler/GF/Compile/Concrete/Compute.hs
Normal file
@@ -0,0 +1,456 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : GF.Compile.Concrete.Compute
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/11/01 15:39:12 $
|
||||
-- > CVS $Author: aarne $
|
||||
-- > CVS $Revision: 1.19 $
|
||||
--
|
||||
-- Computation of source terms. Used in compilation and in @cc@ command.
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module GF.Compile.Concrete.Compute (computeConcrete, computeTerm,computeConcreteRec) where
|
||||
|
||||
import GF.Data.Operations
|
||||
import GF.Grammar.Grammar
|
||||
import GF.Infra.Ident
|
||||
import GF.Infra.Option
|
||||
import GF.Infra.Modules
|
||||
import GF.Data.Str
|
||||
import GF.Grammar.Printer
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.Macros
|
||||
import GF.Grammar.Lookup
|
||||
import GF.Compile.Refresh
|
||||
import GF.Grammar.PatternMatch
|
||||
import GF.Grammar.Lockfield (isLockLabel,unlockRecord) ----
|
||||
|
||||
import GF.Compile.Concrete.AppPredefined
|
||||
|
||||
import Data.List (nub,intersperse)
|
||||
import Control.Monad (liftM2, liftM)
|
||||
import Text.PrettyPrint
|
||||
|
||||
-- | computation of concrete syntax terms into normal form
|
||||
-- used mainly for partial evaluation
|
||||
computeConcrete :: SourceGrammar -> Term -> Err Term
|
||||
computeConcrete g t = {- refreshTerm t >>= -} computeTerm g [] t
|
||||
computeConcreteRec g t = {- refreshTerm t >>= -} computeTermOpt True g [] t
|
||||
|
||||
computeTerm :: SourceGrammar -> Substitution -> Term -> Err Term
|
||||
computeTerm = computeTermOpt False
|
||||
|
||||
-- rec=True is used if it cannot be assumed that looked-up constants
|
||||
-- have already been computed (mainly with -optimize=noexpand in .gfr)
|
||||
|
||||
computeTermOpt :: Bool -> SourceGrammar -> Substitution -> Term -> Err Term
|
||||
computeTermOpt rec gr = comput True where
|
||||
|
||||
comput full g t = ---- errIn ("subterm" +++ prt t) $ --- for debugging
|
||||
case t of
|
||||
|
||||
Q p c | p == cPredef -> return t
|
||||
| otherwise -> look p c
|
||||
|
||||
Vr x -> do
|
||||
t' <- maybe (Bad (render (text "no value given to variable" <+> ppIdent x))) return $ lookup x g
|
||||
case t' of
|
||||
_ | t == t' -> return t
|
||||
_ -> comp g t'
|
||||
|
||||
-- Abs x@(IA _) b -> do
|
||||
Abs _ _ _ | full -> do
|
||||
let (xs,b1) = termFormCnc t
|
||||
b' <- comp ([(x,Vr x) | (_,x) <- xs] ++ g) b1
|
||||
return $ mkAbs xs b'
|
||||
-- b' <- comp (ext x (Vr x) g) b
|
||||
-- return $ Abs x b'
|
||||
Abs _ _ _ -> return t -- hnf
|
||||
|
||||
Let (x,(_,a)) b -> do
|
||||
a' <- comp g a
|
||||
comp (ext x a' g) b
|
||||
|
||||
Prod b x a t -> do
|
||||
a' <- comp g a
|
||||
t' <- comp (ext x (Vr x) g) t
|
||||
return $ Prod b x a' t'
|
||||
|
||||
-- beta-convert
|
||||
App f a -> case appForm t of
|
||||
(h,as) | length as > 1 -> do
|
||||
h' <- hnf g h
|
||||
as' <- mapM (comp g) as
|
||||
case h' of
|
||||
_ | not (null [() | FV _ <- as']) -> compApp g (mkApp h' as')
|
||||
c@(QC _ _) -> do
|
||||
return $ mkApp c as'
|
||||
Q mod f | mod == cPredef -> do
|
||||
(t',b) <- appPredefined (mkApp h' as')
|
||||
if b then return t' else comp g t'
|
||||
|
||||
Abs _ _ _ -> do
|
||||
let (xs,b) = termFormCnc h'
|
||||
let g' = (zip (map snd xs) as') ++ g
|
||||
let as2 = drop (length xs) as'
|
||||
let xs2 = drop (length as') xs
|
||||
b' <- comp g' (mkAbs xs2 b)
|
||||
if null as2 then return b' else comp g (mkApp b' as2)
|
||||
|
||||
_ -> compApp g (mkApp h' as')
|
||||
_ -> compApp g t
|
||||
|
||||
P t l | isLockLabel l -> return $ R []
|
||||
---- a workaround 18/2/2005: take this away and find the reason
|
||||
---- why earlier compilation destroys the lock field
|
||||
|
||||
|
||||
P t l -> do
|
||||
t' <- comp g t
|
||||
case t' of
|
||||
FV rs -> mapM (\c -> comp g (P c l)) rs >>= returnC . variants
|
||||
R r -> maybe (Bad (render (text "no value for label" <+> ppLabel l))) (comp g . snd) $
|
||||
lookup l $ reverse r
|
||||
|
||||
ExtR a (R b) ->
|
||||
case comp g (P (R b) l) of
|
||||
Ok v -> return v
|
||||
_ -> comp g (P a l)
|
||||
|
||||
--- { - --- this is incorrect, since b can contain the proper value
|
||||
ExtR (R a) b -> -- NOT POSSIBLE both a and b records!
|
||||
case comp g (P (R a) l) of
|
||||
Ok v -> return v
|
||||
_ -> comp g (P b l)
|
||||
--- - } ---
|
||||
|
||||
S (T i cs) e -> prawitz g i (flip P l) cs e
|
||||
S (V i cs) e -> prawitzV g i (flip P l) cs e
|
||||
|
||||
_ -> returnC $ P t' l
|
||||
|
||||
S t v -> do
|
||||
t' <- compTable g t
|
||||
v' <- comp g v
|
||||
t1 <- case t' of
|
||||
---- V (RecType fs) _ -> uncurrySelect g fs t' v'
|
||||
---- T (TComp (RecType fs)) _ -> uncurrySelect g fs t' v'
|
||||
_ -> return $ S t' v'
|
||||
compSelect g t1
|
||||
|
||||
-- normalize away empty tokens
|
||||
K "" -> return Empty
|
||||
|
||||
-- glue if you can
|
||||
Glue x0 y0 -> do
|
||||
x <- comp g x0
|
||||
y <- comp g y0
|
||||
case (x,y) of
|
||||
(FV ks,_) -> do
|
||||
kys <- mapM (comp g . flip Glue y) ks
|
||||
return $ variants kys
|
||||
(_,FV ks) -> do
|
||||
xks <- mapM (comp g . Glue x) ks
|
||||
return $ variants xks
|
||||
|
||||
(S (T i cs) e, s) -> prawitz g i (flip Glue s) cs e
|
||||
(s, S (T i cs) e) -> prawitz g i (Glue s) cs e
|
||||
(S (V i cs) e, s) -> prawitzV g i (flip Glue s) cs e
|
||||
(s, S (V i cs) e) -> prawitzV g i (Glue s) cs e
|
||||
(_,Empty) -> return x
|
||||
(Empty,_) -> return y
|
||||
(K a, K b) -> return $ K (a ++ b)
|
||||
(_, Alts (d,vs)) -> do
|
||||
---- (K a, Alts (d,vs)) -> do
|
||||
let glx = Glue x
|
||||
comp g $ Alts (glx d, [(glx v,c) | (v,c) <- vs])
|
||||
(Alts _, ka) -> checks [do
|
||||
y' <- strsFromTerm ka
|
||||
---- (Alts _, K a) -> checks [do
|
||||
x' <- strsFromTerm x -- this may fail when compiling opers
|
||||
return $ variants [
|
||||
foldr1 C (map K (str2strings (glueStr v u))) | v <- x', u <- y']
|
||||
---- foldr1 C (map K (str2strings (glueStr v (str a)))) | v <- x']
|
||||
,return $ Glue x y
|
||||
]
|
||||
(C u v,_) -> comp g $ C u (Glue v y)
|
||||
|
||||
_ -> do
|
||||
mapM_ checkNoArgVars [x,y]
|
||||
r <- composOp (comp g) t
|
||||
returnC r
|
||||
|
||||
Alts (d,aa) -> do
|
||||
d' <- comp g d
|
||||
aa' <- mapM (compInAlts g) aa
|
||||
returnC (Alts (d',aa'))
|
||||
|
||||
-- remove empty
|
||||
C a b -> do
|
||||
a' <- comp g a
|
||||
b' <- comp g b
|
||||
case (a',b') of
|
||||
(Alts _, K a) -> checks [do
|
||||
as <- strsFromTerm a' -- this may fail when compiling opers
|
||||
return $ variants [
|
||||
foldr1 C (map K (str2strings (plusStr v (str a)))) | v <- as]
|
||||
,
|
||||
return $ C a' b'
|
||||
]
|
||||
(Empty,_) -> returnC b'
|
||||
(_,Empty) -> returnC a'
|
||||
_ -> returnC $ C a' b'
|
||||
|
||||
-- reduce free variation as much as you can
|
||||
FV ts -> mapM (comp g) ts >>= returnC . variants
|
||||
|
||||
-- merge record extensions if you can
|
||||
ExtR r s -> do
|
||||
r' <- comp g r
|
||||
s' <- comp g s
|
||||
case (r',s') of
|
||||
(R rs, R ss) -> plusRecord r' s'
|
||||
(RecType rs, RecType ss) -> plusRecType r' s'
|
||||
_ -> return $ ExtR r' s'
|
||||
|
||||
ELin c r -> do
|
||||
r' <- comp g r
|
||||
unlockRecord c r'
|
||||
|
||||
T _ _ -> compTable g t
|
||||
V _ _ -> compTable g t
|
||||
|
||||
-- otherwise go ahead
|
||||
_ -> composOp (comp g) t >>= returnC
|
||||
|
||||
where
|
||||
|
||||
compApp g (App f a) = do
|
||||
f' <- hnf g f
|
||||
a' <- comp g a
|
||||
case (f',a') of
|
||||
(Abs _ x b, FV as) ->
|
||||
mapM (\c -> comp (ext x c g) b) as >>= return . variants
|
||||
(_, FV as) -> mapM (\c -> comp g (App f' c)) as >>= return . variants
|
||||
(FV fs, _) -> mapM (\c -> comp g (App c a')) fs >>= return . variants
|
||||
(Abs _ x b,_) -> comp (ext x a' g) b
|
||||
|
||||
(QC _ _,_) -> returnC $ App f' a'
|
||||
|
||||
(S (T i cs) e,_) -> prawitz g i (flip App a') cs e
|
||||
(S (V i cs) e,_) -> prawitzV g i (flip App a') cs e
|
||||
|
||||
_ -> do
|
||||
(t',b) <- appPredefined (App f' a')
|
||||
if b then return t' else comp g t'
|
||||
|
||||
hnf = comput False
|
||||
comp = comput True
|
||||
|
||||
look p c
|
||||
| rec = lookupResDef gr p c >>= comp []
|
||||
| otherwise = lookupResDef gr p c
|
||||
|
||||
ext x a g = (x,a):g
|
||||
|
||||
returnC = return --- . computed
|
||||
|
||||
variants ts = case nub ts of
|
||||
[t] -> t
|
||||
ts -> FV ts
|
||||
|
||||
isCan v = case v of
|
||||
Con _ -> True
|
||||
QC _ _ -> True
|
||||
App f a -> isCan f && isCan a
|
||||
R rs -> all (isCan . snd . snd) rs
|
||||
_ -> False
|
||||
|
||||
compPatternMacro p = case p of
|
||||
PM m c -> case look m c of
|
||||
Ok (EPatt p') -> compPatternMacro p'
|
||||
_ -> Bad (render (text "pattern expected as value of" $$ nest 2 (ppPatt Unqualified 0 p)))
|
||||
PAs x p -> do
|
||||
p' <- compPatternMacro p
|
||||
return $ PAs x p'
|
||||
PAlt p q -> do
|
||||
p' <- compPatternMacro p
|
||||
q' <- compPatternMacro q
|
||||
return $ PAlt p' q'
|
||||
PSeq p q -> do
|
||||
p' <- compPatternMacro p
|
||||
q' <- compPatternMacro q
|
||||
return $ PSeq p' q'
|
||||
PRep p -> do
|
||||
p' <- compPatternMacro p
|
||||
return $ PRep p'
|
||||
PNeg p -> do
|
||||
p' <- compPatternMacro p
|
||||
return $ PNeg p'
|
||||
PR rs -> do
|
||||
rs' <- mapPairsM compPatternMacro rs
|
||||
return $ PR rs'
|
||||
|
||||
_ -> return p
|
||||
|
||||
compSelect g (S t' v') = case v' of
|
||||
FV vs -> mapM (\c -> comp g (S t' c)) vs >>= returnC . variants
|
||||
_ -> case t' of
|
||||
FV ccs -> mapM (\c -> comp g (S c v')) ccs >>= returnC . variants
|
||||
|
||||
T _ [(PW,c)] -> comp g c --- an optimization
|
||||
T _ [(PT _ PW,c)] -> comp g c
|
||||
|
||||
T _ [(PV z,c)] -> comp (ext z v' g) c --- another optimization
|
||||
T _ [(PT _ (PV z),c)] -> comp (ext z v' g) c
|
||||
|
||||
-- course-of-values table: look up by index, no pattern matching needed
|
||||
|
||||
V ptyp ts -> do
|
||||
vs <- allParamValues gr ptyp
|
||||
case lookupR v' (zip vs [0 .. length vs - 1]) of
|
||||
Just i -> comp g $ ts !! i
|
||||
_ -> return $ S t' v' -- if v' is not canonical
|
||||
T _ cc -> do
|
||||
case matchPattern cc v' of
|
||||
Ok (c,g') -> comp (g' ++ g) c
|
||||
_ | isCan v' -> Bad (render (text "missing case" <+> ppTerm Unqualified 0 v' <+> text "in" <+> ppTerm Unqualified 0 t))
|
||||
_ -> return $ S t' v' -- if v' is not canonical
|
||||
|
||||
S (T i cs) e -> prawitz g i (flip S v') cs e
|
||||
S (V i cs) e -> prawitzV g i (flip S v') cs e
|
||||
_ -> returnC $ S t' v'
|
||||
|
||||
--- needed to match records with and without type information
|
||||
---- todo: eliminate linear search in a list of records!
|
||||
lookupR v vs = case v of
|
||||
R rs -> lookup ([(x,y) | (x,(_,y)) <- rs])
|
||||
[([(x,y) | (x,(_,y)) <- rs],v) | (R rs,v) <- vs]
|
||||
_ -> lookup v vs
|
||||
|
||||
-- case-expand tables
|
||||
-- if already expanded, don't expand again
|
||||
compTable g t = case t of
|
||||
T i@(TComp ty) cs -> do
|
||||
-- if there are no variables, don't even go inside
|
||||
cs' <- if (null g) then return cs else mapPairsM (comp g) cs
|
||||
---- return $ V ty (map snd cs')
|
||||
return $ T i cs'
|
||||
V ty cs -> do
|
||||
ty' <- comp g ty
|
||||
-- if there are no variables, don't even go inside
|
||||
cs' <- if (null g) then return cs else mapM (comp g) cs
|
||||
return $ V ty' cs'
|
||||
|
||||
T i cs -> do
|
||||
pty0 <- getTableType i
|
||||
ptyp <- comp g pty0
|
||||
case allParamValues gr ptyp of
|
||||
Ok vs0 -> do
|
||||
let vs = vs0 ---- [Val v ptyp i | (v,i) <- zip vs0 [0..]]
|
||||
ps0 <- mapM (compPatternMacro . fst) cs
|
||||
cs' <- mapM (compBranchOpt g) (zip ps0 (map snd cs))
|
||||
sts <- mapM (matchPattern cs') vs
|
||||
ts <- mapM (\ (c,g') -> comp (g' ++ g) c) sts
|
||||
ps <- mapM term2patt vs
|
||||
let ps' = ps --- PT ptyp (head ps) : tail ps
|
||||
---- return $ V ptyp ts -- to save space, just course of values
|
||||
return $ T (TComp ptyp) (zip ps' ts)
|
||||
_ -> do
|
||||
ps0 <- mapM (compPatternMacro . fst) cs
|
||||
cs' <- mapM (compBranch g) (zip ps0 (map snd cs))
|
||||
|
||||
---- cs' <- mapM (compBranch g) cs
|
||||
return $ T i cs' -- happens with variable types
|
||||
_ -> comp g t
|
||||
|
||||
compBranch g (p,v) = do
|
||||
let g' = contP p ++ g
|
||||
v' <- comp g' v
|
||||
return (p,v')
|
||||
|
||||
compBranchOpt g c@(p,v) = case contP p of
|
||||
[] -> return c
|
||||
_ -> err (const (return c)) return $ compBranch g c
|
||||
|
||||
contP p = case p of
|
||||
PV x -> [(x,Vr x)]
|
||||
PC _ ps -> concatMap contP ps
|
||||
PP _ _ ps -> concatMap contP ps
|
||||
PT _ p -> contP p
|
||||
PR rs -> concatMap (contP . snd) rs
|
||||
|
||||
PAs x p -> (x,Vr x) : contP p
|
||||
|
||||
PSeq p q -> concatMap contP [p,q]
|
||||
PAlt p q -> concatMap contP [p,q]
|
||||
PRep p -> contP p
|
||||
PNeg p -> contP p
|
||||
|
||||
_ -> []
|
||||
|
||||
prawitz g i f cs e = do
|
||||
cs' <- mapM (compBranch g) [(p, f v) | (p,v) <- cs]
|
||||
return $ S (T i cs') e
|
||||
prawitzV g i f cs e = do
|
||||
cs' <- mapM (comp g) [(f v) | v <- cs]
|
||||
return $ S (V i cs') e
|
||||
|
||||
compInAlts g (v,c) = do
|
||||
v' <- comp g v
|
||||
c' <- comp g c
|
||||
c2 <- case c' of
|
||||
EPatt p -> liftM Strs $ getPatts p
|
||||
_ -> return c'
|
||||
return (v',c2)
|
||||
where
|
||||
getPatts p = case p of
|
||||
PAlt a b -> liftM2 (++) (getPatts a) (getPatts b)
|
||||
PString s -> return [K s]
|
||||
PSeq a b -> do
|
||||
as <- getPatts a
|
||||
bs <- getPatts b
|
||||
return [K (s ++ t) | K s <- as, K t <- bs]
|
||||
_ -> fail (render (text "not valid pattern in pre expression" <+> ppPatt Unqualified 0 p))
|
||||
|
||||
{- ----
|
||||
uncurrySelect g fs t v = do
|
||||
ts <- mapM (allParamValues gr . snd) fs
|
||||
vs <- mapM (comp g) [P v r | r <- map fst fs]
|
||||
return $ reorderSelect t fs ts vs
|
||||
|
||||
reorderSelect t fs pss vs = case (t,fs,pss,vs) of
|
||||
(V _ ts, f:fs1, ps:pss1, v:vs1) ->
|
||||
S (V (snd f)
|
||||
[reorderSelect (V (RecType fs1) t) fs1 pss1 vs1 |
|
||||
t <- segments (length ts `div` length ps) ts]) v
|
||||
(T (TComp _) cs, f:fs1, ps:pss1, v:vs1) ->
|
||||
S (T (TComp (snd f))
|
||||
[(p,reorderSelect (T (TComp (RecType fs1)) c) fs1 pss1 vs1) |
|
||||
(ep,c) <- zip ps (segments (length cs `div` length ps) cs),
|
||||
let Ok p = term2patt ep]) v
|
||||
_ -> t
|
||||
|
||||
segments i xs =
|
||||
let (x0,xs1) = splitAt i xs in x0 : takeWhile (not . null) (segments i xs1)
|
||||
-}
|
||||
|
||||
|
||||
-- | argument variables cannot be glued
|
||||
checkNoArgVars :: Term -> Err Term
|
||||
checkNoArgVars t = case t of
|
||||
Vr (IA _ _) -> Bad $ glueErrorMsg $ ppTerm Unqualified 0 t
|
||||
Vr (IAV _ _ _) -> Bad $ glueErrorMsg $ ppTerm Unqualified 0 t
|
||||
_ -> composOp checkNoArgVars t
|
||||
|
||||
glueErrorMsg s =
|
||||
render (text "Cannot glue (+) term with run-time variable" <+> s <> char '.' $$
|
||||
text "Use Prelude.bind instead.")
|
||||
|
||||
getArgType t = case t of
|
||||
V ty _ -> return ty
|
||||
T (TComp ty) _ -> return ty
|
||||
_ -> Bad (render (text "cannot get argument type of table" $$ nest 2 (ppTerm Unqualified 0 t)))
|
||||
690
src/compiler/GF/Compile/Concrete/TypeCheck.hs
Normal file
690
src/compiler/GF/Compile/Concrete/TypeCheck.hs
Normal file
@@ -0,0 +1,690 @@
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
module GF.Compile.Concrete.TypeCheck( checkLType, inferLType, computeLType, ppType ) where
|
||||
|
||||
import GF.Infra.CheckM
|
||||
import GF.Infra.Modules
|
||||
import GF.Data.Operations
|
||||
|
||||
import GF.Grammar
|
||||
import GF.Grammar.Lookup
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.PatternMatch
|
||||
import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
|
||||
import GF.Compile.Concrete.AppPredefined
|
||||
|
||||
import Data.List
|
||||
import Control.Monad
|
||||
import Text.PrettyPrint
|
||||
|
||||
computeLType :: SourceGrammar -> Context -> Type -> Check Type
|
||||
computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
|
||||
where
|
||||
comp g ty = case ty of
|
||||
_ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
|
||||
| isPredefConstant ty -> return ty ---- shouldn't be needed
|
||||
|
||||
Q m ident -> checkIn (text "module" <+> ppIdent m) $ do
|
||||
ty' <- checkErr (lookupResDef gr m ident)
|
||||
if ty' == ty then return ty else comp g ty' --- is this necessary to test?
|
||||
|
||||
Vr ident -> checkLookup ident g -- never needed to compute!
|
||||
|
||||
App f a -> do
|
||||
f' <- comp g f
|
||||
a' <- comp g a
|
||||
case f' of
|
||||
Abs b x t -> comp ((b,x,a'):g) t
|
||||
_ -> return $ App f' a'
|
||||
|
||||
Prod bt x a b -> do
|
||||
a' <- comp g a
|
||||
b' <- comp ((bt,x,Vr x) : g) b
|
||||
return $ Prod bt x a' b'
|
||||
|
||||
Abs bt x b -> do
|
||||
b' <- comp ((bt,x,Vr x):g) b
|
||||
return $ Abs bt x b'
|
||||
|
||||
ExtR r s -> do
|
||||
r' <- comp g r
|
||||
s' <- comp g s
|
||||
case (r',s') of
|
||||
(RecType rs, RecType ss) -> checkErr (plusRecType r' s') >>= comp g
|
||||
_ -> return $ ExtR r' s'
|
||||
|
||||
RecType fs -> do
|
||||
let fs' = sortRec fs
|
||||
liftM RecType $ mapPairsM (comp g) fs'
|
||||
|
||||
ELincat c t -> do
|
||||
t' <- comp g t
|
||||
checkErr $ lockRecType c t' ---- locking to be removed AR 20/6/2009
|
||||
|
||||
_ | ty == typeTok -> return typeStr
|
||||
_ | isPredefConstant ty -> return ty
|
||||
|
||||
_ -> composOp (comp g) ty
|
||||
|
||||
-- the underlying algorithms
|
||||
|
||||
inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
|
||||
inferLType gr g trm = case trm of
|
||||
|
||||
Q m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
|
||||
|
||||
Q m ident -> checks [
|
||||
termWith trm $ checkErr (lookupResType gr m ident) >>= computeLType gr g
|
||||
,
|
||||
checkErr (lookupResDef gr m ident) >>= inferLType gr g
|
||||
,
|
||||
checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
|
||||
]
|
||||
|
||||
QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
|
||||
|
||||
QC m ident -> checks [
|
||||
termWith trm $ checkErr (lookupResType gr m ident) >>= computeLType gr g
|
||||
,
|
||||
checkErr (lookupResDef gr m ident) >>= inferLType gr g
|
||||
,
|
||||
checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
|
||||
]
|
||||
|
||||
Vr ident -> termWith trm $ checkLookup ident g
|
||||
|
||||
Typed e t -> do
|
||||
t' <- computeLType gr g t
|
||||
checkLType gr g e t'
|
||||
return (e,t')
|
||||
|
||||
App f a -> do
|
||||
over <- getOverload gr g Nothing trm
|
||||
case over of
|
||||
Just trty -> return trty
|
||||
_ -> do
|
||||
(f',fty) <- inferLType gr g f
|
||||
fty' <- computeLType gr g fty
|
||||
case fty' of
|
||||
Prod bt z arg val -> do
|
||||
a' <- justCheck g a arg
|
||||
ty <- if isWildIdent z
|
||||
then return val
|
||||
else substituteLType [(bt,z,a')] val
|
||||
return (App f' a',ty)
|
||||
_ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType fty)
|
||||
|
||||
S f x -> do
|
||||
(f', fty) <- inferLType gr g f
|
||||
case fty of
|
||||
Table arg val -> do
|
||||
x'<- justCheck g x arg
|
||||
return (S f' x', val)
|
||||
_ -> checkError (text "table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
|
||||
|
||||
P t i -> do
|
||||
(t',ty) <- inferLType gr g t --- ??
|
||||
ty' <- computeLType gr g ty
|
||||
let tr2 = P t' i
|
||||
termWith tr2 $ case ty' of
|
||||
RecType ts -> case lookup i ts of
|
||||
Nothing -> checkError (text "unknown label" <+> ppLabel i <+> text "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
|
||||
Just x -> return x
|
||||
_ -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
|
||||
text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
|
||||
|
||||
R r -> do
|
||||
let (ls,fs) = unzip r
|
||||
fsts <- mapM inferM fs
|
||||
let ts = [ty | (Just ty,_) <- fsts]
|
||||
checkCond (text "cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
|
||||
return $ (R (zip ls fsts), RecType (zip ls ts))
|
||||
|
||||
T (TTyped arg) pts -> do
|
||||
(_,val) <- checks $ map (inferCase (Just arg)) pts
|
||||
checkLType gr g trm (Table arg val)
|
||||
T (TComp arg) pts -> do
|
||||
(_,val) <- checks $ map (inferCase (Just arg)) pts
|
||||
checkLType gr g trm (Table arg val)
|
||||
T ti pts -> do -- tries to guess: good in oper type inference
|
||||
let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
|
||||
case pts' of
|
||||
[] -> checkError (text "cannot infer table type of" <+> ppTerm Unqualified 0 trm)
|
||||
---- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
|
||||
_ -> do
|
||||
(arg,val) <- checks $ map (inferCase Nothing) pts'
|
||||
checkLType gr g trm (Table arg val)
|
||||
V arg pts -> do
|
||||
(_,val) <- checks $ map (inferLType gr g) pts
|
||||
return (trm, Table arg val)
|
||||
|
||||
K s -> do
|
||||
if elem ' ' s
|
||||
then do
|
||||
let ss = foldr C Empty (map K (words s))
|
||||
----- removed irritating warning AR 24/5/2008
|
||||
----- checkWarn ("token \"" ++ s ++
|
||||
----- "\" converted to token list" ++ prt ss)
|
||||
return (ss, typeStr)
|
||||
else return (trm, typeStr)
|
||||
|
||||
EInt i -> return (trm, typeInt)
|
||||
|
||||
EFloat i -> return (trm, typeFloat)
|
||||
|
||||
Empty -> return (trm, typeStr)
|
||||
|
||||
C s1 s2 ->
|
||||
check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
|
||||
|
||||
Glue s1 s2 ->
|
||||
check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok
|
||||
|
||||
---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
|
||||
Strs (Cn c : ts) | c == cConflict -> do
|
||||
checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
|
||||
inferLType gr g (head ts)
|
||||
|
||||
Strs ts -> do
|
||||
ts' <- mapM (\t -> justCheck g t typeStr) ts
|
||||
return (Strs ts', typeStrs)
|
||||
|
||||
Alts (t,aa) -> do
|
||||
t' <- justCheck g t typeStr
|
||||
aa' <- flip mapM aa (\ (c,v) -> do
|
||||
c' <- justCheck g c typeStr
|
||||
v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
|
||||
return (c',v'))
|
||||
return (Alts (t',aa'), typeStr)
|
||||
|
||||
RecType r -> do
|
||||
let (ls,ts) = unzip r
|
||||
ts' <- mapM (flip (justCheck g) typeType) ts
|
||||
return (RecType (zip ls ts'), typeType)
|
||||
|
||||
ExtR r s -> do
|
||||
(r',rT) <- inferLType gr g r
|
||||
rT' <- computeLType gr g rT
|
||||
(s',sT) <- inferLType gr g s
|
||||
sT' <- computeLType gr g sT
|
||||
|
||||
let trm' = ExtR r' s'
|
||||
---- trm' <- checkErr $ plusRecord r' s'
|
||||
case (rT', sT') of
|
||||
(RecType rs, RecType ss) -> do
|
||||
rt <- checkErr $ plusRecType rT' sT'
|
||||
checkLType gr g trm' rt ---- return (trm', rt)
|
||||
_ | rT' == typeType && sT' == typeType -> return (trm', typeType)
|
||||
_ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm)
|
||||
|
||||
Sort _ ->
|
||||
termWith trm $ return typeType
|
||||
|
||||
Prod bt x a b -> do
|
||||
a' <- justCheck g a typeType
|
||||
b' <- justCheck ((bt,x,a'):g) b typeType
|
||||
return (Prod bt x a' b', typeType)
|
||||
|
||||
Table p t -> do
|
||||
p' <- justCheck g p typeType --- check p partype!
|
||||
t' <- justCheck g t typeType
|
||||
return $ (Table p' t', typeType)
|
||||
|
||||
FV vs -> do
|
||||
(_,ty) <- checks $ map (inferLType gr g) vs
|
||||
--- checkIfComplexVariantType trm ty
|
||||
checkLType gr g trm ty
|
||||
|
||||
EPattType ty -> do
|
||||
ty' <- justCheck g ty typeType
|
||||
return (EPattType ty',typeType)
|
||||
EPatt p -> do
|
||||
ty <- inferPatt p
|
||||
return (trm, EPattType ty)
|
||||
|
||||
ELin c trm -> do
|
||||
(trm',ty) <- inferLType gr g trm
|
||||
ty' <- checkErr $ lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
|
||||
return $ (ELin c trm', ty')
|
||||
|
||||
_ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
|
||||
|
||||
where
|
||||
isPredef m = elem m [cPredef,cPredefAbs]
|
||||
|
||||
justCheck g ty te = checkLType gr g ty te >>= return . fst
|
||||
|
||||
-- for record fields, which may be typed
|
||||
inferM (mty, t) = do
|
||||
(t', ty') <- case mty of
|
||||
Just ty -> checkLType gr g ty t
|
||||
_ -> inferLType gr g t
|
||||
return (Just ty',t')
|
||||
|
||||
inferCase mty (patt,term) = do
|
||||
arg <- maybe (inferPatt patt) return mty
|
||||
cont <- pattContext gr g arg patt
|
||||
(_,val) <- inferLType gr (reverse cont ++ g) term
|
||||
return (arg,val)
|
||||
isConstPatt p = case p of
|
||||
PC _ ps -> True --- all isConstPatt ps
|
||||
PP _ _ ps -> True --- all isConstPatt ps
|
||||
PR ps -> all (isConstPatt . snd) ps
|
||||
PT _ p -> isConstPatt p
|
||||
PString _ -> True
|
||||
PInt _ -> True
|
||||
PFloat _ -> True
|
||||
PChar -> True
|
||||
PChars _ -> True
|
||||
PSeq p q -> isConstPatt p && isConstPatt q
|
||||
PAlt p q -> isConstPatt p && isConstPatt q
|
||||
PRep p -> isConstPatt p
|
||||
PNeg p -> isConstPatt p
|
||||
PAs _ p -> isConstPatt p
|
||||
_ -> False
|
||||
|
||||
inferPatt p = case p of
|
||||
PP q c ps | q /= cPredef -> checkErr $ liftM valTypeCnc (lookupResType gr q c)
|
||||
PAs _ p -> inferPatt p
|
||||
PNeg p -> inferPatt p
|
||||
PAlt p q -> checks [inferPatt p, inferPatt q]
|
||||
PSeq _ _ -> return $ typeStr
|
||||
PRep _ -> return $ typeStr
|
||||
PChar -> return $ typeStr
|
||||
PChars _ -> return $ typeStr
|
||||
_ -> inferLType gr g (patt2term p) >>= return . snd
|
||||
|
||||
|
||||
-- type inference: Nothing, type checking: Just t
|
||||
-- the latter permits matching with value type
|
||||
getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
|
||||
getOverload gr g mt ot = case appForm ot of
|
||||
(f@(Q m c), ts) -> case lookupOverload gr m c of
|
||||
Ok typs -> do
|
||||
ttys <- mapM (inferLType gr g) ts
|
||||
v <- matchOverload f typs ttys
|
||||
return $ Just v
|
||||
_ -> return Nothing
|
||||
_ -> return Nothing
|
||||
where
|
||||
matchOverload f typs ttys = do
|
||||
let (tts,tys) = unzip ttys
|
||||
let vfs = lookupOverloadInstance tys typs
|
||||
let matches = [vf | vf@((v,_),_) <- vfs, matchVal mt v]
|
||||
|
||||
case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
|
||||
([(val,fun)],_) -> return (mkApp fun tts, val)
|
||||
([],[(val,fun)]) -> do
|
||||
checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
|
||||
return (mkApp fun tts, val)
|
||||
([],[]) -> do
|
||||
let showTypes ty = hsep (map ppType ty)
|
||||
checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
|
||||
text "for" $$
|
||||
nest 2 (showTypes tys) $$
|
||||
text "among" $$
|
||||
nest 2 (vcat [showTypes ty | (ty,_) <- typs]) $$
|
||||
maybe empty (\x -> text "with value type" <+> ppType x) mt
|
||||
|
||||
(vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
|
||||
([(val,fun)],_) -> do
|
||||
return (mkApp fun tts, val)
|
||||
([],[(val,fun)]) -> do
|
||||
checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
|
||||
return (mkApp fun tts, val)
|
||||
|
||||
----- unsafely exclude irritating warning AR 24/5/2008
|
||||
----- checkWarn $ "overloading of" +++ prt f +++
|
||||
----- "resolved by excluding partial applications:" ++++
|
||||
----- unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
|
||||
|
||||
|
||||
_ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
|
||||
text "for" <+> hsep (map ppType tys) $$
|
||||
text "with alternatives" $$
|
||||
nest 2 (vcat [ppType ty | (ty,_) <- if null vfs1 then vfs2 else vfs2])
|
||||
|
||||
matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
|
||||
|
||||
unlocked v = case v of
|
||||
RecType fs -> RecType $ filter (not . isLockLabel . fst) fs
|
||||
_ -> v
|
||||
---- TODO: accept subtypes
|
||||
---- TODO: use a trie
|
||||
lookupOverloadInstance tys typs =
|
||||
[((mkFunType rest val, t),isExact) |
|
||||
let lt = length tys,
|
||||
(ty,(val,t)) <- typs, length ty >= lt,
|
||||
let (pre,rest) = splitAt lt ty,
|
||||
let isExact = pre == tys,
|
||||
isExact || map unlocked pre == map unlocked tys
|
||||
]
|
||||
|
||||
noProds vfs = [(v,f) | (v,f) <- vfs, noProd v]
|
||||
|
||||
noProd ty = case ty of
|
||||
Prod _ _ _ _ -> False
|
||||
_ -> True
|
||||
|
||||
checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
|
||||
checkLType gr g trm typ0 = do
|
||||
|
||||
typ <- computeLType gr g typ0
|
||||
|
||||
case trm of
|
||||
|
||||
Abs bt x c -> do
|
||||
case typ of
|
||||
Prod bt' z a b -> do
|
||||
(c',b') <- if isWildIdent z
|
||||
then checkLType gr ((bt,x,a):g) c b
|
||||
else do b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
|
||||
checkLType gr ((bt,x,a):g) c b'
|
||||
return $ (Abs bt x c', Prod bt' x a b')
|
||||
_ -> checkError $ text "function type expected instead of" <+> ppType typ
|
||||
|
||||
App f a -> do
|
||||
over <- getOverload gr g (Just typ) trm
|
||||
case over of
|
||||
Just trty -> return trty
|
||||
_ -> do
|
||||
(trm',ty') <- inferLType gr g trm
|
||||
termWith trm' $ checkEqLType gr g typ ty' trm'
|
||||
|
||||
Q _ _ -> do
|
||||
over <- getOverload gr g (Just typ) trm
|
||||
case over of
|
||||
Just trty -> return trty
|
||||
_ -> do
|
||||
(trm',ty') <- inferLType gr g trm
|
||||
termWith trm' $ checkEqLType gr g typ ty' trm'
|
||||
|
||||
T _ [] ->
|
||||
checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ)
|
||||
T _ cs -> case typ of
|
||||
Table arg val -> do
|
||||
case allParamValues gr arg of
|
||||
Ok vs -> do
|
||||
let ps0 = map fst cs
|
||||
ps <- checkErr $ testOvershadow ps0 vs
|
||||
if null ps
|
||||
then return ()
|
||||
else checkWarn (text "patterns never reached:" $$
|
||||
nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
|
||||
_ -> return () -- happens with variable types
|
||||
cs' <- mapM (checkCase arg val) cs
|
||||
return (T (TTyped arg) cs', typ)
|
||||
_ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType typ)
|
||||
|
||||
R r -> case typ of --- why needed? because inference may be too difficult
|
||||
RecType rr -> do
|
||||
let (ls,_) = unzip rr -- labels of expected type
|
||||
fsts <- mapM (checkM r) rr -- check that they are found in the record
|
||||
return $ (R fsts, typ) -- normalize record
|
||||
|
||||
_ -> checkError (text "record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
|
||||
|
||||
ExtR r s -> case typ of
|
||||
_ | typ == typeType -> do
|
||||
trm' <- computeLType gr g trm
|
||||
case trm' of
|
||||
RecType _ -> termWith trm $ return typeType
|
||||
ExtR (Vr _) (RecType _) -> termWith trm $ return typeType
|
||||
-- ext t = t ** ...
|
||||
_ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
|
||||
RecType rr -> do
|
||||
(r',ty,s') <- checks [
|
||||
do (r',ty) <- inferLType gr g r
|
||||
return (r',ty,s)
|
||||
,
|
||||
do (s',ty) <- inferLType gr g s
|
||||
return (s',ty,r)
|
||||
]
|
||||
case ty of
|
||||
RecType rr1 -> do
|
||||
let (rr0,rr2) = recParts rr rr1
|
||||
r2 <- justCheck g r' rr0
|
||||
s2 <- justCheck g s' rr2
|
||||
return $ (ExtR r2 s2, typ)
|
||||
_ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$
|
||||
text "but found" <+> ppTerm Unqualified 0 ty)
|
||||
|
||||
ExtR ty ex -> do
|
||||
r' <- justCheck g r ty
|
||||
s' <- justCheck g s ex
|
||||
return $ (ExtR r' s', typ) --- is this all?
|
||||
|
||||
_ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
|
||||
|
||||
FV vs -> do
|
||||
ttys <- mapM (flip (checkLType gr g) typ) vs
|
||||
--- checkIfComplexVariantType trm typ
|
||||
return (FV (map fst ttys), typ) --- typ' ?
|
||||
|
||||
S tab arg -> checks [ do
|
||||
(tab',ty) <- inferLType gr g tab
|
||||
ty' <- computeLType gr g ty
|
||||
case ty' of
|
||||
Table p t -> do
|
||||
(arg',val) <- checkLType gr g arg p
|
||||
checkEqLType gr g typ t trm
|
||||
return (S tab' arg', t)
|
||||
_ -> checkError (text "table type expected for applied table instead of" <+> ppType ty')
|
||||
, do
|
||||
(arg',ty) <- inferLType gr g arg
|
||||
ty' <- computeLType gr g ty
|
||||
(tab',_) <- checkLType gr g tab (Table ty' typ)
|
||||
return (S tab' arg', typ)
|
||||
]
|
||||
Let (x,(mty,def)) body -> case mty of
|
||||
Just ty -> do
|
||||
(def',ty') <- checkLType gr g def ty
|
||||
body' <- justCheck ((Explicit,x,ty'):g) body typ
|
||||
return (Let (x,(Just ty',def')) body', typ)
|
||||
_ -> do
|
||||
(def',ty) <- inferLType gr g def -- tries to infer type of local constant
|
||||
checkLType gr g (Let (x,(Just ty,def')) body) typ
|
||||
|
||||
ELin c tr -> do
|
||||
tr1 <- checkErr $ unlockRecord c tr
|
||||
checkLType gr g tr1 typ
|
||||
|
||||
_ -> do
|
||||
(trm',ty') <- inferLType gr g trm
|
||||
termWith trm' $ checkEqLType gr g typ ty' trm'
|
||||
where
|
||||
justCheck g ty te = checkLType gr g ty te >>= return . fst
|
||||
|
||||
recParts rr t = (RecType rr1,RecType rr2) where
|
||||
(rr1,rr2) = partition (flip elem (map fst t) . fst) rr
|
||||
|
||||
checkM rms (l,ty) = case lookup l rms of
|
||||
Just (Just ty0,t) -> do
|
||||
checkEqLType gr g ty ty0 t
|
||||
(t',ty') <- checkLType gr g t ty
|
||||
return (l,(Just ty',t'))
|
||||
Just (_,t) -> do
|
||||
(t',ty') <- checkLType gr g t ty
|
||||
return (l,(Just ty',t'))
|
||||
_ -> checkError $
|
||||
if isLockLabel l
|
||||
then let cat = drop 5 (showIdent (label2ident l))
|
||||
in ppTerm Unqualified 0 (R rms) <+> text "is not in the lincat of" <+> text cat <>
|
||||
text "; try wrapping it with lin" <+> text cat
|
||||
else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
|
||||
|
||||
checkCase arg val (p,t) = do
|
||||
cont <- pattContext gr g arg p
|
||||
t' <- justCheck (reverse cont ++ g) t val
|
||||
return (p,t')
|
||||
|
||||
pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
|
||||
pattContext env g typ p = case p of
|
||||
PV x -> return [(Explicit,x,typ)]
|
||||
PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
|
||||
t <- checkErr $ lookupResType env q c
|
||||
let (cont,v) = typeFormCnc t
|
||||
checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
|
||||
(length cont == length ps)
|
||||
checkEqLType env g typ v (patt2term p)
|
||||
mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
|
||||
PR r -> do
|
||||
typ' <- computeLType env g typ
|
||||
case typ' of
|
||||
RecType t -> do
|
||||
let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
|
||||
----- checkWarn $ prt p ++++ show pts ----- debug
|
||||
mapM (uncurry (pattContext env g)) pts >>= return . concat
|
||||
_ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
|
||||
PT t p' -> do
|
||||
checkEqLType env g typ t (patt2term p')
|
||||
pattContext env g typ p'
|
||||
|
||||
PAs x p -> do
|
||||
g' <- pattContext env g typ p
|
||||
return ((Explicit,x,typ):g')
|
||||
|
||||
PAlt p' q -> do
|
||||
g1 <- pattContext env g typ p'
|
||||
g2 <- pattContext env g typ q
|
||||
let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
|
||||
checkCond
|
||||
(text "incompatible bindings of" <+>
|
||||
fsep (map ppIdent pts) <+>
|
||||
text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
|
||||
return g1 -- must be g1 == g2
|
||||
PSeq p q -> do
|
||||
g1 <- pattContext env g typ p
|
||||
g2 <- pattContext env g typ q
|
||||
return $ g1 ++ g2
|
||||
PRep p' -> noBind typeStr p'
|
||||
PNeg p' -> noBind typ p'
|
||||
|
||||
_ -> return [] ---- check types!
|
||||
where
|
||||
noBind typ p' = do
|
||||
co <- pattContext env g typ p'
|
||||
if not (null co)
|
||||
then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
|
||||
>> return []
|
||||
else return []
|
||||
|
||||
checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type
|
||||
checkEqLType gr g t u trm = do
|
||||
(b,t',u',s) <- checkIfEqLType gr g t u trm
|
||||
case b of
|
||||
True -> return t'
|
||||
False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
|
||||
text "expected:" <+> ppType t $$
|
||||
text "inferred:" <+> ppType u
|
||||
|
||||
checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
|
||||
checkIfEqLType gr g t u trm = do
|
||||
t' <- computeLType gr g t
|
||||
u' <- computeLType gr g u
|
||||
case t' == u' || alpha [] t' u' of
|
||||
True -> return (True,t',u',[])
|
||||
-- forgive missing lock fields by only generating a warning.
|
||||
--- better: use a flag to forgive? (AR 31/1/2006)
|
||||
_ -> case missingLock [] t' u' of
|
||||
Ok lo -> do
|
||||
checkWarn $ text "missing lock field" <+> fsep (map ppLabel lo)
|
||||
return (True,t',u',[])
|
||||
Bad s -> return (False,t',u',s)
|
||||
|
||||
where
|
||||
|
||||
-- t is a subtype of u
|
||||
--- quick hack version of TC.eqVal
|
||||
alpha g t u = case (t,u) of
|
||||
|
||||
-- error (the empty type!) is subtype of any other type
|
||||
(_,u) | u == typeError -> True
|
||||
|
||||
-- contravariance
|
||||
(Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d
|
||||
|
||||
-- record subtyping
|
||||
(RecType rs, RecType ts) -> all (\ (l,a) ->
|
||||
any (\ (k,b) -> alpha g a b && l == k) ts) rs
|
||||
(ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s'
|
||||
(ExtR r s, t) -> alpha g r t || alpha g s t
|
||||
|
||||
-- the following say that Ints n is a subset of Int and of Ints m >= n
|
||||
(t,u) | Just m <- isTypeInts t, Just n <- isTypeInts t -> m >= n
|
||||
| Just _ <- isTypeInts t, u == typeInt -> True ---- check size!
|
||||
| t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
|
||||
|
||||
---- this should be made in Rename
|
||||
(Q m a, Q n b) | a == b -> elem m (allExtendsPlus gr n)
|
||||
|| elem n (allExtendsPlus gr m)
|
||||
|| m == n --- for Predef
|
||||
(QC m a, QC n b) | a == b -> elem m (allExtendsPlus gr n)
|
||||
|| elem n (allExtendsPlus gr m)
|
||||
(QC m a, Q n b) | a == b -> elem m (allExtendsPlus gr n)
|
||||
|| elem n (allExtendsPlus gr m)
|
||||
(Q m a, QC n b) | a == b -> elem m (allExtendsPlus gr n)
|
||||
|| elem n (allExtendsPlus gr m)
|
||||
|
||||
(Table a b, Table c d) -> alpha g a c && alpha g b d
|
||||
(Vr x, Vr y) -> x == y || elem (x,y) g || elem (y,x) g
|
||||
_ -> t == u
|
||||
--- the following should be one-way coercions only. AR 4/1/2001
|
||||
|| elem t sTypes && elem u sTypes
|
||||
|| (t == typeType && u == typePType)
|
||||
|| (u == typeType && t == typePType)
|
||||
|
||||
missingLock g t u = case (t,u) of
|
||||
(RecType rs, RecType ts) ->
|
||||
let
|
||||
ls = [l | (l,a) <- rs,
|
||||
not (any (\ (k,b) -> alpha g a b && l == k) ts)]
|
||||
(locks,others) = partition isLockLabel ls
|
||||
in case others of
|
||||
_:_ -> Bad $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others)))
|
||||
_ -> return locks
|
||||
-- contravariance
|
||||
(Prod _ x a b, Prod _ y c d) -> do
|
||||
ls1 <- missingLock g c a
|
||||
ls2 <- missingLock g b d
|
||||
return $ ls1 ++ ls2
|
||||
|
||||
_ -> Bad ""
|
||||
|
||||
sTypes = [typeStr, typeTok, typeString]
|
||||
|
||||
-- auxiliaries
|
||||
|
||||
-- | light-weight substitution for dep. types
|
||||
substituteLType :: Context -> Type -> Check Type
|
||||
substituteLType g t = case t of
|
||||
Vr x -> return $ maybe t id $ lookup x [(x,t) | (_,x,t) <- g]
|
||||
_ -> composOp (substituteLType g) t
|
||||
|
||||
termWith :: Term -> Check Type -> Check (Term, Type)
|
||||
termWith t ct = do
|
||||
ty <- ct
|
||||
return (t,ty)
|
||||
|
||||
-- | compositional check\/infer of binary operations
|
||||
check2 :: (Term -> Check Term) -> (Term -> Term -> Term) ->
|
||||
Term -> Term -> Type -> Check (Term,Type)
|
||||
check2 chk con a b t = do
|
||||
a' <- chk a
|
||||
b' <- chk b
|
||||
return (con a' b', t)
|
||||
|
||||
-- printing a type with a lock field lock_C as C
|
||||
ppType :: Type -> Doc
|
||||
ppType ty =
|
||||
case ty of
|
||||
RecType fs -> case filter isLockLabel $ map fst fs of
|
||||
[lock] -> text (drop 5 (showIdent (label2ident lock)))
|
||||
_ -> ppTerm Unqualified 0 ty
|
||||
Prod _ x a b -> ppType a <+> text "->" <+> ppType b
|
||||
_ -> ppTerm Unqualified 0 ty
|
||||
|
||||
checkLookup :: Ident -> Context -> Check Type
|
||||
checkLookup x g =
|
||||
case [ty | (b,y,ty) <- g, x == y] of
|
||||
[] -> checkError (text "unknown variable" <+> ppIdent x)
|
||||
(ty:_) -> return ty
|
||||
Reference in New Issue
Block a user