~ubuntu-branches/ubuntu/raring/agda/raring-proposed

{-# LANGUAGE CPP #-}

 

module Agda.TypeChecking.Monad.Open

        ( makeOpen

        , makeClosed

        , getOpen

        , tryOpen

        ) where

 

import Control.Applicative

import Control.Monad

import Control.Monad.Error

import Data.List

 

import Agda.Syntax.Common

 

import Agda.TypeChecking.Substitute

import Agda.TypeChecking.Monad.Base

 

import {-# SOURCE #-} Agda.TypeChecking.Monad.Context

 

#include "../../undefined.h"

import Agda.Utils.Impossible

 

-- | Create an open term in the current context.

makeOpen :: MonadTCM tcm => a -> tcm (Open a)

makeOpen x = do

    ctx <- getContextId

    return $ OpenThing ctx x

 

-- | Create an open term which is closed.

makeClosed :: a -> Open a

makeClosed = OpenThing []

 

 

-- | Extract the value from an open term. Must be done in an extension of the

--   context in which the term was created.

getOpen :: (MonadTCM tcm, Raise a) => Open a -> tcm a

getOpen (OpenThing []  x) = return x

getOpen (OpenThing ctx x) = do

  ctx' <- getContextId

  unless (ctx `isSuffixOf` ctx') $ fail $ "thing out of context (" ++ show ctx ++ " is not a sub context of " ++ show ctx' ++ ")"

  return $ raise (genericLength ctx' - genericLength ctx) x

 

tryOpen :: (MonadTCM tcm, Raise a) => Open a -> tcm (Maybe a)

tryOpen o = liftTCM $

  (Just <$> getOpen o)

  `catchError` \_ -> return Nothing