content: module TypeChecking.Definitions.Functions
      ( typeCheckFunction
      ) where
  
  import Data.Maybe
  import Data.Void
  
  import Syntax
  import Semantics
  import Semantics.Value
  import Semantics.Pattern as P
  import Syntax.ErrorDoc
  import TypeChecking.Monad
  import TypeChecking.Context as C
  import TypeChecking.Expressions
  import TypeChecking.Expressions.Utils
  import TypeChecking.Expressions.Patterns
  import TypeChecking.Expressions.Coverage
  import TypeChecking.Expressions.Conditions
  import TypeChecking.Definitions.Termination
  import Normalization
  
  typeCheckFunction :: Monad m => PName -> Term (Posn, Syntax) Void
      -> [(Posn, [Term PName Void], Maybe (Term (Posn, Syntax) Void))] -> TCM m ()
  typeCheckFunction p@(pos, name) ety clauses = do
      (ty, Type u _) <- typeCheck ety Nothing
      k <- case nf WHNF u of
              Apply (Semantics _ (Universe k)) _ -> return k
              u' -> throwError [Error TypeMismatch $ emsgLC (termPos ety) "" $ pretty "Expected a type"
                                                                            $$ pretty "Actual type:" <+> prettyOpen C.Nil u']
      let cty = closed (Type ty k)
      fcid <- addFunctionCheck p [] cty
      clausesAndPats <- forW clauses $ \(pos',pats,mexpr) ->  do
          (bf, TermsInCtx ctx rtpats _ ty') <- typeCheckPatterns C.Nil (Type (nf WHNF ty) k) pats
          case (bf,mexpr) of
              (True,  Nothing) -> return $ Just (Nothing, (pos', P.Clause rtpats $ error ""), error "")
              (False, Nothing) -> do
                  let msg = "The right hand side can be omitted only if the absurd pattern is given"
                  warn [Error Other $ emsgLC pos' msg enull]
                  return Nothing
              (True, Just expr) -> do
                  let msg = "If the absurd pattern is given the right hand side must be omitted"
                  warn [Error Other $ emsgLC (termPos expr) msg enull]
                  return $ Just (Nothing, (pos', P.Clause rtpats $ error ""), error "")
              (False, Just expr) -> do
                  (term, _) <- typeCheckCtx ctx expr $ Just (nfType WHNF ty')
                  return $ Just (Just (patternsToTerms rtpats, closed $ abstractTerm ctx term), (pos', P.Clause rtpats term), PatInCtx (Function fcid) (patternsToTermsVar rtpats) term)
      let clauses' = map (\(a,_,_) -> a) clausesAndPats >>= maybe [] return
          eval = map (fmap $ \(Closed scope) -> Closed $ replaceFunCalls fcid fc scope) clauses'
          fc = Closed $ capply $ Semantics (Name Prefix name) (FunCall fcid eval)
          termErrs = checkTermination pos $ clausesAndPats >>= \(ma,_,c) -> maybe [] (const [c]) ma
      warn termErrs
      lift $ replaceFunction name (if null termErrs then eval else []) cty
      case checkCoverage (map (\(_,b,_) -> b) clausesAndPats) of
          Nothing | length clausesAndPats /= length (filter (\(_,_,me) -> isJust me) clauses) -> return ()
          r -> warn (coverageErrorMsg pos r)
      warn $ checkConditions C.Nil (open fc) $ clausesAndPats >>= \(ma,b,_) -> maybe [] (const [b]) ma
  
  replaceFunCalls :: ID -> Closed (Term Semantics) -> Term Semantics a -> Term Semantics a
  replaceFunCalls name fc (Var a ts) = Var a $ map (replaceFunCalls name fc) ts
  replaceFunCalls name fc (Apply (Semantics _ (FunCall name' _)) ts) | name == name' = apps (open fc) ts
  replaceFunCalls name fc (Apply s ts) = Apply s $ map (replaceFunCalls name fc) ts
  replaceFunCalls name fc (Lambda t) = Lambda (replaceFunCalls name fc t)
  