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

{-# LANGUAGE PatternGuards #-}

 

module Agda.TypeChecking.Rules.Def where

import Control.Arrow ((***))

import Control.Applicative

import Control.Monad.State hiding (forM, mapM)

 

import Data.Function

import Data.List hiding (sort)

import Agda.TypeChecking.CompiledClause.Compile

 

import Agda.TypeChecking.Rules.Term                ( checkExpr, inferExpr, inferExprForWith, checkDontExpandLast, checkTelescope_, ConvColor(..) )

import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl ( checkDecls )

 

import Agda.Utils.Size

import Agda.Utils.Permutation

import Agda.Utils.Monad

 

import Agda.Utils.Impossible

 

---------------------------------------------------------------------------

                      , funTerminates     = Nothing

                      , funExtLam         = Nothing

                      , funWith           = Nothing

                      }

  reportSDoc "tc.def.alias" 20 $ text "checkAlias: leaving"

 

              ]

 

        -- Add the definition

             Function

             { funClauses        = cs

             , funCompiled       = Just cc

             , funTerminates     = Nothing

             , funExtLam         = extlam

             , funWith           = with

             }

 

        -- Andreas 2012-02-13: postpone polarity computation until after positivity check

    where

        npats = size . clausePats

 

 

-- | Insert some patterns in the in with-clauses LHS of the given RHS

insertPatterns :: [A.Pattern] -> A.RHS -> A.RHS

insertPatterns pats (A.WithRHS aux es cs) = A.WithRHS aux es (map insertToClause cs)

    where insertToClause (A.Clause (A.LHS i lhscore ps) rhs ds)

              = A.Clause (A.LHS i lhscore (pats ++ ps)) (insertPatterns pats rhs) ds

insertPatterns pats (A.RewriteRHS qs eqs rhs wh) = A.RewriteRHS qs eqs (insertPatterns pats rhs) wh

insertPatterns pats rhs = rhs

    }

 

-- | Type check a function clause.

checkClause :: Type -> A.SpineClause -> TCM Clause

checkClause t c@(A.Clause (A.SpineLHS i x aps withPats) rhs0 wh) = do

    unless (null withPats) $

      typeError $ UnexpectedWithPatterns withPats

    traceCall (CheckClause t c) $ do

    aps <- (traverse . traverse . traverse) expandPatternSynonyms aps

      -- Note that we might now be in irrelevant context,

      -- in case checkLeftHandSide walked over an irrelevant projection pattern.

      let mkBody v = foldr (\x t -> Bind $ Abs x t) (Body $ applySubst sub v) xs

                          -- 1. rewriting with a reflexive equality to happen rarely,

                          -- 2. especially with ?-holes in the rewrite expression

                          -- 3. and a large overall number of ?s.

                          when (sameIP st st') $ put st

                          handleRHS $ A.RewriteRHS names eqs rhs wh

 

                     equality <- primEqualityName

                     Con reflCon [] <- ignoreSharing <$> primRefl

 

                     -- Check that the type is actually an equality (lhs ≡ rhs)

                     -- and extract lhs, rhs, and their type.

 

                                    -- is defined by induction on eqs.

                                    (A.RewriteRHS names eqs (insertPatterns pats rhs) inner)

                                    outer]

                     reportSDoc "tc.rewrite.top" 25 $ vcat

                                         [ text "rewrite"

                                         , text "  from  = " <+> prettyTCM rewriteFromExpr

                    ]

                  reportSDoc "tc.with.top" 30 $

                    prettyA c

                  -- Infer the types of the with expressions

                  (vs, as)  <- normalise (vs0, as)

 

                  -- Split the telescope into the part needed to type the with arguments

                  -- and all the other stuff

                  let fv = allVars $ freeVars (vs, as)

                    ]

 

                  -- Create the body of the original function

                  -- All the context variables

                  us <- getContextArgs

                      -- First the variables bound outside this definition

                      (us0, us1') = genericSplitAt (n - m) us

                      -- Then permute the rest and grab those needed to for the with arguments

                  -- and Δ₁ ⊢ vs : as

                  (vs, as) <- do

                    let -- We know that as does not depend on Δ₂

                    return $ applySubst rho $ renameP (reverseP perm') (vs, as)

 

 

                  -- Andreas, 2013-02-26 add with-name to signature for printing purposes

 

                  -- Andreas, 2013-02-26 separate msgs to see which goes wrong

                  reportSDoc "tc.with.top" 20 $

                  reportSDoc "tc.with.top" 20 $

                    text "              body" <+> (addCtxTel delta $ prettyTCM $ mkBody v)

 

                  gamma <- maybe (typeError $ NotImplemented "with clauses for functions with unfolding arity") return mgamma

                  return (mkBody v, WithFunction x aux gamma delta1 delta2 vs as t' ps perm' perm finalPerm cs)

          in handleRHS rhs0

               , clauseBody      = body

               , clauseType      = Just trhs

               }

 

checkWithFunction :: WithFunctionProblem -> TCM ()

checkWithFunction NoWithFunction = return ()

  reportSLn "tc.with.top" 20 "created with display form"

 

  -- Generate the type of the with function

  candidateType <- withFunctionType delta1 vs as delta2 b

  reportSDoc "tc.with.type" 10 $ sep [ text "candidate type:", nest 2 $ prettyTCM candidateType ]

  reportSDoc "tc.with.type" 50 $ sep [ text "candidate type:", nest 2 $ text $ show candidateType ]

      , prettyList $ map prettyTCM ts

      , prettyTCM dt

      ]

  -- solveSizeConstraints -- Andreas, 2012-10-16 does not seem necessary

 

  reportSDoc "tc.with.top" 10 $ sep

    A.ConP _ _ ps -> any (containsAbsurdPattern . namedArg) ps

    A.DefP _ _ _  -> False  -- projection pattern

    A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- False