mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 03:32:51 -06:00
Sketch of the new type checker for the concrete syntax. Enabled only with -new-comp
This commit is contained in:
@@ -23,9 +23,11 @@
|
|||||||
module GF.Compile.CheckGrammar(checkModule) where
|
module GF.Compile.CheckGrammar(checkModule) where
|
||||||
|
|
||||||
import GF.Infra.Ident
|
import GF.Infra.Ident
|
||||||
|
import GF.Infra.Option
|
||||||
|
|
||||||
import GF.Compile.TypeCheck.Abstract
|
import GF.Compile.TypeCheck.Abstract
|
||||||
import GF.Compile.TypeCheck.Concrete
|
import GF.Compile.TypeCheck.Concrete
|
||||||
|
import qualified GF.Compile.TypeCheck.ConcreteNew as CN
|
||||||
|
|
||||||
import GF.Grammar
|
import GF.Grammar
|
||||||
import GF.Grammar.Lexer
|
import GF.Grammar.Lexer
|
||||||
@@ -42,8 +44,8 @@ import Control.Monad
|
|||||||
import Text.PrettyPrint
|
import Text.PrettyPrint
|
||||||
|
|
||||||
-- | checking is performed in the dependency order of modules
|
-- | checking is performed in the dependency order of modules
|
||||||
checkModule :: [SourceModule] -> SourceModule -> Check SourceModule
|
checkModule :: Options -> [SourceModule] -> SourceModule -> Check SourceModule
|
||||||
checkModule mos mo@(m,mi) = do
|
checkModule opts mos mo@(m,mi) = do
|
||||||
checkRestrictedInheritance mos mo
|
checkRestrictedInheritance mos mo
|
||||||
mo <- case mtype mi of
|
mo <- case mtype mi of
|
||||||
MTConcrete a -> do let gr = mGrammar (mo:mos)
|
MTConcrete a -> do let gr = mGrammar (mo:mos)
|
||||||
@@ -54,7 +56,7 @@ checkModule mos mo@(m,mi) = do
|
|||||||
foldM updateCheckInfo mo infos
|
foldM updateCheckInfo mo infos
|
||||||
where
|
where
|
||||||
updateCheckInfo mo@(m,mi) (i,info) = do
|
updateCheckInfo mo@(m,mi) (i,info) = do
|
||||||
info <- checkInfo mos mo i info
|
info <- checkInfo opts mos mo i info
|
||||||
return (m,mi{jments=updateTree (i,info) (jments mi)})
|
return (m,mi{jments=updateTree (i,info) (jments mi)})
|
||||||
|
|
||||||
-- check if restricted inheritance modules are still coherent
|
-- check if restricted inheritance modules are still coherent
|
||||||
@@ -150,8 +152,8 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = checkIn (ppLocation (msrc cnc) NoLoc
|
|||||||
|
|
||||||
-- | General Principle: only Just-values are checked.
|
-- | General Principle: only Just-values are checked.
|
||||||
-- A May-value has always been checked in its origin module.
|
-- A May-value has always been checked in its origin module.
|
||||||
checkInfo :: [SourceModule] -> SourceModule -> Ident -> Info -> Check Info
|
checkInfo :: Options -> [SourceModule] -> SourceModule -> Ident -> Info -> Check Info
|
||||||
checkInfo ms (m,mo) c info = do
|
checkInfo opts ms (m,mo) c info = do
|
||||||
checkIn (ppLocation (msrc mo) NoLoc <> colon) $
|
checkIn (ppLocation (msrc mo) NoLoc <> colon) $
|
||||||
checkReservedId c
|
checkReservedId c
|
||||||
case info of
|
case info of
|
||||||
@@ -211,11 +213,15 @@ checkInfo ms (m,mo) c info = do
|
|||||||
ty' <- chIn loct "operation" $
|
ty' <- chIn loct "operation" $
|
||||||
checkLType gr [] ty typeType >>= computeLType gr [] . fst
|
checkLType gr [] ty typeType >>= computeLType gr [] . fst
|
||||||
(de',_) <- chIn locd "operation" $
|
(de',_) <- chIn locd "operation" $
|
||||||
checkLType gr [] de ty'
|
(if flag optNewComp opts
|
||||||
|
then CN.checkLType gr de ty'
|
||||||
|
else checkLType gr [] de ty')
|
||||||
return (Just (L loct ty'), Just (L locd de'))
|
return (Just (L loct ty'), Just (L locd de'))
|
||||||
(Nothing , Just (L locd de)) -> do
|
(Nothing , Just (L locd de)) -> do
|
||||||
(de',ty') <- chIn locd "operation" $
|
(de',ty') <- chIn locd "operation" $
|
||||||
inferLType gr [] de
|
(if flag optNewComp opts
|
||||||
|
then CN.inferLType gr de
|
||||||
|
else inferLType gr [] de)
|
||||||
return (Just (L locd ty'), Just (L locd de'))
|
return (Just (L locd ty'), Just (L locd de'))
|
||||||
(Just (L loct ty), Nothing) -> do
|
(Just (L loct ty), Nothing) -> do
|
||||||
chIn loct "operation" $
|
chIn loct "operation" $
|
||||||
|
|||||||
36
src/compiler/GF/Compile/Compute/ConcreteNew.hs
Normal file
36
src/compiler/GF/Compile/Compute/ConcreteNew.hs
Normal file
@@ -0,0 +1,36 @@
|
|||||||
|
module GF.Compile.Compute.ConcreteNew ( Value(..), Env, eval, apply, value2term ) where
|
||||||
|
|
||||||
|
import GF.Grammar hiding (Env, VGen, VApp)
|
||||||
|
|
||||||
|
data Value
|
||||||
|
= VApp QIdent [Value]
|
||||||
|
| VGen Int [Value]
|
||||||
|
| VMeta MetaId Env [Value]
|
||||||
|
| VClosure Env Term
|
||||||
|
| VSort Ident
|
||||||
|
deriving Show
|
||||||
|
|
||||||
|
type Env = [(Ident,Value)]
|
||||||
|
|
||||||
|
eval :: Env -> Term -> Value
|
||||||
|
eval env (Vr x) = case lookup x env of
|
||||||
|
Just v -> v
|
||||||
|
Nothing -> error ("Unknown variable "++showIdent x)
|
||||||
|
eval env (Q x) = VApp x []
|
||||||
|
eval env (Meta i) = VMeta i env []
|
||||||
|
eval env t@(Prod _ _ _ _) = VClosure env t
|
||||||
|
eval env t@(Abs _ _ _) = VClosure env t
|
||||||
|
eval env (Sort s) = VSort s
|
||||||
|
eval env t = error (show t)
|
||||||
|
|
||||||
|
apply env t vs = undefined
|
||||||
|
|
||||||
|
value2term :: [Ident] -> Value -> Term
|
||||||
|
value2term xs (VApp f vs) = foldl App (Q f) (map (value2term xs) vs)
|
||||||
|
value2term xs (VGen j vs) = foldl App (Vr (reverse xs !! j)) (map (value2term xs) vs)
|
||||||
|
value2term xs (VMeta j env vs) = foldl App (Meta j) (map (value2term xs) vs)
|
||||||
|
value2term xs (VClosure env (Prod bt x t1 t2)) = Prod bt x (value2term xs (eval env t1))
|
||||||
|
(value2term (x:xs) (eval ((x,VGen (length xs) []) : env) t2))
|
||||||
|
value2term xs (VClosure env (Abs bt x t)) = Abs bt x (value2term (x:xs) (eval ((x,VGen (length xs) []) : env) t))
|
||||||
|
value2term xs (VSort s) = Sort s
|
||||||
|
value2term xs v = error (show v)
|
||||||
371
src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
Normal file
371
src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
Normal file
@@ -0,0 +1,371 @@
|
|||||||
|
module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where
|
||||||
|
|
||||||
|
import GF.Grammar hiding (Env, VGen, VApp)
|
||||||
|
import GF.Grammar.Lookup
|
||||||
|
import GF.Compile.Compute.ConcreteNew
|
||||||
|
import GF.Infra.CheckM
|
||||||
|
import GF.Infra.UseIO
|
||||||
|
import GF.Data.Operations
|
||||||
|
|
||||||
|
import Text.PrettyPrint
|
||||||
|
import Data.List (nub, (\\))
|
||||||
|
import qualified Data.IntMap as IntMap
|
||||||
|
import qualified Data.ByteString.Char8 as BS
|
||||||
|
|
||||||
|
import GF.Grammar.Parser
|
||||||
|
import System.IO
|
||||||
|
import Debug.Trace
|
||||||
|
|
||||||
|
checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
|
||||||
|
checkLType gr t ty = runTcM $ do
|
||||||
|
t <- checkSigma gr [] t (eval [] ty)
|
||||||
|
t <- zonkTerm t
|
||||||
|
return (t,ty)
|
||||||
|
|
||||||
|
inferLType :: SourceGrammar -> Term -> Check (Term, Type)
|
||||||
|
inferLType gr t = runTcM $ do
|
||||||
|
(t,ty) <- inferSigma gr [] t
|
||||||
|
t <- zonkTerm t
|
||||||
|
ty <- zonkTerm (value2term [] ty)
|
||||||
|
return (t,ty)
|
||||||
|
|
||||||
|
checkSigma :: SourceGrammar -> Scope -> Term -> Sigma -> TcM Term
|
||||||
|
checkSigma gr scope t sigma = do
|
||||||
|
(skol_tvs, rho) <- skolemise scope sigma
|
||||||
|
(t,rho) <- tcRho gr scope t (Just rho)
|
||||||
|
esc_tvs <- getFreeTyVars (sigma : map snd scope)
|
||||||
|
let bad_tvs = filter (`elem` esc_tvs) skol_tvs
|
||||||
|
if null bad_tvs
|
||||||
|
then return t
|
||||||
|
else tcError (text "Type not polymorphic enough")
|
||||||
|
|
||||||
|
inferSigma :: SourceGrammar -> Scope -> Term -> TcM (Term,Sigma)
|
||||||
|
inferSigma gr scope t = do
|
||||||
|
(t,ty) <- tcRho gr scope t Nothing
|
||||||
|
env_tvs <- getMetaVars [ty | (_,ty) <- scope]
|
||||||
|
res_tvs <- getMetaVars [ty]
|
||||||
|
let forall_tvs = res_tvs \\ env_tvs
|
||||||
|
quantify scope t forall_tvs ty
|
||||||
|
|
||||||
|
tcRho :: SourceGrammar -> Scope -> Term -> Maybe Rho -> TcM (Term, Rho)
|
||||||
|
tcRho gr scope t@(EInt _) mb_ty = instSigma scope t (eval [] typeInt) mb_ty
|
||||||
|
tcRho gr scope t@(EFloat _) mb_ty = instSigma scope t (eval [] typeFloat) mb_ty
|
||||||
|
tcRho gr scope t@(K _) mb_ty = instSigma scope t (eval [] typeString) mb_ty
|
||||||
|
tcRho gr scope t@(Empty) mb_ty = instSigma scope t (eval [] typeString) mb_ty
|
||||||
|
tcRho gr scope t@(Vr v) mb_ty = do
|
||||||
|
case lookup v scope of
|
||||||
|
Just v_sigma -> instSigma scope t v_sigma mb_ty
|
||||||
|
Nothing -> tcError (text "Unknown variable" <+> ppIdent v)
|
||||||
|
tcRho gr scope t@(Q id) mb_ty = do
|
||||||
|
case lookupResType gr id of
|
||||||
|
Ok ty -> instSigma scope t (eval [] ty) mb_ty
|
||||||
|
Bad err -> tcError (text err)
|
||||||
|
tcRho gr scope t@(QC id) mb_ty = do
|
||||||
|
case lookupResType gr id of
|
||||||
|
Ok ty -> instSigma scope t (eval [] ty) mb_ty
|
||||||
|
Bad err -> tcError (text err)
|
||||||
|
tcRho gr scope (App fun arg) mb_ty = do
|
||||||
|
(fun,fun_ty) <- tcRho gr scope fun Nothing
|
||||||
|
(arg_ty, res_ty) <- unifyFun scope fun_ty
|
||||||
|
arg <- checkSigma gr scope arg arg_ty
|
||||||
|
instSigma scope (App fun arg) res_ty mb_ty
|
||||||
|
tcRho gr scope (Abs bt var body) (Just ty) = do
|
||||||
|
trace (show ty) $ return ()
|
||||||
|
(var_ty, body_ty) <- unifyFun scope ty
|
||||||
|
(body, body_ty) <- tcRho gr ((var,var_ty):scope) body (Just body_ty)
|
||||||
|
return (Abs bt var body,ty)
|
||||||
|
tcRho gr scope (Abs bt var body) Nothing = do
|
||||||
|
i <- newMeta (eval [] typeType)
|
||||||
|
(body,body_ty) <- tcRho gr ((var,VMeta i (scopeEnv scope) []):scope) body Nothing
|
||||||
|
return (Abs bt var body, (VClosure (scopeEnv scope)
|
||||||
|
(Prod bt identW (Meta i) (value2term (scopeVars scope) body_ty))))
|
||||||
|
tcRho gr scope (Typed body ann_ty) mb_ty = do
|
||||||
|
body <- checkSigma gr scope body (eval (scopeEnv scope) ann_ty)
|
||||||
|
instSigma scope (Typed body ann_ty) (eval (scopeEnv scope) ann_ty) mb_ty
|
||||||
|
tcRho gr scope (FV ts) mb_ty = do
|
||||||
|
case ts of
|
||||||
|
[] -> do i <- newMeta (eval [] typeType)
|
||||||
|
instSigma scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty
|
||||||
|
(t:ts) -> do (t,ty) <- tcRho gr scope t mb_ty
|
||||||
|
|
||||||
|
let go [] ty = return ([],ty)
|
||||||
|
go (t:ts) ty = do (t, ty) <- tcRho gr scope t (Just ty)
|
||||||
|
(ts,ty) <- go ts ty
|
||||||
|
return (t:ts,ty)
|
||||||
|
|
||||||
|
(ts,ty) <- go ts ty
|
||||||
|
return (FV (t:ts), ty)
|
||||||
|
tcRho gr scope t _ = error ("tcRho "++show t)
|
||||||
|
|
||||||
|
-- | Invariant: if the third argument is (Just rho),
|
||||||
|
-- then rho is in weak-prenex form
|
||||||
|
instSigma :: Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho)
|
||||||
|
instSigma scope t ty1 (Just ty2) = do t <- subsCheckRho scope t ty1 ty2
|
||||||
|
return (t,ty2)
|
||||||
|
instSigma scope t ty1 Nothing = instantiate t ty1
|
||||||
|
|
||||||
|
-- | (subsCheck scope args off exp) checks that
|
||||||
|
-- 'off' is at least as polymorphic as 'args -> exp'
|
||||||
|
subsCheck :: Scope -> Term -> Sigma -> Sigma -> TcM Term
|
||||||
|
subsCheck scope t sigma1 sigma2 = do -- Rule DEEP-SKOL
|
||||||
|
(skol_tvs, rho2) <- skolemise scope sigma2
|
||||||
|
t <- subsCheckRho scope t sigma1 rho2
|
||||||
|
esc_tvs <- getFreeTyVars [sigma1,sigma2]
|
||||||
|
let bad_tvs = filter (`elem` esc_tvs) skol_tvs
|
||||||
|
if null bad_tvs
|
||||||
|
then return ()
|
||||||
|
else tcError (vcat [text "Subsumption check failed:",
|
||||||
|
nest 2 (ppTerm Unqualified 0 (value2term [] sigma1)),
|
||||||
|
text "is not as polymorphic as",
|
||||||
|
nest 2 (ppTerm Unqualified 0 (value2term [] sigma2))])
|
||||||
|
return t
|
||||||
|
|
||||||
|
|
||||||
|
-- | Invariant: the second argument is in weak-prenex form
|
||||||
|
subsCheckRho :: Scope -> Term -> Sigma -> Rho -> TcM Term
|
||||||
|
subsCheckRho scope t sigma1@(VClosure env (Prod Implicit _ _ _)) rho2 = do -- Rule SPEC
|
||||||
|
(t,rho1) <- instantiate t sigma1
|
||||||
|
subsCheckRho scope t rho1 rho2
|
||||||
|
subsCheckRho scope t rho1 (VClosure env (Prod Explicit _ a2 r2)) = do -- Rule FUN
|
||||||
|
(a1,r1) <- unifyFun scope rho1
|
||||||
|
subsCheckFun scope t a1 r1 (eval env a2) (eval env r2)
|
||||||
|
subsCheckRho scope t (VClosure env (Prod Explicit _ a1 r1)) rho2 = do -- Rule FUN
|
||||||
|
(a2,r2) <- unifyFun scope rho2
|
||||||
|
subsCheckFun scope t (eval env a1) (eval env r1) a2 r2
|
||||||
|
subsCheckRho scope t tau1 tau2 = do -- Rule MONO
|
||||||
|
unify scope tau1 tau2 -- Revert to ordinary unification
|
||||||
|
return t
|
||||||
|
|
||||||
|
subsCheckFun :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
|
||||||
|
subsCheckFun scope t a1 r1 a2 r2 = do
|
||||||
|
let v = newVar scope
|
||||||
|
vt <- subsCheck scope (Vr v) a2 a1
|
||||||
|
t <- subsCheckRho ((v,eval [] typeType):scope) (App t vt) r1 r2 ;
|
||||||
|
return (Abs Implicit v t)
|
||||||
|
|
||||||
|
|
||||||
|
-----------------------------------------------------------------------
|
||||||
|
-- Unification
|
||||||
|
-----------------------------------------------------------------------
|
||||||
|
|
||||||
|
unifyFun :: Scope -> Rho -> TcM (Sigma, Rho)
|
||||||
|
unifyFun scope (VClosure env (Prod Explicit x arg res))
|
||||||
|
| x /= identW = return (eval env arg,eval ((x,VGen (length scope) []):env) res)
|
||||||
|
| otherwise = return (eval env arg,eval env res)
|
||||||
|
unifyFun scope tau = do
|
||||||
|
arg_ty <- newMeta (eval [] typeType)
|
||||||
|
res_ty <- newMeta (eval [] typeType)
|
||||||
|
unify scope tau (VClosure [] (Prod Explicit identW (Meta arg_ty) (Meta res_ty)))
|
||||||
|
return (VMeta arg_ty [] [], VMeta res_ty [] [])
|
||||||
|
|
||||||
|
unify scope (VApp f1 vs1) (VApp f2 vs2)
|
||||||
|
| f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2)
|
||||||
|
unify scope (VMeta i env1 vs1) (VMeta j env2 vs2)
|
||||||
|
| i == j = sequence_ (zipWith (unify scope) vs1 vs2)
|
||||||
|
| otherwise = do mv <- getMeta j
|
||||||
|
case mv of
|
||||||
|
Bound t2 -> unify scope (VMeta i env1 vs1) (apply env2 t2 vs2)
|
||||||
|
Unbound _ -> setMeta i (Bound (Meta j))
|
||||||
|
unify scope (VMeta i env vs) v = unifyVar scope i env vs v
|
||||||
|
unify scope v (VMeta i env vs) = unifyVar scope i env vs v
|
||||||
|
unify scope v1 v2 = do
|
||||||
|
v1 <- zonkTerm (value2term (scopeVars scope) v1)
|
||||||
|
v2 <- zonkTerm (value2term (scopeVars scope) v2)
|
||||||
|
tcError (text "Cannot unify types:" <+> (ppTerm Unqualified 0 v1 $$
|
||||||
|
ppTerm Unqualified 0 v2))
|
||||||
|
|
||||||
|
-- | Invariant: tv1 is a flexible type variable
|
||||||
|
unifyVar :: Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
|
||||||
|
unifyVar scope i env vs ty2 = do -- Check whether i is bound
|
||||||
|
mv <- getMeta i
|
||||||
|
case mv of
|
||||||
|
Bound ty1 -> unify scope (apply env ty1 vs) ty2
|
||||||
|
Unbound _ -> do let ty2' = value2term [] ty2
|
||||||
|
ms2 <- getMetaVars [ty2]
|
||||||
|
if i `elem` ms2
|
||||||
|
then tcError (text "Occurs check for" <+> ppMeta i <+> text "in:" $$
|
||||||
|
nest 2 (ppTerm Unqualified 0 ty2'))
|
||||||
|
else setMeta i (Bound ty2')
|
||||||
|
|
||||||
|
|
||||||
|
-----------------------------------------------------------------------
|
||||||
|
-- Instantiation and quantification
|
||||||
|
-----------------------------------------------------------------------
|
||||||
|
|
||||||
|
-- | Instantiate the topmost for-alls of the argument type
|
||||||
|
-- with metavariables
|
||||||
|
instantiate :: Term -> Sigma -> TcM (Term,Rho)
|
||||||
|
instantiate t (VClosure env (Prod Implicit x ty1 ty2)) = do
|
||||||
|
i <- newMeta (eval env ty1)
|
||||||
|
instantiate (App t (ImplArg (Meta i))) (eval ((x,VMeta i [] []):env) ty2)
|
||||||
|
instantiate t ty = do
|
||||||
|
return (t,ty)
|
||||||
|
|
||||||
|
skolemise scope (VClosure env (Prod Implicit x arg_ty res_ty)) = do -- Rule PRPOLY
|
||||||
|
sk <- newSkolemTyVar arg_ty
|
||||||
|
(sks, res_ty) <- skolemise scope (eval ((x,undefined):env) res_ty)
|
||||||
|
return (sk : sks, res_ty)
|
||||||
|
skolemise scope (VClosure env (Prod Explicit x arg_ty res_ty)) = do -- Rule PRFUN
|
||||||
|
(sks, res_ty) <- if x /= identW
|
||||||
|
then skolemise scope (eval ((x,VGen (length scope) []):env) res_ty)
|
||||||
|
else skolemise scope (eval env res_ty)
|
||||||
|
return (sks, VClosure env (Prod Explicit x arg_ty (value2term [] res_ty)))
|
||||||
|
skolemise scope ty -- Rule PRMONO
|
||||||
|
= return ([], ty)
|
||||||
|
|
||||||
|
newSkolemTyVar _ = undefined
|
||||||
|
|
||||||
|
-- Quantify over the specified type variables (all flexible)
|
||||||
|
quantify :: Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma)
|
||||||
|
quantify scope t tvs ty0 = do
|
||||||
|
mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way
|
||||||
|
ty <- zonkTerm ty -- of doing the substitution
|
||||||
|
return (foldr (Abs Implicit) t new_bndrs
|
||||||
|
,eval [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs)
|
||||||
|
)
|
||||||
|
where
|
||||||
|
ty = value2term (scopeVars scope) ty0
|
||||||
|
|
||||||
|
used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use
|
||||||
|
new_bndrs = take (length tvs) (allBinders \\ used_bndrs)
|
||||||
|
bind (i, name) = setMeta i (Bound (Vr name))
|
||||||
|
|
||||||
|
bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2
|
||||||
|
bndrs _ = []
|
||||||
|
|
||||||
|
allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,...
|
||||||
|
allBinders = [ identC (BS.pack [x]) | x <- ['a'..'z'] ] ++
|
||||||
|
[ identC (BS.pack (x : show i)) | i <- [1 :: Integer ..], x <- ['a'..'z']]
|
||||||
|
|
||||||
|
|
||||||
|
-----------------------------------------------------------------------
|
||||||
|
-- The Monad
|
||||||
|
-----------------------------------------------------------------------
|
||||||
|
|
||||||
|
type Scope = [(Ident,Value)]
|
||||||
|
|
||||||
|
type Sigma = Value
|
||||||
|
type Rho = Value -- No top-level ForAll
|
||||||
|
type Tau = Value -- No ForAlls anywhere
|
||||||
|
|
||||||
|
data MetaValue
|
||||||
|
= Unbound Sigma
|
||||||
|
| Bound Term
|
||||||
|
type MetaStore = IntMap.IntMap MetaValue
|
||||||
|
data TcResult a
|
||||||
|
= TcOk MetaStore a
|
||||||
|
| TcFail Doc
|
||||||
|
newtype TcM a = TcM {unTcM :: MetaStore -> TcResult a}
|
||||||
|
|
||||||
|
instance Monad TcM where
|
||||||
|
return x = TcM (\ms -> TcOk ms x)
|
||||||
|
f >>= g = TcM (\ms -> case unTcM f ms of
|
||||||
|
TcOk ms x -> unTcM (g x) ms
|
||||||
|
TcFail msg -> TcFail msg)
|
||||||
|
fail = tcError . text
|
||||||
|
|
||||||
|
tcError :: Message -> TcM a
|
||||||
|
tcError msg = TcM (\ms -> TcFail msg)
|
||||||
|
|
||||||
|
runTcM :: TcM a -> Check a
|
||||||
|
runTcM f = case unTcM f IntMap.empty of
|
||||||
|
TcOk _ x -> return x
|
||||||
|
TcFail s -> checkError s
|
||||||
|
|
||||||
|
newMeta :: Sigma -> TcM MetaId
|
||||||
|
newMeta ty = TcM (\ms -> let i = IntMap.size ms
|
||||||
|
in TcOk (IntMap.insert i (Unbound ty) ms) i)
|
||||||
|
|
||||||
|
getMeta :: MetaId -> TcM MetaValue
|
||||||
|
getMeta i = TcM (\ms ->
|
||||||
|
case IntMap.lookup i ms of
|
||||||
|
Just mv -> TcOk ms mv
|
||||||
|
Nothing -> TcFail (text "Unknown metavariable" <+> ppMeta i))
|
||||||
|
|
||||||
|
setMeta :: MetaId -> MetaValue -> TcM ()
|
||||||
|
setMeta i mv = TcM (\ms -> TcOk (IntMap.insert i mv ms) ())
|
||||||
|
|
||||||
|
newVar :: Scope -> Ident
|
||||||
|
newVar scope = head [x | i <- [1..],
|
||||||
|
let x = identC (BS.pack ('v':show i)),
|
||||||
|
isFree scope x]
|
||||||
|
where
|
||||||
|
isFree [] x = True
|
||||||
|
isFree ((y,_):scope) x = x /= y && isFree scope x
|
||||||
|
|
||||||
|
scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..]
|
||||||
|
scopeVars scope = map fst scope
|
||||||
|
|
||||||
|
-- | This function takes account of zonking, and returns a set
|
||||||
|
-- (no duplicates) of unbound meta-type variables
|
||||||
|
getMetaVars :: [Sigma] -> TcM [MetaId]
|
||||||
|
getMetaVars tys = do
|
||||||
|
tys <- mapM (zonkTerm . value2term []) tys
|
||||||
|
return (foldr go [] tys)
|
||||||
|
where
|
||||||
|
-- Get the MetaIds from a term; no duplicates in result
|
||||||
|
go (Vr tv) acc = acc
|
||||||
|
go (Meta i) acc
|
||||||
|
| i `elem` acc = acc
|
||||||
|
| otherwise = i : acc
|
||||||
|
go (Q _) acc = acc
|
||||||
|
go (QC _) acc = acc
|
||||||
|
go (Sort _) acc = acc
|
||||||
|
go (Prod _ _ arg res) acc = go arg (go res acc)
|
||||||
|
go t acc = error ("go "++show t)
|
||||||
|
|
||||||
|
-- | This function takes account of zonking, and returns a set
|
||||||
|
-- (no duplicates) of free type variables
|
||||||
|
getFreeTyVars :: [Sigma] -> TcM [Ident]
|
||||||
|
getFreeTyVars tys = do
|
||||||
|
tys <- mapM (zonkTerm . value2term []) tys
|
||||||
|
return (foldr (go []) [] tys)
|
||||||
|
where
|
||||||
|
go bound (Vr tv) acc
|
||||||
|
| tv `elem` bound = acc
|
||||||
|
| tv `elem` acc = acc
|
||||||
|
| otherwise = tv : acc
|
||||||
|
go bound (Meta _) acc = acc
|
||||||
|
go bound (Q _) acc = acc
|
||||||
|
go bound (QC _) acc = acc
|
||||||
|
go bound (Prod _ x arg res) acc = go bound arg (go (x : bound) res acc)
|
||||||
|
|
||||||
|
-- | Eliminate any substitutions in a term
|
||||||
|
zonkTerm :: Term -> TcM Term
|
||||||
|
zonkTerm (Prod bt x t1 t2) = do
|
||||||
|
t1 <- zonkTerm t1
|
||||||
|
t2 <- zonkTerm t2
|
||||||
|
return (Prod bt x t1 t2)
|
||||||
|
zonkTerm (Q n) = return (Q n)
|
||||||
|
zonkTerm (QC n) = return (QC n)
|
||||||
|
zonkTerm (EInt n) = return (EInt n)
|
||||||
|
zonkTerm (EFloat f) = return (EFloat f)
|
||||||
|
zonkTerm (K s) = return (K s)
|
||||||
|
zonkTerm (Empty) = return (Empty)
|
||||||
|
zonkTerm (Sort s) = return (Sort s)
|
||||||
|
zonkTerm (App arg res) = do
|
||||||
|
arg <- zonkTerm arg
|
||||||
|
res <- zonkTerm res
|
||||||
|
return (App arg res)
|
||||||
|
zonkTerm (Abs bt x body) = do
|
||||||
|
body <- zonkTerm body
|
||||||
|
return (Abs bt x body)
|
||||||
|
zonkTerm (Typed body ty) = do
|
||||||
|
body <- zonkTerm body
|
||||||
|
ty <- zonkTerm ty
|
||||||
|
return (Typed body ty)
|
||||||
|
zonkTerm (Vr x) = return (Vr x)
|
||||||
|
zonkTerm (Meta i) = do
|
||||||
|
mv <- getMeta i
|
||||||
|
case mv of
|
||||||
|
Unbound _ -> return (Meta i)
|
||||||
|
Bound t -> do t <- zonkTerm t
|
||||||
|
setMeta i (Bound t) -- "Short out" multiple hops
|
||||||
|
return t
|
||||||
|
zonkTerm (ImplArg t) = do
|
||||||
|
t <- zonkTerm t
|
||||||
|
return (ImplArg t)
|
||||||
|
zonkTerm (FV ts) = do
|
||||||
|
ts <- mapM zonkTerm ts
|
||||||
|
return (FV ts)
|
||||||
|
zonkTerm t = error ("zonkTerm "++show t)
|
||||||
@@ -19,6 +19,7 @@ module GF.Grammar.Printer
|
|||||||
, ppConstrs
|
, ppConstrs
|
||||||
, ppLocation
|
, ppLocation
|
||||||
, ppQIdent
|
, ppQIdent
|
||||||
|
, ppMeta
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import GF.Infra.Ident
|
import GF.Infra.Ident
|
||||||
@@ -26,6 +27,7 @@ import GF.Infra.Option
|
|||||||
import GF.Grammar.Values
|
import GF.Grammar.Values
|
||||||
import GF.Grammar.Grammar
|
import GF.Grammar.Grammar
|
||||||
|
|
||||||
|
import PGF.Expr (ppMeta)
|
||||||
import PGF.Printer (ppFId, ppFunId, ppSeqId, ppSeq)
|
import PGF.Printer (ppFId, ppFunId, ppSeqId, ppSeq)
|
||||||
|
|
||||||
import Text.PrettyPrint
|
import Text.PrettyPrint
|
||||||
@@ -212,7 +214,7 @@ ppTerm q d (Sort id) = ppIdent id
|
|||||||
ppTerm q d (K s) = str s
|
ppTerm q d (K s) = str s
|
||||||
ppTerm q d (EInt n) = int n
|
ppTerm q d (EInt n) = int n
|
||||||
ppTerm q d (EFloat f) = double f
|
ppTerm q d (EFloat f) = double f
|
||||||
ppTerm q d (Meta _) = char '?'
|
ppTerm q d (Meta i) = ppMeta i
|
||||||
ppTerm q d (Empty) = text "[]"
|
ppTerm q d (Empty) = text "[]"
|
||||||
ppTerm q d (R []) = text "<>" -- to distinguish from {} empty RecType
|
ppTerm q d (R []) = text "<>" -- to distinguish from {} empty RecType
|
||||||
ppTerm q d (R xs) = braces (fsep (punctuate semi [ppLabel l <+>
|
ppTerm q d (R xs) = braces (fsep (punctuate semi [ppLabel l <+>
|
||||||
|
|||||||
@@ -167,7 +167,8 @@ data Flags = Flags {
|
|||||||
optUnlexer :: Maybe String,
|
optUnlexer :: Maybe String,
|
||||||
optWarnings :: [Warning],
|
optWarnings :: [Warning],
|
||||||
optDump :: [Dump],
|
optDump :: [Dump],
|
||||||
optTagsOnly :: Bool
|
optTagsOnly :: Bool,
|
||||||
|
optNewComp :: Bool
|
||||||
}
|
}
|
||||||
deriving (Show)
|
deriving (Show)
|
||||||
|
|
||||||
@@ -269,7 +270,8 @@ defaultFlags = Flags {
|
|||||||
optUnlexer = Nothing,
|
optUnlexer = Nothing,
|
||||||
optWarnings = [],
|
optWarnings = [],
|
||||||
optDump = [],
|
optDump = [],
|
||||||
optTagsOnly = False
|
optTagsOnly = False,
|
||||||
|
optNewComp = False
|
||||||
}
|
}
|
||||||
|
|
||||||
-- Option descriptions
|
-- Option descriptions
|
||||||
@@ -346,6 +348,7 @@ optDescr =
|
|||||||
Option [] ["stem"] (onOff (toggleOptimize OptStem) True) "Perform stem-suffix analysis (default on).",
|
Option [] ["stem"] (onOff (toggleOptimize OptStem) True) "Perform stem-suffix analysis (default on).",
|
||||||
Option [] ["cse"] (onOff (toggleOptimize OptCSE) True) "Perform common sub-expression elimination (default on).",
|
Option [] ["cse"] (onOff (toggleOptimize OptCSE) True) "Perform common sub-expression elimination (default on).",
|
||||||
Option [] ["cfg"] (ReqArg cfgTransform "TRANS") "Enable or disable specific CFG transformations. TRANS = merge, no-merge, bottomup, no-bottomup, ...",
|
Option [] ["cfg"] (ReqArg cfgTransform "TRANS") "Enable or disable specific CFG transformations. TRANS = merge, no-merge, bottomup, no-bottomup, ...",
|
||||||
|
Option [] ["new-comp"] (NoArg (set $ \o -> o{optNewComp = True})) "Use the new experimental compiler.",
|
||||||
dumpOption "source" DumpSource,
|
dumpOption "source" DumpSource,
|
||||||
dumpOption "rebuild" DumpRebuild,
|
dumpOption "rebuild" DumpRebuild,
|
||||||
dumpOption "extend" DumpExtend,
|
dumpOption "extend" DumpExtend,
|
||||||
|
|||||||
Reference in New Issue
Block a user