{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, RankNTypes #-}

----------------------------------------------------------------------
-- |
-- Module      : PGF.TypeCheck
-- Maintainer  : Krasimir Angelov
-- Stability   : (stable)
-- Portability : (portable)
--
-- Type checking in abstract syntax with dependent types.
-- The type checker also performs renaming and checking for unknown
-- functions. The variable references are replaced by de Bruijn indices.
--
-----------------------------------------------------------------------------

module PGF.TypeCheck ( checkType, checkExpr, inferExpr

                     , ppTcError, TcError(..)

                     -- internals needed for the typechecking of forests
                     , 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) -- typeOfHypo
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.Identity
import Control.Monad.State
import Control.Monad.Except
import Text.PrettyPrint

-----------------------------------------------------
-- The Scope
-----------------------------------------------------

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)

-- | returns the type and the De Bruijn index of a local variable
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]

-- | returns the type and the name of a local variable
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

-----------------------------------------------------
-- The Monad
-----------------------------------------------------

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   -- the Int is the number of constraints that have to be solved 
                                                            -- to unlock this meta variable

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)

-----------------------------------------------------
-- Type errors
-----------------------------------------------------

-- | If an error occurs in the typechecking phase
-- the type checker returns not a plain text error message
-- but a 'TcError' structure which describes the error.
data TcError
  = UnknownCat      CId                            -- ^ Unknown category name was found.
  | UnknownFun      CId                            -- ^ Unknown function name was found.
  | WrongCatArgs    [CId] Type CId  Int Int        -- ^ A category was applied to wrong number of arguments.
                                                   -- The first integer is the number of expected arguments and
                                                   -- the second the number of given arguments.
                                                   -- The @[CId]@ argument is the list of free variables
                                                   -- in the type. It should be used for the 'showType' function.
  | TypeMismatch    [CId] Expr Type Type           -- ^ The expression is not of the expected type.
                                                   -- The first type is the expected type, while
                                                   -- the second is the inferred. The @[CId]@ argument is the list
                                                   -- of free variables in both the expression and the type. 
                                                   -- It should be used for the 'showType' and 'showExpr' functions.
  | NotFunType      [CId] Expr Type                -- ^ Something that is not of function type was applied to an argument.
  | CannotInferType [CId] Expr                     -- ^ It is not possible to infer the type of an expression.
  | UnresolvedMetaVars [CId] Expr [MetaId]         -- ^ Some metavariables have to be instantiated in order to complete the typechecking.
  | UnexpectedImplArg [CId] Expr                   -- ^ Implicit argument was passed where the type doesn't allow it
  | UnsolvableGoal [CId] MetaId Type               -- ^ There is a goal that cannot be solved
  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

-- | Renders the type checking error to a document. See 'Text.PrettyPrint'.
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
-----------------------------------------------------

-- | Check whether a given type is consistent with the abstract
-- syntax of the grammar.
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
-----------------------------------------------------

-- | Checks an expression against a specified type.
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
-----------------------------------------------------

-- | Tries to infer the type of a given expression. Note that
-- even if the expression is type correct it is not always
-- possible to infer its type in the GF type system.
-- In this case the function returns the 'CannotInferType' error.
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
-----------------------------------------------------

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)


-----------------------------------------------------------
-- three ways of dealing with meta variables that
-- still have to be resolved
-----------------------------------------------------------

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
--  fillinVariables
  Expr -> TcM Int Expr
forall s. Expr -> TcM s Expr
refineExpr Expr
e
{-
  where
    fillinVariables = do
      fvs <- TcM (\abstr k h ms -> k [(i,s,scope,tty,cs) | (i,MUnbound s scope tty cs) <- IntMap.toList ms] ms)
      case fvs of
        []                   -> return ()
        (i,s,scope,tty,cs):_ -> TcM (\abstr k h ms s0 ->
                                        case snd $ runTcM abstr (prove scope tty) ms s of
                                          []           -> unTcM (do ty <- evalType (scopeSize scope) tty
                                                                    throwError (UnsolvableGoal (scopeVars scope) s ty)
                                                                ) abstr k h ms s
                                          ((ms,_,e):_) -> unTcM (do setMeta i (MBound e)
                                                                    sequence_ [c e | c <- cs]
                                                                    fillinVariables
                                                                ) abstr k h ms s)
-}

-----------------------------------------------------
-- evalType
-----------------------------------------------------

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)


-----------------------------------------------------
-- refinement
-----------------------------------------------------

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)