{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, RankNTypes #-}
module PGF.TypeCheck ( checkType, checkExpr, inferExpr
, ppTcError, TcError(..)
, MetaStore, emptyMetaStore, newMeta, newGuardedMeta
, getMeta, setMeta, lookupMeta, MetaValue(..)
, Scope, emptyScope, scopeSize, scopeEnv, addScopedVar
, TcM(..), runTcM, TType(..), Selector(..)
, tcExpr, infExpr, eqType, eqValue
, lookupFunType, typeGenerators, eval
, generateForMetas, generateForForest, checkResolvedMetaStore
) where
import PGF.Data
import PGF.Expr hiding (eval, apply, applyValue, value2expr)
import qualified PGF.Expr as Expr
import PGF.Macros (cidInt, cidFloat, cidString)
import PGF.CId
import Data.Map as Map
import Data.IntMap as IntMap
import Data.Maybe as Maybe
import Data.List as List
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Control.Monad.Except
import Text.PrettyPrint
data TType = TTyp Env Type
newtype Scope = Scope [(CId,TType)]
emptyScope :: Scope
emptyScope = [(CId, TType)] -> Scope
Scope []
addScopedVar :: CId -> TType -> Scope -> Scope
addScopedVar :: CId -> TType -> Scope -> Scope
addScopedVar CId
x TType
tty (Scope [(CId, TType)]
gamma) = [(CId, TType)] -> Scope
Scope ((CId
x,TType
tty)(CId, TType) -> [(CId, TType)] -> [(CId, TType)]
forall a. a -> [a] -> [a]
:[(CId, TType)]
gamma)
lookupVar :: CId -> Scope -> Maybe (Int,TType)
lookupVar :: CId -> Scope -> Maybe (Int, TType)
lookupVar CId
x (Scope [(CId, TType)]
gamma) = [(Int, TType)] -> Maybe (Int, TType)
forall a. [a] -> Maybe a
listToMaybe [(Int
i,TType
tty) | ((CId
y,TType
tty),Int
i) <- [(CId, TType)] -> [Int] -> [((CId, TType), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(CId, TType)]
gamma [Int
0..], CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
y]
getVar :: Int -> Scope -> (CId,TType)
getVar :: Int -> Scope -> (CId, TType)
getVar Int
i (Scope [(CId, TType)]
gamma) = [(CId, TType)]
gamma [(CId, TType)] -> Int -> (CId, TType)
forall a. [a] -> Int -> a
!! Int
i
scopeEnv :: Scope -> Env
scopeEnv :: Scope -> Env
scopeEnv (Scope [(CId, TType)]
gamma) = let n :: Int
n = [(CId, TType)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(CId, TType)]
gamma
in [Int -> Env -> Value
VGen (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [] | Int
i <- [Int
0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]
scopeVars :: Scope -> [CId]
scopeVars :: Scope -> [CId]
scopeVars (Scope [(CId, TType)]
gamma) = ((CId, TType) -> CId) -> [(CId, TType)] -> [CId]
forall a b. (a -> b) -> [a] -> [b]
List.map (CId, TType) -> CId
forall a b. (a, b) -> a
fst [(CId, TType)]
gamma
scopeSize :: Scope -> Int
scopeSize :: Scope -> Int
scopeSize (Scope [(CId, TType)]
gamma) = [(CId, TType)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(CId, TType)]
gamma
type MetaStore s = IntMap (MetaValue s)
data MetaValue s
= MUnbound s Scope TType [Expr -> TcM s ()]
| MBound Expr
| MGuarded Expr [Expr -> TcM s ()] {-# UNPACK #-} !Int
newtype TcM s a = TcM {TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM :: forall b . Abstr -> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> (MetaStore s -> s -> b -> b)}
class Selector s where
splitSelector :: s -> (s,s)
select :: CId -> Scope -> Maybe Int -> TcM s (Expr,TType)
instance Applicative (TcM s) where
pure :: a -> TcM s a
pure = a -> TcM s a
forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: TcM s (a -> b) -> TcM s a -> TcM s b
(<*>) = TcM s (a -> b) -> TcM s a -> TcM s b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad (TcM s) where
return :: a -> TcM s a
return a
x = (forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr a -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h -> a -> MetaStore s -> s -> b -> b
k a
x)
TcM s a
f >>= :: TcM s a -> (a -> TcM s b) -> TcM s b
>>= a -> TcM s b
g = (forall b.
Abstr
-> (b -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s b
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr b -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h -> TcM s a
-> Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM TcM s a
f Abstr
abstr (\a
x -> TcM s b
-> Abstr
-> (b -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM (a -> TcM s b
g a
x) Abstr
abstr b -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h) TcError -> s -> b -> b
h)
instance Selector s => Alternative (TcM s) where
empty :: TcM s a
empty = TcM s a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
<|> :: TcM s a -> TcM s a -> TcM s a
(<|>) = TcM s a -> TcM s a -> TcM s a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
instance Selector s => MonadPlus (TcM s) where
mzero :: TcM s a
mzero = (forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr a -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms s
s -> b -> b
forall a. a -> a
id)
mplus :: TcM s a -> TcM s a -> TcM s a
mplus TcM s a
f TcM s a
g = (forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr a -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms s
s -> let (s
s1,s
s2) = s -> (s, s)
forall s. Selector s => s -> (s, s)
splitSelector s
s
in TcM s a
-> Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM TcM s a
f Abstr
abstr a -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms s
s1 (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcM s a
-> Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM TcM s a
g Abstr
abstr a -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms s
s2)
instance MonadState s (TcM s) where
get :: TcM s s
get = (forall b.
Abstr
-> (s -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s s
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr s -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms s
s -> s -> MetaStore s -> s -> b -> b
k s
s MetaStore s
ms s
s)
put :: s -> TcM s ()
put s
s = (forall b.
Abstr
-> (() -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s ()
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr () -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms s
_ -> () -> MetaStore s -> s -> b -> b
k () MetaStore s
ms s
s)
instance MonadError TcError (TcM s) where
throwError :: TcError -> TcM s a
throwError TcError
e = (forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr a -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> TcError -> s -> b -> b
h TcError
e)
catchError :: TcM s a -> (TcError -> TcM s a) -> TcM s a
catchError TcM s a
f TcError -> TcM s a
fh = (forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr a -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> TcM s a
-> Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM TcM s a
f Abstr
abstr a -> MetaStore s -> s -> b -> b
k (\TcError
e s
s -> TcM s a
-> Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM (TcError -> TcM s a
fh TcError
e) Abstr
abstr a -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms s
s) MetaStore s
ms)
instance Functor (TcM s) where
fmap :: (a -> b) -> TcM s a -> TcM s b
fmap a -> b
f TcM s a
m = (forall b.
Abstr
-> (b -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s b
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr b -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h -> TcM s a
-> Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM TcM s a
m Abstr
abstr (b -> MetaStore s -> s -> b -> b
k (b -> MetaStore s -> s -> b -> b)
-> (a -> b) -> a -> MetaStore s -> s -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) TcError -> s -> b -> b
h)
runTcM :: Abstr -> TcM s a -> MetaStore s -> s -> ([(s,TcError)],[(MetaStore s,s,a)])
runTcM :: Abstr
-> TcM s a
-> MetaStore s
-> s
-> ([(s, TcError)], [(MetaStore s, s, a)])
runTcM Abstr
abstr TcM s a
f MetaStore s
ms s
s = TcM s a
-> Abstr
-> (a
-> MetaStore s
-> s
-> (([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)]))
-> ([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)]))
-> (TcError
-> s
-> (([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)]))
-> ([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)]))
-> MetaStore s
-> s
-> (([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)]))
-> ([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)])
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM TcM s a
f Abstr
abstr (\a
x MetaStore s
ms s
s ([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)])
cp ([(s, TcError)], [(MetaStore s, s, a)])
b -> let ([(s, TcError)]
es,[(MetaStore s, s, a)]
xs) = ([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)])
cp ([(s, TcError)], [(MetaStore s, s, a)])
b
in ([(s, TcError)]
es,(MetaStore s
ms,s
s,a
x) (MetaStore s, s, a)
-> [(MetaStore s, s, a)] -> [(MetaStore s, s, a)]
forall a. a -> [a] -> [a]
: [(MetaStore s, s, a)]
xs))
(\TcError
e s
s ([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)])
cp ([(s, TcError)], [(MetaStore s, s, a)])
b -> let ([(s, TcError)]
es,[(MetaStore s, s, a)]
xs) = ([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)])
cp ([(s, TcError)], [(MetaStore s, s, a)])
b
in ((s
s,TcError
e) (s, TcError) -> [(s, TcError)] -> [(s, TcError)]
forall a. a -> [a] -> [a]
: [(s, TcError)]
es,[(MetaStore s, s, a)]
xs))
MetaStore s
ms s
s ([(s, TcError)], [(MetaStore s, s, a)])
-> ([(s, TcError)], [(MetaStore s, s, a)])
forall a. a -> a
id ([],[])
lookupCatHyps :: CId -> TcM s [Hypo]
lookupCatHyps :: CId -> TcM s [Hypo]
lookupCatHyps CId
cat = (forall b.
Abstr
-> ([Hypo] -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s [Hypo]
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr [Hypo] -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> case CId
-> Map CId ([Hypo], [(Double, CId)], Double)
-> Maybe ([Hypo], [(Double, CId)], Double)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CId
cat (Abstr -> Map CId ([Hypo], [(Double, CId)], Double)
cats Abstr
abstr) of
Just ([Hypo]
hyps,[(Double, CId)]
_,Double
_) -> [Hypo] -> MetaStore s -> s -> b -> b
k [Hypo]
hyps MetaStore s
ms
Maybe ([Hypo], [(Double, CId)], Double)
Nothing -> TcError -> s -> b -> b
h (CId -> TcError
UnknownCat CId
cat))
lookupFunType :: CId -> TcM s Type
lookupFunType :: CId -> TcM s Type
lookupFunType CId
fun = (forall b.
Abstr
-> (Type -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s Type
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr Type -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> case CId
-> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
-> Maybe (Type, Int, Maybe ([Equation], [[Instr]]), Double)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CId
fun (Abstr -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
funs Abstr
abstr) of
Just (Type
ty,Int
_,Maybe ([Equation], [[Instr]])
_,Double
_) -> Type -> MetaStore s -> s -> b -> b
k Type
ty MetaStore s
ms
Maybe (Type, Int, Maybe ([Equation], [[Instr]]), Double)
Nothing -> TcError -> s -> b -> b
h (CId -> TcError
UnknownFun CId
fun))
typeGenerators :: Scope -> CId -> TcM s [(Double,Expr,TType)]
typeGenerators :: Scope -> CId -> TcM s [(Double, Expr, TType)]
typeGenerators Scope
scope CId
cat = ([(Double, Expr, TType)] -> [(Double, Expr, TType)])
-> TcM s [(Double, Expr, TType)] -> TcM s [(Double, Expr, TType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Double, Expr, TType)] -> [(Double, Expr, TType)]
forall a b c. Fractional a => [(a, b, c)] -> [(a, b, c)]
normalize (([(Double, Expr, TType)]
-> [(Double, Expr, TType)] -> [(Double, Expr, TType)])
-> TcM s [(Double, Expr, TType)]
-> TcM s [(Double, Expr, TType)]
-> TcM s [(Double, Expr, TType)]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 [(Double, Expr, TType)]
-> [(Double, Expr, TType)] -> [(Double, Expr, TType)]
forall a. [a] -> [a] -> [a]
(++) TcM s [(Double, Expr, TType)]
x TcM s [(Double, Expr, TType)]
forall s. TcM s [(Double, Expr, TType)]
y)
where
x :: TcM s [(Double, Expr, TType)]
x = [(Double, Expr, TType)] -> TcM s [(Double, Expr, TType)]
forall (m :: * -> *) a. Monad m => a -> m a
return
[(Double
0.25,Int -> Expr
EVar Int
i,TType
tty) | (Int
i,(CId
_,tty :: TType
tty@(TTyp Env
_ (DTyp [Hypo]
_ CId
cat' [Expr]
_)))) <- [Int] -> [(CId, TType)] -> [(Int, (CId, TType))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [(CId, TType)]
gamma
, CId
cat CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
cat']
where
Scope [(CId, TType)]
gamma = Scope
scope
y :: TcM s [(Double, Expr, TType)]
y | CId
cat CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
cidInt = [(Double, Expr, TType)] -> TcM s [(Double, Expr, TType)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Double
1.0,Literal -> Expr
ELit (Int -> Literal
LInt Int
999), Env -> Type -> TType
TTyp [] ([Hypo] -> CId -> [Expr] -> Type
DTyp [] CId
cat []))]
| CId
cat CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
cidFloat = [(Double, Expr, TType)] -> TcM s [(Double, Expr, TType)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Double
1.0,Literal -> Expr
ELit (Double -> Literal
LFlt Double
3.14), Env -> Type -> TType
TTyp [] ([Hypo] -> CId -> [Expr] -> Type
DTyp [] CId
cat []))]
| CId
cat CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
cidString = [(Double, Expr, TType)] -> TcM s [(Double, Expr, TType)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Double
1.0,Literal -> Expr
ELit (String -> Literal
LStr String
"Foo"),Env -> Type -> TType
TTyp [] ([Hypo] -> CId -> [Expr] -> Type
DTyp [] CId
cat []))]
| Bool
otherwise = (forall b.
Abstr
-> ([(Double, Expr, TType)] -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s [(Double, Expr, TType)]
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr [(Double, Expr, TType)] -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms ->
case CId
-> Map CId ([Hypo], [(Double, CId)], Double)
-> Maybe ([Hypo], [(Double, CId)], Double)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CId
cat (Abstr -> Map CId ([Hypo], [(Double, CId)], Double)
cats Abstr
abstr) of
Just ([Hypo]
_,[(Double, CId)]
fns,Double
_) -> TcM s [(Double, Expr, TType)]
-> Abstr
-> ([(Double, Expr, TType)] -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM (((Double, CId) -> TcM s (Double, Expr, TType))
-> [(Double, CId)] -> TcM s [(Double, Expr, TType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Double, CId) -> TcM s (Double, Expr, TType)
forall a s. (a, CId) -> TcM s (a, Expr, TType)
helper [(Double, CId)]
fns) Abstr
abstr [(Double, Expr, TType)] -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms
Maybe ([Hypo], [(Double, CId)], Double)
Nothing -> TcError -> s -> b -> b
h (CId -> TcError
UnknownCat CId
cat))
helper :: (a, CId) -> TcM s (a, Expr, TType)
helper (a
p,CId
fn) = do
Type
ty <- CId -> TcM s Type
forall s. CId -> TcM s Type
lookupFunType CId
fn
(a, Expr, TType) -> TcM s (a, Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
p,CId -> Expr
EFun CId
fn,Env -> Type -> TType
TTyp [] Type
ty)
normalize :: [(a, b, c)] -> [(a, b, c)]
normalize [(a, b, c)]
gens = [(a
pa -> a -> a
forall a. Fractional a => a -> a -> a
/a
s,b
e,c
tty) | (a
p,b
e,c
tty) <- [(a, b, c)]
gens]
where
s :: a
s = [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [a
p | (a
p,b
_,c
_) <- [(a, b, c)]
gens]
emptyMetaStore :: MetaStore s
emptyMetaStore :: MetaStore s
emptyMetaStore = MetaStore s
forall a. IntMap a
IntMap.empty
newMeta :: Scope -> TType -> TcM s MetaId
newMeta :: Scope -> TType -> TcM s Int
newMeta Scope
scope TType
tty = (forall b.
Abstr
-> (Int -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s Int
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr Int -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms s
s -> let metaid :: Int
metaid = MetaStore s -> Int
forall a. IntMap a -> Int
IntMap.size MetaStore s
ms Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
in Int -> MetaStore s -> s -> b -> b
k Int
metaid (Int -> MetaValue s -> MetaStore s -> MetaStore s
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
metaid (s -> Scope -> TType -> [Expr -> TcM s ()] -> MetaValue s
forall s. s -> Scope -> TType -> [Expr -> TcM s ()] -> MetaValue s
MUnbound s
s Scope
scope TType
tty []) MetaStore s
ms) s
s)
newGuardedMeta :: Expr -> TcM s MetaId
newGuardedMeta :: Expr -> TcM s Int
newGuardedMeta Expr
e = (forall b.
Abstr
-> (Int -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s Int
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr Int -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms s
s -> let metaid :: Int
metaid = MetaStore s -> Int
forall a. IntMap a -> Int
IntMap.size MetaStore s
ms Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
in Int -> MetaStore s -> s -> b -> b
k Int
metaid (Int -> MetaValue s -> MetaStore s -> MetaStore s
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
metaid (Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
forall s. Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
MGuarded Expr
e [] Int
0) MetaStore s
ms) s
s)
getMeta :: MetaId -> TcM s (MetaValue s)
getMeta :: Int -> TcM s (MetaValue s)
getMeta Int
i = (forall b.
Abstr
-> (MetaValue s -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s (MetaValue s)
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr MetaValue s -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> case Int -> MetaStore s -> Maybe (MetaValue s)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i MetaStore s
ms of
Just MetaValue s
mv -> MetaValue s -> MetaStore s -> s -> b -> b
k MetaValue s
mv MetaStore s
ms)
setMeta :: MetaId -> MetaValue s -> TcM s ()
setMeta :: Int -> MetaValue s -> TcM s ()
setMeta Int
i MetaValue s
mv = (forall b.
Abstr
-> (() -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s ()
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr () -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> () -> MetaStore s -> s -> b -> b
k () (Int -> MetaValue s -> MetaStore s -> MetaStore s
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i MetaValue s
mv MetaStore s
ms))
lookupMeta :: IntMap (MetaValue s) -> Int -> Maybe Expr
lookupMeta IntMap (MetaValue s)
ms Int
i =
case Int -> IntMap (MetaValue s) -> Maybe (MetaValue s)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap (MetaValue s)
ms of
Just (MBound Expr
t) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
t
Just (MGuarded Expr
t [Expr -> TcM s ()]
_ Int
x) | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
t
| Bool
otherwise -> Maybe Expr
forall a. Maybe a
Nothing
Just (MUnbound s
_ Scope
_ TType
_ [Expr -> TcM s ()]
_) -> Maybe Expr
forall a. Maybe a
Nothing
Maybe (MetaValue s)
Nothing -> Maybe Expr
forall a. Maybe a
Nothing
addConstraint :: MetaId -> MetaId -> (Expr -> TcM s ()) -> TcM s ()
addConstraint :: Int -> Int -> (Expr -> TcM s ()) -> TcM s ()
addConstraint Int
i Int
j Expr -> TcM s ()
c = do
MetaValue s
mv <- Int -> TcM s (MetaValue s)
forall s. Int -> TcM s (MetaValue s)
getMeta Int
j
case MetaValue s
mv of
MUnbound s
s Scope
scope TType
tty [Expr -> TcM s ()]
cs -> TcM s ()
forall s. TcM s ()
addRef TcM s () -> TcM s () -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> MetaValue s -> TcM s ()
forall s. Int -> MetaValue s -> TcM s ()
setMeta Int
j (s -> Scope -> TType -> [Expr -> TcM s ()] -> MetaValue s
forall s. s -> Scope -> TType -> [Expr -> TcM s ()] -> MetaValue s
MUnbound s
s Scope
scope TType
tty ((\Expr
e -> TcM s ()
forall s. TcM s ()
release TcM s () -> TcM s () -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> TcM s ()
c Expr
e) (Expr -> TcM s ()) -> [Expr -> TcM s ()] -> [Expr -> TcM s ()]
forall a. a -> [a] -> [a]
: [Expr -> TcM s ()]
cs))
MBound Expr
e -> Expr -> TcM s ()
c Expr
e
MGuarded Expr
e [Expr -> TcM s ()]
cs Int
x | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 -> Expr -> TcM s ()
c Expr
e
| Bool
otherwise -> TcM s ()
forall s. TcM s ()
addRef TcM s () -> TcM s () -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> MetaValue s -> TcM s ()
forall s. Int -> MetaValue s -> TcM s ()
setMeta Int
j (Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
forall s. Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
MGuarded Expr
e ((\Expr
e -> TcM s ()
forall s. TcM s ()
release TcM s () -> TcM s () -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> TcM s ()
c Expr
e) (Expr -> TcM s ()) -> [Expr -> TcM s ()] -> [Expr -> TcM s ()]
forall a. a -> [a] -> [a]
: [Expr -> TcM s ()]
cs) Int
x)
where
addRef :: TcM s ()
addRef = (forall b.
Abstr
-> (() -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s ()
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr () -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> case Int -> MetaStore s -> Maybe (MetaValue s)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i MetaStore s
ms of
Just (MGuarded Expr
e [Expr -> TcM s ()]
cs Int
x) -> () -> MetaStore s -> s -> b -> b
k () (MetaStore s -> s -> b -> b) -> MetaStore s -> s -> b -> b
forall a b. (a -> b) -> a -> b
$! Int -> MetaValue s -> MetaStore s -> MetaStore s
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
forall s. Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
MGuarded Expr
e [Expr -> TcM s ()]
cs (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)) MetaStore s
ms)
release :: TcM s ()
release = (forall b.
Abstr
-> (() -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s ()
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr () -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> case Int -> MetaStore s -> Maybe (MetaValue s)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i MetaStore s
ms of
Just (MGuarded Expr
e [Expr -> TcM s ()]
cs Int
x) -> if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
then TcM s ()
-> Abstr
-> (() -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM ([TcM s ()] -> TcM s ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [Expr -> TcM s ()
c Expr
e | Expr -> TcM s ()
c <- [Expr -> TcM s ()]
cs]) Abstr
abstr () -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h (MetaStore s -> s -> b -> b) -> MetaStore s -> s -> b -> b
forall a b. (a -> b) -> a -> b
$! Int -> MetaValue s -> MetaStore s -> MetaStore s
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
forall s. Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
MGuarded Expr
e [] Int
0) MetaStore s
ms
else () -> MetaStore s -> s -> b -> b
k () (MetaStore s -> s -> b -> b) -> MetaStore s -> s -> b -> b
forall a b. (a -> b) -> a -> b
$! Int -> MetaValue s -> MetaStore s -> MetaStore s
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
forall s. Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
MGuarded Expr
e [Expr -> TcM s ()]
cs (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) MetaStore s
ms)
data TcError
= UnknownCat CId
| UnknownFun CId
| WrongCatArgs [CId] Type CId Int Int
| TypeMismatch [CId] Expr Type Type
| NotFunType [CId] Expr Type
| CannotInferType [CId] Expr
| UnresolvedMetaVars [CId] Expr [MetaId]
| UnexpectedImplArg [CId] Expr
| UnsolvableGoal [CId] MetaId Type
deriving TcError -> TcError -> Bool
(TcError -> TcError -> Bool)
-> (TcError -> TcError -> Bool) -> Eq TcError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TcError -> TcError -> Bool
$c/= :: TcError -> TcError -> Bool
== :: TcError -> TcError -> Bool
$c== :: TcError -> TcError -> Bool
Eq
ppTcError :: TcError -> Doc
ppTcError :: TcError -> Doc
ppTcError (UnknownCat CId
cat) = String -> Doc
text String
"Category" Doc -> Doc -> Doc
<+> CId -> Doc
ppCId CId
cat Doc -> Doc -> Doc
<+> String -> Doc
text String
"is not in scope"
ppTcError (UnknownFun CId
fun) = String -> Doc
text String
"Function" Doc -> Doc -> Doc
<+> CId -> Doc
ppCId CId
fun Doc -> Doc -> Doc
<+> String -> Doc
text String
"is not in scope"
ppTcError (WrongCatArgs [CId]
xs Type
ty CId
cat Int
m Int
n) = String -> Doc
text String
"Category" Doc -> Doc -> Doc
<+> CId -> Doc
ppCId CId
cat Doc -> Doc -> Doc
<+> String -> Doc
text String
"should have" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
m Doc -> Doc -> Doc
<+> String -> Doc
text String
"argument(s), but has been given" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
n Doc -> Doc -> Doc
$$
String -> Doc
text String
"In the type:" Doc -> Doc -> Doc
<+> Int -> [CId] -> Type -> Doc
ppType Int
0 [CId]
xs Type
ty
ppTcError (TypeMismatch [CId]
xs Expr
e Type
ty1 Type
ty2) = String -> Doc
text String
"Couldn't match expected type" Doc -> Doc -> Doc
<+> Int -> [CId] -> Type -> Doc
ppType Int
0 [CId]
xs Type
ty1 Doc -> Doc -> Doc
$$
String -> Doc
text String
" against inferred type" Doc -> Doc -> Doc
<+> Int -> [CId] -> Type -> Doc
ppType Int
0 [CId]
xs Type
ty2 Doc -> Doc -> Doc
$$
String -> Doc
text String
"In the expression:" Doc -> Doc -> Doc
<+> Int -> [CId] -> Expr -> Doc
ppExpr Int
0 [CId]
xs Expr
e
ppTcError (NotFunType [CId]
xs Expr
e Type
ty) = String -> Doc
text String
"A function type is expected for the expression" Doc -> Doc -> Doc
<+> Int -> [CId] -> Expr -> Doc
ppExpr Int
0 [CId]
xs Expr
e Doc -> Doc -> Doc
<+> String -> Doc
text String
"instead of type" Doc -> Doc -> Doc
<+> Int -> [CId] -> Type -> Doc
ppType Int
0 [CId]
xs Type
ty
ppTcError (CannotInferType [CId]
xs Expr
e) = String -> Doc
text String
"Cannot infer the type of expression" Doc -> Doc -> Doc
<+> Int -> [CId] -> Expr -> Doc
ppExpr Int
0 [CId]
xs Expr
e
ppTcError (UnresolvedMetaVars [CId]
xs Expr
e [Int]
ms) = String -> Doc
text String
"Meta variable(s)" Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Int -> Doc) -> [Int] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
List.map Int -> Doc
ppMeta [Int]
ms) Doc -> Doc -> Doc
<+> String -> Doc
text String
"should be resolved" Doc -> Doc -> Doc
$$
String -> Doc
text String
"in the expression:" Doc -> Doc -> Doc
<+> Int -> [CId] -> Expr -> Doc
ppExpr Int
0 [CId]
xs Expr
e
ppTcError (UnexpectedImplArg [CId]
xs Expr
e) = Doc -> Doc
braces (Int -> [CId] -> Expr -> Doc
ppExpr Int
0 [CId]
xs Expr
e) Doc -> Doc -> Doc
<+> String -> Doc
text String
"is implicit argument but not implicit argument is expected here"
ppTcError (UnsolvableGoal [CId]
xs Int
metaid Type
ty)= String -> Doc
text String
"The goal:" Doc -> Doc -> Doc
<+> Int -> Doc
ppMeta Int
metaid Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Int -> [CId] -> Type -> Doc
ppType Int
0 [CId]
xs Type
ty Doc -> Doc -> Doc
$$
String -> Doc
text String
"cannot be solved"
checkType :: PGF -> Type -> Either TcError Type
checkType :: PGF -> Type -> Either TcError Type
checkType PGF
pgf Type
ty =
TcM () Type
-> Abstr
-> (Type
-> MetaStore ()
-> ()
-> Either TcError Type
-> Either TcError Type)
-> (TcError -> () -> Either TcError Type -> Either TcError Type)
-> MetaStore ()
-> ()
-> Either TcError Type
-> Either TcError Type
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM (do Type
ty <- Scope -> Type -> TcM () Type
forall s. Scope -> Type -> TcM s Type
tcType Scope
emptyScope Type
ty
Type -> TcM () Type
forall s. Type -> TcM s Type
refineType Type
ty)
(PGF -> Abstr
abstract PGF
pgf)
(\Type
ty MetaStore ()
ms ()
s Either TcError Type
_ -> Type -> Either TcError Type
forall a b. b -> Either a b
Right Type
ty)
(\TcError
err ()
s Either TcError Type
_ -> TcError -> Either TcError Type
forall a b. a -> Either a b
Left TcError
err)
MetaStore ()
forall s. MetaStore s
emptyMetaStore () (String -> Either TcError Type
forall a. HasCallStack => String -> a
error String
"checkType")
tcType :: Scope -> Type -> TcM s Type
tcType :: Scope -> Type -> TcM s Type
tcType Scope
scope ty :: Type
ty@(DTyp [Hypo]
hyps CId
cat [Expr]
es) = do
(Scope
scope,[Hypo]
hyps) <- Scope -> [Hypo] -> TcM s (Scope, [Hypo])
forall s. Scope -> [Hypo] -> TcM s (Scope, [Hypo])
tcHypos Scope
scope [Hypo]
hyps
[Hypo]
c_hyps <- CId -> TcM s [Hypo]
forall s. CId -> TcM s [Hypo]
lookupCatHyps CId
cat
let m :: Int
m = [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
n :: Int
n = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type
ty | (BindType
Explicit,CId
x,Type
ty) <- [Hypo]
c_hyps]
(Env
delta,[Expr]
es) <- Scope
-> [Expr]
-> Env
-> [Hypo]
-> Type
-> Int
-> Int
-> TcM s (Env, [Expr])
forall s.
Scope
-> [Expr]
-> Env
-> [Hypo]
-> Type
-> Int
-> Int
-> TcM s (Env, [Expr])
tcCatArgs Scope
scope [Expr]
es [] [Hypo]
c_hyps Type
ty Int
n Int
m
Type -> TcM s Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hyps CId
cat [Expr]
es)
tcHypos :: Scope -> [Hypo] -> TcM s (Scope,[Hypo])
tcHypos :: Scope -> [Hypo] -> TcM s (Scope, [Hypo])
tcHypos Scope
scope [] = (Scope, [Hypo]) -> TcM s (Scope, [Hypo])
forall (m :: * -> *) a. Monad m => a -> m a
return (Scope
scope,[])
tcHypos Scope
scope (Hypo
h:[Hypo]
hs) = do
(Scope
scope,Hypo
h ) <- Scope -> Hypo -> TcM s (Scope, Hypo)
forall s. Scope -> Hypo -> TcM s (Scope, Hypo)
tcHypo Scope
scope Hypo
h
(Scope
scope,[Hypo]
hs) <- Scope -> [Hypo] -> TcM s (Scope, [Hypo])
forall s. Scope -> [Hypo] -> TcM s (Scope, [Hypo])
tcHypos Scope
scope [Hypo]
hs
(Scope, [Hypo]) -> TcM s (Scope, [Hypo])
forall (m :: * -> *) a. Monad m => a -> m a
return (Scope
scope,Hypo
hHypo -> [Hypo] -> [Hypo]
forall a. a -> [a] -> [a]
:[Hypo]
hs)
tcHypo :: Scope -> Hypo -> TcM s (Scope,Hypo)
tcHypo :: Scope -> Hypo -> TcM s (Scope, Hypo)
tcHypo Scope
scope (BindType
b,CId
x,Type
ty) = do
Type
ty <- Scope -> Type -> TcM s Type
forall s. Scope -> Type -> TcM s Type
tcType Scope
scope Type
ty
if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then (Scope, Hypo) -> TcM s (Scope, Hypo)
forall (m :: * -> *) a. Monad m => a -> m a
return (Scope
scope,(BindType
b,CId
x,Type
ty))
else (Scope, Hypo) -> TcM s (Scope, Hypo)
forall (m :: * -> *) a. Monad m => a -> m a
return (CId -> TType -> Scope -> Scope
addScopedVar CId
x (Env -> Type -> TType
TTyp (Scope -> Env
scopeEnv Scope
scope) Type
ty) Scope
scope,(BindType
b,CId
x,Type
ty))
tcCatArgs :: Scope
-> [Expr]
-> Env
-> [Hypo]
-> Type
-> Int
-> Int
-> TcM s (Env, [Expr])
tcCatArgs Scope
scope [] Env
delta [] Type
ty0 Int
n Int
m = (Env, [Expr]) -> TcM s (Env, [Expr])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
delta,[])
tcCatArgs Scope
scope (EImplArg Expr
e:[Expr]
es) Env
delta ((BindType
Explicit,CId
x,Type
ty):[Hypo]
hs) Type
ty0 Int
n Int
m = TcError -> TcM s (Env, [Expr])
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([CId] -> Expr -> TcError
UnexpectedImplArg (Scope -> [CId]
scopeVars Scope
scope) Expr
e)
tcCatArgs Scope
scope (EImplArg Expr
e:[Expr]
es) Env
delta ((BindType
Implicit,CId
x,Type
ty):[Hypo]
hs) Type
ty0 Int
n Int
m = do
Expr
e <- Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr Scope
scope Expr
e (Env -> Type -> TType
TTyp Env
delta Type
ty)
(Env
delta,[Expr]
es) <- if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then Scope
-> [Expr]
-> Env
-> [Hypo]
-> Type
-> Int
-> Int
-> TcM s (Env, [Expr])
tcCatArgs Scope
scope [Expr]
es Env
delta [Hypo]
hs Type
ty0 Int
n Int
m
else do Value
v <- Env -> Expr -> TcM s Value
forall s. Env -> Expr -> TcM s Value
eval (Scope -> Env
scopeEnv Scope
scope) Expr
e
Scope
-> [Expr]
-> Env
-> [Hypo]
-> Type
-> Int
-> Int
-> TcM s (Env, [Expr])
tcCatArgs Scope
scope [Expr]
es (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta) [Hypo]
hs Type
ty0 Int
n Int
m
(Env, [Expr]) -> TcM s (Env, [Expr])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
delta,Expr -> Expr
EImplArg Expr
eExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
es)
tcCatArgs Scope
scope [Expr]
es Env
delta ((BindType
Implicit,CId
x,Type
ty):[Hypo]
hs) Type
ty0 Int
n Int
m = do
Int
i <- Scope -> TType -> TcM s Int
forall s. Scope -> TType -> TcM s Int
newMeta Scope
scope (Env -> Type -> TType
TTyp Env
delta Type
ty)
(Env
delta,[Expr]
es) <- if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then Scope
-> [Expr]
-> Env
-> [Hypo]
-> Type
-> Int
-> Int
-> TcM s (Env, [Expr])
tcCatArgs Scope
scope [Expr]
es Env
delta [Hypo]
hs Type
ty0 Int
n Int
m
else Scope
-> [Expr]
-> Env
-> [Hypo]
-> Type
-> Int
-> Int
-> TcM s (Env, [Expr])
tcCatArgs Scope
scope [Expr]
es (Int -> Env -> Env -> Value
VMeta Int
i (Scope -> Env
scopeEnv Scope
scope) [] Value -> Env -> Env
forall a. a -> [a] -> [a]
: Env
delta) [Hypo]
hs Type
ty0 Int
n Int
m
(Env, [Expr]) -> TcM s (Env, [Expr])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
delta,Expr -> Expr
EImplArg (Int -> Expr
EMeta Int
i) Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
es)
tcCatArgs Scope
scope (Expr
e:[Expr]
es) Env
delta ((BindType
Explicit,CId
x,Type
ty):[Hypo]
hs) Type
ty0 Int
n Int
m = do
Expr
e <- Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr Scope
scope Expr
e (Env -> Type -> TType
TTyp Env
delta Type
ty)
(Env
delta,[Expr]
es) <- if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then Scope
-> [Expr]
-> Env
-> [Hypo]
-> Type
-> Int
-> Int
-> TcM s (Env, [Expr])
tcCatArgs Scope
scope [Expr]
es Env
delta [Hypo]
hs Type
ty0 Int
n Int
m
else do Value
v <- Env -> Expr -> TcM s Value
forall s. Env -> Expr -> TcM s Value
eval (Scope -> Env
scopeEnv Scope
scope) Expr
e
Scope
-> [Expr]
-> Env
-> [Hypo]
-> Type
-> Int
-> Int
-> TcM s (Env, [Expr])
tcCatArgs Scope
scope [Expr]
es (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta) [Hypo]
hs Type
ty0 Int
n Int
m
(Env, [Expr]) -> TcM s (Env, [Expr])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
delta,Expr
eExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
es)
tcCatArgs Scope
scope [Expr]
_ Env
delta [Hypo]
_ ty0 :: Type
ty0@(DTyp [Hypo]
_ CId
cat [Expr]
_) Int
n Int
m = do
TcError -> TcM s (Env, [Expr])
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([CId] -> Type -> CId -> Int -> Int -> TcError
WrongCatArgs (Scope -> [CId]
scopeVars Scope
scope) Type
ty0 CId
cat Int
n Int
m)
checkExpr :: PGF -> Expr -> Type -> Either TcError Expr
checkExpr :: PGF -> Expr -> Type -> Either TcError Expr
checkExpr PGF
pgf Expr
e Type
ty =
TcM () Expr
-> Abstr
-> (Expr
-> MetaStore ()
-> ()
-> Either TcError Expr
-> Either TcError Expr)
-> (TcError -> () -> Either TcError Expr -> Either TcError Expr)
-> MetaStore ()
-> ()
-> Either TcError Expr
-> Either TcError Expr
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM (do Expr
e <- Scope -> Expr -> TType -> TcM () Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr Scope
emptyScope Expr
e (Env -> Type -> TType
TTyp [] Type
ty)
Scope -> Expr -> TcM () Expr
forall s. Scope -> Expr -> TcM s Expr
checkResolvedMetaStore Scope
emptyScope Expr
e)
(PGF -> Abstr
abstract PGF
pgf)
(\Expr
e MetaStore ()
ms ()
s Either TcError Expr
_ -> Expr -> Either TcError Expr
forall a b. b -> Either a b
Right Expr
e)
(\TcError
err ()
s Either TcError Expr
_ -> TcError -> Either TcError Expr
forall a b. a -> Either a b
Left TcError
err)
MetaStore ()
forall s. MetaStore s
emptyMetaStore () (String -> Either TcError Expr
forall a. HasCallStack => String -> a
error String
"checkExpr")
tcExpr :: Scope -> Expr -> TType -> TcM s Expr
tcExpr :: Scope -> Expr -> TType -> TcM s Expr
tcExpr Scope
scope e0 :: Expr
e0@(EAbs BindType
Implicit CId
x Expr
e) TType
tty =
case TType
tty of
TTyp Env
delta (DTyp ((BindType
Implicit,CId
y,Type
ty):[Hypo]
hs) CId
c [Expr]
es) -> do Expr
e <- if CId
y CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr (CId -> TType -> Scope -> Scope
addScopedVar CId
x (Env -> Type -> TType
TTyp Env
delta Type
ty) Scope
scope)
Expr
e (Env -> Type -> TType
TTyp Env
delta ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es))
else Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr (CId -> TType -> Scope -> Scope
addScopedVar CId
x (Env -> Type -> TType
TTyp Env
delta Type
ty) Scope
scope)
Expr
e (Env -> Type -> TType
TTyp ((Int -> Env -> Value
VGen (Scope -> Int
scopeSize Scope
scope) [])Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta) ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es))
Expr -> TcM s Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType -> CId -> Expr -> Expr
EAbs BindType
Implicit CId
x Expr
e)
TType
_ -> do Type
ty <- Int -> TType -> TcM s Type
forall s. Int -> TType -> TcM s Type
evalType (Scope -> Int
scopeSize Scope
scope) TType
tty
TcError -> TcM s Expr
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([CId] -> Expr -> Type -> TcError
NotFunType (Scope -> [CId]
scopeVars Scope
scope) Expr
e0 Type
ty)
tcExpr Scope
scope Expr
e0 (TTyp Env
delta (DTyp ((BindType
Implicit,CId
y,Type
ty):[Hypo]
hs) CId
c [Expr]
es)) = do
Expr
e0 <- if CId
y CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr (CId -> TType -> Scope -> Scope
addScopedVar CId
wildCId (Env -> Type -> TType
TTyp Env
delta Type
ty) Scope
scope)
Expr
e0 (Env -> Type -> TType
TTyp Env
delta ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es))
else Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr (CId -> TType -> Scope -> Scope
addScopedVar CId
wildCId (Env -> Type -> TType
TTyp Env
delta Type
ty) Scope
scope)
Expr
e0 (Env -> Type -> TType
TTyp ((Int -> Env -> Value
VGen (Scope -> Int
scopeSize Scope
scope) [])Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta) ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es))
Expr -> TcM s Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType -> CId -> Expr -> Expr
EAbs BindType
Implicit CId
wildCId Expr
e0)
tcExpr Scope
scope e0 :: Expr
e0@(EAbs BindType
Explicit CId
x Expr
e) TType
tty =
case TType
tty of
TTyp Env
delta (DTyp ((BindType
Explicit,CId
y,Type
ty):[Hypo]
hs) CId
c [Expr]
es) -> do Expr
e <- if CId
y CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr (CId -> TType -> Scope -> Scope
addScopedVar CId
x (Env -> Type -> TType
TTyp Env
delta Type
ty) Scope
scope)
Expr
e (Env -> Type -> TType
TTyp Env
delta ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es))
else Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr (CId -> TType -> Scope -> Scope
addScopedVar CId
x (Env -> Type -> TType
TTyp Env
delta Type
ty) Scope
scope)
Expr
e (Env -> Type -> TType
TTyp ((Int -> Env -> Value
VGen (Scope -> Int
scopeSize Scope
scope) [])Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta) ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es))
Expr -> TcM s Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType -> CId -> Expr -> Expr
EAbs BindType
Explicit CId
x Expr
e)
TType
_ -> do Type
ty <- Int -> TType -> TcM s Type
forall s. Int -> TType -> TcM s Type
evalType (Scope -> Int
scopeSize Scope
scope) TType
tty
TcError -> TcM s Expr
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([CId] -> Expr -> Type -> TcError
NotFunType (Scope -> [CId]
scopeVars Scope
scope) Expr
e0 Type
ty)
tcExpr Scope
scope (EMeta Int
_) TType
tty = do
Int
i <- Scope -> TType -> TcM s Int
forall s. Scope -> TType -> TcM s Int
newMeta Scope
scope TType
tty
Expr -> TcM s Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Expr
EMeta Int
i)
tcExpr Scope
scope Expr
e0 TType
tty = do
(Expr
e0,TType
tty0) <- Scope -> Expr -> TcM s (Expr, TType)
forall s. Scope -> Expr -> TcM s (Expr, TType)
infExpr Scope
scope Expr
e0
(Expr
e0,TType
tty0) <- Scope -> Expr -> TType -> TcM s (Expr, TType)
forall s. Scope -> Expr -> TType -> TcM s (Expr, TType)
appImplArg Scope
scope Expr
e0 TType
tty0
Int
i <- Expr -> TcM s Int
forall s. Expr -> TcM s Int
newGuardedMeta Expr
e0
Scope -> Int -> Int -> TType -> TType -> TcM s ()
forall s. Scope -> Int -> Int -> TType -> TType -> TcM s ()
eqType Scope
scope (Scope -> Int
scopeSize Scope
scope) Int
i TType
tty TType
tty0
Expr -> TcM s Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Expr
EMeta Int
i)
inferExpr :: PGF -> Expr -> Either TcError (Expr,Type)
inferExpr :: PGF -> Expr -> Either TcError (Expr, Type)
inferExpr PGF
pgf Expr
e =
TcM () (Expr, Type)
-> Abstr
-> ((Expr, Type)
-> MetaStore ()
-> ()
-> Either TcError (Expr, Type)
-> Either TcError (Expr, Type))
-> (TcError
-> ()
-> Either TcError (Expr, Type)
-> Either TcError (Expr, Type))
-> MetaStore ()
-> ()
-> Either TcError (Expr, Type)
-> Either TcError (Expr, Type)
forall s a.
TcM s a
-> forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b
unTcM (do (Expr
e,TType
tty) <- Scope -> Expr -> TcM () (Expr, TType)
forall s. Scope -> Expr -> TcM s (Expr, TType)
infExpr Scope
emptyScope Expr
e
Expr
e <- Scope -> Expr -> TcM () Expr
forall s. Scope -> Expr -> TcM s Expr
checkResolvedMetaStore Scope
emptyScope Expr
e
Type
ty <- Int -> TType -> TcM () Type
forall s. Int -> TType -> TcM s Type
evalType Int
0 TType
tty
(Expr, Type) -> TcM () (Expr, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e,Type
ty))
(PGF -> Abstr
abstract PGF
pgf)
(\(Expr, Type)
e_ty MetaStore ()
ms ()
s Either TcError (Expr, Type)
_ -> (Expr, Type) -> Either TcError (Expr, Type)
forall a b. b -> Either a b
Right (Expr, Type)
e_ty)
(\TcError
err ()
s Either TcError (Expr, Type)
_ -> TcError -> Either TcError (Expr, Type)
forall a b. a -> Either a b
Left TcError
err)
MetaStore ()
forall s. MetaStore s
emptyMetaStore () (String -> Either TcError (Expr, Type)
forall a. HasCallStack => String -> a
error String
"inferExpr")
infExpr :: Scope -> Expr -> TcM s (Expr,TType)
infExpr :: Scope -> Expr -> TcM s (Expr, TType)
infExpr Scope
scope e0 :: Expr
e0@(EApp Expr
e1 Expr
e2) = do
(Expr
e1,TTyp Env
delta Type
ty) <- Scope -> Expr -> TcM s (Expr, TType)
forall s. Scope -> Expr -> TcM s (Expr, TType)
infExpr Scope
scope Expr
e1
(Expr
e0,Env
delta,Type
ty) <- Scope -> Expr -> Expr -> Env -> Type -> TcM s (Expr, Env, Type)
forall s.
Scope -> Expr -> Expr -> Env -> Type -> TcM s (Expr, Env, Type)
tcArg Scope
scope Expr
e1 Expr
e2 Env
delta Type
ty
(Expr, TType) -> TcM s (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e0,Env -> Type -> TType
TTyp Env
delta Type
ty)
infExpr Scope
scope e0 :: Expr
e0@(EFun CId
x) = do
case CId -> Scope -> Maybe (Int, TType)
lookupVar CId
x Scope
scope of
Just (Int
i,TType
tty) -> (Expr, TType) -> TcM s (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Expr
EVar Int
i,TType
tty)
Maybe (Int, TType)
Nothing -> do Type
ty <- CId -> TcM s Type
forall s. CId -> TcM s Type
lookupFunType CId
x
(Expr, TType) -> TcM s (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e0,Env -> Type -> TType
TTyp [] Type
ty)
infExpr Scope
scope e0 :: Expr
e0@(EVar Int
i) = do
(Expr, TType) -> TcM s (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e0,(CId, TType) -> TType
forall a b. (a, b) -> b
snd (Int -> Scope -> (CId, TType)
getVar Int
i Scope
scope))
infExpr Scope
scope e0 :: Expr
e0@(ELit Literal
l) = do
let cat :: CId
cat = case Literal
l of
LStr String
_ -> String -> CId
mkCId String
"String"
LInt Int
_ -> String -> CId
mkCId String
"Int"
LFlt Double
_ -> String -> CId
mkCId String
"Float"
(Expr, TType) -> TcM s (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e0,Env -> Type -> TType
TTyp [] ([Hypo] -> CId -> [Expr] -> Type
DTyp [] CId
cat []))
infExpr Scope
scope (ETyped Expr
e Type
ty) = do
Type
ty <- Scope -> Type -> TcM s Type
forall s. Scope -> Type -> TcM s Type
tcType Scope
scope Type
ty
Expr
e <- Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr Scope
scope Expr
e (Env -> Type -> TType
TTyp (Scope -> Env
scopeEnv Scope
scope) Type
ty)
(Expr, TType) -> TcM s (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Type -> Expr
ETyped Expr
e Type
ty,Env -> Type -> TType
TTyp (Scope -> Env
scopeEnv Scope
scope) Type
ty)
infExpr Scope
scope (EImplArg Expr
e) = do
(Expr
e,TType
tty) <- Scope -> Expr -> TcM s (Expr, TType)
forall s. Scope -> Expr -> TcM s (Expr, TType)
infExpr Scope
scope Expr
e
(Expr, TType) -> TcM s (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
EImplArg Expr
e,TType
tty)
infExpr Scope
scope Expr
e = TcError -> TcM s (Expr, TType)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([CId] -> Expr -> TcError
CannotInferType (Scope -> [CId]
scopeVars Scope
scope) Expr
e)
tcArg :: Scope -> Expr -> Expr -> Env -> Type -> TcM s (Expr, Env, Type)
tcArg Scope
scope Expr
e1 Expr
e2 Env
delta ty0 :: Type
ty0@(DTyp [] CId
c [Expr]
es) = do
Type
ty1 <- Int -> TType -> TcM s Type
forall s. Int -> TType -> TcM s Type
evalType (Scope -> Int
scopeSize Scope
scope) (Env -> Type -> TType
TTyp Env
delta Type
ty0)
TcError -> TcM s (Expr, Env, Type)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([CId] -> Expr -> Type -> TcError
NotFunType (Scope -> [CId]
scopeVars Scope
scope) Expr
e1 Type
ty1)
tcArg Scope
scope Expr
e1 (EImplArg Expr
e2) Env
delta ty0 :: Type
ty0@(DTyp ((BindType
Explicit,CId
x,Type
ty):[Hypo]
hs) CId
c [Expr]
es) = TcError -> TcM s (Expr, Env, Type)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([CId] -> Expr -> TcError
UnexpectedImplArg (Scope -> [CId]
scopeVars Scope
scope) Expr
e2)
tcArg Scope
scope Expr
e1 (EImplArg Expr
e2) Env
delta ty0 :: Type
ty0@(DTyp ((BindType
Implicit,CId
x,Type
ty):[Hypo]
hs) CId
c [Expr]
es) = do
Expr
e2 <- Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr Scope
scope Expr
e2 (Env -> Type -> TType
TTyp Env
delta Type
ty)
if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then (Expr, Env, Type) -> TcM s (Expr, Env, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1 (Expr -> Expr
EImplArg Expr
e2), Env
delta,[Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es)
else do Value
v2 <- Env -> Expr -> TcM s Value
forall s. Env -> Expr -> TcM s Value
eval (Scope -> Env
scopeEnv Scope
scope) Expr
e2
(Expr, Env, Type) -> TcM s (Expr, Env, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1 (Expr -> Expr
EImplArg Expr
e2),Value
v2Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta,[Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es)
tcArg Scope
scope Expr
e1 Expr
e2 Env
delta ty0 :: Type
ty0@(DTyp ((BindType
Explicit,CId
x,Type
ty):[Hypo]
hs) CId
c [Expr]
es) = do
Expr
e2 <- Scope -> Expr -> TType -> TcM s Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr Scope
scope Expr
e2 (Env -> Type -> TType
TTyp Env
delta Type
ty)
if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then (Expr, Env, Type) -> TcM s (Expr, Env, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1 Expr
e2,Env
delta,[Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es)
else do Value
v2 <- Env -> Expr -> TcM s Value
forall s. Env -> Expr -> TcM s Value
eval (Scope -> Env
scopeEnv Scope
scope) Expr
e2
(Expr, Env, Type) -> TcM s (Expr, Env, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1 Expr
e2,Value
v2Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta,[Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es)
tcArg Scope
scope Expr
e1 Expr
e2 Env
delta ty0 :: Type
ty0@(DTyp ((BindType
Implicit,CId
x,Type
ty):[Hypo]
hs) CId
c [Expr]
es) = do
Int
i <- Scope -> TType -> TcM s Int
forall s. Scope -> TType -> TcM s Int
newMeta Scope
scope (Env -> Type -> TType
TTyp Env
delta Type
ty)
if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then Scope -> Expr -> Expr -> Env -> Type -> TcM s (Expr, Env, Type)
tcArg Scope
scope (Expr -> Expr -> Expr
EApp Expr
e1 (Expr -> Expr
EImplArg (Int -> Expr
EMeta Int
i))) Expr
e2 Env
delta ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es)
else Scope -> Expr -> Expr -> Env -> Type -> TcM s (Expr, Env, Type)
tcArg Scope
scope (Expr -> Expr -> Expr
EApp Expr
e1 (Expr -> Expr
EImplArg (Int -> Expr
EMeta Int
i))) Expr
e2 (Int -> Env -> Env -> Value
VMeta Int
i (Scope -> Env
scopeEnv Scope
scope) [] Value -> Env -> Env
forall a. a -> [a] -> [a]
: Env
delta) ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es)
appImplArg :: Scope -> Expr -> TType -> TcM s (Expr, TType)
appImplArg Scope
scope Expr
e (TTyp Env
delta (DTyp ((BindType
Implicit,CId
x,Type
ty1):[Hypo]
hypos) CId
cat [Expr]
es)) = do
Int
i <- Scope -> TType -> TcM s Int
forall s. Scope -> TType -> TcM s Int
newMeta Scope
scope (Env -> Type -> TType
TTyp Env
delta Type
ty1)
let delta' :: Env
delta' = if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then Env
delta
else Int -> Env -> Env -> Value
VMeta Int
i (Scope -> Env
scopeEnv Scope
scope) [] Value -> Env -> Env
forall a. a -> [a] -> [a]
: Env
delta
Scope -> Expr -> TType -> TcM s (Expr, TType)
appImplArg Scope
scope (Expr -> Expr -> Expr
EApp Expr
e (Expr -> Expr
EImplArg (Int -> Expr
EMeta Int
i))) (Env -> Type -> TType
TTyp Env
delta' ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hypos CId
cat [Expr]
es))
appImplArg Scope
scope Expr
e TType
tty = (Expr, TType) -> TcM s (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e,TType
tty)
eqType :: Scope -> Int -> MetaId -> TType -> TType -> TcM s ()
eqType :: Scope -> Int -> Int -> TType -> TType -> TcM s ()
eqType Scope
scope Int
k Int
i0 tty1 :: TType
tty1@(TTyp Env
delta1 ty1 :: Type
ty1@(DTyp [Hypo]
hyps1 CId
cat1 [Expr]
es1)) tty2 :: TType
tty2@(TTyp Env
delta2 ty2 :: Type
ty2@(DTyp [Hypo]
hyps2 CId
cat2 [Expr]
es2))
| CId
cat1 CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
cat2 = do (Int
k,Env
delta1,Env
delta2) <- Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int, Env, Env)
forall s.
Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int, Env, Env)
eqHyps Int
k Env
delta1 [Hypo]
hyps1 Env
delta2 [Hypo]
hyps2
[TcM s ()] -> TcM s ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Env
-> Expr
-> Env
-> Expr
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Env
-> Expr
-> Env
-> Expr
-> TcM s ()
eqExpr forall a. TcM s a
forall s b. TcM s b
raiseTypeMatchError (Int -> Int -> (Expr -> TcM s ()) -> TcM s ()
forall s. Int -> Int -> (Expr -> TcM s ()) -> TcM s ()
addConstraint Int
i0) Int
k Env
delta1 Expr
e1 Env
delta2 Expr
e2 | (Expr
e1,Expr
e2) <- [Expr] -> [Expr] -> [(Expr, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Expr]
es1 [Expr]
es2]
| Bool
otherwise = TcM s ()
forall s b. TcM s b
raiseTypeMatchError
where
raiseTypeMatchError :: TcM s b
raiseTypeMatchError = do Type
ty1 <- Int -> TType -> TcM s Type
forall s. Int -> TType -> TcM s Type
evalType Int
k TType
tty1
Type
ty2 <- Int -> TType -> TcM s Type
forall s. Int -> TType -> TcM s Type
evalType Int
k TType
tty2
Expr
e <- Expr -> TcM s Expr
forall s. Expr -> TcM s Expr
refineExpr (Int -> Expr
EMeta Int
i0)
TcError -> TcM s b
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([CId] -> Expr -> Type -> Type -> TcError
TypeMismatch (Scope -> [CId]
scopeVars Scope
scope) Expr
e Type
ty1 Type
ty2)
eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int,Env,Env)
eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int, Env, Env)
eqHyps Int
k Env
delta1 [] Env
delta2 [] =
(Int, Env, Env) -> TcM s (Int, Env, Env)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
k,Env
delta1,Env
delta2)
eqHyps Int
k Env
delta1 ((BindType
_,CId
x,Type
ty1) : [Hypo]
h1s) Env
delta2 ((BindType
_,CId
y,Type
ty2) : [Hypo]
h2s) = do
Scope -> Int -> Int -> TType -> TType -> TcM s ()
forall s. Scope -> Int -> Int -> TType -> TType -> TcM s ()
eqType Scope
scope Int
k Int
i0 (Env -> Type -> TType
TTyp Env
delta1 Type
ty1) (Env -> Type -> TType
TTyp Env
delta2 Type
ty2)
if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId Bool -> Bool -> Bool
&& CId
y CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int, Env, Env)
forall s.
Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int, Env, Env)
eqHyps Int
k Env
delta1 [Hypo]
h1s Env
delta2 [Hypo]
h2s
else if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
/= CId
wildCId Bool -> Bool -> Bool
&& CId
y CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
/= CId
wildCId
then Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int, Env, Env)
forall s.
Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int, Env, Env)
eqHyps (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ((Int -> Env -> Value
VGen Int
k [])Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta1) [Hypo]
h1s ((Int -> Env -> Value
VGen Int
k [])Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta2) [Hypo]
h2s
else TcM s (Int, Env, Env)
forall s b. TcM s b
raiseTypeMatchError
eqHyps Int
k Env
delta1 [Hypo]
h1s Env
delta2 [Hypo]
h2s = TcM s (Int, Env, Env)
forall s b. TcM s b
raiseTypeMatchError
eqExpr :: (forall a . TcM s a) -> (MetaId -> (Expr -> TcM s ()) -> TcM s ()) -> Int -> Env -> Expr -> Env -> Expr -> TcM s ()
eqExpr :: (forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Env
-> Expr
-> Env
-> Expr
-> TcM s ()
eqExpr forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
k Env
env1 Expr
e1 Env
env2 Expr
e2 = do
Value
v1 <- Env -> Expr -> TcM s Value
forall s. Env -> Expr -> TcM s Value
eval Env
env1 Expr
e1
Value
v2 <- Env -> Expr -> TcM s Value
forall s. Env -> Expr -> TcM s Value
eval Env
env2 Expr
e2
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
k Value
v1 Value
v2
eqValue :: (forall a . TcM s a) -> (MetaId -> (Expr -> TcM s ()) -> TcM s ()) -> Int -> Value -> Value -> TcM s ()
eqValue :: (forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
k Value
v1 Value
v2 = do
Value
v1 <- Value -> TcM s Value
forall s. Value -> TcM s Value
deRef Value
v1
Value
v2 <- Value -> TcM s Value
forall s. Value -> TcM s Value
deRef Value
v2
Int -> Value -> Value -> TcM s ()
eqValue' Int
k Value
v1 Value
v2
where
deRef :: Value -> TcM s Value
deRef v :: Value
v@(VMeta Int
i Env
env Env
vs) = do
MetaValue s
mv <- Int -> TcM s (MetaValue s)
forall s. Int -> TcM s (MetaValue s)
getMeta Int
i
case MetaValue s
mv of
MBound Expr
e -> Env -> Expr -> Env -> TcM s Value
forall s. Env -> Expr -> Env -> TcM s Value
apply Env
env Expr
e Env
vs
MGuarded Expr
e [Expr -> TcM s ()]
_ Int
x | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 -> Env -> Expr -> Env -> TcM s Value
forall s. Env -> Expr -> Env -> TcM s Value
apply Env
env Expr
e Env
vs
| Bool
otherwise -> Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
MUnbound s
_ Scope
_ TType
_ [Expr -> TcM s ()]
_ -> Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
deRef Value
v = Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
eqValue' :: Int -> Value -> Value -> TcM s ()
eqValue' Int
k (VSusp Int
i Env
env Env
vs1 Value -> Value
c) Value
v2 = Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
i (\Expr
e -> Env -> Expr -> Env -> TcM s Value
forall s. Env -> Expr -> Env -> TcM s Value
apply Env
env Expr
e Env
vs1 TcM s Value -> (Value -> TcM s ()) -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value
v1 -> (forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
k (Value -> Value
c Value
v1) Value
v2)
eqValue' Int
k Value
v1 (VSusp Int
i Env
env Env
vs2 Value -> Value
c) = Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
i (\Expr
e -> Env -> Expr -> Env -> TcM s Value
forall s. Env -> Expr -> Env -> TcM s Value
apply Env
env Expr
e Env
vs2 TcM s Value -> (Value -> TcM s ()) -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value
v2 -> (forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
k Value
v1 (Value -> Value
c Value
v2))
eqValue' Int
k (VMeta Int
i Env
env1 Env
vs1) (VMeta Int
j Env
env2 Env
vs2) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = (Value -> Value -> TcM s ()) -> Env -> Env -> TcM s ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ ((forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
k) Env
vs1 Env
vs2
eqValue' Int
k (VMeta Int
i Env
env1 Env
vs1) Value
v2 = do MetaValue s
mv <- Int -> TcM s (MetaValue s)
forall s. Int -> TcM s (MetaValue s)
getMeta Int
i
case MetaValue s
mv of
MUnbound s
_ Scope
scopei TType
_ [Expr -> TcM s ()]
cs -> Int
-> Scope -> [Expr -> TcM s ()] -> Env -> Env -> Value -> TcM s ()
forall a.
Int
-> Scope -> [Expr -> TcM s a] -> Env -> Env -> Value -> TcM s ()
bind Int
i Scope
scopei [Expr -> TcM s ()]
cs Env
env1 Env
vs1 Value
v2
MGuarded Expr
e [Expr -> TcM s ()]
cs Int
x -> Int -> MetaValue s -> TcM s ()
forall s. Int -> MetaValue s -> TcM s ()
setMeta Int
i (Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
forall s. Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
MGuarded Expr
e ((\Expr
e -> Env -> Expr -> Env -> TcM s Value
forall s. Env -> Expr -> Env -> TcM s Value
apply Env
env1 Expr
e Env
vs1 TcM s Value -> (Value -> TcM s ()) -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value
v1 -> Int -> Value -> Value -> TcM s ()
eqValue' Int
k Value
v1 Value
v2) (Expr -> TcM s ()) -> [Expr -> TcM s ()] -> [Expr -> TcM s ()]
forall a. a -> [a] -> [a]
: [Expr -> TcM s ()]
cs) Int
x)
eqValue' Int
k Value
v1 (VMeta Int
i Env
env2 Env
vs2) = do MetaValue s
mv <- Int -> TcM s (MetaValue s)
forall s. Int -> TcM s (MetaValue s)
getMeta Int
i
case MetaValue s
mv of
MUnbound s
_ Scope
scopei TType
_ [Expr -> TcM s ()]
cs -> Int
-> Scope -> [Expr -> TcM s ()] -> Env -> Env -> Value -> TcM s ()
forall a.
Int
-> Scope -> [Expr -> TcM s a] -> Env -> Env -> Value -> TcM s ()
bind Int
i Scope
scopei [Expr -> TcM s ()]
cs Env
env2 Env
vs2 Value
v1
MGuarded Expr
e [Expr -> TcM s ()]
cs Int
x -> Int -> MetaValue s -> TcM s ()
forall s. Int -> MetaValue s -> TcM s ()
setMeta Int
i (Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
forall s. Expr -> [Expr -> TcM s ()] -> Int -> MetaValue s
MGuarded Expr
e ((\Expr
e -> Env -> Expr -> Env -> TcM s Value
forall s. Env -> Expr -> Env -> TcM s Value
apply Env
env2 Expr
e Env
vs2 TcM s Value -> (Value -> TcM s ()) -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value
v2 -> Int -> Value -> Value -> TcM s ()
eqValue' Int
k Value
v1 Value
v2) (Expr -> TcM s ()) -> [Expr -> TcM s ()] -> [Expr -> TcM s ()]
forall a. a -> [a] -> [a]
: [Expr -> TcM s ()]
cs) Int
x)
eqValue' Int
k (VApp CId
f1 Env
vs1) (VApp CId
f2 Env
vs2) | CId
f1 CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
f2 = (Value -> Value -> TcM s ()) -> Env -> Env -> TcM s ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ ((forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
k) Env
vs1 Env
vs2
eqValue' Int
k (VConst CId
f1 Env
vs1) (VConst CId
f2 Env
vs2) | CId
f1 CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
f2 = (Value -> Value -> TcM s ()) -> Env -> Env -> TcM s ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ ((forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
k) Env
vs1 Env
vs2
eqValue' Int
k (VLit Literal
l1) (VLit Literal
l2 ) | Literal
l1 Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l2 = () -> TcM s ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
eqValue' Int
k (VGen Int
i Env
vs1) (VGen Int
j Env
vs2) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = (Value -> Value -> TcM s ()) -> Env -> Env -> TcM s ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ ((forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
k) Env
vs1 Env
vs2
eqValue' Int
k (VClosure Env
env1 (EAbs BindType
_ CId
x1 Expr
e1)) (VClosure Env
env2 (EAbs BindType
_ CId
x2 Expr
e2)) = let v :: Value
v = Int -> Env -> Value
VGen Int
k []
in (forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Env
-> Expr
-> Env
-> Expr
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Env
-> Expr
-> Env
-> Expr
-> TcM s ()
eqExpr forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env1) Expr
e1 (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env2) Expr
e2
eqValue' Int
k (VClosure Env
env1 (EAbs BindType
_ CId
x1 Expr
e1)) Value
v2 = let v :: Value
v = Int -> Env -> Value
VGen Int
k []
in do Value
v1 <- Env -> Expr -> TcM s Value
forall s. Env -> Expr -> TcM s Value
eval (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env1) Expr
e1
Value
v2 <- Value -> Env -> TcM s Value
forall s. Value -> Env -> TcM s Value
applyValue Value
v2 [Value
v]
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Value
v1 Value
v2
eqValue' Int
k Value
v1 (VClosure Env
env2 (EAbs BindType
_ CId
x2 Expr
e2)) = let v :: Value
v = Int -> Env -> Value
VGen Int
k []
in do Value
v1 <- Value -> Env -> TcM s Value
forall s. Value -> Env -> TcM s Value
applyValue Value
v1 [Value
v]
Value
v2 <- Env -> Expr -> TcM s Value
forall s. Env -> Expr -> TcM s Value
eval (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env2) Expr
e2
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Value
v1 Value
v2
eqValue' Int
k Value
v1 Value
v2 = TcM s ()
forall a. TcM s a
fail
bind :: Int
-> Scope -> [Expr -> TcM s a] -> Env -> Env -> Value -> TcM s ()
bind Int
i Scope
scope [Expr -> TcM s a]
cs Env
env Env
vs0 Value
v = do
let k :: Int
k = Scope -> Int
scopeSize Scope
scope
vs :: Env
vs = Env -> Env
forall a. [a] -> [a]
reverse (Int -> Env -> Env
forall a. Int -> [a] -> [a]
List.take Int
k Env
env) Env -> Env -> Env
forall a. [a] -> [a] -> [a]
++ Env
vs0
xs :: [Int]
xs = [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub [Int
i | VGen i [] <- Env
vs]
if Env -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
vs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
xs
then Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
i (\Expr
e -> Env -> Expr -> Env -> TcM s Value
forall s. Env -> Expr -> Env -> TcM s Value
apply Env
env Expr
e Env
vs0 TcM s Value -> (Value -> TcM s ()) -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value
iv -> (forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM s a
fail Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
k Value
iv Value
v)
else do Value
v <- Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i Int
k [Int]
xs Value
v
Expr
e0 <- Int -> Value -> TcM s Expr
forall s. Int -> Value -> TcM s Expr
value2expr ([Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
xs) Value
v
let e :: Expr
e = Env -> Expr -> Expr
forall a. [a] -> Expr -> Expr
addLam Env
vs0 Expr
e0
Int -> MetaValue s -> TcM s ()
forall s. Int -> MetaValue s -> TcM s ()
setMeta Int
i (Expr -> MetaValue s
forall s. Expr -> MetaValue s
MBound Expr
e)
[TcM s a] -> TcM s ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [Expr -> TcM s a
c Expr
e | Expr -> TcM s a
c <- [Expr -> TcM s a]
cs]
where
addLam :: [a] -> Expr -> Expr
addLam [] Expr
e = Expr
e
addLam (a
v:[a]
vs) Expr
e = BindType -> CId -> Expr -> Expr
EAbs BindType
Explicit CId
var ([a] -> Expr -> Expr
addLam [a]
vs Expr
e)
var :: CId
var = String -> CId
mkCId String
"v"
occurCheck :: Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i0 Int
k [Int]
xs (VApp CId
f Env
vs) = do Env
vs <- (Value -> TcM s Value) -> Env -> TcM s Env
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i0 Int
k [Int]
xs) Env
vs
Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return (CId -> Env -> Value
VApp CId
f Env
vs)
occurCheck Int
i0 Int
k [Int]
xs (VLit Literal
l) = Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Literal -> Value
VLit Literal
l)
occurCheck Int
i0 Int
k [Int]
xs (VMeta Int
i Env
env Env
vs) = do if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i0
then TcM s ()
forall a. TcM s a
fail
else () -> TcM s ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
MetaValue s
mv <- Int -> TcM s (MetaValue s)
forall s. Int -> TcM s (MetaValue s)
getMeta Int
i
case MetaValue s
mv of
MBound Expr
e -> Env -> Expr -> Env -> TcM s Value
forall s. Env -> Expr -> Env -> TcM s Value
apply Env
env Expr
e Env
vs TcM s Value -> (Value -> TcM s Value) -> TcM s Value
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i0 Int
k [Int]
xs
MGuarded Expr
e [Expr -> TcM s ()]
_ Int
_ -> Env -> Expr -> Env -> TcM s Value
forall s. Env -> Expr -> Env -> TcM s Value
apply Env
env Expr
e Env
vs TcM s Value -> (Value -> TcM s Value) -> TcM s Value
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i0 Int
k [Int]
xs
MUnbound s
_ Scope
scopei TType
_ [Expr -> TcM s ()]
_ | Scope -> Int
scopeSize Scope
scopei Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
k -> TcM s Value
forall a. TcM s a
fail
| Bool
otherwise -> do Env
vs <- (Value -> TcM s Value) -> Env -> TcM s Env
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i0 Int
k [Int]
xs) Env
vs
Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Env -> Env -> Value
VMeta Int
i Env
env Env
vs)
occurCheck Int
i0 Int
k [Int]
xs (VSusp Int
i Env
env Env
vs Value -> Value
cnt) = do Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
i (\Expr
e -> Env -> Expr -> Env -> TcM s Value
forall s. Env -> Expr -> Env -> TcM s Value
apply Env
env Expr
e Env
vs TcM s Value -> (Value -> TcM s ()) -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value
v -> Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i0 Int
k [Int]
xs (Value -> Value
cnt Value
v) TcM s Value -> TcM s () -> TcM s ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> TcM s ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Env -> Env -> (Value -> Value) -> Value
VSusp Int
i Env
env Env
vs Value -> Value
cnt)
occurCheck Int
i0 Int
k [Int]
xs (VGen Int
i Env
vs) = case (Int -> Bool) -> [Int] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
i) [Int]
xs of
Just Int
i -> do Env
vs <- (Value -> TcM s Value) -> Env -> TcM s Env
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i0 Int
k [Int]
xs) Env
vs
Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Env -> Value
VGen Int
i Env
vs)
Maybe Int
Nothing -> TcM s Value
forall a. TcM s a
fail
occurCheck Int
i0 Int
k [Int]
xs (VConst CId
f Env
vs) = do Env
vs <- (Value -> TcM s Value) -> Env -> TcM s Env
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i0 Int
k [Int]
xs) Env
vs
Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return (CId -> Env -> Value
VConst CId
f Env
vs)
occurCheck Int
i0 Int
k [Int]
xs (VClosure Env
env Expr
e) = do Env
env <- (Value -> TcM s Value) -> Env -> TcM s Env
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i0 Int
k [Int]
xs) Env
env
Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> Expr -> Value
VClosure Env
env Expr
e)
occurCheck Int
i0 Int
k [Int]
xs (VImplArg Value
e) = do Value
e <- Int -> Int -> [Int] -> Value -> TcM s Value
occurCheck Int
i0 Int
k [Int]
xs Value
e
Value -> TcM s Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Value
VImplArg Value
e)
checkResolvedMetaStore :: Scope -> Expr -> TcM s Expr
checkResolvedMetaStore :: Scope -> Expr -> TcM s Expr
checkResolvedMetaStore Scope
scope Expr
e = do
Expr
e <- Expr -> TcM s Expr
forall s. Expr -> TcM s Expr
refineExpr Expr
e
(forall b.
Abstr
-> (() -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s ()
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr () -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms ->
let xs :: [Int]
xs = [Int
i | (Int
i,MetaValue s
mv) <- MetaStore s -> [(Int, MetaValue s)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList MetaStore s
ms, Bool -> Bool
not (MetaValue s -> Bool
forall s. MetaValue s -> Bool
isResolved MetaValue s
mv)]
in if [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
List.null [Int]
xs
then () -> MetaStore s -> s -> b -> b
k () MetaStore s
ms
else TcError -> s -> b -> b
h ([CId] -> Expr -> [Int] -> TcError
UnresolvedMetaVars (Scope -> [CId]
scopeVars Scope
scope) Expr
e [Int]
xs))
Expr -> TcM s Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
where
isResolved :: MetaValue s -> Bool
isResolved (MUnbound s
_ Scope
_ TType
_ []) = Bool
True
isResolved (MGuarded Expr
_ [Expr -> TcM s ()]
_ Int
_) = Bool
True
isResolved (MBound Expr
_) = Bool
True
isResolved MetaValue s
_ = Bool
False
generateForMetas :: Selector s => (Scope -> TType -> TcM s Expr) -> Expr -> TcM s Expr
generateForMetas :: (Scope -> TType -> TcM s Expr) -> Expr -> TcM s Expr
generateForMetas Scope -> TType -> TcM s Expr
prove Expr
e = do
(Expr
e,TType
_) <- Scope -> Expr -> TcM s (Expr, TType)
forall s. Scope -> Expr -> TcM s (Expr, TType)
infExpr Scope
emptyScope Expr
e
TcM s ()
fillinVariables
Expr -> TcM s Expr
forall s. Expr -> TcM s Expr
refineExpr Expr
e
where
fillinVariables :: TcM s ()
fillinVariables = do
[(Int, s, Scope, TType, [Expr -> TcM s ()])]
fvs <- (forall b.
Abstr
-> ([(Int, s, Scope, TType, [Expr -> TcM s ()])]
-> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s [(Int, s, Scope, TType, [Expr -> TcM s ()])]
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr [(Int, s, Scope, TType, [Expr -> TcM s ()])]
-> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> [(Int, s, Scope, TType, [Expr -> TcM s ()])]
-> MetaStore s -> s -> b -> b
k [(Int
i,s
s,Scope
scope,TType
tty,[Expr -> TcM s ()]
cs) | (Int
i,MUnbound s
s Scope
scope TType
tty [Expr -> TcM s ()]
cs) <- MetaStore s -> [(Int, MetaValue s)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList MetaStore s
ms] MetaStore s
ms)
case [(Int, s, Scope, TType, [Expr -> TcM s ()])]
fvs of
[] -> () -> TcM s ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(Int
i,s
_,Scope
scope,TType
tty,[Expr -> TcM s ()]
cs):[(Int, s, Scope, TType, [Expr -> TcM s ()])]
_ -> do Expr
e <- Scope -> TType -> TcM s Expr
prove Scope
scope TType
tty
Int -> MetaValue s -> TcM s ()
forall s. Int -> MetaValue s -> TcM s ()
setMeta Int
i (Expr -> MetaValue s
forall s. Expr -> MetaValue s
MBound Expr
e)
[TcM s ()] -> TcM s ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [Expr -> TcM s ()
c Expr
e | Expr -> TcM s ()
c <- [Expr -> TcM s ()]
cs]
TcM s ()
fillinVariables
generateForForest :: (Scope -> TType -> TcM FId Expr) -> Expr -> TcM FId Expr
generateForForest :: (Scope -> TType -> TcM Int Expr) -> Expr -> TcM Int Expr
generateForForest Scope -> TType -> TcM Int Expr
prove Expr
e = do
Expr -> TcM Int Expr
forall s. Expr -> TcM s Expr
refineExpr Expr
e
evalType :: Int -> TType -> TcM s Type
evalType :: Int -> TType -> TcM s Type
evalType Int
k (TTyp Env
delta Type
ty) = (Abstr
-> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double))
-> Int -> Env -> Type -> TcM s Type
forall t s. t -> Int -> Env -> Type -> TcM s Type
evalTy Abstr -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
funs Int
k Env
delta Type
ty
where
evalTy :: t -> Int -> Env -> Type -> TcM s Type
evalTy t
sig Int
k Env
delta (DTyp [Hypo]
hyps CId
cat [Expr]
es) = do
(Int
k,Env
delta,[Hypo]
hyps) <- t -> Int -> Env -> [Hypo] -> TcM s (Int, Env, [Hypo])
evalHypos t
sig Int
k Env
delta [Hypo]
hyps
[Expr]
es <- (Expr -> TcM s Expr) -> [Expr] -> TcM s [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\Expr
e -> Env -> Expr -> TcM s Value
forall s. Env -> Expr -> TcM s Value
eval Env
delta Expr
e TcM s Value -> (Value -> TcM s Expr) -> TcM s Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> Value -> TcM s Expr
forall s. Int -> Value -> TcM s Expr
value2expr Int
k) [Expr]
es
Type -> TcM s Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hyps CId
cat [Expr]
es)
evalHypos :: t -> Int -> Env -> [Hypo] -> TcM s (Int, Env, [Hypo])
evalHypos t
sig Int
k Env
delta [] = (Int, Env, [Hypo]) -> TcM s (Int, Env, [Hypo])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
k,Env
delta,[])
evalHypos t
sig Int
k Env
delta ((BindType
b,CId
x,Type
ty):[Hypo]
hyps) = do
Type
ty <- t -> Int -> Env -> Type -> TcM s Type
evalTy t
sig Int
k Env
delta Type
ty
(Int
k,Env
delta,[Hypo]
hyps) <- if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then t -> Int -> Env -> [Hypo] -> TcM s (Int, Env, [Hypo])
evalHypos t
sig Int
k Env
delta [Hypo]
hyps
else t -> Int -> Env -> [Hypo] -> TcM s (Int, Env, [Hypo])
evalHypos t
sig (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ((Int -> Env -> Value
VGen Int
k [])Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta) [Hypo]
hyps
(Int, Env, [Hypo]) -> TcM s (Int, Env, [Hypo])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
k,Env
delta,(BindType
b,CId
x,Type
ty) Hypo -> [Hypo] -> [Hypo]
forall a. a -> [a] -> [a]
: [Hypo]
hyps)
refineExpr :: Expr -> TcM s Expr
refineExpr :: Expr -> TcM s Expr
refineExpr Expr
e = (forall b.
Abstr
-> (Expr -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s Expr
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr Expr -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> Expr -> MetaStore s -> s -> b -> b
k (MetaStore s -> Expr -> Expr
forall s. IntMap (MetaValue s) -> Expr -> Expr
refineExpr_ MetaStore s
ms Expr
e) MetaStore s
ms)
refineExpr_ :: IntMap (MetaValue s) -> Expr -> Expr
refineExpr_ IntMap (MetaValue s)
ms Expr
e = Expr -> Expr
refine Expr
e
where
refine :: Expr -> Expr
refine (EAbs BindType
b CId
x Expr
e) = BindType -> CId -> Expr -> Expr
EAbs BindType
b CId
x (Expr -> Expr
refine Expr
e)
refine (EApp Expr
e1 Expr
e2) = Expr -> Expr -> Expr
EApp (Expr -> Expr
refine Expr
e1) (Expr -> Expr
refine Expr
e2)
refine (ELit Literal
l) = Literal -> Expr
ELit Literal
l
refine (EMeta Int
i) = case Int -> IntMap (MetaValue s) -> Maybe (MetaValue s)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap (MetaValue s)
ms of
Just (MBound Expr
e ) -> Expr -> Expr
refine Expr
e
Just (MGuarded Expr
e [Expr -> TcM s ()]
_ Int
_) -> Expr -> Expr
refine Expr
e
Maybe (MetaValue s)
_ -> Int -> Expr
EMeta Int
i
refine (EFun CId
f) = CId -> Expr
EFun CId
f
refine (EVar Int
i) = Int -> Expr
EVar Int
i
refine (ETyped Expr
e Type
ty) = Expr -> Type -> Expr
ETyped (Expr -> Expr
refine Expr
e) (IntMap (MetaValue s) -> Type -> Type
refineType_ IntMap (MetaValue s)
ms Type
ty)
refine (EImplArg Expr
e) = Expr -> Expr
EImplArg (Expr -> Expr
refine Expr
e)
refineType :: Type -> TcM s Type
refineType :: Type -> TcM s Type
refineType Type
ty = (forall b.
Abstr
-> (Type -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s Type
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr Type -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> Type -> MetaStore s -> s -> b -> b
k (MetaStore s -> Type -> Type
forall s. IntMap (MetaValue s) -> Type -> Type
refineType_ MetaStore s
ms Type
ty) MetaStore s
ms)
refineType_ :: IntMap (MetaValue s) -> Type -> Type
refineType_ IntMap (MetaValue s)
ms (DTyp [Hypo]
hyps CId
cat [Expr]
es) = [Hypo] -> CId -> [Expr] -> Type
DTyp [(BindType
b,CId
x,IntMap (MetaValue s) -> Type -> Type
refineType_ IntMap (MetaValue s)
ms Type
ty) | (BindType
b,CId
x,Type
ty) <- [Hypo]
hyps] CId
cat ((Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
List.map (IntMap (MetaValue s) -> Expr -> Expr
refineExpr_ IntMap (MetaValue s)
ms) [Expr]
es)
eval :: Env -> Expr -> TcM s Value
eval :: Env -> Expr -> TcM s Value
eval Env
env Expr
e = (forall b.
Abstr
-> (Value -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s Value
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr Value -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> Value -> MetaStore s -> s -> b -> b
k (Sig -> Env -> Expr -> Value
Expr.eval (Abstr -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
funs Abstr
abstr,MetaStore s -> Int -> Maybe Expr
forall s. IntMap (MetaValue s) -> Int -> Maybe Expr
lookupMeta MetaStore s
ms) Env
env Expr
e) MetaStore s
ms)
apply :: Env -> Expr -> [Value] -> TcM s Value
apply :: Env -> Expr -> Env -> TcM s Value
apply Env
env Expr
e Env
vs = (forall b.
Abstr
-> (Value -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s Value
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr Value -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> Value -> MetaStore s -> s -> b -> b
k (Sig -> Env -> Expr -> Env -> Value
Expr.apply (Abstr -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
funs Abstr
abstr,MetaStore s -> Int -> Maybe Expr
forall s. IntMap (MetaValue s) -> Int -> Maybe Expr
lookupMeta MetaStore s
ms) Env
env Expr
e Env
vs) MetaStore s
ms)
applyValue :: Value -> [Value] -> TcM s Value
applyValue :: Value -> Env -> TcM s Value
applyValue Value
v Env
vs = (forall b.
Abstr
-> (Value -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s Value
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr Value -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> Value -> MetaStore s -> s -> b -> b
k (Sig -> Value -> Env -> Value
Expr.applyValue (Abstr -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
funs Abstr
abstr,MetaStore s -> Int -> Maybe Expr
forall s. IntMap (MetaValue s) -> Int -> Maybe Expr
lookupMeta MetaStore s
ms) Value
v Env
vs) MetaStore s
ms)
value2expr :: Int -> Value -> TcM s Expr
value2expr :: Int -> Value -> TcM s Expr
value2expr Int
i Value
v = (forall b.
Abstr
-> (Expr -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s Expr
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr Expr -> MetaStore s -> s -> b -> b
k TcError -> s -> b -> b
h MetaStore s
ms -> Expr -> MetaStore s -> s -> b -> b
k (Sig -> Int -> Value -> Expr
Expr.value2expr (Abstr -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
funs Abstr
abstr,MetaStore s -> Int -> Maybe Expr
forall s. IntMap (MetaValue s) -> Int -> Maybe Expr
lookupMeta MetaStore s
ms) Int
i Value
v) MetaStore s
ms)