diff --git a/src/compiler/GF/Compile/CheckGrammar.hs b/src/compiler/GF/Compile/CheckGrammar.hs index be7506766..9a566ad8d 100644 --- a/src/compiler/GF/Compile/CheckGrammar.hs +++ b/src/compiler/GF/Compile/CheckGrammar.hs @@ -23,9 +23,11 @@ module GF.Compile.CheckGrammar(checkModule) where import GF.Infra.Ident +import GF.Infra.Option import GF.Compile.TypeCheck.Abstract import GF.Compile.TypeCheck.Concrete +import qualified GF.Compile.TypeCheck.ConcreteNew as CN import GF.Grammar import GF.Grammar.Lexer @@ -42,8 +44,8 @@ import Control.Monad import Text.PrettyPrint -- | checking is performed in the dependency order of modules -checkModule :: [SourceModule] -> SourceModule -> Check SourceModule -checkModule mos mo@(m,mi) = do +checkModule :: Options -> [SourceModule] -> SourceModule -> Check SourceModule +checkModule opts mos mo@(m,mi) = do checkRestrictedInheritance mos mo mo <- case mtype mi of MTConcrete a -> do let gr = mGrammar (mo:mos) @@ -54,7 +56,7 @@ checkModule mos mo@(m,mi) = do foldM updateCheckInfo mo infos where 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)}) -- 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. -- A May-value has always been checked in its origin module. -checkInfo :: [SourceModule] -> SourceModule -> Ident -> Info -> Check Info -checkInfo ms (m,mo) c info = do +checkInfo :: Options -> [SourceModule] -> SourceModule -> Ident -> Info -> Check Info +checkInfo opts ms (m,mo) c info = do checkIn (ppLocation (msrc mo) NoLoc <> colon) $ checkReservedId c case info of @@ -211,11 +213,15 @@ checkInfo ms (m,mo) c info = do ty' <- chIn loct "operation" $ checkLType gr [] ty typeType >>= computeLType gr [] . fst (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')) (Nothing , Just (L locd de)) -> do (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')) (Just (L loct ty), Nothing) -> do chIn loct "operation" $ diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew.hs b/src/compiler/GF/Compile/Compute/ConcreteNew.hs new file mode 100644 index 000000000..1172ece42 --- /dev/null +++ b/src/compiler/GF/Compile/Compute/ConcreteNew.hs @@ -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) diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs new file mode 100644 index 000000000..265563611 --- /dev/null +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -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) diff --git a/src/compiler/GF/Grammar/Printer.hs b/src/compiler/GF/Grammar/Printer.hs index fe5fe8803..08d70928c 100644 --- a/src/compiler/GF/Grammar/Printer.hs +++ b/src/compiler/GF/Grammar/Printer.hs @@ -19,6 +19,7 @@ module GF.Grammar.Printer , ppConstrs , ppLocation , ppQIdent + , ppMeta ) where import GF.Infra.Ident @@ -26,6 +27,7 @@ import GF.Infra.Option import GF.Grammar.Values import GF.Grammar.Grammar +import PGF.Expr (ppMeta) import PGF.Printer (ppFId, ppFunId, ppSeqId, ppSeq) import Text.PrettyPrint @@ -212,7 +214,7 @@ ppTerm q d (Sort id) = ppIdent id ppTerm q d (K s) = str s ppTerm q d (EInt n) = int n 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 (R []) = text "<>" -- to distinguish from {} empty RecType ppTerm q d (R xs) = braces (fsep (punctuate semi [ppLabel l <+> diff --git a/src/compiler/GF/Infra/Option.hs b/src/compiler/GF/Infra/Option.hs index 7d5849684..74020f03b 100644 --- a/src/compiler/GF/Infra/Option.hs +++ b/src/compiler/GF/Infra/Option.hs @@ -167,7 +167,8 @@ data Flags = Flags { optUnlexer :: Maybe String, optWarnings :: [Warning], optDump :: [Dump], - optTagsOnly :: Bool + optTagsOnly :: Bool, + optNewComp :: Bool } deriving (Show) @@ -269,7 +270,8 @@ defaultFlags = Flags { optUnlexer = Nothing, optWarnings = [], optDump = [], - optTagsOnly = False + optTagsOnly = False, + optNewComp = False } -- Option descriptions @@ -346,6 +348,7 @@ optDescr = 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 [] ["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 "rebuild" DumpRebuild, dumpOption "extend" DumpExtend,