----------------------------------------------------------------------
-- |
-- 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 gamma = 
  (length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma) 

-- interface to TC type checker

type2val :: Type -> Val
type2val = VClos []

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

cont2val :: Context -> Val
cont2val = type2val . cont2exp

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

justTypeCheck :: SourceGrammar -> Term -> Val -> Err Constraints
justTypeCheck gr e v = do
  (_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
  (constrs1,_) <- unifyVal constrs0
  return $ filter notJustMeta constrs1

notJustMeta (c,k) = case (c,k) of
    (VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
    _ -> True

grammar2theory :: SourceGrammar -> Theory
grammar2theory gr (m,f) = case lookupFunType gr m f of
  Ok t -> return $ type2val t
  Bad s -> case lookupCatContext gr m f of
    Ok cont -> return $ cont2val cont
    _ -> Bad s

checkContext :: SourceGrammar -> Context -> [Message]
checkContext st = checkTyp st . cont2exp

checkTyp :: SourceGrammar -> Type -> [Message]
checkTyp gr typ = err (\x -> [pp x]) ppConstrs $ justTypeCheck gr typ vType

checkDef :: SourceGrammar -> Fun -> Type -> Equation -> [Message]
checkDef gr (m,fun) typ eq = err (\x -> [pp x]) ppConstrs $ do
  (b,cs) <- checkBranch (grammar2theory gr) (initTCEnv []) eq (type2val typ)
  (constrs,_) <- unifyVal cs
  return $ filter notJustMeta constrs

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