~ubuntu-branches/ubuntu/wily/agda/wily-proposed

{-# LANGUAGE TypeSynonymInstances #-}

 

module Agda.TypeChecking.Conversion where

import Control.Monad

import Control.Monad.Reader

import Control.Monad.State

 

import Data.List hiding (sort)

import qualified Data.List as List

 

import Agda.Interaction.Options

 

import Agda.Utils.Functor (($>))

import Agda.Utils.Monad

import Agda.Utils.Maybe

 

import Agda.Utils.Impossible

 

{- MOVED to TypeChecking.Level

sameVars :: Elims -> Elims -> Bool

sameVars xs ys = and $ zipWith same xs ys

    where

        same _ _ = False

 

-- | @intersectVars us vs@ checks whether all relevant elements in @us@ and @vs@

        "shortcut successful\n  result: " ++ show u

    -- Should be ok with catchError_ but catchError is much safer since we don't

    -- rethrow errors.

 

unifyPointers _ _ _ action = action

-- unifyPointers cmp _ _ action | cmp /= CmpEq = action

-- unifyPointers _ u v action = do

          isrec <- isEtaRecord r

          if isrec

            then do

              let ps = fromMaybe __IMPOSSIBLE__ $ allApplyElims es

              -- Andreas, 2010-10-11: allowing neutrals to be blocked things does not seem

              -- to change Agda's behavior

              --    isNeutral Blocked{}          = False

                  isNeutral = isNeutral' . fmap ignoreSharing

                  isMeta    = isMeta'    . fmap ignoreSharing

              -- Andreas, 2013-09-18: this is expensive:

              -- should only do this when copatterns are on

                  isMeta' (NotBlocked MetaV{})  = True

                  isMeta' _                     = False

 

              reportSDoc "tc.conv.term" 30 $ prettyTCM a <+> text "is eta record type"

              m <- reduceB m

              n <- reduceB n

              case (m, n) of

                _ | isMeta m || isMeta n ->

                    compareAtom cmp a' (ignoreBlocking m) (ignoreBlocking n)

 

                    -- Andreas 2011-03-23: (fixing issue 396)

                    -- if we are dealing with a singleton record,

                    -- we can succeed immediately

 

          addCtx name dom1 $

            if dependent

-}

  where

    -- Andreas, 2011-05-10 better report message about types

    -- if a PatternErr is thrown, rebuild constraint!

    catchConstraint (ValueCmp cmp t m n) $ do

      reportSDoc "tc.conv.atom" 50 $

                                    , prettyTCM n

                                    , text ":" <+> prettyTCM t ]

      -- Andreas: what happens if I cut out the eta expansion here?

      -- Answer: Triggers issue 245, does not resolve 348

 

      -- constructorForm changes literal to constructors

      -- only needed if the other side is not a literal

      (mb'', nb'') <- case (ignoreSharing $ ignoreBlocking mb', ignoreSharing $ ignoreBlocking nb') of

        _ -> (,) <$> traverse constructorForm mb'

                 <*> traverse constructorForm nb'

 

            n <- normalise n    -- is this what we want?

            m <- normalise m

            if m == n

                else postpone

 

          dir = fromCmp cmp

      unifyPointers cmp (ignoreBlocking mb') (ignoreBlocking nb') $ do    -- this needs to go after eta expansion to avoid creating infinite terms

 

      reportSDoc "tc.conv.atom" 30 $

                                    , prettyTCM nb

                                    , text ":" <+> prettyTCM t ]

      case (ignoreSharing <$> mb, ignoreSharing <$> nb) of

                -- instantiate later meta variables first

                let (solve1, solve2)

                      | (p1,x) > (p2,y) = (l,r)

                      where l = assign dir x xArgs n

                            r = assign rid y yArgs m

 

                    try m h = m `catchError_` \err -> case err of

                      _            -> throwError err

 

                -- First try the one with the highest priority. If that doesn't

                try solve1 solve2

 

        -- one side a meta, the other an unblocked term

        (Blocked{}, _)    -> useInjectivity cmp t m n

        (_,Blocked{})     -> useInjectivity cmp t m n

        _ -> do

          m <- elimView False m

          n <- elimView False n

          case (ignoreSharing m, ignoreSharing n) of

                -- Variables are invariant in their arguments

            (Def f es, Def f' es') | f == f' -> do

                a   <- defType <$> getConstInfo f

                pol <- getPolarity' cmp f

                    reportSLn "tc.conv.elim" 50 $ "v (raw) = " ++ show v

                    compareElims pol a v els1 els2

-}

                    -- Get the type of the constructor instantiated to the datatype parameters.

                    a' <- conType x t

                    -- Constructors are invariant in their arguments

            _ -> impossible

-}

        equalFun t1 t2 = case (ignoreSharing t1, ignoreSharing t2) of

            -- Andreas 2010-09-21 compare r1 and r2, but ignore forcing annotations!

                                        (ignoreForced $ argInfoRelevance i1))

                -> typeError $ UnequalRelevance cmp t1 t2

                reportSDoc "tc.conv.fun" 20 $ nest 2 $ vcat

                  [ text "t1 =" <+> prettyTCM t1

                  , text "t2 =" <+> prettyTCM t2 ]

                  then guardConstraint conCoDom checkDom

                  else checkDom >> solveConstraint_ conCoDom

-}

 

compareRelevance :: Comparison -> Relevance -> Relevance -> Bool

compareRelevance CmpEq  = (==)

compareType cmp ty1@(El s1 a1) ty2@(El s2 a2) =

    verboseBracket "tc.conv.type" 20 "compareType" $

    catchConstraint (TypeCmp cmp ty1 ty2) $ do

          [ text "compareType" <+> sep [ prettyTCM ty1 <+> prettyTCM cmp

                                       , prettyTCM ty2 ]

          , hsep [ text "   sorts:", prettyTCM s1, text " and ", prettyTCM s2 ]

          ]

-- Andreas, 2011-4-27 should not compare sorts, but currently this is needed

-- for solving sort and level metas

          TypeError _ e -> do

            reportSDoc "tc.conv.type" 30 $ vcat

              [ text "sort comparison failed"

                -- throwError err

                compareSort CmpEq s1 s2

          _             -> throwError err

 

leqType :: Type -> Type -> TCM ()

leqType = compareType CmpLeq

leqSort s1 s2 =

  ifM typeInType (return ()) $

    catchConstraint (SortCmp CmpLeq s1 s2) $

        let postpone = addConstraint (SortCmp CmpLeq s1 s2)

        reportSDoc "tc.conv.sort" 30 $

          sep [ text "leqSort"

              , nest 2 $ fsep [ prettyTCM s1 <+> text "=<"

                              , prettyTCM s2 ]

              ]

 

            (Type a, Type b) -> leqLevel a b

 

 

 

            (_       , Inf     )             -> return ()

            (Inf     , _       )             -> equalSort s1 s2

            (DLub{}  , _       )             -> postpone

            (_       , DLub{}  )             -> postpone

    where

 

leqLevel :: Level -> Level -> TCM ()

leqLevel a b = liftTCM $ do

                                     , text (show s2) ]

                     ]

              ]

 

            (Type a  , Type b  ) -> equalLevel a b

 

 

            (Inf     , Inf     )             -> return ()

            (Inf     , Type (Max as@(_:_)))  -> mapM_ (isInf $ notEq s1 s2) as

            (DLub{}  , _       )             -> postpone

            (_       , DLub{}  )             -> postpone

    where

 

        isInf notok ClosedLevel{} = notok

        isInf notok (Plus _ l) = case l of