----------------------------------------------------------------------
-- |
-- Module      : TypeCheck
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/09/15 16:22:02 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.16 $
--
-- (Description of the module)
-----------------------------------------------------------------------------

module GF.Compile.TypeCheck.Abstract (-- * top-level type checking functions; TC should not be called directly.
    checkContext,
    checkTyp,
    checkDef,
    checkConstrs,
   ) where

import GF.Data.Operations

import GF.Infra.CheckM
import GF.Grammar
import GF.Grammar.Lookup
import GF.Grammar.Unify
--import GF.Compile.Refresh
--import GF.Compile.Compute.Abstract
import GF.Compile.TypeCheck.TC

import GF.Text.Pretty
--import Control.Monad (foldM, liftM, liftM2)

-- | invariant way of creating TCEnv from context
initTCEnv :: [(Ident, b)] -> (Int, [(Ident, Val)], [(Ident, b)])
initTCEnv [(Ident, b)]
gamma =
  ([(Ident, b)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Ident, b)]
gamma,[(Ident
x,Int -> Ident -> Val
VGen Int
i Ident
x) | ((Ident
x,b
_),Int
i) <- [(Ident, b)] -> [Int] -> [((Ident, b), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Ident, b)]
gamma [Int
0..]], [(Ident, b)]
gamma)

-- interface to TC type checker

type2val :: Type -> Val
type2val :: Type -> Val
type2val = [(Ident, Val)] -> Type -> Val
VClos []

cont2exp :: Context -> Term
cont2exp :: Context -> Type
cont2exp Context
c = Context -> Type -> [Type] -> Type
mkProd Context
c Type
eType [] -- to check a context

cont2val :: Context -> Val
cont2val :: Context -> Val
cont2val = Type -> Val
type2val (Type -> Val) -> (Context -> Type) -> Context -> Val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Type
cont2exp

-- some top-level batch-mode checkers for the compiler

justTypeCheck :: SourceGrammar -> Term -> Val -> Err Constraints
justTypeCheck :: SourceGrammar -> Type -> Val -> Err Constraints
justTypeCheck SourceGrammar
gr Type
e Val
v = do
  (AExp
_,Constraints
constrs0) <- Theory -> TCEnv -> Type -> Val -> Err (AExp, Constraints)
checkExp (SourceGrammar -> Theory
grammar2theory SourceGrammar
gr) ([(Ident, Val)] -> TCEnv
forall b. [(Ident, b)] -> (Int, [(Ident, Val)], [(Ident, b)])
initTCEnv []) Type
e Val
v
  (Constraints
constrs1,MetaSubst
_) <- Constraints -> Err (Constraints, MetaSubst)
unifyVal Constraints
constrs0
  Constraints -> Err Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraints -> Err Constraints) -> Constraints -> Err Constraints
forall a b. (a -> b) -> a -> b
$ ((Val, Val) -> Bool) -> Constraints -> Constraints
forall a. (a -> Bool) -> [a] -> [a]
filter (Val, Val) -> Bool
notJustMeta Constraints
constrs1

notJustMeta :: (Val, Val) -> Bool
notJustMeta (Val
c,Val
k) = case (Val
c,Val
k) of
    (VClos [(Ident, Val)]
g1 (Meta Int
m1), VClos [(Ident, Val)]
g2 (Meta Int
m2)) -> Bool
False
    (Val, Val)
_ -> Bool
True

grammar2theory :: SourceGrammar -> Theory
grammar2theory :: SourceGrammar -> Theory
grammar2theory SourceGrammar
gr (ModuleName
m,Ident
f) = case SourceGrammar -> ModuleName -> Ident -> Err Type
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> ModuleName -> Ident -> m Type
lookupFunType SourceGrammar
gr ModuleName
m Ident
f of
  Ok Type
t -> Val -> Err Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ Type -> Val
type2val Type
t
  Bad String
s -> case SourceGrammar -> ModuleName -> Ident -> Err Context
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> ModuleName -> Ident -> m Context
lookupCatContext SourceGrammar
gr ModuleName
m Ident
f of
    Ok Context
cont -> Val -> Err Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ Context -> Val
cont2val Context
cont
    Err Context
_ -> String -> Err Val
forall a. String -> Err a
Bad String
s

checkContext :: SourceGrammar -> Context -> [Message]
checkContext :: SourceGrammar -> Context -> [Message]
checkContext SourceGrammar
st = SourceGrammar -> Type -> [Message]
checkTyp SourceGrammar
st (Type -> [Message]) -> (Context -> Type) -> Context -> [Message]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Type
cont2exp

checkTyp :: SourceGrammar -> Type -> [Message]
checkTyp :: SourceGrammar -> Type -> [Message]
checkTyp SourceGrammar
gr Type
typ = (String -> [Message])
-> (Constraints -> [Message]) -> Err Constraints -> [Message]
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err (\String
x -> [String -> Message
forall a. Pretty a => a -> Message
pp String
x]) Constraints -> [Message]
ppConstrs (Err Constraints -> [Message]) -> Err Constraints -> [Message]
forall a b. (a -> b) -> a -> b
$ SourceGrammar -> Type -> Val -> Err Constraints
justTypeCheck SourceGrammar
gr Type
typ Val
vType

checkDef :: SourceGrammar -> Fun -> Type -> Equation -> [Message]
checkDef :: SourceGrammar
-> (ModuleName, Ident) -> Type -> Equation -> [Message]
checkDef SourceGrammar
gr (ModuleName
m,Ident
fun) Type
typ Equation
eq = (String -> [Message])
-> (Constraints -> [Message]) -> Err Constraints -> [Message]
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err (\String
x -> [String -> Message
forall a. Pretty a => a -> Message
pp String
x]) Constraints -> [Message]
ppConstrs (Err Constraints -> [Message]) -> Err Constraints -> [Message]
forall a b. (a -> b) -> a -> b
$ do
  (([Type], AExp)
b,Constraints
cs) <- Theory
-> TCEnv -> Equation -> Val -> Err (([Type], AExp), Constraints)
checkBranch (SourceGrammar -> Theory
grammar2theory SourceGrammar
gr) ([(Ident, Val)] -> TCEnv
forall b. [(Ident, b)] -> (Int, [(Ident, Val)], [(Ident, b)])
initTCEnv []) Equation
eq (Type -> Val
type2val Type
typ)
  (Constraints
constrs,MetaSubst
_) <- Constraints -> Err (Constraints, MetaSubst)
unifyVal Constraints
cs
  Constraints -> Err Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraints -> Err Constraints) -> Constraints -> Err Constraints
forall a b. (a -> b) -> a -> b
$ ((Val, Val) -> Bool) -> Constraints -> Constraints
forall a. (a -> Bool) -> [a] -> [a]
filter (Val, Val) -> Bool
notJustMeta Constraints
constrs

checkConstrs :: SourceGrammar -> Cat -> [Ident] -> [String]
checkConstrs :: SourceGrammar -> (ModuleName, Ident) -> [Ident] -> [String]
checkConstrs SourceGrammar
gr (ModuleName, Ident)
cat [Ident]
_ = [] ---- check constructors!