forked from GitHub/gf-core
now since the type checking monad TcM is nondeterministic we can use the same monad in PGF.Forest.getAbsTrees
This commit is contained in:
krasimir
@@ -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)
|
||||
|
||||
@@ -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)
|
||||
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user