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

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

 

module Agda.TypeChecking.Rules.LHS.Unify where

 

import Control.Arrow ((***))

import Control.Applicative hiding (empty)

import Control.Monad.State

import Control.Monad.Reader

import Control.Monad.Writer (WriterT(..), MonadWriter(..), Monoid(..))

 

import Data.Map (Map)

import qualified Data.Map as Map

 

import Data.Typeable (Typeable)

import Data.Foldable (Foldable)

import Agda.Interaction.Options (optInjectiveTypeConstructors)

 

import Agda.Syntax.Common

import Agda.Syntax.Literal

import Agda.Syntax.Position

 

import Agda.TypeChecking.DropArgs

import Agda.TypeChecking.Level (reallyUnLevelView)

import Agda.TypeChecking.Reduce

import Agda.TypeChecking.Substitute hiding (Substitution)

import qualified Agda.TypeChecking.Substitute as S

import Agda.TypeChecking.Telescope

import Agda.TypeChecking.Rules.LHS.Problem

-- import Agda.TypeChecking.SyntacticEquality

 

import Agda.Utils.Maybe

import Agda.Utils.Size

 

import Agda.Utils.Impossible

 

newtype Unify a = U { unUnify :: ReaderT UnifyEnv (WriterT UnifyOutput (ExceptionT UnifyException (StateT UnifyState TCM))) a }

instance HasConstInfo Unify where

  getConstInfo = U . lift . lift . lift . lift . getConstInfo

 

data UnifyMayPostpone = MayPostpone | MayNotPostpone

 

type UnifyEnv = UnifyMayPostpone

 

noPostponing :: Unify a -> Unify a

 

askPostpone :: Unify UnifyMayPostpone

 

-- | Output the result of unification (success or maybe).

type UnifyOutput = Unifiable

 

-- | Were two terms unifiable or did we have to postpone some equation such that we are not sure?

data Unifiable

  = Definitely  -- ^ Unification succeeded.

    Possibly ->   e

 

data Equality = Equal TypeHH Term Term

 

data UnifyException

  = ConstructorMismatch Type Term Term

  noMsg  = strMsg ""

  strMsg = GenericUnifyException

 

 

 

-- | Throw-away error message.

projectionMismatch :: QName -> QName -> Unify a

  applySubst rho (Equal a s t) =

    Equal (applySubst rho a) (applySubst rho s) (applySubst rho t)

 

 

modSub :: (Sub -> Sub) -> Unify ()

modSub f = U $ modify $ \s -> s { uniSub = f $ uniSub s }

i |-> (u, a) = do

  occursCheck i u a

  liftTCM $ reportSDoc "tc.lhs.unify.assign" 15 $ prettyTCM (var i) <+> text ":=" <+> prettyTCM u

  -- Apply substitution to itself (issue 552)

  rho' <- traverse ureduce rho

  modSub $ const rho'

 

makeSubstitution :: Sub -> S.Substitution

makeSubstitution sub

  where

 

-- | Apply the current substitution on a term and reduce to weak head normal form.

class UReduce t where

 

instance UReduce Term where

  ureduce u = doEtaContractImplicit $ do

-- Andreas, 2013-10-24 the following call to 'normalise' is problematic

-- (see issue 924).  Instead, we only normalize if unifyAtomHH is undecided.

--    liftTCM $ etaContract =<< normalise (applySubst rho u)

    instantiate :: Nat -> Substitution -> Substitution

    instantiate i s = map (fmap $ inst i u) s

      where

 

    inst :: Nat -> Term -> Term -> Term

    inst i u v = applySubst us v

      where us = [var j | j <- [0..i - 1] ] ++# u :# raiseS (i + 1)

 

 

-- | Are we in a homogeneous (one type) or heterogeneous (two types) situation?

data HomHet a

      Right _                               -> do

        checkEqualities $ applySubst (makeSubstitution s) eqs

        let n = maximum $ (-1) : flex'

  `catchError` \err -> case err of

     TypeError _ (Closure {clValue = WithoutKError{}}) -> throwError err

     _                                                 -> return $ DontKnow err

    unifyConstructorArgs a12 vs1 vs2 = do

      liftTCM $ reportSDoc "tc.lhs.unify" 15 $ sep

        [ text "unifyConstructorArgs"

        , nest 2 $ text "constructor type:" <+> prettyTCM a12

        ]

      let n = genericLength vs1

    unifyConArgs tel0@(ExtendTel a@(Dom _ bHH) tel) us0@(arg@(Arg _ u) : us) vs0@(Arg _ v : vs) = do

      liftTCM $ reportSDoc "tc.lhs.unify" 15 $ sep

        [ text "unifyConArgs"

        ]

      liftTCM $ reportSDoc "tc.lhs.unify" 25 $

        (text $ "tel0 = " ++ show tel0)

    unifyElims a us0@(Apply arg@(Arg _ u) : us) vs0@(Apply (Arg _ v) : vs) = do

      liftTCM $ reportSDoc "tc.lhs.unify" 15 $ sep

        [ text "unifyElims"

        ]

      a <- ureduce a  -- Q: reduce sufficient?

      case ignoreSharing $ unEl a of

          -- Andreas, Ulf, 2011-09-08 (AIM XVI)

          -- in case of dependent function type, we cannot postpone

          -- unification of u and v, otherwise us or vs might be ill-typed

          let dep = dependent $ unEl a

          -- skip irrelevant parts

            (if dep then noPostponing else id) $

              unify (unDom b) u v

          arg <- traverse ureduce arg

      where dependent (Pi _ NoAbs{}) = False

            dependent (Pi b c)       = 0 `relevantIn` absBody c

            dependent (Shared p)     = dependent (derefPtr p)

    unifyArgs a us0@(arg@(Arg _ u) : us) vs0@(Arg _ v : vs) = do

      liftTCM $ reportSDoc "tc.lhs.unify" 15 $ sep

        [ text "unifyArgs"

        ]

      a <- ureduce a  -- Q: reduce sufficient?

      case ignoreSharing $ unEl a of

          -- Andreas, Ulf, 2011-09-08 (AIM XVI)

          -- in case of dependent function type, we cannot postpone

          -- unification of u and v, otherwise us or vs might be ill-typed

          let dep = dependent $ unEl a

          -- skip irrelevant parts

            (if dep then noPostponing else id) $

              unify (unDom b) u v

          arg <- traverse ureduce arg

      where dependent (Pi _ NoAbs{}) = False

            dependent (Pi b c)       = 0 `relevantIn` absBody c

            dependent (Shared p)     = dependent (derefPtr p)

     -> Term -> Term -> Unify ()

    unifyHH aHH u v = do

      liftTCM $ reportSDoc "tc.lhs.unify" 15 $

      u <- liftTCM . constructorForm =<< ureduce u

      v <- liftTCM . constructorForm =<< ureduce v

      aHH <- ureduce aHH

      liftTCM $ reportSDoc "tc.lhs.unify" 25 $

      -- obtain the (== Size) function

      isSizeName <- liftTCM isSizeNameTest

 

          (|->?) = maybeAssign fallback

 

      liftTCM $ reportSDoc "tc.lhs.unify" 15 $

            , nest 2 $ text "=?="

      liftTCM $ reportSDoc "tc.lhs.unify" 60 $

        text $ "aHH = " ++ show aHH

      case (ignoreSharing u, ignoreSharing v) of

        (_, Level l) -> do

            v <- liftTCM $ reallyUnLevelView l

            unifyAtomHH aHH u v tryAgain

-- Andreas, 2013-03-05: the following flex/flex case is an attempt at

-- better dotting (see Issue811).  Does not work perfectly, maybe the best choice

-- which variable to assign cannot made locally, but would need a look at the full

            -- (in this order, see Problem.hs).

            -- The comparison is total.

            if fj >= fi then j |->? (u, a) else i |->? (v, a)

          | c == c' -> do

              r <- liftTCM (dataOrRecordTypeHH' c aHH)

              case r of

                Nothing -> checkEqualityHH aHH u v

          | otherwise -> constructorMismatchHH aHH u v

        -- Definitions are ok as long as they can't reduce (i.e. datatypes/axioms)

          | d == d' -> do

              -- d must be a data, record or axiom

              def <- getConstInfo d

            if ok then unify a u v

                  else addEquality a u v

 

           md <- isEtaRecordTypeHH aHH

           case md of

             Just (d, parsHH) -> do

               unifyConstructorArgs bHH us vs

             Nothing -> fallback

 

           md <- isEtaRecordTypeHH aHH

           case md of

             Just (d, parsHH) -> do

 

        -- Andreas, 2011-05-30: If I put checkEquality below, then Issue81 fails

        -- because there are definitions blocked by flexibles that need postponement

 

 

    unify :: Type -> Term -> Term -> Unify ()