From fcc80b545dfa688dc2cb1e1847f53cceaa7af9c0 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Mon, 20 Nov 2023 14:53:36 +0100 Subject: [PATCH 01/15] started porting the experimental type checker to the new evaluator --- src/compiler/GF/Compile/Compute/Concrete.hs | 3 +- .../GF/Compile/TypeCheck/ConcreteNew.hs | 264 +++++++++--------- src/compiler/GF/Infra/CheckM.hs | 2 +- 3 files changed, 140 insertions(+), 129 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index 38d04dee6e..a6b220291e 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -5,7 +5,8 @@ module GF.Compile.Compute.Concrete ( normalForm , Value(..), Thunk, ThunkState(..), Env, showValue - , EvalM, runEvalM, evalError + , MetaThunks + , EvalM(..), runEvalM, evalError , eval, apply, force, value2term, patternMatch , newThunk, newEvaluatedThunk , newResiduation, newNarrowing, getVariables diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index b2e27a978b..fe53744cc5 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE CPP #-} +{-# LANGUAGE RankNTypes, CPP #-} module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where -- The code here is based on the paper: @@ -14,69 +14,70 @@ import GF.Compile.Compute.Concrete import GF.Infra.CheckM import GF.Data.Operations import Control.Applicative(Applicative(..)) -import Control.Monad(ap,liftM,mplus) +import Control.Monad(ap,liftM,mplus,foldM) +import Control.Monad.ST import GF.Text.Pretty import Data.List (nub, (\\), tails) -import qualified Data.IntMap as IntMap +import qualified Data.Map as Map import Data.Maybe(fromMaybe,isNothing) import qualified Control.Monad.Fail as Fail checkLType :: Grammar -> Term -> Type -> Check (Term, Type) -checkLType ge t ty = error "TODO: checkLType" {- runTcM $ do - vty <- liftErr (eval ge [] ty) - (t,_) <- tcRho ge [] t (Just vty) +checkLType gr t ty = runTcM gr $ do + vty <- liftEvalM (eval [] ty []) + (t,_) <- tcRho [] t (Just vty) t <- zonkTerm t - return (t,ty) -} + return (t,ty) inferLType :: Grammar -> Term -> Check (Term, Type) -inferLType ge t = error "TODO: inferLType" {- runTcM $ do - (t,ty) <- inferSigma ge [] t +inferLType gr t = runTcM gr $ do + (t,ty) <- inferSigma [] t t <- zonkTerm t - ty <- zonkTerm =<< tc_value2term (geLoc ge) [] ty - return (t,ty) -} -{- -inferSigma :: GlobalEnv -> Scope -> Term -> TcM (Term,Sigma) -inferSigma ge scope t = do -- GEN1 - (t,ty) <- tcRho ge scope t Nothing - env_tvs <- getMetaVars (geLoc ge) (scopeTypes scope) - res_tvs <- getMetaVars (geLoc ge) [(scope,ty)] + ty <- zonkTerm =<< liftEvalM (value2term [] ty) + return (t,ty) + +inferSigma :: Scope s -> Term -> TcM s (Term,Sigma s) +inferSigma scope t = do -- GEN1 + (t,ty) <- tcRho scope t Nothing + env_tvs <- getMetaVars (scopeTypes scope) + res_tvs <- getMetaVars [(scope,ty)] let forall_tvs = res_tvs \\ env_tvs - quantify ge scope t forall_tvs ty + quantify scope t forall_tvs ty -Just vtypeInt = fmap (flip VApp []) (predef cInt) -Just vtypeFloat = fmap (flip VApp []) (predef cFloat) -Just vtypeInts = fmap (\p i -> VApp p [VInt i]) (predef cInts) +vtypeInt = VApp (cPredef,cInt) [] +vtypeFloat = VApp (cPredef,cFloat) [] +vtypeInts i= liftEvalM (newEvaluatedThunk (VInt i)) >>= \tnk -> return (VApp (cPredef,cInts) [tnk]) vtypeStr = VSort cStr vtypeStrs = VSort cStrs vtypeType = VSort cType vtypePType = VSort cPType -tcRho :: GlobalEnv -> Scope -> Term -> Maybe Rho -> TcM (Term, Rho) -tcRho ge scope t@(EInt i) mb_ty = instSigma ge scope t (vtypeInts i) mb_ty -- INT -tcRho ge scope t@(EFloat _) mb_ty = instSigma ge scope t vtypeFloat mb_ty -- FLOAT -tcRho ge scope t@(K _) mb_ty = instSigma ge scope t vtypeStr mb_ty -- STR -tcRho ge scope t@(Empty) mb_ty = instSigma ge scope t vtypeStr mb_ty -tcRho ge scope t@(Vr v) mb_ty = do -- VAR +tcRho :: Scope s -> Term -> Maybe (Rho s) -> TcM s (Term, Rho s) +tcRho scope t@(EInt i) mb_ty = vtypeInts i >>= \sigma -> instSigma scope t sigma mb_ty -- INT +tcRho scope t@(EFloat _) mb_ty = instSigma scope t vtypeFloat mb_ty -- FLOAT +tcRho scope t@(K _) mb_ty = instSigma scope t vtypeStr mb_ty -- STR +tcRho scope t@(Empty) mb_ty = instSigma scope t vtypeStr mb_ty +tcRho scope t@(Vr v) mb_ty = do -- VAR case lookup v scope of - Just v_sigma -> instSigma ge scope t v_sigma mb_ty + Just v_sigma -> instSigma scope t v_sigma mb_ty Nothing -> tcError ("Unknown variable" <+> v) -tcRho ge scope t@(Q id) mb_ty = +tcRho scope t@(Q id) mb_ty = runTcA (tcOverloadFailed t) $ - tcApp ge scope t `bindTcA` \(t,ty) -> - instSigma ge scope t ty mb_ty -tcRho ge scope t@(QC id) mb_ty = + tcApp scope t `bindTcA` \(t,ty) -> + instSigma scope t ty mb_ty +tcRho scope t@(QC id) mb_ty = runTcA (tcOverloadFailed t) $ - tcApp ge scope t `bindTcA` \(t,ty) -> - instSigma ge scope t ty mb_ty -tcRho ge scope t@(App fun arg) mb_ty = do + tcApp scope t `bindTcA` \(t,ty) -> + instSigma scope t ty mb_ty +tcRho scope t@(App fun arg) mb_ty = do runTcA (tcOverloadFailed t) $ - tcApp ge scope t `bindTcA` \(t,ty) -> - instSigma ge scope t ty mb_ty -tcRho ge scope (Abs bt var body) Nothing = do -- ABS1 + tcApp scope t `bindTcA` \(t,ty) -> + instSigma scope t ty mb_ty +{-tcRho scope (Abs bt var body) Nothing = do -- ABS1 i <- newMeta scope vtypeType let arg_ty = VMeta i (scopeEnv scope) [] - (body,body_ty) <- tcRho ge ((var,arg_ty):scope) body Nothing - return (Abs bt var body, (VProd bt arg_ty identW (Bind (const body_ty)))) + (body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing + return (Abs bt var body, (VProd bt arg_ty identW body_ty)) tcRho ge scope t@(Abs Implicit var body) (Just ty) = do -- ABS2 (bt, var_ty, body_ty) <- unifyFun ge scope ty if bt == Implicit @@ -257,9 +258,9 @@ tcCases ge scope ((p,t):cs) p_ty mb_res_ty = do (t,res_ty) <- tcRho ge scope' t mb_res_ty (cs,mb_res_ty) <- tcCases ge scope cs p_ty (Just res_ty) return ((p,t):cs,mb_res_ty) +-} - -tcApp ge scope t@(App fun (ImplArg arg)) = do -- APP1 +tcApp scope t@(App fun (ImplArg arg)) = undefined {- do -- APP1 tcApp ge scope fun `bindTcA` \(fun,fun_ty) -> do (bt, arg_ty, res_ty) <- unifyFun ge scope fun_ty if (bt == Implicit) @@ -286,13 +287,13 @@ tcApp ge scope (QC id) = -- VAR (global) tcApp ge scope t = singleTcA (tcRho ge scope t Nothing) - +-} tcOverloadFailed t ttys = tcError ("Overload resolution failed" $$ "of term " <+> pp t $$ "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys]) - +{- tcPatt ge scope PW ty0 = return scope tcPatt ge scope (PV x) ty0 = @@ -393,18 +394,18 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do "cannot be of type" <+> ppTerm Unqualified 0 sort) (rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty return ((l,ty):rs,mb_ty) - +-} -- | Invariant: if the third argument is (Just rho), -- then rho is in weak-prenex form -instSigma :: GlobalEnv -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho) -instSigma ge scope t ty1 Nothing = return (t,ty1) -- INST1 -instSigma ge scope t ty1 (Just ty2) = do -- INST2 - t <- subsCheckRho ge scope t ty1 ty2 +instSigma :: Scope s -> Term -> Sigma s -> Maybe (Rho s) -> TcM s (Term, Rho s) +instSigma scope t ty1 Nothing = return (t,ty1) -- INST1 +instSigma scope t ty1 (Just ty2) = do -- INST2 + t <- subsCheckRho scope t ty1 ty2 return (t,ty2) -- | Invariant: the second argument is in weak-prenex form -subsCheckRho :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> TcM Term -subsCheckRho ge scope t ty1@(VMeta i env vs) ty2 = do +subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> TcM s Term +subsCheckRho scope t ty1@(VMeta i env vs) ty2 = undefined {- do mv <- getMeta i case mv of Unbound _ _ -> do unify ge scope ty1 ty2 @@ -601,10 +602,10 @@ skolemise ge scope (VProd Implicit ty1 x (Bind ty2)) = do return (scope,Abs Implicit v . f,ty2) skolemise ge scope ty = do return (scope,id,ty) - +-} -- | Quantify over the specified type variables (all flexible) -quantify :: GlobalEnv -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma) -quantify ge scope t tvs ty0 = do +quantify :: Scope s -> Term -> [MetaId] -> Rho s -> TcM s (Term,Sigma s) +quantify scope t tvs ty0 = undefined {- do ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0 let used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use new_bndrs = take (length tvs) (allBinders \\ used_bndrs) @@ -622,72 +623,84 @@ allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,... allBinders = [ identS [x] | x <- ['a'..'z'] ] ++ [ identS (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 +type Scope s = [(Ident,Value s)] +type Sigma s = Value s +type Rho s = Value s -- No top-level ForAll +type Tau s = Value s -- No ForAlls anywhere -data MetaValue - = Unbound Scope Sigma - | Bound Term -type MetaStore = IntMap.IntMap MetaValue -data TcResult a - = TcOk a MetaStore [Message] - | TcFail [Message] -- First msg is error, the rest are warnings? -newtype TcM a = TcM {unTcM :: MetaStore -> [Message] -> TcResult a} +data TcResult s a + = TcOk a (MetaThunks s) [Message] + | TcFail [Message] -- First msg is error, the rest are warnings? +newtype TcM s a = TcM {unTcM :: Grammar -> MetaThunks s -> [Message] -> ST s (TcResult s a)} -instance Monad TcM where - return x = TcM (\ms msgs -> TcOk x ms msgs) - f >>= g = TcM (\ms msgs -> case unTcM f ms msgs of - TcOk x ms msgs -> unTcM (g x) ms msgs - TcFail msgs -> TcFail msgs) +instance Monad (TcM s) where + return x = TcM (\gr ms msgs -> return (TcOk x ms msgs)) + f >>= g = TcM $ \gr ms msgs -> do + res <- unTcM f gr ms msgs + case res of + TcOk x ms msgs -> unTcM (g x) gr ms msgs + TcFail msgs -> return (TcFail msgs) #if !(MIN_VERSION_base(4,13,0)) -- Monad(fail) will be removed in GHC 8.8+ fail = Fail.fail #endif -instance Fail.MonadFail TcM where +instance Fail.MonadFail (TcM s) where fail = tcError . pp -instance Applicative TcM where +instance Applicative (TcM s) where pure = return (<*>) = ap -instance Functor TcM where - fmap f g = TcM (\ms msgs -> case unTcM g ms msgs of - TcOk x ms msgs -> TcOk (f x) ms msgs - TcFail msgs -> TcFail msgs) +instance Functor (TcM s) where + fmap f g = TcM $ \gr ms msgs -> do + res <- unTcM g gr ms msgs + case res of + TcOk x ms msgs -> return (TcOk (f x) ms msgs) + TcFail msgs -> return (TcFail msgs) -instance ErrorMonad TcM where +instance ErrorMonad (TcM s) where raise = tcError . pp - handle f g = TcM (\ms msgs -> case unTcM f ms msgs of - TcFail (msg:msgs) -> unTcM (g (render msg)) ms msgs - r -> r) + handle f g = TcM $ \gr ms msgs -> do + res <- unTcM f gr ms msgs + case res of + TcFail (msg:msgs) -> unTcM (g (render msg)) gr ms msgs + r -> return r -tcError :: Message -> TcM a -tcError msg = TcM (\ms msgs -> TcFail (msg : msgs)) +tcError :: Message -> TcM s a +tcError msg = TcM (\gr ms msgs -> return (TcFail (msg : msgs))) -tcWarn :: Message -> TcM () -tcWarn msg = TcM (\ms msgs -> TcOk () ms (msg : msgs)) +tcWarn :: Message -> TcM s () +tcWarn msg = TcM (\gr ms msgs -> return (TcOk () ms (msg : msgs))) unimplemented str = fail ("Unimplemented: "++str) -runTcM :: TcM a -> Check a -runTcM f = case unTcM f IntMap.empty [] of - TcOk x _ msgs -> do checkWarnings msgs; return x - TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg +runTcM :: Grammar -> (forall s . TcM s a) -> Check a +runTcM gr f = Check $ \(errs,wngs) -> runST $ do + res <- unTcM f gr Map.empty [] + case res of + TcOk x _ msgs -> return ((errs, wngs++msgs),Success x) + TcFail (msg:msgs) -> return ((errs, wngs++msgs),Fail msg) + +liftEvalM :: EvalM s a -> TcM s a +liftEvalM (EvalM f) = TcM $ \gr ms msgs -> do + res <- f gr (\x ms r -> return (Success (x,ms))) ms undefined + case res of + Success (x,ms) -> return (TcOk x ms []) + Fail msg -> return (TcFail [msg]) + -newMeta :: Scope -> Sigma -> TcM MetaId -newMeta scope ty = TcM (\ms msgs -> + +newMeta :: Scope s -> Sigma s -> TcM s MetaId +newMeta scope ty = undefined {- TcM (\ms msgs -> let i = IntMap.size ms in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs) @@ -707,15 +720,15 @@ newVar scope = head [x | i <- [1..], 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 scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope) -- | This function takes account of zonking, and returns a set -- (no duplicates) of unbound meta-type variables -getMetaVars :: GLocation -> [(Scope,Sigma)] -> TcM [MetaId] -getMetaVars loc sc_tys = do +getMetaVars :: [(Scope s,Sigma s)] -> TcM s [MetaId] +getMetaVars sc_tys = undefined {- do tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys return (foldr go [] tys) where @@ -751,10 +764,10 @@ getFreeVars loc sc_tys = do go bound (Prod _ x arg res) acc = go bound arg (go (x : bound) res acc) go bound (RecType rs) acc = foldl (\acc (l,ty) -> go bound ty acc) acc rs go bound (Table p t) acc = go bound p (go bound t acc) - +-} -- | Eliminate any substitutions in a term -zonkTerm :: Term -> TcM Term -zonkTerm (Meta i) = do +zonkTerm :: Term -> TcM s Term +zonkTerm (Meta i) = undefined {- do mv <- getMeta i case mv of Unbound _ _ -> return (Meta i) @@ -763,40 +776,37 @@ zonkTerm (Meta i) = do return t zonkTerm t = composOp zonkTerm t -tc_value2term loc xs v = - return $ value2term loc xs v - -- Old value2term error message: - -- Left i -> tcError ("Variable #" <+> pp i <+> "has escaped") - - +-} -data TcA x a - = TcSingle (MetaStore -> [Message] -> TcResult a) - | TcMany [x] (MetaStore -> [Message] -> [(a,MetaStore,[Message])]) +data TcA s x a + = TcSingle (Grammar -> MetaThunks s -> [Message] -> ST s (TcResult s a)) + | TcMany [x] (Grammar -> MetaThunks s -> [Message] -> ST s [(a,MetaThunks s,[Message])]) -mkTcA :: Err [a] -> TcA a a +mkTcA :: Err [a] -> TcA s a a mkTcA f = case f of - Bad msg -> TcSingle (\ms msgs -> TcFail (pp msg : msgs)) - Ok [x] -> TcSingle (\ms msgs -> TcOk x ms msgs) - Ok xs -> TcMany xs (\ms msgs -> [(x,ms,msgs) | x <- xs]) + Bad msg -> TcSingle (\gr ms msgs -> return (TcFail (pp msg : msgs))) + Ok [x] -> TcSingle (\gr ms msgs -> return (TcOk x ms msgs)) + Ok xs -> TcMany xs (\gr ms msgs -> return [(x,ms,msgs) | x <- xs]) -singleTcA :: TcM a -> TcA x a +singleTcA :: TcM s a -> TcA s x a singleTcA = TcSingle . unTcM -bindTcA :: TcA x a -> (a -> TcM b) -> TcA x b +bindTcA :: TcA s x a -> (a -> TcM s b) -> TcA s x b bindTcA f g = case f of TcSingle f -> TcSingle (unTcM (TcM f >>= g)) - TcMany xs f -> TcMany xs (\ms msgs -> foldr add [] (f ms msgs)) + TcMany xs f -> TcMany xs (\gr ms msgs -> f gr ms msgs >>= foldM (add gr) []) where - add (y,ms,msgs) rs = - case unTcM (g y) ms msgs of - TcFail _ -> rs - TcOk y ms msgs -> (y,ms,msgs):rs - -runTcA :: ([x] -> TcM a) -> TcA x a -> TcM a -runTcA g f = TcM (\ms msgs -> case f of - TcMany xs f -> case f ms msgs of - [(x,ms,msgs)] -> TcOk x ms msgs - rs -> unTcM (g xs) ms msgs - TcSingle f -> f ms msgs) --} + add gr rs (y,ms,msgs) = do + res <- unTcM (g y) gr ms msgs + case res of + TcFail _ -> return rs + TcOk y ms msgs -> return ((y,ms,msgs):rs) + +runTcA :: ([x] -> TcM s a) -> TcA s x a -> TcM s a +runTcA g f = TcM (\gr ms msgs -> case f of + TcMany xs f -> do rs <- f gr ms msgs + case rs of + [(x,ms,msgs)] -> return (TcOk x ms msgs) + rs -> unTcM (g xs) gr ms msgs + TcSingle f -> f gr ms msgs) + diff --git a/src/compiler/GF/Infra/CheckM.hs b/src/compiler/GF/Infra/CheckM.hs index 6ad8d72e0b..96d298f750 100644 --- a/src/compiler/GF/Infra/CheckM.hs +++ b/src/compiler/GF/Infra/CheckM.hs @@ -13,7 +13,7 @@ ----------------------------------------------------------------------------- module GF.Infra.CheckM - (Check, CheckResult(..), Message, runCheck, runCheck', + (Check(..), CheckResult(..), Message, runCheck, runCheck', checkError, checkCond, checkWarn, checkWarnings, checkAccumError, checkIn, checkInModule, checkMap, checkMapRecover, accumulateError, commitCheck, From 511fdeee446a74f262c57646ef7f3b20d2f2d3b9 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Thu, 23 Nov 2023 19:35:18 +0100 Subject: [PATCH 02/15] the normalForm for terms now compresses variants --- src/compiler/GF/Compile/Compute/Concrete.hs | 193 +++++++++++------- src/compiler/GF/Compile/GeneratePMCFG.hs | 2 +- .../GF/Compile/TypeCheck/ConcreteNew.hs | 2 +- 3 files changed, 121 insertions(+), 76 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index a6b220291e..6b19a15e61 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RankNTypes, CPP #-} +{-# LANGUAGE RankNTypes, BangPatterns, CPP #-} -- | Functions for computing the values of terms in the concrete syntax, in -- | preparation for PMCFG generation. @@ -45,10 +45,9 @@ normalForm gr t = mkFV [t] = t mkFV ts = FV ts - data ThunkState s = Unevaluated (Env s) Term - | Evaluated (Value s) + | Evaluated {-# UNPACK #-} !Int (Value s) | Residuation {-# UNPACK #-} !MetaId | Narrowing {-# UNPACK #-} !MetaId Type @@ -114,10 +113,15 @@ showValue (VAlts _ _) = "VAlts" showValue (VStrs _) = "VStrs" showValue (VSymCat _ _ _) = "VSymCat" -eval env (Vr x) vs = case lookup x env of - Just tnk -> do v <- force tnk - apply v vs - Nothing -> evalError ("Variable" <+> pp x <+> "is not in scope") +eval env (Vr x) vs = do (tnk,depth) <- lookup x env + withVar depth $ do + v <- force tnk + apply v vs + where + lookup x [] = evalError ("Variable" <+> pp x <+> "is not in scope") + lookup x ((y,tnk):env) + | x == y = return (tnk,length env) + | otherwise = lookup x env eval env (Sort s) [] = return (VSort s) eval env (EInt n) [] = return (VInt n) eval env (EFloat d) [] = return (VFlt d) @@ -440,30 +444,30 @@ vtableSelect v0 ty tnks tnk2 vs = do "cannot be evaluated at compile time.") -susp i env ki = EvalM $ \gr k mt r -> do +susp i env ki = EvalM $ \gr k mt d r -> do s <- readSTRef i case s of Narrowing id (QC q) -> case lookupOrigInfo gr q of - Ok (m,ResParam (Just (L _ ps)) _) -> bindParam gr k mt r s m ps + Ok (m,ResParam (Just (L _ ps)) _) -> bindParam gr k mt d r s m ps Bad msg -> return (Fail (pp msg)) Narrowing id ty | Just max <- isTypeInts ty - -> bindInt gr k mt r s 0 max - Evaluated v -> case ki v of - EvalM f -> f gr k mt r - _ -> k (VSusp i env ki []) mt r + -> bindInt gr k mt d r s 0 max + Evaluated _ v -> case ki v of + EvalM f -> f gr k mt d r + _ -> k (VSusp i env ki []) mt d r where - bindParam gr k mt r s m [] = return (Success r) - bindParam gr k mt r s m ((p, ctxt):ps) = do + bindParam gr k mt d r s m [] = return (Success r) + bindParam gr k mt d r s m ((p, ctxt):ps) = do (mt',tnks) <- mkArgs mt ctxt let v = VApp (m,p) tnks - writeSTRef i (Evaluated v) + writeSTRef i (Evaluated (length env) v) res <- case ki v of - EvalM f -> f gr k mt' r + EvalM f -> f gr k mt' d r writeSTRef i s case res of Fail msg -> return (Fail msg) - Success r -> bindParam gr k mt r s m ps + Success r -> bindParam gr k mt d r s m ps mkArgs mt [] = return (mt,[]) mkArgs mt ((_,_,ty):ctxt) = do @@ -474,31 +478,31 @@ susp i env ki = EvalM $ \gr k mt r -> do (mt,tnks) <- mkArgs (Map.insert i tnk mt) ctxt return (mt,tnk:tnks) - bindInt gr k mt r s iv max + bindInt gr k mt d r s iv max | iv <= max = do let v = VInt iv - writeSTRef i (Evaluated v) + writeSTRef i (Evaluated (length env) v) res <- case ki v of - EvalM f -> f gr k mt r + EvalM f -> f gr k mt d r writeSTRef i s case res of Fail msg -> return (Fail msg) - Success r -> bindInt gr k mt r s (iv+1) max + Success r -> bindInt gr k mt d r s (iv+1) max | otherwise = return (Success r) value2term xs (VApp q tnks) = - foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term xs)) (if fst q == cPredef then Q q else QC q) tnks + foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (if fst q == cPredef then Q q else QC q) tnks value2term xs (VMeta m env tnks) = do res <- zonk m tnks case res of - Right i -> foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term xs)) (Meta i) tnks + Right i -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) tnks Left v -> value2term xs v value2term xs (VSusp j env k vs) = do v <- k (VGen maxBound vs) value2term xs v value2term xs (VGen j tnks) = - foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term xs)) (Vr (reverse xs !! j)) tnks + foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Vr (reverse xs !! j)) tnks value2term xs (VClosure env (Abs b x t)) = do tnk <- newEvaluatedThunk (VGen (length xs) []) v <- eval ((x,tnk):env) t [] @@ -519,11 +523,11 @@ value2term xs (VRecType lbls) = do lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2term xs v)) lbls return (RecType lbls) value2term xs (VR as) = do - as <- mapM (\(lbl,tnk) -> fmap (\t -> (lbl,(Nothing,t))) (force tnk >>= value2term xs)) as + as <- mapM (\(lbl,tnk) -> fmap (\t -> (lbl,(Nothing,t))) (tnk2term xs tnk)) as return (R as) value2term xs (VP v lbl tnks) = do t <- value2term xs v - foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term xs)) (P t lbl) tnks + foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (P t lbl) tnks value2term xs (VExtR v1 v2) = do t1 <- value2term xs v1 t2 <- value2term xs v2 @@ -541,11 +545,11 @@ value2term xs (VT vty env cs)= do return (p,t) return (T (TTyped ty) cs) value2term xs (VV vty tnks)= do ty <- value2term xs vty - ts <- mapM (\tnk -> force tnk >>= value2term xs) tnks + ts <- mapM (tnk2term xs) tnks return (V ty ts) value2term xs (VS v1 tnk2 tnks) = do t1 <- value2term xs v1 - t2 <- force tnk2 >>= value2term xs - foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term xs)) (S t1 t2) tnks + t2 <- tnk2term xs tnk2 + foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (S t1 t2) tnks value2term xs (VSort s) = return (Sort s) value2term xs (VStr tok) = return (K tok) value2term xs (VInt n) = return (EInt n) @@ -676,7 +680,7 @@ value2int _ = RunTime -- * Evaluation monad type MetaThunks s = Map.Map MetaId (Thunk s) -type Cont s r = MetaThunks s -> r -> ST s (CheckResult r) +type Cont s r = MetaThunks s -> Int -> r -> ST s (CheckResult r) newtype EvalM s a = EvalM (forall r . Grammar -> (a -> Cont s r) -> Cont s r) instance Functor (EvalM s) where @@ -695,76 +699,80 @@ instance Monad (EvalM s) where #endif instance Fail.MonadFail (EvalM s) where - fail msg = EvalM (\gr k _ r -> return (Fail (pp msg))) + fail msg = EvalM (\gr k _ _ r -> return (Fail (pp msg))) instance Alternative (EvalM s) where - empty = EvalM (\gr k _ r -> return (Success r)) - (EvalM f) <|> (EvalM g) = EvalM $ \gr k mt r -> do - res <- f gr k mt r + empty = EvalM (\gr k _ _ r -> return (Success r)) + (EvalM f) <|> (EvalM g) = EvalM $ \gr k mt b r -> do + res <- f gr k mt b r case res of Fail msg -> return (Fail msg) - Success r -> g gr k mt r + Success r -> g gr k mt b r instance MonadPlus (EvalM s) where runEvalM :: Grammar -> (forall s . EvalM s a) -> Check [a] runEvalM gr f = case runST (case f of - EvalM f -> f gr (\x mt xs -> return (Success (x:xs))) Map.empty []) of + EvalM f -> f gr (\x mt _ xs -> return (Success (x:xs))) Map.empty maxBound []) of Fail msg -> checkError msg Success xs -> return (reverse xs) evalError :: Doc -> EvalM s a -evalError msg = EvalM (\gr k _ r -> return (Fail msg)) +evalError msg = EvalM (\gr k _ _ r -> return (Fail msg)) getResDef :: QIdent -> EvalM s Term -getResDef q = EvalM $ \gr k mt r -> do +getResDef q = EvalM $ \gr k mt d r -> do case lookupResDef gr q of - Ok t -> k t mt r + Ok t -> k t mt d r Bad msg -> return (Fail (pp msg)) getInfo :: QIdent -> EvalM s (ModuleName,Info) -getInfo q = EvalM $ \gr k mt r -> do +getInfo q = EvalM $ \gr k mt d r -> do case lookupOrigInfo gr q of - Ok res -> k res mt r + Ok res -> k res mt d r Bad msg -> return (Fail (pp msg)) getAllParamValues :: Type -> EvalM s [Term] -getAllParamValues ty = EvalM $ \gr k mt r -> +getAllParamValues ty = EvalM $ \gr k mt d r -> case allParamValues gr ty of - Ok ts -> k ts mt r + Ok ts -> k ts mt d r Bad msg -> return (Fail (pp msg)) -newThunk env t = EvalM $ \gr k mt r -> do +newThunk env t = EvalM $ \gr k mt d r -> do tnk <- newSTRef (Unevaluated env t) - k tnk mt r + k tnk mt d r -newEvaluatedThunk v = EvalM $ \gr k mt r -> do - tnk <- newSTRef (Evaluated v) - k tnk mt r +newEvaluatedThunk v = EvalM $ \gr k mt d r -> do + tnk <- newSTRef (Evaluated maxBound v) + k tnk mt d r -newResiduation i = EvalM $ \gr k mt r -> +newResiduation i = EvalM $ \gr k mt d r -> if i == 0 then do tnk <- newSTRef (Residuation i) - k tnk mt r + k tnk mt d r else case Map.lookup i mt of - Just tnk -> k tnk mt r + Just tnk -> k tnk mt d r Nothing -> do tnk <- newSTRef (Residuation i) - k tnk (Map.insert i tnk mt) r + k tnk (Map.insert i tnk mt) d r -newNarrowing i ty = EvalM $ \gr k mt r -> +newNarrowing i ty = EvalM $ \gr k mt d r -> if i == 0 then do tnk <- newSTRef (Narrowing i ty) - k tnk mt r + k tnk mt d r else case Map.lookup i mt of - Just tnk -> k tnk mt r + Just tnk -> k tnk mt d r Nothing -> do tnk <- newSTRef (Narrowing i ty) - k tnk (Map.insert i tnk mt) r + k tnk (Map.insert i tnk mt) d r + +withVar d0 (EvalM f) = EvalM $ \gr k mt d1 r -> + let !d = min d0 d1 + in f gr k mt d r getVariables :: EvalM s [(LVar,LIndex)] -getVariables = EvalM $ \gr k mt r -> do +getVariables = EvalM $ \gr k mt d r -> do ps <- metas2params gr (Map.elems mt) - k ps mt r + k ps mt d r where metas2params gr [] = return [] metas2params gr (tnk:tnks) = do @@ -779,24 +787,61 @@ getVariables = EvalM $ \gr k mt r -> do else return params _ -> metas2params gr tnks -getRef tnk = EvalM $ \gr k mt r -> readSTRef tnk >>= \st -> k st mt r +getRef tnk = EvalM $ \gr k mt d r -> readSTRef tnk >>= \st -> k st mt d r -force tnk = EvalM $ \gr k mt r -> do +force tnk = EvalM $ \gr k mt d r -> do s <- readSTRef tnk case s of Unevaluated env t -> case eval env t [] of - EvalM f -> f gr (\v mt r -> do writeSTRef tnk (Evaluated v) - r <- k v mt r - writeSTRef tnk s - return r) mt r - Evaluated v -> k v mt r - Residuation _ -> k (VMeta tnk [] []) mt r - Narrowing _ _ -> k (VMeta tnk [] []) mt r - -zonk tnk vs = EvalM $ \gr k mt r -> do + EvalM f -> f gr (\v mt b r -> do let d = length env + writeSTRef tnk (Evaluated d v) + r <- k v mt d r + writeSTRef tnk s + return r) mt d r + Evaluated d v -> k v mt d r + Residuation _ -> k (VMeta tnk [] []) mt d r + Narrowing _ _ -> k (VMeta tnk [] []) mt d r + +tnk2term xs tnk = EvalM $ \gr k mt d r -> + let join f g = do res <- f + case res of + Fail msg -> return (Fail msg) + Success r -> g r + + flush [] k1 mt r = k1 mt r + flush [x] k1 mt r = join (k x mt d r) (k1 mt) + flush xs k1 mt r = join (k (FV (reverse xs)) mt d r) (k1 mt) + + acc d0 x mt d (r,!c,xs) + | d < d0 = flush xs (\mt r -> join (k x mt d r) (\r -> return (Success (r,c+1,[])))) mt r + | otherwise = return (Success (r,c+1,x:xs)) + + in do s <- readSTRef tnk + case s of + Unevaluated env t -> do let d0 = length env + res <- case eval env t [] of + EvalM f -> f gr (\v mt d r -> do writeSTRef tnk (Evaluated d0 v) + r <- case value2term xs v of + EvalM f -> f gr (acc d0) mt d r + writeSTRef tnk s + return r) mt maxBound (r,0,[]) + case res of + Fail msg -> return (Fail msg) + Success (r,0,xs) -> k (FV []) mt d r + Success (r,c,xs) -> flush xs (\mt r -> return (Success r)) mt r + Evaluated d0 v -> do res <- case value2term xs v of + EvalM f -> f gr (acc d0) mt maxBound (r,0,[]) + case res of + Fail msg -> return (Fail msg) + Success (r,0,xs) -> k (FV []) mt d r + Success (r,c,xs) -> flush xs (\mt r -> return (Success r)) mt r + Residuation i -> k (Meta i) mt d r + Narrowing i _ -> k (Meta i) mt d r + +zonk tnk vs = EvalM $ \gr k mt d r -> do s <- readSTRef tnk case s of - Evaluated v -> case apply v vs of - EvalM f -> f gr (k . Left) mt r - Residuation i -> k (Right i) mt r - Narrowing i _ -> k (Right i) mt r + Evaluated _ v -> case apply v vs of + EvalM f -> f gr (k . Left) mt d r + Residuation i -> k (Right i) mt d r + Narrowing i _ -> k (Right i) mt d r diff --git a/src/compiler/GF/Compile/GeneratePMCFG.hs b/src/compiler/GF/Compile/GeneratePMCFG.hs index eeb42acdc8..0c1fafce71 100644 --- a/src/compiler/GF/Compile/GeneratePMCFG.hs +++ b/src/compiler/GF/Compile/GeneratePMCFG.hs @@ -250,7 +250,7 @@ param2int (VInt n) ty param2int (VMeta tnk _ _) ty = do tnk_st <- getRef tnk case tnk_st of - Evaluated v -> param2int v ty + Evaluated _ v -> param2int v ty Narrowing j ty -> do ts <- getAllParamValues ty return (0,[(1,j-1)],length ts) param2int v ty = do t <- value2term [] v diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index fe53744cc5..e71858975f 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -692,7 +692,7 @@ runTcM gr f = Check $ \(errs,wngs) -> runST $ do liftEvalM :: EvalM s a -> TcM s a liftEvalM (EvalM f) = TcM $ \gr ms msgs -> do - res <- f gr (\x ms r -> return (Success (x,ms))) ms undefined + res <- f gr (\x ms b r -> return (Success (x,ms))) ms maxBound undefined case res of Success (x,ms) -> return (TcOk x ms []) Fail msg -> return (TcFail [msg]) From e996d78b188967e66fbc6db0c6a2fe45e25c53c3 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Thu, 23 Nov 2023 20:26:48 +0100 Subject: [PATCH 03/15] make "cc", "so", "create lin", "create lincat" usable even without loaded grammar --- src/compiler/GF/Command/SourceCommands.hs | 52 ++++++++++--------- .../GF/Compile/TypeCheck/Primitives.hs | 18 ++++++- src/compiler/GF/Interactive.hs | 15 +++--- 3 files changed, 53 insertions(+), 32 deletions(-) diff --git a/src/compiler/GF/Command/SourceCommands.hs b/src/compiler/GF/Command/SourceCommands.hs index 578dcab71e..f254f61458 100644 --- a/src/compiler/GF/Command/SourceCommands.hs +++ b/src/compiler/GF/Command/SourceCommands.hs @@ -1,5 +1,6 @@ -- | Commands requiring source grammar in env module GF.Command.SourceCommands(HasGrammar(..),sourceCommands) where + import Prelude hiding (putStrLn) import qualified Prelude as P(putStrLn) import Data.List(nub,isInfixOf,isPrefixOf) @@ -21,6 +22,7 @@ import GF.Grammar.Lookup (allOpers,allOpersTo) import GF.Compile.Rename(renameSourceTerm) import GF.Compile.Compute.Concrete(normalForm) import GF.Compile.TypeCheck.Concrete as TC(inferLType,ppType) +import GF.Compile.TypeCheck.Primitives(predefMod) import GF.Command.Abstract(Option(..),isOpt,listFlags,valueString,valStrOpts) import GF.Command.CommandInfo @@ -37,8 +39,8 @@ sourceCommands = Map.fromList [ explanation = unlines [ "Compute TERM by concrete syntax definitions. Uses the topmost", "module (the last one imported) to resolve constant names.", - "N.B.1 You need the flag -retain when importing the grammar, if you want", - "the definitions to be retained after compilation.", + "N.B.1 You need the flag -retain or -resource when importing the grammar,", + "if you want the definitions to be available after compilation.", "N.B.2 The resulting term is not a tree in the sense of abstract syntax", "and hence not a valid input to a Tree-expecting command.", "This command must be a line of its own, and thus cannot be a part", @@ -109,8 +111,9 @@ sourceCommands = Map.fromList [ synopsis = "show all operations in scope, possibly restricted to a value type", explanation = unlines [ "Show the names and type signatures of all operations available in the current resource.", - "This command requires a source grammar to be in scope, imported with 'import -retain'.", - "The operations include the parameter constructors that are in scope.", + "If no grammar is loaded with 'import -retain' or 'import -resource',", + "then only the predefined operations are in scope.", + "The operations include also the parameter constructors that are in scope.", "The optional TYPE filters according to the value type.", "The grep STRINGs filter according to other substrings of the type signatures."{-, "This command must be a line of its own, and thus cannot be a part", @@ -198,24 +201,22 @@ sourceCommands = Map.fromList [ | otherwise = unwords $ map prTerm ops return $ fromString printed - show_operations os ts sgr = fmap fst $ runCheck $ - case greatestResource sgr of - Nothing -> checkError (pp "no source grammar in scope; did you import with -retain?") - Just mo -> do - let greps = map valueString (listFlags "grep" os) - let isRaw = isOpt "raw" os - ops <- case ts of - _:_ -> do - let Right t = runP pExp (UTF8.fromString (unwords ts)) - ty <- checkComputeTerm os sgr t - return $ allOpersTo sgr ty - _ -> return $ allOpers sgr - let sigs = [(op,ty) | ((mo,op),ty,pos) <- ops] - let printer = if isRaw - then showTerm sgr TermPrintDefault Qualified - else (render . TC.ppType) - let printed = [unwords [showIdent op, ":", printer ty] | (op,ty) <- sigs] - return . fromString $ unlines [l | l <- printed, all (`isInfixOf` l) greps] + show_operations os ts sgr0 = fmap fst $ runCheck $ do + let (sgr,mo) = case greatestResource sgr0 of + Nothing -> (mGrammar [predefMod], fst predefMod) + Just mo -> (sgr0,mo) + greps = map valueString (listFlags "grep" os) + ops <- case ts of + _:_ -> do let Right t = runP pExp (UTF8.fromString (unwords ts)) + ty <- checkComputeTerm os sgr t + return $ allOpersTo sgr ty + _ -> return $ allOpers sgr + let sigs = [(op,ty) | ((mo,op),ty,pos) <- ops] + printer = if isOpt "raw" os + then showTerm sgr TermPrintDefault Qualified + else (render . TC.ppType) + printed = [unwords [showIdent op, ":", printer ty] | (op,ty) <- sigs] + return . fromString $ unlines [l | l <- printed, all (`isInfixOf` l) greps] show_source os ts sgr = do let strip = if isOpt "strip" os then stripSourceGrammar else id @@ -251,9 +252,10 @@ sourceCommands = Map.fromList [ P.putStrLn "wrote graph in file _gfdepgraph.dot" return void -checkComputeTerm os sgr t = - do mo <- maybe (checkError (pp "no source grammar in scope")) return $ - greatestResource sgr +checkComputeTerm os sgr0 t = + do let (sgr,mo) = case greatestResource sgr0 of + Nothing -> (mGrammar [predefMod], fst predefMod) + Just mo -> (sgr0,mo) t <- renameSourceTerm sgr mo t (t,_) <- inferLType sgr [] t fmap evalStr (normalForm sgr t) diff --git a/src/compiler/GF/Compile/TypeCheck/Primitives.hs b/src/compiler/GF/Compile/TypeCheck/Primitives.hs index 8f9d977b46..5edd88108d 100644 --- a/src/compiler/GF/Compile/TypeCheck/Primitives.hs +++ b/src/compiler/GF/Compile/TypeCheck/Primitives.hs @@ -1,5 +1,6 @@ -module GF.Compile.TypeCheck.Primitives where +module GF.Compile.TypeCheck.Primitives(typPredefined,predefMod) where +import GF.Infra.Option import GF.Grammar import GF.Grammar.Predef import qualified Data.Map as Map @@ -11,6 +12,21 @@ typPredefined f = case Map.lookup f primitives of Just (ResValue (L _ ty) _) -> Just ty _ -> Nothing +predefMod = (cPredef, modInfo) + where + modInfo = ModInfo { + mtype = MTResource, + mstatus = MSComplete, + mflags = noOptions, + mextend = [], + mwith = Nothing, + mopens = [], + mexdeps = [], + msrc = "Predef.gfo", + mseqs = Nothing, + jments = primitives + } + primitives = Map.fromList [ (cErrorType, ResOper (Just (noLoc typeType)) Nothing) , (cInt , ResOper (Just (noLoc typePType)) Nothing) diff --git a/src/compiler/GF/Interactive.hs b/src/compiler/GF/Interactive.hs index ca781972f2..f6be8795be 100644 --- a/src/compiler/GF/Interactive.hs +++ b/src/compiler/GF/Interactive.hs @@ -14,6 +14,7 @@ import GF.Command.Abstract import GF.Command.Parse(readCommandLine,pCommand,readTransactionCommand) import GF.Compile.Rename(renameSourceTerm) import GF.Compile.TypeCheck.Concrete(inferLType) +import GF.Compile.TypeCheck.Primitives(predefMod) import GF.Compile.GeneratePMCFG(pmcfgForm,type2fields) import GF.Data.Operations (Err(..)) import GF.Data.Utilities(whenM,repeatM) @@ -283,10 +284,11 @@ transactionCommand (CreateConcrete opts name) pgf mb_txnid = do lift $ updatePGF pgf mb_txnid (createConcrete name (return ())) return () transactionCommand (CreateLin opts f t is_alter) pgf mb_txnid = do - sgr <- getGrammar + sgr0 <- getGrammar + let (sgr,mo) = case greatestResource sgr0 of + Nothing -> (mGrammar [predefMod], fst predefMod) + Just mo -> (sgr0,mo) lang <- optLang pgf opts - mo <- maybe (fail "no source grammar in scope") return $ - greatestResource sgr lift $ updatePGF pgf mb_txnid $ do mb_ty <- getFunctionType f case mb_ty of @@ -319,10 +321,11 @@ transactionCommand (CreateLin opts f t is_alter) pgf mb_txnid = do mapToSequence m = Seq.fromList (map (Left . fst) (sortOn snd (Map.toList m))) transactionCommand (CreateLincat opts c t) pgf mb_txnid = do - sgr <- getGrammar + sgr0 <- getGrammar + let (sgr,mo) = case greatestResource sgr0 of + Nothing -> (mGrammar [predefMod], fst predefMod) + Just mo -> (sgr0,mo) lang <- optLang pgf opts - mo <- maybe (fail "no source grammar in scope") return $ - greatestResource sgr case runCheck (compileLincatTerm sgr mo t) of Ok (fields,_)-> do lift $ updatePGF pgf mb_txnid (alterConcrete lang (createLincat c fields [] [] Seq.empty >> return ())) return () From bd9bd8b32f61f010a2cb0d38146d0671c7b985eb Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Fri, 24 Nov 2023 08:35:11 +0100 Subject: [PATCH 04/15] the experimental typechecker is almost converted to the new evaluator --- src/compiler/GF/Compile/Compute/Concrete.hs | 50 +- .../GF/Compile/TypeCheck/ConcreteNew.hs | 598 +++++++++--------- 2 files changed, 331 insertions(+), 317 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index 6b19a15e61..7844fcf93a 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -4,20 +4,22 @@ -- | preparation for PMCFG generation. module GF.Compile.Compute.Concrete ( normalForm - , Value(..), Thunk, ThunkState(..), Env, showValue + , Value(..), Thunk, ThunkState(..), Env, Scope, showValue , MetaThunks , EvalM(..), runEvalM, evalError , eval, apply, force, value2term, patternMatch , newThunk, newEvaluatedThunk , newResiduation, newNarrowing, getVariables - , getRef - , getResDef, getInfo, getAllParamValues + , getRef, setRef + , getResDef, getInfo, getResType, getAllParamValues ) where import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint import GF.Grammar hiding (Env, VGen, VApp, VRecType) -import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo,allParamValues) +import GF.Grammar.Lookup(lookupResDef,lookupResType, + lookupOrigInfo,lookupOverloadTypes, + allParamValues) import GF.Grammar.Predef import GF.Grammar.Lockfield(lockLabel) import GF.Grammar.Printer @@ -45,14 +47,18 @@ normalForm gr t = mkFV [t] = t mkFV ts = FV ts +type Sigma s = Value s + data ThunkState s = Unevaluated (Env s) Term | Evaluated {-# UNPACK #-} !Int (Value s) - | Residuation {-# UNPACK #-} !MetaId + | Hole {-# UNPACK #-} !MetaId + | Residuation {-# UNPACK #-} !MetaId (Scope s) (Value s) | Narrowing {-# UNPACK #-} !MetaId Type type Thunk s = STRef s (ThunkState s) type Env s = [(Ident,Thunk s)] +type Scope s = [(Ident,Value s)] data Value s = VApp QIdent [Thunk s] @@ -131,7 +137,7 @@ eval env (App t1 t2) vs = do tnk <- newThunk env t2 eval env t1 (tnk : vs) eval env (Abs b x t) [] = return (VClosure env (Abs b x t)) eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs -eval env (Meta i) vs = do tnk <- newResiduation i +eval env (Meta i) vs = do tnk <- newHole i return (VMeta tnk env vs) eval env (ImplArg t) [] = eval env t [] eval env (Prod b x t1 t2)[] = do v1 <- eval env t1 [] @@ -733,6 +739,12 @@ getInfo q = EvalM $ \gr k mt d r -> do Ok res -> k res mt d r Bad msg -> return (Fail (pp msg)) +getResType :: QIdent -> EvalM s Type +getResType q = EvalM $ \gr k mt d r -> do + case lookupResType gr q of + Ok t -> k t mt d r + Bad msg -> return (Fail (pp msg)) + getAllParamValues :: Type -> EvalM s [Term] getAllParamValues ty = EvalM $ \gr k mt d r -> case allParamValues gr ty of @@ -747,15 +759,19 @@ newEvaluatedThunk v = EvalM $ \gr k mt d r -> do tnk <- newSTRef (Evaluated maxBound v) k tnk mt d r -newResiduation i = EvalM $ \gr k mt d r -> +newHole i = EvalM $ \gr k mt d r -> if i == 0 - then do tnk <- newSTRef (Residuation i) + then do tnk <- newSTRef (Hole i) k tnk mt d r else case Map.lookup i mt of Just tnk -> k tnk mt d r - Nothing -> do tnk <- newSTRef (Residuation i) + Nothing -> do tnk <- newSTRef (Hole i) k tnk (Map.insert i tnk mt) d r +newResiduation scope ty = EvalM $ \gr k mt d r -> do + tnk <- newSTRef (Residuation 0 scope ty) + k tnk mt d r + newNarrowing i ty = EvalM $ \gr k mt d r -> if i == 0 then do tnk <- newSTRef (Narrowing i ty) @@ -788,6 +804,7 @@ getVariables = EvalM $ \gr k mt d r -> do _ -> metas2params gr tnks getRef tnk = EvalM $ \gr k mt d r -> readSTRef tnk >>= \st -> k st mt d r +setRef tnk st = EvalM $ \gr k mt d r -> writeSTRef tnk st >>= \st -> k () mt d r force tnk = EvalM $ \gr k mt d r -> do s <- readSTRef tnk @@ -799,7 +816,8 @@ force tnk = EvalM $ \gr k mt d r -> do writeSTRef tnk s return r) mt d r Evaluated d v -> k v mt d r - Residuation _ -> k (VMeta tnk [] []) mt d r + Hole _ -> k (VMeta tnk [] []) mt d r + Residuation _ _ _ -> k (VMeta tnk [] []) mt d r Narrowing _ _ -> k (VMeta tnk [] []) mt d r tnk2term xs tnk = EvalM $ \gr k mt d r -> @@ -835,13 +853,15 @@ tnk2term xs tnk = EvalM $ \gr k mt d r -> Fail msg -> return (Fail msg) Success (r,0,xs) -> k (FV []) mt d r Success (r,c,xs) -> flush xs (\mt r -> return (Success r)) mt r - Residuation i -> k (Meta i) mt d r + Hole i -> k (Meta i) mt d r + Residuation i _ _ -> k (Meta i) mt d r Narrowing i _ -> k (Meta i) mt d r zonk tnk vs = EvalM $ \gr k mt d r -> do s <- readSTRef tnk case s of - Evaluated _ v -> case apply v vs of - EvalM f -> f gr (k . Left) mt d r - Residuation i -> k (Right i) mt d r - Narrowing i _ -> k (Right i) mt d r + Evaluated _ v -> case apply v vs of + EvalM f -> f gr (k . Left) mt d r + Hole i -> k (Right i) mt d r + Residuation i _ _ -> k (Right i) mt d r + Narrowing i _ -> k (Right i) mt d r diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index e71858975f..6eab451ab9 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -14,7 +14,7 @@ import GF.Compile.Compute.Concrete import GF.Infra.CheckM import GF.Data.Operations import Control.Applicative(Applicative(..)) -import Control.Monad(ap,liftM,mplus,foldM) +import Control.Monad(ap,liftM,mplus,foldM,zipWithM) import Control.Monad.ST import GF.Text.Pretty import Data.List (nub, (\\), tails) @@ -62,308 +62,319 @@ tcRho scope t@(Vr v) mb_ty = do -- VAR Just v_sigma -> instSigma scope t v_sigma mb_ty Nothing -> tcError ("Unknown variable" <+> v) tcRho scope t@(Q id) mb_ty = - runTcA (tcOverloadFailed t) $ - tcApp scope t `bindTcA` \(t,ty) -> + runTcA (tcOverloadFailed t) $ \gr -> + tcApp gr scope t `bindTcA` \(t,ty) -> instSigma scope t ty mb_ty tcRho scope t@(QC id) mb_ty = - runTcA (tcOverloadFailed t) $ - tcApp scope t `bindTcA` \(t,ty) -> + runTcA (tcOverloadFailed t) $ \gr -> + tcApp gr scope t `bindTcA` \(t,ty) -> instSigma scope t ty mb_ty tcRho scope t@(App fun arg) mb_ty = do - runTcA (tcOverloadFailed t) $ - tcApp scope t `bindTcA` \(t,ty) -> + runTcA (tcOverloadFailed t) $ \gr -> + tcApp gr scope t `bindTcA` \(t,ty) -> instSigma scope t ty mb_ty -{-tcRho scope (Abs bt var body) Nothing = do -- ABS1 - i <- newMeta scope vtypeType - let arg_ty = VMeta i (scopeEnv scope) [] +tcRho scope (Abs bt var body) Nothing = do -- ABS1 + tnk <- liftEvalM (newResiduation scope vtypeType) + env <- scopeEnv scope + let arg_ty = VMeta tnk env [] (body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing - return (Abs bt var body, (VProd bt arg_ty identW body_ty)) -tcRho ge scope t@(Abs Implicit var body) (Just ty) = do -- ABS2 - (bt, var_ty, body_ty) <- unifyFun ge scope ty + return (Abs bt var body, (VProd bt identW arg_ty body_ty)) +tcRho scope t@(Abs Implicit var body) (Just ty) = do -- ABS2 + (bt, var_ty, body_ty) <- unifyFun scope ty if bt == Implicit then return () else tcError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") - (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) []))) + (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (Abs Implicit var body,ty) -tcRho ge scope (Abs Explicit var body) (Just ty) = do -- ABS3 - (scope,f,ty') <- skolemise ge scope ty - (_,var_ty,body_ty) <- unifyFun ge scope ty' - (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) []))) +tcRho scope (Abs Explicit var body) (Just ty) = do -- ABS3 + (scope,f,ty') <- skolemise scope ty + (_,var_ty,body_ty) <- unifyFun scope ty' + (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (f (Abs Explicit var body),ty) -tcRho ge scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET +tcRho scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET (rhs,var_ty) <- case mb_ann_ty of - Nothing -> inferSigma ge scope rhs - Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType) - v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty) - (rhs,_) <- tcRho ge scope rhs (Just v_ann_ty) + Nothing -> inferSigma scope rhs + Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType) + env <- scopeEnv scope + v_ann_ty <- liftEvalM (eval env ann_ty []) + (rhs,_) <- tcRho scope rhs (Just v_ann_ty) return (rhs, v_ann_ty) - (body, body_ty) <- tcRho ge ((var,var_ty):scope) body mb_ty - var_ty <- tc_value2term (geLoc ge) (scopeVars scope) var_ty + (body, body_ty) <- tcRho ((var,var_ty):scope) body mb_ty + var_ty <- liftEvalM (value2term (scopeVars scope) var_ty) return (Let (var, (Just var_ty, rhs)) body, body_ty) -tcRho ge scope (Typed body ann_ty) mb_ty = do -- ANNOT - (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType) - v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty) - (body,_) <- tcRho ge scope body (Just v_ann_ty) - instSigma ge scope (Typed body ann_ty) v_ann_ty mb_ty -tcRho ge scope (FV ts) mb_ty = do +tcRho scope (Typed body ann_ty) mb_ty = do -- ANNOT + (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType) + env <- scopeEnv scope + v_ann_ty <- liftEvalM (eval env ann_ty []) + (body,_) <- tcRho scope body (Just v_ann_ty) + instSigma scope (Typed body ann_ty) v_ann_ty mb_ty +tcRho scope (FV ts) mb_ty = do case ts of - [] -> do i <- newMeta scope vtypeType - instSigma ge scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty - (t:ts) -> do (t,ty) <- tcRho ge scope t mb_ty + [] -> do i <- liftEvalM (newResiduation scope vtypeType) + env <- scopeEnv scope + instSigma scope (FV []) (VMeta i env []) mb_ty + (t:ts) -> do (t,ty) <- tcRho scope t mb_ty let go [] ty = return ([],ty) - go (t:ts) ty = do (t, ty) <- tcRho ge scope t (Just ty) + go (t:ts) ty = do (t, ty) <- tcRho scope t (Just ty) (ts,ty) <- go ts ty return (t:ts,ty) (ts,ty) <- go ts ty return (FV (t:ts), ty) -tcRho ge scope t@(Sort s) mb_ty = do - instSigma ge scope t vtypeType mb_ty -tcRho ge scope t@(RecType rs) Nothing = do - (rs,mb_ty) <- tcRecTypeFields ge scope rs Nothing +tcRho scope t@(Sort s) mb_ty = do + instSigma scope t vtypeType mb_ty +tcRho scope t@(RecType rs) Nothing = do + (rs,mb_ty) <- tcRecTypeFields scope rs Nothing return (RecType rs,fromMaybe vtypePType mb_ty) -tcRho ge scope t@(RecType rs) (Just ty) = do - (scope,f,ty') <- skolemise ge scope ty +tcRho scope t@(RecType rs) (Just ty) = do + (scope,f,ty') <- skolemise scope ty case ty' of VSort s | s == cType -> return () | s == cPType -> return () VMeta i env vs -> case rs of - [] -> unifyVar ge scope i env vs vtypePType + [] -> unifyVar scope i env vs vtypePType _ -> return () - ty -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty + ty -> do ty <- zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty) tcError ("The record type" <+> ppTerm Unqualified 0 t $$ "cannot be of type" <+> ppTerm Unqualified 0 ty) - (rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty') + (rs,mb_ty) <- tcRecTypeFields scope rs (Just ty') return (f (RecType rs),ty) -tcRho ge scope t@(Table p res) mb_ty = do - (p, p_ty) <- tcRho ge scope p (Just vtypePType) - (res,res_ty) <- tcRho ge scope res (Just vtypeType) - instSigma ge scope (Table p res) vtypeType mb_ty -tcRho ge scope (Prod bt x ty1 ty2) mb_ty = do - (ty1,ty1_ty) <- tcRho ge scope ty1 (Just vtypeType) - vty1 <- liftErr (eval ge (scopeEnv scope) ty1) - (ty2,ty2_ty) <- tcRho ge ((x,vty1):scope) ty2 (Just vtypeType) - instSigma ge scope (Prod bt x ty1 ty2) vtypeType mb_ty -tcRho ge scope (S t p) mb_ty = do - p_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypePType +tcRho scope t@(Table p res) mb_ty = do + (p, p_ty) <- tcRho scope p (Just vtypePType) + (res,res_ty) <- tcRho scope res (Just vtypeType) + instSigma scope (Table p res) vtypeType mb_ty +tcRho scope (Prod bt x ty1 ty2) mb_ty = do + (ty1,ty1_ty) <- tcRho scope ty1 (Just vtypeType) + env <- scopeEnv scope + vty1 <- liftEvalM (eval env ty1 []) + (ty2,ty2_ty) <- tcRho ((x,vty1):scope) ty2 (Just vtypeType) + instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty +tcRho scope (S t p) mb_ty = do + env <- scopeEnv scope + p_ty <- fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypePType) res_ty <- case mb_ty of - Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType + Nothing -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypeType) Just ty -> return ty - let t_ty = VTblType p_ty res_ty - (t,t_ty) <- tcRho ge scope t (Just t_ty) - (p,_) <- tcRho ge scope p (Just p_ty) + let t_ty = VTable p_ty res_ty + (t,t_ty) <- tcRho scope t (Just t_ty) + (p,_) <- tcRho scope p (Just p_ty) return (S t p, res_ty) -tcRho ge scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables +tcRho scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables + env <- scopeEnv scope p_ty <- case tt of - TRaw -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypePType - TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType) - liftErr (eval ge (scopeEnv scope) ty) - (ps,mb_res_ty) <- tcCases ge scope ps p_ty Nothing + TRaw -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypePType) + TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) + liftEvalM (eval env ty []) + (ps,mb_res_ty) <- tcCases scope ps p_ty Nothing res_ty <- case mb_res_ty of Just res_ty -> return res_ty - Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType - p_ty_t <- tc_value2term (geLoc ge) [] p_ty - return (T (TTyped p_ty_t) ps, VTblType p_ty res_ty) -tcRho ge scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables - (scope,f,ty') <- skolemise ge scope ty - (p_ty, res_ty) <- unifyTbl ge scope ty' + Nothing -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypeType) + p_ty_t <- liftEvalM (value2term [] p_ty) + return (T (TTyped p_ty_t) ps, VTable p_ty res_ty) +tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables + (scope,f,ty') <- skolemise scope ty + (p_ty, res_ty) <- unifyTbl scope ty' case tt of TRaw -> return () - TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType) + TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) return ()--subsCheckRho ge scope -> Term ty res_ty - (ps,Just res_ty) <- tcCases ge scope ps p_ty (Just res_ty) - p_ty_t <- tc_value2term (geLoc ge) [] p_ty - return (f (T (TTyped p_ty_t) ps), VTblType p_ty res_ty) -tcRho ge scope (R rs) Nothing = do - lttys <- inferRecFields ge scope rs - rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys + (ps,Just res_ty) <- tcCases scope ps p_ty (Just res_ty) + p_ty_t <- liftEvalM (value2term [] p_ty) + return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) +tcRho scope (R rs) Nothing = do + lttys <- inferRecFields scope rs + rs <- liftEvalM (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) return (R rs, VRecType [(l, ty) | (l,t,ty) <- lttys] ) -tcRho ge scope (R rs) (Just ty) = do - (scope,f,ty') <- skolemise ge scope ty +tcRho scope (R rs) (Just ty) = do + (scope,f,ty') <- skolemise scope ty case ty' of - (VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys - rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys + (VRecType ltys) -> do lttys <- checkRecFields scope rs ltys + rs <- liftEvalM (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) return ((f . R) rs, VRecType [(l, ty) | (l,t,ty) <- lttys] ) - ty -> do lttys <- inferRecFields ge scope rs - t <- liftM (f . R) (mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) + ty -> do lttys <- inferRecFields scope rs + t <- liftEvalM (liftM (f . R) (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)) let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys] - t <- subsCheckRho ge scope t ty' ty + t <- subsCheckRho scope t ty' ty return (t, ty') -tcRho ge scope (P t l) mb_ty = do +tcRho scope (P t l) mb_ty = do l_ty <- case mb_ty of Just ty -> return ty - Nothing -> do i <- newMeta scope vtypeType - return (VMeta i (scopeEnv scope) []) - (t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,l_ty)])) + Nothing -> do env <- scopeEnv scope + i <- liftEvalM (newEvaluatedThunk vtypeType) + return (VMeta i env []) + (t,t_ty) <- tcRho scope t (Just (VRecType [(l,l_ty)])) return (P t l,l_ty) -tcRho ge scope (C t1 t2) mb_ty = do - (t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr) - (t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr) - instSigma ge scope (C t1 t2) vtypeStr mb_ty -tcRho ge scope (Glue t1 t2) mb_ty = do - (t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr) - (t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr) - instSigma ge scope (Glue t1 t2) vtypeStr mb_ty -tcRho ge scope t@(ExtR t1 t2) mb_ty = do - (t1,t1_ty) <- tcRho ge scope t1 Nothing - (t2,t2_ty) <- tcRho ge scope t2 Nothing +tcRho scope (C t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho scope t1 (Just vtypeStr) + (t2,t2_ty) <- tcRho scope t2 (Just vtypeStr) + instSigma scope (C t1 t2) vtypeStr mb_ty +tcRho scope (Glue t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho scope t1 (Just vtypeStr) + (t2,t2_ty) <- tcRho scope t2 (Just vtypeStr) + instSigma scope (Glue t1 t2) vtypeStr mb_ty +tcRho scope t@(ExtR t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho scope t1 Nothing + (t2,t2_ty) <- tcRho scope t2 Nothing case (t1_ty,t2_ty) of (VSort s1,VSort s2) | (s1 == cType || s1 == cPType) && (s2 == cType || s2 == cPType) -> let sort | s1 == cPType && s2 == cPType = cPType | otherwise = cType - in instSigma ge scope (ExtR t1 t2) (VSort sort) mb_ty - (VRecType rs1, VRecType rs2) -> instSigma ge scope (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty + in instSigma scope (ExtR t1 t2) (VSort sort) mb_ty + (VRecType rs1, VRecType rs2) -> instSigma scope (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty _ -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t) -tcRho ge scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser - tcRho ge scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty -tcRho ge scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser - tcRho ge scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty -tcRho ge scope (Alts t ss) mb_ty = do - (t,_) <- tcRho ge scope t (Just vtypeStr) +tcRho scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty +tcRho scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty +tcRho scope (Alts t ss) mb_ty = do + (t,_) <- tcRho scope t (Just vtypeStr) ss <- flip mapM ss $ \(t1,t2) -> do - (t1,_) <- tcRho ge scope t1 (Just vtypeStr) - (t2,_) <- tcRho ge scope t2 (Just vtypeStrs) + (t1,_) <- tcRho scope t1 (Just vtypeStr) + (t2,_) <- tcRho scope t2 (Just vtypeStrs) return (t1,t2) - instSigma ge scope (Alts t ss) vtypeStr mb_ty -tcRho ge scope (Strs ss) mb_ty = do + instSigma scope (Alts t ss) vtypeStr mb_ty +tcRho scope (Strs ss) mb_ty = do ss <- flip mapM ss $ \t -> do - (t,_) <- tcRho ge scope t (Just vtypeStr) + (t,_) <- tcRho scope t (Just vtypeStr) return t - instSigma ge scope (Strs ss) vtypeStrs mb_ty -tcRho ge scope (EPattType ty) mb_ty = do - (ty, _) <- tcRho ge scope ty (Just vtypeType) - instSigma ge scope (EPattType ty) vtypeType mb_ty -tcRho ge scope t@(EPatt p) mb_ty = do + instSigma scope (Strs ss) vtypeStrs mb_ty +tcRho scope (EPattType ty) mb_ty = do + (ty, _) <- tcRho scope ty (Just vtypeType) + instSigma scope (EPattType ty) vtypeType mb_ty +tcRho scope t@(EPatt min max p) mb_ty = do (scope,f,ty) <- case mb_ty of - Nothing -> do i <- newMeta scope vtypeType - return (scope,id,VMeta i (scopeEnv scope) []) - Just ty -> do (scope,f,ty) <- skolemise ge scope ty + Nothing -> do env <- scopeEnv scope + i <- liftEvalM (newEvaluatedThunk vtypeType) + return (scope,id,VMeta i env []) + Just ty -> do (scope,f,ty) <- skolemise scope ty case ty of VPattType ty -> return (scope,f,ty) _ -> tcError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected") - tcPatt ge scope p ty - return (f (EPatt p), ty) -tcRho gr scope t _ = unimplemented ("tcRho "++show t) - -tcCases ge scope [] p_ty mb_res_ty = return ([],mb_res_ty) -tcCases ge scope ((p,t):cs) p_ty mb_res_ty = do - scope' <- tcPatt ge scope p p_ty - (t,res_ty) <- tcRho ge scope' t mb_res_ty - (cs,mb_res_ty) <- tcCases ge scope cs p_ty (Just res_ty) + tcPatt scope p ty + return (f (EPatt min max p), ty) +tcRho scope t _ = unimplemented ("tcRho "++show t) + +tcCases scope [] p_ty mb_res_ty = return ([],mb_res_ty) +tcCases scope ((p,t):cs) p_ty mb_res_ty = do + scope' <- tcPatt scope p p_ty + (t,res_ty) <- tcRho scope' t mb_res_ty + (cs,mb_res_ty) <- tcCases scope cs p_ty (Just res_ty) return ((p,t):cs,mb_res_ty) --} -tcApp scope t@(App fun (ImplArg arg)) = undefined {- do -- APP1 - tcApp ge scope fun `bindTcA` \(fun,fun_ty) -> - do (bt, arg_ty, res_ty) <- unifyFun ge scope fun_ty +tcApp gr scope t@(App fun (ImplArg arg)) = do -- APP1 + tcApp gr scope fun `bindTcA` \(fun,fun_ty) -> + do (bt, arg_ty, res_ty) <- unifyFun scope fun_ty if (bt == Implicit) then return () else tcError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected") - (arg,_) <- tcRho ge scope arg (Just arg_ty) - varg <- liftErr (eval ge (scopeEnv scope) arg) - return (App fun (ImplArg arg), res_ty varg) -tcApp ge scope (App fun arg) = -- APP2 - tcApp ge scope fun `bindTcA` \(fun,fun_ty) -> + (arg,_) <- tcRho scope arg (Just arg_ty) + env <- scopeEnv scope + varg <- liftEvalM (eval env arg []) + return (App fun (ImplArg arg), res_ty) +tcApp gr scope (App fun arg) = -- APP2 + tcApp gr scope fun `bindTcA` \(fun,fun_ty) -> do (fun,fun_ty) <- instantiate scope fun fun_ty - (_, arg_ty, res_ty) <- unifyFun ge scope fun_ty - (arg,_) <- tcRho ge scope arg (Just arg_ty) - varg <- liftErr (eval ge (scopeEnv scope) arg) - return (App fun arg, res_ty varg) -tcApp ge scope (Q id) = -- VAR (global) - mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> - do ty <- liftErr (eval ge [] ty) + (_, arg_ty, res_ty) <- unifyFun scope fun_ty + (arg,_) <- tcRho scope arg (Just arg_ty) + env <- scopeEnv scope + varg <- liftEvalM (eval env arg []) + return (App fun arg, res_ty) +tcApp gr scope (Q id) = do -- VAR (global) + mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) -> + do ty <- liftEvalM (eval [] ty []) return (t,ty) -tcApp ge scope (QC id) = -- VAR (global) - mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> - do ty <- liftErr (eval ge [] ty) +tcApp gr scope (QC id) = -- VAR (global) + mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) -> + do ty <- liftEvalM (eval [] ty []) return (t,ty) -tcApp ge scope t = - singleTcA (tcRho ge scope t Nothing) +tcApp gr scope t = + singleTcA (tcRho scope t Nothing) + --} tcOverloadFailed t ttys = tcError ("Overload resolution failed" $$ "of term " <+> pp t $$ "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys]) -{- -tcPatt ge scope PW ty0 = + +tcPatt scope PW ty0 = return scope -tcPatt ge scope (PV x) ty0 = +tcPatt scope (PV x) ty0 = return ((x,ty0):scope) -tcPatt ge scope (PP c ps) ty0 = - case lookupResType (geGrammar ge) c of - Ok ty -> do let go scope ty [] = return (scope,ty) - go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun ge scope ty - scope <- tcPatt ge scope p arg_ty - go scope (res_ty (VGen (length scope) [])) ps - vty <- liftErr (eval ge [] ty) - (scope,ty) <- go scope vty ps - unify ge scope ty0 ty - return scope - Bad err -> tcError (pp err) -tcPatt ge scope (PInt i) ty0 = do - subsCheckRho ge scope (EInt i) (vtypeInts i) ty0 +tcPatt scope (PP c ps) ty0 = do + ty <- liftEvalM (getResType c) + let go scope ty [] = return (scope,ty) + go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun scope ty + scope <- tcPatt scope p arg_ty + go scope res_ty ps + vty <- liftEvalM (eval [] ty []) + (scope,ty) <- go scope vty ps + unify scope ty0 ty return scope -tcPatt ge scope (PString s) ty0 = do - unify ge scope ty0 vtypeStr +tcPatt scope (PInt i) ty0 = do + ty <- vtypeInts i + subsCheckRho scope (EInt i) ty ty0 return scope -tcPatt ge scope PChar ty0 = do - unify ge scope ty0 vtypeStr +tcPatt scope (PString s) ty0 = do + unify scope ty0 vtypeStr return scope -tcPatt ge scope (PSeq _ _ p1 _ _ p2) ty0 = do - unify ge scope ty0 vtypeStr - scope <- tcPatt ge scope p1 vtypeStr - scope <- tcPatt ge scope p2 vtypeStr +tcPatt scope PChar ty0 = do + unify scope ty0 vtypeStr return scope -tcPatt ge scope (PAs x p) ty0 = do - tcPatt ge ((x,ty0):scope) p ty0 -tcPatt ge scope (PR rs) ty0 = do +tcPatt scope (PSeq _ _ p1 _ _ p2) ty0 = do + unify scope ty0 vtypeStr + scope <- tcPatt scope p1 vtypeStr + scope <- tcPatt scope p2 vtypeStr + return scope +tcPatt scope (PAs x p) ty0 = do + tcPatt ((x,ty0):scope) p ty0 +tcPatt scope (PR rs) ty0 = do let mk_ltys [] = return [] - mk_ltys ((l,p):rs) = do i <- newMeta scope vtypePType + mk_ltys ((l,p):rs) = do i <- liftEvalM (newEvaluatedThunk vtypePType) ltys <- mk_ltys rs - return ((l,p,VMeta i (scopeEnv scope) []) : ltys) + env <- scopeEnv scope + return ((l,p,VMeta i env []) : ltys) go scope [] = return scope - go scope ((l,p,ty):rs) = do scope <- tcPatt ge scope p ty + go scope ((l,p,ty):rs) = do scope <- tcPatt scope p ty go scope rs ltys <- mk_ltys rs - subsCheckRho ge scope (EPatt (PR rs)) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0 + subsCheckRho scope (EPatt 0 Nothing (PR rs)) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0 go scope ltys -tcPatt ge scope (PAlt p1 p2) ty0 = do - tcPatt ge scope p1 ty0 - tcPatt ge scope p2 ty0 +tcPatt scope (PAlt p1 p2) ty0 = do + tcPatt scope p1 ty0 + tcPatt scope p2 ty0 return scope -tcPatt ge scope (PM q) ty0 = do - case lookupResType (geGrammar ge) q of - Ok (EPattType ty) - -> do vty <- liftErr (eval ge [] ty) - unify ge scope ty0 vty +tcPatt scope (PM q) ty0 = do + ty <- liftEvalM (getResType q) + case ty of + EPattType ty + -> do vty <- liftEvalM (eval [] ty []) + unify scope ty0 vty return scope - Ok ty -> tcError ("Pattern type expected but " <+> pp ty <+> " found.") - Bad err -> tcError (pp err) -tcPatt ge scope p ty = unimplemented ("tcPatt "++show p) + ty -> tcError ("Pattern type expected but " <+> pp ty <+> " found.") +tcPatt scope p ty = unimplemented ("tcPatt "++show p) -inferRecFields ge scope rs = - mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs +inferRecFields scope rs = + mapM (\(l,r) -> tcRecField scope l r Nothing) rs -checkRecFields ge scope [] ltys +checkRecFields scope [] ltys | null ltys = return [] | otherwise = tcError ("Missing fields:" <+> hsep (map fst ltys)) -checkRecFields ge scope ((l,t):lts) ltys = +checkRecFields scope ((l,t):lts) ltys = case takeIt l ltys of - (Just ty,ltys) -> do ltty <- tcRecField ge scope l t (Just ty) - lttys <- checkRecFields ge scope lts ltys + (Just ty,ltys) -> do ltty <- tcRecField scope l t (Just ty) + lttys <- checkRecFields scope lts ltys return (ltty : lttys) (Nothing,ltys) -> do tcWarn ("Discarded field:" <+> l) - ltty <- tcRecField ge scope l t Nothing - lttys <- checkRecFields ge scope lts ltys + ltty <- tcRecField scope l t Nothing + lttys <- checkRecFields scope lts ltys return lttys -- ignore the field where takeIt l1 [] = (Nothing, []) @@ -372,29 +383,30 @@ checkRecFields ge scope ((l,t):lts) ltys = | otherwise = let (mb_ty,ltys') = takeIt l1 ltys in (mb_ty,lty:ltys') -tcRecField ge scope l (mb_ann_ty,t) mb_ty = do +tcRecField scope l (mb_ann_ty,t) mb_ty = do (t,ty) <- case mb_ann_ty of - Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType) - v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty) - (t,_) <- tcRho ge scope t (Just v_ann_ty) - instSigma ge scope t v_ann_ty mb_ty - Nothing -> tcRho ge scope t mb_ty + Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType) + env <- scopeEnv scope + v_ann_ty <- liftEvalM (eval env ann_ty []) + (t,_) <- tcRho scope t (Just v_ann_ty) + instSigma scope t v_ann_ty mb_ty + Nothing -> tcRho scope t mb_ty return (l,t,ty) -tcRecTypeFields ge scope [] mb_ty = return ([],mb_ty) -tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do - (ty,sort) <- tcRho ge scope ty mb_ty +tcRecTypeFields scope [] mb_ty = return ([],mb_ty) +tcRecTypeFields scope ((l,ty):rs) mb_ty = do + (ty,sort) <- tcRho scope ty mb_ty mb_ty <- case sort of VSort s | s == cType -> return (Just sort) | s == cPType -> return mb_ty VMeta _ _ _ -> return mb_ty - _ -> do sort <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) sort + _ -> do sort <- zonkTerm =<< liftEvalM (value2term (scopeVars scope) sort) tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ "cannot be of type" <+> ppTerm Unqualified 0 sort) - (rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty + (rs,mb_ty) <- tcRecTypeFields scope rs mb_ty return ((l,ty):rs,mb_ty) --} + -- | Invariant: if the third argument is (Just rho), -- then rho is in weak-prenex form instSigma :: Scope s -> Term -> Sigma s -> Maybe (Rho s) -> TcM s (Term, Rho s) @@ -405,21 +417,21 @@ instSigma scope t ty1 (Just ty2) = do -- INST2 -- | Invariant: the second argument is in weak-prenex form subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> TcM s Term -subsCheckRho scope t ty1@(VMeta i env vs) ty2 = undefined {- do - mv <- getMeta i +subsCheckRho scope t ty1@(VMeta i env vs) ty2 = do + mv <- liftEvalM (getRef i) case mv of - Unbound _ _ -> do unify ge scope ty1 ty2 - return t - Bound ty1 -> do vty1 <- liftErr (eval ge env ty1) - subsCheckRho ge scope t (vapply (geLoc ge) vty1 vs) ty2 -subsCheckRho ge scope t ty1 ty2@(VMeta i env vs) = do - mv <- getMeta i + Residuation _ _ _ -> do unify scope ty1 ty2 + return t + Evaluated _ vty1 -> do vty1 <- liftEvalM (apply vty1 vs) + subsCheckRho scope t vty1 ty2 +subsCheckRho scope t ty1 ty2@(VMeta i env vs) = do + mv <- liftEvalM (getRef i) case mv of - Unbound _ _ -> do unify ge scope ty1 ty2 - return t - Bound ty2 -> do vty2 <- liftErr (eval ge env ty2) - subsCheckRho ge scope t ty1 (vapply (geLoc ge) vty2 vs) -subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC + Residuation _ _ _ -> do unify scope ty1 ty2 + return t + Evaluated _ vty2 -> do vty2 <- liftEvalM (apply vty2 vs) + subsCheckRho scope t ty1 vty2 +{-subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC i <- newMeta scope ty1 subsCheckRho ge scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) rho2 subsCheckRho ge scope t rho1 (VProd Implicit ty1 x (Bind ty2)) = do -- Rule SKOL @@ -506,34 +518,35 @@ subsCheckTbl ge scope t p1 r1 p2 r2 = do t <- subsCheckRho ge ((x,vtypePType):scope) (S t xt) r1 r2 ; p2 <- tc_value2term (geLoc ge) (scopeVars scope) p2 return (T (TTyped p2) [(PV x,t)]) - +-} ----------------------------------------------------------------------- -- Unification ----------------------------------------------------------------------- -unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (BindType, Sigma, Value -> Rho) -unifyFun ge scope (VProd bt arg x (Bind res)) = +unifyFun :: Scope s -> Rho s -> TcM s (BindType, Sigma s, Rho s) +unifyFun scope (VProd bt x arg res) = return (bt,arg,res) -unifyFun ge scope tau = do +unifyFun scope tau = do let mk_val ty = VMeta ty [] [] - arg <- fmap mk_val $ newMeta scope vtypeType - res <- fmap mk_val $ newMeta scope vtypeType + arg <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType) + res <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType) let bt = Explicit - unify ge scope tau (VProd bt arg identW (Bind (const res))) - return (bt,arg,const res) + unify scope tau (VProd bt identW arg res) + return (bt,arg,res) -unifyTbl :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Rho) -unifyTbl ge scope (VTblType arg res) = +unifyTbl :: Scope s -> Rho s -> TcM s (Sigma s, Rho s) +unifyTbl scope (VTable arg res) = return (arg,res) -unifyTbl ge scope tau = do - let mk_val ty = VMeta ty (scopeEnv scope) [] - arg <- fmap mk_val $ newMeta scope vtypePType - res <- fmap mk_val $ newMeta scope vtypeType - unify ge scope tau (VTblType arg res) +unifyTbl scope tau = do + env <- scopeEnv scope + let mk_val ty = VMeta ty env [] + arg <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypePType) + res <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType) + unify scope tau (VTable arg res) return (arg,res) -unify ge scope (VApp f1 vs1) (VApp f2 vs2) - | f1 == f2 = sequence_ (zipWith (unify ge scope) vs1 vs2) +unify scope (VApp f1 vs1) (VApp f2 vs2) + | f1 == f2 = undefined {- sequence_ (zipWith (unify ge scope) vs1 vs2) unify ge scope (VCApp f1 vs1) (VCApp f2 vs2) | f1 == f2 = sequence_ (zipWith (unify ge scope) vs1 vs2) unify ge scope (VSort s1) (VSort s2) @@ -559,50 +572,48 @@ unify ge scope v1 v2 = do t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2 tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ ppTerm Unqualified 0 t2)) - +-} -- | Invariant: tv1 is a flexible type variable -unifyVar :: GlobalEnv -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM () -unifyVar ge scope i env vs ty2 = do -- Check whether i is bound - mv <- getMeta i +unifyVar :: Scope s -> Thunk s -> Env s -> [Thunk s] -> Tau s -> TcM s () +unifyVar scope tnk env vs ty2 = do -- Check whether i is bound + mv <- liftEvalM (getRef tnk) case mv of - Bound ty1 -> do v <- liftErr (eval ge env ty1) - unify ge scope (vapply (geLoc ge) v vs) ty2 - Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of - -- Left i -> let (v,_) = reverse scope !! i - -- in tcError ("Variable" <+> pp v <+> "has escaped") - ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)] - if i `elem` ms2 - then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$ - nest 2 (ppTerm Unqualified 0 ty2')) - else setMeta i (Bound ty2') + Unevaluated _ ty1 -> do v <- liftEvalM (eval env ty1 [] >>= \v -> apply v vs) + unify scope v ty2 + Residuation i scope' _ -> do ty2' <- liftEvalM (value2term (scopeVars scope') ty2) + ms2 <- getMetaVars [(scope,ty2)] + if i `elem` ms2 + then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$ + nest 2 (ppTerm Unqualified 0 ty2')) + else liftEvalM (setRef tnk (Unevaluated env ty2')) ----------------------------------------------------------------------- -- Instantiation and quantification ----------------------------------------------------------------------- -- | Instantiate the topmost implicit arguments with metavariables -instantiate :: Scope -> Term -> Sigma -> TcM (Term,Rho) -instantiate scope t (VProd Implicit ty1 x (Bind ty2)) = do +instantiate :: Scope s -> Term -> Sigma s -> TcM s (Term,Rho s) +instantiate scope t (VProd Implicit x ty1 ty2) = undefined {- do i <- newMeta scope ty1 - instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) + instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) -} instantiate scope t ty = do return (t,ty) -- | Build fresh lambda abstractions for the topmost implicit arguments -skolemise :: GlobalEnv -> Scope -> Sigma -> TcM (Scope, Term->Term, Rho) -skolemise ge scope ty@(VMeta i env vs) = do - mv <- getMeta i +skolemise :: Scope s -> Sigma s -> TcM s (Scope s, Term->Term, Rho s) +skolemise scope ty@(VMeta i env vs) = undefined {-do + mv <- getRef i case mv of - Unbound _ _ -> return (scope,id,ty) -- guarded constant? - Bound ty -> do vty <- liftErr (eval ge env ty) - skolemise ge scope (vapply (geLoc ge) vty vs) -skolemise ge scope (VProd Implicit ty1 x (Bind ty2)) = do + Residuation _ _ _ -> return (scope,id,ty) -- guarded constant? + Evaluated _ vty -> do vty <- liftEvalM (apply vty vs) + skolemise scope vty +skolemise scope (VProd Implicit ty1 x ty2) = do let v = newVar scope - (scope,f,ty2) <- skolemise ge ((v,ty1):scope) (ty2 (VGen (length scope) [])) - return (scope,Abs Implicit v . f,ty2) -skolemise ge scope ty = do - return (scope,id,ty) --} + (scope,f,ty2) <- skolemise ((v,ty1):scope) (ty2 (VGen (length scope) [])) + return (scope,undefined {-Abs Implicit v . f-},ty2) +skolemise scope ty = do + return (scope,undefined,ty)-} + -- | Quantify over the specified type variables (all flexible) quantify :: Scope s -> Term -> [MetaId] -> Rho s -> TcM s (Term,Sigma s) quantify scope t tvs ty0 = undefined {- do @@ -618,17 +629,16 @@ quantify scope t tvs ty0 = undefined {- do bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2 bndrs _ = [] - +-} allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,... allBinders = [ identS [x] | x <- ['a'..'z'] ] ++ [ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']] --} + ----------------------------------------------------------------------- -- The Monad ----------------------------------------------------------------------- -type Scope s = [(Ident,Value s)] type Sigma s = Value s type Rho s = Value s -- No top-level ForAll type Tau s = Value s -- No ForAlls anywhere @@ -697,39 +707,23 @@ liftEvalM (EvalM f) = TcM $ \gr ms msgs -> do Success (x,ms) -> return (TcOk x ms []) Fail msg -> return (TcFail [msg]) - - -newMeta :: Scope s -> Sigma s -> TcM s MetaId -newMeta scope ty = undefined {- TcM (\ms msgs -> - let i = IntMap.size ms - in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs) - -getMeta :: MetaId -> TcM MetaValue -getMeta i = TcM (\ms msgs -> - case IntMap.lookup i ms of - Just mv -> TcOk mv ms msgs - Nothing -> TcFail (("Unknown metavariable" <+> ppMeta i) : msgs)) - -setMeta :: MetaId -> MetaValue -> TcM () -setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs) - -newVar :: Scope -> Ident +newVar :: Scope s -> Ident newVar scope = head [x | i <- [1..], let x = identS ('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..] + +scopeEnv scope = zipWithM (\(x,ty) i -> liftEvalM (newEvaluatedThunk (VGen i [])) >>= \tnk -> return (x,tnk)) (reverse scope) [0..] scopeVars scope = map fst scope scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope) -- | This function takes account of zonking, and returns a set -- (no duplicates) of unbound meta-type variables getMetaVars :: [(Scope s,Sigma s)] -> TcM s [MetaId] -getMetaVars sc_tys = undefined {- do - tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys +getMetaVars sc_tys = do + tys <- mapM (\(scope,ty) -> zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)) sc_tys return (foldr go [] tys) where -- Get the MetaIds from a term; no duplicates in result @@ -748,9 +742,9 @@ getMetaVars sc_tys = undefined {- do -- | This function takes account of zonking, and returns a set -- (no duplicates) of free type variables -getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident] -getFreeVars loc sc_tys = do - tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys +getFreeVars :: [(Scope s,Sigma s)] -> TcM s [Ident] +getFreeVars sc_tys = do + tys <- mapM (\(scope,ty) -> zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)) sc_tys return (foldr (go []) [] tys) where go bound (Vr tv) acc @@ -764,7 +758,7 @@ getFreeVars loc sc_tys = do go bound (Prod _ x arg res) acc = go bound arg (go (x : bound) res acc) go bound (RecType rs) acc = foldl (\acc (l,ty) -> go bound ty acc) acc rs go bound (Table p t) acc = go bound p (go bound t acc) --} + -- | Eliminate any substitutions in a term zonkTerm :: Term -> TcM s Term zonkTerm (Meta i) = undefined {- do @@ -802,8 +796,8 @@ bindTcA f g = case f of TcFail _ -> return rs TcOk y ms msgs -> return ((y,ms,msgs):rs) -runTcA :: ([x] -> TcM s a) -> TcA s x a -> TcM s a -runTcA g f = TcM (\gr ms msgs -> case f of +runTcA :: ([x] -> TcM s a) -> (SourceGrammar -> TcA s x a) -> TcM s a +runTcA g f = TcM (\gr ms msgs -> case f gr of TcMany xs f -> do rs <- f gr ms msgs case rs of [(x,ms,msgs)] -> return (TcOk x ms msgs) From 4f28d2b3a3b735d4ffd7c22c4c9db98806806ed3 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Fri, 24 Nov 2023 09:40:28 +0100 Subject: [PATCH 05/15] the evaluator and the typechecker now share the same monad --- src/compiler/GF/Compile/Compute/Concrete.hs | 217 +++++++------- .../GF/Compile/TypeCheck/ConcreteNew.hs | 278 +++++++----------- src/compiler/GF/Infra/CheckM.hs | 58 ++-- 3 files changed, 250 insertions(+), 303 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index 7844fcf93a..d0e89863e1 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -6,7 +6,7 @@ module GF.Compile.Compute.Concrete ( normalForm , Value(..), Thunk, ThunkState(..), Env, Scope, showValue , MetaThunks - , EvalM(..), runEvalM, evalError + , EvalM(..), runEvalM, runEvalOneM, evalError, evalWarn , eval, apply, force, value2term, patternMatch , newThunk, newEvaluatedThunk , newResiduation, newNarrowing, getVariables @@ -450,30 +450,30 @@ vtableSelect v0 ty tnks tnk2 vs = do "cannot be evaluated at compile time.") -susp i env ki = EvalM $ \gr k mt d r -> do +susp i env ki = EvalM $ \gr k mt d r msgs -> do s <- readSTRef i case s of Narrowing id (QC q) -> case lookupOrigInfo gr q of - Ok (m,ResParam (Just (L _ ps)) _) -> bindParam gr k mt d r s m ps - Bad msg -> return (Fail (pp msg)) + Ok (m,ResParam (Just (L _ ps)) _) -> bindParam gr k mt d r msgs s m ps + Bad msg -> return (Fail (pp msg) msgs) Narrowing id ty | Just max <- isTypeInts ty - -> bindInt gr k mt d r s 0 max + -> bindInt gr k mt d r msgs s 0 max Evaluated _ v -> case ki v of - EvalM f -> f gr k mt d r - _ -> k (VSusp i env ki []) mt d r + EvalM f -> f gr k mt d r msgs + _ -> k (VSusp i env ki []) mt d r msgs where - bindParam gr k mt d r s m [] = return (Success r) - bindParam gr k mt d r s m ((p, ctxt):ps) = do + bindParam gr k mt d r msgs s m [] = return (Success r msgs) + bindParam gr k mt d r msgs s m ((p, ctxt):ps) = do (mt',tnks) <- mkArgs mt ctxt let v = VApp (m,p) tnks writeSTRef i (Evaluated (length env) v) res <- case ki v of - EvalM f -> f gr k mt' d r + EvalM f -> f gr k mt' d r msgs writeSTRef i s case res of - Fail msg -> return (Fail msg) - Success r -> bindParam gr k mt d r s m ps + Fail msg msgs -> return (Fail msg msgs) + Success r msgs -> bindParam gr k mt d r msgs s m ps mkArgs mt [] = return (mt,[]) mkArgs mt ((_,_,ty):ctxt) = do @@ -484,17 +484,17 @@ susp i env ki = EvalM $ \gr k mt d r -> do (mt,tnks) <- mkArgs (Map.insert i tnk mt) ctxt return (mt,tnk:tnks) - bindInt gr k mt d r s iv max + bindInt gr k mt d r msgs s iv max | iv <= max = do let v = VInt iv writeSTRef i (Evaluated (length env) v) res <- case ki v of - EvalM f -> f gr k mt d r + EvalM f -> f gr k mt d r msgs writeSTRef i s case res of - Fail msg -> return (Fail msg) - Success r -> bindInt gr k mt d r s (iv+1) max - | otherwise = return (Success r) + Fail msg msgs -> return (Fail msg msgs) + Success r msgs -> bindInt gr k mt d r msgs s (iv+1) max + | otherwise = return (Success r msgs) value2term xs (VApp q tnks) = @@ -686,7 +686,7 @@ value2int _ = RunTime -- * Evaluation monad type MetaThunks s = Map.Map MetaId (Thunk s) -type Cont s r = MetaThunks s -> Int -> r -> ST s (CheckResult r) +type Cont s r = MetaThunks s -> Int -> r -> [Message] -> ST s (CheckResult r [Message]) newtype EvalM s a = EvalM (forall r . Grammar -> (a -> Cont s r) -> Cont s r) instance Functor (EvalM s) where @@ -705,90 +705,101 @@ instance Monad (EvalM s) where #endif instance Fail.MonadFail (EvalM s) where - fail msg = EvalM (\gr k _ _ r -> return (Fail (pp msg))) + fail msg = EvalM (\gr k _ _ r msgs -> return (Fail (pp msg) msgs)) instance Alternative (EvalM s) where - empty = EvalM (\gr k _ _ r -> return (Success r)) - (EvalM f) <|> (EvalM g) = EvalM $ \gr k mt b r -> do - res <- f gr k mt b r + empty = EvalM (\gr k _ _ r msgs -> return (Success r msgs)) + (EvalM f) <|> (EvalM g) = EvalM $ \gr k mt b r msgs -> do + res <- f gr k mt b r msgs case res of - Fail msg -> return (Fail msg) - Success r -> g gr k mt b r + Fail msg msgs -> return (Fail msg msgs) + Success r msgs -> g gr k mt b r msgs instance MonadPlus (EvalM s) where runEvalM :: Grammar -> (forall s . EvalM s a) -> Check [a] -runEvalM gr f = +runEvalM gr f = Check $ \(es,ws) -> case runST (case f of - EvalM f -> f gr (\x mt _ xs -> return (Success (x:xs))) Map.empty maxBound []) of - Fail msg -> checkError msg - Success xs -> return (reverse xs) + EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) Map.empty maxBound [] ws) of + Fail msg ws -> Fail msg (es,ws) + Success xs ws -> Success (reverse xs) (es,ws) -evalError :: Doc -> EvalM s a -evalError msg = EvalM (\gr k _ _ r -> return (Fail msg)) +runEvalOneM :: Grammar -> (forall s . EvalM s a) -> Check a +runEvalOneM gr f = Check $ \(es,ws) -> + case runST (case f of + EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) Map.empty maxBound [] ws) of + Fail msg ws -> Fail msg (es,ws) + Success [] ws -> Fail (pp "The evaluation produced no results") (es,ws) + Success (x:_) ws -> Success x (es,ws) + +evalError :: Message -> EvalM s a +evalError msg = EvalM (\gr k _ _ r msgs -> return (Fail msg msgs)) +evalWarn :: Message -> EvalM s () +evalWarn msg = EvalM (\gr k mt d r msgs -> k () mt d r (msg:msgs)) + getResDef :: QIdent -> EvalM s Term -getResDef q = EvalM $ \gr k mt d r -> do +getResDef q = EvalM $ \gr k mt d r msgs -> do case lookupResDef gr q of - Ok t -> k t mt d r - Bad msg -> return (Fail (pp msg)) + Ok t -> k t mt d r msgs + Bad msg -> return (Fail (pp msg) msgs) getInfo :: QIdent -> EvalM s (ModuleName,Info) -getInfo q = EvalM $ \gr k mt d r -> do +getInfo q = EvalM $ \gr k mt d r msgs -> do case lookupOrigInfo gr q of - Ok res -> k res mt d r - Bad msg -> return (Fail (pp msg)) + Ok res -> k res mt d r msgs + Bad msg -> return (Fail (pp msg) msgs) getResType :: QIdent -> EvalM s Type -getResType q = EvalM $ \gr k mt d r -> do +getResType q = EvalM $ \gr k mt d r msgs -> do case lookupResType gr q of - Ok t -> k t mt d r - Bad msg -> return (Fail (pp msg)) + Ok t -> k t mt d r msgs + Bad msg -> return (Fail (pp msg) msgs) getAllParamValues :: Type -> EvalM s [Term] -getAllParamValues ty = EvalM $ \gr k mt d r -> +getAllParamValues ty = EvalM $ \gr k mt d r msgs -> case allParamValues gr ty of - Ok ts -> k ts mt d r - Bad msg -> return (Fail (pp msg)) + Ok ts -> k ts mt d r msgs + Bad msg -> return (Fail (pp msg) msgs) -newThunk env t = EvalM $ \gr k mt d r -> do +newThunk env t = EvalM $ \gr k mt d r msgs -> do tnk <- newSTRef (Unevaluated env t) - k tnk mt d r + k tnk mt d r msgs -newEvaluatedThunk v = EvalM $ \gr k mt d r -> do +newEvaluatedThunk v = EvalM $ \gr k mt d r msgs -> do tnk <- newSTRef (Evaluated maxBound v) - k tnk mt d r + k tnk mt d r msgs -newHole i = EvalM $ \gr k mt d r -> +newHole i = EvalM $ \gr k mt d r msgs -> if i == 0 then do tnk <- newSTRef (Hole i) - k tnk mt d r + k tnk mt d r msgs else case Map.lookup i mt of - Just tnk -> k tnk mt d r + Just tnk -> k tnk mt d r msgs Nothing -> do tnk <- newSTRef (Hole i) - k tnk (Map.insert i tnk mt) d r + k tnk (Map.insert i tnk mt) d r msgs -newResiduation scope ty = EvalM $ \gr k mt d r -> do +newResiduation scope ty = EvalM $ \gr k mt d r msgs -> do tnk <- newSTRef (Residuation 0 scope ty) - k tnk mt d r + k tnk mt d r msgs -newNarrowing i ty = EvalM $ \gr k mt d r -> +newNarrowing i ty = EvalM $ \gr k mt d r msgs -> if i == 0 then do tnk <- newSTRef (Narrowing i ty) - k tnk mt d r + k tnk mt d r msgs else case Map.lookup i mt of - Just tnk -> k tnk mt d r + Just tnk -> k tnk mt d r msgs Nothing -> do tnk <- newSTRef (Narrowing i ty) - k tnk (Map.insert i tnk mt) d r + k tnk (Map.insert i tnk mt) d r msgs -withVar d0 (EvalM f) = EvalM $ \gr k mt d1 r -> +withVar d0 (EvalM f) = EvalM $ \gr k mt d1 r msgs -> let !d = min d0 d1 - in f gr k mt d r + in f gr k mt d r msgs getVariables :: EvalM s [(LVar,LIndex)] -getVariables = EvalM $ \gr k mt d r -> do +getVariables = EvalM $ \gr k mt d ws r -> do ps <- metas2params gr (Map.elems mt) - k ps mt d r + k ps mt d ws r where metas2params gr [] = return [] metas2params gr (tnk:tnks) = do @@ -803,65 +814,65 @@ getVariables = EvalM $ \gr k mt d r -> do else return params _ -> metas2params gr tnks -getRef tnk = EvalM $ \gr k mt d r -> readSTRef tnk >>= \st -> k st mt d r -setRef tnk st = EvalM $ \gr k mt d r -> writeSTRef tnk st >>= \st -> k () mt d r +getRef tnk = EvalM $ \gr k mt d ws r -> readSTRef tnk >>= \st -> k st mt d ws r +setRef tnk st = EvalM $ \gr k mt d ws r -> writeSTRef tnk st >>= \st -> k () mt d ws r -force tnk = EvalM $ \gr k mt d r -> do +force tnk = EvalM $ \gr k mt d r msgs -> do s <- readSTRef tnk case s of Unevaluated env t -> case eval env t [] of - EvalM f -> f gr (\v mt b r -> do let d = length env - writeSTRef tnk (Evaluated d v) - r <- k v mt d r - writeSTRef tnk s - return r) mt d r - Evaluated d v -> k v mt d r - Hole _ -> k (VMeta tnk [] []) mt d r - Residuation _ _ _ -> k (VMeta tnk [] []) mt d r - Narrowing _ _ -> k (VMeta tnk [] []) mt d r - -tnk2term xs tnk = EvalM $ \gr k mt d r -> + EvalM f -> f gr (\v mt b r msgs -> do let d = length env + writeSTRef tnk (Evaluated d v) + r <- k v mt d r msgs + writeSTRef tnk s + return r) mt d r msgs + Evaluated d v -> k v mt d r msgs + Hole _ -> k (VMeta tnk [] []) mt d r msgs + Residuation _ _ _ -> k (VMeta tnk [] []) mt d r msgs + Narrowing _ _ -> k (VMeta tnk [] []) mt d r msgs + +tnk2term xs tnk = EvalM $ \gr k mt d r msgs -> let join f g = do res <- f case res of - Fail msg -> return (Fail msg) - Success r -> g r + Fail msg msgs -> return (Fail msg msgs) + Success r msgs -> g r msgs - flush [] k1 mt r = k1 mt r - flush [x] k1 mt r = join (k x mt d r) (k1 mt) - flush xs k1 mt r = join (k (FV (reverse xs)) mt d r) (k1 mt) + flush [] k1 mt r msgs = k1 mt r msgs + flush [x] k1 mt r msgs = join (k x mt d r msgs) (k1 mt) + flush xs k1 mt r msgs = join (k (FV (reverse xs)) mt d r msgs) (k1 mt) - acc d0 x mt d (r,!c,xs) - | d < d0 = flush xs (\mt r -> join (k x mt d r) (\r -> return (Success (r,c+1,[])))) mt r - | otherwise = return (Success (r,c+1,x:xs)) + acc d0 x mt d (r,!c,xs) msgs + | d < d0 = flush xs (\mt r msgs -> join (k x mt d r msgs) (\r msgs -> return (Success (r,c+1,[]) msgs))) mt r msgs + | otherwise = return (Success (r,c+1,x:xs) msgs) in do s <- readSTRef tnk case s of Unevaluated env t -> do let d0 = length env res <- case eval env t [] of - EvalM f -> f gr (\v mt d r -> do writeSTRef tnk (Evaluated d0 v) - r <- case value2term xs v of - EvalM f -> f gr (acc d0) mt d r - writeSTRef tnk s - return r) mt maxBound (r,0,[]) + EvalM f -> f gr (\v mt d msgs r -> do writeSTRef tnk (Evaluated d0 v) + r <- case value2term xs v of + EvalM f -> f gr (acc d0) mt d msgs r + writeSTRef tnk s + return r) mt maxBound (r,0,[]) msgs case res of - Fail msg -> return (Fail msg) - Success (r,0,xs) -> k (FV []) mt d r - Success (r,c,xs) -> flush xs (\mt r -> return (Success r)) mt r + Fail msg msgs -> return (Fail msg msgs) + Success (r,0,xs) msgs -> k (FV []) mt d r msgs + Success (r,c,xs) msgs -> flush xs (\mt msgs r -> return (Success msgs r)) mt r msgs Evaluated d0 v -> do res <- case value2term xs v of - EvalM f -> f gr (acc d0) mt maxBound (r,0,[]) + EvalM f -> f gr (acc d0) mt maxBound (r,0,[]) msgs case res of - Fail msg -> return (Fail msg) - Success (r,0,xs) -> k (FV []) mt d r - Success (r,c,xs) -> flush xs (\mt r -> return (Success r)) mt r - Hole i -> k (Meta i) mt d r - Residuation i _ _ -> k (Meta i) mt d r - Narrowing i _ -> k (Meta i) mt d r - -zonk tnk vs = EvalM $ \gr k mt d r -> do + Fail msg msgs -> return (Fail msg msgs) + Success (r,0,xs) msgs -> k (FV []) mt d r msgs + Success (r,c,xs) msgs -> flush xs (\mt r msgs -> return (Success r msgs)) mt r msgs + Hole i -> k (Meta i) mt d r msgs + Residuation i _ _ -> k (Meta i) mt d r msgs + Narrowing i _ -> k (Meta i) mt d r msgs + +zonk tnk vs = EvalM $ \gr k mt d r msgs -> do s <- readSTRef tnk case s of Evaluated _ v -> case apply v vs of - EvalM f -> f gr (k . Left) mt d r - Hole i -> k (Right i) mt d r - Residuation i _ _ -> k (Right i) mt d r - Narrowing i _ -> k (Right i) mt d r + EvalM f -> f gr (k . Left) mt d r msgs + Hole i -> k (Right i) mt d r msgs + Residuation i _ _ -> k (Right i) mt d r msgs + Narrowing i _ -> k (Right i) mt d r msgs diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index 6eab451ab9..7a1b3e594f 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -23,20 +23,20 @@ import Data.Maybe(fromMaybe,isNothing) import qualified Control.Monad.Fail as Fail checkLType :: Grammar -> Term -> Type -> Check (Term, Type) -checkLType gr t ty = runTcM gr $ do - vty <- liftEvalM (eval [] ty []) +checkLType gr t ty = runEvalOneM gr $ do + vty <- eval [] ty [] (t,_) <- tcRho [] t (Just vty) t <- zonkTerm t return (t,ty) inferLType :: Grammar -> Term -> Check (Term, Type) -inferLType gr t = runTcM gr $ do +inferLType gr t = runEvalOneM gr $ do (t,ty) <- inferSigma [] t t <- zonkTerm t - ty <- zonkTerm =<< liftEvalM (value2term [] ty) + ty <- zonkTerm =<< value2term [] ty return (t,ty) -inferSigma :: Scope s -> Term -> TcM s (Term,Sigma s) +inferSigma :: Scope s -> Term -> EvalM s (Term,Sigma s) inferSigma scope t = do -- GEN1 (t,ty) <- tcRho scope t Nothing env_tvs <- getMetaVars (scopeTypes scope) @@ -46,13 +46,13 @@ inferSigma scope t = do -- GEN1 vtypeInt = VApp (cPredef,cInt) [] vtypeFloat = VApp (cPredef,cFloat) [] -vtypeInts i= liftEvalM (newEvaluatedThunk (VInt i)) >>= \tnk -> return (VApp (cPredef,cInts) [tnk]) +vtypeInts i= newEvaluatedThunk (VInt i) >>= \tnk -> return (VApp (cPredef,cInts) [tnk]) vtypeStr = VSort cStr vtypeStrs = VSort cStrs vtypeType = VSort cType vtypePType = VSort cPType -tcRho :: Scope s -> Term -> Maybe (Rho s) -> TcM s (Term, Rho s) +tcRho :: Scope s -> Term -> Maybe (Rho s) -> EvalM s (Term, Rho s) tcRho scope t@(EInt i) mb_ty = vtypeInts i >>= \sigma -> instSigma scope t sigma mb_ty -- INT tcRho scope t@(EFloat _) mb_ty = instSigma scope t vtypeFloat mb_ty -- FLOAT tcRho scope t@(K _) mb_ty = instSigma scope t vtypeStr mb_ty -- STR @@ -60,7 +60,7 @@ tcRho scope t@(Empty) mb_ty = instSigma scope t vtypeStr mb_ty tcRho scope t@(Vr v) mb_ty = do -- VAR case lookup v scope of Just v_sigma -> instSigma scope t v_sigma mb_ty - Nothing -> tcError ("Unknown variable" <+> v) + Nothing -> evalError ("Unknown variable" <+> v) tcRho scope t@(Q id) mb_ty = runTcA (tcOverloadFailed t) $ \gr -> tcApp gr scope t `bindTcA` \(t,ty) -> @@ -74,7 +74,7 @@ tcRho scope t@(App fun arg) mb_ty = do tcApp gr scope t `bindTcA` \(t,ty) -> instSigma scope t ty mb_ty tcRho scope (Abs bt var body) Nothing = do -- ABS1 - tnk <- liftEvalM (newResiduation scope vtypeType) + tnk <- newResiduation scope vtypeType env <- scopeEnv scope let arg_ty = VMeta tnk env [] (body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing @@ -83,7 +83,7 @@ tcRho scope t@(Abs Implicit var body) (Just ty) = do -- ABS2 (bt, var_ty, body_ty) <- unifyFun scope ty if bt == Implicit then return () - else tcError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") + else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (Abs Implicit var body,ty) tcRho scope (Abs Explicit var body) (Just ty) = do -- ABS3 @@ -96,21 +96,21 @@ tcRho scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET Nothing -> inferSigma scope rhs Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType) env <- scopeEnv scope - v_ann_ty <- liftEvalM (eval env ann_ty []) + v_ann_ty <- eval env ann_ty [] (rhs,_) <- tcRho scope rhs (Just v_ann_ty) return (rhs, v_ann_ty) (body, body_ty) <- tcRho ((var,var_ty):scope) body mb_ty - var_ty <- liftEvalM (value2term (scopeVars scope) var_ty) + var_ty <- value2term (scopeVars scope) var_ty return (Let (var, (Just var_ty, rhs)) body, body_ty) tcRho scope (Typed body ann_ty) mb_ty = do -- ANNOT (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType) env <- scopeEnv scope - v_ann_ty <- liftEvalM (eval env ann_ty []) + v_ann_ty <- eval env ann_ty [] (body,_) <- tcRho scope body (Just v_ann_ty) instSigma scope (Typed body ann_ty) v_ann_ty mb_ty tcRho scope (FV ts) mb_ty = do case ts of - [] -> do i <- liftEvalM (newResiduation scope vtypeType) + [] -> do i <- newResiduation scope vtypeType env <- scopeEnv scope instSigma scope (FV []) (VMeta i env []) mb_ty (t:ts) -> do (t,ty) <- tcRho scope t mb_ty @@ -136,9 +136,9 @@ tcRho scope t@(RecType rs) (Just ty) = do VMeta i env vs -> case rs of [] -> unifyVar scope i env vs vtypePType _ -> return () - ty -> do ty <- zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty) - tcError ("The record type" <+> ppTerm Unqualified 0 t $$ - "cannot be of type" <+> ppTerm Unqualified 0 ty) + ty -> do ty <- zonkTerm =<< value2term (scopeVars scope) ty + evalError ("The record type" <+> ppTerm Unqualified 0 t $$ + "cannot be of type" <+> ppTerm Unqualified 0 ty) (rs,mb_ty) <- tcRecTypeFields scope rs (Just ty') return (f (RecType rs),ty) tcRho scope t@(Table p res) mb_ty = do @@ -148,14 +148,14 @@ tcRho scope t@(Table p res) mb_ty = do tcRho scope (Prod bt x ty1 ty2) mb_ty = do (ty1,ty1_ty) <- tcRho scope ty1 (Just vtypeType) env <- scopeEnv scope - vty1 <- liftEvalM (eval env ty1 []) + vty1 <- eval env ty1 [] (ty2,ty2_ty) <- tcRho ((x,vty1):scope) ty2 (Just vtypeType) instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty tcRho scope (S t p) mb_ty = do env <- scopeEnv scope - p_ty <- fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypePType) + p_ty <- fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypePType res_ty <- case mb_ty of - Nothing -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypeType) + Nothing -> fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypeType Just ty -> return ty let t_ty = VTable p_ty res_ty (t,t_ty) <- tcRho scope t (Just t_ty) @@ -164,14 +164,14 @@ tcRho scope (S t p) mb_ty = do tcRho scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables env <- scopeEnv scope p_ty <- case tt of - TRaw -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypePType) + TRaw -> fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypePType TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) - liftEvalM (eval env ty []) + eval env ty [] (ps,mb_res_ty) <- tcCases scope ps p_ty Nothing res_ty <- case mb_res_ty of Just res_ty -> return res_ty - Nothing -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypeType) - p_ty_t <- liftEvalM (value2term [] p_ty) + Nothing -> fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypeType + p_ty_t <- value2term [] p_ty return (T (TTyped p_ty_t) ps, VTable p_ty res_ty) tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables (scope,f,ty') <- skolemise scope ty @@ -181,11 +181,11 @@ tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for t TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) return ()--subsCheckRho ge scope -> Term ty res_ty (ps,Just res_ty) <- tcCases scope ps p_ty (Just res_ty) - p_ty_t <- liftEvalM (value2term [] p_ty) + p_ty_t <- value2term [] p_ty return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) tcRho scope (R rs) Nothing = do lttys <- inferRecFields scope rs - rs <- liftEvalM (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) + rs <- mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys return (R rs, VRecType [(l, ty) | (l,t,ty) <- lttys] ) @@ -193,12 +193,12 @@ tcRho scope (R rs) (Just ty) = do (scope,f,ty') <- skolemise scope ty case ty' of (VRecType ltys) -> do lttys <- checkRecFields scope rs ltys - rs <- liftEvalM (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) + rs <- mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys return ((f . R) rs, VRecType [(l, ty) | (l,t,ty) <- lttys] ) ty -> do lttys <- inferRecFields scope rs - t <- liftEvalM (liftM (f . R) (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)) + t <- liftM (f . R) (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys] t <- subsCheckRho scope t ty' ty return (t, ty') @@ -206,7 +206,7 @@ tcRho scope (P t l) mb_ty = do l_ty <- case mb_ty of Just ty -> return ty Nothing -> do env <- scopeEnv scope - i <- liftEvalM (newEvaluatedThunk vtypeType) + i <- newEvaluatedThunk vtypeType return (VMeta i env []) (t,t_ty) <- tcRho scope t (Just (VRecType [(l,l_ty)])) return (P t l,l_ty) @@ -228,7 +228,7 @@ tcRho scope t@(ExtR t1 t2) mb_ty = do | otherwise = cType in instSigma scope (ExtR t1 t2) (VSort sort) mb_ty (VRecType rs1, VRecType rs2) -> instSigma scope (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty - _ -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t) + _ -> evalError ("Cannot type check" <+> ppTerm Unqualified 0 t) tcRho scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser tcRho scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty tcRho scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser @@ -251,12 +251,12 @@ tcRho scope (EPattType ty) mb_ty = do tcRho scope t@(EPatt min max p) mb_ty = do (scope,f,ty) <- case mb_ty of Nothing -> do env <- scopeEnv scope - i <- liftEvalM (newEvaluatedThunk vtypeType) + i <- newEvaluatedThunk vtypeType return (scope,id,VMeta i env []) Just ty -> do (scope,f,ty) <- skolemise scope ty case ty of VPattType ty -> return (scope,f,ty) - _ -> tcError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected") + _ -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected") tcPatt scope p ty return (f (EPatt min max p), ty) tcRho scope t _ = unimplemented ("tcRho "++show t) @@ -273,10 +273,10 @@ tcApp gr scope t@(App fun (ImplArg arg)) = do -- APP1 do (bt, arg_ty, res_ty) <- unifyFun scope fun_ty if (bt == Implicit) then return () - else tcError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected") + else evalError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected") (arg,_) <- tcRho scope arg (Just arg_ty) env <- scopeEnv scope - varg <- liftEvalM (eval env arg []) + varg <- eval env arg [] return (App fun (ImplArg arg), res_ty) tcApp gr scope (App fun arg) = -- APP2 tcApp gr scope fun `bindTcA` \(fun,fun_ty) -> @@ -284,24 +284,24 @@ tcApp gr scope (App fun arg) = -- APP2 (_, arg_ty, res_ty) <- unifyFun scope fun_ty (arg,_) <- tcRho scope arg (Just arg_ty) env <- scopeEnv scope - varg <- liftEvalM (eval env arg []) + varg <- eval env arg [] return (App fun arg, res_ty) tcApp gr scope (Q id) = do -- VAR (global) mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) -> - do ty <- liftEvalM (eval [] ty []) + do ty <- eval [] ty [] return (t,ty) tcApp gr scope (QC id) = -- VAR (global) mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) -> - do ty <- liftEvalM (eval [] ty []) + do ty <- eval [] ty [] return (t,ty) tcApp gr scope t = singleTcA (tcRho scope t Nothing) tcOverloadFailed t ttys = - tcError ("Overload resolution failed" $$ - "of term " <+> pp t $$ - "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys]) + evalError ("Overload resolution failed" $$ + "of term " <+> pp t $$ + "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys]) tcPatt scope PW ty0 = @@ -309,12 +309,12 @@ tcPatt scope PW ty0 = tcPatt scope (PV x) ty0 = return ((x,ty0):scope) tcPatt scope (PP c ps) ty0 = do - ty <- liftEvalM (getResType c) + ty <- getResType c let go scope ty [] = return (scope,ty) go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun scope ty scope <- tcPatt scope p arg_ty go scope res_ty ps - vty <- liftEvalM (eval [] ty []) + vty <- eval [] ty [] (scope,ty) <- go scope vty ps unify scope ty0 ty return scope @@ -337,7 +337,7 @@ tcPatt scope (PAs x p) ty0 = do tcPatt ((x,ty0):scope) p ty0 tcPatt scope (PR rs) ty0 = do let mk_ltys [] = return [] - mk_ltys ((l,p):rs) = do i <- liftEvalM (newEvaluatedThunk vtypePType) + mk_ltys ((l,p):rs) = do i <- newEvaluatedThunk vtypePType ltys <- mk_ltys rs env <- scopeEnv scope return ((l,p,VMeta i env []) : ltys) @@ -352,13 +352,13 @@ tcPatt scope (PAlt p1 p2) ty0 = do tcPatt scope p2 ty0 return scope tcPatt scope (PM q) ty0 = do - ty <- liftEvalM (getResType q) + ty <- getResType q case ty of EPattType ty - -> do vty <- liftEvalM (eval [] ty []) + -> do vty <- eval [] ty [] unify scope ty0 vty return scope - ty -> tcError ("Pattern type expected but " <+> pp ty <+> " found.") + ty -> evalError ("Pattern type expected but " <+> pp ty <+> " found.") tcPatt scope p ty = unimplemented ("tcPatt "++show p) inferRecFields scope rs = @@ -366,13 +366,13 @@ inferRecFields scope rs = checkRecFields scope [] ltys | null ltys = return [] - | otherwise = tcError ("Missing fields:" <+> hsep (map fst ltys)) + | otherwise = evalError ("Missing fields:" <+> hsep (map fst ltys)) checkRecFields scope ((l,t):lts) ltys = case takeIt l ltys of (Just ty,ltys) -> do ltty <- tcRecField scope l t (Just ty) lttys <- checkRecFields scope lts ltys return (ltty : lttys) - (Nothing,ltys) -> do tcWarn ("Discarded field:" <+> l) + (Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l) ltty <- tcRecField scope l t Nothing lttys <- checkRecFields scope lts ltys return lttys -- ignore the field @@ -387,7 +387,7 @@ tcRecField scope l (mb_ann_ty,t) mb_ty = do (t,ty) <- case mb_ann_ty of Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType) env <- scopeEnv scope - v_ann_ty <- liftEvalM (eval env ann_ty []) + v_ann_ty <- eval env ann_ty [] (t,_) <- tcRho scope t (Just v_ann_ty) instSigma scope t v_ann_ty mb_ty Nothing -> tcRho scope t mb_ty @@ -401,35 +401,35 @@ tcRecTypeFields scope ((l,ty):rs) mb_ty = do | s == cType -> return (Just sort) | s == cPType -> return mb_ty VMeta _ _ _ -> return mb_ty - _ -> do sort <- zonkTerm =<< liftEvalM (value2term (scopeVars scope) sort) - tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ - "cannot be of type" <+> ppTerm Unqualified 0 sort) + _ -> do sort <- zonkTerm =<< value2term (scopeVars scope) sort + evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ + "cannot be of type" <+> ppTerm Unqualified 0 sort) (rs,mb_ty) <- tcRecTypeFields scope rs mb_ty return ((l,ty):rs,mb_ty) -- | Invariant: if the third argument is (Just rho), -- then rho is in weak-prenex form -instSigma :: Scope s -> Term -> Sigma s -> Maybe (Rho s) -> TcM s (Term, Rho s) +instSigma :: Scope s -> Term -> Sigma s -> Maybe (Rho s) -> EvalM s (Term, Rho s) instSigma scope t ty1 Nothing = return (t,ty1) -- INST1 instSigma scope t ty1 (Just ty2) = do -- INST2 t <- subsCheckRho scope t ty1 ty2 return (t,ty2) -- | Invariant: the second argument is in weak-prenex form -subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> TcM s Term +subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> EvalM s Term subsCheckRho scope t ty1@(VMeta i env vs) ty2 = do - mv <- liftEvalM (getRef i) + mv <- getRef i case mv of Residuation _ _ _ -> do unify scope ty1 ty2 return t - Evaluated _ vty1 -> do vty1 <- liftEvalM (apply vty1 vs) + Evaluated _ vty1 -> do vty1 <- apply vty1 vs subsCheckRho scope t vty1 ty2 subsCheckRho scope t ty1 ty2@(VMeta i env vs) = do - mv <- liftEvalM (getRef i) + mv <- getRef i case mv of Residuation _ _ _ -> do unify scope ty1 ty2 return t - Evaluated _ vty2 -> do vty2 <- liftEvalM (apply vty2 vs) + Evaluated _ vty2 -> do vty2 <- apply vty2 vs subsCheckRho scope t ty1 vty2 {-subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC i <- newMeta scope ty1 @@ -458,7 +458,7 @@ subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j]) -- Rule | predefName p1 == cInts && predefName p2 == cInts = if i <= j then return t - else tcError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j) + else evalError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j) subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC let mkAccess scope t = case t of @@ -494,15 +494,15 @@ subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule let fields = [(l,ty2,lookup l rs1) | (l,ty2) <- rs2] case [l | (l,_,Nothing) <- fields] of [] -> return () - missing -> tcError ("In the term" <+> pp t $$ - "there are no values for fields:" <+> hsep missing) + missing -> evalError ("In the term" <+> pp t $$ + "there are no values for fields:" <+> hsep missing) rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]] return (mkWrap (R rs)) subsCheckRho ge scope t tau1 tau2 = do -- Rule EQ unify ge scope tau1 tau2 -- Revert to ordinary unification return t -subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> (Value -> Rho) -> Sigma -> (Value -> Rho) -> TcM Term +subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> (Value -> Rho) -> Sigma -> (Value -> Rho) -> EvalM Term subsCheckFun ge scope t a1 r1 a2 r2 = do let v = newVar scope vt <- subsCheckRho ge ((v,a2):scope) (Vr v) a2 a1 @@ -511,7 +511,7 @@ subsCheckFun ge scope t a1 r1 a2 r2 = do t <- subsCheckRho ge ((v,vtypeType):scope) (App t vt) (r1 val1) (r2 val2) return (Abs Explicit v t) -subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term +subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term subsCheckTbl ge scope t p1 r1 p2 r2 = do let x = newVar scope xt <- subsCheckRho ge scope (Vr x) p2 p1 @@ -523,25 +523,25 @@ subsCheckTbl ge scope t p1 r1 p2 r2 = do -- Unification ----------------------------------------------------------------------- -unifyFun :: Scope s -> Rho s -> TcM s (BindType, Sigma s, Rho s) +unifyFun :: Scope s -> Rho s -> EvalM s (BindType, Sigma s, Rho s) unifyFun scope (VProd bt x arg res) = return (bt,arg,res) unifyFun scope tau = do let mk_val ty = VMeta ty [] [] - arg <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType) - res <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType) + arg <- fmap mk_val $ newEvaluatedThunk vtypeType + res <- fmap mk_val $ newEvaluatedThunk vtypeType let bt = Explicit unify scope tau (VProd bt identW arg res) return (bt,arg,res) -unifyTbl :: Scope s -> Rho s -> TcM s (Sigma s, Rho s) +unifyTbl :: Scope s -> Rho s -> EvalM s (Sigma s, Rho s) unifyTbl scope (VTable arg res) = return (arg,res) unifyTbl scope tau = do env <- scopeEnv scope let mk_val ty = VMeta ty env [] - arg <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypePType) - res <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType) + arg <- fmap mk_val $ newEvaluatedThunk vtypePType + res <- fmap mk_val $ newEvaluatedThunk vtypeType unify scope tau (VTable arg res) return (arg,res) @@ -570,29 +570,29 @@ unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v unify ge scope v1 v2 = do t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1 t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2 - tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ - ppTerm Unqualified 0 t2)) + evalError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ + ppTerm Unqualified 0 t2)) -} -- | Invariant: tv1 is a flexible type variable -unifyVar :: Scope s -> Thunk s -> Env s -> [Thunk s] -> Tau s -> TcM s () +unifyVar :: Scope s -> Thunk s -> Env s -> [Thunk s] -> Tau s -> EvalM s () unifyVar scope tnk env vs ty2 = do -- Check whether i is bound - mv <- liftEvalM (getRef tnk) + mv <- getRef tnk case mv of - Unevaluated _ ty1 -> do v <- liftEvalM (eval env ty1 [] >>= \v -> apply v vs) + Unevaluated _ ty1 -> do v <- eval env ty1 [] >>= \v -> apply v vs unify scope v ty2 - Residuation i scope' _ -> do ty2' <- liftEvalM (value2term (scopeVars scope') ty2) + Residuation i scope' _ -> do ty2' <- value2term (scopeVars scope') ty2 ms2 <- getMetaVars [(scope,ty2)] if i `elem` ms2 - then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$ - nest 2 (ppTerm Unqualified 0 ty2')) - else liftEvalM (setRef tnk (Unevaluated env ty2')) + then evalError ("Occurs check for" <+> ppMeta i <+> "in:" $$ + nest 2 (ppTerm Unqualified 0 ty2')) + else setRef tnk (Unevaluated env ty2') ----------------------------------------------------------------------- -- Instantiation and quantification ----------------------------------------------------------------------- -- | Instantiate the topmost implicit arguments with metavariables -instantiate :: Scope s -> Term -> Sigma s -> TcM s (Term,Rho s) +instantiate :: Scope s -> Term -> Sigma s -> EvalM s (Term,Rho s) instantiate scope t (VProd Implicit x ty1 ty2) = undefined {- do i <- newMeta scope ty1 instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) -} @@ -600,12 +600,12 @@ instantiate scope t ty = do return (t,ty) -- | Build fresh lambda abstractions for the topmost implicit arguments -skolemise :: Scope s -> Sigma s -> TcM s (Scope s, Term->Term, Rho s) +skolemise :: Scope s -> Sigma s -> EvalM s (Scope s, Term->Term, Rho s) skolemise scope ty@(VMeta i env vs) = undefined {-do mv <- getRef i case mv of Residuation _ _ _ -> return (scope,id,ty) -- guarded constant? - Evaluated _ vty -> do vty <- liftEvalM (apply vty vs) + Evaluated _ vty -> do vty <- apply vty vs skolemise scope vty skolemise scope (VProd Implicit ty1 x ty2) = do let v = newVar scope @@ -615,7 +615,7 @@ skolemise scope ty = do return (scope,undefined,ty)-} -- | Quantify over the specified type variables (all flexible) -quantify :: Scope s -> Term -> [MetaId] -> Rho s -> TcM s (Term,Sigma s) +quantify :: Scope s -> Term -> [MetaId] -> Rho s -> EvalM s (Term,Sigma s) quantify scope t tvs ty0 = undefined {- do ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0 let used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use @@ -636,77 +636,15 @@ allBinders = [ identS [x] | x <- ['a'..'z'] ] ++ ----------------------------------------------------------------------- --- The Monad +-- Helpers ----------------------------------------------------------------------- type Sigma s = Value s type Rho s = Value s -- No top-level ForAll type Tau s = Value s -- No ForAlls anywhere -data TcResult s a - = TcOk a (MetaThunks s) [Message] - | TcFail [Message] -- First msg is error, the rest are warnings? -newtype TcM s a = TcM {unTcM :: Grammar -> MetaThunks s -> [Message] -> ST s (TcResult s a)} - -instance Monad (TcM s) where - return x = TcM (\gr ms msgs -> return (TcOk x ms msgs)) - f >>= g = TcM $ \gr ms msgs -> do - res <- unTcM f gr ms msgs - case res of - TcOk x ms msgs -> unTcM (g x) gr ms msgs - TcFail msgs -> return (TcFail msgs) - -#if !(MIN_VERSION_base(4,13,0)) - -- Monad(fail) will be removed in GHC 8.8+ - fail = Fail.fail -#endif - -instance Fail.MonadFail (TcM s) where - fail = tcError . pp - - -instance Applicative (TcM s) where - pure = return - (<*>) = ap - -instance Functor (TcM s) where - fmap f g = TcM $ \gr ms msgs -> do - res <- unTcM g gr ms msgs - case res of - TcOk x ms msgs -> return (TcOk (f x) ms msgs) - TcFail msgs -> return (TcFail msgs) - -instance ErrorMonad (TcM s) where - raise = tcError . pp - handle f g = TcM $ \gr ms msgs -> do - res <- unTcM f gr ms msgs - case res of - TcFail (msg:msgs) -> unTcM (g (render msg)) gr ms msgs - r -> return r - -tcError :: Message -> TcM s a -tcError msg = TcM (\gr ms msgs -> return (TcFail (msg : msgs))) - -tcWarn :: Message -> TcM s () -tcWarn msg = TcM (\gr ms msgs -> return (TcOk () ms (msg : msgs))) - unimplemented str = fail ("Unimplemented: "++str) - -runTcM :: Grammar -> (forall s . TcM s a) -> Check a -runTcM gr f = Check $ \(errs,wngs) -> runST $ do - res <- unTcM f gr Map.empty [] - case res of - TcOk x _ msgs -> return ((errs, wngs++msgs),Success x) - TcFail (msg:msgs) -> return ((errs, wngs++msgs),Fail msg) - -liftEvalM :: EvalM s a -> TcM s a -liftEvalM (EvalM f) = TcM $ \gr ms msgs -> do - res <- f gr (\x ms b r -> return (Success (x,ms))) ms maxBound undefined - case res of - Success (x,ms) -> return (TcOk x ms []) - Fail msg -> return (TcFail [msg]) - newVar :: Scope s -> Ident newVar scope = head [x | i <- [1..], let x = identS ('v':show i), @@ -715,15 +653,15 @@ newVar scope = head [x | i <- [1..], isFree [] x = True isFree ((y,_):scope) x = x /= y && isFree scope x -scopeEnv scope = zipWithM (\(x,ty) i -> liftEvalM (newEvaluatedThunk (VGen i [])) >>= \tnk -> return (x,tnk)) (reverse scope) [0..] +scopeEnv scope = zipWithM (\(x,ty) i -> newEvaluatedThunk (VGen i []) >>= \tnk -> return (x,tnk)) (reverse scope) [0..] scopeVars scope = map fst scope scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope) -- | This function takes account of zonking, and returns a set -- (no duplicates) of unbound meta-type variables -getMetaVars :: [(Scope s,Sigma s)] -> TcM s [MetaId] +getMetaVars :: [(Scope s,Sigma s)] -> EvalM s [MetaId] getMetaVars sc_tys = do - tys <- mapM (\(scope,ty) -> zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)) sc_tys + tys <- mapM (\(scope,ty) -> zonkTerm =<< value2term (scopeVars scope) ty) sc_tys return (foldr go [] tys) where -- Get the MetaIds from a term; no duplicates in result @@ -742,9 +680,9 @@ getMetaVars sc_tys = do -- | This function takes account of zonking, and returns a set -- (no duplicates) of free type variables -getFreeVars :: [(Scope s,Sigma s)] -> TcM s [Ident] +getFreeVars :: [(Scope s,Sigma s)] -> EvalM s [Ident] getFreeVars sc_tys = do - tys <- mapM (\(scope,ty) -> zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)) sc_tys + tys <- mapM (\(scope,ty) -> zonkTerm =<< value2term (scopeVars scope) ty) sc_tys return (foldr (go []) [] tys) where go bound (Vr tv) acc @@ -760,7 +698,7 @@ getFreeVars sc_tys = do go bound (Table p t) acc = go bound p (go bound t acc) -- | Eliminate any substitutions in a term -zonkTerm :: Term -> TcM s Term +zonkTerm :: Term -> EvalM s Term zonkTerm (Meta i) = undefined {- do mv <- getMeta i case mv of @@ -773,34 +711,34 @@ zonkTerm t = composOp zonkTerm t -} data TcA s x a - = TcSingle (Grammar -> MetaThunks s -> [Message] -> ST s (TcResult s a)) + = TcSingle (Grammar -> MetaThunks s -> [Message] -> ST s (CheckResult s a)) | TcMany [x] (Grammar -> MetaThunks s -> [Message] -> ST s [(a,MetaThunks s,[Message])]) mkTcA :: Err [a] -> TcA s a a -mkTcA f = case f of +mkTcA f = undefined {- case f of Bad msg -> TcSingle (\gr ms msgs -> return (TcFail (pp msg : msgs))) Ok [x] -> TcSingle (\gr ms msgs -> return (TcOk x ms msgs)) Ok xs -> TcMany xs (\gr ms msgs -> return [(x,ms,msgs) | x <- xs]) +-} +singleTcA :: EvalM s a -> TcA s x a +singleTcA = undefined {- TcSingle . unTcM -} -singleTcA :: TcM s a -> TcA s x a -singleTcA = TcSingle . unTcM - -bindTcA :: TcA s x a -> (a -> TcM s b) -> TcA s x b -bindTcA f g = case f of - TcSingle f -> TcSingle (unTcM (TcM f >>= g)) +bindTcA :: TcA s x a -> (a -> EvalM s b) -> TcA s x b +bindTcA f g = undefined {- case f of + TcSingle f -> TcSingle (unTcM (EvalM f >>= g)) TcMany xs f -> TcMany xs (\gr ms msgs -> f gr ms msgs >>= foldM (add gr) []) where add gr rs (y,ms,msgs) = do res <- unTcM (g y) gr ms msgs case res of - TcFail _ -> return rs - TcOk y ms msgs -> return ((y,ms,msgs):rs) - -runTcA :: ([x] -> TcM s a) -> (SourceGrammar -> TcA s x a) -> TcM s a -runTcA g f = TcM (\gr ms msgs -> case f gr of - TcMany xs f -> do rs <- f gr ms msgs - case rs of - [(x,ms,msgs)] -> return (TcOk x ms msgs) - rs -> unTcM (g xs) gr ms msgs - TcSingle f -> f gr ms msgs) - + Fail _ _ -> return rs + Success y msgs -> return ((y,ms,msgs):rs) +-} +runTcA :: ([x] -> EvalM s a) -> (SourceGrammar -> TcA s x a) -> EvalM s a +runTcA g f = undefined {- EvalM (\gr ms msgs -> case f gr of + TcMany xs f -> do rs <- f gr ms msgs + case rs of + [(x,ms,msgs)] -> return (Success x msgs) + rs -> unTcM (g xs) gr ms msgs + TcSingle f -> f gr ms msgs) +-} diff --git a/src/compiler/GF/Infra/CheckM.hs b/src/compiler/GF/Infra/CheckM.hs index 96d298f750..5a0ac0fcc2 100644 --- a/src/compiler/GF/Infra/CheckM.hs +++ b/src/compiler/GF/Infra/CheckM.hs @@ -37,22 +37,19 @@ import qualified Control.Monad.Fail as Fail type Message = Doc type Error = Message type Warning = Message ---data Severity = Warning | Error ---type NonFatal = ([Severity,Message]) -- preserves order type NonFatal = ([Error],[Warning]) -type Accumulate acc ans = acc -> (acc,ans) -data CheckResult a = Fail Error | Success a +data CheckResult a b = Fail Error b | Success a b newtype Check a - = Check {unCheck :: {-Context ->-} Accumulate NonFatal (CheckResult a)} + = Check {unCheck :: NonFatal -> CheckResult a NonFatal} instance Functor Check where fmap = liftM instance Monad Check where - return x = Check $ \{-ctxt-} ws -> (ws,Success x) - f >>= g = Check $ \{-ctxt-} ws -> - case unCheck f {-ctxt-} ws of - (ws,Success x) -> unCheck (g x) {-ctxt-} ws - (ws,Fail msg) -> (ws,Fail msg) + return x = Check $ \msgs -> Success x msgs + f >>= g = Check $ \ws -> + case unCheck f ws of + Success x msgs -> unCheck (g x) msgs + Fail msg msgs -> Fail msg msgs instance Fail.MonadFail Check where fail = raise @@ -65,26 +62,26 @@ instance ErrorMonad Check where raise s = checkError (pp s) handle f h = handle' f (h . render) -handle' f h = Check (\{-ctxt-} msgs -> case unCheck f {-ctxt-} msgs of - (ws,Success x) -> (ws,Success x) - (ws,Fail msg) -> unCheck (h msg) {-ctxt-} ws) +handle' f h = Check (\msgs -> case unCheck f {-ctxt-} msgs of + Success x msgs -> Success x msgs + Fail msg msgs -> unCheck (h msg) msgs) -- | Report a fatal error checkError :: Message -> Check a -checkError msg = Check (\{-ctxt-} ws -> (ws,Fail msg)) +checkError msg = Check (\msgs -> Fail msg msgs) checkCond :: Message -> Bool -> Check () checkCond s b = if b then return () else checkError s -- | warnings should be reversed in the end checkWarn :: Message -> Check () -checkWarn msg = Check $ \{-ctxt-} (es,ws) -> ((es,("Warning:" <+> msg) : ws),Success ()) +checkWarn msg = Check $ \(es,ws) -> Success () (es,("Warning:" <+> msg) : ws) checkWarnings ms = mapM_ checkWarn ms -- | Report a nonfatal (accumulated) error checkAccumError :: Message -> Check () -checkAccumError msg = Check $ \{-ctxt-} (es,ws) -> ((msg:es,ws),Success ()) +checkAccumError msg = Check $ \(es,ws) -> Success () (msg:es,ws) -- | Turn a fatal error into a nonfatal (accumulated) error accumulateError :: (a -> Check a) -> a -> Check a @@ -94,13 +91,13 @@ accumulateError chk a = -- | Turn accumulated errors into a fatal error commitCheck :: Check a -> Check a commitCheck c = - Check $ \ {-ctxt-} msgs0@(es0,ws0) -> - case unCheck c {-ctxt-} ([],[]) of - (([],ws),Success v) -> ((es0,ws++ws0),Success v) - (msgs ,Success _) -> bad msgs0 msgs - ((es,ws),Fail e) -> bad msgs0 ((e:es),ws) + Check $ \msgs0@(es0,ws0) -> + case unCheck c ([],[]) of + (Success v ([],ws)) -> Success v (es0,ws++ws0) + (Success _ msgs) -> bad msgs0 msgs + (Fail e (es,ws)) -> bad msgs0 ((e:es),ws) where - bad (es0,ws0) (es,ws) = ((es0,ws++ws0),Fail (list es)) + bad (es0,ws0) (es,ws) = (Fail (list es) (es0,ws++ws0)) list = vcat . reverse -- | Run an error check, report errors and warnings @@ -109,10 +106,10 @@ runCheck c = runCheck' noOptions c -- | Run an error check, report errors and (optionally) warnings runCheck' :: ErrorMonad m => Options -> Check a -> m (a,String) runCheck' opts c = - case unCheck c {-[]-} ([],[]) of - (([],ws),Success v) -> return (v,render (wlist ws)) - (msgs ,Success v) -> bad msgs - ((es,ws),Fail e) -> bad ((e:es),ws) + case unCheck c ([],[]) of + Success v ([],ws) -> return (v,render (wlist ws)) + Success v msgs -> bad msgs + Fail e (es,ws) -> bad ((e:es),ws) where bad (es,ws) = raise (render $ wlist ws $$ list es) list = vcat . reverse @@ -128,12 +125,13 @@ checkMapRecover f = fmap Map.fromList . mapM f' . Map.toList where f' (k,v) = fmap ((,)k) (f k v) checkIn :: Doc -> Check a -> Check a -checkIn msg c = Check $ \{-ctxt-} msgs0 -> - case unCheck c {-ctxt-} ([],[]) of - (msgs,Fail msg) -> (augment msgs0 msgs,Fail (augment1 msg)) - (msgs,Success v) -> (augment msgs0 msgs,Success v) +checkIn msg c = Check $ \msgs0 -> + case unCheck c ([],[]) of + Fail msg msgs -> Fail (augment1 msg) (augment msgs0 msgs) + Success v msgs -> Success v (augment msgs0 msgs) where augment (es0,ws0) (es,ws) = (augment' es0 es,augment' ws0 ws) + augment' msgs0 [] = msgs0 augment' msgs0 msgs' = (msg $$ nest 3 (vcat (reverse msgs'))):msgs0 From 65002fb58629015e8227d383da9728f9bba206ec Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Fri, 24 Nov 2023 09:41:23 +0100 Subject: [PATCH 06/15] allow Exp instead of Exp1 for the source commands --- src/compiler/GF/Grammar/Parser.y | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/compiler/GF/Grammar/Parser.y b/src/compiler/GF/Grammar/Parser.y index c632d8f220..c55e03e66f 100644 --- a/src/compiler/GF/Grammar/Parser.y +++ b/src/compiler/GF/Grammar/Parser.y @@ -31,7 +31,7 @@ import qualified Data.Map as Map %name pModDef ModDef %name pTopDef TopDef %partial pModHeader ModHeader -%partial pTerm Exp1 +%partial pTerm Exp %name pExp Exp %name pBNFCRules ListCFRule %name pEBNFRules ListEBNFRule From eb7155762773a15458b5a03d048b730298f23966 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Mon, 27 Nov 2023 13:46:21 +0100 Subject: [PATCH 07/15] ensure that metavariable IDs are always in sync --- src/compiler/GF/Compile/GeneratePMCFG.hs | 52 +++++++++++++----------- 1 file changed, 29 insertions(+), 23 deletions(-) diff --git a/src/compiler/GF/Compile/GeneratePMCFG.hs b/src/compiler/GF/Compile/GeneratePMCFG.hs index 0c1fafce71..8995972e22 100644 --- a/src/compiler/GF/Compile/GeneratePMCFG.hs +++ b/src/compiler/GF/Compile/GeneratePMCFG.hs @@ -24,10 +24,12 @@ import GF.Data.Operations(Err(..)) import PGF2.Transactions import Control.Monad import Control.Monad.State +import Control.Monad.ST import qualified Data.Map.Strict as Map import qualified Data.Sequence as Seq import Data.List(mapAccumL,sortOn,sortBy) import Data.Maybe(fromMaybe,isNothing) +import Data.STRef generatePMCFG :: Options -> FilePath -> SourceGrammar -> SourceModule -> Check SourceModule generatePMCFG opts cwd gr cmo@(cm,cmi) @@ -77,12 +79,12 @@ addPMCFG opts cwd gr cmi id info seqs = return (info,seqs) pmcfgForm :: Grammar -> Term -> Context -> Type -> SequenceSet -> Check ([Production],SequenceSet) pmcfgForm gr t ctxt ty seqs = do res <- runEvalM gr $ do - ((_,ms),args) <- mapAccumM (\(d,ms) (_,_,ty) -> do - let (ms',_,t) = type2metaTerm gr d ms 0 [] ty + (_,args) <- mapAccumM (\arg_no (_,_,ty) -> do + t <- EvalM (\gr k mt d r msgs -> do (mt,_,t) <- type2metaTerm gr arg_no mt 0 [] ty + k t mt d r msgs) tnk <- newThunk [] t - return ((d+1,ms'),tnk)) - (0,Map.empty) ctxt - sequence_ [newNarrowing i ty | (i,ty) <- Map.toList ms] + return (arg_no+1,tnk)) + 0 ctxt v <- eval [] t args (lins,params) <- flatten v ty ([],[]) lins <- fmap reverse $ mapM str2lin lins @@ -116,34 +118,38 @@ pmcfgForm gr t ctxt ty seqs = do Nothing -> let seqid = Map.size m in (seqid,Map.insert lin seqid m) -type2metaTerm :: SourceGrammar -> Int -> Map.Map MetaId Type -> LIndex -> [(LIndex,(Ident,Type))] -> Type -> (Map.Map MetaId Type,Int,Term) +type2metaTerm :: SourceGrammar -> Int -> MetaThunks s -> LIndex -> [(LIndex,(Ident,Type))] -> Type -> ST s (MetaThunks s,Int,Term) type2metaTerm gr d ms r rs (Sort s) | s == cStr = - (ms,r+1,TSymCat d r rs) -type2metaTerm gr d ms r rs (RecType lbls) = - let ((ms',r'),ass) = mapAccumL (\(ms,r) (lbl,ty) -> case lbl of - LVar j -> ((ms,r),(lbl,(Just ty,TSymVar d j))) - lbl -> let (ms',r',t) = type2metaTerm gr d ms r rs ty - in ((ms',r'),(lbl,(Just ty,t)))) + return (ms,r+1,TSymCat d r rs) +type2metaTerm gr d ms r rs (RecType lbls) = do + ((ms',r'),ass) <- mapAccumM (\(ms,r) (lbl,ty) -> case lbl of + LVar j -> return ((ms,r),(lbl,(Just ty,TSymVar d j))) + lbl -> do (ms',r',t) <- type2metaTerm gr d ms r rs ty + return ((ms',r'),(lbl,(Just ty,t)))) (ms,r) lbls - in (ms',r',R ass) + return (ms',r',R ass) type2metaTerm gr d ms r rs (Table p q) - | count == 1 = let (ms',r',t) = type2metaTerm gr d ms r rs q - in (ms',r+(r'-r),T (TTyped p) [(PW,t)]) - | otherwise = let pv = varX (length rs+1) - delta = r'-r - (ms',r',t) = type2metaTerm gr d ms r ((delta,(pv,p)):rs) q - in (ms',r+delta*count,T (TTyped p) [(PV pv,t)]) + | count == 1 = do (ms',r',t) <- type2metaTerm gr d ms r rs q + return (ms',r+(r'-r),T (TTyped p) [(PW,t)]) + | otherwise = do let pv = varX (length rs+1) + (ms',delta,t) <- + fixST $ \(~(_,delta,_)) -> + do (ms',r',t) <- type2metaTerm gr d ms r ((delta,(pv,p)):rs) q + return (ms',r'-r,t) + return (ms',r+delta*count,T (TTyped p) [(PV pv,t)]) where count = case allParamValues gr p of Ok ts -> length ts Bad msg -> error msg -type2metaTerm gr d ms r rs ty@(QC q) = +type2metaTerm gr d ms r rs ty@(QC q) = do let i = Map.size ms + 1 - in (Map.insert i ty ms,r,Meta i) + tnk <- newSTRef (Narrowing i ty) + return (Map.insert i tnk ms,r,Meta i) type2metaTerm gr d ms r rs ty - | Just n <- isTypeInts ty = + | Just n <- isTypeInts ty = do let i = Map.size ms + 1 - in (Map.insert i ty ms,r,Meta i) + tnk <- newSTRef (Narrowing i ty) + return (Map.insert i tnk ms,r,Meta i) flatten (VR as) (RecType lbls) st = do foldM collect st lbls From 6b9bda33280d3c600d3a478b4c29899d0042e44a Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Tue, 28 Nov 2023 07:39:54 +0100 Subject: [PATCH 08/15] fully restore the parser --- src/compiler/GF/Compile/Compute/Concrete.hs | 77 ++- .../GF/Compile/TypeCheck/ConcreteNew.hs | 446 +++++++++--------- 2 files changed, 272 insertions(+), 251 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index d0e89863e1..3a25df75ff 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -11,7 +11,8 @@ module GF.Compile.Compute.Concrete , newThunk, newEvaluatedThunk , newResiduation, newNarrowing, getVariables , getRef, setRef - , getResDef, getInfo, getResType, getAllParamValues + , getResDef, getInfo, getResType, getOverload + , getAllParamValues ) where import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint @@ -53,8 +54,9 @@ data ThunkState s = Unevaluated (Env s) Term | Evaluated {-# UNPACK #-} !Int (Value s) | Hole {-# UNPACK #-} !MetaId - | Residuation {-# UNPACK #-} !MetaId (Scope s) (Value s) | Narrowing {-# UNPACK #-} !MetaId Type + | Residuation {-# UNPACK #-} !MetaId (Scope s) (Sigma s) + | Bound Term type Thunk s = STRef s (ThunkState s) type Env s = [(Ident,Thunk s)] @@ -97,12 +99,12 @@ showValue (VMeta _ _ _) = "VMeta" showValue (VSusp _ _ _ _) = "VSusp" showValue (VGen _ _) = "VGen" showValue (VClosure _ _) = "VClosure" -showValue (VProd _ _ _ _) = "VProd" +showValue (VProd _ x v1 v2) = "VProd ("++show x++") ("++showValue v1++") ("++showValue v2++")" showValue (VRecType _) = "VRecType" showValue (VR lbls) = "(VR {"++unwords (map (\(lbl,_) -> show lbl) lbls)++"})" showValue (VP v l _) = "(VP "++showValue v++" "++show l++")" showValue (VExtR _ _) = "VExtR" -showValue (VTable _ _) = "VTable" +showValue (VTable v1 v2) = "VTable ("++showValue v1++") ("++showValue v2++")" showValue (VT _ _ cs) = "(VT "++show cs++")" showValue (VV _ _) = "VV" showValue (VS v _ _) = "(VS "++showValue v++")" @@ -128,7 +130,9 @@ eval env (Vr x) vs = do (tnk,depth) <- lookup x env lookup x ((y,tnk):env) | x == y = return (tnk,length env) | otherwise = lookup x env -eval env (Sort s) [] = return (VSort s) +eval env (Sort s) [] + | s == cTok = return (VSort cStr) + | otherwise = return (VSort s) eval env (EInt n) [] = return (VInt n) eval env (EFloat d) [] = return (VFlt d) eval env (K t) [] = return (VStr t) @@ -500,7 +504,7 @@ susp i env ki = EvalM $ \gr k mt d r msgs -> do value2term xs (VApp q tnks) = foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (if fst q == cPredef then Q q else QC q) tnks value2term xs (VMeta m env tnks) = do - res <- zonk m tnks + res <- zonk xs m tnks case res of Right i -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) tnks Left v -> value2term xs v @@ -515,14 +519,18 @@ value2term xs (VClosure env (Abs b x t)) = do let x' = mkFreshVar xs x t <- value2term (x':xs) v return (Abs b x' t) -value2term xs (VProd b x v1 (VClosure env t2)) +value2term xs (VProd b x v1 v2) | x == identW = do t1 <- value2term xs v1 - v2 <- eval env t2 [] + v2 <- case v2 of + VClosure env t2 -> eval env t2 [] + v2 -> return v2 t2 <- value2term xs v2 return (Prod b x t1 t2) | otherwise = do t1 <- value2term xs v1 tnk <- newEvaluatedThunk (VGen (length xs) []) - v2 <- eval ((x,tnk):env) t2 [] + v2 <- case v2 of + VClosure env t2 -> eval ((x,tnk):env) t2 [] + v2 -> return v2 t2 <- value2term (x:xs) v2 return (Prod b (mkFreshVar xs x) t1 t2) value2term xs (VRecType lbls) = do @@ -582,6 +590,7 @@ value2term xs (VAlts vd vas) = do value2term xs (VStrs vs) = do ts <- mapM (value2term xs) vs return (Strs ts) +value2term xs v = error (showValue v) pattVars st (PP _ ps) = foldM pattVars st ps pattVars st (PV x) = case st of @@ -756,6 +765,22 @@ getResType q = EvalM $ \gr k mt d r msgs -> do Ok t -> k t mt d r msgs Bad msg -> return (Fail (pp msg) msgs) +getOverload :: Term -> QIdent -> EvalM s (Term,Type) +getOverload t q = EvalM $ \gr k mt d r msgs -> do + case lookupOverloadTypes gr q of + Ok ttys -> let err = "Overload resolution failed" $$ + "of term " <+> pp t $$ + "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys] + + go [] = return (Fail err msgs) + go (tty:ttys) = do res <- k tty mt d r msgs + case res of + Fail _ _ -> return res -- go ttys + Success r msgs -> return (Success r msgs) + + in go ttys + Bad msg -> return (Fail (pp msg) msgs) + getAllParamValues :: Type -> EvalM s [Term] getAllParamValues ty = EvalM $ \gr k mt d r msgs -> case allParamValues gr ty of @@ -780,17 +805,14 @@ newHole i = EvalM $ \gr k mt d r msgs -> k tnk (Map.insert i tnk mt) d r msgs newResiduation scope ty = EvalM $ \gr k mt d r msgs -> do - tnk <- newSTRef (Residuation 0 scope ty) - k tnk mt d r msgs + let i = Map.size mt + 1 + tnk <- newSTRef (Residuation i scope ty) + k (i,tnk) (Map.insert i tnk mt) d r msgs -newNarrowing i ty = EvalM $ \gr k mt d r msgs -> - if i == 0 - then do tnk <- newSTRef (Narrowing i ty) - k tnk mt d r msgs - else case Map.lookup i mt of - Just tnk -> k tnk mt d r msgs - Nothing -> do tnk <- newSTRef (Narrowing i ty) - k tnk (Map.insert i tnk mt) d r msgs +newNarrowing ty = EvalM $ \gr k mt d r msgs -> do + let i = Map.size mt + 1 + tnk <- newSTRef (Narrowing i ty) + k (i,tnk) (Map.insert i tnk mt) d r msgs withVar d0 (EvalM f) = EvalM $ \gr k mt d1 r msgs -> let !d = min d0 d1 @@ -814,8 +836,13 @@ getVariables = EvalM $ \gr k mt d ws r -> do else return params _ -> metas2params gr tnks -getRef tnk = EvalM $ \gr k mt d ws r -> readSTRef tnk >>= \st -> k st mt d ws r -setRef tnk st = EvalM $ \gr k mt d ws r -> writeSTRef tnk st >>= \st -> k () mt d ws r +getRef tnk = EvalM $ \gr k mt d r msgs -> readSTRef tnk >>= \st -> k st mt d r msgs +setRef tnk st = EvalM $ \gr k mt d r msgs -> do + old <- readSTRef tnk + writeSTRef tnk st + res <- k () mt d r msgs + writeSTRef tnk old + return res force tnk = EvalM $ \gr k mt d r msgs -> do s <- readSTRef tnk @@ -868,11 +895,17 @@ tnk2term xs tnk = EvalM $ \gr k mt d r msgs -> Residuation i _ _ -> k (Meta i) mt d r msgs Narrowing i _ -> k (Meta i) mt d r msgs -zonk tnk vs = EvalM $ \gr k mt d r msgs -> do +scopeEnv scope = zipWithM (\x i -> newEvaluatedThunk (VGen i []) >>= \tnk -> return (x,tnk)) (reverse scope) [0..] + +zonk scope tnk vs = EvalM $ \gr k mt d r msgs -> do s <- readSTRef tnk case s of Evaluated _ v -> case apply v vs of EvalM f -> f gr (k . Left) mt d r msgs + Unevaluated env t -> case eval env t vs of + EvalM f -> f gr (k . Left) mt d r msgs + Bound t -> case scopeEnv scope >>= \env -> eval env t vs of + EvalM f -> f gr (k . Left) mt d r msgs Hole i -> k (Right i) mt d r msgs Residuation i _ _ -> k (Right i) mt d r msgs Narrowing i _ -> k (Right i) mt d r msgs diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index 7a1b3e594f..d7a22cddd2 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -17,6 +17,7 @@ import Control.Applicative(Applicative(..)) import Control.Monad(ap,liftM,mplus,foldM,zipWithM) import Control.Monad.ST import GF.Text.Pretty +import Data.STRef import Data.List (nub, (\\), tails) import qualified Data.Map as Map import Data.Maybe(fromMaybe,isNothing) @@ -61,26 +62,23 @@ tcRho scope t@(Vr v) mb_ty = do -- VAR case lookup v scope of Just v_sigma -> instSigma scope t v_sigma mb_ty Nothing -> evalError ("Unknown variable" <+> v) -tcRho scope t@(Q id) mb_ty = - runTcA (tcOverloadFailed t) $ \gr -> - tcApp gr scope t `bindTcA` \(t,ty) -> - instSigma scope t ty mb_ty -tcRho scope t@(QC id) mb_ty = - runTcA (tcOverloadFailed t) $ \gr -> - tcApp gr scope t `bindTcA` \(t,ty) -> - instSigma scope t ty mb_ty +tcRho scope t@(Q id) mb_ty = do + (t,ty) <- tcApp scope t t + instSigma scope t ty mb_ty +tcRho scope t@(QC id) mb_ty = do + (t,ty) <- tcApp scope t t + instSigma scope t ty mb_ty tcRho scope t@(App fun arg) mb_ty = do - runTcA (tcOverloadFailed t) $ \gr -> - tcApp gr scope t `bindTcA` \(t,ty) -> - instSigma scope t ty mb_ty + (t,ty) <- tcApp scope t t + instSigma scope t ty mb_ty tcRho scope (Abs bt var body) Nothing = do -- ABS1 - tnk <- newResiduation scope vtypeType + (_,tnk) <- newResiduation scope vtypeType env <- scopeEnv scope let arg_ty = VMeta tnk env [] (body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing return (Abs bt var body, (VProd bt identW arg_ty body_ty)) tcRho scope t@(Abs Implicit var body) (Just ty) = do -- ABS2 - (bt, var_ty, body_ty) <- unifyFun scope ty + (bt, _, var_ty, body_ty) <- unifyFun scope ty if bt == Implicit then return () else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") @@ -88,9 +86,18 @@ tcRho scope t@(Abs Implicit var body) (Just ty) = do -- ABS2 return (Abs Implicit var body,ty) tcRho scope (Abs Explicit var body) (Just ty) = do -- ABS3 (scope,f,ty') <- skolemise scope ty - (_,var_ty,body_ty) <- unifyFun scope ty' + (_,_,var_ty,body_ty) <- unifyFun scope ty' (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (f (Abs Explicit var body),ty) +tcRho scope (Meta i) (Just ty) = do + (i,_) <- newResiduation scope ty + return (Meta i, ty) +tcRho scope (Meta _) Nothing = do + (_,tnk) <- newResiduation scope vtypeType + env <- scopeEnv scope + let vty = VMeta tnk env [] + (i,_) <- newResiduation scope vty + return (Meta i, vty) tcRho scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET (rhs,var_ty) <- case mb_ann_ty of Nothing -> inferSigma scope rhs @@ -110,9 +117,9 @@ tcRho scope (Typed body ann_ty) mb_ty = do -- ANNOT instSigma scope (Typed body ann_ty) v_ann_ty mb_ty tcRho scope (FV ts) mb_ty = do case ts of - [] -> do i <- newResiduation scope vtypeType + [] -> do (i,tnk) <- newResiduation scope vtypeType env <- scopeEnv scope - instSigma scope (FV []) (VMeta i env []) mb_ty + instSigma scope (FV []) (VMeta tnk env []) mb_ty (t:ts) -> do (t,ty) <- tcRho scope t mb_ty let go [] ty = return ([],ty) @@ -153,9 +160,10 @@ tcRho scope (Prod bt x ty1 ty2) mb_ty = do instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty tcRho scope (S t p) mb_ty = do env <- scopeEnv scope - p_ty <- fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypePType + let mk_val (_,tnk) = VMeta tnk env [] + p_ty <- fmap mk_val $ newResiduation scope vtypePType res_ty <- case mb_ty of - Nothing -> fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypeType + Nothing -> fmap mk_val $ newResiduation scope vtypeType Just ty -> return ty let t_ty = VTable p_ty res_ty (t,t_ty) <- tcRho scope t (Just t_ty) @@ -163,14 +171,15 @@ tcRho scope (S t p) mb_ty = do return (S t p, res_ty) tcRho scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables env <- scopeEnv scope + let mk_val (_,tnk) = VMeta tnk env [] p_ty <- case tt of - TRaw -> fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypePType + TRaw -> fmap mk_val $ newResiduation scope vtypePType TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) eval env ty [] (ps,mb_res_ty) <- tcCases scope ps p_ty Nothing res_ty <- case mb_res_ty of Just res_ty -> return res_ty - Nothing -> fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypeType + Nothing -> fmap mk_val $ newResiduation scope vtypeType p_ty_t <- value2term [] p_ty return (T (TTyped p_ty_t) ps, VTable p_ty res_ty) tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables @@ -206,8 +215,8 @@ tcRho scope (P t l) mb_ty = do l_ty <- case mb_ty of Just ty -> return ty Nothing -> do env <- scopeEnv scope - i <- newEvaluatedThunk vtypeType - return (VMeta i env []) + (i,tnk) <- newResiduation scope vtypeType + return (VMeta tnk env []) (t,t_ty) <- tcRho scope t (Just (VRecType [(l,l_ty)])) return (P t l,l_ty) tcRho scope (C t1 t2) mb_ty = do @@ -251,8 +260,8 @@ tcRho scope (EPattType ty) mb_ty = do tcRho scope t@(EPatt min max p) mb_ty = do (scope,f,ty) <- case mb_ty of Nothing -> do env <- scopeEnv scope - i <- newEvaluatedThunk vtypeType - return (scope,id,VMeta i env []) + (i,tnk) <- newResiduation scope vtypeType + return (scope,id,VMeta tnk env []) Just ty -> do (scope,f,ty) <- skolemise scope ty case ty of VPattType ty -> return (scope,f,ty) @@ -268,35 +277,36 @@ tcCases scope ((p,t):cs) p_ty mb_res_ty = do (cs,mb_res_ty) <- tcCases scope cs p_ty (Just res_ty) return ((p,t):cs,mb_res_ty) -tcApp gr scope t@(App fun (ImplArg arg)) = do -- APP1 - tcApp gr scope fun `bindTcA` \(fun,fun_ty) -> - do (bt, arg_ty, res_ty) <- unifyFun scope fun_ty - if (bt == Implicit) - then return () - else evalError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected") - (arg,_) <- tcRho scope arg (Just arg_ty) - env <- scopeEnv scope - varg <- eval env arg [] - return (App fun (ImplArg arg), res_ty) -tcApp gr scope (App fun arg) = -- APP2 - tcApp gr scope fun `bindTcA` \(fun,fun_ty) -> - do (fun,fun_ty) <- instantiate scope fun fun_ty - (_, arg_ty, res_ty) <- unifyFun scope fun_ty - (arg,_) <- tcRho scope arg (Just arg_ty) - env <- scopeEnv scope - varg <- eval env arg [] - return (App fun arg, res_ty) -tcApp gr scope (Q id) = do -- VAR (global) - mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) -> - do ty <- eval [] ty [] - return (t,ty) -tcApp gr scope (QC id) = -- VAR (global) - mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) -> - do ty <- eval [] ty [] - return (t,ty) -tcApp gr scope t = - singleTcA (tcRho scope t Nothing) - +tcApp scope t0 t@(App fun (ImplArg arg)) = do -- APP1 + (fun,fun_ty) <- tcApp scope t0 fun + (bt, _, arg_ty, res_ty) <- unifyFun scope fun_ty + if (bt == Implicit) + then return () + else evalError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected") + (arg,_) <- tcRho scope arg (Just arg_ty) + env <- scopeEnv scope + varg <- eval env arg [] + return (App fun (ImplArg arg), res_ty) +tcApp scope t0 (App fun arg) = do -- APP2 + (fun,fun_ty) <- tcApp scope t0 fun + (fun,fun_ty) <- instantiate scope fun fun_ty + (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty + (arg,_) <- tcRho scope arg (Just arg_ty) + res_ty <- case res_ty of + VClosure res_env res_ty -> do env <- scopeEnv scope + tnk <- newThunk env arg + eval ((x,tnk):res_env) res_ty [] + res_ty -> return res_ty + return (App fun arg, res_ty) +tcApp scope t0 (Q id) = do -- VAR (global) + (t,ty) <- getOverload t0 id + vty <- eval [] ty [] + return (t,vty) +tcApp scope t0 (QC id) = do -- VAR (global) + (t,ty) <- getOverload t0 id + vty <- eval [] ty [] + return (t,vty) +tcApp scope t0 t = tcRho scope t Nothing tcOverloadFailed t ttys = evalError ("Overload resolution failed" $$ @@ -311,7 +321,7 @@ tcPatt scope (PV x) ty0 = tcPatt scope (PP c ps) ty0 = do ty <- getResType c let go scope ty [] = return (scope,ty) - go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun scope ty + go scope ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty scope <- tcPatt scope p arg_ty go scope res_ty ps vty <- eval [] ty [] @@ -337,10 +347,10 @@ tcPatt scope (PAs x p) ty0 = do tcPatt ((x,ty0):scope) p ty0 tcPatt scope (PR rs) ty0 = do let mk_ltys [] = return [] - mk_ltys ((l,p):rs) = do i <- newEvaluatedThunk vtypePType + mk_ltys ((l,p):rs) = do (_,tnk) <- newResiduation scope vtypePType ltys <- mk_ltys rs env <- scopeEnv scope - return ((l,p,VMeta i env []) : ltys) + return ((l,p,VMeta tnk env []) : ltys) go scope [] = return scope go scope ((l,p,ty):rs) = do scope <- tcPatt scope p ty go scope rs @@ -422,44 +432,53 @@ subsCheckRho scope t ty1@(VMeta i env vs) ty2 = do case mv of Residuation _ _ _ -> do unify scope ty1 ty2 return t - Evaluated _ vty1 -> do vty1 <- apply vty1 vs + Bound ty1 -> do vty1 <- eval env ty1 vs subsCheckRho scope t vty1 ty2 subsCheckRho scope t ty1 ty2@(VMeta i env vs) = do mv <- getRef i case mv of Residuation _ _ _ -> do unify scope ty1 ty2 return t - Evaluated _ vty2 -> do vty2 <- apply vty2 vs + Bound ty2 -> do vty2 <- eval env ty2 vs subsCheckRho scope t ty1 vty2 -{-subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC - i <- newMeta scope ty1 - subsCheckRho ge scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) rho2 -subsCheckRho ge scope t rho1 (VProd Implicit ty1 x (Bind ty2)) = do -- Rule SKOL +subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do -- Rule SPEC + (i,tnk) <- newResiduation scope ty1 + ty2 <- case ty2 of + VClosure env ty2 -> eval ((x,tnk):env) ty2 [] + ty2 -> return ty2 + subsCheckRho scope (App t (ImplArg (Meta i))) ty2 rho2 +subsCheckRho scope t rho1 (VProd Implicit x ty1 ty2) = do -- Rule SKOL let v = newVar scope - t <- subsCheckRho ge ((v,ty1):scope) t rho1 (ty2 (VGen (length scope) [])) + ty2 <- case ty2 of + VClosure env ty2 -> do tnk <- newEvaluatedThunk (VGen (length scope) []) + eval ((x,tnk):env) ty2 [] + ty2 -> return ty2 + t <- subsCheckRho ((v,ty1):scope) t rho1 ty2 return (Abs Implicit v t) -subsCheckRho ge scope t rho1 (VProd Explicit a2 _ (Bind r2)) = do -- Rule FUN - (_,a1,r1) <- unifyFun ge scope rho1 - subsCheckFun ge scope t a1 r1 a2 r2 -subsCheckRho ge scope t (VProd Explicit a1 _ (Bind r1)) rho2 = do -- Rule FUN - (bt,a2,r2) <- unifyFun ge scope rho2 - subsCheckFun ge scope t a1 r1 a2 r2 -subsCheckRho ge scope t rho1 (VTblType p2 r2) = do -- Rule TABLE - (p1,r1) <- unifyTbl ge scope rho1 - subsCheckTbl ge scope t p1 r1 p2 r2 -subsCheckRho ge scope t (VTblType p1 r1) rho2 = do -- Rule TABLE - (p2,r2) <- unifyTbl ge scope rho2 - subsCheckTbl ge scope t p1 r1 p2 r2 -subsCheckRho ge scope t (VSort s1) (VSort s2) -- Rule PTYPE +subsCheckRho scope t rho1 (VProd Explicit _ a2 r2) = do -- Rule FUN + (_,_,a1,r1) <- unifyFun scope rho1 + subsCheckFun scope t a1 r1 a2 r2 +subsCheckRho scope t (VProd Explicit _ a1 r1) rho2 = do -- Rule FUN + (_,_,a2,r2) <- unifyFun scope rho2 + subsCheckFun scope t a1 r1 a2 r2 +subsCheckRho scope t rho1 (VTable p2 r2) = do -- Rule TABLE + (p1,r1) <- unifyTbl scope rho1 + subsCheckTbl scope t p1 r1 p2 r2 +subsCheckRho scope t (VTable p1 r1) rho2 = do -- Rule TABLE + (p2,r2) <- unifyTbl scope rho2 + subsCheckTbl scope t p1 r1 p2 r2 +subsCheckRho scope t (VSort s1) (VSort s2) -- Rule PTYPE | s1 == cPType && s2 == cType = return t -subsCheckRho ge scope t (VApp p1 _) (VApp p2 _) -- Rule INT1 - | predefName p1 == cInts && predefName p2 == cInt = return t -subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j]) -- Rule INT2 - | predefName p1 == cInts && predefName p2 == cInts = +subsCheckRho scope t (VApp p1 _) (VApp p2 _) -- Rule INT1 + | p1 == (cPredef,cInts) && p2 == (cPredef,cInt) = return t +subsCheckRho scope t (VApp p1 [tnk1]) (VApp p2 [tnk2]) -- Rule INT2 + | p1 == (cPredef,cInts) && p2 == (cPredef,cInts) = do + VInt i <- force tnk1 + VInt j <- force tnk2 if i <= j then return t else evalError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j) -subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC +subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC let mkAccess scope t = case t of ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1 @@ -468,7 +487,7 @@ subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule ,\l -> mkProj2 l `mplus` mkProj1 l ,mkWrap1 . mkWrap2 ) - R rs -> do sequence_ [tcWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup l rs2)] + R rs -> do sequence_ [evalWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup l rs2)] return (scope ,\l -> lookup l rs ,id @@ -486,7 +505,7 @@ subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule ) mkField scope l (mb_ty,t) ty1 ty2 = do - t <- subsCheckRho ge scope t ty1 ty2 + t <- subsCheckRho scope t ty1 ty2 return (l, (mb_ty,t)) (scope,mkProj,mkWrap) <- mkAccess scope t @@ -498,94 +517,103 @@ subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule "there are no values for fields:" <+> hsep missing) rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]] return (mkWrap (R rs)) -subsCheckRho ge scope t tau1 tau2 = do -- Rule EQ - unify ge scope tau1 tau2 -- Revert to ordinary unification +subsCheckRho scope t tau1 tau2 = do -- Rule EQ + unify scope tau1 tau2 -- Revert to ordinary unification return t -subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> (Value -> Rho) -> Sigma -> (Value -> Rho) -> EvalM Term -subsCheckFun ge scope t a1 r1 a2 r2 = do +subsCheckFun :: Scope s -> Term -> Sigma s -> Value s -> Sigma s -> Value s -> EvalM s Term +subsCheckFun scope t a1 r1 a2 r2 = do let v = newVar scope - vt <- subsCheckRho ge ((v,a2):scope) (Vr v) a2 a1 - val1 <- liftErr (eval ge (scopeEnv ((v,vtypeType):scope)) vt) - val2 <- return (VGen (length scope) []) - t <- subsCheckRho ge ((v,vtypeType):scope) (App t vt) (r1 val1) (r2 val2) + vt <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1 + tnk <- newEvaluatedThunk (VGen (length scope) []) + r1 <- case r1 of + VClosure env r1 -> eval ((v,tnk):env) r1 [] + r1 -> return r1 + r2 <- case r2 of + VClosure env r2 -> eval ((v,tnk):env) r2 [] + r2 -> return r2 + t <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1 r2 return (Abs Explicit v t) -subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term -subsCheckTbl ge scope t p1 r1 p2 r2 = do +subsCheckTbl :: Scope s -> Term -> Sigma s -> Rho s -> Sigma s -> Rho s -> EvalM s Term +subsCheckTbl scope t p1 r1 p2 r2 = do let x = newVar scope - xt <- subsCheckRho ge scope (Vr x) p2 p1 - t <- subsCheckRho ge ((x,vtypePType):scope) (S t xt) r1 r2 ; - p2 <- tc_value2term (geLoc ge) (scopeVars scope) p2 + xt <- subsCheckRho scope (Vr x) p2 p1 + t <- subsCheckRho ((x,vtypePType):scope) (S t xt) r1 r2 + p2 <- value2term (scopeVars scope) p2 return (T (TTyped p2) [(PV x,t)]) --} + ----------------------------------------------------------------------- -- Unification ----------------------------------------------------------------------- -unifyFun :: Scope s -> Rho s -> EvalM s (BindType, Sigma s, Rho s) +unifyFun :: Scope s -> Rho s -> EvalM s (BindType, Ident, Sigma s, Rho s) unifyFun scope (VProd bt x arg res) = - return (bt,arg,res) + return (bt,x,arg,res) unifyFun scope tau = do - let mk_val ty = VMeta ty [] [] - arg <- fmap mk_val $ newEvaluatedThunk vtypeType - res <- fmap mk_val $ newEvaluatedThunk vtypeType + let mk_val (_,tnk) = VMeta tnk [] [] + arg <- fmap mk_val $ newResiduation scope vtypeType + res <- fmap mk_val $ newResiduation scope vtypeType let bt = Explicit unify scope tau (VProd bt identW arg res) - return (bt,arg,res) + return (bt,identW,arg,res) unifyTbl :: Scope s -> Rho s -> EvalM s (Sigma s, Rho s) unifyTbl scope (VTable arg res) = return (arg,res) unifyTbl scope tau = do env <- scopeEnv scope - let mk_val ty = VMeta ty env [] - arg <- fmap mk_val $ newEvaluatedThunk vtypePType - res <- fmap mk_val $ newEvaluatedThunk vtypeType + let mk_val (i,tnk) = VMeta tnk env [] + arg <- fmap mk_val $ newResiduation scope vtypePType + res <- fmap mk_val $ newResiduation scope vtypeType unify scope tau (VTable arg res) return (arg,res) unify scope (VApp f1 vs1) (VApp f2 vs2) - | f1 == f2 = undefined {- sequence_ (zipWith (unify ge scope) vs1 vs2) -unify ge scope (VCApp f1 vs1) (VCApp f2 vs2) - | f1 == f2 = sequence_ (zipWith (unify ge scope) vs1 vs2) -unify ge scope (VSort s1) (VSort s2) + | f1 == f2 = sequence_ (zipWith (unifyThunk scope) vs1 vs2) +unify scope (VSort s1) (VSort s2) | s1 == s2 = return () -unify ge scope (VGen i vs1) (VGen j vs2) - | i == j = sequence_ (zipWith (unify ge scope) vs1 vs2) -unify ge scope (VTblType p1 res1) (VTblType p2 res2) = do - unify ge scope p1 p2 - unify ge scope res1 res2 -unify ge scope (VMeta i env1 vs1) (VMeta j env2 vs2) - | i == j = sequence_ (zipWith (unify ge scope) vs1 vs2) - | otherwise = do mv <- getMeta j +unify scope (VGen i vs1) (VGen j vs2) + | i == j = sequence_ (zipWith (unifyThunk scope) vs1 vs2) +unify scope (VTable p1 res1) (VTable p2 res2) = do + unify scope p1 p2 + unify scope res1 res2 +unify scope (VMeta i env1 vs1) (VMeta j env2 vs2) + | i == j = sequence_ (zipWith (unifyThunk scope) vs1 vs2) + | otherwise = do mv <- getRef j case mv of - Bound t2 -> do v2 <- liftErr (eval ge env2 t2) - unify ge scope (VMeta i env1 vs1) (vapply (geLoc ge) v2 vs2) - Unbound _ _ -> setMeta i (Bound (Meta j)) -unify ge scope (VInt i) (VInt j) + Bound t2 -> do v2 <- eval env2 t2 vs2 + unify scope (VMeta i env1 vs1) v2 + Residuation j _ _ -> setRef i (Bound (Meta j)) +unify scope (VInt i) (VInt j) | i == j = return () -unify ge scope (VMeta i env vs) v = unifyVar ge scope i env vs v -unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v -unify ge scope v1 v2 = do - t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1 - t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2 +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 + t1 <- value2term (scopeVars scope) v1 + t2 <- value2term (scopeVars scope) v2 evalError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ ppTerm Unqualified 0 t2)) --} + +unifyThunk scope tnk1 tnk2 = do + res1 <- getRef tnk1 + res2 <- getRef tnk2 + case (res1,res2) of + (Evaluated _ v1,Evaluated _ v2) -> unify scope v1 v2 + -- | Invariant: tv1 is a flexible type variable unifyVar :: Scope s -> Thunk s -> Env s -> [Thunk s] -> Tau s -> EvalM s () unifyVar scope tnk env vs ty2 = do -- Check whether i is bound mv <- getRef tnk case mv of - Unevaluated _ ty1 -> do v <- eval env ty1 [] >>= \v -> apply v vs - unify scope v ty2 + Bound ty1 -> do v <- eval env ty1 vs + unify scope v ty2 Residuation i scope' _ -> do ty2' <- value2term (scopeVars scope') ty2 ms2 <- getMetaVars [(scope,ty2)] - if i `elem` ms2 + if tnk `elem` ms2 then evalError ("Occurs check for" <+> ppMeta i <+> "in:" $$ nest 2 (ppTerm Unqualified 0 ty2')) - else setRef tnk (Unevaluated env ty2') + else setRef tnk (Bound ty2') ----------------------------------------------------------------------- -- Instantiation and quantification @@ -593,43 +621,49 @@ unifyVar scope tnk env vs ty2 = do -- Check whether i is bound -- | Instantiate the topmost implicit arguments with metavariables instantiate :: Scope s -> Term -> Sigma s -> EvalM s (Term,Rho s) -instantiate scope t (VProd Implicit x ty1 ty2) = undefined {- do - i <- newMeta scope ty1 - instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) -} +instantiate scope t (VProd Implicit x ty1 ty2) = do + (i,tnk) <- newResiduation scope ty1 + ty2 <- case ty2 of + VClosure env ty2 -> eval ((x,tnk):env) ty2 [] + ty2 -> return ty2 + instantiate scope (App t (ImplArg (Meta i))) ty2 instantiate scope t ty = do return (t,ty) -- | Build fresh lambda abstractions for the topmost implicit arguments skolemise :: Scope s -> Sigma s -> EvalM s (Scope s, Term->Term, Rho s) -skolemise scope ty@(VMeta i env vs) = undefined {-do +skolemise scope ty@(VMeta i env vs) = do mv <- getRef i case mv of Residuation _ _ _ -> return (scope,id,ty) -- guarded constant? - Evaluated _ vty -> do vty <- apply vty vs - skolemise scope vty -skolemise scope (VProd Implicit ty1 x ty2) = do + Bound ty -> do ty <- eval env ty vs + skolemise scope ty +skolemise scope (VProd Implicit x ty1 ty2) = do let v = newVar scope - (scope,f,ty2) <- skolemise ((v,ty1):scope) (ty2 (VGen (length scope) [])) - return (scope,undefined {-Abs Implicit v . f-},ty2) + ty2 <- case ty2 of + VClosure env ty2 -> do tnk <- newEvaluatedThunk (VGen (length scope) []) + eval ((x,tnk) : env) ty2 [] + ty2 -> return ty2 + (scope,f,ty2) <- skolemise ((v,ty1):scope) ty2 + return (scope,Abs Implicit v . f,ty2) skolemise scope ty = do - return (scope,undefined,ty)-} + return (scope,id,ty) -- | Quantify over the specified type variables (all flexible) -quantify :: Scope s -> Term -> [MetaId] -> Rho s -> EvalM s (Term,Sigma s) -quantify scope t tvs ty0 = undefined {- do - ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0 +quantify :: Scope s -> Term -> [Thunk s] -> Rho s -> EvalM s (Term,Sigma s) +quantify scope t tvs ty = do let used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use new_bndrs = take (length tvs) (allBinders \\ used_bndrs) - mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way - ty <- zonkTerm ty -- of doing the substitution - vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs)) + env <- scopeEnv ([(v,vtypeType) | v <- new_bndrs]++scope) + mapM_ (bind env) (zip tvs new_bndrs) + let vty = foldr (\v -> VProd Implicit v vtypeType) ty new_bndrs return (foldr (Abs Implicit) t new_bndrs,vty) where - bind (i, name) = setMeta i (Bound (Vr name)) + bind env (tnk, name) = setRef tnk (Bound (Vr name)) + + bndrs (VProd _ x v1 v2) = [x] ++ bndrs v1 ++ bndrs v2 + bndrs _ = [] - bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2 - bndrs _ = [] --} allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,... allBinders = [ identS [x] | x <- ['a'..'z'] ] ++ [ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']] @@ -659,86 +693,40 @@ scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope) -- | This function takes account of zonking, and returns a set -- (no duplicates) of unbound meta-type variables -getMetaVars :: [(Scope s,Sigma s)] -> EvalM s [MetaId] -getMetaVars sc_tys = do - tys <- mapM (\(scope,ty) -> zonkTerm =<< value2term (scopeVars scope) ty) sc_tys - return (foldr go [] tys) +getMetaVars :: [(Scope s,Sigma s)] -> EvalM s [Thunk s] +getMetaVars sc_tys = foldM (\acc (scope,ty) -> go ty acc) [] sc_tys where - -- Get the MetaIds from a term; no duplicates in result - go (Vr tv) acc = acc - go (App x y) acc = go x (go y 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 (Table p t) acc = go p (go t acc) - go (RecType rs) acc = foldl (\acc (l,ty) -> go ty acc) acc rs - go t acc = unimplemented ("go "++show t) + follow acc tnk = force tnk >>= \v -> go v acc --- | This function takes account of zonking, and returns a set --- (no duplicates) of free type variables -getFreeVars :: [(Scope s,Sigma s)] -> EvalM s [Ident] -getFreeVars sc_tys = do - tys <- mapM (\(scope,ty) -> zonkTerm =<< value2term (scopeVars scope) ty) sc_tys - return (foldr (go []) [] tys) - where - go bound (Vr tv) acc - | tv `elem` bound = acc - | tv `elem` acc = acc - | otherwise = tv : acc - go bound (App x y) acc = go bound x (go bound y 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) - go bound (RecType rs) acc = foldl (\acc (l,ty) -> go bound ty acc) acc rs - go bound (Table p t) acc = go bound p (go bound t acc) + -- Get the MetaIds from a term; no duplicates in result + go (VSort s) acc = return acc + go (VInt _) acc = return acc + go (VRecType as) acc = foldM (\acc (lbl,v) -> go v acc) acc as + go (VClosure _ _) acc = return acc + go (VProd b x v1 v2) acc = go v2 acc >>= go v1 + go (VTable v1 v2) acc = go v2 acc >>= go v1 + go (VMeta m env args) acc + | m `elem` acc = return acc + | otherwise = do res <- getRef m + case res of + Bound _ -> return acc + _ -> foldM follow (m:acc) args + go (VApp f args) acc = foldM follow acc args + go v acc = unimplemented ("go "++showValue v) -- | Eliminate any substitutions in a term zonkTerm :: Term -> EvalM s Term -zonkTerm (Meta i) = undefined {- 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 (Meta i) = do + tnk <- EvalM $ \gr k mt d r msgs -> + case Map.lookup i mt of + Just v -> k v mt d r msgs + Nothing -> return (Fail (pp "Undefined meta variable") msgs) + st <- getRef tnk + case st of + Hole _ -> return (Meta i) + Residuation _ _ _ -> return (Meta i) + Narrowing _ _ -> return (Meta i) + Bound t -> do t <- zonkTerm t + setRef tnk (Bound t) -- "Short out" multiple hops + return t zonkTerm t = composOp zonkTerm t - --} - -data TcA s x a - = TcSingle (Grammar -> MetaThunks s -> [Message] -> ST s (CheckResult s a)) - | TcMany [x] (Grammar -> MetaThunks s -> [Message] -> ST s [(a,MetaThunks s,[Message])]) - -mkTcA :: Err [a] -> TcA s a a -mkTcA f = undefined {- case f of - Bad msg -> TcSingle (\gr ms msgs -> return (TcFail (pp msg : msgs))) - Ok [x] -> TcSingle (\gr ms msgs -> return (TcOk x ms msgs)) - Ok xs -> TcMany xs (\gr ms msgs -> return [(x,ms,msgs) | x <- xs]) --} -singleTcA :: EvalM s a -> TcA s x a -singleTcA = undefined {- TcSingle . unTcM -} - -bindTcA :: TcA s x a -> (a -> EvalM s b) -> TcA s x b -bindTcA f g = undefined {- case f of - TcSingle f -> TcSingle (unTcM (EvalM f >>= g)) - TcMany xs f -> TcMany xs (\gr ms msgs -> f gr ms msgs >>= foldM (add gr) []) - where - add gr rs (y,ms,msgs) = do - res <- unTcM (g y) gr ms msgs - case res of - Fail _ _ -> return rs - Success y msgs -> return ((y,ms,msgs):rs) --} -runTcA :: ([x] -> EvalM s a) -> (SourceGrammar -> TcA s x a) -> EvalM s a -runTcA g f = undefined {- EvalM (\gr ms msgs -> case f gr of - TcMany xs f -> do rs <- f gr ms msgs - case rs of - [(x,ms,msgs)] -> return (Success x msgs) - rs -> unTcM (g xs) gr ms msgs - TcSingle f -> f gr ms msgs) --} From 54e06b5371a99990b962975905b093b4e214cbc9 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Tue, 28 Nov 2023 10:25:27 +0100 Subject: [PATCH 09/15] refactoring --- src/compiler/GF/Compile/Compute/Concrete.hs | 30 +++++++++------------ 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index 3a25df75ff..3dd8f676ce 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -503,11 +503,18 @@ susp i env ki = EvalM $ \gr k mt d r msgs -> do value2term xs (VApp q tnks) = foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (if fst q == cPredef then Q q else QC q) tnks -value2term xs (VMeta m env tnks) = do - res <- zonk xs m tnks - case res of - Right i -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) tnks - Left v -> value2term xs v +value2term xs (VMeta m env vs) = do + s <- getRef m + case s of + Evaluated _ v -> do v <- apply v vs + value2term xs v + Unevaluated env t -> do v <- eval env t vs + value2term xs v + Bound t -> do v <- eval env t vs + value2term xs v + Hole i -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs + Residuation i _ _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs + Narrowing i _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs value2term xs (VSusp j env k vs) = do v <- k (VGen maxBound vs) value2term xs v @@ -896,16 +903,3 @@ tnk2term xs tnk = EvalM $ \gr k mt d r msgs -> Narrowing i _ -> k (Meta i) mt d r msgs scopeEnv scope = zipWithM (\x i -> newEvaluatedThunk (VGen i []) >>= \tnk -> return (x,tnk)) (reverse scope) [0..] - -zonk scope tnk vs = EvalM $ \gr k mt d r msgs -> do - s <- readSTRef tnk - case s of - Evaluated _ v -> case apply v vs of - EvalM f -> f gr (k . Left) mt d r msgs - Unevaluated env t -> case eval env t vs of - EvalM f -> f gr (k . Left) mt d r msgs - Bound t -> case scopeEnv scope >>= \env -> eval env t vs of - EvalM f -> f gr (k . Left) mt d r msgs - Hole i -> k (Right i) mt d r msgs - Residuation i _ _ -> k (Right i) mt d r msgs - Narrowing i _ -> k (Right i) mt d r msgs From 1d64d166be71047a6292503ae348d83d4346bc81 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Tue, 28 Nov 2023 14:07:09 +0100 Subject: [PATCH 10/15] fix the so command in case of dependent types --- src/compiler/GF/Command/SourceCommands.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/compiler/GF/Command/SourceCommands.hs b/src/compiler/GF/Command/SourceCommands.hs index f254f61458..3aee7b41f0 100644 --- a/src/compiler/GF/Command/SourceCommands.hs +++ b/src/compiler/GF/Command/SourceCommands.hs @@ -212,9 +212,8 @@ sourceCommands = Map.fromList [ return $ allOpersTo sgr ty _ -> return $ allOpers sgr let sigs = [(op,ty) | ((mo,op),ty,pos) <- ops] - printer = if isOpt "raw" os - then showTerm sgr TermPrintDefault Qualified - else (render . TC.ppType) + printer = showTerm sgr TermPrintDefault + (if isOpt "raw" os then Qualified else Unqualified) printed = [unwords [showIdent op, ":", printer ty] | (op,ty) <- sigs] return . fromString $ unlines [l | l <- printed, all (`isInfixOf` l) greps] From 5232364a9eec2d4feca1d713bc8c399d233bfd05 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Tue, 28 Nov 2023 21:21:34 +0100 Subject: [PATCH 11/15] typechecking without Value<->Term conversion --- src/compiler/GF/Compile/Compute/Concrete.hs | 53 +-- src/compiler/GF/Compile/GeneratePMCFG.hs | 2 +- .../GF/Compile/TypeCheck/ConcreteNew.hs | 434 ++++++++++++++---- 3 files changed, 368 insertions(+), 121 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index 3dd8f676ce..b8d84116b6 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -56,7 +56,6 @@ data ThunkState s | Hole {-# UNPACK #-} !MetaId | Narrowing {-# UNPACK #-} !MetaId Type | Residuation {-# UNPACK #-} !MetaId (Scope s) (Sigma s) - | Bound Term type Thunk s = STRef s (ThunkState s) type Env s = [(Ident,Thunk s)] @@ -64,8 +63,8 @@ type Scope s = [(Ident,Value s)] data Value s = VApp QIdent [Thunk s] - | VMeta (Thunk s) (Env s) [Thunk s] - | VSusp (Thunk s) (Env s) (Value s -> EvalM s (Value s)) [Thunk s] + | VMeta (Thunk s) [Thunk s] + | VSusp (Thunk s) (Value s -> EvalM s (Value s)) [Thunk s] | VGen {-# UNPACK #-} !Int [Thunk s] | VClosure (Env s) Term | VProd BindType Ident (Value s) (Value s) @@ -95,9 +94,9 @@ data Value s showValue (VApp q tnks) = "(VApp "++unwords (show q : map (const "_") tnks) ++ ")" -showValue (VMeta _ _ _) = "VMeta" -showValue (VSusp _ _ _ _) = "VSusp" -showValue (VGen _ _) = "VGen" +showValue (VMeta _ _) = "VMeta" +showValue (VSusp _ _ _) = "VSusp" +showValue (VGen i _) = "(VGen "++show i++")" showValue (VClosure _ _) = "VClosure" showValue (VProd _ x v1 v2) = "VProd ("++show x++") ("++showValue v1++") ("++showValue v2++")" showValue (VRecType _) = "VRecType" @@ -108,7 +107,7 @@ showValue (VTable v1 v2) = "VTable ("++showValue v1++") ("++showValue v2++")" showValue (VT _ _ cs) = "(VT "++show cs++")" showValue (VV _ _) = "VV" showValue (VS v _ _) = "(VS "++showValue v++")" -showValue (VSort _) = "VSort" +showValue (VSort s) = "(VSort "++show s++")" showValue (VInt _) = "VInt" showValue (VFlt _) = "VFlt" showValue (VStr s) = "(VStr "++show s++")" @@ -142,7 +141,7 @@ eval env (App t1 t2) vs = do tnk <- newThunk env t2 eval env (Abs b x t) [] = return (VClosure env (Abs b x t)) eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs eval env (Meta i) vs = do tnk <- newHole i - return (VMeta tnk env vs) + return (VMeta tnk vs) eval env (ImplArg t) [] = eval env t [] eval env (Prod b x t1 t2)[] = do v1 <- eval env t1 [] return (VProd b x v1 (VClosure env t2)) @@ -256,8 +255,8 @@ eval env (TSymCat d r rs) []= do rs <- forM rs $ \(i,(pv,ty)) -> eval env (TSymVar d r) [] = do return (VSymVar d r) eval env t vs = evalError ("Cannot reduce term" <+> pp t) -apply (VMeta m env vs0) vs = return (VMeta m env (vs0++vs)) -apply (VSusp m env k vs0) vs = return (VSusp m env k (vs0++vs)) +apply (VMeta m vs0) vs = return (VMeta m (vs0++vs)) +apply (VSusp m k vs0) vs = return (VSusp m k (vs0++vs)) apply (VApp f vs0) vs = return (VApp f (vs0++vs)) apply (VGen i vs0) vs = return (VGen i (vs0++vs)) apply (VClosure env (Abs b x t)) (v:vs) = eval ((x,v):env) t vs @@ -345,9 +344,9 @@ patternMatch v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0 match' env p ps eqs arg v args = do case (p,v) of - (p, VMeta i envi vs) -> susp i envi (\v -> apply v vs >>= \v -> match' env p ps eqs arg v args) - (p, VGen i vs ) -> return v0 - (p, VSusp i envi k vs) -> susp i envi (\v -> k v >>= \v -> apply v vs >>= \v -> match' env p ps eqs arg v args) + (p, VMeta i vs) -> susp i (\v -> apply v vs >>= \v -> match' env p ps eqs arg v args) + (p, VGen i vs) -> return v0 + (p, VSusp i k vs) -> susp i (\v -> k v >>= \v -> apply v vs >>= \v -> match' env p ps eqs arg v args) (PP q qs, VApp r tnks) | q == r -> match env (qs++ps) eqs (tnks++args) (PR pas, VR as) -> matchRec env (reverse pas) as ps eqs args @@ -443,18 +442,18 @@ vtableSelect v0 ty tnks tnk2 vs = do return (r*cnt'+r',cnt*cnt') value2index (VInt n) ty | Just max <- isTypeInts ty = return (fromIntegral n,fromIntegral max+1) - value2index (VMeta i envi vs) ty = do - v <- susp i envi (\v -> apply v vs) + value2index (VMeta i vs) ty = do + v <- susp i (\v -> apply v vs) value2index v ty - value2index (VSusp i envi k vs) ty = do - v <- susp i envi (\v -> k v >>= \v -> apply v vs) + value2index (VSusp i k vs) ty = do + v <- susp i (\v -> k v >>= \v -> apply v vs) value2index v ty value2index v ty = do t <- value2term [] v evalError ("the parameter:" <+> ppTerm Unqualified 0 t $$ "cannot be evaluated at compile time.") -susp i env ki = EvalM $ \gr k mt d r msgs -> do +susp i ki = EvalM $ \gr k mt d r msgs -> do s <- readSTRef i case s of Narrowing id (QC q) -> case lookupOrigInfo gr q of @@ -465,13 +464,13 @@ susp i env ki = EvalM $ \gr k mt d r msgs -> do -> bindInt gr k mt d r msgs s 0 max Evaluated _ v -> case ki v of EvalM f -> f gr k mt d r msgs - _ -> k (VSusp i env ki []) mt d r msgs + _ -> k (VSusp i ki []) mt d r msgs where bindParam gr k mt d r msgs s m [] = return (Success r msgs) bindParam gr k mt d r msgs s m ((p, ctxt):ps) = do (mt',tnks) <- mkArgs mt ctxt let v = VApp (m,p) tnks - writeSTRef i (Evaluated (length env) v) + writeSTRef i (Evaluated 0 v) res <- case ki v of EvalM f -> f gr k mt' d r msgs writeSTRef i s @@ -491,7 +490,7 @@ susp i env ki = EvalM $ \gr k mt d r msgs -> do bindInt gr k mt d r msgs s iv max | iv <= max = do let v = VInt iv - writeSTRef i (Evaluated (length env) v) + writeSTRef i (Evaluated 0 v) res <- case ki v of EvalM f -> f gr k mt d r msgs writeSTRef i s @@ -503,19 +502,17 @@ susp i env ki = EvalM $ \gr k mt d r msgs -> do value2term xs (VApp q tnks) = foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (if fst q == cPredef then Q q else QC q) tnks -value2term xs (VMeta m env vs) = do +value2term xs (VMeta m vs) = do s <- getRef m case s of Evaluated _ v -> do v <- apply v vs value2term xs v Unevaluated env t -> do v <- eval env t vs value2term xs v - Bound t -> do v <- eval env t vs - value2term xs v Hole i -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs Residuation i _ _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs Narrowing i _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs -value2term xs (VSusp j env k vs) = do +value2term xs (VSusp j k vs) = do v <- k (VGen maxBound vs) value2term xs v value2term xs (VGen j tnks) = @@ -861,9 +858,9 @@ force tnk = EvalM $ \gr k mt d r msgs -> do writeSTRef tnk s return r) mt d r msgs Evaluated d v -> k v mt d r msgs - Hole _ -> k (VMeta tnk [] []) mt d r msgs - Residuation _ _ _ -> k (VMeta tnk [] []) mt d r msgs - Narrowing _ _ -> k (VMeta tnk [] []) mt d r msgs + Hole _ -> k (VMeta tnk []) mt d r msgs + Residuation _ _ _ -> k (VMeta tnk []) mt d r msgs + Narrowing _ _ -> k (VMeta tnk []) mt d r msgs tnk2term xs tnk = EvalM $ \gr k mt d r msgs -> let join f g = do res <- f diff --git a/src/compiler/GF/Compile/GeneratePMCFG.hs b/src/compiler/GF/Compile/GeneratePMCFG.hs index 8995972e22..0a0b23be41 100644 --- a/src/compiler/GF/Compile/GeneratePMCFG.hs +++ b/src/compiler/GF/Compile/GeneratePMCFG.hs @@ -253,7 +253,7 @@ param2int (VApp q tnks) ty = do return (r*cnt'+r',combine' cnt rs cnt' rs',cnt*cnt') param2int (VInt n) ty | Just max <- isTypeInts ty= return (fromIntegral n,[],fromIntegral max+1) -param2int (VMeta tnk _ _) ty = do +param2int (VMeta tnk _) ty = do tnk_st <- getRef tnk case tnk_st of Evaluated _ v -> param2int v ty diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index d7a22cddd2..40e99c3bc6 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -27,14 +27,14 @@ checkLType :: Grammar -> Term -> Type -> Check (Term, Type) checkLType gr t ty = runEvalOneM gr $ do vty <- eval [] ty [] (t,_) <- tcRho [] t (Just vty) - t <- zonkTerm t + t <- zonkTerm [] t return (t,ty) inferLType :: Grammar -> Term -> Check (Term, Type) inferLType gr t = runEvalOneM gr $ do (t,ty) <- inferSigma [] t - t <- zonkTerm t - ty <- zonkTerm =<< value2term [] ty + t <- zonkTerm [] t + ty <- value2term [] ty return (t,ty) inferSigma :: Scope s -> Term -> EvalM s (Term,Sigma s) @@ -72,21 +72,94 @@ tcRho scope t@(App fun arg) mb_ty = do (t,ty) <- tcApp scope t t instSigma scope t ty mb_ty tcRho scope (Abs bt var body) Nothing = do -- ABS1 - (_,tnk) <- newResiduation scope vtypeType - env <- scopeEnv scope - let arg_ty = VMeta tnk env [] + (i,tnk) <- newResiduation scope vtypeType + let arg_ty = VMeta tnk [] (body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing - return (Abs bt var body, (VProd bt identW arg_ty body_ty)) + let m = length scope + n = m+1 + (b,used_bndrs) <- check m n (False,[]) body_ty + if b + then let v = head (allBinders \\ used_bndrs) + in return (Abs bt var body, (VProd bt v arg_ty body_ty)) + else return (Abs bt var body, (VProd bt identW arg_ty body_ty)) + where + check m n st (VApp f vs) = foldM (follow m n) st vs + check m n st (VMeta i vs) = do + s <- getRef i + case s of + Evaluated _ v -> do v <- apply v vs + check m n st v + _ -> foldM (follow m n) st vs + check m n st@(b,xs) (VGen i vs) + | i == m = return (True, xs) + | otherwise = return st + check m n st (VClosure env (Abs bt x t)) = do + tnk <- newEvaluatedThunk (VGen n []) + v <- eval ((x,tnk):env) t [] + check m (n+1) st v + check m n st (VProd _ x v1 v2) = do + st@(b,xs) <- check m n st v1 + case v2 of + VClosure env t -> do tnk <- newEvaluatedThunk (VGen n []) + v2 <- eval ((x,tnk):env) t [] + check m (n+1) (b,x:xs) v2 + v2 -> check m n st v2 + check m (n+1) (b,x:xs) v2 + check m n st (VRecType as) = foldM (\st (l,v) -> check m n st v) st as + check m n st (VR as) = + foldM (\st (lbl,tnk) -> follow m n st tnk) st as + check m n st (VP v l vs) = + check m n st v >>= \st -> foldM (follow m n) st vs + check m n st (VExtR v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VTable v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VT ty env cs) = + check m n st ty -- Traverse cs as well + check m n st (VV ty cs) = + check m n st ty >>= \st -> foldM (follow m n) st cs + check m n st (VS v1 tnk vs) = do + st <- check m n st v1 + st <- follow m n st tnk + foldM (follow m n) st vs + check m n st (VSort _) = return st + check m n st (VInt _) = return st + check m n st (VFlt _) = return st + check m n st (VStr _) = return st + check m n st VEmpty = return st + check m n st (VC v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VGlue v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VPatt _ _ _) = return st + check m n st (VPattType v) = check m n st v + check m n st (VAlts v vs) = do + st <- check m n st v + foldM (\st (v1,v2) -> check m n st v1 >>= \st -> check m n st v2) st vs + check m n st (VStrs vs) = + foldM (check m n) st vs + check m n st v = error (showValue v) + + follow m n st tnk = force tnk >>= \v -> check m n st v + tcRho scope t@(Abs Implicit var body) (Just ty) = do -- ABS2 - (bt, _, var_ty, body_ty) <- unifyFun scope ty + (bt, x, var_ty, body_ty) <- unifyFun scope ty if bt == Implicit then return () else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") + body_ty <- case body_ty of + VClosure env body_ty -> do tnk <- newEvaluatedThunk (VGen (length scope) []) + eval ((x,tnk):env) body_ty [] + body_ty -> return body_ty (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (Abs Implicit var body,ty) tcRho scope (Abs Explicit var body) (Just ty) = do -- ABS3 (scope,f,ty') <- skolemise scope ty - (_,_,var_ty,body_ty) <- unifyFun scope ty' + (_,x,var_ty,body_ty) <- unifyFun scope ty' + body_ty <- case body_ty of + VClosure env body_ty -> do tnk <- newEvaluatedThunk (VGen (length scope) []) + eval ((x,tnk):env) body_ty [] + body_ty -> return body_ty (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (f (Abs Explicit var body),ty) tcRho scope (Meta i) (Just ty) = do @@ -95,7 +168,7 @@ tcRho scope (Meta i) (Just ty) = do tcRho scope (Meta _) Nothing = do (_,tnk) <- newResiduation scope vtypeType env <- scopeEnv scope - let vty = VMeta tnk env [] + let vty = VMeta tnk [] (i,_) <- newResiduation scope vty return (Meta i, vty) tcRho scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET @@ -114,12 +187,12 @@ tcRho scope (Typed body ann_ty) mb_ty = do -- ANNOT env <- scopeEnv scope v_ann_ty <- eval env ann_ty [] (body,_) <- tcRho scope body (Just v_ann_ty) - instSigma scope (Typed body ann_ty) v_ann_ty mb_ty + (res1,res2) <- instSigma scope (Typed body ann_ty) v_ann_ty mb_ty + return (res1,res2) tcRho scope (FV ts) mb_ty = do case ts of [] -> do (i,tnk) <- newResiduation scope vtypeType - env <- scopeEnv scope - instSigma scope (FV []) (VMeta tnk env []) mb_ty + instSigma scope (FV []) (VMeta tnk []) mb_ty (t:ts) -> do (t,ty) <- tcRho scope t mb_ty let go [] ty = return ([],ty) @@ -140,12 +213,12 @@ tcRho scope t@(RecType rs) (Just ty) = do VSort s | s == cType -> return () | s == cPType -> return () - VMeta i env vs -> case rs of - [] -> unifyVar scope i env vs vtypePType - _ -> return () - ty -> do ty <- zonkTerm =<< value2term (scopeVars scope) ty - evalError ("The record type" <+> ppTerm Unqualified 0 t $$ - "cannot be of type" <+> ppTerm Unqualified 0 ty) + VMeta i vs -> case rs of + [] -> unifyVar scope i vs vtypePType + _ -> return () + ty -> do ty <- value2term (scopeVars scope) ty + evalError ("The record type" <+> ppTerm Unqualified 0 t $$ + "cannot be of type" <+> ppTerm Unqualified 0 ty) (rs,mb_ty) <- tcRecTypeFields scope rs (Just ty') return (f (RecType rs),ty) tcRho scope t@(Table p res) mb_ty = do @@ -160,7 +233,7 @@ tcRho scope (Prod bt x ty1 ty2) mb_ty = do instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty tcRho scope (S t p) mb_ty = do env <- scopeEnv scope - let mk_val (_,tnk) = VMeta tnk env [] + let mk_val (_,tnk) = VMeta tnk [] p_ty <- fmap mk_val $ newResiduation scope vtypePType res_ty <- case mb_ty of Nothing -> fmap mk_val $ newResiduation scope vtypeType @@ -171,7 +244,7 @@ tcRho scope (S t p) mb_ty = do return (S t p, res_ty) tcRho scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables env <- scopeEnv scope - let mk_val (_,tnk) = VMeta tnk env [] + let mk_val (_,tnk) = VMeta tnk [] p_ty <- case tt of TRaw -> fmap mk_val $ newResiduation scope vtypePType TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) @@ -214,9 +287,8 @@ tcRho scope (R rs) (Just ty) = do tcRho scope (P t l) mb_ty = do l_ty <- case mb_ty of Just ty -> return ty - Nothing -> do env <- scopeEnv scope - (i,tnk) <- newResiduation scope vtypeType - return (VMeta tnk env []) + Nothing -> do (i,tnk) <- newResiduation scope vtypeType + return (VMeta tnk []) (t,t_ty) <- tcRho scope t (Just (VRecType [(l,l_ty)])) return (P t l,l_ty) tcRho scope (C t1 t2) mb_ty = do @@ -261,7 +333,7 @@ tcRho scope t@(EPatt min max p) mb_ty = do (scope,f,ty) <- case mb_ty of Nothing -> do env <- scopeEnv scope (i,tnk) <- newResiduation scope vtypeType - return (scope,id,VMeta tnk env []) + return (scope,id,VMeta tnk []) Just ty -> do (scope,f,ty) <- skolemise scope ty case ty of VPattType ty -> return (scope,f,ty) @@ -279,13 +351,16 @@ tcCases scope ((p,t):cs) p_ty mb_res_ty = do tcApp scope t0 t@(App fun (ImplArg arg)) = do -- APP1 (fun,fun_ty) <- tcApp scope t0 fun - (bt, _, arg_ty, res_ty) <- unifyFun scope fun_ty + (bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty if (bt == Implicit) then return () else evalError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected") (arg,_) <- tcRho scope arg (Just arg_ty) - env <- scopeEnv scope - varg <- eval env arg [] + res_ty <- case res_ty of + VClosure res_env res_ty -> do env <- scopeEnv scope + tnk <- newThunk env arg + eval ((x,tnk):res_env) res_ty [] + res_ty -> return res_ty return (App fun (ImplArg arg), res_ty) tcApp scope t0 (App fun arg) = do -- APP2 (fun,fun_ty) <- tcApp scope t0 fun @@ -349,8 +424,7 @@ tcPatt scope (PR rs) ty0 = do let mk_ltys [] = return [] mk_ltys ((l,p):rs) = do (_,tnk) <- newResiduation scope vtypePType ltys <- mk_ltys rs - env <- scopeEnv scope - return ((l,p,VMeta tnk env []) : ltys) + return ((l,p,VMeta tnk []) : ltys) go scope [] = return scope go scope ((l,p,ty):rs) = do scope <- tcPatt scope p ty go scope rs @@ -410,8 +484,8 @@ tcRecTypeFields scope ((l,ty):rs) mb_ty = do VSort s | s == cType -> return (Just sort) | s == cPType -> return mb_ty - VMeta _ _ _ -> return mb_ty - _ -> do sort <- zonkTerm =<< value2term (scopeVars scope) sort + VMeta _ _ -> return mb_ty + _ -> do sort <- value2term (scopeVars scope) sort evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ "cannot be of type" <+> ppTerm Unqualified 0 sort) (rs,mb_ty) <- tcRecTypeFields scope rs mb_ty @@ -427,20 +501,20 @@ instSigma scope t ty1 (Just ty2) = do -- INST2 -- | Invariant: the second argument is in weak-prenex form subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> EvalM s Term -subsCheckRho scope t ty1@(VMeta i env vs) ty2 = do +subsCheckRho scope t ty1@(VMeta i vs) ty2 = do mv <- getRef i case mv of Residuation _ _ _ -> do unify scope ty1 ty2 return t - Bound ty1 -> do vty1 <- eval env ty1 vs - subsCheckRho scope t vty1 ty2 -subsCheckRho scope t ty1 ty2@(VMeta i env vs) = do + Evaluated _ ty1 -> do ty1 <- apply ty1 vs + subsCheckRho scope t ty1 ty2 +subsCheckRho scope t ty1 ty2@(VMeta i vs) = do mv <- getRef i case mv of Residuation _ _ _ -> do unify scope ty1 ty2 return t - Bound ty2 -> do vty2 <- eval env ty2 vs - subsCheckRho scope t ty1 vty2 + Evaluated _ ty2 -> do ty2 <- apply ty2 vs + subsCheckRho scope t ty1 ty2 subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do -- Rule SPEC (i,tnk) <- newResiduation scope ty1 ty2 <- case ty2 of @@ -551,7 +625,7 @@ unifyFun :: Scope s -> Rho s -> EvalM s (BindType, Ident, Sigma s, Rho s) unifyFun scope (VProd bt x arg res) = return (bt,x,arg,res) unifyFun scope tau = do - let mk_val (_,tnk) = VMeta tnk [] [] + let mk_val (_,tnk) = VMeta tnk [] arg <- fmap mk_val $ newResiduation scope vtypeType res <- fmap mk_val $ newResiduation scope vtypeType let bt = Explicit @@ -562,8 +636,7 @@ unifyTbl :: Scope s -> Rho s -> EvalM s (Sigma s, Rho s) unifyTbl scope (VTable arg res) = return (arg,res) unifyTbl scope tau = do - env <- scopeEnv scope - let mk_val (i,tnk) = VMeta tnk env [] + let mk_val (i,tnk) = VMeta tnk [] arg <- fmap mk_val $ newResiduation scope vtypePType res <- fmap mk_val $ newResiduation scope vtypeType unify scope tau (VTable arg res) @@ -578,17 +651,30 @@ unify scope (VGen i vs1) (VGen j vs2) unify scope (VTable p1 res1) (VTable p2 res2) = do unify scope p1 p2 unify scope res1 res2 -unify scope (VMeta i env1 vs1) (VMeta j env2 vs2) - | i == j = sequence_ (zipWith (unifyThunk scope) vs1 vs2) - | otherwise = do mv <- getRef j - case mv of - Bound t2 -> do v2 <- eval env2 t2 vs2 - unify scope (VMeta i env1 vs1) v2 - Residuation j _ _ -> setRef i (Bound (Meta j)) +unify scope (VMeta i vs1) (VMeta j vs2) + | i == j = sequence_ (zipWith (unifyThunk scope) vs1 vs2) + | otherwise = do + mv <- getRef i + case mv of + Evaluated _ v1 -> do + v1 <- apply v1 vs1 + unify scope v1 (VMeta j vs2) + Residuation _ scope1 _ -> do + mv <- getRef j + case mv of + Evaluated _ v2 -> do + v2 <- apply v2 vs2 + unify scope (VMeta i vs1) v2 + Residuation _ scope2 _ + | m > n -> setRef i (Evaluated m (VMeta j vs2)) + | otherwise -> setRef j (Evaluated n (VMeta i vs2)) + where + m = length scope1 + n = length scope2 unify scope (VInt i) (VInt j) | i == j = return () -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 (VMeta i vs) v = unifyVar scope i vs v +unify scope v (VMeta i vs) = unifyVar scope i vs v unify scope v1 v2 = do t1 <- value2term (scopeVars scope) v1 t2 <- value2term (scopeVars scope) v2 @@ -602,18 +688,78 @@ unifyThunk scope tnk1 tnk2 = do (Evaluated _ v1,Evaluated _ v2) -> unify scope v1 v2 -- | Invariant: tv1 is a flexible type variable -unifyVar :: Scope s -> Thunk s -> Env s -> [Thunk s] -> Tau s -> EvalM s () -unifyVar scope tnk env vs ty2 = do -- Check whether i is bound +unifyVar :: Scope s -> Thunk s -> [Thunk s] -> Tau s -> EvalM s () +unifyVar scope tnk vs ty2 = do -- Check whether i is bound mv <- getRef tnk case mv of - Bound ty1 -> do v <- eval env ty1 vs - unify scope v ty2 - Residuation i scope' _ -> do ty2' <- value2term (scopeVars scope') ty2 - ms2 <- getMetaVars [(scope,ty2)] - if tnk `elem` ms2 - then evalError ("Occurs check for" <+> ppMeta i <+> "in:" $$ - nest 2 (ppTerm Unqualified 0 ty2')) - else setRef tnk (Bound ty2') + Evaluated _ ty1 -> do ty1 <- apply ty1 vs + unify scope ty1 ty2 + Residuation i scope' _ -> do let m = length scope' + n = length scope + check m n ty2 + setRef tnk (Evaluated m ty2) + where + check m n (VApp f vs) = mapM_ (follow m n) vs + check m n (VMeta i vs) + | tnk == i = do ty1 <- value2term (scopeVars scope) (VMeta tnk vs) + ty2 <- value2term (scopeVars scope) ty2 + evalError ("Occurs check for" <+> ppTerm Unqualified 0 ty1 <+> "in:" $$ + nest 2 (ppTerm Unqualified 0 ty2)) + | otherwise = do + s <- getRef i + case s of + Evaluated _ v -> do v <- apply v vs + check m n v + _ -> mapM_ (follow m n) vs + check m n (VGen i vs) + | i > m = let (v,_) = reverse scope !! i + in evalError ("Variable" <+> pp v <+> "has escaped") + | otherwise = mapM_ (follow m n) vs + check m n (VClosure env (Abs bt x t)) = do + tnk <- newEvaluatedThunk (VGen n []) + v <- eval ((x,tnk):env) t [] + check (m+1) (n+1) v + check m n (VProd bt x ty1 ty2) = do + check m n ty1 + case ty2 of + VClosure env t -> do tnk <- newEvaluatedThunk (VGen n []) + v <- eval ((x,tnk):env) t [] + check (m+1) (n+1) v + _ -> check m n ty2 + check m n (VRecType as) = + mapM_ (\(lbl,v) -> check m n v) as + check m n (VR as) = + mapM_ (\(lbl,tnk) -> follow m n tnk) as + check m n (VP v l vs) = + check m n v >> mapM_ (follow m n) vs + check m n (VExtR v1 v2) = + check m n v1 >> check m n v2 + check m n (VTable v1 v2) = + check m n v1 >> check m n v2 + check m n (VT ty env cs) = + check m n ty -- Traverse cs as well + check m n (VV ty cs) = + check m n ty >> mapM_ (follow m n) cs + check m n (VS v1 tnk vs) = + check m n v1 >> follow m n tnk >> mapM_ (follow m n) vs + check m n (VSort _) = return () + check m n (VInt _) = return () + check m n (VFlt _) = return () + check m n (VStr _) = return () + check m n VEmpty = return () + check m n (VC v1 v2) = + check m n v1 >> check m n v2 + check m n (VGlue v1 v2) = + check m n v1 >> check m n v2 + check m n (VPatt _ _ _) = return () + check m n (VPattType v) = + check m n v + check m n (VAlts v vs) = + check m n v >> mapM_ (\(v1,v2) -> check m n v1 >> check m n v2) vs + check m n (VStrs vs) = + mapM_ (check m n) vs + + follow m n tnk = check m n =<< force tnk ----------------------------------------------------------------------- -- Instantiation and quantification @@ -632,11 +778,11 @@ instantiate scope t ty = do -- | Build fresh lambda abstractions for the topmost implicit arguments skolemise :: Scope s -> Sigma s -> EvalM s (Scope s, Term->Term, Rho s) -skolemise scope ty@(VMeta i env vs) = do +skolemise scope ty@(VMeta i vs) = do mv <- getRef i case mv of Residuation _ _ _ -> return (scope,id,ty) -- guarded constant? - Bound ty -> do ty <- eval env ty vs + Evaluated _ ty -> do ty <- apply ty vs skolemise scope ty skolemise scope (VProd Implicit x ty1 ty2) = do let v = newVar scope @@ -652,17 +798,112 @@ skolemise scope ty = do -- | Quantify over the specified type variables (all flexible) quantify :: Scope s -> Term -> [Thunk s] -> Rho s -> EvalM s (Term,Sigma s) quantify scope t tvs ty = do - let used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use - new_bndrs = take (length tvs) (allBinders \\ used_bndrs) - env <- scopeEnv ([(v,vtypeType) | v <- new_bndrs]++scope) - mapM_ (bind env) (zip tvs new_bndrs) - let vty = foldr (\v -> VProd Implicit v vtypeType) ty new_bndrs - return (foldr (Abs Implicit) t new_bndrs,vty) + let m = length tvs + n = length scope + (used_bndrs,ty) <- check m n [] ty + let new_bndrs = take m (allBinders \\ used_bndrs) + mapM_ bind (zip3 [0..] tvs new_bndrs) + let ty' = foldr (\ty -> VProd Implicit ty vtypeType) ty new_bndrs + return (foldr (Abs Implicit) t new_bndrs,ty') where - bind env (tnk, name) = setRef tnk (Bound (Vr name)) - - bndrs (VProd _ x v1 v2) = [x] ++ bndrs v1 ++ bndrs v2 - bndrs _ = [] + bind (i, tnk, name) = setRef tnk (Evaluated (length scope) (VGen i [])) + + check m n xs (VApp f vs) = do + (xs,vs) <- mapAccumM (follow m n) xs vs + return (xs,VApp f vs) + check m n xs (VMeta i vs) = do + s <- getRef i + case s of + Evaluated _ v -> do v <- apply v vs + check m n xs v + _ -> do (xs,vs) <- mapAccumM (follow m n) xs vs + return (xs,VMeta i vs) + check m n st (VGen i vs)= do + (st,vs) <- mapAccumM (follow m n) st vs + return (st, VGen (m+i) vs) + check m n st (VClosure env (Abs bt x t)) = do + (st,env) <- mapAccumM (\st (x,tnk) -> follow m n st tnk >>= \(st,tnk) -> return (st,(x,tnk))) st env + return (st,VClosure env (Abs bt x t)) + check m n xs (VProd bt x v1 v2) = do + (xs,v1) <- check m n xs v1 + case v2 of + VClosure env t -> do tnk <- newEvaluatedThunk (VGen n []) + (st,env) <- mapAccumM (\xs (x,tnk) -> follow m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env + return (x:xs,VProd bt x v1 (VClosure env t)) + v2 -> do (xs,v2) <- check m (n+1) xs v2 + return (x:xs,VProd bt x v1 v2) + check m n xs (VRecType as) = do + (xs,as) <- mapAccumM (\xs (l,v) -> check m n xs v >>= \(xs,v) -> return (xs,(l,v))) xs as + return (xs,VRecType as) + check m n xs (VR as) = do + (xs,as) <- mapAccumM (\xs (lbl,tnk) -> follow m n xs tnk >>= \(xs,tnk) -> return (xs,(lbl,tnk))) xs as + return (xs,VR as) + check m n xs (VP v l vs) = do + (xs,v) <- check m n xs v + (xs,vs) <- mapAccumM (follow m n) xs vs + return (xs,VP v l vs) + check m n xs (VExtR v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VExtR v1 v2) + check m n xs (VTable v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VTable v1 v2) + check m n xs (VT ty env cs) = do + (xs,ty) <- check m n xs ty + (xs,env) <- mapAccumM (\xs (x,tnk) -> follow m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env + return (xs,VT ty env cs) + check m n xs (VV ty cs) = do + (xs,ty) <- check m n xs ty + (xs,cs) <- mapAccumM (follow m n) xs cs + return (xs,VV ty cs) + check m n xs (VS v1 tnk vs) = do + (xs,v1) <- check m n xs v1 + (xs,tnk) <- follow m n xs tnk + (xs,vs) <- mapAccumM (follow m n) xs vs + return (xs,VS v1 tnk vs) + check m n xs v@(VSort _) = return (xs,v) + check m n xs v@(VInt _) = return (xs,v) + check m n xs v@(VFlt _) = return (xs,v) + check m n xs v@(VStr _) = return (xs,v) + check m n xs v@VEmpty = return (xs,v) + check m n xs (VC v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VC v1 v2) + check m n xs (VGlue v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VGlue v1 v2) + check m n xs v@(VPatt _ _ _) = return (xs,v) + check m n xs (VPattType v) = do + (xs,v) <- check m n xs v + return (xs,VPattType v) + check m n xs (VAlts v vs) = do + (xs,v) <- check m n xs v + (xs,vs) <- mapAccumM (\xs (v1,v2) -> do (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,(v1,v2))) + xs vs + return (xs,VAlts v vs) + check m n xs (VStrs vs) = do + (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VStrs vs) + check m n st v = error (showValue v) + + follow m n st tnk = do + v <- force tnk + (st,v) <- check m n st v + tnk <- newEvaluatedThunk v + return (st,tnk) + + mapAccumM :: Monad m => (a -> b -> m (a,c)) -> a -> [b] -> m (a,[c]) + mapAccumM f s [] = return (s,[]) + mapAccumM f s (x:xs) = do + (s,y) <- f s x + (s,ys) <- mapAccumM f s xs + return (s,y:ys) allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,... allBinders = [ identS [x] | x <- ['a'..'z'] ] ++ @@ -699,24 +940,35 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go ty acc) [] sc_tys follow acc tnk = force tnk >>= \v -> go v acc -- Get the MetaIds from a term; no duplicates in result - go (VSort s) acc = return acc - go (VInt _) acc = return acc - go (VRecType as) acc = foldM (\acc (lbl,v) -> go v acc) acc as - go (VClosure _ _) acc = return acc - go (VProd b x v1 v2) acc = go v2 acc >>= go v1 - go (VTable v1 v2) acc = go v2 acc >>= go v1 - go (VMeta m env args) acc - | m `elem` acc = return acc - | otherwise = do res <- getRef m - case res of - Bound _ -> return acc - _ -> foldM follow (m:acc) args - go (VApp f args) acc = foldM follow acc args - go v acc = unimplemented ("go "++showValue v) + go (VGen i args) acc = foldM follow acc args + go (VSort s) acc = return acc + go (VInt _) acc = return acc + go (VRecType as) acc = foldM (\acc (lbl,v) -> go v acc) acc as + go (VClosure _ _) acc = return acc + go (VProd b x v1 v2) acc = go v2 acc >>= go v1 + go (VTable v1 v2) acc = go v2 acc >>= go v1 + go (VMeta m args) acc + | m `elem` acc = return acc + | otherwise = do res <- getRef m + case res of + Evaluated _ v -> go v acc + _ -> foldM follow (m:acc) args + go (VApp f args) acc = foldM follow acc args + go v acc = unimplemented ("go "++showValue v) -- | Eliminate any substitutions in a term -zonkTerm :: Term -> EvalM s Term -zonkTerm (Meta i) = do +zonkTerm :: [Ident] -> Term -> EvalM s Term +zonkTerm xs (Abs b x t) = do + t <- zonkTerm (x:xs) t + return (Abs b x t) +zonkTerm xs (Prod b x t1 t2) = do + t1 <- zonkTerm xs t1 + t2 <- zonkTerm xs' t2 + return (Prod b x t1 t2) + where + xs' | x == identW = xs + | otherwise = x:xs +zonkTerm xs (Meta i) = do tnk <- EvalM $ \gr k mt d r msgs -> case Map.lookup i mt of Just v -> k v mt d r msgs @@ -726,7 +978,5 @@ zonkTerm (Meta i) = do Hole _ -> return (Meta i) Residuation _ _ _ -> return (Meta i) Narrowing _ _ -> return (Meta i) - Bound t -> do t <- zonkTerm t - setRef tnk (Bound t) -- "Short out" multiple hops - return t -zonkTerm t = composOp zonkTerm t + Evaluated _ v -> zonkTerm xs =<< value2term xs v +zonkTerm xs t = composOp (zonkTerm xs) t From 8540e44e9d00d1b756816707a02ab21c82c42f75 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Wed, 29 Nov 2023 08:47:40 +0100 Subject: [PATCH 12/15] small fixes --- .../GF/Compile/TypeCheck/ConcreteNew.hs | 39 +++++++++++++++---- 1 file changed, 32 insertions(+), 7 deletions(-) diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index 40e99c3bc6..f8e4129522 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -167,7 +167,6 @@ tcRho scope (Meta i) (Just ty) = do return (Meta i, ty) tcRho scope (Meta _) Nothing = do (_,tnk) <- newResiduation scope vtypeType - env <- scopeEnv scope let vty = VMeta tnk [] (i,_) <- newResiduation scope vty return (Meta i, vty) @@ -232,7 +231,6 @@ tcRho scope (Prod bt x ty1 ty2) mb_ty = do (ty2,ty2_ty) <- tcRho ((x,vty1):scope) ty2 (Just vtypeType) instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty tcRho scope (S t p) mb_ty = do - env <- scopeEnv scope let mk_val (_,tnk) = VMeta tnk [] p_ty <- fmap mk_val $ newResiduation scope vtypePType res_ty <- case mb_ty of @@ -243,11 +241,11 @@ tcRho scope (S t p) mb_ty = do (p,_) <- tcRho scope p (Just p_ty) return (S t p, res_ty) tcRho scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables - env <- scopeEnv scope let mk_val (_,tnk) = VMeta tnk [] p_ty <- case tt of TRaw -> fmap mk_val $ newResiduation scope vtypePType TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) + env <- scopeEnv scope eval env ty [] (ps,mb_res_ty) <- tcCases scope ps p_ty Nothing res_ty <- case mb_res_ty of @@ -261,10 +259,38 @@ tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for t case tt of TRaw -> return () TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) - return ()--subsCheckRho ge scope -> Term ty res_ty + env <- scopeEnv scope + ty <- eval env ty [] + subsCheckRho scope (Meta 0) ty p_ty + return () (ps,Just res_ty) <- tcCases scope ps p_ty (Just res_ty) - p_ty_t <- value2term [] p_ty + p_ty_t <- value2term (scopeVars scope) p_ty return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) +tcRho scope (V p_ty ts) Nothing = do + (p_ty, _) <- tcRho scope p_ty (Just vtypeType) + case ts of + [] -> do (i,tnk) <- newResiduation scope vtypeType + return (V p_ty [],VMeta tnk []) + (t:ts) -> do (t,ty) <- tcRho scope t Nothing + + let go [] ty = return ([],ty) + go (t:ts) ty = do (t, ty) <- tcRho scope t (Just ty) + (ts,ty) <- go ts ty + return (t:ts,ty) + + (ts,ty) <- go ts ty + env <- scopeEnv scope + p_vty <- eval env p_ty [] + return (V p_ty (t:ts), VTable p_vty ty) +tcRho scope (V p_ty0 ts) (Just ty) = do + (scope,f,ty') <- skolemise scope ty + (p_ty, res_ty) <- unifyTbl scope ty' + (p_ty0, _) <- tcRho scope p_ty0 (Just vtypeType) + env <- scopeEnv scope + p_vty0 <- eval env p_ty0 [] + subsCheckRho scope (Meta 0) p_vty0 p_ty + ts <- mapM (\t -> fmap fst $ tcRho scope t (Just res_ty)) ts + return (V p_ty0 ts, VTable p_ty res_ty) tcRho scope (R rs) Nothing = do lttys <- inferRecFields scope rs rs <- mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys @@ -331,8 +357,7 @@ tcRho scope (EPattType ty) mb_ty = do instSigma scope (EPattType ty) vtypeType mb_ty tcRho scope t@(EPatt min max p) mb_ty = do (scope,f,ty) <- case mb_ty of - Nothing -> do env <- scopeEnv scope - (i,tnk) <- newResiduation scope vtypeType + Nothing -> do (i,tnk) <- newResiduation scope vtypeType return (scope,id,VMeta tnk []) Just ty -> do (scope,f,ty) <- skolemise scope ty case ty of From 2631f0af8ffd35f8103f4b3b6b1bed677097bebe Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Fri, 1 Dec 2023 15:26:24 +0100 Subject: [PATCH 13/15] partial implementation for type inference with records --- src/compiler/GF/Compile/Compute/Concrete.hs | 36 ++- .../GF/Compile/TypeCheck/ConcreteNew.hs | 267 ++++++++++++------ 2 files changed, 200 insertions(+), 103 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index b8d84116b6..18da8ffda6 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -5,7 +5,7 @@ module GF.Compile.Compute.Concrete ( normalForm , Value(..), Thunk, ThunkState(..), Env, Scope, showValue - , MetaThunks + , MetaThunks, Constraint , EvalM(..), runEvalM, runEvalOneM, evalError, evalWarn , eval, apply, force, value2term, patternMatch , newThunk, newEvaluatedThunk @@ -49,13 +49,14 @@ normalForm gr t = mkFV ts = FV ts type Sigma s = Value s +type Constraint s = Value s data ThunkState s = Unevaluated (Env s) Term | Evaluated {-# UNPACK #-} !Int (Value s) | Hole {-# UNPACK #-} !MetaId | Narrowing {-# UNPACK #-} !MetaId Type - | Residuation {-# UNPACK #-} !MetaId (Scope s) (Sigma s) + | Residuation {-# UNPACK #-} !MetaId (Scope s) (Maybe (Constraint s)) type Thunk s = STRef s (ThunkState s) type Env s = [(Ident,Thunk s)] @@ -87,10 +88,14 @@ data Value s | VPattType (Value s) | VAlts (Value s) [(Value s, Value s)] | VStrs [Value s] - -- These last constructors are only generated internally + -- These two constructors are only used internally -- in the PMCFG generator. | VSymCat Int LIndex [(LIndex, (Thunk s, Type))] | VSymVar Int Int + -- These two constructors are only used internally + -- in the type checker. + | VCRecType [(Label, Bool, Constraint s)] + | VCInts (Maybe Integer) (Maybe Integer) showValue (VApp q tnks) = "(VApp "++unwords (show q : map (const "_") tnks) ++ ")" @@ -505,13 +510,15 @@ value2term xs (VApp q tnks) = value2term xs (VMeta m vs) = do s <- getRef m case s of - Evaluated _ v -> do v <- apply v vs - value2term xs v - Unevaluated env t -> do v <- eval env t vs - value2term xs v - Hole i -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs - Residuation i _ _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs - Narrowing i _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs + Evaluated _ v -> do v <- apply v vs + value2term xs v + Unevaluated env t -> do v <- eval env t vs + value2term xs v + Hole i -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs + Residuation i _ ctr -> case ctr of + Just ctr -> value2term xs ctr + Nothing -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs + Narrowing i _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs value2term xs (VSusp j k vs) = do v <- k (VGen maxBound vs) value2term xs v @@ -594,6 +601,11 @@ value2term xs (VAlts vd vas) = do value2term xs (VStrs vs) = do ts <- mapM (value2term xs) vs return (Strs ts) +value2term xs (VCInts (Just i) Nothing) = return (App (Q (cPredef,cInts)) (EInt i)) +value2term xs (VCInts Nothing (Just j)) = return (App (Q (cPredef,cInts)) (EInt j)) +value2term xs (VCRecType lctrs) = do + ltys <- mapM (\(l,o,ctr) -> value2term xs ctr >>= \ty -> return (l,ty)) lctrs + return (RecType ltys) value2term xs v = error (showValue v) pattVars st (PP _ ps) = foldM pattVars st ps @@ -808,9 +820,9 @@ newHole i = EvalM $ \gr k mt d r msgs -> Nothing -> do tnk <- newSTRef (Hole i) k tnk (Map.insert i tnk mt) d r msgs -newResiduation scope ty = EvalM $ \gr k mt d r msgs -> do +newResiduation scope = EvalM $ \gr k mt d r msgs -> do let i = Map.size mt + 1 - tnk <- newSTRef (Residuation i scope ty) + tnk <- newSTRef (Residuation i scope Nothing) k (i,tnk) (Map.insert i tnk mt) d r msgs newNarrowing ty = EvalM $ \gr k mt d r msgs -> do diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index f8e4129522..0f2a85f084 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -72,7 +72,7 @@ tcRho scope t@(App fun arg) mb_ty = do (t,ty) <- tcApp scope t t instSigma scope t ty mb_ty tcRho scope (Abs bt var body) Nothing = do -- ABS1 - (i,tnk) <- newResiduation scope vtypeType + (i,tnk) <- newResiduation scope let arg_ty = VMeta tnk [] (body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing let m = length scope @@ -162,14 +162,13 @@ tcRho scope (Abs Explicit var body) (Just ty) = do -- ABS3 body_ty -> return body_ty (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (f (Abs Explicit var body),ty) -tcRho scope (Meta i) (Just ty) = do - (i,_) <- newResiduation scope ty +tcRho scope (Meta _) mb_ty = do + (i,_) <- newResiduation scope + ty <- case mb_ty of + Just ty -> return ty + Nothing -> do (_,tnk) <- newResiduation scope + return (VMeta tnk []) return (Meta i, ty) -tcRho scope (Meta _) Nothing = do - (_,tnk) <- newResiduation scope vtypeType - let vty = VMeta tnk [] - (i,_) <- newResiduation scope vty - return (Meta i, vty) tcRho scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET (rhs,var_ty) <- case mb_ann_ty of Nothing -> inferSigma scope rhs @@ -189,18 +188,18 @@ tcRho scope (Typed body ann_ty) mb_ty = do -- ANNOT (res1,res2) <- instSigma scope (Typed body ann_ty) v_ann_ty mb_ty return (res1,res2) tcRho scope (FV ts) mb_ty = do - case ts of - [] -> do (i,tnk) <- newResiduation scope vtypeType - instSigma scope (FV []) (VMeta tnk []) mb_ty - (t:ts) -> do (t,ty) <- tcRho scope t mb_ty - - let go [] ty = return ([],ty) - go (t:ts) ty = do (t, ty) <- tcRho scope t (Just ty) - (ts,ty) <- go ts ty - return (t:ts,ty) - - (ts,ty) <- go ts ty - return (FV (t:ts), ty) + (ty,subsume) <- + case mb_ty of + Just ty -> do return (ty, \t ty' -> return t) + Nothing -> do (i,tnk) <- newResiduation scope + let ty = VMeta tnk [] + return (ty, \t ty' -> subsCheckRho scope t ty' ty) + + let go t = do (t, ty) <- tcRho scope t mb_ty + subsume t ty + + ts <- mapM go ts + return (FV ts, ty) tcRho scope t@(Sort s) mb_ty = do instSigma scope t vtypeType mb_ty tcRho scope t@(RecType rs) Nothing = do @@ -232,9 +231,9 @@ tcRho scope (Prod bt x ty1 ty2) mb_ty = do instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty tcRho scope (S t p) mb_ty = do let mk_val (_,tnk) = VMeta tnk [] - p_ty <- fmap mk_val $ newResiduation scope vtypePType + p_ty <- fmap mk_val $ newResiduation scope res_ty <- case mb_ty of - Nothing -> fmap mk_val $ newResiduation scope vtypeType + Nothing -> fmap mk_val $ newResiduation scope Just ty -> return ty let t_ty = VTable p_ty res_ty (t,t_ty) <- tcRho scope t (Just t_ty) @@ -243,14 +242,12 @@ tcRho scope (S t p) mb_ty = do tcRho scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables let mk_val (_,tnk) = VMeta tnk [] p_ty <- case tt of - TRaw -> fmap mk_val $ newResiduation scope vtypePType + TRaw -> fmap mk_val $ newResiduation scope TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) env <- scopeEnv scope eval env ty [] - (ps,mb_res_ty) <- tcCases scope ps p_ty Nothing - res_ty <- case mb_res_ty of - Just res_ty -> return res_ty - Nothing -> fmap mk_val $ newResiduation scope vtypeType + res_ty <- fmap mk_val $ newResiduation scope + ps <- tcCases scope ps p_ty res_ty p_ty_t <- value2term [] p_ty return (T (TTyped p_ty_t) ps, VTable p_ty res_ty) tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables @@ -261,34 +258,29 @@ tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for t TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) env <- scopeEnv scope ty <- eval env ty [] - subsCheckRho scope (Meta 0) ty p_ty - return () - (ps,Just res_ty) <- tcCases scope ps p_ty (Just res_ty) + unify scope ty p_ty + ps <- tcCases scope ps p_ty res_ty p_ty_t <- value2term (scopeVars scope) p_ty return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) tcRho scope (V p_ty ts) Nothing = do (p_ty, _) <- tcRho scope p_ty (Just vtypeType) - case ts of - [] -> do (i,tnk) <- newResiduation scope vtypeType - return (V p_ty [],VMeta tnk []) - (t:ts) -> do (t,ty) <- tcRho scope t Nothing - - let go [] ty = return ([],ty) - go (t:ts) ty = do (t, ty) <- tcRho scope t (Just ty) - (ts,ty) <- go ts ty - return (t:ts,ty) - - (ts,ty) <- go ts ty - env <- scopeEnv scope - p_vty <- eval env p_ty [] - return (V p_ty (t:ts), VTable p_vty ty) + (i,tnk) <- newResiduation scope + let res_ty = VMeta tnk [] + + let go t = do (t, ty) <- tcRho scope t Nothing + subsCheckRho scope t ty res_ty + + ts <- mapM go ts + env <- scopeEnv scope + p_vty <- eval env p_ty [] + return (V p_ty ts, VTable p_vty res_ty) tcRho scope (V p_ty0 ts) (Just ty) = do (scope,f,ty') <- skolemise scope ty (p_ty, res_ty) <- unifyTbl scope ty' (p_ty0, _) <- tcRho scope p_ty0 (Just vtypeType) env <- scopeEnv scope p_vty0 <- eval env p_ty0 [] - subsCheckRho scope (Meta 0) p_vty0 p_ty + unify scope p_ty p_vty0 ts <- mapM (\t -> fmap fst $ tcRho scope t (Just res_ty)) ts return (V p_ty0 ts, VTable p_ty res_ty) tcRho scope (R rs) Nothing = do @@ -313,7 +305,7 @@ tcRho scope (R rs) (Just ty) = do tcRho scope (P t l) mb_ty = do l_ty <- case mb_ty of Just ty -> return ty - Nothing -> do (i,tnk) <- newResiduation scope vtypeType + Nothing -> do (i,tnk) <- newResiduation scope return (VMeta tnk []) (t,t_ty) <- tcRho scope t (Just (VRecType [(l,l_ty)])) return (P t l,l_ty) @@ -357,7 +349,7 @@ tcRho scope (EPattType ty) mb_ty = do instSigma scope (EPattType ty) vtypeType mb_ty tcRho scope t@(EPatt min max p) mb_ty = do (scope,f,ty) <- case mb_ty of - Nothing -> do (i,tnk) <- newResiduation scope vtypeType + Nothing -> do (i,tnk) <- newResiduation scope return (scope,id,VMeta tnk []) Just ty -> do (scope,f,ty) <- skolemise scope ty case ty of @@ -367,12 +359,12 @@ tcRho scope t@(EPatt min max p) mb_ty = do return (f (EPatt min max p), ty) tcRho scope t _ = unimplemented ("tcRho "++show t) -tcCases scope [] p_ty mb_res_ty = return ([],mb_res_ty) -tcCases scope ((p,t):cs) p_ty mb_res_ty = do +tcCases scope [] p_ty res_ty = return [] +tcCases scope ((p,t):cs) p_ty res_ty = do scope' <- tcPatt scope p p_ty - (t,res_ty) <- tcRho scope' t mb_res_ty - (cs,mb_res_ty) <- tcCases scope cs p_ty (Just res_ty) - return ((p,t):cs,mb_res_ty) + (t,_) <- tcRho scope' t (Just res_ty) + cs <- tcCases scope cs p_ty res_ty + return ((p,t):cs) tcApp scope t0 t@(App fun (ImplArg arg)) = do -- APP1 (fun,fun_ty) <- tcApp scope t0 fun @@ -430,7 +422,7 @@ tcPatt scope (PP c ps) ty0 = do return scope tcPatt scope (PInt i) ty0 = do ty <- vtypeInts i - subsCheckRho scope (EInt i) ty ty0 + unify scope ty ty0 return scope tcPatt scope (PString s) ty0 = do unify scope ty0 vtypeStr @@ -447,7 +439,7 @@ tcPatt scope (PAs x p) ty0 = do tcPatt ((x,ty0):scope) p ty0 tcPatt scope (PR rs) ty0 = do let mk_ltys [] = return [] - mk_ltys ((l,p):rs) = do (_,tnk) <- newResiduation scope vtypePType + mk_ltys ((l,p):rs) = do (_,tnk) <- newResiduation scope ltys <- mk_ltys rs return ((l,p,VMeta tnk []) : ltys) go scope [] = return scope @@ -526,22 +518,53 @@ instSigma scope t ty1 (Just ty2) = do -- INST2 -- | Invariant: the second argument is in weak-prenex form subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> EvalM s Term -subsCheckRho scope t ty1@(VMeta i vs) ty2 = do - mv <- getRef i +subsCheckRho scope t (VMeta i vs1) (VMeta j vs2) + | i == j = do sequence_ (zipWith (unifyThunk scope) vs1 vs2) + return t + | otherwise = do + mv <- getRef i + case mv of + Evaluated _ v1 -> do + v1 <- apply v1 vs1 + subsCheckRho scope t v1 (VMeta j vs2) + Residuation _ scope1 _ -> do + mv <- getRef j + case mv of + Evaluated _ v2 -> do + v2 <- apply v2 vs2 + subsCheckRho scope t (VMeta i vs1) v2 + Residuation _ scope2 _ + | m > n -> do setRef i (Evaluated m (VMeta j vs2)) + return t + | otherwise -> do setRef j (Evaluated n (VMeta i vs2)) + return t + where + m = length scope1 + n = length scope2 +subsCheckRho scope t ty1@(VMeta tnk vs) ty2 = do + mv <- getRef tnk case mv of - Residuation _ _ _ -> do unify scope ty1 ty2 - return t - Evaluated _ ty1 -> do ty1 <- apply ty1 vs - subsCheckRho scope t ty1 ty2 -subsCheckRho scope t ty1 ty2@(VMeta i vs) = do - mv <- getRef i + Evaluated _ ty1 -> do + ty1 <- apply ty1 vs + subsCheckRho scope t ty1 ty2 + Residuation i scope' ctr -> do + occursCheck scope' tnk scope ty2 + ctr <- subtype scope ctr ty2 + setRef tnk (Residuation i scope' (Just ctr)) + return t +subsCheckRho scope t ty1 ty2@(VMeta tnk vs) = do + mv <- getRef tnk case mv of - Residuation _ _ _ -> do unify scope ty1 ty2 - return t - Evaluated _ ty2 -> do ty2 <- apply ty2 vs - subsCheckRho scope t ty1 ty2 + Evaluated _ ty2 -> do + ty2 <- apply ty2 vs + subsCheckRho scope t ty1 ty2 + Residuation i scope' ctr -> do + occursCheck scope' tnk scope ty1 + ctr <- supertype scope ctr ty1 + setRef tnk (Residuation i scope' (Just ctr)) + return t subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do -- Rule SPEC - (i,tnk) <- newResiduation scope ty1 + (i,tnk) <- newResiduation scope ty2 <- case ty2 of VClosure env ty2 -> eval ((x,tnk):env) ty2 [] ty2 -> return ty2 @@ -642,6 +665,59 @@ subsCheckTbl scope t p1 r1 p2 r2 = do p2 <- value2term (scopeVars scope) p2 return (T (TTyped p2) [(PV x,t)]) +subtype scope Nothing (VApp p [tnk]) + | p == (cPredef,cInts) = do + VInt i <- force tnk + return (VCInts Nothing (Just i)) +subtype scope (Just (VCInts i j)) (VApp p [tnk]) + | p == (cPredef,cInts) = do + VInt k <- force tnk + return (VCInts j (Just (maybe k (min k) i))) +subtype scope Nothing (VRecType ltys) = do + lctrs <- mapM (\(l,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,True,ctr)) ltys + return (VCRecType lctrs) +subtype scope (Just (VCRecType lctrs)) (VRecType ltys) = do + lctrs <- foldM (\lctrs (l,ty) -> union l ty lctrs) lctrs ltys + return (VCRecType lctrs) + where + union l ty [] = do ctr <- subtype scope Nothing ty + return [(l,True,ctr)] + union l ty ((l',o,ctr):lctrs) + | l == l' = do ctr <- subtype scope (Just ctr) ty + return ((l,True,ctr):lctrs) + | otherwise = do lctrs <- union l ty lctrs + return ((l',o,ctr):lctrs) +subtype scope Nothing ty = return ty +subtype scope (Just ctr) ty = do + unify scope ctr ty + return ty + +supertype scope Nothing (VApp p [tnk]) + | p == (cPredef,cInts) = do + VInt i <- force tnk + return (VCInts (Just i) Nothing) +supertype scope (Just (VCInts i j)) (VApp p [tnk]) + | p == (cPredef,cInts) = do + VInt k <- force tnk + return (VCInts (Just (maybe k (max k) i)) j) +supertype scope Nothing (VRecType ltys) = do + lctrs <- mapM (\(l,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys + return (VCRecType lctrs) +supertype scope (Just (VCRecType lctrs)) (VRecType ltys) = do + lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs ltys) [] lctrs + return (VCRecType lctrs) + where + intersect l o ctr lctrs [] = return lctrs + intersect l o ctr lctrs ((l',ty):ltys2) + | l == l' = do ctr <- supertype scope (Just ctr) ty + return ((l,o,ctr):lctrs) + | otherwise = do intersect l o ctr lctrs ltys2 +supertype scope Nothing ty = return ty +supertype scope (Just ctr) ty = do + unify scope ctr ty + return ty + + ----------------------------------------------------------------------- -- Unification ----------------------------------------------------------------------- @@ -651,8 +727,8 @@ unifyFun scope (VProd bt x arg res) = return (bt,x,arg,res) unifyFun scope tau = do let mk_val (_,tnk) = VMeta tnk [] - arg <- fmap mk_val $ newResiduation scope vtypeType - res <- fmap mk_val $ newResiduation scope vtypeType + arg <- fmap mk_val $ newResiduation scope + res <- fmap mk_val $ newResiduation scope let bt = Explicit unify scope tau (VProd bt identW arg res) return (bt,identW,arg,res) @@ -662,20 +738,13 @@ unifyTbl scope (VTable arg res) = return (arg,res) unifyTbl scope tau = do let mk_val (i,tnk) = VMeta tnk [] - arg <- fmap mk_val $ newResiduation scope vtypePType - res <- fmap mk_val $ newResiduation scope vtypeType + arg <- fmap mk_val $ newResiduation scope + res <- fmap mk_val $ newResiduation scope unify scope tau (VTable arg res) return (arg,res) -unify scope (VApp f1 vs1) (VApp f2 vs2) - | f1 == f2 = sequence_ (zipWith (unifyThunk scope) vs1 vs2) -unify scope (VSort s1) (VSort s2) - | s1 == s2 = return () -unify scope (VGen i vs1) (VGen j vs2) - | i == j = sequence_ (zipWith (unifyThunk scope) vs1 vs2) -unify scope (VTable p1 res1) (VTable p2 res2) = do - unify scope p1 p2 - unify scope res1 res2 +unify scope (VApp f1 vs1) (VApp f2 vs2) + | f1 == f2 = sequence_ (zipWith (unifyThunk scope) vs1 vs2) unify scope (VMeta i vs1) (VMeta j vs2) | i == j = sequence_ (zipWith (unifyThunk scope) vs1 vs2) | otherwise = do @@ -696,10 +765,22 @@ unify scope (VMeta i vs1) (VMeta j vs2) where m = length scope1 n = length scope2 -unify scope (VInt i) (VInt j) - | i == j = return () unify scope (VMeta i vs) v = unifyVar scope i vs v unify scope v (VMeta i vs) = unifyVar scope i vs v +unify scope (VGen i vs1) (VGen j vs2) + | i == j = sequence_ (zipWith (unifyThunk scope) vs1 vs2) +unify scope (VTable p1 res1) (VTable p2 res2) = do + unify scope p2 p1 + unify scope res1 res2 +unify scope (VSort s1) (VSort s2) + | s1 == s2 = return () +unify scope (VInt i) (VInt j) + | i == j = return () +unify scope (VFlt x) (VFlt y) + | x == y = return () +unify scope (VStr s1) (VStr s2) + | s1 == s2 = return () +unify scope VEmpty VEmpty = return () unify scope v1 v2 = do t1 <- value2term (scopeVars scope) v1 t2 <- value2term (scopeVars scope) v2 @@ -719,15 +800,18 @@ unifyVar scope tnk vs ty2 = do -- Check whether i is bound case mv of Evaluated _ ty1 -> do ty1 <- apply ty1 vs unify scope ty1 ty2 - Residuation i scope' _ -> do let m = length scope' - n = length scope - check m n ty2 - setRef tnk (Evaluated m ty2) + Residuation i scope' _ -> do occursCheck scope' tnk scope ty2 + setRef tnk (Evaluated (length scope') ty2) + +occursCheck scope' tnk scope v = + let m = length scope' + n = length scope + in check m n v where check m n (VApp f vs) = mapM_ (follow m n) vs check m n (VMeta i vs) - | tnk == i = do ty1 <- value2term (scopeVars scope) (VMeta tnk vs) - ty2 <- value2term (scopeVars scope) ty2 + | tnk == i = do ty1 <- value2term (scopeVars scope) (VMeta i vs) + ty2 <- value2term (scopeVars scope) v evalError ("Occurs check for" <+> ppTerm Unqualified 0 ty1 <+> "in:" $$ nest 2 (ppTerm Unqualified 0 ty2)) | otherwise = do @@ -793,7 +877,7 @@ unifyVar scope tnk vs ty2 = do -- Check whether i is bound -- | Instantiate the topmost implicit arguments with metavariables instantiate :: Scope s -> Term -> Sigma s -> EvalM s (Term,Rho s) instantiate scope t (VProd Implicit x ty1 ty2) = do - (i,tnk) <- newResiduation scope ty1 + (i,tnk) <- newResiduation scope ty2 <- case ty2 of VClosure env ty2 -> eval ((x,tnk):env) ty2 [] ty2 -> return ty2 @@ -976,8 +1060,9 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go ty acc) [] sc_tys | m `elem` acc = return acc | otherwise = do res <- getRef m case res of - Evaluated _ v -> go v acc - _ -> foldM follow (m:acc) args + Evaluated _ v -> go v acc + Residuation _ _ Nothing -> foldM follow (m:acc) args + _ -> return acc go (VApp f args) acc = foldM follow acc args go v acc = unimplemented ("go "++showValue v) From 86315bc8c229aeb81038af71b80594e8aa7aef29 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Tue, 5 Dec 2023 13:56:56 +0100 Subject: [PATCH 14/15] remove a premature optimization that caused problems --- src/runtime/c/pgf/phrasetable.cxx | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/runtime/c/pgf/phrasetable.cxx b/src/runtime/c/pgf/phrasetable.cxx index ed0d6db6cb..e4c6dc8667 100644 --- a/src/runtime/c/pgf/phrasetable.cxx +++ b/src/runtime/c/pgf/phrasetable.cxx @@ -474,16 +474,12 @@ PgfPhrasetable phrasetable_delete(PgfPhrasetable table, PgfPhrasetable left = phrasetable_delete(table->left, container, seq_index, seq); - if (left == table->left) - return table; table = Node::upd_node(table,left,table->right); return Node::balanceR(table); } else if (cmp > 0) { PgfPhrasetable right = phrasetable_delete(table->right, container, seq_index, seq); - if (right == table->right) - return table; table = Node::upd_node(table,table->left,right); return Node::balanceL(table); } else { From d0e3c30ea6c2e0cd86cb4b5d8f93fad18bbe4d1c Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Tue, 5 Dec 2023 14:01:11 +0100 Subject: [PATCH 15/15] remove phrasetable_lookup_epsilons which is no longer in use --- src/runtime/c/pgf/phrasetable.cxx | 50 ------------------------------- src/runtime/c/pgf/phrasetable.h | 5 ---- 2 files changed, 55 deletions(-) diff --git a/src/runtime/c/pgf/phrasetable.cxx b/src/runtime/c/pgf/phrasetable.cxx index e4c6dc8667..ade41844ac 100644 --- a/src/runtime/c/pgf/phrasetable.cxx +++ b/src/runtime/c/pgf/phrasetable.cxx @@ -817,56 +817,6 @@ void phrasetable_lookup_cohorts(PgfPhrasetable table, } } -PGF_INTERNAL -void phrasetable_lookup_epsilons(PgfPhrasetable table, - ref lincat, size_t r, - std::function,size_t)> &f) -{ - while (table->left != 0) { - table = table->left; - } - - if (table->value.seq->syms.len > 0) - return; - - size_t len = (table->value.backrefs != 0) - ? table->value.backrefs->len - : 0; - - ssize_t i = 0; - ssize_t j = len-1; - while (i <= j) { - ssize_t k = (i + j) / 2; - ref backref = vector_elem(table->value.backrefs, k); - - int cmp = backref_cmp(backref, lincat, r); - if (cmp < 0) { - j = k-1; - } else if (cmp > 0) { - i = k+1; - } else { - i = k; - while (i > 0) { - ref backref = vector_elem(table->value.backrefs, i-1); - if (backref_cmp(backref, lincat, r) != 0) - break; - f(ref::untagged(backref->container),backref->seq_index); - i--; - } - f(ref::untagged(backref->container),backref->seq_index); - j = k; - while (j < len-1) { - ref backref = vector_elem(table->value.backrefs, j+1); - if (backref_cmp(backref, lincat, r) != 0) - break; - f(ref::untagged(backref->container),backref->seq_index); - j++; - } - break; - } - } -} - PGF_INTERNAL void phrasetable_iter(PgfConcr *concr, PgfPhrasetable table, diff --git a/src/runtime/c/pgf/phrasetable.h b/src/runtime/c/pgf/phrasetable.h index 2d8abc8cda..6d4236df98 100644 --- a/src/runtime/c/pgf/phrasetable.h +++ b/src/runtime/c/pgf/phrasetable.h @@ -105,11 +105,6 @@ void phrasetable_lookup_cohorts(PgfPhrasetable table, bool case_sensitive, PgfPhraseScanner *scanner, PgfExn* err); -PGF_INTERNAL_DECL -void phrasetable_lookup_epsilons(PgfPhrasetable table, - ref lincat, size_t r, - std::function, size_t)> &f); - PGF_INTERNAL_DECL void phrasetable_iter(PgfConcr *concr, PgfPhrasetable table,