diff --git a/src/runtime/haskell/PGF/Forest.hs b/src/runtime/haskell/PGF/Forest.hs index a843e7e1d..54204cabb 100644 --- a/src/runtime/haskell/PGF/Forest.hs +++ b/src/runtime/haskell/PGF/Forest.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE TypeSynonymInstances #-} + ------------------------------------------------- -- | -- Module : PGF @@ -29,6 +31,7 @@ import qualified Data.Map as Map import qualified Data.IntSet as IntSet import qualified Data.IntMap as IntMap import Control.Monad +import Control.Monad.State import GF.Data.SortedList data Forest @@ -114,41 +117,39 @@ isLindefCId id -- the same as the startup category. getAbsTrees :: Forest -> PArg -> Maybe Type -> Either [(FId,TcError)] [Expr] getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty = - let (res,err) = unTcFM (do e <- go Set.empty emptyScope arg (fmap (TTyp []) ty) - e <- runTcM abs fid (refineExpr e) - runTcM abs fid (checkResolvedMetaStore emptyScope e) - return e) IntMap.empty + let (err,res) = runTcM abs (do e <- go Set.empty emptyScope (fmap (TTyp []) ty) arg + e <- refineExpr e + checkResolvedMetaStore emptyScope e + return e) fid IntMap.empty in if null res then Left (nub err) - else Right (nubsort (map snd res)) + else Right (nubsort [e | (_,_,e) <- res]) where - go rec_ scope_ (PArg hypos fid) mb_tty_ + go rec_ scope_ mb_tty_ (PArg hypos fid) | fid < totalCats cnc = case mb_tty of - Just tty -> do i <- runTcM abs fid (newMeta scope tty) + Just tty -> do i <- newMeta scope tty return (mkAbs (EMeta i)) Nothing -> mzero | Set.member fid rec_ = mzero | otherwise = foldForest (\funid args trees -> do let CncFun fn lins = cncfuns cnc ! funid case isLindefCId fn of - Just _ -> do arg <- go (Set.insert fid rec_) scope (head args) mb_tty + Just _ -> do arg <- bracket (go (Set.insert fid rec_) scope mb_tty) arg return (mkAbs arg) - Nothing -> do ty_fn <- runTcM abs fid (lookupFunType fn) + Nothing -> do ty_fn <- lookupFunType fn (e,tty0) <- foldM (\(e1,tty) arg -> goArg (Set.insert fid rec_) scope fid e1 arg tty) (EFun fn,TTyp [] ty_fn) args case mb_tty of - Just tty -> runTcM abs fid $ do - i <- newGuardedMeta e - eqType scope (scopeSize scope) i tty tty0 + Just tty -> do i <- newGuardedMeta e + eqType scope (scopeSize scope) i tty tty0 Nothing -> return () return (mkAbs e) `mplus` trees) (\const _ trees -> do - const <- runTcM abs fid $ - case mb_tty of - Just tty -> tcExpr scope const tty - Nothing -> fmap fst $ infExpr scope const + const <- case mb_tty of + Just tty -> tcExpr scope const tty + Nothing -> fmap fst $ infExpr scope const return (mkAbs const) `mplus` trees) @@ -157,13 +158,13 @@ getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty = (scope,mkAbs,mb_tty) = updateScope hypos scope_ id mb_tty_ goArg rec_ scope fid e1 arg (TTyp delta (DTyp ((bt,x,ty):hs) c es)) = do - e2' <- go rec_ scope arg (Just (TTyp delta ty)) + e2' <- bracket (go rec_ scope (Just (TTyp delta ty))) arg let e2 = case bt of Explicit -> e2' Implicit -> EImplArg e2' if x == wildCId then return (EApp e1 e2,TTyp delta (DTyp hs c es)) - else do v2 <- runTcM abs fid (eval (scopeEnv scope) e2') + else do v2 <- eval (scopeEnv scope) e2' return (EApp e1 e2,TTyp (v2:delta) (DTyp hs c es)) updateScope [] scope mkAbs mb_tty = (scope,mkAbs,mb_tty) @@ -181,31 +182,15 @@ getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty = where (x:_) | fid == fidVar = [wildCId] | otherwise = [x | PConst _ (EFun x) _ <- maybe [] Set.toList (IntMap.lookup fid forest)] + + bracket f arg@(PArg _ fid) = do + fid0 <- get + put fid + x <- f arg + put fid0 + return x -newtype TcFM a = TcFM {unTcFM :: MetaStore () -> ([(MetaStore (),a)],[(FId,TcError)])} - -instance Functor TcFM where - fmap f g = TcFM (\ms -> let (res_g,err_g) = unTcFM g ms - in ([(ms,f x) | (ms,x) <- res_g],err_g)) - -instance Monad TcFM where - return x = TcFM (\ms -> ([(ms,x)],[])) - f >>= g = TcFM (\ms -> case unTcFM f ms of - (res,err) -> let (res',err') = unzip [unTcFM (g x) ms | (ms,x) <- res] - in (concat res',concat (err:err'))) - -instance MonadPlus TcFM where - mzero = TcFM (\ms -> ([],[])) - mplus f g = TcFM (\ms -> let (res_f,err_f) = unTcFM f ms - (res_g,err_g) = unTcFM g ms - in (res_f++res_g,err_f++err_g)) - -runTcM :: Abstr -> FId -> TcM () a -> TcFM a -runTcM abstr fid f = TcFM (\ms -> case unTcM f abstr () ms of - Ok _ ms x -> ([(ms,x)],[] ) - Fail err -> ([], [(fid,err)])) - foldForest :: (FunId -> [PArg] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b foldForest f g b fcat forest = case IntMap.lookup fcat forest of @@ -215,3 +200,20 @@ foldForest f g b fcat forest = foldProd (PCoerce fcat) b = foldForest f g b fcat forest foldProd (PApply funid args) b = f funid args b foldProd (PConst _ const toks) b = g const toks b + + +------------------------------------------------------------------------------ +-- Selectors + +instance Selector FId where + splitSelector s = (s,s) + select cat dp = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of + Just (_,fns) -> iter abstr s ms fns + Nothing -> Fail s (UnknownCat cat)) + where + iter abstr s ms [] = Zero + iter abstr s ms ((_,fn):fns) = Plus (select_helper fn abstr s ms) (iter abstr s ms fns) + +select_helper fn = unTcM $ do + ty <- lookupFunType fn + return (EFun fn,ty) diff --git a/src/runtime/haskell/PGF/Generate.hs b/src/runtime/haskell/PGF/Generate.hs index 3e4285617..cbd3d23ab 100644 --- a/src/runtime/haskell/PGF/Generate.hs +++ b/src/runtime/haskell/PGF/Generate.hs @@ -12,12 +12,17 @@ import PGF.Macros import PGF.TypeCheck import PGF.Probabilistic +import Data.Maybe (fromMaybe) import qualified Data.Map as Map import qualified Data.IntMap as IntMap import Control.Monad import Control.Monad.Identity import System.Random + +------------------------------------------------------------------------------ +-- The API + -- | Generates an exhaustive possibly infinite list of -- abstract syntax expressions. generateAll :: PGF -> Type -> [Expr] @@ -66,24 +71,23 @@ generateRandomFromDepth g pgf e dp = generate :: Selector sel => sel -> PGF -> Type -> Maybe Int -> [Expr] generate sel pgf ty dp = - [value2expr (funs (abstract pgf),lookupMeta ms) 0 v | - (ms,v) <- runGenM (abstract pgf) (prove emptyScope (TTyp [] ty) dp) sel emptyMetaStore] + [e | (_,ms,e) <- snd $ runTcM (abstract pgf) (prove emptyScope (TTyp [] ty) dp >>= refineExpr) sel emptyMetaStore] generateForMetas :: Selector sel => sel -> PGF -> Expr -> Maybe Int -> [Expr] generateForMetas sel pgf e dp = case unTcM (infExpr emptyScope e) abs sel emptyMetaStore of Ok sel ms (e,_) -> let gen = do fillinVariables $ \scope tty -> do - v <- prove scope tty dp - return (value2expr (funs abs,lookupMeta ms) 0 v) + prove scope tty dp refineExpr e - in [e | (ms,e) <- runGenM abs gen sel ms] - Fail _ -> [] + in [e | (_,ms,e) <- snd $ runTcM abs gen sel ms] + Fail _ _ -> [] where abs = abstract pgf -prove :: Selector sel => Scope -> TType -> Maybe Int -> TcM sel Value +prove :: Selector sel => Scope -> TType -> Maybe Int -> TcM sel Expr prove scope (TTyp env1 (DTyp [] cat es1)) dp = do - (fn,DTyp hypos _ es2) <- clauses cat + (fe,DTyp hypos _ es2) <- select cat dp + if fe == EFun (mkCId "plus") then mzero else return () case dp of Just 0 | not (null hypos) -> mzero _ -> return () @@ -91,55 +95,34 @@ prove scope (TTyp env1 (DTyp [] cat es1)) dp = do vs1 <- mapM (PGF.TypeCheck.eval env1) es1 vs2 <- mapM (PGF.TypeCheck.eval env2) es2 sequence_ [eqValue mzero suspend (scopeSize scope) v1 v2 | (v1,v2) <- zip vs1 vs2] - vs <- mapM descend args - return (VApp fn vs) + es <- mapM descend args + return (foldl EApp fe es) where suspend i c = do mv <- getMeta i case mv of MBound e -> c e - MUnbound scope tty cs -> do v <- prove scope tty dp - e <- TcM (\abs sel ms -> Ok sel ms (value2expr (funs abs,lookupMeta ms) 0 v)) + MUnbound scope tty cs -> do e <- prove scope tty dp setMeta i (MBound e) sequence_ [c e | c <- (c:cs)] - clauses cat = do - fn <- select cat - if fn == mkCId "plus" then mzero else return () - ty <- lookupFunType fn - return (fn,ty) - mkEnv env [] = return (env,[]) mkEnv env ((bt,x,ty):hypos) = do (env,arg) <- if x /= wildCId then do i <- newMeta scope (TTyp env ty) - let v = VMeta i env [] - return (v : env,Right v) + return (VMeta i env [] : env,Right (EMeta i)) else return (env,Left (TTyp env ty)) (env,args) <- mkEnv env hypos return (env,(bt,arg):args) descend (bt,arg) = do let dp' = fmap (flip (-) 1) dp - v <- case arg of - Right v -> return v + e <- case arg of + Right e -> return e Left tty -> prove scope tty dp' - v <- case bt of - Implicit -> return (VImplArg v) - Explicit -> return v - return v - - ------------------------------------------------------------------------------- --- Generation Monad - - -runGenM :: Abstr -> TcM s a -> s -> MetaStore s -> [(MetaStore s,a)] -runGenM abs f s ms = toList (unTcM f abs s ms) [] - where - toList (Ok s ms x) xs = (ms,x) : xs - toList (Fail _) xs = xs - toList (Zero) xs = xs - toList (Plus b1 b2) xs = toList b1 (toList b2 xs) + e <- case bt of + Implicit -> return (EImplArg e) + Explicit -> return e + return e -- Helper function for random generation. After every @@ -150,3 +133,57 @@ restart g f = in case f g1 of [] -> [] (x:xs) -> x : restart g2 f + + +------------------------------------------------------------------------------ +-- Selectors + +instance Selector () where + splitSelector s = (s,s) + select cat dp + | cat == cidInt = return (ELit (LInt 999), DTyp [] cat []) + | cat == cidFloat = return (ELit (LFlt 3.14), DTyp [] cat []) + | cat == cidString = return (ELit (LStr "Foo"),DTyp [] cat []) + | otherwise = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of + Just (_,fns) -> iter abstr ms fns + Nothing -> Fail s (UnknownCat cat)) + where + iter abstr ms [] = Zero + iter abstr ms ((_,fn):fns) = Plus (select_helper fn abstr () ms) (iter abstr ms fns) + +instance RandomGen g => Selector (Identity g) where + splitSelector (Identity g) = let (g1,g2) = split g + in (Identity g1, Identity g2) + + select cat dp + | cat == cidInt = TcM (\abstr (Identity g) ms -> + let (n,g') = maybe random (\d -> randomR ((-10)*d,10*d)) dp g + in Ok (Identity g) ms (ELit (LInt n),DTyp [] cat [])) + | cat == cidFloat = TcM (\abstr (Identity g) ms -> + let (d,g') = maybe random (\d' -> let d = fromIntegral d' + in randomR ((-pi)*d,pi*d)) dp g + in Ok (Identity g) ms (ELit (LFlt d),DTyp [] cat [])) + | cat == cidString = TcM (\abstr (Identity g) ms -> + let (g1,g2) = split g + s = take (fromMaybe 10 dp) (randomRs ('A','Z') g1) + in Ok (Identity g2) ms (ELit (LStr s),DTyp [] cat [])) + | otherwise = TcM (\abstr (Identity g) ms -> + case Map.lookup cat (cats abstr) of + Just (_,fns) -> do_rand abstr g ms 1.0 fns + Nothing -> Fail (Identity g) (UnknownCat cat)) + where + do_rand abstr g ms p [] = Zero + do_rand abstr g ms p fns = let (d,g') = randomR (0.0,p) g + (g1,g2) = split g' + (p',fn,fns') = hit d fns + in Plus (select_helper fn abstr (Identity g1) ms) (do_rand abstr g2 ms (p-p') fns') + + hit :: Double -> [(Double,a)] -> (Double,a,[(Double,a)]) + hit d (px@(p,x):xs) + | d < p = (p,x,xs) + | otherwise = let (p',x',xs') = hit (d-p) xs + in (p,x',px:xs') + +select_helper fn = unTcM $ do + ty <- lookupFunType fn + return (EFun fn,ty) diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs index d7225dd0b..843326e4c 100644 --- a/src/runtime/haskell/PGF/TypeCheck.hs +++ b/src/runtime/haskell/PGF/TypeCheck.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE FlexibleContexts, RankNTypes #-} +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, RankNTypes #-} ---------------------------------------------------------------------- -- | @@ -20,7 +20,7 @@ module PGF.TypeCheck ( checkType, checkExpr, inferExpr -- internals needed for the typechecking of forests , MetaStore, emptyMetaStore, newMeta, newGuardedMeta, fillinVariables, getMeta, setMeta, MetaValue(..) , Scope, emptyScope, scopeSize, scopeEnv, addScopedVar - , TcM(..), TcResult(..), TType(..), Selector(..), tcError + , TcM(..), TcResult(..), runTcM, TType(..), Selector(..) , tcExpr, infExpr, eqType, eqValue , lookupFunType, eval , refineExpr, checkResolvedMetaStore, lookupMeta @@ -38,8 +38,9 @@ import Data.Maybe as Maybe import Data.List as List import Control.Monad import Control.Monad.Identity +import Control.Monad.State +import Control.Monad.Error import Text.PrettyPrint -import System.Random as Random ----------------------------------------------------- -- The Scope @@ -85,16 +86,20 @@ data MetaValue s newtype TcM s a = TcM {unTcM :: Abstr -> s -> MetaStore s -> TcResult s a} data TcResult s a = Ok s (MetaStore s) a - | Fail TcError + | Fail s TcError | Zero | Plus (TcResult s a) (TcResult s a) +class Selector s where + splitSelector :: s -> (s,s) + select :: CId -> Maybe Int -> TcM s (Expr,Type) + instance Monad (TcM s) where return x = TcM (\abstr s ms -> Ok s ms x) f >>= g = TcM (\abstr s ms -> iter abstr (unTcM f abstr s ms)) where iter abstr (Ok s ms x) = unTcM (g x) abstr s ms - iter abstr (Fail e) = Fail e + iter abstr (Fail s e) = Fail s e iter abstr Zero = Zero iter abstr (Plus b1 b2) = Plus (iter abstr b1) (iter abstr b2) @@ -103,23 +108,44 @@ instance Selector s => MonadPlus (TcM s) where mplus f g = TcM (\abstr s ms -> let (s1,s2) = splitSelector s in Plus (unTcM f abstr s1 ms) (unTcM g abstr s2 ms)) +instance MonadState s (TcM s) where + get = TcM (\abstr s ms -> Ok s ms s) + put s = TcM (\abstr _ ms -> Ok s ms ()) + +instance MonadError TcError (TcM s) where + throwError e = TcM (\abstr s ms -> Fail s e) + catchError f h = TcM (\abstr s ms -> iter abstr ms (unTcM f abstr s ms)) + where + iter abstr _ (Ok s ms x) = Ok s ms x + iter abstr ms (Fail s e) = unTcM (h e) abstr s ms + iter abstr _ Zero = Zero + iter abstr ms (Plus b1 b2) = Plus (iter abstr ms b1) (iter abstr ms b2) + instance Functor (TcM s) where fmap f x = TcM (\abstr s ms -> iter (unTcM x abstr s ms)) where iter (Ok s ms x) = Ok s ms (f x) - iter (Fail e) = Fail e + iter (Fail s e) = Fail s e iter Zero = Zero iter (Plus b1 b2) = Plus (iter b1) (iter b2) +runTcM :: Abstr -> TcM s a -> s -> MetaStore s -> ([(s,TcError)],[(s,MetaStore s,a)]) +runTcM abs f s ms = collect (unTcM f abs s ms) ([],[]) + where + collect (Ok _ ms x) (es,xs) = (es,(s,ms,x) : xs) + collect (Fail s e) (es,xs) = ((s,e) : es,xs) + collect (Zero) exs = exs + collect (Plus b1 b2) exs = collect b1 (collect b2 exs) + lookupCatHyps :: CId -> TcM s [Hypo] lookupCatHyps cat = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of Just (hyps,_) -> Ok s ms hyps - Nothing -> Fail (UnknownCat cat)) + Nothing -> Fail s (UnknownCat cat)) lookupFunType :: CId -> TcM s Type lookupFunType fun = TcM (\abstr s ms -> case Map.lookup fun (funs abstr) of Just (ty,_,_,_) -> Ok s ms ty - Nothing -> Fail (UnknownFun fun)) + Nothing -> Fail s (UnknownFun fun)) emptyMetaStore :: MetaStore s emptyMetaStore = IntMap.empty @@ -157,9 +183,6 @@ fillinVariables f = do sequence_ [c e | c <- cs] fillinVariables f -tcError :: TcError -> TcM s a -tcError e = TcM (\abstr s ms -> Fail e) - addConstraint :: MetaId -> MetaId -> (Expr -> TcM s ()) -> TcM s () addConstraint i j c = do mv <- getMeta j @@ -221,43 +244,6 @@ ppTcError (UnexpectedImplArg xs e) = braces (ppExpr 0 xs e) <+> text "is imp ppTcError (UnsolvableGoal xs metaid ty)= text "The goal:" <+> ppMeta metaid <+> colon <+> ppType 0 xs ty $$ text "cannot be solved" ------------------------------------------------------------------------------- --- Selectors - -class Selector s where - splitSelector :: s -> (s,s) - select :: CId -> TcM s CId - -instance Selector () where - splitSelector s = (s,s) - select cat = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of - Just (_,fns) -> iter ms fns - Nothing -> Fail (UnknownCat cat)) - where - iter ms [] = Zero - iter ms ((_,fn):fns) = Plus (Ok () ms fn) (iter ms fns) - -instance RandomGen g => Selector (Identity g) where - splitSelector (Identity g) = let (g1,g2) = Random.split g - in (Identity g1, Identity g2) - - select cat = TcM (\abstr (Identity g) ms -> - case Map.lookup cat (cats abstr) of - Just (_,fns) -> do_rand g ms 1.0 fns - Nothing -> Fail (UnknownCat cat)) - where - do_rand g ms p [] = Zero - do_rand g ms p fns = let (d,g') = randomR (0.0,p) g - (g1,g2) = Random.split g' - (p',fn,fns') = hit d fns - in Plus (Ok (Identity g1) ms fn) (do_rand g2 ms (p-p') fns') - - hit :: Double -> [(Double,a)] -> (Double,a,[(Double,a)]) - hit d (px@(p,x):xs) - | d < p = (p,x,xs) - | otherwise = let (p',x',xs') = hit (d-p) xs - in (p,x',px:xs') - ----------------------------------------------------- -- checkType ----------------------------------------------------- @@ -268,7 +254,7 @@ checkType :: PGF -> Type -> Either TcError Type checkType pgf ty = case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) () emptyMetaStore of Ok s ms ty -> Right ty - Fail err -> Left err + Fail _ err -> Left err tcType :: Scope -> Type -> TcM s Type tcType scope ty@(DTyp hyps cat es) = do @@ -294,7 +280,7 @@ tcHypo scope (b,x,ty) = do else return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,(b,x,ty)) tcCatArgs scope [] delta [] ty0 n m = return (delta,[]) -tcCatArgs scope (EImplArg e:es) delta ((Explicit,x,ty):hs) ty0 n m = tcError (UnexpectedImplArg (scopeVars scope) e) +tcCatArgs scope (EImplArg e:es) delta ((Explicit,x,ty):hs) ty0 n m = throwError (UnexpectedImplArg (scopeVars scope) e) tcCatArgs scope (EImplArg e:es) delta ((Implicit,x,ty):hs) ty0 n m = do e <- tcExpr scope e (TTyp delta ty) (delta,es) <- if x == wildCId @@ -316,7 +302,7 @@ tcCatArgs scope (e:es) delta ((Explicit,x,ty):hs) ty0 n m = do tcCatArgs scope es (v:delta) hs ty0 n m return (delta,e:es) tcCatArgs scope _ delta _ ty0@(DTyp _ cat _) n m = do - tcError (WrongCatArgs (scopeVars scope) ty0 cat n m) + throwError (WrongCatArgs (scopeVars scope) ty0 cat n m) ----------------------------------------------------- -- checkExpr @@ -329,8 +315,8 @@ checkExpr pgf e ty = e <- refineExpr e checkResolvedMetaStore emptyScope e return e) (abstract pgf) () emptyMetaStore of - Ok _ ms e -> Right e - Fail err -> Left err + Ok _ ms e -> Right e + Fail _ err -> Left err tcExpr :: Scope -> Expr -> TType -> TcM s Expr tcExpr scope e0@(EAbs Implicit x e) tty = @@ -342,7 +328,7 @@ tcExpr scope e0@(EAbs Implicit x e) tty = e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es)) return (EAbs Implicit x e) _ -> do ty <- evalType (scopeSize scope) tty - tcError (NotFunType (scopeVars scope) e0 ty) + throwError (NotFunType (scopeVars scope) e0 ty) tcExpr scope e0 (TTyp delta (DTyp ((Implicit,y,ty):hs) c es)) = do e0 <- if y == wildCId then tcExpr (addScopedVar wildCId (TTyp delta ty) scope) @@ -359,7 +345,7 @@ tcExpr scope e0@(EAbs Explicit x e) tty = e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es)) return (EAbs Explicit x e) _ -> do ty <- evalType (scopeSize scope) tty - tcError (NotFunType (scopeVars scope) e0 ty) + throwError (NotFunType (scopeVars scope) e0 ty) tcExpr scope (EMeta _) tty = do i <- newMeta scope tty return (EMeta i) @@ -386,7 +372,7 @@ inferExpr pgf e = ty <- evalType 0 tty return (e,ty)) (abstract pgf) () emptyMetaStore of Ok _ ms (e,ty) -> Right (e,ty) - Fail err -> Left err + Fail _ err -> Left err infExpr :: Scope -> Expr -> TcM s (Expr,TType) infExpr scope e0@(EApp e1 e2) = do @@ -413,12 +399,12 @@ infExpr scope (ETyped e ty) = do infExpr scope (EImplArg e) = do (e,tty) <- infExpr scope e return (EImplArg e,tty) -infExpr scope e = tcError (CannotInferType (scopeVars scope) e) +infExpr scope e = throwError (CannotInferType (scopeVars scope) e) tcArg scope e1 e2 delta ty0@(DTyp [] c es) = do ty1 <- evalType (scopeSize scope) (TTyp delta ty0) - tcError (NotFunType (scopeVars scope) e1 ty1) -tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = tcError (UnexpectedImplArg (scopeVars scope) e2) + throwError (NotFunType (scopeVars scope) e1 ty1) +tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = throwError (UnexpectedImplArg (scopeVars scope) e2) tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do e2 <- tcExpr scope e2 (TTyp delta ty) if x == wildCId @@ -450,7 +436,7 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 raiseTypeMatchError = do ty1 <- evalType k tty1 ty2 <- evalType k tty2 e <- refineExpr (EMeta i0) - tcError (TypeMismatch (scopeVars scope) e ty1 ty2) + throwError (TypeMismatch (scopeVars scope) e ty1 ty2) eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int,Env,Env) eqHyps k delta1 [] delta2 [] = @@ -558,7 +544,7 @@ checkResolvedMetaStore scope e = TcM (\abstr s ms -> let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)] in if List.null xs then Ok s ms () - else Fail (UnresolvedMetaVars (scopeVars scope) e xs)) + else Fail s (UnresolvedMetaVars (scopeVars scope) e xs)) where isResolved (MUnbound _ _ []) = True isResolved (MGuarded _ _ _) = True