content: {-|
  Module      : Idris.Elab.Type
  Description : Code to elaborate types.
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  {-# LANGUAGE PatternGuards #-}
  module Idris.Elab.Type (
      buildType, elabType, elabType'
    , elabPostulate, elabExtern
    ) where
  
  import Idris.AbsSyntax
  import Idris.ASTUtils
  import Idris.Core.Elaborate hiding (Tactic(..))
  import Idris.Core.Evaluate
  import Idris.Core.TT
  import Idris.Docstrings (Docstring)
  import Idris.Elab.Term
  import Idris.Elab.Utils
  import Idris.Elab.Value
  import Idris.Error
  import Idris.Options
  import Idris.Output (sendHighlighting)
  
  import Prelude hiding (id, (.))
  
  import Control.Category
  import Control.Monad
  import qualified Data.Set as S
  
  buildType :: ElabInfo
            -> SyntaxInfo
            -> FC
            -> FnOpts
            -> Name
            -> PTerm
            -> Idris (Type, Type, PTerm, [(Int, Name)])
  buildType info syn fc opts n ty' = do
           ctxt <- getContext
           i <- getIState
  
           logElab 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)
           ty' <- addUsingConstraints syn fc ty'
           ty' <- addUsingImpls syn n fc ty'
           let ty = addImpl (imp_methods syn) i ty'
  
           logElab 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
           logElab 5 $ "with methods " ++ show (imp_methods syn)
           logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
  
           ((ElabResult tyT' defer is ctxt' newDecls highlights newGName, est), log) <-
              tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState
                       (errAt "type of " n Nothing
                          (erunAux fc (build i info ETyDecl [] n ty)))
  
           displayWarnings est
           setContext ctxt'
           processTacticDecls info newDecls
           sendHighlighting highlights
           updateIState $ \i -> i { idris_name = newGName }
  
           let tyT = patToImp tyT'
  
           logElab 3 $ show ty ++ "\nElaborated: " ++ show tyT'
  
           ds <- checkAddDef True False info fc iderr True defer
           -- if the type is not complete, note that we'll need to infer
           -- things later (for solving metavariables)
           when (length ds > length is) -- more deferred than case blocks
                $ addTyInferred n
  
           mapM_ (elabCaseBlock info opts) is
           ctxt <- getContext
           logElab 5 "Rechecking"
           logElab 6 (show tyT)
           logElab 10 $ "Elaborated to " ++ showEnvDbg [] tyT
           (cty, ckind)   <- recheckC (constraintNS info) fc id [] tyT
  
           -- record the implicit and inaccessible arguments
           i <- getIState
           let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty
           let inacc = inaccessibleImps 0 cty inaccData
           logElab 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++
                       " from " ++ show cty ++ "\n" ++ showTmImpls ty
  
           putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }
           logElab 3 ("Implicit " ++ show n ++ " " ++ show impls)
           addIBC (IBCImp n)
  
           -- Add the names referenced to the call graph, and check we're not
           -- referring to anything less visible
           -- In particular, a public/export type can not refer to anything
           -- private, but can refer to any public/export
           let refs = freeNames cty
           nvis <- getFromHideList n
           case nvis of
                Nothing -> return ()
                Just acc -> mapM_ (checkVisibility fc n (max Frozen acc) acc) refs
           addCalls n refs
           addIBC (IBCCG n)
  
           when (Constructor `notElem` opts) $ do
               let pnames = getParamsInType i [] impls cty
               let fninfo = FnInfo (param_pos 0 pnames cty)
               setFnInfo n fninfo
               addIBC (IBCFnInfo n fninfo)
  
           return (cty, ckind, ty, inacc)
    where
      patToImp (Bind n (PVar rig t) sc) = Bind n (Pi rig Nothing t (TType (UVar [] 0))) (patToImp sc)
      patToImp (Bind n b sc) = Bind n b (patToImp sc)
      patToImp t = t
  
      param_pos i ns (Bind n (Pi _ _ t _) sc)
          | n `elem` ns = i : param_pos (i + 1) ns sc
          | otherwise = param_pos (i + 1) ns sc
      param_pos i ns t = []
  
  -- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
  elabType :: ElabInfo
           -> SyntaxInfo
           -> Docstring (Either Err PTerm)
           -> [(Name, Docstring (Either Err PTerm))]
           -> FC
           -> FnOpts
           -> Name
           -> FC -- ^ The precise location of the name
           -> PTerm
           -> Idris Type
  elabType = elabType' False
  
  elabType' :: Bool  -- normalise it
            -> ElabInfo
            -> SyntaxInfo
            -> Docstring (Either Err PTerm)
            -> [(Name, Docstring (Either Err PTerm))]
            -> FC
            -> FnOpts
            -> Name
            -> FC
            -> PTerm
            -> Idris Type
  elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (params info) ty_in
                                                         n  = liftname info n_in in    -}
        do checkUndefined fc n
           (cty, _, ty, inacc) <- buildType info syn fc opts n ty'
  
           addStatics n cty ty
           let nty = cty -- normalise ctxt [] cty
           -- if the return type is something coinductive, freeze the definition
           ctxt <- getContext
           logElab 2 $ "Rechecked to " ++ show nty
           let nty' = normalise ctxt [] nty
           logElab 2 $ "Rechecked to " ++ show nty'
  
           -- Add function name to internals (used for making :addclause know
           -- the name unambiguously)
           i <- getIState
           rep <- useREPL
           when rep $ do
             addInternalApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty') -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
           addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))
  
           let (fam, _) = unApply (getRetTy nty')
           -- Productivity checking now via checking for guarded 'Delay'
           let opts' = opts -- if corec then (Coinductive : opts) else opts
           let usety = if norm then nty' else nty
           ds <- checkDef info fc iderr True [(n, (-1, Nothing, usety, []))]
           addIBC (IBCDef n)
           addDefinedName n
           let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True, True))) ds
           addDeferred ds'
           setFlags n opts'
           checkDocs fc argDocs ty
           doc' <- elabDocTerms info doc
           argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
                                           return (n, d')) argDocs
           addDocStr n doc' argDocs'
           addIBC (IBCDoc n)
           addIBC (IBCFlags n)
           fputState (opt_inaccessible . ist_optimisation n) inacc
           addIBC (IBCOpt n)
           when (Implicit `elem` opts') $ do addCoercion n
                                             addIBC (IBCCoercion n)
           when (AutoHint `elem` opts') $
               case fam of
                  P _ tyn _ -> do addAutoHint tyn n
                                  addIBC (IBCAutoHint tyn n)
                  t -> ifail "Hints must return a data or record type"
  
           -- If the function is declared as an error handler and the language
           -- extension is enabled, then add it to the list of error handlers.
           errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
           when (ErrorHandler `elem` opts) $ do
             if errorReflection
               then
                 -- Check that the declared type is the correct type for an error handler:
                 -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt
                 if tyIsHandler nty'
                   then do i <- getIState
                           putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }
                           addIBC (IBCErrorHandler n)
                   else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
               else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
           -- Send highlighting information about the name being declared
           sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)]
           -- if it's an export list type, make a note of it
           case (unApply usety) of
                (P _ ut _, _)
                   | ut == ffiexport -> do addIBC (IBCExport n)
                                           addExport n
                _ -> return ()
           return usety
    where
      ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]
  
      err = txt "Err"
      maybe = txt "Maybe"
      lst = txt "List"
      errrep = txt "ErrorReportPart"
  
      tyIsHandler (Bind _ (Pi _ _ (P _ (NS (UN e) ns1) _) _)
                          (App _ (P _ (NS (UN m) ns2) _)
                               (App _ (P _ (NS (UN l) ns3) _)
                                    (P _ (NS (UN r) ns4) _))))
          | e == err && m == maybe && l == lst && r == errrep
          , ns1 == map txt ["Errors","Reflection","Language"]
          , ns2 == map txt ["Maybe", "Prelude"]
          , ns3 == map txt ["List", "Prelude"]
          , ns4 == map txt ["Reflection","Language"] = True
      tyIsHandler _                                           = False
  
  elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->
                   FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()
  elabPostulate info syn doc fc nfc opts n ty = do
      elabType info syn doc [] fc opts n NoFC ty
      putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState
      addIBC (IBCPostulate n)
      sendHighlighting $ S.fromList [(FC' nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]
  
      -- remove it from the deferred definitions list
      solveDeferred fc n
  
  elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->
                   FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()
  elabExtern info syn doc fc nfc opts n ty = do
      cty <- elabType info syn doc [] fc opts n NoFC ty
      ist <- getIState
      let arity = length (getArgTys (normalise (tt_ctxt ist) [] cty))
  
      putIState . (\ist -> ist{ idris_externs = S.insert (n, arity) (idris_externs ist) }) =<< getIState
      addIBC (IBCExtern (n, arity))
  
      -- remove it from the deferred definitions list
      solveDeferred fc n
  