packages feed

Agda 2.4.0 → 2.4.0.1

raw patch · 49 files changed

+656/−326 lines, 49 filesdep ~Agda

Dependency ranges changed: Agda

Files

Agda.cabal view
@@ -1,5 +1,5 @@ name:            Agda-version:         2.4.0+version:         2.4.0.1 cabal-version:   >= 1.8 build-type:      Custom license:         OtherLicense@@ -49,13 +49,14 @@                     lib/prim/Agda/Primitive.agda  source-repository head-  type:     darcs-  location: http://code.haskell.org/Agda/+  type:     git+  location: https://github.com/agda/agda.git  source-repository this-  type:     darcs-  location: http://code.haskell.org/Agda/-  tag:      2.4.0+  type:     git+  location: https://github.com/agda/agda.git+  branch:   maint-2.4.0+  tag:      2.4.0.1  flag epic   default: False@@ -410,7 +411,7 @@ executable agda   hs-source-dirs: src/main   main-is:        Main.hs-  build-depends:  Agda == 2.4.0,+  build-depends:  Agda == 2.4.0.1,                   -- Nothing is used from the following package, except                   -- for the prelude.                   base >= 3 && < 6
CHANGELOG view
@@ -1,4 +1,16 @@ ------------------------------------------------------------------------+-- Release notes for Agda 2 version 2.4.0.1+------------------------------------------------------------------------++Important changes since 2.4.0:++* The option --compile-no-main has been renamed to --no-main.++* COMPILED_DATA pragmas can now be given for records.++* Various bug fixes.++------------------------------------------------------------------------ -- Release notes for Agda 2 version 2.4.0 ------------------------------------------------------------------------ @@ -105,7 +117,23 @@ Language ======== -TODO: Document quoteContext.+* Experimental feature: quoteContext+  +  There is a new keyword 'quoteContext' that gives users access to the+  list of names in the current local context. For instance:++    open import Data.Nat+    open import Data.List+    open import Reflection++    foo : ℕ → ℕ → ℕ+    foo 0 m = 0+    foo (suc n) m = quoteContext xs in ?++  In the remaining goal, the list xs will consist of two names, n and+  m, corresponding to the two local variables. At the moment it is not+  possible to access let bound variables -- this feature may be added+  in the future.  * Experimental feature: Varying arity.   Function clauses may now have different arity, e.g.,
src/data/emacs-mode/agda2-highlight.el view
@@ -85,51 +85,54 @@         (cond          ((equal group 'conor)           '((agda2-highlight-keyword-face-             :underline t)-            (agda2-highlight-string-face)-            (agda2-highlight-number-face)-            (agda2-highlight-symbol-face)+             :bold t)+            (agda2-highlight-string-face+             :foreground "firebrick3")+            (agda2-highlight-number-face+             :foreground "firebrick3")+            (agda2-highlight-symbol-face+             :foreground "grey25")             (agda2-highlight-primitive-type-face-             :foreground "blue")+             :foreground "medium blue")             (agda2-highlight-bound-variable-face              :foreground "purple")             (agda2-highlight-inductive-constructor-face-             :foreground "dark red")+             :foreground "firebrick3")             (agda2-highlight-coinductive-constructor-face-             :foreground "dark red")+             :foreground "firebrick3")             (agda2-highlight-datatype-face-             :foreground "blue")+             :foreground "medium blue")             (agda2-highlight-field-face-             :foreground "dark red")+             :foreground "deeppink")             (agda2-highlight-function-face-             :foreground "dark green")+             :foreground "darkgreen")             (agda2-highlight-module-face-             :foreground "dark green")+             :foreground "medium blue")             (agda2-highlight-postulate-face-             :foreground "dark green")+             :foreground "darkgreen")             (agda2-highlight-primitive-face-             :foreground "dark green")+             :foreground "darkgreen")             (agda2-highlight-record-face-             :foreground "blue")+             :foreground "medium blue")             (agda2-highlight-dotted-face)             (agda2-highlight-error-face-             :foreground "black"-             :background "sandy brown")+             :foreground "red"+             :underline)             (agda2-highlight-unsolved-meta-face              :foreground "black"-             :background "gold")+             :background "yellow")             (agda2-highlight-unsolved-constraint-face              :foreground "black"-             :background "gold")+             :background "yellow")             (agda2-highlight-termination-problem-face              :foreground "black"-             :background "red")+             :background "light salmon")             (agda2-highlight-incomplete-pattern-face              :foreground "black"              :background "purple")             (agda2-highlight-typechecks-face              :foreground "black"-             :background "light steel blue")))+             :background "light blue"))) 	 ((equal group 'default-faces)           (list (cons 'agda2-highlight-keyword-face 		      (agda2-highlight-face-attributes
src/data/emacs-mode/agda2-mode.el view
@@ -10,7 +10,7 @@  ;;; Code: -(defvar agda2-version "2.4.0"+(defvar agda2-version "2.4.0.1"   "The version of the Agda mode. Note that the same version of the Agda executable must be used.")
src/full/Agda/Compiler/HaskellTypes.hs view
@@ -122,9 +122,10 @@           hsApp <$> getHsType d <*> fromArgs args         Pi a b ->           if isBinderUsed b  -- Andreas, 2012-04-03.  Q: could we rely on Abs/NoAbs instead of again checking freeness of variable?-          then underAbstraction a b $ \b ->-            hsForall <$> getHsVar 0 <*>-              (hsFun <$> fromType (unDom a) <*> fromType b)+          then do+            hsA <- fromType (unDom a)+            underAbstraction a b $ \b ->+              hsForall <$> getHsVar 0 <*> (hsFun hsA <$> fromType b)           else hsFun <$> fromType (unDom a) <*> fromType (absApp b __IMPOSSIBLE__)         Con c args -> hsApp <$> getHsType (conName c) <*> fromArgs args         Lam{}      -> err
src/full/Agda/Interaction/BasicOps.hs view
@@ -188,12 +188,12 @@ data Rewrite =  AsIs | Instantiated | HeadNormal | Simplified | Normalised     deriving (Read) ---rewrite :: Rewrite -> Term -> TCM Term-rewrite AsIs	     t = return t-rewrite Instantiated t = return t   -- reify does instantiation-rewrite HeadNormal   t = {- etaContract =<< -} reduce t-rewrite Simplified   t = {- etaContract =<< -} simplify t-rewrite Normalised   t = {- etaContract =<< -} normalise t+--normalForm :: Rewrite -> Term -> TCM Term+normalForm AsIs	     t = return t+normalForm Instantiated t = return t   -- reify does instantiation+normalForm HeadNormal   t = {- etaContract =<< -} reduce t+normalForm Simplified   t = {- etaContract =<< -} simplify t+normalForm Normalised   t = {- etaContract =<< -} normalise t   data OutputForm a b = OutputForm Range ProblemId (OutputConstraint a b)@@ -428,7 +428,7 @@    where     rewriteJudg mv (HasType i t) = do       ms <- getMetaNameSuggestion i-      t <- rewrite norm t+      t <- normalForm norm t       vs <- getContextArgs       let x = NamedMeta ms i       reportSDoc "interactive.meta" 10 $ TP.vcat@@ -482,7 +482,7 @@       TelV atel _ <- telView a       let arity = size atel       a        <- local (\e -> e { envPrintDomainFreePi = True }) $ do-        reify =<< cleanupType arity args =<< rewrite norm =<< withFunctionType tel vs as EmptyTel a+        reify =<< cleanupType arity args =<< normalForm norm =<< withFunctionType tel vs as EmptyTel a       return (OfType' h a)   where     cleanupType arity args t = do@@ -578,7 +578,7 @@                                xs          out i (Dom _ (x, t)) = escapeContext i $ do-          t' <- reify =<< rewrite norm t+          t' <- reify =<< normalForm norm t           return $ OfType x t'  @@ -588,7 +588,7 @@ typeInCurrent :: Rewrite -> Expr -> TCM Expr typeInCurrent norm e =     do 	(_,t) <- wakeIrrelevantVars $ inferExpr e-        v <- rewrite norm t+        v <- normalForm norm t         reify v
src/full/Agda/Interaction/FindFile.hs view
@@ -13,8 +13,6 @@   , findInterfaceFile   , checkModuleName   , moduleName', moduleName-  , ModuleToSource-  , SourceToModule, sourceToModule   , tests   ) where @@ -30,6 +28,8 @@ import Agda.Syntax.Concrete import Agda.Syntax.Parser import Agda.TypeChecking.Monad.Base+import Agda.TypeChecking.Monad.Benchmark (billTo)+import qualified Agda.TypeChecking.Monad.Benchmark as Bench import {-# SOURCE #-} Agda.TypeChecking.Monad.Options (getIncludeDirs) import Agda.Utils.FileName @@ -153,7 +153,7 @@ --   Use wisely!  moduleName' :: AbsolutePath -> TCM TopLevelModuleName-moduleName' file = liftIO $ do+moduleName' file = billTo [Bench.ModuleName] $ liftIO $ do   name <- topLevelModuleName <$> parseFile' moduleParser file   case name of     TopLevelModuleName ["_"] -> return $ TopLevelModuleName [defaultName]@@ -172,23 +172,3 @@   m <- moduleName' file   checkModuleName m file   return m---- | Maps top-level module names to the corresponding source file--- names.--type ModuleToSource = Map TopLevelModuleName AbsolutePath---- | Maps source file names to the corresponding top-level module--- names.--type SourceToModule = Map AbsolutePath TopLevelModuleName---- | Creates a 'SourceToModule' map based on 'stModuleToSource'.--sourceToModule :: TCM SourceToModule-sourceToModule =-  Map.fromList-     .  map (\(m, f) -> (f, m))-     .  Map.toList-     .  stModuleToSource-    <$> get
src/full/Agda/Interaction/Highlighting/Emacs.hs view
@@ -13,7 +13,7 @@ import Agda.Interaction.EmacsCommand import Agda.Syntax.Common import Agda.TypeChecking.Monad-  (TCM, envHighlightingMethod, HighlightingMethod(..))+  (TCM, envHighlightingMethod, HighlightingMethod(..), ModuleToSource) import Agda.Utils.FileName import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.String
src/full/Agda/Interaction/InteractionTop.hs view
@@ -21,6 +21,7 @@ import Data.Function import Data.List as List import Data.Maybe+import Data.Map (Map) import qualified Data.Map as Map import Data.Monoid import Data.Traversable (Traversable)@@ -94,6 +95,10 @@     -- the file when it was last loaded.   , optionsOnReload :: CommandLineOptions     -- ^ Reset the options on each reload to these.+  , oldInteractionScopes :: Map InteractionId ScopeInfo+    -- ^ We remember (the scope of) old interaction points to make it+    --   possible to parse and compute highlighting information for the+    --   expression that it got replaced by.   }  -- | Initial auxiliary interaction state@@ -103,6 +108,7 @@   { theInteractionPoints = []   , theCurrentFile       = Nothing   , optionsOnReload      = defaultOptions+  , oldInteractionScopes = Map.empty   }  @@ -149,6 +155,23 @@   s { theInteractionPoints = f (theInteractionPoints s) }  +-- | Operations for manipulating 'oldInteractionScopes'.++insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()+insertOldInteractionScope ii scope =+  modify $ \s -> s { oldInteractionScopes = Map.insert ii scope $ oldInteractionScopes s }++removeOldInteractionScope :: InteractionId -> CommandM ()+removeOldInteractionScope ii =+  modify $ \s -> s { oldInteractionScopes = Map.delete ii $ oldInteractionScopes s }++getOldInteractionScope :: InteractionId -> CommandM ScopeInfo+getOldInteractionScope ii = do+  ms <- gets $ Map.lookup ii . oldInteractionScopes+  case ms of+    Nothing    -> fail $ "not an old interaction point: " ++ show ii+    Just scope -> return scope+ -- | Run an 'IOTCM' value, catch the exceptions, emit output -- --   If an error happens the state of 'CommandM' does not change,@@ -554,10 +577,10 @@                 return Nothing     mapM_ putResponse resp -interpret (Cmd_highlight ii rng s) = withCurrentFile $+interpret (Cmd_highlight ii rng s) = withCurrentFile $ do+  scope <- getOldInteractionScope ii+  removeOldInteractionScope ii   lift (do-    scope <- getOldInteractionScope ii-    removeOldInteractionPoint ii     e     <- concreteToAbstract scope =<< B.parseExpr rng s     printHighlightingInfo =<< generateTokenInfoFromString rng s     highlightExpr e)@@ -788,6 +811,8 @@     mis' <- getInteractionPoints     reportSLn "interaction.give" 30 $ "interaction points after = " ++ show mis'     return (ae, mis' \\ mis)+  -- favonia: backup the old scope for highlighting+  when (giveRefine == Give) $ insertOldInteractionScope ii scope   -- sort the new interaction points and put them into the state   -- in replacement of the old interaction point   iis       <- lift $ sortInteractionPoints iis
src/full/Agda/Interaction/Options.hs view
@@ -216,11 +216,13 @@  checkOpts :: Flag CommandLineOptions checkOpts opts-  | not (atMostOne [optAllowUnsolved . p, \x -> optCompile x || optCompileNoMain x]) = Left+  | not (atMostOne [optAllowUnsolved . p, \x -> optCompile x]) = Left       "Unsolved meta variables are not allowed when compiling.\n"+  | optCompileNoMain opts && not (optCompile opts) = Left+      "--no-main only allowed in combination with --compile.\n"   | not (atMostOne [optGHCiInteraction, isJust . optInputFile]) =       Left "Choose at most one: input file or --interaction.\n"-  | not (atMostOne $ interactive ++ [\x -> optCompile x || optCompileNoMain x, optEpicCompile, optJSCompile]) =+  | not (atMostOne $ interactive ++ [\x -> optCompile x, optEpicCompile, optJSCompile]) =       Left "Choose at most one: compilers/--interactive/--interaction.\n"   | not (atMostOne $ interactive ++ [optGenerateHTML]) =       Left "Choose at most one: --html/--interactive/--interaction.\n"@@ -357,8 +359,8 @@                     "for use with the Emacs mode"     , Option ['c']  ["compile"] (NoArg compileFlag)                     "compile program using the MAlonzo backend (experimental)"-    , Option []  ["compile-no-main"] (NoArg compileFlagNoMain)-                    "compile module and dependencies using the MAlonzo backend (experimental)"+    , Option []     ["no-main"] (NoArg compileFlagNoMain)+                    "when compiling using the MAlonzo backend (experimental), do not treat the requested module as the main module of a program"     , Option []     ["epic"] (NoArg compileEpicFlag) "compile program using the Epic backend"     , Option []     ["js"] (NoArg compileJSFlag) "compile program using the JS backend"     , Option []     ["compile-dir"] (ReqArg compileDirFlag "DIR")
src/full/Agda/Interaction/Response.hs view
@@ -14,7 +14,6 @@   ) where  import Agda.Interaction.Highlighting.Precise-import Agda.Interaction.FindFile (ModuleToSource) import Agda.TypeChecking.Monad.Base import Agda.Syntax.Common   (InteractionId(..)) import Agda.Syntax.Concrete (Expr)
src/full/Agda/Main.hs view
@@ -109,8 +109,9 @@           interaction :: TCM (Maybe Interface) -> TCM ()           interaction | i             = runIM . interactionLoop                       | ghci          = (failIfInt mimicGHCi =<<)+                      | compile && compileNoMain+                                      = (MAlonzo.compilerMain False =<<) . (failIfNoInt =<<)                       | compile       = (MAlonzo.compilerMain True =<<) . (failIfNoInt =<<)-                      | compileNoMain = (MAlonzo.compilerMain False =<<) . (failIfNoInt =<<)                       | epic          = (Epic.compilerMain    =<<) . (failIfNoInt =<<)                       | js            = (JS.compilerMain      =<<) . (failIfNoInt =<<)                       | otherwise     = (() <$)
src/full/Agda/Syntax/Abstract/Name.hs view
@@ -298,7 +298,11 @@  instance KillRange Name where   killRange x = x { nameConcrete = killRange $ nameConcrete x-                  , nameBindingSite = noRange+                  -- Andreas, 2014-03-30+                  -- An experiment: what happens if we preserve+                  -- the range of the binding site, but kill all+                  -- other ranges before serialization?+                  -- , nameBindingSite = noRange                   }  instance KillRange ModuleName where
src/full/Agda/Syntax/Concrete.hs view
@@ -47,6 +47,7 @@     )     where +import Control.DeepSeq import Data.Typeable (Typeable) import Data.Foldable (Foldable) import Data.Traversable (Traversable)@@ -114,6 +115,7 @@         | Equal !Range Expr Expr               -- ^ ex: @a = b@, used internally in the parser     deriving (Typeable) +instance NFData Expr  -- | Concrete patterns. No literals in patterns at the moment. data Pattern@@ -131,6 +133,7 @@ 	| LitP Literal                            -- ^ @0@, @1@, etc.     deriving (Typeable) +instance NFData Pattern  -- | A lambda binding is either domain free or typed. type LamBinding = LamBinding' TypedBindings@@ -206,6 +209,8 @@              , lhsPatsRight  :: [NamedArg Pattern]  -- ^ side patterns              }   deriving (Typeable)++instance NFData LHSCore  {- TRASH lhsCoreToPattern :: LHSCore -> Pattern
src/full/Agda/Syntax/Concrete/Name.hs view
@@ -7,6 +7,7 @@ -} module Agda.Syntax.Concrete.Name where +import Control.DeepSeq import Control.Applicative  import Data.List@@ -36,6 +37,8 @@   = Name !Range [NamePart]  -- ^ A (mixfix) identifier.   | NoName !Range NameId    -- ^ @_@.   deriving (Typeable)++instance NFData Name  -- | Mixfix identifiers are composed of words and holes, --   e.g. @_+_@ or @if_then_else_@ or @[_/_]@.
src/full/Agda/Syntax/Concrete/Operators.hs view
@@ -27,6 +27,7 @@     , patternQNames     ) where +import Control.DeepSeq import Control.Applicative import Control.Monad @@ -399,7 +400,7 @@     patP <- buildParser (getRange p) flat DontUseBoundNames     let cons = getNames [ConName, PatternSynName] flat     let flds = getNames [FldName] flat-    case [ res | p' <- parsePat patP p+    case [ res | p' <- force $ parsePat patP p                , res <- validPattern (PatternCheckConfig top cons flds) p' ] of         [(p,lhs)] -> return lhs         []        -> typeError $ NoParseForLHS lhsOrPatSyn p@@ -547,7 +548,7 @@       buildParser (getRange es) flat UseBoundNames      -- Parse-    case parse p es of+    case force $ parse p es of         [e] -> return e         []  -> do           -- When the parser fails and a name is not in scope, it is more
src/full/Agda/Syntax/Internal.hs view
@@ -329,8 +329,8 @@ properlyMatching VarP{} = False properlyMatching DotP{} = False properlyMatching LitP{} = True-properlyMatching (ConP _ mt ps) = List.or $ isNothing mt -- not a record cons-  : map (properlyMatching . namedArg) ps  -- or one of subpatterns is a proper m+properlyMatching (ConP _ mt ps) = isNothing mt || -- not a record cons+  List.any (properlyMatching . namedArg) ps  -- or one of subpatterns is a proper m properlyMatching ProjP{} = True  ---------------------------------------------------------------------------@@ -416,7 +416,8 @@  -- | An unapplied variable. var :: Nat -> Term-var i = Var i []+var i | i >= 0    = Var i []+      | otherwise = __IMPOSSIBLE__  -- | Add 'DontCare' is it is not already a @DontCare@. dontCare :: Term -> Term
src/full/Agda/Syntax/Scope/Monad.hs view
@@ -170,10 +170,19 @@ -- * Names  -- | Create a fresh abstract name from a concrete name.+--+--   This function is used when we translate a concrete name+--   in a binder.  The 'Range' of the concrete name is+--   saved as the 'nameBindingSite' of the abstract name. freshAbstractName :: Fixity' -> C.Name -> ScopeM A.Name freshAbstractName fx x = do   i <- fresh-  return $ A.Name i x (getRange x) fx+  return $ A.Name+    { nameId          = i+    , nameConcrete    = x+    , nameBindingSite = getRange x+    , nameFixity      = fx+    }  -- | @freshAbstractName_ = freshAbstractName defaultFixity@ freshAbstractName_ :: C.Name -> ScopeM A.Name
src/full/Agda/Syntax/Translation/InternalToAbstract.hs view
@@ -146,45 +146,50 @@     DDot  v -> reify v     DCon c vs -> apps (A.Con (AmbQ [c])) =<< reifyIArgs vs     DDef f vs -> apps (A.Def f) =<< reifyIArgs vs-    DWithApp us vs -> do-      us <- reify us-      let wapp [e] = e-          wapp (e : es) = A.WithApp exprInfo e es-          wapp [] = __IMPOSSIBLE__-      reifyApp (wapp us) vs+    DWithApp u us vs -> do+      (e, es) <- reify (u, us)+      reifyApp (if null es then e else A.WithApp exprInfo e es) vs +-- | @reifyDisplayForm f vs fallback@+--   tries to rewrite @f vs@ with a display form for @f@.+--   If successful, reifies the resulting display term,+--   otherwise, does @fallback@. reifyDisplayForm :: QName -> I.Args -> TCM A.Expr -> TCM A.Expr-reifyDisplayForm x vs fallback = do-  enabled <- displayFormsEnabled-  if enabled-    then do-      md <- liftTCM $ displayForm x vs-      case md of-        Nothing -> fallback-        Just d  -> reify d-    else fallback+reifyDisplayForm f vs fallback = do+  ifNotM displayFormsEnabled fallback $ {- else -} do+  caseMaybeM (liftTCM $ displayForm f vs) fallback reify -{--reifyDisplayFormP :: A.LHS -> TCM A.LHS-reifyDisplayFormP lhs@(A.LHS i A.LHSProj{} wps) =-  typeError $ NotImplemented "reifyDisplayForm for copatterns"-reifyDisplayFormP lhs@(A.LHS i (A.LHSHead x ps) wps) =--}+-- | @reifyDisplayFormP@ tries to recursively+--   rewrite a lhs with a display form.+--+--   Note: we are not necessarily in the empty context upon entry! reifyDisplayFormP :: A.SpineLHS -> TCM A.SpineLHS-reifyDisplayFormP lhs@(A.SpineLHS i x ps wps) =+reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =   ifNotM displayFormsEnabled (return lhs) $ {- else -} do-    let vs = [ setHiding h $ defaultArg $ I.var n-             | (n, h) <- zip [0..] $ map getHiding ps+    let vs = [ setHiding h $ defaultArg $ I.var i+             | (i, h) <- zip [0..] $ map getHiding ps              ]-    md <- liftTCM $ displayForm x vs+    -- Try to rewrite @f 0 1 2 ... |ps|-1@ to a dt.+    -- Andreas, 2014-06-11  Issue 1177:+    -- I thought we need to add the placeholders for ps to the context,+    -- because otherwise displayForm will not raise the display term+    -- and we will have variable clashes.+    -- But apparently, it has no influence...+    -- Ulf, can you add an explanation?+    md <- liftTCM $ -- addContext (replicate (length ps) "x") $+      displayForm f vs     reportSLn "reify.display" 20 $-      "display form of " ++ show x ++ " " ++ show ps ++ " " ++ show wps ++ ":\n  " ++ show md+      "display form of " ++ show f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n  " ++ show md     case md of       Just d  | okDisplayForm d ->+        -- In the display term @d@, @var i@ should be a placeholder+        -- for the @i@th pattern of @ps@.+        -- Andreas, 2014-06-11:+        -- Are we sure that @d@ did not use @var i@ otherwise?         reifyDisplayFormP =<< displayLHS (map namedArg ps) wps d       _ -> return lhs   where-    okDisplayForm (DWithApp (d : ds) []) =+    okDisplayForm (DWithApp d ds []) =       okDisplayForm d && all okDisplayTerm ds     okDisplayForm (DTerm (I.Def f vs)) = all okElim vs     okDisplayForm (DDef f vs) = all okDArg vs@@ -210,14 +215,17 @@     okTerm (I.Def x []) = show x == "_" -- Handling wildcards in display forms     okTerm _            = True -- False -    flattenWith (DWithApp (d : ds) ds1) = case flattenWith d of-      (f, vs, ds') -> (f, vs, ds' ++ ds ++ map (DTerm . unArg) ds1)+    -- Flatten a dt into (parentName, parentArgs, withArgs).+    flattenWith :: DisplayTerm -> (QName, [I.Arg DisplayTerm], [DisplayTerm])+    flattenWith (DWithApp d ds1 ds2) = case flattenWith d of+      (f, vs, ds0) -> (f, vs, ds0 ++ ds1 ++ map (DTerm . unArg) ds2)     flattenWith (DDef f vs) = (f, vs, [])     -- .^ hacky, but we should only hit this when printing debug info     flattenWith (DTerm (I.Def f es)) =       let vs = maybe __IMPOSSIBLE__ id $ mapM isApplyElim es       in (f, map (fmap DTerm) vs, [])     flattenWith _ = __IMPOSSIBLE__ +    displayLHS :: [A.Pattern] -> [A.Pattern] -> DisplayTerm -> TCM A.SpineLHS     displayLHS ps wps d = case flattenWith d of       (f, vs, ds) -> do         ds <- mapM termToPat ds@@ -229,8 +237,6 @@         ci   = ConPatInfo False patNoRange         argToPat arg = fmap unnamed <$> traverse termToPat arg -        len = genericLength ps-         termToPat :: DisplayTerm -> TCM A.Pattern          termToPat (DTerm (I.Var n [])) = return $ ps !! n@@ -247,13 +253,16 @@         termToPat (DDot v)             = A.DotP patNoRange <$> termToExpr v         termToPat v                    = A.DotP patNoRange <$> reify v -- __IMPOSSIBLE__ +        len = genericLength ps+         argsToExpr = mapM (traverse termToExpr)          -- TODO: restructure this to avoid having to repeat the code for reify         termToExpr :: Term -> TCM A.Expr-        termToExpr v =+        termToExpr v = do+          reportSLn "reify.display" 60 $ "termToExpr " ++ show v+          -- After unSpine, a Proj elimination is __IMPOSSIBLE__!           case unSpine v of-            I.Var n [] | n < len -> return $ A.patternToExpr $ ps !! n             I.Con c vs ->               apps (A.Con (AmbQ [conName c])) =<< argsToExpr vs             I.Def f es -> do@@ -261,7 +270,14 @@               apps (A.Def f) =<< argsToExpr vs             I.Var n es -> do               let vs = maybe __IMPOSSIBLE__ id $ mapM isApplyElim es-              uncurry apps =<< (,) <$> reify (I.var (n - len)) <*> argsToExpr vs+              -- Andreas, 2014-06-11  Issue 1177+              -- due to β-normalization in substitution,+              -- even the pattern variables @n < len@ can be+              -- applied to some args @vs@.+              e <- if n < len+                   then return $ A.patternToExpr $ ps !! n+                   else reify (I.var (n - len))+              apps e =<< argsToExpr vs             _ -> return underscore  instance Reify Literal Expr where@@ -659,9 +675,10 @@         stripArgs _ [] = []         stripArgs fixedPos (a : as) =           case getHiding a of-            Hidden | canStrip a as -> stripArgs False as-            _                      -> stripName fixedPos (stripArg a) :-                                      stripArgs True as+            Hidden   | canStrip a as -> stripArgs False as+            Instance | canStrip a as -> stripArgs False as+            _                        -> stripName fixedPos (stripArg a) :+                                        stripArgs True as          stripName True  = fmap (unnamed . namedThing)         stripName False = id@@ -673,7 +690,7 @@           ]           where p = namedArg a -        isUnnamedHidden x = isHidden x && nameOf (unArg x) == Nothing+        isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing          stripArg a = fmap (fmap stripPat) a
src/full/Agda/Termination/Inlining.hs view
@@ -186,7 +186,7 @@           where n' = n - 1      dispToPats :: DisplayTerm -> TCM ([NamedArg Pattern], Permutation)-    dispToPats (DWithApp (DDef _ vs : ws) zs) = do+    dispToPats (DWithApp (DDef _ vs) ws zs) = do       let us = vs ++ map defaultArg ws ++ map (fmap DTerm) zs       (ps, (j, ren)) <- (`runStateT` (0, [])) $                         map (fmap unnamed) <$> mapM (traverse dtermToPat) us@@ -231,8 +231,7 @@     (vs, es') = splitApplyElims es  dtermToTerm :: DisplayTerm -> Term-dtermToTerm (DWithApp [] _)        = __IMPOSSIBLE__-dtermToTerm (DWithApp (d : ds) vs) = dtermToTerm d `apply` (map (defaultArg . dtermToTerm) ds ++ vs)+dtermToTerm (DWithApp d ds vs)     = dtermToTerm d `apply` (map (defaultArg . dtermToTerm) ds ++ vs) dtermToTerm (DCon c args)          = Con (ConHead c []) $ map (fmap dtermToTerm) args dtermToTerm (DDef f args)          = Def f $ map (Apply . fmap dtermToTerm) args dtermToTerm (DDot v)               = v
src/full/Agda/Termination/TermCheck.hs view
@@ -54,6 +54,7 @@ import Agda.TypeChecking.Monad.Builtin import Agda.TypeChecking.Substitute import Agda.TypeChecking.SizedTypes+import Agda.TypeChecking.Datatypes  import qualified Agda.TypeChecking.Monad.Base.Benchmark as Benchmark import Agda.TypeChecking.Monad.Benchmark (billTo, billPureTo)@@ -489,6 +490,27 @@     LitDBP{}  -> return p     ProjDBP{} -> return p +stripNonDataArgs :: [DeBruijnPat] -> TerM [DeBruijnPat]+stripNonDataArgs ps = do+  withoutKEnabled <- liftTCM $ optWithoutK <$> pragmaOptions+  if withoutKEnabled+    then do+      f   <- terGetCurrent+      def <- liftTCM $ getConstInfo f+      ty  <- liftTCM $ reduce $ defType def+      TelV tel _ <- liftTCM $ telView ty+      let types = map (unEl . snd . unDom) $ telToList tel+      zipWithM stripIfNotData ps types+    else return ps+  where+    stripIfNotData :: DeBruijnPat -> Term -> TerM DeBruijnPat+    stripIfNotData p ty = liftTCM $ do+      isData <- isDataOrRecord ty+      case isData of+        Just _  -> return p+        Nothing -> return unusedVar++ -- | cf. 'TypeChecking.Coverage.Match.buildMPatterns' openClause :: Permutation -> [Pattern] -> ClauseBody -> TerM ([DeBruijnPat], Maybe Term) openClause perm ps body = do@@ -517,9 +539,13 @@ -- | Extract recursive calls from one clause. termClause :: Clause -> TerM Calls termClause clause = do-  name <- terGetCurrent-  ifM (isJust <$> do isWithFunction name) (return mempty) $ do-  mapM' termClause' =<< do liftTCM $ inlineWithClauses name clause+  withoutKEnabled <- liftTCM $ optWithoutK <$> pragmaOptions+  if withoutKEnabled+    then termClause' clause+    else do+      name <- terGetCurrent+      ifM (isJust <$> do isWithFunction name) (return mempty) $ do+      mapM' termClause' =<< do liftTCM $ inlineWithClauses name clause  termClause' :: Clause -> TerM Calls termClause' clause = do@@ -541,6 +567,7 @@       Nothing -> return CallGraph.empty       Just v -> do         dbpats <- mapM stripCoConstructors dbpats+        dbpats <- stripNonDataArgs dbpats         terSetPatterns dbpats $ do         reportBody v   {-
src/full/Agda/TypeChecking/CheckInternal.hs view
@@ -96,7 +96,9 @@     , text " : "     , prettyTCM t     ]-  v <- elimView v  -- bring projection-like funs in post-fix form+  -- Bring projection-like funs in post-fix form,+  -- even lone ones (True).+  v <- elimView True v   case ignoreSharing v of     Var i es   -> do       a <- typeOfBV i
src/full/Agda/TypeChecking/Conversion.hs view
@@ -470,8 +470,10 @@         _ -> do           -- Andreas, 2013-10-20 put projection-like function           -- into the spine, to make compareElims work.-          m <- elimView m-          n <- elimView n+          -- 'False' means: leave (Def f []) unchanged even for+          -- proj-like funs.+          m <- elimView False m+          n <- elimView False n           case (ignoreSharing m, ignoreSharing n) of 	    (Pi{}, Pi{}) -> equalFun m n
src/full/Agda/TypeChecking/Coverage.hs view
@@ -332,13 +332,15 @@   -> OneHolePatterns            -- ^ Patterns with hole at split point.   -> QName                      -- ^ Constructor to fit into hole.   -> CoverM (Maybe SplitClause) -- ^ New split clause if successful.-computeNeighbourhood delta1 n delta2 perm d pars ixs hix hps con = do+computeNeighbourhood delta1 n delta2 perm d pars ixs hix hps c = do    -- Get the type of the datatype   dtype <- liftTCM $ (`piApply` pars) . defType <$> getConstInfo d    -- Get the real constructor name-  con <- liftTCM $ getConForm con+  con <- liftTCM $ getConForm c+  con <- return $ con { conName = c }  -- What if we restore the current name?+                                       -- Andreas, 2013-11-29 changes nothing! {-   con <- conSrcCon . theDef <$> getConstInfo con   Con con [] <- liftTCM $ ignoreSharing <$> (constructorForm =<< normalise (Con con []))
src/full/Agda/TypeChecking/DisplayForm.hs view
@@ -4,99 +4,137 @@  import Control.Applicative import Control.Monad.Error+import Control.Monad.Trans.Maybe+ import Data.Traversable (traverse)  import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo) import Agda.Syntax.Internal+ import Agda.TypeChecking.Monad import Agda.TypeChecking.Substitute import Agda.TypeChecking.Level +import Agda.Utils.List+import Agda.Utils.Maybe+ #include "../undefined.h" import Agda.Utils.Impossible +-- | Find a matching display form for @q vs@.+--   In essence this tries to reqwrite @q vs@ with any+--   display form @q ps --> dt@ and returns the instantiated+--   @dt@ if successful.  First match wins. displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)-displayForm c vs = do-    odfs  <- defDisplay <$> getConstInfo c+displayForm q vs = do+    -- Get display forms for name q.+    odfs  <- defDisplay <$> getConstInfo q+    -- Display debug info about the @Open@s.     unless (null odfs) $ verboseS "tc.display.top" 100 $ do       n <- getContextId-      let fvs = map (\(OpenThing n _) -> n) odfs-      reportSLn "tc.display.top" 100 $ "displayForm: context = " ++ show n ++ ", dfs = " ++ show fvs-    dfs	  <- do-      xs <- mapM tryOpen odfs-      return [ df | Just df <- xs ]+      reportSLn "tc.display.top" 100 $+        "displayForm: context = " ++ show n +++        ", dfs = " ++ show (map openThingCtxIds odfs)+    -- Use only the display forms that can be opened in the current context.+    dfs	  <- catMaybes <$> mapM tryOpen odfs     scope <- getScope+    -- Keep the display forms that match the application @c vs@.     ms <- do-      ms <- mapM (flip matchDisplayForm vs) dfs+      ms <- mapM (runMaybeT . (`matchDisplayForm` vs)) dfs       return [ m | Just m <- ms, inScope scope m ]     -- Not safe when printing non-terminating terms.     -- (nfdfs, us) <- normalise (dfs, vs)     unless (null odfs) $ reportSLn "tc.display.top" 100 $ unlines-      [ "name        : " ++ show c+      [ "name        : " ++ show q       , "displayForms: " ++ show dfs       , "arguments   : " ++ show vs       , "matches     : " ++ show ms       , "result      : " ++ show (foldr (const . Just) Nothing ms)       ]-    return $ foldr (const . Just) Nothing ms-  `catchError` \_ -> return Nothing+    -- Return the first display form that matches.+    return $ mhead ms++--  Andreas, 2014-06-11: The following error swallowing+--  is potentially harmful, making debugging harder.+--  I removed it, and it does not cause problems on the test suite.+--  `catchError` \_ -> return Nothing+   where     inScope _ _ = True  -- TODO: distinguish between with display forms and other display forms --     inScope scope d = case hd d of---       Just h  -> maybe False (const True) $ inverseScopeLookupName h scope+--       Just h  -> isJust $ inverseScopeLookupName h scope --       Nothing -> __IMPOSSIBLE__ -- TODO: currently all display forms have heads-    hd (DTerm (Def x _))    = Just x-    hd (DTerm (Con x _))    = Just $ conName x-    hd (DTerm (Shared p))   = hd (DTerm $ derefPtr p)-    hd (DWithApp (d : _) _) = hd d-    hd _		    = Nothing+    -- 'hd' is only used in the commented-out code for 'inScope' above.+    -- hd (DTerm (Def x _))    = Just x+    -- hd (DTerm (Con x _))    = Just $ conName x+    -- hd (DTerm (Shared p))   = hd (DTerm $ derefPtr p)+    -- hd (DWithApp d _ _) = hd d+    -- hd _		    = Nothing -matchDisplayForm :: DisplayForm -> Args -> TCM (Maybe DisplayTerm)-matchDisplayForm (Display n ps v) vs-  | length ps > length vs = return Nothing+-- | Match a 'DisplayForm' @q ps = v@ against @q vs@.+--   Return the 'DisplayTerm' @v[us]@ if the match was successful,+--   i.e., @vs / ps = Just us@.+matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM DisplayTerm+matchDisplayForm (Display _ ps v) vs+  | length ps > length vs = mzero   | otherwise             = do-      fmap (\ us -> applySubst (parallelS $ reverse us) v `apply` vs1) <$> do-        match n ps $ raise 1 $ map unArg vs0+      us <- match ps $ raise 1 $ map unArg vs0+      return $ applySubst (parallelS $ reverse us) v `apply` vs1   where     (vs0, vs1) = splitAt (length ps) vs +-- | Class @Match@ for matching a term @p@ in the role of a pattern+--   against a term @v@.+--+--   The 0th variable in @p@ plays the role+--   of a place holder (pattern variable).  Each occurrence of+--   @var 0@ in @p@ stands for a different pattern variable.+--+--   The result of matching, if successful, is a list of solutions for the+--   pattern variables, in left-to-right order.+--+--   The 0th variable is in scope in the input @v@, but should not+--   actually occur!+--   In the output solution, the @0th@ variable is no longer in scope.+--   (It has been substituted by __IMPOSSIBLE__ which corresponds to+--   a raise by -1). class Match a where-  match :: Nat -> a -> a -> TCM (Maybe [Term])+  match :: a -> a -> MaybeT TCM [Term]  instance Match a => Match [a] where-  match n xs ys = fmap concat . traverse id <$> zipWithM (match n) xs ys+  match xs ys = concat <$> zipWithM match xs ys  instance Match a => Match (Arg a) where-  match n p v = match n (unArg p) (unArg v)+  match p v = match (unArg p) (unArg v)  instance Match a => Match (Elim' a) where-  match n p v =+  match p v =     case (p, v) of-      (Proj f, Proj f') | f == f' -> return $ Just []-      (Apply a, Apply a')         -> match n a a'-      _                           -> return Nothing+      (Proj f, Proj f') | f == f' -> return []+      (Apply a, Apply a')         -> match a a'+      _                           -> mzero  instance Match Term where-  match n p v = case (ignoreSharing p, ignoreSharing v) of-    (Var 0 [], v)                  -> return $ Just [subst __IMPOSSIBLE__ v]-    (Var i ps, Var j vs) | i == j  -> match n ps vs-    (Def c ps, Def d vs) | c == d  -> match n ps vs-    (Con c ps, Con d vs) | c == d  -> match n ps vs-    (Lit l, Lit l')      | l == l' -> return $ Just []-    (p, v)               | p == v  -> return $ Just []-    (p, Level l)                   -> match n p =<< reallyUnLevelView l-    (Sort ps, Sort pv)             -> match n ps pv-    (p, Sort (Type v))             -> match n p =<< reallyUnLevelView v-    _                              -> return Nothing+  match p v = case (ignoreSharing p, ignoreSharing v) of+    (Var 0 [], v)                  -> return [subst __IMPOSSIBLE__ v]+    (Var i ps, Var j vs) | i == j  -> match ps vs+    (Def c ps, Def d vs) | c == d  -> match ps vs+    (Con c ps, Con d vs) | c == d  -> match ps vs+    (Lit l, Lit l')      | l == l' -> return []+    (p, v)               | p == v  -> return []+    (p, Level l)                   -> match p =<< reallyUnLevelView l+    (Sort ps, Sort pv)             -> match ps pv+    (p, Sort (Type v))             -> match p =<< reallyUnLevelView v+    _                              -> mzero  instance Match Sort where-  match n p v = case (p, v) of-    (Type pl, Type vl) -> match n pl vl-    _ | p == v -> return $ Just []-    _          -> return Nothing+  match p v = case (p, v) of+    (Type pl, Type vl) -> match pl vl+    _ | p == v -> return []+    _          -> mzero  instance Match Level where-  match n p v = do+  match p v = do     p <- reallyUnLevelView p     v <- reallyUnLevelView v-    match n p v+    match p v
src/full/Agda/TypeChecking/Injectivity.hs view
@@ -71,17 +71,17 @@  checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse checkInjectivity f cs-  | pointLess cs = return NotInjective+  | pointLess cs = do+      reportSLn "tc.inj.check" 20 $ "Injectivity of " ++ show f ++ " would be pointless."+      return NotInjective   where     -- Is it pointless to use injectivity for this function?     pointLess []      = True     pointLess (_:_:_) = False-    pointLess [cl] = all (noMatch . unArg) $ clausePats cl-      where noMatch ConP{} = False-            noMatch LitP{} = False-            noMatch ProjP{}= False-            noMatch VarP{} = True-            noMatch DotP{} = True+    pointLess [cl] = not $ any (properlyMatching . unArg) $ clausePats cl+        -- Andreas, 2014-06-12+        -- If we only have record patterns, it is also pointless.+        -- We need at least one proper match. checkInjectivity f cs = do   reportSLn "tc.inj.check" 40 $ "Checking injectivity of " ++ show f   -- Extract the head symbol of the rhs of each clause (skip absurd clauses)@@ -130,6 +130,12 @@   uinv <- functionInverse u   vinv <- functionInverse v   case (uinv, vinv) of+    -- Andreas, Francesco, 2014-06-12:+    -- We know that one of u,v is neutral+    -- (see calls to useInjectivity in Conversion.hs).+    -- Otherwise, (e.g. if both were Blocked), the following case would be+    -- unsound, since it assumes the arguments to be pointwise equal.+    -- It would deliver non-unique solutions for metas.     (Inv f fArgs _, Inv g gArgs _)       | f == g    -> do         a <- defType <$> getConstInfo f
src/full/Agda/TypeChecking/Level.hs view
@@ -73,8 +73,9 @@ unLevel (Shared p) = unLevel (derefPtr p) unLevel v = return v -reallyUnLevelView :: Level -> TCM Term-reallyUnLevelView nv =+{-# SPECIALIZE reallyUnLevelView :: Level -> TCM Term #-}+reallyUnLevelView :: MonadTCM tcm => Level -> tcm Term+reallyUnLevelView nv = liftTCM $ do   case nv of     Max []              -> primLevelZero     Max [Plus 0 a]      -> return $ unLevelAtom a
src/full/Agda/TypeChecking/Monad/Base.hs view
@@ -14,6 +14,7 @@ import Control.Monad.State import Control.Monad.Reader import Control.Monad.Writer+import Control.Monad.Trans.Maybe import Control.Applicative  import Data.Function@@ -27,6 +28,7 @@ import Data.Traversable import Data.IORef +import Agda.Syntax.Concrete (TopLevelModuleName) import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo) import qualified Agda.Syntax.Common as Common import qualified Agda.Syntax.Concrete as C@@ -39,7 +41,7 @@ import Agda.TypeChecking.CompiledClause  import Agda.Interaction.Exceptions-import {-# SOURCE #-} Agda.Interaction.FindFile+-- import {-# SOURCE #-} Agda.Interaction.FindFile import Agda.Interaction.Options import {-# SOURCE #-} Agda.Interaction.Response   (InteractionOutputCallback, defaultInteractionOutputCallback, Response)@@ -76,10 +78,6 @@          , stTermErrs          :: Seq TerminationError 	 , stMetaStore	       :: MetaStore 	 , stInteractionPoints :: InteractionPoints-         , stOldInteractionPoints :: OldInteractionPoints-            -- ^ We remember (the scope of) old interaction points to make it-            --   possible to parse and compute highlighting information for the-            --   expression that it got replaced by. 	 , stAwakeConstraints    :: Constraints 	 , stSleepingConstraints :: Constraints          , stDirty               :: Bool@@ -161,7 +159,6 @@   , stTokens               = mempty   , stTermErrs             = Seq.empty   , stInteractionPoints    = Map.empty-  , stOldInteractionPoints = Map.empty   , stAwakeConstraints     = []   , stSleepingConstraints  = []   , stDirty                = False@@ -234,6 +231,30 @@   ---------------------------------------------------------------------------+-- ** Managing file names+---------------------------------------------------------------------------++-- | Maps top-level module names to the corresponding source file+-- names.++type ModuleToSource = Map TopLevelModuleName AbsolutePath++-- | Maps source file names to the corresponding top-level module+-- names.++type SourceToModule = Map AbsolutePath TopLevelModuleName++-- | Creates a 'SourceToModule' map based on 'stModuleToSource'.++sourceToModule :: TCM SourceToModule+sourceToModule =+  Map.fromList+     .  List.map (\(m, f) -> (f, m))+     .  Map.toList+     .  stModuleToSource+    <$> get++--------------------------------------------------------------------------- -- ** Interface --------------------------------------------------------------------------- @@ -390,7 +411,7 @@ ---------------------------------------------------------------------------  -- | A thing tagged with the context it came from.-data Open a = OpenThing [CtxId] a+data Open a = OpenThing { openThingCtxIds :: [CtxId], openThing :: a }     deriving (Typeable, Show, Functor)  ---------------------------------------------------------------------------@@ -566,8 +587,6 @@ -- | Data structure managing the interaction points. type InteractionPoints = Map InteractionId InteractionPoint -type OldInteractionPoints = Map InteractionId ScopeInfo- --------------------------------------------------------------------------- -- ** Signature ---------------------------------------------------------------------------@@ -595,24 +614,51 @@ emptySignature :: Signature emptySignature = Sig Map.empty HMap.empty -data DisplayForm = Display Nat [Term] DisplayTerm-		-- ^ The three arguments are:-		---		--   * @n@: number of free variables;-		---		--   * Patterns for arguments, one extra free var which-		--     represents pattern vars. There should @n@ of them.-		---		--   * Display form. @n@ free variables.+-- | A @DisplayForm@ is in essence a rewrite rule+--   @+--      q ts --> dt+--   @+--   for a defined symbol (could be a constructor as well) @q@.+--   The right hand side is a 'DisplayTerm' which is used to+--   'reify' to a more readable 'Abstract.Syntax'.+--+--   The patterns @ts@ are just terms, but @var 0@ is interpreted+--   as a hole.  Each occurrence of @var 0@ is a new hole (pattern var).+--   For each *occurrence* of @var0@ the rhs @dt@ has a free variable.+--   These are instantiated when matching a display form against a+--   term @q vs@ succeeds.+data DisplayForm = Display+  { dfFreeVars :: Nat+    -- ^ Number @n@ of free variables in 'dfRHS'.+  , dfPats     :: [Term]+    -- ^ Left hand side patterns, where @var 0@ stands for a pattern+    --   variable.  There should be @n@ occurrences of @var0@ in+    --   'dfPats'.+  , dfRHS      :: DisplayTerm+    -- ^ Right hand side, with @n@ free variables.+  }   deriving (Typeable, Show) -data DisplayTerm = DWithApp [DisplayTerm] Args-                 | DCon QName [Arg DisplayTerm]-                 | DDef QName [Arg DisplayTerm]-                 | DDot Term-		 | DTerm Term+-- | A structured presentation of a 'Term' for reification into+--   'Abstract.Syntax'.+data DisplayTerm+  = DWithApp DisplayTerm [DisplayTerm] Args+    -- ^ @(f vs | ws) us@.+    --   The first 'DisplayTerm' is the parent function @f@ with its args @vs@.+    --   The list of 'DisplayTerm's are the with expressions @ws@.+    --   The 'Args' are additional arguments @us@+    --   (possible in case the with-application is of function type).+  | DCon QName [Arg DisplayTerm]+    -- ^ @c vs@.+  | DDef QName [Arg DisplayTerm]+    -- ^ @d vs@.+  | DDot Term+    -- ^ @.v@.+  | DTerm Term+    -- ^ @v@.   deriving (Typeable, Show) +-- | By default, we have no display form. defaultDisplayForm :: QName -> [Open DisplayForm] defaultDisplayForm c = [] @@ -712,6 +758,8 @@     --   will be created: @t = \ pars r -> r .p@     --   In case of a projection-like function, just the function symbol     --   is returned as 'Def':  @t = \ pars -> f@.+  , projArgInfo   :: I.ArgInfo+    -- ^ The info of the principal (record) argument.   } deriving (Typeable, Show)  data Defn = Axiom@@ -877,8 +925,9 @@  -- | Controlling 'reduce'. data AllowedReduction-  = ProjectionReductions -- ^ (projection and) projection-like functions may be reduced-  | FunctionReductions   -- ^ functions which are not projections may be reduced+  = ProjectionReductions -- ^ (Projection and) projection-like functions may be reduced.+  | FunctionReductions   -- ^ Functions which are not projections may be reduced.+  | LevelReductions      -- ^ Reduce @'Level'@ terms.   deriving (Show, Eq, Ord, Enum, Bounded)  type AllowedReductions = [AllowedReduction]@@ -1244,6 +1293,7 @@ data ExpandHidden   = ExpandLast      -- ^ Add implicit arguments in the end until type is no longer hidden 'Pi'.   | DontExpandLast  -- ^ Do not append implicit arguments.+  deriving (Eq)  data ExpandInstances   = ExpandInstanceArguments@@ -1624,6 +1674,9 @@ {-# RULES "liftTCM/id" liftTCM = id #-} instance MonadIO m => MonadTCM (TCMT m) where     liftTCM = mapTCMT liftIO++instance MonadTCM tcm => MonadTCM (MaybeT tcm) where+  liftTCM = lift . liftTCM  instance (Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm) where   liftTCM = lift . liftTCM
src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs view
@@ -42,6 +42,8 @@     -- ^ Subphase for 'Termination'.   | With     -- ^ Subphase for 'Termination'.+  | ModuleName+    -- ^ Subphase for 'Import'.   | Sort     -- ^ Subphase for 'Serialize'.   | Operators
src/full/Agda/TypeChecking/Monad/Base/KillRange.hs view
@@ -60,7 +60,7 @@   killRange (ConsHead q) = ConsHead $ killRange q  instance KillRange Projection where-  killRange (Projection a b c d) = killRange4 Projection a b c d+  killRange (Projection a b c d e) = killRange4 Projection a b c d e  instance KillRange Occurrence where   killRange = id@@ -77,7 +77,7 @@ instance KillRange DisplayTerm where   killRange dt =     case dt of-      DWithApp dts args -> killRange2 DWithApp dts args+      DWithApp dt dts args -> killRange3 DWithApp dt dts args       DCon q dts        -> killRange2 DCon q dts       DDef q dts        -> killRange2 DDef q dts       DDot v            -> killRange1 DDot v
src/full/Agda/TypeChecking/Monad/Benchmark.hs view
@@ -16,7 +16,7 @@  import Agda.TypeChecking.Monad.Base.Benchmark import Agda.TypeChecking.Monad.Base-import Agda.TypeChecking.Monad.Options+import{-# SOURCE #-} Agda.TypeChecking.Monad.Options import Agda.TypeChecking.Monad.State  import Agda.Utils.Monad
src/full/Agda/TypeChecking/Monad/Env.hs view
@@ -75,7 +75,10 @@ onlyReduceProjections = local $ \ e -> e { envAllowedReductions = [ProjectionReductions] }  dontReduceProjections :: TCM a -> TCM a-dontReduceProjections = local $ \ e -> e { envAllowedReductions = [FunctionReductions] }+dontReduceProjections = local $ \ e -> e { envAllowedReductions = allReductions \\ [ProjectionReductions] }++dontReduceLevels :: TCM a -> TCM a+dontReduceLevels = local $ \ e -> e { envAllowedReductions = allReductions \\ [LevelReductions] }  allowAllReductions :: TCM a -> TCM a allowAllReductions = local $ \ e -> e { envAllowedReductions = allReductions }
src/full/Agda/TypeChecking/Monad/MetaVars.hs view
@@ -12,7 +12,7 @@ import qualified Data.Foldable as Fold import qualified Data.Traversable as Trav -import Agda.Syntax.Common+import Agda.Syntax.Common as Common import Agda.Syntax.Internal import Agda.Syntax.Position import Agda.Syntax.Scope.Base@@ -24,9 +24,10 @@ import Agda.TypeChecking.Monad.Context import Agda.TypeChecking.Substitute -import Agda.Utils.Maybe import Agda.Utils.Functor ((<.>)) import Agda.Utils.Fresh+import Agda.Utils.Maybe+import Agda.Utils.Monad import Agda.Utils.Permutation import Agda.Utils.Tuple import Agda.Utils.Size@@ -86,9 +87,49 @@       return $ piApply t $ permute (takeP (size vs) p) vs     IsSort{}                 -> __IMPOSSIBLE__ -isInstantiatedMeta :: MetaId -> TCM Bool-isInstantiatedMeta m = isJust <$> isInstantiatedMeta' m+-- | Check whether all metas are instantiated.+--   Precondition: argument is a meta (in some form) or a list of metas.+class IsInstantiatedMeta a where+  isInstantiatedMeta :: a -> TCM Bool +instance IsInstantiatedMeta MetaId where+  isInstantiatedMeta m = isJust <$> isInstantiatedMeta' m++instance IsInstantiatedMeta Term where+  isInstantiatedMeta = loop where+   loop v =+    case ignoreSharing v of+      MetaV x _  -> isInstantiatedMeta x+      DontCare v -> loop v+      Level l    -> isInstantiatedMeta l+      Lam _ b    -> isInstantiatedMeta b+      Con _ vs   -> isInstantiatedMeta vs+      _          -> __IMPOSSIBLE__++instance IsInstantiatedMeta Level where+  isInstantiatedMeta (Max ls) = isInstantiatedMeta ls++instance IsInstantiatedMeta PlusLevel where+  isInstantiatedMeta (Plus n l) | n == 0 = isInstantiatedMeta l+  isInstantiatedMeta _ = __IMPOSSIBLE__++instance IsInstantiatedMeta LevelAtom where+  isInstantiatedMeta (MetaLevel x es) = isInstantiatedMeta x+  isInstantiatedMeta _ = __IMPOSSIBLE__++instance IsInstantiatedMeta a => IsInstantiatedMeta [a] where+  isInstantiatedMeta = andM . map isInstantiatedMeta++instance IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) where+  isInstantiatedMeta = isInstantiatedMeta . maybeToList++instance IsInstantiatedMeta a => IsInstantiatedMeta (Common.Arg c a) where+  isInstantiatedMeta = isInstantiatedMeta . unArg++-- | Does not worry about raising.+instance IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) where+  isInstantiatedMeta = isInstantiatedMeta . unAbs+ isInstantiatedMeta' :: MetaId -> TCM (Maybe Term) isInstantiatedMeta' m = do   mv <- lookupMeta m@@ -173,12 +214,7 @@ removeInteractionPoint ii = do   scope <- getInteractionScope ii   modifyInteractionPoints $ Map.delete ii-  modify $ \s -> s { stOldInteractionPoints = Map.insert ii scope $ stOldInteractionPoints s } -removeOldInteractionPoint :: InteractionId -> TCM ()-removeOldInteractionPoint ii =-  modify $ \s -> s { stOldInteractionPoints = Map.delete ii $ stOldInteractionPoints s }- -- | Get a list of interaction ids. getInteractionPoints :: TCM [InteractionId] getInteractionPoints = Map.keys <$> gets stInteractionPoints@@ -240,13 +276,6 @@ getInteractionScope :: InteractionId -> TCM ScopeInfo getInteractionScope = getMetaScope <.> lookupMeta <=< lookupInteractionId -getOldInteractionScope :: InteractionId -> TCM ScopeInfo-getOldInteractionScope ii = do-  ms <- gets $ Map.lookup ii . stOldInteractionPoints-  case ms of-    Nothing    -> fail $ "not an old interaction point: " ++ show ii-    Just scope -> return scope- withMetaInfo' :: MetaVariable -> TCM a -> TCM a withMetaInfo' mv = withMetaInfo (miClosRange $ mvInfo mv) @@ -362,3 +391,4 @@  instance UnFreezeMeta a => UnFreezeMeta (Abs a) where   unfreezeMeta = Fold.mapM_ unfreezeMeta+
src/full/Agda/TypeChecking/Monad/Open.hs view
@@ -27,7 +27,6 @@ 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 :: Subst a => Open a -> TCM a@@ -37,6 +36,9 @@   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 +-- | Try to use an 'Open' the current context.+--   Returns 'Nothing' if current context is not an extension of the+--   context in which the 'Open' was created. tryOpen :: Subst a => Open a -> TCM (Maybe a) tryOpen o =   (Just <$> getOpen o)
src/full/Agda/TypeChecking/Monad/Options.hs-boot view
@@ -1,5 +1,9 @@ module Agda.TypeChecking.Monad.Options where +import Control.Applicative+import Control.Monad.Trans++import Agda.Interaction.Options import Agda.TypeChecking.Monad.Base import Agda.Utils.FileName import Agda.Utils.Pretty@@ -8,6 +12,15 @@  type VerboseKey = String +class (Functor m, Applicative m, Monad m) => HasOptions m where+  -- | Returns the pragma options which are currently in effect.+  pragmaOptions      :: m PragmaOptions+  -- | Returns the command line options which are currently in effect.+  commandLineOptions :: m CommandLineOptions++instance MonadIO m => HasOptions (TCMT m)++hasVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool verboseS :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm () reportSLn :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm () reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> TCM Doc -> tcm ()
src/full/Agda/TypeChecking/Monad/State.hs view
@@ -9,7 +9,8 @@ import Data.Map as Map import qualified Data.Set as Set -import {-# SOURCE #-} Agda.Interaction.Response+-- import {-# SOURCE #-} Agda.Interaction.Response+import Agda.Interaction.Response   (InteractionOutputCallback, Response)  import Agda.Syntax.Common
src/full/Agda/TypeChecking/Primitive.hs view
@@ -580,7 +580,8 @@      -- Other stuff     , "primTrustMe"         |-> primTrustMe-    , "primQNameEquality"  |-> mkPrimFun2 ((==) :: Rel QName)+    , "primQNameEquality"   |-> mkPrimFun2 ((==) :: Rel QName)+    , "primShowQName"       |-> mkPrimFun1 (Str . show :: QName -> Str)     ]     where 	(|->) = (,)
src/full/Agda/TypeChecking/ProjectionLike.hs view
@@ -28,33 +28,54 @@  -- | View for a @Def f (Apply a : es)@ where @isProjection f@. --   Used for projection-like @f@s.-data ProjectionView = ProjectionView-  { projViewProj  :: QName-  , projViewSelf  :: I.Arg Term-  , projViewSpine :: Elims-  }+data ProjectionView+  = ProjectionView+    { projViewProj  :: QName+    , projViewSelf  :: I.Arg Term+    , projViewSpine :: Elims+    }+    -- ^ A projection or projection-like function, applied to its+    --   principal argument+  | LoneProjectionLike QName I.ArgInfo+    -- ^ Just a lone projection-like function, missing its principal+    --   argument (from which we could infer the parameters).+  | NoProjection Term+    -- ^ Not a projection or projection-like thing.  -- | Semantics of 'ProjectionView'. unProjView :: ProjectionView -> Term-unProjView (ProjectionView f a es) = Def f (Apply a : es)+unProjView pv =+  case pv of+    ProjectionView f a es   -> Def f (Apply a : es)+    LoneProjectionLike f ai -> Def f []+    NoProjection v          -> v  -- | Top-level 'ProjectionView' (no reduction).-projView :: Term -> TCM (Maybe ProjectionView)+projView :: Term -> TCM ProjectionView projView v = do+  let fallback = return $ NoProjection v   case ignoreSharing v of-    Def f (Apply a : es) -> (ProjectionView f a es <$) <$> isProjection f-    _                    -> return Nothing+    Def f es -> caseMaybeM (isProjection f) fallback $ \ isP -> do+      case es of+        []           -> return $ LoneProjectionLike f $ projArgInfo isP+        Apply a : es -> return $ ProjectionView f a es+        -- Since a projection is a function, it cannot be projected itself.+        Proj{}  : _  -> __IMPOSSIBLE__+    _ -> fallback  -- | Reduce away top-level projection like functions. --   (Also reduces projections, but they should not be there, --   since Internal is in lambda- and projection-beta-normal form.) -- reduceProjectionLike :: Term -> TCM Term-reduceProjectionLike v =+reduceProjectionLike v = do   -- Andreas, 2013-11-01 make sure we do not reduce a constructor   -- because that could be folded back into a literal by reduce.-  maybeM (return v) (\ _ -> onlyReduceProjections $ reduce v) $ projView v+  pv <- projView v+  case pv of+    ProjectionView{} -> onlyReduceProjections $ reduce v                             -- ordinary reduce, only different for Def's+    _                -> return v  -- | Turn prefix projection-like function application into postfix ones. --   This does just one layer, such that the top spine contains@@ -62,18 +83,27 @@ --   Used in 'compareElims' in @TypeChecking.Conversion@ --   and in 'Agda.TypeChecking.CheckInternal'. --+--   If the 'Bool' is 'True', a lone projection like function will be+--   turned into a lambda-abstraction, expecting the principal argument.+--   If the 'Bool' is 'False', it will be returned unaltered.+-- --   No precondition. --   Preserves constructorForm, since it really does only something---   applications of projection-like functions.-elimView :: Term -> TCM Term-elimView v = do+--   on (applications of) projection-like functions.+elimView :: Bool -> Term -> TCM Term+elimView loneProjToLambda v = do   reportSDoc "tc.conv.elim" 30 $ text "elimView of " <+> prettyTCM v   reportSLn  "tc.conv.elim" 50 $ "v = " ++ show v   v <- reduceProjectionLike v   reportSDoc "tc.conv.elim" 40 $     text "elimView (projections reduced) of " <+> prettyTCM v-  caseMaybeM (projView v) (return v) $ \ (ProjectionView f a es) -> do-        (`applyE` (Proj f : es)) <$> elimView (unArg a)+  pv <- projView v+  case pv of+    NoProjection{}        -> return v+    LoneProjectionLike f ai+      | loneProjToLambda  -> return $ Lam ai $ Abs "r" $ Var 0 [Proj f]+      | otherwise         -> return v+    ProjectionView f a es -> (`applyE` (Proj f : es)) <$> elimView loneProjToLambda (unArg a)  {- Andreas, 2013-11-01: Use of unLevel no longer necessary, since we do not reduce!   case ignoreSharing v of@@ -149,7 +179,7 @@           reportSLn "tc.proj.like" 60 $ "  rewrote clauses to\n    " ++ show cc            -- Andreas, 2013-10-20 build parameter dropping function-          let ptel = take n $ telToList $ theTel $ telView' t+          let (ptel, Dom ai _ : _) = splitAt n $ telToList $ theTel $ telView' t               -- leading lambdas are to ignore parameter applications               proj = teleNoAbs ptel $ Def x []               -- proj = foldr (\ (Dom ai (y, _)) -> Lam ai . NoAbs y) (Def x []) ptel@@ -159,6 +189,7 @@                 , projFromType = d                 , projIndex    = n + 1                 , projDropPars = proj+                , projArgInfo  = ai                 }           let newDef = def                        { funProjection     = Just projection
src/full/Agda/TypeChecking/Reduce.hs view
@@ -36,6 +36,9 @@  import Agda.Utils.Monad import Agda.Utils.HashMap (HashMap)+import Agda.Utils.Maybe+import Agda.Utils.Monad+import Agda.Utils.Tuple  #include "../undefined.h" import Agda.Utils.Impossible@@ -282,7 +285,10 @@           v <- unfoldDefinition False reduceB' (Con c []) (conName c) args           traverse reduceNat v       Sort s   -> fmap sortTm <$> reduceB' s-      Level l  -> fmap levelTm <$> reduceB' l+      Level l  -> ifM (elem LevelReductions <$> asks envAllowedReductions)+                    {- then -} (fmap levelTm <$> reduceB' l)+                    {- else -} done+      -- Level l  -> fmap levelTm <$> reduceB' l       Pi _ _   -> done       Lit _    -> done       Var _ _  -> done@@ -390,7 +396,7 @@                   = retSimpl $ notBlocked $ v0 `applyE` es -- not fully applied       | otherwise = {-# SCC "reducePrimitive" #-} do           let (es1,es2) = genericSplitAt ar es-              args1     = maybe __IMPOSSIBLE__ id $ mapM isApplyElim es1+              args1     = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es1           r <- primFunImplementation pf args1           case r of             NoReduction args1' -> do@@ -1101,7 +1107,7 @@   instantiateFull' (DDot  v)	   = DDot  <$> instantiateFull' v   instantiateFull' (DCon c vs)	   = DCon c <$> instantiateFull' vs   instantiateFull' (DDef c vs)	   = DDef c <$> instantiateFull' vs-  instantiateFull' (DWithApp vs ws) = uncurry DWithApp <$> instantiateFull' (vs, ws)+  instantiateFull' (DWithApp v vs ws) = uncurry3 DWithApp <$> instantiateFull' (v, vs, ws)  instance InstantiateFull Defn where     instantiateFull' d = case d of
src/full/Agda/TypeChecking/Reduce/Monad.hs view
@@ -177,6 +177,3 @@           init' [] = {-'-} __IMPOSSIBLE__           init' xs = init xs -instantiateDef :: Definition -> ReduceM Definition-instantiateDef def = undefined-
src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs view
@@ -139,6 +139,7 @@           , projFromType = inf           , projIndex    = 3           , projDropPars = teleNoAbs (take 2 $ telToList tel) $ Def flat []+          , projArgInfo  = defaultArgInfo           }     addConstant flat $       flatDefn { defPolarity       = []
src/full/Agda/TypeChecking/Rules/Decl.hs view
@@ -287,7 +287,7 @@   -- namesDefs <- mapM (\ q -> (q,) <$> getConstInfo q) $ Set.toList names   -- mapM_ checkInj namesDefs -  forM_ (Set.toList names) $ \ q -> do+  Fold.forM_ names $ \ q -> do     def <- getConstInfo q     case theDef def of       d@Function{ funClauses = cs, funTerminates = Just True } -> do@@ -376,20 +376,7 @@              unless (m == m') $ typeError $ GenericError $               "COMPILED_DATA directives must appear in the same module " ++               "as their corresponding datatype definition,"-          case theDef def of-            Datatype{dataCons = cs}-              | length cs /= length hcs -> do-                  let n_forms_are = case length hcs of-                        1 -> "1 compiled form is"-                        n -> show n ++ " compiled forms are"-                      only | null hcs               = ""-                           | length hcs < length cs = "only "-                           | otherwise              = ""--                  err <- fsep $ [prettyTCM x] ++ pwords ("has " ++ show (length cs) ++-                                " constructors, but " ++ only ++ n_forms_are ++ " given [" ++ unwords hcs ++ "]")-                  typeError $ GenericError $ show err-              | otherwise -> do+          let addCompiledData cs = do                 addHaskellType x hs                 let computeHaskellType c = do                       def <- getConstInfo c@@ -399,13 +386,33 @@                             a <- reduce a                             case unEl a of                               Pi a (NoAbs _ b) -> underPars (n - 1) b-                              Pi a b  -> underAbstraction a b $ underPars (n - 1)+                              Pi a b  -> underAbstraction a b $ \b -> hsForall <$> getHsVar 0 <*> underPars (n - 1) b                               _       -> __IMPOSSIBLE__                       ty <- underPars np $ defType def                       reportSLn "tc.pragma.compile" 10 $ "Haskell type for " ++ show c ++ ": " ++ ty                       return ty                 hts <- mapM computeHaskellType cs                 sequence_ $ zipWith3 addHaskellCode cs hts hcs+          case theDef def of+            Datatype{dataCons = cs}+              | length cs /= length hcs -> do+                  let n_forms_are = case length hcs of+                        1 -> "1 compiled form is"+                        n -> show n ++ " compiled forms are"+                      only | null hcs               = ""+                           | length hcs < length cs = "only "+                           | otherwise              = ""++                  err <- fsep $ [prettyTCM x] ++ pwords ("has " ++ show (length cs) +++                                " constructors, but " ++ only ++ n_forms_are ++ " given [" ++ unwords hcs ++ "]")+                  typeError $ GenericError $ show err+              | otherwise -> addCompiledData cs+            Record{recConHead = ch}+              | length hcs == 1 -> addCompiledData [conName ch]+              | otherwise -> do+                  err <- fsep $ [prettyTCM x] ++ pwords ("has 1 constructor, but " +++                                show (length hcs) ++ " Haskell constructors are given [" ++ unwords hcs ++ "]")+                  typeError $ GenericError $ show err             _ -> typeError $ GenericError "COMPILED_DATA on non datatype"         A.CompiledPragma x hs -> do           def <- getConstInfo x
src/full/Agda/TypeChecking/Rules/Def.hs view
@@ -355,21 +355,24 @@ insertPatterns pats (A.RewriteRHS qs eqs rhs wh) = A.RewriteRHS qs eqs (insertPatterns pats rhs) wh insertPatterns pats rhs = rhs +-- | Parameters for creating a @with@-function. data WithFunctionProblem-      = NoWithFunction-      | WithFunction QName                -- parent function name-                     QName                -- with function name-                     Telescope            -- arguments to parent function-                     Telescope            -- arguments to the with function before the with expressions-                     Telescope            -- arguments to the with function after the with expressions-                     [Term]               -- with expressions-                     [Type]               -- types of the with expressions-                     Type                 -- type of the right hand side-                     [I.NamedArg Pattern] -- parent patterns-                     Permutation          -- permutation resulting from splitting the telescope into needed and unneeded vars-                     Permutation          -- permutation reordering the variables in the parent pattern-                     Permutation          -- final permutation (including permutation for the parent clause)-                     [A.Clause]           -- the given clauses for the with function+  = NoWithFunction+  | WithFunction+    { wfParentName :: QName                -- ^ parent function name+    , wfName       :: QName                -- ^ with function name+    , wfParentTel  :: Telescope            -- ^ arguments to parent function+    , wfBeforeTel  :: Telescope            -- ^ arguments to the with function before the with expressions+    , wfAfterTel   :: Telescope            -- ^ arguments to the with function after the with expressions+    , wfExprs      :: [Term]               -- ^ with expressions+    , wfExprTypes  :: [Type]               -- ^ types of the with expressions+    , wfRHSType    :: Type                 -- ^ type of the right hand side+    , wfParentPats :: [I.NamedArg Pattern] -- ^ parent patterns+    , wfPermSplit  :: Permutation          -- ^ permutation resulting from splitting the telescope into needed and unneeded vars+    , wfPermParent :: Permutation          -- ^ permutation reordering the variables in the parent pattern+    , wfPermFinal  :: Permutation          -- ^ final permutation (including permutation for the parent clause)+    , wfClauses    :: [A.Clause]           -- ^ the given clauses for the with function+    }  -- | Type check a function clause. {-
src/full/Agda/TypeChecking/Rules/Record.hs view
@@ -360,6 +360,7 @@           -- split the telescope into parameters (ptel) and the type or the record           -- (rt) which should be  R ptel           (ptel,[rt]) = splitAt (size tel - 1) $ telToList tel+          projArgI    = domInfo rt 	  conp	 = defaultArg 		 $ ConP con (Just (False, argFromDom $ fmap snd rt))                    [ Arg info $ unnamed $ VarP "x" | Dom info _ <- telToList ftel ]@@ -380,7 +381,7 @@        -- Andreas, 2013-10-20       -- creating the projection construction function-      let core = Lam defaultArgInfo $ Abs "r" $ bodyMod $ projcall+      let core = Lam projArgI $ Abs "r" $ bodyMod $ projcall           -- leading lambdas are to ignore parameter applications           proj = teleNoAbs ptel core           -- proj = foldr (\ (Dom ai (x, _)) -> Lam ai . NoAbs x) core ptel@@ -392,6 +393,7 @@             -- start counting with 1:             , projIndex    = size ptel + 1  -- which is @size tel@             , projDropPars = proj+            , projArgInfo  = projArgI             }        reportSDoc "tc.rec.proj" 80 $ sep
src/full/Agda/TypeChecking/Rules/Term.hs view
@@ -687,11 +687,13 @@               blockTerm t' $ coerce v ty t'         e0@(A.QuoteContext _ x e) -> do           ctx <- getContext-          lets <- envLetBindings <$> ask           thisModule <- currentModule+--          Disabled let bindings for now, as there is no way to get your hands on the+--          associated terms using the current reflection mechanism.+--          lets <- envLetBindings <$> ask+--          let letNames = map (quoteName . qualify thisModule) $ Map.keys lets           let contextNames = map (\(Dom _ (nm,_)) -> quoteName $ qualify thisModule nm) ctx-          let letNames = map (quoteName . qualify thisModule) $ Map.keys lets-          let names = contextNames ++ letNames+          let names = contextNames -- ++ letNames           nameList <- buildList <*> return names           ctxType <- el (list primQName)           (v, ctxType) <- addLetBinding defaultArgInfo x nameList ctxType (inferExpr e)@@ -1201,7 +1203,7 @@                   ErrorT (Args, [I.NamedArg A.Expr], Type) TCM (Args, Type)  -- Case: no arguments, do not insert trailing hidden arguments: We are done.-checkArguments DontExpandLast _ _ [] t0 t1 = return ([], t0)+checkArguments DontExpandLast DontExpandInstanceArguments _ [] t0 t1 = return ([], t0)  -- Case: no arguments, but need to insert trailing hiddens. checkArguments exh    expandIFS r [] t0 t1 =@@ -1209,8 +1211,9 @@       t1' <- unEl <$> reduce t1       implicitArgs (-1) (expand t1') t0     where-      expand (Pi (Dom info _) _)   Hidden = getHiding info /= Hidden-      expand _                     Hidden = True+      expand (Pi (Dom info _) _)   Hidden = getHiding info /= Hidden &&+                                            exh == ExpandLast+      expand _                     Hidden = exh == ExpandLast       expand (Pi (Dom info _) _) Instance = getHiding info /= Instance &&                                             expandIFS == ExpandInstanceArguments       expand _                   Instance = expandIFS == ExpandInstanceArguments
src/full/Agda/TypeChecking/Serialise.hs view
@@ -71,7 +71,7 @@  import Agda.TypeChecking.Monad import Agda.TypeChecking.CompiledClause-import Agda.TypeChecking.Pretty+-- import Agda.TypeChecking.Pretty  import Agda.Utils.BiMap (BiMap) import qualified Agda.Utils.BiMap as BiMap@@ -89,7 +89,7 @@ -- 32-bit machines). Word64 does not have these problems.  currentInterfaceVersion :: Word64-currentInterfaceVersion = 20140603 * 10 + 0+currentInterfaceVersion = 20140611 * 10 + 0  -- | Constructor tag (maybe omitted) and argument indices. @@ -257,9 +257,12 @@   case r of     Right x   -> return (Just x)     Left  err -> do-      reportSDoc "import.iface" 5 $-        text "Error when decoding interface file:" $+$-        nest 2 (prettyTCM err)+      reportSLn "import.iface" 5 $ "Error when decoding interface file"+      -- Andreas, 2014-06-11 deactivated debug printing+      -- in order to get rid of dependency of Serialize on TCM.Pretty+      -- reportSDoc "import.iface" 5 $+      --   text "Error when decoding interface file:"+      --   $+$ nest 2 (prettyTCM err)       return Nothing    where@@ -885,12 +888,12 @@   icode (DDot     a  ) = icode1 1 a   icode (DCon     a b) = icode2 2 a b   icode (DDef     a b) = icode2 3 a b-  icode (DWithApp a b) = icode2 4 a b+  icode (DWithApp a b c) = icode3 4 a b c   value = vcase valu where valu [a]       = valu1 DTerm a                            valu [1, a]    = valu1 DDot a                            valu [2, a, b] = valu2 DCon a b                            valu [3, a, b] = valu2 DDef a b-                           valu [4, a, b] = valu2 DWithApp a b+                           valu [4, a, b, c] = valu3 DWithApp a b c                            valu _         = malformed  instance EmbPrj MutualId where@@ -903,9 +906,9 @@                            valu _                             = malformed  instance EmbPrj Projection where-  icode (Projection a b c d) = icode4' a b c d-  value = vcase valu where valu [a, b, c, d] = valu4 Projection a b c d-                           valu _            = malformed+  icode (Projection a b c d e) = icode5' a b c d e+  value = vcase valu where valu [a, b, c, d, e] = valu5 Projection a b c d e+                           valu _               = malformed  instance EmbPrj HaskellExport where   icode (HsExport a b) = icode2' a b
src/full/Agda/TypeChecking/Substitute.hs view
@@ -24,8 +24,9 @@  import Agda.Utils.List import Agda.Utils.Monad-import Agda.Utils.Size import Agda.Utils.Permutation+import Agda.Utils.Size+import Agda.Utils.Tuple  #include "../undefined.h" import Agda.Utils.Impossible@@ -268,7 +269,7 @@   apply (DDot v)           args = DDot  $ apply v args   apply (DCon c vs)        args = DCon c $ vs ++ map (fmap DTerm) args   apply (DDef c vs)        args = DDef c $ vs ++ map (fmap DTerm) args-  apply (DWithApp v args') args = DWithApp v $ args' ++ args+  apply (DWithApp v ws args') args = DWithApp v ws $ args' ++ args  instance Apply t => Apply [t] where   apply  ts args = map (`apply` args) ts@@ -646,7 +647,7 @@   applySubst rho (DDot v)         = DDot  $ applySubst rho v   applySubst rho (DCon c vs)      = DCon c $ applySubst rho vs   applySubst rho (DDef c vs)      = DDef c $ applySubst rho vs-  applySubst rho (DWithApp vs ws) = uncurry DWithApp $ applySubst rho (vs, ws)+  applySubst rho (DWithApp v vs ws) = uncurry3 DWithApp $ applySubst rho (v, vs, ws)  instance Subst a => Subst (Tele a) where   applySubst rho  EmptyTel         = EmptyTel
src/full/Agda/TypeChecking/With.hs view
@@ -292,24 +292,42 @@ --   For instance, @aux a b c@ as @f (suc a) (suc b) | c@ -- --   @n@ is the number of with arguments.-withDisplayForm :: QName -> QName -> Telescope -> Telescope -> Nat -> [I.NamedArg Pattern] -> Permutation -> Permutation -> TCM DisplayForm+withDisplayForm+  :: QName       -- ^ The name of parent function.+  -> QName       -- ^ The name of the with-function.+  -> Telescope   -- ^ The arguments of the with function before the with exprs.+  -> Telescope   -- ^ The arguments of the with function after the with exprs.+  -> Nat         -- ^ The number of with expressions.+  -> [I.NamedArg Pattern] -- ^ The parent patterns.+  -> Permutation -- ^ Permutation to split into needed and unneeded vars.+  -> Permutation -- ^ Permutation reordering the variables in parent patterns.+  -> TCM DisplayForm withDisplayForm f aux delta1 delta2 n qs perm@(Perm m _) lhsPerm = do-  topArgs <- raise (n + size delta1 + size delta2) <$> getContextArgs++  -- Compute the arity of the display form.+  let arity0 = n + size delta1 + size delta2+  -- The currently free variables have to be added to the front.+  topArgs <- raise arity0 <$> getContextArgs+  let top    = genericLength topArgs+      arity  = arity0 + top++  -- Build the rhs of the display form.   x <- freshNoName_   let wild = Def (qualify (mnameFromList []) x) []+      -- Building the arguments to the with function+      (ys0, ys1) = splitAt (size delta1) (permute perm $ map Just [m - 1, m - 2..0])+      ys = reverse $ ys0 ++ genericReplicate n Nothing ++ ys1    let tqs = patsToTerms lhsPerm qs-      top = genericLength topArgs       vs = map (fmap DTerm) topArgs ++ applySubst (sub top ys wild) tqs-      dt = DWithApp (DDef f vs : map DTerm withArgs) []       withArgs = map var $ genericTake n $ downFrom $ size delta2 + n---      withArgs = reverse $ map var [size delta2..size delta2 + n - 1]-      pats = genericReplicate (n + size delta1 + size delta2 + top) (var 0)-      -- Building the arguments to the with function-      (ys0, ys1) = splitAt (size delta1) (permute perm $ map Just [m - 1, m - 2..0])-      ys = reverse $ ys0 ++ genericReplicate n Nothing ++ ys1+      dt = DWithApp (DDef f vs) (map DTerm withArgs) [] -  let display = Display (n + size delta1 + size delta2 + top) pats dt+  -- Build the lhs of the display form.+  -- @var 0@ is the pattern variable (hole).+  let pats = genericReplicate arity (var 0)++  let display = Display arity pats dt       addFullCtx = addCtxTel delta1                  . flip (foldr addCtxString_) (map ("w" ++) $ map show [1..n])                  . addCtxTel delta2
src/full/Agda/Utils/List.hs view
@@ -44,16 +44,12 @@   loop [a]      = ([], a)   loop (a : as) = mapFst (a:) $ loop as --- | Lookup function (safe).-+-- | Lookup function (partially safe). (!!!) :: [a] -> Int -> Maybe a-[]     !!! _ = Nothing-(x:xs) !!! 0 = Just x-(x:xs) !!! n = xs !!! predecessor n--predecessor n-  | n > 0     = n - 1-  | otherwise = __IMPOSSIBLE__+_        !!! n | n < 0 = __IMPOSSIBLE__+[]       !!! _         = Nothing+(x : _)  !!! 0         = Just x+(_ : xs) !!! n         = xs !!! (n - 1)  -- | downFrom n = [n-1,..1,0] downFrom :: Integral a => a -> [a]