forked from GitHub/gf-core
move GF.Devel.TC and GF.Devel.TypeCheck to GF.Compile.*
This commit is contained in:
kr.angelov
@@ -24,20 +24,19 @@
|
||||
module GF.Compile.CheckGrammar (
|
||||
showCheckModule, justCheckLTerm, allOperDependencies, topoSortOpers) where
|
||||
|
||||
import GF.Grammar.Grammar
|
||||
import GF.Infra.Ident
|
||||
import GF.Infra.Modules
|
||||
import GF.Grammar.Refresh ----
|
||||
|
||||
import GF.Devel.TypeCheck
|
||||
import GF.Grammar.Predef (cPredef, cPredefAbs) ---
|
||||
import GF.Compile.TypeCheck
|
||||
|
||||
import GF.Grammar.Refresh
|
||||
import GF.Grammar.Grammar
|
||||
import GF.Grammar.PrGrammar
|
||||
import GF.Grammar.Lookup
|
||||
import GF.Grammar.LookAbs
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.Macros
|
||||
import GF.Grammar.ReservedWords ----
|
||||
import GF.Grammar.ReservedWords
|
||||
import GF.Grammar.PatternMatch
|
||||
import GF.Grammar.AppPredefined
|
||||
import GF.Grammar.Lockfield (isLockLabel)
|
||||
|
||||
292
src-3.0/GF/Compile/TC.hs
Normal file
292
src-3.0/GF/Compile/TC.hs
Normal file
@@ -0,0 +1,292 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : TC
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/10/02 20:50:19 $
|
||||
-- > CVS $Author: aarne $
|
||||
-- > CVS $Revision: 1.11 $
|
||||
--
|
||||
-- Thierry Coquand's type checking algorithm that creates a trace
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module GF.Compile.TC (AExp(..),
|
||||
Theory,
|
||||
checkExp,
|
||||
inferExp,
|
||||
checkEqs,
|
||||
eqVal,
|
||||
whnf
|
||||
) where
|
||||
|
||||
import GF.Data.Operations
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.Abstract
|
||||
|
||||
import Control.Monad
|
||||
import Data.List (sortBy)
|
||||
|
||||
data AExp =
|
||||
AVr Ident Val
|
||||
| ACn QIdent Val
|
||||
| AType
|
||||
| AInt Integer
|
||||
| AFloat Double
|
||||
| AStr String
|
||||
| AMeta MetaSymb Val
|
||||
| AApp AExp AExp Val
|
||||
| AAbs Ident Val AExp
|
||||
| AProd Ident AExp AExp
|
||||
| AEqs [([Exp],AExp)] --- not used
|
||||
| AData Val
|
||||
deriving (Eq,Show)
|
||||
|
||||
type Theory = QIdent -> Err Val
|
||||
|
||||
lookupConst :: Theory -> QIdent -> Err Val
|
||||
lookupConst th f = th f
|
||||
|
||||
lookupVar :: Env -> Ident -> Err Val
|
||||
lookupVar g x = maybe (prtBad "unknown variable" x) return $ lookup x ((IW,uVal):g)
|
||||
-- wild card IW: no error produced, ?0 instead.
|
||||
|
||||
type TCEnv = (Int,Env,Env)
|
||||
|
||||
emptyTCEnv :: TCEnv
|
||||
emptyTCEnv = (0,[],[])
|
||||
|
||||
whnf :: Val -> Err Val
|
||||
whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
|
||||
case v of
|
||||
VApp u w -> do
|
||||
u' <- whnf u
|
||||
w' <- whnf w
|
||||
app u' w'
|
||||
VClos env e -> eval env e
|
||||
_ -> return v
|
||||
|
||||
app :: Val -> Val -> Err Val
|
||||
app u v = case u of
|
||||
VClos env (Abs x e) -> eval ((x,v):env) e
|
||||
_ -> return $ VApp u v
|
||||
|
||||
eval :: Env -> Exp -> Err Val
|
||||
eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
|
||||
case e of
|
||||
Vr x -> lookupVar env x
|
||||
Q m c -> return $ VCn (m,c)
|
||||
QC m c -> return $ VCn (m,c) ---- == Q ?
|
||||
Sort c -> return $ VType --- the only sort is Type
|
||||
App f a -> join $ liftM2 app (eval env f) (eval env a)
|
||||
_ -> return $ VClos env e
|
||||
|
||||
eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
|
||||
eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
|
||||
do
|
||||
w1 <- whnf u1
|
||||
w2 <- whnf u2
|
||||
let v = VGen k
|
||||
case (w1,w2) of
|
||||
(VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
|
||||
(VClos env1 (Abs x1 e1), VClos env2 (Abs x2 e2)) ->
|
||||
eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
|
||||
(VClos env1 (Prod x1 a1 e1), VClos env2 (Prod x2 a2 e2)) ->
|
||||
liftM2 (++)
|
||||
(eqVal k (VClos env1 a1) (VClos env2 a2))
|
||||
(eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
|
||||
(VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
|
||||
(VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j]
|
||||
--- thus ignore qualifications; valid because inheritance cannot
|
||||
--- be qualified. Simplifies annotation. AR 17/3/2005
|
||||
_ -> return [(w1,w2) | w1 /= w2]
|
||||
-- invariant: constraints are in whnf
|
||||
|
||||
checkType :: Theory -> TCEnv -> Exp -> Err (AExp,[(Val,Val)])
|
||||
checkType th tenv e = checkExp th tenv e vType
|
||||
|
||||
checkExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
|
||||
checkExp th tenv@(k,rho,gamma) e ty = do
|
||||
typ <- whnf ty
|
||||
let v = VGen k
|
||||
case e of
|
||||
Meta m -> return $ (AMeta m typ,[])
|
||||
EData -> return $ (AData typ,[])
|
||||
|
||||
Abs x t -> case typ of
|
||||
VClos env (Prod y a b) -> do
|
||||
a' <- whnf $ VClos env a ---
|
||||
(t',cs) <- checkExp th
|
||||
(k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
|
||||
return (AAbs x a' t', cs)
|
||||
_ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
|
||||
|
||||
-- {- --- to get deprec when checkEqs works (15/9/2005)
|
||||
Eqs es -> do
|
||||
bcs <- mapM (\b -> checkBranch th tenv b typ) es
|
||||
let (bs,css) = unzip bcs
|
||||
return (AEqs bs, concat css)
|
||||
-- - }
|
||||
Prod x a b -> do
|
||||
testErr (typ == vType) "expected Type"
|
||||
(a',csa) <- checkType th tenv a
|
||||
(b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
|
||||
return (AProd x a' b', csa ++ csb)
|
||||
|
||||
_ -> checkInferExp th tenv e typ
|
||||
|
||||
checkInferExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
|
||||
checkInferExp th tenv@(k,_,_) e typ = do
|
||||
(e',w,cs1) <- inferExp th tenv e
|
||||
cs2 <- eqVal k w typ
|
||||
return (e',cs1 ++ cs2)
|
||||
|
||||
inferExp :: Theory -> TCEnv -> Exp -> Err (AExp, Val, [(Val,Val)])
|
||||
inferExp th tenv@(k,rho,gamma) e = case e of
|
||||
Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
|
||||
Q m c | m == cPredefAbs && isPredefCat c
|
||||
-> return (ACn (m,c) vType, vType, [])
|
||||
| otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
|
||||
QC m c -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c) ----
|
||||
EInt i -> return (AInt i, valAbsInt, [])
|
||||
EFloat i -> return (AFloat i, valAbsFloat, [])
|
||||
K i -> return (AStr i, valAbsString, [])
|
||||
Sort _ -> return (AType, vType, [])
|
||||
App f t -> do
|
||||
(f',w,csf) <- inferExp th tenv f
|
||||
typ <- whnf w
|
||||
case typ of
|
||||
VClos env (Prod x a b) -> do
|
||||
(a',csa) <- checkExp th tenv t (VClos env a)
|
||||
b' <- whnf $ VClos ((x,VClos rho t):env) b
|
||||
return $ (AApp f' a' b', b', csf ++ csa)
|
||||
_ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
|
||||
_ -> prtBad "cannot infer type of expression" e
|
||||
|
||||
checkEqs :: Theory -> TCEnv -> (Fun,Trm) -> Val -> Err [(Val,Val)]
|
||||
checkEqs th tenv@(k,rho,gamma) (fun@(m,f),def) val = case def of
|
||||
Eqs es -> liftM concat $ mapM checkBranch es
|
||||
_ -> liftM snd $ checkExp th tenv def val
|
||||
where
|
||||
checkBranch (ps,df) =
|
||||
let
|
||||
(ps',_,vars) = foldr p2t ([],0,[]) ps
|
||||
fps = mkApp (Q m f) ps'
|
||||
in errIn ("branch" +++ prt fps) $ do
|
||||
(aexp, typ, cs1) <- inferExp th tenv fps
|
||||
let
|
||||
bds = binds vars aexp
|
||||
tenv' = (k, rho, bds ++ gamma)
|
||||
(_,cs2) <- errIn (show bds) $ checkExp th tenv' df typ
|
||||
return $ (cs1 ++ cs2)
|
||||
p2t p (ps,i,g) = case p of
|
||||
PW -> (Meta (MetaSymb i) : ps, i+1, g)
|
||||
PV IW -> (Meta (MetaSymb i) : ps, i+1, g)
|
||||
PV x -> (Meta (MetaSymb i) : ps, i+1,upd x i g)
|
||||
PString s -> ( K s : ps, i, g)
|
||||
PInt n -> (EInt n : ps, i, g)
|
||||
PFloat n -> (EFloat n : ps, i, g)
|
||||
PP m c xs -> (mkApp (qq (m,c)) xss : ps, i', g')
|
||||
where (xss,i',g') = foldr p2t ([],i,g) xs
|
||||
_ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
|
||||
upd x i g = (x,i) : g --- to annotate pattern variables: treat as metas
|
||||
|
||||
-- notice: in vars, the sequence 0.. is sorted. In subst aexp, all
|
||||
-- this occurs and nothing else.
|
||||
binds vars aexp = [(x,v) | ((x,_),v) <- zip vars metas] where
|
||||
metas = map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ subst aexp
|
||||
subst aexp = case aexp of
|
||||
AMeta (MetaSymb i) v -> [(i,v)]
|
||||
AApp c a _ -> subst c ++ subst a
|
||||
_ -> [] -- never matter in patterns
|
||||
|
||||
checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
|
||||
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
|
||||
chB tenv' ps' ty
|
||||
where
|
||||
|
||||
(ps',_,rho2,k') = ps2ts k ps
|
||||
tenv' = (k, rho2++rho, gamma) ---- k' ?
|
||||
(k,rho,gamma) = tenv
|
||||
|
||||
chB tenv@(k,rho,gamma) ps ty = case ps of
|
||||
p:ps2 -> do
|
||||
typ <- whnf ty
|
||||
case typ of
|
||||
VClos env (Prod y a b) -> do
|
||||
a' <- whnf $ VClos env a
|
||||
(p', sigma, binds, cs1) <- checkP tenv p y a'
|
||||
let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
|
||||
((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b)
|
||||
return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
|
||||
_ -> prtBad ("Product expected for definiens" +++prt t +++ "instead of") typ
|
||||
[] -> do
|
||||
(e,cs) <- checkExp th tenv t ty
|
||||
return (([],e),cs)
|
||||
checkP env@(k,rho,gamma) t x a = do
|
||||
(delta,cs) <- checkPatt th env t a
|
||||
let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
|
||||
return (VClos sigma t, sigma, delta, cs)
|
||||
|
||||
ps2ts k = foldr p2t ([],0,[],k)
|
||||
p2t p (ps,i,g,k) = case p of
|
||||
PW -> (Meta (MetaSymb i) : ps, i+1,g,k)
|
||||
PV IW -> (Meta (MetaSymb i) : ps, i+1,g,k)
|
||||
PV x -> (Vr x : ps, i, upd x k g,k+1)
|
||||
PString s -> (K s : ps, i, g, k)
|
||||
PInt n -> (EInt n : ps, i, g, k)
|
||||
PFloat n -> (EFloat n : ps, i, g, k)
|
||||
PP m c xs -> (mkApp (qq (m,c)) xss : ps, j, g',k')
|
||||
where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
|
||||
_ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
|
||||
|
||||
upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables
|
||||
|
||||
|
||||
checkPatt :: Theory -> TCEnv -> Exp -> Val -> Err (Binds,[(Val,Val)])
|
||||
checkPatt th tenv exp val = do
|
||||
(aexp,_,cs) <- checkExpP tenv exp val
|
||||
let binds = extrBinds aexp
|
||||
return (binds,cs)
|
||||
where
|
||||
extrBinds aexp = case aexp of
|
||||
AVr i v -> [(i,v)]
|
||||
AApp f a _ -> extrBinds f ++ extrBinds a
|
||||
_ -> [] -- no other cases are possible
|
||||
|
||||
--- ad hoc, to find types of variables
|
||||
checkExpP tenv@(k,rho,gamma) exp val = case exp of
|
||||
Meta m -> return $ (AMeta m val, val, [])
|
||||
Vr x -> return $ (AVr x val, val, [])
|
||||
EInt i -> return (AInt i, valAbsInt, [])
|
||||
EFloat i -> return (AFloat i, valAbsFloat, [])
|
||||
K s -> return (AStr s, valAbsString, [])
|
||||
|
||||
Q m c -> do
|
||||
typ <- lookupConst th (m,c)
|
||||
return $ (ACn (m,c) typ, typ, [])
|
||||
QC m c -> do
|
||||
typ <- lookupConst th (m,c)
|
||||
return $ (ACn (m,c) typ, typ, []) ----
|
||||
App f t -> do
|
||||
(f',w,csf) <- checkExpP tenv f val
|
||||
typ <- whnf w
|
||||
case typ of
|
||||
VClos env (Prod x a b) -> do
|
||||
(a',_,csa) <- checkExpP tenv t (VClos env a)
|
||||
b' <- whnf $ VClos ((x,VClos rho t):env) b
|
||||
return $ (AApp f' a' b', b', csf ++ csa)
|
||||
_ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
|
||||
_ -> prtBad "cannot typecheck pattern" exp
|
||||
|
||||
-- auxiliaries
|
||||
|
||||
noConstr :: Err Val -> Err (Val,[(Val,Val)])
|
||||
noConstr er = er >>= (\v -> return (v,[]))
|
||||
|
||||
mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)])
|
||||
mkAnnot a ti = do
|
||||
(v,cs) <- ti
|
||||
return (a v, v, cs)
|
||||
|
||||
118
src-3.0/GF/Compile/TypeCheck.hs
Normal file
118
src-3.0/GF/Compile/TypeCheck.hs
Normal file
@@ -0,0 +1,118 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : TypeCheck
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/09/15 16:22:02 $
|
||||
-- > CVS $Author: aarne $
|
||||
-- > CVS $Revision: 1.16 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module GF.Compile.TypeCheck (-- * top-level type checking functions; TC should not be called directly.
|
||||
checkContext,
|
||||
checkTyp,
|
||||
checkEquation,
|
||||
checkConstrs,
|
||||
) where
|
||||
|
||||
import GF.Data.Operations
|
||||
import GF.Data.Zipper
|
||||
|
||||
import GF.Grammar.Abstract
|
||||
import GF.Grammar.Refresh
|
||||
import GF.Grammar.LookAbs
|
||||
import qualified GF.Grammar.Lookup as Lookup ---
|
||||
import GF.Grammar.Unify ---
|
||||
|
||||
import GF.Compile.TC
|
||||
|
||||
import Control.Monad (foldM, liftM, liftM2)
|
||||
import Data.List (nub) ---
|
||||
|
||||
-- | invariant way of creating TCEnv from context
|
||||
initTCEnv gamma =
|
||||
(length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma)
|
||||
|
||||
-- interface to TC type checker
|
||||
|
||||
type2val :: Type -> Val
|
||||
type2val = VClos []
|
||||
|
||||
aexp2tree :: (AExp,[(Val,Val)]) -> Err Tree
|
||||
aexp2tree (aexp,cs) = do
|
||||
(bi,at,vt,ts) <- treeForm aexp
|
||||
ts' <- mapM aexp2tree [(t,[]) | t <- ts]
|
||||
return $ Tr (N (bi,at,vt,(cs,[]),False),ts')
|
||||
where
|
||||
treeForm a = case a of
|
||||
AAbs x v b -> do
|
||||
(bi, at, vt, args) <- treeForm b
|
||||
v' <- whnf v ---- should not be needed...
|
||||
return ((x,v') : bi, at, vt, args)
|
||||
AApp c a v -> do
|
||||
(_,at,_,args) <- treeForm c
|
||||
v' <- whnf v ----
|
||||
return ([],at,v',args ++ [a])
|
||||
AVr x v -> do
|
||||
v' <- whnf v ----
|
||||
return ([],AtV x,v',[])
|
||||
ACn c v -> do
|
||||
v' <- whnf v ----
|
||||
return ([],AtC c,v',[])
|
||||
AInt i -> do
|
||||
return ([],AtI i,valAbsInt,[])
|
||||
AFloat i -> do
|
||||
return ([],AtF i,valAbsFloat,[])
|
||||
AStr s -> do
|
||||
return ([],AtL s,valAbsString,[])
|
||||
AMeta m v -> do
|
||||
v' <- whnf v ----
|
||||
return ([],AtM m,v',[])
|
||||
_ -> Bad "illegal tree" -- AProd
|
||||
|
||||
cont2exp :: Context -> Exp
|
||||
cont2exp c = mkProd (c, eType, []) -- to check a context
|
||||
|
||||
cont2val :: Context -> Val
|
||||
cont2val = type2val . cont2exp
|
||||
|
||||
-- some top-level batch-mode checkers for the compiler
|
||||
|
||||
justTypeCheck :: Grammar -> Exp -> Val -> Err Constraints
|
||||
justTypeCheck gr e v = do
|
||||
(_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
|
||||
return $ filter notJustMeta constrs0
|
||||
---- return $ fst $ splitConstraintsSrc gr constrs0
|
||||
---- this change was to force proper tc of abstract modules.
|
||||
---- May not be quite right. AR 13/9/2005
|
||||
|
||||
notJustMeta (c,k) = case (c,k) of
|
||||
(VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
|
||||
_ -> True
|
||||
|
||||
grammar2theory :: Grammar -> Theory
|
||||
grammar2theory gr (m,f) = case lookupFunType gr m f of
|
||||
Ok t -> return $ type2val t
|
||||
Bad s -> case lookupCatContext gr m f of
|
||||
Ok cont -> return $ cont2val cont
|
||||
_ -> Bad s
|
||||
|
||||
checkContext :: Grammar -> Context -> [String]
|
||||
checkContext st = checkTyp st . cont2exp
|
||||
|
||||
checkTyp :: Grammar -> Type -> [String]
|
||||
checkTyp gr typ = err singleton prConstrs $ justTypeCheck gr typ vType
|
||||
|
||||
checkEquation :: Grammar -> Fun -> Trm -> [String]
|
||||
checkEquation gr (m,fun) def = err singleton id $ do
|
||||
typ <- lookupFunType gr m fun
|
||||
cs <- justTypeCheck gr def (vClos typ)
|
||||
let cs1 = filter notJustMeta cs
|
||||
return $ ifNull [] (singleton . prConstraints) cs1
|
||||
|
||||
checkConstrs :: Grammar -> Cat -> [Ident] -> [String]
|
||||
checkConstrs gr cat _ = [] ---- check constructors!
|
||||
Reference in New Issue
Block a user